From 01e6c5c55804ff790e1c0069046847a3329720fe Mon Sep 17 00:00:00 2001 From: Timotej Kapus Date: Wed, 19 Jun 2019 06:17:24 -0700 Subject: [PATCH] [sledge] [solver] add handling of trivial equality MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 | 6 ++++++ sledge/src/symbheap/solver_test.ml | 7 +++++++ 2 files changed, 13 insertions(+) diff --git a/sledge/src/symbheap/solver.ml b/sledge/src/symbheap/solver.ml index a48fc4997..7f9a35f80 100644 --- a/sledge/src/symbheap/solver.ml +++ b/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 diff --git a/sledge/src/symbheap/solver_test.ml b/sledge/src/symbheap/solver_test.ml index c7aca89b3..29a3523f6 100644 --- a/sledge/src/symbheap/solver_test.ml +++ b/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})