isl_*_eliminate: perform integer elimination

The original code would perform the elimination "rationally" by
simply applying Fourier-Motzkin on them.  If the input
is an integer set or map, this could drop information on other dimensions.
For example, eliminating the second dimension of

        { [i, j] : i = 2 j }

would result in

        { [i, j] }

while it should result in

        { [i, j] : exists a : i = 2 a }

We now perform an integer elimination (on integer sets and maps).

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

2 files changed, 34 insertions, 5 deletions

diff --git a/isl_map_simplify.c b/isl_map_simplify.c
index 145428e4..ef9e90d3 100644
--- a/isl_map_simplify.c
+++ b/isl_map_simplify.c
@@ -1376,13 +1376,16 @@ struct isl_basic_set *isl_basic_set_eliminate_vars(
 }
 
 /* Eliminate the specified n dimensions starting at first from the
- * constraints using Fourier-Motzkin.  The dimensions themselves
- * are not removed.
+ * constraints, without removing the dimensions from the space.
+ * If the set is rational, the dimensions are eliminated using Fourier-Motzkin.
+ * Otherwise, they are projected out and the original space is restored.
  */
 __isl_give isl_basic_map *isl_basic_map_eliminate(
 	__isl_take isl_basic_map *bmap,
 	enum isl_dim_type type, unsigned first, unsigned n)
 {
+	isl_space *space;
+
 	if (!bmap)
 		return NULL;
 	if (n == 0)
@@ -1392,9 +1395,17 @@ __isl_give isl_basic_map *isl_basic_map_eliminate(
 		isl_die(bmap->ctx, isl_error_invalid,
 			"index out of bounds", goto error);
 
-	first += isl_basic_map_offset(bmap, type) - 1;
-	bmap = isl_basic_map_eliminate_vars(bmap, first, n);
-	return isl_basic_map_finalize(bmap);
+	if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_RATIONAL)) {
+		first += isl_basic_map_offset(bmap, type) - 1;
+		bmap = isl_basic_map_eliminate_vars(bmap, first, n);
+		return isl_basic_map_finalize(bmap);
+	}
+
+	space = isl_basic_map_get_space(bmap);
+	bmap = isl_basic_map_project_out(bmap, type, first, n);
+	bmap = isl_basic_map_insert(bmap, type, first, n);
+	bmap = isl_basic_map_reset_space(bmap, space);
+	return bmap;
 error:
 	isl_basic_map_free(bmap);
 	return NULL;
diff --git a/isl_test.c b/isl_test.c
index 8bf31f36..22871c1f 100644
--- a/isl_test.c
+++ b/isl_test.c
@@ -2963,10 +2963,28 @@ int test_slice(isl_ctx *ctx)
 	return 0;
 }
 
+int test_eliminate(isl_ctx *ctx)
+{
+	const char *str;
+	isl_map *map;
+	int equal;
+
+	str = "{ [i] -> [j] : i = 2j }";
+	map = isl_map_read_from_str(ctx, str);
+	map = isl_map_eliminate(map, isl_dim_out, 0, 1);
+	equal = map_check_equal(map, "{ [i] -> [j] : exists a : i = 2a }");
+	isl_map_free(map);
+	if (equal < 0)
+		return -1;
+
+	return 0;
+}
+
 struct {
 	const char *name;
 	int (*fn)(isl_ctx *ctx);
 } tests [] = {
+	{ "eliminate", &test_eliminate },
 	{ "div", &test_div },
 	{ "slice", &test_slice },
 	{ "fixed power", &test_fixed_power },