gcc/omega.c

   1 /* Source code for an implementation of the Omega test, an integer
   2    programming algorithm for dependence analysis, by William Pugh,
   3    appeared in Supercomputing '91 and CACM Aug 92.
   4
   5    This code has no license restrictions, and is considered public
   6    domain.
   7
   8    Changes copyright (C) 2005, 2006, 2007, 2008, 2009,
   9    2010 Free Software Foundation, Inc.
  10    Contributed by Sebastian Pop <sebastian.pop@inria.fr>
  11
  12 This file is part of GCC.
  13
  14 GCC is free software; you can redistribute it and/or modify it under
  15 the terms of the GNU General Public License as published by the Free
  16 Software Foundation; either version 3, or (at your option) any later
  17 version.
  18
  19 GCC is distributed in the hope that it will be useful, but WITHOUT ANY
  20 WARRANTY; without even the implied warranty of MERCHANTABILITY or
  21 FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
  22 for more details.
  23
  24 You should have received a copy of the GNU General Public License
  25 along with GCC; see the file COPYING3.  If not see
  26 <http://www.gnu.org/licenses/>.  */
  27
  28 /* For a detailed description, see "Constraint-Based Array Dependence
  29    Analysis" William Pugh, David Wonnacott, TOPLAS'98 and David
  30    Wonnacott's thesis:
  31    ftp://ftp.cs.umd.edu/pub/omega/davewThesis/davewThesis.ps.gz
  32 */
  33
  34 #include "config.h"
  35 #include "system.h"
  36 #include "coretypes.h"
  37 #include "tm.h"
  38 #include "ggc.h"
  39 #include "tree.h"
  40 #include "diagnostic-core.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 DEBUG_FUNCTION 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                       /* verify alpha1*v1+alpha2*v2 = alpha3*v3 */
