		Search-engine friendly clone of the ACL2 documentation.

Ipasir

Ipasir-failed$c

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

Definitions and Theorems

Function: ipasir-failed$c

(defun ipasir-failed$c (ipasir$c lit)
  (declare (xargs :stobjs (ipasir$c)))
  (declare (xargs :guard (litp lit)))
  (declare (xargs :guard
                  (b* (((ipasir$a solver)
                        (ipasir-get ipasir$c)))
                    (and (eq solver.status :unsat)
                         (member lit solver.solved-assumption)))))
  (let ((__function__ 'ipasir-failed$c))
    (declare (ignorable __function__))
    (ipasir-failed$a (ipasir-get ipasir$c)
                     lit)))

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

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

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

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