pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[sledge] Remove the "simplified" intermediate between interpreted and uninterpreted

Browse Source 
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
master
Josh Berdine 5 years ago committed by Facebook GitHub Bot
parent ee595f2ebf
commit 2124be1c71
2 changed files with 73 additions and 42 deletions
Show Stats Download Patch File Download Diff File

31
sledge/lib/equality.ml
Unescape View File

@ -9,7 +9,7 @@
(** Classification of Terms by Theory *) (** Classification of Terms by Theory *)
type kind = Interpreted | Simplified | Atomic | Uninterpreted type kind = Interpreted | Atomic | Uninterpreted
[@@deriving compare, equal] [@@deriving compare, equal]
let classify e = let classify e =
@ -19,7 +19,6 @@ let classify e =
|Ap3 (Extract, _, _, _) |Ap3 (Extract, _, _, _)
|ApN (Concat, _) -> |ApN (Concat, _) ->
Interpreted Interpreted
| Ap2 ((Eq | Dq), _, _) -> Simplified
| Ap1 _ | Ap2 _ | Ap3 _ | ApN _ -> Uninterpreted | Ap1 _ | Ap2 _ | Ap3 _ | ApN _ -> Uninterpreted
| RecN _ | Var _ | Integer _ | Rational _ | Float _ | Nondet _ | Label _ | RecN _ | Var _ | Integer _ | Rational _ | Float _ | Nondet _ | Label _
-> ->
@ -86,10 +85,7 @@ end = struct
(** apply a substitution to maximal non-interpreted subterms *) (** apply a substitution to maximal non-interpreted subterms *)
let rec norm s a = let rec norm s a =
match classify a with if interpreted a then Term.map ~f:(norm s) a else apply s a
| Interpreted -> Term.map ~f:(norm s) a
| Simplified -> apply s (Term.map ~f:(norm s) a)
| Atomic | Uninterpreted -> apply s a
(** compose two substitutions *) (** compose two substitutions *)
let compose r s = let compose r s =
@ -353,8 +349,8 @@ let classes r =
Subst.fold r.rep ~init:Term.Map.empty ~f:(fun ~key ~data cls -> Subst.fold r.rep ~init:Term.Map.empty ~f:(fun ~key ~data cls ->
match classify key with match classify key with
| Interpreted | Atomic -> add key data cls | Interpreted | Atomic -> add key data cls
| Simplified | Uninterpreted -> | Uninterpreted -> add (Term.map ~f:(Subst.apply r.rep) key) data cls
add (Term.map ~f:(Subst.apply r.rep) key) data cls ) )
let cls_of r e = let cls_of r e =
let e' = Subst.apply r.rep e in let e' = Subst.apply r.rep e in
@ -469,29 +465,26 @@ let rec canon r a =
( match classify a with ( match classify a with
| Atomic -> Subst.apply r.rep a | Atomic -> Subst.apply r.rep a
| Interpreted -> Term.map ~f:(canon r) a | Interpreted -> Term.map ~f:(canon r) a
| Simplified | Uninterpreted -> ( | Uninterpreted -> (
let a' = Term.map ~f:(canon r) a in let a' = Term.map ~f:(canon r) a in
match classify a' with match classify a' with
| Atomic -> Subst.apply r.rep a' | Atomic -> Subst.apply r.rep a'
| Interpreted -> a' | Interpreted -> a'
| Simplified | Uninterpreted -> lookup r a' ) ) | Uninterpreted -> lookup r a' ) )
|> |>
[%Trace.retn fun {pf} -> pf "%a" Term.pp] [%Trace.retn fun {pf} -> pf "%a" Term.pp]
let rec extend_ a r = let rec extend_ a r =
(* omit identity mappings for constants *) (* omit identity mappings for constants *)
if Term.is_constant a then r if Term.is_constant a then r
else
match classify a with
(* omit interpreted terms, but consider their subterms *) (* 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 *) (* add uninterpreted terms *)
| Uninterpreted -> ( match Subst.extend a r with
match Subst.extend a r with (* and their subterms if newly added *)
(* and their subterms if newly added *) | Some r -> Term.fold ~f:extend_ a ~init:r
| Some r -> Term.fold ~f:extend_ a ~init:r | None -> r
| None -> r )
| Atomic -> r
(** add a term to the carrier *) (** add a term to the carrier *)
let extend a r = let extend a r =

84
sledge/lib/equality_test.ml
Unescape View File

@ -64,19 +64,24 @@ let%test_module _ =
let f2 = of_eqs [(x, x + !1)] let f2 = of_eqs [(x, x + !1)]
let%test _ = is_false f2 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 f3 = of_eqs [(x + !0, x + !1)]
let%test _ = is_false f3 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 f4 = of_eqs [(x, y); (x + !0, y + !1)]
let%test _ = is_false f4 let%test _ = is_false f4
let%expect_test _ = 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)] let t1 = of_eqs [(!1, !1)]
@ -103,8 +108,8 @@ let%test_module _ =
[%expect [%expect
{| {|
%x_5 = %y_6 %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 let%test _ = entails_eq r1 x y
@ -118,7 +123,10 @@ let%test_module _ =
%x_5 = %y_6 = %z_7 = ((u8) %x_5) %x_5 = %y_6 = %z_7 = ((u8) %x_5)
{sat= true; {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 r2 x z
let%test _ = entails_eq (or_ r1 r2) x y let%test _ = entails_eq (or_ r1 r2) x y
@ -139,11 +147,11 @@ let%test_module _ =
pp rs ; pp rs ;
[%expect [%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%test _ =
let r = of_eqs [(w, y); (y, z)] in let r = of_eqs [(w, y); (y, z)] in
@ -162,10 +170,12 @@ let%test_module _ =
= (%y_6 rem %t_1) = (%y_6 rem %t_1)
{sat= true; {sat= true;
rep= [[%u_2 ↦ %t_1]; rep= [[%t_1 ↦ ];
[%u_2 ↦ %t_1];
[%v_3 ↦ %t_1]; [%v_3 ↦ %t_1];
[%w_4 ↦ %t_1]; [%w_4 ↦ %t_1];
[%x_5 ↦ %t_1]; [%x_5 ↦ %t_1];
[%y_6 ↦ ];
[%z_7 ↦ %t_1]; [%z_7 ↦ %t_1];
[(%y_6 rem %v_3) ↦ %t_1]; [(%y_6 rem %v_3) ↦ %t_1];
[(%y_6 rem %z_7) ↦ %t_1]]} |}] [(%y_6 rem %z_7) ↦ %t_1]]} |}]
@ -186,7 +196,8 @@ let%test_module _ =
{sat= true; {sat= true;
rep= [[%w_4 ↦ (%z_7 + 3)]; rep= [[%w_4 ↦ (%z_7 + 3)];
[%x_5 ↦ (%z_7 + 8)]; [%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 _ = entails_eq r4 x (w + !5)
let%test _ = difference r4 x w |> Poly.equal (Some (Z.of_int 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 %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; {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 |}] %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 %v_3 = %w_4 = %x_5 = %y_6 = %z_7
{sat= true; {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 let%test _ = normalize r7' w |> Term.equal v
@ -267,7 +291,7 @@ let%test_module _ =
{| {|
(13 × %z_7) = %x_5 ∧ 14 = %y_6 (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 let%test _ = entails_eq r8 y !14
@ -280,7 +304,7 @@ let%test_module _ =
{| {|
(%z_7 + -16) = %x_5 (%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)) 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 (%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) (-1 × %x_5 + %z_7 + -8)
@ -327,7 +351,11 @@ let%test_module _ =
[%expect [%expect
{| {|
{sat= true; {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 *) let%test _ = not (is_false r13) (* incomplete *)
@ -335,7 +363,9 @@ let%test_module _ =
let r14 = of_eqs [(a, a); (x, !1)] let r14 = of_eqs [(a, a); (x, !1)]
let%expect_test _ = 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_ let%test _ = entails_eq r14 a Term.true_
@ -346,7 +376,8 @@ let%test_module _ =
pp r14 ; pp r14 ;
[%expect [%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 a Term.true_
let%test _ = entails_eq r14 b 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 r15 = of_eqs [(b, b); (x, !1)]
let%expect_test _ = 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 b (Term.signed 1 !1)
let%test _ = entails_eq r15 (Term.unsigned 1 b) !1 let%test _ = entails_eq r15 (Term.unsigned 1 b) !1
@ -370,6 +403,7 @@ let%test_module _ =
{| {|
{sat= false; {sat= false;
rep= [[%x_5 ↦ (%y_6 + 1)]; rep= [[%x_5 ↦ (%y_6 + 1)];
[%y_6 ↦ ];
[((u8) %y_6) ↦ (%y_6 + -2)]; [((u8) %y_6) ↦ (%y_6 + -2)];
[((u8) (%x_5 + -1)) ↦ (%y_6 + 3)]]} |}] [((u8) (%x_5 + -1)) ↦ (%y_6 + 3)]]} |}]
@ -383,7 +417,8 @@ let%test_module _ =
[%expect [%expect
{| {|
{sat= false; {sat= false;
rep= [[%y_6 ↦ %x_5]; rep= [[%x_5 ↦ ];
[%y_6 ↦ %x_5];
[((u8) %x_5) ↦ %x_5]; [((u8) %x_5) ↦ %x_5];
[((u8) %y_6) ↦ (%x_5 + -1)]]} |}] [((u8) %y_6) ↦ (%x_5 + -1)]]} |}]
@ -396,7 +431,10 @@ let%test_module _ =
[%expect [%expect
{| {|
{sat= true; {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) |}] %x_5 = ((u8) %x_5) ∧ (%y_6 + -1) = ((u8) %y_6) |}]

Write Preview
Loading…
Cancel
Save