From ec4cb61db3b6da333d7db31dece106015bca70a4 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Sun, 25 Oct 2020 16:01:22 -0700
Subject: [PATCH] [sledge] Shift to a more standard Set API

Summary:
The changes in set_intf.ml dictate the rest. The previous API
minimized changes when changing the backing implementation. But that
API is hostile toward composition, partial application, and
state-passing style code.

Reviewed By: jvillard

Differential Revision: D24306089

fbshipit-source-id: 00a09f486
---
 sledge/cli/domain_itv.ml          |  7 ++++---
 sledge/cli/sledge_cli.ml          |  2 +-
 sledge/nonstdlib/set.ml           | 10 ++++-----
 sledge/nonstdlib/set_intf.ml      | 12 ++++++-----
 sledge/src/domain_sh.ml           |  9 ++++----
 sledge/src/domain_used_globals.ml |  2 +-
 sledge/src/exec.ml                |  4 ++--
 sledge/src/fol.ml                 | 20 +++++++++---------
 sledge/src/llair/llair.ml         |  6 +++---
 sledge/src/llair_to_Fol.ml        |  7 ++++---
 sledge/src/ses/equality.ml        | 35 +++++++++++++++----------------
 sledge/src/ses/term.ml            | 19 ++++++++---------
 sledge/src/ses/var0.ml            | 14 ++++++-------
 sledge/src/sh.ml                  | 26 ++++++++++++-----------
 sledge/src/solver.ml              | 10 ++++-----
 15 files changed, 93 insertions(+), 90 deletions(-)

diff --git a/sledge/cli/domain_itv.ml b/sledge/cli/domain_itv.ml
index 469887e9f..6fd0cbe24 100644
--- a/sledge/cli/domain_itv.ml
+++ b/sledge/cli/domain_itv.ml
@@ -177,8 +177,9 @@ let exec_move q move_vec =
   let defs, uses =
     IArray.fold move_vec ~init:(Llair.Reg.Set.empty, Llair.Reg.Set.empty)
       ~f:(fun (defs, uses) (r, e) ->
-        ( Llair.Reg.Set.add defs r
-        , Llair.Exp.fold_regs e ~init:uses ~f:Llair.Reg.Set.add ) )
+        ( Llair.Reg.Set.add r defs
+        , Llair.Exp.fold_regs e ~init:uses ~f:(Fun.flip Llair.Reg.Set.add)
+        ) )
   in
   assert (Llair.Reg.Set.disjoint defs uses) ;
   IArray.fold move_vec ~init:q ~f:(fun a (r, e) -> assign r e a)
