From 124a1fed20b60d551698e2c919280d04b13bd656 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 17 Mar 2020 09:04:34 -0700
Subject: [PATCH] [sledge] Do not use Base.Set

Summary:
The base containers have inconvenient interfaces due to lacking
support for functors, which also leads to the representation of values
of containers including closures for the comparison functions. This
causes problems when `Marshal`ing these values.

This diff is one step toward not using the base containers.

Reviewed By: ngorogiannis

Differential Revision: D20482756

fbshipit-source-id: 0312c422d
---
 sledge/bin/domain_itv.ml          |   6 +-
 sledge/bin/sledge.ml              |   2 +-
 sledge/lib/control.ml             |   2 +-
 sledge/lib/domain_sh.ml           |  48 ++++----
 sledge/lib/domain_used_globals.ml |  12 +-
 sledge/lib/equality.ml            |  52 +++++----
 sledge/lib/equality_test.ml       |   3 +-
 sledge/lib/exec.ml                |  40 ++++---
 sledge/lib/exp.ml                 | 157 +++++++++++++--------------
 sledge/lib/exp.mli                |  14 +--
 sledge/lib/import/import.ml       | 149 +++++++++++++++++--------
 sledge/lib/import/import.mli      |  99 ++++++++++-------
 sledge/lib/llair.ml               |  21 ++--
 sledge/lib/sh.ml                  | 175 ++++++++++++++++--------------
 sledge/lib/solver.ml              |  85 ++++++++-------
 sledge/lib/term.ml                |  21 ++--
 sledge/lib/term.mli               |  17 +--
 17 files changed, 497 insertions(+), 406 deletions(-)

diff --git a/sledge/bin/domain_itv.ml b/sledge/bin/domain_itv.ml
index a4cfe10d7..3d1ba2963 100644
--- a/sledge/bin/domain_itv.ml
+++ b/sledge/bin/domain_itv.ml
@@ -219,9 +219,9 @@ let exec_move q move_vec =
   let defs, uses =
     Vector.fold move_vec ~init:(Reg.Set.empty, Reg.Set.empty)
       ~f:(fun (defs, uses) (r, e) ->
-        (Set.add defs r, Exp.fold_regs e ~init:uses ~f:Set.add) )
+        (Reg.Set.add defs r, Exp.fold_regs e ~init:uses ~f:Reg.Set.add) )
   in
-  assert (Set.disjoint defs uses) ;
+  assert (Reg.Set.disjoint defs uses) ;
   Vector.fold move_vec ~init:q ~f:(fun a (r, e) -> assign r e a)
 
 let exec_inst q i =
@@ -259,7 +259,7 @@ let recursion_beyond_bound = `prune
 (** existentially quantify locals *)
 let post locals _ (q : t) =
   let locals =
-    Set.fold locals ~init:[] ~f:(fun a r ->
+    Reg.Set.fold locals ~init:[] ~f:(fun a r ->
         let v = apron_var_of_reg r in
         if Environment.mem_var q.env v then v :: a else a )
     |> Array.of_list
diff --git a/sledge/bin/sledge.ml b/sledge/bin/sledge.ml
index e935cefa6..a5d9e514e 100644
--- a/sledge/bin/sledge.ml
+++ b/sledge/bin/sledge.ml
@@ -85,7 +85,7 @@ let used_globals pgm preanalyze : Domain_used_globals.r =
   else
     Declared
       (Vector.fold pgm.globals ~init:Reg.Set.empty ~f:(fun acc g ->
-           Set.add acc g.reg ))
+           Reg.Set.add acc g.reg ))
 
 let analyze =
   let%map_open bound =
diff --git a/sledge/lib/control.ml b/sledge/lib/control.ml
index 01782ea51..7b249acc4 100644
--- a/sledge/lib/control.ml
+++ b/sledge/lib/control.ml
@@ -319,7 +319,7 @@ module Make (Dom : Domain_intf.Dom) = struct
         in
         let function_summary, post_state =
           Dom.create_summary ~locals post_state
-            ~formals:(Set.union (Reg.Set.of_list formals) globals)
+            ~formals:(Reg.Set.union (Reg.Set.of_list formals) globals)
         in
         Hashtbl.add_multi summary_table ~key:name.reg ~data:function_summary ;
         pp_st () ;
diff --git a/sledge/lib/domain_sh.ml b/sledge/lib/domain_sh.ml
index 0ea8f28a5..8ed4ba3ac 100644
--- a/sledge/lib/domain_sh.ml
+++ b/sledge/lib/domain_sh.ml
@@ -81,7 +81,7 @@ let term_eq_class_has_only_vars_in fvs cong term =
       Equality.pp cong Term.pp term]
   ;
   let term_has_only_vars_in fvs term =
-    Set.is_subset (Term.fv term) ~of_:fvs
+    Var.Set.is_subset (Term.fv term) ~of_:fvs
   in
   let term_eq_class = Equality.class_of cong term in
   List.exists ~f:(term_has_only_vars_in fvs) term_eq_class
@@ -100,7 +100,7 @@ let garbage_collect (q : t) ~wrt =
         List.fold ~init:current q.heap ~f:(fun current seg ->
             if term_eq_class_has_only_vars_in current q.cong seg.loc then
               List.fold (Equality.class_of q.cong seg.arr) ~init:current
-                ~f:(fun c e -> Set.union c (Term.fv e))
+                ~f:(fun c e -> Var.Set.union c (Term.fv e))
             else current )
       in
       all_reachable_vars current new_set q
@@ -121,10 +121,10 @@ let and_eqs sub formals actuals q =
 let localize_entry globals actuals formals freturn locals subst pre entry =
   (* Add the formals here to do garbage collection and then get rid of them *)
   let formals_set = Var.Set.of_list formals in
-  let freturn_locals = Reg.Set.vars (Set.add_option freturn locals) in
+  let freturn_locals = Reg.Set.vars (Reg.Set.add_option freturn locals) in
   let function_summary_pre =
     garbage_collect entry
-      ~wrt:(Set.union formals_set (Reg.Set.vars globals))
+      ~wrt:(Var.Set.union formals_set (Reg.Set.vars globals))
   in
   [%Trace.info "function summary pre %a" pp function_summary_pre] ;
   let foot = Sh.exists formals_set function_summary_pre in
@@ -156,18 +156,23 @@ let call ~summaries ~globals ~actuals ~areturn ~formals ~freturn ~locals q =
   let actuals = List.map ~f:Exp.term actuals in
   let areturn = Option.map ~f:Reg.var areturn in
   let formals = List.map ~f:Reg.var formals in
-  let freturn_locals = Reg.Set.vars (Set.add_option freturn locals) in
+  let freturn_locals = Reg.Set.vars (Reg.Set.add_option freturn locals) in
   let modifs = Var.Set.of_option areturn in
   (* quantify modifs, their current value will be overwritten and so does
      not need to be saved in the freshening renaming *)
   let q = Sh.exists modifs q in
   (* save current values of shadowed formals and locals with a renaming *)
-  let q', subst = Sh.freshen q ~wrt:(Set.add_list formals freturn_locals) in
-  assert (Set.disjoint modifs (Var.Subst.domain subst)) ;
+  let q', subst =
+    Sh.freshen q ~wrt:(Var.Set.add_list formals freturn_locals)
+  in
+  assert (Var.Set.disjoint modifs (Var.Subst.domain subst)) ;
   (* pass arguments by conjoining equations between formals and actuals *)
   let entry = and_eqs subst formals actuals q' in
   (* note: locals and formals are in scope *)
-  assert (Set.is_subset (Set.add_list formals freturn_locals) ~of_:entry.us) ;
+  assert (
+    Var.Set.is_subset
+      (Var.Set.add_list formals freturn_locals)
+      ~of_:entry.us ) ;
   (* simplify *)
   let entry = simplify entry in
   ( if not summaries then (entry, {areturn; subst; frame= Sh.emp})
@@ -218,7 +223,9 @@ let retn formals freturn {areturn; subst; frame} q =
     | None -> (q, inv_subst)
   in
   (* exit scope of formals *)
-  let q = Sh.exists (Set.add_list formals (Var.Set.of_option freturn)) q in
+  let q =
+    Sh.exists (Var.Set.add_list formals (Var.Set.of_option freturn)) q
+  in
   (* reinstate shadowed values of locals *)
   let q = Sh.rename inv_subst q in
   (* reconjoin frame *)
@@ -249,9 +256,9 @@ let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) =
   let locals = Reg.Set.vars locals in
   let formals = Reg.Set.vars formals in
   let foot = Sh.exists locals entry in
-  let foot, subst = Sh.freshen ~wrt:(Set.union foot.us post.us) foot in
+  let foot, subst = Sh.freshen ~wrt:(Var.Set.union foot.us post.us) foot in
   let restore_formals q =
-    Set.fold formals ~init:q ~f:(fun q var ->
+    Var.Set.fold formals ~init:q ~f:(fun q var ->
         let var = Term.var var in
         let renamed_var = Term.rename subst var in
         Sh.and_ (Term.eq renamed_var var) q )
@@ -261,11 +268,11 @@ let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) =
   let foot = restore_formals foot in
   let post = restore_formals post in
   [%Trace.info "subst: %a" Var.Subst.pp subst] ;
-  let xs = Set.inter (Sh.fv foot) (Sh.fv post) in
-  let xs = Set.diff xs formals in
-  let xs_and_formals = Set.union xs formals in
-  let foot = Sh.exists (Set.diff foot.us xs_and_formals) foot in
-  let post = Sh.exists (Set.diff post.us xs_and_formals) post in
+  let xs = Var.Set.inter (Sh.fv foot) (Sh.fv post) in
+  let xs = Var.Set.diff xs formals in
+  let xs_and_formals = Var.Set.union xs formals in
+  let foot = Sh.exists (Var.Set.diff foot.us xs_and_formals) foot in
+  let post = Sh.exists (Var.Set.diff post.us xs_and_formals) post in
   let current = Sh.extend_us xs post in
   ({xs; foot; post}, current)
   |>
@@ -274,8 +281,8 @@ let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) =
 let apply_summary q ({xs; foot; post} as fs) =
   [%Trace.call fun {pf} -> pf "fs: %a@ q: %a" pp_summary fs pp q]
   ;
-  let xs_in_q = Set.inter xs q.Sh.us in
-  let xs_in_fv_q = Set.inter xs (Sh.fv q) in
+  let xs_in_q = Var.Set.inter xs q.Sh.us in
+  let xs_in_fv_q = Var.Set.inter xs (Sh.fv q) in
   (* Between creation of a summary and its use, the vocabulary of q (q.us)
      might have been extended. That means infer_frame would fail, because q
      and foot have different vocabulary. This might indicate that the
@@ -286,11 +293,12 @@ let apply_summary q ({xs; foot; post} as fs) =
   [%Trace.info "xs inter q.us: %a" Var.Set.pp xs_in_q] ;
   [%Trace.info "xs inter fv.q %a" Var.Set.pp xs_in_fv_q] ;
   let q, add_back =
-    if Set.is_empty xs_in_fv_q then (Sh.exists xs_in_q q, xs_in_q)
+    if Var.Set.is_empty xs_in_fv_q then (Sh.exists xs_in_q q, xs_in_q)
     else (q, Var.Set.empty)
   in
   let frame =
-    if Set.is_empty xs_in_fv_q then Solver.infer_frame q xs foot else None
+    if Var.Set.is_empty xs_in_fv_q then Solver.infer_frame q xs foot
+    else None
   in
   [%Trace.info "frame %a" (Option.pp "%a" pp) frame] ;
   Option.map ~f:(Sh.extend_us add_back) (Option.map ~f:(Sh.star post) frame)
diff --git a/sledge/lib/domain_used_globals.ml b/sledge/lib/domain_used_globals.ml
index 106f7b839..4a6d551a6 100644
--- a/sledge/lib/domain_used_globals.ml
+++ b/sledge/lib/domain_used_globals.ml
@@ -9,7 +9,7 @@
 
 type t = Reg.Set.t [@@deriving equal, sexp]
 
-let pp = Set.pp Reg.pp
+let pp = Reg.Set.pp
 let report_fmt_thunk = Fn.flip pp
 let empty = Reg.Set.empty
 
@@ -17,13 +17,15 @@ let init globals =
   [%Trace.info "pgm globals: {%a}" (Vector.pp ", " Global.pp) globals] ;
   empty
 
-let join l r = Some (Set.union l r)
+let join l r = Some (Reg.Set.union l r)
 let recursion_beyond_bound = `skip
 let is_false _ = false
 let post _ _ state = state
