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