• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Svex-compilation
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
        • Rewriting
        • Svex
        • Bit-blasting
        • Functions
        • 4vmask
        • Why-infinite-width
        • Svex-vars
        • Evaluation
          • Svex-xeval
          • Svex-mono-eval
            • Svex-alist-mono-eval
              • Svex-alist-mono-eval-aux
            • Svex-mono-eval-monotonicity
            • Svexlist-mono-eval
            • Svex-fn/args-mono-eval
            • Svex-call-mono-eval
          • Svex-eval
          • Svex-apply
          • Svex-env
          • Svex-alist-eval
          • Svar-boolmasks-lookup
          • Svex-s4eval
          • Svexlist-unquote
          • Svex-alist-eval-for-symbolic
          • Svexlist-eval
          • Svexlist-quotesp
          • Svar-boolmasks
          • Svexlist-s4eval
          • Svexlist-eval-for-symbolic
        • Values
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Svex-mono-eval

Svex-alist-mono-eval

Maps svex-mono-eval over an svex alist.

Signature

(svex-alist-mono-eval x env) → result

Arguments

x — Alist of variables to svex expressions to evaluate. Need not be fast.
    Guard (svex-alist-p x).

env — Guard (svex-env-p env).

Returns

result — New (slow) alist, binds the variables to their expressions' values.
    Type (svex-env-p result).

Definitions and Theorems

Function: svex-alist-mono-eval

(defun svex-alist-mono-eval (x env)
 (declare (xargs :guard (and (svex-alist-p x)
                             (svex-env-p env))))
 (let ((__function__ 'svex-alist-mono-eval))
  (declare (ignorable __function__))
  (mbe
     :logic
     (if (atom x)
         nil
       (if (mbt (and (consp (car x)) (svar-p (caar x))))
           (cons (cons (caar x)
                       (svex-mono-eval (cdar x) env))
                 (svex-alist-mono-eval (cdr x) env))
         (svex-alist-mono-eval (cdr x) env)))
     :exec (with-fast-alist env (svex-alist-mono-eval-aux x env)))))

Theorem: svex-env-p-of-svex-alist-mono-eval

(defthm svex-env-p-of-svex-alist-mono-eval
  (b* ((result (svex-alist-mono-eval x env)))
    (svex-env-p result))
  :rule-classes :rewrite)

Theorem: svex-alist-mono-eval-of-svex-alist-fix-x

(defthm svex-alist-mono-eval-of-svex-alist-fix-x
  (equal (svex-alist-mono-eval (svex-alist-fix x)
                               env)
         (svex-alist-mono-eval x env)))

Theorem: svex-alist-mono-eval-svex-alist-equiv-congruence-on-x

(defthm svex-alist-mono-eval-svex-alist-equiv-congruence-on-x
  (implies (svex-alist-equiv x x-equiv)
           (equal (svex-alist-mono-eval x env)
                  (svex-alist-mono-eval x-equiv env)))
  :rule-classes :congruence)

Theorem: svex-alist-mono-eval-of-svex-env-fix-env

(defthm svex-alist-mono-eval-of-svex-env-fix-env
  (equal (svex-alist-mono-eval x (svex-env-fix env))
         (svex-alist-mono-eval x env)))

Theorem: svex-alist-mono-eval-svex-env-equiv-congruence-on-env

(defthm svex-alist-mono-eval-svex-env-equiv-congruence-on-env
  (implies (svex-env-equiv env env-equiv)
           (equal (svex-alist-mono-eval x env)
                  (svex-alist-mono-eval x env-equiv)))
  :rule-classes :congruence)

Theorem: svex-env-lookup-of-svex-alist-mono-eval

(defthm svex-env-lookup-of-svex-alist-mono-eval
  (equal (svex-env-lookup k (svex-alist-mono-eval x env))
         (let ((xk (svex-lookup k x)))
           (if xk (svex-mono-eval xk env)
             (4vec-x)))))

Theorem: svex-env-boundp-of-svex-alist-mono-eval

(defthm svex-env-boundp-of-svex-alist-mono-eval
  (iff (svex-env-boundp k (svex-alist-mono-eval x env))
       (svex-lookup k x)))

Theorem: svex-alist-mono-eval-of-append

(defthm svex-alist-mono-eval-of-append
  (equal (svex-alist-mono-eval (append a b) env)
         (append (svex-alist-mono-eval a env)
                 (svex-alist-mono-eval b env))))

Theorem: alist-keys-of-svex-alist-mono-eval

(defthm alist-keys-of-svex-alist-mono-eval
  (equal (alist-keys (svex-alist-mono-eval x env))
         (svex-alist-keys x)))

Subtopics

Svex-alist-mono-eval-aux