• Top
    • Documentation
    • Books
    • Boolean-reasoning
      • Ipasir
      • Aignet
        • Base-api
        • Aignet-construction
        • Representation
        • Aignet-copy-init
        • Aignet-simplify-with-tracking
        • Aignet-simplify-marked-with-tracking
        • Aignet-cnf
        • Aignet-simplify-marked
        • Aignet-complete-copy
        • Aignet-transforms
          • Aignet-output-ranges
          • Aignet-comb-transforms
            • Fraig
            • Parametrize
            • Observability-fix
            • Constprop
            • Apply-m-assumption-n-output-output-transform-default
            • Balance
            • Apply-n-output-comb-transform-default
            • Apply-comb-transform-default
            • Obs-constprop
              • Obs-constprop-config
                • Obs-constprop-config-fix
                • Obs-constprop-config-equiv
                • Make-obs-constprop-config
                • Obs-constprop-config->obs-hyp-max-size
                • Obs-constprop-config->obs-concl-min-size
                • Obs-constprop-config->constprop-iterations
                • Obs-constprop-config->obs-min-ratio
                • Obs-constprop-config->gatesimp
                • Change-obs-constprop-config
                • Obs-constprop-config-p
              • Obs-constprop!
            • Rewrite
            • Comb-transform
            • Abc-comb-simplify
            • Prune
            • Rewrite!
            • M-assumption-n-output-comb-transform->name
            • N-output-comb-transform->name
            • Comb-transform->name
            • N-output-comb-transformlist
            • M-assumption-n-output-comb-transformlist
            • Comb-transformlist
            • Apply-comb-transform
          • Aignet-m-assumption-n-output-transforms
          • Aignet-n-output-comb-transforms
        • Aignet-eval
        • Semantics
        • Aignet-read-aiger
        • Aignet-write-aiger
        • Aignet-abc-interface
        • Utilities
      • Aig
      • Satlink
      • Truth
      • Ubdds
      • Bdd
      • Faig
      • Bed
      • 4v
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Obs-constprop
  • Comb-transform

Obs-constprop-config

Configuration object for the obs-constprop aignet transform.

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

Fields
gatesimp — gatesimp
Gate simplification parameters. Warning: This transform will do nothing good if hashing is turned off.
constprop-iterations — natp
Number of constant propagation iterations.
obs-hyp-max-size — ACL2::maybe-natp
Maximum fanin cone size for the hyp
obs-concl-min-size — ACL2::maybe-natp
Minimum fanin cone size for the conclusion
obs-min-ratio — rationalp
Minimum ratio of conclusion to hyp

Subtopics

Obs-constprop-config-fix
Fixing function for obs-constprop-config structures.
Obs-constprop-config-equiv
Basic equivalence relation for obs-constprop-config structures.
Make-obs-constprop-config
Basic constructor macro for obs-constprop-config structures.
Obs-constprop-config->obs-hyp-max-size
Get the obs-hyp-max-size field from a obs-constprop-config.
Obs-constprop-config->obs-concl-min-size
Get the obs-concl-min-size field from a obs-constprop-config.
Obs-constprop-config->constprop-iterations
Get the constprop-iterations field from a obs-constprop-config.
Obs-constprop-config->obs-min-ratio
Get the obs-min-ratio field from a obs-constprop-config.
Obs-constprop-config->gatesimp
Get the gatesimp field from a obs-constprop-config.
Change-obs-constprop-config
Modifying constructor for obs-constprop-config structures.
Obs-constprop-config-p
Recognizer for obs-constprop-config structures.