		Search-engine friendly clone of the ACL2 documentation.

Symbolic-test-vectors

Stv->outs

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

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

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

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

Then the returned list will include res1 and res2.

Definitions and Theorems

Function: stv->outs

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