This is documentation for ACL2 Version 3.1
Copyright (C) 2006  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.

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.  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.

SET-MATCH-FREE-DEFAULT    provide default for :match-free in future rules

     General Forms:
     (set-match-free-default :once)
     (set-match-free-default :all)
     (set-match-free-default nil)

As described elsewhere (see FREE-VARIABLES), a rewrite, linear,
or forward-chaining rule may have free variables in its hypotheses, and
ACL2 can be directed either to try all bindings (":all") or just the
first (":once") when relieving that hypothesis, as a basis for
relieving subsequent hypotheses.  This direction of :all or :once is
generally provided by specifying either :match-free :once or
:match-free :all in the :rule-classes of the rule.  If neither of these
is specified, then the most recent set-match-free-default is used by
ACL2 to fill in this missing :match-free field.  See
RULE-CLASSES.  Except: If the last set-match-free-default specifies
nil, then ACL2 reverts to the behavior it had at start-up, as described
in Remarks (2) and (3) below.

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
uses the acl2-defaults-table, and hence its effect is local to the book
or encapsulate form in which it occurs.

Remarks.

(1) The use of set-match-free-default has no effect on existing rules.
In order to change the behavior of existing rules with respect to
free-variable matching, see ADD-MATCH-FREE-OVERRIDE.

(2) If you submit a rewrite, linear, or forward-chaining rule with a
free variable in a hypothesis, and no default setting was previously
specified with set-match-free-default or the default setting is nil,
and the rule is not within a book being processed with include-book,
certify-book, or rebuild, then a warning or error is caused.  In order
to make this an error instead of a warning, see
SET-MATCH-FREE-ERROR.

(3) If you submit a rewrite, linear, or forward-chaining rule with a
free variable in a hypothesis, and no default setting has been
previously specified with set-match-free-default or the default setting
is nil, and no error is caused (see (2) above), then the default :all
is used.

SET-MATCH-FREE-ERROR    control error vs. warning when :match-free is missing

     Legal Forms:
     (set-match-free-error nil)
     :set-match-free-error nil
     (set-match-free-error t)
     :set-match-free-error t

As described elsewhere (see FREE-VARIABLES), when a rewrite,
linear, or forward-chaining rule has free variables in its hypotheses,
the user can specify whether to try all bindings (":all") or just the
first (":once") when relieving its hypotheses, as a basis for relieving
subsequent hypotheses.  This direction of :all or :once is generally
provided by specifying either :match-free :once or :match-free :all in
the :rule-classes of the rule.

But suppose that neither of these is specified, and that
set-match-free-default has not specified a default of :once or :all
(see SET-MATCH-FREE-DEFAULT).  In this case a warning will occur
except when in the context of include-book.  If you prefer to see an
error in such cases, except in the context of certify-book, execute
(set-match-free-error t).  If there is no error, then a default of :all
is used.

Note: This is NOT an event!  Instead, set-match-free-error sets the
state global 'match-free-error (see STATE and see
ASSIGN).  Thus, this form cannot be put into a book.  If you are
tempted to put it into a book, consider the fact that it really isn't
needed there, since the absence of :match-free does not cause an error
in the context of certify-book or include-book.  If you still feel the
need for such a form, consider using set-match-free-default to provide
a default, at least within the scope of the current book (if any); see
SET-MATCH-FREE-DEFAULT.

SET-MEASURE-FUNCTION    set the default measure function symbol

     Examples:
     (set-measure-function nqthm::count)

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-measure-function name)

