From 0cbcb878f9970b36123e018d25ffb709db1a7d30 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 21 May 2019 08:32:30 -0700
Subject: [PATCH] [sledge] Classify fully-interpreted and simplified exps
 differently
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Summary:
For some Exp forms, Exp.solve is not complete, and this is necessary
since the result of solve is a substitution that needs to encode the
input equation as a conjunction of equations each between a variable
and an exp. This is tantamount to, stronger even than, the theory
being convex. So Exp.solve is not complete for some exps, and some of
those have constructors that perform some simplification. For example,
`(1 ≠ 0)` simplifies to `-1` (i.e. true). To enable deductions such as
`((x ≠ 0) = b) && x = 1 |- b = -1` needs the equality solver to
substitute through subexps of simplifiable exps like = and ≠, as it
does for interpreted exps like + and ×. At the same time, since
Exp.solve for non-interpreted exps cannot be complete, to enable
deductions such as `((x ≠ 0) = (y ≠ 0)) && x = 1 |- y ≠ 0` needs the
equality solver to congruence-close over subexps of simplifiable exps
such as = and ≠, as it does for uninterpreted exps.

To strengthen the equality solver in these sorts of cases, this diff
adds a new class of exps for = and ≠, and revises the equality solver
to handle them in a hybrid fashion between interpreted and
uninterpreted.

I am not currently sure whether or not this breaks the termination
proof, but I have also not managed to adapt usual divergent cases to
break this. One notable point is that simplifying = and ≠ exps always
produces genuinely simpler and smaller exps, in contrast to
e.g. polynomial simplification and gaussian elimination.

Note that the real solution to this problem is likely to be to
eliminate the i1 type in favor or a genuine boolean type, and
translate all integer operations on i1 to boolean/logical ones. Then
the disjunction implicit in e.g. equations between disequations would
appear as actual disjunction, and could be dealt with as such.

Reviewed By: jvillard

Differential Revision: D15424823

fbshipit-source-id: 67d62df1f
---
 sledge/src/llair/exp.ml              |  3 +-
 sledge/src/llair/exp.mli             |  2 +-
 sledge/src/symbheap/equality.ml      | 24 +++++++---
 sledge/src/symbheap/equality_test.ml | 67 +++++++++++++++++++++++++++-
 4 files changed, 86 insertions(+), 10 deletions(-)

diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml
index 5003eb716..0615e4064 100644
--- a/sledge/src/llair/exp.ml
+++ b/sledge/src/llair/exp.ml
@@ -1319,7 +1319,8 @@ let rec is_constant e =
   | _ -> true
 
 let classify = function
-  | Add _ | Mul _ | App {op= Eq | Dq | App {op= Eq | Dq}} -> `Interpreted
+  | Add _ | Mul _ -> `Interpreted
+  | App {op= Eq | Dq | App {op= Eq | Dq}} -> `Simplified
   | App _ -> `Uninterpreted
   | _ -> `Atomic
 
diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli
index 82f61b4d1..c82866c11 100644
--- a/sledge/src/llair/exp.mli
+++ b/sledge/src/llair/exp.mli
@@ -206,5 +206,5 @@ val fv : t -> Var.Set.t
 val is_true : t -> bool
 val is_false : t -> bool
 val typ : t -> Typ.t option
-val classify : t -> [> `Atomic | `Interpreted | `Uninterpreted]
+val classify : t -> [> `Atomic | `Interpreted | `Simplified | `Uninterpreted]
 val solve : t -> t -> (t, t, comparator_witness) Map.t option
diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml
index 8a9ce6f81..1fa9527b7 100644
--- a/sledge/src/symbheap/equality.ml
+++ b/sledge/src/symbheap/equality.ml
@@ -111,7 +111,8 @@ let apply s a = try Map.find_exn s a with Caml.Not_found -> a
 let rec norm s a =
   match Exp.classify a with
   | `Interpreted -> Exp.map ~f:(norm s) a
-  | _ -> apply s a
+  | `Simplified -> apply s (Exp.map ~f:(norm s) a)
+  | `Atomic | `Uninterpreted -> apply s a
 
 (** exps are congruent if equal after normalizing subexps *)
 let congruent r a b =
@@ -132,14 +133,14 @@ let lookup r a =
 let rec canon r a =
   match Exp.classify a with
   | `Interpreted -> Exp.map ~f:(canon r) a
-  | `Uninterpreted -> lookup r (Exp.map ~f:(canon r) a)
+  | `Simplified | `Uninterpreted -> lookup r (Exp.map ~f:(canon r) a)
   | `Atomic -> apply r.rep a
 
 (** add an exp to the carrier *)
 let rec extend a r =
   match Exp.classify a with
-  | `Interpreted -> Exp.fold ~f:extend a ~init:r
-  | _ ->
+  | `Interpreted | `Simplified -> Exp.fold ~f:extend a ~init:r
+  | `Atomic | `Uninterpreted ->
       Map.find_or_add r.rep a
         ~if_found:(fun _ -> r)
         ~default:a
