		Search-engine friendly clone of the ACL2 documentation.

Compiled-stv-p

(compiled-stv-p x) is a std::defaggregate of the following fields.

nphases — number of phases for this simulation.
Invariant (posp nphases).
nst-extract-alists — what to extract at times 0...{N-1} from next-states.
Invariant (true-listp nst-extract-alists).
out-extract-alists — what to extract at times 0...{N-1} from outputs.
Invariant (true-listp out-extract-alists).
int-extract-alists — what to extract at times 0...{N-1} from internals.
Invariant (true-listp int-extract-alists).
override-bits — flat list of state bits involved in overrides, i.e., just the override_value and override_decision vars.
Invariant (symbol-listp override-bits).
restrict-alist — combined alist binding (input-bit@phase → sexpr) and (override-bit@phase → sexpr).
in-usersyms — (simulation var → bit list) alist for Inputs + Overrides (replacement value insertion).
out-usersyms — (simulation var → bit list) alist for Outputs + Internals + Overrides (original value extraction).
expanded-ins — Input lines with s-expression values, used only so that we can resolve ~s in stv-doc.
override-paths — Paths being overridden, so we can recreate the cut module as needed.
Invariant (true-listp override-paths).

Source link: compiled-stv-p

Compiled-stv: Raw constructor for compiled-stv-p structures.
Make-compiled-stv: Constructor macro for compiled-stv-p structures.
Change-compiled-stv: A copying macro that lets you create new compiled-stv-p structures, based on existing structures.
Honsed-compiled-stv: Raw constructor for honsed compiled-stv-p structures.
Make-honsed-compiled-stv: Constructor macro for honsed compiled-stv-p structures.
Compiled-stv->restrict-alist: Access the restrict-alist field of a compiled-stv-p structure.
Compiled-stv->override-paths: Access the override-paths field of a compiled-stv-p structure.
Compiled-stv->override-bits: Access the override-bits field of a compiled-stv-p structure.
Compiled-stv->out-usersyms: Access the out-usersyms field of a compiled-stv-p structure.
Compiled-stv->out-extract-alists: Access the out-extract-alists field of a compiled-stv-p structure.
Compiled-stv->nst-extract-alists: Access the nst-extract-alists field of a compiled-stv-p structure.
Compiled-stv->nphases: Access the nphases field of a compiled-stv-p structure.
Compiled-stv->int-extract-alists: Access the int-extract-alists field of a compiled-stv-p structure.
Compiled-stv->in-usersyms: Access the in-usersyms field of a compiled-stv-p structure.
Compiled-stv->expanded-ins: Access the expanded-ins field of a compiled-stv-p structure.