gcc/omega.c

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