		Search-engine friendly clone of the ACL2 documentation.

4v-sexprs

4v-sexpr-vars

Collect the set of variables in an s-expression.

(4v-sexpr-vars x) is one way to produce a list of all the variables that occur in the sexpr x.

WARNING: Variable collection is surprisingly difficult to do efficiently, and is also often unnecessary.

Before deciding to collect variables, it may be worth considering whether you really need to compute the exact set of variables for a sexpr. It is often possible to efficiently overapproximate the set of all variables, e.g., if you have just carried out an esim run, the variables you assigned to the input and state bits is probably readily available.

You can often use overapproximations in scenarios such as

evaluating sexprs with 4v-sexpr-eval,
substituting into sexprs with 4v-sexpr-restrict, or
converting sexprs into faigs with 4v-sexpr-to-faig,

because in these cases it is perfectly fine for the alists to include extraneous bindings for variables that aren't in the sexpr.

Depending on your application, 4v-sexpr-vars-1pass may be a more efficient way to collect variables than 4v-sexpr-vars.

The basic approach taken by 4v-sexpr-vars is to

memoize the entire computation to avoid revisiting shared subexpressions,
produce honsed, ordered variable lists at each node so that merging is linear, and
memoize the unioning operation hons-alphorder-merge to avoid recomputing the same unions.

This might be a reasonable strategy when you care about the precise set of variables for a large number of closely-related sexprs. However, it is very memory intensive, and can be very slow unless you are really getting a lot of reuse out of the variable sets being computed. Moreover, computing the precise set of variables for every subexpression may be far more work than you really need to do, so 4v-sexpr-vars-1pass might be more appropriate.

See also 4v-nsexpr-vars, which only works when the sexprs involved have natural-numbered variables, but can use a sparse bitset representation that generally performs very well.

Definitions and Theorems

Function: 4v-sexpr-vars

(defun 4v-sexpr-vars (x)
  (declare (xargs :guard t))
  (if (atom x)
      (and x
           (mbe :logic (set::insert x nil)
                :exec (hons x nil)))
    (4v-sexpr-vars-list (cdr x))))

Function: 4v-sexpr-vars-list

(defun 4v-sexpr-vars-list (x)
 (declare (xargs :guard t))
 (if (atom x)
     nil
   (mbe :logic (set::union (4v-sexpr-vars (car x))
                           (4v-sexpr-vars-list (cdr x)))
        :exec (hons-alphorder-merge (4v-sexpr-vars (car x))
                                    (4v-sexpr-vars-list (cdr x))))))

Theorem: atom-listp-4v-sexpr-vars

(defthm atom-listp-4v-sexpr-vars
  (atom-listp (4v-sexpr-vars x)))

Theorem: atom-listp-4v-sexpr-vars-list

(defthm atom-listp-4v-sexpr-vars-list
  (atom-listp (4v-sexpr-vars-list x)))

Theorem: true-listp-4v-sexpr-vars

(defthm true-listp-4v-sexpr-vars
  (true-listp (4v-sexpr-vars x))
  :rule-classes (:rewrite :type-prescription))

Theorem: true-listp-4v-sexpr-vars-list

(defthm true-listp-4v-sexpr-vars-list
  (true-listp (4v-sexpr-vars-list x))
  :rule-classes (:rewrite :type-prescription))

Theorem: setp-4v-sexpr-vars

(defthm setp-4v-sexpr-vars
  (set::setp (4v-sexpr-vars x)))

Theorem: setp-4v-sexpr-vars-list

(defthm setp-4v-sexpr-vars-list
  (set::setp (4v-sexpr-vars-list x)))

Function: 4v-sexpr-vars-memoize-condition

(defun 4v-sexpr-vars-memoize-condition (x)
  (declare (ignorable x)
           (xargs :guard 't))
  (and (consp x) (consp (cdr x))))

Theorem: not-member-4v-sexpr-vars-lookup-when-not-member-vars-alist-vals

(defthm
    not-member-4v-sexpr-vars-lookup-when-not-member-vars-alist-vals
 (implies
  (not (member-equal k (4v-sexpr-vars-list (alist-vals al))))
  (not
     (member-equal k
                   (4v-sexpr-vars (cdr (hons-assoc-equal x al)))))))

Theorem: 4v-sexpr-vars-4v-sexpr-compose

(defthm 4v-sexpr-vars-4v-sexpr-compose
 (implies
      (not (member-equal v (4v-sexpr-vars-list (alist-vals al))))
      (not (member-equal v
                         (4v-sexpr-vars (4v-sexpr-compose x al))))))

Theorem: 4v-sexpr-vars-list-4v-sexpr-compose-list

(defthm 4v-sexpr-vars-list-4v-sexpr-compose-list
 (implies
     (not (member-equal v (4v-sexpr-vars-list (alist-vals al))))
     (not (member-equal
               v
               (4v-sexpr-vars-list (4v-sexpr-compose-list x al))))))

Theorem: 4v-sexpr-vars-4v-sexpr-restrict

(defthm 4v-sexpr-vars-4v-sexpr-restrict
 (implies
    (and (not (member-equal k (4v-sexpr-vars-list (alist-vals al))))
         (not (and (member-equal k (4v-sexpr-vars x))
                   (not (member-equal k (alist-keys al))))))
    (not (member-equal k
                       (4v-sexpr-vars (4v-sexpr-restrict x al))))))

Theorem: 4v-sexpr-vars-list-4v-sexpr-restrict-list

(defthm 4v-sexpr-vars-list-4v-sexpr-restrict-list
 (implies
    (and (not (member-equal k (4v-sexpr-vars-list (alist-vals al))))
         (not (and (member-equal k (4v-sexpr-vars-list x))
                   (not (member-equal k (alist-keys al))))))
    (not (member-equal
              k
              (4v-sexpr-vars-list (4v-sexpr-restrict-list x al))))))

Subtopics

4v-sexpr-vars-1pass: Often faster alternative to 4v-sexpr-vars.
4v-nsexpr-vars: Optimized version of 4v-sexpr-vars for sexprs whose variables are natural numbers.
4v-sexpr-vars-1pass-list-list: Often faster alternative to 4v-sexpr-vars-list-list.
4v-sexpr-vars-list-list: Extension of 4v-sexpr-vars to a list of sexpr lists.
4v-sexpr-vars-alists: Extension of 4v-sexpr-vars-alists to a list of sexpr alists.
4v-sexpr-vars-alist: Extension of 4v-sexpr-vars to a sexpr alist.
4v-sexpr-vars-1pass-list: Often faster alternative to 4v-sexpr-vars-list.
4v-sexpr-vars-list: Extension of 4v-sexpr-vars to a sexpr list.