Construct an alist binding fully-general input names (for all phases) to 4v-sexprs derived from the symbolic test vector.
(stv-restrict-alist lines acc) → restrict-alist
We construct an ordinary (slow) alist that binds the input names we are going to use in our fully-general esim simulation to their bindings according to the symbolic test vector. This is a single alist that includes the bindings for the variables at all phases, plus (presumably, via acc) any initial bindings for state bits.
The sexprs in this alist will often be constants (e.g., when natural
The general intent is to make the resulting alist fast, and use it along with 4v-sexpr-restrict to specialize the fully general simulation, effectively "assuming" the STV.
(defun stv-restrict-alist (lines acc) (declare (xargs :guard (true-list-listp lines))) (let ((__function__ 'stv-restrict-alist)) (declare (ignorable __function__)) (b* (((when (atom lines)) acc) (line1 (car lines)) ((cons name entries) line1) ((unless (atom-listp name)) (raise "Name should be a list of E bits, but is ~x0." name)) (acc (stv-restrict-alist-aux name 0 entries acc))) (stv-restrict-alist (cdr lines) acc))))
(defthm alistp-of-stv-restrict-alist (implies (alistp acc) (b* ((restrict-alist (stv-restrict-alist lines acc))) (alistp restrict-alist))) :rule-classes :rewrite)