This is documentation for ACL2 Version 3.0
Copyright (C) 2006  University of Texas at Austin

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

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

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

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

OOPS    undo a :u or :ubt

The keyword command :oops will undo the most recent :ubt (or :u, which
we here consider just another :ubt).  A second :oops will undo the next
most recent :ubt, a third will undo the :ubt before that one, and a
fourth :oops will return the logical world to its configuration before
the first :oops.

Consider the logical world (see WORLD) that represents the
current extension of the logic and ACL2's rules for dealing with it.
The :ubt and :u commands "roll back" to some previous world (see
UBT).  Sometimes these commands are used to inadvertently undo useful
work and user's wish they could "undo the last undo."  That is the
function provided by :oops.

:Oops is best described in terms of an implementation.  Imagine a ring
of four worlds and a marker (*) indicating the current ACL2 world:

                  *
                w0
              /    \
            w3      w1
              \    /
                w2

This is called the "kill ring" and it is maintained as follows.  When
you execute an event the current world is extended and the kill ring is
not otherwise affected.  When you execute :ubt or :u, the current world
marker is moved one step counterclockwise and that world in the ring is
replaced by the result, say w0', of the :ubt or :u.

                w0
              /    \
           *w0'     w1
              \    /
                w2

If you were to execute events at this point, w0' would be extended and
no other changes would occur in the kill ring.

When you execute :oops, the marker is moved one step clockwise.  Thus
the kill ring becomes

                  *
                w0
              /    \
            w0'     w1
              \    /
                w2

and the current ACL2 world is w0 once again.  That is, :oops "undoes"
the :ubt that produced w0' from w0.  Similarly, a second :oops will move
the marker to w1, undoing the undo that produced w0 from w1.  A third
:oops makes w2 the current world.  Note however that a fourth :oops
restores us to the configuration previously displayed above in which w0'
has the marker.

In general, the kill ring contains the current world and the three most
recent worlds in which a :ubt or :u were done.

While :ubt may appear to discard the information in the events undone,
we can see that the world in which the :ubt occurred is still available.
No information has been lost about that world.  But :ubt does discard
information!  :Ubt discards the information necessary to recover from
the third most recent ubt!  An :oops, on the other hand, discards no
information, it just selects the next available world on the kill ring
and doing enough :oopses will return you to your starting point.

We can put this another way.  You can freely type :oops and inspect the
world that you thus obtain with :pe, :pc, and other history commands.
You can repeat this as often as you wish without risking the permanent
loss of any information.  But you must be more careful typing :ubt or
:u.  While :oops makes :ubt seem "safe" because the most recent :ubt can
always be undone, information is lost when you execute :ubt.

We note that :ubt and :u may remove compiled definitions (except in
Lisps such as OpenMCL, in which functions are always compiled).  When
the original world is restored using :oops, restored functions will not
generally be compiled, though the user can remedy this situation; see
COMP.

Finally, we note that our implementation of oops can use a significant
amount of memory, because of the saving of old logical worlds.  Most
users are unlikely to experience a memory problem, but if you do, then
you may want to disable oops by evaluting (reset-kill-ring 0 state); see
RESET-KILL-RING.

PBT    print the commands back through a command descriptor

     Examples:
     :pbt :max      ; print back through the most recent command
     :pbt :x        ; print back through the most recent command
     :pbt fn        ; print back through the introduction of fn
     :pbt 5         ; print back through the fifth command executed
     :pbt (:x -4)   ; print back through the most recent five commands

See COMMAND-DESCRIPTOR.

Pbt takes one argument, a command descriptor, and prints the commands
from :max (aka :x) through the one described.  See
COMMAND-DESCRIPTOR for a description of what a command descriptor is.
See PC for a description of the format used to display commands.
Pbt will print the commands that ubt will undo.

PC    print the command described by a command descriptor

     Examples:
     :pc 3    ; print the third command executed
     :pc :max ; print the most recent command
     :pc :x   ; print the most recent command
     :pc fn   ; print the command that introduced fn

See COMMAND-DESCRIPTOR.

Pc takes one argument, a command descriptor, and prints the command
identified by that descriptor.  See COMMAND-DESCRIPTOR.  For
example

     ACL2 !>:pc foo
      LVd     52 (DEFUN FOO (X) X)

