		Search-engine friendly clone of the ACL2 documentation.

Bed-from-aig

Translate an AIG into a BED.

Signature
(bed-from-aig x) → (mv bed order)
Arguments: x — An AIG to transform into a BED.
Returns: bed — A bed that evaluates in the same way as x.; order — An ordering on the nodes of bed for bed-order.

Definitions and Theorems

Function: bed-from-aig

(defun bed-from-aig (x)
  (declare (xargs :guard t))
  (let ((__function__ 'bed-from-aig))
    (declare (ignorable __function__))
    (b* ((memo 10000)
         (order :bed-order)
         ((mv bed order memo)
          (bed-from-aig-aux x order memo)))
      (fast-alist-free memo)
      (mv bed order))))

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

(defthm bed-eval-of-bed-from-aig
  (b* (((mv bed ?order) (bed-from-aig aig)))
    (equal (bed-eval bed env)
           (bool->bit (aig-eval aig env)))))

Subtopics

Match-aig-var-ite
Match-aig-var-ite-aux: We have been given the AIG (OR (AND A1 A2) (OR B1 B2)). We want to pattern match it against (IF VAR A B)?
Match-aig-xor-1
Match-aig-iff-2
Match-aig-xor-2
Match-aig-iff-1
Bed-from-aig-aux
Match-aig-nor
Match-aig-andc2
Match-aig-andc1
Match-aig-xor
Match-aig-or
Match-aig-iff
Match-aig-and
Match-aig-not