00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023 #include <ppl-config.h>
00024
00025 #include "Constraint.defs.hh"
00026 #include "Variable.defs.hh"
00027 #include "Congruence.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_invalid_argument(const char* method,
00036 const char* message) const {
00037 std::ostringstream s;
00038 s << "PPL::Constraint::" << method << ":" << std::endl
00039 << message;
00040 throw std::invalid_argument(s.str());
00041 }
00042
00043 void
00044 PPL::Constraint::throw_dimension_incompatible(const char* method,
00045 const char* name_var,
00046 const Variable v) const {
00047 std::ostringstream s;
00048 s << "PPL::Constraint::" << method << ":" << std::endl
00049 << "this->space_dimension() == " << space_dimension() << ", "
00050 << name_var << ".space_dimension() == " << v.space_dimension() << ".";
00051 throw std::invalid_argument(s.str());
00052 }
00053
00054 PPL::Constraint
00055 PPL::Constraint::construct_epsilon_geq_zero() {
00056 Linear_Expression e = Variable(0);
00057 Constraint c(e, NONSTRICT_INEQUALITY, NOT_NECESSARILY_CLOSED);
00058 return c;
00059 }
00060
00061 PPL::Constraint::Constraint(const Congruence& cg)
00062 : Linear_Row(cg.is_equality()
00063
00064 ? cg.space_dimension() + 1
00065 : (throw_invalid_argument("Constraint(cg)",
00066 "congruence cg must be an equality."),
00067 0),
00068
00069 compute_capacity(cg.space_dimension() + 2, Row::max_size()),
00070 Flags(NECESSARILY_CLOSED, LINE_OR_EQUALITY)) {
00071 Constraint& c = *this;
00072
00073 for (dimension_type i = cg.space_dimension() + 1; i-- > 0; )
00074 c[i] = cg[i];
00075
00076 strong_normalize();
00077 }
00078
00079 PPL::Constraint::Constraint(const Congruence& cg,
00080 dimension_type sz,
00081 dimension_type capacity)
00082 : Linear_Row(cg.is_equality()
00083 ? sz
00084 : (throw_invalid_argument("Constraint(cg, sz, c)",
00085 "congruence cg must be an equality."),
00086 0),
00087 capacity,
00088 Flags(NECESSARILY_CLOSED, LINE_OR_EQUALITY)) {
00089 Constraint& c = *this;
00090
00091 assert(sz > 0);
00092 while (sz-- > 0)
00093 c[sz] = cg[sz];
00094 }
00095
00096 bool
00097 PPL::Constraint::is_tautological() const {
00098 assert(size() > 0);
00099 const Constraint& x = *this;
00100 if (x.all_homogeneous_terms_are_zero())
00101 if (is_equality())
00102 return x[0] == 0;
00103 else
00104
00105 return x[0] >= 0;
00106 else
00107
00108 if (is_necessarily_closed())
00109 return false;
00110 else {
00111
00112 const dimension_type eps_index = size() - 1;
00113 const int eps_sign = sgn(x[eps_index]);
00114 if (eps_sign > 0)
00115
00116 return true;
00117 if (eps_sign == 0)
00118
00119 return false;
00120 else {
00121
00122 if (x[0] <= 0)
00123
00124
00125 return false;
00126
00127 for (dimension_type i = eps_index; --i > 0; )
00128 if (x[i] != 0)
00129 return false;
00130
00131
00132 return true;
00133 }
00134 }
00135 }
00136
00137 bool
00138 PPL::Constraint::is_inconsistent() const {
00139 assert(size() > 0);
00140 const Constraint& x = *this;
00141 if (x.all_homogeneous_terms_are_zero())
00142
00143 if (is_equality())
00144 return x[0] != 0;
00145 else
00146
00147 return x[0] < 0;
00148 else
00149
00150 if (is_necessarily_closed())
00151 return false;
00152 else {
00153
00154 const dimension_type eps_index = size() - 1;
00155 if (x[eps_index] >= 0)
00156
00157
00158
00159 return false;
00160 else {
00161
00162 if (x[0] > 0)
00163
00164
00165 return false;
00166
00167 for (dimension_type i = eps_index; --i > 0; )
00168 if (x[i] != 0)
00169 return false;
00170
00171
00172 return true;
00173 }
00174 }
00175 }
00176
00177 bool
00178 PPL::Constraint::is_equivalent_to(const Constraint& y) const {
00179 const Constraint& x = *this;
00180 const dimension_type x_space_dim = x.space_dimension();
00181 if (x_space_dim != y.space_dimension())
00182 return false;
00183
00184 const Type x_type = x.type();
00185 if (x_type != y.type()) {
00186
00187 if (x.is_tautological())
00188 return y.is_tautological();
00189 else
00190 return x.is_inconsistent() && y.is_inconsistent();
00191 }
00192
00193 if (x_type == STRICT_INEQUALITY) {
00194
00195
00196
00197
00198 Linear_Expression x_expr(x);
00199 Linear_Expression y_expr(y);
00200
00201 x_expr.normalize();
00202 y_expr.normalize();
00203
00204 for (dimension_type i = x_space_dim + 1; i-- > 0; )
00205 if (x_expr[i] != y_expr[i])
00206 return false;
00207 return true;
00208 }
00209
00210
00211
00212
00213 for (dimension_type i = x_space_dim + 1; i-- > 0; )
00214 if (x[i] != y[i])
00215 return false;
00216 return true;
00217 }
00218
00219 const PPL::Constraint* PPL::Constraint::zero_dim_false_p = 0;
00220 const PPL::Constraint* PPL::Constraint::zero_dim_positivity_p = 0;
00221 const PPL::Constraint* PPL::Constraint::epsilon_geq_zero_p = 0;
00222 const PPL::Constraint* PPL::Constraint::epsilon_leq_one_p = 0;
00223
00224 void
00225 PPL::Constraint::initialize() {
00226 assert(zero_dim_false_p == 0);
00227 zero_dim_false_p
00228 = new Constraint(Linear_Expression::zero() == Coefficient_one());
00229
00230 assert(zero_dim_positivity_p == 0);
00231 zero_dim_positivity_p
00232 = new Constraint(Linear_Expression::zero() <= Coefficient_one());
00233
00234 assert(epsilon_geq_zero_p == 0);
00235 epsilon_geq_zero_p
00236 = new Constraint(construct_epsilon_geq_zero());
00237
00238 assert(epsilon_leq_one_p == 0);
00239 epsilon_leq_one_p
00240 = new Constraint(Linear_Expression::zero() < Coefficient_one());
00241 }
00242
00243 void
00244 PPL::Constraint::finalize() {
00245 assert(zero_dim_false_p != 0);
00246 delete zero_dim_false_p;
00247 zero_dim_false_p = 0;
00248
00249 assert(zero_dim_positivity_p != 0);
00250 delete zero_dim_positivity_p;
00251 zero_dim_positivity_p = 0;
00252
00253 assert(epsilon_geq_zero_p != 0);
00254 delete epsilon_geq_zero_p;
00255 epsilon_geq_zero_p = 0;
00256
00257 assert(epsilon_leq_one_p != 0);
00258 delete epsilon_leq_one_p;
00259 epsilon_leq_one_p = 0;
00260 }
00261
00263 std::ostream&
00264 PPL::IO_Operators::operator<<(std::ostream& s, const Constraint& c) {
00265 const dimension_type num_variables = c.space_dimension();
00266 TEMP_INTEGER(cv);
00267 bool first = true;
00268 for (dimension_type v = 0; v < num_variables; ++v) {
00269 cv = c.coefficient(Variable(v));
00270 if (cv != 0) {
00271 if (!first) {
00272 if (cv > 0)
00273 s << " + ";
00274 else {
00275 s << " - ";
00276 neg_assign(cv);
00277 }
00278 }
00279 else
00280 first = false;
00281 if (cv == -1)
00282 s << "-";
00283 else if (cv != 1)
00284 s << cv << "*";
00285 s << PPL::Variable(v);
00286 }
00287 }
00288 if (first)
00289 s << Coefficient_zero();
00290 const char* relation_symbol = 0;
00291 switch (c.type()) {
00292 case Constraint::EQUALITY:
00293 relation_symbol = " = ";
00294 break;
00295 case Constraint::NONSTRICT_INEQUALITY:
00296 relation_symbol = " >= ";
00297 break;
00298 case Constraint::STRICT_INEQUALITY:
00299 relation_symbol = " > ";
00300 break;
00301 }
00302 s << relation_symbol << -c.inhomogeneous_term();
00303 return s;
00304 }
00305
00307 std::ostream&
00308 PPL::IO_Operators::operator<<(std::ostream& s, const Constraint::Type& t) {
00309 const char* n = 0;
00310 switch (t) {
00311 case Constraint::EQUALITY:
00312 n = "EQUALITY";
00313 break;
00314 case Constraint::NONSTRICT_INEQUALITY:
00315 n = "NONSTRICT_INEQUALITY";
00316 break;
00317 case Constraint::STRICT_INEQUALITY:
00318 n = "STRICT_INEQUALITY";
00319 break;
00320 }
00321 s << n;
00322 return s;
00323 }
00324
00325 PPL_OUTPUT_DEFINITIONS(Constraint)
00326
00327 bool
00328 PPL::Constraint::OK() const {
00329
00330 if (!Linear_Row::OK())
00331 return false;
00332
00333
00334 const dimension_type min_size = is_necessarily_closed() ? 1 : 2;
00335 if (size() < min_size) {
00336 #ifndef NDEBUG
00337 std::cerr << "Constraint has fewer coefficients than the minimum "
00338 << "allowed by its topology:"
00339 << std::endl
00340 << "size is " << size()
00341 << ", minimum is " << min_size << "."
00342 << std::endl;
00343 #endif
00344 return false;
00345 }
00346
00347 if (is_equality() && !is_necessarily_closed() && (*this)[size() - 1] != 0) {
00348 #ifndef NDEBUG
00349 std::cerr << "Illegal constraint: an equality cannot be strict."
00350 << std::endl;
00351 #endif
00352 return false;
00353 }
00354
00355
00356 Constraint tmp = *this;
00357 tmp.strong_normalize();
00358 if (tmp != *this) {
00359 #ifndef NDEBUG
00360 std::cerr << "Constraint is not strongly normalized as it should be."
00361 << std::endl;
00362 #endif
00363 return false;
00364 }
00365
00366
00367 return true;
00368 }