(aignet-balance-build-superxor-rec neg lits config levels aignet2 strash) → (mv result-lit new-levels new-aignet2 new-strash)
Function:
(defun aignet-balance-build-superxor-rec (neg lits config levels aignet2 strash) (declare (xargs :stobjs (levels aignet2 strash))) (declare (xargs :guard (and (bitp neg) (lit-listp lits) (balance-config-p config)))) (declare (xargs :guard (and (consp lits) (aignet-lit-listp lits aignet2) (<= (num-fanins aignet2) (u32-length levels))))) (let ((__function__ 'aignet-balance-build-superxor-rec)) (declare (ignorable __function__)) (b* (((when (atom (cdr lits))) (mv (lit-negate-cond (car lits) neg) levels aignet2 strash)) ((mv lit1 lit2 rest) (aignet-balance-find-xor-pairing lits config levels aignet2 strash)) ((balance-config config)) ((mv new-lit strash aignet2) (aignet-hash-xor lit1 lit2 config.gatesimp strash aignet2)) (levels (aignet-update-node-level (lit-id new-lit) levels aignet2)) ((when (eql (lit-id new-lit) 0)) (if (consp rest) (aignet-balance-build-superxor-rec (b-xor (lit-neg new-lit) neg) rest config levels aignet2 strash) (mv (mbe :logic (mk-lit 0 (b-xor (lit-neg new-lit) neg)) :exec (b-xor (lit-neg new-lit) neg)) levels aignet2 strash))) (rest (levels-sort-insert new-lit rest levels))) (aignet-balance-build-superxor-rec neg rest config levels aignet2 strash))))
Theorem:
(defthm litp-of-aignet-balance-build-superxor-rec.result-lit (b* (((mv ?result-lit ?new-levels ?new-aignet2 ?new-strash) (aignet-balance-build-superxor-rec neg lits config levels aignet2 strash))) (litp result-lit)) :rule-classes :rewrite)
Theorem:
(defthm aignet-balance-build-superxor-rec-correct (b* (((mv ?result-lit ?new-levels ?new-aignet2 ?new-strash) (aignet-balance-build-superxor-rec neg lits config levels aignet2 strash))) (implies (and (aignet-lit-listp lits aignet2) (consp lits)) (equal (lit-eval result-lit invals regvals new-aignet2) (b-xor neg (aignet-eval-parity lits invals regvals aignet2))))))
Theorem:
(defthm aignet-litp-of-aignet-balance-build-superxor-rec (b* (((mv ?result-lit ?new-levels ?new-aignet2 ?new-strash) (aignet-balance-build-superxor-rec neg 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-rec (b* (((mv ?result-lit ?new-levels ?new-aignet2 ?new-strash) (aignet-balance-build-superxor-rec neg 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-rec (b* (((mv ?result-lit ?new-levels ?new-aignet2 ?new-strash) (aignet-balance-build-superxor-rec neg lits config levels aignet2 strash))) (aignet-extension-p new-aignet2 aignet2)))
Theorem:
(defthm stype-counts-of-aignet-balance-build-superxor-rec (b* (((mv ?result-lit ?new-levels ?new-aignet2 ?new-strash) (aignet-balance-build-superxor-rec neg 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-rec-of-bfix-neg (equal (aignet-balance-build-superxor-rec (bfix neg) lits config levels aignet2 strash) (aignet-balance-build-superxor-rec neg lits config levels aignet2 strash)))
Theorem:
(defthm aignet-balance-build-superxor-rec-bit-equiv-congruence-on-neg (implies (bit-equiv neg neg-equiv) (equal (aignet-balance-build-superxor-rec neg lits config levels aignet2 strash) (aignet-balance-build-superxor-rec neg-equiv lits config levels aignet2 strash))) :rule-classes :congruence)
Theorem:
(defthm aignet-balance-build-superxor-rec-of-lit-list-fix-lits (equal (aignet-balance-build-superxor-rec neg (lit-list-fix lits) config levels aignet2 strash) (aignet-balance-build-superxor-rec neg lits config levels aignet2 strash)))
Theorem:
(defthm aignet-balance-build-superxor-rec-lit-list-equiv-congruence-on-lits (implies (satlink::lit-list-equiv lits lits-equiv) (equal (aignet-balance-build-superxor-rec neg lits config levels aignet2 strash) (aignet-balance-build-superxor-rec neg lits-equiv config levels aignet2 strash))) :rule-classes :congruence)
Theorem:
(defthm aignet-balance-build-superxor-rec-of-balance-config-fix-config (equal (aignet-balance-build-superxor-rec neg lits (balance-config-fix config) levels aignet2 strash) (aignet-balance-build-superxor-rec neg lits config levels aignet2 strash)))
Theorem:
(defthm aignet-balance-build-superxor-rec-balance-config-equiv-congruence-on-config (implies (balance-config-equiv config config-equiv) (equal (aignet-balance-build-superxor-rec neg lits config levels aignet2 strash) (aignet-balance-build-superxor-rec neg lits config-equiv levels aignet2 strash))) :rule-classes :congruence)