Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
erikjwaxx opened this issue Sep 24, 2019 · 0 comments

Comments

@erikjwaxx
Copy link

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant