Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Equivalent queries with conditions on a date column generate invalid Coq code #74

Open
milos-simic opened this issue Sep 5, 2019 · 0 comments

Comments

@milos-simic
Copy link

This code:

schema student_schema(indeks:int, ime:varchar, prezime:varchar, datum_upisa:date, datum_rodjenja:date, mesto_rodjenja:varchar);
schema predmet_schema(id_predmeta:int, shifra:char, naziv:varchar, bodovi:int);
schema ispitni_rok_schema(godina_roka:int, oznaka_roka:char, naziv:varchar);
schema ispit_schema(indeks:int, id_predmeta:int, godina_roka:int, oznaka_roka:char, ocena:int, datum_ispita:date, bodovi:int);

table student(student_schema);
table predmet(predmet_schema);
table ispitni_rok(ispitni_rok_schema);
table ispit(ispit_schema);

query q1 
`SELECT DISTINCT s.* FROM student s WHERE s.datum_rodjenja='2014-7-1'`;

query q2
`select distinct s.* from student s where s.datum_rodjenja = '2014-7-1'`;

verify q1 q2;

returns this message: Invalid generated Coq code. Please file an issue.

When I changed the condition to s.indeks=1, the two queries were correctly recognized as equivalent to one another.

I thought that maybe the date should be formatted so that the month and day have leading zeroes, so I changed '2014-7-1' to '2014-07-01', but the error was still there.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant