(stv-fully-general-simulation-run n mod override-stbits) → (mv init-st in-alists nst-alists out-alists nil)
This is a fully general simulation, so the nst/out-alists bind signal names to 4v-sexprs in terms of the variables in the init-st and in-alists.
See also stv-fully-general-simulation-debug, which produces the same outputs but also captures the internal signals after each phase.
We memoize this function so that if we're reusing an STV, we can just reuse the same general simulation repeatedly. BOZO maybe we should be memoizing the individual steps instead of the whole run, to get more cross-stv sharing.
(defun stv-fully-general-simulation-run (n mod override-stbits) (declare (xargs :guard (and (posp n) (symbol-listp override-stbits)))) (let ((__function__ 'stv-fully-general-simulation-run)) (declare (ignorable __function__)) (b* ((in-alists (stv-fully-general-in-alists n mod)) (init-st-alist (stv-fully-general-st-alist mod)) (override-alists (stv-fully-general-in-alists-aux (- n 1) override-stbits nil)) ((mv nsts outs) (ec-call (stv-run-esim mod in-alists override-alists init-st-alist)))) (mv init-st-alist in-alists nsts outs nil))))