-let retn _ _ from_call post = Set.union from_call post
+let retn _ _ from_call post = Reg.Set.union from_call post
 let dnf t = [t]
-let add_if_global gs v = if Var.global (Reg.var v) then Set.add gs v else gs
+
+let add_if_global gs v =
+  if Var.global (Reg.var v) then Reg.Set.add gs v else gs
 
 let used_globals ?(init = empty) exp =
   Exp.fold_regs exp ~init ~f:add_if_global
@@ -79,7 +81,7 @@ type summary = t
 
 let pp_summary = pp
 let create_summary ~locals:_ ~formals:_ state = (state, state)
-let apply_summary st summ = Some (Set.union st summ)
+let apply_summary st summ = Some (Reg.Set.union st summ)
 
 (** Query *)
 
diff --git a/sledge/lib/equality.ml b/sledge/lib/equality.ml
index d34f9b2e5..53066e720 100644
--- a/sledge/lib/equality.ml
+++ b/sledge/lib/equality.ml
@@ -126,7 +126,9 @@ end = struct
       [not (is_valid_eq xs e f)] implies [not (is_valid_eq ys e f)] for
       [ys ⊆ xs]. *)
   let is_valid_eq xs e f =
-    let is_var_in xs e = Option.exists ~f:(Set.mem xs) (Var.of_term e) in
+    let is_var_in xs e =
+      Option.exists ~f:(Var.Set.mem xs) (Var.of_term e)
+    in
     ( is_var_in xs e || is_var_in xs f
     || (uninterpreted e && Term.exists ~f:(is_var_in xs) e)
     || (uninterpreted f && Term.exists ~f:(is_var_in xs) f) )
@@ -148,7 +150,8 @@ end = struct
             if is_valid_eq ks key data then (t, ks, s)
             else
               let t = Term.Map.set ~key ~data t
-              and ks = Set.diff ks (Set.union (Term.fv key) (Term.fv data))
+              and ks =
+                Var.Set.diff ks (Var.Set.union (Term.fv key) (Term.fv data))
               and s = Term.Map.remove s key in
               (t, ks, s) )
       in
@@ -202,7 +205,7 @@ let extend ?f ~var ~rep (us, xs, s) =
 
 let fresh name (us, xs, s) =
   let x, us = Var.fresh name ~wrt:us in
-  let xs = Set.add xs x in
+  let xs = Var.Set.add xs x in
   (Term.var x, (us, xs, s))
 
 let solve_poly ?f p q s =
@@ -270,14 +273,14 @@ and solve_ ?f d e s =
       | Some m -> solve_ ?f n m s )
       >>= solve_ ?f a b
   | Some ((Var _ as v), (Ap3 (Extract, _, _, l) as e)) ->
-      if not (Set.mem (Term.fv e) (Var.of_ v)) then
+      if not (Var.Set.mem (Term.fv e) (Var.of_ v)) then
         (* v = α[o,l) ==> v ↦ α[o,l) when v ∉ fv(α[o,l)) *)
         extend ?f ~var:v ~rep:e s
       else
         (* v = α[o,l) ==> α[o,l) ↦ ⟨l,v⟩ when v ∈ fv(α[o,l)) *)
         extend ?f ~var:e ~rep:(Term.memory ~siz:l ~arr:v) s
   | Some ((Var _ as v), (ApN (Concat, a0V) as c)) ->
-      if not (Set.mem (Term.fv c) (Var.of_ v)) then
+      if not (Var.Set.mem (Term.fv c) (Var.of_ v)) then
         (* v = α₀^…^αᵥ ==> v ↦ α₀^…^αᵥ when v ∉ fv(α₀^…^αᵥ) *)
         extend ?f ~var:v ~rep:c s
       else
@@ -467,7 +470,7 @@ let merge us a b r =
   ;
   ( match solve ~us ~xs:r.xs a b with
   | Some (xs, s) ->
-      {r with xs= Set.union r.xs xs; rep= Subst.compose r.rep s}
+      {r with xs= Var.Set.union r.xs xs; rep= Subst.compose r.rep s}
   | None -> {r with sat= false} )
   |>
   [%Trace.retn fun {pf} r' ->
@@ -648,7 +651,7 @@ let fold_terms r ~init ~f =
 let fold_vars r ~init ~f =
   fold_terms r ~init ~f:(fun init -> Term.fold_vars ~f ~init)
 
-let fv e = fold_vars e ~f:Set.add ~init:Var.Set.empty
+let fv e = fold_vars e ~f:Var.Set.add ~init:Var.Set.empty
 let pp_classes fs r = pp_clss fs (classes r)
 let ppx_classes x fs r = ppx_clss x fs (classes r)
 
@@ -678,11 +681,11 @@ let subst_invariant us s0 s =
         (* dom of new entries not ito us *)
         assert (
           Option.for_all ~f:(Term.equal data) (Subst.find s0 key)
-          || not (Set.is_subset (Term.fv key) ~of_:us) ) ;
+          || not (Var.Set.is_subset (Term.fv key) ~of_:us) ) ;
         (* rep not ito us implies trm not ito us *)
         assert (
-          Set.is_subset (Term.fv data) ~of_:us
-          || not (Set.is_subset (Term.fv key) ~of_:us) ) ) ;
+          Var.Set.is_subset (Term.fv data) ~of_:us
+          || not (Var.Set.is_subset (Term.fv key) ~of_:us) ) ) ;
     true )
 
 type 'a zom = Zero | One of 'a | Many
@@ -696,7 +699,7 @@ let solve_poly_eq us p' q' subst =
   let max_solvables_not_ito_us =
     fold_max_solvables diff ~init:Zero ~f:(fun solvable_subterm -> function
       | Many -> Many
-      | zom when Set.is_subset (Term.fv solvable_subterm) ~of_:us -> zom
+      | zom when Var.Set.is_subset (Term.fv solvable_subterm) ~of_:us -> zom
       | One _ -> Many
       | Zero -> One solvable_subterm )
   in
@@ -710,8 +713,8 @@ let solve_memory_eq us e' f' subst =
   [%Trace.call fun {pf} -> pf "%a = %a" Term.pp e' Term.pp f']
   ;
   let f x u =
-    (not (Set.is_subset (Term.fv x) ~of_:us))
-    && Set.is_subset (Term.fv u) ~of_:us
+    (not (Var.Set.is_subset (Term.fv x) ~of_:us))
+    && Var.Set.is_subset (Term.fv u) ~of_:us
   in
   let solve_concat ms n a =
     let a, n =
@@ -720,7 +723,7 @@ let solve_memory_eq us e' f' subst =
       | None -> (Term.memory ~siz:n ~arr:a, n)
     in
     let+ _, xs, s = solve_concat ~f ms a n (us, Var.Set.empty, subst) in
