gcc/omega.c

   1 /* Source code for an implementation of the Omega test, an integer
   2    programming algorithm for dependence analysis, by William Pugh,
   3    appeared in Supercomputing '91 and CACM Aug 92.
   4
   5    This code has no license restrictions, and is considered public
   6    domain.
   7
   8    Changes copyright (C) 2005, 2006, 2007 Free Software Foundation, Inc.
   9    Contributed by Sebastian Pop <sebastian.pop@inria.fr>
  10
  11 This file is part of GCC.
  12
  13 GCC is free software; you can redistribute it and/or modify it under
  14 the terms of the GNU General Public License as published by the Free
  15 Software Foundation; either version 3, or (at your option) any later
  16 version.
  17
  18 GCC is distributed in the hope that it will be useful, but WITHOUT ANY
  19 WARRANTY; without even the implied warranty of MERCHANTABILITY or
  20 FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
  21 for more details.
  22
  23 You should have received a copy of the GNU General Public License
  24 along with GCC; see the file COPYING3.  If not see
  25 <http://www.gnu.org/licenses/>.  */
  26
  27 /* For a detailed description, see "Constraint-Based Array Dependence
  28    Analysis" William Pugh, David Wonnacott, TOPLAS'98 and David
  29    Wonnacott's thesis:
  30    ftp://ftp.cs.umd.edu/pub/omega/davewThesis/davewThesis.ps.gz
  31 */
  32
  33 #include "config.h"
  34 #include "system.h"
  35 #include "coretypes.h"
  36 #include "tm.h"
  37 #include "errors.h"
  38 #include "ggc.h"
  39 #include "tree.h"
  40 #include "diagnostic.h"
  41 #include "varray.h"
  42 #include "tree-pass.h"
  43 #include "omega.h"
  44
  45 /* When set to true, keep substitution variables.  When set to false,
  46    resurrect substitution variables (convert substitutions back to EQs).  */
  47 static bool omega_reduce_with_subs = true;
  48
  49 /* When set to true, omega_simplify_problem checks for problem with no
  50    solutions, calling verify_omega_pb.  */
  51 static bool omega_verify_simplification = false;
  52
  53 /* When set to true, only produce a single simplified result.  */
  54 static bool omega_single_result = false;
  55
  56 /* Set return_single_result to 1 when omega_single_result is true.  */
  57 static int return_single_result = 0;
  58
  59 /* Hash table for equations generated by the solver.  */
  60 #define HASH_TABLE_SIZE PARAM_VALUE (PARAM_OMEGA_HASH_TABLE_SIZE)
  61 #define MAX_KEYS PARAM_VALUE (PARAM_OMEGA_MAX_KEYS)
  62 static eqn hash_master;
  63 static int next_key;
  64 static int hash_version = 0;
  65
  66 /* Set to true for making the solver enter in approximation mode.  */
  67 static bool in_approximate_mode = false;
  68
  69 /* When set to zero, the solver is allowed to add new equalities to
  70    the problem to be solved.  */
  71 static int conservative = 0;
  72
  73 /* Set to omega_true when the problem was successfully reduced, set to
  74    omega_unknown when the solver is unable to determine an answer.  */
  75 static enum omega_result omega_found_reduction;
  76
  77 /* Set to true when the solver is allowed to add omega_red equations.  */
  78 static bool create_color = false;
  79
  80 /* Set to nonzero when the problem to be solved can be reduced.  */
  81 static int may_be_red = 0;
  82
  83 /* When false, there should be no substitution equations in the
  84    simplified problem.  */
  85 static int please_no_equalities_in_simplified_problems = 0;
  86
  87 /* Variables names for pretty printing.  */
  88 static char wild_name[200][40];
  89
  90 /* Pointer to the void problem.  */
  91 static omega_pb no_problem = (omega_pb) 0;
  92
  93 /* Pointer to the problem to be solved.  */
  94 static omega_pb original_problem = (omega_pb) 0;
  95
  96
  97 /* Return the integer A divided by B.  */
  98
  99 static inline int
 100 int_div (int a, int b)
 101 {
 102   if (a > 0)
 103     return a/b;
 104   else
 105     return -((-a + b - 1)/b);
 106 }
 107
 108 /* Return the integer A modulo B.  */
 109
 110 static inline int
 111 int_mod (int a, int b)
 112 {
 113   return a - b * int_div (a, b);
 114 }
 115
 116 /* For X and Y positive integers, return X multiplied by Y and check
 117    that the result does not overflow.  */
 118
 119 static inline int
 120 check_pos_mul (int x, int y)
 121 {
 122   if (x != 0)
 123     gcc_assert ((INT_MAX) / x > y);
 124
 125   return x * y;
 126 }
 127
 128 /* Return X multiplied by Y and check that the result does not
 129    overflow.  */
 130
 131 static inline int
 132 check_mul (int x, int y)
 133 {
 134   if (x >= 0)
 135     {
 136       if (y >= 0)
 137         return check_pos_mul (x, y);
 138       else
 139         return -check_pos_mul (x, -y);
 140     }
 141   else if (y >= 0)
 142     return -check_pos_mul (-x, y);
 143   else
 144     return check_pos_mul (-x, -y);
 145 }
 146
 147 /* Test whether equation E is red.  */
 148
 149 static inline bool
 150 omega_eqn_is_red (eqn e, int desired_res)
 151 {
 152   return (desired_res == omega_simplify && e->color == omega_red);
 153 }
 154
 155 /* Return a string for VARIABLE.  */
 156
 157 static inline char *
 158 omega_var_to_str (int variable)
 159 {
 160   if (0 <= variable && variable <= 20)
 161     return wild_name[variable];
 162
 163   if (-20 < variable && variable < 0)
 164     return wild_name[40 + variable];
 165
 166   /* Collapse all the entries that would have overflowed.  */
 167   return wild_name[21];
 168 }
 169
 170 /* Return a string for variable I in problem PB.  */
 171
 172 static inline char *
 173 omega_variable_to_str (omega_pb pb, int i)
 174 {
 175   return omega_var_to_str (pb->var[i]);
 176 }
 177
 178 /* Do nothing function: used for default initializations.  */
 179
 180 void
 181 omega_no_procedure (omega_pb pb ATTRIBUTE_UNUSED)
 182 {
 183 }
 184
 185 void (*omega_when_reduced) (omega_pb) = omega_no_procedure;
 186
 187 /* Compute the greatest common divisor of A and B.  */
 188
 189 static inline int
 190 gcd (int b, int a)
 191 {
 192   if (b == 1)
 193     return 1;
 194
 195   while (b != 0)
 196     {
 197       int t = b;
 198       b = a % b;
 199       a = t;
 200     }
 201
 202   return a;
 203 }
 204
 205 /* Print to FILE from PB equation E with all its coefficients
 206    multiplied by C.  */
 207
 208 static void
 209 omega_print_term (FILE *file, omega_pb pb, eqn e, int c)
 210 {
 211   int i;
 212   bool first = true;
 213   int n = pb->num_vars;
 214   int went_first = -1;
 215
 216   for (i = 1; i <= n; i++)
 217     if (c * e->coef[i] > 0)
 218       {
 219         first = false;
 220         went_first = i;
 221
 222         if (c * e->coef[i] == 1)
 223           fprintf (file, "%s", omega_variable_to_str (pb, i));
 224         else
 225           fprintf (file, "%d * %s", c * e->coef[i],
 226                    omega_variable_to_str (pb, i));
 227         break;
 228       }
 229
 230   for (i = 1; i <= n; i++)
 231     if (i != went_first && c * e->coef[i] != 0)
 232       {
 233         if (!first && c * e->coef[i] > 0)
 234           fprintf (file, " + ");
 235
 236         first = false;
 237
 238         if (c * e->coef[i] == 1)
 239           fprintf (file, "%s", omega_variable_to_str (pb, i));
 240         else if (c * e->coef[i] == -1)
 241           fprintf (file, " - %s", omega_variable_to_str (pb, i));
 242         else
 243           fprintf (file, "%d * %s", c * e->coef[i],
 244                    omega_variable_to_str (pb, i));
 245       }
 246
 247   if (!first && c * e->coef[0] > 0)
 248     fprintf (file, " + ");
 249
 250   if (first || c * e->coef[0] != 0)
 251     fprintf (file, "%d", c * e->coef[0]);
 252 }
 253
 254 /* Print to FILE the equation E of problem PB.  */
 255
 256 void
 257 omega_print_eqn (FILE *file, omega_pb pb, eqn e, bool test, int extra)
 258 {
 259   int i;
 260   int n = pb->num_vars + extra;
 261   bool is_lt = test && e->coef[0] == -1;
 262   bool first;
 263
 264   if (test)
 265     {
 266       if (e->touched)
 267         fprintf (file, "!");
 268
 269       else if (e->key != 0)
 270         fprintf (file, "%d: ", e->key);
 271     }
 272
 273   if (e->color == omega_red)
 274     fprintf (file, "[");
 275
 276   first = true;
 277
 278   for (i = is_lt ? 1 : 0; i <= n; i++)
 279     if (e->coef[i] < 0)
 280       {
 281         if (!first)
 282           fprintf (file, " + ");
 283         else
 284           first = false;
 285
 286         if (i == 0)
 287           fprintf (file, "%d", -e->coef[i]);
 288         else if (e->coef[i] == -1)
 289           fprintf (file, "%s", omega_variable_to_str (pb, i));
 290         else
 291           fprintf (file, "%d * %s", -e->coef[i],
 292                    omega_variable_to_str (pb, i));
 293       }
 294
 295   if (first)
 296     {
 297       if (is_lt)
 298         {
 299           fprintf (file, "1");
 300           is_lt = false;
 301         }
 302       else
 303         fprintf (file, "0");
 304     }
 305
 306   if (test == 0)
 307     fprintf (file, " = ");
 308   else if (is_lt)
 309     fprintf (file, " < ");
 310   else
 311     fprintf (file, " <= ");
 312
 313   first = true;
 314
 315   for (i = 0; i <= n; i++)
 316     if (e->coef[i] > 0)
 317       {
 318         if (!first)
 319           fprintf (file, " + ");
 320         else
 321           first = false;
 322
 323         if (i == 0)
 324           fprintf (file, "%d", e->coef[i]);
 325         else if (e->coef[i] == 1)
 326           fprintf (file, "%s", omega_variable_to_str (pb, i));
 327         else
 328           fprintf (file, "%d * %s", e->coef[i],
 329                    omega_variable_to_str (pb, i));
 330       }
 331
 332   if (first)
 333     fprintf (file, "0");
 334
 335   if (e->color == omega_red)
 336     fprintf (file, "]");
 337 }
 338
 339 /* Print to FILE all the variables of problem PB.  */
 340
 341 static void
 342 omega_print_vars (FILE *file, omega_pb pb)
 343 {
 344   int i;
 345
 346   fprintf (file, "variables = ");
 347
 348   if (pb->safe_vars > 0)
 349     fprintf (file, "protected (");
 350
 351   for (i = 1; i <= pb->num_vars; i++)
 352     {
 353       fprintf (file, "%s", omega_variable_to_str (pb, i));
 354
 355       if (i == pb->safe_vars)
 356         fprintf (file, ")");
 357
 358       if (i < pb->num_vars)
 359         fprintf (file, ", ");
 360     }
 361
 362   fprintf (file, "\n");
 363 }
 364
 365 /* Debug problem PB.  */
 366
 367 void
 368 debug_omega_problem (omega_pb pb)
 369 {
 370   omega_print_problem (stderr, pb);
 371 }
 372
 373 /* Print to FILE problem PB.  */
 374
 375 void
 376 omega_print_problem (FILE *file, omega_pb pb)
 377 {
 378   int e;
 379
 380   if (!pb->variables_initialized)
 381     omega_initialize_variables (pb);
 382
 383   omega_print_vars (file, pb);
 384
 385   for (e = 0; e < pb->num_eqs; e++)
 386     {
 387       omega_print_eq (file, pb, &pb->eqs[e]);
 388       fprintf (file, "\n");
 389     }
 390
 391   fprintf (file, "Done with EQ\n");
 392
 393   for (e = 0; e < pb->num_geqs; e++)
 394     {
 395       omega_print_geq (file, pb, &pb->geqs[e]);
 396       fprintf (file, "\n");
 397     }
 398
 399   fprintf (file, "Done with GEQ\n");
 400
 401   for (e = 0; e < pb->num_subs; e++)
 402     {
 403       eqn eq = &pb->subs[e];
 404
 405       if (eq->color == omega_red)
 406         fprintf (file, "[");
 407
 408       if (eq->key > 0)
 409         fprintf (file, "%s := ", omega_var_to_str (eq->key));
 410       else
 411         fprintf (file, "#%d := ", eq->key);
 412
 413       omega_print_term (file, pb, eq, 1);
 414
 415       if (eq->color == omega_red)
 416         fprintf (file, "]");
 417
 418       fprintf (file, "\n");
 419     }
 420 }
 421
 422 /* Return the number of equations in PB tagged omega_red.  */
 423
 424 int
 425 omega_count_red_equations (omega_pb pb)
 426 {
 427   int e, i;
 428   int result = 0;
 429
 430   for (e = 0; e < pb->num_eqs; e++)
 431     if (pb->eqs[e].color == omega_red)
 432       {
 433         for (i = pb->num_vars; i > 0; i--)
 434           if (pb->geqs[e].coef[i])
 435             break;
 436
 437         if (i == 0 && pb->geqs[e].coef[0] == 1)
 438           return 0;
 439         else
 440           result += 2;
 441       }
 442
 443   for (e = 0; e < pb->num_geqs; e++)
 444     if (pb->geqs[e].color == omega_red)
 445       result += 1;
 446
 447   for (e = 0; e < pb->num_subs; e++)
 448     if (pb->subs[e].color == omega_red)
 449       result += 2;
 450
 451   return result;
 452 }
 453
 454 /* Print to FILE all the equations in PB that are tagged omega_red.  */
 455
 456 void
 457 omega_print_red_equations (FILE *file, omega_pb pb)
 458 {
 459   int e;
 460
 461   if (!pb->variables_initialized)
 462     omega_initialize_variables (pb);
 463
 464   omega_print_vars (file, pb);
 465
 466   for (e = 0; e < pb->num_eqs; e++)
 467     if (pb->eqs[e].color == omega_red)
 468       {
 469         omega_print_eq (file, pb, &pb->eqs[e]);
 470         fprintf (file, "\n");
 471       }
 472
 473   for (e = 0; e < pb->num_geqs; e++)
 474     if (pb->geqs[e].color == omega_red)
 475       {
 476         omega_print_geq (file, pb, &pb->geqs[e]);
 477         fprintf (file, "\n");
 478       }
 479
 480   for (e = 0; e < pb->num_subs; e++)
 481     if (pb->subs[e].color == omega_red)
 482       {
 483         eqn eq = &pb->subs[e];
 484         fprintf (file, "[");
 485
 486         if (eq->key > 0)
 487           fprintf (file, "%s := ", omega_var_to_str (eq->key));
 488         else
 489           fprintf (file, "#%d := ", eq->key);
 490
 491         omega_print_term (file, pb, eq, 1);
 492         fprintf (file, "]\n");
 493       }
 494 }
 495
 496 /* Pretty print PB to FILE.  */
 497
 498 void
 499 omega_pretty_print_problem (FILE *file, omega_pb pb)
 500 {
 501   int e, v, v1, v2, v3, t;
 502   bool *live = XNEWVEC (bool, OMEGA_MAX_GEQS);
 503   int stuffPrinted = 0;
 504   bool change;
 505
 506   typedef enum {
 507     none, le, lt
 508   } partial_order_type;
 509
 510   partial_order_type **po = XNEWVEC (partial_order_type *,
 511                                      OMEGA_MAX_VARS * OMEGA_MAX_VARS);
 512   int **po_eq = XNEWVEC (int *, OMEGA_MAX_VARS * OMEGA_MAX_VARS);
 513   int *last_links = XNEWVEC (int, OMEGA_MAX_VARS);
 514   int *first_links = XNEWVEC (int, OMEGA_MAX_VARS);
 515   int *chain_length = XNEWVEC (int, OMEGA_MAX_VARS);
 516   int *chain = XNEWVEC (int, OMEGA_MAX_VARS);
 517   int i, m;
 518   bool multiprint;
 519
 520   if (!pb->variables_initialized)
 521     omega_initialize_variables (pb);
 522
 523   if (pb->num_vars > 0)
 524     {
 525       omega_eliminate_redundant (pb, false);
 526
 527       for (e = 0; e < pb->num_eqs; e++)
 528         {
 529           if (stuffPrinted)
 530             fprintf (file, "; ");
 531
 532           stuffPrinted = 1;
 533           omega_print_eq (file, pb, &pb->eqs[e]);
 534         }
 535
 536       for (e = 0; e < pb->num_geqs; e++)
 537         live[e] = true;
 538
 539       while (1)
 540         {
 541           for (v = 1; v <= pb->num_vars; v++)
 542             {
 543               last_links[v] = first_links[v] = 0;
 544               chain_length[v] = 0;
 545
 546               for (v2 = 1; v2 <= pb->num_vars; v2++)
 547                 po[v][v2] = none;
 548             }
 549
 550           for (e = 0; e < pb->num_geqs; e++)
 551             if (live[e])
 552               {
 553                 for (v = 1; v <= pb->num_vars; v++)
 554                   if (pb->geqs[e].coef[v] == 1)
 555                     first_links[v]++;
 556                   else if (pb->geqs[e].coef[v] == -1)
 557                     last_links[v]++;
 558
 559                 v1 = pb->num_vars;
 560
 561                 while (v1 > 0 && pb->geqs[e].coef[v1] == 0)
 562                   v1--;
 563
 564                 v2 = v1 - 1;
 565
 566                 while (v2 > 0 && pb->geqs[e].coef[v2] == 0)
 567                   v2--;
 568
 569                 v3 = v2 - 1;
 570
 571                 while (v3 > 0 && pb->geqs[e].coef[v3] == 0)
 572                   v3--;
 573
 574                 if (pb->geqs[e].coef[0] > 0 || pb->geqs[e].coef[0] < -1
 575                     || v2 <= 0 || v3 > 0
 576                     || pb->geqs[e].coef[v1] * pb->geqs[e].coef[v2] != -1)
 577                   {
 578                     /* Not a partial order relation.  */
 579                   }
 580                 else
 581                   {
 582                     if (pb->geqs[e].coef[v1] == 1)
 583                       {
 584                         v3 = v2;
 585                         v2 = v1;
 586                         v1 = v3;
 587                       }
 588
 589                     /* Relation is v1 <= v2 or v1 < v2.  */
 590                     po[v1][v2] = ((pb->geqs[e].coef[0] == 0) ? le : lt);
 591                     po_eq[v1][v2] = e;
 592                   }
 593               }
 594           for (v = 1; v <= pb->num_vars; v++)
 595             chain_length[v] = last_links[v];
 596
 597           /* Just in case pb->num_vars <= 0.  */
 598           change = false;
 599           for (t = 0; t < pb->num_vars; t++)
 600             {
 601               change = false;
 602
 603               for (v1 = 1; v1 <= pb->num_vars; v1++)
 604                 for (v2 = 1; v2 <= pb->num_vars; v2++)
 605                   if (po[v1][v2] != none &&
 606                       chain_length[v1] <= chain_length[v2])
 607                     {
 608                       chain_length[v1] = chain_length[v2] + 1;
 609                       change = true;
 610                     }
 611             }
 612
 613           /* Caught in cycle.  */
 614           gcc_assert (!change);
 615
 616           for (v1 = 1; v1 <= pb->num_vars; v1++)
 617             if (chain_length[v1] == 0)
 618               first_links[v1] = 0;
 619
 620           v = 1;
 621
 622           for (v1 = 2; v1 <= pb->num_vars; v1++)
 623             if (chain_length[v1] + first_links[v1] >
 624                 chain_length[v] + first_links[v])
 625               v = v1;
 626
 627           if (chain_length[v] + first_links[v] == 0)
 628             break;
 629
 630           if (stuffPrinted)
 631             fprintf (file, "; ");
 632
 633           stuffPrinted = 1;
 634
 635           /* Chain starts at v. */
 636           {
 637             int tmp;
 638             bool first = true;
 639
 640             for (e = 0; e < pb->num_geqs; e++)
 641               if (live[e] && pb->geqs[e].coef[v] == 1)
 642                 {
 643                   if (!first)
 644                     fprintf (file, ", ");
 645
 646                   tmp = pb->geqs[e].coef[v];
 647                   pb->geqs[e].coef[v] = 0;
 648                   omega_print_term (file, pb, &pb->geqs[e], -1);
 649                   pb->geqs[e].coef[v] = tmp;
 650                   live[e] = false;
 651                   first = false;
 652                 }
 653
 654             if (!first)
 655               fprintf (file, " <= ");
 656           }
 657
 658           /* Find chain.  */
 659           chain[0] = v;
 660           m = 1;
 661           while (1)
 662             {
 663               /* Print chain.  */
 664               for (v2 = 1; v2 <= pb->num_vars; v2++)
 665                 if (po[v][v2] && chain_length[v] == 1 + chain_length[v2])
 666                   break;
 667
 668               if (v2 > pb->num_vars)
 669                 break;
 670
 671               chain[m++] = v2;
 672               v = v2;
 673             }
 674
 675           fprintf (file, "%s", omega_variable_to_str (pb, chain[0]));
 676
 677           for (multiprint = false, i = 1; i < m; i++)
 678             {
 679               v = chain[i - 1];
 680               v2 = chain[i];
 681
 682               if (po[v][v2] == le)
 683                 fprintf (file, " <= ");
 684               else
 685                 fprintf (file, " < ");
 686
 687               fprintf (file, "%s", omega_variable_to_str (pb, v2));
 688               live[po_eq[v][v2]] = false;
 689
 690               if (!multiprint && i < m - 1)
 691                 for (v3 = 1; v3 <= pb->num_vars; v3++)
 692                   {
 693                     if (v == v3 || v2 == v3
 694                         || po[v][v2] != po[v][v3]
 695                         || po[v2][chain[i + 1]] != po[v3][chain[i + 1]])
 696                       continue;
 697
 698                     fprintf (file, ",%s", omega_variable_to_str (pb, v3));
 699                     live[po_eq[v][v3]] = false;
 700                     live[po_eq[v3][chain[i + 1]]] = false;
 701                     multiprint = true;
 702                   }
 703               else
 704                 multiprint = false;
 705             }
 706
 707           v = chain[m - 1];
 708           /* Print last_links.  */
 709           {
 710             int tmp;
 711             bool first = true;
 712
 713             for (e = 0; e < pb->num_geqs; e++)
 714               if (live[e] && pb->geqs[e].coef[v] == -1)
 715                 {
 716                   if (!first)
 717                     fprintf (file, ", ");
 718                   else
 719                     fprintf (file, " <= ");
 720
 721                   tmp = pb->geqs[e].coef[v];
 722                   pb->geqs[e].coef[v] = 0;
 723                   omega_print_term (file, pb, &pb->geqs[e], 1);
 724                   pb->geqs[e].coef[v] = tmp;
 725                   live[e] = false;
 726                   first = false;
 727                 }
 728           }
 729         }
 730
 731       for (e = 0; e < pb->num_geqs; e++)
 732         if (live[e])
 733           {
 734             if (stuffPrinted)
 735               fprintf (file, "; ");
 736             stuffPrinted = 1;
 737             omega_print_geq (file, pb, &pb->geqs[e]);
 738           }
 739
 740       for (e = 0; e < pb->num_subs; e++)
 741         {
 742           eqn eq = &pb->subs[e];
 743
 744           if (stuffPrinted)
 745             fprintf (file, "; ");
 746
 747           stuffPrinted = 1;
 748
 749           if (eq->key > 0)
 750             fprintf (file, "%s := ", omega_var_to_str (eq->key));
 751           else
 752             fprintf (file, "#%d := ", eq->key);
 753
 754           omega_print_term (file, pb, eq, 1);
 755         }
 756     }
 757
 758   free (live);
 759   free (po);
 760   free (po_eq);
 761   free (last_links);
 762   free (first_links);
 763   free (chain_length);
 764   free (chain);
 765 }
 766
 767 /* Assign to variable I in PB the next wildcard name.  The name of a
 768    wildcard is a negative number.  */
 769 static int next_wild_card = 0;
 770
 771 static void
 772 omega_name_wild_card (omega_pb pb, int i)
 773 {
 774   --next_wild_card;
 775   if (next_wild_card < -PARAM_VALUE (PARAM_OMEGA_MAX_WILD_CARDS))
 776     next_wild_card = -1;
 777   pb->var[i] = next_wild_card;
 778 }
 779
 780 /* Return the index of the last protected (or safe) variable in PB,
 781    after having added a new wildcard variable.  */
 782
 783 static int
 784 omega_add_new_wild_card (omega_pb pb)
 785 {
 786   int e;
 787   int i = ++pb->safe_vars;
 788   pb->num_vars++;
 789
 790   /* Make a free place in the protected (safe) variables, by moving
 791      the non protected variable pointed by "I" at the end, ie. at
 792      offset pb->num_vars.  */
 793   if (pb->num_vars != i)
 794     {
 795       /* Move "I" for all the inequalities.  */
 796       for (e = pb->num_geqs - 1; e >= 0; e--)
 797         {
 798           if (pb->geqs[e].coef[i])
 799             pb->geqs[e].touched = 1;
 800
 801           pb->geqs[e].coef[pb->num_vars] = pb->geqs[e].coef[i];
 802         }
 803
 804       /* Move "I" for all the equalities.  */
 805       for (e = pb->num_eqs - 1; e >= 0; e--)
 806         pb->eqs[e].coef[pb->num_vars] = pb->eqs[e].coef[i];
 807
 808       /* Move "I" for all the substitutions.  */
 809       for (e = pb->num_subs - 1; e >= 0; e--)
 810         pb->subs[e].coef[pb->num_vars] = pb->subs[e].coef[i];
 811
 812       /* Move the identifier.  */
 813       pb->var[pb->num_vars] = pb->var[i];
 814     }
 815
 816   /* Initialize at zero all the coefficients  */
 817   for (e = pb->num_geqs - 1; e >= 0; e--)
 818     pb->geqs[e].coef[i] = 0;
 819
 820   for (e = pb->num_eqs - 1; e >= 0; e--)
 821     pb->eqs[e].coef[i] = 0;
 822
 823   for (e = pb->num_subs - 1; e >= 0; e--)
 824     pb->subs[e].coef[i] = 0;
 825
 826   /* And give it a name.  */
 827   omega_name_wild_card (pb, i);
 828   return i;
 829 }
 830
 831 /* Delete inequality E from problem PB that has N_VARS variables.  */
 832
 833 static void
 834 omega_delete_geq (omega_pb pb, int e, int n_vars)
 835 {
 836   if (dump_file && (dump_flags & TDF_DETAILS))
 837     {
 838       fprintf (dump_file, "Deleting %d (last:%d): ", e, pb->num_geqs - 1);
 839       omega_print_geq (dump_file, pb, &pb->geqs[e]);
 840       fprintf (dump_file, "\n");
 841     }
 842
 843   if (e < pb->num_geqs - 1)
 844     omega_copy_eqn (&pb->geqs[e], &pb->geqs[pb->num_geqs - 1], n_vars);
 845
 846   pb->num_geqs--;
 847 }
 848
 849 /* Delete extra inequality E from problem PB that has N_VARS
 850    variables.  */
 851
 852 static void
 853 omega_delete_geq_extra (omega_pb pb, int e, int n_vars)
 854 {
 855   if (dump_file && (dump_flags & TDF_DETAILS))
 856     {
 857       fprintf (dump_file, "Deleting %d: ",e);
 858       omega_print_geq_extra (dump_file, pb, &pb->geqs[e]);
 859       fprintf (dump_file, "\n");
 860     }
 861
 862   if (e < pb->num_geqs - 1)
 863     omega_copy_eqn (&pb->geqs[e], &pb->geqs[pb->num_geqs - 1], n_vars);
 864
 865   pb->num_geqs--;
 866 }
 867
 868
 869 /* Remove variable I from problem PB.  */
 870
 871 static void
 872 omega_delete_variable (omega_pb pb, int i)
 873 {
 874   int n_vars = pb->num_vars;
 875   int e;
 876
 877   if (omega_safe_var_p (pb, i))
 878     {
 879       int j = pb->safe_vars;
 880
 881       for (e = pb->num_geqs - 1; e >= 0; e--)
 882         {
 883           pb->geqs[e].touched = 1;
 884           pb->geqs[e].coef[i] = pb->geqs[e].coef[j];
 885           pb->geqs[e].coef[j] = pb->geqs[e].coef[n_vars];
 886         }
 887
 888       for (e = pb->num_eqs - 1; e >= 0; e--)
 889         {
 890           pb->eqs[e].coef[i] = pb->eqs[e].coef[j];
 891           pb->eqs[e].coef[j] = pb->eqs[e].coef[n_vars];
 892         }
 893
 894       for (e = pb->num_subs - 1; e >= 0; e--)
 895         {
 896           pb->subs[e].coef[i] = pb->subs[e].coef[j];
 897           pb->subs[e].coef[j] = pb->subs[e].coef[n_vars];
 898         }
 899
 900       pb->var[i] = pb->var[j];
 901       pb->var[j] = pb->var[n_vars];
 902     }
 903   else if (i < n_vars)
 904     {
 905       for (e = pb->num_geqs - 1; e >= 0; e--)
 906         if (pb->geqs[e].coef[n_vars])
 907           {
 908             pb->geqs[e].coef[i] = pb->geqs[e].coef[n_vars];
 909             pb->geqs[e].touched = 1;
 910           }
 911
 912       for (e = pb->num_eqs - 1; e >= 0; e--)
 913         pb->eqs[e].coef[i] = pb->eqs[e].coef[n_vars];
 914
 915       for (e = pb->num_subs - 1; e >= 0; e--)
 916         pb->subs[e].coef[i] = pb->subs[e].coef[n_vars];
 917
 918       pb->var[i] = pb->var[n_vars];
 919     }
 920
 921   if (omega_safe_var_p (pb, i))
 922     pb->safe_vars--;
 923
 924   pb->num_vars--;
 925 }
 926
 927 /* Because the coefficients of an equation are sparse, PACKING records
 928    indices for non null coefficients.  */
 929 static int *packing;
 930
 931 /* Set up the coefficients of PACKING, following the coefficients of
 932    equation EQN that has NUM_VARS variables.  */
 933
 934 static inline int
 935 setup_packing (eqn eqn, int num_vars)
 936 {
 937   int k;
 938   int n = 0;
 939
 940   for (k = num_vars; k >= 0; k--)
 941     if (eqn->coef[k])
 942       packing[n++] = k;
 943
 944   return n;
 945 }
 946
 947 /* Computes a linear combination of EQ and SUB at VAR with coefficient
 948    C, such that EQ->coef[VAR] is set to 0.  TOP_VAR is the number of
 949    non null indices of SUB stored in PACKING.  */
 950
 951 static inline void
 952 omega_substitute_red_1 (eqn eq, eqn sub, int var, int c, bool *found_black,
 953                         int top_var)
 954 {
 955   if (eq->coef[var] != 0)
 956     {
 957       if (eq->color == omega_black)
 958         *found_black = true;
 959       else
 960         {
 961           int j, k = eq->coef[var];
 962
 963           eq->coef[var] = 0;
 964
 965           for (j = top_var; j >= 0; j--)
 966             eq->coef[packing[j]] -= sub->coef[packing[j]] * k * c;
 967         }
 968     }
 969 }
 970
 971 /* Substitute in PB variable VAR with "C * SUB".  */
 972
 973 static void
 974 omega_substitute_red (omega_pb pb, eqn sub, int var, int c, bool *found_black)
 975 {
 976   int e, top_var = setup_packing (sub, pb->num_vars);
 977
 978   *found_black = false;
 979
 980   if (dump_file && (dump_flags & TDF_DETAILS))
 981     {
 982       if (sub->color == omega_red)
 983         fprintf (dump_file, "[");
 984
 985       fprintf (dump_file, "substituting using %s := ",
 986                omega_variable_to_str (pb, var));
 987       omega_print_term (dump_file, pb, sub, -c);
 988
 989       if (sub->color == omega_red)
 990         fprintf (dump_file, "]");
 991
 992       fprintf (dump_file, "\n");
 993       omega_print_vars (dump_file, pb);
 994     }
 995
 996   for (e = pb->num_eqs - 1; e >= 0; e--)
 997     {
 998       eqn eqn = &(pb->eqs[e]);
 999
1000       omega_substitute_red_1 (eqn, sub, var, c, found_black, top_var);
1001
1002       if (dump_file && (dump_flags & TDF_DETAILS))
1003         {
1004           omega_print_eq (dump_file, pb, eqn);
1005           fprintf (dump_file, "\n");
1006         }
1007     }
1008
1009   for (e = pb->num_geqs - 1; e >= 0; e--)
1010     {
1011       eqn eqn = &(pb->geqs[e]);
1012
1013       omega_substitute_red_1 (eqn, sub, var, c, found_black, top_var);
1014
1015       if (eqn->coef[var] && eqn->color == omega_red)
1016         eqn->touched = 1;
1017
1018       if (dump_file && (dump_flags & TDF_DETAILS))
1019         {
1020           omega_print_geq (dump_file, pb, eqn);
1021           fprintf (dump_file, "\n");
1022         }
1023     }
1024
1025   for (e = pb->num_subs - 1; e >= 0; e--)
1026     {
1027       eqn eqn = &(pb->subs[e]);
1028
1029       omega_substitute_red_1 (eqn, sub, var, c, found_black, top_var);
1030
1031       if (dump_file && (dump_flags & TDF_DETAILS))
1032         {
1033           fprintf (dump_file, "%s := ", omega_var_to_str (eqn->key));
1034           omega_print_term (dump_file, pb, eqn, 1);
1035           fprintf (dump_file, "\n");
1036         }
1037     }
1038
1039   if (dump_file && (dump_flags & TDF_DETAILS))
1040     fprintf (dump_file, "---\n\n");
1041
1042   if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
1043     *found_black = true;
1044 }
1045
1046 /* Substitute in PB variable VAR with "C * SUB".  */
1047
1048 static void
1049 omega_substitute (omega_pb pb, eqn sub, int var, int c)
1050 {
1051   int e, j, j0;
1052   int top_var = setup_packing (sub, pb->num_vars);
1053
1054   if (dump_file && (dump_flags & TDF_DETAILS))
1055     {
1056       fprintf (dump_file, "substituting using %s := ",
1057                omega_variable_to_str (pb, var));
1058       omega_print_term (dump_file, pb, sub, -c);
1059       fprintf (dump_file, "\n");
1060       omega_print_vars (dump_file, pb);
1061     }
1062
1063   if (top_var < 0)
1064     {
1065       for (e = pb->num_eqs - 1; e >= 0; e--)
1066         pb->eqs[e].coef[var] = 0;
1067
1068       for (e = pb->num_geqs - 1; e >= 0; e--)
1069         if (pb->geqs[e].coef[var] != 0)
1070           {
1071             pb->geqs[e].touched = 1;
1072             pb->geqs[e].coef[var] = 0;
1073           }
1074
1075       for (e = pb->num_subs - 1; e >= 0; e--)
1076         pb->subs[e].coef[var] = 0;
1077
1078       if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
1079         {
1080           int k;
1081           eqn eqn = &(pb->subs[pb->num_subs++]);
1082
1083           for (k = pb->num_vars; k >= 0; k--)
1084             eqn->coef[k] = 0;
1085
1086           eqn->key = pb->var[var];
1087           eqn->color = omega_black;
1088         }
1089     }
1090   else if (top_var == 0 && packing[0] == 0)
1091     {
1092       c = -sub->coef[0] * c;
1093
1094       for (e = pb->num_eqs - 1; e >= 0; e--)
1095         {
1096           pb->eqs[e].coef[0] += pb->eqs[e].coef[var] * c;
1097           pb->eqs[e].coef[var] = 0;
1098         }
1099
1100       for (e = pb->num_geqs - 1; e >= 0; e--)
1101         if (pb->geqs[e].coef[var] != 0)
1102           {
1103             pb->geqs[e].coef[0] += pb->geqs[e].coef[var] * c;
1104             pb->geqs[e].coef[var] = 0;
1105             pb->geqs[e].touched = 1;
1106           }
1107
1108       for (e = pb->num_subs - 1; e >= 0; e--)
1109         {
1110           pb->subs[e].coef[0] += pb->subs[e].coef[var] * c;
1111           pb->subs[e].coef[var] = 0;
1112         }
1113
1114       if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
1115         {
1116           int k;
1117           eqn eqn = &(pb->subs[pb->num_subs++]);
1118
1119           for (k = pb->num_vars; k >= 1; k--)
1120             eqn->coef[k] = 0;
1121
1122           eqn->coef[0] = c;
1123           eqn->key = pb->var[var];
1124           eqn->color = omega_black;
1125         }
1126
1127       if (dump_file && (dump_flags & TDF_DETAILS))
1128         {
1129           fprintf (dump_file, "---\n\n");
1130           omega_print_problem (dump_file, pb);
1131           fprintf (dump_file, "===\n\n");
1132         }
1133     }
1134   else
1135     {
1136       for (e = pb->num_eqs - 1; e >= 0; e--)
1137         {
1138           eqn eqn = &(pb->eqs[e]);
1139           int k = eqn->coef[var];
1140
1141           if (k != 0)
1142             {
1143               k = c * k;
1144               eqn->coef[var] = 0;
1145
1146               for (j = top_var; j >= 0; j--)
1147                 {
1148                   j0 = packing[j];
1149                   eqn->coef[j0] -= sub->coef[j0] * k;
1150                 }
1151             }
1152
1153           if (dump_file && (dump_flags & TDF_DETAILS))
1154             {
1155               omega_print_eq (dump_file, pb, eqn);
1156               fprintf (dump_file, "\n");
1157             }
1158         }
1159
1160       for (e = pb->num_geqs - 1; e >= 0; e--)
1161         {
1162           eqn eqn = &(pb->geqs[e]);
1163           int k = eqn->coef[var];
1164
1165           if (k != 0)
1166             {
1167               k = c * k;
1168               eqn->touched = 1;
1169               eqn->coef[var] = 0;
1170
1171               for (j = top_var; j >= 0; j--)
1172                 {
1173                   j0 = packing[j];
1174                   eqn->coef[j0] -= sub->coef[j0] * k;
1175                 }
1176             }
1177
1178           if (dump_file && (dump_flags & TDF_DETAILS))
1179             {
1180               omega_print_geq (dump_file, pb, eqn);
1181               fprintf (dump_file, "\n");
1182             }
1183         }
1184
1185       for (e = pb->num_subs - 1; e >= 0; e--)
1186         {
1187           eqn eqn = &(pb->subs[e]);
1188           int k = eqn->coef[var];
1189
1190           if (k != 0)
1191             {
1192               k = c * k;
1193               eqn->coef[var] = 0;
1194
1195               for (j = top_var; j >= 0; j--)
1196                 {
1197                   j0 = packing[j];
1198                   eqn->coef[j0] -= sub->coef[j0] * k;
1199                 }
1200             }
1201
1202           if (dump_file && (dump_flags & TDF_DETAILS))
1203             {
1204               fprintf (dump_file, "%s := ", omega_var_to_str (eqn->key));
1205               omega_print_term (dump_file, pb, eqn, 1);
1206               fprintf (dump_file, "\n");
1207             }
1208         }
1209
1210       if (dump_file && (dump_flags & TDF_DETAILS))
1211         {
1212           fprintf (dump_file, "---\n\n");
1213           omega_print_problem (dump_file, pb);
1214           fprintf (dump_file, "===\n\n");
1215         }
1216
1217       if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
1218         {
1219           int k;
1220           eqn eqn = &(pb->subs[pb->num_subs++]);
1221           c = -c;
1222
1223           for (k = pb->num_vars; k >= 0; k--)
1224             eqn->coef[k] = c * (sub->coef[k]);
1225
1226           eqn->key = pb->var[var];
1227           eqn->color = sub->color;
1228         }
1229     }
1230 }
1231
1232 /* Solve e = factor alpha for x_j and substitute.  */
1233
1234 static void
1235 omega_do_mod (omega_pb pb, int factor, int e, int j)
1236 {
1237   int k, i;
1238   eqn eq = omega_alloc_eqns (0, 1);
1239   int nfactor;
1240   bool kill_j = false;
1241
1242   omega_copy_eqn (eq, &pb->eqs[e], pb->num_vars);
1243
1244   for (k = pb->num_vars; k >= 0; k--)
1245     {
1246       eq->coef[k] = int_mod (eq->coef[k], factor);
1247
1248       if (2 * eq->coef[k] >= factor)
1249         eq->coef[k] -= factor;
1250     }
1251
1252   nfactor = eq->coef[j];
1253
1254   if (omega_safe_var_p (pb, j) && !omega_wildcard_p (pb, j))
1255     {
1256       i = omega_add_new_wild_card (pb);
1257       eq->coef[pb->num_vars] = eq->coef[i];
1258       eq->coef[j] = 0;
1259       eq->coef[i] = -factor;
1260       kill_j = true;
1261     }
1262   else
1263     {
1264       eq->coef[j] = -factor;
1265       if (!omega_wildcard_p (pb, j))
1266         omega_name_wild_card (pb, j);
1267     }
1268
1269   omega_substitute (pb, eq, j, nfactor);
1270
1271   for (k = pb->num_vars; k >= 0; k--)
1272     pb->eqs[e].coef[k] = pb->eqs[e].coef[k] / factor;
1273
1274   if (kill_j)
1275     omega_delete_variable (pb, j);
1276
1277   if (dump_file && (dump_flags & TDF_DETAILS))
1278     {
1279       fprintf (dump_file, "Mod-ing and normalizing produces:\n");
1280       omega_print_problem (dump_file, pb);
1281     }
1282
1283   omega_free_eqns (eq, 1);
1284 }
1285
1286 /* Multiplies by -1 inequality E.  */
1287
1288 void
1289 omega_negate_geq (omega_pb pb, int e)
1290 {
1291   int i;
1292
1293   for (i = pb->num_vars; i >= 0; i--)
1294     pb->geqs[e].coef[i] *= -1;
1295
1296   pb->geqs[e].coef[0]--;
1297   pb->geqs[e].touched = 1;
1298 }
1299
1300 /* Returns OMEGA_TRUE when problem PB has a solution.  */
1301
1302 static enum omega_result
1303 verify_omega_pb (omega_pb pb)
1304 {
1305   enum omega_result result;
1306   int e;
1307   bool any_color = false;
1308   omega_pb tmp_problem = XNEW (struct omega_pb);
1309
1310   omega_copy_problem (tmp_problem, pb);
1311   tmp_problem->safe_vars = 0;
1312   tmp_problem->num_subs = 0;
1313
1314   for (e = pb->num_geqs - 1; e >= 0; e--)
1315     if (pb->geqs[e].color == omega_red)
1316       {
1317         any_color = true;
1318         break;
1319       }
1320
1321   if (please_no_equalities_in_simplified_problems)
1322     any_color = true;
1323
1324   if (any_color)
1325     original_problem = no_problem;
1326   else
1327     original_problem = pb;
1328
1329   if (dump_file && (dump_flags & TDF_DETAILS))
1330     {
1331       fprintf (dump_file, "verifying problem");
1332
1333       if (any_color)
1334         fprintf (dump_file, " (color mode)");
1335
1336       fprintf (dump_file, " :\n");
1337       omega_print_problem (dump_file, pb);
1338     }
1339
1340   result = omega_solve_problem (tmp_problem, omega_unknown);
1341   original_problem = no_problem;
1342   free (tmp_problem);
1343
1344   if (dump_file && (dump_flags & TDF_DETAILS))
1345     {
1346       if (result != omega_false)
1347         fprintf (dump_file, "verified problem\n");
1348       else
1349         fprintf (dump_file, "disproved problem\n");
1350       omega_print_problem (dump_file, pb);
1351     }
1352
1353   return result;
1354 }
1355
1356 /* Add a new equality to problem PB at last position E.  */
1357
1358 static void
1359 adding_equality_constraint (omega_pb pb, int e)
1360 {
1361   if (original_problem != no_problem
1362       && original_problem != pb
1363       && !conservative)
1364     {
1365       int i, j;
1366       int e2 = original_problem->num_eqs++;
1367
1368       if (dump_file && (dump_flags & TDF_DETAILS))
1369         fprintf (dump_file,
1370                  "adding equality constraint %d to outer problem\n", e2);
1371       omega_init_eqn_zero (&original_problem->eqs[e2],
1372                            original_problem->num_vars);
1373
1374       for (i = pb->num_vars; i >= 1; i--)
1375         {
1376           for (j = original_problem->num_vars; j >= 1; j--)
1377             if (original_problem->var[j] == pb->var[i])
1378               break;
1379
1380           if (j <= 0)
1381             {
1382               if (dump_file && (dump_flags & TDF_DETAILS))
1383                 fprintf (dump_file, "retracting\n");
1384               original_problem->num_eqs--;
1385               return;
1386             }
1387           original_problem->eqs[e2].coef[j] = pb->eqs[e].coef[i];
1388         }
1389
1390       original_problem->eqs[e2].coef[0] = pb->eqs[e].coef[0];
1391
1392       if (dump_file && (dump_flags & TDF_DETAILS))
1393         omega_print_problem (dump_file, original_problem);
1394     }
1395 }
1396
1397 static int *fast_lookup;
1398 static int *fast_lookup_red;
1399
1400 typedef enum {
1401   normalize_false,
1402   normalize_uncoupled,
1403   normalize_coupled
1404 } normalize_return_type;
1405
1406 /* Normalizes PB by removing redundant constraints.  Returns
1407    normalize_false when the constraints system has no solution,
1408    otherwise returns normalize_coupled or normalize_uncoupled.  */
1409
1410 static normalize_return_type
1411 normalize_omega_problem (omega_pb pb)
1412 {
1413   int e, i, j, k, n_vars;
1414   int coupled_subscripts = 0;
1415
1416   n_vars = pb->num_vars;
1417
1418   for (e = 0; e < pb->num_geqs; e++)
1419     {
1420       if (!pb->geqs[e].touched)
1421         {
1422           if (!single_var_geq (&pb->geqs[e], n_vars))
1423             coupled_subscripts = 1;
1424         }
1425       else
1426         {
1427           int g, top_var, i0, hashCode;
1428           int *p = &packing[0];
1429
1430           for (k = 1; k <= n_vars; k++)
1431             if (pb->geqs[e].coef[k])
1432               *(p++) = k;
1433
1434           top_var = (p - &packing[0]) - 1;
1435
1436           if (top_var == -1)
1437             {
1438               if (pb->geqs[e].coef[0] < 0)
1439                 {
1440                   if (dump_file && (dump_flags & TDF_DETAILS))
1441                     {
1442                       omega_print_geq (dump_file, pb, &pb->geqs[e]);
1443                       fprintf (dump_file, "\nequations have no solution \n");
1444                     }
1445                   return normalize_false;
1446                 }
1447
1448               omega_delete_geq (pb, e, n_vars);
1449               e--;
1450               continue;
1451             }
1452           else if (top_var == 0)
1453             {
1454               int singlevar = packing[0];
1455
1456               g = pb->geqs[e].coef[singlevar];
1457
1458               if (g > 0)
1459                 {
1460                   pb->geqs[e].coef[singlevar] = 1;
1461                   pb->geqs[e].key = singlevar;
1462                 }
1463               else
1464                 {
1465                   g = -g;
1466                   pb->geqs[e].coef[singlevar] = -1;
1467                   pb->geqs[e].key = -singlevar;
1468                 }
1469
1470               if (g > 1)
1471                 pb->geqs[e].coef[0] = int_div (pb->geqs[e].coef[0], g);
1472             }
1473           else
1474             {
1475               int g2;
1476               int hash_key_multiplier = 31;
1477
1478               coupled_subscripts = 1;
1479               i0 = top_var;
1480               i = packing[i0--];
1481               g = pb->geqs[e].coef[i];
1482               hashCode = g * (i + 3);
1483
1484               if (g < 0)
1485                 g = -g;
1486
1487               for (; i0 >= 0; i0--)
1488                 {
1489                   int x;
1490
1491                   i = packing[i0];
1492                   x = pb->geqs[e].coef[i];
1493                   hashCode = hashCode * hash_key_multiplier * (i + 3) + x;
1494
1495                   if (x < 0)
1496                     x = -x;
1497
1498                   if (x == 1)
1499                     {
1500                       g = 1;
1501                       i0--;
1502                       break;
1503                     }
1504                   else
1505                     g = gcd (x, g);
1506                 }
1507
1508               for (; i0 >= 0; i0--)
1509                 {
1510                   int x;
1511                   i = packing[i0];
1512                   x = pb->geqs[e].coef[i];
1513                   hashCode = hashCode * hash_key_multiplier * (i + 3) + x;
1514                 }
1515
1516               if (g > 1)
1517                 {
1518                   pb->geqs[e].coef[0] = int_div (pb->geqs[e].coef[0], g);
1519                   i0 = top_var;
1520                   i = packing[i0--];
1521                   pb->geqs[e].coef[i] = pb->geqs[e].coef[i] / g;
1522                   hashCode = pb->geqs[e].coef[i] * (i + 3);
1523
1524                   for (; i0 >= 0; i0--)
1525                     {
1526                       i = packing[i0];
1527                       pb->geqs[e].coef[i] = pb->geqs[e].coef[i] / g;
1528                       hashCode = hashCode * hash_key_multiplier * (i + 3)
1529                         + pb->geqs[e].coef[i];
1530                     }
1531                 }
1532
1533               g2 = abs (hashCode);
1534
1535               if (dump_file && (dump_flags & TDF_DETAILS))
1536                 {
1537                   fprintf (dump_file, "Hash code = %d, eqn = ", hashCode);
1538                   omega_print_geq (dump_file, pb, &pb->geqs[e]);
1539                   fprintf (dump_file, "\n");
1540                 }
1541
1542               j = g2 % HASH_TABLE_SIZE;
1543
1544               do {
1545                 eqn proto = &(hash_master[j]);
1546
1547                 if (proto->touched == g2)
1548                   {
1549                     if (proto->coef[0] == top_var)
1550                       {
1551                         if (hashCode >= 0)
1552                           for (i0 = top_var; i0 >= 0; i0--)
1553                             {
1554                               i = packing[i0];
1555
1556                               if (pb->geqs[e].coef[i] != proto->coef[i])
1557                                 break;
1558                             }
1559                         else
1560                           for (i0 = top_var; i0 >= 0; i0--)
1561                             {
1562                               i = packing[i0];
1563
1564                               if (pb->geqs[e].coef[i] != -proto->coef[i])
1565                                 break;
1566                             }
1567
1568                         if (i0 < 0)
1569                           {
1570                             if (hashCode >= 0)
1571                               pb->geqs[e].key = proto->key;
1572                             else
1573                               pb->geqs[e].key = -proto->key;
1574                             break;
1575                           }
1576                       }
1577                   }
1578                 else if (proto->touched < 0)
1579                   {
1580                     omega_init_eqn_zero (proto, pb->num_vars);
1581                     if (hashCode >= 0)
1582                       for (i0 = top_var; i0 >= 0; i0--)
1583                         {
1584                           i = packing[i0];
1585                           proto->coef[i] = pb->geqs[e].coef[i];
1586                         }
1587                     else
1588                       for (i0 = top_var; i0 >= 0; i0--)
1589                         {
1590                           i = packing[i0];
1591                           proto->coef[i] = -pb->geqs[e].coef[i];
1592                         }
1593
1594                     proto->coef[0] = top_var;
1595                     proto->touched = g2;
1596
1597                     if (dump_file && (dump_flags & TDF_DETAILS))
1598                       fprintf (dump_file, " constraint key = %d\n",
1599                                next_key);
1600
1601                     proto->key = next_key++;
1602
1603                     /* Too many hash keys generated.  */
1604                     gcc_assert (proto->key <= MAX_KEYS);
1605
1606                     if (hashCode >= 0)
1607                       pb->geqs[e].key = proto->key;
1608                     else
1609                       pb->geqs[e].key = -proto->key;
1610
1611                     break;
1612                   }
1613
1614                 j = (j + 1) % HASH_TABLE_SIZE;
1615               } while (1);
1616             }
1617
1618           pb->geqs[e].touched = 0;
1619         }
1620
1621       {
1622         int eKey = pb->geqs[e].key;
1623         int e2;
1624         if (e > 0)
1625           {
1626             int cTerm = pb->geqs[e].coef[0];
1627             e2 = fast_lookup[MAX_KEYS - eKey];
1628
1629             if (e2 < e && pb->geqs[e2].key == -eKey
1630                 && pb->geqs[e2].color == omega_black)
1631               {
1632                 if (pb->geqs[e2].coef[0] < -cTerm)
1633                   {
1634                     if (dump_file && (dump_flags & TDF_DETAILS))
1635                       {
1636                         omega_print_geq (dump_file, pb, &pb->geqs[e]);
1637                         fprintf (dump_file, "\n");
1638                         omega_print_geq (dump_file, pb, &pb->geqs[e2]);
1639                         fprintf (dump_file,
1640                                  "\nequations have no solution \n");
1641                       }
1642                     return normalize_false;
1643                   }
1644
1645                 if (pb->geqs[e2].coef[0] == -cTerm
1646                     && (create_color
1647                         || pb->geqs[e].color == omega_black))
1648                   {
1649                     omega_copy_eqn (&pb->eqs[pb->num_eqs], &pb->geqs[e],
1650                                     pb->num_vars);
1651                     if (pb->geqs[e].color == omega_black)
1652                       adding_equality_constraint (pb, pb->num_eqs);
1653                     pb->num_eqs++;
1654                     gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
1655                   }
1656               }
1657
1658             e2 = fast_lookup_red[MAX_KEYS - eKey];
1659
1660             if (e2 < e && pb->geqs[e2].key == -eKey
1661                 && pb->geqs[e2].color == omega_red)
1662               {
1663                 if (pb->geqs[e2].coef[0] < -cTerm)
1664                   {
1665                     if (dump_file && (dump_flags & TDF_DETAILS))
1666                       {
1667                         omega_print_geq (dump_file, pb, &pb->geqs[e]);
1668                         fprintf (dump_file, "\n");
1669                         omega_print_geq (dump_file, pb, &pb->geqs[e2]);
1670                         fprintf (dump_file,
1671                                  "\nequations have no solution \n");
1672                       }
1673                     return normalize_false;
1674                   }
1675
1676                 if (pb->geqs[e2].coef[0] == -cTerm && create_color)
1677                   {
1678                     omega_copy_eqn (&pb->eqs[pb->num_eqs], &pb->geqs[e],
1679                                     pb->num_vars);
1680                     pb->eqs[pb->num_eqs].color = omega_red;
1681                     pb->num_eqs++;
1682                     gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
1683                   }
1684               }
1685
1686             e2 = fast_lookup[MAX_KEYS + eKey];
1687
1688             if (e2 < e && pb->geqs[e2].key == eKey
1689                 && pb->geqs[e2].color == omega_black)
1690               {
1691                 if (pb->geqs[e2].coef[0] > cTerm)
1692                   {
1693                     if (pb->geqs[e].color == omega_black)
1694                       {
1695                         if (dump_file && (dump_flags & TDF_DETAILS))
1696                           {
1697                             fprintf (dump_file,
1698                                      "Removing Redundant Equation: ");
1699                             omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
1700                             fprintf (dump_file, "\n");
1701                             fprintf (dump_file,
1702                                      "[a]      Made Redundant by: ");
1703                             omega_print_geq (dump_file, pb, &(pb->geqs[e]));
1704                             fprintf (dump_file, "\n");
1705                           }
1706                         pb->geqs[e2].coef[0] = cTerm;
1707                         omega_delete_geq (pb, e, n_vars);
1708                         e--;
1709                         continue;
1710                       }
1711                   }
1712                 else
1713                   {
1714                     if (dump_file && (dump_flags & TDF_DETAILS))
1715                       {
1716                         fprintf (dump_file, "Removing Redundant Equation: ");
1717                         omega_print_geq (dump_file, pb, &(pb->geqs[e]));
1718                         fprintf (dump_file, "\n");
1719                         fprintf (dump_file, "[b]      Made Redundant by: ");
1720                         omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
1721                         fprintf (dump_file, "\n");
1722                       }
1723                     omega_delete_geq (pb, e, n_vars);
1724                     e--;
1725                     continue;
1726                   }
1727               }
1728
1729             e2 = fast_lookup_red[MAX_KEYS + eKey];
1730
1731             if (e2 < e && pb->geqs[e2].key == eKey
1732                 && pb->geqs[e2].color == omega_red)
1733               {
1734                 if (pb->geqs[e2].coef[0] >= cTerm)
1735                   {
1736                     if (dump_file && (dump_flags & TDF_DETAILS))
1737                       {
1738                         fprintf (dump_file, "Removing Redundant Equation: ");
1739                         omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
1740                         fprintf (dump_file, "\n");
1741                         fprintf (dump_file, "[c]      Made Redundant by: ");
1742                         omega_print_geq (dump_file, pb, &(pb->geqs[e]));
1743                         fprintf (dump_file, "\n");
1744                       }
1745                     pb->geqs[e2].coef[0] = cTerm;
1746                     pb->geqs[e2].color = pb->geqs[e].color;
1747                   }
1748                 else if (pb->geqs[e].color == omega_red)
1749                   {
1750                     if (dump_file && (dump_flags & TDF_DETAILS))
1751                       {
1752                         fprintf (dump_file, "Removing Redundant Equation: ");
1753                         omega_print_geq (dump_file, pb, &(pb->geqs[e]));
1754                         fprintf (dump_file, "\n");
1755                         fprintf (dump_file, "[d]      Made Redundant by: ");
1756                         omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
1757                         fprintf (dump_file, "\n");
1758                       }
1759                   }
1760                 omega_delete_geq (pb, e, n_vars);
1761                 e--;
1762                 continue;
1763
1764               }
1765           }
1766
1767         if (pb->geqs[e].color == omega_red)
1768           fast_lookup_red[MAX_KEYS + eKey] = e;
1769         else
1770           fast_lookup[MAX_KEYS + eKey] = e;
1771       }
1772     }
1773
1774   create_color = false;
1775   return coupled_subscripts ? normalize_coupled : normalize_uncoupled;
1776 }
1777
1778 /* Divide the coefficients of EQN by their gcd.  N_VARS is the number
1779    of variables in EQN.  */
1780
1781 static inline void
1782 divide_eqn_by_gcd (eqn eqn, int n_vars)
1783 {
1784   int var, g = 0;
1785
1786   for (var = n_vars; var >= 0; var--)
1787     g = gcd (abs (eqn->coef[var]), g);
1788
1789   if (g)
1790     for (var = n_vars; var >= 0; var--)
1791       eqn->coef[var] = eqn->coef[var] / g;
1792 }
1793
1794 /* Rewrite some non-safe variables in function of protected
1795    wildcard variables.  */
1796
1797 static void
1798 cleanout_wildcards (omega_pb pb)
1799 {
1800   int e, i, j;
1801   int n_vars = pb->num_vars;
1802   bool renormalize = false;
1803
1804   for (e = pb->num_eqs - 1; e >= 0; e--)
1805     for (i = n_vars; !omega_safe_var_p (pb, i); i--)
1806       if (pb->eqs[e].coef[i] != 0)
1807         {
1808           /* i is the last nonzero non-safe variable.  */
1809
1810           for (j = i - 1; !omega_safe_var_p (pb, j); j--)
1811             if (pb->eqs[e].coef[j] != 0)
1812               break;
1813
1814           /* j is the next nonzero non-safe variable, or points
1815              to a safe variable: it is then a wildcard variable.  */
1816
1817           /* Clean it out.  */
1818           if (omega_safe_var_p (pb, j))
1819             {
1820               eqn sub = &(pb->eqs[e]);
1821               int c = pb->eqs[e].coef[i];
1822               int a = abs (c);
1823               int e2;
1824
1825               if (dump_file && (dump_flags & TDF_DETAILS))
1826                 {
1827                   fprintf (dump_file,
1828                            "Found a single wild card equality: ");
1829                   omega_print_eq (dump_file, pb, &pb->eqs[e]);
1830                   fprintf (dump_file, "\n");
1831                   omega_print_problem (dump_file, pb);
1832                 }
1833
1834               for (e2 = pb->num_eqs - 1; e2 >= 0; e2--)
1835                 if (e != e2 && pb->eqs[e2].coef[i]
1836                     && (pb->eqs[e2].color == omega_red
1837                         || (pb->eqs[e2].color == omega_black
1838                             && pb->eqs[e].color == omega_black)))
1839                   {
1840                     eqn eqn = &(pb->eqs[e2]);
1841                     int var, k;
1842
1843                     for (var = n_vars; var >= 0; var--)
1844                       eqn->coef[var] *= a;
1845
1846                     k = eqn->coef[i];
1847
1848                     for (var = n_vars; var >= 0; var--)
1849                       eqn->coef[var] -= sub->coef[var] * k / c;
1850
1851                     eqn->coef[i] = 0;
1852                     divide_eqn_by_gcd (eqn, n_vars);
1853                   }
1854
1855               for (e2 = pb->num_geqs - 1; e2 >= 0; e2--)
1856                 if (pb->geqs[e2].coef[i]
1857                     && (pb->geqs[e2].color == omega_red
1858                         || (pb->eqs[e].color == omega_black
1859                             && pb->geqs[e2].color == omega_black)))
1860                   {
1861                     eqn eqn = &(pb->geqs[e2]);
1862                     int var, k;
1863
1864                     for (var = n_vars; var >= 0; var--)
1865                       eqn->coef[var] *= a;
1866
1867                     k = eqn->coef[i];
1868
1869                     for (var = n_vars; var >= 0; var--)
1870                       eqn->coef[var] -= sub->coef[var] * k / c;
1871
1872                     eqn->coef[i] = 0;
1873                     eqn->touched = 1;
1874                     renormalize = true;
1875                   }
1876
1877               for (e2 = pb->num_subs - 1; e2 >= 0; e2--)
1878                 if (pb->subs[e2].coef[i]
1879                     && (pb->subs[e2].color == omega_red
1880                         || (pb->subs[e2].color == omega_black
1881                             && pb->eqs[e].color == omega_black)))
1882                   {
1883                     eqn eqn = &(pb->subs[e2]);
1884                     int var, k;
1885
1886                     for (var = n_vars; var >= 0; var--)
1887                       eqn->coef[var] *= a;
1888
1889                     k = eqn->coef[i];
1890
1891                     for (var = n_vars; var >= 0; var--)
1892                       eqn->coef[var] -= sub->coef[var] * k / c;
1893
1894                     eqn->coef[i] = 0;
1895                     divide_eqn_by_gcd (eqn, n_vars);
1896                   }
1897
1898               if (dump_file && (dump_flags & TDF_DETAILS))
1899                 {
1900                   fprintf (dump_file, "cleaned-out wildcard: ");
1901                   omega_print_problem (dump_file, pb);
1902                 }
1903               break;
1904             }
1905         }
1906
1907   if (renormalize)
1908     normalize_omega_problem (pb);
1909 }
1910
1911 /* Swap values contained in I and J.  */
1912
1913 static inline void
1914 swap (int *i, int *j)
1915 {
1916   int tmp;
1917   tmp = *i;
1918   *i = *j;
1919   *j = tmp;
1920 }
1921
1922 /* Swap values contained in I and J.  */
1923
1924 static inline void
1925 bswap (bool *i, bool *j)
1926 {
1927   bool tmp;
1928   tmp = *i;
1929   *i = *j;
1930   *j = tmp;
1931 }
1932
1933 /* Make variable IDX unprotected in PB, by swapping its index at the
1934    PB->safe_vars rank.  */
1935
1936 static inline void
1937 omega_unprotect_1 (omega_pb pb, int *idx, bool *unprotect)
1938 {
1939   /* If IDX is protected...  */
1940   if (*idx < pb->safe_vars)
1941     {
1942       /* ... swap its index with the last non protected index.  */
1943       int j = pb->safe_vars;
1944       int e;
1945
1946       for (e = pb->num_geqs - 1; e >= 0; e--)
1947         {
1948           pb->geqs[e].touched = 1;
1949           swap (&pb->geqs[e].coef[*idx], &pb->geqs[e].coef[j]);
1950         }
1951
1952       for (e = pb->num_eqs - 1; e >= 0; e--)
1953         swap (&pb->eqs[e].coef[*idx], &pb->eqs[e].coef[j]);
1954
1955       for (e = pb->num_subs - 1; e >= 0; e--)
1956         swap (&pb->subs[e].coef[*idx], &pb->subs[e].coef[j]);
1957
1958       if (unprotect)
1959         bswap (&unprotect[*idx], &unprotect[j]);
1960
1961       swap (&pb->var[*idx], &pb->var[j]);
1962       pb->forwarding_address[pb->var[*idx]] = *idx;
1963       pb->forwarding_address[pb->var[j]] = j;
1964       (*idx)--;
1965     }
1966
1967   /* The variable at pb->safe_vars is also unprotected now.  */
1968   pb->safe_vars--;
1969 }
1970
1971 /* During the Fourier-Motzkin elimination some variables are
1972    substituted with other variables.  This function resurrects the
1973    substituted variables in PB.  */
1974
1975 static void
1976 resurrect_subs (omega_pb pb)
1977 {
1978   if (pb->num_subs > 0
1979       && please_no_equalities_in_simplified_problems == 0)
1980     {
1981       int i, e, n, m;
1982
1983       if (dump_file && (dump_flags & TDF_DETAILS))
1984         {
1985           fprintf (dump_file,
1986                    "problem reduced, bringing variables back to life\n");
1987           omega_print_problem (dump_file, pb);
1988         }
1989
1990       for (i = 1; omega_safe_var_p (pb, i); i++)
1991         if (omega_wildcard_p (pb, i))
1992           omega_unprotect_1 (pb, &i, NULL);
1993
1994       m = pb->num_subs;
1995       n = MAX (pb->num_vars, pb->safe_vars + m);
1996
1997       for (e = pb->num_geqs - 1; e >= 0; e--)
1998         if (single_var_geq (&pb->geqs[e], pb->num_vars))
1999           {
2000             if (!omega_safe_var_p (pb, abs (pb->geqs[e].key)))
2001               pb->geqs[e].key += (pb->geqs[e].key > 0 ? m : -m);
2002           }
2003         else
2004           {
2005             pb->geqs[e].touched = 1;
2006             pb->geqs[e].key = 0;
2007           }
2008
2009       for (i = pb->num_vars; !omega_safe_var_p (pb, i); i--)
2010         {
2011           pb->var[i + m] = pb->var[i];
2012
2013           for (e = pb->num_geqs - 1; e >= 0; e--)
2014             pb->geqs[e].coef[i + m] = pb->geqs[e].coef[i];
2015
2016           for (e = pb->num_eqs - 1; e >= 0; e--)
2017             pb->eqs[e].coef[i + m] = pb->eqs[e].coef[i];
2018
2019           for (e = pb->num_subs - 1; e >= 0; e--)
2020             pb->subs[e].coef[i + m] = pb->subs[e].coef[i];
2021         }
2022
2023       for (i = pb->safe_vars + m; !omega_safe_var_p (pb, i); i--)
2024         {
2025           for (e = pb->num_geqs - 1; e >= 0; e--)
2026             pb->geqs[e].coef[i] = 0;
2027
2028           for (e = pb->num_eqs - 1; e >= 0; e--)
2029             pb->eqs[e].coef[i] = 0;
2030
2031           for (e = pb->num_subs - 1; e >= 0; e--)
2032             pb->subs[e].coef[i] = 0;
2033         }
2034
2035       pb->num_vars += m;
2036
2037       for (e = pb->num_subs - 1; e >= 0; e--)
2038         {
2039           pb->var[pb->safe_vars + 1 + e] = pb->subs[e].key;
2040           omega_copy_eqn (&(pb->eqs[pb->num_eqs]), &(pb->subs[e]),
2041                           pb->num_vars);
2042           pb->eqs[pb->num_eqs].coef[pb->safe_vars + 1 + e] = -1;
2043           pb->eqs[pb->num_eqs].color = omega_black;
2044
2045           if (dump_file && (dump_flags & TDF_DETAILS))
2046             {
2047               fprintf (dump_file, "brought back: ");
2048               omega_print_eq (dump_file, pb, &pb->eqs[pb->num_eqs]);
2049               fprintf (dump_file, "\n");
2050             }
2051
2052           pb->num_eqs++;
2053           gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
2054         }
2055
2056       pb->safe_vars += m;
2057       pb->num_subs = 0;
2058
2059       if (dump_file && (dump_flags & TDF_DETAILS))
2060         {
2061           fprintf (dump_file, "variables brought back to life\n");
2062           omega_print_problem (dump_file, pb);
2063         }
2064
2065       cleanout_wildcards (pb);
2066     }
2067 }
2068
2069 static inline bool
2070 implies (unsigned int a, unsigned int b)
2071 {
2072   return (a == (a & b));
2073 }
2074
2075 /* Eliminate redundant equations in PB.  When EXPENSIVE is true, an
2076    extra step is performed.  Returns omega_false when there exist no
2077    solution, omega_true otherwise.  */
2078
2079 enum omega_result
2080 omega_eliminate_redundant (omega_pb pb, bool expensive)
2081 {
2082   int c, e, e1, e2, e3, p, q, i, k, alpha, alpha1, alpha2, alpha3;
2083   bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
2084   omega_pb tmp_problem;
2085
2086   /* {P,Z,N}EQS = {Positive,Zero,Negative} Equations.  */
2087   unsigned int *peqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS);
2088   unsigned int *zeqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS);
2089   unsigned int *neqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS);
2090
2091   /* PP = Possible Positives, PZ = Possible Zeros, PN = Possible Negatives */
2092   unsigned int pp, pz, pn;
2093
2094   if (dump_file && (dump_flags & TDF_DETAILS))
2095     {
2096       fprintf (dump_file, "in eliminate Redundant:\n");
2097       omega_print_problem (dump_file, pb);
2098     }
2099
2100   for (e = pb->num_geqs - 1; e >= 0; e--)
2101     {
2102       int tmp = 1;
2103
2104       is_dead[e] = false;
2105       peqs[e] = zeqs[e] = neqs[e] = 0;
2106
2107       for (i = pb->num_vars; i >= 1; i--)
2108         {
2109           if (pb->geqs[e].coef[i] > 0)
2110             peqs[e] |= tmp;
2111           else if (pb->geqs[e].coef[i] < 0)
2112             neqs[e] |= tmp;
2113           else
2114             zeqs[e] |= tmp;
2115
2116           tmp <<= 1;
2117         }
2118     }
2119
2120
2121   for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
2122     if (!is_dead[e1])
2123       for (e2 = e1 - 1; e2 >= 0; e2--)
2124         if (!is_dead[e2])
2125           {
2126             for (p = pb->num_vars; p > 1; p--)
2127               for (q = p - 1; q > 0; q--)
2128                 if ((alpha = pb->geqs[e1].coef[p] * pb->geqs[e2].coef[q]
2129                      - pb->geqs[e2].coef[p] * pb->geqs[e1].coef[q]) != 0)
2130                   goto foundPQ;
2131
2132             continue;
2133
2134           foundPQ:
2135             pz = ((zeqs[e1] & zeqs[e2]) | (peqs[e1] & neqs[e2])
2136                   | (neqs[e1] & peqs[e2]));
2137             pp = peqs[e1] | peqs[e2];
2138             pn = neqs[e1] | neqs[e2];
2139
2140             for (e3 = pb->num_geqs - 1; e3 >= 0; e3--)
2141               if (e3 != e1 && e3 != e2)
2142                 {
2143                   if (!implies (zeqs[e3], pz))
2144                     goto nextE3;
2145
2146                   alpha1 = (pb->geqs[e2].coef[q] * pb->geqs[e3].coef[p]
2147                             - pb->geqs[e2].coef[p] * pb->geqs[e3].coef[q]);
2148                   alpha2 = -(pb->geqs[e1].coef[q] * pb->geqs[e3].coef[p]
2149                              - pb->geqs[e1].coef[p] * pb->geqs[e3].coef[q]);
2150                   alpha3 = alpha;
2151
2152                   if (alpha1 * alpha2 <= 0)
2153                     goto nextE3;
2154
2155                   if (alpha1 < 0)
2156                     {
2157                       alpha1 = -alpha1;
2158                       alpha2 = -alpha2;
2159                       alpha3 = -alpha3;
2160                     }
2161
2162                   if (alpha3 > 0)
2163                     {
2164                       /* Trying to prove e3 is redundant.  */
2165                       if (!implies (peqs[e3], pp)
2166                           || !implies (neqs[e3], pn))
2167                         goto nextE3;
2168
2169                       if (pb->geqs[e3].color == omega_black
2170                           && (pb->geqs[e1].color == omega_red
2171                               || pb->geqs[e2].color == omega_red))
2172                         goto nextE3;
2173
2174                       for (k = pb->num_vars; k >= 1; k--)
2175                         if (alpha3 * pb->geqs[e3].coef[k]
2176                             != (alpha1 * pb->geqs[e1].coef[k]
2177                                 + alpha2 * pb->geqs[e2].coef[k]))
2178                           goto nextE3;
2179
2180                       c = (alpha1 * pb->geqs[e1].coef[0]
2181                            + alpha2 * pb->geqs[e2].coef[0]);
2182
2183                       if (c < alpha3 * (pb->geqs[e3].coef[0] + 1))
2184                         {
2185                           if (dump_file && (dump_flags & TDF_DETAILS))
2186                             {
2187                               fprintf (dump_file,
2188                                        "found redundant inequality\n");
2189                               fprintf (dump_file,
2190                                        "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2191                                        alpha1, alpha2, alpha3);
2192
2193                               omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
2194                               fprintf (dump_file, "\n");
2195                               omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2196                               fprintf (dump_file, "\n=> ");
2197                               omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2198                               fprintf (dump_file, "\n\n");
2199                             }
2200
2201                           is_dead[e3] = true;
2202                         }
2203                     }
2204                   else
2205                     {
2206                       /* Trying to prove e3 <= 0 and therefore e3 = 0,
2207                         or trying to prove e3 < 0, and therefore the
2208                         problem has no solutions.  */
2209                       if (!implies (peqs[e3], pn)
2210                           || !implies (neqs[e3], pp))
2211                         goto nextE3;
2212
2213                       if (pb->geqs[e1].color == omega_red
2214                           || pb->geqs[e2].color == omega_red
2215                           || pb->geqs[e3].color == omega_red)
2216                         goto nextE3;
2217
2218                       alpha3 = alpha3;
2219                       /* verify alpha1*v1+alpha2*v2 = alpha3*v3 */
2220                       for (k = pb->num_vars; k >= 1; k--)
2221                         if (alpha3 * pb->geqs[e3].coef[k]
2222                             != (alpha1 * pb->geqs[e1].coef[k]
2223                                 + alpha2 * pb->geqs[e2].coef[k]))
2224                           goto nextE3;
2225
2226                       c = (alpha1 * pb->geqs[e1].coef[0]
2227                            + alpha2 * pb->geqs[e2].coef[0]);
2228
2229                       if (c < alpha3 * (pb->geqs[e3].coef[0]))
2230                         {
2231                           /* We just proved e3 < 0, so no solutions exist.  */
2232                           if (dump_file && (dump_flags & TDF_DETAILS))
2233                             {
2234                               fprintf (dump_file,
2235                                        "found implied over tight inequality\n");
2236                               fprintf (dump_file,
2237                                        "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2238                                        alpha1, alpha2, -alpha3);
2239                               omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
2240                               fprintf (dump_file, "\n");
2241                               omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2242                               fprintf (dump_file, "\n=> not ");
2243                               omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2244                               fprintf (dump_file, "\n\n");
2245                             }
2246                           free (is_dead);
2247                           free (peqs);
2248                           free (zeqs);
2249                           free (neqs);
2250                           return omega_false;
2251                         }
2252                       else if (c < alpha3 * (pb->geqs[e3].coef[0] - 1))
2253                         {
2254                           /* We just proved that e3 <=0, so e3 = 0.  */
2255                           if (dump_file && (dump_flags & TDF_DETAILS))
2256                             {
2257                               fprintf (dump_file,
2258                                        "found implied tight inequality\n");
2259                               fprintf (dump_file,
2260                                        "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2261                                        alpha1, alpha2, -alpha3);
2262                               omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
2263                               fprintf (dump_file, "\n");
2264                               omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2265                               fprintf (dump_file, "\n=> inverse ");
2266                               omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2267                               fprintf (dump_file, "\n\n");
2268                             }
2269
2270                           omega_copy_eqn (&pb->eqs[pb->num_eqs++],
2271                                           &pb->geqs[e3], pb->num_vars);
2272                           gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
2273                           adding_equality_constraint (pb, pb->num_eqs - 1);
2274                           is_dead[e3] = true;
2275                         }
2276                     }
2277                 nextE3:;
2278                 }
2279           }
2280
2281   /* Delete the inequalities that were marked as dead.  */
2282   for (e = pb->num_geqs - 1; e >= 0; e--)
2283     if (is_dead[e])
2284       omega_delete_geq (pb, e, pb->num_vars);
2285
2286   if (!expensive)
2287     goto eliminate_redundant_done;
2288
2289   tmp_problem = XNEW (struct omega_pb);
2290   conservative++;
2291
2292   for (e = pb->num_geqs - 1; e >= 0; e--)
2293     {
2294       if (dump_file && (dump_flags & TDF_DETAILS))
2295         {
2296           fprintf (dump_file,
2297                    "checking equation %d to see if it is redundant: ", e);
2298           omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2299           fprintf (dump_file, "\n");
2300         }
2301
2302       omega_copy_problem (tmp_problem, pb);
2303       omega_negate_geq (tmp_problem, e);
2304       tmp_problem->safe_vars = 0;
2305       tmp_problem->variables_freed = false;
2306
2307       if (omega_solve_problem (tmp_problem, omega_false) == omega_false)
2308         omega_delete_geq (pb, e, pb->num_vars);
2309     }
2310
2311   free (tmp_problem);
2312   conservative--;
2313
2314   if (!omega_reduce_with_subs)
2315     {
2316       resurrect_subs (pb);
2317       gcc_assert (please_no_equalities_in_simplified_problems
2318                   || pb->num_subs == 0);
2319     }
2320
2321  eliminate_redundant_done:
2322   free (is_dead);
2323   free (peqs);
2324   free (zeqs);
2325   free (neqs);
2326   return omega_true;
2327 }
2328
2329 /* For each inequality that has coefficients bigger than 20, try to
2330    create a new constraint that cannot be derived from the original
2331    constraint and that has smaller coefficients.  Add the new
2332    constraint at the end of geqs.  Return the number of inequalities
2333    that have been added to PB.  */
2334
2335 static int
2336 smooth_weird_equations (omega_pb pb)
2337 {
2338   int e1, e2, e3, p, q, k, alpha, alpha1, alpha2, alpha3;
2339   int c;
2340   int v;
2341   int result = 0;
2342
2343   for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
2344     if (pb->geqs[e1].color == omega_black)
2345       {
2346         int g = 999999;
2347
2348         for (v = pb->num_vars; v >= 1; v--)
2349           if (pb->geqs[e1].coef[v] != 0 && abs (pb->geqs[e1].coef[v]) < g)
2350             g = abs (pb->geqs[e1].coef[v]);
2351
2352         /* Magic number.  */
2353         if (g > 20)
2354           {
2355             e3 = pb->num_geqs;
2356
2357             for (v = pb->num_vars; v >= 1; v--)
2358               pb->geqs[e3].coef[v] = int_div (6 * pb->geqs[e1].coef[v] + g / 2,
2359                                               g);
2360
2361             pb->geqs[e3].color = omega_black;
2362             pb->geqs[e3].touched = 1;
2363             /* Magic number.  */
2364             pb->geqs[e3].coef[0] = 9997;
2365
2366             if (dump_file && (dump_flags & TDF_DETAILS))
2367               {
2368                 fprintf (dump_file, "Checking to see if we can derive: ");
2369                 omega_print_geq (dump_file, pb, &pb->geqs[e3]);
2370                 fprintf (dump_file, "\n from: ");
2371                 omega_print_geq (dump_file, pb, &pb->geqs[e1]);
2372                 fprintf (dump_file, "\n");
2373               }
2374
2375             for (e2 = pb->num_geqs - 1; e2 >= 0; e2--)
2376               if (e1 != e2 && pb->geqs[e2].color == omega_black)
2377                 {
2378                   for (p = pb->num_vars; p > 1; p--)
2379                     {
2380                       for (q = p - 1; q > 0; q--)
2381                         {
2382                           alpha =
2383                             (pb->geqs[e1].coef[p] * pb->geqs[e2].coef[q] -
2384                              pb->geqs[e2].coef[p] * pb->geqs[e1].coef[q]);
2385                           if (alpha != 0)
2386                             goto foundPQ;
2387                         }
2388                     }
2389                   continue;
2390
2391                 foundPQ:
2392
2393                   alpha1 = (pb->geqs[e2].coef[q] * pb->geqs[e3].coef[p]
2394                             - pb->geqs[e2].coef[p] * pb->geqs[e3].coef[q]);
2395                   alpha2 = -(pb->geqs[e1].coef[q] * pb->geqs[e3].coef[p]
2396                              - pb->geqs[e1].coef[p] * pb->geqs[e3].coef[q]);
2397                   alpha3 = alpha;
2398
2399                   if (alpha1 * alpha2 <= 0)
2400                     continue;
2401
2402                   if (alpha1 < 0)
2403                     {
2404                       alpha1 = -alpha1;
2405                       alpha2 = -alpha2;
2406                       alpha3 = -alpha3;
2407                     }
2408
2409                   if (alpha3 > 0)
2410                     {
2411                       /* Try to prove e3 is redundant: verify
2412                          alpha1*v1 + alpha2*v2 = alpha3*v3.  */
2413                       for (k = pb->num_vars; k >= 1; k--)
2414                         if (alpha3 * pb->geqs[e3].coef[k]
2415                             != (alpha1 * pb->geqs[e1].coef[k]
2416                                 + alpha2 * pb->geqs[e2].coef[k]))
2417                           goto nextE2;
2418
2419                       c = alpha1 * pb->geqs[e1].coef[0]
2420                         + alpha2 * pb->geqs[e2].coef[0];
2421
2422                       if (c < alpha3 * (pb->geqs[e3].coef[0] + 1))
2423                         pb->geqs[e3].coef[0] = int_div (c, alpha3);
2424                     }
2425                 nextE2:;
2426                 }
2427
2428             if (pb->geqs[e3].coef[0] < 9997)
2429               {
2430                 result++;
2431                 pb->num_geqs++;
2432
2433                 if (dump_file && (dump_flags & TDF_DETAILS))
2434                   {
2435                     fprintf (dump_file,
2436                              "Smoothing wierd equations; adding:\n");
2437                     omega_print_geq (dump_file, pb, &pb->geqs[e3]);
2438                     fprintf (dump_file, "\nto:\n");
2439                     omega_print_problem (dump_file, pb);
2440                     fprintf (dump_file, "\n\n");
2441                   }
2442               }
2443           }
2444       }
2445   return result;
2446 }
2447
2448 /* Replace tuples of inequalities, that define upper and lower half
2449    spaces, with an equation.  */
2450
2451 static void
2452 coalesce (omega_pb pb)
2453 {
2454   int e, e2;
2455   int colors = 0;
2456   bool *is_dead;
2457   int found_something = 0;
2458
2459   for (e = 0; e < pb->num_geqs; e++)
2460     if (pb->geqs[e].color == omega_red)
2461       colors++;
2462
2463   if (colors < 2)
2464     return;
2465
2466   is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
2467
2468   for (e = 0; e < pb->num_geqs; e++)
2469     is_dead[e] = false;
2470
2471   for (e = 0; e < pb->num_geqs; e++)
2472     if (pb->geqs[e].color == omega_red
2473         && !pb->geqs[e].touched)
2474       for (e2 = e + 1; e2 < pb->num_geqs; e2++)
2475         if (!pb->geqs[e2].touched
2476             && pb->geqs[e].key == -pb->geqs[e2].key
2477             && pb->geqs[e].coef[0] == -pb->geqs[e2].coef[0]
2478             && pb->geqs[e2].color == omega_red)
2479           {
2480             omega_copy_eqn (&pb->eqs[pb->num_eqs++], &pb->geqs[e],
2481                             pb->num_vars);
2482             gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
2483             found_something++;
2484             is_dead[e] = true;
2485             is_dead[e2] = true;
2486           }
2487
2488   for (e = pb->num_geqs - 1; e >= 0; e--)
2489     if (is_dead[e])
2490       omega_delete_geq (pb, e, pb->num_vars);
2491
2492   if (dump_file && (dump_flags & TDF_DETAILS) && found_something)
2493     {
2494       fprintf (dump_file, "Coalesced pb->geqs into %d EQ's:\n",
2495                found_something);
2496       omega_print_problem (dump_file, pb);
2497     }
2498
2499   free (is_dead);
2500 }
2501
2502 /* Eliminate red inequalities from PB.  When ELIMINATE_ALL is
2503    true, continue to eliminate all the red inequalities.  */
2504
2505 void
2506 omega_eliminate_red (omega_pb pb, bool eliminate_all)
2507 {
2508   int e, e2, e3, i, j, k, a, alpha1, alpha2;
2509   int c = 0;
2510   bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
2511   int dead_count = 0;
2512   int red_found;
2513   omega_pb tmp_problem;
2514
2515   if (dump_file && (dump_flags & TDF_DETAILS))
2516     {
2517       fprintf (dump_file, "in eliminate RED:\n");
2518       omega_print_problem (dump_file, pb);
2519     }
2520
2521   if (pb->num_eqs > 0)
2522     omega_simplify_problem (pb);
2523
2524   for (e = pb->num_geqs - 1; e >= 0; e--)
2525     is_dead[e] = false;
2526
2527   for (e = pb->num_geqs - 1; e >= 0; e--)
2528     if (pb->geqs[e].color == omega_black && !is_dead[e])
2529       for (e2 = e - 1; e2 >= 0; e2--)
2530         if (pb->geqs[e2].color == omega_black
2531             && !is_dead[e2])
2532           {
2533             a = 0;
2534
2535             for (i = pb->num_vars; i > 1; i--)
2536               for (j = i - 1; j > 0; j--)
2537                 if ((a = (pb->geqs[e].coef[i] * pb->geqs[e2].coef[j]
2538                           - pb->geqs[e2].coef[i] * pb->geqs[e].coef[j])) != 0)
2539                   goto found_pair;
2540
2541             continue;
2542
2543           found_pair:
2544             if (dump_file && (dump_flags & TDF_DETAILS))
2545               {
2546                 fprintf (dump_file,
2547                          "found two equations to combine, i = %s, ",
2548                          omega_variable_to_str (pb, i));
2549                 fprintf (dump_file, "j = %s, alpha = %d\n",
2550                          omega_variable_to_str (pb, j), a);
2551                 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2552                 fprintf (dump_file, "\n");
2553                 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2554                 fprintf (dump_file, "\n");
2555               }
2556
2557             for (e3 = pb->num_geqs - 1; e3 >= 0; e3--)
2558               if (pb->geqs[e3].color == omega_red)
2559                 {
2560                   alpha1 = (pb->geqs[e2].coef[j] * pb->geqs[e3].coef[i]
2561                             - pb->geqs[e2].coef[i] * pb->geqs[e3].coef[j]);
2562                   alpha2 = -(pb->geqs[e].coef[j] * pb->geqs[e3].coef[i]
2563                              - pb->geqs[e].coef[i] * pb->geqs[e3].coef[j]);
2564
2565                   if ((a > 0 && alpha1 > 0 && alpha2 > 0)
2566                       || (a < 0 && alpha1 < 0 && alpha2 < 0))
2567                     {
2568                       if (dump_file && (dump_flags & TDF_DETAILS))
2569                         {
2570                           fprintf (dump_file,
2571                                    "alpha1 = %d, alpha2 = %d;"
2572                                    "comparing against: ",
2573                                    alpha1, alpha2);
2574                           omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2575                           fprintf (dump_file, "\n");
2576                         }
2577
2578                       for (k = pb->num_vars; k >= 0; k--)
2579                         {
2580                           c = (alpha1 * pb->geqs[e].coef[k]
2581                                + alpha2 * pb->geqs[e2].coef[k]);
2582
2583                           if (c != a * pb->geqs[e3].coef[k])
2584                             break;
2585
2586                           if (dump_file && (dump_flags & TDF_DETAILS) && k > 0)
2587                             fprintf (dump_file, " %s: %d, %d\n",
2588                                      omega_variable_to_str (pb, k), c,
2589                                      a * pb->geqs[e3].coef[k]);
2590                         }
2591
2592                       if (k < 0
2593                           || (k == 0 &&
2594                               ((a > 0 && c < a * pb->geqs[e3].coef[k])
2595                                || (a < 0 && c > a * pb->geqs[e3].coef[k]))))
2596                         {
2597                           if (dump_file && (dump_flags & TDF_DETAILS))
2598                             {
2599                               dead_count++;
2600                               fprintf (dump_file,
2601                                        "red equation#%d is dead "
2602                                        "(%d dead so far, %d remain)\n",
2603                                        e3, dead_count,
2604                                        pb->num_geqs - dead_count);
2605                               omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2606                               fprintf (dump_file, "\n");
2607                               omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2608                               fprintf (dump_file, "\n");
2609                               omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2610                               fprintf (dump_file, "\n");
2611                             }
2612                           is_dead[e3] = true;
2613                         }
2614                     }
2615                 }
2616           }
2617
2618   for (e = pb->num_geqs - 1; e >= 0; e--)
2619     if (is_dead[e])
2620       omega_delete_geq (pb, e, pb->num_vars);
2621
2622   free (is_dead);
2623
2624   if (dump_file && (dump_flags & TDF_DETAILS))
2625     {
2626       fprintf (dump_file, "in eliminate RED, easy tests done:\n");
2627       omega_print_problem (dump_file, pb);
2628     }
2629
2630   for (red_found = 0, e = pb->num_geqs - 1; e >= 0; e--)
2631     if (pb->geqs[e].color == omega_red)
2632       red_found = 1;
2633
2634   if (!red_found)
2635     {
2636       if (dump_file && (dump_flags & TDF_DETAILS))
2637         fprintf (dump_file, "fast checks worked\n");
2638
2639       if (!omega_reduce_with_subs)
2640         gcc_assert (please_no_equalities_in_simplified_problems
2641                     || pb->num_subs == 0);
2642
2643       return;
2644     }
2645
2646   if (!omega_verify_simplification
2647       && verify_omega_pb (pb) == omega_false)
2648     return;
2649
2650   conservative++;
2651   tmp_problem = XNEW (struct omega_pb);
2652
2653   for (e = pb->num_geqs - 1; e >= 0; e--)
2654     if (pb->geqs[e].color == omega_red)
2655       {
2656         if (dump_file && (dump_flags & TDF_DETAILS))
2657           {
2658             fprintf (dump_file,
2659                      "checking equation %d to see if it is redundant: ", e);
2660             omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2661             fprintf (dump_file, "\n");
2662           }
2663
2664         omega_copy_problem (tmp_problem, pb);
2665         omega_negate_geq (tmp_problem, e);
2666         tmp_problem->safe_vars = 0;
2667         tmp_problem->variables_freed = false;
2668         tmp_problem->num_subs = 0;
2669
2670         if (omega_solve_problem (tmp_problem, omega_false) == omega_false)
2671           {
2672             if (dump_file && (dump_flags & TDF_DETAILS))
2673               fprintf (dump_file, "it is redundant\n");
2674             omega_delete_geq (pb, e, pb->num_vars);
2675           }
2676         else
2677           {
2678             if (dump_file && (dump_flags & TDF_DETAILS))
2679               fprintf (dump_file, "it is not redundant\n");
2680
2681             if (!eliminate_all)
2682               {
2683                 if (dump_file && (dump_flags & TDF_DETAILS))
2684                   fprintf (dump_file, "no need to check other red equations\n");
2685                 break;
2686               }
2687           }
2688       }
2689
2690   conservative--;
2691   free (tmp_problem);
2692   /* omega_simplify_problem (pb); */
2693
2694   if (!omega_reduce_with_subs)
2695     gcc_assert (please_no_equalities_in_simplified_problems
2696                 || pb->num_subs == 0);
2697 }
2698
2699 /* Transform some wildcard variables to non-safe variables.  */
2700
2701 static void
2702 chain_unprotect (omega_pb pb)
2703 {
2704   int i, e;
2705   bool *unprotect = XNEWVEC (bool, OMEGA_MAX_VARS);
2706
2707   for (i = 1; omega_safe_var_p (pb, i); i++)
2708     {
2709       unprotect[i] = omega_wildcard_p (pb, i);
2710
2711       for (e = pb->num_subs - 1; e >= 0; e--)
2712         if (pb->subs[e].coef[i])
2713           unprotect[i] = false;
2714     }
2715
2716   if (dump_file && (dump_flags & TDF_DETAILS))
2717     {
2718       fprintf (dump_file, "Doing chain reaction unprotection\n");
2719       omega_print_problem (dump_file, pb);
2720
2721       for (i = 1; omega_safe_var_p (pb, i); i++)
2722         if (unprotect[i])
2723           fprintf (dump_file, "unprotecting %s\n",
2724                    omega_variable_to_str (pb, i));
2725     }
2726
2727   for (i = 1; omega_safe_var_p (pb, i); i++)
2728     if (unprotect[i])
2729       omega_unprotect_1 (pb, &i, unprotect);
2730
2731   if (dump_file && (dump_flags & TDF_DETAILS))
2732     {
2733       fprintf (dump_file, "After chain reactions\n");
2734       omega_print_problem (dump_file, pb);
2735     }
2736
2737   free (unprotect);
2738 }
2739
2740 /* Reduce problem PB.  */
2741
2742 static void
2743 omega_problem_reduced (omega_pb pb)
2744 {
2745   if (omega_verify_simplification
2746       && !in_approximate_mode
2747       && verify_omega_pb (pb) == omega_false)
2748     return;
2749
2750   if (PARAM_VALUE (PARAM_OMEGA_ELIMINATE_REDUNDANT_CONSTRAINTS)
2751       && !omega_eliminate_redundant (pb, true))
2752     return;
2753
2754   omega_found_reduction = omega_true;
2755
2756   if (!please_no_equalities_in_simplified_problems)
2757     coalesce (pb);
2758
2759   if (omega_reduce_with_subs
2760       || please_no_equalities_in_simplified_problems)
2761     chain_unprotect (pb);
2762   else
2763     resurrect_subs (pb);
2764
2765   if (!return_single_result)
2766     {
2767       int i;
2768
2769       for (i = 1; omega_safe_var_p (pb, i); i++)
2770         pb->forwarding_address[pb->var[i]] = i;
2771
2772       for (i = 0; i < pb->num_subs; i++)
2773         pb->forwarding_address[pb->subs[i].key] = -i - 1;
2774
2775       (*omega_when_reduced) (pb);
2776     }
2777
2778   if (dump_file && (dump_flags & TDF_DETAILS))
2779     {
2780       fprintf (dump_file, "-------------------------------------------\n");
2781       fprintf (dump_file, "problem reduced:\n");
2782       omega_print_problem (dump_file, pb);
2783       fprintf (dump_file, "-------------------------------------------\n");
2784     }
2785 }
2786
2787 /* Eliminates all the free variables for problem PB, that is all the
2788    variables from FV to PB->NUM_VARS.  */
2789
2790 static void
2791 omega_free_eliminations (omega_pb pb, int fv)
2792 {
2793   bool try_again = true;
2794   int i, e, e2;
2795   int n_vars = pb->num_vars;
2796
2797   while (try_again)
2798     {
2799       try_again = false;
2800
2801       for (i = n_vars; i > fv; i--)
2802         {
2803           for (e = pb->num_geqs - 1; e >= 0; e--)
2804             if (pb->geqs[e].coef[i])
2805               break;
2806
2807           if (e < 0)
2808             e2 = e;
2809           else if (pb->geqs[e].coef[i] > 0)
2810             {
2811               for (e2 = e - 1; e2 >= 0; e2--)
2812                 if (pb->geqs[e2].coef[i] < 0)
2813                   break;
2814             }
2815           else
2816             {
2817               for (e2 = e - 1; e2 >= 0; e2--)
2818                 if (pb->geqs[e2].coef[i] > 0)
2819                   break;
2820             }
2821
2822           if (e2 < 0)
2823             {
2824               int e3;
2825               for (e3 = pb->num_subs - 1; e3 >= 0; e3--)
2826                 if (pb->subs[e3].coef[i])
2827                   break;
2828
2829               if (e3 >= 0)
2830                 continue;
2831
2832               for (e3 = pb->num_eqs - 1; e3 >= 0; e3--)
2833                 if (pb->eqs[e3].coef[i])
2834                   break;
2835
2836               if (e3 >= 0)
2837                 continue;
2838
2839               if (dump_file && (dump_flags & TDF_DETAILS))
2840                 fprintf (dump_file, "a free elimination of %s\n",
2841                          omega_variable_to_str (pb, i));
2842
2843               if (e >= 0)
2844                 {
2845                   omega_delete_geq (pb, e, n_vars);
2846
2847                   for (e--; e >= 0; e--)
2848                     if (pb->geqs[e].coef[i])
2849                       omega_delete_geq (pb, e, n_vars);
2850
2851                   try_again = (i < n_vars);
2852                 }
2853
2854               omega_delete_variable (pb, i);
2855               n_vars = pb->num_vars;
2856             }
2857         }
2858     }
2859
2860   if (dump_file && (dump_flags & TDF_DETAILS))
2861     {
2862       fprintf (dump_file, "\nafter free eliminations:\n");
2863       omega_print_problem (dump_file, pb);
2864       fprintf (dump_file, "\n");
2865     }
2866 }
2867
2868 /* Do free red eliminations.  */
2869
2870 static void
2871 free_red_eliminations (omega_pb pb)
2872 {
2873   bool try_again = true;
2874   int i, e, e2;
2875   int n_vars = pb->num_vars;
2876   bool *is_red_var = XNEWVEC (bool, OMEGA_MAX_VARS);
2877   bool *is_dead_var = XNEWVEC (bool, OMEGA_MAX_VARS);
2878   bool *is_dead_geq = XNEWVEC (bool, OMEGA_MAX_GEQS);
2879
2880   for (i = n_vars; i > 0; i--)
2881     {
2882       is_red_var[i] = false;
2883       is_dead_var[i] = false;
2884     }
2885
2886   for (e = pb->num_geqs - 1; e >= 0; e--)
2887     {
2888       is_dead_geq[e] = false;
2889
2890       if (pb->geqs[e].color == omega_red)
2891         for (i = n_vars; i > 0; i--)
2892           if (pb->geqs[e].coef[i] != 0)
2893             is_red_var[i] = true;
2894     }
2895
2896   while (try_again)
2897     {
2898       try_again = false;
2899       for (i = n_vars; i > 0; i--)
2900         if (!is_red_var[i] && !is_dead_var[i])
2901           {
2902             for (e = pb->num_geqs - 1; e >= 0; e--)
2903               if (!is_dead_geq[e] && pb->geqs[e].coef[i])
2904                 break;
2905
2906             if (e < 0)
2907               e2 = e;
2908             else if (pb->geqs[e].coef[i] > 0)
2909               {
2910                 for (e2 = e - 1; e2 >= 0; e2--)
2911                   if (!is_dead_geq[e2] && pb->geqs[e2].coef[i] < 0)
2912                     break;
2913               }
2914             else
2915               {
2916                 for (e2 = e - 1; e2 >= 0; e2--)
2917                   if (!is_dead_geq[e2] && pb->geqs[e2].coef[i] > 0)
2918                     break;
2919               }
2920
2921             if (e2 < 0)
2922               {
2923                 int e3;
2924                 for (e3 = pb->num_subs - 1; e3 >= 0; e3--)
2925                   if (pb->subs[e3].coef[i])
2926                     break;
2927
2928                 if (e3 >= 0)
2929                   continue;
2930
2931                 for (e3 = pb->num_eqs - 1; e3 >= 0; e3--)
2932                   if (pb->eqs[e3].coef[i])
2933                     break;
2934
2935                 if (e3 >= 0)
2936                   continue;
2937
2938                 if (dump_file && (dump_flags & TDF_DETAILS))
2939                   fprintf (dump_file, "a free red elimination of %s\n",
2940                            omega_variable_to_str (pb, i));
2941
2942                 for (; e >= 0; e--)
2943                   if (pb->geqs[e].coef[i])
2944                     is_dead_geq[e] = true;
2945
2946                 try_again = true;
2947                 is_dead_var[i] = true;
2948               }
2949           }
2950     }
2951
2952   for (e = pb->num_geqs - 1; e >= 0; e--)
2953     if (is_dead_geq[e])
2954       omega_delete_geq (pb, e, n_vars);
2955
2956   for (i = n_vars; i > 0; i--)
2957     if (is_dead_var[i])
2958       omega_delete_variable (pb, i);
2959
2960   if (dump_file && (dump_flags & TDF_DETAILS))
2961     {
2962       fprintf (dump_file, "\nafter free red eliminations:\n");
2963       omega_print_problem (dump_file, pb);
2964       fprintf (dump_file, "\n");
2965     }
2966
2967   free (is_red_var);
2968   free (is_dead_var);
2969   free (is_dead_geq);
2970 }
2971
2972 /* For equation EQ of the form "0 = EQN", insert in PB two
2973    inequalities "0 <= EQN" and "0 <= -EQN".  */
2974
2975 void
2976 omega_convert_eq_to_geqs (omega_pb pb, int eq)
2977 {
2978   int i;
2979
2980   if (dump_file && (dump_flags & TDF_DETAILS))
2981     fprintf (dump_file, "Converting Eq to Geqs\n");
2982
2983   /* Insert "0 <= EQN".  */
2984   omega_copy_eqn (&pb->geqs[pb->num_geqs], &pb->eqs[eq], pb->num_vars);
2985   pb->geqs[pb->num_geqs].touched = 1;
2986   pb->num_geqs++;
2987
2988   /* Insert "0 <= -EQN".  */
2989   omega_copy_eqn (&pb->geqs[pb->num_geqs], &pb->eqs[eq], pb->num_vars);
2990   pb->geqs[pb->num_geqs].touched = 1;
2991
2992   for (i = 0; i <= pb->num_vars; i++)
2993     pb->geqs[pb->num_geqs].coef[i] *= -1;
2994
2995   pb->num_geqs++;
2996
2997   if (dump_file && (dump_flags & TDF_DETAILS))
2998     omega_print_problem (dump_file, pb);
2999 }
3000
3001 /* Eliminates variable I from PB.  */
3002
3003 static void
3004 omega_do_elimination (omega_pb pb, int e, int i)
3005 {
3006   eqn sub = omega_alloc_eqns (0, 1);
3007   int c;
3008   int n_vars = pb->num_vars;
3009
3010   if (dump_file && (dump_flags & TDF_DETAILS))
3011     fprintf (dump_file, "eliminating variable %s\n",
3012              omega_variable_to_str (pb, i));
3013
3014   omega_copy_eqn (sub, &pb->eqs[e], pb->num_vars);
3015   c = sub->coef[i];
3016   sub->coef[i] = 0;
3017   if (c == 1 || c == -1)
3018     {
3019       if (pb->eqs[e].color == omega_red)
3020         {
3021           bool fB;
3022           omega_substitute_red (pb, sub, i, c, &fB);
3023           if (fB)
3024             omega_convert_eq_to_geqs (pb, e);
3025           else
3026             omega_delete_variable (pb, i);
3027         }
3028       else
3029         {
3030           omega_substitute (pb, sub, i, c);
3031           omega_delete_variable (pb, i);
3032         }
3033     }
3034   else
3035     {
3036       int a = abs (c);
3037       int e2 = e;
3038
3039       if (dump_file && (dump_flags & TDF_DETAILS))
3040         fprintf (dump_file, "performing non-exact elimination, c = %d\n", c);
3041
3042       for (e = pb->num_eqs - 1; e >= 0; e--)
3043         if (pb->eqs[e].coef[i])
3044           {
3045             eqn eqn = &(pb->eqs[e]);
3046             int j, k;
3047             for (j = n_vars; j >= 0; j--)
3048               eqn->coef[j] *= a;
3049             k = eqn->coef[i];
3050             eqn->coef[i] = 0;
3051             eqn->color |= sub->color;
3052             for (j = n_vars; j >= 0; j--)
3053               eqn->coef[j] -= sub->coef[j] * k / c;
3054           }
3055
3056       for (e = pb->num_geqs - 1; e >= 0; e--)
3057         if (pb->geqs[e].coef[i])
3058           {
3059             eqn eqn = &(pb->geqs[e]);
3060             int j, k;
3061
3062             if (sub->color == omega_red)
3063               eqn->color = omega_red;
3064
3065             for (j = n_vars; j >= 0; j--)
3066               eqn->coef[j] *= a;
3067
3068             eqn->touched = 1;
3069             k = eqn->coef[i];
3070             eqn->coef[i] = 0;
3071
3072             for (j = n_vars; j >= 0; j--)
3073               eqn->coef[j] -= sub->coef[j] * k / c;
3074
3075           }
3076
3077       for (e = pb->num_subs - 1; e >= 0; e--)
3078         if (pb->subs[e].coef[i])
3079           {
3080             eqn eqn = &(pb->subs[e]);
3081             int j, k;
3082             gcc_assert (0);
3083             gcc_assert (sub->color == omega_black);
3084             for (j = n_vars; j >= 0; j--)
3085               eqn->coef[j] *= a;
3086             k = eqn->coef[i];
3087             eqn->coef[i] = 0;
3088             for (j = n_vars; j >= 0; j--)
3089               eqn->coef[j] -= sub->coef[j] * k / c;
3090           }
3091
3092       if (in_approximate_mode)
3093         omega_delete_variable (pb, i);
3094       else
3095         omega_convert_eq_to_geqs (pb, e2);
3096     }
3097
3098   omega_free_eqns (sub, 1);
3099 }
3100
3101 /* Helper function for printing "sorry, no solution".  */
3102
3103 static inline enum omega_result
3104 omega_problem_has_no_solution (void)
3105 {
3106   if (dump_file && (dump_flags & TDF_DETAILS))
3107     fprintf (dump_file, "\nequations have no solution \n");
3108
3109   return omega_false;
3110 }
3111
3112 /* Helper function: solve equations in PB one at a time, following the
3113    DESIRED_RES result.  */
3114
3115 static enum omega_result
3116 omega_solve_eq (omega_pb pb, enum omega_result desired_res)
3117 {
3118   int i, j, e;
3119   int g, g2;
3120   g = 0;
3121
3122
3123   if (dump_file && (dump_flags & TDF_DETAILS) && pb->num_eqs > 0)
3124     {
3125       fprintf (dump_file, "\nomega_solve_eq (%d, %d)\n",
3126                desired_res, may_be_red);
3127       omega_print_problem (dump_file, pb);
3128       fprintf (dump_file, "\n");
3129     }
3130
3131   if (may_be_red)
3132     {
3133       i = 0;
3134       j = pb->num_eqs - 1;
3135
3136       while (1)
3137         {
3138           eqn eq;
3139
3140           while (i <= j && pb->eqs[i].color == omega_red)
3141             i++;
3142
3143           while (i <= j && pb->eqs[j].color == omega_black)
3144             j--;
3145
3146           if (i >= j)
3147             break;
3148
3149           eq = omega_alloc_eqns (0, 1);
3150           omega_copy_eqn (eq, &pb->eqs[i], pb->num_vars);
3151           omega_copy_eqn (&pb->eqs[i], &pb->eqs[j], pb->num_vars);
3152           omega_copy_eqn (&pb->eqs[j], eq, pb->num_vars);
3153           omega_free_eqns (eq, 1);
3154           i++;
3155           j--;
3156         }
3157     }
3158
3159   /* Eliminate all EQ equations */
3160   for (e = pb->num_eqs - 1; e >= 0; e--)
3161     {
3162       eqn eqn = &(pb->eqs[e]);
3163       int sv;
3164
3165       if (dump_file && (dump_flags & TDF_DETAILS))
3166         fprintf (dump_file, "----\n");
3167
3168       for (i = pb->num_vars; i > 0; i--)
3169         if (eqn->coef[i])
3170           break;
3171
3172       g = eqn->coef[i];
3173
3174       for (j = i - 1; j > 0; j--)
3175         if (eqn->coef[j])
3176           break;
3177
3178       /* i is the position of last nonzero coefficient,
3179          g is the coefficient of i,
3180          j is the position of next nonzero coefficient.  */
3181
3182       if (j == 0)
3183         {
3184           if (eqn->coef[0] % g != 0)
3185             return omega_problem_has_no_solution ();
3186
3187           eqn->coef[0] = eqn->coef[0] / g;
3188           eqn->coef[i] = 1;
3189           pb->num_eqs--;
3190           omega_do_elimination (pb, e, i);
3191           continue;
3192         }
3193
3194       else if (j == -1)
3195         {
3196           if (eqn->coef[0] != 0)
3197             return omega_problem_has_no_solution ();
3198
3199           pb->num_eqs--;
3200           continue;
3201         }
3202
3203       if (g < 0)
3204         g = -g;
3205
3206       if (g == 1)
3207         {
3208           pb->num_eqs--;
3209           omega_do_elimination (pb, e, i);
3210         }
3211
3212       else
3213         {
3214           int k = j;
3215           bool promotion_possible =
3216             (omega_safe_var_p (pb, j)
3217              && pb->safe_vars + 1 == i
3218              && !omega_eqn_is_red (eqn, desired_res)
3219              && !in_approximate_mode);
3220
3221           if (dump_file && (dump_flags & TDF_DETAILS) && promotion_possible)
3222             fprintf (dump_file, " Promotion possible\n");
3223
3224         normalizeEQ:
3225           if (!omega_safe_var_p (pb, j))
3226             {
3227               for (; g != 1 && !omega_safe_var_p (pb, j); j--)
3228                 g = gcd (abs (eqn->coef[j]), g);
3229               g2 = g;
3230             }
3231           else if (!omega_safe_var_p (pb, i))
3232             g2 = g;
3233           else
3234             g2 = 0;
3235
3236           for (; g != 1 && j > 0; j--)
3237             g = gcd (abs (eqn->coef[j]), g);
3238
3239           if (g > 1)
3240             {
3241               if (eqn->coef[0] % g != 0)
3242                 return omega_problem_has_no_solution ();
3243
3244               for (j = 0; j <= pb->num_vars; j++)
3245                 eqn->coef[j] /= g;
3246
3247               g2 = g2 / g;
3248             }
3249
3250           if (g2 > 1)
3251             {
3252               int e2;
3253
3254               for (e2 = e - 1; e2 >= 0; e2--)
3255                 if (pb->eqs[e2].coef[i])
3256                   break;
3257
3258               if (e2 == -1)
3259                 for (e2 = pb->num_geqs - 1; e2 >= 0; e2--)
3260                   if (pb->geqs[e2].coef[i])
3261                     break;
3262
3263               if (e2 == -1)
3264                 for (e2 = pb->num_subs - 1; e2 >= 0; e2--)
3265                   if (pb->subs[e2].coef[i])
3266                     break;
3267
3268               if (e2 == -1)
3269                 {
3270                   bool change = false;
3271
3272                   if (dump_file && (dump_flags & TDF_DETAILS))
3273                     {
3274                       fprintf (dump_file, "Ha! We own it! \n");
3275                       omega_print_eq (dump_file, pb, eqn);
3276                       fprintf (dump_file, " \n");
3277                     }
3278
3279                   g = eqn->coef[i];
3280                   g = abs (g);
3281
3282                   for (j = i - 1; j >= 0; j--)
3283                     {
3284                       int t = int_mod (eqn->coef[j], g);
3285
3286                       if (2 * t >= g)
3287                         t -= g;
3288
3289                       if (t != eqn->coef[j])
3290                         {
3291                           eqn->coef[j] = t;
3292                           change = true;
3293                         }
3294                     }
3295
3296                   if (!change)
3297                     {
3298                       if (dump_file && (dump_flags & TDF_DETAILS))
3299                         fprintf (dump_file, "So what?\n");
3300                     }
3301
3302                   else
3303                     {
3304                       omega_name_wild_card (pb, i);
3305
3306                       if (dump_file && (dump_flags & TDF_DETAILS))
3307                         {
3308                           omega_print_eq (dump_file, pb, eqn);
3309                           fprintf (dump_file, " \n");
3310                         }
3311
3312                       e++;
3313                       continue;
3314                     }
3315                 }
3316             }
3317
3318           if (promotion_possible)
3319             {
3320               if (dump_file && (dump_flags & TDF_DETAILS))
3321                 {
3322                   fprintf (dump_file, "promoting %s to safety\n",
3323                            omega_variable_to_str (pb, i));
3324                   omega_print_vars (dump_file, pb);
3325                 }
3326
3327               pb->safe_vars++;
3328
3329               if (!omega_wildcard_p (pb, i))
3330                 omega_name_wild_card (pb, i);
3331
3332               promotion_possible = false;
3333               j = k;
3334               goto normalizeEQ;
3335             }
3336
3337           if (g2 > 1 && !in_approximate_mode)
3338             {
3339               if (pb->eqs[e].color == omega_red)
3340                 {
3341                   if (dump_file && (dump_flags & TDF_DETAILS))
3342                     fprintf (dump_file, "handling red equality\n");
3343
3344                   pb->num_eqs--;
3345                   omega_do_elimination (pb, e, i);
3346                   continue;
3347                 }
3348
3349               if (dump_file && (dump_flags & TDF_DETAILS))
3350                 {
3351                   fprintf (dump_file,
3352                            "adding equation to handle safe variable \n");
3353                   omega_print_eq (dump_file, pb, eqn);
3354                   fprintf (dump_file, "\n----\n");
3355                   omega_print_problem (dump_file, pb);
3356                   fprintf (dump_file, "\n----\n");
3357                   fprintf (dump_file, "\n----\n");
3358                 }
3359
3360               i = omega_add_new_wild_card (pb);
3361               pb->num_eqs++;
3362               gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
3363               omega_init_eqn_zero (&pb->eqs[e + 1], pb->num_vars);
3364               omega_copy_eqn (&pb->eqs[e + 1], eqn, pb->safe_vars);
3365
3366               for (j = pb->num_vars; j >= 0; j--)
3367                 {
3368                   pb->eqs[e + 1].coef[j] = int_mod (pb->eqs[e + 1].coef[j], g2);
3369
3370                   if (2 * pb->eqs[e + 1].coef[j] >= g2)
3371                     pb->eqs[e + 1].coef[j] -= g2;
3372                 }
3373
3374               pb->eqs[e + 1].coef[i] = g2;
3375               e += 2;
3376
3377               if (dump_file && (dump_flags & TDF_DETAILS))
3378                 omega_print_problem (dump_file, pb);
3379
3380               continue;
3381             }
3382
3383           sv = pb->safe_vars;
3384           if (g2 == 0)
3385             sv = 0;
3386
3387           /* Find variable to eliminate.  */
3388           if (g2 > 1)
3389             {
3390               gcc_assert (in_approximate_mode);
3391
3392               if (dump_file && (dump_flags & TDF_DETAILS))
3393                 {
3394                   fprintf (dump_file, "non-exact elimination: ");
3395                   omega_print_eq (dump_file, pb, eqn);
3396                   fprintf (dump_file, "\n");
3397                   omega_print_problem (dump_file, pb);
3398                 }
3399
3400               for (i = pb->num_vars; i > sv; i--)
3401                 if (pb->eqs[e].coef[i] != 0)
3402                   break;
3403             }
3404           else
3405             for (i = pb->num_vars; i > sv; i--)
3406               if (pb->eqs[e].coef[i] == 1 || pb->eqs[e].coef[i] == -1)
3407                 break;
3408
3409           if (i > sv)
3410             {
3411               pb->num_eqs--;
3412               omega_do_elimination (pb, e, i);
3413
3414               if (dump_file && (dump_flags & TDF_DETAILS) && g2 > 1)
3415                 {
3416                   fprintf (dump_file, "result of non-exact elimination:\n");
3417                   omega_print_problem (dump_file, pb);
3418                 }
3419             }
3420           else
3421             {
3422               int factor = (INT_MAX);
3423               j = 0;
3424
3425               if (dump_file && (dump_flags & TDF_DETAILS))
3426                 fprintf (dump_file, "doing moding\n");
3427
3428               for (i = pb->num_vars; i != sv; i--)
3429                 if ((pb->eqs[e].coef[i] & 1) != 0)
3430                   {
3431                     j = i;
3432                     i--;
3433
3434                     for (; i != sv; i--)
3435                       if ((pb->eqs[e].coef[i] & 1) != 0)
3436                         break;
3437
3438                     break;
3439                   }
3440
3441               if (j != 0 && i == sv)
3442                 {
3443                   omega_do_mod (pb, 2, e, j);
3444                   e++;
3445                   continue;
3446                 }
3447
3448               j = 0;
3449               for (i = pb->num_vars; i != sv; i--)
3450                 if (pb->eqs[e].coef[i] != 0
3451                     && factor > abs (pb->eqs[e].coef[i]) + 1)
3452                   {
3453                     factor = abs (pb->eqs[e].coef[i]) + 1;
3454                     j = i;
3455                   }
3456
3457               if (j == sv)
3458                 {
3459                   if (dump_file && (dump_flags & TDF_DETAILS))
3460                     fprintf (dump_file, "should not have happened\n");
3461                   gcc_assert (0);
3462                 }
3463
3464               omega_do_mod (pb, factor, e, j);
3465               /* Go back and try this equation again.  */
3466               e++;
3467             }
3468         }
3469     }
3470
3471   pb->num_eqs = 0;
3472   return omega_unknown;
3473 }
3474
3475 /* Transform an inequation E to an equality, then solve DIFF problems
3476    based on PB, and only differing by the constant part that is
3477    diminished by one, trying to figure out which of the constants
3478    satisfies PB.    */
3479
3480 static enum omega_result
3481 parallel_splinter (omega_pb pb, int e, int diff,
3482                    enum omega_result desired_res)
3483 {
3484   omega_pb tmp_problem;
3485   int i;
3486
3487   if (dump_file && (dump_flags & TDF_DETAILS))
3488     {
3489       fprintf (dump_file, "Using parallel splintering\n");
3490       omega_print_problem (dump_file, pb);
3491     }
3492
3493   tmp_problem = XNEW (struct omega_pb);
3494   omega_copy_eqn (&pb->eqs[0], &pb->geqs[e], pb->num_vars);
3495   pb->num_eqs = 1;
3496
3497   for (i = 0; i <= diff; i++)
3498     {
3499       omega_copy_problem (tmp_problem, pb);
3500
3501       if (dump_file && (dump_flags & TDF_DETAILS))
3502         {
3503           fprintf (dump_file, "Splinter # %i\n", i);
3504           omega_print_problem (dump_file, pb);
3505         }
3506
3507       if (omega_solve_problem (tmp_problem, desired_res) == omega_true)
3508         {
3509           free (tmp_problem);
3510           return omega_true;
3511         }
3512
3513       pb->eqs[0].coef[0]--;
3514     }
3515
3516   free (tmp_problem);
3517   return omega_false;
3518 }
3519
3520 /* Helper function: solve equations one at a time.  */
3521
3522 static enum omega_result
3523 omega_solve_geq (omega_pb pb, enum omega_result desired_res)
3524 {
3525   int i, e;
3526   int n_vars, fv;
3527   enum omega_result result;
3528   bool coupled_subscripts = false;
3529   bool smoothed = false;
3530   bool eliminate_again;
3531   bool tried_eliminating_redundant = false;
3532
3533   if (desired_res != omega_simplify)
3534     {
3535       pb->num_subs = 0;
3536       pb->safe_vars = 0;
3537     }
3538
3539  solve_geq_start:
3540   do {
3541     gcc_assert (desired_res == omega_simplify || pb->num_subs == 0);
3542
3543     /* Verify that there are not too many inequalities.  */
3544     gcc_assert (pb->num_geqs <= OMEGA_MAX_GEQS);
3545
3546     if (dump_file && (dump_flags & TDF_DETAILS))
3547       {
3548         fprintf (dump_file, "\nomega_solve_geq (%d,%d):\n",
3549                  desired_res, please_no_equalities_in_simplified_problems);
3550         omega_print_problem (dump_file, pb);
3551         fprintf (dump_file, "\n");
3552       }
3553
3554     n_vars = pb->num_vars;
3555
3556     if (n_vars == 1)
3557       {
3558         enum omega_eqn_color u_color = omega_black;
3559         enum omega_eqn_color l_color = omega_black;
3560         int upper_bound = pos_infinity;
3561         int lower_bound = neg_infinity;
3562
3563         for (e = pb->num_geqs - 1; e >= 0; e--)
3564           {
3565             int a = pb->geqs[e].coef[1];
3566             int c = pb->geqs[e].coef[0];
3567
3568             /* Our equation is ax + c >= 0, or ax >= -c, or c >= -ax.  */
3569             if (a == 0)
3570               {
3571                 if (c < 0)
3572                   return omega_problem_has_no_solution ();
3573               }
3574             else if (a > 0)
3575               {
3576                 if (a != 1)
3577                   c = int_div (c, a);
3578
3579                 if (lower_bound < -c
3580                     || (lower_bound == -c
3581                         && !omega_eqn_is_red (&pb->geqs[e], desired_res)))
3582                   {
3583                     lower_bound = -c;
3584                     l_color = pb->geqs[e].color;
3585                   }
3586               }
3587             else
3588               {
3589                 if (a != -1)
3590                   c = int_div (c, -a);
3591
3592                 if (upper_bound > c
3593                     || (upper_bound == c
3594                         && !omega_eqn_is_red (&pb->geqs[e], desired_res)))
3595                   {
3596                     upper_bound = c;
3597                     u_color = pb->geqs[e].color;
3598                   }
3599               }
3600           }
3601
3602         if (dump_file && (dump_flags & TDF_DETAILS))
3603           {
3604             fprintf (dump_file, "upper bound = %d\n", upper_bound);
3605             fprintf (dump_file, "lower bound = %d\n", lower_bound);
3606           }
3607
3608         if (lower_bound > upper_bound)
3609           return omega_problem_has_no_solution ();
3610
3611         if (desired_res == omega_simplify)
3612           {
3613             pb->num_geqs = 0;
3614             if (pb->safe_vars == 1)
3615               {
3616
3617                 if (lower_bound == upper_bound
3618                     && u_color == omega_black
3619                     && l_color == omega_black)
3620                   {
3621                     pb->eqs[0].coef[0] = -lower_bound;
3622                     pb->eqs[0].coef[1] = 1;
3623                     pb->eqs[0].color = omega_black;
3624                     pb->num_eqs = 1;
3625                     return omega_solve_problem (pb, desired_res);
3626                   }
3627                 else
3628                   {
3629                     if (lower_bound > neg_infinity)
3630                       {
3631                         pb->geqs[0].coef[0] = -lower_bound;
3632                         pb->geqs[0].coef[1] = 1;
3633                         pb->geqs[0].key = 1;
3634                         pb->geqs[0].color = l_color;
3635                         pb->geqs[0].touched = 0;
3636                         pb->num_geqs = 1;
3637                       }
3638
3639                     if (upper_bound < pos_infinity)
3640                       {
3641                         pb->geqs[pb->num_geqs].coef[0] = upper_bound;
3642                         pb->geqs[pb->num_geqs].coef[1] = -1;
3643                         pb->geqs[pb->num_geqs].key = -1;
3644                         pb->geqs[pb->num_geqs].color = u_color;
3645                         pb->geqs[pb->num_geqs].touched = 0;
3646                         pb->num_geqs++;
3647                       }
3648                   }
3649               }
3650             else
3651               pb->num_vars = 0;
3652
3653             omega_problem_reduced (pb);
3654             return omega_false;
3655           }
3656
3657         if (original_problem != no_problem
3658             && l_color == omega_black
3659             && u_color == omega_black
3660             && !conservative
3661             && lower_bound == upper_bound)
3662           {
3663             pb->eqs[0].coef[0] = -lower_bound;
3664             pb->eqs[0].coef[1] = 1;
3665             pb->num_eqs = 1;
3666             adding_equality_constraint (pb, 0);
3667           }
3668
3669         return omega_true;
3670       }
3671
3672     if (!pb->variables_freed)
3673       {
3674         pb->variables_freed = true;
3675
3676         if (desired_res != omega_simplify)
3677           omega_free_eliminations (pb, 0);
3678         else
3679           omega_free_eliminations (pb, pb->safe_vars);
3680
3681         n_vars = pb->num_vars;
3682
3683         if (n_vars == 1)
3684           continue;
3685       }
3686
3687     switch (normalize_omega_problem (pb))
3688       {
3689       case normalize_false:
3690         return omega_false;
3691         break;
3692
3693       case normalize_coupled:
3694         coupled_subscripts = true;
3695         break;
3696
3697       case normalize_uncoupled:
3698         coupled_subscripts = false;
3699         break;
3700
3701       default:
3702         gcc_unreachable ();
3703       }
3704
3705     n_vars = pb->num_vars;
3706
3707     if (dump_file && (dump_flags & TDF_DETAILS))
3708       {
3709         fprintf (dump_file, "\nafter normalization:\n");
3710         omega_print_problem (dump_file, pb);
3711         fprintf (dump_file, "\n");
3712         fprintf (dump_file, "eliminating variable using Fourier-Motzkin.\n");
3713       }
3714
3715     do {
3716       int parallel_difference = INT_MAX;
3717       int best_parallel_eqn = -1;
3718       int minC, maxC, minCj = 0;
3719       int lower_bound_count = 0;
3720       int e2, Le = 0, Ue;
3721       bool possible_easy_int_solution;
3722       int max_splinters = 1;
3723       bool exact = false;
3724       bool lucky_exact = false;
3725       int neweqns = 0;
3726       int best = (INT_MAX);
3727       int j = 0, jLe = 0, jLowerBoundCount = 0;
3728
3729
3730       eliminate_again = false;
3731
3732       if (pb->num_eqs > 0)
3733         return omega_solve_problem (pb, desired_res);
3734
3735       if (!coupled_subscripts)
3736         {
3737           if (pb->safe_vars == 0)
3738             pb->num_geqs = 0;
3739           else
3740             for (e = pb->num_geqs - 1; e >= 0; e--)
3741               if (!omega_safe_var_p (pb, abs (pb->geqs[e].key)))
3742                 omega_delete_geq (pb, e, n_vars);
3743
3744           pb->num_vars = pb->safe_vars;
3745
3746           if (desired_res == omega_simplify)
3747             {
3748               omega_problem_reduced (pb);
3749               return omega_false;
3750             }
3751
3752           return omega_true;
3753         }
3754
3755       if (desired_res != omega_simplify)
3756         fv = 0;
3757       else
3758         fv = pb->safe_vars;
3759
3760       if (pb->num_geqs == 0)
3761         {
3762           if (desired_res == omega_simplify)
3763             {
3764               pb->num_vars = pb->safe_vars;
3765               omega_problem_reduced (pb);
3766               return omega_false;
3767             }
3768           return omega_true;
3769         }
3770
3771       if (desired_res == omega_simplify && n_vars == pb->safe_vars)
3772         {
3773           omega_problem_reduced (pb);
3774           return omega_false;
3775         }
3776
3777       if (pb->num_geqs > OMEGA_MAX_GEQS - 30
3778           || pb->num_geqs > 2 * n_vars * n_vars + 4 * n_vars + 10)
3779         {
3780           if (dump_file && (dump_flags & TDF_DETAILS))
3781             fprintf (dump_file,
3782                      "TOO MANY EQUATIONS; "
3783                      "%d equations, %d variables, "
3784                      "ELIMINATING REDUNDANT ONES\n",
3785                      pb->num_geqs, n_vars);
3786
3787           if (!omega_eliminate_redundant (pb, false))
3788             return omega_false;
3789
3790           n_vars = pb->num_vars;
3791
3792           if (pb->num_eqs > 0)
3793             return omega_solve_problem (pb, desired_res);
3794
3795           if (dump_file && (dump_flags & TDF_DETAILS))
3796             fprintf (dump_file, "END ELIMINATION OF REDUNDANT EQUATIONS\n");
3797         }
3798
3799       if (desired_res != omega_simplify)
3800         fv = 0;
3801       else
3802         fv = pb->safe_vars;
3803
3804       for (i = n_vars; i != fv; i--)
3805         {
3806           int score;
3807           int ub = -2;
3808           int lb = -2;
3809           bool lucky = false;
3810           int upper_bound_count = 0;
3811
3812           lower_bound_count = 0;
3813           minC = maxC = 0;
3814
3815           for (e = pb->num_geqs - 1; e >= 0; e--)
3816             if (pb->geqs[e].coef[i] < 0)
3817               {
3818                 minC = MIN (minC, pb->geqs[e].coef[i]);
3819                 upper_bound_count++;
3820                 if (pb->geqs[e].coef[i] < -1)
3821                   {
3822                     if (ub == -2)
3823                       ub = e;
3824                     else
3825                       ub = -1;
3826                   }
3827               }
3828             else if (pb->geqs[e].coef[i] > 0)
3829               {
3830                 maxC = MAX (maxC, pb->geqs[e].coef[i]);
3831                 lower_bound_count++;
3832                 Le = e;
3833                 if (pb->geqs[e].coef[i] > 1)
3834                   {
3835                     if (lb == -2)
3836                       lb = e;
3837                     else
3838                       lb = -1;
3839                   }
3840               }
3841
3842           if (lower_bound_count == 0
3843               || upper_bound_count == 0)
3844             {
3845               lower_bound_count = 0;
3846               break;
3847             }
3848
3849           if (ub >= 0 && lb >= 0
3850               && pb->geqs[lb].key == -pb->geqs[ub].key)
3851             {
3852               int Lc = pb->geqs[lb].coef[i];
3853               int Uc = -pb->geqs[ub].coef[i];
3854               int diff =
3855                 Lc * pb->geqs[ub].coef[0] + Uc * pb->geqs[lb].coef[0];
3856               lucky = (diff >= (Uc - 1) * (Lc - 1));
3857             }
3858
3859           if (maxC == 1
3860               || minC == -1
3861               || lucky
3862               || in_approximate_mode)
3863             {
3864               neweqns = score = upper_bound_count * lower_bound_count;
3865
3866               if (dump_file && (dump_flags & TDF_DETAILS))
3867                 fprintf (dump_file,
3868                          "For %s, exact, score = %d*%d, range = %d ... %d,"
3869                          "\nlucky = %d, in_approximate_mode=%d \n",
3870                          omega_variable_to_str (pb, i),
3871                          upper_bound_count,
3872                          lower_bound_count, minC, maxC, lucky,
3873                          in_approximate_mode);
3874
3875               if (!exact
3876                   || score < best)
3877                 {
3878
3879                   best = score;
3880                   j = i;
3881                   minCj = minC;
3882                   jLe = Le;
3883                   jLowerBoundCount = lower_bound_count;
3884                   exact = true;
3885                   lucky_exact = lucky;
3886                   if (score == 1)
3887                     break;
3888                 }
3889             }
3890           else if (!exact)
3891             {
3892               if (dump_file && (dump_flags & TDF_DETAILS))
3893                 fprintf (dump_file,
3894                          "For %s, non-exact, score = %d*%d,"
3895                          "range = %d ... %d \n",
3896                          omega_variable_to_str (pb, i),
3897                          upper_bound_count,
3898                          lower_bound_count, minC, maxC);
3899
3900               neweqns = upper_bound_count * lower_bound_count;
3901               score = maxC - minC;
3902
3903               if (best > score)
3904                 {
3905                   best = score;
3906                   j = i;
3907                   minCj = minC;
3908                   jLe = Le;
3909                   jLowerBoundCount = lower_bound_count;
3910                 }
3911             }
3912         }
3913
3914       if (lower_bound_count == 0)
3915         {
3916           omega_free_eliminations (pb, pb->safe_vars);
3917           n_vars = pb->num_vars;
3918           eliminate_again = true;
3919           continue;
3920         }
3921
3922       i = j;
3923       minC = minCj;
3924       Le = jLe;
3925       lower_bound_count = jLowerBoundCount;
3926
3927       for (e = pb->num_geqs - 1; e >= 0; e--)
3928         if (pb->geqs[e].coef[i] > 0)
3929           {
3930             if (pb->geqs[e].coef[i] == -minC)
3931               max_splinters += -minC - 1;
3932             else
3933               max_splinters +=
3934                 check_pos_mul ((pb->geqs[e].coef[i] - 1),
3935                                (-minC - 1)) / (-minC) + 1;
3936           }
3937
3938       /* #ifdef Omega3 */
3939       /* Trying to produce exact elimination by finding redundant
3940          constraints.  */
3941       if (!exact && !tried_eliminating_redundant)
3942         {
3943           omega_eliminate_redundant (pb, false);
3944           tried_eliminating_redundant = true;
3945           eliminate_again = true;
3946           continue;
3947         }
3948       tried_eliminating_redundant = false;
3949       /* #endif */
3950
3951       if (return_single_result && desired_res == omega_simplify && !exact)
3952         {
3953           omega_problem_reduced (pb);
3954           return omega_true;
3955         }
3956
3957       /* #ifndef Omega3 */
3958       /* Trying to produce exact elimination by finding redundant
3959          constraints.  */
3960       if (!exact && !tried_eliminating_redundant)
3961         {
3962           omega_eliminate_redundant (pb, false);
3963           tried_eliminating_redundant = true;
3964           continue;
3965         }
3966       tried_eliminating_redundant = false;
3967       /* #endif */
3968
3969       if (!exact)
3970         {
3971           int e1, e2;
3972
3973           for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
3974             if (pb->geqs[e1].color == omega_black)
3975               for (e2 = e1 - 1; e2 >= 0; e2--)
3976                 if (pb->geqs[e2].color == omega_black
3977                     && pb->geqs[e1].key == -pb->geqs[e2].key
3978                     && ((pb->geqs[e1].coef[0] + pb->geqs[e2].coef[0])
3979                         * (3 - single_var_geq (&pb->geqs[e1], pb->num_vars))
3980                         / 2 < parallel_difference))
3981                   {
3982                     parallel_difference =
3983                       (pb->geqs[e1].coef[0] + pb->geqs[e2].coef[0])
3984                       * (3 - single_var_geq (&pb->geqs[e1], pb->num_vars))
3985                       / 2;
3986                     best_parallel_eqn = e1;
3987                   }
3988
3989           if (dump_file && (dump_flags & TDF_DETAILS)
3990               && best_parallel_eqn >= 0)
3991             {
3992               fprintf (dump_file,
3993                        "Possible parallel projection, diff = %d, in ",
3994                        parallel_difference);
3995               omega_print_geq (dump_file, pb, &(pb->geqs[best_parallel_eqn]));
3996               fprintf (dump_file, "\n");
3997               omega_print_problem (dump_file, pb);
3998             }
3999         }
4000
4001       if (dump_file && (dump_flags & TDF_DETAILS))
4002         {
4003           fprintf (dump_file, "going to eliminate %s, (%d,%d,%d)\n",
4004                    omega_variable_to_str (pb, i), i, minC,
4005                    lower_bound_count);
4006           omega_print_problem (dump_file, pb);
4007
4008           if (lucky_exact)
4009             fprintf (dump_file, "(a lucky exact elimination)\n");
4010
4011           else if (exact)
4012             fprintf (dump_file, "(an exact elimination)\n");
4013
4014           fprintf (dump_file, "Max # of splinters = %d\n", max_splinters);
4015         }
4016
4017       gcc_assert (max_splinters >= 1);
4018
4019       if (!exact && desired_res == omega_simplify && best_parallel_eqn >= 0
4020           && parallel_difference <= max_splinters)
4021         return parallel_splinter (pb, best_parallel_eqn, parallel_difference,
4022                                   desired_res);
4023
4024       smoothed = false;
4025
4026       if (i != n_vars)
4027         {
4028           int t;
4029           int j = pb->num_vars;
4030
4031           if (dump_file && (dump_flags & TDF_DETAILS))
4032             {
4033               fprintf (dump_file, "Swapping %d and %d\n", i, j);
4034               omega_print_problem (dump_file, pb);
4035             }
4036
4037           swap (&pb->var[i], &pb->var[j]);
4038
4039           for (e = pb->num_geqs - 1; e >= 0; e--)
4040             if (pb->geqs[e].coef[i] != pb->geqs[e].coef[j])
4041               {
4042                 pb->geqs[e].touched = 1;
4043                 t = pb->geqs[e].coef[i];
4044                 pb->geqs[e].coef[i] = pb->geqs[e].coef[j];
4045                 pb->geqs[e].coef[j] = t;
4046               }
4047
4048           for (e = pb->num_subs - 1; e >= 0; e--)
4049             if (pb->subs[e].coef[i] != pb->subs[e].coef[j])
4050               {
4051                 t = pb->subs[e].coef[i];
4052                 pb->subs[e].coef[i] = pb->subs[e].coef[j];
4053                 pb->subs[e].coef[j] = t;
4054               }
4055
4056           if (dump_file && (dump_flags & TDF_DETAILS))
4057             {
4058               fprintf (dump_file, "Swapping complete \n");
4059               omega_print_problem (dump_file, pb);
4060               fprintf (dump_file, "\n");
4061             }
4062
4063           i = j;
4064         }
4065
4066       else if (dump_file && (dump_flags & TDF_DETAILS))
4067         {
4068           fprintf (dump_file, "No swap needed\n");
4069           omega_print_problem (dump_file, pb);
4070         }
4071
4072       pb->num_vars--;
4073       n_vars = pb->num_vars;
4074
4075       if (exact)
4076         {
4077           if (n_vars == 1)
4078             {
4079               int upper_bound = pos_infinity;
4080               int lower_bound = neg_infinity;
4081               enum omega_eqn_color ub_color = omega_black;
4082               enum omega_eqn_color lb_color = omega_black;
4083               int topeqn = pb->num_geqs - 1;
4084               int Lc = pb->geqs[Le].coef[i];
4085
4086               for (Le = topeqn; Le >= 0; Le--)
4087                 if ((Lc = pb->geqs[Le].coef[i]) == 0)
4088                   {
4089                     if (pb->geqs[Le].coef[1] == 1)
4090                       {
4091                         int constantTerm = -pb->geqs[Le].coef[0];
4092
4093                         if (constantTerm > lower_bound ||
4094                             (constantTerm == lower_bound &&
4095                              !omega_eqn_is_red (&pb->geqs[Le], desired_res)))
4096                           {
4097                             lower_bound = constantTerm;
4098                             lb_color = pb->geqs[Le].color;
4099                           }
4100
4101                         if (dump_file && (dump_flags & TDF_DETAILS))
4102                           {
4103                             if (pb->geqs[Le].color == omega_black)
4104                               fprintf (dump_file, " :::=> %s >= %d\n",
4105                                        omega_variable_to_str (pb, 1),
4106                                        constantTerm);
4107                             else
4108                               fprintf (dump_file,
4109                                        " :::=> [%s >= %d]\n",
4110                                        omega_variable_to_str (pb, 1),
4111                                        constantTerm);
4112                           }
4113                       }
4114                     else
4115                       {
4116                         int constantTerm = pb->geqs[Le].coef[0];
4117                         if (constantTerm < upper_bound ||
4118                             (constantTerm == upper_bound
4119                              && !omega_eqn_is_red (&pb->geqs[Le],
4120                                                    desired_res)))
4121                           {
4122                             upper_bound = constantTerm;
4123                             ub_color = pb->geqs[Le].color;
4124                           }
4125
4126                         if (dump_file && (dump_flags & TDF_DETAILS))
4127                           {
4128                             if (pb->geqs[Le].color == omega_black)
4129                               fprintf (dump_file, " :::=> %s <= %d\n",
4130                                        omega_variable_to_str (pb, 1),
4131                                        constantTerm);
4132                             else
4133                               fprintf (dump_file,
4134                                        " :::=> [%s <= %d]\n",
4135                                        omega_variable_to_str (pb, 1),
4136                                        constantTerm);
4137                           }
4138                       }
4139                   }
4140                 else if (Lc > 0)
4141                   for (Ue = topeqn; Ue >= 0; Ue--)
4142                     if (pb->geqs[Ue].coef[i] < 0
4143                         && pb->geqs[Le].key != -pb->geqs[Ue].key)
4144                       {
4145                         int Uc = -pb->geqs[Ue].coef[i];
4146                         int coefficient = pb->geqs[Ue].coef[1] * Lc
4147                           + pb->geqs[Le].coef[1] * Uc;
4148                         int constantTerm = pb->geqs[Ue].coef[0] * Lc
4149                           + pb->geqs[Le].coef[0] * Uc;
4150
4151                         if (dump_file && (dump_flags & TDF_DETAILS))
4152                           {
4153                             omega_print_geq_extra (dump_file, pb,
4154                                                    &(pb->geqs[Ue]));
4155                             fprintf (dump_file, "\n");
4156                             omega_print_geq_extra (dump_file, pb,
4157                                                    &(pb->geqs[Le]));
4158                             fprintf (dump_file, "\n");
4159                           }
4160
4161                         if (coefficient > 0)
4162                           {
4163                             constantTerm = -int_div (constantTerm, coefficient);
4164
4165                             if (constantTerm > lower_bound
4166                                 || (constantTerm == lower_bound
4167                                     && (desired_res != omega_simplify
4168                                         || (pb->geqs[Ue].color == omega_black
4169                                             && pb->geqs[Le].color == omega_black))))
4170                               {
4171                                 lower_bound = constantTerm;
4172                                 lb_color = (pb->geqs[Ue].color == omega_red
4173                                             || pb->geqs[Le].color == omega_red)
4174                                   ? omega_red : omega_black;
4175                               }
4176
4177                             if (dump_file && (dump_flags & TDF_DETAILS))
4178                               {
4179                                 if (pb->geqs[Ue].color == omega_red
4180                                     || pb->geqs[Le].color == omega_red)
4181                                   fprintf (dump_file,
4182                                            " ::=> [%s >= %d]\n",
4183                                            omega_variable_to_str (pb, 1),
4184                                            constantTerm);
4185                                 else
4186                                   fprintf (dump_file,
4187                                            " ::=> %s >= %d\n",
4188                                            omega_variable_to_str (pb, 1),
4189                                            constantTerm);
4190                               }
4191                           }
4192                         else
4193                           {
4194                             constantTerm = int_div (constantTerm, -coefficient);
4195                             if (constantTerm < upper_bound
4196                                 || (constantTerm == upper_bound
4197                                     && pb->geqs[Ue].color == omega_black
4198                                     && pb->geqs[Le].color == omega_black))
4199                               {
4200                                 upper_bound = constantTerm;
4201                                 ub_color = (pb->geqs[Ue].color == omega_red
4202                                             || pb->geqs[Le].color == omega_red)
4203                                   ? omega_red : omega_black;
4204                               }
4205
4206                             if (dump_file
4207                                 && (dump_flags & TDF_DETAILS))
4208                               {
4209                                 if (pb->geqs[Ue].color == omega_red
4210                                     || pb->geqs[Le].color == omega_red)
4211                                   fprintf (dump_file,
4212                                            " ::=> [%s <= %d]\n",
4213                                            omega_variable_to_str (pb, 1),
4214                                            constantTerm);
4215                                 else
4216                                   fprintf (dump_file,
4217                                            " ::=> %s <= %d\n",
4218                                            omega_variable_to_str (pb, 1),
4219                                            constantTerm);
4220                               }
4221                           }
4222                       }
4223
4224               pb->num_geqs = 0;
4225
4226               if (dump_file && (dump_flags & TDF_DETAILS))
4227                 fprintf (dump_file,
4228                          " therefore, %c%d <= %c%s%c <= %d%c\n",
4229                          lb_color == omega_red ? '[' : ' ', lower_bound,
4230                          (lb_color == omega_red && ub_color == omega_black)
4231                          ? ']' : ' ',
4232                          omega_variable_to_str (pb, 1),
4233                          (lb_color == omega_black && ub_color == omega_red)
4234                          ? '[' : ' ',
4235                          upper_bound, ub_color == omega_red ? ']' : ' ');
4236
4237               if (lower_bound > upper_bound)
4238                 return omega_false;
4239
4240               if (pb->safe_vars == 1)
4241                 {
4242                   if (upper_bound == lower_bound
4243                       && !(ub_color == omega_red || lb_color == omega_red)
4244                       && !please_no_equalities_in_simplified_problems)
4245                     {
4246                       pb->num_eqs++;
4247                       pb->eqs[0].coef[1] = -1;
4248                       pb->eqs[0].coef[0] = upper_bound;
4249
4250                       if (ub_color == omega_red
4251                           || lb_color == omega_red)
4252                         pb->eqs[0].color = omega_red;
4253
4254                       if (desired_res == omega_simplify
4255                           && pb->eqs[0].color == omega_black)
4256                         return omega_solve_problem (pb, desired_res);
4257                     }
4258
4259                   if (upper_bound != pos_infinity)
4260                     {
4261                       pb->geqs[0].coef[1] = -1;
4262                       pb->geqs[0].coef[0] = upper_bound;
4263                       pb->geqs[0].color = ub_color;
4264                       pb->geqs[0].key = -1;
4265                       pb->geqs[0].touched = 0;
4266                       pb->num_geqs++;
4267                     }
4268
4269                   if (lower_bound != neg_infinity)
4270                     {
4271                       pb->geqs[pb->num_geqs].coef[1] = 1;
4272                       pb->geqs[pb->num_geqs].coef[0] = -lower_bound;
4273                       pb->geqs[pb->num_geqs].color = lb_color;
4274                       pb->geqs[pb->num_geqs].key = 1;
4275                       pb->geqs[pb->num_geqs].touched = 0;
4276                       pb->num_geqs++;
4277                     }
4278                 }
4279
4280               if (desired_res == omega_simplify)
4281                 {
4282                   omega_problem_reduced (pb);
4283                   return omega_false;
4284                 }
4285               else
4286                 {
4287                   if (!conservative
4288                       && (desired_res != omega_simplify
4289                           || (lb_color == omega_black
4290                               && ub_color == omega_black))
4291                       && original_problem != no_problem
4292                       && lower_bound == upper_bound)
4293                     {
4294                       for (i = original_problem->num_vars; i >= 0; i--)
4295                         if (original_problem->var[i] == pb->var[1])
4296                           break;
4297
4298                       if (i == 0)
4299                         break;
4300
4301                       e = original_problem->num_eqs++;
4302                       omega_init_eqn_zero (&original_problem->eqs[e],
4303                                            original_problem->num_vars);
4304                       original_problem->eqs[e].coef[i] = -1;
4305                       original_problem->eqs[e].coef[0] = upper_bound;
4306
4307                       if (dump_file && (dump_flags & TDF_DETAILS))
4308                         {
4309                           fprintf (dump_file,
4310                                    "adding equality %d to outer problem\n", e);
4311                           omega_print_problem (dump_file, original_problem);
4312                         }
4313                     }
4314                   return omega_true;
4315                 }
4316             }
4317
4318           eliminate_again = true;
4319
4320           if (lower_bound_count == 1)
4321             {
4322               eqn lbeqn = omega_alloc_eqns (0, 1);
4323               int Lc = pb->geqs[Le].coef[i];
4324
4325               if (dump_file && (dump_flags & TDF_DETAILS))
4326                 fprintf (dump_file, "an inplace elimination\n");
4327
4328               omega_copy_eqn (lbeqn, &pb->geqs[Le], (n_vars + 1));
4329               omega_delete_geq_extra (pb, Le, n_vars + 1);
4330
4331               for (Ue = pb->num_geqs - 1; Ue >= 0; Ue--)
4332                 if (pb->geqs[Ue].coef[i] < 0)
4333                   {
4334                     if (lbeqn->key == -pb->geqs[Ue].key)
4335                       omega_delete_geq_extra (pb, Ue, n_vars + 1);
4336                     else
4337                       {
4338                         int k;
4339                         int Uc = -pb->geqs[Ue].coef[i];
4340                         pb->geqs[Ue].touched = 1;
4341                         eliminate_again = false;
4342
4343                         if (lbeqn->color == omega_red)
4344                           pb->geqs[Ue].color = omega_red;
4345
4346                         for (k = 0; k <= n_vars; k++)
4347                           pb->geqs[Ue].coef[k] =
4348                             check_mul (pb->geqs[Ue].coef[k], Lc) +
4349                             check_mul (lbeqn->coef[k], Uc);
4350
4351                         if (dump_file && (dump_flags & TDF_DETAILS))
4352                           {
4353                             omega_print_geq (dump_file, pb,
4354                                              &(pb->geqs[Ue]));
4355                             fprintf (dump_file, "\n");
4356                           }
4357                       }
4358                   }
4359
4360               omega_free_eqns (lbeqn, 1);
4361               continue;
4362             }
4363           else
4364             {
4365               int *dead_eqns = XNEWVEC (int, OMEGA_MAX_GEQS);
4366               bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
4367               int num_dead = 0;
4368               int top_eqn = pb->num_geqs - 1;
4369               lower_bound_count--;
4370
4371               if (dump_file && (dump_flags & TDF_DETAILS))
4372                 fprintf (dump_file, "lower bound count = %d\n",
4373                          lower_bound_count);
4374
4375               for (Le = top_eqn; Le >= 0; Le--)
4376                 if (pb->geqs[Le].coef[i] > 0)
4377                   {
4378                     int Lc = pb->geqs[Le].coef[i];
4379                     for (Ue = top_eqn; Ue >= 0; Ue--)
4380                       if (pb->geqs[Ue].coef[i] < 0)
4381                         {
4382                           if (pb->geqs[Le].key != -pb->geqs[Ue].key)
4383                             {
4384                               int k;
4385                               int Uc = -pb->geqs[Ue].coef[i];
4386
4387                               if (num_dead == 0)
4388                                 e2 = pb->num_geqs++;
4389                               else
4390                                 e2 = dead_eqns[--num_dead];
4391
4392                               gcc_assert (e2 < OMEGA_MAX_GEQS);
4393
4394                               if (dump_file && (dump_flags & TDF_DETAILS))
4395                                 {
4396                                   fprintf (dump_file,
4397                                            "Le = %d, Ue = %d, gen = %d\n",
4398                                            Le, Ue, e2);
4399                                   omega_print_geq_extra (dump_file, pb,
4400                                                          &(pb->geqs[Le]));
4401                                   fprintf (dump_file, "\n");
4402                                   omega_print_geq_extra (dump_file, pb,
4403                                                          &(pb->geqs[Ue]));
4404                                   fprintf (dump_file, "\n");
4405                                 }
4406
4407                               eliminate_again = false;
4408
4409                               for (k = n_vars; k >= 0; k--)
4410                                 pb->geqs[e2].coef[k] =
4411                                   check_mul (pb->geqs[Ue].coef[k], Lc) +
4412                                   check_mul (pb->geqs[Le].coef[k], Uc);
4413
4414                               pb->geqs[e2].coef[n_vars + 1] = 0;
4415                               pb->geqs[e2].touched = 1;
4416
4417                               if (pb->geqs[Ue].color == omega_red
4418                                   || pb->geqs[Le].color == omega_red)
4419                                 pb->geqs[e2].color = omega_red;
4420                               else
4421                                 pb->geqs[e2].color = omega_black;
4422
4423                               if (dump_file && (dump_flags & TDF_DETAILS))
4424                                 {
4425                                   omega_print_geq (dump_file, pb,
4426                                                    &(pb->geqs[e2]));
4427                                   fprintf (dump_file, "\n");
4428                                 }
4429                             }
4430
4431                           if (lower_bound_count == 0)
4432                             {
4433                               dead_eqns[num_dead++] = Ue;
4434
4435                               if (dump_file && (dump_flags & TDF_DETAILS))
4436                                 fprintf (dump_file, "Killed %d\n", Ue);
4437                             }
4438                         }
4439
4440                     lower_bound_count--;
4441                     dead_eqns[num_dead++] = Le;
4442
4443                     if (dump_file && (dump_flags & TDF_DETAILS))
4444                       fprintf (dump_file, "Killed %d\n", Le);
4445                   }
4446
4447               for (e = pb->num_geqs - 1; e >= 0; e--)
4448                 is_dead[e] = false;
4449
4450               while (num_dead > 0)
4451                 is_dead[dead_eqns[--num_dead]] = true;
4452
4453               for (e = pb->num_geqs - 1; e >= 0; e--)
4454                 if (is_dead[e])
4455                   omega_delete_geq_extra (pb, e, n_vars + 1);
4456
4457               free (dead_eqns);
4458               free (is_dead);
4459               continue;
4460             }
4461         }
4462       else
4463         {
4464           omega_pb rS, iS;
4465
4466           rS = omega_alloc_problem (0, 0);
4467           iS = omega_alloc_problem (0, 0);
4468           e2 = 0;
4469           possible_easy_int_solution = true;
4470
4471           for (e = 0; e < pb->num_geqs; e++)
4472             if (pb->geqs[e].coef[i] == 0)
4473               {
4474                 omega_copy_eqn (&(rS->geqs[e2]), &pb->geqs[e],
4475                                 pb->num_vars);
4476                 omega_copy_eqn (&(iS->geqs[e2]), &pb->geqs[e],
4477                                 pb->num_vars);
4478
4479                 if (dump_file && (dump_flags & TDF_DETAILS))
4480                   {
4481                     int t;
4482                     fprintf (dump_file, "Copying (%d, %d): ", i,
4483                              pb->geqs[e].coef[i]);
4484                     omega_print_geq_extra (dump_file, pb, &pb->geqs[e]);
4485                     fprintf (dump_file, "\n");
4486                     for (t = 0; t <= n_vars + 1; t++)
4487                       fprintf (dump_file, "%d ", pb->geqs[e].coef[t]);
4488                     fprintf (dump_file, "\n");
4489
4490                   }
4491                 e2++;
4492                 gcc_assert (e2 < OMEGA_MAX_GEQS);
4493               }
4494
4495           for (Le = pb->num_geqs - 1; Le >= 0; Le--)
4496             if (pb->geqs[Le].coef[i] > 0)
4497               for (Ue = pb->num_geqs - 1; Ue >= 0; Ue--)
4498                 if (pb->geqs[Ue].coef[i] < 0)
4499                   {
4500                     int k;
4501                     int Lc = pb->geqs[Le].coef[i];
4502                     int Uc = -pb->geqs[Ue].coef[i];
4503
4504                     if (pb->geqs[Le].key != -pb->geqs[Ue].key)
4505                       {
4506
4507                         rS->geqs[e2].touched = iS->geqs[e2].touched = 1;
4508
4509                         if (dump_file && (dump_flags & TDF_DETAILS))
4510                           {
4511                             fprintf (dump_file, "---\n");
4512                             fprintf (dump_file,
4513                                      "Le(Lc) = %d(%d_, Ue(Uc) = %d(%d), gen = %d\n",
4514                                      Le, Lc, Ue, Uc, e2);
4515                             omega_print_geq_extra (dump_file, pb, &pb->geqs[Le]);
4516                             fprintf (dump_file, "\n");
4517                             omega_print_geq_extra (dump_file, pb, &pb->geqs[Ue]);
4518                             fprintf (dump_file, "\n");
4519                           }
4520
4521                         if (Uc == Lc)
4522                           {
4523                             for (k = n_vars; k >= 0; k--)
4524                               iS->geqs[e2].coef[k] = rS->geqs[e2].coef[k] =
4525                                 pb->geqs[Ue].coef[k] + pb->geqs[Le].coef[k];
4526
4527                             iS->geqs[e2].coef[0] -= (Uc - 1);
4528                           }
4529                         else
4530                           {
4531                             for (k = n_vars; k >= 0; k--)
4532                               iS->geqs[e2].coef[k] = rS->geqs[e2].coef[k] =
4533                                 check_mul (pb->geqs[Ue].coef[k], Lc) +
4534                                 check_mul (pb->geqs[Le].coef[k], Uc);
4535
4536                             iS->geqs[e2].coef[0] -= (Uc - 1) * (Lc - 1);
4537                           }
4538
4539                         if (pb->geqs[Ue].color == omega_red
4540                             || pb->geqs[Le].color == omega_red)
4541                           iS->geqs[e2].color = rS->geqs[e2].color = omega_red;
4542                         else
4543                           iS->geqs[e2].color = rS->geqs[e2].color = omega_black;
4544
4545                         if (dump_file && (dump_flags & TDF_DETAILS))
4546                           {
4547                             omega_print_geq (dump_file, pb, &(rS->geqs[e2]));
4548                             fprintf (dump_file, "\n");
4549                           }
4550
4551                         e2++;
4552                         gcc_assert (e2 < OMEGA_MAX_GEQS);
4553                       }
4554                     else if (pb->geqs[Ue].coef[0] * Lc +
4555                              pb->geqs[Le].coef[0] * Uc -
4556                              (Uc - 1) * (Lc - 1) < 0)
4557                       possible_easy_int_solution = false;
4558                   }
4559
4560           iS->variables_initialized = rS->variables_initialized = true;
4561           iS->num_vars = rS->num_vars = pb->num_vars;
4562           iS->num_geqs = rS->num_geqs = e2;
4563           iS->num_eqs = rS->num_eqs = 0;
4564           iS->num_subs = rS->num_subs = pb->num_subs;
4565           iS->safe_vars = rS->safe_vars = pb->safe_vars;
4566
4567           for (e = n_vars; e >= 0; e--)
4568             rS->var[e] = pb->var[e];
4569
4570           for (e = n_vars; e >= 0; e--)
4571             iS->var[e] = pb->var[e];
4572
4573           for (e = pb->num_subs - 1; e >= 0; e--)
4574             {
4575               omega_copy_eqn (&(rS->subs[e]), &(pb->subs[e]), pb->num_vars);
4576               omega_copy_eqn (&(iS->subs[e]), &(pb->subs[e]), pb->num_vars);
4577             }
4578
4579           pb->num_vars++;
4580           n_vars = pb->num_vars;
4581
4582           if (desired_res != omega_true)
4583             {
4584               if (original_problem == no_problem)
4585                 {
4586                   original_problem = pb;
4587                   result = omega_solve_geq (rS, omega_false);
4588                   original_problem = no_problem;
4589                 }
4590               else
4591                 result = omega_solve_geq (rS, omega_false);
4592
4593               if (result == omega_false)
4594                 {
4595                   free (rS);
4596                   free (iS);
4597                   return result;
4598                 }
4599
4600               if (pb->num_eqs > 0)
4601                 {
4602                   /* An equality constraint must have been found */
4603                   free (rS);
4604                   free (iS);
4605                   return omega_solve_problem (pb, desired_res);
4606                 }
4607             }
4608
4609           if (desired_res != omega_false)
4610             {
4611               int j;
4612               int lower_bounds = 0;
4613               int *lower_bound = XNEWVEC (int, OMEGA_MAX_GEQS);
4614
4615               if (possible_easy_int_solution)
4616                 {
4617                   conservative++;
4618                   result = omega_solve_geq (iS, desired_res);
4619                   conservative--;
4620
4621                   if (result != omega_false)
4622                     {
4623                       free (rS);
4624                       free (iS);
4625                       free (lower_bound);
4626                       return result;
4627                     }
4628                 }
4629
4630               if (!exact && best_parallel_eqn >= 0
4631                   && parallel_difference <= max_splinters)
4632                 {
4633                   free (rS);
4634                   free (iS);
4635                   free (lower_bound);
4636                   return parallel_splinter (pb, best_parallel_eqn,
4637                                             parallel_difference,
4638                                             desired_res);
4639                 }
4640
4641               if (dump_file && (dump_flags & TDF_DETAILS))
4642                 fprintf (dump_file, "have to do exact analysis\n");
4643
4644               conservative++;
4645
4646               for (e = 0; e < pb->num_geqs; e++)
4647                 if (pb->geqs[e].coef[i] > 1)
4648                   lower_bound[lower_bounds++] = e;
4649
4650               /* Sort array LOWER_BOUND.  */
4651               for (j = 0; j < lower_bounds; j++)
4652                 {
4653                   int k, smallest = j;
4654
4655                   for (k = j + 1; k < lower_bounds; k++)
4656                     if (pb->geqs[lower_bound[smallest]].coef[i] >
4657                         pb->geqs[lower_bound[k]].coef[i])
4658                       smallest = k;
4659
4660                   k = lower_bound[smallest];
4661                   lower_bound[smallest] = lower_bound[j];
4662                   lower_bound[j] = k;
4663                 }
4664
4665               if (dump_file && (dump_flags & TDF_DETAILS))
4666                 {
4667                   fprintf (dump_file, "lower bound coefficients = ");
4668
4669                   for (j = 0; j < lower_bounds; j++)
4670                     fprintf (dump_file, " %d",
4671                              pb->geqs[lower_bound[j]].coef[i]);
4672
4673                   fprintf (dump_file, "\n");
4674                 }
4675
4676               for (j = 0; j < lower_bounds; j++)
4677                 {
4678                   int max_incr;
4679                   int c;
4680                   int worst_lower_bound_constant = -minC;
4681
4682                   e = lower_bound[j];
4683                   max_incr = (((pb->geqs[e].coef[i] - 1) *
4684                                (worst_lower_bound_constant - 1) - 1)
4685                               / worst_lower_bound_constant);
4686                   /* max_incr += 2; */
4687
4688                   if (dump_file && (dump_flags & TDF_DETAILS))
4689                     {
4690                       fprintf (dump_file, "for equation ");
4691                       omega_print_geq (dump_file, pb, &pb->geqs[e]);
4692                       fprintf (dump_file,
4693                                "\ntry decrements from 0 to %d\n",
4694                                max_incr);
4695                       omega_print_problem (dump_file, pb);
4696                     }
4697
4698                   if (max_incr > 50 && !smoothed
4699                       && smooth_weird_equations (pb))
4700                     {
4701                       conservative--;
4702                       free (rS);
4703                       free (iS);
4704                       smoothed = true;
4705                       goto solve_geq_start;
4706                     }
4707
4708                   omega_copy_eqn (&pb->eqs[0], &pb->geqs[e],
4709                                   pb->num_vars);
4710                   pb->eqs[0].color = omega_black;
4711                   omega_init_eqn_zero (&pb->geqs[e], pb->num_vars);
4712                   pb->geqs[e].touched = 1;
4713                   pb->num_eqs = 1;
4714
4715                   for (c = max_incr; c >= 0; c--)
4716                     {
4717                       if (dump_file && (dump_flags & TDF_DETAILS))
4718                         {
4719                           fprintf (dump_file,
4720                                    "trying next decrement of %d\n",
4721                                    max_incr - c);
4722                           omega_print_problem (dump_file, pb);
4723                         }
4724
4725                       omega_copy_problem (rS, pb);
4726
4727                       if (dump_file && (dump_flags & TDF_DETAILS))
4728                         omega_print_problem (dump_file, rS);
4729
4730                       result = omega_solve_problem (rS, desired_res);
4731
4732                       if (result == omega_true)
4733                         {
4734                           free (rS);
4735                           free (iS);
4736                           free (lower_bound);
4737                           conservative--;
4738                           return omega_true;
4739                         }
4740
4741                       pb->eqs[0].coef[0]--;
4742                     }
4743
4744                   if (j + 1 < lower_bounds)
4745                     {
4746                       pb->num_eqs = 0;
4747                       omega_copy_eqn (&pb->geqs[e], &pb->eqs[0],
4748                                       pb->num_vars);
4749                       pb->geqs[e].touched = 1;
4750                       pb->geqs[e].color = omega_black;
4751                       omega_copy_problem (rS, pb);
4752
4753                       if (dump_file && (dump_flags & TDF_DETAILS))
4754                         fprintf (dump_file,
4755                                  "exhausted lower bound, "
4756                                  "checking if still feasible ");
4757
4758                       result = omega_solve_problem (rS, omega_false);
4759
4760                       if (result == omega_false)
4761                         break;
4762                     }
4763                 }
4764
4765               if (dump_file && (dump_flags & TDF_DETAILS))
4766                 fprintf (dump_file, "fall-off the end\n");
4767
4768               free (rS);
4769               free (iS);
4770               free (lower_bound);
4771               conservative--;
4772               return omega_false;
4773             }
4774
4775           free (rS);
4776           free (iS);
4777         }
4778       return omega_unknown;
4779     } while (eliminate_again);
4780   } while (1);
4781 }
4782
4783 /* Because the omega solver is recursive, this counter limits the
4784    recursion depth.  */
4785 static int omega_solve_depth = 0;
4786
4787 /* Return omega_true when the problem PB has a solution following the
4788    DESIRED_RES.  */
4789
4790 enum omega_result
4791 omega_solve_problem (omega_pb pb, enum omega_result desired_res)
4792 {
4793   enum omega_result result;
4794
4795   gcc_assert (pb->num_vars >= pb->safe_vars);
4796   omega_solve_depth++;
4797
4798   if (desired_res != omega_simplify)
4799     pb->safe_vars = 0;
4800
4801   if (omega_solve_depth > 50)
4802     {
4803       if (dump_file && (dump_flags & TDF_DETAILS))
4804         {
4805           fprintf (dump_file,
4806                    "Solve depth = %d, in_approximate_mode = %d, aborting\n",
4807                    omega_solve_depth, in_approximate_mode);
4808           omega_print_problem (dump_file, pb);
4809         }
4810       gcc_assert (0);
4811     }
4812
4813   if (omega_solve_eq (pb, desired_res) == omega_false)
4814     {
4815       omega_solve_depth--;
4816       return omega_false;
4817     }
4818
4819   if (in_approximate_mode && !pb->num_geqs)
4820     {
4821       result = omega_true;
4822       pb->num_vars = pb->safe_vars;
4823       omega_problem_reduced (pb);
4824     }
4825   else
4826     result = omega_solve_geq (pb, desired_res);
4827
4828   omega_solve_depth--;
4829
4830   if (!omega_reduce_with_subs)
4831     {
4832       resurrect_subs (pb);
4833       gcc_assert (please_no_equalities_in_simplified_problems
4834                   || !result || pb->num_subs == 0);
4835     }
4836
4837   return result;
4838 }
4839
4840 /* Return true if red equations constrain the set of possible solutions.
4841    We assume that there are solutions to the black equations by
4842    themselves, so if there is no solution to the combined problem, we
4843    return true.  */
4844
4845 bool
4846 omega_problem_has_red_equations (omega_pb pb)
4847 {
4848   bool result;
4849   int e;
4850   int i;
4851
4852   if (dump_file && (dump_flags & TDF_DETAILS))
4853     {
4854       fprintf (dump_file, "Checking for red equations:\n");
4855       omega_print_problem (dump_file, pb);
4856     }
4857
4858   please_no_equalities_in_simplified_problems++;
4859   may_be_red++;
4860
4861   if (omega_single_result)
4862     return_single_result++;
4863
4864   create_color = true;
4865   result = (omega_simplify_problem (pb) == omega_false);
4866
4867   if (omega_single_result)
4868     return_single_result--;
4869
4870   may_be_red--;
4871   please_no_equalities_in_simplified_problems--;
4872
4873   if (result)
4874     {
4875       if (dump_file && (dump_flags & TDF_DETAILS))
4876         fprintf (dump_file, "Gist is FALSE\n");
4877
4878       pb->num_subs = 0;
4879       pb->num_geqs = 0;
4880       pb->num_eqs = 1;
4881       pb->eqs[0].color = omega_red;
4882
4883       for (i = pb->num_vars; i > 0; i--)
4884         pb->eqs[0].coef[i] = 0;
4885
4886       pb->eqs[0].coef[0] = 1;
4887       return true;
4888     }
4889
4890   free_red_eliminations (pb);
4891   gcc_assert (pb->num_eqs == 0);
4892
4893   for (e = pb->num_geqs - 1; e >= 0; e--)
4894     if (pb->geqs[e].color == omega_red)
4895       result = true;
4896
4897   if (!result)
4898     return false;
4899
4900   for (i = pb->safe_vars; i >= 1; i--)
4901     {
4902       int ub = 0;
4903       int lb = 0;
4904
4905       for (e = pb->num_geqs - 1; e >= 0; e--)
4906         {
4907           if (pb->geqs[e].coef[i])
4908             {
4909               if (pb->geqs[e].coef[i] > 0)
4910                 lb |= (1 + (pb->geqs[e].color == omega_red ? 1 : 0));
4911
4912               else
4913                 ub |= (1 + (pb->geqs[e].color == omega_red ? 1 : 0));
4914             }
4915         }
4916
4917       if (ub == 2 || lb == 2)
4918         {
4919
4920           if (dump_file && (dump_flags & TDF_DETAILS))
4921             fprintf (dump_file, "checks for upper/lower bounds worked!\n");
4922
4923           if (!omega_reduce_with_subs)
4924             {
4925               resurrect_subs (pb);
4926               gcc_assert (pb->num_subs == 0);
4927             }
4928
4929           return true;
4930         }
4931     }
4932
4933
4934   if (dump_file && (dump_flags & TDF_DETAILS))
4935     fprintf (dump_file,
4936              "*** Doing potentially expensive elimination tests "
4937              "for red equations\n");
4938
4939   please_no_equalities_in_simplified_problems++;
4940   omega_eliminate_red (pb, true);
4941   please_no_equalities_in_simplified_problems--;
4942
4943   result = false;
4944   gcc_assert (pb->num_eqs == 0);
4945
4946   for (e = pb->num_geqs - 1; e >= 0; e--)
4947     if (pb->geqs[e].color == omega_red)
4948       result = true;
4949
4950   if (dump_file && (dump_flags & TDF_DETAILS))
4951     {
4952       if (!result)
4953         fprintf (dump_file,
4954                  "******************** Redundant Red Equations eliminated!!\n");
4955       else
4956         fprintf (dump_file,
4957                  "******************** Red Equations remain\n");
4958
4959       omega_print_problem (dump_file, pb);
4960     }
4961
4962   if (!omega_reduce_with_subs)
4963     {
4964       normalize_return_type r;
4965
4966       resurrect_subs (pb);
4967       r = normalize_omega_problem (pb);
4968       gcc_assert (r != normalize_false);
4969
4970       coalesce (pb);
4971       cleanout_wildcards (pb);
4972       gcc_assert (pb->num_subs == 0);
4973     }
4974
4975   return result;
4976 }
4977
4978 /* Calls omega_simplify_problem in approximate mode.  */
4979
4980 enum omega_result
4981 omega_simplify_approximate (omega_pb pb)
4982 {
4983   enum omega_result result;
4984
4985   if (dump_file && (dump_flags & TDF_DETAILS))
4986     fprintf (dump_file, "(Entering approximate mode\n");
4987
4988   in_approximate_mode = true;
4989   result = omega_simplify_problem (pb);
4990   in_approximate_mode = false;
4991
4992   gcc_assert (pb->num_vars == pb->safe_vars);
4993   if (!omega_reduce_with_subs)
4994     gcc_assert (pb->num_subs == 0);
4995
4996   if (dump_file && (dump_flags & TDF_DETAILS))
4997     fprintf (dump_file, "Leaving approximate mode)\n");
4998
4999   return result;
5000 }
5001
5002
5003 /* Simplifies problem PB by eliminating redundant constraints and
5004    reducing the constraints system to a minimal form.  Returns
5005    omega_true when the problem was successfully reduced, omega_unknown
5006    when the solver is unable to determine an answer.  */
5007
5008 enum omega_result
5009 omega_simplify_problem (omega_pb pb)
5010 {
5011   int i;
5012
5013   omega_found_reduction = omega_false;
5014
5015   if (!pb->variables_initialized)
5016     omega_initialize_variables (pb);
5017
5018   if (next_key * 3 > MAX_KEYS)
5019     {
5020       int e;
5021
5022       hash_version++;
5023       next_key = OMEGA_MAX_VARS + 1;
5024
5025       for (e = pb->num_geqs - 1; e >= 0; e--)
5026         pb->geqs[e].touched = 1;
5027
5028       for (i = 0; i < HASH_TABLE_SIZE; i++)
5029         hash_master[i].touched = -1;
5030
5031       pb->hash_version = hash_version;
5032     }
5033
5034   else if (pb->hash_version != hash_version)
5035     {
5036       int e;
5037
5038       for (e = pb->num_geqs - 1; e >= 0; e--)
5039         pb->geqs[e].touched = 1;
5040
5041       pb->hash_version = hash_version;
5042     }
5043
5044   if (pb->num_vars > pb->num_eqs + 3 * pb->safe_vars)
5045     omega_free_eliminations (pb, pb->safe_vars);
5046
5047   if (!may_be_red && pb->num_subs == 0 && pb->safe_vars == 0)
5048     {
5049       omega_found_reduction = omega_solve_problem (pb, omega_unknown);
5050
5051       if (omega_found_reduction != omega_false
5052           && !return_single_result)
5053         {
5054           pb->num_geqs = 0;
5055           pb->num_eqs = 0;
5056           (*omega_when_reduced) (pb);
5057         }
5058
5059       return omega_found_reduction;
5060     }
5061
5062   omega_solve_problem (pb, omega_simplify);
5063
5064   if (omega_found_reduction != omega_false)
5065     {
5066       for (i = 1; omega_safe_var_p (pb, i); i++)
5067         pb->forwarding_address[pb->var[i]] = i;
5068
5069       for (i = 0; i < pb->num_subs; i++)
5070         pb->forwarding_address[pb->subs[i].key] = -i - 1;
5071     }
5072
5073   if (!omega_reduce_with_subs)
5074     gcc_assert (please_no_equalities_in_simplified_problems
5075                 || omega_found_reduction == omega_false
5076                 || pb->num_subs == 0);
5077
5078   return omega_found_reduction;
5079 }
5080
5081 /* Make variable VAR unprotected: it then can be eliminated.  */
5082
5083 void
5084 omega_unprotect_variable (omega_pb pb, int var)
5085 {
5086   int e, idx;
5087   idx = pb->forwarding_address[var];
5088
5089   if (idx < 0)
5090     {
5091       idx = -1 - idx;
5092       pb->num_subs--;
5093
5094       if (idx < pb->num_subs)
5095         {
5096           omega_copy_eqn (&pb->subs[idx], &pb->subs[pb->num_subs],
5097                           pb->num_vars);
5098           pb->forwarding_address[pb->subs[idx].key] = -idx - 1;
5099         }
5100     }
5101   else
5102     {
5103       int *bring_to_life = XNEWVEC (int, OMEGA_MAX_VARS);
5104       int e2;
5105
5106       for (e = pb->num_subs - 1; e >= 0; e--)
5107         bring_to_life[e] = (pb->subs[e].coef[idx] != 0);
5108
5109       for (e2 = pb->num_subs - 1; e2 >= 0; e2--)
5110         if (bring_to_life[e2])
5111           {
5112             pb->num_vars++;
5113             pb->safe_vars++;
5114
5115             if (pb->safe_vars < pb->num_vars)
5116               {
5117                 for (e = pb->num_geqs - 1; e >= 0; e--)
5118                   {
5119                     pb->geqs[e].coef[pb->num_vars] =
5120                       pb->geqs[e].coef[pb->safe_vars];
5121
5122                     pb->geqs[e].coef[pb->safe_vars] = 0;
5123                   }
5124
5125                 for (e = pb->num_eqs - 1; e >= 0; e--)
5126                   {
5127                     pb->eqs[e].coef[pb->num_vars] =
5128                       pb->eqs[e].coef[pb->safe_vars];
5129
5130                     pb->eqs[e].coef[pb->safe_vars] = 0;
5131                   }
5132
5133                 for (e = pb->num_subs - 1; e >= 0; e--)
5134                   {
5135                     pb->subs[e].coef[pb->num_vars] =
5136                       pb->subs[e].coef[pb->safe_vars];
5137
5138                     pb->subs[e].coef[pb->safe_vars] = 0;
5139                   }
5140
5141                 pb->var[pb->num_vars] = pb->var[pb->safe_vars];
5142                 pb->forwarding_address[pb->var[pb->num_vars]] =
5143                   pb->num_vars;
5144               }
5145             else
5146               {
5147                 for (e = pb->num_geqs - 1; e >= 0; e--)
5148                   pb->geqs[e].coef[pb->safe_vars] = 0;
5149
5150                 for (e = pb->num_eqs - 1; e >= 0; e--)
5151                   pb->eqs[e].coef[pb->safe_vars] = 0;
5152
5153                 for (e = pb->num_subs - 1; e >= 0; e--)
5154                   pb->subs[e].coef[pb->safe_vars] = 0;
5155               }
5156
5157             pb->var[pb->safe_vars] = pb->subs[e2].key;
5158             pb->forwarding_address[pb->subs[e2].key] = pb->safe_vars;
5159
5160             omega_copy_eqn (&(pb->eqs[pb->num_eqs]), &(pb->subs[e2]),
5161                             pb->num_vars);
5162             pb->eqs[pb->num_eqs++].coef[pb->safe_vars] = -1;
5163             gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5164
5165             if (e2 < pb->num_subs - 1)
5166               omega_copy_eqn (&(pb->subs[e2]), &(pb->subs[pb->num_subs - 1]),
5167                               pb->num_vars);
5168
5169             pb->num_subs--;
5170           }
5171
5172       omega_unprotect_1 (pb, &idx, NULL);
5173       free (bring_to_life);
5174     }
5175
5176   chain_unprotect (pb);
5177 }
5178
5179 /* Unprotects VAR and simplifies PB.  */
5180
5181 enum omega_result
5182 omega_constrain_variable_sign (omega_pb pb, enum omega_eqn_color color,
5183                                int var, int sign)
5184 {
5185   int n_vars = pb->num_vars;
5186   int e, j;
5187   int k = pb->forwarding_address[var];
5188
5189   if (k < 0)
5190     {
5191       k = -1 - k;
5192
5193       if (sign != 0)
5194         {
5195           e = pb->num_geqs++;
5196           omega_copy_eqn (&pb->geqs[e], &pb->subs[k], pb->num_vars);
5197
5198           for (j = 0; j <= n_vars; j++)
5199             pb->geqs[e].coef[j] *= sign;
5200
5201           pb->geqs[e].coef[0]--;
5202           pb->geqs[e].touched = 1;
5203           pb->geqs[e].color = color;
5204         }
5205       else
5206         {
5207           e = pb->num_eqs++;
5208           gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5209           omega_copy_eqn (&pb->eqs[e], &pb->subs[k], pb->num_vars);
5210           pb->eqs[e].color = color;
5211         }
5212     }
5213   else if (sign != 0)
5214     {
5215       e = pb->num_geqs++;
5216       omega_init_eqn_zero (&pb->geqs[e], pb->num_vars);
5217       pb->geqs[e].coef[k] = sign;
5218       pb->geqs[e].coef[0] = -1;
5219       pb->geqs[e].touched = 1;
5220       pb->geqs[e].color = color;
5221     }
5222   else
5223     {
5224       e = pb->num_eqs++;
5225       gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5226       omega_init_eqn_zero (&pb->eqs[e], pb->num_vars);
5227       pb->eqs[e].coef[k] = 1;
5228       pb->eqs[e].color = color;
5229     }
5230
5231   omega_unprotect_variable (pb, var);
5232   return omega_simplify_problem (pb);
5233 }
5234
5235 /* Add an equation "VAR = VALUE" with COLOR to PB.  */
5236
5237 void
5238 omega_constrain_variable_value (omega_pb pb, enum omega_eqn_color color,
5239                                 int var, int value)
5240 {
5241   int e;
5242   int k = pb->forwarding_address[var];
5243
5244   if (k < 0)
5245     {
5246       k = -1 - k;
5247       e = pb->num_eqs++;
5248       gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5249       omega_copy_eqn (&pb->eqs[e], &pb->subs[k], pb->num_vars);
5250       pb->eqs[e].coef[0] -= value;
5251     }
5252   else
5253     {
5254       e = pb->num_eqs++;
5255       omega_init_eqn_zero (&pb->eqs[e], pb->num_vars);
5256       pb->eqs[e].coef[k] = 1;
5257       pb->eqs[e].coef[0] = -value;
5258     }
5259
5260   pb->eqs[e].color = color;
5261 }
5262
5263 /* Return false when the upper and lower bounds are not coupled.
5264    Initialize the bounds LOWER_BOUND and UPPER_BOUND for the values of
5265    variable I.  */
5266
5267 bool
5268 omega_query_variable (omega_pb pb, int i, int *lower_bound, int *upper_bound)
5269 {
5270   int n_vars = pb->num_vars;
5271   int e, j;
5272   bool is_simple;
5273   bool coupled = false;
5274
5275   *lower_bound = neg_infinity;
5276   *upper_bound = pos_infinity;
5277   i = pb->forwarding_address[i];
5278
5279   if (i < 0)
5280     {
5281       i = -i - 1;
5282
5283       for (j = 1; j <= n_vars; j++)
5284         if (pb->subs[i].coef[j] != 0)
5285           return true;
5286
5287       *upper_bound = *lower_bound = pb->subs[i].coef[0];
5288       return false;
5289     }
5290
5291   for (e = pb->num_subs - 1; e >= 0; e--)
5292     if (pb->subs[e].coef[i] != 0)
5293       coupled = true;
5294
5295   for (e = pb->num_eqs - 1; e >= 0; e--)
5296     if (pb->eqs[e].coef[i] != 0)
5297       {
5298         is_simple = true;
5299
5300         for (j = 1; j <= n_vars; j++)
5301           if (i != j && pb->eqs[e].coef[j] != 0)
5302             {
5303               is_simple = false;
5304               coupled = true;
5305               break;
5306             }
5307
5308         if (!is_simple)
5309           continue;
5310         else
5311           {
5312             *lower_bound = *upper_bound =
5313               -pb->eqs[e].coef[i] * pb->eqs[e].coef[0];
5314             return false;
5315           }
5316       }
5317
5318   for (e = pb->num_geqs - 1; e >= 0; e--)
5319     if (pb->geqs[e].coef[i] != 0)
5320       {
5321         if (pb->geqs[e].key == i)
5322           *lower_bound = MAX (*lower_bound, -pb->geqs[e].coef[0]);
5323
5324         else if (pb->geqs[e].key == -i)
5325           *upper_bound = MIN (*upper_bound, pb->geqs[e].coef[0]);
5326
5327         else
5328           coupled = true;
5329       }
5330
5331   return coupled;
5332 }
5333
5334 /* Sets the lower bound L and upper bound U for the values of variable
5335    I, and sets COULD_BE_ZERO to true if variable I might take value
5336    zero.  LOWER_BOUND and UPPER_BOUND are bounds on the values of
5337    variable I.  */
5338
5339 static void
5340 query_coupled_variable (omega_pb pb, int i, int *l, int *u,
5341                         bool *could_be_zero, int lower_bound, int upper_bound)
5342 {
5343   int e, b1, b2;
5344   eqn eqn;
5345   int sign;
5346   int v;
5347
5348   /* Preconditions.  */
5349   gcc_assert (abs (pb->forwarding_address[i]) == 1
5350               && pb->num_vars + pb->num_subs == 2
5351               && pb->num_eqs + pb->num_subs == 1);
5352
5353   /* Define variable I in terms of variable V.  */
5354   if (pb->forwarding_address[i] == -1)
5355     {
5356       eqn = &pb->subs[0];
5357       sign = 1;
5358       v = 1;
5359     }
5360   else
5361     {
5362       eqn = &pb->eqs[0];
5363       sign = -eqn->coef[1];
5364       v = 2;
5365     }
5366
5367   for (e = pb->num_geqs - 1; e >= 0; e--)
5368     if (pb->geqs[e].coef[v] != 0)
5369       {
5370         if (pb->geqs[e].coef[v] == 1)
5371           lower_bound = MAX (lower_bound, -pb->geqs[e].coef[0]);
5372
5373         else
5374           upper_bound = MIN (upper_bound, pb->geqs[e].coef[0]);
5375       }
5376
5377   if (lower_bound > upper_bound)
5378     {
5379       *l = pos_infinity;
5380       *u = neg_infinity;
5381       *could_be_zero = 0;
5382       return;
5383     }
5384
5385   if (lower_bound == neg_infinity)
5386     {
5387       if (eqn->coef[v] > 0)
5388         b1 = sign * neg_infinity;
5389
5390       else
5391         b1 = -sign * neg_infinity;
5392     }
5393   else
5394     b1 = sign * (eqn->coef[0] + eqn->coef[v] * lower_bound);
5395
5396   if (upper_bound == pos_infinity)
5397     {
5398       if (eqn->coef[v] > 0)
5399         b2 = sign * pos_infinity;
5400
5401       else
5402         b2 = -sign * pos_infinity;
5403     }
5404   else
5405     b2 = sign * (eqn->coef[0] + eqn->coef[v] * upper_bound);
5406
5407   *l = MAX (*l, b1 <= b2 ? b1 : b2);
5408   *u = MIN (*u, b1 <= b2 ? b2 : b1);
5409
5410   *could_be_zero = (*l <= 0 && 0 <= *u
5411                     && int_mod (eqn->coef[0], abs (eqn->coef[v])) == 0);
5412 }
5413
5414 /* Return false when a lower bound L and an upper bound U for variable
5415    I in problem PB have been initialized.  */
5416
5417 bool
5418 omega_query_variable_bounds (omega_pb pb, int i, int *l, int *u)
5419 {
5420   *l = neg_infinity;
5421   *u = pos_infinity;
5422
5423   if (!omega_query_variable (pb, i, l, u)
5424       || (pb->num_vars == 1 && pb->forwarding_address[i] == 1))
5425     return false;
5426
5427   if (abs (pb->forwarding_address[i]) == 1
5428       && pb->num_vars + pb->num_subs == 2
5429       && pb->num_eqs + pb->num_subs == 1)
5430     {
5431       bool could_be_zero;
5432       query_coupled_variable (pb, i, l, u, &could_be_zero, neg_infinity,
5433                               pos_infinity);
5434       return false;
5435     }
5436
5437   return true;
5438 }
5439
5440 /* For problem PB, return an integer that represents the classic data
5441    dependence direction in function of the DD_LT, DD_EQ and DD_GT bit
5442    masks that are added to the result.  When DIST_KNOWN is true, DIST
5443    is set to the classic data dependence distance.  LOWER_BOUND and
5444    UPPER_BOUND are bounds on the value of variable I, for example, it
5445    is possible to narrow the iteration domain with safe approximations
5446    of loop counts, and thus discard some data dependences that cannot
5447    occur.  */
5448
5449 int
5450 omega_query_variable_signs (omega_pb pb, int i, int dd_lt,
5451                             int dd_eq, int dd_gt, int lower_bound,
5452                             int upper_bound, bool *dist_known, int *dist)
5453 {
5454   int result;
5455   int l, u;
5456   bool could_be_zero;
5457
5458   l = neg_infinity;
5459   u = pos_infinity;
5460
5461   omega_query_variable (pb, i, &l, &u);
5462   query_coupled_variable (pb, i, &l, &u, &could_be_zero, lower_bound,
5463                           upper_bound);
5464   result = 0;
5465
5466   if (l < 0)
5467     result |= dd_gt;
5468
5469   if (u > 0)
5470     result |= dd_lt;
5471
5472   if (could_be_zero)
5473     result |= dd_eq;
5474
5475   if (l == u)
5476     {
5477       *dist_known = true;
5478       *dist = l;
5479     }
5480   else
5481     *dist_known = false;
5482
5483   return result;
5484 }
5485
5486 /* Initialize PB as an Omega problem with NVARS variables and NPROT
5487    safe variables.  Safe variables are not eliminated during the
5488    Fourier-Motzkin elimination.  Safe variables are all those
5489    variables that are placed at the beginning of the array of
5490    variables: P->var[0, ..., NPROT - 1].  */
5491
5492 omega_pb
5493 omega_alloc_problem (int nvars, int nprot)
5494 {
5495   omega_pb pb;
5496
5497   gcc_assert (nvars <= OMEGA_MAX_VARS);
5498   omega_initialize ();
5499
5500   /* Allocate and initialize PB.  */
5501   pb = XCNEW (struct omega_pb);
5502   pb->var = XCNEWVEC (int, OMEGA_MAX_VARS + 2);
5503   pb->forwarding_address = XCNEWVEC (int, OMEGA_MAX_VARS + 2);
5504   pb->geqs = omega_alloc_eqns (0, OMEGA_MAX_GEQS);
5505   pb->eqs = omega_alloc_eqns (0, OMEGA_MAX_EQS);
5506   pb->subs = omega_alloc_eqns (0, OMEGA_MAX_VARS + 1);
5507
5508   pb->hash_version = hash_version;
5509   pb->num_vars = nvars;
5510   pb->safe_vars = nprot;
5511   pb->variables_initialized = false;
5512   pb->variables_freed = false;
5513   pb->num_eqs = 0;
5514   pb->num_geqs = 0;
5515   pb->num_subs = 0;
5516   return pb;
5517 }
5518
5519 /* Keeps the state of the initialization.  */
5520 static bool omega_initialized = false;
5521
5522 /* Initialization of the Omega solver.  */
5523
5524 void
5525 omega_initialize (void)
5526 {
5527   int i;
5528
5529   if (omega_initialized)
5530     return;
5531
5532   next_wild_card = 0;
5533   next_key = OMEGA_MAX_VARS + 1;
5534   packing = XCNEWVEC (int, OMEGA_MAX_VARS);
5535   fast_lookup = XCNEWVEC (int, MAX_KEYS * 2);
5536   fast_lookup_red = XCNEWVEC (int, MAX_KEYS * 2);
5537   hash_master = omega_alloc_eqns (0, HASH_TABLE_SIZE);
5538
5539   for (i = 0; i < HASH_TABLE_SIZE; i++)
5540     hash_master[i].touched = -1;
5541
5542   sprintf (wild_name[0], "1");
5543   sprintf (wild_name[1], "a");
5544   sprintf (wild_name[2], "b");
5545   sprintf (wild_name[3], "c");
5546   sprintf (wild_name[4], "d");
5547   sprintf (wild_name[5], "e");
5548   sprintf (wild_name[6], "f");
5549   sprintf (wild_name[7], "g");
5550   sprintf (wild_name[8], "h");
5551   sprintf (wild_name[9], "i");
5552   sprintf (wild_name[10], "j");
5553   sprintf (wild_name[11], "k");
5554   sprintf (wild_name[12], "l");
5555   sprintf (wild_name[13], "m");
5556   sprintf (wild_name[14], "n");
5557   sprintf (wild_name[15], "o");
5558   sprintf (wild_name[16], "p");
5559   sprintf (wild_name[17], "q");
5560   sprintf (wild_name[18], "r");
5561   sprintf (wild_name[19], "s");
5562   sprintf (wild_name[20], "t");
5563   sprintf (wild_name[40 - 1], "alpha");
5564   sprintf (wild_name[40 - 2], "beta");
5565   sprintf (wild_name[40 - 3], "gamma");
5566   sprintf (wild_name[40 - 4], "delta");
5567   sprintf (wild_name[40 - 5], "tau");
5568   sprintf (wild_name[40 - 6], "sigma");
5569   sprintf (wild_name[40 - 7], "chi");
5570   sprintf (wild_name[40 - 8], "omega");
5571   sprintf (wild_name[40 - 9], "pi");
5572   sprintf (wild_name[40 - 10], "ni");
5573   sprintf (wild_name[40 - 11], "Alpha");
5574   sprintf (wild_name[40 - 12], "Beta");
5575   sprintf (wild_name[40 - 13], "Gamma");
5576   sprintf (wild_name[40 - 14], "Delta");
5577   sprintf (wild_name[40 - 15], "Tau");
5578   sprintf (wild_name[40 - 16], "Sigma");
5579   sprintf (wild_name[40 - 17], "Chi");
5580   sprintf (wild_name[40 - 18], "Omega");
5581   sprintf (wild_name[40 - 19], "xxx");
5582
5583   omega_initialized = true;
5584 }