isl_pw_qpolynomial_gist: also try to eliminate integer divisions

Signed-off-by: Sven Verdoolaege <skimo@kotnet.org>

diff --git a/isl_fold.c b/isl_fold.c
index 2f37054..38fbf99 100644 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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)