X-Git-Url: http://review.tizen.org/git/?a=blobdiff_plain;f=isl_map.c;h=6fffa6018b12a4d71754c94e60618d04a6f64aeb;hb=27b230c534bdef3411e89011354b8606514f8614;hp=d08f8c4f8711ec3946ea471a4c35b58683f56d52;hpb=74218a8133bd6864724192a1a58c83548012d578;p=platform%2Fupstream%2Fisl.git

diff --git a/isl_map.c b/isl_map.c
index d08f8c4..6fffa60 100644
--- a/isl_map.c
+++ b/isl_map.c
@@ -1,7 +1,7 @@
 /*
  * Copyright 2008-2009 Katholieke Universiteit Leuven
  * Copyright 2010      INRIA Saclay
- * Copyright 2012      Ecole Normale Superieure
+ * Copyright 2012-2013 Ecole Normale Superieure
  *
  * Use of this software is governed by the MIT license
  *
@@ -33,6 +33,7 @@
 #include <isl_local_space_private.h>
 #include <isl_aff_private.h>
 #include <isl_options_private.h>
+#include <isl_morph.h>
 
 static unsigned n(__isl_keep isl_space *dim, enum isl_dim_type type)
 {
@@ -1145,6 +1146,13 @@ int isl_basic_set_drop_equality(struct isl_basic_set *bset, unsigned pos)
 	return isl_basic_map_drop_equality((struct isl_basic_map *)bset, pos);
 }
 
+/* Turn inequality "pos" of "bmap" into an equality.
+ *
+ * In particular, we move the inequality in front of the equalities
+ * and move the last inequality in the position of the moved inequality.
+ * Note that isl_tab_make_equalities_explicit depends on this particular
+ * change in the ordering of the constraints.
+ */
 void isl_basic_map_inequality_to_equality(
 		struct isl_basic_map *bmap, unsigned pos)
 {
@@ -1666,13 +1674,25 @@ struct isl_basic_set *isl_basic_set_set_to_empty(struct isl_basic_set *bset)
 		isl_basic_map_set_to_empty((struct isl_basic_map *)bset);
 }
 
-void isl_basic_map_swap_div(struct isl_basic_map *bmap, int a, int b)
+/* Swap divs "a" and "b" in "bmap" (without modifying any of the constraints
+ * of "bmap").
+ */
+static void swap_div(__isl_keep isl_basic_map *bmap, int a, int b)
 {
-	int i;
-	unsigned off = isl_space_dim(bmap->dim, isl_dim_all);
 	isl_int *t = bmap->div[a];
 	bmap->div[a] = bmap->div[b];
 	bmap->div[b] = t;
+}
+
+/* Swap divs "a" and "b" in "bmap" and adjust the constraints and
+ * div definitions accordingly.
+ */
+void isl_basic_map_swap_div(struct isl_basic_map *bmap, int a, int b)
+{
+	int i;
+	unsigned off = isl_space_dim(bmap->dim, isl_dim_all);
+
+	swap_div(bmap, a, b);
 
 	for (i = 0; i < bmap->n_eq; ++i)
 		isl_int_swap(bmap->eq[i][1+off+a], bmap->eq[i][1+off+b]);
@@ -3347,31 +3367,22 @@ static __isl_give isl_basic_map *move_last(__isl_take isl_basic_map *bmap,
 	return res;
 }
 
-/* Turn the n dimensions of type type, starting at first
- * into existentially quantified variables.
+/* Insert "n" rows in the divs of "bmap".
+ *
+ * The number of columns is not changed, which means that the last
+ * dimensions of "bmap" are being reintepreted as the new divs.
+ * The space of "bmap" is not adjusted, however, which means
+ * that "bmap" is left in an inconsistent state.  Removing "n" dimensions
+ * from the space of "bmap" is the responsibility of the caller.
  */
-__isl_give isl_basic_map *isl_basic_map_project_out(
-		__isl_take isl_basic_map *bmap,
-		enum isl_dim_type type, unsigned first, unsigned n)
+static __isl_give isl_basic_map *insert_div_rows(__isl_take isl_basic_map *bmap,
+	int n)
 {
 	int i;
 	size_t row_size;
 	isl_int **new_div;
 	isl_int *old;
 
-	if (n == 0)
-		return basic_map_space_reset(bmap, type);
-
-	if (!bmap)
-		return NULL;
-
-	if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_RATIONAL))
-		return isl_basic_map_remove_dims(bmap, type, first, n);
-
-	isl_assert(bmap->ctx, first + n <= isl_basic_map_dim(bmap, type),
-			goto error);
-
-	bmap = move_last(bmap, type, first, n);
 	bmap = isl_basic_map_cow(bmap);
 	if (!bmap)
 		return NULL;
