+/*
+ * 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_tab.h"
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);
#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;
}
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 (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)
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);
projects / platform / upstream / isl.git / blobdiff