search

uwdb / Cosette

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

Invalid generated Coq code when subquery contains predicate #54

Open duremar opened 7 years ago

duremar commented 7 years ago

perhaps something is wrong with processing a predicate with two arguments (b1): cosette_bug

stechu commented 7 years ago

Thanks for the bug report! There is a minor mistake in Coq code generation. @duremar I believe this is fixed through 43cbd27. The web frontend deployment takes about 15 mins to work.

duremar commented 7 years ago

thank you for quick fix i've found another example of invalid code generation:

schema s(??);
table a(s);
predicate p(s);

query q1
`select * from a x where exists ( select * from a y where p(y) )`;

query q2
`select * from a x`;

verify q1 q2;

it works if where p(y) removed from the program but fails otherwise