Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Gl
Witness-cp
Ccg
Install-not-normalized
Rewrite$
Removable-runes
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
Efficiency
Rewrite-bounds
Bash
Def-dag-measure
Bdd
Remove-hyps
Contextual-rewriting
Simp
Rewrite$-hyps
Bash-term-to-dnf
Use-trivial-ancestors-check
Minimal-runes
Clause-processor-tools
Fn-is-body
Without-subsumption
Rewrite-equiv-hint
Def-bounds
Rewrite$-context
Try-gl-concls
Hint-utils
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
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
.