Logic form of ipasir-val. See ipasir for usage.
(ipasir-val$a solver lit) → val
Function:
(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:
(defthm return-type-of-ipasir-val$a (b* ((val (ipasir-val$a solver lit))) (or (bitp val) (not val))) :rule-classes :type-prescription)
Theorem:
(defthm ipasir-val$a-of-ipasir$a-fix-solver (equal (ipasir-val$a (ipasir$a-fix solver) lit) (ipasir-val$a solver lit)))
Theorem:
(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:
(defthm ipasir-val$a-of-lit-fix-lit (equal (ipasir-val$a solver (lit-fix lit)) (ipasir-val$a solver lit)))
Theorem:
(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)