Fgl-interpreter-state
Description of FGL's interpreter state object.
The FGL interpreter state is a stobj containing, as the name suggests,
essentially the entire state of the FGL interpreter. We list and describe
several of the major components of this object.
- stack: a representation of the interpreter stack; see fgl-stack. This is a nested abstract stobj whose logical representation is a
major-stack object but whose implementation uses arrays for efficiency.
- logicman: a nested stobj containing several subfields geared toward
Boolean logic: primarily an AIG (see aignet), an array of ipasir::ipasir incremental SAT solver objects, and the mappings between AIG
literals and CNF literals for each of the ipasir instances.
- bvar-db: a mapping between Boolean variable indices (AIG primary input
numbers) and the symbolic objects they represent. See fgl-getting-bits-from-objects for a discussion of how and when Boolean
variables are derived from terms.
- pathcond: a stack of Boolean constraints (AIG literals) representing
the current path condition. May or may not be used as a constraint on SAT
checks.
