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