Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Basic select distinct program - Coq and Rosette executions don't agree #77

Open
qaisjp opened this issue Dec 17, 2019 · 0 comments
Open
Assignees

Comments

@qaisjp
Copy link

qaisjp commented Dec 17, 2019

/* 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 a.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 a.balance = (select max(al.balance) from accs as al)
    `;

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

results in

Coq and Rosette executions doesn't agree. File an issue!
@stechu stechu self-assigned this Dec 17, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants