:allin existing rules
Major Section: EVENTS
Example Forms: (add-match-free-override :once t) ; try only the first binding of free variables when relieving hypotheses (add-match-free-override :all (:rewrite foo) (:rewrite bar)) ; for rewrite rules foo and bar, try all bindings of free variables when ; relieving hypotheses (add-match-free-override :clear) ; restore :match-free to what was originally stored for each rule (either ; :all or :once)As described elsewhere (see free-variables), a rewrite or linear rule may have free variables in its hypotheses, and ACL2 can be directed either to try all bindings (``
:all'') or just the first (``
:once'') when relieving a hypothesis, as a basis for relieving subsequent hypotheses. This direction is generally provided by specifying either
:match-free :allin the
rule-classesof the rule, or by using the most recent
set-match-free-defaultevent. Also see rule-classes.
However, if a proof is going slowly, you may want to modify the behavior of
existing rewrite or linear rules so that they use only the first
match for free variables in a hypothesis when relieving subsequent
hypotheses, rather than backtracking and trying additional matches as
necessary. The event
(add-match-free-override :once t) has that effect.
Or at the other extreme, perhaps you want to specify all rules as
rules except for a some specific exceptions. Then you can execute
(add-match-free-override :all t) followed by, say,
(add-match-free-override :once (:rewrite foo) (:linear bar)).
General Forms: (add-match-free-override :clear) (add-match-free-override flg t) (add-match-free-override flg rune1 rune2 ... runek)where
:clearis specified then all rules will have the
:oncebehavior from when they were first stored. The second general form causes all rewrite and linear rules to have the behavior specified by
:once). Finally, the last of these, where runes are specified, is additive in the sense that only the indicated rules are affected; all others keep the behavior they had just before this event was executed (possible because of earlier
At the conclusion of this event, ACL2 prints out the list of all
rewrite runes whose rules contain free
variables in hypotheses that are to be bound
:once, except that if there
are no overrides (value
:clear was used), then
:clear is printed.
This event only affects rules that exist at the time it is executed. Future rules are not affected by the override.
Note: This is an event! It does not print the usual event summary
but nevertheless changes the ACL2 logical world and is so
recorded. It uses the
acl2-defaults-table, and hence its effect is
local to the book in which it occurs.
Lists of the
linear runes whose
behavior was originally
:all are returned by the following
(free-var-runes :once (w state)) (free-var-runes :all (w state))The form
(match-free-override (w state))evaluates to a pair, whose
caris a number used by ACL2 to determine whether a rune is sufficiently old to be affected by the override, and whose
cdris the list of runes whose behavior is specified as
add-match-free-override; except, if no runes have been overridden, then the keyword