		Search-engine friendly clone of the ACL2 documentation.

Fraig

Fraig-ctrexes-reinit

Signature
(fraig-ctrexes-reinit fraig-ctrexes) → new-fraig-ctrexes

Definitions and Theorems

Function: fraig-ctrexes-reinit

(defun fraig-ctrexes-reinit (fraig-ctrexes)
  (declare (xargs :stobjs (fraig-ctrexes)))
  (declare (xargs :guard (fraig-ctrexes-ok fraig-ctrexes)))
  (let ((__function__ 'fraig-ctrexes-reinit))
    (declare (ignorable __function__))
    (b* ((fraig-ctrexes (update-fraig-ctrex-nbits 0 fraig-ctrexes))
         (fraig-ctrexes (update-fraig-ctrex-count 0 fraig-ctrexes))
         (data-rows (fraig-ctrex-data-rows fraig-ctrexes))
         ((acl2::stobj-get bitarr)
          ((bitarr (fraig-ctrex-resim-classes fraig-ctrexes)))
          (b* ((bitarr (resize-bits 0 bitarr))
               (bitarr (resize-bits data-rows bitarr)))
            bitarr))
         ((acl2::stobj-get packed-relevants)
          ((packed-relevants
                (fraig-ctrex-in/reg-relevants fraig-ctrexes)))
          (s32v-zero-rows 0 packed-relevants)))
      fraig-ctrexes)))

Theorem: fraig-ctrexes-ok-of-fraig-ctrexes-reinit

(defthm fraig-ctrexes-ok-of-fraig-ctrexes-reinit
  (b* ((?new-fraig-ctrexes (fraig-ctrexes-reinit fraig-ctrexes)))
    (implies (fraig-ctrexes-ok fraig-ctrexes)
             (fraig-ctrexes-ok new-fraig-ctrexes))))

Theorem: fraig-ctrex-data-rows-of-fraig-ctrexes-reinit

(defthm fraig-ctrex-data-rows-of-fraig-ctrexes-reinit
  (b* ((?new-fraig-ctrexes (fraig-ctrexes-reinit fraig-ctrexes)))
    (equal (fraig-ctrex-data-rows new-fraig-ctrexes)
           (fraig-ctrex-data-rows fraig-ctrexes))))

Theorem: fraig-ctrex-in/reg-rows-of-fraig-ctrexes-reinit

(defthm fraig-ctrex-in/reg-rows-of-fraig-ctrexes-reinit
  (b* ((?new-fraig-ctrexes (fraig-ctrexes-reinit fraig-ctrexes)))
    (equal (fraig-ctrex-in/reg-rows new-fraig-ctrexes)
           (fraig-ctrex-in/reg-rows fraig-ctrexes))))

Theorem: fraig-ctrex-ncols-of-fraig-ctrexes-reinit

(defthm fraig-ctrex-ncols-of-fraig-ctrexes-reinit
  (b* ((?new-fraig-ctrexes (fraig-ctrexes-reinit fraig-ctrexes)))
    (equal (fraig-ctrex-ncols new-fraig-ctrexes)
           (fraig-ctrex-ncols fraig-ctrexes))))

Theorem: fraig-ctrex-nbits-of-fraig-ctrexes-reinit

(defthm fraig-ctrex-nbits-of-fraig-ctrexes-reinit
  (b* ((?new-fraig-ctrexes (fraig-ctrexes-reinit fraig-ctrexes)))
    (equal (nth *fraig-ctrex-nbits* new-fraig-ctrexes)
           0)))