(aignet-balance-find-xor-pairing lits config levels aignet2 strash) → (mv first second rest)
Function:
(defun aignet-balance-find-xor-pairing (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) (consp (cdr lits)) (aignet-lit-listp lits aignet2) (<= (num-fanins aignet2) (u32-length levels))))) (let ((__function__ 'aignet-balance-find-xor-pairing)) (declare (ignorable __function__)) (b* ((first (lit-fix (car lits))) (second (lit-fix (cadr lits))) ((balance-config config)) (level-ref1 (if config.search-higher-levels 0 second)) ((mv pairing rest) (mbe :logic (aignet-balance-find-xor-pairing-rec first config.search-limit level-ref1 (cdr lits) levels config.gatesimp aignet2 strash) :exec (if (<= first 536870911) (aignet-balance-find-xor-pairing-rec first config.search-limit level-ref1 (cdr lits) levels config.gatesimp aignet2 strash) (ec-call (aignet-balance-find-xor-pairing-rec first config.search-limit level-ref1 (cdr lits) levels config.gatesimp aignet2 strash))))) ((when pairing) (mv first pairing rest)) ((when (or (not config.search-second-lit) (atom (cddr lits)))) (mv first second (lit-list-fix (cddr lits)))) (level-ref2 (if config.search-higher-levels 0 (caddr lits))) ((mv pairing rest) (mbe :logic (aignet-balance-find-xor-pairing-rec second config.search-limit level-ref2 (cddr lits) levels config.gatesimp aignet2 strash) :exec (if (<= second 536870911) (aignet-balance-find-xor-pairing-rec second config.search-limit level-ref2 (cddr lits) levels config.gatesimp aignet2 strash) (ec-call (aignet-balance-find-xor-pairing-rec second config.search-limit level-ref2 (cddr lits) levels config.gatesimp aignet2 strash))))) ((when pairing) (mv second pairing (cons first rest)))) (mv first second (lit-list-fix (cddr lits))))))
Theorem:
(defthm litp-of-aignet-balance-find-xor-pairing.first (b* (((mv common-lisp::?first common-lisp::?second common-lisp::?rest) (aignet-balance-find-xor-pairing lits config levels aignet2 strash))) (litp first)) :rule-classes :rewrite)
Theorem:
(defthm litp-of-aignet-balance-find-xor-pairing.second (b* (((mv common-lisp::?first common-lisp::?second common-lisp::?rest) (aignet-balance-find-xor-pairing lits config levels aignet2 strash))) (litp second)) :rule-classes :rewrite)
Theorem:
(defthm lit-listp-of-aignet-balance-find-xor-pairing.rest (b* (((mv common-lisp::?first common-lisp::?second common-lisp::?rest) (aignet-balance-find-xor-pairing lits config levels aignet2 strash))) (lit-listp rest)) :rule-classes :rewrite)
Theorem:
(defthm aignet-balance-find-xor-pairing-correct (b* (((mv common-lisp::?first common-lisp::?second common-lisp::?rest) (aignet-balance-find-xor-pairing lits config levels aignet2 strash))) (implies (and (consp lits) (consp (cdr lits))) (equal (aignet-eval-parity (list* first second rest) invals regvals aignet2) (aignet-eval-parity lits invals regvals aignet2)))))
Theorem:
(defthm len-of-aignet-balance-find-xor-pairing (b* (((mv common-lisp::?first common-lisp::?second common-lisp::?rest) (aignet-balance-find-xor-pairing lits config levels aignet2 strash))) (implies (and (consp lits) (consp (cdr lits))) (equal (len rest) (- (len lits) 2)))))
Theorem:
(defthm aignet-lit-listp-of-aignet-balance-find-xor-pairing (b* (((mv common-lisp::?first common-lisp::?second common-lisp::?rest) (aignet-balance-find-xor-pairing lits config levels aignet2 strash))) (implies (and (aignet-lit-listp lits aignet) (consp lits) (consp (cdr lits))) (aignet-lit-listp rest aignet))))
Theorem:
(defthm aignet-litp-of-aignet-balance-find-xor-pairing (b* (((mv common-lisp::?first common-lisp::?second common-lisp::?rest) (aignet-balance-find-xor-pairing lits config levels aignet2 strash))) (implies (and (aignet-lit-listp lits aignet) (consp lits) (consp (cdr lits))) (and (aignet-litp first aignet) (aignet-litp second aignet)))))
Theorem:
(defthm aignet-balance-find-xor-pairing-of-lit-list-fix-lits (equal (aignet-balance-find-xor-pairing (lit-list-fix lits) config levels aignet2 strash) (aignet-balance-find-xor-pairing lits config levels aignet2 strash)))
Theorem:
(defthm aignet-balance-find-xor-pairing-lit-list-equiv-congruence-on-lits (implies (satlink::lit-list-equiv lits lits-equiv) (equal (aignet-balance-find-xor-pairing lits config levels aignet2 strash) (aignet-balance-find-xor-pairing lits-equiv config levels aignet2 strash))) :rule-classes :congruence)
Theorem:
(defthm aignet-balance-find-xor-pairing-of-balance-config-fix-config (equal (aignet-balance-find-xor-pairing lits (balance-config-fix config) levels aignet2 strash) (aignet-balance-find-xor-pairing lits config levels aignet2 strash)))
Theorem:
(defthm aignet-balance-find-xor-pairing-balance-config-equiv-congruence-on-config (implies (balance-config-equiv config config-equiv) (equal (aignet-balance-find-xor-pairing lits config levels aignet2 strash) (aignet-balance-find-xor-pairing lits config-equiv levels aignet2 strash))) :rule-classes :congruence)