BREAK-LEMMA

a quick introduction to breaking rewrite rules in ACL2 
Major Section:  BREAK-REWRITE


Example:
:brr t                          ; if you haven't done that yet
:monitor (:rewrite lemma12) t   ; to install a break point on the
                                ; rule named (:rewrite lemma12)

ACL2 does not support Nqthm's break-lemma but supports a very similar and more powerful break facility. Suppose some proof is failing; apparently some particular rule is not being used and you wish to learn why. Then you need the ACL2 break-rewrite facility. See break-rewrite and all of its associated :doc topics for details. The following basic steps are required.

(1) To enable the ``break rewrite'' feature, you must first execute 

ACL2 !>:brr t
at the top-level of ACL2. Equivalently, evaluate (brr t). Break-rewrite stays enabled until you disable it with (brr nil). When break-rewrite is enabled the ACL2 rewriter will run slower than normal but you will be able to monitor the attempts to apply specified rules.

(2) Decide what runes (see rune) you wish to monitor. For example, you might want to know why (:rewrite lemma12 . 2) is not being used in the attempted proof. That, by the way, is the name of the second rewrite rule generated from the event named lemma12.

The command 

ACL2 !>:monitor (:rewrite lemma12 . 2) t
will install an ``unconditional'' break point on that rule. The ``t'' at the end of the command means it is unconditional, i.e., a break will occur every time the rule is tried. ACL2 supports conditional breaks also, in which case the t is replaced by an expression that evaluates to non-nil when you wish for a break to occur. See monitor. The above keyword command is, of course, equivalent to 
ACL2 !>(monitor '(:rewrite lemma12 . 2) t)
which you may also type. You may install breaks on as many rules as you wish. You must use monitor on each rule. You may also change the break condition on a rule with monitor. Use unmonitor (see unmonitor) to remove a rule from the list of monitored rules.

(3) Then try the proof again. When a monitored rule is tried by the rewriter you will enter an interactive break, called break-rewrite. See break-rewrite for a detailed description. Very simply, break-rewrite lets you inspect the context of the attempted application both before and after the attempt. When break-rewrite is entered it will print out the ``target'' term being rewritten. If you type :go break-rewrite will try the rule and then exit, telling you (a) whether the rule was applied, (b) if so, how the target was rewritten, and (c) if not, why the rule failed. There are many other commands. See brr-commands.

(4) When you have finished using the break-rewrite feature you should disable it to speed up the rewriter. You can disable it with 

ACL2 !>:brr nil
The list of monitored rules and their break conditions persists but is ignored. If you enable break-rewrite later, the list of monitored rules will be displayed and will be used again by rewrite.

You should disable the break-rewrite feature whenever you are not intending to use it, even if the list of monitored rules is empty, because the rewriter is slowed down as long as break-rewrite is enabled.

Finally, a wonderful trick is the following. When there is a stack overflow, abort the proof and then try it again after turning on rewrite stack monitoring with :brr t. Then, provoke the stack overflow again. Quit the ACL2 top-level loop and execute the following form in raw Lisp: 



  (cw-gstack *deep-gstack* state)
The loop in the rewriter will probably be evident!