(fraig-core-aux aignet aignet2 config copy strash classes s32v state) → (mv new-aignet2 new-copy new-strash new-classes new-s32v new-state)
Function:
(defun fraig-core-aux (aignet aignet2 config copy strash classes s32v state) (declare (xargs :stobjs (aignet aignet2 copy strash classes s32v state))) (declare (xargs :guard (fraig-config-p config))) (declare (xargs :guard (non-exec (and (equal strash (create-strash)) (equal s32v (create-s32v)) (equal classes (create-classes)))))) (let ((__function__ 'fraig-core-aux)) (declare (ignorable __function__)) (b* (((fraig-config config)) (- (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)) (config.n-outputs-are-initial-equiv-classes (classes-init-n-outputs config.n-outputs-are-initial-equiv-classes config.initial-equiv-classes-last classes aignet)) (t (classes-init (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 config state)) (aignet2 (finish-copy-comb aignet copy aignet2))) (mv aignet2 copy strash classes s32v state))))
Theorem:
(defthm num-ins-of-fraig-core-aux (b* (((mv ?new-aignet2 ?new-copy ?new-strash ?new-classes ?new-s32v ?new-state) (fraig-core-aux aignet aignet2 config copy strash classes s32v 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-state) (fraig-core-aux aignet aignet2 config copy strash classes s32v state))) (equal (stype-count :reg new-aignet2) (stype-count :reg aignet))))
Theorem:
(defthm num-outs-of-fraig-core-aux (b* (((mv ?new-aignet2 ?new-copy ?new-strash ?new-classes ?new-s32v ?new-state) (fraig-core-aux aignet aignet2 config copy strash classes s32v state))) (equal (stype-count :po new-aignet2) (stype-count :po aignet))))
Theorem:
(defthm fraig-core-aux-comb-equivalent (b* (((mv ?new-aignet2 ?new-copy ?new-strash ?new-classes ?new-s32v ?new-state) (fraig-core-aux aignet aignet2 config copy strash classes s32v state))) (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-state) (fraig-core-aux aignet aignet2 config copy strash classes s32v 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-state) (fraig-core-aux aignet aignet2 config copy strash classes s32v 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 (fraig-core-aux aignet aignet2 config copy strash classes s32v state) (fraig-core-aux aignet nil config nil nil nil nil state))))
Theorem:
(defthm w-state-of-fraig-core-aux (b* (((mv ?new-aignet2 ?new-copy ?new-strash ?new-classes ?new-s32v ?new-state) (fraig-core-aux aignet aignet2 config copy strash classes s32v state))) (equal (w new-state) (w state))))
Theorem:
(defthm fraig-core-aux-of-fraig-config-fix-config (equal (fraig-core-aux aignet aignet2 (fraig-config-fix config) copy strash classes s32v state) (fraig-core-aux aignet aignet2 config copy strash classes s32v state)))
Theorem:
(defthm fraig-core-aux-fraig-config-equiv-congruence-on-config (implies (fraig-config-equiv config config-equiv) (equal (fraig-core-aux aignet aignet2 config copy strash classes s32v state) (fraig-core-aux aignet aignet2 config-equiv copy strash classes s32v state))) :rule-classes :congruence)