Basic constructor macro for balance-config structures.
(make-balance-config [:search-higher-levels <search-higher-levels>] [:search-second-lit <search-second-lit>] [:search-limit <search-limit>] [:supergate-limit <supergate-limit>] [:verbosity-level <verbosity-level>] [:gatesimp <gatesimp>])
This is the usual way to construct balance-config structures. It simply conses together a structure with the specified fields.
This macro generates a new balance-config structure from scratch. See also change-balance-config, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-balance-config (&rest args) (std::make-aggregate 'balance-config args '((:search-higher-levels . t) (:search-second-lit . t) (:search-limit . 1000) (:supergate-limit . 1000) (:verbosity-level . 0) (:gatesimp default-gatesimp)) 'make-balance-config nil))
Function:
(defun balance-config (search-higher-levels search-second-lit search-limit supergate-limit verbosity-level gatesimp) (declare (xargs :guard (and (booleanp search-higher-levels) (booleanp search-second-lit) (natp search-limit) (posp supergate-limit) (natp verbosity-level) (gatesimp-p gatesimp)))) (declare (xargs :guard t)) (let ((__function__ 'balance-config)) (declare (ignorable __function__)) (b* ((search-higher-levels (mbe :logic (acl2::bool-fix search-higher-levels) :exec search-higher-levels)) (search-second-lit (mbe :logic (acl2::bool-fix search-second-lit) :exec search-second-lit)) (search-limit (mbe :logic (nfix search-limit) :exec search-limit)) (supergate-limit (mbe :logic (pos-fix supergate-limit) :exec supergate-limit)) (verbosity-level (mbe :logic (nfix verbosity-level) :exec verbosity-level)) (gatesimp (mbe :logic (gatesimp-fix gatesimp) :exec gatesimp))) (cons :balance-config (list (cons 'search-higher-levels search-higher-levels) (cons 'search-second-lit search-second-lit) (cons 'search-limit search-limit) (cons 'supergate-limit supergate-limit) (cons 'verbosity-level verbosity-level) (cons 'gatesimp gatesimp))))))