-    assert (Set.is_empty xs) ;
+    assert (Var.Set.is_empty xs) ;
     s
   in
   ( match ((e' : Term.t), (f' : Term.t)) with
@@ -805,7 +808,7 @@ let solve_uninterp_eqs us (cls, subst) =
   let {rep_us; cls_us; rep_xs; cls_xs} =
     List.fold cls ~init:{rep_us= None; cls_us= []; rep_xs= None; cls_xs= []}
       ~f:(fun ({rep_us; cls_us; rep_xs; cls_xs} as s) trm ->
-        if Set.is_subset (Term.fv trm) ~of_:us then
+        if Var.Set.is_subset (Term.fv trm) ~of_:us then
           match rep_us with
           | Some rep when compare rep trm <= 0 ->
               {s with cls_us= trm :: cls_us}
@@ -869,7 +872,7 @@ let solve_class us us_xs ~key:rep ~data:cls (classes, subst) =
   ;
   let cls, cls_not_ito_us_xs =
     List.partition_tf
-      ~f:(fun e -> Set.is_subset (Term.fv e) ~of_:us_xs)
+      ~f:(fun e -> Var.Set.is_subset (Term.fv e) ~of_:us_xs)
       (rep :: cls)
   in
   let cls, subst = solve_interp_eqs us (cls, subst) in
@@ -929,7 +932,8 @@ let solve_concat_extracts r us x (classes, subst, us_xs) =
               List.fold (cls_of r e) ~init:None ~f:(fun rep_ito_us trm ->
                   match rep_ito_us with
                   | Some rep when Term.compare rep trm <= 0 -> rep_ito_us
-                  | _ when Set.is_subset (Term.fv trm) ~of_:us -> Some trm
+                  | _ when Var.Set.is_subset (Term.fv trm) ~of_:us ->
+                      Some trm
                   | _ -> rep_ito_us )
             in
             Term.memory ~siz:(Term.agg_size_exn e) ~arr:rep_ito_us :: suffix
@@ -943,7 +947,7 @@ let solve_concat_extracts r us x (classes, subst, us_xs) =
   | None -> (classes, subst, us_xs)
 
 let solve_for_xs r us xs (classes, subst, us_xs) =
-  Set.fold xs ~init:(classes, subst, us_xs)
+  Var.Set.fold xs ~init:(classes, subst, us_xs)
     ~f:(fun (classes, subst, us_xs) x ->
       let x = Term.var x in
       if Subst.mem subst x then (classes, subst, us_xs)
@@ -964,7 +968,7 @@ let solve_classes r (classes, subst, us) xs =
     if subst != subst0 then solve_classes_ (classes, subst, us_xs)
     else (classes, subst, us_xs)
   in
-  (classes, subst, Set.union us xs)
+  (classes, subst, Var.Set.union us xs)
   |> solve_classes_ |> solve_for_xs r us xs
   |>
   [%Trace.retn fun {pf} (classes', subst', _) ->
@@ -1000,14 +1004,14 @@ let solve_for_vars vss r =
         assert (
           List.fold_until vss ~init:us
             ~f:(fun us xs ->
-              let us_xs = Set.union us xs in
+              let us_xs = Var.Set.union us xs in
               let ks = Term.fv key in
               let ds = Term.fv data in
               if
-                Set.is_subset ks ~of_:us_xs
-                && Set.is_subset ds ~of_:us_xs
-                && ( Set.is_subset ds ~of_:us
-                   || not (Set.is_subset ks ~of_:us) )
+                Var.Set.is_subset ks ~of_:us_xs
+                && Var.Set.is_subset ds ~of_:us_xs
+                && ( Var.Set.is_subset ds ~of_:us
+                   || not (Var.Set.is_subset ks ~of_:us) )
               then Stop true
               else Continue us_xs )
             ~finish:(fun _ -> false) ) )]
diff --git a/sledge/lib/equality_test.ml b/sledge/lib/equality_test.ml
index 4a1ef942e..da90bd149 100644
--- a/sledge/lib/equality_test.ml
+++ b/sledge/lib/equality_test.ml
@@ -188,8 +188,7 @@ let%test_module _ =
 
     let r5 = of_eqs [(x, y); (g w x, y); (g w y, f z)]
 
-    let%test _ =
-      Set.equal (fv r5) (Set.of_list (module Var) [w_; x_; y_; z_])
+    let%test _ = Var.Set.equal (fv r5) (Var.Set.of_list [w_; x_; y_; z_])
 
     let r6 = of_eqs [(x, !1); (!1, y)]
 
diff --git a/sledge/lib/exec.ml b/sledge/lib/exec.ml
index 0e0bafd1c..e5783c824 100644
--- a/sledge/lib/exec.ml
+++ b/sledge/lib/exec.ml
@@ -17,7 +17,7 @@ type xseg = {us: Var.Set.t; xs: Var.Set.t; seg: Sh.seg}
 
 let fresh_var nam us xs =
   let var, us = Var.fresh nam ~wrt:us in
-  (Term.var var, us, Set.add xs var)
+  (Term.var var, us, Var.Set.add xs var)
 
 let fresh_seg ~loc ?bas ?len ?siz ?arr ?(xs = Var.Set.empty) us =
   let freshen term nam us xs =
@@ -38,10 +38,10 @@ let null_eq ptr = Sh.pure (Term.eq Term.null ptr)
    precondition; [us] are the variables to which ghosts must be chosen
    fresh. *)
 let assign ~ws ~rs ~us =
-  let ovs = Set.inter ws rs in
+  let ovs = Var.Set.inter ws rs in
   let sub = Var.Subst.freshen ovs ~wrt:us in
-  let us = Set.union us (Var.Subst.range sub) in
-  let ms = Set.diff ws (Var.Subst.domain sub) in
+  let us = Var.Set.union us (Var.Subst.range sub) in
+  let ms = Var.Set.diff ws (Var.Subst.domain sub) in
   (sub, ms, us)
 
 (*
@@ -58,7 +58,7 @@ let move_spec us reg_exps =
   let ws, rs =
     Vector.fold reg_exps ~init:(Var.Set.empty, Var.Set.empty)
       ~f:(fun (ws, rs) (reg, exp) ->
-        (Set.add ws reg, Set.union rs (Term.fv exp)) )
+        (Var.Set.add ws reg, Var.Set.union rs (Term.fv exp)) )
   in
   let sub, ms, _ = assign ~ws ~rs ~us in
   let post =
@@ -327,7 +327,9 @@ let posix_memalign_spec us reg ptr siz =
   let {us; xs; seg= pseg} = fresh_seg ~loc:ptr ~siz:size_of_ptr us in
   let foot = Sh.seg pseg in
   let sub, ms, us =
-    assign ~ws:(Var.Set.of_ reg) ~rs:(Set.union foot.us (Term.fv siz)) ~us
+    assign ~ws:(Var.Set.of_ reg)
+      ~rs:(Var.Set.union foot.us (Term.fv siz))
+      ~us
   in
   let q, us, xs = fresh_var "q" us xs in
   let pseg' = {pseg with arr= q} in
@@ -358,7 +360,9 @@ let realloc_spec us reg ptr siz =
   in
   let foot = Sh.or_ (null_eq ptr) (Sh.seg pseg) in
   let sub, ms, us =
-    assign ~ws:(Var.Set.of_ reg) ~rs:(Set.union foot.us (Term.fv siz)) ~us
+    assign ~ws:(Var.Set.of_ reg)
+      ~rs:(Var.Set.union foot.us (Term.fv siz))
+      ~us
   in
   let loc = Term.var reg in
   let siz = Term.rename sub siz in
@@ -421,7 +425,7 @@ let xallocx_spec us reg ptr siz ext =
   let foot = Sh.and_ Term.(dq siz zero) (Sh.seg seg) in
   let sub, ms, us =
     assign ~ws:(Var.Set.of_ reg)
-      ~rs:Set.(union foot.us (union (Term.fv siz) (Term.fv ext)))
+      ~rs:Var.Set.(union foot.us (union (Term.fv siz) (Term.fv ext)))
       ~us
   in
   let reg = Term.var reg in
@@ -601,10 +605,10 @@ let strlen_spec us reg ptr =
  *)
 
 let check_preserve_us (q0 : Sh.t) (q1 : Sh.t) =
-  let gain_us = Set.diff q1.us q0.us in
-  let lose_us = Set.diff q0.us q1.us in
-  (Set.is_empty gain_us || fail "gain us: %a" Var.Set.pp gain_us ())
-  && (Set.is_empty lose_us || fail "lose us: %a" Var.Set.pp lose_us ())
+  let gain_us = Var.Set.diff q1.us q0.us in
+  let lose_us = Var.Set.diff q0.us q1.us in
+  (Var.Set.is_empty gain_us || fail "gain us: %a" Var.Set.pp gain_us ())
+  && (Var.Set.is_empty lose_us || fail "lose us: %a" Var.Set.pp lose_us ())
 
 (* execute a command with given spec from pre *)
 let exec_spec pre0 {xs; foot; sub; ms; post} =
@@ -617,20 +621,20 @@ let exec_spec pre0 {xs; foot; sub; ms; post} =
            Format.fprintf fs "∧ %a" Var.Subst.pp sub )
        sub
        (fun fs ms ->
-         if not (Set.is_empty ms) then
+         if not (Var.Set.is_empty ms) then
            Format.fprintf fs "%a := " Var.Set.pp ms )
        ms Sh.pp post ;
      assert (
-       let vs = Set.diff (Set.diff foot.us xs) pre0.us in
-       Set.is_empty vs || fail "unbound foot: {%a}" Var.Set.pp vs () ) ;
+       let vs = Var.Set.diff (Var.Set.diff foot.us xs) pre0.us in
+       Var.Set.is_empty vs || fail "unbound foot: {%a}" Var.Set.pp vs () ) ;
      assert (
-       let vs = Set.diff (Set.diff post.us xs) pre0.us in
-       Set.is_empty vs || fail "unbound post: {%a}" Var.Set.pp vs () )]
+       let vs = Var.Set.diff (Var.Set.diff post.us xs) pre0.us in
+       Var.Set.is_empty vs || fail "unbound post: {%a}" Var.Set.pp vs () )]
   ;
   let foot = Sh.extend_us xs foot in
   let zs, pre = Sh.bind_exists pre0 ~wrt:xs in
   let+ frame = Solver.infer_frame pre xs foot in
