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 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 "errors.h"
  39 #include "ggc.h"
  40 #include "tree.h"
  41 #include "diagnostic.h"
  42 #include "varray.h"
  43 #include "tree-pass.h"
  44 #include "omega.h"
  45
  46 /* When set to true, keep substitution variables.  When set to false,
  47    resurrect substitution variables (convert substitutions back to EQs).  */
  48 static bool omega_reduce_with_subs = true;
  49
  50 /* When set to true, omega_simplify_problem checks for problem with no
  51    solutions, calling verify_omega_pb.  */
  52 static bool omega_verify_simplification = false;
  53
  54 /* When set to true, only produce a single simplified result.  */
  55 static bool omega_single_result = false;
  56
  57 /* Set return_single_result to 1 when omega_single_result is true.  */
  58 static int return_single_result = 0;
  59
  60 /* Hash table for equations generated by the solver.  */
  61 #define HASH_TABLE_SIZE PARAM_VALUE (PARAM_OMEGA_HASH_TABLE_SIZE)
  62 #define MAX_KEYS PARAM_VALUE (PARAM_OMEGA_MAX_KEYS)
  63 static eqn hash_master;
  64 static int next_key;
  65 static int hash_version = 0;
  66
  67 /* Set to true for making the solver enter in approximation mode.  */
  68 static bool in_approximate_mode = false;
  69
  70 /* When set to zero, the solver is allowed to add new equalities to
  71    the problem to be solved.  */
  72 static int conservative = 0;
  73
  74 /* Set to omega_true when the problem was successfully reduced, set to
  75    omega_unknown when the solver is unable to determine an answer.  */
  76 static enum omega_result omega_found_reduction;
  77
  78 /* Set to true when the solver is allowed to add omega_red equations.  */
  79 static bool create_color = false;
  80
  81 /* Set to nonzero when the problem to be solved can be reduced.  */
  82 static int may_be_red = 0;
  83
  84 /* When false, there should be no substitution equations in the
  85    simplified problem.  */
  86 static int please_no_equalities_in_simplified_problems = 0;
  87
  88 /* Variables names for pretty printing.  */
  89 static char wild_name[200][40];
  90
  91 /* Pointer to the void problem.  */
  92 static omega_pb no_problem = (omega_pb) 0;
  93
  94 /* Pointer to the problem to be solved.  */
  95 static omega_pb original_problem = (omega_pb) 0;
  96
  97
  98 /* Return the integer A divided by B.  */
  99
 100 static inline int
 101 int_div (int a, int b)
 102 {
 103   if (a > 0)
 104     return a/b;
 105   else
 106     return -((-a + b - 1)/b);
 107 }
 108
 109 /* Return the integer A modulo B.  */
 110
 111 static inline int
 112 int_mod (int a, int b)
 113 {
 114   return a - b * int_div (a, b);
 115 }
 116
 117 /* For X and Y positive integers, return X multiplied by Y and check
 118    that the result does not overflow.  */
 119
 120 static inline int
 121 check_pos_mul (int x, int y)
 122 {
 123   if (x != 0)
 124     gcc_assert ((INT_MAX) / x > y);
 125
 126   return x * y;
 127 }
 128
 129 /* Return X multiplied by Y and check that the result does not
 130    overflow.  */
 131
 132 static inline int
 133 check_mul (int x, int y)
 134 {
 135   if (x >= 0)
 136     {
 137       if (y >= 0)
 138         return check_pos_mul (x, y);
 139       else
 140         return -check_pos_mul (x, -y);
 141     }
 142   else if (y >= 0)
 143     return -check_pos_mul (-x, y);
 144   else
 145     return check_pos_mul (-x, -y);
 146 }
 147
 148 /* Test whether equation E is red.  */
 149
 150 static inline bool
 151 omega_eqn_is_red (eqn e, int desired_res)
 152 {
 153   return (desired_res == omega_simplify && e->color == omega_red);
 154 }
 155
 156 /* Return a string for VARIABLE.  */
 157
 158 static inline char *
 159 omega_var_to_str (int variable)
 160 {
 161   if (0 <= variable && variable <= 20)
 162     return wild_name[variable];
 163
 164   if (-20 < variable && variable < 0)
 165     return wild_name[40 + variable];
 166
 167   /* Collapse all the entries that would have overflowed.  */
 168   return wild_name[21];
 169 }
 170
 171 /* Return a string for variable I in problem PB.  */
 172
 173 static inline char *
 174 omega_variable_to_str (omega_pb pb, int i)
 175 {
 176   return omega_var_to_str (pb->var[i]);
 177 }
 178
 179 /* Do nothing function: used for default initializations.  */
 180
 181 void
 182 omega_no_procedure (omega_pb pb ATTRIBUTE_UNUSED)
 183 {
 184 }
 185
 186 void (*omega_when_reduced) (omega_pb) = omega_no_procedure;
 187
 188 /* Compute the greatest common divisor of A and B.  */
 189
 190 static inline int
 191 gcd (int b, int a)
 192 {
 193   if (b == 1)
 194     return 1;
 195
 196   while (b != 0)
 197     {
 198       int t = b;
 199       b = a % b;
 200       a = t;
 201     }
 202
 203   return a;
 204 }
 205
 206 /* Print to FILE from PB equation E with all its coefficients
 207    multiplied by C.  */
 208
 209 static void
 210 omega_print_term (FILE *file, omega_pb pb, eqn e, int c)
 211 {
 212   int i;
 213   bool first = true;
 214   int n = pb->num_vars;
 215   int went_first = -1;
 216
 217   for (i = 1; i <= n; i++)
 218     if (c * e->coef[i] > 0)
 219       {
 220         first = false;
 221         went_first = i;
 222
 223         if (c * e->coef[i] == 1)
 224           fprintf (file, "%s", omega_variable_to_str (pb, i));
 225         else
 226           fprintf (file, "%d * %s", c * e->coef[i],
 227                    omega_variable_to_str (pb, i));
 228         break;
 229       }
 230
 231   for (i = 1; i <= n; i++)
 232     if (i != went_first && c * e->coef[i] != 0)
 233       {
 234         if (!first && c * e->coef[i] > 0)
 235           fprintf (file, " + ");
 236
 237         first = false;
 238
 239         if (c * e->coef[i] == 1)
 240           fprintf (file, "%s", omega_variable_to_str (pb, i));
 241         else if (c * e->coef[i] == -1)
 242           fprintf (file, " - %s", omega_variable_to_str (pb, i));
 243         else
 244           fprintf (file, "%d * %s", c * e->coef[i],
 245                    omega_variable_to_str (pb, i));
 246       }
 247
 248   if (!first && c * e->coef[0] > 0)
 249     fprintf (file, " + ");
 250
 251   if (first || c * e->coef[0] != 0)
 252     fprintf (file, "%d", c * e->coef[0]);
 253 }
 254
 255 /* Print to FILE the equation E of problem PB.  */
 256
 257 void
 258 omega_print_eqn (FILE *file, omega_pb pb, eqn e, bool test, int extra)
 259 {
 260   int i;
 261   int n = pb->num_vars + extra;
 262   bool is_lt = test && e->coef[0] == -1;
 263   bool first;
 264
 265   if (test)
 266     {
 267       if (e->touched)
 268         fprintf (file, "!");
 269
 270       else if (e->key != 0)
 271         fprintf (file, "%d: ", e->key);
 272     }
 273
 274   if (e->color == omega_red)
 275     fprintf (file, "[");
 276
 277   first = true;
 278
 279   for (i = is_lt ? 1 : 0; i <= n; i++)
 280     if (e->coef[i] < 0)
 281       {
 282         if (!first)
 283           fprintf (file, " + ");
 284         else
 285           first = false;
 286
 287         if (i == 0)
 288           fprintf (file, "%d", -e->coef[i]);
 289         else if (e->coef[i] == -1)
 290           fprintf (file, "%s", omega_variable_to_str (pb, i));
 291         else
 292           fprintf (file, "%d * %s", -e->coef[i],
 293                    omega_variable_to_str (pb, i));
 294       }
 295
 296   if (first)
 297     {
 298       if (is_lt)
 299         {
 300           fprintf (file, "1");
 301           is_lt = false;
 302         }
 303       else
 304         fprintf (file, "0");
 305     }
 306
 307   if (test == 0)
 308     fprintf (file, " = ");
 309   else if (is_lt)
 310     fprintf (file, " < ");
 311   else
 312     fprintf (file, " <= ");
 313
 314   first = true;
 315
 316   for (i = 0; i <= n; i++)
 317     if (e->coef[i] > 0)
 318       {
 319         if (!first)
 320           fprintf (file, " + ");
 321         else
 322           first = false;
 323
 324         if (i == 0)
 325           fprintf (file, "%d", e->coef[i]);
 326         else if (e->coef[i] == 1)
 327           fprintf (file, "%s", omega_variable_to_str (pb, i));
 328         else
 329           fprintf (file, "%d * %s", e->coef[i],
 330                    omega_variable_to_str (pb, i));
 331       }
 332
 333   if (first)
 334     fprintf (file, "0");
 335
 336   if (e->color == omega_red)
 337     fprintf (file, "]");
 338 }
 339
 340 /* Print to FILE all the variables of problem PB.  */
 341
 342 static void
 343 omega_print_vars (FILE *file, omega_pb pb)
 344 {
 345   int i;
 346
 347   fprintf (file, "variables = ");
 348
 349   if (pb->safe_vars > 0)
 350     fprintf (file, "protected (");
 351
 352   for (i = 1; i <= pb->num_vars; i++)
 353     {
 354       fprintf (file, "%s", omega_variable_to_str (pb, i));
 355
 356       if (i == pb->safe_vars)
 357         fprintf (file, ")");
 358
 359       if (i < pb->num_vars)
 360         fprintf (file, ", ");
 361     }
 362
 363   fprintf (file, "\n");
 364 }
 365
 366 /* Debug problem PB.  */
 367
 368 void
 369 debug_omega_problem (omega_pb pb)
 370 {
 371   omega_print_problem (stderr, pb);
 372 }
 373
 374 /* Print to FILE problem PB.  */
 375
 376 void
 377 omega_print_problem (FILE *file, omega_pb pb)
 378 {
 379   int e;
 380
 381   if (!pb->variables_initialized)
 382     omega_initialize_variables (pb);
 383
 384   omega_print_vars (file, pb);
 385
 386   for (e = 0; e < pb->num_eqs; e++)
 387     {
 388       omega_print_eq (file, pb, &pb->eqs[e]);
 389       fprintf (file, "\n");
 390     }
 391
 392   fprintf (file, "Done with EQ\n");
 393
 394   for (e = 0; e < pb->num_geqs; e++)
 395     {
 396       omega_print_geq (file, pb, &pb->geqs[e]);
 397       fprintf (file, "\n");
 398     }
 399
 400   fprintf (file, "Done with GEQ\n");
 401
 402   for (e = 0; e < pb->num_subs; e++)
 403     {
 404       eqn eq = &pb->subs[e];
 405
 406       if (eq->color == omega_red)
 407         fprintf (file, "[");
 408
 409       if (eq->key > 0)
 410         fprintf (file, "%s := ", omega_var_to_str (eq->key));
 411       else
 412         fprintf (file, "#%d := ", eq->key);
 413
 414       omega_print_term (file, pb, eq, 1);
 415
 416       if (eq->color == omega_red)
 417         fprintf (file, "]");
 418
 419       fprintf (file, "\n");
 420     }
 421 }
 422
 423 /* Return the number of equations in PB tagged omega_red.  */
 424
 425 int
 426 omega_count_red_equations (omega_pb pb)
 427 {
 428   int e, i;
 429   int result = 0;
 430
 431   for (e = 0; e < pb->num_eqs; e++)
 432     if (pb->eqs[e].color == omega_red)
 433       {
 434         for (i = pb->num_vars; i > 0; i--)
 435           if (pb->geqs[e].coef[i])
 436             break;
 437
 438         if (i == 0 && pb->geqs[e].coef[0] == 1)
 439           return 0;
 440         else
 441           result += 2;
 442       }
 443
 444   for (e = 0; e < pb->num_geqs; e++)
 445     if (pb->geqs[e].color == omega_red)
 446       result += 1;
 447
 448   for (e = 0; e < pb->num_subs; e++)
 449     if (pb->subs[e].color == omega_red)
 450       result += 2;
 451
 452   return result;
 453 }
 454
 455 /* Print to FILE all the equations in PB that are tagged omega_red.  */
 456
 457 void
 458 omega_print_red_equations (FILE *file, omega_pb pb)
 459 {
 460   int e;
 461
 462   if (!pb->variables_initialized)
 463     omega_initialize_variables (pb);
 464
 465   omega_print_vars (file, pb);
 466
 467   for (e = 0; e < pb->num_eqs; e++)
 468     if (pb->eqs[e].color == omega_red)
 469       {
 470         omega_print_eq (file, pb, &pb->eqs[e]);
 471         fprintf (file, "\n");
 472       }
 473
 474   for (e = 0; e < pb->num_geqs; e++)
 475     if (pb->geqs[e].color == omega_red)
 476       {
 477         omega_print_geq (file, pb, &pb->geqs[e]);
 478         fprintf (file, "\n");
 479       }
 480
 481   for (e = 0; e < pb->num_subs; e++)
 482     if (pb->subs[e].color == omega_red)
 483       {
 484         eqn eq = &pb->subs[e];
 485         fprintf (file, "[");
 486
 487         if (eq->key > 0)
 488           fprintf (file, "%s := ", omega_var_to_str (eq->key));
 489         else
 490           fprintf (file, "#%d := ", eq->key);
 491
 492         omega_print_term (file, pb, eq, 1);
 493         fprintf (file, "]\n");
 494       }
 495 }
 496
 497 /* Pretty print PB to FILE.  */
 498
 499 void
 500 omega_pretty_print_problem (FILE *file, omega_pb pb)
 501 {
 502   int e, v, v1, v2, v3, t;
 503   bool *live = XNEWVEC (bool, OMEGA_MAX_GEQS);
 504   int stuffPrinted = 0;
 505   bool change;
 506
 507   typedef enum {
 508     none, le, lt
 509   } partial_order_type;
 510
 511   partial_order_type **po = XNEWVEC (partial_order_type *,
 512                                      OMEGA_MAX_VARS * OMEGA_MAX_VARS);
 513   int **po_eq = XNEWVEC (int *, OMEGA_MAX_VARS * OMEGA_MAX_VARS);
 514   int *last_links = XNEWVEC (int, OMEGA_MAX_VARS);
 515   int *first_links = XNEWVEC (int, OMEGA_MAX_VARS);
 516   int *chain_length = XNEWVEC (int, OMEGA_MAX_VARS);
 517   int *chain = XNEWVEC (int, OMEGA_MAX_VARS);
 518   int i, m;
 519   bool multiprint;
 520
 521   if (!pb->variables_initialized)
 522     omega_initialize_variables (pb);
 523
 524   if (pb->num_vars > 0)
 525     {
 526       omega_eliminate_redundant (pb, false);
 527
 528       for (e = 0; e < pb->num_eqs; e++)
 529         {
 530           if (stuffPrinted)
 531             fprintf (file, "; ");
 532
 533           stuffPrinted = 1;
 534           omega_print_eq (file, pb, &pb->eqs[e]);
 535         }
 536
 537       for (e = 0; e < pb->num_geqs; e++)
 538         live[e] = true;
 539
 540       while (1)
 541         {
 542           for (v = 1; v <= pb->num_vars; v++)
 543             {
 544               last_links[v] = first_links[v] = 0;
 545               chain_length[v] = 0;
 546
 547               for (v2 = 1; v2 <= pb->num_vars; v2++)
 548                 po[v][v2] = none;
 549             }
 550
 551           for (e = 0; e < pb->num_geqs; e++)
 552             if (live[e])
 553               {
 554                 for (v = 1; v <= pb->num_vars; v++)
 555                   if (pb->geqs[e].coef[v] == 1)
 556                     first_links[v]++;
 557                   else if (pb->geqs[e].coef[v] == -1)
 558                     last_links[v]++;
 559
 560                 v1 = pb->num_vars;
 561
 562                 while (v1 > 0 && pb->geqs[e].coef[v1] == 0)
 563                   v1--;
 564
 565                 v2 = v1 - 1;
 566
 567                 while (v2 > 0 && pb->geqs[e].coef[v2] == 0)
 568                   v2--;
 569
 570                 v3 = v2 - 1;
 571
 572                 while (v3 > 0 && pb->geqs[e].coef[v3] == 0)
 573                   v3--;
 574
 575                 if (pb->geqs[e].coef[0] > 0 || pb->geqs[e].coef[0] < -1
 576                     || v2 <= 0 || v3 > 0
 577                     || pb->geqs[e].coef[v1] * pb->geqs[e].coef[v2] != -1)
 578                   {
 579                     /* Not a partial order relation.  */
 580                   }
 581                 else
 582                   {
 583                     if (pb->geqs[e].coef[v1] == 1)
 584                       {
 585                         v3 = v2;
 586                         v2 = v1;
 587                         v1 = v3;
 588                       }
 589
 590                     /* Relation is v1 <= v2 or v1 < v2.  */
 591                     po[v1][v2] = ((pb->geqs[e].coef[0] == 0) ? le : lt);
 592                     po_eq[v1][v2] = e;
 593                   }
 594               }
 595           for (v = 1; v <= pb->num_vars; v++)
 596             chain_length[v] = last_links[v];
 597
 598           /* Just in case pb->num_vars <= 0.  */
 599           change = false;
 600           for (t = 0; t < pb->num_vars; t++)
 601             {
 602               change = false;
 603
 604               for (v1 = 1; v1 <= pb->num_vars; v1++)
 605                 for (v2 = 1; v2 <= pb->num_vars; v2++)
 606                   if (po[v1][v2] != none &&
 607                       chain_length[v1] <= chain_length[v2])
 608                     {
 609                       chain_length[v1] = chain_length[v2] + 1;
 610                       change = true;
 611                     }
 612             }
 613
 614           /* Caught in cycle.  */
 615           gcc_assert (!change);
 616
 617           for (v1 = 1; v1 <= pb->num_vars; v1++)
 618             if (chain_length[v1] == 0)
 619               first_links[v1] = 0;
 620
 621           v = 1;
 622
 623           for (v1 = 2; v1 <= pb->num_vars; v1++)
 624             if (chain_length[v1] + first_links[v1] >
 625                 chain_length[v] + first_links[v])
 626               v = v1;
 627
 628           if (chain_length[v] + first_links[v] == 0)
 629             break;
 630
 631           if (stuffPrinted)
 632             fprintf (file, "; ");
 633
 634           stuffPrinted = 1;
 635
 636           /* Chain starts at v. */
 637           {
 638             int tmp;
 639             bool first = true;
 640
 641             for (e = 0; e < pb->num_geqs; e++)
 642               if (live[e] && pb->geqs[e].coef[v] == 1)
 643                 {
 644                   if (!first)
 645                     fprintf (file, ", ");
 646
 647                   tmp = pb->geqs[e].coef[v];
 648                   pb->geqs[e].coef[v] = 0;
 649                   omega_print_term (file, pb, &pb->geqs[e], -1);
 650                   pb->geqs[e].coef[v] = tmp;
 651                   live[e] = false;
 652                   first = false;
 653                 }
 654
 655             if (!first)
 656               fprintf (file, " <= ");
 657           }
 658
 659           /* Find chain.  */
 660           chain[0] = v;
 661           m = 1;
 662           while (1)
 663             {
 664               /* Print chain.  */
 665               for (v2 = 1; v2 <= pb->num_vars; v2++)
 666                 if (po[v][v2] && chain_length[v] == 1 + chain_length[v2])
 667                   break;
 668
 669               if (v2 > pb->num_vars)
 670                 break;
 671
 672               chain[m++] = v2;
 673               v = v2;
 674             }
 675
 676           fprintf (file, "%s", omega_variable_to_str (pb, chain[0]));
 677
 678           for (multiprint = false, i = 1; i < m; i++)
 679             {
 680               v = chain[i - 1];
 681               v2 = chain[i];
 682
 683               if (po[v][v2] == le)
 684                 fprintf (file, " <= ");
 685               else
 686                 fprintf (file, " < ");
 687
 688               fprintf (file, "%s", omega_variable_to_str (pb, v2));
 689               live[po_eq[v][v2]] = false;
 690
 691               if (!multiprint && i < m - 1)
 692                 for (v3 = 1; v3 <= pb->num_vars; v3++)
 693                   {
 694                     if (v == v3 || v2 == v3
 695                         || po[v][v2] != po[v][v3]
 696                         || po[v2][chain[i + 1]] != po[v3][chain[i + 1]])
 697                       continue;
 698
 699                     fprintf (file, ",%s", omega_variable_to_str (pb, v3));
 700                     live[po_eq[v][v3]] = false;
 701                     live[po_eq[v3][chain[i + 1]]] = false;
 702                     multiprint = true;
 703                   }
 704               else
 705                 multiprint = false;
 706             }
 707
 708           v = chain[m - 1];
 709           /* Print last_links.  */
 710           {
 711             int tmp;
 712             bool first = true;
 713
 714             for (e = 0; e < pb->num_geqs; e++)
 715               if (live[e] && pb->geqs[e].coef[v] == -1)
 716                 {
 717                   if (!first)
 718                     fprintf (file, ", ");
 719                   else
 720                     fprintf (file, " <= ");
 721
 722                   tmp = pb->geqs[e].coef[v];
 723                   pb->geqs[e].coef[v] = 0;
 724                   omega_print_term (file, pb, &pb->geqs[e], 1);
 725                   pb->geqs[e].coef[v] = tmp;
 726                   live[e] = false;
 727                   first = false;
 728                 }
 729           }
 730         }
 731
 732       for (e = 0; e < pb->num_geqs; e++)
 733         if (live[e])
 734           {
 735             if (stuffPrinted)
 736               fprintf (file, "; ");
 737             stuffPrinted = 1;
 738             omega_print_geq (file, pb, &pb->geqs[e]);
 739           }
 740
 741       for (e = 0; e < pb->num_subs; e++)
 742         {
 743           eqn eq = &pb->subs[e];
 744
 745           if (stuffPrinted)
 746             fprintf (file, "; ");
 747
 748           stuffPrinted = 1;
 749
 750           if (eq->key > 0)
 751             fprintf (file, "%s := ", omega_var_to_str (eq->key));
 752           else
 753             fprintf (file, "#%d := ", eq->key);
 754
 755           omega_print_term (file, pb, eq, 1);
 756         }
 757     }
 758
 759   free (live);
 760   free (po);
 761   free (po_eq);
 762   free (last_links);
 763   free (first_links);
 764   free (chain_length);
 765   free (chain);
 766 }
 767
 768 /* Assign to variable I in PB the next wildcard name.  The name of a
 769    wildcard is a negative number.  */
 770 static int next_wild_card = 0;
 771
 772 static void
 773 omega_name_wild_card (omega_pb pb, int i)
 774 {
 775   --next_wild_card;
 776   if (next_wild_card < -PARAM_VALUE (PARAM_OMEGA_MAX_WILD_CARDS))
 777     next_wild_card = -1;
 778   pb->var[i] = next_wild_card;
 779 }
 780
 781 /* Return the index of the last protected (or safe) variable in PB,
 782    after having added a new wildcard variable.  */
 783
 784 static int
 785 omega_add_new_wild_card (omega_pb pb)
 786 {
 787   int e;
 788   int i = ++pb->safe_vars;
 789   pb->num_vars++;
 790
 791   /* Make a free place in the protected (safe) variables, by moving
 792      the non protected variable pointed by "I" at the end, ie. at
 793      offset pb->num_vars.  */
 794   if (pb->num_vars != i)
 795     {
 796       /* Move "I" for all the inequalities.  */
 797       for (e = pb->num_geqs - 1; e >= 0; e--)
 798         {
 799           if (pb->geqs[e].coef[i])
 800             pb->geqs[e].touched = 1;
 801
 802           pb->geqs[e].coef[pb->num_vars] = pb->geqs[e].coef[i];
 803         }
 804
 805       /* Move "I" for all the equalities.  */
 806       for (e = pb->num_eqs - 1; e >= 0; e--)
 807         pb->eqs[e].coef[pb->num_vars] = pb->eqs[e].coef[i];
 808
 809       /* Move "I" for all the substitutions.  */
 810       for (e = pb->num_subs - 1; e >= 0; e--)
 811         pb->subs[e].coef[pb->num_vars] = pb->subs[e].coef[i];
 812
 813       /* Move the identifier.  */
 814       pb->var[pb->num_vars] = pb->var[i];
 815     }
 816
 817   /* Initialize at zero all the coefficients  */
 818   for (e = pb->num_geqs - 1; e >= 0; e--)
 819     pb->geqs[e].coef[i] = 0;
 820
 821   for (e = pb->num_eqs - 1; e >= 0; e--)
 822     pb->eqs[e].coef[i] = 0;
 823
 824   for (e = pb->num_subs - 1; e >= 0; e--)
 825     pb->subs[e].coef[i] = 0;
 826
 827   /* And give it a name.  */
 828   omega_name_wild_card (pb, i);
 829   return i;
 830 }
 831
 832 /* Delete inequality E from problem PB that has N_VARS variables.  */
 833
 834 static void
 835 omega_delete_geq (omega_pb pb, int e, int n_vars)
 836 {
 837   if (dump_file && (dump_flags & TDF_DETAILS))
 838     {
 839       fprintf (dump_file, "Deleting %d (last:%d): ", e, pb->num_geqs - 1);
 840       omega_print_geq (dump_file, pb, &pb->geqs[e]);
 841       fprintf (dump_file, "\n");
 842     }
 843
 844   if (e < pb->num_geqs - 1)
 845     omega_copy_eqn (&pb->geqs[e], &pb->geqs[pb->num_geqs - 1], n_vars);
 846
 847   pb->num_geqs--;
 848 }
 849
 850 /* Delete extra inequality E from problem PB that has N_VARS
 851    variables.  */
 852
 853 static void
 854 omega_delete_geq_extra (omega_pb pb, int e, int n_vars)
 855 {
 856   if (dump_file && (dump_flags & TDF_DETAILS))
 857     {
 858       fprintf (dump_file, "Deleting %d: ",e);
 859       omega_print_geq_extra (dump_file, pb, &pb->geqs[e]);
 860       fprintf (dump_file, "\n");
 861     }
 862
 863   if (e < pb->num_geqs - 1)
 864     omega_copy_eqn (&pb->geqs[e], &pb->geqs[pb->num_geqs - 1], n_vars);
 865
 866   pb->num_geqs--;
 867 }
 868
 869
 870 /* Remove variable I from problem PB.  */
 871
 872 static void
 873 omega_delete_variable (omega_pb pb, int i)
 874 {
 875   int n_vars = pb->num_vars;
 876   int e;
 877
 878   if (omega_safe_var_p (pb, i))
 879     {
 880       int j = pb->safe_vars;
 881
 882       for (e = pb->num_geqs - 1; e >= 0; e--)
 883         {
 884           pb->geqs[e].touched = 1;
 885           pb->geqs[e].coef[i] = pb->geqs[e].coef[j];
 886           pb->geqs[e].coef[j] = pb->geqs[e].coef[n_vars];
 887         }
 888
 889       for (e = pb->num_eqs - 1; e >= 0; e--)
 890         {
 891           pb->eqs[e].coef[i] = pb->eqs[e].coef[j];
 892           pb->eqs[e].coef[j] = pb->eqs[e].coef[n_vars];
 893         }
 894
 895       for (e = pb->num_subs - 1; e >= 0; e--)
 896         {
 897           pb->subs[e].coef[i] = pb->subs[e].coef[j];
 898           pb->subs[e].coef[j] = pb->subs[e].coef[n_vars];
 899         }
 900
 901       pb->var[i] = pb->var[j];
 902       pb->var[j] = pb->var[n_vars];
 903     }
 904   else if (i < n_vars)
 905     {
 906       for (e = pb->num_geqs - 1; e >= 0; e--)
 907         if (pb->geqs[e].coef[n_vars])
 908           {
 909             pb->geqs[e].coef[i] = pb->geqs[e].coef[n_vars];
 910             pb->geqs[e].touched = 1;
 911           }
 912
 913       for (e = pb->num_eqs - 1; e >= 0; e--)
 914         pb->eqs[e].coef[i] = pb->eqs[e].coef[n_vars];
 915
 916       for (e = pb->num_subs - 1; e >= 0; e--)
 917         pb->subs[e].coef[i] = pb->subs[e].coef[n_vars];
 918
 919       pb->var[i] = pb->var[n_vars];
 920     }
 921
 922   if (omega_safe_var_p (pb, i))
 923     pb->safe_vars--;
 924
 925   pb->num_vars--;
 926 }
 927
 928 /* Because the coefficients of an equation are sparse, PACKING records
 929    indices for non null coefficients.  */
 930 static int *packing;
 931
 932 /* Set up the coefficients of PACKING, following the coefficients of
 933    equation EQN that has NUM_VARS variables.  */
 934
 935 static inline int
 936 setup_packing (eqn eqn, int num_vars)
 937 {
 938   int k;
 939   int n = 0;
 940
 941   for (k = num_vars; k >= 0; k--)
 942     if (eqn->coef[k])
 943       packing[n++] = k;
 944
 945   return n;
 946 }
 947
 948 /* Computes a linear combination of EQ and SUB at VAR with coefficient
 949    C, such that EQ->coef[VAR] is set to 0.  TOP_VAR is the number of
 950    non null indices of SUB stored in PACKING.  */
 951
 952 static inline void
 953 omega_substitute_red_1 (eqn eq, eqn sub, int var, int c, bool *found_black,
 954                         int top_var)
 955 {
 956   if (eq->coef[var] != 0)
 957     {
 958       if (eq->color == omega_black)
 959         *found_black = true;
 960       else
 961         {
 962           int j, k = eq->coef[var];
 963
 964           eq->coef[var] = 0;
 965
 966           for (j = top_var; j >= 0; j--)
 967             eq->coef[packing[j]] -= sub->coef[packing[j]] * k * c;
 968         }
 969     }
 970 }
 971
 972 /* Substitute in PB variable VAR with "C * SUB".  */
 973
 974 static void
 975 omega_substitute_red (omega_pb pb, eqn sub, int var, int c, bool *found_black)
 976 {
 977   int e, top_var = setup_packing (sub, pb->num_vars);
 978
 979   *found_black = false;
 980
 981   if (dump_file && (dump_flags & TDF_DETAILS))
 982     {
 983       if (sub->color == omega_red)
 984         fprintf (dump_file, "[");
 985
 986       fprintf (dump_file, "substituting using %s := ",
 987                omega_variable_to_str (pb, var));
 988       omega_print_term (dump_file, pb, sub, -c);
 989
 990       if (sub->color == omega_red)
 991         fprintf (dump_file, "]");
 992
 993       fprintf (dump_file, "\n");
 994       omega_print_vars (dump_file, pb);
 995     }
 996
 997   for (e = pb->num_eqs - 1; e >= 0; e--)
 998     {
 999       eqn eqn = &(pb->eqs[e]);
1000
1001       omega_substitute_red_1 (eqn, sub, var, c, found_black, top_var);
1002
1003       if (dump_file && (dump_flags & TDF_DETAILS))
1004         {
1005           omega_print_eq (dump_file, pb, eqn);
1006           fprintf (dump_file, "\n");
1007         }
1008     }
1009
1010   for (e = pb->num_geqs - 1; e >= 0; e--)
1011     {
1012       eqn eqn = &(pb->geqs[e]);
1013
1014       omega_substitute_red_1 (eqn, sub, var, c, found_black, top_var);
1015
1016       if (eqn->coef[var] && eqn->color == omega_red)
1017         eqn->touched = 1;
1018
1019       if (dump_file && (dump_flags & TDF_DETAILS))
1020         {
1021           omega_print_geq (dump_file, pb, eqn);
1022           fprintf (dump_file, "\n");
1023         }
1024     }
1025
1026   for (e = pb->num_subs - 1; e >= 0; e--)
1027     {
1028       eqn eqn = &(pb->subs[e]);
1029
1030       omega_substitute_red_1 (eqn, sub, var, c, found_black, top_var);
1031
1032       if (dump_file && (dump_flags & TDF_DETAILS))
1033         {
1034           fprintf (dump_file, "%s := ", omega_var_to_str (eqn->key));
1035           omega_print_term (dump_file, pb, eqn, 1);
1036           fprintf (dump_file, "\n");
1037         }
1038     }
1039
1040   if (dump_file && (dump_flags & TDF_DETAILS))
1041     fprintf (dump_file, "---\n\n");
1042
1043   if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
1044     *found_black = true;
1045 }
1046
1047 /* Substitute in PB variable VAR with "C * SUB".  */
1048
1049 static void
1050 omega_substitute (omega_pb pb, eqn sub, int var, int c)
1051 {
1052   int e, j, j0;
1053   int top_var = setup_packing (sub, pb->num_vars);
1054
1055   if (dump_file && (dump_flags & TDF_DETAILS))
1056     {
1057       fprintf (dump_file, "substituting using %s := ",
1058                omega_variable_to_str (pb, var));
1059       omega_print_term (dump_file, pb, sub, -c);
1060       fprintf (dump_file, "\n");
1061       omega_print_vars (dump_file, pb);
1062     }
1063
1064   if (top_var < 0)
1065     {
1066       for (e = pb->num_eqs - 1; e >= 0; e--)
1067         pb->eqs[e].coef[var] = 0;
1068
1069       for (e = pb->num_geqs - 1; e >= 0; e--)
1070         if (pb->geqs[e].coef[var] != 0)
1071           {
1072             pb->geqs[e].touched = 1;
1073             pb->geqs[e].coef[var] = 0;
1074           }
1075
1076       for (e = pb->num_subs - 1; e >= 0; e--)
1077         pb->subs[e].coef[var] = 0;
1078
1079       if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
1080         {
1081           int k;
1082           eqn eqn = &(pb->subs[pb->num_subs++]);
1083
1084           for (k = pb->num_vars; k >= 0; k--)
1085             eqn->coef[k] = 0;
1086
1087           eqn->key = pb->var[var];
1088           eqn->color = omega_black;
1089         }
1090     }
1091   else if (top_var == 0 && packing[0] == 0)
1092     {
1093       c = -sub->coef[0] * c;
1094
1095       for (e = pb->num_eqs - 1; e >= 0; e--)
1096         {
1097           pb->eqs[e].coef[0] += pb->eqs[e].coef[var] * c;
1098           pb->eqs[e].coef[var] = 0;
1099         }
1100
1101       for (e = pb->num_geqs - 1; e >= 0; e--)
1102         if (pb->geqs[e].coef[var] != 0)
1103           {
1104             pb->geqs[e].coef[0] += pb->geqs[e].coef[var] * c;
1105             pb->geqs[e].coef[var] = 0;
1106             pb->geqs[e].touched = 1;
1107           }
1108
1109       for (e = pb->num_subs - 1; e >= 0; e--)
1110         {
1111           pb->subs[e].coef[0] += pb->subs[e].coef[var] * c;
1112           pb->subs[e].coef[var] = 0;
1113         }
1114
1115       if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
1116         {
1117           int k;
1118           eqn eqn = &(pb->subs[pb->num_subs++]);
1119
1120           for (k = pb->num_vars; k >= 1; k--)
1121             eqn->coef[k] = 0;
1122
1123           eqn->coef[0] = c;
1124           eqn->key = pb->var[var];
1125           eqn->color = omega_black;
1126         }
1127
1128       if (dump_file && (dump_flags & TDF_DETAILS))
1129         {
1130           fprintf (dump_file, "---\n\n");
1131           omega_print_problem (dump_file, pb);
1132           fprintf (dump_file, "===\n\n");
1133         }
1134     }
1135   else
1136     {
1137       for (e = pb->num_eqs - 1; e >= 0; e--)
1138         {
1139           eqn eqn = &(pb->eqs[e]);
1140           int k = eqn->coef[var];
1141
1142           if (k != 0)
1143             {
1144               k = c * k;
1145               eqn->coef[var] = 0;
1146
1147               for (j = top_var; j >= 0; j--)
1148                 {
1149                   j0 = packing[j];
1150                   eqn->coef[j0] -= sub->coef[j0] * k;
1151                 }
1152             }
1153
1154           if (dump_file && (dump_flags & TDF_DETAILS))
1155             {
1156               omega_print_eq (dump_file, pb, eqn);
1157               fprintf (dump_file, "\n");
1158             }
1159         }
1160
1161       for (e = pb->num_geqs - 1; e >= 0; e--)
1162         {
1163           eqn eqn = &(pb->geqs[e]);
1164           int k = eqn->coef[var];
1165
1166           if (k != 0)
1167             {
1168               k = c * k;
1169               eqn->touched = 1;
1170               eqn->coef[var] = 0;
1171
1172               for (j = top_var; j >= 0; j--)
1173                 {
1174                   j0 = packing[j];
1175                   eqn->coef[j0] -= sub->coef[j0] * k;
1176                 }
1177             }
1178
1179           if (dump_file && (dump_flags & TDF_DETAILS))
1180             {
1181               omega_print_geq (dump_file, pb, eqn);
1182               fprintf (dump_file, "\n");
1183             }
1184         }
1185
1186       for (e = pb->num_subs - 1; e >= 0; e--)
1187         {
1188           eqn eqn = &(pb->subs[e]);
1189           int k = eqn->coef[var];
1190
1191           if (k != 0)
1192             {
1193               k = c * k;
1194               eqn->coef[var] = 0;
1195
1196               for (j = top_var; j >= 0; j--)
1197                 {
1198                   j0 = packing[j];
1199                   eqn->coef[j0] -= sub->coef[j0] * k;
1200                 }
1201             }
1202
1203           if (dump_file && (dump_flags & TDF_DETAILS))
1204             {
1205               fprintf (dump_file, "%s := ", omega_var_to_str (eqn->key));
1206               omega_print_term (dump_file, pb, eqn, 1);
1207               fprintf (dump_file, "\n");
1208             }
1209         }
1210
1211       if (dump_file && (dump_flags & TDF_DETAILS))
1212         {
1213           fprintf (dump_file, "---\n\n");
1214           omega_print_problem (dump_file, pb);
1215           fprintf (dump_file, "===\n\n");
1216         }
1217
1218       if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
1219         {
1220           int k;
1221           eqn eqn = &(pb->subs[pb->num_subs++]);
1222           c = -c;
1223
1224           for (k = pb->num_vars; k >= 0; k--)
1225             eqn->coef[k] = c * (sub->coef[k]);
1226
1227           eqn->key = pb->var[var];
1228           eqn->color = sub->color;
1229         }
1230     }
1231 }
1232
1233 /* Solve e = factor alpha for x_j and substitute.  */
1234
1235 static void
1236 omega_do_mod (omega_pb pb, int factor, int e, int j)
1237 {
1238   int k, i;
1239   eqn eq = omega_alloc_eqns (0, 1);
1240   int nfactor;
1241   bool kill_j = false;
1242
1243   omega_copy_eqn (eq, &pb->eqs[e], pb->num_vars);
1244
1245   for (k = pb->num_vars; k >= 0; k--)
1246     {
1247       eq->coef[k] = int_mod (eq->coef[k], factor);
1248
1249       if (2 * eq->coef[k] >= factor)
1250         eq->coef[k] -= factor;
1251     }
1252
1253   nfactor = eq->coef[j];
1254
1255   if (omega_safe_var_p (pb, j) && !omega_wildcard_p (pb, j))
1256     {
1257       i = omega_add_new_wild_card (pb);
1258       eq->coef[pb->num_vars] = eq->coef[i];
1259       eq->coef[j] = 0;
1260       eq->coef[i] = -factor;
1261       kill_j = true;
1262     }
1263   else
1264     {
1265       eq->coef[j] = -factor;
1266       if (!omega_wildcard_p (pb, j))
1267         omega_name_wild_card (pb, j);
1268     }
1269
1270   omega_substitute (pb, eq, j, nfactor);
1271
1272   for (k = pb->num_vars; k >= 0; k--)
1273     pb->eqs[e].coef[k] = pb->eqs[e].coef[k] / factor;
1274
1275   if (kill_j)
1276     omega_delete_variable (pb, j);
1277
1278   if (dump_file && (dump_flags & TDF_DETAILS))
1279     {
1280       fprintf (dump_file, "Mod-ing and normalizing produces:\n");
1281       omega_print_problem (dump_file, pb);
1282     }
1283
1284   omega_free_eqns (eq, 1);
1285 }
1286
1287 /* Multiplies by -1 inequality E.  */
1288
1289 void
1290 omega_negate_geq (omega_pb pb, int e)
1291 {
1292   int i;
1293
1294   for (i = pb->num_vars; i >= 0; i--)
1295     pb->geqs[e].coef[i] *= -1;
1296
1297   pb->geqs[e].coef[0]--;
1298   pb->geqs[e].touched = 1;
1299 }
1300
1301 /* Returns OMEGA_TRUE when problem PB has a solution.  */
1302
1303 static enum omega_result
1304 verify_omega_pb (omega_pb pb)
1305 {
1306   enum omega_result result;
1307   int e;
1308   bool any_color = false;
1309   omega_pb tmp_problem = XNEW (struct omega_pb);
1310
1311   omega_copy_problem (tmp_problem, pb);
1312   tmp_problem->safe_vars = 0;
1313   tmp_problem->num_subs = 0;
1314
1315   for (e = pb->num_geqs - 1; e >= 0; e--)
1316     if (pb->geqs[e].color == omega_red)
1317       {
1318         any_color = true;
1319         break;
1320       }
1321
1322   if (please_no_equalities_in_simplified_problems)
1323     any_color = true;
1324
1325   if (any_color)
1326     original_problem = no_problem;
1327   else
1328     original_problem = pb;
1329
1330   if (dump_file && (dump_flags & TDF_DETAILS))
1331     {
1332       fprintf (dump_file, "verifying problem");
1333
1334       if (any_color)
1335         fprintf (dump_file, " (color mode)");
1336
1337       fprintf (dump_file, " :\n");
1338       omega_print_problem (dump_file, pb);
1339     }
1340
1341   result = omega_solve_problem (tmp_problem, omega_unknown);
1342   original_problem = no_problem;
1343   free (tmp_problem);
1344
1345   if (dump_file && (dump_flags & TDF_DETAILS))
1346     {
1347       if (result != omega_false)
1348         fprintf (dump_file, "verified problem\n");
1349       else
1350         fprintf (dump_file, "disproved problem\n");
1351       omega_print_problem (dump_file, pb);
1352     }
1353
1354   return result;
1355 }
1356
1357 /* Add a new equality to problem PB at last position E.  */
1358
1359 static void
1360 adding_equality_constraint (omega_pb pb, int e)
1361 {
1362   if (original_problem != no_problem
1363       && original_problem != pb
1364       && !conservative)
1365     {
1366       int i, j;
1367       int e2 = original_problem->num_eqs++;
1368
1369       if (dump_file && (dump_flags & TDF_DETAILS))
1370         fprintf (dump_file,
1371                  "adding equality constraint %d to outer problem\n", e2);
1372       omega_init_eqn_zero (&original_problem->eqs[e2],
1373                            original_problem->num_vars);
1374
1375       for (i = pb->num_vars; i >= 1; i--)
1376         {
1377           for (j = original_problem->num_vars; j >= 1; j--)
1378             if (original_problem->var[j] == pb->var[i])
1379               break;
1380
1381           if (j <= 0)
1382             {
1383               if (dump_file && (dump_flags & TDF_DETAILS))
1384                 fprintf (dump_file, "retracting\n");
1385               original_problem->num_eqs--;
1386               return;
1387             }
1388           original_problem->eqs[e2].coef[j] = pb->eqs[e].coef[i];
1389         }
1390
1391       original_problem->eqs[e2].coef[0] = pb->eqs[e].coef[0];
1392
1393       if (dump_file && (dump_flags & TDF_DETAILS))
1394         omega_print_problem (dump_file, original_problem);
1395     }
1396 }
1397
1398 static int *fast_lookup;
1399 static int *fast_lookup_red;
1400
1401 typedef enum {
1402   normalize_false,
1403   normalize_uncoupled,
1404   normalize_coupled
1405 } normalize_return_type;
1406
1407 /* Normalizes PB by removing redundant constraints.  Returns
1408    normalize_false when the constraints system has no solution,
1409    otherwise returns normalize_coupled or normalize_uncoupled.  */
1410
1411 static normalize_return_type
1412 normalize_omega_problem (omega_pb pb)
1413 {
1414   int e, i, j, k, n_vars;
1415   int coupled_subscripts = 0;
1416
1417   n_vars = pb->num_vars;
1418
1419   for (e = 0; e < pb->num_geqs; e++)
1420     {
1421       if (!pb->geqs[e].touched)
1422         {
1423           if (!single_var_geq (&pb->geqs[e], n_vars))
1424             coupled_subscripts = 1;
1425         }
1426       else
1427         {
1428           int g, top_var, i0, hashCode;
1429           int *p = &packing[0];
1430
1431           for (k = 1; k <= n_vars; k++)
1432             if (pb->geqs[e].coef[k])
1433               *(p++) = k;
1434
1435           top_var = (p - &packing[0]) - 1;
1436
1437           if (top_var == -1)
1438             {
1439               if (pb->geqs[e].coef[0] < 0)
1440                 {
1441                   if (dump_file && (dump_flags & TDF_DETAILS))
1442                     {
1443                       omega_print_geq (dump_file, pb, &pb->geqs[e]);
1444                       fprintf (dump_file, "\nequations have no solution \n");
1445                     }
1446                   return normalize_false;
1447                 }
1448
1449               omega_delete_geq (pb, e, n_vars);
1450               e--;
1451               continue;
1452             }
1453           else if (top_var == 0)
1454             {
1455               int singlevar = packing[0];
1456
1457               g = pb->geqs[e].coef[singlevar];
1458
1459               if (g > 0)
1460                 {
1461                   pb->geqs[e].coef[singlevar] = 1;
1462                   pb->geqs[e].key = singlevar;
1463                 }
1464               else
1465                 {
1466                   g = -g;
1467                   pb->geqs[e].coef[singlevar] = -1;
1468                   pb->geqs[e].key = -singlevar;
1469                 }
1470
1471               if (g > 1)
1472                 pb->geqs[e].coef[0] = int_div (pb->geqs[e].coef[0], g);
1473             }
1474           else
1475             {
1476               int g2;
1477               int hash_key_multiplier = 31;
1478
1479               coupled_subscripts = 1;
1480               i0 = top_var;
1481               i = packing[i0--];
1482               g = pb->geqs[e].coef[i];
1483               hashCode = g * (i + 3);
1484
1485               if (g < 0)
1486                 g = -g;
1487
1488               for (; i0 >= 0; i0--)
1489                 {
1490                   int x;
1491
1492                   i = packing[i0];
1493                   x = pb->geqs[e].coef[i];
1494                   hashCode = hashCode * hash_key_multiplier * (i + 3) + x;
1495
1496                   if (x < 0)
1497                     x = -x;
1498
1499                   if (x == 1)
1500                     {
1501                       g = 1;
1502                       i0--;
1503                       break;
1504                     }
1505                   else
1506                     g = gcd (x, g);
1507                 }
1508
1509               for (; i0 >= 0; i0--)
1510                 {
1511                   int x;
1512                   i = packing[i0];
1513                   x = pb->geqs[e].coef[i];
1514                   hashCode = hashCode * hash_key_multiplier * (i + 3) + x;
1515                 }
1516
1517               if (g > 1)
1518                 {
1519                   pb->geqs[e].coef[0] = int_div (pb->geqs[e].coef[0], g);
1520                   i0 = top_var;
1521                   i = packing[i0--];
1522                   pb->geqs[e].coef[i] = pb->geqs[e].coef[i] / g;
1523                   hashCode = pb->geqs[e].coef[i] * (i + 3);
1524
1525                   for (; i0 >= 0; i0--)
1526                     {
1527                       i = packing[i0];
1528                       pb->geqs[e].coef[i] = pb->geqs[e].coef[i] / g;
1529                       hashCode = hashCode * hash_key_multiplier * (i + 3)
1530                         + pb->geqs[e].coef[i];
1531                     }
1532                 }
1533
1534               g2 = abs (hashCode);
1535
1536               if (dump_file && (dump_flags & TDF_DETAILS))
1537                 {
1538                   fprintf (dump_file, "Hash code = %d, eqn = ", hashCode);
1539                   omega_print_geq (dump_file, pb, &pb->geqs[e]);
1540                   fprintf (dump_file, "\n");
1541                 }
1542
1543               j = g2 % HASH_TABLE_SIZE;
1544
1545               do {
1546                 eqn proto = &(hash_master[j]);
1547
1548                 if (proto->touched == g2)
1549                   {
1550                     if (proto->coef[0] == top_var)
1551                       {
1552                         if (hashCode >= 0)
1553                           for (i0 = top_var; i0 >= 0; i0--)
1554                             {
1555                               i = packing[i0];
1556
1557                               if (pb->geqs[e].coef[i] != proto->coef[i])
1558                                 break;
1559                             }
1560                         else
1561                           for (i0 = top_var; i0 >= 0; i0--)
1562                             {
1563                               i = packing[i0];
1564
1565                               if (pb->geqs[e].coef[i] != -proto->coef[i])
1566                                 break;
1567                             }
1568
1569                         if (i0 < 0)
1570                           {
1571                             if (hashCode >= 0)
1572                               pb->geqs[e].key = proto->key;
1573                             else
1574                               pb->geqs[e].key = -proto->key;
1575                             break;
1576                           }
1577                       }
1578                   }
1579                 else if (proto->touched < 0)
1580                   {
1581                     omega_init_eqn_zero (proto, pb->num_vars);
1582                     if (hashCode >= 0)
1583                       for (i0 = top_var; i0 >= 0; i0--)
1584                         {
1585                           i = packing[i0];
1586                           proto->coef[i] = pb->geqs[e].coef[i];
1587                         }
1588                     else
1589                       for (i0 = top_var; i0 >= 0; i0--)
1590                         {
1591                           i = packing[i0];
1592                           proto->coef[i] = -pb->geqs[e].coef[i];
1593                         }
1594
1595                     proto->coef[0] = top_var;
1596                     proto->touched = g2;
1597
1598                     if (dump_file && (dump_flags & TDF_DETAILS))
1599                       fprintf (dump_file, " constraint key = %d\n",
1600                                next_key);
1601
1602                     proto->key = next_key++;
1603
1604                     /* Too many hash keys generated.  */
1605                     gcc_assert (proto->key <= MAX_KEYS);
1606
1607                     if (hashCode >= 0)
1608                       pb->geqs[e].key = proto->key;
1609                     else
1610                       pb->geqs[e].key = -proto->key;
1611
1612                     break;
1613                   }
1614
1615                 j = (j + 1) % HASH_TABLE_SIZE;
1616               } while (1);
1617             }
1618
1619           pb->geqs[e].touched = 0;
1620         }
1621
1622       {
1623         int eKey = pb->geqs[e].key;
1624         int e2;
1625         if (e > 0)
1626           {
1627             int cTerm = pb->geqs[e].coef[0];
1628             e2 = fast_lookup[MAX_KEYS - eKey];
1629
1630             if (e2 < e && pb->geqs[e2].key == -eKey
1631                 && pb->geqs[e2].color == omega_black)
1632               {
1633                 if (pb->geqs[e2].coef[0] < -cTerm)
1634                   {
1635                     if (dump_file && (dump_flags & TDF_DETAILS))
1636                       {
1637                         omega_print_geq (dump_file, pb, &pb->geqs[e]);
1638                         fprintf (dump_file, "\n");
1639                         omega_print_geq (dump_file, pb, &pb->geqs[e2]);
1640                         fprintf (dump_file,
1641                                  "\nequations have no solution \n");
1642                       }
1643                     return normalize_false;
1644                   }
1645
1646                 if (pb->geqs[e2].coef[0] == -cTerm
1647                     && (create_color
1648                         || pb->geqs[e].color == omega_black))
1649                   {
1650                     omega_copy_eqn (&pb->eqs[pb->num_eqs], &pb->geqs[e],
1651                                     pb->num_vars);
1652                     if (pb->geqs[e].color == omega_black)
1653                       adding_equality_constraint (pb, pb->num_eqs);
1654                     pb->num_eqs++;
1655                     gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
1656                   }
1657               }
1658
1659             e2 = fast_lookup_red[MAX_KEYS - eKey];
1660
1661             if (e2 < e && pb->geqs[e2].key == -eKey
1662                 && pb->geqs[e2].color == omega_red)
1663               {
1664                 if (pb->geqs[e2].coef[0] < -cTerm)
1665                   {
1666                     if (dump_file && (dump_flags & TDF_DETAILS))
1667                       {
1668                         omega_print_geq (dump_file, pb, &pb->geqs[e]);
1669                         fprintf (dump_file, "\n");
1670                         omega_print_geq (dump_file, pb, &pb->geqs[e2]);
1671                         fprintf (dump_file,
1672                                  "\nequations have no solution \n");
1673                       }
1674                     return normalize_false;
1675                   }
1676
1677                 if (pb->geqs[e2].coef[0] == -cTerm && create_color)
1678                   {
1679                     omega_copy_eqn (&pb->eqs[pb->num_eqs], &pb->geqs[e],
1680                                     pb->num_vars);
1681                     pb->eqs[pb->num_eqs].color = omega_red;
1682                     pb->num_eqs++;
1683                     gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
1684                   }
1685               }
1686
1687             e2 = fast_lookup[MAX_KEYS + eKey];
1688
1689             if (e2 < e && pb->geqs[e2].key == eKey
1690                 && pb->geqs[e2].color == omega_black)
1691               {
1692                 if (pb->geqs[e2].coef[0] > cTerm)
1693                   {
1694                     if (pb->geqs[e].color == omega_black)
1695                       {
1696                         if (dump_file && (dump_flags & TDF_DETAILS))
1697                           {
1698                             fprintf (dump_file,
1699                                      "Removing Redundant Equation: ");
1700                             omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
1701                             fprintf (dump_file, "\n");
1702                             fprintf (dump_file,
1703                                      "[a]      Made Redundant by: ");
1704                             omega_print_geq (dump_file, pb, &(pb->geqs[e]));
1705                             fprintf (dump_file, "\n");
1706                           }
1707                         pb->geqs[e2].coef[0] = cTerm;
1708                         omega_delete_geq (pb, e, n_vars);
1709                         e--;
1710                         continue;
1711                       }
1712                   }
1713                 else
1714                   {
1715                     if (dump_file && (dump_flags & TDF_DETAILS))
1716                       {
1717                         fprintf (dump_file, "Removing Redundant Equation: ");
1718                         omega_print_geq (dump_file, pb, &(pb->geqs[e]));
1719                         fprintf (dump_file, "\n");
1720                         fprintf (dump_file, "[b]      Made Redundant by: ");
1721                         omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
1722                         fprintf (dump_file, "\n");
1723                       }
1724                     omega_delete_geq (pb, e, n_vars);
1725                     e--;
1726                     continue;
1727                   }
1728               }
1729
1730             e2 = fast_lookup_red[MAX_KEYS + eKey];
1731
1732             if (e2 < e && pb->geqs[e2].key == eKey
1733                 && pb->geqs[e2].color == omega_red)
1734               {
1735                 if (pb->geqs[e2].coef[0] >= cTerm)
1736                   {
1737                     if (dump_file && (dump_flags & TDF_DETAILS))
1738                       {
1739                         fprintf (dump_file, "Removing Redundant Equation: ");
1740                         omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
1741                         fprintf (dump_file, "\n");
1742                         fprintf (dump_file, "[c]      Made Redundant by: ");
1743                         omega_print_geq (dump_file, pb, &(pb->geqs[e]));
1744                         fprintf (dump_file, "\n");
1745                       }
1746                     pb->geqs[e2].coef[0] = cTerm;
1747                     pb->geqs[e2].color = pb->geqs[e].color;
1748                   }
1749                 else if (pb->geqs[e].color == omega_red)
1750                   {
1751                     if (dump_file && (dump_flags & TDF_DETAILS))
1752                       {
1753                         fprintf (dump_file, "Removing Redundant Equation: ");
1754                         omega_print_geq (dump_file, pb, &(pb->geqs[e]));
1755                         fprintf (dump_file, "\n");
1756                         fprintf (dump_file, "[d]      Made Redundant by: ");
1757                         omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
1758                         fprintf (dump_file, "\n");
1759                       }
1760                   }
1761                 omega_delete_geq (pb, e, n_vars);
1762                 e--;
1763                 continue;
1764
1765               }
1766           }
1767
1768         if (pb->geqs[e].color == omega_red)
1769           fast_lookup_red[MAX_KEYS + eKey] = e;
1770         else
1771           fast_lookup[MAX_KEYS + eKey] = e;
1772       }
1773     }
1774
1775   create_color = false;
1776   return coupled_subscripts ? normalize_coupled : normalize_uncoupled;
1777 }
1778
1779 /* Divide the coefficients of EQN by their gcd.  N_VARS is the number
1780    of variables in EQN.  */
1781
1782 static inline void
1783 divide_eqn_by_gcd (eqn eqn, int n_vars)
1784 {
1785   int var, g = 0;
1786
1787   for (var = n_vars; var >= 0; var--)
1788     g = gcd (abs (eqn->coef[var]), g);
1789
1790   if (g)
1791     for (var = n_vars; var >= 0; var--)
1792       eqn->coef[var] = eqn->coef[var] / g;
1793 }
1794
1795 /* Rewrite some non-safe variables in function of protected
1796    wildcard variables.  */
1797
1798 static void
1799 cleanout_wildcards (omega_pb pb)
1800 {
1801   int e, i, j;
1802   int n_vars = pb->num_vars;
1803   bool renormalize = false;
1804
1805   for (e = pb->num_eqs - 1; e >= 0; e--)
1806     for (i = n_vars; !omega_safe_var_p (pb, i); i--)
1807       if (pb->eqs[e].coef[i] != 0)
1808         {
1809           /* i is the last nonzero non-safe variable.  */
1810
1811           for (j = i - 1; !omega_safe_var_p (pb, j); j--)
1812             if (pb->eqs[e].coef[j] != 0)
1813               break;
1814
1815           /* j is the next nonzero non-safe variable, or points
1816              to a safe variable: it is then a wildcard variable.  */
1817
1818           /* Clean it out.  */
1819           if (omega_safe_var_p (pb, j))
1820             {
1821               eqn sub = &(pb->eqs[e]);
1822               int c = pb->eqs[e].coef[i];
1823               int a = abs (c);
1824               int e2;
1825
1826               if (dump_file && (dump_flags & TDF_DETAILS))
1827                 {
1828                   fprintf (dump_file,
1829                            "Found a single wild card equality: ");
1830                   omega_print_eq (dump_file, pb, &pb->eqs[e]);
1831                   fprintf (dump_file, "\n");
1832                   omega_print_problem (dump_file, pb);
1833                 }
1834
1835               for (e2 = pb->num_eqs - 1; e2 >= 0; e2--)
1836                 if (e != e2 && pb->eqs[e2].coef[i]
1837                     && (pb->eqs[e2].color == omega_red
1838                         || (pb->eqs[e2].color == omega_black
1839                             && pb->eqs[e].color == omega_black)))
1840                   {
1841                     eqn eqn = &(pb->eqs[e2]);
1842                     int var, k;
1843
1844                     for (var = n_vars; var >= 0; var--)
1845                       eqn->coef[var] *= a;
1846
1847                     k = eqn->coef[i];
1848
1849                     for (var = n_vars; var >= 0; var--)
1850                       eqn->coef[var] -= sub->coef[var] * k / c;
1851
1852                     eqn->coef[i] = 0;
1853                     divide_eqn_by_gcd (eqn, n_vars);
1854                   }
1855
1856               for (e2 = pb->num_geqs - 1; e2 >= 0; e2--)
1857                 if (pb->geqs[e2].coef[i]
1858                     && (pb->geqs[e2].color == omega_red
1859                         || (pb->eqs[e].color == omega_black
1860                             && pb->geqs[e2].color == omega_black)))
1861                   {
1862                     eqn eqn = &(pb->geqs[e2]);
1863                     int var, k;
1864
1865                     for (var = n_vars; var >= 0; var--)
1866                       eqn->coef[var] *= a;
1867
1868                     k = eqn->coef[i];
1869
1870                     for (var = n_vars; var >= 0; var--)
1871                       eqn->coef[var] -= sub->coef[var] * k / c;
1872
1873                     eqn->coef[i] = 0;
1874                     eqn->touched = 1;
1875                     renormalize = true;
1876                   }
1877
1878               for (e2 = pb->num_subs - 1; e2 >= 0; e2--)
1879                 if (pb->subs[e2].coef[i]
1880                     && (pb->subs[e2].color == omega_red
1881                         || (pb->subs[e2].color == omega_black
1882                             && pb->eqs[e].color == omega_black)))
1883                   {
1884                     eqn eqn = &(pb->subs[e2]);
1885                     int var, k;
1886
1887                     for (var = n_vars; var >= 0; var--)
1888                       eqn->coef[var] *= a;
1889
1890                     k = eqn->coef[i];
1891
1892                     for (var = n_vars; var >= 0; var--)
1893                       eqn->coef[var] -= sub->coef[var] * k / c;
1894
1895                     eqn->coef[i] = 0;
1896                     divide_eqn_by_gcd (eqn, n_vars);
1897                   }
1898
1899               if (dump_file && (dump_flags & TDF_DETAILS))
1900                 {
1901                   fprintf (dump_file, "cleaned-out wildcard: ");
1902                   omega_print_problem (dump_file, pb);
1903                 }
1904               break;
1905             }
1906         }
1907
1908   if (renormalize)
1909     normalize_omega_problem (pb);
1910 }
1911
1912 /* Swap values contained in I and J.  */
1913
1914 static inline void
1915 swap (int *i, int *j)
1916 {
1917   int tmp;
1918   tmp = *i;
1919   *i = *j;
1920   *j = tmp;
1921 }
1922
1923 /* Swap values contained in I and J.  */
1924
1925 static inline void
1926 bswap (bool *i, bool *j)
1927 {
1928   bool tmp;
1929   tmp = *i;
1930   *i = *j;
1931   *j = tmp;
1932 }
1933
1934 /* Make variable IDX unprotected in PB, by swapping its index at the
1935    PB->safe_vars rank.  */
1936
1937 static inline void
1938 omega_unprotect_1 (omega_pb pb, int *idx, bool *unprotect)
1939 {
1940   /* If IDX is protected...  */
1941   if (*idx < pb->safe_vars)
1942     {
1943       /* ... swap its index with the last non protected index.  */
1944       int j = pb->safe_vars;
1945       int e;
1946
1947       for (e = pb->num_geqs - 1; e >= 0; e--)
1948         {
1949           pb->geqs[e].touched = 1;
1950           swap (&pb->geqs[e].coef[*idx], &pb->geqs[e].coef[j]);
1951         }
1952
1953       for (e = pb->num_eqs - 1; e >= 0; e--)
1954         swap (&pb->eqs[e].coef[*idx], &pb->eqs[e].coef[j]);
1955
1956       for (e = pb->num_subs - 1; e >= 0; e--)
1957         swap (&pb->subs[e].coef[*idx], &pb->subs[e].coef[j]);
1958
1959       if (unprotect)
1960         bswap (&unprotect[*idx], &unprotect[j]);
1961
1962       swap (&pb->var[*idx], &pb->var[j]);
1963       pb->forwarding_address[pb->var[*idx]] = *idx;
1964       pb->forwarding_address[pb->var[j]] = j;
1965       (*idx)--;
1966     }
1967
1968   /* The variable at pb->safe_vars is also unprotected now.  */
1969   pb->safe_vars--;
1970 }
1971
1972 /* During the Fourier-Motzkin elimination some variables are
1973    substituted with other variables.  This function resurrects the
1974    substituted variables in PB.  */
1975
1976 static void
1977 resurrect_subs (omega_pb pb)
1978 {
1979   if (pb->num_subs > 0
1980       && please_no_equalities_in_simplified_problems == 0)
1981     {
1982       int i, e, n, m;
1983
1984       if (dump_file && (dump_flags & TDF_DETAILS))
1985         {
1986           fprintf (dump_file,
1987                    "problem reduced, bringing variables back to life\n");
1988           omega_print_problem (dump_file, pb);
1989         }
1990
1991       for (i = 1; omega_safe_var_p (pb, i); i++)
1992         if (omega_wildcard_p (pb, i))
1993           omega_unprotect_1 (pb, &i, NULL);
1994
1995       m = pb->num_subs;
1996       n = MAX (pb->num_vars, pb->safe_vars + m);
1997
1998       for (e = pb->num_geqs - 1; e >= 0; e--)
1999         if (single_var_geq (&pb->geqs[e], pb->num_vars))
2000           {
2001             if (!omega_safe_var_p (pb, abs (pb->geqs[e].key)))
2002               pb->geqs[e].key += (pb->geqs[e].key > 0 ? m : -m);
2003           }
2004         else
2005           {
2006             pb->geqs[e].touched = 1;
2007             pb->geqs[e].key = 0;
2008           }
2009
2010       for (i = pb->num_vars; !omega_safe_var_p (pb, i); i--)
2011         {
2012           pb->var[i + m] = pb->var[i];
2013
2014           for (e = pb->num_geqs - 1; e >= 0; e--)
2015             pb->geqs[e].coef[i + m] = pb->geqs[e].coef[i];
2016
2017           for (e = pb->num_eqs - 1; e >= 0; e--)
2018             pb->eqs[e].coef[i + m] = pb->eqs[e].coef[i];
2019
2020           for (e = pb->num_subs - 1; e >= 0; e--)
2021             pb->subs[e].coef[i + m] = pb->subs[e].coef[i];
2022         }
2023
2024       for (i = pb->safe_vars + m; !omega_safe_var_p (pb, i); i--)
2025         {
2026           for (e = pb->num_geqs - 1; e >= 0; e--)
2027             pb->geqs[e].coef[i] = 0;
2028
2029           for (e = pb->num_eqs - 1; e >= 0; e--)
2030             pb->eqs[e].coef[i] = 0;
2031
2032           for (e = pb->num_subs - 1; e >= 0; e--)
2033             pb->subs[e].coef[i] = 0;
2034         }
2035
2036       pb->num_vars += m;
2037
2038       for (e = pb->num_subs - 1; e >= 0; e--)
2039         {
2040           pb->var[pb->safe_vars + 1 + e] = pb->subs[e].key;
2041           omega_copy_eqn (&(pb->eqs[pb->num_eqs]), &(pb->subs[e]),
2042                           pb->num_vars);
2043           pb->eqs[pb->num_eqs].coef[pb->safe_vars + 1 + e] = -1;
2044           pb->eqs[pb->num_eqs].color = omega_black;
2045
2046           if (dump_file && (dump_flags & TDF_DETAILS))
2047             {
2048               fprintf (dump_file, "brought back: ");
2049               omega_print_eq (dump_file, pb, &pb->eqs[pb->num_eqs]);
2050               fprintf (dump_file, "\n");
2051             }
2052
2053           pb->num_eqs++;
2054           gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
2055         }
2056
2057       pb->safe_vars += m;
2058       pb->num_subs = 0;
2059
2060       if (dump_file && (dump_flags & TDF_DETAILS))
2061         {
2062           fprintf (dump_file, "variables brought back to life\n");
2063           omega_print_problem (dump_file, pb);
2064         }
2065
2066       cleanout_wildcards (pb);
2067     }
2068 }
2069
2070 static inline bool
2071 implies (unsigned int a, unsigned int b)
2072 {
2073   return (a == (a & b));
2074 }
2075
2076 /* Eliminate redundant equations in PB.  When EXPENSIVE is true, an
2077    extra step is performed.  Returns omega_false when there exist no
2078    solution, omega_true otherwise.  */
2079
2080 enum omega_result
2081 omega_eliminate_redundant (omega_pb pb, bool expensive)
2082 {
2083   int c, e, e1, e2, e3, p, q, i, k, alpha, alpha1, alpha2, alpha3;
2084   bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
2085   omega_pb tmp_problem;
2086
2087   /* {P,Z,N}EQS = {Positive,Zero,Negative} Equations.  */
2088   unsigned int *peqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS);
2089   unsigned int *zeqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS);
2090   unsigned int *neqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS);
2091
2092   /* PP = Possible Positives, PZ = Possible Zeros, PN = Possible Negatives */
2093   unsigned int pp, pz, pn;
2094
2095   if (dump_file && (dump_flags & TDF_DETAILS))
2096     {
2097       fprintf (dump_file, "in eliminate Redundant:\n");
2098       omega_print_problem (dump_file, pb);
2099     }
2100
2101   for (e = pb->num_geqs - 1; e >= 0; e--)
2102     {
2103       int tmp = 1;
2104
2105       is_dead[e] = false;
2106       peqs[e] = zeqs[e] = neqs[e] = 0;
2107
2108       for (i = pb->num_vars; i >= 1; i--)
2109         {
2110           if (pb->geqs[e].coef[i] > 0)
2111             peqs[e] |= tmp;
2112           else if (pb->geqs[e].coef[i] < 0)
2113             neqs[e] |= tmp;
2114           else
2115             zeqs[e] |= tmp;
2116
2117           tmp <<= 1;
2118         }
2119     }
2120
2121
2122   for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
2123     if (!is_dead[e1])
2124       for (e2 = e1 - 1; e2 >= 0; e2--)
2125         if (!is_dead[e2])
2126           {
2127             for (p = pb->num_vars; p > 1; p--)
2128               for (q = p - 1; q > 0; q--)
2129                 if ((alpha = pb->geqs[e1].coef[p] * pb->geqs[e2].coef[q]
2130                      - pb->geqs[e2].coef[p] * pb->geqs[e1].coef[q]) != 0)
2131                   goto foundPQ;
2132
2133             continue;
2134
2135           foundPQ:
2136             pz = ((zeqs[e1] & zeqs[e2]) | (peqs[e1] & neqs[e2])
2137                   | (neqs[e1] & peqs[e2]));
2138             pp = peqs[e1] | peqs[e2];
2139             pn = neqs[e1] | neqs[e2];
2140
2141             for (e3 = pb->num_geqs - 1; e3 >= 0; e3--)
2142               if (e3 != e1 && e3 != e2)
2143                 {
2144                   if (!implies (zeqs[e3], pz))
2145                     goto nextE3;
2146
2147                   alpha1 = (pb->geqs[e2].coef[q] * pb->geqs[e3].coef[p]
2148                             - pb->geqs[e2].coef[p] * pb->geqs[e3].coef[q]);
2149                   alpha2 = -(pb->geqs[e1].coef[q] * pb->geqs[e3].coef[p]
2150                              - pb->geqs[e1].coef[p] * pb->geqs[e3].coef[q]);
2151                   alpha3 = alpha;
2152
2153                   if (alpha1 * alpha2 <= 0)
2154                     goto nextE3;
2155
2156                   if (alpha1 < 0)
2157                     {
2158                       alpha1 = -alpha1;
2159                       alpha2 = -alpha2;
2160                       alpha3 = -alpha3;
2161                     }
2162
2163                   if (alpha3 > 0)
2164                     {
2165                       /* Trying to prove e3 is redundant.  */
2166                       if (!implies (peqs[e3], pp)
2167                           || !implies (neqs[e3], pn))
2168                         goto nextE3;
2169
2170                       if (pb->geqs[e3].color == omega_black
2171                           && (pb->geqs[e1].color == omega_red
2172                               || pb->geqs[e2].color == omega_red))
2173                         goto nextE3;
2174
2175                       for (k = pb->num_vars; k >= 1; k--)
2176                         if (alpha3 * pb->geqs[e3].coef[k]
2177                             != (alpha1 * pb->geqs[e1].coef[k]
2178                                 + alpha2 * pb->geqs[e2].coef[k]))
2179                           goto nextE3;
2180
2181                       c = (alpha1 * pb->geqs[e1].coef[0]
2182                            + alpha2 * pb->geqs[e2].coef[0]);
2183
2184                       if (c < alpha3 * (pb->geqs[e3].coef[0] + 1))
2185                         {
2186                           if (dump_file && (dump_flags & TDF_DETAILS))
2187                             {
2188                               fprintf (dump_file,
2189                                        "found redundant inequality\n");
2190                               fprintf (dump_file,
2191                                        "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2192                                        alpha1, alpha2, alpha3);
2193
2194                               omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
2195                               fprintf (dump_file, "\n");
2196                               omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2197                               fprintf (dump_file, "\n=> ");
2198                               omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2199                               fprintf (dump_file, "\n\n");
2200                             }
2201
2202                           is_dead[e3] = true;
2203                         }
2204                     }
2205                   else
2206                     {
2207                       /* Trying to prove e3 <= 0 and therefore e3 = 0,
2208                         or trying to prove e3 < 0, and therefore the
2209                         problem has no solutions.  */
2210                       if (!implies (peqs[e3], pn)
2211                           || !implies (neqs[e3], pp))
2212                         goto nextE3;
2213
2214                       if (pb->geqs[e1].color == omega_red
2215                           || pb->geqs[e2].color == omega_red
2216                           || pb->geqs[e3].color == omega_red)
2217                         goto nextE3;
2218
2219                       alpha3 = alpha3;
2220                       /* verify alpha1*v1+alpha2*v2 = alpha3*v3 */
2221                       for (k = pb->num_vars; k >= 1; k--)
2222                         if (alpha3 * pb->geqs[e3].coef[k]
2223                             != (alpha1 * pb->geqs[e1].coef[k]
2224                                 + alpha2 * pb->geqs[e2].coef[k]))
2225                           goto nextE3;
2226
2227                       c = (alpha1 * pb->geqs[e1].coef[0]
2228                            + alpha2 * pb->geqs[e2].coef[0]);
2229
2230                       if (c < alpha3 * (pb->geqs[e3].coef[0]))
2231                         {
2232                           /* We just proved e3 < 0, so no solutions exist.  */
2233                           if (dump_file && (dump_flags & TDF_DETAILS))
2234                             {
2235                               fprintf (dump_file,
2236                                        "found implied over tight inequality\n");
2237                               fprintf (dump_file,
2238                                        "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2239                                        alpha1, alpha2, -alpha3);
2240                               omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
2241                               fprintf (dump_file, "\n");
2242                               omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2243                               fprintf (dump_file, "\n=> not ");
2244                               omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2245                               fprintf (dump_file, "\n\n");
2246                             }
2247                           free (is_dead);
2248                           free (peqs);
2249                           free (zeqs);
2250                           free (neqs);
2251                           return omega_false;
2252                         }
2253                       else if (c < alpha3 * (pb->geqs[e3].coef[0] - 1))
2254                         {
2255                           /* We just proved that e3 <=0, so e3 = 0.  */
2256                           if (dump_file && (dump_flags & TDF_DETAILS))
2257                             {
2258                               fprintf (dump_file,
2259                                        "found implied tight inequality\n");
2260                               fprintf (dump_file,
2261                                        "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2262                                        alpha1, alpha2, -alpha3);
2263                               omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
2264                               fprintf (dump_file, "\n");
2265                               omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2266                               fprintf (dump_file, "\n=> inverse ");
2267                               omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2268                               fprintf (dump_file, "\n\n");
2269                             }
2270
2271                           omega_copy_eqn (&pb->eqs[pb->num_eqs++],
2272                                           &pb->geqs[e3], pb->num_vars);
2273                           gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
2274                           adding_equality_constraint (pb, pb->num_eqs - 1);
2275                           is_dead[e3] = true;
2276                         }
2277                     }
2278                 nextE3:;
2279                 }
2280           }
2281
2282   /* Delete the inequalities that were marked as dead.  */
2283   for (e = pb->num_geqs - 1; e >= 0; e--)
2284     if (is_dead[e])
2285       omega_delete_geq (pb, e, pb->num_vars);
2286
2287   if (!expensive)
2288     goto eliminate_redundant_done;
2289
2290   tmp_problem = XNEW (struct omega_pb);
2291   conservative++;
2292
2293   for (e = pb->num_geqs - 1; e >= 0; e--)
2294     {
2295       if (dump_file && (dump_flags & TDF_DETAILS))
2296         {
2297           fprintf (dump_file,
2298                    "checking equation %d to see if it is redundant: ", e);
2299           omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2300           fprintf (dump_file, "\n");
2301         }
2302
2303       omega_copy_problem (tmp_problem, pb);
2304       omega_negate_geq (tmp_problem, e);
2305       tmp_problem->safe_vars = 0;
2306       tmp_problem->variables_freed = false;
2307
2308       if (omega_solve_problem (tmp_problem, omega_false) == omega_false)
2309         omega_delete_geq (pb, e, pb->num_vars);
2310     }
2311
2312   free (tmp_problem);
2313   conservative--;
2314
2315   if (!omega_reduce_with_subs)
2316     {
2317       resurrect_subs (pb);
2318       gcc_assert (please_no_equalities_in_simplified_problems
2319                   || pb->num_subs == 0);
2320     }
2321
2322  eliminate_redundant_done:
2323   free (is_dead);
2324   free (peqs);
2325   free (zeqs);
2326   free (neqs);
2327   return omega_true;
2328 }
2329
2330 /* For each inequality that has coefficients bigger than 20, try to
2331    create a new constraint that cannot be derived from the original
2332    constraint and that has smaller coefficients.  Add the new
2333    constraint at the end of geqs.  Return the number of inequalities
2334    that have been added to PB.  */
2335
2336 static int
2337 smooth_weird_equations (omega_pb pb)
2338 {
2339   int e1, e2, e3, p, q, k, alpha, alpha1, alpha2, alpha3;
2340   int c;
2341   int v;
2342   int result = 0;
2343
2344   for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
2345     if (pb->geqs[e1].color == omega_black)
2346       {
2347         int g = 999999;
2348
2349         for (v = pb->num_vars; v >= 1; v--)
2350           if (pb->geqs[e1].coef[v] != 0 && abs (pb->geqs[e1].coef[v]) < g)
2351             g = abs (pb->geqs[e1].coef[v]);
2352
2353         /* Magic number.  */
2354         if (g > 20)
2355           {
2356             e3 = pb->num_geqs;
2357
2358             for (v = pb->num_vars; v >= 1; v--)
2359               pb->geqs[e3].coef[v] = int_div (6 * pb->geqs[e1].coef[v] + g / 2,
2360                                               g);
2361
2362             pb->geqs[e3].color = omega_black;
2363             pb->geqs[e3].touched = 1;
2364             /* Magic number.  */
2365             pb->geqs[e3].coef[0] = 9997;
2366
2367             if (dump_file && (dump_flags & TDF_DETAILS))
2368               {
2369                 fprintf (dump_file, "Checking to see if we can derive: ");
2370                 omega_print_geq (dump_file, pb, &pb->geqs[e3]);
2371                 fprintf (dump_file, "\n from: ");
2372                 omega_print_geq (dump_file, pb, &pb->geqs[e1]);
2373                 fprintf (dump_file, "\n");
2374               }
2375
2376             for (e2 = pb->num_geqs - 1; e2 >= 0; e2--)
2377               if (e1 != e2 && pb->geqs[e2].color == omega_black)
2378                 {
2379                   for (p = pb->num_vars; p > 1; p--)
2380                     {
2381                       for (q = p - 1; q > 0; q--)
2382                         {
2383                           alpha =
2384                             (pb->geqs[e1].coef[p] * pb->geqs[e2].coef[q] -
2385                              pb->geqs[e2].coef[p] * pb->geqs[e1].coef[q]);
2386                           if (alpha != 0)
2387                             goto foundPQ;
2388                         }
2389                     }
2390                   continue;
2391
2392                 foundPQ:
2393
2394                   alpha1 = (pb->geqs[e2].coef[q] * pb->geqs[e3].coef[p]
2395                             - pb->geqs[e2].coef[p] * pb->geqs[e3].coef[q]);
2396                   alpha2 = -(pb->geqs[e1].coef[q] * pb->geqs[e3].coef[p]
2397                              - pb->geqs[e1].coef[p] * pb->geqs[e3].coef[q]);
2398                   alpha3 = alpha;
2399
2400                   if (alpha1 * alpha2 <= 0)
2401                     continue;
2402
2403                   if (alpha1 < 0)
2404                     {
2405                       alpha1 = -alpha1;
2406                       alpha2 = -alpha2;
2407                       alpha3 = -alpha3;
2408                     }
2409
2410                   if (alpha3 > 0)
2411                     {
2412                       /* Try to prove e3 is redundant: verify
2413                          alpha1*v1 + alpha2*v2 = alpha3*v3.  */
2414                       for (k = pb->num_vars; k >= 1; k--)
2415                         if (alpha3 * pb->geqs[e3].coef[k]
2416                             != (alpha1 * pb->geqs[e1].coef[k]
2417                                 + alpha2 * pb->geqs[e2].coef[k]))
2418                           goto nextE2;
2419
2420                       c = alpha1 * pb->geqs[e1].coef[0]
2421                         + alpha2 * pb->geqs[e2].coef[0];
2422
2423                       if (c < alpha3 * (pb->geqs[e3].coef[0] + 1))
2424                         pb->geqs[e3].coef[0] = int_div (c, alpha3);
2425                     }
2426                 nextE2:;
2427                 }
2428
2429             if (pb->geqs[e3].coef[0] < 9997)
2430               {
2431                 result++;
2432                 pb->num_geqs++;
2433
2434                 if (dump_file && (dump_flags & TDF_DETAILS))
2435                   {
2436                     fprintf (dump_file,
2437                              "Smoothing weird equations; adding:\n");
2438                     omega_print_geq (dump_file, pb, &pb->geqs[e3]);
2439                     fprintf (dump_file, "\nto:\n");
2440                     omega_print_problem (dump_file, pb);
2441                     fprintf (dump_file, "\n\n");
2442                   }
2443               }
2444           }
2445       }
2446   return result;
2447 }
2448
2449 /* Replace tuples of inequalities, that define upper and lower half
2450    spaces, with an equation.  */
2451
2452 static void
2453 coalesce (omega_pb pb)
2454 {
2455   int e, e2;
2456   int colors = 0;
2457   bool *is_dead;
2458   int found_something = 0;
2459
2460   for (e = 0; e < pb->num_geqs; e++)
2461     if (pb->geqs[e].color == omega_red)
2462       colors++;
2463
2464   if (colors < 2)
2465     return;
2466
2467   is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
2468
2469   for (e = 0; e < pb->num_geqs; e++)
2470     is_dead[e] = false;
2471
2472   for (e = 0; e < pb->num_geqs; e++)
2473     if (pb->geqs[e].color == omega_red
2474         && !pb->geqs[e].touched)
2475       for (e2 = e + 1; e2 < pb->num_geqs; e2++)
2476         if (!pb->geqs[e2].touched
2477             && pb->geqs[e].key == -pb->geqs[e2].key
2478             && pb->geqs[e].coef[0] == -pb->geqs[e2].coef[0]
2479             && pb->geqs[e2].color == omega_red)
2480           {
2481             omega_copy_eqn (&pb->eqs[pb->num_eqs++], &pb->geqs[e],
2482                             pb->num_vars);
2483             gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
2484             found_something++;
2485             is_dead[e] = true;
2486             is_dead[e2] = true;
2487           }
2488
2489   for (e = pb->num_geqs - 1; e >= 0; e--)
2490     if (is_dead[e])
2491       omega_delete_geq (pb, e, pb->num_vars);
2492
2493   if (dump_file && (dump_flags & TDF_DETAILS) && found_something)
2494     {
2495       fprintf (dump_file, "Coalesced pb->geqs into %d EQ's:\n",
2496                found_something);
2497       omega_print_problem (dump_file, pb);
2498     }
2499
2500   free (is_dead);
2501 }
2502
2503 /* Eliminate red inequalities from PB.  When ELIMINATE_ALL is
2504    true, continue to eliminate all the red inequalities.  */
2505
2506 void
2507 omega_eliminate_red (omega_pb pb, bool eliminate_all)
2508 {
2509   int e, e2, e3, i, j, k, a, alpha1, alpha2;
2510   int c = 0;
2511   bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
2512   int dead_count = 0;
2513   int red_found;
2514   omega_pb tmp_problem;
2515
2516   if (dump_file && (dump_flags & TDF_DETAILS))
2517     {
2518       fprintf (dump_file, "in eliminate RED:\n");
2519       omega_print_problem (dump_file, pb);
2520     }
2521
2522   if (pb->num_eqs > 0)
2523     omega_simplify_problem (pb);
2524
2525   for (e = pb->num_geqs - 1; e >= 0; e--)
2526     is_dead[e] = false;
2527
2528   for (e = pb->num_geqs - 1; e >= 0; e--)
2529     if (pb->geqs[e].color == omega_black && !is_dead[e])
2530       for (e2 = e - 1; e2 >= 0; e2--)
2531         if (pb->geqs[e2].color == omega_black
2532             && !is_dead[e2])
2533           {
2534             a = 0;
2535
2536             for (i = pb->num_vars; i > 1; i--)
2537               for (j = i - 1; j > 0; j--)
2538                 if ((a = (pb->geqs[e].coef[i] * pb->geqs[e2].coef[j]
2539                           - pb->geqs[e2].coef[i] * pb->geqs[e].coef[j])) != 0)
2540                   goto found_pair;
2541
2542             continue;
2543
2544           found_pair:
2545             if (dump_file && (dump_flags & TDF_DETAILS))
2546               {
2547                 fprintf (dump_file,
2548                          "found two equations to combine, i = %s, ",
2549                          omega_variable_to_str (pb, i));
2550                 fprintf (dump_file, "j = %s, alpha = %d\n",
2551                          omega_variable_to_str (pb, j), a);
2552                 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2553                 fprintf (dump_file, "\n");
2554                 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2555                 fprintf (dump_file, "\n");
2556               }
2557
2558             for (e3 = pb->num_geqs - 1; e3 >= 0; e3--)
2559               if (pb->geqs[e3].color == omega_red)
2560                 {
2561                   alpha1 = (pb->geqs[e2].coef[j] * pb->geqs[e3].coef[i]
2562                             - pb->geqs[e2].coef[i] * pb->geqs[e3].coef[j]);
2563                   alpha2 = -(pb->geqs[e].coef[j] * pb->geqs[e3].coef[i]
2564                              - pb->geqs[e].coef[i] * pb->geqs[e3].coef[j]);
2565
2566                   if ((a > 0 && alpha1 > 0 && alpha2 > 0)
2567                       || (a < 0 && alpha1 < 0 && alpha2 < 0))
2568                     {
2569                       if (dump_file && (dump_flags & TDF_DETAILS))
2570                         {
2571                           fprintf (dump_file,
2572                                    "alpha1 = %d, alpha2 = %d;"
2573                                    "comparing against: ",
2574                                    alpha1, alpha2);
2575                           omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2576                           fprintf (dump_file, "\n");
2577                         }
2578
2579                       for (k = pb->num_vars; k >= 0; k--)
2580                         {
2581                           c = (alpha1 * pb->geqs[e].coef[k]
2582                                + alpha2 * pb->geqs[e2].coef[k]);
2583
2584                           if (c != a * pb->geqs[e3].coef[k])
2585                             break;
2586
2587                           if (dump_file && (dump_flags & TDF_DETAILS) && k > 0)
2588                             fprintf (dump_file, " %s: %d, %d\n",
2589                                      omega_variable_to_str (pb, k), c,
2590                                      a * pb->geqs[e3].coef[k]);
2591                         }
2592
2593                       if (k < 0
2594                           || (k == 0 &&
2595                               ((a > 0 && c < a * pb->geqs[e3].coef[k])
2596                                || (a < 0 && c > a * pb->geqs[e3].coef[k]))))
2597                         {
2598                           if (dump_file && (dump_flags & TDF_DETAILS))
2599                             {
2600                               dead_count++;
2601                               fprintf (dump_file,
2602                                        "red equation#%d is dead "
2603                                        "(%d dead so far, %d remain)\n",
2604                                        e3, dead_count,
2605                                        pb->num_geqs - dead_count);
2606                               omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2607                               fprintf (dump_file, "\n");
2608                               omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2609                               fprintf (dump_file, "\n");
2610                               omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2611                               fprintf (dump_file, "\n");
2612                             }
2613                           is_dead[e3] = true;
2614                         }
2615                     }
2616                 }
2617           }
2618
2619   for (e = pb->num_geqs - 1; e >= 0; e--)
2620     if (is_dead[e])
2621       omega_delete_geq (pb, e, pb->num_vars);
2622
2623   free (is_dead);
2624
2625   if (dump_file && (dump_flags & TDF_DETAILS))
2626     {
2627       fprintf (dump_file, "in eliminate RED, easy tests done:\n");
2628       omega_print_problem (dump_file, pb);
2629     }
2630
2631   for (red_found = 0, e = pb->num_geqs - 1; e >= 0; e--)
2632     if (pb->geqs[e].color == omega_red)
2633       red_found = 1;
2634
2635   if (!red_found)
2636     {
2637       if (dump_file && (dump_flags & TDF_DETAILS))
2638         fprintf (dump_file, "fast checks worked\n");
2639
2640       if (!omega_reduce_with_subs)
2641         gcc_assert (please_no_equalities_in_simplified_problems
2642                     || pb->num_subs == 0);
2643
2644       return;
2645     }
2646
2647   if (!omega_verify_simplification
2648       && verify_omega_pb (pb) == omega_false)
2649     return;
2650
2651   conservative++;
2652   tmp_problem = XNEW (struct omega_pb);
2653
2654   for (e = pb->num_geqs - 1; e >= 0; e--)
2655     if (pb->geqs[e].color == omega_red)
2656       {
2657         if (dump_file && (dump_flags & TDF_DETAILS))
2658           {
2659             fprintf (dump_file,
2660                      "checking equation %d to see if it is redundant: ", e);
2661             omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2662             fprintf (dump_file, "\n");
2663           }
2664
2665         omega_copy_problem (tmp_problem, pb);
2666         omega_negate_geq (tmp_problem, e);
2667         tmp_problem->safe_vars = 0;
2668         tmp_problem->variables_freed = false;
2669         tmp_problem->num_subs = 0;
2670
2671         if (omega_solve_problem (tmp_problem, omega_false) == omega_false)
2672           {
2673             if (dump_file && (dump_flags & TDF_DETAILS))
2674               fprintf (dump_file, "it is redundant\n");
2675             omega_delete_geq (pb, e, pb->num_vars);
2676           }
2677         else
2678           {
2679             if (dump_file && (dump_flags & TDF_DETAILS))
2680               fprintf (dump_file, "it is not redundant\n");
2681
2682             if (!eliminate_all)
2683               {
2684                 if (dump_file && (dump_flags & TDF_DETAILS))
2685                   fprintf (dump_file, "no need to check other red equations\n");
2686                 break;
2687               }
2688           }
2689       }
2690
2691   conservative--;
2692   free (tmp_problem);
2693   /* omega_simplify_problem (pb); */
2694
2695   if (!omega_reduce_with_subs)
2696     gcc_assert (please_no_equalities_in_simplified_problems
2697                 || pb->num_subs == 0);
2698 }
2699
2700 /* Transform some wildcard variables to non-safe variables.  */
2701
2702 static void
2703 chain_unprotect (omega_pb pb)
2704 {
2705   int i, e;
2706   bool *unprotect = XNEWVEC (bool, OMEGA_MAX_VARS);
2707
2708   for (i = 1; omega_safe_var_p (pb, i); i++)
2709     {
2710       unprotect[i] = omega_wildcard_p (pb, i);
2711
2712       for (e = pb->num_subs - 1; e >= 0; e--)
2713         if (pb->subs[e].coef[i])
2714           unprotect[i] = false;
2715     }
2716
2717   if (dump_file && (dump_flags & TDF_DETAILS))
2718     {
2719       fprintf (dump_file, "Doing chain reaction unprotection\n");
2720       omega_print_problem (dump_file, pb);
2721
2722       for (i = 1; omega_safe_var_p (pb, i); i++)
2723         if (unprotect[i])
2724           fprintf (dump_file, "unprotecting %s\n",
2725                    omega_variable_to_str (pb, i));
2726     }
2727
2728   for (i = 1; omega_safe_var_p (pb, i); i++)
2729     if (unprotect[i])
2730       omega_unprotect_1 (pb, &i, unprotect);
2731
2732   if (dump_file && (dump_flags & TDF_DETAILS))
2733     {
2734       fprintf (dump_file, "After chain reactions\n");
2735       omega_print_problem (dump_file, pb);
2736     }
2737
2738   free (unprotect);
2739 }
2740
2741 /* Reduce problem PB.  */
2742
2743 static void
2744 omega_problem_reduced (omega_pb pb)
2745 {
2746   if (omega_verify_simplification
2747       && !in_approximate_mode
2748       && verify_omega_pb (pb) == omega_false)
2749     return;
2750
2751   if (PARAM_VALUE (PARAM_OMEGA_ELIMINATE_REDUNDANT_CONSTRAINTS)
2752       && !omega_eliminate_redundant (pb, true))
2753     return;
2754
2755   omega_found_reduction = omega_true;
2756
2757   if (!please_no_equalities_in_simplified_problems)
2758     coalesce (pb);
2759
2760   if (omega_reduce_with_subs
2761       || please_no_equalities_in_simplified_problems)
2762     chain_unprotect (pb);
2763   else
2764     resurrect_subs (pb);
2765
2766   if (!return_single_result)
2767     {
2768       int i;
2769
2770       for (i = 1; omega_safe_var_p (pb, i); i++)
2771         pb->forwarding_address[pb->var[i]] = i;
2772
2773       for (i = 0; i < pb->num_subs; i++)
2774         pb->forwarding_address[pb->subs[i].key] = -i - 1;
2775
2776       (*omega_when_reduced) (pb);
2777     }
2778
2779   if (dump_file && (dump_flags & TDF_DETAILS))
2780     {
2781       fprintf (dump_file, "-------------------------------------------\n");
2782       fprintf (dump_file, "problem reduced:\n");
2783       omega_print_problem (dump_file, pb);
2784       fprintf (dump_file, "-------------------------------------------\n");
2785     }
2786 }
2787
2788 /* Eliminates all the free variables for problem PB, that is all the
2789    variables from FV to PB->NUM_VARS.  */
2790
2791 static void
2792 omega_free_eliminations (omega_pb pb, int fv)
2793 {
2794   bool try_again = true;
2795   int i, e, e2;
2796   int n_vars = pb->num_vars;
2797
2798   while (try_again)
2799     {
2800       try_again = false;
2801
2802       for (i = n_vars; i > fv; i--)
2803         {
2804           for (e = pb->num_geqs - 1; e >= 0; e--)
2805             if (pb->geqs[e].coef[i])
2806               break;
2807
2808           if (e < 0)
2809             e2 = e;
2810           else if (pb->geqs[e].coef[i] > 0)
2811             {
2812               for (e2 = e - 1; e2 >= 0; e2--)
2813                 if (pb->geqs[e2].coef[i] < 0)
2814                   break;
2815             }
2816           else
2817             {
2818               for (e2 = e - 1; e2 >= 0; e2--)
2819                 if (pb->geqs[e2].coef[i] > 0)
2820                   break;
2821             }
2822
2823           if (e2 < 0)
2824             {
2825               int e3;
2826               for (e3 = pb->num_subs - 1; e3 >= 0; e3--)
2827                 if (pb->subs[e3].coef[i])
2828                   break;
2829
2830               if (e3 >= 0)
2831                 continue;
2832
2833               for (e3 = pb->num_eqs - 1; e3 >= 0; e3--)
2834                 if (pb->eqs[e3].coef[i])
2835                   break;
2836
2837               if (e3 >= 0)
2838                 continue;
2839
2840               if (dump_file && (dump_flags & TDF_DETAILS))
2841                 fprintf (dump_file, "a free elimination of %s\n",
2842                          omega_variable_to_str (pb, i));
2843
2844               if (e >= 0)
2845                 {
2846                   omega_delete_geq (pb, e, n_vars);
2847
2848                   for (e--; e >= 0; e--)
2849                     if (pb->geqs[e].coef[i])
2850                       omega_delete_geq (pb, e, n_vars);
2851
2852                   try_again = (i < n_vars);
2853                 }
2854
2855               omega_delete_variable (pb, i);
2856               n_vars = pb->num_vars;
2857             }
2858         }
2859     }
2860
2861   if (dump_file && (dump_flags & TDF_DETAILS))
2862     {
2863       fprintf (dump_file, "\nafter free eliminations:\n");
2864       omega_print_problem (dump_file, pb);
2865       fprintf (dump_file, "\n");
2866     }
2867 }
2868
2869 /* Do free red eliminations.  */
2870
2871 static void
2872 free_red_eliminations (omega_pb pb)
2873 {
2874   bool try_again = true;
2875   int i, e, e2;
2876   int n_vars = pb->num_vars;
2877   bool *is_red_var = XNEWVEC (bool, OMEGA_MAX_VARS);
2878   bool *is_dead_var = XNEWVEC (bool, OMEGA_MAX_VARS);
2879   bool *is_dead_geq = XNEWVEC (bool, OMEGA_MAX_GEQS);
2880
2881   for (i = n_vars; i > 0; i--)
2882     {
2883       is_red_var[i] = false;
2884       is_dead_var[i] = false;
2885     }
2886
2887   for (e = pb->num_geqs - 1; e >= 0; e--)
2888     {
2889       is_dead_geq[e] = false;
2890
2891       if (pb->geqs[e].color == omega_red)
2892         for (i = n_vars; i > 0; i--)
2893           if (pb->geqs[e].coef[i] != 0)
2894             is_red_var[i] = true;
2895     }
2896
2897   while (try_again)
2898     {
2899       try_again = false;
2900       for (i = n_vars; i > 0; i--)
2901         if (!is_red_var[i] && !is_dead_var[i])
2902           {
2903             for (e = pb->num_geqs - 1; e >= 0; e--)
2904               if (!is_dead_geq[e] && pb->geqs[e].coef[i])
2905                 break;
2906
2907             if (e < 0)
2908               e2 = e;
2909             else if (pb->geqs[e].coef[i] > 0)
2910               {
2911                 for (e2 = e - 1; e2 >= 0; e2--)
2912                   if (!is_dead_geq[e2] && pb->geqs[e2].coef[i] < 0)
2913                     break;
2914               }
2915             else
2916               {
2917                 for (e2 = e - 1; e2 >= 0; e2--)
2918                   if (!is_dead_geq[e2] && pb->geqs[e2].coef[i] > 0)
2919                     break;
2920               }
2921
2922             if (e2 < 0)
2923               {
2924                 int e3;
2925                 for (e3 = pb->num_subs - 1; e3 >= 0; e3--)
2926                   if (pb->subs[e3].coef[i])
2927                     break;
2928
2929                 if (e3 >= 0)
2930                   continue;
2931
2932                 for (e3 = pb->num_eqs - 1; e3 >= 0; e3--)
2933                   if (pb->eqs[e3].coef[i])
2934                     break;
2935
2936                 if (e3 >= 0)
2937                   continue;
2938
2939                 if (dump_file && (dump_flags & TDF_DETAILS))
2940                   fprintf (dump_file, "a free red elimination of %s\n",
2941                            omega_variable_to_str (pb, i));
2942
2943                 for (; e >= 0; e--)
2944                   if (pb->geqs[e].coef[i])
2945                     is_dead_geq[e] = true;
2946
2947                 try_again = true;
2948                 is_dead_var[i] = true;
2949               }
2950           }
2951     }
2952
2953   for (e = pb->num_geqs - 1; e >= 0; e--)
2954     if (is_dead_geq[e])
2955       omega_delete_geq (pb, e, n_vars);
2956
2957   for (i = n_vars; i > 0; i--)
2958     if (is_dead_var[i])
2959       omega_delete_variable (pb, i);
2960
2961   if (dump_file && (dump_flags & TDF_DETAILS))
2962     {
2963       fprintf (dump_file, "\nafter free red eliminations:\n");
2964       omega_print_problem (dump_file, pb);
2965       fprintf (dump_file, "\n");
2966     }
2967
2968   free (is_red_var);
2969   free (is_dead_var);
2970   free (is_dead_geq);
2971 }
2972
2973 /* For equation EQ of the form "0 = EQN", insert in PB two
2974    inequalities "0 <= EQN" and "0 <= -EQN".  */
2975
2976 void
2977 omega_convert_eq_to_geqs (omega_pb pb, int eq)
2978 {
2979   int i;
2980
2981   if (dump_file && (dump_flags & TDF_DETAILS))
2982     fprintf (dump_file, "Converting Eq to Geqs\n");
2983
2984   /* Insert "0 <= EQN".  */
2985   omega_copy_eqn (&pb->geqs[pb->num_geqs], &pb->eqs[eq], pb->num_vars);
2986   pb->geqs[pb->num_geqs].touched = 1;
2987   pb->num_geqs++;
2988
2989   /* Insert "0 <= -EQN".  */
2990   omega_copy_eqn (&pb->geqs[pb->num_geqs], &pb->eqs[eq], pb->num_vars);
2991   pb->geqs[pb->num_geqs].touched = 1;
2992
2993   for (i = 0; i <= pb->num_vars; i++)
2994     pb->geqs[pb->num_geqs].coef[i] *= -1;
2995
2996   pb->num_geqs++;
2997
2998   if (dump_file && (dump_flags & TDF_DETAILS))
2999     omega_print_problem (dump_file, pb);
3000 }
3001
3002 /* Eliminates variable I from PB.  */
3003
3004 static void
3005 omega_do_elimination (omega_pb pb, int e, int i)
3006 {
3007   eqn sub = omega_alloc_eqns (0, 1);
3008   int c;
3009   int n_vars = pb->num_vars;
3010
3011   if (dump_file && (dump_flags & TDF_DETAILS))
3012     fprintf (dump_file, "eliminating variable %s\n",
3013              omega_variable_to_str (pb, i));
3014
3015   omega_copy_eqn (sub, &pb->eqs[e], pb->num_vars);
3016   c = sub->coef[i];
3017   sub->coef[i] = 0;
3018   if (c == 1 || c == -1)
3019     {
3020       if (pb->eqs[e].color == omega_red)
3021         {
3022           bool fB;
3023           omega_substitute_red (pb, sub, i, c, &fB);
3024           if (fB)
3025             omega_convert_eq_to_geqs (pb, e);
3026           else
3027             omega_delete_variable (pb, i);
3028         }
3029       else
3030         {
3031           omega_substitute (pb, sub, i, c);
3032           omega_delete_variable (pb, i);
3033         }
3034     }
3035   else
3036     {
3037       int a = abs (c);
3038       int e2 = e;
3039
3040       if (dump_file && (dump_flags & TDF_DETAILS))
3041         fprintf (dump_file, "performing non-exact elimination, c = %d\n", c);
3042
3043       for (e = pb->num_eqs - 1; e >= 0; e--)
3044         if (pb->eqs[e].coef[i])
3045           {
3046             eqn eqn = &(pb->eqs[e]);
3047             int j, k;
3048             for (j = n_vars; j >= 0; j--)
3049               eqn->coef[j] *= a;
3050             k = eqn->coef[i];
3051             eqn->coef[i] = 0;
3052             eqn->color |= sub->color;
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);
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);
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 }