+/*
+ * Copyright 2008-2009 Katholieke Universiteit Leuven
+ *
+ * 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
+ */
+
#include "isl_map_private.h"
-#include "isl_seq.h"
+#include <isl/seq.h>
#include "isl_tab.h"
#include "isl_sample.h"
+#include <isl_mat_private.h>
/*
* The implementation of parametric integer linear programming in this file
/* 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 index and non-negativity */
- int (*add_div)(struct isl_context *context, struct isl_vec *div,
- int *nonneg);
+ /* add div "div" to context and return non-negativity */
+ int (*add_div)(struct isl_context *context, struct isl_vec *div);
int (*detect_equalities)(struct isl_context *context,
struct isl_tab *tab);
/* return row index of "best" split */
isl_seq_clr(mat->row[1 + row], mat->n_col);
if (!tab->var[i].is_row) {
- /* no unbounded */
- isl_assert(mat->ctx, !tab->M, goto error2);
+ if (tab->M)
+ isl_die(mat->ctx, isl_error_invalid,
+ "unbounded optimum", goto error2);
continue;
}
r = tab->var[i].index;
- /* no unbounded */
- if (tab->M)
- isl_assert(mat->ctx, isl_int_eq(tab->mat->row[r][2],
- tab->mat->row[r][0]),
- goto error2);
+ if (tab->M &&
+ isl_int_ne(tab->mat->row[r][2], tab->mat->row[r][0]))
+ isl_die(mat->ctx, isl_error_invalid,
+ "unbounded optimum", goto error2);
isl_int_gcd(m, mat->row[0][0], tab->mat->row[r][0]);
isl_int_divexact(m, tab->mat->row[r][0], m);
scale_rows(mat, m, 1 + row);
error:
isl_basic_set_free(bset);
isl_mat_free(mat);
- sol_free(sol);
+ sol->error = 1;
}
struct isl_sol_map {
static void sol_map_free(struct isl_sol_map *sol_map)
{
+ if (!sol_map)
+ return;
if (sol_map->sol.context)
sol_map->sol.context->op->free(sol_map->sol.context);
isl_map_free(sol_map->map);
sol->empty = isl_set_grow(sol->empty, 1);
bset = isl_basic_set_simplify(bset);
bset = isl_basic_set_finalize(bset);
- sol->empty = isl_set_add(sol->empty, isl_basic_set_copy(bset));
+ sol->empty = isl_set_add_basic_set(sol->empty, isl_basic_set_copy(bset));
if (!sol->empty)
goto error;
isl_basic_set_free(bset);
sol_map_add_empty((struct isl_sol_map *)sol, bset);
}
+/* Add bset to sol's empty, but only if we are actually collecting
+ * the empty set.
+ */
+static void sol_map_add_empty_if_needed(struct isl_sol_map *sol,
+ struct isl_basic_set *bset)
+{
+ if (sol->empty)
+ sol_map_add_empty(sol, bset);
+ else
+ isl_basic_set_free(bset);
+}
+
/* Given a basic map "dom" that represents the context and an affine
* matrix "M" that maps the dimensions of the context to the
* output variables, construct a basic map with the same parameters
bmap = isl_basic_map_simplify(bmap);
bmap = isl_basic_map_finalize(bmap);
sol->map = isl_map_grow(sol->map, 1);
- sol->map = isl_map_add(sol->map, bmap);
+ sol->map = isl_map_add_basic_map(sol->map, bmap);
if (!sol->map)
goto error;
isl_basic_set_free(dom);
for (row = tab->n_redundant; row < tab->n_row; ++row) {
if (!isl_tab_var_from_row(tab, row)->is_nonneg)
continue;
- if (isl_int_is_neg(tab->mat->row[row][2]))
- return row;
+ if (!isl_int_is_neg(tab->mat->row[row][2]))
+ continue;
+ if (tab->row_sign)
+ tab->row_sign[row] = isl_tab_row_neg;
+ return row;
}
for (row = tab->n_redundant; row < tab->n_row; ++row) {
if (!isl_tab_var_from_row(tab, row)->is_nonneg)
if (isl_tab_kill_col(tab, i) < 0)
goto error;
tab->n_eq++;
-
- tab = restore_lexmin(tab);
}
return tab;
#define I_PAR 1 << 1
#define I_VAR 1 << 2
-/* Check for first (non-parameter) variable that is non-integer and
- * therefore requires a cut.
+/* Check for next (non-parameter) variable after "var" (first if var == -1)
+ * that is non-integer and therefore requires a cut and return
+ * the index of the variable.
* For parametric tableaus, there are three parts in a row,
* the constant, the coefficients of the parameters and the rest.
* For each part, we check whether the coefficients in that part
* current sample value is integral and no cut is required
* (irrespective of whether the variable part is integral).
*/
-static int first_non_integer(struct isl_tab *tab, int *f)
+static int next_non_integer_var(struct isl_tab *tab, int var, int *f)
{
- int i;
+ var = var < 0 ? tab->n_param : var + 1;
- for (i = tab->n_param; i < tab->n_var - tab->n_div; ++i) {
+ for (; var < tab->n_var - tab->n_div; ++var) {
int flags = 0;
int row;
- if (!tab->var[i].is_row)
+ if (!tab->var[var].is_row)
continue;
- row = tab->var[i].index;
+ row = tab->var[var].index;
if (integer_constant(tab, row))
ISL_FL_SET(flags, I_CST);
if (integer_parameter(tab, row))
if (integer_variable(tab, row))
ISL_FL_SET(flags, I_VAR);
*f = flags;
- return row;
+ return var;
}
return -1;
}
+/* Check for first (non-parameter) variable that is non-integer and
+ * therefore requires a cut and return the corresponding row.
+ * For parametric tableaus, there are three parts in a row,
+ * the constant, the coefficients of the parameters and the rest.
+ * For each part, we check whether the coefficients in that part
+ * are all integral and if so, set the corresponding flag in *f.
+ * If the constant and the parameter part are integral, then the
+ * current sample value is integral and no cut is required
+ * (irrespective of whether the variable part is integral).
+ */
+static int first_non_integer_row(struct isl_tab *tab, int *f)
+{
+ int var = next_non_integer_var(tab, -1, f);
+
+ return var < 0 ? -1 : tab->var[var].index;
+}
+
/* Add a (non-parametric) cut to cut away the non-integral sample
* value of the given row.
*
* sample point is obtained or until the tableau is determined
* to be integer infeasible.
* As long as there is any non-integer value in the sample point,
- * we add an appropriate cut, if possible and resolve the violated
- * cut constraint using restore_lexmin.
+ * we add appropriate cuts, if possible, for each of these
+ * non-integer values and then resolve the violated
+ * cut constraints using restore_lexmin.
* If one of the corresponding rows is equal to an integral
* combination of variables/constraints plus a non-integral constant,
- * then there is no way to obtain an integer point an we return
+ * then there is no way to obtain an integer point and we return
* a tableau that is marked empty.
*/
static struct isl_tab *cut_to_integer_lexmin(struct isl_tab *tab)
{
+ int var;
int row;
int flags;
if (tab->empty)
return tab;
- while ((row = first_non_integer(tab, &flags)) != -1) {
- if (ISL_FL_ISSET(flags, I_VAR)) {
- if (isl_tab_mark_empty(tab) < 0)
+ while ((var = next_non_integer_var(tab, -1, &flags)) != -1) {
+ do {
+ if (ISL_FL_ISSET(flags, I_VAR)) {
+ if (isl_tab_mark_empty(tab) < 0)
+ goto error;
+ return tab;
+ }
+ row = tab->var[var].index;
+ row = add_cut(tab, row);
+ if (row < 0)
goto error;
- return tab;
- }
- row = add_cut(tab, row);
- if (row < 0)
- goto error;
+ } while ((var = next_non_integer_var(tab, var, &flags)) != -1);
tab = restore_lexmin(tab);
if (!tab || tab->empty)
break;
return i < tab->n_sample;
}
-/* For a div d = floor(f/m), add the constraints
- *
- * f - m d >= 0
- * -(f-(m-1)) + m d >= 0
- *
- * Note that the second constraint is the negation of
- *
- * f - m d >= m
- */
-static void add_div_constraints(struct isl_context *context, unsigned div)
-{
- unsigned total;
- unsigned div_pos;
- struct isl_vec *ineq;
- struct isl_basic_set *bset;
-
- bset = context->op->peek_basic_set(context);
- if (!bset)
- goto error;
-
- total = isl_basic_set_total_dim(bset);
- div_pos = 1 + total - bset->n_div + div;
-
- ineq = ineq_for_div(bset, div);
- if (!ineq)
- goto error;
-
- context->op->add_ineq(context, ineq->el, 0, 0);
-
- isl_seq_neg(ineq->el, bset->div[div] + 1, 1 + total);
- isl_int_set(ineq->el[div_pos], bset->div[div][0]);
- isl_int_add(ineq->el[0], ineq->el[0], ineq->el[div_pos]);
- isl_int_sub_ui(ineq->el[0], ineq->el[0], 1);
-
- context->op->add_ineq(context, ineq->el, 0, 0);
-
- isl_vec_free(ineq);
-
- return;
-error:
- context->op->invalidate(context);
-}
-
/* Add a div specifed by "div" to the tableau "tab" and return
- * the index of the new div. *nonneg is set to 1 if the div
- * is obviously non-negative.
+ * 1 if the div is obviously non-negative.
*/
static int context_tab_add_div(struct isl_tab *tab, struct isl_vec *div,
- int *nonneg)
+ int (*add_ineq)(void *user, isl_int *), void *user)
{
int i;
int r;
- int k;
struct isl_mat *samples;
+ int nonneg;
- for (i = 0; i < tab->n_var; ++i) {
- if (isl_int_is_zero(div->el[2 + i]))
- continue;
- if (!tab->var[i].is_nonneg)
- break;
- }
- *nonneg = i == tab->n_var;
-
- if (isl_tab_extend_cons(tab, 3) < 0)
- return -1;
- if (isl_tab_extend_vars(tab, 1) < 0)
- return -1;
- r = isl_tab_allocate_var(tab);
+ r = isl_tab_add_div(tab, div, add_ineq, user);
if (r < 0)
return -1;
- if (*nonneg)
- tab->var[r].is_nonneg = 1;
+ nonneg = tab->var[r].is_nonneg;
tab->var[r].frozen = 1;
samples = isl_mat_extend(tab->samples,
samples->row[i][samples->n_col - 1], div->el[0]);
}
- tab->bmap = isl_basic_map_extend_dim(tab->bmap,
- isl_basic_map_get_dim(tab->bmap), 1, 0, 2);
- k = isl_basic_map_alloc_div(tab->bmap);
- if (k < 0)
- return -1;
- isl_seq_cpy(tab->bmap->div[k], div->el, div->size);
- if (isl_tab_push(tab, isl_tab_undo_bmap_div) < 0)
- return -1;
-
- return k;
+ return nonneg;
}
/* Add a div specified by "div" to both the main tableau and
struct isl_vec *div)
{
int r;
- int k;
int nonneg;
- k = context->op->add_div(context, div, &nonneg);
- if (k < 0)
+ if ((nonneg = context->op->add_div(context, div)) < 0)
goto error;
- add_div_constraints(context, k);
if (!context->op->is_ok(context))
goto error;
for (i = 0; i < tab->bmap->n_div; ++i) {
if (isl_int_ne(tab->bmap->div[i][0], denom))
continue;
- if (!isl_seq_eq(tab->bmap->div[i] + 1, div, total))
+ if (!isl_seq_eq(tab->bmap->div[i] + 1, div, 1 + total))
continue;
return i;
}
if (!tab || tab->empty)
return tab;
}
+ if (bmap->n_eq)
+ tab = restore_lexmin(tab);
for (i = 0; i < bmap->n_ineq; ++i) {
if (max)
isl_seq_neg(bmap->ineq[i] + 1 + tab->n_param,
clex->tab = NULL;
}
+static int context_lex_add_ineq_wrap(void *user, isl_int *ineq)
+{
+ struct isl_context *context = (struct isl_context *)user;
+ context_lex_add_ineq(context, ineq, 0, 0);
+ return context->op->is_ok(context) ? 0 : -1;
+}
+
/* Check which signs can be obtained by "ineq" on all the currently
* active sample values. See row_sign for more information.
*/
int i;
int sgn;
isl_int tmp;
- int res = isl_tab_row_unknown;
+ enum isl_tab_row_sign res = isl_tab_row_unknown;
- isl_assert(tab->mat->ctx, tab->samples, return 0);
- isl_assert(tab->mat->ctx, tab->samples->n_col == 1 + tab->n_var, return 0);
+ isl_assert(tab->mat->ctx, tab->samples, return isl_tab_row_unknown);
+ isl_assert(tab->mat->ctx, tab->samples->n_col == 1 + tab->n_var,
+ return isl_tab_row_unknown);
isl_int_init(tmp);
for (i = tab->n_outside; i < tab->n_sample; ++i) {
return get_div(tab, context, div);
}
-static int context_lex_add_div(struct isl_context *context, struct isl_vec *div,
- int *nonneg)
+static int context_lex_add_div(struct isl_context *context, struct isl_vec *div)
{
struct isl_context_lex *clex = (struct isl_context_lex *)context;
- return context_tab_add_div(clex->tab, div, nonneg);
+ return context_tab_add_div(clex->tab, div,
+ context_lex_add_ineq_wrap, context);
}
static int context_lex_detect_equalities(struct isl_context *context,
return -1;
r = best_split(tab, clex->tab);
- if (isl_tab_rollback(clex->tab, snap) < 0)
+ if (r >= 0 && isl_tab_rollback(clex->tab, snap) < 0)
return -1;
return r;
struct isl_context_lex *clex = (struct isl_context_lex *)context;
struct isl_tab_undo *snap;
+ if (!tab)
+ return NULL;
+
snap = isl_tab_snap(clex->tab);
if (isl_tab_push_basis(clex->tab) < 0)
goto error;
struct isl_context *context, struct isl_tab *tab)
{
struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
+ if (!tab)
+ return NULL;
return tab_detect_nonnegative_parameters(tab, cgbr->tab);
}
if (!cgbr->cone) {
bset = isl_tab_peek_bset(cgbr->tab);
- cgbr->cone = isl_tab_from_recession_cone(bset);
+ cgbr->cone = isl_tab_from_recession_cone(bset, 0);
if (!cgbr->cone)
return NULL;
if (isl_tab_track_bset(cgbr->cone, isl_basic_set_dup(bset)) < 0)
return NULL;
}
- cgbr->cone = isl_tab_detect_implicit_equalities(cgbr->cone);
- if (!cgbr->cone)
+ if (isl_tab_detect_implicit_equalities(cgbr->cone) < 0)
return NULL;
if (cgbr->cone->n_dead == cgbr->cone->n_col) {
if (cgbr->tab->basis->n_col != 1 + cgbr->tab->n_var) {
isl_mat_free(cgbr->tab->basis);
cgbr->tab->basis = NULL;
- } else {
- cgbr->tab->n_zero = 0;
- cgbr->tab->n_unbounded = 0;
}
+ cgbr->tab->n_zero = 0;
+ cgbr->tab->n_unbounded = 0;
}
snap = isl_tab_snap(cgbr->tab);
if (isl_tab_extend_cons(tab, 2) < 0)
goto error;
- tab = isl_tab_add_eq(tab, eq);
+ if (isl_tab_add_eq(tab, eq) < 0)
+ goto error;
return tab;
error:
if (cgbr->cone && cgbr->cone->n_col != cgbr->cone->n_dead) {
if (isl_tab_extend_cons(cgbr->cone, 2) < 0)
goto error;
- cgbr->cone = isl_tab_add_eq(cgbr->cone, eq);
+ if (isl_tab_add_eq(cgbr->cone, eq) < 0)
+ goto error;
}
if (check) {
cgbr->tab = NULL;
}
+static int context_gbr_add_ineq_wrap(void *user, isl_int *ineq)
+{
+ struct isl_context *context = (struct isl_context *)user;
+ context_gbr_add_ineq(context, ineq, 0, 0);
+ return context->op->is_ok(context) ? 0 : -1;
+}
+
static enum isl_tab_row_sign context_gbr_ineq_sign(struct isl_context *context,
isl_int *ineq, int strict)
{
if (!cgbr->cone) {
struct isl_basic_set *bset = isl_tab_peek_bset(cgbr->tab);
- cgbr->cone = isl_tab_from_recession_cone(bset);
+ cgbr->cone = isl_tab_from_recession_cone(bset, 0);
if (!cgbr->cone)
goto error;
if (isl_tab_track_bset(cgbr->cone, isl_basic_set_dup(bset)) < 0)
goto error;
}
- cgbr->cone = isl_tab_detect_implicit_equalities(cgbr->cone);
+ if (isl_tab_detect_implicit_equalities(cgbr->cone) < 0)
+ goto error;
n_ineq = cgbr->tab->bmap->n_ineq;
cgbr->tab = isl_tab_detect_equalities(cgbr->tab, cgbr->cone);
return get_div(tab, context, div);
}
-static int context_gbr_add_div(struct isl_context *context, struct isl_vec *div,
- int *nonneg)
+static int context_gbr_add_div(struct isl_context *context, struct isl_vec *div)
{
struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
if (cgbr->cone) {
if (isl_tab_push(cgbr->cone, isl_tab_undo_bmap_div) < 0)
return -1;
}
- return context_tab_add_div(cgbr->tab, div, nonneg);
+ return context_tab_add_div(cgbr->tab, div,
+ context_gbr_add_ineq_wrap, context);
}
static int context_gbr_best_split(struct isl_context *context,
snap = isl_tab_snap(cgbr->tab);
r = best_split(tab, cgbr->tab);
- if (isl_tab_rollback(cgbr->tab, snap) < 0)
+ if (r >= 0 && isl_tab_rollback(cgbr->tab, snap) < 0)
return -1;
return r;
static struct isl_sol_map *sol_map_init(struct isl_basic_map *bmap,
struct isl_basic_set *dom, int track_empty, int max)
{
- struct isl_sol_map *sol_map;
+ struct isl_sol_map *sol_map = NULL;
+
+ if (!bmap)
+ goto error;
- sol_map = isl_calloc_type(bset->ctx, struct isl_sol_map);
+ sol_map = isl_calloc_type(bmap->ctx, struct isl_sol_map);
if (!sol_map)
goto error;
struct isl_sol *sol, int row)
{
struct isl_vec *ineq = NULL;
- int res = isl_tab_row_unknown;
+ enum isl_tab_row_sign res = isl_tab_row_unknown;
int critical;
int strict;
int row2;
return res;
error:
isl_vec_free(ineq);
- return 0;
+ return isl_tab_row_unknown;
}
static void find_solutions(struct isl_sol *sol, struct isl_tab *tab);
find_solutions(sol, tab);
- sol->context->op->restore(sol->context, saved);
+ if (!sol->error)
+ sol->context->op->restore(sol->context, saved);
return;
error:
sol->error = 1;
int empty;
void *saved;
- if (!sol->context)
+ if (!sol->context || sol->error)
goto error;
saved = sol->context->op->save(sol->context);
for (; tab && !tab->empty; tab = restore_lexmin(tab)) {
int flags;
int row;
- int sgn;
+ enum isl_tab_row_sign sgn;
int split = -1;
int n_split = 0;
row = split;
isl_seq_neg(ineq->el, ineq->el, ineq->size);
isl_int_sub_ui(ineq->el[0], ineq->el[0], 1);
- context->op->add_ineq(context, ineq->el, 0, 1);
+ if (!sol->error)
+ context->op->add_ineq(context, ineq->el, 0, 1);
isl_vec_free(ineq);
if (sol->error)
goto error;
}
if (tab->rational)
break;
- row = first_non_integer(tab, &flags);
+ row = first_non_integer_row(tab, &flags);
if (row < 0)
break;
if (ISL_FL_ISSET(flags, I_PAR)) {
if (d < 0)
goto error;
ineq = ineq_for_div(context->op->peek_basic_set(context), d);
+ if (!ineq)
+ goto error;
sol_inc_level(sol);
no_sol_in_strict(sol, tab, ineq);
isl_seq_neg(ineq->el, ineq->el, ineq->size);
if (sol->error || !context->op->is_ok(context))
goto error;
tab = set_row_cst_to_div(tab, row, d);
+ if (context->op->is_empty(context))
+ break;
} else
row = add_parametric_cut(tab, row, context);
if (row < 0)
return;
error:
isl_tab_free(tab);
- sol_free(sol);
+ sol->error = 1;
}
/* Compute the lexicographic minimum of the set represented by the main
{
int row;
+ if (!tab)
+ goto error;
+
sol->level = 0;
for (row = tab->n_redundant; row < tab->n_row; ++row) {
+ tab->n_param - (tab->n_var - tab->n_div);
eq = isl_vec_alloc(tab->mat->ctx, 1+tab->n_param+tab->n_div);
+ if (!eq)
+ goto error;
get_row_parameter_line(tab, row, eq->el);
isl_int_neg(eq->el[1 + p], tab->mat->row[row][0]);
eq = isl_vec_normalize(eq);
return;
error:
isl_tab_free(tab);
- sol_free(sol);
+ sol->error = 1;
}
static void sol_map_find_solutions(struct isl_sol_map *sol_map,
if (empty)
*empty = NULL;
if (!bmap || !dom)
- goto error;
+ goto error2;
isl_assert(bmap->ctx,
isl_basic_map_compatible_domain(bmap, dom), goto error);
if (isl_basic_set_fast_is_empty(context->op->peek_basic_set(context)))
/* nothing */;
else if (isl_basic_map_fast_is_empty(bmap))
- sol_map_add_empty(sol_map,
- isl_basic_set_dup(context->op->peek_basic_set(context)));
+ sol_map_add_empty_if_needed(sol_map,
+ isl_basic_set_copy(context->op->peek_basic_set(context)));
else {
tab = tab_for_lexmin(bmap,
context->op->peek_basic_set(context), 1, max);
sol_free(&sol_map->sol);
isl_basic_map_free(bmap);
return result;
+error2:
+ isl_basic_set_free(dom);
error:
sol_free(&sol_map->sol);
isl_basic_map_free(bmap);
struct isl_dim *dom_dim;
struct isl_basic_set *dom = NULL;
- sol_for = isl_calloc_type(bset->ctx, struct isl_sol_for);
+ sol_for = isl_calloc_type(bmap->ctx, struct isl_sol_for);
if (!sol_for)
goto error;
projects / platform / upstream / isl.git / blobdiff