isl_tab_pip.c

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