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

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

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

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

only takes about 1.5 times as long as the

Finally, consider the preceding example, with a `executable-counterpart`

Notice that when we issue the

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

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

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.