isl_tab: optionally save dual solution
[platform/upstream/isl.git] / isl_map_simplify.c
index bb48508..b797b5e 100644 (file)
@@ -110,7 +110,34 @@ error:
        return NULL;
 }
 
-/* Drop n input dimensions starting at first.
+/* Move "n" divs starting at "first" to the end of the list of divs.
+ */
+static struct isl_basic_map *move_divs_last(struct isl_basic_map *bmap,
+       unsigned first, unsigned n)
+{
+       isl_int **div;
+       int i;
+
+       if (first + n == bmap->n_div)
+               return bmap;
+
+       div = isl_alloc_array(bmap->ctx, isl_int *, n);
+       if (!div)
+               goto error;
+       for (i = 0; i < n; ++i)
+               div[i] = bmap->div[first + i];
+       for (i = 0; i < bmap->n_div - first - n; ++i)
+               bmap->div[first + i] = bmap->div[first + n + i];
+       for (i = 0; i < n; ++i)
+               bmap->div[bmap->n_div - n + i] = div[i];
+       free(div);
+       return bmap;
+error:
+       isl_basic_map_free(bmap);
+       return NULL;
+}
+
+/* Drop "n" dimensions of type "type" starting at "first".
  *
  * In principle, this frees up some extra variables as the number
  * of columns remains constant, but we would have to extend
@@ -149,7 +176,13 @@ struct isl_basic_map *isl_basic_map_drop(struct isl_basic_map *bmap,
        for (i = 0; i < bmap->n_div; ++i)
                constraint_drop_vars(bmap->div[i]+1+offset, n, left);
 
-       bmap->dim = isl_dim_drop(bmap->dim, type, first, n);
+       if (type == isl_dim_div) {
+               bmap = move_divs_last(bmap, first, n);
+               if (!bmap)
+                       goto error;
+               isl_basic_map_free_div(bmap, n);
+       } else
+               bmap->dim = isl_dim_drop(bmap->dim, type, first, n);
        if (!bmap->dim)
                goto error;
 
@@ -627,6 +660,23 @@ out:
        return bmap;
 }
 
+static int n_pure_div_eq(struct isl_basic_map *bmap)
+{
+       int i, j;
+       unsigned total;
+
+       total = isl_dim_total(bmap->dim);
+       for (i = 0, j = bmap->n_div-1; i < bmap->n_eq; ++i) {
+               while (j >= 0 && isl_int_is_zero(bmap->eq[i][1 + total + j]))
+                       --j;
+               if (j < 0)
+                       break;
+               if (isl_seq_first_non_zero(bmap->eq[i] + 1 + total, j) != -1)
+                       return 0;
+       }
+       return i;
+}
+
 /* Normalize divs that appear in equalities.
  *
  * In particular, we assume that bmap contains some equalities
@@ -703,15 +753,7 @@ static struct isl_basic_map *normalize_divs(
                return bmap;
 
        total = isl_dim_total(bmap->dim);
-       for (i = 0, j = bmap->n_div-1; i < bmap->n_eq; ++i) {
-               while (j >= 0 && isl_int_is_zero(bmap->eq[i][1 + total + j]))
-                       --j;
-               if (j < 0)
-                       break;
-               if (isl_seq_first_non_zero(bmap->eq[i] + 1 + total, j) != -1)
-                       goto done;
-       }
-       div_eq = i;
+       div_eq = n_pure_div_eq(bmap);
        if (div_eq == 0)
                return bmap;
 
@@ -817,7 +859,8 @@ static struct isl_basic_map *normalize_divs(
        isl_mat_free(bmap->ctx, C2);
        isl_mat_free(bmap->ctx, T);
 
-       *progress = 1;
+       if (progress)
+               *progress = 1;
 done:
        ISL_F_SET(bmap, ISL_BASIC_MAP_NORMALIZED_DIVS);
 
@@ -829,6 +872,92 @@ error:
        return bmap;
 }
 
+static struct isl_basic_map *set_div_from_lower_bound(
+       struct isl_basic_map *bmap, int div, int ineq)
+{
+       unsigned total = 1 + isl_dim_total(bmap->dim);
+
+       isl_seq_neg(bmap->div[div] + 1, bmap->ineq[ineq], total + bmap->n_div);
+       isl_int_set(bmap->div[div][0], bmap->ineq[ineq][total + div]);
+       isl_int_add(bmap->div[div][1], bmap->div[div][1], bmap->div[div][0]);
+       isl_int_sub_ui(bmap->div[div][1], bmap->div[div][1], 1);
+       isl_int_set_si(bmap->div[div][1 + total + div], 0);
+
+       return bmap;
+}
+
+/* Check whether it is ok to define a div based on an inequality.
+ * To avoid the introduction of circular definitions of divs, we
+ * do not allow such a definition if the resulting expression would refer to
+ * any other undefined divs or if any known div is defined in
+ * terms of the unknown div.
+ */
+static int ok_to_set_div_from_bound(struct isl_basic_map *bmap,
+       int div, int ineq)
+{
+       int j;
+       unsigned total = 1 + isl_dim_total(bmap->dim);
+
+       /* Not defined in terms of unknown divs */
+       for (j = 0; j < bmap->n_div; ++j) {
+               if (div == j)
+                       continue;
+               if (isl_int_is_zero(bmap->ineq[ineq][total + j]))
+                       continue;
+               if (isl_int_is_zero(bmap->div[j][0]))
+                       return 0;
+       }
+
+       /* No other div defined in terms of this one => avoid loops */
+       for (j = 0; j < bmap->n_div; ++j) {
+               if (div == j)
+                       continue;
+               if (isl_int_is_zero(bmap->div[j][0]))
+                       continue;
+               if (!isl_int_is_zero(bmap->div[j][1 + total + div]))
+                       return 0;
+       }
+
+       return 1;
+}
+
+/* Given two constraints "k" and "l" that are opposite to each other,
+ * except for the constant term, check if we can use them
+ * to obtain an expression for one of the hitherto unknown divs.
+ * "sum" is the sum of the constant terms of the constraints.
+ * If this sum is strictly smaller than the coefficient of one
+ * of the divs, then this pair can be used define the div.
+ * To avoid the introduction of circular definitions of divs, we
+ * do not use the pair if the resulting expression would refer to
+ * any other undefined divs or if any known div is defined in
+ * terms of the unknown div.
+ */
+static struct isl_basic_map *check_for_div_constraints(
+       struct isl_basic_map *bmap, int k, int l, isl_int sum, int *progress)
+{
+       int i, j;
+       unsigned total = 1 + isl_dim_total(bmap->dim);
+
+       for (i = 0; i < bmap->n_div; ++i) {
+               if (!isl_int_is_zero(bmap->div[i][0]))
+                       continue;
+               if (isl_int_is_zero(bmap->ineq[k][total + i]))
+                       continue;
+               if (isl_int_abs_ge(sum, bmap->ineq[k][total + i]))
+                       continue;
+               if (!ok_to_set_div_from_bound(bmap, i, k))
+                       break;
+               if (isl_int_is_pos(bmap->ineq[k][total + i]))
+                       bmap = set_div_from_lower_bound(bmap, i, k);
+               else
+                       bmap = set_div_from_lower_bound(bmap, i, l);
+               if (progress)
+                       *progress = 1;
+               break;
+       }
+       return bmap;
+}
+
 static struct isl_basic_map *remove_duplicate_constraints(
        struct isl_basic_map *bmap, int *progress)
 {
@@ -872,8 +1001,11 @@ static struct isl_basic_map *remove_duplicate_constraints(
                        continue;
                l = index[h] - &bmap->ineq[0];
                isl_int_add(sum, bmap->ineq[k][0], bmap->ineq[l][0]);
-               if (isl_int_is_pos(sum))
+               if (isl_int_is_pos(sum)) {
+                       bmap = check_for_div_constraints(bmap, k, l, sum,
+                                                        progress);
                        continue;
+               }
                if (isl_int_is_zero(sum)) {
                        /* We need to break out of the loop after these
                         * changes since the contents of the hash
@@ -901,12 +1033,12 @@ struct isl_basic_map *isl_basic_map_simplify(struct isl_basic_map *bmap)
        while (progress) {
                progress = 0;
                bmap = isl_basic_map_normalize_constraints(bmap);
+               bmap = remove_duplicate_divs(bmap, &progress);
                bmap = eliminate_divs_eq(bmap, &progress);
                bmap = eliminate_divs_ineq(bmap, &progress);
                bmap = isl_basic_map_gauss(bmap, &progress);
                /* requires equalities in normal form */
                bmap = normalize_divs(bmap, &progress);
-               bmap = remove_duplicate_divs(bmap, &progress);
                bmap = remove_duplicate_constraints(bmap, &progress);
        }
        return bmap;
@@ -1336,6 +1468,9 @@ static struct isl_basic_set *normalize_constraints_in_compressed_space(
        if (ISL_F_ISSET(bset, ISL_BASIC_SET_RATIONAL))
                return bset;
 
+       if (!bset->n_ineq)
+               return bset;
+
        bset = isl_basic_set_cow(bset);
        if (!bset)
                return NULL;
@@ -1409,6 +1544,10 @@ static struct isl_basic_set *uset_gist(struct isl_basic_set *bset,
                                        isl_basic_set_copy(context));
        if (!bset)
                goto error;
+       if (isl_basic_set_fast_is_empty(bset))
+               goto done;
+       if (!bset->n_ineq)
+               goto done;
 
        if (bset->n_eq > 0) {
                struct isl_basic_set *affine_hull;
@@ -1473,6 +1612,43 @@ error2:
        return NULL;
 }
 
+/* Normalize the divs in "bmap" in the context of the equalities in "context".
+ * We simply add the equalities in context to bmap and then do a regular
+ * div normalizations.  Better results can be obtained by normalizing
+ * only the divs in bmap than do not also appear in context.
+ * We need to be careful to reduce the divs using the equalities
+ * so that later calls to isl_basic_map_overlying_set wouldn't introduce
+ * spurious constraints.
+ */
+static struct isl_basic_map *normalize_divs_in_context(
+       struct isl_basic_map *bmap, struct isl_basic_map *context)
+{
+       int i;
+       unsigned total_context;
+       int div_eq;
+
+       div_eq = n_pure_div_eq(bmap);
+       if (div_eq == 0)
+               return bmap;
+
+       if (context->n_div > 0)
+               bmap = isl_basic_map_align_divs(bmap, context);
+
+       total_context = isl_basic_map_total_dim(context);
+       bmap = isl_basic_map_extend_constraints(bmap, context->n_eq, 0);
+       for (i = 0; i < context->n_eq; ++i) {
+               int k;
+               k = isl_basic_map_alloc_equality(bmap);
+               isl_seq_cpy(bmap->eq[k], context->eq[i], 1 + total_context);
+               isl_seq_clr(bmap->eq[k] + 1 + total_context,
+                               isl_basic_map_total_dim(bmap) - total_context);
+       }
+       bmap = isl_basic_map_gauss(bmap, NULL);
+       bmap = normalize_divs(bmap, NULL);
+       bmap = isl_basic_map_gauss(bmap, NULL);
+       return bmap;
+}
+
 struct isl_basic_map *isl_basic_map_gist(struct isl_basic_map *bmap,
        struct isl_basic_map *context)
 {
@@ -1503,6 +1679,9 @@ struct isl_basic_map *isl_basic_map_gist(struct isl_basic_map *bmap,
        bmap = isl_basic_map_convex_hull(bmap);
        context = isl_basic_map_convex_hull(context);
 
+       if (context->n_eq)
+               bmap = normalize_divs_in_context(bmap, context);
+
        context = isl_basic_map_align_divs(context, bmap);
        bmap = isl_basic_map_align_divs(bmap, context);
 
@@ -1630,15 +1809,15 @@ int isl_basic_map_fast_is_disjoint(struct isl_basic_map *bmap1,
                    isl_seq_first_non_zero(v->block.data + 1, total) == -1)
                        goto disjoint;
        }
-       isl_vec_free(bmap1->ctx, v);
+       isl_vec_free(v);
        free(elim);
        return 0;
 disjoint:
-       isl_vec_free(bmap1->ctx, v);
+       isl_vec_free(v);
        free(elim);
        return 1;
 error:
-       isl_vec_free(bmap1->ctx, v);
+       isl_vec_free(v);
        free(elim);
        return -1;
 }
@@ -1676,3 +1855,509 @@ 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);
 }
+
+/* Check if we can combine a given div with lower bound l and upper
+ * bound u with some other div and if so return that other div.
+ * Otherwise return -1.
+ *
+ * We first check that
+ *     - the bounds are opposites of each other (expect for the constant
+ *       term
+ *     - the bounds do not reference any other div
+ *     - no div is defined in terms of this div
+ *
+ * Let m be the size of the range allowed on the div by the bounds.
+ * That is, the bounds are of the form
+ *
+ *     e <= a <= e + m - 1
+ *
+ * with e some expression in the other variables.
+ * We look for another div b such that no third div is defined in terms
+ * of this second div b and such that in any constraint that contains
+ * a (except for the given lower and upper bound), also contains b
+ * with a coefficient that is m times that of b.
+ * That is, all constraints (execpt for the lower and upper bound)
+ * are of the form
+ *
+ *     e + f (a + m b) >= 0
+ *
+ * If so, we return b so that "a + m b" can be replaced by
+ * a single div "c = a + m b".
+ */
+static int div_find_coalesce(struct isl_basic_map *bmap, int *pairs,
+       unsigned div, unsigned l, unsigned u)
+{
+       int i, j;
+       unsigned dim;
+       int coalesce = -1;
+
+       if (bmap->n_div <= 1)
+               return -1;
+       dim = isl_dim_total(bmap->dim);
+       if (isl_seq_first_non_zero(bmap->ineq[l] + 1 + dim, div) != -1)
+               return -1;
+       if (isl_seq_first_non_zero(bmap->ineq[l] + 1 + dim + div + 1,
+                                  bmap->n_div - div - 1) != -1)
+               return -1;
+       if (!isl_seq_is_neg(bmap->ineq[l] + 1, bmap->ineq[u] + 1,
+                           dim + bmap->n_div))
+               return -1;
+
+       for (i = 0; i < bmap->n_div; ++i) {
+               if (isl_int_is_zero(bmap->div[i][0]))
+                       continue;
+               if (!isl_int_is_zero(bmap->div[i][1 + 1 + dim + div]))
+                       return -1;
+       }
+
+       isl_int_add(bmap->ineq[l][0], bmap->ineq[l][0], bmap->ineq[u][0]);
+       isl_int_add_ui(bmap->ineq[l][0], bmap->ineq[l][0], 1);
+       for (i = 0; i < bmap->n_div; ++i) {
+               if (i == div)
+                       continue;
+               if (!pairs[i])
+                       continue;
+               for (j = 0; j < bmap->n_div; ++j) {
+                       if (isl_int_is_zero(bmap->div[j][0]))
+                               continue;
+                       if (!isl_int_is_zero(bmap->div[j][1 + 1 + dim + i]))
+                               break;
+               }
+               if (j < bmap->n_div)
+                       continue;
+               for (j = 0; j < bmap->n_ineq; ++j) {
+                       int valid;
+                       if (j == l || j == u)
+                               continue;
+                       if (isl_int_is_zero(bmap->ineq[j][1 + dim + div]))
+                               continue;
+                       if (isl_int_is_zero(bmap->ineq[j][1 + dim + i]))
+                               break;
+                       isl_int_mul(bmap->ineq[j][1 + dim + div],
+                                   bmap->ineq[j][1 + dim + div],
+                                   bmap->ineq[l][0]);
+                       valid = isl_int_eq(bmap->ineq[j][1 + dim + div],
+                                          bmap->ineq[j][1 + dim + i]);
+                       isl_int_divexact(bmap->ineq[j][1 + dim + div],
+                                        bmap->ineq[j][1 + dim + div],
+                                        bmap->ineq[l][0]);
+                       if (!valid)
+                               break;
+               }
+               if (j < bmap->n_ineq)
+                       continue;
+               coalesce = i;
+               break;
+       }
+       isl_int_sub_ui(bmap->ineq[l][0], bmap->ineq[l][0], 1);
+       isl_int_sub(bmap->ineq[l][0], bmap->ineq[l][0], bmap->ineq[u][0]);
+       return coalesce;
+}
+
+/* Given a lower and an upper bound on div i, construct an inequality
+ * that when nonnegative ensures that this pair of bounds always allows
+ * for an integer value of the given div.
+ * The lower bound is inequality l, while the upper bound is inequality u.
+ * The constructed inequality is stored in ineq.
+ * g, fl, fu are temporary scalars.
+ *
+ * Let the upper bound be
+ *
+ *     -n_u a + e_u >= 0
+ *
+ * and the lower bound
+ *
+ *     n_l a + e_l >= 0
+ *
+ * Let n_u = f_u g and n_l = f_l g, with g = gcd(n_u, n_l).
+ * We have
+ *
+ *     - f_u e_l <= f_u f_l g a <= f_l e_u
+ *
+ * Since all variables are integer valued, this is equivalent to
+ *
+ *     - f_u e_l - (f_u - 1) <= f_u f_l g a <= f_l e_u + (f_l - 1)
+ *
+ * If this interval is at least f_u f_l g, then it contains at least
+ * one integer value for a.
+ * That is, the test constraint is
+ *
+ *     f_l e_u + f_u e_l + f_l - 1 + f_u - 1 + 1 >= f_u f_l g
+ */
+static void construct_test_ineq(struct isl_basic_map *bmap, int i,
+       int l, int u, isl_int *ineq, isl_int g, isl_int fl, isl_int fu)
+{
+       unsigned dim;
+       dim = isl_dim_total(bmap->dim);
+
+       isl_int_gcd(g, bmap->ineq[l][1 + dim + i], bmap->ineq[u][1 + dim + i]);
+       isl_int_divexact(fl, bmap->ineq[l][1 + dim + i], g);
+       isl_int_divexact(fu, bmap->ineq[u][1 + dim + i], g);
+       isl_int_neg(fu, fu);
+       isl_seq_combine(ineq, fl, bmap->ineq[u], fu, bmap->ineq[l],
+                       1 + dim + bmap->n_div);
+       isl_int_add(ineq[0], ineq[0], fl);
+       isl_int_add(ineq[0], ineq[0], fu);
+       isl_int_sub_ui(ineq[0], ineq[0], 1);
+       isl_int_mul(g, g, fl);
+       isl_int_mul(g, g, fu);
+       isl_int_sub(ineq[0], ineq[0], g);
+}
+
+/* Remove more kinds of divs that are not strictly needed.
+ * In particular, if all pairs of lower and upper bounds on a div
+ * are such that they allow at least one integer value of the div,
+ * the we can eliminate the div using Fourier-Motzkin without
+ * introducing any spurious solutions.
+ */
+static struct isl_basic_map *drop_more_redundant_divs(
+       struct isl_basic_map *bmap, int *pairs, int n)
+{
+       struct isl_ctx *ctx = NULL;
+       struct isl_tab *tab = NULL;
+       struct isl_vec *vec = NULL;
+       unsigned dim;
+       int remove = -1;
+       isl_int g, fl, fu;
+
+       isl_int_init(g);
+       isl_int_init(fl);
+       isl_int_init(fu);
+
+       if (!bmap)
+               goto error;
+
+       ctx = bmap->ctx;
+
+       dim = isl_dim_total(bmap->dim);
+       vec = isl_vec_alloc(ctx, 1 + dim + bmap->n_div);
+       if (!vec)
+               goto error;
+
+       tab = isl_tab_from_basic_map(bmap);
+
+       while (n > 0) {
+               int i, l, u;
+               int best = -1;
+               enum isl_lp_result res;
+
+               for (i = 0; i < bmap->n_div; ++i) {
+                       if (!pairs[i])
+                               continue;
+                       if (best >= 0 && pairs[best] <= pairs[i])
+                               continue;
+                       best = i;
+               }
+
+               i = best;
+               for (l = 0; l < bmap->n_ineq; ++l) {
+                       if (!isl_int_is_pos(bmap->ineq[l][1 + dim + i]))
+                               continue;
+                       for (u = 0; u < bmap->n_ineq; ++u) {
+                               if (!isl_int_is_neg(bmap->ineq[u][1 + dim + i]))
+                                       continue;
+                               construct_test_ineq(bmap, i, l, u,
+                                                   vec->el, g, fl, fu);
+                               res = isl_tab_min(ctx, tab, vec->el,
+                                                 ctx->one, &g, NULL, 0);
+                               if (res == isl_lp_error)
+                                       goto error;
+                               if (res == isl_lp_empty) {
+                                       bmap = isl_basic_map_set_to_empty(bmap);
+                                       break;
+                               }
+                               if (res != isl_lp_ok || isl_int_is_neg(g))
+                                       break;
+                       }
+                       if (u < bmap->n_ineq)
+                               break;
+               }
+               if (l == bmap->n_ineq) {
+                       remove = i;
+                       break;
+               }
+               pairs[i] = 0;
+               --n;
+       }
+
+       isl_tab_free(ctx, tab);
+       isl_vec_free(vec);
+
+       isl_int_clear(g);
+       isl_int_clear(fl);
+       isl_int_clear(fu);
+
+       free(pairs);
+
+       if (remove < 0)
+               return bmap;
+
+       bmap = isl_basic_map_remove(bmap, isl_dim_div, remove, 1);
+       return isl_basic_map_drop_redundant_divs(bmap);
+error:
+       free(pairs);
+       isl_basic_map_free(bmap);
+       if (ctx) {
+               isl_tab_free(ctx, tab);
+               isl_vec_free(vec);
+       }
+       isl_int_clear(g);
+       isl_int_clear(fl);
+       isl_int_clear(fu);
+       return NULL;
+}
+
+/* Given a pair of divs div1 and div2 such that, expect for the lower bound l
+ * and the upper bound u, div1 always occurs together with div2 in the form 
+ * (div1 + m div2), where m is the constant range on the variable div1
+ * allowed by l and u, replace the pair div1 and div2 by a single
+ * div that is equal to div1 + m div2.
+ *
+ * The new div will appear in the location that contains div2.
+ * We need to modify all constraints that contain
+ * div2 = (div - div1) / m
+ * (If a constraint does not contain div2, it will also not contain div1.)
+ * If the constraint also contains div1, then we know they appear
+ * as f (div1 + m div2) and we can simply replace (div1 + m div2) by div,
+ * i.e., the coefficient of div is f.
+ *
+ * Otherwise, we first need to introduce div1 into the constraint.
+ * Let the l be
+ *
+ *     div1 + f >=0
+ *
+ * and u
+ *
+ *     -div1 + f' >= 0
+ *
+ * A lower bound on div2
+ *
+ *     n div2 + t >= 0
+ *
+ * can be replaced by
+ *
+ *     (n * (m div 2 + div1) + m t + n f)/g >= 0
+ *
+ * with g = gcd(m,n).
+ * An upper bound
+ *
+ *     -n div2 + t >= 0
+ *
+ * can be replaced by
+ *
+ *     (-n * (m div2 + div1) + m t + n f')/g >= 0
+ *
+ * These constraint are those that we would obtain from eliminating
+ * div1 using Fourier-Motzkin.
+ *
+ * After all constraints have been modified, we drop the lower and upper
+ * bound and then drop div1.
+ */
+static struct isl_basic_map *coalesce_divs(struct isl_basic_map *bmap,
+       unsigned div1, unsigned div2, unsigned l, unsigned u)
+{
+       isl_int a;
+       isl_int b;
+       isl_int m;
+       unsigned dim, total;
+       int i;
+
+       dim = isl_dim_total(bmap->dim);
+       total = 1 + dim + bmap->n_div;
+
+       isl_int_init(a);
+       isl_int_init(b);
+       isl_int_init(m);
+       isl_int_add(m, bmap->ineq[l][0], bmap->ineq[u][0]);
+       isl_int_add_ui(m, m, 1);
+
+       for (i = 0; i < bmap->n_ineq; ++i) {
+               if (i == l || i == u)
+                       continue;
+               if (isl_int_is_zero(bmap->ineq[i][1 + dim + div2]))
+                       continue;
+               if (isl_int_is_zero(bmap->ineq[i][1 + dim + div1])) {
+                       isl_int_gcd(b, m, bmap->ineq[i][1 + dim + div2]);
+                       isl_int_divexact(a, m, b);
+                       isl_int_divexact(b, bmap->ineq[i][1 + dim + div2], b);
+                       if (isl_int_is_pos(b)) {
+                               isl_seq_combine(bmap->ineq[i], a, bmap->ineq[i],
+                                               b, bmap->ineq[l], total);
+                       } else {
+                               isl_int_neg(b, b);
+                               isl_seq_combine(bmap->ineq[i], a, bmap->ineq[i],
+                                               b, bmap->ineq[u], total);
+                       }
+               }
+               isl_int_set(bmap->ineq[i][1 + dim + div2],
+                           bmap->ineq[i][1 + dim + div1]);
+               isl_int_set_si(bmap->ineq[i][1 + dim + div1], 0);
+       }
+
+       isl_int_clear(a);
+       isl_int_clear(b);
+       isl_int_clear(m);
+       if (l > u) {
+               isl_basic_map_drop_inequality(bmap, l);
+               isl_basic_map_drop_inequality(bmap, u);
+       } else {
+               isl_basic_map_drop_inequality(bmap, u);
+               isl_basic_map_drop_inequality(bmap, l);
+       }
+       bmap = isl_basic_map_drop_div(bmap, div1);
+       return bmap;
+}
+
+/* First check if we can coalesce any pair of divs and
+ * then continue with dropping more redundant divs.
+ *
+ * We loop over all pairs of lower and upper bounds on a div
+ * with coefficient 1 and -1, respectively, check if there
+ * is any other div "c" with which we can coalesce the div
+ * and if so, perform the coalescing.
+ */
+static struct isl_basic_map *coalesce_or_drop_more_redundant_divs(
+       struct isl_basic_map *bmap, int *pairs, int n)
+{
+       int i, l, u;
+       unsigned dim;
+
+       dim = isl_dim_total(bmap->dim);
+
+       for (i = 0; i < bmap->n_div; ++i) {
+               if (!pairs[i])
+                       continue;
+               for (l = 0; l < bmap->n_ineq; ++l) {
+                       if (!isl_int_is_one(bmap->ineq[l][1 + dim + i]))
+                               continue;
+                       for (u = 0; u < bmap->n_ineq; ++u) {
+                               int c;
+
+                               if (!isl_int_is_negone(bmap->ineq[u][1+dim+i]))
+                                       continue;
+                               c = div_find_coalesce(bmap, pairs, i, l, u);
+                               if (c < 0)
+                                       continue;
+                               free(pairs);
+                               bmap = coalesce_divs(bmap, i, c, l, u);
+                               return isl_basic_map_drop_redundant_divs(bmap);
+                       }
+               }
+       }
+
+       return drop_more_redundant_divs(bmap, pairs, n);
+}
+
+/* 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.
+ *
+ * If any divs are left after these simple checks then we move on
+ * to more complicated cases in drop_more_redundant_divs.
+ */
+struct isl_basic_map *isl_basic_map_drop_redundant_divs(
+       struct isl_basic_map *bmap)
+{
+       int i, j;
+       unsigned off;
+       int *pairs = NULL;
+       int n = 0;
+
+       if (!bmap)
+               goto error;
+
+       off = isl_dim_total(bmap->dim);
+       pairs = isl_calloc_array(bmap->ctx, int, bmap->n_div);
+       if (!pairs)
+               goto error;
+
+       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;
+               ++n;
+               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;
+                       }
+               }
+               pairs[i] = pos * neg;
+               if (pairs[i] == 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);
+                       free(pairs);
+                       return isl_basic_map_drop_redundant_divs(bmap);
+               }
+               if (pairs[i] != 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) {
+                       if (!ok_to_set_div_from_bound(bmap, i, last_pos)) {
+                               pairs[i] = 0;
+                               --n;
+                               continue;
+                       }
+                       bmap = set_div_from_lower_bound(bmap, i, last_pos);
+                       bmap = isl_basic_map_simplify(bmap);
+                       free(pairs);
+                       return isl_basic_map_drop_redundant_divs(bmap);
+               }
+               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);
+               free(pairs);
+               return isl_basic_map_drop_redundant_divs(bmap);
+       }
+
+       if (n > 0)
+               return coalesce_or_drop_more_redundant_divs(bmap, pairs, n);
+
+       free(pairs);
+       return bmap;
+error:
+       free(pairs);
+       isl_basic_map_free(bmap);
+       return NULL;
+}