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