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