Major Section: NOTE-2-7
ACL2 now has a more powerful technique for relieving a
linear rule's hypothesis that contains free variables. A new
documentation section has been written describing the handling free
variables in rules; see free-variables. In brief, the primary change is
that when a free-variable match for the current hypothesis fails to allow
subsequent hypotheses to be relieved, then additional matches may be
attempted until they have all been tried. Also see rule-classes (discussion
:match-free). Also see set-match-free-error,
see set-match-free-default, and see add-match-free-override for interfaces
provided to the user for controlling the way ACL2 deals with free variables
in hypotheses. We thank Rob Sumners for several helpful discussions about
the designs of those interfaces, as well as Eric Smith and Robert Krug for
helpful related discussions. Robert Krug also found a performance bug in a
preliminary version, for which we are grateful.
WARNING: Book certification attempts may take much longer now that, by default, ACL2 looks for more free variable matches (see paragraph just above). You can get the old behavior by inserting the form
(set-match-free-default :once)just after the initial
in-packageform. However, rules from included books that have free variables can still slow down certification. This can be fixed by inserting
(add-match-free-override :once t)before the first event in the file that generates a proof.
Forward-chaining has been made more powerful in the presence of free
variables (see free-variables), thanks to a contribution by Erik Reeber.
Both before and now, when an attempt is made to relieve (prove) a hypothesis
:forward-chaining rule in the case that at least one variable in
that hypothesis is not yet bound, ACL2 looks in the current context for an
instance of that hypothesis. If it finds one, then it binds the unbound
variables and continues to the next hyopothesis. What is new is that ACL2
can now looks for multiple instances of that hypothesis. Consider the
following example; an explanation is below.
(encapsulate (((op * *) => *)) (local (defun op (x y) (< x y))) (defthm transitivity-of-op (implies (and (op x y) (op y z)) (op x z)) :rule-classes :forward-chaining))Before Version_2.7, the proof of the
; fails in Version_2.6; succeeds in in Version_2.7 (thm (implies (and (op a b) (op b c) (op b e)) (op a c)))
thmabove fails. When the
b, it then looks for an instance of
(op y z)in the current context, with
zunbound. It happens to find
(op b e)before
(op b c), and it then adds
(op a e)to the context. But starting with Version_2.7, it continues to look for additional instances and finds
(op b c)in the context as well, chaining forward to
(op a c)and thus proving the theorem.
A new macro,
bind-free, provides a simple way to get much or most of
the power of metafunctions. Thanks to Eric Smith for coming up with the
idea and to Robert Krug for providing an implementation (which we modified
only very slightly) and documentation. See bind-free and
With the addition of
bind-free (mentioned above),
become a macro, although that change should be transparent to the user. More
importantly, the argument of
syntaxp may now refer to variables
syntaxp some of the power of extended metafunctions;
see syntaxp and see extended-metafunctions. Thanks to Robert Krug for
implementing that extension. Also, the argument of
syntaxp may now
include calls of
program mode functions. See syntaxp and
see syntaxp-examples (thanks to Robert Krug for updating the former and
creating the latter documentation).
The linear-arithmetic decision procedure (see linear-arithmetic) has now been extended so that ACL2 can reason about non-linear arithmetic as well (see non-linear-arithmetic for how to turn on this feature). We thank Robert Krug for the initial implementation of this, and Eric Smith for finding a couple of bugs in it.
trace utilities have been made available in the ACL2 loop.
untrace$) calls the corresponding underlying Lisp routine
untrace), which however continues (as it has for some time) to be enhanced for GCL and Allegro CL.
open-trace-filecauses trace output to go to a specified file. Macro
close-trace-filecauses trace output to go to the screen (which is the default).
wetfor short) causes a backtrace to be written out for many failures, including guard violations. See trace, see trace$, and see wet.
minimal-theory has been provided (see theories).
It can be particularly useful for speeding up proofs involving
defthmd behave exactly like
defthm, respectively, except that these new events
disable the new name.
The new macro
with-output can be used to suppress output that would
normally result from evaluation of a form.
) can give the user an idea of what the
prover has been up to during a proof, or after a user-aborted proof.
Moreover, by evaluating
(verbose-pstack t) (see verbose-pstack)
one can get trace-like information about prover functions, including
time summaries, printed to the screen during a proof. Thanks to Bill Legato
and Robert Krug for initiating this work and to Robert for providing some
The new command
comp-gcl is identical in functionality, except
that it always leaves
.h files when compiling in GCL. Thanks
to Rob Sumners and Vernon Austel for suggesting such a capability.
e/d provides a convenient way to
enable some rules and
disable others. It was formerly in a book supplied with the
books/ihs/ihs-init.lisp, written by Bishop Brock (who we
thank for providing this useful macro).
New distributed books include those in
books/misc/simplify-defuns.lisp (which is
:expand hint now accepts a special value,
:LAMBDAS, that tells
the ACL2 rewriter to expand all lambda applications (
A new function
zpf has been added as fast test against 0 for
A new macro
gc$ allows the user to call the garbage collector of the
underlying Common Lisp. Thanks to Rob Sumners for suggesting this feature.
It is now possible to
monitor simple (abbreviation) rules.
However, as a warning explains, they are still not considered monitored
during preprocessing; see monitor. Thanks to Robert Krug for providing this
The second argument of
certify-book, if supplied, formerly had to be
t or a non-negative integer. Now it can be the symbol
ACL2 package, indicating that the usual check should be suppressed on
the number of commands that have been executed to create the world in which
certify-book was called.