From 84bb40941296eba67b3c0805357ccd2d1cf92e7d Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 9 Jan 2020 05:06:17 -0800
Subject: [PATCH] [sledge] Sort arguments of Eq terms

Summary:
Now that they are uncurried, congruence closure does not need the
order of subterms to be preserved. Sorting them reduces redundancy in
case the same equality in different orders is encountered, and
improved printing.

Reviewed By: ngorogiannis

Differential Revision: D19221875

fbshipit-source-id: c6bf4ccad
---
 sledge/src/llair/term.ml      |  9 ++++++---
 sledge/src/llair/term_test.ml | 18 +++++++++---------
 2 files changed, 15 insertions(+), 12 deletions(-)

diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml
index 88ade7e12..02f9374a1 100644
--- a/sledge/src/llair/term.ml
+++ b/sledge/src/llair/term.ml
@@ -680,9 +680,12 @@ let rec simp_eq x y =
   (* e = (c ? t : f) ==> (c ? e = t : e = f) *)
   | e, Ap3 (Conditional, c, t, f) | Ap3 (Conditional, c, t, f), e ->
       simp_cond c (simp_eq e t) (simp_eq e f)
-  (* e = e ==> true *)
-  | x, y when equal x y -> bool true
-  | x, y -> Ap2 (Eq, x, y)
+  | x, y -> (
+    match Int.sign (compare x y) with
+    (* e = e ==> true *)
+    | Zero -> bool true
+    | Neg -> Ap2 (Eq, x, y)
+    | Pos -> Ap2 (Eq, y, x) )
 
 and simp_dq x y =
   match (x, y) with
diff --git a/sledge/src/llair/term_test.ml b/sledge/src/llair/term_test.ml
index 6fde19254..ad8de1264 100644
--- a/sledge/src/llair/term_test.ml
+++ b/sledge/src/llair/term_test.ml
@@ -151,7 +151,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp (z = y) ;
-      [%expect {| (%z_2 = %y_1) |}]
+      [%expect {| (%y_1 = %z_2) |}]
 
     let%expect_test _ =
       pp (z = z) ;
@@ -191,7 +191,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp (y = (!(-3) * y) + !4) ;
-      [%expect {| (%y_1 = (-3 × %y_1 + 4)) |}]
+      [%expect {| ((-3 × %y_1 + 4) = %y_1) |}]
 
     let%expect_test _ =
       pp ((!(-3) * y) + !4 = y) ;
@@ -207,23 +207,23 @@ let%test_module _ =
 
     let%expect_test _ =
       pp ((!13 * z) + !42 = (!3 * y) + (!13 * z)) ;
-      [%expect {| ((13 × %z_2 + 42) = (3 × %y_1 + 13 × %z_2)) |}]
+      [%expect {| ((3 × %y_1 + 13 × %z_2) = (13 × %z_2 + 42)) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !(-42) = (!3 * y) + (!13 * z)) ;
-      [%expect {| ((13 × %z_2 + -42) = (3 × %y_1 + 13 × %z_2)) |}]
+      [%expect {| ((3 × %y_1 + 13 × %z_2) = (13 × %z_2 + -42)) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 = (!(-3) * y) + (!13 * z)) ;
-      [%expect {| ((13 × %z_2 + 42) = (-3 × %y_1 + 13 × %z_2)) |}]
+      [%expect {| ((-3 × %y_1 + 13 × %z_2) = (13 × %z_2 + 42)) |}]
 
     let%expect_test _ =
       pp ((!10 * z) + !42 = (!(-3) * y) + (!13 * z)) ;
-      [%expect {| ((10 × %z_2 + 42) = (-3 × %y_1 + 13 × %z_2)) |}]
+      [%expect {| ((-3 × %y_1 + 13 × %z_2) = (10 × %z_2 + 42)) |}]
 
     let%expect_test _ =
       pp ~~((!13 * z) + !(-42) != (!3 * y) + (!13 * z)) ;
-      [%expect {| ((13 × %z_2 + -42) = (3 × %y_1 + 13 × %z_2)) |}]
+      [%expect {| ((3 × %y_1 + 13 × %z_2) = (13 × %z_2 + -42)) |}]
 
     let%expect_test _ =
       pp ~~(!2 < y && z <= !3) ;
@@ -241,9 +241,9 @@ let%test_module _ =
         {|
         (%z_2 = 0)
 
-        (0 = %z_2)
+        (%z_2 = 0)
 
-        (0 = %z_2) |}]
+        (%z_2 = 0) |}]
 
     let%expect_test _ =
       let z1 = z + !1 in