Major Section: RELEASE-NOTES
ACL2 can now use Ordered Binary Decision Diagram technology.
See bdd. There is also a proof-checker bdd command.
ACL2 is now more respectful of the intention of the function
hide. In particular, it is more careful not to dive inside any
call of hide during equality substitution and case splitting.
The ld special (see ld) ld-pre-eval-print may now be used
to turn off printing of input forms during processing of
encapsulate and certify-book forms, by setting it to the value
:never, i.e., (set-ld-pre-eval-print :never state).
See ld-pre-eval-print.
The TUTORIAL documentation section has, with much help from Bill Young, been substantially improved to a bona fide introduction, and has been renamed acl2-tutorial.
The term pretty-printer has been modified to introduce (<= X Y)
as an abbreviation for (not (< Y X)).
Forward chaining and linear arithmetic now both benefit from the evaluation of ground subterms.
A new macro set-inhibit-output-lst has been defined. This should
be used when setting the state global inhibit-output-lst;
see set-inhibit-output-lst and see proof-tree.
The test for redundancy in definitions includes the guard and type declarations. See redundant-events.
See generalized-booleans for a discussion of a potential soundness problem for ACL2 related to the question: Which Common Lisp functions are known to return Boolean values?
Here we will put some less important changes, additions, and so on.
A bug has been fixed so that now, execution of :comp t
(see comp) correctly handles non-standard characters.
A bug in digit-char-p has been fixed, so that the ``default'' is
nil rather than 0.
True-listp now tests the final cdr against nil using eq
instead of equal, for improved efficiency. The logical meaning
is, however, unchanged.
Put-assoc-equal has been added to the logic (it used to have
:defun-mode :program, and has been documented.
Major Section: RELEASE-NOTES
By default, when the system is started it is illegal to use the
variable STATE as a formal parameter of a function definition.
The aim is to prevent novice users from stumbling into the Byzantine
syntactic restrictions on that variable symbol. Use
:set-state-ok tor, equivalently,
(set-state-ok t)to switch back to the old default mode. See set-state-ok
Set-state-ok is an event that affects the ACL2 defaults table
(see acl2-defaults-table). Recall that when books are
included, the defaults table is restored to its pre-inclusion state.
Thus, while a set-state-ok form will permit the book to define a
state-using function, it will not permit the user of the book to
make such a definition. We recommend putting (set-state-ok t) in
any book that defines a state using function.
Books certified under Version 1.8 must be recertified under Version 1.9. See :DOC version.
The simplifier has been made to look out for built-in clauses,
whereas in past versions such clauses were only noticed by the
``preprocessor'' at the top of the waterfall. THIS CHANGE MAY
PREVENT OLD SCRIPTS FROM REPLAYING! The undesirable side-effect is
caused by the fact that :HINTS require you to refer to clauses by
their exact name (see goal-spec) and because the new simplifier
proves more clauses than before, the goals produced have different
names. Thus, if a script uses :HINTS that refer to clauses other
than "Goal", e.g., "Subgoal 1.3" then the hint may be applied to
a different subgoal than originally intended.
The use of built-in-clauses has been made more efficient. If a set of clauses arise often in a piece of work, it might be advantageous to build them in even if that results in a large set (hundreds?) of built-in clauses. See built-in-clauses
Wormholes can now be used in :logic mode functions. See wormhole
It is now possible to provide ``computed hints.'' For example, have you ever wished to say ``in all goals with a name like this, :use that'' or ``if this term is in the subgoal, then :use that''? Well, see computed-hints and the extraordinarily long example in see using-computed-hints.
Hide terms may be rewritten with :rewrite rules about hide.
See hide, where we also now explain why hide terms are sometimes
introduced into your proof attempts.
A bug that sometimes caused the ``non-lazy IF'' hard error message was fixed.
A bug that sometimes caused a hard error in forward chaining was fixed.
A bug in print-rules (:pr) was fixed.
We report the use of :executable-counterparts in the evaluation of SYNTAXP forms.
Some documentation errors were fixed.
A bug in parent-tree tracking in add-literal-and-pt was fixed.
A bug in ok$, go$ and eval$ was fixed.
Clausify now optimizes (mv-nth 'k (list x0 ... xk ... xn)) to xk.
Major Section: RELEASE-NOTES
Important changes to non-standard version:
Please see note-2-5 for changes to Version 2.5 of ACL2. We hope to write more documentation for ACL2(r) in the future.