• Top
    • Documentation
    • Books
    • Boolean-reasoning
      • Ipasir
      • Aignet
      • Aig
      • Satlink
        • Sat-solver-options
        • Config-p
          • Config
          • Make-config
          • Change-config
          • Honsed-config
          • Make-honsed-config
          • *default-config*
          • Config->verbose
          • Config->timing
          • Config->remove-temps
          • Config->mintime
          • Config->lrat-check
          • Config->cmdline
        • Logical-story
        • Dimacs
        • Gather-benchmarks
        • Cnf
        • Satlink-extra-hook
        • Sat
      • Truth
      • Ubdds
      • Bdd
      • Faig
      • Bed
      • 4v
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Satlink

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.