Optimized version of 4v-sexpr-vars for sexprs whose variables are natural numbers.
In the execution, we use a strategy that is quite similar to the ordinary
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.
(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)))))