OSDN Git Service

* doc/loop.texi: Document the Omega linear constraints solver.
authorspop <spop@138bc75d-0d04-0410-961f-82ee72b054a4>
Fri, 9 Mar 2007 12:39:49 +0000 (12:39 +0000)
committerspop <spop@138bc75d-0d04-0410-961f-82ee72b054a4>
Fri, 9 Mar 2007 12:39:49 +0000 (12:39 +0000)
* doc/invoke.texi: Document -fcheck-data-deps, omega-max-vars,
omega-max-geqs, omega-max-eqs, omega-max-wild-cards,
omega-hash-table-size, omega-max-keys, and
omega-eliminate-redundant-constraints.
* tree-pass.h (pass_check_data_deps): Declared.
* omega.c: New.
* omega.h: New.
* timevar.def (TV_CHECK_DATA_DEPS): Declared.
* tree-ssa-loop.c (check_data_deps, gate_check_data_deps,
pass_check_data_deps): New.
* tree-data-ref.c (init_data_ref): Remove declaration.
(dump_data_dependence_relation): Dump DDR_INNER_LOOP.
(analyze_array): Renamed init_array_ref, move up initializations.
(init_data_ref): Renamed init_pointer_ref.  Moved before its call.
Removed arguments that are set to NULL.
(analyze_indirect_ref): Correct indentation, correct call to
init_pointer_ref.
(object_analysis): Call init_array_ref instead of analyze_array.
(initialize_data_dependence_relation): Initialize DDR_INNER_LOOP.
(access_functions_are_affine_or_constant_p): Use DR_ACCESS_FNS instead
of DR_ACCESS_FNS_ADDR.
(init_omega_eq_with_af, omega_extract_distance_vectors,
omega_setup_subscript, init_omega_for_ddr_1, init_omega_for_ddr,
ddr_consistent_p): New.
(compute_affine_dependence): Check consistency of ddrs when
flag_check_data_deps is passed.
(analyze_all_data_dependences): Uncomment.
(tree_check_data_deps): New.
* tree-data-ref.h: Include omega.h.
(DR_ACCESS_FNS_ADDR): Removed.
(data_dependence_relation): Add inner_loop.
(DDR_INNER_LOOP): New.
* common.opt (fcheck-data-deps): New.
* tree-flow.h (tree_check_data_deps): Declare.
* Makefile.in (TREE_DATA_REF_H): Depend on omega.h.
(OBJS-common): Depend on omega.o.
(omega.o): Define.
* passes.c (pass_check_data_deps): Scheduled.
* params.def (PARAM_OMEGA_MAX_VARS, PARAM_OMEGA_MAX_GEQS,
PARAM_OMEGA_MAX_EQS, PARAM_OMEGA_MAX_WILD_CARDS,
PARAM_OMEGA_HASH_TABLE_SIZE, PARAM_OMEGA_MAX_KEYS,
PARAM_VECT_MAX_VERSION_CHECKS,
PARAM_OMEGA_ELIMINATE_REDUNDANT_CONSTRAINTS): New.

git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@122749 138bc75d-0d04-0410-961f-82ee72b054a4

15 files changed:
gcc/ChangeLog
gcc/Makefile.in
gcc/common.opt
gcc/doc/invoke.texi
gcc/doc/loop.texi
gcc/omega.c [new file with mode: 0644]
gcc/omega.h [new file with mode: 0644]
gcc/params.def
gcc/passes.c
gcc/timevar.def
gcc/tree-data-ref.c
gcc/tree-data-ref.h
gcc/tree-flow.h
gcc/tree-pass.h
gcc/tree-ssa-loop.c

index 576aab0..ffb5e3d 100644 (file)
@@ -1,3 +1,50 @@
+2007-03-09  Sebastian Pop  <sebastian.pop@inria.fr>
+
+       * doc/loop.texi: Document the Omega linear constraints solver.
+       * doc/invoke.texi: Document -fcheck-data-deps, omega-max-vars,
+       omega-max-geqs, omega-max-eqs, omega-max-wild-cards, 
+       omega-hash-table-size, omega-max-keys, and 
+       omega-eliminate-redundant-constraints.
+       * tree-pass.h (pass_check_data_deps): Declared.
+       * omega.c: New.
+       * omega.h: New.
+       * timevar.def (TV_CHECK_DATA_DEPS): Declared.
+       * tree-ssa-loop.c (check_data_deps, gate_check_data_deps, 
+       pass_check_data_deps): New.
+       * tree-data-ref.c (init_data_ref): Remove declaration.
+       (dump_data_dependence_relation): Dump DDR_INNER_LOOP.
+       (analyze_array): Renamed init_array_ref, move up initializations.
+       (init_data_ref): Renamed init_pointer_ref.  Moved before its call.
+       Removed arguments that are set to NULL.
+       (analyze_indirect_ref): Correct indentation, correct call to 
+       init_pointer_ref.
+       (object_analysis): Call init_array_ref instead of analyze_array.
+       (initialize_data_dependence_relation): Initialize DDR_INNER_LOOP.
+       (access_functions_are_affine_or_constant_p): Use DR_ACCESS_FNS instead
+       of DR_ACCESS_FNS_ADDR.
+       (init_omega_eq_with_af, omega_extract_distance_vectors, 
+       omega_setup_subscript, init_omega_for_ddr_1, init_omega_for_ddr,
+       ddr_consistent_p): New.
+       (compute_affine_dependence): Check consistency of ddrs when 
+       flag_check_data_deps is passed.
+       (analyze_all_data_dependences): Uncomment.
+       (tree_check_data_deps): New.
+       * tree-data-ref.h: Include omega.h.
+       (DR_ACCESS_FNS_ADDR): Removed.
+       (data_dependence_relation): Add inner_loop.
+       (DDR_INNER_LOOP): New.
+       * common.opt (fcheck-data-deps): New.
+       * tree-flow.h (tree_check_data_deps): Declare.
+       * Makefile.in (TREE_DATA_REF_H): Depend on omega.h.
+       (OBJS-common): Depend on omega.o.
+       (omega.o): Define.
+       * passes.c (pass_check_data_deps): Scheduled.
+       * params.def (PARAM_OMEGA_MAX_VARS, PARAM_OMEGA_MAX_GEQS, 
+       PARAM_OMEGA_MAX_EQS, PARAM_OMEGA_MAX_WILD_CARDS,
+       PARAM_OMEGA_HASH_TABLE_SIZE, PARAM_OMEGA_MAX_KEYS,
+       PARAM_VECT_MAX_VERSION_CHECKS,
+       PARAM_OMEGA_ELIMINATE_REDUNDANT_CONSTRAINTS): New.
+
 2007-03-09  Richard Guenther  <rguenther@suse.de>
 
        PR tree-optimization/30904
index 82821cb..a8792b8 100644 (file)
@@ -785,7 +785,7 @@ DIAGNOSTIC_H = diagnostic.h diagnostic.def $(PRETTY_PRINT_H) options.h
 C_PRETTY_PRINT_H = c-pretty-print.h $(PRETTY_PRINT_H) $(C_COMMON_H) $(TREE_H)
 SCEV_H = tree-scalar-evolution.h $(GGC_H) tree-chrec.h $(PARAMS_H)
 LAMBDA_H = lambda.h $(TREE_H) vec.h $(GGC_H)
-TREE_DATA_REF_H = tree-data-ref.h $(LAMBDA_H)
+TREE_DATA_REF_H = tree-data-ref.h $(LAMBDA_H) omega.h
 VARRAY_H = varray.h $(MACHMODE_H) $(SYSTEM_H) coretypes.h $(TM_H)
 TREE_INLINE_H = tree-inline.h $(VARRAY_H) $(SPLAY_TREE_H)
 REAL_H = real.h $(MACHMODE_H)
@@ -1028,6 +1028,7 @@ OBJS-common = \
        lower-subreg.o \
        mode-switching.o \
        modulo-sched.o \
+       omega.o \
        omp-low.o \
        optabs.o \
        options.o \
@@ -2191,6 +2192,8 @@ omp-low.o : omp-low.c $(CONFIG_H) $(SYSTEM_H) coretypes.h $(TM_H) $(TREE_H) \
 tree-browser.o : tree-browser.c tree-browser.def $(CONFIG_H) $(SYSTEM_H) \
    $(TREE_H) $(TREE_INLINE_H) $(DIAGNOSTIC_H) $(HASHTAB_H) \
    $(TM_H) coretypes.h
+omega.o : omega.c omega.h $(CONFIG_H) $(SYSTEM_H) coretypes.h $(TM_H) \
+   errors.h $(GGC_H) $(TREE_H) diagnostic.h varray.h tree-pass.h 
 tree-chrec.o: tree-chrec.c $(CONFIG_H) $(SYSTEM_H) coretypes.h $(TM_H) \
    $(GGC_H) $(TREE_H) $(REAL_H) $(SCEV_H) tree-pass.h $(PARAMS_H) \
    $(DIAGNOSTIC_H) $(CFGLOOP_H) $(TREE_FLOW_H)
index 30649a6..938ea59 100644 (file)
@@ -352,6 +352,10 @@ fcaller-saves
 Common Report Var(flag_caller_saves) Optimization
 Save registers around function calls
 
+fcheck-data-deps
+Common Report Var(flag_check_data_deps)
+Compare the results of several data dependence analyzers.
+
 fcommon
 Common Report Var(flag_no_common,0) Optimization
 Do not put uninitialized globals in the common section
index f09b9b1..6ecde2e 100644 (file)
@@ -350,6 +350,7 @@ Objective-C and Objective-C++ Dialects}.
 -fvariable-expansion-in-unroller @gol
 -ftree-pre  -ftree-ccp  -ftree-dce -ftree-loop-optimize @gol
 -ftree-loop-linear -ftree-loop-im -ftree-loop-ivcanon -fivopts @gol
+-fcheck-data-deps @gol
 -ftree-dominator-opts -ftree-dse -ftree-copyrename -ftree-sink @gol
 -ftree-ch -ftree-sra -ftree-ter -ftree-fre -ftree-vectorize @gol
 -ftree-vect-loop-version -ftree-salias -fipa-pta -fweb @gol
@@ -5447,6 +5448,10 @@ at @option{-O} and higher.
 Perform linear loop transformations on tree.  This flag can improve cache
 performance and allow further loop optimizations to take place.
 
+@item -fcheck-data-deps
+Compare the results of several data dependence analyzers.  This option
+is used for debugging the data dependence analyzers.
+
 @item -ftree-loop-im
 Perform loop invariant motion on trees.  This pass moves only invariants that
 would be hard to handle at RTL level (function calls, operations that expand to
@@ -6450,6 +6455,34 @@ optimization when a new iv is added to the set.
 Bound on size of expressions used in the scalar evolutions analyzer.
 Large expressions slow the analyzer.
 
+@item omega-max-vars
+The maximum number of variables in an Omega constraint system.
+The default value is 128.
+
+@item omega-max-geqs
+The maximum number of inequalities in an Omega constraint system.
+The default value is 256.
+
+@item omega-max-eqs
+The maximum number of equalities in an Omega constraint system.
+The default value is 128.
+
+@item omega-max-wild-cards
+The maximum number of wildcard variables that the Omega solver will
+be able to insert.  The default value is 18.
+
+@item omega-hash-table-size
+The size of the hash table in the Omega solver.  The default value is
+550.
+
+@item omega-max-keys
+The maximal number of keys used by the Omega solver.  The default
+value is 500.
+
+@item omega-eliminate-redundant-constraints
+When set to 1, use expensive methods to eliminate all redundant
+constraints.  The default value is 0.
+
 @item vect-max-version-checks
 The maximum number of runtime checks that can be performed when doing
 loop versioning in the vectorizer.  See option ftree-vect-loop-version
index 3f0076e..c904a87 100644 (file)
@@ -26,6 +26,7 @@ variable analysis and number of iterations analysis).
 * Number of iterations::       Number of iterations analysis.
 * Dependency analysis::                Data dependency analysis.
 * Lambda::                     Linear loop transformations framework.
+* Omega::                      A solver for linear programming problems.
 @end menu
 
 @node Loop representation
@@ -623,3 +624,32 @@ Given a transformed loopnest, conversion back into gcc IR is done by
 @code{lambda_loopnest_to_gcc_loopnest}.  This function will modify the
 loops so that they match the transformed loopnest.
 
