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