@@ -234,7 +235,7 @@ let recursion_beyond_bound = `prune
 (** existentially quantify locals *)
 let post locals _ (q : t) =
   let locals =
-    Llair.Reg.Set.fold locals ~init:[] ~f:(fun a r ->
+    Llair.Reg.Set.fold locals ~init:[] ~f:(fun r a ->
         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/cli/sledge_cli.ml b/sledge/cli/sledge_cli.ml
index bbd070a45..34ac51cdb 100644
--- a/sledge/cli/sledge_cli.ml
+++ b/sledge/cli/sledge_cli.ml
@@ -96,7 +96,7 @@ let used_globals pgm preanalyze : Domain_used_globals.r =
   else
     Declared
       (IArray.fold pgm.globals ~init:Llair.Reg.Set.empty ~f:(fun acc g ->
-           Llair.Reg.Set.add acc g.reg ))
+           Llair.Reg.Set.add g.reg acc ))
 
 let analyze =
   let%map_open bound =
diff --git a/sledge/nonstdlib/set.ml b/sledge/nonstdlib/set.ml
index 674e7e048..5a29c7a92 100644
--- a/sledge/nonstdlib/set.ml
+++ b/sledge/nonstdlib/set.ml
@@ -30,8 +30,8 @@ end) : S with type elt = Elt.t = struct
   let of_ = S.singleton
   let of_option xo = Option.map_or ~f:S.singleton xo ~default:empty
   let of_list = S.of_list
-  let add s x = S.add x s
-  let add_option xo s = Option.fold ~f:add ~init:s xo
+  let add x s = S.add x s
+  let add_option xo s = Option.fold ~f:(Fun.flip add) ~init:s xo
   let add_list xs s = S.add_list s xs
   let diff = S.diff
   let inter = S.inter
@@ -41,7 +41,7 @@ end) : S with type elt = Elt.t = struct
   let is_empty = S.is_empty
   let cardinal = S.cardinal
   let mem s x = S.mem x s
-  let is_subset s ~of_:t = S.subset s t
+  let subset s ~of_:t = S.subset s t
   let disjoint = S.disjoint
   let max_elt = S.max_elt_opt
 
@@ -73,13 +73,13 @@ end) : S with type elt = Elt.t = struct
     let elt = choose_exn s in
     (elt, S.remove elt s)
 
-  let elements = S.elements
   let map s ~f = S.map f s
   let filter s ~f = S.filter f s
   let iter s ~f = S.iter f s
   let exists s ~f = S.exists f s
   let for_all s ~f = S.for_all f s
-  let fold s ~init ~f = S.fold (fun x a -> f a x) s init
+  let fold s ~init ~f = S.fold f s init
+  let to_iter = S.to_iter
 
   let pp ?pre ?suf ?(sep = (",@ " : (unit, unit) fmt)) pp_elt fs x =
     List.pp ?pre ?suf sep pp_elt fs (S.elements x)
diff --git a/sledge/nonstdlib/set_intf.ml b/sledge/nonstdlib/set_intf.ml
index 386374942..87d381bb5 100644
--- a/sledge/nonstdlib/set_intf.ml
+++ b/sledge/nonstdlib/set_intf.ml
@@ -23,7 +23,7 @@ module type S = sig
   val of_ : elt -> t
   val of_option : elt option -> t
   val of_list : elt list -> t
-  val add : t -> elt -> t
+  val add : elt -> t -> t
   val add_option : elt option -> t -> t
   val add_list : elt list -> t -> t
   val diff : t -> t -> t
@@ -37,7 +37,7 @@ module type S = sig
   val is_empty : t -> bool
   val cardinal : t -> int
   val mem : t -> elt -> bool
-  val is_subset : t -> of_:t -> bool
+  val subset : t -> of_:t -> bool
   val disjoint : t -> t -> bool
   val max_elt : t -> elt option
   val only_elt : t -> elt option
@@ -45,8 +45,6 @@ module type S = sig
   val pop_exn : t -> elt * t
   (** Find and remove an unspecified element. [O(1)]. *)
 
-  val elements : t -> elt list
-
   (** {1 Transform} *)
 
   val map : t -> f:(elt -> elt) -> t
@@ -57,7 +55,11 @@ module type S = sig
   val iter : t -> f:(elt -> unit) -> unit
   val exists : t -> f:(elt -> bool) -> bool
   val for_all : t -> f:(elt -> bool) -> bool
-  val fold : t -> init:'a -> f:('a -> elt -> 'a) -> 'a
+  val fold : t -> init:'s -> f:(elt -> 's -> 's) -> 's
+
+  (** {1 Convert} *)
+
+  val to_iter : t -> elt iter
 
   (** {1 Pretty-print} *)
 
diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index 234438462..0f6667cc4 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -78,7 +78,7 @@ let term_eq_class_has_only_vars_in fvs ctx term =
       Context.pp ctx Term.pp term]
   ;
   let term_has_only_vars_in fvs term =
-    Var.Set.is_subset (Term.fv term) ~of_:fvs
+    Var.Set.subset (Term.fv term) ~of_:fvs
   in
   let term_eq_class = Context.class_of ctx term in
   List.exists ~f:(term_has_only_vars_in fvs) term_eq_class
@@ -170,9 +170,8 @@ let call ~summaries ~globals ~actuals ~areturn ~formals ~freturn ~locals q =
   let entry = and_eqs shadow formals actuals q' in
   (* note: locals and formals are in scope *)
   assert (
-    Var.Set.is_subset
-      (Var.Set.add_list formals freturn_locals)
-      ~of_:entry.us ) ;
+    Var.Set.subset (Var.Set.add_list formals freturn_locals) ~of_:entry.us
+  ) ;
   (* simplify *)
   let entry = simplify entry in
   ( if not summaries then (entry, {areturn; unshadow; frame= Sh.emp})
@@ -258,7 +257,7 @@ let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) =
   let foot = Sh.exists locals entry in
   let foot, subst = Sh.freshen ~wrt:(Var.Set.union foot.us post.us) foot in
   let restore_formals q =
-    Var.Set.fold formals ~init:q ~f:(fun q var ->
+    Var.Set.fold formals ~init:q ~f:(fun var q ->
         let var = Term.var var in
         let renamed_var = Term.rename subst var in
         Sh.and_ (Formula.eq renamed_var var) q )
diff --git a/sledge/src/domain_used_globals.ml b/sledge/src/domain_used_globals.ml
index 54edcb86e..3764ea3da 100644
--- a/sledge/src/domain_used_globals.ml
+++ b/sledge/src/domain_used_globals.ml
@@ -25,7 +25,7 @@ let retn _ _ from_call post = Llair.Reg.Set.union from_call post
 let dnf t = [t]
 
 let add_if_global gs v =
-  if Llair.Reg.is_global v then Llair.Reg.Set.add gs v else gs
+  if Llair.Reg.is_global v then Llair.Reg.Set.add v gs else gs
 
 let used_globals ?(init = empty) exp =
   Llair.Exp.fold_regs exp ~init ~f:add_if_global
diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml
index d96ae5e70..df71c2f25 100644
--- a/sledge/src/exec.ml
+++ b/sledge/src/exec.ml
@@ -52,7 +52,7 @@ end = struct
 
   let var nam {wrt; xs} =
     let x, wrt = Var.fresh nam ~wrt in
-    let xs = Var.Set.add xs x in
+    let xs = Var.Set.add x xs in
     return (Term.var x) {wrt; xs}
 
   let seg ?bas ?len ?siz ?seq loc =
@@ -104,7 +104,7 @@ let move_spec reg_exps =
   let ws, rs =
     IArray.fold reg_exps ~init:(Var.Set.empty, Var.Set.empty)
       ~f:(fun (ws, rs) (reg, exp) ->
-        (Var.Set.add ws reg, Var.Set.union rs (Term.fv exp)) )
+        (Var.Set.add reg ws, Var.Set.union rs (Term.fv exp)) )
   in
   let+ sub, ms = Fresh.assign ~ws ~rs in
   let post =
diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 7d070e326..6925954e4 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -351,8 +351,8 @@ let pp = ppx (fun _ -> None)
 (** fold_vars *)
 
 let fold_pos_neg ~pos ~neg ~init ~f =
-  let f_not s p = f s (_Not p) in
-  Fmls.fold ~init:(Fmls.fold ~init ~f pos) ~f:f_not neg
+  let f_not p s = f s (_Not p) in
+  Fmls.fold ~init:(Fmls.fold ~init ~f:(Fun.flip f) pos) ~f:f_not neg
 
 let rec fold_vars_t e ~init ~f =
   match e with
@@ -718,7 +718,7 @@ module Term = struct
 
   (** Query *)
 
-  let fv e = fold_vars e ~f:Var.Set.add ~init:Var.Set.empty
+  let fv e = fold_vars e ~f:(Fun.flip Var.Set.add) ~init:Var.Set.empty
 end
 
 (*
@@ -773,7 +773,7 @@ module Formula = struct
 
   (** Query *)
 
-  let fv e = fold_vars_f e ~f:Var.Set.add ~init:Var.Set.empty
+  let fv e = fold_vars_f e ~f:(Fun.flip Var.Set.add) ~init:Var.Set.empty
 
   (** Traverse *)
 
@@ -858,8 +858,8 @@ let v_to_ses : var -> Ses.Var.t =
 
 let vs_to_ses : Var.Set.t -> Ses.Var.Set.t =
  fun vs ->
-  Var.Set.fold vs ~init:Ses.Var.Set.empty ~f:(fun vs v ->
-      Ses.Var.Set.add vs (v_to_ses v) )
+  Var.Set.fold vs ~init:Ses.Var.Set.empty ~f:(fun v vs ->
+      Ses.Var.Set.add (v_to_ses v) vs )
 
 let rec arith_to_ses poly =
   Arith.fold_monomials poly ~init:Ses.Term.zero ~f:(fun mono coeff e ->
@@ -941,8 +941,8 @@ let v_of_ses : Ses.Var.t -> var =
 
 let vs_of_ses : Ses.Var.Set.t -> Var.Set.t =
  fun vs ->
-  Ses.Var.Set.fold vs ~init:Var.Set.empty ~f:(fun vs v ->
-      Var.Set.add vs (v_of_ses v) )
+  Ses.Var.Set.fold vs ~init:Var.Set.empty ~f:(fun v vs ->
+      Var.Set.add (v_of_ses v) vs )
 
 let uap1 f = ap1t (fun x -> _Apply f [|x|])
 let uap2 f = ap2t (fun x y -> _Apply f [|x; y|])
@@ -960,7 +960,7 @@ and ap2_f mk_f mk_t a b = ap2 mk_f (fun x y -> `Fml (mk_t x y)) a b
 
 and apN mk_f mk_t mk_unit es =
   match
