• 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
            • Rewrite
            • Comb-transform
              • Fraig-config
              • Comb-transform-p
              • Comb-transform-fix
              • Rewrite-config
              • Obs-constprop-config
              • Observability-config
                • Observability-config-fix
                • Observability-config-equiv
                • Make-observability-config
                • Observability-config-p
                • Observability-config->hyp-max-size
                • Observability-config->concl-min-size
                • Observability-config->min-ratio
                • Observability-config->gatesimp
                • Change-observability-config
              • Constprop-config
              • Abc-comb-simp-config
              • M-assum-n-output-observability-config
              • Comb-transform-equiv
              • Snapshot-config
              • Prune-config
            • 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
  • Observability-fix
  • Comb-transform

Observability-config

Configuration object for the observability-fix aignet transform.

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

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

Subtopics

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