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>

diff --git a/isl_map_simplify.c b/isl_map_simplify.c
index 145428e..ef9e90d 100644 (file)
--- 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 8bf31f3..22871c1 100644 (file)
--- 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 },