Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

5530 lines (4536 sloc) 130.148 kB
/* Source code for an implementation of the Omega test, an integer
programming algorithm for dependence analysis, by William Pugh,
appeared in Supercomputing '91 and CACM Aug 92.
This code has no license restrictions, and is considered public
domain.
Changes copyright (C) 2005, 2006, 2007, 2008, 2009,
2010 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 "tree.h"
#include "diagnostic-core.h"
#include "tree-pass.h"
#include "omega.h"
/* When set to true, keep substitution variables. When set to false,
resurrect substitution variables (convert substitutions back to EQs). */
static bool omega_reduce_with_subs = true;
/* When set to true, omega_simplify_problem checks for problem with no
solutions, calling verify_omega_pb. */
static bool omega_verify_simplification = false;
/* When set to true, only produce a single simplified result. */
static bool omega_single_result = false;
/* Set return_single_result to 1 when omega_single_result is true. */
static int return_single_result = 0;
/* Hash table for equations generated by the solver. */
#define HASH_TABLE_SIZE PARAM_VALUE (PARAM_OMEGA_HASH_TABLE_SIZE)
#define MAX_KEYS PARAM_VALUE (PARAM_OMEGA_MAX_KEYS)
static eqn hash_master;
static int next_key;
static int hash_version = 0;
/* Set to true for making the solver enter in approximation mode. */
static bool in_approximate_mode = false;
/* When set to zero, the solver is allowed to add new equalities to
the problem to be solved. */
static int conservative = 0;
/* Set to omega_true when the problem was successfully reduced, set to
omega_unknown when the solver is unable to determine an answer. */
static enum omega_result omega_found_reduction;
/* Set to true when the solver is allowed to add omega_red equations. */
static bool create_color = false;
/* Set to nonzero when the problem to be solved can be reduced. */
static int may_be_red = 0;
/* When false, there should be no substitution equations in the
simplified problem. */
static int please_no_equalities_in_simplified_problems = 0;
/* Variables names for pretty printing. */
static char wild_name[200][40];
/* Pointer to the void problem. */
static omega_pb no_problem = (omega_pb) 0;
/* Pointer to the problem to be solved. */
static omega_pb original_problem = (omega_pb) 0;
/* Return the integer A divided by B. */
static inline int
int_div (int a, int b)
{
if (a > 0)
return a/b;
else
return -((-a + b - 1)/b);
}
/* Return the integer A modulo B. */
static inline int
int_mod (int a, int b)
{
return a - b * int_div (a, b);
}
/* 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");
}
/* 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)
{
v3 = v2;
v2 = v1;
v1 = v3;
}
/* Relation is v1 <= v2 or v1 < v2. */
po[v1][v2] = ((pb->geqs[e].coef[0] == 0) ? le : lt);
po_eq[v1][v2] = e;
}
}
for (v = 1; v <= pb->num_vars; v++)
chain_length[v] = last_links[v];
/* Just in case pb->num_vars <= 0. */
change = false;
for (t = 0; t < pb->num_vars; t++)
{
change = false;
for (v1 = 1; v1 <= pb->num_vars; v1++)
for (v2 = 1; v2 <= pb->num_vars; v2++)
if (po[v1][v2] != none &&
chain_length[v1] <= chain_length[v2])
{
chain_length[v1] = chain_length[v2] + 1;
change = true;
}
}
/* Caught in cycle. */
gcc_assert (!change);
for (v1 = 1; v1 <= pb->num_vars; v1++)
if (chain_length[v1] == 0)
first_links[v1] = 0;
v = 1;
for (v1 = 2; v1 <= pb->num_vars; v1++)
if (chain_length[v1] + first_links[v1] >
chain_length[v] + first_links[v])
v = v1;
if (chain_length[v] + first_links[v] == 0)
break;
if (stuffPrinted)
fprintf (file, "; ");
stuffPrinted = 1;
/* Chain starts at v. */
{
int tmp;
bool first = true;
for (e = 0; e < pb->num_geqs; e++)
if (live[e] && pb->geqs[e].coef[v] == 1)
{
if (!first)
fprintf (file, ", ");
tmp = pb->geqs[e].coef[v];
pb->geqs[e].coef[v] = 0;
omega_print_term (file, pb, &pb->geqs[e], -1);
pb->geqs[e].coef[v] = tmp;
live[e] = false;
first = false;
}
if (!first)
fprintf (file, " <= ");
}
/* Find chain. */
chain[0] = v;
m = 1;
while (1)
{
/* Print chain. */
for (v2 = 1; v2 <= pb->num_vars; v2++)
if (po[v][v2] && chain_length[v] == 1 + chain_length[v2])
break;
if (v2 > pb->num_vars)
break;
chain[m++] = v2;
v = v2;
}
fprintf (file, "%s", omega_variable_to_str (pb, chain[0]));
for (multiprint = false, i = 1; i < m; i++)
{
v = chain[i - 1];
v2 = chain[i];
if (po[v][v2] == le)
fprintf (file, " <= ");
else
fprintf (file, " < ");
fprintf (file, "%s", omega_variable_to_str (pb, v2));
live[po_eq[v][v2]] = false;
if (!multiprint && i < m - 1)
for (v3 = 1; v3 <= pb->num_vars; v3++)
{
if (v == v3 || v2 == v3
|| po[v][v2] != po[v][v3]
|| po[v2][chain[i + 1]] != po[v3][chain[i + 1]])
continue;
fprintf (file, ",%s", omega_variable_to_str (pb, v3));
live[po_eq[v][v3]] = false;
live[po_eq[v3][chain[i + 1]]] = false;
multiprint = true;
}
else
multiprint = false;
}
v = chain[m - 1];
/* Print last_links. */
{
int tmp;
bool first = true;
for (e = 0; e < pb->num_geqs; e++)
if (live[e] && pb->geqs[e].coef[v] == -1)
{
if (!first)
fprintf (file, ", ");
else
fprintf (file, " <= ");
tmp = pb->geqs[e].coef[v];
pb->geqs[e].coef[v] = 0;
omega_print_term (file, pb, &pb->geqs[e], 1);
pb->geqs[e].coef[v] = tmp;
live[e] = false;
first = false;
}
}
}
for (e = 0; e < pb->num_geqs; e++)
if (live[e])
{
if (stuffPrinted)
fprintf (file, "; ");
stuffPrinted = 1;
omega_print_geq (file, pb, &pb->geqs[e]);
}
for (e = 0; e < pb->num_subs; e++)
{
eqn eq = &pb->subs[e];
if (stuffPrinted)
fprintf (file, "; ");
stuffPrinted = 1;
if (eq->key > 0)
fprintf (file, "%s := ", omega_var_to_str (eq->key));
else
fprintf (file, "#%d := ", eq->key);
omega_print_term (file, pb, eq, 1);
}
}
free (live);
free (po);
free (po_eq);
free (last_links);
free (first_links);
free (chain_length);
free (chain);
}
/* Assign to variable I in PB the next wildcard name. The name of a
wildcard is a negative number. */
static int next_wild_card = 0;
static void
omega_name_wild_card (omega_pb pb, int i)
{
--next_wild_card;
if (next_wild_card < -PARAM_VALUE (PARAM_OMEGA_MAX_WILD_CARDS))
next_wild_card = -1;
pb->var[i] = next_wild_card;
}
/* Return the index of the last protected (or safe) variable in PB,
after having added a new wildcard variable. */
static int
omega_add_new_wild_card (omega_pb pb)
{
int e;
int i = ++pb->safe_vars;
pb->num_vars++;
/* Make a free place in the protected (safe) variables, by moving
the non protected variable pointed by "I" at the end, ie. at
offset pb->num_vars. */
if (pb->num_vars != i)
{
/* Move "I" for all the inequalities. */
for (e = pb->num_geqs - 1; e >= 0; e--)
{
if (pb->geqs[e].coef[i])
pb->geqs[e].touched = 1;
pb->geqs[e].coef[pb->num_vars] = pb->geqs[e].coef[i];
}
/* Move "I" for all the equalities. */
for (e = pb->num_eqs - 1; e >= 0; e--)
pb->eqs[e].coef[pb->num_vars] = pb->eqs[e].coef[i];
/* Move "I" for all the substitutions. */
for (e = pb->num_subs - 1; e >= 0; e--)
pb->subs[e].coef[pb->num_vars] = pb->subs[e].coef[i];
/* Move the identifier. */
pb->var[pb->num_vars] = pb->var[i];
}
/* Initialize at zero all the coefficients */
for (e = pb->num_geqs - 1; e >= 0; e--)
pb->geqs[e].coef[i] = 0;
for (e = pb->num_eqs - 1; e >= 0; e--)
pb->eqs[e].coef[i] = 0;
for (e = pb->num_subs - 1; e >= 0; e--)
pb->subs[e].coef[i] = 0;
/* And give it a name. */
omega_name_wild_card (pb, i);
return i;
}
/* Delete inequality E from problem PB that has N_VARS variables. */
static void
omega_delete_geq (omega_pb pb, int e, int n_vars)
{
if (dump_file && (dump_flags & TDF_DETAILS))
{
fprintf (dump_file, "Deleting %d (last:%d): ", e, pb->num_geqs - 1);
omega_print_geq (dump_file, pb, &pb->geqs[e]);
fprintf (dump_file, "\n");
}
if (e < pb->num_geqs - 1)
omega_copy_eqn (&pb->geqs[e], &pb->geqs[pb->num_geqs - 1], n_vars);
pb->num_geqs--;
}
/* Delete extra inequality E from problem PB that has N_VARS
variables. */
static void
omega_delete_geq_extra (omega_pb pb, int e, int n_vars)
{
if (dump_file && (dump_flags & TDF_DETAILS))
{
fprintf (dump_file, "Deleting %d: ",e);
omega_print_geq_extra (dump_file, pb, &pb->geqs[e]);
fprintf (dump_file, "\n");
}
if (e < pb->num_geqs - 1)
omega_copy_eqn (&pb->geqs[e], &pb->geqs[pb->num_geqs - 1], n_vars);
pb->num_geqs--;
}
/* Remove variable I from problem PB. */
static void
omega_delete_variable (omega_pb pb, int i)
{
int n_vars = pb->num_vars;
int e;
if (omega_safe_var_p (pb, i))
{
int j = pb->safe_vars;
for (e = pb->num_geqs - 1; e >= 0; e--)
{
pb->geqs[e].touched = 1;
pb->geqs[e].coef[i] = pb->geqs[e].coef[j];
pb->geqs[e].coef[j] = pb->geqs[e].coef[n_vars];
}
for (e = pb->num_eqs - 1; e >= 0; e--)
{
pb->eqs[e].coef[i] = pb->eqs[e].coef[j];
pb->eqs[e].coef[j] = pb->eqs[e].coef[n_vars];
}
for (e = pb->num_subs - 1; e >= 0; e--)
{
pb->subs[e].coef[i] = pb->subs[e].coef[j];
pb->subs[e].coef[j] = pb->subs[e].coef[n_vars];
}
pb->var[i] = pb->var[j];
pb->var[j] = pb->var[n_vars];
}
else if (i < n_vars)
{
for (e = pb->num_geqs - 1; e >= 0; e--)
if (pb->geqs[e].coef[n_vars])
{
pb->geqs[e].coef[i] = pb->geqs[e].coef[n_vars];
pb->geqs[e].touched = 1;
}
for (e = pb->num_eqs - 1; e >= 0; e--)
pb->eqs[e].coef[i] = pb->eqs[e].coef[n_vars];
for (e = pb->num_subs - 1; e >= 0; e--)
pb->subs[e].coef[i] = pb->subs[e].coef[n_vars];
pb->var[i] = pb->var[n_vars];
}
if (omega_safe_var_p (pb, i))
pb->safe_vars--;
pb->num_vars--;
}
/* Because the coefficients of an equation are sparse, PACKING records
indices for non null coefficients. */
static int *packing;
/* Set up the coefficients of PACKING, following the coefficients of
equation EQN that has NUM_VARS variables. */
static inline int
setup_packing (eqn eqn, int num_vars)
{
int k;
int n = 0;
for (k = num_vars; k >= 0; k--)
if (eqn->coef[k])
packing[n++] = k;
return n;
}
/* Computes a linear combination of EQ and SUB at VAR with coefficient
C, such that EQ->coef[VAR] is set to 0. TOP_VAR is the number of
non null indices of SUB stored in PACKING. */
static inline void
omega_substitute_red_1 (eqn eq, eqn sub, int var, int c, bool *found_black,
int top_var)
{
if (eq->coef[var] != 0)
{
if (eq->color == omega_black)
*found_black = true;
else
{
int j, k = eq->coef[var];
eq->coef[var] = 0;
for (j = top_var; j >= 0; j--)
eq->coef[packing[j]] -= sub->coef[packing[j]] * k * c;
}
}
}
/* Substitute in PB variable VAR with "C * SUB". */
static void
omega_substitute_red (omega_pb pb, eqn sub, int var, int c, bool *found_black)
{
int e, top_var = setup_packing (sub, pb->num_vars);
*found_black = false;
if (dump_file && (dump_flags & TDF_DETAILS))
{
if (sub->color == omega_red)
fprintf (dump_file, "[");
fprintf (dump_file, "substituting using %s := ",
omega_variable_to_str (pb, var));
omega_print_term (dump_file, pb, sub, -c);
if (sub->color == omega_red)
fprintf (dump_file, "]");
fprintf (dump_file, "\n");
omega_print_vars (dump_file, pb);
}
for (e = pb->num_eqs - 1; e >= 0; e--)
{
eqn eqn = &(pb->eqs[e]);
omega_substitute_red_1 (eqn, sub, var, c, found_black, top_var);
if (dump_file && (dump_flags & TDF_DETAILS))
{
omega_print_eq (dump_file, pb, eqn);
fprintf (dump_file, "\n");
}
}
for (e = pb->num_geqs - 1; e >= 0; e--)
{
eqn eqn = &(pb->geqs[e]);
omega_substitute_red_1 (eqn, sub, var, c, found_black, top_var);
if (eqn->coef[var] && eqn->color == omega_red)
eqn->touched = 1;
if (dump_file && (dump_flags & TDF_DETAILS))
{
omega_print_geq (dump_file, pb, eqn);
fprintf (dump_file, "\n");
}
}
for (e = pb->num_subs - 1; e >= 0; e--)
{
eqn eqn = &(pb->subs[e]);
omega_substitute_red_1 (eqn, sub, var, c, found_black, top_var);
if (dump_file && (dump_flags & TDF_DETAILS))
{
fprintf (dump_file, "%s := ", omega_var_to_str (eqn->key));
omega_print_term (dump_file, pb, eqn, 1);
fprintf (dump_file, "\n");
}
}
if (dump_file && (dump_flags & TDF_DETAILS))
fprintf (dump_file, "---\n\n");
if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
*found_black = true;
}
/* Substitute in PB variable VAR with "C * SUB". */
static void
omega_substitute (omega_pb pb, eqn sub, int var, int c)
{
int e, j, j0;
int top_var = setup_packing (sub, pb->num_vars);
if (dump_file && (dump_flags & TDF_DETAILS))
{
fprintf (dump_file, "substituting using %s := ",
omega_variable_to_str (pb, var));
omega_print_term (dump_file, pb, sub, -c);
fprintf (dump_file, "\n");
omega_print_vars (dump_file, pb);
}
if (top_var < 0)
{
for (e = pb->num_eqs - 1; e >= 0; e--)
pb->eqs[e].coef[var] = 0;
for (e = pb->num_geqs - 1; e >= 0; e--)
if (pb->geqs[e].coef[var] != 0)
{
pb->geqs[e].touched = 1;
pb->geqs[e].coef[var] = 0;
}
for (e = pb->num_subs - 1; e >= 0; e--)
pb->subs[e].coef[var] = 0;
if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
{
int k;
eqn eqn = &(pb->subs[pb->num_subs++]);
for (k = pb->num_vars; k >= 0; k--)
eqn->coef[k] = 0;
eqn->key = pb->var[var];
eqn->color = omega_black;
}
}
else if (top_var == 0 && packing[0] == 0)
{
c = -sub->coef[0] * c;
for (e = pb->num_eqs - 1; e >= 0; e--)
{
pb->eqs[e].coef[0] += pb->eqs[e].coef[var] * c;
pb->eqs[e].coef[var] = 0;
}
for (e = pb->num_geqs - 1; e >= 0; e--)
if (pb->geqs[e].coef[var] != 0)
{
pb->geqs[e].coef[0] += pb->geqs[e].coef[var] * c;
pb->geqs[e].coef[var] = 0;
pb->geqs[e].touched = 1;
}
for (e = pb->num_subs - 1; e >= 0; e--)
{
pb->subs[e].coef[0] += pb->subs[e].coef[var] * c;
pb->subs[e].coef[var] = 0;
}
if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
{
int k;
eqn eqn = &(pb->subs[pb->num_subs++]);
for (k = pb->num_vars; k >= 1; k--)
eqn->coef[k] = 0;
eqn->coef[0] = c;
eqn->key = pb->var[var];
eqn->color = omega_black;
}
if (dump_file && (dump_flags & TDF_DETAILS))
{
fprintf (dump_file, "---\n\n");
omega_print_problem (dump_file, pb);
fprintf (dump_file, "===\n\n");
}
}
else
{
for (e = pb->num_eqs - 1; e >= 0; e--)
{
eqn eqn = &(pb->eqs[e]);
int k = eqn->coef[var];
if (k != 0)
{
k = c * k;
eqn->coef[var] = 0;
for (j = top_var; j >= 0; j--)
{
j0 = packing[j];
eqn->coef[j0] -= sub->coef[j0] * k;
}
}
if (dump_file && (dump_flags & TDF_DETAILS))
{
omega_print_eq (dump_file, pb, eqn);
fprintf (dump_file, "\n");
}
}
for (e = pb->num_geqs - 1; e >= 0; e--)
{
eqn eqn = &(pb->geqs[e]);
int k = eqn->coef[var];
if (k != 0)
{
k = c * k;
eqn->touched = 1;
eqn->coef[var] = 0;
for (j = top_var; j >= 0; j--)
{
j0 = packing[j];
eqn->coef[j0] -= sub->coef[j0] * k;
}
}
if (dump_file && (dump_flags & TDF_DETAILS))
{
omega_print_geq (dump_file, pb, eqn);
fprintf (dump_file, "\n");
}
}
for (e = pb->num_subs - 1; e >= 0; e--)
{
eqn eqn = &(pb->subs[e]);
int k = eqn->coef[var];
if (k != 0)
{
k = c * k;
eqn->coef[var] = 0;
for (j = top_var; j >= 0; j--)
{
j0 = packing[j];
eqn->coef[j0] -= sub->coef[j0] * k;
}
}
if (dump_file && (dump_flags & TDF_DETAILS))
{
fprintf (dump_file, "%s := ", omega_var_to_str (eqn->key));
omega_print_term (dump_file, pb, eqn, 1);
fprintf (dump_file, "\n");
}
}
if (dump_file && (dump_flags & TDF_DETAILS))
{
fprintf (dump_file, "---\n\n");
omega_print_problem (dump_file, pb);
fprintf (dump_file, "===\n\n");
}
if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
{
int k;
eqn eqn = &(pb->subs[pb->num_subs++]);
c = -c;
for (k = pb->num_vars; k >= 0; k--)
eqn->coef[k] = c * (sub->coef[k]);
eqn->key = pb->var[var];
eqn->color = sub->color;
}
}
}
/* Solve e = factor alpha for x_j and substitute. */
static void
omega_do_mod (omega_pb pb, int factor, int e, int j)
{
int k, i;
eqn eq = omega_alloc_eqns (0, 1);
int nfactor;
bool kill_j = false;
omega_copy_eqn (eq, &pb->eqs[e], pb->num_vars);
for (k = pb->num_vars; k >= 0; k--)
{
eq->coef[k] = int_mod (eq->coef[k], factor);
if (2 * eq->coef[k] >= factor)
eq->coef[k] -= factor;
}
nfactor = eq->coef[j];
if (omega_safe_var_p (pb, j) && !omega_wildcard_p (pb, j))
{
i = omega_add_new_wild_card (pb);
eq->coef[pb->num_vars] = eq->coef[i];
eq->coef[j] = 0;
eq->coef[i] = -factor;
kill_j = true;
}
else
{
eq->coef[j] = -factor;
if (!omega_wildcard_p (pb, j))
omega_name_wild_card (pb, j);
}
omega_substitute (pb, eq, j, nfactor);
for (k = pb->num_vars; k >= 0; k--)
pb->eqs[e].coef[k] = pb->eqs[e].coef[k] / factor;
if (kill_j)
omega_delete_variable (pb, j);
if (dump_file && (dump_flags & TDF_DETAILS))
{
fprintf (dump_file, "Mod-ing and normalizing produces:\n");
omega_print_problem (dump_file, pb);
}
omega_free_eqns (eq, 1);
}
/* Multiplies by -1 inequality E. */
void
omega_negate_geq (omega_pb pb, int e)
{
int i;
for (i = pb->num_vars; i >= 0; i--)
pb->geqs[e].coef[i] *= -1;
pb->geqs[e].coef[0]--;
pb->geqs[e].touched = 1;
}
/* Returns OMEGA_TRUE when problem PB has a solution. */
static enum omega_result
verify_omega_pb (omega_pb pb)
{
enum omega_result result;
int e;
bool any_color = false;
omega_pb tmp_problem = XNEW (struct omega_pb_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);
}
/* Swap values contained in I and J. */
static inline void
swap (int *i, int *j)
{
int tmp;
tmp = *i;
*i = *j;
*j = tmp;
}
/* Swap values contained in I and J. */
static inline void
bswap (bool *i, bool *j)
{
bool tmp;
tmp = *i;
*i = *j;
*j = tmp;
}
/* Make variable IDX unprotected in PB, by swapping its index at the
PB->safe_vars rank. */
static inline void
omega_unprotect_1 (omega_pb pb, int *idx, bool *unprotect)
{
/* If IDX is protected... */
if (*idx < pb->safe_vars)
{
/* ... swap its index with the last non protected index. */
int j = pb->safe_vars;
int e;
for (e = pb->num_geqs - 1; e >= 0; e--)
{
pb->geqs[e].touched = 1;
swap (&pb->geqs[e].coef[*idx], &pb->geqs[e].coef[j]);
}
for (e = pb->num_eqs - 1; e >= 0; e--)
swap (&pb->eqs[e].coef[*idx], &pb->eqs[e].coef[j]);
for (e = pb->num_subs - 1; e >= 0; e--)
swap (&pb->subs[e].coef[*idx], &pb->subs[e].coef[j]);
if (unprotect)
bswap (&unprotect[*idx], &unprotect[j]);
swap (&pb->var[*idx], &pb->var[j]);
pb->forwarding_address[pb->var[*idx]] = *idx;
pb->forwarding_address[pb->var[j]] = j;
(*idx)--;
}
/* The variable at pb->safe_vars is also unprotected now. */
pb->safe_vars--;
}
/* During the Fourier-Motzkin elimination some variables are
substituted with other variables. This function resurrects the
substituted variables in PB. */
static void
resurrect_subs (omega_pb pb)
{
if (pb->num_subs > 0
&& please_no_equalities_in_simplified_problems == 0)
{
int i, e, 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;
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 t;
int j = pb->num_vars;
if (dump_file && (dump_flags & TDF_DETAILS))
{
fprintf (dump_file, "Swapping %d and %d\n", i, j);
omega_print_problem (dump_file, pb);
}
swap (&pb->var[i], &pb->var[j]);
for (e = pb->num_geqs - 1; e >= 0; e--)
if (pb->geqs[e].coef[i] != pb->geqs[e].coef[j])
{
pb->geqs[e].touched = 1;
t = pb->geqs[e].coef[i];
pb->geqs[e].coef[i] = pb->geqs[e].coef[j];
pb->geqs[e].coef[j] = t;
}
for (e = pb->num_subs - 1; e >= 0; e--)
if (pb->subs[e].coef[i] != pb->subs[e].coef[j])
{
t = pb->subs[e].coef[i];
pb->subs[e].coef[i] = pb->subs[e].coef[j];
pb->subs[e].coef[j] = t;
}
if (dump_file && (dump_flags & TDF_DETAILS))
{
fprintf (dump_file, "Swapping complete \n");
omega_print_problem (dump_file, pb);
fprintf (dump_file, "\n");
}
i = j;
}
else if (dump_file && (dump_flags & TDF_DETAILS))
{
fprintf (dump_file, "No swap needed\n");
omega_print_problem (dump_file, pb);
}
pb->num_vars--;
n_vars = pb->num_vars;
if (exact)
{
if (n_vars == 1)
{
int upper_bound = pos_infinity;
int lower_bound = neg_infinity;
enum omega_eqn_color ub_color = omega_black;
enum omega_eqn_color lb_color = omega_black;
int topeqn = pb->num_geqs - 1;
int Lc = pb->geqs[Le].coef[i];
for (Le = topeqn; Le >= 0; Le--)
if ((Lc = pb->geqs[Le].coef[i]) == 0)
{
if (pb->geqs[Le].coef[1] == 1)
{
int constantTerm = -pb->geqs[Le].coef[0];
if (constantTerm > lower_bound ||
(constantTerm == lower_bound &&
!omega_eqn_is_red (&pb->geqs[Le], desired_res)))
{
lower_bound = constantTerm;
lb_color = pb->geqs[Le].color;
}
if (dump_file && (dump_flags & TDF_DETAILS))
{
if (pb->geqs[Le].color == omega_black)
fprintf (dump_file, " :::=> %s >= %d\n",
omega_variable_to_str (pb, 1),
constantTerm);
else
fprintf (dump_file,
" :::=> [%s >= %d]\n",
omega_variable_to_str (pb, 1),
constantTerm);
}
}
else
{
int constantTerm = pb->geqs[Le].coef[0];
if (constantTerm < upper_bound ||
(constantTerm == upper_bound
&& !omega_eqn_is_red (&pb->geqs[Le],
desired_res)))
{
upper_bound = constantTerm;
ub_color = pb->geqs[Le].color;
}
if (dump_file && (dump_flags & TDF_DETAILS))
{
if (pb->geqs[Le].color == omega_black)
fprintf (dump_file, " :::=> %s <= %d\n",
omega_variable_to_str (pb, 1),
constantTerm);
else
fprintf (dump_file,
" :::=> [%s <= %d]\n",
omega_variable_to_str (pb, 1),
constantTerm);
}
}
}
else if (Lc > 0)
for (Ue = topeqn; Ue >= 0; Ue--)
if (pb->geqs[Ue].coef[i] < 0
&& pb->geqs[Le].key != -pb->geqs[Ue].key)
{
int Uc = -pb->geqs[Ue].coef[i];
int coefficient = pb->geqs[Ue].coef[1] * Lc
+ pb->geqs[Le].coef[1] * Uc;
int constantTerm = pb->geqs[Ue].coef[0] * Lc
+ pb->geqs[Le].coef[0] * Uc;
if (dump_file && (dump_flags & TDF_DETAILS))
{
omega_print_geq_extra (dump_file, pb,
&(pb->geqs[Ue]));
fprintf (dump_file, "\n");
omega_print_geq_extra (dump_file, pb,
&(pb->geqs[Le]));
fprintf (dump_file, "\n");
}
if (coefficient > 0)
{
constantTerm = -int_div (constantTerm, coefficient);
if (constantTerm > lower_bound
|| (constantTerm == lower_bound
&& (desired_res != omega_simplify
|| (pb->geqs[Ue].color == omega_black
&& pb->geqs[Le].color == omega_black))))
{
lower_bound = constantTerm;
lb_color = (pb->geqs[Ue].color == omega_red
|| pb->geqs[Le].color == omega_red)
? omega_red : omega_black;
}
if (dump_file && (dump_flags & TDF_DETAILS))
{
if (pb->geqs[Ue].color == omega_red
|| pb->geqs[Le].color == omega_red)
fprintf (dump_file,
" ::=> [%s >= %d]\n",
omega_variable_to_str (pb, 1),
constantTerm);
else
fprintf (dump_file,
" ::=> %s >= %d\n",
omega_variable_to_str (pb, 1),
constantTerm);
}
}
else
{
constantTerm = int_div (constantTerm, -coefficient);
if (constantTerm < upper_bound
|| (constantTerm == upper_bound
&& pb->geqs[Ue].color == omega_black
&& pb->geqs[Le].color == omega_black))
{
upper_bound = constantTerm;
ub_color = (pb->geqs[Ue].color == omega_red
|| pb->geqs[Le].color == omega_red)
? omega_red : omega_black;
}
if (dump_file
&& (dump_flags & TDF_DETAILS))
{
if (pb->geqs[Ue].color == omega_red
|| pb->geqs[Le].color == omega_red)
fprintf (dump_file,
" ::=> [%s <= %d]\n",
omega_variable_to_str (pb, 1),
constantTerm);
else
fprintf (dump_file,
" ::=> %s <= %d\n",
omega_variable_to_str (pb, 1),
constantTerm);
}
}
}
pb->num_geqs = 0;
if (dump_file && (dump_flags & TDF_DETAILS))
fprintf (dump_file,
" therefore, %c%d <= %c%s%c <= %d%c\n",
lb_color == omega_red ? '[' : ' ', lower_bound,
(lb_color == omega_red && ub_color == omega_black)
? ']' : ' ',
omega_variable_to_str (pb, 1),
(lb_color == omega_black && ub_color == omega_red)
? '[' : ' ',
upper_bound, ub_color == omega_red ? ']' : ' ');
if (lower_bound > upper_bound)
return omega_false;
if (pb->safe_vars == 1)
{
if (upper_bound == lower_bound
&& !(ub_color == omega_red || lb_color == omega_red)
&& !please_no_equalities_in_simplified_problems)
{
pb->num_eqs++;
pb->eqs[0].coef[1] = -1;
pb->eqs[0].coef[0] = upper_bound;
if (ub_color == omega_red
|| lb_color == omega_red)
pb->eqs[0].color = omega_red;
if (desired_res == omega_simplify
&& pb->eqs[0].color == omega_black)
return omega_solve_problem (pb, desired_res);
}
if (upper_bound != pos_infinity)
{
pb->geqs[0].coef[1] = -1;
pb->geqs[0].coef[0] = upper_bound;
pb->geqs[0].color = ub_color;
pb->geqs[0].key = -1;
pb->geqs[0].touched = 0;
pb->num_geqs++;
}
if (lower_bound != neg_infinity)
{
pb->geqs[pb->num_geqs].coef[1] = 1;
pb->geqs[pb->num_geqs].coef[0] = -lower_bound;
pb->geqs[pb->num_geqs].color = lb_color;
pb->geqs[pb->num_geqs].key = 1;
pb->geqs[pb->num_geqs].touched = 0;
pb->num_geqs++;
}
}
if (desired_res == omega_simplify)
{
omega_problem_reduced (pb);
return omega_false;
}
else
{
if (!conservative
&& (desired_res != omega_simplify
|| (lb_color == omega_black
&& ub_color == omega_black))
&& original_problem != no_problem
&& lower_bound == upper_bound)
{
for (i = original_problem->num_vars; i >= 0; i--)
if (original_problem->var[i] == pb->var[1])
break;
if (i == 0)
break;
e = original_problem->num_eqs++;