25 karma · joined September 19, 2014
Xiaomi is like Amazon in China's smart home market, except with a much stronger mobile department that Amazon would dream to get.
ROWNUM is interesting. You can actually declare ROWNUM as an extra attribute of the table and then assert it is a key (We will add support of key constraints very soon). Then many cases will be covered.
There is some existing work. You might want to look at this one: https://pdfs.semanticscholar.org/c243/25d76c3ba91388e16085c1...
One problem is that bag semantic chase is very complicated to implement. We are actually working on a new chase algorithm on our SQL formalization right now.
I changed your query:
/* define schema s1, here s1 can contain any number of attributes, but it has to at least contain integer attributes x and y */ schema s1(x:int, ya:int, ??);
schema s2(yb:int, ??); -- define schema s2
table a(s1); -- define table a using schema s1
table b(s2); -- define table b using schema s1
query q1 -- define query q1 on tables a and b
`select distinct x.x as ax
from a x, b y
where x.ya = y.yb`;
query q2 -- define query q2 likewise
`(select x.x as ax
from a x, a y, b z
where x.x = y.x and x.ya = z.yb)
union all (select 1 as ax from a x where 1 = 0)`;
verify q1 q2; -- does q1 equal to q2?
The Rosette execution indeed returns a counterexample (since they are not equal). There is an error in Coq code generation part, we are fixing that now.