From 9865bc0f741e9f6bd4263289845d3adb6f6c0e6a Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 16 Jul 2019 02:24:56 -0700 Subject: [PATCH] [sledge] [solver] Strengthen handling of existential subtrahends MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Summary: A frame inference query `Minuend ⊢ ∃xs. Subtrahend` returns a `∃zs. Remainder` formula such that `Minuend ⊢ ∃xs. Subtrahend * ∃zs. Remainder` when successful. Currently if the subtrahend is itself existentially quantified, its existentials are treated trivially: they must witness themselves. This diff allows the solver to find witnesses as the `xs`. They are still existentially quantified in the remainder, so clients that need to constrain them should still name them before calling the solver. Reviewed By: kren1 Differential Revision: D16269630 fbshipit-source-id: 65136edd1 --- sledge/src/symbheap/solver.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/sledge/src/symbheap/solver.ml b/sledge/src/symbheap/solver.ml index 1d9d14a16..ecfb1db45 100644 --- a/sledge/src/symbheap/solver.ml +++ b/sledge/src/symbheap/solver.ml @@ -605,9 +605,9 @@ let excise_dnf : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option = [%Trace.info "@[<2>subtrahend@ %a@]" Sh.pp sub] ; let sub = Sh.extend_us us sub in let ws, sub = Sh.bind_exists sub ~wrt:xs in + let xs = Set.union xs ws in let sub = Sh.and_cong min.cong sub in let zs = Var.Set.empty in - let min = Sh.extend_us ws min in excise {us; com; min; xs; sub; zs; pgs= true} >>| fun remainder -> Sh.exists (Set.union ys ws) remainder ) >>| fun remainder -> Sh.or_ remainders remainder )