From d20327e32a2be929523d101a35e1af90f9cedb3f Mon Sep 17 00:00:00 2001 From: Sven Verdoolaege Date: Fri, 18 Feb 2011 15:37:37 +0100 Subject: [PATCH] isl_basic_map_gist: prefer contraints without existentially quantified variables Signed-off-by: Sven Verdoolaege --- isl_map.c | 3 +++ isl_map_simplify.c | 8 ++++++++ isl_test.c | 26 ++++++++++++++++++++++++++ 3 files changed, 37 insertions(+) diff --git a/isl_map.c b/isl_map.c index 5173369d..06aa85c8 100644 --- a/isl_map.c +++ b/isl_map.c @@ -6735,6 +6735,9 @@ struct constraint { isl_int *c; }; +/* uset_gist depends on constraints without existentially quantified + * variables sorting first. + */ static int qsort_constraint_cmp(const void *p1, const void *p2) { const struct constraint *c1 = (const struct constraint *)p1; diff --git a/isl_map_simplify.c b/isl_map_simplify.c index 302c1234..093d1ca2 100644 --- a/isl_map_simplify.c +++ b/isl_map_simplify.c @@ -1702,6 +1702,13 @@ error: * We first compute the integer affine hull of the intersection, * compute the gist inside this affine hull and then add back * those equalities that are not implied by the context. + * + * If two constraints are mutually redundant, then uset_gist_full + * will remove the second of those constraints. We therefore first + * sort the constraints so that constraints not involving existentially + * quantified variables are given precedence over those that do. + * We have to perform this sorting before the variable compression, + * because that may effect the order of the variables. */ static __isl_give isl_basic_set *uset_gist(__isl_take isl_basic_set *bset, __isl_take isl_basic_set *context) @@ -1720,6 +1727,7 @@ static __isl_give isl_basic_set *uset_gist(__isl_take isl_basic_set *bset, isl_basic_set_free(context); return bset; } + bset = isl_basic_set_sort_constraints(bset); aff = isl_basic_set_affine_hull(isl_basic_set_copy(bset)); if (!aff) goto error; diff --git a/isl_test.c b/isl_test.c index 56ee9fbb..c6f1f26b 100644 --- a/isl_test.c +++ b/isl_test.c @@ -650,7 +650,33 @@ void test_gist_case(struct isl_ctx *ctx, const char *name) void test_gist(struct isl_ctx *ctx) { + const char *str; + isl_basic_set *bset1, *bset2; + test_gist_case(ctx, "gist1"); + + str = "[p0, p2, p3, p5, p6, p10] -> { [] : " + "exists (e0 = [(15 + p0 + 15p6 + 15p10)/16], e1 = [(p5)/8], " + "e2 = [(p6)/128], e3 = [(8p2 - p5)/128], " + "e4 = [(128p3 - p6)/4096]: 8e1 = p5 and 128e2 = p6 and " + "128e3 = 8p2 - p5 and 4096e4 = 128p3 - p6 and p2 >= 0 and " + "16e0 >= 16 + 16p6 + 15p10 and p2 <= 15 and p3 >= 0 and " + "p3 <= 31 and p6 >= 128p3 and p5 >= 8p2 and p10 >= 0 and " + "16e0 <= 15 + p0 + 15p6 + 15p10 and 16e0 >= p0 + 15p6 + 15p10 and " + "p10 <= 15 and p10 <= -1 + p0 - p6) }"; + bset1 = isl_basic_set_read_from_str(ctx, str, -1); + str = "[p0, p2, p3, p5, p6, p10] -> { [] : exists (e0 = [(p5)/8], " + "e1 = [(p6)/128], e2 = [(8p2 - p5)/128], " + "e3 = [(128p3 - p6)/4096]: 8e0 = p5 and 128e1 = p6 and " + "128e2 = 8p2 - p5 and 4096e3 = 128p3 - p6 and p5 >= -7 and " + "p2 >= 0 and 8p2 <= -1 + p0 and p2 <= 15 and p3 >= 0 and " + "p3 <= 31 and 128p3 <= -1 + p0 and p6 >= -127 and " + "p5 <= -1 + p0 and p6 <= -1 + p0 and p6 >= 128p3 and " + "p0 >= 1 and p5 >= 8p2 and p10 >= 0 and p10 <= 15 ) }"; + bset2 = isl_basic_set_read_from_str(ctx, str, -1); + bset1 = isl_basic_set_gist(bset1, bset2); + assert(bset1 && bset1->n_div == 0); + isl_basic_set_free(bset1); } void test_coalesce_set(isl_ctx *ctx, const char *str, int check_one) -- 2.11.4.GIT