isl_tab_pip.c

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