[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

@@ -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 -> (
-  | x, y when equal x y -> bool true
+    match Int.sign (compare x y) with
-  | x, y -> Ap2 (Eq, x, y)
+    (* 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

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