		Search-engine friendly clone of the ACL2 documentation.

Parametrize

Ubdd-to-aignet

Signature
(ubdd-to-aignet x level memo litarr gatesimp strash aignet) → (mv val new-memo new-strash new-aignet)
Arguments: x — Guard (acl2::ubddp x).; level — Guard (natp level).; memo — Guard (ubdd-to-aignet-memo-p memo).; gatesimp — Guard (gatesimp-p gatesimp).
Returns: val — Type (litp val).; new-memo — Type (ubdd-to-aignet-memo-p new-memo).

Definitions and Theorems

Function: ubdd-to-aignet

(defun ubdd-to-aignet (x level
                         memo litarr gatesimp strash aignet)
 (declare (xargs :stobjs (litarr strash aignet)))
 (declare (xargs :guard (and (acl2::ubddp x)
                             (natp level)
                             (ubdd-to-aignet-memo-p memo)
                             (gatesimp-p gatesimp))))
 (declare (xargs :guard (and (aignet-lit-listp (alist-vals memo)
                                               aignet)
                             (aignet-copies-in-bounds litarr aignet)
                             (<= (+ level (acl2::max-depth x))
                                 (lits-length litarr)))))
 (let ((__function__ 'ubdd-to-aignet))
   (declare (ignorable __function__))
   (b* ((memo (ubdd-to-aignet-memo-fix memo))
        (aignet (mbe :logic (non-exec (node-list-fix aignet))
                     :exec aignet))
        (x (lubdd-fix x))
        ((when (atom x))
         (mv (bool->bit x) memo strash aignet))
        (key (make-ubdd/level :ubdd x :level level))
        (look (hons-get key memo))
        ((when look)
         (mv (cdr look) memo strash aignet))
        ((mv then memo strash aignet)
         (ubdd-to-aignet (car x)
                         (1+ (lnfix level))
                         memo litarr gatesimp strash aignet))
        ((mv else memo strash aignet)
         (ubdd-to-aignet (cdr x)
                         (1+ (lnfix level))
                         memo litarr gatesimp strash aignet))
        (test (get-lit level litarr))
        ((mv ite strash aignet)
         (aignet-hash-mux test then else gatesimp strash aignet))
        (memo (hons-acons key ite memo)))
     (mv ite memo strash aignet))))

Theorem: litp-of-ubdd-to-aignet.val

(defthm litp-of-ubdd-to-aignet.val
  (b* (((mv ?val ?new-memo ?new-strash ?new-aignet)
        (ubdd-to-aignet x level
                        memo litarr gatesimp strash aignet)))
    (litp val))
  :rule-classes :rewrite)

Theorem: ubdd-to-aignet-memo-p-of-ubdd-to-aignet.new-memo

(defthm ubdd-to-aignet-memo-p-of-ubdd-to-aignet.new-memo
  (b* (((mv ?val ?new-memo ?new-strash ?new-aignet)
        (ubdd-to-aignet x level
                        memo litarr gatesimp strash aignet)))
    (ubdd-to-aignet-memo-p new-memo))
  :rule-classes :rewrite)

Theorem: aignet-extension-p-of-ubdd-to-aignet

(defthm aignet-extension-p-of-ubdd-to-aignet
  (b* (((mv ?val ?new-memo ?new-strash ?new-aignet)
        (ubdd-to-aignet x level
                        memo litarr gatesimp strash aignet)))
    (aignet-extension-p new-aignet aignet)))

Theorem: num-ins-of-ubdd-to-aignet

(defthm num-ins-of-ubdd-to-aignet
  (b* (((mv ?val ?new-memo ?new-strash ?new-aignet)
        (ubdd-to-aignet x level
                        memo litarr gatesimp strash aignet)))
    (equal (stype-count :pi new-aignet)
           (stype-count :pi aignet))))

Theorem: num-regs-of-ubdd-to-aignet

(defthm num-regs-of-ubdd-to-aignet
  (b* (((mv ?val ?new-memo ?new-strash ?new-aignet)
        (ubdd-to-aignet x level
                        memo litarr gatesimp strash aignet)))
    (equal (stype-count :reg new-aignet)
           (stype-count :reg aignet))))

Theorem: num-outs-of-ubdd-to-aignet

(defthm num-outs-of-ubdd-to-aignet
  (b* (((mv ?val ?new-memo ?new-strash ?new-aignet)
        (ubdd-to-aignet x level
                        memo litarr gatesimp strash aignet)))
    (equal (stype-count :po new-aignet)
           (stype-count :po aignet))))

Theorem: result-lits-of-ubdd-to-aignet

(defthm result-lits-of-ubdd-to-aignet
 (b* (((mv ?val ?new-memo ?new-strash ?new-aignet)
       (ubdd-to-aignet x level
                       memo litarr gatesimp strash aignet)))
  (implies
   (and
       (aignet-lit-listp (alist-vals (ubdd-to-aignet-memo-fix memo))
                         aignet)
       (aignet-copies-in-bounds litarr aignet))
   (and (aignet-litp val new-aignet)
        (aignet-lit-listp (alist-vals new-memo)
                          new-aignet)))))

Theorem: ubdd-to-aignet-preserves-ubdd-to-aignet-memo-ok

(defthm ubdd-to-aignet-preserves-ubdd-to-aignet-memo-ok
 (b* (((mv ?val ?new-memo ?new-strash ?new-aignet)
       (ubdd-to-aignet x level
                       memo litarr gatesimp strash aignet)))
  (b*
   ((values
        (bits->bools (lit-eval-list litarr invals regvals aignet))))
   (implies
    (and
       (ubdd-to-aignet-memo-ok memo litarr aignet invals regvals)
       (aignet-copies-in-bounds litarr aignet)
       (aignet-lit-listp (alist-vals (ubdd-to-aignet-memo-fix memo))
                         aignet))
    (and
     (ubdd-to-aignet-memo-ok new-memo
                             litarr new-aignet invals regvals)
     (equal
          (lit-eval val invals regvals new-aignet)
          (bool->bit (acl2::eval-bdd x (nthcdr level values)))))))))

Theorem: ubdd-to-aignet-of-ubdd-fix-x

(defthm ubdd-to-aignet-of-ubdd-fix-x
  (equal (ubdd-to-aignet (acl2::ubdd-fix x)
                         level
                         memo litarr gatesimp strash aignet)
         (ubdd-to-aignet x level
                         memo litarr gatesimp strash aignet)))

Theorem: ubdd-to-aignet-ubdd-equiv-congruence-on-x

(defthm ubdd-to-aignet-ubdd-equiv-congruence-on-x
  (implies
       (acl2::ubdd-equiv x x-equiv)
       (equal (ubdd-to-aignet x level
                              memo litarr gatesimp strash aignet)
              (ubdd-to-aignet x-equiv level
                              memo litarr gatesimp strash aignet)))
  :rule-classes :congruence)

Theorem: ubdd-to-aignet-of-nfix-level

(defthm ubdd-to-aignet-of-nfix-level
  (equal (ubdd-to-aignet x (nfix level)
                         memo litarr gatesimp strash aignet)
         (ubdd-to-aignet x level
                         memo litarr gatesimp strash aignet)))

Theorem: ubdd-to-aignet-nat-equiv-congruence-on-level

(defthm ubdd-to-aignet-nat-equiv-congruence-on-level
  (implies
       (nat-equiv level level-equiv)
       (equal (ubdd-to-aignet x level
                              memo litarr gatesimp strash aignet)
              (ubdd-to-aignet x level-equiv
                              memo litarr gatesimp strash aignet)))
  :rule-classes :congruence)

Theorem: ubdd-to-aignet-of-ubdd-to-aignet-memo-fix-memo

(defthm ubdd-to-aignet-of-ubdd-to-aignet-memo-fix-memo
  (equal (ubdd-to-aignet x level (ubdd-to-aignet-memo-fix memo)
                         litarr gatesimp strash aignet)
         (ubdd-to-aignet x level
                         memo litarr gatesimp strash aignet)))

Theorem: ubdd-to-aignet-ubdd-to-aignet-memo-equiv-congruence-on-memo

(defthm ubdd-to-aignet-ubdd-to-aignet-memo-equiv-congruence-on-memo
 (implies (ubdd-to-aignet-memo-equiv memo memo-equiv)
          (equal (ubdd-to-aignet x level
                                 memo litarr gatesimp strash aignet)
                 (ubdd-to-aignet x level memo-equiv
                                 litarr gatesimp strash aignet)))
 :rule-classes :congruence)

Theorem: ubdd-to-aignet-of-gatesimp-fix-gatesimp

(defthm ubdd-to-aignet-of-gatesimp-fix-gatesimp
  (equal (ubdd-to-aignet x level
                         memo litarr (gatesimp-fix gatesimp)
                         strash aignet)
         (ubdd-to-aignet x level
                         memo litarr gatesimp strash aignet)))

Theorem: ubdd-to-aignet-gatesimp-equiv-congruence-on-gatesimp

(defthm ubdd-to-aignet-gatesimp-equiv-congruence-on-gatesimp
  (implies
       (gatesimp-equiv gatesimp gatesimp-equiv)
       (equal (ubdd-to-aignet x level
                              memo litarr gatesimp strash aignet)
              (ubdd-to-aignet x level memo
                              litarr gatesimp-equiv strash aignet)))
  :rule-classes :congruence)

Theorem: ubdd-to-aignet-of-node-list-fix-aignet

(defthm ubdd-to-aignet-of-node-list-fix-aignet
  (equal (ubdd-to-aignet x level memo litarr
                         gatesimp strash (node-list-fix aignet))
         (ubdd-to-aignet x level
                         memo litarr gatesimp strash aignet)))

Theorem: ubdd-to-aignet-node-list-equiv-congruence-on-aignet

(defthm ubdd-to-aignet-node-list-equiv-congruence-on-aignet
  (implies
       (node-list-equiv aignet aignet-equiv)
       (equal (ubdd-to-aignet x level
                              memo litarr gatesimp strash aignet)
              (ubdd-to-aignet x level memo
                              litarr gatesimp strash aignet-equiv)))
  :rule-classes :congruence)