From 74086e926a724391df892a8fafe1919ea9c9c1b6 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 4 Sep 2020 13:38:35 -0700 Subject: [PATCH] [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 | 27 +++++++++++++++++++++------ sledge/src/test/fol_test.ml | 9 +++++---- sledge/src/test/sh_test.ml | 4 ++-- sledge/src/test/solver_test.ml | 18 +++++++++--------- 4 files changed, 37 insertions(+), 21 deletions(-) diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml index 969c6b575..dc6128da7 100644 --- a/sledge/src/fol.ml +++ b/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 diff --git a/sledge/src/test/fol_test.ml b/sledge/src/test/fol_test.ml index 718339f8b..bb66d99a7 100644 --- a/sledge/src/test/fol_test.ml +++ b/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)) - ∨ ((((%x_5 = %y_6) ∧ (%w_4 = 5)) ∧ (0 = %x_5)) ∧ (%z_7 = 2))) - ∨ ((((%x_5 = %y_6) ∧ (%w_4 = 4)) ∧ (0 ≠ %x_5)) ∧ (%z_7 = 3))) - ∨ ((((%x_5 = %y_6) ∧ (%w_4 = 4)) ∧ (0 = %x_5)) ∧ (%z_7 = 2))) |}] + (((0 = %x_5) ∧ ((%z_7 = 2) ∧ ((%w_4 = 4) ∧ (%x_5 = %y_6)))) + ∨ (((0 ≠ %x_5) ∧ ((%z_7 = 3) ∧ ((%w_4 = 4) ∧ (%x_5 = %y_6)))) + ∨ (((0 = %x_5) ∧ ((%z_7 = 2) ∧ ((%w_4 = 5) ∧ (%x_5 = %y_6)))) + ∨ ((0 ≠ %x_5) + ∧ ((%z_7 = 3) ∧ ((%w_4 = 5) ∧ (%x_5 = %y_6))))))) |}] end ) diff --git a/sledge/src/test/sh_test.ml b/sledge/src/test/sh_test.ml index ddfc1f29b..b70ce7e8c 100644 --- a/sledge/src/test/sh_test.ml +++ b/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 |}] diff --git a/sledge/src/test/solver_test.ml b/sledge/src/test/solver_test.ml index 7cd2ebb03..26663f1ba 100644 --- a/sledge/src/test/solver_test.ml +++ b/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 = _ - ∧ 0 = %n_9 + ( ( %a_1 = %a_2 + ∧ 2 = %n_9 ∧ 16 = %m_8 - ∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1 - ∧ emp) + ∧ (16 + %l_6) -[ %l_6, 16 )-> ⟨0,%a_3⟩) ∨ ( %a_3 = _ ∧ 1 = %n_9 ∧ 16 = %m_8 ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1 ∧ emp) - ∨ ( %a_1 = %a_2 - ∧ 2 = %n_9 + ∨ ( %a_3 = _ + ∧ 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 ∨ *)