Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Gl
Esim
Vl2014
Sv
Vwsim
Fgl
Fgl-rewrite-rules
Fgl-function-mode
Fgl-object
Fgl-solving
Fgl-handling-if-then-elses
Fgl-getting-bits-from-objects
Fgl-primitive-and-meta-rules
Fgl-interpreter-overview
Fgl-counterexamples
Fgl-correctness-of-binding-free-variables
Fgl-debugging
Fgl-testbenches
Def-fgl-boolean-constraint
Fgl-stack
Fgl-rewrite-tracing
Def-fgl-param-thm
Def-fgl-thm
Fgl-config
Fgl-config-fix
Make-fgl-config
Fgl-config-p
Fgl-config-equiv
Fgl-config->skip-toplevel-sat-check
Change-fgl-config
Fgl-config->skip-vacuity-check
Fgl-config->function-modes
Fgl-config->trace-rewrites
Fgl-config->prof-enabledp
Fgl-config->make-ites
Fgl-config->reclimit
Fgl-config->sat-config-vacuity
Fgl-config->rewrite-rule-table
Fgl-config->branch-merge-rules
Fgl-config->sat-config
Fgl-fast-alist-support
Fgl-array-support
Advanced-equivalence-checking-with-fgl
Fgl-internals
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Def-fgl-thm
Fgl-config
Config object for the FGL clause processor
This is a product type introduced by
defprod
.
Fields
trace-rewrites —
booleanp
reclimit —
posp
make-ites —
booleanp
rewrite-rule-table
branch-merge-rules
function-modes —
fgl-function-mode-alist
prof-enabledp —
booleanp
sat-config
sat-config-vacuity
skip-toplevel-sat-check —
booleanp
skip-vacuity-check —
booleanp
Subtopics
Fgl-config-fix
Fixing function for
fgl-config
structures.
Make-fgl-config
Basic constructor macro for
fgl-config
structures.
Fgl-config-p
Recognizer for
fgl-config
structures.
Fgl-config-equiv
Basic equivalence relation for
fgl-config
structures.
Fgl-config->skip-toplevel-sat-check
Get the
skip-toplevel-sat-check
field from a
fgl-config
.
Change-fgl-config
Modifying constructor for
fgl-config
structures.
Fgl-config->skip-vacuity-check
Get the
skip-vacuity-check
field from a
fgl-config
.
Fgl-config->function-modes
Get the
function-modes
field from a
fgl-config
.
Fgl-config->trace-rewrites
Get the
trace-rewrites
field from a
fgl-config
.
Fgl-config->prof-enabledp
Get the
prof-enabledp
field from a
fgl-config
.
Fgl-config->make-ites
Get the
make-ites
field from a
fgl-config
.
Fgl-config->reclimit
Get the
reclimit
field from a
fgl-config
.
Fgl-config->sat-config-vacuity
Get the
sat-config-vacuity
field from a
fgl-config
.
Fgl-config->rewrite-rule-table
Get the
rewrite-rule-table
field from a
fgl-config
.
Fgl-config->branch-merge-rules
Get the
branch-merge-rules
field from a
fgl-config
.
Fgl-config->sat-config
Get the
sat-config
field from a
fgl-config
.