		Search-engine friendly clone of the ACL2 documentation.

4v-sexpr-vars

4v-nsexpr-vars

Optimized version of 4v-sexpr-vars for sexprs whose variables are natural numbers.

(4v-nsexpr-vars x) is logically just 4v-sexpr-vars. However, its guard requires that all variables in the sexpr are natural numbers; see 4v-nsexpr-p.

In the execution, we use a strategy that is quite similar to the ordinary 4v-sexpr-vars function: we memoize the entire computation and build variable sets for every sexpr subexpression. But, instead of using ordered lists of variables, we use either bitsets or sparse bitsets as our set representation. This turns out to make a very significant performance difference.

By default we use sparse bitsets since in our experiments they appear to significantly outperform ordinary bitsets when dealing with large modules. However, you can instead choose to use ordinary bitsets by running:

(4v-nsexpr-vars x :sparsep nil)

The real computation is done by 4v-nsexpr-vars-sparse or by 4v-nsexpr-vars-nonsparse. You will probably want to clear the memo tables for these functions occasionally. You may also need to clear the table for 4v-nsexpr-vars unless your guards are strong enough to ensure it will not be called.

Definitions and Theorems

Function: 4v-nsexpr-vars-fn

(defun 4v-nsexpr-vars-fn (x sparsep)
  (declare (xargs :guard (4v-nsexpr-p x)))
  (mbe :logic (4v-sexpr-vars x)
       :exec
       (if sparsep (sbitset-members (4v-nsexpr-vars-sparse x))
         (bitset-members (4v-nsexpr-vars-nonsparse x)))))

Subtopics

4v-nsexpr-vars-sparse: Sparse version.
4v-nsexpr-vars-nonsparse: Non-sparse version.