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