		Search-engine friendly clone of the ACL2 documentation.

Symbolic-test-vectors

Stv-out->width

Get the bit-length for a particular output simulation variable.

Signature
(stv-out->width x stv) → width
Arguments: x — Guard (symbolp x).; stv — Guard (processed-stv-p stv).
Returns: width — Type (natp width).

For instance, if you have an STV output line like:

("main_result"  _ _ _ res1 _ res2 _ _)

Then (stv-out->width 'res1 stv) will return the width of main_result, say 64.

If x isn't one of the STV's outputs, we cause a runtime error and logically return 0.

Definitions and Theorems

Function: stv-out->width

(defun stv-out->width (x stv)
  (declare (xargs :guard (and (symbolp x)
                              (processed-stv-p stv))))
  (let ((__function__ 'stv-out->width))
    (declare (ignorable __function__))
    (b* (((processed-stv stv) stv)
         ((compiled-stv cstv) stv.compiled-stv)
         (look (hons-assoc-equal x cstv.out-usersyms))
         ((unless look)
          (raise "Unknown output: ~x0~%" x)
          0))
      (len (cdr look)))))

Theorem: natp-of-stv-out->width

(defthm natp-of-stv-out->width
  (b* ((width (stv-out->width x stv)))
    (natp width))
  :rule-classes :type-prescription)