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

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.

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

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@lists.cc.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@lists.cc.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.  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>.

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

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.

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.