Cosette icon indicating copy to clipboard operation
Cosette copied to clipboard

Equivalence check for DISTINCT UNION ALL of disjoint sets yields invalid Coq code

Open erikjwaxx opened this issue 4 years ago • 0 comments

The following query:

schema base(id:int, join_id:int);
schema rel1(id:int, other_value:int);
schema rel2(id:int, other_value:int);

table aa(base);
table bb(rel1);
table cc(rel2);

query q1
`SELECT DISTINCT id AS id,
                 from_b AS from_b,
                 from_c AS from_c
   FROM (SELECT DISTINCT a.id AS id,
                1 AS from_b,
                0 AS from_c,
                b.other_value AS other_value
           FROM aa a
           JOIN bb b
             ON a.join_id = b.id
          UNION ALL
         SELECT DISTINCT a.id AS id,
                0 AS from_b,
                1 AS from_c,
                c.other_value AS other_value
           FROM aa a
           JOIN cc c
             ON a.join_id = c.id) _`;
query q2
`SELECT DISTINCT a.id AS id,
                1 AS from_b,
                0 AS from_c,
                b.other_value AS other_value
           FROM aa a
           JOIN bb b
             ON a.join_id = b.id
          UNION ALL
         SELECT DISTINCT a.id AS id,
                0 AS from_b,
                1 AS from_c,
                c.other_value AS other_value
           FROM aa a
           JOIN cc c
             ON a.join_id = c.id`;
             
verify q1 q2;

yields the error:

Invalid generated Coq code. Please file an issue. 
 
 {"size":[1],"status":"UNSAT"}
generated/nbdZQWtaTnVSi.rkt:19:25: id: unbound identifier in module
  in: id
  context...:
   /root/.racket/6.8/pkgs/rosette/rosette/base/form/module.rkt:16:0
   standard-module-name-resolver
   /Cosette-Web/backend/Cosette/rosette/server.rkt:38:10

AFAICT these two queries should be equivalent, since the two subqueries UNION ALLd are disjoint and each is DISTINCTed.

erikjwaxx avatar Sep 24 '19 15:09 erikjwaxx