+
+@node Omega
+@section Omega a solver for linear programming problems
+@cindex Omega a solver for linear programming problems
+
+The data dependence analysis contains several solvers triggered
+sequentially from the less complex ones to the more sophisticated.
+For ensuring the consistency of the results of these solvers, a data
+dependence check pass has been implemented based on two different
+solvers.  The second method that has been integrated to GCC is based
+on the Omega dependence solver, written in the 1990's by William Pugh
+and David Wonnacott.  Data dependence tests can be formulated using a
+subset of the Presburger arithmetics that can be translated to linear
+constraint systems.  These linear constraint systems can then be
+solved using the Omega solver.
+
+The Omega solver is using Fourier-Motzkin's algorithm for variable
+elimination: a linear constraint system containing @code{n} variables
+is reduced to a linear constraint system with @code{n-1} variables.
+The Omega solver can also be used for solving other problems that can
+be expressed under the form of a system of linear equalities and
+inequalities.  The Omega solver is known to have an exponential worst
+case, also known under the name of ``omega nightmare'' in the
+literature, but in practice, the omega test is known to be efficient
+for the common data dependence tests.
+
+The interface used by the Omega solver for describing the linear
+programming problems is described in @file{omega.h}, and the solver is
+@code{omega_solve_problem}.  
diff --git a/gcc/omega.c b/gcc/omega.c
new file mode 100644 (file)
index 0000000..9f5abaf
--- /dev/null
@@ -0,0 +1,5583 @@
+/* Source code for an implementation of the Omega test, an integer 
+   programming algorithm for dependence analysis, by William Pugh, 
+   appeared in Supercomputing '91 and CACM Aug 92.
+
+   This code has no license restrictions, and is considered public
+   domain.
+
+   Changes copyright (C) 2005, 2006, 2007 Free Software Foundation, Inc.
+   Contributed by Sebastian Pop <sebastian.pop@inria.fr>
+
+This file is part of GCC.
+
+GCC is free software; you can redistribute it and/or modify it under
+the terms of the GNU General Public License as published by the Free
+Software Foundation; either version 2, or (at your option) any later
+version.
+
+GCC is distributed in the hope that it will be useful, but WITHOUT ANY
+WARRANTY; without even the implied warranty of MERCHANTABILITY or
+FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
+for more details.
+
+You should have received a copy of the GNU General Public License
+along with GCC; see the file COPYING.  If not, write to the Free
+Software Foundation, 59 Temple Place - Suite 330, Boston, MA
+02111-1307, USA.  */
+
+/* For a detailed description, see "Constraint-Based Array Dependence
+   Analysis" William Pugh, David Wonnacott, TOPLAS'98 and David
+   Wonnacott's thesis:
+   ftp://ftp.cs.umd.edu/pub/omega/davewThesis/davewThesis.ps.gz
+*/
+
+#include "config.h"
+#include "system.h"
+#include "coretypes.h"
+#include "tm.h"
+#include "errors.h"
+#include "ggc.h"
+#include "tree.h"
+#include "diagnostic.h"
+#include "varray.h"
+#include "tree-pass.h"
+#include "omega.h"
+
+/* When set to true, keep substitution variables.  When set to false,
+   resurrect substitution variables (convert substitutions back to EQs).  */
+static bool omega_reduce_with_subs = true;
+
+/* When set to true, omega_simplify_problem checks for problem with no
+   solutions, calling verify_omega_pb.  */
+static bool omega_verify_simplification = false;
+
+/* When set to true, only produce a single simplified result.  */
+static bool omega_single_result = false;
+
+/* Set return_single_result to 1 when omega_single_result is true.  */
+static int return_single_result = 0;
+
+/* Hash table for equations generated by the solver.  */
+#define HASH_TABLE_SIZE PARAM_VALUE (PARAM_OMEGA_HASH_TABLE_SIZE)
+#define MAX_KEYS PARAM_VALUE (PARAM_OMEGA_MAX_KEYS)
+static eqn hash_master;
+static int next_key;
+static int hash_version = 0;
+
+/* Set to true for making the solver enter in approximation mode.  */
+static bool in_approximate_mode = false;
+
+/* When set to zero, the solver is allowed to add new equalities to
+   the problem to be solved.  */
+static int conservative = 0;
+
+/* Set to omega_true when the problem was successfully reduced, set to
+   omega_unknown when the solver is unable to determine an answer.  */
+static enum omega_result omega_found_reduction;
+
+/* Set to true when the solver is allowed to add omega_red equations.  */
+static bool create_color = false;
+
+/* Set to nonzero when the problem to be solved can be reduced.  */
+static int may_be_red = 0;
+
+/* When false, there should be no substitution equations in the
+   simplified problem.  */
+static int please_no_equalities_in_simplified_problems = 0;
+
+/* Variables names for pretty printing.  */
+static char wild_name[200][40];
+
+/* Pointer to the void problem.  */
+static omega_pb no_problem = (omega_pb) 0;
+
+/* Pointer to the problem to be solved.  */
+static omega_pb original_problem = (omega_pb) 0;
+
+
+/* Return the integer A divided by B.  */
+
+static inline int
+int_div (int a, int b)
+{
+  if (a > 0)
+    return a/b;
+  else
+    return -((-a + b - 1)/b);
+}
+
+/* Return the integer A modulo B.  */
+
+static inline int
+int_mod (int a, int b)
+{
+  return a - b * int_div (a, b);
+}
+
+/* For X and Y positive integers, return X multiplied by Y and check
+   that the result does not overflow.  */
+
+static inline int
+check_pos_mul (int x, int y)
+{
+  if (x != 0)
+    gcc_assert ((INT_MAX) / x > y);
+
+  return x * y;
+}
+
+/* Return X multiplied by Y and check that the result does not
+   overflow.  */
+
+static inline int
+check_mul (int x, int y)
+{
+  if (x >= 0)
+    {
+      if (y >= 0)
+       return check_pos_mul (x, y);
+      else
+       return -check_pos_mul (x, -y);
+    }
+  else if (y >= 0)
+    return -check_pos_mul (-x, y);
+  else
+    return check_pos_mul (-x, -y);
+}
+
+/* Test whether equation E is red.  */
+
+static inline bool
+omega_eqn_is_red (eqn e, int desired_res)
+{
+  return (desired_res == omega_simplify && e->color == omega_red);
+}
+
+/* Return a string for VARIABLE.  */
+
+static inline char *
+omega_var_to_str (int variable)
+{
+  if (0 <= variable && variable <= 20)
+    return wild_name[variable];
+
+  if (-20 < variable && variable < 0)
+    return wild_name[40 + variable];
+
+  /* Collapse all the entries that would have overflowed.  */
+  return wild_name[21];
+}
+
+/* Return a string for variable I in problem PB.  */
+
+static inline char *
+omega_variable_to_str (omega_pb pb, int i)
+{
+  return omega_var_to_str (pb->var[i]);
+}
+
+/* Do nothing function: used for default initializations.  */
+
+void
+omega_no_procedure (omega_pb pb ATTRIBUTE_UNUSED)
+{
+}
+
+void (*omega_when_reduced) (omega_pb) = omega_no_procedure;
+
+/* Compute the greatest common divisor of A and B.  */
+
+static inline int
+gcd (int b, int a)
+{
+  if (b == 1)
+    return 1;
+
+  while (b != 0)
+    {
+      int t = b;
+      b = a % b;
+      a = t;
+    }
+
+  return a;
+}
+
+/* Print to FILE from PB equation E with all its coefficients
+   multiplied by C.  */
+
+static void
+omega_print_term (FILE *file, omega_pb pb, eqn e, int c)
+{
+  int i;
+  bool first = true;
+  int n = pb->num_vars;
+  int went_first = -1;
+
+  for (i = 1; i <= n; i++)
+    if (c * e->coef[i] > 0)
+      {
+       first = false;
+       went_first = i;
+
+       if (c * e->coef[i] == 1)
+         fprintf (file, "%s", omega_variable_to_str (pb, i));
+       else
+         fprintf (file, "%d * %s", c * e->coef[i],
+                  omega_variable_to_str (pb, i));
+       break;
+      }
+
+  for (i = 1; i <= n; i++)
+    if (i != went_first && c * e->coef[i] != 0)
+      {
+       if (!first && c * e->coef[i] > 0)
+         fprintf (file, " + ");
+
+       first = false;
+
+       if (c * e->coef[i] == 1)
+         fprintf (file, "%s", omega_variable_to_str (pb, i));
+       else if (c * e->coef[i] == -1)
+         fprintf (file, " - %s", omega_variable_to_str (pb, i));
+       else
+         fprintf (file, "%d * %s", c * e->coef[i],
+                  omega_variable_to_str (pb, i));
+      }
+
+  if (!first && c * e->coef[0] > 0)
+    fprintf (file, " + ");
+
+  if (first || c * e->coef[0] != 0)
+    fprintf (file, "%d", c * e->coef[0]);
+}
+
+/* Print to FILE the equation E of problem PB.  */
+
+void
+omega_print_eqn (FILE *file, omega_pb pb, eqn e, bool test, int extra)
+{
+  int i;
+  int n = pb->num_vars + extra;
+  bool is_lt = test && e->coef[0] == -1;
+  bool first;
+
+  if (test)
+    {
+      if (e->touched)
+       fprintf (file, "!");
+
+      else if (e->key != 0)
+       fprintf (file, "%d: ", e->key);
+    }
+
+  if (e->color == omega_red)
+    fprintf (file, "[");
+
+  first = true;
+
+  for (i = is_lt ? 1 : 0; i <= n; i++)
+    if (e->coef[i] < 0)
+      {
+       if (!first)
+         fprintf (file, " + ");
+       else
+         first = false;
+
+       if (i == 0)
+         fprintf (file, "%d", -e->coef[i]);
+       else if (e->coef[i] == -1)
+         fprintf (file, "%s", omega_variable_to_str (pb, i));
+       else
+         fprintf (file, "%d * %s", -e->coef[i],
+                  omega_variable_to_str (pb, i));
+      }
+
+  if (first)
+    {
+      if (is_lt)
+       {
+         fprintf (file, "1");
+         is_lt = false;
+       }
+      else
+       fprintf (file, "0");
+    }
+
+  if (test == 0)
+    fprintf (file, " = ");
+  else if (is_lt)
+    fprintf (file, " < ");
+  else
+    fprintf (file, " <= ");
+
+  first = true;
+
+  for (i = 0; i <= n; i++)
+    if (e->coef[i] > 0)
+      {
+       if (!first)
+         fprintf (file, " + ");
+       else
+         first = false;
+
+       if (i == 0)
+         fprintf (file, "%d", e->coef[i]);
+       else if (e->coef[i] == 1)
+         fprintf (file, "%s", omega_variable_to_str (pb, i));
+       else
+         fprintf (file, "%d * %s", e->coef[i],
+                  omega_variable_to_str (pb, i));
+      }
+
+  if (first)
+    fprintf (file, "0");
+
+  if (e->color == omega_red)
+    fprintf (file, "]");
+}
+
+/* Print to FILE all the variables of problem PB.  */
+
+static void
+omega_print_vars (FILE *file, omega_pb pb)
+{
+  int i;
+
+  fprintf (file, "variables = ");
+
+  if (pb->safe_vars > 0)
+    fprintf (file, "protected (");
+
+  for (i = 1; i <= pb->num_vars; i++)
+    {
+      fprintf (file, "%s", omega_variable_to_str (pb, i));
+
+      if (i == pb->safe_vars)
+       fprintf (file, ")");
+
+      if (i < pb->num_vars)
+       fprintf (file, ", ");
+    }
+
+  fprintf (file, "\n");
+}
+
+/* Debug problem PB.  */
+
+void
+debug_omega_problem (omega_pb pb)
+{
+  omega_print_problem (stderr, pb);
+}
+
+/* Print to FILE problem PB.  */
+
+void
+omega_print_problem (FILE *file, omega_pb pb)
+{
+  int e;
+
+  if (!pb->variables_initialized)
+    omega_initialize_variables (pb);
+
+  omega_print_vars (file, pb);
+
+  for (e = 0; e < pb->num_eqs; e++)
+    {
+      omega_print_eq (file, pb, &pb->eqs[e]);
+      fprintf (file, "\n");
+    }
+
+  fprintf (file, "Done with EQ\n");
+
+  for (e = 0; e < pb->num_geqs; e++)
+    {
+      omega_print_geq (file, pb, &pb->geqs[e]);
+      fprintf (file, "\n");
+    }
+
+  fprintf (file, "Done with GEQ\n");
+
+  for (e = 0; e < pb->num_subs; e++)
+    {
+      eqn eq = &pb->subs[e];
+
+      if (eq->color == omega_red)
+       fprintf (file, "[");
+
+      if (eq->key > 0)
+       fprintf (file, "%s := ", omega_var_to_str (eq->key));
+      else
+       fprintf (file, "#%d := ", eq->key);
+
+      omega_print_term (file, pb, eq, 1);
+
+      if (eq->color == omega_red)
+       fprintf (file, "]");
+
+      fprintf (file, "\n");
+    }
+}
+
+/* Return the number of equations in PB tagged omega_red.  */
+
+int
+omega_count_red_equations (omega_pb pb)
+{
+  int e, i;
+  int result = 0;
+
+  for (e = 0; e < pb->num_eqs; e++)
+    if (pb->eqs[e].color == omega_red)
+      {
+       for (i = pb->num_vars; i > 0; i--)
+         if (pb->geqs[e].coef[i])
+           break;
+
+       if (i == 0 && pb->geqs[e].coef[0] == 1)
+         return 0;
+       else
+         result += 2;
+      }
+
+  for (e = 0; e < pb->num_geqs; e++)
+    if (pb->geqs[e].color == omega_red)
+      result += 1;
+
+  for (e = 0; e < pb->num_subs; e++)
+    if (pb->subs[e].color == omega_red)
+      result += 2;
+
+  return result;
+}
+
+/* Print to FILE all the equations in PB that are tagged omega_red.  */
+
+void
+omega_print_red_equations (FILE *file, omega_pb pb)
+{
+  int e;
+
+  if (!pb->variables_initialized)
+    omega_initialize_variables (pb);
+
+  omega_print_vars (file, pb);
+
+  for (e = 0; e < pb->num_eqs; e++)
+    if (pb->eqs[e].color == omega_red)
+      {
+       omega_print_eq (file, pb, &pb->eqs[e]);
+       fprintf (file, "\n");
+      }
+
+  for (e = 0; e < pb->num_geqs; e++)
+    if (pb->geqs[e].color == omega_red)
+      {
+       omega_print_geq (file, pb, &pb->geqs[e]);
+       fprintf (file, "\n");
+      }
+
+  for (e = 0; e < pb->num_subs; e++)
+    if (pb->subs[e].color == omega_red)
+      {
+       eqn eq = &pb->subs[e];
+       fprintf (file, "[");
+
+       if (eq->key > 0)
+         fprintf (file, "%s := ", omega_var_to_str (eq->key));
+       else
+         fprintf (file, "#%d := ", eq->key);
+
+       omega_print_term (file, pb, eq, 1);
+       fprintf (file, "]\n");
+      }
+}
+
+/* Pretty print PB to FILE.  */
+
+void
+omega_pretty_print_problem (FILE *file, omega_pb pb)
+{
+  int e, v, v1, v2, v3, t;
+  bool *live = XNEWVEC (bool, OMEGA_MAX_GEQS);
+  int stuffPrinted = 0;
+  bool change;
+
+  typedef enum {
+    none, le, lt
+  } partial_order_type;
+
+  partial_order_type **po = XNEWVEC (partial_order_type *, 
+                                    OMEGA_MAX_VARS * OMEGA_MAX_VARS);
+  int **po_eq = XNEWVEC (int *, OMEGA_MAX_VARS * OMEGA_MAX_VARS);
+  int *last_links = XNEWVEC (int, OMEGA_MAX_VARS);
+  int *first_links = XNEWVEC (int, OMEGA_MAX_VARS);
+  int *chain_length = XNEWVEC (int, OMEGA_MAX_VARS);
+  int *chain = XNEWVEC (int, OMEGA_MAX_VARS);
+  int i, m;
+  bool multiprint;
+
+  if (!pb->variables_initialized)
+    omega_initialize_variables (pb);
+
+  if (pb->num_vars > 0)
+    {
+      omega_eliminate_redundant (pb, false);
+
+      for (e = 0; e < pb->num_eqs; e++)
+       {
+         if (stuffPrinted)
+           fprintf (file, "; ");
+
+         stuffPrinted = 1;
+         omega_print_eq (file, pb, &pb->eqs[e]);
+       }
+
+      for (e = 0; e < pb->num_geqs; e++)
+       live[e] = true;
+
+      while (1)
+       {
+         for (v = 1; v <= pb->num_vars; v++)
+           {
+             last_links[v] = first_links[v] = 0;
+             chain_length[v] = 0;
+
+             for (v2 = 1; v2 <= pb->num_vars; v2++)
+               po[v][v2] = none;
+           }
+
+         for (e = 0; e < pb->num_geqs; e++)
+           if (live[e])
+             {
+               for (v = 1; v <= pb->num_vars; v++)
+                 if (pb->geqs[e].coef[v] == 1)
+                   first_links[v]++;
+                 else if (pb->geqs[e].coef[v] == -1)
+                   last_links[v]++;
+
+               v1 = pb->num_vars;
+
+               while (v1 > 0 && pb->geqs[e].coef[v1] == 0)
+                 v1--;
+
+               v2 = v1 - 1;
+
+               while (v2 > 0 && pb->geqs[e].coef[v2] == 0)
+                 v2--;
+
+               v3 = v2 - 1;
+
+               while (v3 > 0 && pb->geqs[e].coef[v3] == 0)
+                 v3--;
+
+               if (pb->geqs[e].coef[0] > 0 || pb->geqs[e].coef[0] < -1
+                   || v2 <= 0 || v3 > 0
+                   || pb->geqs[e].coef[v1] * pb->geqs[e].coef[v2] != -1)
+                 {
+                   /* Not a partial order relation.  */
+                 }
+               else
+                 {
+                   if (pb->geqs[e].coef[v1] == 1)
+                     {
+                       v3 = v2;
+                       v2 = v1;
+                       v1 = v3;
+                     }
+
+                   /* Relation is v1 <= v2 or v1 < v2.  */
+                   po[v1][v2] = ((pb->geqs[e].coef[0] == 0) ? le : lt);
+                   po_eq[v1][v2] = e;
+                 }
+             }
+         for (v = 1; v <= pb->num_vars; v++)
+           chain_length[v] = last_links[v];
+
+         /* Just in case pb->num_vars <= 0.  */
+         change = false;
+         for (t = 0; t < pb->num_vars; t++)
+           {
+             change = false;
+
+             for (v1 = 1; v1 <= pb->num_vars; v1++)
+               for (v2 = 1; v2 <= pb->num_vars; v2++)
+                 if (po[v1][v2] != none &&
+                     chain_length[v1] <= chain_length[v2])
+                   {
+                     chain_length[v1] = chain_length[v2] + 1;
+                     change = true;
+                   }
+           }
+
+         /* Caught in cycle.  */
+         gcc_assert (!change);
+
+         for (v1 = 1; v1 <= pb->num_vars; v1++)
+           if (chain_length[v1] == 0)
+             first_links[v1] = 0;
+
+         v = 1;
+
+         for (v1 = 2; v1 <= pb->num_vars; v1++)
+           if (chain_length[v1] + first_links[v1] >
+               chain_length[v] + first_links[v])
+             v = v1;
+
+         if (chain_length[v] + first_links[v] == 0)
+           break;
+
+         if (stuffPrinted)
+           fprintf (file, "; ");
+
+         stuffPrinted = 1;
+
+         /* Chain starts at v. */
+         {
+           int tmp;
+           bool first = true;
+
+           for (e = 0; e < pb->num_geqs; e++)
+             if (live[e] && pb->geqs[e].coef[v] == 1)
+               {
+                 if (!first)
+                   fprintf (file, ", ");
+
+                 tmp = pb->geqs[e].coef[v];
+                 pb->geqs[e].coef[v] = 0;
+                 omega_print_term (file, pb, &pb->geqs[e], -1);
+                 pb->geqs[e].coef[v] = tmp;
+                 live[e] = false;
+                 first = false;
+               }
+
+           if (!first)
+             fprintf (file, " <= ");
+         }
+
+         /* Find chain.  */
+         chain[0] = v;
+         m = 1;
+         while (1)
+           {
+             /* Print chain.  */
+             for (v2 = 1; v2 <= pb->num_vars; v2++)
+               if (po[v][v2] && chain_length[v] == 1 + chain_length[v2])
+                 break;
+
+             if (v2 > pb->num_vars)
+               break;
+
+             chain[m++] = v2;
+             v = v2;
+           }
+
+         fprintf (file, "%s", omega_variable_to_str (pb, chain[0]));
+         
+         for (multiprint = false, i = 1; i < m; i++)
+           {
+             v = chain[i - 1];
+             v2 = chain[i];
+
+             if (po[v][v2] == le)
+               fprintf (file, " <= ");
+             else
+               fprintf (file, " < ");
+
+             fprintf (file, "%s", omega_variable_to_str (pb, v2));
+             live[po_eq[v][v2]] = false;
+
+             if (!multiprint && i < m - 1)
+               for (v3 = 1; v3 <= pb->num_vars; v3++)
+                 {
+                   if (v == v3 || v2 == v3
+                       || po[v][v2] != po[v][v3]
+                       || po[v2][chain[i + 1]] != po[v3][chain[i + 1]])
+                     continue;
+
+                   fprintf (file, ",%s", omega_variable_to_str (pb, v3));
+                   live[po_eq[v][v3]] = false;
+                   live[po_eq[v3][chain[i + 1]]] = false;
+                   multiprint = true;
+                 }
+             else
+               multiprint = false;
+           }
+
+         v = chain[m - 1];
+         /* Print last_links.  */
+         {
+           int tmp;
+           bool first = true;
+
+           for (e = 0; e < pb->num_geqs; e++)
+             if (live[e] && pb->geqs[e].coef[v] == -1)
+               {
+                 if (!first)
+                   fprintf (file, ", ");
+                 else
+                   fprintf (file, " <= ");
+
+                 tmp = pb->geqs[e].coef[v];
+                 pb->geqs[e].coef[v] = 0;
+                 omega_print_term (file, pb, &pb->geqs[e], 1);
+                 pb->geqs[e].coef[v] = tmp;
+                 live[e] = false;
+                 first = false;
+               }
+         }
+       }
+
+      for (e = 0; e < pb->num_geqs; e++)
+       if (live[e])
+         {
+           if (stuffPrinted)
+             fprintf (file, "; ");
+           stuffPrinted = 1;
+           omega_print_geq (file, pb, &pb->geqs[e]);
+         }
+
+      for (e = 0; e < pb->num_subs; e++)
+       {
+         eqn eq = &pb->subs[e];
+
+         if (stuffPrinted)
+           fprintf (file, "; ");
+
+         stuffPrinted = 1;
+
+         if (eq->key > 0)
+           fprintf (file, "%s := ", omega_var_to_str (eq->key));
+         else
+           fprintf (file, "#%d := ", eq->key);
+
+         omega_print_term (file, pb, eq, 1);
+       }
+    }
+
+  free (live);
+  free (po);
+  free (po_eq);
+  free (last_links);
+  free (first_links);
+  free (chain_length);
+  free (chain);
+}
+
+/* Assign to variable I in PB the next wildcard name.  The name of a
+   wildcard is a negative number.  */
+static int next_wild_card = 0;
+
+static void
+omega_name_wild_card (omega_pb pb, int i)
+{
+  --next_wild_card;
+  if (next_wild_card < -PARAM_VALUE (PARAM_OMEGA_MAX_WILD_CARDS))
+    next_wild_card = -1;
+  pb->var[i] = next_wild_card;
+}
+
+/* Return the index of the last protected (or safe) variable in PB,
+   after having added a new wildcard variable.  */
+
+static int
+omega_add_new_wild_card (omega_pb pb)
+{
+  int e;
+  int i = ++pb->safe_vars;
+  pb->num_vars++;
+
+  /* Make a free place in the protected (safe) variables, by moving
+     the non protected variable pointed by "I" at the end, ie. at
+     offset pb->num_vars.  */
+  if (pb->num_vars != i)
+    {
+      /* Move "I" for all the inequalities.  */
+      for (e = pb->num_geqs - 1; e >= 0; e--)
+       {
+         if (pb->geqs[e].coef[i])
+           pb->geqs[e].touched = 1;
+
+         pb->geqs[e].coef[pb->num_vars] = pb->geqs[e].coef[i];
+       }
+
+      /* Move "I" for all the equalities.  */
+      for (e = pb->num_eqs - 1; e >= 0; e--)
+       pb->eqs[e].coef[pb->num_vars] = pb->eqs[e].coef[i];
+
+      /* Move "I" for all the substitutions.  */
+      for (e = pb->num_subs - 1; e >= 0; e--)
+       pb->subs[e].coef[pb->num_vars] = pb->subs[e].coef[i];
+
+      /* Move the identifier.  */
+      pb->var[pb->num_vars] = pb->var[i];
+    }
+
+  /* Initialize at zero all the coefficients  */
+  for (e = pb->num_geqs - 1; e >= 0; e--)
+    pb->geqs[e].coef[i] = 0;
+
+  for (e = pb->num_eqs - 1; e >= 0; e--)
+    pb->eqs[e].coef[i] = 0;
+
+  for (e = pb->num_subs - 1; e >= 0; e--)
+    pb->subs[e].coef[i] = 0;
+
+  /* And give it a name.  */
+  omega_name_wild_card (pb, i);
+  return i;
+}
+
+/* Delete inequality E from problem PB that has N_VARS variables.  */
+
+static void
+omega_delete_geq (omega_pb pb, int e, int n_vars)
+{
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    {
+      fprintf (dump_file, "Deleting %d (last:%d): ", e, pb->num_geqs - 1);
+      omega_print_geq (dump_file, pb, &pb->geqs[e]);
+      fprintf (dump_file, "\n");
+    }
+
+  if (e < pb->num_geqs - 1)
+    omega_copy_eqn (&pb->geqs[e], &pb->geqs[pb->num_geqs - 1], n_vars);
+
+  pb->num_geqs--;
+}
+
+/* Delete extra inequality E from problem PB that has N_VARS
+   variables.  */
+
+static void
+omega_delete_geq_extra (omega_pb pb, int e, int n_vars)
+{
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    {
+      fprintf (dump_file, "Deleting %d: ",e);
+      omega_print_geq_extra (dump_file, pb, &pb->geqs[e]);
+      fprintf (dump_file, "\n");
+    }
+
+  if (e < pb->num_geqs - 1)
+    omega_copy_eqn (&pb->geqs[e], &pb->geqs[pb->num_geqs - 1], n_vars);
+
+  pb->num_geqs--;
+}
+
+
+/* Remove variable I from problem PB.  */
+
+static void
+omega_delete_variable (omega_pb pb, int i)
+{
+  int n_vars = pb->num_vars;
+  int e;
+
+  if (omega_safe_var_p (pb, i))
+    {
+      int j = pb->safe_vars;
+
+      for (e = pb->num_geqs - 1; e >= 0; e--)
+       {
+         pb->geqs[e].touched = 1;
+         pb->geqs[e].coef[i] = pb->geqs[e].coef[j];
+         pb->geqs[e].coef[j] = pb->geqs[e].coef[n_vars];
+       }
+
+      for (e = pb->num_eqs - 1; e >= 0; e--)
+       {
+         pb->eqs[e].coef[i] = pb->eqs[e].coef[j];
+         pb->eqs[e].coef[j] = pb->eqs[e].coef[n_vars];
+       }
+
+      for (e = pb->num_subs - 1; e >= 0; e--)
+       {
+         pb->subs[e].coef[i] = pb->subs[e].coef[j];
+         pb->subs[e].coef[j] = pb->subs[e].coef[n_vars];
+       }
+
+      pb->var[i] = pb->var[j];
+      pb->var[j] = pb->var[n_vars];
+    }
+  else if (i < n_vars)
+    {
+      for (e = pb->num_geqs - 1; e >= 0; e--)
+       if (pb->geqs[e].coef[n_vars])
+         {
+           pb->geqs[e].coef[i] = pb->geqs[e].coef[n_vars];
+           pb->geqs[e].touched = 1;
+         }
+
+      for (e = pb->num_eqs - 1; e >= 0; e--)
+       pb->eqs[e].coef[i] = pb->eqs[e].coef[n_vars];
+
+      for (e = pb->num_subs - 1; e >= 0; e--)
+       pb->subs[e].coef[i] = pb->subs[e].coef[n_vars];
+
+      pb->var[i] = pb->var[n_vars];
+    }
+
+  if (omega_safe_var_p (pb, i))
+    pb->safe_vars--;
+
+  pb->num_vars--;
+}
+
+/* Because the coefficients of an equation are sparse, PACKING records
+   indices for non null coefficients.  */
+static int *packing;
+
+/* Set up the coefficients of PACKING, following the coefficients of
+   equation EQN that has NUM_VARS variables.  */
+
+static inline int
+setup_packing (eqn eqn, int num_vars)
+{
+  int k;
+  int n = 0;
+
+  for (k = num_vars; k >= 0; k--)
+    if (eqn->coef[k])
+      packing[n++] = k;
+
+  return n;
+}
+
+/* Computes a linear combination of EQ and SUB at VAR with coefficient
+   C, such that EQ->coef[VAR] is set to 0.  TOP_VAR is the number of
+   non null indices of SUB stored in PACKING.  */
+
+static inline void
+omega_substitute_red_1 (eqn eq, eqn sub, int var, int c, bool *found_black,
+                       int top_var)
+{
+  if (eq->coef[var] != 0)
+    {
+      if (eq->color == omega_black)
+       *found_black = true;
+      else
+       {
+         int j, k = eq->coef[var];
+
+         eq->coef[var] = 0;
+
+         for (j = top_var; j >= 0; j--)
+           eq->coef[packing[j]] -= sub->coef[packing[j]] * k * c;
+       }
+    }
+}
+
+/* Substitute in PB variable VAR with "C * SUB".  */
+
+static void
+omega_substitute_red (omega_pb pb, eqn sub, int var, int c, bool *found_black)
+{
+  int e, top_var = setup_packing (sub, pb->num_vars);
+
+  *found_black = false;
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    {
+      if (sub->color == omega_red)
+       fprintf (dump_file, "[");
+
+      fprintf (dump_file, "substituting using %s := ",
+              omega_variable_to_str (pb, var));
+      omega_print_term (dump_file, pb, sub, -c);
+
+      if (sub->color == omega_red)
+       fprintf (dump_file, "]");
+
+      fprintf (dump_file, "\n");
+      omega_print_vars (dump_file, pb);
+    }
+
+  for (e = pb->num_eqs - 1; e >= 0; e--)
+    {
+      eqn eqn = &(pb->eqs[e]);
+
+      omega_substitute_red_1 (eqn, sub, var, c, found_black, top_var);
+
+      if (dump_file && (dump_flags & TDF_DETAILS))
+       {
+         omega_print_eq (dump_file, pb, eqn);
+         fprintf (dump_file, "\n");
+       }
+    }
+
+  for (e = pb->num_geqs - 1; e >= 0; e--)
+    {
+      eqn eqn = &(pb->geqs[e]);
+
+      omega_substitute_red_1 (eqn, sub, var, c, found_black, top_var);
+
+      if (eqn->coef[var] && eqn->color == omega_red)
+       eqn->touched = 1;
+
+      if (dump_file && (dump_flags & TDF_DETAILS))
+       {
+         omega_print_geq (dump_file, pb, eqn);
+         fprintf (dump_file, "\n");
+       }
+    }
+
+  for (e = pb->num_subs - 1; e >= 0; e--)
+    {
+      eqn eqn = &(pb->subs[e]);
+
+      omega_substitute_red_1 (eqn, sub, var, c, found_black, top_var);
+
+      if (dump_file && (dump_flags & TDF_DETAILS))
+       {
+         fprintf (dump_file, "%s := ", omega_var_to_str (eqn->key));
+         omega_print_term (dump_file, pb, eqn, 1);
+         fprintf (dump_file, "\n");
+       }
+    }
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    fprintf (dump_file, "---\n\n");
+
+  if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
+    *found_black = true;
+}
+
+/* Substitute in PB variable VAR with "C * SUB".  */
+
+static void
+omega_substitute (omega_pb pb, eqn sub, int var, int c)
+{
+  int e, j, j0;
+  int top_var = setup_packing (sub, pb->num_vars);
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    {
+      fprintf (dump_file, "substituting using %s := ",
+              omega_variable_to_str (pb, var));
+      omega_print_term (dump_file, pb, sub, -c);
+      fprintf (dump_file, "\n");
+      omega_print_vars (dump_file, pb);
+    }
+
+  if (top_var < 0)
+    {
+      for (e = pb->num_eqs - 1; e >= 0; e--)
+       pb->eqs[e].coef[var] = 0;
+
+      for (e = pb->num_geqs - 1; e >= 0; e--)
+       if (pb->geqs[e].coef[var] != 0)
+         {
+           pb->geqs[e].touched = 1;
+           pb->geqs[e].coef[var] = 0;
+         }
+
+      for (e = pb->num_subs - 1; e >= 0; e--)
+       pb->subs[e].coef[var] = 0;
+
+      if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
+       {
+         int k;
+         eqn eqn = &(pb->subs[pb->num_subs++]);
+
+         for (k = pb->num_vars; k >= 0; k--)
+           eqn->coef[k] = 0;
+
+         eqn->key = pb->var[var];
+         eqn->color = omega_black;
+       }
+    }
+  else if (top_var == 0 && packing[0] == 0)
+    {
+      c = -sub->coef[0] * c;
+
+      for (e = pb->num_eqs - 1; e >= 0; e--)
+       {
+         pb->eqs[e].coef[0] += pb->eqs[e].coef[var] * c;
+         pb->eqs[e].coef[var] = 0;
+       }
+
+      for (e = pb->num_geqs - 1; e >= 0; e--)
+       if (pb->geqs[e].coef[var] != 0)
+         {
+           pb->geqs[e].coef[0] += pb->geqs[e].coef[var] * c;
+           pb->geqs[e].coef[var] = 0;
+           pb->geqs[e].touched = 1;
+         }
+
+      for (e = pb->num_subs - 1; e >= 0; e--)
+       {
+         pb->subs[e].coef[0] += pb->subs[e].coef[var] * c;
+         pb->subs[e].coef[var] = 0;
+       }
+
+      if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
+       {
+         int k;
+         eqn eqn = &(pb->subs[pb->num_subs++]);
+
+         for (k = pb->num_vars; k >= 1; k--)
+           eqn->coef[k] = 0;
+
+         eqn->coef[0] = c;
+         eqn->key = pb->var[var];
+         eqn->color = omega_black;
+       }
+
+      if (dump_file && (dump_flags & TDF_DETAILS))
+       {
+         fprintf (dump_file, "---\n\n");
+         omega_print_problem (dump_file, pb);
+         fprintf (dump_file, "===\n\n");
+       }
+    }
+  else
+    {
+      for (e = pb->num_eqs - 1; e >= 0; e--)
+       {
+         eqn eqn = &(pb->eqs[e]);
+         int k = eqn->coef[var];
+
+         if (k != 0)
+           {
+             k = c * k;
+             eqn->coef[var] = 0;
+
+             for (j = top_var; j >= 0; j--)
+               {
+                 j0 = packing[j];
+                 eqn->coef[j0] -= sub->coef[j0] * k;
+               }
+           }
+
+         if (dump_file && (dump_flags & TDF_DETAILS))
+           {
+             omega_print_eq (dump_file, pb, eqn);
+             fprintf (dump_file, "\n");
+           }
+       }
+
+      for (e = pb->num_geqs - 1; e >= 0; e--)
+       {
+         eqn eqn = &(pb->geqs[e]);
+         int k = eqn->coef[var];
+
+         if (k != 0)
+           {
+             k = c * k;
+             eqn->touched = 1;
+             eqn->coef[var] = 0;
+
+             for (j = top_var; j >= 0; j--)
+               {
+                 j0 = packing[j];
+                 eqn->coef[j0] -= sub->coef[j0] * k;
+               }
+           }
+
+         if (dump_file && (dump_flags & TDF_DETAILS))
+           {
+             omega_print_geq (dump_file, pb, eqn);
+             fprintf (dump_file, "\n");
+           }
+       }
+
+      for (e = pb->num_subs - 1; e >= 0; e--)
+       {
+         eqn eqn = &(pb->subs[e]);
+         int k = eqn->coef[var];
+
+         if (k != 0)
+           {
+             k = c * k;
+             eqn->coef[var] = 0;
+
+             for (j = top_var; j >= 0; j--)
+               {
+                 j0 = packing[j];
+                 eqn->coef[j0] -= sub->coef[j0] * k;
+               }
+           }
+
+         if (dump_file && (dump_flags & TDF_DETAILS))
+           {
+             fprintf (dump_file, "%s := ", omega_var_to_str (eqn->key));
+             omega_print_term (dump_file, pb, eqn, 1);
+             fprintf (dump_file, "\n");
+           }
+       }
+
+      if (dump_file && (dump_flags & TDF_DETAILS))
+       {
+         fprintf (dump_file, "---\n\n");
+         omega_print_problem (dump_file, pb);
+         fprintf (dump_file, "===\n\n");
+       }
+
+      if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
+       {
+         int k;
+         eqn eqn = &(pb->subs[pb->num_subs++]);
+         c = -c;
+
+         for (k = pb->num_vars; k >= 0; k--)
+           eqn->coef[k] = c * (sub->coef[k]);
+
+         eqn->key = pb->var[var];
+         eqn->color = sub->color;
+       }
+    }
+}
+
+/* Solve e = factor alpha for x_j and substitute.  */
+
+static void
+omega_do_mod (omega_pb pb, int factor, int e, int j)
+{
+  int k, i;
+  eqn eq = omega_alloc_eqns (0, 1);
+  int nfactor;
+  bool kill_j = false;
+
+  omega_copy_eqn (eq, &pb->eqs[e], pb->num_vars);
+
+  for (k = pb->num_vars; k >= 0; k--)
+    {
+      eq->coef[k] = int_mod (eq->coef[k], factor);
+
+      if (2 * eq->coef[k] >= factor)
+       eq->coef[k] -= factor;
+    }
+
+  nfactor = eq->coef[j];
+
+  if (omega_safe_var_p (pb, j) && !omega_wildcard_p (pb, j))
+    {
+      i = omega_add_new_wild_card (pb);
+      eq->coef[pb->num_vars] = eq->coef[i];
+      eq->coef[j] = 0;
+      eq->coef[i] = -factor;
+      kill_j = true;
+    }
+  else
+    {
+      eq->coef[j] = -factor;
+      if (!omega_wildcard_p (pb, j))
+       omega_name_wild_card (pb, j);
+    }
+
+  omega_substitute (pb, eq, j, nfactor);
+
+  for (k = pb->num_vars; k >= 0; k--)
+    pb->eqs[e].coef[k] = pb->eqs[e].coef[k] / factor;
+
+  if (kill_j)
+    omega_delete_variable (pb, j);
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    {
+      fprintf (dump_file, "Mod-ing and normalizing produces:\n");
+      omega_print_problem (dump_file, pb);
+    }
+
+  omega_free_eqns (eq, 1);
+}
+
+/* Multiplies by -1 inequality E.  */
+
+void
+omega_negate_geq (omega_pb pb, int e)
+{
+  int i;
+
+  for (i = pb->num_vars; i >= 0; i--)
+    pb->geqs[e].coef[i] *= -1;
+
+  pb->geqs[e].coef[0]--;
+  pb->geqs[e].touched = 1;
+}
+
+/* Returns OMEGA_TRUE when problem PB has a solution.  */
+
+static enum omega_result
+verify_omega_pb (omega_pb pb)
+{
+  enum omega_result result;
+  int e;
+  bool any_color = false;
+  omega_pb tmp_problem = XNEW (struct omega_pb);
+
+  omega_copy_problem (tmp_problem, pb);
+  tmp_problem->safe_vars = 0;
+  tmp_problem->num_subs = 0;
+  
+  for (e = pb->num_geqs - 1; e >= 0; e--)
+    if (pb->geqs[e].color == omega_red)
+      {
+       any_color = true;
+       break;
+      }
+
+  if (please_no_equalities_in_simplified_problems)
+    any_color = true;
+
+  if (any_color)
+    original_problem = no_problem;
+  else
+    original_problem = pb;
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    {
+      fprintf (dump_file, "verifying problem");
+
+      if (any_color)
+       fprintf (dump_file, " (color mode)");
+
+      fprintf (dump_file, " :\n");
+      omega_print_problem (dump_file, pb);
+    }
+
+  result = omega_solve_problem (tmp_problem, omega_unknown);
+  original_problem = no_problem;
+  free (tmp_problem);
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    {
+      if (result != omega_false)
+       fprintf (dump_file, "verified problem\n");
+      else
+       fprintf (dump_file, "disproved problem\n");
+      omega_print_problem (dump_file, pb);
+    }
+
+  return result;
+}
+
+/* Add a new equality to problem PB at last position E.  */
+
+static void
+adding_equality_constraint (omega_pb pb, int e)
+{
+  if (original_problem != no_problem 
+      && original_problem != pb
+      && !conservative)
+    {
+      int i, j;
+      int e2 = original_problem->num_eqs++;
+
+      if (dump_file && (dump_flags & TDF_DETAILS))
+       fprintf (dump_file,
+                "adding equality constraint %d to outer problem\n", e2);
+      omega_init_eqn_zero (&original_problem->eqs[e2],
+                          original_problem->num_vars);
+
+      for (i = pb->num_vars; i >= 1; i--)
+       {
+         for (j = original_problem->num_vars; j >= 1; j--)
+           if (original_problem->var[j] == pb->var[i])
+             break;
+
+         if (j <= 0)
+           {
+             if (dump_file && (dump_flags & TDF_DETAILS))
+               fprintf (dump_file, "retracting\n");
+             original_problem->num_eqs--;
+             return;
+           }
+         original_problem->eqs[e2].coef[j] = pb->eqs[e].coef[i];
+       }
+
+      original_problem->eqs[e2].coef[0] = pb->eqs[e].coef[0];
+
+      if (dump_file && (dump_flags & TDF_DETAILS))
+       omega_print_problem (dump_file, original_problem);
+    }
+}
+
+static int *fast_lookup;
+static int *fast_lookup_red;
+
+typedef enum {
+  normalize_false,
+  normalize_uncoupled,
+  normalize_coupled
+} normalize_return_type;
+
+/* Normalizes PB by removing redundant constraints.  Returns
+   normalize_false when the constraints system has no solution,
+   otherwise returns normalize_coupled or normalize_uncoupled.  */
+
+static normalize_return_type
+normalize_omega_problem (omega_pb pb)
+{
+  int e, i, j, k, n_vars;
+  int coupled_subscripts = 0;
+
+  n_vars = pb->num_vars;
+
+  for (e = 0; e < pb->num_geqs; e++)
+    {
+      if (!pb->geqs[e].touched)
+       {
+         if (!single_var_geq (&pb->geqs[e], n_vars))
+           coupled_subscripts = 1;
+       }
+      else
+       {
+         int g, top_var, i0, hashCode;
+         int *p = &packing[0];
+
+         for (k = 1; k <= n_vars; k++)
+           if (pb->geqs[e].coef[k])
+             *(p++) = k;
+
+         top_var = (p - &packing[0]) - 1;
+
+         if (top_var == -1)
+           {
+             if (pb->geqs[e].coef[0] < 0)
+               {
+                 if (dump_file && (dump_flags & TDF_DETAILS))
+                   {
+                     omega_print_geq (dump_file, pb, &pb->geqs[e]);
+                     fprintf (dump_file, "\nequations have no solution \n");
+                   }
+                 return normalize_false;
+               }
+
+             omega_delete_geq (pb, e, n_vars);
+             e--;
+             continue;
+           }
+         else if (top_var == 0)
+           {
+             int singlevar = packing[0];
+
+             g = pb->geqs[e].coef[singlevar];
+
+             if (g > 0)
+               {
+                 pb->geqs[e].coef[singlevar] = 1;
+                 pb->geqs[e].key = singlevar;
+               }
+             else
+               {
+                 g = -g;
+                 pb->geqs[e].coef[singlevar] = -1;
+                 pb->geqs[e].key = -singlevar;
+               }
+
+             if (g > 1)
+               pb->geqs[e].coef[0] = int_div (pb->geqs[e].coef[0], g);
+           }
+         else
+           {
+             int g2;
+             int hash_key_multiplier = 31;
+
+             coupled_subscripts = 1;
+             i0 = top_var;
+             i = packing[i0--];
+             g = pb->geqs[e].coef[i];
+             hashCode = g * (i + 3);
+
+             if (g < 0)
+               g = -g;
+
+             for (; i0 >= 0; i0--)
+               {
+                 int x;
+
+                 i = packing[i0];
+                 x = pb->geqs[e].coef[i];
+                 hashCode = hashCode * hash_key_multiplier * (i + 3) + x;
+
+                 if (x < 0)
+                   x = -x;
+
+                 if (x == 1)
+                   {
+                     g = 1;
+                     i0--;
+                     break;
+                   }
+                 else
+                   g = gcd (x, g);
+               }
+
+             for (; i0 >= 0; i0--)
+               {
+                 int x;
+                 i = packing[i0];
+                 x = pb->geqs[e].coef[i];
+                 hashCode = hashCode * hash_key_multiplier * (i + 3) + x;
+               }
+
+             if (g > 1)
+               {
+                 pb->geqs[e].coef[0] = int_div (pb->geqs[e].coef[0], g);
+                 i0 = top_var;
+                 i = packing[i0--];
+                 pb->geqs[e].coef[i] = pb->geqs[e].coef[i] / g;
+                 hashCode = pb->geqs[e].coef[i] * (i + 3);
+
+                 for (; i0 >= 0; i0--)
+                   {
+                     i = packing[i0];
+                     pb->geqs[e].coef[i] = pb->geqs[e].coef[i] / g;
+                     hashCode = hashCode * hash_key_multiplier * (i + 3) 
+                       + pb->geqs[e].coef[i];
+                   }
+               }
+
+             g2 = abs (hashCode);
+
+             if (dump_file && (dump_flags & TDF_DETAILS))
+               {
+                 fprintf (dump_file, "Hash code = %d, eqn = ", hashCode);
+                 omega_print_geq (dump_file, pb, &pb->geqs[e]);
+                 fprintf (dump_file, "\n");
+               }
+
+             j = g2 % HASH_TABLE_SIZE;
+
+             do {
+               eqn proto = &(hash_master[j]);
+
+               if (proto->touched == g2)
+                 {
+                   if (proto->coef[0] == top_var)
+                     {
+                       if (hashCode >= 0)
+                         for (i0 = top_var; i0 >= 0; i0--)
+                           {
+                             i = packing[i0];
+
+                             if (pb->geqs[e].coef[i] != proto->coef[i])
+                               break;
+                           }
+                       else
+                         for (i0 = top_var; i0 >= 0; i0--)
+                           {
+                             i = packing[i0];
+
+                             if (pb->geqs[e].coef[i] != -proto->coef[i])
+                               break;
+                           }
+
+                       if (i0 < 0)
+                         {
+                           if (hashCode >= 0)
+                             pb->geqs[e].key = proto->key;
+                           else
+                             pb->geqs[e].key = -proto->key;
+                           break;
+                         }
+                     }
+                 }
+               else if (proto->touched < 0)
+                 {
+                   omega_init_eqn_zero (proto, pb->num_vars);
+                   if (hashCode >= 0)
+                     for (i0 = top_var; i0 >= 0; i0--)
+                       {
+                         i = packing[i0];
+                         proto->coef[i] = pb->geqs[e].coef[i];
+                       }
+                   else
+                     for (i0 = top_var; i0 >= 0; i0--)
+                       {
+                         i = packing[i0];
+                         proto->coef[i] = -pb->geqs[e].coef[i];
+                       }
+
+                   proto->coef[0] = top_var;
+                   proto->touched = g2;
+
+                   if (dump_file && (dump_flags & TDF_DETAILS))
+                     fprintf (dump_file, " constraint key = %d\n",
+                              next_key);
+
+                   proto->key = next_key++;
+
+                   /* Too many hash keys generated.  */
+                   gcc_assert (proto->key <= MAX_KEYS);
+
+                   if (hashCode >= 0)
+                     pb->geqs[e].key = proto->key;
+                   else
+                     pb->geqs[e].key = -proto->key;
+
+                   break;
+                 }
+
+               j = (j + 1) % HASH_TABLE_SIZE;
+             } while (1);
+           }
+
+         pb->geqs[e].touched = 0;
+       }
+
+      {
+       int eKey = pb->geqs[e].key;
+       int e2;
+       if (e > 0)
+         {
+           int cTerm = pb->geqs[e].coef[0];
+           e2 = fast_lookup[MAX_KEYS - eKey];
+
+           if (e2 < e && pb->geqs[e2].key == -eKey
+               && pb->geqs[e2].color == omega_black)
+             {
+               if (pb->geqs[e2].coef[0] < -cTerm)
+                 {
+                   if (dump_file && (dump_flags & TDF_DETAILS))
+                     {
+                       omega_print_geq (dump_file, pb, &pb->geqs[e]);
+                       fprintf (dump_file, "\n");
+                       omega_print_geq (dump_file, pb, &pb->geqs[e2]);
+                       fprintf (dump_file,
+                                "\nequations have no solution \n");
+                     }
+                   return normalize_false;
+                 }
+
+               if (pb->geqs[e2].coef[0] == -cTerm
+                   && (create_color 
+                       || pb->geqs[e].color == omega_black))
+                 {
+                   omega_copy_eqn (&pb->eqs[pb->num_eqs], &pb->geqs[e],
+                                   pb->num_vars);
+                   if (pb->geqs[e].color == omega_black)
+                     adding_equality_constraint (pb, pb->num_eqs);
+                   pb->num_eqs++;
+                   gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
+                 }
+             }
+
+           e2 = fast_lookup_red[MAX_KEYS - eKey];
+
+           if (e2 < e && pb->geqs[e2].key == -eKey
+               && pb->geqs[e2].color == omega_red)
+             {
+               if (pb->geqs[e2].coef[0] < -cTerm)
+                 {
+                   if (dump_file && (dump_flags & TDF_DETAILS))
+                     {
+                       omega_print_geq (dump_file, pb, &pb->geqs[e]);
+                       fprintf (dump_file, "\n");
+                       omega_print_geq (dump_file, pb, &pb->geqs[e2]);
+                       fprintf (dump_file,
+                                "\nequations have no solution \n");
+                     }
+                   return normalize_false;
+                 }
+
+               if (pb->geqs[e2].coef[0] == -cTerm && create_color)
+                 {
+                   omega_copy_eqn (&pb->eqs[pb->num_eqs], &pb->geqs[e],
+                                   pb->num_vars);
+                   pb->eqs[pb->num_eqs].color = omega_red;
+                   pb->num_eqs++;
+                   gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
+                 }
+             }
+
+           e2 = fast_lookup[MAX_KEYS + eKey];
+
+           if (e2 < e && pb->geqs[e2].key == eKey 
+               && pb->geqs[e2].color == omega_black)
+             {
+               if (pb->geqs[e2].coef[0] > cTerm)
+                 {
+                   if (pb->geqs[e].color == omega_black)
+                     {
+                       if (dump_file && (dump_flags & TDF_DETAILS))
+                         {
+                           fprintf (dump_file,
+                                    "Removing Redudant Equation: ");
+                           omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
+                           fprintf (dump_file, "\n");
+                           fprintf (dump_file,
+                                    "[a]      Made Redundant by: ");
+                           omega_print_geq (dump_file, pb, &(pb->geqs[e]));
+                           fprintf (dump_file, "\n");
+                         }
+                       pb->geqs[e2].coef[0] = cTerm;
+                       omega_delete_geq (pb, e, n_vars);
+                       e--;
+                       continue;
+                     }
+                 }
+               else
+                 {
+                   if (dump_file && (dump_flags & TDF_DETAILS))
+                     {
+                       fprintf (dump_file, "Removing Redudant Equation: ");
+                       omega_print_geq (dump_file, pb, &(pb->geqs[e]));
+                       fprintf (dump_file, "\n");
+                       fprintf (dump_file, "[b]      Made Redundant by: ");
+                       omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
+                       fprintf (dump_file, "\n");
+                     }
+                   omega_delete_geq (pb, e, n_vars);
+                   e--;
+                   continue;
+                 }
+             }
+
+           e2 = fast_lookup_red[MAX_KEYS + eKey];
+
+           if (e2 < e && pb->geqs[e2].key == eKey
+               && pb->geqs[e2].color == omega_red)
+             {
+               if (pb->geqs[e2].coef[0] >= cTerm)
+                 {
+                   if (dump_file && (dump_flags & TDF_DETAILS))
+                     {
+                       fprintf (dump_file, "Removing Redudant Equation: ");
+                       omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
+                       fprintf (dump_file, "\n");
+                       fprintf (dump_file, "[c]      Made Redundant by: ");
+                       omega_print_geq (dump_file, pb, &(pb->geqs[e]));
+                       fprintf (dump_file, "\n");
+                     }
+                   pb->geqs[e2].coef[0] = cTerm;
+                   pb->geqs[e2].color = pb->geqs[e].color;
+                 }
+               else if (pb->geqs[e].color == omega_red)
+                 {
+                   if (dump_file && (dump_flags & TDF_DETAILS))
+                     {
+                       fprintf (dump_file, "Removing Redudant Equation: ");
+                       omega_print_geq (dump_file, pb, &(pb->geqs[e]));
+                       fprintf (dump_file, "\n");
+                       fprintf (dump_file, "[d]      Made Redundant by: ");
+                       omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
+                       fprintf (dump_file, "\n");
+                     }
+                 }
+               omega_delete_geq (pb, e, n_vars);
+               e--;
+               continue;
+
+             }
+         }
+
+       if (pb->geqs[e].color == omega_red)
+         fast_lookup_red[MAX_KEYS + eKey] = e;
+       else
+         fast_lookup[MAX_KEYS + eKey] = e;
+      }
+    }
+
+  create_color = false;
+  return coupled_subscripts ? normalize_coupled : normalize_uncoupled;
+}
+
+/* Divide the coefficients of EQN by their gcd.  N_VARS is the number
+   of variables in EQN.  */
+
+static inline void
+divide_eqn_by_gcd (eqn eqn, int n_vars)
+{
+  int var, g = 0;
+
+  for (var = n_vars; var >= 0; var--)
+    g = gcd (abs (eqn->coef[var]), g);
+
+  if (g)
+    for (var = n_vars; var >= 0; var--)
+      eqn->coef[var] = eqn->coef[var] / g;
+}
+
+/* Rewrite some non-safe variables in function of protected
+   wildcard variables.  */
+
+static void
+cleanout_wildcards (omega_pb pb)
+{
+  int e, i, j;
+  int n_vars = pb->num_vars;
+  bool renormalize = false;
+
+  for (e = pb->num_eqs - 1; e >= 0; e--)
+    for (i = n_vars; !omega_safe_var_p (pb, i); i--)
+      if (pb->eqs[e].coef[i] != 0)
+       {
+         /* i is the last non-zero non-safe variable.  */
+
+         for (j = i - 1; !omega_safe_var_p (pb, j); j--)
+           if (pb->eqs[e].coef[j] != 0)
+             break;
+
+         /* j is the next non-zero non-safe variable, or points
+            to a safe variable: it is then a wildcard variable.  */
+
+         /* Clean it out.  */
+         if (omega_safe_var_p (pb, j))
+           {
+             eqn sub = &(pb->eqs[e]);
+             int c = pb->eqs[e].coef[i];
+             int a = abs (c);
+             int e2;
+
+             if (dump_file && (dump_flags & TDF_DETAILS))
+               {
+                 fprintf (dump_file,
+                          "Found a single wild card equality: ");
+                 omega_print_eq (dump_file, pb, &pb->eqs[e]);
+                 fprintf (dump_file, "\n");
+                 omega_print_problem (dump_file, pb);
+               }
+
+             for (e2 = pb->num_eqs - 1; e2 >= 0; e2--)
+               if (e != e2 && pb->eqs[e2].coef[i]
+                   && (pb->eqs[e2].color == omega_red
+                       || (pb->eqs[e2].color == omega_black 
+                           && pb->eqs[e].color == omega_black)))
+                 {
+                   eqn eqn = &(pb->eqs[e2]);
+                   int var, k;
+
+                   for (var = n_vars; var >= 0; var--)
+                     eqn->coef[var] *= a;
+
+                   k = eqn->coef[i];
+
+                   for (var = n_vars; var >= 0; var--)
+                     eqn->coef[var] -= sub->coef[var] * k / c;
+
+                   eqn->coef[i] = 0;
+                   divide_eqn_by_gcd (eqn, n_vars);
+                 }
+
+             for (e2 = pb->num_geqs - 1; e2 >= 0; e2--)
+               if (pb->geqs[e2].coef[i] 
+                   && (pb->geqs[e2].color == omega_red
+                       || (pb->eqs[e].color == omega_black 
+                           && pb->geqs[e2].color == omega_black)))
+                 {
+                   eqn eqn = &(pb->geqs[e2]);
+                   int var, k;
+
+                   for (var = n_vars; var >= 0; var--)
+                     eqn->coef[var] *= a;
+
+                   k = eqn->coef[i];
+
+                   for (var = n_vars; var >= 0; var--)
+                     eqn->coef[var] -= sub->coef[var] * k / c;
+
+                   eqn->coef[i] = 0;
+                   eqn->touched = 1;
+                   renormalize = true;
+                 }
+
+             for (e2 = pb->num_subs - 1; e2 >= 0; e2--)
+               if (pb->subs[e2].coef[i] 
+                   && (pb->subs[e2].color == omega_red
+                       || (pb->subs[e2].color == omega_black 
+                           && pb->eqs[e].color == omega_black)))
+                 {
+                   eqn eqn = &(pb->subs[e2]);
+                   int var, k;
+
+                   for (var = n_vars; var >= 0; var--)
+                     eqn->coef[var] *= a;
+
+                   k = eqn->coef[i];
+
+                   for (var = n_vars; var >= 0; var--)
+                     eqn->coef[var] -= sub->coef[var] * k / c;
+
+                   eqn->coef[i] = 0;
+                   divide_eqn_by_gcd (eqn, n_vars);
+                 }
+
+             if (dump_file && (dump_flags & TDF_DETAILS))
+               {
+                 fprintf (dump_file, "cleaned-out wildcard: ");
+                 omega_print_problem (dump_file, pb);
+               }
+             break;
+           }
+       }
+
+  if (renormalize)
+    normalize_omega_problem (pb);
+}
+
+/* Swap values contained in I and J.  */
+
+static inline void
+swap (int *i, int *j)
+{
+  int tmp;
+  tmp = *i;
+  *i = *j;
+  *j = tmp;
+}
+
+/* Swap values contained in I and J.  */
+
+static inline void
+bswap (bool *i, bool *j)
+{
+  bool tmp;
+  tmp = *i;
+  *i = *j;
+  *j = tmp;
+}
+
+/* Make variable IDX unprotected in PB, by swapping its index at the
+   PB->safe_vars rank.  */
+
+static inline void
+omega_unprotect_1 (omega_pb pb, int *idx, bool *unprotect)
+{
+  /* If IDX is protected...  */
+  if (*idx < pb->safe_vars)
+    {
+      /* ... swap its index with the last non protected index.  */
+      int j = pb->safe_vars;
+      int e;
+
+      for (e = pb->num_geqs - 1; e >= 0; e--)
+       {
+         pb->geqs[e].touched = 1;
+         swap (&pb->geqs[e].coef[*idx], &pb->geqs[e].coef[j]);
+       }
+
+      for (e = pb->num_eqs - 1; e >= 0; e--)
+       swap (&pb->eqs[e].coef[*idx], &pb->eqs[e].coef[j]);
+
+      for (e = pb->num_subs - 1; e >= 0; e--)
+       swap (&pb->subs[e].coef[*idx], &pb->subs[e].coef[j]);
+
+      if (unprotect)
+       bswap (&unprotect[*idx], &unprotect[j]);
+
+      swap (&pb->var[*idx], &pb->var[j]);
+      pb->forwarding_address[pb->var[*idx]] = *idx;
+      pb->forwarding_address[pb->var[j]] = j;
+      (*idx)--;
+    }
+
+  /* The variable at pb->safe_vars is also unprotected now.  */
+  pb->safe_vars--;
+}
+
+/* During the Fourier-Motzkin elimination some variables are
+   substituted with other variables.  This function resurrects the
+   substituted variables in PB.  */
+
+static void
+resurrect_subs (omega_pb pb)
+{
+  if (pb->num_subs > 0 
+      && please_no_equalities_in_simplified_problems == 0)
+    {
+      int i, e, n, m;
+
+      if (dump_file && (dump_flags & TDF_DETAILS))
+       {
+         fprintf (dump_file,
+                  "problem reduced, bringing variables back to life\n");
+         omega_print_problem (dump_file, pb);
+       }
+
+      for (i = 1; omega_safe_var_p (pb, i); i++)
+       if (omega_wildcard_p (pb, i))
+         omega_unprotect_1 (pb, &i, NULL);
+
+      m = pb->num_subs;
+      n = MAX (pb->num_vars, pb->safe_vars + m);
+
+      for (e = pb->num_geqs - 1; e >= 0; e--)
+       if (single_var_geq (&pb->geqs[e], pb->num_vars))
+         {
+           if (!omega_safe_var_p (pb, abs (pb->geqs[e].key)))
+             pb->geqs[e].key += (pb->geqs[e].key > 0 ? m : -m);
+         }
+       else
+         {
+           pb->geqs[e].touched = 1;
+           pb->geqs[e].key = 0;
+         }
+
+      for (i = pb->num_vars; !omega_safe_var_p (pb, i); i--)
+       {
+         pb->var[i + m] = pb->var[i];
+
+         for (e = pb->num_geqs - 1; e >= 0; e--)
+           pb->geqs[e].coef[i + m] = pb->geqs[e].coef[i];
+
+         for (e = pb->num_eqs - 1; e >= 0; e--)
+           pb->eqs[e].coef[i + m] = pb->eqs[e].coef[i];
+
+         for (e = pb->num_subs - 1; e >= 0; e--)
+           pb->subs[e].coef[i + m] = pb->subs[e].coef[i];
+       }
+
+      for (i = pb->safe_vars + m; !omega_safe_var_p (pb, i); i--)
+       {
+         for (e = pb->num_geqs - 1; e >= 0; e--)
+           pb->geqs[e].coef[i] = 0;
+
+         for (e = pb->num_eqs - 1; e >= 0; e--)
+           pb->eqs[e].coef[i] = 0;
+
+         for (e = pb->num_subs - 1; e >= 0; e--)
+           pb->subs[e].coef[i] = 0;
+       }
+
+      pb->num_vars += m;
+
+      for (e = pb->num_subs - 1; e >= 0; e--)
+       {
+         pb->var[pb->safe_vars + 1 + e] = pb->subs[e].key;
+         omega_copy_eqn (&(pb->eqs[pb->num_eqs]), &(pb->subs[e]),
+                         pb->num_vars);
+         pb->eqs[pb->num_eqs].coef[pb->safe_vars + 1 + e] = -1;
+         pb->eqs[pb->num_eqs].color = omega_black;
+
+         if (dump_file && (dump_flags & TDF_DETAILS))
+           {
+             fprintf (dump_file, "brought back: ");
+             omega_print_eq (dump_file, pb, &pb->eqs[pb->num_eqs]);
+             fprintf (dump_file, "\n");
+           }
+
+         pb->num_eqs++;
+         gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
+       }
+
+      pb->safe_vars += m;
+      pb->num_subs = 0;
+
+      if (dump_file && (dump_flags & TDF_DETAILS))
+       {
+         fprintf (dump_file, "variables brought back to life\n");
+         omega_print_problem (dump_file, pb);
+       }
+
+      cleanout_wildcards (pb);
+    }
+}
+
+static inline bool
+implies (unsigned int a, unsigned int b)
+{
+  return (a == (a & b));
+}
+
+/* Eliminate redundant equations in PB.  When EXPENSIVE is true, an
+   extra step is performed.  Returns omega_false when there exist no
+   solution, omega_true otherwise.  */
+
+enum omega_result
+omega_eliminate_redundant (omega_pb pb, bool expensive)
+{
+  int c, e, e1, e2, e3, p, q, i, k, alpha, alpha1, alpha2, alpha3;
+  bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
+  omega_pb tmp_problem;
+
+  /* {P,Z,N}EQS = {Positive,Zero,Negative} Equations.  */
+  unsigned int *peqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS);
+  unsigned int *zeqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS);
+  unsigned int *neqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS);
+
+  /* PP = Possible Positives, PZ = Possible Zeros, PN = Possible Negatives */
+  unsigned int pp, pz, pn;
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    {
+      fprintf (dump_file, "in eliminate Redudant:\n");
+      omega_print_problem (dump_file, pb);
+    }
+
+  for (e = pb->num_geqs - 1; e >= 0; e--)
+    {
+      int tmp = 1;
+
+      is_dead[e] = false;
+      peqs[e] = zeqs[e] = neqs[e] = 0;
+
+      for (i = pb->num_vars; i >= 1; i--)
+       {
+         if (pb->geqs[e].coef[i] > 0)
+           peqs[e] |= tmp;
+         else if (pb->geqs[e].coef[i] < 0)
+           neqs[e] |= tmp;
+         else
+           zeqs[e] |= tmp;
+
+         tmp <<= 1;
+       }
+    }
+
+
+  for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
+    if (!is_dead[e1])
+      for (e2 = e1 - 1; e2 >= 0; e2--)
+       if (!is_dead[e2])
+         {
+           for (p = pb->num_vars; p > 1; p--)
+             for (q = p - 1; q > 0; q--)
+               if ((alpha = pb->geqs[e1].coef[p] * pb->geqs[e2].coef[q]
+                    - pb->geqs[e2].coef[p] * pb->geqs[e1].coef[q]) != 0)
+                 goto foundPQ;
+
+           continue;
+
+         foundPQ:
+           pz = ((zeqs[e1] & zeqs[e2]) | (peqs[e1] & neqs[e2]) 
+                 | (neqs[e1] & peqs[e2]));
+           pp = peqs[e1] | peqs[e2];
+           pn = neqs[e1] | neqs[e2];
+
+           for (e3 = pb->num_geqs - 1; e3 >= 0; e3--)
+             if (e3 != e1 && e3 != e2)
+               {
+                 if (!implies (zeqs[e3], pz))
+                   goto nextE3;
+
+                 alpha1 = (pb->geqs[e2].coef[q] * pb->geqs[e3].coef[p]
+                           - pb->geqs[e2].coef[p] * pb->geqs[e3].coef[q]);
+                 alpha2 = -(pb->geqs[e1].coef[q] * pb->geqs[e3].coef[p]
+                            - pb->geqs[e1].coef[p] * pb->geqs[e3].coef[q]);
+                 alpha3 = alpha;
+
+                 if (alpha1 * alpha2 <= 0)
+                   goto nextE3;
+
+                 if (alpha1 < 0)
+                   {
+                     alpha1 = -alpha1;
+                     alpha2 = -alpha2;
+                     alpha3 = -alpha3;
+                   }
+
+                 if (alpha3 > 0)
+                   {
+                     /* Trying to prove e3 is redundant.  */
+                     if (!implies (peqs[e3], pp) 
+                         || !implies (neqs[e3], pn))
+                       goto nextE3;
+
+                     if (pb->geqs[e3].color == omega_black
+                         && (pb->geqs[e1].color == omega_red
+                             || pb->geqs[e2].color == omega_red))
+                       goto nextE3;
+
+                     for (k = pb->num_vars; k >= 1; k--)
+                       if (alpha3 * pb->geqs[e3].coef[k]
+                           != (alpha1 * pb->geqs[e1].coef[k]
+                               + alpha2 * pb->geqs[e2].coef[k]))
+                         goto nextE3;
+
+                     c = (alpha1 * pb->geqs[e1].coef[0]
+                          + alpha2 * pb->geqs[e2].coef[0]);
+
+                     if (c < alpha3 * (pb->geqs[e3].coef[0] + 1))
+                       {
+                         if (dump_file && (dump_flags & TDF_DETAILS))
+                           {
+                             fprintf (dump_file,
+                                      "found redundant inequality\n");
+                             fprintf (dump_file,
+                                      "alpha1, alpha2, alpha3 = %d,%d,%d\n",
+                                      alpha1, alpha2, alpha3);
+
+                             omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
+                             fprintf (dump_file, "\n");
+                             omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
+                             fprintf (dump_file, "\n=> ");
+                             omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
+                             fprintf (dump_file, "\n\n");
+                           }
+
+                         is_dead[e3] = true;
+                       }
+                   }
+                 else
+                   {
+                     /* Trying to prove e3 <= 0 and therefore e3 = 0,
+                       or trying to prove e3 < 0, and therefore the
+                       problem has no solutions.  */
+                     if (!implies (peqs[e3], pn) 
+                         || !implies (neqs[e3], pp))
+                       goto nextE3;
+
+                     if (pb->geqs[e1].color == omega_red
+                         || pb->geqs[e2].color == omega_red
+                         || pb->geqs[e3].color == omega_red)
+                       goto nextE3;
+
+                     alpha3 = alpha3;
+                     /* verify alpha1*v1+alpha2*v2 = alpha3*v3 */
+                     for (k = pb->num_vars; k >= 1; k--)
+                       if (alpha3 * pb->geqs[e3].coef[k]
+                           != (alpha1 * pb->geqs[e1].coef[k]
+                               + alpha2 * pb->geqs[e2].coef[k]))
+                         goto nextE3;
+
+                     c = (alpha1 * pb->geqs[e1].coef[0]
+                          + alpha2 * pb->geqs[e2].coef[0]);
+
+                     if (c < alpha3 * (pb->geqs[e3].coef[0]))
+                       {
+                         /* We just proved e3 < 0, so no solutions exist.  */
+                         if (dump_file && (dump_flags & TDF_DETAILS))
+                           {
+                             fprintf (dump_file,
+                                      "found implied over tight inequality\n");
+                             fprintf (dump_file,
+                                      "alpha1, alpha2, alpha3 = %d,%d,%d\n",
+                                      alpha1, alpha2, -alpha3);
+                             omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
+                             fprintf (dump_file, "\n");
+                             omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
+                             fprintf (dump_file, "\n=> not ");
+                             omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
+                             fprintf (dump_file, "\n\n");
+                           }
+                         free (is_dead);
+                         free (peqs);
+                         free (zeqs);
+                         free (neqs);
+                         return omega_false;
+                       }
+                     else if (c < alpha3 * (pb->geqs[e3].coef[0] - 1))
+                       {
+                         /* We just proved that e3 <=0, so e3 = 0.  */
+                         if (dump_file && (dump_flags & TDF_DETAILS))
+                           {
+                             fprintf (dump_file,
+                                      "found implied tight inequality\n");
+                             fprintf (dump_file,
+                                      "alpha1, alpha2, alpha3 = %d,%d,%d\n",
+                                      alpha1, alpha2, -alpha3);
+                             omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
+                             fprintf (dump_file, "\n");
+                             omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
+                             fprintf (dump_file, "\n=> inverse ");
+                             omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
+                             fprintf (dump_file, "\n\n");
+                           }
+
+                         omega_copy_eqn (&pb->eqs[pb->num_eqs++], 
+                                         &pb->geqs[e3], pb->num_vars);
+                         gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
+                         adding_equality_constraint (pb, pb->num_eqs - 1);
+                         is_dead[e3] = true;
+                       }
+                   }
+               nextE3:;
+               }
+         }
+
+  /* Delete the inequalities that were marked as dead.  */
+  for (e = pb->num_geqs - 1; e >= 0; e--)
+    if (is_dead[e])
+      omega_delete_geq (pb, e, pb->num_vars);
+
+  if (!expensive)
+    goto eliminate_redundant_done;
+
+  tmp_problem = XNEW (struct omega_pb);
+  conservative++;
+
+  for (e = pb->num_geqs - 1; e >= 0; e--)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+       {
+         fprintf (dump_file,
+                  "checking equation %d to see if it is redundant: ", e);
+         omega_print_geq (dump_file, pb, &(pb->geqs[e]));
+         fprintf (dump_file, "\n");
+       }
+
+      omega_copy_problem (tmp_problem, pb);
+      omega_negate_geq (tmp_problem, e);
+      tmp_problem->safe_vars = 0;
+      tmp_problem->variables_freed = false;
+
+      if (omega_solve_problem (tmp_problem, omega_false) == omega_false)
+       omega_delete_geq (pb, e, pb->num_vars);
+    }
+
+  free (tmp_problem);
+  conservative--;
+
+  if (!omega_reduce_with_subs)
+    {
+      resurrect_subs (pb);
+      gcc_assert (please_no_equalities_in_simplified_problems
+                 || pb->num_subs == 0);
+    }
+
+ eliminate_redundant_done:
+  free (is_dead);
+  free (peqs);
+  free (zeqs);
+  free (neqs);
+  return omega_true;
+}
+
+/* For each inequality that has coefficients bigger than 20, try to
+   create a new constraint that cannot be derived from the original
+   constraint and that has smaller coefficients.  Add the new
+   constraint at the end of geqs.  Return the number of inequalities
+   that have been added to PB.  */
+
+static int
+smooth_weird_equations (omega_pb pb)
+{
+  int e1, e2, e3, p, q, k, alpha, alpha1, alpha2, alpha3;
+  int c;
+  int v;
+  int result = 0;
+
+  for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
+    if (pb->geqs[e1].color == omega_black)
+      {
+       int g = 999999;
+
+       for (v = pb->num_vars; v >= 1; v--)
+         if (pb->geqs[e1].coef[v] != 0 && abs (pb->geqs[e1].coef[v]) < g)
+           g = abs (pb->geqs[e1].coef[v]);
+
+       /* Magic number.  */
+       if (g > 20)
+         {
+           e3 = pb->num_geqs;
+
+           for (v = pb->num_vars; v >= 1; v--)
+             pb->geqs[e3].coef[v] = int_div (6 * pb->geqs[e1].coef[v] + g / 2,
+                                             g);
+
+           pb->geqs[e3].color = omega_black;
+           pb->geqs[e3].touched = 1;
+           /* Magic number.  */
+           pb->geqs[e3].coef[0] = 9997;
+
+           if (dump_file && (dump_flags & TDF_DETAILS))
+             {
+               fprintf (dump_file, "Checking to see if we can derive: ");
+               omega_print_geq (dump_file, pb, &pb->geqs[e3]);
+               fprintf (dump_file, "\n from: ");
+               omega_print_geq (dump_file, pb, &pb->geqs[e1]);
+               fprintf (dump_file, "\n");
+             }
+
+           for (e2 = pb->num_geqs - 1; e2 >= 0; e2--)
+             if (e1 != e2 && pb->geqs[e2].color == omega_black)
+               {
+                 for (p = pb->num_vars; p > 1; p--)
+                   {
+                     for (q = p - 1; q > 0; q--)
+                       {
+                         alpha =
+                           (pb->geqs[e1].coef[p] * pb->geqs[e2].coef[q] -
+                            pb->geqs[e2].coef[p] * pb->geqs[e1].coef[q]);
+                         if (alpha != 0)
+                           goto foundPQ;
+                       }
+                   }
+                 continue;
+
+               foundPQ:
+
+                 alpha1 = (pb->geqs[e2].coef[q] * pb->geqs[e3].coef[p]
+                           - pb->geqs[e2].coef[p] * pb->geqs[e3].coef[q]);
+                 alpha2 = -(pb->geqs[e1].coef[q] * pb->geqs[e3].coef[p]
+                            - pb->geqs[e1].coef[p] * pb->geqs[e3].coef[q]);
+                 alpha3 = alpha;
+
+                 if (alpha1 * alpha2 <= 0)
+                   continue;
+
+                 if (alpha1 < 0)
+                   {
+                     alpha1 = -alpha1;
+                     alpha2 = -alpha2;
+                     alpha3 = -alpha3;
+                   }
+
+                 if (alpha3 > 0)
+                   {
+                     /* Try to prove e3 is redundant: verify
+                        alpha1*v1 + alpha2*v2 = alpha3*v3.  */
+                     for (k = pb->num_vars; k >= 1; k--)
+                       if (alpha3 * pb->geqs[e3].coef[k]
+                           != (alpha1 * pb->geqs[e1].coef[k]
+                               + alpha2 * pb->geqs[e2].coef[k]))
+                         goto nextE2;
+
+                     c = alpha1 * pb->geqs[e1].coef[0]
+                       + alpha2 * pb->geqs[e2].coef[0];
+
+                     if (c < alpha3 * (pb->geqs[e3].coef[0] + 1))
+                       pb->geqs[e3].coef[0] = int_div (c, alpha3);
+                   }
+               nextE2:;
+               }
+
+           if (pb->geqs[e3].coef[0] < 9997)
+             {
+               result++;
+               pb->num_geqs++;
+
+               if (dump_file && (dump_flags & TDF_DETAILS))
+                 {
+                   fprintf (dump_file,
+                            "Smoothing wierd equations; adding:\n");
+                   omega_print_geq (dump_file, pb, &pb->geqs[e3]);
+                   fprintf (dump_file, "\nto:\n");
+                   omega_print_problem (dump_file, pb);
+                   fprintf (dump_file, "\n\n");
+                 }
+             }
+         }
+      }
+  return result;
+}
+
+/* Replace tuples of inequalities, that define upper and lower half
+   spaces, with an equation.  */
+
+static void
+coalesce (omega_pb pb)
+{
+  int e, e2;
+  int colors = 0;
+  bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
+  int found_something = 0;
+
+  for (e = 0; e < pb->num_geqs; e++)
+    if (pb->geqs[e].color == omega_red)
+      colors++;
+
+  if (colors < 2)
+    return;
+
+  for (e = 0; e < pb->num_geqs; e++)
+    is_dead[e] = false;
+
+  for (e = 0; e < pb->num_geqs; e++)
+    if (pb->geqs[e].color == omega_red 
+       && !pb->geqs[e].touched)
+      for (e2 = e + 1; e2 < pb->num_geqs; e2++)
+       if (!pb->geqs[e2].touched 
+           && pb->geqs[e].key == -pb->geqs[e2].key
+           && pb->geqs[e].coef[0] == -pb->geqs[e2].coef[0] 
+           && pb->geqs[e2].color == omega_red)
+         {
+           omega_copy_eqn (&pb->eqs[pb->num_eqs++], &pb->geqs[e],
+                           pb->num_vars);
+           gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
+           found_something++;
+           is_dead[e] = true;
+           is_dead[e2] = true;
+         }
+
+  for (e = pb->num_geqs - 1; e >= 0; e--)
+    if (is_dead[e])
+      omega_delete_geq (pb, e, pb->num_vars);
+
+  if (dump_file && (dump_flags & TDF_DETAILS) && found_something)
+    {
+      fprintf (dump_file, "Coalesced pb->geqs into %d EQ's:\n",
+              found_something);
+      omega_print_problem (dump_file, pb);
+    }
+
+  free (is_dead);
+}
+
+/* Eliminate red inequalities from PB.  When ELIMINATE_ALL is
+   true, continue to eliminate all the red inequalities.  */
+
+void
+omega_eliminate_red (omega_pb pb, bool eliminate_all)
+{
+  int e, e2, e3, i, j, k, a, alpha1, alpha2;
+  int c = 0;
+  bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
+  int dead_count = 0;
+  int red_found;
+  omega_pb tmp_problem;
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    {
+      fprintf (dump_file, "in eliminate RED:\n");
+      omega_print_problem (dump_file, pb);
+    }
+
+  if (pb->num_eqs > 0)
+    omega_simplify_problem (pb);
+
+  for (e = pb->num_geqs - 1; e >= 0; e--)
+    is_dead[e] = false;
+
+  for (e = pb->num_geqs - 1; e >= 0; e--)
+    if (pb->geqs[e].color == omega_black && !is_dead[e])
+      for (e2 = e - 1; e2 >= 0; e2--)
+       if (pb->geqs[e2].color == omega_black 
+           && !is_dead[e2])
+         {
+           a = 0;
+
+           for (i = pb->num_vars; i > 1; i--)
+             for (j = i - 1; j > 0; j--)
+               if ((a = (pb->geqs[e].coef[i] * pb->geqs[e2].coef[j]
+                         - pb->geqs[e2].coef[i] * pb->geqs[e].coef[j])) != 0)
+                 goto found_pair;
+
+           continue;
+
+         found_pair:
+           if (dump_file && (dump_flags & TDF_DETAILS))
+             {
+               fprintf (dump_file,
+                        "found two equations to combine, i = %s, ",
+                        omega_variable_to_str (pb, i));
+               fprintf (dump_file, "j = %s, alpha = %d\n",
+                        omega_variable_to_str (pb, j), a);
+               omega_print_geq (dump_file, pb, &(pb->geqs[e]));
+               fprintf (dump_file, "\n");
+               omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
+               fprintf (dump_file, "\n");
+             }
+
+           for (e3 = pb->num_geqs - 1; e3 >= 0; e3--)
+             if (pb->geqs[e3].color == omega_red)
+               {
+                 alpha1 = (pb->geqs[e2].coef[j] * pb->geqs[e3].coef[i] 
+                           - pb->geqs[e2].coef[i] * pb->geqs[e3].coef[j]);
+                 alpha2 = -(pb->geqs[e].coef[j] * pb->geqs[e3].coef[i]
+                            - pb->geqs[e].coef[i] * pb->geqs[e3].coef[j]);
+
+                 if ((a > 0 && alpha1 > 0 && alpha2 > 0)
+                     || (a < 0 && alpha1 < 0 && alpha2 < 0))
+                   {
+                     if (dump_file && (dump_flags & TDF_DETAILS))
+                       {
+                         fprintf (dump_file,
+                                  "alpha1 = %d, alpha2 = %d;"
+                                  "comparing against: ",
+                                  alpha1, alpha2);
+                         omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
+                         fprintf (dump_file, "\n");
+                       }
+
+                     for (k = pb->num_vars; k >= 0; k--)
+                       {
+                         c = (alpha1 * pb->geqs[e].coef[k] 
+                              + alpha2 * pb->geqs[e2].coef[k]);
+
+                         if (c != a * pb->geqs[e3].coef[k])
+                           break;
+
+                         if (dump_file && (dump_flags & TDF_DETAILS) && k > 0)
+                           fprintf (dump_file, " %s: %d, %d\n",
+                                    omega_variable_to_str (pb, k), c,
+                                    a * pb->geqs[e3].coef[k]);
+                       }
+
+                     if (k < 0
+                         || (k == 0 &&
+                             ((a > 0 && c < a * pb->geqs[e3].coef[k])
+                              || (a < 0 && c > a * pb->geqs[e3].coef[k]))))
+                       {
+                         if (dump_file && (dump_flags & TDF_DETAILS))
+                           {
+                             dead_count++;
+                             fprintf (dump_file,
+                                      "red equation#%d is dead "
+                                      "(%d dead so far, %d remain)\n",
+                                      e3, dead_count,
+                                      pb->num_geqs - dead_count);
+                             omega_print_geq (dump_file, pb, &(pb->geqs[e]));
+                             fprintf (dump_file, "\n");
+                             omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
+                             fprintf (dump_file, "\n");
+                             omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
+                             fprintf (dump_file, "\n");
+                           }
+                         is_dead[e3] = true;
+                       }
+                   }
+               }
+         }
+
+  for (e = pb->num_geqs - 1; e >= 0; e--)
+    if (is_dead[e])
+      omega_delete_geq (pb, e, pb->num_vars);
+
+  free (is_dead);
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    {
+      fprintf (dump_file, "in eliminate RED, easy tests done:\n");
+      omega_print_problem (dump_file, pb);
+    }
+
+  for (red_found = 0, e = pb->num_geqs - 1; e >= 0; e--)
+    if (pb->geqs[e].color == omega_red)
+      red_found = 1;
+
+  if (!red_found)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+       fprintf (dump_file, "fast checks worked\n");
+
+      if (!omega_reduce_with_subs)
+       gcc_assert (please_no_equalities_in_simplified_problems
+                   || pb->num_subs == 0);
+
+      return;
+    }
+
+  if (!omega_verify_simplification
+      && verify_omega_pb (pb) == omega_false)
+    return;
+
+  conservative++;
+  tmp_problem = XNEW (struct omega_pb);
+
+  for (e = pb->num_geqs - 1; e >= 0; e--)
+    if (pb->geqs[e].color == omega_red)
+      {
+       if (dump_file && (dump_flags & TDF_DETAILS))
+         {
+           fprintf (dump_file,
+                    "checking equation %d to see if it is redundant: ", e);
+           omega_print_geq (dump_file, pb, &(pb->geqs[e]));
+           fprintf (dump_file, "\n");
+         }
+
+       omega_copy_problem (tmp_problem, pb);
+       omega_negate_geq (tmp_problem, e);
+       tmp_problem->safe_vars = 0;
+       tmp_problem->variables_freed = false;
+       tmp_problem->num_subs = 0;
+
+       if (omega_solve_problem (tmp_problem, omega_false) == omega_false)
+         {
+           if (dump_file && (dump_flags & TDF_DETAILS))
+             fprintf (dump_file, "it is redundant\n");
+           omega_delete_geq (pb, e, pb->num_vars);
+         }
+       else
+         {
+           if (dump_file && (dump_flags & TDF_DETAILS))
+             fprintf (dump_file, "it is not redundant\n");
+
+           if (!eliminate_all)
+             {
+               if (dump_file && (dump_flags & TDF_DETAILS))
+                 fprintf (dump_file, "no need to check other red equations\n");
+               break;
+             }
+         }
+      }
+
+  conservative--;
+  free (tmp_problem);
+  /* omega_simplify_problem (pb); */
+
+  if (!omega_reduce_with_subs)
+    gcc_assert (please_no_equalities_in_simplified_problems
+               || pb->num_subs == 0);
+}
+
+/* Transform some wildcard variables to non-safe variables.  */
+
+static void
+chain_unprotect (omega_pb pb)
+{
+  int i, e;
+  bool *unprotect = XNEWVEC (bool, OMEGA_MAX_VARS);
+
+  for (i = 1; omega_safe_var_p (pb, i); i++)
+    {
+      unprotect[i] = omega_wildcard_p (pb, i);
+
+      for (e = pb->num_subs - 1; e >= 0; e--)
+       if (pb->subs[e].coef[i])
+         unprotect[i] = false;
+    }
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    {
+      fprintf (dump_file, "Doing chain reaction unprotection\n");
+      omega_print_problem (dump_file, pb);
+
+      for (i = 1; omega_safe_var_p (pb, i); i++)
+       if (unprotect[i])
+         fprintf (dump_file, "unprotecting %s\n",
+                  omega_variable_to_str (pb, i));
+    }
+
+  for (i = 1; omega_safe_var_p (pb, i); i++)
+    if (unprotect[i])
+      omega_unprotect_1 (pb, &i, unprotect);
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    {
+      fprintf (dump_file, "After chain reactions\n");
+      omega_print_problem (dump_file, pb);
+    }
+
+  free (unprotect);
+}
+
+/* Reduce problem PB.  */
+
+static void
+omega_problem_reduced (omega_pb pb)
+{
+  if (omega_verify_simplification
+      && !in_approximate_mode 
+      && verify_omega_pb (pb) == omega_false)
+    return;
+
+  if (PARAM_VALUE (PARAM_OMEGA_ELIMINATE_REDUNDANT_CONSTRAINTS)
+      && !omega_eliminate_redundant (pb, true))
+    return;
+
+  omega_found_reduction = omega_true;
+
+  if (!please_no_equalities_in_simplified_problems)
+    coalesce (pb);
+
+  if (omega_reduce_with_subs 
+      || please_no_equalities_in_simplified_problems)
+    chain_unprotect (pb);
+  else
+    resurrect_subs (pb);
+
+  if (!return_single_result)
+    {
+      int i;
+
+      for (i = 1; omega_safe_var_p (pb, i); i++)
+       pb->forwarding_address[pb->var[i]] = i;
+
+      for (i = 0; i < pb->num_subs; i++)
+       pb->forwarding_address[pb->subs[i].key] = -i - 1;
+
+      (*omega_when_reduced) (pb);
+    }
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    {
+      fprintf (dump_file, "-------------------------------------------\n");
+      fprintf (dump_file, "problem reduced:\n");
+      omega_print_problem (dump_file, pb);
+      fprintf (dump_file, "-------------------------------------------\n");
+    }
+}
+
+/* Eliminates all the free variables for problem PB, that is all the
+   variables from FV to PB->NUM_VARS.  */
+
+static void
+omega_free_eliminations (omega_pb pb, int fv)
+{
+  bool try_again = true;
+  int i, e, e2;
+  int n_vars = pb->num_vars;
+
+  while (try_again)
+    {
+      try_again = false;
+
+      for (i = n_vars; i > fv; i--)
+       {
+         for (e = pb->num_geqs - 1; e >= 0; e--)
+           if (pb->geqs[e].coef[i])
+             break;
+
+         if (e < 0)
+           e2 = e;
+         else if (pb->geqs[e].coef[i] > 0)
+           {
+             for (e2 = e - 1; e2 >= 0; e2--)
+               if (pb->geqs[e2].coef[i] < 0)
+                 break;
+           }
+         else
+           {
+             for (e2 = e - 1; e2 >= 0; e2--)
+               if (pb->geqs[e2].coef[i] > 0)
+                 break;
+           }
+
+         if (e2 < 0)
+           {
+             int e3;
+             for (e3 = pb->num_subs - 1; e3 >= 0; e3--)
+               if (pb->subs[e3].coef[i])
+                 break;
+
+             if (e3 >= 0)
+               continue;
+
+             for (e3 = pb->num_eqs - 1; e3 >= 0; e3--)
+               if (pb->eqs[e3].coef[i])
+                 break;
+
+             if (e3 >= 0)
+               continue;
+
+             if (dump_file && (dump_flags & TDF_DETAILS))
+               fprintf (dump_file, "a free elimination of %s\n",
+                        omega_variable_to_str (pb, i));
+
+             if (e >= 0)
+               {
+                 omega_delete_geq (pb, e, n_vars);
+
+                 for (e--; e >= 0; e--)
+                   if (pb->geqs[e].coef[i])
+                     omega_delete_geq (pb, e, n_vars);
+
+                 try_again = (i < n_vars);
+               }
+
+             omega_delete_variable (pb, i);
+             n_vars = pb->num_vars;
+           }
+       }
+    }
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    {
+      fprintf (dump_file, "\nafter free eliminations:\n");
+      omega_print_problem (dump_file, pb);
+      fprintf (dump_file, "\n");
+    }
+}
+
+/* Do free red eliminations.  */
+
+static void
+free_red_eliminations (omega_pb pb)
+{
+  bool try_again = true;
+  int i, e, e2;
+  int n_vars = pb->num_vars;
+  bool *is_red_var = XNEWVEC (bool, OMEGA_MAX_VARS);
+  bool *is_dead_var = XNEWVEC (bool, OMEGA_MAX_VARS);
+  bool *is_dead_geq = XNEWVEC (bool, OMEGA_MAX_GEQS);
+
+  for (i = n_vars; i > 0; i--)
+    {
+      is_red_var[i] = false;
+      is_dead_var[i] = false;
+    }
+
+  for (e = pb->num_geqs - 1; e >= 0; e--)
+    {
+      is_dead_geq[e] = false;
+
+      if (pb->geqs[e].color == omega_red)
+       for (i = n_vars; i > 0; i--)
+         if (pb->geqs[e].coef[i] != 0)
+           is_red_var[i] = true;
+    }
+
+  while (try_again)
+    {
+      try_again = false;
+      for (i = n_vars; i > 0; i--)
+       if (!is_red_var[i] && !is_dead_var[i])
+         {
+           for (e = pb->num_geqs - 1; e >= 0; e--)
+             if (!is_dead_geq[e] && pb->geqs[e].coef[i])
+               break;
+
+           if (e < 0)
+             e2 = e;
+           else if (pb->geqs[e].coef[i] > 0)
+             {
+               for (e2 = e - 1; e2 >= 0; e2--)
+                 if (!is_dead_geq[e2] && pb->geqs[e2].coef[i] < 0)
+                   break;
+             }
+           else
+             {
+               for (e2 = e - 1; e2 >= 0; e2--)
+                 if (!is_dead_geq[e2] && pb->geqs[e2].coef[i] > 0)
+                   break;
+             }
+
+           if (e2 < 0)
+             {
+               int e3;
+               for (e3 = pb->num_subs - 1; e3 >= 0; e3--)
+                 if (pb->subs[e3].coef[i])
+                   break;
+
+               if (e3 >= 0)
+                 continue;
+
+               for (e3 = pb->num_eqs - 1; e3 >= 0; e3--)
+                 if (pb->eqs[e3].coef[i])
+                   break;
+
+               if (e3 >= 0)
+                 continue;
+
+               if (dump_file && (dump_flags & TDF_DETAILS))
+                 fprintf (dump_file, "a free red elimination of %s\n",
+                          omega_variable_to_str (pb, i));
+
+               for (; e >= 0; e--)
+                 if (pb->geqs[e].coef[i])
+                   is_dead_geq[e] = true;
+
+               try_again = true;
+               is_dead_var[i] = true;
+             }
+         }
+    }
+
+  for (e = pb->num_geqs - 1; e >= 0; e--)
+    if (is_dead_geq[e])
+      omega_delete_geq (pb, e, n_vars);
+
+  for (i = n_vars; i > 0; i--)
+    if (is_dead_var[i])
+      omega_delete_variable (pb, i);
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    {
+      fprintf (dump_file, "\nafter free red eliminations:\n");
+      omega_print_problem (dump_file, pb);
+      fprintf (dump_file, "\n");
+    }
+
+  free (is_red_var);
+  free (is_dead_var);
+  free (is_dead_geq);
+}
+
+/* For equation EQ of the form "0 = EQN", insert in PB two
+   inequalities "0 <= EQN" and "0 <= -EQN".  */
+
+void
+omega_convert_eq_to_geqs (omega_pb pb, int eq)
+{
+  int i;
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    fprintf (dump_file, "Converting Eq to Geqs\n");
+
+  /* Insert "0 <= EQN".  */
+  omega_copy_eqn (&pb->geqs[pb->num_geqs], &pb->eqs[eq], pb->num_vars);
+  pb->geqs[pb->num_geqs].touched = 1;
+  pb->num_geqs++;
+
+  /* Insert "0 <= -EQN".  */
+  omega_copy_eqn (&pb->geqs[pb->num_geqs], &pb->eqs[eq], pb->num_vars);
+  pb->geqs[pb->num_geqs].touched = 1;
+
+  for (i = 0; i <= pb->num_vars; i++)
+    pb->geqs[pb->num_geqs].coef[i] *= -1;
+
+  pb->num_geqs++;
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    omega_print_problem (dump_file, pb);
+}
+
+/* Eliminates variable I from PB.  */
+
+static void
+omega_do_elimination (omega_pb pb, int e, int i)
+{
+  eqn sub = omega_alloc_eqns (0, 1);
+  int c;
+  int n_vars = pb->num_vars;
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    fprintf (dump_file, "eliminating variable %s\n",
+            omega_variable_to_str (pb, i));
+
+  omega_copy_eqn (sub, &pb->eqs[e], pb->num_vars);
+  c = sub->coef[i];
+  sub->coef[i] = 0;
+  if (c == 1 || c == -1)
+    {
+      if (pb->eqs[e].color == omega_red)
+       {
+         bool fB;
+         omega_substitute_red (pb, sub, i, c, &fB);
+         if (fB)
+           omega_convert_eq_to_geqs (pb, e);
+         else
+           omega_delete_variable (pb, i);
+       }
+      else
+       {
+         omega_substitute (pb, sub, i, c);
+         omega_delete_variable (pb, i);
+       }
+    }
+  else
+    {
+      int a = abs (c);
+      int e2 = e;
+
+      if (dump_file && (dump_flags & TDF_DETAILS))
+       fprintf (dump_file, "performing non-exact elimination, c = %d\n", c);
+
+      for (e = pb->num_eqs - 1; e >= 0; e--)
+       if (pb->eqs[e].coef[i])
+         {
+           eqn eqn = &(pb->eqs[e]);
+           int j, k;
+           for (j = n_vars; j >= 0; j--)
+             eqn->coef[j] *= a;
+           k = eqn->coef[i];
+           eqn->coef[i] = 0;
+           eqn->color |= sub->color;
+           for (j = n_vars; j >= 0; j--)
+             eqn->coef[j] -= sub->coef[j] * k / c;
+         }
+
+      for (e = pb->num_geqs - 1; e >= 0; e--)
+       if (pb->geqs[e].coef[i])
+         {
+           eqn eqn = &(pb->geqs[e]);
+           int j, k;
+
+           if (sub->color == omega_red)
+             eqn->color = omega_red;
+
+           for (j = n_vars; j >= 0; j--)
+             eqn->coef[j] *= a;
+
+           eqn->touched = 1;
+           k = eqn->coef[i];
+           eqn->coef[i] = 0;
+
+           for (j = n_vars; j >= 0; j--)
+             eqn->coef[j] -= sub->coef[j] * k / c;
+
+         }
+
+      for (e = pb->num_subs - 1; e >= 0; e--)
+       if (pb->subs[e].coef[i])
+         {
+           eqn eqn = &(pb->subs[e]);
+           int j, k;
+           gcc_assert (0);
+           gcc_assert (sub->color == omega_black);
+           for (j = n_vars; j >= 0; j--)
+             eqn->coef[j] *= a;
+           k = eqn->coef[i];
+           eqn->coef[i] = 0;
+           for (j = n_vars; j >= 0; j--)
+             eqn->coef[j] -= sub->coef[j] * k / c;
+         }
+
+      if (in_approximate_mode)
+       omega_delete_variable (pb, i);
+      else
+       omega_convert_eq_to_geqs (pb, e2);
+    }
+
+  omega_free_eqns (sub, 1);
+}
+
+/* Helper function for printing "sorry, no solution".  */
+
+static inline enum omega_result
+omega_problem_has_no_solution (void)
+{
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    fprintf (dump_file, "\nequations have no solution \n");
+
+  return omega_false;
+}
+
+/* Helper function: solve equations in PB one at a time, following the
+   DESIRED_RES result.  */
+
+static enum omega_result
+omega_solve_eq (omega_pb pb, enum omega_result desired_res)
+{
+  int i, j, e;
+  int g, g2;
+  g = 0;
+
+
+  if (dump_file && (dump_flags & TDF_DETAILS) && pb->num_eqs > 0)
+    {
+      fprintf (dump_file, "\nomega_solve_eq (%d, %d)\n",
+              desired_res, may_be_red);
+      omega_print_problem (dump_file, pb);
+      fprintf (dump_file, "\n");
+    }
+
+  if (may_be_red)
+    {
+      i = 0;
+      j = pb->num_eqs - 1;
+
+      while (1)
+       {
+         eqn eq;
+
+         while (i <= j && pb->eqs[i].color == omega_red)
+           i++;
+
+         while (i <= j && pb->eqs[j].color == omega_black)
+           j--;
+
+         if (i >= j)
+           break;
+
+         eq = omega_alloc_eqns (0, 1);
+         omega_copy_eqn (eq, &pb->eqs[i], pb->num_vars);
+         omega_copy_eqn (&pb->eqs[i], &pb->eqs[j], pb->num_vars);
+         omega_copy_eqn (&pb->eqs[j], eq, pb->num_vars);
+         omega_free_eqns (eq, 1);
+         i++;
+         j--;
+       }
+    }
+
+  /* Eliminate all EQ equations */
+  for (e = pb->num_eqs - 1; e >= 0; e--)
+    {
+      eqn eqn = &(pb->eqs[e]);
+      int sv;
+
+      if (dump_file && (dump_flags & TDF_DETAILS))
+       fprintf (dump_file, "----\n");
+
+      for (i = pb->num_vars; i > 0; i--)
+       if (eqn->coef[i])
+         break;
+
+      g = eqn->coef[i];
+
+      for (j = i - 1; j > 0; j--)
+       if (eqn->coef[j])
+         break;
+
+      /* i is the position of last non-zero coefficient,
+        g is the coefficient of i,
+        j is the position of next non-zero coefficient.  */
+
+      if (j == 0)
+       {
+         if (eqn->coef[0] % g != 0)
+           return omega_problem_has_no_solution ();
+
+         eqn->coef[0] = eqn->coef[0] / g;
+         eqn->coef[i] = 1;
+         pb->num_eqs--;
+         omega_do_elimination (pb, e, i);
+         continue;
+       }
+
+      else if (j == -1)
+       {
+         if (eqn->coef[0] != 0)
+           return omega_problem_has_no_solution ();
+
+         pb->num_eqs--;
+         continue;
+       }
+
+      if (g < 0)
+       g = -g;
+
+      if (g == 1)
+       {
+         pb->num_eqs--;
+         omega_do_elimination (pb, e, i);
+       }
+
+      else
+       {
+         int k = j;
+         bool promotion_possible =
+           (omega_safe_var_p (pb, j)
+            && pb->safe_vars + 1 == i
+            && !omega_eqn_is_red (eqn, desired_res)
+            && !in_approximate_mode);
+
+         if (dump_file && (dump_flags & TDF_DETAILS) && promotion_possible)
+           fprintf (dump_file, " Promotion possible\n");
+
+       normalizeEQ:
+         if (!omega_safe_var_p (pb, j))
+           {
+             for (; g != 1 && !omega_safe_var_p (pb, j); j--)
+               g = gcd (abs (eqn->coef[j]), g);
+             g2 = g;
+           }
+         else if (!omega_safe_var_p (pb, i))
+           g2 = g;
+         else
+           g2 = 0;
+
+         for (; g != 1 && j > 0; j--)
+           g = gcd (abs (eqn->coef[j]), g);
+
+         if (g > 1)
+           {
+             if (eqn->coef[0] % g != 0)
+               return omega_problem_has_no_solution ();
+
+             for (j = 0; j <= pb->num_vars; j++)
+               eqn->coef[j] /= g;
+
+             g2 = g2 / g;
+           }
+
+         if (g2 > 1)
+           {
+             int e2;
+
+             for (e2 = e - 1; e2 >= 0; e2--)
+               if (pb->eqs[e2].coef[i])
+                 break;
+
+             if (e2 == -1)
+               for (e2 = pb->num_geqs - 1; e2 >= 0; e2--)
+                 if (pb->geqs[e2].coef[i])
+                   break;
+
+             if (e2 == -1)
+               for (e2 = pb->num_subs - 1; e2 >= 0; e2--)
+                 if (pb->subs[e2].coef[i])
+                   break;
+
+             if (e2 == -1)
+               {
+                 bool change = false;
+
+                 if (dump_file && (dump_flags & TDF_DETAILS))
+                   {
+                     fprintf (dump_file, "Ha! We own it! \n");
+                     omega_print_eq (dump_file, pb, eqn);
+                     fprintf (dump_file, " \n");
+                   }
+
+                 g = eqn->coef[i];
+                 g = abs (g);
+
+                 for (j = i - 1; j >= 0; j--)
+                   {
+                     int t = int_mod (eqn->coef[j], g);
+
+                     if (2 * t >= g)
+                       t -= g;
+
+                     if (t != eqn->coef[j])
+                       {
+                         eqn->coef[j] = t;
+                         change = true;
+                       }
+                   }
+
+                 if (!change)
+                   {
+                     if (dump_file && (dump_flags & TDF_DETAILS))
+                       fprintf (dump_file, "So what?\n");
+                   }
+
+                 else
+                   {
+                     omega_name_wild_card (pb, i);
+
+                     if (dump_file && (dump_flags & TDF_DETAILS))
+                       {
+                         omega_print_eq (dump_file, pb, eqn);
+                         fprintf (dump_file, " \n");
+                       }
+
+                     e++;
+                     continue;
+                   }
+               }
+           }
+
+         if (promotion_possible)
+           {
+             if (dump_file && (dump_flags & TDF_DETAILS))
+               {
+                 fprintf (dump_file, "promoting %s to safety\n",
+                          omega_variable_to_str (pb, i));
+                 omega_print_vars (dump_file, pb);
+               }
+
+             pb->safe_vars++;
+
+             if (!omega_wildcard_p (pb, i))
+               omega_name_wild_card (pb, i);
+
+             promotion_possible = false;
+             j = k;
+             goto normalizeEQ;
+           }
+
+         if (g2 > 1 && !in_approximate_mode)
+           {
+             if (pb->eqs[e].color == omega_red)
+               {
+                 if (dump_file && (dump_flags & TDF_DETAILS))
+                   fprintf (dump_file, "handling red equality\n");
+
+                 pb->num_eqs--;
+                 omega_do_elimination (pb, e, i);
+                 continue;
+               }
+
+             if (dump_file && (dump_flags & TDF_DETAILS))
+               {
+                 fprintf (dump_file,
+                          "adding equation to handle safe variable \n");
+                 omega_print_eq (dump_file, pb, eqn);
+                 fprintf (dump_file, "\n----\n");
+                 omega_print_problem (dump_file, pb);
+                 fprintf (dump_file, "\n----\n");
+                 fprintf (dump_file, "\n----\n");
+               }
+
+             i = omega_add_new_wild_card (pb);
+             pb->num_eqs++;
+             gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
+             omega_init_eqn_zero (&pb->eqs[e + 1], pb->num_vars);
+             omega_copy_eqn (&pb->eqs[e + 1], eqn, pb->safe_vars);
+
+             for (j = pb->num_vars; j >= 0; j--)
+               {
+                 pb->eqs[e + 1].coef[j] = int_mod (pb->eqs[e + 1].coef[j], g2);
+
+                 if (2 * pb->eqs[e + 1].coef[j] >= g2)
+                   pb->eqs[e + 1].coef[j] -= g2;
+               }
+
+             pb->eqs[e + 1].coef[i] = g2;
+             e += 2;
+
+             if (dump_file && (dump_flags & TDF_DETAILS))
+               omega_print_problem (dump_file, pb);
+
+             continue;
+           }
+
+         sv = pb->safe_vars;
+         if (g2 == 0)
+           sv = 0;
+
+         /* Find variable to eliminate.  */
+         if (g2 > 1)
+           {
+             gcc_assert (in_approximate_mode);
+
+             if (dump_file && (dump_flags & TDF_DETAILS))
+               {
+                 fprintf (dump_file, "non-exact elimination: ");
+                 omega_print_eq (dump_file, pb, eqn);
+                 fprintf (dump_file, "\n");
+                 omega_print_problem (dump_file, pb);
+               }
+
+             for (i = pb->num_vars; i > sv; i--)
+               if (pb->eqs[e].coef[i] != 0)
+                 break;
+           }
+         else
+           for (i = pb->num_vars; i > sv; i--)
+             if (pb->eqs[e].coef[i] == 1 || pb->eqs[e].coef[i] == -1)
+               break;
+
+         if (i > sv)
+           {
+             pb->num_eqs--;
+             omega_do_elimination (pb, e, i);
+
+             if (dump_file && (dump_flags & TDF_DETAILS) && g2 > 1)
+               {
+                 fprintf (dump_file, "result of non-exact elimination:\n");
+                 omega_print_problem (dump_file, pb);
+               }
+           }
+         else
+           {
+             int factor = (INT_MAX);
+             j = 0;
+
+             if (dump_file && (dump_flags & TDF_DETAILS))
+               fprintf (dump_file, "doing moding\n");
+
+             for (i = pb->num_vars; i != sv; i--)
+               if ((pb->eqs[e].coef[i] & 1) != 0)
+                 {
+                   j = i;
+                   i--;
+
+                   for (; i != sv; i--)
+                     if ((pb->eqs[e].coef[i] & 1) != 0)
+                       break;
+
+                   break;
+                 }
+
+             if (j != 0 && i == sv)
+               {
+                 omega_do_mod (pb, 2, e, j);
+                 e++;
+                 continue;
+               }
+
+             j = 0;
+             for (i = pb->num_vars; i != sv; i--)
+               if (pb->eqs[e].coef[i] != 0 
+                   && factor > abs (pb->eqs[e].coef[i]) + 1)
+                 {
+                   factor = abs (pb->eqs[e].coef[i]) + 1;
+                   j = i;
+                 }
+
+             if (j == sv)
+               {
+                 if (dump_file && (dump_flags & TDF_DETAILS))
+                   fprintf (dump_file, "should not have happened\n");
+                 gcc_assert (0);
+               }
+
+             omega_do_mod (pb, factor, e, j);
+             /* Go back and try this equation again.  */
+             e++;
+           }
+       }
+    }
+
+  pb->num_eqs = 0;
+  return omega_unknown;
+}
+
+/* Transform an inequation E to an equality, then solve DIFF problems
+   based on PB, and only differing by the constant part that is
+   diminished by one, trying to figure out which of the constants
+   satisfies PB.    */
+
+static enum omega_result
+parallel_splinter (omega_pb pb, int e, int diff,
+                  enum omega_result desired_res)
+{
+  omega_pb tmp_problem;
+  int i;
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    {
+      fprintf (dump_file, "Using parallel splintering\n");
+      omega_print_problem (dump_file, pb);
+    }
+
+  tmp_problem = XNEW (struct omega_pb);
+  omega_copy_eqn (&pb->eqs[0], &pb->geqs[e], pb->num_vars);
+  pb->num_eqs = 1;
+
+  for (i = 0; i <= diff; i++)
+    {
+      omega_copy_problem (tmp_problem, pb);
+
+      if (dump_file && (dump_flags & TDF_DETAILS))
+       {
+         fprintf (dump_file, "Splinter # %i\n", i);
+         omega_print_problem (dump_file, pb);
+       }
+
+      if (omega_solve_problem (tmp_problem, desired_res) == omega_true)
+       {
+         free (tmp_problem);
+         return omega_true;
+       }
+
+      pb->eqs[0].coef[0]--;
+    }
+
+  free (tmp_problem);
+  return omega_false;
+}
+
+/* Helper function: solve equations one at a time.  */
+
+static enum omega_result
+omega_solve_geq (omega_pb pb, enum omega_result desired_res)
+{
+  int i, e;
+  int n_vars, fv;
+  enum omega_result result;
+  bool coupled_subscripts = false;
+  bool smoothed = false;
+  bool eliminate_again;
+  bool tried_eliminating_redundant = false;
+
+  if (desired_res != omega_simplify)
+    {
+      pb->num_subs = 0;
+      pb->safe_vars = 0;
+    }
+
+ solve_geq_start:
+  do {
+    gcc_assert (desired_res == omega_simplify || pb->num_subs == 0);
+
+    /* Verify that there are not too many inequalities.  */
+    gcc_assert (pb->num_geqs <= OMEGA_MAX_GEQS);
+
+    if (dump_file && (dump_flags & TDF_DETAILS))
+      {
+       fprintf (dump_file, "\nomega_solve_geq (%d,%d):\n",
+                desired_res, please_no_equalities_in_simplified_problems);
+       omega_print_problem (dump_file, pb);
+       fprintf (dump_file, "\n");
+      }
+
+    n_vars = pb->num_vars;
+
+    if (n_vars == 1)
+      {
+       enum omega_eqn_color u_color = omega_black;
+       enum omega_eqn_color l_color = omega_black;
+       int upper_bound = pos_infinity;
+       int lower_bound = neg_infinity;
+
+       for (e = pb->num_geqs - 1; e >= 0; e--)
+         {
+           int a = pb->geqs[e].coef[1];
+           int c = pb->geqs[e].coef[0];
+
+           /* Our equation is ax + c >= 0, or ax >= -c, or c >= -ax.  */
+           if (a == 0)
+             {
+               if (c < 0)
+                 return omega_problem_has_no_solution ();
+             }
+           else if (a > 0)
+             {
+               if (a != 1)
+                 c = int_div (c, a);
+
+               if (lower_bound < -c
+                   || (lower_bound == -c
+                       && !omega_eqn_is_red (&pb->geqs[e], desired_res)))
+                 {
+                   lower_bound = -c;
+                   l_color = pb->geqs[e].color;
+                 }
+             }
+           else
+             {
+               if (a != -1)
+                 c = int_div (c, -a);
+
+               if (upper_bound > c
+                   || (upper_bound == c 
+                       && !omega_eqn_is_red (&pb->geqs[e], desired_res)))
+                 {
+                   upper_bound = c;
+                   u_color = pb->geqs[e].color;
+                 }
+             }
+         }
+
+       if (dump_file && (dump_flags & TDF_DETAILS))
+         {
+           fprintf (dump_file, "upper bound = %d\n", upper_bound);
+           fprintf (dump_file, "lower bound = %d\n", lower_bound);
+         }
+
+       if (lower_bound > upper_bound)
+         return omega_problem_has_no_solution ();
+
+       if (desired_res == omega_simplify)
+         {
+           pb->num_geqs = 0;
+           if (pb->safe_vars == 1)
+             {
+
+               if (lower_bound == upper_bound
+                   && u_color == omega_black
+                   && l_color == omega_black)
+                 {
+                   pb->eqs[0].coef[0] = -lower_bound;
+                   pb->eqs[0].coef[1] = 1;
+                   pb->eqs[0].color = omega_black;
+                   pb->num_eqs = 1;
+                   return omega_solve_problem (pb, desired_res);
+                 }
+               else
+                 {
+                   if (lower_bound > neg_infinity)
+                     {
+                       pb->geqs[0].coef[0] = -lower_bound;
+                       pb->geqs[0].coef[1] = 1;
+                       pb->geqs[0].key = 1;
+                       pb->geqs[0].color = l_color;
+                       pb->geqs[0].touched = 0;
+                       pb->num_geqs = 1;
+                     }
+
+                   if (upper_bound < pos_infinity)
+                     {
+                       pb->geqs[pb->num_geqs].coef[0] = upper_bound;
+                       pb->geqs[pb->num_geqs].coef[1] = -1;
+                       pb->geqs[pb->num_geqs].key = -1;
+                       pb->geqs[pb->num_geqs].color = u_color;
+                       pb->geqs[pb->num_geqs].touched = 0;
+                       pb->num_geqs++;
+                     }
+                 }
+             }
+           else
+             pb->num_vars = 0;
+
+           omega_problem_reduced (pb);
+           return omega_false;
+         }
+
+       if (original_problem != no_problem
+           && l_color == omega_black
+           && u_color == omega_black
+           && !conservative
+           && lower_bound == upper_bound)
+         {
+           pb->eqs[0].coef[0] = -lower_bound;
+           pb->eqs[0].coef[1] = 1;
+           pb->num_eqs = 1;
+           adding_equality_constraint (pb, 0);
+         }
+
+       return omega_true;
+      }
+
+    if (!pb->variables_freed)
+      {
+       pb->variables_freed = true;
+
+       if (desired_res != omega_simplify)
+         omega_free_eliminations (pb, 0);
+       else
+         omega_free_eliminations (pb, pb->safe_vars);
+
+       n_vars = pb->num_vars;
+
+       if (n_vars == 1)
+         continue;
+      }
+
+    switch (normalize_omega_problem (pb))
+      {
+      case normalize_false:
+       return omega_false;
+       break;
+
+      case normalize_coupled:
+       coupled_subscripts = true;
+       break;
+
+      case normalize_uncoupled:
+       coupled_subscripts = false;
+       break;
+
+      default:
+       gcc_unreachable ();
+      }
+
+    n_vars = pb->num_vars;
+
+    if (dump_file && (dump_flags & TDF_DETAILS))
+      {
+       fprintf (dump_file, "\nafter normalization:\n");
+       omega_print_problem (dump_file, pb);
+       fprintf (dump_file, "\n");
+       fprintf (dump_file, "eliminating variable using Fourier-Motzkin.\n");
+      }
+
+    do {
+      int parallel_difference = INT_MAX;
+      int best_parallel_eqn = -1;
+      int minC, maxC, minCj = 0;
+      int lower_bound_count = 0;
+      int e2, Le = 0, Ue;
+      bool possible_easy_int_solution;
+      int max_splinters = 1;
+      bool exact = false;
+      bool lucky_exact = false;
+      int neweqns = 0;
+      int best = (INT_MAX);
+      int j = 0, jLe = 0, jLowerBoundCount = 0;
+
+
+      eliminate_again = false;
+
+      if (pb->num_eqs > 0)
+       return omega_solve_problem (pb, desired_res);
+
+      if (!coupled_subscripts)
+       {
+         if (pb->safe_vars == 0)
+           pb->num_geqs = 0;
+         else
+           for (e = pb->num_geqs - 1; e >= 0; e--)
+             if (!omega_safe_var_p (pb, abs (pb->geqs[e].key)))
+               omega_delete_geq (pb, e, n_vars);
+
+         pb->num_vars = pb->safe_vars;
+
+         if (desired_res == omega_simplify)
+           {
+             omega_problem_reduced (pb);
+             return omega_false;
+           }
+
+         return omega_true;
+       }
+
+      if (desired_res != omega_simplify)
+       fv = 0;
+      else
+       fv = pb->safe_vars;
+
+      if (pb->num_geqs == 0)
+       {
+         if (desired_res == omega_simplify)
+           {
+             pb->num_vars = pb->safe_vars;
+             omega_problem_reduced (pb);
+             return omega_false;
+           }
+         return omega_true;
+       }
+
+      if (desired_res == omega_simplify && n_vars == pb->safe_vars)
+       {
+         omega_problem_reduced (pb);
+         return omega_false;
+       }
+
+      if (pb->num_geqs > OMEGA_MAX_GEQS - 30
+         || pb->num_geqs > 2 * n_vars * n_vars + 4 * n_vars + 10)
+       {
+         if (dump_file && (dump_flags & TDF_DETAILS))
+           fprintf (dump_file,
+                    "TOO MANY EQUATIONS; "
+                    "%d equations, %d variables, "
+                    "ELIMINATING REDUNDANT ONES\n",
+                    pb->num_geqs, n_vars);
+
+         if (!omega_eliminate_redundant (pb, false))
+           return omega_false;
+
+         n_vars = pb->num_vars;
+
+         if (pb->num_eqs > 0)
+           return omega_solve_problem (pb, desired_res);
+
+         if (dump_file && (dump_flags & TDF_DETAILS))
+           fprintf (dump_file, "END ELIMINATION OF REDUNDANT EQUATIONS\n");
+       }
+
+      if (desired_res != omega_simplify)
+       fv = 0;
+      else
+       fv = pb->safe_vars;
+
+      for (i = n_vars; i != fv; i--)
+       {
+         int score;
+         int ub = -2;
+         int lb = -2;
+         bool lucky = false;
+         int upper_bound_count = 0;
+
+         lower_bound_count = 0;
+         minC = maxC = 0;
+
+         for (e = pb->num_geqs - 1; e >= 0; e--)
+           if (pb->geqs[e].coef[i] < 0)
+             {
+               minC = MIN (minC, pb->geqs[e].coef[i]);
+               upper_bound_count++;
+               if (pb->geqs[e].coef[i] < -1)
+                 {
+                   if (ub == -2)
+                     ub = e;
+                   else
+                     ub = -1;
+                 }
+             }
+           else if (pb->geqs[e].coef[i] > 0)
+             {
+               maxC = MAX (maxC, pb->geqs[e].coef[i]);
+               lower_bound_count++;
+               Le = e;
+               if (pb->geqs[e].coef[i] > 1)
+                 {
+                   if (lb == -2)
+                     lb = e;
+                   else
+                     lb = -1;
+                 }
+             }
+
+         if (lower_bound_count == 0
+             || upper_bound_count == 0)
+           {
+             lower_bound_count = 0;
+             break;
+           }
+
+         if (ub >= 0 && lb >= 0
+             && pb->geqs[lb].key == -pb->geqs[ub].key)
+           {
+             int Lc = pb->geqs[lb].coef[i];
+             int Uc = -pb->geqs[ub].coef[i];
+             int diff =
+               Lc * pb->geqs[ub].coef[0] + Uc * pb->geqs[lb].coef[0];
+             lucky = (diff >= (Uc - 1) * (Lc - 1));
+           }
+
+         if (maxC == 1 
+             || minC == -1 
+             || lucky 
+             || in_approximate_mode)
+           {
+             neweqns = score = upper_bound_count * lower_bound_count;
+
+             if (dump_file && (dump_flags & TDF_DETAILS))
+               fprintf (dump_file,
+                        "For %s, exact, score = %d*%d, range = %d ... %d,"
+                        "\nlucky = %d, in_approximate_mode=%d \n",
+                        omega_variable_to_str (pb, i),
+                        upper_bound_count,
+                        lower_bound_count, minC, maxC, lucky, 
+                        in_approximate_mode);
+
+             if (!exact
+                 || score < best)
+               {
+
+                 best = score;
+                 j = i;
+                 minCj = minC;
+                 jLe = Le;
+                 jLowerBoundCount = lower_bound_count;
+                 exact = true;
+                 lucky_exact = lucky;
+                 if (score == 1)
+                   break;
+               }
+           }
+         else if (!exact)
+           {
+             if (dump_file && (dump_flags & TDF_DETAILS))
+               fprintf (dump_file,
+                        "For %s, non-exact, score = %d*%d,"
+                        "range = %d ... %d \n",
+                        omega_variable_to_str (pb, i),
+                        upper_bound_count,
+                        lower_bound_count, minC, maxC);
+
+             neweqns = upper_bound_count * lower_bound_count;
+             score = maxC - minC;
+
+             if (best > score)
+               {
+                 best = score;
+                 j = i;
+                 minCj = minC;
+                 jLe = Le;
+                 jLowerBoundCount = lower_bound_count;
+               }
+           }
+       }
+
+      if (lower_bound_count == 0)
+       {
+         omega_free_eliminations (pb, pb->safe_vars);
+         n_vars = pb->num_vars;
+         eliminate_again = true;
+         continue;
+       }
+
+      i = j;
+      minC = minCj;
+      Le = jLe;
+      lower_bound_count = jLowerBoundCount;
+
+      for (e = pb->num_geqs - 1; e >= 0; e--)
+       if (pb->geqs[e].coef[i] > 0)
+         {
+           if (pb->geqs[e].coef[i] == -minC)
+             max_splinters += -minC - 1;
+           else
+             max_splinters +=
+               check_pos_mul ((pb->geqs[e].coef[i] - 1),
+                              (-minC - 1)) / (-minC) + 1;
+         }
+
+      /* #ifdef Omega3 */
+      /* Trying to produce exact elimination by finding redundant
+        constraints.  */
+      if (!exact && !tried_eliminating_redundant)
+       {
+         omega_eliminate_redundant (pb, false);
+         tried_eliminating_redundant = true;
+         eliminate_again = true;
+         continue;
+       }
+      tried_eliminating_redundant = false;
+      /* #endif */
+
+      if (return_single_result && desired_res == omega_simplify && !exact)
+       {
+         omega_problem_reduced (pb);
+         return omega_true;
+       }
+
+      /* #ifndef Omega3 */
+      /* Trying to produce exact elimination by finding redundant
+        constraints.  */
+      if (!exact && !tried_eliminating_redundant)
+       {
+         omega_eliminate_redundant (pb, false);
+         tried_eliminating_redundant = true;
+         continue;
+       }
+      tried_eliminating_redundant = false;
+      /* #endif */
+
+      if (!exact)
+       {
+         int e1, e2;
+
+         for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
+           if (pb->geqs[e1].color == omega_black)
+             for (e2 = e1 - 1; e2 >= 0; e2--)
+               if (pb->geqs[e2].color == omega_black
+                   && pb->geqs[e1].key == -pb->geqs[e2].key
+                   && ((pb->geqs[e1].coef[0] + pb->geqs[e2].coef[0])
+                       * (3 - single_var_geq (&pb->geqs[e1], pb->num_vars))
+                       / 2 < parallel_difference))
+                 {
+                   parallel_difference =
+                     (pb->geqs[e1].coef[0] + pb->geqs[e2].coef[0])
+                     * (3 - single_var_geq (&pb->geqs[e1], pb->num_vars))
+                     / 2;
+                   best_parallel_eqn = e1;
+                 }
+
+         if (dump_file && (dump_flags & TDF_DETAILS)
+             && best_parallel_eqn >= 0)
+           {
+             fprintf (dump_file,
+                      "Possible parallel projection, diff = %d, in ",
+                      parallel_difference);
+             omega_print_geq (dump_file, pb, &(pb->geqs[best_parallel_eqn]));
+             fprintf (dump_file, "\n");
+             omega_print_problem (dump_file, pb);
+           }
+       }
+
+      if (dump_file && (dump_flags & TDF_DETAILS))
+       {
+         fprintf (dump_file, "going to eliminate %s, (%d,%d,%d)\n",
+                  omega_variable_to_str (pb, i), i, minC,
+                  lower_bound_count);
+         omega_print_problem (dump_file, pb);
+
+         if (lucky_exact)
+           fprintf (dump_file, "(a lucky exact elimination)\n");
+
+         else if (exact)
+           fprintf (dump_file, "(an exact elimination)\n");
+
+         fprintf (dump_file, "Max # of splinters = %d\n", max_splinters);
+       }
+
+      gcc_assert (max_splinters >= 1);
+
+      if (!exact && desired_res == omega_simplify && best_parallel_eqn >= 0
+         && parallel_difference <= max_splinters)
+       return parallel_splinter (pb, best_parallel_eqn, parallel_difference,
+                                 desired_res);
+
+      smoothed = false;
+
+      if (i != n_vars)
+       {
+         int t;
+         int j = pb->num_vars;
+
+         if (dump_file && (dump_flags & TDF_DETAILS))
+           {
+             fprintf (dump_file, "Swapping %d and %d\n", i, j);
+             omega_print_problem (dump_file, pb);
+           }
+
+         swap (&pb->var[i], &pb->var[j]);
+
+         for (e = pb->num_geqs - 1; e >= 0; e--)
+           if (pb->geqs[e].coef[i] != pb->geqs[e].coef[j])
+             {
+               pb->geqs[e].touched = 1;
+               t = pb->geqs[e].coef[i];
+               pb->geqs[e].coef[i] = pb->geqs[e].coef[j];
+               pb->geqs[e].coef[j] = t;
+             }
+
+         for (e = pb->num_subs - 1; e >= 0; e--)
+           if (pb->subs[e].coef[i] != pb->subs[e].coef[j])
+             {
+               t = pb->subs[e].coef[i];
+               pb->subs[e].coef[i] = pb->subs[e].coef[j];
+               pb->subs[e].coef[j] = t;
+             }
+
+         if (dump_file && (dump_flags & TDF_DETAILS))
+           {
+             fprintf (dump_file, "Swapping complete \n");
+             omega_print_problem (dump_file, pb);
+             fprintf (dump_file, "\n");
+           }
+
+         i = j;
+       }
+
+      else if (dump_file && (dump_flags & TDF_DETAILS))
+       {
+         fprintf (dump_file, "No swap needed\n");
+         omega_print_problem (dump_file, pb);
+       }
+
+      pb->num_vars--;
+      n_vars = pb->num_vars;
+
+      if (exact)
+       {
+         if (n_vars == 1)
+           {
+             int upper_bound = pos_infinity;
+             int lower_bound = neg_infinity;
+             enum omega_eqn_color ub_color = omega_black;
+             enum omega_eqn_color lb_color = omega_black;
+             int topeqn = pb->num_geqs - 1;
+             int Lc = pb->geqs[Le].coef[i];
+
+             for (Le = topeqn; Le >= 0; Le--)
+               if ((Lc = pb->geqs[Le].coef[i]) == 0)
+                 {
+                   if (pb->geqs[Le].coef[1] == 1)
+                     {
+                       int constantTerm = -pb->geqs[Le].coef[0];
+
+                       if (constantTerm > lower_bound ||
+                           (constantTerm == lower_bound &&
+                            !omega_eqn_is_red (&pb->geqs[Le], desired_res)))
+                         {
+                           lower_bound = constantTerm;
+                           lb_color = pb->geqs[Le].color;
+                         }
+
+                       if (dump_file && (dump_flags & TDF_DETAILS))
+                         {
+                           if (pb->geqs[Le].color == omega_black)
+                             fprintf (dump_file, " :::=> %s >= %d\n",
+                                      omega_variable_to_str (pb, 1),
+                                      constantTerm);
+                           else
+                             fprintf (dump_file,
+                                      " :::=> [%s >= %d]\n",
+                                      omega_variable_to_str (pb, 1),
+                                      constantTerm);
+                         }
+                     }
+                   else
+                     {
+                       int constantTerm = pb->geqs[Le].coef[0];
+                       if (constantTerm < upper_bound ||
+                           (constantTerm == upper_bound
+                            && !omega_eqn_is_red (&pb->geqs[Le],
+                                                  desired_res)))
+                         {
+                           upper_bound = constantTerm;
+                           ub_color = pb->geqs[Le].color;
+                         }
+
+                       if (dump_file && (dump_flags & TDF_DETAILS))
+                         {
+                           if (pb->geqs[Le].color == omega_black)
+                             fprintf (dump_file, " :::=> %s <= %d\n",
+                                      omega_variable_to_str (pb, 1),
+                                      constantTerm);
+                           else
+                             fprintf (dump_file,
+                                      " :::=> [%s <= %d]\n",
+                                      omega_variable_to_str (pb, 1),
+                                      constantTerm);
+                         }
+                     }
+                 }
+               else if (Lc > 0)
+                 for (Ue = topeqn; Ue >= 0; Ue--)
+                   if (pb->geqs[Ue].coef[i] < 0
+                       && pb->geqs[Le].key != -pb->geqs[Ue].key)
+                     {
+                       int Uc = -pb->geqs[Ue].coef[i];
+                       int coefficient = pb->geqs[Ue].coef[1] * Lc
+                         + pb->geqs[Le].coef[1] * Uc;
+                       int constantTerm = pb->geqs[Ue].coef[0] * Lc
+                         + pb->geqs[Le].coef[0] * Uc;
+
+                       if (dump_file && (dump_flags & TDF_DETAILS))
+                         {
+                           omega_print_geq_extra (dump_file, pb,
+                                                  &(pb->geqs[Ue]));
+                           fprintf (dump_file, "\n");
+                           omega_print_geq_extra (dump_file, pb,
+                                                  &(pb->geqs[Le]));
+                           fprintf (dump_file, "\n");
+                         }
+
+                       if (coefficient > 0)
+                         {
+                           constantTerm = -int_div (constantTerm, coefficient);
+
+                           if (constantTerm > lower_bound 
+                               || (constantTerm == lower_bound 
+                                   && (desired_res != omega_simplify 
+                                       || (pb->geqs[Ue].color == omega_black
+                                           && pb->geqs[Le].color == omega_black))))
+                             {
+                               lower_bound = constantTerm;
+                               lb_color = (pb->geqs[Ue].color == omega_red
+                                           || pb->geqs[Le].color == omega_red)
+                                 ? omega_red : omega_black;
+                             }
+
+                           if (dump_file && (dump_flags & TDF_DETAILS))
+                             {
+                               if (pb->geqs[Ue].color == omega_red
+                                   || pb->geqs[Le].color == omega_red)
+                                 fprintf (dump_file,
+                                          " ::=> [%s >= %d]\n",
+                                          omega_variable_to_str (pb, 1),
+                                          constantTerm);
+                               else
+                                 fprintf (dump_file,
+                                          " ::=> %s >= %d\n",
+                                          omega_variable_to_str (pb, 1),
+                                          constantTerm);
+                             }
+                         }
+                       else
+                         {
+                           constantTerm = int_div (constantTerm, -coefficient);
+                           if (constantTerm < upper_bound
+                               || (constantTerm == upper_bound
+                                   && pb->geqs[Ue].color == omega_black
+                                   && pb->geqs[Le].color == omega_black))
+                             {
+                               upper_bound = constantTerm;
+                               ub_color = (pb->geqs[Ue].color == omega_red
+                                           || pb->geqs[Le].color == omega_red)
+                                 ? omega_red : omega_black;
+                             }
+
+                           if (dump_file
+                               && (dump_flags & TDF_DETAILS))
+                             {
+                               if (pb->geqs[Ue].color == omega_red
+                                   || pb->geqs[Le].color == omega_red)
+                                 fprintf (dump_file,
+                                          " ::=> [%s <= %d]\n",
+                                          omega_variable_to_str (pb, 1),
+                                          constantTerm);
+                               else
+                                 fprintf (dump_file,
+                                          " ::=> %s <= %d\n",
+                                          omega_variable_to_str (pb, 1),
+                                          constantTerm);
+                             }
+                         }
+                     }
+
+             pb->num_geqs = 0;
+
+             if (dump_file && (dump_flags & TDF_DETAILS))
+               fprintf (dump_file,
+                        " therefore, %c%d <= %c%s%c <= %d%c\n",
+                        lb_color == omega_red ? '[' : ' ', lower_bound,
+                        (lb_color == omega_red && ub_color == omega_black)
+                        ? ']' : ' ',
+                        omega_variable_to_str (pb, 1),
+                        (lb_color == omega_black && ub_color == omega_red)
+                        ? '[' : ' ',
+                        upper_bound, ub_color == omega_red ? ']' : ' ');
+
+             if (lower_bound > upper_bound)
+               return omega_false;
+
+             if (pb->safe_vars == 1)
+               {
+                 if (upper_bound == lower_bound
+                     && !(ub_color == omega_red || lb_color == omega_red)
+                     && !please_no_equalities_in_simplified_problems)
+                   {
+                     pb->num_eqs++;
+                     pb->eqs[0].coef[1] = -1;
+                     pb->eqs[0].coef[0] = upper_bound;
+
+                     if (ub_color == omega_red
+                         || lb_color == omega_red)
+                       pb->eqs[0].color = omega_red;
+
+                     if (desired_res == omega_simplify
+                         && pb->eqs[0].color == omega_black)
+                       return omega_solve_problem (pb, desired_res);
+                   }
+
+                 if (upper_bound != pos_infinity)
+                   {
+                     pb->geqs[0].coef[1] = -1;
+                     pb->geqs[0].coef[0] = upper_bound;
+                     pb->geqs[0].color = ub_color;
+                     pb->geqs[0].key = -1;
+                     pb->geqs[0].touched = 0;
+                     pb->num_geqs++;
+                   }
+
+                 if (lower_bound != neg_infinity)
+                   {
+                     pb->geqs[pb->num_geqs].coef[1] = 1;
+                     pb->geqs[pb->num_geqs].coef[0] = -lower_bound;
+                     pb->geqs[pb->num_geqs].color = lb_color;
+                     pb->geqs[pb->num_geqs].key = 1;
+                     pb->geqs[pb->num_geqs].touched = 0;
+                     pb->num_geqs++;
+                   }
+               }
+
+             if (desired_res == omega_simplify)
+               {
+                 omega_problem_reduced (pb);
+                 return omega_false;
+               }
+             else
+               {
+                 if (!conservative 
+                     && (desired_res != omega_simplify
+                         || (lb_color == omega_black
+                             && ub_color == omega_black))
+                     && original_problem != no_problem
+                     && lower_bound == upper_bound)
+                   {
+                     for (i = original_problem->num_vars; i >= 0; i--)
+                       if (original_problem->var[i] == pb->var[1])
+                         break;
+
+                     if (i == 0)
+                       break;
+
+                     e = original_problem->num_eqs++;
+                     omega_init_eqn_zero (&original_problem->eqs[e],
+                                          original_problem->num_vars);
+                     original_problem->eqs[e].coef[i] = -1;
+                     original_problem->eqs[e].coef[0] = upper_bound;
+
+                     if (dump_file && (dump_flags & TDF_DETAILS))
+                       {
+                         fprintf (dump_file,
+                                  "adding equality %d to outer problem\n", e);
+                         omega_print_problem (dump_file, original_problem);
+                       }
+                   }
+                 return omega_true;
+               }
+           }
+
+         eliminate_again = true;
+
+         if (lower_bound_count == 1)
+           {
+             eqn lbeqn = omega_alloc_eqns (0, 1);
+             int Lc = pb->geqs[Le].coef[i];
+
+             if (dump_file && (dump_flags & TDF_DETAILS))
+               fprintf (dump_file, "an inplace elimination\n");
+
+             omega_copy_eqn (lbeqn, &pb->geqs[Le], (n_vars + 1));
+             omega_delete_geq_extra (pb, Le, n_vars + 1);
+
+             for (Ue = pb->num_geqs - 1; Ue >= 0; Ue--)
+               if (pb->geqs[Ue].coef[i] < 0)
+                 {
+                   if (lbeqn->key == -pb->geqs[Ue].key)
+                     omega_delete_geq_extra (pb, Ue, n_vars + 1);
+                   else
+                     {
+                       int k;
+                       int Uc = -pb->geqs[Ue].coef[i];
+                       pb->geqs[Ue].touched = 1;
+                       eliminate_again = false;
+
+                       if (lbeqn->color == omega_red)
+                         pb->geqs[Ue].color = omega_red;
+
+                       for (k = 0; k <= n_vars; k++)
+                         pb->geqs[Ue].coef[k] =
+                           check_mul (pb->geqs[Ue].coef[k], Lc) +
+                           check_mul (lbeqn->coef[k], Uc);
+
+                       if (dump_file && (dump_flags & TDF_DETAILS))
+                         {
+                           omega_print_geq (dump_file, pb,
+                                            &(pb->geqs[Ue]));
+                           fprintf (dump_file, "\n");
+                         }
+                     }
+                 }
+
+             omega_free_eqns (lbeqn, 1);
+             continue;
+           }
+         else
+           {
+             int *dead_eqns = XNEWVEC (int, OMEGA_MAX_GEQS);
+             bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
+             int num_dead = 0;
+             int top_eqn = pb->num_geqs - 1;
+             lower_bound_count--;
+
+             if (dump_file && (dump_flags & TDF_DETAILS))
+               fprintf (dump_file, "lower bound count = %d\n",
+                        lower_bound_count);
+
+             for (Le = top_eqn; Le >= 0; Le--)
+               if (pb->geqs[Le].coef[i] > 0)
+                 {
+                   int Lc = pb->geqs[Le].coef[i];
+                   for (Ue = top_eqn; Ue >= 0; Ue--)
+                     if (pb->geqs[Ue].coef[i] < 0)
+                       {
+                         if (pb->geqs[Le].key != -pb->geqs[Ue].key)
+                           {
+                             int k;
+                             int Uc = -pb->geqs[Ue].coef[i];
+
+                             if (num_dead == 0)
+                               e2 = pb->num_geqs++;
+                             else
+                               e2 = dead_eqns[--num_dead];
+
+                             gcc_assert (e2 < OMEGA_MAX_GEQS);
+
+                             if (dump_file && (dump_flags & TDF_DETAILS))
+                               {
+                                 fprintf (dump_file,
+                                          "Le = %d, Ue = %d, gen = %d\n",
+                                          Le, Ue, e2);
+                                 omega_print_geq_extra (dump_file, pb,
+                                                        &(pb->geqs[Le]));
+                                 fprintf (dump_file, "\n");
+                                 omega_print_geq_extra (dump_file, pb,
+                                                        &(pb->geqs[Ue]));
+                                 fprintf (dump_file, "\n");
+                               }
+
+                             eliminate_again = false;
+
+                             for (k = n_vars; k >= 0; k--)
+                               pb->geqs[e2].coef[k] =
+                                 check_mul (pb->geqs[Ue].coef[k], Lc) +
+                                 check_mul (pb->geqs[Le].coef[k], Uc);
+
+                             pb->geqs[e2].coef[n_vars + 1] = 0;
+                             pb->geqs[e2].touched = 1;
+
+                             if (pb->geqs[Ue].color == omega_red 
+                                 || pb->geqs[Le].color == omega_red)
+                               pb->geqs[e2].color = omega_red;
+                             else
+                               pb->geqs[e2].color = omega_black;
+
+                             if (dump_file && (dump_flags & TDF_DETAILS))
+                               {
+                                 omega_print_geq (dump_file, pb,
+                                                  &(pb->geqs[e2]));
+                                 fprintf (dump_file, "\n");
+                               }
+                           }
+
+                         if (lower_bound_count == 0)
+                           {
+                             dead_eqns[num_dead++] = Ue;
+
+                             if (dump_file && (dump_flags & TDF_DETAILS))
+                               fprintf (dump_file, "Killed %d\n", Ue);
+                           }
+                       }
+
+                   lower_bound_count--;
+                   dead_eqns[num_dead++] = Le;
+
+                   if (dump_file && (dump_flags & TDF_DETAILS))
+                     fprintf (dump_file, "Killed %d\n", Le);
+                 }
+
+             for (e = pb->num_geqs - 1; e >= 0; e--)
+               is_dead[e] = false;
+
+             while (num_dead > 0)
+               is_dead[dead_eqns[--num_dead]] = true;
+
+             for (e = pb->num_geqs - 1; e >= 0; e--)
+               if (is_dead[e])
+                 omega_delete_geq_extra (pb, e, n_vars + 1);
+
+             free (dead_eqns);
+             free (is_dead);
+             continue;
+           }
+       }
+      else
+       {
+         omega_pb rS, iS;
+
+         rS = omega_alloc_problem (0, 0);
+         iS = omega_alloc_problem (0, 0);
+         e2 = 0;
+         possible_easy_int_solution = true;
+
+         for (e = 0; e < pb->num_geqs; e++)
+           if (pb->geqs[e].coef[i] == 0)
+             {
+               omega_copy_eqn (&(rS->geqs[e2]), &pb->geqs[e],
+                               pb->num_vars);
+               omega_copy_eqn (&(iS->geqs[e2]), &pb->geqs[e],
+                               pb->num_vars);
+
+               if (dump_file && (dump_flags & TDF_DETAILS))
+                 {
+                   int t;
+                   fprintf (dump_file, "Copying (%d, %d): ", i,
+                            pb->geqs[e].coef[i]);
+                   omega_print_geq_extra (dump_file, pb, &pb->geqs[e]);
+                   fprintf (dump_file, "\n");
+                   for (t = 0; t <= n_vars + 1; t++)
+                     fprintf (dump_file, "%d ", pb->geqs[e].coef[t]);
+                   fprintf (dump_file, "\n");
+
+                 }
+               e2++;
+               gcc_assert (e2 < OMEGA_MAX_GEQS);
+             }
+
+         for (Le = pb->num_geqs - 1; Le >= 0; Le--)
+           if (pb->geqs[Le].coef[i] > 0)
+             for (Ue = pb->num_geqs - 1; Ue >= 0; Ue--)
+               if (pb->geqs[Ue].coef[i] < 0)
+                 {
+                   int k;
+                   int Lc = pb->geqs[Le].coef[i];
+                   int Uc = -pb->geqs[Ue].coef[i];
+
+                   if (pb->geqs[Le].key != -pb->geqs[Ue].key)
+                     {
+
+                       rS->geqs[e2].touched = iS->geqs[e2].touched = 1;
+
+                       if (dump_file && (dump_flags & TDF_DETAILS))
+                         {
+                           fprintf (dump_file, "---\n");
+                           fprintf (dump_file,
+                                    "Le(Lc) = %d(%d_, Ue(Uc) = %d(%d), gen = %d\n",
+                                    Le, Lc, Ue, Uc, e2);
+                           omega_print_geq_extra (dump_file, pb, &pb->geqs[Le]);
+                           fprintf (dump_file, "\n");
+                           omega_print_geq_extra (dump_file, pb, &pb->geqs[Ue]);
+                           fprintf (dump_file, "\n");
+                         }
+
+                       if (Uc == Lc)
+                         {
+                           for (k = n_vars; k >= 0; k--)
+                             iS->geqs[e2].coef[k] = rS->geqs[e2].coef[k] =
+                               pb->geqs[Ue].coef[k] + pb->geqs[Le].coef[k];
+
+                           iS->geqs[e2].coef[0] -= (Uc - 1);
+                         }
+                       else
+                         {
+                           for (k = n_vars; k >= 0; k--)
+                             iS->geqs[e2].coef[k] = rS->geqs[e2].coef[k] =
+                               check_mul (pb->geqs[Ue].coef[k], Lc) +
+                               check_mul (pb->geqs[Le].coef[k], Uc);
+
+                           iS->geqs[e2].coef[0] -= (Uc - 1) * (Lc - 1);
+                         }
+
+                       if (pb->geqs[Ue].color == omega_red
+                           || pb->geqs[Le].color == omega_red)
+                         iS->geqs[e2].color = rS->geqs[e2].color = omega_red;
+                       else
+                         iS->geqs[e2].color = rS->geqs[e2].color = omega_black;
+
+                       if (dump_file && (dump_flags & TDF_DETAILS))
+                         {
+                           omega_print_geq (dump_file, pb, &(rS->geqs[e2]));
+                           fprintf (dump_file, "\n");
+                         }
+
+                       e2++;
+                       gcc_assert (e2 < OMEGA_MAX_GEQS);
+                     }
+                   else if (pb->geqs[Ue].coef[0] * Lc +
+                            pb->geqs[Le].coef[0] * Uc -
+                            (Uc - 1) * (Lc - 1) < 0)
+                     possible_easy_int_solution = false;
+                 }
+
+         iS->variables_initialized = rS->variables_initialized = true;
+         iS->num_vars = rS->num_vars = pb->num_vars;
+         iS->num_geqs = rS->num_geqs = e2;
+         iS->num_eqs = rS->num_eqs = 0;
+         iS->num_subs = rS->num_subs = pb->num_subs;
+         iS->safe_vars = rS->safe_vars = pb->safe_vars;
+
+         for (e = n_vars; e >= 0; e--)
+           rS->var[e] = pb->var[e];
+
+         for (e = n_vars; e >= 0; e--)
+           iS->var[e] = pb->var[e];
+
+         for (e = pb->num_subs - 1; e >= 0; e--)
+           {
+             omega_copy_eqn (&(rS->subs[e]), &(pb->subs[e]), pb->num_vars);
+             omega_copy_eqn (&(iS->subs[e]), &(pb->subs[e]), pb->num_vars);
+           }
+
+         pb->num_vars++;
+         n_vars = pb->num_vars;
+
+         if (desired_res != omega_true)
+           {
+             if (original_problem == no_problem)
+               {
+                 original_problem = pb;
+                 result = omega_solve_geq (rS, omega_false);
+                 original_problem = no_problem;
+               }
+             else
+               result = omega_solve_geq (rS, omega_false);
+
+             if (result == omega_false)
+               {
+                 free (rS);
+                 free (iS);
+                 return result;
+               }
+
+             if (pb->num_eqs > 0)
+               {
+                 /* An equality constraint must have been found */
+                 free (rS);
+                 free (iS);
+                 return omega_solve_problem (pb, desired_res);
+               }
+           }
+
+         if (desired_res != omega_false)
+           {
+             int j;
+             int lower_bounds = 0;
+             int *lower_bound = XNEWVEC (int, OMEGA_MAX_GEQS);
+
+             if (possible_easy_int_solution)
+               {
+                 conservative++;
+                 result = omega_solve_geq (iS, desired_res);
+                 conservative--;
+
+                 if (result != omega_false)
+                   {
+                     free (rS);
+                     free (iS);
+                     free (lower_bound);
+                     return result;
+                   }
+               }
+
+             if (!exact && best_parallel_eqn >= 0
+                 && parallel_difference <= max_splinters)
+               {
+                 free (rS);
+                 free (iS);
+                 free (lower_bound);
+                 return parallel_splinter (pb, best_parallel_eqn,
+                                           parallel_difference,
+                                           desired_res);
+               }
+
+             if (dump_file && (dump_flags & TDF_DETAILS))
+               fprintf (dump_file, "have to do exact analysis\n");
+
+             conservative++;
+
+             for (e = 0; e < pb->num_geqs; e++)
+               if (pb->geqs[e].coef[i] > 1)
+                 lower_bound[lower_bounds++] = e;
+
+             /* Sort array LOWER_BOUND.  */
+             for (j = 0; j < lower_bounds; j++)
+               {
+                 int k, smallest = j;
+
+                 for (k = j + 1; k < lower_bounds; k++)
+                   if (pb->geqs[lower_bound[smallest]].coef[i] >
+                       pb->geqs[lower_bound[k]].coef[i])
+                     smallest = k;
+
+                 k = lower_bound[smallest];
+                 lower_bound[smallest] = lower_bound[j];
+                 lower_bound[j] = k;
+               }
+
+             if (dump_file && (dump_flags & TDF_DETAILS))
+               {
+                 fprintf (dump_file, "lower bound coeeficients = ");
+
+                 for (j = 0; j < lower_bounds; j++)
+                   fprintf (dump_file, " %d",
+                            pb->geqs[lower_bound[j]].coef[i]);
+
+                 fprintf (dump_file, "\n");
+               }
+
+             for (j = 0; j < lower_bounds; j++)
+               {
+                 int max_incr;
+                 int c;
+                 int worst_lower_bound_constant = -minC;
+
+                 e = lower_bound[j];
+                 max_incr = (((pb->geqs[e].coef[i] - 1) *
+                              (worst_lower_bound_constant - 1) - 1)
+                             / worst_lower_bound_constant);
+                 /* max_incr += 2; */
+
+                 if (dump_file && (dump_flags & TDF_DETAILS))
+                   {
+                     fprintf (dump_file, "for equation ");
+                     omega_print_geq (dump_file, pb, &pb->geqs[e]);
+                     fprintf (dump_file,
+                              "\ntry decrements from 0 to %d\n",
+                              max_incr);
+                     omega_print_problem (dump_file, pb);
+                   }
+
+                 if (max_incr > 50 && !smoothed
+                     && smooth_weird_equations (pb))
+                   {
+                     conservative--;
+                     free (rS);
+                     free (iS);
+                     smoothed = true;
+                     goto solve_geq_start;
+                   }
+
+                 omega_copy_eqn (&pb->eqs[0], &pb->geqs[e],
+                                 pb->num_vars);
+                 pb->eqs[0].color = omega_black;
+                 omega_init_eqn_zero (&pb->geqs[e], pb->num_vars);
+                 pb->geqs[e].touched = 1;
+                 pb->num_eqs = 1;
+
+                 for (c = max_incr; c >= 0; c--)
+                   {
+                     if (dump_file && (dump_flags & TDF_DETAILS))
+                       {
+                         fprintf (dump_file,
+                                  "trying next decrement of %d\n",
+                                  max_incr - c);
+                         omega_print_problem (dump_file, pb);
+                       }
+
+                     omega_copy_problem (rS, pb);
+
+                     if (dump_file && (dump_flags & TDF_DETAILS))
+                       omega_print_problem (dump_file, rS);
+
+                     result = omega_solve_problem (rS, desired_res);
+
+                     if (result == omega_true)
+                       {
+                         free (rS);
+                         free (iS);
+                         free (lower_bound);
+                         conservative--;
+                         return omega_true;
+                       }
+
+                     pb->eqs[0].coef[0]--;
+                   }
+
+                 if (j + 1 < lower_bounds)
+                   {
+                     pb->num_eqs = 0;
+                     omega_copy_eqn (&pb->geqs[e], &pb->eqs[0],
+                                     pb->num_vars);
+                     pb->geqs[e].touched = 1;
+                     pb->geqs[e].color = omega_black;
+                     omega_copy_problem (rS, pb);
+
+                     if (dump_file && (dump_flags & TDF_DETAILS))
+                       fprintf (dump_file,
+                                "exhausted lower bound, "
+                                "checking if still feasible ");
+
+                     result = omega_solve_problem (rS, omega_false);
+
+                     if (result == omega_false)
+                       break;
+                   }
+               }
+
+             if (dump_file && (dump_flags & TDF_DETAILS))
+               fprintf (dump_file, "fall-off the end\n");
+
+             free (rS);
+             free (iS);
+             free (lower_bound);
+             conservative--;
+             return omega_false;
+           }
+
+         free (rS);
+         free (iS);
+       }
+      return omega_unknown;
+    } while (eliminate_again);
+  } while (1);
+}
+
+/* Because the omega solver is recursive, this counter limits the
+   recursion depth.  */
+static int omega_solve_depth = 0;
+
+/* Return omega_true when the problem PB has a solution following the
+   DESIRED_RES.  */
+
+enum omega_result
+omega_solve_problem (omega_pb pb, enum omega_result desired_res)
+{
+  enum omega_result result;
+
+  gcc_assert (pb->num_vars >= pb->safe_vars);
+  omega_solve_depth++;
+
+  if (desired_res != omega_simplify)
+    pb->safe_vars = 0;
+
+  if (omega_solve_depth > 50)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+       {
+         fprintf (dump_file, 
+                  "Solve depth = %d, in_approximate_mode = %d, aborting\n",
+                  omega_solve_depth, in_approximate_mode);
+         omega_print_problem (dump_file, pb);
+       }
+      gcc_assert (0);
+    }
+
+  if (omega_solve_eq (pb, desired_res) == omega_false)
+    {
+      omega_solve_depth--;
+      return omega_false;
+    }
+
+  if (in_approximate_mode && !pb->num_geqs)
+    {
+      result = omega_true;
+      pb->num_vars = pb->safe_vars;
+      omega_problem_reduced (pb);
+    }
+  else
+    result = omega_solve_geq (pb, desired_res);
+
+  omega_solve_depth--;
+
+  if (!omega_reduce_with_subs)
+    {
+      resurrect_subs (pb);
+      gcc_assert (please_no_equalities_in_simplified_problems 
+                 || !result || pb->num_subs == 0);
+    }
+
+  return result;
+}
+
+/* Return true if red equations constrain the set of possible solutions.
+   We assume that there are solutions to the black equations by
+   themselves, so if there is no solution to the combined problem, we
+   return true.  */
+
+bool
+omega_problem_has_red_equations (omega_pb pb)
+{
+  bool result;
+  int e;
+  int i;
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    {
+      fprintf (dump_file, "Checking for red equations:\n");
+      omega_print_problem (dump_file, pb);
+    }
+
+  please_no_equalities_in_simplified_problems++;
+  may_be_red++;
+
+  if (omega_single_result)
+    return_single_result++;
+
+  create_color = true;
+  result = (omega_simplify_problem (pb) == omega_false);
+
+  if (omega_single_result)
+    return_single_result--;
+
+  may_be_red--;
+  please_no_equalities_in_simplified_problems--;
+
+  if (result)
+    {
+      if (dump_file && (dump_flags & TDF_DETAILS))
+       fprintf (dump_file, "Gist is FALSE\n");
+
+      pb->num_subs = 0;
+      pb->num_geqs = 0;
+      pb->num_eqs = 1;
+      pb->eqs[0].color = omega_red;
+
+      for (i = pb->num_vars; i > 0; i--)
+       pb->eqs[0].coef[i] = 0;
+
+      pb->eqs[0].coef[0] = 1;
+      return true;
+    }
+
+  free_red_eliminations (pb);
+  gcc_assert (pb->num_eqs == 0);
+
+  for (e = pb->num_geqs - 1; e >= 0; e--)
+    if (pb->geqs[e].color == omega_red)
+      result = true;
+
+  if (!result)
+    return false;
+
+  for (i = pb->safe_vars; i >= 1; i--)
+    {
+      int ub = 0;
+      int lb = 0;
+
+      for (e = pb->num_geqs - 1; e >= 0; e--)
+       {
+         if (pb->geqs[e].coef[i])
+           {
+             if (pb->geqs[e].coef[i] > 0)
+               lb |= (1 + (pb->geqs[e].color == omega_red ? 1 : 0));
+
+             else
+               ub |= (1 + (pb->geqs[e].color == omega_red ? 1 : 0));
+           }
+       }
+
+      if (ub == 2 || lb == 2)
+       {
+
+         if (dump_file && (dump_flags & TDF_DETAILS))
+           fprintf (dump_file, "checks for upper/lower bounds worked!\n");
+
+         if (!omega_reduce_with_subs)
+           {
+             resurrect_subs (pb);
+             gcc_assert (pb->num_subs == 0);
+           }
+
+         return true;
+       }
+    }
+
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    fprintf (dump_file,
+            "*** Doing potentially expensive elimination tests "
+            "for red equations\n");
+
+  please_no_equalities_in_simplified_problems++;
+  omega_eliminate_red (pb, true);
+  please_no_equalities_in_simplified_problems--;
+
+  result = false;
+  gcc_assert (pb->num_eqs == 0);
+
+  for (e = pb->num_geqs - 1; e >= 0; e--)
+    if (pb->geqs[e].color == omega_red)
+      result = true;
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    {
+      if (!result)
+       fprintf (dump_file,
+                "******************** Redudant Red Equations eliminated!!\n");
+      else
+       fprintf (dump_file,
+                "******************** Red Equations remain\n");
+
+      omega_print_problem (dump_file, pb);
+    }
+
+  if (!omega_reduce_with_subs)
+    {
+      normalize_return_type r;
+
+      resurrect_subs (pb);
+      r = normalize_omega_problem (pb);
+      gcc_assert (r != normalize_false);
+
+      coalesce (pb);
+      cleanout_wildcards (pb);
+      gcc_assert (pb->num_subs == 0);
+    }
+
+  return result;
+}
+
+/* Calls omega_simplify_problem in approximate mode.  */
+
+enum omega_result
+omega_simplify_approximate (omega_pb pb)
+{
+  enum omega_result result;
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    fprintf (dump_file, "(Entering approximate mode\n");
+
+  in_approximate_mode = true;
+  result = omega_simplify_problem (pb);
+  in_approximate_mode = false;
+
+  gcc_assert (pb->num_vars == pb->safe_vars);
+  if (!omega_reduce_with_subs)
+    gcc_assert (pb->num_subs == 0);
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    fprintf (dump_file, "Leaving approximate mode)\n");
+
+  return result;
+}
+
+
+/* Simplifies problem PB by eliminating redundant constraints and
+   reducing the constraints system to a minimal form.  Returns
+   omega_true when the problem was successfully reduced, omega_unknown
+   when the solver is unable to determine an answer.  */
+
+enum omega_result
+omega_simplify_problem (omega_pb pb)
+{
+  int i;
+
+  omega_found_reduction = omega_false;
+
+  if (!pb->variables_initialized)
+    omega_initialize_variables (pb);
+
+  if (next_key * 3 > MAX_KEYS)
+    {
+      int e;
+
+      hash_version++;
+      next_key = OMEGA_MAX_VARS + 1;
+
+      for (e = pb->num_geqs - 1; e >= 0; e--)
+       pb->geqs[e].touched = 1;
+
+      for (i = 0; i < HASH_TABLE_SIZE; i++)
+       hash_master[i].touched = -1;
+
+      pb->hash_version = hash_version;
+    }
+
+  else if (pb->hash_version != hash_version)
+    {
+      int e;
+
+      for (e = pb->num_geqs - 1; e >= 0; e--)
+       pb->geqs[e].touched = 1;
+
+      pb->hash_version = hash_version;
+    }
+
+  if (pb->num_vars > pb->num_eqs + 3 * pb->safe_vars)
+    omega_free_eliminations (pb, pb->safe_vars);
+
+  if (!may_be_red && pb->num_subs == 0 && pb->safe_vars == 0)
+    {
+      omega_found_reduction = omega_solve_problem (pb, omega_unknown);
+
+      if (omega_found_reduction != omega_false
+         && !return_single_result)
+       {
+         pb->num_geqs = 0;
+         pb->num_eqs = 0;
+         (*omega_when_reduced) (pb);
+       }
+
+      return omega_found_reduction;
+    }
+
+  omega_solve_problem (pb, omega_simplify);
+
+  if (omega_found_reduction != omega_false)
+    {
+      for (i = 1; omega_safe_var_p (pb, i); i++)
+       pb->forwarding_address[pb->var[i]] = i;
+
+      for (i = 0; i < pb->num_subs; i++)
+       pb->forwarding_address[pb->subs[i].key] = -i - 1;
+    }
+
+  if (!omega_reduce_with_subs)
+    gcc_assert (please_no_equalities_in_simplified_problems
+               || omega_found_reduction == omega_false
+               || pb->num_subs == 0);
+
+  return omega_found_reduction;
+}
+
+/* Make variable VAR unprotected: it then can be eliminated.  */
+
+void
+omega_unprotect_variable (omega_pb pb, int var)
+{
+  int e, idx;
+  idx = pb->forwarding_address[var];
+
+  if (idx < 0)
+    {
+      idx = -1 - idx;
+      pb->num_subs--;
+
+      if (idx < pb->num_subs)
+       {
+         omega_copy_eqn (&pb->subs[idx], &pb->subs[pb->num_subs],
+                         pb->num_vars);
+         pb->forwarding_address[pb->subs[idx].key] = -idx - 1;
+       }
+    }
+  else
+    {
+      int *bring_to_life = XNEWVEC (int, OMEGA_MAX_VARS);
+      int e2;
+
+      for (e = pb->num_subs - 1; e >= 0; e--)
+       bring_to_life[e] = (pb->subs[e].coef[idx] != 0);
+
+      for (e2 = pb->num_subs - 1; e2 >= 0; e2--)
+       if (bring_to_life[e2])
+         {
+           pb->num_vars++;
+           pb->safe_vars++;
+
+           if (pb->safe_vars < pb->num_vars)
+             {
+               for (e = pb->num_geqs - 1; e >= 0; e--)
+                 {
+                   pb->geqs[e].coef[pb->num_vars] = 
+                     pb->geqs[e].coef[pb->safe_vars];
+
+                   pb->geqs[e].coef[pb->safe_vars] = 0;
+                 }
+
+               for (e = pb->num_eqs - 1; e >= 0; e--)
+                 {
+                   pb->eqs[e].coef[pb->num_vars] =
+                     pb->eqs[e].coef[pb->safe_vars];
+
+                   pb->eqs[e].coef[pb->safe_vars] = 0;
+                 }
+
+               for (e = pb->num_subs - 1; e >= 0; e--)
+                 {
+                   pb->subs[e].coef[pb->num_vars] =
+                     pb->subs[e].coef[pb->safe_vars];
+
+                   pb->subs[e].coef[pb->safe_vars] = 0;
+                 }
+
+               pb->var[pb->num_vars] = pb->var[pb->safe_vars];
+               pb->forwarding_address[pb->var[pb->num_vars]] =
+                 pb->num_vars;
+             }
+           else
+             {
+               for (e = pb->num_geqs - 1; e >= 0; e--)
+                 pb->geqs[e].coef[pb->safe_vars] = 0;
+
+               for (e = pb->num_eqs - 1; e >= 0; e--)
+                 pb->eqs[e].coef[pb->safe_vars] = 0;
+
+               for (e = pb->num_subs - 1; e >= 0; e--)
+                 pb->subs[e].coef[pb->safe_vars] = 0;
+             }
+
+           pb->var[pb->safe_vars] = pb->subs[e2].key;
+           pb->forwarding_address[pb->subs[e2].key] = pb->safe_vars;
+
+           omega_copy_eqn (&(pb->eqs[pb->num_eqs]), &(pb->subs[e2]),
+                           pb->num_vars);
+           pb->eqs[pb->num_eqs++].coef[pb->safe_vars] = -1;
+           gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
+
+           if (e2 < pb->num_subs - 1)
+             omega_copy_eqn (&(pb->subs[e2]), &(pb->subs[pb->num_subs - 1]),
+                             pb->num_vars);
+
+           pb->num_subs--;
+         }
+
+      omega_unprotect_1 (pb, &idx, NULL);
+      free (bring_to_life);
+    }
+
+  chain_unprotect (pb);
+}
+
+/* Unprotects VAR and simplifies PB.  */
+
+enum omega_result
+omega_constrain_variable_sign (omega_pb pb, enum omega_eqn_color color,
+                              int var, int sign)
+{
+  int n_vars = pb->num_vars;
+  int e, j;
+  int k = pb->forwarding_address[var];
+
+  if (k < 0)
+    {
+      k = -1 - k;
+
+      if (sign != 0)
+       {
+         e = pb->num_geqs++;
+         omega_copy_eqn (&pb->geqs[e], &pb->subs[k], pb->num_vars);
+
+         for (j = 0; j <= n_vars; j++)
+           pb->geqs[e].coef[j] *= sign;
+
+         pb->geqs[e].coef[0]--;
+         pb->geqs[e].touched = 1;
+         pb->geqs[e].color = color;
+       }
+      else
+       {
+         e = pb->num_eqs++;
+         gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
+         omega_copy_eqn (&pb->eqs[e], &pb->subs[k], pb->num_vars);
+         pb->eqs[e].color = color;
+       }
+    }
+  else if (sign != 0)
+    {
+      e = pb->num_geqs++;
+      omega_init_eqn_zero (&pb->geqs[e], pb->num_vars);
+      pb->geqs[e].coef[k] = sign;
+      pb->geqs[e].coef[0] = -1;
+      pb->geqs[e].touched = 1;
+      pb->geqs[e].color = color;
+    }
+  else
+    {
+      e = pb->num_eqs++;
+      gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
+      omega_init_eqn_zero (&pb->eqs[e], pb->num_vars);
+      pb->eqs[e].coef[k] = 1;
+      pb->eqs[e].color = color;
+    }
+
+  omega_unprotect_variable (pb, var);
+  return omega_simplify_problem (pb);
+}
+
+/* Add an equation "VAR = VALUE" with COLOR to PB.  */
+
+void
+omega_constrain_variable_value (omega_pb pb, enum omega_eqn_color color,
+                               int var, int value)
+{
+  int e;
+  int k = pb->forwarding_address[var];
+
+  if (k < 0)
+    {
+      k = -1 - k;
+      e = pb->num_eqs++;
+      gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
+      omega_copy_eqn (&pb->eqs[e], &pb->subs[k], pb->num_vars);
+      pb->eqs[e].coef[0] -= value;
+    }
+  else
+    {
+      e = pb->num_eqs++;
+      omega_init_eqn_zero (&pb->eqs[e], pb->num_vars);
+      pb->eqs[e].coef[k] = 1;
+      pb->eqs[e].coef[0] = -value;
+    }
+
+  pb->eqs[e].color = color;
+}
+
+/* Return false when the upper and lower bounds are not coupled.
+   Initialize the bounds LOWER_BOUND and UPPER_BOUND for the values of
+   variable I.  */
+
+bool
+omega_query_variable (omega_pb pb, int i, int *lower_bound, int *upper_bound)
+{
+  int n_vars = pb->num_vars;
+  int e, j;
+  bool is_simple;
+  bool coupled = false;
+
+  *lower_bound = neg_infinity;
+  *upper_bound = pos_infinity;
+  i = pb->forwarding_address[i];
+
+  if (i < 0)
+    {
+      i = -i - 1;
+
+      for (j = 1; j <= n_vars; j++)
+       if (pb->subs[i].coef[j] != 0)
+         return true;
+
+      *upper_bound = *lower_bound = pb->subs[i].coef[0];
+      return false;
+    }
+
+  for (e = pb->num_subs - 1; e >= 0; e--)
+    if (pb->subs[e].coef[i] != 0)
+      coupled = true;
+
+  for (e = pb->num_eqs - 1; e >= 0; e--)
+    if (pb->eqs[e].coef[i] != 0)
+      {
+       is_simple = true;
+
+       for (j = 1; j <= n_vars; j++)
+         if (i != j && pb->eqs[e].coef[j] != 0)
+           {
+             is_simple = false;
+             coupled = true;
+             break;
+           }
+
+       if (!is_simple)
+         continue;
+       else
+         {
+           *lower_bound = *upper_bound = 
+             -pb->eqs[e].coef[i] * pb->eqs[e].coef[0];
+           return false;
+         }
+      }
+
+  for (e = pb->num_geqs - 1; e >= 0; e--)
+    if (pb->geqs[e].coef[i] != 0)
+      {
+       if (pb->geqs[e].key == i)
+         *lower_bound = MAX (*lower_bound, -pb->geqs[e].coef[0]);
+
+       else if (pb->geqs[e].key == -i)
+         *upper_bound = MIN (*upper_bound, pb->geqs[e].coef[0]);
+
+       else
+         coupled = true;
+      }
+
+  return coupled;
+}
+
+/* Sets the lower bound L and upper bound U for the values of variable
+   I, and sets COULD_BE_ZERO to true if variable I might take value
+   zero.  LOWER_BOUND and UPPER_BOUND are bounds on the values of
+   variable I.  */
+
+static void
+query_coupled_variable (omega_pb pb, int i, int *l, int *u,
+                       bool *could_be_zero, int lower_bound, int upper_bound)
+{
+  int e, b1, b2;
+  eqn eqn;
+  int sign;
+  int v;
+
+  /* Preconditions.  */
+  gcc_assert (abs (pb->forwarding_address[i]) == 1
+             && pb->num_vars + pb->num_subs == 2
+             && pb->num_eqs + pb->num_subs == 1);
+
+  /* Define variable I in terms of variable V.  */
+  if (pb->forwarding_address[i] == -1)
+    {
+      eqn = &pb->subs[0];
+      sign = 1;
+      v = 1;
+    }
+  else
+    {
+      eqn = &pb->eqs[0];
+      sign = -eqn->coef[1];
+      v = 2;
+    }
+
+  for (e = pb->num_geqs - 1; e >= 0; e--)
+    if (pb->geqs[e].coef[v] != 0)
+      {
+       if (pb->geqs[e].coef[v] == 1)
+         lower_bound = MAX (lower_bound, -pb->geqs[e].coef[0]);
+
+       else
+         upper_bound = MIN (upper_bound, pb->geqs[e].coef[0]);
+      }
+
+  if (lower_bound > upper_bound)
+    {
+      *l = pos_infinity;
+      *u = neg_infinity;
+      *could_be_zero = 0;
+      return;
+    }
+
+  if (lower_bound == neg_infinity)
+    {
+      if (eqn->coef[v] > 0)
+       b1 = sign * neg_infinity;
+
+      else
+       b1 = -sign * neg_infinity;
+    }
+  else
+    b1 = sign * (eqn->coef[0] + eqn->coef[v] * lower_bound);
+
+  if (upper_bound == pos_infinity)
+    {
+      if (eqn->coef[v] > 0)
+       b2 = sign * pos_infinity;
+
+      else
+       b2 = -sign * pos_infinity;
+    }
+  else
+    b2 = sign * (eqn->coef[0] + eqn->coef[v] * upper_bound);
+
+  *l = MAX (*l, b1 <= b2 ? b1 : b2);
+  *u = MIN (*u, b1 <= b2 ? b2 : b1);
+
+  *could_be_zero = (*l <= 0 && 0 <= *u
+                   && int_mod (eqn->coef[0], abs (eqn->coef[v])) == 0);
+}
+
+/* Return false when a lower bound L and an upper bound U for variable
+   I in problem PB have been initialized.  */
+
+bool
+omega_query_variable_bounds (omega_pb pb, int i, int *l, int *u)
+{
+  *l = neg_infinity;
+  *u = pos_infinity;
+
+  if (!omega_query_variable (pb, i, l, u)
+      || (pb->num_vars == 1 && pb->forwarding_address[i] == 1))
+    return false;
+
+  if (abs (pb->forwarding_address[i]) == 1 
+      && pb->num_vars + pb->num_subs == 2
+      && pb->num_eqs + pb->num_subs == 1)
+    {
+      bool could_be_zero;
+      query_coupled_variable (pb, i, l, u, &could_be_zero, neg_infinity,
+                             pos_infinity);
+      return false;
+    }
+
+  return true;
+}
+
+/* For problem PB, return an integer that represents the classic data
+   dependence direction in function of the DD_LT, DD_EQ and DD_GT bit
+   masks that are added to the result.  When DIST_KNOWN is true, DIST
+   is set to the classic data dependence distance.  LOWER_BOUND and
+   UPPER_BOUND are bounds on the value of variable I, for example, it
+   is possible to narrow the iteration domain with safe approximations
+   of loop counts, and thus discard some data dependences that cannot
+   occur.  */
+
+int
+omega_query_variable_signs (omega_pb pb, int i, int dd_lt,
+                           int dd_eq, int dd_gt, int lower_bound,
+                           int upper_bound, bool *dist_known, int *dist)
+{
+  int result;
+  int l, u;
+  bool could_be_zero;
+
+  l = neg_infinity;
+  u = pos_infinity;
+
+  omega_query_variable (pb, i, &l, &u);
+  query_coupled_variable (pb, i, &l, &u, &could_be_zero, lower_bound,
+                         upper_bound);
+  result = 0;
+
+  if (l < 0)
+    result |= dd_gt;
+
+  if (u > 0)
+    result |= dd_lt;
+
+  if (could_be_zero)
+    result |= dd_eq;
+
+  if (l == u)
+    {
+      *dist_known = true;
+      *dist = l;
+    }
+  else
+    *dist_known = false;
+
+  return result;
+}
+
+/* Initialize PB as an Omega problem with NVARS variables and NPROT
+   safe variables.  Safe variables are not eliminated during the
+   Fourier-Motzkin elimination.  Safe variables are all those
+   variables that are placed at the beginning of the array of
+   variables: P->var[0, ..., NPROT - 1].  */
+
+omega_pb
+omega_alloc_problem (int nvars, int nprot)
+{
+  omega_pb pb;
+
+  gcc_assert (nvars <= OMEGA_MAX_VARS);
+  omega_initialize ();
+
+  /* Allocate and initialize PB.  */
+  pb = XCNEW (struct omega_pb);
+  pb->var = XCNEWVEC (int, OMEGA_MAX_VARS + 2);
+  pb->forwarding_address = XCNEWVEC (int, OMEGA_MAX_VARS + 2);
+  pb->geqs = omega_alloc_eqns (0, OMEGA_MAX_GEQS);
+  pb->eqs = omega_alloc_eqns (0, OMEGA_MAX_EQS);
+  pb->subs = omega_alloc_eqns (0, OMEGA_MAX_VARS + 1);
+
+  pb->hash_version = hash_version;
+  pb->num_vars = nvars;
+  pb->safe_vars = nprot;
+  pb->variables_initialized = false;
+  pb->variables_freed = false;
+  pb->num_eqs = 0;
+  pb->num_geqs = 0;
+  pb->num_subs = 0;
+  return pb;
+}
+
+/* Keeps the state of the initialization.  */
+static bool omega_initialized = false;
+
+/* Initialization of the Omega solver.  */
+
+void
+omega_initialize (void)
+{
+  int i;
+
+  if (omega_initialized)
+    return;
+
+  next_wild_card = 0;
+  next_key = OMEGA_MAX_VARS + 1;
+  packing = XCNEWVEC (int, OMEGA_MAX_VARS);
+  fast_lookup = XCNEWVEC (int, MAX_KEYS * 2);
+  fast_lookup_red = XCNEWVEC (int, MAX_KEYS * 2);
+  hash_master = omega_alloc_eqns (0, HASH_TABLE_SIZE);
+
+  for (i = 0; i < HASH_TABLE_SIZE; i++)
+    hash_master[i].touched = -1;
+
+  sprintf (wild_name[0], "1");
+  sprintf (wild_name[1], "a");
+  sprintf (wild_name[2], "b");
+  sprintf (wild_name[3], "c");
+  sprintf (wild_name[4], "d");
+  sprintf (wild_name[5], "e");
+  sprintf (wild_name[6], "f");
+  sprintf (wild_name[7], "g");
+  sprintf (wild_name[8], "h");
+  sprintf (wild_name[9], "i");
+  sprintf (wild_name[10], "j");
+  sprintf (wild_name[11], "k");
+  sprintf (wild_name[12], "l");
+  sprintf (wild_name[13], "m");
+  sprintf (wild_name[14], "n");
+  sprintf (wild_name[15], "o");
+  sprintf (wild_name[16], "p");
+  sprintf (wild_name[17], "q");
+  sprintf (wild_name[18], "r");
+  sprintf (wild_name[19], "s");
+  sprintf (wild_name[20], "t");
+  sprintf (wild_name[40 - 1], "alpha");
+  sprintf (wild_name[40 - 2], "beta");
+  sprintf (wild_name[40 - 3], "gamma");
+  sprintf (wild_name[40 - 4], "delta");
+  sprintf (wild_name[40 - 5], "tau");
+  sprintf (wild_name[40 - 6], "sigma");
+  sprintf (wild_name[40 - 7], "chi");
+  sprintf (wild_name[40 - 8], "omega");
+  sprintf (wild_name[40 - 9], "pi");
+  sprintf (wild_name[40 - 10], "ni");
+  sprintf (wild_name[40 - 11], "Alpha");
+  sprintf (wild_name[40 - 12], "Beta");
+  sprintf (wild_name[40 - 13], "Gamma");
+  sprintf (wild_name[40 - 14], "Delta");
+  sprintf (wild_name[40 - 15], "Tau");
+  sprintf (wild_name[40 - 16], "Sigma");
+  sprintf (wild_name[40 - 17], "Chi");
+  sprintf (wild_name[40 - 18], "Omega");
+  sprintf (wild_name[40 - 19], "xxx");
+
+  omega_initialized = true;
+}
diff --git a/gcc/omega.h b/gcc/omega.h
new file mode 100644 (file)
index 0000000..c050a6e
--- /dev/null
@@ -0,0 +1,340 @@
+/* Source code for an implementation of the Omega test, a integer 
+   programming algorithm for dependence analysis, by William Pugh, 
+   appeared in Supercomputing '91 and CACM Aug 92.
+
+   This code has no license restrictions, and is considered public
+   domain.
+
+   Changes copyright (C) 2005, 2006, 2007 Free Software Foundation, Inc.
+   Contributed by Sebastian Pop <sebastian.pop@inria.fr>
+
+This file is part of GCC.
+
+GCC is free software; you can redistribute it and/or modify it under
+the terms of the GNU General Public License as published by the Free
+Software Foundation; either version 2, or (at your option) any later
+version.
+
+GCC is distributed in the hope that it will be useful, but WITHOUT ANY
+WARRANTY; without even the implied warranty of MERCHANTABILITY or
+FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
+for more details.
+
+You should have received a copy of the GNU General Public License
+along with GCC; see the file COPYING.  If not, write to the Free
+Software Foundation, 59 Temple Place - Suite 330, Boston, MA
+02111-1307, USA.  */
+
+#include "config.h"
+#include "params.h"
+
+#ifndef GCC_OMEGA_H
+#define GCC_OMEGA_H
+
+#define OMEGA_MAX_VARS PARAM_VALUE (PARAM_OMEGA_MAX_VARS)
+#define OMEGA_MAX_GEQS PARAM_VALUE (PARAM_OMEGA_MAX_GEQS)
+#define OMEGA_MAX_EQS PARAM_VALUE (PARAM_OMEGA_MAX_EQS)
+
+#define pos_infinity (0x7ffffff)
+#define neg_infinity (-0x7ffffff)
+
+/* Results of the Omega solver.  */
+enum omega_result {
+  omega_false = 0,
+  omega_true = 1,
+
+  /* Value returned when the solver is unable to determine an
+     answer.  */
+  omega_unknown = 2,
+
+  /* Value used for asking the solver to simplify the system.  */
+  omega_simplify = 3
+};
+
+/* Values used for labeling equations.  Private (not used outside the
+   solver).  */
+enum omega_eqn_color { 
+  omega_black = 0,
+  omega_red = 1
+};
+
+/* Structure for equations.  */
+typedef struct eqn
+{
+  int key;
+  int touched;
+  enum omega_eqn_color color;
+
+  /* Array of coefficients for the equation.  The layout of the data
+     is as follows: coef[0] is the constant, coef[i] for 1 <= i <=
+     OMEGA_MAX_VARS, are the coefficients for each dimension.  Examples:
+     the equation 0 = 9 + x + 0y + 5z is encoded as [9 1 0 5], the
+     inequality 0 <= -8 + x + 2y + 3z is encoded as [-8 1 2 3].  */
+  int *coef;
+} *eqn;
+
+typedef struct omega_pb
+{
+  /* The number of variables in the system of equations.  */
+  int num_vars;
+  
+  /* Safe variables are not eliminated during the Fourier-Motzkin
+     simplification of the system.  Safe variables are all those
+     variables that are placed at the beginning of the array of
+     variables: PB->var[1, ..., SAFE_VARS].  PB->var[0] is not used,
+     as PB->eqs[x]->coef[0] represents the constant of the equation.  */
+  int safe_vars;
+
+  /* Number of elements in eqs[].  */
+  int num_eqs;
+  /* Number of elements in geqs[].  */
+  int num_geqs;
+  /* Number of elements in subs[].  */
+  int num_subs;
+
+  int hash_version;
+  bool variables_initialized;
+  bool variables_freed;
+
+  /* Index or name of variables.  Negative integers are reserved for
+     wildcard variables.  Maps the index of variables in the original
+     problem to the new index of the variable.  The index for a
+     variable in the coef array of an equation can change as some
+     variables are eliminated.  */
+  int *var;
+
+  int *forwarding_address;
+
+  /* Inequalities in the system of constraints.  */
+  eqn geqs;
+
+  /* Equations in the system of constraints.  */
+  eqn eqs;
+
+  /* A map of substituted variables.  */
+  eqn subs;
+} *omega_pb;
+
+extern void omega_initialize (void);
+extern omega_pb omega_alloc_problem (int, int);
+extern enum omega_result omega_solve_problem (omega_pb, enum omega_result);
+extern enum omega_result omega_simplify_problem (omega_pb);
+extern enum omega_result omega_simplify_approximate (omega_pb);
+extern enum omega_result omega_constrain_variable_sign (omega_pb,
+                                                       enum omega_eqn_color,
+                                                       int, int);
+extern void debug_omega_problem (omega_pb);
+extern void omega_print_problem (FILE *, omega_pb);
+extern void omega_print_red_equations (FILE *, omega_pb);
+extern int omega_count_red_equations (omega_pb);
+extern void omega_pretty_print_problem (FILE *, omega_pb);
+extern void omega_unprotect_variable (omega_pb, int var);
+extern void omega_negate_geq (omega_pb, int);
+extern void omega_convert_eq_to_geqs (omega_pb, int eq);
+extern void omega_print_eqn (FILE *, omega_pb, eqn, bool, int);
+extern bool omega_problem_has_red_equations (omega_pb);
+extern enum omega_result omega_eliminate_redundant (omega_pb, bool);
+extern void omega_eliminate_red (omega_pb, bool);
+extern void omega_constrain_variable_value (omega_pb, enum omega_eqn_color,
+                                           int, int);
+extern bool omega_query_variable (omega_pb, int, int *, int *);
+extern int omega_query_variable_signs (omega_pb, int, int, int, int,
+                                      int, int, bool *, int *);
+extern bool omega_query_variable_bounds (omega_pb, int, int *, int *);
+extern void (*omega_when_reduced) (omega_pb);
+extern void omega_no_procedure (omega_pb);
+
+/* Return true when variable I in problem PB is a wildcard.  */
+
+static inline bool
+omega_wildcard_p (omega_pb pb, int i)
+{
+  return (pb->var[i] < 0);
+}
+
+/* Return true when variable I in problem PB is a safe variable.  */
+
+static inline bool
+omega_safe_var_p (omega_pb pb, int i)
+{
+  /* The constant of an equation is not a variable.  */
+  gcc_assert (0 < i);
+  return (i <= pb->safe_vars);
+}
+
+/* Print to FILE equality E from PB.  */
+
+static inline void
+omega_print_eq (FILE *file, omega_pb pb, eqn e)
+{
+  omega_print_eqn (file, pb, e, false, 0);
+}
+
+/* Print to FILE inequality E from PB.  */
+
+static inline void
+omega_print_geq (FILE *file, omega_pb pb, eqn e)
+{
+  omega_print_eqn (file, pb, e, true, 0);
+}
+
+/* Print to FILE inequality E from PB.  */
+
+static inline void
+omega_print_geq_extra (FILE *file, omega_pb pb, eqn e)
+{
+  omega_print_eqn (file, pb, e, true, 1);
+}
+
+/* E1 = E2, make a copy of E2 into E1.  Equations contain S variables.  */
+
+static inline void
+omega_copy_eqn (eqn e1, eqn e2, int s)
+{
+  e1->key = e2->key;
+  e1->touched = e2->touched;
+  e1->color = e2->color;
+
+  memcpy (e1->coef, e2->coef, (s + 1) * sizeof (int));
+}
+
+/* Intialize E = 0.  Equation E contains S variables.  */
+
+static inline void
+omega_init_eqn_zero (eqn e, int s)
+{
+  e->key = 0;
+  e->touched = 0;
+  e->color = omega_black;
+
+  memset (e->coef, 0, (s + 1) * sizeof (int));
+}
+
+/* Allocate N equations with S variables.  */
+
+static inline eqn
+omega_alloc_eqns (int s, int n)
+{
+  int i;
+  eqn res = (eqn) (xcalloc (n, sizeof (struct eqn)));
+
+  for (i = n - 1; i >= 0; i--)
+    {
+      res[i].coef = (int *) (xcalloc (OMEGA_MAX_VARS + 1, sizeof (int)));
+      omega_init_eqn_zero (&res[i], s);
+    }
+
+  return res;
+}
+
+/* Free N equations from array EQ.  */
+
+static inline void
+omega_free_eqns (eqn eq, int n)
+{
+  int i;
+
+  for (i = n - 1; i >= 0; i--)
+    free (eq[i].coef);
+
+  free (eq);
+}
+
+/* Returns true when E is an inequality with a single variable.  */
+
+static inline bool
+single_var_geq (eqn e, int nv ATTRIBUTE_UNUSED)
+{
+  return (e->key != 0
+         && -OMEGA_MAX_VARS <= e->key && e->key <= OMEGA_MAX_VARS);
+}
+
+/* Allocate a new equality with all coefficients 0, and tagged with
+   COLOR.  Return the index of this equality in problem PB.  */
+
+static inline int
+omega_add_zero_eq (omega_pb pb, enum omega_eqn_color color)
+{
+  int idx = pb->num_eqs++;
+
+  gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
+  omega_init_eqn_zero (&pb->eqs[idx], pb->num_vars);
+  pb->eqs[idx].color = color;
+  return idx;
+}
+
+/* Allocate a new inequality with all coefficients 0, and tagged with
+   COLOR.  Return the index of this inequality in problem PB.  */
+
+static inline int
+omega_add_zero_geq (omega_pb pb, enum omega_eqn_color color)
+{
+  int idx = pb->num_geqs;
+
+  pb->num_geqs++;
+  gcc_assert (pb->num_geqs <= OMEGA_MAX_GEQS);
+  omega_init_eqn_zero (&pb->geqs[idx], pb->num_vars);
+  pb->geqs[idx].touched = 1;
+  pb->geqs[idx].color = color;
+  return idx;
+}
+
+/* Initialize variables for problem PB.  */
+
+static inline void
+omega_initialize_variables (omega_pb pb)
+{
+  int i;
+
+  for (i = pb->num_vars; i >= 0; i--)
+    pb->forwarding_address[i] = pb->var[i] = i;
+
+  pb->variables_initialized = true;
+}
+
+/* Free problem PB.  */
+
+static inline void
+omega_free_problem (omega_pb pb)
+{
+  free (pb->var);
+  free (pb->forwarding_address);
+  omega_free_eqns (pb->geqs, OMEGA_MAX_GEQS);
+  omega_free_eqns (pb->eqs, OMEGA_MAX_EQS);
+  omega_free_eqns (pb->subs, OMEGA_MAX_VARS + 1);
+  free (pb);
+}
+
+/* Copy omega problems: P1 = P2.  */
+
+static inline void
+omega_copy_problem (omega_pb p1, omega_pb p2)
+{
+  int e, i;
+
+  p1->num_vars = p2->num_vars;
+  p1->hash_version = p2->hash_version;
+  p1->variables_initialized = p2->variables_initialized;
+  p1->variables_freed = p2->variables_freed;
+  p1->safe_vars = p2->safe_vars;
+  p1->num_eqs = p2->num_eqs;
+  p1->num_subs = p2->num_subs;
+  p1->num_geqs = p2->num_geqs;
+
+  for (e = p2->num_eqs - 1; e >= 0; e--)
+    omega_copy_eqn (&(p1->eqs[e]), &(p2->eqs[e]), p2->num_vars);
+
+  for (e = p2->num_geqs - 1; e >= 0; e--)
+    omega_copy_eqn (&(p1->geqs[e]), &(p2->geqs[e]), p2->num_vars);
+
+  for (e = p2->num_subs - 1; e >= 0; e--)
+    omega_copy_eqn (&(p1->subs[e]), &(p2->subs[e]), p2->num_vars);
+
+  for (i = p2->num_vars; i >= 0; i--)
+    p1->var[i] = p2->var[i];
+
+  for (i = OMEGA_MAX_VARS; i >= 0; i--)
+    p1->forwarding_address[i] = p2->forwarding_address[i];
+}
+
+#endif /* GCC_OMEGA_H */
index e583025..3725148 100644 (file)
@@ -1,5 +1,6 @@
 /* params.def - Run-time parameters.
-   Copyright (C) 2001, 2002, 2004, 2005 Free Software Foundation, Inc.
+   Copyright (C) 2001, 2002, 2003, 2004, 2005, 2006, 2007 
+   Free Software Foundation, Inc.
    Written by Mark Mitchell <mark@codesourcery.com>.
 
 This file is part of GCC.
@@ -452,6 +453,41 @@ DEFPARAM(PARAM_SCEV_MAX_EXPR_SIZE,
         "Bound on size of expressions used in the scalar evolutions analyzer",
         20, 0, 0)
 
+DEFPARAM(PARAM_OMEGA_MAX_VARS,
+        "omega-max-vars",
+        "Bound on the number of variables in Omega constraint systems",
+        128, 0, 0)
+
+DEFPARAM(PARAM_OMEGA_MAX_GEQS,
+        "omega-max-geqs",
+        "Bound on the number of inequalities in Omega constraint systems",
+        256, 0, 0)
+
+DEFPARAM(PARAM_OMEGA_MAX_EQS,
+        "omega-max-eqs",
+        "Bound on the number of equalities in Omega constraint systems",
+        128, 0, 0)
+
+DEFPARAM(PARAM_OMEGA_MAX_WILD_CARDS,
+        "omega-max-wild-cards",
+        "Bound on the number of wild cards in Omega constraint systems",
+        18, 0, 0)
+
+DEFPARAM(PARAM_OMEGA_HASH_TABLE_SIZE,
+        "omega-hash-table-size",
+        "Bound on the size of the hash table in Omega constraint systems",
+        550, 0, 0)
+
+DEFPARAM(PARAM_OMEGA_MAX_KEYS,
+        "omega-max-keys",
+        "Bound on the number of keys in Omega constraint systems",
+        500, 0, 0)
+
+DEFPARAM(PARAM_OMEGA_ELIMINATE_REDUNDANT_CONSTRAINTS,
+        "omega-eliminate-redundant-constraints",
+        "When set to 1, use expensive methods to eliminate all redundant constraints",
+        0, 0, 1)
+
 DEFPARAM(PARAM_VECT_MAX_VERSION_CHECKS,
          "vect-max-version-checks",
          "Bound on number of runtime checks inserted by the vectorizer's loop versioning",
index 0c28075..28bda44 100644 (file)
@@ -590,6 +590,7 @@ init_optimization_passes (void)
          NEXT_PASS (pass_scev_cprop);
          NEXT_PASS (pass_empty_loop);
          NEXT_PASS (pass_record_bounds);
+         NEXT_PASS (pass_check_data_deps);
          NEXT_PASS (pass_linear_transform);
          NEXT_PASS (pass_iv_canon);
          NEXT_PASS (pass_if_conversion);
index a30efc5..855f959 100644 (file)
@@ -109,6 +109,7 @@ DEFTIMEVAR (TV_TREE_LOOP_UNSWITCH    , "tree loop unswitching")
 DEFTIMEVAR (TV_COMPLETE_UNROLL       , "complete unrolling")
 DEFTIMEVAR (TV_TREE_VECTORIZATION    , "tree vectorization")
 DEFTIMEVAR (TV_TREE_LINEAR_TRANSFORM , "tree loop linear")
+DEFTIMEVAR (TV_CHECK_DATA_DEPS       , "tree check data dependences")
 DEFTIMEVAR (TV_TREE_PREFETCH        , "tree prefetching")
 DEFTIMEVAR (TV_TREE_LOOP_IVOPTS             , "tree iv optimization")
 DEFTIMEVAR (TV_TREE_LOOP_INIT       , "tree loop init")
index b6750ee..7eadde7 100644 (file)
@@ -1,5 +1,5 @@
 /* Data references and dependences detectors.
-   Copyright (C) 2003, 2004, 2005, 2006 Free Software Foundation, Inc.
+   Copyright (C) 2003, 2004, 2005, 2006, 2007 Free Software Foundation, Inc.
    Contributed by Sebastian Pop <pop@cri.ensmp.fr>
 
 This file is part of GCC.
@@ -125,10 +125,6 @@ static struct datadep_stats
 static tree object_analysis (tree, tree, bool, struct data_reference **, 
                             tree *, tree *, tree *, tree *, tree *,
                             struct ptr_info_def **, subvar_t *);
-static struct data_reference * init_data_ref (tree, tree, tree, tree, bool, 
-                                             tree, tree, tree, tree, tree, 
-                                             struct ptr_info_def *,
-                                             enum  data_ref_type);
 static bool subscript_dependence_tester_1 (struct data_dependence_relation *,
                                           struct data_reference *,
                                           struct data_reference *);
@@ -832,6 +828,7 @@ dump_data_dependence_relation (FILE *outf,
          dump_subscript (outf, DDR_SUBSCRIPT (ddr, i));
        }
 
+      fprintf (outf, "  inner loop index: %d\n", DDR_INNER_LOOP (ddr));
       fprintf (outf, "  loop nest: (");
       for (i = 0; VEC_iterate (loop_p, DDR_LOOP_NEST (ddr), i, loopi); i++)
        fprintf (outf, "%d ", loopi->num);
@@ -985,27 +982,24 @@ analyze_array_indexes (struct loop *loop,
    set to true when REF is in the right hand side of an
    assignment.  */
 
