		Search-engine friendly clone of the ACL2 documentation.

Fraig

S32v-copy-cares

Signature
(s32v-copy-cares col in-row out-row packed-vals packed-relevants s32v) → new-s32v
Arguments: col — Guard (natp col).; in-row — Guard (natp in-row).; out-row — Guard (natp out-row).

Definitions and Theorems

Function: s32v-copy-cares

(defun s32v-copy-cares (col in-row out-row
                            packed-vals packed-relevants s32v)
  (declare (xargs :stobjs (packed-vals packed-relevants s32v)))
  (declare (xargs :guard (and (natp col)
                              (natp in-row)
                              (natp out-row))))
  (declare
       (xargs :guard (and (<= (s32v-ncols s32v)
                              (s32v-ncols packed-vals))
                          (<= (s32v-ncols s32v)
                              (s32v-ncols packed-relevants))
                          (<= col (s32v-ncols s32v))
                          (< in-row (s32v-nrows packed-vals))
                          (< in-row (s32v-nrows packed-relevants))
                          (< out-row (s32v-nrows s32v)))))
  (let ((__function__ 's32v-copy-cares))
    (declare (ignorable __function__))
    (b* (((when (mbe :logic (zp (- (s32v-ncols s32v) (nfix col)))
                     :exec (eql col (s32v-ncols s32v))))
          s32v)
         (in-data (s32v-get2 in-row col packed-vals))
         (in-mask (s32v-get2 in-row col packed-relevants))
         (out-data (s32v-get2 out-row col s32v))
         (new-data (logior (logand in-mask in-data)
                           (logand (lognot in-mask) out-data)))
         (s32v (s32v-set2 out-row col new-data s32v)))
      (s32v-copy-cares (1+ (lnfix col))
                       in-row out-row
                       packed-vals packed-relevants s32v))))

Theorem: nrows-of-s32v-copy-cares

(defthm nrows-of-s32v-copy-cares
  (b*
   ((?new-s32v (s32v-copy-cares col in-row out-row
                                packed-vals packed-relevants s32v)))
   (implies (< (nfix out-row)
               (len (stobjs::2darr->rows s32v)))
            (equal (len (stobjs::2darr->rows new-s32v))
                   (len (stobjs::2darr->rows s32v))))))

Theorem: ncols-of-s32v-copy-cares

(defthm ncols-of-s32v-copy-cares
  (b*
   ((?new-s32v (s32v-copy-cares col in-row out-row
                                packed-vals packed-relevants s32v)))
   (implies (<= (nfix col)
                (stobjs::2darr->ncols s32v))
            (equal (stobjs::2darr->ncols new-s32v)
                   (stobjs::2darr->ncols s32v)))))

Theorem: s32v-copy-cares-of-nfix-col

(defthm s32v-copy-cares-of-nfix-col
  (equal (s32v-copy-cares (nfix col)
                          in-row out-row
                          packed-vals packed-relevants s32v)
         (s32v-copy-cares col in-row out-row
                          packed-vals packed-relevants s32v)))

Theorem: s32v-copy-cares-nat-equiv-congruence-on-col

(defthm s32v-copy-cares-nat-equiv-congruence-on-col
  (implies
       (nat-equiv col col-equiv)
       (equal (s32v-copy-cares col in-row out-row
                               packed-vals packed-relevants s32v)
              (s32v-copy-cares col-equiv in-row out-row
                               packed-vals packed-relevants s32v)))
  :rule-classes :congruence)

Theorem: s32v-copy-cares-of-nfix-in-row

(defthm s32v-copy-cares-of-nfix-in-row
  (equal (s32v-copy-cares col (nfix in-row)
                          out-row
                          packed-vals packed-relevants s32v)
         (s32v-copy-cares col in-row out-row
                          packed-vals packed-relevants s32v)))

Theorem: s32v-copy-cares-nat-equiv-congruence-on-in-row

(defthm s32v-copy-cares-nat-equiv-congruence-on-in-row
  (implies
       (nat-equiv in-row in-row-equiv)
       (equal (s32v-copy-cares col in-row out-row
                               packed-vals packed-relevants s32v)
              (s32v-copy-cares col in-row-equiv out-row
                               packed-vals packed-relevants s32v)))
  :rule-classes :congruence)

Theorem: s32v-copy-cares-of-nfix-out-row

(defthm s32v-copy-cares-of-nfix-out-row
  (equal (s32v-copy-cares col in-row (nfix out-row)
                          packed-vals packed-relevants s32v)
         (s32v-copy-cares col in-row out-row
                          packed-vals packed-relevants s32v)))

Theorem: s32v-copy-cares-nat-equiv-congruence-on-out-row

(defthm s32v-copy-cares-nat-equiv-congruence-on-out-row
  (implies
       (nat-equiv out-row out-row-equiv)
       (equal (s32v-copy-cares col in-row out-row
                               packed-vals packed-relevants s32v)
              (s32v-copy-cares col in-row out-row-equiv
                               packed-vals packed-relevants s32v)))
  :rule-classes :congruence)