		Search-engine friendly clone of the ACL2 documentation.

Ipasir$a

Ipasir-val$a

Logic form of ipasir-val. See ipasir for usage.

Signature
(ipasir-val$a solver lit) → val
Arguments: solver — Guard (ipasir$a-p solver).; lit — Guard (litp lit).
Returns: val — Type (or (bitp val) (not val)).

Definitions and Theorems

Function: ipasir-val$a

(defun
     ipasir-val$a (solver lit)
     (declare (xargs :guard (and (ipasir$a-p solver) (litp lit))))
     (declare (xargs :guard (eq (ipasir-get-status$a solver) :sat)))
     (let ((__function__ 'ipasir-val$a))
          (declare (ignorable __function__))
          (b* (((ipasir$a solver))
               (lit (lit-fix lit)))
              (lit-cube-val lit solver.solution))))

Theorem: return-type-of-ipasir-val$a

(defthm return-type-of-ipasir-val$a
        (b* ((val (ipasir-val$a solver lit)))
            (or (bitp val) (not val)))
        :rule-classes :type-prescription)

Theorem: ipasir-val$a-of-ipasir$a-fix-solver

(defthm ipasir-val$a-of-ipasir$a-fix-solver
        (equal (ipasir-val$a (ipasir$a-fix solver) lit)
               (ipasir-val$a solver lit)))

Theorem: ipasir-val$a-ipasir$a-equiv-congruence-on-solver

(defthm ipasir-val$a-ipasir$a-equiv-congruence-on-solver
        (implies (ipasir$a-equiv solver solver-equiv)
                 (equal (ipasir-val$a solver lit)
                        (ipasir-val$a solver-equiv lit)))
        :rule-classes :congruence)

Theorem: ipasir-val$a-of-lit-fix-lit

(defthm ipasir-val$a-of-lit-fix-lit
        (equal (ipasir-val$a solver (lit-fix lit))
               (ipasir-val$a solver lit)))

Theorem: ipasir-val$a-lit-equiv-congruence-on-lit

(defthm ipasir-val$a-lit-equiv-congruence-on-lit
        (implies (lit-equiv lit lit-equiv)
                 (equal (ipasir-val$a solver lit)
                        (ipasir-val$a solver lit-equiv)))
        :rule-classes :congruence)