Major Section: BDD

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

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

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

.

`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 branchHere, 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.

Major Section: BDD

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

TheACL2 !>(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 !>

`: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))It turns out the 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; 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)))))

`: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-counterpart`

`s`

, 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))))The term that has caused the BDD algorithm to abort is thus[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 !>

`(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-bit 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))))See if* for another example.[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 ; that if we bind x3 to a non-nil value other than T, ; and bind x0, x1, and x2 to t, then we expect to get 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 !>

Major Section: BDD

The function `IF*`

is defined to be `IF`

, but it is used in a
special way by ACL2's BDD package.

As explained elsewhere (see bdd-algorithm), ACL2's BDD
algorithm gives special treatment to terms of the form
`(IF* TEST TBR FBR)`

. In such cases, the algorithm simplifies
`TEST`

first, and the result of that simplification must be a
constant (normally `t`

or `nil`

, but any non-`nil`

explicit value is
treated like `t`

here). Otherwise, the algorithm aborts.

Thus, `IF*`

may be used to implement a sort of conditional
rewriting for ACL2's BDD package, even though this package only
nominally supports unconditional rewriting. The following contrived
example should make this point clear.

Suppose that we want to prove that `(nthcdr (length x) (append x y))`

is equal to `y`

, but that we would be happy to prove this only for
lists having length 4. We can state such a theorem as follows.

(let ((x (list x0 x1 x2 x3))) (equal (nthcdr (length x) (append x y)) y))If we want to prove this formula with a

`:`

`BDD`

hint, then we need to
have appropriate rewrite rules around. First, note that `LENGTH`

is
defined as follows (try `:`

`PE`

`LENGTH`

):
(length x) = (if (stringp x) (len (coerce x 'list)) (len x))Since BDD-based rewriting is merely very simple unconditional rewriting (see bdd-algorithm), we expect to have to prove a rule reducing

`STRINGP`

of a `CONS`

:
(defthm stringp-cons (equal (stringp (cons x y)) nil))Now we need a rule to compute the

`LEN`

of `X`

, because the definition
of `LEN`

is recursive and hence not used by the BDD package.
(defthm len-cons (equal (len (cons a x)) (1+ (len x))))We imagine this rule simplifying

`(LEN (LIST X0 X1 X2 X3))`

in terms of
`(LEN (LIST X1 X2 X3))`

, and so on, and then finally `(LEN nil)`

should
be computed by execution (see bdd-algorithm).
We also need to imagine simplifying `(APPEND X Y)`

, where still `X`

is
bound to `(LIST X0 X1 X2 X3)`

. The following two rules suffice for
this purpose (but are needed, since `APPEND`

, actually `BINARY-APPEND`

,
is recursive).

(defthm append-cons (equal (append (cons a x) y) (cons a (append x y))))Finally, we imagine needing to simplify calls of(defthm append-nil (equal (append nil x) x))

`NTHCDR`

, where the
the first argument is a number (initially, the length of
`(LIST X0 X1 X2 X3)`

, which is 4). The second lemma below is the
traditional way to accomplish that goal (when not using BDDs), by
proving a conditional rewrite rule. (The first lemma is only proved
in order to assist in the proof of the second lemma.)
(defthm fold-constants-in-+ (implies (and (syntaxp (quotep x)) (syntaxp (quotep y))) (equal (+ x y z) (+ (+ x y) z))))The problem with this rule is that its hypothesis makes it a conditional rewrite rule, and conditional rewrite rules are not used by the BDD package. (See bdd-algorithm for a discussion of ``BDD rules.'') (Note that the hypothesis cannot simply be removed; the resulting formula would be false for(defthm nthcdr-add1-conditional (implies (not (zp (1+ n))) (equal (nthcdr (1+ n) x) (nthcdr n (cdr x)))))

`n = -1`

and `x = '(a)`

, for example.) We can solve this problem by using
`IF*`

, as follows; comments follow.
(defthm nthcdr-add1 (equal (nthcdr (+ 1 n) x) (if* (zp (1+ n)) x (nthcdr n (cdr x)))))How is

`nthcdr-add1`

applied by the BDD package? Suppose that the BDD
computation encounters a term of the form `(NTHCDR (+ 1 N) X)`

.
Then the BDD package will apply the rewrite rule `nthcdr-add1`

. The
first thing it will do when attempting to simplify the right hand
side of that rule is to attempt to simplify the term `(ZP (1+ N))`

.
If `N`

