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