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