• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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
          • Svex-alist-vars
          • Svex-collect-vars
            • Svexlist-collect-vars1
            • Svex-collect-vars1
          • Svexlist-collect-vars
          • Svexlist-vars
          • Svex-vars-basics
        • Evaluation
        • Values
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Svex-vars

Svex-collect-vars

Usually faster alternative to svex-vars.

Signature

(svex-collect-vars x) → vars

Arguments

x — Guard (svex-p x).

Returns

vars — Type (svarlist-p vars).

We compute a list of variables which occur in the svex x. This list is similar to the set of variables returned by svex-vars, except that it is not necessarily ordered. More formally:

Theorem: svex-collect-vars-correct

(defthm svex-collect-vars-correct
  (set-equiv (svex-collect-vars x)
             (svex-vars x)))

This function is usually more efficient than svex-vars. It walks over the svex, gathering variables into an accumulator and keeping track of which subtrees have already been explored using a seen table. This avoids computing exact variable information for each subexpression.

The implementation of this function is ugly and you would not want to reason about it; instead we typically prefer to reason about svex-vars and appeal to svex-collect-vars-correct.

Definitions and Theorems

Function: svex-collect-vars

(defun svex-collect-vars (x)
  (declare (xargs :guard (svex-p x)))
  (let ((__function__ 'svex-collect-vars))
    (declare (ignorable __function__))
    (b* (((mv seen vars)
          (svex-collect-vars1 x nil nil)))
      (fast-alist-free seen)
      vars)))

Theorem: svarlist-p-of-svex-collect-vars

(defthm svarlist-p-of-svex-collect-vars
  (b* ((vars (svex-collect-vars x)))
    (svarlist-p vars))
  :rule-classes :rewrite)

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

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

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

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

Theorem: svex-collect-vars-correct

(defthm svex-collect-vars-correct
  (set-equiv (svex-collect-vars x)
             (svex-vars x)))

Subtopics

Svexlist-collect-vars1

Svex-collect-vars1