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, 2008, 2009 Free Software Foundation,
   9    Inc.
  10    Contributed by Sebastian Pop <sebastian.pop@inria.fr>
  11
  12 This file is part of GCC.
  13
  14 GCC is free software; you can redistribute it and/or modify it under
  15 the terms of the GNU General Public License as published by the Free
  16 Software Foundation; either version 3, or (at your option) any later
  17 version.
  18
  19 GCC is distributed in the hope that it will be useful, but WITHOUT ANY
  20 WARRANTY; without even the implied warranty of MERCHANTABILITY or
  21 FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
  22 for more details.
  23
  24 You should have received a copy of the GNU General Public License
  25 along with GCC; see the file COPYING3.  If not see
  26 <http://www.gnu.org/licenses/>.  */
  27
  28 /* For a detailed description, see "Constraint-Based Array Dependence
  29    Analysis" William Pugh, David Wonnacott, TOPLAS'98 and David
  30    Wonnacott's thesis:
  31    ftp://ftp.cs.umd.edu/pub/omega/davewThesis/davewThesis.ps.gz
  32 */
  33
  34 #include "config.h"
  35 #include "system.h"
  36 #include "coretypes.h"
  37 #include "tm.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_d);
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, 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
1996       for (e = pb->num_geqs - 1; e >= 0; e--)
1997         if (single_var_geq (&pb->geqs[e], pb->num_vars))
1998           {
1999             if (!omega_safe_var_p (pb, abs (pb->geqs[e].key)))
2000               pb->geqs[e].key += (pb->geqs[e].key > 0 ? m : -m);
2001           }
2002         else
2003           {
2004             pb->geqs[e].touched = 1;
2005             pb->geqs[e].key = 0;
2006           }
2007
2008       for (i = pb->num_vars; !omega_safe_var_p (pb, i); i--)
2009         {
2010           pb->var[i + m] = pb->var[i];
2011
2012           for (e = pb->num_geqs - 1; e >= 0; e--)
2013             pb->geqs[e].coef[i + m] = pb->geqs[e].coef[i];
2014
2015           for (e = pb->num_eqs - 1; e >= 0; e--)
2016             pb->eqs[e].coef[i + m] = pb->eqs[e].coef[i];
2017
2018           for (e = pb->num_subs - 1; e >= 0; e--)
2019             pb->subs[e].coef[i + m] = pb->subs[e].coef[i];
2020         }
2021
2022       for (i = pb->safe_vars + m; !omega_safe_var_p (pb, i); i--)
2023         {
2024           for (e = pb->num_geqs - 1; e >= 0; e--)
2025             pb->geqs[e].coef[i] = 0;
2026
2027           for (e = pb->num_eqs - 1; e >= 0; e--)
2028             pb->eqs[e].coef[i] = 0;
2029
2030           for (e = pb->num_subs - 1; e >= 0; e--)
2031             pb->subs[e].coef[i] = 0;
2032         }
2033
2034       pb->num_vars += m;
2035
2036       for (e = pb->num_subs - 1; e >= 0; e--)
2037         {
2038           pb->var[pb->safe_vars + 1 + e] = pb->subs[e].key;
2039           omega_copy_eqn (&(pb->eqs[pb->num_eqs]), &(pb->subs[e]),
2040                           pb->num_vars);
2041           pb->eqs[pb->num_eqs].coef[pb->safe_vars + 1 + e] = -1;
2042           pb->eqs[pb->num_eqs].color = omega_black;
2043
2044           if (dump_file && (dump_flags & TDF_DETAILS))
2045             {
2046               fprintf (dump_file, "brought back: ");
2047               omega_print_eq (dump_file, pb, &pb->eqs[pb->num_eqs]);
2048               fprintf (dump_file, "\n");
2049             }
2050
2051           pb->num_eqs++;
2052           gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
2053         }
2054
2055       pb->safe_vars += m;
2056       pb->num_subs = 0;
2057
2058       if (dump_file && (dump_flags & TDF_DETAILS))
2059         {
2060           fprintf (dump_file, "variables brought back to life\n");
2061           omega_print_problem (dump_file, pb);
2062         }
2063
2064       cleanout_wildcards (pb);
2065     }
2066 }
2067
2068 static inline bool
2069 implies (unsigned int a, unsigned int b)
2070 {
2071   return (a == (a & b));
2072 }
2073
2074 /* Eliminate redundant equations in PB.  When EXPENSIVE is true, an
2075    extra step is performed.  Returns omega_false when there exist no
2076    solution, omega_true otherwise.  */
2077
2078 enum omega_result
2079 omega_eliminate_redundant (omega_pb pb, bool expensive)
2080 {
2081   int c, e, e1, e2, e3, p, q, i, k, alpha, alpha1, alpha2, alpha3;
2082   bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
2083   omega_pb tmp_problem;
2084
2085   /* {P,Z,N}EQS = {Positive,Zero,Negative} Equations.  */
2086   unsigned int *peqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS);
2087   unsigned int *zeqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS);
2088   unsigned int *neqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS);
2089
2090   /* PP = Possible Positives, PZ = Possible Zeros, PN = Possible Negatives */
2091   unsigned int pp, pz, pn;
2092
2093   if (dump_file && (dump_flags & TDF_DETAILS))
2094     {
2095       fprintf (dump_file, "in eliminate Redundant:\n");
2096       omega_print_problem (dump_file, pb);
2097     }
2098
2099   for (e = pb->num_geqs - 1; e >= 0; e--)
2100     {
2101       int tmp = 1;
2102
2103       is_dead[e] = false;
2104       peqs[e] = zeqs[e] = neqs[e] = 0;
2105
2106       for (i = pb->num_vars; i >= 1; i--)
2107         {
2108           if (pb->geqs[e].coef[i] > 0)
2109             peqs[e] |= tmp;
2110           else if (pb->geqs[e].coef[i] < 0)
2111             neqs[e] |= tmp;
2112           else
2113             zeqs[e] |= tmp;
2114
2115           tmp <<= 1;
2116         }
2117     }
2118
2119
2120   for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
2121     if (!is_dead[e1])
2122       for (e2 = e1 - 1; e2 >= 0; e2--)
2123         if (!is_dead[e2])
2124           {
2125             for (p = pb->num_vars; p > 1; p--)
2126               for (q = p - 1; q > 0; q--)
2127                 if ((alpha = pb->geqs[e1].coef[p] * pb->geqs[e2].coef[q]
2128                      - pb->geqs[e2].coef[p] * pb->geqs[e1].coef[q]) != 0)
2129                   goto foundPQ;
2130
2131             continue;
2132
2133           foundPQ:
2134             pz = ((zeqs[e1] & zeqs[e2]) | (peqs[e1] & neqs[e2])
2135                   | (neqs[e1] & peqs[e2]));
2136             pp = peqs[e1] | peqs[e2];
2137             pn = neqs[e1] | neqs[e2];
2138
2139             for (e3 = pb->num_geqs - 1; e3 >= 0; e3--)
2140               if (e3 != e1 && e3 != e2)
2141                 {
2142                   if (!implies (zeqs[e3], pz))
2143                     goto nextE3;
2144
2145                   alpha1 = (pb->geqs[e2].coef[q] * pb->geqs[e3].coef[p]
2146                             - pb->geqs[e2].coef[p] * pb->geqs[e3].coef[q]);
2147                   alpha2 = -(pb->geqs[e1].coef[q] * pb->geqs[e3].coef[p]
2148                              - pb->geqs[e1].coef[p] * pb->geqs[e3].coef[q]);
2149                   alpha3 = alpha;
2150
2151                   if (alpha1 * alpha2 <= 0)
2152                     goto nextE3;
2153
2154                   if (alpha1 < 0)
2155                     {
2156                       alpha1 = -alpha1;
2157                       alpha2 = -alpha2;
2158                       alpha3 = -alpha3;
2159                     }
2160
2161                   if (alpha3 > 0)
2162                     {
2163                       /* Trying to prove e3 is redundant.  */
2164                       if (!implies (peqs[e3], pp)
2165                           || !implies (neqs[e3], pn))
2166                         goto nextE3;
2167
2168                       if (pb->geqs[e3].color == omega_black
2169                           && (pb->geqs[e1].color == omega_red
2170                               || pb->geqs[e2].color == omega_red))
2171                         goto nextE3;
2172
2173                       for (k = pb->num_vars; k >= 1; k--)
2174                         if (alpha3 * pb->geqs[e3].coef[k]
2175                             != (alpha1 * pb->geqs[e1].coef[k]
2176                                 + alpha2 * pb->geqs[e2].coef[k]))
2177                           goto nextE3;
2178
2179                       c = (alpha1 * pb->geqs[e1].coef[0]
2180                            + alpha2 * pb->geqs[e2].coef[0]);
2181
2182                       if (c < alpha3 * (pb->geqs[e3].coef[0] + 1))
2183                         {
2184                           if (dump_file && (dump_flags & TDF_DETAILS))
2185                             {
2186                               fprintf (dump_file,
2187                                        "found redundant inequality\n");
2188                               fprintf (dump_file,
2189                                        "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2190                                        alpha1, alpha2, alpha3);
2191
2192                               omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
2193                               fprintf (dump_file, "\n");
2194                               omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2195                               fprintf (dump_file, "\n=> ");
2196                               omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2197                               fprintf (dump_file, "\n\n");
2198                             }
2199
2200                           is_dead[e3] = true;
2201                         }
2202                     }
2203                   else
2204                     {
2205                       /* Trying to prove e3 <= 0 and therefore e3 = 0,
2206                         or trying to prove e3 < 0, and therefore the
2207                         problem has no solutions.  */
2208                       if (!implies (peqs[e3], pn)
2209                           || !implies (neqs[e3], pp))
2210                         goto nextE3;
2211
2212                       if (pb->geqs[e1].color == omega_red
2213                           || pb->geqs[e2].color == omega_red
2214                           || pb->geqs[e3].color == omega_red)
2215                         goto nextE3;
2216
2217                       alpha3 = alpha3;
2218                       /* verify alpha1*v1+alpha2*v2 = alpha3*v3 */
2219                       for (k = pb->num_vars; k >= 1; k--)
2220                         if (alpha3 * pb->geqs[e3].coef[k]
2221                             != (alpha1 * pb->geqs[e1].coef[k]
2222                                 + alpha2 * pb->geqs[e2].coef[k]))
2223                           goto nextE3;
2224
2225                       c = (alpha1 * pb->geqs[e1].coef[0]
2226                            + alpha2 * pb->geqs[e2].coef[0]);
2227
2228                       if (c < alpha3 * (pb->geqs[e3].coef[0]))
2229                         {
2230                           /* We just proved e3 < 0, so no solutions exist.  */
2231                           if (dump_file && (dump_flags & TDF_DETAILS))
2232                             {
2233                               fprintf (dump_file,
2234                                        "found implied over tight inequality\n");
2235                               fprintf (dump_file,
2236                                        "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2237                                        alpha1, alpha2, -alpha3);
2238                               omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
2239                               fprintf (dump_file, "\n");
2240                               omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2241                               fprintf (dump_file, "\n=> not ");
2242                               omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2243                               fprintf (dump_file, "\n\n");
2244                             }
2245                           free (is_dead);
2246                           free (peqs);
2247                           free (zeqs);
2248                           free (neqs);
2249                           return omega_false;
2250                         }
2251                       else if (c < alpha3 * (pb->geqs[e3].coef[0] - 1))
2252                         {
2253                           /* We just proved that e3 <=0, so e3 = 0.  */
2254                           if (dump_file && (dump_flags & TDF_DETAILS))
2255                             {
2256                               fprintf (dump_file,
2257                                        "found implied tight inequality\n");
2258                               fprintf (dump_file,
2259                                        "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2260                                        alpha1, alpha2, -alpha3);
2261                               omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
2262                               fprintf (dump_file, "\n");
2263                               omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2264                               fprintf (dump_file, "\n=> inverse ");
2265                               omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2266                               fprintf (dump_file, "\n\n");
2267                             }
2268
2269                           omega_copy_eqn (&pb->eqs[pb->num_eqs++],
2270                                           &pb->geqs[e3], pb->num_vars);
2271                           gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
2272                           adding_equality_constraint (pb, pb->num_eqs - 1);
2273                           is_dead[e3] = true;
2274                         }
2275                     }
2276                 nextE3:;
2277                 }
2278           }
2279
2280   /* Delete the inequalities that were marked as dead.  */
2281   for (e = pb->num_geqs - 1; e >= 0; e--)
2282     if (is_dead[e])
2283       omega_delete_geq (pb, e, pb->num_vars);
2284
2285   if (!expensive)
2286     goto eliminate_redundant_done;
2287
2288   tmp_problem = XNEW (struct omega_pb_d);
2289   conservative++;
2290
2291   for (e = pb->num_geqs - 1; e >= 0; e--)
2292     {
2293       if (dump_file && (dump_flags & TDF_DETAILS))
2294         {
2295           fprintf (dump_file,
2296                    "checking equation %d to see if it is redundant: ", e);
2297           omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2298           fprintf (dump_file, "\n");
2299         }
2300
2301       omega_copy_problem (tmp_problem, pb);
2302       omega_negate_geq (tmp_problem, e);
2303       tmp_problem->safe_vars = 0;
2304       tmp_problem->variables_freed = false;
2305
2306       if (omega_solve_problem (tmp_problem, omega_false) == omega_false)
2307         omega_delete_geq (pb, e, pb->num_vars);
2308     }
2309
2310   free (tmp_problem);
2311   conservative--;
2312
2313   if (!omega_reduce_with_subs)
2314     {
2315       resurrect_subs (pb);
2316       gcc_assert (please_no_equalities_in_simplified_problems
2317                   || pb->num_subs == 0);
2318     }
2319
2320  eliminate_redundant_done:
2321   free (is_dead);
2322   free (peqs);
2323   free (zeqs);
2324   free (neqs);
2325   return omega_true;
2326 }
2327
2328 /* For each inequality that has coefficients bigger than 20, try to
2329    create a new constraint that cannot be derived from the original
2330    constraint and that has smaller coefficients.  Add the new
2331    constraint at the end of geqs.  Return the number of inequalities
2332    that have been added to PB.  */
2333
2334 static int
2335 smooth_weird_equations (omega_pb pb)
2336 {
2337   int e1, e2, e3, p, q, k, alpha, alpha1, alpha2, alpha3;
2338   int c;
2339   int v;
2340   int result = 0;
2341
2342   for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
2343     if (pb->geqs[e1].color == omega_black)
2344       {
2345         int g = 999999;
2346
2347         for (v = pb->num_vars; v >= 1; v--)
2348           if (pb->geqs[e1].coef[v] != 0 && abs (pb->geqs[e1].coef[v]) < g)
2349             g = abs (pb->geqs[e1].coef[v]);
2350
2351         /* Magic number.  */
2352         if (g > 20)
2353           {
2354             e3 = pb->num_geqs;
2355
2356             for (v = pb->num_vars; v >= 1; v--)
2357               pb->geqs[e3].coef[v] = int_div (6 * pb->geqs[e1].coef[v] + g / 2,
2358                                               g);
2359
2360             pb->geqs[e3].color = omega_black;
2361             pb->geqs[e3].touched = 1;
2362             /* Magic number.  */
2363             pb->geqs[e3].coef[0] = 9997;
2364
2365             if (dump_file && (dump_flags & TDF_DETAILS))
2366               {
2367                 fprintf (dump_file, "Checking to see if we can derive: ");
2368                 omega_print_geq (dump_file, pb, &pb->geqs[e3]);
2369                 fprintf (dump_file, "\n from: ");
2370                 omega_print_geq (dump_file, pb, &pb->geqs[e1]);
2371                 fprintf (dump_file, "\n");
2372               }
2373
2374             for (e2 = pb->num_geqs - 1; e2 >= 0; e2--)
2375               if (e1 != e2 && pb->geqs[e2].color == omega_black)
2376                 {
2377                   for (p = pb->num_vars; p > 1; p--)
2378                     {
2379                       for (q = p - 1; q > 0; q--)
2380                         {
2381                           alpha =
2382                             (pb->geqs[e1].coef[p] * pb->geqs[e2].coef[q] -
2383                              pb->geqs[e2].coef[p] * pb->geqs[e1].coef[q]);
2384                           if (alpha != 0)
2385                             goto foundPQ;
2386                         }
2387                     }
2388                   continue;
2389
2390                 foundPQ:
2391
2392                   alpha1 = (pb->geqs[e2].coef[q] * pb->geqs[e3].coef[p]
2393                             - pb->geqs[e2].coef[p] * pb->geqs[e3].coef[q]);
2394                   alpha2 = -(pb->geqs[e1].coef[q] * pb->geqs[e3].coef[p]
2395                              - pb->geqs[e1].coef[p] * pb->geqs[e3].coef[q]);
2396                   alpha3 = alpha;
2397
2398                   if (alpha1 * alpha2 <= 0)
2399                     continue;
2400
2401                   if (alpha1 < 0)
2402                     {
2403                       alpha1 = -alpha1;
2404                       alpha2 = -alpha2;
2405                       alpha3 = -alpha3;
2406                     }
2407
2408                   if (alpha3 > 0)
2409                     {
2410                       /* Try to prove e3 is redundant: verify
2411                          alpha1*v1 + alpha2*v2 = alpha3*v3.  */
2412                       for (k = pb->num_vars; k >= 1; k--)
2413                         if (alpha3 * pb->geqs[e3].coef[k]
2414                             != (alpha1 * pb->geqs[e1].coef[k]
2415                                 + alpha2 * pb->geqs[e2].coef[k]))
2416                           goto nextE2;
2417
2418                       c = alpha1 * pb->geqs[e1].coef[0]
2419                         + alpha2 * pb->geqs[e2].coef[0];
2420
2421                       if (c < alpha3 * (pb->geqs[e3].coef[0] + 1))
2422                         pb->geqs[e3].coef[0] = int_div (c, alpha3);
2423                     }
2424                 nextE2:;
2425                 }
2426
2427             if (pb->geqs[e3].coef[0] < 9997)
2428               {
2429                 result++;
2430                 pb->num_geqs++;
2431
2432                 if (dump_file && (dump_flags & TDF_DETAILS))
2433                   {
2434                     fprintf (dump_file,
2435                              "Smoothing weird equations; adding:\n");
2436                     omega_print_geq (dump_file, pb, &pb->geqs[e3]);
2437                     fprintf (dump_file, "\nto:\n");
2438                     omega_print_problem (dump_file, pb);
2439                     fprintf (dump_file, "\n\n");
2440                   }
2441               }
2442           }
2443       }
2444   return result;
2445 }
2446
2447 /* Replace tuples of inequalities, that define upper and lower half
2448    spaces, with an equation.  */
2449
2450 static void
2451 coalesce (omega_pb pb)
2452 {
2453   int e, e2;
2454   int colors = 0;
2455   bool *is_dead;
2456   int found_something = 0;
2457
2458   for (e = 0; e < pb->num_geqs; e++)
2459     if (pb->geqs[e].color == omega_red)
2460       colors++;
2461
2462   if (colors < 2)
2463     return;
2464
2465   is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
2466
2467   for (e = 0; e < pb->num_geqs; e++)
2468     is_dead[e] = false;
2469
2470   for (e = 0; e < pb->num_geqs; e++)
2471     if (pb->geqs[e].color == omega_red
2472         && !pb->geqs[e].touched)
2473       for (e2 = e + 1; e2 < pb->num_geqs; e2++)
2474         if (!pb->geqs[e2].touched
2475             && pb->geqs[e].key == -pb->geqs[e2].key
2476             && pb->geqs[e].coef[0] == -pb->geqs[e2].coef[0]
2477             && pb->geqs[e2].color == omega_red)
2478           {
2479             omega_copy_eqn (&pb->eqs[pb->num_eqs++], &pb->geqs[e],
2480                             pb->num_vars);
2481             gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
2482             found_something++;
2483             is_dead[e] = true;
2484             is_dead[e2] = true;
2485           }
2486
2487   for (e = pb->num_geqs - 1; e >= 0; e--)
2488     if (is_dead[e])
2489       omega_delete_geq (pb, e, pb->num_vars);
2490
2491   if (dump_file && (dump_flags & TDF_DETAILS) && found_something)
2492     {
2493       fprintf (dump_file, "Coalesced pb->geqs into %d EQ's:\n",
2494                found_something);
2495       omega_print_problem (dump_file, pb);
2496     }
2497
2498   free (is_dead);
2499 }
2500
2501 /* Eliminate red inequalities from PB.  When ELIMINATE_ALL is
2502    true, continue to eliminate all the red inequalities.  */
2503
2504 void
2505 omega_eliminate_red (omega_pb pb, bool eliminate_all)
2506 {
2507   int e, e2, e3, i, j, k, a, alpha1, alpha2;
2508   int c = 0;
2509   bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
2510   int dead_count = 0;
2511   int red_found;
2512   omega_pb tmp_problem;
2513
2514   if (dump_file && (dump_flags & TDF_DETAILS))
2515     {
2516       fprintf (dump_file, "in eliminate RED:\n");
2517       omega_print_problem (dump_file, pb);
2518     }
2519
2520   if (pb->num_eqs > 0)
2521     omega_simplify_problem (pb);
2522
2523   for (e = pb->num_geqs - 1; e >= 0; e--)
2524     is_dead[e] = false;
2525
2526   for (e = pb->num_geqs - 1; e >= 0; e--)
2527     if (pb->geqs[e].color == omega_black && !is_dead[e])
2528       for (e2 = e - 1; e2 >= 0; e2--)
2529         if (pb->geqs[e2].color == omega_black
2530             && !is_dead[e2])
2531           {
2532             a = 0;
2533
2534             for (i = pb->num_vars; i > 1; i--)
2535               for (j = i - 1; j > 0; j--)
2536                 if ((a = (pb->geqs[e].coef[i] * pb->geqs[e2].coef[j]
2537                           - pb->geqs[e2].coef[i] * pb->geqs[e].coef[j])) != 0)
2538                   goto found_pair;
2539
2540             continue;
2541
2542           found_pair:
2543             if (dump_file && (dump_flags & TDF_DETAILS))
2544               {
2545                 fprintf (dump_file,
2546                          "found two equations to combine, i = %s, ",
2547                          omega_variable_to_str (pb, i));
2548                 fprintf (dump_file, "j = %s, alpha = %d\n",
2549                          omega_variable_to_str (pb, j), a);
2550                 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2551                 fprintf (dump_file, "\n");
2552                 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2553                 fprintf (dump_file, "\n");
2554               }
2555
2556             for (e3 = pb->num_geqs - 1; e3 >= 0; e3--)
2557               if (pb->geqs[e3].color == omega_red)
2558                 {
2559                   alpha1 = (pb->geqs[e2].coef[j] * pb->geqs[e3].coef[i]
2560                             - pb->geqs[e2].coef[i] * pb->geqs[e3].coef[j]);
2561                   alpha2 = -(pb->geqs[e].coef[j] * pb->geqs[e3].coef[i]
2562                              - pb->geqs[e].coef[i] * pb->geqs[e3].coef[j]);
2563
2564                   if ((a > 0 && alpha1 > 0 && alpha2 > 0)
2565                       || (a < 0 && alpha1 < 0 && alpha2 < 0))
2566                     {
2567                       if (dump_file && (dump_flags & TDF_DETAILS))
2568                         {
2569                           fprintf (dump_file,
2570                                    "alpha1 = %d, alpha2 = %d;"
2571                                    "comparing against: ",
2572                                    alpha1, alpha2);
2573                           omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2574                           fprintf (dump_file, "\n");
2575                         }
2576
2577                       for (k = pb->num_vars; k >= 0; k--)
2578                         {
2579                           c = (alpha1 * pb->geqs[e].coef[k]
2580                                + alpha2 * pb->geqs[e2].coef[k]);
2581
2582                           if (c != a * pb->geqs[e3].coef[k])
2583                             break;
2584
2585                           if (dump_file && (dump_flags & TDF_DETAILS) && k > 0)
2586                             fprintf (dump_file, " %s: %d, %d\n",
2587                                      omega_variable_to_str (pb, k), c,
2588                                      a * pb->geqs[e3].coef[k]);
2589                         }
2590
2591                       if (k < 0
2592                           || (k == 0 &&
2593                               ((a > 0 && c < a * pb->geqs[e3].coef[k])
2594                                || (a < 0 && c > a * pb->geqs[e3].coef[k]))))
2595                         {
2596                           if (dump_file && (dump_flags & TDF_DETAILS))
2597                             {
2598                               dead_count++;
2599                               fprintf (dump_file,
2600                                        "red equation#%d is dead "
2601                                        "(%d dead so far, %d remain)\n",
2602                                        e3, dead_count,
2603                                        pb->num_geqs - dead_count);
2604                               omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2605                               fprintf (dump_file, "\n");
2606                               omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2607                               fprintf (dump_file, "\n");
2608                               omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2609                               fprintf (dump_file, "\n");
2610                             }
2611                           is_dead[e3] = true;
2612                         }
2613                     }
2614                 }
2615           }
2616
2617   for (e = pb->num_geqs - 1; e >= 0; e--)
2618     if (is_dead[e])
2619       omega_delete_geq (pb, e, pb->num_vars);
2620
2621   free (is_dead);
2622
2623   if (dump_file && (dump_flags & TDF_DETAILS))
2624     {
2625       fprintf (dump_file, "in eliminate RED, easy tests done:\n");
2626       omega_print_problem (dump_file, pb);
2627     }
2628
2629   for (red_found = 0, e = pb->num_geqs - 1; e >= 0; e--)
2630     if (pb->geqs[e].color == omega_red)
2631       red_found = 1;
2632
2633   if (!red_found)
2634     {
2635       if (dump_file && (dump_flags & TDF_DETAILS))
2636         fprintf (dump_file, "fast checks worked\n");
2637
2638       if (!omega_reduce_with_subs)
2639         gcc_assert (please_no_equalities_in_simplified_problems
2640                     || pb->num_subs == 0);
2641
2642       return;
2643     }
2644
2645   if (!omega_verify_simplification
2646       && verify_omega_pb (pb) == omega_false)
2647     return;
2648
2649   conservative++;
2650   tmp_problem = XNEW (struct omega_pb_d);
2651
2652   for (e = pb->num_geqs - 1; e >= 0; e--)
2653     if (pb->geqs[e].color == omega_red)
2654       {
2655         if (dump_file && (dump_flags & TDF_DETAILS))
2656           {
2657             fprintf (dump_file,
2658                      "checking equation %d to see if it is redundant: ", e);
2659             omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2660             fprintf (dump_file, "\n");
2661           }
2662
2663         omega_copy_problem (tmp_problem, pb);
2664         omega_negate_geq (tmp_problem, e);
2665         tmp_problem->safe_vars = 0;
2666         tmp_problem->variables_freed = false;
2667         tmp_problem->num_subs = 0;
2668
2669         if (omega_solve_problem (tmp_problem, omega_false) == omega_false)
2670           {
2671             if (dump_file && (dump_flags & TDF_DETAILS))
2672               fprintf (dump_file, "it is redundant\n");
2673             omega_delete_geq (pb, e, pb->num_vars);
2674           }
2675         else
2676           {
2677             if (dump_file && (dump_flags & TDF_DETAILS))
2678               fprintf (dump_file, "it is not redundant\n");
2679
2680             if (!eliminate_all)
2681               {
2682                 if (dump_file && (dump_flags & TDF_DETAILS))
2683                   fprintf (dump_file, "no need to check other red equations\n");
2684                 break;
2685               }
2686           }
2687       }
2688
2689   conservative--;
2690   free (tmp_problem);
2691   /* omega_simplify_problem (pb); */
2692
2693   if (!omega_reduce_with_subs)
2694     gcc_assert (please_no_equalities_in_simplified_problems
2695                 || pb->num_subs == 0);
2696 }
2697
2698 /* Transform some wildcard variables to non-safe variables.  */
2699
2700 static void
2701 chain_unprotect (omega_pb pb)
2702 {
2703   int i, e;
2704   bool *unprotect = XNEWVEC (bool, OMEGA_MAX_VARS);
2705
2706   for (i = 1; omega_safe_var_p (pb, i); i++)
2707     {
2708       unprotect[i] = omega_wildcard_p (pb, i);
2709
2710       for (e = pb->num_subs - 1; e >= 0; e--)
2711         if (pb->subs[e].coef[i])
2712           unprotect[i] = false;
2713     }
2714
2715   if (dump_file && (dump_flags & TDF_DETAILS))
2716     {
2717       fprintf (dump_file, "Doing chain reaction unprotection\n");
2718       omega_print_problem (dump_file, pb);
2719
2720       for (i = 1; omega_safe_var_p (pb, i); i++)
2721         if (unprotect[i])
2722           fprintf (dump_file, "unprotecting %s\n",
2723                    omega_variable_to_str (pb, i));
2724     }
2725
2726   for (i = 1; omega_safe_var_p (pb, i); i++)
2727     if (unprotect[i])
2728       omega_unprotect_1 (pb, &i, unprotect);
2729
2730   if (dump_file && (dump_flags & TDF_DETAILS))
2731     {
2732       fprintf (dump_file, "After chain reactions\n");
2733       omega_print_problem (dump_file, pb);
2734     }
2735
2736   free (unprotect);
2737 }
2738
2739 /* Reduce problem PB.  */
2740
2741 static void
2742 omega_problem_reduced (omega_pb pb)
2743 {
2744   if (omega_verify_simplification
2745       && !in_approximate_mode
2746       && verify_omega_pb (pb) == omega_false)
2747     return;
2748
2749   if (PARAM_VALUE (PARAM_OMEGA_ELIMINATE_REDUNDANT_CONSTRAINTS)
2750       && !omega_eliminate_redundant (pb, true))
2751     return;
2752
2753   omega_found_reduction = omega_true;
2754
2755   if (!please_no_equalities_in_simplified_problems)
2756     coalesce (pb);
2757
2758   if (omega_reduce_with_subs
2759       || please_no_equalities_in_simplified_problems)
2760     chain_unprotect (pb);
2761   else
2762     resurrect_subs (pb);
2763
2764   if (!return_single_result)
2765     {
2766       int i;
2767
2768       for (i = 1; omega_safe_var_p (pb, i); i++)
2769         pb->forwarding_address[pb->var[i]] = i;
2770
2771       for (i = 0; i < pb->num_subs; i++)
2772         pb->forwarding_address[pb->subs[i].key] = -i - 1;
2773
2774       (*omega_when_reduced) (pb);
2775     }
2776
2777   if (dump_file && (dump_flags & TDF_DETAILS))
2778     {
2779       fprintf (dump_file, "-------------------------------------------\n");
2780       fprintf (dump_file, "problem reduced:\n");
2781       omega_print_problem (dump_file, pb);
2782       fprintf (dump_file, "-------------------------------------------\n");
2783     }
2784 }
2785
2786 /* Eliminates all the free variables for problem PB, that is all the
2787    variables from FV to PB->NUM_VARS.  */
2788
2789 static void
2790 omega_free_eliminations (omega_pb pb, int fv)
2791 {
2792   bool try_again = true;
2793   int i, e, e2;
2794   int n_vars = pb->num_vars;
2795
2796   while (try_again)
2797     {
2798       try_again = false;
2799
2800       for (i = n_vars; i > fv; i--)
2801         {
2802           for (e = pb->num_geqs - 1; e >= 0; e--)
2803             if (pb->geqs[e].coef[i])
2804               break;
2805
2806           if (e < 0)
2807             e2 = e;
2808           else if (pb->geqs[e].coef[i] > 0)
2809             {
2810               for (e2 = e - 1; e2 >= 0; e2--)
2811                 if (pb->geqs[e2].coef[i] < 0)
2812                   break;
2813             }
2814           else
2815             {
2816               for (e2 = e - 1; e2 >= 0; e2--)
2817                 if (pb->geqs[e2].coef[i] > 0)
2818                   break;
2819             }
2820
2821           if (e2 < 0)
2822             {
2823               int e3;
2824               for (e3 = pb->num_subs - 1; e3 >= 0; e3--)
2825                 if (pb->subs[e3].coef[i])
2826                   break;
2827
2828               if (e3 >= 0)
2829                 continue;
2830
2831               for (e3 = pb->num_eqs - 1; e3 >= 0; e3--)
2832                 if (pb->eqs[e3].coef[i])
2833                   break;
2834
2835               if (e3 >= 0)
2836                 continue;
2837
2838               if (dump_file && (dump_flags & TDF_DETAILS))
2839                 fprintf (dump_file, "a free elimination of %s\n",
2840                          omega_variable_to_str (pb, i));
2841
2842               if (e >= 0)
2843                 {
2844                   omega_delete_geq (pb, e, n_vars);
2845
2846                   for (e--; e >= 0; e--)
2847                     if (pb->geqs[e].coef[i])
2848                       omega_delete_geq (pb, e, n_vars);
2849
2850                   try_again = (i < n_vars);
2851                 }
2852
2853               omega_delete_variable (pb, i);
2854               n_vars = pb->num_vars;
2855             }
2856         }
2857     }
2858
2859   if (dump_file && (dump_flags & TDF_DETAILS))
2860     {
2861       fprintf (dump_file, "\nafter free eliminations:\n");
2862       omega_print_problem (dump_file, pb);
2863       fprintf (dump_file, "\n");
2864     }
2865 }
2866
2867 /* Do free red eliminations.  */
2868
2869 static void
2870 free_red_eliminations (omega_pb pb)
2871 {
2872   bool try_again = true;
2873   int i, e, e2;
2874   int n_vars = pb->num_vars;
2875   bool *is_red_var = XNEWVEC (bool, OMEGA_MAX_VARS);
2876   bool *is_dead_var = XNEWVEC (bool, OMEGA_MAX_VARS);
2877   bool *is_dead_geq = XNEWVEC (bool, OMEGA_MAX_GEQS);
2878
2879   for (i = n_vars; i > 0; i--)
2880     {
2881       is_red_var[i] = false;
2882       is_dead_var[i] = false;
2883     }
2884
2885   for (e = pb->num_geqs - 1; e >= 0; e--)
2886     {
2887       is_dead_geq[e] = false;
2888
2889       if (pb->geqs[e].color == omega_red)
2890         for (i = n_vars; i > 0; i--)
2891           if (pb->geqs[e].coef[i] != 0)
2892             is_red_var[i] = true;
2893     }
2894
2895   while (try_again)
2896     {
2897       try_again = false;
2898       for (i = n_vars; i > 0; i--)
2899         if (!is_red_var[i] && !is_dead_var[i])
2900           {
2901             for (e = pb->num_geqs - 1; e >= 0; e--)
2902               if (!is_dead_geq[e] && pb->geqs[e].coef[i])
2903                 break;
2904
2905             if (e < 0)
2906               e2 = e;
2907             else if (pb->geqs[e].coef[i] > 0)
2908               {
2909                 for (e2 = e - 1; e2 >= 0; e2--)
2910                   if (!is_dead_geq[e2] && pb->geqs[e2].coef[i] < 0)
2911                     break;
2912               }
2913             else
2914               {
2915                 for (e2 = e - 1; e2 >= 0; e2--)
2916                   if (!is_dead_geq[e2] && pb->geqs[e2].coef[i] > 0)
2917                     break;
2918               }
2919
2920             if (e2 < 0)
2921               {
2922                 int e3;
2923                 for (e3 = pb->num_subs - 1; e3 >= 0; e3--)
2924                   if (pb->subs[e3].coef[i])
2925                     break;
2926
2927                 if (e3 >= 0)
2928                   continue;
2929
2930                 for (e3 = pb->num_eqs - 1; e3 >= 0; e3--)
2931                   if (pb->eqs[e3].coef[i])
2932                     break;
2933
2934                 if (e3 >= 0)
2935                   continue;
2936
2937                 if (dump_file && (dump_flags & TDF_DETAILS))
2938                   fprintf (dump_file, "a free red elimination of %s\n",
2939                            omega_variable_to_str (pb, i));
2940
2941                 for (; e >= 0; e--)
2942                   if (pb->geqs[e].coef[i])
2943                     is_dead_geq[e] = true;
2944
2945                 try_again = true;
2946                 is_dead_var[i] = true;
2947               }
2948           }
2949     }
2950
2951   for (e = pb->num_geqs - 1; e >= 0; e--)
2952     if (is_dead_geq[e])
2953       omega_delete_geq (pb, e, n_vars);
2954
2955   for (i = n_vars; i > 0; i--)
2956     if (is_dead_var[i])
2957       omega_delete_variable (pb, i);
2958
2959   if (dump_file && (dump_flags & TDF_DETAILS))
2960     {
2961       fprintf (dump_file, "\nafter free red eliminations:\n");
2962       omega_print_problem (dump_file, pb);
2963       fprintf (dump_file, "\n");
2964     }
2965
2966   free (is_red_var);
2967   free (is_dead_var);
2968   free (is_dead_geq);
2969 }
2970
2971 /* For equation EQ of the form "0 = EQN", insert in PB two
2972    inequalities "0 <= EQN" and "0 <= -EQN".  */
2973
2974 void
2975 omega_convert_eq_to_geqs (omega_pb pb, int eq)
2976 {
2977   int i;
2978
2979   if (dump_file && (dump_flags & TDF_DETAILS))
2980     fprintf (dump_file, "Converting Eq to Geqs\n");
2981
2982   /* Insert "0 <= EQN".  */
2983   omega_copy_eqn (&pb->geqs[pb->num_geqs], &pb->eqs[eq], pb->num_vars);
2984   pb->geqs[pb->num_geqs].touched = 1;
2985   pb->num_geqs++;
2986
2987   /* Insert "0 <= -EQN".  */
2988   omega_copy_eqn (&pb->geqs[pb->num_geqs], &pb->eqs[eq], pb->num_vars);
2989   pb->geqs[pb->num_geqs].touched = 1;
2990
2991   for (i = 0; i <= pb->num_vars; i++)
2992     pb->geqs[pb->num_geqs].coef[i] *= -1;
2993
2994   pb->num_geqs++;
2995
2996   if (dump_file && (dump_flags & TDF_DETAILS))
2997     omega_print_problem (dump_file, pb);
2998 }
2999
3000 /* Eliminates variable I from PB.  */
3001
3002 static void
3003 omega_do_elimination (omega_pb pb, int e, int i)
3004 {
3005   eqn sub = omega_alloc_eqns (0, 1);
3006   int c;
3007   int n_vars = pb->num_vars;
3008
3009   if (dump_file && (dump_flags & TDF_DETAILS))
3010     fprintf (dump_file, "eliminating variable %s\n",
3011              omega_variable_to_str (pb, i));
3012
3013   omega_copy_eqn (sub, &pb->eqs[e], pb->num_vars);
3014   c = sub->coef[i];
3015   sub->coef[i] = 0;
3016   if (c == 1 || c == -1)
3017     {
3018       if (pb->eqs[e].color == omega_red)
3019         {
3020           bool fB;
3021           omega_substitute_red (pb, sub, i, c, &fB);
3022           if (fB)
3023             omega_convert_eq_to_geqs (pb, e);
3024           else
3025             omega_delete_variable (pb, i);
3026         }
3027       else
3028         {
3029           omega_substitute (pb, sub, i, c);
3030           omega_delete_variable (pb, i);
3031         }
3032     }
3033   else
3034     {
3035       int a = abs (c);
3036       int e2 = e;
3037
3038       if (dump_file && (dump_flags & TDF_DETAILS))
3039         fprintf (dump_file, "performing non-exact elimination, c = %d\n", c);
3040
3041       for (e = pb->num_eqs - 1; e >= 0; e--)
3042         if (pb->eqs[e].coef[i])
3043           {
3044             eqn eqn = &(pb->eqs[e]);
3045             int j, k;
3046             for (j = n_vars; j >= 0; j--)
3047               eqn->coef[j] *= a;
3048             k = eqn->coef[i];
3049             eqn->coef[i] = 0;
3050             if (sub->color == omega_red)
3051               eqn->color = omega_red;
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_d);
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 best = (INT_MAX);
3726       int j = 0, jLe = 0, jLowerBoundCount = 0;
3727
3728
3729       eliminate_again = false;
3730
3731       if (pb->num_eqs > 0)
3732         return omega_solve_problem (pb, desired_res);
3733
3734       if (!coupled_subscripts)
3735         {
3736           if (pb->safe_vars == 0)
3737             pb->num_geqs = 0;
3738           else
3739             for (e = pb->num_geqs - 1; e >= 0; e--)
3740               if (!omega_safe_var_p (pb, abs (pb->geqs[e].key)))
3741                 omega_delete_geq (pb, e, n_vars);
3742
3743           pb->num_vars = pb->safe_vars;
3744
3745           if (desired_res == omega_simplify)
3746             {
3747               omega_problem_reduced (pb);
3748               return omega_false;
3749             }
3750
3751           return omega_true;
3752         }
3753
3754       if (desired_res != omega_simplify)
3755         fv = 0;
3756       else
3757         fv = pb->safe_vars;
3758
3759       if (pb->num_geqs == 0)
3760         {
3761           if (desired_res == omega_simplify)
3762             {
3763               pb->num_vars = pb->safe_vars;
3764               omega_problem_reduced (pb);
3765               return omega_false;
3766             }
3767           return omega_true;
3768         }
3769
3770       if (desired_res == omega_simplify && n_vars == pb->safe_vars)
3771         {
3772           omega_problem_reduced (pb);
3773           return omega_false;
3774         }
3775
3776       if (pb->num_geqs > OMEGA_MAX_GEQS - 30
3777           || pb->num_geqs > 2 * n_vars * n_vars + 4 * n_vars + 10)
3778         {
3779           if (dump_file && (dump_flags & TDF_DETAILS))
3780             fprintf (dump_file,
3781                      "TOO MANY EQUATIONS; "
3782                      "%d equations, %d variables, "
3783                      "ELIMINATING REDUNDANT ONES\n",
3784                      pb->num_geqs, n_vars);
3785
3786           if (!omega_eliminate_redundant (pb, false))
3787             return omega_false;
3788
3789           n_vars = pb->num_vars;
3790
3791           if (pb->num_eqs > 0)
3792             return omega_solve_problem (pb, desired_res);
3793
3794           if (dump_file && (dump_flags & TDF_DETAILS))
3795             fprintf (dump_file, "END ELIMINATION OF REDUNDANT EQUATIONS\n");
3796         }
3797
3798       if (desired_res != omega_simplify)
3799         fv = 0;
3800       else
3801         fv = pb->safe_vars;
3802
3803       for (i = n_vars; i != fv; i--)
3804         {
3805           int score;
3806           int ub = -2;
3807           int lb = -2;
3808           bool lucky = false;
3809           int upper_bound_count = 0;
3810
3811           lower_bound_count = 0;
3812           minC = maxC = 0;
3813
3814           for (e = pb->num_geqs - 1; e >= 0; e--)
3815             if (pb->geqs[e].coef[i] < 0)
3816               {
3817                 minC = MIN (minC, pb->geqs[e].coef[i]);
3818                 upper_bound_count++;
3819                 if (pb->geqs[e].coef[i] < -1)
3820                   {
3821                     if (ub == -2)
3822                       ub = e;
3823                     else
3824                       ub = -1;
3825                   }
3826               }
3827             else if (pb->geqs[e].coef[i] > 0)
3828               {
3829                 maxC = MAX (maxC, pb->geqs[e].coef[i]);
3830                 lower_bound_count++;
3831                 Le = e;
3832                 if (pb->geqs[e].coef[i] > 1)
3833                   {
3834                     if (lb == -2)
3835                       lb = e;
3836                     else
3837                       lb = -1;
3838                   }
3839               }
3840
3841           if (lower_bound_count == 0
3842               || upper_bound_count == 0)
3843             {
3844               lower_bound_count = 0;
3845               break;
3846             }
3847
3848           if (ub >= 0 && lb >= 0
3849               && pb->geqs[lb].key == -pb->geqs[ub].key)
3850             {
3851               int Lc = pb->geqs[lb].coef[i];
3852               int Uc = -pb->geqs[ub].coef[i];
3853               int diff =
3854                 Lc * pb->geqs[ub].coef[0] + Uc * pb->geqs[lb].coef[0];
3855               lucky = (diff >= (Uc - 1) * (Lc - 1));
3856             }
3857
3858           if (maxC == 1
3859               || minC == -1
3860               || lucky
3861               || in_approximate_mode)
3862             {
3863               score = upper_bound_count * lower_bound_count;
3864
3865               if (dump_file && (dump_flags & TDF_DETAILS))
3866                 fprintf (dump_file,
3867                          "For %s, exact, score = %d*%d, range = %d ... %d,"
3868                          "\nlucky = %d, in_approximate_mode=%d \n",
3869                          omega_variable_to_str (pb, i),
3870                          upper_bound_count,
3871                          lower_bound_count, minC, maxC, lucky,
3872                          in_approximate_mode);
3873
3874               if (!exact
3875                   || score < best)
3876                 {
3877
3878                   best = score;
3879                   j = i;
3880                   minCj = minC;
3881                   jLe = Le;
3882                   jLowerBoundCount = lower_bound_count;
3883                   exact = true;
3884                   lucky_exact = lucky;
3885                   if (score == 1)
3886                     break;
3887                 }
3888             }
3889           else if (!exact)
3890             {
3891               if (dump_file && (dump_flags & TDF_DETAILS))
3892                 fprintf (dump_file,
3893                          "For %s, non-exact, score = %d*%d,"
3894                          "range = %d ... %d \n",
3895                          omega_variable_to_str (pb, i),
3896                          upper_bound_count,
3897                          lower_bound_count, minC, maxC);
3898
3899               score = maxC - minC;
3900
3901               if (best > score)
3902                 {
3903                   best = score;
3904                   j = i;
3905                   minCj = minC;
3906                   jLe = Le;
3907                   jLowerBoundCount = lower_bound_count;
3908                 }
3909             }
3910         }
3911
3912       if (lower_bound_count == 0)
3913         {
3914           omega_free_eliminations (pb, pb->safe_vars);
3915           n_vars = pb->num_vars;
3916           eliminate_again = true;
3917           continue;
3918         }
3919
3920       i = j;
3921       minC = minCj;
3922       Le = jLe;
3923       lower_bound_count = jLowerBoundCount;
3924
3925       for (e = pb->num_geqs - 1; e >= 0; e--)
3926         if (pb->geqs[e].coef[i] > 0)
3927           {
3928             if (pb->geqs[e].coef[i] == -minC)
3929               max_splinters += -minC - 1;
3930             else
3931               max_splinters +=
3932                 check_pos_mul ((pb->geqs[e].coef[i] - 1),
3933                                (-minC - 1)) / (-minC) + 1;
3934           }
3935
3936       /* #ifdef Omega3 */
3937       /* Trying to produce exact elimination by finding redundant
3938          constraints.  */
3939       if (!exact && !tried_eliminating_redundant)
3940         {
3941           omega_eliminate_redundant (pb, false);
3942           tried_eliminating_redundant = true;
3943           eliminate_again = true;
3944           continue;
3945         }
3946       tried_eliminating_redundant = false;
3947       /* #endif */
3948
3949       if (return_single_result && desired_res == omega_simplify && !exact)
3950         {
3951           omega_problem_reduced (pb);
3952           return omega_true;
3953         }
3954
3955       /* #ifndef Omega3 */
3956       /* Trying to produce exact elimination by finding redundant
3957          constraints.  */
3958       if (!exact && !tried_eliminating_redundant)
3959         {
3960           omega_eliminate_redundant (pb, false);
3961           tried_eliminating_redundant = true;
3962           continue;
3963         }
3964       tried_eliminating_redundant = false;
3965       /* #endif */
3966
3967       if (!exact)
3968         {
3969           int e1, e2;
3970
3971           for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
3972             if (pb->geqs[e1].color == omega_black)
3973               for (e2 = e1 - 1; e2 >= 0; e2--)
3974                 if (pb->geqs[e2].color == omega_black
3975                     && pb->geqs[e1].key == -pb->geqs[e2].key
3976                     && ((pb->geqs[e1].coef[0] + pb->geqs[e2].coef[0])
3977                         * (3 - single_var_geq (&pb->geqs[e1], pb->num_vars))
3978                         / 2 < parallel_difference))
3979                   {
3980                     parallel_difference =
3981                       (pb->geqs[e1].coef[0] + pb->geqs[e2].coef[0])
3982                       * (3 - single_var_geq (&pb->geqs[e1], pb->num_vars))
3983                       / 2;
3984                     best_parallel_eqn = e1;
3985                   }
3986
3987           if (dump_file && (dump_flags & TDF_DETAILS)
3988               && best_parallel_eqn >= 0)
3989             {
3990               fprintf (dump_file,
3991                        "Possible parallel projection, diff = %d, in ",
3992                        parallel_difference);
3993               omega_print_geq (dump_file, pb, &(pb->geqs[best_parallel_eqn]));
3994               fprintf (dump_file, "\n");
3995               omega_print_problem (dump_file, pb);
3996             }
3997         }
3998
3999       if (dump_file && (dump_flags & TDF_DETAILS))
4000         {
4001           fprintf (dump_file, "going to eliminate %s, (%d,%d,%d)\n",
4002                    omega_variable_to_str (pb, i), i, minC,
4003                    lower_bound_count);
4004           omega_print_problem (dump_file, pb);
4005
4006           if (lucky_exact)
4007             fprintf (dump_file, "(a lucky exact elimination)\n");
4008
4009           else if (exact)
4010             fprintf (dump_file, "(an exact elimination)\n");
4011
4012           fprintf (dump_file, "Max # of splinters = %d\n", max_splinters);
4013         }
4014
4015       gcc_assert (max_splinters >= 1);
4016
4017       if (!exact && desired_res == omega_simplify && best_parallel_eqn >= 0
4018           && parallel_difference <= max_splinters)
4019         return parallel_splinter (pb, best_parallel_eqn, parallel_difference,
4020                                   desired_res);
4021
4022       smoothed = false;
4023
4024       if (i != n_vars)
4025         {
4026           int t;
4027           int j = pb->num_vars;
4028
4029           if (dump_file && (dump_flags & TDF_DETAILS))
4030             {
4031               fprintf (dump_file, "Swapping %d and %d\n", i, j);
4032               omega_print_problem (dump_file, pb);
4033             }
4034
4035           swap (&pb->var[i], &pb->var[j]);
4036
4037           for (e = pb->num_geqs - 1; e >= 0; e--)
4038             if (pb->geqs[e].coef[i] != pb->geqs[e].coef[j])
4039               {
4040                 pb->geqs[e].touched = 1;
4041                 t = pb->geqs[e].coef[i];
4042                 pb->geqs[e].coef[i] = pb->geqs[e].coef[j];
4043                 pb->geqs[e].coef[j] = t;
4044               }
4045
4046           for (e = pb->num_subs - 1; e >= 0; e--)
4047             if (pb->subs[e].coef[i] != pb->subs[e].coef[j])
4048               {
4049                 t = pb->subs[e].coef[i];
4050                 pb->subs[e].coef[i] = pb->subs[e].coef[j];
4051                 pb->subs[e].coef[j] = t;
4052               }
4053
4054           if (dump_file && (dump_flags & TDF_DETAILS))
4055             {
4056               fprintf (dump_file, "Swapping complete \n");
4057               omega_print_problem (dump_file, pb);
4058               fprintf (dump_file, "\n");
4059             }
4060
4061           i = j;
4062         }
4063
4064       else if (dump_file && (dump_flags & TDF_DETAILS))
4065         {
4066           fprintf (dump_file, "No swap needed\n");
4067           omega_print_problem (dump_file, pb);
4068         }
4069
4070       pb->num_vars--;
4071       n_vars = pb->num_vars;
4072
4073       if (exact)
4074         {
4075           if (n_vars == 1)
4076             {
4077               int upper_bound = pos_infinity;
4078               int lower_bound = neg_infinity;
4079               enum omega_eqn_color ub_color = omega_black;
4080               enum omega_eqn_color lb_color = omega_black;
4081               int topeqn = pb->num_geqs - 1;
4082               int Lc = pb->geqs[Le].coef[i];
4083
4084               for (Le = topeqn; Le >= 0; Le--)
4085                 if ((Lc = pb->geqs[Le].coef[i]) == 0)
4086                   {
4087                     if (pb->geqs[Le].coef[1] == 1)
4088                       {
4089                         int constantTerm = -pb->geqs[Le].coef[0];
4090
4091                         if (constantTerm > lower_bound ||
4092                             (constantTerm == lower_bound &&
4093                              !omega_eqn_is_red (&pb->geqs[Le], desired_res)))
4094                           {
4095                             lower_bound = constantTerm;
4096                             lb_color = pb->geqs[Le].color;
4097                           }
4098
4099                         if (dump_file && (dump_flags & TDF_DETAILS))
4100                           {
4101                             if (pb->geqs[Le].color == omega_black)
4102                               fprintf (dump_file, " :::=> %s >= %d\n",
4103                                        omega_variable_to_str (pb, 1),
4104                                        constantTerm);
4105                             else
4106                               fprintf (dump_file,
4107                                        " :::=> [%s >= %d]\n",
4108                                        omega_variable_to_str (pb, 1),
4109                                        constantTerm);
4110                           }
4111                       }
4112                     else
4113                       {
4114                         int constantTerm = pb->geqs[Le].coef[0];
4115                         if (constantTerm < upper_bound ||
4116                             (constantTerm == upper_bound
4117                              && !omega_eqn_is_red (&pb->geqs[Le],
4118                                                    desired_res)))
4119                           {
4120                             upper_bound = constantTerm;
4121                             ub_color = pb->geqs[Le].color;
4122                           }
4123
4124                         if (dump_file && (dump_flags & TDF_DETAILS))
4125                           {
4126                             if (pb->geqs[Le].color == omega_black)
4127                               fprintf (dump_file, " :::=> %s <= %d\n",
4128                                        omega_variable_to_str (pb, 1),
4129                                        constantTerm);
4130                             else
4131                               fprintf (dump_file,
4132                                        " :::=> [%s <= %d]\n",
4133                                        omega_variable_to_str (pb, 1),
4134                                        constantTerm);
4135                           }
4136                       }
4137                   }
4138                 else if (Lc > 0)
4139                   for (Ue = topeqn; Ue >= 0; Ue--)
4140                     if (pb->geqs[Ue].coef[i] < 0
4141                         && pb->geqs[Le].key != -pb->geqs[Ue].key)
4142                       {
4143                         int Uc = -pb->geqs[Ue].coef[i];
4144                         int coefficient = pb->geqs[Ue].coef[1] * Lc
4145                           + pb->geqs[Le].coef[1] * Uc;
4146                         int constantTerm = pb->geqs[Ue].coef[0] * Lc
4147                           + pb->geqs[Le].coef[0] * Uc;
4148
4149                         if (dump_file && (dump_flags & TDF_DETAILS))
4150                           {
4151                             omega_print_geq_extra (dump_file, pb,
4152                                                    &(pb->geqs[Ue]));
4153                             fprintf (dump_file, "\n");
4154                             omega_print_geq_extra (dump_file, pb,
4155                                                    &(pb->geqs[Le]));
4156                             fprintf (dump_file, "\n");
4157                           }
4158
4159                         if (coefficient > 0)
4160                           {
4161                             constantTerm = -int_div (constantTerm, coefficient);
4162
4163                             if (constantTerm > lower_bound
4164                                 || (constantTerm == lower_bound
4165                                     && (desired_res != omega_simplify
4166                                         || (pb->geqs[Ue].color == omega_black
4167                                             && pb->geqs[Le].color == omega_black))))
4168                               {
4169                                 lower_bound = constantTerm;
4170                                 lb_color = (pb->geqs[Ue].color == omega_red
4171                                             || pb->geqs[Le].color == omega_red)
4172                                   ? omega_red : omega_black;
4173                               }
4174
4175                             if (dump_file && (dump_flags & TDF_DETAILS))
4176                               {
4177                                 if (pb->geqs[Ue].color == omega_red
4178                                     || pb->geqs[Le].color == omega_red)
4179                                   fprintf (dump_file,
4180                                            " ::=> [%s >= %d]\n",
4181                                            omega_variable_to_str (pb, 1),
4182                                            constantTerm);
4183                                 else
4184                                   fprintf (dump_file,
4185                                            " ::=> %s >= %d\n",
4186                                            omega_variable_to_str (pb, 1),
4187                                            constantTerm);
4188                               }
4189                           }
4190                         else
4191                           {
4192                             constantTerm = int_div (constantTerm, -coefficient);
4193                             if (constantTerm < upper_bound
4194                                 || (constantTerm == upper_bound
4195                                     && pb->geqs[Ue].color == omega_black
4196                                     && pb->geqs[Le].color == omega_black))
4197                               {
4198                                 upper_bound = constantTerm;
4199                                 ub_color = (pb->geqs[Ue].color == omega_red
4200                                             || pb->geqs[Le].color == omega_red)
4201                                   ? omega_red : omega_black;
4202                               }
4203
4204                             if (dump_file
4205                                 && (dump_flags & TDF_DETAILS))
4206                               {
4207                                 if (pb->geqs[Ue].color == omega_red
4208                                     || pb->geqs[Le].color == omega_red)
4209                                   fprintf (dump_file,
4210                                            " ::=> [%s <= %d]\n",
4211                                            omega_variable_to_str (pb, 1),
4212                                            constantTerm);
4213                                 else
4214                                   fprintf (dump_file,
4215                                            " ::=> %s <= %d\n",
4216                                            omega_variable_to_str (pb, 1),
4217                                            constantTerm);
4218                               }
4219                           }
4220                       }
4221
4222               pb->num_geqs = 0;
4223
4224               if (dump_file && (dump_flags & TDF_DETAILS))
4225                 fprintf (dump_file,
4226                          " therefore, %c%d <= %c%s%c <= %d%c\n",
4227                          lb_color == omega_red ? '[' : ' ', lower_bound,
4228                          (lb_color == omega_red && ub_color == omega_black)
4229                          ? ']' : ' ',
4230                          omega_variable_to_str (pb, 1),
4231                          (lb_color == omega_black && ub_color == omega_red)
4232                          ? '[' : ' ',
4233                          upper_bound, ub_color == omega_red ? ']' : ' ');
4234
4235               if (lower_bound > upper_bound)
4236                 return omega_false;
4237
4238               if (pb->safe_vars == 1)
4239                 {
4240                   if (upper_bound == lower_bound
4241                       && !(ub_color == omega_red || lb_color == omega_red)
4242                       && !please_no_equalities_in_simplified_problems)
4243                     {
4244                       pb->num_eqs++;
4245                       pb->eqs[0].coef[1] = -1;
4246                       pb->eqs[0].coef[0] = upper_bound;
4247
4248                       if (ub_color == omega_red
4249                           || lb_color == omega_red)
4250                         pb->eqs[0].color = omega_red;
4251
4252                       if (desired_res == omega_simplify
4253                           && pb->eqs[0].color == omega_black)
4254                         return omega_solve_problem (pb, desired_res);
4255                     }
4256
4257                   if (upper_bound != pos_infinity)
4258                     {
4259                       pb->geqs[0].coef[1] = -1;
4260                       pb->geqs[0].coef[0] = upper_bound;
4261                       pb->geqs[0].color = ub_color;
4262                       pb->geqs[0].key = -1;
4263                       pb->geqs[0].touched = 0;
4264                       pb->num_geqs++;
4265                     }
4266
4267                   if (lower_bound != neg_infinity)
4268                     {
4269                       pb->geqs[pb->num_geqs].coef[1] = 1;
4270                       pb->geqs[pb->num_geqs].coef[0] = -lower_bound;
4271                       pb->geqs[pb->num_geqs].color = lb_color;
4272                       pb->geqs[pb->num_geqs].key = 1;
4273                       pb->geqs[pb->num_geqs].touched = 0;
4274                       pb->num_geqs++;
4275                     }
4276                 }
4277
4278               if (desired_res == omega_simplify)
4279                 {
4280                   omega_problem_reduced (pb);
4281                   return omega_false;
4282                 }
4283               else
4284                 {
4285                   if (!conservative
4286                       && (desired_res != omega_simplify
4287                           || (lb_color == omega_black
4288                               && ub_color == omega_black))
4289                       && original_problem != no_problem
4290                       && lower_bound == upper_bound)
4291                     {
4292                       for (i = original_problem->num_vars; i >= 0; i--)
4293                         if (original_problem->var[i] == pb->var[1])
4294                           break;
4295
4296                       if (i == 0)
4297                         break;
4298
4299                       e = original_problem->num_eqs++;
4300                       omega_init_eqn_zero (&original_problem->eqs[e],
4301                                            original_problem->num_vars);
4302                       original_problem->eqs[e].coef[i] = -1;
4303                       original_problem->eqs[e].coef[0] = upper_bound;
4304
4305                       if (dump_file && (dump_flags & TDF_DETAILS))
4306                         {
4307                           fprintf (dump_file,
4308                                    "adding equality %d to outer problem\n", e);
4309                           omega_print_problem (dump_file, original_problem);
4310                         }
4311                     }
4312                   return omega_true;
4313                 }
4314             }
4315
4316           eliminate_again = true;
4317
4318           if (lower_bound_count == 1)
4319             {
4320               eqn lbeqn = omega_alloc_eqns (0, 1);
4321               int Lc = pb->geqs[Le].coef[i];
4322
4323               if (dump_file && (dump_flags & TDF_DETAILS))
4324                 fprintf (dump_file, "an inplace elimination\n");
4325
4326               omega_copy_eqn (lbeqn, &pb->geqs[Le], (n_vars + 1));
4327               omega_delete_geq_extra (pb, Le, n_vars + 1);
4328
4329               for (Ue = pb->num_geqs - 1; Ue >= 0; Ue--)
4330                 if (pb->geqs[Ue].coef[i] < 0)
4331                   {
4332                     if (lbeqn->key == -pb->geqs[Ue].key)
4333                       omega_delete_geq_extra (pb, Ue, n_vars + 1);
4334                     else
4335                       {
4336                         int k;
4337                         int Uc = -pb->geqs[Ue].coef[i];
4338                         pb->geqs[Ue].touched = 1;
4339                         eliminate_again = false;
4340
4341                         if (lbeqn->color == omega_red)
4342                           pb->geqs[Ue].color = omega_red;
4343
4344                         for (k = 0; k <= n_vars; k++)
4345                           pb->geqs[Ue].coef[k] =
4346                             check_mul (pb->geqs[Ue].coef[k], Lc) +
4347                             check_mul (lbeqn->coef[k], Uc);
4348
4349                         if (dump_file && (dump_flags & TDF_DETAILS))
4350                           {
4351                             omega_print_geq (dump_file, pb,
4352                                              &(pb->geqs[Ue]));
4353                             fprintf (dump_file, "\n");
4354                           }
4355                       }
4356                   }
4357
4358               omega_free_eqns (lbeqn, 1);
4359               continue;
4360             }
4361           else
4362             {
4363               int *dead_eqns = XNEWVEC (int, OMEGA_MAX_GEQS);
4364               bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
4365               int num_dead = 0;
4366               int top_eqn = pb->num_geqs - 1;
4367               lower_bound_count--;
4368
4369               if (dump_file && (dump_flags & TDF_DETAILS))
4370                 fprintf (dump_file, "lower bound count = %d\n",
4371                          lower_bound_count);
4372
4373               for (Le = top_eqn; Le >= 0; Le--)
4374                 if (pb->geqs[Le].coef[i] > 0)
4375                   {
4376                     int Lc = pb->geqs[Le].coef[i];
4377                     for (Ue = top_eqn; Ue >= 0; Ue--)
4378                       if (pb->geqs[Ue].coef[i] < 0)
4379                         {
4380                           if (pb->geqs[Le].key != -pb->geqs[Ue].key)
4381                             {
4382                               int k;
4383                               int Uc = -pb->geqs[Ue].coef[i];
4384
4385                               if (num_dead == 0)
4386                                 e2 = pb->num_geqs++;
4387                               else
4388                                 e2 = dead_eqns[--num_dead];
4389
4390                               gcc_assert (e2 < OMEGA_MAX_GEQS);
4391
4392                               if (dump_file && (dump_flags & TDF_DETAILS))
4393                                 {
4394                                   fprintf (dump_file,
4395                                            "Le = %d, Ue = %d, gen = %d\n",
4396                                            Le, Ue, e2);
4397                                   omega_print_geq_extra (dump_file, pb,
4398                                                          &(pb->geqs[Le]));
4399                                   fprintf (dump_file, "\n");
4400                                   omega_print_geq_extra (dump_file, pb,
4401                                                          &(pb->geqs[Ue]));
4402                                   fprintf (dump_file, "\n");
4403                                 }
4404
4405                               eliminate_again = false;
4406
4407                               for (k = n_vars; k >= 0; k--)
4408                                 pb->geqs[e2].coef[k] =
4409                                   check_mul (pb->geqs[Ue].coef[k], Lc) +
4410                                   check_mul (pb->geqs[Le].coef[k], Uc);
4411
4412                               pb->geqs[e2].coef[n_vars + 1] = 0;
4413                               pb->geqs[e2].touched = 1;
4414
4415                               if (pb->geqs[Ue].color == omega_red
4416                                   || pb->geqs[Le].color == omega_red)
4417                                 pb->geqs[e2].color = omega_red;
4418                               else
4419                                 pb->geqs[e2].color = omega_black;
4420
4421                               if (dump_file && (dump_flags & TDF_DETAILS))
4422                                 {
4423                                   omega_print_geq (dump_file, pb,
4424                                                    &(pb->geqs[e2]));
4425                                   fprintf (dump_file, "\n");
4426                                 }
4427                             }
4428
4429                           if (lower_bound_count == 0)
4430                             {
4431                               dead_eqns[num_dead++] = Ue;
4432
4433                               if (dump_file && (dump_flags & TDF_DETAILS))
4434                                 fprintf (dump_file, "Killed %d\n", Ue);
4435                             }
4436                         }
4437
4438                     lower_bound_count--;
4439                     dead_eqns[num_dead++] = Le;
4440
4441                     if (dump_file && (dump_flags & TDF_DETAILS))
4442                       fprintf (dump_file, "Killed %d\n", Le);
4443                   }
4444
4445               for (e = pb->num_geqs - 1; e >= 0; e--)
4446                 is_dead[e] = false;
4447
4448               while (num_dead > 0)
4449                 is_dead[dead_eqns[--num_dead]] = true;
4450
4451               for (e = pb->num_geqs - 1; e >= 0; e--)
4452                 if (is_dead[e])
4453                   omega_delete_geq_extra (pb, e, n_vars + 1);
4454
4455               free (dead_eqns);
4456               free (is_dead);
4457               continue;
4458             }
4459         }
4460       else
4461         {
4462           omega_pb rS, iS;
4463
4464           rS = omega_alloc_problem (0, 0);
4465           iS = omega_alloc_problem (0, 0);
4466           e2 = 0;
4467           possible_easy_int_solution = true;
4468
4469           for (e = 0; e < pb->num_geqs; e++)
4470             if (pb->geqs[e].coef[i] == 0)
4471               {
4472                 omega_copy_eqn (&(rS->geqs[e2]), &pb->geqs[e],
4473                                 pb->num_vars);
4474                 omega_copy_eqn (&(iS->geqs[e2]), &pb->geqs[e],
4475                                 pb->num_vars);
4476
4477                 if (dump_file && (dump_flags & TDF_DETAILS))
4478                   {
4479                     int t;
4480                     fprintf (dump_file, "Copying (%d, %d): ", i,
4481                              pb->geqs[e].coef[i]);
4482                     omega_print_geq_extra (dump_file, pb, &pb->geqs[e]);
4483                     fprintf (dump_file, "\n");
4484                     for (t = 0; t <= n_vars + 1; t++)
4485                       fprintf (dump_file, "%d ", pb->geqs[e].coef[t]);
4486                     fprintf (dump_file, "\n");
4487
4488                   }
4489                 e2++;
4490                 gcc_assert (e2 < OMEGA_MAX_GEQS);
4491               }
4492
4493           for (Le = pb->num_geqs - 1; Le >= 0; Le--)
4494             if (pb->geqs[Le].coef[i] > 0)
4495               for (Ue = pb->num_geqs - 1; Ue >= 0; Ue--)
4496                 if (pb->geqs[Ue].coef[i] < 0)
4497                   {
4498                     int k;
4499                     int Lc = pb->geqs[Le].coef[i];
4500                     int Uc = -pb->geqs[Ue].coef[i];
4501
4502                     if (pb->geqs[Le].key != -pb->geqs[Ue].key)
4503                       {
4504
4505                         rS->geqs[e2].touched = iS->geqs[e2].touched = 1;
4506
4507                         if (dump_file && (dump_flags & TDF_DETAILS))
4508                           {
4509                             fprintf (dump_file, "---\n");
4510                             fprintf (dump_file,
4511                                      "Le(Lc) = %d(%d_, Ue(Uc) = %d(%d), gen = %d\n",
4512                                      Le, Lc, Ue, Uc, e2);
4513                             omega_print_geq_extra (dump_file, pb, &pb->geqs[Le]);
4514                             fprintf (dump_file, "\n");
4515                             omega_print_geq_extra (dump_file, pb, &pb->geqs[Ue]);
4516                             fprintf (dump_file, "\n");
4517                           }
4518
4519                         if (Uc == Lc)
4520                           {
4521                             for (k = n_vars; k >= 0; k--)
4522                               iS->geqs[e2].coef[k] = rS->geqs[e2].coef[k] =
4523                                 pb->geqs[Ue].coef[k] + pb->geqs[Le].coef[k];
4524
4525                             iS->geqs[e2].coef[0] -= (Uc - 1);
4526                           }
4527                         else
4528                           {
4529                             for (k = n_vars; k >= 0; k--)
4530                               iS->geqs[e2].coef[k] = rS->geqs[e2].coef[k] =
4531                                 check_mul (pb->geqs[Ue].coef[k], Lc) +
4532                                 check_mul (pb->geqs[Le].coef[k], Uc);
4533
4534                             iS->geqs[e2].coef[0] -= (Uc - 1) * (Lc - 1);
4535                           }
4536
4537                         if (pb->geqs[Ue].color == omega_red
4538                             || pb->geqs[Le].color == omega_red)
4539                           iS->geqs[e2].color = rS->geqs[e2].color = omega_red;
4540                         else
4541                           iS->geqs[e2].color = rS->geqs[e2].color = omega_black;
4542
4543                         if (dump_file && (dump_flags & TDF_DETAILS))
4544                           {
4545                             omega_print_geq (dump_file, pb, &(rS->geqs[e2]));
4546                             fprintf (dump_file, "\n");
4547                           }
4548
4549                         e2++;
4550                         gcc_assert (e2 < OMEGA_MAX_GEQS);
4551                       }
4552                     else if (pb->geqs[Ue].coef[0] * Lc +
4553                              pb->geqs[Le].coef[0] * Uc -
4554                              (Uc - 1) * (Lc - 1) < 0)
4555                       possible_easy_int_solution = false;
4556                   }
4557
4558           iS->variables_initialized = rS->variables_initialized = true;
4559           iS->num_vars = rS->num_vars = pb->num_vars;
4560           iS->num_geqs = rS->num_geqs = e2;
4561           iS->num_eqs = rS->num_eqs = 0;
4562           iS->num_subs = rS->num_subs = pb->num_subs;
4563           iS->safe_vars = rS->safe_vars = pb->safe_vars;
4564
4565           for (e = n_vars; e >= 0; e--)
4566             rS->var[e] = pb->var[e];
4567
4568           for (e = n_vars; e >= 0; e--)
4569             iS->var[e] = pb->var[e];
4570
4571           for (e = pb->num_subs - 1; e >= 0; e--)
4572             {
4573               omega_copy_eqn (&(rS->subs[e]), &(pb->subs[e]), pb->num_vars);
4574               omega_copy_eqn (&(iS->subs[e]), &(pb->subs[e]), pb->num_vars);
4575             }
4576
4577           pb->num_vars++;
4578           n_vars = pb->num_vars;
4579
4580           if (desired_res != omega_true)
4581             {
4582               if (original_problem == no_problem)
4583                 {
4584                   original_problem = pb;
4585                   result = omega_solve_geq (rS, omega_false);
4586                   original_problem = no_problem;
4587                 }
4588               else
4589                 result = omega_solve_geq (rS, omega_false);
4590
4591               if (result == omega_false)
4592                 {
4593                   free (rS);
4594                   free (iS);
4595                   return result;
4596                 }
4597
4598               if (pb->num_eqs > 0)
4599                 {
4600                   /* An equality constraint must have been found */
4601                   free (rS);
4602                   free (iS);
4603                   return omega_solve_problem (pb, desired_res);
4604                 }
4605             }
4606
4607           if (desired_res != omega_false)
4608             {
4609               int j;
4610               int lower_bounds = 0;
4611               int *lower_bound = XNEWVEC (int, OMEGA_MAX_GEQS);
4612
4613               if (possible_easy_int_solution)
4614                 {
4615                   conservative++;
4616                   result = omega_solve_geq (iS, desired_res);
4617                   conservative--;
4618
4619                   if (result != omega_false)
4620                     {
4621                       free (rS);
4622                       free (iS);
4623                       free (lower_bound);
4624                       return result;
4625                     }
4626                 }
4627
4628               if (!exact && best_parallel_eqn >= 0
4629                   && parallel_difference <= max_splinters)
4630                 {
4631                   free (rS);
4632                   free (iS);
4633                   free (lower_bound);
4634                   return parallel_splinter (pb, best_parallel_eqn,
4635                                             parallel_difference,
4636                                             desired_res);
4637                 }
4638
4639               if (dump_file && (dump_flags & TDF_DETAILS))
4640                 fprintf (dump_file, "have to do exact analysis\n");
4641
4642               conservative++;
4643
4644               for (e = 0; e < pb->num_geqs; e++)
4645                 if (pb->geqs[e].coef[i] > 1)
4646                   lower_bound[lower_bounds++] = e;
4647
4648               /* Sort array LOWER_BOUND.  */
4649               for (j = 0; j < lower_bounds; j++)
4650                 {
4651                   int k, smallest = j;
4652
4653                   for (k = j + 1; k < lower_bounds; k++)
4654                     if (pb->geqs[lower_bound[smallest]].coef[i] >
4655                         pb->geqs[lower_bound[k]].coef[i])
4656                       smallest = k;
4657
4658                   k = lower_bound[smallest];
4659                   lower_bound[smallest] = lower_bound[j];
4660                   lower_bound[j] = k;
4661                 }
4662
4663               if (dump_file && (dump_flags & TDF_DETAILS))
4664                 {
4665                   fprintf (dump_file, "lower bound coefficients = ");
4666
4667                   for (j = 0; j < lower_bounds; j++)
4668                     fprintf (dump_file, " %d",
4669                              pb->geqs[lower_bound[j]].coef[i]);
4670
4671                   fprintf (dump_file, "\n");
4672                 }
4673
4674               for (j = 0; j < lower_bounds; j++)
4675                 {
4676                   int max_incr;
4677                   int c;
4678                   int worst_lower_bound_constant = -minC;
4679
4680                   e = lower_bound[j];
4681                   max_incr = (((pb->geqs[e].coef[i] - 1) *
4682                                (worst_lower_bound_constant - 1) - 1)
4683                               / worst_lower_bound_constant);
4684                   /* max_incr += 2; */
4685
4686                   if (dump_file && (dump_flags & TDF_DETAILS))
4687                     {
4688                       fprintf (dump_file, "for equation ");
4689                       omega_print_geq (dump_file, pb, &pb->geqs[e]);
4690                       fprintf (dump_file,
4691                                "\ntry decrements from 0 to %d\n",
4692                                max_incr);
4693                       omega_print_problem (dump_file, pb);
4694                     }
4695
4696                   if (max_incr > 50 && !smoothed
4697                       && smooth_weird_equations (pb))
4698                     {
4699                       conservative--;
4700                       free (rS);
4701                       free (iS);
4702                       smoothed = true;
4703                       goto solve_geq_start;
4704                     }
4705
4706                   omega_copy_eqn (&pb->eqs[0], &pb->geqs[e],
4707                                   pb->num_vars);
4708                   pb->eqs[0].color = omega_black;
4709                   omega_init_eqn_zero (&pb->geqs[e], pb->num_vars);
4710                   pb->geqs[e].touched = 1;
4711                   pb->num_eqs = 1;
4712
4713                   for (c = max_incr; c >= 0; c--)
4714                     {
4715                       if (dump_file && (dump_flags & TDF_DETAILS))
4716                         {
4717                           fprintf (dump_file,
4718                                    "trying next decrement of %d\n",
4719                                    max_incr - c);
4720                           omega_print_problem (dump_file, pb);
4721                         }
4722
4723                       omega_copy_problem (rS, pb);
4724
4725                       if (dump_file && (dump_flags & TDF_DETAILS))
4726                         omega_print_problem (dump_file, rS);
4727
4728                       result = omega_solve_problem (rS, desired_res);
4729
4730                       if (result == omega_true)
4731                         {
4732                           free (rS);
4733                           free (iS);
4734                           free (lower_bound);
4735                           conservative--;
4736                           return omega_true;
4737                         }
4738
4739                       pb->eqs[0].coef[0]--;
4740                     }
4741
4742                   if (j + 1 < lower_bounds)
4743                     {
4744                       pb->num_eqs = 0;
4745                       omega_copy_eqn (&pb->geqs[e], &pb->eqs[0],
4746                                       pb->num_vars);
4747                       pb->geqs[e].touched = 1;
4748                       pb->geqs[e].color = omega_black;
4749                       omega_copy_problem (rS, pb);
4750
4751                       if (dump_file && (dump_flags & TDF_DETAILS))
4752                         fprintf (dump_file,
4753                                  "exhausted lower bound, "
4754                                  "checking if still feasible ");
4755
4756                       result = omega_solve_problem (rS, omega_false);
4757
4758                       if (result == omega_false)
4759                         break;
4760                     }
4761                 }
4762
4763               if (dump_file && (dump_flags & TDF_DETAILS))
4764                 fprintf (dump_file, "fall-off the end\n");
4765
4766               free (rS);
4767               free (iS);
4768               free (lower_bound);
4769               conservative--;
4770               return omega_false;
4771             }
4772
4773           free (rS);
4774           free (iS);
4775         }
4776       return omega_unknown;
4777     } while (eliminate_again);
4778   } while (1);
4779 }
4780
4781 /* Because the omega solver is recursive, this counter limits the
4782    recursion depth.  */
4783 static int omega_solve_depth = 0;
4784
4785 /* Return omega_true when the problem PB has a solution following the
4786    DESIRED_RES.  */
4787
4788 enum omega_result
4789 omega_solve_problem (omega_pb pb, enum omega_result desired_res)
4790 {
4791   enum omega_result result;
4792
4793   gcc_assert (pb->num_vars >= pb->safe_vars);
4794   omega_solve_depth++;
4795
4796   if (desired_res != omega_simplify)
4797     pb->safe_vars = 0;
4798
4799   if (omega_solve_depth > 50)
4800     {
4801       if (dump_file && (dump_flags & TDF_DETAILS))
4802         {
4803           fprintf (dump_file,
4804                    "Solve depth = %d, in_approximate_mode = %d, aborting\n",
4805                    omega_solve_depth, in_approximate_mode);
4806           omega_print_problem (dump_file, pb);
4807         }
4808       gcc_assert (0);
4809     }
4810
4811   if (omega_solve_eq (pb, desired_res) == omega_false)
4812     {
4813       omega_solve_depth--;
4814       return omega_false;
4815     }
4816
4817   if (in_approximate_mode && !pb->num_geqs)
4818     {
4819       result = omega_true;
4820       pb->num_vars = pb->safe_vars;
4821       omega_problem_reduced (pb);
4822     }
4823   else
4824     result = omega_solve_geq (pb, desired_res);
4825
4826   omega_solve_depth--;
4827
4828   if (!omega_reduce_with_subs)
4829     {
4830       resurrect_subs (pb);
4831       gcc_assert (please_no_equalities_in_simplified_problems
4832                   || !result || pb->num_subs == 0);
4833     }
4834
4835   return result;
4836 }
4837
4838 /* Return true if red equations constrain the set of possible solutions.
4839    We assume that there are solutions to the black equations by
4840    themselves, so if there is no solution to the combined problem, we
4841    return true.  */
4842
4843 bool
4844 omega_problem_has_red_equations (omega_pb pb)
4845 {
4846   bool result;
4847   int e;
4848   int i;
4849
4850   if (dump_file && (dump_flags & TDF_DETAILS))
4851     {
4852       fprintf (dump_file, "Checking for red equations:\n");
4853       omega_print_problem (dump_file, pb);
4854     }
4855
4856   please_no_equalities_in_simplified_problems++;
4857   may_be_red++;
4858
4859   if (omega_single_result)
4860     return_single_result++;
4861
4862   create_color = true;
4863   result = (omega_simplify_problem (pb) == omega_false);
4864
4865   if (omega_single_result)
4866     return_single_result--;
4867
4868   may_be_red--;
4869   please_no_equalities_in_simplified_problems--;
4870
4871   if (result)
4872     {
4873       if (dump_file && (dump_flags & TDF_DETAILS))
4874         fprintf (dump_file, "Gist is FALSE\n");
4875
4876       pb->num_subs = 0;
4877       pb->num_geqs = 0;
4878       pb->num_eqs = 1;
4879       pb->eqs[0].color = omega_red;
4880
4881       for (i = pb->num_vars; i > 0; i--)
4882         pb->eqs[0].coef[i] = 0;
4883
4884       pb->eqs[0].coef[0] = 1;
4885       return true;
4886     }
4887
4888   free_red_eliminations (pb);
4889   gcc_assert (pb->num_eqs == 0);
4890
4891   for (e = pb->num_geqs - 1; e >= 0; e--)
4892     if (pb->geqs[e].color == omega_red)
4893       result = true;
4894
4895   if (!result)
4896     return false;
4897
4898   for (i = pb->safe_vars; i >= 1; i--)
4899     {
4900       int ub = 0;
4901       int lb = 0;
4902
4903       for (e = pb->num_geqs - 1; e >= 0; e--)
4904         {
4905           if (pb->geqs[e].coef[i])
4906             {
4907               if (pb->geqs[e].coef[i] > 0)
4908                 lb |= (1 + (pb->geqs[e].color == omega_red ? 1 : 0));
4909
4910               else
4911                 ub |= (1 + (pb->geqs[e].color == omega_red ? 1 : 0));
4912             }
4913         }
4914
4915       if (ub == 2 || lb == 2)
4916         {
4917
4918           if (dump_file && (dump_flags & TDF_DETAILS))
4919             fprintf (dump_file, "checks for upper/lower bounds worked!\n");
4920
4921           if (!omega_reduce_with_subs)
4922             {
4923               resurrect_subs (pb);
4924               gcc_assert (pb->num_subs == 0);
4925             }
4926
4927           return true;
4928         }
4929     }
4930
4931
4932   if (dump_file && (dump_flags & TDF_DETAILS))
4933     fprintf (dump_file,
4934              "*** Doing potentially expensive elimination tests "
4935              "for red equations\n");
4936
4937   please_no_equalities_in_simplified_problems++;
4938   omega_eliminate_red (pb, true);
4939   please_no_equalities_in_simplified_problems--;
4940
4941   result = false;
4942   gcc_assert (pb->num_eqs == 0);
4943
4944   for (e = pb->num_geqs - 1; e >= 0; e--)
4945     if (pb->geqs[e].color == omega_red)
4946       result = true;
4947
4948   if (dump_file && (dump_flags & TDF_DETAILS))
4949     {
4950       if (!result)
4951         fprintf (dump_file,
4952                  "******************** Redundant Red Equations eliminated!!\n");
4953       else
4954         fprintf (dump_file,
4955                  "******************** Red Equations remain\n");
4956
4957       omega_print_problem (dump_file, pb);
4958     }
4959
4960   if (!omega_reduce_with_subs)
4961     {
4962       normalize_return_type r;
4963
4964       resurrect_subs (pb);
4965       r = normalize_omega_problem (pb);
4966       gcc_assert (r != normalize_false);
4967
4968       coalesce (pb);
4969       cleanout_wildcards (pb);
4970       gcc_assert (pb->num_subs == 0);
4971     }
4972
4973   return result;
4974 }
4975
4976 /* Calls omega_simplify_problem in approximate mode.  */
4977
4978 enum omega_result
4979 omega_simplify_approximate (omega_pb pb)
4980 {
4981   enum omega_result result;
4982
4983   if (dump_file && (dump_flags & TDF_DETAILS))
4984     fprintf (dump_file, "(Entering approximate mode\n");
4985
4986   in_approximate_mode = true;
4987   result = omega_simplify_problem (pb);
4988   in_approximate_mode = false;
4989
4990   gcc_assert (pb->num_vars == pb->safe_vars);
4991   if (!omega_reduce_with_subs)
4992     gcc_assert (pb->num_subs == 0);
4993
4994   if (dump_file && (dump_flags & TDF_DETAILS))
4995     fprintf (dump_file, "Leaving approximate mode)\n");
4996
4997   return result;
4998 }
4999
5000
5001 /* Simplifies problem PB by eliminating redundant constraints and
5002    reducing the constraints system to a minimal form.  Returns
5003    omega_true when the problem was successfully reduced, omega_unknown
5004    when the solver is unable to determine an answer.  */
5005
5006 enum omega_result
5007 omega_simplify_problem (omega_pb pb)
5008 {
5009   int i;
5010
5011   omega_found_reduction = omega_false;
5012
5013   if (!pb->variables_initialized)
5014     omega_initialize_variables (pb);
5015
5016   if (next_key * 3 > MAX_KEYS)
5017     {
5018       int e;
5019
5020       hash_version++;
5021       next_key = OMEGA_MAX_VARS + 1;
5022
5023       for (e = pb->num_geqs - 1; e >= 0; e--)
5024         pb->geqs[e].touched = 1;
5025
5026       for (i = 0; i < HASH_TABLE_SIZE; i++)
5027         hash_master[i].touched = -1;
5028
5029       pb->hash_version = hash_version;
5030     }
5031
5032   else if (pb->hash_version != hash_version)
5033     {
5034       int e;
5035
5036       for (e = pb->num_geqs - 1; e >= 0; e--)
5037         pb->geqs[e].touched = 1;
5038
5039       pb->hash_version = hash_version;
5040     }
5041
5042   if (pb->num_vars > pb->num_eqs + 3 * pb->safe_vars)
5043     omega_free_eliminations (pb, pb->safe_vars);
5044
5045   if (!may_be_red && pb->num_subs == 0 && pb->safe_vars == 0)
5046     {
5047       omega_found_reduction = omega_solve_problem (pb, omega_unknown);
5048
5049       if (omega_found_reduction != omega_false
5050           && !return_single_result)
5051         {
5052           pb->num_geqs = 0;
5053           pb->num_eqs = 0;
5054           (*omega_when_reduced) (pb);
5055         }
5056
5057       return omega_found_reduction;
5058     }
5059
5060   omega_solve_problem (pb, omega_simplify);
5061
5062   if (omega_found_reduction != omega_false)
5063     {
5064       for (i = 1; omega_safe_var_p (pb, i); i++)
5065         pb->forwarding_address[pb->var[i]] = i;
5066
5067       for (i = 0; i < pb->num_subs; i++)
5068         pb->forwarding_address[pb->subs[i].key] = -i - 1;
5069     }
5070
5071   if (!omega_reduce_with_subs)
5072     gcc_assert (please_no_equalities_in_simplified_problems
5073                 || omega_found_reduction == omega_false
5074                 || pb->num_subs == 0);
5075
5076   return omega_found_reduction;
5077 }
5078
5079 /* Make variable VAR unprotected: it then can be eliminated.  */
5080
5081 void
5082 omega_unprotect_variable (omega_pb pb, int var)
5083 {
5084   int e, idx;
5085   idx = pb->forwarding_address[var];
5086
5087   if (idx < 0)
5088     {
5089       idx = -1 - idx;
5090       pb->num_subs--;
5091
5092       if (idx < pb->num_subs)
5093         {
5094           omega_copy_eqn (&pb->subs[idx], &pb->subs[pb->num_subs],
5095                           pb->num_vars);
5096           pb->forwarding_address[pb->subs[idx].key] = -idx - 1;
5097         }
5098     }
5099   else
5100     {
5101       int *bring_to_life = XNEWVEC (int, OMEGA_MAX_VARS);
5102       int e2;
5103
5104       for (e = pb->num_subs - 1; e >= 0; e--)
5105         bring_to_life[e] = (pb->subs[e].coef[idx] != 0);
5106
5107       for (e2 = pb->num_subs - 1; e2 >= 0; e2--)
5108         if (bring_to_life[e2])
5109           {
5110             pb->num_vars++;
5111             pb->safe_vars++;
5112
5113             if (pb->safe_vars < pb->num_vars)
5114               {
5115                 for (e = pb->num_geqs - 1; e >= 0; e--)
5116                   {
5117                     pb->geqs[e].coef[pb->num_vars] =
5118                       pb->geqs[e].coef[pb->safe_vars];
5119
5120                     pb->geqs[e].coef[pb->safe_vars] = 0;
5121                   }
5122
5123                 for (e = pb->num_eqs - 1; e >= 0; e--)
5124                   {
5125                     pb->eqs[e].coef[pb->num_vars] =
5126                       pb->eqs[e].coef[pb->safe_vars];
5127
5128                     pb->eqs[e].coef[pb->safe_vars] = 0;
5129                   }
5130
5131                 for (e = pb->num_subs - 1; e >= 0; e--)
5132                   {
5133                     pb->subs[e].coef[pb->num_vars] =
5134                       pb->subs[e].coef[pb->safe_vars];
5135
5136                     pb->subs[e].coef[pb->safe_vars] = 0;
5137                   }
5138
5139                 pb->var[pb->num_vars] = pb->var[pb->safe_vars];
5140                 pb->forwarding_address[pb->var[pb->num_vars]] =
5141                   pb->num_vars;
5142               }
5143             else
5144               {
5145                 for (e = pb->num_geqs - 1; e >= 0; e--)
5146                   pb->geqs[e].coef[pb->safe_vars] = 0;
5147
5148                 for (e = pb->num_eqs - 1; e >= 0; e--)
5149                   pb->eqs[e].coef[pb->safe_vars] = 0;
5150
5151                 for (e = pb->num_subs - 1; e >= 0; e--)
5152                   pb->subs[e].coef[pb->safe_vars] = 0;
5153               }
5154
5155             pb->var[pb->safe_vars] = pb->subs[e2].key;
5156             pb->forwarding_address[pb->subs[e2].key] = pb->safe_vars;
5157
5158             omega_copy_eqn (&(pb->eqs[pb->num_eqs]), &(pb->subs[e2]),
5159                             pb->num_vars);
5160             pb->eqs[pb->num_eqs++].coef[pb->safe_vars] = -1;
5161             gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5162
5163             if (e2 < pb->num_subs - 1)
5164               omega_copy_eqn (&(pb->subs[e2]), &(pb->subs[pb->num_subs - 1]),
5165                               pb->num_vars);
5166
5167             pb->num_subs--;
5168           }
5169
5170       omega_unprotect_1 (pb, &idx, NULL);
5171       free (bring_to_life);
5172     }
5173
5174   chain_unprotect (pb);
5175 }
5176
5177 /* Unprotects VAR and simplifies PB.  */
5178
5179 enum omega_result
5180 omega_constrain_variable_sign (omega_pb pb, enum omega_eqn_color color,
5181                                int var, int sign)
5182 {
5183   int n_vars = pb->num_vars;
5184   int e, j;
5185   int k = pb->forwarding_address[var];
5186
5187   if (k < 0)
5188     {
5189       k = -1 - k;
5190
5191       if (sign != 0)
5192         {
5193           e = pb->num_geqs++;
5194           omega_copy_eqn (&pb->geqs[e], &pb->subs[k], pb->num_vars);
5195
5196           for (j = 0; j <= n_vars; j++)
5197             pb->geqs[e].coef[j] *= sign;
5198
5199           pb->geqs[e].coef[0]--;
5200           pb->geqs[e].touched = 1;
5201           pb->geqs[e].color = color;
5202         }
5203       else
5204         {
5205           e = pb->num_eqs++;
5206           gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5207           omega_copy_eqn (&pb->eqs[e], &pb->subs[k], pb->num_vars);
5208           pb->eqs[e].color = color;
5209         }
5210     }
5211   else if (sign != 0)
5212     {
5213       e = pb->num_geqs++;
5214       omega_init_eqn_zero (&pb->geqs[e], pb->num_vars);
5215       pb->geqs[e].coef[k] = sign;
5216       pb->geqs[e].coef[0] = -1;
5217       pb->geqs[e].touched = 1;
5218       pb->geqs[e].color = color;
5219     }
5220   else
5221     {
5222       e = pb->num_eqs++;
5223       gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5224       omega_init_eqn_zero (&pb->eqs[e], pb->num_vars);
5225       pb->eqs[e].coef[k] = 1;
5226       pb->eqs[e].color = color;
5227     }
5228
5229   omega_unprotect_variable (pb, var);
5230   return omega_simplify_problem (pb);
5231 }
5232
5233 /* Add an equation "VAR = VALUE" with COLOR to PB.  */
5234
5235 void
5236 omega_constrain_variable_value (omega_pb pb, enum omega_eqn_color color,
5237                                 int var, int value)
5238 {
5239   int e;
5240   int k = pb->forwarding_address[var];
5241
5242   if (k < 0)
5243     {
5244       k = -1 - k;
5245       e = pb->num_eqs++;
5246       gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5247       omega_copy_eqn (&pb->eqs[e], &pb->subs[k], pb->num_vars);
5248       pb->eqs[e].coef[0] -= value;
5249     }
5250   else
5251     {
5252       e = pb->num_eqs++;
5253       omega_init_eqn_zero (&pb->eqs[e], pb->num_vars);
5254       pb->eqs[e].coef[k] = 1;
5255       pb->eqs[e].coef[0] = -value;
5256     }
5257
5258   pb->eqs[e].color = color;
5259 }
5260
5261 /* Return false when the upper and lower bounds are not coupled.
5262    Initialize the bounds LOWER_BOUND and UPPER_BOUND for the values of
5263    variable I.  */
5264
5265 bool
5266 omega_query_variable (omega_pb pb, int i, int *lower_bound, int *upper_bound)
5267 {
5268   int n_vars = pb->num_vars;
5269   int e, j;
5270   bool is_simple;
5271   bool coupled = false;
5272
5273   *lower_bound = neg_infinity;
5274   *upper_bound = pos_infinity;
5275   i = pb->forwarding_address[i];
5276
5277   if (i < 0)
5278     {
5279       i = -i - 1;
5280
5281       for (j = 1; j <= n_vars; j++)
5282         if (pb->subs[i].coef[j] != 0)
5283           return true;
5284
5285       *upper_bound = *lower_bound = pb->subs[i].coef[0];
5286       return false;
5287     }
5288
5289   for (e = pb->num_subs - 1; e >= 0; e--)
5290     if (pb->subs[e].coef[i] != 0)
5291       coupled = true;
5292
5293   for (e = pb->num_eqs - 1; e >= 0; e--)
5294     if (pb->eqs[e].coef[i] != 0)
5295       {
5296         is_simple = true;
5297
5298         for (j = 1; j <= n_vars; j++)
5299           if (i != j && pb->eqs[e].coef[j] != 0)
5300             {
5301               is_simple = false;
5302               coupled = true;
5303               break;
5304             }
5305
5306         if (!is_simple)
5307           continue;
5308         else
5309           {
5310             *lower_bound = *upper_bound =
5311               -pb->eqs[e].coef[i] * pb->eqs[e].coef[0];
5312             return false;
5313           }
5314       }
5315
5316   for (e = pb->num_geqs - 1; e >= 0; e--)
5317     if (pb->geqs[e].coef[i] != 0)
5318       {
5319         if (pb->geqs[e].key == i)
5320           *lower_bound = MAX (*lower_bound, -pb->geqs[e].coef[0]);
5321
5322         else if (pb->geqs[e].key == -i)
5323           *upper_bound = MIN (*upper_bound, pb->geqs[e].coef[0]);
5324
5325         else
5326           coupled = true;
5327       }
5328
5329   return coupled;
5330 }
5331
5332 /* Sets the lower bound L and upper bound U for the values of variable
5333    I, and sets COULD_BE_ZERO to true if variable I might take value
5334    zero.  LOWER_BOUND and UPPER_BOUND are bounds on the values of
5335    variable I.  */
5336
5337 static void
5338 query_coupled_variable (omega_pb pb, int i, int *l, int *u,
5339                         bool *could_be_zero, int lower_bound, int upper_bound)
5340 {
5341   int e, b1, b2;
5342   eqn eqn;
5343   int sign;
5344   int v;
5345
5346   /* Preconditions.  */
5347   gcc_assert (abs (pb->forwarding_address[i]) == 1
5348               && pb->num_vars + pb->num_subs == 2
5349               && pb->num_eqs + pb->num_subs == 1);
5350
5351   /* Define variable I in terms of variable V.  */
5352   if (pb->forwarding_address[i] == -1)
5353     {
5354       eqn = &pb->subs[0];
5355       sign = 1;
5356       v = 1;
5357     }
5358   else
5359     {
5360       eqn = &pb->eqs[0];
5361       sign = -eqn->coef[1];
5362       v = 2;
5363     }
5364
5365   for (e = pb->num_geqs - 1; e >= 0; e--)
5366     if (pb->geqs[e].coef[v] != 0)
5367       {
5368         if (pb->geqs[e].coef[v] == 1)
5369           lower_bound = MAX (lower_bound, -pb->geqs[e].coef[0]);
5370
5371         else
5372           upper_bound = MIN (upper_bound, pb->geqs[e].coef[0]);
5373       }
5374
5375   if (lower_bound > upper_bound)
5376     {
5377       *l = pos_infinity;
5378       *u = neg_infinity;
5379       *could_be_zero = 0;
5380       return;
5381     }
5382
5383   if (lower_bound == neg_infinity)
5384     {
5385       if (eqn->coef[v] > 0)
5386         b1 = sign * neg_infinity;
5387
5388       else
5389         b1 = -sign * neg_infinity;
5390     }
5391   else
5392     b1 = sign * (eqn->coef[0] + eqn->coef[v] * lower_bound);
5393
5394   if (upper_bound == pos_infinity)
5395     {
5396       if (eqn->coef[v] > 0)
5397         b2 = sign * pos_infinity;
5398
5399       else
5400         b2 = -sign * pos_infinity;
5401     }
5402   else
5403     b2 = sign * (eqn->coef[0] + eqn->coef[v] * upper_bound);
5404
5405   *l = MAX (*l, b1 <= b2 ? b1 : b2);
5406   *u = MIN (*u, b1 <= b2 ? b2 : b1);
5407
5408   *could_be_zero = (*l <= 0 && 0 <= *u
5409                     && int_mod (eqn->coef[0], abs (eqn->coef[v])) == 0);
5410 }
5411
5412 /* Return false when a lower bound L and an upper bound U for variable
5413    I in problem PB have been initialized.  */
5414
5415 bool
5416 omega_query_variable_bounds (omega_pb pb, int i, int *l, int *u)
5417 {
5418   *l = neg_infinity;
5419   *u = pos_infinity;
5420
5421   if (!omega_query_variable (pb, i, l, u)
5422       || (pb->num_vars == 1 && pb->forwarding_address[i] == 1))
5423     return false;
5424
5425   if (abs (pb->forwarding_address[i]) == 1
5426       && pb->num_vars + pb->num_subs == 2
5427       && pb->num_eqs + pb->num_subs == 1)
5428     {
5429       bool could_be_zero;
5430       query_coupled_variable (pb, i, l, u, &could_be_zero, neg_infinity,
5431                               pos_infinity);
5432       return false;
5433     }
5434
5435   return true;
5436 }
5437
5438 /* For problem PB, return an integer that represents the classic data
5439    dependence direction in function of the DD_LT, DD_EQ and DD_GT bit
5440    masks that are added to the result.  When DIST_KNOWN is true, DIST
5441    is set to the classic data dependence distance.  LOWER_BOUND and
5442    UPPER_BOUND are bounds on the value of variable I, for example, it
5443    is possible to narrow the iteration domain with safe approximations
5444    of loop counts, and thus discard some data dependences that cannot
5445    occur.  */
5446
5447 int
5448 omega_query_variable_signs (omega_pb pb, int i, int dd_lt,
5449                             int dd_eq, int dd_gt, int lower_bound,
5450                             int upper_bound, bool *dist_known, int *dist)
5451 {
5452   int result;
5453   int l, u;
5454   bool could_be_zero;
5455
5456   l = neg_infinity;
5457   u = pos_infinity;
5458
5459   omega_query_variable (pb, i, &l, &u);
5460   query_coupled_variable (pb, i, &l, &u, &could_be_zero, lower_bound,
5461                           upper_bound);
5462   result = 0;
5463
5464   if (l < 0)
5465     result |= dd_gt;
5466
5467   if (u > 0)
5468     result |= dd_lt;
5469
5470   if (could_be_zero)
5471     result |= dd_eq;
5472
5473   if (l == u)
5474     {
5475       *dist_known = true;
5476       *dist = l;
5477     }
5478   else
5479     *dist_known = false;
5480
5481   return result;
5482 }
5483
5484 /* Initialize PB as an Omega problem with NVARS variables and NPROT
5485    safe variables.  Safe variables are not eliminated during the
5486    Fourier-Motzkin elimination.  Safe variables are all those
5487    variables that are placed at the beginning of the array of
5488    variables: P->var[0, ..., NPROT - 1].  */
5489
5490 omega_pb
5491 omega_alloc_problem (int nvars, int nprot)
5492 {
5493   omega_pb pb;
5494
5495   gcc_assert (nvars <= OMEGA_MAX_VARS);
5496   omega_initialize ();
5497
5498   /* Allocate and initialize PB.  */
5499   pb = XCNEW (struct omega_pb_d);
5500   pb->var = XCNEWVEC (int, OMEGA_MAX_VARS + 2);
5501   pb->forwarding_address = XCNEWVEC (int, OMEGA_MAX_VARS + 2);
5502   pb->geqs = omega_alloc_eqns (0, OMEGA_MAX_GEQS);
5503   pb->eqs = omega_alloc_eqns (0, OMEGA_MAX_EQS);
5504   pb->subs = omega_alloc_eqns (0, OMEGA_MAX_VARS + 1);
5505
5506   pb->hash_version = hash_version;
5507   pb->num_vars = nvars;
5508   pb->safe_vars = nprot;
5509   pb->variables_initialized = false;
5510   pb->variables_freed = false;
5511   pb->num_eqs = 0;
5512   pb->num_geqs = 0;
5513   pb->num_subs = 0;
5514   return pb;
5515 }
5516
5517 /* Keeps the state of the initialization.  */
5518 static bool omega_initialized = false;
5519
5520 /* Initialization of the Omega solver.  */
5521
5522 void
5523 omega_initialize (void)
5524 {
5525   int i;
5526
5527   if (omega_initialized)
5528     return;
5529
5530   next_wild_card = 0;
5531   next_key = OMEGA_MAX_VARS + 1;
5532   packing = XCNEWVEC (int, OMEGA_MAX_VARS);
5533   fast_lookup = XCNEWVEC (int, MAX_KEYS * 2);
5534   fast_lookup_red = XCNEWVEC (int, MAX_KEYS * 2);
5535   hash_master = omega_alloc_eqns (0, HASH_TABLE_SIZE);
5536
5537   for (i = 0; i < HASH_TABLE_SIZE; i++)
5538     hash_master[i].touched = -1;
5539
5540   sprintf (wild_name[0], "1");
5541   sprintf (wild_name[1], "a");
5542   sprintf (wild_name[2], "b");
5543   sprintf (wild_name[3], "c");
5544   sprintf (wild_name[4], "d");
5545   sprintf (wild_name[5], "e");
5546   sprintf (wild_name[6], "f");
5547   sprintf (wild_name[7], "g");
5548   sprintf (wild_name[8], "h");
5549   sprintf (wild_name[9], "i");
5550   sprintf (wild_name[10], "j");
5551   sprintf (wild_name[11], "k");
5552   sprintf (wild_name[12], "l");
5553   sprintf (wild_name[13], "m");
5554   sprintf (wild_name[14], "n");
5555   sprintf (wild_name[15], "o");
5556   sprintf (wild_name[16], "p");
5557   sprintf (wild_name[17], "q");
5558   sprintf (wild_name[18], "r");
5559   sprintf (wild_name[19], "s");
5560   sprintf (wild_name[20], "t");
5561   sprintf (wild_name[40 - 1], "alpha");
5562   sprintf (wild_name[40 - 2], "beta");
5563   sprintf (wild_name[40 - 3], "gamma");
5564   sprintf (wild_name[40 - 4], "delta");
5565   sprintf (wild_name[40 - 5], "tau");
5566   sprintf (wild_name[40 - 6], "sigma");
5567   sprintf (wild_name[40 - 7], "chi");
5568   sprintf (wild_name[40 - 8], "omega");
5569   sprintf (wild_name[40 - 9], "pi");
5570   sprintf (wild_name[40 - 10], "ni");
5571   sprintf (wild_name[40 - 11], "Alpha");
5572   sprintf (wild_name[40 - 12], "Beta");
5573   sprintf (wild_name[40 - 13], "Gamma");
5574   sprintf (wild_name[40 - 14], "Delta");
5575   sprintf (wild_name[40 - 15], "Tau");
5576   sprintf (wild_name[40 - 16], "Sigma");
5577   sprintf (wild_name[40 - 17], "Chi");
5578   sprintf (wild_name[40 - 18], "Omega");
5579   sprintf (wild_name[40 - 19], "xxx");
5580
5581   omega_initialized = true;
5582 }