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.

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

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