From df276d7be6eaac39747d5b05be524e096b88ffc6 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sat, 15 Aug 2020 02:19:07 -0700 Subject: [PATCH] [sledge] Change: Move printing of Sh context and pure part to Context Summary: Also, when printing in raw mode, do not print the context. Reviewed By: jvillard Differential Revision: D22571145 fbshipit-source-id: b3596d9cc --- sledge/src/fol.ml | 27 +++++++++++++++++---------- sledge/src/fol.mli | 15 +++------------ sledge/src/sh.ml | 28 +++++++++++++--------------- sledge/src/sh_test.ml | 25 +++++++++---------------- 4 files changed, 42 insertions(+), 53 deletions(-) diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml index 4f197f2d5..79d9bb29c 100644 --- a/sledge/src/fol.ml +++ b/sledge/src/fol.ml @@ -1220,7 +1220,6 @@ module Context = struct Ses.Term.is_false (Ses.Equality.normalize x (f_to_ses b)) let normalize x e = ses_map (Ses.Equality.normalize x) e - let normalizef x e = f_ses_map (Ses.Equality.normalize x) e let difference x e f = Term.d_int (normalize x (Term.sub e f)) let fold_terms ~init x ~f = @@ -1230,8 +1229,6 @@ module Context = struct let class_of x e = List.map ~f:of_ses (Ses.Equality.class_of x (to_ses e)) - type classes = exp list Term.Map.t - let classes_of_ses clss = Ses.Term.Map.fold clss ~init:Term.Map.empty ~f:(fun ~key:rep ~data:cls clss -> @@ -1261,6 +1258,23 @@ module Context = struct let pp_classes fs r = ppx_classes (fun _ -> None) fs (classes r) + let ppx_diff var_strength fs parent_ctx fml ctx = + let clss = diff_classes ctx parent_ctx in + let first = Term.Map.is_empty clss in + if not first then Format.fprintf fs " " ; + ppx_classes var_strength fs clss ; + let fml = + let normalizef x e = f_ses_map (Ses.Equality.normalize x) e in + let fml' = normalizef ctx fml in + if Formula.is_true fml' then [] else [fml'] + in + List.pp + ~pre:(if first then "@[ " else "@ @[@<2>∧ ") + "@ @<2>∧ " + (Formula.ppx var_strength) + fs fml ~suf:"@]" ; + first && List.is_empty fml + (* Substs *) module Subst = struct @@ -1294,7 +1308,6 @@ module Context = struct type call = | Normalize of t * exp - | Normalizef of t * fml | And_formula of Var.Set.t * fml * t | And_ of Var.Set.t * t * t | OrN of Var.Set.t * t list @@ -1306,7 +1319,6 @@ module Context = struct let replay c = match call_of_sexp (Sexp.of_string c) with | Normalize (r, e) -> normalize r e |> ignore - | Normalizef (r, e) -> normalizef r e |> ignore | And_formula (us, e, r) -> and_formula us e r |> ignore | And_ (us, r, s) -> and_ us r s |> ignore | OrN (us, rs) -> orN us rs |> ignore @@ -1349,11 +1361,6 @@ module Context = struct let normalize r e = wrap normalize_tmr (fun () -> normalize r e) (fun () -> Normalize (r, e)) - let normalizef r e = - wrap normalize_tmr - (fun () -> normalizef r e) - (fun () -> Normalizef (r, e)) - let and_formula us e r = wrap and_formula_tmr (fun () -> and_formula us e r) diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli index d52995637..eb6bd7c37 100644 --- a/sledge/src/fol.mli +++ b/sledge/src/fol.mli @@ -180,19 +180,12 @@ end (** Inference System *) module Context : sig type t [@@deriving sexp] - type classes = Term.t list Term.Map.t - - val classes : t -> classes - (** [classes r] maps each equivalence class representative to the other - terms [r] proves equal to it. *) - - val diff_classes : t -> t -> classes - (** [diff_classes r s] is the equality classes of [r] omitting equalities - in [s]. *) val pp : t pp val pp_classes : t pp - val ppx_classes : Var.strength -> classes pp + + val ppx_diff : + Var.strength -> Format.formatter -> t -> Formula.t -> t -> bool include Invariant.S with type t := t @@ -237,8 +230,6 @@ module Context : sig relation, where [e'] and its subterms are expressed in terms of the relation's canonical representatives of each equivalence class. *) - val normalizef : t -> Formula.t -> Formula.t - val difference : t -> Term.t -> Term.t -> Z.t option (** The difference as an offset. [difference r a b = Some k] if [r] implies [a = b+k], or [None] if [a] and [b] are not equal up to an diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml index 674706281..6cbe90b5d 100644 --- a/sledge/src/sh.ml +++ b/sledge/src/sh.ml @@ -217,20 +217,13 @@ let rec pp_ ?var_strength vs parent_xs parent_ctx fs if not (Var.Set.is_empty xs_d_vs) then Format.fprintf fs "@ " ) ; if not (Var.Set.is_empty xs_d_vs) then Format.fprintf fs "@<2>∃ @[%a@] .@ " (Var.Set.ppx x) xs_d_vs ; - let clss = Context.diff_classes ctx parent_ctx in - let first = Term.Map.is_empty clss in - if not first then Format.fprintf fs " " ; - Context.ppx_classes x fs clss ; - let pure = - if Option.is_none var_strength then [pure] - else - let pure' = Context.normalizef ctx pure in - if Formula.is_true pure' then [] else [pure'] + let first = + if Option.is_some var_strength then + Context.ppx_diff x fs parent_ctx pure ctx + else ( + Format.fprintf fs "@[ %a@]" Formula.pp pure ; + false ) in - List.pp - ~pre:(if first then "@[ " else "@ @[@<2>∧ ") - "@ @<2>∧ " (Formula.ppx x) fs pure ~suf:"@]" ; - let first = first && List.is_empty pure in if List.is_empty heap then Format.fprintf fs ( if first then if List.is_empty djns then " emp" else "" @@ -265,8 +258,13 @@ let pp_diff_eq ?(us = Var.Set.empty) ?(xs = Var.Set.empty) ctx fs q = pp_ ~var_strength:(var_strength ~xs q) us xs ctx fs q let pp fs q = pp_diff_eq Context.true_ fs q -let pp_djn fs d = pp_djn Var.Set.empty Var.Set.empty Context.true_ fs d -let pp_raw fs q = pp_ Var.Set.empty Var.Set.empty Context.true_ fs q + +let pp_djn fs d = + pp_djn ?var_strength:None Var.Set.empty Var.Set.empty Context.true_ fs d + +let pp_raw fs q = + pp_ ?var_strength:None Var.Set.empty Var.Set.empty Context.true_ fs q + let fv_seg seg = fold_vars_seg seg ~f:Var.Set.add ~init:Var.Set.empty let fv ?ignore_ctx q = diff --git a/sledge/src/sh_test.ml b/sledge/src/sh_test.ml index ba235e0c8..282b80447 100644 --- a/sledge/src/sh_test.ml +++ b/sledge/src/sh_test.ml @@ -84,9 +84,9 @@ let%test_module _ = ∨ ( ( ( 1 = _ = %y_7 ∧ emp) ∨ ( 2 = _ ∧ emp) )) ) - ( (∃ %x_6, %x_7 . 2 = %x_7 ∧ (%x_7 = 2) ∧ emp) - ∨ (∃ %x_6 . 1 = %x_6 = %y_7 ∧ ((%x_6 = 1) ∧ (%y_7 = 1)) ∧ emp) - ∨ ( 0 = %x_6 ∧ (%x_6 = 0) ∧ emp) + ( (∃ %x_6, %x_7 . (%x_7 = 2) ∧ emp) + ∨ (∃ %x_6 . ((%x_6 = 1) ∧ (%y_7 = 1)) ∧ emp) + ∨ ( (%x_6 = 0) ∧ emp) ) |}] let%expect_test _ = @@ -109,12 +109,9 @@ let%test_module _ = ∨ ( ( ( 1 = _ = %y_7 ∧ emp) ∨ ( 2 = _ ∧ emp) )) ) - ( (∃ %x_6, %x_8, %x_9 . 2 = %x_9 ∧ (%x_9 = 2) ∧ emp) - ∨ (∃ %x_6, %x_8 . - 1 = %y_7 = %x_8 - ∧ ((%x_8 = 1) ∧ (%y_7 = 1)) - ∧ emp) - ∨ (∃ %x_6 . 0 = %x_6 ∧ (%x_6 = 0) ∧ emp) + ( (∃ %x_6, %x_8, %x_9 . (%x_9 = 2) ∧ emp) + ∨ (∃ %x_6, %x_8 . ((%x_8 = 1) ∧ (%y_7 = 1)) ∧ emp) + ∨ (∃ %x_6 . (%x_6 = 0) ∧ emp) ) |}] let%expect_test _ = @@ -149,7 +146,7 @@ let%test_module _ = {| ∃ %x_6 . %x_6 = %x_6^ ∧ (-1 + %y_7) = %y_7^ ∧ emp - (-1 + %y_7) = %y_7^ ∧ (%y_7^ = (-1 + %y_7)) ∧ emp + (%y_7^ = (-1 + %y_7)) ∧ emp (-1 + %y_7) = %y_7^ ∧ emp |}] @@ -172,14 +169,10 @@ let%test_module _ = [%expect {| ∃ %a_1, %c_3, %d_4, %e_5 . - (⟨8,%a_1⟩^⟨8,%d_4⟩) = %e_5 - ∧ ((⟨16,%e_5⟩ = (⟨8,%a_1⟩^⟨8,%d_4⟩)) ∧ tt) + ((⟨16,%e_5⟩ = (⟨8,%a_1⟩^⟨8,%d_4⟩)) ∧ tt) ∧ emp * ( ( (%x_6 ≠ 0) ∧ emp) - ∨ (∃ %b_2 . - (⟨4,%c_3⟩^⟨4,%b_2⟩) = %a_1 - ∧ (⟨8,%a_1⟩ = (⟨4,%c_3⟩^⟨4,%b_2⟩)) - ∧ emp) + ∨ (∃ %b_2 . (⟨8,%a_1⟩ = (⟨4,%c_3⟩^⟨4,%b_2⟩)) ∧ emp) ) tt ∧ emp * ( ( tt ∧ emp) ∨ ( (%x_6 ≠ 0) ∧ emp) )