Fgl-config
Config object for the FGL clause processor
This is a product type introduced by defprod.
Fields
- trace-rewrites — booleanp
- If T, Turn on tracing of rewrite rules -- see fgl-rewrite-tracing.
- reclimit — posp
- Recursion limit for the FGL interpreter/rewriter. Defaults to 1
million; set smaller to catch rewrite loops faster.
- make-ites — booleanp
- If NIL (the default), then if the two branches of an IF term
rewrite to objects that cannot be merged, FGL produces an error. If T, then it
creates an if-then-else object, which allows simplification to proceed but
perhaps not in a useful direction.
- rewrite-rule-table
- The rewrite rule table. Probably shouldn't be changed
by the user; instead use the utilities described in fgl-rewrite-rules.
- branch-merge-rules
- The branch-merge rewrite rule table. Probably
shouldn't be changed by the user; instead use the utilities described in fgl-rewrite-rules.
- function-modes — fgl-function-mode-alist
- The function mode table (see fgl-function-mode). Probably
shouldn't be changed by the user; instead use the utilities described in fgl-rewrite-rules.
- prof-enabledp — booleanp
- If T (the default), then the interpreter collects rule
profiling information (like ACL2's accumulated-persistence) and
displays it when the interpreter finishes.
- sat-config
- SAT config object for the final toplevel SAT check. If
NIL (the default), then instead uses the attachment for
(fgl-toplevel-sat-check-config). If nonnil, should be a fgl-sat-config object. See fgl-solving.
- sat-config-vacuity
- SAT config object for the vacuity check, if not
skipped. If NIL (the default), then instead uses the attachment for
(fgl-toplevel-vacuity-check-config). If nonnil, should be a fgl-sat-config object. See fgl-solving.
- toplevel-sat-check — fgl-toplevel-sat-check-mode-p
- If T (the default), then the FGL clause processor runs
the interpreter on the given goal and then tries to prove the validity of the
resulting Boolean expression using SAT. If :insert, a preprocessing step
inserts an fgl-prove wrapper around the conclusion of the conjecture so
that the SAT check will be attempted when the interpreter gets there.. If
:nil, then we do neither of these.
- skip-vacuity-check — booleanp
- If NIL, we use SAT to check vacuity of the
hypotheses. Set to T to disable this vacuity check.
Typically, instead of constructing an fgl-config object directly,
the user provides arguments to def-fgl-thm or def-fgl-param-thm.
In these macros, each field of the fgl-config object is assigned as follows:
- The explicit value given as a keyword argument to the macro, if there is one
- Else if the table fgl::fgl-config-table has an entry for the keyword field name, the value to which it is bound
- Else if the keyword field name prefixed by "FGL-" is bound as a state
global, its global value (e.g., keyword :fgl-trace-rewrites for the
trace-rewrites config field).
- Else the default value defined by make-fgl-config.
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->toplevel-sat-check
- Get the 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.
