		Search-engine friendly clone of the ACL2 documentation.

Balance-config

Make-balance-config

Basic constructor macro for balance-config structures.

Syntax

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

Definition

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

Macro: make-balance-config

(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: balance-config

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