From 867131e964d5e6d98d05278ffd52bf762f8f57fe Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Sat, 15 Aug 2020 02:18:47 -0700
Subject: [PATCH] [sledge] Change: Generalize entails_eq to implies

Summary:
Generalize Fol interface to allow checking if a context implies any
formula, rather than restricting to only equalities.

Reviewed By: jvillard

Differential Revision: D22571144

fbshipit-source-id: 726bd87fd
---
 sledge/src/fol.ml               |  5 ++--
 sledge/src/fol.mli              |  6 ++--
 sledge/src/ses/equality.ml      | 16 ++++++-----
 sledge/src/ses/equality.mli     |  4 +--
 sledge/src/ses/equality_test.ml | 49 +++++++++++++++++----------------
 sledge/src/sh.ml                |  5 ++--
 sledge/src/solver.ml            |  4 +--
 7 files changed, 48 insertions(+), 41 deletions(-)

diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 9cb827631..0ea15f3f8 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -1212,7 +1212,7 @@ module Context = struct
   let fv x = vs_of_ses (Ses.Equality.fv x)
   let is_true x = Ses.Equality.is_true x
   let is_false x = Ses.Equality.is_false x
-  let entails_eq x e f = Ses.Equality.entails_eq x (to_ses e) (to_ses f)
+  let implies x b = Ses.Equality.implies 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))
@@ -1238,7 +1238,8 @@ module Context = struct
   let diff_classes r s =
     Term.Map.filter_mapi (classes r) ~f:(fun ~key:rep ~data:cls ->
         match
-          List.filter cls ~f:(fun exp -> not (entails_eq s rep exp))
+          List.filter cls ~f:(fun exp ->
+              not (implies s (Formula.eq rep exp)) )
         with
         | [] -> None
         | cls -> Some cls )
diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli
index cd521c924..504b6248e 100644
--- a/sledge/src/fol.mli
+++ b/sledge/src/fol.mli
@@ -218,8 +218,10 @@ module Context : sig
   val is_false : t -> bool
   (** Test if the relation is empty / inconsistent. *)
 
-  val entails_eq : t -> Term.t -> Term.t -> bool
-  (** Test if an equation is entailed by a relation. *)
+  val implies : t -> Formula.t -> bool
+  (** [implies x f] holds only if [f] is a logical consequence of [x]. This
+      only checks if [f] is valid in the current state of [x], without doing
+      any further logical reasoning or propagation. *)
 
   val class_of : t -> Term.t -> Term.t list
   (** Equivalence class of [e]: all the terms [f] in the relation such that
diff --git a/sledge/src/ses/equality.ml b/sledge/src/ses/equality.ml
index cd5296fa2..7a8b60d1c 100644
--- a/sledge/src/ses/equality.ml
+++ b/sledge/src/ses/equality.ml
@@ -561,10 +561,10 @@ let is_true {sat; rep} =
 
 let is_false {sat} = not sat
 
-let entails_eq r d e =
-  [%Trace.call fun {pf} -> pf "%a = %a@ %a" Term.pp d Term.pp e pp r]
+let implies r b =
+  [%Trace.call fun {pf} -> pf "%a@ %a" Term.pp b pp r]
   ;
-  Term.is_true (Term.eq (canon r d) (canon r e))
+  Term.is_true (canon r b)
   |>
   [%Trace.retn fun {pf} -> pf "%b"]
 
@@ -630,7 +630,9 @@ let or_ us r s =
           List.fold cls
             ~init:([rep], rs)
             ~f:(fun (reps, rs) exp ->
-              match List.find ~f:(entails_eq r exp) reps with
+              match
+                List.find ~f:(fun rep -> implies r (Term.eq exp rep)) reps
+              with
               | Some rep -> (reps, and_eq_ us exp rep rs)
               | None -> (exp :: reps, rs) )
           |> snd )
@@ -934,7 +936,7 @@ let solve_concat_extracts_eq r x =
   let find_extracts_at_off off =
     List.filter uses ~f:(fun use ->
         match (use : Term.t) with
-        | Ap3 (Extract, _, o, _) -> entails_eq r o off
+        | Ap3 (Extract, _, o, _) -> implies r (Term.eq o off)
         | _ -> false )
   in
   let rec find_extracts full_rev_extracts rev_prefix off =
@@ -943,7 +945,7 @@ let solve_concat_extracts_eq r x =
         match e with
         | Ap3 (Extract, Ap2 (Sized, n, _), o, l) ->
             let o_l = Term.add o l in
-            if entails_eq r n o_l then
+            if implies r (Term.eq n o_l) then
               (e :: rev_prefix) :: full_rev_extracts
             else find_extracts full_rev_extracts (e :: rev_prefix) o_l
         | _ -> full_rev_extracts )
