(aignet-balance-build-superxor lits config levels aignet2 strash) → (mv result-lit new-levels new-aignet2 new-strash)
Function:
(defun aignet-balance-build-superxor (lits config levels aignet2 strash) (declare (xargs :stobjs (levels aignet2 strash))) (declare (xargs :guard (and (lit-listp lits) (balance-config-p config)))) (declare (xargs :guard (and (aignet-lit-listp lits aignet2) (<= (num-fanins aignet2) (u32-length levels))))) (let ((__function__ 'aignet-balance-build-superxor)) (declare (ignorable __function__)) (b* ((lits (lit-list-fix lits)) ((mv neg lits) (cancel-parity-lits (literal-sort lits) 0)) ((when (atom lits)) (mv (mbe :logic (mk-lit 0 neg) :exec neg) levels aignet2 strash)) (lits (levels-sort lits levels))) (aignet-balance-build-superxor-rec neg lits config levels aignet2 strash))))
Theorem:
(defthm litp-of-aignet-balance-build-superxor.result-lit (b* (((mv ?result-lit ?new-levels ?new-aignet2 ?new-strash) (aignet-balance-build-superxor lits config levels aignet2 strash))) (litp result-lit)) :rule-classes :rewrite)
Theorem:
(defthm aignet-balance-build-superxor-correct (b* (((mv ?result-lit ?new-levels ?new-aignet2 ?new-strash) (aignet-balance-build-superxor lits config levels aignet2 strash))) (implies (aignet-lit-listp lits aignet2) (equal (lit-eval result-lit invals regvals new-aignet2) (aignet-eval-parity lits invals regvals aignet2)))))
Theorem:
(defthm aignet-litp-of-aignet-balance-build-superxor (b* (((mv ?result-lit ?new-levels ?new-aignet2 ?new-strash) (aignet-balance-build-superxor lits config levels aignet2 strash))) (implies (aignet-lit-listp lits aignet2) (aignet-litp result-lit new-aignet2))))
Theorem:
(defthm levels-length-of-aignet-balance-build-superxor (b* (((mv ?result-lit ?new-levels ?new-aignet2 ?new-strash) (aignet-balance-build-superxor lits config levels aignet2 strash))) (implies (and (<= (num-fanins aignet2) (len levels)) (aignet-lit-listp lits aignet2)) (< (fanin-count new-aignet2) (len new-levels)))) :rule-classes :linear)
Theorem:
(defthm aignet-extension-p-of-aignet-balance-build-superxor (b* (((mv ?result-lit ?new-levels ?new-aignet2 ?new-strash) (aignet-balance-build-superxor lits config levels aignet2 strash))) (aignet-extension-p new-aignet2 aignet2)))
Theorem:
(defthm stype-counts-of-aignet-balance-build-superxor (b* (((mv ?result-lit ?new-levels ?new-aignet2 ?new-strash) (aignet-balance-build-superxor lits config levels aignet2 strash))) (implies (and (not (equal (stype-fix stype) (and-stype))) (not (equal (stype-fix stype) (xor-stype)))) (equal (stype-count stype new-aignet2) (stype-count stype aignet2)))))
Theorem:
(defthm aignet-balance-build-superxor-of-lit-list-fix-lits (equal (aignet-balance-build-superxor (lit-list-fix lits) config levels aignet2 strash) (aignet-balance-build-superxor lits config levels aignet2 strash)))
Theorem:
(defthm aignet-balance-build-superxor-lit-list-equiv-congruence-on-lits (implies (satlink::lit-list-equiv lits lits-equiv) (equal (aignet-balance-build-superxor lits config levels aignet2 strash) (aignet-balance-build-superxor lits-equiv config levels aignet2 strash))) :rule-classes :congruence)
Theorem:
(defthm aignet-balance-build-superxor-of-balance-config-fix-config (equal (aignet-balance-build-superxor lits (balance-config-fix config) levels aignet2 strash) (aignet-balance-build-superxor lits config levels aignet2 strash)))
Theorem:
(defthm aignet-balance-build-superxor-balance-config-equiv-congruence-on-config (implies (balance-config-equiv config config-equiv) (equal (aignet-balance-build-superxor lits config levels aignet2 strash) (aignet-balance-build-superxor lits config-equiv levels aignet2 strash))) :rule-classes :congruence)