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

STATE    the von Neumannesque ACL2 state object

The ACL2 state object is used extensively in programming the ACL2
system, and has been used in other ACL2 programs as well.  However,
most users, especially those interested in specification and
verification (as opposed to programming per se), need not be aware of
the role of the state object in ACL2, and will not write functions that
use it explicitly.  We say more about this point at the end of this
documentation topic.

The ACL2 state object is an example of a single-threaded object or
stobj.  ACL2 allows the user to define new single-threaded objects.
Generally, ACL2 may need to access the ACL2 state but should not
(cannot) change it except via a certain set of approved functions such
as defun and defthm.  If you need a state-like object to which you have
complete rights, you may want a stobj.

Key to the idea of our state is the notion of single-threadedness.  For
an explanation, see STOBJ.  The upshot of it is that state is a
variable symbol with severe restrictions on its use, so that it can be
passed into only certain functions in certain slots, and must be
returned by those functions that "modify" it.  Henceforth, we do not
discuss single-threaded objects in general (which the user can introduce
with defstobj) but one in particular, namely ACL2's state object.

The global table is perhaps the most visible portion of the state
object.  Using the interface functions @ and assign, a user may bind
global variables to the results of function evaluations (much as an
Nqthm user exploits the Nqthm utility r-loop).  See @,
and see ASSIGN.

ACL2 supports several facilities of a truly von Neumannesque state
machine character, including file io and global variables.  Logically
speaking, the state is a true list of the 14 components described
below.  There is a "current" state object at the top-level of the ACL2
command loop.  This object is understood to be the value of what would
otherwise be the free variable state appearing in top-level input.
When any command returns a state object as one of its values, that
object becomes the new current state.  But ACL2 provides von Neumann
style speed for state operations by maintaining only one physical (as
opposed to logical) state object.  Operations on the state are in fact
destructive.  This implementation does not violate the applicative
semantics because we enforce certain draconian syntactic rules
regarding the use of state objects.  For example, one cannot "hold on"
to an old state, access the components of a state arbitrarily, or
"modify" a state object without passing it on to subsequent
state-sensitive functions.

Every routine that uses the state facilities (e.g. does io, or calls a
routine that does io), must be passed a "state object." And a routine
must return a state object if the routine modifies the state in any
way.  Rigid syntactic rules governing the use of state objects are
enforced by the function translate, through which all ACL2 user input
first passes.  State objects can only be "held" in the formal parameter
state, never in any other formal parameter and never in any structure
(excepting a multiple-value return list field which is always a state
object).  State objects can only be accessed with the primitives we
specifically permit.  Thus, for example, one cannot ask, in code to be
executed, for the length of state or the car of state.  In the
statement and proof of theorems, there are no syntactic rules
prohibiting arbitrary treatment of state objects.

