NOTE-2-7-NEW-FUNCTIONALITY

ACL2 Version 2.7 Notes on New Functionality 
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 also untrace$) calls the corresponding underlying Lisp routine trace (and untrace), which however continues (as it has for some time) to be enhanced for GCL and Allegro CL.

o Macro open-trace-file causes trace output to go to a specified file. Macro close-trace-file causes trace output to go to the screen (which is the default).

o Macro with-error-trace (or, wet for 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 (checkpoints) 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 (print-checkpoints t) (see print-checkpoints) one can get trace-like information about prover functions, including time summaries, printed to the screen during a proof.

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.