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