gcc/omega.c

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