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