		Search-engine friendly clone of the ACL2 documentation.

Parametrize

Parametrize-config

Config object for the parametrize AIG transform

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

Fields

build-limit — natp: BDD size limit when recursively building from AIGs.
conjoin-limit — natp: Bdd size limit when conjoining hypotheses together. Should be at least as big as build-limit.
output-types — parametrize-output-type-map: Mapping from output range names (see aignet-output-ranges) to parametrize-output-type objects, indicating that the outputs are to be treated specially. The default output type is (parametrize-output-type-param).))

Two of the fields configure BDD size limits. These limits put an approximate upper bound on the size of BDDs, and are maintained by checking after each BDD operation to see if the limit is violated. Size limit violations are dealt with by using an overapproximation of the assumption, which is sound but may not be useful.

Subtopics

Parametrize-output-type: Indicator of how the parametrize transform should treat a range of outputs
Parametrize-config-fix: Fixing function for parametrize-config structures.
Parametrize-config-equiv: Basic equivalence relation for parametrize-config structures.
Make-parametrize-config: Basic constructor macro for parametrize-config structures.
Parametrize-config->output-types: Get the output-types field from a parametrize-config.
Parametrize-config->conjoin-limit: Get the conjoin-limit field from a parametrize-config.
Parametrize-config->build-limit: Get the build-limit field from a parametrize-config.
Change-parametrize-config: Modifying constructor for parametrize-config structures.
Parametrize-config-p: Recognizer for parametrize-config structures.