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`

.