Bfr
An abstraction of the Boolean Function
Representation used by FGL.
GL, the predecessor to FGL, was originally designed to represent
Boolean functions with on ubdds, with support for hons-aigs added
later. In one mode of operation, all Boolean functions were represented with
BDDs, and in another, all Boolean functions were represented with AIGs. BFR was
a type that depended on the mode, meaning UBDD when in BDD mode and AIG when in
AIG mode.
FGL currently only supports representing Boolean functions using references
into an AIGNET stobj, but in case we want to add support for other
representations we still use the BFR concept. The particular representation
used is governed by a bfr-mode object stored in the logicman field
of the interp-st.
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
- Bfr-p
- Recognizer for valid Boolean Function Representation (bfr) objects.
- Bounded-lit-fix
- Bfr-list-fix
- Aignet-lit->bfr
- Variable-g-bindings
- Bfr-listp$
- (bfr-listp$ x bfrstate) recognizes lists where every element satisfies bfr-p.
- Bfrstate>=
- Bfr-listp-witness
- Fgl-object-bindings-bfrlist
- Bfr-set-var
- Set the nth BFR variable to some value in an AIG/BDD environment.
- Bfr-negate
- Bfr-fix
- Fgl-bfr-object-bindings-p
- 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
