		Search-engine friendly clone of the ACL2 documentation.

Stv-compile

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