		Search-engine friendly clone of the ACL2 documentation.

Ipasir

Ipasir-solve$c

Signature
(ipasir-solve$c ipasir$c) → (mv * ipasir$c)

Definitions and Theorems

Function: ipasir-solve$c

(defun ipasir-solve$c (ipasir$c)
 (declare (xargs :stobjs (ipasir$c)))
 (declare
  (xargs
       :guard (and (not (eq (ipasir$a->status (ipasir-get ipasir$c))
                            :undef))
                   (eq (ipasir$a->new-clause (ipasir-get ipasir$c))
                       nil))))
 (let ((__function__ 'ipasir-solve$c))
   (declare (ignorable __function__))
   (b* (((mv status solver)
         (ipasir-solve$a (ipasir-get ipasir$c)))
        (ipasir$c (ipasir-set solver ipasir$c)))
     (mv status ipasir$c))))