(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 saw-unsat-p saw-sat-p saw-zero-p env$) (satlink-handle-lines out nil nil nil env$)) ((when error-p) (mv :failed env$)) ((when (and saw-unsat-p saw-sat-p)) (cw "SATLINK: solver says both SAT and UNSAT? Uh... guys?") (mv :failed env$)) ((when (and saw-sat-p (not saw-zero-p))) (cw "SATLINK: solver says SAT but we didn't find a 0 in variable lines?") (mv :failed env$)) ((when (and saw-unsat-p saw-zero-p)) (cw "SATLINK: solver says UNSAT but is giving us variables?") (mv :failed env$)) ((when saw-unsat-p) (mv :unsat env$)) ((when saw-sat-p) (mv :sat env$))) (mv :failed env$))))