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