• 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-ite-fn
          • 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-constructors

Aig-ite

(aig-ite a b c) constructs an AIG representing (if a b c).

This is logically just aig-ite-fn, but we try to lazily avoid computing b or c when the value of a is known.

Subtopics

Aig-ite-fn