		Search-engine friendly clone of the ACL2 documentation.

Satlink-parser-state

Satlink-parser-state->saw-unsat-p

Get the saw-unsat-p field from a satlink-parser-state.

Signature
(satlink-parser-state->saw-unsat-p x) → saw-unsat-p
Arguments: x — Guard (satlink-parser-state-p x).
Returns: saw-unsat-p — Type (booleanp saw-unsat-p).

This is an ordinary field accessor created by fty::defprod.

Definitions and Theorems

Function: satlink-parser-state->saw-unsat-p$inline

(defun satlink-parser-state->saw-unsat-p$inline (x)
  (declare (xargs :guard (satlink-parser-state-p x)))
  (declare (xargs :guard t))
  (let ((__function__ 'satlink-parser-state->saw-unsat-p))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((x (and t x)))
           (acl2::bool-fix (std::prod-car (std::prod-car x))))
         :exec (std::prod-car (std::prod-car x)))))

Theorem: booleanp-of-satlink-parser-state->saw-unsat-p

(defthm booleanp-of-satlink-parser-state->saw-unsat-p
  (b* ((saw-unsat-p (satlink-parser-state->saw-unsat-p$inline x)))
    (booleanp saw-unsat-p))
  :rule-classes :rewrite)

Theorem: satlink-parser-state->saw-unsat-p$inline-of-satlink-parser-state-fix-x

(defthm
 satlink-parser-state->saw-unsat-p$inline-of-satlink-parser-state-fix-x
 (equal (satlink-parser-state->saw-unsat-p$inline
             (satlink-parser-state-fix x))
        (satlink-parser-state->saw-unsat-p$inline x)))

Theorem: satlink-parser-state->saw-unsat-p$inline-satlink-parser-state-equiv-congruence-on-x

(defthm
 satlink-parser-state->saw-unsat-p$inline-satlink-parser-state-equiv-congruence-on-x
 (implies
      (satlink-parser-state-equiv x x-equiv)
      (equal (satlink-parser-state->saw-unsat-p$inline x)
             (satlink-parser-state->saw-unsat-p$inline x-equiv)))
 :rule-classes :congruence)