(aignet-lit-constprop lit aignet gatesimp aignet2) → (mv new-lit new-aignet2)
Function:
(defun aignet-lit-constprop (lit aignet gatesimp aignet2) (declare (xargs :stobjs (aignet aignet2))) (declare (type (integer 0 *) lit)) (declare (xargs :guard (and (litp lit) (gatesimp-p gatesimp)))) (declare (xargs :split-types t :guard (fanin-litp lit aignet))) (let ((__function__ 'aignet-lit-constprop)) (declare (ignorable __function__)) (b* (((local-stobjs copy strash) (mv new-lit aignet2 strash copy)) ((mv constr-lit strash copy aignet2) (aignet-lit-constprop-init-and-sweep lit aignet gatesimp strash copy aignet2)) ((acl2::hintcontext-bind ((sweep-aignet2 aignet2)))) ((mv conj strash aignet2) (aignet-hash-and constr-lit (lit-copy (lit-abs lit) copy) gatesimp strash aignet2)) (result-lit (lit-negate-cond conj (lit->neg lit))) ((acl2::hintcontext :here))) (mv result-lit aignet2 strash copy))))
Theorem:
(defthm litp-of-aignet-lit-constprop.new-lit (b* (((mv ?new-lit ?new-aignet2) (aignet-lit-constprop lit aignet gatesimp aignet2))) (litp new-lit)) :rule-classes :rewrite)
Theorem:
(defthm stype-count-of-aignet-lit-constprop (b* (((mv ?new-lit ?new-aignet2) (aignet-lit-constprop lit aignet gatesimp 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 (b* (((mv ?new-lit ?new-aignet2) (aignet-lit-constprop lit aignet gatesimp aignet2))) (implies (and (aignet-litp lit aignet)) (aignet-litp new-lit new-aignet2))))
Theorem:
(defthm aignet-lit-constprop-correct (b* (((mv ?new-lit ?new-aignet2) (aignet-lit-constprop lit aignet gatesimp aignet2))) (implies (aignet-litp lit aignet) (equal (lit-eval new-lit invals regvals new-aignet2) (lit-eval lit invals regvals aignet)))))
Theorem:
(defthm normalize-inputs-of-aignet-lit-constprop (b* nil (implies (syntaxp (not (equal aignet2 ''nil))) (equal (aignet-lit-constprop lit aignet gatesimp aignet2) (let ((aignet2 nil)) (aignet-lit-constprop lit aignet gatesimp aignet2))))))
Theorem:
(defthm aignet-lit-constprop-of-lit-fix-lit (equal (aignet-lit-constprop (lit-fix lit) aignet gatesimp aignet2) (aignet-lit-constprop lit aignet gatesimp aignet2)))
Theorem:
(defthm aignet-lit-constprop-lit-equiv-congruence-on-lit (implies (lit-equiv lit lit-equiv) (equal (aignet-lit-constprop lit aignet gatesimp aignet2) (aignet-lit-constprop lit-equiv aignet gatesimp aignet2))) :rule-classes :congruence)
Theorem:
(defthm aignet-lit-constprop-of-node-list-fix-aignet (equal (aignet-lit-constprop lit (node-list-fix aignet) gatesimp aignet2) (aignet-lit-constprop lit aignet gatesimp aignet2)))
Theorem:
(defthm aignet-lit-constprop-node-list-equiv-congruence-on-aignet (implies (node-list-equiv aignet aignet-equiv) (equal (aignet-lit-constprop lit aignet gatesimp aignet2) (aignet-lit-constprop lit aignet-equiv gatesimp aignet2))) :rule-classes :congruence)
Theorem:
(defthm aignet-lit-constprop-of-gatesimp-fix-gatesimp (equal (aignet-lit-constprop lit aignet (gatesimp-fix gatesimp) aignet2) (aignet-lit-constprop lit aignet gatesimp aignet2)))
Theorem:
(defthm aignet-lit-constprop-gatesimp-equiv-congruence-on-gatesimp (implies (gatesimp-equiv gatesimp gatesimp-equiv) (equal (aignet-lit-constprop lit aignet gatesimp aignet2) (aignet-lit-constprop lit aignet gatesimp-equiv aignet2))) :rule-classes :congruence)
Theorem:
(defthm aignet-lit-constprop-of-node-list-fix-aignet2 (equal (aignet-lit-constprop lit aignet gatesimp (node-list-fix aignet2)) (aignet-lit-constprop lit aignet gatesimp aignet2)))
Theorem:
(defthm aignet-lit-constprop-node-list-equiv-congruence-on-aignet2 (implies (node-list-equiv aignet2 aignet2-equiv) (equal (aignet-lit-constprop lit aignet gatesimp aignet2) (aignet-lit-constprop lit aignet gatesimp aignet2-equiv))) :rule-classes :congruence)