• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
      • Bed-op-p
      • Bed-from-aig
      • Bed-mk1
      • Bed-eval
      • Up
      • Aig-translation
        • Aig-from-bed
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Aig-translation

Aig-from-bed

Translate a BED into an AIG.

Signature

(aig-from-bed bed) → aig

Arguments

bed — The BED to convert.

Returns

aig — A new AIG that is equivalent to the input bed.

This is an especially naive conversion. For efficiency this function is memoized, and you should generally clear its memo table after you use it.

Definitions and Theorems

Function: aig-from-bed

(defun aig-from-bed (bed)
  (declare (xargs :guard t))
  (let ((__function__ 'aig-from-bed))
    (declare (ignorable __function__))
    (b* (((when (atom bed)) (if bed t nil))
         ((cons a b) bed)
         ((unless (integerp b))
          (if (booleanp a)
              (if a (aig-from-bed (car$ b))
                (aig-from-bed (cdr$ b)))
            (aig-ite (make-aig-var a)
                     (aig-from-bed (car$ b))
                     (aig-from-bed (cdr$ b)))))
         (op (bed-op-fix b))
         (left (aig-from-bed (car$ a)))
         (right (aig-from-bed (cdr$ a)))
         ((when (eql op (bed-op-true))) t)
         ((when (eql op (bed-op-false))) nil)
         ((when (eql op (bed-op-ior)))
          (aig-or left right))
         ((when (eql op (bed-op-orc2)))
          (aig-or left (aig-not right)))
         ((when (eql op (bed-op-arg1))) left)
         ((when (eql op (bed-op-orc1)))
          (aig-or (aig-not left) right))
         ((when (eql op (bed-op-arg2))) right)
         ((when (eql op (bed-op-eqv)))
          (aig-iff left right))
         ((when (eql op (bed-op-and)))
          (aig-and left right))
         ((when (eql op (bed-op-nand)))
          (aig-not (aig-and left right)))
         ((when (eql op (bed-op-xor)))
          (aig-xor left right))
         ((when (eql op (bed-op-not2)))
          (aig-not right))
         ((when (eql op (bed-op-andc2)))
          (aig-and left (aig-not right)))
         ((when (eql op (bed-op-not1)))
          (aig-not left))
         ((when (eql op (bed-op-andc1)))
          (aig-and (aig-not left) right))
         ((when (eql op (bed-op-nor)))
          (aig-not (aig-or left right))))
      :impossible)))

Function: aig-from-bed-memoize-condition

(defun aig-from-bed-memoize-condition (bed)
  (declare (ignorable bed)
           (xargs :guard 't))
  (consp bed))

Theorem: aig-eval-of-aig-from-bed

(defthm aig-eval-of-aig-from-bed
  (equal (aig-eval (aig-from-bed bed) env)
         (eql 1
              (bed-eval bed (aig-env-to-bed-env env)))))