From: Sebastian Pop Date: Sat, 18 Jul 2015 01:11:05 +0000 (+0000) Subject: fix pr46851 and pr60340: remove unmaintained omega dependence test X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=49b8fe6c1a585edfeb5dd0f292e05a167f475f68;p=gcc.git fix pr46851 and pr60340: remove unmaintained omega dependence test Regstrapped on amd64-linux. 2015-07-18 Sebastian Pop PR middle-end/46851 PR middle-end/60340 * Makefile.in: Removed omega.o. * common.opt: Remove flag fcheck-data-deps. * doc/invoke.texi: Remove documentation for fcheck-data-deps and its associated params: omega-max-vars, omega-max-geqs, omega-max-eqs, omega-max-wild-cards, omega-hash-table-size, omega-max-keys, omega-eliminate-redundant-constraints. * doc/loop.texi: Remove all the section on Omega. * graphite-blocking.c: Include missing params.h: it used to be included through tree-data-ref.h and omega.h. * graphite-isl-ast-to-gimple.c: Same. * graphite-optimize-isl.c: Same. * graphite-sese-to-poly.c: Same. * graphite.c: Same. * omega.c: Remove. * omega.h: Remove. * params.def: Removed PARAM_OMEGA_MAX_VARS, PARAM_OMEGA_MAX_GEQS, PARAM_OMEGA_MAX_EQS, PARAM_OMEGA_MAX_WILD_CARDS, PARAM_OMEGA_HASH_TABLE_SIZE, PARAM_OMEGA_MAX_KEYS, and PARAM_OMEGA_ELIMINATE_REDUNDANT_CONSTRAINTS. * passes.def: Remove pass_check_data_deps. * tree-data-ref.c (dump_affine_function): Declare DEBUG_FUNCTION. (dump_conflict_function): Same. (dump_subscript): Same. (print_direction_vector): Same. (print_dir_vectors): Same. (print_lambda_vector): Same. (print_dist_vectors): Same. (dump_data_dependence_relation): Same. (dump_data_dependence_relations): Same. (dump_dist_dir_vectors): Same. (dump_ddrs): Same. (init_omega_eq_with_af): Removed. (omega_extract_distance_vectors): Removed. (omega_setup_subscript): Removed. (init_omega_for_ddr_1): Removed. (init_omega_for_ddr): Removed. (ddr_consistent_p): Removed. (compute_affine_dependence): Do not use omega to check data dependences. (compute_data_dependences_for_bb): Removed. (analyze_all_data_dependences): Removed. (tree_check_data_deps): Removed. * tree-data-ref.h: Do not include omega.h. (compute_data_dependences_for_bb): Removed. (tree_check_data_deps): Removed. * tree-ssa-loop.c (pass_check_data_deps): Removed. (make_pass_check_data_deps): Removed. * tree-ssa-phiopt.c: Include params.h. * tree-vect-data-refs.c: Same. * tree-vect-slp.c: Same. testsuite/ * gcc.dg/tree-ssa/pr42327.c: Removed. * g++.dg/other/pr35011.C: Removed. From-SVN: r225979 --- diff --git a/gcc/ChangeLog b/gcc/ChangeLog index f0854ae15f0..98fb37bb2a8 100644 --- a/gcc/ChangeLog +++ b/gcc/ChangeLog @@ -1,3 +1,58 @@ +2015-07-18 Sebastian Pop + + PR middle-end/46851 + PR middle-end/60340 + * Makefile.in: Removed omega.o. + * common.opt: Document flag fcheck-data-deps as deprecated. + * doc/invoke.texi: Remove documentation for fcheck-data-deps and + its associated params: omega-max-vars, omega-max-geqs, + omega-max-eqs, omega-max-wild-cards, omega-hash-table-size, + omega-max-keys, omega-eliminate-redundant-constraints. + * doc/loop.texi: Remove all the section on Omega. + * graphite-blocking.c: Include missing params.h: it used to be + included through tree-data-ref.h and omega.h. + * graphite-isl-ast-to-gimple.c: Same. + * graphite-optimize-isl.c: Same. + * graphite-sese-to-poly.c: Same. + * graphite.c: Same. + * omega.c: Remove. + * omega.h: Remove. + * params.def: Removed PARAM_OMEGA_MAX_VARS, PARAM_OMEGA_MAX_GEQS, + PARAM_OMEGA_MAX_EQS, PARAM_OMEGA_MAX_WILD_CARDS, + PARAM_OMEGA_HASH_TABLE_SIZE, PARAM_OMEGA_MAX_KEYS, and + PARAM_OMEGA_ELIMINATE_REDUNDANT_CONSTRAINTS. + * passes.def: Remove pass_check_data_deps. + * tree-data-ref.c (dump_affine_function): Declare DEBUG_FUNCTION. + (dump_conflict_function): Same. + (dump_subscript): Same. + (print_direction_vector): Same. + (print_dir_vectors): Same. + (print_lambda_vector): Same. + (print_dist_vectors): Same. + (dump_data_dependence_relation): Same. + (dump_data_dependence_relations): Same. + (dump_dist_dir_vectors): Same. + (dump_ddrs): Same. + (init_omega_eq_with_af): Removed. + (omega_extract_distance_vectors): Removed. + (omega_setup_subscript): Removed. + (init_omega_for_ddr_1): Removed. + (init_omega_for_ddr): Removed. + (ddr_consistent_p): Removed. + (compute_affine_dependence): Do not use omega to check data + dependences. + (compute_data_dependences_for_bb): Removed. + (analyze_all_data_dependences): Removed. + (tree_check_data_deps): Removed. + * tree-data-ref.h: Do not include omega.h. + (compute_data_dependences_for_bb): Removed. + (tree_check_data_deps): Removed. + * tree-ssa-loop.c (pass_check_data_deps): Removed. + (make_pass_check_data_deps): Removed. + * tree-ssa-phiopt.c: Include params.h. + * tree-vect-data-refs.c: Same. + * tree-vect-slp.c: Same. + 2015-07-18 Uros Bizjak * config/i386/i386.md (pushsf splitter): Pass curr_insn to diff --git a/gcc/Makefile.in b/gcc/Makefile.in index bf2186a24ee..333461b5ccb 100644 --- a/gcc/Makefile.in +++ b/gcc/Makefile.in @@ -1347,7 +1347,6 @@ OBJS = \ mcf.o \ mode-switching.o \ modulo-sched.o \ - omega.o \ omp-low.o \ optabs.o \ options-save.o \ diff --git a/gcc/common.opt b/gcc/common.opt index 6b2ccbc5239..8f25f8b35cf 100644 --- a/gcc/common.opt +++ b/gcc/common.opt @@ -987,7 +987,7 @@ Save registers around function calls fcheck-data-deps Common Report Var(flag_check_data_deps) -Compare the results of several data dependence analyzers. +This switch is deprecated; do not use. fcheck-new Common Var(flag_check_new) diff --git a/gcc/doc/invoke.texi b/gcc/doc/invoke.texi index 522e924f03b..a62c8b33e92 100644 --- a/gcc/doc/invoke.texi +++ b/gcc/doc/invoke.texi @@ -385,7 +385,7 @@ Objective-C and Objective-C++ Dialects}. -fauto-inc-dec -fbranch-probabilities @gol -fbranch-target-load-optimize -fbranch-target-load-optimize2 @gol -fbtr-bb-exclusive -fcaller-saves @gol --fcheck-data-deps -fcombine-stack-adjustments -fconserve-stack @gol +-fcombine-stack-adjustments -fconserve-stack @gol -fcompare-elim -fcprop-registers -fcrossjumping @gol -fcse-follow-jumps -fcse-skip-blocks -fcx-fortran-rules @gol -fcx-limited-range @gol @@ -8812,11 +8812,6 @@ be parallelized. Parallelize all the loops that can be analyzed to not contain loop carried dependences without checking that it is profitable to parallelize the loops. -@item -fcheck-data-deps -@opindex fcheck-data-deps -Compare the results of several data dependence analyzers. This option -is used for debugging the data dependence analyzers. - @item -ftree-loop-if-convert @opindex ftree-loop-if-convert Attempt to transform conditional jumps in the innermost loops to @@ -10475,34 +10470,6 @@ Large expressions slow the analyzer. Bound on the complexity of the expressions in the scalar evolutions analyzer. Complex expressions slow the analyzer. -@item omega-max-vars -The maximum number of variables in an Omega constraint system. -The default value is 128. - -@item omega-max-geqs -The maximum number of inequalities in an Omega constraint system. -The default value is 256. - -@item omega-max-eqs -The maximum number of equalities in an Omega constraint system. -The default value is 128. - -@item omega-max-wild-cards -The maximum number of wildcard variables that the Omega solver is -able to insert. The default value is 18. - -@item omega-hash-table-size -The size of the hash table in the Omega solver. The default value is -550. - -@item omega-max-keys -The maximal number of keys used by the Omega solver. The default -value is 500. - -@item omega-eliminate-redundant-constraints -When set to 1, use expensive methods to eliminate all redundant -constraints. The default value is 0. - @item vect-max-version-for-alignment-checks The maximum number of run-time checks that can be performed when doing loop versioning for alignment in the vectorizer. diff --git a/gcc/doc/loop.texi b/gcc/doc/loop.texi index 74f6f8dc8d6..18f8b651478 100644 --- a/gcc/doc/loop.texi +++ b/gcc/doc/loop.texi @@ -25,7 +25,6 @@ variable analysis and number of iterations analysis). * loop-iv:: Induction variables on RTL. * Number of iterations:: Number of iterations analysis. * Dependency analysis:: Data dependency analysis. -* Omega:: A solver for linear programming problems. @end menu @node Loop representation @@ -602,33 +601,3 @@ maximum verbosity the details of a data dependence relations array, direction vectors for a data dependence relations array, and @code{dump_data_references} prints the details of the data references contained in a data reference array. - - -@node Omega -@section Omega a solver for linear programming problems -@cindex Omega a solver for linear programming problems - -The data dependence analysis contains several solvers triggered -sequentially from the less complex ones to the more sophisticated. -For ensuring the consistency of the results of these solvers, a data -dependence check pass has been implemented based on two different -solvers. The second method that has been integrated to GCC is based -on the Omega dependence solver, written in the 1990's by William Pugh -and David Wonnacott. Data dependence tests can be formulated using a -subset of the Presburger arithmetics that can be translated to linear -constraint systems. These linear constraint systems can then be -solved using the Omega solver. - -The Omega solver is using Fourier-Motzkin's algorithm for variable -elimination: a linear constraint system containing @code{n} variables -is reduced to a linear constraint system with @code{n-1} variables. -The Omega solver can also be used for solving other problems that can -be expressed under the form of a system of linear equalities and -inequalities. The Omega solver is known to have an exponential worst -case, also known under the name of ``omega nightmare'' in the -literature, but in practice, the omega test is known to be efficient -for the common data dependence tests. - -The interface used by the Omega solver for describing the linear -programming problems is described in @file{omega.h}, and the solver is -@code{omega_solve_problem}. diff --git a/gcc/graphite-blocking.c b/gcc/graphite-blocking.c index 73d7c59748c..d9d16e8f15a 100644 --- a/gcc/graphite-blocking.c +++ b/gcc/graphite-blocking.c @@ -38,6 +38,7 @@ along with GCC; see the file COPYING3. If not see #include "cfghooks.h" #include "tree.h" #include "gimple.h" +#include "params.h" #include "fold-const.h" #include "gimple-iterator.h" #include "tree-ssa-loop.h" diff --git a/gcc/graphite-isl-ast-to-gimple.c b/gcc/graphite-isl-ast-to-gimple.c index b32781a5b78..b620a488050 100644 --- a/gcc/graphite-isl-ast-to-gimple.c +++ b/gcc/graphite-isl-ast-to-gimple.c @@ -44,6 +44,7 @@ extern "C" { #include "cfghooks.h" #include "tree.h" #include "gimple.h" +#include "params.h" #include "fold-const.h" #include "gimple-iterator.h" #include "tree-ssa-loop.h" diff --git a/gcc/graphite-optimize-isl.c b/gcc/graphite-optimize-isl.c index f4904017efd..87536b2a176 100644 --- a/gcc/graphite-optimize-isl.c +++ b/gcc/graphite-optimize-isl.c @@ -44,6 +44,7 @@ along with GCC; see the file COPYING3. If not see #include "cfgloop.h" #include "tree-data-ref.h" #include "graphite-poly.h" +#include "params.h" static isl_union_set * scop_get_domains (scop_p scop ATTRIBUTE_UNUSED) diff --git a/gcc/graphite-sese-to-poly.c b/gcc/graphite-sese-to-poly.c index 1e234fe232d..8960c3fca26 100644 --- a/gcc/graphite-sese-to-poly.c +++ b/gcc/graphite-sese-to-poly.c @@ -47,6 +47,7 @@ extern "C" { #include "tree.h" #include "gimple.h" #include "ssa.h" +#include "params.h" #include "fold-const.h" #include "gimple-iterator.h" #include "gimplify.h" diff --git a/gcc/graphite.c b/gcc/graphite.c index a81ef6aba68..6417da27215 100644 --- a/gcc/graphite.c +++ b/gcc/graphite.c @@ -50,6 +50,7 @@ along with GCC; see the file COPYING3. If not see #include "diagnostic-core.h" #include "cfgloop.h" #include "tree-pass.h" +#include "params.h" #ifdef HAVE_isl #include "cfghooks.h" diff --git a/gcc/omega.c b/gcc/omega.c deleted file mode 100644 index 55ed77d6b89..00000000000 --- a/gcc/omega.c +++ /dev/null @@ -1,5524 +0,0 @@ -/* 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 - -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 -. */ - -/* 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, "\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; -} diff --git a/gcc/omega.h b/gcc/omega.h deleted file mode 100644 index 33361b86363..00000000000 --- a/gcc/omega.h +++ /dev/null @@ -1,341 +0,0 @@ -/* 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 - -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 -. */ - - -#ifndef GCC_OMEGA_H -#define GCC_OMEGA_H - -#include "params.h" - -#define OMEGA_MAX_VARS PARAM_VALUE (PARAM_OMEGA_MAX_VARS) -#define OMEGA_MAX_GEQS PARAM_VALUE (PARAM_OMEGA_MAX_GEQS) -#define OMEGA_MAX_EQS PARAM_VALUE (PARAM_OMEGA_MAX_EQS) - -#define pos_infinity (0x7ffffff) -#define neg_infinity (-0x7ffffff) - -/* Results of the Omega solver. */ -enum omega_result { - omega_false = 0, - omega_true = 1, - - /* Value returned when the solver is unable to determine an - answer. */ - omega_unknown = 2, - - /* Value used for asking the solver to simplify the system. */ - omega_simplify = 3 -}; - -/* Values used for labeling equations. Private (not used outside the - solver). */ -enum omega_eqn_color { - omega_black = 0, - omega_red = 1 -}; - -/* Structure for equations. */ -typedef struct eqn_d -{ - int key; - int touched; - enum omega_eqn_color color; - - /* Array of coefficients for the equation. The layout of the data - is as follows: coef[0] is the constant, coef[i] for 1 <= i <= - OMEGA_MAX_VARS, are the coefficients for each dimension. Examples: - the equation 0 = 9 + x + 0y + 5z is encoded as [9 1 0 5], the - inequality 0 <= -8 + x + 2y + 3z is encoded as [-8 1 2 3]. */ - int *coef; -} *eqn; - -typedef struct omega_pb_d -{ - /* The number of variables in the system of equations. */ - int num_vars; - - /* Safe variables are not eliminated during the Fourier-Motzkin - simplification of the system. Safe variables are all those - variables that are placed at the beginning of the array of - variables: PB->var[1, ..., SAFE_VARS]. PB->var[0] is not used, - as PB->eqs[x]->coef[0] represents the constant of the equation. */ - int safe_vars; - - /* Number of elements in eqs[]. */ - int num_eqs; - /* Number of elements in geqs[]. */ - int num_geqs; - /* Number of elements in subs[]. */ - int num_subs; - - int hash_version; - bool variables_initialized; - bool variables_freed; - - /* Index or name of variables. Negative integers are reserved for - wildcard variables. Maps the index of variables in the original - problem to the new index of the variable. The index for a - variable in the coef array of an equation can change as some - variables are eliminated. */ - int *var; - - int *forwarding_address; - - /* Inequalities in the system of constraints. */ - eqn geqs; - - /* Equations in the system of constraints. */ - eqn eqs; - - /* A map of substituted variables. */ - eqn subs; -} *omega_pb; - -extern void omega_initialize (void); -extern omega_pb omega_alloc_problem (int, int); -extern enum omega_result omega_solve_problem (omega_pb, enum omega_result); -extern enum omega_result omega_simplify_problem (omega_pb); -extern enum omega_result omega_simplify_approximate (omega_pb); -extern enum omega_result omega_constrain_variable_sign (omega_pb, - enum omega_eqn_color, - int, int); -extern void debug (omega_pb_d &ref); -extern void debug (omega_pb_d *ptr); -extern void debug_omega_problem (omega_pb); -extern void omega_print_problem (FILE *, omega_pb); -extern void omega_print_red_equations (FILE *, omega_pb); -extern int omega_count_red_equations (omega_pb); -extern void omega_pretty_print_problem (FILE *, omega_pb); -extern void omega_unprotect_variable (omega_pb, int var); -extern void omega_negate_geq (omega_pb, int); -extern void omega_convert_eq_to_geqs (omega_pb, int eq); -extern void omega_print_eqn (FILE *, omega_pb, eqn, bool, int); -extern bool omega_problem_has_red_equations (omega_pb); -extern enum omega_result omega_eliminate_redundant (omega_pb, bool); -extern void omega_eliminate_red (omega_pb, bool); -extern void omega_constrain_variable_value (omega_pb, enum omega_eqn_color, - int, int); -extern bool omega_query_variable (omega_pb, int, int *, int *); -extern int omega_query_variable_signs (omega_pb, int, int, int, int, - int, int, bool *, int *); -extern bool omega_query_variable_bounds (omega_pb, int, int *, int *); -extern void (*omega_when_reduced) (omega_pb); -extern void omega_no_procedure (omega_pb); - -/* Return true when variable I in problem PB is a wildcard. */ - -static inline bool -omega_wildcard_p (omega_pb pb, int i) -{ - return (pb->var[i] < 0); -} - -/* Return true when variable I in problem PB is a safe variable. */ - -static inline bool -omega_safe_var_p (omega_pb pb, int i) -{ - /* The constant of an equation is not a variable. */ - gcc_assert (0 < i); - return (i <= pb->safe_vars); -} - -/* Print to FILE equality E from PB. */ - -static inline void -omega_print_eq (FILE *file, omega_pb pb, eqn e) -{ - omega_print_eqn (file, pb, e, false, 0); -} - -/* Print to FILE inequality E from PB. */ - -static inline void -omega_print_geq (FILE *file, omega_pb pb, eqn e) -{ - omega_print_eqn (file, pb, e, true, 0); -} - -/* Print to FILE inequality E from PB. */ - -static inline void -omega_print_geq_extra (FILE *file, omega_pb pb, eqn e) -{ - omega_print_eqn (file, pb, e, true, 1); -} - -/* E1 = E2, make a copy of E2 into E1. Equations contain S variables. */ - -static inline void -omega_copy_eqn (eqn e1, eqn e2, int s) -{ - e1->key = e2->key; - e1->touched = e2->touched; - e1->color = e2->color; - - memcpy (e1->coef, e2->coef, (s + 1) * sizeof (int)); -} - -/* Initialize E = 0. Equation E contains S variables. */ - -static inline void -omega_init_eqn_zero (eqn e, int s) -{ - e->key = 0; - e->touched = 0; - e->color = omega_black; - - memset (e->coef, 0, (s + 1) * sizeof (int)); -} - -/* Allocate N equations with S variables. */ - -static inline eqn -omega_alloc_eqns (int s, int n) -{ - int i; - eqn res = (eqn) (xcalloc (n, sizeof (struct eqn_d))); - - for (i = n - 1; i >= 0; i--) - { - res[i].coef = (int *) (xcalloc (OMEGA_MAX_VARS + 1, sizeof (int))); - omega_init_eqn_zero (&res[i], s); - } - - return res; -} - -/* Free N equations from array EQ. */ - -static inline void -omega_free_eqns (eqn eq, int n) -{ - int i; - - for (i = n - 1; i >= 0; i--) - free (eq[i].coef); - - free (eq); -} - -/* Returns true when E is an inequality with a single variable. */ - -static inline bool -single_var_geq (eqn e, int nv ATTRIBUTE_UNUSED) -{ - return (e->key != 0 - && -OMEGA_MAX_VARS <= e->key && e->key <= OMEGA_MAX_VARS); -} - -/* Allocate a new equality with all coefficients 0, and tagged with - COLOR. Return the index of this equality in problem PB. */ - -static inline int -omega_add_zero_eq (omega_pb pb, enum omega_eqn_color color) -{ - int idx = pb->num_eqs++; - - gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS); - omega_init_eqn_zero (&pb->eqs[idx], pb->num_vars); - pb->eqs[idx].color = color; - return idx; -} - -/* Allocate a new inequality with all coefficients 0, and tagged with - COLOR. Return the index of this inequality in problem PB. */ - -static inline int -omega_add_zero_geq (omega_pb pb, enum omega_eqn_color color) -{ - int idx = pb->num_geqs; - - pb->num_geqs++; - gcc_assert (pb->num_geqs <= OMEGA_MAX_GEQS); - omega_init_eqn_zero (&pb->geqs[idx], pb->num_vars); - pb->geqs[idx].touched = 1; - pb->geqs[idx].color = color; - return idx; -} - -/* Initialize variables for problem PB. */ - -static inline void -omega_initialize_variables (omega_pb pb) -{ - int i; - - for (i = pb->num_vars; i >= 0; i--) - pb->forwarding_address[i] = pb->var[i] = i; - - pb->variables_initialized = true; -} - -/* Free problem PB. */ - -static inline void -omega_free_problem (omega_pb pb) -{ - free (pb->var); - free (pb->forwarding_address); - omega_free_eqns (pb->geqs, OMEGA_MAX_GEQS); - omega_free_eqns (pb->eqs, OMEGA_MAX_EQS); - omega_free_eqns (pb->subs, OMEGA_MAX_VARS + 1); - free (pb); -} - -/* Copy omega problems: P1 = P2. */ - -static inline void -omega_copy_problem (omega_pb p1, omega_pb p2) -{ - int e, i; - - p1->num_vars = p2->num_vars; - p1->hash_version = p2->hash_version; - p1->variables_initialized = p2->variables_initialized; - p1->variables_freed = p2->variables_freed; - p1->safe_vars = p2->safe_vars; - p1->num_eqs = p2->num_eqs; - p1->num_subs = p2->num_subs; - p1->num_geqs = p2->num_geqs; - - for (e = p2->num_eqs - 1; e >= 0; e--) - omega_copy_eqn (&(p1->eqs[e]), &(p2->eqs[e]), p2->num_vars); - - for (e = p2->num_geqs - 1; e >= 0; e--) - omega_copy_eqn (&(p1->geqs[e]), &(p2->geqs[e]), p2->num_vars); - - for (e = p2->num_subs - 1; e >= 0; e--) - omega_copy_eqn (&(p1->subs[e]), &(p2->subs[e]), p2->num_vars); - - for (i = p2->num_vars; i >= 0; i--) - p1->var[i] = p2->var[i]; - - for (i = OMEGA_MAX_VARS; i >= 0; i--) - p1->forwarding_address[i] = p2->forwarding_address[i]; -} - -#endif /* GCC_OMEGA_H */ diff --git a/gcc/params.def b/gcc/params.def index 3e4ba3ad6ce..0ca345133dc 100644 --- a/gcc/params.def +++ b/gcc/params.def @@ -525,41 +525,6 @@ DEFPARAM(PARAM_SCEV_MAX_EXPR_COMPLEXITY, "Bound on the complexity of the expressions in the scalar evolutions analyzer", 10, 0, 0) -DEFPARAM(PARAM_OMEGA_MAX_VARS, - "omega-max-vars", - "Bound on the number of variables in Omega constraint systems", - 128, 0, 0) - -DEFPARAM(PARAM_OMEGA_MAX_GEQS, - "omega-max-geqs", - "Bound on the number of inequalities in Omega constraint systems", - 256, 0, 0) - -DEFPARAM(PARAM_OMEGA_MAX_EQS, - "omega-max-eqs", - "Bound on the number of equalities in Omega constraint systems", - 128, 0, 0) - -DEFPARAM(PARAM_OMEGA_MAX_WILD_CARDS, - "omega-max-wild-cards", - "Bound on the number of wild cards in Omega constraint systems", - 18, 0, 0) - -DEFPARAM(PARAM_OMEGA_HASH_TABLE_SIZE, - "omega-hash-table-size", - "Bound on the size of the hash table in Omega constraint systems", - 550, 0, 0) - -DEFPARAM(PARAM_OMEGA_MAX_KEYS, - "omega-max-keys", - "Bound on the number of keys in Omega constraint systems", - 500, 0, 0) - -DEFPARAM(PARAM_OMEGA_ELIMINATE_REDUNDANT_CONSTRAINTS, - "omega-eliminate-redundant-constraints", - "When set to 1, use expensive methods to eliminate all redundant constraints", - 0, 0, 1) - DEFPARAM(PARAM_VECT_MAX_VERSION_FOR_ALIGNMENT_CHECKS, "vect-max-version-for-alignment-checks", "Bound on number of runtime checks inserted by the vectorizer's loop versioning for alignment check", diff --git a/gcc/passes.def b/gcc/passes.def index 5cd07aed8f4..6b66f8f5396 100644 --- a/gcc/passes.def +++ b/gcc/passes.def @@ -233,7 +233,6 @@ along with GCC; see the file COPYING3. If not see NEXT_PASS (pass_tree_unswitch); NEXT_PASS (pass_scev_cprop); NEXT_PASS (pass_record_bounds); - NEXT_PASS (pass_check_data_deps); NEXT_PASS (pass_loop_distribution); NEXT_PASS (pass_copy_prop); NEXT_PASS (pass_graphite); diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog index 9628a20dc12..a9b34ba71f1 100644 --- a/gcc/testsuite/ChangeLog +++ b/gcc/testsuite/ChangeLog @@ -1,3 +1,10 @@ +2015-07-18 Sebastian Pop + + PR middle-end/46851 + PR middle-end/60340 + * gcc.dg/tree-ssa/pr42327.c: Removed. + * g++.dg/other/pr35011.C: Removed. + 2015-07-17 H.J. Lu PR target/66906 diff --git a/gcc/testsuite/g++.dg/other/pr35011.C b/gcc/testsuite/g++.dg/other/pr35011.C deleted file mode 100644 index ca75516d6e1..00000000000 --- a/gcc/testsuite/g++.dg/other/pr35011.C +++ /dev/null @@ -1,26 +0,0 @@ -// { dg-do compile } -// { dg-options "-O3 -fcheck-data-deps" } - -double foo(const double* p0, const double* p1, const double* q0) -{ - double d; - for (; p0 != p1; ++p0, ++q0) - d += *p0 * *q0; - return d; -} - -struct A -{ - double x[3]; - const double* begin() const { return x; } -}; - -struct B -{ - A a0, a1; - double d; - B(const A&); -}; - -B::B(const A& a) : a0(a), a1(a), d(foo(a0.begin(), a0.begin()+3, a1.begin())) -{} diff --git a/gcc/testsuite/gcc.dg/tree-ssa/pr42327.c b/gcc/testsuite/gcc.dg/tree-ssa/pr42327.c deleted file mode 100644 index c0d3811b249..00000000000 --- a/gcc/testsuite/gcc.dg/tree-ssa/pr42327.c +++ /dev/null @@ -1,7 +0,0 @@ -/* { dg-do compile } */ -/* { dg-options "-O1 -fcheck-data-deps" } */ - -void foo(char *str) -{ - while (*str != 0) *str++ = 0; -} diff --git a/gcc/tree-data-ref.c b/gcc/tree-data-ref.c index e6ff4efae34..d0b7aa21eac 100644 --- a/gcc/tree-data-ref.c +++ b/gcc/tree-data-ref.c @@ -249,7 +249,7 @@ debug (data_reference *ptr) /* Dumps the affine function described by FN to the file OUTF. */ -static void +DEBUG_FUNCTION void dump_affine_function (FILE *outf, affine_fn fn) { unsigned i; @@ -266,7 +266,7 @@ dump_affine_function (FILE *outf, affine_fn fn) /* Dumps the conflict function CF to the file OUTF. */ -static void +DEBUG_FUNCTION void dump_conflict_function (FILE *outf, conflict_function *cf) { unsigned i; @@ -290,7 +290,7 @@ dump_conflict_function (FILE *outf, conflict_function *cf) /* Dump function for a SUBSCRIPT structure. */ -static void +DEBUG_FUNCTION void dump_subscript (FILE *outf, struct subscript *subscript) { conflict_function *cf = SUB_CONFLICTS_IN_A (subscript); @@ -322,7 +322,7 @@ dump_subscript (FILE *outf, struct subscript *subscript) /* Print the classic direction vector DIRV to OUTF. */ -static void +DEBUG_FUNCTION void print_direction_vector (FILE *outf, lambda_vector dirv, int length) @@ -367,7 +367,7 @@ print_direction_vector (FILE *outf, /* Print a vector of direction vectors. */ -static void +DEBUG_FUNCTION void print_dir_vectors (FILE *outf, vec dir_vects, int length) { @@ -380,7 +380,7 @@ print_dir_vectors (FILE *outf, vec dir_vects, /* Print out a vector VEC of length N to OUTFILE. */ -static inline void +DEBUG_FUNCTION void print_lambda_vector (FILE * outfile, lambda_vector vector, int n) { int i; @@ -392,7 +392,7 @@ print_lambda_vector (FILE * outfile, lambda_vector vector, int n) /* Print a vector of distance vectors. */ -static void +DEBUG_FUNCTION void print_dist_vectors (FILE *outf, vec dist_vects, int length) { @@ -405,7 +405,7 @@ print_dist_vectors (FILE *outf, vec dist_vects, /* Dump function for a DATA_DEPENDENCE_RELATION structure. */ -static void +DEBUG_FUNCTION void dump_data_dependence_relation (FILE *outf, struct data_dependence_relation *ddr) { @@ -488,7 +488,7 @@ debug_data_dependence_relation (struct data_dependence_relation *ddr) /* Dump into FILE all the dependence relations from DDRS. */ -void +DEBUG_FUNCTION void dump_data_dependence_relations (FILE *file, vec ddrs) { @@ -528,7 +528,7 @@ debug_data_dependence_relations (vec ddrs) dependence vectors, or in other words the number of loops in the considered nest. */ -static void +DEBUG_FUNCTION void dump_dist_dir_vectors (FILE *file, vec ddrs) { unsigned int i, j; @@ -558,7 +558,7 @@ dump_dist_dir_vectors (FILE *file, vec ddrs) /* Dumps the data dependence relations DDRS in FILE. */ -static void +DEBUG_FUNCTION void dump_ddrs (FILE *file, vec ddrs) { unsigned int i; @@ -3682,531 +3682,6 @@ access_functions_are_affine_or_constant_p (const struct data_reference *a, return true; } -/* Initializes an equation for an OMEGA problem using the information - contained in the ACCESS_FUN. Returns true when the operation - succeeded. - - PB is the omega constraint system. - EQ is the number of the equation to be initialized. - OFFSET is used for shifting the variables names in the constraints: - a constrain is composed of 2 * the number of variables surrounding - dependence accesses. OFFSET is set either to 0 for the first n variables, - then it is set to n. - ACCESS_FUN is expected to be an affine chrec. */ - -static bool -init_omega_eq_with_af (omega_pb pb, unsigned eq, - unsigned int offset, tree access_fun, - struct data_dependence_relation *ddr) -{ - switch (TREE_CODE (access_fun)) - { - case POLYNOMIAL_CHREC: - { - tree left = CHREC_LEFT (access_fun); - tree right = CHREC_RIGHT (access_fun); - int var = CHREC_VARIABLE (access_fun); - unsigned var_idx; - - if (TREE_CODE (right) != INTEGER_CST) - return false; - - var_idx = index_in_loop_nest (var, DDR_LOOP_NEST (ddr)); - pb->eqs[eq].coef[offset + var_idx + 1] = int_cst_value (right); - - /* Compute the innermost loop index. */ - DDR_INNER_LOOP (ddr) = MAX (DDR_INNER_LOOP (ddr), var_idx); - - if (offset == 0) - pb->eqs[eq].coef[var_idx + DDR_NB_LOOPS (ddr) + 1] - += int_cst_value (right); - - switch (TREE_CODE (left)) - { - case POLYNOMIAL_CHREC: - return init_omega_eq_with_af (pb, eq, offset, left, ddr); - - case INTEGER_CST: - pb->eqs[eq].coef[0] += int_cst_value (left); - return true; - - default: - return false; - } - } - - case INTEGER_CST: - pb->eqs[eq].coef[0] += int_cst_value (access_fun); - return true; - - default: - return false; - } -} - -/* As explained in the comments preceding init_omega_for_ddr, we have - to set up a system for each loop level, setting outer loops - variation to zero, and current loop variation to positive or zero. - Save each lexico positive distance vector. */ - -static void -omega_extract_distance_vectors (omega_pb pb, - struct data_dependence_relation *ddr) -{ - int eq, geq; - unsigned i, j; - struct loop *loopi, *loopj; - enum omega_result res; - - /* Set a new problem for each loop in the nest. The basis is the - problem that we have initialized until now. On top of this we - add new constraints. */ - for (i = 0; i <= DDR_INNER_LOOP (ddr) - && DDR_LOOP_NEST (ddr).iterate (i, &loopi); i++) - { - int dist = 0; - omega_pb copy = omega_alloc_problem (2 * DDR_NB_LOOPS (ddr), - DDR_NB_LOOPS (ddr)); - - omega_copy_problem (copy, pb); - - /* For all the outer loops "loop_j", add "dj = 0". */ - for (j = 0; j < i && DDR_LOOP_NEST (ddr).iterate (j, &loopj); j++) - { - eq = omega_add_zero_eq (copy, omega_black); - copy->eqs[eq].coef[j + 1] = 1; - } - - /* For "loop_i", add "0 <= di". */ - geq = omega_add_zero_geq (copy, omega_black); - copy->geqs[geq].coef[i + 1] = 1; - - /* Reduce the constraint system, and test that the current - problem is feasible. */ - res = omega_simplify_problem (copy); - if (res == omega_false - || res == omega_unknown - || copy->num_geqs > (int) DDR_NB_LOOPS (ddr)) - goto next_problem; - - for (eq = 0; eq < copy->num_subs; eq++) - if (copy->subs[eq].key == (int) i + 1) - { - dist = copy->subs[eq].coef[0]; - goto found_dist; - } - - if (dist == 0) - { - /* Reinitialize problem... */ - omega_copy_problem (copy, pb); - for (j = 0; j < i && DDR_LOOP_NEST (ddr).iterate (j, &loopj); j++) - { - eq = omega_add_zero_eq (copy, omega_black); - copy->eqs[eq].coef[j + 1] = 1; - } - - /* ..., but this time "di = 1". */ - eq = omega_add_zero_eq (copy, omega_black); - copy->eqs[eq].coef[i + 1] = 1; - copy->eqs[eq].coef[0] = -1; - - res = omega_simplify_problem (copy); - if (res == omega_false - || res == omega_unknown - || copy->num_geqs > (int) DDR_NB_LOOPS (ddr)) - goto next_problem; - - for (eq = 0; eq < copy->num_subs; eq++) - if (copy->subs[eq].key == (int) i + 1) - { - dist = copy->subs[eq].coef[0]; - goto found_dist; - } - } - - found_dist:; - /* Save the lexicographically positive distance vector. */ - if (dist >= 0) - { - lambda_vector dist_v = lambda_vector_new (DDR_NB_LOOPS (ddr)); - lambda_vector dir_v = lambda_vector_new (DDR_NB_LOOPS (ddr)); - - dist_v[i] = dist; - - for (eq = 0; eq < copy->num_subs; eq++) - if (copy->subs[eq].key > 0) - { - dist = copy->subs[eq].coef[0]; - dist_v[copy->subs[eq].key - 1] = dist; - } - - for (j = 0; j < DDR_NB_LOOPS (ddr); j++) - dir_v[j] = dir_from_dist (dist_v[j]); - - save_dist_v (ddr, dist_v); - save_dir_v (ddr, dir_v); - } - - next_problem:; - omega_free_problem (copy); - } -} - -/* This is called for each subscript of a tuple of data references: - insert an equality for representing the conflicts. */ - -static bool -omega_setup_subscript (tree access_fun_a, tree access_fun_b, - struct data_dependence_relation *ddr, - omega_pb pb, bool *maybe_dependent) -{ - int eq; - tree type = signed_type_for_types (TREE_TYPE (access_fun_a), - TREE_TYPE (access_fun_b)); - tree fun_a = chrec_convert (type, access_fun_a, NULL); - tree fun_b = chrec_convert (type, access_fun_b, NULL); - tree difference = chrec_fold_minus (type, fun_a, fun_b); - tree minus_one; - - /* When the fun_a - fun_b is not constant, the dependence is not - captured by the classic distance vector representation. */ - if (TREE_CODE (difference) != INTEGER_CST) - return false; - - /* ZIV test. */ - if (ziv_subscript_p (fun_a, fun_b) && !integer_zerop (difference)) - { - /* There is no dependence. */ - *maybe_dependent = false; - return true; - } - - minus_one = build_int_cst (type, -1); - fun_b = chrec_fold_multiply (type, fun_b, minus_one); - - eq = omega_add_zero_eq (pb, omega_black); - if (!init_omega_eq_with_af (pb, eq, DDR_NB_LOOPS (ddr), fun_a, ddr) - || !init_omega_eq_with_af (pb, eq, 0, fun_b, ddr)) - /* There is probably a dependence, but the system of - constraints cannot be built: answer "don't know". */ - return false; - - /* GCD test. */ - if (DDR_NB_LOOPS (ddr) != 0 && pb->eqs[eq].coef[0] - && !int_divides_p (lambda_vector_gcd - ((lambda_vector) &(pb->eqs[eq].coef[1]), - 2 * DDR_NB_LOOPS (ddr)), - pb->eqs[eq].coef[0])) - { - /* There is no dependence. */ - *maybe_dependent = false; - return true; - } - - return true; -} - -/* Helper function, same as init_omega_for_ddr but specialized for - data references A and B. */ - -static bool -init_omega_for_ddr_1 (struct data_reference *dra, struct data_reference *drb, - struct data_dependence_relation *ddr, - omega_pb pb, bool *maybe_dependent) -{ - unsigned i; - int ineq; - struct loop *loopi; - unsigned nb_loops = DDR_NB_LOOPS (ddr); - - /* Insert an equality per subscript. */ - for (i = 0; i < DDR_NUM_SUBSCRIPTS (ddr); i++) - { - if (!omega_setup_subscript (DR_ACCESS_FN (dra, i), DR_ACCESS_FN (drb, i), - ddr, pb, maybe_dependent)) - return false; - else if (*maybe_dependent == false) - { - /* There is no dependence. */ - DDR_ARE_DEPENDENT (ddr) = chrec_known; - return true; - } - } - - /* Insert inequalities: constraints corresponding to the iteration - domain, i.e. the loops surrounding the references "loop_x" and - the distance variables "dx". The layout of the OMEGA - representation is as follows: - - coef[0] is the constant - - coef[1..nb_loops] are the protected variables that will not be - removed by the solver: the "dx" - - coef[nb_loops + 1, 2*nb_loops] are the loop variables: "loop_x". - */ - for (i = 0; i <= DDR_INNER_LOOP (ddr) - && DDR_LOOP_NEST (ddr).iterate (i, &loopi); i++) - { - HOST_WIDE_INT nbi = max_stmt_executions_int (loopi); - - /* 0 <= loop_x */ - ineq = omega_add_zero_geq (pb, omega_black); - pb->geqs[ineq].coef[i + nb_loops + 1] = 1; - - /* 0 <= loop_x + dx */ - ineq = omega_add_zero_geq (pb, omega_black); - pb->geqs[ineq].coef[i + nb_loops + 1] = 1; - pb->geqs[ineq].coef[i + 1] = 1; - - if (nbi != -1) - { - /* loop_x <= nb_iters */ - ineq = omega_add_zero_geq (pb, omega_black); - pb->geqs[ineq].coef[i + nb_loops + 1] = -1; - pb->geqs[ineq].coef[0] = nbi; - - /* loop_x + dx <= nb_iters */ - ineq = omega_add_zero_geq (pb, omega_black); - pb->geqs[ineq].coef[i + nb_loops + 1] = -1; - pb->geqs[ineq].coef[i + 1] = -1; - pb->geqs[ineq].coef[0] = nbi; - - /* A step "dx" bigger than nb_iters is not feasible, so - add "0 <= nb_iters + dx", */ - ineq = omega_add_zero_geq (pb, omega_black); - pb->geqs[ineq].coef[i + 1] = 1; - pb->geqs[ineq].coef[0] = nbi; - /* and "dx <= nb_iters". */ - ineq = omega_add_zero_geq (pb, omega_black); - pb->geqs[ineq].coef[i + 1] = -1; - pb->geqs[ineq].coef[0] = nbi; - } - } - - omega_extract_distance_vectors (pb, ddr); - - return true; -} - -/* Sets up the Omega dependence problem for the data dependence - relation DDR. Returns false when the constraint system cannot be - built, ie. when the test answers "don't know". Returns true - otherwise, and when independence has been proved (using one of the - trivial dependence test), set MAYBE_DEPENDENT to false, otherwise - set MAYBE_DEPENDENT to true. - - Example: for setting up the dependence system corresponding to the - conflicting accesses - - | loop_i - | loop_j - | A[i, i+1] = ... - | ... A[2*j, 2*(i + j)] - | endloop_j - | endloop_i - - the following constraints come from the iteration domain: - - 0 <= i <= Ni - 0 <= i + di <= Ni - 0 <= j <= Nj - 0 <= j + dj <= Nj - - where di, dj are the distance variables. The constraints - representing the conflicting elements are: - - i = 2 * (j + dj) - i + 1 = 2 * (i + di + j + dj) - - For asking that the resulting distance vector (di, dj) be - lexicographically positive, we insert the constraint "di >= 0". If - "di = 0" in the solution, we fix that component to zero, and we - look at the inner loops: we set a new problem where all the outer - loop distances are zero, and fix this inner component to be - positive. When one of the components is positive, we save that - distance, and set a new problem where the distance on this loop is - zero, searching for other distances in the inner loops. Here is - the classic example that illustrates that we have to set for each - inner loop a new problem: - - | loop_1 - | loop_2 - | A[10] - | endloop_2 - | endloop_1 - - we have to save two distances (1, 0) and (0, 1). - - Given two array references, refA and refB, we have to set the - dependence problem twice, refA vs. refB and refB vs. refA, and we - cannot do a single test, as refB might occur before refA in the - inner loops, and the contrary when considering outer loops: ex. - - | loop_0 - | loop_1 - | loop_2 - | T[{1,+,1}_2][{1,+,1}_1] // refA - | T[{2,+,1}_2][{0,+,1}_1] // refB - | endloop_2 - | endloop_1 - | endloop_0 - - refB touches the elements in T before refA, and thus for the same - loop_0 refB precedes refA: ie. the distance vector (0, 1, -1) - but for successive loop_0 iterations, we have (1, -1, 1) - - The Omega solver expects the distance variables ("di" in the - previous example) to come first in the constraint system (as - variables to be protected, or "safe" variables), the constraint - system is built using the following layout: - - "cst | distance vars | index vars". -*/ - -static bool -init_omega_for_ddr (struct data_dependence_relation *ddr, - bool *maybe_dependent) -{ - omega_pb pb; - bool res = false; - - *maybe_dependent = true; - - if (same_access_functions (ddr)) - { - unsigned j; - lambda_vector dir_v; - - /* Save the 0 vector. */ - save_dist_v (ddr, lambda_vector_new (DDR_NB_LOOPS (ddr))); - dir_v = lambda_vector_new (DDR_NB_LOOPS (ddr)); - for (j = 0; j < DDR_NB_LOOPS (ddr); j++) - dir_v[j] = dir_equal; - save_dir_v (ddr, dir_v); - - /* Save the dependences carried by outer loops. */ - pb = omega_alloc_problem (2 * DDR_NB_LOOPS (ddr), DDR_NB_LOOPS (ddr)); - res = init_omega_for_ddr_1 (DDR_A (ddr), DDR_B (ddr), ddr, pb, - maybe_dependent); - omega_free_problem (pb); - return res; - } - - /* Omega expects the protected variables (those that have to be kept - after elimination) to appear first in the constraint system. - These variables are the distance variables. In the following - initialization we declare NB_LOOPS safe variables, and the total - number of variables for the constraint system is 2*NB_LOOPS. */ - pb = omega_alloc_problem (2 * DDR_NB_LOOPS (ddr), DDR_NB_LOOPS (ddr)); - res = init_omega_for_ddr_1 (DDR_A (ddr), DDR_B (ddr), ddr, pb, - maybe_dependent); - omega_free_problem (pb); - - /* Stop computation if not decidable, or no dependence. */ - if (res == false || *maybe_dependent == false) - return res; - - pb = omega_alloc_problem (2 * DDR_NB_LOOPS (ddr), DDR_NB_LOOPS (ddr)); - res = init_omega_for_ddr_1 (DDR_B (ddr), DDR_A (ddr), ddr, pb, - maybe_dependent); - omega_free_problem (pb); - - return res; -} - -/* Return true when DDR contains the same information as that stored - in DIR_VECTS and in DIST_VECTS, return false otherwise. */ - -static bool -ddr_consistent_p (FILE *file, - struct data_dependence_relation *ddr, - vec dist_vects, - vec dir_vects) -{ - unsigned int i, j; - - /* If dump_file is set, output there. */ - if (dump_file && (dump_flags & TDF_DETAILS)) - file = dump_file; - - if (dist_vects.length () != DDR_NUM_DIST_VECTS (ddr)) - { - lambda_vector b_dist_v; - fprintf (file, "\n(Number of distance vectors differ: Banerjee has %d, Omega has %d.\n", - dist_vects.length (), - DDR_NUM_DIST_VECTS (ddr)); - - fprintf (file, "Banerjee dist vectors:\n"); - FOR_EACH_VEC_ELT (dist_vects, i, b_dist_v) - print_lambda_vector (file, b_dist_v, DDR_NB_LOOPS (ddr)); - - fprintf (file, "Omega dist vectors:\n"); - for (i = 0; i < DDR_NUM_DIST_VECTS (ddr); i++) - print_lambda_vector (file, DDR_DIST_VECT (ddr, i), DDR_NB_LOOPS (ddr)); - - fprintf (file, "data dependence relation:\n"); - dump_data_dependence_relation (file, ddr); - - fprintf (file, ")\n"); - return false; - } - - if (dir_vects.length () != DDR_NUM_DIR_VECTS (ddr)) - { - fprintf (file, "\n(Number of direction vectors differ: Banerjee has %d, Omega has %d.)\n", - dir_vects.length (), - DDR_NUM_DIR_VECTS (ddr)); - return false; - } - - for (i = 0; i < DDR_NUM_DIST_VECTS (ddr); i++) - { - lambda_vector a_dist_v; - lambda_vector b_dist_v = DDR_DIST_VECT (ddr, i); - - /* Distance vectors are not ordered in the same way in the DDR - and in the DIST_VECTS: search for a matching vector. */ - FOR_EACH_VEC_ELT (dist_vects, j, a_dist_v) - if (lambda_vector_equal (a_dist_v, b_dist_v, DDR_NB_LOOPS (ddr))) - break; - - if (j == dist_vects.length ()) - { - fprintf (file, "\n(Dist vectors from the first dependence analyzer:\n"); - print_dist_vectors (file, dist_vects, DDR_NB_LOOPS (ddr)); - fprintf (file, "not found in Omega dist vectors:\n"); - print_dist_vectors (file, DDR_DIST_VECTS (ddr), DDR_NB_LOOPS (ddr)); - fprintf (file, "data dependence relation:\n"); - dump_data_dependence_relation (file, ddr); - fprintf (file, ")\n"); - } - } - - for (i = 0; i < DDR_NUM_DIR_VECTS (ddr); i++) - { - lambda_vector a_dir_v; - lambda_vector b_dir_v = DDR_DIR_VECT (ddr, i); - - /* Direction vectors are not ordered in the same way in the DDR - and in the DIR_VECTS: search for a matching vector. */ - FOR_EACH_VEC_ELT (dir_vects, j, a_dir_v) - if (lambda_vector_equal (a_dir_v, b_dir_v, DDR_NB_LOOPS (ddr))) - break; - - if (j == dist_vects.length ()) - { - fprintf (file, "\n(Dir vectors from the first dependence analyzer:\n"); - print_dir_vectors (file, dir_vects, DDR_NB_LOOPS (ddr)); - fprintf (file, "not found in Omega dir vectors:\n"); - print_dir_vectors (file, DDR_DIR_VECTS (ddr), DDR_NB_LOOPS (ddr)); - fprintf (file, "data dependence relation:\n"); - dump_data_dependence_relation (file, ddr); - fprintf (file, ")\n"); - } - } - - return true; -} - /* This computes the affine dependence relation between A and B with respect to LOOP_NEST. CHREC_KNOWN is used for representing the independence between two accesses, while CHREC_DONT_KNOW is used @@ -4239,55 +3714,13 @@ compute_affine_dependence (struct data_dependence_relation *ddr, if (access_functions_are_affine_or_constant_p (dra, loop_nest) && access_functions_are_affine_or_constant_p (drb, loop_nest)) - { - subscript_dependence_tester (ddr, loop_nest); - - if (flag_check_data_deps) - { - /* Dump the dependences from the first algorithm. */ - if (dump_file && (dump_flags & TDF_DETAILS)) - { - fprintf (dump_file, "\n\nBanerjee Analyzer\n"); - dump_data_dependence_relation (dump_file, ddr); - } - - if (DDR_ARE_DEPENDENT (ddr) == NULL_TREE) - { - bool maybe_dependent; - vec dir_vects, dist_vects; - - /* Save the result of the first DD analyzer. */ - dist_vects = DDR_DIST_VECTS (ddr); - dir_vects = DDR_DIR_VECTS (ddr); - - /* Reset the information. */ - DDR_DIST_VECTS (ddr).create (0); - DDR_DIR_VECTS (ddr).create (0); - - /* Compute the same information using Omega. */ - if (!init_omega_for_ddr (ddr, &maybe_dependent)) - goto csys_dont_know; - - if (dump_file && (dump_flags & TDF_DETAILS)) - { - fprintf (dump_file, "Omega Analyzer\n"); - dump_data_dependence_relation (dump_file, ddr); - } - - /* Check that we get the same information. */ - if (maybe_dependent) - gcc_assert (ddr_consistent_p (stderr, ddr, dist_vects, - dir_vects)); - } - } - } + subscript_dependence_tester (ddr, loop_nest); /* As a last case, if the dependence cannot be determined, or if the dependence is considered too difficult to determine, answer "don't know". */ else { - csys_dont_know:; dependence_stats.num_dependence_undetermined++; if (dump_file && (dump_flags & TDF_DETAILS)) @@ -4731,110 +4164,6 @@ compute_data_dependences_for_loop (struct loop *loop, return res; } -/* Returns true when the data dependences for the basic block BB have been - computed, false otherwise. - DATAREFS is initialized to all the array elements contained in this basic - block, DEPENDENCE_RELATIONS contains the relations between the data - references. Compute read-read and self relations if - COMPUTE_SELF_AND_READ_READ_DEPENDENCES is TRUE. */ -bool -compute_data_dependences_for_bb (basic_block bb, - bool compute_self_and_read_read_dependences, - vec *datarefs, - vec *dependence_relations) -{ - if (find_data_references_in_bb (NULL, bb, datarefs) == chrec_dont_know) - return false; - - return compute_all_dependences (*datarefs, dependence_relations, vNULL, - compute_self_and_read_read_dependences); -} - -/* Entry point (for testing only). Analyze all the data references - and the dependence relations in LOOP. - - The data references are computed first. - - A relation on these nodes is represented by a complete graph. Some - of the relations could be of no interest, thus the relations can be - computed on demand. - - In the following function we compute all the relations. This is - just a first implementation that is here for: - - for showing how to ask for the dependence relations, - - for the debugging the whole dependence graph, - - for the dejagnu testcases and maintenance. - - It is possible to ask only for a part of the graph, avoiding to - compute the whole dependence graph. The computed dependences are - stored in a knowledge base (KB) such that later queries don't - recompute the same information. The implementation of this KB is - transparent to the optimizer, and thus the KB can be changed with a - more efficient implementation, or the KB could be disabled. */ -static void -analyze_all_data_dependences (struct loop *loop) -{ - unsigned int i; - int nb_data_refs = 10; - vec datarefs; - datarefs.create (nb_data_refs); - vec dependence_relations; - dependence_relations.create (nb_data_refs * nb_data_refs); - vec loop_nest; - loop_nest.create (3); - - /* Compute DDs on the whole function. */ - compute_data_dependences_for_loop (loop, false, &loop_nest, &datarefs, - &dependence_relations); - - if (dump_file) - { - dump_data_dependence_relations (dump_file, dependence_relations); - fprintf (dump_file, "\n\n"); - - if (dump_flags & TDF_DETAILS) - dump_dist_dir_vectors (dump_file, dependence_relations); - - if (dump_flags & TDF_STATS) - { - unsigned nb_top_relations = 0; - unsigned nb_bot_relations = 0; - unsigned nb_chrec_relations = 0; - struct data_dependence_relation *ddr; - - FOR_EACH_VEC_ELT (dependence_relations, i, ddr) - { - if (chrec_contains_undetermined (DDR_ARE_DEPENDENT (ddr))) - nb_top_relations++; - - else if (DDR_ARE_DEPENDENT (ddr) == chrec_known) - nb_bot_relations++; - - else - nb_chrec_relations++; - } - - gather_stats_on_scev_database (); - } - } - - loop_nest.release (); - free_dependence_relations (dependence_relations); - free_data_refs (datarefs); -} - -/* Computes all the data dependences and check that the results of - several analyzers are the same. */ - -void -tree_check_data_deps (void) -{ - struct loop *loop_nest; - - FOR_EACH_LOOP (loop_nest, 0) - analyze_all_data_dependences (loop_nest); -} - /* Free the memory used by a data dependence relation DDR. */ void diff --git a/gcc/tree-data-ref.h b/gcc/tree-data-ref.h index 9d8e6992f80..18bcc5c89bb 100644 --- a/gcc/tree-data-ref.h +++ b/gcc/tree-data-ref.h @@ -22,7 +22,6 @@ along with GCC; see the file COPYING3. If not see #define GCC_TREE_DATA_REF_H #include "graphds.h" -#include "omega.h" #include "tree-chrec.h" /* @@ -301,9 +300,6 @@ extern bool compute_data_dependences_for_loop (struct loop *, bool, vec *, vec *, vec *); -extern bool compute_data_dependences_for_bb (basic_block, bool, - vec *, - vec *); extern void debug_ddrs (vec ); extern void dump_data_reference (FILE *, struct data_reference *); extern void debug (data_reference &ref); @@ -343,8 +339,6 @@ extern bool dr_may_alias_p (const struct data_reference *, const struct data_reference *, bool); extern bool dr_equal_offsets_p (struct data_reference *, struct data_reference *); -extern void tree_check_data_deps (void); - /* Return true when the base objects of data references A and B are the same memory object. */ diff --git a/gcc/tree-ssa-loop.c b/gcc/tree-ssa-loop.c index 609aff9793b..078b1d128c7 100644 --- a/gcc/tree-ssa-loop.c +++ b/gcc/tree-ssa-loop.c @@ -286,54 +286,6 @@ make_pass_vectorize (gcc::context *ctxt) return new pass_vectorize (ctxt); } -/* Check the correctness of the data dependence analyzers. */ - -namespace { - -const pass_data pass_data_check_data_deps = -{ - GIMPLE_PASS, /* type */ - "ckdd", /* name */ - OPTGROUP_LOOP, /* optinfo_flags */ - TV_CHECK_DATA_DEPS, /* tv_id */ - ( PROP_cfg | PROP_ssa ), /* properties_required */ - 0, /* properties_provided */ - 0, /* properties_destroyed */ - 0, /* todo_flags_start */ - 0, /* todo_flags_finish */ -}; - -class pass_check_data_deps : public gimple_opt_pass -{ -public: - pass_check_data_deps (gcc::context *ctxt) - : gimple_opt_pass (pass_data_check_data_deps, ctxt) - {} - - /* opt_pass methods: */ - virtual bool gate (function *) { return flag_check_data_deps != 0; } - virtual unsigned int execute (function *); - -}; // class pass_check_data_deps - -unsigned int -pass_check_data_deps::execute (function *fun) -{ - if (number_of_loops (fun) <= 1) - return 0; - - tree_check_data_deps (); - return 0; -} - -} // anon namespace - -gimple_opt_pass * -make_pass_check_data_deps (gcc::context *ctxt) -{ - return new pass_check_data_deps (ctxt); -} - /* Propagation of constants using scev. */ namespace { diff --git a/gcc/tree-ssa-phiopt.c b/gcc/tree-ssa-phiopt.c index cab20bcd0c8..633ccc7edf2 100644 --- a/gcc/tree-ssa-phiopt.c +++ b/gcc/tree-ssa-phiopt.c @@ -57,6 +57,7 @@ along with GCC; see the file COPYING3. If not see #include "optabs.h" #include "tree-scalar-evolution.h" #include "tree-inline.h" +#include "params.h" static unsigned int tree_ssa_phiopt_worker (bool, bool); static bool conditional_replacement (basic_block, basic_block, diff --git a/gcc/tree-vect-data-refs.c b/gcc/tree-vect-data-refs.c index c98cee4d94a..731fe7decc5 100644 --- a/gcc/tree-vect-data-refs.c +++ b/gcc/tree-vect-data-refs.c @@ -63,6 +63,7 @@ along with GCC; see the file COPYING3. If not see #include "insn-codes.h" #include "optabs.h" #include "builtins.h" +#include "params.h" /* Return true if load- or store-lanes optab OPTAB is implemented for COUNT vectors of type VECTYPE. NAME is the name of OPTAB. */ diff --git a/gcc/tree-vect-slp.c b/gcc/tree-vect-slp.c index a2402276072..2face16501f 100644 --- a/gcc/tree-vect-slp.c +++ b/gcc/tree-vect-slp.c @@ -26,6 +26,7 @@ along with GCC; see the file COPYING3. If not see #include "backend.h" #include "tree.h" #include "gimple.h" +#include "params.h" #include "rtl.h" #include "ssa.h" #include "alias.h"