(satlink-parse-output out env$) → (mv status env$)
Function:
(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$))))