From a7b6a83e955d426b8e8db3ce43579bba80dd63a8 Mon Sep 17 00:00:00 2001
From: Sven Verdoolaege <skimo@kotnet.org>
Date: Mon, 26 Jan 2009 23:38:49 +0100
Subject: [PATCH] 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.
---
 isl_map_simplify.c | 18 ++++++++++++++++--
 isl_test.c         | 29 +++++++++++++++++++++++++++++
 2 files changed, 45 insertions(+), 2 deletions(-)

diff --git a/isl_map_simplify.c b/isl_map_simplify.c
index d8c9dab..b6d891a 100644
--- 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
--- 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);
 }
 
-- 
2.7.4