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