[polly] r276138 - Update isl to isl-0.17.1-191-g540b2fd

Tobias Grosser via llvm-commits llvm-commits at lists.llvm.org
Wed Jul 20 09:53:07 PDT 2016


Author: grosser
Date: Wed Jul 20 11:53:07 2016
New Revision: 276138

URL: http://llvm.org/viewvc/llvm-project?rev=276138&view=rev
Log:
Update isl to isl-0.17.1-191-g540b2fd

This update resolves a bug in computing lexicographic minima/maxima.

Modified:
    polly/trunk/lib/External/isl/GIT_HEAD_ID
    polly/trunk/lib/External/isl/doc/manual.pdf
    polly/trunk/lib/External/isl/isl_map.c
    polly/trunk/lib/External/isl/isl_map_private.h
    polly/trunk/lib/External/isl/isl_map_simplify.c
    polly/trunk/lib/External/isl/isl_map_subtract.c
    polly/trunk/lib/External/isl/isl_tab.c
    polly/trunk/lib/External/isl/isl_tab.h
    polly/trunk/lib/External/isl/isl_tab_pip.c
    polly/trunk/lib/External/isl/isl_test.c

Modified: polly/trunk/lib/External/isl/GIT_HEAD_ID
URL: http://llvm.org/viewvc/llvm-project/polly/trunk/lib/External/isl/GIT_HEAD_ID?rev=276138&r1=276137&r2=276138&view=diff
==============================================================================
--- polly/trunk/lib/External/isl/GIT_HEAD_ID (original)
+++ polly/trunk/lib/External/isl/GIT_HEAD_ID Wed Jul 20 11:53:07 2016
@@ -1 +1 @@
-isl-0.17.1-171-g233f589
+isl-0.17.1-191-g540b2fd

Modified: polly/trunk/lib/External/isl/doc/manual.pdf
URL: http://llvm.org/viewvc/llvm-project/polly/trunk/lib/External/isl/doc/manual.pdf?rev=276138&r1=276137&r2=276138&view=diff
==============================================================================
Binary files polly/trunk/lib/External/isl/doc/manual.pdf (original) and polly/trunk/lib/External/isl/doc/manual.pdf Wed Jul 20 11:53:07 2016 differ

Modified: polly/trunk/lib/External/isl/isl_map.c
URL: http://llvm.org/viewvc/llvm-project/polly/trunk/lib/External/isl/isl_map.c?rev=276138&r1=276137&r2=276138&view=diff
==============================================================================
--- polly/trunk/lib/External/isl/isl_map.c (original)
+++ polly/trunk/lib/External/isl/isl_map.c Wed Jul 20 11:53:07 2016
@@ -1425,6 +1425,43 @@ int isl_basic_set_alloc_div(struct isl_b
 	return isl_basic_map_alloc_div((struct isl_basic_map *)bset);
 }
 
