Major Section: NOTE-2-7
ACL2 now has a more powerful technique for relieving a :rewrite or
: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
of :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-package form. 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
of a :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))
; 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)))
Before Version_2.7, the proof of the thm above fails. When the
:forward-chaining rule transitivity-of-op binds x to a and
y to b, it then looks for an instance of (op y z) in the current
context, with y bound to b but z unbound. 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
see bind-free-examples.
With the addition of bind-free (mentioned above), syntaxp has
become a macro, although that change should be transparent to the user. More
importantly, the argument of syntaxp may now refer to variables mfc
and state, giving 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.
Some trace utilities have been made available in the ACL2 loop.
o Function
trace$(and alsountrace$) calls the corresponding underlying Lisp routinetrace(anduntrace), which however continues (as it has for some time) to be enhanced for GCL and Allegro CL.o Macro
open-trace-filecauses trace output to go to a specified file. Macroclose-trace-filecauses trace output to go to the screen (which is the default).o Macro
with-error-trace(or,wetfor short) causes a backtrace to be written out for many failures, including guard violations. See trace, see trace$, and see wet.
A new theory, minimal-theory has been provided (see theories).
It can be particularly useful for speeding up proofs involving :use
hints.
New events defund and defthmd behave exactly like
defun and 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.
The form (pstack) 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
initial implementation.
The new command :comp-gcl is identical in functionality, except
that it always leaves .c and .h files when compiling in GCL. Thanks
to Rob Sumners and Vernon Austel for suggesting such a capability.
The macro e/d provides a convenient way to enable some rules and
disable others. It was formerly in a book supplied with the
distribution, books/ihs/ihs-init.lisp, written by Bishop Brock (who we
thank for providing this useful macro).
New distributed books include those in books/ordinals/,
books/rtl/rel3/, and books/misc/simplify-defuns.lisp (which is
documented in books/misc/simplify-defuns.txt).
The :expand hint now accepts a special value, :LAMBDAS, that tells
the ACL2 rewriter to expand all lambda applications (let expressions).
See hints.
A new function zpf has been added as fast test against 0 for
nonnegative fixnums.
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
improvement.
The second argument of certify-book, if supplied, formerly had to be
either t or a non-negative integer. Now it can be the symbol ?, in
the 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.