-  Sh.exists (Set.union zs xs)
+  Sh.exists (Var.Set.union zs xs)
     (Sh.star post (Sh.exists ms (Sh.rename sub frame))))
   |>
   [%Trace.retn fun {pf} r ->
diff --git a/sledge/lib/exp.ml b/sledge/lib/exp.ml
index b5ea865da..114be01fd 100644
--- a/sledge/lib/exp.ml
+++ b/sledge/lib/exp.ml
@@ -10,80 +10,82 @@
 [@@@warning "+9"]
 
 module T = struct
-  module T0 = struct
-    type op1 =
-      (* conversion *)
-      | Signed of {bits: int}
-      | Unsigned of {bits: int}
-      | Convert of {src: Typ.t}
-      (* array/struct operations *)
-      | Splat
-      | Select of int
-    [@@deriving compare, equal, hash, sexp]
-
-    type op2 =
-      (* comparison *)
-      | Eq
-      | Dq
-      | Gt
-      | Ge
-      | Lt
-      | Le
-      | Ugt
-      | Uge
-      | Ult
-      | Ule
-      | Ord
-      | Uno
-      (* arithmetic, numeric and pointer *)
-      | Add
-      | Sub
-      | Mul
-      | Div
-      | Rem
-      | Udiv
-      | Urem
-      (* boolean / bitwise *)
-      | And
-      | Or
-      | Xor
-      | Shl
-      | Lshr
-      | Ashr
-      (* array/struct operations *)
-      | Update of int
-    [@@deriving compare, equal, hash, sexp]
-
-    type op3 = (* if-then-else *)
-      | Conditional
-    [@@deriving compare, equal, hash, sexp]
-
-    type opN =
-      (* array/struct constants *)
-      | Record
-      | Struct_rec  (** NOTE: may be cyclic *)
-    [@@deriving compare, equal, hash, sexp]
-
-    type t = {desc: desc; term: Term.t}
-
-    and desc =
-      | Reg of {name: string; typ: Typ.t}
-      | Nondet of {msg: string; typ: Typ.t}
-      | Label of {parent: string; name: string}
-      | Integer of {data: Z.t; typ: Typ.t}
-      | Float of {data: string; typ: Typ.t}
-      | Ap1 of op1 * Typ.t * t
-      | Ap2 of op2 * Typ.t * t * t
-      | Ap3 of op3 * Typ.t * t * t * t
-      | ApN of opN * Typ.t * t vector
-    [@@deriving compare, equal, hash, sexp]
-  end
-
-  include T0
-  include Comparator.Make (T0)
+  type op1 =
+    (* conversion *)
+    | Signed of {bits: int}
+    | Unsigned of {bits: int}
+    | Convert of {src: Typ.t}
+    (* array/struct operations *)
+    | Splat
+    | Select of int
+  [@@deriving compare, equal, hash, sexp]
+
+  type op2 =
+    (* comparison *)
+    | Eq
+    | Dq
+    | Gt
+    | Ge
+    | Lt
+    | Le
+    | Ugt
+    | Uge
+    | Ult
+    | Ule
+    | Ord
+    | Uno
+    (* arithmetic, numeric and pointer *)
+    | Add
+    | Sub
+    | Mul
+    | Div
+    | Rem
+    | Udiv
+    | Urem
+    (* boolean / bitwise *)
+    | And
+    | Or
+    | Xor
+    | Shl
+    | Lshr
+    | Ashr
+    (* array/struct operations *)
+    | Update of int
+  [@@deriving compare, equal, hash, sexp]
+
+  type op3 = (* if-then-else *)
+    | Conditional
+  [@@deriving compare, equal, hash, sexp]
+
+  type opN =
+    (* array/struct constants *)
+    | Record
+    | Struct_rec  (** NOTE: may be cyclic *)
+  [@@deriving compare, equal, hash, sexp]
+
+  type t = {desc: desc; term: Term.t}
+
+  and desc =
+    | Reg of {name: string; typ: Typ.t}
+    | Nondet of {msg: string; typ: Typ.t}
+    | Label of {parent: string; name: string}
+    | Integer of {data: Z.t; typ: Typ.t}
+    | Float of {data: string; typ: Typ.t}
+    | Ap1 of op1 * Typ.t * t
+    | Ap2 of op2 * Typ.t * t * t
+    | Ap3 of op3 * Typ.t * t * t * t
+    | ApN of opN * Typ.t * t vector
+  [@@deriving compare, equal, hash, sexp]
 end
 
 include T
+
+module Set = struct
+  include Set.Make (T)
+
+  let t_of_sexp = t_of_sexp T.t_of_sexp
+end
+
 module Map = Map.Make (T)
 
 let term e = e.term
@@ -316,17 +318,12 @@ module Reg = struct
     match Var.of_term r.term with Some v -> v | _ -> violates invariant r
 
   module Set = struct
-    include (
-      Set :
-        module type of Set with type ('elt, 'cmp) t := ('elt, 'cmp) Set.t )
-
-    type t = Set.M(T).t [@@deriving compare, equal, sexp]
+    include Set
 
     let pp = Set.pp pp_exp
-    let empty = Set.empty (module T)
-    let of_list = Set.of_list (module T)
-    let union_list = Set.union_list (module T)
-    let vars = Set.fold ~init:Var.Set.empty ~f:(fun s r -> add s (var r))
+
+    let vars =
+      Set.fold ~init:Var.Set.empty ~f:(fun s r -> Var.Set.add s (var r))
   end
 
   module Map = Map
diff --git a/sledge/lib/exp.mli b/sledge/lib/exp.mli
index d0012f347..d0ef04c48 100644
--- a/sledge/lib/exp.mli
+++ b/sledge/lib/exp.mli
@@ -90,8 +90,6 @@ and desc = private
   | ApN of opN * Typ.t * t vector
 [@@deriving compare, equal, hash, sexp]
 
-include Comparator.S with type t := t
-
 val pp : t pp
 
 include Invariant.S with type t := t
@@ -101,18 +99,12 @@ module Reg : sig
   type exp := t
   type t = private exp [@@deriving compare, equal, hash, sexp]
 
-  include Comparator.S with type t := t
-
   module Set : sig
-    type reg := t
-
-    type t = (reg, comparator_witness) Set.t
-    [@@deriving compare, equal, sexp]
+    include Set.S with type elt := t
 
+    val sexp_of_t : t -> Sexp.t
+    val t_of_sexp : Sexp.t -> t
     val pp : t pp
-    val empty : t
-    val of_list : reg list -> t
-    val union_list : t list -> t
     val vars : t -> Var.Set.t
   end
 
diff --git a/sledge/lib/import/import.ml b/sledge/lib/import/import.ml
index ac0304eea..d966aa860 100644
--- a/sledge/lib/import/import.ml
+++ b/sledge/lib/import/import.ml
@@ -171,6 +171,14 @@ end
 include Option.Monad_infix
 include Option.Monad_syntax
 
+module Result = struct
+  include Base.Result
+
+  let pp fmt pp_elt fs = function
+    | Ok x -> Format.fprintf fs fmt pp_elt x
+    | Error _ -> ()
+end
+
 module List = struct
   include Base.List
 
@@ -253,6 +261,14 @@ module List = struct
     pp sep pp_diff_elt fs (symmetric_diff ~compare xs ys)
 end
 
+module Vector = struct
+  include Vector
+
+  let pp sep pp_elt fs v = List.pp sep pp_elt fs (to_list v)
+end
+
+include Vector.Infix
+
 module type OrderedType = sig
   type t
 
@@ -262,6 +278,94 @@ end
 
 exception Duplicate
 
+module Set = struct
+  module type S = sig
+    type elt
+    type t
+
+    val compare : t -> t -> int
+    val equal : t -> t -> bool
+    val sexp_of_t : t -> Sexp.t
+    val t_of_sexp : (Sexp.t -> elt) -> Sexp.t -> t
+    val pp : elt pp -> t pp
+    val pp_diff : elt pp -> (t * t) pp
+
+    (* initial constructors *)
+    val empty : t
+    val of_ : elt -> t
+    val of_option : elt option -> t
+    val of_list : elt list -> t
+    val of_vector : elt vector -> t
+
+    (* constructors *)
+    val add : t -> elt -> t
+    val add_option : elt option -> t -> t
+    val add_list : elt list -> t -> t
+    val remove : t -> elt -> t
+    val filter : t -> f:(elt -> bool) -> t
+    val union : t -> t -> t
+    val union_list : t list -> t
+    val diff : t -> t -> t
+    val inter : t -> t -> t
+    val diff_inter : t -> t -> t * t
+
+    (* queries *)
+    val is_empty : t -> bool
+    val mem : t -> elt -> bool
+    val is_subset : t -> of_:t -> bool
+    val disjoint : t -> t -> bool
+    val max_elt : t -> elt option
+
+    (* traversals *)
+    val fold : t -> init:'s -> f:('s -> elt -> 's) -> 's
+  end
+
+  module Make (Elt : OrderedType) : S with type elt = Elt.t = struct
+    module S = Caml.Set.Make (Elt)
+
+    type elt = Elt.t
+    type t = S.t
+
+    let compare = S.compare
+    let equal = S.equal
+    let sexp_of_t s = List.sexp_of_t Elt.sexp_of_t (S.elements s)
+
+    let t_of_sexp elt_of_sexp sexp =
+      S.of_list (List.t_of_sexp elt_of_sexp sexp)
+
+    let pp pp_elt fs x = List.pp ",@ " pp_elt fs (S.elements x)
+
+    let pp_diff pp_elt fs (xs, ys) =
+      let lose = S.diff xs ys and gain = S.diff ys xs in
+      if not (S.is_empty lose) then
+        Format.fprintf fs "-- %a" (pp pp_elt) lose ;
+      if not (S.is_empty gain) then
+        Format.fprintf fs "++ %a" (pp pp_elt) gain
+
+    let empty = S.empty
+    let of_ x = S.add x empty
+    let of_option = Option.fold ~f:(fun x y -> S.add y x) ~init:empty
+    let of_list = S.of_list
+    let of_vector x = S.of_list (Vector.to_list x)
+    let add s e = S.add e s
+    let add_option yo x = Option.fold ~f:(fun x y -> S.add y x) ~init:x yo
+    let add_list ys x = List.fold ~f:(fun x y -> S.add y x) ~init:x ys
+    let remove s e = S.remove e s
+    let filter s ~f = S.filter f s
+    let union = S.union
+    let union_list ss = List.fold ss ~init:empty ~f:union
+    let diff = S.diff
+    let inter = S.inter
+    let diff_inter x y = (S.diff x y, S.inter x y)
+    let is_empty = S.is_empty
+    let mem s e = S.mem e s
+    let is_subset x ~of_ = S.subset x of_
+    let disjoint = S.disjoint
+    let max_elt = S.max_elt_opt
+    let fold s ~init:z ~f = S.fold (fun z x -> f x z) s z
+  end
+end
+
 module Map = struct
   module type S = sig
     type key
@@ -450,51 +554,6 @@ module Map = struct
   end
 end
 
-module Result = struct
-  include Base.Result
-
-  let pp fmt pp_elt fs = function
-    | Ok x -> Format.fprintf fs fmt pp_elt x
-    | Error _ -> ()
-end
-
-module Vector = struct
-  include Vector
-
-  let pp sep pp_elt fs v = List.pp sep pp_elt fs (to_list v)
-end
-
-include Vector.Infix
-
-module Set = struct
-  include Base.Set
-
-  type ('elt, 'cmp) tree = ('elt, 'cmp) Using_comparator.Tree.t
-
-  let equal_m__t (module Elt : Compare_m) = equal
-  let pp pp_elt fs x = List.pp ",@ " pp_elt fs (to_list x)
-
-  let pp_diff pp_elt fs (xs, ys) =
-    let lose = diff xs ys and gain = diff ys xs in
-    if not (is_empty lose) then Format.fprintf fs "-- %a" (pp pp_elt) lose ;
-    if not (is_empty gain) then Format.fprintf fs "++ %a" (pp pp_elt) gain
-
-  let disjoint x y = is_empty (inter x y)
-  let add_option yo x = Option.fold ~f:add ~init:x yo
-  let add_list ys x = List.fold ~f:add ~init:x ys
-  let diff_inter x y = (diff x y, inter x y)
-  let diff_inter_diff x y = (diff x y, inter x y, diff y x)
-  let of_vector cmp x = of_array cmp (Vector.to_array x)
-  let to_tree = Using_comparator.to_tree
-
-  let union x y =
-    let xy = union x y in
-    let xy_tree = to_tree xy in
-    if xy_tree == to_tree x then x
-    else if xy_tree == to_tree y then y
-    else xy
-end
-
 module Qset = struct
   include Qset
 
diff --git a/sledge/lib/import/import.mli b/sledge/lib/import/import.mli
index e9a2fcf53..feb2bb099 100644
--- a/sledge/lib/import/import.mli
+++ b/sledge/lib/import/import.mli
@@ -138,6 +138,13 @@ end
 include module type of Option.Monad_infix
 include module type of Option.Monad_syntax with type 'a t = 'a option
 
+module Result : sig
+  include module type of Base.Result
+
+  val pp : ('a_pp -> 'a -> unit, unit) fmt -> 'a_pp -> ('a, _) t pp
+  (** Pretty-print a result. *)
+end
+
 module List : sig
   include module type of Base.List
 
@@ -192,6 +199,15 @@ module List : sig
     compare:('a -> 'a -> int) -> 'a t -> 'a t -> ('a, 'a) Either.t t
 end
 
+module Vector : sig
+  include module type of Vector
+
+  val pp : (unit, unit) fmt -> 'a pp -> 'a t pp
+  (** Pretty-print a vector. *)
+end
+
+include module type of Vector.Infix
+
 module type OrderedType = sig
   type t
 
@@ -201,6 +217,51 @@ end
 
 exception Duplicate
 
