		Search-engine friendly clone of the ACL2 documentation.

Balance-config

This is a product type introduced by fty::defprod.

search-higher-levels — booleanp: Says whether to search literals with higher fanin depths when looking for a pairing for a given literal. Tends to find more reductions, may take somewhat longer.
search-second-lit — booleanp: If no reducing pairing is found for the first literal of a supergate, says whether to search for a pairing for the next literal before defaulting to pairing it with the first literal. Tends to find more reductions but reduce the network depth less and take somewhat longer.
search-limit — natp: Search at most this many literals for a match.
supergate-limit — posp: Build supergates at most this big.
verbosity-level — natp: Controls the level of output during balance transformation. Level 0 will speed things up for larger aignets.
gatesimp — gatesimp: Gate simplification parameters. Warning: This transform will do nothing good if hashing is turned off.

Balance-config-fix: Fixing function for balance-config structures.
Make-balance-config: Basic constructor macro for balance-config structures.
Balance-config-p: Recognizer for balance-config structures.
Balance-config-equiv: Basic equivalence relation for balance-config structures.
Balance-config->search-higher-levels: Get the search-higher-levels field from a balance-config.
Balance-config->search-second-lit: Get the search-second-lit field from a balance-config.
Change-balance-config: Modifying constructor for balance-config structures.
Balance-config->verbosity-level: Get the verbosity-level field from a balance-config.
Balance-config->supergate-limit: Get the supergate-limit field from a balance-config.
Balance-config->search-limit: Get the search-limit field from a balance-config.
Balance-config->gatesimp: Get the gatesimp field from a balance-config.