# 4v-sexpr-vars-1pass

Often faster alternative to 4v-sexpr-vars.

`(4v-sexpr-vars-1pass x)` is logically identical to 4v-sexpr-vars. But in the execution, a much different strategy for collecting
variables is used.

In particular, we use an ordinary fast alist as a seen-table to keep track
of the sexprs whose variables we have already seen, and a separate accumulator
for the variables we have encountered.

This approach allows us to much more quickly gather the variables from a
single sexpr. But it can be a poor choice if you need to compute the variables
of many related sexprs, basically because no information can be reused across
separate runs.

See also 4v-nsexpr-vars.

### Technical Note

The definition is slightly odd in that (1) we update SEEN even in the ATOM
case, and (2) we do the update to SEEN **after** the recursive call, even
though it means that we don't get to have a tail call.

These oddities ensure that VARS are always correct w.r.t. SEEN as we recur,
by which we mean that VARS are set-equiv to collecting vars from the keys of
SEEN.

If we were to recur in the other way, i.e., by first updating SEEN, then we
would be temporarily violating the invariant until the recursion finished.
This stupid twist makes the proof ridiculously harder!

### Definitions and Theorems

**Function: **4v-sexpr-vars-1pass-exec

(defun 4v-sexpr-vars-1pass-exec (x seen vars)
"Returns (MV SEEN VARS)"
(declare (xargs :guard t))
(b* (((when (hons-get x seen))
(mv seen vars))
((when (atom x))
(mv (hons-acons x t seen)
(if x (cons x vars) vars)))
((mv seen vars)
(4v-sexpr-vars-1pass-list-exec (cdr x)
seen vars))
(seen (hons-acons x t seen)))
(mv seen vars)))

**Function: **4v-sexpr-vars-1pass-list-exec

(defun 4v-sexpr-vars-1pass-list-exec
(x seen vars)
"Returns (MV SEEN VARS)"
(declare (xargs :guard t))
(b* (((when (atom x)) (mv seen vars))
((mv seen vars)
(4v-sexpr-vars-1pass-exec (car x)
seen vars)))
(4v-sexpr-vars-1pass-list-exec (cdr x)
seen vars)))

**Function: **4v-sexpr-vars-1pass

(defun 4v-sexpr-vars-1pass (x)
(declare (xargs :guard t))
(mbe :logic (4v-sexpr-vars x)
:exec (b* (((mv seen vars)
(4v-sexpr-vars-1pass-exec x nil nil)))
(fast-alist-free seen)
(set::mergesort vars))))

**Theorem: **4v-sexpr-vars-1pass-exec-correct

(defthm
4v-sexpr-vars-1pass-exec-correct
(equal
(set::mergesort (mv-nth 1 (4v-sexpr-vars-1pass-exec x nil nil)))
(4v-sexpr-vars x)))

**Theorem: **4v-sexpr-vars-1pass-list-exec-correct

(defthm
4v-sexpr-vars-1pass-list-exec-correct
(equal (set::mergesort
(mv-nth 1
(4v-sexpr-vars-1pass-list-exec x nil nil)))
(4v-sexpr-vars-list x)))