[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

@@ -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)

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

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 =
-  let first = Term.Map.is_empty clss in
+    if Option.is_some var_strength then
-  if not first then Format.fprintf fs "  " ;
+      Context.ppx_diff x fs parent_ctx pure ctx
-  Context.ppx_classes x fs clss ;
+    else (
-  let pure =
+      Format.fprintf fs "@[  %a@]" Formula.pp pure ;
-    if Option.is_none var_strength then [pure]
+      false )
-    else
-      let pure' = Context.normalizef ctx pure in
-      if Formula.is_true pure' then [] else [pure']
   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 =

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, %x_7 .   (%x_7 = 2) ∧ emp)
-        ∨ (∃ %x_6 .   1 = %x_6 = %y_7 ∧ ((%x_6 = 1) ∧ (%y_7 = 1)) ∧ emp)
+        ∨ (∃ %x_6 .   ((%x_6 = 1) ∧ (%y_7 = 1)) ∧ emp)
-        ∨ (  0 = %x_6 ∧ (%x_6 = 0) ∧ 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, %x_9 .   (%x_9 = 2) ∧ emp)
-        ∨ (∃ %x_6, %x_8 .
+        ∨ (∃ %x_6, %x_8 .   ((%x_8 = 1) ∧ (%y_7 = 1)) ∧ emp)
-             1 = %y_7 = %x_8
+        ∨ (∃ %x_6 .   (%x_6 = 0) ∧ emp)
-           ∧ ((%x_8 = 1) ∧ (%y_7 = 1))
-           ∧ emp)
-        ∨ (∃ %x_6 .   0 = %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 .
+          ∨ (∃ %b_2 .   (⟨8,%a_1⟩ = (⟨4,%c_3⟩^⟨4,%b_2⟩)) ∧ emp)
-               (⟨4,%c_3⟩^⟨4,%b_2⟩) = %a_1
-             ∧ (⟨8,%a_1⟩ = (⟨4,%c_3⟩^⟨4,%b_2⟩))
-             ∧ emp)
           )
 
           tt ∧ emp * ( (  tt ∧ emp) ∨ (  (%x_6 ≠ 0) ∧ emp) )