• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
      • Sat-solver-options
      • Config-p
      • Logical-story
      • Dimacs
        • Dimacs-export
        • Dimacs-interp
          • Satlink-handle-line
          • Satlink-parse-variable-line
          • Satlink-skip-ws
          • Satlink-parse-output
          • Satlink-handle-lines
      • 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

• Dimacs-interp

Satlink-handle-line

Signature

(satlink-handle-line line pstate env$) 
  → 
(mv error-p new-pstate env$)

Arguments

line — one line of sat solver output.
    Guard (stringp line).

pstate — Guard (satlink-parser-state-p pstate).

env$ — evolving variable bindings.

Returns

error-p — did we see something we don't understand?.

new-pstate — Type (satlink-parser-state-p new-pstate).

Definitions and Theorems

Function: satlink-handle-line

(defun satlink-handle-line (line pstate env$)
 (declare (xargs :stobjs (env$)))
 (declare (xargs :guard (and (stringp line)
                             (satlink-parser-state-p pstate))))
 (let ((__function__ 'satlink-handle-line))
  (declare (ignorable __function__))
  (b*
   ((len (length line))
    ((when (< len 2))
     (mv nil (satlink-parser-state-fix pstate)
         env$))
    (char (char line 0))
    ((unless (and (or (eql char #\s) (eql char #\v))
                  (eql (char line 1) #\Space)))
     (mv nil (satlink-parser-state-fix pstate)
         env$))
    ((when (eql char #\s))
     (cond ((str::strprefixp "s SATISFIABLE" line)
            (mv nil
                (change-satlink-parser-state pstate
                                             :saw-sat-p t)
                env$))
           ((str::strprefixp "s UNSATISFIABLE" line)
            (mv nil
                (change-satlink-parser-state pstate
                                             :saw-unsat-p t)
                env$))
           ((str::strprefixp "s UNKNOWN" line)
            (mv nil
                (change-satlink-parser-state pstate
                                             :saw-unknown-p t)
                env$))
           (t (prog2$ (cw "SATLINK: Unrecognized result line: ~s0~%"
                          line)
                      (mv nil (satlink-parser-state-fix pstate)
                          env$)))))
    ((when (satlink-parser-state->saw-zero-p pstate))
     (cw "SATLINK: Variable lines after already saw zero: ~s0~%"
         line)
     (mv t (satlink-parser-state-fix pstate)
         env$))
    ((mv error saw-zero-p env$)
     (satlink-parse-variable-line line 1 len nil env$)))
   (mv error
       (change-satlink-parser-state pstate
                                    :saw-zero-p (and saw-zero-p t))
       env$))))

Theorem: satlink-parser-state-p-of-satlink-handle-line.new-pstate

(defthm satlink-parser-state-p-of-satlink-handle-line.new-pstate
  (b* (((mv ?error-p ?new-pstate ?env$)
        (satlink-handle-line line pstate env$)))
    (satlink-parser-state-p new-pstate))
  :rule-classes :rewrite)