		Search-engine friendly clone of the ACL2 documentation.

Vector-simulation

S32v

Stobj containing a 2-dimensional array of 32-bit signed integers. Used to store the data for vector-simulation.

This is a two dimensional abstract stobj array, introduced by def-2d-arr.

Definition: s32v

(defabsstobj s32v
  :foundation s32ve-arr2
  :recognizer (s32vp :logic s32vl-arr2-wfp
                     :exec s32ve-arr2p)
  :creator (create-s32v :logic create-s32vl-arr2
                        :exec create-s32ve-arr2)
  :corr-fn s32v-corr
  :exports ((s32v-nrows :logic s32vl-nrows
                        :exec s32ve-nrows)
            (s32v-ncols :logic s32vl-ncols
                        :exec s32ve-ncols)
            (s32v-get2 :logic s32vl-get2
                       :exec s32ve-get2$inline)
            (s32v-get :logic s32vl-get
                      :exec s32ve-get$inline)
            (s32v-set2$g :logic s32vl-set2
                         :exec s32ve-set2$inline)
            (s32v-set$g :logic s32vl-set
                        :exec s32ve-set$inline)
            (s32v-resize-rows$g :logic s32vl-resize-rows
                                :exec s32ve-resize-rows$inline
                                :protect t)
            (s32v-resize-cols$g :logic s32vl-resize-cols
                                :exec s32ve-resize-cols$inline
                                :protect t)))

Definition: s32v

(defabsstobj s32v
  :foundation s32ve-arr2
  :recognizer (s32vp :logic s32vl-arr2-wfp
                     :exec s32ve-arr2p)
  :creator (create-s32v :logic create-s32vl-arr2
                        :exec create-s32ve-arr2)
  :corr-fn s32v-corr
  :exports ((s32v-nrows :logic s32vl-nrows
                        :exec s32ve-nrows)
            (s32v-ncols :logic s32vl-ncols
                        :exec s32ve-ncols)
            (s32v-get2 :logic s32vl-get2
                       :exec s32ve-get2$inline)
            (s32v-get :logic s32vl-get
                      :exec s32ve-get$inline)
            (s32v-set2$g :logic s32vl-set2
                         :exec s32ve-set2$inline)
            (s32v-set$g :logic s32vl-set
                        :exec s32ve-set$inline)
            (s32v-resize-rows$g :logic s32vl-resize-rows
                                :exec s32ve-resize-rows$inline
                                :protect t)
            (s32v-resize-cols$g :logic s32vl-resize-cols
                                :exec s32ve-resize-cols$inline
                                :protect t)))

Subtopics

S32v-set2: Set the element at arr[row][col] in the s32v array to some new value.
S32v-resize-rows: Change the number of rows in the s32v, preserving data.
S32v-resize-cols: Change the number of columns in the s32v, deleting data.
S32v-get2: Get the element at arr[row][col] from the s32v array.
S32v-nrows: Get the number of rows in the s32v array.
S32v-ncols: Get the number of columns in the s32v array.