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 tat 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
ACL2 !>:monitor (:rewrite lemma12 . 2) twill 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
tis replaced by an expression that evaluates to non-
nilwhen 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
monitoron each rule. You may also change the break condition on a rule with
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 nilThe 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:
The loop in the rewriter will probably be evident!
(cw-gstack *deep-gstack* state)