		Search-engine friendly clone of the ACL2 documentation.

Stv-process

Stv-extract-relevant-signals

Pull out the fully general expressions for the signals that we care about, and bind them to the bit names of the simulation variables.

Signature
(stv-extract-relevant-signals extract-alists out-alists acc) → *
Arguments: extract-alists — The stv-extraction-alists we obtained from stv-compile.; out-alists — The list of output alists from the fully general simulation, e.g., from stv-fully-general-simulation-run.; acc — An accumulator to extend, which should initially be nil.

We walk down the extract-alists and out-alists together, extracting the expressions for the signals that we care about at each phase, and naming them with the output simulation variable bit names.

Definitions and Theorems

Function: stv-extract-relevant-signals

(defun stv-extract-relevant-signals (extract-alists out-alists acc)
 (declare (xargs :guard t))
 (let ((__function__ 'stv-extract-relevant-signals))
  (declare (ignorable __function__))
  (b* (((when (and (atom extract-alists)
                   (atom out-alists)))
        acc)
       ((when (or (atom extract-alists)
                  (atom out-alists)))
        (raise "Should have as many extract alists as out-alists."))
       (extr1 (car extract-alists))
       (outs1 (car out-alists))
       ((when (not extr1))
        (stv-extract-relevant-signals (cdr extract-alists)
                                      (cdr out-alists)
                                      acc))
       (user-bits (alist-vals extr1))
       (want-names (alist-keys extr1))
       (outs1 (make-fast-alist outs1))
       (want-exprs (vl2014::look-up-each-fast want-names outs1))
       (- (fast-alist-free outs1))
       (acc (safe-pairlis-onto-acc user-bits want-exprs acc)))
    (stv-extract-relevant-signals (cdr extract-alists)
                                  (cdr out-alists)
                                  acc))))