• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
      • Ipasir
      • Aignet
        • Base-api
        • Aignet-construction
        • Representation
        • Aignet-copy-init
        • Aignet-simplify-marked-with-tracking
        • Aignet-cnf
        • Aignet-simplify-with-tracking
        • Aignet-complete-copy
        • Aignet-eval
          • Vector-simulation
            • Aignet-vecsim
            • Aignet-vecsim1
            • S32v
              • S32v-set2
              • S32v-resize-rows
              • S32v-resize-cols
              • S32v-get2
              • S32v-nrows
              • S32v-ncols
            • Exhaustive-sim
            • S32v-randomize-regs
            • S32v-randomize-inputs
            • Aignet-vecsim-top
        • Semantics
        • Aignet-transforms
        • Aignet-simplify-marked
        • Aignet-read-aiger
        • Aignet-write-aiger
        • Aignet-abc-interface
        • Utilities
      • Aig
      • Satlink
      • Truth
      • Ubdds
      • Bdd
      • Faig
      • Bed
      • 4v
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Testing-utilities
    • Math
  • 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.