-struct data_reference *
-analyze_array (tree stmt, tree ref, bool is_read)
+static struct data_reference *
+init_array_ref (tree stmt, tree ref, bool is_read)
 {
-  struct data_reference *res;
-  VEC(tree,heap) *acc_fns;
+  struct loop *loop = loop_containing_stmt (stmt);
+  VEC(tree,heap) *acc_fns = VEC_alloc (tree, heap, 3);
+  struct data_reference *res = XNEW (struct data_reference);;
 
   if (dump_file && (dump_flags & TDF_DETAILS))
     {
-      fprintf (dump_file, "(analyze_array \n");
+      fprintf (dump_file, "(init_array_ref \n");
       fprintf (dump_file, "  (ref = ");
       print_generic_stmt (dump_file, ref, 0);
       fprintf (dump_file, ")\n");
     }
 
-  res = XNEW (struct data_reference);
-
   DR_STMT (res) = stmt;
   DR_REF (res) = ref;
-  acc_fns = VEC_alloc (tree, heap, 3);
-  DR_BASE_OBJECT (res) = analyze_array_indexes
-    (loop_containing_stmt (stmt), &acc_fns, ref, stmt);
+  DR_BASE_OBJECT (res) = analyze_array_indexes (loop, &acc_fns, ref, stmt);
   DR_TYPE (res) = ARRAY_REF_TYPE;
   DR_SET_ACCESS_FNS (res, acc_fns);
   DR_IS_READ (res) = is_read;
@@ -1023,6 +1017,45 @@ analyze_array (tree stmt, tree ref, bool is_read)
   return res;
 }
 
