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 "Congruence.defs.hh"
00026
00027 #include "Variable.defs.hh"
00028 #include <cassert>
00029 #include <iostream>
00030 #include <sstream>
00031 #include <stdexcept>
00032 #include <string>
00033
00034 namespace PPL = Parma_Polyhedra_Library;
00035
00036 PPL::Congruence::Congruence(const Constraint& c)
00037 : Row(c.is_equality()
00038 ? c
00039 : (throw_invalid_argument("Congruence(c)",
00040 "constraint c must be an equality."),
00041 c),
00042 c.space_dimension() + 2,
00043 compute_capacity(c.space_dimension() + 2, Row::max_size())) {
00044 (*this)[size()-1] = 0;
00045 }
00046
00047 PPL::Congruence::Congruence(const Constraint& c,
00048 dimension_type sz, dimension_type capacity)
00049 : Row(c.is_equality()
00050 ? c
00051 : (throw_invalid_argument("Congruence(c)",
00052 "constraint c must be an equality."),
00053 c),
00054 sz,
00055 capacity) {
00056 assert(sz > 1);
00057 (*this)[sz-1] = 0;
00058 }
00059
00060 void
00061 PPL::Congruence::sign_normalize() {
00062 Row& x = *this;
00063 const dimension_type sz = x.size() - 1;
00064
00065
00066
00067 dimension_type first_non_zero;
00068 for (first_non_zero = 1; first_non_zero < sz; ++first_non_zero)
00069 if (x[first_non_zero] != 0)
00070 break;
00071 if (first_non_zero < sz)
00072
00073
00074 if (x[first_non_zero] < 0) {
00075 for (dimension_type j = first_non_zero; j < sz; ++j)
00076 neg_assign(x[j]);
00077
00078 neg_assign(x[0]);
00079 }
00080 }
00081
00082 void
00083 PPL::Congruence::normalize() {
00084 sign_normalize();
00085
00086 dimension_type sz = size();
00087 if (sz == 0)
00088 return;
00089
00090 const Coefficient& mod = modulus();
00091 if (mod == 0)
00092 return;
00093
00094 Coefficient& row_0 = (*this)[0];
00095
00096 row_0 %= mod;
00097 if (row_0 < 0)
00098
00099 row_0 += mod;
00100 return;
00101 }
00102
00103 void
00104 PPL::Congruence::strong_normalize() {
00105 normalize();
00106 Row::normalize();
00107 }
00108
00109 PPL::Congruence
00110 PPL::Congruence::create(const Linear_Expression& e1,
00111 const Linear_Expression& e2) {
00112
00113 dimension_type dim, e1_dim, e2_dim;
00114 e1_dim = e1.space_dimension();
00115 e2_dim = e2.space_dimension();
00116 if (e1_dim > e2_dim)
00117 dim = e1_dim;
00118 else
00119 dim = e2_dim;
00120 Linear_Expression diff(e1_dim > e2_dim ? e1 : e2,
00121 dim + 2);
00122 diff -= (e1_dim > e2_dim ? e2 : e1);
00123 Congruence cg(diff, 1);
00124 return cg;
00125 }
00126
00127 void
00128 PPL::Congruence::throw_invalid_argument(const char* method,
00129 const char* message) const {
00130 std::ostringstream s;
00131 s << "PPL::Congruence::" << method << ":" << std::endl
00132 << message;
00133 throw std::invalid_argument(s.str());
00134 }
00135
00136 void
00137 PPL::Congruence::throw_dimension_incompatible(const char* method,
00138 const char* v_name,
00139 const Variable v) const {
00140 std::ostringstream s;
00141 s << "this->space_dimension() == " << space_dimension() << ", "
00142 << v_name << ".space_dimension() == " << v.space_dimension() << ".";
00143 std::string str = s.str();
00144 throw_invalid_argument(method, str.c_str());
00145 }
00146
00148 std::ostream&
00149 PPL::IO_Operators::operator<<(std::ostream& s, const Congruence& c) {
00150 const dimension_type num_variables = c.space_dimension();
00151 TEMP_INTEGER(cv);
00152 bool first = true;
00153 for (dimension_type v = 0; v < num_variables; ++v) {
00154 cv = c.coefficient(Variable(v));
00155 if (cv != 0) {
00156 if (!first) {
00157 if (cv > 0)
00158 s << " + ";
00159 else {
00160 s << " - ";
00161 neg_assign(cv);
00162 }
00163 }
00164 else
00165 first = false;
00166 if (cv == -1)
00167 s << "-";
00168 else if (cv != 1)
00169 s << cv << "*";
00170 s << PPL::Variable(v);
00171 }
00172 }
00173 if (first)
00174 s << Coefficient_zero();
00175 s << " = " << -c.inhomogeneous_term();
00176 if (c.is_proper_congruence())
00177 s << " (mod " << c.modulus() << ")";
00178 return s;
00179 }
00180
00181 bool
00182 PPL::Congruence::is_tautological() const {
00183 if ((is_equality() && inhomogeneous_term() == 0)
00184 || (is_proper_congruence()
00185 && (inhomogeneous_term() % modulus() == 0))) {
00186 for (unsigned i = space_dimension(); i > 0; --i)
00187 if (operator[](i) != 0)
00188 return false;
00189 return true;
00190 }
00191 return false;
00192 }
00193
00194 bool
00195 PPL::Congruence::is_inconsistent() const {
00196 if (inhomogeneous_term() == 0
00197 || (is_proper_congruence()
00198 && ((inhomogeneous_term() % modulus()) == 0)))
00199 return false;
00200 for (unsigned i = space_dimension(); i > 0; --i)
00201 if (operator[](i) != 0)
00202 return false;
00203 return true;
00204 }
00205
00206 void
00207 PPL::Congruence::ascii_dump(std::ostream& s) const {
00208 const Row& x = *this;
00209 const dimension_type x_size = x.size();
00210 s << "size " << x_size << " ";
00211 if (x_size > 0) {
00212 for (dimension_type i = 0; i < x_size - 1; ++i)
00213 s << x[i] << ' ';
00214 s << "m " << x[x_size - 1];
00215 }
00216 s << std::endl;
00217 }
00218
00219 PPL_OUTPUT_DEFINITIONS(Congruence)
00220
00221 bool
00222 PPL::Congruence::ascii_load(std::istream& s) {
00223 std::string str;
00224 if (!(s >> str) || str != "size")
00225 return false;
00226 dimension_type new_size;
00227 if (!(s >> new_size))
00228 return false;
00229
00230 Row& x = *this;
00231 const dimension_type old_size = x.size();
00232 if (new_size < old_size)
00233 x.shrink(new_size);
00234 else if (new_size > old_size) {
00235 Row y(new_size, Row::Flags());
00236 x.swap(y);
00237 }
00238
00239 if (new_size > 0) {
00240 for (dimension_type col = 0; col < new_size - 1; ++col)
00241 if (!(s >> x[col]))
00242 return false;
00243 if (!(s >> str) || (str.compare("m") != 0))
00244 return false;
00245 if (!(s >> x[new_size-1]))
00246 return false;
00247 }
00248 return true;
00249 }
00250
00251 bool
00252 PPL::Congruence::OK() const {
00253
00254 if (!Row::OK())
00255 return false;
00256
00257
00258 if (modulus() < 0) {
00259 #ifndef NDEBUG
00260 std::cerr << "Congruence has a negative modulus " << modulus() << "."
00261 << std::endl;
00262 #endif
00263 return false;
00264 }
00265
00266
00267 return true;
00268 }
00269
00270 const PPL::Congruence* PPL::Congruence::zero_dim_false_p = 0;
00271 const PPL::Congruence* PPL::Congruence::zero_dim_integrality_p = 0;
00272
00273 void
00274 PPL::Congruence::initialize() {
00275 assert(zero_dim_false_p == 0);
00276 zero_dim_false_p
00277 = new Congruence((Linear_Expression::zero() %= Coefficient(-1)) / 0);
00278
00279 assert(zero_dim_integrality_p == 0);
00280 zero_dim_integrality_p
00281 = new Congruence(Linear_Expression::zero() %= Coefficient(-1));
00282 }
00283
00284 void
00285 PPL::Congruence::finalize() {
00286 assert(zero_dim_false_p != 0);
00287 delete zero_dim_false_p;
00288 zero_dim_false_p = 0;
00289
00290 assert(zero_dim_integrality_p != 0);
00291 delete zero_dim_integrality_p;
00292 zero_dim_integrality_p = 0;
00293 }