[sledge] Replace Set.inter_diff with clearer diff_inter

Summary: It is easier to understand the order of args with diff_inter.

Reviewed By: ngorogiannis

Differential Revision: D19221869

fbshipit-source-id: b29ac83c8

sledge/src/import/import.ml

@@ -291,8 +291,8 @@ module Set = struct
   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 inter_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
 

sledge/src/import/import.mli

@@ -231,11 +231,11 @@ module Set : sig
   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 inter_diff : ('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

sledge/src/symbheap/sh.ml

@@ -48,7 +48,7 @@ let rec pp vs all_xs fs {us; xs; cong; pure; heap; djns} =
   let all_xs = Set.union all_xs xs in
   let is_x var = Set.mem all_xs (Option.value_exn (Var.of_term var)) in
   pp_us fs us ;
-  let xs_i_vs, xs_d_vs = Set.inter_diff vs xs in
+  let xs_d_vs, xs_i_vs = Set.diff_inter xs vs in
   if not (Set.is_empty xs_i_vs) then (
     Format.fprintf fs "@<2>∃ @[%a@] ." (Var.Set.pp_full ~is_x) xs_i_vs ;
     if not (Set.is_empty xs_d_vs) then Format.fprintf fs "@ " ) ;