From f1d94d58b052da2efa964a45241c54b066ff8e6a Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 27 Jan 2020 08:20:30 -0800
Subject: [PATCH] [sledge] Strengthen Equality.solve_for_vars for vars under
 Memory
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Summary:
Strengthen Equality.solve_for_vars so that it will solve cases such as
```
∃ a. ⟨n,a⟩ = ⟨m,b⟩^⟨o,c⟩
```

Reviewed By: ngorogiannis

Differential Revision: D19356324

fbshipit-source-id: a57625ba6
---
 sledge/src/symbheap/equality.ml | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml
index d48ee9746..09a20ba22 100644
--- a/sledge/src/symbheap/equality.ml
+++ b/sledge/src/symbheap/equality.ml
@@ -592,6 +592,17 @@ let solve_poly_eq us p' q' subst =
       Subst.compose1 ~key:kill ~data:keep subst
   | Many | Zero -> None
 
+let solve_memory_eq us e' f' subst =
+  match ((e' : Term.t), (f' : Term.t)) with
+  | (Ap2 (Memory, _, (Var _ as v)) as m), u
+   |u, (Ap2 (Memory, _, (Var _ as v)) as m) ->
+      if
+        (not (Set.is_subset (Term.fv m) ~of_:us))
+        && Set.is_subset (Term.fv u) ~of_:us
+      then Some (Subst.compose1 ~key:v ~data:u subst)
+      else None
+  | _ -> None
+
 let solve_interp_eq us e' (cls, subst) =
   [%Trace.call fun {pf} ->
     pf "trm: @[%a@]@ cls: @[%a@]@ subst: @[%a@]" Term.pp e' pp_cls cls
@@ -599,7 +610,9 @@ let solve_interp_eq us e' (cls, subst) =
   ;
   List.find_map cls ~f:(fun f ->
       let f' = Subst.norm subst f in
-      solve_poly_eq us e' f' subst )
+      match solve_memory_eq us e' f' subst with
+      | Some subst -> Some subst
+      | None -> solve_poly_eq us e' f' subst )
   |>
   [%Trace.retn fun {pf} subst' ->
     pf "@[%a@]" Subst.pp_diff (subst, Option.value subst' ~default:subst) ;