		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

Svexlist-vars-for-symbolic-eval

Signature
(svexlist-vars-for-symbolic-eval x env symbolic-params) → vars
Arguments: x — Guard (svexlist-p x).; env — Guard (svex-env-p env).; symbolic-params — Guard (alistp symbolic-params).
Returns: vars — Type (svarlist-p vars).

Definitions and Theorems

Function: svexlist-vars-for-symbolic-eval

(defun svexlist-vars-for-symbolic-eval (x env symbolic-params)
 (declare (xargs :guard (and (svexlist-p x)
                             (svex-env-p env)
                             (alistp symbolic-params))))
 (let ((__function__ 'svexlist-vars-for-symbolic-eval))
  (declare (ignorable __function__))
  (b*
   ((allvars (assoc :allvars symbolic-params))
    (vars
     (if allvars (svexlist-vars-memo x)
      (ec-call (svarlist-fix (cdr (assoc :vars symbolic-params))))))
    (svars (mbe :logic (mergesort vars)
                :exec (if (setp vars) vars (mergesort vars))))
    ((when allvars) (hons-copy svars))
    (keys (svarlist-filter (alist-keys env)))
    (keys (mbe :logic (mergesort keys)
               :exec
               (if (setp keys)
                   keys
                 (mergesort keys)))))
   (hons-copy (mbe :logic (union keys svars)
                   :exec
                   (if (subset keys svars)
                       svars
                     (if (eq svars nil)
                         keys
                       (union keys svars))))))))

Theorem: svarlist-p-of-svexlist-vars-for-symbolic-eval

(defthm svarlist-p-of-svexlist-vars-for-symbolic-eval
  (b*
    ((vars (svexlist-vars-for-symbolic-eval x env symbolic-params)))
    (svarlist-p vars))
  :rule-classes :rewrite)

Theorem: svexlist-vars-for-symbolic-eval-sufficient

(defthm svexlist-vars-for-symbolic-eval-sufficient
  (b*
   ((?vars (svexlist-vars-for-symbolic-eval x env symbolic-params)))
   (subsetp (intersection-equal (svexlist-vars x)
                                (alist-keys (svex-env-fix env)))
            vars)))

Theorem: member-of-svexlist-vars-for-symbolic-eval

(defthm member-of-svexlist-vars-for-symbolic-eval
  (b*
   ((?vars (svexlist-vars-for-symbolic-eval x env symbolic-params)))
   (implies (and (member v (svexlist-vars x))
                 (hons-assoc-equal v (svex-env-fix env)))
            (member v vars))))

Theorem: svexlist-vars-for-symbolic-eval-of-svexlist-fix-x

(defthm svexlist-vars-for-symbolic-eval-of-svexlist-fix-x
  (equal (svexlist-vars-for-symbolic-eval (svexlist-fix x)
                                          env symbolic-params)
         (svexlist-vars-for-symbolic-eval x env symbolic-params)))

Theorem: svexlist-vars-for-symbolic-eval-svexlist-equiv-congruence-on-x

(defthm
     svexlist-vars-for-symbolic-eval-svexlist-equiv-congruence-on-x
 (implies
  (svexlist-equiv x x-equiv)
  (equal
     (svexlist-vars-for-symbolic-eval x env symbolic-params)
     (svexlist-vars-for-symbolic-eval x-equiv env symbolic-params)))
 :rule-classes :congruence)

Theorem: svexlist-vars-for-symbolic-eval-of-svex-env-fix-env

(defthm svexlist-vars-for-symbolic-eval-of-svex-env-fix-env
  (equal (svexlist-vars-for-symbolic-eval x (svex-env-fix env)
                                          symbolic-params)
         (svexlist-vars-for-symbolic-eval x env symbolic-params)))

Theorem: svexlist-vars-for-symbolic-eval-svex-env-equiv-congruence-on-env

(defthm
   svexlist-vars-for-symbolic-eval-svex-env-equiv-congruence-on-env
 (implies
  (svex-env-equiv env env-equiv)
  (equal
     (svexlist-vars-for-symbolic-eval x env symbolic-params)
     (svexlist-vars-for-symbolic-eval x env-equiv symbolic-params)))
 :rule-classes :congruence)