dandougherty
commented
9 years ago Why do we care if e3 is not equated to a previous element? It violates the bound, sure, but it's hard to image the user caring about the bound add a true upper bound
Sent from my iPhone
On Jan 16, 2015, at 9:16 PM, Salman Saghafi notifications@github.com wrote:
Consider a sequent P(x) => exists y . Q(y)
where a new element is not created in the head of the sequent during the Chase because a maximum depth is reached. In the relaxed mode, the following ground sequents must be passed to the SMT solver: P(e^1) => Q(e^3) => e^3 = e^0 | e^3 = e^1 | e^3 = e^2
where e^3 is a fresh elemet and e^0, e^1 and e^2 are all existing elements.
Notice that the second ground sequent is necessary because we want to force the solver to make the fresh element equal to at least one of the existing elements. Without this sequent, the SMT solver may choose not to collapse the fresh element with any of the previous ones.
— Reply to this email directly or view it on GitHub.
salmans
thedotmatrix
Consider a sequent
P(x) => exists y . Q(y)where a new element is not created in the head of the sequent during the Chase because a maximum depth is reached. In the relaxed mode, the following ground sequents must be passed to the SMT solver:
P(e^1) => Q(e^3)=> e^3 = e^0 | e^3 = e^1 | e^3 = e^2where e^3 is a fresh elemet and e^0, e^1 and e^2 are all existing elements.
Notice that the second ground sequent is necessary because we want to force the solver to make the fresh element equal to at least one of the existing elements. Without this sequent, the SMT solver may choose not to collapse the fresh element with any of the previous ones.