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