[sledge] Fix bug in quantifier handling during Sh.or simplification

Summary:
P ∨ (∃x. Q ∨ R) could be simplified to (∃x. P ∨ Q ∨ R) and capture
occurrences of x in P.

Reviewed By: ngorogiannis

Differential Revision: D14481990

fbshipit-source-id: 92b474d59
master
Josh Berdine 6 years ago committed by Facebook Github Bot
parent e7374bc62e
commit 0bef279ed1

@ -314,8 +314,13 @@ let or_ q1 q2 =
| _, {djns= [[]]; _} -> | _, {djns= [[]]; _} ->
let us = Set.union q1.us q2.us in let us = Set.union q1.us q2.us in
if us == q1.us then q1 else {q1 with us} if us == q1.us then q1 else {q1 with us}
| ({djns= []; _} as q), ({pure= []; heap= []; djns= [djn]; _} as d) | ( ({djns= []; _} as q)
|({pure= []; heap= []; djns= [djn]; _} as d), ({djns= []; _} as q) -> , ({us= _; xs; cong= _; pure= []; heap= []; djns= [djn]} as d) )
when Set.is_empty xs ->
{d with us= Set.union q.us d.us; djns= [q :: djn]}
| ( ({us= _; xs; cong= _; pure= []; heap= []; djns= [djn]} as d)
, ({djns= []; _} as q) )
when Set.is_empty xs ->
{d with us= Set.union q.us d.us; djns= [q :: djn]} {d with us= Set.union q.us d.us; djns= [q :: djn]}
| _ -> | _ ->
{ us= Set.union q1.us q2.us { us= Set.union q1.us q2.us

Loading…
Cancel
Save