This is documentation for ACL2 Version 3.2
Copyright (C) 2007  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

Written by:  Matt Kaufmann and J Strother Moore
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.

DEFAULT-HINTS-TABLE    a table used to provide hints for proofs

Please see SET-DEFAULT-HINTS, see ADD-DEFAULT-HINTS, and
see REMOVE-DEFAULT-HINTS for how to use this table.  For
completeness, we mention here that under the hood, these events all
update the default-hints-table by updating its unique key, t, for
example as follows.

     (table default-hints-table t
            '((computed-hint-1 clause)
              (computed-hint-2 clause
                               stable-under-simplificationp)))

The use of default hints is explained elsewhere; see
SET-DEFAULT-HINTS.

DELETE-INCLUDE-BOOK-DIR    remove association of keyword for include-book's :dir argument

     Example Forms:
     (delete-include-book-dir :smith)
      ; Remove association of directory with :smith for include-book.

     General Form:
     (delete-include-book-dir kwd)

where kwd is a keywordp.  The effect of this event is to modify the
meaning of the :dir keyword argument of include-book as indicated by
the examples above, namely by removing association of any directory with
the indicated keyword for purposes of the include-book :dir argument.
Normally one would instead use add-include-book-dir to associate a new
directory with that keyword; see ADD-INCLUDE-BOOK-DIR.

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.

This macro generates a call (table acl2-defaults-table
:include-book-dir-alist ...)  and hence is local to any books and
encapsulate events in which it occurs. See ACL2-DEFAULTS-TABLE.

