		Search-engine friendly clone of the ACL2 documentation.

Debug.lisp

Svtv-debug-lhs-eval

Signature
(svtv-debug-lhs-eval x bound wirevals vcd-vals) → xval
Arguments: x — Guard (lhs-p x).; bound — Guard (natp bound).; wirevals — Guard (svex-env-p wirevals).
Returns: xval — Type (4vec-p xval).

Definitions and Theorems

Function: svtv-debug-lhs-eval

(defun svtv-debug-lhs-eval (x bound wirevals vcd-vals)
  (declare (xargs :stobjs (vcd-vals)))
  (declare (xargs :guard (and (lhs-p x)
                              (natp bound)
                              (svex-env-p wirevals))))
  (declare (xargs :guard (< bound (4vecs-length vcd-vals))))
  (let ((__function__ 'svtv-debug-lhs-eval))
    (declare (ignorable __function__))
    (b* (((mv xf xr) (lhs-decomp x))
         ((unless xf) (4vec-z))
         ((lhrange xf) xf)
         (rest (svtv-debug-lhs-eval xr bound wirevals vcd-vals))
         ((when (eq (lhatom-kind xf.atom) :z))
          (4vec-concat (2vec xf.w) (4vec-z) rest))
         ((lhatom-var xf) xf.atom)
         (idx (and (svar-indexedp xf.name)
                   (svar-index xf.name)))
         (val (if (and idx (< idx (lnfix bound)))
                  (get-4vec idx vcd-vals)
                (svex-env-fastlookup xf.name wirevals))))
      (4vec-concat (2vec xf.w)
                   (4vec-rsh (2vec xf.rsh) val)
                   rest))))

Theorem: 4vec-p-of-svtv-debug-lhs-eval

(defthm 4vec-p-of-svtv-debug-lhs-eval
  (b* ((xval (svtv-debug-lhs-eval x bound wirevals vcd-vals)))
    (4vec-p xval))
  :rule-classes :rewrite)

Theorem: svtv-debug-lhs-eval-of-lhs-fix-x

(defthm svtv-debug-lhs-eval-of-lhs-fix-x
  (equal (svtv-debug-lhs-eval (lhs-fix x)
                              bound wirevals vcd-vals)
         (svtv-debug-lhs-eval x bound wirevals vcd-vals)))

Theorem: svtv-debug-lhs-eval-lhs-equiv-congruence-on-x

(defthm svtv-debug-lhs-eval-lhs-equiv-congruence-on-x
 (implies
      (lhs-equiv x x-equiv)
      (equal (svtv-debug-lhs-eval x bound wirevals vcd-vals)
             (svtv-debug-lhs-eval x-equiv bound wirevals vcd-vals)))
 :rule-classes :congruence)

Theorem: svtv-debug-lhs-eval-of-nfix-bound

(defthm svtv-debug-lhs-eval-of-nfix-bound
  (equal (svtv-debug-lhs-eval x (nfix bound)
                              wirevals vcd-vals)
         (svtv-debug-lhs-eval x bound wirevals vcd-vals)))

Theorem: svtv-debug-lhs-eval-nat-equiv-congruence-on-bound

(defthm svtv-debug-lhs-eval-nat-equiv-congruence-on-bound
 (implies
      (nat-equiv bound bound-equiv)
      (equal (svtv-debug-lhs-eval x bound wirevals vcd-vals)
             (svtv-debug-lhs-eval x bound-equiv wirevals vcd-vals)))
 :rule-classes :congruence)

Theorem: svtv-debug-lhs-eval-of-svex-env-fix-wirevals

(defthm svtv-debug-lhs-eval-of-svex-env-fix-wirevals
  (equal (svtv-debug-lhs-eval x bound (svex-env-fix wirevals)
                              vcd-vals)
         (svtv-debug-lhs-eval x bound wirevals vcd-vals)))

Theorem: svtv-debug-lhs-eval-svex-env-equiv-congruence-on-wirevals

(defthm svtv-debug-lhs-eval-svex-env-equiv-congruence-on-wirevals
 (implies
      (svex-env-equiv wirevals wirevals-equiv)
      (equal (svtv-debug-lhs-eval x bound wirevals vcd-vals)
             (svtv-debug-lhs-eval x bound wirevals-equiv vcd-vals)))
 :rule-classes :congruence)