(aignet-parametrize-copy-init litarr in-ubdds reg-ubdds aignet copy strash gatesimp aignet2) → (mv new-copy new-strash new-aignet2)
Function:
(defun aignet-parametrize-copy-init (litarr in-ubdds reg-ubdds aignet copy strash gatesimp aignet2) (declare (xargs :stobjs (litarr in-ubdds reg-ubdds aignet copy strash aignet2))) (declare (xargs :guard (gatesimp-p gatesimp))) (declare (xargs :guard (and (aignet-copies-in-bounds litarr aignet2) (<= (num-regs aignet) (ubdds-length reg-ubdds)) (<= (num-ins aignet) (ubdds-length in-ubdds)) (<= (ec-call (ubdd-arr-max-depth in-ubdds)) (lits-length litarr)) (<= (ec-call (ubdd-arr-max-depth reg-ubdds)) (lits-length litarr)) (non-exec (equal copy (create-litarr)))))) (let ((__function__ 'aignet-parametrize-copy-init)) (declare (ignorable __function__)) (b* ((memo nil) (copy (mbe :logic (non-exec (create-litarr)) :exec copy)) (copy (resize-lits (num-fanins aignet) copy)) ((mv memo copy strash aignet2) (aignet-parametrize-copy-set-ins 0 litarr in-ubdds aignet memo copy strash gatesimp aignet2)) ((mv memo copy strash aignet2) (aignet-parametrize-copy-set-regs 0 litarr reg-ubdds aignet memo copy strash gatesimp aignet2)) (- (fast-alist-free memo))) (mv copy strash aignet2))))
Theorem:
(defthm aignet-extension-p-of-aignet-parametrize-copy-init (b* (((mv ?new-copy ?new-strash ?new-aignet2) (aignet-parametrize-copy-init litarr in-ubdds reg-ubdds aignet copy strash gatesimp aignet2))) (aignet-extension-p new-aignet2 aignet2)))
Theorem:
(defthm num-ins-of-aignet-parametrize-copy-init (b* (((mv ?new-copy ?new-strash ?new-aignet2) (aignet-parametrize-copy-init litarr in-ubdds reg-ubdds aignet copy strash gatesimp aignet2))) (equal (stype-count :pi new-aignet2) (stype-count :pi aignet2))))
Theorem:
(defthm num-regs-of-aignet-parametrize-copy-init (b* (((mv ?new-copy ?new-strash ?new-aignet2) (aignet-parametrize-copy-init litarr in-ubdds reg-ubdds aignet copy strash gatesimp aignet2))) (equal (stype-count :reg new-aignet2) (stype-count :reg aignet2))))
Theorem:
(defthm num-outs-of-aignet-parametrize-copy-init (b* (((mv ?new-copy ?new-strash ?new-aignet2) (aignet-parametrize-copy-init litarr in-ubdds reg-ubdds aignet copy strash gatesimp aignet2))) (equal (stype-count :po new-aignet2) (stype-count :po aignet2))))
Theorem:
(defthm copy-len-of-aignet-parametrize-copy-init (b* (((mv ?new-copy ?new-strash ?new-aignet2) (aignet-parametrize-copy-init litarr in-ubdds reg-ubdds aignet copy strash gatesimp aignet2))) (equal (len new-copy) (num-fanins aignet))))
Theorem:
(defthm result-lits-of-aignet-parametrize-copy-init (b* (((mv ?new-copy ?new-strash ?new-aignet2) (aignet-parametrize-copy-init litarr in-ubdds reg-ubdds aignet copy strash gatesimp aignet2))) (implies (aignet-copies-in-bounds litarr aignet2) (aignet-copies-in-bounds new-copy new-aignet2))))
Theorem:
(defthm eval-nth-lit-of-aignet-parametrize-copy-init (b* (((mv ?new-copy ?new-strash ?new-aignet2) (aignet-parametrize-copy-init litarr in-ubdds reg-ubdds aignet copy strash gatesimp aignet2))) (b* ((suff (lookup-id id aignet)) (node (car suff)) (rest (cdr suff)) (stype (stype node)) (regnum (stype-count :reg rest)) (innum (stype-count :pi rest))) (implies (aignet-copies-in-bounds litarr aignet2) (and (implies (equal stype :reg) (equal (lit-eval (nth-lit id new-copy) invals regvals new-aignet2) (bool->bit (acl2::eval-bdd (nth regnum reg-ubdds) (bits->bools (lit-eval-list litarr invals regvals aignet2)))))) (implies (equal stype :pi) (equal (lit-eval (nth-lit id new-copy) invals regvals new-aignet2) (bool->bit (acl2::eval-bdd (nth innum in-ubdds) (bits->bools (lit-eval-list litarr invals regvals aignet2)))))))))))
Theorem:
(defthm input-copy-values-of-aignet-parametrize-copy-init (b* (((mv ?new-copy ?new-strash ?new-aignet2) (aignet-parametrize-copy-init litarr in-ubdds reg-ubdds aignet copy strash gatesimp aignet2))) (implies (aignet-copies-in-bounds litarr aignet2) (bits-equiv (input-copy-values 0 invals regvals aignet new-copy new-aignet2) (take (stype-count :pi aignet) (eval-ubddarr in-ubdds (bits->bools (lit-eval-list litarr invals regvals aignet2))))))))
Theorem:
(defthm reg-copy-values-of-aignet-parametrize-copy-init (b* (((mv ?new-copy ?new-strash ?new-aignet2) (aignet-parametrize-copy-init litarr in-ubdds reg-ubdds aignet copy strash gatesimp aignet2))) (implies (aignet-copies-in-bounds litarr aignet2) (bits-equiv (reg-copy-values 0 invals regvals aignet new-copy new-aignet2) (take (stype-count :reg aignet) (eval-ubddarr reg-ubdds (bits->bools (lit-eval-list litarr invals regvals aignet2))))))))
Theorem:
(defthm aignet-parametrize-copy-init-of-node-list-fix-aignet (equal (aignet-parametrize-copy-init litarr in-ubdds reg-ubdds (node-list-fix aignet) copy strash gatesimp aignet2) (aignet-parametrize-copy-init litarr in-ubdds reg-ubdds aignet copy strash gatesimp aignet2)))
Theorem:
(defthm aignet-parametrize-copy-init-node-list-equiv-congruence-on-aignet (implies (node-list-equiv aignet aignet-equiv) (equal (aignet-parametrize-copy-init litarr in-ubdds reg-ubdds aignet copy strash gatesimp aignet2) (aignet-parametrize-copy-init litarr in-ubdds reg-ubdds aignet-equiv copy strash gatesimp aignet2))) :rule-classes :congruence)
Theorem:
(defthm aignet-parametrize-copy-init-of-gatesimp-fix-gatesimp (equal (aignet-parametrize-copy-init litarr in-ubdds reg-ubdds aignet copy strash (gatesimp-fix gatesimp) aignet2) (aignet-parametrize-copy-init litarr in-ubdds reg-ubdds aignet copy strash gatesimp aignet2)))
Theorem:
(defthm aignet-parametrize-copy-init-gatesimp-equiv-congruence-on-gatesimp (implies (gatesimp-equiv gatesimp gatesimp-equiv) (equal (aignet-parametrize-copy-init litarr in-ubdds reg-ubdds aignet copy strash gatesimp aignet2) (aignet-parametrize-copy-init litarr in-ubdds reg-ubdds aignet copy strash gatesimp-equiv aignet2))) :rule-classes :congruence)
Theorem:
(defthm aignet-parametrize-copy-init-of-node-list-fix-aignet2 (equal (aignet-parametrize-copy-init litarr in-ubdds reg-ubdds aignet copy strash gatesimp (node-list-fix aignet2)) (aignet-parametrize-copy-init litarr in-ubdds reg-ubdds aignet copy strash gatesimp aignet2)))
Theorem:
(defthm aignet-parametrize-copy-init-node-list-equiv-congruence-on-aignet2 (implies (node-list-equiv aignet2 aignet2-equiv) (equal (aignet-parametrize-copy-init litarr in-ubdds reg-ubdds aignet copy strash gatesimp aignet2) (aignet-parametrize-copy-init litarr in-ubdds reg-ubdds aignet copy strash gatesimp aignet2-equiv))) :rule-classes :congruence)