@@ -1029,7 +1031,7 @@ let solve_for_vars vss r =
     pf "%a" Subst.pp subst ;
     Subst.iteri subst ~f:(fun ~key ~data ->
         assert (
-          entails_eq r key data
+          implies r (Term.eq key data)
           || fail "@[%a@ = %a@ not entailed by@ @[%a@]@]" Term.pp key
                Term.pp data pp_classes r () ) ;
         assert (
diff --git a/sledge/src/ses/equality.mli b/sledge/src/ses/equality.mli
index 29ddb36c7..b945bc197 100644
--- a/sledge/src/ses/equality.mli
+++ b/sledge/src/ses/equality.mli
@@ -56,8 +56,8 @@ val is_true : t -> bool
 val is_false : t -> bool
 (** Test if the relation is empty / inconsistent. *)
 
-val entails_eq : t -> Term.t -> Term.t -> bool
-(** Test if an equation is entailed by a relation. *)
+val implies : t -> Term.t -> bool
+(** Test if a term is implied by a relation. *)
 
 val class_of : t -> Term.t -> Term.t list
 (** Equivalence class of [e]: all the terms [f] in the relation such that
diff --git a/sledge/src/ses/equality_test.ml b/sledge/src/ses/equality_test.ml
index 2c67353f1..d9b5d8d5d 100644
--- a/sledge/src/ses/equality_test.ml
+++ b/sledge/src/ses/equality_test.ml
@@ -49,6 +49,7 @@ let%test_module _ =
         l
       |> snd
 
+    let implies_eq r a b = implies r (Term.eq a b)
     let and_eq a b r = and_eq wrt a b r |> snd
     let and_ r s = and_ wrt r s |> snd
     let or_ r s = or_ wrt r s |> snd
@@ -122,7 +123,7 @@ let%test_module _ =
 
       {sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [-1 ↦ ]; [0 ↦ ]]} |}]
 
-    let%test _ = entails_eq r1 x y
+    let%test _ = implies_eq r1 x y
 
     let r2 = of_eqs [(x, y); (f x, y); (f y, z)]
 
@@ -141,14 +142,14 @@ let%test_module _ =
              [-1 ↦ ];
              [0 ↦ ]]} |}]
 
-    let%test _ = entails_eq r2 x z
-    let%test _ = entails_eq (or_ r1 r2) x y
-    let%test _ = not (entails_eq (or_ r1 r2) x z)
-    let%test _ = entails_eq (or_ f1 r2) x z
-    let%test _ = entails_eq (or_ r2 f3) x z
-    let%test _ = entails_eq r2 (f y) y
-    let%test _ = entails_eq r2 (f x) (f z)
-    let%test _ = entails_eq r2 (g x y) (g z y)
+    let%test _ = implies_eq r2 x z
+    let%test _ = implies_eq (or_ r1 r2) x y
+    let%test _ = not (implies_eq (or_ r1 r2) x z)
+    let%test _ = implies_eq (or_ f1 r2) x z
+    let%test _ = implies_eq (or_ r2 f3) x z
+    let%test _ = implies_eq r2 (f y) y
+    let%test _ = implies_eq r2 (f x) (f z)
+    let%test _ = implies_eq r2 (g x y) (g z y)
 
     let%expect_test _ =
       let r = of_eqs [(w, y); (y, z)] in
@@ -171,7 +172,7 @@ let%test_module _ =
       let r = of_eqs [(w, y); (y, z)] in
       let s = of_eqs [(x, y); (y, z)] in
       let rs = or_ r s in
-      entails_eq rs y z
+      implies_eq rs y z
 
     let r3 = of_eqs [(g y z, w); (v, w); (g y w, t); (x, v); (x, u); (u, z)]
 
@@ -196,9 +197,9 @@ let%test_module _ =
              [-1 ↦ ];
              [0 ↦ ]]} |}]
 
-    let%test _ = entails_eq r3 t z
-    let%test _ = entails_eq r3 x z
-    let%test _ = entails_eq (and_ r2 r3) x z
+    let%test _ = implies_eq r3 t z
+    let%test _ = implies_eq r3 x z
+    let%test _ = implies_eq (and_ r2 r3) x z
 
     let r4 = of_eqs [(w + !2, x - !3); (x - !5, y + !7); (y, z - !4)]
 
@@ -217,7 +218,7 @@ let%test_module _ =
              [-1 ↦ ];
              [0 ↦ ]]} |}]
 
-    let%test _ = entails_eq r4 x (w + !5)
+    let%test _ = implies_eq r4 x (w + !5)
 
     let r5 = of_eqs [(x, y); (g w x, y); (g w y, f z)]
 
@@ -234,7 +235,7 @@ let%test_module _ =
 
       {sat= true; rep= [[%x_5 ↦ 1]; [%y_6 ↦ 1]; [-1 ↦ ]; [0 ↦ ]]} |}]
 
-    let%test _ = entails_eq r6 x y
+    let%test _ = implies_eq r6 x y
 
     let r7 = of_eqs [(v, x); (w, z); (y, z)]
 
