• Top
    • Documentation
    • Books
    • Boolean-reasoning
      • Ipasir
      • Aignet
      • Aig
        • Aig-constructors
          • Aig-and
          • Aig-or-list
          • Aig-and-list
          • Aig-or
            • Aig-binary-or
            • Aig-or-macro-exec-part
            • Aig-or-macro-logic-part
          • 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-constructors

Aig-or

(aig-or x1 x2 ...) constructs an AIG representing (or x1 x2 ...).

Like aig-and, we attempt to lazily avoid computing later terms in the expression.

Macro: aig-or

(defmacro aig-or (&rest args)
  (cons 'mbe
        (cons ':logic
              (cons (aig-or-macro-logic-part args)
                    (cons ':exec
                          (cons (aig-or-macro-exec-part args)
                                'nil))))))

Subtopics

Aig-binary-or
(aig-binary-or x y) constructs an AIG representing (or x y).
Aig-or-macro-exec-part
Aig-or-macro-logic-part