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