isl_basic_map_simplify: normalize div expressions

That is, remove common divisors in numerator and denominator.

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

diff --git a/isl_map_simplify.c b/isl_map_simplify.c
index d550698..fa80971 100644 (file)
--- a/isl_map_simplify.c
+++ b/isl_map_simplify.c
@@ -1,10 +1,12 @@
 /*
  * Copyright 2008-2009 Katholieke Universiteit Leuven
+ * Copyright 2012      Ecole Normale Superieure
  *
  * Use of this software is governed by the GNU LGPLv2.1 license
  *
  * Written by Sven Verdoolaege, K.U.Leuven, Departement
  * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium
+ * and Ecole Normale Superieure, 45 rue d’Ulm, 75230 Paris, France
  */
 
 #include <strings.h>
@@ -370,6 +372,49 @@ struct isl_basic_set *isl_basic_set_normalize_constraints(
                (struct isl_basic_map *)bset);
 }
 
+/* Remove any common factor in numerator and denominator of a div expression,
+ * not taking into account the constant term.
+ * That is, look for any div of the form
+ *
+ *     floor((a + m f(x))/(m d))
+ *
+ * and replace it by
+ *
+ *     floor((floor(a/m) + f(x))/d)
+ *
+ * The difference {a/m}/d in the argument satisfies 0 <= {a/m}/d < 1/d
+ * and can therefore not influence the result of the floor.
+ */
+static __isl_give isl_basic_map *normalize_div_expressions(
+       __isl_take isl_basic_map *bmap)
+{
+       int i;
+       isl_int gcd;
+       unsigned total = isl_basic_map_total_dim(bmap);
+
+       if (!bmap)
+               return NULL;
+       if (bmap->n_div == 0)
+               return bmap;
+
+       isl_int_init(gcd);
+       for (i = 0; i < bmap->n_div; ++i) {
+               if (isl_int_is_zero(bmap->div[i][0]))
+                       continue;
+               isl_seq_gcd(bmap->div[i] + 2, total, &gcd);
+               isl_int_gcd(gcd, gcd, bmap->div[i][0]);
+               if (isl_int_is_one(gcd))
+                       continue;
+               isl_int_fdiv_q(bmap->div[i][1], bmap->div[i][1], gcd);
+               isl_int_divexact(bmap->div[i][0], bmap->div[i][0], gcd);
+               isl_seq_scale_down(bmap->div[i] + 2, bmap->div[i] + 2, gcd,
+                                       total);
+       }
+       isl_int_clear(gcd);
+
+       return bmap;
+}
+
 /* Assumes divs have been ordered if keep_divs is set.
  */
 static void eliminate_var_using_equality(struct isl_basic_map *bmap,
@@ -1092,6 +1137,7 @@ 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 = normalize_div_expressions(bmap);
                bmap = remove_duplicate_divs(bmap, &progress);
                bmap = eliminate_divs_eq(bmap, &progress);
                bmap = eliminate_divs_ineq(bmap, &progress);

diff --git a/isl_test.c b/isl_test.c
index 05c8364..7c12366 100644 (file)
--- a/isl_test.c
+++ b/isl_test.c
@@ -312,6 +312,7 @@ void test_dim(struct isl_ctx *ctx)
 
 static int test_div(isl_ctx *ctx)
 {
+       unsigned n;
        const char *str;
        isl_int v;
        isl_space *dim;
@@ -617,6 +618,16 @@ static int test_div(isl_ctx *ctx)
        if (!set)
                return -1;
 
+       str = "{ [i,j] : 2*[i/2] + 3 * [j/4] <= 10 and 2 i = j }";
+       bset = isl_basic_set_read_from_str(ctx, str);
+       n = isl_basic_set_dim(bset, isl_dim_div);
+       isl_basic_set_free(bset);
+       if (!bset)
+               return -1;
+       if (n != 1)
+               isl_die(ctx, isl_error_unknown,
+                       "expecting a single existential", return -1);
+
        return 0;
 }