BDD-ALGORITHM

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

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

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

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)

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

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

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

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

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

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

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

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

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


[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 !>

IF*

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

(length x)
 =
(if (stringp x)
    (len (coerce x 'list))
    (len x))

(defthm stringp-cons
  (equal (stringp (cons x y))
         nil))

(defthm len-cons
  (equal (len (cons a x))
         (1+ (len x))))

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


(defthm append-nil
  (equal (append nil x)
         x))

(defthm fold-constants-in-+
  (implies (and (syntaxp (quotep x))
                (syntaxp (quotep y)))
           (equal (+ x y z)
                  (+ (+ x y) z))))


(defthm nthcdr-add1-conditional
  (implies (not (zp (1+ n)))
           (equal (nthcdr (1+ n) x)
                  (nthcdr n (cdr x)))))

(defthm nthcdr-add1
  (equal (nthcdr (+ 1 n) x)
         (if* (zp (1+ n))
              x
              (nthcdr n (cdr x)))))

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

ACL2 Error in ( THM ...):  Unable to resolve test of IF* for term


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


BDD 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 !>

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.

SHOW-BDD

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)

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