		Search-engine friendly clone of the ACL2 documentation.

Fraig-config

Make-fraig-config

Basic constructor macro for fraig-config structures.

Syntax

(make-fraig-config [:initial-sim-words <initial-sim-words>] 
                   [:initial-sim-rounds <initial-sim-rounds>] 
                   [:sim-words <sim-words>] 
                   [:ipasir-limit <ipasir-limit>] 
                   [:ipasir-recycle-count <ipasir-recycle-count>] 
                   [:ctrex-queue-limit <ctrex-queue-limit>] 
                   [:ctrex-force-resim <ctrex-force-resim>] 
                   [:final-force-resim <final-force-resim>] 
                   [:random-seed-name <random-seed-name>] 
                   [:outs-only <outs-only>] 
                   [:miters-only <miters-only>] 
                   [:delete-class-on-fail <delete-class-on-fail>] 
                   [:gatesimp <gatesimp>] 
                   [:level-limit <level-limit>] 
                   [:output-types <output-types>] 
                   [:save-candidate-equivs-as <save-candidate-equivs-as>] 
                   [:remove-candidate-equivs <remove-candidate-equivs>])

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

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

Definition

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

Macro: make-fraig-config

(defmacro make-fraig-config (&rest args)
  (std::make-aggregate 'fraig-config
                       args
                       '((:initial-sim-words . 4)
                         (:initial-sim-rounds . 10)
                         (:sim-words . 1)
                         (:ipasir-limit . 8)
                         (:ipasir-recycle-count . 1000)
                         (:ctrex-queue-limit . 16)
                         (:ctrex-force-resim . t)
                         (:final-force-resim)
                         (:random-seed-name)
                         (:outs-only)
                         (:miters-only)
                         (:delete-class-on-fail . 0)
                         (:gatesimp default-gatesimp)
                         (:level-limit . 0)
                         (:output-types)
                         (:save-candidate-equivs-as)
                         (:remove-candidate-equivs))
                       'make-fraig-config
                       nil))

Function: fraig-config

(defun fraig-config
       (initial-sim-words initial-sim-rounds
                          sim-words ipasir-limit
                          ipasir-recycle-count ctrex-queue-limit
                          ctrex-force-resim final-force-resim
                          random-seed-name outs-only
                          miters-only delete-class-on-fail
                          gatesimp level-limit
                          output-types save-candidate-equivs-as
                          remove-candidate-equivs)
 (declare (xargs :guard (and (posp initial-sim-words)
                             (posp initial-sim-rounds)
                             (posp sim-words)
                             (acl2::maybe-natp ipasir-limit)
                             (acl2::maybe-natp ipasir-recycle-count)
                             (acl2::maybe-natp ctrex-queue-limit)
                             (booleanp ctrex-force-resim)
                             (booleanp final-force-resim)
                             (symbolp random-seed-name)
                             (booleanp outs-only)
                             (booleanp miters-only)
                             (natp delete-class-on-fail)
                             (gatesimp-p gatesimp)
                             (natp level-limit)
                             (fraig-output-type-map-p output-types)
                             (symbolp save-candidate-equivs-as)
                             (symbolp remove-candidate-equivs))))
 (declare (xargs :guard t))
 (let ((__function__ 'fraig-config))
  (declare (ignorable __function__))
  (b* ((initial-sim-words (mbe :logic (pos-fix initial-sim-words)
                               :exec initial-sim-words))
       (initial-sim-rounds (mbe :logic (pos-fix initial-sim-rounds)
                                :exec initial-sim-rounds))
       (sim-words (mbe :logic (pos-fix sim-words)
                       :exec sim-words))
       (ipasir-limit (mbe :logic (acl2::maybe-natp-fix ipasir-limit)
                          :exec ipasir-limit))
       (ipasir-recycle-count
            (mbe :logic (acl2::maybe-natp-fix ipasir-recycle-count)
                 :exec ipasir-recycle-count))
       (ctrex-queue-limit
            (mbe :logic (acl2::maybe-natp-fix ctrex-queue-limit)
                 :exec ctrex-queue-limit))
       (ctrex-force-resim
            (mbe :logic (acl2::bool-fix ctrex-force-resim)
                 :exec ctrex-force-resim))
       (final-force-resim
            (mbe :logic (acl2::bool-fix final-force-resim)
                 :exec final-force-resim))
       (random-seed-name
            (mbe :logic (acl2::symbol-fix random-seed-name)
                 :exec random-seed-name))
       (outs-only (mbe :logic (acl2::bool-fix outs-only)
                       :exec outs-only))
       (miters-only (mbe :logic (acl2::bool-fix miters-only)
                         :exec miters-only))
       (delete-class-on-fail (mbe :logic (nfix delete-class-on-fail)
                                  :exec delete-class-on-fail))
       (gatesimp (mbe :logic (gatesimp-fix gatesimp)
                      :exec gatesimp))
       (level-limit (mbe :logic (nfix level-limit)
                         :exec level-limit))
       (output-types
            (mbe :logic (fraig-output-type-map-fix output-types)
                 :exec output-types))
       (save-candidate-equivs-as
            (mbe :logic (acl2::symbol-fix save-candidate-equivs-as)
                 :exec save-candidate-equivs-as))
       (remove-candidate-equivs
            (mbe :logic (acl2::symbol-fix remove-candidate-equivs)
                 :exec remove-candidate-equivs)))
    (cons :fraig-config (list (cons 'initial-sim-words
                                    initial-sim-words)
                              (cons 'initial-sim-rounds
                                    initial-sim-rounds)
                              (cons 'sim-words sim-words)
                              (cons 'ipasir-limit ipasir-limit)
                              (cons 'ipasir-recycle-count
                                    ipasir-recycle-count)
                              (cons 'ctrex-queue-limit
                                    ctrex-queue-limit)
                              (cons 'ctrex-force-resim
                                    ctrex-force-resim)
                              (cons 'final-force-resim
                                    final-force-resim)
                              (cons 'random-seed-name
                                    random-seed-name)
                              (cons 'outs-only outs-only)
                              (cons 'miters-only miters-only)
                              (cons 'delete-class-on-fail
                                    delete-class-on-fail)
                              (cons 'gatesimp gatesimp)
                              (cons 'level-limit level-limit)
                              (cons 'output-types output-types)
                              (cons 'save-candidate-equivs-as
                                    save-candidate-equivs-as)
                              (cons 'remove-candidate-equivs
                                    remove-candidate-equivs))))))