		Search-engine friendly clone of the ACL2 documentation.

Stv-process

Stv-fully-general-in-alists

Create the sexpr-alists to use as the inputs for each phase of fully general simulations of a module.

Signature
(stv-fully-general-in-alists n mod) → in-alists
Arguments: n — The number of phases to simulate.
Guard (posp n).; mod — The esim module.
Returns: in-alists — Type (cons-list-listp in-alists).

This is basically name mangling. For instance, at phase 5 the input |foo[3]| will be represented by the variable |foo[3].P5|. There can't be any name clashes since we're adding a such a suffix to every signal.

Definitions and Theorems

Function: stv-fully-general-in-alists

(defun
 stv-fully-general-in-alists (n mod)
 (declare (xargs :guard (posp n)))
 (let
    ((__function__ 'stv-fully-general-in-alists))
    (declare (ignorable __function__))
    (b* ((ins (gpl :i mod))
         (flat-ins (pat-flatten1 ins))
         ((when (mbe :logic (not (posp n)) :exec nil))
          nil)
         ((unless (symbol-listp flat-ins))
          (raise "Expected :i for ~x0 to be a symbol pattern."
                 (gpl :n mod))
          (ec-call (stv-fully-general-in-alists-aux (- n 1)
                                                    flat-ins nil))))
        (stv-fully-general-in-alists-aux (- n 1)
                                         flat-ins nil))))

Theorem: cons-list-listp-of-stv-fully-general-in-alists

(defthm cons-list-listp-of-stv-fully-general-in-alists
        (b* ((in-alists (stv-fully-general-in-alists n mod)))
            (cons-list-listp in-alists))
        :rule-classes :rewrite)

Theorem: len-stv-fully-general-in-alists

(defthm len-stv-fully-general-in-alists
        (equal (len (stv-fully-general-in-alists n mod))
               (nfix n)))

Subtopics

Stv-fully-general-in-alists-aux
Stv-fully-general-in-alist-n