		Search-engine friendly clone of the ACL2 documentation.

Satlink-parser-state

Satlink-parser-state-p

Recognizer for satlink-parser-state structures.

Signature
(satlink-parser-state-p x) → *

Definitions and Theorems

Function: satlink-parser-state-p

(defun satlink-parser-state-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'satlink-parser-state-p))
    (declare (ignorable __function__))
    (and (std::prod-consp x)
         (std::prod-consp (std::prod-car x))
         (std::prod-consp (std::prod-cdr x))
         (b* ((saw-unsat-p (std::prod-car (std::prod-car x)))
              (saw-sat-p (std::prod-cdr (std::prod-car x)))
              (saw-unknown-p (std::prod-car (std::prod-cdr x)))
              (saw-zero-p (std::prod-cdr (std::prod-cdr x))))
           (and (booleanp saw-unsat-p)
                (booleanp saw-sat-p)
                (booleanp saw-unknown-p)
                (booleanp saw-zero-p))))))