uwdb / Cosette

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

Strings with dots result in "Invalid generated Coq file" #81

Open andrew4699 opened 4 years ago

andrew4699 commented 4 years ago

The following says "Invalid generated Coq file":

schema sch_flights(fid: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
);

table Flights(sch_flights);
table Carriers(sch_carriers);

query a
`select distinct F.flight_num as flight_num
from Flights F, Carriers C
where F.carrier_id = C.cid
and C.name='xyz.'
`;

query b
`select distinct F.flight_num as flight_num
from Flights F, Carriers C
where F.carrier_id = C.cid
and C.name='xyz.'
`;

verify a b;

but removing the "." in "xyz." makes it work correctly (the queries are equivalent).