Test on demo website runs into out of time

[matthiastz]

setup: schema AlbumSchema(AlbumId: int, Title: varchar, ArtistId: int); table Album(AlbumSchema);

query q1 -- define query q1 SELECT * FROM Album a;

query q2 -- define query q1 SELECT a.AlbumId, a.Title, a.ArtistId FROM Album a;

verify q1 q2; -- does q1 equal to q2?

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

[stechu]

Thanks for the report. This looks like an edge case in prover code gen.

[matthiastz]

While working with Cosette I found more cases where the solver runs into out of time. Maybe that is of interest for you:

redundant sql clauses

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

query q1
`SELECT tr.Name, tr.MediaTypeId FROM Track tr WHERE tr.MediaTypeId > 2`;

query q2
`SELECT tr.Name, tr.MediaTypeId FROM Track tr WHERE tr.MediaTypeId > 2 and tr.MediaTypeId > 1`;

verify q1 q2;

joins

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

query q1
`select tr.TrackId, tr.Name, tr.Composer from Track tr
join (select mt.MediaTypeId,  mt.Name from MediaType mt where mt.Name = 'AAC audio file')
as tMediaType ON tr.MediaTypeId = tMediaType.MediaTypeId`;

query q2
`select tr.TrackId, tr.Name, tr.Composer  from Track tr
join MediaType mt
ON tr.MediaTypeId = mt.MediaTypeId
WHERE mt.Name = 'AAC audio file'`;

verify q1 q2;