		Search-engine friendly clone of the ACL2 documentation.

Bed-from-aig

Bed-from-aig-aux

Signature
(bed-from-aig-aux x order memo) → (mv bed order memo)
Arguments: x — The AIG to transform into a BED.; order — The ordering for bed-order.; memo — Seen table, associates AIGs to BEDs.
Returns: bed — A bed that evaluates in the same way as x.; order — The updated ordering.; memo — The updated seen table.

Definitions and Theorems

Function: bed-from-aig-aux

(defun bed-from-aig-aux (x order memo)
  (declare (xargs :guard t))
  (let ((__function__ 'bed-from-aig-aux))
    (declare (ignorable __function__))
    (b* (((when (aig-atom-p x))
          (cond ((or (eq x t) (eq x nil))
                 (mv x order memo))
                (t (mv (mk-var-raw x t nil) order memo))))
         (look (hons-get x memo))
         ((when look) (mv (cdr look) order memo))
         ((mv okp var a b) (match-aig-var-ite x))
         ((when okp)
          (b* (((mv bed1 order memo)
                (bed-from-aig-aux a order memo))
               ((mv bed2 order memo)
                (bed-from-aig-aux b order memo))
               (ans (mk-var1 var bed1 bed2))
               (memo (hons-acons x ans memo)))
            (mv ans order memo)))
         ((mv okp a b) (match-aig-iff x))
         ((when okp)
          (b* (((mv bed1 order memo)
                (bed-from-aig-aux a order memo))
               ((mv bed2 order memo)
                (bed-from-aig-aux b order memo))
               ((mv ans order)
                (mk-op1 (bed-op-eqv) bed1 bed2 order))
               (memo (hons-acons x ans memo)))
            (mv ans order memo)))
         ((mv okp a b) (match-aig-xor x))
         ((when okp)
          (b* (((mv bed1 order memo)
                (bed-from-aig-aux a order memo))
               ((mv bed2 order memo)
                (bed-from-aig-aux b order memo))
               ((mv ans order)
                (mk-op1 (bed-op-xor) bed1 bed2 order))
               (memo (hons-acons x ans memo)))
            (mv ans order memo)))
         ((mv okp a b) (match-aig-or x))
         ((when okp)
          (b* (((mv bed1 order memo)
                (bed-from-aig-aux a order memo))
               ((when (eq bed1 t))
                (mv t order (hons-acons x t memo)))
               ((mv bed2 order memo)
                (bed-from-aig-aux b order memo))
               ((mv ans order)
                (mk-op1 (bed-op-ior) bed1 bed2 order))
               (memo (hons-acons x ans memo)))
            (mv ans order memo)))
         ((unless (cdr x))
          (b* (((mv arg order memo)
                (bed-from-aig-aux (car x) order memo)))
            (mv (mk-not arg) order memo)))
         ((mv bed1 order memo)
          (bed-from-aig-aux (car x) order memo))
         ((when (not bed1))
          (mv nil order (hons-acons x nil memo)))
         ((mv bed2 order memo)
          (bed-from-aig-aux (cdr x) order memo))
         ((mv ans order)
          (mk-op1 (bed-op-and) bed1 bed2 order)))
      (mv ans order (hons-acons x ans memo)))))