gcc/omega.c

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