-    Ses.Term.Set.fold ~init:(None, None) es ~f:(fun (fs, ts) e ->
+    Ses.Term.Set.fold ~init:(None, None) es ~f:(fun e (fs, ts) ->
         match of_ses e with
         | `Fml f ->
             (Some (match fs with None -> f | Some g -> mk_f f g), ts)
@@ -1076,7 +1076,7 @@ module Context = struct
   let fold_vars ~init x ~f =
     Ses.Equality.fold_vars x ~init ~f:(fun s v -> f s (v_of_ses v))
 
-  let fv e = fold_vars e ~f:Var.Set.add ~init:Var.Set.empty
+  let fv e = fold_vars e ~f:(Fun.flip Var.Set.add) ~init:Var.Set.empty
   let is_empty x = Ses.Equality.is_true x
   let is_unsat x = Ses.Equality.is_false x
   let implies x b = Ses.Equality.implies x (f_to_ses b)
diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml
index b5af535b2..37013303f 100644
--- a/sledge/src/llair/llair.ml
+++ b/sledge/src/llair/llair.ml
@@ -261,10 +261,10 @@ module Inst = struct
     match inst with
     | Move {reg_exps; _} ->
         IArray.fold
-          ~f:(fun vs (reg, _) -> Reg.Set.add vs reg)
+          ~f:(fun vs (reg, _) -> Reg.Set.add reg vs)
           ~init:vs reg_exps
     | Load {reg; _} | Alloc {reg; _} | Nondet {reg= Some reg; _} ->
-        Reg.Set.add vs reg
+        Reg.Set.add reg vs
     | Store _ | Memcpy _ | Memmov _ | Memset _ | Free _
      |Nondet {reg= None; _}
      |Abort _ ->
@@ -549,7 +549,7 @@ let set_derived_metadata functions =
     let rec visit ancestors func src =
       if BlockQ.mem tips_to_roots src then ()
       else
-        let ancestors = Block_label.Set.add ancestors src in
+        let ancestors = Block_label.Set.add src ancestors in
         let jump jmp =
           if Block_label.Set.mem ancestors jmp.dst then
             jmp.retreating <- true
diff --git a/sledge/src/llair_to_Fol.ml b/sledge/src/llair_to_Fol.ml
index d30a44f87..ae03337d8 100644
--- a/sledge/src/llair_to_Fol.ml
+++ b/sledge/src/llair_to_Fol.ml
@@ -16,9 +16,10 @@ let reg r =
   let global = Llair.Reg.is_global r in
   Var.program ~name ~global
 
-let regs =
-  Llair.Reg.Set.fold ~init:Var.Set.empty ~f:(fun s r ->
-      Var.Set.add s (reg r) )
+let regs rs =
+  Llair.Reg.Set.fold
+    ~f:(fun r -> Var.Set.add (reg r))
+    rs ~init:Var.Set.empty
 
 let uap0 f = T.apply f [||]
 let uap1 f a = T.apply f [|a|]
diff --git a/sledge/src/ses/equality.ml b/sledge/src/ses/equality.ml
index 673ee3127..f2257500b 100644
--- a/sledge/src/ses/equality.ml
+++ b/sledge/src/ses/equality.ml
@@ -116,7 +116,7 @@ end = struct
 
   (** remove entries for vars *)
   let remove xs s =
-    Var.Set.fold ~f:(fun s x -> Term.Map.remove (Term.var x) s) ~init:s xs
+    Var.Set.fold ~f:(fun x s -> Term.Map.remove (Term.var x) s) xs ~init:s
 
   (** map over a subst, applying [f] to both domain and range, requires that
       [f] is injective and for any set of terms [E], [f\[E\]] is disjoint
@@ -212,7 +212,7 @@ let compose1 ?f ~var ~rep (us, xs, s) =
 
 let fresh name (us, xs, s) =
   let x, us = Var.fresh name ~wrt:us in
-  let xs = Var.Set.add xs x in
+  let xs = Var.Set.add x xs in
   (Term.var x, (us, xs, s))
 
 let solve_poly ?f p q s =
@@ -654,7 +654,7 @@ let rec and_term_ us e r =
   let eq_false b r = and_eq_ us b Term.false_ r in
   match (e : Term.t) with
   | Integer {data} -> if Z.is_false data then false_ else r
-  | And cs -> Term.Set.fold cs ~init:r ~f:(fun r e -> and_term_ us e r)
+  | And cs -> Term.Set.fold ~f:(and_term_ us) cs ~init:r
   | Ap2 (Eq, a, b) -> and_eq_ us a b r
   | Ap2 (Xor, Integer {data}, a) when Z.is_true data -> eq_false a r
   | Ap2 (Xor, a, Integer {data}) when Z.is_true data -> eq_false a r
@@ -703,11 +703,11 @@ let subst_invariant us s0 s =
         (* dom of new entries not ito us *)
         assert (
           Option.for_all ~f:(Term.equal data) (Subst.find key s0)
-          || not (Var.Set.is_subset (Term.fv key) ~of_:us) ) ;
+          || not (Var.Set.subset (Term.fv key) ~of_:us) ) ;
         (* rep not ito us implies trm not ito us *)
         assert (
-          Var.Set.is_subset (Term.fv data) ~of_:us
-          || not (Var.Set.is_subset (Term.fv key) ~of_:us) ) ) ;
+          Var.Set.subset (Term.fv data) ~of_:us
+          || not (Var.Set.subset (Term.fv key) ~of_:us) ) ) ;
     true )
 
 type 'a zom = Zero | One of 'a | Many
@@ -723,7 +723,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 Var.Set.is_subset (Term.fv solvable_subterm) ~of_:us -> zom
+      | zom when Var.Set.subset (Term.fv solvable_subterm) ~of_:us -> zom
       | One _ -> Many
       | Zero -> One solvable_subterm )
   in
@@ -740,8 +740,8 @@ let solve_seq_eq us e' f' subst =
   [%Trace.call fun {pf} -> pf "%a = %a" Term.pp e' Term.pp f']
   ;
   let f x u =
-    (not (Var.Set.is_subset (Term.fv x) ~of_:us))
-    && Var.Set.is_subset (Term.fv u) ~of_:us
+    (not (Var.Set.subset (Term.fv x) ~of_:us))
+    && Var.Set.subset (Term.fv u) ~of_:us
   in
   let solve_concat ms n a =
     let a, n =
@@ -835,7 +835,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 Var.Set.is_subset (Term.fv trm) ~of_:us then
+        if Var.Set.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}
@@ -899,7 +899,7 @@ let solve_class us us_xs ~key:rep ~data:cls (classes, subst) =
   ;
   let cls, cls_not_ito_us_xs =
     List.partition
-      ~f:(fun e -> Var.Set.is_subset (Term.fv e) ~of_:us_xs)
+      ~f:(fun e -> Var.Set.subset (Term.fv e) ~of_:us_xs)
       (rep :: cls)
   in
   let cls, subst = solve_interp_eqs us (cls, subst) in
@@ -957,8 +957,7 @@ 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 Var.Set.is_subset (Term.fv trm) ~of_:us ->
-                      Some trm
+                  | _ when Var.Set.subset (Term.fv trm) ~of_:us -> Some trm
                   | _ -> rep_ito_us )
             in
             Term.sized ~siz:(Term.seq_size_exn e) ~seq:rep_ito_us :: suffix ) )
@@ -973,7 +972,7 @@ let solve_concat_extracts r us x (classes, subst, us_xs) =
 
 let solve_for_xs r us xs (classes, subst, us_xs) =
   Var.Set.fold xs ~init:(classes, subst, us_xs)
-    ~f:(fun (classes, subst, us_xs) x ->
+    ~f:(fun x (classes, subst, us_xs) ->
       let x = Term.var x in
       if Subst.mem x subst then (classes, subst, us_xs)
       else solve_concat_extracts r us x (classes, subst, us_xs) )
@@ -1036,10 +1035,10 @@ let solve_for_vars vss r =
               let ks = Term.fv key in
               let ds = Term.fv data in
               if
-                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) )
+                Var.Set.subset ks ~of_:us_xs
+                && Var.Set.subset ds ~of_:us_xs
+                && ( Var.Set.subset ds ~of_:us
+                   || not (Var.Set.subset ks ~of_:us) )
               then `Stop true
               else `Continue us_xs )
             ~finish:(fun _ -> false) ) )]
diff --git a/sledge/src/ses/term.ml b/sledge/src/ses/term.ml
index 4a2b1f57c..acc3c1c42 100644
--- a/sledge/src/ses/term.ml
+++ b/sledge/src/ses/term.ml
@@ -566,7 +566,7 @@ let rec simp_and2 x y =
   (* e && e ==> e *)
   | _ when equal x y -> x
   | _ ->
-      let add s = function And cs -> Set.union s cs | c -> Set.add s c in
+      let add s = function And cs -> Set.union s cs | c -> Set.add c s in
       And (add (add Set.empty x) y)
 
 let simp_and xs = Set.fold xs ~init:true_ ~f:simp_and2
@@ -587,7 +587,7 @@ let rec simp_or2 x y =
   (* e || e ==> e *)
   | _ when equal x y -> x
   | _ ->
-      let add s = function Or cs -> Set.union s cs | c -> Set.add s c in
+      let add s = function Or cs -> Set.union s cs | c -> Set.add c s in
       Or (add (add Set.empty x) y)
 
 let simp_or xs = Set.fold xs ~init:false_ ~f:simp_or2
@@ -1041,15 +1041,15 @@ let disjuncts e =
     match e with
     | Or es ->
         let e0, e1N = Set.pop_exn es in
-        Set.fold e1N ~init:(disjuncts_ e0) ~f:(fun cs e ->
+        Set.fold e1N ~init:(disjuncts_ e0) ~f:(fun e cs ->
             Set.union cs (disjuncts_ e) )
     | Ap3 (Conditional, cnd, thn, els) ->
         Set.add
-          (Set.of_ (and_ (orN (disjuncts_ cnd)) (orN (disjuncts_ thn))))
           (and_ (orN (disjuncts_ (not_ cnd))) (orN (disjuncts_ els)))
+          (Set.of_ (and_ (orN (disjuncts_ cnd)) (orN (disjuncts_ thn))))
     | _ -> Set.of_ e
   in
-  Set.elements (disjuncts_ e)
+  Iter.to_list (Set.to_iter (disjuncts_ e))
 
 let rename f e =
   let f = (f : Var.t -> Var.t :> Var.t -> t) in
@@ -1102,7 +1102,7 @@ let fold e ~init:s ~f =
   | Ap3 (_, x, y, z) -> f z (f y (f x s))
   | ApN (_, xs) | Apply (_, xs) | PosLit (_, xs) | NegLit (_, xs) ->
       IArray.fold ~f:(fun s x -> f x s) xs ~init:s
-  | And args | Or args -> Set.fold ~f:(fun s e -> f e s) args ~init:s
+  | And args | Or args -> Set.fold ~f args ~init:s
   | Add args | Mul args -> Qset.fold ~f:(fun e _ s -> f e s) args ~init:s
   | Var _ | Integer _ | Rational _ | RecRecord _ -> s
 
@@ -1133,8 +1133,7 @@ let rec fold_terms e ~init:s ~f =
     | Ap3 (_, x, y, z) -> fold_terms f z (fold_terms f y (fold_terms f x s))
     | ApN (_, xs) | Apply (_, xs) | PosLit (_, xs) | NegLit (_, xs) ->
         IArray.fold ~f:(fun s x -> fold_terms f x s) xs ~init:s
-    | And args | Or args ->
-        Set.fold args ~init:s ~f:(fun s x -> fold_terms f x s)
+    | And args | Or args -> Set.fold args ~init:s ~f:(fold_terms f)
     | Add args | Mul args ->
         Qset.fold args ~init:s ~f:(fun arg _ s -> fold_terms f arg s)
     | Var _ | Integer _ | Rational _ | RecRecord _ -> s
@@ -1152,7 +1151,7 @@ let fold_vars e ~init ~f =
 
 (** Query *)
 
-let fv e = fold_vars e ~f:Var.Set.add ~init:Var.Set.empty
+let fv e = fold_vars e ~f:(Fun.flip Var.Set.add) ~init:Var.Set.empty
 let is_true = function Integer {data} -> Z.is_true data | _ -> false
 let is_false = function Integer {data} -> Z.is_false data | _ -> false
 
@@ -1169,7 +1168,7 @@ let rec height = function
   | ApN (_, v) | Apply (_, v) | PosLit (_, v) | NegLit (_, v) ->
       1 + IArray.fold v ~init:0 ~f:(fun m a -> max m (height a))
   | And bs | Or bs ->
-      1 + Set.fold bs ~init:0 ~f:(fun m a -> max m (height a))
+      1 + Set.fold bs ~init:0 ~f:(fun a m -> max m (height a))
   | Add qs | Mul qs ->
       1 + Qset.fold qs ~init:0 ~f:(fun a _ m -> max m (height a))
   | Integer _ | Rational _ | RecRecord _ -> 0
diff --git a/sledge/src/ses/var0.ml b/sledge/src/ses/var0.ml
index 7f3df66fa..3c6c03577 100644
--- a/sledge/src/ses/var0.ml
+++ b/sledge/src/ses/var0.ml
@@ -50,7 +50,7 @@ module Make (T : REPR) = struct
   let fresh name ~wrt =
     let max = match Set.max_elt wrt with None -> 0 | Some max -> id max in
     let x' = make ~id:(max + 1) ~name in
-    (x', Set.add wrt x')
+    (x', Set.add x' wrt)
 
   let program ~name ~global = make ~id:(if global then -1 else 0) ~name
   let identified ~name ~id = make ~id ~name
@@ -70,7 +70,7 @@ module Make (T : REPR) = struct
           ~f:(fun ~key ~data (domain, range) ->
             (* substs are injective *)
             assert (not (Set.mem range data)) ;
-            (Set.add domain key, Set.add range data) )
+            (Set.add key domain, Set.add data range) )
       in
       assert (Set.disjoint domain range)
 
@@ -85,10 +85,10 @@ module Make (T : REPR) = struct
         let wrt = Set.union wrt vs in
         let sub, rng, wrt =
           Set.fold dom ~init:(empty, Set.empty, wrt)
-            ~f:(fun (sub, rng, wrt) x ->
+            ~f:(fun x (sub, rng, wrt) ->
               let x', wrt = fresh (name x) ~wrt in
               let sub = Map.add_exn ~key:x ~data:x' sub in
-              let rng = Set.add rng x' in
+              let rng = Set.add x' rng in
               (sub, rng, wrt) )
         in
         ({sub; dom; rng}, wrt) )
@@ -99,11 +99,11 @@ module Make (T : REPR) = struct
 
     let domain sub =
       Map.fold sub ~init:Set.empty ~f:(fun ~key ~data:_ domain ->
-          Set.add domain key )
+          Set.add key domain )
 
     let range sub =
       Map.fold sub ~init:Set.empty ~f:(fun ~key:_ ~data range ->
-          Set.add range data )
+          Set.add data range )
 
     let invert sub =
       Map.fold sub ~init:empty ~f:(fun ~key ~data sub' ->
@@ -114,7 +114,7 @@ module Make (T : REPR) = struct
       Map.fold sub ~init:{sub; dom= Set.empty; rng= Set.empty}
         ~f:(fun ~key ~data z ->
           if Set.mem vs key then
-            {z with dom= Set.add z.dom key; rng= Set.add z.rng data}
+            {z with dom= Set.add key z.dom; rng= Set.add data z.rng}
           else (
             assert (
               (* all substs are injective, so the current mapping is the
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index dc6f15cd7..42fb1cb04 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -118,7 +118,7 @@ let rec var_strength_ xs m q =
 
 let var_strength ?(xs = Var.Set.empty) q =
   let m =
-    Var.Set.fold xs ~init:Var.Map.empty ~f:(fun m x ->
+    Var.Set.fold xs ~init:Var.Map.empty ~f:(fun x m ->
         Var.Map.add ~key:x ~data:`Existential m )
   in
   var_strength_ xs m q
@@ -258,12 +258,14 @@ let pp_djn fs d =
 let pp_raw fs q =
   pp_ ?var_strength:None Var.Set.empty Var.Set.empty Context.empty fs q
 
-let fv_seg seg = fold_vars_seg seg ~f:Var.Set.add ~init:Var.Set.empty
+let fv_seg seg =
+  fold_vars_seg seg ~f:(Fun.flip Var.Set.add) ~init:Var.Set.empty
 
 let fv ?ignore_ctx ?ignore_pure q =
   let rec fv_union init q =
     Var.Set.diff
-      (fold_vars ?ignore_ctx ?ignore_pure fv_union q ~init ~f:Var.Set.add)
+      (fold_vars ?ignore_ctx ?ignore_pure fv_union q ~init
+         ~f:(Fun.flip Var.Set.add))
       q.xs
   in
   fv_union Var.Set.empty q
@@ -280,7 +282,7 @@ let rec invariant q =
       || fail "inter: @[%a@]@\nq: @[%a@]" Var.Set.pp (Var.Set.inter us xs)
            pp q () ) ;
     assert (
-      Var.Set.is_subset (fv q) ~of_:us
+      Var.Set.subset (fv q) ~of_:us
       || fail "unbound but free: %a" Var.Set.pp (Var.Set.diff (fv q) us) ()
     ) ;
     Context.invariant ctx ;