Pc always prints a space first, followed by three (possibly blank)
characters ("LVd" above) explained below.  Then pc prints the command
number, a number uniquely identifying the command's position in the
sequence of commands since the beginning of the user's session.
Finally, the command itself is printed.

While pc always prints a space first, some history commands, for example
:pcs and :pe, use the first column of output to delimit a region of
commands or to point to a particular event within a command.

For example, :pcs 52 54 will print something like

     /LVd     52 (DEFUN FOO (X) X)
      LV      53 (DEFUN BAR (X) (CONS X X))
     \        54 (DEFTHM FOO-BAR (EQUAL (CAR (BAR X)) (FOO X)))
               : ...
             127 (DEFUN LATEST (X) X)

Here, the two slash characters in the first column are intended to
suggest a bracket delimiting commands 52 through 54.  The last command
printed by pcs is always the most recent command, i.e., the command at
:here, and is separated from the rest of the display by an elipsis if
some commands are omitted.

Similarly, the :pe command will print a particular event within a
command block and will indicate that event by printing a ">" in the
first column.  The symbol is intended to be an arrow pointing at the
event in question.

For example, :pe true-listp-app might print:

              1 (INCLUDE-BOOK "list-book")
                 \
     >           (DEFTHM TRUE-LISTP-APP
                         (EQUAL (TRUE-LISTP (APP A B)) (TRUE-LISTP B)))

using the arrow to indicate the event itself.  The slash printed to
connect the command, include-book, with the event, defthm, is intended
to suggest a tree branch indicating that the event is inferior to (and
part of) the command.

The mysterious three characters sometimes preceding a command have the
following interpretations.  The first two have to do with the function
symbols introduced by the command and are blank if no symbols were
introduced.

At any time we can classify our function symbols into three disjoint
sets, which we will here name with characters.  The "P" functions are
those in :program mode.  The "L" functions are those in :logic mode
whose guards have not been verified.  The "V" functions are those in
:logic mode whose guards have been verified.  Note that
verify-termination and verify-guards cause function symbols to be
reclassified.  If a command introduces function symbols then the first
mysterious character indicates the class of the symbols at the time of
introduction and the second character indicates the current class of the
symbols (if the current class is different from the introductory class).

Thus, the display

      PLd     52 (DEFUN FOO (X) X)

tells us that command 52 introduced a :program function but that some
command after 52 changed its mode to :logic and that the guards of foo
have not been verified.  That is, foo's termination has been verified
even though it was not verified as part of the command that introduced
foo.  Had a subsequent command verified the guards of foo, the display
would contain a V where the L is.

The display

      P d     52 (DEFUN FOO (X) X)

indicates that foo was introduced in :program mode and still is in that
mode.

The third character indicates the enabled/disabled status of the runes
introduced by the command.  If the status character is blank then all
the runes (if any) introduced are enabled.  If the status character is
"D" then some runes were introduced and they are all disabled.  If the
status character is "d" then at least one, but not all, of the runes
introduced is disabled.  Thus, in the display

      L d     52 (DEFUN FOO (X) X)

we see that some rune introduced by command 52 is disabled.  As noted in
the documentation for rune, a defun command introduces many runes, e.g.,
the axiomatic definition rule, (:definition fn), the executable
counterpart rule, (:executable-counterpart fn), and type-prescriptions,
(:type-prescription fn).  The display above does not say which of the
runes based on foo is disabled, but it does tell us one of them is; see
DISABLEDP for how to obtain the disabled runes for a given
function symbol.

PCB    print the command block described by a command descriptor

     Examples:
     :pcb :max ; print the most recent command block
     :pcb :x   ; print the most recent command block
     :pcb fn   ; print the command block that introduced fn
     :pcb 5    ; print the fifth command block

See COMMAND-DESCRIPTOR.

Pcb takes one argument, a command descriptor, and prints the command
block of the command described.  See COMMAND-DESCRIPTOR for
details of command descriptors.  See PC for description of the
format in which commands are displayed.  The command block of a command
consists of the command itself and all of the events it created.  If the
command created a single event and that event is in fact the command
(i.e., if the command typed was just an event such as a defun or defthm
rather than a macro that expanded to some event forms), then pcb just
prints the command.  Pcb sketches command and all of the events it
created, rather than printing them fully.  If you wish to see just the
command, in its entirety, use pc.  If you wish to see one of the events
within the block, in its entirety, use pe.  If you wish to see the
command sketched and all of the events it created, in their entirety,
use pcb!.

