(aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash gatesimp aignet2) → (mv new-memo new-copy new-strash new-aignet2)
Function:
(defun aignet-parametrize-copy-set-ins (n litarr in-ubdds aignet memo copy strash gatesimp aignet2) (declare (xargs :stobjs (litarr in-ubdds aignet copy strash aignet2))) (declare (xargs :guard (and (natp n) (ubdd-to-aignet-memo-p memo) (gatesimp-p gatesimp)))) (declare (xargs :guard (and (<= n (num-ins aignet)) (aignet-lit-listp (alist-vals memo) aignet2) (<= (num-fanins aignet) (lits-length copy)) (aignet-copies-in-bounds litarr aignet2) (<= (num-ins aignet) (ubdds-length in-ubdds)) (<= (ec-call (ubdd-arr-max-depth in-ubdds)) (lits-length litarr))))) (let ((__function__ 'aignet-parametrize-copy-set-ins)) (declare (ignorable __function__)) (b* (((when (mbe :logic (zp (- (num-ins aignet) (nfix n))) :exec (eql (num-ins aignet) n))) (b* ((aignet2 (mbe :logic (non-exec (node-list-fix aignet2)) :exec aignet2))) (mv (ubdd-to-aignet-memo-fix memo) copy strash aignet2))) (ubdd (get-ubdd n in-ubdds)) ((mv ubdd-lit memo strash aignet2) (ubdd-to-aignet ubdd 0 memo litarr gatesimp strash aignet2)) (id (innum->id n aignet)) (copy (set-lit id ubdd-lit copy))) (aignet-parametrize-copy-set-ins (1+ (lnfix n)) litarr in-ubdds aignet memo copy strash gatesimp aignet2))))
Theorem:
(defthm ubdd-to-aignet-memo-p-of-aignet-parametrize-copy-set-ins.new-memo (b* (((mv ?new-memo ?new-copy ?new-strash ?new-aignet2) (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash gatesimp aignet2))) (ubdd-to-aignet-memo-p new-memo)) :rule-classes :rewrite)
Theorem:
(defthm aignet-extension-p-of-aignet-parametrize-copy-set-ins (b* (((mv ?new-memo ?new-copy ?new-strash ?new-aignet2) (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash gatesimp aignet2))) (aignet-extension-p new-aignet2 aignet2)))
Theorem:
(defthm num-ins-of-aignet-parametrize-copy-set-ins (b* (((mv ?new-memo ?new-copy ?new-strash ?new-aignet2) (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash gatesimp aignet2))) (equal (stype-count :pi new-aignet2) (stype-count :pi aignet2))))
Theorem:
(defthm num-regs-of-aignet-parametrize-copy-set-ins (b* (((mv ?new-memo ?new-copy ?new-strash ?new-aignet2) (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash gatesimp aignet2))) (equal (stype-count :reg new-aignet2) (stype-count :reg aignet2))))
Theorem:
(defthm num-outs-of-aignet-parametrize-copy-set-ins (b* (((mv ?new-memo ?new-copy ?new-strash ?new-aignet2) (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash gatesimp aignet2))) (equal (stype-count :po new-aignet2) (stype-count :po aignet2))))
Theorem:
(defthm copy-len-of-aignet-parametrize-copy-set-ins (b* (((mv ?new-memo ?new-copy ?new-strash ?new-aignet2) (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash gatesimp aignet2))) (implies (<= (num-fanins aignet) (len copy)) (equal (len new-copy) (len copy)))))
Theorem:
(defthm result-lits-of-aignet-parametrize-copy-set-ins (b* (((mv ?new-memo ?new-copy ?new-strash ?new-aignet2) (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash gatesimp aignet2))) (implies (and (aignet-lit-listp (alist-vals (ubdd-to-aignet-memo-fix memo)) aignet2) (aignet-copies-in-bounds litarr aignet2)) (and (implies (aignet-copies-in-bounds copy aignet2) (aignet-copies-in-bounds new-copy new-aignet2)) (aignet-lit-listp (alist-vals new-memo) new-aignet2)))))
Theorem:
(defthm aignet-parametrize-copy-set-ins-preserves-ubdd-to-aignet-memo-ok (b* (((mv ?new-memo ?new-copy ?new-strash ?new-aignet2) (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash gatesimp aignet2))) (implies (and (ubdd-to-aignet-memo-ok memo litarr aignet2 invals regvals) (aignet-copies-in-bounds litarr aignet2) (aignet-lit-listp (alist-vals (ubdd-to-aignet-memo-fix memo)) aignet2)) (ubdd-to-aignet-memo-ok new-memo litarr new-aignet2 invals regvals))))
Theorem:
(defthm nth-lit-preserved-of-aignet-parametrize-copy-set-ins (b* (((mv ?new-memo ?new-copy ?new-strash ?new-aignet2) (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash gatesimp aignet2))) (b* ((suff (lookup-id id aignet)) (node (car suff)) (rest (cdr suff)) (stype (stype node)) (innum (stype-count :pi rest))) (implies (not (and (eq stype :pi) (<= (nfix n) innum))) (equal (nth-lit id new-copy) (nth-lit id copy))))))
Theorem:
(defthm eval-nth-lit-of-aignet-parametrize-copy-set-ins (b* (((mv ?new-memo ?new-copy ?new-strash ?new-aignet2) (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash gatesimp aignet2))) (b* ((suff (lookup-id id aignet)) (node (car suff)) (rest (cdr suff)) (stype (stype node)) (innum (stype-count :pi rest))) (implies (and (eq stype :pi) (<= (nfix n) innum) (ubdd-to-aignet-memo-ok memo litarr aignet2 invals regvals) (aignet-copies-in-bounds litarr aignet2) (aignet-lit-listp (alist-vals (ubdd-to-aignet-memo-fix memo)) aignet2)) (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 aignet-parametrize-copy-set-ins-of-nfix-n (equal (aignet-parametrize-copy-set-ins (nfix n) litarr in-ubdds aignet memo copy strash gatesimp aignet2) (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash gatesimp aignet2)))
Theorem:
(defthm aignet-parametrize-copy-set-ins-nat-equiv-congruence-on-n (implies (nat-equiv n n-equiv) (equal (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash gatesimp aignet2) (aignet-parametrize-copy-set-ins n-equiv litarr in-ubdds aignet memo copy strash gatesimp aignet2))) :rule-classes :congruence)
Theorem:
(defthm aignet-parametrize-copy-set-ins-of-node-list-fix-aignet (equal (aignet-parametrize-copy-set-ins n litarr in-ubdds (node-list-fix aignet) memo copy strash gatesimp aignet2) (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash gatesimp aignet2)))
Theorem:
(defthm aignet-parametrize-copy-set-ins-node-list-equiv-congruence-on-aignet (implies (node-list-equiv aignet aignet-equiv) (equal (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash gatesimp aignet2) (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet-equiv memo copy strash gatesimp aignet2))) :rule-classes :congruence)
Theorem:
(defthm aignet-parametrize-copy-set-ins-of-ubdd-to-aignet-memo-fix-memo (equal (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet (ubdd-to-aignet-memo-fix memo) copy strash gatesimp aignet2) (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash gatesimp aignet2)))
Theorem:
(defthm aignet-parametrize-copy-set-ins-ubdd-to-aignet-memo-equiv-congruence-on-memo (implies (ubdd-to-aignet-memo-equiv memo memo-equiv) (equal (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash gatesimp aignet2) (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo-equiv copy strash gatesimp aignet2))) :rule-classes :congruence)
Theorem:
(defthm aignet-parametrize-copy-set-ins-of-gatesimp-fix-gatesimp (equal (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash (gatesimp-fix gatesimp) aignet2) (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash gatesimp aignet2)))
Theorem:
(defthm aignet-parametrize-copy-set-ins-gatesimp-equiv-congruence-on-gatesimp (implies (gatesimp-equiv gatesimp gatesimp-equiv) (equal (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash gatesimp aignet2) (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash gatesimp-equiv aignet2))) :rule-classes :congruence)
Theorem:
(defthm aignet-parametrize-copy-set-ins-of-node-list-fix-aignet2 (equal (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash gatesimp (node-list-fix aignet2)) (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash gatesimp aignet2)))
Theorem:
(defthm aignet-parametrize-copy-set-ins-node-list-equiv-congruence-on-aignet2 (implies (node-list-equiv aignet2 aignet2-equiv) (equal (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash gatesimp aignet2) (aignet-parametrize-copy-set-ins n litarr in-ubdds aignet memo copy strash gatesimp aignet2-equiv))) :rule-classes :congruence)