		Search-engine friendly clone of the ACL2 documentation.

Ipasir$a

Make-ipasir$a

Basic constructor macro for ipasir$a structures.

Syntax

(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.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-ipasir$a

(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))

Function: ipasir$a

(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)))))