		Search-engine friendly clone of the ACL2 documentation.

4v-sexprs

4v-sexpr-purebool-p

Does a 4v-sexpr always evaluate to a purely Boolean value, i.e., is it never X or Z?

It is sometimes useful to know whether a 4v-sexpr is always purely Boolean valued; see faig-purebool-p for some directly analogous discussion about faigs.

(4v-sexpr-purebool-p sexpr) is a logically nice, but non-executable way to express pure Boolean-ness. See also 4v-sexpr-purebool-check, which can be executed, and uses a SAT solver to answer the question.

Definitions and Theorems

Theorem: 4v-sexpr-purebool-p-necc

(defthm 4v-sexpr-purebool-p-necc
        (implies (not (or (equal (4v-sexpr-eval sexpr env) (4vt))
                          (equal (4v-sexpr-eval sexpr env)
                                 (4vf))))
                 (not (4v-sexpr-purebool-p sexpr))))

Theorem: 4v-sexpr-purebool-p-to-faig-purebool-p

(defthm 4v-sexpr-purebool-p-to-faig-purebool-p
        (equal (4v-sexpr-purebool-p sexpr)
               (faig-purebool-p (sfaig sexpr))))

Subtopics

4v-sexpr-purebool-check: An executable version of 4v-sexpr-purebool-p using SAT.
4v-sexpr-purebool-list-check: An executable version of 4v-sexpr-purebool-list-p using SAT.
4v-sexpr-purebool-list-p: Do a list of 4v-sexprs always evaluate to purely Boolean values, i.e., are they never X or Z?
4v-sexpr-purebool-list-p-to-faig-purebool-list-p: Main theorem showing that 4v-sexpr-purebool-list-p is equivalent to faig-purebool-list-p.