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

    Aig-nand

    (aig-nand x y) constructs an AIG representing (not (and x y)).

    Macro: aig-nand

    (defmacro aig-nand (x y)
      (cons 'aig-not
            (cons (cons 'aig-and (cons x (cons y 'nil)))
                  'nil)))