From 2124be1c7158c334624d0b3153033ac518bb1ebd Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 16 Apr 2020 03:39:28 -0700 Subject: [PATCH] [sledge] Remove the "simplified" intermediate between interpreted and uninterpreted Summary: The current notion of "simplified" function symbols, which are treated as a hybrid between interpreted and uninterpreted, has no logical basis. Normalization is now strong enough, due to stronger handling of the changing carrier set, that the "simplified" classification can be removed. Reviewed By: jvillard Differential Revision: D20726961 fbshipit-source-id: 9962ea323 --- sledge/lib/equality.ml | 31 ++++++-------- sledge/lib/equality_test.ml | 84 +++++++++++++++++++++++++++---------- 2 files changed, 73 insertions(+), 42 deletions(-) diff --git a/sledge/lib/equality.ml b/sledge/lib/equality.ml index 2e669e240..465c69b4a 100644 --- a/sledge/lib/equality.ml +++ b/sledge/lib/equality.ml @@ -9,7 +9,7 @@ (** Classification of Terms by Theory *) -type kind = Interpreted | Simplified | Atomic | Uninterpreted +type kind = Interpreted | Atomic | Uninterpreted [@@deriving compare, equal] let classify e = @@ -19,7 +19,6 @@ let classify e = |Ap3 (Extract, _, _, _) |ApN (Concat, _) -> Interpreted - | Ap2 ((Eq | Dq), _, _) -> Simplified | Ap1 _ | Ap2 _ | Ap3 _ | ApN _ -> Uninterpreted | RecN _ | Var _ | Integer _ | Rational _ | Float _ | Nondet _ | Label _ -> @@ -86,10 +85,7 @@ end = struct (** apply a substitution to maximal non-interpreted subterms *) let rec norm s a = - match classify a with - | Interpreted -> Term.map ~f:(norm s) a - | Simplified -> apply s (Term.map ~f:(norm s) a) - | Atomic | Uninterpreted -> apply s a + if interpreted a then Term.map ~f:(norm s) a else apply s a (** compose two substitutions *) let compose r s = @@ -353,8 +349,8 @@ let classes r = Subst.fold r.rep ~init:Term.Map.empty ~f:(fun ~key ~data cls -> match classify key with | Interpreted | Atomic -> add key data cls - | Simplified | Uninterpreted -> - add (Term.map ~f:(Subst.apply r.rep) key) data cls ) + | Uninterpreted -> add (Term.map ~f:(Subst.apply r.rep) key) data cls + ) let cls_of r e = let e' = Subst.apply r.rep e in @@ -469,29 +465,26 @@ let rec canon r a = ( match classify a with | Atomic -> Subst.apply r.rep a | Interpreted -> Term.map ~f:(canon r) a - | Simplified | Uninterpreted -> ( + | Uninterpreted -> ( let a' = Term.map ~f:(canon r) a in match classify a' with | Atomic -> Subst.apply r.rep a' | Interpreted -> a' - | Simplified | Uninterpreted -> lookup r a' ) ) + | Uninterpreted -> lookup r a' ) ) |> [%Trace.retn fun {pf} -> pf "%a" Term.pp] let rec extend_ a r = (* omit identity mappings for constants *) if Term.is_constant a then r - else - match classify a with (* omit interpreted terms, but consider their subterms *) - | Interpreted | Simplified -> Term.fold ~f:extend_ a ~init:r + else if interpreted a then Term.fold ~f:extend_ a ~init:r + else (* add uninterpreted terms *) - | Uninterpreted -> ( - match Subst.extend a r with - (* and their subterms if newly added *) - | Some r -> Term.fold ~f:extend_ a ~init:r - | None -> r ) - | Atomic -> r + match Subst.extend a r with + (* and their subterms if newly added *) + | Some r -> Term.fold ~f:extend_ a ~init:r + | None -> r (** add a term to the carrier *) let extend a r = diff --git a/sledge/lib/equality_test.ml b/sledge/lib/equality_test.ml index 0e620605a..793b164a9 100644 --- a/sledge/lib/equality_test.ml +++ b/sledge/lib/equality_test.ml @@ -64,19 +64,24 @@ let%test_module _ = let f2 = of_eqs [(x, x + !1)] let%test _ = is_false f2 - let%expect_test _ = pp f2 ; [%expect {| {sat= false; rep= []} |}] + + let%expect_test _ = + pp f2 ; [%expect {| {sat= false; rep= [[%x_5 ↦ ]]} |}] let f3 = of_eqs [(x + !0, x + !1)] let%test _ = is_false f3 - let%expect_test _ = pp f3 ; [%expect {| {sat= false; rep= []} |}] + + let%expect_test _ = + pp f3 ; [%expect {| {sat= false; rep= [[%x_5 ↦ ]]} |}] let f4 = of_eqs [(x, y); (x + !0, y + !1)] let%test _ = is_false f4 let%expect_test _ = - pp f4 ; [%expect {| {sat= false; rep= [[%y_6 ↦ %x_5]]} |}] + pp f4 ; + [%expect {| {sat= false; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]]} |}] let t1 = of_eqs [(!1, !1)] @@ -103,8 +108,8 @@ let%test_module _ = [%expect {| %x_5 = %y_6 - - {sat= true; rep= [[%y_6 ↦ %x_5]]} |}] + + {sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]]} |}] let%test _ = entails_eq r1 x y @@ -118,7 +123,10 @@ let%test_module _ = %x_5 = %y_6 = %z_7 = ((u8) %x_5) {sat= true; - rep= [[%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]; [((u8) %x_5) ↦ %x_5]]} |}] + rep= [[%x_5 ↦ ]; + [%y_6 ↦ %x_5]; + [%z_7 ↦ %x_5]; + [((u8) %x_5) ↦ %x_5]]} |}] let%test _ = entails_eq r2 x z let%test _ = entails_eq (or_ r1 r2) x y @@ -139,11 +147,11 @@ let%test_module _ = pp rs ; [%expect {| - {sat= true; rep= [[%y_6 ↦ %w_4]; [%z_7 ↦ %w_4]]} + {sat= true; rep= [[%w_4 ↦ ]; [%y_6 ↦ %w_4]; [%z_7 ↦ %w_4]]} - {sat= true; rep= [[%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]]} + {sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]]} - {sat= true; rep= [[%z_7 ↦ %y_6]]} |}] + {sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]]} |}] let%test _ = let r = of_eqs [(w, y); (y, z)] in @@ -162,10 +170,12 @@ let%test_module _ = = (%y_6 rem %t_1) {sat= true; - rep= [[%u_2 ↦ %t_1]; + rep= [[%t_1 ↦ ]; + [%u_2 ↦ %t_1]; [%v_3 ↦ %t_1]; [%w_4 ↦ %t_1]; [%x_5 ↦ %t_1]; + [%y_6 ↦ ]; [%z_7 ↦ %t_1]; [(%y_6 rem %v_3) ↦ %t_1]; [(%y_6 rem %z_7) ↦ %t_1]]} |}] @@ -186,7 +196,8 @@ let%test_module _ = {sat= true; rep= [[%w_4 ↦ (%z_7 + 3)]; [%x_5 ↦ (%z_7 + 8)]; - [%y_6 ↦ (%z_7 + -4)]]} |}] + [%y_6 ↦ (%z_7 + -4)]; + [%z_7 ↦ ]]} |}] let%test _ = entails_eq r4 x (w + !5) let%test _ = difference r4 x w |> Poly.equal (Some (Z.of_int 5)) @@ -219,10 +230,19 @@ let%test_module _ = {| %v_3 = %x_5 ∧ %w_4 = %y_6 = %z_7 - {sat= true; rep= [[%x_5 ↦ %v_3]; [%y_6 ↦ %w_4]; [%z_7 ↦ %w_4]]} + {sat= true; + rep= [[%v_3 ↦ ]; + [%w_4 ↦ ]; + [%x_5 ↦ %v_3]; + [%y_6 ↦ %w_4]; + [%z_7 ↦ %w_4]]} {sat= true; - rep= [[%w_4 ↦ %v_3]; [%x_5 ↦ %v_3]; [%y_6 ↦ %v_3]; [%z_7 ↦ %v_3]]} + rep= [[%v_3 ↦ ]; + [%w_4 ↦ %v_3]; + [%x_5 ↦ %v_3]; + [%y_6 ↦ %v_3]; + [%z_7 ↦ %v_3]]} %v_3 = %w_4 = %x_5 = %y_6 = %z_7 |}] @@ -248,7 +268,11 @@ let%test_module _ = %v_3 = %w_4 = %x_5 = %y_6 = %z_7 {sat= true; - rep= [[%w_4 ↦ %v_3]; [%x_5 ↦ %v_3]; [%y_6 ↦ %v_3]; [%z_7 ↦ %v_3]]} |}] + rep= [[%v_3 ↦ ]; + [%w_4 ↦ %v_3]; + [%x_5 ↦ %v_3]; + [%y_6 ↦ %v_3]; + [%z_7 ↦ %v_3]]} |}] let%test _ = normalize r7' w |> Term.equal v @@ -267,7 +291,7 @@ let%test_module _ = {| (13 × %z_7) = %x_5 ∧ 14 = %y_6 - {sat= true; rep= [[%x_5 ↦ (13 × %z_7)]; [%y_6 ↦ 14]]} |}] + {sat= true; rep= [[%x_5 ↦ (13 × %z_7)]; [%y_6 ↦ 14]; [%z_7 ↦ ]]} |}] let%test _ = entails_eq r8 y !14 @@ -280,7 +304,7 @@ let%test_module _ = {| (%z_7 + -16) = %x_5 - {sat= true; rep= [[%x_5 ↦ (%z_7 + -16)]]} |}] + {sat= true; rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]]} |}] let%test _ = difference r9 z (x + !8) |> Poly.equal (Some (Z.of_int 8)) @@ -297,7 +321,7 @@ let%test_module _ = {| (%z_7 + -16) = %x_5 - {sat= true; rep= [[%x_5 ↦ (%z_7 + -16)]]} + {sat= true; rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]]} (-1 × %x_5 + %z_7 + -8) @@ -327,7 +351,11 @@ let%test_module _ = [%expect {| {sat= true; - rep= [[%z_7 ↦ %y_6]; [(%x_5 = 2) ↦ %y_6]; [(%x_5 ≠ 2) ↦ %y_6]]} |}] + rep= [[%x_5 ↦ ]; + [%y_6 ↦ ]; + [%z_7 ↦ %y_6]; + [(%x_5 = 2) ↦ %y_6]; + [(%x_5 ≠ 2) ↦ %y_6]]} |}] let%test _ = not (is_false r13) (* incomplete *) @@ -335,7 +363,9 @@ let%test_module _ = let r14 = of_eqs [(a, a); (x, !1)] let%expect_test _ = - pp r14 ; [%expect {| {sat= true; rep= [[%x_5 ↦ 1]]} |}] + pp r14 ; + [%expect + {| {sat= true; rep= [[%x_5 ↦ 1]; [(%x_5 ≠ 0) ↦ -1]]} |}] let%test _ = entails_eq r14 a Term.true_ @@ -346,7 +376,8 @@ let%test_module _ = pp r14 ; [%expect {| - {sat= true; rep= [[%x_5 ↦ 1]; [(%y_6 ≠ 0) ↦ -1]]} |}] + {sat= true; + rep= [[%x_5 ↦ 1]; [%y_6 ↦ ]; [(%x_5 ≠ 0) ↦ -1]; [(%y_6 ≠ 0) ↦ -1]]} |}] let%test _ = entails_eq r14 a Term.true_ let%test _ = entails_eq r14 b Term.true_ @@ -355,7 +386,9 @@ let%test_module _ = let r15 = of_eqs [(b, b); (x, !1)] let%expect_test _ = - pp r15 ; [%expect {| {sat= true; rep= [[%x_5 ↦ 1]]} |}] + pp r15 ; + [%expect + {| {sat= true; rep= [[%x_5 ↦ 1]; [(%x_5 ≠ 0) ↦ -1]]} |}] let%test _ = entails_eq r15 b (Term.signed 1 !1) let%test _ = entails_eq r15 (Term.unsigned 1 b) !1 @@ -370,6 +403,7 @@ let%test_module _ = {| {sat= false; rep= [[%x_5 ↦ (%y_6 + 1)]; + [%y_6 ↦ ]; [((u8) %y_6) ↦ (%y_6 + -2)]; [((u8) (%x_5 + -1)) ↦ (%y_6 + 3)]]} |}] @@ -383,7 +417,8 @@ let%test_module _ = [%expect {| {sat= false; - rep= [[%y_6 ↦ %x_5]; + rep= [[%x_5 ↦ ]; + [%y_6 ↦ %x_5]; [((u8) %x_5) ↦ %x_5]; [((u8) %y_6) ↦ (%x_5 + -1)]]} |}] @@ -396,7 +431,10 @@ let%test_module _ = [%expect {| {sat= true; - rep= [[((u8) %x_5) ↦ %x_5]; [((u8) %y_6) ↦ (%y_6 + -1)]]} + rep= [[%x_5 ↦ ]; + [%y_6 ↦ ]; + [((u8) %x_5) ↦ %x_5]; + [((u8) %y_6) ↦ (%y_6 + -1)]]} %x_5 = ((u8) %x_5) ∧ (%y_6 + -1) = ((u8) %y_6) |}]