From 6b2f0a4a1ee382a1d3a0d8ee478c1d912ab210e0 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sun, 25 Oct 2020 16:02:00 -0700 Subject: [PATCH] [sledge] Strengthen normalization of arithmetic equalities Reviewed By: jvillard Differential Revision: D24371083 fbshipit-source-id: b928f534d --- sledge/src/fol.ml | 9 ++++++--- sledge/src/test/fol_test.ml | 16 ++++++++-------- sledge/src/test/sh_test.ml | 10 +++++----- sledge/src/test/solver_test.ml | 12 ++++++------ 4 files changed, 25 insertions(+), 22 deletions(-) diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml index 655d70fdc..168a230f6 100644 --- a/sledge/src/fol.ml +++ b/sledge/src/fol.ml @@ -103,6 +103,7 @@ and Trm : sig val _Record : trm array -> trm val _Ancestor : int -> trm val _Apply : Funsym.t -> trm array -> trm + val sub : trm -> trm -> trm end = struct type var = Var.t @@ -223,6 +224,7 @@ end = struct | Compound -> Arith a ) |> check invariant + let sub x y = _Arith Arith.(sub (trm x) (trm y)) let _Splat x = Splat x |> check invariant let _Sized seq siz = Sized {seq; siz} |> check invariant let _Extract seq off len = Extract {seq; off; len} |> check invariant @@ -274,8 +276,9 @@ module Fml = struct else if y == zero then _Eq0 x else match (x, y) with - | Z y, Z z -> bool (Z.equal y z) - | Q q, Q r -> bool (Q.equal q r) + (* x = y ==> 0 = x - y when x = y is an arithmetic equality *) + | (Z _ | Q _ | Arith _), _ | _, (Z _ | Q _ | Arith _) -> + _Eq0 (sub x y) | _ -> ( match Sign.of_int (compare_trm x y) with | Neg -> _Eq x y @@ -660,7 +663,7 @@ module Term = struct let rational q = `Trm (_Q q) let neg = ap1t @@ fun x -> _Arith Arith.(neg (trm x)) let add = ap2t @@ fun x y -> _Arith Arith.(add (trm x) (trm y)) - let sub = ap2t @@ fun x y -> _Arith Arith.(sub (trm x) (trm y)) + let sub = ap2t Trm.sub let mulq q = ap1t @@ fun x -> _Arith Arith.(mulc q (trm x)) let mul = ap2t @@ fun x y -> _Arith (Arith.mul x y) let div = ap2t @@ fun x y -> _Arith (Arith.div x y) diff --git a/sledge/src/test/fol_test.ml b/sledge/src/test/fol_test.ml index a14d9d372..9f114318a 100644 --- a/sledge/src/test/fol_test.ml +++ b/sledge/src/test/fol_test.ml @@ -76,7 +76,7 @@ let%test_module _ = let%expect_test _ = pp_raw f2 ; - [%expect {| {sat= false; rep= [[%x_5 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}] + [%expect {| {sat= false; rep= [[-1 ↦ ]; [0 ↦ ]]} |}] let f3 = of_eqs [(x + !0, x + !1)] @@ -84,7 +84,7 @@ let%test_module _ = let%expect_test _ = pp_raw f3 ; - [%expect {| {sat= false; rep= [[%x_5 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}] + [%expect {| {sat= false; rep= [[-1 ↦ ]; [0 ↦ ]]} |}] let f4 = of_eqs [(x, y); (x + !0, y + !1)] @@ -512,13 +512,13 @@ let%test_module _ = (Formula.orN (Iter.to_list (Iter.map ~f:snd3 (Context.dnf f)))) ; [%expect {| - ((%x_5 = %y_6) ∧ ((%w_4 = 4) ∨ (%w_4 = 5)) - ∧ ((0 = %x_5) ? (%z_7 = 2) : (%z_7 = 3))) + ((%x_5 = %y_6) ∧ ((5 = %w_4) ∨ (4 = %w_4)) + ∧ ((0 = %x_5) ? (2 = %z_7) : (3 = %z_7))) - (((%w_4 = 4) ∧ (%x_5 = %y_6) ∧ (%z_7 = 2) ∧ (0 = %x_5)) - ∨ ((%w_4 = 4) ∧ (%x_5 = %y_6) ∧ (%z_7 = 3) ∧ (0 ≠ %x_5)) - ∨ ((%w_4 = 5) ∧ (%x_5 = %y_6) ∧ (%z_7 = 2) ∧ (0 = %x_5)) - ∨ ((%w_4 = 5) ∧ (%x_5 = %y_6) ∧ (%z_7 = 3) ∧ (0 ≠ %x_5))) |}] + (((%x_5 = %y_6) ∧ (0 = %x_5) ∧ (5 = %w_4) ∧ (2 = %z_7)) + ∨ ((%x_5 = %y_6) ∧ (0 = %x_5) ∧ (4 = %w_4) ∧ (2 = %z_7)) + ∨ ((%x_5 = %y_6) ∧ (5 = %w_4) ∧ (3 = %z_7) ∧ (0 ≠ %x_5)) + ∨ ((%x_5 = %y_6) ∧ (4 = %w_4) ∧ (3 = %z_7) ∧ (0 ≠ %x_5))) |}] let%test "unsigned boolean overflow" = Formula.equal Formula.tt diff --git a/sledge/src/test/sh_test.ml b/sledge/src/test/sh_test.ml index bfec4838b..b08825d84 100644 --- a/sledge/src/test/sh_test.ml +++ b/sledge/src/test/sh_test.ml @@ -94,8 +94,8 @@ let%test_module _ = ∨ ( ( ( 1 = _ = %y_7 ∧ emp) ∨ ( 2 = _ ∧ emp) )) ) - ( (∃ %x_6, %x_7 . (%x_7 = 2) ∧ emp) - ∨ (∃ %x_6 . ((%x_6 = 1) ∧ (%y_7 = 1)) ∧ emp) + ( (∃ %x_6, %x_7 . (2 = %x_7) ∧ emp) + ∨ (∃ %x_6 . ((1 = %x_6) ∧ (1 = %y_7)) ∧ emp) ∨ ( (0 = %x_6) ∧ emp) ) |}] @@ -119,8 +119,8 @@ let%test_module _ = ∨ ( ( ( 1 = _ = %y_7 ∧ emp) ∨ ( 2 = _ ∧ emp) )) ) - ( (∃ %x_6, %x_8, %x_9 . (%x_9 = 2) ∧ emp) - ∨ (∃ %x_6, %x_8 . ((%y_7 = 1) ∧ (%x_8 = 1)) ∧ emp) + ( (∃ %x_6, %x_8, %x_9 . (2 = %x_9) ∧ emp) + ∨ (∃ %x_6, %x_8 . ((1 = %y_7) ∧ (1 = %x_8)) ∧ emp) ∨ (∃ %x_6 . (0 = %x_6) ∧ emp) ) |}] @@ -156,7 +156,7 @@ let%test_module _ = {| ∃ %x_6 . %x_6 = %x_6^ ∧ (-1 + %y_7) = %y_7^ ∧ emp - (tt ∧ ((-1 + %y_7) = %y_7^)) ∧ emp + (tt ∧ (-1 = (-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 1b7473951..acdbe2ea9 100644 --- a/sledge/src/test/solver_test.ml +++ b/sledge/src/test/solver_test.ml @@ -238,26 +238,26 @@ let%test_module _ = {| ( infer_frame: %l_6 -[ %l_6, 16 )-> ⟨8×%n_9,%a_2⟩^⟨(16 + -8×%n_9),%a_3⟩ - * ( ( 1 = %n_9 ∧ emp) - ∨ ( 0 = %n_9 ∧ emp) + * ( ( 0 = %n_9 ∧ emp) + ∨ ( 1 = %n_9 ∧ emp) ∨ ( 2 = %n_9 ∧ emp) ) \- ∃ %a_1, %m_8 . %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩ ) infer_frame: ( ( %a_3 = _ - ∧ 1 = %n_9 + ∧ 0 = %n_9 ∧ 16 = %m_8 - ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1 + ∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1 ∧ emp) ∨ ( %a_1 = %a_2 ∧ 2 = %n_9 ∧ 16 = %m_8 ∧ (16 + %l_6) -[ %l_6, 16 )-> ⟨0,%a_3⟩) ∨ ( %a_3 = _ - ∧ 0 = %n_9 + ∧ 1 = %n_9 ∧ 16 = %m_8 - ∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1 + ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1 ∧ emp) ) |}]