Fgl-sat-check
Checking satisfiability of intermediate terms during FGL interpretation.
- Signature
(fgl-sat-check params x) → *
- Arguments
- params — Parameters for the SAT check -- typically of type fgl-sat-config.
- x — Object to check for satisfiability.
Logically, (fgl-sat-check params x) just returns x fixed to a
Boolean value. But when FGL symbolic execution encounters an
fgl-sat-check term, it checks Boolean satisfiability of x and if it
is able to prove that all evaluations of x are NIL, then it returns NIL;
otherwise, it returns x unchanged. To instead perform a validity check,
you could do:
(not (fgl-sat-check params (not x)))
It isn't necessary to call this around the entire conclusion of the theorem
you wish to prove -- FGL SAT-checks the final result of symbolically
executing the conclusion by default; see fgl-solving. The purpose of
fgl-sat-check is to force SAT checks during symbolic execution, so as
to e.g. avoid unnecessary execution paths.
The counterexamples from intermediate SAT checks may be pulled out of the
interpreter state during symbolic execution using syntax-bind forms.
For example, the rewrite rule show-counterexample-rw demonstrates how to
extract a counterexample from SAT and print it when a show-counterexample
term is encountered.
See also fgl-sat-check/print-counterexample for a version that prints
counterexample info for the stack frame from which it is called.
Definitions and Theorems
Function: fgl-sat-check
(defun fgl-sat-check (params x)
(declare (ignore params))
(declare (xargs :guard t))
(let ((__function__ 'fgl-sat-check))
(declare (ignorable __function__))
(if x t nil)))
Subtopics
- Fgl-ipasir-config
- Configuration object for IPASIR SAT checks in the default FGL configuration.
- Fgl-sat-config
- Configuration object for either monolithic or incremental SAT in the default FGL configuration.
