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