• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
      • Sat-solver-options
      • Config-p
      • Logical-story
        • Satlink-run-impl
        • Satlink-run
      • 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

• Logical-story

Satlink-run-impl

Core function used to run the SAT solver.

Signature

(satlink-run-impl config cnf env$ &key (state 'state)) 
  → 
(mv status env$ lrat-proof state)

Arguments

config — Which solver to call, etc.
    Guard (config-p config).

cnf — The formula to solve.
    Guard (lit-list-listp cnf).

env$ — Empty env to populate, will usually be resized.

Returns

status — :sat, :unsat, or :failed.

env$ — Variable assignment, in the :sat case.

lrat-proof — LRAT proof, in the :unsat case, if config.lrat-check is set.

state — Type (state-p1 state), given (state-p1 state).

This function actually runs the SAT solver: it exports the formula into a dimacs file, invokes the SAT solver on it, and interprets the answer. This function is typically never used directly; instead see satlink-run.

Definitions and Theorems

Function: satlink-run-impl-fn

(defun satlink-run-impl-fn (config cnf env$ state)
 (declare (xargs :stobjs (env$ state)))
 (declare (xargs :guard (and (config-p config)
                             (lit-list-listp cnf))))
 (let ((__function__ 'satlink-run-impl))
  (declare (ignorable __function__))
  (b*
   (((config config))
    ((mv filename state)
     (oslib::tempfile "satlink"))
    ((unless filename)
     (cw "SATLINK: Error generating temporary filename.~%")
     (mv :failed env$ nil state))
    ((mv okp max-index state)
     (time$ (dimacs-export cnf :filename filename)
            :msg "; SATLINK: writing ~s0: ~st sec, ~sa bytes~%"
            :args (list filename)
            :mintime config.mintime))
    ((unless okp)
     (cw "SATLINK: Error writing dimacs file ~s0~%"
         filename)
     (mv :failed env$ nil state))
    ((acl2::fun (cleanup filename config state))
     (b* (((unless (config->remove-temps config))
           state)
          ((mv & & state)
           (tshell-call (str::cat "rm " filename))))
       state))
    (cmd (str::cat config.cmdline " " filename))
    ((mv status lines state)
     (time$ (tshell-call
                 cmd
                 :print (or (and config.verbose 'satlink-echo)
                            (and config.timing 'satlink-echo-time))
                 :save t)
            :msg "; SATLINK: `~s0`: ~st sec, ~sa bytes~%"
            :args (list cmd)
            :mintime config.mintime))
    ((when (eql status 127))
     (cw
      "SATLINK: Couldn't execute SAT solver command `~s0` (exit code 127).  Not in path?~%"
      cmd)
     (mv :failed env$ nil state))
    ((unless (string-listp lines))
     (cw "SATLINK: Tshell somehow didn't give us a string list.~%")
     (b* ((state (cleanup filename config state)))
       (mv :failed env$ nil state)))
    ((mv status env$)
     (time$
         (b* ((env$ (resize-bits (1+ max-index) env$))
              ((mv status env$)
               (satlink-parse-output lines env$)))
           (mv status env$))
         :msg "; SATLINK: interpreting output: ~st sec, ~sa bytes~%"
         :mintime config.mintime))
    ((mv lrat-proof state)
     (if
      (and (eq status :unsat)
           config.lrat-check)
      (b*
       ((lrat-proof
         (time$
              (lrat::lrat-read-file (str::cat filename ".lrat")
                                    state)
              :msg "; SATLINK: read lrat file: ~st sec, ~sa bytes~%"
              :mintime config.mintime))
        ((unless (config->remove-temps config))
         (mv lrat-proof state))
        ((mv & & state)
         (tshell-call
              (str::cat "rm " (str::cat filename ".lrat")))))
       (mv lrat-proof state))
      (mv nil state)))
    (state (if (or (eq status :sat) (eq status :unsat))
               (satlink-extra-hook cnf filename status env$ state)
             state))
    (state (cleanup filename config state)))
   (mv status env$ lrat-proof state))))

Theorem: state-p1-of-satlink-run-impl.state

(defthm state-p1-of-satlink-run-impl.state
  (implies (state-p1 state)
           (b* (((mv ?status ?env$ ?lrat-proof acl2::?state)
                 (satlink-run-impl-fn config cnf env$ state)))
             (state-p1 state)))
  :rule-classes :rewrite)