An abstraction of the **B**oolean **F**unction
**R**epresentation used by GL.

GL was originally designed to operate on ubdds, with support for aigs being added later. To avoid redoing a lot of proof work, a small level of indirection was added.

The particular Boolean function representation that we are using at any particular time is governed by bfr-mode, and operations like bfr-and allow us to construct new function nodes using whatever the current representation is.

- Pbfr-depends-on
- Bfr-varname-p
- Bfr-varname-fix
- Bfr-to-param-space
- Perhaps strengthen a BFR under some hypothesis.
- Bfr-depends-on
- Aig-var-fix
- Bfr-reasoning
- Clause processor for ACL2::witness-style BFR reasoning.
- Bfr-andc2
`(bfr-andc2 x y)`constructs the ANDC2 of these BFRs.- Bfr-andc1
`(bfr-andc1 x y)`constructs the ANDC1 of these BFRs.- Bfr-unparam-env
- Bfr-set-var
- Set the
n th BFR variable to some value in an AIG/BDD environment. - Bfr-nor
`(bfr-nor x y)`constructs the NOR of these BFRs.- Bfr-nand
`(bfr-nand x y)`constructs the NAND of these BFRs.- Bfr-mode
- Determine the current bfr mode we are using.
- Bfr-equiv
- Semantics equivalence of BFRs, i.e., equal evaluation under every possible environment.
- Bfr-xor
`(bfr-xor x y)`constructs the XOR of these BFRs.- Bfr-iff
`(bfr-iff x y)`constructs the IFF of these BFRs.- Bfr-eval
- Evaluate a BFR under an appropriate BDD/AIG environment.
- Bfr-param-env
- Bfr-lookup
- Look up a BFR variable in an appropriate BDD/AIG environment.
- Bfr-env-equiv
- Bfr-and
(bfr-and x1 x2 ...) constructs the AND of these BFRs.- Bfr-var
- Construct the
n th BFR variable. - Bfr-or
(bfr-or x1 x2 ...) constructs the OR of these BFRs.- Bfr-not
- Construct the NOT of a BFR.
- Bfr-ite
`(bfr-ite x y z)`constructs the If-Then-Else of these BFRs.- Bdd-mode-or-p-true
- Aig-mode-or-p-true
- Bfr-case
- Choose behavior based on the current bfr mode.