From ecafffade5c2c60f5bd13c6699b675245c2c3797 Mon Sep 17 00:00:00 2001 From: Sven Verdoolaege Date: Fri, 21 Nov 2014 12:23:57 +0100 Subject: [PATCH] isl_map_gist: try and exploit implicit constraints in multi-disjunct contexts If the context is a multi-disjunct set, then we first compute a single-disjunct approximation and compute the gist with respect to this approximation. The approximation may however drop some constraints that are only implicitly available in the disjuncts of the context. Check which of the constraints in the input map are also valid for the context so that they can be used to simplify away those constraints of the input. For example, the constraint a <= 2147 + n is implied by the set { [m, n, a, b] : (n >= 1 and a >= 0 and b <= 2148 - n - a and b >= 0) or (m >= 1 and n >= 1 and a <= 2148 - m and b <= 2148 - n and b >= 0 and b >= 2149 - n - a) } but it is not implied by the simple hull of this set, i.e., { [m, n, a, b] : n >= 1 and a >= 0 and b <= 4295 - n - a and b >= 0 and b <= 2148 - n } When also considering the constraint a <= 2147 + n while building the simple hull, we obtain { [m, n, a, b] : b <= 2148 - n and b >= 0 and a >= 0 and a <= 2147 + n and n >= 1 } instead, which can be used to simplify away the original "a <= 2147 + n" constraint. Signed-off-by: Sven Verdoolaege --- isl_map_simplify.c | 26 +++++++++++++++++++++++++- isl_test.c | 6 ++++++ 2 files changed, 31 insertions(+), 1 deletion(-) diff --git a/isl_map_simplify.c b/isl_map_simplify.c index 09619a6a..d00a6edd 100644 --- a/isl_map_simplify.c +++ b/isl_map_simplify.c @@ -2352,12 +2352,21 @@ error: * return the corresponding universe. * * If none of these cases apply, we have to work a bit harder. + * During this computation, we make use of a single disjunct context, + * so if the original context consists of more than one disjunct + * then we need to approximate the context by a single disjunct set. + * Simply taking the simple hull may drop constraints that are + * only implicitly available in each disjunct. We therefore also + * look for constraints among those defining "map" that are valid + * for the context. These can then be used to simplify away + * the corresponding constraints in "map". */ static __isl_give isl_map *map_gist(__isl_take isl_map *map, __isl_take isl_map *context) { int equal; int is_universe; + isl_basic_map *hull; is_universe = isl_map_plain_is_universe(map); if (is_universe >= 0 && !is_universe) @@ -2380,7 +2389,22 @@ static __isl_give isl_map *map_gist(__isl_take isl_map *map, } context = isl_map_compute_divs(context); - return isl_map_gist_basic_map(map, isl_map_simple_hull(context)); + if (!context) + goto error; + if (isl_map_n_basic_map(context) == 1) { + hull = isl_map_simple_hull(context); + } else { + isl_ctx *ctx; + isl_map_list *list; + + ctx = isl_map_get_ctx(map); + list = isl_map_list_alloc(ctx, 2); + list = isl_map_list_add(list, isl_map_copy(context)); + list = isl_map_list_add(list, isl_map_copy(map)); + hull = isl_map_unshifted_simple_hull_from_map_list(context, + list); + } + return isl_map_gist_basic_map(map, hull); error: isl_map_free(map); isl_map_free(context); diff --git a/isl_test.c b/isl_test.c index 3f4e2c70..a730243c 100644 --- a/isl_test.c +++ b/isl_test.c @@ -1167,6 +1167,12 @@ struct { { "{ : 1 = 0 }", "{ : 1 = 0 }", "{ : }" }, { "[M] -> { [x] : exists (e0 = floor((-2 + x)/3): 3e0 = -2 + x) }", "[M] -> { [3M] }" , "[M] -> { [x] : 1 = 0 }" }, + { "{ [m, n, a, b] : a <= 2147 + n }", + "{ [m, n, a, b] : (m >= 1 and n >= 1 and a <= 2148 - m and " + "b <= 2148 - n and b >= 0 and b >= 2149 - n - a) or " + "(n >= 1 and a >= 0 and b <= 2148 - n - a and " + "b >= 0) }", + "{ [m, n, ku, kl] }" }, }; static int test_gist(struct isl_ctx *ctx) -- 2.11.4.GIT