+/* For a data reference REF contained in the statement STMT, initialize
+   a DATA_REFERENCE structure, and return it.  */
+
+static struct data_reference *
+init_pointer_ref (tree stmt, tree ref, tree access_fn, bool is_read,
+                 tree base_address, tree step, struct ptr_info_def *ptr_info)
+{
+  struct data_reference *res = XNEW (struct data_reference);
+  VEC(tree,heap) *acc_fns = VEC_alloc (tree, heap, 3);
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    {
+      fprintf (dump_file, "(init_pointer_ref \n");
+      fprintf (dump_file, "  (ref = ");
+      print_generic_stmt (dump_file, ref, 0);
+      fprintf (dump_file, ")\n");
+    }
+
+  DR_STMT (res) = stmt;
+  DR_REF (res) = ref;
+  DR_BASE_OBJECT (res) = NULL_TREE;
+  DR_TYPE (res) = POINTER_REF_TYPE;
+  DR_SET_ACCESS_FNS (res, acc_fns);
+  VEC_quick_push (tree, DR_ACCESS_FNS (res), access_fn);
+  DR_IS_READ (res) = is_read;
+  DR_BASE_ADDRESS (res) = base_address;
+  DR_OFFSET (res) = NULL_TREE;
+  DR_INIT (res) = NULL_TREE;
+  DR_STEP (res) = step;
+  DR_OFFSET_MISALIGNMENT (res) = NULL_TREE;
+  DR_MEMTAG (res) = NULL_TREE;
+  DR_PTR_INFO (res) = ptr_info;
+
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    fprintf (dump_file, ")\n");
+
+  return res;
+}
+
 /* Analyze an indirect memory reference, REF, that comes from STMT.
    IS_READ is true if this is an indirect load, and false if it is
    an indirect store.
@@ -1063,7 +1096,7 @@ analyze_indirect_ref (tree stmt, tree ref, bool is_read)
 
   if (!expr_invariant_in_loop_p (loop, init))
     {
-    if (dump_file && (dump_flags & TDF_DETAILS))
+      if (dump_file && (dump_flags & TDF_DETAILS))
        fprintf (dump_file, "\ninitial condition is not loop invariant.\n");    
     }
   else
@@ -1087,61 +1120,8 @@ analyze_indirect_ref (tree stmt, tree ref, bool is_read)
        if (dump_file && (dump_flags & TDF_DETAILS))
          fprintf (dump_file, "\nunknown evolution of ptr.\n"); 
     }
-  return init_data_ref (stmt, ref, NULL_TREE, access_fn, is_read, base_address, 
-                       NULL_TREE, step, NULL_TREE, NULL_TREE, 
-                       ptr_info, POINTER_REF_TYPE);
-}
-
-/* For a data reference REF contained in the statement STMT, initialize
-   a DATA_REFERENCE structure, and return it.  */
-
-struct data_reference *
-init_data_ref (tree stmt, 
-              tree ref,
-              tree base,
-              tree access_fn,
-              bool is_read,
-              tree base_address,
-              tree init_offset,
-              tree step,
-              tree misalign,
-              tree memtag,
-               struct ptr_info_def *ptr_info,
-              enum data_ref_type type)
-{
-  struct data_reference *res;
-  VEC(tree,heap) *acc_fns;
-
-  if (dump_file && (dump_flags & TDF_DETAILS))
-    {
-      fprintf (dump_file, "(init_data_ref \n");
-      fprintf (dump_file, "  (ref = ");
-      print_generic_stmt (dump_file, ref, 0);
-      fprintf (dump_file, ")\n");
-    }
-
-  res = XNEW (struct data_reference);
-
-  DR_STMT (res) = stmt;
-  DR_REF (res) = ref;
-  DR_BASE_OBJECT (res) = base;
-  DR_TYPE (res) = type;
-  acc_fns = VEC_alloc (tree, heap, 3);
-  DR_SET_ACCESS_FNS (res, acc_fns);
-  VEC_quick_push (tree, DR_ACCESS_FNS (res), access_fn);
-  DR_IS_READ (res) = is_read;
-  DR_BASE_ADDRESS (res) = base_address;
-  DR_OFFSET (res) = init_offset;
-  DR_INIT (res) = NULL_TREE;
-  DR_STEP (res) = step;
-  DR_OFFSET_MISALIGNMENT (res) = misalign;
-  DR_MEMTAG (res) = memtag;
-  DR_PTR_INFO (res) = ptr_info;
-
-  if (dump_file && (dump_flags & TDF_DETAILS))
-    fprintf (dump_file, ")\n");
-
-  return res;
+  return init_pointer_ref (stmt, ref, access_fn, is_read, base_address, 
+                          step, ptr_info);
 }
 
 /* Function strip_conversions
@@ -1598,7 +1578,7 @@ object_analysis (tree memref, tree stmt, bool is_read,
       if (!(*dr))
        { 
          if (TREE_CODE (memref) == ARRAY_REF)
-           *dr = analyze_array (stmt, memref, is_read);          
+           *dr = init_array_ref (stmt, memref, is_read);         
          else if (TREE_CODE (memref) == COMPONENT_REF)
            comp_ref = memref;
          else  
@@ -1671,7 +1651,7 @@ object_analysis (tree memref, tree stmt, bool is_read,
        {
          if (comp_ref && TREE_CODE (TREE_OPERAND (comp_ref, 0)) == ARRAY_REF)
            {
-             *dr = analyze_array (stmt, TREE_OPERAND (comp_ref, 0), is_read);                
+             *dr = init_array_ref (stmt, TREE_OPERAND (comp_ref, 0), is_read);               
              if (DR_NUM_DIMENSIONS (*dr) != 1)
                {
                  if (dump_file && (dump_flags & TDF_DETAILS))
@@ -2302,6 +2282,7 @@ initialize_data_dependence_relation (struct data_reference *a,
   DDR_ARE_DEPENDENT (res) = NULL_TREE;
   DDR_SUBSCRIPTS (res) = VEC_alloc (subscript_p, heap, DR_NUM_DIMENSIONS (a));
   DDR_LOOP_NEST (res) = loop_nest;
+  DDR_INNER_LOOP (res) = 0;
   DDR_DIR_VECTS (res) = NULL;
   DDR_DIST_VECTS (res) = NULL;
 
@@ -4176,10 +4157,10 @@ static bool
 access_functions_are_affine_or_constant_p (struct data_reference *a)
 {
   unsigned int i;
-  VEC(tree,heap) **fns = DR_ACCESS_FNS_ADDR (a);
+  VEC(tree,heap) *fns = DR_ACCESS_FNS (a);
   tree t;
-  
-  for (i = 0; VEC_iterate (tree, *fns, i, t); i++)
+
+  for (i = 0; VEC_iterate (tree, fns, i, t); i++)
     if (!evolution_function_is_constant_p (t)
        && !evolution_function_is_affine_multivariate_p (t))
       return false;
@@ -4187,6 +4168,530 @@ access_functions_are_affine_or_constant_p (struct data_reference *a)
   return true;
 }
 
+/* Initializes an equation for an OMEGA problem using the information
+   contained in the ACCESS_FUN.  Returns true when the operation
+   succeeded.
+
+   PB is the omega constraint system.
+   EQ is the number of the equation to be initialized.
+   OFFSET is used for shifting the variables names in the constraints:
+   a constrain is composed of 2 * the number of variables surrounding
+   dependence accesses.  OFFSET is set either to 0 for the first n variables,
+   then it is set to n.
+   ACCESS_FUN is expected to be an affine chrec.  */
+
+static bool
+init_omega_eq_with_af (omega_pb pb, unsigned eq, 
+                      unsigned int offset, tree access_fun, 
+                      struct data_dependence_relation *ddr)
+{
+  switch (TREE_CODE (access_fun))
+    {
+    case POLYNOMIAL_CHREC:
+      {
+       tree left = CHREC_LEFT (access_fun);
+       tree right = CHREC_RIGHT (access_fun);
+       int var = CHREC_VARIABLE (access_fun);
+       unsigned var_idx;
+
+       if (TREE_CODE (right) != INTEGER_CST)
+         return false;
+
+       var_idx = index_in_loop_nest (var, DDR_LOOP_NEST (ddr));
+       pb->eqs[eq].coef[offset + var_idx + 1] = int_cst_value (right);
+
+       /* Compute the innermost loop index.  */
+       DDR_INNER_LOOP (ddr) = MAX (DDR_INNER_LOOP (ddr), var_idx);
+
+       if (offset == 0)
+         pb->eqs[eq].coef[var_idx + DDR_NB_LOOPS (ddr) + 1] 
+           += int_cst_value (right);
+
+       switch (TREE_CODE (left))
+         {
+         case POLYNOMIAL_CHREC:
+           return init_omega_eq_with_af (pb, eq, offset, left, ddr);
+
+         case INTEGER_CST:
+           pb->eqs[eq].coef[0] += int_cst_value (left);
+           return true;
+
+         default:
+           return false;
+         }
+      }
+
+    case INTEGER_CST:
+      pb->eqs[eq].coef[0] += int_cst_value (access_fun);
+      return true;
+
+    default:
+      return false;
+    }
+}
+
+/* As explained in the comments preceding init_omega_for_ddr, we have
+   to set up a system for each loop level, setting outer loops
+   variation to zero, and current loop variation to positive or zero.
+   Save each lexico positive distance vector.  */
+
+static void
+omega_extract_distance_vectors (omega_pb pb,
+                               struct data_dependence_relation *ddr)
+{
+  int eq, geq;
+  unsigned i, j;
+  struct loop *loopi, *loopj;
+  enum omega_result res;
+
+  /* Set a new problem for each loop in the nest.  The basis is the
+     problem that we have initialized until now.  On top of this we
+     add new constraints.  */
+  for (i = 0; i <= DDR_INNER_LOOP (ddr) 
+        && VEC_iterate (loop_p, DDR_LOOP_NEST (ddr), i, loopi); i++)
+    {
+      int dist = 0;
+      omega_pb copy = omega_alloc_problem (2 * DDR_NB_LOOPS (ddr),
+                                          DDR_NB_LOOPS (ddr));
+
+      omega_copy_problem (copy, pb);
+
+      /* For all the outer loops "loop_j", add "dj = 0".  */
+      for (j = 0;
+          j < i && VEC_iterate (loop_p, DDR_LOOP_NEST (ddr), j, loopj); j++)
+       {
+         eq = omega_add_zero_eq (copy, omega_black);
+         copy->eqs[eq].coef[j + 1] = 1;
+       }
+
+      /* For "loop_i", add "0 <= di".  */
+      geq = omega_add_zero_geq (copy, omega_black);
+      copy->geqs[geq].coef[i + 1] = 1;
+
+      /* Reduce the constraint system, and test that the current
+        problem is feasible.  */
+      res = omega_simplify_problem (copy);
+      if (res == omega_false 
+         || res == omega_unknown
+         || copy->num_geqs > (int) DDR_NB_LOOPS (ddr))
+       goto next_problem;
+
+      for (eq = 0; eq < copy->num_subs; eq++)
+       if (copy->subs[eq].key == (int) i + 1)
+         {
+           dist = copy->subs[eq].coef[0];
+           goto found_dist;
+         }
+
+      if (dist == 0)
+       {
+         /* Reinitialize problem...  */
+         omega_copy_problem (copy, pb);
+         for (j = 0;
+              j < i && VEC_iterate (loop_p, DDR_LOOP_NEST (ddr), j, loopj); j++)
+           {
+             eq = omega_add_zero_eq (copy, omega_black);
+             copy->eqs[eq].coef[j + 1] = 1;
+           }
+
+         /* ..., but this time "di = 1".  */
+         eq = omega_add_zero_eq (copy, omega_black);
+         copy->eqs[eq].coef[i + 1] = 1;
+         copy->eqs[eq].coef[0] = -1;
+
+         res = omega_simplify_problem (copy);
+         if (res == omega_false 
+             || res == omega_unknown
+             || copy->num_geqs > (int) DDR_NB_LOOPS (ddr))
+           goto next_problem;
+
+         for (eq = 0; eq < copy->num_subs; eq++)
+           if (copy->subs[eq].key == (int) i + 1)
+             {
+               dist = copy->subs[eq].coef[0];
+               goto found_dist;
+             }
+       }
+
+    found_dist:;
+      /* Save the lexicographically positive distance vector.  */
+      if (dist >= 0)
+       {
+         lambda_vector dist_v = lambda_vector_new (DDR_NB_LOOPS (ddr));
+         lambda_vector dir_v = lambda_vector_new (DDR_NB_LOOPS (ddr));
+
+         dist_v[i] = dist;
+
+         for (eq = 0; eq < copy->num_subs; eq++)
+           if (copy->subs[eq].key > 0)
+             {
+               dist = copy->subs[eq].coef[0];
+               dist_v[copy->subs[eq].key - 1] = dist;
+             }
+
+         for (j = 0; j < DDR_NB_LOOPS (ddr); j++)
+           dir_v[j] = dir_from_dist (dist_v[j]);
+
+         save_dist_v (ddr, dist_v);
+         save_dir_v (ddr, dir_v);
+       }
+
+    next_problem:;
+      omega_free_problem (copy);
+    }
+}
+
+/* This is called for each subscript of a tuple of data references:
+   insert an equality for representing the conflicts.  */
+
+static bool
+omega_setup_subscript (tree access_fun_a, tree access_fun_b,
+                      struct data_dependence_relation *ddr,
+                      omega_pb pb, bool *maybe_dependent)
+{
+  int eq;
+  tree fun_a = chrec_convert (integer_type_node, access_fun_a, NULL_TREE);
+  tree fun_b = chrec_convert (integer_type_node, access_fun_b, NULL_TREE);
+  tree difference = chrec_fold_minus (integer_type_node, fun_a, fun_b);
+
+  /* When the fun_a - fun_b is not constant, the dependence is not
+     captured by the classic distance vector representation.  */
+  if (TREE_CODE (difference) != INTEGER_CST)
+    return false;
+
+  /* ZIV test.  */
+  if (ziv_subscript_p (fun_a, fun_b) && !integer_zerop (difference))
+    {
+      /* There is no dependence.  */
+      *maybe_dependent = false;
+      return true;
+    }
+
+  fun_b = chrec_fold_multiply (integer_type_node, fun_b, 
+                              integer_minus_one_node);
+
+  eq = omega_add_zero_eq (pb, omega_black);
+  if (!init_omega_eq_with_af (pb, eq, DDR_NB_LOOPS (ddr), fun_a, ddr)
+      || !init_omega_eq_with_af (pb, eq, 0, fun_b, ddr))
+    /* There is probably a dependence, but the system of
+       constraints cannot be built: answer "don't know".  */
+    return false;
+
+  /* GCD test.  */
+  if (DDR_NB_LOOPS (ddr) != 0 && pb->eqs[eq].coef[0]
+      && !int_divides_p (lambda_vector_gcd 
+                        ((lambda_vector) &(pb->eqs[eq].coef[1]),
+                         2 * DDR_NB_LOOPS (ddr)),
+                        pb->eqs[eq].coef[0]))
+    {
+      /* There is no dependence.  */
+      *maybe_dependent = false;
+      return true;
+    }
+
+  return true;
+}
+
+/* Helper function, same as init_omega_for_ddr but specialized for
+   data references A and B.  */
+
+static bool
+init_omega_for_ddr_1 (struct data_reference *dra, struct data_reference *drb,
+                     struct data_dependence_relation *ddr,
+                     omega_pb pb, bool *maybe_dependent)
+{
+  unsigned i;
+  int ineq;
+  struct loop *loopi;
+  unsigned nb_loops = DDR_NB_LOOPS (ddr);
+
+  /* Insert an equality per subscript.  */
+  for (i = 0; i < DDR_NUM_SUBSCRIPTS (ddr); i++)
+    {
+      if (!omega_setup_subscript (DR_ACCESS_FN (dra, i), DR_ACCESS_FN (drb, i),
+                                 ddr, pb, maybe_dependent))
+       return false;
+      else if (*maybe_dependent == false)
+       {
+         /* There is no dependence.  */
+         DDR_ARE_DEPENDENT (ddr) = chrec_known;
+         return true;
+       }
+    }
+
+  /* Insert inequalities: constraints corresponding to the iteration
+     domain, i.e. the loops surrounding the references "loop_x" and
+     the distance variables "dx".  The layout of the OMEGA
+     representation is as follows:
+     - coef[0] is the constant
+     - coef[1..nb_loops] are the protected variables that will not be
+     removed by the solver: the "dx"
+     - coef[nb_loops + 1, 2*nb_loops] are the loop variables: "loop_x".
+  */
+  for (i = 0; i <= DDR_INNER_LOOP (ddr) 
+        && VEC_iterate (loop_p, DDR_LOOP_NEST (ddr), i, loopi); i++)
+    {
+      HOST_WIDE_INT nbi = estimated_loop_iterations_int (loopi, true);
+
+      /* 0 <= loop_x */
+      ineq = omega_add_zero_geq (pb, omega_black);
+      pb->geqs[ineq].coef[i + nb_loops + 1] = 1;
+
+      /* 0 <= loop_x + dx */
+      ineq = omega_add_zero_geq (pb, omega_black);
+      pb->geqs[ineq].coef[i + nb_loops + 1] = 1;
+      pb->geqs[ineq].coef[i + 1] = 1;
+
+      if (nbi != -1)
+       {
+         /* loop_x <= nb_iters */
+         ineq = omega_add_zero_geq (pb, omega_black);
+         pb->geqs[ineq].coef[i + nb_loops + 1] = -1;
+         pb->geqs[ineq].coef[0] = nbi;
+
+         /* loop_x + dx <= nb_iters */
+         ineq = omega_add_zero_geq (pb, omega_black);
+         pb->geqs[ineq].coef[i + nb_loops + 1] = -1;
+         pb->geqs[ineq].coef[i + 1] = -1;
+         pb->geqs[ineq].coef[0] = nbi;
+
+         /* A step "dx" bigger than nb_iters is not feasible, so
+            add "0 <= nb_iters + dx",  */
+         ineq = omega_add_zero_geq (pb, omega_black);
+         pb->geqs[ineq].coef[i + 1] = 1;
+         pb->geqs[ineq].coef[0] = nbi;
+         /* and "dx <= nb_iters".  */
+         ineq = omega_add_zero_geq (pb, omega_black);
+         pb->geqs[ineq].coef[i + 1] = -1;
+         pb->geqs[ineq].coef[0] = nbi;
+       }
+    }
+
+  omega_extract_distance_vectors (pb, ddr);
+
+  return true;
+}
+
+/* Sets up the Omega dependence problem for the data dependence
+   relation DDR.  Returns false when the constraint system cannot be
+   built, ie. when the test answers "don't know".  Returns true
+   otherwise, and when independence has been proved (using one of the
+   trivial dependence test), set MAYBE_DEPENDENT to false, otherwise
+   set MAYBE_DEPENDENT to true.
+
+   Example: for setting up the dependence system corresponding to the
+   conflicting accesses 
+
+   | loop_i
+   |   loop_j
+   |     A[i, i+1] = ...
+   |     ... A[2*j, 2*(i + j)]
+   |   endloop_j
+   | endloop_i
+   
+   the following constraints come from the iteration domain:
+
+   0 <= i <= Ni
+   0 <= i + di <= Ni
+   0 <= j <= Nj
+   0 <= j + dj <= Nj
+
+   where di, dj are the distance variables.  The constraints
+   representing the conflicting elements are:
+
+   i = 2 * (j + dj)
+   i + 1 = 2 * (i + di + j + dj)
+
+   For asking that the resulting distance vector (di, dj) be
+   lexicographically positive, we insert the constraint "di >= 0".  If
+   "di = 0" in the solution, we fix that component to zero, and we
+   look at the inner loops: we set a new problem where all the outer
+   loop distances are zero, and fix this inner component to be
+   positive.  When one of the components is positive, we save that
+   distance, and set a new problem where the distance on this loop is
+   zero, searching for other distances in the inner loops.  Here is
+   the classic example that illustrates that we have to set for each
+   inner loop a new problem:
+
+   | loop_1
+   |   loop_2
+   |     A[10]
+   |   endloop_2
+   | endloop_1
+
+   we have to save two distances (1, 0) and (0, 1).
+
+   Given two array references, refA and refB, we have to set the
+   dependence problem twice, refA vs. refB and refB vs. refA, and we
+   cannot do a single test, as refB might occur before refA in the
+   inner loops, and the contrary when considering outer loops: ex.
+
+   | loop_0
+   |   loop_1
+   |     loop_2
+   |       T[{1,+,1}_2][{1,+,1}_1]  // refA
+   |       T[{2,+,1}_2][{0,+,1}_1]  // refB
+   |     endloop_2
+   |   endloop_1
+   | endloop_0
+
+   refB touches the elements in T before refA, and thus for the same
+   loop_0 refB precedes refA: ie. the distance vector (0, 1, -1)
+   but for successive loop_0 iterations, we have (1, -1, 1)
+
+   The Omega solver expects the distance variables ("di" in the
+   previous example) to come first in the constraint system (as
+   variables to be protected, or "safe" variables), the constraint
+   system is built using the following layout:
+
+   "cst | distance vars | index vars".
+*/
+
+static bool
+init_omega_for_ddr (struct data_dependence_relation *ddr,
+                   bool *maybe_dependent)
+{
+  omega_pb pb;
+  bool res = false;
+
+  *maybe_dependent = true;
+
+  if (same_access_functions (ddr))
+    {
+      unsigned j;
+      lambda_vector dir_v;
+
+      /* Save the 0 vector.  */
+      save_dist_v (ddr, lambda_vector_new (DDR_NB_LOOPS (ddr)));
+      dir_v = lambda_vector_new (DDR_NB_LOOPS (ddr));
+      for (j = 0; j < DDR_NB_LOOPS (ddr); j++)
+       dir_v[j] = dir_equal;
+      save_dir_v (ddr, dir_v);
+
+      /* Save the dependences carried by outer loops.  */
+      pb = omega_alloc_problem (2 * DDR_NB_LOOPS (ddr), DDR_NB_LOOPS (ddr));
+      res = init_omega_for_ddr_1 (DDR_A (ddr), DDR_B (ddr), ddr, pb,
+                                 maybe_dependent);
+      omega_free_problem (pb);
+      return res;
+    }
+
+  /* Omega expects the protected variables (those that have to be kept
+     after elimination) to appear first in the constraint system.
+     These variables are the distance variables.  In the following
+     initialization we declare NB_LOOPS safe variables, and the total
+     number of variables for the constraint system is 2*NB_LOOPS.  */
+  pb = omega_alloc_problem (2 * DDR_NB_LOOPS (ddr), DDR_NB_LOOPS (ddr));
+  res = init_omega_for_ddr_1 (DDR_A (ddr), DDR_B (ddr), ddr, pb,
+                             maybe_dependent);
+  omega_free_problem (pb);
+
+  /* Stop computation if not decidable, or no dependence.  */
+  if (res == false || *maybe_dependent == false)
+    return res;
+
+  pb = omega_alloc_problem (2 * DDR_NB_LOOPS (ddr), DDR_NB_LOOPS (ddr));
+  res = init_omega_for_ddr_1 (DDR_B (ddr), DDR_A (ddr), ddr, pb,
+                             maybe_dependent);
+  omega_free_problem (pb);
+
+  return res;
+}
+
+/* Return true when DDR contains the same information as that stored
+   in DIR_VECTS and in DIST_VECTS, return false otherwise.   */
+
+static bool
+ddr_consistent_p (FILE *file,
+                 struct data_dependence_relation *ddr,
+                 VEC (lambda_vector, heap) *dist_vects,
+                 VEC (lambda_vector, heap) *dir_vects)
+{
+  unsigned int i, j;
+
+  /* If dump_file is set, output there.  */
+  if (dump_file && (dump_flags & TDF_DETAILS))
+    file = dump_file;
+
+  if (VEC_length (lambda_vector, dist_vects) != DDR_NUM_DIST_VECTS (ddr))
+    {
+      lambda_vector b_dist_v;
+      fprintf (file, "\n(Number of distance vectors differ: Banerjee has %d, Omega has %d.\n",
+              VEC_length (lambda_vector, dist_vects),
+              DDR_NUM_DIST_VECTS (ddr));
+
+      fprintf (file, "Banerjee dist vectors:\n");
+      for (i = 0; VEC_iterate (lambda_vector, dist_vects, i, b_dist_v); i++)
+       print_lambda_vector (file, b_dist_v, DDR_NB_LOOPS (ddr));
+
+      fprintf (file, "Omega dist vectors:\n");
+      for (i = 0; i < DDR_NUM_DIST_VECTS (ddr); i++)
+       print_lambda_vector (file, DDR_DIST_VECT (ddr, i), DDR_NB_LOOPS (ddr));
+
+      fprintf (file, "data dependence relation:\n");
+      dump_data_dependence_relation (file, ddr);
+
+      fprintf (file, ")\n");
+      return false;
+    }
+
+  if (VEC_length (lambda_vector, dir_vects) != DDR_NUM_DIR_VECTS (ddr))
+    {
+      fprintf (file, "\n(Number of direction vectors differ: Banerjee has %d, Omega has %d.)\n",
+              VEC_length (lambda_vector, dir_vects),
+              DDR_NUM_DIR_VECTS (ddr));
+      return false;
+    }
+
+  for (i = 0; i < DDR_NUM_DIST_VECTS (ddr); i++)
+    {
+      lambda_vector a_dist_v;
+      lambda_vector b_dist_v = DDR_DIST_VECT (ddr, i);
+
+      /* Distance vectors are not ordered in the same way in the DDR
+        and in the DIST_VECTS: search for a matching vector.  */
+      for (j = 0; VEC_iterate (lambda_vector, dist_vects, j, a_dist_v); j++)
+       if (lambda_vector_equal (a_dist_v, b_dist_v, DDR_NB_LOOPS (ddr)))
+         break;
+
+      if (j == VEC_length (lambda_vector, dist_vects))
+       {
+         fprintf (file, "\n(Dist vectors from the first dependence analyzer:\n");
+         print_dist_vectors (file, dist_vects, DDR_NB_LOOPS (ddr));
+         fprintf (file, "not found in Omega dist vectors:\n");
+         print_dist_vectors (file, DDR_DIST_VECTS (ddr), DDR_NB_LOOPS (ddr));
+         fprintf (file, "data dependence relation:\n");
+         dump_data_dependence_relation (file, ddr);
+         fprintf (file, ")\n");
+       }
+    }
+
+  for (i = 0; i < DDR_NUM_DIR_VECTS (ddr); i++)
+    {
+      lambda_vector a_dir_v;
+      lambda_vector b_dir_v = DDR_DIR_VECT (ddr, i);
+
+      /* Direction vectors are not ordered in the same way in the DDR
+        and in the DIR_VECTS: search for a matching vector.  */
+      for (j = 0; VEC_iterate (lambda_vector, dir_vects, j, a_dir_v); j++)
+       if (lambda_vector_equal (a_dir_v, b_dir_v, DDR_NB_LOOPS (ddr)))
+         break;
+
+      if (j == VEC_length (lambda_vector, dist_vects))
+       {
+         fprintf (file, "\n(Dir vectors from the first dependence analyzer:\n");
+         print_dir_vectors (file, dir_vects, DDR_NB_LOOPS (ddr));
+         fprintf (file, "not found in Omega dir vectors:\n");
+         print_dir_vectors (file, DDR_DIR_VECTS (ddr), DDR_NB_LOOPS (ddr));
+         fprintf (file, "data dependence relation:\n");
+         dump_data_dependence_relation (file, ddr);
+         fprintf (file, ")\n");
+       }
+    }
+
+  return true;  
+}
+
 /* This computes the affine dependence relation between A and B.
    CHREC_KNOWN is used for representing the independence between two
    accesses, while CHREC_DONT_KNOW is used for representing the unknown
@@ -4219,13 +4724,57 @@ compute_affine_dependence (struct data_dependence_relation *ddr)
 
       if (access_functions_are_affine_or_constant_p (dra)
          && access_functions_are_affine_or_constant_p (drb))
-       subscript_dependence_tester (ddr);
-      
+       {
+         if (flag_check_data_deps)
+           {
+             /* Compute the dependences using the first algorithm.  */
+             subscript_dependence_tester (ddr);
+
+             if (dump_file && (dump_flags & TDF_DETAILS))
+               {
+                 fprintf (dump_file, "\n\nBanerjee Analyzer\n");
+                 dump_data_dependence_relation (dump_file, ddr);
+               }
+
+             if (DDR_ARE_DEPENDENT (ddr) == NULL_TREE)
+               {
+                 bool maybe_dependent;
+                 VEC (lambda_vector, heap) *dir_vects, *dist_vects;
+
+                 /* Save the result of the first DD analyzer.  */
+                 dist_vects = DDR_DIST_VECTS (ddr);
+                 dir_vects = DDR_DIR_VECTS (ddr);
+
+                 /* Reset the information.  */
+                 DDR_DIST_VECTS (ddr) = NULL;
+                 DDR_DIR_VECTS (ddr) = NULL;
+
+                 /* Compute the same information using Omega.  */
+                 if (!init_omega_for_ddr (ddr, &maybe_dependent))
+                   goto csys_dont_know;
+
+                 if (dump_file && (dump_flags & TDF_DETAILS))
+                   {
+                     fprintf (dump_file, "Omega Analyzer\n");
+                     dump_data_dependence_relation (dump_file, ddr);
+                   }
+
+                 /* Check that we get the same information.  */
+                 if (maybe_dependent)
+                   gcc_assert (ddr_consistent_p (stderr, ddr, dist_vects,
+                                                 dir_vects));
+               }
+           }
+         else
+           subscript_dependence_tester (ddr);
+       }
+     
       /* As a last case, if the dependence cannot be determined, or if
         the dependence is considered too difficult to determine, answer
         "don't know".  */
       else
        {
+       csys_dont_know:;
          dependence_stats.num_dependence_undetermined++;
 
          if (dump_file && (dump_flags & TDF_DETAILS))
@@ -4584,7 +5133,7 @@ compute_data_dependences_for_loop (struct loop *loop,
 }
 
 /* Entry point (for testing only).  Analyze all the data references
-   and the dependence relations.
+   and the dependence relations in LOOP.
 
    The data references are computed first.  
    
@@ -4604,9 +5153,8 @@ compute_data_dependences_for_loop (struct loop *loop,
    recompute the same information.  The implementation of this KB is
    transparent to the optimizer, and thus the KB can be changed with a
    more efficient implementation, or the KB could be disabled.  */
-#if 0
 static void 
-analyze_all_data_dependences (struct loops *loops)
+analyze_all_data_dependences (struct loop *loop)
 {
   unsigned int i;
   int nb_data_refs = 10;
@@ -4616,8 +5164,8 @@ analyze_all_data_dependences (struct loops *loops)
     VEC_alloc (ddr_p, heap, nb_data_refs * nb_data_refs);
 
   /* Compute DDs on the whole function.  */
-  compute_data_dependences_for_loop (loops->parray[0], false,
-                                    &datarefs, &dependence_relations);
+  compute_data_dependences_for_loop (loop, false, &datarefs,
+                                    &dependence_relations);
 
   if (dump_file)
     {
@@ -4666,7 +5214,19 @@ analyze_all_data_dependences (struct loops *loops)
   free_dependence_relations (dependence_relations);
   free_data_refs (datarefs);
 }
-#endif
+
+/* Computes all the data dependences and check that the results of
+   several analyzers are the same.  */
+
+void
+tree_check_data_deps (void)
+{
+  loop_iterator li;
+  struct loop *loop_nest;
+
+  FOR_EACH_LOOP (li, loop_nest, 0)
+    analyze_all_data_dependences (loop_nest);
+}
 
 /* Free the memory used by a data dependence relation DDR.  */
 
index ba47174..02e1540 100644 (file)
@@ -1,5 +1,5 @@
 /* Data references and dependences detectors. 
-   Copyright (C) 2003, 2004, 2005, 2006 Free Software Foundation, Inc.
+   Copyright (C) 2003, 2004, 2005, 2006, 2007 Free Software Foundation, Inc.
    Contributed by Sebastian Pop <pop@cri.ensmp.fr>
 
 This file is part of GCC.
@@ -23,6 +23,7 @@ Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA
 #define GCC_TREE_DATA_REF_H
 
 #include "lambda.h"
+#include "omega.h"
 
 /*
   The first location accessed by data-ref in the loop is the address of data-ref's 
@@ -160,10 +161,6 @@ DEF_VEC_ALLOC_P (data_reference_p, heap);
 #define DR_OFFSET_MISALIGNMENT(DR) (DR)->misalignment
 #define DR_PTR_INFO(DR)            (DR)->ptr_info
 #define DR_SUBVARS(DR)             (DR)->subvars
-
-#define DR_ACCESS_FNS_ADDR(DR)       \
-  (DR_TYPE(DR) == ARRAY_REF_TYPE ?   \
-   &((DR)->object_info.access_fns) : &((DR)->first_location.access_fns))
 #define DR_SET_ACCESS_FNS(DR, ACC_FNS)         \
 {                                              \
   if (DR_TYPE(DR) == ARRAY_REF_TYPE)           \
@@ -281,6 +278,10 @@ struct data_dependence_relation
   /* The analyzed loop nest.  */
   VEC (loop_p, heap) *loop_nest;
 
+  /* An index in loop_nest for the innermost loop that varies for
+     this data dependence relation.  */
+  unsigned inner_loop;
+
   /* The classic direction vector.  */
   VEC (lambda_vector, heap) *dir_vects;
 
@@ -304,6 +305,7 @@ DEF_VEC_ALLOC_P(ddr_p,heap);
 /* The size of the direction/distance vectors: the number of loops in
    the loop nest.  */
 #define DDR_NB_LOOPS(DDR) (VEC_length (loop_p, DDR_LOOP_NEST (DDR)))
+#define DDR_INNER_LOOP(DDR) DDR->inner_loop
 
 #define DDR_DIST_VECTS(DDR) ((DDR)->dist_vects)
 #define DDR_DIR_VECTS(DDR) ((DDR)->dir_vects)
index bb08732..99db89d 100644 (file)
@@ -1,5 +1,6 @@
 /* Data and Control Flow Analysis for Trees.
-   Copyright (C) 2001, 2003, 2004, 2005 Free Software Foundation, Inc.
+   Copyright (C) 2001, 2003, 2004, 2005, 2006, 2007
+   Free Software Foundation, Inc.
    Contributed by Diego Novillo <dnovillo@redhat.com>
 
 This file is part of GCC.
@@ -993,6 +994,9 @@ bool sra_type_can_be_decomposed_p (tree);
 /* In tree-loop-linear.c  */
 extern void linear_transform_loops (void);
 
+/* In tree-data-ref.c  */
+extern void tree_check_data_deps (void);
+
 /* In tree-ssa-loop-ivopts.c  */
 bool expr_invariant_in_loop_p (struct loop *, tree);
 bool multiplier_allowed_in_address_p (HOST_WIDE_INT, enum machine_mode);
index 7cdee50..141ac29 100644 (file)
@@ -298,6 +298,7 @@ extern struct tree_opt_pass pass_rest_of_compilation;
 extern struct tree_opt_pass pass_sink_code;
 extern struct tree_opt_pass pass_fre;
 extern struct tree_opt_pass pass_linear_transform;
+extern struct tree_opt_pass pass_check_data_deps;
 extern struct tree_opt_pass pass_copy_prop;
 extern struct tree_opt_pass pass_store_ccp;
 extern struct tree_opt_pass pass_store_copy_prop;
index bdf7ade..7457e53 100644 (file)
@@ -1,5 +1,5 @@
 /* Loop optimizations over tree-ssa.
-   Copyright (C) 2003, 2005 Free Software Foundation, Inc.
+   Copyright (C) 2003, 2005, 2006, 2007 Free Software Foundation, Inc.
    
 This file is part of GCC.
    
@@ -241,6 +241,41 @@ struct tree_opt_pass pass_linear_transform =
   0                                    /* letter */    
 };
 
+/* Check the correctness of the data dependence analyzers.  */
+
+static unsigned int
+check_data_deps (void)
+{
+  if (!current_loops)
+    return 0;
+
+  tree_check_data_deps ();
+  return 0;
+}
+
+static bool
+gate_check_data_deps (void)
+{
+  return flag_check_data_deps != 0;
+}
+
+struct tree_opt_pass pass_check_data_deps =
+{
+  "ckdd",                              /* name */
+  gate_check_data_deps,                        /* gate */
+  check_data_deps,                     /* execute */
+  NULL,                                        /* sub */
+  NULL,                                        /* next */
+  0,                                   /* static_pass_number */
+  TV_CHECK_DATA_DEPS,                          /* tv_id */
+  PROP_cfg | PROP_ssa,                 /* properties_required */
+  0,                                   /* properties_provided */
+  0,                                   /* properties_destroyed */
+  0,                                   /* todo_flags_start */
+  TODO_dump_func,                      /* todo_flags_finish */
+  0                                    /* letter */    
+};
+
 /* Canonical induction variable creation pass.  */
 
 static unsigned int