Fraig-config
Configuration object for the fraig aignet transform.
This is a product type introduced by fty::defprod.
Fields
- initial-sim-words — posp
- Number of 32-bit simulation words per node for initial simulation
- initial-sim-rounds — posp
- Number of times to simulate initially
- sim-words — posp
- Number of 32-bit simulation words per node for simulation during fraiging
- ipasir-limit — ACL2::maybe-natp
- Ipasir effort limit
- ipasir-recycle-count — ACL2::maybe-natp
- Number of callbacks after which to recycle the solver
- ctrex-queue-limit — ACL2::maybe-natp
- Limit to number of counterexamples that may be queued before resimulation
- ctrex-force-resim — booleanp
- Force resimulation of a counterexample before checking another node in the same equivalence class
- final-force-resim — booleanp
- Force resimulation of any pending counterexamples at the
end of the sweep. Useful when a subsequent FRAIG transform will use (with the
output-types option) this transform's resulting equivalence classes (stored
with the save-candidate-equivs-as option) (see fraig).
- random-seed-name — symbolp
- Name to use for seed-random, or NIL to not reseed the random number generator
- outs-only — booleanp
- Only check the combinational outputs of the network
- miters-only — booleanp
- Instead of starting with all nodes in a single equivalence
class and refining them with random simulation, start with equivalence classes
consisting of the mitered outputs of the network. That is, whenever an output contains
an XOR under a top-level conjunction, put the inputs of that XOR into an
equivalence class. This is useful for checking equivalences when you know
exactly which nodes in a network are supposed to be equivalent, because it
avoids checking false equivalences.
- delete-class-on-fail — natp
- If set greater than 0, then if a SAT check fails, don't try to prove any
of the other equivalences in that node's equiv class (delete the class), unless
it was the constant class. If set greater than 1, delete the class even if
it's the constant class (drastic!).
- gatesimp — gatesimp
- Gate simplification parameters. Warning: This transform will do
nothing good if hashing is turned off.
- level-limit — natp
- If set greater than 0, we'll only try to check the current
node's candidatae equivalence if its level (see aignet-record-levels) is
less than or equal to the level limit.
- output-types — fraig-output-type-map
- If this is empty, then all outputs are treated as nodes to
simplify. Otherwise, it gives a mapping from output range names (see aignet-output-ranges) to fraig-output-type objects, determining how to
treat the named ranges of objects. (This depends on the output-types argument
to the transform, which determines which range of outputs corresponds to each
output range name.) The default output type is
(fraig-output-type-simplify).
- save-candidate-equivs-as — symbolp
- If this is a nonnil symbol and this transform is
called with strict-count nonnil (i.e. only preserving a fixed number of primary
outputs, not full combinational equivalence), then at the end of the SAT sweep,
a new output range (see aignet-output-ranges) of the given name is added
to the resulting AIG, encoding the remaining equivalence classes that were
neither proved nor disproved. If an output range of that name already exists,
then it is replaced. This can be consumed in a subsequent FRAIG transform by
mapping this symbol to (fraig-output-type-initial-equiv-classes) in the
output-types map. This can speed up that subsequent FRAIG transform since it
doesn't need to re-disprove candidate equivalences for which we have already
found counterexamples.
- remove-candidate-equivs — symbolp
- If this is a nonnil symbol and this transform is
called with strict-count nonnil (i.e. only preserving a fixed number of primary
outputs, not full combinational equivalence), then at the end of the SAT sweep,
the given output range will be deleted. This is intended to be used to remove a
set of candidate equivalences that is no longer useful (e.g. because this is
the last FRAIG transform in the sequence), but it will in fact remove any
output range.
Subtopics
- Make-fraig-config
- Basic constructor macro for fraig-config structures.
- Fraig-config-fix
- Fixing function for fraig-config structures.
- Fraig-config-p
- Recognizer for fraig-config structures.
- Change-fraig-config
- Modifying constructor for fraig-config structures.
- Fraig-config-equiv
- Basic equivalence relation for fraig-config structures.
- Fraig-config->save-candidate-equivs-as
- Get the save-candidate-equivs-as field from a fraig-config.
- Fraig-config->remove-candidate-equivs
- Get the remove-candidate-equivs field from a fraig-config.
- Fraig-config->ipasir-recycle-count
- Get the ipasir-recycle-count field from a fraig-config.
- Fraig-config->delete-class-on-fail
- Get the delete-class-on-fail field from a fraig-config.
- Fraig-config->ctrex-queue-limit
- Get the ctrex-queue-limit field from a fraig-config.
- Fraig-config->random-seed-name
- Get the random-seed-name field from a fraig-config.
- Fraig-config->output-types
- Get the output-types field from a fraig-config.
- Fraig-config->initial-sim-words
- Get the initial-sim-words field from a fraig-config.
- Fraig-config->initial-sim-rounds
- Get the initial-sim-rounds field from a fraig-config.
- Fraig-config->final-force-resim
- Get the final-force-resim field from a fraig-config.
- Fraig-config->ctrex-force-resim
- Get the ctrex-force-resim field from a fraig-config.
- Fraig-config->miters-only
- Get the miters-only field from a fraig-config.
- Fraig-config->level-limit
- Get the level-limit field from a fraig-config.
- Fraig-config->ipasir-limit
- Get the ipasir-limit field from a fraig-config.
- Fraig-config->sim-words
- Get the sim-words field from a fraig-config.
- Fraig-config->outs-only
- Get the outs-only field from a fraig-config.
- Fraig-config->gatesimp
- Get the gatesimp field from a fraig-config.
