:allin existing rules
Major Section: SWITCHES-PARAMETERS-AND-MODES
Example Forms: (add-match-free-override :once t) ; Try only the first binding of free variables when relieving hypotheses ; of any rule of class :rewrite, :linear, or :forward-chaining. (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, linear, or forward-chaining 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
some such 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. (But note:
add-match-free-override is not relevant for type-prescription
rules.) The event
(add-match-free-override :once t) has that effect. Or
at the other extreme, perhaps you want to specify all rules as
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 linear, and forward-chaining 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
whose rules contain free variables in hypotheses that are to be bound
:once, except that if there are no overrides (value
:clear was used),
: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 or
encapsulate form in which it occurs.
Lists of the
forward-chaining runes whose behavior was originally
:all are returned by the following forms, respectively.
(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