@@ -300,10 +301,10 @@ let%test_module _ =
     let%test _ = normalize r7' w |> Term.equal v
 
     let%test _ =
-      entails_eq (of_eqs [(g w x, g y z); (x, z)]) (g w x) (g w z)
+      implies_eq (of_eqs [(g w x, g y z); (x, z)]) (g w x) (g w z)
 
     let%test _ =
-      entails_eq (of_eqs [(g w x, g y w); (x, z)]) (g w x) (g w z)
+      implies_eq (of_eqs [(g w x, g y w); (x, z)]) (g w x) (g w z)
 
     let r8 = of_eqs [(x + !42, (3 * y) + (13 * z)); (13 * z, x)]
 
@@ -317,7 +318,7 @@ let%test_module _ =
       {sat= true;
        rep= [[%x_5 ↦ (13 × %z_7)]; [%y_6 ↦ 14]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}]
 
-    let%test _ = entails_eq r8 y !14
+    let%test _ = implies_eq r8 y !14
 
     let r11 = of_eqs [(!16, z - x); (x + !8 - z, z - !16 + !8 - z)]
 
@@ -357,7 +358,7 @@ let%test_module _ =
         {|
           {sat= true; rep= [[%x_5 ↦ 1]; [(%x_5 ≠ 0) ↦ -1]; [-1 ↦ ]; [0 ↦ ]]} |}]
 
-    let%test _ = entails_eq r14 a Term.true_
+    let%test _ = implies_eq r14 a Term.true_
 
     let b = Term.dq y !0
     let r14 = of_eqs [(a, b); (x, !1)]
@@ -374,8 +375,8 @@ let%test_module _ =
                  [-1 ↦ ];
                  [0 ↦ ]]} |}]
 
-    let%test _ = entails_eq r14 a Term.true_
-    let%test _ = entails_eq r14 b Term.true_
+    let%test _ = implies_eq r14 a Term.true_
+    let%test _ = implies_eq r14 b Term.true_
 
     let b = Term.dq x !0
     let r15 = of_eqs [(b, b); (x, !1)]
@@ -386,8 +387,8 @@ let%test_module _ =
         {|
           {sat= true; rep= [[%x_5 ↦ 1]; [(%x_5 ≠ 0) ↦ -1]; [-1 ↦ ]; [0 ↦ ]]} |}]
 
-    let%test _ = entails_eq r15 b (Term.signed 1 !1)
-    let%test _ = entails_eq r15 (Term.unsigned 1 b) !1
+    let%test _ = implies_eq r15 b (Term.signed 1 !1)
+    let%test _ = implies_eq r15 (Term.unsigned 1 b) !1
 
     (* f(x−1)−1=x+1, f(y)+1=y−1, y+1=x ⊢ false *)
     let r16 =
@@ -449,5 +450,5 @@ let%test_module _ =
           {sat= true;
            rep= [[%x_5 ↦ 0]; [%y_6 ↦ 0]; [%z_7 ↦ 0]; [-1 ↦ ]; [0 ↦ ]]} |}]
 
-    let%test _ = entails_eq r19 z !0
+    let%test _ = implies_eq r19 z !0
   end )
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 8c9e432bb..b8e23866c 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -185,7 +185,8 @@ let pp_heap x ?pre ctx fs heap =
   let break s1 s2 =
     (not (Term.equal s1.bas s2.bas))
     || (not (Term.equal s1.len s2.len))
-    || not (Context.entails_eq ctx (Term.add s1.loc s1.siz) s2.loc)
+    || not
+         (Context.implies ctx (Formula.eq (Term.add s1.loc s1.siz) s2.loc))
   in
   let heap = List.map heap ~f:(map_seg ~f:(Context.normalize ctx)) in
   let blocks = List.group ~break (List.sort ~compare heap) in
@@ -591,7 +592,7 @@ let is_false = function
   | {ctx; pure; heap; _} ->
       Formula.is_false (Context.normalizef ctx pure)
       || List.exists heap ~f:(fun seg ->
-             Context.entails_eq ctx seg.loc Term.zero )
+             Context.implies ctx (Formula.eq seg.loc Term.zero) )
 
 let rec pure_approx ({us; xs; ctx; pure; heap= _; djns} as q) =
   let heap = emp.heap in
diff --git a/sledge/src/solver.ml b/sledge/src/solver.ml
index 26d26a90c..c6b66f0fb 100644
--- a/sledge/src/solver.ml
+++ b/sledge/src/solver.ml
@@ -563,8 +563,8 @@ let excise_seg ({sub} as goal) msg ssg =
   let {Sh.loc= l; bas= b'; len= m'; siz= n} = ssg in
   let* k_l = Context.difference sub.ctx k l in
   if
-    (not (Context.entails_eq sub.ctx b b'))
-    || not (Context.entails_eq sub.ctx m m')
+    (not (Context.implies sub.ctx (Formula.eq b b')))
+    || not (Context.implies sub.ctx (Formula.eq m m'))
   then
     Some
       ( goal