@@ -3381,10 +3392,10 @@ __isl_give isl_basic_map *isl_basic_map_project_out(
 	bmap->block2 = isl_blk_extend(bmap->ctx, bmap->block2,
 					(bmap->extra + n) * (1 + row_size));
 	if (!bmap->block2.data)
-		goto error;
+		return isl_basic_map_free(bmap);
 	new_div = isl_alloc_array(bmap->ctx, isl_int *, bmap->extra + n);
 	if (!new_div)
-		goto error;
+		return isl_basic_map_free(bmap);
 	for (i = 0; i < n; ++i) {
 		new_div[i] = bmap->block2.data +
 				(bmap->extra + i) * (1 + row_size);
@@ -3397,6 +3408,34 @@ __isl_give isl_basic_map *isl_basic_map_project_out(
 	bmap->n_div += n;
 	bmap->extra += n;
 
+	return bmap;
+}
+
+/* Turn the n dimensions of type type, starting at first
+ * into existentially quantified variables.
+ */
+__isl_give isl_basic_map *isl_basic_map_project_out(
+		__isl_take isl_basic_map *bmap,
+		enum isl_dim_type type, unsigned first, unsigned n)
+{
+	if (n == 0)
+		return basic_map_space_reset(bmap, type);
+
+	if (!bmap)
+		return NULL;
+
+	if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_RATIONAL))
+		return isl_basic_map_remove_dims(bmap, type, first, n);
+
+	isl_assert(bmap->ctx, first + n <= isl_basic_map_dim(bmap, type),
+			goto error);
+
+	bmap = move_last(bmap, type, first, n);
+	bmap = isl_basic_map_cow(bmap);
+	bmap = insert_div_rows(bmap, n);
+	if (!bmap)
+		return NULL;
+
 	bmap->dim = isl_space_drop_dims(bmap->dim, type, first, n);
 	if (!bmap->dim)
 		goto error;
@@ -5331,6 +5370,39 @@ static int remove_if_empty(__isl_keep isl_map *map, int i)
 	return 0;
 }
 
+/* Perform "fn" on each basic map of "map", where we may not be holding
+ * the only reference to "map".
+ * In particular, "fn" should be a semantics preserving operation
+ * that we want to apply to all copies of "map".  We therefore need
+ * to be careful not to modify "map" in a way that breaks "map"
+ * in case anything goes wrong.
+ */
+__isl_give isl_map *isl_map_inline_foreach_basic_map(__isl_take isl_map *map,
+	__isl_give isl_basic_map *(*fn)(__isl_take isl_basic_map *bmap))
+{
+	struct isl_basic_map *bmap;
+	int i;
+
+	if (!map)
+		return NULL;
+
+	for (i = map->n - 1; i >= 0; --i) {
+		bmap = isl_basic_map_copy(map->p[i]);
+		bmap = fn(bmap);
+		if (!bmap)
+			goto error;
+		isl_basic_map_free(map->p[i]);
+		map->p[i] = bmap;
+		if (remove_if_empty(map, i) < 0)
+			goto error;
+	}
+
+	return map;
+error:
+	isl_map_free(map);
+	return NULL;
+}
+
 struct isl_map *isl_map_fix_si(struct isl_map *map,
 		enum isl_dim_type type, unsigned pos, int value)
 {
@@ -5990,19 +6062,33 @@ __isl_give isl_set *isl_set_partial_lexmax(
 			dom, empty);
 }
 
