(ubdd-to-aignet x level memo litarr gatesimp strash aignet) → (mv val new-memo new-strash new-aignet)
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)