		Search-engine friendly clone of the ACL2 documentation.

Fgl-internals

Bfr

An abstraction of the Boolean Function Representation used by GL.

GL was originally designed to operate on ubdds, with support for hons-aigs and aignet 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.

To support aignets, it is important for BFRs to be well-formed, i.e. literals whose node index is in bounds for the current aignet. So we also use a bfrstate object which simultaneously tracks the bfr-mode and current bound.

Subtopics

Bfr-eval: Evaluate a BFR under an appropriate BDD/AIG environment.
Bfrstate: Object encoding the bfr-mode and current node index bound, if using AIGNET mode.
Bfr->aignet-lit
Bounded-lit-fix
Bfr-p: Recognizer for valid Boolean Function Representation (bfr) objects.
Bfr-list-fix
Aignet-lit->bfr
Bfr-listp$: (bfr-listp$ x bfrstate) recognizes lists where every element satisfies bfr-p.
Bfrstate>=
Bfr-listp-witness
Fgl-object-bindings-bfrlist
Bfr-negate
Bfr-set-var: Set the nth BFR variable to some value in an AIG/BDD environment.
Fgl-bfr-object-bindings-p
Bfr-fix
Bfr-mode: Determines whether FGL is using ubdds, hons-aigs, or aignet literals as its Boolean function representation.
Bfr-mode-is: Check the current bfr-mode.
Lbfr-case: Choose behavior based on the current bfr mode of a logicman.
Bfrstate-case: Choose behavior based on the current bfr mode of the bfrstate
Bfrstate-mode-is: Check the current bfr-mode of a bfrstate object.
Lbfr-mode-is: Check the current bfr-mode of a logicman stobj
Bfr-mode-p