+/* Compute the lexicographic minimum (or maximum if "max" is set)
+ * of "bmap" over its domain.
+ *
+ * Since we are not interested in the part of the domain space where
+ * there is no solution, we initialize the domain to those constraints
+ * of "bmap" that only involve the parameters and the input dimensions.
+ * This relieves the parametric programming engine from detecting those
+ * inequalities and transferring them to the context.  More importantly,
+ * it ensures that those inequalities are transferred first and not
+ * intermixed with inequalities that actually split the domain.
+ */
 __isl_give isl_map *isl_basic_map_lexopt(__isl_take isl_basic_map *bmap, int max)
 {
-	struct isl_basic_set *dom = NULL;
-	isl_space *dom_dim;
+	int n_div;
+	int n_out;
+	isl_basic_map *copy;
+	isl_basic_set *dom;
 
-	if (!bmap)
-		goto error;
-	dom_dim = isl_space_domain(isl_space_copy(bmap->dim));
-	dom = isl_basic_set_universe(dom_dim);
+	n_div = isl_basic_map_dim(bmap, isl_dim_div);
+	n_out = isl_basic_map_dim(bmap, isl_dim_out);
+	copy = isl_basic_map_copy(bmap);
+	copy = isl_basic_map_drop_constraints_involving_dims(copy,
+							isl_dim_div, 0, n_div);
+	copy = isl_basic_map_drop_constraints_involving_dims(copy,
+							isl_dim_out, 0, n_out);
+	dom = isl_basic_map_domain(copy);
 	return isl_basic_map_partial_lexopt(bmap, dom, NULL, max);
-error:
-	isl_basic_map_free(bmap);
-	return NULL;
 }
 
 __isl_give isl_map *isl_basic_map_lexmin(__isl_take isl_basic_map *bmap)
@@ -6306,6 +6392,72 @@ error:
 	return NULL;
 }
 
+/* Given a basic set "bset" that only involves parameters and existentially
+ * quantified variables, return the index of the first equality
+ * that only involves parameters.  If there is no such equality then
+ * return bset->n_eq.
+ *
+ * This function assumes that isl_basic_set_gauss has been called on "bset".
+ */
+static int first_parameter_equality(__isl_keep isl_basic_set *bset)
+{
+	int i, j;
+	unsigned nparam, n_div;
+
+	if (!bset)
+		return -1;
+
+	nparam = isl_basic_set_dim(bset, isl_dim_param);
+	n_div = isl_basic_set_dim(bset, isl_dim_div);
+
+	for (i = 0, j = n_div - 1; i < bset->n_eq && j >= 0; --j) {
+		if (!isl_int_is_zero(bset->eq[i][1 + nparam + j]))
+			++i;
+	}
+
+	return i;
+}
+
+/* Compute an explicit representation for the existentially quantified
+ * variables in "bset" by computing the "minimal value" of the set
+ * variables.  Since there are no set variables, the computation of
+ * the minimal value essentially computes an explicit representation
+ * of the non-empty part(s) of "bset".
+ *
+ * The input only involves parameters and existentially quantified variables.
+ * All equalities among parameters have been removed.
+ *
+ * Since the existentially quantified variables in the result are in general
+ * going to be different from those in the input, we first replace
+ * them by the minimal number of variables based on their equalities.
+ * This should simplify the parametric integer programming.
+ */
+static __isl_give isl_set *base_compute_divs(__isl_take isl_basic_set *bset)
+{
+	isl_morph *morph1, *morph2;
+	isl_set *set;
+	unsigned n;
+
+	if (!bset)
+		return NULL;
+	if (bset->n_eq == 0)
+		return isl_basic_set_lexmin(bset);
+
+	morph1 = isl_basic_set_parameter_compression(bset);
+	bset = isl_morph_basic_set(isl_morph_copy(morph1), bset);
+	bset = isl_basic_set_lift(bset);
+	morph2 = isl_basic_set_variable_compression(bset, isl_dim_set);
+	bset = isl_morph_basic_set(morph2, bset);
+	n = isl_basic_set_dim(bset, isl_dim_set);
+	bset = isl_basic_set_project_out(bset, isl_dim_set, 0, n);
+
+	set = isl_basic_set_lexmin(bset);
+
+	set = isl_morph_set(isl_morph_inverse(morph1), set);
+
+	return set;
+}
+
 /* Project the given basic set onto its parameter domain, possibly introducing
  * new, explicit, existential variables in the constraints.
  * The input has parameters and (possibly implicit) existential variables.
@@ -6317,21 +6469,27 @@ error:
  * among the parameters by performing a variable compression on
  * the parameters.  Afterward, an inverse transformation is performed
  * and the equalities among the parameters are inserted back in.
+ *
+ * The variable compression on the parameters may uncover additional
+ * equalities that were only implicit before.  We therefore check
+ * if there are any new parameter equalities in the result and
+ * if so recurse.  The removal of parameter equalities is required
+ * for the parameter compression performed by base_compute_divs.
  */
 static struct isl_set *parameter_compute_divs(struct isl_basic_set *bset)
 {
-	int i, j;
+	int i;
 	struct isl_mat *eq;
 	struct isl_mat *T, *T2;
 	struct isl_set *set;
-	unsigned nparam, n_div;
+	unsigned nparam;
 
 	bset = isl_basic_set_cow(bset);
 	if (!bset)
 		return NULL;
 
 	if (bset->n_eq == 0)
-		return isl_basic_set_lexmin(bset);
+		return base_compute_divs(bset);
 
 	bset = isl_basic_set_gauss(bset, NULL);
 	if (!bset)
@@ -6339,16 +6497,11 @@ static struct isl_set *parameter_compute_divs(struct isl_basic_set *bset)
 	if (isl_basic_set_plain_is_empty(bset))
 		return isl_set_from_basic_set(bset);
 
-	nparam = isl_basic_set_dim(bset, isl_dim_param);
-	n_div = isl_basic_set_dim(bset, isl_dim_div);
-
-	for (i = 0, j = n_div - 1; i < bset->n_eq && j >= 0; --j) {
-		if (!isl_int_is_zero(bset->eq[i][1 + nparam + j]))
-			++i;
-	}
+	i = first_parameter_equality(bset);
 	if (i == bset->n_eq)
-		return isl_basic_set_lexmin(bset);
+		return base_compute_divs(bset);
 
+	nparam = isl_basic_set_dim(bset, isl_dim_param);
 	eq = isl_mat_sub_alloc6(bset->ctx, bset->eq, i, bset->n_eq - i,
 		0, 1 + nparam);
 	eq = isl_mat_cow(eq);
@@ -6362,47 +6515,174 @@ static struct isl_set *parameter_compute_divs(struct isl_basic_set *bset)
 	}
 	bset = basic_set_parameter_preimage(bset, T);
 
