• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
      • 4v-sexprs
        • 4v-sexpr-vars
          • 4v-sexpr-vars-1pass
          • 4v-nsexpr-vars
          • 4v-sexpr-vars-1pass-list-list
          • 4v-sexpr-vars-list-list
          • 4v-sexpr-vars-alists
          • 4v-sexpr-vars-alist
          • 4v-sexpr-vars-1pass-list
          • 4v-sexpr-vars-list
        • 4v-sexpr-eval
        • 4v-sexpr-to-faig
        • 4v-sexpr-restrict-with-rw
        • 4vs-constructors
        • 4v-sexpr-compose-with-rw
        • 4v-sexpr-restrict
        • 4v-sexpr-alist-extract
        • 4v-sexpr-compose
        • 4v-nsexpr-p
        • 4v-sexpr-purebool-p
        • 4v-sexpr-<=
        • Sfaig
        • Sexpr-equivs
        • 3v-syntax-sexprp
        • Sexpr-rewriting
        • 4v-sexpr-ind
        • 4v-alist-extract
      • 4v-monotonicity
      • 4v-operations
      • Why-4v-logic
      • 4v-<=
      • 4vp
      • 4vcases
      • 4v-fix
      • 4v-lookup
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 4v-sexpr-vars

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)))