PCB!    print in full the command block described by a command descriptor

     Examples:
     :pcb! :max ; print the most recent command block
     :pcb! :x   ; print the most recent command block
     :pcb! fn   ; print the command block that introduced fn
     :pcb! 5    ; print the fifth command block

See COMMAND-DESCRIPTOR.

Pcb! takes one argument, a command descriptor, and prints the command
block of the command described.  Unlike pcb, pcb! prints the event forms
in full; see PCB for details.

PCS    print the sequence of commands between two command descriptors

     Examples:
     :pcs 1 5              ; print commands 1 through 5
     :pcs 5 1              ; same as above
     :pcs :x (:x -3)       ; print the 3 most recently executed commands
     :pcs fn assoc-of-fn   ; print the commands between the one that introduced
                           ; fn and the one that introduced assoc-of-fn

Pcs takes two arguments, both of which are command descriptors, and
prints the commands between them with pc.  The order of the two
descriptors is irrelevant.  See COMMAND-DESCRIPTOR for a
description of command descriptors.  See PC for a description of
the format in which commands are displayed.

PE    print the events named by a logical name

     Example:
     :pe fn   ; sketches the command that introduced fn and
              ; prints in full the event within it that created fn.

See LOGICAL-NAME.

Pe takes one argument, a logical name, and prints in full the event
corresponding to the name.  Pe also sketches the command responsible for
that event if the command is different from the event itself.  See
PC for a description of the format used to display a command.  To
remind you that the event is inferior to the command, i.e., you can only
undo the entire command, not just the event, the event is indented
slightly from the command and a slash (meant to suggest a tree branch)
connects them.

If the given logical name corresponds to more than one event, then :pe
will print the above information for every such event.  Here is an
example. of such behavior.

     ACL2 !>:pe nth
           -4270  (ENCAPSULATE NIL ...)
                  \
     >V            (VERIFY-TERMINATION NTH)

     Additional events for the logical name NTH:
      PV   -4949  (DEFUN NTH (N L)
                         "Documentation available via :doc"
                         (DECLARE (XARGS :GUARD (AND (INTEGERP N)
                                                     (>= N 0)
                                                     (TRUE-LISTP L))))
                         (IF (ENDP L)
                             NIL
                             (IF (ZP N)
                                 (CAR L)
                                 (NTH (- N 1) (CDR L)))))
     ACL2 !>

PE!    deprecated (see PE)

Please see PE.  :Pe now has the functionality formerly provided
by :pe!.

PF    print the formula corresponding to the given name

     Examples:
     :pf (:definition fn) ; prints the definition of fn as an equality
     :pf fn               ; same as above

     :pf (:rewrite foo)   ; prints the statement of the rewrite rule foo
     :pf foo              ; same as above

pf takes one argument, an event name or a rune, and prints the formula
associated with name.  If the argument is the name of a macro associated
with a function name by macro-aliases-table, then the function name is
used as the argument.

PL    print the rules for the given name or term

     Examples:
     :pl foo     ; prints rules that rewrite some call of foo
     :pl (+ x y) ; prints rules that rewrite (+ x y)

Pl takes one argument, a function symbol or a term.  If the argument is
a function symbol, :pl displays the rules that rewrite some term whose
top function symbol is the given one.  Otherwisel, :pl displays the
rules that rewrite that term.

The kinds of rules printed by :pl are rewrite rules, definition rules,
and meta rules.

PR    print the rules stored by the event with the given name

     Examples:

     :pr fn ; prints the rules from the definition of fn (including any
            ; :type-prescription rule and :definition rule)

     :pr assoc-append ; if assoc-append is a rewrite rule, prints that rule

Also see PR!, which is similar but works at the command level
instead of at the event level, and see PL, which displays all
rewrite rules for calls of fn, not just those introduced at definition
time.

