		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svstate-vars

Signature
(svstate-vars st) → vars
Arguments: st — Guard (svstate-p st).
Returns: vars — Type (and (svarlist-p vars) (setp vars)).

Definitions and Theorems

Function: svstate-vars

(defun svstate-vars (st)
  (declare (xargs :guard (svstate-p st)))
  (let ((__function__ 'svstate-vars))
    (declare (ignorable __function__))
    (b* (((svstate st))
         (blkst-alist (svstack-to-svex-alist st.blkst)))
      (union (union (svex-alist-vars blkst-alist)
                    (mergesort (svex-alist-keys blkst-alist)))
             (union (svex-alist-vars st.nonblkst)
                    (mergesort (svex-alist-keys st.nonblkst)))))))

Theorem: return-type-of-svstate-vars

(defthm return-type-of-svstate-vars
  (b* ((vars (svstate-vars st)))
    (and (svarlist-p vars) (setp vars)))
  :rule-classes :rewrite)

Theorem: vars-of-accessors-of-svstate-vars

(defthm vars-of-accessors-of-svstate-vars
  (b* ((?vars (svstate-vars st)))
    (implies
         (not (member v vars))
         (b* (((svstate st))
              (blkst-alist (svstack-to-svex-alist st.blkst)))
           (and (not (member v (svex-alist-vars blkst-alist)))
                (not (member v (svex-alist-keys blkst-alist)))
                (not (member v (svex-alist-vars st.nonblkst)))
                (not (member v (svex-alist-keys st.nonblkst))))))))

Theorem: svar-lookup-of-accessors-of-svstate-vars

(defthm svar-lookup-of-accessors-of-svstate-vars
  (b* ((?vars (svstate-vars st)))
    (implies (not (member (svar-fix v) vars))
             (b* (((svstate st))
                  (blkst-alist (svstack-to-svex-alist st.blkst)))
               (and (not (svex-lookup v blkst-alist))
                    (not (svex-lookup v st.nonblkst)))))))

Theorem: svstate-vars-of-svstate-fix-st

(defthm svstate-vars-of-svstate-fix-st
  (equal (svstate-vars (svstate-fix st))
         (svstate-vars st)))

Theorem: svstate-vars-svstate-equiv-congruence-on-st

(defthm svstate-vars-svstate-equiv-congruence-on-st
  (implies (svstate-equiv st st-equiv)
           (equal (svstate-vars st)
                  (svstate-vars st-equiv)))
  :rule-classes :congruence)