Set the default rw-cache-state
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 its behavior to be modified or even disabled by changing the so-called rw-cache-state. 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)
The following example illustrates the rw-cache in action. You will see a
break during evaluation of the thm form. Type
(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