[sledge] Fix bug in Equality.or_

Summary:
Equality.or_ assumed a simpler representation of equality relations,
and was incomplete as a result.

Reviewed By: jvillard

Differential Revision: D18298138

fbshipit-source-id: cf91229f6

sledge/src/symbheap/equality.ml

@@ -250,17 +250,27 @@ let and_ r s =
     Map.fold s.rep ~init:r ~f:(fun ~key:e ~data:e' r -> and_eq e e' r)
 
 let or_ r s =
-  if not s.sat then r
+  [%Trace.call fun {pf} -> pf "@[<hv 1>   %a@ @<2>∨ %a@]" pp r pp s]
+  ;
+  ( if not s.sat then r
   else if not r.sat then s
   else
     let merge_mems rs r s =
-      Map.fold s.rep ~init:rs ~f:(fun ~key:e ~data:e' rs ->
+      Map.fold (classes s) ~init:rs ~f:(fun ~key:rep ~data:cls rs ->
-          if entails_eq r e e' then and_eq e e' rs else rs )
+          List.fold cls
+            ~init:([rep], rs)
+            ~f:(fun (reps, rs) exp ->
+              match List.find ~f:(entails_eq r exp) reps with
+              | Some rep -> (reps, and_eq exp rep rs)
+              | None -> (exp :: reps, rs) )
+          |> snd )
     in
     let rs = true_ in
     let rs = merge_mems rs r s in
     let rs = merge_mems rs s r in
-    rs
+    rs )
+  |>
+  [%Trace.retn fun {pf} -> pf "%a" pp]
 
 (* assumes that f is injective and for any set of terms E, f[E] is disjoint
    from E *)

sledge/src/symbheap/equality_test.ml

@@ -112,6 +112,27 @@ let%test_module _ =
     let%test _ = entails_eq r2 (g x y) (g z y)
     let%test _ = difference (or_ r1 r2) x z |> Poly.equal None
 
+    let%expect_test _ =
+      let r = of_eqs [(w, y); (y, z)] in
+      let s = of_eqs [(x, y); (y, z)] in
+      let rs = or_ r s in
+      pp r ;
+      pp s ;
+      pp rs ;
+      [%expect
+        {|
+        {sat= true; rep= [[%y_6 ↦ %w_4]; [%z_7 ↦ %w_4]]}
+
+        {sat= true; rep= [[%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]]}
+
+        {sat= true; rep= [[%z_7 ↦ %y_6]]} |}]
+
+    let%test _ =
+      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
+
     let r3 = of_eqs [(g y z, w); (v, w); (g y w, t); (x, v); (x, u); (u, z)]
 
     let%expect_test _ =