uwdb / Cosette

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

Feature request: Avoid useless repetition in counter examples #72

Open beta-ziliani opened 5 years ago

beta-ziliani commented 5 years ago

The following example (slightly modified from the one in the page) generates tables with lots of repetition, which could be easily avoided by truncation.

schema employee(eid:int, age:int, ??);
schema payroll(eid:int, salary:int, ??);        

table uw_emp(employee);
table uw_payroll(payroll);

query q1                
`select distinct e.eid as eid 
 from uw_emp e, uw_payroll p
 where e.eid = p.eid`;

query q2                
`select distinct e1.eid as eid 
 from uw_emp e1, uw_emp e2, uw_payroll p 
 where e1.eid = e2.eid and e1.eid = e2.eid`;

verify q1 q2;

Result:

Table uw_payroll

eid salary ??
1 0 0
1 0 0
1 0 0
1 0 0
1 0 0
1 0 0
1 0 0
1 0 0
1 0 0
1 0 0
1 0 0
1 0 0

Table uw_emp

eid age ??
0 0 0
0 0 0
0 0 0
0 0 0
0 0 0
0 0 0
0 0 0
0 0 0
0 0 0
0 0 0
0 0 0
0 0 0
0 0 0
0 0 0
0 0 0