• Top
    • Documentation
    • Books
    • Boolean-reasoning
      • Ipasir
      • Aignet
      • Aig
        • Aig-constructors
        • Aig-vars
        • Aig-sat
        • Bddify
        • Aig-substitution
        • Aig-other
          • Best-aig
          • Aig2c
          • Expr-to-aig
          • Aiger-write
          • Aig-random-sim
          • Aiger-read
          • Aig-print
          • Aig-cases
        • Aig-semantics
        • Aig-and-count
      • Satlink
      • Truth
      • Ubdds
      • Bdd
      • Faig
      • Bed
      • 4v
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Aig

Aig-other

Various hard-to-categorize algorithms for working with AIGs.

Subtopics

Best-aig
Algorithms for choosing "better" (smaller) AIGs.
Aig2c
Naive compiler from Hons AIGs into C/C++ code fragments.
Expr-to-aig
Convert an ACL2-like S-expression into an AIG.
Aiger-write
Write out a collection of AIGs into an AIGER file, directly, without going through aignet.
Aig-random-sim
Functions for randomly vector simulations of Hons aigs.
Aiger-read
Read an AIGER file into a collection of AIGs.
Aig-print
Convert an AIG into an ACL2-like S-expression.
Aig-cases
Control-flow macro to split into cases on what kind of AIG you have encountered.