Pr takes one argument, a logical name, and prints the rules associated
with it.  In each case it prints the rune, the current enabled/disabled
status, and other appropriate fields from the rule.  It may be helpful
to read the documentation for various kinds of rules in order to
understand the information printed by this command.  For example, the
information printed for a linear rule might be:

       Rune:     (:LINEAR ABC)
       Status:   Enabled
       Hyps:     ((CONSP X))
       Concl:    (< (ACL2-COUNT (CAR X)) (ACL2-COUNT X))
       Max-term: (ACL2-COUNT (CAR X))
       Backchain-limit-lst:    (3)

The hyps and concl fields for this rule are fairly self-explanatory, but
it is useful to see LINEAR to learn about maximal terms (which,
as one might guess, are stored under "Max-term").

Currently, this function does not print congruence rules or equivalence
rules.

The expert user might also wish to use find-rules-of-rune.  See
FIND-RULES-OF-RUNE.

PR!    print rules stored by the command with a given command descriptor

     Examples:

     :pr! fn ; prints the rules from the definition of fn (including any
             ; :type-prescription rule and :definition rule), as well as all other
             ; rules created by the command that created by fn (which could be
             ; many rules if, for example, fn was defined by an include-book
             ; command).

     :pr! :max ; prints all the rules stored by the most recent command

Also see PR, which is similar but works at the event level
instead of at the command level.

Pr takes one argument, a command descriptor, and prints the rules
created by the corresponding event.  In each case it prints the rune,
the current enabled/disabled status, and other appropriate fields from
the rule.  See PR for further details.

PUFF    replace a compound command by its immediate subevents

     Example Forms:
     ACL2 !>:puff :max
     ACL2 !>:puff :x
     ACL2 !>:puff 15
     ACL2 !>:puff "book"

     General Form:
     :puff cd

where cd is a command descriptor (see COMMAND-DESCRIPTOR) for a
"puffable" command (see below).  Puff replaces the command at cd by the
immediate subevents of the command, executed as commands.  Puff then
prints, using pcs, the puffed region.

A command is "puffable" if it is an encapsulate command, an include-book
command, or any command other than those consisting of a single
primitive event.  For example, since defun is a primitive event, a defun
command is not puffable.  But a macro form that expands into several
defun events is puffable.  The only primitive event commands that are
puffable are encapsulate and include-book commands.  A puffable command
contains (interesting) subevents, namely, the events in the body of the
encapsulate, in the file of the book included, or in the command block.

The puff command "lifts" the immediate subevents of the indicated
command so that they become commands themselves.  The command puff*
recursively puffs the newly introduced commands.  See PUFF*,
which also gives an example illustrating both puff and puff*.  Puff
undoes the command at cd and replaces it by its immediate subevents.
Thus, in general the length of the history grows when a puff command is
executed.  If puff causes an error (see below), the logical world
remains unchanged from its initial configuration.

The intended use of puff is to allow the user access to the events
"hidden" inside compound commands.  For example, while trying to prove
some theorem, p, about a constrained function, fn, one might find that
the encapsulate, cd, that introduced fn failed to include an important
constraint, q.  Without puff, the only way to proceed is to undo back
through cd, create a suitable encapsulate that proves and exports q as
well as the old constraints, re-execute the new encapsulate, re-execute
the events since cd, and then try p again.  Unfortunately, it may be
hard to prove q and additional events may have to be inserted into the
encapsulate to prove it.  It may also be hard to formulate the "right"
q, i.e., one that is provable in the encapsulate and provides the
appropriate facts for use in the proof of p.

Using puff, the user can erase the encapsulate at cd, replacing it by
the events in its body.  Now the formerly constrained function, fn, is
defined as its witness.  The user can experiment with formulations and
proofs of q suitable for p.  Of course, to get into the ultimately
desired state -- where fn is constrained rather than defined and q is
exported by an encapsulate at cd -- the user must ultimately undo back
to cd and carry out the more tedious program described above.  But by
using puff it is easier to experiment.

Similar applications of puff allow the user of a book to expose the
innards of the book as though they had all be typed as commands.  The
user might then "partially undo" the book, keeping only some of the
events in it.

Puff operates as follows.  First, it determines the list of immediate
subevents of the command indicated by cd.  It causes an error if there
is only one subevent and that subevent is identical to the command --
i.e., if the command at cd is a primitive.  Next, puff undoes back
through the indicated command.  This not only erases the command at cd
but all the commands executed after it.  Finally, puff re-executes the
subevents of (the now erased) cd followed by all the commands that were
executed afterwards.