where name is a function symbol of one argument.  This macro is
equivalent to (table acl2-defaults-table :measure-function 'name), and
hence is local to any books and encapsulate events in which it occurs;
see ACL2-DEFAULTS-TABLE.  Although this is thus an event (see
TABLE), nevertheless no output results from a
set-measure-function event.

This event sets the default measure function to name.  Subsequently, if
a recursively defined function is submitted to defun with no explicitly
given :measure argument, defun "guesses" the measure (name var), where
name is the then current default measure function and var is the first
formal found to be tested along every branch and changed in every
recursive call.

Note that if (table acl2-defaults-table :measure-function 'name) has its
default value of nil, then the default measure function is acl2-count.

SET-NON-LINEARP    to turn on or off non-linear arithmetic reasoning

     Examples:
     (set-non-linearp t)
     (set-non-linearp nil)

See NON-LINEAR-ARITHMETIC.   This event is equivalent to (table
acl2-defaults-table :non-linearp <t-or-nil>), and hence is local to any
books and encapsulate events in which it occurs; see
ACL2-DEFAULTS-TABLE.

The initial value is nil.

SET-NU-REWRITER-MODE    to turn on and off the nu-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.

This event sets a flag that controls whether the ACL2 rewriter uses the
special-purpose nth/update-nth rewriter (nu-rewriter).  The flag may
have one of three values: nil, t, or :literals.

     :set-nu-rewriter-mode nil        ; do not use nu-rewriter
     :set-nu-rewriter-mode t          ; use nu-rewriter in rewriting
     :set-nu-rewriter-mode :literals  ; use nu-rewriter in rewriting after
                                      ;  a pre-pass through every literal
     (set-nu-rewriter-mode :literals) ; same as above

The value nil prevents the use of the nu-rewriter.  The other two
values allow the use of the nu-rewriter.

When the flag is non-nil and the rewriter encounters a term that
"begins with an nth", the nu-rewriter is applied.  By "begins with an
nth" here we mean either the term is an application of nth or is an
application of some nonrecursive function or lambda expression whose
body contains an expression that begins with an nth.

Note that the use of the nu-rewriter here described above is driven by
the rewriter, i.e., the nu-rewriter is applied only to terms visited by
the rewriter in its inside-out sweep.  When the flag is set to
:literals the system makes a pre-pass through every goal clause and
applies the nu-rewriter to every subterm.  The rewriter is then used on
the output of that pre-pass.

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.

We expect to write more documentation as we gain experience with the
nu-rewriter.

SET-REWRITE-STACK-LIMIT    Sets the rewrite stack depth 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.

     Example Forms:
     (set-rewrite-stack-limit 30)                            ; set to small limit
     :set-rewrite-stack-limit 30                             ; same as above
     (set-rewrite-stack-limit *default-rewrite-stack-limit*) ; the default
     :set-rewrite-stack-limit (1- (expt 2 28))               ; maximum legal limit
     :set-rewrite-stack-limit nil         ; same as above -- essentially, no limit

This event sets the maximum stack depth for calls of certain functions
that implement the ACL2 rewriter; see REWRITE-STACK-LIMIT.  It
must be a non-negative integer less than 2^28.  A call
(set-rewrite-stack-limit limit) is equivalent to:

     (table acl2-defaults-table :rewrite-stack-limit limit).

The use of acl2-defaults-table ensures that this event's effect is
implicitly local to the book or encapsulate form in which it occurs.

For a different but somewhat related concept, see
BACKCHAIN-LIMIT.

SET-STATE-OK    allow the use of STATE as a formal parameter

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

In brief:  The variable symbol STATE has an unusual status in ACL2.  In
order to use it, you either need to issue :set-state-ok t, as we
explain below, or you need to declare it to be a stobj, as explained
elsewhere (see DECLARE-STOBJS).  Now we explain in more detail.

Because the variable symbol STATE denotes the "current ACL2 state,"
ACL2 treats the symbol very restrictively when it occurs as a formal
parameter of a defined function.  The novice user, who is unlikely to
be aware of the special status of that symbol, is likely to be confused
when error messages about STATE are printed in response to the innocent
choice of that symbol as a formal variable.  Therefore the top-level
ACL2 loop can operate in a mode in which STATE is simply disallowed as
a formal parameter.

For a discussion of STATE, See STATE and see STOBJ.
Roughly speaking, at the top-level, the "current ACL2 state" is denoted
by the variable symbol STATE.  Only the current state may be passed
into a function expecting a state as an argument.  Furthermore, the
name of the formal parameter into which the current state is passed
must be STATE and nothing but the current state may be passed into a
formal of that name.  Therefore, only certain access and change
functions can use that formal - namely with a STATE formal - and if any
such function produces a new state it becomes the "current state" and
must be passed along in the STATE position thereafter.  Thus, ACL2
requires that the state be single-threaded.  This, in turn, allows us
to represent only one state at a time and to produce new states from it
destructively in a von Neumaneque fashion.  The syntactic restrictions
on the variable STATE are enforced by the translate mechanism (see
TRANS and see TERM) when terms are read.

To prevent the novice user from seeing messages prohibiting certain
uses of the variable symbol STATE ACL2 has a mode in which it simply
disallows the use of that symbol as a formal parameter.  Use of the
symbol causes a simple error message.  The system is initially in that
mode.

To get out of that mode, execute:

     :set-state-ok t ;;; or, (set-state-ok t)

It is not recommended that you do this until you have read the
documentation of STATE.

To enter the mode in which use of state is prohibited as a formal
parameter, do:

     :set-state-ok nil

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

SET-VERIFY-GUARDS-EAGERNESS    the eagerness with which guard verification is tried.

     Example Forms:                        try guard verification?
     (set-verify-guards-eagerness 0) ; no, unless :verify-guards t
     (set-verify-guards-eagerness 1) ; yes if a :guard is supplied
     (set-verify-guards-eagerness 2) ; yes, unless :verify-guards 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.

     General Form:
     (set-verify-guards-eagerness n)

where n is a variable-free term that evaluates to 0, 1, or 2.  This
macro is essentially equivalent to

     (table acl2-defaults-table :verify-guards-eagerness n)

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-verify-guards-eagerness event.

Set-verify-guards-eagerness may be thought of as an event that merely
sets a flag to 0, 1, or 2.  The flag is used by certain defun events to
determine whether guard verification is tried.  The flag is irrelevant
to those defun events in :program mode and to those defun events in
which an explicit :verify-guards setting is provided among the xargs.
In the former case, guard verification is not done because it can only
be done when logical functions are being defined.  In the latter case,
the explicit :verify-guards setting determines whether guard
verification is tried.  So consider a :logic mode defun in which no
:verify-guards setting is provided.  Is guard verification tried?  The
answer depends on the eagerness setting as follows.  If the eagerness
is 0, guard verification is not tried.  If the eagerness is 1, it is
tried iff a :guard is explicitly provided in the defun.  If the
eagerness is 2, guard verification is tried.

The default behavior of the system is as though the
:verify-guards-eagerness is 1.  The current behavior can be ascertained
by evaluating the form (default-verify-guards-eagerness (w state)).

SET-WELL-FOUNDED-RELATION    set the default well-founded relation

     Examples:
     (set-well-founded-relation lex2)

provided lex2 has been proved to be a well-founded relation (see
WELL-FOUNDED-RELATION).  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-well-founded-relation rel)

where rel has been proved to be a well-founded relation on objects
satisfying some predicate, mp; see WELL-FOUNDED-RELATION.  This
macro is equivalent to (table acl2-defaults-table
:well-founded-relation 'rel), and hence is local to any books and
encapsulate events in which it occurs; see ACL2-DEFAULTS-TABLE.

This event sets the default well-founded relation to be that imposed on
mp-measures by the relation rel.  Subsequently, if a recursively
defined function is submitted to defun with no explicitly given
:well-founded-relation argument, defun uses the default relation, rel,
and the associated domain predicate mp used in its well-foundedness
theorem.  That is, the termination conditions generated will require
proving that the measure used by the defun is an mp-measure and that in
every recursive call the measure of the arguments decreases according
to rel.

TABLE    user-managed tables

     Examples:
     (table tests 1 '(...))                ; set contents of tests[1] to '(...)
     (table tests 25)                      ; get contents of tests[25]
     (table tests)                         ; return table tests as an alist
     (table tests nil nil :clear)          ; clear table tests
     (table tests nil '((foo . 7)) :clear) ; set table tests to (foo 7)
     (table tests nil nil :guard)          ; fetch the table guard
     (table tests nil nil :guard term)     ; set the table guard

     General Form:
     (table table-name key-term value-term op term)

where table-name is a symbol that is the name of a (possibly new)
table, key-term and value-term, if present, are arbitrary terms
involving (at most) the single variable world, op, if present, is one
of the table operations below, and term, if present, is a term.  Table
returns an acl2 "error triple." The effect of table on state depends on
op and how many arguments are presented.  Some invocations actually
have no effect on the ACL2 world and hence an invocation of table is
not always an "event".  We explain below, after giving some background
information.

Important Note:  The table forms above are calls of a macro that expand
to involve the special variable state.  This will prevent you from
accessing a table from within a hint or theory where where you do not
have the state variable.  However, the form

     (table-alist 'tests world)

returns the alist representation of the table named test in the given
world.  Often you have access to world.

The ACL2 system provides "tables" by which the user can associate one
object with another.  Tables are in essence just conventional
association lists -- lists of pairs -- but the ACL2 environment
provides a means of storing these lists in the "ACL2 world" of the
current state.  The ACL2 user could accomplish the same ends by using
ACL2 "global variables;" however, limitations on global variable names
are imposed to ensure ACL2's soundness.  By convention, no table is
important to ACL2's soundness, even though some features of the system
use tables, and the user is invited to make free use of tables.
Because tables are stored in the ACL2 world they are restored by
include-book and undone by :ubt.  Many users of Nqthm requested a
facility by which user data could be saved in Nqthm "lib files" and
tables are ACL2's answer to that request.

Abstractly, each table is an association list mapping "keys" to
"values." In addition, each table has a ":guard," which is a term that
must be true of any key and value used.  By setting the :guard on a
table you may enforce an invariant on the objects in the table, e.g.,
that all keys are positive integers and all values are symbols.  Each
table has a "name," which must be a symbol.  Given a table name, there
are six operations one might perform on the table.

:put -- associate a value with a key (possibly changing the value
currently associated with that key).

:get -- retrieve the value associated with a key (or nil if no value
has been associated with that key).

:alist -- return an alist showing all keys and non-nil values in the
table.

:clear -- clear the table (so that every value is nil), or if val is
supplied then set table to that value (which must be an alist).

:guard -- fetch or set the :guard of the table.

When the operations above suggest that the table or its :guard are
modified, what is actually meant is that the current state is redefined
so that in it, the affected table name has the appropriate properties.
in such cases, the table form is an event (see EVENTS).  In the
:put case, if the key is already in the table and associated with the
proposed value, then the table event is redundant (see
REDUNDANT-EVENTS).

Table forms are commonly typed by the user while interacting with the
system.  :Put and :get forms are especially common.  Therefore, we have
adopted a positional syntax that is intended to be convenient for most
applications.  Essentially, some operations admit a "short form" of
invocation.

     (table name key-term value-term :put)   ; long form
     (table name key-term value-term)        ; short form

evaluates the key- and value-terms, obtaining two objects that we call
key and value, checks that the key and value satisfy the :guard on the
named table and then "modifies" the named table so that the value
associated with key is value.  When used like this, table is actually
an event in the sense that it changes the ACL2 world.  In general, the
forms evaluated to obtain the key and value may involve the variable
world, which is bound to the then-current world during the evaluation
of the forms.  However, in the special case that the table in question
is named acl2-defaults-table, the key and value terms may not contain
any variables.  Essentially, the keys and values used in events setting
the acl2-defaults-table must be explicitly given constants.  See
ACL2-DEFAULTS-TABLE.

     (table name key-term nil :get)          ; long form
     (table name key-term)                   ; short form

evaluates the key-term (see note below), obtaining an object, key, and
returns the value associated with key in the named table (or, nil if
there is no value associated with key).  When used like this, table is
not an event; the value is simply returned.

     (table name nil nil :alist)             ; long form
     (table name)                            ; short form

returns an alist representing the named table; for every key in the
table with a non-nil associated value, the alist pairs the key and its
value.  The order in which the keys are presented is unspecified.  When
used like this, table is not an event; the alist is simply returned.

     (table name nil val :clear)

sets the named table to the alist val, making the checks that :put
makes for each key and value of val.  When used like this, table is an
event because it changes the ACL2 world.

     (table name nil nil :guard)

returns the translated form of the guard of the named table.

     (table name nil nil :guard term)

Provided the named table is empty and has not yet been assigned a
:guard and term (which is not evaluated) is a term that mentions at
most the variables key, val and world, this event sets the :guard of
the named table to term.  Whenever a subsequent :put occurs, term will
be evaluated with key bound to the key argument of the :put, val bound
to the val argument of the :put, and world bound to the then current
world.  An error will be caused by the :put if the result of the
evaluation is nil.

Note that it is not allowed to change the :guard on a table once it has
been explicitly set.  Before the :guard is explicitly set, it is
effectively just t.  After it is set it can be changed only by undoing
the event that set it.  The purpose of this restriction is to prevent
the user from changing the :guards on tables provided by other people
or the system.

The intuition behind the :guard mechanism on tables is to enforce
invariants on the keys and values in a table, so that the values, say,
can be used without run-time checking.  But if the :guard of a table is
sensitive to the ACL2 world, it may be possible to cause some value in
the table to cease satisfying the :guard without doing any operations
on the table.  Consider for example the :guard "no value in this table
is the name of an event." As described, that is enforced each time a
value is stored.  Thus, 'bang can be :put in the table provided there
is no event named bang.  But once it is in the table, there is nothing
to prevent the user from defining bang as a function, causing the table
to contain a value that could not be :put there anymore.  Observe that
not all state-sensitive :guards suffer this problem.  The :guard "every
value is an event name" remains invariant, courtesy of the fact that
undoing back through an event name in the table would necessarily undo
the :put of the name into the table.

Table was designed primarily for convenient top-level use.  Tables are
not especially efficient.  Each table is represented by an alist stored
on the property list of the table name.  :Get is just a getprop and
assoc-equal.  :Put does a getprop to the get the table alist, a
put-assoc-equal to record the new association, and a putprop to store
the new table alist -- plus the overhead associated with :guards and
undoable events, and checking (for redundancy) if the key is already
bound to its proposed value.  Note that there are never duplicate keys
in the resulting alist; in particular, when the operation :clear is
used to install new alist, duplicate keys are removed from that alist.

A table name may be any symbol whatsoever.  Symbols already in use as
function or theorem names, for example, may be used as table names.
Symbols in use only as table names may be defined with defun, etc.
Because there are no restrictions on the user's choice of table names,
table names are not included among the logical names.  Thus, :pe name
will never display a table event (for a logical name other than :here).
Either :pe name will display a "normal" event such as (defun name ...)
or (defthm name ...) or else :pe name will cause an error indicating
that name is not a logical name.  This happens even if name is in use
as a table name.  Similarly, we do not permit table names to have
documentation strings, since the same name might already have a
documentation string.  If you want to associate a documentation string
with a table name that is being used no other way, define the name as a
label and use the :doc feature of deflabel (see DEFLABEL); also
see DEFDOC.

TERM-TABLE    a table used to validate meta rules

     Example:
     (table term-table t '((binary-+ x y) '3 'nil (car x)))

See TABLE for a general discussion of tables and the table
event used to manipulate tables.

The "term-table" is used at the time a meta rule is checked for
syntactic correctness.  Each proposed metafunction is run on each term
in this table, and the result in each case is checked to make sure that
it is a termp in the current world.  In each case where this test
fails, a warning is printed.

Whenever a metafunction is run in support of the application of a meta
rule, the result must be a term in the current world.  When the result
is not a term, a hard error arises.  The term-table is simply a means
for providing feedback to the user at the time a meta rule is
submitted, warning of the definite possibility that such a hard error
will occur at some point in the future.

The key used in term-table is arbitrary.  The top-most value is always
the one that is used; it is the entire list of terms to be considered.
Each must be a termp in the current ACL2 world.