For conditional rewriting with BDDs

The function `if`, but it is used
in a special way by ACL2's bdd package.

**Function: **

(defun if* (x y z) (if x y z))

As explained elsewhere (see bdd-algorithm), ACL2's bdd
algorithm gives special treatment to terms of the form

Thus,

Suppose that we want to prove that

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

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

We imagine this rule simplifying

We also need to imagine simplifying `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))

Finally, we imagine needing to simplify calls of `nthcdr`, where the
first argument is a number (initially, the length of

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

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 (equal (nthcdr (+ 1 n) x) (if* (zp (1+ n)) x (nthcdr n (cdr x)))))

How is `zp` and `binary-+` are enabled) to

(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

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.

If we follow the advice above, we can see rather clearly what happened. See show-bdd.

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

Each of these term-alist pairs led to the next, and the test of the last
one, namely

What would have happened if we had used `if` in place of

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