Observe that the commands executed after cd will generally have higher
command numbers than they did before the puff.  For example, suppose 100
commands have been executed and that :puff 80 is then executed.  Suppose
command 80 contains 5 immediate subevents (i.e., is an encapsulation of
five events).  Then, after puffing, command 80 is the first event of the
puffed command, command 81 is the second, and so on; 104 commands appear
to have been executed.

When puffing an encapsulate or include-book, the local commands are
executed.  Note that this will replace constrained functions by their
witnesses.

Finally, it is impossible to puff in the presence of include-book
commands involving certified files that have been altered since they
were included.  To be specific, suppose "arith" is a certified book that
has been included in a session.  Suppose that after "arith" was
included, the source file is modified.  (This might happen if the user
of "arith" is not its author and the author happens to be working on a
new version of "arith" during the same time period.)  Now suppose the
user tries to puff the command that included "arith".  The attempt to
obtain the subevents in "arith" will discover that the check sum of
"arith" has changed and an error will be caused.  No change is made in
the logical world.  A similar error is caused if, in this same
situation, the user tries to puff *any command that occurred before the
inclusion* of "arith"!  That is, puff may cause an error and leave the
world unchanged even if the command puffed is not one involving the
modified book.  This happens because in order to reconstruct the world
after the puffed command, puff must obtain the events in the book and if
the book's source file has changed there is no assurance that the
reconstructed world is the one the user intends.

Warning: We do not detect changes to uncertified books that have been
included and are then puffed or re-included!  The act of including an
uncertified book leaves no trace of the check sum of the book.
Furthermore, the act prints a warning message disclaiming soundness.  In
light of this, :puff quietly "re-"executes the current contents of the
book.

PUFF*    replace a compound command by its subevents

     Example Forms:
     ACL2 !>:puff* :max
     ACL2 !>:puff* :x
     ACL2 !>:puff* 15
     ACL2 !>:puff* "book"

     General Form:
     :puff* cd

where cd is a command descriptor (see COMMAND-DESCRIPTOR) for a
"puffable" command.  See PUFF for the definition of "puffable"
and for a description of the basic act of "puffing" a command.  Puff* is
just the recursive application of puff.  Puff* prints the region puffed,
using pcs.

To puff a command is to replace it by its immediate subevents, each of
which is executed as a command.  To puff* a command is to replace the
command by each of its immediate subevents and then to puff* each of the
puffable commands among the newly introduced ones.

For example, suppose "ab" is a book containing the following

     (in-package "ACL2")
     (include-book "a")
     (include-book "b")

Suppose that book "a" only contained defuns for the functions a1 and a2
and that "b" only contained defuns for b1 and b2.

Now consider an ACL2 state in which only two commands have been
executed, the first being (include-book "ab") and the second being
(include-book "c").  Thus, the relevant part of the display produced by
:pbt 1 would be:

     1 (INCLUDE-BOOK "ab")
     2 (INCLUDE-BOOK "c")

Call this state the "starting state" in this example, because we will
refer to it several times.

Suppose :puff 1 is executed in the starting state.  Then the first
command is replaced by its immediate subevents and :pbt 1 would show:

     1 (INCLUDE-BOOK "a")
     2 (INCLUDE-BOOK "b")
     3 (INCLUDE-BOOK "c")

Contrast this with the execution of :puff* 1 in the starting state.
Puff* would first puff (include-book "ab") to get the state shown above.
But then it would recursively puff* the puffable commands introduced by
the first puff.  This continues recursively as long as any puff
introduced a puffable command.  The end result of :puff* 1 in the
starting state is

     1 (DEFUN A1 ...)
     2 (DEFUN A2 ...)
     3 (DEFUN B1 ...)
     4 (DEFUN B2 ...)
     5 (INCLUDE-BOOK "c")

Observe that when puff* is done, the originally indicated command,
(include-book "ab"), has been replaced by the corresponding sequence of
primitive events.  Observe also that puffable commands elsewhere in the
history, for example, command 2 in the starting state, are not affected
(except that their command numbers grow as a result of the splicing in
of earlier commands).

RESET-KILL-RING    save memory by resetting and perhaps resizing the kill ring used by oops

