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.
- stacklimit — posp
- Limit on the number of major frames (rewrite rule applications) on FGL's
stack. Set smaller to catch rewrite rules faster. Similar to reclimit, but maybe easier for
users to predict the behavior.
- steplimit — posp
- Limit on the number of steps (rewrite / meta rule applications) in an FGL run.
- 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.
- counterexample-analysis-enabledp — booleanp
- If T (the default), then the FGL clause processor will try to analyze and run
counterexamples. Specifically, if the interpreter finishes and the (SAT-based)
validity check of its result produces a counterexample, the SAT counterexample
will be analyzed to try and create a counterexample to the conjecture (in terms
of its original variables). This also affects any rewrite rules that call
interp-st-run-ctrex (it will exit without running the counterexample).
- 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.
- evisc-tuple
- Evisc tuple to use for printing potentially large objects.
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->counterexample-analysis-enabledp
- Get the counterexample-analysis-enabledp field from a fgl-config.
- Change-fgl-config
- Modifying constructor 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.
- Fgl-config->function-modes
- Get the function-modes field from a fgl-config.
- Fgl-config->skip-vacuity-check
- Get the skip-vacuity-check 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->steplimit
- Get the steplimit field from a fgl-config.
- Fgl-config->stacklimit
- Get the stacklimit field from a fgl-config.
- Fgl-config->reclimit
- Get the reclimit field from a fgl-config.
- Fgl-config->make-ites
- Get the make-ites 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.
- Fgl-config->evisc-tuple
- Get the evisc-tuple field from a fgl-config.
