• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
      • Ipasir
      • Aignet
        • Base-api
        • Aignet-construction
        • Representation
        • Aignet-copy-init
        • Aignet-simplify-marked-with-tracking
        • Aignet-cnf
        • Aignet-simplify-with-tracking
        • Aignet-complete-copy
        • Aignet-eval
        • Semantics
        • Aignet-transforms
          • Aignet-comb-transforms
          • Aignet-m-assumption-n-output-transforms
            • M-assumption-n-output-comb-transform
              • M-assumption-n-output-comb-transform-fix
              • M-assumption-n-output-comb-transform-p
              • M-assumption-n-output-comb-transform-equiv
            • Apply-m-assumption-n-output-transform
          • Aignet-n-output-comb-transforms
        • Aignet-simplify-marked
        • 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
    • Testing-utilities
    • Math
  • Aignet-m-assumption-n-output-transforms

M-assumption-n-output-comb-transform

Configuration object for any combinational transform supported by apply-m-assumption-n-output-output-transform-default.

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

  • comb-transform
  • n-outputs-unreachability-config
  • n-outputs-dom-supergates-sweep-config
  • m-assum-n-output-observability-config

Subtopics

M-assumption-n-output-comb-transform-fix
(m-assumption-n-output-comb-transform-fix x) is a ACL2::fty fixing function.
M-assumption-n-output-comb-transform-p
Recognizer for m-assumption-n-output-comb-transform.
M-assumption-n-output-comb-transform-equiv
Basic equivalence relation for m-assumption-n-output-comb-transform structures.