By default, ACL2 holds on to old logical worlds when you undo commands
(see UBT), as documented elswhere; see OOPS.  You can
free up memory by deleting those old worlds using reset-kill-ring.

     Examples:
     (reset-kill-ring t state)   ; replace each element of the kill ring by nil
     (reset-kill-ring 2 state)   ; create a new kill ring of '(nil nil)
     (reset-kill-ring 0 state)   ; create a new kill ring that is empty
     (reset-kill-ring nil state) ; just return the length of the kill ring

     General form:
     (reset-kill-ring n state)

where n evaluates either to t, to nil, or to a nonnegative integer (a
natp).  If n evaluates to t, it is treated as the length of the current
kill ring.  If n is nil, then the length k of the current kill ring is
returned as a value triple (mv nil k state).  If n is a natp, then the
kill ring is replaced with a list of n nils.

In particular, use (reset-kill-ring 0 state) to avoid saving any old
logical worlds, at the cost of disabling the effect of the oops command.

U    undo last command, without a query

     Example:
     :u

The keyword command :u is the same as :ubt :max, but with related
queries suppressed appropriately.  :Oops will undo the last :u.  See
UBT and see UBT!.

UBT    undo the commands back through a command descriptor

     Examples:
     :ubt :max      ; undo back through the most recent command
                    ; (which just means undo the most recent command)
     :ubt :x        ; same as :ubt :max
     :u             ; same as :ubt :max with no questions asked
     :ubt fn        ; undo back through the introduction of fn
                    ; (including all the other events in fn's block)
     :ubt 5         ; undo back through the fifth command executed
     :ubt (:max -4) ; undo back through the most recent five commands
     :ubt (:x -4)   ; undo back through the most recent five commands

See COMMAND-DESCRIPTOR.

Ubt takes one argument, a command descriptor, and undoes the commands
from :max (aka :x) through the one described.  See
COMMAND-DESCRIPTOR.  Pbt will print the commands that ubt will undo.
:Oops will undo the undo.  See OOPS.

Ubt can cause errors or queries.  To avoid these, see UBT!.

It is important to remember that a command may create several events.
That is, the command that introduces fn1 may also introduce fn2.
Undoing the command that created either of these will undo them both.
The events created by a command constitute the command's "block" and we
can only undo entire blocks.  Use pcb to print the command block of a
command if you wish to see what will be lost by undoing the command.

Ubt will not undo into "prehistory".  :Ubt 1 will undo all of your
commands.  But :ubt -5 will cause an error, warning you that :ubt cannot
undo system initialization.

UBT!    undo commands, without a query or an error

     Example:
     :ubt! :x-4

The keyword command :ubt! is the same as :ubt, but with related queries
suppressed appropriately, and with a guarantee that it is "error-free."
More precisely, the error triple returned by :ubt!  will always have a
first component of nil.  :Oops will undo the last :ubt!.  See
UBT and see U.

MISCELLANEOUS    a miscellany of documented functions and concepts
               (often cited in more accessible documentation)

Perhaps as the system matures this section will become more structured.

ABORT!    to return to the top-level of ACL2's command loop

When (abort!) is evaluated inside of ACL2's command loop, the current
computation is aborted and control returns to the top of the command
loop, exactly as though the user had interrupted and aborted the current
computation.

Logically speaking, (abort!) = nil.  But imagine that it is defined in
such a way that it causes a stack overflow or other resource exhaustion
when called.

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

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.

Accumulated persistence tracking can be turned on or off.  It is
generally off.  When on, the system runs about two times slower 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 is
thus the number of stack frames built while the given rune was on the
stack.

Note that accumulated persistence is not concerned with whether 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 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.

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.

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

ACKNOWLEDGMENTS    some contributors to the well-being of ACL2

The development of ACL2 was initially made possible by funding from the
U. S. Department of Defense, including ARPA and ONR.  We thank all the
organizations that have contributed support, including the following (in
alphabetical order).

     o AMD, for providing significant time over several years for Matt Kaufmann
     to carry out ACL2 research, support, and development

     o Computational Logic, Inc. and its president, Don Good, where the first
     eight years of ACL2 development occurred

     o DARPA

     o Digital Equipment Corporation

     o EDS, which provided some time for Matt Kaufmann's ACL2 work 1998-1999

     o IBM

     o NSF

     o ONR

     o Rockwell Collins

     o SRC

     o Sun Microsystems

     o University of Texas at Austin (in particular support to J Moore
     through the Admiral B. R.  Inman Chair of Computing Theory)

ACL2 was started in August, 1989 by Boyer and Moore working together.
They co-authored the first versions of axioms.lisp and basis.lisp, with
Boyer taking the lead in the formalization of "state" and the most
primitive io functions.  Boyer also had a significant hand in the
development of the early versions of the files interface-raw.lisp and
translate.lisp.  For several years, Moore alone was responsible for
developing the ACL2 system code, though he consulted often with both
Boyer and Kaufmann.  In August, 1993, Kaufmann became jointly
responsible with Moore for developing the system.  Boyer has continued
to provide valuable consulting on an informal basis.

Bishop Brock was the heaviest early user of ACL2, and provided many
suggestions for improvements.  In particular, the :cases and :restrict
hints were his idea; he developed an early version of congruence-based
reasoning for Nqthm; and he helped in the development of some early
books about arithmetic.  In a demonstration of his courage and faith in
us, he pushed for Computational Logic, Inc., to agree to the Motorola
CAP contract -- which required formalizing a commercial DSP in the
untested ACL2 -- and moved to Scottsdale, AZ, to do the work with the
Motorola design team.  His demonstration of ACL2's utility was an
inspiration, even to those of us designing ACL2.

John Cowles also helped in the development of some early books about
arithmetic, and also provided valuable feedback and bug reports.

Other early users of ACL2 at Computational Logic, Inc. helped influence
its development.  In particular, Warren Hunt helped with the port to
Macintosh Common Lisp, and Art Flatau and Mike Smith provided useful
general feedback.

Mike Smith helped develop the Emacs portion of the implementation of
proof trees.

Bill Schelter made some enhancements to akcl (now gcl) that helped to
enhance ACL2 performance in that Common Lisp implementation, and more
generally, responded helpfully to our bug reports.  Camm Maguire has
since provided wonderful gcl support, and has created a Debian package
for ACL2 built on GCL.  We are also grateful to developers of other
Common Lisp implementations.

Kent Pitman helped in our interaction with the ANSI Common Lisp
standardization committee, X3J13.

John Cowles helped with the port to Windows (98) by answering questions
and running tests.

Ruben Gamboa created a modification of ACL2 to allow reasoning about the
real numbers using non-standard analysis.  His work has been
incorporated into the ACL2 distribution; see REAL.

Rob Sumners has made numerous useful suggestions.  In particular, he has
designed and implemented improvements for stobjs and been key in our
development of locally-bound stobjs; see NOTE-2-6.

Robert Krug has designed and implemented many changes in the vicinity of
the linear arithmetic package and its connection to type-set and
rewrite.  He was also instrumental in the development of
extended-metafunctions.

Pete Manolios has made numerous useful suggestions.  In particular, Pete
helped us to organize the first workshop and was a wonderful equal
partner with the two of us (Kaufmann and Moore) in producing the books
that arose from that workshop.  Pete and his student, Daron Vroon,
provided the current implementation of ordinals.

We also thank the contributors to the ACL2 workshops for some suggested
improvements and for the extensive collection of publicly distributed
benchmark problems.  And we thank participants at the ACL2 seminar at
the University of Texas for useful feedback.

*Regarding the documentation:*

     Bill Young wrote significant portions of the ACL2-TUTORIAL section
     of the ACL2 documentation, an important task for which we are
     grateful.  He, Bishop Brock, Rich Cohen, and Noah Friedman read
     over considerable amounts of the documentation, and made many
     useful comments.  Others, particularly Bill Bevier and John Cowles,
     have also made useful comments on the documentation.

     Art Flatau helped develop the ACL2 markup language and translators
     from that language to Texinfo and HTML.  Michael "Bogo" Bogomolny
     created a search engine, beginning with Version 2.6, and for that
     purpose modified the HTML translator to create one file per topic
     (a good idea in any case).

     Laura Lawless provided many hours of help in marking up appropriate
     parts of the documentation in typewriter font.

     Noah Friedman developed an Emacs tool that helped us insert
     "invisible links" into the documentation, which improve the
     usability of that documentation under HTML readers such as Mosaic.

     Richard Stallman contributed a texinfo patch, to be found in the
     file doc/texinfo.tex.