Basic constructor macro for ipasir$a structures.
(make-ipasir$a [:formula <formula>] [:assumption <assumption>] [:new-clause <new-clause>] [:status <status>] [:solution <solution>] [:solved-assumption <solved-assumption>] [:callback-count <callback-count>] [:history <history>])
This is the usual way to construct ipasir$a structures. It simply conses together a structure with the specified fields.
This macro generates a new ipasir$a structure from scratch. See also change-ipasir$a, which can "change" an existing structure, instead.
This is an ordinary
(defmacro make-ipasir$a (&rest args) (std::make-aggregate 'ipasir$a args '((:formula) (:assumption) (:new-clause) (:status quote :undef) (:solution) (:solved-assumption) (:callback-count . 0) (:history)) 'make-ipasir$a nil))
(defun ipasir$a (formula assumption new-clause status solution solved-assumption callback-count history) (declare (xargs :guard (and (lit-list-listp formula) (lit-listp assumption) (lit-listp new-clause) (ipasir-status-p status) (lit-listp solution) (lit-listp solved-assumption) (natp callback-count)))) (declare (xargs :guard t)) (let ((__function__ 'ipasir$a)) (declare (ignorable __function__)) (b* ((formula (mbe :logic (lit-list-list-fix formula) :exec formula)) (assumption (mbe :logic (lit-list-fix assumption) :exec assumption)) (new-clause (mbe :logic (lit-list-fix new-clause) :exec new-clause)) (status (mbe :logic (ipasir-status-fix status) :exec status)) (solution (mbe :logic (lit-list-fix solution) :exec solution)) (solved-assumption (mbe :logic (lit-list-fix solved-assumption) :exec solved-assumption)) (callback-count (mbe :logic (nfix callback-count) :exec callback-count))) (list (cons 'formula formula) (cons 'assumption assumption) (cons 'new-clause new-clause) (cons 'status status) (cons 'solution solution) (cons 'solved-assumption solved-assumption) (cons 'callback-count callback-count) (cons 'history history)))))