From 12ab42e1a97e01c32c16d87bfcf9055c85875c70 Mon Sep 17 00:00:00 2001 From: Sven Verdoolaege Date: Wed, 5 Jan 2011 09:50:28 +0100 Subject: [PATCH] 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 --- isl_tab_pip.c | 15 ++++++++++++--- isl_test.c | 17 +++++++++++++++++ 2 files changed, 29 insertions(+), 3 deletions(-) diff --git a/isl_tab_pip.c b/isl_tab_pip.c index a2cf3a2..f9f700e 100644 --- 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 --- 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); -- 2.7.4