Summary of the BDD algorithm in ACL2

The BDD algorithm in ACL2 uses a combination of manipulation of

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

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-**no** subterm of either of the following forms, where

(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

(a)

x is a variable, and it precedes (in the BDD term order) every variable occurring iny orz ;(b)

y andz are syntactically distinct; and,(c) it is not the case that

y ist andz isnil .

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

(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

**Theorem**. Suppose that

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

(EQUAL t1 (if t3 t4 t5))

is provable, it follows that we may substitute either

Next, suppose that at least one term is a call of

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

Note that

We have covered all cases in which at least one term is a variable or at
least one term is a call of *not* equal!

So, we are left with a final case, in which canonical BDD terms `pe`) shows
that equality of the given terms is equivalent to the conjunction of

(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 `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

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

(B3) *IF-lifting* and the *IF-lifting-for-IF loop*

Suppose that one has a term of the form

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

Here, we replace each argument of

We consider arguments

There is one special case, however, for IF-lifting. Suppose that the given
term is of the form

We may now describe the IF-lifting-for-IF loop, which applies to terms of
the form

(i) If

y andz are the same term, then returny .(ii) Otherwise, if

x andz are the same term, then replacez bynil before recursively applying IF-lifting-for-IF.(iii) Otherwise, if

x andy are the same term andy is known to be Boolean, then replacey byt before recursively applying IF-lifting-for-IF.(iv) If

z isnil and eitherx andy are the same term orx is ``known to be Boolean'' andy ist , then returnx .

NOTE: When a variable

(B4) *The ACL2 BDD algorithm*

We are now ready to present the BDD algorithm for ACL2. It is given an
ACL2 term,

If

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

x is a constant, returnx .If

x is of the form(IF test tbr fbr) , then first run the algorithm ontest with the givenva to obtaintest' . Iftest' isnil , then return the resultfbr' of running the algorithm onfbr with the givenva . Iftest' is a constant other thannil , or is a call ofCONS , then return the resulttbr' of running the algorithm ontbr with the givenva . Iftbr is identical tofbr , returntbr . 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 thoughifwere used rather thanif*, except that iftest' is not a constant or a call ofCONS (see paragraph above), then abort the BDD computation. Informally, the tests ofif*terms are expected to ``resolve.'' NOTE: This description shows howif*can be used to implement conditional rewriting in the BDD algorithm.If

x is aLAMBDA expression((LAMBDA vars body) . args) (which often corresponds to aletterm; see let), then first form an alistva' by binding eachv invars to the result of running the algorithm on the corresponding member ofargs , with the current alistva . Then, return the result of the algorithm onbody in the alistva' .Otherwise,

x is of the form(f x1 x2 ... xn) , wheref is a function symbol other thaniforif*. In that case, letxi' be the result of running the algorithm onxi , fori from 1 ton , using the given alistva . First there are a few special cases. Iff isequalthen we returnt ifx1' is syntactically identical tox2' (where this test is very fast; see (B6) below); we returnx1' if it is known to be Boolean andx2' ist ; and similarly, we returnx2' if it is known to be Boolean andx1' ist . Next, if eachxi' is a constant and the: executable-counterpartoff is enabled, then the result is obtained by computation. Next, iff isbooleanpandx1' 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 iff 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 andf 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) ontbr andfbr to obtain termstbr' andfbr' , and we return(IF test tbr' fbr')unlesstbr' is syntactically identical tofbr' , in which case we returntbr' .

When is it the case that, as said above, ``

(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

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

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

**Claim** (Completeness). Suppose that

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

**Lemma**. Suppose that the result of running the ACL2 BDD algorithm on
a top-level 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 `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

Finally, consider the effect in practice of the assumption that the terms
resulting from application of the algorithm contain calls of `if*`.) We leave it to future work to formulate a theorem that
guarantees that the BDD algorithm produces terms containing calls only of

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