		Search-engine friendly clone of the ACL2 documentation.

Ipasir

Ipasir-val$c

Signature
(ipasir-val$c ipasir$c lit) → *
Arguments: lit — Guard (litp lit).

Definitions and Theorems

Function: ipasir-val$c

(defun ipasir-val$c (ipasir$c lit)
 (declare (xargs :stobjs (ipasir$c)))
 (declare (xargs :guard (litp lit)))
 (declare (xargs :guard (eq (ipasir$a->status (ipasir-get ipasir$c))
                            :sat)))
 (let ((__function__ 'ipasir-val$c))
   (declare (ignorable __function__))
   (ipasir-val$a (ipasir-get ipasir$c)
                 lit)))

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

(defthm ipasir-val$c-of-lit-fix-lit
  (equal (ipasir-val$c ipasir$c (lit-fix lit))
         (ipasir-val$c ipasir$c lit)))

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

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