(fraig-finish-copy-outs offset output-ranges equivs-name remove-equivs classes aignet copy aignet2) → (mv new-output-ranges new-aignet2)
Function:
(defun fraig-finish-copy-outs (offset output-ranges equivs-name remove-equivs classes aignet copy aignet2) (declare (xargs :stobjs (classes aignet copy aignet2))) (declare (xargs :guard (and (natp offset) (aignet-output-range-map-p output-ranges) (symbolp equivs-name) (symbolp remove-equivs)))) (declare (xargs :guard (and (<= (num-fanins aignet) (lits-length copy)) (aignet-copies-in-bounds copy aignet2) (equal (+ offset (aignet-output-range-map-length output-ranges)) (num-outs aignet)) (classes-wellformed classes) (equal (classes-size classes) (num-fanins aignet))))) (let ((__function__ 'fraig-finish-copy-outs)) (declare (ignorable __function__)) (b* ((equivs-name (mbe :logic (acl2::symbol-fix equivs-name) :exec equivs-name)) (remove-equivs (mbe :logic (acl2::symbol-fix remove-equivs) :exec remove-equivs)) ((when (atom output-ranges)) (if equivs-name (b* (((mv count aignet2) (fraig-add-equiv-class-outputs classes copy aignet2))) (mv (list (cons equivs-name count)) aignet2)) (mv nil aignet2))) ((unless (mbt (consp (car output-ranges)))) (fraig-finish-copy-outs offset (cdr output-ranges) equivs-name remove-equivs classes aignet copy aignet2)) (name (mbe :logic (acl2::symbol-fix (caar output-ranges)) :exec (caar output-ranges))) (len (lnfix (cdar output-ranges))) ((when (and equivs-name (eq name equivs-name))) (b* (((mv count aignet2) (fraig-add-equiv-class-outputs classes copy aignet2)) (aignet2 (aignet-copy-outs-range (+ (lnfix offset) len) (aignet-output-range-map-length (cdr output-ranges)) aignet copy aignet2))) (mv (cons (cons equivs-name count) (aignet-output-range-map-fix (cdr output-ranges))) aignet2))) ((when (and remove-equivs (eq name remove-equivs))) (fraig-finish-copy-outs (+ (lnfix offset) len) (cdr output-ranges) equivs-name remove-equivs classes aignet copy aignet2)) (aignet2 (aignet-copy-outs-range offset len aignet copy aignet2)) ((mv rest-output-ranges aignet2) (fraig-finish-copy-outs (+ (lnfix offset) len) (cdr output-ranges) equivs-name remove-equivs classes aignet copy aignet2))) (mv (cons (mbe :logic (cons name len) :exec (car output-ranges)) rest-output-ranges) aignet2))))
Theorem:
(defthm aignet-output-range-map-p-of-fraig-finish-copy-outs.new-output-ranges (b* (((mv ?new-output-ranges ?new-aignet2) (fraig-finish-copy-outs offset output-ranges equivs-name remove-equivs classes aignet copy aignet2))) (aignet-output-range-map-p new-output-ranges)) :rule-classes :rewrite)
Theorem:
(defthm aignet-extension-p-of-fraig-finish-copy-outs (b* (((mv ?new-output-ranges ?new-aignet2) (fraig-finish-copy-outs offset output-ranges equivs-name remove-equivs classes aignet copy aignet2))) (aignet-extension-p new-aignet2 aignet2)))
Theorem:
(defthm stype-count-of-fraig-finish-copy-outs (b* (((mv ?new-output-ranges ?new-aignet2) (fraig-finish-copy-outs offset output-ranges equivs-name remove-equivs classes aignet copy aignet2))) (implies (not (equal (stype-fix stype) :po)) (equal (stype-count stype new-aignet2) (stype-count stype aignet2)))))
Theorem:
(defthm output-range-length-of-fraig-finish-copy-outs (b* (((mv ?new-output-ranges ?new-aignet2) (fraig-finish-copy-outs offset output-ranges equivs-name remove-equivs classes aignet copy aignet2))) (equal (aignet-output-range-map-length new-output-ranges) (- (stype-count :po new-aignet2) (stype-count :po aignet2)))))
Theorem:
(defthm fraig-finish-copy-outs-of-nfix-offset (equal (fraig-finish-copy-outs (nfix offset) output-ranges equivs-name remove-equivs classes aignet copy aignet2) (fraig-finish-copy-outs offset output-ranges equivs-name remove-equivs classes aignet copy aignet2)))
Theorem:
(defthm fraig-finish-copy-outs-nat-equiv-congruence-on-offset (implies (nat-equiv offset offset-equiv) (equal (fraig-finish-copy-outs offset output-ranges equivs-name remove-equivs classes aignet copy aignet2) (fraig-finish-copy-outs offset-equiv output-ranges equivs-name remove-equivs classes aignet copy aignet2))) :rule-classes :congruence)
Theorem:
(defthm fraig-finish-copy-outs-of-aignet-output-range-map-fix-output-ranges (equal (fraig-finish-copy-outs offset (aignet-output-range-map-fix output-ranges) equivs-name remove-equivs classes aignet copy aignet2) (fraig-finish-copy-outs offset output-ranges equivs-name remove-equivs classes aignet copy aignet2)))
Theorem:
(defthm fraig-finish-copy-outs-aignet-output-range-map-equiv-congruence-on-output-ranges (implies (aignet-output-range-map-equiv output-ranges output-ranges-equiv) (equal (fraig-finish-copy-outs offset output-ranges equivs-name remove-equivs classes aignet copy aignet2) (fraig-finish-copy-outs offset output-ranges-equiv equivs-name remove-equivs classes aignet copy aignet2))) :rule-classes :congruence)
Theorem:
(defthm fraig-finish-copy-outs-of-symbol-fix-equivs-name (equal (fraig-finish-copy-outs offset output-ranges (acl2::symbol-fix equivs-name) remove-equivs classes aignet copy aignet2) (fraig-finish-copy-outs offset output-ranges equivs-name remove-equivs classes aignet copy aignet2)))
Theorem:
(defthm fraig-finish-copy-outs-symbol-equiv-congruence-on-equivs-name (implies (acl2::symbol-equiv equivs-name equivs-name-equiv) (equal (fraig-finish-copy-outs offset output-ranges equivs-name remove-equivs classes aignet copy aignet2) (fraig-finish-copy-outs offset output-ranges equivs-name-equiv remove-equivs classes aignet copy aignet2))) :rule-classes :congruence)
Theorem:
(defthm fraig-finish-copy-outs-of-symbol-fix-remove-equivs (equal (fraig-finish-copy-outs offset output-ranges equivs-name (acl2::symbol-fix remove-equivs) classes aignet copy aignet2) (fraig-finish-copy-outs offset output-ranges equivs-name remove-equivs classes aignet copy aignet2)))
Theorem:
(defthm fraig-finish-copy-outs-symbol-equiv-congruence-on-remove-equivs (implies (acl2::symbol-equiv remove-equivs remove-equivs-equiv) (equal (fraig-finish-copy-outs offset output-ranges equivs-name remove-equivs classes aignet copy aignet2) (fraig-finish-copy-outs offset output-ranges equivs-name remove-equivs-equiv classes aignet copy aignet2))) :rule-classes :congruence)