Satlink-parse-output
- Signature
(satlink-parse-output out env$) → (mv status env$)
- Arguments
- out — output lines from the SAT solver.
Guard (string-listp out).
- env$ — empty env to populate, should be sized already.
- Returns
- status — Either :failed, :sat, or :unsat.
- env$ — Variable assignment, in the :sat case.
Definitions and Theorems
Function: satlink-parse-output
(defun satlink-parse-output (out env$)
(declare (xargs :stobjs (env$)))
(declare (xargs :guard (string-listp out)))
(let ((__function__ 'satlink-parse-output))
(declare (ignorable __function__))
(b*
(((mv error-p (satlink-parser-state pstate)
env$)
(satlink-handle-lines out (make-satlink-parser-state)
env$))
((when error-p) (mv :failed env$))
((when (and pstate.saw-unsat-p pstate.saw-sat-p))
(cw "SATLINK error: solver says both SAT and UNSAT~%")
(mv :failed env$))
((when (and pstate.saw-unsat-p
pstate.saw-unknown-p))
(cw "SATLINK error: solver says both UNSAT and UNKNOWN~%")
(mv :failed env$))
((when (and pstate.saw-sat-p pstate.saw-unknown-p))
(cw "SATLINK error: solver says both SAT and UNKNOWN~%")
(mv :failed env$))
((when (and pstate.saw-sat-p
(not pstate.saw-zero-p)))
(cw
"SATLINK error: solver says SAT but we didn't find a 0 in variable lines?~%")
(mv :failed env$))
((when (and pstate.saw-unsat-p pstate.saw-zero-p))
(cw
"SATLINK error: solver says UNSAT but is giving us variables?~%")
(mv :failed env$))
((when (and pstate.saw-unknown-p pstate.saw-zero-p))
(cw
"SATLINK error: solver says UNKNOWN but is giving us variables?~%")
(mv :failed env$))
((when pstate.saw-unsat-p)
(mv :unsat env$))
((when pstate.saw-sat-p) (mv :sat env$))
((when pstate.saw-unknown-p)
(mv :failed env$)))
(cw "SATLINK error: solver didn't report its result~%")
(mv :failed env$))))
