ADD-MATCH-FREE-OVERRIDE

set :match-free value to :once or :all in 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 :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)). 

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.