* to M from the initial context tableau.
*/
+struct isl_context;
+struct isl_context_op {
+ /* detect nonnegative parameters in context and mark them in tab */
+ struct isl_tab *(*detect_nonnegative_parameters)(
+ struct isl_context *context, struct isl_tab *tab);
+ /* return temporary reference to basic set representation of context */
+ struct isl_basic_set *(*peek_basic_set)(struct isl_context *context);
+ /* return temporary reference to tableau representation of context */
+ struct isl_tab *(*peek_tab)(struct isl_context *context);
+ /* add equality; check is 1 if eq may not be valid;
+ * update is 1 if we may want to call ineq_sign on context later.
+ */
+ void (*add_eq)(struct isl_context *context, isl_int *eq,
+ int check, int update);
+ /* add inequality; check is 1 if ineq may not be valid;
+ * update is 1 if we may want to call ineq_sign on context later.
+ */
+ void (*add_ineq)(struct isl_context *context, isl_int *ineq,
+ int check, int update);
+ /* check sign of ineq based on previous information.
+ * strict is 1 if saturation should be treated as a positive sign.
+ */
+ enum isl_tab_row_sign (*ineq_sign)(struct isl_context *context,
+ isl_int *ineq, int strict);
+ /* check if inequality maintains feasibility */
+ int (*test_ineq)(struct isl_context *context, isl_int *ineq);
+ /* 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);
+ /* return row index of "best" split */
+ int (*best_split)(struct isl_context *context, struct isl_tab *tab);
+ /* check if context has already been determined to be empty */
+ int (*is_empty)(struct isl_context *context);
+ /* check if context is still usable */
+ int (*is_ok)(struct isl_context *context);
+ /* save a copy/snapshot of context */
+ void *(*save)(struct isl_context *context);
+ /* restore saved context */
+ void (*restore)(struct isl_context *context, void *);
+ /* invalidate context */
+ void (*invalidate)(struct isl_context *context);
+ /* free context */
+ void (*free)(struct isl_context *context);
+};
+
+struct isl_context {
+ struct isl_context_op *op;
+};
+
+struct isl_context_lex {
+ struct isl_context context;
+ struct isl_tab *tab;
+};
+
/* isl_sol is an interface for constructing a solution to
* a parametric integer linear programming problem.
* Every time the algorithm reaches a state where a solution
* the solution.
*/
struct isl_sol {
- struct isl_tab *context_tab;
+ struct isl_context *context;
struct isl_sol *(*add)(struct isl_sol *sol, struct isl_tab *tab);
void (*free)(struct isl_sol *sol);
};
static void sol_map_free(struct isl_sol_map *sol_map)
{
- isl_tab_free(sol_map->sol.context_tab);
+ if (sol_map->sol.context)
+ sol_map->sol.context->op->free(sol_map->sol.context);
isl_map_free(sol_map->map);
isl_set_free(sol_map->empty);
free(sol_map);
if (!sol->empty)
return sol;
sol->empty = isl_set_grow(sol->empty, 1);
- bset = isl_basic_set_copy(sol->sol.context_tab->bset);
+ bset = sol->sol.context->op->peek_basic_set(sol->sol.context);
+ bset = isl_basic_set_copy(bset);
bset = isl_basic_set_simplify(bset);
bset = isl_basic_set_finalize(bset);
sol->empty = isl_set_add(sol->empty, bset);
{
int i;
struct isl_basic_map *bmap = NULL;
- struct isl_tab *context_tab;
+ isl_basic_set *context_bset;
unsigned n_eq;
unsigned n_ineq;
unsigned nparam;
if (tab->empty)
return add_empty(sol);
- context_tab = sol->sol.context_tab;
+ context_bset = sol->sol.context->op->peek_basic_set(sol->sol.context);
off = 2 + tab->M;
n_out = isl_map_dim(sol->map, isl_dim_out);
- n_eq = context_tab->bset->n_eq + n_out;
- n_ineq = context_tab->bset->n_ineq;
+ n_eq = context_bset->n_eq + n_out;
+ n_ineq = context_bset->n_ineq;
nparam = tab->n_param;
total = isl_map_dim(sol->map, isl_dim_all);
bmap = isl_basic_map_alloc_dim(isl_map_get_dim(sol->map),
n_div = tab->n_div;
if (tab->rational)
ISL_F_SET(bmap, ISL_BASIC_MAP_RATIONAL);
- for (i = 0; i < context_tab->bset->n_div; ++i) {
+ for (i = 0; i < context_bset->n_div; ++i) {
int k = isl_basic_map_alloc_div(bmap);
if (k < 0)
goto error;
isl_seq_cpy(bmap->div[k],
- context_tab->bset->div[i], 1 + 1 + nparam);
+ context_bset->div[i], 1 + 1 + nparam);
isl_seq_clr(bmap->div[k] + 1 + 1 + nparam, total - nparam);
isl_seq_cpy(bmap->div[k] + 1 + 1 + total,
- context_tab->bset->div[i] + 1 + 1 + nparam, i);
+ context_bset->div[i] + 1 + 1 + nparam, i);
}
- for (i = 0; i < context_tab->bset->n_eq; ++i) {
+ for (i = 0; i < context_bset->n_eq; ++i) {
int k = isl_basic_map_alloc_equality(bmap);
if (k < 0)
goto error;
- isl_seq_cpy(bmap->eq[k], context_tab->bset->eq[i], 1 + nparam);
+ isl_seq_cpy(bmap->eq[k], context_bset->eq[i], 1 + nparam);
isl_seq_clr(bmap->eq[k] + 1 + nparam, total - nparam);
isl_seq_cpy(bmap->eq[k] + 1 + total,
- context_tab->bset->eq[i] + 1 + nparam, n_div);
+ context_bset->eq[i] + 1 + nparam, n_div);
}
- for (i = 0; i < context_tab->bset->n_ineq; ++i) {
+ for (i = 0; i < context_bset->n_ineq; ++i) {
int k = isl_basic_map_alloc_inequality(bmap);
if (k < 0)
goto error;
isl_seq_cpy(bmap->ineq[k],
- context_tab->bset->ineq[i], 1 + nparam);
+ context_bset->ineq[i], 1 + nparam);
isl_seq_clr(bmap->ineq[k] + 1 + nparam, total - nparam);
isl_seq_cpy(bmap->ineq[k] + 1 + total,
- context_tab->bset->ineq[i] + 1 + nparam, n_div);
+ context_bset->ineq[i] + 1 + nparam, n_div);
}
for (i = tab->n_param; i < total; ++i) {
int k = isl_basic_map_alloc_equality(bmap);
unsigned div_pos;
struct isl_vec *ineq;
+ if (!bset)
+ return NULL;
+
total = isl_basic_set_total_dim(bset);
div_pos = 1 + total - bset->n_div + div;
}
/* Check if the context tableau of sol has any integer points.
- * Returns -1 if an error occurred.
+ * Leave tab in empty state if no integer point can be found.
* If an integer point can be found and if moreover it is finite,
* then it is added to the list of sample values.
*
* This function is only called when none of the currently active sample
* values satisfies the most recently added constraint.
*/
-static int context_is_feasible(struct isl_sol *sol)
+static struct isl_tab *check_integer_feasible(struct isl_tab *tab)
{
struct isl_tab_undo *snap;
- struct isl_tab *tab;
int feasible;
- if (!sol || !sol->context_tab)
- return -1;
+ if (!tab)
+ return NULL;
- snap = isl_tab_snap(sol->context_tab);
- isl_tab_push_basis(sol->context_tab);
+ snap = isl_tab_snap(tab);
+ isl_tab_push_basis(tab);
- sol->context_tab = cut_to_integer_lexmin(sol->context_tab);
- if (!sol->context_tab)
+ tab = cut_to_integer_lexmin(tab);
+ if (!tab)
goto error;
- tab = sol->context_tab;
if (!tab->empty && sample_is_finite(tab)) {
struct isl_vec *sample;
tab = isl_tab_add_sample(tab, sample);
}
- feasible = !sol->context_tab->empty;
- if (isl_tab_rollback(sol->context_tab, snap) < 0)
+ if (!tab->empty && isl_tab_rollback(tab, snap) < 0)
goto error;
- return feasible;
+ return tab;
error:
- isl_tab_free(sol->context_tab);
- sol->context_tab = NULL;
- return -1;
+ isl_tab_free(tab);
+ return NULL;
}
-/* First check if any of the currently active sample values satisfies
+/* Check if any of the currently active sample values satisfies
* the inequality "ineq" (an equality if eq is set).
- * If not, continue with check_integer_feasible.
*/
-static int context_valid_sample_or_feasible(struct isl_sol *sol,
- isl_int *ineq, int eq)
+static int tab_has_valid_sample(struct isl_tab *tab, isl_int *ineq, int eq)
{
int i;
isl_int v;
- struct isl_tab *tab;
- if (!sol || !sol->context_tab)
+ if (!tab)
return -1;
- tab = sol->context_tab;
isl_assert(tab->mat->ctx, tab->bset, return -1);
isl_assert(tab->mat->ctx, tab->samples, return -1);
isl_assert(tab->mat->ctx, tab->samples->n_col == 1 + tab->n_var, return -1);
}
isl_int_clear(v);
- if (i < tab->n_sample)
- return 1;
-
- return context_is_feasible(sol);
+ return i < tab->n_sample;
}
/* For a div d = floor(f/m), add the constraints
*
* f - m d >= m
*/
-static struct isl_tab *add_div_constraints(struct isl_tab *tab, unsigned div)
+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;
- if (!tab)
- return NULL;
+ bset = context->op->peek_basic_set(context);
+ if (!bset)
+ goto error;
- total = isl_basic_set_total_dim(tab->bset);
- div_pos = 1 + total - tab->bset->n_div + div;
+ total = isl_basic_set_total_dim(bset);
+ div_pos = 1 + total - bset->n_div + div;
- ineq = ineq_for_div(tab->bset, div);
+ ineq = ineq_for_div(bset, div);
if (!ineq)
goto error;
- tab = add_lexmin_ineq(tab, ineq->el);
+ context->op->add_ineq(context, ineq->el, 0, 0);
- isl_seq_neg(ineq->el, tab->bset->div[div] + 1, 1 + total);
- isl_int_set(ineq->el[div_pos], tab->bset->div[div][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);
- tab = add_lexmin_ineq(tab, ineq->el);
+
+ context->op->add_ineq(context, ineq->el, 0, 0);
isl_vec_free(ineq);
- return tab;
+ return;
error:
- isl_tab_free(tab);
- return NULL;
+ context->op->invalidate(context);
}
-/* Add a div specified by "div" to both the main tableau and
- * the context tableau. In case of the main tableau, we only
- * 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.
+/* 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.
*/
-static int add_div(struct isl_tab *tab, struct isl_tab **context_tab,
- struct isl_vec *div)
+static int context_tab_add_div(struct isl_tab *tab, struct isl_vec *div,
+ int *nonneg)
{
int i;
int r;
int k;
- int nonneg;
struct isl_mat *samples;
- for (i = 0; i < (*context_tab)->n_var; ++i) {
+ for (i = 0; i < tab->n_var; ++i) {
if (isl_int_is_zero(div->el[2 + i]))
continue;
- if (!(*context_tab)->var[i].is_nonneg)
+ if (!tab->var[i].is_nonneg)
break;
}
- nonneg = i == (*context_tab)->n_var;
+ *nonneg = i == tab->n_var;
- if (isl_tab_extend_vars(*context_tab, 1) < 0)
- goto error;
- r = isl_tab_allocate_var(*context_tab);
+ 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);
if (r < 0)
- goto error;
- if (nonneg)
- (*context_tab)->var[r].is_nonneg = 1;
- (*context_tab)->var[r].frozen = 1;
+ return -1;
+ if (*nonneg)
+ tab->var[r].is_nonneg = 1;
+ tab->var[r].frozen = 1;
- samples = isl_mat_extend((*context_tab)->samples,
- (*context_tab)->n_sample, 1 + (*context_tab)->n_var);
- (*context_tab)->samples = samples;
+ samples = isl_mat_extend(tab->samples,
+ tab->n_sample, 1 + tab->n_var);
+ tab->samples = samples;
if (!samples)
- goto error;
- for (i = (*context_tab)->n_outside; i < samples->n_row; ++i) {
+ return -1;
+ 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]);
}
- (*context_tab)->bset = isl_basic_set_extend_dim((*context_tab)->bset,
- isl_basic_set_get_dim((*context_tab)->bset), 1, 0, 2);
- k = isl_basic_set_alloc_div((*context_tab)->bset);
+ tab->bset = isl_basic_set_extend_dim(tab->bset,
+ isl_basic_set_get_dim(tab->bset), 1, 0, 2);
+ k = isl_basic_set_alloc_div(tab->bset);
+ if (k < 0)
+ return -1;
+ isl_seq_cpy(tab->bset->div[k], div->el, div->size);
+ isl_tab_push(tab, isl_tab_undo_bset_div);
+
+ return k;
+}
+
+/* Add a div specified by "div" to both the main tableau and
+ * the context tableau. In case of the main tableau, we only
+ * 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.
+ */
+static int add_div(struct isl_tab *tab, struct isl_context *context,
+ struct isl_vec *div)
+{
+ int r;
+ int k;
+ int nonneg;
+
+ k = context->op->add_div(context, div, &nonneg);
if (k < 0)
goto error;
- isl_seq_cpy((*context_tab)->bset->div[k], div->el, div->size);
- isl_tab_push((*context_tab), isl_tab_undo_bset_div);
- *context_tab = add_div_constraints(*context_tab, k);
- if (!*context_tab)
+
+ add_div_constraints(context, k);
+ if (!context->op->is_ok(context))
goto error;
if (isl_tab_extend_vars(tab, 1) < 0)
return tab->n_div - 1;
error:
- isl_tab_free(*context_tab);
- *context_tab = NULL;
+ context->op->invalidate(context);
return -1;
}
/* Return the index of a div that corresponds to "div".
* We first check if we already have such a div and if not, we create one.
*/
-static int get_div(struct isl_tab *tab, struct isl_tab **context_tab,
+static int get_div(struct isl_tab *tab, struct isl_context *context,
struct isl_vec *div)
{
int d;
+ struct isl_tab *context_tab = context->op->peek_tab(context);
+
+ if (!context_tab)
+ return -1;
- d = find_div(*context_tab, div->el + 1, div->el[0]);
+ d = find_div(context_tab, div->el + 1, div->el[0]);
if (d != -1)
return d;
- return add_div(tab, context_tab, div);
+ return add_div(tab, context, div);
}
/* Add a parametric cut to cut away the non-integral sample value
* Return the row of the cut or -1.
*/
static int add_parametric_cut(struct isl_tab *tab, int row,
- struct isl_tab **context_tab)
+ struct isl_context *context)
{
struct isl_vec *div;
int d;
int col;
unsigned off = 2 + tab->M;
- if (!*context_tab)
- goto error;
-
- if (isl_tab_extend_cons(*context_tab, 3) < 0)
- goto error;
+ if (!context)
+ return -1;
div = get_row_parameter_div(tab, row);
if (!div)
return -1;
- d = get_div(tab, context_tab, div);
+ d = context->op->get_div(context, tab, div);
if (d < 0)
- goto error;
+ return -1;
if (isl_tab_extend_cons(tab, 1) < 0)
return -1;
isl_vec_free(div);
return tab->con[r].index;
-error:
- isl_tab_free(*context_tab);
- *context_tab = NULL;
- return -1;
}
/* Construct a tableau for bmap that can be used for computing
return NULL;
}
-static struct isl_tab *context_tab_for_lexmin(struct isl_basic_set *bset)
+/* Given a main tableau where more than one row requires a split,
+ * determine and return the "best" row to split on.
+ *
+ * Given two rows in the main tableau, if the inequality corresponding
+ * to the first row is redundant with respect to that of the second row
+ * in the current tableau, then it is better to split on the second row,
+ * since in the positive part, both row will be positive.
+ * (In the negative part a pivot will have to be performed and just about
+ * anything can happen to the sign of the other row.)
+ *
+ * As a simple heuristic, we therefore select the row that makes the most
+ * of the other rows redundant.
+ *
+ * Perhaps it would also be useful to look at the number of constraints
+ * that conflict with any given constraint.
+ */
+static int best_split(struct isl_tab *tab, struct isl_tab *context_tab)
{
- struct isl_tab *tab;
+ struct isl_tab_undo *snap;
+ int split;
+ int row;
+ int best = -1;
+ int best_r;
- bset = isl_basic_set_cow(bset);
- if (!bset)
+ if (isl_tab_extend_cons(context_tab, 2) < 0)
+ return -1;
+
+ snap = isl_tab_snap(context_tab);
+
+ for (split = tab->n_redundant; split < tab->n_row; ++split) {
+ struct isl_tab_undo *snap2;
+ struct isl_vec *ineq = NULL;
+ int r = 0;
+
+ if (!isl_tab_var_from_row(tab, split)->is_nonneg)
+ continue;
+ if (tab->row_sign[split] != isl_tab_row_any)
+ continue;
+
+ ineq = get_row_parameter_ineq(tab, split);
+ if (!ineq)
+ return -1;
+ context_tab = isl_tab_add_ineq(context_tab, ineq->el);
+ isl_vec_free(ineq);
+
+ snap2 = isl_tab_snap(context_tab);
+
+ for (row = tab->n_redundant; row < tab->n_row; ++row) {
+ struct isl_tab_var *var;
+
+ if (row == split)
+ continue;
+ if (!isl_tab_var_from_row(tab, row)->is_nonneg)
+ continue;
+ if (tab->row_sign[row] != isl_tab_row_any)
+ continue;
+
+ ineq = get_row_parameter_ineq(tab, row);
+ if (!ineq)
+ return -1;
+ context_tab = isl_tab_add_ineq(context_tab, ineq->el);
+ isl_vec_free(ineq);
+ var = &context_tab->con[context_tab->n_con - 1];
+ if (!context_tab->empty &&
+ !isl_tab_min_at_most_neg_one(context_tab, var))
+ r++;
+ if (isl_tab_rollback(context_tab, snap2) < 0)
+ return -1;
+ }
+ if (best == -1 || r > best_r) {
+ best = split;
+ best_r = r;
+ }
+ if (isl_tab_rollback(context_tab, snap) < 0)
+ return -1;
+ }
+
+ return best;
+}
+
+static struct isl_basic_set *context_lex_peek_basic_set(
+ struct isl_context *context)
+{
+ struct isl_context_lex *clex = (struct isl_context_lex *)context;
+ if (!clex->tab)
return NULL;
- tab = tab_for_lexmin((struct isl_basic_map *)bset, NULL, 1, 0);
- if (!tab)
+ return clex->tab->bset;
+}
+
+static struct isl_tab *context_lex_peek_tab(struct isl_context *context)
+{
+ struct isl_context_lex *clex = (struct isl_context_lex *)context;
+ return clex->tab;
+}
+
+static void context_lex_extend(struct isl_context *context, int n)
+{
+ struct isl_context_lex *clex = (struct isl_context_lex *)context;
+ if (!clex->tab)
+ return;
+ if (isl_tab_extend_cons(clex->tab, n) >= 0)
+ return;
+ isl_tab_free(clex->tab);
+ clex->tab = NULL;
+}
+
+static void context_lex_add_eq(struct isl_context *context, isl_int *eq,
+ int check, int update)
+{
+ struct isl_context_lex *clex = (struct isl_context_lex *)context;
+ if (isl_tab_extend_cons(clex->tab, 2) < 0)
goto error;
- tab->bset = bset;
- tab = isl_tab_init_samples(tab);
- return tab;
+ clex->tab = add_lexmin_eq(clex->tab, eq);
+ if (check) {
+ int v = tab_has_valid_sample(clex->tab, eq, 1);
+ if (v < 0)
+ goto error;
+ if (!v)
+ clex->tab = check_integer_feasible(clex->tab);
+ }
+ if (update)
+ clex->tab = check_samples(clex->tab, eq, 1);
+ return;
error:
- isl_basic_set_free(bset);
- return NULL;
+ isl_tab_free(clex->tab);
+ clex->tab = NULL;
}
-/* Construct an isl_sol_map structure for accumulating the solution.
- * If track_empty is set, then we also keep track of the parts
- * of the context where there is no solution.
- * If max is set, then we are solving a maximization, rather than
- * a minimization problem, which means that the variables in the
- * tableau have value "M - x" rather than "M + x".
+static void context_lex_add_ineq(struct isl_context *context, isl_int *ineq,
+ int check, int update)
+{
+ struct isl_context_lex *clex = (struct isl_context_lex *)context;
+ if (isl_tab_extend_cons(clex->tab, 1) < 0)
+ goto error;
+ clex->tab = add_lexmin_ineq(clex->tab, ineq);
+ if (check) {
+ int v = tab_has_valid_sample(clex->tab, ineq, 0);
+ if (v < 0)
+ goto error;
+ if (!v)
+ clex->tab = check_integer_feasible(clex->tab);
+ }
+ if (update)
+ clex->tab = check_samples(clex->tab, ineq, 0);
+ return;
+error:
+ isl_tab_free(clex->tab);
+ clex->tab = NULL;
+}
+
+/* Check which signs can be obtained by "ineq" on all the currently
+ * active sample values. See row_sign for more information.
*/
-static struct isl_sol_map *sol_map_init(struct isl_basic_map *bmap,
- struct isl_basic_set *dom, int track_empty, int max)
+static enum isl_tab_row_sign tab_ineq_sign(struct isl_tab *tab, isl_int *ineq,
+ int strict)
{
- struct isl_sol_map *sol_map;
- struct isl_tab *context_tab;
- int f;
+ int i;
+ int sgn;
+ isl_int tmp;
+ int res = isl_tab_row_unknown;
- sol_map = isl_calloc_type(bset->ctx, struct isl_sol_map);
- if (!sol_map)
- goto error;
+ isl_assert(tab->mat->ctx, tab->samples, return 0);
+ isl_assert(tab->mat->ctx, tab->samples->n_col == 1 + tab->n_var, return 0);
- sol_map->max = max;
- sol_map->sol.add = &sol_map_add_wrap;
- sol_map->sol.free = &sol_map_free_wrap;
- sol_map->map = isl_map_alloc_dim(isl_basic_map_get_dim(bmap), 1,
- ISL_MAP_DISJOINT);
- if (!sol_map->map)
- goto error;
+ isl_int_init(tmp);
+ for (i = tab->n_outside; i < tab->n_sample; ++i) {
+ isl_seq_inner_product(tab->samples->row[i], ineq,
+ 1 + tab->n_var, &tmp);
+ sgn = isl_int_sgn(tmp);
+ if (sgn > 0 || (sgn == 0 && strict)) {
+ if (res == isl_tab_row_unknown)
+ res = isl_tab_row_pos;
+ if (res == isl_tab_row_neg)
+ res = isl_tab_row_any;
+ }
+ if (sgn < 0) {
+ if (res == isl_tab_row_unknown)
+ res = isl_tab_row_neg;
+ if (res == isl_tab_row_pos)
+ res = isl_tab_row_any;
+ }
+ if (res == isl_tab_row_any)
+ break;
+ }
+ isl_int_clear(tmp);
- context_tab = context_tab_for_lexmin(isl_basic_set_copy(dom));
- context_tab = restore_lexmin(context_tab);
- sol_map->sol.context_tab = context_tab;
- f = context_is_feasible(&sol_map->sol);
- if (f < 0)
- goto error;
+ return res;
+}
- if (track_empty) {
- sol_map->empty = isl_set_alloc_dim(isl_basic_set_get_dim(dom),
- 1, ISL_SET_DISJOINT);
- if (!sol_map->empty)
- goto error;
+static enum isl_tab_row_sign context_lex_ineq_sign(struct isl_context *context,
+ isl_int *ineq, int strict)
+{
+ struct isl_context_lex *clex = (struct isl_context_lex *)context;
+ return tab_ineq_sign(clex->tab, ineq, strict);
+}
+
+/* Check whether "ineq" can be added to the tableau without rendering
+ * it infeasible.
+ */
+static int context_lex_test_ineq(struct isl_context *context, isl_int *ineq)
+{
+ struct isl_context_lex *clex = (struct isl_context_lex *)context;
+ struct isl_tab_undo *snap;
+ int feasible;
+
+ if (!clex->tab)
+ return -1;
+
+ if (isl_tab_extend_cons(clex->tab, 1) < 0)
+ return -1;
+
+ snap = isl_tab_snap(clex->tab);
+ isl_tab_push_basis(clex->tab);
+ clex->tab = add_lexmin_ineq(clex->tab, ineq);
+ clex->tab = check_integer_feasible(clex->tab);
+ if (!clex->tab)
+ return -1;
+ feasible = !clex->tab->empty;
+ if (isl_tab_rollback(clex->tab, snap) < 0)
+ return -1;
+
+ return feasible;
+}
+
+static int context_lex_get_div(struct isl_context *context, struct isl_tab *tab,
+ struct isl_vec *div)
+{
+ return get_div(tab, context, div);
+}
+
+static int context_lex_add_div(struct isl_context *context, struct isl_vec *div,
+ int *nonneg)
+{
+ struct isl_context_lex *clex = (struct isl_context_lex *)context;
+ return context_tab_add_div(clex->tab, div, nonneg);
+}
+
+static int context_lex_best_split(struct isl_context *context,
+ struct isl_tab *tab)
+{
+ struct isl_context_lex *clex = (struct isl_context_lex *)context;
+ struct isl_tab_undo *snap;
+ int r;
+
+ snap = isl_tab_snap(clex->tab);
+ isl_tab_push_basis(clex->tab);
+ r = best_split(tab, clex->tab);
+
+ if (isl_tab_rollback(clex->tab, snap) < 0)
+ return -1;
+
+ return r;
+}
+
+static int context_lex_is_empty(struct isl_context *context)
+{
+ struct isl_context_lex *clex = (struct isl_context_lex *)context;
+ if (!clex->tab)
+ return -1;
+ return clex->tab->empty;
+}
+
+static void *context_lex_save(struct isl_context *context)
+{
+ struct isl_context_lex *clex = (struct isl_context_lex *)context;
+ struct isl_tab_undo *snap;
+
+ snap = isl_tab_snap(clex->tab);
+ isl_tab_push_basis(clex->tab);
+ isl_tab_save_samples(clex->tab);
+
+ return snap;
+}
+
+static void context_lex_restore(struct isl_context *context, void *save)
+{
+ struct isl_context_lex *clex = (struct isl_context_lex *)context;
+ if (isl_tab_rollback(clex->tab, (struct isl_tab_undo *)save) < 0) {
+ isl_tab_free(clex->tab);
+ clex->tab = NULL;
}
+}
- isl_basic_set_free(dom);
- return sol_map;
-error:
- isl_basic_set_free(dom);
- sol_map_free(sol_map);
- return NULL;
+static int context_lex_is_ok(struct isl_context *context)
+{
+ struct isl_context_lex *clex = (struct isl_context_lex *)context;
+ return !!clex->tab;
}
/* For each variable in the context tableau, check if the variable can
struct isl_tab *context_tab)
{
int i;
- struct isl_tab_undo *snap, *snap2;
+ struct isl_tab_undo *snap;
struct isl_vec *ineq = NULL;
struct isl_tab_var *var;
int n;
goto error;
snap = isl_tab_snap(context_tab);
- isl_tab_push_basis(context_tab);
-
- snap2 = isl_tab_snap(context_tab);
n = 0;
isl_seq_clr(ineq->el, ineq->size);
n++;
}
isl_int_set_si(ineq->el[1 + i], 0);
- if (isl_tab_rollback(context_tab, snap2) < 0)
+ if (isl_tab_rollback(context_tab, snap) < 0)
goto error;
}
- if (isl_tab_rollback(context_tab, snap) < 0)
- goto error;
-
- if (n == context_tab->n_var) {
+ if (context_tab->M && n == context_tab->n_var) {
context_tab->mat = isl_mat_drop_cols(context_tab->mat, 2, 1);
context_tab->M = 0;
}
return NULL;
}
+static struct isl_tab *context_lex_detect_nonnegative_parameters(
+ struct isl_context *context, struct isl_tab *tab)
+{
+ struct isl_context_lex *clex = (struct isl_context_lex *)context;
+ struct isl_tab_undo *snap;
+
+ snap = isl_tab_snap(clex->tab);
+ isl_tab_push_basis(clex->tab);
+
+ tab = tab_detect_nonnegative_parameters(tab, clex->tab);
+
+ if (isl_tab_rollback(clex->tab, snap) < 0)
+ goto error;
+
+ return tab;
+error:
+ isl_tab_free(tab);
+ return NULL;
+}
+
+static void context_lex_invalidate(struct isl_context *context)
+{
+ struct isl_context_lex *clex = (struct isl_context_lex *)context;
+ isl_tab_free(clex->tab);
+ clex->tab = NULL;
+}
+
+static void context_lex_free(struct isl_context *context)
+{
+ struct isl_context_lex *clex = (struct isl_context_lex *)context;
+ isl_tab_free(clex->tab);
+ free(clex);
+}
+
+struct isl_context_op isl_context_lex_op = {
+ context_lex_detect_nonnegative_parameters,
+ context_lex_peek_basic_set,
+ context_lex_peek_tab,
+ context_lex_add_eq,
+ context_lex_add_ineq,
+ context_lex_ineq_sign,
+ context_lex_test_ineq,
+ context_lex_get_div,
+ context_lex_add_div,
+ context_lex_best_split,
+ context_lex_is_empty,
+ context_lex_is_ok,
+ context_lex_save,
+ context_lex_restore,
+ context_lex_invalidate,
+ context_lex_free,
+};
+
+static struct isl_tab *context_tab_for_lexmin(struct isl_basic_set *bset)
+{
+ struct isl_tab *tab;
+
+ bset = isl_basic_set_cow(bset);
+ if (!bset)
+ return NULL;
+ tab = tab_for_lexmin((struct isl_basic_map *)bset, NULL, 1, 0);
+ if (!tab)
+ goto error;
+ tab->bset = bset;
+ tab = isl_tab_init_samples(tab);
+ return tab;
+error:
+ isl_basic_set_free(bset);
+ return NULL;
+}
+
+static struct isl_context *isl_context_lex_alloc(struct isl_basic_set *dom)
+{
+ struct isl_context_lex *clex;
+
+ if (!dom)
+ return NULL;
+
+ clex = isl_alloc_type(dom->ctx, struct isl_context_lex);
+ if (!clex)
+ return NULL;
+
+ clex->context.op = &isl_context_lex_op;
+
+ clex->tab = context_tab_for_lexmin(isl_basic_set_copy(dom));
+ clex->tab = restore_lexmin(clex->tab);
+ clex->tab = check_integer_feasible(clex->tab);
+ if (!clex->tab)
+ goto error;
+
+ return &clex->context;
+error:
+ clex->context.op->free(&clex->context);
+ return NULL;
+}
+
+/* Construct an isl_sol_map structure for accumulating the solution.
+ * If track_empty is set, then we also keep track of the parts
+ * of the context where there is no solution.
+ * If max is set, then we are solving a maximization, rather than
+ * a minimization problem, which means that the variables in the
+ * tableau have value "M - x" rather than "M + x".
+ */
+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;
+
+ sol_map = isl_calloc_type(bset->ctx, struct isl_sol_map);
+ if (!sol_map)
+ goto error;
+
+ sol_map->max = max;
+ sol_map->sol.add = &sol_map_add_wrap;
+ sol_map->sol.free = &sol_map_free_wrap;
+ sol_map->map = isl_map_alloc_dim(isl_basic_map_get_dim(bmap), 1,
+ ISL_MAP_DISJOINT);
+ if (!sol_map->map)
+ goto error;
+
+ sol_map->sol.context = isl_context_lex_alloc(dom);
+ if (!sol_map->sol.context)
+ goto error;
+
+ if (track_empty) {
+ sol_map->empty = isl_set_alloc_dim(isl_basic_set_get_dim(dom),
+ 1, ISL_SET_DISJOINT);
+ if (!sol_map->empty)
+ goto error;
+ }
+
+ isl_basic_set_free(dom);
+ return sol_map;
+error:
+ isl_basic_set_free(dom);
+ sol_map_free(sol_map);
+ return NULL;
+}
+
/* Check whether all coefficients of (non-parameter) variables
* are non-positive, meaning that no pivots can be performed on the row.
*/
* >=0 ? Y N
* any neg
*/
-static int row_sign(struct isl_tab *tab, struct isl_sol *sol, int row)
+static enum isl_tab_row_sign row_sign(struct isl_tab *tab,
+ struct isl_sol *sol, int row)
{
- int i;
- struct isl_tab_undo *snap = NULL;
struct isl_vec *ineq = NULL;
int res = isl_tab_row_unknown;
int critical;
int strict;
- int sgn;
int row2;
- isl_int tmp;
- struct isl_tab *context_tab = sol->context_tab;
if (tab->row_sign[row] != isl_tab_row_unknown)
return tab->row_sign[row];
critical = is_critical(tab, row);
- isl_assert(tab->mat->ctx, context_tab->samples, goto error);
- isl_assert(tab->mat->ctx, context_tab->samples->n_col == 1 + context_tab->n_var, goto error);
-
ineq = get_row_parameter_ineq(tab, row);
if (!ineq)
goto error;
strict = is_strict(ineq);
- isl_int_init(tmp);
- for (i = context_tab->n_outside; i < context_tab->n_sample; ++i) {
- isl_seq_inner_product(context_tab->samples->row[i], ineq->el,
- ineq->size, &tmp);
- sgn = isl_int_sgn(tmp);
- if (sgn > 0 || (sgn == 0 && (critical || strict))) {
- if (res == isl_tab_row_unknown)
- res = isl_tab_row_pos;
- if (res == isl_tab_row_neg)
- res = isl_tab_row_any;
- }
- if (sgn < 0) {
- if (res == isl_tab_row_unknown)
- res = isl_tab_row_neg;
- if (res == isl_tab_row_pos)
- res = isl_tab_row_any;
- }
- if (res == isl_tab_row_any)
- break;
- }
- isl_int_clear(tmp);
-
- if (res != isl_tab_row_any) {
- if (isl_tab_extend_cons(context_tab, 1) < 0)
- goto error;
-
- snap = isl_tab_snap(context_tab);
- isl_tab_push_basis(context_tab);
- }
+ res = sol->context->op->ineq_sign(sol->context, ineq->el,
+ critical || strict);
if (res == isl_tab_row_unknown || res == isl_tab_row_pos) {
/* test for negative values */
isl_seq_neg(ineq->el, ineq->el, ineq->size);
isl_int_sub_ui(ineq->el[0], ineq->el[0], 1);
- isl_tab_push_basis(context_tab);
- sol->context_tab = add_lexmin_ineq(sol->context_tab, ineq->el);
- feasible = context_is_feasible(sol);
+ feasible = sol->context->op->test_ineq(sol->context, ineq->el);
if (feasible < 0)
goto error;
- context_tab = sol->context_tab;
if (!feasible)
res = isl_tab_row_pos;
else
res = (res == isl_tab_row_unknown) ? isl_tab_row_neg
: isl_tab_row_any;
- if (isl_tab_rollback(context_tab, snap) < 0)
- goto error;
-
if (res == isl_tab_row_neg) {
isl_seq_neg(ineq->el, ineq->el, ineq->size);
isl_int_sub_ui(ineq->el[0], ineq->el[0], 1);
if (!critical && !strict)
isl_int_sub_ui(ineq->el[0], ineq->el[0], 1);
- isl_tab_push_basis(context_tab);
- sol->context_tab = add_lexmin_ineq(sol->context_tab, ineq->el);
- feasible = context_is_feasible(sol);
+ feasible = sol->context->op->test_ineq(sol->context, ineq->el);
if (feasible < 0)
goto error;
- context_tab = sol->context_tab;
if (feasible)
res = isl_tab_row_any;
- if (isl_tab_rollback(context_tab, snap) < 0)
- goto error;
}
isl_vec_free(ineq);
static struct isl_sol *find_in_pos(struct isl_sol *sol,
struct isl_tab *tab, isl_int *ineq)
{
- struct isl_tab_undo *snap;
+ void *saved;
- snap = isl_tab_snap(sol->context_tab);
- isl_tab_push_basis(sol->context_tab);
- isl_tab_save_samples(sol->context_tab);
- if (isl_tab_extend_cons(sol->context_tab, 1) < 0)
+ if (!sol->context)
goto error;
+ saved = sol->context->op->save(sol->context);
tab = isl_tab_dup(tab);
if (!tab)
goto error;
- sol->context_tab = add_lexmin_ineq(sol->context_tab, ineq);
- sol->context_tab = check_samples(sol->context_tab, ineq, 0);
+ sol->context->op->add_ineq(sol->context, ineq, 0, 1);
sol = find_solutions(sol, tab);
- isl_tab_rollback(sol->context_tab, snap);
+ sol->context->op->restore(sol->context, saved);
return sol;
error:
- isl_tab_rollback(sol->context_tab, snap);
sol_free(sol);
return NULL;
}
struct isl_tab *tab, struct isl_vec *ineq)
{
int empty;
- int f;
- struct isl_tab_undo *snap;
- snap = isl_tab_snap(sol->context_tab);
- isl_tab_push_basis(sol->context_tab);
- isl_tab_save_samples(sol->context_tab);
- if (isl_tab_extend_cons(sol->context_tab, 1) < 0)
+ void *saved;
+
+ if (!sol->context)
goto error;
+ saved = sol->context->op->save(sol->context);
isl_int_sub_ui(ineq->el[0], ineq->el[0], 1);
- sol->context_tab = add_lexmin_ineq(sol->context_tab, ineq->el);
- f = context_valid_sample_or_feasible(sol, ineq->el, 0);
- if (f < 0)
+ sol->context->op->add_ineq(sol->context, ineq->el, 1, 0);
+ if (!sol->context)
goto error;
empty = tab->empty;
isl_int_add_ui(ineq->el[0], ineq->el[0], 1);
- if (isl_tab_rollback(sol->context_tab, snap) < 0)
- goto error;
+ sol->context->op->restore(sol->context, saved);
return sol;
error:
sol_free(sol);
return NULL;
}
-/* Given a main tableau where more than one row requires a split,
- * determine and return the "best" row to split on.
- *
- * Given two rows in the main tableau, if the inequality corresponding
- * to the first row is redundant with respect to that of the second row
- * in the current tableau, then it is better to split on the second row,
- * since in the positive part, both row will be positive.
- * (In the negative part a pivot will have to be performed and just about
- * anything can happen to the sign of the other row.)
- *
- * As a simple heuristic, we therefore select the row that makes the most
- * of the other rows redundant.
- *
- * Perhaps it would also be useful to look at the number of constraints
- * that conflict with any given constraint.
- */
-static int best_split(struct isl_tab *tab, struct isl_tab *context_tab)
-{
- struct isl_tab_undo *snap, *snap2;
- int split;
- int row;
- int best = -1;
- int best_r;
-
- if (isl_tab_extend_cons(context_tab, 2) < 0)
- return -1;
-
- snap = isl_tab_snap(context_tab);
- isl_tab_push_basis(context_tab);
- snap2 = isl_tab_snap(context_tab);
-
- for (split = tab->n_redundant; split < tab->n_row; ++split) {
- struct isl_tab_undo *snap3;
- struct isl_vec *ineq = NULL;
- int r = 0;
-
- if (!isl_tab_var_from_row(tab, split)->is_nonneg)
- continue;
- if (tab->row_sign[split] != isl_tab_row_any)
- continue;
-
- ineq = get_row_parameter_ineq(tab, split);
- if (!ineq)
- return -1;
- context_tab = isl_tab_add_ineq(context_tab, ineq->el);
- isl_vec_free(ineq);
-
- snap3 = isl_tab_snap(context_tab);
-
- for (row = tab->n_redundant; row < tab->n_row; ++row) {
- struct isl_tab_var *var;
-
- if (row == split)
- continue;
- if (!isl_tab_var_from_row(tab, row)->is_nonneg)
- continue;
- if (tab->row_sign[row] != isl_tab_row_any)
- continue;
-
- ineq = get_row_parameter_ineq(tab, row);
- if (!ineq)
- return -1;
- context_tab = isl_tab_add_ineq(context_tab, ineq->el);
- isl_vec_free(ineq);
- var = &context_tab->con[context_tab->n_con - 1];
- if (!context_tab->empty &&
- !isl_tab_min_at_most_neg_one(context_tab, var))
- r++;
- if (isl_tab_rollback(context_tab, snap3) < 0)
- return -1;
- }
- if (best == -1 || r > best_r) {
- best = split;
- best_r = r;
- }
- if (isl_tab_rollback(context_tab, snap2) < 0)
- return -1;
- }
-
- if (isl_tab_rollback(context_tab, snap) < 0)
- return -1;
-
- return best;
-}
-
/* Compute the lexicographic minimum of the set represented by the main
* tableau "tab" within the context "sol->context_tab".
* On entry the sample value of the main tableau is lexicographically
*/
static struct isl_sol *find_solutions(struct isl_sol *sol, struct isl_tab *tab)
{
- struct isl_tab **context_tab;
+ struct isl_context *context;
if (!tab || !sol)
goto error;
- context_tab = &sol->context_tab;
+ context = sol->context;
if (tab->empty)
goto done;
- if ((*context_tab)->empty)
+ if (context->op->is_empty(context))
goto done;
for (; tab && !tab->empty; tab = restore_lexmin(tab)) {
if (split != -1) {
struct isl_vec *ineq;
if (n_split != 1)
- split = best_split(tab, *context_tab);
+ split = context->op->best_split(context, tab);
if (split < 0)
goto error;
ineq = get_row_parameter_ineq(tab, split);
row = split;
isl_seq_neg(ineq->el, ineq->el, ineq->size);
isl_int_sub_ui(ineq->el[0], ineq->el[0], 1);
- *context_tab = add_lexmin_ineq(*context_tab, ineq->el);
- *context_tab = check_samples(*context_tab, ineq->el, 0);
+ context->op->add_ineq(context, ineq->el, 0, 1);
isl_vec_free(ineq);
if (!sol)
goto error;
struct isl_vec *div;
struct isl_vec *ineq;
int d;
- if (isl_tab_extend_cons(*context_tab, 3) < 0)
- goto error;
div = get_row_split_div(tab, row);
if (!div)
goto error;
- d = get_div(tab, context_tab, div);
+ d = context->op->get_div(context, tab, div);
isl_vec_free(div);
if (d < 0)
goto error;
- ineq = ineq_for_div((*context_tab)->bset, d);
+ ineq = ineq_for_div(context->op->peek_basic_set(context), d);
sol = no_sol_in_strict(sol, tab, ineq);
isl_seq_neg(ineq->el, ineq->el, ineq->size);
- *context_tab = add_lexmin_ineq(*context_tab, ineq->el);
- *context_tab = check_samples(*context_tab, ineq->el, 0);
+ context->op->add_ineq(context, ineq->el, 1, 1);
isl_vec_free(ineq);
- if (!sol)
+ if (!sol || !context->op->is_ok(context))
goto error;
tab = set_row_cst_to_div(tab, row, d);
} else
- row = add_parametric_cut(tab, row, context_tab);
+ row = add_parametric_cut(tab, row, context);
if (row < 0)
goto error;
}
p = tab->row_var[row]
+ tab->n_param - (tab->n_var - tab->n_div);
- if (isl_tab_extend_cons(sol->context_tab, 2) < 0)
- goto error;
-
eq = isl_vec_alloc(tab->mat->ctx, 1+tab->n_param+tab->n_div);
get_row_parameter_line(tab, row, eq->el);
isl_int_neg(eq->el[1 + p], tab->mat->row[row][0]);
sol = no_sol_in_strict(sol, tab, eq);
isl_seq_neg(eq->el, eq->el, eq->size);
- sol->context_tab = add_lexmin_eq(sol->context_tab, eq->el);
- context_valid_sample_or_feasible(sol, eq->el, 1);
- sol->context_tab = check_samples(sol->context_tab, eq->el, 1);
+ sol->context->op->add_eq(sol->context, eq->el, 1, 1);
isl_vec_free(eq);
isl_tab_mark_redundant(tab, row);
- if (!sol->context_tab)
- goto error;
- if (sol->context_tab->empty)
+ if (sol->context->op->is_empty(sol->context))
break;
row = tab->n_redundant - 1;
struct isl_tab *tab;
struct isl_map *result = NULL;
struct isl_sol_map *sol_map = NULL;
+ struct isl_context *context;
if (empty)
*empty = NULL;
if (!sol_map)
goto error;
- if (isl_basic_set_fast_is_empty(sol_map->sol.context_tab->bset))
+ context = sol_map->sol.context;
+ 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);
else {
tab = tab_for_lexmin(bmap,
- sol_map->sol.context_tab->bset, 1, max);
- tab = tab_detect_nonnegative_parameters(tab,
- sol_map->sol.context_tab);
+ context->op->peek_basic_set(context), 1, max);
+ tab = context->op->detect_nonnegative_parameters(context, tab);
sol_map = sol_map_find_solutions(sol_map, tab);
if (!sol_map)
goto error;
static void sol_for_free(struct isl_sol_for *sol_for)
{
- isl_tab_free(sol_for->sol.context_tab);
+ if (sol_for->sol.context)
+ sol_for->sol.context->op->free(sol_for->sol.context);
free(sol_for);
}
static struct isl_sol_for *sol_for_add(struct isl_sol_for *sol,
struct isl_tab *tab)
{
- struct isl_tab *context_tab;
struct isl_basic_set *bset;
struct isl_mat *mat = NULL;
unsigned n_out;
return sol;
off = 2 + tab->M;
- context_tab = sol->sol.context_tab;
n_out = tab->n_var - tab->n_param - tab->n_div;
mat = isl_mat_alloc(tab->mat->ctx, 1 + n_out, 1 + tab->n_param + tab->n_div);
mat->n_col);
}
- bset = isl_basic_set_dup(context_tab->bset);
+ bset = sol->sol.context->op->peek_basic_set(sol->sol.context);
+ bset = isl_basic_set_dup(bset);
bset = isl_basic_set_finalize(bset);
if (sol->fn(bset, isl_mat_copy(mat), sol->user) < 0)
struct isl_sol_for *sol_for = NULL;
struct isl_dim *dom_dim;
struct isl_basic_set *dom = NULL;
- struct isl_tab *context_tab;
- int f;
sol_for = isl_calloc_type(bset->ctx, struct isl_sol_for);
if (!sol_for)
sol_for->sol.add = &sol_for_add_wrap;
sol_for->sol.free = &sol_for_free_wrap;
- context_tab = context_tab_for_lexmin(isl_basic_set_copy(dom));
- context_tab = restore_lexmin(context_tab);
- sol_for->sol.context_tab = context_tab;
- f = context_is_feasible(&sol_for->sol);
- if (f < 0)
+ sol_for->sol.context = isl_context_lex_alloc(dom);
+ if (!sol_for->sol.context)
goto error;
isl_basic_set_free(dom);
/* nothing */;
else {
struct isl_tab *tab;
+ struct isl_context *context = sol_for->sol.context;
tab = tab_for_lexmin(bmap,
- sol_for->sol.context_tab->bset, 1, max);
- tab = tab_detect_nonnegative_parameters(tab,
- sol_for->sol.context_tab);
+ context->op->peek_basic_set(context), 1, max);
+ tab = context->op->detect_nonnegative_parameters(context, tab);
sol_for = sol_for_find_solutions(sol_for, tab);
if (!sol_for)
goto error;
projects / platform / upstream / isl.git / commitdiff