		Search-engine friendly clone of the ACL2 documentation.

Fgl-ipasir-config

Make-fgl-ipasir-config

Basic constructor macro for fgl-ipasir-config structures.

Syntax

(make-fgl-ipasir-config [:ignore-pathcond <ignore-pathcond>] 
                        [:ignore-constraint <ignore-constraint>] 
                        [:ipasir-callback-limit <ipasir-callback-limit>] 
                        [:ipasir-recycle-callback-limit <ipasir-recycle-callback-limit>] 
                        [:ipasir-index <ipasir-index>])

This is the usual way to construct fgl-ipasir-config structures. It simply conses together a structure with the specified fields.

This macro generates a new fgl-ipasir-config structure from scratch. See also change-fgl-ipasir-config, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-fgl-ipasir-config

(defmacro make-fgl-ipasir-config (&rest args)
  (std::make-aggregate 'fgl-ipasir-config
                       args
                       '((:ignore-pathcond)
                         (:ignore-constraint)
                         (:ipasir-callback-limit)
                         (:ipasir-recycle-callback-limit)
                         (:ipasir-index quote 0))
                       'make-fgl-ipasir-config
                       nil))

Function: fgl-ipasir-config

(defun fgl-ipasir-config
       (ignore-pathcond ignore-constraint ipasir-callback-limit
                        ipasir-recycle-callback-limit
                        ipasir-index)
 (declare
   (xargs
        :guard (and (booleanp ignore-pathcond)
                    (booleanp ignore-constraint)
                    (acl2::maybe-natp ipasir-callback-limit)
                    (acl2::maybe-natp ipasir-recycle-callback-limit)
                    (natp ipasir-index))))
 (declare (xargs :guard t))
 (let ((__function__ 'fgl-ipasir-config))
  (declare (ignorable __function__))
  (b*
   ((ignore-pathcond (mbe :logic (bool-fix ignore-pathcond)
                          :exec ignore-pathcond))
    (ignore-constraint (mbe :logic (bool-fix ignore-constraint)
                            :exec ignore-constraint))
    (ipasir-callback-limit
         (mbe :logic (acl2::maybe-natp-fix ipasir-callback-limit)
              :exec ipasir-callback-limit))
    (ipasir-recycle-callback-limit
     (mbe
         :logic (acl2::maybe-natp-fix ipasir-recycle-callback-limit)
         :exec ipasir-recycle-callback-limit))
    (ipasir-index (mbe :logic (nfix ipasir-index)
                       :exec ipasir-index)))
   (cons
    :fgl-ipasir-config (list (cons 'ignore-pathcond ignore-pathcond)
                             (cons 'ignore-constraint
                                   ignore-constraint)
                             (cons 'ipasir-callback-limit
                                   ipasir-callback-limit)
                             (cons 'ipasir-recycle-callback-limit
                                   ipasir-recycle-callback-limit)
                             (cons 'ipasir-index ipasir-index))))))