+++ /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-2015 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 "alias.h"
-#include "tree.h"
-#include "options.h"
-#include "diagnostic-core.h"
-#include "dumpfile.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);
-}
-
-/* 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;
-
-/* 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");
-}
-
-/* Dump problem PB. */
-
-DEBUG_FUNCTION void
-debug (omega_pb_d &ref)
-{
- omega_print_problem (stderr, &ref);
-}
-
-DEBUG_FUNCTION void
-debug (omega_pb_d *ptr)
-{
- if (ptr)
- debug (*ptr);
- else
- fprintf (stderr, "<nil>\n");
-}
-
-/* Debug problem PB. */
-
-DEBUG_FUNCTION 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)
- std::swap (v1, v2);
-
- /* 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_d);
-
- 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);
-}
-
-/* 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;
- std::swap (pb->geqs[e].coef[*idx], pb->geqs[e].coef[j]);
- }
-
- for (e = pb->num_eqs - 1; e >= 0; e--)
- std::swap (pb->eqs[e].coef[*idx], pb->eqs[e].coef[j]);
-
- for (e = pb->num_subs - 1; e >= 0; e--)
- std::swap (pb->subs[e].coef[*idx], pb->subs[e].coef[j]);
-
- if (unprotect)
- std::swap (unprotect[*idx], unprotect[j]);
-
- std::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, 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;
-
- 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;
-
- /* 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_d);
- 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;
- break;
- }
-
- 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_d);
-
- 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;
- if (sub->color == omega_red)
- eqn->color = omega_red;
- 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_d);
- 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 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)
- {
- 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);
-
- 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 +=
- pos_mul_hwi ((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 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);
- }
-
- std::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;
- std::swap (pb->geqs[e].coef[i], pb->geqs[e].coef[j]);
- }
-
- for (e = pb->num_subs - 1; e >= 0; e--)
- if (pb->subs[e].coef[i] != pb->subs[e].coef[j])
- std::swap (pb->subs[e].coef[i], pb->subs[e].coef[j]);
-
- 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] =
- mul_hwi (pb->geqs[Ue].coef[k], Lc) +
- mul_hwi (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] =
- mul_hwi (pb->geqs[Ue].coef[k], Lc) +
- mul_hwi (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] =
- mul_hwi (pb->geqs[Ue].coef[k], Lc) +
- mul_hwi (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 smallest = j;
-
- for (int k = j + 1; k < lower_bounds; k++)
- if (pb->geqs[lower_bound[smallest]].coef[i] >
- pb->geqs[lower_bound[k]].coef[i])
- smallest = k;
-
- std::swap (lower_bound[smallest], lower_bound[j]);
- }
-
- 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;
- break;
- }
-
- 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;
- break;
- }
-
- 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;
- break;
- }
-
- 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_d);
- 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 / gcc.git / commitdiff