		Search-engine friendly clone of the ACL2 documentation.

Fraig

Fraig-ctrexes-resim

Signature
(fraig-ctrexes-resim aignet fraig-ctrexes classes fraig-stats state) → (mv new-classes new-fraig-ctrexes new-fraig-stats new-state)

Definitions and Theorems

Function: fraig-ctrexes-resim

(defun fraig-ctrexes-resim
       (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))
   (declare (ignorable __function__))
   (b* (((mv classes fraig-ctrexes fraig-stats state)
         (fraig-ctrexes-resim-aux aignet fraig-ctrexes
                                  classes fraig-stats state))
        (fraig-ctrexes (fraig-ctrexes-reinit fraig-ctrexes)))
     (mv classes
         fraig-ctrexes fraig-stats state))))

Theorem: classes-wellformed-of-fraig-ctrexes-resim

(defthm classes-wellformed-of-fraig-ctrexes-resim
  (b* (((mv ?new-classes ?new-fraig-ctrexes
            ?new-fraig-stats ?new-state)
        (fraig-ctrexes-resim aignet fraig-ctrexes
                             classes fraig-stats state)))
    (implies (classes-wellformed classes)
             (classes-wellformed new-classes))))

Theorem: classes-size-of-fraig-ctrexes-resim

(defthm classes-size-of-fraig-ctrexes-resim
  (b* (((mv ?new-classes ?new-fraig-ctrexes
            ?new-fraig-stats ?new-state)
        (fraig-ctrexes-resim aignet fraig-ctrexes
                             classes fraig-stats state)))
    (equal (classes-size new-classes)
           (classes-size classes))))

Theorem: fraig-ctrexes-ok-of-fraig-ctrexes-resim

(defthm fraig-ctrexes-ok-of-fraig-ctrexes-resim
  (b* (((mv ?new-classes ?new-fraig-ctrexes
            ?new-fraig-stats ?new-state)
        (fraig-ctrexes-resim 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-resim

(defthm fraig-ctrex-data-rows-of-fraig-ctrexes-resim
  (b* (((mv ?new-classes ?new-fraig-ctrexes
            ?new-fraig-stats ?new-state)
        (fraig-ctrexes-resim 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-resim

(defthm fraig-ctrex-in/reg-rows-of-fraig-ctrexes-resim
  (b* (((mv ?new-classes ?new-fraig-ctrexes
            ?new-fraig-stats ?new-state)
        (fraig-ctrexes-resim 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-resim

(defthm fraig-ctrex-ncols-of-fraig-ctrexes-resim
  (b* (((mv ?new-classes ?new-fraig-ctrexes
            ?new-fraig-stats ?new-state)
        (fraig-ctrexes-resim 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-resim

(defthm fraig-ctrex-nbits-of-fraig-ctrexes-resim
  (b* (((mv ?new-classes ?new-fraig-ctrexes
            ?new-fraig-stats ?new-state)
        (fraig-ctrexes-resim aignet fraig-ctrexes
                             classes fraig-stats state)))
    (equal (nth *fraig-ctrex-nbits* new-fraig-ctrexes)
           0)))

Theorem: w-state-of-fraig-ctrexes-resim

(defthm w-state-of-fraig-ctrexes-resim
  (b* (((mv ?new-classes ?new-fraig-ctrexes
            ?new-fraig-stats ?new-state)
        (fraig-ctrexes-resim aignet fraig-ctrexes
                             classes fraig-stats state)))
    (equal (w new-state) (w state))))