• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-fixpoint-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Moddb
      • Svex-compilation
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
        • Rewriting
        • Svex
        • Bit-blasting
        • Functions
        • 4vmask
        • Why-infinite-width
        • Svex-vars
          • Svex-alist-vars
          • Svex-collect-vars
          • Svexlist-collect-vars
          • Svexlist-vars
          • Svex-vars-basics
        • Evaluation
        • Values
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Svex-vars
• Svex-alist

Svex-alist-vars

Collect all of the variables from all the expressions in an svex-alist.

Signature

(svex-alist-vars x) → vars

Arguments

x — Binds variables (not collected!) to their expressions (whose variables are collected).
    Guard (svex-alist-p x).

Returns

vars — An ordered set of all variables used in any of the expressions.
    Type (and (svarlist-p vars) (setp vars)).

This function is based on svex-vars; it is logically nice to reason about but probably is not what you want to execute. BOZO where is the collect- version of this; recommend an alternative.

We collect the variables from all of the expressions that are bound in the svex-alist. Note that this does not collect the keys of the alist, even though they are variables. It instead collects the variables from the expressions that the keys are bound to.

Definitions and Theorems

Function: svex-alist-vars

(defun
  svex-alist-vars (x)
  (declare (xargs :guard (svex-alist-p x)))
  (let ((__function__ 'svex-alist-vars))
       (declare (ignorable __function__))
       (if (atom x)
           nil
           (union (and (mbt (and (consp (car x)) (svar-p (caar x))))
                       (svex-vars (cdar x)))
                  (svex-alist-vars (cdr x))))))

Theorem: return-type-of-svex-alist-vars

(defthm return-type-of-svex-alist-vars
        (b* ((vars (svex-alist-vars x)))
            (and (svarlist-p vars) (setp vars)))
        :rule-classes :rewrite)

Theorem: svex-alist-vars-of-svex-alist-fix-x

(defthm svex-alist-vars-of-svex-alist-fix-x
        (equal (svex-alist-vars (svex-alist-fix x))
               (svex-alist-vars x)))

Theorem: svex-alist-vars-svex-alist-equiv-congruence-on-x

(defthm svex-alist-vars-svex-alist-equiv-congruence-on-x
        (implies (svex-alist-equiv x x-equiv)
                 (equal (svex-alist-vars x)
                        (svex-alist-vars x-equiv)))
        :rule-classes :congruence)

Theorem: svex-vars-of-svex-alist-lookup

(defthm svex-vars-of-svex-alist-lookup
        (subsetp-equal (svex-vars (svex-lookup k x))
                       (svex-alist-vars x)))

Theorem: svex-vars-of-svex-acons

(defthm svex-vars-of-svex-acons
        (equal (svex-alist-vars (svex-acons k v x))
               (union (svex-vars v)
                      (svex-alist-vars x))))

Theorem: svex-alist-vars-of-append

(defthm svex-alist-vars-of-append
        (set-equiv (svex-alist-vars (append a b))
                   (append (svex-alist-vars a)
                           (svex-alist-vars b))))

Theorem: vars-of-svex-alist-lookup

(defthm
 vars-of-svex-alist-lookup
 (implies
  (not (member v (svex-alist-vars x)))
  (not
   (member
       v
       (svex-vars (cdr (hons-assoc-equal k (svex-alist-fix x))))))))

Theorem: vars-of-fast-alist-fork

(defthm
   vars-of-fast-alist-fork
   (implies (and (not (member v (svex-alist-vars x)))
                 (not (member v (svex-alist-vars y))))
            (not (member v
                         (svex-alist-vars (fast-alist-fork x y))))))