SET-RW-CACHE-STATE

set the default rw-cache-state 
Major Section:  SWITCHES-PARAMETERS-AND-MODES

The ACL2 rewriter uses a data structure, called the rw-cache (rewriter cache), to save failed attempts to apply conditional rewrite rules. The regression suite has taken approximately 11% less time with this mechanism. The rw-cache is active by default but this event allows it to be turned off or modified. Note that this event is local to its context (from encapsulate or include-book). For a non-local version, use set-rw-cache-state!.

Example forms:
(set-rw-cache-state :atom)     ; default: rw-cache cleared for each literal
                               ;   (i.e., hypothesis or conclusion of a goal)
(set-rw-cache-state nil)       ; rw-cache is inactive
(set-rw-cache-state t)         ; rw-cache persists beyond each literal
(set-rw-cache-state :disabled) ; rw-cache is inactive, but the rw-cache-state
                               ;   transitions to state t after
                               ;   simplification takes place

General Form:
(set-rw-cache-state val)
where val evaluates to one of the four values shown in ``Example forms'' above. The default is :atom, which enables the rw-cache but clears it before rewriting a hypothesis or conclusion of any goal. The value t is provides more aggresive use of the rw-cache, basically preserving the rw-cache when there is a single subgoal. The value :disabled is the same as t, except that the rw-cache is initially inactive and only becomes active when some simplification has taken place. We have seen a few cases where value t will make a proof fail but :disabled does not.

The following example illustrates the rw-cache in action. You will see a break during evaluation of the thm form. Type :eval and you will see a failed rewriting attempt. Type :go to continue, and at the next break type :eval again. This time you will see the same failed rewriting attempt, but this time labeled with a notation saying that the failure was cached earlier, which indicates that this time the rewriter did not even attempt to prove the hypothesis of the rewrite rule f1->f2.

(defstub f1 (x) t)
(defstub f2 (x) t)
(defaxiom f1->f2
         (implies (f1 x) (equal (f2 x) t)))
:brr t
:monitor (:rewrite f1->f2) t
(thm (equal (car (f2 a)) (cdr (f2 a))))

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 is local to the book or encapsulate form in which it occurs (see set-rw-cache-state! for a corresponding non-local event).

We also note that rw-cache-state changes may also be caused at the subgoal level; see hints.

We welcome you to experiment with different rw-cache states. If the more aggressive values of t and :disabled cause proofs to fail, then you can revert to the default of :atom or even turn off the rw-cache using (set-rw-cache-state nil). We don't expect users to need a deep knowledge of the rw-cache in order to do such experiments, but readers interested in details of the rw-cache implementation are invited to read the ``Essay on Rw-cache'' in the ACL2 source code.