+module Set : sig
+  module type S = sig
+    type elt
+    type t
+
+    val compare : t -> t -> int
+    val equal : t -> t -> bool
+    val sexp_of_t : t -> Sexp.t
+    val t_of_sexp : (Sexp.t -> elt) -> Sexp.t -> t
+    val pp : elt pp -> t pp
+    val pp_diff : elt pp -> (t * t) pp
+
+    (* initial constructors *)
+    val empty : t
+    val of_ : elt -> t
+    val of_option : elt option -> t
+    val of_list : elt list -> t
+    val of_vector : elt vector -> t
+
+    (* constructors *)
+    val add : t -> elt -> t
+    val add_option : elt option -> t -> t
+    val add_list : elt list -> t -> t
+    val remove : t -> elt -> t
+    val filter : t -> f:(elt -> bool) -> t
+    val union : t -> t -> t
+    val union_list : t list -> t
+    val diff : t -> t -> t
+    val inter : t -> t -> t
+    val diff_inter : t -> t -> t * t
+
+    (* queries *)
+    val is_empty : t -> bool
+    val mem : t -> elt -> bool
+    val is_subset : t -> of_:t -> bool
+    val disjoint : t -> t -> bool
+    val max_elt : t -> elt option
+
+    (* traversals *)
+    val fold : t -> init:'s -> f:('s -> elt -> 's) -> 's
+  end
+
+  module Make (Elt : OrderedType) : S with type elt = Elt.t
+end
+
 module Map : sig
   module type S = sig
     type key
@@ -265,44 +326,6 @@ module Map : sig
   module Make (Key : OrderedType) : S with type key = Key.t
 end
 
-module Result : sig
-  include module type of Base.Result
-
-  val pp : ('a_pp -> 'a -> unit, unit) fmt -> 'a_pp -> ('a, _) t pp
-  (** Pretty-print a result. *)
-end
-
-module Vector : sig
-  include module type of Vector
-
-  val pp : (unit, unit) fmt -> 'a pp -> 'a t pp
-  (** Pretty-print a vector. *)
-end
-
-include module type of Vector.Infix
-
-module Set : sig
-  include module type of Base.Set
-
-  type ('e, 'c) tree
-
-  val equal_m__t :
-    (module Compare_m) -> ('elt, 'cmp) t -> ('elt, 'cmp) t -> bool
-
-  val pp : 'e pp -> ('e, 'c) t pp
-  val pp_diff : 'e pp -> (('e, 'c) t * ('e, 'c) t) pp
-  val disjoint : ('e, 'c) t -> ('e, 'c) t -> bool
-  val add_option : 'e option -> ('e, 'c) t -> ('e, 'c) t
-  val add_list : 'e list -> ('e, 'c) t -> ('e, 'c) t
-  val diff_inter : ('e, 'c) t -> ('e, 'c) t -> ('e, 'c) t * ('e, 'c) t
-
-  val diff_inter_diff :
-    ('e, 'c) t -> ('e, 'c) t -> ('e, 'c) t * ('e, 'c) t * ('e, 'c) t
-
-  val of_vector : ('e, 'c) comparator -> 'e vector -> ('e, 'c) t
-  val to_tree : ('e, 'c) t -> ('e, 'c) tree
-end
-
 module Qset : sig
   include module type of Qset
 
diff --git a/sledge/lib/llair.ml b/sledge/lib/llair.ml
index 4051545fd..e2c87a942 100644
--- a/sledge/lib/llair.ml
+++ b/sledge/lib/llair.ml
@@ -254,9 +254,11 @@ module Inst = struct
   let union_locals inst vs =
     match inst with
     | Move {reg_exps; _} ->
-        Vector.fold ~f:(fun vs (reg, _) -> Set.add vs reg) ~init:vs reg_exps
+        Vector.fold
+          ~f:(fun vs (reg, _) -> Reg.Set.add vs reg)
+          ~init:vs reg_exps
     | Load {reg; _} | Alloc {reg; _} | Nondet {reg= Some reg; _} ->
-        Set.add vs reg
+        Reg.Set.add vs reg
     | Store _ | Memcpy _ | Memmov _ | Memset _ | Free _
      |Nondet {reg= None; _}
      |Abort _ ->
@@ -349,7 +351,7 @@ module Term = struct
 
   let union_locals term vs =
     match term with
-    | Call {areturn; _} -> Set.add_option areturn vs
+    | Call {areturn; _} -> Reg.Set.add_option areturn vs
     | _ -> vs
 end
 
@@ -389,8 +391,7 @@ module Block_label = struct
   end
 
   include T
-
-  let empty_set = Set.empty (module T)
+  module Set = Set.Make (T)
 end
 
 module BlockQ = Hash_queue.Make (Block_label)
@@ -535,9 +536,10 @@ let set_derived_metadata functions =
     let rec visit ancestors func src =
       if BlockQ.mem tips_to_roots src then ()
       else
-        let ancestors = Set.add ancestors src in
+        let ancestors = Block_label.Set.add ancestors src in
         let jump jmp =
-          if Set.mem ancestors jmp.dst then jmp.retreating <- true
+          if Block_label.Set.mem ancestors jmp.dst then
+            jmp.retreating <- true
           else visit ancestors func jmp.dst
         in
         ( match src.term with
@@ -551,7 +553,8 @@ let set_derived_metadata functions =
                   (Option.map ~f:Reg.name (Reg.of_exp callee))
               with
             | Some func ->
-                if Set.mem ancestors func.entry then call.recursive <- true
+                if Block_label.Set.mem ancestors func.entry then
+                  call.recursive <- true
                 else visit ancestors func func.entry
             | None ->
                 (* conservatively assume all virtual calls are recursive *)
@@ -561,7 +564,7 @@ let set_derived_metadata functions =
         BlockQ.enqueue_back_exn tips_to_roots src ()
     in
     FuncQ.iter roots ~f:(fun root ->
-        visit Block_label.empty_set root root.entry ) ;
+        visit Block_label.Set.empty root root.entry ) ;
     tips_to_roots
   in
   let set_sort_indices tips_to_roots =
diff --git a/sledge/lib/sh.ml b/sledge/lib/sh.ml
index 395bc0600..02c9f40b4 100644
--- a/sledge/lib/sh.ml
+++ b/sledge/lib/sh.ml
@@ -103,10 +103,11 @@ let rec var_strength_ xs m q =
     | Some `Anonymous -> Var.Map.set m ~key:v ~data:`Existential
     | Some _ -> m
   in
-  let xs = Set.union xs q.xs in
+  let xs = Var.Set.union xs q.xs in
   let m_stem =
     fold_vars_stem ~ignore_cong:() q ~init:m ~f:(fun m var ->
-        if not (Set.mem xs var) then Var.Map.set m ~key:var ~data:`Universal
+        if not (Var.Set.mem xs var) then
+          Var.Map.set m ~key:var ~data:`Universal
         else add m var )
   in
   let m =
@@ -124,7 +125,7 @@ let rec var_strength_ xs m q =
 
 let var_strength_full ?(xs = Var.Set.empty) q =
   let m =
