		Search-engine friendly clone of the ACL2 documentation.

Fraig

Fraig-ctrexes-init

Signature
(fraig-ctrexes-init ncols fraig-ctrexes aignet) → new-fraig-ctrexes
Arguments: ncols — Guard (posp ncols).

Definitions and Theorems

Function: fraig-ctrexes-init

(defun fraig-ctrexes-init (ncols fraig-ctrexes aignet)
 (declare (xargs :stobjs (fraig-ctrexes aignet)))
 (declare (xargs :guard (posp ncols)))
 (let ((__function__ 'fraig-ctrexes-init))
   (declare (ignorable __function__))
   (b*
    ((ncols (lposfix ncols))
     (fraig-ctrexes (update-fraig-ctrex-nbits 0 fraig-ctrexes))
     (fraig-ctrexes (update-fraig-ctrex-count 0 fraig-ctrexes))
     (size (num-fanins aignet))
     ((acl2::stobj-get s32v bitarr)
      ((s32v (fraig-ctrex-data fraig-ctrexes))
       (bitarr (fraig-ctrex-resim-classes fraig-ctrexes)))
      (b* ((bitarr (resize-bits 0 bitarr))
           (bitarr (resize-bits size bitarr))
           (s32v (s32v-resize-rows 0 s32v))
           (s32v (s32v-resize-cols ncols s32v))
           (s32v (s32v-resize-rows size s32v)))
        (mv s32v bitarr)))
     (in/reg-size (+ (num-ins aignet) (num-regs aignet)))
     ((acl2::stobj-get packed-vals packed-relevants)
      ((packed-vals (fraig-ctrex-in/reg-vals fraig-ctrexes))
       (packed-relevants
            (fraig-ctrex-in/reg-relevants fraig-ctrexes)))
      (b*
       ((packed-vals (s32v-resize-rows 0 packed-vals))
        (packed-vals (s32v-resize-cols ncols packed-vals))
        (packed-vals (s32v-resize-rows in/reg-size packed-vals))
        (packed-relevants (s32v-resize-rows 0 packed-relevants))
        (packed-relevants (s32v-resize-cols ncols packed-relevants))
        (packed-relevants
             (s32v-resize-rows in/reg-size packed-relevants)))
       (mv packed-vals packed-relevants))))
    fraig-ctrexes)))

Theorem: fraig-ctrexes-ok-of-fraig-ctrexes-init

(defthm fraig-ctrexes-ok-of-fraig-ctrexes-init
  (b* ((?new-fraig-ctrexes
            (fraig-ctrexes-init ncols fraig-ctrexes aignet)))
    (fraig-ctrexes-ok new-fraig-ctrexes)))

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

(defthm fraig-ctrex-data-rows-of-fraig-ctrexes-init
  (b* ((?new-fraig-ctrexes
            (fraig-ctrexes-init ncols fraig-ctrexes aignet)))
    (equal (fraig-ctrex-data-rows new-fraig-ctrexes)
           (num-fanins aignet))))

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

(defthm fraig-ctrex-in/reg-rows-of-fraig-ctrexes-init
  (b* ((?new-fraig-ctrexes
            (fraig-ctrexes-init ncols fraig-ctrexes aignet)))
    (equal (fraig-ctrex-in/reg-rows new-fraig-ctrexes)
           (+ (num-ins aignet)
              (num-regs aignet)))))

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

(defthm fraig-ctrex-ncols-of-fraig-ctrexes-init
  (b* ((?new-fraig-ctrexes
            (fraig-ctrexes-init ncols fraig-ctrexes aignet)))
    (equal (fraig-ctrex-ncols new-fraig-ctrexes)
           (pos-fix ncols))))

Theorem: fraig-ctrexes-init-of-pos-fix-ncols

(defthm fraig-ctrexes-init-of-pos-fix-ncols
  (equal (fraig-ctrexes-init (pos-fix ncols)
                             fraig-ctrexes aignet)
         (fraig-ctrexes-init ncols fraig-ctrexes aignet)))

Theorem: fraig-ctrexes-init-pos-equiv-congruence-on-ncols

(defthm fraig-ctrexes-init-pos-equiv-congruence-on-ncols
 (implies
      (pos-equiv ncols ncols-equiv)
      (equal (fraig-ctrexes-init ncols fraig-ctrexes aignet)
             (fraig-ctrexes-init ncols-equiv fraig-ctrexes aignet)))
 :rule-classes :congruence)