		Search-engine friendly clone of the ACL2 documentation.

Symbolic-test-vectors

Stv->ins

Get a list of an STV's input simulation variables.

Signature
(stv->ins x) → inputs
Arguments: x — Guard (processed-stv-p x).
Returns: inputs — Should be a symbol-listp in practice.

We collect simulation variables from all input and initial lines. For instance, if you have an input line like:

("a_bus"  _ _ _ a1 _ a2 _ _)

Then the returned list will include a1 and a2.

Definitions and Theorems

Function: stv->ins

(defun stv->ins (x)
  (declare (xargs :guard (processed-stv-p x)))
  (let ((__function__ 'stv->ins))
    (declare (ignorable __function__))
    (b* (((processed-stv x) x)
         ((compiled-stv cstv) x.compiled-stv))
      (alist-keys cstv.in-usersyms))))