uwdb / Cosette

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

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

Open milos-simic opened 5 years ago

milos-simic commented 5 years ago

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.