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