search

uwdb / Cosette

Cosette is an automated SQL solver.
BSD 2-Clause "Simplified" License
666 stars 54 forks source link

Can't verify queries with const expr #52

Open zedware opened 7 years ago

zedware commented 7 years ago

/ define schema s1, here s1 can contain any number of attributes, but it has to at least contain integer attributes x and y / schema s1(x:int, y:int, ??);

table a(s1); -- table a of schema s1

query q1 -- query 1 select x.x as ax from a x where 1=1;

query q2 -- query 2 select x.x as ax from a x where 0=0;

verify q1 q2; -- verify the equivalence

stechu commented 7 years ago

@zedware which result did you get? I assume it is UNKNOWN?

zedware commented 7 years ago

Result Two queries' equivalence is unknown. Solver runs out of time.

stechu commented 7 years ago

@zedware thank you! this is a known issue. currently we don't interpret predicate. We are working on Cosette 2.0 that will fix this issue.