(fraig-sweep aignet aignet2 copy strash classes config state) → (mv new-aignet2 new-copy new-strash new-classes new-state)
Function:
(defun fraig-sweep (aignet aignet2 copy strash classes config state) (declare (xargs :stobjs (aignet aignet2 copy strash classes state))) (declare (xargs :guard (fraig-config-p config))) (declare (xargs :guard (and (<= (num-fanins aignet) (lits-length copy)) (aignet-copies-in-bounds copy aignet2) (classes-wellformed classes) (equal (classes-size classes) (num-fanins aignet)) (equal (num-ins aignet) (num-ins aignet2)) (equal (num-regs aignet) (num-regs aignet2))))) (let ((__function__ 'fraig-sweep)) (declare (ignorable __function__)) (b* (((local-stobjs fraig-ctrexes sat-lits aignet-refcounts aignet-levels fraig-stats) (mv aignet2 copy strash fraig-ctrexes classes aignet-refcounts sat-lits aignet-levels fraig-stats state)) ((ipasir::local-ipasir ipasir) (mv aignet2 copy strash fraig-ctrexes classes aignet-refcounts sat-lits ipasir aignet-levels fraig-stats state)) ((fraig-config config)) (ipasir (ipasir-set-limit ipasir config.ipasir-limit)) (fraig-ctrexes (fraig-ctrexes-init config.sim-words fraig-ctrexes aignet)) (sat-lits (resize-aignet->sat (ash (num-fanins aignet) -1) sat-lits)) (aignet-levels (aignet-record-levels aignet aignet-levels)) ((mv nclasses nconst-lits nclass-lits) (classes-counts classes)) (fraig-stats (update-fraig-initial-nclasses nclasses fraig-stats)) (fraig-stats (update-fraig-initial-nconst-lits nconst-lits fraig-stats)) (fraig-stats (update-fraig-initial-nclass-lits nclass-lits fraig-stats)) (- (print-fraig-stats-initial fraig-stats)) ((mv aignet2 copy strash fraig-ctrexes classes aignet-refcounts sat-lits ipasir fraig-stats state) (fraig-sweep-aux 0 aignet aignet2 copy strash fraig-ctrexes classes aignet-refcounts sat-lits ipasir aignet-levels fraig-stats config state)) (- (print-aignet-stats "Tmp" aignet2)) (- (print-fraig-stats-noninitial classes ipasir fraig-stats))) (mv aignet2 copy strash fraig-ctrexes classes aignet-refcounts sat-lits ipasir aignet-levels fraig-stats state))))
Theorem:
(defthm aignet-extension-p-of-fraig-sweep (aignet-extension-p (mv-nth 0 (fraig-sweep aignet aignet2 copy strash classes config state)) aignet2) :rule-classes :rewrite)
Theorem:
(defthm classes-wellformed-of-fraig-sweep (b* (((mv ?new-aignet2 ?new-copy ?new-strash ?new-classes ?new-state) (fraig-sweep aignet aignet2 copy strash classes config state))) (implies (classes-wellformed classes) (classes-wellformed new-classes))))
Theorem:
(defthm classes-size-of-fraig-sweep (b* (((mv ?new-aignet2 ?new-copy ?new-strash ?new-classes ?new-state) (fraig-sweep aignet aignet2 copy strash classes config state))) (equal (classes-size new-classes) (classes-size classes))))
Theorem:
(defthm stype-count-preserved-of-fraig-sweep (b* (((mv ?new-aignet2 ?new-copy ?new-strash ?new-classes ?new-state) (fraig-sweep aignet aignet2 copy strash classes config state))) (implies (and (not (eq (stype-fix stype) (and-stype))) (not (eq (stype-fix stype) (xor-stype)))) (equal (stype-count stype new-aignet2) (stype-count stype aignet2)))))
Theorem:
(defthm copy-len-of-fraig-sweep (b* (((mv ?new-aignet2 ?new-copy ?new-strash ?new-classes ?new-state) (fraig-sweep aignet aignet2 copy strash classes config state))) (implies (< (fanin-count aignet) (len copy)) (equal (len new-copy) (len copy)))))
Theorem:
(defthm aignet-copies-ok-of-fraig-sweep (b* (((mv ?new-aignet2 ?new-copy ?new-strash ?new-classes ?new-state) (fraig-sweep aignet aignet2 copy strash classes config state))) (implies (aignet-copies-in-bounds copy aignet2) (aignet-copies-in-bounds new-copy new-aignet2))))
Theorem:
(defthm aignet-copy-is-comb-equivalent-for-non-gates-of-fraig-sweep (b* (((mv ?new-aignet2 ?new-copy ?new-strash ?new-classes ?new-state) (fraig-sweep aignet aignet2 copy strash classes config state))) (implies (and (aignet-copy-is-comb-equivalent-for-non-gates (num-fanins aignet) aignet copy aignet2) (aignet-copies-in-bounds copy aignet2)) (aignet-copy-is-comb-equivalent-for-non-gates (+ 1 (fanin-count aignet)) aignet new-copy new-aignet2))))
Theorem:
(defthm aignet-copy-is-comb-equivalent-of-fraig-sweep (b* (((mv ?new-aignet2 ?new-copy ?new-strash ?new-classes ?new-state) (fraig-sweep aignet aignet2 copy strash classes config state))) (implies (and (aignet-copy-is-comb-equivalent-for-non-gates (num-fanins aignet) aignet copy aignet2) (aignet-copies-in-bounds copy aignet2)) (aignet-copy-is-comb-equivalent (+ 1 (fanin-count aignet)) aignet new-copy new-aignet2))))
Theorem:
(defthm w-state-of-fraig-sweep (b* (((mv ?new-aignet2 ?new-copy ?new-strash ?new-classes ?new-state) (fraig-sweep aignet aignet2 copy strash classes config state))) (equal (w new-state) (w state))))
Theorem:
(defthm fraig-sweep-of-fraig-config-fix-config (equal (fraig-sweep aignet aignet2 copy strash classes (fraig-config-fix config) state) (fraig-sweep aignet aignet2 copy strash classes config state)))
Theorem:
(defthm fraig-sweep-fraig-config-equiv-congruence-on-config (implies (fraig-config-equiv config config-equiv) (equal (fraig-sweep aignet aignet2 copy strash classes config state) (fraig-sweep aignet aignet2 copy strash classes config-equiv state))) :rule-classes :congruence)