Config-p
Settings for which SAT solver to run, how to invoke it, what output
to print, etc.
(config-p x) is a defaggregate of the following fields.
- cmdline — Command line to use to invoke the SAT solver, except for the
filename. For instance, "lingeling" or
"glucose-cert"; see sat-solver-options.
Invariant (stringp cmdline).
- verbose — Should we print excessive output for debugging?.
Invariant (booleanp verbose).
- timing — Should we print stylized timing messages from the solver? E.g.,
"c Sat solving took 103 seconds."
The verbose setting overrides this.
Invariant (booleanp timing).
- mintime — Minimum amount of time that is worth reporting for the overall run.
This gets passed to time$ as we do, e.g., our export to DIMACS
and invoke the SAT solver.
- remove-temps — Should temporary files (e.g., DIMACS files) be removed after
we're done calling SAT? Usually you will want to remove
them, but occasionally they may be useful for debugging, or
for comparing SAT solvers' performance. Note that these
files are created with oslib::tempfile, see its
documentation for details about their paths and filenames.
Invariant (booleanp remove-temps).
- lrat-check — Should we check an LRAT proof output by the solver? When this
is set, SATLINK will use the Heule/Hunt/Kaufmann checker from
projects/sat/lrat/stobj-based to check an LRAT proof which should
be output to file [input filename].lrat.
Invariant (booleanp lrat-check).
Source link: config-p
A config-p object controls how routines like sat will
invoke the SAT solver.
Subtopics
- Config
- Raw constructor for config-p structures.
- Make-config
- Constructor macro for config-p structures.
- Change-config
- A copying macro that lets you create new config-p structures, based on existing structures.
- Honsed-config
- Raw constructor for honsed config-p structures.
- Make-honsed-config
- Constructor macro for honsed config-p structures.
- *default-config*
- Default SAT solver configuration for routines like sat.
- Config->verbose
- Access the verbose field of a config-p structure.
- Config->timing
- Access the timing field of a config-p structure.
- Config->remove-temps
- Access the remove-temps field of a config-p structure.
- Config->mintime
- Access the mintime field of a config-p structure.
- Config->lrat-check
- Access the lrat-check field of a config-p structure.
- Config->cmdline
- Access the cmdline field of a config-p structure.
