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