• 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
              • 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
  • Aignet-comb-transforms

Comb-transform

Configuration object for any combinational transform supported by apply-comb-transforms.

This is a ``transparent'' sum type introduced using fty::deftranssum. It is simply any one of the following types:

  • balance-config
  • fraig-config
  • rewrite-config
  • abc-comb-simp-config
  • obs-constprop-config
  • observability-config
  • constprop-config
  • snapshot-config
  • prune-config
  • unreachability-config
  • dom-supergates-sweep-config

Subtopics

Fraig-config
Configuration object for the fraig aignet transform.
Comb-transform-p
Recognizer for comb-transform.
Comb-transform-fix
(comb-transform-fix x) is a ACL2::fty fixing function.
Rewrite-config
Configuration object for the rewrite aignet transform.
Obs-constprop-config
Configuration object for the obs-constprop aignet transform.
Observability-config
Configuration object for the observability-fix aignet transform.
Constprop-config
Configuration object for the constprop aignet transform.
Abc-comb-simp-config
Configuration object for using the abc-comb-simplify transform on an aignet.
M-assum-n-output-observability-config
Configuration object for the m-assum-n-output-observability aignet transform.
Comb-transform-equiv
Basic equivalence relation for comb-transform structures.
Snapshot-config
Aignet transform that returns the same network and simply writes a snapshot into an aiger file for debugging.
Prune-config
Aignet transform that prunes out unused logic in the network.