@@ -294,7 +296,7 @@ let rec invariant q =
     List.iter heap ~f:invariant_seg ;
     List.iter djns ~f:(fun djn ->
         List.iter djn ~f:(fun sjn ->
-            assert (Var.Set.is_subset sjn.us ~of_:(Var.Set.union us xs)) ;
+            assert (Var.Set.subset sjn.us ~of_:(Var.Set.union us xs)) ;
             invariant sjn ) )
   with exc ->
     [%Trace.info "%a" pp q] ;
@@ -314,7 +316,7 @@ let rec apply_subst sub q =
 and rename_ Var.Subst.{sub; dom; rng} q =
   [%Trace.call fun {pf} ->
     pf "@[%a@]@ %a" Var.Subst.pp sub pp q ;
-    assert (Var.Set.is_subset dom ~of_:q.us)]
+    assert (Var.Set.subset dom ~of_:q.us)]
   ;
   ( if Var.Subst.is_empty sub then q
   else
@@ -342,7 +344,7 @@ and rename sub q =
 and freshen_xs q ~wrt =
   [%Trace.call fun {pf} ->
     pf "{@[%a@]}@ %a" Var.Set.pp wrt pp q ;
-    assert (Var.Set.is_subset q.us ~of_:wrt)]
+    assert (Var.Set.subset q.us ~of_:wrt)]
   ;
   let Var.Subst.{sub; dom; rng}, _ = Var.Subst.freshen q.xs ~wrt in
   ( if Var.Subst.is_empty sub then q
@@ -373,7 +375,7 @@ let freshen q ~wrt =
   [%Trace.retn fun {pf} (q', _) ->
     pf "%a" pp q' ;
     invariant q' ;
-    assert (Var.Set.is_subset wrt ~of_:q'.us) ;
+    assert (Var.Set.subset wrt ~of_:q'.us) ;
     assert (Var.Set.disjoint wrt (fv q'))]
 
 let bind_exists q ~wrt =
@@ -404,7 +406,7 @@ let exists xs q =
   [%Trace.call fun {pf} -> pf "{@[%a@]}@ %a" Var.Set.pp xs pp q]
   ;
   assert (
-    Var.Set.is_subset xs ~of_:q.us
+    Var.Set.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
@@ -423,7 +425,7 @@ let elim_exists xs q =
 
 (** conjoin an FOL context assuming vocabulary is compatible *)
 let and_ctx_ ctx q =
-  assert (Var.Set.is_subset (Context.fv ctx) ~of_:q.us) ;
+  assert (Var.Set.subset (Context.fv ctx) ~of_:q.us) ;
   let xs, ctx = Context.union (Var.Set.union q.us q.xs) q.ctx ctx in
   if Context.is_unsat ctx then false_ q.us else exists_fresh xs {q with ctx}
 
@@ -546,7 +548,7 @@ let subst sub q =
   let dom, eqs =
     Var.Subst.fold sub ~init:(Var.Set.empty, Formula.tt)
       ~f:(fun var trm (dom, eqs) ->
-        ( Var.Set.add dom var
+        ( Var.Set.add var dom
         , Formula.and_ (Formula.eq (Term.var var) (Term.var trm)) eqs ) )
   in
   exists dom (and_ eqs q)
@@ -697,7 +699,7 @@ let rec propagate_context_ ancestor_vs ancestor_ctx q =
          let djn_xs = Var.Set.diff (Context.fv djn_ctx) q'.us in
          let djn = List.map ~f:(elim_exists djn_xs) djn in
          let ctx_djn = and_ctx_ djn_ctx (orN djn) in
-         assert (is_false ctx_djn || Var.Set.is_subset new_xs ~of_:djn_xs) ;
+         assert (is_false ctx_djn || Var.Set.subset new_xs ~of_:djn_xs) ;
          star (exists djn_xs ctx_djn) q' ))
   |>
   [%Trace.retn fun {pf} q' ->
diff --git a/sledge/src/solver.ml b/sledge/src/solver.ml
index 4ba9a95f1..2cd88460a 100644
--- a/sledge/src/solver.ml
+++ b/sledge/src/solver.ml
@@ -81,7 +81,7 @@ end = struct
       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))
+      assert (Var.Set.subset zs ~of_:(Var.Set.union us xs))
     with exc ->
       [%Trace.info "%a" pp g] ;
       raise exc
@@ -139,8 +139,8 @@ let eq_concat (siz, seq) ms =
 
 let fresh_var name vs zs ~wrt =
   let v, wrt = Var.fresh name ~wrt in
-  let vs = Var.Set.add vs v in
-  let zs = Var.Set.add zs v in
+  let vs = Var.Set.add v vs in
+  let zs = Var.Set.add v zs in
   let v = Term.var v in
   (v, vs, zs, wrt)
 
@@ -693,6 +693,6 @@ let infer_frame : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option =
       )
   @@ fun () ->
   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) ;
+  assert (Var.Set.subset xs ~of_:subtrahend.us) ;
+  assert (Var.Set.subset (Var.Set.diff subtrahend.us xs) ~of_:minuend.us) ;
   excise_dnf minuend xs subtrahend