		Search-engine friendly clone of the ACL2 documentation.

Stv-process

Stv-run-esim-debug

Signature
(stv-run-esim-debug mod in-alists state-alists initial-state) → (mv nsts outs ints)
Arguments: mod — The module to run.
Guard (and (good-esim-modulep mod) (new-good-esim-probe-modulep mod)).; in-alists — A list of N alists, to be used at each phase.; state-alists — A list of N alists, to override particular state bits.; initial-state — Initial state to use.
Returns: nsts — A list of next-state alists.; outs — A list of outputs alists.; ints — A list of internals alists.

Definitions and Theorems

Function: stv-run-esim-debug

(defun
    stv-run-esim-debug
    (mod in-alists state-alists initial-state)
    (declare (xargs :guard (and (good-esim-modulep mod)
                                (new-good-esim-probe-modulep mod))))
    (declare (xargs :guard (eql (len in-alists)
                                (len state-alists))))
    (let ((__function__ 'stv-run-esim-debug))
         (declare (ignorable __function__))
         (b* (((when (atom in-alists))
               (mv nil nil nil))
              (state-alist (append-without-guard (car state-alists)
                                                 initial-state))
              ((mv nst1 out1 int1)
               (esim-sexpr-simp-new-probe mod (car in-alists)
                                          state-alist))
              ((mv nst-rest out-rest int-rest)
               (stv-run-esim-debug mod (cdr in-alists)
                                   (cdr state-alists)
                                   nst1)))
             (mv (cons nst1 nst-rest)
                 (cons out1 out-rest)
                 (cons int1 int-rest)))))

Theorem: len-of-stv-run-esim-debug-0

(defthm
 len-of-stv-run-esim-debug-0
 (equal
  (len
      (mv-nth 0
              (stv-run-esim-debug mod ins st-overrides initial-st)))
  (len ins)))

Theorem: len-of-stv-run-esim-debug-1

(defthm
 len-of-stv-run-esim-debug-1
 (equal
  (len
      (mv-nth 1
              (stv-run-esim-debug mod ins st-overrides initial-st)))
  (len ins)))

Theorem: len-of-stv-run-esim-debug-2

(defthm
 len-of-stv-run-esim-debug-2
 (equal
  (len
      (mv-nth 2
              (stv-run-esim-debug mod ins st-overrides initial-st)))
  (len ins)))