-	set = isl_basic_set_lexmin(bset);
+	i = first_parameter_equality(bset);
+	if (!bset)
+		set = NULL;
+	else if (i == bset->n_eq)
+		set = base_compute_divs(bset);
+	else
+		set = parameter_compute_divs(bset);
 	set = set_parameter_preimage(set, T2);
 	set = set_append_equalities(set, eq);
 	return set;
 }
 
-/* Compute an explicit representation for all the existentially
- * quantified variables.
- * The input and output dimensions are first turned into parameters.
- * compute_divs then returns a map with the same parameters and
+/* Insert the divs from "ls" before those of "bmap".
+ *
+ * The number of columns is not changed, which means that the last
+ * dimensions of "bmap" are being reintepreted as the divs from "ls".
+ * The caller is responsible for removing the same number of dimensions
+ * from the space of "bmap".
+ */
+static __isl_give isl_basic_map *insert_divs_from_local_space(
+	__isl_take isl_basic_map *bmap, __isl_keep isl_local_space *ls)
+{
+	int i;
+	int n_div;
+	int old_n_div;
+
+	n_div = isl_local_space_dim(ls, isl_dim_div);
+	if (n_div == 0)
+		return bmap;
+
+	old_n_div = bmap->n_div;
+	bmap = insert_div_rows(bmap, n_div);
+	if (!bmap)
+		return NULL;
+
+	for (i = 0; i < n_div; ++i) {
+		isl_seq_cpy(bmap->div[i], ls->div->row[i], ls->div->n_col);
+		isl_seq_clr(bmap->div[i] + ls->div->n_col, old_n_div);
+	}
+
+	return bmap;
+}
+
+/* Replace the space of "bmap" by the space and divs of "ls".
+ *
+ * If "ls" has any divs, then we simplify the result since we may
+ * have discovered some additional equalities that could simplify
+ * the div expressions.
+ */
+static __isl_give isl_basic_map *basic_replace_space_by_local_space(
+	__isl_take isl_basic_map *bmap, __isl_take isl_local_space *ls)
+{
+	int n_div;
+
+	bmap = isl_basic_map_cow(bmap);
+	if (!bmap || !ls)
+		goto error;
+
+	n_div = isl_local_space_dim(ls, isl_dim_div);
+	bmap = insert_divs_from_local_space(bmap, ls);
+	if (!bmap)
+		goto error;
+
+	isl_space_free(bmap->dim);
+	bmap->dim = isl_local_space_get_space(ls);
+	if (!bmap->dim)
+		goto error;
+
+	isl_local_space_free(ls);
+	if (n_div > 0)
+		bmap = isl_basic_map_simplify(bmap);
+	bmap = isl_basic_map_finalize(bmap);
+	return bmap;
+error:
+	isl_basic_map_free(bmap);
+	isl_local_space_free(ls);
+	return NULL;
+}
+
+/* Replace the space of "map" by the space and divs of "ls".
+ */
+static __isl_give isl_map *replace_space_by_local_space(__isl_take isl_map *map,
+	__isl_take isl_local_space *ls)
+{
+	int i;
+
+	map = isl_map_cow(map);
+	if (!map || !ls)
+		goto error;
+
+	for (i = 0; i < map->n; ++i) {
+		map->p[i] = basic_replace_space_by_local_space(map->p[i],
+						    isl_local_space_copy(ls));
+		if (!map->p[i])
+			goto error;
+	}
+	isl_space_free(map->dim);
+	map->dim = isl_local_space_get_space(ls);
+	if (!map->dim)
+		goto error;
+
+	isl_local_space_free(ls);
+	return map;
+error:
+	isl_local_space_free(ls);
+	isl_map_free(map);
+	return NULL;
+}
+
+/* Compute an explicit representation for the existentially
+ * quantified variables for which do not know any explicit representation yet.
+ *
+ * We first sort the existentially quantified variables so that the
+ * existentially quantified variables for which we already have an explicit
+ * representation are placed before those for which we do not.
+ * The input dimensions, the output dimensions and the existentially
+ * quantified variables for which we already have an explicit
+ * representation are then turned into parameters.
+ * compute_divs returns a map with the same parameters and
  * no input or output dimensions and the dimension specification
- * is reset to that of the input.
+ * is reset to that of the input, including the existentially quantified
+ * variables for which we already had an explicit representation.
  */
 static struct isl_map *compute_divs(struct isl_basic_map *bmap)
 {
 	struct isl_basic_set *bset;
 	struct isl_set *set;
 	struct isl_map *map;
-	isl_space *dim, *orig_dim = NULL;
+	isl_space *dim;
+	isl_local_space *ls;
 	unsigned	 nparam;
 	unsigned	 n_in;
 	unsigned	 n_out;
+	unsigned n_known;
+	int i;
 
+	bmap = isl_basic_map_sort_divs(bmap);
 	bmap = isl_basic_map_cow(bmap);
 	if (!bmap)
 		return NULL;
 
+	for (n_known = 0; n_known < bmap->n_div; ++n_known)
+		if (isl_int_is_zero(bmap->div[n_known][0]))
+			break;
+
 	nparam = isl_basic_map_dim(bmap, isl_dim_param);
 	n_in = isl_basic_map_dim(bmap, isl_dim_in);
 	n_out = isl_basic_map_dim(bmap, isl_dim_out);
-	dim = isl_space_set_alloc(bmap->ctx, nparam + n_in + n_out, 0);
+	dim = isl_space_set_alloc(bmap->ctx,
+				    nparam + n_in + n_out + n_known, 0);
 	if (!dim)
 		goto error;
 
-	orig_dim = bmap->dim;
-	bmap->dim = dim;
+	ls = isl_basic_map_get_local_space(bmap);
+	ls = isl_local_space_drop_dims(ls, isl_dim_div,
+					n_known, bmap->n_div - n_known);
+	if (n_known > 0) {
+		for (i = n_known; i < bmap->n_div; ++i)
+			swap_div(bmap, i - n_known, i);
+		bmap->n_div -= n_known;
+		bmap->extra -= n_known;
+	}
+	bmap = isl_basic_map_reset_space(bmap, dim);
 	bset = (struct isl_basic_set *)bmap;
 
 	set = parameter_compute_divs(bset);
 	map = (struct isl_map *)set;
-	map = isl_map_reset_space(map, orig_dim);
+	map = replace_space_by_local_space(map, ls);
 
 	return map;
 error:
@@ -10243,7 +10523,8 @@ __isl_give isl_basic_map *isl_basic_map_from_constraint_matrices(
 	isl_mat_free(eq);
 	isl_mat_free(ineq);
 
-	return bmap;
+	bmap = isl_basic_map_simplify(bmap);
+	return isl_basic_map_finalize(bmap);
 error:
 	isl_space_free(dim);
 	isl_mat_free(eq);