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