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.
* 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);
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
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
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;
/* 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 */
/* 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 {
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;
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;
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;
}
* 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)
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;
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)
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;
}
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 = {
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,
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);
}
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 = {
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,
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.
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
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));
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
* 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)
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);
projects / platform / upstream / llvm.git / commitdiff