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_System.defs.hh"
00026 #include "Congruence_System.inlines.hh"
00027 #include "Constraint_System.defs.hh"
00028 #include "Constraint_System.inlines.hh"
00029 #include "Congruence.defs.hh"
00030 #include "Grid_Generator.defs.hh"
00031 #include "Scalar_Products.defs.hh"
00032 #include <cassert>
00033 #include <string>
00034 #include <vector>
00035 #include <iostream>
00036 #include <stdexcept>
00037
00038 namespace PPL = Parma_Polyhedra_Library;
00039
00040 PPL::Congruence_System::Congruence_System(const Constraint_System& cs)
00041 : Matrix(0, 2) {
00042 for (Constraint_System::const_iterator i = cs.begin(),
00043 cs_end = cs.end(); i != cs_end; ++i)
00044 if (i->is_equality())
00045 insert(*i);
00046 }
00047
00048 bool
00049 PPL::Congruence_System::
00050 increase_space_dimension(const dimension_type new_space_dim) {
00051 assert(space_dimension() <= new_space_dim);
00052
00053 dimension_type cols_to_add = new_space_dim - space_dimension();
00054
00055 if (cols_to_add)
00056 if (num_rows()) {
00057 dimension_type old_num_cols = num_columns();
00058 add_zero_columns(cols_to_add);
00059
00060 swap_columns(num_columns() - 1, old_num_cols - 1);
00061 }
00062 else
00063
00064 add_zero_columns(cols_to_add);
00065
00066 assert(OK());
00067 return true;
00068 }
00069
00070 void
00071 PPL::Congruence_System::insert_verbatim(const Congruence& cg) {
00072 const dimension_type old_num_columns = num_columns();
00073 const dimension_type cg_size = cg.size();
00074
00075 if (cg_size > old_num_columns) {
00076
00077 add_zero_columns(cg_size - old_num_columns);
00078 if (num_rows() != 0)
00079
00080 swap_columns(old_num_columns - 1, cg_size - 1);
00081 add_row(cg);
00082 }
00083 else if (cg_size < old_num_columns) {
00084
00085 Congruence rc(cg, old_num_columns, row_capacity);
00086
00087 std::swap(rc[cg_size - 1], rc[old_num_columns - 1]);
00088 add_recycled_row(rc);
00089 }
00090 else
00091
00092 add_row(cg);
00093
00094 assert(OK());
00095 }
00096
00097 void
00098 PPL::Congruence_System::insert(const Constraint& c) {
00099 dimension_type cg_size = c.space_dimension() + 2;
00100 const dimension_type old_num_columns = num_columns();
00101 if (cg_size < old_num_columns) {
00102
00103 Congruence cg(c, old_num_columns, row_capacity);
00104 add_recycled_row(cg);
00105 }
00106 else {
00107 if (cg_size > old_num_columns) {
00108
00109 add_zero_columns(cg_size - old_num_columns);
00110 if (num_rows() != 0)
00111
00112 swap_columns(old_num_columns - 1, cg_size - 1);
00113 }
00114 Congruence cg(c, cg_size, row_capacity);
00115 add_recycled_row(cg);
00116 }
00117 operator[](rows.size()-1).strong_normalize();
00118
00119 assert(OK());
00120 }
00121
00122 void
00123 PPL::Congruence_System::recycling_insert(Congruence_System& cgs) {
00124 const dimension_type old_num_rows = num_rows();
00125 const dimension_type cgs_num_rows = cgs.num_rows();
00126 const dimension_type old_num_cols = num_columns();
00127 dimension_type cgs_num_cols = cgs.num_columns();
00128 if (old_num_cols >= cgs_num_cols)
00129 add_zero_rows(cgs_num_rows, Row::Flags());
00130 else {
00131 add_zero_rows_and_columns(cgs_num_rows,
00132 cgs_num_cols - old_num_cols,
00133 Row::Flags());
00134
00135 swap_columns(old_num_cols - 1, num_columns() - 1);
00136 }
00137 --cgs_num_cols;
00138 const dimension_type mod_index = num_columns() - 1;
00139 for (dimension_type i = cgs_num_rows; i-- > 0; ) {
00140
00141
00142
00143 Congruence& new_cg = operator[](old_num_rows + i);
00144 Congruence& old_cg = cgs[i];
00145 for (dimension_type j = cgs_num_cols; j-- > 0; )
00146 std::swap(new_cg[j], old_cg[j]);
00147 std::swap(new_cg[mod_index], old_cg[cgs_num_cols]);
00148 }
00149
00150 assert(OK());
00151 }
00152
00153 void
00154 PPL::Congruence_System::insert(const Congruence_System& y) {
00155 Congruence_System& x = *this;
00156
00157 const dimension_type x_n_rows = x.num_rows();
00158 const dimension_type y_n_rows = y.num_rows();
00159 const dimension_type old_n_cols = x.num_columns();
00160 const dimension_type y_n_cols = y.num_columns();
00161
00162 if (old_n_cols >= y_n_cols)
00163 add_zero_rows(y_n_rows, Row::Flags());
00164 else {
00165 add_zero_rows_and_columns(y_n_rows,
00166 y_n_cols - old_n_cols,
00167 Row::Flags());
00168
00169 swap_columns(old_n_cols - 1, num_columns() - 1);
00170 }
00171
00172
00173 const dimension_type x_mod_index = x.num_columns() - 1;
00174 const dimension_type y_mod_index = y_n_cols - 1;
00175 for (dimension_type i = y_n_rows; i-- > 0; ) {
00176 Row copy(y[i], x.row_size, x.row_capacity);
00177
00178 std::swap(copy[x_mod_index], copy[y_mod_index]);
00179 std::swap(copy, x[x_n_rows+i]);
00180 }
00181 assert(OK());
00182 }
00183
00184 void
00185 PPL::Congruence_System::normalize_moduli() {
00186 dimension_type row = num_rows();
00187 if (row > 0) {
00188
00189 TEMP_INTEGER(lcm);
00190
00191 while (true) {
00192 lcm = operator[](--row).modulus();
00193 if (lcm > 0)
00194 break;
00195 if (row == 0)
00196
00197 return;
00198 }
00199 while (row > 0) {
00200 TEMP_INTEGER(modulus);
00201 modulus = operator[](--row).modulus();
00202 if (modulus > 0)
00203 lcm_assign(lcm, lcm, modulus);
00204 }
00205
00206
00207 dimension_type row_size = operator[](0).size();
00208 for (dimension_type row = num_rows(); row-- > 0; ) {
00209 TEMP_INTEGER(modulus);
00210 modulus = operator[](row).modulus();
00211 if (modulus <= 0 || modulus == lcm)
00212 continue;
00213 TEMP_INTEGER(factor);
00214 factor = lcm / modulus;
00215 for (dimension_type col = row_size; col-- > 0; )
00216 operator[](row)[col] *= factor;
00217 operator[](row)[row_size-1] = lcm;
00218 }
00219 }
00220 assert(OK());
00221 }
00222
00223 bool
00224 PPL::Congruence_System::is_equal_to(const Congruence_System& cgs) const {
00225 if (num_rows() != cgs.num_rows())
00226 return false;
00227
00228 for (dimension_type row = 0; row < cgs.num_rows(); ++row)
00229 for (dimension_type col = 0; col < cgs.num_columns(); ++col) {
00230 if (operator[](row)[col] == cgs[row][col])
00231 continue;
00232 return false;
00233 }
00234 return true;
00235 }
00236
00237 bool
00238 PPL::Congruence_System::has_linear_equalities() const {
00239 const Congruence_System& cgs = *this;
00240 dimension_type modulus_index = cgs.num_columns() - 1;
00241 for (dimension_type i = cgs.num_rows(); i-- > 0; )
00242 if (cgs[i][modulus_index] == 0)
00243 return true;
00244 return false;
00245 }
00246
00247 void
00248 PPL::Congruence_System::const_iterator::skip_forward() {
00249 const Matrix::const_iterator csp_end = csp->end();
00250 while (i != csp_end && (*this)->is_trivial_true())
00251 ++i;
00252 }
00253
00254 PPL::dimension_type
00255 PPL::Congruence_System::num_equalities() const {
00256 const Congruence_System& cgs = *this;
00257 dimension_type n = 0;
00258 for (dimension_type i = num_rows(); i-- > 0 ; )
00259 if (cgs[i].is_equality())
00260 ++n;
00261 return n;
00262 }
00263
00264 PPL::dimension_type
00265 PPL::Congruence_System::num_proper_congruences() const {
00266 const Congruence_System& cgs = *this;
00267 dimension_type n = 0;
00268 for (dimension_type i = num_rows(); i-- > 0 ; ) {
00269 const Congruence& cg = cgs[i];
00270 if (cg.is_proper_congruence())
00271 ++n;
00272 }
00273 return n;
00274 }
00275
00276 bool
00277 PPL::Congruence_System::
00278 satisfies_all_congruences(const Grid_Generator& g) const {
00279 assert(g.space_dimension() <= space_dimension());
00280
00281 const Congruence_System& cgs = *this;
00282 TEMP_INTEGER(sp);
00283 if (g.is_line())
00284 for (dimension_type i = cgs.num_rows(); i-- > 0; ) {
00285 const Congruence& cg = cgs[i];
00286 Scalar_Products::assign(sp, g, cg);
00287 if (sp != 0)
00288 return false;
00289 }
00290 else {
00291 const Coefficient& divisor = g.divisor();
00292 for (dimension_type i = cgs.num_rows(); i-- > 0; ) {
00293 const Congruence& cg = cgs[i];
00294 Scalar_Products::assign(sp, g, cg);
00295 if (cg.is_equality()) {
00296 if (sp != 0)
00297 return false;
00298 }
00299 else if (sp % (cg.modulus() * divisor) != 0)
00300 return false;
00301 }
00302 }
00303 return true;
00304 }
00305
00306 bool
00307 PPL::Congruence_System::has_a_free_dimension() const {
00308
00309
00310 dimension_type space_dim = space_dimension();
00311 std::vector<bool> free_dim(space_dim, true);
00312 dimension_type free_dims = space_dim;
00313 for (dimension_type row = num_rows(); row-- > 0; ) {
00314 const Congruence& cg = operator[](row);
00315 for (dimension_type dim = 0; dim < space_dim; ++dim)
00316 if (free_dim[dim] && cg[dim+1] != 0) {
00317 if (--free_dims == 0) {
00318
00319 #ifndef NDEBUG
00320 free_dim[dim] = false;
00321
00322
00323 dimension_type count = 0;
00324 for (dimension_type dim = 0; dim < space_dim; ++dim)
00325 count += free_dim[dim];
00326 assert(count == free_dims);
00327 #endif
00328 return true;
00329 }
00330 free_dim[dim] = false;
00331 }
00332 }
00333
00334 return false;
00335 }
00336
00337 void
00338 PPL::Congruence_System::
00339 affine_preimage(dimension_type v,
00340 const Linear_Expression& expr,
00341 Coefficient_traits::const_reference denominator) {
00342
00343
00344 assert(v > 0 && v <= space_dimension());
00345 assert(expr.space_dimension() <= space_dimension());
00346 assert(denominator > 0);
00347
00348 const dimension_type n_columns = num_columns();
00349 const dimension_type n_rows = num_rows();
00350 const dimension_type expr_size = expr.size();
00351 const bool not_invertible = (v >= expr_size || expr[v] == 0);
00352 Congruence_System& x = *this;
00353
00354 if (denominator == 1)
00355
00356
00357 for (dimension_type i = n_rows; i-- > 0; ) {
00358 Congruence& row = x[i];
00359 Coefficient& row_v = row[v];
00360 if (row_v != 0) {
00361 for (dimension_type j = expr_size; j-- > 0; )
00362 if (j != v)
00363
00364 add_mul_assign(row[j], row_v, expr[j]);
00365 if (not_invertible)
00366 row_v = 0;
00367 else
00368 row_v *= expr[v];
00369 }
00370 }
00371 else
00372 for (dimension_type i = n_rows; i-- > 0; ) {
00373 Congruence& row = x[i];
00374 Coefficient& row_v = row[v];
00375 if (row_v != 0) {
00376 for (dimension_type j = n_columns; j-- > 0; )
00377 if (j != v) {
00378 Coefficient& row_j = row[j];
00379 row_j *= denominator;
00380 if (j < expr_size)
00381 add_mul_assign(row_j, row_v, expr[j]);
00382 }
00383 if (not_invertible)
00384 row_v = 0;
00385 else
00386 row_v *= expr[v];
00387 }
00388 }
00389 }
00390
00391 void
00392 PPL::Congruence_System::ascii_dump(std::ostream& s) const {
00393 const Congruence_System& x = *this;
00394 dimension_type x_num_rows = x.num_rows();
00395 dimension_type x_num_columns = x.num_columns();
00396 s << x_num_rows << " x " << x_num_columns
00397 << std::endl;
00398 if (x_num_rows && x_num_columns)
00399 for (dimension_type i = 0; i < x_num_rows; ++i)
00400 x[i].ascii_dump(s);
00401 }
00402
00403 PPL_OUTPUT_DEFINITIONS(Congruence_System);
00404
00405 bool
00406 PPL::Congruence_System::ascii_load(std::istream& s) {
00407 std::string str;
00408 dimension_type nrows;
00409 dimension_type ncols;
00410 if (!(s >> nrows))
00411 return false;
00412 if (!(s >> str))
00413 return false;
00414 if (!(s >> ncols))
00415 return false;
00416 resize_no_copy(nrows, ncols);
00417
00418 Congruence_System& x = *this;
00419 for (dimension_type i = 0; i < x.num_rows(); ++i)
00420 x[i].ascii_load(s);
00421
00422
00423 assert(OK());
00424 return true;
00425 }
00426
00427 bool
00428 PPL::Congruence_System::OK() const {
00429
00430 if (!Matrix::OK())
00431 return false;
00432
00433 if (num_rows()) {
00434 if (num_columns() < 2) {
00435 #ifndef NDEBUG
00436 std::cerr << "Congruence_System has rows and fewer than two columns."
00437 << std::endl;
00438 #endif
00439 return false;
00440 }
00441 }
00442
00443
00444 const Congruence_System& x = *this;
00445 for (dimension_type i = num_rows(); i-- > 0; ) {
00446 const Congruence& cg = x[i];
00447 if (!cg.OK())
00448 return false;
00449 }
00450
00451
00452 return true;
00453 }
00454
00456 std::ostream&
00457 PPL::IO_Operators::operator<<(std::ostream& s, const Congruence_System& cgs) {
00458 Congruence_System::const_iterator i = cgs.begin();
00459 const Congruence_System::const_iterator cgs_end = cgs.end();
00460 if (i == cgs_end)
00461 return s << "true";
00462 while (true) {
00463 Congruence cg = *i++;
00464 cg.strong_normalize();
00465 s << cg;
00466 if (i == cgs_end)
00467 return s;
00468 s << ", ";
00469 }
00470 }
00471
00473 bool
00474 PPL::operator==(const Congruence_System& x, const Congruence_System& y) {
00475 if (x.num_columns() == y.num_columns()) {
00476 dimension_type num_rows = x.num_rows();
00477 if (num_rows == y.num_rows()) {
00478 while (num_rows--) {
00479 if (x[num_rows] == y[num_rows])
00480 continue;
00481 return false;
00482 }
00483 return true;
00484 }
00485 }
00486 return false;
00487 }
00488
00489 void
00490 PPL::Congruence_System::add_unit_rows_and_columns(dimension_type dims) {
00491 assert(num_columns() > 0);
00492 dimension_type col = num_columns() - 1;
00493 dimension_type old_num_rows = num_rows();
00494 add_zero_rows_and_columns(dims, dims,
00495 Linear_Row::Flags(NECESSARILY_CLOSED,
00496 Linear_Row::LINE_OR_EQUALITY));
00497
00498 swap_columns(col, col + dims);
00499
00500
00501 for (dimension_type row = old_num_rows; row-- > 0; )
00502 std::swap(operator[](row), operator[](row + dims));
00503
00504 col += dims - 1;
00505
00506 for (dimension_type row = 0; row < dims; ++row)
00507 const_cast<Coefficient&>(operator[](row)[col - row]) = 1;
00508 }
00509
00510 void
00511 PPL::Congruence_System::concatenate(const Congruence_System& const_cgs) {
00512
00513 Congruence_System cgs = const_cgs;
00514
00515 dimension_type added_rows = cgs.num_rows();
00516 dimension_type added_columns = cgs.space_dimension();
00517
00518 if (added_rows == 0) {
00519 increase_space_dimension(space_dimension() + added_columns);
00520 return;
00521 }
00522
00523 dimension_type old_num_rows = num_rows();
00524 dimension_type old_modi = num_columns() - 1;
00525 dimension_type old_space_dim = space_dimension();
00526
00527 add_zero_rows_and_columns(added_rows, added_columns,
00528 Row::Flags());
00529
00530 dimension_type cgs_num_columns = cgs.num_columns();
00531 dimension_type modi = num_columns() - 1;
00532
00533
00534 for (dimension_type i = 0; i < old_num_rows; ++i) {
00535 Congruence& cg = operator[](i);
00536 std::swap(cg[old_modi], cg[modi]);
00537 }
00538
00539
00540
00541 for (dimension_type i = added_rows; i-- > 0; ) {
00542 Congruence& cg_old = cgs[i];
00543 Congruence& cg_new = operator[](old_num_rows + i);
00544
00545 std::swap(cg_new[0], cg_old[0]);
00546
00547 for (dimension_type j = 1; j < cgs_num_columns; ++j)
00548 std::swap(cg_old[j], cg_new[old_space_dim + j]);
00549 }
00550 }