[sledge] Improve: Normalize order of symmetric binary formulas

Summary:
Sort the subterms or subformulas of binary formulas that are
symmetric. This avoids redundant formulas such as both `x = y` and `y
= x`.

Reviewed By: ngorogiannis

Differential Revision: D23487501

fbshipit-source-id: 7e2295aba

sledge/src/fol.ml

@@ -95,6 +95,7 @@ let equal_trm x y =
       Int.equal i j
   | _ -> equal_trm x y
 
+let sort_trm x y = if compare_trm x y <= 0 then (x, y) else (y, x)
 let zero = Z Z.zero
 let one = Z Z.one
 let _Neg x = Neg x
@@ -199,6 +200,8 @@ end = struct
     | UNegLit of Predsym.t * trm
   [@@deriving compare, equal, sexp]
 
+  let sort_fml x y = if compare_fml x y <= 0 then (x, y) else (y, x)
+
   (** Some normalization is necessary for [embed_into_fml] (defined below)
       to be left inverse to [embed_into_cnd]. Essentially
       [0 ≠ (p ? 1 : 0)] needs to normalize to [p], by way of
@@ -241,7 +244,9 @@ end = struct
       match equal_or_separate x y with
       | Equal -> Tt
       | Separate -> Ff
-      | Unknown -> Eq (x, y)
+      | Unknown ->
+          let x, y = sort_trm x y in
+          Eq (x, y)
 
   let _Dq x y =
     if x == zero then _Dq0 y
@@ -250,7 +255,9 @@ end = struct
       match equal_or_separate x y with
       | Equal -> Ff
       | Separate -> Tt
-      | Unknown -> Dq (x, y)
+      | Unknown ->
+          let x, y = sort_trm x y in
+          Dq (x, y)
 
   let _Gt0 = function
     | Z z -> if Z.gt z Z.zero then Tt else Ff
@@ -290,7 +297,9 @@ end = struct
       match equal_or_opposite p q with
       | Equal -> p
       | Opposite -> Ff
-      | Unknown -> And (p, q) )
+      | Unknown ->
+          let p, q = sort_fml p q in
+          And (p, q) )
 
   and _Or p q =
     match (p, q) with
@@ -300,7 +309,9 @@ end = struct
       match equal_or_opposite p q with
       | Equal -> p
       | Opposite -> Tt
-      | Unknown -> Or (p, q) )
+      | Unknown ->
+          let p, q = sort_fml p q in
+          Or (p, q) )
 
   and _Iff p q =
     match (p, q) with
@@ -310,7 +321,9 @@ end = struct
       match equal_or_opposite p q with
       | Equal -> Tt
       | Opposite -> Ff
-      | Unknown -> Iff (p, q) )
+      | Unknown ->
+          let p, q = sort_fml p q in
+          Iff (p, q) )
 
   and _Xor p q =
     match (p, q) with
@@ -320,7 +333,9 @@ end = struct
       match equal_or_opposite p q with
       | Equal -> Ff
       | Opposite -> Tt
-      | Unknown -> Xor (p, q) )
+      | Unknown ->
+          let p, q = sort_fml p q in
+          Xor (p, q) )
 
   and _Not = function
     | Tt -> _Ff

sledge/src/test/fol_test.ml

@@ -515,8 +515,9 @@ let%test_module _ =
         (((%x_5 = %y_6) ∧ ((0 = %x_5) ? (%z_7 = 2) : (%z_7 = 3)))
           ∧ ((%w_4 = 4) ∨ (%w_4 = 5)))
 
-        (((((((%x_5 = %y_6) ∧ (%w_4 = 5)) ∧ (0 ≠ %x_5)) ∧ (%z_7 = 3))
+        (((0 = %x_5) ∧ ((%z_7 = 2) ∧ ((%w_4 = 4) ∧ (%x_5 = %y_6))))
-            ∨ ((((%x_5 = %y_6) ∧ (%w_4 = 5)) ∧ (0 = %x_5)) ∧ (%z_7 = 2)))
+          ∨ (((0 ≠ %x_5) ∧ ((%z_7 = 3) ∧ ((%w_4 = 4) ∧ (%x_5 = %y_6))))
-           ∨ ((((%x_5 = %y_6) ∧ (%w_4 = 4)) ∧ (0 ≠ %x_5)) ∧ (%z_7 = 3)))
+              ∨ (((0 = %x_5) ∧ ((%z_7 = 2) ∧ ((%w_4 = 5) ∧ (%x_5 = %y_6))))
-          ∨ ((((%x_5 = %y_6) ∧ (%w_4 = 4)) ∧ (0 = %x_5)) ∧ (%z_7 = 2))) |}]
+                  ∨ ((0 ≠ %x_5)
+                      ∧ ((%z_7 = 3) ∧ ((%w_4 = 5) ∧ (%x_5 = %y_6))))))) |}]
   end )

sledge/src/test/sh_test.ml

@@ -111,7 +111,7 @@ let%test_module _ =
           )
     
         ( (∃ %x_6, %x_8, %x_9 .   (%x_9 = 2) ∧ emp)
-        ∨ (∃ %x_6, %x_8 .   ((%x_8 = 1) ∧ (%y_7 = 1)) ∧ emp)
+        ∨ (∃ %x_6, %x_8 .   ((%y_7 = 1) ∧ (%x_8 = 1)) ∧ emp)
         ∨ (∃ %x_6 .   (0 = %x_6) ∧ emp)
         ) |}]
 
@@ -147,7 +147,7 @@ let%test_module _ =
         {|
         ∃ %x_6 .   %x_6 = %x_6^ ∧ (-1 + %y_7) = %y_7^ ∧ emp
     
-          (%y_7^ = (-1 + %y_7)) ∧ emp
+          ((-1 + %y_7) = %y_7^) ∧ emp
 
           (-1 + %y_7) = %y_7^ ∧ emp |}]
 

sledge/src/test/solver_test.ml

@@ -239,27 +239,27 @@ let%test_module _ =
         ( infer_frame:
             %l_6
               -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(16 + (-8 × %n_9)),%a_3⟩
-          * ( (  0 = %n_9 ∧ emp)
+          * ( (  2 = %n_9 ∧ emp)
-            ∨ (  2 = %n_9 ∧ emp)
+            ∨ (  0 = %n_9 ∧ emp)
             ∨ (  1 = %n_9 ∧ emp)
             )
           \- ∃ %a_1, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩
         ) infer_frame:
-            ( (  %a_3 = _
+            ( (  %a_1 = %a_2
-               ∧ 0 = %n_9
+               ∧ 2 = %n_9
                ∧ 16 = %m_8
-               ∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1
+               ∧ (16 + %l_6) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
-               ∧ emp)
             ∨ (  %a_3 = _
                ∧ 1 = %n_9
                ∧ 16 = %m_8
                ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1
                ∧ emp)
-            ∨ (  %a_1 = %a_2
+            ∨ (  %a_3 = _
-               ∧ 2 = %n_9
+               ∧ 0 = %n_9
                ∧ 16 = %m_8
-               ∧ (16 + %l_6) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
+               ∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1
+               ∧ emp)
             ) |}]
 
     (* Incompleteness: equivalent to above but using ≤ instead of ∨ *)