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

Aignet-m-assumption-n-output-transforms

Aignet transforms that simplify the network while preserving combinational equivalence of the first M primary outputs and combinational equivalence when assuming the first M primary outputs true on the next N primary outputs.

Subtopics

M-assumption-n-output-comb-transform
Configuration object for any combinational transform supported by apply-m-assumption-n-output-output-transform-default.
Apply-m-assumption-n-output-transform
Stub for an AIG transform that preserves combinational equivalence of the first M primary outputs, then preserves combinational equivalence of the next N primary outputs under the assumption of the first N