isl_tab_pip.c

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