isl_tab_pip.c

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