--- /dev/null
+/* 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, 2008 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 3, 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 COPYING3. If not see
+<http://www.gnu.org/licenses/>. */
+
+/* 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 Redundant 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 Redundant 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 Redundant 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 Redundant 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 nonzero 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 nonzero 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 Redundant:\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 weird 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;
+ int found_something = 0;
+
+ for (e = 0; e < pb->num_geqs; e++)
+ if (pb->geqs[e].color == omega_red)
+ colors++;
+
+ if (colors < 2)
+ return;
+
+ is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
+
+ 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 nonzero coefficient,
+ g is the coefficient of i,
+ j is the position of next nonzero 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 coefficients = ");
+
+ 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,
+ "******************** Redundant 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;
+}
projects / msp430-gcc.git / blobdiff