:match-free value to :once or :all in existing rules
Major Section: EVENTS
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 :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. 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)).
General Forms: (add-match-free-override :clear) (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.
Remarks
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))The form
(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.