is an explicit number (which is the case in the scenario we
envision), this test will reduce (assuming the executable
counterparts of `ZP`

and `BINARY-+`

are enabled) to `t`

or
to `nil`

. In fact, the lemmas above (not including the lemma
`nthcdr-add1-conditional`

) suffice to prove our goal:
(thm (let ((x (list x0 x1 x2 x3))) (equal (nthcdr (length x) (append x y)) y)) :hints (("Goal" :bdd (:vars nil))))

If we execute the following form that disables the definition and
executable counterpart of the function `ZP`

(in-theory (disable zp (zp)))before attempting the proof of the theorem above, we can see more clearly the point of using

`IF*`

. In this case, the prover makes
the following report.
ACL2 Error in ( THM ...): Unable to resolve test of IF* for termIf we follow the advice above, we can see rather clearly what happened. See show-bdd.(IF* (ZP (+ 1 N)) X (NTHCDR N (CDR X)))

under the bindings

((X (CONS X0 (CONS X1 (CONS X2 #)))) (N '3))

-- use SHOW-BDD to see a backtrace.

ACL2 !>(show-bdd)Each of these term-alist pairs led to the next, and the test of the last one, namelyBDD computation on Goal yielded 21 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))) (EQUAL (NTHCDR (LENGTH X) (APPEND X Y)) Y)) alist: ((Y Y) (X3 X3) (X2 X2) (X1 X1) (X0 X0))

(NTHCDR (LENGTH X) (APPEND X Y)) alist: ((X (LIST X0 X1 X2 X3)) (Y Y))

(IF* (ZP (+ 1 N)) X (NTHCDR N (CDR X))) alist: ((X (LIST* X0 X1 X2 X3 Y)) (N 3)) ACL2 !>

`(ZP (+ 1 N))`

where `N`

is bound to `3`

, was
not simplified to `t`

or to `nil`

.
What would have happened if we had used `IF`

in place of `IF*`

in
the rule `nthcdr-add1`

? In that case, if `ZP`

and its executable
counterpart were disabled then we would be put into an infinite
loop! For, each time a term of the form `(NTHCDR k V)`

is
encountered by the BDD package (where k is an explicit number), it
will be rewritten in terms of `(NTHCDR k-1 (CDR V))`

. We would
prefer that if for some reason the term `(ZP (+ 1 N))`

cannot be
decided to be `t`

or to be `nil`

, then the BDD computation should
simply abort.

Even if there were no infinite loop, this kind of use of `IF*`

is
useful in order to provide feedback of the form shown above whenever
the test of an `IF`

term fails to simplify to `t`

or to `nil`

.

Major Section: BDD

Attempts to use BDDs (see bdd), using `:`

`bdd`

hints,
can fail for various reasons. Sometimes it is useful to explore
such failures. To do so, one may simply execute the form

(show-bdd)inside the ACL2 loop. The system's response is generally self-explanatory. Perhaps you have already seen

`show-bdd`

used in
some examples (see bdd-introduction and see if*). Here we
give some details about `show-bdd`

.
`(Show-bdd)`

prints the goal to which the BDD procedure was applied
and reports the number of nodes created during the BDD
computation, followed by additional information depending on whether
or not the computation ran to completion or aborted (for reasons
explained elsewhere; see bdd-algorithm). If the computation
did abort, a backtrace is printed that should be useful in
understanding where the problem lies. Otherwise, `(show-bdd)`

prints out ``falsifying constraints.'' This list of pairs
associates terms with values and suggests how to construct a
binding list for the variables in the conjecture that will falsify
the conjecture. It also prints out the term that is the result
of simplifying the input term. In each of these cases, parts
of the object may be hidden during printing, in order to avoid
creating reams of uninteresting output. If so, the user will be
queried about whether he wishes to see the entire object (alist or
term), which may be quite large. The following responses are
legal:

`w`

-- Walk around the object with a structure editor

`t`

-- Print the object in full

`nil`

-- Do not print any more of the object

`Show-bdd`

actually has four optional arguments, probably rarely
used. The general form is

(show-bdd goal-name goal-ans falsifying-ans term-ans)where

`goal-name`

is the name of the goal on which the `:`

`bdd`

hint was used (or, `nil`

if the system should find such a goal),
`goal-ans`

is the answer to be used in place of the query for
whether to print the input goal in full, `falsifying-ans`

is the
answer to be used in place of the query for whether to print the
falsifying constraints in full, and `term-ans`

is the answer to be
used in place of the query for whether to print the resulting
term in full.