uwdb / Cosette

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

Invalid Cosette program yields invalid Coq code #76

Open qaisjp opened 4 years ago

qaisjp commented 4 years ago

Input example:

/* define schema employee, 
   here employee can contain any number of attributes, 
   but it has to at least contain integer attributes 
   eid and age */
schema customer(id:int, name:text, city:text);
schema account(num:int, branch:text, custid:int, balance:int);        

-- define table uw_emp using schema s1
table accs(account);
-- define table uw_sal using schema s1
table custs(customer);

-- define query q1 over uw_emp and uw_payroll
query q1                
`select c.id, c.name
    from accs a, custs c
    where c.id=a.custid
    and balance = (select max(al.balance) from accs as al)
    group by c.id, c.name`;

-- define query q2 likewise
query q2                
`select distinct c.id, c.name
    from accs a, custs c
    where c.id=a.custid
    and balance = (select max(al.balance) from accs as al)
    `;

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

Which causes the following error output:

Invalid generated Coq code. Please file an issue.

{"size":[1],"status":"UNSAT"}
generated/jxOJRPUUIWDyf.rkt:19:47: balance: unbound identifier in module
in: balance
context...:
/root/.racket/6.8/pkgs/rosette/rosette/base/form/module.rkt:16:0
standard-module-name-resolver
/Cosette-Web/backend/Cosette/rosette/server.rkt:38:10

Problematic line: and balance = (select max(al.balance) from accs as al)

It should be: and a.balance = [..]