-    Set.fold xs ~init:Var.Map.empty ~f:(fun m x ->
+    Var.Set.fold xs ~init:Var.Map.empty ~f:(fun m x ->
         Var.Map.set m ~key:x ~data:`Existential )
   in
   var_strength_ xs m q
@@ -202,12 +203,12 @@ let pp_heap x ?pre cong fs heap =
 let pp_us ?(pre = ("" : _ fmt)) ?vs () fs us =
   match vs with
   | None ->
-      if not (Set.is_empty us) then
+      if not (Var.Set.is_empty us) then
         [%Trace.fprintf fs "%( %)@[%a@] .@ " pre Var.Set.pp us]
   | Some vs ->
-      if not (Set.equal vs us) then
+      if not (Var.Set.equal vs us) then
         [%Trace.fprintf
-          fs "%( %)@[%a@] .@ " pre (Set.pp_diff Var.pp) (vs, us)]
+          fs "%( %)@[%a@] .@ " pre (Var.Set.pp_diff Var.pp) (vs, us)]
 
 let rec pp_ ?var_strength vs parent_xs parent_cong fs
     {us; xs; cong; pure; heap; djns} =
@@ -215,14 +216,14 @@ let rec pp_ ?var_strength vs parent_xs parent_cong fs
   let x v = Option.bind ~f:(fun (_, m) -> Var.Map.find m v) var_strength in
   pp_us ~vs () fs us ;
   let xs_d_vs, xs_i_vs =
-    Set.diff_inter
-      (Set.filter xs ~f:(fun v -> Poly.(x v <> Some `Anonymous)))
+    Var.Set.diff_inter
+      (Var.Set.filter xs ~f:(fun v -> Poly.(x v <> Some `Anonymous)))
       vs
   in
-  if not (Set.is_empty xs_i_vs) then (
+  if not (Var.Set.is_empty xs_i_vs) then (
     Format.fprintf fs "@<2>∃ @[%a@] ." (Var.Set.ppx x) xs_i_vs ;
-    if not (Set.is_empty xs_d_vs) then Format.fprintf fs "@ " ) ;
-  if not (Set.is_empty xs_d_vs) then
+    if not (Var.Set.is_empty xs_d_vs) then Format.fprintf fs "@ " ) ;
+  if not (Var.Set.is_empty xs_d_vs) then
     Format.fprintf fs "@<2>∃ @[%a@] .@ " (Var.Set.ppx x) xs_d_vs ;
   let first = Equality.entails parent_cong cong in
   if not first then Format.fprintf fs "  " ;
@@ -250,8 +251,9 @@ let rec pp_ ?var_strength vs parent_xs parent_cong fs
     ~pre:(if first then "  " else "@ * ")
     "@ * "
     (pp_djn ?var_strength
-       (Set.union vs (Set.union us xs))
-       (Set.union parent_xs xs) cong)
+       (Var.Set.union vs (Var.Set.union us xs))
+       (Var.Set.union parent_xs xs)
+       cong)
     fs djns ;
   Format.pp_close_box fs ()
 
@@ -265,7 +267,7 @@ and pp_djn ?var_strength vs xs cong fs = function
                var_strength_ xs var_strength_stem sjn
              in
              Format.fprintf fs "@[<hv 1>(%a)@]"
-               (pp_ ?var_strength vs (Set.union xs sjn.xs) cong)
+               (pp_ ?var_strength vs (Var.Set.union xs sjn.xs) cong)
                sjn ))
         djn
 
@@ -275,11 +277,13 @@ let pp_diff_eq ?(us = Var.Set.empty) ?(xs = Var.Set.empty) cong fs q =
 let pp fs q = pp_diff_eq Equality.true_ fs q
 let pp_djn fs d = pp_djn Var.Set.empty Var.Set.empty Equality.true_ fs d
 let pp_raw fs q = pp_ Var.Set.empty Var.Set.empty Equality.true_ fs q
-let fv_seg seg = fold_vars_seg seg ~f:Set.add ~init:Var.Set.empty
+let fv_seg seg = fold_vars_seg seg ~f:Var.Set.add ~init:Var.Set.empty
 
 let fv ?ignore_cong q =
   let rec fv_union init q =
-    Set.diff (fold_vars ?ignore_cong fv_union q ~init ~f:Set.add) q.xs
+    Var.Set.diff
+      (fold_vars ?ignore_cong fv_union q ~init ~f:Var.Set.add)
+      q.xs
   in
   fv_union Var.Set.empty q
 
@@ -295,12 +299,13 @@ let rec invariant q =
   let {us; xs; cong; pure; heap; djns} = q in
   try
     assert (
-      Set.disjoint us xs
-      || fail "inter: @[%a@]@\nq: @[%a@]" Var.Set.pp (Set.inter us xs) pp q
-           () ) ;
+      Var.Set.disjoint us xs
+      || fail "inter: @[%a@]@\nq: @[%a@]" Var.Set.pp (Var.Set.inter us xs)
+           pp q () ) ;
     assert (
-      Set.is_subset (fv q) ~of_:us
-      || fail "unbound but free: %a" Var.Set.pp (Set.diff (fv q) us) () ) ;
+      Var.Set.is_subset (fv q) ~of_:us
+      || fail "unbound but free: %a" Var.Set.pp (Var.Set.diff (fv q) us) ()
+    ) ;
     Equality.invariant cong ;
     ( match djns with
     | [[]] ->
@@ -312,7 +317,7 @@ let rec invariant q =
     List.iter heap ~f:invariant_seg ;
     List.iter djns ~f:(fun djn ->
         List.iter djn ~f:(fun sjn ->
-            assert (Set.is_subset sjn.us ~of_:(Set.union us xs)) ;
+            assert (Var.Set.is_subset sjn.us ~of_:(Var.Set.union us xs)) ;
             invariant sjn ) )
   with exc -> [%Trace.info "%a" pp q] ; raise exc
 
@@ -324,7 +329,8 @@ let rec apply_subst sub q =
   map q ~f_sjn:(rename sub)
     ~f_cong:(fun r -> Equality.rename r sub)
     ~f_trm:(Term.rename sub)
-  |> check (fun q' -> assert (Set.disjoint (fv q') (Var.Subst.domain sub)))
+  |> check (fun q' ->
+         assert (Var.Set.disjoint (fv q') (Var.Subst.domain sub)) )
 
 and rename sub q =
   [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Var.Subst.pp sub pp q]
@@ -333,20 +339,20 @@ and rename sub q =
   ( if Var.Subst.is_empty sub then q
   else
     let us = Var.Subst.apply_set sub q.us in
-    assert (not (Set.equal us q.us)) ;
-    let q' = apply_subst sub (freshen_xs q ~wrt:(Set.union q.us us)) in
+    assert (not (Var.Set.equal us q.us)) ;
+    let q' = apply_subst sub (freshen_xs q ~wrt:(Var.Set.union q.us us)) in
     {q' with us} )
   |>
   [%Trace.retn fun {pf} q' ->
     pf "%a" pp q' ;
     invariant q' ;
-    assert (Set.disjoint q'.us (Var.Subst.domain sub))]
+    assert (Var.Set.disjoint q'.us (Var.Subst.domain sub))]
 
 (** freshen existentials, preserving vocabulary *)
 and freshen_xs q ~wrt =
   [%Trace.call fun {pf} ->
     pf "{@[%a@]}@ %a" Var.Set.pp wrt pp q ;
-    assert (Set.is_subset q.us ~of_:wrt)]
+    assert (Var.Set.is_subset q.us ~of_:wrt)]
   ;
   let sub = Var.Subst.freshen q.xs ~wrt in
   ( if Var.Subst.is_empty sub then q
@@ -357,32 +363,33 @@ and freshen_xs q ~wrt =
   |>
   [%Trace.retn fun {pf} q' ->
     pf "%a@ %a" Var.Subst.pp sub pp q' ;
-    assert (Set.equal q'.us q.us) ;
-    assert (Set.disjoint q'.xs (Var.Subst.domain sub)) ;
-    assert (Set.disjoint q'.xs (Set.inter q.xs wrt)) ;
+    assert (Var.Set.equal q'.us q.us) ;
+    assert (Var.Set.disjoint q'.xs (Var.Subst.domain sub)) ;
+    assert (Var.Set.disjoint q'.xs (Var.Set.inter q.xs wrt)) ;
     invariant q']
 
 let extend_us us q =
-  let us = Set.union us q.us in
+  let us = Var.Set.union us q.us in
   let q' = freshen_xs q ~wrt:us in
   (if us == q.us && q' == q then q else {q' with us}) |> check invariant
 
 let freshen ~wrt q =
-  let sub = Var.Subst.freshen q.us ~wrt:(Set.union wrt q.xs) in
+  let sub = Var.Subst.freshen q.us ~wrt:(Var.Set.union wrt q.xs) in
   let q' = extend_us wrt (rename sub q) in
   (if q' == q then (q, sub) else (q', sub))
   |> check (fun (q', _) ->
          invariant q' ;
-         assert (Set.is_subset wrt ~of_:q'.us) ;
-         assert (Set.disjoint wrt (fv q')) )
+         assert (Var.Set.is_subset wrt ~of_:q'.us) ;
+         assert (Var.Set.disjoint wrt (fv q')) )
 
 let bind_exists q ~wrt =
   [%Trace.call fun {pf} -> pf "{@[%a@]}@ %a" Var.Set.pp wrt pp q]
   ;
   let q' =
-    if Set.is_empty wrt then q else freshen_xs q ~wrt:(Set.union q.us wrt)
+    if Var.Set.is_empty wrt then q
+    else freshen_xs q ~wrt:(Var.Set.union q.us wrt)
   in
-  (q'.xs, {q' with us= Set.union q'.us q'.xs; xs= Var.Set.empty})
+  (q'.xs, {q' with us= Var.Set.union q'.us q'.xs; xs= Var.Set.empty})
   |>
   [%Trace.retn fun {pf} (_, q') -> pf "%a" pp q']
 
@@ -390,12 +397,12 @@ let exists_fresh xs q =
   [%Trace.call fun {pf} ->
     pf "{@[%a@]}@ %a" Var.Set.pp xs pp q ;
     assert (
-      Set.disjoint xs q.us
+      Var.Set.disjoint xs q.us
       || fail "Sh.exists_fresh xs ∩ q.us: %a" Var.Set.pp
-           (Set.inter xs q.us) () )]
+           (Var.Set.inter xs q.us) () )]
   ;
-  ( if Set.is_empty xs then q
-  else {q with xs= Set.union q.xs xs} |> check invariant )
+  ( if Var.Set.is_empty xs then q
+  else {q with xs= Var.Set.union q.xs xs} |> check invariant )
   |>
   [%Trace.retn fun {pf} -> pf "%a" pp]
 
@@ -403,26 +410,27 @@ let exists xs q =
   [%Trace.call fun {pf} -> pf "{@[%a@]}@ %a" Var.Set.pp xs pp q]
   ;
   assert (
-    Set.is_subset xs ~of_:q.us
-    || fail "Sh.exists xs - q.us: %a" Var.Set.pp (Set.diff xs q.us) () ) ;
-  ( if Set.is_empty xs then q
+    Var.Set.is_subset xs ~of_:q.us
+    || fail "Sh.exists xs - q.us: %a" Var.Set.pp (Var.Set.diff xs q.us) ()
+  ) ;
+  ( if Var.Set.is_empty xs then q
   else
-    {q with us= Set.diff q.us xs; xs= Set.union q.xs xs} |> check invariant
-  )
+    {q with us= Var.Set.diff q.us xs; xs= Var.Set.union q.xs xs}
+    |> check invariant )
   |>
   [%Trace.retn fun {pf} -> pf "%a" pp]
 
 (** remove quantification on variables disjoint from vocabulary *)
 let elim_exists xs q =
-  assert (Set.disjoint xs q.us) ;
-  {q with us= Set.union q.us xs; xs= Set.diff q.xs xs}
+  assert (Var.Set.disjoint xs q.us) ;
+  {q with us= Var.Set.union q.us xs; xs= Var.Set.diff q.xs xs}
 
 (** Construct *)
 
 (** conjoin an equality relation assuming vocabulary is compatible *)
 let and_cong_ cong q =
-  assert (Set.is_subset (Equality.fv cong) ~of_:q.us) ;
-  let xs, cong = Equality.and_ (Set.union q.us q.xs) q.cong cong in
+  assert (Var.Set.is_subset (Equality.fv cong) ~of_:q.us) ;
+  let xs, cong = Equality.and_ (Var.Set.union q.us q.xs) q.cong cong in
   if Equality.is_false cong then false_ q.us
   else exists_fresh xs {q with cong}
 
@@ -440,30 +448,30 @@ let star q1 q2 =
   ;
   ( match (q1, q2) with
   | {djns= [[]]; _}, _ | _, {djns= [[]]; _} ->
-      false_ (Set.union q1.us q2.us)
+      false_ (Var.Set.union q1.us q2.us)
   | {us= _; xs= _; cong; pure= []; heap= []; djns= []}, _
     when Equality.is_true cong ->
-      let us = Set.union q1.us q2.us in
+      let us = Var.Set.union q1.us q2.us in
       if us == q2.us then q2 else {q2 with us}
   | _, {us= _; xs= _; cong; pure= []; heap= []; djns= []}
     when Equality.is_true cong ->
-      let us = Set.union q1.us q2.us in
+      let us = Var.Set.union q1.us q2.us in
       if us == q1.us then q1 else {q1 with us}
   | _ ->
-      let us = Set.union q1.us q2.us in
-      let q1 = freshen_xs q1 ~wrt:(Set.union us q2.xs) in
-      let q2 = freshen_xs q2 ~wrt:(Set.union us q1.xs) in
+      let us = Var.Set.union q1.us q2.us in
+      let q1 = freshen_xs q1 ~wrt:(Var.Set.union us q2.xs) in
+      let q2 = freshen_xs q2 ~wrt:(Var.Set.union us q1.xs) in
       let {us= us1; xs= xs1; cong= c1; pure= p1; heap= h1; djns= d1} = q1 in
       let {us= us2; xs= xs2; cong= c2; pure= p2; heap= h2; djns= d2} = q2 in
-      assert (Set.equal us (Set.union us1 us2)) ;
+      assert (Var.Set.equal us (Var.Set.union us1 us2)) ;
       let xs, cong =
-        Equality.and_ (Set.union us (Set.union xs1 xs2)) c1 c2
+        Equality.and_ (Var.Set.union us (Var.Set.union xs1 xs2)) c1 c2
       in
       if Equality.is_false cong then false_ us
       else
         exists_fresh xs
           { us
-          ; xs= Set.union xs1 xs2
+          ; xs= Var.Set.union xs1 xs2
           ; cong
           ; pure= List.append p1 p2
           ; heap= List.append h1 h2
@@ -472,7 +480,7 @@ let star q1 q2 =
   [%Trace.retn fun {pf} q ->
     pf "%a" pp q ;
     invariant q ;
-    assert (Set.equal q.us (Set.union q1.us q2.us))]
+    assert (Var.Set.equal q.us (Var.Set.union q1.us q2.us))]
 
 let starN = function
   | [] -> emp
@@ -487,14 +495,14 @@ let or_ q1 q2 =
   | _, {djns= [[]]; _} -> extend_us q2.us q1
   | ( ({djns= []; _} as q)
     , ({us= _; xs; cong= _; pure= []; heap= []; djns= [djn]} as d) )
-    when Set.is_empty xs ->
-      {d with us= Set.union q.us d.us; djns= [q :: djn]}
+    when Var.Set.is_empty xs ->
+      {d with us= Var.Set.union q.us d.us; djns= [q :: djn]}
   | ( ({us= _; xs; cong= _; pure= []; heap= []; djns= [djn]} as d)
     , ({djns= []; _} as q) )
-    when Set.is_empty xs ->
-      {d with us= Set.union q.us d.us; djns= [q :: djn]}
+    when Var.Set.is_empty xs ->
+      {d with us= Var.Set.union q.us d.us; djns= [q :: djn]}
   | _ ->
-      { us= Set.union q1.us q2.us
+      { us= Var.Set.union q1.us q2.us
       ; xs= Var.Set.empty
       ; cong= Equality.true_
       ; pure= []
@@ -504,7 +512,7 @@ let or_ q1 q2 =
   [%Trace.retn fun {pf} q ->
     pf "%a" pp_raw q ;
     invariant q ;
-    assert (Set.equal q.us (Set.union q1.us q2.us))]
+    assert (Var.Set.equal q.us (Var.Set.union q1.us q2.us))]
 
 let orN = function
   | [] -> false_ Var.Set.empty
@@ -545,7 +553,7 @@ let subst sub q =
   let dom, eqs =
     Var.Subst.fold sub ~init:(Var.Set.empty, Term.true_)
       ~f:(fun var trm (dom, eqs) ->
-        ( Set.add dom var
+        ( Var.Set.add dom var
         , Term.and_ (Term.eq (Term.var var) (Term.var trm)) eqs ) )
   in
   exists dom (and_ eqs q)
@@ -553,7 +561,7 @@ let subst sub q =
   [%Trace.retn fun {pf} q' ->
     pf "%a" pp q' ;
     invariant q' ;
-    assert (Set.disjoint q'.us (Var.Subst.domain sub))]
+    assert (Var.Set.disjoint q'.us (Var.Subst.domain sub))]
 
 let seg pt =
   let us = fv_seg pt in
@@ -603,7 +611,7 @@ let pure_approx q =
 let fold_dnf ~conj ~disj sjn (xs, conjuncts) disjuncts =
   let rec add_disjunct pending_splits sjn (xs, conjuncts) disjuncts =
     let ys, sjn = bind_exists sjn ~wrt:xs in
-    let xs = Set.union ys xs in
+    let xs = Var.Set.union ys xs in
     let djns = sjn.djns in
     let sjn = {sjn with djns= []} in
     split_case
@@ -638,7 +646,7 @@ let rec norm_ s q =
   let q =
     map q ~f_sjn:(norm_ s) ~f_cong:Fn.id ~f_trm:(Equality.Subst.subst s)
   in
-  let xs, cong = Equality.apply_subst (Set.union q.us q.xs) s q.cong in
+  let xs, cong = Equality.apply_subst (Var.Set.union q.us q.xs) s q.cong in
   exists_fresh xs {q with cong}
   |>
   [%Trace.retn fun {pf} q' -> pf "%a" pp_raw q' ; invariant q']
@@ -657,19 +665,19 @@ let rec freshen_nested_xs q =
   ;
   (* trim xs to those that appear in the stem and sink the rest *)
   let fv_stem = fv {q with xs= Var.Set.empty; djns= []} in
-  let xs_sink, xs = Set.diff_inter q.xs fv_stem in
+  let xs_sink, xs = Var.Set.diff_inter q.xs fv_stem in
   let xs_below, djns =
     List.fold_map ~init:Var.Set.empty q.djns ~f:(fun xs_below djn ->
         List.fold_map ~init:xs_below djn ~f:(fun xs_below dj ->
             (* quantify xs not in stem and freshen disjunct *)
             let dj' =
-              freshen_nested_xs (exists (Set.inter xs_sink dj.us) dj)
+              freshen_nested_xs (exists (Var.Set.inter xs_sink dj.us) dj)
             in
-            let xs_below' = Set.union xs_below dj'.xs in
+            let xs_below' = Var.Set.union xs_below dj'.xs in
             (xs_below', dj') ) )
   in
   (* rename xs to miss all xs in subformulas *)
-  freshen_xs {q with xs; djns} ~wrt:(Set.union q.us xs_below)
+  freshen_xs {q with xs; djns} ~wrt:(Var.Set.union q.us xs_below)
   |>
   [%Trace.retn fun {pf} q' -> pf "%a" pp q' ; invariant q']
 
@@ -678,7 +686,7 @@ let rec propagate_equality_ ancestor_vs ancestor_cong q =
     pf "(%a)@ %a" Equality.pp_classes ancestor_cong pp q]
   ;
   (* extend vocabulary with variables in scope above *)
-  let ancestor_vs = Set.union ancestor_vs (Set.union q.us q.xs) in
+  let ancestor_vs = Var.Set.union ancestor_vs (Var.Set.union q.us q.xs) in
   (* decompose formula *)
   let xs, stem, djns =
     (q.xs, {q with us= ancestor_vs; xs= emp.xs; djns= emp.djns}, q.djns)
@@ -695,10 +703,10 @@ let rec propagate_equality_ ancestor_vs ancestor_cong q =
          in
          let new_xs, djn_cong = Equality.orN ancestor_vs dj_congs in
          (* hoist xs appearing in disjunction's equality relation *)
-         let djn_xs = Set.diff (Equality.fv djn_cong) q'.us in
+         let djn_xs = Var.Set.diff (Equality.fv djn_cong) q'.us in
          let djn = List.map ~f:(elim_exists djn_xs) djn in
          let cong_djn = and_cong_ djn_cong (orN djn) in
-         assert (is_false cong_djn || Set.is_subset new_xs ~of_:djn_xs) ;
+         assert (is_false cong_djn || Var.Set.is_subset new_xs ~of_:djn_xs) ;
          star (exists djn_xs cong_djn) q' ))
   |>
   [%Trace.retn fun {pf} q' -> pf "%a" pp q' ; invariant q']
@@ -717,16 +725,17 @@ let pp_vss fs vss =
     vss
 
 let remove_absent_xs ks q =
-  let ks = Set.inter ks q.xs in
-  if Set.is_empty ks then q
+  let ks = Var.Set.inter ks q.xs in
+  if Var.Set.is_empty ks then q
   else
-    let xs = Set.diff q.xs ks in
+    let xs = Var.Set.diff q.xs ks in
     let djns =
       let rec trim_ks ks djns =
         List.map djns ~f:(fun djn ->
             List.map djn ~f:(fun sjn ->
-                {sjn with us= Set.diff sjn.us ks; djns= trim_ks ks sjn.djns}
-            ) )
+                { sjn with
+                  us= Var.Set.diff sjn.us ks
+                ; djns= trim_ks ks sjn.djns } ) )
       in
       trim_ks ks q.djns
     in
@@ -740,7 +749,7 @@ let rec simplify_ us rev_xss q =
   let q =
     exists q.xs
       (starN
-         ( {q with us= Set.union q.us q.xs; xs= emp.xs; djns= []}
+         ( {q with us= Var.Set.union q.us q.xs; xs= emp.xs; djns= []}
          :: List.map q.djns ~f:(fun djn ->
                 orN (List.map djn ~f:(fun sjn -> simplify_ us rev_xss sjn))
             ) ))
@@ -755,7 +764,7 @@ let rec simplify_ us rev_xss q =
     let q = norm subst q in
     (* reconjoin only non-redundant equations *)
     let removed =
-      Set.diff
+      Var.Set.diff
         (Var.Set.union_list rev_xss)
         (fv ~ignore_cong:() (elim_exists q.xs q))
     in
diff --git a/sledge/lib/solver.ml b/sledge/lib/solver.ml
index c3d83d559..7ed13ab43 100644
--- a/sledge/lib/solver.ml
+++ b/sledge/lib/solver.ml
@@ -69,7 +69,7 @@ end = struct
     Format.fprintf fs "@[<hv>%s %a@ | %a@ @[\\- %a%a@]@]"
       (if pgs then "t" else "f")
       Sh.pp com Sh.pp min Var.Set.pp_xs xs
-      (Sh.pp_diff_eq ~us:(Set.union min.us sub.us) ~xs min.cong)
+      (Sh.pp_diff_eq ~us:(Var.Set.union min.us sub.us) ~xs min.cong)
       sub
 
   let invariant g =
@@ -77,11 +77,11 @@ end = struct
     @@ fun () ->
     try
       let {us; com; min; xs; sub; zs; pgs= _} = g in
-      assert (Set.equal us com.us) ;
-      assert (Set.equal us min.us) ;
-      assert (Set.equal (Set.union us xs) sub.us) ;
-      assert (Set.disjoint us xs) ;
-      assert (Set.is_subset zs ~of_:(Set.union us xs))
+      assert (Var.Set.equal us com.us) ;
+      assert (Var.Set.equal us min.us) ;
+      assert (Var.Set.equal (Var.Set.union us xs) sub.us) ;
+      assert (Var.Set.disjoint us xs) ;
+      assert (Var.Set.is_subset zs ~of_:(Var.Set.union us xs))
     with exc -> [%Trace.info "%a" pp g] ; raise exc
 
   let with_ ?us ?com ?min ?xs ?sub ?zs ?pgs g =
@@ -91,11 +91,13 @@ end = struct
       let us = Option.value us ~default:Var.Set.empty in
       let us =
         Option.fold
-          ~f:(fun us sub -> Set.union (Set.diff sub.Sh.us xs) us)
+          ~f:(fun us sub -> Var.Set.union (Var.Set.diff sub.Sh.us xs) us)
           sub ~init:us
       in
       let union_us q_opt us' =
-        Option.fold ~f:(fun us' q -> Set.union q.Sh.us us') q_opt ~init:us'
+        Option.fold
+          ~f:(fun us' q -> Var.Set.union q.Sh.us us')
+          q_opt ~init:us'
       in
       union_us com (union_us min us)
     in
@@ -104,10 +106,10 @@ end = struct
     let xs, sub, zs =
       match sub with
       | Some sub ->
-          let sub = Sh.extend_us (Set.union new_us xs) sub in
+          let sub = Sh.extend_us (Var.Set.union new_us xs) sub in
           let ys, sub = Sh.bind_exists sub ~wrt:xs in
-          let xs = Set.union xs ys in
-          let zs = Set.union zs ys in
+          let xs = Var.Set.union xs ys in
+          let zs = Var.Set.union zs ys in
           (xs, sub, zs)
       | None ->
           let sub = Sh.extend_us new_us (Option.value sub ~default:g.sub) in
@@ -131,8 +133,8 @@ open Goal
 
 let fresh_var name vs zs ~wrt =
   let v, wrt = Var.fresh name ~wrt in
-  let vs = Set.add vs v in
-  let zs = Set.add zs v in
+  let vs = Var.Set.add vs v in
+  let zs = Var.Set.add zs v in
   let v = Term.var v in
   (v, vs, zs, wrt)
 
@@ -141,21 +143,22 @@ let trace (k : Trace.pf -> _) = [%Trace.infok k]
 
 let excise_exists goal =
   trace (fun {pf} -> pf "@[<2>excise_exists@ %a@]" pp goal) ;
-  if Set.is_empty goal.xs then goal
+  if Var.Set.is_empty goal.xs then goal
   else
     let solutions_for_xs =
       let xs =
-        Set.diff goal.xs (Sh.fv ~ignore_cong:() (Sh.with_pure [] goal.sub))
+        Var.Set.diff goal.xs
+          (Sh.fv ~ignore_cong:() (Sh.with_pure [] goal.sub))
       in
       Equality.solve_for_vars [Var.Set.empty; goal.us; xs] goal.sub.cong
     in
     if Equality.Subst.is_empty solutions_for_xs then goal
     else
       let removed =
-        Set.diff goal.xs
+        Var.Set.diff goal.xs
           (Sh.fv ~ignore_cong:() (Sh.norm solutions_for_xs goal.sub))
       in
-      if Set.is_empty removed then goal
+      if Var.Set.is_empty removed then goal
       else
         let _, removed, witnesses =
           Equality.Subst.partition_valid removed solutions_for_xs
@@ -165,8 +168,8 @@ let excise_exists goal =
           excise (fun {pf} ->
               pf "@[<2>excise_exists @[%a%a@]@]" Var.Set.pp_xs removed
                 Equality.Subst.pp witnesses ) ;
-          let us = Set.union goal.us removed in
-          let xs = Set.diff goal.xs removed in
+          let us = Var.Set.union goal.us removed in
+          let xs = Var.Set.diff goal.xs removed in
           let min = Sh.and_subst witnesses goal.min in
           goal |> with_ ~us ~min ~xs ~pgs:true )
 
@@ -234,9 +237,9 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n
   let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
   let {Sh.bas= b'; len= m'; siz= n; arr= a'} = ssg in
   let o_n = Term.integer o_n in
-  let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in
+  let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Var.Set.union us xs) in
   let a1, us, zs, _ = fresh_var "a1" us zs ~wrt in
-  let xs = Set.diff xs (Term.fv n) in
+  let xs = Var.Set.diff xs (Term.fv n) in
   let com = Sh.star (Sh.seg {msg with siz= n; arr= a0}) com in
   let min =
     Sh.and_
@@ -276,7 +279,7 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o
   let n_o = Term.integer n_o in
   let com = Sh.star (Sh.seg msg) com in
   let min = Sh.rem_seg msg min in
-  let a1', xs, zs, _ = fresh_var "a1" xs zs ~wrt:(Set.union us xs) in
+  let a1', xs, zs, _ = fresh_var "a1" xs zs ~wrt:(Var.Set.union us xs) in
   let sub =
     Sh.and_ (Term.eq b b')
       (Sh.and_ (Term.eq m m')
@@ -310,9 +313,9 @@ let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
   let l_k = Term.integer l_k in
-  let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in
+  let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Var.Set.union us xs) in
   let a1, us, zs, _ = fresh_var "a1" us zs ~wrt in
-  let xs = Set.diff xs (Term.fv n) in
+  let xs = Var.Set.diff xs (Term.fv n) in
   let com =
     Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; arr= a1}) com
   in
@@ -354,10 +357,10 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   let l_k = Term.integer l_k in
   let ko_ln = Term.integer ko_ln in
   let ln = Term.add l n in
-  let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in
+  let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Var.Set.union us xs) in
   let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in
   let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in
-  let xs = Set.diff xs (Set.union (Term.fv l) (Term.fv n)) in
+  let xs = Var.Set.diff xs (Var.Set.union (Term.fv l) (Term.fv n)) in
   let com =
     Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; arr= a1}) com
   in
@@ -402,10 +405,10 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   let ko_l = Term.integer ko_l in
   let ln_ko = Term.integer ln_ko in
   let ko = Term.add k o in
-  let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in
+  let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Var.Set.union us xs) in
   let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in
   let a2', xs, zs, _ = fresh_var "a2" xs zs ~wrt in
-  let xs = Set.diff xs (Term.fv l) in
+  let xs = Var.Set.diff xs (Term.fv l) in
   let com =
     Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= ko_l; arr= a1}) com
   in
@@ -449,7 +452,7 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
   let {Sh.bas= b; len= m; siz= o; arr= a} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
   let k_l = Term.integer k_l in
-  let a0', xs, zs, _ = fresh_var "a0" xs zs ~wrt:(Set.union us xs) in
+  let a0', xs, zs, _ = fresh_var "a0" xs zs ~wrt:(Var.Set.union us xs) in
   let com = Sh.star (Sh.seg msg) com in
   let min = Sh.rem_seg msg min in
   let sub =
@@ -488,7 +491,7 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
   let k_l = Term.integer k_l in
   let ln_ko = Term.integer ln_ko in
   let ko = Term.add k o in
-  let a0', xs, zs, wrt = fresh_var "a0" xs zs ~wrt:(Set.union us xs) in
+  let a0', xs, zs, wrt = fresh_var "a0" xs zs ~wrt:(Var.Set.union us xs) in
   let a2', xs, zs, _ = fresh_var "a2" xs zs ~wrt in
   let com = Sh.star (Sh.seg msg) com in
   let min = Sh.rem_seg msg min in
@@ -530,7 +533,7 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
   let ln_k = Term.integer ln_k in
   let ko_ln = Term.integer ko_ln in
   let ln = Term.add l n in
-  let a0', xs, zs, wrt = fresh_var "a0" xs zs ~wrt:(Set.union us xs) in
+  let a0', xs, zs, wrt = fresh_var "a0" xs zs ~wrt:(Var.Set.union us xs) in
   let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in
   let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in
   let com =
@@ -644,7 +647,7 @@ let excise_heap ({min; sub} as goal) =
 
 let rec excise ({min; xs; sub; zs; pgs} as goal) =
   [%Trace.info "@[<2>excise@ %a@]" pp goal] ;
-  if Sh.is_false min then Some (Sh.false_ (Set.diff sub.us zs))
+  if Sh.is_false min then Some (Sh.false_ (Var.Set.diff sub.us zs))
   else if Sh.is_emp sub then Some (Sh.exists zs (Sh.extend_us xs min))
   else if Sh.is_false sub then None
   else if pgs then
@@ -657,7 +660,7 @@ let excise_dnf : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option =
   let dnf_minuend = Sh.dnf minuend in
   let dnf_subtrahend = Sh.dnf subtrahend in
   List.fold_option dnf_minuend
-    ~init:(Sh.false_ (Set.union minuend.us xs))
+    ~init:(Sh.false_ (Var.Set.union minuend.us xs))
     ~f:(fun remainders minuend ->
       ([%Trace.call fun {pf} -> pf "@[<2>minuend@ %a@]" Sh.pp minuend]
       ;
@@ -683,16 +686,16 @@ let infer_frame : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option =
     pf "@[<hv>%a@ \\- %a%a@]" Sh.pp minuend Var.Set.pp_xs xs Sh.pp
       subtrahend]
   ;
-  assert (Set.disjoint minuend.us xs) ;
-  assert (Set.is_subset xs ~of_:subtrahend.us) ;
-  assert (Set.is_subset (Set.diff subtrahend.us xs) ~of_:minuend.us) ;
+  assert (Var.Set.disjoint minuend.us xs) ;
+  assert (Var.Set.is_subset xs ~of_:subtrahend.us) ;
+  assert (Var.Set.is_subset (Var.Set.diff subtrahend.us xs) ~of_:minuend.us) ;
   excise_dnf minuend xs subtrahend
   |>
   [%Trace.retn fun {pf} r ->
     pf "%a" (Option.pp "%a" Sh.pp) r ;
     Option.iter r ~f:(fun frame ->
-        let lost = Set.diff (Set.union minuend.us xs) frame.us in
-        let gain = Set.diff frame.us (Set.union minuend.us xs) in
-        assert (Set.is_empty lost || fail "lost: %a" Var.Set.pp lost ()) ;
-        assert (Set.is_empty gain || fail "gained: %a" Var.Set.pp gain ())
-    )]
+        let lost = Var.Set.diff (Var.Set.union minuend.us xs) frame.us in
+        let gain = Var.Set.diff frame.us (Var.Set.union minuend.us xs) in
+        assert (Var.Set.is_empty lost || fail "lost: %a" Var.Set.pp lost ()) ;
+        assert (
+          Var.Set.is_empty gain || fail "gained: %a" Var.Set.pp gain () ) )]
diff --git a/sledge/lib/term.ml b/sledge/lib/term.ml
index 499131931..9fc81ab99 100644
--- a/sledge/lib/term.ml
+++ b/sledge/lib/term.ml
@@ -118,6 +118,12 @@ type _t = T0.t
 include T
 module Map = Map.Make (T)
 
+module Set = struct
+  include Set.Make (T)
+
+  let t_of_sexp = t_of_sexp T.t_of_sexp
+end
+
 let empty_qset = Qset.empty (module T)
 
 let fix (f : (t -> 'a as 'f) -> 'f) (bot : 'f) (e : t) : 'a =
@@ -316,11 +322,7 @@ module Var = struct
   module Map = Map
 
   module Set = struct
-    include (
-      Set :
-        module type of Set with type ('elt, 'cmp) t := ('elt, 'cmp) Set.t )
-
-    type t = Set.M(T).t [@@deriving compare, equal, sexp]
+    include Set
 
     let pp vs = Set.pp pp_t vs
     let ppx strength vs = Set.pp (ppx strength) vs
@@ -328,13 +330,6 @@ module Var = struct
     let pp_xs fs xs =
       if not (is_empty xs) then
         Format.fprintf fs "@<2>∃ @[%a@] .@;<1 2>" pp xs
-
-    let empty = Set.empty (module T)
-    let of_ = Set.add empty
-    let of_option = Option.fold ~f:Set.add ~init:empty
-    let of_list = Set.of_list (module T)
-    let of_vector = Set.of_vector (module T)
-    let union_list = Set.union_list (module T)
   end
 
   let invariant x =
@@ -415,7 +410,7 @@ module Var = struct
     let apply_set sub vs =
       Map.fold sub ~init:vs ~f:(fun ~key ~data vs ->
           let vs' = Set.remove vs key in
-          if Set.to_tree vs' == Set.to_tree vs then vs
+          if vs' == vs then vs
           else (
             assert (not (Set.equal vs' vs)) ;
             Set.add vs' data ) )
diff --git a/sledge/lib/term.mli b/sledge/lib/term.mli
index a60722291..73da97c60 100644
--- a/sledge/lib/term.mli
+++ b/sledge/lib/term.mli
@@ -93,25 +93,18 @@ module Var : sig
 
   type strength = t -> [`Universal | `Existential | `Anonymous] option
 
-  module Set : sig
-    type var := t
+  module Map : Map.S with type key := t
 
-    type t = (var, comparator_witness) Set.t
-    [@@deriving compare, equal, sexp]
+  module Set : sig
+    include Set.S with type elt := t
 
+    val sexp_of_t : t -> Sexp.t
+    val t_of_sexp : Sexp.t -> t
     val ppx : strength -> t pp
     val pp : t pp
     val pp_xs : t pp
-    val empty : t
-    val of_ : var -> t
-    val of_option : var option -> t
-    val of_list : var list -> t
-    val of_vector : var vector -> t
-    val union_list : t list -> t
   end
 
-  module Map : Map.S with type key := t
-
   val pp : t pp
 
   include Invariant.S with type t := t