		Search-engine friendly clone of the ACL2 documentation.

Fraig

Fraig-ctrexes-maybe-resim

Signature
(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)
Arguments: node — Guard (natp node).; config — Guard (fraig-config-p config).; aignet — input aignet.; classes — equiv classes data structure.; fraig-stats — statistics record.

Definitions and Theorems

Function: fraig-ctrexes-maybe-resim

(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: classes-wellformed-of-fraig-ctrexes-maybe-resim

(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: classes-size-of-fraig-ctrexes-maybe-resim

(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: fraig-ctrexes-ok-of-fraig-ctrexes-maybe-resim

(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: fraig-ctrex-data-rows-of-fraig-ctrexes-maybe-resim

(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: fraig-ctrex-in/reg-rows-of-fraig-ctrexes-maybe-resim

(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: fraig-ctrex-ncols-of-fraig-ctrexes-maybe-resim

(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: fraig-ctrex-nbits-of-fraig-ctrexes-maybe-resim

(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: w-state-of-fraig-ctrexes-maybe-resim

(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: fraig-ctrexes-maybe-resim-of-nfix-node

(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: fraig-ctrexes-maybe-resim-nat-equiv-congruence-on-node

(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: fraig-ctrexes-maybe-resim-of-fraig-config-fix-config

(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: fraig-ctrexes-maybe-resim-fraig-config-equiv-congruence-on-config

(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)