Skip to content

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

Description

@erikjwaxx

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.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions