uwdb / Cosette

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

EXISTS with subquery runs into out of time #83

Open matthiastz opened 4 years ago

matthiastz commented 4 years ago

setup:

schema TrackSchema(TrackId: int, Name: varchar, AlbumId: int,
        MediaTypeId: int, GenreId: int, Composer: varchar,
        Milliseconds: int, Bytes: int, UnitPrice: numeric); 
table Track(TrackSchema);
schema GenreSchema(GenreId: int, Name: varchar); 
table Genre(GenreSchema);

query q1
`SELECT t.TrackId, t.Name, t.GenreId 
FROM Track t
WHERE EXISTS
(SELECT g.GenreId FROM Genre g WHERE t.GenreId = g.GenreId AND (g.Name = 'Reggae' OR g.Name = 'Jazz'))`;

query q2
`SELECT t.TrackId, t.Name, t.GenreId 
FROM Track t
WHERE EXISTS
(SELECT g.GenreId FROM Genre g WHERE t.GenreId = g.GenreId AND g.Name = 'Reggae' OR g.Name = 'Jazz')`;

verify q1 q2;

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

stechu commented 4 years ago

Interesting! Thanks for the issue.