isl_map_simplify.c: normalize_divs: ensure enough existentials are available

Before, we would assume that normalizing the divs could never
increase the number of existential variables, but as shown by
the added test case, this isn't always true.

diff --git a/isl_map_simplify.c b/isl_map_simplify.c
index d8c9dab..b6d891a 100644 (file)
--- a/isl_map_simplify.c
+++ b/isl_map_simplify.c
@@ -644,6 +644,7 @@ static struct isl_basic_map *normalize_divs(
        struct isl_mat *C2 = NULL;
        isl_int v;
        int *pos;
+       int dropped, needed;
 
        if (!bmap)
                return NULL;
@@ -718,6 +719,7 @@ static struct isl_basic_map *normalize_divs(
        isl_int_clear(v);
        pos = isl_alloc_array(bmap->ctx, int, T->n_row);
        /* We have to be careful because dropping equalities may reorder them */
+       dropped = 0;
        for (j = bmap->n_div - 1; j >= 0; --j) {
                for (i = 0; i < bmap->n_eq; ++i)
                        if (!isl_int_is_zero(bmap->eq[i][1 + total + j]))
@@ -725,14 +727,26 @@ static struct isl_basic_map *normalize_divs(
                if (i < bmap->n_eq) {
                        bmap = isl_basic_map_drop_div(bmap, j);
                        isl_basic_map_drop_equality(bmap, i);
+                       ++dropped;
                }
        }
        pos[0] = 0;
+       needed = 0;
        for (i = 1; i < T->n_row; ++i) {
-               if (isl_int_is_one(T->row[i][i])) {
+               if (isl_int_is_one(T->row[i][i]))
                        pos[i] = i;
+               else
+                       needed++;
+       }
+       if (needed > dropped) {
+               bmap = isl_basic_map_extend_dim(bmap, isl_dim_copy(bmap->dim),
+                               needed, needed, 0);
+               if (!bmap)
+                       goto error;
+       }
+       for (i = 1; i < T->n_row; ++i) {
+               if (isl_int_is_one(T->row[i][i]))
                        continue;
-               }
                k = isl_basic_map_alloc_div(bmap);
                pos[i] = 1 + total + k;
                isl_seq_clr(bmap->div[k] + 1, 1 + total + bmap->n_div);

diff --git a/isl_test.c b/isl_test.c
index c2516c8..8db04a4 100644 (file)
--- a/isl_test.c
+++ b/isl_test.c
@@ -237,6 +237,35 @@ void test_div(struct isl_ctx *ctx)
        assert(bset->n_div == 1);
        isl_basic_set_free(bset);
 
+       /* test 7 */
+       /* This test is a bit tricky.  We set up an equality
+        *              a + 3b + 3c = 6 e0
+        * Normalization of divs creates _two_ divs
+        *              a = 3 e0
+        *              c - b - e0 = 2 e1
+        * Afterwards e0 is removed again because it has coefficient -1
+        * and we end up with the original equality and div again.
+        * Perhaps we can avoid the introduction of this temporary div.
+        */
+       dim = isl_dim_set_alloc(ctx, 0, 3);
+       bset = isl_basic_set_universe(dim);
+
+       c = isl_equality_alloc(isl_dim_copy(bset->dim));
+       isl_int_set_si(v, -1);
+       isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
+       isl_int_set_si(v, -3);
+       isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
+       isl_int_set_si(v, -3);
+       isl_constraint_set_coefficient(c, isl_dim_set, 2, v);
+       div = isl_div_alloc(isl_dim_copy(bset->dim));
+       c = isl_constraint_add_div(c, div, &pos);
+       isl_int_set_si(v, 6);
+       isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
+       bset = isl_basic_set_add_constraint(bset, c);
+
+       assert(bset->n_div == 1);
+       isl_basic_set_free(bset);
+
        isl_int_clear(v);
 }