From 661c3743a58bd69d5c7e5d62a716c0f2cd857e65 Mon Sep 17 00:00:00 2001 From: Sven Verdoolaege Date: Fri, 5 Nov 2010 16:44:54 +0100 Subject: [PATCH] isl_pw_qpolynomial_gist: also try to eliminate integer divisions Signed-off-by: Sven Verdoolaege --- isl_fold.c | 27 ++++++++++++++++ isl_polynomial.c | 82 +++++++++++++++++++++++++++++++++--------------- isl_polynomial_private.h | 4 +++ isl_pw_templ.c | 6 ++-- isl_test.c | 14 +++++++++ 5 files changed, 103 insertions(+), 30 deletions(-) diff --git a/isl_fold.c b/isl_fold.c index 2f37054..38fbf99 100644 --- a/isl_fold.c +++ b/isl_fold.c @@ -530,6 +530,33 @@ error: return NULL; } +__isl_give isl_qpolynomial_fold *isl_qpolynomial_fold_gist( + __isl_take isl_qpolynomial_fold *fold, __isl_take isl_set *context) +{ + int i; + + if (!fold || !context) + goto error; + + fold = isl_qpolynomial_fold_cow(fold); + if (!fold) + return NULL; + + for (i = 0; i < fold->n; ++i) { + fold->qp[i] = isl_qpolynomial_gist(fold->qp[i], + isl_set_copy(context)); + if (!fold->qp[i]) + goto error; + } + + isl_set_free(context); + return fold; +error: + isl_set_free(context); + isl_qpolynomial_fold_free(fold); + return NULL; +} + #define HAS_TYPE #undef PW diff --git a/isl_polynomial.c b/isl_polynomial.c index 43d79e9..a9de881 100644 --- a/isl_polynomial.c +++ b/isl_polynomial.c @@ -2111,6 +2111,62 @@ error: return NULL; } +static __isl_give isl_basic_set *add_div_constraints( + __isl_take isl_basic_set *bset, __isl_take isl_mat *div) +{ + int i; + unsigned total; + + if (!bset || !div) + goto error; + + bset = isl_basic_set_extend_constraints(bset, 0, 2 * div->n_row); + if (!bset) + goto error; + total = isl_basic_set_total_dim(bset); + for (i = 0; i < div->n_row; ++i) + if (isl_basic_set_add_div_constraints_var(bset, + total - div->n_row + i, div->row[i]) < 0) + goto error; + + isl_mat_free(div); + return bset; +error: + isl_mat_free(div); + isl_basic_set_free(bset); + return NULL; +} + +/* Look for equalities among the variables shared by context and qp + * and the integer divisions of qp, if any. + * The equalities are then used to eliminate variables and/or integer + * divisions from qp. + */ +__isl_give isl_qpolynomial *isl_qpolynomial_gist( + __isl_take isl_qpolynomial *qp, __isl_take isl_set *context) +{ + isl_basic_set *aff; + + if (!qp) + goto error; + if (qp->div->n_row > 0) { + isl_basic_set *bset; + context = isl_set_add_dims(context, isl_dim_set, + qp->div->n_row); + bset = isl_basic_set_universe(isl_set_get_dim(context)); + bset = add_div_constraints(bset, isl_mat_copy(qp->div)); + context = isl_set_intersect(context, + isl_set_from_basic_set(bset)); + } + + aff = isl_set_affine_hull(context); + return isl_qpolynomial_substitute_equalities(qp, aff); +error: + isl_qpolynomial_free(qp); + isl_set_free(context); + return NULL; +} + #undef PW #define PW isl_pw_qpolynomial #undef EL @@ -2667,32 +2723,6 @@ error: return NULL; } -static __isl_give isl_basic_set *add_div_constraints( - __isl_take isl_basic_set *bset, __isl_take isl_mat *div) -{ - int i; - unsigned total; - - if (!bset || !div) - goto error; - - bset = isl_basic_set_extend_constraints(bset, 0, 2 * div->n_row); - if (!bset) - goto error; - total = isl_basic_set_total_dim(bset); - for (i = 0; i < div->n_row; ++i) - if (isl_basic_set_add_div_constraints_var(bset, - total - div->n_row + i, div->row[i]) < 0) - goto error; - - isl_mat_free(div); - return bset; -error: - isl_mat_free(div); - isl_basic_set_free(bset); - return NULL; -} - /* Extend "bset" with extra set dimensions for each integer division * in "qp" and then call "fn" with the extended bset and the polynomial * that results from replacing each of the integer divisions by the diff --git a/isl_polynomial_private.h b/isl_polynomial_private.h index 32fbc86..1e4295c 100644 --- a/isl_polynomial_private.h +++ b/isl_polynomial_private.h @@ -199,6 +199,10 @@ __isl_give isl_qpolynomial *isl_qpolynomial_substitute_equalities( __isl_take isl_qpolynomial *qp, __isl_take isl_basic_set *eq); __isl_give isl_qpolynomial_fold *isl_qpolynomial_fold_substitute_equalities( __isl_take isl_qpolynomial_fold *fold, __isl_take isl_basic_set *eq); +__isl_give isl_qpolynomial *isl_qpolynomial_gist( + __isl_take isl_qpolynomial *qp, __isl_take isl_set *context); +__isl_give isl_qpolynomial_fold *isl_qpolynomial_fold_gist( + __isl_take isl_qpolynomial_fold *fold, __isl_take isl_set *context); __isl_give isl_qpolynomial *isl_qpolynomial_realign( __isl_take isl_qpolynomial *qp, __isl_take isl_reordering *r); diff --git a/isl_pw_templ.c b/isl_pw_templ.c index 7f780b2..0555091 100644 --- a/isl_pw_templ.c +++ b/isl_pw_templ.c @@ -409,14 +409,12 @@ __isl_give PW *FN(PW,gist)(__isl_take PW *pw, __isl_take isl_set *context) goto error; for (i = pw->n - 1; i >= 0; --i) { - isl_basic_set *aff; pw->p[i].set = isl_set_intersect(pw->p[i].set, isl_set_copy(context)); if (!pw->p[i].set) goto error; - aff = isl_set_affine_hull(isl_set_copy(pw->p[i].set)); - pw->p[i].FIELD = FN(EL,substitute_equalities)(pw->p[i].FIELD, - aff); + pw->p[i].FIELD = FN(EL,gist)(pw->p[i].FIELD, + isl_set_copy(pw->p[i].set)); pw->p[i].set = isl_set_gist_basic_set(pw->p[i].set, isl_basic_set_copy(hull)); if (!pw->p[i].set) diff --git a/isl_test.c b/isl_test.c index bc03b84..190083b 100644 --- a/isl_test.c +++ b/isl_test.c @@ -1465,6 +1465,20 @@ void test_pwqp(struct isl_ctx *ctx) assert(isl_pw_qpolynomial_is_zero(pwqp1)); isl_pw_qpolynomial_free(pwqp1); + + str = "{ [i] -> ([(i)/2]) }"; + pwqp1 = isl_pw_qpolynomial_read_from_str(ctx, str); + str = "{ [k] : exists a : k = 2a+1 }"; + set = isl_set_read_from_str(ctx, str, 0); + pwqp1 = isl_pw_qpolynomial_gist(pwqp1, set); + str = "{ [i] -> -1/2 + 1/2 * i }"; + pwqp2 = isl_pw_qpolynomial_read_from_str(ctx, str); + + pwqp1 = isl_pw_qpolynomial_sub(pwqp1, pwqp2); + + assert(isl_pw_qpolynomial_is_zero(pwqp1)); + + isl_pw_qpolynomial_free(pwqp1); } void test_split_periods(isl_ctx *ctx) -- 2.7.4