		Search-engine friendly clone of the ACL2 documentation.

Balance-config

Change-balance-config

Modifying constructor for balance-config structures.

Syntax

(change-balance-config x 
                       [: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 an often useful alternative to make-balance-config.

We construct a new balance-config structure that is a copy of x, except that you can explicitly change some particular fields. Any fields you don't mention just keep their values from x.

Definition

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

Macro: change-balance-config

(defmacro change-balance-config (x &rest args)
 (std::change-aggregate
    'balance-config
    x args
    '((:search-higher-levels . balance-config->search-higher-levels)
      (:search-second-lit . balance-config->search-second-lit)
      (:search-limit . balance-config->search-limit)
      (:supergate-limit . balance-config->supergate-limit)
      (:verbosity-level . balance-config->verbosity-level)
      (:gatesimp . balance-config->gatesimp))
    'change-balance-config
    'nil))