00001 /* Constraint class implementation (non-inline functions). 00002 Copyright (C) 2001-2006 Roberto Bagnara <bagnara@cs.unipr.it> 00003 00004 This file is part of the Parma Polyhedra Library (PPL). 00005 00006 The PPL is free software; you can redistribute it and/or modify it 00007 under the terms of the GNU General Public License as published by the 00008 Free Software Foundation; either version 2 of the License, or (at your 00009 option) any later version. 00010 00011 The PPL is distributed in the hope that it will be useful, but WITHOUT 00012 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or 00013 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License 00014 for more details. 00015 00016 You should have received a copy of the GNU General Public License 00017 along with this program; if not, write to the Free Software Foundation, 00018 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. 00019 00020 For the most up-to-date information see the Parma Polyhedra Library 00021 site: http://www.cs.unipr.it/ppl/ . */ 00022 00023 #include <config.h> 00024 00025 #include "Constraint.defs.hh" 00026 00027 #include "Variable.defs.hh" 00028 #include <iostream> 00029 #include <sstream> 00030 #include <stdexcept> 00031 00032 namespace PPL = Parma_Polyhedra_Library; 00033 00034 void 00035 PPL::Constraint::throw_dimension_incompatible(const char* method, 00036 const char* name_var, 00037 const Variable v) const { 00038 std::ostringstream s; 00039 s << "PPL::Constraint::" << method << ":" << std::endl 00040 << "this->space_dimension() == " << space_dimension() << ", " 00041 << name_var << ".space_dimension() == " << v.space_dimension() << "."; 00042 throw std::invalid_argument(s.str()); 00043 } 00044 00045 PPL::Constraint 00046 PPL::Constraint::construct_epsilon_geq_zero() { 00047 Linear_Expression e = Variable(0); 00048 Constraint c(e, NONSTRICT_INEQUALITY, NOT_NECESSARILY_CLOSED); 00049 return c; 00050 } 00051 00052 bool 00053 PPL::Constraint::is_tautological() const { 00054 assert(size() > 0); 00055 const Constraint& x = *this; 00056 if (x.all_homogeneous_terms_are_zero()) 00057 if (is_equality()) 00058 return x[0] == 0; 00059 else 00060 // Non-strict inequality constraint. 00061 return x[0] >= 0; 00062 else 00063 // There is a non-zero homogeneous coefficient. 00064 if (is_necessarily_closed()) 00065 return false; 00066 else { 00067 // The constraint is NOT necessarily closed. 00068 const dimension_type eps_index = size() - 1; 00069 const int eps_sign = sgn(x[eps_index]); 00070 if (eps_sign > 0) 00071 // We have found the constraint epsilon >= 0. 00072 return true; 00073 if (eps_sign == 0) 00074 // One of the `true' dimensions has a non-zero coefficient. 00075 return false; 00076 else { 00077 // Here the epsilon coefficient is negative: strict inequality. 00078 if (x[0] <= 0) 00079 // A strict inequality such as `lhs - k > 0', 00080 // where k is a non negative integer, cannot be trivially true. 00081 return false; 00082 // Checking for another non-zero coefficient. 00083 for (dimension_type i = eps_index; --i > 0; ) 00084 if (x[i] != 0) 00085 return false; 00086 // We have the inequality `k > 0', 00087 // where k is a positive integer. 00088 return true; 00089 } 00090 } 00091 } 00092 00093 bool 00094 PPL::Constraint::is_inconsistent() const { 00095 assert(size() > 0); 00096 const Constraint& x = *this; 00097 if (x.all_homogeneous_terms_are_zero()) 00098 // The inhomogeneous term is the only non-zero coefficient. 00099 if (is_equality()) 00100 return x[0] != 0; 00101 else 00102 // Non-strict inequality constraint. 00103 return x[0] < 0; 00104 else 00105 // There is a non-zero homogeneous coefficient. 00106 if (is_necessarily_closed()) 00107 return false; 00108 else { 00109 // The constraint is NOT necessarily closed. 00110 const dimension_type eps_index = size() - 1; 00111 if (x[eps_index] >= 0) 00112 // If positive, we have found the constraint epsilon >= 0. 00113 // If zero, one of the `true' dimensions has a non-zero coefficient. 00114 // In both cases, it is not trivially false. 00115 return false; 00116 else { 00117 // Here the epsilon coefficient is negative: strict inequality. 00118 if (x[0] > 0) 00119 // A strict inequality such as `lhs + k > 0', 00120 // where k is a positive integer, cannot be trivially false. 00121 return false; 00122 // Checking for another non-zero coefficient. 00123 for (dimension_type i = eps_index; --i > 0; ) 00124 if (x[i] != 0) 00125 return false; 00126 // We have the inequality `k > 0', 00127 // where k is zero or a negative integer. 00128 return true; 00129 } 00130 } 00131 } 00132 00133 bool 00134 PPL::Constraint::is_equivalent_to(const Constraint& y) const { 00135 const Constraint& x = *this; 00136 const dimension_type x_space_dim = x.space_dimension(); 00137 if (x_space_dim != y.space_dimension()) 00138 return false; 00139 00140 const Type x_type = x.type(); 00141 if (x_type != y.type()) { 00142 // Check for special cases. 00143 if (x.is_tautological()) 00144 return y.is_tautological(); 00145 else 00146 return x.is_inconsistent() && y.is_inconsistent(); 00147 } 00148 00149 if (x_type == STRICT_INEQUALITY) { 00150 // Due to the presence of epsilon-coefficients, syntactically 00151 // different strict inequalities may actually encode the same 00152 // topologically open half-space. 00153 // First, drop the epsilon-coefficient ... 00154 Linear_Expression x_expr(x); 00155 Linear_Expression y_expr(y); 00156 // ... then, re-normalize ... 00157 x_expr.normalize(); 00158 y_expr.normalize(); 00159 // ... and finally check for syntactic equality. 00160 for (dimension_type i = x_space_dim + 1; i-- > 0; ) 00161 if (x_expr[i] != y_expr[i]) 00162 return false; 00163 return true; 00164 } 00165 00166 // `x' and 'y' are of the same type and they are not strict inequalities; 00167 // thus, the epsilon-coefficient, if present, is zero. 00168 // It is sufficient to check for syntactic equality. 00169 for (dimension_type i = x_space_dim + 1; i-- > 0; ) 00170 if (x[i] != y[i]) 00171 return false; 00172 return true; 00173 } 00174 00176 std::ostream& 00177 PPL::IO_Operators::operator<<(std::ostream& s, const Constraint& c) { 00178 const int num_variables = c.space_dimension(); 00179 bool first = true; 00180 for (int v = 0; v < num_variables; ++v) { 00181 Coefficient cv = c.coefficient(Variable(v)); 00182 if (cv != 0) { 00183 if (!first) { 00184 if (cv > 0) 00185 s << " + "; 00186 else { 00187 s << " - "; 00188 neg_assign(cv); 00189 } 00190 } 00191 else 00192 first = false; 00193 if (cv == -1) 00194 s << "-"; 00195 else if (cv != 1) 00196 s << cv << "*"; 00197 s << PPL::Variable(v); 00198 } 00199 } 00200 if (first) 00201 s << Coefficient_zero(); 00202 const char* relation_symbol = 0; 00203 switch (c.type()) { 00204 case Constraint::EQUALITY: 00205 relation_symbol = " = "; 00206 break; 00207 case Constraint::NONSTRICT_INEQUALITY: 00208 relation_symbol = " >= "; 00209 break; 00210 case Constraint::STRICT_INEQUALITY: 00211 relation_symbol = " > "; 00212 break; 00213 } 00214 s << relation_symbol << -c.inhomogeneous_term(); 00215 return s; 00216 } 00217 00219 std::ostream& 00220 PPL::IO_Operators::operator<<(std::ostream& s, const Constraint::Type& t) { 00221 const char* n = 0; 00222 switch (t) { 00223 case Constraint::EQUALITY: 00224 n = "EQUALITY"; 00225 break; 00226 case Constraint::NONSTRICT_INEQUALITY: 00227 n = "NONSTRICT_INEQUALITY"; 00228 break; 00229 case Constraint::STRICT_INEQUALITY: 00230 n = "STRICT_INEQUALITY"; 00231 break; 00232 } 00233 s << n; 00234 return s; 00235 } 00236 00237 PPL_OUTPUT_DEFINITIONS(Constraint); 00238 00239 bool 00240 PPL::Constraint::OK() const { 00241 // Topology consistency check. 00242 const dimension_type min_size = is_necessarily_closed() ? 1 : 2; 00243 if (size() < min_size) { 00244 #ifndef NDEBUG 00245 std::cerr << "Constraint has fewer coefficients than the minimum " 00246 << "allowed by its topology:" 00247 << std::endl 00248 << "size is " << size() 00249 << ", minimum is " << min_size << "." 00250 << std::endl; 00251 #endif 00252 return false; 00253 } 00254 00255 // Normalization check. 00256 Constraint tmp = *this; 00257 tmp.strong_normalize(); 00258 if (tmp != *this) { 00259 #ifndef NDEBUG 00260 std::cerr << "Constraint is not strongly normalized as it should be." 00261 << std::endl; 00262 #endif 00263 return false; 00264 } 00265 00266 // All tests passed. 00267 return true; 00268 }