(fraig-core-aux strict-count aignet aignet2 config output-ranges copy strash classes s32v mark state) → (mv new-aignet2 new-copy new-strash new-classes new-s32v new-mark new-output-ranges new-state)
Function:
(defun fraig-core-aux (strict-count aignet aignet2 config output-ranges copy strash classes s32v mark state) (declare (xargs :stobjs (aignet aignet2 copy strash classes s32v mark state))) (declare (xargs :guard (and (acl2::maybe-natp strict-count) (fraig-config-p config) (aignet-output-range-map-p output-ranges)))) (declare (xargs :guard (non-exec (and (or (not strict-count) (<= strict-count (num-outs aignet))) (equal strash (create-strash)) (equal s32v (create-s32v)) (equal classes (create-classes)) (equal mark (acl2::create-bitarr)))))) (let ((__function__ 'fraig-core-aux)) (declare (ignorable __function__)) (b* (((fraig-config config)) (- (fraig-debug-output-ranges output-ranges aignet)) ((mv outmap output-ranges) (fraig-config-normalized-output-map config output-ranges aignet)) (- (and config.random-seed-name (acl2::seed-random$ config.random-seed-name))) (classes (mbe :logic (non-exec (create-classes)) :exec classes)) (classes (cond (config.outs-only (classes-init-outs classes aignet)) (config.miters-only (classes-init-out-miters classes aignet)) ((fraig-output-map-has-initial-equivs outmap) (b* (((mv offset count) (fraig-output-map-initial-equiv-start/count outmap 0)) (classes (classes-init-n-outputs count offset classes aignet))) (classes-check-consistency (num-fanins aignet) classes) (print-classes-counts classes) classes)) (t (classes-init (num-fanins aignet) classes)))) (mark (fraig-create-aignet-node-mask aignet outmap config.level-limit mark)) (- (print-classes-counts-with-mark classes mark) (classes-check-consistency (num-fanins aignet) classes)) (s32v (mbe :logic (non-exec (create-s32v)) :exec s32v)) (s32v (s32v-resize-cols config.initial-sim-words s32v)) (s32v (s32v-resize-rows (classes-size classes) s32v)) ((mv classes s32v state) (fraig-initial-sim config.initial-sim-rounds s32v classes aignet state)) (strash (mbe :logic (non-exec '(nil)) :exec (strashtab-init (num-gates aignet) nil nil strash))) ((mv copy aignet2) (init-copy-comb aignet copy aignet2)) ((mv aignet2 copy strash classes state) (fraig-sweep aignet aignet2 copy strash classes mark config state)) ((mv output-ranges aignet2) (fraig-finish-copy-nonstrict strict-count output-ranges config.save-candidate-equivs-as config.remove-candidate-equivs classes aignet copy aignet2))) (mv aignet2 copy strash classes s32v mark output-ranges state))))
Theorem:
(defthm aignet-output-range-map-p-of-fraig-core-aux.new-output-ranges (b* (((mv ?new-aignet2 ?new-copy ?new-strash ?new-classes ?new-s32v ?new-mark ?new-output-ranges ?new-state) (fraig-core-aux strict-count aignet aignet2 config output-ranges copy strash classes s32v mark state))) (aignet-output-range-map-p new-output-ranges)) :rule-classes :rewrite)
Theorem:
(defthm num-ins-of-fraig-core-aux (b* (((mv ?new-aignet2 ?new-copy ?new-strash ?new-classes ?new-s32v ?new-mark ?new-output-ranges ?new-state) (fraig-core-aux strict-count aignet aignet2 config output-ranges copy strash classes s32v mark state))) (equal (stype-count :pi new-aignet2) (stype-count :pi aignet))))
Theorem:
(defthm num-regs-of-fraig-core-aux (b* (((mv ?new-aignet2 ?new-copy ?new-strash ?new-classes ?new-s32v ?new-mark ?new-output-ranges ?new-state) (fraig-core-aux strict-count aignet aignet2 config output-ranges copy strash classes s32v mark state))) (equal (stype-count :reg new-aignet2) (stype-count :reg aignet))))
Theorem:
(defthm output-range-map-length-of-fraig-core-aux (b* (((mv ?new-aignet2 ?new-copy ?new-strash ?new-classes ?new-s32v ?new-mark ?new-output-ranges ?new-state) (fraig-core-aux strict-count aignet aignet2 config output-ranges copy strash classes s32v mark state))) (equal (aignet-output-range-map-length new-output-ranges) (stype-count :po new-aignet2))))
Theorem:
(defthm num-outs-of-fraig-core-aux (b* (((mv ?new-aignet2 ?new-copy ?new-strash ?new-classes ?new-s32v ?new-mark ?new-output-ranges ?new-state) (fraig-core-aux strict-count aignet aignet2 config output-ranges copy strash classes s32v mark state))) (implies (not strict-count) (equal (stype-count :po new-aignet2) (stype-count :po aignet)))))
Theorem:
(defthm num-outs-lower-bound-of-fraig-core-aux-nonstrict (b* (((mv ?new-aignet2 ?new-copy ?new-strash ?new-classes ?new-s32v ?new-mark ?new-output-ranges ?new-state) (fraig-core-aux strict-count aignet aignet2 config output-ranges copy strash classes s32v mark state))) (implies strict-count (<= (nfix strict-count) (stype-count :po new-aignet2)))) :rule-classes :linear)
Theorem:
(defthm fraig-core-aux-comb-equivalent (b* (((mv ?new-aignet2 ?new-copy ?new-strash ?new-classes ?new-s32v ?new-mark ?new-output-ranges ?new-state) (fraig-core-aux strict-count aignet aignet2 config output-ranges copy strash classes s32v mark state))) (implies (not strict-count) (comb-equiv new-aignet2 aignet))))
Theorem:
(defthm classes-wellformed-of-fraig-core-aux (b* (((mv ?new-aignet2 ?new-copy ?new-strash ?new-classes ?new-s32v ?new-mark ?new-output-ranges ?new-state) (fraig-core-aux strict-count aignet aignet2 config output-ranges copy strash classes s32v mark state))) (classes-wellformed new-classes)))
Theorem:
(defthm classes-size-of-fraig-core-aux (b* (((mv ?new-aignet2 ?new-copy ?new-strash ?new-classes ?new-s32v ?new-mark ?new-output-ranges ?new-state) (fraig-core-aux strict-count aignet aignet2 config output-ranges copy strash classes s32v mark state))) (equal (classes-size new-classes) (num-fanins aignet))))
Theorem:
(defthm normalize-input-of-fraig-core-aux (implies (syntaxp (not (and (equal aignet2 ''nil) (equal copy ''nil) (equal strash ''nil) (equal classes ''nil) (equal s32v ''nil) (equal mark ''nil)))) (equal (fraig-core-aux aignet strict-count aignet2 config output-ranges copy strash classes s32v mark state) (fraig-core-aux aignet strict-count nil config output-ranges nil nil nil nil nil state))))
Theorem:
(defthm output-eval-of-fraig-core-aux-when-nonstrict (b* (((mv ?new-aignet2 ?new-copy ?new-strash ?new-classes ?new-s32v ?new-mark ?new-output-ranges ?new-state) (fraig-core-aux strict-count aignet aignet2 config output-ranges copy strash classes s32v mark state))) (implies (and strict-count (< (nfix i) (nfix strict-count))) (equal (output-eval i invals regvals new-aignet2) (output-eval i invals regvals aignet)))))
Theorem:
(defthm w-state-of-fraig-core-aux (b* (((mv ?new-aignet2 ?new-copy ?new-strash ?new-classes ?new-s32v ?new-mark ?new-output-ranges ?new-state) (fraig-core-aux strict-count aignet aignet2 config output-ranges copy strash classes s32v mark state))) (equal (w new-state) (w state))))
Theorem:
(defthm fraig-core-aux-of-maybe-natp-fix-strict-count (equal (fraig-core-aux (acl2::maybe-natp-fix strict-count) aignet aignet2 config output-ranges copy strash classes s32v mark state) (fraig-core-aux strict-count aignet aignet2 config output-ranges copy strash classes s32v mark state)))
Theorem:
(defthm fraig-core-aux-maybe-nat-equiv-congruence-on-strict-count (implies (acl2::maybe-nat-equiv strict-count strict-count-equiv) (equal (fraig-core-aux strict-count aignet aignet2 config output-ranges copy strash classes s32v mark state) (fraig-core-aux strict-count-equiv aignet aignet2 config output-ranges copy strash classes s32v mark state))) :rule-classes :congruence)
Theorem:
(defthm fraig-core-aux-of-fraig-config-fix-config (equal (fraig-core-aux strict-count aignet aignet2 (fraig-config-fix config) output-ranges copy strash classes s32v mark state) (fraig-core-aux strict-count aignet aignet2 config output-ranges copy strash classes s32v mark state)))
Theorem:
(defthm fraig-core-aux-fraig-config-equiv-congruence-on-config (implies (fraig-config-equiv config config-equiv) (equal (fraig-core-aux strict-count aignet aignet2 config output-ranges copy strash classes s32v mark state) (fraig-core-aux strict-count aignet aignet2 config-equiv output-ranges copy strash classes s32v mark state))) :rule-classes :congruence)
Theorem:
(defthm fraig-core-aux-of-aignet-output-range-map-fix-output-ranges (equal (fraig-core-aux strict-count aignet aignet2 config (aignet-output-range-map-fix output-ranges) copy strash classes s32v mark state) (fraig-core-aux strict-count aignet aignet2 config output-ranges copy strash classes s32v mark state)))
Theorem:
(defthm fraig-core-aux-aignet-output-range-map-equiv-congruence-on-output-ranges (implies (aignet-output-range-map-equiv output-ranges output-ranges-equiv) (equal (fraig-core-aux strict-count aignet aignet2 config output-ranges copy strash classes s32v mark state) (fraig-core-aux strict-count aignet aignet2 config output-ranges-equiv copy strash classes s32v mark state))) :rule-classes :congruence)