uwdb / Cosette

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

racket error returned #64

Closed akcheung closed 6 years ago

akcheung commented 6 years ago

This currently returns a racket error:

schema s1(x:int, ya:int);

schema s2(yb:int, yc: 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 A.x as ax from a A
 where NOT EXISTS (select * from b B
 where (B.yb < A.ya) or (B.yb>A.ya) )`;

query q2                -- define query q2 likewise
`select distinct A.x as ax from a A
where 
 ((select count(B.yb)  from b B where B.yb=A.ya) = 
(select count(B.yb) from b B))`;

verify q1 q2;           -- does q1 equal to q2?
{"size":[1],"status":"UNSAT"}
$=: expected real? arguments
arguments: '(#<void>)
context...:
/root/.racket/6.8/pkgs/rosette/rosette/base/core/real.rkt:160:10
/root/.racket/6.8/pkgs/rosette/rosette/base/form/control.rkt:31:25
/root/.racket/6.8/pkgs/rosette/rosette/base/adt/list.rkt:119:9: @for-each
/Cosette-Web/backend/Cosette/rosette/cosette.rkt:185:0: solve-queries-symbreak
Mestway commented 6 years ago

The cosette in the main branch works well on this example. We can solve this issue by simply pushing the current version to the online demo.

stechu commented 6 years ago

@akcheung @Mestway pushed