From c0ea488b845dbfc17fda82a88bfa119cbc9fc726 Mon Sep 17 00:00:00 2001 From: Sven Verdoolaege Date: Sat, 14 Jul 2012 13:50:29 +0200 Subject: [PATCH] add isl_basic_set_preimage_multi_aff Signed-off-by: Sven Verdoolaege --- doc/user.pod | 13 +++ include/isl/set.h | 2 + isl_aff.c | 71 ++++++++++++++++ isl_aff_private.h | 3 + isl_map.c | 241 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ isl_test.c | 56 +++++++++++++ 6 files changed, 386 insertions(+) diff --git a/doc/user.pod b/doc/user.pod index 1328a18..d4d4ca0 100644 --- a/doc/user.pod +++ b/doc/user.pod @@ -2773,6 +2773,19 @@ a parametric set as well. __isl_take isl_union_map *umap1, __isl_take isl_union_map *umap2); +=item * Preimage + + __isl_give isl_basic_set * + isl_basic_set_preimage_multi_aff( + __isl_take isl_basic_set *bset, + __isl_take isl_multi_aff *ma); + +This function computes the preimage of the given set under +the given function. In other words, the expression is plugged +into the set description. +Objects of type C are described in +L. + =item * Cartesian Product __isl_give isl_set *isl_set_product( diff --git a/include/isl/set.h b/include/isl/set.h index 3e41d0e..60a99fe 100644 --- a/include/isl/set.h +++ b/include/isl/set.h @@ -120,6 +120,8 @@ __isl_export __isl_give isl_basic_set *isl_basic_set_apply( __isl_take isl_basic_set *bset, __isl_take isl_basic_map *bmap); +__isl_give isl_basic_set *isl_basic_set_preimage_multi_aff( + __isl_take isl_basic_set *bset, __isl_take isl_multi_aff *ma); __isl_export __isl_give isl_basic_set *isl_basic_set_affine_hull( __isl_take isl_basic_set *bset); diff --git a/isl_aff.c b/isl_aff.c index 499298c..9174069 100644 --- a/isl_aff.c +++ b/isl_aff.c @@ -3417,6 +3417,77 @@ __isl_give isl_pw_multi_aff *isl_pw_multi_aff_substitute( return res; } +/* Compute the preimage of the affine expression "src" under "ma" + * and put the result in "dst". If "has_denom" is set (to one), + * then "src" and "dst" have an extra initial denominator. + * "n_div_ma" is the number of existentials in "ma" + * "n_div_bset" is the number of existentials in "src" + * The resulting "dst" (which is assumed to have been allocated by + * the caller) contains coefficients for both sets of existentials, + * first those in "ma" and then those in "src". + * f, c1, c2 and g are temporary objects that have been initialized + * by the caller. + * + * Let src represent the expression + * + * (a(p) + b x + c(divs))/d + * + * and let ma represent the expressions + * + * x_i = (r_i(p) + s_i(y) + t_i(divs'))/m_i + * + * We start out with the following expression for dst: + * + * (a(p) + 0 y + 0 divs' + f \sum_i b_i x_i + c(divs))/d + * + * with the multiplication factor f initially equal to 1. + * For each x_i that we substitute, we multiply the numerator + * (and denominator) of dst by c_1 = m_i and add the numerator + * of the x_i expression multiplied by c_2 = f b_i, + * after removing the common factors of c_1 and c_2. + * The multiplication factor f also needs to be multiplied by c_1 + * for the next x_j, j > i. + */ +void isl_seq_preimage(isl_int *dst, isl_int *src, + __isl_keep isl_multi_aff *ma, int n_div_ma, int n_div_bset, + isl_int f, isl_int c1, isl_int c2, isl_int g, int has_denom) +{ + int i; + int n_param, n_in, n_out; + int o_div_bset; + + n_param = isl_multi_aff_dim(ma, isl_dim_param); + n_in = isl_multi_aff_dim(ma, isl_dim_in); + n_out = isl_multi_aff_dim(ma, isl_dim_out); + + o_div_bset = has_denom + 1 + n_param + n_in + n_div_ma; + + isl_seq_cpy(dst, src, has_denom + 1 + n_param); + isl_seq_clr(dst + has_denom + 1 + n_param, n_in + n_div_ma); + isl_seq_cpy(dst + o_div_bset, + src + has_denom + 1 + n_param + n_out, n_div_bset); + + isl_int_set_si(f, 1); + + for (i = 0; i < n_out; ++i) { + if (isl_int_is_zero(src[has_denom + 1 + n_param + i])) + continue; + isl_int_set(c1, ma->p[i]->v->el[0]); + isl_int_mul(c2, f, src[has_denom + 1 + n_param + i]); + isl_int_gcd(g, c1, c2); + isl_int_divexact(c1, c1, g); + isl_int_divexact(c2, c2, g); + + isl_int_mul(f, f, c1); + isl_seq_combine(dst + has_denom, c1, dst + has_denom, + c2, ma->p[i]->v->el + 1, ma->p[i]->v->size - 1); + isl_seq_scale(dst + o_div_bset, + dst + o_div_bset, c1, n_div_bset); + if (has_denom) + isl_int_mul(dst[0], dst[0], c1); + } +} + /* Extend the local space of "dst" to include the divs * in the local space of "src". */ diff --git a/isl_aff_private.h b/isl_aff_private.h index 9b20ea5..dc031c4 100644 --- a/isl_aff_private.h +++ b/isl_aff_private.h @@ -101,6 +101,9 @@ __isl_give isl_pw_multi_aff *isl_pw_multi_aff_project_out( void isl_seq_substitute(isl_int *p, int pos, isl_int *subs, int p_len, int subs_len, isl_int v); +void isl_seq_preimage(isl_int *dst, isl_int *src, + __isl_keep isl_multi_aff *ma, int n_div_ma, int n_div_bset, + isl_int f, isl_int c1, isl_int c2, isl_int g, int has_denom); __isl_give isl_pw_multi_aff *isl_pw_multi_aff_substitute( __isl_take isl_pw_multi_aff *pma, enum isl_dim_type type, unsigned pos, diff --git a/isl_map.c b/isl_map.c index 0704f5d..a0ab7e3 100644 --- a/isl_map.c +++ b/isl_map.c @@ -10899,3 +10899,244 @@ error: isl_set_free(set); return NULL; } + +/* Check if the range of "ma" is compatible with "space". + * Return -1 if anything is wrong. + */ +static int check_space_compatible_range_multi_aff( + __isl_keep isl_space *space, __isl_keep isl_multi_aff *ma) +{ + int m; + isl_space *ma_space; + + ma_space = isl_multi_aff_get_space(ma); + m = isl_space_is_range_internal(space, ma_space); + isl_space_free(ma_space); + if (m >= 0 && !m) + isl_die(isl_space_get_ctx(space), isl_error_invalid, + "spaces don't match", return -1); + return m; +} + +/* Check if the range of "ma" is compatible with "bset". + * Return -1 if anything is wrong. + */ +static int check_basic_set_compatible_range_multi_aff( + __isl_keep isl_basic_set *bset, __isl_keep isl_multi_aff *ma) +{ + return check_space_compatible_range_multi_aff(bset->dim, ma); +} + +/* Copy the divs from "ma" to "bset", adding zeros for the coefficients + * of the other divs in "bset". + */ +static int set_ma_divs(__isl_keep isl_basic_set *bset, + __isl_keep isl_multi_aff *ma, int n_div) +{ + int i; + isl_local_space *ls; + + if (n_div == 0) + return 0; + + ls = isl_aff_get_domain_local_space(ma->p[0]); + if (!ls) + return -1; + + for (i = 0; i < n_div; ++i) { + isl_seq_cpy(bset->div[i], ls->div->row[i], ls->div->n_col); + isl_seq_clr(bset->div[i] + ls->div->n_col, bset->n_div - n_div); + if (isl_basic_set_add_div_constraints(bset, i) < 0) + goto error; + } + + isl_local_space_free(ls); + return 0; +error: + isl_local_space_free(ls); + return -1; +} + +/* How many stride constraints does "ma" enforce? + * That is, how many of the affine expressions have a denominator + * different from one? + */ +static int multi_aff_strides(__isl_keep isl_multi_aff *ma) +{ + int i; + int strides = 0; + + for (i = 0; i < ma->n; ++i) + if (!isl_int_is_one(ma->p[i]->v->el[0])) + strides++; + + return strides; +} + +/* For each affine expression in ma of the form + * + * x_i = (f_i y + h_i)/m_i + * + * with m_i different from one, add a constraint to "bset" + * of the form + * + * f_i y + h_i = m_i alpha_i + * + * with alpha_i an additional existentially quantified variable. + */ +static __isl_give isl_basic_set *add_ma_strides( + __isl_take isl_basic_set *bset, __isl_keep isl_multi_aff *ma) +{ + int i, k; + int div; + int total; + + total = isl_basic_set_total_dim(bset); + for (i = 0; i < ma->n; ++i) { + int len; + + if (isl_int_is_one(ma->p[i]->v->el[0])) + continue; + div = isl_basic_set_alloc_div(bset); + k = isl_basic_set_alloc_equality(bset); + if (div < 0 || k < 0) + goto error; + isl_int_set_si(bset->div[div][0], 0); + len = ma->p[i]->v->size; + isl_seq_cpy(bset->eq[k], ma->p[i]->v->el + 1, len - 1); + isl_seq_clr(bset->eq[k] + len - 1, 1 + total - (len - 1)); + isl_int_neg(bset->eq[k][1 + total], ma->p[i]->v->el[0]); + total++; + } + + return bset; +error: + isl_basic_set_free(bset); + return NULL; +} + +/* Compute the preimage of "bset" under the function represented by "ma". + * In other words, plug in "ma" in "bset". The result is a basic set + * that lives in the domain space of "ma". + * + * If bset is represented by + * + * A(p) + B x + C(divs) >= 0 + * + * and ma is represented by + * + * x = D(p) + F(y) + G(divs') + * + * then the result is + * + * A(p) + B D(p) + B F(y) + B G(divs') + C(divs) >= 0 + * + * The divs in the input set are similarly adjusted. + * In particular + * + * floor((a_i(p) + b_i x + c_i(divs))/n_i) + * + * becomes + * + * floor((a_i(p) + b_i D(p) + b_i F(y) + B_i G(divs') + c_i(divs))/n_i) + * + * If bset is not a rational set and if F(y) involves any denominators + * + * x_i = (f_i y + h_i)/m_i + * + * the additional constraints are added to ensure that we only + * map back integer points. That is we enforce + * + * f_i y + h_i = m_i alpha_i + * + * with alpha_i an additional existentially quantified variable. + * + * We first copy over the divs from "ma". + * Then we add the modified constraints and divs from "bset". + * Finally, we add the stride constraints, if needed. + */ +__isl_give isl_basic_set *isl_basic_set_preimage_multi_aff( + __isl_take isl_basic_set *bset, __isl_take isl_multi_aff *ma) +{ + int i, k; + isl_space *space; + isl_basic_set *res = NULL; + int n_div_bset, n_div_ma; + isl_int f, c1, c2, g; + int rational, strides; + + isl_int_init(f); + isl_int_init(c1); + isl_int_init(c2); + isl_int_init(g); + + ma = isl_multi_aff_align_divs(ma); + if (!bset || !ma) + goto error; + if (check_basic_set_compatible_range_multi_aff(bset, ma) < 0) + goto error; + + n_div_bset = isl_basic_set_dim(bset, isl_dim_div); + n_div_ma = ma->n ? isl_aff_dim(ma->p[0], isl_dim_div) : 0; + + space = isl_space_domain(isl_multi_aff_get_space(ma)); + rational = isl_basic_set_is_rational(bset); + strides = rational ? 0 : multi_aff_strides(ma); + res = isl_basic_set_alloc_space(space, n_div_ma + n_div_bset + strides, + bset->n_eq + strides, bset->n_ineq + 2 * n_div_ma); + if (rational) + res = isl_basic_set_set_rational(res); + + for (i = 0; i < n_div_ma + n_div_bset; ++i) + if (isl_basic_set_alloc_div(res) < 0) + goto error; + + if (set_ma_divs(res, ma, n_div_ma) < 0) + goto error; + + for (i = 0; i < bset->n_eq; ++i) { + k = isl_basic_set_alloc_equality(res); + if (k < 0) + goto error; + isl_seq_preimage(res->eq[k], bset->eq[i], ma, n_div_ma, + n_div_bset, f, c1, c2, g, 0); + } + + for (i = 0; i < bset->n_ineq; ++i) { + k = isl_basic_set_alloc_inequality(res); + if (k < 0) + goto error; + isl_seq_preimage(res->ineq[k], bset->ineq[i], ma, n_div_ma, + n_div_bset, f, c1, c2, g, 0); + } + + for (i = 0; i < bset->n_div; ++i) { + if (isl_int_is_zero(bset->div[i][0])) { + isl_int_set_si(res->div[n_div_ma + i][0], 0); + continue; + } + isl_seq_preimage(res->div[n_div_ma + i], bset->div[i], + ma, n_div_ma, n_div_bset, f, c1, c2, g, 1); + } + + if (strides) + res = add_ma_strides(res, ma); + + isl_int_clear(f); + isl_int_clear(c1); + isl_int_clear(c2); + isl_int_clear(g); + isl_basic_set_free(bset); + isl_multi_aff_free(ma); + res = isl_basic_set_simplify(res); + return isl_basic_set_finalize(res); +error: + isl_int_clear(f); + isl_int_clear(c1); + isl_int_clear(c2); + isl_int_clear(g); + isl_basic_set_free(bset); + isl_multi_aff_free(ma); + isl_basic_set_free(res); + return NULL; +} diff --git a/isl_test.c b/isl_test.c index a831b7d..60f70a5 100644 --- a/isl_test.c +++ b/isl_test.c @@ -3184,11 +3184,67 @@ static int test_list(isl_ctx *ctx) } struct { + const char *set; + const char *ma; + const char *res; +} preimage_tests[] = { + { "{ B[i,j] : 0 <= i < 10 and 0 <= j < 100 }", + "{ A[j,i] -> B[i,j] }", + "{ A[j,i] : 0 <= i < 10 and 0 <= j < 100 }" }, + { "{ rat: B[i,j] : 0 <= i, j and 3 i + 5 j <= 100 }", + "{ A[a,b] -> B[a/2,b/6] }", + "{ rat: A[a,b] : 0 <= a, b and 9 a + 5 b <= 600 }" }, + { "{ B[i,j] : 0 <= i, j and 3 i + 5 j <= 100 }", + "{ A[a,b] -> B[a/2,b/6] }", + "{ A[a,b] : 0 <= a, b and 9 a + 5 b <= 600 and " + "exists i,j : a = 2 i and b = 6 j }" }, + { "[n] -> { S[i] : 0 <= i <= 100 }", "[n] -> { S[n] }", + "[n] -> { : 0 <= n <= 100 }" }, + { "{ B[i] : 0 <= i < 100 and exists a : i = 4 a }", + "{ A[a] -> B[2a] }", + "{ A[a] : 0 <= a < 50 and exists b : a = 2 b }" }, + { "{ B[i] : 0 <= i < 100 and exists a : i = 4 a }", + "{ A[a] -> B[([a/2])] }", + "{ A[a] : 0 <= a < 200 and exists b : [a/2] = 4 b }" }, + { "{ B[i,j,k] : 0 <= i,j,k <= 100 }", + "{ A[a] -> B[a,a,a/3] }", + "{ A[a] : 0 <= a <= 100 and exists b : a = 3 b }" }, + { "{ B[i,j] : j = [(i)/2] } ", "{ A[i,j] -> B[i/3,j] }", + "{ A[i,j] : j = [(i)/6] and exists a : i = 3 a }" }, +}; + +int test_preimage(isl_ctx *ctx) +{ + int i; + isl_basic_set *bset1, *bset2; + isl_multi_aff *ma; + int equal; + + for (i = 0; i < ARRAY_SIZE(preimage_tests); ++i) { + bset1 = isl_basic_set_read_from_str(ctx, preimage_tests[i].set); + ma = isl_multi_aff_read_from_str(ctx, preimage_tests[i].ma); + bset2 = isl_basic_set_read_from_str(ctx, preimage_tests[i].res); + bset1 = isl_basic_set_preimage_multi_aff(bset1, ma); + equal = isl_basic_set_is_equal(bset1, bset2); + isl_basic_set_free(bset1); + isl_basic_set_free(bset2); + if (equal < 0) + return -1; + if (!equal) + isl_die(ctx, isl_error_unknown, "bad preimage", + return -1); + } + + return 0; +} + +struct { const char *name; int (*fn)(isl_ctx *ctx); } tests [] = { { "list", &test_list }, { "align parameters", &test_align_parameters }, + { "preimage", &test_preimage }, { "eliminate", &test_eliminate }, { "reisdue class", &test_residue_class }, { "div", &test_div }, -- 2.7.4