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

    Aig-cases

    Control-flow macro to split into cases on what kind of AIG you have encountered.

    Macro: aig-cases

    (defmacro aig-cases (x &key true false var inv and)
     (cons
      'let
      (cons
       (cons (cons 'aig-cases-var (cons x 'nil))
             'nil)
       (cons
        (cons
         'cond
         (cons
          (cons
           '(aig-atom-p aig-cases-var)
           (cons
              (cons 'cond
                    (cons (cons '(eq aig-cases-var t)
                                (cons true 'nil))
                          (cons (cons '(eq aig-cases-var nil)
                                      (cons false 'nil))
                                (cons (cons 't (cons var 'nil)) 'nil))))
              'nil))
          (cons (cons '(eq (cdr aig-cases-var) nil)
                      (cons inv 'nil))
                (cons (cons 't (cons and 'nil)) 'nil))))
        'nil))))