Set :match-free value to :once or :all in existing
(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.
; 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 :once or
:match-free :all in the :rule-classes of the rule, or by
using the most recent set-match-free-default event. 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 :all 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)).
(add-match-free-override flg t)
(add-match-free-override flg rune1 rune2 ... runek)
where flg is :once or :all and the runei are runes. If :clear is specified then all rules will have the
:all/:once behavior from when they were first stored. The second
general form causes all rewrite linear, and forward-chaining rules to have the behavior specified by flg (:all
or :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 add-match-free-override events).
At the conclusion of this event, ACL2 prints out the list of all
:linear, :rewrite, and :forward-chaining 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 or encapsulate form in which it occurs.
Lists of the :rewrite, :linear, and :forward-chaining runes whose behavior was originally :once or
:all are returned by the following forms, respectively.
(free-var-runes :once (w state))
(free-var-runes :all (w state))
(match-free-override (w state))
evaluates to a pair, whose car is a number used by ACL2 to
determine whether a rune is sufficiently old to be affected by the
override, and whose cdr is the list of runes whose behavior is
specified as :once by add-match-free-override; except, if no runes
have been overridden, then the keyword :clear is returned.