From 6e01fa91d5a3fd1fecb347c1f562012185ac7619 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Wed, 8 Jan 2020 08:03:31 -0800
Subject: [PATCH] [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  | 2 +-
 sledge/src/import/import.mli | 2 +-
 sledge/src/symbheap/sh.ml    | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/sledge/src/import/import.ml b/sledge/src/import/import.ml
index f72ebdb84..b14977615 100644
--- a/sledge/src/import/import.ml
+++ b/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
 
diff --git a/sledge/src/import/import.mli b/sledge/src/import/import.mli
index 40a1e6758..284035966 100644
--- a/sledge/src/import/import.mli
+++ b/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
diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml
index 6a1d21c06..9549d7586 100644
--- a/sledge/src/symbheap/sh.ml
+++ b/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 "@ " ) ;