Proving SAT instances in FGL
Calls of SAT in FGL are controlled by configuration objects of the type
fgl-sat-config. (An exception is when the default attachment of the
stub function interp-st-sat-check is changed by the user; this topic
pertains to the usual situation where its attachment is
When FGL calls SAT automatically on the result of symbolically executing a
theorem, the fgl-sat-config object that is used is the result of calling
the attachable stub function fgl-toplevel-sat-check-config. When FGL
rewrite rules or top-level theorems call SAT using fgl-sat-check, the
configuration object is provided as an argument to that function.
An fgl-sat-config object is either an fgl-satlink-monolithic-sat-config or an fgl-ipasir-config object. When
it is a fgl-satlink-monolithic-sat-config, satisfiability is checked by
perhaps performing some
and subsequently calling a
When it is an fgl-ipasir-config, satisfiability is
checked by calling an
incremental SAT shared library, which may allow the
current check to benefit from learned lemmas and heuristic information from
Both the fgl-satlink-monolithic-sat-config and fgl-ipasir-config types are simple tagged products, and they have two fields
- ignore-pathcond says to ignore the path condition when checking satisfiability
- ignore-constraint says to ignore the constraint condition (see def-fgl-boolean-constraint when checking satisfiability.
The other fields of the fgl-satlink-monolithic-sat-config object are
- satlink-config-override may either be a satlink::config object
or nil. If set, this object determines how to call SAT, e.g., what
command-line solver to use. If not, the SATLINK configuration object used is
the attachment of the stub function fgl-satlink-config.
- transform is a Boolean value; if T, then AIGNET transforms are
used to simplify the problem before calling the solver.
- transform-config-override is a list of AIGNET transform configuration
objects; see aignet::aignet-comb-transforms. If empty, the attachment
of the stub function fgl-aignet-transforms-config is used as the list of
The other fields of the fgl-ipasir-config object are:
- ipasir-callback-limit may be nil or a natural number. If a number, it
provides a work limit for the incremental SAT checker, the precise meaning of
which depends on the solver but is generally a conflict or restart count.
- ipasir-recycle-callback-limit may be nil or a natural number. If a
number, it causes the solver object to be destroyed and recreated after the
given number of callbacks, which may be important for performance.
- ipasir-index is a natural number, default 0. This determines which
solver object is used. If a new ipasir index is used, then a new solver object
is created and initialized, and every subsequent use of that ipasir index
refers to that solver object (until perhaps the recycle-callback-limit causes
it to be reinitialized).
- Checking satisfiability of intermediate terms during FGL interpretation.
- Check satisfiability during FGL interpretation and print counterexamples.