		Search-engine friendly clone of the ACL2 documentation.

Faig-purebool-p

Faig-purebool-list-p

Do a list of FAIGs always evaluate to purely Boolean values, i.e., are they never X or Z?

Signature
(faig-purebool-list-p x) → std::bool

This is a logically nice, but non-executable way to express pure Boolean-ness. See also faig-purebool-list-check, which can be executed; it uses a SAT solver to answer the question.

Definitions and Theorems

Function: faig-purebool-list-p

(defun faig-purebool-list-p (x)
       (declare (xargs :guard t))
       (let ((__function__ 'faig-purebool-list-p))
            (declare (ignorable __function__))
            (if (consp x)
                (and (faig-purebool-p (car x))
                     (faig-purebool-list-p (cdr x)))
                t)))

Subtopics

Faig-purebool-list-p-basics: Basic theorems about faig-purebool-list-p, generated by std::deflist.
Faig-purebool-list-check: An executable version of faig-purebool-list-p using SAT.
Faig-purebool-list-aig: An AIG that captures exactly when a list of FAIGs always evaluate to purely Boolean values.