• Top
    • Documentation
    • Books
    • Boolean-reasoning
      • Ipasir
      • Aignet
      • Aig
        • Aig-constructors
          • Aig-and
          • Aig-or-list
          • Aig-and-list
          • Aig-or
          • Aig-not
          • Aig-implies
          • Aig-implies-lists
          • Aig-xor-lists
          • Aig-xor
          • Aig-orc2-lists
          • Aig-or-lists
          • Aig-nor-lists
          • Aig-nand-lists
          • Aig-iff-lists
          • Aig-iff
          • Aig-andc2-lists
          • Aig-andc1-lists
          • Aig-and-lists
          • Aig-not-list
          • Aig-ite
          • Aig-orc1-lists
          • Aig-orc1
          • Aig-nand
          • Aig-orc2
          • Aig-nor
          • Aig-andc2
          • Aig-andc1
        • Aig-vars
        • Aig-sat
        • Bddify
        • Aig-substitution
        • Aig-other
        • 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-constructors

Low-level functions for constructing AIGs.

Note that you can enable/disable these together using the ruleset aig-constructors.

Subtopics

Aig-and
(aig-and x1 x2 ...) constructs an AIG representing (and x1 x2 ...).
Aig-or-list
(aig-or-list x) ors together all of the AIGs in the list x.
Aig-and-list
(aig-and-list x) ands together all of the AIGs in the list x.
Aig-or
(aig-or x1 x2 ...) constructs an AIG representing (or x1 x2 ...).
Aig-not
(aig-not x) constructs an AIG representing (not x).
Aig-implies
(aig-implies x y) constructs an AIG representing (implies x y).
Aig-implies-lists
(aig-implies-lists x y) pairwise implies together the AIGs from the lists x and y.
Aig-xor-lists
(aig-xor-lists x y) pairwise xors together the AIGs from the lists x and y.
Aig-xor
(aig-xor x y) constructs an AIG representing (xor x y).
Aig-orc2-lists
(aig-orc2-lists x y) pairwise orc2s together the AIGs from the lists x or y.
Aig-or-lists
(aig-or-lists x y) pairwise ors together the AIGs from the lists x and y.
Aig-nor-lists
(aig-nor-lists x y) pairwise nors together the AIGs from the lists x and y.
Aig-nand-lists
(aig-nand-lists x y) pairwise nands together the AIGs from the lists x and y.
Aig-iff-lists
(aig-iff-lists x y) pairwise iffs together the AIGs from the lists x and y.
Aig-iff
(aig-iff x y) constructs an AIG representing (iff x y).
Aig-andc2-lists
(aig-andc2-lists x y) pairwise andc2s together the AIGs from the lists x and y.
Aig-andc1-lists
(aig-andc1-lists x y) pairwise andc1s together the AIGs from the lists x and y.
Aig-and-lists
(aig-and-lists x y) pairwise ands together the AIGs from the lists x and y.
Aig-not-list
(aig-not-list x) negates every AIG in the list x.
Aig-ite
(aig-ite a b c) constructs an AIG representing (if a b c).
Aig-orc1-lists
(aig-orc1-lists x y) is identical to aig-implies-lists.
Aig-orc1
(aig-orc1 x y) is identical to aig-implies.
Aig-nand
(aig-nand x y) constructs an AIG representing (not (and x y)).
Aig-orc2
(aig-orc2 x y) constructs an AIG representing (or x (not y)).
Aig-nor
(aig-nor x y) constructs an AIG representing (not (or x y)).
Aig-andc2
(aig-andc2 x y) constructs an AIG representing (and x (not y)).
Aig-andc1
(aig-andc1 x y) constructs an AIG representing (and (not x) y).