From 610a641b4528beb48191019b569e910ffccc760c Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 25 Feb 2019 07:07:21 -0800
Subject: [PATCH] [sledge] Sort congruence classes when printing

Reviewed By: mbouaziz

Differential Revision: D14075527

fbshipit-source-id: 8a31dbc8a
---
 sledge/src/symbheap/congruence.ml      |  5 +++--
 sledge/src/symbheap/congruence_test.ml | 10 +++++-----
 2 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/sledge/src/symbheap/congruence.ml b/sledge/src/symbheap/congruence.ml
index 85da5f167..ef3d9dfee 100644
--- a/sledge/src/symbheap/congruence.ml
+++ b/sledge/src/symbheap/congruence.ml
@@ -23,7 +23,8 @@ module Cls = struct
   type t = Exp.t list [@@deriving compare, sexp]
 
   let pp fs cls =
-    Format.fprintf fs "@[<hov 1>{@[%a@]}@]" (List.pp ",@ " Exp.pp) cls
+    Format.fprintf fs "@[<hov 1>{@[%a@]}@]" (List.pp ",@ " Exp.pp)
+      (List.sort ~compare:Exp.compare cls)
 
   let singleton e = [e]
   let add cls exp = exp :: cls
@@ -111,7 +112,7 @@ let pp_classes fs {cls} =
       let es = Cls.remove_exn ~equal:Exp.equal data key in
       if not (Cls.is_empty es) then
         Format.fprintf fs "@[%a@ = %a@]" Exp.pp key (List.pp "@ = " Exp.pp)
-          es )
+          (List.sort ~compare:Exp.compare es) )
     fs (Map.to_alist cls)
 
 let invariant r =
diff --git a/sledge/src/symbheap/congruence_test.ml b/sledge/src/symbheap/congruence_test.ml
index 9a87dc8dc..3e67d964d 100644
--- a/sledge/src/symbheap/congruence_test.ml
+++ b/sledge/src/symbheap/congruence_test.ml
@@ -83,7 +83,7 @@ let%test_module _ =
           {sat= true;
            rep= [[%x_5 ↦ %y_6]];
            lkp= [];
-           cls= [[%y_6 ↦ {%y_6, %x_5}]];
+           cls= [[%y_6 ↦ {%x_5, %y_6}]];
            use= []} |}]
 
     let%expect_test _ = printf pp_classes r1 ; [%expect {| %y_6 = %x_5 |}]
@@ -101,13 +101,13 @@ let%test_module _ =
                  [%x_5 ↦ %y_6];
                  [%z_7 ↦ %y_6]];
            lkp= [[((i64)(i8) %y_6) ↦ ((i64)(i8) %x_5)]];
-           cls= [[%y_6 ↦ {((i64)(i8) %y_6), %z_7, ((i64)(i8) %x_5), %y_6, %x_5}]];
+           cls= [[%y_6 ↦ {((i64)(i8) %x_5), ((i64)(i8) %y_6), %x_5, %y_6, %z_7}]];
            use= [[%y_6 ↦ {((i64)(i8) %x_5)}]]} |}]
 
     let%expect_test _ =
       printf pp_classes r2 ;
       [%expect
-        {| %y_6 = ((i64)(i8) %y_6) = %z_7 = ((i64)(i8) %x_5) = %x_5 |}]
+        {| %y_6 = ((i64)(i8) %x_5) = ((i64)(i8) %y_6) = %x_5 = %z_7 |}]
 
     let%test _ = mem_eq x z r2
     let%test _ = mem_eq x y (or_ r1 r2)
@@ -153,8 +153,8 @@ let%test_module _ =
              [(xor %w_4) ↦ (xor %w_4)];
              [(xor %y_6) ↦ (xor %y_6)]];
        cls= [[%w_4
-              ↦ {(%w_4 xor %y_6), %t_1, %z_7, %u_2, %x_5, %v_3, %w_4,
-                 (%y_6 xor %z_7)}]];
+              ↦ {(%w_4 xor %y_6), (%y_6 xor %z_7), %t_1, %u_2, %v_3, %w_4,
+                 %x_5, %z_7}]];
        use= [[(xor %w_4) ↦ {(%w_4 xor %y_6)}];
              [(xor %y_6) ↦ {(%y_6 xor %z_7)}];
              [%w_4 ↦ {(xor %w_4)}];