From e1ad18235dc0cfc6c1ac81b80b3ac7231dde1d76 Mon Sep 17 00:00:00 2001 From: Sven Verdoolaege Date: Mon, 30 Dec 2013 17:03:11 +0100 Subject: [PATCH] isl_basic_map_simplify: fix elimination of unit coefficient known divs If a known div appears with a unit coefficient in a constraint, then it is eliminated from that constraint in order to simplify the constraint. However, one if the div constraints may have been eliminated as being redundant with respect to the modified constraint and the elimination of the div from the constraint may therefore result in a loss of information about the div from the constraints. To make sure this problem does not occur, we (re)introduce the div constraint that could potentially have been eliminated with respect to the modified constraint. Signed-off-by: Sven Verdoolaege --- isl_map.c | 88 +++++++++++++++++++++++++++++++++++++++++++++--------- isl_map_private.h | 2 ++ isl_map_simplify.c | 10 +++++++ isl_test.c | 12 ++++++++ 4 files changed, 98 insertions(+), 14 deletions(-) diff --git a/isl_map.c b/isl_map.c index af999167..4b3b0bf6 100644 --- a/isl_map.c +++ b/isl_map.c @@ -4299,19 +4299,14 @@ error: return NULL; } -/* For a div d = floor(f/m), add the constraints +/* For a div d = floor(f/m), add the constraint * * f - m d >= 0 - * -(f-(n-1)) + m d >= 0 - * - * Note that the second constraint is the negation of - * - * f - m d >= n */ -int isl_basic_map_add_div_constraints_var(__isl_keep isl_basic_map *bmap, +static int add_upper_div_constraint(__isl_keep isl_basic_map *bmap, unsigned pos, isl_int *div) { - int i, j; + int i; unsigned total = isl_basic_map_total_dim(bmap); i = isl_basic_map_alloc_inequality(bmap); @@ -4320,13 +4315,47 @@ int isl_basic_map_add_div_constraints_var(__isl_keep isl_basic_map *bmap, isl_seq_cpy(bmap->ineq[i], div + 1, 1 + total); isl_int_neg(bmap->ineq[i][1 + pos], div[0]); - j = isl_basic_map_alloc_inequality(bmap); - if (j < 0) + return 0; +} + +/* For a div d = floor(f/m), add the constraint + * + * -(f-(n-1)) + m d >= 0 + */ +static int add_lower_div_constraint(__isl_keep isl_basic_map *bmap, + unsigned pos, isl_int *div) +{ + int i; + unsigned total = isl_basic_map_total_dim(bmap); + + i = isl_basic_map_alloc_inequality(bmap); + if (i < 0) + return -1; + isl_seq_neg(bmap->ineq[i], div + 1, 1 + total); + isl_int_set(bmap->ineq[i][1 + pos], div[0]); + isl_int_add(bmap->ineq[i][0], bmap->ineq[i][0], bmap->ineq[i][1 + pos]); + isl_int_sub_ui(bmap->ineq[i][0], bmap->ineq[i][0], 1); + + return 0; +} + +/* For a div d = floor(f/m), add the constraints + * + * f - m d >= 0 + * -(f-(n-1)) + m d >= 0 + * + * Note that the second constraint is the negation of + * + * f - m d >= n + */ +int isl_basic_map_add_div_constraints_var(__isl_keep isl_basic_map *bmap, + unsigned pos, isl_int *div) +{ + if (add_upper_div_constraint(bmap, pos, div) < 0) return -1; - isl_seq_neg(bmap->ineq[j], bmap->ineq[i], 1 + total); - isl_int_add(bmap->ineq[j][0], bmap->ineq[j][0], bmap->ineq[j][1 + pos]); - isl_int_sub_ui(bmap->ineq[j][0], bmap->ineq[j][0], 1); - return j; + if (add_lower_div_constraint(bmap, pos, div) < 0) + return -1; + return 0; } int isl_basic_set_add_div_constraints_var(__isl_keep isl_basic_set *bset, @@ -4345,6 +4374,37 @@ int isl_basic_map_add_div_constraints(struct isl_basic_map *bmap, unsigned div) bmap->div[div]); } +/* Add the div constraint of sign "sign" for div "div" of "bmap". + * + * In particular, if this div is of the form d = floor(f/m), + * then add the constraint + * + * f - m d >= 0 + * + * if sign < 0 or the constraint + * + * -(f-(n-1)) + m d >= 0 + * + * if sign > 0. + */ +int isl_basic_map_add_div_constraint(__isl_keep isl_basic_map *bmap, + unsigned div, int sign) +{ + unsigned total; + unsigned div_pos; + + if (!bmap) + return -1; + + total = isl_basic_map_total_dim(bmap); + div_pos = total - bmap->n_div + div; + + if (sign < 0) + return add_upper_div_constraint(bmap, div_pos, bmap->div[div]); + else + return add_lower_div_constraint(bmap, div_pos, bmap->div[div]); +} + int isl_basic_set_add_div_constraints(struct isl_basic_set *bset, unsigned div) { return isl_basic_map_add_div_constraints(bset, div); diff --git a/isl_map_private.h b/isl_map_private.h index 66862d78..db5f96b8 100644 --- a/isl_map_private.h +++ b/isl_map_private.h @@ -272,6 +272,8 @@ __isl_give isl_set *isl_set_eliminate(__isl_take isl_set *set, int isl_basic_set_constraint_is_redundant(struct isl_basic_set **bset, isl_int *c, isl_int *opt_n, isl_int *opt_d); +int isl_basic_map_add_div_constraint(__isl_keep isl_basic_map *bmap, + unsigned div, int sign); int isl_basic_map_add_div_constraints(struct isl_basic_map *bmap, unsigned div); struct isl_basic_map *isl_basic_map_drop_redundant_divs( struct isl_basic_map *bmap); diff --git a/isl_map_simplify.c b/isl_map_simplify.c index af24943f..a575db0d 100644 --- a/isl_map_simplify.c +++ b/isl_map_simplify.c @@ -1207,6 +1207,12 @@ static struct isl_basic_map *remove_duplicate_constraints( * -floor(e/m) = ceil(-e/m) = floor((-e + m - 1)/m) * * + * Note that one of the div constraints may have been eliminated + * due to being redundant with respect to the constraint that is + * being modified by this function. The modified constraint may + * no longer imply this div constraint, so we add it back to make + * sure we do not lose any information. + * * We skip integral divs, i.e., those with denominator 1, as we would * risk eliminating the div from the div constraints. We do not need * to handle those divs here anyway since the div constraints will turn @@ -1258,6 +1264,10 @@ static __isl_give isl_basic_map *eliminate_unit_divs( isl_int_sub_ui(bmap->ineq[j][0], bmap->ineq[j][0], 1); } + + bmap = isl_basic_map_extend_constraints(bmap, 0, 1); + if (isl_basic_map_add_div_constraint(bmap, i, s) < 0) + return isl_basic_map_free(bmap); } } diff --git a/isl_test.c b/isl_test.c index 94e105e2..738af55c 100644 --- a/isl_test.c +++ b/isl_test.c @@ -2300,6 +2300,18 @@ struct { { "{ rat: [i] : 0 <= i <= 10 }", "{ [i] : 0 <= i <= 10 }", 0 }, { "{ rat: [0] }", "{ [i] : 0 <= i <= 10 }", 1 }, { "{ rat: [(1)/2] }", "{ [i] : 0 <= i <= 10 }", 0 }, + { "{ [t, i] : (exists (e0 = [(2 + t)/4]: 4e0 <= 2 + t and " + "4e0 >= -1 + t and i >= 57 and i <= 62 and " + "4e0 <= 62 + t - i and 4e0 >= -61 + t + i and " + "t >= 0 and t <= 511 and 4e0 <= -57 + t + i and " + "4e0 >= 58 + t - i and i >= 58 + t and i >= 62 - t)) }", + "{ [i0, i1] : (exists (e0 = [(4 + i0)/4]: 4e0 <= 62 + i0 - i1 and " + "4e0 >= 1 + i0 and i0 >= 0 and i0 <= 511 and " + "4e0 <= -57 + i0 + i1)) or " + "(exists (e0 = [(2 + i0)/4]: 4e0 <= i0 and " + "4e0 >= 58 + i0 - i1 and i0 >= 2 and i0 <= 511 and " + "4e0 >= -61 + i0 + i1)) or " + "(i1 <= 66 - i0 and i0 >= 2 and i1 >= 59 + i0) }", 1 }, }; static int test_subset(isl_ctx *ctx) -- 2.11.4.GIT