2217                       for (k = pb->num_vars; k >= 1; k--)
2218                         if (alpha3 * pb->geqs[e3].coef[k]
2219                             != (alpha1 * pb->geqs[e1].coef[k]
2220                                 + alpha2 * pb->geqs[e2].coef[k]))
2221                           goto nextE3;
2222
2223                       c = (alpha1 * pb->geqs[e1].coef[0]
2224                            + alpha2 * pb->geqs[e2].coef[0]);
2225
2226                       if (c < alpha3 * (pb->geqs[e3].coef[0]))
2227                         {
2228                           /* We just proved e3 < 0, so no solutions exist.  */
2229                           if (dump_file && (dump_flags & TDF_DETAILS))
2230                             {
2231                               fprintf (dump_file,
2232                                        "found implied over tight inequality\n");
2233                               fprintf (dump_file,
2234                                        "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2235                                        alpha1, alpha2, -alpha3);
2236                               omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
2237                               fprintf (dump_file, "\n");
2238                               omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2239                               fprintf (dump_file, "\n=> not ");
2240                               omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2241                               fprintf (dump_file, "\n\n");
2242                             }
2243                           free (is_dead);
2244                           free (peqs);
2245                           free (zeqs);
2246                           free (neqs);
2247                           return omega_false;
2248                         }
2249                       else if (c < alpha3 * (pb->geqs[e3].coef[0] - 1))
2250                         {
2251                           /* We just proved that e3 <=0, so e3 = 0.  */
2252                           if (dump_file && (dump_flags & TDF_DETAILS))
2253                             {
2254                               fprintf (dump_file,
2255                                        "found implied tight inequality\n");
2256                               fprintf (dump_file,
2257                                        "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2258                                        alpha1, alpha2, -alpha3);
2259                               omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
2260                               fprintf (dump_file, "\n");
2261                               omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2262                               fprintf (dump_file, "\n=> inverse ");
2263                               omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2264                               fprintf (dump_file, "\n\n");
2265                             }
2266
2267                           omega_copy_eqn (&pb->eqs[pb->num_eqs++],
2268                                           &pb->geqs[e3], pb->num_vars);
2269                           gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
2270                           adding_equality_constraint (pb, pb->num_eqs - 1);
2271                           is_dead[e3] = true;
2272                         }
2273                     }
2274                 nextE3:;
2275                 }
2276           }
2277
2278   /* Delete the inequalities that were marked as dead.  */
2279   for (e = pb->num_geqs - 1; e >= 0; e--)
2280     if (is_dead[e])
2281       omega_delete_geq (pb, e, pb->num_vars);
2282
2283   if (!expensive)
2284     goto eliminate_redundant_done;
2285
2286   tmp_problem = XNEW (struct omega_pb_d);
2287   conservative++;
2288
2289   for (e = pb->num_geqs - 1; e >= 0; e--)
2290     {
2291       if (dump_file && (dump_flags & TDF_DETAILS))
2292         {
2293           fprintf (dump_file,
2294                    "checking equation %d to see if it is redundant: ", e);
2295           omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2296           fprintf (dump_file, "\n");
2297         }
2298
2299       omega_copy_problem (tmp_problem, pb);
2300       omega_negate_geq (tmp_problem, e);
2301       tmp_problem->safe_vars = 0;
2302       tmp_problem->variables_freed = false;
2303
2304       if (omega_solve_problem (tmp_problem, omega_false) == omega_false)
2305         omega_delete_geq (pb, e, pb->num_vars);
2306     }
2307
2308   free (tmp_problem);
2309   conservative--;
2310
2311   if (!omega_reduce_with_subs)
2312     {
2313       resurrect_subs (pb);
2314       gcc_assert (please_no_equalities_in_simplified_problems
2315                   || pb->num_subs == 0);
2316     }
2317
2318  eliminate_redundant_done:
2319   free (is_dead);
2320   free (peqs);
2321   free (zeqs);
2322   free (neqs);
2323   return omega_true;
2324 }
2325
2326 /* For each inequality that has coefficients bigger than 20, try to
2327    create a new constraint that cannot be derived from the original
2328    constraint and that has smaller coefficients.  Add the new
2329    constraint at the end of geqs.  Return the number of inequalities
2330    that have been added to PB.  */
2331
2332 static int
2333 smooth_weird_equations (omega_pb pb)
2334 {
2335   int e1, e2, e3, p, q, k, alpha, alpha1, alpha2, alpha3;
2336   int c;
2337   int v;
2338   int result = 0;
2339
2340   for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
2341     if (pb->geqs[e1].color == omega_black)
2342       {
2343         int g = 999999;
2344
2345         for (v = pb->num_vars; v >= 1; v--)
2346           if (pb->geqs[e1].coef[v] != 0 && abs (pb->geqs[e1].coef[v]) < g)
2347             g = abs (pb->geqs[e1].coef[v]);
2348
2349         /* Magic number.  */
2350         if (g > 20)
2351           {
2352             e3 = pb->num_geqs;
2353
2354             for (v = pb->num_vars; v >= 1; v--)
2355               pb->geqs[e3].coef[v] = int_div (6 * pb->geqs[e1].coef[v] + g / 2,
2356                                               g);
2357
2358             pb->geqs[e3].color = omega_black;
2359             pb->geqs[e3].touched = 1;
2360             /* Magic number.  */
2361             pb->geqs[e3].coef[0] = 9997;
2362
2363             if (dump_file && (dump_flags & TDF_DETAILS))
2364               {
2365                 fprintf (dump_file, "Checking to see if we can derive: ");
2366                 omega_print_geq (dump_file, pb, &pb->geqs[e3]);
2367                 fprintf (dump_file, "\n from: ");
2368                 omega_print_geq (dump_file, pb, &pb->geqs[e1]);
2369                 fprintf (dump_file, "\n");
2370               }
2371
2372             for (e2 = pb->num_geqs - 1; e2 >= 0; e2--)
2373               if (e1 != e2 && pb->geqs[e2].color == omega_black)
2374                 {
2375                   for (p = pb->num_vars; p > 1; p--)
2376                     {
2377                       for (q = p - 1; q > 0; q--)
2378                         {
2379                           alpha =
2380                             (pb->geqs[e1].coef[p] * pb->geqs[e2].coef[q] -
2381                              pb->geqs[e2].coef[p] * pb->geqs[e1].coef[q]);
2382                           if (alpha != 0)
2383                             goto foundPQ;
2384                         }
2385                     }
2386                   continue;
2387
2388                 foundPQ:
2389
2390                   alpha1 = (pb->geqs[e2].coef[q] * pb->geqs[e3].coef[p]
2391                             - pb->geqs[e2].coef[p] * pb->geqs[e3].coef[q]);
2392                   alpha2 = -(pb->geqs[e1].coef[q] * pb->geqs[e3].coef[p]
2393                              - pb->geqs[e1].coef[p] * pb->geqs[e3].coef[q]);
2394                   alpha3 = alpha;
2395
2396                   if (alpha1 * alpha2 <= 0)
2397                     continue;
2398
2399                   if (alpha1 < 0)
2400                     {
2401                       alpha1 = -alpha1;
2402                       alpha2 = -alpha2;
2403                       alpha3 = -alpha3;
2404                     }
2405
2406                   if (alpha3 > 0)
2407                     {
2408                       /* Try to prove e3 is redundant: verify
2409                          alpha1*v1 + alpha2*v2 = alpha3*v3.  */
2410                       for (k = pb->num_vars; k >= 1; k--)
2411                         if (alpha3 * pb->geqs[e3].coef[k]
2412                             != (alpha1 * pb->geqs[e1].coef[k]
2413                                 + alpha2 * pb->geqs[e2].coef[k]))
2414                           goto nextE2;
2415
2416                       c = alpha1 * pb->geqs[e1].coef[0]
2417                         + alpha2 * pb->geqs[e2].coef[0];
2418
2419                       if (c < alpha3 * (pb->geqs[e3].coef[0] + 1))
2420                         pb->geqs[e3].coef[0] = int_div (c, alpha3);
2421                     }
2422                 nextE2:;
2423                 }
2424
2425             if (pb->geqs[e3].coef[0] < 9997)
2426               {
2427                 result++;
2428                 pb->num_geqs++;
2429
2430                 if (dump_file && (dump_flags & TDF_DETAILS))
2431                   {
2432                     fprintf (dump_file,
2433                              "Smoothing weird equations; adding:\n");
2434                     omega_print_geq (dump_file, pb, &pb->geqs[e3]);
2435                     fprintf (dump_file, "\nto:\n");
2436                     omega_print_problem (dump_file, pb);
2437                     fprintf (dump_file, "\n\n");
2438                   }
2439               }
2440           }
2441       }
2442   return result;
2443 }
2444
2445 /* Replace tuples of inequalities, that define upper and lower half
2446    spaces, with an equation.  */
2447
2448 static void
2449 coalesce (omega_pb pb)
2450 {
2451   int e, e2;
2452   int colors = 0;
2453   bool *is_dead;
2454   int found_something = 0;
2455
2456   for (e = 0; e < pb->num_geqs; e++)
2457     if (pb->geqs[e].color == omega_red)
2458       colors++;
2459
2460   if (colors < 2)
2461     return;
2462
2463   is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
2464
2465   for (e = 0; e < pb->num_geqs; e++)
2466     is_dead[e] = false;
2467
2468   for (e = 0; e < pb->num_geqs; e++)
2469     if (pb->geqs[e].color == omega_red
2470         && !pb->geqs[e].touched)
2471       for (e2 = e + 1; e2 < pb->num_geqs; e2++)
2472         if (!pb->geqs[e2].touched
2473             && pb->geqs[e].key == -pb->geqs[e2].key
2474             && pb->geqs[e].coef[0] == -pb->geqs[e2].coef[0]
2475             && pb->geqs[e2].color == omega_red)
2476           {
2477             omega_copy_eqn (&pb->eqs[pb->num_eqs++], &pb->geqs[e],
2478                             pb->num_vars);
2479             gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
2480             found_something++;
2481             is_dead[e] = true;
2482             is_dead[e2] = true;
2483           }
2484
2485   for (e = pb->num_geqs - 1; e >= 0; e--)
2486     if (is_dead[e])
2487       omega_delete_geq (pb, e, pb->num_vars);
2488
2489   if (dump_file && (dump_flags & TDF_DETAILS) && found_something)
2490     {
2491       fprintf (dump_file, "Coalesced pb->geqs into %d EQ's:\n",
2492                found_something);
2493       omega_print_problem (dump_file, pb);
2494     }
2495
2496   free (is_dead);
2497 }
2498
2499 /* Eliminate red inequalities from PB.  When ELIMINATE_ALL is
2500    true, continue to eliminate all the red inequalities.  */
2501
2502 void
2503 omega_eliminate_red (omega_pb pb, bool eliminate_all)
2504 {
2505   int e, e2, e3, i, j, k, a, alpha1, alpha2;
2506   int c = 0;
2507   bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
2508   int dead_count = 0;
2509   int red_found;
2510   omega_pb tmp_problem;
2511
2512   if (dump_file && (dump_flags & TDF_DETAILS))
2513     {
2514       fprintf (dump_file, "in eliminate RED:\n");
2515       omega_print_problem (dump_file, pb);
2516     }
2517
2518   if (pb->num_eqs > 0)
2519     omega_simplify_problem (pb);
2520
2521   for (e = pb->num_geqs - 1; e >= 0; e--)
2522     is_dead[e] = false;
2523
2524   for (e = pb->num_geqs - 1; e >= 0; e--)
2525     if (pb->geqs[e].color == omega_black && !is_dead[e])
2526       for (e2 = e - 1; e2 >= 0; e2--)
2527         if (pb->geqs[e2].color == omega_black
2528             && !is_dead[e2])
2529           {
2530             a = 0;
2531
2532             for (i = pb->num_vars; i > 1; i--)
2533               for (j = i - 1; j > 0; j--)
2534                 if ((a = (pb->geqs[e].coef[i] * pb->geqs[e2].coef[j]
2535                           - pb->geqs[e2].coef[i] * pb->geqs[e].coef[j])) != 0)
2536                   goto found_pair;
2537
2538             continue;
2539
2540           found_pair:
2541             if (dump_file && (dump_flags & TDF_DETAILS))
2542               {
2543                 fprintf (dump_file,
2544                          "found two equations to combine, i = %s, ",
2545                          omega_variable_to_str (pb, i));
2546                 fprintf (dump_file, "j = %s, alpha = %d\n",
2547                          omega_variable_to_str (pb, j), a);
2548                 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2549                 fprintf (dump_file, "\n");
2550                 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2551                 fprintf (dump_file, "\n");
2552               }
2553
2554             for (e3 = pb->num_geqs - 1; e3 >= 0; e3--)
2555               if (pb->geqs[e3].color == omega_red)
2556                 {
2557                   alpha1 = (pb->geqs[e2].coef[j] * pb->geqs[e3].coef[i]
2558                             - pb->geqs[e2].coef[i] * pb->geqs[e3].coef[j]);
2559                   alpha2 = -(pb->geqs[e].coef[j] * pb->geqs[e3].coef[i]
2560                              - pb->geqs[e].coef[i] * pb->geqs[e3].coef[j]);
2561
2562                   if ((a > 0 && alpha1 > 0 && alpha2 > 0)
2563                       || (a < 0 && alpha1 < 0 && alpha2 < 0))
2564                     {
2565                       if (dump_file && (dump_flags & TDF_DETAILS))
2566                         {
2567                           fprintf (dump_file,
2568                                    "alpha1 = %d, alpha2 = %d;"
2569                                    "comparing against: ",
2570                                    alpha1, alpha2);
2571                           omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2572                           fprintf (dump_file, "\n");
2573                         }
2574
2575                       for (k = pb->num_vars; k >= 0; k--)
2576                         {
2577                           c = (alpha1 * pb->geqs[e].coef[k]
2578                                + alpha2 * pb->geqs[e2].coef[k]);
2579
2580                           if (c != a * pb->geqs[e3].coef[k])
2581                             break;
2582
2583                           if (dump_file && (dump_flags & TDF_DETAILS) && k > 0)
2584                             fprintf (dump_file, " %s: %d, %d\n",
2585                                      omega_variable_to_str (pb, k), c,
2586                                      a * pb->geqs[e3].coef[k]);
2587                         }
2588
2589                       if (k < 0
2590                           || (k == 0 &&
2591                               ((a > 0 && c < a * pb->geqs[e3].coef[k])
2592                                || (a < 0 && c > a * pb->geqs[e3].coef[k]))))
2593                         {
2594                           if (dump_file && (dump_flags & TDF_DETAILS))
2595                             {
2596                               dead_count++;
2597                               fprintf (dump_file,
2598                                        "red equation#%d is dead "
2599                                        "(%d dead so far, %d remain)\n",
2600                                        e3, dead_count,
2601                                        pb->num_geqs - dead_count);
2602                               omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2603                               fprintf (dump_file, "\n");
2604                               omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2605                               fprintf (dump_file, "\n");
2606                               omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2607                               fprintf (dump_file, "\n");
2608                             }
2609                           is_dead[e3] = true;
2610                         }
2611                     }
2612                 }
2613           }
2614
2615   for (e = pb->num_geqs - 1; e >= 0; e--)
2616     if (is_dead[e])
2617       omega_delete_geq (pb, e, pb->num_vars);
2618
2619   free (is_dead);
2620
2621   if (dump_file && (dump_flags & TDF_DETAILS))
2622     {
2623       fprintf (dump_file, "in eliminate RED, easy tests done:\n");
2624       omega_print_problem (dump_file, pb);
2625     }
2626
2627   for (red_found = 0, e = pb->num_geqs - 1; e >= 0; e--)
2628     if (pb->geqs[e].color == omega_red)
2629       red_found = 1;
2630
2631   if (!red_found)
2632     {
2633       if (dump_file && (dump_flags & TDF_DETAILS))
2634         fprintf (dump_file, "fast checks worked\n");
2635
2636       if (!omega_reduce_with_subs)
2637         gcc_assert (please_no_equalities_in_simplified_problems
2638                     || pb->num_subs == 0);
2639
2640       return;
2641     }
2642
2643   if (!omega_verify_simplification
2644       && verify_omega_pb (pb) == omega_false)
2645     return;
2646
2647   conservative++;
2648   tmp_problem = XNEW (struct omega_pb_d);
2649
2650   for (e = pb->num_geqs - 1; e >= 0; e--)
2651     if (pb->geqs[e].color == omega_red)
2652       {
2653         if (dump_file && (dump_flags & TDF_DETAILS))
2654           {
2655             fprintf (dump_file,
2656                      "checking equation %d to see if it is redundant: ", e);
2657             omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2658             fprintf (dump_file, "\n");
2659           }
2660
2661         omega_copy_problem (tmp_problem, pb);
2662         omega_negate_geq (tmp_problem, e);
2663         tmp_problem->safe_vars = 0;
2664         tmp_problem->variables_freed = false;
2665         tmp_problem->num_subs = 0;
2666
2667         if (omega_solve_problem (tmp_problem, omega_false) == omega_false)
2668           {
2669             if (dump_file && (dump_flags & TDF_DETAILS))
2670               fprintf (dump_file, "it is redundant\n");
2671             omega_delete_geq (pb, e, pb->num_vars);
2672           }
2673         else
2674           {
2675             if (dump_file && (dump_flags & TDF_DETAILS))
2676               fprintf (dump_file, "it is not redundant\n");
2677
2678             if (!eliminate_all)
2679               {
2680                 if (dump_file && (dump_flags & TDF_DETAILS))
2681                   fprintf (dump_file, "no need to check other red equations\n");
2682                 break;
2683               }
2684           }
2685       }
2686
2687   conservative--;
2688   free (tmp_problem);
2689   /* omega_simplify_problem (pb); */
2690
2691   if (!omega_reduce_with_subs)
2692     gcc_assert (please_no_equalities_in_simplified_problems
2693                 || pb->num_subs == 0);
2694 }
2695
2696 /* Transform some wildcard variables to non-safe variables.  */
2697
2698 static void
2699 chain_unprotect (omega_pb pb)
2700 {
2701   int i, e;
2702   bool *unprotect = XNEWVEC (bool, OMEGA_MAX_VARS);
2703
2704   for (i = 1; omega_safe_var_p (pb, i); i++)
2705     {
2706       unprotect[i] = omega_wildcard_p (pb, i);
2707
2708       for (e = pb->num_subs - 1; e >= 0; e--)
2709         if (pb->subs[e].coef[i])
2710           unprotect[i] = false;
2711     }
2712
2713   if (dump_file && (dump_flags & TDF_DETAILS))
2714     {
2715       fprintf (dump_file, "Doing chain reaction unprotection\n");
2716       omega_print_problem (dump_file, pb);
2717
2718       for (i = 1; omega_safe_var_p (pb, i); i++)
2719         if (unprotect[i])
2720           fprintf (dump_file, "unprotecting %s\n",
2721                    omega_variable_to_str (pb, i));
2722     }
2723
2724   for (i = 1; omega_safe_var_p (pb, i); i++)
2725     if (unprotect[i])
2726       omega_unprotect_1 (pb, &i, unprotect);
2727
2728   if (dump_file && (dump_flags & TDF_DETAILS))
2729     {
2730       fprintf (dump_file, "After chain reactions\n");
2731       omega_print_problem (dump_file, pb);
2732     }
2733
2734   free (unprotect);
2735 }
2736
2737 /* Reduce problem PB.  */
2738
2739 static void
2740 omega_problem_reduced (omega_pb pb)
2741 {
2742   if (omega_verify_simplification
2743       && !in_approximate_mode
2744       && verify_omega_pb (pb) == omega_false)
2745     return;
2746
2747   if (PARAM_VALUE (PARAM_OMEGA_ELIMINATE_REDUNDANT_CONSTRAINTS)
2748       && !omega_eliminate_redundant (pb, true))
2749     return;
2750
2751   omega_found_reduction = omega_true;
2752
2753   if (!please_no_equalities_in_simplified_problems)
2754     coalesce (pb);
2755
2756   if (omega_reduce_with_subs
2757       || please_no_equalities_in_simplified_problems)
2758     chain_unprotect (pb);
2759   else
2760     resurrect_subs (pb);
2761
2762   if (!return_single_result)
2763     {
2764       int i;
2765
2766       for (i = 1; omega_safe_var_p (pb, i); i++)
2767         pb->forwarding_address[pb->var[i]] = i;
2768
2769       for (i = 0; i < pb->num_subs; i++)
2770         pb->forwarding_address[pb->subs[i].key] = -i - 1;
2771
2772       (*omega_when_reduced) (pb);
2773     }
2774
2775   if (dump_file && (dump_flags & TDF_DETAILS))
2776     {
2777       fprintf (dump_file, "-------------------------------------------\n");
2778       fprintf (dump_file, "problem reduced:\n");
2779       omega_print_problem (dump_file, pb);
2780       fprintf (dump_file, "-------------------------------------------\n");
2781     }
2782 }
2783
2784 /* Eliminates all the free variables for problem PB, that is all the
2785    variables from FV to PB->NUM_VARS.  */
2786
2787 static void
2788 omega_free_eliminations (omega_pb pb, int fv)
2789 {
2790   bool try_again = true;
2791   int i, e, e2;
2792   int n_vars = pb->num_vars;
2793
2794   while (try_again)
2795     {
2796       try_again = false;
2797
2798       for (i = n_vars; i > fv; i--)
2799         {
2800           for (e = pb->num_geqs - 1; e >= 0; e--)
2801             if (pb->geqs[e].coef[i])
2802               break;
2803
2804           if (e < 0)
2805             e2 = e;
2806           else if (pb->geqs[e].coef[i] > 0)
2807             {
2808               for (e2 = e - 1; e2 >= 0; e2--)
2809                 if (pb->geqs[e2].coef[i] < 0)
2810                   break;
2811             }
2812           else
2813             {
2814               for (e2 = e - 1; e2 >= 0; e2--)
2815                 if (pb->geqs[e2].coef[i] > 0)
2816                   break;
2817             }
2818
2819           if (e2 < 0)
2820             {
2821               int e3;
2822               for (e3 = pb->num_subs - 1; e3 >= 0; e3--)
2823                 if (pb->subs[e3].coef[i])
2824                   break;
2825
2826               if (e3 >= 0)
2827                 continue;
2828
2829               for (e3 = pb->num_eqs - 1; e3 >= 0; e3--)
2830                 if (pb->eqs[e3].coef[i])
2831                   break;
2832
2833               if (e3 >= 0)
2834                 continue;
2835
2836               if (dump_file && (dump_flags & TDF_DETAILS))
2837                 fprintf (dump_file, "a free elimination of %s\n",
2838                          omega_variable_to_str (pb, i));
2839
2840               if (e >= 0)
2841                 {
2842                   omega_delete_geq (pb, e, n_vars);
2843
2844                   for (e--; e >= 0; e--)
2845                     if (pb->geqs[e].coef[i])
2846                       omega_delete_geq (pb, e, n_vars);
2847
2848                   try_again = (i < n_vars);
2849                 }
2850
2851               omega_delete_variable (pb, i);
2852               n_vars = pb->num_vars;
2853             }
2854         }
2855     }
2856
2857   if (dump_file && (dump_flags & TDF_DETAILS))
2858     {
2859       fprintf (dump_file, "\nafter free eliminations:\n");
2860       omega_print_problem (dump_file, pb);
2861       fprintf (dump_file, "\n");
2862     }
2863 }
2864
2865 /* Do free red eliminations.  */
2866
2867 static void
2868 free_red_eliminations (omega_pb pb)
2869 {
2870   bool try_again = true;
2871   int i, e, e2;
2872   int n_vars = pb->num_vars;
2873   bool *is_red_var = XNEWVEC (bool, OMEGA_MAX_VARS);
2874   bool *is_dead_var = XNEWVEC (bool, OMEGA_MAX_VARS);
2875   bool *is_dead_geq = XNEWVEC (bool, OMEGA_MAX_GEQS);
2876
2877   for (i = n_vars; i > 0; i--)
2878     {
2879       is_red_var[i] = false;
2880       is_dead_var[i] = false;
2881     }
2882
2883   for (e = pb->num_geqs - 1; e >= 0; e--)
2884     {
2885       is_dead_geq[e] = false;
2886
2887       if (pb->geqs[e].color == omega_red)
2888         for (i = n_vars; i > 0; i--)
2889           if (pb->geqs[e].coef[i] != 0)
2890             is_red_var[i] = true;
2891     }
2892
2893   while (try_again)
2894     {
2895       try_again = false;
2896       for (i = n_vars; i > 0; i--)
2897         if (!is_red_var[i] && !is_dead_var[i])
2898           {
2899             for (e = pb->num_geqs - 1; e >= 0; e--)
2900               if (!is_dead_geq[e] && pb->geqs[e].coef[i])
2901                 break;
2902
2903             if (e < 0)
2904               e2 = e;
2905             else if (pb->geqs[e].coef[i] > 0)
2906               {
2907                 for (e2 = e - 1; e2 >= 0; e2--)
2908                   if (!is_dead_geq[e2] && pb->geqs[e2].coef[i] < 0)
2909                     break;
2910               }
2911             else
2912               {
2913                 for (e2 = e - 1; e2 >= 0; e2--)
2914                   if (!is_dead_geq[e2] && pb->geqs[e2].coef[i] > 0)
2915                     break;
2916               }
2917
2918             if (e2 < 0)
2919               {
2920                 int e3;
2921                 for (e3 = pb->num_subs - 1; e3 >= 0; e3--)
2922                   if (pb->subs[e3].coef[i])
2923                     break;
2924
2925                 if (e3 >= 0)
2926                   continue;
2927
2928                 for (e3 = pb->num_eqs - 1; e3 >= 0; e3--)
2929                   if (pb->eqs[e3].coef[i])
2930                     break;
2931
2932                 if (e3 >= 0)
2933                   continue;
2934
2935                 if (dump_file && (dump_flags & TDF_DETAILS))
2936                   fprintf (dump_file, "a free red elimination of %s\n",
2937                            omega_variable_to_str (pb, i));
2938
2939                 for (; e >= 0; e--)
2940                   if (pb->geqs[e].coef[i])
2941                     is_dead_geq[e] = true;
2942
2943                 try_again = true;
2944                 is_dead_var[i] = true;
2945               }
2946           }
2947     }
2948
2949   for (e = pb->num_geqs - 1; e >= 0; e--)
2950     if (is_dead_geq[e])
2951       omega_delete_geq (pb, e, n_vars);
2952
2953   for (i = n_vars; i > 0; i--)
2954     if (is_dead_var[i])
2955       omega_delete_variable (pb, i);
2956
2957   if (dump_file && (dump_flags & TDF_DETAILS))
2958     {
2959       fprintf (dump_file, "\nafter free red eliminations:\n");
2960       omega_print_problem (dump_file, pb);
2961       fprintf (dump_file, "\n");
2962     }
2963
2964   free (is_red_var);
2965   free (is_dead_var);
2966   free (is_dead_geq);
2967 }
2968
2969 /* For equation EQ of the form "0 = EQN", insert in PB two
2970    inequalities "0 <= EQN" and "0 <= -EQN".  */
2971
2972 void
2973 omega_convert_eq_to_geqs (omega_pb pb, int eq)
2974 {
2975   int i;
2976
2977   if (dump_file && (dump_flags & TDF_DETAILS))
2978     fprintf (dump_file, "Converting Eq to Geqs\n");
2979
2980   /* Insert "0 <= EQN".  */
2981   omega_copy_eqn (&pb->geqs[pb->num_geqs], &pb->eqs[eq], pb->num_vars);
2982   pb->geqs[pb->num_geqs].touched = 1;
2983   pb->num_geqs++;
2984
2985   /* Insert "0 <= -EQN".  */
2986   omega_copy_eqn (&pb->geqs[pb->num_geqs], &pb->eqs[eq], pb->num_vars);
2987   pb->geqs[pb->num_geqs].touched = 1;
2988
2989   for (i = 0; i <= pb->num_vars; i++)
2990     pb->geqs[pb->num_geqs].coef[i] *= -1;
2991
2992   pb->num_geqs++;
2993
2994   if (dump_file && (dump_flags & TDF_DETAILS))
2995     omega_print_problem (dump_file, pb);
2996 }
2997
2998 /* Eliminates variable I from PB.  */
2999
3000 static void
3001 omega_do_elimination (omega_pb pb, int e, int i)
3002 {
3003   eqn sub = omega_alloc_eqns (0, 1);
3004   int c;
3005   int n_vars = pb->num_vars;
3006
3007   if (dump_file && (dump_flags & TDF_DETAILS))
3008     fprintf (dump_file, "eliminating variable %s\n",
3009              omega_variable_to_str (pb, i));
3010
3011   omega_copy_eqn (sub, &pb->eqs[e], pb->num_vars);
3012   c = sub->coef[i];
3013   sub->coef[i] = 0;
3014   if (c == 1 || c == -1)
3015     {
3016       if (pb->eqs[e].color == omega_red)
3017         {
3018           bool fB;
3019           omega_substitute_red (pb, sub, i, c, &fB);
3020           if (fB)
3021             omega_convert_eq_to_geqs (pb, e);
3022           else
3023             omega_delete_variable (pb, i);
3024         }
3025       else
3026         {
3027           omega_substitute (pb, sub, i, c);
3028           omega_delete_variable (pb, i);
3029         }
3030     }
3031   else
3032     {
3033       int a = abs (c);
3034       int e2 = e;
3035
3036       if (dump_file && (dump_flags & TDF_DETAILS))
3037         fprintf (dump_file, "performing non-exact elimination, c = %d\n", c);
3038
3039       for (e = pb->num_eqs - 1; e >= 0; e--)
3040         if (pb->eqs[e].coef[i])
3041           {
3042             eqn eqn = &(pb->eqs[e]);
3043             int j, k;
3044             for (j = n_vars; j >= 0; j--)
3045               eqn->coef[j] *= a;
3046             k = eqn->coef[i];
3047             eqn->coef[i] = 0;
3048             if (sub->color == omega_red)
3049               eqn->color = omega_red;
3050             for (j = n_vars; j >= 0; j--)
3051               eqn->coef[j] -= sub->coef[j] * k / c;
3052           }
3053
3054       for (e = pb->num_geqs - 1; e >= 0; e--)
3055         if (pb->geqs[e].coef[i])
3056           {
3057             eqn eqn = &(pb->geqs[e]);
3058             int j, k;
3059
3060             if (sub->color == omega_red)
3061               eqn->color = omega_red;
3062
3063             for (j = n_vars; j >= 0; j--)
3064               eqn->coef[j] *= a;
3065
3066             eqn->touched = 1;
3067             k = eqn->coef[i];
3068             eqn->coef[i] = 0;
3069
3070             for (j = n_vars; j >= 0; j--)
3071               eqn->coef[j] -= sub->coef[j] * k / c;
3072
3073           }
3074
3075       for (e = pb->num_subs - 1; e >= 0; e--)
3076         if (pb->subs[e].coef[i])
3077           {
3078             eqn eqn = &(pb->subs[e]);
3079             int j, k;
3080             gcc_assert (0);
3081             gcc_assert (sub->color == omega_black);
3082             for (j = n_vars; j >= 0; j--)
3083               eqn->coef[j] *= a;
3084             k = eqn->coef[i];
3085             eqn->coef[i] = 0;
3086             for (j = n_vars; j >= 0; j--)
3087               eqn->coef[j] -= sub->coef[j] * k / c;
3088           }
3089
3090       if (in_approximate_mode)
3091         omega_delete_variable (pb, i);
3092       else
3093         omega_convert_eq_to_geqs (pb, e2);
3094     }
3095
3096   omega_free_eqns (sub, 1);
3097 }
3098
3099 /* Helper function for printing "sorry, no solution".  */
3100
3101 static inline enum omega_result
3102 omega_problem_has_no_solution (void)
3103 {
3104   if (dump_file && (dump_flags & TDF_DETAILS))
3105     fprintf (dump_file, "\nequations have no solution \n");
3106
3107   return omega_false;
3108 }
3109
3110 /* Helper function: solve equations in PB one at a time, following the
3111    DESIRED_RES result.  */
3112
3113 static enum omega_result
3114 omega_solve_eq (omega_pb pb, enum omega_result desired_res)
3115 {
3116   int i, j, e;
3117   int g, g2;
3118   g = 0;
3119
3120
3121   if (dump_file && (dump_flags & TDF_DETAILS) && pb->num_eqs > 0)
3122     {
3123       fprintf (dump_file, "\nomega_solve_eq (%d, %d)\n",
3124                desired_res, may_be_red);
3125       omega_print_problem (dump_file, pb);
3126       fprintf (dump_file, "\n");
3127     }
3128
3129   if (may_be_red)
3130     {
3131       i = 0;
3132       j = pb->num_eqs - 1;
3133
3134       while (1)
3135         {
3136           eqn eq;
3137
3138           while (i <= j && pb->eqs[i].color == omega_red)
3139             i++;
3140
3141           while (i <= j && pb->eqs[j].color == omega_black)
3142             j--;
3143
3144           if (i >= j)
3145             break;
3146
3147           eq = omega_alloc_eqns (0, 1);
3148           omega_copy_eqn (eq, &pb->eqs[i], pb->num_vars);
3149           omega_copy_eqn (&pb->eqs[i], &pb->eqs[j], pb->num_vars);
3150           omega_copy_eqn (&pb->eqs[j], eq, pb->num_vars);
3151           omega_free_eqns (eq, 1);
3152           i++;
3153           j--;
3154         }
3155     }
3156
3157   /* Eliminate all EQ equations */
3158   for (e = pb->num_eqs - 1; e >= 0; e--)
3159     {
3160       eqn eqn = &(pb->eqs[e]);
3161       int sv;
3162
3163       if (dump_file && (dump_flags & TDF_DETAILS))
3164         fprintf (dump_file, "----\n");
3165
3166       for (i = pb->num_vars; i > 0; i--)
3167         if (eqn->coef[i])
3168           break;
3169
3170       g = eqn->coef[i];
3171
3172       for (j = i - 1; j > 0; j--)
3173         if (eqn->coef[j])
3174           break;
3175
3176       /* i is the position of last nonzero coefficient,
3177          g is the coefficient of i,
3178          j is the position of next nonzero coefficient.  */
3179
3180       if (j == 0)
3181         {
3182           if (eqn->coef[0] % g != 0)
3183             return omega_problem_has_no_solution ();
3184
3185           eqn->coef[0] = eqn->coef[0] / g;
3186           eqn->coef[i] = 1;
3187           pb->num_eqs--;
3188           omega_do_elimination (pb, e, i);
3189           continue;
3190         }
3191
3192       else if (j == -1)
3193         {
3194           if (eqn->coef[0] != 0)
3195             return omega_problem_has_no_solution ();
3196
3197           pb->num_eqs--;
3198           continue;
3199         }
3200
3201       if (g < 0)
3202         g = -g;
3203
3204       if (g == 1)
3205         {
3206           pb->num_eqs--;
3207           omega_do_elimination (pb, e, i);
3208         }
3209
3210       else
3211         {
3212           int k = j;
3213           bool promotion_possible =
3214             (omega_safe_var_p (pb, j)
3215              && pb->safe_vars + 1 == i
3216              && !omega_eqn_is_red (eqn, desired_res)
3217              && !in_approximate_mode);
3218
3219           if (dump_file && (dump_flags & TDF_DETAILS) && promotion_possible)
3220             fprintf (dump_file, " Promotion possible\n");
3221
3222         normalizeEQ:
3223           if (!omega_safe_var_p (pb, j))
3224             {
3225               for (; g != 1 && !omega_safe_var_p (pb, j); j--)
3226                 g = gcd (abs (eqn->coef[j]), g);
3227               g2 = g;
3228             }
3229           else if (!omega_safe_var_p (pb, i))
3230             g2 = g;
3231           else
3232             g2 = 0;
3233
3234           for (; g != 1 && j > 0; j--)
3235             g = gcd (abs (eqn->coef[j]), g);
3236
3237           if (g > 1)
3238             {
3239               if (eqn->coef[0] % g != 0)
3240                 return omega_problem_has_no_solution ();
3241
3242               for (j = 0; j <= pb->num_vars; j++)
3243                 eqn->coef[j] /= g;
3244
3245               g2 = g2 / g;
3246             }
3247
3248           if (g2 > 1)
3249             {
3250               int e2;
3251
3252               for (e2 = e - 1; e2 >= 0; e2--)
3253                 if (pb->eqs[e2].coef[i])
3254                   break;
3255
3256               if (e2 == -1)
3257                 for (e2 = pb->num_geqs - 1; e2 >= 0; e2--)
3258                   if (pb->geqs[e2].coef[i])
3259                     break;
3260
3261               if (e2 == -1)
3262                 for (e2 = pb->num_subs - 1; e2 >= 0; e2--)
3263                   if (pb->subs[e2].coef[i])
3264                     break;
3265
3266               if (e2 == -1)
3267                 {
3268                   bool change = false;
3269
3270                   if (dump_file && (dump_flags & TDF_DETAILS))
3271                     {
3272                       fprintf (dump_file, "Ha! We own it! \n");
3273                       omega_print_eq (dump_file, pb, eqn);
3274                       fprintf (dump_file, " \n");
3275                     }
3276
3277                   g = eqn->coef[i];
3278                   g = abs (g);
3279
3280                   for (j = i - 1; j >= 0; j--)
3281                     {
3282                       int t = int_mod (eqn->coef[j], g);
3283
3284                       if (2 * t >= g)
3285                         t -= g;
3286
3287                       if (t != eqn->coef[j])
3288                         {
3289                           eqn->coef[j] = t;
3290                           change = true;
3291                         }
3292                     }
3293
3294                   if (!change)
3295                     {
3296                       if (dump_file && (dump_flags & TDF_DETAILS))
3297                         fprintf (dump_file, "So what?\n");
3298                     }
3299
3300                   else
3301                     {
3302                       omega_name_wild_card (pb, i);
3303
3304                       if (dump_file && (dump_flags & TDF_DETAILS))
3305                         {
3306                           omega_print_eq (dump_file, pb, eqn);
3307                           fprintf (dump_file, " \n");
3308                         }
3309
3310                       e++;
3311                       continue;
3312                     }
3313                 }
3314             }
3315
3316           if (promotion_possible)
3317             {
3318               if (dump_file && (dump_flags & TDF_DETAILS))
3319                 {
3320                   fprintf (dump_file, "promoting %s to safety\n",
3321                            omega_variable_to_str (pb, i));
3322                   omega_print_vars (dump_file, pb);
3323                 }
3324
3325               pb->safe_vars++;
3326
3327               if (!omega_wildcard_p (pb, i))
3328                 omega_name_wild_card (pb, i);
3329
3330               promotion_possible = false;
3331               j = k;
3332               goto normalizeEQ;
3333             }
3334
3335           if (g2 > 1 && !in_approximate_mode)
3336             {
3337               if (pb->eqs[e].color == omega_red)
3338                 {
3339                   if (dump_file && (dump_flags & TDF_DETAILS))
3340                     fprintf (dump_file, "handling red equality\n");
3341
3342                   pb->num_eqs--;
3343                   omega_do_elimination (pb, e, i);
3344                   continue;
3345                 }
3346
3347               if (dump_file && (dump_flags & TDF_DETAILS))
3348                 {
3349                   fprintf (dump_file,
3350                            "adding equation to handle safe variable \n");
3351                   omega_print_eq (dump_file, pb, eqn);
3352                   fprintf (dump_file, "\n----\n");
3353                   omega_print_problem (dump_file, pb);
3354                   fprintf (dump_file, "\n----\n");
3355                   fprintf (dump_file, "\n----\n");
3356                 }
3357
3358               i = omega_add_new_wild_card (pb);
3359               pb->num_eqs++;
3360               gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
3361               omega_init_eqn_zero (&pb->eqs[e + 1], pb->num_vars);
3362               omega_copy_eqn (&pb->eqs[e + 1], eqn, pb->safe_vars);
3363
3364               for (j = pb->num_vars; j >= 0; j--)
3365                 {
3366                   pb->eqs[e + 1].coef[j] = int_mod (pb->eqs[e + 1].coef[j], g2);
3367
3368                   if (2 * pb->eqs[e + 1].coef[j] >= g2)
3369                     pb->eqs[e + 1].coef[j] -= g2;
3370                 }
3371
3372               pb->eqs[e + 1].coef[i] = g2;
3373               e += 2;
3374
3375               if (dump_file && (dump_flags & TDF_DETAILS))
3376                 omega_print_problem (dump_file, pb);
3377
3378               continue;
3379             }
3380
3381           sv = pb->safe_vars;
3382           if (g2 == 0)
3383             sv = 0;
3384
3385           /* Find variable to eliminate.  */
3386           if (g2 > 1)
3387             {
3388               gcc_assert (in_approximate_mode);
3389
3390               if (dump_file && (dump_flags & TDF_DETAILS))
3391                 {
3392                   fprintf (dump_file, "non-exact elimination: ");
3393                   omega_print_eq (dump_file, pb, eqn);
3394                   fprintf (dump_file, "\n");
3395                   omega_print_problem (dump_file, pb);
3396                 }
3397
3398               for (i = pb->num_vars; i > sv; i--)
3399                 if (pb->eqs[e].coef[i] != 0)
3400                   break;
3401             }
3402           else
3403             for (i = pb->num_vars; i > sv; i--)
3404               if (pb->eqs[e].coef[i] == 1 || pb->eqs[e].coef[i] == -1)
3405                 break;
3406
3407           if (i > sv)
3408             {
3409               pb->num_eqs--;
3410               omega_do_elimination (pb, e, i);
3411
3412               if (dump_file && (dump_flags & TDF_DETAILS) && g2 > 1)
3413                 {
3414                   fprintf (dump_file, "result of non-exact elimination:\n");
3415                   omega_print_problem (dump_file, pb);
3416                 }
3417             }
3418           else
3419             {
3420               int factor = (INT_MAX);
3421               j = 0;
3422
3423               if (dump_file && (dump_flags & TDF_DETAILS))
3424                 fprintf (dump_file, "doing moding\n");
3425
3426               for (i = pb->num_vars; i != sv; i--)
3427                 if ((pb->eqs[e].coef[i] & 1) != 0)
3428                   {
3429                     j = i;
3430                     i--;
3431
3432                     for (; i != sv; i--)
3433                       if ((pb->eqs[e].coef[i] & 1) != 0)
3434                         break;
3435
3436                     break;
3437                   }
3438
3439               if (j != 0 && i == sv)
3440                 {
3441                   omega_do_mod (pb, 2, e, j);
3442                   e++;
3443                   continue;
3444                 }
3445
3446               j = 0;
3447               for (i = pb->num_vars; i != sv; i--)
3448                 if (pb->eqs[e].coef[i] != 0
3449                     && factor > abs (pb->eqs[e].coef[i]) + 1)
3450                   {
3451                     factor = abs (pb->eqs[e].coef[i]) + 1;
3452                     j = i;
3453                   }
3454
3455               if (j == sv)
3456                 {
3457                   if (dump_file && (dump_flags & TDF_DETAILS))
3458                     fprintf (dump_file, "should not have happened\n");
3459                   gcc_assert (0);
3460                 }
3461
3462               omega_do_mod (pb, factor, e, j);
3463               /* Go back and try this equation again.  */
3464               e++;
3465             }
3466         }
3467     }
3468
3469   pb->num_eqs = 0;
3470   return omega_unknown;
3471 }
3472
3473 /* Transform an inequation E to an equality, then solve DIFF problems
3474    based on PB, and only differing by the constant part that is
3475    diminished by one, trying to figure out which of the constants
3476    satisfies PB.    */
3477
3478 static enum omega_result
3479 parallel_splinter (omega_pb pb, int e, int diff,
3480                    enum omega_result desired_res)
3481 {
3482   omega_pb tmp_problem;
3483   int i;
3484
3485   if (dump_file && (dump_flags & TDF_DETAILS))
3486     {
3487       fprintf (dump_file, "Using parallel splintering\n");
3488       omega_print_problem (dump_file, pb);
3489     }
3490
3491   tmp_problem = XNEW (struct omega_pb_d);
3492   omega_copy_eqn (&pb->eqs[0], &pb->geqs[e], pb->num_vars);
3493   pb->num_eqs = 1;
3494
3495   for (i = 0; i <= diff; i++)
3496     {
3497       omega_copy_problem (tmp_problem, pb);
3498
3499       if (dump_file && (dump_flags & TDF_DETAILS))
3500         {
3501           fprintf (dump_file, "Splinter # %i\n", i);
3502           omega_print_problem (dump_file, pb);
3503         }
3504
3505       if (omega_solve_problem (tmp_problem, desired_res) == omega_true)
3506         {
3507           free (tmp_problem);
3508           return omega_true;
3509         }
3510
3511       pb->eqs[0].coef[0]--;
3512     }
3513
3514   free (tmp_problem);
3515   return omega_false;
3516 }
3517
3518 /* Helper function: solve equations one at a time.  */
3519
3520 static enum omega_result
3521 omega_solve_geq (omega_pb pb, enum omega_result desired_res)
3522 {
3523   int i, e;
3524   int n_vars, fv;
3525   enum omega_result result;
3526   bool coupled_subscripts = false;
3527   bool smoothed = false;
3528   bool eliminate_again;
3529   bool tried_eliminating_redundant = false;
3530
3531   if (desired_res != omega_simplify)
3532     {
3533       pb->num_subs = 0;
3534       pb->safe_vars = 0;
3535     }
3536
3537  solve_geq_start:
3538   do {
3539     gcc_assert (desired_res == omega_simplify || pb->num_subs == 0);
3540
3541     /* Verify that there are not too many inequalities.  */
3542     gcc_assert (pb->num_geqs <= OMEGA_MAX_GEQS);
3543
3544     if (dump_file && (dump_flags & TDF_DETAILS))
3545       {
3546         fprintf (dump_file, "\nomega_solve_geq (%d,%d):\n",
3547                  desired_res, please_no_equalities_in_simplified_problems);
3548         omega_print_problem (dump_file, pb);
3549         fprintf (dump_file, "\n");
3550       }
3551
3552     n_vars = pb->num_vars;
3553
3554     if (n_vars == 1)
3555       {
3556         enum omega_eqn_color u_color = omega_black;
3557         enum omega_eqn_color l_color = omega_black;
3558         int upper_bound = pos_infinity;
3559         int lower_bound = neg_infinity;
3560
3561         for (e = pb->num_geqs - 1; e >= 0; e--)
3562           {
3563             int a = pb->geqs[e].coef[1];
3564             int c = pb->geqs[e].coef[0];
3565
3566             /* Our equation is ax + c >= 0, or ax >= -c, or c >= -ax.  */
3567             if (a == 0)
3568               {
3569                 if (c < 0)
3570                   return omega_problem_has_no_solution ();
3571               }
3572             else if (a > 0)
3573               {
3574                 if (a != 1)
3575                   c = int_div (c, a);
3576
3577                 if (lower_bound < -c
3578                     || (lower_bound == -c
3579                         && !omega_eqn_is_red (&pb->geqs[e], desired_res)))
3580                   {
3581                     lower_bound = -c;
3582                     l_color = pb->geqs[e].color;
3583                   }
3584               }
3585             else
3586               {
3587                 if (a != -1)
3588                   c = int_div (c, -a);
3589
3590                 if (upper_bound > c
3591                     || (upper_bound == c
3592                         && !omega_eqn_is_red (&pb->geqs[e], desired_res)))
3593                   {
3594                     upper_bound = c;
3595                     u_color = pb->geqs[e].color;
3596                   }
3597               }
3598           }
3599
3600         if (dump_file && (dump_flags & TDF_DETAILS))
3601           {
3602             fprintf (dump_file, "upper bound = %d\n", upper_bound);
3603             fprintf (dump_file, "lower bound = %d\n", lower_bound);
3604           }
3605
3606         if (lower_bound > upper_bound)
3607           return omega_problem_has_no_solution ();
3608
3609         if (desired_res == omega_simplify)
3610           {
3611             pb->num_geqs = 0;
3612             if (pb->safe_vars == 1)
3613               {
3614
3615                 if (lower_bound == upper_bound
3616                     && u_color == omega_black
3617                     && l_color == omega_black)
3618                   {
3619                     pb->eqs[0].coef[0] = -lower_bound;
3620                     pb->eqs[0].coef[1] = 1;
3621                     pb->eqs[0].color = omega_black;
3622                     pb->num_eqs = 1;
3623                     return omega_solve_problem (pb, desired_res);
3624                   }
3625                 else
3626                   {
3627                     if (lower_bound > neg_infinity)
3628                       {
3629                         pb->geqs[0].coef[0] = -lower_bound;
3630                         pb->geqs[0].coef[1] = 1;
3631                         pb->geqs[0].key = 1;
3632                         pb->geqs[0].color = l_color;
3633                         pb->geqs[0].touched = 0;
3634                         pb->num_geqs = 1;
3635                       }
3636
3637                     if (upper_bound < pos_infinity)
3638                       {
3639                         pb->geqs[pb->num_geqs].coef[0] = upper_bound;
3640                         pb->geqs[pb->num_geqs].coef[1] = -1;
3641                         pb->geqs[pb->num_geqs].key = -1;
3642                         pb->geqs[pb->num_geqs].color = u_color;
3643                         pb->geqs[pb->num_geqs].touched = 0;
3644                         pb->num_geqs++;
3645                       }
3646                   }
3647               }
3648             else
3649               pb->num_vars = 0;
3650
3651             omega_problem_reduced (pb);
3652             return omega_false;
3653           }
3654
3655         if (original_problem != no_problem
3656             && l_color == omega_black
3657             && u_color == omega_black
3658             && !conservative
3659             && lower_bound == upper_bound)
3660           {
3661             pb->eqs[0].coef[0] = -lower_bound;
3662             pb->eqs[0].coef[1] = 1;
3663             pb->num_eqs = 1;
3664             adding_equality_constraint (pb, 0);
3665           }
3666
3667         return omega_true;
3668       }
3669
3670     if (!pb->variables_freed)
3671       {
3672         pb->variables_freed = true;
3673
3674         if (desired_res != omega_simplify)
3675           omega_free_eliminations (pb, 0);
3676         else
3677           omega_free_eliminations (pb, pb->safe_vars);
3678
3679         n_vars = pb->num_vars;
3680
3681         if (n_vars == 1)
3682           continue;
3683       }
3684
3685     switch (normalize_omega_problem (pb))
3686       {
3687       case normalize_false:
3688         return omega_false;
3689         break;
3690
3691       case normalize_coupled:
3692         coupled_subscripts = true;
3693         break;
3694
3695       case normalize_uncoupled:
3696         coupled_subscripts = false;
3697         break;
3698
3699       default:
3700         gcc_unreachable ();
3701       }
3702
3703     n_vars = pb->num_vars;
3704
3705     if (dump_file && (dump_flags & TDF_DETAILS))
3706       {
3707         fprintf (dump_file, "\nafter normalization:\n");
3708         omega_print_problem (dump_file, pb);
3709         fprintf (dump_file, "\n");
3710         fprintf (dump_file, "eliminating variable using Fourier-Motzkin.\n");
3711       }
3712
3713     do {
3714       int parallel_difference = INT_MAX;
3715       int best_parallel_eqn = -1;
3716       int minC, maxC, minCj = 0;
3717       int lower_bound_count = 0;
3718       int e2, Le = 0, Ue;
3719       bool possible_easy_int_solution;
3720       int max_splinters = 1;
3721       bool exact = false;
3722       bool lucky_exact = false;
3723       int best = (INT_MAX);
3724       int j = 0, jLe = 0, jLowerBoundCount = 0;
3725
3726
3727       eliminate_again = false;
3728
3729       if (pb->num_eqs > 0)
3730         return omega_solve_problem (pb, desired_res);
3731
3732       if (!coupled_subscripts)
3733         {
3734           if (pb->safe_vars == 0)
3735             pb->num_geqs = 0;
3736           else
3737             for (e = pb->num_geqs - 1; e >= 0; e--)
3738               if (!omega_safe_var_p (pb, abs (pb->geqs[e].key)))
3739                 omega_delete_geq (pb, e, n_vars);
3740
3741           pb->num_vars = pb->safe_vars;
3742
3743           if (desired_res == omega_simplify)
3744             {
3745               omega_problem_reduced (pb);
3746               return omega_false;
3747             }
3748
3749           return omega_true;
3750         }
3751
3752       if (desired_res != omega_simplify)
3753         fv = 0;
3754       else
3755         fv = pb->safe_vars;
3756
3757       if (pb->num_geqs == 0)
3758         {
3759           if (desired_res == omega_simplify)
3760             {
3761               pb->num_vars = pb->safe_vars;
3762               omega_problem_reduced (pb);
3763               return omega_false;
3764             }
3765           return omega_true;
3766         }
3767
3768       if (desired_res == omega_simplify && n_vars == pb->safe_vars)
3769         {
3770           omega_problem_reduced (pb);
3771           return omega_false;
3772         }
3773
3774       if (pb->num_geqs > OMEGA_MAX_GEQS - 30
3775           || pb->num_geqs > 2 * n_vars * n_vars + 4 * n_vars + 10)
3776         {
3777           if (dump_file && (dump_flags & TDF_DETAILS))
3778             fprintf (dump_file,
3779                      "TOO MANY EQUATIONS; "
3780                      "%d equations, %d variables, "
3781                      "ELIMINATING REDUNDANT ONES\n",
3782                      pb->num_geqs, n_vars);
3783
3784           if (!omega_eliminate_redundant (pb, false))
3785             return omega_false;
3786
3787           n_vars = pb->num_vars;
3788
3789           if (pb->num_eqs > 0)
3790             return omega_solve_problem (pb, desired_res);
3791
3792           if (dump_file && (dump_flags & TDF_DETAILS))
3793             fprintf (dump_file, "END ELIMINATION OF REDUNDANT EQUATIONS\n");
3794         }
3795
3796       if (desired_res != omega_simplify)
3797         fv = 0;
3798       else
3799         fv = pb->safe_vars;
3800
3801       for (i = n_vars; i != fv; i--)
3802         {
3803           int score;
3804           int ub = -2;
3805           int lb = -2;
3806           bool lucky = false;
3807           int upper_bound_count = 0;
3808
3809           lower_bound_count = 0;
3810           minC = maxC = 0;
3811
3812           for (e = pb->num_geqs - 1; e >= 0; e--)
3813             if (pb->geqs[e].coef[i] < 0)
3814               {
3815                 minC = MIN (minC, pb->geqs[e].coef[i]);
3816                 upper_bound_count++;
3817                 if (pb->geqs[e].coef[i] < -1)
3818                   {
3819                     if (ub == -2)
3820                       ub = e;
3821                     else
3822                       ub = -1;
3823                   }
3824               }
3825             else if (pb->geqs[e].coef[i] > 0)
3826               {
3827                 maxC = MAX (maxC, pb->geqs[e].coef[i]);
3828                 lower_bound_count++;
3829                 Le = e;
3830                 if (pb->geqs[e].coef[i] > 1)
3831                   {
3832                     if (lb == -2)
3833                       lb = e;
3834                     else
3835                       lb = -1;
3836                   }
3837               }
3838
3839           if (lower_bound_count == 0
3840               || upper_bound_count == 0)
3841             {
3842               lower_bound_count = 0;
3843               break;
3844             }
3845
3846           if (ub >= 0 && lb >= 0
3847               && pb->geqs[lb].key == -pb->geqs[ub].key)
3848             {
3849               int Lc = pb->geqs[lb].coef[i];
3850               int Uc = -pb->geqs[ub].coef[i];
3851               int diff =
3852                 Lc * pb->geqs[ub].coef[0] + Uc * pb->geqs[lb].coef[0];
3853               lucky = (diff >= (Uc - 1) * (Lc - 1));
3854             }
3855
3856           if (maxC == 1
3857               || minC == -1
3858               || lucky
3859               || in_approximate_mode)
3860             {
3861               score = upper_bound_count * lower_bound_count;
3862
3863               if (dump_file && (dump_flags & TDF_DETAILS))
3864                 fprintf (dump_file,
3865                          "For %s, exact, score = %d*%d, range = %d ... %d,"
3866                          "\nlucky = %d, in_approximate_mode=%d \n",
3867                          omega_variable_to_str (pb, i),
3868                          upper_bound_count,
3869                          lower_bound_count, minC, maxC, lucky,
3870                          in_approximate_mode);
3871
3872               if (!exact
3873                   || score < best)
3874                 {
3875
3876                   best = score;
3877                   j = i;
3878                   minCj = minC;
3879                   jLe = Le;
3880                   jLowerBoundCount = lower_bound_count;
3881                   exact = true;
3882                   lucky_exact = lucky;
3883                   if (score == 1)
3884                     break;
3885                 }
3886             }
3887           else if (!exact)
3888             {
3889               if (dump_file && (dump_flags & TDF_DETAILS))
3890                 fprintf (dump_file,
3891                          "For %s, non-exact, score = %d*%d,"
3892                          "range = %d ... %d \n",
3893                          omega_variable_to_str (pb, i),
3894                          upper_bound_count,
3895                          lower_bound_count, minC, maxC);
3896
3897               score = maxC - minC;
3898
3899               if (best > score)
3900                 {
3901                   best = score;
3902                   j = i;
3903                   minCj = minC;
3904                   jLe = Le;
3905                   jLowerBoundCount = lower_bound_count;
3906                 }
3907             }
3908         }
3909
3910       if (lower_bound_count == 0)
3911         {
3912           omega_free_eliminations (pb, pb->safe_vars);
3913           n_vars = pb->num_vars;
3914           eliminate_again = true;
3915           continue;
3916         }
3917
3918       i = j;
3919       minC = minCj;
3920       Le = jLe;
3921       lower_bound_count = jLowerBoundCount;
3922
3923       for (e = pb->num_geqs - 1; e >= 0; e--)
3924         if (pb->geqs[e].coef[i] > 0)
3925           {
3926             if (pb->geqs[e].coef[i] == -minC)
3927               max_splinters += -minC - 1;
3928             else
3929               max_splinters +=
3930                 check_pos_mul ((pb->geqs[e].coef[i] - 1),
3931                                (-minC - 1)) / (-minC) + 1;
3932           }
3933
3934       /* #ifdef Omega3 */
3935       /* Trying to produce exact elimination by finding redundant
3936          constraints.  */
3937       if (!exact && !tried_eliminating_redundant)
3938         {
3939           omega_eliminate_redundant (pb, false);
3940           tried_eliminating_redundant = true;
3941           eliminate_again = true;
3942           continue;
3943         }
3944       tried_eliminating_redundant = false;
3945       /* #endif */
3946
3947       if (return_single_result && desired_res == omega_simplify && !exact)
3948         {
3949           omega_problem_reduced (pb);
3950           return omega_true;
3951         }
3952
3953       /* #ifndef Omega3 */
3954       /* Trying to produce exact elimination by finding redundant
3955          constraints.  */
3956       if (!exact && !tried_eliminating_redundant)
3957         {
3958           omega_eliminate_redundant (pb, false);
3959           tried_eliminating_redundant = true;
3960           continue;
3961         }
3962       tried_eliminating_redundant = false;
3963       /* #endif */
3964
3965       if (!exact)
3966         {
3967           int e1, e2;
3968
3969           for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
3970             if (pb->geqs[e1].color == omega_black)
3971               for (e2 = e1 - 1; e2 >= 0; e2--)
3972                 if (pb->geqs[e2].color == omega_black
3973                     && pb->geqs[e1].key == -pb->geqs[e2].key
3974                     && ((pb->geqs[e1].coef[0] + pb->geqs[e2].coef[0])
3975                         * (3 - single_var_geq (&pb->geqs[e1], pb->num_vars))
3976                         / 2 < parallel_difference))
3977                   {
3978                     parallel_difference =
3979                       (pb->geqs[e1].coef[0] + pb->geqs[e2].coef[0])
3980                       * (3 - single_var_geq (&pb->geqs[e1], pb->num_vars))
3981                       / 2;
3982                     best_parallel_eqn = e1;
3983                   }
3984
3985           if (dump_file && (dump_flags & TDF_DETAILS)
3986               && best_parallel_eqn >= 0)
3987             {
3988               fprintf (dump_file,
3989                        "Possible parallel projection, diff = %d, in ",
3990                        parallel_difference);
3991               omega_print_geq (dump_file, pb, &(pb->geqs[best_parallel_eqn]));
3992               fprintf (dump_file, "\n");
3993               omega_print_problem (dump_file, pb);
3994             }
3995         }
3996
3997       if (dump_file && (dump_flags & TDF_DETAILS))
3998         {
3999           fprintf (dump_file, "going to eliminate %s, (%d,%d,%d)\n",
4000                    omega_variable_to_str (pb, i), i, minC,
4001                    lower_bound_count);
4002           omega_print_problem (dump_file, pb);
4003
4004           if (lucky_exact)
4005             fprintf (dump_file, "(a lucky exact elimination)\n");
4006
4007           else if (exact)
4008             fprintf (dump_file, "(an exact elimination)\n");
4009
4010           fprintf (dump_file, "Max # of splinters = %d\n", max_splinters);
4011         }
4012
4013       gcc_assert (max_splinters >= 1);
4014
4015       if (!exact && desired_res == omega_simplify && best_parallel_eqn >= 0
4016           && parallel_difference <= max_splinters)
4017         return parallel_splinter (pb, best_parallel_eqn, parallel_difference,
4018                                   desired_res);
4019
4020       smoothed = false;
4021
4022       if (i != n_vars)
4023         {
4024           int t;
4025           int j = pb->num_vars;
4026
4027           if (dump_file && (dump_flags & TDF_DETAILS))
4028             {
4029               fprintf (dump_file, "Swapping %d and %d\n", i, j);
4030               omega_print_problem (dump_file, pb);
4031             }
4032
4033           swap (&pb->var[i], &pb->var[j]);
4034
4035           for (e = pb->num_geqs - 1; e >= 0; e--)
4036             if (pb->geqs[e].coef[i] != pb->geqs[e].coef[j])
4037               {
4038                 pb->geqs[e].touched = 1;
4039                 t = pb->geqs[e].coef[i];
4040                 pb->geqs[e].coef[i] = pb->geqs[e].coef[j];
4041                 pb->geqs[e].coef[j] = t;
4042               }
4043
4044           for (e = pb->num_subs - 1; e >= 0; e--)
4045             if (pb->subs[e].coef[i] != pb->subs[e].coef[j])
4046               {
4047                 t = pb->subs[e].coef[i];
4048                 pb->subs[e].coef[i] = pb->subs[e].coef[j];
4049                 pb->subs[e].coef[j] = t;
4050               }
4051
4052           if (dump_file && (dump_flags & TDF_DETAILS))
4053             {
4054               fprintf (dump_file, "Swapping complete \n");
4055               omega_print_problem (dump_file, pb);
4056               fprintf (dump_file, "\n");
4057             }
4058
4059           i = j;
4060         }
4061
4062       else if (dump_file && (dump_flags & TDF_DETAILS))
4063         {
4064           fprintf (dump_file, "No swap needed\n");
4065           omega_print_problem (dump_file, pb);
4066         }
4067
4068       pb->num_vars--;
4069       n_vars = pb->num_vars;
4070
4071       if (exact)
4072         {
4073           if (n_vars == 1)
4074             {
4075               int upper_bound = pos_infinity;
4076               int lower_bound = neg_infinity;
4077               enum omega_eqn_color ub_color = omega_black;
4078               enum omega_eqn_color lb_color = omega_black;
4079               int topeqn = pb->num_geqs - 1;
4080               int Lc = pb->geqs[Le].coef[i];
4081
4082               for (Le = topeqn; Le >= 0; Le--)
4083                 if ((Lc = pb->geqs[Le].coef[i]) == 0)
4084                   {
4085                     if (pb->geqs[Le].coef[1] == 1)
4086                       {
4087                         int constantTerm = -pb->geqs[Le].coef[0];
4088
4089                         if (constantTerm > lower_bound ||
4090                             (constantTerm == lower_bound &&
4091                              !omega_eqn_is_red (&pb->geqs[Le], desired_res)))
4092                           {
4093                             lower_bound = constantTerm;
4094                             lb_color = pb->geqs[Le].color;
4095                           }
4096
4097                         if (dump_file && (dump_flags & TDF_DETAILS))
4098                           {
4099                             if (pb->geqs[Le].color == omega_black)
4100                               fprintf (dump_file, " :::=> %s >= %d\n",
4101                                        omega_variable_to_str (pb, 1),
4102                                        constantTerm);
4103                             else
4104                               fprintf (dump_file,
4105                                        " :::=> [%s >= %d]\n",
4106                                        omega_variable_to_str (pb, 1),
4107                                        constantTerm);
4108                           }
4109                       }
4110                     else
4111                       {
4112                         int constantTerm = pb->geqs[Le].coef[0];
4113                         if (constantTerm < upper_bound ||
4114                             (constantTerm == upper_bound
4115                              && !omega_eqn_is_red (&pb->geqs[Le],
4116                                                    desired_res)))
4117                           {
4118                             upper_bound = constantTerm;
4119                             ub_color = pb->geqs[Le].color;
4120                           }
4121
4122                         if (dump_file && (dump_flags & TDF_DETAILS))
4123                           {
4124                             if (pb->geqs[Le].color == omega_black)
4125                               fprintf (dump_file, " :::=> %s <= %d\n",
4126                                        omega_variable_to_str (pb, 1),
4127                                        constantTerm);
4128                             else
4129                               fprintf (dump_file,
4130                                        " :::=> [%s <= %d]\n",
4131                                        omega_variable_to_str (pb, 1),
4132                                        constantTerm);
4133                           }
4134                       }
4135                   }
4136                 else if (Lc > 0)
4137                   for (Ue = topeqn; Ue >= 0; Ue--)
4138                     if (pb->geqs[Ue].coef[i] < 0
4139                         && pb->geqs[Le].key != -pb->geqs[Ue].key)
4140                       {
4141                         int Uc = -pb->geqs[Ue].coef[i];
4142                         int coefficient = pb->geqs[Ue].coef[1] * Lc
4143                           + pb->geqs[Le].coef[1] * Uc;
4144                         int constantTerm = pb->geqs[Ue].coef[0] * Lc
4145                           + pb->geqs[Le].coef[0] * Uc;
4146
4147                         if (dump_file && (dump_flags & TDF_DETAILS))
4148                           {
4149                             omega_print_geq_extra (dump_file, pb,
4150                                                    &(pb->geqs[Ue]));
4151                             fprintf (dump_file, "\n");
4152                             omega_print_geq_extra (dump_file, pb,
4153                                                    &(pb->geqs[Le]));
4154                             fprintf (dump_file, "\n");
4155                           }
4156
4157                         if (coefficient > 0)
4158                           {
4159                             constantTerm = -int_div (constantTerm, coefficient);
4160
4161                             if (constantTerm > lower_bound
4162                                 || (constantTerm == lower_bound
4163                                     && (desired_res != omega_simplify
4164                                         || (pb->geqs[Ue].color == omega_black
4165                                             && pb->geqs[Le].color == omega_black))))
4166                               {
4167                                 lower_bound = constantTerm;
4168                                 lb_color = (pb->geqs[Ue].color == omega_red
4169                                             || pb->geqs[Le].color == omega_red)
4170                                   ? omega_red : omega_black;
4171                               }
4172
4173                             if (dump_file && (dump_flags & TDF_DETAILS))
4174                               {
4175                                 if (pb->geqs[Ue].color == omega_red
4176                                     || pb->geqs[Le].color == omega_red)
4177                                   fprintf (dump_file,
4178                                            " ::=> [%s >= %d]\n",
4179                                            omega_variable_to_str (pb, 1),
4180                                            constantTerm);
4181                                 else
4182                                   fprintf (dump_file,
4183                                            " ::=> %s >= %d\n",
4184                                            omega_variable_to_str (pb, 1),
4185                                            constantTerm);
4186                               }
4187                           }
4188                         else
4189                           {
4190                             constantTerm = int_div (constantTerm, -coefficient);
4191                             if (constantTerm < upper_bound
4192                                 || (constantTerm == upper_bound
4193                                     && pb->geqs[Ue].color == omega_black
4194                                     && pb->geqs[Le].color == omega_black))
4195                               {
4196                                 upper_bound = constantTerm;
4197                                 ub_color = (pb->geqs[Ue].color == omega_red
4198                                             || pb->geqs[Le].color == omega_red)
4199                                   ? omega_red : omega_black;
4200                               }
4201
4202                             if (dump_file
4203                                 && (dump_flags & TDF_DETAILS))
4204                               {
4205                                 if (pb->geqs[Ue].color == omega_red
4206                                     || pb->geqs[Le].color == omega_red)
4207                                   fprintf (dump_file,
4208                                            " ::=> [%s <= %d]\n",
4209                                            omega_variable_to_str (pb, 1),
4210                                            constantTerm);
4211                                 else
4212                                   fprintf (dump_file,
4213                                            " ::=> %s <= %d\n",
4214                                            omega_variable_to_str (pb, 1),
4215                                            constantTerm);
4216                               }
4217                           }
4218                       }
4219
4220               pb->num_geqs = 0;
4221
4222               if (dump_file && (dump_flags & TDF_DETAILS))
4223                 fprintf (dump_file,
4224                          " therefore, %c%d <= %c%s%c <= %d%c\n",
4225                          lb_color == omega_red ? '[' : ' ', lower_bound,
4226                          (lb_color == omega_red && ub_color == omega_black)
4227                          ? ']' : ' ',
4228                          omega_variable_to_str (pb, 1),
4229                          (lb_color == omega_black && ub_color == omega_red)
4230                          ? '[' : ' ',
4231                          upper_bound, ub_color == omega_red ? ']' : ' ');
4232
4233               if (lower_bound > upper_bound)
4234                 return omega_false;
4235
4236               if (pb->safe_vars == 1)
4237                 {
4238                   if (upper_bound == lower_bound
4239                       && !(ub_color == omega_red || lb_color == omega_red)
4240                       && !please_no_equalities_in_simplified_problems)
4241                     {
4242                       pb->num_eqs++;
4243                       pb->eqs[0].coef[1] = -1;
4244                       pb->eqs[0].coef[0] = upper_bound;
4245
4246                       if (ub_color == omega_red
4247                           || lb_color == omega_red)
4248                         pb->eqs[0].color = omega_red;
4249
4250                       if (desired_res == omega_simplify
4251                           && pb->eqs[0].color == omega_black)
4252                         return omega_solve_problem (pb, desired_res);
4253                     }
4254
4255                   if (upper_bound != pos_infinity)
4256                     {
4257                       pb->geqs[0].coef[1] = -1;
4258                       pb->geqs[0].coef[0] = upper_bound;
4259                       pb->geqs[0].color = ub_color;
4260                       pb->geqs[0].key = -1;
4261                       pb->geqs[0].touched = 0;
4262                       pb->num_geqs++;
4263                     }
4264
4265                   if (lower_bound != neg_infinity)
4266                     {
4267                       pb->geqs[pb->num_geqs].coef[1] = 1;
4268                       pb->geqs[pb->num_geqs].coef[0] = -lower_bound;
4269                       pb->geqs[pb->num_geqs].color = lb_color;
4270                       pb->geqs[pb->num_geqs].key = 1;
4271                       pb->geqs[pb->num_geqs].touched = 0;
4272                       pb->num_geqs++;
4273                     }
4274                 }
4275
4276               if (desired_res == omega_simplify)
4277                 {
4278                   omega_problem_reduced (pb);
4279                   return omega_false;
4280                 }
4281               else
4282                 {
4283                   if (!conservative
4284                       && (desired_res != omega_simplify
4285                           || (lb_color == omega_black
4286                               && ub_color == omega_black))
4287                       && original_problem != no_problem
4288                       && lower_bound == upper_bound)
4289                     {
4290                       for (i = original_problem->num_vars; i >= 0; i--)
4291                         if (original_problem->var[i] == pb->var[1])
4292                           break;
4293
4294                       if (i == 0)
4295                         break;
4296
4297                       e = original_problem->num_eqs++;
4298                       omega_init_eqn_zero (&original_problem->eqs[e],
4299                                            original_problem->num_vars);
4300                       original_problem->eqs[e].coef[i] = -1;
4301                       original_problem->eqs[e].coef[0] = upper_bound;
4302
4303                       if (dump_file && (dump_flags & TDF_DETAILS))
4304                         {
4305                           fprintf (dump_file,
4306                                    "adding equality %d to outer problem\n", e);
4307                           omega_print_problem (dump_file, original_problem);
4308                         }
4309                     }
4310                   return omega_true;
4311                 }
4312             }
4313
4314           eliminate_again = true;
4315
4316           if (lower_bound_count == 1)
4317             {
4318               eqn lbeqn = omega_alloc_eqns (0, 1);
4319               int Lc = pb->geqs[Le].coef[i];
4320
4321               if (dump_file && (dump_flags & TDF_DETAILS))
4322                 fprintf (dump_file, "an inplace elimination\n");
4323
4324               omega_copy_eqn (lbeqn, &pb->geqs[Le], (n_vars + 1));
4325               omega_delete_geq_extra (pb, Le, n_vars + 1);
4326
4327               for (Ue = pb->num_geqs - 1; Ue >= 0; Ue--)
4328                 if (pb->geqs[Ue].coef[i] < 0)
4329                   {
4330                     if (lbeqn->key == -pb->geqs[Ue].key)
4331                       omega_delete_geq_extra (pb, Ue, n_vars + 1);
4332                     else
4333                       {
4334                         int k;
4335                         int Uc = -pb->geqs[Ue].coef[i];
4336                         pb->geqs[Ue].touched = 1;
4337                         eliminate_again = false;
4338
4339                         if (lbeqn->color == omega_red)
4340                           pb->geqs[Ue].color = omega_red;
4341
4342                         for (k = 0; k <= n_vars; k++)
4343                           pb->geqs[Ue].coef[k] =
4344                             check_mul (pb->geqs[Ue].coef[k], Lc) +
4345                             check_mul (lbeqn->coef[k], Uc);
4346
4347                         if (dump_file && (dump_flags & TDF_DETAILS))
4348                           {
4349                             omega_print_geq (dump_file, pb,
4350                                              &(pb->geqs[Ue]));
4351                             fprintf (dump_file, "\n");
4352                           }
4353                       }
4354                   }
4355
4356               omega_free_eqns (lbeqn, 1);
4357               continue;
4358             }
4359           else
4360             {
4361               int *dead_eqns = XNEWVEC (int, OMEGA_MAX_GEQS);
4362               bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
4363               int num_dead = 0;
4364               int top_eqn = pb->num_geqs - 1;
4365               lower_bound_count--;
4366
4367               if (dump_file && (dump_flags & TDF_DETAILS))
4368                 fprintf (dump_file, "lower bound count = %d\n",
4369                          lower_bound_count);
4370
4371               for (Le = top_eqn; Le >= 0; Le--)
4372                 if (pb->geqs[Le].coef[i] > 0)
4373                   {
4374                     int Lc = pb->geqs[Le].coef[i];
4375                     for (Ue = top_eqn; Ue >= 0; Ue--)
4376                       if (pb->geqs[Ue].coef[i] < 0)
4377                         {
4378                           if (pb->geqs[Le].key != -pb->geqs[Ue].key)
4379                             {
4380                               int k;
4381                               int Uc = -pb->geqs[Ue].coef[i];
4382
4383                               if (num_dead == 0)
4384                                 e2 = pb->num_geqs++;
4385                               else
4386                                 e2 = dead_eqns[--num_dead];
4387
4388                               gcc_assert (e2 < OMEGA_MAX_GEQS);
4389
4390                               if (dump_file && (dump_flags & TDF_DETAILS))
4391                                 {
4392                                   fprintf (dump_file,
4393                                            "Le = %d, Ue = %d, gen = %d\n",
4394                                            Le, Ue, e2);
4395                                   omega_print_geq_extra (dump_file, pb,
4396                                                          &(pb->geqs[Le]));
4397                                   fprintf (dump_file, "\n");
4398                                   omega_print_geq_extra (dump_file, pb,
4399                                                          &(pb->geqs[Ue]));
4400                                   fprintf (dump_file, "\n");
4401                                 }
4402
4403                               eliminate_again = false;
4404
4405                               for (k = n_vars; k >= 0; k--)
4406                                 pb->geqs[e2].coef[k] =
4407                                   check_mul (pb->geqs[Ue].coef[k], Lc) +
4408                                   check_mul (pb->geqs[Le].coef[k], Uc);
4409
4410                               pb->geqs[e2].coef[n_vars + 1] = 0;
4411                               pb->geqs[e2].touched = 1;
4412
4413                               if (pb->geqs[Ue].color == omega_red
4414                                   || pb->geqs[Le].color == omega_red)
4415                                 pb->geqs[e2].color = omega_red;
4416                               else
4417                                 pb->geqs[e2].color = omega_black;
4418
4419                               if (dump_file && (dump_flags & TDF_DETAILS))
4420                                 {
4421                                   omega_print_geq (dump_file, pb,
4422                                                    &(pb->geqs[e2]));
4423                                   fprintf (dump_file, "\n");
4424                                 }
4425                             }
4426
4427                           if (lower_bound_count == 0)
4428                             {
4429                               dead_eqns[num_dead++] = Ue;
4430
4431                               if (dump_file && (dump_flags & TDF_DETAILS))
4432                                 fprintf (dump_file, "Killed %d\n", Ue);
4433                             }
4434                         }
4435
4436                     lower_bound_count--;
4437                     dead_eqns[num_dead++] = Le;
4438
4439                     if (dump_file && (dump_flags & TDF_DETAILS))
4440                       fprintf (dump_file, "Killed %d\n", Le);
4441                   }
4442
4443               for (e = pb->num_geqs - 1; e >= 0; e--)
4444                 is_dead[e] = false;
4445
4446               while (num_dead > 0)
4447                 is_dead[dead_eqns[--num_dead]] = true;
4448
4449               for (e = pb->num_geqs - 1; e >= 0; e--)
4450                 if (is_dead[e])
4451                   omega_delete_geq_extra (pb, e, n_vars + 1);
4452
4453               free (dead_eqns);
4454               free (is_dead);
4455               continue;
4456             }
4457         }
4458       else
4459         {
4460           omega_pb rS, iS;
4461
4462           rS = omega_alloc_problem (0, 0);
4463           iS = omega_alloc_problem (0, 0);
4464           e2 = 0;
4465           possible_easy_int_solution = true;
4466
4467           for (e = 0; e < pb->num_geqs; e++)
4468             if (pb->geqs[e].coef[i] == 0)
4469               {
4470                 omega_copy_eqn (&(rS->geqs[e2]), &pb->geqs[e],
4471                                 pb->num_vars);
4472                 omega_copy_eqn (&(iS->geqs[e2]), &pb->geqs[e],
4473                                 pb->num_vars);
4474
4475                 if (dump_file && (dump_flags & TDF_DETAILS))
4476                   {
4477                     int t;
4478                     fprintf (dump_file, "Copying (%d, %d): ", i,
4479                              pb->geqs[e].coef[i]);
4480                     omega_print_geq_extra (dump_file, pb, &pb->geqs[e]);
4481                     fprintf (dump_file, "\n");
4482                     for (t = 0; t <= n_vars + 1; t++)
4483                       fprintf (dump_file, "%d ", pb->geqs[e].coef[t]);
4484                     fprintf (dump_file, "\n");
4485
4486                   }
4487                 e2++;
4488                 gcc_assert (e2 < OMEGA_MAX_GEQS);
4489               }
4490
4491           for (Le = pb->num_geqs - 1; Le >= 0; Le--)
4492             if (pb->geqs[Le].coef[i] > 0)
4493               for (Ue = pb->num_geqs - 1; Ue >= 0; Ue--)
4494                 if (pb->geqs[Ue].coef[i] < 0)
4495                   {
4496                     int k;
4497                     int Lc = pb->geqs[Le].coef[i];
4498                     int Uc = -pb->geqs[Ue].coef[i];
4499
4500                     if (pb->geqs[Le].key != -pb->geqs[Ue].key)
4501                       {
4502
4503                         rS->geqs[e2].touched = iS->geqs[e2].touched = 1;
4504
4505                         if (dump_file && (dump_flags & TDF_DETAILS))
4506                           {
4507                             fprintf (dump_file, "---\n");
4508                             fprintf (dump_file,
4509                                      "Le(Lc) = %d(%d_, Ue(Uc) = %d(%d), gen = %d\n",
4510                                      Le, Lc, Ue, Uc, e2);
4511                             omega_print_geq_extra (dump_file, pb, &pb->geqs[Le]);
4512                             fprintf (dump_file, "\n");
4513                             omega_print_geq_extra (dump_file, pb, &pb->geqs[Ue]);
4514                             fprintf (dump_file, "\n");
4515                           }
4516
4517                         if (Uc == Lc)
4518                           {
4519                             for (k = n_vars; k >= 0; k--)
4520                               iS->geqs[e2].coef[k] = rS->geqs[e2].coef[k] =
4521                                 pb->geqs[Ue].coef[k] + pb->geqs[Le].coef[k];
4522
4523                             iS->geqs[e2].coef[0] -= (Uc - 1);
4524                           }
4525                         else
4526                           {
4527                             for (k = n_vars; k >= 0; k--)
4528                               iS->geqs[e2].coef[k] = rS->geqs[e2].coef[k] =
4529                                 check_mul (pb->geqs[Ue].coef[k], Lc) +
4530                                 check_mul (pb->geqs[Le].coef[k], Uc);
4531
4532                             iS->geqs[e2].coef[0] -= (Uc - 1) * (Lc - 1);
4533                           }
4534
4535                         if (pb->geqs[Ue].color == omega_red
4536                             || pb->geqs[Le].color == omega_red)
4537                           iS->geqs[e2].color = rS->geqs[e2].color = omega_red;
4538                         else
4539                           iS->geqs[e2].color = rS->geqs[e2].color = omega_black;
4540
4541                         if (dump_file && (dump_flags & TDF_DETAILS))
4542                           {
4543                             omega_print_geq (dump_file, pb, &(rS->geqs[e2]));
4544                             fprintf (dump_file, "\n");
4545                           }
4546
4547                         e2++;
4548                         gcc_assert (e2 < OMEGA_MAX_GEQS);
4549                       }
4550                     else if (pb->geqs[Ue].coef[0] * Lc +
4551                              pb->geqs[Le].coef[0] * Uc -
4552                              (Uc - 1) * (Lc - 1) < 0)
4553                       possible_easy_int_solution = false;
4554                   }
4555
4556           iS->variables_initialized = rS->variables_initialized = true;
4557           iS->num_vars = rS->num_vars = pb->num_vars;
4558           iS->num_geqs = rS->num_geqs = e2;
4559           iS->num_eqs = rS->num_eqs = 0;
4560           iS->num_subs = rS->num_subs = pb->num_subs;
4561           iS->safe_vars = rS->safe_vars = pb->safe_vars;
4562
4563           for (e = n_vars; e >= 0; e--)
4564             rS->var[e] = pb->var[e];
4565
4566           for (e = n_vars; e >= 0; e--)
4567             iS->var[e] = pb->var[e];
4568
4569           for (e = pb->num_subs - 1; e >= 0; e--)
4570             {
4571               omega_copy_eqn (&(rS->subs[e]), &(pb->subs[e]), pb->num_vars);
4572               omega_copy_eqn (&(iS->subs[e]), &(pb->subs[e]), pb->num_vars);
4573             }
4574
4575           pb->num_vars++;
4576           n_vars = pb->num_vars;
4577
4578           if (desired_res != omega_true)
4579             {
4580               if (original_problem == no_problem)
4581                 {
4582                   original_problem = pb;
4583                   result = omega_solve_geq (rS, omega_false);
4584                   original_problem = no_problem;
4585                 }
4586               else
4587                 result = omega_solve_geq (rS, omega_false);
4588
4589               if (result == omega_false)
4590                 {
4591                   free (rS);
4592                   free (iS);
4593                   return result;
4594                 }
4595
4596               if (pb->num_eqs > 0)
4597                 {
4598                   /* An equality constraint must have been found */
4599                   free (rS);
4600                   free (iS);
4601                   return omega_solve_problem (pb, desired_res);
4602                 }
4603             }
4604
4605           if (desired_res != omega_false)
4606             {
4607               int j;
4608               int lower_bounds = 0;
4609               int *lower_bound = XNEWVEC (int, OMEGA_MAX_GEQS);
4610
4611               if (possible_easy_int_solution)
4612                 {
4613                   conservative++;
4614                   result = omega_solve_geq (iS, desired_res);
4615                   conservative--;
4616
4617                   if (result != omega_false)
4618                     {
4619                       free (rS);
4620                       free (iS);
4621                       free (lower_bound);
4622                       return result;
4623                     }
4624                 }
4625
4626               if (!exact && best_parallel_eqn >= 0
4627                   && parallel_difference <= max_splinters)
4628                 {
4629                   free (rS);
4630                   free (iS);
4631                   free (lower_bound);
4632                   return parallel_splinter (pb, best_parallel_eqn,
4633                                             parallel_difference,
4634                                             desired_res);
4635                 }
4636
4637               if (dump_file && (dump_flags & TDF_DETAILS))
4638                 fprintf (dump_file, "have to do exact analysis\n");
4639
4640               conservative++;
4641
4642               for (e = 0; e < pb->num_geqs; e++)
4643                 if (pb->geqs[e].coef[i] > 1)
4644                   lower_bound[lower_bounds++] = e;
4645
4646               /* Sort array LOWER_BOUND.  */
4647               for (j = 0; j < lower_bounds; j++)
4648                 {
4649                   int k, smallest = j;
4650
4651                   for (k = j + 1; k < lower_bounds; k++)
4652                     if (pb->geqs[lower_bound[smallest]].coef[i] >
4653                         pb->geqs[lower_bound[k]].coef[i])
4654                       smallest = k;
4655
4656                   k = lower_bound[smallest];
4657                   lower_bound[smallest] = lower_bound[j];
4658                   lower_bound[j] = k;
4659                 }
4660
4661               if (dump_file && (dump_flags & TDF_DETAILS))
4662                 {
4663                   fprintf (dump_file, "lower bound coefficients = ");
4664
4665                   for (j = 0; j < lower_bounds; j++)
4666                     fprintf (dump_file, " %d",
4667                              pb->geqs[lower_bound[j]].coef[i]);
4668
4669                   fprintf (dump_file, "\n");
4670                 }
4671
4672               for (j = 0; j < lower_bounds; j++)
4673                 {
4674                   int max_incr;
4675                   int c;
4676                   int worst_lower_bound_constant = -minC;
4677
4678                   e = lower_bound[j];
4679                   max_incr = (((pb->geqs[e].coef[i] - 1) *
4680                                (worst_lower_bound_constant - 1) - 1)
4681                               / worst_lower_bound_constant);
4682                   /* max_incr += 2; */
4683
4684                   if (dump_file && (dump_flags & TDF_DETAILS))
4685                     {
4686                       fprintf (dump_file, "for equation ");
4687                       omega_print_geq (dump_file, pb, &pb->geqs[e]);
4688                       fprintf (dump_file,
4689                                "\ntry decrements from 0 to %d\n",
4690                                max_incr);
4691                       omega_print_problem (dump_file, pb);
4692                     }
4693
4694                   if (max_incr > 50 && !smoothed
4695                       && smooth_weird_equations (pb))
4696                     {
4697                       conservative--;
4698                       free (rS);
4699                       free (iS);
4700                       smoothed = true;
4701                       goto solve_geq_start;
4702                     }
4703
4704                   omega_copy_eqn (&pb->eqs[0], &pb->geqs[e],
4705                                   pb->num_vars);
4706                   pb->eqs[0].color = omega_black;
4707                   omega_init_eqn_zero (&pb->geqs[e], pb->num_vars);
4708                   pb->geqs[e].touched = 1;
4709                   pb->num_eqs = 1;
4710
4711                   for (c = max_incr; c >= 0; c--)
4712                     {
4713                       if (dump_file && (dump_flags & TDF_DETAILS))
4714                         {
4715                           fprintf (dump_file,
4716                                    "trying next decrement of %d\n",
4717                                    max_incr - c);
4718                           omega_print_problem (dump_file, pb);
4719                         }
4720
4721                       omega_copy_problem (rS, pb);
4722
4723                       if (dump_file && (dump_flags & TDF_DETAILS))
4724                         omega_print_problem (dump_file, rS);
4725
4726                       result = omega_solve_problem (rS, desired_res);
4727
4728                       if (result == omega_true)
4729                         {
4730                           free (rS);
4731                           free (iS);
4732                           free (lower_bound);
4733                           conservative--;
4734                           return omega_true;
4735                         }
4736
4737                       pb->eqs[0].coef[0]--;
4738                     }
4739
4740                   if (j + 1 < lower_bounds)
4741                     {
4742                       pb->num_eqs = 0;
4743                       omega_copy_eqn (&pb->geqs[e], &pb->eqs[0],
4744                                       pb->num_vars);
4745                       pb->geqs[e].touched = 1;
4746                       pb->geqs[e].color = omega_black;
4747                       omega_copy_problem (rS, pb);
4748
4749                       if (dump_file && (dump_flags & TDF_DETAILS))
4750                         fprintf (dump_file,
4751                                  "exhausted lower bound, "
4752                                  "checking if still feasible ");
4753
4754                       result = omega_solve_problem (rS, omega_false);
4755
4756                       if (result == omega_false)
4757                         break;
4758                     }
4759                 }
4760
4761               if (dump_file && (dump_flags & TDF_DETAILS))
4762                 fprintf (dump_file, "fall-off the end\n");
4763
4764               free (rS);
4765               free (iS);
4766               free (lower_bound);
4767               conservative--;
4768               return omega_false;
4769             }
4770
4771           free (rS);
4772           free (iS);
4773         }
4774       return omega_unknown;
4775     } while (eliminate_again);
4776   } while (1);
4777 }
4778
4779 /* Because the omega solver is recursive, this counter limits the
4780    recursion depth.  */
4781 static int omega_solve_depth = 0;
4782
4783 /* Return omega_true when the problem PB has a solution following the
4784    DESIRED_RES.  */
4785
4786 enum omega_result
4787 omega_solve_problem (omega_pb pb, enum omega_result desired_res)
4788 {
4789   enum omega_result result;
4790
4791   gcc_assert (pb->num_vars >= pb->safe_vars);
4792   omega_solve_depth++;
4793
4794   if (desired_res != omega_simplify)
4795     pb->safe_vars = 0;
4796
4797   if (omega_solve_depth > 50)
4798     {
4799       if (dump_file && (dump_flags & TDF_DETAILS))
4800         {
4801           fprintf (dump_file,
4802                    "Solve depth = %d, in_approximate_mode = %d, aborting\n",
4803                    omega_solve_depth, in_approximate_mode);
4804           omega_print_problem (dump_file, pb);
4805         }
4806       gcc_assert (0);
4807     }
4808
4809   if (omega_solve_eq (pb, desired_res) == omega_false)
4810     {
4811       omega_solve_depth--;
4812       return omega_false;
4813     }
4814
4815   if (in_approximate_mode && !pb->num_geqs)
4816     {
4817       result = omega_true;
4818       pb->num_vars = pb->safe_vars;
4819       omega_problem_reduced (pb);
4820     }
4821   else
4822     result = omega_solve_geq (pb, desired_res);
4823
4824   omega_solve_depth--;
4825
4826   if (!omega_reduce_with_subs)
4827     {
4828       resurrect_subs (pb);
4829       gcc_assert (please_no_equalities_in_simplified_problems
4830                   || !result || pb->num_subs == 0);
4831     }
4832
4833   return result;
4834 }
4835
4836 /* Return true if red equations constrain the set of possible solutions.
4837    We assume that there are solutions to the black equations by
4838    themselves, so if there is no solution to the combined problem, we
4839    return true.  */
4840
4841 bool
4842 omega_problem_has_red_equations (omega_pb pb)
4843 {
4844   bool result;
4845   int e;
4846   int i;
4847
4848   if (dump_file && (dump_flags & TDF_DETAILS))
4849     {
4850       fprintf (dump_file, "Checking for red equations:\n");
4851       omega_print_problem (dump_file, pb);
4852     }
4853
4854   please_no_equalities_in_simplified_problems++;
4855   may_be_red++;
4856
4857   if (omega_single_result)
4858     return_single_result++;
4859
4860   create_color = true;
4861   result = (omega_simplify_problem (pb) == omega_false);
4862
4863   if (omega_single_result)
4864     return_single_result--;
4865
4866   may_be_red--;
4867   please_no_equalities_in_simplified_problems--;
4868
4869   if (result)
4870     {
4871       if (dump_file && (dump_flags & TDF_DETAILS))
4872         fprintf (dump_file, "Gist is FALSE\n");
4873
4874       pb->num_subs = 0;
4875       pb->num_geqs = 0;
4876       pb->num_eqs = 1;
4877       pb->eqs[0].color = omega_red;
4878
4879       for (i = pb->num_vars; i > 0; i--)
4880         pb->eqs[0].coef[i] = 0;
4881
4882       pb->eqs[0].coef[0] = 1;
4883       return true;
4884     }
4885
4886   free_red_eliminations (pb);
4887   gcc_assert (pb->num_eqs == 0);
4888
4889   for (e = pb->num_geqs - 1; e >= 0; e--)
4890     if (pb->geqs[e].color == omega_red)
4891       result = true;
4892
4893   if (!result)
4894     return false;
4895
4896   for (i = pb->safe_vars; i >= 1; i--)
4897     {
4898       int ub = 0;
4899       int lb = 0;
4900
4901       for (e = pb->num_geqs - 1; e >= 0; e--)
4902         {
4903           if (pb->geqs[e].coef[i])
4904             {
4905               if (pb->geqs[e].coef[i] > 0)
4906                 lb |= (1 + (pb->geqs[e].color == omega_red ? 1 : 0));
4907
4908               else
4909                 ub |= (1 + (pb->geqs[e].color == omega_red ? 1 : 0));
4910             }
4911         }
4912
4913       if (ub == 2 || lb == 2)
4914         {
4915
4916           if (dump_file && (dump_flags & TDF_DETAILS))
4917             fprintf (dump_file, "checks for upper/lower bounds worked!\n");
4918
4919           if (!omega_reduce_with_subs)
4920             {
4921               resurrect_subs (pb);
4922               gcc_assert (pb->num_subs == 0);
4923             }
4924
4925           return true;
4926         }
4927     }
4928
4929
4930   if (dump_file && (dump_flags & TDF_DETAILS))
4931     fprintf (dump_file,
4932              "*** Doing potentially expensive elimination tests "
4933              "for red equations\n");
4934
4935   please_no_equalities_in_simplified_problems++;
4936   omega_eliminate_red (pb, true);
4937   please_no_equalities_in_simplified_problems--;
4938
4939   result = false;
4940   gcc_assert (pb->num_eqs == 0);
4941
4942   for (e = pb->num_geqs - 1; e >= 0; e--)
4943     if (pb->geqs[e].color == omega_red)
4944       result = true;
4945
4946   if (dump_file && (dump_flags & TDF_DETAILS))
4947     {
4948       if (!result)
4949         fprintf (dump_file,
4950                  "******************** Redundant Red Equations eliminated!!\n");
4951       else
4952         fprintf (dump_file,
4953                  "******************** Red Equations remain\n");
4954
4955       omega_print_problem (dump_file, pb);
4956     }
4957
4958   if (!omega_reduce_with_subs)
4959     {
4960       normalize_return_type r;
4961
4962       resurrect_subs (pb);
4963       r = normalize_omega_problem (pb);
4964       gcc_assert (r != normalize_false);
4965
4966       coalesce (pb);
4967       cleanout_wildcards (pb);
4968       gcc_assert (pb->num_subs == 0);
4969     }
4970
4971   return result;
4972 }
4973
4974 /* Calls omega_simplify_problem in approximate mode.  */
4975
4976 enum omega_result
4977 omega_simplify_approximate (omega_pb pb)
4978 {
4979   enum omega_result result;
4980
4981   if (dump_file && (dump_flags & TDF_DETAILS))
4982     fprintf (dump_file, "(Entering approximate mode\n");
4983
4984   in_approximate_mode = true;
4985   result = omega_simplify_problem (pb);
4986   in_approximate_mode = false;
4987
4988   gcc_assert (pb->num_vars == pb->safe_vars);
4989   if (!omega_reduce_with_subs)
4990     gcc_assert (pb->num_subs == 0);
4991
4992   if (dump_file && (dump_flags & TDF_DETAILS))
4993     fprintf (dump_file, "Leaving approximate mode)\n");
4994
4995   return result;
4996 }
4997
4998
4999 /* Simplifies problem PB by eliminating redundant constraints and
5000    reducing the constraints system to a minimal form.  Returns
5001    omega_true when the problem was successfully reduced, omega_unknown
5002    when the solver is unable to determine an answer.  */
5003
5004 enum omega_result
5005 omega_simplify_problem (omega_pb pb)
5006 {
5007   int i;
5008
5009   omega_found_reduction = omega_false;
5010
5011   if (!pb->variables_initialized)
5012     omega_initialize_variables (pb);
5013
5014   if (next_key * 3 > MAX_KEYS)
5015     {
5016       int e;
5017
5018       hash_version++;
5019       next_key = OMEGA_MAX_VARS + 1;
5020
5021       for (e = pb->num_geqs - 1; e >= 0; e--)
5022         pb->geqs[e].touched = 1;
5023
5024       for (i = 0; i < HASH_TABLE_SIZE; i++)
5025         hash_master[i].touched = -1;
5026
5027       pb->hash_version = hash_version;
5028     }
5029
5030   else if (pb->hash_version != hash_version)
5031     {
5032       int e;
5033
5034       for (e = pb->num_geqs - 1; e >= 0; e--)
5035         pb->geqs[e].touched = 1;
5036
5037       pb->hash_version = hash_version;
5038     }
5039
5040   if (pb->num_vars > pb->num_eqs + 3 * pb->safe_vars)
5041     omega_free_eliminations (pb, pb->safe_vars);
5042
5043   if (!may_be_red && pb->num_subs == 0 && pb->safe_vars == 0)
5044     {
5045       omega_found_reduction = omega_solve_problem (pb, omega_unknown);
5046
5047       if (omega_found_reduction != omega_false
5048           && !return_single_result)
5049         {
5050           pb->num_geqs = 0;
5051           pb->num_eqs = 0;
5052           (*omega_when_reduced) (pb);
5053         }
5054
5055       return omega_found_reduction;
5056     }
5057
5058   omega_solve_problem (pb, omega_simplify);
5059
5060   if (omega_found_reduction != omega_false)
5061     {
5062       for (i = 1; omega_safe_var_p (pb, i); i++)
5063         pb->forwarding_address[pb->var[i]] = i;
5064
5065       for (i = 0; i < pb->num_subs; i++)
5066         pb->forwarding_address[pb->subs[i].key] = -i - 1;
5067     }
5068
5069   if (!omega_reduce_with_subs)
5070     gcc_assert (please_no_equalities_in_simplified_problems
5071                 || omega_found_reduction == omega_false
5072                 || pb->num_subs == 0);
5073
5074   return omega_found_reduction;
5075 }
5076
5077 /* Make variable VAR unprotected: it then can be eliminated.  */
5078
5079 void
5080 omega_unprotect_variable (omega_pb pb, int var)
5081 {
5082   int e, idx;
5083   idx = pb->forwarding_address[var];
5084
5085   if (idx < 0)
5086     {
5087       idx = -1 - idx;
5088       pb->num_subs--;
5089
5090       if (idx < pb->num_subs)
5091         {
5092           omega_copy_eqn (&pb->subs[idx], &pb->subs[pb->num_subs],
5093                           pb->num_vars);
5094           pb->forwarding_address[pb->subs[idx].key] = -idx - 1;
5095         }
5096     }
5097   else
5098     {
5099       int *bring_to_life = XNEWVEC (int, OMEGA_MAX_VARS);
5100       int e2;
5101
5102       for (e = pb->num_subs - 1; e >= 0; e--)
5103         bring_to_life[e] = (pb->subs[e].coef[idx] != 0);
5104
5105       for (e2 = pb->num_subs - 1; e2 >= 0; e2--)
5106         if (bring_to_life[e2])
5107           {
5108             pb->num_vars++;
5109             pb->safe_vars++;
5110
5111             if (pb->safe_vars < pb->num_vars)
5112               {
5113                 for (e = pb->num_geqs - 1; e >= 0; e--)
5114                   {
5115                     pb->geqs[e].coef[pb->num_vars] =
5116                       pb->geqs[e].coef[pb->safe_vars];
5117
5118                     pb->geqs[e].coef[pb->safe_vars] = 0;
5119                   }
5120
5121                 for (e = pb->num_eqs - 1; e >= 0; e--)
5122                   {
5123                     pb->eqs[e].coef[pb->num_vars] =
5124                       pb->eqs[e].coef[pb->safe_vars];
5125
5126                     pb->eqs[e].coef[pb->safe_vars] = 0;
5127                   }
5128
5129                 for (e = pb->num_subs - 1; e >= 0; e--)
5130                   {
5131                     pb->subs[e].coef[pb->num_vars] =
5132                       pb->subs[e].coef[pb->safe_vars];
5133
5134                     pb->subs[e].coef[pb->safe_vars] = 0;
5135                   }
5136
5137                 pb->var[pb->num_vars] = pb->var[pb->safe_vars];
5138                 pb->forwarding_address[pb->var[pb->num_vars]] =
5139                   pb->num_vars;
5140               }
5141             else
5142               {
5143                 for (e = pb->num_geqs - 1; e >= 0; e--)
5144                   pb->geqs[e].coef[pb->safe_vars] = 0;
5145
5146                 for (e = pb->num_eqs - 1; e >= 0; e--)
5147                   pb->eqs[e].coef[pb->safe_vars] = 0;
5148
5149                 for (e = pb->num_subs - 1; e >= 0; e--)
5150                   pb->subs[e].coef[pb->safe_vars] = 0;
5151               }
5152
5153             pb->var[pb->safe_vars] = pb->subs[e2].key;
5154             pb->forwarding_address[pb->subs[e2].key] = pb->safe_vars;
5155
5156             omega_copy_eqn (&(pb->eqs[pb->num_eqs]), &(pb->subs[e2]),
5157                             pb->num_vars);
5158             pb->eqs[pb->num_eqs++].coef[pb->safe_vars] = -1;
5159             gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5160
5161             if (e2 < pb->num_subs - 1)
5162               omega_copy_eqn (&(pb->subs[e2]), &(pb->subs[pb->num_subs - 1]),
5163                               pb->num_vars);
5164
5165             pb->num_subs--;
5166           }
5167
5168       omega_unprotect_1 (pb, &idx, NULL);
5169       free (bring_to_life);
5170     }
5171
5172   chain_unprotect (pb);
5173 }
5174
5175 /* Unprotects VAR and simplifies PB.  */
5176
5177 enum omega_result
5178 omega_constrain_variable_sign (omega_pb pb, enum omega_eqn_color color,
5179                                int var, int sign)
5180 {
5181   int n_vars = pb->num_vars;
5182   int e, j;
5183   int k = pb->forwarding_address[var];
5184
5185   if (k < 0)
5186     {
5187       k = -1 - k;
5188
5189       if (sign != 0)
5190         {
5191           e = pb->num_geqs++;
5192           omega_copy_eqn (&pb->geqs[e], &pb->subs[k], pb->num_vars);
5193
5194           for (j = 0; j <= n_vars; j++)
5195             pb->geqs[e].coef[j] *= sign;
5196
5197           pb->geqs[e].coef[0]--;
5198           pb->geqs[e].touched = 1;
5199           pb->geqs[e].color = color;
5200         }
5201       else
5202         {
5203           e = pb->num_eqs++;
5204           gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5205           omega_copy_eqn (&pb->eqs[e], &pb->subs[k], pb->num_vars);
5206           pb->eqs[e].color = color;
5207         }
5208     }
5209   else if (sign != 0)
5210     {
5211       e = pb->num_geqs++;
5212       omega_init_eqn_zero (&pb->geqs[e], pb->num_vars);
5213       pb->geqs[e].coef[k] = sign;
5214       pb->geqs[e].coef[0] = -1;
5215       pb->geqs[e].touched = 1;
5216       pb->geqs[e].color = color;
5217     }
5218   else
5219     {
5220       e = pb->num_eqs++;
5221       gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5222       omega_init_eqn_zero (&pb->eqs[e], pb->num_vars);
5223       pb->eqs[e].coef[k] = 1;
5224       pb->eqs[e].color = color;
5225     }
5226
5227   omega_unprotect_variable (pb, var);
5228   return omega_simplify_problem (pb);
5229 }
5230
5231 /* Add an equation "VAR = VALUE" with COLOR to PB.  */
5232
5233 void
5234 omega_constrain_variable_value (omega_pb pb, enum omega_eqn_color color,
5235                                 int var, int value)
5236 {
5237   int e;
5238   int k = pb->forwarding_address[var];
5239
5240   if (k < 0)
5241     {
5242       k = -1 - k;
5243       e = pb->num_eqs++;
5244       gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5245       omega_copy_eqn (&pb->eqs[e], &pb->subs[k], pb->num_vars);
5246       pb->eqs[e].coef[0] -= value;
5247     }
5248   else
5249     {
5250       e = pb->num_eqs++;
5251       omega_init_eqn_zero (&pb->eqs[e], pb->num_vars);
5252       pb->eqs[e].coef[k] = 1;
5253       pb->eqs[e].coef[0] = -value;
5254     }
5255
5256   pb->eqs[e].color = color;
5257 }
5258
5259 /* Return false when the upper and lower bounds are not coupled.
5260    Initialize the bounds LOWER_BOUND and UPPER_BOUND for the values of
5261    variable I.  */
5262
5263 bool
5264 omega_query_variable (omega_pb pb, int i, int *lower_bound, int *upper_bound)
5265 {
5266   int n_vars = pb->num_vars;
5267   int e, j;
5268   bool is_simple;
5269   bool coupled = false;
5270
5271   *lower_bound = neg_infinity;
5272   *upper_bound = pos_infinity;
5273   i = pb->forwarding_address[i];
5274
5275   if (i < 0)
5276     {
5277       i = -i - 1;
5278
5279       for (j = 1; j <= n_vars; j++)
5280         if (pb->subs[i].coef[j] != 0)
5281           return true;
5282
5283       *upper_bound = *lower_bound = pb->subs[i].coef[0];
5284       return false;
5285     }
5286
5287   for (e = pb->num_subs - 1; e >= 0; e--)
5288     if (pb->subs[e].coef[i] != 0)
5289       coupled = true;
5290
5291   for (e = pb->num_eqs - 1; e >= 0; e--)
5292     if (pb->eqs[e].coef[i] != 0)
5293       {
5294         is_simple = true;
5295
5296         for (j = 1; j <= n_vars; j++)
5297           if (i != j && pb->eqs[e].coef[j] != 0)
5298             {
5299               is_simple = false;
5300               coupled = true;
5301               break;
5302             }
5303
5304         if (!is_simple)
5305           continue;
5306         else
5307           {
5308             *lower_bound = *upper_bound =
5309               -pb->eqs[e].coef[i] * pb->eqs[e].coef[0];
5310             return false;
5311           }
5312       }
5313
5314   for (e = pb->num_geqs - 1; e >= 0; e--)
5315     if (pb->geqs[e].coef[i] != 0)
5316       {
5317         if (pb->geqs[e].key == i)
5318           *lower_bound = MAX (*lower_bound, -pb->geqs[e].coef[0]);
5319
5320         else if (pb->geqs[e].key == -i)
5321           *upper_bound = MIN (*upper_bound, pb->geqs[e].coef[0]);
5322
5323         else
5324           coupled = true;
5325       }
5326
5327   return coupled;
5328 }
5329
5330 /* Sets the lower bound L and upper bound U for the values of variable
5331    I, and sets COULD_BE_ZERO to true if variable I might take value
5332    zero.  LOWER_BOUND and UPPER_BOUND are bounds on the values of
5333    variable I.  */
5334
5335 static void
5336 query_coupled_variable (omega_pb pb, int i, int *l, int *u,
5337                         bool *could_be_zero, int lower_bound, int upper_bound)
5338 {
5339   int e, b1, b2;
5340   eqn eqn;
5341   int sign;
5342   int v;
5343
5344   /* Preconditions.  */
5345   gcc_assert (abs (pb->forwarding_address[i]) == 1
5346               && pb->num_vars + pb->num_subs == 2
5347               && pb->num_eqs + pb->num_subs == 1);
5348
5349   /* Define variable I in terms of variable V.  */
5350   if (pb->forwarding_address[i] == -1)
5351     {
5352       eqn = &pb->subs[0];
5353       sign = 1;
5354       v = 1;
5355     }
5356   else
5357     {
5358       eqn = &pb->eqs[0];
5359       sign = -eqn->coef[1];
5360       v = 2;
5361     }
5362
5363   for (e = pb->num_geqs - 1; e >= 0; e--)
5364     if (pb->geqs[e].coef[v] != 0)
5365       {
5366         if (pb->geqs[e].coef[v] == 1)
5367           lower_bound = MAX (lower_bound, -pb->geqs[e].coef[0]);
5368
5369         else
5370           upper_bound = MIN (upper_bound, pb->geqs[e].coef[0]);
5371       }
5372
5373   if (lower_bound > upper_bound)
5374     {
5375       *l = pos_infinity;
5376       *u = neg_infinity;
5377       *could_be_zero = 0;
5378       return;
5379     }
5380
5381   if (lower_bound == neg_infinity)
5382     {
5383       if (eqn->coef[v] > 0)
5384         b1 = sign * neg_infinity;
5385
5386       else
5387         b1 = -sign * neg_infinity;
5388     }
5389   else
5390     b1 = sign * (eqn->coef[0] + eqn->coef[v] * lower_bound);
5391
5392   if (upper_bound == pos_infinity)
5393     {
5394       if (eqn->coef[v] > 0)
5395         b2 = sign * pos_infinity;
5396
5397       else
5398         b2 = -sign * pos_infinity;
5399     }
5400   else
5401     b2 = sign * (eqn->coef[0] + eqn->coef[v] * upper_bound);
5402
5403   *l = MAX (*l, b1 <= b2 ? b1 : b2);
5404   *u = MIN (*u, b1 <= b2 ? b2 : b1);
5405
5406   *could_be_zero = (*l <= 0 && 0 <= *u
5407                     && int_mod (eqn->coef[0], abs (eqn->coef[v])) == 0);
5408 }
5409
5410 /* Return false when a lower bound L and an upper bound U for variable
5411    I in problem PB have been initialized.  */
5412
5413 bool
5414 omega_query_variable_bounds (omega_pb pb, int i, int *l, int *u)
5415 {
5416   *l = neg_infinity;
5417   *u = pos_infinity;
5418
5419   if (!omega_query_variable (pb, i, l, u)
5420       || (pb->num_vars == 1 && pb->forwarding_address[i] == 1))
5421     return false;
5422
5423   if (abs (pb->forwarding_address[i]) == 1
5424       && pb->num_vars + pb->num_subs == 2
5425       && pb->num_eqs + pb->num_subs == 1)
5426     {
5427       bool could_be_zero;
5428       query_coupled_variable (pb, i, l, u, &could_be_zero, neg_infinity,
5429                               pos_infinity);
5430       return false;
5431     }
5432
5433   return true;
5434 }
5435
5436 /* For problem PB, return an integer that represents the classic data
5437    dependence direction in function of the DD_LT, DD_EQ and DD_GT bit
5438    masks that are added to the result.  When DIST_KNOWN is true, DIST
5439    is set to the classic data dependence distance.  LOWER_BOUND and
5440    UPPER_BOUND are bounds on the value of variable I, for example, it
5441    is possible to narrow the iteration domain with safe approximations
5442    of loop counts, and thus discard some data dependences that cannot
5443    occur.  */
5444
5445 int
5446 omega_query_variable_signs (omega_pb pb, int i, int dd_lt,
5447                             int dd_eq, int dd_gt, int lower_bound,
5448                             int upper_bound, bool *dist_known, int *dist)
5449 {
5450   int result;
5451   int l, u;
5452   bool could_be_zero;
5453
5454   l = neg_infinity;
5455   u = pos_infinity;
5456
5457   omega_query_variable (pb, i, &l, &u);
5458   query_coupled_variable (pb, i, &l, &u, &could_be_zero, lower_bound,
5459                           upper_bound);
5460   result = 0;
5461
5462   if (l < 0)
5463     result |= dd_gt;
5464
5465   if (u > 0)
5466     result |= dd_lt;
5467
5468   if (could_be_zero)
5469     result |= dd_eq;
5470
5471   if (l == u)
5472     {
5473       *dist_known = true;
5474       *dist = l;
5475     }
5476   else
5477     *dist_known = false;
5478
5479   return result;
5480 }
5481
5482 /* Initialize PB as an Omega problem with NVARS variables and NPROT
5483    safe variables.  Safe variables are not eliminated during the
5484    Fourier-Motzkin elimination.  Safe variables are all those
5485    variables that are placed at the beginning of the array of
5486    variables: P->var[0, ..., NPROT - 1].  */
5487
5488 omega_pb
5489 omega_alloc_problem (int nvars, int nprot)
5490 {
5491   omega_pb pb;
5492
5493   gcc_assert (nvars <= OMEGA_MAX_VARS);
5494   omega_initialize ();
5495
5496   /* Allocate and initialize PB.  */
5497   pb = XCNEW (struct omega_pb_d);
5498   pb->var = XCNEWVEC (int, OMEGA_MAX_VARS + 2);
5499   pb->forwarding_address = XCNEWVEC (int, OMEGA_MAX_VARS + 2);
5500   pb->geqs = omega_alloc_eqns (0, OMEGA_MAX_GEQS);
5501   pb->eqs = omega_alloc_eqns (0, OMEGA_MAX_EQS);
5502   pb->subs = omega_alloc_eqns (0, OMEGA_MAX_VARS + 1);
5503
5504   pb->hash_version = hash_version;
5505   pb->num_vars = nvars;
5506   pb->safe_vars = nprot;
5507   pb->variables_initialized = false;
5508   pb->variables_freed = false;
5509   pb->num_eqs = 0;
5510   pb->num_geqs = 0;
5511   pb->num_subs = 0;
5512   return pb;
5513 }
5514
5515 /* Keeps the state of the initialization.  */
5516 static bool omega_initialized = false;
5517
5518 /* Initialization of the Omega solver.  */
5519
5520 void
5521 omega_initialize (void)
5522 {
5523   int i;
5524
5525   if (omega_initialized)
5526     return;
5527
5528   next_wild_card = 0;
5529   next_key = OMEGA_MAX_VARS + 1;
5530   packing = XCNEWVEC (int, OMEGA_MAX_VARS);
5531   fast_lookup = XCNEWVEC (int, MAX_KEYS * 2);
5532   fast_lookup_red = XCNEWVEC (int, MAX_KEYS * 2);
5533   hash_master = omega_alloc_eqns (0, HASH_TABLE_SIZE);
5534
5535   for (i = 0; i < HASH_TABLE_SIZE; i++)
5536     hash_master[i].touched = -1;
5537
5538   sprintf (wild_name[0], "1");
5539   sprintf (wild_name[1], "a");
5540   sprintf (wild_name[2], "b");
5541   sprintf (wild_name[3], "c");
5542   sprintf (wild_name[4], "d");
5543   sprintf (wild_name[5], "e");
5544   sprintf (wild_name[6], "f");
5545   sprintf (wild_name[7], "g");
5546   sprintf (wild_name[8], "h");
5547   sprintf (wild_name[9], "i");
5548   sprintf (wild_name[10], "j");
5549   sprintf (wild_name[11], "k");
5550   sprintf (wild_name[12], "l");
5551   sprintf (wild_name[13], "m");
5552   sprintf (wild_name[14], "n");
5553   sprintf (wild_name[15], "o");
5554   sprintf (wild_name[16], "p");
5555   sprintf (wild_name[17], "q");
5556   sprintf (wild_name[18], "r");
5557   sprintf (wild_name[19], "s");
5558   sprintf (wild_name[20], "t");
5559   sprintf (wild_name[40 - 1], "alpha");
5560   sprintf (wild_name[40 - 2], "beta");
5561   sprintf (wild_name[40 - 3], "gamma");
5562   sprintf (wild_name[40 - 4], "delta");
5563   sprintf (wild_name[40 - 5], "tau");
5564   sprintf (wild_name[40 - 6], "sigma");
5565   sprintf (wild_name[40 - 7], "chi");
5566   sprintf (wild_name[40 - 8], "omega");
5567   sprintf (wild_name[40 - 9], "pi");
5568   sprintf (wild_name[40 - 10], "ni");
5569   sprintf (wild_name[40 - 11], "Alpha");
5570   sprintf (wild_name[40 - 12], "Beta");
5571   sprintf (wild_name[40 - 13], "Gamma");
5572   sprintf (wild_name[40 - 14], "Delta");
5573   sprintf (wild_name[40 - 15], "Tau");
5574   sprintf (wild_name[40 - 16], "Sigma");
5575   sprintf (wild_name[40 - 17], "Chi");
5576   sprintf (wild_name[40 - 18], "Omega");
5577   sprintf (wild_name[40 - 19], "xxx");
5578
5579   omega_initialized = true;
5580 }