@@ -154,7 +155,7 @@ let compose r s =
         if Exp.equal v1 v2 then v1
         else fail "domains intersect: %a" Exp.pp key () )
   in
-  {r with rep} |> check invariant
+  {r with rep}
 
 let merge a b r =
   [%Trace.call fun {pf} -> pf "%a@ %a@ %a" Exp.pp a Exp.pp b pp r]
@@ -187,6 +188,15 @@ let rec close r =
     | Some (a', b') -> close (merge a' b' r)
     | None -> r
 
+let close r =
+  [%Trace.call fun {pf} -> pf "%a" pp r]
+  ;
+  close r
+  |>
+  [%Trace.retn fun {pf} r' ->
+    pf "%a" pp_diff (r, r') ;
+    invariant r']
+
 let and_eq a b r =
   if not r.sat then r
   else
@@ -266,7 +276,9 @@ let map_exps ({sat= _; rep} as r) ~f =
   in
   (if rep' == rep then r else {r with rep= rep'})
   |>
-  [%Trace.retn fun {pf} r -> pf "%a" pp r ; invariant r]
+  [%Trace.retn fun {pf} r' ->
+    pf "%a" pp_diff (r, r') ;
+    invariant r']
 
 let rename r sub = map_exps r ~f:(fun e -> Exp.rename e sub)
 
diff --git a/sledge/src/symbheap/equality_test.ml b/sledge/src/symbheap/equality_test.ml
index 9ce11e30c..127d9b95b 100644
--- a/sledge/src/symbheap/equality_test.ml
+++ b/sledge/src/symbheap/equality_test.ml
@@ -9,9 +9,9 @@ let%test_module _ =
   ( module struct
     open Equality
 
-    (* let () = Trace.init ~margin:160 ~config:all () *)
-
     let () = Trace.init ~margin:68 ~config:none ()
+
+    (* let () = Trace.init ~margin:160 ~config:all () *)
     let printf pp = Format.printf "@\n%a@." pp
     let pp = printf pp
     let pp_classes = printf pp_classes
@@ -327,4 +327,67 @@ let%test_module _ =
     let r12 = of_eqs [(!16, z - x); (x + !8 - z, z + !16 + !8 - z)]
 
     let%expect_test _ = pp_classes r12 ; [%expect {| (%z_7 + -16) = %x_5 |}]
+
+    let r13 = of_eqs [(Exp.eq x !2, y); (Exp.dq x !2, z); (y, z)]
+
+    let%expect_test _ =
+      pp r13 ;
+      [%expect
+        {|
+      {sat= true;
+       rep= [[%x_5 ↦ ];
+             [%y_6 ↦ ];
+             [%z_7 ↦ %y_6];
+             [(%x_5 = 2) ↦ %y_6];
+             [(%x_5 ≠ 2) ↦ %y_6];
+             [= ↦ ];
+             [≠ ↦ ];
+             [2 ↦ ]]} |}]
+
+    let%test _ = not (is_false r13) (* incomplete *)
+
+    let a = Exp.dq x !0
+    let r14 = of_eqs [(a, a); (x, !1)]
+
+    let%expect_test _ =
+      pp r14 ;
+      [%expect
+        {| {sat= true; rep= [[%x_5 ↦ 1]; [≠ ↦ ]; [0 ↦ ]; [1 ↦ ]]} |}]
+
+    let%test _ = entails_eq r14 a (Exp.bool true)
+
+    let b = Exp.dq y !0
+    let r14 = of_eqs [(a, b); (x, !1)]
+
+    let%expect_test _ =
+      pp r14 ;
+      [%expect
+        {|
+          {sat= true;
+           rep= [[%x_5 ↦ 1];
+                 [%y_6 ↦ ];
+                 [(%y_6 ≠ 0) ↦ -1];
+                 [≠ ↦ ];
+                 [0 ↦ ];
+                 [1 ↦ ]]} |}]
+
+    let%test _ = entails_eq r14 a (Exp.bool true)
+    let%test _ = entails_eq r14 b (Exp.bool true)
+
+    let b = Exp.convert ~dst:i64 ~src:i8 (Exp.dq x !0)
+    let r15 = of_eqs [(b, b); (x, !1)]
+
+    let%expect_test _ =
+      pp r15 ;
+      [%expect
+        {|
+          {sat= true;
+           rep= [[%x_5 ↦ 1];
+                 [((i64)(i8) (%x_5 ≠ 0)) ↦ 1];
+                 [≠ ↦ ];
+                 [(i64)(i8) ↦ ];
+                 [0 ↦ ];
+                 [1 ↦ ]]} |}]
+
+    let%test _ = entails_eq r15 b !1
   end )