uwdb / Cosette

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

Invalid Coq generated #59

Closed Njanderson closed 6 years ago

Njanderson commented 6 years ago

This generated an "Invalid Coq generated" message and told me to create an issue.

schema sch_flights(fid:int,
    year:int,
    month_id:string,
    day_of_month:int,
    day_of_week_id:int,
    carrier_id:int,
    flight_num:int,
    origin_city:string,
    origin_state:int,
    dest_city:string,
    dest_state:int,
    departure_delay:int,
    taxi_out:int,
    arrival_delay:int,
    canceled:int,
    actual_time:int,
    distance:int
);

schema sch_carriers
(
    cid:int,
    name:int
);

SCHEMA sch_months
(
    mid:int,
    month:int
);

SCHEMA sch_days
(
    did:int,
    day_of_week:int
);

table Flights(sch_flights);
table Carriers(sch_carriers);
table Weekdays(sch_days);
table Months(sch_months);

query q1 `SELECT C.name AS name,
       F1.flight_num AS f1_flight_num,
       F1.origin_city AS f1_origin_city,
       F1.dest_city AS f1_dest_city,
       F1.actual_time AS f1_actual_time,
       F2.flight_num AS f2_flight_num,
       F2.origin_city AS f2_origin_city,
       F2.dest_city AS f2_dest_city,
       F2.actual_time AS f2_actual_time,
       (F1.actual_time + F2.actual_time) AS actual_time
  FROM FLIGHTS F1, FLIGHTS F2
  JOIN MONTHS M
    ON F1.month_id = M.mid AND F2.month_id = M.mid
  JOIN CARRIERS C
    ON F1.carrier_id = C.cid AND F2.carrier_id = C.cid
 WHERE M.month = 'July'
   AND F1.day_of_month = 15
   AND F2.day_of_month = 15
   AND F1.year = 2015
   AND F2.year = 2015
   AND F1.origin_city = 'Seattle WA'
   AND F2.dest_city = 'Boston MA'
   AND F1.dest_city = F2.origin_city
   AND (F1.actual_time + F2.actual_time) < 7 * 60
   AND F1.carrier_id = F2.carrier_id`;

query q2                -- define query q2 likewise
`SELECT C.name AS name,
       F1.flight_num AS f1_flight_num,
       F1.origin_city AS f1_origin_city,
       F1.dest_city AS f1_dest_city,
       F1.actual_time AS f1_actual_time,
       F2.flight_num AS f2_flight_num,
       F2.origin_city AS f2_origin_city,
       F2.dest_city AS f2_dest_city,
       F2.actual_time AS f2_actual_time,
       (F1.actual_time + F2.actual_time) AS actual_time
  FROM FLIGHTS F1, FLIGHTS F2
  JOIN MONTHS M
    ON F1.month_id = M.mid AND F2.month_id = M.mid
  JOIN CARRIERS C
    ON F1.carrier_id = C.cid AND F2.carrier_id = C.cid
 WHERE M.month = 'July'
   AND F1.day_of_month = 15
   AND F2.day_of_month = 15
   AND F1.year = 2015
   AND F2.year = 2015
   AND F1.origin_city = 'Seattle WA'
   AND F2.dest_city = 'Boston MA'
   AND F1.dest_city = F2.origin_city
   AND (F1.actual_time + F2.actual_time) < 7 * 60
   AND F1.carrier_id = F2.carrier_id`;

verify q1 q2;           -- does q1 equal to q2?
stechu commented 6 years ago

@Njanderson it would be great if you can "minimize" the problem a bit, too :)

stechu commented 6 years ago

fixed.