Major Section: BREAK-REWRITE
Example: :brr t ; enable :brr nil ; disablewhere
General Form: (brr flg)
nil. This function modifies
stateso that the attempted application of certain rewrite rules are ``broken.'' ``
Brr'' stands for ``break-rewrite'' and can be thought of as a mode with two settings. The normal mode is ``disabled.''
brr mode is ``enabled'' the ACL2 rewriter monitors the attempts
to apply certain rules and advises the user of those attempts by
entering an interactive wormhole break. From within this break the
user can watch selected application attempts.
The rules monitored are selected by using the
commands. It is possible to break a rune ``conditionally'' in the
sense that an interactive break will occur only if a specified
predicate is true of the environment at the time of the attempted
application. See monitor and see unmonitor.
Even if a non-empty set of rules has been selected, no breaks will
brr mode is enabled. Thus, the first time in a session
that you wish to monitor a rewrite rule, use
t to enable
mode. Thereafter you may select runes to be monitored with
unmonitor with the effect that whenever monitored rules are
tried (and their break conditions are met) an interactive break will
occur. Be advised that when
brr mode is enabled the rewriter is
somewhat slower than normal. Furthermore, that sluggishness
persists even if no runes are monitored. You may regain normal
performance -- regardless of what runes are monitored -- by
brr mode with
brr mode disabled automatically when no runes are
monitored? More generally, why does ACL2 have
brr mode at all? Why
not just test whether there are monitored runes? If you care about
the answers, see why-brr.