# Stv-restrict-alist

Construct an alist binding fully-general input names (for all phases)
to 4v-sexprs derived from the symbolic test vector.

- Signature
(stv-restrict-alist lines acc) → restrict-alist

- Arguments
`lines` — The output from stv-expand-input-lines. That is, these
should STV input lines that have already been widened, had their
names resolved into E bits, and had their entries turned into
4v-sexpr lists.

Guard (true-list-listp lines).
`acc` — An alist that we extend. Typically it is the alist that has the
:initial bindings.
- Returns
`restrict-alist` — Type (alistp restrict-alist), given (alistp acc).

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
numbers, :ones, x, or ~ values are used), but they can also have
free variables from _ symbols and also simulation variable bits.

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.

### Definitions and Theorems

**Function: **stv-restrict-alist

(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))))

**Theorem: **alistp-of-stv-restrict-alist

(defthm alistp-of-stv-restrict-alist
(implies (alistp acc)
(b* ((restrict-alist (stv-restrict-alist lines acc)))
(alistp restrict-alist)))
:rule-classes :rewrite)

### Subtopics

- Stv-restrict-alist-aux