DIVE-INTO-MACROS-TABLE    right-associated function information for the proof-checker

     Examples:
     ACL2 !>(dive-into-macros-table (w state))
     ((CAT . EXPAND-ADDRESS-CAT)
      (LXOR . EXPAND-ADDRESS-LXOR)

This table associates macro names with functions used by the
proof-checker's DV and numeric diving commands (e.g., 3) in order to
dive properly into subterms.  See PROOF-CHECKER, in particular
the documentation for DV.

This table can be extended easily.  See ADD-DIVE-INTO-MACRO and
also see REMOVE-DIVE-INTO-MACRO.

The symbol associated with a macro should be a function symbol taking
four arguments, in this order:

     car-addr ; the first number in the list given to the proof-checker's
                DV command
     raw-term ; the untranslated term into which we will dive
     term     ; the translated term into which we will dive
     wrld     ; the current ACL2 logical world

The function will normally return a list of positive integers,
representing the (one-based) address for diving into term that
corresponds to the single-address dive into raw-term by car-address.
However, it can return (cons str alist), where str is a string suitable
for fmt and args is the corresponding alist for fmt.

Referring to the example above, expand-address-cat would be such a
function, which will be called on raw-term values that are calls of
cat.  See the distributed book books/misc/rtl-untranslate.lisp for the
definition of such a function.

See TABLE for a general discussion of tables.

INVISIBLE-FNS-TABLE    functions that are invisible to the loop-stopper algorithm

     Examples:
     ACL2 !>(invisible-fns-table (w state))
     ((binary-+ unary--)
      (binary-* unary-/)
      (unary-- unary--)
      (unary-/ unary-/))

Among other things, the setting above has the effect of making unary-
"invisible" for the purposes of applying permutative :rewrite rules to
binary-+ trees.  Also see ADD-INVISIBLE-FNS, see
REMOVE-INVISIBLE-FNS, and see SET-INVISIBLE-FNS-TABLE.

See TABLE for a general discussion of tables.

The "invisible functions table" is an alist with elements of the
following form, where fn is a function symbol and the ufni are unary
function symbols in the current ACL2 world, and k is at least 1.

     (fn ufn1 ufn2 ... ufnk)

This table thus associates with certain function symbols, e.g., fn
above, a set of unary functions, e.g., the ufni above.  The ufni
associated with fn in the invisible functions table are said to be
"invisible with respect to fn."  If fn is not the car of any pair in
the alist, then no function is invisible for it.  Thus for example,
setting the invisible functions alist to nil completely eliminates the
consideration of invisibility.

The notion of invisibility is involved in the use of the :loop-stopper
field of :rewrite rules to prevent the indefinite application of
permutative rewrite rules.  Roughly speaking, if rewrite rules are
being used to permute arg and (ufni arg) inside of a nest of fn calls,
and ufni is invisible with respect to fn, then arg and (ufni arg) are
considered to have the same "weight" and will be permuted so as to end
up as adjacent tips in the fn nest.  See LOOP-STOPPER.

LOGIC    to set the default defun-mode to :logic

     Example:
     ACL2 p!>:logic
     ACL2 !>

Typing the keyword :logic sets the default defun-mode to :logic.

Functions defined in :logic mode are logically defined.  See
DEFUN-MODE.

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.

See DEFUN-MODE for a discussion of the defun-modes available
and what their effects on the logic are.  See
DEFAULT-DEFUN-MODE for a discussion of how the default defun-mode is
used.  This event is equivalent to (table acl2-defaults-table
:defun-mode :logic), and hence is local to any books and encapsulate
events in which it occurs. See ACL2-DEFAULTS-TABLE.

Recall that the top-level form :logic is equivalent to (logic); see
KEYWORD-COMMANDS.  Thus, to change the default defun-mode to
:logic in a book, use (logic), which is an embedded event form, rather
than :logic, which is not a legal form for books.  See
EMBEDDED-EVENT-FORM.

MACRO-ALIASES-TABLE    a table used to associate function names with macro names

     Example:
     (table macro-aliases-table 'append 'binary-append)

This example associates the function symbol binary-append with the
macro name append.  As a result, the name append may be used as a runic
designator (see THEORIES) by the various theory functions.
Thus, for example, it will be legal to write

     (in-theory (disable append))

as an abbreviation for

     (in-theory (disable binary-append))

which in turn really abbreviates

     (in-theory (set-difference-theories (current-theory :here)
                                         '(binary-append)))

     General Form:

     (table macro-aliases-table 'macro-name 'function-name)

or very generally

     (table macro-aliases-table macro-name-form function-name-form)

where macro-name-form and function-name-form evaluate, respectively, to
a macro name and a function name in the current ACL2 world.  See
TABLE for a general discussion of tables and the table event used to
manipulate tables.

The table macro-aliases-table is an alist that associates macro symbols
with function symbols, so that macro names may be used as runic
designators (see THEORIES).  For a convenient way to add
entries to this table, see ADD-MACRO-ALIAS.  To remove entries
from the table with ease, see REMOVE-MACRO-ALIAS.

This table is used by the theory functions.  For example, in order that
(disable append) be interpreted as (disable binary-append), it is
necessary that the example form above has been executed.  In fact, this
table does indeed associate many of the macros provided by the ACL2
system, including append, with function symbols.  Loosely speaking, it
only does so when the macro is "essentially the same thing as" a
corresponding function; for example, (append x y) and (binary-append x
y) represent the same term, for any expressions x and y.

NTH-ALIASES-TABLE    a table used to associate names for nth/update-nth printing

     Example:
     (table nth-aliases-table 'st0 'st)

This example associates the symbol st0 with the symbol st.  As a
result, when the theorem prover prints terms of the form (nth n st0) or
(update-nth n val st0), where st is a stobj whose nth accessor function
is f-n, then it will print n as *f-n*.

     General Form:
     (table nth-aliases-table 'alias-name 'name)

This event causes alias-name to be treated like name for purposes of
the printing of terms that are calls of nth and update-nth.  (Note
however that name is not recursively looked up in this table.)  Both
must be symbols other than state.  See TERM, in particular the
discussion there of untranslated terms.

For a convenient way to add entries to this table, see
ADD-NTH-ALIAS.  To remove entries from the table with ease, see
REMOVE-NTH-ALIAS.

PROGRAM    to set the default defun-mode to :program

     Example:
     ACL2 !>:program
     ACL2 p!>

Typing the keyword :program sets the default defun-mode to :program.

Functions defined in :program mode are logically undefined but can be
executed on constants outside of deductive contexts.  See
DEFUN-MODE.

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.

See DEFUN-MODE for a discussion of the defun-modes available
and what their effects on the logic are.  See
DEFAULT-DEFUN-MODE for a discussion of how the default defun-mode is
used.  This event is equivalent to (table acl2-defaults-table
:defun-mode :program), and hence is local to any books and encapsulate
events in which it occurs. See ACL2-DEFAULTS-TABLE.

Recall that the top-level form :program is equivalent to (program); see
KEYWORD-COMMANDS.  Thus, to change the default defun-mode to
:program in a book, use (program), which is an embedded event form,
rather than :program, which is not a legal form for books.  See
EMBEDDED-EVENT-FORM.

PUSH-UNTOUCHABLE    add name or list of names to the list of untouchable symbols

     Examples:
     (push-untouchable my-var nil)
     (push-untouchable set-mem t)

     General Form:
     (push-untouchable name{s}  fn-p :doc doc-string)

where name{s} is a non-nil symbol or a non-nil true list of symbols,
fn-p is any value (but generally nil or t), and doc-string is an
optional documentation string not beginning with ":doc-section ...".
If name{s} is a symbol it is treated as the singleton list containing
that symbol.  The effect of this event is to union the given symbols
into the list of "untouchable variables" in the current world if fn-p is
nil, else to union the symbols into the list of "untouchable
functions".  This event is redundant if every symbol listed is already
a member of the appropriate untouchables list (variables or functions).

When a symbol is on the untouchables list it is syntactically illegal
for any event to call a function or macro of that name, if fn-p is
non-nil, or to change the value of a state global variable of that
name, if fn-p is nil.  Thus, the effect of pushing a function symbol,
name, onto untouchables is to prevent any future event from using that
symbol as a function or macro, or as a state global variable (according
to fn-p).  This is generally done to "fence off" some primitive
function symbol from "users" after the developer has used the symbol
freely in the development of some higher level mechanism.

REMOVE-BINOP    remove the association of a binary function name with a macro name

     Example:
     (remove-binop binary-append)

     General Form:
     (remove-binop binop)

See ADD-BINOP for a discussion of how to associate a macro name
with a binary function name for proof output purposes.  This form sets
binop-table to the result of deleting the association of a macro name
with the given binary function name.  If the function name has no such
association, then this form still generates an event, but the event has
no real effect.

REMOVE-DEFAULT-HINTS    remove from the default hints

     Examples:
     (remove-default-hints '((computed-hint-1 clause)
                             (computed-hint-2 clause
                                              stable-under-simplificationp)))

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.  It is
local to the book or encapsulate form in which it occurs (see
REMOVE-DEFAULT-HINTS! for a corresponding non-local event).

     General Form:
     (remove-default-hints lst)

where lst is a list.  Generally speaking, the elements of lst should be
suitable for use as computed-hints.  Also see ADD-DEFAULT-HINTS.

If some elements of the given list do not belong to the existing default
hints, they will simply be ignored by this event.

Finally, note that the effects of set-default-hints, add-default-hints,
and remove-default-hints are local to the book in which they appear.
Thus, users who include a book with such forms will not have their
default hints affected by such forms.  In order to export the effect of
setting the default hints, use set-default-hints!, add-default-hints!,
or remove-default-hints!.

REMOVE-DEFAULT-HINTS!    remove from the default hints non-locally

Please see REMOVE-DEFAULT-HINTS, which is the same as
remove-default-hints!  except that the latter is not local to the
encapsulate or the book in which it occurs.  Probably
remove-default-hints is to be preferred unless you have a good reason
for wanting to export the effect of this event outside the enclosing
encapsulate or book.

REMOVE-DIVE-INTO-MACRO    removes association of proof-checker diving function with macro name

     Example:
     (remove-dive-into-macro logand)

This feature undoes the effect of add-dive-into-macro, which is used so
that the proof-checker's DV command and numeric diving commands (e.g.,
3) will dive properly into subterms.  Please see
ADD-DIVE-INTO-MACRO and especially see DIVE-INTO-MACROS-TABLE.

REMOVE-INVISIBLE-FNS    make some unary functions no longer invisible

     Examples:
     (remove-invisible-fns (binary-+ unary-- foo)

The setting above has makes unary functions unary- and foo no longer
"invisible" for the purposes of applying permutative :rewrite rules to
binary-+ trees.

     General Form:
     (remove-invisible-fns top-fn unary-fn1 ... unary-fnk)

where top-fn is a function symbol and the unary-fni are unary function
symbols.

See ADD-INVISIBLE-FNS and also see INVISIBLE-FNS-TABLE
and see SET-INVISIBLE-FNS-TABLE.

REMOVE-MACRO-ALIAS    remove the association of a function name with a macro name

     Example:
     (remove-macro-alias append)

     General Form:
     (remove-macro-alias macro-name)

See MACRO-ALIASES-TABLE for a discussion of macro aliases; also
see ADD-MACRO-ALIAS.  This form sets macro-aliases-table to the
result of deleting the key macro-name from that table.  If the name
does not occur in the table, then this form still generates an event,
but the event has no real effect.

REMOVE-NTH-ALIAS    remove the association of one symbol with another for printing of nth/update-nth terms

     Example:
     (remove-nth-alias append)

     General Form:
     (remove-nth-alias alias-name)

See NTH-ALIASES-TABLE for further discussion; also see
ADD-NTH-ALIAS.  This form sets nth-aliases-table to the result of
deleting the key alias-name from that table.  If the name does not
occur in the table, then this form still generates an event, but the
event has no real effect.

REMOVE-UNTOUCHABLE    remove names from lists of untouchable symbols

Also see PUSH-UNTOUCHABLE.

This documentation topic is directed at those who build systems on top
of ACL2.  We first describe a means for removing restrictions related to
so-called "untouchables": functions (or macros) that cannot be called,
or state global variables that cannot be modified or unbound, without
intervention that requires an active trust tag (see DEFTTAG).
Then we describe the remove-untouchable event.

We begin by discussing untouchable state global variables
temp-touchable-vars and temp-touchable-fns, which initially have value
nil.  These can often be used in place of remove-untouchable.  When the
value is t, no variable (respectively, no function or macro) is treated
as untouchable, regardless of the set of initial untouchables or the
remove-untouchable or push-untouchable events that have been admitted.
Otherwise the value of each of these two variables is a symbol-listp,
and no member of this list is treated as an untouchable variable (in
the case of temp-touchable-vars) or as an untouchable function or macro
(in the case of temp-touchable-fns).  These two state global variables
can be set by set-temp-touchable-vars and set-temp-touchable-fns,
respectively, provided there is an active trust tag (see
DEFTTAG).  Here is an illustrative example.  This macro executes the
indicated forms in a context where there are no untouchable variables,
but requires an active trust tag when invoked.

     (defmacro with-all-touchable (&rest forms)
       `(progn!
         (state-global-let*
          ((temp-touchable-vars t set-temp-touchable-vars))
          (progn! ,@forms))))

Finally, the value t for temp-touchable-vars removes the requirement
that built-in state globals cannot be made unbound (with
makunbound-global).

We now turn to the remove-untouchable event, in case the approach above
is for some reason not adequate.  This event is illegal by default,
since it can be used to provide access to ACL2 internal functions and
data structures that are intentionally made untouchable for the user.
If you want to call it, you must first create an active trust tag; see
DEFTTAG.

     Examples:
     (remove-untouchable my-var nil)
     (remove-untouchable set-mem t)

     General Form:
     (remove-untouchable name{s}  fn-p :doc doc-string)

where name{s} is a non-nil symbol or a non-nil true list of symbols,
fn-p is any value (but generally nil or t), and doc-string is an
optional documentation string not beginning with ":doc-section ...".
If name{s} is a symbol it is treated as the singleton list containing
that symbol.  The effect of this event is to remove the given symbols
from the list of "untouchable variables" in the current world if fn-p
is nil, else to remove the symbols into the list of "untouchable
functions".  This event is redundant if no symbol listed is a member of
the appropriate untouchables list (variables or functions).

RESET-PREHISTORY    reset the prehistory

     Examples:
     (reset-prehistory)     ; restart command numbering at 0
     (reset-prehistory nil) ; same as above
     (reset-prehistory t)   ; as above except also disable ubt-prehistory

     General Forms:
     (reset-prehistory)
     (reset-prehistory permanent-p)
     (reset-prehistory permanent-p doc-string)

where permanent-p is t or nil, and doc-string is an optional
documentation string not beginning with ":doc-section ...".  After
execution of this command, ACL2 will change the numbering provided by
its history utilities so that this reset-prehistory command (or the
top-level compound command containing it, which for example might be an
include-book) is assigned the number 0.  The only way to undo this
command is with command ubt-prehistory.  However, even that is
disallowed if permanent-p is t.

Note that the second argument of certify-book, which specifies the
number of commands in the certification world (i.e., since
ground-zero), is not sensitive to reset-prehistory; rather, it expects
the number of commands since ground-zero.  To see such commands, :pbt
:start.

A reset-prehistory event with value nil for permanent-p (the default)
is always skipped during certify-book and include-book (indeed,
whenever ld-skip-proofsp is t).  Otherwise one would find the history
numbering reset to 0 just by virtue of including (or certifying) a book
-- probably not what was intended.

See UBT-PREHISTORY for how to undo a reset-prehistory command
that does not have a permanent-p of t.

SET-BACKCHAIN-LIMIT    Sets the backchain-limit used by the rewriter

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the acl2-defaults-table, and hence its
effect is local to the book or encapsulate form containing it; see
ACL2-DEFAULTS-TABLE.

This event sets the global backchain-limit used by the ACL2 rewriter.
It must be nil or a non-negative integer.  (See BACKCHAIN-LIMIT
for details.)

     :set-backchain-limit nil  ; do not impose any additional limits
     :set-backchain-limit 0    ; allow only type reasoning for relieving
                               ; hypotheses
     :set-backchain-limit 500  ; allow backchaining to a depth of no more
                               ; than 500
     (set-backchain-limit 500) ; same as above

The default limit is nil.

SET-BOGUS-MUTUAL-RECURSION-OK    allow unnecessary ``mutual recursion''

     Examples:
     (set-bogus-mutual-recursion-ok t)
     (set-bogus-mutual-recursion-ok nil)
     (set-bogus-mutual-recursion-ok :warn)

By default, ACL2 checks that when a "clique" of more than one function
is defined simultaneously (using mutual-recursion or defuns), then
every body calls at least one of the functions in the "clique."  Below,
we refer to definitional events that fail this check as "bogus" mutual
recursions.  The check is important because ACL2 does not store
induction schemes for functions defined with other functions in a
mutual-recursion or defuns event.  Thus, ACL2 may have difficulty
proving theorems by induction that involve such functions.  Moreover,
the check can call attention to bugs, since users generally intend that
their mutual recursions are not bogus.

Nevertheless, there are times when it is advantageous to allow bogus
mutual recursions, for example when they are generated mechanically,
even at the expense of losing stored induction schemes.  The first
example above allows bogus mutual recursion.  The second example
disallows bogus mutual recursion; this is the default.  The third
example allows bogus mutual recursion, but prints an appropriate
warning.

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the acl2-defaults-table, and hence its
effect is local to the book or encapsulate form containing it; see
ACL2-DEFAULTS-TABLE.

     General Form:
     (set-bogus-mutual-recursion-ok flg)

where flg is either t, nil, or :warn.

SET-CASE-SPLIT-LIMITATIONS    set the case-split-limitations

     Examples:
     (set-case-split-limitations '(500 100))
     (set-case-split-limitations 'nil)
     (set-case-split-limitations '(500 nil))

The first of these prevents clausify from trying the
subsumption/replacement (see below) loop if more than 500 clauses are
involved.  It also discourages the clause simplifier from splitting
into more than 100 cases at once.

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the acl2-defaults-table, and hence its
effect is local to the book or encapsulate form containing it; see
ACL2-DEFAULTS-TABLE.

     General Form:
     (set-case-split-limitations lst)

where lst is either nil (denoting a list of two nils), or a list of
length two, each element of which is either nil or a natural number.
When nil is used as an element, it is treated as positive infinity.
The default setting is (500 100).

The first number specifies the maximum number of clauses that may
participate in the "subsumption/replacement" loop.  Because of the
expensive nature of that loop (which compares every clause to every
other in a way that is quadratic in the number of literals in the
clauses), when the number of clauses exceeds about 1000, the system
tends to "go into a black hole," printing nothing and not even doing
many garbage collections (because the subsumption/replacement loop does
not create new clauses so much as it just tries to delete old ones).
The initial setting is lower than the threshold at which we see
noticeably bad performance, so you probably will not see this behavior
unless you have raised or disabled the limit.

Why raise the subsumption/replacement limit?  The
subsumption/replacement loop cleans up the set of subgoals produced by
the simplifier.  For example, if one subgoal is

     (implies (and p q r) s)            [1]

and another is

     (implies (and p (not q) r) s)      [2]

then the subsumption/replacement loop would produce the single subgoal

     (implies (and p r) s)              [3]

instead.  This cleanup process is simply skipped when the number of
subgoals exceeds the subsumption/replacement limit.  But each subgoal
must nonetheless be proved.  The proofs of [1] and [2] are likely to
duplicate much work, which is only done once in proving [3].  So with a
low limit, you may find the system quickly produces a set of subgoals
but then takes a long time to prove that set.  With a higher limit, you
may find the set of subgoals to be "cleaner" and faster to prove.

Why lower the subsumption/replacement limit?  If you see the system go
into a "black hole" of the sort described above (no output, and few
garbage collections), it could due to the subsumption/replacement loop
working on a large set of large subgoals.  You might temporarily lower
the limit so that it begins to print the uncleaned set of subgoals.
Perhaps by looking at the output you will realize that some function
can be disabled so as to prevent the case explosion.  Then raise or
disable the limit again!

The second number in the case-split-limitations specifies how many case
splits the simplifier will allow before it begins to shut down case
splitting.  In normal operation, when a literal rewrites to a nest of
IFs, the system simplifies all subsequent literals in all the contexts
generated by walking through the nest in all possible ways.  This can
also cause the system to "go into a black hole" printing nothing except
garbage collection messages.  This "black hole" behavior is different
from than mentioned above because space is typically being consumed at
a prodigious rate, since the system is rewriting the literals over and
over in many different contexts.

As the simplifier sweeps across the clause, it keeps track of the
number of cases that have been generated.  When that number exceeds the
second number in case-split-limitations, the simplifier stops rewriting
literals.  The remaining, unrewritten, literals are copied over into
the output clauses.  IFs in those literals are split out, but the
literals themselves are not rewritten.  Each output clause is then
attacked again, by subsequent simplification, and eventually the
unrewritten literals in the tail of the clause will be rewritten
because the earlier literals will stabilize and stop producing case
splits.

The default setting of 100 is fairly low.  We have seen successful
proofs in which thousands of subgoals were created by a simplification.
By setting the second number to small values, you can force the system
to case split slowly.  For example, a setting of 5 will cause it to
generate "about 5" subgoals per simplification.

You can read about how the simplifier works in the book Computer-Aided
Reasoning: An Approach (Kaufmann, Manolios, Moore).  If you think about
it, you will see that with a low case limit, the initial literals of a
goal are repeatedly simplified, because each time a subgoal is
simplified we start at the left-most subterm.  So when case splitting
prevents the later subterms from being fully split out, we revisit the
earlier terms before getting to the later ones.  This can be good.
Perhaps it takes several rounds of rewriting before the earlier terms
are in normal form and then the later terms rewrite quickly.  But it
could happen that the earlier terms are expensive to rewrite and do not
change, making the strategy of delayed case splits less efficient.  It
is up to you.

Sometimes the simplifier produces more clauses than you might expect,
even with case-split-limitations in effect.  As noted above, once the
limit has been exceeded, the simplifier does not rewrite subsequent
literals.  But IFs in those literals are split out nonetheless.
Furthermore, the enforcement of the limit is - as described above - all
or nothing: if the limit allows us to rewrite a literal then we rewrite
the literal fully, without regard for limitations, and get as many
cases as "naturally" are produced.  It quite often happens that a
single literal, when expanded, may grossly exceed the specified limits.

If the second "number" is nil and the simplifier is going to produce
more than 1000 clauses, a "helpful little message" to this effect is
printed out.  This output is printed to the system's "comment window"
not the standard proofs output.

SET-COMPILE-FNS    have each function compiled as you go along.

     Example Forms:
     (set-compile-fns t)    ; new functions compiled after DEFUN
     (set-compile-fns nil)  ; new functions not compiled after DEFUN

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.

Also see COMP, because it may be more efficient in some Common
Lisps to compile many functions at once rather than to compile each one
as you go along.

     General Form:
     (set-compile-fns term)

where term is a variable-free term that evaluates to t or nil.  This
macro is equivalent to

     (table acl2-defaults-table :compile-fns term)

and hence is local to any books and encapsulate events in which it
occurs; see ACL2-DEFAULTS-TABLE.  However, unlike the above
simple call of the table event function (see TABLE), no output
results from a set-compile-fns event.

Set-compile-fns may be thought of as an event that merely sets a flag
to t or nil.  The flag's effect is felt when functions are defined, as
with defun.  If the flag is t, functions are automatically compiled
after they are defined, as are their executable counterparts (see
EXECUTABLE-COUNTERPART).  Otherwise, functions are not automatically
compiled.  Exception: The flag has no effect when explicit compilation
is suppressed; see COMPILATION.

Because set-compile-fns is an event, the old value of the flag is
restored when a set-compile-fns event is undone.

Even when :set-compile-fns t has been executed, functions are not
individually compiled when processing an include-book event.  If you
wish to include a book of compiled functions, we suggest that you first
certify it with the compilation flag set (see CERTIFY-BOOK) or
else compile the book by supplying the appropriate load-compiled-file
argument to include-book.  More generally, compilation via
set-compile-fns is suppressed when the state global variable
ld-skip-proofsp has value 'include-book.

SET-DEFAULT-BACKCHAIN-LIMIT    sets the default backchain-limit used when admitting a rule

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the acl2-defaults-table, and hence its
effect is local to the book or encapsulate form containing it; see
ACL2-DEFAULTS-TABLE.

This event sets the default backchain-limit used when a new rewrite or
linear rule is admitted.  It must be nil or a non-negative integer.
(See BACKCHAIN-LIMIT for details.)

     :set-default-backchain-limit nil  ; do not impose additional limits
     :set-default-backchain-limit 0    ; allow only type-reasoning for
                                       ; relieving hypotheses
     :set-default-backchain-limit 500  ; allow backchaining to a depth of
                                       ; no more than 500
     (set-default-backchain-limit 500) ; same as above

The initial default backchain-limit is nil.

SET-DEFAULT-HINTS    set the default hints

     Examples:
     (set-default-hints '((computed-hint-1 clause)
                          (computed-hint-2 clause
                                           stable-under-simplificationp)))
     (set-default-hints nil)

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.  It is
local to the book or encapsulate form in which it occurs (see
SET-DEFAULT-HINTS! for a corresponding non-local event).

     General Form:
     (set-default-hints lst)

where lst is a list.  Generally speaking, the elements of lst should be
suitable for use as computed-hints.

Whenever a defthm or thm command is executed, the default hints are
appended to the right of any explicitly provided :hints in the command.
The same applies to defuns as well (:hints, :guard-hints, and (for
ACL2(r)) :std-hints).  The hints are then translated and processed just
as though they had been explicitly included.

Technically, we do not put restrictions on lst, beyond that it is a
true list.  It would be legal to execute

     (set-default-hints '(("Goal" :use lemma23)))

with the effect that the given hint is added to subsequent hints
supplied explicitly.  An explicit "Goal" hint would, however, take
priority, as suggested by the mention above of "appended to the right."

Note that set-default-hints sets the default hints as specified.  To
add to or remove from the current default, see
ADD-DEFAULT-HINTS and see REMOVE-DEFAULT-HINTS.

Finally, note that the effects of set-default-hints, add-default-hints,
and remove-default-hints are local to the book in which they appear.
Thus, users who include a book with such forms will not have their
default hints affected by such forms.  In order to export the effect of
setting the default hints, use set-default-hints!, add-default-hints!,
or remove-default-hints!.

SET-DEFAULT-HINTS!    set the default hints non-locally

Please see SET-DEFAULT-HINTS, which is the same as
set-default-hints!  except that the latter is not local to the
encapsulate or the book in which it occurs.  Probably set-default-hints
is to be preferred unless you have a good reason for wanting to export
the effect of this event outside the enclosing encapsulate or book.

SET-ENFORCE-REDUNDANCY    require most events to be redundant

     General Forms:
     (set-enforce-redundancy nil)   ; do not require redundancy (default)
     (set-enforce-redundancy t)     ; most events (see below) must be redundant
     (set-enforce-redundancy :warn) ; warn for most non-redundant events

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.

     General Form:
     (set-enforce-redundancy flag)

where flag is nil, t, or :warn, as indicated above.  This macro is
essentially equivalent to

     (table acl2-defaults-table :enforce-redundancy flag)

and hence is local to any books and encapsulate events in which it
occurs; see ACL2-DEFAULTS-TABLE.  However, unlike the above
simple call of the table event function (see TABLE), no output
results from a set-enforce-redundancy event.

Set-enforce-redundancy may be thought of as an event that merely sets a
flag as indicated above, which determines whether most events, including
defun and defthm events, are allowed to be redundant; see
REDUNDANT-EVENTS.  The exceptions are deflabel, defpkg, encapsulate,
include-book, push-untouchable, remove-untouchable, set-body, and table
events.  Any other type of non-redundant event will cause an error if
flag is t and a warning if flag is nil, _except_ in the course of
carrying out an include-book form.

Note that because table events that set the acl2-defaults-table are
implicitly local, set-enforce-redundancy events are ignored when
including books.  However, the presence of the event
(set-enforce-redundancy t) in a book guarantees that its subsequent
definitions and theorems are redundant.  This can be a useful property
to maintain in library development, as we now describe.

An example of the use of this form can be found in the distributed books
under directory books/rtl/rel4/.  The intention in that directory has
been to put all the gory details in subdirectories support/ and
arithmetic/, so that the books in subdirectory lib/ contain only the
"exported" definitions and theorems.  This approach is useful for human
readability.  Moreover, suppose we want to prove new theorems in lib/.
Typically we wish to prove the new theorems using the existing books in
lib/; however, our methodology demands that the proofs go into books in
support/.  If every theorem in lib/ is redundant, then we can _develop_
the proofs in lib/ but then when we are done, _move_ each book with
such proofs into support/ as follows.  In any such book, we first
replace include-book forms referring to books in lib/ by include-book
forms referring to corresponding books in support/ and/or arithmetic/.
Then, we add suitable in-theory events to get us back into the original
lib/ proof environment.

The default behavior of the system is as though the :enforce-redundancy
value is nil.  The current behavior can be ascertained by evaluating the
following form.

     (cdr (assoc-eq :enforce-redundancy (table-alist 'acl2-defaults-table wrld)))

SET-IGNORE-OK    allow unused formals and locals without an ignore or ignorable declaration

     Examples:
     (set-ignore-ok t)
     (set-ignore-ok nil)
     (set-ignore-ok :warn)

The first example above allows unused formals and locals, i.e.,
variables that would normally have to be declared ignored or ignorable.
The second example disallows unused formals and locals; this is the
default.  The third example allows them, but prints an appropriate
warning.

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the acl2-defaults-table, and hence its
effect is local to the book or encapsulate form containing it; see
ACL2-DEFAULTS-TABLE.

     General Form:
     (set-ignore-ok flg)

where flg is either t, nil, or :warn.

One might find this event useful when one is generating function
definitions by an automated procedure, when that procedure does not
take care to make sure that all formals are actually used in the
definitions that it generates.

Note:  Defun will continue to report irrelevant formals even if
:set-ignore-ok has been set to t, unless you also use
set-irrelevant-formals-ok to instruct it otherwise.

SET-INHIBIT-WARNINGS    control warnings

     Examples:
     (set-inhibit-warnings "theory" "use")

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the acl2-defaults-table, and hence its
effect is local to the book or encapsulate form containing it; see
ACL2-DEFAULTS-TABLE.

     General Form:
     (set-inhibit-warnings string1 string2 ...)

where each string is considered without regard to case.  This macro is
equivalent to (table acl2-defaults-table :inhibit-warnings lst), where
lst is the list of strings supplied.  This macro is an event (see
TABLE), but no output results from a set-inhibit-warnings event.

The effect of this event is to suppress any warning whose label is a
member of this list (where again, case is ignored).  For example, the
warning

       ACL2 Warning [Use] in ( THM ...):  It is unusual to :USE ....

will not be printed if "use" (or "USE", etc.) is a member of the given
list of strings.

Of course, if warnings are inhibited overall -- see
SET-INHIBIT-OUTPUT-LST -- then the value of :inhibit-warnings is
entirely irrelevant.

SET-INVISIBLE-FNS-TABLE    set the invisible functions table

     Examples:
     (set-invisible-fns-table ((binary-+ unary--)
                               (binary-* unary-/)
                               (unary-- unary--)
                               (unary-/ unary-/)))
     (set-invisible-fns-table t) ; restore original invisible-fns-table

Among other things, the setting above has the effect of making unary-
"invisible" for the purposes of applying permutative :rewrite rules to
binary-+ trees.  Thus, arg and (unary- arg) will be given the same
weight and will be permuted so as to be adjacent.  The form
(invisible-fns-table (w state)) returns the current value of the
invisible functions table.

Also see ADD-INVISIBLE-FNS and see REMOVE-INVISIBLE-FNS
for events that add to and remove from the invisible functions table.

     General Form:
     (set-invisible-fns-table alist)

where alist is either t or a true list of pairs, each element of which
is of the form (fn ufn1 ... ufnk), where fn is a function symbol and
each ufni is a unary function symbol.  When alist is t, the initial
value of this table is used in its place.  Modulo the replacement of
alist by the default setting when alist is t, this macro is equivalent
to

     (table invisible-fns-table nil 'alist :clear)

which is also an event (see TABLE).

Note that set-invisible-fns-table does not evaluate its argument.
However, you can call table directly for that purpose.  For example,

     (set-invisible-fns-table ((binary-+ unary--)
                               (binary-* unary-/)
                               (unary-- unary--)
                               (unary-/ unary-/)))

ie equivalent to the following; see TABLE.

     (table invisible-fns-table nil
            (quote ((binary-+ unary--)
                    (binary-* unary-/)
                    (unary-- unary--)
                    (unary-/ unary-/)))
            :clear)

See INVISIBLE-FNS-TABLE for a description of the invisible
functions table.

SET-IRRELEVANT-FORMALS-OK    allow irrelevant formals in definitions

     Examples:
     (set-irrelevant-formals-ok t)
     (set-irrelevant-formals-ok nil)
     (set-irrelevant-formals-ok :warn)

The first example above allows irrelevant formals in definitions; see
IRRELEVANT-FORMALS.  The second example disallows irrelevant
formals; this is the default.  The third example allows irrelevant
formals, but prints an appropriate warning.

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the acl2-defaults-table, and hence its
effect is local to the book or encapsulate form containing it; see
ACL2-DEFAULTS-TABLE.

     General Form:
     (set-irrelevant-formals-ok flg)

where flg is either t, nil, or :warn.

SET-LET*-ABSTRACTIONP    to shorten many prettyprinted clauses

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the acl2-defaults-table, and hence its
effect is local to the book or encapsulate form containing it; see
ACL2-DEFAULTS-TABLE.

When this flag is set to t, subterms that occur more than once in a
clause are abstracted away with let*, generally shortening the
displayed size of the clauses.  This flag only affects how clauses are
printed.  It does not change what terms the theorem prover manipulates.

     :set-let*-abstractionp t ;;; or, (set-let*-abstractionp t)

will cause the prettyprinter to do "let* abstraction" on clauses before
they are printed.  The algorithm finds the maximal multiply-occuring
subterm and extracts it, binding it to some new variable and replacing
its occurrences by that variable.  This produces a let* form.  This
process is iterated until no subterm occurs more than once.  This
process generally takes a little time, but less time than to print
large clauses.  The process can greatly reduce the amount of text
produced by the prover.

THIS ONLY AFFECTS HOW THE CLAUSES ARE PRINTED!  The unabstracted
clauses are manipulated by the theorem prover.

     :set-let*-abstractionp nil

restores normal clause printing.

The mode is stored in the defaults table, See
ACL2-DEFAULTS-TABLE.  Thus, the mode may be set locally in books.