		Search-engine friendly clone of the ACL2 documentation.

Fgl-exhaustive-test-config

Make-fgl-exhaustive-test-config

Basic constructor macro for fgl-exhaustive-test-config structures.

Syntax

(make-fgl-exhaustive-test-config [:ignore-pathcond <ignore-pathcond>] 
                                 [:ignore-constraint <ignore-constraint>] 
                                 [:transform <transform>] 
                                 [:transform-config-override <transform-config-override>] 
                                 [:random-iters <random-iters>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-fgl-exhaustive-test-config

(defmacro make-fgl-exhaustive-test-config (&rest args)
  (std::make-aggregate 'fgl-exhaustive-test-config
                       args
                       '((:ignore-pathcond)
                         (:ignore-constraint)
                         (:transform)
                         (:transform-config-override)
                         (:random-iters))
                       'make-fgl-exhaustive-test-config
                       nil))

Function: fgl-exhaustive-test-config

(defun fgl-exhaustive-test-config
       (ignore-pathcond ignore-constraint transform
                        transform-config-override random-iters)
 (declare (xargs :guard (and (booleanp ignore-pathcond)
                             (booleanp ignore-constraint)
                             (booleanp transform)
                             (acl2::maybe-natp random-iters))))
 (declare (xargs :guard t))
 (let ((__function__ 'fgl-exhaustive-test-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))
       (transform (mbe :logic (bool-fix transform)
                       :exec transform))
       (random-iters (mbe :logic (acl2::maybe-natp-fix random-iters)
                          :exec random-iters)))
    (cons :fgl-exhaustive-test-config
          (list (cons 'ignore-pathcond ignore-pathcond)
                (cons 'ignore-constraint
                      ignore-constraint)
                (cons 'transform transform)
                (cons 'transform-config-override
                      transform-config-override)
                (cons 'random-iters random-iters))))))