Cosette
Cosette copied to clipboard
Exactly Equal Queries Time out
The following queries are not known as equivalent, even though they are exactly the same. Maybe you could try sorting the x = y and y = x, such that they are all x = y or something. Either way, I feel like it should know that these are equivalent statements.
schema sch_flights(fid:int,
year:int,
month_id:int,
day_of_month:int,
day_of_week_id:int,
carrier_id:string,
flight_num:int,
origin_city:string,
origin_state:string,
dest_city:string,
dest_state:string,
departure_delay:int,
taxi_out:int,
arrival_delay:int,
canceled:int,
actual_time:int,
distance:int,
capacity:int,
price:int
);
schema sch_carriers
(
cid:int,
name:string
);
SCHEMA sch_months
(
mid:int,
month:string
);
SCHEMA sch_days
(
did:int,
day_of_week:string
);
table Flights(sch_flights);
table Carriers(sch_carriers);
table Weekdays(sch_days);
table Months(sch_months);
query q1 -- define query q1 on tables a and b
` select C.name as name, sum(F.departure_delay) as delay
from FLIGHTS as F, CARRIERS as C
where C.cid=F.carrier_id
group by F.carrier_id`;
query q2 -- define query q2 likewise
`select c.name as name, sum(f.departure_delay) as delay
from FLIGHTS as f, CARRIERS as c
where f.carrier_id = c.cid
group by f.carrier_id`;
verify q1 q2; -- does q1 equal to q2?
Thanks! @Njanderson
That's one of the known problems. We will fix this in the next version. Unfortunately, it will take some time.
One thing that may help is, I would like to change UNKNOWN
to LIKELY EQ
. Since it is acutally bounded model checking, 99.9 % UNKNOWN
now is actually equal.