(fraig-ctrexes-resim-aux aignet fraig-ctrexes classes fraig-stats state) → (mv new-classes new-fraig-ctrexes new-fraig-stats new-state)
Function:
(defun fraig-ctrexes-resim-aux (aignet fraig-ctrexes classes fraig-stats state) (declare (xargs :stobjs (aignet fraig-ctrexes classes fraig-stats state))) (declare (xargs :guard (and (classes-wellformed classes) (fraig-ctrexes-ok fraig-ctrexes) (equal (fraig-ctrex-data-rows fraig-ctrexes) (num-fanins aignet)) (equal (classes-size classes) (num-fanins aignet)) (equal (fraig-ctrex-in/reg-rows fraig-ctrexes) (+ (num-ins aignet) (num-regs aignet)))))) (let ((__function__ 'fraig-ctrexes-resim-aux)) (declare (ignorable __function__)) (b* ((nbits (fraig-ctrex-nbits fraig-ctrexes)) ((acl2::stobj-get packed-vals packed-relevants s32v classes fraig-stats state) ((packed-vals (fraig-ctrex-in/reg-vals fraig-ctrexes)) (packed-relevants (fraig-ctrex-in/reg-relevants fraig-ctrexes)) (s32v (fraig-ctrex-data fraig-ctrexes))) (b* ((packed-relevants (if (eql nbits 0) packed-relevants (s32v-repeat-bitcols nbits 0 packed-relevants))) (packed-vals (if (eql nbits 0) packed-vals (s32v-repeat-bitcols nbits 0 packed-vals))) ((mv packed-vals state) (if (eql 0 (s32v-nrows packed-vals)) (mv packed-vals state) (s32v-add-salt nbits packed-vals packed-relevants state))) ((mv s32v state) (s32v-randomize-inputs 0 s32v aignet state)) ((mv s32v state) (s32v-randomize-regs 0 s32v aignet state)) (s32v (fraig-ctrex-invals->vecsim 0 packed-vals packed-relevants s32v aignet)) (s32v (fraig-ctrex-regvals->vecsim 0 packed-vals packed-relevants s32v aignet)) (s32v (aignet-vecsim-top s32v aignet)) ((mv classes nclass-lits-refined nconst-lits-refined nclasses-refined) (classes-refine s32v classes aignet)) (fraig-stats (update-fraig-class-lits-refined (+ nclass-lits-refined (fraig-class-lits-refined fraig-stats)) fraig-stats)) (fraig-stats (update-fraig-const-lits-refined (+ nconst-lits-refined (fraig-const-lits-refined fraig-stats)) fraig-stats)) (fraig-stats (update-fraig-classes-refined (+ nclasses-refined (fraig-classes-refined fraig-stats)) fraig-stats)) (fraig-stats (update-fraig-resims (+ 1 (fraig-resims fraig-stats)) fraig-stats))) (mv packed-vals packed-relevants s32v classes fraig-stats state)))) (mv classes fraig-ctrexes fraig-stats state))))
Theorem:
(defthm classes-wellformed-of-fraig-ctrexes-resim-aux (b* (((mv ?new-classes ?new-fraig-ctrexes ?new-fraig-stats ?new-state) (fraig-ctrexes-resim-aux aignet fraig-ctrexes classes fraig-stats state))) (implies (classes-wellformed classes) (classes-wellformed new-classes))))
Theorem:
(defthm classes-size-of-fraig-ctrexes-resim-aux (b* (((mv ?new-classes ?new-fraig-ctrexes ?new-fraig-stats ?new-state) (fraig-ctrexes-resim-aux aignet fraig-ctrexes classes fraig-stats state))) (equal (classes-size new-classes) (classes-size classes))))
Theorem:
(defthm fraig-ctrexes-ok-of-fraig-ctrexes-resim-aux (b* (((mv ?new-classes ?new-fraig-ctrexes ?new-fraig-stats ?new-state) (fraig-ctrexes-resim-aux aignet fraig-ctrexes classes fraig-stats state))) (implies (and (fraig-ctrexes-ok fraig-ctrexes) (equal (fraig-ctrex-data-rows fraig-ctrexes) (num-fanins aignet))) (fraig-ctrexes-ok new-fraig-ctrexes))))
Theorem:
(defthm fraig-ctrex-data-rows-of-fraig-ctrexes-resim-aux (b* (((mv ?new-classes ?new-fraig-ctrexes ?new-fraig-stats ?new-state) (fraig-ctrexes-resim-aux aignet fraig-ctrexes classes fraig-stats state))) (implies (equal (fraig-ctrex-data-rows fraig-ctrexes) (num-fanins aignet)) (equal (fraig-ctrex-data-rows new-fraig-ctrexes) (num-fanins aignet)))))
Theorem:
(defthm fraig-ctrex-in/reg-rows-of-fraig-ctrexes-resim-aux (b* (((mv ?new-classes ?new-fraig-ctrexes ?new-fraig-stats ?new-state) (fraig-ctrexes-resim-aux aignet fraig-ctrexes classes fraig-stats state))) (equal (fraig-ctrex-in/reg-rows new-fraig-ctrexes) (fraig-ctrex-in/reg-rows fraig-ctrexes))))
Theorem:
(defthm fraig-ctrex-ncols-of-fraig-ctrexes-resim-aux (b* (((mv ?new-classes ?new-fraig-ctrexes ?new-fraig-stats ?new-state) (fraig-ctrexes-resim-aux aignet fraig-ctrexes classes fraig-stats state))) (equal (fraig-ctrex-ncols new-fraig-ctrexes) (fraig-ctrex-ncols fraig-ctrexes))))
Theorem:
(defthm w-state-of-fraig-ctrexes-resim-aux (b* (((mv ?new-classes ?new-fraig-ctrexes ?new-fraig-stats ?new-state) (fraig-ctrexes-resim-aux aignet fraig-ctrexes classes fraig-stats state))) (equal (w new-state) (w state))))