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

GUARD-EXAMPLE    a brief transcript illustrating guards in ACL2

This note addresses the question:  what is the use of guards in ACL2?
Although we recommend that beginners try to avoid guards for a while,
we hope that the summary here is reasonably self-contained and will
provide a reasonable introduction to guards in ACL2.  For a more
systematic discussion, see GUARD.  For a summary of that topic,
see GUARD-QUICK-REFERENCE.

Before we get into the issue of guards, let us note that there are two
important "modes":

defun-mode -- "Does this defun add an axiom (`:logic mode') or not
(`:program mode')?"  (See DEFUN-MODE.)  Only :logic mode
functions can have their "guards verified" via mechanized proof; see
VERIFY-GUARDS.

set-guard-checking -- "Should runtime guard violations signal an error
(:all, and usually with t or :nowarn) or go undetected (nil, :none)?
Equivalently, are expressions evaluated in Common Lisp or in the
logic?"  (See SET-GUARD-CHECKING.)

_Prompt examples_

Here some examples of the relation between the ACL2 prompt and the
"modes" discussed above.  Also see DEFAULT-PRINT-PROMPT.  The
first examples all have ld-skip-proofsp nil; that is, proofs are _not_
skipped.

       ACL2 !>    ; logic mode with guard checking on
       ACL2 >     ; logic mode with guard checking off
       ACL2 p!>   ; program mode with guard checking on
       ACL2 p>    ; program mode with guard checking off

Here are some examples with default-defun-mode of :logic.

       ACL2 >     ; guard checking off, ld-skip-proofsp nil
       ACL2 s>    ; guard checking off, ld-skip-proofsp t
       ACL2 !>    ; guard checking on, ld-skip-proofsp nil
       ACL2 !s>   ; guard checking on, ld-skip-proofsp t

_Sample session_

     ACL2 !>(+ 'abc 3)

     ACL2 Error in TOP-LEVEL: The guard for the function symbol
     BINARY-+, which is (AND (ACL2-NUMBERP X) (ACL2-NUMBERP Y)),
     is violated by the arguments in the call (+ 'ABC 3).

     ACL2 !>:set-guard-checking nil
     ;;;; verbose output omitted here
     ACL2 >(+ 'abc 3)
     3
     ACL2 >(< 'abc 3)
     T
     ACL2 >(< 3 'abc)
     NIL
     ACL2 >(< -3 'abc)
     T
     ACL2 >:set-guard-checking t

     Turning guard checking on, value T.

     ACL2 !>(defun sum-list (x)
             (declare (xargs :guard (integer-listp x)
                             :verify-guards nil))
             (cond ((endp x) 0)
                   (t (+ (car x) (sum-list (cdr x))))))

     The admission of SUM-LIST is trivial, using the relation
     O< (which is known to be well-founded on the domain
     recognized by O-P) and the measure (ACL2-COUNT X).
     We observe that the type of SUM-LIST is described by the
     theorem (ACL2-NUMBERP (SUM-LIST X)).  We used primitive type
     reasoning.

     Summary
     Form:  ( DEFUN SUM-LIST ...)
     Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
     Warnings:  None
     Time:  0.03 seconds
        (prove: 0.00, print: 0.00, proof tree: 0.00, other: 0.03)
      SUM-LIST
     ACL2 !>(sum-list '(1 2 3))

     ACL2 Warning [Guards] in TOP-LEVEL:  Guard-checking will be inhibited
     on recursive calls of the executable counterpart (i.e., in the ACL2
     logic) of SUM-LIST.  To check guards on all recursive calls:
       (set-guard-checking :all)
     To leave behavior unchanged except for inhibiting this message:
       (set-guard-checking :nowarn)

     6
     ACL2 !>(sum-list '(1 2 abc 3))

     ACL2 Error in TOP-LEVEL: The guard for the function symbol
     BINARY-+, which is (AND (ACL2-NUMBERP X) (ACL2-NUMBERP Y)),
     is violated by the arguments in the call (+ 'ABC 3).

     ACL2 !>:set-guard-checking nil
     ;;;; verbose output omitted here
     ACL2 >(sum-list '(1 2 abc 3))
     6
     ACL2 >(defthm sum-list-append
            (equal (sum-list (append a b))
                   (+ (sum-list a) (sum-list b))))

     << Starting proof tree logging >>

     Name the formula above *1.

     Perhaps we can prove *1 by induction.  Three induction
     schemes are suggested by this conjecture.  Subsumption
     reduces that number to two.  However, one of these is flawed
     and so we are left with one viable candidate.

     ...

     That completes the proof of *1.

     Q.E.D.

_Guard verification vs. defun_

           Declare Form                        Guards Verified?

       (declare (xargs :mode :program ...))          no
       (declare (xargs :guard g))                    yes
       (declare (xargs :guard g :verify-guards nil)) no
       (declare (xargs ...<no :guard>...))           no

     ACL2 >:pe sum-list
      l        8  (DEFUN SUM-LIST (X)
                   (DECLARE (XARGS :GUARD (INTEGER-LISTP X)
                                   :VERIFY-GUARDS NIL))
                   (COND ((ENDP X) 0)
                         (T (+ (CAR X) (SUM-LIST (CDR X))))))
     ACL2 >(verify-guards sum-list)
     The non-trivial part of the guard conjecture for SUM-LIST,
     given the :type-prescription rule SUM-LIST, is

     Goal
     (AND (IMPLIES (AND (INTEGER-LISTP X) (NOT (CONSP X)))
                   (EQUAL X NIL))
          (IMPLIES (AND (INTEGER-LISTP X) (NOT (ENDP X)))
                   (INTEGER-LISTP (CDR X)))
          (IMPLIES (AND (INTEGER-LISTP X) (NOT (ENDP X)))
                   (ACL2-NUMBERP (CAR X)))).

     ...

     ACL2 >:pe sum-list
      lv       8  (DEFUN SUM-LIST (X)
                   (DECLARE (XARGS :GUARD (INTEGER-LISTP X)
                                   :VERIFY-GUARDS NIL))
     ACL2 >:set-guard-checking t

     Turning guard checking on, value T.

     ACL2 !>(sum-list '(1 2 abc 3))

     ACL2 Error in TOP-LEVEL: The guard for the function symbol
     SUM-LIST, which is (INTEGER-LISTP X), is violated by the
     arguments in the call (SUM-LIST '(1 2 ABC ...)).  See :DOC wet
     for how you might be able to get an error backtrace.

     ACL2 !>:set-guard-checking nil
     ;;;; verbose output omitted here
     ACL2 >(sum-list '(1 2 abc 3))
     6
     ACL2 >:comp sum-list
     Compiling gazonk0.lsp.
     End of Pass 1.
     End of Pass 2.
     Finished compiling gazonk0.lsp.
     Loading gazonk0.o
     start address -T 1bbf0b4 Finished loading gazonk0.o
     Compiling gazonk0.lsp.
     End of Pass 1.
     End of Pass 2.
     Finished compiling gazonk0.lsp.
     Loading gazonk0.o
     start address -T 1bc4408 Finished loading gazonk0.o
      SUM-LIST
     ACL2 >:q

     Exiting the ACL2 read-eval-print loop.
     ACL2>(trace sum-list)
     (SUM-LIST)

     ACL2>(lp)

     ACL2 Version 1.8.  Level 1.  Cbd "/slocal/src/acl2/v1-9/".
     Type :help for help.
     ACL2 >(sum-list '(1 2 abc 3))
     6
     ACL2 >(sum-list '(1 2 3))
       1> (SUM-LIST (1 2 3))>
         2> (SUM-LIST (2 3))>
           3> (SUM-LIST (3))>
             4> (SUM-LIST NIL)>
             <4 (SUM-LIST 0)>
           <3 (SUM-LIST 3)>
         <2 (SUM-LIST 5)>
       <1 (SUM-LIST 6)>
     6
     ACL2 >:pe sum-list-append
               9  (DEFTHM SUM-LIST-APPEND
                          (EQUAL (SUM-LIST (APPEND A B))
                                 (+ (SUM-LIST A) (SUM-LIST B))))
     ACL2 >(verify-guards sum-list-append)

     The non-trivial part of the guard conjecture for
     SUM-LIST-APPEND, given the :type-prescription rule SUM-LIST,
     is

     Goal
     (AND (TRUE-LISTP A)
          (INTEGER-LISTP (APPEND A B))
          (INTEGER-LISTP A)
          (INTEGER-LISTP B)).

     ...

     ****** FAILED ******* See :DOC failure ****** FAILED ******
     ACL2 >(defthm common-lisp-sum-list-append
              (if (and (integer-listp a)
                       (integer-listp b))
                  (equal (sum-list (append a b))
                         (+ (sum-list a) (sum-list b)))
                  t)
              :rule-classes nil)

     << Starting proof tree logging >>

     By the simple :rewrite rule SUM-LIST-APPEND we reduce the
     conjecture to

     Goal'
     (IMPLIES (AND (INTEGER-LISTP A)
                   (INTEGER-LISTP B))
              (EQUAL (+ (SUM-LIST A) (SUM-LIST B))
                     (+ (SUM-LIST A) (SUM-LIST B)))).

     But we reduce the conjecture to T, by primitive type
     reasoning.

     Q.E.D.
     ;;;; summary omitted here
     ACL2 >(verify-guards common-lisp-sum-list-append)

     The non-trivial part of the guard conjecture for
     COMMON-LISP-SUM-LIST-APPEND, given the :type-prescription
     rule SUM-LIST, is

     Goal
     (AND (IMPLIES (AND (INTEGER-LISTP A)
                        (INTEGER-LISTP B))
                   (TRUE-LISTP A))
          (IMPLIES (AND (INTEGER-LISTP A)
                        (INTEGER-LISTP B))
                   (INTEGER-LISTP (APPEND A B)))).

     ...

     Q.E.D.

     That completes the proof of the guard theorem for
     COMMON-LISP-SUM-LIST-APPEND.  COMMON-LISP-SUM-LIST-APPEND
     is compliant with Common Lisp.
     ;;;; Summary omitted here.
     ACL2 >(defthm foo (consp (mv x y)))

     ...

     Q.E.D.

     ACL2 >(verify-guards foo)

     ACL2 Error in (VERIFY-GUARDS FOO): The number of values we
     need to return is 1 but the number of values returned by the
     call (MV X Y) is 2.

     > (CONSP (MV X Y))

     ACL2 Error in (VERIFY-GUARDS FOO): The guards for FOO cannot
     be verified because the theorem has the wrong syntactic
     form.  See :DOC verify-guards.

MUTUAL-RECURSION-PROOF-EXAMPLE    a small proof about mutually recursive functions

Sometimes one wants to reason about mutually recursive functions.
Although this is possible in ACL2, it can be a bit awkward.  This
example is intended to give some ideas about how one can go about such
proofs.

For an introduction to mutual recursion in ACL2, see
MUTUAL-RECURSION.

We begin by defining two mutually recursive functions:  one that
collects the variables from a term, the other that collects the
variables from a list of terms.  We actually imagine the term argument
to be a pseudo-termp; see PSEUDO-TERMP.

     (mutual-recursion

     (defun free-vars1 (term ans)
       (cond ((atom term)
              (add-to-set-eq term ans))
             ((fquotep term) ans)
             (t (free-vars1-lst (fargs term) ans))))

     (defun free-vars1-lst (lst ans)
       (cond ((atom lst) ans)
             (t (free-vars1-lst (cdr lst)
                                (free-vars1 (car lst) ans)))))

     )

The idea of the following function is that it suggests a proof by
induction in two cases, according to the top-level if structure of the
body.  In one case, (atom x) is true, and the theorem to be proved
should be proved under no additional hypotheses except for (atom x).
In the other case, (not (atom x)) is assumed together with three
instances of the theorem to be proved, one for each recursive call in
this case.  So, one instance substitutes (car x) for x; one substitutes
(cdr x) for x; and the third substitutes (cdr x) for x and (free-vars1
(car x) ans) for ans.  If you think about how you would go about a hand
proof of the theorem to follow, you'll come up with a similar scheme.

     (defun symbol-listp-free-vars1-induction (x ans)
       (if (atom x)
     ; then we just make sure x and ans aren't considered irrelevant
           (list x ans)
         (list (symbol-listp-free-vars1-induction (car x) ans)
               (symbol-listp-free-vars1-induction (cdr x) ans)
               (symbol-listp-free-vars1-induction
                (cdr x)
                (free-vars1 (car x) ans)))))

We now prove the two theorems together as a conjunction, because the
inductive hypotheses for one are sometimes needed in the proof of the
other (even when you do this proof on paper!).

     (defthm symbol-listp-free-vars1
       (and (implies (and (pseudo-termp x)
                          (symbol-listp ans))
                     (symbol-listp (free-vars1 x ans)))
            (implies (and (pseudo-term-listp x)
                          (symbol-listp ans))
                     (symbol-listp (free-vars1-lst x ans))))
       :hints
       (("Goal" :induct (symbol-listp-free-vars1-induction x ans))))

The above works, but let's try for a more efficient proof, which avoids
cluttering the proof with irrelevant (false) inductive hypotheses.

     (ubt 'symbol-listp-free-vars1-induction)

     (defun symbol-listp-free-vars1-induction (flg x ans)

     ; Flg is non-nil (or t) if we are ``thinking'' of a single term.

       (if (atom x)
           (list x ans)
         (if flg
             (symbol-listp-free-vars1-induction nil (cdr x) ans)
           (list (symbol-listp-free-vars1-induction t (car x) ans)
                 (symbol-listp-free-vars1-induction
                  nil
                  (cdr x)
                  (free-vars1 (car x) ans))))))

We now state the theorem as a conditional, so that it can be proved
nicely using the induction scheme that we have just coded.  The prover
will not store an if term as a rewrite rule, but that's OK (as long as
we tell it not to try), because we're going to derive the corollaries
of interest later and make *them* into rewrite rules.

     (defthm symbol-listp-free-vars1-flg
       (if flg
           (implies (and (pseudo-termp x)
                         (symbol-listp ans))
                    (symbol-listp (free-vars1 x ans)))
         (implies (and (pseudo-term-listp x)
                       (symbol-listp ans))
                  (symbol-listp (free-vars1-lst x ans))))
       :hints
       (("Goal" :induct (symbol-listp-free-vars1-induction flg x ans)))
       :rule-classes nil)

And finally, we may derive the theorems we are interested in as
immediate corollaries.

     (defthm symbol-listp-free-vars1
       (implies (and (pseudo-termp x)
                     (symbol-listp ans))
                (symbol-listp (free-vars1 x ans)))
       :hints (("Goal" :by (:instance symbol-listp-free-vars1-flg
                                      (flg t)))))

     (defthm symbol-listp-free-vars1-lst
       (implies (and (pseudo-term-listp x)
                     (symbol-listp ans))
                (symbol-listp (free-vars1-lst x ans)))
       :hints (("Goal" :by (:instance symbol-listp-free-vars1-flg
                                      (flg nil)))))

BDD    ordered binary decision diagrams with rewriting

Ordered binary decision diagrams (OBDDs, often simply called BDDs) are
a technique, originally published by Randy Bryant, for the efficient
simplification of Boolean expressions.  In ACL2 we combine this
technique with rewriting to handle arbitrary ACL2 terms that can
represent not only Boolean values, but non-Boolean values as well.  In
particular, we provide a setting for deciding equality of bit vectors
(lists of Boolean values).

An introduction to BDDs for the automated reasoning community may be
found in "Introduction to the OBDD Algorithm for the ATP Community" by
J Moore, Journal of Automated Reasoning (1994), pp. 33-45.  (This paper
also appears as Technical Report #84 from Computational Logic, Inc.)

Further information about BDDs in ACL2 can be found in the subtopics of
this documentation section.  In particular, see
BDD-INTRODUCTION for a good starting place that provides a number of
examples.

See HINTS for a description of :bdd hints.  For quick
reference, here is an example; but only the :vars part of the hint is
required, as explained in the documentation for hints.  The values
shown are the defaults.

     (:vars nil :bdd-constructors (cons) :prove t :literal :all)

We suggest that you next visit the documentation topic BDD-INTRODUCTION.

BDD-ALGORITHM    summary of the BDD algorithm in ACL2

The BDD algorithm in ACL2 uses a combination of manipulation of IF
terms and unconditional rewriting.  In this discussion we begin with
some relevant mathematical theory.  This is followed by a description
of how ACL2 does BDDs, including concluding discussions of soundness,
completeness, and efficiency.

We recommend that you read the other documentation about BDDs in ACL2
before reading the rather technical material that follows.  See
BDD.

Here is an outline of our presentation.  Readers who want a user
perspective, without undue mathematical theory, may wish to skip to
Part (B), referring to Part (A) only on occasion if necessary.

(A) *Mathematical Considerations*

     (A1) BDD term order

     (A2) BDD-constructors and BDD terms, and their connection with
     aborting the BDD algorithm

     (A3) Canonical BDD terms

     (A4) A theorem stating the equivalence of provable and syntactic
     equality for canonical BDD terms

(B) *Algorithmic Considerations*

     (B1) BDD rules (rules used by the rewriting portion of the ACL2 BDD
     algorithm)

     (B2) Terms "known to be Boolean"

     (B3) An "IF-lifting" operation used by the algorithm, as well as an
     iterative version of that operation

     (B4) The ACL2 BDD algorithm

     (B5) Soundness and Completeness of the ACL2 BDD algorithm

     (B6) Efficiency considerations

(A) *Mathematical Considerations*

(A1) _BDD term order_

Our BDD algorithm creates a total "BDD term order" on ACL2 terms, on
the fly.  We use this order in our discussions below of IF-lifting and
of canonical BDD terms, and in the algorithm's use of commutativity.
The particular order is unimportant, except that we guarantee (for
purposes of commutative functions) that constants are smaller in this
order than non-constants.

(A2) _BDD-constructors_ (assumed to be '(cons)) and _BDD terms_

We take as given a list of function symbols that we call the
"BDD-constructors."  By default, the only BDD-constructor is cons,
although it is legal to specify any list of function symbols as the
BDD-constructors, either by using the acl2-defaults-table (see
ACL2-DEFAULTS-TABLE) or by supplying a :BDD-CONSTRUCTORS hint (see
HINTS).  Warning: this capability is largely untested and may
produce undesirable results.  Henceforth, except when explicitly stated
to the contrary, we assume that BDD-constructors is '(cons).

Roughly speaking, a BDD term is the sort of term produced by our BDD
algorithm, namely a tree with all cons nodes lying above all non-CONS
nodes.  More formally, a term is said to be a BDD term if it contains
*no* subterm of either of the following forms, where f is not CONS.

     (f ... (CONS ...) ...)

     (f ... 'x ...)  ; where (consp x) = t

We will see that whenever the BDD algorithm attempts to create a term
that is not a BDD term, it aborts instead.  Thus, whenever the
algorithm completes without aborting, it creates a BDD term.

(A3) _Canonical BDD terms_

We can strengthen the notion of "BDD term" to a notion of "canonical
BDD term" by imposing the following additional requirements, for every
subterm of the form (IF x y z):

     (a) x is a variable, and it precedes (in the BDD term order) every
     variable occurring in y or z;

     (b) y and z are syntactically distinct; and,

     (c) it is not the case that y is t and z is nil.

We claim that it follows easily from our description of the BDD
algorithm that every term it creates is a canonical BDD term, assuming
that the variables occurring in all such terms are treated by the
algorithm as being Boolean (see (B2) below) and that the terms contain
no function symbols other than IF and CONS.  Thus, under those
assumptions the following theorem shows that the BDD algorithm never
creates distinct terms that are provably equal, a property that is
useful for completeness and efficiency (as we explain in (B5) and (B6)
below).

(A4) _Provably equal canonical BDD terms are identical_

We believe that the following theorem and proof are routine extensions
of a standard result and proof to terms that allow calls of CONS.

*Theorem*.  Suppose that t1 and t2 are canonical BDD terms that contain
no function symbols other than IF and CONS.  Also suppose that (EQUAL
t1 t2) is a theorem.  Then t1 and t2 are syntactically identical.

Proof of theorem:  By induction on the total number of symbols
occurring in these two terms.  First suppose that at least one term is
a variable; without loss of generality let it be t1.  We must prove
that t2 is syntactically the same as t1.  Now it is clearly consistent
that (EQUAL t1 t2) is false if t2 is a call of CONS (to see this,
simply let t1 be an value that is not a CONSP).  Similarly, t2 cannot
be a constant or a variable other than t1.  The remaining possibility
to rule out is that t2 is of the form (IF t3 t4 t5), since by
assumption its function symbol must be IF or CONS and we have already
handled the latter case.  Since t2 is canonical, we know that t3 is a
variable.  Since (EQUAL t1 t2) is provable, i.e.,

     (EQUAL t1 (if t3 t4 t5))

is provable, it follows that we may substitute either t or nil for t3
into this equality to obtain two new provable equalities.  First,
suppose that t1 and t3 are distinct variables.  Then these
substitutions show that t1 is provably equal to both t4 and t5 (since
t3 does not occur in t4 or t5 by property (a) above, as t2 is
canonical), and hence t4 and t5 are provably equal to each other, which
implies by the inductive hypothesis that they are the same term -- and
this contradicts the assumption that t2 is canonical (property (b)).
Therefore t1 and t3 are the same variable, i.e., the equality displayed
above is actually (EQUAL t1 (if t1 t4 t5)).  Substituting t and then
nil for t1 into this provable equality lets us prove (EQUAL t t4) and
(EQUAL nil t5), which by the inductive hypothesis implies that t4 is
(syntactically) the term t and t5 is nil.  That is, t2 is (IF t1 t
nil), which contradicts the assumption that t2 is canonical (property
(c)).

Next, suppose that at least one term is a call of IF.  Our first
observation is that the other term is also a call of IF.  For if the
other is a call of CONS, then they cannot be provably equal, because
the former has no function symbols other than IF and hence is Boolean
when all its variables are assigned Boolean values.  Also, if the other
is a constant, then both branches of the IF term are provably equal to
that constant and hence these branches are syntactically identical by
the inductive hypothesis, contradicting property (b).  Hence, we may
assume for this case that both terms are calls of IF; let us write them
as follows.

     t0:  (IF t1 t2 t3)
     u0:  (IF u1 u2 u3)

Note that t1 and u1 are variables, by property (a) of canonical BDD
terms.  First we claim that t1 does not strictly precede u1 in the BDD
term order.  For suppose t1 does strictly precede u1.  Then property
(a) of canonical BDD terms guarantees that t1 does not occur in u0.
Hence, an argument much like one used above shows that u0 is provably
equal to both t2 (substituting t for t1) and t3 (substituting nil for
t1), and hence t2 and t3 are provably equal.  That implies that they
are identical terms, by the inductive hypothesis, which then
contradicts property (b) for t0.  Similarly, u1 does not strictly
precede t1 in the BDD term order.  Therefore, t1 and u1 are the same
variable.  By substituting t for this variable we see that t2 and u2
are provably equal, and hence they are equal by the inductive
hypothesis.  Similarly, by substituting nil for t1 (and u1) we see that
t3 and u3 are provably, hence syntactically, equal.

We have covered all cases in which at least one term is a variable or
at least one term is a call of IF.  If both terms are constants, then
provable and syntactic equality are clearly equivalent.  Finally, then,
we may assume that one term is a call of CONS and the other is a
constant or a call of CONS.  The constant case is similar to the CONS
case if the constant is a CONSP, so we omit it; while if the constant
is not a CONSP then it is not provably equal to a call of CONS; in fact
it is provably _not_ equal!

So, we are left with a final case, in which canonical BDD terms (CONS
t1 t2) and (CONS u1 u2) are provably equal, and we want to show that t1
and u1 are syntactically equal as are t2 and u2.  These conclusions are
easy consequences of the inductive hypothesis, since the ACL2 axiom
CONS-EQUAL (which you can inspect using :PE) shows that equality of the
given terms is equivalent to the conjunction of (EQUAL t1 t2) and
(EQUAL u1 u2).  Q.E.D.

(B) *Algorithmic Considerations*

(B1) _BDD rules_

A rule of class :rewrite (see RULE-CLASSES) is said to be a
"BDD rewrite rule" if and only if it satisfies the following criteria.
(1) The rule is enabled.  (2) Its equivalence relation is equal.  (3)
It has no hypotheses.  (4) Its :loop-stopper field is nil, i.e., it is
not a permutative rule.  (5) All variables occurring in the rule occur
in its left-hand side (i.e., there are no "free variables"; see
REWRITE).  A rule of class :definition (see RULE-CLASSES) is
said to be a "BDD definition rule" if it satisfies all the criteria
above (except (4), which does not apply), and moreover the top function
symbol of the left-hand side was not recursively (or mutually
recursively) defined.  Technical point:  Note that this additional
criterion is independent of whether or not the indicated function
symbol actually occurs in the right-hand side of the rule.

Both BDD rewrite rules and BDD definition rules are said to be "BDD
rules."

(B2) _Terms "known to be Boolean"_

We apply the BDD algorithm in the context of a top-level goal to prove,
namely, the goal at which the :BDD hint is attached.  As we run the BDD
algorithm, we allow ourselves to say that a set of terms is "known to
be Boolean" if we can verify that the goal is provable from the
assumption that at least one of the terms is not Boolean.
Equivalently, we allow ourselves to say that a set of terms is "known
to be Boolean" if we can verify that the original goal is provably
equivalent to the assertion that if all terms in the set are Boolean,
then the goal holds.  The notion "known to be Boolean" is conservative
in the sense that there are generally sets of terms for which the above
equivalent criteria hold and yet the sets of terms are not noted as as
being "known to be Boolean."  However, ACL2 uses a number of tricks,
including type-set reasoning and analysis of the structure of the
top-level goal, to attempt to establish that a sufficiently inclusive
set of terms is known to be Boolean.

From a practical standpoint, the algorithm determines a set of terms
known to be Boolean; we allow ourselves to say that each term in this
set is "known to be Boolean."  The algorithm assumes that these terms
are indeed Boolean, and can make use of that assumption.  For example,
if t1 is known to be Boolean then the algorithm simplifies (IF t1 t
nil) to t1; see (iv) in the discussion immediately below.

(B3) _IF-lifting_ and the _IF-lifting-for-IF loop_

Suppose that one has a term of the form (f ... (IF test x y) ...),
where f is a function symbol other than CONS.  Then we say that
"IF-lifting" test "from" this term produces the following term, which
is provably equal to the given term.

     (if test
         (f ... x ...)  ; resulting true branch
         (f ... y ...)) ; resulting false branch

Here, we replace each argument of f of the form (IF test .. ..), for
the same test, in the same way.  In this case we say that "IF-lifting
applies to" the given term, "yielding the test" test and with the
"resulting two branches" displayed above.  Whenever we apply
IF-lifting, we do so for the available test that is least in the BDD
term order (see (A1) above).

We consider arguments v of f that are "known to be Boolean" (see above)
to be replaced by (IF v t nil) for the purposes of IF-lifting, i.e.,
before IF-lifting is applied.

There is one special case, however, for IF-lifting.  Suppose that the
given term is of the form (IF v y z) where v is a variable and is the
test to be lifted out (i.e., it is least in the BDD term order among
the potential tests).  Moroever, suppose that neither y nor z is of the
form (IF v W1 W2) for that same v.  Then IF-lifting does not apply to
the given term.

We may now describe the IF-lifting-for-IF loop, which applies to terms
of the form (IF test tbr fbr) where the algorithm has already produced
test, tbr, and fbr.  First, if test is nil then we return fbr, while if
test is a non-nil constant or a call of CONS then we return tbr.
Otherwise, we see if IF-lifting applies.  If IF-lifting does not apply,
then we return (IF test tbr fbr).  Otherwise, we apply IF-lifting to
obtain a term of the form (IF x y z), by lifting out the appropriate
test.  Now we recursively apply the IF-lifting-for-IF loop to the term
(IF x y z), unless any of the following special cases apply.

     (i) If y and z are the same term, then return y.

     (ii) Otherwise, if x and z are the same term, then replace z by
     nil before recursively applying IF-lifting-for-IF.

     (iii) Otherwise, if x and y are the same term and y is known to be
     Boolean, then replace y by t before recursively applying
     IF-lifting-for-IF.

     (iv) If z is nil and either x and y are the same term or x is
     "known to be Boolean" and y is t, then return x.

NOTE:  When a variable x is known to be Boolean, it is easy to see that
the form (IF x t nil) is always reduced to x by this algorithm.

(B4) _The ACL2 BDD algorithm_

We are now ready to present the BDD algorithm for ACL2.  It is given an
ACL2 term, x, as well as an association list va that maps variables to
terms, including all variables occurring in x.  We maintain the
invariant that whenever a variable is mapped by va to a term, that term
has already been constructed by the algorithm, except:  initially va
maps every variable occurring in the top-level term to itself.  The
algorithm proceeds as follows.  We implicitly ordain that whenever the
BDD algorithm attempts to create a term that is not a BDD term (as
defined above in (A2)), it aborts instead.  Thus, whenever the
algorithm completes without aborting, it creates a BDD term.

     If x is a variable, return the result of looking it up in va.

     If x is a constant, return x.

     If x is of the form (IF test tbr fbr), then first run the
     algorithm on test with the given va to obtain test'.  If test' is
     nil, then return the result fbr' of running the algorithm on fbr
     with the given va.  If test' is a constant other than nil, or is a
     call of CONS, then return the result tbr' of running the algorithm
     on tbr with the given va.  If tbr is identical to fbr, return tbr.
     Otherwise, return the result of applying the IF-lifting-for-IF
     loop (described above) to the term (IF test' tbr' fbr').

     If x is of the form (IF* test tbr fbr), then compute the result
     exactly as though IF were used rather than IF*, except that if
     test' is not a constant or a call of CONS (see paragraph above),
     then abort the BDD computation.  Informally, the tests of IF*
     terms are expected to "resolve."  NOTE:  This description shows
     how IF* can be used to implement conditional rewriting in the BDD
     algorithm.

     If x is a LAMBDA expression ((LAMBDA vars body) . args) (which
     often corresponds to a LET term; see LET), then first form
     an alist va' by binding each v in vars to the result of running
     the algorithm on the corresponding member of args, with the
     current alist va.  Then, return the result of the algorithm on
     body in the alist va'.

     Otherwise, x is of the form (f x1 x2 ... xn), where f is a
     function symbol other than IF or IF*.  In that case, let xi' be
     the result of running the algorithm on xi, for i from 1 to n,
     using the given alist va.  First there are a few special cases.
     If f is EQUAL then we return t if x1' is syntactically identical
     to x2' (where this test is very fast; see (B6) below); we return
     x1' if it is known to be Boolean and x2' is t; and similarly, we
     return x2' if it is known to be Boolean and x1' is t.  Next, if
     each xi' is a constant and the :executable-counterpart of f is
     enabled, then the result is obtained by computation.  Next, if f
     is BOOLEANP and x1' is known to be Boolean, t is returned.
     Otherwise, we proceed as follows, first possibly swapping the
     arguments if they are out of (the BDD term) order and if f is
     known to be commutative (see below).  If a BDD rewrite rule (as
     defined above) matches the term (f x1'... xn'), then the most
     recently stored such rule is applied.  If there is no such match
     and f is a BDD-constructor, then we return (f x1'... xn').
     Otherwise, if a BDD definition rule matches this term, then the
     most recently stored such rule (which will usually be the original
     definition for most users) is applied.  If none of the above
     applies and neither does IF-lifting, then we return (f x1'...
     xn').  Otherwise we apply IF-lifting to (f x1'... xn') to obtain a
     term (IF test tbr fbr); but we aren't done yet.  Rather, we run
     the BDD algorithm (using the same alist) on tbr and fbr to obtain
     terms tbr' and fbr', and we return (IF test tbr' fbr') unless tbr'
     is syntactically identical to fbr', in which case we return tbr'.

When is it the case that, as said above, "f is known to be
commutative"?  This happens when an enabled rewrite rule is of the form
(EQUAL (f X Y) (f Y X)).  Regarding swapping the arguments in that
case:  recall that we may assume very little about the BDD term order,
essentially only that we swap the two arguments when the second is a
constant and the first is not, for example, in (+ x 1).  Other than
that situation, one cannot expect to predict accurately when the
arguments of commutative operators will be swapped.

(B5) Soundness and Completeness of the ACL2 BDD algorithm

Roughly speaking, "soundness" means that the BDD algorithm should give
correct answers, and "completeness" means that it should be powerful
enough to prove all true facts.  Let us make the soundness claim a
little more precise, and then we'll address completeness under suitable
hypotheses.

*Claim* (Soundness).  If the ACL2 BDD algorithm runs to completion on
an input term t0, then it produces a result that is provably equal to
t0.

We leave the proof of this claim to the reader.  The basic idea is
simply to check that each step of the algorithm preserves the meaning
of the term under the bindings in the given alist.

Let us start our discussion of completeness by recalling the theorem
proved above in (A4).

*Theorem*.  Suppose that t1 and t2 are canonical BDD terms that contain
no function symbols other than IF and CONS.  Also suppose that (EQUAL
t1 t2) is a theorem.  Then t1 and t2 are syntactically identical.

Below we show how this theorem implies the following completeness
property of the ACL2 BDD algorithm.  We continue to assume that CONS is
the only BDD-constructor.

*Claim* (Completeness).  Suppose that t1 and t2 are provably equal
terms, under the assumption that all their variables are known to be
Boolean.  Assume further that under this same assumption, top-level
runs of the ACL2 BDD algorithm on these terms return terms that contain
only the function symbols IF and CONS.  Then the algorithm returns the
same term for both t1 and t2, and the algorithm reduces (EQUAL t1 t2)
to t.

Why is this claim true?  First, notice that the second part of the
conclusion follows immediately from the first, by definition of the
algorithm.  Next, notice that the terms u1 and u2 obtained by running
the algorithm on t1 and t2, respectively, are provably equal to t1 and
t2, respectively, by the Soundness Claim.  It follows that u1 and u2
are provably equal to each other.  Since these terms contain no
function symbols other than IF or CONS, by hypothesis, the Claim now
follows from the Theorem above together with the following lemma.

*Lemma*.  Suppose that the result of running the ACL2 BDD algorithm on
a top-level term t0 is a term u0 that contains only the function
symbols IF and CONS, where all variables of t0 are known to be Boolean.
Then u0 is a canonical BDD term.

Proof:  left to the reader.  Simply follow the definition of the
algorithm, with a separate argument for the IF-lifting-for-IF loop.

Finally, let us remark on the assumptions of the Completeness Claim
above.  The assumption that all variables are known to be Boolean is
often true; in fact, the system uses the forward-chaining rule
boolean-listp-forward (you can see it using :pe) to try to establish
this assumption, if your theorem has a form such as the following.

     (let ((x (list x0 x1 ...))
           (y (list y0 y1 ...)))
       (implies (and (boolean-listp x)
                     (boolean-listp y))
                ...))

Moreover, the :BDD hint can be used to force the prover to abort if it
cannot check that the indicated variables are known to be Boolean; see
HINTS.

Finally, consider the effect in practice of the assumption that the
terms resulting from application of the algorithm contain calls of IF
and CONS only.  Typical use of BDDs in ACL2 takes place in a theory
(see THEORIES) in which all relevant non-recursive function
symbols are enabled and all recursive function symbols possess enabled
BDD rewrite rules that tell them how open up.  For example, such a rule
may say how to expand on a given function call's argument that has the
form (CONS a x), while another may say how to expand when that argument
is nil).  (See for example the rules append-cons and append-nil in the
documentation for IF*.)  We leave it to future work to formulate a
theorem that guarantees that the BDD algorithm produces terms
containing calls only of IF and CONS assuming a suitably "complete"
collection of rewrite rules.

(B6) _Efficiency considerations_

Following Bryant's algorithm, we use a graph representation of terms
created by the BDD algorithm's computation.  This representation enjoys
some important properties.

     (Time efficiency) The test for syntactic equality of BDD terms is
     very fast.

     (Space efficiency) Equal BDD data structures are stored identically
     in memory.

_Implementation note._  The representation actually uses a sort of hash
table for BDD terms that is implemented as an ACL2 1-dimensional array.
See ARRAYS.  In addition, we use a second such hash table to
avoid recomputing the result of applying a function symbol to the
result of running the algorithm on its arguments.  We believe that
these uses of hash tables are standard.  They are also discussed in
Moore's paper on BDDs; see BDD for the reference.

BDD-INTRODUCTION    examples illustrating the use of BDDs in ACL2

See BDD for a brief introduction to BDDs in ACL2 and for
pointers to other documentation on BDDs in ACL2.  Here, we illustrate
the use of BDDs in ACL2 by way of some examples.  For a further
example, see IF*.

Let us begin with a really simple example.  (We will explain the :bdd
hint (:vars nil) below.)

     ACL2 !>(thm (equal (if a b c) (if (not a) c b))
                 :hints (("Goal" :bdd (:vars nil)))) ; Prove with BDDs

     [Note:  A hint was supplied for our processing of the goal above.
     Thanks!]

     But simplification with BDDs (7 nodes) reduces this to T, using the
     :definitions EQUAL and NOT.

     Q.E.D.

     Summary
     Form:  ( THM ...)
     Rules: ((:DEFINITION EQUAL) (:DEFINITION NOT))
     Warnings:  None
     Time:  0.18 seconds (prove: 0.05, print: 0.02, other: 0.12)

     Proof succeeded.
     ACL2 !>

The :bdd hint (:vars nil) indicates that BDDs are to be used on the
indicated goal, and that any so-called "variable ordering" may be used:
ACL2 may use a convenient order that is far from optimal.  It is
beyond the scope of the present documentation to address the issue of
how the user may choose good variable orderings.  Someday our
implementation of BDDs may be improved to include heuristically-chosen
variable orderings rather than rather random ones.

Here is a more interesting example.

     (defun v-not (x)
     ; Complement every element of a list of Booleans.
       (if (consp x)
           (cons (not (car x)) (v-not (cdr x)))
         nil))

     ; Now we prove a rewrite rule that explains how to open up v-not on
     ; a consp.
     (defthm v-not-cons
       (equal (v-not (cons x y))
              (cons (not x) (v-not y))))

     ; Finally, we prove for 7-bit lists that v-not is self-inverting.
     (thm
      (let ((x (list x0 x1 x2 x3 x4 x5 x6)))
        (implies (boolean-listp x)
                 (equal (v-not (v-not x)) x)))
      :hints (("Goal" :bdd
                      ;; Note that this time we specify a variable order.
                      (:vars (x0 x1 x2 x3 x4 x5 x6)))))

It turns out that the variable order doesn't seem to matter in this
example; using several orders we found that 30 nodes were created, and
the proof time was about 1/10 of a second on a (somewhat enhanced)
Sparc 2.  The same proof took about a minute and a half without any
:bdd hint!  This observation is a bit misleading perhaps, since the
theorem for arbitrary x,

     (thm
      (implies (boolean-listp x)
               (equal (v-not (v-not x)) x)))

only takes about 1.5 times as long as the :bdd proof for 7 bits, above!
Nevertheless, BDDs can be very useful in reducing proof time,
especially when there is no regular structure to facilitate proof by
induction, or when the induction scheme is so complicated to construct
that significant user effort is required to get the proof by induction
to go through.

Finally, consider the preceding example, with a :bdd hint of (say)
(:vars nil), but with the rewrite rule v-not-cons above disabled.  In
that case, the proof fails, as we see below.  That is because the BDD
algorithm in ACL2 uses hypothesis-free :rewrite rules,
:executable-counterparts, and nonrecursive definitions, but it does not
use recursive definitions.

Notice that when we issue the (show-bdd) command, the system's response
clearly shows that we need a rewrite rule for simplifying terms of the
form (v-not (cons ...)).

     ACL2 !>(thm
             (let ((x (list x0 x1 x2 x3 x4 x5 x6)))
               (implies (boolean-listp x)
                        (equal (v-not (v-not x)) x)))
             :hints (("Goal" :bdd (:vars nil)
                      :in-theory (disable v-not-cons))))

     [Note:  A hint was supplied for our processing of the goal above.
     Thanks!]

     ACL2 Error in ( THM ...):  Attempted to create V-NOT node during BDD
     processing with an argument that is a call of a bdd-constructor,
     which would produce a non-BDD term (as defined in :DOC
     bdd-algorithm).  See :DOC show-bdd.

     Summary
     Form:  ( THM ...)
     Rules: NIL
     Warnings:  None
     Time:  0.58 seconds (prove: 0.13, print: 0.00, other: 0.45)

     ******** FAILED ********  See :DOC failure  ******** FAILED ********
     ACL2 !>(show-bdd)

     BDD computation on Goal yielded 17 nodes.
     ==============================

     BDD computation was aborted on Goal, and hence there is no
     falsifying assignment that can be constructed.  Here is a backtrace
     of calls, starting with the top-level call and ending with the one
     that led to the abort.  See :DOC show-bdd.

     (LET ((X (LIST X0 X1 X2 X3 X4 X5 ...)))
          (IMPLIES (BOOLEAN-LISTP X)
                   (EQUAL (V-NOT (V-NOT X)) X)))
       alist: ((X6 X6) (X5 X5) (X4 X4) (X3 X3) (X2 X2) (X1 X1) (X0 X0))

     (EQUAL (V-NOT (V-NOT X)) X)
       alist: ((X (LIST X0 X1 X2 X3 X4 X5 ...)))

     (V-NOT (V-NOT X))
       alist: ((X (LIST X0 X1 X2 X3 X4 X5 ...)))

     (V-NOT X)
       alist: ((X (LIST X0 X1 X2 X3 X4 X5 ...)))
     ACL2 !>

The term that has caused the BDD algorithm to abort is thus (V-NOT X),
where X has the value (LIST X0 X1 X2 X3 X4 X5 ...), i.e., (CONS X0
(LIST X1 X2 X3 X4 X5 ...)).  Thus, we see the utility of introducing a
rewrite rule to simplify terms of the form (V-NOT (CONS ...)).  The
moral of this story is that if you get an error of the sort shown
above, you may find it useful to execute the command (show-bdd) and use
the result as advice that suggests the left hand side of a rewrite rule.

Here is another sort of failed proof.  In this version we have omitted
the hypothesis that the input is a bit vector.  Below we use show-bdd
to see what went wrong, and use the resulting information to construct
a counterexample.  This failed proof corresponds to a slightly modified
input theorem, in which x is bound to the 4-element list (list x0 x1 x2
x3).

     ACL2 !>(thm
             (let ((x (list x0 x1 x2 x3)))
               (equal (v-not (v-not x)) x))
             :hints (("Goal" :bdd
                      ;; This time we do not specify a variable order.
                      (:vars nil))))

     [Note:  A hint was supplied for our processing of the goal above.
     Thanks!]

     ACL2 Error in ( THM ...):  The :BDD hint for the current goal has
     successfully simplified this goal, but has failed to prove it.
     Consider using (SHOW-BDD) to suggest a counterexample; see :DOC
     show-bdd.

     Summary
     Form:  ( THM ...)
     Rules: NIL
     Warnings:  None
     Time:  0.18 seconds (prove: 0.07, print: 0.00, other: 0.12)

     ******** FAILED ********  See :DOC failure  ******** FAILED ********
     ACL2 !>(show-bdd)

     BDD computation on Goal yielded 73 nodes.
     ==============================

     Falsifying constraints:
     ((X0 "Some non-nil value")
      (X1 "Some non-nil value")
      (X2 "Some non-nil value")
      (X3 "Some non-nil value")
      ((EQUAL 'T X0) T)
      ((EQUAL 'T X1) T)
      ((EQUAL 'T X2) T)
      ((EQUAL 'T X3) NIL))

     ==============================

     Term obtained from BDD computation on Goal:

     (IF X0
         (IF X1
             (IF X2 (IF X3 (IF # # #) (IF X3 # #))
                 (IF X2 'NIL (IF X3 # #)))
             (IF X1 'NIL
                 (IF X2 (IF X3 # #) (IF X2 # #))))
         (IF X0 'NIL
             (IF X1 (IF X2 (IF X3 # #) (IF X2 # #))
                 (IF X1 'NIL (IF X2 # #)))))

     ACL2 Query (:SHOW-BDD):  Print the term in full?  (N, Y, W or ?):
     n ; I've seen enough.  The assignment shown above suggests
       ; (though not conclusively) that if we bind x3 to a non-nil
       ; value other than T, and bind x0, x1, and x2 to t, then we
       ; this may give us a counterexample.
     ACL2 !>(let ((x0 t) (x1 t) (x2 t) (x3 7))
              (let ((x (list x0 x1 x2 x3)))
                ;; Let's use LIST instead of EQUAL to see how the two
                ;; lists differ.
                (list (v-not (v-not x)) x)))
     ((T T T T) (T T T 7))
     ACL2 !>

See IF* for another example.