From: Sven Verdoolaege <skimo@kotnet.org>
Date: Wed, 16 May 2012 14:01:24 +0000 (+0200)
Subject: isl_basic_map_simplify: normalize div expressions
X-Git-Tag: isl-0.11~275
X-Git-Url: http://review.tizen.org/git/?a=commitdiff_plain;h=7c513a3bc2033ec87934c7287262ba0ec65c9adb;p=platform%2Fupstream%2Fisl.git

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
--- 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
--- 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;
 }