00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023 #include <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
00045 (*this)[size()-1] = 0;
00046 }
00047
00048 PPL::Congruence::Congruence(const Constraint& c,
00049 dimension_type sz, dimension_type capacity)
00050 : Row(c.is_equality()
00051 ? c
00052 : (throw_invalid_argument("Congruence(c)",
00053 "constraint c must be an equality."),
00054 c),
00055 sz,
00056 capacity) {
00057
00058 (*this)[sz-1] = 0;
00059 }
00060
00061 void
00062 PPL::Congruence::sign_normalize() {
00063 Row& x = *this;
00064 const dimension_type sz = x.size() - 1;
00065
00066
00067
00068 dimension_type first_non_zero;
00069 for (first_non_zero = 1; first_non_zero < sz; ++first_non_zero)
00070 if (x[first_non_zero] != 0)
00071 break;
00072 if (first_non_zero < sz)
00073
00074
00075 if (x[first_non_zero] < 0) {
00076 for (dimension_type j = first_non_zero; j < sz; ++j)
00077 neg_assign(x[j]);
00078
00079 neg_assign(x[0]);
00080 }
00081 }
00082
00083 void
00084 PPL::Congruence::normalize() {
00085 sign_normalize();
00086
00087 dimension_type sz = size();
00088 if (sz == 0)
00089 return;
00090
00091 Coefficient_traits::const_reference mod = modulus();
00092 if (mod == 0)
00093 return;
00094
00095 Coefficient& row_0 = (*this)[0];
00096
00097 row_0 %= mod;
00098 if (row_0 < 0)
00099
00100 row_0 += mod;
00101 return;
00102 }
00103
00104 void
00105 PPL::Congruence::strong_normalize() {
00106 normalize();
00107 Row::normalize();
00108 }
00109
00111 PPL::Congruence
00112 PPL::operator%=(const Linear_Expression& e1, const Linear_Expression& e2) {
00113
00114 dimension_type dim, e1_dim, e2_dim;
00115 e1_dim = e1.space_dimension();
00116 e2_dim = e2.space_dimension();
00117 if (e1_dim > e2_dim)
00118 dim = e1_dim;
00119 else
00120 dim = e2_dim;
00121 Linear_Expression diff(e1_dim > e2_dim ? e1 : e2,
00122 dim + 2);
00123 diff -= (e1_dim > e2_dim ? e2 : e1);
00124 Congruence cg(diff, 1, false);
00125 return cg;
00126 }
00127
00128 void
00129 PPL::Congruence::throw_invalid_argument(const char* method,
00130 const char* message) const {
00131 std::ostringstream s;
00132 s << "PPL::Congruence::" << method << ":" << std::endl
00133 << message;
00134 throw std::invalid_argument(s.str());
00135 }
00136
00137 void
00138 PPL::Congruence::throw_dimension_incompatible(const char* method,
00139 const char* v_name,
00140 const Variable v) const {
00141 std::ostringstream s;
00142 s << "this->space_dimension() == " << space_dimension() << ", "
00143 << v_name << ".space_dimension() == " << v.space_dimension() << ".";
00144 throw_invalid_argument(method, s.str().c_str());
00145 }
00146
00148 std::ostream&
00149 PPL::IO_Operators::operator<<(std::ostream& s, const Congruence& c) {
00150 const int num_variables = c.space_dimension();
00151 bool first = true;
00152 for (int v = 0; v < num_variables; ++v) {
00153 Coefficient cv = c.coefficient(Variable(v));
00154 if (cv != 0) {
00155 if (!first) {
00156 if (cv > 0)
00157 s << " + ";
00158 else {
00159 s << " - ";
00160 neg_assign(cv);
00161 }
00162 }
00163 else
00164 first = false;
00165 if (cv == -1)
00166 s << "-";
00167 else if (cv != 1)
00168 s << cv << "*";
00169 s << PPL::Variable(v);
00170 }
00171 }
00172 if (first)
00173 s << Coefficient_zero();
00174 s << " = " << -c.inhomogeneous_term();
00175 if (c.is_proper_congruence())
00176 s << " (mod " << c.modulus() << ")";
00177 return s;
00178 }
00179
00180 bool
00181 PPL::Congruence::is_trivial_true() const {
00182 if ((is_equality() && inhomogeneous_term() == 0)
00183 || (is_proper_congruence()
00184 && (inhomogeneous_term() % modulus() == 0))) {
00185 for (unsigned i = 1; i <= space_dimension(); i++)
00186 if ((*this)[i] != 0)
00187 return false;
00188 return true;
00189 }
00190 return false;
00191 }
00192
00193 bool
00194 PPL::Congruence::is_trivial_false() const {
00195 if (inhomogeneous_term() == 0
00196 || (is_proper_congruence()
00197 && ((inhomogeneous_term() % modulus()) == 0)))
00198 return false;
00199 for (unsigned i = 1; i <= space_dimension(); i++)
00200 if ((*this)[i] != 0)
00201 return false;
00202 return true;
00203 }
00204
00205 void
00206 PPL::Congruence::ascii_dump(std::ostream& s) const {
00207 const Row& x = *this;
00208 dimension_type x_size = x.size();
00209 for (dimension_type i = 0; i < x_size - 1; ++i)
00210 s << x[i] << ' ';
00211 if (x_size)
00212 s << "m " << x[x_size - 1];
00213 s << std::endl;
00214 }
00215
00216 PPL_OUTPUT_DEFINITIONS(Congruence);
00217
00218 bool
00219 PPL::Congruence::ascii_load(std::istream& s) {
00220 std::string str;
00221 Congruence& x = *this;
00222 dimension_type col = 0;
00223 while (col < x.size() - 1)
00224 if (!(s >> x[col]))
00225 return false;
00226 else
00227 col++;
00228
00229 if (!(s >> str) || str.compare("m"))
00230 return false;
00231
00232 if (!(s >> x[col]))
00233 return false;
00234
00235 return true;
00236 }
00237
00238 bool
00239 PPL::Congruence::OK() const {
00240
00241 if (modulus() < 0) {
00242 #ifndef NDEBUG
00243 std::cerr << "Congruence has a negative modulus " << modulus() << "."
00244 << std::endl;
00245 #endif
00246 return false;
00247 }
00248
00249
00250 return true;
00251 }