		Search-engine friendly clone of the ACL2 documentation.

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