isl_tab_basic_map_partial_lexopt: fix up symmetry detection

The symmetry detection of a41dca9 (isl_tab_basic_map_partial_lexopt:
detect and exploit simple symmetries, Mon Dec 13 16:45:44 2010 +0100)
was a bit too eager in that it would also detect symmetries on affine
expressions involving existentially quantified variables.
Those variables are only available in the input and therefore the
mechanism for exploiting symmetries does not work on them, leading
to incorrect results.

Signed-off-by: Sven Verdoolaege <skimo@kotnet.org>

diff --git a/isl_tab_pip.c b/isl_tab_pip.c
index a2cf3a2..f9f700e 100644 (file)
--- a/isl_tab_pip.c
+++ b/isl_tab_pip.c
@@ -3946,7 +3946,10 @@ static int constraint_equal(const void *entry, const void *val)
 }
 
 /* Check whether "bmap" has a pair of constraints that have
- * the same coefficients for the "output" variables, i.e.,
+ * the same coefficients for the output variables.
+ * Note that the coefficients of the existentially quantified
+ * variables need to be zero since the existentially quantified
+ * of the result are usually not the same as those of the input.
  * the isl_dim_out and isl_dim_div dimensions.
  * If so, return 1 and return the row indices of the two constraints
  * in *first and *second.
@@ -3959,6 +3962,8 @@ static int parallel_constraints(__isl_keep isl_basic_map *bmap,
        struct isl_hash_table *table = NULL;
        struct isl_hash_table_entry *entry;
        struct isl_constraint_equal_info info;
+       unsigned n_out;
+       unsigned n_div;
 
        ctx = isl_basic_map_get_ctx(bmap);
        table = isl_hash_table_alloc(ctx, bmap->n_ineq);
@@ -3968,12 +3973,16 @@ static int parallel_constraints(__isl_keep isl_basic_map *bmap,
        info.n_in = isl_basic_map_dim(bmap, isl_dim_param) +
                    isl_basic_map_dim(bmap, isl_dim_in);
        info.bmap = bmap;
-       info.n_out = isl_basic_map_dim(bmap, isl_dim_all) - info.n_in;
+       n_out = isl_basic_map_dim(bmap, isl_dim_out);
+       n_div = isl_basic_map_dim(bmap, isl_dim_div);
+       info.n_out = n_out + n_div;
        for (i = 0; i < bmap->n_ineq; ++i) {
                uint32_t hash;
 
                info.val = bmap->ineq[i] + 1 + info.n_in;
-               if (isl_seq_first_non_zero(info.val, info.n_out) < 0)
+               if (isl_seq_first_non_zero(info.val, n_out) < 0)
+                       continue;
+               if (isl_seq_first_non_zero(info.val + n_out, n_div) >= 0)
                        continue;
                hash = isl_seq_get_hash(info.val, info.n_out);
                entry = isl_hash_table_find(ctx, table, hash,

diff --git a/isl_test.c b/isl_test.c
index ab446a2..af517f1 100644 (file)
--- a/isl_test.c
+++ b/isl_test.c
@@ -1577,6 +1577,22 @@ void test_lift(isl_ctx *ctx)
        isl_basic_set_free(bset);
 }
 
+void test_subset(isl_ctx *ctx)
+{
+       const char *str;
+       isl_set *set1, *set2;
+
+       str = "{ [112, 0] }";
+       set1 = isl_set_read_from_str(ctx, str, 0);
+       str = "{ [i0, i1] : exists (e0 = [(i0 - i1)/16], e1: "
+               "16e0 <= i0 - i1 and 16e0 >= -15 + i0 - i1 and "
+               "16e1 <= i1 and 16e0 >= -i1 and 16e1 >= -i0 + i1) }";
+       set2 = isl_set_read_from_str(ctx, str, 0);
+       assert(isl_set_is_subset(set1, set2));
+       isl_set_free(set1);
+       isl_set_free(set2);
+}
+
 int main()
 {
        struct isl_ctx *ctx;
@@ -1585,6 +1601,7 @@ int main()
        assert(srcdir);
 
        ctx = isl_ctx_alloc();
+       test_subset(ctx);
        test_lift(ctx);
        test_bound(ctx);
        test_union(ctx);