+/* Insert an extra integer division, prescribed by "div", to "bmap"
+ * at (integer division) position "pos".
+ *
+ * The integer division is first added at the end and then moved
+ * into the right position.
+ */
+__isl_give isl_basic_map *isl_basic_map_insert_div(
+	__isl_take isl_basic_map *bmap, int pos, __isl_keep isl_vec *div)
+{
+	int i, k, n_div;
+
+	bmap = isl_basic_map_cow(bmap);
+	if (!bmap || !div)
+		return isl_basic_map_free(bmap);
+
+	if (div->size != 1 + 1 + isl_basic_map_dim(bmap, isl_dim_all))
+		isl_die(isl_basic_map_get_ctx(bmap), isl_error_invalid,
+			"unexpected size", return isl_basic_map_free(bmap));
+	n_div = isl_basic_map_dim(bmap, isl_dim_div);
+	if (pos < 0 || pos > n_div)
+		isl_die(isl_basic_map_get_ctx(bmap), isl_error_invalid,
+			"invalid position", return isl_basic_map_free(bmap));
+
+	bmap = isl_basic_map_extend_space(bmap,
+					isl_basic_map_get_space(bmap), 1, 0, 2);
+	k = isl_basic_map_alloc_div(bmap);
+	if (k < 0)
+		return isl_basic_map_free(bmap);
+	isl_seq_cpy(bmap->div[k], div->el, div->size);
+	isl_int_set_si(bmap->div[k][div->size], 0);
+
+	for (i = k; i > pos; --i)
+		isl_basic_map_swap_div(bmap, i, i - 1);
+
+	return bmap;
+}
+
 int isl_basic_map_free_div(struct isl_basic_map *bmap, unsigned n)
 {
 	if (!bmap)
@@ -6918,6 +6955,17 @@ int isl_basic_map_first_unknown_div(__is
 	return bmap->n_div;
 }
 
+/* Return the position of the first local variable that does not
+ * have an explicit representation.
+ * Return the total number of local variables if they all have
+ * an explicit representation.
+ * Return -1 on error.
+ */
+int isl_basic_set_first_unknown_div(__isl_keep isl_basic_set *bset)
+{
+	return isl_basic_map_first_unknown_div(bset);
+}
+
 /* Does "bmap" have an explicit representation for all local variables?
  */
 isl_bool isl_basic_map_divs_known(__isl_keep isl_basic_map *bmap)

Modified: polly/trunk/lib/External/isl/isl_map_private.h
URL: http://llvm.org/viewvc/llvm-project/polly/trunk/lib/External/isl/isl_map_private.h?rev=276138&r1=276137&r2=276138&view=diff
==============================================================================
--- polly/trunk/lib/External/isl/isl_map_private.h (original)
+++ polly/trunk/lib/External/isl/isl_map_private.h Wed Jul 20 11:53:07 2016
@@ -231,9 +231,13 @@ int isl_basic_set_alloc_inequality(struc
 int isl_basic_map_alloc_inequality(struct isl_basic_map *bmap);
 int isl_basic_map_free_inequality(struct isl_basic_map *bmap, unsigned n);
 int isl_basic_map_alloc_div(struct isl_basic_map *bmap);
+__isl_give isl_basic_map *isl_basic_map_insert_div(
+	__isl_take isl_basic_map *bmap, int pos, __isl_keep isl_vec *div);
 int isl_basic_set_alloc_div(struct isl_basic_set *bset);
 int isl_basic_map_free_div(struct isl_basic_map *bmap, unsigned n);
 int isl_basic_set_free_div(struct isl_basic_set *bset, unsigned n);
+__isl_give isl_basic_map *isl_basic_map_drop_div(
+	__isl_take isl_basic_map *bmap, unsigned div);
 void isl_basic_map_inequality_to_equality(
 		struct isl_basic_map *bmap, unsigned pos);
 int isl_basic_map_drop_equality(struct isl_basic_map *bmap, unsigned pos);
@@ -427,6 +431,7 @@ isl_bool isl_basic_map_div_is_marked_unk
 	int div);
 isl_bool isl_basic_set_div_is_known(__isl_keep isl_basic_set *bset, int div);
 isl_bool isl_basic_map_div_is_known(__isl_keep isl_basic_map *bmap, int div);
+int isl_basic_set_first_unknown_div(__isl_keep isl_basic_set *bset);
 int isl_basic_map_first_unknown_div(__isl_keep isl_basic_map *bmap);
 isl_bool isl_basic_map_divs_known(__isl_keep isl_basic_map *bmap);
 isl_bool isl_map_divs_known(__isl_keep isl_map *map);

Modified: polly/trunk/lib/External/isl/isl_map_simplify.c
URL: http://llvm.org/viewvc/llvm-project/polly/trunk/lib/External/isl/isl_map_simplify.c?rev=276138&r1=276137&r2=276138&view=diff
==============================================================================
--- polly/trunk/lib/External/isl/isl_map_simplify.c (original)
+++ polly/trunk/lib/External/isl/isl_map_simplify.c Wed Jul 20 11:53:07 2016
@@ -269,8 +269,8 @@ struct isl_map *isl_map_drop_inputs(
 /*
  * We don't cow, as the div is assumed to be redundant.
  */
-static struct isl_basic_map *isl_basic_map_drop_div(
-		struct isl_basic_map *bmap, unsigned div)
+__isl_give isl_basic_map *isl_basic_map_drop_div(
+	__isl_take isl_basic_map *bmap, unsigned div)
 {
 	int i;
 	unsigned pos;

Modified: polly/trunk/lib/External/isl/isl_map_subtract.c
URL: http://llvm.org/viewvc/llvm-project/polly/trunk/lib/External/isl/isl_map_subtract.c?rev=276138&r1=276137&r2=276138&view=diff
==============================================================================
--- polly/trunk/lib/External/isl/isl_map_subtract.c (original)
+++ polly/trunk/lib/External/isl/isl_map_subtract.c Wed Jul 20 11:53:07 2016
@@ -193,7 +193,7 @@ static int tab_add_divs(struct isl_tab *
 		(*div_map)[i] = j;
 		if (j == tab->bmap->n_div) {
 			vec->size = 2 + dim + tab->bmap->n_div;
-			if (isl_tab_add_div(tab, vec, NULL, NULL) < 0)
+			if (isl_tab_add_div(tab, vec) < 0)
 				goto error;
 		}
 	}

Modified: polly/trunk/lib/External/isl/isl_tab.c
URL: http://llvm.org/viewvc/llvm-project/polly/trunk/lib/External/isl/isl_tab.c?rev=276138&r1=276137&r2=276138&view=diff
==============================================================================
--- polly/trunk/lib/External/isl/isl_tab.c (original)
+++ polly/trunk/lib/External/isl/isl_tab.c Wed Jul 20 11:53:07 2016
@@ -2287,8 +2287,10 @@ static int div_is_nonneg(struct isl_tab
 	return 1;
 }
 
-/* Add an extra div, prescribed by "div" to the tableau and
+/* Insert an extra div, prescribed by "div", to the tableau and
  * the associated bmap (which is assumed to be non-NULL).
+ * The extra integer division is inserted at (tableau) position "pos".
+ * Return "pos" or -1 if an error occurred.
  *
  * If add_ineq is not NULL, then this function is used instead
  * of isl_tab_add_ineq to add the div constraints.
@@ -2296,17 +2298,26 @@ static int div_is_nonneg(struct isl_tab
  * wants to perform some extra processing when an inequality
  * is added to the tableau.
  */
-int isl_tab_add_div(struct isl_tab *tab, __isl_keep isl_vec *div,
+int isl_tab_insert_div(struct isl_tab *tab, int pos, __isl_keep isl_vec *div,
 	int (*add_ineq)(void *user, isl_int *), void *user)
 {
 	int r;
-	int k;
 	int nonneg;
+	int n_div, o_div;
 
 	if (!tab || !div)
 		return -1;
 
+	if (div->size != 1 + 1 + tab->n_var)
+		isl_die(isl_tab_get_ctx(tab), isl_error_invalid,
+			"unexpected size", return -1);
+
 	isl_assert(tab->mat->ctx, tab->bmap, return -1);
+	n_div = isl_basic_map_dim(tab->bmap, isl_dim_div);
+	o_div = tab->n_var - n_div;
+	if (pos < o_div || pos > tab->n_var)
+		isl_die(isl_tab_get_ctx(tab), isl_error_invalid,
+			"invalid position", return -1);
 
 	nonneg = div_is_nonneg(tab, div);
 
@@ -2314,28 +2325,35 @@ int isl_tab_add_div(struct isl_tab *tab,
 		return -1;
 	if (isl_tab_extend_vars(tab, 1) < 0)
 		return -1;
-	r = isl_tab_allocate_var(tab);
+	r = isl_tab_insert_var(tab, pos);
 	if (r < 0)
 		return -1;
 
 	if (nonneg)
 		tab->var[r].is_nonneg = 1;
 
-	tab->bmap = isl_basic_map_extend_space(tab->bmap,
-		isl_basic_map_get_space(tab->bmap), 1, 0, 2);
-	k = isl_basic_map_alloc_div(tab->bmap);
-	if (k < 0)
+	tab->bmap = isl_basic_map_insert_div(tab->bmap, pos - o_div, div);
+	if (!tab->bmap)
 		return -1;
-	isl_seq_cpy(tab->bmap->div[k], div->el, div->size);
-	if (isl_tab_push(tab, isl_tab_undo_bmap_div) < 0)
+	if (isl_tab_push_var(tab, isl_tab_undo_bmap_div, &tab->var[r]) < 0)
 		return -1;
 
-	if (add_div_constraints(tab, k, add_ineq, user) < 0)
+	if (add_div_constraints(tab, pos - o_div, add_ineq, user) < 0)
 		return -1;
 
 	return r;
 }
 
+/* Add an extra div, prescribed by "div", to the tableau and
+ * the associated bmap (which is assumed to be non-NULL).
+ */
+int isl_tab_add_div(struct isl_tab *tab, __isl_keep isl_vec *div)
+{
+	if (!tab)
+		return -1;
+	return isl_tab_insert_div(tab, tab->n_var, div, NULL, NULL);
+}
+
 /* If "track" is set, then we want to keep track of all constraints in tab
  * in its bmap field.  This field is initialized from a copy of "bmap",
  * so we need to make sure that all constraints in "bmap" also appear
@@ -3408,6 +3426,25 @@ static int perform_undo_var(struct isl_t
 	return 0;
 }
 
+/* Undo the addition of an integer division to the basic map representation
+ * of "tab" in position "pos".
+ */
+static isl_stat drop_bmap_div(struct isl_tab *tab, int pos)
+{
+	int off;
+
+	off = tab->n_var - isl_basic_map_dim(tab->bmap, isl_dim_div);
+	if (isl_basic_map_drop_div(tab->bmap, pos - off) < 0)
+		return isl_stat_error;
+	if (tab->samples) {
+		tab->samples = isl_mat_drop_cols(tab->samples, 1 + pos, 1);
+		if (!tab->samples)
+			return isl_stat_error;
+	}
+
+	return isl_stat_ok;
+}
+
 /* Restore the tableau to the state where the basic variables
  * are those in "col_var".
  * We first construct a list of variables that are currently in
@@ -3509,11 +3546,7 @@ static int perform_undo(struct isl_tab *
 	case isl_tab_undo_bmap_ineq:
 		return isl_basic_map_free_inequality(tab->bmap, 1);
 	case isl_tab_undo_bmap_div:
-		if (isl_basic_map_free_div(tab->bmap, 1) < 0)
-			return -1;
-		if (tab->samples)
-			tab->samples->n_col--;
-		break;
+		return drop_bmap_div(tab, undo->u.var_index);
 	case isl_tab_undo_saved_basis:
 		if (restore_basis(tab, undo->u.col_var) < 0)
 			return -1;

Modified: polly/trunk/lib/External/isl/isl_tab.h
URL: http://llvm.org/viewvc/llvm-project/polly/trunk/lib/External/isl/isl_tab.h?rev=276138&r1=276137&r2=276138&view=diff
==============================================================================
--- polly/trunk/lib/External/isl/isl_tab.h (original)
+++ polly/trunk/lib/External/isl/isl_tab.h Wed Jul 20 11:53:07 2016
@@ -320,8 +320,9 @@ struct isl_tab *isl_tab_detect_equalitie
 int isl_tab_push_callback(struct isl_tab *tab,
 	struct isl_tab_callback *callback) WARN_UNUSED;
 
-int isl_tab_add_div(struct isl_tab *tab, __isl_keep isl_vec *div,
+int isl_tab_insert_div(struct isl_tab *tab, int pos, __isl_keep isl_vec *div,
 	int (*add_ineq)(void *user, isl_int *), void *user);
+int isl_tab_add_div(struct isl_tab *tab, __isl_keep isl_vec *div);
 
 int isl_tab_shift_var(struct isl_tab *tab, int pos, isl_int shift) WARN_UNUSED;
 

Modified: polly/trunk/lib/External/isl/isl_tab_pip.c
URL: http://llvm.org/viewvc/llvm-project/polly/trunk/lib/External/isl/isl_tab_pip.c?rev=276138&r1=276137&r2=276138&view=diff
==============================================================================
--- polly/trunk/lib/External/isl/isl_tab_pip.c (original)
+++ polly/trunk/lib/External/isl/isl_tab_pip.c Wed Jul 20 11:53:07 2016
@@ -91,8 +91,9 @@ struct isl_context_op {
 	/* return index of a div that corresponds to "div" */
 	int (*get_div)(struct isl_context *context, struct isl_tab *tab,
 			struct isl_vec *div);
-	/* add div "div" to context and return non-negativity */
-	int (*add_div)(struct isl_context *context, struct isl_vec *div);
+	/* insert div "div" to context at "pos" and return non-negativity */
+	isl_bool (*insert_div)(struct isl_context *context, int pos,
+		__isl_keep isl_vec *div);
 	int (*detect_equalities)(struct isl_context *context,
 			struct isl_tab *tab);
 	/* return row index of "best" split */
@@ -110,11 +111,17 @@ struct isl_context_op {
 	/* invalidate context */
 	void (*invalidate)(struct isl_context *context);
 	/* free context */
-	void (*free)(struct isl_context *context);
+	__isl_null struct isl_context *(*free)(struct isl_context *context);
 };
 
+/* Shared parts of context representation.
+ *
+ * "n_unknown" is the number of final unknown integer divisions
+ * in the input domain.
+ */
 struct isl_context {
 	struct isl_context_op *op;
+	int n_unknown;
 };
 
 struct isl_context_lex {
@@ -1860,10 +1867,11 @@ static int tab_has_valid_sample(struct i
 	return i < tab->n_sample;
 }
 
-/* Add a div specified by "div" to the tableau "tab" and return
- * 1 if the div is obviously non-negative.
+/* Insert a div specified by "div" to the tableau "tab" at position "pos" and
+ * return isl_bool_true if the div is obviously non-negative.
  */
-static int context_tab_add_div(struct isl_tab *tab, struct isl_vec *div,
+static isl_bool context_tab_insert_div(struct isl_tab *tab, int pos,
+	__isl_keep isl_vec *div,
 	int (*add_ineq)(void *user, isl_int *), void *user)
 {
 	int i;
@@ -1871,9 +1879,9 @@ static int context_tab_add_div(struct is
 	struct isl_mat *samples;
 	int nonneg;
 
-	r = isl_tab_add_div(tab, div, add_ineq, user);
+	r = isl_tab_insert_div(tab, pos, div, add_ineq, user);
 	if (r < 0)
-		return -1;
+		return isl_bool_error;
 	nonneg = tab->var[r].is_nonneg;
 	tab->var[r].frozen = 1;
 
@@ -1881,13 +1889,17 @@ static int context_tab_add_div(struct is
 			tab->n_sample, 1 + tab->n_var);
 	tab->samples = samples;
 	if (!samples)
-		return -1;
+		return isl_bool_error;
 	for (i = tab->n_outside; i < samples->n_row; ++i) {
 		isl_seq_inner_product(div->el + 1, samples->row[i],
 			div->size - 1, &samples->row[i][samples->n_col - 1]);
 		isl_int_fdiv_q(samples->row[i][samples->n_col - 1],
 			       samples->row[i][samples->n_col - 1], div->el[0]);
 	}
+	tab->samples = isl_mat_move_cols(tab->samples, 1 + pos,
+					1 + tab->n_var - 1, 1);
+	if (!tab->samples)
+		return isl_bool_error;
 
 	return nonneg;
 }
@@ -1897,22 +1909,34 @@ static int context_tab_add_div(struct is
  * need to add an extra div.  In the context tableau, we also
  * need to express the meaning of the div.
  * Return the index of the div or -1 if anything went wrong.
+ *
+ * The new integer division is added before any unknown integer
+ * divisions in the context to ensure that it does not get
+ * equated to some linear combination involving unknown integer
+ * divisions.
  */
 static int add_div(struct isl_tab *tab, struct isl_context *context,
-	struct isl_vec *div)
+	__isl_keep isl_vec *div)
 {
 	int r;
-	int nonneg;
+	int pos;
+	isl_bool nonneg;
+	struct isl_tab *context_tab = context->op->peek_tab(context);
+
+	if (!tab || !context_tab)
+		goto error;
 
-	if ((nonneg = context->op->add_div(context, div)) < 0)
+	pos = context_tab->n_var - context->n_unknown;
+	if ((nonneg = context->op->insert_div(context, pos, div)) < 0)
 		goto error;
 
 	if (!context->op->is_ok(context))
 		goto error;
 
+	pos = tab->n_var - context->n_unknown;
 	if (isl_tab_extend_vars(tab, 1) < 0)
 		goto error;
-	r = isl_tab_allocate_var(tab);
+	r = isl_tab_insert_var(tab, pos);
 	if (r < 0)
 		goto error;
 	if (nonneg)
@@ -1920,7 +1944,7 @@ static int add_div(struct isl_tab *tab,
 	tab->var[r].frozen = 1;
 	tab->n_div++;
 
-	return tab->n_div - 1;
+	return tab->n_div - 1 - context->n_unknown;
 error:
 	context->op->invalidate(context);
 	return -1;
@@ -2002,7 +2026,7 @@ static int add_parametric_cut(struct isl
 	if (!div)
 		return -1;
 
-	n = tab->n_div;
+	n = tab->n_div - context->n_unknown;
 	d = context->op->get_div(context, tab, div);
 	isl_vec_free(div);
 	if (d < 0)
@@ -2395,24 +2419,25 @@ static int context_lex_get_div(struct is
 	return get_div(tab, context, div);
 }
 
-/* Add a div specified by "div" to the context tableau and return
- * 1 if the div is obviously non-negative.
- * context_tab_add_div will always return 1, because all variables
+/* Insert a div specified by "div" to the context tableau at position "pos" and
+ * return isl_bool_true if the div is obviously non-negative.
+ * context_tab_add_div will always return isl_bool_true, because all variables
  * in a isl_context_lex tableau are non-negative.
  * However, if we are using a big parameter in the context, then this only
  * reflects the non-negativity of the variable used to _encode_ the
  * div, i.e., div' = M + div, so we can't draw any conclusions.
  */
-static int context_lex_add_div(struct isl_context *context, struct isl_vec *div)
+static isl_bool context_lex_insert_div(struct isl_context *context, int pos,
+	__isl_keep isl_vec *div)
 {
 	struct isl_context_lex *clex = (struct isl_context_lex *)context;
-	int nonneg;
-	nonneg = context_tab_add_div(clex->tab, div,
+	isl_bool nonneg;
+	nonneg = context_tab_insert_div(clex->tab, pos, div,
 					context_lex_add_ineq_wrap, context);
 	if (nonneg < 0)
-		return -1;
+		return isl_bool_error;
 	if (clex->tab->M)
-		return 0;
+		return isl_bool_false;
 	return nonneg;
 }
 
@@ -2571,11 +2596,14 @@ static void context_lex_invalidate(struc
 	clex->tab = NULL;
 }
 
-static void context_lex_free(struct isl_context *context)
+static __isl_null struct isl_context *context_lex_free(
+	struct isl_context *context)
 {
 	struct isl_context_lex *clex = (struct isl_context_lex *)context;
 	isl_tab_free(clex->tab);
 	free(clex);
+
+	return NULL;
 }
 
 struct isl_context_op isl_context_lex_op = {
@@ -2587,7 +2615,7 @@ struct isl_context_op isl_context_lex_op
 	context_lex_ineq_sign,
 	context_lex_test_ineq,
 	context_lex_get_div,
-	context_lex_add_div,
+	context_lex_insert_div,
 	context_lex_detect_equalities,
 	context_lex_best_split,
 	context_lex_is_empty,
@@ -3199,29 +3227,32 @@ static int context_gbr_get_div(struct is
 	return get_div(tab, context, div);
 }
 
-static int context_gbr_add_div(struct isl_context *context, struct isl_vec *div)
+static isl_bool context_gbr_insert_div(struct isl_context *context, int pos,
+	__isl_keep isl_vec *div)
 {
 	struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
 	if (cgbr->cone) {
-		int k;
+		int r, n_div, o_div;
+
+		n_div = isl_basic_map_dim(cgbr->cone->bmap, isl_dim_div);
+		o_div = cgbr->cone->n_var - n_div;
 
 		if (isl_tab_extend_cons(cgbr->cone, 3) < 0)
-			return -1;
+			return isl_bool_error;
 		if (isl_tab_extend_vars(cgbr->cone, 1) < 0)
-			return -1;
-		if (isl_tab_allocate_var(cgbr->cone) <0)
-			return -1;
-
-		cgbr->cone->bmap = isl_basic_map_extend_space(cgbr->cone->bmap,
-			isl_basic_map_get_space(cgbr->cone->bmap), 1, 0, 2);
-		k = isl_basic_map_alloc_div(cgbr->cone->bmap);
-		if (k < 0)
-			return -1;
-		isl_seq_cpy(cgbr->cone->bmap->div[k], div->el, div->size);
-		if (isl_tab_push(cgbr->cone, isl_tab_undo_bmap_div) < 0)
-			return -1;
+			return isl_bool_error;
+		if ((r = isl_tab_insert_var(cgbr->cone, pos)) <0)
+			return isl_bool_error;
+
+		cgbr->cone->bmap = isl_basic_map_insert_div(cgbr->cone->bmap,
+						    r - o_div, div);
+		if (!cgbr->cone->bmap)
+			return isl_bool_error;
+		if (isl_tab_push_var(cgbr->cone, isl_tab_undo_bmap_div,
+				    &cgbr->cone->var[r]) < 0)
+			return isl_bool_error;
 	}
-	return context_tab_add_div(cgbr->tab, div,
+	return context_tab_insert_div(cgbr->tab, pos, div,
 					context_gbr_add_ineq_wrap, context);
 }
 
@@ -3340,13 +3371,16 @@ static void context_gbr_invalidate(struc
 	cgbr->tab = NULL;
 }
 
-static void context_gbr_free(struct isl_context *context)
+static __isl_null struct isl_context *context_gbr_free(
+	struct isl_context *context)
 {
 	struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
 	isl_tab_free(cgbr->tab);
 	isl_tab_free(cgbr->shifted);
 	isl_tab_free(cgbr->cone);
 	free(cgbr);
+
+	return NULL;
 }
 
 struct isl_context_op isl_context_gbr_op = {
@@ -3358,7 +3392,7 @@ struct isl_context_op isl_context_gbr_op
 	context_gbr_ineq_sign,
 	context_gbr_test_ineq,
 	context_gbr_get_div,
-	context_gbr_add_div,
+	context_gbr_insert_div,
 	context_gbr_detect_equalities,
 	context_gbr_best_split,
 	context_gbr_is_empty,
@@ -3397,15 +3431,34 @@ error:
 	return NULL;
 }
 
+/* Allocate a context corresponding to "dom".
+ * The representation specific fields are initialized by
+ * isl_context_lex_alloc or isl_context_gbr_alloc.
+ * The shared "n_unknown" field is initialized to the number
+ * of final unknown integer divisions in "dom".
+ */
 static struct isl_context *isl_context_alloc(__isl_keep isl_basic_set *dom)
 {
+	struct isl_context *context;
+	int first;
+
 	if (!dom)
 		return NULL;
 
 	if (dom->ctx->opt->context == ISL_CONTEXT_LEXMIN)
-		return isl_context_lex_alloc(dom);
+		context = isl_context_lex_alloc(dom);
 	else
-		return isl_context_gbr_alloc(dom);
+		context = isl_context_gbr_alloc(dom);
+
+	if (!context)
+		return NULL;
+
+	first = isl_basic_set_first_unknown_div(dom);
+	if (first < 0)
+		return context->op->free(context);
+	context->n_unknown = isl_basic_set_dim(dom, isl_dim_div) - first;
+
+	return context;
 }
 
 /* Construct an isl_sol_map structure for accumulating the solution.
@@ -5302,110 +5355,6 @@ error:
 	sol->sol.error = 1;
 }
 
-/* Return the equality constraint in "bset" that defines existentially
- * quantified variable "pos" in terms of earlier dimensions.
- * The equality constraint is guaranteed to exist by the caller.
- * If "c" is not NULL, then it is the result of a previous call
- * to this function for the same variable, so simply return the input "c"
- * in that case.
- */
-static __isl_give isl_constraint *get_equality(__isl_keep isl_basic_set *bset,
-	int pos, __isl_take isl_constraint *c)
-{
-	int r;
-
-	if (c)
-		return c;
-	r = isl_basic_set_has_defining_equality(bset, isl_dim_div, pos, &c);
-	if (r < 0)
-		return NULL;
-	if (!r)
-		isl_die(isl_basic_set_get_ctx(bset), isl_error_internal,
-			"unexpected missing equality", return NULL);
-	return c;
-}
-
-/* Given a set "dom", of which only the first "n_known" existentially
- * quantified variables have a known explicit representation, and
- * a matrix "M", the rows of which are defined in terms of the dimensions
- * of "dom", eliminate all references to the existentially quantified
- * variables without a known explicit representation from "M"
- * by exploiting the equality constraints of "dom".
- *
- * In particular, for each of those existentially quantified variables,
- * if there are non-zero entries in the corresponding column of "M",
- * then look for an equality constraint of "dom" that defines that variable
- * in terms of earlier variables and use it to clear the entries.
- *
- * In particular, if the equality is of the form
- *
- *	f() + a alpha = 0
- *
- * while the matrix entry is b/d (with d the global denominator of "M"),
- * then first scale the matrix such that the entry becomes b'/d' with
- * b' a multiple of a.  Do this by multiplying the entire matrix
- * by abs(a/gcd(a,b)).  Then subtract the equality multiplied by b'/a
- * from the row of "M" to clear the entry.
- */
-static __isl_give isl_mat *eliminate_unknown_divs(__isl_take isl_mat *M,
-	__isl_keep isl_basic_set *dom, int n_known)
-{
-	int i, j, n_div, off;
-	isl_int t;
-	isl_constraint *c = NULL;
-
-	if (!M)
-		return NULL;
-
-	n_div = isl_basic_set_dim(dom, isl_dim_div);
-	off = M->n_col - n_div;
-
-	isl_int_init(t);
-	for (i = n_div - 1; i >= n_known; --i) {
-		for (j = 1; j < M->n_row; ++j) {
-			if (isl_int_is_zero(M->row[j][off + i]))
-				continue;
-			c = get_equality(dom, i, c);
-			if (!c)
-				goto error;
-			isl_int_gcd(t, M->row[j][off + i], c->v->el[off + i]);
-			isl_int_divexact(t, c->v->el[off + i], t);
-			isl_int_abs(t, t);
-			M = isl_mat_scale(M, t);
-			M = isl_mat_cow(M);
-			if (!M)
-				goto error;
-			isl_int_divexact(t,
-					M->row[j][off + i], c->v->el[off + i]);
-			isl_seq_submul(M->row[j], t, c->v->el, M->n_col);
-		}
-		c = isl_constraint_free(c);
-	}
-	isl_int_clear(t);
-
-	return M;
-error:
-	isl_int_clear(t);
-	isl_constraint_free(c);
-	isl_mat_free(M);
-	return NULL;
-}
-
-/* Return the index of the last known div of "bset" after "start" and
- * up to (but not including) "end".
- * Return "start" if there is no such known div.
- */
-static int last_known_div_after(__isl_keep isl_basic_set *bset,
-	int start, int end)
-{
-	for (end = end - 1; end > start; --end) {
-		if (isl_basic_set_div_is_known(bset, end))
-			return end;
-	}
-
-	return start;
-}
-
 /* Set the affine expressions in "ma" according to the rows in "M", which
  * are defined over the local space "ls".
  * The matrix "M" may have extra (zero) columns beyond the number
@@ -5418,6 +5367,9 @@ static __isl_give isl_multi_aff *set_fro
 	int i, dim;
 	isl_aff *aff;
 
+	if (!ma || !ls || !M)
+		goto error;
+
 	dim = isl_local_space_dim(ls, isl_dim_all);
 	for (i = 1; i < M->n_row; ++i) {
 		aff = isl_aff_alloc(isl_local_space_copy(ls));
@@ -5432,6 +5384,11 @@ static __isl_give isl_multi_aff *set_fro
 	isl_mat_free(M);
 
 	return ma;
+error:
+	isl_local_space_free(ls);
+	isl_mat_free(M);
+	isl_multi_aff_free(ma);
+	return NULL;
 }
 
 /* Given a basic map "dom" that represents the context and an affine
@@ -5443,21 +5400,13 @@ static __isl_give isl_multi_aff *set_fro
  * existentially quantified variables, in which case they also appear
  * in "dom".  These need to be removed before creating the affine
  * expression because an affine expression cannot be defined in terms
- * of existentially quantified variables without a known representation.
- * In particular, they are first moved to the end in both "dom" and "M" and
- * then ignored in "M".  In principle, the final columns of "M"
- * (i.e., those that will be ignored) should be zero at this stage
+ * Since newly added integer divisions are inserted before these
+ * existentially quantified variables, they are still in the final
+ * positions and the corresponding final columns "M" are zero
  * because align_context_divs adds the existentially quantified
- * variables of the context to the main tableau without any constraints.
- * The computed minimal value can therefore not depend on these variables.
- * However, additional integer divisions that get added for parametric cuts
- * get added to the end and they may happen to be equal to some affine
- * expression involving the original existentially quantified variables.
- * These equality constraints are then propagated to the main tableau
- * such that the computed minimum can in fact depend on those existentially
- * quantified variables.  This dependence can however be removed again
- * by exploiting the equality constraints in "dom".
- * eliminate_unknown_divs takes care of this.
+ * variables of the context to the main tableau without any constraints and
+ * any equality constraints that are added later on can only serve
+ * to eliminate these existentially quantified variables.
  */
 static void sol_pma_add(struct isl_sol_pma *sol,
 	__isl_take isl_basic_set *dom, __isl_take isl_mat *M)
@@ -5465,23 +5414,10 @@ static void sol_pma_add(struct isl_sol_p
 	isl_local_space *ls;
 	isl_multi_aff *maff;
 	isl_pw_multi_aff *pma;
-	int n_div, n_known, end, off;
+	int n_div, n_known;
 
 	n_div = isl_basic_set_dim(dom, isl_dim_div);
-	off = M->n_col - n_div;
-	end = n_div;
-	for (n_known = 0; n_known < end; ++n_known) {
-		if (isl_basic_set_div_is_known(dom, n_known))
-			continue;
-		end = last_known_div_after(dom, n_known, end);
-		if (end == n_known)
-			break;
-		isl_basic_set_swap_div(dom, n_known, end);
-		M = isl_mat_swap_cols(M, off + n_known, off + end);
-	}
-	dom = isl_basic_set_gauss(dom, NULL);
-	if (n_known < n_div)
-		M = eliminate_unknown_divs(M, dom, n_known);
+	n_known = n_div - sol->sol.context->n_unknown;
 
 	maff = isl_multi_aff_alloc(isl_pw_multi_aff_get_space(sol->pma));
 	ls = isl_basic_set_get_local_space(dom);

Modified: polly/trunk/lib/External/isl/isl_test.c
URL: http://llvm.org/viewvc/llvm-project/polly/trunk/lib/External/isl/isl_test.c?rev=276138&r1=276137&r2=276138&view=diff
==============================================================================
--- polly/trunk/lib/External/isl/isl_test.c (original)
+++ polly/trunk/lib/External/isl/isl_test.c Wed Jul 20 11:53:07 2016
@@ -2297,6 +2297,11 @@ struct {
 		"247j >= 62738 - i and 509j <= 129795 + i and "
 		"742j >= 188724 - i; "
 	    "[0, k, j] -> [1, 0, 248, 1] : k <= 255 and 248 <= j <= 254, k }" },
+	{ "{ [a] -> [b] : 0 <= b <= 255 and -509 + a <= 512b < a and "
+			"16*floor((8 + b)/16) <= 7 + b; "
+	    "[a] -> [1] }",
+	  "{ [a] -> [b = 1] : a >= 510 or a <= 0; "
+	    "[a] -> [b = 0] : 0 < a <= 509 }" },
 };
 
 static int test_lexmin(struct isl_ctx *ctx)




More information about the llvm-commits mailing list