(fraig-ctrexes-maybe-resim node config aignet fraig-ctrexes classes fraig-stats state) → (mv forced-last-chancep new-classes new-fraig-ctrexes new-fraig-stats new-state)
Function:
(defun fraig-ctrexes-maybe-resim (node config aignet fraig-ctrexes classes fraig-stats state) (declare (xargs :stobjs (aignet fraig-ctrexes classes fraig-stats state))) (declare (xargs :guard (and (natp node) (fraig-config-p config)))) (declare (xargs :guard (and (id-existsp node aignet) (classes-wellformed classes) (fraig-ctrexes-ok fraig-ctrexes) (equal (fraig-ctrex-data-rows fraig-ctrexes) (classes-size classes)) (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-maybe-resim)) (declare (ignorable __function__)) (b* (((fraig-config config)) (head (node-head node classes)) (force-resim (and config.ctrex-force-resim (b* (((acl2::stobj-get force-resim) ((bitarr (fraig-ctrex-resim-classes fraig-ctrexes))) (eql 1 (get-bit head bitarr)))) force-resim))) ((unless (or (>= (lnfix (fraig-ctrex-nbits fraig-ctrexes)) (* 32 (fraig-ctrex-ncols fraig-ctrexes))) (and config.ctrex-queue-limit (>= (lnfix (fraig-ctrex-count fraig-ctrexes)) config.ctrex-queue-limit)) force-resim)) (mv nil classes fraig-ctrexes fraig-stats state)) ((mv classes fraig-ctrexes fraig-stats state) (fraig-ctrexes-resim aignet fraig-ctrexes classes fraig-stats state)) (fraig-stats (if (eql head (node-head node classes)) fraig-stats (fraig-stats-update-last-chance force-resim fraig-stats)))) (mv (and force-resim (not (eql head (node-head node classes)))) classes fraig-ctrexes fraig-stats state))))
Theorem:
(defthm classes-wellformed-of-fraig-ctrexes-maybe-resim (b* (((mv ?forced-last-chancep ?new-classes ?new-fraig-ctrexes ?new-fraig-stats ?new-state) (fraig-ctrexes-maybe-resim node config aignet fraig-ctrexes classes fraig-stats state))) (implies (classes-wellformed classes) (classes-wellformed new-classes))))
Theorem:
(defthm classes-size-of-fraig-ctrexes-maybe-resim (b* (((mv ?forced-last-chancep ?new-classes ?new-fraig-ctrexes ?new-fraig-stats ?new-state) (fraig-ctrexes-maybe-resim node config aignet fraig-ctrexes classes fraig-stats state))) (equal (classes-size new-classes) (classes-size classes))))
Theorem:
(defthm fraig-ctrexes-ok-of-fraig-ctrexes-maybe-resim (b* (((mv ?forced-last-chancep ?new-classes ?new-fraig-ctrexes ?new-fraig-stats ?new-state) (fraig-ctrexes-maybe-resim node config 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-maybe-resim (b* (((mv ?forced-last-chancep ?new-classes ?new-fraig-ctrexes ?new-fraig-stats ?new-state) (fraig-ctrexes-maybe-resim node config 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-maybe-resim (b* (((mv ?forced-last-chancep ?new-classes ?new-fraig-ctrexes ?new-fraig-stats ?new-state) (fraig-ctrexes-maybe-resim node config 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-maybe-resim (b* (((mv ?forced-last-chancep ?new-classes ?new-fraig-ctrexes ?new-fraig-stats ?new-state) (fraig-ctrexes-maybe-resim node config aignet fraig-ctrexes classes fraig-stats state))) (equal (fraig-ctrex-ncols new-fraig-ctrexes) (fraig-ctrex-ncols fraig-ctrexes))))
Theorem:
(defthm fraig-ctrex-nbits-of-fraig-ctrexes-maybe-resim (b* (((mv ?forced-last-chancep ?new-classes ?new-fraig-ctrexes ?new-fraig-stats ?new-state) (fraig-ctrexes-maybe-resim node config aignet fraig-ctrexes classes fraig-stats state))) (implies (and (<= (nfix (nth *fraig-ctrex-nbits* fraig-ctrexes)) (* 32 (fraig-ctrex-ncols fraig-ctrexes))) (posp (fraig-ctrex-ncols fraig-ctrexes))) (< (nfix (nth *fraig-ctrex-nbits* new-fraig-ctrexes)) (* 32 (fraig-ctrex-ncols fraig-ctrexes))))) :rule-classes :linear)
Theorem:
(defthm w-state-of-fraig-ctrexes-maybe-resim (b* (((mv ?forced-last-chancep ?new-classes ?new-fraig-ctrexes ?new-fraig-stats ?new-state) (fraig-ctrexes-maybe-resim node config aignet fraig-ctrexes classes fraig-stats state))) (equal (w new-state) (w state))))
Theorem:
(defthm fraig-ctrexes-maybe-resim-of-nfix-node (equal (fraig-ctrexes-maybe-resim (nfix node) config aignet fraig-ctrexes classes fraig-stats state) (fraig-ctrexes-maybe-resim node config aignet fraig-ctrexes classes fraig-stats state)))
Theorem:
(defthm fraig-ctrexes-maybe-resim-nat-equiv-congruence-on-node (implies (nat-equiv node node-equiv) (equal (fraig-ctrexes-maybe-resim node config aignet fraig-ctrexes classes fraig-stats state) (fraig-ctrexes-maybe-resim node-equiv config aignet fraig-ctrexes classes fraig-stats state))) :rule-classes :congruence)
Theorem:
(defthm fraig-ctrexes-maybe-resim-of-fraig-config-fix-config (equal (fraig-ctrexes-maybe-resim node (fraig-config-fix config) aignet fraig-ctrexes classes fraig-stats state) (fraig-ctrexes-maybe-resim node config aignet fraig-ctrexes classes fraig-stats state)))
Theorem:
(defthm fraig-ctrexes-maybe-resim-fraig-config-equiv-congruence-on-config (implies (fraig-config-equiv config config-equiv) (equal (fraig-ctrexes-maybe-resim node config aignet fraig-ctrexes classes fraig-stats state) (fraig-ctrexes-maybe-resim node config-equiv aignet fraig-ctrexes classes fraig-stats state))) :rule-classes :congruence)