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