Add a clause (given as a list of literals) to the formula
(ipasir-add-list-ordered ipasir clause) → new-ipasir
Function:
(defun ipasir-add-list-ordered (ipasir clause) (declare (xargs :stobjs (ipasir))) (declare (xargs :guard (lit-listp clause))) (declare (xargs :guard (and (not (eq (ipasir-get-status ipasir) :undef)) (ipasir-empty-new-clause ipasir)))) (let ((__function__ 'ipasir-add-list-ordered)) (declare (ignorable __function__)) (b* ((ipasir (ipasir-cancel-new-clause ipasir)) (ipasir (ipasir-add-list-ordered-aux ipasir clause))) (ipasir-finalize-clause ipasir))))
Theorem:
(defthm ipasir-add-list-ordered-status (b* ((?new-ipasir (ipasir-add-list-ordered ipasir clause))) (equal (ipasir$a->status new-ipasir) :input)))
Theorem:
(defthm ipasir-add-list-ordered-formula (b* ((?new-ipasir (ipasir-add-list-ordered ipasir clause))) (equal (ipasir$a->formula new-ipasir) (cons (lit-list-fix clause) (ipasir$a->formula ipasir)))))
Theorem:
(defthm ipasir-add-list-ordered-new-clause (b* ((?new-ipasir (ipasir-add-list-ordered ipasir clause))) (not (ipasir$a->new-clause new-ipasir))))
Theorem:
(defthm ipasir-add-list-ordered-assumption (b* ((?new-ipasir (ipasir-add-list-ordered ipasir clause))) (equal (ipasir$a->assumption new-ipasir) (ipasir$a->assumption ipasir))))