		Search-engine friendly clone of the ACL2 documentation.

Ubdds

Q-sat-any

(q-sat-any a) finds an assignment that satisfies at least one UBDD in the list of UBDDs x.

BOZO naming. This shouldn't start with q- since it's constructing a list of values instead of a UBDD.

Definitions and Theorems

Function: q-sat-any

(defun q-sat-any (a)
       (declare (xargs :guard t))
       (if (atom a)
           nil
           (if (eq (car a) nil)
               (q-sat-any (cdr a))
               (q-sat (car a)))))