isl_tab_pip.c

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