(aignet-lit-constprop-init-and-sweep lit aignet gatesimp strash copy aignet2) → (mv constraint new-strash new-copy new-aignet2)
Function:
(defun aignet-lit-constprop-init-and-sweep (lit aignet gatesimp strash copy aignet2) (declare (xargs :stobjs (aignet strash copy aignet2))) (declare (type (integer 0 *) lit)) (declare (xargs :guard (and (litp lit) (gatesimp-p gatesimp)))) (declare (xargs :split-types t :guard (and (fanin-litp lit aignet) (non-exec (equal copy (acl2::create-bitarr)))))) (let ((__function__ 'aignet-lit-constprop-init-and-sweep)) (declare (ignorable __function__)) (b* (((local-stobjs constmarks litclasses) (mv constr-lit strash copy aignet2 constmarks litclasses)) (aignet2 (aignet-init 1 (num-ins aignet) (num-regs aignet) (+ 10 (ash (* 5 (num-fanins aignet)) -2)) aignet2)) (aignet2 (aignet-add-ins (num-ins aignet) aignet2)) (aignet2 (aignet-add-regs (num-regs aignet) aignet2)) (copy (mbe :logic (non-exec (acl2::create-bitarr)) :exec copy)) (copy (resize-lits (num-fanins aignet) copy)) (copy (aignet-copy-set-ins 0 aignet copy aignet2)) (copy (aignet-copy-set-regs 0 aignet copy aignet2)) ((acl2::hintcontext-bind ((orig-constmarks constmarks) (orig-litclasses litclasses)))) ((mv contra constmarks litclasses) (aignet-mark-const-nodes-top (lit-abs lit) aignet constmarks litclasses)) (- (aignet-constprop-stats 0 constmarks litclasses aignet 0 0 0 0)) ((when contra) (b* ((- (cw "Contradiction in top-level AND gate -- literal is constant ~x0~%" (lit->neg lit))) ((acl2::hintcontext :contra))) (mv 0 strash copy aignet2 constmarks litclasses))) (strash (strashtab-init (+ 10 (ash (* 5 (num-gates aignet)) -2)) nil nil strash)) ((acl2::hintcontext-bind ((orig-copy copy) (orig-strash strash) (orig-aignet2 aignet2)))) ((mv copy constr-lit strash aignet2) (aignet-constprop-sweep 1 constmarks litclasses aignet 1 copy gatesimp strash aignet2)) ((acl2::hintcontext :no-contra))) (mv constr-lit strash copy aignet2 constmarks litclasses))))
Theorem:
(defthm litp-of-aignet-lit-constprop-init-and-sweep.constraint (b* (((mv ?constraint ?new-strash ?new-copy ?new-aignet2) (aignet-lit-constprop-init-and-sweep lit aignet gatesimp strash copy aignet2))) (litp constraint)) :rule-classes :rewrite)
Theorem:
(defthm stype-count-of-aignet-lit-constprop-init-and-sweep (b* (((mv ?constraint ?new-strash ?new-copy ?new-aignet2) (aignet-lit-constprop-init-and-sweep lit aignet gatesimp strash copy aignet2))) (and (equal (stype-count :pi new-aignet2) (stype-count :pi aignet)) (equal (stype-count :reg new-aignet2) (stype-count :reg aignet)) (equal (stype-count :po new-aignet2) 0) (equal (stype-count :nxst new-aignet2) 0) (equal (stype-count :const new-aignet2) 0))))
Theorem:
(defthm aignet-litp-of-aignet-lit-constprop-init-and-sweep (b* (((mv ?constraint ?new-strash ?new-copy ?new-aignet2) (aignet-lit-constprop-init-and-sweep lit aignet gatesimp strash copy aignet2))) (implies (and (aignet-litp lit aignet)) (aignet-litp constraint new-aignet2))))
Theorem:
(defthm copy-len-of-aignet-lit-constprop-init-and-sweep (b* (((mv ?constraint ?new-strash ?new-copy ?new-aignet2) (aignet-lit-constprop-init-and-sweep lit aignet gatesimp strash copy aignet2))) (equal (len new-copy) (num-fanins aignet))))
Theorem:
(defthm aignet-copies-in-bounds-of-aignet-lit-constprop-init-and-sweep (b* (((mv ?constraint ?new-strash ?new-copy ?new-aignet2) (aignet-lit-constprop-init-and-sweep lit aignet gatesimp strash copy aignet2))) (aignet-copies-in-bounds new-copy new-aignet2)))
Theorem:
(defthm aignet-lit-constprop-init-and-sweep-constr-correct (b* (((mv ?constraint ?new-strash ?new-copy ?new-aignet2) (aignet-lit-constprop-init-and-sweep lit aignet gatesimp strash copy aignet2))) (implies (and (aignet-litp lit aignet) (equal (lit-eval (lit-abs lit) invals regvals aignet) 1)) (equal (lit-eval constraint invals regvals new-aignet2) 1))))
Theorem:
(defthm aignet-lit-constprop-init-and-sweep-correct (b* (((mv ?constraint ?new-strash ?new-copy ?new-aignet2) (aignet-lit-constprop-init-and-sweep lit aignet gatesimp strash copy aignet2))) (implies (and (aignet-litp lit aignet) (equal (lit-eval constraint invals regvals new-aignet2) 1)) (equal (lit-eval (lit-copy lit new-copy) invals regvals new-aignet2) (lit-eval lit invals regvals aignet)))))
Theorem:
(defthm aignet-lit-constprop-init-and-sweep-correct-nth-lit (b* (((mv ?constraint ?new-strash ?new-copy ?new-aignet2) (aignet-lit-constprop-init-and-sweep lit aignet gatesimp strash copy aignet2))) (implies (and (aignet-litp lit aignet) (equal (lit-eval constraint invals regvals new-aignet2) 1)) (equal (lit-eval (nth-lit (lit->var lit) new-copy) invals regvals new-aignet2) (lit-eval (lit-abs lit) invals regvals aignet)))))
Theorem:
(defthm normalize-inputs-of-aignet-lit-constprop-init-and-sweep (b* nil (implies (syntaxp (not (equal aignet2 ''nil))) (equal (aignet-lit-constprop-init-and-sweep lit aignet gatesimp strash copy aignet2) (let ((aignet2 nil)) (aignet-lit-constprop-init-and-sweep lit aignet gatesimp strash copy aignet2))))))
Theorem:
(defthm aignet-lit-constprop-init-and-sweep-of-lit-fix-lit (equal (aignet-lit-constprop-init-and-sweep (lit-fix lit) aignet gatesimp strash copy aignet2) (aignet-lit-constprop-init-and-sweep lit aignet gatesimp strash copy aignet2)))
Theorem:
(defthm aignet-lit-constprop-init-and-sweep-lit-equiv-congruence-on-lit (implies (lit-equiv lit lit-equiv) (equal (aignet-lit-constprop-init-and-sweep lit aignet gatesimp strash copy aignet2) (aignet-lit-constprop-init-and-sweep lit-equiv aignet gatesimp strash copy aignet2))) :rule-classes :congruence)
Theorem:
(defthm aignet-lit-constprop-init-and-sweep-of-node-list-fix-aignet (equal (aignet-lit-constprop-init-and-sweep lit (node-list-fix aignet) gatesimp strash copy aignet2) (aignet-lit-constprop-init-and-sweep lit aignet gatesimp strash copy aignet2)))
Theorem:
(defthm aignet-lit-constprop-init-and-sweep-node-list-equiv-congruence-on-aignet (implies (node-list-equiv aignet aignet-equiv) (equal (aignet-lit-constprop-init-and-sweep lit aignet gatesimp strash copy aignet2) (aignet-lit-constprop-init-and-sweep lit aignet-equiv gatesimp strash copy aignet2))) :rule-classes :congruence)
Theorem:
(defthm aignet-lit-constprop-init-and-sweep-of-gatesimp-fix-gatesimp (equal (aignet-lit-constprop-init-and-sweep lit aignet (gatesimp-fix gatesimp) strash copy aignet2) (aignet-lit-constprop-init-and-sweep lit aignet gatesimp strash copy aignet2)))
Theorem:
(defthm aignet-lit-constprop-init-and-sweep-gatesimp-equiv-congruence-on-gatesimp (implies (gatesimp-equiv gatesimp gatesimp-equiv) (equal (aignet-lit-constprop-init-and-sweep lit aignet gatesimp strash copy aignet2) (aignet-lit-constprop-init-and-sweep lit aignet gatesimp-equiv strash copy aignet2))) :rule-classes :congruence)
Theorem:
(defthm aignet-lit-constprop-init-and-sweep-of-node-list-fix-aignet2 (equal (aignet-lit-constprop-init-and-sweep lit aignet gatesimp strash copy (node-list-fix aignet2)) (aignet-lit-constprop-init-and-sweep lit aignet gatesimp strash copy aignet2)))
Theorem:
(defthm aignet-lit-constprop-init-and-sweep-node-list-equiv-congruence-on-aignet2 (implies (node-list-equiv aignet2 aignet2-equiv) (equal (aignet-lit-constprop-init-and-sweep lit aignet gatesimp strash copy aignet2) (aignet-lit-constprop-init-and-sweep lit aignet gatesimp strash copy aignet2-equiv))) :rule-classes :congruence)