[sledge] [solver] add handling of trivial equality

Summary:
The solver couldn't deal with `∃ a,b . a = b` , so this diff adds
a special case to deal with it.

Reviewed By: ngorogiannis

Differential Revision: D15897953

fbshipit-source-id: d841d3557

sledge/src/symbheap/solver.ml

@@ -60,8 +60,14 @@ let single_existential_occurrence xs exp =
           | _ -> raise Multiple_existential_occurrences )
   with Multiple_existential_occurrences -> Many
 
+let special_cases xs = function
+  | Exp.(App {op= App {op= Eq; arg= Var _}; arg= Var _}) as e ->
+      if Set.is_subset (Exp.fv e) ~of_:xs then Exp.bool true else e
+  | e -> e
+
 let excise_exp ({us; min; xs} as goal) pure exp =
   let exp' = Equality.normalize min.cong exp in
+  let exp' = special_cases xs exp' in
   if Exp.is_true exp' then Some ({goal with pgs= true}, pure)
   else
     match single_existential_occurrence xs exp' with

sledge/src/symbheap/solver_test.ml

@@ -60,6 +60,13 @@ let%test_module _ =
         ( infer_frame: emp * false \- emp
         ) infer_frame: emp * false |}]
 
+    let%expect_test _ =
+      check_frame Sh.emp [n_; m_] (Sh.and_ (Exp.eq m n) Sh.emp) ;
+      [%expect
+        {|
+        ( infer_frame: emp \- ∃ %m_8, %n_9 .   %m_8 = %n_9 ∧ emp
+        ) infer_frame: emp |}]
+
     let%expect_test _ =
       check_frame
         (Sh.seg {loc= l; bas= b; len= m; siz= n; arr= a})