		Search-engine friendly clone of the ACL2 documentation.

Reference

Bfr

An abstraction of the Boolean Function Representation 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.

Subtopics

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 nth 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 nth 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.