		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

Svexlist/env-list-vars-for-symbolic-eval

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

Definitions and Theorems

Function: svexlist/env-list-vars-for-symbolic-eval

(defun svexlist/env-list-vars-for-symbolic-eval
       (x envs symbolic-params)
 (declare (xargs :guard (and (svexlist-p x)
                             (svex-envlist-p envs)
                             (alistp symbolic-params))))
 (let ((__function__ 'svexlist/env-list-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 (svex-envlist-keyset envs)))
   (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/env-list-vars-for-symbolic-eval

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

Theorem: svexlist/env-list-vars-for-symbolic-eval-sufficient

(defthm svexlist/env-list-vars-for-symbolic-eval-sufficient
  (b* ((?vars (svexlist/env-list-vars-for-symbolic-eval
                   x envs symbolic-params)))
    (subsetp (intersection-equal (svexlist-vars x)
                                 (svex-envlist-keyset envs))
             vars)))

Theorem: svexlist/env-list-vars-for-symbolic-eval-of-svexlist-fix-x

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

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

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

Theorem: svexlist/env-list-vars-for-symbolic-eval-of-svex-envlist-fix-envs

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

Theorem: svexlist/env-list-vars-for-symbolic-eval-svex-envlist-equiv-congruence-on-envs

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