+ 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;
+ int ok;
+
+ 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;
+ ok = isl_tab_add_ineq(context_tab, ineq->el) >= 0;
+ isl_vec_free(ineq);
+ if (!ok)
+ return -1;
+
+ 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;
+ ok = isl_tab_add_ineq(context_tab, ineq->el) >= 0;
+ isl_vec_free(ineq);
+ if (!ok)
+ return -1;
+ 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;
+ return isl_tab_peek_bset(clex->tab);
+}
+
+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_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;
+ if (add_lexmin_eq(clex->tab, eq) < 0)
+ goto error;
+ 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_tab_free(clex->tab);
+ clex->tab = NULL;
+}
+
+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;
+}
+
+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.
+ */
+static enum isl_tab_row_sign tab_ineq_sign(struct isl_tab *tab, isl_int *ineq,
+ int strict)
+{
+ int i;
+ int sgn;
+ isl_int tmp;
+ enum isl_tab_row_sign res = isl_tab_row_unknown;
+
+ 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) {
+ 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);
+
+ return res;
+}
+
+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);
+ if (isl_tab_push_basis(clex->tab) < 0)
+ return -1;
+ 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);
+}
+
+/* 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
+ * 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)
+{
+ struct isl_context_lex *clex = (struct isl_context_lex *)context;
+ int nonneg;
+ nonneg = context_tab_add_div(clex->tab, div,
+ context_lex_add_ineq_wrap, context);
+ if (nonneg < 0)
+ return -1;
+ if (clex->tab->M)
+ return 0;
+ return nonneg;
+}
+
+static int context_lex_detect_equalities(struct isl_context *context,
+ struct isl_tab *tab)
+{
+ return 0;
+}
+
+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);
+ if (isl_tab_push_basis(clex->tab) < 0)
+ return -1;
+ r = best_split(tab, clex->tab);
+
+ if (r >= 0 && 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);
+ if (isl_tab_push_basis(clex->tab) < 0)
+ return NULL;
+ if (isl_tab_save_samples(clex->tab) < 0)
+ return NULL;
+
+ 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;
+ }
+}
+
+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
+ * only attain non-negative values. If so, mark the parameter as non-negative
+ * in the main tableau. This allows for a more direct identification of some
+ * cases of violated constraints.
+ */
+static struct isl_tab *tab_detect_nonnegative_parameters(struct isl_tab *tab,
+ struct isl_tab *context_tab)
+{
+ int i;
+ struct isl_tab_undo *snap;
+ struct isl_vec *ineq = NULL;
+ struct isl_tab_var *var;
+ int n;
+
+ if (context_tab->n_var == 0)
+ return tab;
+
+ ineq = isl_vec_alloc(tab->mat->ctx, 1 + context_tab->n_var);
+ if (!ineq)
+ goto error;
+
+ if (isl_tab_extend_cons(context_tab, 1) < 0)
+ goto error;
+
+ snap = isl_tab_snap(context_tab);
+
+ n = 0;
+ isl_seq_clr(ineq->el, ineq->size);
+ for (i = 0; i < context_tab->n_var; ++i) {
+ isl_int_set_si(ineq->el[1 + i], 1);
+ if (isl_tab_add_ineq(context_tab, ineq->el) < 0)
+ goto error;
+ var = &context_tab->con[context_tab->n_con - 1];
+ if (!context_tab->empty &&
+ !isl_tab_min_at_most_neg_one(context_tab, var)) {
+ int j = i;
+ if (i >= tab->n_param)
+ j = i - tab->n_param + tab->n_var - tab->n_div;
+ tab->var[j].is_nonneg = 1;
+ n++;
+ }
+ isl_int_set_si(ineq->el[1 + i], 0);
+ if (isl_tab_rollback(context_tab, snap) < 0)
+ goto error;
+ }
+
+ 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;
+ }
+
+ isl_vec_free(ineq);
+ return tab;
+error:
+ isl_vec_free(ineq);
+ isl_tab_free(tab);
+ 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;
+
+ if (!tab)
+ return NULL;
+
+ snap = isl_tab_snap(clex->tab);
+ if (isl_tab_push_basis(clex->tab) < 0)
+ goto error;
+
+ 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_detect_equalities,
+ 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;
+ if (isl_tab_track_bset(tab, bset) < 0)
+ goto error;
+ 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));
+ if (restore_lexmin(clex->tab) < 0)
+ goto error;
+ clex->tab = check_integer_feasible(clex->tab);
+ if (!clex->tab)
+ goto error;
+
+ return &clex->context;
+error:
+ clex->context.op->free(&clex->context);
+ return NULL;
+}
+
+struct isl_context_gbr {
+ struct isl_context context;
+ struct isl_tab *tab;
+ struct isl_tab *shifted;
+ struct isl_tab *cone;
+};
+
+static struct isl_tab *context_gbr_detect_nonnegative_parameters(
+ 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);
+}
+
+static struct isl_basic_set *context_gbr_peek_basic_set(
+ struct isl_context *context)
+{
+ struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
+ if (!cgbr->tab)
+ return NULL;
+ return isl_tab_peek_bset(cgbr->tab);
+}
+
+static struct isl_tab *context_gbr_peek_tab(struct isl_context *context)
+{
+ struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
+ return cgbr->tab;
+}
+
+/* Initialize the "shifted" tableau of the context, which
+ * contains the constraints of the original tableau shifted
+ * by the sum of all negative coefficients. This ensures
+ * that any rational point in the shifted tableau can
+ * be rounded up to yield an integer point in the original tableau.
+ */
+static void gbr_init_shifted(struct isl_context_gbr *cgbr)
+{
+ int i, j;
+ struct isl_vec *cst;
+ struct isl_basic_set *bset = isl_tab_peek_bset(cgbr->tab);
+ unsigned dim = isl_basic_set_total_dim(bset);
+
+ cst = isl_vec_alloc(cgbr->tab->mat->ctx, bset->n_ineq);
+ if (!cst)
+ return;
+
+ for (i = 0; i < bset->n_ineq; ++i) {
+ isl_int_set(cst->el[i], bset->ineq[i][0]);
+ for (j = 0; j < dim; ++j) {
+ if (!isl_int_is_neg(bset->ineq[i][1 + j]))
+ continue;
+ isl_int_add(bset->ineq[i][0], bset->ineq[i][0],
+ bset->ineq[i][1 + j]);
+ }
+ }
+
+ cgbr->shifted = isl_tab_from_basic_set(bset);
+
+ for (i = 0; i < bset->n_ineq; ++i)
+ isl_int_set(bset->ineq[i][0], cst->el[i]);
+
+ isl_vec_free(cst);
+}
+
+/* Check if the shifted tableau is non-empty, and if so
+ * use the sample point to construct an integer point
+ * of the context tableau.
+ */
+static struct isl_vec *gbr_get_shifted_sample(struct isl_context_gbr *cgbr)
+{
+ struct isl_vec *sample;
+
+ if (!cgbr->shifted)
+ gbr_init_shifted(cgbr);
+ if (!cgbr->shifted)
+ return NULL;
+ if (cgbr->shifted->empty)
+ return isl_vec_alloc(cgbr->tab->mat->ctx, 0);
+
+ sample = isl_tab_get_sample_value(cgbr->shifted);
+ sample = isl_vec_ceil(sample);
+
+ return sample;
+}
+
+static struct isl_basic_set *drop_constant_terms(struct isl_basic_set *bset)
+{
+ int i;
+
+ if (!bset)
+ return NULL;
+
+ for (i = 0; i < bset->n_eq; ++i)
+ isl_int_set_si(bset->eq[i][0], 0);
+
+ for (i = 0; i < bset->n_ineq; ++i)
+ isl_int_set_si(bset->ineq[i][0], 0);
+
+ return bset;
+}
+
+static int use_shifted(struct isl_context_gbr *cgbr)
+{
+ return cgbr->tab->bmap->n_eq == 0 && cgbr->tab->bmap->n_div == 0;
+}
+
+static struct isl_vec *gbr_get_sample(struct isl_context_gbr *cgbr)
+{
+ struct isl_basic_set *bset;
+ struct isl_basic_set *cone;
+
+ if (isl_tab_sample_is_integer(cgbr->tab))
+ return isl_tab_get_sample_value(cgbr->tab);
+
+ if (use_shifted(cgbr)) {
+ struct isl_vec *sample;
+
+ sample = gbr_get_shifted_sample(cgbr);
+ if (!sample || sample->size > 0)
+ return sample;
+
+ isl_vec_free(sample);
+ }
+
+ if (!cgbr->cone) {
+ bset = isl_tab_peek_bset(cgbr->tab);
+ 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;
+ }
+ if (isl_tab_detect_implicit_equalities(cgbr->cone) < 0)
+ return NULL;
+
+ if (cgbr->cone->n_dead == cgbr->cone->n_col) {
+ struct isl_vec *sample;
+ struct isl_tab_undo *snap;
+
+ if (cgbr->tab->basis) {
+ if (cgbr->tab->basis->n_col != 1 + cgbr->tab->n_var) {
+ isl_mat_free(cgbr->tab->basis);
+ cgbr->tab->basis = NULL;
+ }
+ cgbr->tab->n_zero = 0;
+ cgbr->tab->n_unbounded = 0;
+ }
+
+ snap = isl_tab_snap(cgbr->tab);
+
+ sample = isl_tab_sample(cgbr->tab);
+
+ if (isl_tab_rollback(cgbr->tab, snap) < 0) {
+ isl_vec_free(sample);
+ return NULL;
+ }
+
+ return sample;
+ }
+
+ cone = isl_basic_set_dup(isl_tab_peek_bset(cgbr->cone));
+ cone = drop_constant_terms(cone);
+ cone = isl_basic_set_update_from_tab(cone, cgbr->cone);
+ cone = isl_basic_set_underlying_set(cone);
+ cone = isl_basic_set_gauss(cone, NULL);
+
+ bset = isl_basic_set_dup(isl_tab_peek_bset(cgbr->tab));
+ bset = isl_basic_set_update_from_tab(bset, cgbr->tab);
+ bset = isl_basic_set_underlying_set(bset);
+ bset = isl_basic_set_gauss(bset, NULL);
+
+ return isl_basic_set_sample_with_cone(bset, cone);
+}
+
+static void check_gbr_integer_feasible(struct isl_context_gbr *cgbr)
+{
+ struct isl_vec *sample;
+
+ if (!cgbr->tab)
+ return;
+
+ if (cgbr->tab->empty)
+ return;
+
+ sample = gbr_get_sample(cgbr);
+ if (!sample)
+ goto error;
+
+ if (sample->size == 0) {
+ isl_vec_free(sample);
+ if (isl_tab_mark_empty(cgbr->tab) < 0)
+ goto error;
+ return;
+ }
+
+ cgbr->tab = isl_tab_add_sample(cgbr->tab, sample);
+
+ return;
+error:
+ isl_tab_free(cgbr->tab);
+ cgbr->tab = NULL;
+}
+
+static struct isl_tab *add_gbr_eq(struct isl_tab *tab, isl_int *eq)
+{
+ if (!tab)
+ return NULL;
+
+ if (isl_tab_extend_cons(tab, 2) < 0)
+ goto error;
+
+ if (isl_tab_add_eq(tab, eq) < 0)
+ goto error;
+
+ return tab;
+error:
+ isl_tab_free(tab);
+ return NULL;
+}
+
+static void context_gbr_add_eq(struct isl_context *context, isl_int *eq,
+ int check, int update)
+{
+ struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
+
+ cgbr->tab = add_gbr_eq(cgbr->tab, eq);
+
+ if (cgbr->cone && cgbr->cone->n_col != cgbr->cone->n_dead) {
+ if (isl_tab_extend_cons(cgbr->cone, 2) < 0)
+ goto error;
+ if (isl_tab_add_eq(cgbr->cone, eq) < 0)
+ goto error;
+ }
+
+ if (check) {
+ int v = tab_has_valid_sample(cgbr->tab, eq, 1);
+ if (v < 0)
+ goto error;
+ if (!v)
+ check_gbr_integer_feasible(cgbr);
+ }
+ if (update)
+ cgbr->tab = check_samples(cgbr->tab, eq, 1);
+ return;
+error:
+ isl_tab_free(cgbr->tab);
+ cgbr->tab = NULL;
+}
+
+static void add_gbr_ineq(struct isl_context_gbr *cgbr, isl_int *ineq)
+{
+ if (!cgbr->tab)
+ return;
+
+ if (isl_tab_extend_cons(cgbr->tab, 1) < 0)
+ goto error;
+
+ if (isl_tab_add_ineq(cgbr->tab, ineq) < 0)
+ goto error;
+
+ if (cgbr->shifted && !cgbr->shifted->empty && use_shifted(cgbr)) {
+ int i;
+ unsigned dim;
+ dim = isl_basic_map_total_dim(cgbr->tab->bmap);
+
+ if (isl_tab_extend_cons(cgbr->shifted, 1) < 0)
+ goto error;
+
+ for (i = 0; i < dim; ++i) {
+ if (!isl_int_is_neg(ineq[1 + i]))
+ continue;
+ isl_int_add(ineq[0], ineq[0], ineq[1 + i]);
+ }
+
+ if (isl_tab_add_ineq(cgbr->shifted, ineq) < 0)
+ goto error;
+
+ for (i = 0; i < dim; ++i) {
+ if (!isl_int_is_neg(ineq[1 + i]))
+ continue;
+ isl_int_sub(ineq[0], ineq[0], ineq[1 + i]);
+ }
+ }
+
+ if (cgbr->cone && cgbr->cone->n_col != cgbr->cone->n_dead) {
+ if (isl_tab_extend_cons(cgbr->cone, 1) < 0)
+ goto error;
+ if (isl_tab_add_ineq(cgbr->cone, ineq) < 0)
+ goto error;
+ }
+
+ return;
+error:
+ isl_tab_free(cgbr->tab);
+ cgbr->tab = NULL;
+}
+
+static void context_gbr_add_ineq(struct isl_context *context, isl_int *ineq,
+ int check, int update)
+{
+ struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
+
+ add_gbr_ineq(cgbr, ineq);
+ if (!cgbr->tab)
+ return;
+
+ if (check) {
+ int v = tab_has_valid_sample(cgbr->tab, ineq, 0);
+ if (v < 0)
+ goto error;
+ if (!v)
+ check_gbr_integer_feasible(cgbr);
+ }
+ if (update)
+ cgbr->tab = check_samples(cgbr->tab, ineq, 0);
+ return;
+error:
+ isl_tab_free(cgbr->tab);
+ 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)
+{
+ struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
+ return tab_ineq_sign(cgbr->tab, ineq, strict);
+}
+
+/* Check whether "ineq" can be added to the tableau without rendering
+ * it infeasible.
+ */
+static int context_gbr_test_ineq(struct isl_context *context, isl_int *ineq)
+{
+ struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
+ struct isl_tab_undo *snap;
+ struct isl_tab_undo *shifted_snap = NULL;
+ struct isl_tab_undo *cone_snap = NULL;
+ int feasible;
+
+ if (!cgbr->tab)
+ return -1;
+
+ if (isl_tab_extend_cons(cgbr->tab, 1) < 0)
+ return -1;
+
+ snap = isl_tab_snap(cgbr->tab);
+ if (cgbr->shifted)
+ shifted_snap = isl_tab_snap(cgbr->shifted);
+ if (cgbr->cone)
+ cone_snap = isl_tab_snap(cgbr->cone);
+ add_gbr_ineq(cgbr, ineq);
+ check_gbr_integer_feasible(cgbr);
+ if (!cgbr->tab)
+ return -1;
+ feasible = !cgbr->tab->empty;
+ if (isl_tab_rollback(cgbr->tab, snap) < 0)
+ return -1;
+ if (shifted_snap) {
+ if (isl_tab_rollback(cgbr->shifted, shifted_snap))
+ return -1;
+ } else if (cgbr->shifted) {
+ isl_tab_free(cgbr->shifted);
+ cgbr->shifted = NULL;
+ }
+ if (cone_snap) {
+ if (isl_tab_rollback(cgbr->cone, cone_snap))
+ return -1;
+ } else if (cgbr->cone) {
+ isl_tab_free(cgbr->cone);
+ cgbr->cone = NULL;
+ }
+
+ return feasible;
+}
+
+/* Return the column of the last of the variables associated to
+ * a column that has a non-zero coefficient.
+ * This function is called in a context where only coefficients
+ * of parameters or divs can be non-zero.
+ */
+static int last_non_zero_var_col(struct isl_tab *tab, isl_int *p)
+{
+ int i;
+ int col;
+
+ if (tab->n_var == 0)
+ return -1;
+
+ for (i = tab->n_var - 1; i >= 0; --i) {
+ if (i >= tab->n_param && i < tab->n_var - tab->n_div)
+ continue;
+ if (tab->var[i].is_row)
+ continue;
+ col = tab->var[i].index;
+ if (!isl_int_is_zero(p[col]))
+ return col;
+ }
+
+ return -1;
+}
+
+/* Look through all the recently added equalities in the context
+ * to see if we can propagate any of them to the main tableau.
+ *
+ * The newly added equalities in the context are encoded as pairs
+ * of inequalities starting at inequality "first".
+ *
+ * We tentatively add each of these equalities to the main tableau
+ * and if this happens to result in a row with a final coefficient
+ * that is one or negative one, we use it to kill a column
+ * in the main tableau. Otherwise, we discard the tentatively
+ * added row.
+ */
+static void propagate_equalities(struct isl_context_gbr *cgbr,
+ struct isl_tab *tab, unsigned first)
+{
+ int i;
+ struct isl_vec *eq = NULL;
+
+ eq = isl_vec_alloc(tab->mat->ctx, 1 + tab->n_var);
+ if (!eq)
+ goto error;
+
+ if (isl_tab_extend_cons(tab, (cgbr->tab->bmap->n_ineq - first)/2) < 0)
+ goto error;
+
+ isl_seq_clr(eq->el + 1 + tab->n_param,
+ tab->n_var - tab->n_param - tab->n_div);
+ for (i = first; i < cgbr->tab->bmap->n_ineq; i += 2) {
+ int j;
+ int r;
+ struct isl_tab_undo *snap;
+ snap = isl_tab_snap(tab);
+
+ isl_seq_cpy(eq->el, cgbr->tab->bmap->ineq[i], 1 + tab->n_param);
+ isl_seq_cpy(eq->el + 1 + tab->n_var - tab->n_div,
+ cgbr->tab->bmap->ineq[i] + 1 + tab->n_param,
+ tab->n_div);
+
+ r = isl_tab_add_row(tab, eq->el);
+ if (r < 0)
+ goto error;
+ r = tab->con[r].index;
+ j = last_non_zero_var_col(tab, tab->mat->row[r] + 2 + tab->M);
+ if (j < 0 || j < tab->n_dead ||
+ !isl_int_is_one(tab->mat->row[r][0]) ||
+ (!isl_int_is_one(tab->mat->row[r][2 + tab->M + j]) &&
+ !isl_int_is_negone(tab->mat->row[r][2 + tab->M + j]))) {
+ if (isl_tab_rollback(tab, snap) < 0)
+ goto error;
+ continue;
+ }
+ if (isl_tab_pivot(tab, r, j) < 0)
+ goto error;
+ if (isl_tab_kill_col(tab, j) < 0)
+ goto error;
+
+ if (restore_lexmin(tab) < 0)
+ goto error;
+ }
+
+ isl_vec_free(eq);
+
+ return;
+error:
+ isl_vec_free(eq);
+ isl_tab_free(cgbr->tab);
+ cgbr->tab = NULL;
+}
+
+static int context_gbr_detect_equalities(struct isl_context *context,
+ struct isl_tab *tab)
+{
+ struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
+ struct isl_ctx *ctx;
+ unsigned n_ineq;
+
+ ctx = cgbr->tab->mat->ctx;
+
+ if (!cgbr->cone) {
+ struct isl_basic_set *bset = isl_tab_peek_bset(cgbr->tab);
+ 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;
+ }
+ 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);
+ if (cgbr->tab && cgbr->tab->bmap->n_ineq > n_ineq)
+ propagate_equalities(cgbr, tab, n_ineq);
+
+ return 0;
+error:
+ isl_tab_free(cgbr->tab);
+ cgbr->tab = NULL;
+ return -1;
+}
+
+static int context_gbr_get_div(struct isl_context *context, struct isl_tab *tab,
+ struct isl_vec *div)
+{
+ return get_div(tab, context, div);
+}
+
+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) {
+ int k;
+
+ if (isl_tab_extend_cons(cgbr->cone, 3) < 0)
+ return -1;
+ 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_dim(cgbr->cone->bmap,
+ isl_basic_map_get_dim(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 context_tab_add_div(cgbr->tab, div,
+ context_gbr_add_ineq_wrap, context);
+}
+
+static int context_gbr_best_split(struct isl_context *context,
+ struct isl_tab *tab)
+{
+ struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
+ struct isl_tab_undo *snap;
+ int r;
+
+ snap = isl_tab_snap(cgbr->tab);
+ r = best_split(tab, cgbr->tab);
+
+ if (r >= 0 && isl_tab_rollback(cgbr->tab, snap) < 0)
+ return -1;
+
+ return r;
+}
+
+static int context_gbr_is_empty(struct isl_context *context)
+{
+ struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
+ if (!cgbr->tab)
+ return -1;
+ return cgbr->tab->empty;
+}
+
+struct isl_gbr_tab_undo {
+ struct isl_tab_undo *tab_snap;
+ struct isl_tab_undo *shifted_snap;
+ struct isl_tab_undo *cone_snap;
+};
+
+static void *context_gbr_save(struct isl_context *context)
+{
+ struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
+ struct isl_gbr_tab_undo *snap;
+
+ snap = isl_alloc_type(cgbr->tab->mat->ctx, struct isl_gbr_tab_undo);
+ if (!snap)
+ return NULL;
+
+ snap->tab_snap = isl_tab_snap(cgbr->tab);
+ if (isl_tab_save_samples(cgbr->tab) < 0)
+ goto error;
+
+ if (cgbr->shifted)
+ snap->shifted_snap = isl_tab_snap(cgbr->shifted);
+ else
+ snap->shifted_snap = NULL;
+
+ if (cgbr->cone)
+ snap->cone_snap = isl_tab_snap(cgbr->cone);
+ else
+ snap->cone_snap = NULL;
+
+ return snap;
+error:
+ free(snap);
+ return NULL;
+}
+
+static void context_gbr_restore(struct isl_context *context, void *save)
+{
+ struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
+ struct isl_gbr_tab_undo *snap = (struct isl_gbr_tab_undo *)save;
+ if (!snap)
+ goto error;
+ if (isl_tab_rollback(cgbr->tab, snap->tab_snap) < 0) {
+ isl_tab_free(cgbr->tab);
+ cgbr->tab = NULL;
+ }
+
+ if (snap->shifted_snap) {
+ if (isl_tab_rollback(cgbr->shifted, snap->shifted_snap) < 0)
+ goto error;
+ } else if (cgbr->shifted) {
+ isl_tab_free(cgbr->shifted);
+ cgbr->shifted = NULL;
+ }
+
+ if (snap->cone_snap) {
+ if (isl_tab_rollback(cgbr->cone, snap->cone_snap) < 0)
+ goto error;
+ } else if (cgbr->cone) {
+ isl_tab_free(cgbr->cone);
+ cgbr->cone = NULL;
+ }
+
+ free(snap);
+
+ return;
+error:
+ free(snap);
+ isl_tab_free(cgbr->tab);
+ cgbr->tab = NULL;
+}
+
+static int context_gbr_is_ok(struct isl_context *context)
+{
+ struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
+ return !!cgbr->tab;
+}
+
+static void context_gbr_invalidate(struct isl_context *context)
+{
+ struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
+ isl_tab_free(cgbr->tab);
+ cgbr->tab = NULL;
+}
+
+static void 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);
+}
+
+struct isl_context_op isl_context_gbr_op = {
+ context_gbr_detect_nonnegative_parameters,
+ context_gbr_peek_basic_set,
+ context_gbr_peek_tab,
+ context_gbr_add_eq,
+ context_gbr_add_ineq,
+ context_gbr_ineq_sign,
+ context_gbr_test_ineq,
+ context_gbr_get_div,
+ context_gbr_add_div,
+ context_gbr_detect_equalities,
+ context_gbr_best_split,
+ context_gbr_is_empty,
+ context_gbr_is_ok,
+ context_gbr_save,
+ context_gbr_restore,
+ context_gbr_invalidate,
+ context_gbr_free,
+};
+
+static struct isl_context *isl_context_gbr_alloc(struct isl_basic_set *dom)
+{
+ struct isl_context_gbr *cgbr;
+
+ if (!dom)
+ return NULL;
+
+ cgbr = isl_calloc_type(dom->ctx, struct isl_context_gbr);
+ if (!cgbr)
+ return NULL;
+
+ cgbr->context.op = &isl_context_gbr_op;
+
+ cgbr->shifted = NULL;
+ cgbr->cone = NULL;
+ cgbr->tab = isl_tab_from_basic_set(dom);
+ cgbr->tab = isl_tab_init_samples(cgbr->tab);
+ if (!cgbr->tab)
+ goto error;
+ if (isl_tab_track_bset(cgbr->tab,
+ isl_basic_set_cow(isl_basic_set_copy(dom))) < 0)
+ goto error;
+ check_gbr_integer_feasible(cgbr);
+
+ return &cgbr->context;
+error:
+ cgbr->context.op->free(&cgbr->context);
+ return NULL;
+}
+
+static struct isl_context *isl_context_alloc(struct isl_basic_set *dom)
+{
+ if (!dom)
+ return NULL;
+
+ if (dom->ctx->opt->context == ISL_CONTEXT_LEXMIN)
+ return isl_context_lex_alloc(dom);
+ else
+ return isl_context_gbr_alloc(dom);
+}