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

    S32v-nrows

    Get the number of rows in the s32v array.

    Logical definition:

    Function: s32vl-nrows

    (defun s32vl-nrows (s32vl-arr2)
      (declare (xargs :guard (s32vl-arr2-wfp s32vl-arr2)))
      (len (stobjs::2darr->rows s32vl-arr2)))