isl_map_compute_divs: drop obviously redundant divs first

diff --git a/isl_map.c b/isl_map.c
index d23c30e..3f84e07 100644 (file)
--- a/isl_map.c
+++ b/isl_map.c
@@ -2944,6 +2944,11 @@ error:
        return NULL;
 }
 
+/* If bmap contains any unknown divs, then compute explicit
+ * expressions for them.  However, this computation may be
+ * quite expensive, so first try to remove divs that aren't
+ * strictly needed.
+ */
 struct isl_map *isl_basic_map_compute_divs(struct isl_basic_map *bmap)
 {
        int i;
@@ -2954,11 +2959,22 @@ struct isl_map *isl_basic_map_compute_divs(struct isl_basic_map *bmap)
        off = isl_dim_total(bmap->dim);
        for (i = 0; i < bmap->n_div; ++i) {
                if (isl_int_is_zero(bmap->div[i][0]))
-                       return isl_pip_basic_map_compute_divs(bmap);
+                       break;
                isl_assert(bmap->ctx, isl_int_is_zero(bmap->div[i][1+1+off+i]),
                                goto error);
        }
-       return isl_map_from_basic_map(bmap);
+       if (i == bmap->n_div)
+               return isl_map_from_basic_map(bmap);
+       bmap = isl_basic_map_drop_redundant_divs(bmap);
+       if (!bmap)
+               goto error;
+       for (i = 0; i < bmap->n_div; ++i)
+               if (isl_int_is_zero(bmap->div[i][0]))
+                       break;
+       if (i == bmap->n_div)
+               return isl_map_from_basic_map(bmap);
+       struct isl_map *map = isl_pip_basic_map_compute_divs(bmap);
+       return map;
 error:
        isl_basic_map_free(bmap);
        return NULL;

diff --git a/isl_map_private.h b/isl_map_private.h
index 3ef8dbf..de112b4 100644 (file)
--- a/isl_map_private.h
+++ b/isl_map_private.h
@@ -106,3 +106,6 @@ struct isl_basic_set *isl_basic_set_eliminate_vars(
 
 int isl_basic_set_constraint_is_redundant(struct isl_basic_set **bset,
        isl_int *c, isl_int *opt_n, isl_int *opt_d);
+
+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 d43f609..1a4bfa2 100644 (file)
--- a/isl_map_simplify.c
+++ b/isl_map_simplify.c
@@ -1855,3 +1855,91 @@ int isl_set_fast_is_disjoint(struct isl_set *set1, struct isl_set *set2)
        return isl_map_fast_is_disjoint((struct isl_map *)set1,
                                        (struct isl_map *)set2);
 }
+
+/* Remove divs that are not strictly needed.
+ * In particular, if a div only occurs positively (or negatively)
+ * in constraints, then it can simply be dropped.
+ * Also, if a div occurs only occurs in two constraints and if moreover
+ * those two constraints are opposite to each other, except for the constant
+ * term and if the sum of the constant terms is such that for any value
+ * of the other values, there is always at least one integer value of the
+ * div, i.e., if one plus this sum is greater than or equal to
+ * the (absolute value) of the coefficent of the div in the constraints,
+ * then we can also simply drop the div.
+ */
+struct isl_basic_map *isl_basic_map_drop_redundant_divs(
+       struct isl_basic_map *bmap)
+{
+       int i, j;
+       unsigned off;
+
+       if (!bmap)
+               goto error;
+
+       off = isl_dim_total(bmap->dim);
+
+       for (i = 0; i < bmap->n_div; ++i) {
+               int pos, neg;
+               int last_pos, last_neg;
+               int redundant;
+
+               if (!isl_int_is_zero(bmap->div[i][0]))
+                       continue;
+               for (j = 0; j < bmap->n_eq; ++j)
+                       if (!isl_int_is_zero(bmap->eq[j][1 + off + i]))
+                               break;
+               if (j < bmap->n_eq)
+                       continue;
+               pos = neg = 0;
+               for (j = 0; j < bmap->n_ineq; ++j) {
+                       if (isl_int_is_pos(bmap->ineq[j][1 + off + i])) {
+                               last_pos = j;
+                               ++pos;
+                       }
+                       if (isl_int_is_neg(bmap->ineq[j][1 + off + i])) {
+                               last_neg = j;
+                               ++neg;
+                       }
+               }
+               if (pos * neg == 0) {
+                       for (j = bmap->n_ineq - 1; j >= 0; --j)
+                               if (!isl_int_is_zero(bmap->ineq[j][1+off+i]))
+                                       isl_basic_map_drop_inequality(bmap, j);
+                       bmap = isl_basic_map_drop_div(bmap, i);
+                       return isl_basic_map_drop_redundant_divs(bmap);
+               }
+               if (pos * neg != 1)
+                       continue;
+               if (!isl_seq_is_neg(bmap->ineq[last_pos] + 1,
+                                   bmap->ineq[last_neg] + 1,
+                                   off + bmap->n_div))
+                       continue;
+
+               isl_int_add(bmap->ineq[last_pos][0],
+                           bmap->ineq[last_pos][0], bmap->ineq[last_neg][0]);
+               isl_int_add_ui(bmap->ineq[last_pos][0],
+                              bmap->ineq[last_pos][0], 1);
+               redundant = isl_int_ge(bmap->ineq[last_pos][0],
+                               bmap->ineq[last_pos][1+off+i]);
+               isl_int_sub_ui(bmap->ineq[last_pos][0],
+                              bmap->ineq[last_pos][0], 1);
+               isl_int_sub(bmap->ineq[last_pos][0],
+                           bmap->ineq[last_pos][0], bmap->ineq[last_neg][0]);
+               if (!redundant)
+                       continue;
+               if (last_pos > last_neg) {
+                       isl_basic_map_drop_inequality(bmap, last_pos);
+                       isl_basic_map_drop_inequality(bmap, last_neg);
+               } else {
+                       isl_basic_map_drop_inequality(bmap, last_neg);
+                       isl_basic_map_drop_inequality(bmap, last_pos);
+               }
+               bmap = isl_basic_map_drop_div(bmap, i);
+               return isl_basic_map_drop_redundant_divs(bmap);
+       }
+
+       return bmap;
+error:
+       isl_basic_map_free(bmap);
+       return NULL;
+}