		Search-engine friendly clone of the ACL2 documentation.

Ubdd-constructors

Q-ite-fn

Basic way to construct a new if-then-else UBDD.

(q-ite-fn x y z) builds a new UBDD representing (if x y z). That is, the following is a theorem:

(equal (eval-bdd (q-ite-fn x y z) values)
       (if (eval-bdd x values)
           (eval-bdd y values)
         (eval-bdd z values)))

Normally you will want to use q-ite instead, which is a macro that is logically the same as q-ite-fn, but expands into a lazy call of q-ite-fn and can sometimes avoid the need to evaluate y and z.

Note: memoized for efficiency.

Definitions and Theorems

Function: q-ite-fn

(defun q-ite-fn (x y z)
  (declare (xargs :guard t))
  (cond ((null x) z)
        ((atom x) y)
        (t (let ((y (if (hons-equal x y) t y))
                 (z (if (hons-equal x z) nil z)))
             (cond ((hons-equal y z) y)
                   ((and (eq y t) (eq z nil)) x)
                   ((and (eq y nil) (eq z t)) (q-not x))
                   (t (qcons (q-ite-fn (car x) (qcar y) (qcar z))
                             (q-ite-fn (cdr x)
                                       (qcdr y)
                                       (qcdr z)))))))))

Function: q-ite-fn-memoize-condition

(defun q-ite-fn-memoize-condition (x y z)
  (declare (ignorable x y z)
           (xargs :guard 't))
  (and (consp x)
       (or (consp (car x)) (consp (cdr x)))))