isl_tab_pip.c

   1 #include "isl_map_private.h"
   2 #include "isl_seq.h"
   3 #include "isl_tab.h"
   4 #include "isl_sample.h"
   5
   6 /*
   7  * The implementation of parametric integer linear programming in this file
   8  * was inspired by the paper "Parametric Integer Programming" and the
   9  * report "Solving systems of affine (in)equalities" by Paul Feautrier
  10  * (and others).
  11  *
  12  * The strategy used for obtaining a feasible solution is different
  13  * from the one used in isl_tab.c.  In particular, in isl_tab.c,
  14  * upon finding a constraint that is not yet satisfied, we pivot
  15  * in a row that increases the constant term of row holding the
  16  * constraint, making sure the sample solution remains feasible
  17  * for all the constraints it already satisfied.
  18  * Here, we always pivot in the row holding the constraint,
  19  * choosing a column that induces the lexicographically smallest
  20  * increment to the sample solution.
  21  *
  22  * By starting out from a sample value that is lexicographically
  23  * smaller than any integer point in the problem space, the first
  24  * feasible integer sample point we find will also be the lexicographically
  25  * smallest.  If all variables can be assumed to be non-negative,
  26  * then the initial sample value may be chosen equal to zero.
  27  * However, we will not make this assumption.  Instead, we apply
  28  * the "big parameter" trick.  Any variable x is then not directly
  29  * used in the tableau, but instead it its represented by another
  30  * variable x' = M + x, where M is an arbitrarily large (positive)
  31  * value.  x' is therefore always non-negative, whatever the value of x.
  32  * Taking as initial smaple value x' = 0 corresponds to x = -M,
  33  * which is always smaller than any possible value of x.
  34  *
  35  * The big parameter trick is used in the main tableau and
  36  * also in the context tableau if isl_context_lex is used.
  37  * In this case, each tableaus has its own big parameter.
  38  * Before doing any real work, we check if all the parameters
  39  * happen to be non-negative.  If so, we drop the column corresponding
  40  * to M from the initial context tableau.
  41  * If isl_context_gbr is used, then the big parameter trick is only
  42  * used in the main tableau.
  43  */
  44
  45 struct isl_context;
  46 struct isl_context_op {
  47         /* detect nonnegative parameters in context and mark them in tab */
  48         struct isl_tab *(*detect_nonnegative_parameters)(
  49                         struct isl_context *context, struct isl_tab *tab);
  50         /* return temporary reference to basic set representation of context */
  51         struct isl_basic_set *(*peek_basic_set)(struct isl_context *context);
  52         /* return temporary reference to tableau representation of context */
  53         struct isl_tab *(*peek_tab)(struct isl_context *context);
  54         /* add equality; check is 1 if eq may not be valid;
  55          * update is 1 if we may want to call ineq_sign on context later.
  56          */
  57         void (*add_eq)(struct isl_context *context, isl_int *eq,
  58                         int check, int update);
  59         /* add inequality; check is 1 if ineq may not be valid;
  60          * update is 1 if we may want to call ineq_sign on context later.
  61          */
  62         void (*add_ineq)(struct isl_context *context, isl_int *ineq,
  63                         int check, int update);
  64         /* check sign of ineq based on previous information.
  65          * strict is 1 if saturation should be treated as a positive sign.
  66          */
  67         enum isl_tab_row_sign (*ineq_sign)(struct isl_context *context,
  68                         isl_int *ineq, int strict);
  69         /* check if inequality maintains feasibility */
  70         int (*test_ineq)(struct isl_context *context, isl_int *ineq);
  71         /* return index of a div that corresponds to "div" */
  72         int (*get_div)(struct isl_context *context, struct isl_tab *tab,
  73                         struct isl_vec *div);
  74         /* add div "div" to context and return index and non-negativity */
  75         int (*add_div)(struct isl_context *context, struct isl_vec *div,
  76                         int *nonneg);
  77         int (*detect_equalities)(struct isl_context *context,
  78                         struct isl_tab *tab);
  79         /* return row index of "best" split */
  80         int (*best_split)(struct isl_context *context, struct isl_tab *tab);
  81         /* check if context has already been determined to be empty */
  82         int (*is_empty)(struct isl_context *context);
  83         /* check if context is still usable */
  84         int (*is_ok)(struct isl_context *context);
  85         /* save a copy/snapshot of context */
  86         void *(*save)(struct isl_context *context);
  87         /* restore saved context */
  88         void (*restore)(struct isl_context *context, void *);
  89         /* invalidate context */
  90         void (*invalidate)(struct isl_context *context);
  91         /* free context */
  92         void (*free)(struct isl_context *context);
  93 };
  94
  95 struct isl_context {
  96         struct isl_context_op *op;
  97 };
  98
  99 struct isl_context_lex {
 100         struct isl_context context;
 101         struct isl_tab *tab;
 102 };
 103
 104 /* isl_sol is an interface for constructing a solution to
 105  * a parametric integer linear programming problem.
 106  * Every time the algorithm reaches a state where a solution
 107  * can be read off from the tableau (including cases where the tableau
 108  * is empty), the function "add" is called on the isl_sol passed
 109  * to find_solutions_main.
 110  *
 111  * The context tableau is owned by isl_sol and is updated incrementally.
 112  *
 113  * There are currently two implementations of this interface,
 114  * isl_sol_map, which simply collects the solutions in an isl_map
 115  * and (optionally) the parts of the context where there is no solution
 116  * in an isl_set, and
 117  * isl_sol_for, which calls a user-defined function for each part of
 118  * the solution.
 119  */
 120 struct isl_sol {
 121         int error;
 122         int max;
 123         int n_out;
 124         struct isl_context *context;
 125         void (*add)(struct isl_sol *sol,
 126                             struct isl_basic_set *dom, struct isl_mat *M);
 127         void (*add_empty)(struct isl_sol *sol, struct isl_basic_set *bset);
 128         void (*free)(struct isl_sol *sol);
 129 };
 130
 131 static void sol_free(struct isl_sol *sol)
 132 {
 133         if (!sol)
 134                 return;
 135         sol->free(sol);
 136 }
 137
 138 static void scale_rows(struct isl_mat *mat, isl_int m, int n_row)
 139 {
 140         int i;
 141
 142         if (isl_int_is_one(m))
 143                 return;
 144
 145         for (i = 0; i < n_row; ++i)
 146                 isl_seq_scale(mat->row[i], mat->row[i], m, mat->n_col);
 147 }
 148
 149 /* Add the solution identified by the tableau and the context tableau.
 150  *
 151  * The layout of the variables is as follows.
 152  *      tab->n_var is equal to the total number of variables in the input
 153  *                      map (including divs that were copied from the context)
 154  *                      + the number of extra divs constructed
 155  *      Of these, the first tab->n_param and the last tab->n_div variables
 156  *      correspond to the variables in the context, i.e.,
 157  *              tab->n_param + tab->n_div = context_tab->n_var
 158  *      tab->n_param is equal to the number of parameters and input
 159  *                      dimensions in the input map
 160  *      tab->n_div is equal to the number of divs in the context
 161  *
 162  * If there is no solution, then call add_empty with a basic set
 163  * that corresponds to the context tableau.  (If add_empty is NULL,
 164  * then do nothing).
 165  *
 166  * If there is a solution, then first construct a matrix that maps
 167  * all dimensions of the context to the output variables, i.e.,
 168  * the output dimensions in the input map.
 169  * The divs in the input map (if any) that do not correspond to any
 170  * div in the context do not appear in the solution.
 171  * The algorithm will make sure that they have an integer value,
 172  * but these values themselves are of no interest.
 173  * We have to be careful not to drop or rearrange any divs in the
 174  * context because that would change the meaning of the matrix.
 175  *
 176  * To extract the value of the output variables, it should be noted
 177  * that we always use a big parameter M in the main tableau and so
 178  * the variable stored in this tableau is not an output variable x itself, but
 179  *      x' = M + x (in case of minimization)
 180  * or
 181  *      x' = M - x (in case of maximization)
 182  * If x' appears in a column, then its optimal value is zero,
 183  * which means that the optimal value of x is an unbounded number
 184  * (-M for minimization and M for maximization).
 185  * We currently assume that the output dimensions in the original map
 186  * are bounded, so this cannot occur.
 187  * Similarly, when x' appears in a row, then the coefficient of M in that
 188  * row is necessarily 1.
 189  * If the row in the tableau represents
 190  *      d x' = c + d M + e(y)
 191  * then, in case of minimization, the corresponding row in the matrix
 192  * will be
 193  *      a c + a e(y)
 194  * with a d = m, the (updated) common denominator of the matrix.
 195  * In case of maximization, the row will be
 196  *      -a c - a e(y)
 197  */
 198 static void sol_add(struct isl_sol *sol, struct isl_tab *tab)
 199 {
 200         struct isl_basic_set *bset = NULL;
 201         struct isl_mat *mat = NULL;
 202         unsigned off;
 203         int row, i;
 204         isl_int m;
 205
 206         if (sol->error || !tab)
 207                 goto error;
 208
 209         if (tab->empty && !sol->add_empty)
 210                 return;
 211
 212         bset = isl_basic_set_dup(sol->context->op->peek_basic_set(sol->context));
 213         bset = isl_basic_set_update_from_tab(bset,
 214                         sol->context->op->peek_tab(sol->context));
 215         if (tab->rational)
 216                 ISL_F_SET(bset, ISL_BASIC_SET_RATIONAL);
 217
 218         if (tab->empty) {
 219                 sol->add_empty(sol, bset);
 220                 return;
 221         }
 222
 223         off = 2 + tab->M;
 224
 225         mat = isl_mat_alloc(tab->mat->ctx, 1 + sol->n_out,
 226                                             1 + tab->n_param + tab->n_div);
 227         if (!mat)
 228                 goto error;
 229
 230         isl_int_init(m);
 231
 232         isl_seq_clr(mat->row[0] + 1, mat->n_col - 1);
 233         isl_int_set_si(mat->row[0][0], 1);
 234         for (row = 0; row < sol->n_out; ++row) {
 235                 int i = tab->n_param + row;
 236                 int r, j;
 237
 238                 isl_seq_clr(mat->row[1 + row], mat->n_col);
 239                 if (!tab->var[i].is_row) {
 240                         /* no unbounded */
 241                         isl_assert(mat->ctx, !tab->M, goto error2);
 242                         continue;
 243                 }
 244
 245                 r = tab->var[i].index;
 246                 /* no unbounded */
 247                 if (tab->M)
 248                         isl_assert(mat->ctx, isl_int_eq(tab->mat->row[r][2],
 249                                                         tab->mat->row[r][0]),
 250                                     goto error2);
 251                 isl_int_gcd(m, mat->row[0][0], tab->mat->row[r][0]);
 252                 isl_int_divexact(m, tab->mat->row[r][0], m);
 253                 scale_rows(mat, m, 1 + row);
 254                 isl_int_divexact(m, mat->row[0][0], tab->mat->row[r][0]);
 255                 isl_int_mul(mat->row[1 + row][0], m, tab->mat->row[r][1]);
 256                 for (j = 0; j < tab->n_param; ++j) {
 257                         int col;
 258                         if (tab->var[j].is_row)
 259                                 continue;
 260                         col = tab->var[j].index;
 261                         isl_int_mul(mat->row[1 + row][1 + j], m,
 262                                     tab->mat->row[r][off + col]);
 263                 }
 264                 for (j = 0; j < tab->n_div; ++j) {
 265                         int col;
 266                         if (tab->var[tab->n_var - tab->n_div+j].is_row)
 267                                 continue;
 268                         col = tab->var[tab->n_var - tab->n_div+j].index;
 269                         isl_int_mul(mat->row[1 + row][1 + tab->n_param + j], m,
 270                                     tab->mat->row[r][off + col]);
 271                 }
 272                 if (sol->max)
 273                         isl_seq_neg(mat->row[1 + row], mat->row[1 + row],
 274                                     mat->n_col);
 275         }
 276
 277         isl_int_clear(m);
 278
 279         sol->add(sol, bset, mat);
 280         return;
 281 error2:
 282         isl_int_clear(m);
 283 error:
 284         isl_basic_set_free(bset);
 285         isl_mat_free(mat);
 286         sol_free(sol);
 287 }
 288
 289 struct isl_sol_map {
 290         struct isl_sol  sol;
 291         struct isl_map  *map;
 292         struct isl_set  *empty;
 293 };
 294
 295 static void sol_map_free(struct isl_sol_map *sol_map)
 296 {
 297         if (sol_map->sol.context)
 298                 sol_map->sol.context->op->free(sol_map->sol.context);
 299         isl_map_free(sol_map->map);
 300         isl_set_free(sol_map->empty);
 301         free(sol_map);
 302 }
 303
 304 static void sol_map_free_wrap(struct isl_sol *sol)
 305 {
 306         sol_map_free((struct isl_sol_map *)sol);
 307 }
 308
 309 /* This function is called for parts of the context where there is
 310  * no solution, with "bset" corresponding to the context tableau.
 311  * Simply add the basic set to the set "empty".
 312  */
 313 static void sol_map_add_empty(struct isl_sol_map *sol,
 314         struct isl_basic_set *bset)
 315 {
 316         if (!bset)
 317                 goto error;
 318         isl_assert(bset->ctx, sol->empty, goto error);
 319
 320         sol->empty = isl_set_grow(sol->empty, 1);
 321         bset = isl_basic_set_simplify(bset);
 322         bset = isl_basic_set_finalize(bset);
 323         sol->empty = isl_set_add(sol->empty, isl_basic_set_copy(bset));
 324         if (!sol->empty)
 325                 goto error;
 326         isl_basic_set_free(bset);
 327         return;
 328 error:
 329         isl_basic_set_free(bset);
 330         sol->sol.error = 1;
 331 }
 332
 333 static void sol_map_add_empty_wrap(struct isl_sol *sol,
 334         struct isl_basic_set *bset)
 335 {
 336         sol_map_add_empty((struct isl_sol_map *)sol, bset);
 337 }
 338
 339 /* Given a basic map "dom" that represents the context and an affine
 340  * matrix "M" that maps the dimensions of the context to the
 341  * output variables, construct a basic map with the same parameters
 342  * and divs as the context, the dimensions of the context as input
 343  * dimensions and a number of output dimensions that is equal to
 344  * the number of output dimensions in the input map.
 345  *
 346  * The constraints and divs of the context are simply copied
 347  * from "dom".  For each row
 348  *      x = c + e(y)
 349  * an equality
 350  *      c + e(y) - d x = 0
 351  * is added, with d the common denominator of M.
 352  */
 353 static void sol_map_add(struct isl_sol_map *sol,
 354         struct isl_basic_set *dom, struct isl_mat *M)
 355 {
 356         int i;
 357         struct isl_basic_map *bmap = NULL;
 358         isl_basic_set *context_bset;
 359         unsigned n_eq;
 360         unsigned n_ineq;
 361         unsigned nparam;
 362         unsigned total;
 363         unsigned n_div;
 364         unsigned n_out;
 365
 366         if (sol->sol.error || !dom || !M)
 367                 goto error;
 368
 369         n_out = sol->sol.n_out;
 370         n_eq = dom->n_eq + n_out;
 371         n_ineq = dom->n_ineq;
 372         n_div = dom->n_div;
 373         nparam = isl_basic_set_total_dim(dom) - n_div;
 374         total = isl_map_dim(sol->map, isl_dim_all);
 375         bmap = isl_basic_map_alloc_dim(isl_map_get_dim(sol->map),
 376                                         n_div, n_eq, 2 * n_div + n_ineq);
 377         if (!bmap)
 378                 goto error;
 379         if (ISL_F_ISSET(dom, ISL_BASIC_SET_RATIONAL))
 380                 ISL_F_SET(bmap, ISL_BASIC_MAP_RATIONAL);
 381         for (i = 0; i < dom->n_div; ++i) {
 382                 int k = isl_basic_map_alloc_div(bmap);
 383                 if (k < 0)
 384                         goto error;
 385                 isl_seq_cpy(bmap->div[k], dom->div[i], 1 + 1 + nparam);
 386                 isl_seq_clr(bmap->div[k] + 1 + 1 + nparam, total - nparam);
 387                 isl_seq_cpy(bmap->div[k] + 1 + 1 + total,
 388                             dom->div[i] + 1 + 1 + nparam, i);
 389         }
 390         for (i = 0; i < dom->n_eq; ++i) {
 391                 int k = isl_basic_map_alloc_equality(bmap);
 392                 if (k < 0)
 393                         goto error;
 394                 isl_seq_cpy(bmap->eq[k], dom->eq[i], 1 + nparam);
 395                 isl_seq_clr(bmap->eq[k] + 1 + nparam, total - nparam);
 396                 isl_seq_cpy(bmap->eq[k] + 1 + total,
 397                             dom->eq[i] + 1 + nparam, n_div);
 398         }
 399         for (i = 0; i < dom->n_ineq; ++i) {
 400                 int k = isl_basic_map_alloc_inequality(bmap);
 401                 if (k < 0)
 402                         goto error;
 403                 isl_seq_cpy(bmap->ineq[k], dom->ineq[i], 1 + nparam);
 404                 isl_seq_clr(bmap->ineq[k] + 1 + nparam, total - nparam);
 405                 isl_seq_cpy(bmap->ineq[k] + 1 + total,
 406                         dom->ineq[i] + 1 + nparam, n_div);
 407         }
 408         for (i = 0; i < M->n_row - 1; ++i) {
 409                 int k = isl_basic_map_alloc_equality(bmap);
 410                 if (k < 0)
 411                         goto error;
 412                 isl_seq_cpy(bmap->eq[k], M->row[1 + i], 1 + nparam);
 413                 isl_seq_clr(bmap->eq[k] + 1 + nparam, n_out);
 414                 isl_int_neg(bmap->eq[k][1 + nparam + i], M->row[0][0]);
 415                 isl_seq_cpy(bmap->eq[k] + 1 + nparam + n_out,
 416                             M->row[1 + i] + 1 + nparam, n_div);
 417         }
 418         bmap = isl_basic_map_simplify(bmap);
 419         bmap = isl_basic_map_finalize(bmap);
 420         sol->map = isl_map_grow(sol->map, 1);
 421         sol->map = isl_map_add(sol->map, bmap);
 422         if (!sol->map)
 423                 goto error;
 424         isl_basic_set_free(dom);
 425         isl_mat_free(M);
 426         return;
 427 error:
 428         isl_basic_set_free(dom);
 429         isl_mat_free(M);
 430         isl_basic_map_free(bmap);
 431         sol->sol.error = 1;
 432 }
 433
 434 static void sol_map_add_wrap(struct isl_sol *sol,
 435         struct isl_basic_set *dom, struct isl_mat *M)
 436 {
 437         sol_map_add((struct isl_sol_map *)sol, dom, M);
 438 }
 439
 440
 441 /* Store the "parametric constant" of row "row" of tableau "tab" in "line",
 442  * i.e., the constant term and the coefficients of all variables that
 443  * appear in the context tableau.
 444  * Note that the coefficient of the big parameter M is NOT copied.
 445  * The context tableau may not have a big parameter and even when it
 446  * does, it is a different big parameter.
 447  */
 448 static void get_row_parameter_line(struct isl_tab *tab, int row, isl_int *line)
 449 {
 450         int i;
 451         unsigned off = 2 + tab->M;
 452
 453         isl_int_set(line[0], tab->mat->row[row][1]);
 454         for (i = 0; i < tab->n_param; ++i) {
 455                 if (tab->var[i].is_row)
 456                         isl_int_set_si(line[1 + i], 0);
 457                 else {
 458                         int col = tab->var[i].index;
 459                         isl_int_set(line[1 + i], tab->mat->row[row][off + col]);
 460                 }
 461         }
 462         for (i = 0; i < tab->n_div; ++i) {
 463                 if (tab->var[tab->n_var - tab->n_div + i].is_row)
 464                         isl_int_set_si(line[1 + tab->n_param + i], 0);
 465                 else {
 466                         int col = tab->var[tab->n_var - tab->n_div + i].index;
 467                         isl_int_set(line[1 + tab->n_param + i],
 468                                     tab->mat->row[row][off + col]);
 469                 }
 470         }
 471 }
 472
 473 /* Check if rows "row1" and "row2" have identical "parametric constants",
 474  * as explained above.
 475  * In this case, we also insist that the coefficients of the big parameter
 476  * be the same as the values of the constants will only be the same
 477  * if these coefficients are also the same.
 478  */
 479 static int identical_parameter_line(struct isl_tab *tab, int row1, int row2)
 480 {
 481         int i;
 482         unsigned off = 2 + tab->M;
 483
 484         if (isl_int_ne(tab->mat->row[row1][1], tab->mat->row[row2][1]))
 485                 return 0;
 486
 487         if (tab->M && isl_int_ne(tab->mat->row[row1][2],
 488                                  tab->mat->row[row2][2]))
 489                 return 0;
 490
 491         for (i = 0; i < tab->n_param + tab->n_div; ++i) {
 492                 int pos = i < tab->n_param ? i :
 493                         tab->n_var - tab->n_div + i - tab->n_param;
 494                 int col;
 495
 496                 if (tab->var[pos].is_row)
 497                         continue;
 498                 col = tab->var[pos].index;
 499                 if (isl_int_ne(tab->mat->row[row1][off + col],
 500                                tab->mat->row[row2][off + col]))
 501                         return 0;
 502         }
 503         return 1;
 504 }
 505
 506 /* Return an inequality that expresses that the "parametric constant"
 507  * should be non-negative.
 508  * This function is only called when the coefficient of the big parameter
 509  * is equal to zero.
 510  */
 511 static struct isl_vec *get_row_parameter_ineq(struct isl_tab *tab, int row)
 512 {
 513         struct isl_vec *ineq;
 514
 515         ineq = isl_vec_alloc(tab->mat->ctx, 1 + tab->n_param + tab->n_div);
 516         if (!ineq)
 517                 return NULL;
 518
 519         get_row_parameter_line(tab, row, ineq->el);
 520         if (ineq)
 521                 ineq = isl_vec_normalize(ineq);
 522
 523         return ineq;
 524 }
 525
 526 /* Return a integer division for use in a parametric cut based on the given row.
 527  * In particular, let the parametric constant of the row be
 528  *
 529  *              \sum_i a_i y_i
 530  *
 531  * where y_0 = 1, but none of the y_i corresponds to the big parameter M.
 532  * The div returned is equal to
 533  *
 534  *              floor(\sum_i {-a_i} y_i) = floor((\sum_i (-a_i mod d) y_i)/d)
 535  */
 536 static struct isl_vec *get_row_parameter_div(struct isl_tab *tab, int row)
 537 {
 538         struct isl_vec *div;
 539
 540         div = isl_vec_alloc(tab->mat->ctx, 1 + 1 + tab->n_param + tab->n_div);
 541         if (!div)
 542                 return NULL;
 543
 544         isl_int_set(div->el[0], tab->mat->row[row][0]);
 545         get_row_parameter_line(tab, row, div->el + 1);
 546         div = isl_vec_normalize(div);
 547         isl_seq_neg(div->el + 1, div->el + 1, div->size - 1);
 548         isl_seq_fdiv_r(div->el + 1, div->el + 1, div->el[0], div->size - 1);
 549
 550         return div;
 551 }
 552
 553 /* Return a integer division for use in transferring an integrality constraint
 554  * to the context.
 555  * In particular, let the parametric constant of the row be
 556  *
 557  *              \sum_i a_i y_i
 558  *
 559  * where y_0 = 1, but none of the y_i corresponds to the big parameter M.
 560  * The the returned div is equal to
 561  *
 562  *              floor(\sum_i {a_i} y_i) = floor((\sum_i (a_i mod d) y_i)/d)
 563  */
 564 static struct isl_vec *get_row_split_div(struct isl_tab *tab, int row)
 565 {
 566         struct isl_vec *div;
 567
 568         div = isl_vec_alloc(tab->mat->ctx, 1 + 1 + tab->n_param + tab->n_div);
 569         if (!div)
 570                 return NULL;
 571
 572         isl_int_set(div->el[0], tab->mat->row[row][0]);
 573         get_row_parameter_line(tab, row, div->el + 1);
 574         div = isl_vec_normalize(div);
 575         isl_seq_fdiv_r(div->el + 1, div->el + 1, div->el[0], div->size - 1);
 576
 577         return div;
 578 }
 579
 580 /* Construct and return an inequality that expresses an upper bound
 581  * on the given div.
 582  * In particular, if the div is given by
 583  *
 584  *      d = floor(e/m)
 585  *
 586  * then the inequality expresses
 587  *
 588  *      m d <= e
 589  */
 590 static struct isl_vec *ineq_for_div(struct isl_basic_set *bset, unsigned div)
 591 {
 592         unsigned total;
 593         unsigned div_pos;
 594         struct isl_vec *ineq;
 595
 596         if (!bset)
 597                 return NULL;
 598
 599         total = isl_basic_set_total_dim(bset);
 600         div_pos = 1 + total - bset->n_div + div;
 601
 602         ineq = isl_vec_alloc(bset->ctx, 1 + total);
 603         if (!ineq)
 604                 return NULL;
 605
 606         isl_seq_cpy(ineq->el, bset->div[div] + 1, 1 + total);
 607         isl_int_neg(ineq->el[div_pos], bset->div[div][0]);
 608         return ineq;
 609 }
 610
 611 /* Given a row in the tableau and a div that was created
 612  * using get_row_split_div and that been constrained to equality, i.e.,
 613  *
 614  *              d = floor(\sum_i {a_i} y_i) = \sum_i {a_i} y_i
 615  *
 616  * replace the expression "\sum_i {a_i} y_i" in the row by d,
 617  * i.e., we subtract "\sum_i {a_i} y_i" and add 1 d.
 618  * The coefficients of the non-parameters in the tableau have been
 619  * verified to be integral.  We can therefore simply replace coefficient b
 620  * by floor(b).  For the coefficients of the parameters we have
 621  * floor(a_i) = a_i - {a_i}, while for the other coefficients, we have
 622  * floor(b) = b.
 623  */
 624 static struct isl_tab *set_row_cst_to_div(struct isl_tab *tab, int row, int div)
 625 {
 626         isl_seq_fdiv_q(tab->mat->row[row] + 1, tab->mat->row[row] + 1,
 627                         tab->mat->row[row][0], 1 + tab->M + tab->n_col);
 628
 629         isl_int_set_si(tab->mat->row[row][0], 1);
 630
 631         if (tab->var[tab->n_var - tab->n_div + div].is_row) {
 632                 int drow = tab->var[tab->n_var - tab->n_div + div].index;
 633
 634                 isl_assert(tab->mat->ctx,
 635                         isl_int_is_one(tab->mat->row[drow][0]), goto error);
 636                 isl_seq_combine(tab->mat->row[row] + 1,
 637                         tab->mat->ctx->one, tab->mat->row[row] + 1,
 638                         tab->mat->ctx->one, tab->mat->row[drow] + 1,
 639                         1 + tab->M + tab->n_col);
 640         } else {
 641                 int dcol = tab->var[tab->n_var - tab->n_div + div].index;
 642
 643                 isl_int_set_si(tab->mat->row[row][2 + tab->M + dcol], 1);
 644         }
 645
 646         return tab;
 647 error:
 648         isl_tab_free(tab);
 649         return NULL;
 650 }
 651
 652 /* Check if the (parametric) constant of the given row is obviously
 653  * negative, meaning that we don't need to consult the context tableau.
 654  * If there is a big parameter and its coefficient is non-zero,
 655  * then this coefficient determines the outcome.
 656  * Otherwise, we check whether the constant is negative and
 657  * all non-zero coefficients of parameters are negative and
 658  * belong to non-negative parameters.
 659  */
 660 static int is_obviously_neg(struct isl_tab *tab, int row)
 661 {
 662         int i;
 663         int col;
 664         unsigned off = 2 + tab->M;
 665
 666         if (tab->M) {
 667                 if (isl_int_is_pos(tab->mat->row[row][2]))
 668                         return 0;
 669                 if (isl_int_is_neg(tab->mat->row[row][2]))
 670                         return 1;
 671         }
 672
 673         if (isl_int_is_nonneg(tab->mat->row[row][1]))
 674                 return 0;
 675         for (i = 0; i < tab->n_param; ++i) {
 676                 /* Eliminated parameter */
 677                 if (tab->var[i].is_row)
 678                         continue;
 679                 col = tab->var[i].index;
 680                 if (isl_int_is_zero(tab->mat->row[row][off + col]))
 681                         continue;
 682                 if (!tab->var[i].is_nonneg)
 683                         return 0;
 684                 if (isl_int_is_pos(tab->mat->row[row][off + col]))
 685                         return 0;
 686         }
 687         for (i = 0; i < tab->n_div; ++i) {
 688                 if (tab->var[tab->n_var - tab->n_div + i].is_row)
 689                         continue;
 690                 col = tab->var[tab->n_var - tab->n_div + i].index;
 691                 if (isl_int_is_zero(tab->mat->row[row][off + col]))
 692                         continue;
 693                 if (!tab->var[tab->n_var - tab->n_div + i].is_nonneg)
 694                         return 0;
 695                 if (isl_int_is_pos(tab->mat->row[row][off + col]))
 696                         return 0;
 697         }
 698         return 1;
 699 }
 700
 701 /* Check if the (parametric) constant of the given row is obviously
 702  * non-negative, meaning that we don't need to consult the context tableau.
 703  * If there is a big parameter and its coefficient is non-zero,
 704  * then this coefficient determines the outcome.
 705  * Otherwise, we check whether the constant is non-negative and
 706  * all non-zero coefficients of parameters are positive and
 707  * belong to non-negative parameters.
 708  */
 709 static int is_obviously_nonneg(struct isl_tab *tab, int row)
 710 {
 711         int i;
 712         int col;
 713         unsigned off = 2 + tab->M;
 714
 715         if (tab->M) {
 716                 if (isl_int_is_pos(tab->mat->row[row][2]))
 717                         return 1;
 718                 if (isl_int_is_neg(tab->mat->row[row][2]))
 719                         return 0;
 720         }
 721
 722         if (isl_int_is_neg(tab->mat->row[row][1]))
 723                 return 0;
 724         for (i = 0; i < tab->n_param; ++i) {
 725                 /* Eliminated parameter */
 726                 if (tab->var[i].is_row)
 727                         continue;
 728                 col = tab->var[i].index;
 729                 if (isl_int_is_zero(tab->mat->row[row][off + col]))
 730                         continue;
 731                 if (!tab->var[i].is_nonneg)
 732                         return 0;
 733                 if (isl_int_is_neg(tab->mat->row[row][off + col]))
 734                         return 0;
 735         }
 736         for (i = 0; i < tab->n_div; ++i) {
 737                 if (tab->var[tab->n_var - tab->n_div + i].is_row)
 738                         continue;
 739                 col = tab->var[tab->n_var - tab->n_div + i].index;
 740                 if (isl_int_is_zero(tab->mat->row[row][off + col]))
 741                         continue;
 742                 if (!tab->var[tab->n_var - tab->n_div + i].is_nonneg)
 743                         return 0;
 744                 if (isl_int_is_neg(tab->mat->row[row][off + col]))
 745                         return 0;
 746         }
 747         return 1;
 748 }
 749
 750 /* Given a row r and two columns, return the column that would
 751  * lead to the lexicographically smallest increment in the sample
 752  * solution when leaving the basis in favor of the row.
 753  * Pivoting with column c will increment the sample value by a non-negative
 754  * constant times a_{V,c}/a_{r,c}, with a_{V,c} the elements of column c
 755  * corresponding to the non-parametric variables.
 756  * If variable v appears in a column c_v, the a_{v,c} = 1 iff c = c_v,
 757  * with all other entries in this virtual row equal to zero.
 758  * If variable v appears in a row, then a_{v,c} is the element in column c
 759  * of that row.
 760  *
 761  * Let v be the first variable with a_{v,c1}/a_{r,c1} != a_{v,c2}/a_{r,c2}.
 762  * Then if a_{v,c1}/a_{r,c1} < a_{v,c2}/a_{r,c2}, i.e.,
 763  * a_{v,c2} a_{r,c1} - a_{v,c1} a_{r,c2} > 0, c1 results in the minimal
 764  * increment.  Otherwise, it's c2.
 765  */
 766 static int lexmin_col_pair(struct isl_tab *tab,
 767         int row, int col1, int col2, isl_int tmp)
 768 {
 769         int i;
 770         isl_int *tr;
 771
 772         tr = tab->mat->row[row] + 2 + tab->M;
 773
 774         for (i = tab->n_param; i < tab->n_var - tab->n_div; ++i) {
 775                 int s1, s2;
 776                 isl_int *r;
 777
 778                 if (!tab->var[i].is_row) {
 779                         if (tab->var[i].index == col1)
 780                                 return col2;
 781                         if (tab->var[i].index == col2)
 782                                 return col1;
 783                         continue;
 784                 }
 785
 786                 if (tab->var[i].index == row)
 787                         continue;
 788
 789                 r = tab->mat->row[tab->var[i].index] + 2 + tab->M;
 790                 s1 = isl_int_sgn(r[col1]);
 791                 s2 = isl_int_sgn(r[col2]);
 792                 if (s1 == 0 && s2 == 0)
 793                         continue;
 794                 if (s1 < s2)
 795                         return col1;
 796                 if (s2 < s1)
 797                         return col2;
 798
 799                 isl_int_mul(tmp, r[col2], tr[col1]);
 800                 isl_int_submul(tmp, r[col1], tr[col2]);
 801                 if (isl_int_is_pos(tmp))
 802                         return col1;
 803                 if (isl_int_is_neg(tmp))
 804                         return col2;
 805         }
 806         return -1;
 807 }
 808
 809 /* Given a row in the tableau, find and return the column that would
 810  * result in the lexicographically smallest, but positive, increment
 811  * in the sample point.
 812  * If there is no such column, then return tab->n_col.
 813  * If anything goes wrong, return -1.
 814  */
 815 static int lexmin_pivot_col(struct isl_tab *tab, int row)
 816 {
 817         int j;
 818         int col = tab->n_col;
 819         isl_int *tr;
 820         isl_int tmp;
 821
 822         tr = tab->mat->row[row] + 2 + tab->M;
 823
 824         isl_int_init(tmp);
 825
 826         for (j = tab->n_dead; j < tab->n_col; ++j) {
 827                 if (tab->col_var[j] >= 0 &&
 828                     (tab->col_var[j] < tab->n_param  ||
 829                     tab->col_var[j] >= tab->n_var - tab->n_div))
 830                         continue;
 831
 832                 if (!isl_int_is_pos(tr[j]))
 833                         continue;
 834
 835                 if (col == tab->n_col)
 836                         col = j;
 837                 else
 838                         col = lexmin_col_pair(tab, row, col, j, tmp);
 839                 isl_assert(tab->mat->ctx, col >= 0, goto error);
 840         }
 841
 842         isl_int_clear(tmp);
 843         return col;
 844 error:
 845         isl_int_clear(tmp);
 846         return -1;
 847 }
 848
 849 /* Return the first known violated constraint, i.e., a non-negative
 850  * contraint that currently has an either obviously negative value
 851  * or a previously determined to be negative value.
 852  *
 853  * If any constraint has a negative coefficient for the big parameter,
 854  * if any, then we return one of these first.
 855  */
 856 static int first_neg(struct isl_tab *tab)
 857 {
 858         int row;
 859
 860         if (tab->M)
 861                 for (row = tab->n_redundant; row < tab->n_row; ++row) {
 862                         if (!isl_tab_var_from_row(tab, row)->is_nonneg)
 863                                 continue;
 864                         if (isl_int_is_neg(tab->mat->row[row][2]))
 865                                 return row;
 866                 }
 867         for (row = tab->n_redundant; row < tab->n_row; ++row) {
 868                 if (!isl_tab_var_from_row(tab, row)->is_nonneg)
 869                         continue;
 870                 if (tab->row_sign) {
 871                         if (tab->row_sign[row] == 0 &&
 872                             is_obviously_neg(tab, row))
 873                                 tab->row_sign[row] = isl_tab_row_neg;
 874                         if (tab->row_sign[row] != isl_tab_row_neg)
 875                                 continue;
 876                 } else if (!is_obviously_neg(tab, row))
 877                         continue;
 878                 return row;
 879         }
 880         return -1;
 881 }
 882
 883 /* Resolve all known or obviously violated constraints through pivoting.
 884  * In particular, as long as we can find any violated constraint, we
 885  * look for a pivoting column that would result in the lexicographicallly
 886  * smallest increment in the sample point.  If there is no such column
 887  * then the tableau is infeasible.
 888  */
 889 static struct isl_tab *restore_lexmin(struct isl_tab *tab) WARN_UNUSED;
 890 static struct isl_tab *restore_lexmin(struct isl_tab *tab)
 891 {
 892         int row, col;
 893
 894         if (!tab)
 895                 return NULL;
 896         if (tab->empty)
 897                 return tab;
 898         while ((row = first_neg(tab)) != -1) {
 899                 col = lexmin_pivot_col(tab, row);
 900                 if (col >= tab->n_col)
 901                         return isl_tab_mark_empty(tab);
 902                 if (col < 0)
 903                         goto error;
 904                 if (isl_tab_pivot(tab, row, col) < 0)
 905                         goto error;
 906         }
 907         return tab;
 908 error:
 909         isl_tab_free(tab);
 910         return NULL;
 911 }
 912
 913 /* Given a row that represents an equality, look for an appropriate
 914  * pivoting column.
 915  * In particular, if there are any non-zero coefficients among
 916  * the non-parameter variables, then we take the last of these
 917  * variables.  Eliminating this variable in terms of the other
 918  * variables and/or parameters does not influence the property
 919  * that all column in the initial tableau are lexicographically
 920  * positive.  The row corresponding to the eliminated variable
 921  * will only have non-zero entries below the diagonal of the
 922  * initial tableau.  That is, we transform
 923  *
 924  *              I                               I
 925  *                1             into            a
 926  *                  I                             I
 927  *
 928  * If there is no such non-parameter variable, then we are dealing with
 929  * pure parameter equality and we pick any parameter with coefficient 1 or -1
 930  * for elimination.  This will ensure that the eliminated parameter
 931  * always has an integer value whenever all the other parameters are integral.
 932  * If there is no such parameter then we return -1.
 933  */
 934 static int last_var_col_or_int_par_col(struct isl_tab *tab, int row)
 935 {
 936         unsigned off = 2 + tab->M;
 937         int i;
 938
 939         for (i = tab->n_var - tab->n_div - 1; i >= 0 && i >= tab->n_param; --i) {
 940                 int col;
 941                 if (tab->var[i].is_row)
 942                         continue;
 943                 col = tab->var[i].index;
 944                 if (col <= tab->n_dead)
 945                         continue;
 946                 if (!isl_int_is_zero(tab->mat->row[row][off + col]))
 947                         return col;
 948         }
 949         for (i = tab->n_dead; i < tab->n_col; ++i) {
 950                 if (isl_int_is_one(tab->mat->row[row][off + i]))
 951                         return i;
 952                 if (isl_int_is_negone(tab->mat->row[row][off + i]))
 953                         return i;
 954         }
 955         return -1;
 956 }
 957
 958 /* Add an equality that is known to be valid to the tableau.
 959  * We first check if we can eliminate a variable or a parameter.
 960  * If not, we add the equality as two inequalities.
 961  * In this case, the equality was a pure parameter equality and there
 962  * is no need to resolve any constraint violations.
 963  */
 964 static struct isl_tab *add_lexmin_valid_eq(struct isl_tab *tab, isl_int *eq)
 965 {
 966         int i;
 967         int r;
 968
 969         if (!tab)
 970                 return NULL;
 971         r = isl_tab_add_row(tab, eq);
 972         if (r < 0)
 973                 goto error;
 974
 975         r = tab->con[r].index;
 976         i = last_var_col_or_int_par_col(tab, r);
 977         if (i < 0) {
 978                 tab->con[r].is_nonneg = 1;
 979                 if (isl_tab_push_var(tab, isl_tab_undo_nonneg, &tab->con[r]) < 0)
 980                         goto error;
 981                 isl_seq_neg(eq, eq, 1 + tab->n_var);
 982                 r = isl_tab_add_row(tab, eq);
 983                 if (r < 0)
 984                         goto error;
 985                 tab->con[r].is_nonneg = 1;
 986                 if (isl_tab_push_var(tab, isl_tab_undo_nonneg, &tab->con[r]) < 0)
 987                         goto error;
 988         } else {
 989                 if (isl_tab_pivot(tab, r, i) < 0)
 990                         goto error;
 991                 if (isl_tab_kill_col(tab, i) < 0)
 992                         goto error;
 993                 tab->n_eq++;
 994
 995                 tab = restore_lexmin(tab);
 996         }
 997
 998         return tab;
 999 error:
1000         isl_tab_free(tab);
1001         return NULL;
1002 }
1003
1004 /* Check if the given row is a pure constant.
1005  */
1006 static int is_constant(struct isl_tab *tab, int row)
1007 {
1008         unsigned off = 2 + tab->M;
1009
1010         return isl_seq_first_non_zero(tab->mat->row[row] + off + tab->n_dead,
1011                                         tab->n_col - tab->n_dead) == -1;
1012 }
1013
1014 /* Add an equality that may or may not be valid to the tableau.
1015  * If the resulting row is a pure constant, then it must be zero.
1016  * Otherwise, the resulting tableau is empty.
1017  *
1018  * If the row is not a pure constant, then we add two inequalities,
1019  * each time checking that they can be satisfied.
1020  * In the end we try to use one of the two constraints to eliminate
1021  * a column.
1022  */
1023 static struct isl_tab *add_lexmin_eq(struct isl_tab *tab, isl_int *eq) WARN_UNUSED;
1024 static struct isl_tab *add_lexmin_eq(struct isl_tab *tab, isl_int *eq)
1025 {
1026         int r1, r2;
1027         int row;
1028         struct isl_tab_undo *snap;
1029
1030         if (!tab)
1031                 return NULL;
1032         snap = isl_tab_snap(tab);
1033         r1 = isl_tab_add_row(tab, eq);
1034         if (r1 < 0)
1035                 goto error;
1036         tab->con[r1].is_nonneg = 1;
1037         if (isl_tab_push_var(tab, isl_tab_undo_nonneg, &tab->con[r1]) < 0)
1038                 goto error;
1039
1040         row = tab->con[r1].index;
1041         if (is_constant(tab, row)) {
1042                 if (!isl_int_is_zero(tab->mat->row[row][1]) ||
1043                     (tab->M && !isl_int_is_zero(tab->mat->row[row][2])))
1044                         return isl_tab_mark_empty(tab);
1045                 if (isl_tab_rollback(tab, snap) < 0)
1046                         goto error;
1047                 return tab;
1048         }
1049
1050         tab = restore_lexmin(tab);
1051         if (!tab || tab->empty)
1052                 return tab;
1053
1054         isl_seq_neg(eq, eq, 1 + tab->n_var);
1055
1056         r2 = isl_tab_add_row(tab, eq);
1057         if (r2 < 0)
1058                 goto error;
1059         tab->con[r2].is_nonneg = 1;
1060         if (isl_tab_push_var(tab, isl_tab_undo_nonneg, &tab->con[r2]) < 0)
1061                 goto error;
1062
1063         tab = restore_lexmin(tab);
1064         if (!tab || tab->empty)
1065                 return tab;
1066
1067         if (!tab->con[r1].is_row) {
1068                 if (isl_tab_kill_col(tab, tab->con[r1].index) < 0)
1069                         goto error;
1070         } else if (!tab->con[r2].is_row) {
1071                 if (isl_tab_kill_col(tab, tab->con[r2].index) < 0)
1072                         goto error;
1073         } else if (isl_int_is_zero(tab->mat->row[tab->con[r1].index][1])) {
1074                 unsigned off = 2 + tab->M;
1075                 int i;
1076                 int row = tab->con[r1].index;
1077                 i = isl_seq_first_non_zero(tab->mat->row[row]+off+tab->n_dead,
1078                                                 tab->n_col - tab->n_dead);
1079                 if (i != -1) {
1080                         if (isl_tab_pivot(tab, row, tab->n_dead + i) < 0)
1081                                 goto error;
1082                         if (isl_tab_kill_col(tab, tab->n_dead + i) < 0)
1083                                 goto error;
1084                 }
1085         }
1086
1087         if (tab->bset) {
1088                 tab->bset = isl_basic_set_add_ineq(tab->bset, eq);
1089                 if (isl_tab_push(tab, isl_tab_undo_bset_ineq) < 0)
1090                         goto error;
1091                 isl_seq_neg(eq, eq, 1 + tab->n_var);
1092                 tab->bset = isl_basic_set_add_ineq(tab->bset, eq);
1093                 isl_seq_neg(eq, eq, 1 + tab->n_var);
1094                 if (isl_tab_push(tab, isl_tab_undo_bset_ineq) < 0)
1095                         goto error;
1096                 if (!tab->bset)
1097                         goto error;
1098         }
1099
1100         return tab;
1101 error:
1102         isl_tab_free(tab);
1103         return NULL;
1104 }
1105
1106 /* Add an inequality to the tableau, resolving violations using
1107  * restore_lexmin.
1108  */
1109 static struct isl_tab *add_lexmin_ineq(struct isl_tab *tab, isl_int *ineq)
1110 {
1111         int r;
1112
1113         if (!tab)
1114                 return NULL;
1115         if (tab->bset) {
1116                 tab->bset = isl_basic_set_add_ineq(tab->bset, ineq);
1117                 if (isl_tab_push(tab, isl_tab_undo_bset_ineq) < 0)
1118                         goto error;
1119                 if (!tab->bset)
1120                         goto error;
1121         }
1122         r = isl_tab_add_row(tab, ineq);
1123         if (r < 0)
1124                 goto error;
1125         tab->con[r].is_nonneg = 1;
1126         if (isl_tab_push_var(tab, isl_tab_undo_nonneg, &tab->con[r]) < 0)
1127                 goto error;
1128         if (isl_tab_row_is_redundant(tab, tab->con[r].index)) {
1129                 if (isl_tab_mark_redundant(tab, tab->con[r].index) < 0)
1130                         goto error;
1131                 return tab;
1132         }
1133
1134         tab = restore_lexmin(tab);
1135         if (tab && !tab->empty && tab->con[r].is_row &&
1136                  isl_tab_row_is_redundant(tab, tab->con[r].index))
1137                 if (isl_tab_mark_redundant(tab, tab->con[r].index) < 0)
1138                         goto error;
1139         return tab;
1140 error:
1141         isl_tab_free(tab);
1142         return NULL;
1143 }
1144
1145 /* Check if the coefficients of the parameters are all integral.
1146  */
1147 static int integer_parameter(struct isl_tab *tab, int row)
1148 {
1149         int i;
1150         int col;
1151         unsigned off = 2 + tab->M;
1152
1153         for (i = 0; i < tab->n_param; ++i) {
1154                 /* Eliminated parameter */
1155                 if (tab->var[i].is_row)
1156                         continue;
1157                 col = tab->var[i].index;
1158                 if (!isl_int_is_divisible_by(tab->mat->row[row][off + col],
1159                                                 tab->mat->row[row][0]))
1160                         return 0;
1161         }
1162         for (i = 0; i < tab->n_div; ++i) {
1163                 if (tab->var[tab->n_var - tab->n_div + i].is_row)
1164                         continue;
1165                 col = tab->var[tab->n_var - tab->n_div + i].index;
1166                 if (!isl_int_is_divisible_by(tab->mat->row[row][off + col],
1167                                                 tab->mat->row[row][0]))
1168                         return 0;
1169         }
1170         return 1;
1171 }
1172
1173 /* Check if the coefficients of the non-parameter variables are all integral.
1174  */
1175 static int integer_variable(struct isl_tab *tab, int row)
1176 {
1177         int i;
1178         unsigned off = 2 + tab->M;
1179
1180         for (i = 0; i < tab->n_col; ++i) {
1181                 if (tab->col_var[i] >= 0 &&
1182                     (tab->col_var[i] < tab->n_param ||
1183                      tab->col_var[i] >= tab->n_var - tab->n_div))
1184                         continue;
1185                 if (!isl_int_is_divisible_by(tab->mat->row[row][off + i],
1186                                                 tab->mat->row[row][0]))
1187                         return 0;
1188         }
1189         return 1;
1190 }
1191
1192 /* Check if the constant term is integral.
1193  */
1194 static int integer_constant(struct isl_tab *tab, int row)
1195 {
1196         return isl_int_is_divisible_by(tab->mat->row[row][1],
1197                                         tab->mat->row[row][0]);
1198 }
1199
1200 #define I_CST   1 << 0
1201 #define I_PAR   1 << 1
1202 #define I_VAR   1 << 2
1203
1204 /* Check for first (non-parameter) variable that is non-integer and
1205  * therefore requires a cut.
1206  * For parametric tableaus, there are three parts in a row,
1207  * the constant, the coefficients of the parameters and the rest.
1208  * For each part, we check whether the coefficients in that part
1209  * are all integral and if so, set the corresponding flag in *f.
1210  * If the constant and the parameter part are integral, then the
1211  * current sample value is integral and no cut is required
1212  * (irrespective of whether the variable part is integral).
1213  */
1214 static int first_non_integer(struct isl_tab *tab, int *f)
1215 {
1216         int i;
1217
1218         for (i = tab->n_param; i < tab->n_var - tab->n_div; ++i) {
1219                 int flags = 0;
1220                 int row;
1221                 if (!tab->var[i].is_row)
1222                         continue;
1223                 row = tab->var[i].index;
1224                 if (integer_constant(tab, row))
1225                         ISL_FL_SET(flags, I_CST);
1226                 if (integer_parameter(tab, row))
1227                         ISL_FL_SET(flags, I_PAR);
1228                 if (ISL_FL_ISSET(flags, I_CST) && ISL_FL_ISSET(flags, I_PAR))
1229                         continue;
1230                 if (integer_variable(tab, row))
1231                         ISL_FL_SET(flags, I_VAR);
1232                 *f = flags;
1233                 return row;
1234         }
1235         return -1;
1236 }
1237
1238 /* Add a (non-parametric) cut to cut away the non-integral sample
1239  * value of the given row.
1240  *
1241  * If the row is given by
1242  *
1243  *      m r = f + \sum_i a_i y_i
1244  *
1245  * then the cut is
1246  *
1247  *      c = - {-f/m} + \sum_i {a_i/m} y_i >= 0
1248  *
1249  * The big parameter, if any, is ignored, since it is assumed to be big
1250  * enough to be divisible by any integer.
1251  * If the tableau is actually a parametric tableau, then this function
1252  * is only called when all coefficients of the parameters are integral.
1253  * The cut therefore has zero coefficients for the parameters.
1254  *
1255  * The current value is known to be negative, so row_sign, if it
1256  * exists, is set accordingly.
1257  *
1258  * Return the row of the cut or -1.
1259  */
1260 static int add_cut(struct isl_tab *tab, int row)
1261 {
1262         int i;
1263         int r;
1264         isl_int *r_row;
1265         unsigned off = 2 + tab->M;
1266
1267         if (isl_tab_extend_cons(tab, 1) < 0)
1268                 return -1;
1269         r = isl_tab_allocate_con(tab);
1270         if (r < 0)
1271                 return -1;
1272
1273         r_row = tab->mat->row[tab->con[r].index];
1274         isl_int_set(r_row[0], tab->mat->row[row][0]);
1275         isl_int_neg(r_row[1], tab->mat->row[row][1]);
1276         isl_int_fdiv_r(r_row[1], r_row[1], tab->mat->row[row][0]);
1277         isl_int_neg(r_row[1], r_row[1]);
1278         if (tab->M)
1279                 isl_int_set_si(r_row[2], 0);
1280         for (i = 0; i < tab->n_col; ++i)
1281                 isl_int_fdiv_r(r_row[off + i],
1282                         tab->mat->row[row][off + i], tab->mat->row[row][0]);
1283
1284         tab->con[r].is_nonneg = 1;
1285         if (isl_tab_push_var(tab, isl_tab_undo_nonneg, &tab->con[r]) < 0)
1286                 return -1;
1287         if (tab->row_sign)
1288                 tab->row_sign[tab->con[r].index] = isl_tab_row_neg;
1289
1290         return tab->con[r].index;
1291 }
1292
1293 /* Given a non-parametric tableau, add cuts until an integer
1294  * sample point is obtained or until the tableau is determined
1295  * to be integer infeasible.
1296  * As long as there is any non-integer value in the sample point,
1297  * we add an appropriate cut, if possible and resolve the violated
1298  * cut constraint using restore_lexmin.
1299  * If one of the corresponding rows is equal to an integral
1300  * combination of variables/constraints plus a non-integral constant,
1301  * then there is no way to obtain an integer point an we return
1302  * a tableau that is marked empty.
1303  */
1304 static struct isl_tab *cut_to_integer_lexmin(struct isl_tab *tab)
1305 {
1306         int row;
1307         int flags;
1308
1309         if (!tab)
1310                 return NULL;
1311         if (tab->empty)
1312                 return tab;
1313
1314         while ((row = first_non_integer(tab, &flags)) != -1) {
1315                 if (ISL_FL_ISSET(flags, I_VAR))
1316                         return isl_tab_mark_empty(tab);
1317                 row = add_cut(tab, row);
1318                 if (row < 0)
1319                         goto error;
1320                 tab = restore_lexmin(tab);
1321                 if (!tab || tab->empty)
1322                         break;
1323         }
1324         return tab;
1325 error:
1326         isl_tab_free(tab);
1327         return NULL;
1328 }
1329
1330 /* Check whether all the currently active samples also satisfy the inequality
1331  * "ineq" (treated as an equality if eq is set).
1332  * Remove those samples that do not.
1333  */
1334 static struct isl_tab *check_samples(struct isl_tab *tab, isl_int *ineq, int eq)
1335 {
1336         int i;
1337         isl_int v;
1338
1339         if (!tab)
1340                 return NULL;
1341
1342         isl_assert(tab->mat->ctx, tab->bset, goto error);
1343         isl_assert(tab->mat->ctx, tab->samples, goto error);
1344         isl_assert(tab->mat->ctx, tab->samples->n_col == 1 + tab->n_var, goto error);
1345
1346         isl_int_init(v);
1347         for (i = tab->n_outside; i < tab->n_sample; ++i) {
1348                 int sgn;
1349                 isl_seq_inner_product(ineq, tab->samples->row[i],
1350                                         1 + tab->n_var, &v);
1351                 sgn = isl_int_sgn(v);
1352                 if (eq ? (sgn == 0) : (sgn >= 0))
1353                         continue;
1354                 tab = isl_tab_drop_sample(tab, i);
1355                 if (!tab)
1356                         break;
1357         }
1358         isl_int_clear(v);
1359
1360         return tab;
1361 error:
1362         isl_tab_free(tab);
1363         return NULL;
1364 }
1365
1366 /* Check whether the sample value of the tableau is finite,
1367  * i.e., either the tableau does not use a big parameter, or
1368  * all values of the variables are equal to the big parameter plus
1369  * some constant.  This constant is the actual sample value.
1370  */
1371 static int sample_is_finite(struct isl_tab *tab)
1372 {
1373         int i;
1374
1375         if (!tab->M)
1376                 return 1;
1377
1378         for (i = 0; i < tab->n_var; ++i) {
1379                 int row;
1380                 if (!tab->var[i].is_row)
1381                         return 0;
1382                 row = tab->var[i].index;
1383                 if (isl_int_ne(tab->mat->row[row][0], tab->mat->row[row][2]))
1384                         return 0;
1385         }
1386         return 1;
1387 }
1388
1389 /* Check if the context tableau of sol has any integer points.
1390  * Leave tab in empty state if no integer point can be found.
1391  * If an integer point can be found and if moreover it is finite,
1392  * then it is added to the list of sample values.
1393  *
1394  * This function is only called when none of the currently active sample
1395  * values satisfies the most recently added constraint.
1396  */
1397 static struct isl_tab *check_integer_feasible(struct isl_tab *tab)
1398 {
1399         struct isl_tab_undo *snap;
1400         int feasible;
1401
1402         if (!tab)
1403                 return NULL;
1404
1405         snap = isl_tab_snap(tab);
1406         if (isl_tab_push_basis(tab) < 0)
1407                 goto error;
1408
1409         tab = cut_to_integer_lexmin(tab);
1410         if (!tab)
1411                 goto error;
1412
1413         if (!tab->empty && sample_is_finite(tab)) {
1414                 struct isl_vec *sample;
1415
1416                 sample = isl_tab_get_sample_value(tab);
1417
1418                 tab = isl_tab_add_sample(tab, sample);
1419         }
1420
1421         if (!tab->empty && isl_tab_rollback(tab, snap) < 0)
1422                 goto error;
1423
1424         return tab;
1425 error:
1426         isl_tab_free(tab);
1427         return NULL;
1428 }
1429
1430 /* Check if any of the currently active sample values satisfies
1431  * the inequality "ineq" (an equality if eq is set).
1432  */
1433 static int tab_has_valid_sample(struct isl_tab *tab, isl_int *ineq, int eq)
1434 {
1435         int i;
1436         isl_int v;
1437
1438         if (!tab)
1439                 return -1;
1440
1441         isl_assert(tab->mat->ctx, tab->bset, return -1);
1442         isl_assert(tab->mat->ctx, tab->samples, return -1);
1443         isl_assert(tab->mat->ctx, tab->samples->n_col == 1 + tab->n_var, return -1);
1444
1445         isl_int_init(v);
1446         for (i = tab->n_outside; i < tab->n_sample; ++i) {
1447                 int sgn;
1448                 isl_seq_inner_product(ineq, tab->samples->row[i],
1449                                         1 + tab->n_var, &v);
1450                 sgn = isl_int_sgn(v);
1451                 if (eq ? (sgn == 0) : (sgn >= 0))
1452                         break;
1453         }
1454         isl_int_clear(v);
1455
1456         return i < tab->n_sample;
1457 }
1458
1459 /* For a div d = floor(f/m), add the constraints
1460  *
1461  *              f - m d >= 0
1462  *              -(f-(m-1)) + m d >= 0
1463  *
1464  * Note that the second constraint is the negation of
1465  *
1466  *              f - m d >= m
1467  */
1468 static void add_div_constraints(struct isl_context *context, unsigned div)
1469 {
1470         unsigned total;
1471         unsigned div_pos;
1472         struct isl_vec *ineq;
1473         struct isl_basic_set *bset;
1474
1475         bset = context->op->peek_basic_set(context);
1476         if (!bset)
1477                 goto error;
1478
1479         total = isl_basic_set_total_dim(bset);
1480         div_pos = 1 + total - bset->n_div + div;
1481
1482         ineq = ineq_for_div(bset, div);
1483         if (!ineq)
1484                 goto error;
1485
1486         context->op->add_ineq(context, ineq->el, 0, 0);
1487
1488         isl_seq_neg(ineq->el, bset->div[div] + 1, 1 + total);
1489         isl_int_set(ineq->el[div_pos], bset->div[div][0]);
1490         isl_int_add(ineq->el[0], ineq->el[0], ineq->el[div_pos]);
1491         isl_int_sub_ui(ineq->el[0], ineq->el[0], 1);
1492
1493         context->op->add_ineq(context, ineq->el, 0, 0);
1494
1495         isl_vec_free(ineq);
1496
1497         return;
1498 error:
1499         context->op->invalidate(context);
1500 }
1501
1502 /* Add a div specifed by "div" to the tableau "tab" and return
1503  * the index of the new div.  *nonneg is set to 1 if the div
1504  * is obviously non-negative.
1505  */
1506 static int context_tab_add_div(struct isl_tab *tab, struct isl_vec *div,
1507         int *nonneg)
1508 {
1509         int i;
1510         int r;
1511         int k;
1512         struct isl_mat *samples;
1513
1514         for (i = 0; i < tab->n_var; ++i) {
1515                 if (isl_int_is_zero(div->el[2 + i]))
1516                         continue;
1517                 if (!tab->var[i].is_nonneg)
1518                         break;
1519         }
1520         *nonneg = i == tab->n_var;
1521
1522         if (isl_tab_extend_cons(tab, 3) < 0)
1523                 return -1;
1524         if (isl_tab_extend_vars(tab, 1) < 0)
1525                 return -1;
1526         r = isl_tab_allocate_var(tab);
1527         if (r < 0)
1528                 return -1;
1529         if (*nonneg)
1530                 tab->var[r].is_nonneg = 1;
1531         tab->var[r].frozen = 1;
1532
1533         samples = isl_mat_extend(tab->samples,
1534                         tab->n_sample, 1 + tab->n_var);
1535         tab->samples = samples;
1536         if (!samples)
1537                 return -1;
1538         for (i = tab->n_outside; i < samples->n_row; ++i) {
1539                 isl_seq_inner_product(div->el + 1, samples->row[i],
1540                         div->size - 1, &samples->row[i][samples->n_col - 1]);
1541                 isl_int_fdiv_q(samples->row[i][samples->n_col - 1],
1542                                samples->row[i][samples->n_col - 1], div->el[0]);
1543         }
1544
1545         tab->bset = isl_basic_set_extend_dim(tab->bset,
1546                 isl_basic_set_get_dim(tab->bset), 1, 0, 2);
1547         k = isl_basic_set_alloc_div(tab->bset);
1548         if (k < 0)
1549                 return -1;
1550         isl_seq_cpy(tab->bset->div[k], div->el, div->size);
1551         if (isl_tab_push(tab, isl_tab_undo_bset_div) < 0)
1552                 return -1;
1553
1554         return k;
1555 }
1556
1557 /* Add a div specified by "div" to both the main tableau and
1558  * the context tableau.  In case of the main tableau, we only
1559  * need to add an extra div.  In the context tableau, we also
1560  * need to express the meaning of the div.
1561  * Return the index of the div or -1 if anything went wrong.
1562  */
1563 static int add_div(struct isl_tab *tab, struct isl_context *context,
1564         struct isl_vec *div)
1565 {
1566         int r;
1567         int k;
1568         int nonneg;
1569
1570         k = context->op->add_div(context, div, &nonneg);
1571         if (k < 0)
1572                 goto error;
1573
1574         add_div_constraints(context, k);
1575         if (!context->op->is_ok(context))
1576                 goto error;
1577
1578         if (isl_tab_extend_vars(tab, 1) < 0)
1579                 goto error;
1580         r = isl_tab_allocate_var(tab);
1581         if (r < 0)
1582                 goto error;
1583         if (nonneg)
1584                 tab->var[r].is_nonneg = 1;
1585         tab->var[r].frozen = 1;
1586         tab->n_div++;
1587
1588         return tab->n_div - 1;
1589 error:
1590         context->op->invalidate(context);
1591         return -1;
1592 }
1593
1594 static int find_div(struct isl_tab *tab, isl_int *div, isl_int denom)
1595 {
1596         int i;
1597         unsigned total = isl_basic_set_total_dim(tab->bset);
1598
1599         for (i = 0; i < tab->bset->n_div; ++i) {
1600                 if (isl_int_ne(tab->bset->div[i][0], denom))
1601                         continue;
1602                 if (!isl_seq_eq(tab->bset->div[i] + 1, div, total))
1603                         continue;
1604                 return i;
1605         }
1606         return -1;
1607 }
1608
1609 /* Return the index of a div that corresponds to "div".
1610  * We first check if we already have such a div and if not, we create one.
1611  */
1612 static int get_div(struct isl_tab *tab, struct isl_context *context,
1613         struct isl_vec *div)
1614 {
1615         int d;
1616         struct isl_tab *context_tab = context->op->peek_tab(context);
1617
1618         if (!context_tab)
1619                 return -1;
1620
1621         d = find_div(context_tab, div->el + 1, div->el[0]);
1622         if (d != -1)
1623                 return d;
1624
1625         return add_div(tab, context, div);
1626 }
1627
1628 /* Add a parametric cut to cut away the non-integral sample value
1629  * of the give row.
1630  * Let a_i be the coefficients of the constant term and the parameters
1631  * and let b_i be the coefficients of the variables or constraints
1632  * in basis of the tableau.
1633  * Let q be the div q = floor(\sum_i {-a_i} y_i).
1634  *
1635  * The cut is expressed as
1636  *
1637  *      c = \sum_i -{-a_i} y_i + \sum_i {b_i} x_i + q >= 0
1638  *
1639  * If q did not already exist in the context tableau, then it is added first.
1640  * If q is in a column of the main tableau then the "+ q" can be accomplished
1641  * by setting the corresponding entry to the denominator of the constraint.
1642  * If q happens to be in a row of the main tableau, then the corresponding
1643  * row needs to be added instead (taking care of the denominators).
1644  * Note that this is very unlikely, but perhaps not entirely impossible.
1645  *
1646  * The current value of the cut is known to be negative (or at least
1647  * non-positive), so row_sign is set accordingly.
1648  *
1649  * Return the row of the cut or -1.
1650  */
1651 static int add_parametric_cut(struct isl_tab *tab, int row,
1652         struct isl_context *context)
1653 {
1654         struct isl_vec *div;
1655         int d;
1656         int i;
1657         int r;
1658         isl_int *r_row;
1659         int col;
1660         int n;
1661         unsigned off = 2 + tab->M;
1662
1663         if (!context)
1664                 return -1;
1665
1666         div = get_row_parameter_div(tab, row);
1667         if (!div)
1668                 return -1;
1669
1670         n = tab->n_div;
1671         d = context->op->get_div(context, tab, div);
1672         if (d < 0)
1673                 return -1;
1674
1675         if (isl_tab_extend_cons(tab, 1) < 0)
1676                 return -1;
1677         r = isl_tab_allocate_con(tab);
1678         if (r < 0)
1679                 return -1;
1680
1681         r_row = tab->mat->row[tab->con[r].index];
1682         isl_int_set(r_row[0], tab->mat->row[row][0]);
1683         isl_int_neg(r_row[1], tab->mat->row[row][1]);
1684         isl_int_fdiv_r(r_row[1], r_row[1], tab->mat->row[row][0]);
1685         isl_int_neg(r_row[1], r_row[1]);
1686         if (tab->M)
1687                 isl_int_set_si(r_row[2], 0);
1688         for (i = 0; i < tab->n_param; ++i) {
1689                 if (tab->var[i].is_row)
1690                         continue;
1691                 col = tab->var[i].index;
1692                 isl_int_neg(r_row[off + col], tab->mat->row[row][off + col]);
1693                 isl_int_fdiv_r(r_row[off + col], r_row[off + col],
1694                                 tab->mat->row[row][0]);
1695                 isl_int_neg(r_row[off + col], r_row[off + col]);
1696         }
1697         for (i = 0; i < tab->n_div; ++i) {
1698                 if (tab->var[tab->n_var - tab->n_div + i].is_row)
1699                         continue;
1700                 col = tab->var[tab->n_var - tab->n_div + i].index;
1701                 isl_int_neg(r_row[off + col], tab->mat->row[row][off + col]);
1702                 isl_int_fdiv_r(r_row[off + col], r_row[off + col],
1703                                 tab->mat->row[row][0]);
1704                 isl_int_neg(r_row[off + col], r_row[off + col]);
1705         }
1706         for (i = 0; i < tab->n_col; ++i) {
1707                 if (tab->col_var[i] >= 0 &&
1708                     (tab->col_var[i] < tab->n_param ||
1709                      tab->col_var[i] >= tab->n_var - tab->n_div))
1710                         continue;
1711                 isl_int_fdiv_r(r_row[off + i],
1712                         tab->mat->row[row][off + i], tab->mat->row[row][0]);
1713         }
1714         if (tab->var[tab->n_var - tab->n_div + d].is_row) {
1715                 isl_int gcd;
1716                 int d_row = tab->var[tab->n_var - tab->n_div + d].index;
1717                 isl_int_init(gcd);
1718                 isl_int_gcd(gcd, tab->mat->row[d_row][0], r_row[0]);
1719                 isl_int_divexact(r_row[0], r_row[0], gcd);
1720                 isl_int_divexact(gcd, tab->mat->row[d_row][0], gcd);
1721                 isl_seq_combine(r_row + 1, gcd, r_row + 1,
1722                                 r_row[0], tab->mat->row[d_row] + 1,
1723                                 off - 1 + tab->n_col);
1724                 isl_int_mul(r_row[0], r_row[0], tab->mat->row[d_row][0]);
1725                 isl_int_clear(gcd);
1726         } else {
1727                 col = tab->var[tab->n_var - tab->n_div + d].index;
1728                 isl_int_set(r_row[off + col], tab->mat->row[row][0]);
1729         }
1730
1731         tab->con[r].is_nonneg = 1;
1732         if (isl_tab_push_var(tab, isl_tab_undo_nonneg, &tab->con[r]) < 0)
1733                 return -1;
1734         if (tab->row_sign)
1735                 tab->row_sign[tab->con[r].index] = isl_tab_row_neg;
1736
1737         isl_vec_free(div);
1738
1739         row = tab->con[r].index;
1740
1741         if (d >= n && context->op->detect_equalities(context, tab) < 0)
1742                 return -1;
1743
1744         return row;
1745 }
1746
1747 /* Construct a tableau for bmap that can be used for computing
1748  * the lexicographic minimum (or maximum) of bmap.
1749  * If not NULL, then dom is the domain where the minimum
1750  * should be computed.  In this case, we set up a parametric
1751  * tableau with row signs (initialized to "unknown").
1752  * If M is set, then the tableau will use a big parameter.
1753  * If max is set, then a maximum should be computed instead of a minimum.
1754  * This means that for each variable x, the tableau will contain the variable
1755  * x' = M - x, rather than x' = M + x.  This in turn means that the coefficient
1756  * of the variables in all constraints are negated prior to adding them
1757  * to the tableau.
1758  */
1759 static struct isl_tab *tab_for_lexmin(struct isl_basic_map *bmap,
1760         struct isl_basic_set *dom, unsigned M, int max)
1761 {
1762         int i;
1763         struct isl_tab *tab;
1764
1765         tab = isl_tab_alloc(bmap->ctx, 2 * bmap->n_eq + bmap->n_ineq + 1,
1766                             isl_basic_map_total_dim(bmap), M);
1767         if (!tab)
1768                 return NULL;
1769
1770         tab->rational = ISL_F_ISSET(bmap, ISL_BASIC_MAP_RATIONAL);
1771         if (dom) {
1772                 tab->n_param = isl_basic_set_total_dim(dom) - dom->n_div;
1773                 tab->n_div = dom->n_div;
1774                 tab->row_sign = isl_calloc_array(bmap->ctx,
1775                                         enum isl_tab_row_sign, tab->mat->n_row);
1776                 if (!tab->row_sign)
1777                         goto error;
1778         }
1779         if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_EMPTY))
1780                 return isl_tab_mark_empty(tab);
1781
1782         for (i = tab->n_param; i < tab->n_var - tab->n_div; ++i) {
1783                 tab->var[i].is_nonneg = 1;
1784                 tab->var[i].frozen = 1;
1785         }
1786         for (i = 0; i < bmap->n_eq; ++i) {
1787                 if (max)
1788                         isl_seq_neg(bmap->eq[i] + 1 + tab->n_param,
1789                                     bmap->eq[i] + 1 + tab->n_param,
1790                                     tab->n_var - tab->n_param - tab->n_div);
1791                 tab = add_lexmin_valid_eq(tab, bmap->eq[i]);
1792                 if (max)
1793                         isl_seq_neg(bmap->eq[i] + 1 + tab->n_param,
1794                                     bmap->eq[i] + 1 + tab->n_param,
1795                                     tab->n_var - tab->n_param - tab->n_div);
1796                 if (!tab || tab->empty)
1797                         return tab;
1798         }
1799         for (i = 0; i < bmap->n_ineq; ++i) {
1800                 if (max)
1801                         isl_seq_neg(bmap->ineq[i] + 1 + tab->n_param,
1802                                     bmap->ineq[i] + 1 + tab->n_param,
1803                                     tab->n_var - tab->n_param - tab->n_div);
1804                 tab = add_lexmin_ineq(tab, bmap->ineq[i]);
1805                 if (max)
1806                         isl_seq_neg(bmap->ineq[i] + 1 + tab->n_param,
1807                                     bmap->ineq[i] + 1 + tab->n_param,
1808                                     tab->n_var - tab->n_param - tab->n_div);
1809                 if (!tab || tab->empty)
1810                         return tab;
1811         }
1812         return tab;
1813 error:
1814         isl_tab_free(tab);
1815         return NULL;
1816 }
1817
1818 /* Given a main tableau where more than one row requires a split,
1819  * determine and return the "best" row to split on.
1820  *
1821  * Given two rows in the main tableau, if the inequality corresponding
1822  * to the first row is redundant with respect to that of the second row
1823  * in the current tableau, then it is better to split on the second row,
1824  * since in the positive part, both row will be positive.
1825  * (In the negative part a pivot will have to be performed and just about
1826  * anything can happen to the sign of the other row.)
1827  *
1828  * As a simple heuristic, we therefore select the row that makes the most
1829  * of the other rows redundant.
1830  *
1831  * Perhaps it would also be useful to look at the number of constraints
1832  * that conflict with any given constraint.
1833  */
1834 static int best_split(struct isl_tab *tab, struct isl_tab *context_tab)
1835 {
1836         struct isl_tab_undo *snap;
1837         int split;
1838         int row;
1839         int best = -1;
1840         int best_r;
1841
1842         if (isl_tab_extend_cons(context_tab, 2) < 0)
1843                 return -1;
1844
1845         snap = isl_tab_snap(context_tab);
1846
1847         for (split = tab->n_redundant; split < tab->n_row; ++split) {
1848                 struct isl_tab_undo *snap2;
1849                 struct isl_vec *ineq = NULL;
1850                 int r = 0;
1851
1852                 if (!isl_tab_var_from_row(tab, split)->is_nonneg)
1853                         continue;
1854                 if (tab->row_sign[split] != isl_tab_row_any)
1855                         continue;
1856
1857                 ineq = get_row_parameter_ineq(tab, split);
1858                 if (!ineq)
1859                         return -1;
1860                 context_tab = isl_tab_add_ineq(context_tab, ineq->el);
1861                 isl_vec_free(ineq);
1862
1863                 snap2 = isl_tab_snap(context_tab);
1864
1865                 for (row = tab->n_redundant; row < tab->n_row; ++row) {
1866                         struct isl_tab_var *var;
1867
1868                         if (row == split)
1869                                 continue;
1870                         if (!isl_tab_var_from_row(tab, row)->is_nonneg)
1871                                 continue;
1872                         if (tab->row_sign[row] != isl_tab_row_any)
1873                                 continue;
1874
1875                         ineq = get_row_parameter_ineq(tab, row);
1876                         if (!ineq)
1877                                 return -1;
1878                         context_tab = isl_tab_add_ineq(context_tab, ineq->el);
1879                         isl_vec_free(ineq);
1880                         var = &context_tab->con[context_tab->n_con - 1];
1881                         if (!context_tab->empty &&
1882                             !isl_tab_min_at_most_neg_one(context_tab, var))
1883                                 r++;
1884                         if (isl_tab_rollback(context_tab, snap2) < 0)
1885                                 return -1;
1886                 }
1887                 if (best == -1 || r > best_r) {
1888                         best = split;
1889                         best_r = r;
1890                 }
1891                 if (isl_tab_rollback(context_tab, snap) < 0)
1892                         return -1;
1893         }
1894
1895         return best;
1896 }
1897
1898 static struct isl_basic_set *context_lex_peek_basic_set(
1899         struct isl_context *context)
1900 {
1901         struct isl_context_lex *clex = (struct isl_context_lex *)context;
1902         if (!clex->tab)
1903                 return NULL;
1904         return clex->tab->bset;
1905 }
1906
1907 static struct isl_tab *context_lex_peek_tab(struct isl_context *context)
1908 {
1909         struct isl_context_lex *clex = (struct isl_context_lex *)context;
1910         return clex->tab;
1911 }
1912
1913 static void context_lex_extend(struct isl_context *context, int n)
1914 {
1915         struct isl_context_lex *clex = (struct isl_context_lex *)context;
1916         if (!clex->tab)
1917                 return;
1918         if (isl_tab_extend_cons(clex->tab, n) >= 0)
1919                 return;
1920         isl_tab_free(clex->tab);
1921         clex->tab = NULL;
1922 }
1923
1924 static void context_lex_add_eq(struct isl_context *context, isl_int *eq,
1925                 int check, int update)
1926 {
1927         struct isl_context_lex *clex = (struct isl_context_lex *)context;
1928         if (isl_tab_extend_cons(clex->tab, 2) < 0)
1929                 goto error;
1930         clex->tab = add_lexmin_eq(clex->tab, eq);
1931         if (check) {
1932                 int v = tab_has_valid_sample(clex->tab, eq, 1);
1933                 if (v < 0)
1934                         goto error;
1935                 if (!v)
1936                         clex->tab = check_integer_feasible(clex->tab);
1937         }
1938         if (update)
1939                 clex->tab = check_samples(clex->tab, eq, 1);
1940         return;
1941 error:
1942         isl_tab_free(clex->tab);
1943         clex->tab = NULL;
1944 }
1945
1946 static void context_lex_add_ineq(struct isl_context *context, isl_int *ineq,
1947                 int check, int update)
1948 {
1949         struct isl_context_lex *clex = (struct isl_context_lex *)context;
1950         if (isl_tab_extend_cons(clex->tab, 1) < 0)
1951                 goto error;
1952         clex->tab = add_lexmin_ineq(clex->tab, ineq);
1953         if (check) {
1954                 int v = tab_has_valid_sample(clex->tab, ineq, 0);
1955                 if (v < 0)
1956                         goto error;
1957                 if (!v)
1958                         clex->tab = check_integer_feasible(clex->tab);
1959         }
1960         if (update)
1961                 clex->tab = check_samples(clex->tab, ineq, 0);
1962         return;
1963 error:
1964         isl_tab_free(clex->tab);
1965         clex->tab = NULL;
1966 }
1967
1968 /* Check which signs can be obtained by "ineq" on all the currently
1969  * active sample values.  See row_sign for more information.
1970  */
1971 static enum isl_tab_row_sign tab_ineq_sign(struct isl_tab *tab, isl_int *ineq,
1972         int strict)
1973 {
1974         int i;
1975         int sgn;
1976         isl_int tmp;
1977         int res = isl_tab_row_unknown;
1978
1979         isl_assert(tab->mat->ctx, tab->samples, return 0);
1980         isl_assert(tab->mat->ctx, tab->samples->n_col == 1 + tab->n_var, return 0);
1981
1982         isl_int_init(tmp);
1983         for (i = tab->n_outside; i < tab->n_sample; ++i) {
1984                 isl_seq_inner_product(tab->samples->row[i], ineq,
1985                                         1 + tab->n_var, &tmp);
1986                 sgn = isl_int_sgn(tmp);
1987                 if (sgn > 0 || (sgn == 0 && strict)) {
1988                         if (res == isl_tab_row_unknown)
1989                                 res = isl_tab_row_pos;
1990                         if (res == isl_tab_row_neg)
1991                                 res = isl_tab_row_any;
1992                 }
1993                 if (sgn < 0) {
1994                         if (res == isl_tab_row_unknown)
1995                                 res = isl_tab_row_neg;
1996                         if (res == isl_tab_row_pos)
1997                                 res = isl_tab_row_any;
1998                 }
1999                 if (res == isl_tab_row_any)
2000                         break;
2001         }
2002         isl_int_clear(tmp);
2003
2004         return res;
2005 }
2006
2007 static enum isl_tab_row_sign context_lex_ineq_sign(struct isl_context *context,
2008                         isl_int *ineq, int strict)
2009 {
2010         struct isl_context_lex *clex = (struct isl_context_lex *)context;
2011         return tab_ineq_sign(clex->tab, ineq, strict);
2012 }
2013
2014 /* Check whether "ineq" can be added to the tableau without rendering
2015  * it infeasible.
2016  */
2017 static int context_lex_test_ineq(struct isl_context *context, isl_int *ineq)
2018 {
2019         struct isl_context_lex *clex = (struct isl_context_lex *)context;
2020         struct isl_tab_undo *snap;
2021         int feasible;
2022
2023         if (!clex->tab)
2024                 return -1;
2025
2026         if (isl_tab_extend_cons(clex->tab, 1) < 0)
2027                 return -1;
2028
2029         snap = isl_tab_snap(clex->tab);
2030         if (isl_tab_push_basis(clex->tab) < 0)
2031                 return -1;
2032         clex->tab = add_lexmin_ineq(clex->tab, ineq);
2033         clex->tab = check_integer_feasible(clex->tab);
2034         if (!clex->tab)
2035                 return -1;
2036         feasible = !clex->tab->empty;
2037         if (isl_tab_rollback(clex->tab, snap) < 0)
2038                 return -1;
2039
2040         return feasible;
2041 }
2042
2043 static int context_lex_get_div(struct isl_context *context, struct isl_tab *tab,
2044                 struct isl_vec *div)
2045 {
2046         return get_div(tab, context, div);
2047 }
2048
2049 static int context_lex_add_div(struct isl_context *context, struct isl_vec *div,
2050         int *nonneg)
2051 {
2052         struct isl_context_lex *clex = (struct isl_context_lex *)context;
2053         return context_tab_add_div(clex->tab, div, nonneg);
2054 }
2055
2056 static int context_lex_detect_equalities(struct isl_context *context,
2057                 struct isl_tab *tab)
2058 {
2059         return 0;
2060 }
2061
2062 static int context_lex_best_split(struct isl_context *context,
2063                 struct isl_tab *tab)
2064 {
2065         struct isl_context_lex *clex = (struct isl_context_lex *)context;
2066         struct isl_tab_undo *snap;
2067         int r;
2068
2069         snap = isl_tab_snap(clex->tab);
2070         if (isl_tab_push_basis(clex->tab) < 0)
2071                 return -1;
2072         r = best_split(tab, clex->tab);
2073
2074         if (isl_tab_rollback(clex->tab, snap) < 0)
2075                 return -1;
2076
2077         return r;
2078 }
2079
2080 static int context_lex_is_empty(struct isl_context *context)
2081 {
2082         struct isl_context_lex *clex = (struct isl_context_lex *)context;
2083         if (!clex->tab)
2084                 return -1;
2085         return clex->tab->empty;
2086 }
2087
2088 static void *context_lex_save(struct isl_context *context)
2089 {
2090         struct isl_context_lex *clex = (struct isl_context_lex *)context;
2091         struct isl_tab_undo *snap;
2092
2093         snap = isl_tab_snap(clex->tab);
2094         if (isl_tab_push_basis(clex->tab) < 0)
2095                 return NULL;
2096         if (isl_tab_save_samples(clex->tab) < 0)
2097                 return NULL;
2098
2099         return snap;
2100 }
2101
2102 static void context_lex_restore(struct isl_context *context, void *save)
2103 {
2104         struct isl_context_lex *clex = (struct isl_context_lex *)context;
2105         if (isl_tab_rollback(clex->tab, (struct isl_tab_undo *)save) < 0) {
2106                 isl_tab_free(clex->tab);
2107                 clex->tab = NULL;
2108         }
2109 }
2110
2111 static int context_lex_is_ok(struct isl_context *context)
2112 {
2113         struct isl_context_lex *clex = (struct isl_context_lex *)context;
2114         return !!clex->tab;
2115 }
2116
2117 /* For each variable in the context tableau, check if the variable can
2118  * only attain non-negative values.  If so, mark the parameter as non-negative
2119  * in the main tableau.  This allows for a more direct identification of some
2120  * cases of violated constraints.
2121  */
2122 static struct isl_tab *tab_detect_nonnegative_parameters(struct isl_tab *tab,
2123         struct isl_tab *context_tab)
2124 {
2125         int i;
2126         struct isl_tab_undo *snap;
2127         struct isl_vec *ineq = NULL;
2128         struct isl_tab_var *var;
2129         int n;
2130
2131         if (context_tab->n_var == 0)
2132                 return tab;
2133
2134         ineq = isl_vec_alloc(tab->mat->ctx, 1 + context_tab->n_var);
2135         if (!ineq)
2136                 goto error;
2137
2138         if (isl_tab_extend_cons(context_tab, 1) < 0)
2139                 goto error;
2140
2141         snap = isl_tab_snap(context_tab);
2142
2143         n = 0;
2144         isl_seq_clr(ineq->el, ineq->size);
2145         for (i = 0; i < context_tab->n_var; ++i) {
2146                 isl_int_set_si(ineq->el[1 + i], 1);
2147                 context_tab = isl_tab_add_ineq(context_tab, ineq->el);
2148                 var = &context_tab->con[context_tab->n_con - 1];
2149                 if (!context_tab->empty &&
2150                     !isl_tab_min_at_most_neg_one(context_tab, var)) {
2151                         int j = i;
2152                         if (i >= tab->n_param)
2153                                 j = i - tab->n_param + tab->n_var - tab->n_div;
2154                         tab->var[j].is_nonneg = 1;
2155                         n++;
2156                 }
2157                 isl_int_set_si(ineq->el[1 + i], 0);
2158                 if (isl_tab_rollback(context_tab, snap) < 0)
2159                         goto error;
2160         }
2161
2162         if (context_tab->M && n == context_tab->n_var) {
2163                 context_tab->mat = isl_mat_drop_cols(context_tab->mat, 2, 1);
2164                 context_tab->M = 0;
2165         }
2166
2167         isl_vec_free(ineq);
2168         return tab;
2169 error:
2170         isl_vec_free(ineq);
2171         isl_tab_free(tab);
2172         return NULL;
2173 }
2174
2175 static struct isl_tab *context_lex_detect_nonnegative_parameters(
2176         struct isl_context *context, struct isl_tab *tab)
2177 {
2178         struct isl_context_lex *clex = (struct isl_context_lex *)context;
2179         struct isl_tab_undo *snap;
2180
2181         snap = isl_tab_snap(clex->tab);
2182         if (isl_tab_push_basis(clex->tab) < 0)
2183                 goto error;
2184
2185         tab = tab_detect_nonnegative_parameters(tab, clex->tab);
2186
2187         if (isl_tab_rollback(clex->tab, snap) < 0)
2188                 goto error;
2189
2190         return tab;
2191 error:
2192         isl_tab_free(tab);
2193         return NULL;
2194 }
2195
2196 static void context_lex_invalidate(struct isl_context *context)
2197 {
2198         struct isl_context_lex *clex = (struct isl_context_lex *)context;
2199         isl_tab_free(clex->tab);
2200         clex->tab = NULL;
2201 }
2202
2203 static void context_lex_free(struct isl_context *context)
2204 {
2205         struct isl_context_lex *clex = (struct isl_context_lex *)context;
2206         isl_tab_free(clex->tab);
2207         free(clex);
2208 }
2209
2210 struct isl_context_op isl_context_lex_op = {
2211         context_lex_detect_nonnegative_parameters,
2212         context_lex_peek_basic_set,
2213         context_lex_peek_tab,
2214         context_lex_add_eq,
2215         context_lex_add_ineq,
2216         context_lex_ineq_sign,
2217         context_lex_test_ineq,
2218         context_lex_get_div,
2219         context_lex_add_div,
2220         context_lex_detect_equalities,
2221         context_lex_best_split,
2222         context_lex_is_empty,
2223         context_lex_is_ok,
2224         context_lex_save,
2225         context_lex_restore,
2226         context_lex_invalidate,
2227         context_lex_free,
2228 };
2229
2230 static struct isl_tab *context_tab_for_lexmin(struct isl_basic_set *bset)
2231 {
2232         struct isl_tab *tab;
2233
2234         bset = isl_basic_set_cow(bset);
2235         if (!bset)
2236                 return NULL;
2237         tab = tab_for_lexmin((struct isl_basic_map *)bset, NULL, 1, 0);
2238         if (!tab)
2239                 goto error;
2240         tab->bset = bset;
2241         tab = isl_tab_init_samples(tab);
2242         return tab;
2243 error:
2244         isl_basic_set_free(bset);
2245         return NULL;
2246 }
2247
2248 static struct isl_context *isl_context_lex_alloc(struct isl_basic_set *dom)
2249 {
2250         struct isl_context_lex *clex;
2251
2252         if (!dom)
2253                 return NULL;
2254
2255         clex = isl_alloc_type(dom->ctx, struct isl_context_lex);
2256         if (!clex)
2257                 return NULL;
2258
2259         clex->context.op = &isl_context_lex_op;
2260
2261         clex->tab = context_tab_for_lexmin(isl_basic_set_copy(dom));
2262         clex->tab = restore_lexmin(clex->tab);
2263         clex->tab = check_integer_feasible(clex->tab);
2264         if (!clex->tab)
2265                 goto error;
2266
2267         return &clex->context;
2268 error:
2269         clex->context.op->free(&clex->context);
2270         return NULL;
2271 }
2272
2273 struct isl_context_gbr {
2274         struct isl_context context;
2275         struct isl_tab *tab;
2276         struct isl_tab *shifted;
2277         struct isl_tab *cone;
2278 };
2279
2280 static struct isl_tab *context_gbr_detect_nonnegative_parameters(
2281         struct isl_context *context, struct isl_tab *tab)
2282 {
2283         struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
2284         return tab_detect_nonnegative_parameters(tab, cgbr->tab);
2285 }
2286
2287 static struct isl_basic_set *context_gbr_peek_basic_set(
2288         struct isl_context *context)
2289 {
2290         struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
2291         if (!cgbr->tab)
2292                 return NULL;
2293         return cgbr->tab->bset;
2294 }
2295
2296 static struct isl_tab *context_gbr_peek_tab(struct isl_context *context)
2297 {
2298         struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
2299         return cgbr->tab;
2300 }
2301
2302 /* Initialize the "shifted" tableau of the context, which
2303  * contains the constraints of the original tableau shifted
2304  * by the sum of all negative coefficients.  This ensures
2305  * that any rational point in the shifted tableau can
2306  * be rounded up to yield an integer point in the original tableau.
2307  */
2308 static void gbr_init_shifted(struct isl_context_gbr *cgbr)
2309 {
2310         int i, j;
2311         struct isl_vec *cst;
2312         struct isl_basic_set *bset = cgbr->tab->bset;
2313         unsigned dim = isl_basic_set_total_dim(bset);
2314
2315         cst = isl_vec_alloc(cgbr->tab->mat->ctx, bset->n_ineq);
2316         if (!cst)
2317                 return;
2318
2319         for (i = 0; i < bset->n_ineq; ++i) {
2320                 isl_int_set(cst->el[i], bset->ineq[i][0]);
2321                 for (j = 0; j < dim; ++j) {
2322                         if (!isl_int_is_neg(bset->ineq[i][1 + j]))
2323                                 continue;
2324                         isl_int_add(bset->ineq[i][0], bset->ineq[i][0],
2325                                     bset->ineq[i][1 + j]);
2326                 }
2327         }
2328
2329         cgbr->shifted = isl_tab_from_basic_set(bset);
2330
2331         for (i = 0; i < bset->n_ineq; ++i)
2332                 isl_int_set(bset->ineq[i][0], cst->el[i]);
2333
2334         isl_vec_free(cst);
2335 }
2336
2337 /* Check if the shifted tableau is non-empty, and if so
2338  * use the sample point to construct an integer point
2339  * of the context tableau.
2340  */
2341 static struct isl_vec *gbr_get_shifted_sample(struct isl_context_gbr *cgbr)
2342 {
2343         struct isl_vec *sample;
2344
2345         if (!cgbr->shifted)
2346                 gbr_init_shifted(cgbr);
2347         if (!cgbr->shifted)
2348                 return NULL;
2349         if (cgbr->shifted->empty)
2350                 return isl_vec_alloc(cgbr->tab->mat->ctx, 0);
2351
2352         sample = isl_tab_get_sample_value(cgbr->shifted);
2353         sample = isl_vec_ceil(sample);
2354
2355         return sample;
2356 }
2357
2358 static struct isl_basic_set *drop_constant_terms(struct isl_basic_set *bset)
2359 {
2360         int i;
2361
2362         if (!bset)
2363                 return NULL;
2364
2365         for (i = 0; i < bset->n_eq; ++i)
2366                 isl_int_set_si(bset->eq[i][0], 0);
2367
2368         for (i = 0; i < bset->n_ineq; ++i)
2369                 isl_int_set_si(bset->ineq[i][0], 0);
2370
2371         return bset;
2372 }
2373
2374 static int use_shifted(struct isl_context_gbr *cgbr)
2375 {
2376         return cgbr->tab->bset->n_eq == 0 && cgbr->tab->bset->n_div == 0;
2377 }
2378
2379 static struct isl_vec *gbr_get_sample(struct isl_context_gbr *cgbr)
2380 {
2381         struct isl_basic_set *bset;
2382         struct isl_basic_set *cone;
2383
2384         if (isl_tab_sample_is_integer(cgbr->tab))
2385                 return isl_tab_get_sample_value(cgbr->tab);
2386
2387         if (use_shifted(cgbr)) {
2388                 struct isl_vec *sample;
2389
2390                 sample = gbr_get_shifted_sample(cgbr);
2391                 if (!sample || sample->size > 0)
2392                         return sample;
2393
2394                 isl_vec_free(sample);
2395         }
2396
2397         if (!cgbr->cone) {
2398                 cgbr->cone = isl_tab_from_recession_cone(cgbr->tab->bset);
2399                 if (!cgbr->cone)
2400                         return NULL;
2401                 cgbr->cone->bset = isl_basic_set_dup(cgbr->tab->bset);
2402         }
2403         cgbr->cone = isl_tab_detect_implicit_equalities(cgbr->cone);
2404         if (!cgbr->cone)
2405                 return NULL;
2406
2407         if (cgbr->cone->n_dead == cgbr->cone->n_col) {
2408                 struct isl_vec *sample;
2409                 struct isl_tab_undo *snap;
2410
2411                 if (cgbr->tab->basis) {
2412                         if (cgbr->tab->basis->n_col != 1 + cgbr->tab->n_var) {
2413                                 isl_mat_free(cgbr->tab->basis);
2414                                 cgbr->tab->basis = NULL;
2415                         } else {
2416                                 cgbr->tab->n_zero = 0;
2417                                 cgbr->tab->n_unbounded = 0;
2418                         }
2419                 }
2420
2421                 snap = isl_tab_snap(cgbr->tab);
2422
2423                 sample = isl_tab_sample(cgbr->tab);
2424
2425                 if (isl_tab_rollback(cgbr->tab, snap) < 0) {
2426                         isl_vec_free(sample);
2427                         return NULL;
2428                 }
2429
2430                 return sample;
2431         }
2432
2433         cone = isl_basic_set_dup(cgbr->cone->bset);
2434         cone = drop_constant_terms(cone);
2435         cone = isl_basic_set_update_from_tab(cone, cgbr->cone);
2436         cone = isl_basic_set_underlying_set(cone);
2437         cone = isl_basic_set_gauss(cone, NULL);
2438
2439         bset = isl_basic_set_dup(cgbr->tab->bset);
2440         bset = isl_basic_set_update_from_tab(bset, cgbr->tab);
2441         bset = isl_basic_set_underlying_set(bset);
2442         bset = isl_basic_set_gauss(bset, NULL);
2443
2444         return isl_basic_set_sample_with_cone(bset, cone);
2445 }
2446
2447 static void check_gbr_integer_feasible(struct isl_context_gbr *cgbr)
2448 {
2449         struct isl_vec *sample;
2450
2451         if (!cgbr->tab)
2452                 return;
2453
2454         if (cgbr->tab->empty)
2455                 return;
2456
2457         sample = gbr_get_sample(cgbr);
2458         if (!sample)
2459                 goto error;
2460
2461         if (sample->size == 0) {
2462                 isl_vec_free(sample);
2463                 cgbr->tab = isl_tab_mark_empty(cgbr->tab);
2464                 return;
2465         }
2466
2467         cgbr->tab = isl_tab_add_sample(cgbr->tab, sample);
2468
2469         return;
2470 error:
2471         isl_tab_free(cgbr->tab);
2472         cgbr->tab = NULL;
2473 }
2474
2475 static struct isl_tab *add_gbr_eq(struct isl_tab *tab, isl_int *eq)
2476 {
2477         int r;
2478
2479         if (!tab)
2480                 return NULL;
2481
2482         if (isl_tab_extend_cons(tab, 2) < 0)
2483                 goto error;
2484
2485         tab = isl_tab_add_eq(tab, eq);
2486
2487         return tab;
2488 error:
2489         isl_tab_free(tab);
2490         return NULL;
2491 }
2492
2493 static void context_gbr_add_eq(struct isl_context *context, isl_int *eq,
2494                 int check, int update)
2495 {
2496         struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
2497
2498         cgbr->tab = add_gbr_eq(cgbr->tab, eq);
2499
2500         if (cgbr->cone && cgbr->cone->n_col != cgbr->cone->n_dead) {
2501                 if (isl_tab_extend_cons(cgbr->cone, 2) < 0)
2502                         goto error;
2503                 cgbr->cone = isl_tab_add_eq(cgbr->cone, eq);
2504         }
2505
2506         if (check) {
2507                 int v = tab_has_valid_sample(cgbr->tab, eq, 1);
2508                 if (v < 0)
2509                         goto error;
2510                 if (!v)
2511                         check_gbr_integer_feasible(cgbr);
2512         }
2513         if (update)
2514                 cgbr->tab = check_samples(cgbr->tab, eq, 1);
2515         return;
2516 error:
2517         isl_tab_free(cgbr->tab);
2518         cgbr->tab = NULL;
2519 }
2520
2521 static void add_gbr_ineq(struct isl_context_gbr *cgbr, isl_int *ineq)
2522 {
2523         if (!cgbr->tab)
2524                 return;
2525
2526         if (isl_tab_extend_cons(cgbr->tab, 1) < 0)
2527                 goto error;
2528
2529         cgbr->tab = isl_tab_add_ineq(cgbr->tab, ineq);
2530
2531         if (cgbr->shifted && !cgbr->shifted->empty && use_shifted(cgbr)) {
2532                 int i;
2533                 unsigned dim;
2534                 dim = isl_basic_set_total_dim(cgbr->tab->bset);
2535
2536                 if (isl_tab_extend_cons(cgbr->shifted, 1) < 0)
2537                         goto error;
2538
2539                 for (i = 0; i < dim; ++i) {
2540                         if (!isl_int_is_neg(ineq[1 + i]))
2541                                 continue;
2542                         isl_int_add(ineq[0], ineq[0], ineq[1 + i]);
2543                 }
2544
2545                 cgbr->shifted = isl_tab_add_ineq(cgbr->shifted, ineq);
2546
2547                 for (i = 0; i < dim; ++i) {
2548                         if (!isl_int_is_neg(ineq[1 + i]))
2549                                 continue;
2550                         isl_int_sub(ineq[0], ineq[0], ineq[1 + i]);
2551                 }
2552         }
2553
2554         if (cgbr->cone && cgbr->cone->n_col != cgbr->cone->n_dead) {
2555                 if (isl_tab_extend_cons(cgbr->cone, 1) < 0)
2556                         goto error;
2557                 cgbr->cone = isl_tab_add_ineq(cgbr->cone, ineq);
2558         }
2559
2560         return;
2561 error:
2562         isl_tab_free(cgbr->tab);
2563         cgbr->tab = NULL;
2564 }
2565
2566 static void context_gbr_add_ineq(struct isl_context *context, isl_int *ineq,
2567                 int check, int update)
2568 {
2569         struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
2570
2571         add_gbr_ineq(cgbr, ineq);
2572         if (!cgbr->tab)
2573                 return;
2574
2575         if (check) {
2576                 int v = tab_has_valid_sample(cgbr->tab, ineq, 0);
2577                 if (v < 0)
2578                         goto error;
2579                 if (!v)
2580                         check_gbr_integer_feasible(cgbr);
2581         }
2582         if (update)
2583                 cgbr->tab = check_samples(cgbr->tab, ineq, 0);
2584         return;
2585 error:
2586         isl_tab_free(cgbr->tab);
2587         cgbr->tab = NULL;
2588 }
2589
2590 static enum isl_tab_row_sign context_gbr_ineq_sign(struct isl_context *context,
2591                         isl_int *ineq, int strict)
2592 {
2593         struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
2594         return tab_ineq_sign(cgbr->tab, ineq, strict);
2595 }
2596
2597 /* Check whether "ineq" can be added to the tableau without rendering
2598  * it infeasible.
2599  */
2600 static int context_gbr_test_ineq(struct isl_context *context, isl_int *ineq)
2601 {
2602         struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
2603         struct isl_tab_undo *snap;
2604         struct isl_tab_undo *shifted_snap = NULL;
2605         struct isl_tab_undo *cone_snap = NULL;
2606         int feasible;
2607
2608         if (!cgbr->tab)
2609                 return -1;
2610
2611         if (isl_tab_extend_cons(cgbr->tab, 1) < 0)
2612                 return -1;
2613
2614         snap = isl_tab_snap(cgbr->tab);
2615         if (cgbr->shifted)
2616                 shifted_snap = isl_tab_snap(cgbr->shifted);
2617         if (cgbr->cone)
2618                 cone_snap = isl_tab_snap(cgbr->cone);
2619         add_gbr_ineq(cgbr, ineq);
2620         check_gbr_integer_feasible(cgbr);
2621         if (!cgbr->tab)
2622                 return -1;
2623         feasible = !cgbr->tab->empty;
2624         if (isl_tab_rollback(cgbr->tab, snap) < 0)
2625                 return -1;
2626         if (shifted_snap) {
2627                 if (isl_tab_rollback(cgbr->shifted, shifted_snap))
2628                         return -1;
2629         } else if (cgbr->shifted) {
2630                 isl_tab_free(cgbr->shifted);
2631                 cgbr->shifted = NULL;
2632         }
2633         if (cone_snap) {
2634                 if (isl_tab_rollback(cgbr->cone, cone_snap))
2635                         return -1;
2636         } else if (cgbr->cone) {
2637                 isl_tab_free(cgbr->cone);
2638                 cgbr->cone = NULL;
2639         }
2640
2641         return feasible;
2642 }
2643
2644 /* Return the column of the last of the variables associated to
2645  * a column that has a non-zero coefficient.
2646  * This function is called in a context where only coefficients
2647  * of parameters or divs can be non-zero.
2648  */
2649 static int last_non_zero_var_col(struct isl_tab *tab, isl_int *p)
2650 {
2651         int i;
2652         int col;
2653         unsigned dim = tab->n_var - tab->n_param - tab->n_div;
2654
2655         if (tab->n_var == 0)
2656                 return -1;
2657
2658         for (i = tab->n_var - 1; i >= 0; --i) {
2659                 if (i >= tab->n_param && i < tab->n_var - tab->n_div)
2660                         continue;
2661                 if (tab->var[i].is_row)
2662                         continue;
2663                 col = tab->var[i].index;
2664                 if (!isl_int_is_zero(p[col]))
2665                         return col;
2666         }
2667
2668         return -1;
2669 }
2670
2671 /* Look through all the recently added equalities in the context
2672  * to see if we can propagate any of them to the main tableau.
2673  *
2674  * The newly added equalities in the context are encoded as pairs
2675  * of inequalities starting at inequality "first".
2676  *
2677  * We tentatively add each of these equalities to the main tableau
2678  * and if this happens to result in a row with a final coefficient
2679  * that is one or negative one, we use it to kill a column
2680  * in the main tableau.  Otherwise, we discard the tentatively
2681  * added row.
2682  */
2683 static void propagate_equalities(struct isl_context_gbr *cgbr,
2684         struct isl_tab *tab, unsigned first)
2685 {
2686         int i;
2687         struct isl_vec *eq = NULL;
2688
2689         eq = isl_vec_alloc(tab->mat->ctx, 1 + tab->n_var);
2690         if (!eq)
2691                 goto error;
2692
2693         if (isl_tab_extend_cons(tab, (cgbr->tab->bset->n_ineq - first)/2) < 0)
2694                 goto error;
2695
2696         isl_seq_clr(eq->el + 1 + tab->n_param,
2697                     tab->n_var - tab->n_param - tab->n_div);
2698         for (i = first; i < cgbr->tab->bset->n_ineq; i += 2) {
2699                 int j;
2700                 int r;
2701                 struct isl_tab_undo *snap;
2702                 snap = isl_tab_snap(tab);
2703
2704                 isl_seq_cpy(eq->el, cgbr->tab->bset->ineq[i], 1 + tab->n_param);
2705                 isl_seq_cpy(eq->el + 1 + tab->n_var - tab->n_div,
2706                             cgbr->tab->bset->ineq[i] + 1 + tab->n_param,
2707                             tab->n_div);
2708
2709                 r = isl_tab_add_row(tab, eq->el);
2710                 if (r < 0)
2711                         goto error;
2712                 r = tab->con[r].index;
2713                 j = last_non_zero_var_col(tab, tab->mat->row[r] + 2 + tab->M);
2714                 if (j < 0 || j < tab->n_dead ||
2715                     !isl_int_is_one(tab->mat->row[r][0]) ||
2716                     (!isl_int_is_one(tab->mat->row[r][2 + tab->M + j]) &&
2717                      !isl_int_is_negone(tab->mat->row[r][2 + tab->M + j]))) {
2718                         if (isl_tab_rollback(tab, snap) < 0)
2719                                 goto error;
2720                         continue;
2721                 }
2722                 if (isl_tab_pivot(tab, r, j) < 0)
2723                         goto error;
2724                 if (isl_tab_kill_col(tab, j) < 0)
2725                         goto error;
2726
2727                 tab = restore_lexmin(tab);
2728         }
2729
2730         isl_vec_free(eq);
2731
2732         return;
2733 error:
2734         isl_vec_free(eq);
2735         isl_tab_free(cgbr->tab);
2736         cgbr->tab = NULL;
2737 }
2738
2739 static int context_gbr_detect_equalities(struct isl_context *context,
2740         struct isl_tab *tab)
2741 {
2742         struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
2743         struct isl_ctx *ctx;
2744         int i;
2745         enum isl_lp_result res;
2746         unsigned n_ineq;
2747
2748         ctx = cgbr->tab->mat->ctx;
2749
2750         if (!cgbr->cone) {
2751                 cgbr->cone = isl_tab_from_recession_cone(cgbr->tab->bset);
2752                 if (!cgbr->cone)
2753                         goto error;
2754                 cgbr->cone->bset = isl_basic_set_dup(cgbr->tab->bset);
2755         }
2756         cgbr->cone = isl_tab_detect_implicit_equalities(cgbr->cone);
2757
2758         n_ineq = cgbr->tab->bset->n_ineq;
2759         cgbr->tab = isl_tab_detect_equalities(cgbr->tab, cgbr->cone);
2760         if (cgbr->tab && cgbr->tab->bset->n_ineq > n_ineq)
2761                 propagate_equalities(cgbr, tab, n_ineq);
2762
2763         return 0;
2764 error:
2765         isl_tab_free(cgbr->tab);
2766         cgbr->tab = NULL;
2767         return -1;
2768 }
2769
2770 static int context_gbr_get_div(struct isl_context *context, struct isl_tab *tab,
2771                 struct isl_vec *div)
2772 {
2773         return get_div(tab, context, div);
2774 }
2775
2776 static int context_gbr_add_div(struct isl_context *context, struct isl_vec *div,
2777         int *nonneg)
2778 {
2779         struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
2780         if (cgbr->cone) {
2781                 int k;
2782
2783                 if (isl_tab_extend_cons(cgbr->cone, 3) < 0)
2784                         return -1;
2785                 if (isl_tab_extend_vars(cgbr->cone, 1) < 0)
2786                         return -1;
2787                 if (isl_tab_allocate_var(cgbr->cone) <0)
2788                         return -1;
2789
2790                 cgbr->cone->bset = isl_basic_set_extend_dim(cgbr->cone->bset,
2791                         isl_basic_set_get_dim(cgbr->cone->bset), 1, 0, 2);
2792                 k = isl_basic_set_alloc_div(cgbr->cone->bset);
2793                 if (k < 0)
2794                         return -1;
2795                 isl_seq_cpy(cgbr->cone->bset->div[k], div->el, div->size);
2796                 if (isl_tab_push(cgbr->cone, isl_tab_undo_bset_div) < 0)
2797                         return -1;
2798         }
2799         return context_tab_add_div(cgbr->tab, div, nonneg);
2800 }
2801
2802 static int context_gbr_best_split(struct isl_context *context,
2803                 struct isl_tab *tab)
2804 {
2805         struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
2806         struct isl_tab_undo *snap;
2807         int r;
2808
2809         snap = isl_tab_snap(cgbr->tab);
2810         r = best_split(tab, cgbr->tab);
2811
2812         if (isl_tab_rollback(cgbr->tab, snap) < 0)
2813                 return -1;
2814
2815         return r;
2816 }
2817
2818 static int context_gbr_is_empty(struct isl_context *context)
2819 {
2820         struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
2821         if (!cgbr->tab)
2822                 return -1;
2823         return cgbr->tab->empty;
2824 }
2825
2826 struct isl_gbr_tab_undo {
2827         struct isl_tab_undo *tab_snap;
2828         struct isl_tab_undo *shifted_snap;
2829         struct isl_tab_undo *cone_snap;
2830 };
2831
2832 static void *context_gbr_save(struct isl_context *context)
2833 {
2834         struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
2835         struct isl_gbr_tab_undo *snap;
2836
2837         snap = isl_alloc_type(cgbr->tab->mat->ctx, struct isl_gbr_tab_undo);
2838         if (!snap)
2839                 return NULL;
2840
2841         snap->tab_snap = isl_tab_snap(cgbr->tab);
2842         if (isl_tab_save_samples(cgbr->tab) < 0)
2843                 goto error;
2844
2845         if (cgbr->shifted)
2846                 snap->shifted_snap = isl_tab_snap(cgbr->shifted);
2847         else
2848                 snap->shifted_snap = NULL;
2849
2850         if (cgbr->cone)
2851                 snap->cone_snap = isl_tab_snap(cgbr->cone);
2852         else
2853                 snap->cone_snap = NULL;
2854
2855         return snap;
2856 error:
2857         free(snap);
2858         return NULL;
2859 }
2860
2861 static void context_gbr_restore(struct isl_context *context, void *save)
2862 {
2863         struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
2864         struct isl_gbr_tab_undo *snap = (struct isl_gbr_tab_undo *)save;
2865         if (!snap)
2866                 goto error;
2867         if (isl_tab_rollback(cgbr->tab, snap->tab_snap) < 0) {
2868                 isl_tab_free(cgbr->tab);
2869                 cgbr->tab = NULL;
2870         }
2871
2872         if (snap->shifted_snap) {
2873                 if (isl_tab_rollback(cgbr->shifted, snap->shifted_snap) < 0)
2874                         goto error;
2875         } else if (cgbr->shifted) {
2876                 isl_tab_free(cgbr->shifted);
2877                 cgbr->shifted = NULL;
2878         }
2879
2880         if (snap->cone_snap) {
2881                 if (isl_tab_rollback(cgbr->cone, snap->cone_snap) < 0)
2882                         goto error;
2883         } else if (cgbr->cone) {
2884                 isl_tab_free(cgbr->cone);
2885                 cgbr->cone = NULL;
2886         }
2887
2888         free(snap);
2889
2890         return;
2891 error:
2892         free(snap);
2893         isl_tab_free(cgbr->tab);
2894         cgbr->tab = NULL;
2895 }
2896
2897 static int context_gbr_is_ok(struct isl_context *context)
2898 {
2899         struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
2900         return !!cgbr->tab;
2901 }
2902
2903 static void context_gbr_invalidate(struct isl_context *context)
2904 {
2905         struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
2906         isl_tab_free(cgbr->tab);
2907         cgbr->tab = NULL;
2908 }
2909
2910 static void context_gbr_free(struct isl_context *context)
2911 {
2912         struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
2913         isl_tab_free(cgbr->tab);
2914         isl_tab_free(cgbr->shifted);
2915         isl_tab_free(cgbr->cone);
2916         free(cgbr);
2917 }
2918
2919 struct isl_context_op isl_context_gbr_op = {
2920         context_gbr_detect_nonnegative_parameters,
2921         context_gbr_peek_basic_set,
2922         context_gbr_peek_tab,
2923         context_gbr_add_eq,
2924         context_gbr_add_ineq,
2925         context_gbr_ineq_sign,
2926         context_gbr_test_ineq,
2927         context_gbr_get_div,
2928         context_gbr_add_div,
2929         context_gbr_detect_equalities,
2930         context_gbr_best_split,
2931         context_gbr_is_empty,
2932         context_gbr_is_ok,
2933         context_gbr_save,
2934         context_gbr_restore,
2935         context_gbr_invalidate,
2936         context_gbr_free,
2937 };
2938
2939 static struct isl_context *isl_context_gbr_alloc(struct isl_basic_set *dom)
2940 {
2941         struct isl_context_gbr *cgbr;
2942
2943         if (!dom)
2944                 return NULL;
2945
2946         cgbr = isl_calloc_type(dom->ctx, struct isl_context_gbr);
2947         if (!cgbr)
2948                 return NULL;
2949
2950         cgbr->context.op = &isl_context_gbr_op;
2951
2952         cgbr->shifted = NULL;
2953         cgbr->cone = NULL;
2954         cgbr->tab = isl_tab_from_basic_set(dom);
2955         cgbr->tab = isl_tab_init_samples(cgbr->tab);
2956         if (!cgbr->tab)
2957                 goto error;
2958         cgbr->tab->bset = isl_basic_set_cow(isl_basic_set_copy(dom));
2959         if (!cgbr->tab->bset)
2960                 goto error;
2961         check_gbr_integer_feasible(cgbr);
2962
2963         return &cgbr->context;
2964 error:
2965         cgbr->context.op->free(&cgbr->context);
2966         return NULL;
2967 }
2968
2969 static struct isl_context *isl_context_alloc(struct isl_basic_set *dom)
2970 {
2971         if (!dom)
2972                 return NULL;
2973
2974         if (dom->ctx->context == ISL_CONTEXT_LEXMIN)
2975                 return isl_context_lex_alloc(dom);
2976         else
2977                 return isl_context_gbr_alloc(dom);
2978 }
2979
2980 /* Construct an isl_sol_map structure for accumulating the solution.
2981  * If track_empty is set, then we also keep track of the parts
2982  * of the context where there is no solution.
2983  * If max is set, then we are solving a maximization, rather than
2984  * a minimization problem, which means that the variables in the
2985  * tableau have value "M - x" rather than "M + x".
2986  */
2987 static struct isl_sol_map *sol_map_init(struct isl_basic_map *bmap,
2988         struct isl_basic_set *dom, int track_empty, int max)
2989 {
2990         struct isl_sol_map *sol_map;
2991
2992         sol_map = isl_calloc_type(bset->ctx, struct isl_sol_map);
2993         if (!sol_map)
2994                 goto error;
2995
2996         sol_map->sol.max = max;
2997         sol_map->sol.n_out = isl_basic_map_dim(bmap, isl_dim_out);
2998         sol_map->sol.add = &sol_map_add_wrap;
2999         sol_map->sol.add_empty = track_empty ? &sol_map_add_empty_wrap : NULL;
3000         sol_map->sol.free = &sol_map_free_wrap;
3001         sol_map->map = isl_map_alloc_dim(isl_basic_map_get_dim(bmap), 1,
3002                                             ISL_MAP_DISJOINT);
3003         if (!sol_map->map)
3004                 goto error;
3005
3006         sol_map->sol.context = isl_context_alloc(dom);
3007         if (!sol_map->sol.context)
3008                 goto error;
3009
3010         if (track_empty) {
3011                 sol_map->empty = isl_set_alloc_dim(isl_basic_set_get_dim(dom),
3012                                                         1, ISL_SET_DISJOINT);
3013                 if (!sol_map->empty)
3014                         goto error;
3015         }
3016
3017         isl_basic_set_free(dom);
3018         return sol_map;
3019 error:
3020         isl_basic_set_free(dom);
3021         sol_map_free(sol_map);
3022         return NULL;
3023 }
3024
3025 /* Check whether all coefficients of (non-parameter) variables
3026  * are non-positive, meaning that no pivots can be performed on the row.
3027  */
3028 static int is_critical(struct isl_tab *tab, int row)
3029 {
3030         int j;
3031         unsigned off = 2 + tab->M;
3032
3033         for (j = tab->n_dead; j < tab->n_col; ++j) {
3034                 if (tab->col_var[j] >= 0 &&
3035                     (tab->col_var[j] < tab->n_param  ||
3036                     tab->col_var[j] >= tab->n_var - tab->n_div))
3037                         continue;
3038
3039                 if (isl_int_is_pos(tab->mat->row[row][off + j]))
3040                         return 0;
3041         }
3042
3043         return 1;
3044 }
3045
3046 /* Check whether the inequality represented by vec is strict over the integers,
3047  * i.e., there are no integer values satisfying the constraint with
3048  * equality.  This happens if the gcd of the coefficients is not a divisor
3049  * of the constant term.  If so, scale the constraint down by the gcd
3050  * of the coefficients.
3051  */
3052 static int is_strict(struct isl_vec *vec)
3053 {
3054         isl_int gcd;
3055         int strict = 0;
3056
3057         isl_int_init(gcd);
3058         isl_seq_gcd(vec->el + 1, vec->size - 1, &gcd);
3059         if (!isl_int_is_one(gcd)) {
3060                 strict = !isl_int_is_divisible_by(vec->el[0], gcd);
3061                 isl_int_fdiv_q(vec->el[0], vec->el[0], gcd);
3062                 isl_seq_scale_down(vec->el + 1, vec->el + 1, gcd, vec->size-1);
3063         }
3064         isl_int_clear(gcd);
3065
3066         return strict;
3067 }
3068
3069 /* Determine the sign of the given row of the main tableau.
3070  * The result is one of
3071  *      isl_tab_row_pos: always non-negative; no pivot needed
3072  *      isl_tab_row_neg: always non-positive; pivot
3073  *      isl_tab_row_any: can be both positive and negative; split
3074  *
3075  * We first handle some simple cases
3076  *      - the row sign may be known already
3077  *      - the row may be obviously non-negative
3078  *      - the parametric constant may be equal to that of another row
3079  *        for which we know the sign.  This sign will be either "pos" or
3080  *        "any".  If it had been "neg" then we would have pivoted before.
3081  *
3082  * If none of these cases hold, we check the value of the row for each
3083  * of the currently active samples.  Based on the signs of these values
3084  * we make an initial determination of the sign of the row.
3085  *
3086  *      all zero                        ->      unk(nown)
3087  *      all non-negative                ->      pos
3088  *      all non-positive                ->      neg
3089  *      both negative and positive      ->      all
3090  *
3091  * If we end up with "all", we are done.
3092  * Otherwise, we perform a check for positive and/or negative
3093  * values as follows.
3094  *
3095  *      samples        neg             unk             pos
3096  *      <0 ?                        Y        N      Y        N
3097  *                                          pos    any      pos
3098  *      >0 ?         Y      N    Y     N
3099  *                  any    neg  any   neg
3100  *
3101  * There is no special sign for "zero", because we can usually treat zero
3102  * as either non-negative or non-positive, whatever works out best.
3103  * However, if the row is "critical", meaning that pivoting is impossible
3104  * then we don't want to limp zero with the non-positive case, because
3105  * then we we would lose the solution for those values of the parameters
3106  * where the value of the row is zero.  Instead, we treat 0 as non-negative
3107  * ensuring a split if the row can attain both zero and negative values.
3108  * The same happens when the original constraint was one that could not
3109  * be satisfied with equality by any integer values of the parameters.
3110  * In this case, we normalize the constraint, but then a value of zero
3111  * for the normalized constraint is actually a positive value for the
3112  * original constraint, so again we need to treat zero as non-negative.
3113  * In both these cases, we have the following decision tree instead:
3114  *
3115  *      all non-negative                ->      pos
3116  *      all negative                    ->      neg
3117  *      both negative and non-negative  ->      all
3118  *
3119  *      samples        neg                             pos
3120  *      <0 ?                                        Y        N
3121  *                                                 any      pos
3122  *      >=0 ?        Y      N
3123  *                  any    neg
3124  */
3125 static enum isl_tab_row_sign row_sign(struct isl_tab *tab,
3126         struct isl_sol *sol, int row)
3127 {
3128         struct isl_vec *ineq = NULL;
3129         int res = isl_tab_row_unknown;
3130         int critical;
3131         int strict;
3132         int row2;
3133
3134         if (tab->row_sign[row] != isl_tab_row_unknown)
3135                 return tab->row_sign[row];
3136         if (is_obviously_nonneg(tab, row))
3137                 return isl_tab_row_pos;
3138         for (row2 = tab->n_redundant; row2 < tab->n_row; ++row2) {
3139                 if (tab->row_sign[row2] == isl_tab_row_unknown)
3140                         continue;
3141                 if (identical_parameter_line(tab, row, row2))
3142                         return tab->row_sign[row2];
3143         }
3144
3145         critical = is_critical(tab, row);
3146
3147         ineq = get_row_parameter_ineq(tab, row);
3148         if (!ineq)
3149                 goto error;
3150
3151         strict = is_strict(ineq);
3152
3153         res = sol->context->op->ineq_sign(sol->context, ineq->el,
3154                                           critical || strict);
3155
3156         if (res == isl_tab_row_unknown || res == isl_tab_row_pos) {
3157                 /* test for negative values */
3158                 int feasible;
3159                 isl_seq_neg(ineq->el, ineq->el, ineq->size);
3160                 isl_int_sub_ui(ineq->el[0], ineq->el[0], 1);
3161
3162                 feasible = sol->context->op->test_ineq(sol->context, ineq->el);
3163                 if (feasible < 0)
3164                         goto error;
3165                 if (!feasible)
3166                         res = isl_tab_row_pos;
3167                 else
3168                         res = (res == isl_tab_row_unknown) ? isl_tab_row_neg
3169                                                            : isl_tab_row_any;
3170                 if (res == isl_tab_row_neg) {
3171                         isl_seq_neg(ineq->el, ineq->el, ineq->size);
3172                         isl_int_sub_ui(ineq->el[0], ineq->el[0], 1);
3173                 }
3174         }
3175
3176         if (res == isl_tab_row_neg) {
3177                 /* test for positive values */
3178                 int feasible;
3179                 if (!critical && !strict)
3180                         isl_int_sub_ui(ineq->el[0], ineq->el[0], 1);
3181
3182                 feasible = sol->context->op->test_ineq(sol->context, ineq->el);
3183                 if (feasible < 0)
3184                         goto error;
3185                 if (feasible)
3186                         res = isl_tab_row_any;
3187         }
3188
3189         isl_vec_free(ineq);
3190         return res;
3191 error:
3192         isl_vec_free(ineq);
3193         return 0;
3194 }
3195
3196 static void find_solutions(struct isl_sol *sol, struct isl_tab *tab);
3197
3198 /* Find solutions for values of the parameters that satisfy the given
3199  * inequality.
3200  *
3201  * We currently take a snapshot of the context tableau that is reset
3202  * when we return from this function, while we make a copy of the main
3203  * tableau, leaving the original main tableau untouched.
3204  * These are fairly arbitrary choices.  Making a copy also of the context
3205  * tableau would obviate the need to undo any changes made to it later,
3206  * while taking a snapshot of the main tableau could reduce memory usage.
3207  * If we were to switch to taking a snapshot of the main tableau,
3208  * we would have to keep in mind that we need to save the row signs
3209  * and that we need to do this before saving the current basis
3210  * such that the basis has been restore before we restore the row signs.
3211  */
3212 static void find_in_pos(struct isl_sol *sol, struct isl_tab *tab, isl_int *ineq)
3213 {
3214         void *saved;
3215
3216         if (!sol->context)
3217                 goto error;
3218         saved = sol->context->op->save(sol->context);
3219
3220         tab = isl_tab_dup(tab);
3221         if (!tab)
3222                 goto error;
3223
3224         sol->context->op->add_ineq(sol->context, ineq, 0, 1);
3225
3226         find_solutions(sol, tab);
3227
3228         sol->context->op->restore(sol->context, saved);
3229         return;
3230 error:
3231         sol->error = 1;
3232 }
3233
3234 /* Record the absence of solutions for those values of the parameters
3235  * that do not satisfy the given inequality with equality.
3236  */
3237 static void no_sol_in_strict(struct isl_sol *sol,
3238         struct isl_tab *tab, struct isl_vec *ineq)
3239 {
3240         int empty;
3241         void *saved;
3242
3243         if (!sol->context)
3244                 goto error;
3245         saved = sol->context->op->save(sol->context);
3246
3247         isl_int_sub_ui(ineq->el[0], ineq->el[0], 1);
3248
3249         sol->context->op->add_ineq(sol->context, ineq->el, 1, 0);
3250         if (!sol->context)
3251                 goto error;
3252
3253         empty = tab->empty;
3254         tab->empty = 1;
3255         sol_add(sol, tab);
3256         tab->empty = empty;
3257
3258         isl_int_add_ui(ineq->el[0], ineq->el[0], 1);
3259
3260         sol->context->op->restore(sol->context, saved);
3261         return;
3262 error:
3263         sol->error = 1;
3264 }
3265
3266 /* Compute the lexicographic minimum of the set represented by the main
3267  * tableau "tab" within the context "sol->context_tab".
3268  * On entry the sample value of the main tableau is lexicographically
3269  * less than or equal to this lexicographic minimum.
3270  * Pivots are performed until a feasible point is found, which is then
3271  * necessarily equal to the minimum, or until the tableau is found to
3272  * be infeasible.  Some pivots may need to be performed for only some
3273  * feasible values of the context tableau.  If so, the context tableau
3274  * is split into a part where the pivot is needed and a part where it is not.
3275  *
3276  * Whenever we enter the main loop, the main tableau is such that no
3277  * "obvious" pivots need to be performed on it, where "obvious" means
3278  * that the given row can be seen to be negative without looking at
3279  * the context tableau.  In particular, for non-parametric problems,
3280  * no pivots need to be performed on the main tableau.
3281  * The caller of find_solutions is responsible for making this property
3282  * hold prior to the first iteration of the loop, while restore_lexmin
3283  * is called before every other iteration.
3284  *
3285  * Inside the main loop, we first examine the signs of the rows of
3286  * the main tableau within the context of the context tableau.
3287  * If we find a row that is always non-positive for all values of
3288  * the parameters satisfying the context tableau and negative for at
3289  * least one value of the parameters, we perform the appropriate pivot
3290  * and start over.  An exception is the case where no pivot can be
3291  * performed on the row.  In this case, we require that the sign of
3292  * the row is negative for all values of the parameters (rather than just
3293  * non-positive).  This special case is handled inside row_sign, which
3294  * will say that the row can have any sign if it determines that it can
3295  * attain both negative and zero values.
3296  *
3297  * If we can't find a row that always requires a pivot, but we can find
3298  * one or more rows that require a pivot for some values of the parameters
3299  * (i.e., the row can attain both positive and negative signs), then we split
3300  * the context tableau into two parts, one where we force the sign to be
3301  * non-negative and one where we force is to be negative.
3302  * The non-negative part is handled by a recursive call (through find_in_pos).
3303  * Upon returning from this call, we continue with the negative part and
3304  * perform the required pivot.
3305  *
3306  * If no such rows can be found, all rows are non-negative and we have
3307  * found a (rational) feasible point.  If we only wanted a rational point
3308  * then we are done.
3309  * Otherwise, we check if all values of the sample point of the tableau
3310  * are integral for the variables.  If so, we have found the minimal
3311  * integral point and we are done.
3312  * If the sample point is not integral, then we need to make a distinction
3313  * based on whether the constant term is non-integral or the coefficients
3314  * of the parameters.  Furthermore, in order to decide how to handle
3315  * the non-integrality, we also need to know whether the coefficients
3316  * of the other columns in the tableau are integral.  This leads
3317  * to the following table.  The first two rows do not correspond
3318  * to a non-integral sample point and are only mentioned for completeness.
3319  *
3320  *      constant        parameters      other
3321  *
3322  *      int             int             int     |
3323  *      int             int             rat     | -> no problem
3324  *
3325  *      rat             int             int       -> fail
3326  *
3327  *      rat             int             rat       -> cut
3328  *
3329  *      int             rat             rat     |
3330  *      rat             rat             rat     | -> parametric cut
3331  *
3332  *      int             rat             int     |
3333  *      rat             rat             int     | -> split context
3334  *
3335  * If the parametric constant is completely integral, then there is nothing
3336  * to be done.  If the constant term is non-integral, but all the other
3337  * coefficient are integral, then there is nothing that can be done
3338  * and the tableau has no integral solution.
3339  * If, on the other hand, one or more of the other columns have rational
3340  * coeffcients, but the parameter coefficients are all integral, then
3341  * we can perform a regular (non-parametric) cut.
3342  * Finally, if there is any parameter coefficient that is non-integral,
3343  * then we need to involve the context tableau.  There are two cases here.
3344  * If at least one other column has a rational coefficient, then we
3345  * can perform a parametric cut in the main tableau by adding a new
3346  * integer division in the context tableau.
3347  * If all other columns have integral coefficients, then we need to
3348  * enforce that the rational combination of parameters (c + \sum a_i y_i)/m
3349  * is always integral.  We do this by introducing an integer division
3350  * q = floor((c + \sum a_i y_i)/m) and stipulating that its argument should
3351  * always be integral in the context tableau, i.e., m q = c + \sum a_i y_i.
3352  * Since q is expressed in the tableau as
3353  *      c + \sum a_i y_i - m q >= 0
3354  *      -c - \sum a_i y_i + m q + m - 1 >= 0
3355  * it is sufficient to add the inequality
3356  *      -c - \sum a_i y_i + m q >= 0
3357  * In the part of the context where this inequality does not hold, the
3358  * main tableau is marked as being empty.
3359  */
3360 static void find_solutions(struct isl_sol *sol, struct isl_tab *tab)
3361 {
3362         struct isl_context *context;
3363
3364         if (!tab || sol->error)
3365                 goto error;
3366
3367         context = sol->context;
3368
3369         if (tab->empty)
3370                 goto done;
3371         if (context->op->is_empty(context))
3372                 goto done;
3373
3374         for (; tab && !tab->empty; tab = restore_lexmin(tab)) {
3375                 int flags;
3376                 int row;
3377                 int sgn;
3378                 int split = -1;
3379                 int n_split = 0;
3380
3381                 for (row = tab->n_redundant; row < tab->n_row; ++row) {
3382                         if (!isl_tab_var_from_row(tab, row)->is_nonneg)
3383                                 continue;
3384                         sgn = row_sign(tab, sol, row);
3385                         if (!sgn)
3386                                 goto error;
3387                         tab->row_sign[row] = sgn;
3388                         if (sgn == isl_tab_row_any)
3389                                 n_split++;
3390                         if (sgn == isl_tab_row_any && split == -1)
3391                                 split = row;
3392                         if (sgn == isl_tab_row_neg)
3393                                 break;
3394                 }
3395                 if (row < tab->n_row)
3396                         continue;
3397                 if (split != -1) {
3398                         struct isl_vec *ineq;
3399                         if (n_split != 1)
3400                                 split = context->op->best_split(context, tab);
3401                         if (split < 0)
3402                                 goto error;
3403                         ineq = get_row_parameter_ineq(tab, split);
3404                         if (!ineq)
3405                                 goto error;
3406                         is_strict(ineq);
3407                         for (row = tab->n_redundant; row < tab->n_row; ++row) {
3408                                 if (!isl_tab_var_from_row(tab, row)->is_nonneg)
3409                                         continue;
3410                                 if (tab->row_sign[row] == isl_tab_row_any)
3411                                         tab->row_sign[row] = isl_tab_row_unknown;
3412                         }
3413                         tab->row_sign[split] = isl_tab_row_pos;
3414                         find_in_pos(sol, tab, ineq->el);
3415                         tab->row_sign[split] = isl_tab_row_neg;
3416                         row = split;
3417                         isl_seq_neg(ineq->el, ineq->el, ineq->size);
3418                         isl_int_sub_ui(ineq->el[0], ineq->el[0], 1);
3419                         context->op->add_ineq(context, ineq->el, 0, 1);
3420                         isl_vec_free(ineq);
3421                         if (sol->error)
3422                                 goto error;
3423                         continue;
3424                 }
3425                 if (tab->rational)
3426                         break;
3427                 row = first_non_integer(tab, &flags);
3428                 if (row < 0)
3429                         break;
3430                 if (ISL_FL_ISSET(flags, I_PAR)) {
3431                         if (ISL_FL_ISSET(flags, I_VAR)) {
3432                                 tab = isl_tab_mark_empty(tab);
3433                                 break;
3434                         }
3435                         row = add_cut(tab, row);
3436                 } else if (ISL_FL_ISSET(flags, I_VAR)) {
3437                         struct isl_vec *div;
3438                         struct isl_vec *ineq;
3439                         int d;
3440                         div = get_row_split_div(tab, row);
3441                         if (!div)
3442                                 goto error;
3443                         d = context->op->get_div(context, tab, div);
3444                         isl_vec_free(div);
3445                         if (d < 0)
3446                                 goto error;
3447                         ineq = ineq_for_div(context->op->peek_basic_set(context), d);
3448                         no_sol_in_strict(sol, tab, ineq);
3449                         isl_seq_neg(ineq->el, ineq->el, ineq->size);
3450                         context->op->add_ineq(context, ineq->el, 1, 1);
3451                         isl_vec_free(ineq);
3452                         if (sol->error || !context->op->is_ok(context))
3453                                 goto error;
3454                         tab = set_row_cst_to_div(tab, row, d);
3455                 } else
3456                         row = add_parametric_cut(tab, row, context);
3457                 if (row < 0)
3458                         goto error;
3459         }
3460 done:
3461         sol_add(sol, tab);
3462         isl_tab_free(tab);
3463         return;
3464 error:
3465         isl_tab_free(tab);
3466         sol_free(sol);
3467 }
3468
3469 /* Compute the lexicographic minimum of the set represented by the main
3470  * tableau "tab" within the context "sol->context_tab".
3471  *
3472  * As a preprocessing step, we first transfer all the purely parametric
3473  * equalities from the main tableau to the context tableau, i.e.,
3474  * parameters that have been pivoted to a row.
3475  * These equalities are ignored by the main algorithm, because the
3476  * corresponding rows may not be marked as being non-negative.
3477  * In parts of the context where the added equality does not hold,
3478  * the main tableau is marked as being empty.
3479  */
3480 static void find_solutions_main(struct isl_sol *sol, struct isl_tab *tab)
3481 {
3482         int row;
3483
3484         for (row = tab->n_redundant; row < tab->n_row; ++row) {
3485                 int p;
3486                 struct isl_vec *eq;
3487
3488                 if (tab->row_var[row] < 0)
3489                         continue;
3490                 if (tab->row_var[row] >= tab->n_param &&
3491                     tab->row_var[row] < tab->n_var - tab->n_div)
3492                         continue;
3493                 if (tab->row_var[row] < tab->n_param)
3494                         p = tab->row_var[row];
3495                 else
3496                         p = tab->row_var[row]
3497                                 + tab->n_param - (tab->n_var - tab->n_div);
3498
3499                 eq = isl_vec_alloc(tab->mat->ctx, 1+tab->n_param+tab->n_div);
3500                 get_row_parameter_line(tab, row, eq->el);
3501                 isl_int_neg(eq->el[1 + p], tab->mat->row[row][0]);
3502                 eq = isl_vec_normalize(eq);
3503
3504                 no_sol_in_strict(sol, tab, eq);
3505
3506                 isl_seq_neg(eq->el, eq->el, eq->size);
3507                 no_sol_in_strict(sol, tab, eq);
3508                 isl_seq_neg(eq->el, eq->el, eq->size);
3509
3510                 sol->context->op->add_eq(sol->context, eq->el, 1, 1);
3511
3512                 isl_vec_free(eq);
3513
3514                 if (isl_tab_mark_redundant(tab, row) < 0)
3515                         goto error;
3516
3517                 if (sol->context->op->is_empty(sol->context))
3518                         break;
3519
3520                 row = tab->n_redundant - 1;
3521         }
3522
3523         find_solutions(sol, tab);
3524         return;
3525 error:
3526         isl_tab_free(tab);
3527         sol_free(sol);
3528 }
3529
3530 static void sol_map_find_solutions(struct isl_sol_map *sol_map,
3531         struct isl_tab *tab)
3532 {
3533         find_solutions_main(&sol_map->sol, tab);
3534 }
3535
3536 /* Check if integer division "div" of "dom" also occurs in "bmap".
3537  * If so, return its position within the divs.
3538  * If not, return -1.
3539  */
3540 static int find_context_div(struct isl_basic_map *bmap,
3541         struct isl_basic_set *dom, unsigned div)
3542 {
3543         int i;
3544         unsigned b_dim = isl_dim_total(bmap->dim);
3545         unsigned d_dim = isl_dim_total(dom->dim);
3546
3547         if (isl_int_is_zero(dom->div[div][0]))
3548                 return -1;
3549         if (isl_seq_first_non_zero(dom->div[div] + 2 + d_dim, dom->n_div) != -1)
3550                 return -1;
3551
3552         for (i = 0; i < bmap->n_div; ++i) {
3553                 if (isl_int_is_zero(bmap->div[i][0]))
3554                         continue;
3555                 if (isl_seq_first_non_zero(bmap->div[i] + 2 + d_dim,
3556                                            (b_dim - d_dim) + bmap->n_div) != -1)
3557                         continue;
3558                 if (isl_seq_eq(bmap->div[i], dom->div[div], 2 + d_dim))
3559                         return i;
3560         }
3561         return -1;
3562 }
3563
3564 /* The correspondence between the variables in the main tableau,
3565  * the context tableau, and the input map and domain is as follows.
3566  * The first n_param and the last n_div variables of the main tableau
3567  * form the variables of the context tableau.
3568  * In the basic map, these n_param variables correspond to the
3569  * parameters and the input dimensions.  In the domain, they correspond
3570  * to the parameters and the set dimensions.
3571  * The n_div variables correspond to the integer divisions in the domain.
3572  * To ensure that everything lines up, we may need to copy some of the
3573  * integer divisions of the domain to the map.  These have to be placed
3574  * in the same order as those in the context and they have to be placed
3575  * after any other integer divisions that the map may have.
3576  * This function performs the required reordering.
3577  */
3578 static struct isl_basic_map *align_context_divs(struct isl_basic_map *bmap,
3579         struct isl_basic_set *dom)
3580 {
3581         int i;
3582         int common = 0;
3583         int other;
3584
3585         for (i = 0; i < dom->n_div; ++i)
3586                 if (find_context_div(bmap, dom, i) != -1)
3587                         common++;
3588         other = bmap->n_div - common;
3589         if (dom->n_div - common > 0) {
3590                 bmap = isl_basic_map_extend_dim(bmap, isl_dim_copy(bmap->dim),
3591                                 dom->n_div - common, 0, 0);
3592                 if (!bmap)
3593                         return NULL;
3594         }
3595         for (i = 0; i < dom->n_div; ++i) {
3596                 int pos = find_context_div(bmap, dom, i);
3597                 if (pos < 0) {
3598                         pos = isl_basic_map_alloc_div(bmap);
3599                         if (pos < 0)
3600                                 goto error;
3601                         isl_int_set_si(bmap->div[pos][0], 0);
3602                 }
3603                 if (pos != other + i)
3604                         isl_basic_map_swap_div(bmap, pos, other + i);
3605         }
3606         return bmap;
3607 error:
3608         isl_basic_map_free(bmap);
3609         return NULL;
3610 }
3611
3612 /* Compute the lexicographic minimum (or maximum if "max" is set)
3613  * of "bmap" over the domain "dom" and return the result as a map.
3614  * If "empty" is not NULL, then *empty is assigned a set that
3615  * contains those parts of the domain where there is no solution.
3616  * If "bmap" is marked as rational (ISL_BASIC_MAP_RATIONAL),
3617  * then we compute the rational optimum.  Otherwise, we compute
3618  * the integral optimum.
3619  *
3620  * We perform some preprocessing.  As the PILP solver does not
3621  * handle implicit equalities very well, we first make sure all
3622  * the equalities are explicitly available.
3623  * We also make sure the divs in the domain are properly order,
3624  * because they will be added one by one in the given order
3625  * during the construction of the solution map.
3626  */
3627 struct isl_map *isl_tab_basic_map_partial_lexopt(
3628                 struct isl_basic_map *bmap, struct isl_basic_set *dom,
3629                 struct isl_set **empty, int max)
3630 {
3631         struct isl_tab *tab;
3632         struct isl_map *result = NULL;
3633         struct isl_sol_map *sol_map = NULL;
3634         struct isl_context *context;
3635
3636         if (empty)
3637                 *empty = NULL;
3638         if (!bmap || !dom)
3639                 goto error;
3640
3641         isl_assert(bmap->ctx,
3642             isl_basic_map_compatible_domain(bmap, dom), goto error);
3643
3644         bmap = isl_basic_map_detect_equalities(bmap);
3645
3646         if (dom->n_div) {
3647                 dom = isl_basic_set_order_divs(dom);
3648                 bmap = align_context_divs(bmap, dom);
3649         }
3650         sol_map = sol_map_init(bmap, dom, !!empty, max);
3651         if (!sol_map)
3652                 goto error;
3653
3654         context = sol_map->sol.context;
3655         if (isl_basic_set_fast_is_empty(context->op->peek_basic_set(context)))
3656                 /* nothing */;
3657         else if (isl_basic_map_fast_is_empty(bmap))
3658                 sol_map_add_empty(sol_map,
3659                     isl_basic_set_dup(context->op->peek_basic_set(context)));
3660         else {
3661                 tab = tab_for_lexmin(bmap,
3662                                     context->op->peek_basic_set(context), 1, max);
3663                 tab = context->op->detect_nonnegative_parameters(context, tab);
3664                 sol_map_find_solutions(sol_map, tab);
3665         }
3666         if (sol_map->sol.error)
3667                 goto error;
3668
3669         result = isl_map_copy(sol_map->map);
3670         if (empty)
3671                 *empty = isl_set_copy(sol_map->empty);
3672         sol_free(&sol_map->sol);
3673         isl_basic_map_free(bmap);
3674         return result;
3675 error:
3676         sol_free(&sol_map->sol);
3677         isl_basic_map_free(bmap);
3678         return NULL;
3679 }
3680
3681 struct isl_sol_for {
3682         struct isl_sol  sol;
3683         int             (*fn)(__isl_take isl_basic_set *dom,
3684                                 __isl_take isl_mat *map, void *user);
3685         void            *user;
3686 };
3687
3688 static void sol_for_free(struct isl_sol_for *sol_for)
3689 {
3690         if (sol_for->sol.context)
3691                 sol_for->sol.context->op->free(sol_for->sol.context);
3692         free(sol_for);
3693 }
3694
3695 static void sol_for_free_wrap(struct isl_sol *sol)
3696 {
3697         sol_for_free((struct isl_sol_for *)sol);
3698 }
3699
3700 /* Add the solution identified by the tableau and the context tableau.
3701  *
3702  * See documentation of sol_add for more details.
3703  *
3704  * Instead of constructing a basic map, this function calls a user
3705  * defined function with the current context as a basic set and
3706  * an affine matrix reprenting the relation between the input and output.
3707  * The number of rows in this matrix is equal to one plus the number
3708  * of output variables.  The number of columns is equal to one plus
3709  * the total dimension of the context, i.e., the number of parameters,
3710  * input variables and divs.  Since some of the columns in the matrix
3711  * may refer to the divs, the basic set is not simplified.
3712  * (Simplification may reorder or remove divs.)
3713  */
3714 static void sol_for_add(struct isl_sol_for *sol,
3715         struct isl_basic_set *dom, struct isl_mat *M)
3716 {
3717         if (sol->sol.error || !dom || !M)
3718                 goto error;
3719
3720         dom = isl_basic_set_simplify(dom);
3721         dom = isl_basic_set_finalize(dom);
3722
3723         if (sol->fn(isl_basic_set_copy(dom), isl_mat_copy(M), sol->user) < 0)
3724                 goto error;
3725
3726         isl_basic_set_free(dom);
3727         isl_mat_free(M);
3728         return;
3729 error:
3730         isl_basic_set_free(dom);
3731         isl_mat_free(M);
3732         sol->sol.error = 1;
3733 }
3734
3735 static void sol_for_add_wrap(struct isl_sol *sol,
3736         struct isl_basic_set *dom, struct isl_mat *M)
3737 {
3738         sol_for_add((struct isl_sol_for *)sol, dom, M);
3739 }
3740
3741 static struct isl_sol_for *sol_for_init(struct isl_basic_map *bmap, int max,
3742         int (*fn)(__isl_take isl_basic_set *dom, __isl_take isl_mat *map,
3743                   void *user),
3744         void *user)
3745 {
3746         struct isl_sol_for *sol_for = NULL;
3747         struct isl_dim *dom_dim;
3748         struct isl_basic_set *dom = NULL;
3749
3750         sol_for = isl_calloc_type(bset->ctx, struct isl_sol_for);
3751         if (!sol_for)
3752                 goto error;
3753
3754         dom_dim = isl_dim_domain(isl_dim_copy(bmap->dim));
3755         dom = isl_basic_set_universe(dom_dim);
3756
3757         sol_for->fn = fn;
3758         sol_for->user = user;
3759         sol_for->sol.max = max;
3760         sol_for->sol.n_out = isl_basic_map_dim(bmap, isl_dim_out);
3761         sol_for->sol.add = &sol_for_add_wrap;
3762         sol_for->sol.add_empty = NULL;
3763         sol_for->sol.free = &sol_for_free_wrap;
3764
3765         sol_for->sol.context = isl_context_alloc(dom);
3766         if (!sol_for->sol.context)
3767                 goto error;
3768
3769         isl_basic_set_free(dom);
3770         return sol_for;
3771 error:
3772         isl_basic_set_free(dom);
3773         sol_for_free(sol_for);
3774         return NULL;
3775 }
3776
3777 static void sol_for_find_solutions(struct isl_sol_for *sol_for,
3778         struct isl_tab *tab)
3779 {
3780         find_solutions_main(&sol_for->sol, tab);
3781 }
3782
3783 int isl_basic_map_foreach_lexopt(__isl_keep isl_basic_map *bmap, int max,
3784         int (*fn)(__isl_take isl_basic_set *dom, __isl_take isl_mat *map,
3785                   void *user),
3786         void *user)
3787 {
3788         struct isl_sol_for *sol_for = NULL;
3789
3790         bmap = isl_basic_map_copy(bmap);
3791         if (!bmap)
3792                 return -1;
3793
3794         bmap = isl_basic_map_detect_equalities(bmap);
3795         sol_for = sol_for_init(bmap, max, fn, user);
3796
3797         if (isl_basic_map_fast_is_empty(bmap))
3798                 /* nothing */;
3799         else {
3800                 struct isl_tab *tab;
3801                 struct isl_context *context = sol_for->sol.context;
3802                 tab = tab_for_lexmin(bmap,
3803                                 context->op->peek_basic_set(context), 1, max);
3804                 tab = context->op->detect_nonnegative_parameters(context, tab);
3805                 sol_for_find_solutions(sol_for, tab);
3806                 if (sol_for->sol.error)
3807                         goto error;
3808         }
3809
3810         sol_free(&sol_for->sol);
3811         isl_basic_map_free(bmap);
3812         return 0;
3813 error:
3814         sol_free(&sol_for->sol);
3815         isl_basic_map_free(bmap);
3816         return -1;
3817 }
3818
3819 int isl_basic_map_foreach_lexmin(__isl_keep isl_basic_map *bmap,
3820         int (*fn)(__isl_take isl_basic_set *dom, __isl_take isl_mat *map,
3821                   void *user),
3822         void *user)
3823 {
3824         return isl_basic_map_foreach_lexopt(bmap, 0, fn, user);
3825 }
3826
3827 int isl_basic_map_foreach_lexmax(__isl_keep isl_basic_map *bmap,
3828         int (*fn)(__isl_take isl_basic_set *dom, __isl_take isl_mat *map,
3829                   void *user),
3830         void *user)
3831 {
3832         return isl_basic_map_foreach_lexopt(bmap, 1, fn, user);
3833 }