Logically speaking, a state object is a true list whose members are as
follows:

     Open-input-channels, an alist with keys that are symbols in
     package "ACL2-INPUT-CHANNEL".  The value (cdr) of each pair has
     the form ((:header type file-name open-time) . elements), where
     type is one of :character, :byte, or :object and elements is a
     list of things of the corresponding type, i.e. characters,
     integers of type (mod 255), or lisp objects in our theory.
     File-name is a string.  Open-time is an integer.  See IO.

     Open-output-channels, an alist with keys that are symbols in
     package "ACL2-OUTPUT-CHANNEL".  The value of a pair has the form
     ((:header type file-name open-time) .  current-contents).  See
     IO.

     Global-table, an alist associating symbols (to be used as "global
     variables") with values.  See @, and see
     ASSIGN.

     T-stack, a list of arbitrary objects accessed and changed by the
     functions aref-t-stack and aset-t-stack.

     32-bit-integer-stack, a list of arbitrary 32-bit-integers accessed
     and changed by the functions aref-32-bit-integer-stack and
     aset-32-bit-integer-stack.

     Big-clock-entry, an integer, that is used logically to bound the
     amount of effort spent to evaluate a quoted form.

     Idates, a list of dates and times, used to implement the function
     print-current-idate, which prints the date and time.

     Acl2-oracle, a list of objects, used for example to implement the
     functions that let ACL2 report how much time was used, but
     inaccessible to the user.  Also see WITH-PROVER-TIME-LIMIT.

     File-clock, an integer that is increased on every file opening and
     closing, and on each call of sys-call, and is used to maintain the
     consistency of the io primitives.

     Readable-files, an alist whose keys have the form (string type
     time), where string is a file name and time is an integer.  The
     value associated with such a key is a list of characters, bytes,
     or objects, according to type.  The time field is used in the
     following way:  when it comes time to open a file for input, we
     will only look for a file of the specified name and type whose
     time field is that of file-clock.  This permits us to have a
     "probe-file" aspect to open-file: one can ask for a file, find it
     does not exist, but come back later and find that it does now
     exist.

     Written-files, an alist whose keys have the form (string type
     time1 time2), where string is a file name, type is one of
     :character, :byte or :object, and time1 and time2 are integers.
     Time1 and time2 correspond to the file-clock time at which the
     channel for the file was opened and closed.  This field is
     write-only; the only operation that affects this field is
     close-output-channel, which conses a new entry on the front.

     Read-files, a list of the form (string type time1 time2), where
     string is a file name and time1 and time2 were the times at which
     the file was opened for reading and closed.  This field is write
     only.

     Writeable-files, an alist whose keys have the form (string type
     time).  To open a file for output, we require that the name, type,
     and time be on this list.

     List-all-package-names-lst, a list of true-listps.  Roughly
     speaking, the car of this list is the list of all package names
     known to this Common Lisp right now and the cdr of this list is
     the value of this state variable after you look at its car.  The
     function, list-all-package-names, which takes the state as an
     argument, returns the car and cdrs the list (returning a new state
     too).  This essentially gives ACL2 access to what is provided by
     CLTL's list-all-packages.  Defpkg uses this feature to ensure that
     the about-to-be-created package is new in this lisp.  Thus, for
     example, in akcl it is impossible to create the package "COMPILER"
     with defpkg because it is on the list, while in Lucid that package
     name is not initially on the list.

     User-stobj-alist, an alist which associates user-defined
     single-threaded objects (see STOBJ) with their values.

We recommend avoiding the use of the state object when writing ACL2
code intended to be used as a formal model of some system, for several
reasons.  First, the state object is complicated and contains many
components that are oriented toward implementation and are likely to be
irrelevant to the model in question.  Second, there is currently not
much support for reasoning about ACL2 functions that manipulate the
state object, beyond their logical definitions.  Third, the
documentation about state is not as complete as one might wish.

User-defined single-threaded objects offer the speed of state while
giving the user complete access to all the fields.  See STOBJ.

STOBJS    xargs keyword :STOBJS

See XARGS.

SUBVERSIVE-INDUCTIONS    why we restrict encapsulated recursive functions

See SUBVERSIVE-RECURSIONS.

SUBVERSIVE-RECURSIONS    why we restrict encapsulated recursive functions

Subtleties arise when one of the "constrained" functions, f, introduced
in the signature of an encapsulate event, is involved in the
termination argument for a non-local recursively defined function, g, in
that encapsulate.  During the processing of the encapsulated events, f
is locally defined to be some witness function, f'.  Properties of f'
are explicitly proved and exported from the encapsulate as the
constraints on the undefined function f.  But if f is used in a
recursive g defined within the encapsulate, then the termination proof
for g may use properties of f' -- the witness -- that are not
explicitly set forth in the constraints stated for f.

Such recursive g are said be "subversive" because if naively treated
they give rise to unsound induction schemes or (via functional
instantiation) recurrence equations that are impossible to satisfy.  We
illustrate what could go wrong below.

Subversive recursions are not banned outright.  Instead, they are
treated as part of the constraint.  That is, in the case above, the
definitional equation for g becomes one of the constraints on f.  This
is generally a severe restriction on future functional instantiations
of f.  In addition, ACL2 removes from its knowledge of g any
suggestions about legal inductions to "unwind" its recursion.

What should you do?  Often, the simplest response is to move the
offending recursive definition, e.g., g, out of the encapsulate.  That
is, introduce f by constraint and then define g as an "independent"
event.  You may need to constrain "additional" properties of f in order
to admit g, e.g., constrain it to reduce some ordinal measure.  However,
by separating the introduction of f from the admission of g you will
clearly identify the necessary constraints on f, functional
instantiations of f will be simpler, and g will be a useful function
which suggests inductions to the theorem prover.

Note that the functions introduced in the signature should not even
occur ancestrally in the termination proofs for non-local recursive
functions in the encapsulate.  That is, the constrained functions of an
encapsulate should not be reachable in the dependency graph of the
functions used in the termination arguments of recursive functions in
encapsulate.  If they are reachable, their definitions become part of
the constraints.

The following event illustrates the problem posed by subversive
recursions.

     (encapsulate (((f *) => *))
       (local (defun f (x) (cdr x)))
       (defun g (x)
         (if (consp x) (not (g (f x))) t)))

Suppose, contrary to how ACL2 works, that the encapsulate above were to
introduce no constraints on f on the bogus grounds that the only use of
f in the encapsulate is in an admissible function.  We discuss the
plausibility of this bogus argument in a moment.

Then it would be possible to prove the theorem:

     (defthm f-not-identity
       (not (equal (f '(a . b)) '(a . b)))
       :rule-classes nil
       :hints (("Goal" :use (:instance g (x '(a . b))))))

simply by observing that if (f '(a . b)) were '(a . b), then (g '(a .
b)) would be (not (g '(a . b))), which is impossible.

But then we could functionally instantiate f-not-identity, replacing f
by the identity function, to prove nil!  This is bad.

     (defthm bad
       nil
       :rule-classes nil
       :hints
       (("Goal" :use (:functional-instance f-not-identity (f identity)))))

This sequence of events was legal in versions of ACL2 prior to Version
1.5.  When we realized the problem we took steps to make it illegal.
However, our steps were insufficient and it was possible to sneak in a
subversive function (via mutual recursion) as late as Version 2.3.

We now turn to the plausibility of the bogus argument above.  Why might
one even be tempted to think that the definition of g above poses no
constraint on f?  Here is a very similar encapsulate.

     (encapsulate (((f *) => *))
       (local (defun f (x) (cdr x)))
       (defun map (x)
         (if (consp x)
             (cons (f x) (map (cdr x)))
           nil)))

Here map plays the role of g above.  Like g, map calls the constrained
function f.  But map truly does not constrain f.  In particular, the
definition of map could be moved "out" of the encapsulate so that map
is introduced afterwards.  The difference between map and g is that the
constrained function plays no role in the termination argument for the
one but does for the other.

As a "user-friendly" gesture, ACL2 implicitly moves map-like functions
out of encapsulations; logically speaking, they are introduced after the
encapsulation.  This simplifies the constraint.  This is done only for
"top-level" encapsulations.  When an encapsulate containing a non-empty
signature list is embedded in another encapsulate with a non-empty
signature list, no attempt is made to move map-like functions out.  The
user is advised, via the "infected" warning, to phrase the
encapsulation in the simplest way possible.

The lingering bug between Versions 1.5 and 2.3 mentioned above was due
to our failure to detect the g-like nature of some functions when they
were defined in mutually recursively cliques with other functions.  The
singly recursive case was recognized.  The bug arose because our
detection "algorithm" was based on the "suggested inductions" left
behind by successful definitions.  We failed to recall that
mutually-recursive definitions do not, as of this writing, make any
suggestions about inductions and so did not leave any traces of their
subversive natures.

We conclude by elaborating on the criterion "involved in the termination
argument" mentioned at the outset.  Suppose that function f is
recursively defined in an encapsulate, where the body of f has no
"ancestor" among the functions introduced in the signature of that
encapsulate, i.e.: the body contains no call of a signature function,
no call of a function whose body calls a signature function, and so on.
Then ACL2 treats f as though it is defined in front of that encapsulate
form; so f is not constrained by the encapsulate, and its definition is
hence certainly not subversive in the sense discussed above.  But
suppose to the contrary that some function introduced in the signature
is an ancestor of the body of f.  Then the definition of f is
subversive if moreover, its termination proof obligation has an
ancestor among the signature functions.  Now, that proof obligation
involves terms from the first argument of selected calls of IF, as well
as recursive calls; for a detailed discussion, see
RULER-EXTENDERS.  The important point here is that for the recursive
calls, only the arguments in "measured" positions are relevant to the
termination proof obligation.  Consider the following example.

       (encapsulate
        (((h *) => *))
        (local (defun h (n) n))
        (defun f (i n)
          (if (zp i)
              n
            (f (1- i) (h n)))))

ACL2 heuristically picks the measure (acl2-count i) for the definition
of f; thus, i is the only "measured formal" of f.  Since i is the first
formal of f, then for the recursive call of f, only the first argument
contributes to the termination proof obligation: in this case, (1- i)
but not (h n).  Thus, even though h is a signature function, the
definition of f is not considered to be subversive; an induction scheme
is thus stored for f.  (This restriction to measured formal positions
of recursive calls, for determining subversive definitions, is new in
Version_3.5 of ACL2.)

SYNTAX    the syntax of ACL2 is that of Common Lisp

For the details of ACL2 syntax, see CLTL.  For examples of ACL2 syntax,
use :pe to print some of the ACL2 system code.  For example:

     :pe assoc-equal
     :pe dumb-occur
     :pe var-fn-count
     :pe add-linear-variable-to-alist

There is no comprehensive description of the ACL2 syntax yet, except
that found in CLTL.  Also see TERM.

SYNTAXP    attach a heuristic filter on a :rewrite, :meta, or :linear rule

     Example:
     Consider the :REWRITE rule created from

     (IMPLIES (SYNTAXP (NOT (AND (CONSP X)
                                 (EQ (CAR X) 'NORM))))
              (EQUAL (LXD X)
                     (LXD (NORM X)))).

The syntaxp hypothesis in this rule will allow the rule to be applied
to (lxd (trn a b)) but will not allow it to be applied to (lxd (norm
a)).

     General Form:
     (SYNTAXP test)

Syntaxp always returns t and so may be added as a vacuous hypothesis.
However, when relieving the hypothesis, the test "inside" the syntaxp
form is actually treated as a meta-level proposition about the proposed
instantiation of the rule's variables and that proposition must
evaluate to true (non-nil) to "establish" the syntaxp hypothesis.

Note that the test of a syntaxp hypothesis does not, in general, deal
with the meaning or semantics or values of the terms, but rather with
their syntactic forms.  In the example above, the syntaxp hypothesis
allows the rule to be applied to every target of the form (lxd u),
provided u is not of the form (norm v).  Observe that without this
syntactic restriction the rule above could loop producing a sequence of
increasingly complex targets (lxd a), (lxd (norm a)), (lxd (norm (norm
a))), etc.  An intuitive reading of the rule might be "norm the
argument of lxd unless it has already been normed."

Note also that a syntaxp hypothesis deals with the syntactic form used
internally by ACL2, rather than that seen by the user.  In some cases
these are the same, but there can be subtle differences with which the
writer of a syntaxp hypothesis must be aware.  You can use :trans to
display this internal representation.

There are two types of syntaxp hypotheses.  The simpler type of syntaxp
hypothesis may be used as the nth hypothesis in a :rewrite or :linear
rule whose :corollary is (implies (and hyp1 ... hypn ... hypk) (equiv
lhs rhs)) provided test is a term, test contains at least one variable,
and every variable occuring freely in test occurs freely in lhs or in
some hypi, i<n.  In addition, test must not use any stobjs.  The case
of :meta rules is similar to the above, except that it applies to the
result of applying the hypothesis metafunction.  (Later below we will
describe the second type, an _extended_ syntaxp hypothesis, which may
use state.)

We illustrate the use of simple syntaxp hypotheses by slightly
elaborating the example given above.  Consider a :rewrite rule whose
:corollary is:

     (IMPLIES (AND (RATIONALP X)
                   (SYNTAXP (NOT (AND (CONSP X)
                                      (EQ (CAR X) 'NORM)))))
              (EQUAL (LXD X)
                     (LXD (NORM X))))

How is this rule applied to (lxd (trn a b))?  First, we form a
substitution that instantiates the left-hand side of the conclusion of
the rule so that it is identical to the target term.  In the present
case, the substitution replaces x with (trn a b).

     (LXD X) ==> (LXD (trn a b)).

Then we backchain to establish the hypotheses, in order.  Ordinarily
this means that we instantiate each hypothesis with our substitution and
then attempt to rewrite the resulting instance to true.  Thus, in order
to relieve the first hypothesis above, we rewrite

     (RATIONALP (trn a b)).

If this rewrites to true, we continue.

Of course, most users are aware of some exceptions to this general
description of the way we relieve hypotheses.  For example, if a
hypothesis contains a "free-variable" -- one not bound by the current
substitution -- we attempt to extend the substitution by searching for
an instance of the hypothesis among known truths.  See
FREE-VARIABLES.  Forced hypotheses are another exception to the
general rule of how hypotheses are relieved.

Hypotheses marked with syntaxp, as in (syntaxp test), are also
exceptions.  We instantiate such a hypothesis; but instead of rewriting
the instantiated instance, we evaluate the instantiated test.  More
precisely, we evaluate test in an environment in which its variable
symbols are bound to the quotations of the terms to which those
variables are bound in the instantiating substitution.  So in the case
in point, we (in essence) evaluate

     (NOT (AND (CONSP '(trn a b)) (EQ (CAR '(trn a b)) 'NORM))).

This clearly evaluates to t.  When a syntaxp test evaluates to true, we
consider the syntaxp hypothesis to have been established; this is sound
because logically (syntaxp test) is t regardless of test.  If the test
evaluates to nil (or fails to evaluate because of guard violations) we
act as though we cannot establish the hypothesis and abandon the
attempt to apply the rule; it is always sound to give up.

The acute reader will have noticed something odd about the form

     (NOT (AND (CONSP '(trn a b)) (EQ (CAR '(trn a b)) 'NORM))).

When relieving the first hypothesis, (RATIONALP X), we substituted (trn
a b) for X; but when relieving the second hypothesis, (SYNTAXP (NOT
(AND (CONSP X) (EQ (CAR X) 'NORM)))), we substituted the quotation of
(trn a b) for X.  Why the difference?  Remember that in the first
hypothesis we are talking about the value of (trn a b) -- is it
rational -- while in the second one we are talking about its syntactic
form.  Remember also that Lisp, and hence ACL2, evaluates the arguments
to a function before applying the function to the resulting values.
Thus, we are asking "Is the list (trn a b) a consp and if so, is its
car the symbol NORM?"  The quotes on both (trn a b) and NORM are
therefore necessary.  One can verify this by defining trn to be, say
cons, and then evaluating forms such as

     (AND (CONSP '(trn a b)) (EQ (CAR '(trn a b)) 'NORM))
     (AND (CONSP (trn a b)) (EQ (CAR (trn a b)) NORM))
     (AND (CONSP (trn 'a 'b)) (EQ (CAR (trn 'a 'b)) NORM))
     (AND (CONSP '(trn a b)) (EQ '(CAR (trn a b)) ''NORM))

at the top-level ACL2 prompt.

See SYNTAXP-EXAMPLES for more examples of the use of syntaxp.

An extended syntaxp hypothesis is similar to the simple type described
above, but it uses two additional variables, mfc and state, which must
not be bound by the left hand side or an earlier hypothesis of the
rule.  They must be the last two variables mentioned by form; first
mfc, then state.  These two variables give access to the functions
mfc-xxx; see EXTENDED-METAFUNCTIONS.  As described there, mfc
is bound to the so-called metafunction-context and state to ACL2's
state.  See SYNTAXP-EXAMPLES for an example of the use of these
extended syntaxp hypotheses.

SYNTAXP-EXAMPLES    examples pertaining to syntaxp hypotheses

See SYNTAXP for a basic discussion of the use of syntaxp to
control rewriting.

A common syntactic restriction is

     (SYNTAXP (AND (CONSP X) (EQ (CAR X) 'QUOTE)))

or, equivalently,

     (SYNTAXP (QUOTEP X)).

A rule with such a hypothesis can be applied only if x is bound to a
specific constant.  Thus, if x is 23 (which is actually represented
internally as (quote 23)), the test evaluates to t; but if x prints as
(+ 11 12) then the test evaluates to nil (because (car x) is the symbol
binary-+).  We see the use of this restriction in the rule

     (implies (and (syntaxp (quotep c))
                   (syntaxp (quotep d)))
              (equal (+ c d x)
                     (+ (+ c d) x))).

If c and d are constants, then the executable-counterpart of binary-+
will evaluate the sum of c and d.  For instance, under the influence of
this rule

     (+ 11 12 foo)

rewrites to

     (+ (+ 11 12) foo)

which in turn rewrites to (+ 23 foo).  Without the syntactic
restriction, this rule would loop with the built-in rules
ASSOCIATIVITY-OF-+ or COMMUTATIVITY-OF-+.

We here recommend that the reader try the affects of entering
expressions such as the following at the top level ACL2 prompt.

     (+ 11 23)
     (+ '11 23)
     (+ '11 '23)
     (+ ''11 ''23)
     :trans (+ 11 23)
     :trans (+ '11 23)
     :trans (+ ''11 23)
     :trans (+ c d x)
     :trans (+ (+ c d) x)

We also recommend that the reader verify our claim above about looping
by trying the affect of each of the following rules individually.

     (defthm good
        (implies (and (syntaxp (quotep c))
                      (syntaxp (quotep d)))
                 (equal (+ c d x)
                        (+ (+ c d) x))))

     (defthm bad
        (implies (and (acl2-numberp c)
                      (acl2-numberp d))
                 (equal (+ c d x)
                        (+ (+ c d) x))))

on (the false) theorems:

     (thm
       (equal (+ 11 12 x) y))

     (thm
       (implies (and (acl2-numberp c)
                     (acl2-numberp d)
                     (acl2-numberp x))
                (equal (+ c d x) y))).

One can use :brr, perhaps in conjunction with cw-gstack, to investigate
any looping.

Here is a simple example showing the value of rule good above.  Without
good, the thm form below fails.

     (defstub foo (x) t)

     (thm (equal (foo (+ 3 4 x)) (foo (+ 7 x))))

The next three examples further explore the use of quote in syntaxp
hypotheses.

We continue the examples of syntaxp hypotheses with a rule from
books/finite-set-theory/set-theory.lisp.  We will not discuss here the
meaning of this rule, but it is necessary to point out that
(ur-elementp nil) is true in this book.

     (defthm scons-nil
       (implies (and (syntaxp (not (equal a ''nil)))
                     (ur-elementp a))
                (= (scons e a)
                   (scons e nil)))).

Here also, syntaxp is used to prevent looping.  Without the
restriction, (scons e nil) would be rewritten to itself since
(ur-elementp nil) is true.
Question: Why the use of two quotes in "nil?
Hints: Nil is a constant just as 23 is.  Try :trans (cons a nil),
:trans (cons 'a 'nil), and :trans (cons "a "nil).  Also, don't forget
that the arguments to a function are evaluated before the function is
applied.

The next two rules move negative constants to the other side of an
inequality.

     (defthm |(< (+ (- c) x) y)|
       (implies (and (syntaxp (quotep c))
                     (syntaxp (< (cadr c) 0))
                     (acl2-numberp y))
                (equal (< (+ c x) y)
                       (< (fix x) (+ (- c) y)))))

     (defthm |(< y (+ (- c) x))|
       (implies (and (syntaxp (quotep c))
                     (syntaxp (< (cadr c) 0))
                     (acl2-numberp y))
                (equal (< y (+ c x))
                       (< (+ (- c) y) (fix x)))))

Questions: What would happen if (< (cadr c) '0) were used?  What about
(< (cadr c) "0)?

One can also use syntaxp to restrict the application of a rule to a
particular set of variable bindings as in the following taken from
books/ihs/quotient-remainder-lemmas.lisp.

     (encapsulate ()

       (local
        (defthm floor-+-crock
          (implies
           (and (real/rationalp x)
                (real/rationalp y)
                (real/rationalp z)
                (syntaxp (and (eq x 'x) (eq y 'y) (eq z 'z))))
           (equal (floor (+ x y) z)
                  (floor (+ (+ (mod x z) (mod y z))
                            (* (+ (floor x z) (floor y z)) z)) z)))))

       (defthm floor-+
         (implies
          (and (force (real/rationalp x))
               (force (real/rationalp y))
               (force (real/rationalp z))
               (force (not (equal z 0))))
          (equal (floor (+ x y) z)
                 (+ (floor (+ (mod x z) (mod y z)) z)
                    (+ (floor x z) (floor y z))))))

       )

We recommend the use of :brr to investigate the use of floor-+-crock.

Another useful restriction is defined by

     (defun rewriting-goal-literal (x mfc state)

       ;; Are we rewriting a top-level goal literal, rather than rewriting
       ;; to establish a hypothesis from a rewrite (or other) rule?

       (declare (ignore x state))
       (null (access metafunction-context mfc :ancestors))).

We use this restriction in the rule

     (defthm |(< (* x y) 0)|
         (implies (and (syntaxp (rewriting-goal-literal x mfc state))
                       (rationalp x)
                       (rationalp y))
                  (equal (< (* x y) 0)
                         (cond ((equal x 0)
                                nil)
                               ((equal y 0)
                                nil)
                               ((< x 0)
                                (< 0 y))
                               ((< 0 x)
                                (< y 0))))))

which has been found to be useful, but which also leads to excessive
thrashing in the linear arithmetic package if used indiscriminately.

See EXTENDED-METAFUNCTIONS for information on the use of mfc
and metafunction-context.

TERM    the three senses of well-formed ACL2 expressions or formulas

     Examples of Terms:
     (cond ((caar x) (cons t x)) (t 0))   ; an untranslated term

     (if (car (car x)) (cons 't x) '0)    ; a translated term

     (car (cons x y) 'nil v)              ; a pseudo-term

In traditional first-order predicate calculus a "term" is a syntactic
entity denoting some object in the universe of individuals.  Often, for
example, the syntactic characterization of a term is that it is either
a variable symbol or the application of a function symbol to the
appropriate number of argument terms.  Traditionally, "atomic formulas"
are built from terms with predicate symbols such as "equal" and
"member;" "formulas" are then built from atomic formulas with
propositional "operators" like "not," "and," and "implies." Theorems
are formulas.  Theorems are "valid" in the sense that the value of a
theorem is true, in any model of the axioms and under all possible
assignments of individuals to variables.

However, in ACL2, terms are used in place of both atomic formulas and
formulas.  ACL2 does not have predicate symbols or propositional
operators as distinguished syntactic entities.  The ACL2 universe of
individuals includes a "true" object (denoted by t) and a "false"
object (denoted by nil), predicates and propositional operators are
functions that return these objects.  Theorems in ACL2 are terms and
the "validity" of a term means that, under no assignment to the
variables does the term evaluate to nil.

We use the word "term" in ACL2 in three distinct senses.  We will speak
of "translated" terms, "untranslated" terms, and "pseudo-" terms.

_Translated Terms:  The Strict Sense and Internal Form_

In its most strict sense, a "term" is either a legal variable symbol, a
quoted constant, or the application of an n-ary function symbol or
closed lambda expression to a true list of n terms.

The legal variable symbols are symbols other than t or nil which are
not in the keyword package, do not start with ampersand, do not start
and end with asterisks, and if in the main Lisp package, do not violate
an appropriate restriction (see NAME).

Quoted constants are expressions of the form (quote x), where x is any
ACL2 object.  Such expressions may also be written 'x.

Closed lambda expressions are expressions of the form (lambda (v1 ...
vn) body) where the vi are distinct legal variable symbols, body is a
term, and the only free variables in body are among the vi.

The function termp, which takes two arguments, an alleged term x and a
logical world w (see WORLD), recognizes terms of a given
extension of the logic.  Termp is defined in :program mode.  Its
definition may be inspected with :pe termp for a complete specification
of what we mean by "term" in the most strict sense.  Most ACL2
term-processing functions deal with terms in this strict sense and use
termp as a guard.  That is, the "internal form" of a term satisfies
termp, the strict sense of the word "term."

_Untranslated Terms:  What the User Types_

While terms in the strict sense are easy to explore (because their
structure is so regular and simple) they can be cumbersome to type.
Thus, ACL2 supports a more sugary syntax that includes uses of macros
and constant symbols.  Very roughly speaking, macros are functions that
produce terms as their results.  Constants are symbols that are
associated with quoted objects.  Terms in this sugary syntax are
"translated" to terms in the strict sense; the sugary syntax is more
often called "untranslated."  Roughly speaking, translation just
implements macroexpansion, the replacement of constant symbols by their
quoted values, and the checking of all the rules governing the strict
sense of "term."

More precisely, macro symbols are as described in the documentation for
defmacro.  A macro, mac, can be thought of as a function, mac-fn, from
ACL2 objects to an ACL2 object to be treated as an untranslated term.
For example, caar is defined as a macro symbol; the associated macro
function maps the object x into the object (car (car x)).  A macro form
is a "call" of a macro symbol, i.e., a list whose car is the macro
symbol and whose cdr is an arbitrary true list of objects, used as a
term.  Macroexpansion is the process of replacing in an untranslated
term every occurrence of a macro form by the result of applying the
macro function to the appropriate arguments.  The "appropriate"
arguments are determined by the exact form of the definition of the
macro; macros support positional, keyword, optional and other kinds of
arguments.  See DEFMACRO.

In addition to macroexpansion and constant symbol dereferencing,
translation implements the mapping of let and let* forms into
applications of lambda expressions and closes lambda expressions
containing free variables.  Thus, the translation of

     (let ((x (1+ i))) (cons x k))

can be seen as a two-step process that first produces

     ((lambda (x) (cons x k)) (1+ i))

and then

     ((lambda (x k) (cons x k)) (1+ i) k) .

Observe that the body of the let and of the first lambda expression
contains a free k which is finally bound and passed into the second
lambda expression.

Translation also maps flet forms into applications of lambda
expressions.  See FLET.

When we say, of an event-level function such as defun or defthm, that
some argument "must be a term" we mean an untranslated term.  The event
functions translate their term-like arguments.

To better understand the mapping between untranslated terms and
translated terms it is convenient to use the keyword command :trans to
see examples of translations.  See TRANS and also see
TRANS1.

Finally, we note that the theorem prover prints terms in untranslated
form.  But there can be more than one correct untranslated term
corresponding to a given translated term.  For example, the translated
term (if x y 'nil) can be untranslated as (if x y nil) and can also be
untranslated as (and x y).  The theorem prover attempts to print an
untranslated term that is as helpful to the user as possible.  In
particular, consider a term of the form (nth k st) where st is a
single-threaded object (see STOBJ) and the kth accessor of st
is, say, kn.  The theorem prover typically would expand (kn st) to (nth
k st).  If k is large then it could be difficult for the user to make
sense out of a proof transcript that mentions the expanded term.
Fortunately, the untranslation of (nth k st) would be (nth *kn* st);
here *kn* would be a constant (see DEFCONST) added by the
defstobj event introducing st, defined to have value k.  The user can
extend this user-friendly style of printing applications of nth to
stobjs; see ADD-NTH-ALIAS.  These remarks about printing
applications of function nth extend naturally to function update-nth.
Moreover, the prover will attempt to treat terms as stobjs for the
above purpose when appropriate.  For example, if function foo has
signature ((foo * st) => (mv * * * st)), where st is introduced with
(defstobj st f0 f1), then the term (nth '1 (mv-nth '3 (foo x st0)))
will be printed as (nth *f1* (mv-nth 3 (foo x st0))).

_Pseudo-Terms:  A Common Guard for Metafunctions_

Because termp is defined in :program mode, it cannot be used
effectively in conjectures to be proved.  Furthermore, from the
perspective of merely guarding a term processing function, termp often
checks more than is required.  Finally, because termp requires the
logical world as one of its arguments it is impossible to use termp as
a guard in places where the logical world is not itself one of the
arguments.

For these reasons we support the idea of "pseudo-terms."  A pseudo-term
is either a symbol (but not necessarily one having the syntax of a
legal variable symbol), a true list beginning with quote (but not
necessarily well-formed), or the "application of" a symbol or pseudo
lambda expression to a true list of pseudo-terms.  A pseudo lambda
expression is an expression of the form (lambda (v1 ... vn) body) where
the vi are all symbols and body is a pseudo-term.

Pseudo-terms are recognized by the unary function pseudo-termp.  If
(termp x w) is true, then (pseudo-termp x) is true.  However, if x
fails to be a (strict) term it may nevertheless still be a pseudo-term.
For example, (car a b) is not a term, because car is applied to the
wrong number of arguments, but it is a pseudo-term.

The structures recognized by pseudo-termp can be recursively explored
with the same simplicity that terms can be.  In particular, if x is not
a variablep or an fquotep, then (ffn-symb x) is the function (symbol or
lambda expression) and (fargs x) is the list of argument pseudo-terms.
A metafunction (see META) or clause-processor (see
CLAUSE-PROCESSOR) may use pseudo-termp as the guard.

TERM-ORDER    the ordering relation on terms used by ACL2

ACL2 must occasionally choose which of two terms is syntactically
smaller.  The need for such a choice arises, for example, when using
equality hypotheses in conjectures (the smaller term is substituted for
the larger elsewhere in the formula), in stopping loops in permutative
rewrite rules (see LOOP-STOPPER), and in choosing the order in
which to try to cancel the addends in linear arithmetic inequalities.
When this notion of syntactic size is needed, ACL2 uses "term order."
Popularly speaking, term order is just a lexicographic ordering on
terms.  But the situation is actually more complicated.

We define term order only with respect to terms in translated form.
See TRANS.  Constants are viewed as built up by
_pseudo-function_ applications, as described at the end of this
documentation.

Term1 comes before term2 in the term order iff

     (a) the number of variable occurrences in term1 is less than that
     in term2, or

     (b) the numbers of variable occurrences in the two terms are equal
     but the number of function applications in term1 is less than that
     in term2, or

     (c) the numbers of variable occurrences in the two terms are
     equal, the numbers of functions applications in the two terms are
     equal, but pseudo-function application count for term1 is less
     than that for term2, or

     (d) the numbers of variable occurrences in the two terms are
     equal, the numbers of functions applications in the two terms are
     equal, the pseudo-function application counts for the two terms
     are equal, and term1 comes before term2 in a lexicographic
     ordering, lexorder, based their structure as Lisp objects: see
     LEXORDER.

The function term-order, when applied to the translations of two ACL2
terms, returns t iff the first is "less than or equal" to the second in
the term order.

By "number of variable occurrences" we do not mean "number of distinct
variables" but "number of times a variable symbol is mentioned."  (Cons
x x) has two variable occurrences, not one.  Thus, perhaps
counterintuitively, a large term that contains only one variable
occurrence, e.g., (standard-char-p (car (reverse x))) comes before
(cons x x) in the term order.

Since constants contain no variable occurrences and non-constant
expressions must contain at least one variable occurrence, constants
come before non-constants in the term order, no matter how large the
constants.  For example, the list constant

     '(monday tuesday wednesday thursday friday)

comes before x in the term order.  Because term order is involved in the
control of permutative rewrite rules and used to shift smaller terms to
the left, a set of permutative rules designed to allow the permutation
of any two tips in a tree representing the nested application of some
function will always move the constants into the left-most tips.  Thus,

     (+ x 3 (car (reverse klst)) (dx i j)) ,

which in translated form is

     (binary-+ x
               (binary-+ '3
                         (binary-+ (dx i j)
                                   (car (reverse klst))))),

will be permuted under the built-in commutativity rules to

     (binary-+ '3
               (binary-+ x
                         (binary-+ (car (reverse klst))
                                   (dx i j))))

or

     (+ 3 x (car (reverse klst)) (dx i j)).

Two terms with the same numbers of variable occurrences and function
applications and the same pseudo-function application count are ordered
by lexicographic means, based on their structures.  See
LEXORDER.  Thus, if two terms (member ...) and (reverse ...) contain
the same numbers of variable occurrences and function applications, and
no quoted constants, then the member term is first in the term order
because member comes before reverse in the term order (which is here
reduced to alphabetic ordering).

It remains to discuss the notion of _pseudo-function application count_.

Clearly, two constants are ordered using cases (c) and (d) of term
order, since they each contain 0 variable occurrences and no function
calls.  This raises the question "How many function applications are in
a constant?"  Because we regard the number of function applications as
a more fundamental measure of the size of a constant than lexicographic
considerations, we decided that for the purposes of term order,
constants would be seen as being built by primitive constructor
functions.  These constructor functions are not actually defined in
ACL2 but merely imagined for the purposes of term order.  We here use
suggestive names for these imagined functions, ignoring entirely the
prior use of these names within ACL2.  The imagined applications of
these functions are what we refer to as _pseudo-function_ applications.

The constant function z constructs 0.  Positive integers are
constructed from (z) by the successor function, s.  Thus 2 is (s (s
(z))) and contains three function applications.  100 contains one
hundred and one applications.  Negative integers are constructed from
their positive counterparts by -.  Thus, -2 is (- (s (s (z)))) and has
four applications.  Ratios are constructed by the dyadic function /.
Thus, -1/2 is

     (/ (- (s (z))) (s (s (z))))

and contains seven applications.  Complex rationals are similarly
constructed from rationals.  All character objects are considered
primitive and are constructed by constant functions of the same name.
Thus #\a and #\b both contain one application.  Strings are built from
the empty string, (o) by the "string-cons" function written cs.  Thus
"AB" is (cs (#\a) (cs (#\b) (o))) and contains five applications.
Symbols are obtained from strings by "packing" the symbol-name with the
unary function p.  Thus 'ab is

     (p (cs (#\a) (cs (#\b) (o))))

and has six applications.  Note that packages are here ignored and thus
'acl2::ab and 'my-package::ab each contain just six applications.
Finally, conses are built with cons, as usual.  So '(1 . 2) is (cons '1
'2) and contains six applications, since '1 contains two and '2
contains three.  This, for better or worse, answers the question "How
many function applications are in a constant?"

Finally, when we refer to the "pseudo-function application count", we
mean the number of pseudo-function applications as described above,
except that we bound this number by the constant
(fn-count-evg-max-val).  (This bound is important for efficiency, so
that constants that are very large cons structures do not cause
significant slowdown as ACL2 attempts to walk through them while
computing their pseudo-function application count.)

THE-METHOD    how to find proofs

Many users develop proof scripts in an Emacs buffer and submit one
event at a time to the theorem prover running in a *shell* buffer.  The
script buffer is logically divided into two regions: the events that
have been accepted by the theorem prover and those that have not yet
been accepted.  An imaginary "barrier" divides these two regions.  The
region above the barrier describes the state of the *shell* buffer (and
ACL2's logical world).  The region below the barrier is the "to do"
list.

We usually start a proof project by typing the key lemmas, and main
goal into the to do list.  Definitions are here just regarded as
theorems to prove (i.e., the measure conjectures).  Then we follow "The
Method."

(1) Think about the proof of the first theorem in the to do list.
Structure the proof either as an induction followed by simplification
or just simplification.  Have the necessary lemmas been proved? That
is, are the necessary lemmas in the done list already?  If so, proceed
to Step 2.  Otherwise, add the necessary lemmas at the front of the to
do list and repeat Step 1.

(2) Call the theorem prover on the first theorem in the to do list and
let the output stream into the *shell* buffer.  Abort the proof if it
runs more than a few seconds.

(3) If the theorem prover succeeded, advance the barrier past the
successful command and go to Step 1.

(4) Otherwise, inspect the failed proof attempt, starting from the
beginning, not the end.  Basically you should look for the first place
the proof attempt deviates from your imagined proof.  If your imagined
proof was inductive, inspect the induction scheme used by ACL2.  If
that is ok, then find the first subsequent subgoal that is stable under
simplification and think about why it was not proved by the simplifier.
If your imagined proof was not inductive, then think about the first
subgoal stable under simplification, as above.  Modify the script
appropriately.  It usually means adding lemmas to the to do list, just
in front of the theorem just tried.  It could mean adding hints to the
current theorem.  In any case, after the modifications go to Step 1.

We do not seriously suggest that this or any rotely applied algorithm
will let you drive ACL2 to difficult proofs.  Indeed, to remind you of
this we call this "The Method" rather than "the method."  That is, we
are aware of the somewhat pretentious nature of any such advice.  But
these remarks have helped many users approach ACL2 in a constructive
and disciplined way.

We say much more about The Method in the ACL2 book.  See the home page.
Also see SET-GAG-MODE for a discussion of a way for ACL2 to
help you to use The Method.

Learning to read failed proofs is a useful skill.  There are several
kinds of "checkpoints" in a proof: (1) a formula to which induction is
being (or would be) applied, (2) the first formula stable under
simplification, (3) a formula that is possibly generalized, either by
cross-fertilizing with and throwing away an equivalence hypothesis or
by explicit generalization of a term with a new variable.

At the induction checkpoint, confirm that you believe the formula being
proved is a theorem and that it is appropriately strong for an
inductive proof.  Read the selected induction scheme and make sure it
agrees with your idea of how the proof should go.

At the post-simplification checkpoint, which is probably the most
commonly seen, consider whether there are additional rewrite rules you
could prove to make the formula simplify still further.  Look for
compositions of function symbols you could rewrite.  Look for
contradictions among hypotheses and prove the appropriate implications:
for example, the checkpoint might contain the two hypotheses (P (F A))
and (NOT (Q (G (F A)))) and you might realize that (implies (p x) (q (g
x))) is a theorem.  Look for signs that your existing rules did not
apply, e.g., for terms that should have been rewritten, and figure out
why they were not.  Possible causes include that they do not exactly
match your old rules, that your old rules have hypotheses that cannot
be relieved here - perhaps because some other rules are missing, or
perhaps your old rules are disabled.  If you cannot find any further
simplifications to make in the formula, ask yourself whether it is
valid.  If so, sketch a proof.  Perhaps the proof is by appeal to a
combination of lemmas you should now prove?

At the two generalization checkpoints -- where hypotheses are discarded
or terms are replaced by variables -- ask yourself whether the result
is a theorem.  It often is not.  Think about rewrite rules that would
prove the formula.  These are often restricted versions of the
overly-general formulas created by the system's heuristics.

See PROOF-TREE for a discussion of a tool to help you navigate
through ACL2 proofs.

TTAGS-SEEN    list some declared trust tags (ttags)

     General Forms:
     :ttags-seen
     (ttags-seen)

Suppose the output is as follows.

     (T NIL)
     (FOO "/home/bob/bar.lisp"
          "/home/cindy/bar.lisp")
     Warning: This output is minimally trustworthy (see :DOC TTAGS-SEEN).

This output indicates that the current logical world has seen the
declaration of trust tag T at the top-level (see DEFTTAG) and
the declaration of trust tag FOO in the two books included from the
listed locations.  The warning emphasizes that this command cannot be
used to validate the "purity" of an ACL2 session, because using a ttag
renders enough power to hide from this or any other command the fact
that the ttag was ever declared.

As discussed elsewhere (see DEFTTAG), the only reliable way to
validate the "purity" of a session is to watch for "TTAG NOTE" output.

Another shortcoming of this command is that it only checks the current
logical world for ttag declarations.  For example, one could execute a
defttag event; then use progn! and set-raw-mode to replace system
functions with corrupt definitions or to introduce inconsistent axioms
in the ground-zero world; and finally, execute :ubt! 1 to remove all
evidence of the ttag in the world while leaving in place the corrupt
definitions or axioms.  The base world is now tainted, meaning we could
prove nil or certify a book that proves nil, but the resulting session
or book would contain no trace of the ttag that tainted it!

Despite shortcomings, this command might be useful to system hackers.
It also serves to illustrate the inherent flaw in asking a session
whether or how it is "tainted", justifying the "TTAG NOTE" approach
(see DEFTTAG).

TTREE    tag trees

Many low-level ACL2 functions take and return "tag trees" or "ttrees"
(pronounced "tee-trees") which contain various useful bits of
information such as the lemmas used, the linearize assumptions made,
etc.

Let a "tagged pair" be a list whose car is a symbol, called the "tag,"
and whose cdr is an arbitrary object, called the "tagged object."  A
"tag tree" is either nil, a tagged pair consed onto a tag tree, or a
non-nil tag tree consed onto a tag tree.

Abstractly a tag tree represents a list of sets, each member set having
a name given by one of the tags occurring in the ttree.  The elements
of the set named tag are all of the objects tagged tag in the tree.  To
cons a tagged pair (tag . obj) onto a tree is to add-to-set-equal obj
to the set corresponding to tag.  To cons two tag trees together is to
union-equal the corresponding sets.  The concrete representation of the
union so produced has duplicates in it, but we feel free to ignore or
delete duplicates.

The beauty of this definition is that to combine two non-nil tag trees
you need do only one cons.

The following function accumulates onto ans the set associated with a
given tag in a ttree:

     (defun tagged-objects (tag ttree ans)
      (cond
       ((null ttree) ans)
       ((symbolp (caar ttree))             ; ttree = ((tag . obj) . ttree)
        (tagged-objects tag (cdr ttree)
                        (cond ((eq (caar ttree) tag)
                               (add-to-set-equal (cdar ttree) ans))
                              (t ans))))
       (t                                  ; ttree = (ttree . ttree)
          (tagged-objects tag (cdr ttree)
                              (tagged-objects tag (car ttree) ans)))))

This function is defined as a :PROGRAM mode function in ACL2.

The rewriter, for example, takes a term and a ttree (among other
things), and returns a new term, term', and new ttree, ttree'.  Term'
is equivalent to term (under the current assumptions) and the ttree' is
an extension of ttree.  If we focus just on the set associated with the
tag LEMMA in the ttrees, then the set for ttree' is the extension of
that for ttree obtained by unioning into it all the runes used by the
rewrite.  The set associated with LEMMA can be obtained by
(tagged-objects 'LEMMA ttree nil).

TYPE-SET    how type information is encoded in ACL2

To help you experiment with type-sets we briefly note the following
utility functions.

(type-set-quote x) will return the type-set of the object x.  For
example, (type-set-quote "test") is 2048 and (type-set-quote '(a b c))
is 512.

(type-set 'term nil nil nil nil (ens state) (w state) nil nil nil) will
return the type-set of term.  For example,

     (type-set '(integerp x) nil nil nil nil (ens state) (w state) nil nil nil)

will return (mv 192 nil).  192, otherwise known as *ts-boolean*, is the
type-set containing t and nil.  The second result may be ignored in
these experiments.  Term must be in the translated, internal form shown
by :trans.  See TRANS and see TERM.

(type-set-implied-by-term 'x nil 'term (ens state)(w state) nil) will
return the type-set deduced for the variable symbol x assuming the
translated term, term, true.  The second result may be ignored in these
experiments.  For example,

     (type-set-implied-by-term 'v nil '(integerp v)
                               (ens state) (w state) nil)

returns 11.

(convert-type-set-to-term 'x ts (ens state) (w state) nil) will return
a term whose truth is equivalent to the assertion that the term x has
type-set ts.  The second result may be ignored in these experiments.
For example

     (convert-type-set-to-term 'v 523 (ens state) (w state) nil)

returns a term expressing the claim that v is either an integer or a
non-nil true-list.  523 is the logical-or of 11 (which denotes the
integers) with 512 (which denotes the non-nil true-lists).

The "actual primitive types" of ACL2 are listed in
*actual-primitive-types*, whose elements are shown below.  Each actual
primitive type denotes a set -- sometimes finite and sometimes not --
of ACL2 objects and these sets are pairwise disjoint.  For example,
*ts-zero* denotes the set containing 0 while *ts-positive-integer*
denotes the set containing all of the positive integers.

     *TS-ZERO*                  ;;; {0}
     *TS-POSITIVE-INTEGER*      ;;; positive integers
     *TS-POSITIVE-RATIO*        ;;; positive non-integer rationals
     *TS-NEGATIVE-INTEGER*      ;;; negative integers
     *TS-NEGATIVE-RATIO*        ;;; negative non-integer rationals
     *TS-COMPLEX-RATIONAL*      ;;; complex rationals
     *TS-NIL*                   ;;; {nil}
     *TS-T*                     ;;; {t}
     *TS-NON-T-NON-NIL-SYMBOL*  ;;; symbols other than nil, t
     *TS-PROPER-CONS*           ;;; null-terminated non-empty lists
     *TS-IMPROPER-CONS*         ;;; conses that are not proper
     *TS-STRING*                ;;; strings
     *TS-CHARACTER*             ;;; characters

The actual primitive types were chosen by us to make theorem proving
convenient.  Thus, for example, the actual primitive type *ts-nil*
contains just nil so that we can encode the hypothesis "x is nil" by
saying "x has type *ts-nil*" and the hypothesis "x is non-nil" by
saying "x has type complement of *ts-nil*."  We similarly devote a
primitive type to t, *ts-t*, and to a third type,
*ts-non-t-non-nil-symbol*, to contain all the other ACL2 symbols.

Let *ts-other* denote the set of all Common Lisp objects other than
those in the actual primitive types.  Thus, *ts-other* includes such
things as floating point numbers and CLTL array objects.  The actual
primitive types together with *ts-other* constitute what we call
*universe*.  Note that *universe* is a finite set containing one more
object than there are actual primitive types; that is, here we are
using *universe* to mean the finite set of primitive types, not the
infinite set of all objects in all of those primitive types.
*Universe* is a partitioning of the set of all Common Lisp objects:
every object belongs to exactly one of the sets in *universe*.

Abstractly, a "type-set" is a subset of *universe*.  To say that a
term, x, "has type-set ts" means that under all possible assignments to
the variables in x, the value of x is a member of some member of ts.
Thus, (cons x y) has type-set {*ts-proper-cons* *ts-improper-cons*}.  A
term can have more than one type-set.  For example, (cons x y) also has
the type-set {*ts-proper-cons* *ts-improper-cons* *ts-nil*}.
Extraneous types can be added to a type-set without invalidating the
claim that a term "has" that type-set.  Generally we are interested in
the smallest type-set a term has, but because the entire theorem-proving
problem for ACL2 can be encoded as a type-set question, namely, "Does p
have type-set complement of *ts-nil*?," finding the smallest type-set
for a term is an undecidable problem.  When we speak informally of
"the" type-set we generally mean "the type-set found by our heuristics"
or "the type-set assumed in the current context."

Note that if a type-set, ts, does not contain *ts-other* as an element
then it is just a subset of the actual primitive types.  If it does
contain *ts-other* it can be obtained by subtracting from *universe*
the complement of ts.  Thus, every type-set can be written as a
(possibly complemented) subset of the actual primitive types.

By assigning a unique bit position to each actual primitive type we can
encode every subset, s, of the actual primitive types by the
nonnegative integer whose ith bit is on precisely if s contains the ith
actual primitive type.  The type-sets written as the complement of s
are encoded as the twos-complement of the encoding of s.  Those
type-sets are thus negative integers.  The bit positions assigned to
the actual primitive types are enumerated from 0 in the same order as
the types are listed in *actual-primitive-types*.  At the concrete
level, a type-set is an integer between *min-type-set* and
*max-type-set*, inclusive.

For example, *ts-nil* has bit position 6.  The type-set containing just
*ts-nil* is thus represented by 64.  If a term has type-set 64 then the
term is always equal to nil.  The type-set containing everything but
*ts-nil* is the twos-complement of 64, which is -65.  If a term has
type-set -65, it is never equal to nil.  By "always" and "never" we
mean under all, or under no, assignments to the variables, respectively.

Here is a more complicated example.  Let s be the type-set containing
all of the symbols and the natural numbers.  The relevant actual
primitive types, their bit positions and their encodings are:

     actual primitive type       bit    value

     *ts-zero*                    0       1
     *ts-positive-integer*        1       2
     *ts-nil*                     6      64
     *ts-t*                       7     128
     *ts-non-t-non-nil-symbol*    8     256

Thus, the type-set s is represented by (+ 1 2 64 128 256) = 451.  The
complement of s, i.e., the set of all objects other than the natural
numbers and the symbols, is -452.

UNTRANSLATE    See USER-DEFINED-FUNCTIONS-TABLE.

USE    hints keyword :USE

See HINTS.

USING-COMPUTED-HINTS    how to use computed hints

Computed hints (see COMPUTED-HINTS) are extraordinarily
powerful.  We show a few examples here to illustrate their use.  We
recommend that the using-computed-hints-n topics be read in the order
using-computed-hints-1, using-computed-hints-2, and so on.

Related topics other than immediate subtopics:

USING-COMPUTED-HINTS-1    Driving Home the Basics

The common hint

     ("Subgoal 3.2.1''" :use lemma42)

has the same effect as the computed hint

     (if (equal id '((0) (3 2 1) . 2))
         '(:use lemma42)
         nil)

which, of course, is equivalent to

     (and (equal id '((0) (3 2 1) . 2))
          '(:use lemma42))

which is also equivalent to the computed hint

     my-special-hint

provided the following defun has first been executed

     (defun my-special-hint (id clause world)
       (declare (xargs :mode :program)
                (ignore clause world))
       (if (equal id '((0) (3 2 1) . 2))
           '(:use lemma42)
           nil))

It is permitted for the defun to be in :LOGIC mode (see
DEFUN-MODE) also.

Just to be concrete, the following three events all behave the same way
(if my-special-hint is as above):

     (defthm main (big-thm a b c)
       :hints (("Subgoal 3.2.1''" :use lemma42)))

     (defthm main (big-thm a b c)
       :hints ((and (equal id '((0) (3 2 1) . 2)) '(:use lemma42))))

     (defthm main (big-thm a b c)
       :hints (my-special-hint))

USING-COMPUTED-HINTS-2    One Hint to Every Top-Level Goal in a Forcing Round

Suppose the main proof completes with a forcing round on three
subgoals, "[1]Subgoal 3", "[1]Subgoal 2", and "[1]Subgoal 1".  Suppose
you wish to :use lemma42 in all top-level goals of the first forcing
round.  This can be done supplying the hint

     (if test '(:use lemma42) nil),

where test is an expression that returns t when ID is one of the clause
ids in question.

         goal-spec     (parse-clause-id goal-spec)

     "[1]Subgoal 3"        ((1) (3) . 0)
     "[1]Subgoal 2"        ((1) (2) . 0)
     "[1]Subgoal 1"        ((1) (1) . 0)

Recall (see CLAUSE-IDENTIFIER) that parse-clause-id maps from a
goal spec to a clause id, so you can use that function on the goal
specs printed in the failed proof attempt to determine the clause ids
in question.

So one acceptable test is

     (member-equal id '(((1) (3) . 0)
                        ((1) (2) . 0)
                        ((1) (1) . 0)))

or you could use parse-clause-id in your computed hint if you don't
want to see clause ids in your script:

     (or (equal id (parse-clause-id "[1]Subgoal 3"))
         (equal id (parse-clause-id "[1]Subgoal 2"))
         (equal id (parse-clause-id "[1]Subgoal 1")))

or you could use the inverse function (see CLAUSE-IDENTIFIER):

     (member-equal (string-for-tilde-@-clause-id-phrase id)
                   '("[1]Subgoal 3"
                     "[1]Subgoal 2"
                     "[1]Subgoal 1"))

Recall that what we've shown above are the tests to use in the computed
hint.  The hint itself is (if test '(:use lemma42) nil) or something
equivalent like (and test '(:use lemma42)).

The three tests above are all equivalent.  They suffer from the problem
of requiring the explicit enumeration of all the goal specs in the
first forcing round.  A change in the script might cause more forced
subgoals and the ones other than those enumerated would not be given
the hint.

You could write a test that recognizes all first round top-level
subgoals no matter how many there are.  Just think of the programming
problem:  how do I recognize all the clause id's of the form ((1) (n) .
0)?  Often you can come to this formulation of the problem by using
parse-clause-id on a few of the candidate goal-specs to see the common
structure.  A suitable test in this case is:

     (and (equal (car id) '(1))     ; forcing round 1, top-level (pre-induction)
          (equal (len (cadr id)) 1) ; Subgoal n (not Subgoal n.i ...)
          (equal (cddr id) 0))      ; no primes

The test above is "overkill" because it recognizes precisely the clause
ids in question.  But recall that once a computed hint is used, it is
(by default) removed from the hints available to the children of the
clause.  Thus, we can widen the set of clause ids recognized to include
all the children without worrying that the hint will be applied to
those children.

In particular, the following test supplies the hint to every top-level
goal of the first forcing round:

     (equal (car id) '(1))

You might worry that it would also supply the hint to the subgoal
produced by the hint - the cases we ruled out by the "overkill" above.
But that doesn't happen since the hint is unavailable to the children.
You could even write:

     (equal (car (car id)) 1)

which would supply the hint to every goal of the form "[1]Subgoal ..."
and again, because we see and fire on the top-level goals first, we
will not fire on, say, "[1]Subgoal *1.3/2", i.e., the id '((1 1 3) (2)
. 0) even though the test recognizes that id.

Finally, the following test supplies the hint to every top-level goal
of every forcing round (except the 0th, which is the "gist" of the
proof, not "really" a forcing round):

     (not (equal (car (car id)) 0))

Recall again that in all the examples above we have exhibited the test
in a computed hint of the form (if test '(:key1 val1 ...) nil).

USING-COMPUTED-HINTS-3    Hints as a Function of the Goal (not its Name)

Sometimes it is desirable to supply a hint whenever a certain term
arises in a conjecture.  For example, suppose we have proved

     (defthm all-swaps-have-the-property
        (the-property (swap x))
        :rule-classes nil)

and suppose that whenever (SWAP A) occurs in a goal, we wish to add the
additional hypothesis that (THE-PROPERTY (SWAP A)).  Note that this is
equivalent supplying the hint

     (if test
         '(:use (:instance all-swaps-have-the-property (x A)))
         nil)

where test answers the question "does the clause contain (SWAP A)?"
That question can be asked with (occur-lst '(SWAP A) clause).  Briefly,
occur-lst takes the representation of a translated term, x, and a list
of translated terms, y, and determines whether x occurs as a subterm of
any term in y.  (By "subterm" here we mean proper or improper, e.g.,
the subterms of (CAR X) are X and (CAR X).)

Thus, the computed hint:

     (if (occur-lst '(swap a) clause)
         '(:use (:instance all-swaps-have-the-property (x A)))
         nil)

will add the hypothesis (THE-PROPERTY (SWAP A)) to every goal
containing (SWAP A) - except the children of goals to which the
hypothesis was added.

A COMMON MISTAKE users are likely to make is to forget that they are
dealing with translated terms.  For example, suppose we wished to look
for (SWAP (LIST 1 A)) with occur-lst.  We would never find it with

     (occur-lst '(SWAP (LIST 1 A)) clause)

because that presentation of the term contains macros and other
abbreviations.  By using :trans (see TRANS) we can obtain the
translation of the target term.  Then we can look for it with:

     (occur-lst '(SWAP (CONS '1 (CONS A 'NIL))) clause)

Note in particular that you must

     * eliminate all macros and
     * explicitly quote all constants.

We recommend using :trans to obtain the translated form of the terms in
which you are interested, before programming your hints.

An alternative is to use the expression (prettyify-clause clause nil
nil) in your hint to convert the current goal clause into the
s-expression that is actually printed.  For example, the clause

     ((NOT (CONSP X)) (SYMBOLP Y) (EQUAL (CONS '1 (CAR X)) Y))

"prettyifies" to

     (IMPLIES (AND (CONSP X)
                   (NOT (SYMBOLP Y)))
              (EQUAL (CONS 1 (CAR X)) Y))

which is what you would see printed by ACL2 when the goal clause is
that shown.

However, if you choose to convert your clauses to prettyified form, you
will have to write your own explorers (like our occur-lst), because all
of the ACL2 term processing utilities work on translated and/or clausal
forms.  This should not be taken as a terrible burden.  You will, at
least, gain the benefit of knowing what you are really looking for,
because your explorers will be looking at exactly the s-expressions you
see at your terminal.  And you won't have to wade through our still
undocumented term/clause utilities.  The approach will slow things down
a little, since you will be paying the price of independently consing
up the prettyified term.

We make one more note on this example.  We said above that the computed
hint:

     (if (occur-lst '(swap a) clause)
         '(:use (:instance all-swaps-have-the-property (x A)))
         nil)

will add the hypothesis (THE-PROPERTY (SWAP A)) to every goal
containing (SWAP A) - except the children of goals to which the
hypothesis was added.

It bears noting that the subgoals produced by induction and top-level
forcing round goals are not children.  For example, suppose the hint
above fires on "Subgoal 3" and produces, say, "Subgoal 3'".  Then the
hint will not fire on "Subgoal 3'" even though it (still) contains
(SWAP A) because "Subgoal 3'" is a child of a goal on which the hint
fired.

But now suppose that "Subgoal 3'" is pushed for induction.  Then the
goals created by that induction, i.e., the base case and induction
step, are not considered children of "Subgoal 3'".  All of the original
hints are available.

Alternatively, suppose that "Subgoal 3' is proved but forces some other
subgoal, "[1]Subgoal 1" which is attacked in Forcing Round 1.  That
top-level forced subgoal is not a child.  All the original hints are
available to it.  Thus, if it contains (SWAP A), the hint will fire and
supply the hypothesis, producing "[1]Subgoal 1'".  This may be
unnecessary, as the hypothesis might already be present in "[1]Subgoal
1".  In this case, no harm is done.  The hint won't fire on "[1]Subgoal
1" because it is a child of "[1]Subgoal 1" and the hint fired on that.

USING-COMPUTED-HINTS-4    Computing the Hints

So far we have used computed hints only to compute when a fixed set of
keys and values are to be used as a hint.  But computed hints can, of
course, compute the set of keys and values.  You might, for example,
write a hint that recognizes when a clause "ought" to be provable by a
:BDD hint and generate the appropriate hint.  You might build in a set
of useful lemmas and check to see if the clause is provable :BY one of
them.  You can keep all function symbols disabled and use computed
hints to compute which ones you want to :EXPAND.  In general, you can
write a theorem prover for use in your hints, provided you can get it
do its job by directing our theorem prover.

Suppose for example we wish to find every occurrence of an instance of
(SWAP x) and provide the corresponding instance of
ALL-SWAPS-HAVE-THE-PROPERTY.  Obviously, we must explore the clause
looking for instances of (SWAP x) and build the appropriate instances
of the lemma.  We could do this in many different ways, but below we
show a general purpose set of utilities for doing it.  The functions
are not defined in ACL2 but could be defined as shown.

Our plan is:  (1) Find all instances of a given pattern (term) in a
clause, obtaining a set of substitutions.  (2) Build a set of :instance
expressions for a given lemma name and set of substitutions.  (3)
Generate a :use hint for those instances when instances are found.

The pair of functions below find all instances of a given pattern term
in either a term or a list of terms.  The functions each return a list
of substitutions, each substitution accounting for one of the matches
of pat to a subterm.  At this level in ACL2 substitutions are lists of
pairs of the form (var . term).  All terms mentioned here are presumed
to be in translated form.

The functions take as their third argument a list of substitutions
accumulated to date and add to it the substitutions produced by
matching pat to the subterms of the term.  We intend this accumulator
to be nil initially.  If the returned value is nil, then no instances
of pat occurred.

     (mutual-recursion

     (defun find-all-instances (pat term alists)
      (declare (xargs :mode :program))
      (mv-let
       (instancep alist)
       (one-way-unify pat term)
       (let ((alists (if instancep (add-to-set-equal alist alists) alists)))
         (cond
          ((variablep term) alists)
          ((fquotep term) alists)
          ((flambdap (ffn-symb term))
           (find-all-instances pat
                               (lambda-body (ffn-symb term))
                               (find-all-instances-list pat (fargs term) alists)))
          (t (find-all-instances-list pat (fargs term) alists))))))

     (defun find-all-instances-list (pat list-of-terms alists)
      (declare (xargs :mode :program))
      (cond
       ((null list-of-terms) alists)
       (t (find-all-instances pat
                              (car list-of-terms)
                              (find-all-instances-list pat
                                                       (cdr list-of-terms)
                                                       alists))))))

We now turn our attention to converting a list of substitutions into a
list of lemma instances, each of the form

     (:INSTANCE name (var1 term1) ... (vark termk))

as written in :use hints.  In the code shown above, substitutions are
lists of pairs of the form (var . term), but in lemma instances we must
write "doublets."  So here we show how to convert from one to the other:

     (defun pairs-to-doublets (alist)
       (declare (xargs :mode :program))
       (cond ((null alist) nil)
             (t (cons (list (caar alist) (cdar alist))
                      (pairs-to-doublets (cdr alist))))))

Now we can make a list of lemma instances:

     (defun make-lemma-instances (name alists)
       (declare (xargs :mode :program))
       (cond
        ((null alists) nil)
        (t (cons (list* :instance name (pairs-to-doublets (car alists)))
                 (make-lemma-instances name (cdr alists))))))

Finally, we can package it all together into a hint function.  The
function takes a pattern, pat, which must be a translated term, the
name of a lemma, name, and a clause.  If some instances of pat occur in
clause, then the corresponding instances of name are :USEd in the
computed hint.  Otherwise, the hint does not apply.

     (defun add-corresponding-instances (pat name clause)
       (declare (xargs :mode :program))
       (let ((alists (find-all-instances-list pat clause nil)))
         (cond
          ((null alists) nil)
          (t (list :use (make-lemma-instances name alists))))))

The design of this particular hint function makes it important that the
variables of the pattern be the variables of the named lemma and that
all of the variables we wish to instantiate occur in the pattern.  We
could, of course, redesign it to allow "free variables" or some sort of
renaming.

We could now use this hint as shown below:

     (defthm ... ...
       :hints ((add-corresponding-instances
                '(SWAP x)
                'ALL-SWAPS-HAVE-THE-PROPERTY
                clause)))

The effect of the hint above is that any time a clause arises in which
any instance of (SWAP x) appears, we add the corresponding instance of
ALL-SWAPS-HAVE-THE-PROPERTY.  So for example, if Subgoal *1/3.5
contains the subterm (SWAP (SWAP A)) then this hint fires and makes the
system behave as though the hint:

     ("Subgoal *1/3.5"
      :USE ((:INSTANCE ALL-SWAPS-HAVE-THE-PROPERTY (X A))
            (:INSTANCE ALL-SWAPS-HAVE-THE-PROPERTY (X (SWAP A)))))

had been present.

USING-COMPUTED-HINTS-5    Debugging Computed Hints

We have found that it is sometimes helpful to define hints so that they
print out messages to the terminal when they fire, so you can see what
hint was generated and which of your computed hints did it.

To that end we have defined a macro we sometimes use.  Suppose you have
a :hints specification such as:

     :hints (computed-hint-fn (hint-expr id))

If you defmacro the macro below you could then write instead:

     :hints ((show-hint computed-hint-fn 1)
             (show-hint (hint-expr id) 2))

with the effect that whenever either hint is fired (i.e., returns
non-nil), a message identifying the hint by the marker (1 or 2, above)
and the non-nil value is printed.

     (defmacro show-hint (hint &optional marker)
       (cond
        ((and (consp hint)
              (stringp (car hint)))
         hint)
        (t
         `(let ((marker ,marker)
                (ans ,(if (symbolp hint)
                          `(,hint id clause world stable-under-simplificationp)
                        hint)))
            (if ans
                (prog2$
                 (cw "~%***** Computed Hint~#0~[~/ (from hint ~x1)~]~%~x2~%~%"
                     (if (null marker) 0 1)
                     marker
                     (cons (string-for-tilde-@-clause-id-phrase id)
                           ans))
                 ans)
              nil)))))

Note that when show-hint is applied to a hint that is a symbol, e.g.,
computed-hint-fn, it applies the symbol to the four computed-hint
arguments: id, clause, world, and stable-under-simplificationp.  If
computed-hint-fn is of arity 3 the code above would cause an error.
One way to avoid it is to write

     :hints ((show-hints (computed-hint-fn id clause world) 1)
             (show-hint (hint-expr id) 2)).

If you only use computed hints of arity 3, you might eliminate the
occurrence of stable-under-simplificationp in the definition of
show-hint above.

Putting a show-hint around a common hint has no effect.  If you find
yourself using this utility let us know and we'll consider putting it
into the system itself.  But it does illustrate that you can use
computed hints to do unusual things.

USING-COMPUTED-HINTS-6    Using the computed-hint-replacement feature

So far none of our computed hints have used the
:COMPUTED-HINT-REPLACEMENT feature.  We now illustrate that.

The :computed-hint-replacement feature can easily lead to loops.  So as
you experiment with the examples in this section and your own hints
using this feature, be ready to interrupt the theorem prover and abort!

A non-looping use of the :computed-hint-replacement feature would be a
hint like this:

     (if (certain-terms-present clause)
         '(:computed-hint-replacement t
           :in-theory (enable lemma25))
         '(:computed-hint-replacement t
           :in-theory (disable lemma25)))

In this hint, if certain terms are present in clause, as determined by
the function with the obvious name (here undefined), then this hint
enables lemma25 and otherwise disables it.  Lemma25 might be a very
expensive lemma, e.g., one that matches frequently and has an expensive
and rarely established hypothesis.  One might wish it enabled only
under certain conditions.  Recall that theories are inherited by
children.  So once lemma25 is enabled it "stays" enabled for the
children, until disabled; and vice versa.  If the
:computed-hint-replacement feature were not present and computed hints
were always deleted after they had been used, then lemma25 would be
left enabled (or disabled) for all the childen produced by the first
firing of the hint.  But with the arrangement here, every subgoal gets
a theory deemed suitable by the hint, and the hint persists.

Now we will set up a toy to allow us to play with computed hints to
understand them more deeply.  To follow the discussion it is best to
execute the following events.

     (defstub wrapper (x) t)
     (defaxiom wrapper-axiom (wrapper x) :rule-classes nil)

Now submit the following event and watch what happens.

     (thm (equal u v)
       :hints (`(:use (:instance wrapper-axiom (x a)))))

The theorem prover adds (wrapper a) to the goal and then abandons the
proof attempt because it cannot prove the subgoal.  Since the computed
hint is deleted upon use, the hint is not applied to the subgoal (i.e.,
the child of the goal).

What happens if we do the following?

     (thm (equal u v)
       :hints (`(:computed-hint-replacement t
                 :use (:instance wrapper-axiom (x a)))))

As one might expect, this loops forever: The hint is applied to the
child and adds the hypothesis again.  When the hint fires, nothing is
actually changed, since (wrapper a) is already in the subgoal.

So let's change the experiment a little.  Let's make the hint add the
hypothesis (wrapper p) where p is the first literal of the clause.
This is silly but it allows us to explore the behavior of computed
hints a little more.

     (thm (equal u v)
       :hints (`(:use (:instance wrapper-axiom (x ,(car clause))))))

So in this case, the theorem prover changes the goal to

     (IMPLIES (WRAPPER (EQUAL U V)) (EQUAL U V))

which then simplifies to

     (IMPLIES (WRAPPER NIL) (EQUAL U V))

because the concluding equality can be assumed false in the hypothesis
(e.g., think of the contrapositive version).  Nothing else happens
because the hint has been removed and so is not applicable to the child.

Now consider the following - and be ready to interrupt it and abort!

     (thm (equal u v)
       :hints (`(:computed-hint-replacement t
                 :use (:instance wrapper-axiom (x ,(car clause))))))

This time the hint is not removed and so is applied to the child.  So
from Goal we get

     Goal'
     (IMPLIES (WRAPPER (EQUAL U V))
              (EQUAL U V))

and then

     Goal''
     (IMPLIES (AND (WRAPPER (NOT (WRAPPER (EQUAL U V))))
                   (WRAPPER (EQUAL U V)))
              (EQUAL U V))

etc.

First, note that the hint is repeatedly applied to its children.  That
is because we wrote :computed-hint-replacement t.  But second, note
that Goal' is not even being simplified before Goal" is produced from
it.  If it were being simplified, the (equal u v)'s in the hypotheses
would be replaced by nil.  This is a feature.  It means after a
computed hint has fired, other hints are given a chance at the result,
even the hint itself unless it is removed from the list of hints.

As an exercise, let's arrange for the hint to stay around and be
applied indefinitely but with a simplification between each use of the
the hint.  To do this we need to pass information from one application
of the hint to the next, essentially to say "stay around but don't
fire."

First, we will define a function to use in the hint.  This is more than
a mere convenience; it allows the hint to "reproduce itself" in the
replacement.

     (defun wrapper-challenge (clause parity)
       (if parity
           `(:computed-hint-replacement ((wrapper-challenge clause nil))
             :use (:instance wrapper-axiom (x ,(car clause))))
           `(:computed-hint-replacement ((wrapper-challenge clause t)))))

Note that this function is not recursive, even though it uses its own
name.  That is because the occurrence of its name is in a quoted
constant.

Now consider the following.  What will it do?

     (thm (equal u v)
       :hints ((wrapper-challenge clause t)))

First, observe that this is a legal hint because it is a term that
mentions only the free variable CLAUSE.  When defining hint functions
you may sometimes think their only arguments are the four variables id,
clause, world, and stable-under-simplificationp.  That is not so.  But
in your hints you must call those functions so that those are the only
free variables.  Note also that the occurrence of clause inside the
:computed-hint-replacement is not an occurrence of the variable clause
but just a constant.  Just store this note away for a moment.  We'll
return to it momentarily.

Second, the basic cleverness of this hint is that every time it fires
it reproduces itself with the opposite parity.  When the parity is t it
actually changes the goal by adding a hypothesis.  When the parity is
nil it doesn't change the goal and so allows simplification to proceed
- but it swaps the parity back to t.  What you can see with this simple
toy is that we can use the computed hints to pass information from
parent to child.

Ok, so what happens when the event above is executed?  Try it.  You will
see that ACL2 applied the hint the first time.  It doesn't get around to
printing the output because an error is caused before it can print.
But here is a blow-by-blow description of what happens.  The hint is
evaluated on Goal with the clause ((equal u v)).  It produces a hint
exactly as though we had typed:

     ("Goal" :use (:instance wrapper-axiom (x (equal u v))))

which is applied to this goal. In addition, it produces the new hints
argument

     :hints ((wrapper-challenge clause nil)).

By applying the "Goal" hint we get the new subgoal

     Goal'
     (implies (wrapper (equal u v))
              (equal u v))

but this is not printed because, before printing it, the theorem prover
looks for hints to apply to it and finds

     (wrapper-challenge clause nil)

That is evaluated and produces a hint exactly as though we had typed:

     ("Goal'" )

and the new hints argument:

     :hints ((wrapper-challenge clause nil)).

But if you supply the hint ("Goal'" ), ACL2 will signal an error
because it does not allow you to specify an empty hint!

So the definition of wrapper-challenge above is almost correct but
fatally flawed.  We need a non-empty "no-op" hint.  One such hint is to
tell the system to expand a term that will always be expanded anyway.
So undo wrapper-challenge, redefine it, and try the proof again.  Now
remember the observation about clause that we asked you to "store"
above.  The new definition of wrapper-challenge illustrates what we
meant.  Note that the first formal parameter of wrapper-challenge,
below, is no longer named clause but is called cl instead.  But the
"call" of wrapper-challenge in the replacements is on clause.  This may
seem to violate the rule that a function definition cannot use
variables other than the formals.  But the occurrences of clause below
are not variables but constants in an object that will eventually be
treated as hint term.

     :ubt wrapper-challenge

     (defun wrapper-challenge (cl parity)
       (if parity
           `(:computed-hint-replacement ((wrapper-challenge clause nil))
             :use (:instance wrapper-axiom (x ,(car cl))))
           `(:computed-hint-replacement ((wrapper-challenge clause t))
             :expand ((atom zzz)))))

     (thm (equal u v)
       :hints ((wrapper-challenge clause t)))

This time, things go as you might have expected!  Goal' is produced and
simplified, to

     Goal''
     (implies (wrapper nil)
              (equal u v)).

Simplification gets a chance because when the new hint
(wrapper-challenge clause nil) is fired it does not change the goal.
But it does change the parity in the hints argument so that before
Goal" is simplified again, the hint fires and adds the hypothesis:

     Goal'''
     (IMPLIES (AND (WRAPPER (NOT (WRAPPER NIL)))
                   (WRAPPER NIL))
              (EQUAL U V)).

This simplifies, replacing the first (NOT (WRAPPER NIL)) by NIL, since
(WRAPPER NIL) is known to be true here.  Thus the goal simplifies to

     Goal'4'
     (IMPLIES (WRAPPER NIL) (EQUAL U V)).

The process repeats indefinitely.

So we succeeded in getting a hint to fire indefinitely but allow a full
simplification between rounds.

USING-COMPUTED-HINTS-7    Using the stable-under-simplificationp flag

A problem with the example in using-computed-hints-6 is that exactly
one simplification occurs between each (effective) firing of the hint.
Much more commonly we wish to fire a hint once a subgoal has become
stable under simplification.

A classic example of this is when we are dealing with an interpreter
for some state machine.  We typically do not want the "step" function
to open up on the symbolic representation of a state until that state
has been maximally simplified.  We will illustrate with a simple state
machine.

Let us start by defining the step function, stp, and the corresponding
run function that applies it a given number of times.

     (defun stp (s)
       (+ 1 s))

     (defun run (s n)
       (if (zp n)
           s
           (run (stp s) (- n 1))))

The step function here is trivial:  a state is just a number and the
step function increments it.  In this example we will not be interested
in the theorems we prove but in how we prove them.  The formula we will
focus on is

     (thm (equal (run s 7) xxx))

This is not a theorem, of course.  But we want to test our advice on
non-theorems because we do not want the advice to work only for proofs
that succeed.  (In the past, we gave advice about using computed hints
and that advice caused the theorem prover to run forever when given
formulas that it couldn't prove - but most of the time the system is
presented with formulas it cannot prove!)

Furthermore, without some kind of additional rules, the (run s 7)
expression in the conjecture above will not expand at all, because
ACL2's heuristics do not approve.

In fact, we do not want to take chances that run will be expanded - we
want to control its expansion completely.  Therefore, disable run.

     (in-theory (disable run))

Now, what do we want?  (That is always a good question to ask!)  We want
(run s 7) to expand "slowly."  In particular, we want it to expand
once, to (run (stp s) 6).  Then we want the stp to be expanded and
fully simplified before the run expression is expanded again.  That is,
we want to force the expansion of run whenever the goal is stable under
simplification.  This is sometimes called "staged simplification."

We can achieve staged simplification for any given function symbol by
defining the functions shown below and then using a simple computed
hint:

     (thm (equal (run s 7) xxx)
          :hints ((stage run)))

By inspecting how stage is defined you can see how to extend it, but we
explain as we go.  To experiment, you can just paste the definitions
(and defmacro) below into your ACL2 shell and then try the thm command.

First, define this pair of mutually recursive functions.
Find-first-call finds the first call of the function symbol fn in a
given term.

     (mutual-recursion
      (defun find-first-call (fn term)
      ; Find the first call of fn in term.
       (cond ((variablep term) nil)
             ((fquotep term) nil)
             ((equal (ffn-symb term) fn)
              term)
             (t (find-first-call-lst fn (fargs term)))))
      (defun find-first-call-lst (fn lst)
      ; Find the first call of fn in a list of terms.
       (cond ((endp lst) nil)
             (t (or (find-first-call fn (car lst))
                    (find-first-call-lst fn (cdr lst)))))))

We will arrange for the computed hint to generate an :EXPAND hint for
the first call of fn, whenever the goal becomes stable under
simplification.  If no call is found, the hint will do nothing.  To
make sure the hint will not loop indefinitely (for example, by forcing
fn to expand only to have the rewriter "fold" it back up again), we
will provide the hint with a bound that stops it after some number of
iterations.  Here is the basic function that creates the expand hint
and replaces itself to count down.

     (defun stage1 (fn max clause flg)
     ; If the clause is stable under simplification and there is a call of
     ; fn in it, expand it.  But don't do it more than max times.
      (let ((temp (and flg
                       (find-first-call-lst fn clause))))
        (if temp
            (if (zp max)
                (cw "~%~%HINT PROBLEM:  The maximum repetition count of ~
                     your STAGE hint been reached without eliminating ~
                     all of the calls of ~x0.  You could supply a larger ~
                     count with the optional second argument to STAGE ~
                     (which defaults to 100).  But think about what is ~
                     happening! Is each stage permanently eliminating a ~
                     call of ~x0?~%~%"
                    fn)
              `(:computed-hint-replacement
                 ((stage1 ',fn ,(- max 1)
                          clause
                          stable-under-simplificationp))
                :expand (,temp)))
          nil)))

Suppose that when stage1 is called, fn is the function we want to
expand, max is the maximum number of iterations of this expansion,
clause is the current goal clause, and flg is the value of the
stable-under-simplificationp flag.  Then if clause is stable and we can
find a call of fn in it, we ask whether max is exhausted.  If so, we
print an "error message" to the comment window with cw and return nil
(the value of cw).  That nil means the hint does nothing.  But if max
is not yet exhausted, we return a new hint.  As you can see above, the
hint replaces itself with another stage1 hint with the same fn and a
decremented max to be applied to the new clause and the then-current
value of stable-under-simplificationp.  The hint also contains an
:expand directive for the call of fn found.

Thus, if the computed hint was:

     (stage1 'run 5 clause stable-under-simplificationp)

and (run s 7) occurs in the clause, then it will generate

     (:computed-hint-replacement
       ((stage1 'run 4 clause stable-under-simplificationp))
      :expand ((run s 7)))

which will in turn replace the old stage1 hint with the new one and
will apply :expand ((run s 7)) to the current goal.

We can make this more convenient by defining the macro:

     (defmacro stage (fn &optional (max '100))
      `(stage1 ',fn ,max clause stable-under-simplificationp))

Note that the macro allows us to either provide the maximum bound or
let it default to 100.

Henceforth, we can type

     (thm (equal (run s 7) xxx)
          :hints ((stage run)))

to stage the opening of run up to 100 times, or we can write

     (thm (equal (run s 7) xxx)
          :hints ((stage run 5)))

to stage it only 5 times.  In the latter example, the system with print
a "error message" after the fifth expansion.

Note that if we executed

     (set-default-hints '((stage run)))

then we could attack all theorems (involving run) with staged
simplification (up to bound 100), without typing an explicit hint.

     (thm (equal (run s 7) xxx))

Using techniques similar to those above we have implemented "priority
phased simplification" and provided it as a book.  See
books/misc/priorities.lisp.  This is an idea suggested by Pete
Manolios, by which priorities may be assigned to rules and then the
simplifier simplifies each subgoal maximally under the rules of a given
priority before enabling the rules of the next priority level.  The
book above documents both how we implement it with computed hints and
how to use it.

Here is another example of using the stable-under-simplificationp flag
to delay certain actions.  It defines a default hint, see
DEFAULT-HINTS, which will enable non-linear-arithmetic on precisely
those goals which are stable-under-simplificationp.  It also uses the
HISTORY and PSPV variables to determine when toggling
non-linear-arithmetic is appropriate.  These variables are documented
only in the source code.  If you start using these variables
extensively, please contact the developers of ACL2 or Robert Krug
(rkrug@cs.utexas.edu) and let us know how we can help.

     (defun nonlinearp-default-hint (stable-under-simplificationp hist pspv)
       (cond (stable-under-simplificationp
              (if (not (access rewrite-constant
                               (access prove-spec-var pspv :rewrite-constant)
                               :nonlinearp))
                  '(:computed-hint-replacement t
                    :nonlinearp t)
                nil))
             ((access rewrite-constant
                      (access prove-spec-var pspv :rewrite-constant)
                      :nonlinearp)
              (if (not (equal (caar hist) 'SETTLED-DOWN-CLAUSE))
                  '(:computed-hint-replacement t
                    :nonlinearp nil)
                nil))
             (t
              nil)))

USING-COMPUTED-HINTS-8    Some Final Comments

None of the examples show the use of the variable WORLD, which is
allowed in computed hints.  There are some (undocumented) ACL2
utilities that might be useful in programming hints, but these
utilities need access to the ACL2 logical world (see WORLD).

A very useful fact to know is that (table-alist name world) returns an
alist representation of the current value of the table named name.

The ACL2 source code is littered with :program mode functions for
manipulating world.  In our source code, the world is usually bound a
variable named wrld; so searching our code for that name might be
helpful.

Using these utilities to look at the WORLD one can, for example,
determine whether a symbol is defined recursively or not, get the body
and formals of a defined function, or fetch the statement of a given
lemma.  Because these utilities are not yet documented, we do not
expect users to employ WORLD in computed hints.  But experts might and
it might lead to the formulation of a more convenient language for
computed hints.

None of our examples illustrated the 7 argument form of a computed hint,
(fn ID CLAUSE WORLD STABLE-UNDER-SIMPLIFICATIONP HIST PSPV CTX).  When
used, the variables HIST, PSPV, and CTX, are bound to the clause
history, the package of "special variables" governing the clause, and
the "error message context."  These variables are commonly used
throughout our source code but are, unfortunately, undocumented.
Again, we expect a few experts will find them useful in developing
computed hints.

If you start using computed hints extensively, please contact the
developers of ACL2 and let us know what you are doing with them and how
we can help.

VERSION    ACL2 Version Number

To determine the version number of your copy of ACL2, evaluate the form
(@ acl2-version).  The value will be a string.  For example,

     ACL2 !>(@ acl2-version)
     "ACL2 Version 3.4"

The part of the string after "ACL2 Version " is of the form x.y or
x.y.z, optionally followed by a succession of values in parentheses,
where x, y, and z are natural numbers.  If z is omitted then it is
implicitly 0.  We refer to X, y, and z as the "major", "minor", and
"incrl" fields, respectively.  The incrl field is used for incremental
releases.  The discussion just below assumes that incremental releases
are not employed at the user's site, i.e., the incrl fields are always
0.  We remove this assumption when we discuss incremental releases at
the end of this documenttation topic.

Books are considered certified only in the same version of ACL2 in
which the certification was done.  The certificate file records the
version number of the certifying ACL2 and include-book considers the
book uncertified if that does not match the current version number.
Thus, each time we release a new version of ACL2, previously certified
books should be recertified.

Note that there are over 150 constants in the system, most having to do
with the fact that ACL2 is coded in ACL2.  Many of these, for example
*common-lisp-specials-and-constants* and *acl2-exports*, may change
from version to version, and this can cause unsoundness.  For example,
the symbol 'set-difference-eq was added to *acl2-exports* in
Version_2.9, so we can certify a book in Version_2.8 containing the
following theorem, which is false in Version_2.9.

     (null (member 'set-difference-eq *acl2-exports*))

Therefore, we need to disallow inclusion of such a book in a Version_2.9
session, which otherwise would allow us to prove nil.  Furthermore, it
is possible that from one version of the system to another we might
change, say, the default values on some system function or otherwise
make "intentional" changes to the axioms.  It is even possible one
version of the system is discovered to be unsound and we release a new
version to correct our error.

Therefore we adopted the draconian policy that books are certified by a
given version of ACL2 and "must" be recertified to be used in other
versions.  We put "must" in quotes because in fact, ACL2 allows a book
that was certified in one ACL2 version to be included in a later
version, using include-book.  But ACL2 does not allow certify-book to
succeed when such an include-book is executed on its behalf.  Also, you
may experience undesirable behavior if you avoid recertification when
moving to a different version.  Hence we recommend that you stick to
the draconion policy of recertifying books when updating to a new ACL2
version.

The string (@ acl2-version) can contain implementation-specific
information in addition to the version number.  For example, in
Macintosh Common Lisp (MCL) (char-code #Newline) is 13, while as far as
we know, it is 10 in every other Common Lisp.  Our concern is that one
could certify a book in an MCL-based ACL2 with the theorem

     (equal (char-code #Newline) 13)

and then include this book in another Lisp and thereby prove nil.  So,
when a book is certified in an MCL-based ACL2, the book's certificate
mentions "MCL" in its version string.  Moreover, (@ acl2-version)
similarly mentions "MCL" when the ACL2 image has been built on top of
MCL.  Thus, an attempt to include a book in an MCL-based ACL2 that was
certified in a non-MCL-based ACL2, or vice-versa, will be treated like
an attempt to include an uncertified book.

_Incremental releases._

From time to time, so-called "incremental releases" of ACL2 are made
available.  These releases are thoroughly tested on at least two
platforms; "normal" releases, on the other hand, are thoroughly tested
on many more platforms (perhaps a dozen or so) and are accompanied by
updates to the ACL2 home page.  We provide incremental releases in
order to provide timely updates for ACL2 users who want them, without
imposing unnecessary burdens on either on the ACL2 implementors or on
ACL2 users who prefer to update less frequently.  The implementors
expect users to update their copies of ACL2 when normal releases are
made available, but not necessarily when incremental releases are made
available.

Incremental releases are accompanied by a bump in the incrl field of the
version field, while normal releases are accompanied by a bump in the
minor or (much less frequently) major field and zeroing out of the
incrl field.

Note that LOGICALLY SPEAKING, INCREMENTAL RELEASES ARE FULL-FLEDGE
RELEASES.  However, ACL2 users may wish to experiment with incremental
releases without recertifying all of their existing ACL2 books (see
CERTIFY-BOOK).  In order to learn how to avoid such
recertification, see SET-TAINTED-OKP.  The basic idea is that
if certification may depend on including books from an ACL2 version
with a different incrl field, the book's certificate is marked with a
"tainted" version, i.e., a version with "(tainted" as a substring.
Subsequent inclusion of any such book is restricted to sessions in
which the user explicitly invokes (set-tainted-okp t), which is
intended as an acknowledgment that including such a book may render the
ACL2 session unsound.

WATERFALL    See HINTS-AND-THE-WATERFALL.

WHY-BRR    an explanation of why ACL2 has an explicit brr mode

Why isn't brr mode automatically disabled when there are no monitored
runes?  The reason is that the list of monitored runes is kept in a
wormhole state.

See WORMHOLE for more information on wormholes in general.  But
the fundamental property of the wormhole function is that it is a
logical no-op, a constant function that does not take state as an
argument.  When entering a wormhole, arbitrary information can be
passed in (including the external state).  That information is used to
construct a near copy of the external state and that "wormhole state"
is the one with respect to which interactions occur during breaks.  But
no information is carried by ACL2 out of a wormhole -- if that were
allowed wormholes would not be logical no-ops.  The only information
carried out of a wormhole is in the user's head.

Break-rewrite interacts with the user in a wormhole state because the
signature of the ACL2 rewrite function does not permit it to modify
state.  Hence, only wormhole interaction is possible.  (This has the
additional desirable property that the correctness of the rewriter does
not depend on what the user does during interactive breaks within it;
indeed, it is logically impossible for the user to affect the course of
rewrite.)

Now consider the list of monitored runes.  Is that kept in the external
state as a normal state global or is it kept in the wormhole state?  If
it is in the external state then it can be inspected within the
wormhole but not changed.  This is unacceptable; it is common to change
the monitored rules as the proof attempt progresses, installing
monitors when certain rules are about to be used in certain contexts.
Thus, the list of monitored runes must be kept as a wormhole variable.
Hence, its value cannot be determined outside the wormhole, where the
proof attempt is ongoing.

This raises another question: If the list of monitored runes is unknown
to the rewriter operating on the external state, how does the rewriter
know when to break?  The answer is simple: it breaks every time, for
every rune, if brr mode is enabled.  The wormhole is entered
(silently), computations are done within the wormhole state to
determine if the user wants to see the break, and if so, interactions
begin.  For unmonitored runes and runes with false break conditions,
the silent wormhole entry is followed by a silent wormhole exit and the
user perceives no break.

Thus, the penalty for running with brr mode enabled when there are no
monitored runes is high: a wormhole is entered on every application of
every rune and the user is simply unware of it.  The user who has
finally unmonitored all runes is therefore strongly advised to carry
this information out of the wormhole and to do :brr nil in the external
state when the next opportunity arises.

WORLD    ACL2 property lists and the ACL2 logical data base

A "world" is a list of triples, each of the form (sym prop . val),
implementing the ACL2 notion of property lists.  ACL2 permits the
simultaneous existence of many property list worlds.  "The world" is
often used as a shorthand for "the ACL2 logical world" which is the
particular property list world used within the ACL2 system to maintain
the data base of rules.

Common Lisp provides the notion of "property lists" by which one can
attach "properties" and their corresponding "values" to symbols.  For
example, one can arrange for the 'color property of the symbol 'box-14
to be 'purple and the 'color property of the symbol 'triangle-7 to be
'yellow.  Access to property lists is given via the Common Lisp
function get.  Thus, (get 'box-14 'color) might return 'purple.
Property lists can be changed via the special form setf.  Thus, (setf
(get 'box-14 'color) 'blue) changes the Common Lisp property list
configuration so that (get 'box-14 'color) returns 'blue.  It should be
obvious that ACL2 cannot provide this facility, because Common Lisp's
get "function" is not a function of its argument, but instead a
function of some implicit state object representing the property list
settings for all symbols.

ACL2 provides the functions getprop and putprop which allow one to
mimic the Common Lisp property list facility.  However, ACL2's getprop
takes as one of its arguments a list that is a direct encoding of what
was above called the "state object representing the property list
settings for all symbols."  Because ACL2 already has a notion of
"state" that is quite distinct from that used here, we call this
property list object a "world."  A world is just a true list of
triples.  Each triple is of the form (sym prop . val).  This world can
be thought of as a slightly elaborated form of association list and
getprop is a slightly elaborated form of assoc that takes two keys.
When getprop is called on a symbol, s, property p, and world, w, it
scans w for the first triple whose sym is s and prop is p and returns
the corresponding val. Getprop has two additional arguments, one of
which that controls what it returns if no such sym and prop exist in w,
and other other of which allows an extremely efficient implementation.
To set some property's value for some symbol, ACL2 provides putprop.
(putprop sym prop val w) merely returns a new world, w', in which (sym
prop . val) has been consed onto the front of w, thus "overwriting" the
prop value of sym in w to val and leaving all other properties in w
unchanged.

One aspect of ACL2's property list arrangment is that it is possible to
have many different property list worlds.  For example, 'box-14 can
have 'color 'purple in one world and can have 'color 'yes in another,
and these two worlds can exist simultaneously because getprop is
explicitly provided the world from which the property value is to be
extracted.

The efficiency alluded to above stems from the fact that Common Lisp
provides property lists.  Using Common Lisp's provisions behind the
scenes, ACL2 can "install" the properties of a given world into the
Common Lisp property list state so as to make retrieval via getprop
very fast in the special case that the world provided to getprop has
been installed.  To permit more than one installed world, each of which
is permitted to be changed via putprop, ACL2 requires that worlds be
named and these names are used to distinquish installed versions of the
various worlds.  At the moment we do not further document getprop and
putprop.

However, the ACL2 system uses a property list world, named
'current-acl2-world, in which to store the succession of user commands
and their effects on the logic.  This world is often referred to in our
documentation as "the world" though it should be stressed that the user
is permitted to have worlds and ACL2's is in no way distinguished
except that the user is not permitted to modify it except via event
commands.  The ACL2 world is part of the ACL2 state and may be obtained
via (w state).

*Warning*: The ACL2 world is very large.  Its length as of this writing
(Version  2.5) is over 40,000 and it grows with each release.
Furthermore, some of the values stored in it are pointers to old
versions of itself.  Printing (w state) is something you should avoid
because you likely will not have the patience to await its completion.
For these practical reasons, the only thing you should do with (w
state) is provide it to getprop, as in the form

       (getprop sym prop default 'current-acl2-world (w state))

to inspect properties within it, or to pass it to ACL2 primitives, such
as theory functions, where it is expected.

Some ACL2 command forms, such as theory expressions (see
THEORIES) and the values to be stored in tables (see TABLE),
are permitted to use the variable symbol world freely with the
understanding that when these forms are evaluated that variable is
bound to (w state).  Theoretically, this gives those forms complete
knowledge of the current logical configuration of ACL2.  However, at
the moment, few world scanning functions have been documented for the
ACL2 user.  Instead, supposedly convenient macro forms have been
created and documented.  For example, (current-theory :here), which is
the theory expression which returns the currently enabled theory,
actually macroexpands to (current-theory-fn :here world).  When
evaluated with world bound to (w state), current-theory-fn scans the
current ACL2 world and computes the set of runes currently enabled in
it.

WORMHOLE    ld without state -- a short-cut to a parallel universe

     Example Form:
     (wormhole t 'interactive-break nil '(value 'hi!))
                                  ; Enters a recursive read-eval-print loop
                                  ; on a copy of the ``current state'' and
                                  ; returns nil!

     General Form:
     (wormhole pseudo-flg name input form
       :current-package    ...  ; known package name
       :ld-skip-proofsp    ...  ; t, nil or 'include-book
       :ld-redefinition-action  ; nil or '(:a . :b)
       :ld-prompt          ...  ; nil, t, or some prompt printer fn
       :ld-keyword-aliases ...  ; an alist pairing keywords to parse info
       :ld-pre-eval-filter ...  ; :all, :query, or some new name
       :ld-pre-eval-print  ...  ; nil, t, or :never
       :ld-post-eval-print ...  ; nil, t, or :command-conventions
       :ld-evisc-tuple     ...  ; nil or '(alist level length hiding-cars)
       :ld-error-triples   ...  ; nil or t
       :ld-error-action    ...  ; :continue, :return, or :error
       :ld-query-control-alist  ; alist supplying default responses
       :ld-verbose         ...) ; nil or t

The keyword arguments above are exactly those of ld (see LD)
except that three of ld's keyword arguments are missing: the three that
specify the channels standard-oi, standard-co and proofs-co.
Essentially wormhole is just a call of ld on the current state with the
given keyword arguments.  Wormhole always returns nil.  The *amazing*
thing about wormhole is that it calls ld and interacts with the user
even though state is not available as an argument!

Wormhole does this by manufacturing a "wormhole state," a copy of the
"current state" (whatever that is) modified so as to contain some of
the wormhole arguments.  Ld is called on that wormhole state with the
three ld channels directed to ACL2's "comment window." At the moment,
the comment window is overlaid on the terminal and you cannot tell when
output is going to *standard-co* and when it is going to the comment
window.  But we imagine that eventually a different window will pop up
on your screen.  In any case, the interaction provided by this call of
ld does not modify the state "from which" wormhole was called, it
modifies the copied state.  When ld exits (e.g., in response to :q
being typed in the comment window) the wormhole state evaporates and
wormhole returns nil.  Logically and actually (from the perspective of
the ongoing computation) nothing has happened except that a "no-op"
function was called and returned nil.

The name wormhole is meant to suggest the idea that the function
provides easy access to state in situations where it is apparently
impossible to get state.  Thus, for example, if you define the
factorial function, say, except that you sprinkled into its body
appropriate calls of wormhole, then the execution of (factorial 6)
would cause interactive breaks in the comment window.  During those
breaks you would apparently be able to inspect the "current state" even
though factorial does not take state as an argument.  The whole notion
of there being a "current state" during the evaluation of (factorial 6)
is logically ill-defined.  And yet, we know from practical experience
with the sequential computing machines upon which ACL2 is implemented
that there is a "current state" (to which the factorial function is
entirely insensitive) and that is the state to which wormhole
"tunnels." A call of wormhole from within factorial can pass
factorial-specific information that is embedded in the wormhole state
and made available for inspection by the user in an interactive
setting.  But no information ever flows out of a wormhole state:
wormhole always returns nil.

There are some restrictions about what can be done inside a wormhole.
As you may imagine, we really do not "copy the current state" but
rather just keep track of how we modified it and undo those
modifications upon exit.  An error is signalled if you try to modify
state in an unsupported way.  For this same reason, wormholes do not
allow updating of any user-defined single-threaded objects.  See
STOBJ.

There are four arguments to wormhole that need further explanation:
pseudo-flg, name, input, and form.  Roughly speaking, the value of
pseudo-flg should be t or nil and indicates whether we are actually to
enter a wormhole or just return nil immediately.  The actual handling
of pseudo-flg is more sophisticated and is explained in detail at the
end of this documentation.

Name and input are used as follows.  Recall that wormhole copies the
"current state" and then modifies it slightly to obtain the state upon
which ld is called.  We now describe the modifications.  First, the
state global variable 'wormhole-name is set to name, which may be any
non-nil ACL2 object but is usually a symbol.  Then, 'wormhole-input is
set to input, which may be any ACL2 object.  Finally, and inexplicably,
'wormhole-output is set to the value of 'wormhole-output the last time
a wormhole named name was exited (or nil if this is the first time a
wormhole named name was entered).  This last aspect of wormholes,
namely the preservation of 'wormhole-output, allows all the wormholes
of a given name to communicate with each other.

We can now explain how form is used.  The modified state described
above is the state on which ld is called.  However, standard-oi -- the
input channel from which ld reads commands -- is set so that the first
command that ld reads and evaluates is form.  If form returns an error
triple with value :q, i.e., form returns via (value :q), then no
further commands are read, ld exits, and the wormhole exits and returns
nil.  But if form returns any other value (or is not an error triple),
then subsequent commands are read from the comment window.

As usual, the ld-specials affect whether a herald is printed upon
entry, whether form is printed before evaluation, whether a prompt is
printed, how errors are handled, etc.  The ld-specials can be specified
with the corresponding arguments to wormhole.  It is standard practice
to call wormhole so that the entry to ld and the evaluation of form are
totally silent.  Then, tests in form can inspect the state and decide
whether user interaction is desired.  If so, form can appropriately set
ld-prompt, ld-error-action, etc., print a herald, and then return
(value :invisible).  Recall (see LD) that (value :invisible)
causes ld not to print a value for the just executed form.  The result
of this arrangement is that whether interaction occurs can be based on
tests that are performed on the wormhole state after (@ wormhole-input)
and the last (@ wormhole-output) are available for inspection.  This is
important because outside the wormhole you can access wormhole-input
(you are passing it into the wormhole) but you may not be able to
access the current state (because you might be in factorial) and you
definitely cannot access the wormhole-output of the last wormhole
because it is not part of the ACL2 state.  Thus, if the condition under
which you wish to interact depends upon the state or that part of it
preserved from the last wormhole interaction, that condition can only
be tested from within the wormhole, via form.

It is via this mechanism that break-rewrite (see BREAK-REWRITE)
is implemented.  To be more precise, the list of monitored runes is
maintained as part of the preserved wormhole-output of the
break-rewrite wormhole.  Because it is not part of the normal state, it
may be changed by the user during proofs.  That is what allows you to
install new monitors while debugging proofs.  But that means that the
list of monitored runes cannot be inspected from outside the wormhole.
Therefore, to decide whether a break is to occur when a given rule is
applied, the rewriter must enter the break-rewrite wormhole, supplying
a form that causes interaction if the given rule's break condition is
satisfied.  The user perceives this as though the wormhole was
conditionally entered -- a perception that is happily at odds with the
informed user's knowledge that the list of monitored runes is not part
of the state.  In fact, the wormhole was unconditionally entered and
the condition was checked from within the wormhole, that being the only
state in which the condition is known.

Another illustrative example is available in the implemention of the
monitor command.  How can we add a new rune to the list of monitored
runes while in the normal ACL2 state (i.e., while not in a wormhole)?
The answer is: by getting into a wormhole.  In particular, when you
type (monitor rune expr) at the top-level of ACL2, monitor enters the
break-rewrite wormhole with a cleverly designed first form.  That form
adds rune and expr to the list of monitored runes -- said list only
being available in break-rewrite wormhole states.  Then the first form
returns (value :q), which causes us to exit the wormhole.  By using
ld-specials that completely suppress all output during the process, it
does not appear to the user that a wormhole was entered.  The moral
here is rather subtle: the first form supplied to wormhole may be the
entire computation you want to perform in the wormhole; it need not
just be a predicate that decides if interaction is to occur.  Using
wormholes of different names you can maintain a variety of "hidden"
data structures that are always accessible (whether passed in or not).
This appears to violate completely the applicative semantics of ACL2,
but it does not: because these data structures are only accessible via
wormholes, it is impossible for them to affect any ACL2 computation
(except in the comment window).

As one might imagine, there is some overhead associated with entering a
wormhole because of the need to copy the current state.  This brings us
back to pseudo-flg.  Ostensibly, wormhole is a function and hence all
of its argument expressions are evaluated outside the function (and
hence, outside the wormhole it creates) and then their values are
passed into the function where an appropriate wormhole is created.  In
fact, wormhole is a macro that permits the pseudo-flg expression to
peer dimly into the wormhole that will be created before it is created.
In particular, pseudo-flg allows the user to access the
wormhole-output that will be used to create the wormhole state.

This is done by allowing the user to mention the (apparently unbound)
variable wormhole-output in the first argument to wormhole.  Logically,
wormhole is a macro that wraps

     (let ((wormhole-output nil)) ...)

around the expression supplied as its first argument.  So logically,
wormhole-output is always nil when the expression is evaluated.
However, actually, wormhole-output is bound to the value of (@
wormhole-output) on the last exit from a wormhole of the given name (or
nil if this is the first entrance).  Thus, the pseudo-flg expression,
while having to handle the possibility that wormhole-output is nil,
will sometimes see non-nil values.  The next question is, of course,
"But how can you get away with saying that logically wormhole-output is
always nil but actually it is not?  That doesn't appear to be sound."
But it is sound because whether pseudo-flg evaluates to nil or non-nil
doesn't matter, since in either case wormhole returns nil.  To make
that point slightly more formal, imagine that wormhole did not take
pseudo-flg as an argument.  Then it could be implemented by writing

     (if pseudo-flg (wormhole name input form ...) nil).

Now since wormhole always returns nil, this expression is equivalent to
(if pseudo-flg nil nil) and we see that the value of pseudo-flg is
irrelevant.  So we could in fact allow the user to access arbitrary
information to decide which branch of this if to take.  We allow access
to wormhole-output because it is often all that is needed.  We don't
allow access to state (unless state is available at the level of the
wormhole call) for technical reasons having to do with the difficulty
of overcoming translate's prohibition of the sudden appearance of the
variable state.

We conclude with an example of the use of pseudo-flg.  This example is
a simplification of our implementation of break-rewrite.  To enter
break-rewrite at the beginning of the attempted application of a rule,
rule, we use

     (wormhole
      (and (f-get-global 'brr-mode state)
           (member-equal (access rewrite-rule rule :rune)
                         (cdr (assoc-eq 'monitored-runes wormhole-output))))
      'break-rewrite
      ...)

The function in which this call of wormhole occurs has state as a
formal.  The pseudo-flg expression can therefore refer to state to
determine whether 'brr-mode is set.  But the pseudo-flg expression
above mentions the variable wormhole-output; this variable is not bound
in the context of the call of wormhole; if wormhole were a simple
function symbol, this expression would be illegal because it mentions a
free variable.

However, it is useful to think of wormhole as a simple function that
evaluates all of its arguments but to also imagine that somehow
wormhole-output is magically bound around the first argument so that
wormhole-output is the output of the last break-rewrite wormhole.  If
we so imagine, then the pseudo-flg expression above evaluates either to
nil or non-nil and we will enter the wormhole named break-rewrite in
the latter case.

Now what does the pseudo-flg expression above actually test?  We know
the format of our own wormhole-output because we are responsible for
maintaining it.  In particular, we know that the list of monitored
runes can be obtained via

     (cdr (assoc-eq 'monitored-runes wormhole-output)).

Using that knowledge we can design a pseudo-flg expression which tests
whether (a) we are in brr-mode and (b) the rune of the current rule is
a member of the monitored runes.  Question (a) is answered by looking
into the current state.  Question (b) is answered by looking into that
part of the about-to-be-created wormhole state that will differ from
the current state.  To reiterate the reason we can make wormhole-output
available here even though it is not in the current state: logically
speaking the value of wormhole-output is irrelevant because it is only
used to choose between two identical alternatives.  This example also
makes it clear that pseudo-flg provides no additional functionality.
The test made in the pseudo-flg expression could be moved into the
first form evaluated by the wormhole -- changing the free variable
wormhole-output to (@ wormhole-output) and arranging for the first form
to return (value :q) when the pseudo-flg expression returns nil.  The
only reason we provide the pseudo-flg feature is because it allows the
test to be carried out without the overhead of entering the wormhole.

Wormholes can be used not only in :program mode definitions but also in
:logic mode definitions.  Thus, it is possible (though somewhat
cumbersome without investing in macro support) to annotate logical
functions with output facilities that do not require state.  These
facilities do not complicate proof obligations.  Suppose then that one
doctored a simple function, e.g., APP, so as to do some printing and
then proved that APP is associative.  The proof may generate extraneous
output due to the doctoring.  Furthermore, contrary to the theorem
proved, execution of the function appears to affect *standard-co*.  To
see what the function "really" does when evaluated, enter raw lisp and
set the global variable *inhibit-wormhole-activityp* to t.

WORMHOLE-P    predicate to determine if you are inside a wormhole

See WORMHOLE for a discussion of wormholes.  (Wormhole-p state)
returns (mv nil t state) when evaluated inside a wormhole, else (mv nil
nil state).

XARGS    giving hints to defun

Common Lisp's defun function does not easily allow one to pass extra
arguments such as "hints".  ACL2 therefore supports a peculiar new
declaration (see DECLARE) designed explicitly for passing
additional arguments to defun via a keyword-like syntax.

The following declaration is nonsensical but does illustrate all of the
xargs keywords (which are the members of the list *xargs-keywords*).

     (declare (xargs :guard (symbolp x)
                     :guard-hints (("Goal" :in-theory (theory batch1)))
                     :guard-debug t
                     :hints (("Goal" :in-theory (theory batch1)))
                     :measure (- i j)
                     :ruler-extenders :basic
                     :mode :logic
                     :non-executable t
                     :normalize nil
                     :otf-flg t
                     :stobjs ($s)
                     :verify-guards t
                     :well-founded-relation my-wfr))

     General Form:
     (xargs :key1 val1 ... :keyn valn)

where the keywords and their respective values are as shown below.
Note that once "inside" the xargs form, the "extra arguments" to defun
are passed exactly as though they were keyword arguments.

:GUARD
Value is a term involving only the formals of the function being
defined.  The actual guard used for the definition is the conjunction
of all the guards and types (see DECLARE) declared.

:GUARD-HINTS
Value:  hints (see HINTS), to be used during the guard
verification proofs as opposed to the termination proofs of the defun.

:GUARD-DEBUG
Value:  nil by default, else directs ACL2 to decorate each guard proof
obligation with hypotheses indicating its sources.  See
GUARD-DEBUG.

:HINTS
Value:  hints (see HINTS), to be used during the termination
proofs as opposed to the guard verification proofs of the defun.

:MEASURE
Value is a term involving only the formals of the function being
defined.  This term is indicates what is getting smaller in the
recursion.  The well-founded relation with which successive measures
are compared is o<.  Also allowed is a special case, (:? v1 ... vk),
where (v1 ... vk) enumerates a subset of the formal parameters such
that some valid measure involves only those formal parameters.
However, this special case is only allowed for definitions that are
redundant (see REDUNDANT-EVENTS) or are executed when skipping
proofs (see SKIP-PROOFS).

:RULER-EXTENDERS
For recursive definitions (possibly mutually recursive), value controls
termination analysis and the resulting stored induction scheme.  See
RULER-EXTENDERS for a discussion of legal values and their
effects.

:MODE
Value is :program or :logic, indicating the defun mode of the function
introduced.  See DEFUN-MODE.  If unspecified, the defun mode
defaults to the default defun mode of the current world.  To convert a
function from :program mode to :logic mode, see
VERIFY-TERMINATION.

:NON-EXECUTABLE
Value is t or nil (the default).  If t, the function has no executable
counterpart and is permitted to use single-threaded object names and
functions arbitrarily, as in theorems rather than as in executable
definitions.  Such functions are not permitted to declare any names to
be :stobjs but accessors, etc., may be used, just as in theorems.
Since the default is nil, the value supplied is only of interest when it
is t.

:NORMALIZE
Value is a flag telling defun whether to propagate if tests upward.
Since the default is to do so, the value supplied is only of interest
when it is nil.  (See DEFUN).

:OTF-FLG
Value is a flag indicating "onward through the fog" (see
OTF-FLG).

:STOBJS
Value is either a single stobj name or a true list of stobj names (see
STOBJ and see DEFSTOBJ).  Every stobj name among the
formals of the function must be listed, if the corresponding actual is
to be treated as a stobj.  That is, if a function uses a stobj name as
a formal parameter but the name is not declared among the :stobjs then
the corresponding argument is treated as ordinary.  The only exception
to this rule is state: whether you include it or not, state is always
treated as a single-threaded object.  This declaration has two effects.
One is to enforce the syntactic restrictions on single-threaded
objects.  The other is to strengthen the guard of the function being
defined so that it includes conjuncts specifying that each declared
single-threaded object argument satisfies the recognizer for the
corresponding single-threaded object.

:VERIFY-GUARDS
Value is t or nil, indicating whether or not guards are to be verified
upon completion of the termination proof.  This flag should only be t
if the :mode is unspecified but the default defun mode is :logic, or
else the :mode is :logic.

:WELL-FOUNDED-RELATION
Value is a function symbol that is known to be a well-founded relation
in the sense that a rule of class :well-founded-relation has been
proved about it.  See WELL-FOUNDED-RELATION.

OTHER    other commonly used top-level functions

Related topics other than immediate subtopics:

This section contains an assortment of top-level functions that fit
into none of the other categories and yet are suffiently useful as to
merit "advertisement" in the :help command.

@    get the value of a global variable in state

     Examples:
     (+ (@ y) 1)
     (assign a (aset1 'ascii-map-array (@ a) 66 'Upper-case-B))

     General Form:
     (@ symbol)

where symbol is any symbol to which you have assigned a global value.
This macro expands into (f-get-global 'symbol state), which retrieves
the stored value of the symbol.

The macro assign makes it convenient to set the value of a symbol.  The
:ubt operation has no effect on the global-table of state.  Thus, you
may use these globals to hang onto useful data structures even though
you may undo back past where you computed and saved them.

ACCUMULATED-PERSISTENCE    to get statistics on which runes are being tried

     Useful Forms:
     (accumulated-persistence t)              ; Activate statistics gathering.

     (show-accumulated-persistence :frames)   ; Display statistics ordered by
     (show-accumulated-persistence :tries)    ; frames built, times tried,
     (show-accumulated-persistence :ratio)    ; or their ratio.

     (accumulated-persistence nil)            ; Deactivate.

     Advanced forms:
     (show-accumulated-persistence :frames-s) ; The `s', `f', and `a' suffices
     (show-accumulated-persistence :frames-f) ; stand for `success' (`useful'),
     (show-accumulated-persistence :frames-a) ; `failure' (`useless'), and `all',
     (show-accumulated-persistence :tries-s)  ; respectively.  The only effect of
     (show-accumulated-persistence :tries-f)  ; the `s' and `f' versions is to
     (show-accumulated-persistence :tries-a)  ; sort first by useful or useless
                                              ; applications, respectively (see
                                              ; below).  The `a' versions avoid
                                              ; showing the useful/useless
                                              ; breakdown.

Related topics other than immediate subtopics:

Generally speaking, the more ACL2 knows, the slower it runs.  That is
because the search space grows with the number of alternative rules.
Often, the system tries to apply rules that you have forgotten were
even there, if you knew about them in the first place!
"Accumulated-persistence" is a statistic (originally developed for
Nqthm) that helps you identify the rules that are causing ACL2's search
space to explode.

For other proof debugging utilities, see BREAK-REWRITE and see
DMR.

Accumulated persistence tracking can be turned on or off.  It is
generally off.  When on, proofs may take perhaps 50% more time than
otherwise!  But some useful numbers are collected.  When it is turned
on, by

     ACL2 !>(accumulated-persistence t)

an accumulation site is initialized and henceforth data about which
rules are being tried is accumulated into that site.  That accumulated
data can be displayed with show-accumulated-persistence, as described
in detail below.  When accumulated persistence is turned off, with
(accumulated-persistence nil), the accumulation site is wiped out and
the data in it is lost.

The "accumulated persistence" of a rune is the number of runes the
system has attempted to apply (since accumulated persistence was last
activated) while the given rune was being tried.

Consider a :rewrite rule named rune.  For simplicity, let us imagine
that rune is tried only once in the period during which accumulated
persistence is being monitored.  Recall that to apply a rewrite rule we
must match the left-hand side of the conclusion to some term we are
trying to rewrite, establish the hypotheses of rune by rewriting, and,
if successful, then rewrite the right-hand side of the conclusion.  We
say rune is "being tried" from the time we have matched its left-hand
side to the time we have either abandoned the attempt or finished
rewriting its right-hand side.  (By "match" we mean to include any
loop-stopper requirement; see LOOP-STOPPER.)  During that
period of time other rules might be tried, e.g., to establish the
hypotheses.  The rules tried while rune is being tried are "billed" to
rune in the sense that they are being considered here only because of
the demands of rune.  Thus, if no other rules are tried during that
period, the accumulated persistence of rune is 1 -- we "bill" rune once
for its own application attempt.  If, on the other hand, we tried 10
rules on behalf of that application of rune, then rune's accumulated
persistence would be 11.

One way to envision accumulated persistence is to imagine that every
time a rune is tried it is pushed onto a stack.  The rules tried on
behalf of a given application of a rune are thus pushed and popped on
the stack above that rune.  A lot of work might be done on its behalf
-- the stack above the rune grows and shrinks repeatedly as the search
continues for a way to use the rune.  All the while, the rune itself
"persists" in the stack, until we finish with the attempt to apply it,
at which time we pop it off.  The accumulated persistence of a rune
application is thus the number of stack frames built while that rune
was on the stack.

Note that accumulated persistence is tallied whether or not the attempt
to apply a rune is successful.  Each of the rules tried on its behalf
might have failed and the attempt to apply the rune might have also
failed.  The ACL2 proof script would make no mention of the rune or the
rules tried on its behalf because they did not contribute to the proof.
But time was spent pursuing the possible application of the rune and
accumulated persistence is a measure of that time.

A high accumulated persistence might come about in two extreme ways.
One is that the rule causes a great deal of work every time it is
tried.  The other is that the rule is "cheap" but is tried very often.
We therefore keep track of the number of times each rule is tried as
well as its persistence.  The ratio between the two is the average
amount of work done on behalf of the rule each time it is tried.

When the accumulated persistence totals are displayed by the function
show-accumulated-persistence we sort them so that the most expensive
runes are shown first.  We can sort according to one of three basic
keys:

     :frames - the number of frames built on behalf of the rune
     :tries  - the number of times the rune was tried
     :ratio  - frames built per try

The key simply determines the order in which the information is
presented.  If no argument is supplied to show-accumulated-persistence,
:frames is used.

The display breaks each total into "useful" and "useless" subtotals.  A
"useful" rule try is one that is viewed as contributing to the progress
of the proof, and the rest are "useless" rule applications.  For
example, if a :rewrite rule is tried but its hypotheses are not
successfully relieved, then that rule application and all work done on
behalf of those hypotheses is "useless" work.  In general, an attempt
to apply a rune is viewed as "useful" unless the attempt fails or the
attempt is on the stack (as described above) for a rune application
that ultimately fails.  A large number of "useless" :frames or :tries
along with correspondingly small "useful" counts may suggest runes to
consider disabling (see DISABLE and see IN-THEORY).
Thus, here is a more complete list of the arguments that may be
supplied to show-accumulated-persistence, Suffices "s", "f", and "a" are
intended to suggest "success" ("useful"), "failure" ("useless"), and
"all".

     :frames     - sort by the number of frames built on behalf of the rune
        :frames-s -   as above, but sort by useful applications
        :frames-f -   as above, but sort by useless applications
        :frames-a -   as above, but inhibit display of ``useful'' and
                      ``useless'' subtotals
     :tries      - sort by the number of times the rune was tried
        :tries-s  -   as above, but sort by useful applications
        :tries-f  -   as above, but sort by useless applications
        :tries-a  -   as above, but inhibit display of ``useful'' and
                      ``useless'' subtotals
     :ratio      - sort by frames built per try
     :useless    - show only the runes tried whose tries were all ``useless''

For a given line of the report, every frame credited to a "useful"
(respectively, "useless") rule application is considered "useful"
(respectively, "useless").  We illustrate with the following example.

     (progn
       (defstub hyp (x) t)
       (defstub concl (x) t)
       (defstub bad (x) t)
       (defstub good (x) t)
       (defaxiom good-ax
         (implies (good x) (hyp x)))
       (defaxiom bad-ax
         (implies (bad x) (hyp x)))
       (defaxiom hyp-implies-concl
         (implies (hyp x) (concl x)))
       )
     (accumulated-persistence t)
     (thm (implies (good x) (concl x)))
     (show-accumulated-persistence)

To prove the thm form, ACL2 attempts to rewrite (concl x) to true by
applying rule hyp-implies-concl.  It then attempts to establish (hyp x)
first by trying rule bad-ax, which fails, and second by trying rule
good-ax, which succeeds.  As expected, the report labels as "useless"
the failure of the attempt to establish the hypothesis, (bad x).

        --------------------------------
              1        1 (    1.00) (:REWRITE BAD-AX)
              0        0    [useful]
              1        1    [useless]
        --------------------------------

Now consider the top-level application of rule hyp-implies-concl.  Even
though the above report shows the application of bad-ax as "useless",
note that this rule was applied on behalf of the successful ("useful")
application of hyp-implies-concl, and hence is incorporated into the
"useful" line for hyp-implies-concl, as follows.

        --------------------------------
              3        1 (    3.00) (:REWRITE HYP-IMPLIES-CONCL)
              3        1    [useful]
              0        0    [useless]
        --------------------------------

In summary: categorization of :frames as "useful" or "useless" is based
on whether they support "useful" or "useless" :tries.

Note that a rune with high accumulated persistence may not actually be
the "culprit."  For example, suppose rune1 is reported to have a :ratio
of 101, meaning that on the average a hundred and one frames were built
each time rune1 was tried.  Suppose rune2 has a :ratio of 100.  It
could be that the attempt to apply rune1 resulted in the attempted
application of rune2 and no other rune.  Thus, in some sense, rune1 is
"cheap" and rune2 is the "culprit" even though it costs less than rune1.

If a proof is aborted, then in general, show-accumulated-persistence
will only display totals for runes whose attempted application is
complete: that is, if the rewriter was in the process of relieving
hypotheses for a rule, then information for that rule will not be
included in the tally.  We say "in general" because, as indicated near
the top of the output from show-accumulated-persistence when such
incomplete information is omitted, you can get this information by
using argument :frames-a or :tries-a.

There are other subtleties in how rune applications are tallied,
documented elsewhere:  see ACCUMULATED-PERSISTENCE-SUBTLETIES.

Users are encouraged to think about other meters we could install in
ACL2 to help diagnose performance problems.

ACCUMULATED-PERSISTENCE-SUBTLETIES    some subtle aspects of the counting done by accumulated-persistence

In this topic we cover the overcounting of "useful" and of recursive
rune application attempts, and we describe how "useless" rune
application attempts can actually be critical for a proof's success.

_Overcounting of "useful" and of recursive rune application attempts._
Not every rune application may be necessary for a proof's success.
Consider for example:

     (thm (equal (car (cons a (cdr (cons b x))))
                 a))

Then show-accumulated-persistence will tell us that :rewrite rules
car-cons and cdr-cons each had one useful application.  However, the
rule cdr-cons is used to simplify (cdr (cons b x)) to x, and this
simplification is unecessary for the proof.  Indeed, the proof succeeds
even when preceded by the event: (in-theory (disable cdr-cons)).  We
thus see that a rune application labeled as "useful" may be simplifying
a term that is not relevant to the proof.

As of this writing, we consider every :forward-chaining rule
application to be "useful", for simplicity of the implementation.
Moreover, our counting of these rules is such that a single rule may be
counted more than once.

Next we show how recursive rule applications are overcounted.  Consider
the following example.

     (defun mem (a x)
       (if (atom x)
           nil
         (or (equal a (car x)) (mem a (cdr x)))))

Now suppose we consider the sequence of theorems (mem a (list a)), (mem
a (list 1 a)), (mem a (list 1 2 a)), (mem a (list 1 2 3 a)), and so on.
We will see that the :frames reported for each increases
quadratically, even though the :tries increases linearly; so in this
case the :tries statistics are more appropriate.  Each time the
definition of mem is applied, a new stack frame is pushed (see
ACCUMULATED-PERSISTENCE), and all subsequent applications of that
definition are accumulated into the :frames count for that stack frame.
The final :frames count will be the sum of the counts for those
individual frames, which form a linear sequence whose sum is therefore
quadratic in the number of applications of the definition of mem.

_How "useless" attempts can be critical for a proof's success._  The
command (accumulated-persistence :useless)] will list rules that did not
contribute directly to the proof (see ACCUMULATED-PERSISTENCE,
in particular the discussion of "useless" there).  However, a "useless"
rule can on rare occasions be critical to the success of a proof.  In
the following example, we have a "bad" rule that can take the proof in
the wrong direction, but a "useless" rule does a rewrite that prevents
the succesful relieving of a hypothesis of the "bad" rule.  In summary:

     ; Assume p0.  We want to prove p1.

     ; Key rule:
     p0 -> p1 = t

     ; Bad rule that could ruin the proof:
     p3 -> p1 = p2

     ; But unfortunately, we know p3:
     p0 -> p3

     ; Important ``useless'' rule, preventing ``bad rule'' above from firing:
     p3 = p4

The following event captures the rules described above.

     (encapsulate
      ((p0 (x) t)
       (p1 (x) t)
       (p2 (x) t)
       (p3 (x) t)
       (p4 (x) t))
      (local (defun p0 (x) x))
      (local (defun p1 (x) x))
      (local (defun p2 (x) x))
      (local (defun p3 (x) x))
      (local (defun p4 (x) x))

     ; Key rule:
      (defthm p0-implies-p1
        (implies (p0 x)
                 (p1 x)))

     ; Bad rule that could ruin the proof:
      (defthm p3-implies-p1-is-p2
        (implies (p3 x)
                 (equal (p1 x) (p2 x))))

     ; But unfortunately, we know p3:
      (defthm p0-implies-p3
        (implies (p0 x)
                 (p3 x)))

     ; Important ``useless'' rule, preventing p3-implies-p1-is-p2 from firing:
      (defthm p3-is-p4
        (equal (p3 x) (p4 x))))

Now we can see that p3-is-p4 is labeled as "useless", by evaluating
these commands.

     (accumulated-persistence t)
     (thm (implies (p0 x) (p1 x)))
     (show-accumulated-persistence)

If instead we first evaluate (in-theory (disable p3-is-p4)) before the
thm above, then the proof fails, even though p3-is-p4 was labeled as
"useless"!

Nevertheless, in general it is probably safe to disable rules reported
as "useless" by (show-accumulated-persistence :useless), and doing so
may speed up a proof considerably.

Remark. The example above suggests a surprising fact: on rare
occasions, a proof may fail when you give an :in-theory hint consisting
of exactly the runes reported in a proof that succeeds.  For, imagine a
rule R that is needed in part of the proof but is "bad" in a second
part, and that some other, "useless" rule prevents the application of R
in that second part.  The example above suggests that disabling this
"useless" rule can allow the second application of R, thus preventing
the proof.

ACL2-DEFAULTS-TABLE    a table specifying certain defaults, e.g., the default defun-mode

     Example Forms:
     (table acl2-defaults-table :defun-mode) ; current default defun-mode
     (table acl2-defaults-table :defun-mode :program)
                ; set default defun-mode to :program

See TABLE for a discussion of tables in general.  The legal
keys for this table are shown below.  They may be accessed and changed
via the general mechanisms provided by tables.  However, there are
often more convenient ways to access and/or change the defaults.  (See
also the note below.)

     :defun-mode

the default defun-mode, which must be :program or :logic.  See
DEFUN-MODE for a general discussion of defun-modes.  The :defun-mode
key may be conveniently set by keyword commands naming the new
defun-mode, :program and :logic.  See PROGRAM and see
LOGIC.

     :enforce-redundancy

if t, cause ACL2 to insist that most events are redundant (see
REDUNDANT-EVENTS); if :warn, cause a warning instead of an error for
such non-redundant events; else, nil.  See
SET-ENFORCE-REDUNDANCY.

     :ignore-doc-string-error

if t, cause ACL2 to ignore ill-formed documentation strings rather than
causing an erorr; if :warn, cause a warning instead of an error in such
cases; else, nil (the default).  See
SET-IGNORE-DOC-STRING-ERROR.

     :verify-guards-eagerness

an integer between 0 and 2 indicating how eager the system is to verify
the guards of a defun event.  See SET-VERIFY-GUARDS-EAGERNESS.

     :compile-fns

When this key's value is t, functions are compiled when they are
defun'd; otherwise, the value is nil.  (Except, this key's value is
ignored when explicit compilation is suppressed; see
COMPILATION.  To set the flag, see SET-COMPILE-FNS.

     :measure-function

the default measure function used by defun when no :measure is supplied
in xargs.  The default measure function must be a function symbol of
one argument. Let mfn be the default measure function and suppose no
:measure is supplied with some recursive function definition.  Then
defun finds the first formal, var, that is tested along every branch
and changed in each recursive call.  The system then "guesses" that
(mfn var) is the :measure for that defun.

     :well-founded-relation

the default well-founded relation used by defun when no
:well-founded-relation is supplied in xargs.  The default well-founded
relation must be a function symbol, rel, of two arguments about which a
:well-founded-relation rule has been proved.  See
WELL-FOUNDED-RELATION.

     :bogus-defun-hints-ok

When this key's value is t, ACL2 allows :hints for nonrecursive
function definitions.  Otherwise, the value is the nil (the default) or
:warn (which makes the check but merely warns when the check fails).
See SET-BOGUS-DEFUN-HINTS-OK.

     :bogus-mutual-recursion-ok

When this key's value is t, ACL2 skips the check that every function in
a mutual-recursion (or defuns) "clique" calls at least one other
function in that "clique."  Otherwise, the value is nil (the default)
or :warn (which makes the check but merely warns when the check fails).
See SET-BOGUS-MUTUAL-RECURSION-OK.

     :irrelevant-formals-ok

When this key's value is t, the check for irrelevant formals is
bypassed; otherwise, the value is the keyword nil (the default) or
:warn (which makes the check but merely warns when the check fails).
See IRRELEVANT-FORMALS and see
SET-IRRELEVANT-FORMALS-OK.

     :ignore-ok

When this key's value is t, the check for ignored variables is
bypassed; otherwise, the value is the keyword nil (the default) or
:warn (which makes the check but merely warns when the check fails).
See SET-IGNORE-OK.

     :inhibit-warnings

ACL2 prints warnings that may, from time to time, seem excessive to
experienced users.  Each warning is "labeled" with a string identifying
the type of warning.  Consider for example

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

Here, the label is "Use".  The value of the key :inhibit-warnings is a
list of such labels, where case is ignored.  Any warning whose label is
a member of this list (where again, case is ignored) is suppressed.
See SET-INHIBIT-WARNINGS and also see
SET-INHIBIT-OUTPUT-LST.

     :bdd-constructors

This key's value is a list of function symbols used to define the
notion of "BDD normal form."  See BDD-ALGORITHM and see
HINTS.

     :ttag

This key's value, when non-nil, allows certain operations that extend
the trusted code base beyond what is provided by ACL2.  See
DEFTTAG.  See DEFTTAG.

     :state-ok

This key's value is either t or nil and indicates whether the user is
aware of the syntactic restrictions on the variable symbol STATE.  See
SET-STATE-OK.

     :backchain-limit

This key's value is either nil or a non-negative integer.  It is used
to set the backchain limit upon starting rewriting.  See
BACKCHAIN-LIMIT.

     :default-backchain-limit

This key's value is either nil or a non-negative integer.  It is used
to set the backchain limit of a rule if one has not been specified.
See BACKCHAIN-LIMIT.

     :rewrite-stack-limit

This key's value is a nonnegative integer less than (expt 2 28).  It is
used to limit the depth of calls of ACL2 rewriter functions.  See
REWRITE-STACK-LIMIT.

     :let*-abstractionp

This key affects how the system displays subgoals.  The value is either
t or nil.  When t, let* expressions are introduced before printing to
eliminate common subexpressions.  The actual goal being worked on is
unchanged.

     :nu-rewriter-mode

This key's value is nil, t, or :literals.  When the value is non-nil,
the rewriter gives special treatment to expressions and functions
defined in terms of nth and update-nth.  See set-nu-rewriter-mode.

     :case-split-limitations

This key's value is a list of two "numbers."  Either "number" may
optionally be nil, which is treated like positive infinity.  The
numbers control how the system handles case splits in the simplifier.
See SET-CASE-SPLIT-LIMITATIONS.

     :include-book-dir-alist

This key's value is used by include-book's :DIR argument to associate a
directory with a keyword.  An exception is the keyword :SYSTEM for the
distributed ACL2 books/ directory; see INCLUDE-BOOK, in
particular the section on "Books Directory."

     :match-free-default

This key's value is either :all, :once, or nil.  See
SET-MATCH-FREE-DEFAULT.

     :match-free-override

This key's value is a list of runes.  See
ADD-MATCH-FREE-OVERRIDE.

     :match-free-override-nume

This key's value is an integer used in the implementation of
add-match-free-override, so that only existing runes are affected by
that event.

     :non-linearp

This key's value is either t or nil and indicates whether the user
wishes ACL2 to extend the linear arithmetic decision procedure to
include non-linear reasoning.  See NON-LINEAR-ARITHMETIC.

     :ruler-extenders

This key's value may be a list of symbols, indicating those function
symbols that are not to block the collection of rulers; see
DEFUN.  Otherwise the value is :all to indicate all function symbols,
i.e., so that no function symbol blocks the collection of rulers.  If a
list is specified (rather than :all), then it may contain the keyword
:lambdas, which has the special role of specifying all lambda
applications.  No other keyword is permitted in the list.  See
RULER-EXTENDERS.

Note: Unlike all other tables, acl2-defaults-table can affect the
soundness of the system.  The table mechanism therefore enforces on it
a restriction not imposed on other tables: when table is used to update
the acl2-defaults-table, the key and value must be variable-free forms.
Thus, while

     (table acl2-defaults-table :defun-mode :program),

     (table acl2-defaults-table :defun-mode ':program), and

     (table acl2-defaults-table :defun-mode (compute-mode *my-data*))

are all examples of legal events (assuming compute-mode is a function
of one non-state argument that produces a defun-mode as its single
value),

     (table acl2-defaults-table :defun-mode (compute-mode (w state)))

is not legal because the value form is state-sensitive.

Consider for example the following three events which one might make
into the text of a book.

     (in-package "ACL2")

     (table acl2-defaults-table
       :defun-mode
       (if (ld-skip-proofsp state) :logic :program))

     (defun crash-and-burn (x) (car x))

The second event is illegal because its value form is state-sensitive.
If it were not illegal, then it would set the :defun-mode to :program
when the book was being certified but would set the defun-mode to
:logic when the book was being loaded by include-book.  That is because
during certification, ld-skip-proofsp is nil (proof obligations are
generated and proved), but during book inclusion ld-skip-proofsp is
non-nil (those obligations are assumed to have been satisfied.)  Thus,
the above book, when loaded, would create a function in :logic mode that
does not actually meet the conditions for such status.

For similar reasons, table events affecting acl2-defaults-table are
illegal within the scope of local forms.  That is, the text

     (in-package "ACL2")

     (local (table acl2-defaults-table :defun-mode :program))

     (defun crash-and-burn (x) (car x))

is illegal because acl2-defaults-table is changed locally.  If this
text were acceptable as a book, then when the book was certified,
crash-and-burn would be processed in :program mode, but when the
certified book was included later, crash-and-burn would have :logic
mode because the local event would be skipped.

The text

     (in-package "ACL2")

     (program) ;which is (table acl2-defaults-table :defun-mode :program)

     (defun crash-and-burn (x) (car x))

is acceptable and defines crash-and-burn in :program mode, both during
certification and subsequent inclusion.

We conclude with an important observation about the relation between
acl2-defaults-table and include-book, certify-book, and encapsulate.
Including or certifying a book never has an effect on the
acl2-defaults-table, nor does executing an encapsulate event; we always
restore the value of this table as a final act.  (Also see
INCLUDE-BOOK, see ENCAPSULATE, and see CERTIFY-BOOK.)
That is, no matter how a book fiddles with the acl2-defaults-table,
its value immediately after including that book is the same as
immediately before including that book.  If you want to set the
acl2-defaults-table in a way that persists, you need to do so using
commands that are not inside books.  It may be useful to set your
favorite defaults in your acl2-customization file; see
ACL2-CUSTOMIZATION.

ACL2-HELP    the acl2-help mailing list

You can email questions about ACL2 usage to the acl2-help mailing list:
acl2-help@utlists.utexas.edu.  If you have more general questions about
ACL2, for example, about projects completed using ACL2, you may prefer
the acl2 mailing list, acl2@utlists.utexas.edu, which tends to have
wider distribution.

ASSIGN    assign to a global variable in state

     Examples:
     (assign x (expt 2 10))
     (assign a (aset1 'ascii-map-array (@ a) 66 'Upper-case-B))

     General Form:
     (assign symbol term)

where symbol is any symbol (with certain enforced exclusions to avoid
overwriting ACL2 system "globals") and term is any ACL2 term that could
be evaluated at the top-level.  Assign evaluates the term, stores the
result as the value of the given symbol in the global-table of state,
and returns the result.  (Note:  the actual implementation of the
storage of this value is much more efficient than this discussion of
the logic might suggest.)  Assign is a macro that effectively expands
to the more complicated but understandable:

     (pprogn (f-put-global 'symbol term state)
             (mv nil (f-get-global 'symbol term state) state)).

The macro @ gives convenient access to the value of such globals.  The
:ubt operation has no effect on the global-table of state.  Thus, you
may use these globals to hang onto useful data structures even though
you may undo back past where you computed and saved them.

BREAK$    cause an immediate Lisp break

ACL2 users are generally advised to avoid breaking into raw Lisp.
Advanced users may, on occasion, see the need to do so.  Evaluating
(break$) will have that effect.  (Exception: break$ is disabled after
evaluation of (set-debugger-enable :never); see
SET-DEBUGGER-ENABLE.)

CERTIFY-BOOK!    a variant of certify-book

     Examples:
     (certify-book! "my-arith" 3)     ;Certify in a world with 3
                                        ; commands, starting in a world
                                        ; with at least 3 commands.
     (certify-book! "my-arith")       ;Certify in the initial world.

     General Form:
     (certify-book! book-name k compile-flg)

where book-name is a book name (see BOOK-NAME), k is a
nonnegative integer used to indicate the "certification world," and
compile-flg indicates whether you wish to compile the (functions in
the) book.  As with certify-book, compile-flg is coerced to nil if
explicit compilation is suppressed; see COMPILATION.

This command is identical to certify-book, except that the second
argument k may not be t in certify-book! and if k exceeds the current
command number, then an appropriate ubt! will be executed first.  See
CERTIFY-BOOK and see UBT!.

CW-GSTACK    debug a rewriting loop or stack overflow

     General Forms:
     (cw-gstack)
     (cw-gstack :frames 10)       ; show only the top 10 frames
     (cw-gstack :frames (1 10))   ; same as above:  show only frames 1 through 10
     (cw-gstack :frames (10 20))  ; show only frames 10 through 20
     (cw-gstack :evisc-tuple nil) ; print using default ``evisceration''
     (cw-gstack :evisc-tuple x)   ; print with evisceration tuple x

For the last case above, see LD-EVISC-TUPLE.

Stack overflows may occur, perhaps caused by looping rewrite rules.  In
some Lisps, especially GCL, stack overflows often manifest themselves
as segmentation faults, causing the entire ACL2 image to crash.
Finding looping rewrite rules can be tricky, especially if you are
using books supplied by other people.  (However, see
SET-REWRITE-STACK-LIMIT for a way to avoid stack overflows caused by
rewriter loops.)

A wonderful trick is the following.  When there is a stack overflow
during a proof, abort and then try it again after turning on rewrite
stack monitoring with :brr t.  When the stack overflows again, exit to
raw Lisp.  How you exit to raw Lisp depends on which Lisp you are
using.  In Allegro Common Lisp, for example, the stack overflow will
leave you in an interactive break.  It is often a good idea to exit the
break immediately (e.g., using :pop if you use Allegro Common Lisp, or
:q using GCL), which will leave you in the top-level ACL2 command loop,
after which it is recommended to leave that loop using :q.  That will
leave you in raw Lisp.  Then, execute

     (cw-gstack)

If the loop is in the rewriter, it will probably be evident!  You can
re-enter the ACL2 loop now with (lp).

Note: By default, cw-gstack "eviscerates" terms, printing abbreviated
representations of large terms using print-level 3 and print-length 4;
see EVISC-TUPLE.  The user can control this behavior by using
(cw-gstack :evisc-tuple x), where x is nil or an evisceration tuple;
see LD-EVISC-TUPLE.  For example, (cw-gstack :evisc-tuple nil)
will avoid all evisceration, while the default behavior can be obtained
by using (cw-gstack :evisc-tuple '(nil 3 4 (hide))), meaning that
substructures deeper than 3 are replaced by "#" and those longer than 4
are replaced by "...", and terms of the form (hide ...) are printed as
<hidden>.  Also see SET-IPRINT for an alternative to printing
"#" and "...".

If you are in GCL the stack overflow may cause a segmentation fault and
abort the Lisp job.  This makes it harder to debug but here is what you
do.  First, re-create the situation just prior to submitting the form
that will cause the stack overflow.  You can do this without suffering
through all the proofs by using the :ld-skip-proofsp option of ld to
reload your scripts.  Before you submit the form that causes the stack
overflow, exit the ACL2 command loop with :q.  In raw GCL type:

     (si::use-fast-links nil)

This will slow GCL down but make it detect and signal stack overflows
rather than overwrite the system memory.  Now reenter the ACL2 command
loop with (lp).

Now carry on as described above, turning on rewrite stack monitoring
with :brr t and provoking the stack overflow.  When it occurs, you will
be in an interactive break.  Exit to raw Lisp with two successive :q's,
one to get out of the error break and the next to get out of the
top-level ACL2 command loop.  Then in raw GCL execute (cw-gstack).

Suggestion: Once you have found the loop and fixed it, you should
execute the ACL2 command :brr nil, so that you don't slow down
subsequent proof attempts.  If you are in GCL, you should also get into
raw Lisp and execute (si::use-fast-links t).

DMR    dynamically monitor rewrites and other prover activity

In addition to utilities that allow you to set breakpoints or print
rewriting information to the screen -- see BREAK-REWRITE --
ACL2 provides a utility for watching the activity of the rewriter and
some other proof processes, in real time.  This utility is called
"dmr", which is an acronym for "dynamically monitor rewrites".  The
utility comes in two parts: an ACL2 component that frequently writes a
file (the "dmr file") containing the relevant information, and an Emacs
component that frequently displays the contents of that file in an
Emacs buffer (the "dmr buffer").  Other editors could, in principle, be
programmed to display that file; anyone developing such a capability is
invited to contribute it to the ACL2 community.

The dmr utility can be extremely helpful for expensive proofs,
especially when ACL2 is not providing any output.  The break-rewrite and
accumulated-persistence utilities may be a bit easier to use, so you
might want to try those first.  But the dmr utility can be a very
helpful debugging aide, as it can visually give you a sense of where
ACL2 is spending its time.

The Emacs portion of this utility is already loaded if you load the
distributed Emacs file emacs/emacs-acl2.el.  Otherwise, invoke the
following Emacs command, say by typing Control-X Control-E after the
right parenthesis, where DIR is the directory of your ACL2 distribution.

     (load "<DIR>/emacs/monitor.el") ; absolute pathnames might work best

You only need to do that once.  Then each time you want to observe the
rewriter in action, invoke the following to see it displayed in a
buffer, which we call the "dmr buffer":

     Control-t 1

But first you will need to enable monitoring at the ACL2 level:

     (dmr-start)

Monitoring has some cost.  So if you have started it, then at some
point you may want to turn it off when not using it.  Any time the dmr
buffer (generally called "acl2-dmr-<user_name>") is not visible, Emacs
monitoring is turned off.  You can also turn off Emacs monitoring
explicitly, with:

     Control-t 2

At the ACL2 level you can disable monitoring as follows:

     (dmr-stop)

_Interpreting the dmr buffer display._

We explain the dmr buffer display by way of the following example.  It
is a snapshot of a dmr buffer taken from one of the distributed
workshop books,
books/workshops/2004/legato/support/proof-by-generalization-mult.lisp.

      0. (DEFTHM . WP-ZCOEF-G-MULTIPLIES)
      1. SIMPLIFY-CLAUSE
        2. Rewriting (to simplify) the atom of literal 18; argument(s) 1
        4. Rewriting (to simplify) the expansion; argument(s) 3|2
        7. Applying (:DEFINITION WP-ZCOEF-G)
     *  8. Rewriting (to simplify) the rewritten body; argument(s) 2|1|2|2
     *  13. Applying (:REWRITE MOD-ZERO . 2)
     *    14. Rewriting (to establish) the atom of hypothesis 4
     *    15. Applying (:META META-INTEGERP-CORRECT)

Each line indicates an ACL2 activity that leads to the activity shown
on the line just below it.  Moreover, lines are sometimes collapsed to
make the display more compact.  Consider for example the first few
lines.  Above, we are proving a theorem named WP-ZCOEF-G-MULTIPLIES.
Lines 1 and 2 show the clause simplification process invokes the
rewriter on the 18th literal.  (Recall that a clause is a disjunction
of literals; for example the clause {(NOT A), (NOT B), C} would be
displayed as (IMPLIES (AND A B) C).)  This 18th literal mentioned on
line 2 is a function call (f arg1 ...), and "argument(s) 1" indicates
that the rewriter, which works inside-out, is considering the first
argument ("arg1").  Thus the display could instead have shown the
following.

        2. Rewriting (to simplify) the atom of literal 18
        3. Rewriting (to simplify) the first argument
        4. Rewriting (to simplify) the expansion; argument(s) 3|2

But it saved space to combine lines 2 and 3.  Line 4 suggests that the
above arg1 is a function call that has been opened up because of an
:expand hint or, perhaps, an expansion directed explicitly by the
prover (as can happen during induction).  The annotation "argument(s)
3|2" then indicates that the rewriter is diving into the third argument
of the expansion, and then into the second argument of that.  Let us
call the result term7 (since it is the one to be considered on line 7).

Now consider the next two lines:

        7. Applying (:DEFINITION WP-ZCOEF-G)
     *  8. Rewriting (to simplify) the rewritten body; argument(s) 2|1|2|2

Line 7 is saying that term7 (defined above) is modified by applying the
definition of WP-ZCOEF-G to it.  Line 8 then says that the body of this
definition has been rewritten (with its formals bound to the actuals
from term7) and the rewriter is diving into the subterms of that
rewritten body, as indicated.  Notice also that line 8 is the first
line marked with an asterisk ("*") in the margin.  This line is the
first that is different from what was shown the previous time the
display was updated (about 1/10 second earlier, by default).  When a
line is marked with an asterisk, so are all the lines below it; so the
lines without an asterisk are those that have been stable since the
last display.  In this example we may see line 7 marked without an
asterisk for a while, which suggests that the rule (:DEFINITION
WP-ZCOEF-G) is expensive.  (Also see ACCUMULATED-PERSISTENCE.)
In general, a line that persists for awhile without a leading asterisk
can suggest why the proof is taking a long time.

Finally, note the indentation of line 14 relative to line 13.  Extra
indentation occurs when an attempt is being made to relieve a hypothesis
(i.e., rewrite it to t).  In particular, rewrites that will be
incorporated directly into a (top-level) literal are all indented just
two spaces, starting with the first rewrite directly under a process
such as SIMPLIFY-CLAUSE (shown line 1 above).  If the indentation is at
least the value of raw Lisp variable *dmr-indent-max* (by default, 20),
then indenttion is restricted to that column, but ACL2 prints {n} where
n is the column that would have been used for indentation if there were
no maximum.

You can move the cursor around in the dmr buffer even while it is being
updated.  But emacs will attempt to keep the cursor no later than the
first asterisk ("*") in the margin.  Thus, you can move the cursor
around in the stable part of the display, and emacs will keep the
cursor in that stable part.

WARNING: Things could go terribly wrong if the same user runs two
different ACL2 sessions with dmr active, because the same file will be
written by two different ACL2 processes.

WARNING: For dmr to work, emacs and ACL2 need to be run on the same
machine because the file used to communicate between ACL2 and emacs is
under /tmp.  Except, you can probably hack around that restriction by
changing *dmr-file-name* in ACL2 (in raw Lisp) and correspondingly in
Emacs file monitor.el.

More generally, advanced users are welcome to search for the string

     User-settable dmr variables

in ACL2 files interface-raw.lisp and emacs/monitor.el in order to
customize their dmr environments.

Finally, in order to update the dmr file with the latest stack
information, interrupt ACL2 and then evaluate: (dmr-flush).  In order
to support resumption of the interrupted proof (assuming your host
Common Lisp supports resumption), evaluation of (dmr-start)
automatically causes evaluation of the form (set-debugger-enable t);
see SET-DEBUGGER-ENABLE.

DYNAMICALLY-MONITOR-REWRITES    See DMR.

EXIT    quit entirely out of Lisp

Same as good-bye.

GOOD-BYE    quit entirely out of Lisp

     Examples:
     ACL2 !>(good-bye)
     ; [ACL2 is exited]

     ACL2 !>(good-bye 3)
     ; [ACL2 is exited with Unix exit status 3]

Note:  Your entire session will disappear forever when you evaluate
(good-bye).

The command (good-bye) quits not only out of the ACL2 command loop, but
in fact quits entirely out of the underlying Lisp.  Thus, there is no
going back!  You will *not* be able to re-enter the command loop after
typing (good-bye)!  All your work will be lost!!!

This command may not work in some underlying Common Lisp
implementations.  In such cases, there is no harm in trying; ACL2 will
let you know how to proceed if it cannot exit.

In some systems, typing control-d at the top-level ACL2 prompt
(control-c control-d if inside emacs) will call this function.

If you give good-bye an argument, it should be a natural number, and it
indicates the Unix (Linux) exit status.

If you merely want to exit the ACL2 command loop, use :q instead (see
Q).

GUARD-OBLIGATION    the guard proof obligation

See VERIFY-GUARDS, and see GUARD for a discussion of
guards.  Also see VERIFY-GUARDS-FORMULA for a utility provided
for viewing the guard proof obligation, without proof.
Guard-obligation is a lower level function for use in system programs,
not typically appropriate for most ACL2 users.  If you simply want to
see the guard proof obligations, see VERIFY-GUARDS-FORMULA.

     Example Form:
     (guard-obligation 'foo nil 'top-level state)
     (guard-obligation '(if (consp x) (foo (car x)) t) nil 'my-function state)

     General Forms:
     (guard-obligation name guard-debug ctx state)
     (guard-obligation term guard-debug ctx state)

where the first argument is either the name of a function or theorem or
is a non-variable term that may be in untranslated form; guard-debug is
typically nil but may be t (see GUARD-DEBUG); ctx is a context
(typically, a symbol used in error and warning messages); and state
references the ACL2 state.

If you want to obtain the formula but you don't care about the so-called
"tag tree":

     (mv-let (erp val state)
             (guard-obligation x guard-debug 'top-level state)
             (if erp
                ( .. code for handling error case, e.g., name is undefined .. )
               (let ((cl-set (cadr val))) ; to be proved for guard verification
                 ( .. code using cl-set, which is a list of clauses,
                      implicitly conjoined, each of which is viewed as
                      a disjunction .. ))))

The form (guard-obligation x guard-debug ctx state) evaluates to a
triple (mv erp val state), where erp is nil unless there is an error,
and state is the ACL2 state.  Suppose erp is nil.  Then val is the
keyword :redundant if the corresponding verify-guards event would be
redundant; see REDUNDANT-EVENTS.  Otherwise, val is a tuple
(list* names cl-set ttree), where: names is (cons :term xt) if x is not
a variable, where xt is the translated form of x; and otherwise is a
list containing x along with, if x is defined in a mutual-recursion,
any other functions defined in the same mutual-recursion nest; cl-set
is a list of lists of terms, viewed as a conjunction of clauses (each
viewed (as a disjunction); and ttree is an assumption-free tag tree
that justifies cl-set.  (The notion of "tag tree" may probably be
ignored except for system developers.)

Guard-obligation is typically used for function names or non-variable
terms, but as for verify-guards, it may also be applied to theorem
names.

See the source code for verify-guards-formula for an example of how to
use guard-obligation.

IN-PACKAGE    select current package

     Example:
     (in-package "MY-PKG")

     General Form:
     (in-package str)

where str is a string that names an existing ACL2 package, i.e., one of
the initial packages such as "KEYWORD" or "ACL2" or a package
introduced with defpkg.  For a complete list of the known packages
created with defpkg, evaluate

     (strip-cars (known-package-alist state)).

See DEFPKG.  An ACL2 book (see BOOKS) must contain a
single in-package form, which must be the first form in that book.

LD    the ACL2 read-eval-print loop, file loader, and command processor

     Examples:
     (LD "foo.lisp")              ; read and evaluate each form in file
                                  ; "foo.lisp", in order
     (LD "foo.lisp" :ld-pre-eval-print t)
                                  ; as above, but print each form to standard
                                  ; character output just before it is evaluated

     General Form:
     (LD standard-oi                  ; open obj in channel, stringp file name
                                      ; to open and close, or list of forms

     ; Optional keyword arguments:
         :dir                ...      ; use this add-include-book-dir directory
         :standard-co        ...      ; open char out or file to open and close
         :proofs-co          ...      ; open char out or file to open and close
         :current-package    ...      ; known package name
         :ld-skip-proofsp    ...      ; nil, 'include-book, or t
                                      ;   (see LD-SKIP-PROOFSP)
         :ld-redefinition-action ...  ; nil or '(:a . :b)
         :ld-prompt          ...      ; nil, t, or some prompt printer fn
         :ld-keyword-aliases ...      ; an alist pairing keywords to parse info
         :ld-pre-eval-filter ...      ; :all, :query, or some new name
         :ld-pre-eval-print  ...      ; nil, t, or :never
         :ld-post-eval-print ...      ; nil, t, or :command-conventions
         :ld-evisc-tuple     ...      ; nil or '(alist nil nil level length)
         :ld-error-triples   ...      ; nil or t
         :ld-error-action    ...      ; :return (default), :continue or :error
         :ld-query-control-alist ...  ; alist supplying default responses
         :ld-verbose         ...)     ; nil or t

Ld is the top-level ACL2 read-eval-print loop.  (When you call lp, a
little initialization is done in raw Common Lisp and then ld is
called.)  Ld is also a general-purpose ACL2 file loader and a command
interpreter.  Ld is actually a macro that expands to a function call
involving state.  Ld returns an "error/value/state" triple as explained
below.

See REBUILD for a variant of ld that skips proofs.

The arguments to ld, except for :dir, all happen to be global variables
in state.  For example, 'current-package and 'ld-verbose are global
variables, which may be accessed via (@ current-package) and (@
ld-verbose).  When ld is called, it "binds" these variables.  By
"binds" we actually mean the variables are globally set but restored to
their old values on exit.  Because ld provides the illusion of state
global variables being bound, they are called "ld specials" (after the
Lisp convention of calling a variable "special" if it is referenced
freely after having been bound).

Note that all arguments but the first are passed via keyword.  Any
variable not explicitly given a value in a call retains its pre-call
value, with the exception of :ld-error-action, which defaults to
:return if not explicitly specified.

Just as an example to drive the point home: If current-package is
"ACL2" and you typed

     (ld *standard-oi* :current-package "MY-PKG")

you would find yourself in (an inner) read-eval-print loop in which the
current-package was "MY-PKG".  You could operate there as long as you
wished, changing the current package at will.  But when you typed :q
you would return to the outer read-eval-print loop where the current
package would still be "ACL2".

Roughly speaking, ld repeatedly reads a form from standard-oi,
evaluates it, and prints its result to standard-co.  It does this until
the form evaluates to an error triple whose value component is :q or
until the input channel or list is emptied.  However, ld has many bells
and whistles controlled by the ld specials.  Each such special is
documented individually.  For example, see the documentation for
standard-oi, current-package, ld-pre-eval-print, etc.

A more precise description of ld is as follows.  In the description
below we use the ld specials as variables, e.g., we say "a form is read
from standard-oi."  By this usage we refer to the current value of the
named state global variable, e.g., we mean "a form is read from the
current value of 'standard-oi." This technicality has an important
implication: If while interacting with ld you change the value of one of
the ld specials, e.g., 'standard-oi, you will change the behavior of
ld, e.g., subsequent input will be taken from the new value.

Three ld specials are treated as channels: standard-oi is treated as an
object input channel and is the source of forms evaluated by ld;
standard-co and proofs-co are treated as character output channels and
various flavors of output are printed to them.  However, the supplied
values of these specials need not actually be channels; several special
cases are recognized.

If the supplied value of one of these is in fact an open channel of the
appropriate type, that channel is used and is not closed by ld.  If the
supplied value of one of these specials is a string, the string is
treated as a file name in (essentially) Unix syntax (see
PATHNAME) and a channel of the appropriate type is opened to/from
that file.  Any channel opened by ld during the binding of the ld
specials is automatically closed by ld upon termination.  If
standard-co and proofs-co are equal strings, only one channel to that
file is opened and is used for both.

As a special convenience, when standard-oi is a string and the :dir
argument provided and not nil, we look up :dir in the table of
directories maintained by add-include-book-dir, and prepend this
directory to standard-oi to create the filename.  (In this case,
however, we require that standard-oi is a relative pathname, not an
absolute pathname.)  For example, one can write (ld
"arithmetic/top-with-meta.lisp" :dir :system) to ld that particular
system library.  (Of course, you should almost always load books like
arithmetic/top-with-meta using include-book instead of ld.)  If :dir is
not specified, then a relative pathname is resolved using the connected
book directory; see CBD.

Several other alternatives are allowed for standard-oi.  If standard-oi
is a true list then it is taken as the list of forms to be processed.
If standard-oi is a list ending in an open channel, then ld processes
the forms in the list and then reads and processes the forms from the
channel.  Analogously, if standard-oi is a list ending a string, an
object channel from the named file is opened and ld processes the forms
in the list followed by the forms in the file.  That channel is closed
upon termination of ld.

The remaining ld specials are handled more simply and generally have to
be bound to one of a finite number of tokens described in the :doc
entries for each ld special.  Should any ld special be supplied an
inappropriate value, an error message is printed.

Next, if ld-verbose is t, ld prints the message "ACL2 loading name"
where name names the file or channel from which forms are being read.
At the conclusion of ld, it will print "Finished loading name" if
ld-verbose is t.

Finally, ld repeatedly executes the ACL2 read-eval-print step, which
may be described as follows.  A prompt is printed to standard-co if
ld-prompt is non-nil.  The format of the prompt is determined by
ld-prompt.  If it is t, the default ACL2 prompt is used.  If it is any
other non-nil value then it is treated as an ACL2 function that will
print the desired prompt.  See LD-PROMPT.  In the exceptional
case where ld's input is coming from the terminal (*standard-oi*) but
its output is going to a different sink (i.e., standard-co is not
*standard-co*), we also print the prompt to the terminal.

Ld then reads a form from standard-oi.  If the object read is a
keyword, ld constructs a "keyword command form" by possibly reading
several more objects.  See KEYWORD-COMMANDS.  This construction
process is sensitive to the value of ld-keyword-aliases.  See
LD-KEYWORD-ALIASES.  Otherwise, the object read is treated as the
command form.

Ld next decides whether to evaluate or skip this form, depending on
ld-pre-eval-filter.  Initially, the filter must be either :all, :query,
or a new name.  If it is :all, it means all forms are evaluated.  If it
is :query, it means each form that is read is displayed and the user is
queried.  Otherwise, the filter is a name and each form that is read is
evaluated as long as the name remains new, but if the name is ever
introduced then no more forms are read and ld terminates.  See
LD-PRE-EVAL-FILTER.

If the form is to be evaluated, first prints the form to standard-co,
if ld-pre-eval-print is t.  With this feature, ld can process an input
file or form list and construct a script of the session that appears as
though each form was typed in.  See LD-PRE-EVAL-PRINT.

Ld then evaluates the form, with state bound to the current state.  The
result is some list of (multiple) values.  If a state is among the
values, then ld uses that state as the subsequent current state.

Depending on ld-error-triples, ld may interpret the result as an
"error." See LD-ERROR-TRIPLES.  We first discuss ld's behavior
if no error signal is detected (either because none was sent or because
ld is ignoring them as per ld-error-triples).

In the case of a non-erroneous result, ld does two things: First, if
the logical world in the now current state is different than the world
before execution of the form, ld adds to the world a "command landmark"
containing the form evaluated.  See COMMAND-DESCRIPTOR.
Second, ld prints the result to standard-co, according to
ld-post-eval-print.  If ld-post-eval-print is nil, no result is
printed.  If it is t, all of the results are printed as a list of
(multiple) values.  Otherwise, it is :command-conventions and only the
non-erroneous "value" component of the result is printed.  See
LD-POST-EVAL-PRINT.

Whenever ld prints anything (whether the input form, a query, or some
results) it "eviscerates" it if ld-evisc-tuple is non-nil.
Essentially, evisceration is a generalization of Common Lisp's use of
*print-level* and *print-length* to hide large substructures.  See
EVISC-TUPLE.

We now return to the case of a form whose evaluation signals an error.
In this case, ld first restores the ACL2 logical world to what it was
just before the erroneous form was evaluated.  Thus, a form that
partially changes the world (i.e., begins to store properties) and then
signals an error, has no effect on the world.  You may see this happen
on commands that execute several events (e.g., an encapsulate or a
progn of several defuns): even though the output makes it appear that
the initial events were executed, if an error is signalled by a later
event the entire block of events is discarded.

After rolling back, ld takes an action determined by ld-error-action.
If the action is :continue, ld merely iterates the read-eval-print
step.  Note that nothing suggestive of the value of the "erroneous"
form is printed.  If the action is :return, ld terminates normally.  If
the action is :error, ld terminates signalling an error to its caller.
If its caller is in fact another instance of ld and that instance is
watching out for error signals, the entire world created by the
erroneous inner ld will be discarded by the outer ld.

Ld returns an error triple, (mv erp val state).  Erp is t or nil
indicating whether an error is being signalled.  If no error is
signalled, val is the "reason" ld terminated and is one of :exit
(meaning :q was read), :eof (meaning the input source was exhausted),
:error (meaning an error occurred but has been supressed) or :filter
(meaning the ld-pre-eval-filter terminated ld).

PRINT-GV    print a form whose evaluation caused a guard violation

By default, ACL2 checks input constraints on functions, known as
guards.  When guards are violated, an informative message is printed;
but sometimes it is useful to investigate why the guard check fails.
The utility print-gv is provided for that purpose.  (Alternatively, you
may prefer to avoid guards entirely with (set-guard-checking :none);
see SET-GUARD-CHECKING.)

     Example Forms:
     (print-gv)
     (print-gv :evisc-tuple (evisc-tuple 4 4 nil nil))
     (print-gv :evisc-tuple (evisc-tuple 4 ; print-level
                                         5 ; print-length
                                         (world-evisceration-alist state nil)
                                         nil ; hiding-cars
                                         ))

     General Form:
     (print-gv :evisc-tuple x)

where the :evisc-tuple argument is optional and defaults to one that
hides only the ACL2 logical world, by printing <world> instead of a
very large structure.  See EVISC-TUPLE for a discussion of
evisc-tuples.

To see how one might use print-gv, consider the following definition.

     (defun foo (x)
       (declare (xargs :guard (and (my-first-predicate x)
                                   (my-second-predicate x))))
       (cdr x))

Now suppose we evaluate a call of foo and obtain a guard violation.

     ACL2 !>(foo 3)

     ACL2 Error in TOP-LEVEL:  The guard for the function call (FOO X),
     which is (AND (MY-FIRST-PREDICATE X) (MY-SECOND-PREDICATE X)), is violated
     by the arguments in the call (FOO 3).  To debug: See :DOC print-gv,
     see :DOC trace, and see :DOC wet.  See :DOC set-guard-checking for
     information about suppressing this check with (set-guard-checking :none),
     as recommended for new users.

     ACL2 !>

We can obtain (in essence) the guard form that was false, as follows.

     ACL2 !>(print-gv)

     (LET ((X '3))
          (DECLARE (IGNORABLE X))
          (AND (MY-FIRST-PREDICATE X)
               (MY-SECOND-PREDICATE X)))

     ACL2 !>

But which conjunct is to blame?  With a bit of editing we can try each
conjunct in turn.

     ACL2 !>(LET ((X '3))
                 (DECLARE (IGNORABLE X))
                 (MY-FIRST-PREDICATE X))
     T
     ACL2 !>(LET ((X '3))
                 (DECLARE (IGNORABLE X))
                 (MY-SECOND-PREDICATE X))
     NIL
     ACL2 !>

Aha!  Now we can investigate why the second predicate fails for 3.

Finally, we mention a hack that will give you access in raw Lisp to the
form printed by (print-gv).  After a guard violation, just submit this
form to raw Lisp:

     (print-gv1 (cdr (assoc 'ev-fncall-guard-er-wormhole *wormhole-outputs*))
                (w state))

And even more finally, we note that while print-gv is a utility for
debugging guard violations, in contrast, see GUARD-DEBUG for a
utility to assist in debugging failed proofs arising from guard
verification.

PROPS    print the ACL2 properties on a symbol

     Example:
     :props assoc-eq

Props takes one argument, a symbol, and prints all of the properties
that are on that symbol in the ACL2 world.

PSO    show the most recently saved output

Evaluate :pso in order to print output that was generated in an
environment where output was being saved;  see SET-SAVED-OUTPUT
for details.  However, proof-tree output will be suppressed; use :pso!
if you want that output to be printed as well.

Also see PSOG, for printing saved output in gag-mode.

PSO!    show the most recently saved output, including proof-tree output

Evaluate :pso! in order to print output that was generated in an
environment where output was being saved; see SET-SAVED-OUTPUT
for details.  Note that proof-tree will be included; use :pso if you
want that output to be suppressed.

Also see PSOG, for printing saved output in gag-mode.

PSOG    show the most recently saved output in gag-mode

Evaluate :psog in order to print output in gag-mode that was generated
in an environment where output was being saved;  see
SET-SAVED-OUTPUT for details.

Also see PSO and see PSO! for printing the full output.

PSTACK    seeing what is the prover up to

     General Forms:
     (pstack)      ; inspect break
     (pstack t)    ; inspect break, printing all calls in abbreviated form
     (pstack :all) ; as above, but only abbreviating the ACL2 world

When the form (pstack) is executed during a break from a proof, or at
the end of a proof that the user has aborted, a "process stack" (or
"prover stack") will be printed that gives some idea of what the
theorem prover has been doing.  Moreover, by evaluating (verbose-pstack
t) before starting a proof (see VERBOSE-PSTACK) one can get
trace-like information about prover functions, including time
summaries, printed to the screen during a proof.  This feature is
currently quite raw and may be refined considerably as time goes on,
based on user suggestions.  For example, the usual control of printing
given by set-inhibit-output-lst is irrelevant for printing the pstack.

The use of (pstack t) or (pstack :all) should only be used by those who
are comfortable looking at functions in the ACL2 source code.
Otherwise, simply use (pstack).

Entries in the pstack include the following (listed here alphabetically,
except for the first).

preprocess-clause, simplify-clause, etc. (in general,xxx-clause):
top-level processes in the prover "waterfall"

clausify: splitting a goal into subgoals

ev-fncall: evaluating a function on explicit arguments

ev-fncall-meta:  evaluating a metafunction

forward-chain: building a context for the current goal using
forward-chaining rules

induct: finding an induction scheme

pop-clause:  getting the next goal to prove by induction

process-assumptions:  creating forcing rounds

remove-built-in-clauses: removing built-in clauses (see
BUILT-IN-CLAUSES)

process-equational-polys:  deducing interesting equations

remove-trivial-equivalences:  removing trivial equalities (and
equivalences) from the current goal

rewrite-atm:  rewriting a top-level term in the current goal

setup-simplify-clause-pot-lst:  building the linear arithmetic database
for the current goal

strip-branches,  subsumption-replacement-loop:  subroutines of clausify

waterfall: top-level proof control

VERBOSE-PSTACK    seeing what is the prover up to (for advanced users)

     General Forms:
     (verbose-pstack t)   ; get trace-like information on prover during proofs
     (verbose-pstack '(fn1 fn2 ...))
                          ; as above, but omit calls of the indicated functions
     (verbose-pstack nil) ; turn off trace-like information on prover

For example, (verbose-pstack '(ev-fncall)) will provide a trace of
various prover functions during proofs, except for the function
ev-fncall.

By evaluating (verbose-pstack t) one can get trace-like information
during subsequent proofs about prover functions, including time
summaries, printed to the screen during a proof.  To turn off this
feature, evaluate (verbose-pstack nil).  Also See PSTACK.

Q    quit ACL2 (type :q) -- reenter with (lp)

     Example:
     ACL2 !>:Q

The keyword command :q typed at the top-level of the ACL2 loop will
terminate the loop and return control to the Common Lisp top-level (or,
more precisely, to whatever program invoked lp).  To reenter the ACL2
loop, execute (acl2::lp) in Common Lisp.  You will be in the same state
as you were when you exited with :q, unless during your stay in Common
Lisp you messed the data structures representating the ACL2 state
(including files, property lists, and single-threaded objects).

Unlike all other keyword commands, typing :q is not equivalent to
invoking the function q.  There is no function q.

QUIT    quit entirely out of Lisp

Same as good-bye.

REBUILD    a convenient way to reconstruct your old state

     Examples:
     ACL2 !>(rebuild "project.lisp")
     ACL2 !>(rebuild "project.lisp" t)
     ACL2 !>(rebuild "project.lisp" t :dir :system)
     ACL2 !>(rebuild "project.lisp" :all)
     ACL2 !>(rebuild "project.lisp" :query)
     ACL2 !>(rebuild "project.lisp" 'lemma-22)

Rebuild allows you to assume all the commands in a given file or list,
supplied in the first argument.  Because rebuild processes an arbitrary
sequence of commands with ld-skip-proofsp t, it is unsound!  However,
if each of these commands is in fact admissible, then processing them
with rebuild will construct the same logical state that you would be in
if you typed each command and waited through the proofs again.  Thus,
rebuild is a way to reconstruct a state previously obtained by proving
your way through the commands.

The second, optional argument to rebuild is a "filter" (see
LD-PRE-EVAL-FILTER) that lets you specify which commands to process.
You may specify t, :all, :query, or a new logical name.  t and :all
both mean that you expect the entire file or list to be processed.
:query means that you will be asked about each command in turn.  A new
name means that all commands will be processed as long as the name is
new, i.e., rebuild will stop processing commands immediately after
executing a command that introduces name.  Rebuild will also stop if
any command causes an error.  You may therefore wish to plant an
erroneous form in the file, e.g., (mv t nil state), (see
LD-ERROR-TRIPLES), to cause rebuild to stop there.  The form
(i-am-here) is such a pre-defined form.  If you do not specify a
filter, rebuild will query you for one.

Inspection of the definition of rebuild, e.g., via :pc rebuild-fn, will
reveal that it is just a glorified call to the function ld.  See
LD if you find yourself wishing that rebuild had additional
functionality.

If you supply the above "filter" argument, then you may also supply the
keyword argument :dir, which is then passed to ld; see LD.

RESET-LD-SPECIALS    restores initial settings of the ld specials

     Examples:
     (reset-ld-specials t)
     (reset-ld-specials nil)

Roughly speaking, the ld specials are certain state global variables,
such as current-package, ld-prompt, and ld-pre-eval-filter, which are
managed by ld as though they were local variables.  These variables
determine the channels on which ld reads and prints and control many
options of ld.  See LD for the details on what the ld specials
are.

This function, reset-ld-specials, takes one Boolean argument, flg.  The
function resets all of the ld specials to their initial, top-level
values, except for the three channel variables, standard-oi,
standard-co, and proofs-co, which are reset to their initial values
only if flg is non-nil.  Of course, if you are in a recursive call of
ld, then when you exit that call, the ld specials will be restored to
the values they had at the time ld was called recursively.  To see what
the initial values are, inspect the value of the constant
*initial-ld-special-bindings*.

SAVE-EXEC    save an executable image and (for most Common Lisps) a wrapper script

See SAVING-AND-RESTORING for an explanation of why one might
want to use this function.

     Examples:
     ; Save an executable named my-saved_acl2:
     (save-exec "my-saved_acl2"
                "This saved image includes Version 7 of Project Foo.")

     ; Same as above, but with a generic comment instead:
     (save-exec "my-saved_acl2" nil)

     General Form:
     (save-exec exec-filename extra-startup-string)

where exec-filename is the filename of the proposed executable and
extra-startup-string is a non-empty string to be printed after the
normal ACL2 startup message when you start up the saved image.  However,
extra-startup-string is allowed to be nil, in which case a generic
string will be printed instead.

*Notes*:

1. For technical reasons, you must first exit the ACL2 read-eval-print
loop, for example by executing :q, before evaluating a save-exec call.

2. The image will be saved so that in the new image, the raw Lisp
package and the package in the ACL2 read-eval-print loop (see
LP) will be the same as their respective values at the time save-exec
is called.

3. For most Common Lisps, the specified file (e.g., "my-saved_acl2" in
the examples above) will be written as a small script, which in turn
invokes a saved image to which an extension has been appended (e.g.,
my-saved_acl2.gcl for the examples above, when the underlying Common
Lisp is GCL on a non-Windows system).

SHARP-BANG-READER    package prefix that is not restricted to symbols

     Examples:

     ACL2 !>(defpkg "FOO" nil)

     Summary
     Form:  ( DEFPKG "FOO" ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      "FOO"
     ACL2 !>'#!foo(a b)
     (FOO::A FOO::B)
     ACL2 !>'#!foo(a #!acl2 b)
     (FOO::A B)
     ACL2 !>'#!foo(#!acl2 a b)
     (A FOO::B)
     ACL2 !>'#!foo(#!"ACL2" a b)
     (A FOO::B)
     ACL2 !>

The ACL2 reader supports the syntax #!pkg-name expr where pkg-name is a
string or symbol that names a package known to ACL2.  As illustrated
above, this syntax nests as one might expect.  In the special case that
expr is a symbol, #!pkg-name expr is equivalent to pkg-name::expr.

SHARP-COMMA-READER    DEPRECATED read-time evaluation of constants

The use of `#,' has been deprecated.  Please use `#.' instead; see
SHARP-DOT-READER.

SHARP-DOT-READER    read-time evaluation of constants

     Example:

     ACL2 !>(defconst *a* '(a b c))

     Summary
     Form:  ( DEFCONST *A* ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      *A*
     ACL2 !>(quote (1 2 #.*a* 3 4))
     (1 2 (A B C) 3 4)
     ACL2 !>

The ACL2 reader supports the syntax #.*a* where *a* was defined by
defconst.  In this case, the reader treats #.*a* as though it were
reading the value of *a*.  This feature can be useful in conjunction
with the use of evisc-table to abbreviate large constants, so that the
abbreviation can be read back in; see EVISC-TABLE.

Note that the ACL2 reader only supports `#.' as described above, unlike
Common Lisp.  Older versions (preceding  3.5) used `#.' to abort, but
that functionality is now carried out by (a!); see A!.

SHOW-ACCUMULATED-PERSISTENCE    See ACCUMULATED-PERSISTENCE.

SKIP-PROOFS    skip proofs for a given form -- a quick way to introduce unsoundness

     Example Form:
     (skip-proofs
       (defun foo (x)
         (if (atom x) nil (cons (car x) (foo (reverse (cdr x)))))))

     General Form:
     (skip-proofs form)

where form is processed as usual except that the proof obligations
usually generated are merely assumed.

Normally form is an event; see EVENTS.  If you want to put
skip-proofs around more than one event, consider the following (see
PROGN): (skip-proofs (progn event1 event2 ... eventk)).

WARNING:  Skip-proofs allows inconsistent events to be admitted to the
logic.  Use it at your own risk!

Sometimes in the development of a formal model or proof it is
convenient to skip the proofs required by a given event.  By embedding
the event in a skip-proofs form, you can avoid the proof burdens
generated by the event, at the risk of introducing unsoundness.  Below
we list four illustrative situations in which you might find
skip-proofs useful.

1. The termination argument for a proposed function definition is
complicated.  You presume you could admit it, but are not sure that
your definition has the desired properties.  By embedding the defun
event in a skip-proofs you can "admit" the function and experiment with
theorems about it before undoing (see UBT) and then paying the
price of its admission.  Note however that you might still have to
supply a measure.  The set of formals used in some valid measure, known
as the "measured subset" of the set of formals, is used by ACL2's
induction heuristics and therefore needs to be suitably specified.  You
may wish to specify the special measure of (:? v1 ... vk), where (v1
... vk) enumerates the measured subset.

2. You intend eventually to verify the guards for a definition but do
not want to take the time now to pursue that.  By embedding the
verify-guards event in a skip-proofs you can get the system to behave
as though the guards were verified.

3. You are repeatedly recertifying a book while making many
experimental changes.  A certain defthm in the book takes a very long
time to prove and you believe the proof is not affected by the changes
you are making.  By embedding the defthm event in a skip-proofs you
allow the theorem to be assumed without proof during the experimental
recertifications.

4. You are constructing a proof top-down and wish to defer the proof of
a defthm until you are convinced of its utility.  You can embed the
defthm in a skip-proofs.  Of course, you may find later (when you
attempt prove the theorem) that the proposed defthm is not a theorem.

Unsoundness or Lisp errors may result if the presumptions underlying a
use of skip-proofs are incorrect.  Therefore, skip-proofs must be
considered a dangerous (though useful) tool in system development.

Roughly speaking, a defthm embedded in a skip-proofs is essentially a
defaxiom, except that it is not noted as an axiom for the purposes of
functional instantiation (see LEMMA-INSTANCE).  But a skipped
defun is much more subtle since not only is the definitional equation
being assumed but so are formulas relating to termination and type.
The situation is also difficult to characterize if the skip-proofs
events are within the scope of an encapsulate in which constrained
functions are being introduced.  In such contexts no clear logical
story is maintained; in particular, constraints aren't properly tracked
for definitions.  A proof script involving skip-proofs should be
regarded as work-in-progress, not as a completed proof with some
unproved assumptions.  A skip-proofs event represents a promise by the
author to admit the given event without further axioms.  In other
words, skip-proofs should only be used when the belief is that the
proof obligations are indeed theorems in the existing ACL2 logical
world.

ACL2 allows the certification of books containing skip-proofs events.
This is contrary to the spirit of certified books, since one is
supposedly assured by a valid certificate that a book has been
"blessed."  But certification, too, takes the view of skip-proofs as
"work-in-progress" and so allows the author of the book to promise to
finish.  When such books are certified, a warning to the author is
printed, reminding him or her of the incurred obligation.  When books
containing skip-proofs are included into a session, a warning to the
user is printed, reminding the user that the book is in fact incomplete
and possibly inconsistent.  This warning is in fact an error if
:skip-proofs-okp is nil in the include-book form; see
INCLUDE-BOOK.

THM    prove a theorem

     Example:
     (thm (equal (app (app a b) c)
                 (app a (app b c))))

Also see DEFTHM.  Unlike defthm, thm does not create an event;
it merely causes the theorem prover to attempt a proof.

     General Form:
     (thm term
          :hints        hints
          :otf-flg      otf-flg
          :doc          doc-string)

where term is a term alleged to be a theorem, and hints, otf-flg and
doc-string are as described in the corresponding :doc entries.  The
three keyword arguments above are all optional.

TIME$    time a form

     Examples:
     (time$ (foo 3 4))
     (time$ (mini-proveall))
     (defun bar (x) (time$ (f x)))

     General Form:
     (time$ form)

where form is processed as usual except that the host Common Lisp times
its evaluation.

Semantically, (time$ x) equals x.  However, its evaluation produces
timing output, via the time utility in the host Common Lisp.

Notes:

(1) Common Lisp specifies that the time utility prints to "trace
output."  If you have opened a trace file (see
OPEN-TRACE-FILE), then you can expect to find the time$ output there.
You can probably arrange for the time$ output to go to the terminal
instead, say by using a suitable form in raw Lisp, for example: (let
((*trace-output* *terminal-io*)) (time <form>)).

(2) In some Common Lisp implementations, for example CCL (OpenMCL), you
may see that the form being timed is a call of the ACL2 evaluator
function ev-rec.  This is normal.

TRANS    print the macroexpansion of a form

     Examples:
     :trans (list a b c)
     :trans (caddr x)
     :trans (cond (p q) (r))

This function takes one argument, an alleged term, and translates it,
expanding the macros in it completely.  Either an error is caused or
the formal meaning of the term is printed.  We also print the "output
signature" which indicates how many results are returned and which are
single-threaded objects.  For example, a term that returns one ordinary
object (e.g., an object other than STATE or a user-defined
single-threaded object (see DEFSTOBJ)) has the output signature

     => *

A term that returns the single-threaded object STATE has the output
signature

     => STATE

and a term that returns four results might have the output signature

     => (MV $MEM * * STATE)

This signature indicates that the first result is the (user defined)
single-threaded object $MEM, that the next two results are ordinary,
and that the last result is STATE.

See TRANS! for a corresponding command that does not enforce
restrictions of single-threaded objects.

It is sometimes more convenient to use trans1 which is like trans but
which only does top-level macroexpansion.

For more, see TERM.

TRANS!    print the macroexpansion of a form without single-threadedness concerns

     Examples:
     :trans! (list a b c)
     :trans! (append x state)

:Trans! is identical to :trans, except that unlike :trans, :trans!
ignores single-threadedness restrictions.  Thus, the second form above
is legal for :trans!.  Also see TRANS and see TRANS1.

TRANS1    print the one-step macroexpansion of a form

     Examples:
     :trans1 (list a b c)
     :trans1 (caddr x)
     :trans1 (cond (p q) (r))

This function takes one argument, an alleged term, and expands the
top-level macro in it for one step only.  Either an error is caused,
which happens when the form is not a call of a macro, or the result is
printed.  Also see TRANS, which translates the given form
completely.

VERIFY-GUARDS-FORMULA    view the guard proof obligation, without prooving it

See VERIFY-GUARDS and see GUARD for a discussion of
guards.  This utility is provided for viewing a guard proof obligation,
without doing a proof.

     Example Forms:
     (verify-guards-formula foo)
     (verify-guards-formula foo :guard-debug t)
     (verify-guards-formula foo :otf-flg dont-care :xyz whatever)
     (verify-guards-formula (+ (foo x) (bar y)) :guard-debug t)

Verify-guards-formula allows all keywords, but only pays attention to
:guard-debug, which has the same effect as in verify-guards (see
GUARD-DEBUG).  Apply verify-guards-formula to a name just as you
would use verify-guards, but when you only want to view the formula
rather than creating an event.  If the first argument is not a symbol

See GUARD-OBLIGATION if you want to obtain guard proof
obligations for use in a program.

WITH-PROVER-TIME-LIMIT    limit the time for proofs

     Examples:

     ; Limit (mini-proveall) to about 1/4 second:
     (with-prover-time-limit 1/4 (mini-proveall))

     ; Limit (mini-proveall) to about 1/4 second, even if surrounding call of
     ; with-prover-time-limit provides for a more restrictive bound:
     (with-prover-time-limit '(1/4) (mini-proveall))

     ; Limit the indicated theorem to about 1/50 second, and if the proof does not
     ; complete or it fails, then put down a label instead.
     (mv-let (erp val state)
             (with-prover-time-limit
              1/50
              (thm (equal (append (append x x) x)
                          (append x x x))))
             (if erp
                 (deflabel foo :doc "Attempt failed.")
               (value (list :succeeded-with val))))

     General Form:
     (with-prover-time-limit time form)

where time evaluates to a positive rational number or to a list
containing such, and form is arbitrary.  Logically,
(with-prover-time-limit time form) is equivalent to form.  However, if
the runtime for evaluation of form exceeds the value specified by time,
and if ACL2 notices this fact during a proof, then that proof will
abort, for example like this:

     ACL2 Error in ( DEFTHM PERM-REFLEXIVE ...):  Out of time in the rewriter.

If there is already a surrounding call of with-prover-time-limit that
has set up an expiration time, the inner with-prover-time-limit call is
not allowed to push that time further into the future unless the inner
time is specified as a list containing a rational, rather than as a
rational.

Although with-prover-time-limit is an ACL2 function -- in particular it
evaluates both its arguments -- nevertheless, it is not a standard
function in some respects.  (1) The value of its first (time limit)
argument affects the evaluation of its second argument (by causing an
error during that evaluation if the time for completion is
insufficient).  (2) The second argument can return multiple values (see
MV), which are then returned by the call of
with-prover-time-limit. (3) Thus, there is not a fixed number of values
returned by with-prover-time-limit.

If you find that the time limit appears to be implemented too loosely,
you are encouraged to email an example to the ACL2 implementors with
instructions on how to observe the undesirable behavior.  This
information can probably be used to improve ACL2 by the insertion of
more checks for expiration of the time limit.

The rest of this documentation topic explains the rather subtle logical
story, and is not necessary for understanding how to use
with-prover-time-limit.  The ACL2 state object logically contains a
field called the acl2-oracle, which is an arbitrary true list of
objects.  This field can be read by a function called read-acl2-oracle,
which however is untouchable (see PUSH-UNTOUCHABLE), meaning
that it is cannot be called by ACL2 users.  The acl2-oracle field is
thus "secret".  Our claim is that any ACL2 session makes sense for
*some* value of acl2-oracle in the initial state for that session.
Logically, with-prover-time-limit is a no-op, just returning its second
value.  But under the hood, it provides a "hint" for the acl2-oracle,
so that (logically speaking) when its first element (car) is consulted
by ACL2's prover to see if the time limit has expired, it gets the
"right" answer (specifically, either nil if all is well or else a
message to print if the time limit has expired).  Logically, the
acl2-oracle is then cdr'ed -- that is, its first element is popped off
-- so that future results from read-acl2-oracle are independent of the
one just obtained.

PARALLELISM    experimental extension for evaluating forms in parallel

This documentation topic relates to an experimental extension of ACL2,
created initially by David L. Rager.  See PARALLELISM-BUILD for
how to build an executable image that supports parallel evaluation.
Also see books/parallel for examples.

One of ACL2's strengths lies in its ability to execute industrial models
efficiently.  The ACL2 source code provides an experimental parallel
evaluation capability that can increase the speed of explicit
evaluation, including simulator runs using such models, and it can also
decrease the time required for proofs that make heavy use of the
evaluation of ground terms.

The parallelism primitives are plet, pargs, pand, and por.  Pand and
por terminate early when an argument is found to evaluate to nil or
non-nil, respectively, thus potentially improving on the efficiency of
lazy evaluation.

The parallelism primitives allow for limiting parallel evaluation
(spawning of so-called "threads") depending on resource availability.
Specifically, the primitives allow specification of a size condition to
control the granularity under which threads are allowed to spawn.  You
can use such granularity declarations in recursively-defined functions
to implement data-dependent parallelism in their execution.

We recommend that in order to learn to use the parallelism primitives,
you begin by reading examples: see PARALLELISM-TUTORIAL.  That
section will direct you to further documentation topics.

EARLY-TERMINATION    early termination for pand and por.

The evaluation of (and expr1 expr2) returns nil if expr1 evaluates to
nil, avoiding the evaluation of expr2.  More generally, the evaluation
of (and expr1 expr2 ... exprk) terminates with a return value of nil as
soon as any expri evaluates to nil -- no exprj is evaluated in this
case for j > i.  This so-called "lazy evaluation" of and terms can thus
save some computation; roughly speaking, the smaller the i, the more
computation is saved.

If the above call of and is replaced by its parallel version, pand,
then there can be even more opportunity for skipping work.  The
arguments to pand can be evaluated in parallel, in which case the first
such evaluation that returns with a value of nil, if any, causes the
remaining such evaluations to abort.

Consider the following functions that compute whether a tree is valid
(see GRANULARITY for a discussion of the granularity form).

     (defun valid-tip (x)
       (declare (xargs :guard t))
       (or (eq x 'A)
           (eq x 'T)
           (eq x 'C)
           (eq x 'G)))

     (defun pvalid-tree (x depth)
       (declare (xargs :guard (natp depth)))
       (if (atom x)
           (valid-tip x)
         (pand (declare (granularity (< depth 10)))
               (pvalid-tree (car x) (1+ depth))
               (pvalid-tree (cdr x) (1+ depth)))))

We would like to stop execution as soon as any tip is found to be
invalid.  So, when computing the conjunction of terms by using pand,
once one of those terms evaluates to nil, the computations for the
other terms are aborted and the pand call returns nil.  By using pand,
we can in principle attain a speedup factor greater than the number of
available cores.

The concept of early termination also applies to por, except that early
termination occurs when an argument evaluates to non-nil.

GRANULARITY    limit the amount of parallelism

Some function calls are on arguments whose evaluation time is long
enough to warrant parallel evaluation, while others are not.  A
granularity form can be used to make appropriate restrictions on the
use of parallelism.

For example, consider the Fibonacci function.  Experiments have
suggested that execution time can be reduced if whenever the argument
is less than 27, a serial version of the Fibonacci function is called.
One way to utilize this information is to write two definitions of the
Fibonacci function, one serial and one parallel.

     (defun fib (x)
       (declare (xargs :guard (natp x)))
       (cond ((or (zp x) (<= x 0)) 0)
             ((= x 1) 1)
             (t (binary-+ (fib (- x 1))
                          (fib (- x 2))))))

     (defun pfib (x)
       (declare (xargs :guard (natp x)))
       (cond ((or (zp x) (<= x 0)) 0)
             ((= x 1) 1)
             ((< x 27) (binary-+ (fib (- x 1))
                                 (fib (- x 2))))
             (t (pargs (binary-+ (pfib (- x 1))
                                 (pfib (- x 2)))))))

We realize quickly that writing both of these function definitions is
cumbersome and redundant.  This problem can be avoided by using a
granularity declaration with a parallelism primitive.  This form ensures
that a call is parallelized only if resources are available and the
granularity form evaluates to a non-nil value at the time of the call.
Below is a definition of the Fibonacci function using a granularity
form.

     (defun pfib (x)
       (declare (xargs :guard (natp x)))
       (cond ((or (zp x) (<= x 0)) 0)
             ((= x 1) 1)
             (t (pargs (declare (granularity (>= x 27)))
                       (binary-+ (pfib (- x 1))
                                 (pfib (- x 2)))))))

A granularity form can reference an extra formal parameter that
describes the call depth of the function the user is parallelizing.
Consider for example the following parallel mergesort function, based
on Davis's Ordered Sets library.  It splits the data into symmetric
chunks for computation, so we increment the depth argument during the
recursive call on both the car and cdr.

     (include-book "finite-set-theory/osets/sets" :dir :system)
     (defun sets::pmergesort-exec (x depth)
       (declare (xargs :mode :program))
       (cond ((endp x) nil)
             ((endp (cdr x)) (sets::insert (car x) nil))
             (t (mv-let (part1 part2)
                        (sets::split-list x nil nil)
                        (pargs
                         (declare (granularity (< depth 2)))
                         (sets::union (sets::pmergesort-exec part1
                                                             (1+ depth))
                                      (sets::pmergesort-exec part2
                                                             (1+ depth))))))))

A less intrusive method (i.e., not requiring an extra formal parameter
like the depth argument just above), which however can be less
efficient, involves analyzing the data itself for structural
properties.  For example:

     (defun some-depth-exceeds (x n)
       (declare (xargs :guard (natp n)))
       (if (atom x)
           nil
         (if (zp n)
             t
           (or (some-depth-exceeds (car x) (1- n))
               (some-depth-exceeds (cdr x) (1- n))))))

     (defun valid-tip (x)
       (declare (xargs :guard t))
       (or (eq x 'A)
           (eq x 'T)
           (eq x 'C)
           (eq x 'G)))

     (defun pvalid-tree (x)
       (declare (xargs :guard t))
       (if (atom x)
           (valid-tip x)
         (pand (declare (granularity (some-depth-exceeds x 3)))
               (pvalid-tree (car x))
               (pvalid-tree (cdr x)))))

If you experiment with calls of pvalid-tree, you are likely to find that
the "speedup" it provides over a corresponding serial version is, in
fact, a slowdown!  The problem is likely that some-depth-exceeds is an
expensive function to run repeatedly.  Instead of the approach above,
it is often handy to add an extra formal parameter in order to allow
for more efficient granularity forms, as we have done above in the
definition of SETS::pmergesort-exec.

PAND    parallel, Boolean version of and

     Example Forms:
     (pand (subsetp-equal x y)
           (subsetp-equal y x))

     (pand (declare
            (granularity
             (and (> (length x) 500)
                  (> (length y) 500))))
            (subsetp-equal x y)
            (subsetp-equal y x))

     General Form:
     (pand (declare (granularity expr)) ; optional granularity declaration
           arg1 ... argN)

where N >= 0 and each argi and expr are arbitrary terms.

Pand evaluates its arguments in parallel.  It returns a Boolean result:
nil if any argument evaluates to nil, else t.  Note that pand always
returns a Boolean result, even though and can return a non-nil value
other than t, namely the value of its last argument.  (A moment's
reflection will make it clear that in order for por to parallelize
efficiently, it needs to return a Boolean value; so pand returns a
Boolean value for consistency with por.)

Another difference between pand and and is that for a call of pand,
even if an argument evaluates to nil, a subsequent argument may be
evaluated.  Consider the following example (where cw prints a string;
see CW).

     (defun bar ()
       (pand (equal (make-list 100000) nil) ; evaluates to nil
             (cw "hello world~%")))

When (bar) is evaluated, the above arguments of pand can execute in
parallel, causing "hello world" to be printed to the terminal.  If we
had used and rather than pand, then since (equal (make-list 100000)
nil) evaluates to nil, the above call of cw would be avoided and no
such printing would take place.  Even with pand, such printing _might_
not take place, depending on resources, timing of thread creation, and
whether or not parallel evaluation is enabled (see
SET-PARALLEL-EVALUATION).

Note that unlike the case for and, the definition of pand does not
provide (consp x) as a guard to (car x) in the call of pand below:

     (defun h (x)
       (declare (xargs :guard t))
       (pand (consp x) (equal (car x) 'foo)))

As a result, guard verification will fail for the above definition.  If
pand were replaced by and, then guard verification would succeed.

See PARALLELISM-TUTORIAL for another example.  Also see
PARALLELISM-AT-THE-TOP-LEVEL for restrictions on evaluating
parallelism primitives from within the ACL2 top-level loop.  Finally
see EARLY-TERMINATION to read how pand can offer more
efficiency than and by avoiding evaluation of some of its arguments.

PARALLEL    evaluating forms in parallel

See PARALLELISM.

PARALLELISM-AT-THE-TOP-LEVEL    parallel evaluation in the ACL2 top-level loop

Calls of parallelism primitives made explicitly in the ACL2 top-level
loop, as opposed to inside function bodies, will never cause parallel
evaluation.  Such calls will either execute with serial evaluation or
will cause an error; see SET-PARALLEL-EVALUATION.

Consider for example the following call of pargs in the ACL2 top-level
loop.  Instead of executing parge, ACL2 macroexpands away this call,
leaving us with serial evaluation of the arguments to the cons call, or
else causes an error (see SET-PARALLEL-EVALUATION).  If there
is no error, then

     (pargs (cons (expensive-fn-1 4) (expensive-fn-2 5)))

expands into:

     (cons (expensive-fn-1 4) (expensive-fn-2 5))

A trivial way to enable parallel evaluation of a form is to put it
inside a function body.  For example, consider the following definition.

     (defun foo (x y)
       (declare (xargs :guard t))
       (pargs (cons (expensive-fn-1 x) (expensive-fn-2 y))))

Then in an executable image that supports parallel evaluation -- see
PARALLELISM-BUILD for instructions on how to build such an
executable -- submission of the form (foo 4 5), even in the ACL2
top-level loop, can cause parallel evaluation of (expensive-fn-1 4) and
(expensive-fn-2 5).

Note that guards need not be verified in order to obtain parallel
evaluation.  The only restrictions on parallel evaluation are to use an
executable supporting it, to avoid calling parallelism primitives
directly in the top-level loop, to have sufficient resources
(especially, threads) available, and to avoid explicitly disabling
parallel evaluation see SET-PARALLEL-EVALUATION).

PARALLELISM-BUILD    building an ACL2 executable with parallel evaluation enabled

See PARALLEL and see PARALLELISM-TUTORIAL for an
introduction to parallel evaluation in ACL2 using parallelism
primitives pand, por, plet, and pargs.

You can build an experimental version of ACL2 that supports parallel
evaluation in the following host Common Lisp implementations:

     * CCL (OpenMCL)

     * SBCL with threads (feature :sb-thread)

An easy way is to build an executable supporting parallel evaluation is
to include the following with a make command:

     ACL2_PAR=p

So for example, to make an executable image and also documentation
(which will appear in subdirectories doc/EMACS and doc/HTML):

     make large DOC ACL2_PAR=p

PARALLELISM-PERFORMANCE    performance issues for parallel evaluation

See GRANULARITY for an important construct that limits the
spawning of parallel computations, which can be important when a
computation is too short-lived to warrant a separate thread.

There are times in which parallelism provides no speedup because of
garbage collection in the underlying Lisp implementation.  The
following example illustrates this phenomenon.  If you change the
granularity declaration so that the depth bound is 3, 4, or larger
instead of 2, you may still find no speedup.  In all cases you may find
that parallelism results in a significantly greater time spent in
garbage collection.

     (include-book "finite-set-theory/osets/sets" :dir :system)
     (defun sets::pmergesort-exec (x depth)
         (declare (xargs :mode :program))
         (cond ((endp x) nil)
               ((endp (cdr x)) (sets::insert (car x) nil))
               (t (mv-let (part1 part2)
                          (sets::split-list x nil nil)
                          (pargs
                           (declare (granularity (< depth 2)))
                           (sets::union (sets::pmergesort-exec part1
                                                               (1+ depth))
                                        (sets::pmergesort-exec part2
                                                               (1+ depth))))))))
     (defconst *x* (reverse (fromto 1 400000)))
     (time$ (length (sets::pmergesort-exec *x* 0)))
     (set-parallel-evaluation nil)
     (time$ (length (sets::pmergesort-exec *x* 0)))

PARALLELISM-TUTORIAL    a tutorial on how to use the parallelism library.

In this topic we introduce the ACL2 parallelism primitives using the
example of a doubly-recursive Fibonacci function, whose basic
definition is as follows.  See PARALLELISM for a very
high-level summary of the parallelism capability described here, and
see PARALLELISM-BUILD for how to build an executable image that
supports parallel evaluation.  Here, we assume that such an executable
is being used.

Serial Fibonacci

     (defun fib (x)
       (declare (xargs :guard (natp x)))
       (cond ((or (zp x) (<= x 0)) 0)
             ((= x 1) 1)
             (t (+ (fib (- x 1)) (fib (- x 2))))))

Introducing Pargs

A simple way to introduce parallelism into this function definition is
to wrap the addition expression with a call of pargs, and the arguments
to the addition will be computed in parallel whenever resources are
available.  As a result, we end up with a very similar and thus
intuitive function definition.  Note that we replaced + by binary-+,
since pargs expects a function call, not a macro call.

     (defun pfib (x)
       (declare (xargs :guard (natp x)))
       (cond ((or (zp x) (<= x 0)) 0)
             ((= x 1) 1)
             (t (pargs (binary-+ (pfib (- x 1))
                                 (pfib (- x 2)))))))

Introducing the Granularity Problem

After you submit the above two versions of the Fibonacci function, test
them with the following forms.

     (time$ (fib 10))
     (time$ (pfib 10))

Now increase the argument by increments of 5 to 10 until you find your
curiosity satisfied or your patience wearing thin.  You can interrupt
evaluation if necessary and return to the ACL2 loop.  You will
immediately notice that you have not increased execution speed, at
least not by much, by introducing parallelism.

First, consider the computation of (pfib 4).  Assuming resources are
available, (pfib 4) will create a thread for computing (pfib 3) and
another thread for (pfib 2).  It is easy to imagine that setting up each
thread takes much longer than the entire computation of (fib 4).

Second, we must realize that if we have two threads available for
computing (fib 10), then the evaluation of (fib 8) will probably
complete before the evaluation of (fib 9).  Once (fib 8) finishes,
parallelism resources will become available for the next recursive call
made on behalf of (fib 9).  If for example that call is (fib 3), we
will waste a lot of cycles just handing work to the thread that does
this relatively small computation.  We need a way to ensure that
parallelism resources are only used on problems of a "large" size.
Ensuring that only "large" problems are spawned is called the
"granularity problem."

In summary: We want to tell ACL2 that it can evaluate the arguments of
pargs in parallel only when the parameter of pfib is greater than some
threshold.  Our tests using OpenMCL have suggested that 27 is a
reasonable threshold.

Explicit Programming for the Granularity Problem

One way to avoid the granularity problem is to duplicate code as
follows.

     (defun pfib (x)
       (declare (xargs :guard (natp x)))
       (cond ((or (zp x) (<= x 0)) 0)
             ((= x 1) 1)
             (t (if (> x 27) ; the granularity test
                    (pargs (binary-+ (pfib (- x 1))
                                     (pfib (- x 2))))
                  (binary-+ (pfib (- x 1))
                            (pfib (- x 2)))))))

Duplicating code is fundamentally a bad design principle, because it can
double the work for future maintenance.  A "granularity form" is an
expression

     (declare (granularity <form>))

that can allow threads to be spawned (without duplicating code)
whenever the evaluation of <form> results in a non-nil value.  It may
be placed inside any call of a parallelism primitive, in a position
documentated separately for each primitive.  Here is a definition of
pfib using this feature for a call of the parallelism primitive pargs.

     (defun pfib (x)
       (declare (xargs :guard (natp x)))
       (cond ((or (zp x) (<= x 0)) 0)
             ((= x 1) 1)
             (t (pargs
                 (declare (granularity (> x 27)))
                 (binary-+ (pfib (- x 1))
                           (pfib (- x 2)))))))

Test each version as follows (or substitute your own natural number for
33).

       (time$ (fib 33))
       (time$ (pfib 33))

Another Granularity Issue Related to Thread Limitations

Our implementation of parallelism primitives has the property that once
a thread is assigned a computation, that assignment stays in effect
until the computation is complete.  In particular, if a thread
encounters a parallelism primitive that spawns child threads, the
parent thread stays assigned, waiting until the child computations
complete before it can continue its own computation.  In the meantime,
the parent thread reduces the number of additional threads that Lisp
can provide by 1, rather than being reassigned to do other work.

How can this lack of reassignment affect the user?  Consider, for
example, the application of a recursive function to a long list.
Imagine that this function is written so that the body contains a
recursive call, for example as (pargs (process (car x)) (recur (cdr
x))).  Each such pargs call that spawns child work must wait for its
children, one of which is the work of evaluating (recur (cdr x)), to
complete.  There is an ACL2 limit on how much pending work can be in
the system, limiting the number of pargs calls that can result in
parallel evaluation.  For example, if the ACL2 limit is k and each call
of pargs actually spawns threads for evaluating  its arguments, then
after k cdrs there will be no further parallel evaluation.

Possible solutions may include reworking of algorithms (for example to
be tree-based rather than list-based) or using appropriate granularity
forms.  We hope that future implementations will allow thread
"re-deployment" in order to mitigate this problem.

Introducing Plet

We can use a let binding to compute the recursive calls of fib and then
add the bound variables together, as follows.

     (defun fib (x)
       (declare (xargs :guard (natp x)))
       (cond ((or (zp x) (<= x 0)) 0)
             ((= x 1) 1)
             (t (let ((a (fib (- x 1)))
                      (b (fib (- x 2))))
                  (+ a b)))))

By using the parallelism primitive plet, we can introduce parallelism
much as we did using pargs, with an optional granularity form, as
follows.

     (defun pfib (x)
       (declare (xargs :guard (natp x)))
       (cond ((or (zp x) (<= x 0)) 0)
             ((= x 1) 1)
             (t (plet
                 (declare (granularity (> x 27)))
                 ((a (pfib (- x 1)))
                  (b (pfib (- x 2))))
                 (+ a b)))))

Notice that this time, we were able to use + rather than being forced to
use binary-+.  Unlike pargs, which expects a function call (not a macro
call), plet allows macros at the top level of its body.

Introducing Pand (By Way of a Tree Validation Example)

Consider "genetic trees" that contains leaves of DNA elements, in the
sense that each tip is one of the symbols A, G, C, or T.  First we
define the function valid-tip which recognizes whether a tip contains
one of these symbols.

     (defun valid-tip (tip)
       (declare (xargs :guard t))
       (or (eq tip 'A)
           (eq tip 'G)
           (eq tip 'C)
           (eq tip 'T)))

Now we define a function that traverses the tree, checking that every
tip is valid.

     (defun valid-tree-serial (tree)
       (declare (xargs :guard t))
       (if (atom tree)
           (valid-tip tree)
         (and (valid-tree-serial (car tree))
              (valid-tree-serial (cdr tree)))))

We also define a parallel version.

     (defun valid-tree-parallel (tree)
       (declare (xargs :guard t))
       (if (atom tree)
           (valid-tip tree)
         (pand (valid-tree-parallel (car tree))
               (valid-tree-parallel (cdr tree)))))

Before we can time the functions, we need to create test trees.  We have
found that test trees need to be approximately 1 gigabyte before we
clearly see speedup, and we make them asymmetric to demonstrate the
ability of our implementation to adapt to asymmetric data.  We can
create the trees with the execution of the following forms.

     (defun make-valid-binary-tree (x)
       (declare (xargs :mode :program))
       (if (< x 0)
           (cons (cons 'C 'G) (cons 'A 'T))
         (cons (make-valid-binary-tree (- x 2)) ; 2 to make asymmetric
               (make-valid-binary-tree (- x 1)))))

     (defconst *valid-tree* (make-valid-binary-tree 30)) ; takes awhile
     (defconst *invalid-tree* (cons *valid-tree* nil)) ; nil is invalid tip

We can time our functions with the forms:

     (time$ (valid-tree-serial *valid-tree*))
     (time$ (valid-tree-parallel *valid-tree*))

Unfortunately, the serial version runs faster than the parallelism
version; however, there is more to this story.

Demonstrating Early Termination with an Invalid Tree

Now observe this magic:

     (time$ (valid-tree-serial   *invalid-tree*))
     (time$ (valid-tree-parallel *invalid-tree*))

The serial version took awhile, while the parallel version finished
almost immediately.  The test for validation was split into testing the
car and the cdr of the *invalid-tree* root, and since the cdr was equal
to nil, its test returned immediately.  This immediate return quickly
interrupted the computation associated with the car, and returned the
result.

Granularity with Pand

We can also define a parallel version with a granularity form:

     (defun valid-tree-parallel (tree depth)
       (declare (xargs :guard (natp depth)))
       (if (atom tree)
           (valid-tip tree)
         (pand
          (declare (granularity (< depth 5)))
          (valid-tree-parallel (car tree) (1+ depth))
          (valid-tree-parallel (cdr tree) (1+ depth)))))

We can test this form by executing our previous forms.  You will
probably find some speedup on a machine with several cores available,
but more speedup can likely be obtained with an expensive test on the
leaves in place of valid-tip.

     (time$ (valid-tree-serial   *valid-tree*))
     (time$ (valid-tree-parallel *valid-tree* 0))

Introducing Por

Por can be used in the same way as pand, but with early termination
occurring when an argument evaluates to a non-nil value, in which case
the value returned is t.  Finally, por also supports the use of a
granularity form.

PARGS    parallel evaluation of arguments in a function call

     Example Forms:
     (pargs (binary-+ (fibonacci (- x 1)) (fibonacci (- x 2))))

     (pargs (declare (granularity (> x 35)))
            (binary-+ (fibonacci (- x 1)) (fibonacci (- x 2))))

     General Form:
     (pargs (declare (granularity expr)) ; optional granularity declaration
            (f arg1 ... argN))

where N >= 0 and each argi and expr are arbitrary terms.  Logically,
pargs is just the identity macro, in the sense that the above forms can
logically be replaced by (f arg1 ... argN).  However, this pargs form
may parallelize the evaluation of arguments arg1 through argN before
applying function f to those results.  If the above granularity
declaration is present, then its expression (expr above) is first
evaluated, and if the result is nil, then such parallelism is avoided.
Even if parallelism is not thus avoided, parallelism may be limited by
available resources.

Since macros can change expressions in unexpected ways, it is illegal
to call pargs on a form that is a macro call.  To parallelize
computation of arguments to a macro, see PLET.

See PARALLELISM-AT-THE-TOP-LEVEL for restrictions on evaluating
parallelism primitives from within the ACL2 top-level loop.

PLET    parallel version of let

     Example Forms:
     (plet ((a (fibonacci (- x 1)))
            (b (fibonacci (- x 2))))
           (+ a b))

     (plet (declare (granularity (> x 35)))
           ((a (fibonacci (- x 1)))
            (b (fibonacci (- x 2))))
           (+ a b))

     General Form:
     (plet (declare (granularity expr)) ; optional granularity declaration
           ((var1 val1)
            ...
            (varN valN))
           (declare ...) ... (declare ...) ; optional declarations
           body)

The syntax of plet is identical to the syntax of let, except that plet
permits an optional granularity declaration in the first argument
position; see GRANULARITY.  In the logic a call of plet
macroexpands to the corresponding call of let, where the granularity
declaration (if any) is dropped.

Plet cause the evaluation of each vali above to be done in parallel
before processing the body.  If the above granularity declaration is
present, then its expression (expr above) is first evaluated, and if the
result is nil, then such parallelism is avoided.  Even if parallelism is
not thus avoided, parallelism may be limited by available resources.

See PARALLELISM-AT-THE-TOP-LEVEL for restrictions on evaluating
parallelism primitives from within the ACL2 top-level loop.

POR    parallel, Boolean version of or

     Example Forms:
     (por (subsetp-equal x y)
          (subsetp-equal y x))

     (por (declare
           (granularity
            (and (> (length x) 500)
                 (> (length y) 500))))
           (subsetp-equal x y)
           (subsetp-equal y x))

     General Form:
     (por (declare (granularity expr)) ; optional granularity declaration
          arg1 ... argN)

where N >= 0 and each argi and expr are arbitrary terms.

Por evaluates its arguments in parallel.  It returns a Boolean result:
t if any argument evaluates to non-nil, else nil.  Note that while or
returns the first non-nil value from evaluating its arguments
left-to-right (if any such value is not nil) por always returns a
Boolean result, in support of efficiency (see EARLY-TERMINATION)
in light of the nondeterministic order in which argument values are
returned.

Another difference between por and or is that for a call of por, even
if the an argument's value is not nil, a subsequent argument may be
evaluated.  See PAND for a discussion of the analogous property
of pand.  In particular, guards generated from calls of por may not
assume for an argument that the preceding arguments evaluated to nil.

See PARALLELISM-TUTORIAL for another example.  Also see
PARALLELISM-AT-THE-TOP-LEVEL for restrictions on evaluating
parallelism primitives from within the ACL2 top-level loop.  Finally
see EARLY-TERMINATION to read how por can offer more efficiency
than or by avoiding evaluation of some of its arguments.

SET-PARALLEL-EVALUATION    enabling or disabling parallel evaluation

See PARALLEL and see PARALLELISM-TUTORIAL for an
introduction to parallel evaluation in ACL2 using parallelism
primitives pand, por, plet, and pargs.

     General Forms:
     (set-parallel-evaluation nil) ; default for images not built for parallelism
     (set-parallel-evaluation t)   ; default for images built for parallelism
     (set-parallel-evaluation :bogus-parallelism-ok)

Set-parallel-evaluation takes an argument that specifies the enabling or
disabling of parallel evaluation.  However, calls of parallelism
primitives made explicitly in the ACL2 top-level loop, as opposed to
inside function bodies, will never cause parallel evaluation; see
PARALLELISM-AT-THE-TOP-LEVEL.  Parallel evaluation is determined by
the value of the argument to set-parallel-evaluation, as follows.

Value t:
All parallelism primitives used in bodies of function definitions are
given the opportunity to execute in parallel.  However, the use of
parallelism primitives directly in the ACL2 top-level loop causes an
error.

Value :bogus-parallelism-ok:
Parallel evaluation is enabled, as for value t.  However, the use of
parallelism primitives directly in the ACL2 top-level loop does not
cause an error, but rather, simply results in serial evaluation for
these primitives.

Value nil:
All parallelism primitives will degrade to their serial equivalents,
include their calls made directly in the ACL2 top-level loop, which
does not cause an error.

PROGRAMMING    built-in ACL2 functions

The built-in ACL2 functions that one typically uses in writing programs
are listed below.  See their individual documentations.  We do not
bother to document some of the more obscure functions provided by ACL2
that do not correspond to functions of Common Lisp.

Related topics other than immediate subtopics:

See any documentation for Common Lisp for more details on many of these
functions.

*    multiplication macro

* is really a macro that expands to calls of the function binary-*.  So
for example

     (* x y 4 z)

represents the same term as

     (binary-* x (binary-* y (binary-* 4 z))).

See BINARY-*.

* is a Common Lisp function.  See any Common Lisp documentation for
more information.

*STANDARD-CI*    an ACL2 character-based analogue of CLTL's *standard-input*

The value of the ACL2 constant *standard-ci* is an open character input
channel that is synonymous to Common Lisp's *standard-input*.

ACL2 character input from *standard-ci* is actually obtained by reading
characters from the stream named by Common Lisp's *standard-input*.
That is, by changing the setting of *standard-input* in raw Common Lisp
you can change the source from which ACL2 reads on the channel
*standard-ci*.  See *STANDARD-CO*.

*STANDARD-CO*    the ACL2 analogue of CLTL's *standard-output*

The value of the ACL2 constant *standard-co* is an open character
output channel that is synonymous to Common Lisp's *standard-output*.

ACL2 character output to *standard-co* will go to the stream named by
Common Lisp's *standard-output*.  That is, by changing the setting of
*standard-output* in raw Common Lisp you can change the actual
destination of ACL2 output on the channel named by *standard-co*.
Observe that this happens without changing the logical value of
*standard-co* (which is some channel symbol).  Changing the setting of
*standard-output* in raw Common Lisp essentially just changes the map
that relates ACL2 to the physical world of terminals, files, etc.

To see the value of this observation, consider the following.  Suppose
you write an ACL2 function which does character output to the constant
channel *standard-co*.  During testing you see that the output actually
goes to your terminal.  Can you use the function to output to a file?
Yes, if you are willing to do a little work in raw Common Lisp: open a
stream to the file in question, set *standard-output* to that stream,
call your ACL2 function, and then close the stream and restore
*standard-output* to its nominal value.  Similar observations can be
made about the two ACL2 input channels, *standard-oi* and
*standard-ci*, which are analogues of *standard-input*.

Another reason you might have for wanting to change the actual streams
associated with *standard-oi* and *standard-co* is to drive the ACL2
top-level loop, ld, on alternative input and output streams.  This end
can be accomplished easily within ACL2 by either calling ld on the
desired channels or file names or by resetting the ACL2 state global
variables 'standard-oi and 'standard-co which are used by ld.  See
STANDARD-OI and see STANDARD-CO.

*STANDARD-OI*    an ACL2 object-based analogue of CLTL's *standard-input*

The value of the ACL2 constant *standard-oi* is an open object input
channel that is synonymous to Common Lisp's *standard-input*.

ACL2 object input from *standard-oi* is actually obtained by reading
from the stream named by Common Lisp's *standard-input*.  That is, by
changing the setting of *standard-input* in raw Common Lisp you can
change the source from which ACL2 reads on the channel *standard-oi*.
See *STANDARD-CO*.

+    addition macro

+ is really a macro that expands to calls of the function binary-+.  So
for example

     (+ x y 4 z)

represents the same term as

     (binary-+ x (binary-+ y (binary-+ 4 z))).

See BINARY-+.

-    macro for subtraction and negation

See BINARY-+ for addition and see UNARY-- for negation.

Note that - represents subtraction as follows:

     (- x y)

represents the same term as

     (+ x (- y))

which is really

     (binary-+ x (unary-- y)).

Also note that - represents arithmetic negation as follows:

     (- x)

expands to

     (unary-- x).

/    macro for division and reciprocal

See BINARY-* for multiplication and see UNARY-/ for
reciprocal.

Note that / represents division as follows:

     (/ x y)

represents the same term as

     (* x (/ y))

which is really

     (binary-* x (unary-/ y)).

Also note that / represents reciprocal as follows:

     (/ x)

expands to

     (unary-/ x).

/ is a Common Lisp macro.  See any Common Lisp documentation for more
information.

/=    test inequality of two numbers

(/= x y) is logically equivalent to (not (equal x y)).

Unlike equal, /= has a guard requiring both of its arguments to be
numbers.  Generally, /= is executed more efficiently than a combination
of not and equal.

For a discussion of the various ways to test against 0, See
ZERO-TEST-IDIOMS.

/= is a Common Lisp function.  See any Common Lisp documentation for
more information.

1+    increment by 1

(1+ x) is the same as (+ 1 x).  See +.

1+ is a Common Lisp function.  See any Common Lisp documentation for
more information.

1-    decrement by 1

(1- x) is the same as (- x 1).  See -.

1- is a Common Lisp function.  See any Common Lisp documentation for
more information.

<    less-than

Completion Axiom:

     (equal (< x y)
            (if (and (rationalp x)
                     (rationalp y))
                (< x y)
              (let ((x1 (if (acl2-numberp x) x 0))
                    (y1 (if (acl2-numberp y) y 0)))
                (or (< (realpart x1) (realpart y1))
                    (and (equal (realpart x1) (realpart y1))
                         (< (imagpart x1) (imagpart y1)))))))

Guard for (< x y):

     (and (rationalp x) (rationalp y))

Notice that like all arithmetic functions, < treats non-numeric inputs
as 0.

This function has the usual meaning on the rational numbers, but is
extended to the complex rational numbers using the lexicographic order:
first the real parts are compared, and if they are equal, then the
imaginary parts are compared.

<=    less-than-or-equal test

<= is a macro, and (<= x y) expands to the same thing as (not (< y x)).
See <.

<= is a Common Lisp function.  See any Common Lisp documentation for
more information.

=    test equality of two numbers

(= x y) is logically equivalent to (equal x y).

Unlike equal, = has a guard requiring both of its arguments to be
numbers.  Generally, = is executed more efficiently than equal.

For a discussion of the various ways to test against 0, See
ZERO-TEST-IDIOMS.

= is a Common Lisp function.  See any Common Lisp documentation for
more information.

>    greater-than test

> is a macro, and (> x y) expands to the same thing as (< y x).  See
<.

> is a Common Lisp function.  See any Common Lisp documentation for
more information.

>=    greater-than-or-equal test

>= is a macro, and (>= x y) expands to the same thing as (not (< x y)).
See <.

>= is a Common Lisp function.  See any Common Lisp documentation for
more information.

ABS    the absolute value of a real number

(Abs x) is -x if x is negative and is x otherwise.

The guard for abs requires its argument to be a rational (real, in
ACL2(r)) number.

Abs is a Common Lisp function.  See any Common Lisp documentation for
more information.

From "Common Lisp the Language" page 205, we must not allow complex x
as an argument to abs in ACL2, because if we did we would have to
return a number that might be a floating point number and hence not an
ACL2 object.

ACL2-NUMBERP    recognizer for numbers

(acl2-numberp x) is true if and only if x is a number, i.e., a rational
or complex rational number.

ACL2-USER    a package the ACL2 user may prefer

This package imports the standard Common Lisp symbols that ACL2
supports and also a few symbols from package "ACL2" that are commonly
used when interacting with ACL2.  You may prefer to select this as your
current package so as to avoid colliding with ACL2 system names.

This package imports the symbols listed in
*common-lisp-symbols-from-main-lisp-package*, which contains hundreds
of CLTL function and macro names including those supported by ACL2 such
as cons, car, and cdr.  It also imports the symbols in *acl2-exports*,
which contains a few symbols that are frequently used while interacting
with the ACL2 system, such as implies, defthm, and rewrite.  It imports
nothing else.

Thus, names such as alistp, member-equal, and type-set, which are
defined in the "ACL2" package are not present here.  If you find
yourself frequently colliding with names that are defined in "ACL2" you
might consider selecting "ACL2-USER" as your current package (see
IN-PACKAGE).  If you select "ACL2-USER" as the current package, you
may then simply type member-equal to refer to acl2-user::member-equal,
which you may define as you see fit.  Of course, should you desire to
refer to the "ACL2" version of member-equal, you will have to use the
"ACL2::" prefix, e.g., acl2::member-equal.

If, while using "ACL2-USER" as the current package, you find that there
are symbols from "ACL2" that you wish we had imported into it (because
they are frequently used in interaction), please bring those symbols to
our attention.  For example, should union-theories and universal-theory
be imported?  Except for stabilizing on the "frequently used" names
from "ACL2", we intend never to define a symbol whose
symbol-package-name is "ACL2-USER".

ACONS    constructor for association lists

(Acons key datum alist) equals the result of consing the pair (cons key
datum) to the front of the association list alist.

(Acons key datum alist) has a guard of (alistp alist).  Acons is a
Common Lisp function.  See any Common Lisp documentation for more
information.

ADD-TO-SET-EQ    add a symbol to a list

For a symbol x and a true list lst, (add-to-set-eq x lst) is the result
of consing x on to the front of lst, unless x is already a member of
lst, in which case it equals lst.

(add-to-set-eq x lst) has a guard that lst is a true list and moreover,
either x is a symbol or lst is a list of symbols.

ADD-TO-SET-EQL    add an object to a list

For an object x and a true list lst, (add-to-set-eql x lst) is the
result of consing x on to the front of lst, unless x is already a
member of lst, in which case it equals lst.

(add-to-set-eql x lst) has a guard that lst is a true list and
moreover, either x is eqlablep or lst is an eqlable-listp.

ADD-TO-SET-EQUAL    add an object to a list

For an object x and a true list lst, (add-to-set-equal x lst) is the
result of consing x on to the front of lst, unless x is already a
member of lst, in which case it equals lst.

(add-to-set-equal x lst) has a guard that lst is a true list.

ALISTP    recognizer for association lists

(alistp x) is true if and only if x is a list of cons pairs.

(alistp x) has a guard of t.

ALLOCATE-FIXNUM-RANGE    set aside fixnums in GCL

(Allocate-fixnum-range fixnum-lo fixnum-hi) causes Gnu Common Lisp
(GCL) to create a persistent table for the integers between fixnum-lo
and fixnum-hi (both bounds inclusive). This table is referenced first
when any integer is boxed and the existing box in the table is used if
the integer is in bounds.  This can speed up GCL considerably by
avoiding wasteful fixnum boxing.  Here, fixnum-lo and fixnum-hi should
be fixnums, more specifically of type (signed-byte 30), with fixnum-lo
<= fixnum-hi.

When this function is executed in a Lisp implementation other than GCL,
it has no side effect.  This function always returns nil.

ALPHA-CHAR-P    recognizer for alphabetic characters

(Alpha-char-p x) is true if and only if x is a alphabetic character,
i.e., one of the characters #a, #b, ..., #z, #A, #B, ..., #Z.

The guard for alpha-char-p requires its argument to be a character.

Alpha-char-p is a Common Lisp function.  See any Common Lisp
documentation for more information.

ALPHORDER    total order on atoms

Alphorder is a non-strict total order, a "less than or equal," on
atoms.  By "non-strict total order" we mean a function that always
returns t or nil and satisfies the following properties.

     o Antisymmetry:  XrY & YrX -> X=Y

     o Transitivity:  XrY & YrZ -> XrZ

     o Trichotomy:  XrY v YrX

Also see LEXORDER, which extends alphorder to all objects.

(Alphorder x y) has a guard of (and (atom x) (atom y)).

Within a single type: rationals are compared arithmetically, complex
rationals are compared lexicographically, characters are compared via
their char-codes, and strings and symbols are compared with alphabetic
ordering.  Across types, rationals come before complexes, complexes
come before characters, characters before strings, and strings before
symbols.  We also allow for "bad atoms," i.e., atoms that are not legal
Lisp objects but make sense in the ACL2 logic; these come at the end,
after symbols.

AND    conjunction

And is the macro for conjunctions.  And takes any number of arguments.
And returns nil if one of the arguments is nil, but otherwise returns
the last argument.  If there are no arguments, and returns t.

And is a Common Lisp macro.  See any Common Lisp documentation for more
information.

APPEND    concatenate two or more lists

Append, which takes two or more arguments, expects all the arguments
except perhaps the last to be true (null-terminated) lists.  It returns
the result of concatenating all the elements of all the given lists
into a single list.  Actually, in ACL2 append is a macro that expands
into calls of the binary function binary-append.

Append is a Common Lisp function.  See any Common Lisp documentation
for more information.

ASH    arithmetic shift operation

(ash i c) is the result of taking the two's complement representation
of the integer i and shifting it by c bits:  shifting left and padding
with c 0 bits if c is positive, shifting right and dropping (abs c)
bits if c is negative, and simply returning i if c is 0.

The guard for ash requires that its arguments are integers.

Ash is a Common Lisp function.  See any Common Lisp documentation for
more information.

ASSERT$    cause a hard error if the given test is false

     General Form:
     (assert$ test form)

where test returns a single value and form is arbitrary.  Semantically,
this call of assert$ is equivalent to form.  However, it causes a hard
error (using illegal) if the value of test is nil.

ASSOC    look up key in association list, using eql as test

(Assoc x alist) is the first member of alist whose car is x, or nil if
no such member exists.

(Assoc x alist) is provably the same in the ACL2 logic as (assoc-equal
x alist).  It has a stronger guard than assoc-equal because it uses eql
to test whether x is equal to the car of a given member of alist.  Its
guard requires that alist is an alistp, and moreover, either (eqlablep
x) or all cars of members of alist are eqlablep.  See
ASSOC-EQUAL and see ASSOC-EQ.

Assoc is a Common Lisp function.  See any Common Lisp documentation for
more information.  Since ACL2 functions cannot take keyword arguments
(though macros can), the ACL2 functions assoc-equal and assoc-eq are
defined to correspond to calls of the Common Lisp function assoc whose
keyword argument :test is equal or eq, respectively.

ASSOC-EQ    look up key in association list, using eq as test

(Assoc-eq x alist) is the first member of alist whose car is x, or nil
if no such member exists.

(Assoc-eq x alist) is provably the same in the ACL2 logic as (assoc x
alist) and (assoc-equal x alist), but it has a stronger guard because
it uses eq for a more efficient test for whether x is equal to a given
key of alist.  Its guard requires that alist is an association list
(see ALISTP), and moreover, either x is a symbol or all keys of
alist are symbols, i.e., alist is a symbol-alistp.

ASSOC-EQUAL    look up key in association list

(Assoc-equal x alist) is the first member of alist whose car is x, or
nil if no such member exists.

(Assoc-equal x alist) has a guard of (alistp alist), and returns the
first member of alist whose car is x, or nil if no such member exists.
Thus, assoc-equal has the same functionality as the Common Lisp
function assoc, except that it uses the equal function to test whether
x is the same as each successive `key' of alist.  See ASSOC and
see ASSOC-EQ.

ASSOC-KEYWORD    look up key in a keyword-value-listp

If l is a list of even length of the form (k1 a1 k2 a2 ... kn an),
where each ki is a keyword, then (assoc-keyword key l) is the first
tail of l starting with key if key is some ki, and is nil otherwise.

The guard for (assoc-keyword key l) is (keyword-value-listp l).