		Search-engine friendly clone of the ACL2 documentation.

Symbolic-test-vectors

Stv-run-squash-dontcares

Evaluate a symbolic test vector at particular, concrete inputs, and set all inputs and initial states that aren't bound to false.

Signature
(stv-run-squash-dontcares pstv input-alist &key skip quiet) → out-alist
Arguments: pstv — The symbolic test vector to run.
Guard (processed-stv-p pstv).; input-alist — An alist that should typically bind at least some of the input simulation variables to natural numbers, or to the symbol X. Any inputs that aren't mentioned are implicitly bound to X.; skip — Advanced option to avoid computing certain outputs; see below.; quiet — Suppress debugging output. By default, stv-run will print certain debugging information. This is generally convenient in def-gl-thm forms involving an stv-run, and will allow you to see nicely-formatted debugging info when counter-examples are found. But you can use :quiet t to suppress it.
Returns: out-alist — Alist binding user-level STV outputs to either natural numbers or X.

See stv-run. The only difference between stv-run and this function is that this function uses 4v-sexpr-eval-default instead of 4v-sexpr-eval, which means that any variables not bound by the user-provided inputs are set to false, instead of (effectively) X.

Definitions and Theorems

Function: stv-run-squash-dontcares-fn

(defun stv-run-squash-dontcares-fn (pstv input-alist skip quiet)
 (declare (xargs :guard (processed-stv-p pstv)))
 (let ((__function__ 'stv-run-squash-dontcares))
  (declare (ignorable __function__))
  (time$
   (b*
    (((mv sigs out-usersyms)
      (stv-run-collect-eval-signals pstv skip))
     (- (or quiet
            (cw "STV Raw Inputs: ~x0.~%" input-alist)))
     (ev-alist (stv-run-make-eval-env pstv input-alist))
     ((with-fast ev-alist))
     (evaled-out-bits
         (time$ (make-fast-alist
                     (4v-sexpr-eval-default-alist sigs ev-alist 'f))
                :mintime 1/2
                :msg "; stv-run out-bits: ~st sec, ~sa bytes.~%"))
     (- (fast-alist-free ev-alist))
     (assembled-outs
       (time$
            (stv-assemble-output-alist evaled-out-bits out-usersyms)
            :mintime 1/2
            :msg "; stv-run outs: ~st sec, ~sa bytes.~%"))
     (- (fast-alist-free evaled-out-bits))
     (- (or quiet
            (progn$ (cw "~%STV Inputs:~%")
                    (stv-print-alist input-alist)
                    (cw "~%STV Outputs:~%")
                    (stv-print-alist assembled-outs)
                    (cw "~%")))))
    assembled-outs)
   :msg "; stv-run-squash-dontcares: ~st sec, ~sa bytes.~%"
   :mintime 1)))