search

uwdb / Cosette

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

COUNT usage leads to error: Invalid generated Coq code #82

Open matthiastz opened 4 years ago

matthiastz commented 4 years ago

setup:

schema InvoiceSchema(InvoiceId: int, CustomerId: int, InvoiceDate: date,
            BillingAddress: varchar, BillingCity: varchar,
            BillingState: varchar, BillingCountry: varchar,
            BillingPostalCode: varchar, Total: numeric); 
table Invoice(InvoiceSchema);

query q1
`SELECT i.InvoiceId, i.CustomerId, count(i.CustomerId) FROM Invoice i`;

query q2
`SELECT i.InvoiceId, i.CustomerId, count(i.CustomerId) FROM Invoice i`;

verify q1 q2;

result: Invalid generated Coq code. Please file an issue.

Rosette find an counterexample.

matthiastz commented 4 years ago

original queries I wanted to test:

schema InvoiceSchema(InvoiceId: int, CustomerId: int, InvoiceDate: date,
            BillingAddress: varchar, BillingCity: varchar,
            BillingState: varchar, BillingCountry: varchar,
            BillingPostalCode: varchar, Total: numeric); 
table Invoice(InvoiceSchema);

query q1
`SELECT i.InvoiceId, i.CustomerId, count(i.CustomerId) FROM Invoice i
 GROUP BY i.CustomerId`;

query q2
`SELECT i.InvoiceId, i.CustomerId, count(i.CustomerId) FROM Invoice i`;

verify q1 q2;