(aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp strash aignet2) → (mv new-copy new-constr-lit new-strash new-aignet2)
Function:
(defun aignet-constprop-sweep (n constmarks litclasses aignet constr-lit copy gatesimp strash aignet2) (declare (xargs :stobjs (constmarks litclasses aignet copy strash aignet2))) (declare (type (unsigned-byte 29) n) (type (unsigned-byte 6) gatesimp)) (declare (xargs :guard (and (posp n) (litp constr-lit) (gatesimp-p gatesimp)))) (declare (xargs :guard (and (<= n (num-fanins aignet)) (<= (num-fanins aignet) (bits-length constmarks)) (<= (num-fanins aignet) (lits-length litclasses)) (<= (num-fanins aignet) (lits-length copy)) (equal (num-regs aignet) (num-regs aignet2)) (equal (num-ins aignet) (num-ins aignet2)) (fanin-litp constr-lit aignet2) (aignet-copies-in-bounds copy aignet2) (ec-call (litclasses-orderedp litclasses))) :split-types t)) (let ((__function__ 'aignet-constprop-sweep)) (declare (ignorable __function__)) (b* ((n (lposfix n)) ((when (mbe :logic (zp (- (num-fanins aignet) n)) :exec (eql (num-fanins aignet) n))) (mbe :logic (non-exec (mv copy (lit-fix constr-lit) strash (node-list-fix aignet2))) :exec (mv copy constr-lit strash aignet2))) (type (id->type n aignet)) ((when (eql type (gate-type))) (b* ((fanin0 (lit-copy (gate-id->fanin0 n aignet) copy)) (fanin1 (lit-copy (gate-id->fanin1 n aignet) copy)) ((mv lit strash aignet2) (if (eql (id->regp n aignet) 1) (aignet-hash-xor fanin0 fanin1 gatesimp strash aignet2) (aignet-hash-and fanin0 fanin1 gatesimp strash aignet2))) (copy (set-lit n lit copy)) ((acl2::hintcontext :gate))) (aignet-constprop-sweep (1+ n) constmarks litclasses aignet constr-lit copy gatesimp strash aignet2))) ((unless (eql type (in-type))) (b* ((copy (set-lit n 0 copy)) ((acl2::hintcontext :const))) (aignet-constprop-sweep (1+ n) constmarks litclasses aignet constr-lit copy gatesimp strash aignet2))) (norm-lit (id-normal-form n constmarks litclasses)) (corresp-lit (get-lit n copy)) ((when (eql (lit->var norm-lit) n)) (b* ((copy (set-lit n corresp-lit copy)) ((acl2::hintcontext :no-replace-in))) (aignet-constprop-sweep (1+ n) constmarks litclasses aignet constr-lit copy gatesimp strash aignet2))) (norm-copy (lit-copy norm-lit copy)) (copy (set-lit n norm-copy copy)) ((mv unequal-lit strash aignet2) (aignet-hash-xor corresp-lit norm-copy gatesimp strash aignet2)) ((mv next-constr-lit strash aignet2) (aignet-hash-and constr-lit (lit-negate unequal-lit) gatesimp strash aignet2)) ((acl2::hintcontext :replace-in))) (aignet-constprop-sweep (1+ n) constmarks litclasses aignet next-constr-lit copy gatesimp strash aignet2))))
Theorem:
(defthm litp-of-aignet-constprop-sweep.new-constr-lit (b* (((mv ?new-copy ?new-constr-lit ?new-strash ?new-aignet2) (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp strash aignet2))) (litp new-constr-lit)) :rule-classes :rewrite)
Theorem:
(defthm aignet-extension-p-of-aignet-constprop-sweep (aignet-extension-p (mv-nth 3 (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp strash aignet2)) aignet2) :rule-classes :rewrite)
Theorem:
(defthm aignet-constprop-sweep-preserves-copy-length (b* (((mv ?new-copy ?new-constr-lit ?new-strash ?new-aignet2) (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp strash aignet2))) (implies (<= (num-fanins aignet) (len copy)) (equal (len new-copy) (len copy)))))
Theorem:
(defthm aignet-constprop-sweep-preserves-copies-in-bounds (b* (((mv ?new-copy ?new-constr-lit ?new-strash ?new-aignet2) (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp strash aignet2))) (implies (aignet-copies-in-bounds copy aignet2) (aignet-copies-in-bounds new-copy new-aignet2))))
Theorem:
(defthm stype-count-of-aignet-constprop-sweep (b* (((mv ?new-copy ?new-constr-lit ?new-strash ?new-aignet2) (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp strash aignet2))) (implies (and (not (equal (stype-fix stype) :and)) (not (equal (stype-fix stype) :xor))) (equal (stype-count stype new-aignet2) (stype-count stype aignet2)))))
Theorem:
(defthm aignet-litp-constr-lit-of-aignet-constprop-sweep (b* (((mv ?new-copy ?new-constr-lit ?new-strash ?new-aignet2) (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp strash aignet2))) (implies (and (aignet-litp constr-lit aignet2) (aignet-copies-in-bounds copy aignet2)) (aignet-litp new-constr-lit new-aignet2))))
Theorem:
(defthm aignet-constprop-sweep-constr-lit-ok-implies-previous (b* (((mv ?new-copy ?new-constr-lit ?new-strash ?new-aignet2) (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp strash aignet2))) (implies (and (equal 0 (lit-eval constr-lit invals regvals aignet2)) (aignet-litp constr-lit aignet2) (aignet-copies-in-bounds copy aignet2)) (equal (lit-eval new-constr-lit invals regvals new-aignet2) 0))))
Theorem:
(defthm aignet-constprop-sweep-invar-when-constr-of-aignet-constprop-sweep (b* (((mv ?new-copy ?new-constr-lit ?new-strash ?new-aignet2) (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp strash aignet2))) (implies (and (equal (lit-eval new-constr-lit invals regvals new-aignet2) 1) (aignet-constprop-sweep-invar (pos-fix n) invals regvals aignet copy aignet2) (aignet-constprop-sweep-cis-ok invals regvals aignet copy aignet2) (aignet-copies-in-bounds copy aignet2) (equal (num-ins aignet2) (num-ins aignet)) (equal (num-regs aignet2) (num-regs aignet))) (aignet-constprop-sweep-invar (+ 1 (fanin-count aignet)) invals regvals aignet new-copy new-aignet2))))
Theorem:
(defthm aignet-constprop-sweep-cis-ok-when-constr-of-aignet-constprop-sweep (b* (((mv ?new-copy ?new-constr-lit ?new-strash ?new-aignet2) (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp strash aignet2))) (implies (and (equal (lit-eval new-constr-lit invals regvals new-aignet2) 1) (aignet-constprop-sweep-invar (pos-fix n) invals regvals aignet copy aignet2) (aignet-constprop-sweep-cis-ok invals regvals aignet copy aignet2) (aignet-copies-in-bounds copy aignet2) (equal (num-ins aignet2) (num-ins aignet)) (equal (num-regs aignet2) (num-regs aignet))) (aignet-constprop-sweep-cis-ok invals regvals aignet new-copy new-aignet2))))
Theorem:
(defthm litclasses-invar-implies-constraint-satisfied-of-aignet-constprop-sweep (b* (((mv ?new-copy ?new-constr-lit ?new-strash ?new-aignet2) (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp strash aignet2))) (implies (and (litclasses-invar invals regvals constmarks litclasses aignet) (aignet-constprop-sweep-invar (pos-fix n) invals regvals aignet copy aignet2) (aignet-constprop-sweep-cis-ok invals regvals aignet copy aignet2) (equal (lit-eval constr-lit invals regvals aignet2) 1) (aignet-litp constr-lit aignet2) (aignet-copies-in-bounds copy aignet2) (equal (num-ins aignet2) (num-ins aignet)) (equal (num-regs aignet2) (num-regs aignet))) (equal (lit-eval new-constr-lit invals regvals new-aignet2) 1))))
Theorem:
(defthm aignet-constprop-sweep-preserves-past-copy-lits (b* (((mv ?new-copy ?new-constr-lit ?new-strash ?new-aignet2) (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp strash aignet2))) (implies (< (nfix m) (pos-fix n)) (equal (nth-lit m new-copy) (nth-lit m copy)))))
Theorem:
(defthm aignet-constprop-sweep-of-pos-fix-n (equal (aignet-constprop-sweep (pos-fix n) constmarks litclasses aignet constr-lit copy gatesimp strash aignet2) (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp strash aignet2)))
Theorem:
(defthm aignet-constprop-sweep-pos-equiv-congruence-on-n (implies (pos-equiv n n-equiv) (equal (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp strash aignet2) (aignet-constprop-sweep n-equiv constmarks litclasses aignet constr-lit copy gatesimp strash aignet2))) :rule-classes :congruence)
Theorem:
(defthm aignet-constprop-sweep-of-node-list-fix-aignet (equal (aignet-constprop-sweep n constmarks litclasses (node-list-fix aignet) constr-lit copy gatesimp strash aignet2) (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp strash aignet2)))
Theorem:
(defthm aignet-constprop-sweep-node-list-equiv-congruence-on-aignet (implies (node-list-equiv aignet aignet-equiv) (equal (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp strash aignet2) (aignet-constprop-sweep n constmarks litclasses aignet-equiv constr-lit copy gatesimp strash aignet2))) :rule-classes :congruence)
Theorem:
(defthm aignet-constprop-sweep-of-lit-fix-constr-lit (equal (aignet-constprop-sweep n constmarks litclasses aignet (lit-fix constr-lit) copy gatesimp strash aignet2) (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp strash aignet2)))
Theorem:
(defthm aignet-constprop-sweep-lit-equiv-congruence-on-constr-lit (implies (lit-equiv constr-lit constr-lit-equiv) (equal (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp strash aignet2) (aignet-constprop-sweep n constmarks litclasses aignet constr-lit-equiv copy gatesimp strash aignet2))) :rule-classes :congruence)
Theorem:
(defthm aignet-constprop-sweep-of-gatesimp-fix-gatesimp (equal (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy (gatesimp-fix gatesimp) strash aignet2) (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp strash aignet2)))
Theorem:
(defthm aignet-constprop-sweep-gatesimp-equiv-congruence-on-gatesimp (implies (gatesimp-equiv gatesimp gatesimp-equiv) (equal (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp strash aignet2) (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp-equiv strash aignet2))) :rule-classes :congruence)
Theorem:
(defthm aignet-constprop-sweep-of-node-list-fix-aignet2 (equal (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp strash (node-list-fix aignet2)) (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp strash aignet2)))
Theorem:
(defthm aignet-constprop-sweep-node-list-equiv-congruence-on-aignet2 (implies (node-list-equiv aignet2 aignet2-equiv) (equal (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp strash aignet2) (aignet-constprop-sweep n constmarks litclasses aignet constr-lit copy gatesimp strash aignet2-equiv))) :rule-classes :congruence)