# Faig-purebool-p

Does a FAIG always evaluate to a purely Boolean value, i.e., is it
never X or Z?

When an FAIG is known to be purely Boolean, then there is not much
reason to represent it as an FAIG—we might as well throw its offset away
and just work with its onset as an AIG.

When you are dealing with nice, well-behaved, RTL-level circuits that don't
use any fancy low-level, four-valued sorts of things like tri-state buffers,
this can be a useful optimization. For instance, it may reduce the complexity
of SAT queries, or carry out other kinds of analysis where you don't have to
think about four-valuedness.

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

**Function: **faig-purebool-p

(defun faig-purebool-p (x)
(declare (xargs :non-executable t))
(declare (xargs :guard t))
(prog2$ (throw-nonexec-error 'faig-purebool-p
(list x))
(let ((env (faig-purebool-p-witness x)))
(or (equal (faig-eval x env) (faig-t))
(equal (faig-eval x env) (faig-f))))))

### Definitions and Theorems

**Theorem: **faig-purebool-p-necc

(defthm faig-purebool-p-necc
(implies (not (or (equal (faig-eval x env) (faig-t))
(equal (faig-eval x env) (faig-f))))
(not (faig-purebool-p x))))

### Subtopics

- Faig-purebool-check
- An executable version of faig-purebool-p using SAT.
- Faig-purebool-list-p
- Do a list of FAIGs always evaluate to purely Boolean values, i.e.,
are they never X or Z?
- Faig-purebool-aig
- An AIG that captures exactly when the FAIG X is Boolean valued.