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_System.defs.hh"
00026 #include "Constraint_System.inlines.hh"
00027 #include "Generator.defs.hh"
00028 #include "Scalar_Products.defs.hh"
00029 #include "Congruence_System.defs.hh"
00030 #include "Congruence_System.inlines.hh"
00031 #include <cassert>
00032 #include <string>
00033 #include <vector>
00034 #include <iostream>
00035 #include <stdexcept>
00036
00037 namespace PPL = Parma_Polyhedra_Library;
00038
00039 PPL::Constraint_System::Constraint_System(const Congruence_System& cgs)
00040 : Linear_System(NECESSARILY_CLOSED, 0, cgs.space_dimension() + 1) {
00041 for (Congruence_System::const_iterator i = cgs.begin(),
00042 cgs_end = cgs.end(); i != cgs_end; ++i)
00043 if (i->is_equality())
00044
00045 insert(Constraint(*i));
00046 }
00047
00048 bool
00049 PPL::Constraint_System::
00050 adjust_topology_and_space_dimension(const Topology new_topology,
00051 const dimension_type new_space_dim) {
00052 assert(space_dimension() <= new_space_dim);
00053
00054 const dimension_type old_space_dim = space_dimension();
00055 const Topology old_topology = topology();
00056 dimension_type cols_to_be_added = new_space_dim - old_space_dim;
00057
00058
00059 if (num_rows() == 0) {
00060 if (num_columns() == 0)
00061 if (new_topology == NECESSARILY_CLOSED) {
00062 add_zero_columns(++cols_to_be_added);
00063 set_necessarily_closed();
00064 }
00065 else {
00066 cols_to_be_added += 2;
00067 add_zero_columns(cols_to_be_added);
00068 set_not_necessarily_closed();
00069 }
00070 else
00071
00072 if (old_topology != new_topology)
00073 if (new_topology == NECESSARILY_CLOSED) {
00074 switch (cols_to_be_added) {
00075 case 0:
00076 remove_trailing_columns(1);
00077 break;
00078 case 1:
00079
00080 break;
00081 default:
00082 add_zero_columns(--cols_to_be_added);
00083 }
00084 set_necessarily_closed();
00085 }
00086 else {
00087
00088
00089 add_zero_columns(++cols_to_be_added);
00090 set_not_necessarily_closed();
00091 }
00092 else {
00093
00094 if (cols_to_be_added > 0)
00095 add_zero_columns(cols_to_be_added);
00096 }
00097 assert(OK());
00098 return true;
00099 }
00100
00101
00102 if (cols_to_be_added > 0)
00103 if (old_topology != new_topology)
00104 if (new_topology == NECESSARILY_CLOSED) {
00105
00106
00107
00108 if (has_strict_inequalities())
00109 return false;
00110
00111
00112
00113
00114
00115
00116 Constraint_System& cs = *this;
00117 const dimension_type eps_index = old_space_dim + 1;
00118 dimension_type cs_num_rows = cs.num_rows();
00119 bool was_sorted = cs.is_sorted();
00120 if (was_sorted)
00121 cs.set_sorted(false);
00122
00123
00124
00125 if (cs.num_pending_rows() == 0) {
00126 for (dimension_type i = cs_num_rows; i-- > 0; )
00127 if (cs[i][eps_index] != 0) {
00128 --cs_num_rows;
00129 std::swap(cs[i], cs[cs_num_rows]);
00130 }
00131 cs.erase_to_end(cs_num_rows);
00132 cs.unset_pending_rows();
00133 }
00134 else {
00135
00136
00137
00138
00139 const dimension_type old_first_pending = cs.first_pending_row();
00140 dimension_type new_first_pending = old_first_pending;
00141 for (dimension_type i = new_first_pending; i-- > 0; )
00142 if (cs[i][eps_index] != 0) {
00143 --new_first_pending;
00144 std::swap(cs[i], cs[new_first_pending]);
00145 }
00146 const dimension_type num_swaps
00147 = old_first_pending - new_first_pending;
00148 cs.set_index_first_pending_row(new_first_pending);
00149
00150 for (dimension_type i = num_swaps; i-- > 0; )
00151 std::swap(cs[old_first_pending - i], cs[cs_num_rows - i]);
00152 cs_num_rows -= num_swaps;
00153
00154 for (dimension_type i = cs_num_rows; i-- > new_first_pending; )
00155 if (cs[i][eps_index] != 0) {
00156 --cs_num_rows;
00157 std::swap(cs[i], cs[cs_num_rows]);
00158 }
00159 cs.erase_to_end(cs_num_rows);
00160 }
00161
00162
00163 if (was_sorted)
00164 cs.sort_rows();
00165 if (--cols_to_be_added > 0)
00166 add_zero_columns(cols_to_be_added);
00167 set_necessarily_closed();
00168 }
00169 else {
00170
00171
00172
00173 add_zero_columns(++cols_to_be_added);
00174 set_not_necessarily_closed();
00175 }
00176 else {
00177
00178 add_zero_columns(cols_to_be_added);
00179
00180
00181 if (old_topology == NOT_NECESSARILY_CLOSED)
00182 swap_columns(old_space_dim + 1, new_space_dim + 1);
00183 }
00184 else
00185
00186 if (old_topology != new_topology) {
00187 if (new_topology == NECESSARILY_CLOSED) {
00188
00189
00190
00191 if (has_strict_inequalities())
00192 return false;
00193
00194 remove_trailing_columns(1);
00195 set_necessarily_closed();
00196 }
00197 else {
00198
00199 add_zero_columns(1);
00200 set_not_necessarily_closed();
00201 }
00202 }
00203
00204 assert(OK());
00205 return true;
00206 }
00207
00208 bool
00209 PPL::Constraint_System::has_strict_inequalities() const {
00210 if (is_necessarily_closed())
00211 return false;
00212 const Constraint_System& cs = *this;
00213 const dimension_type eps_index = cs.num_columns() - 1;
00214
00215
00216 for (dimension_type i = cs.num_rows(); i-- > 0; ) {
00217 const Constraint& c = cs[i];
00218
00219
00220
00221
00222 if (c[eps_index] < 0 && !c.is_tautological())
00223 return true;
00224 }
00225 return false;
00226 }
00227
00228 void
00229 PPL::Constraint_System::insert(const Constraint& c) {
00230
00231
00232 assert(num_pending_rows() == 0);
00233 if (topology() == c.topology())
00234 Linear_System::insert(c);
00235 else
00236
00237 if (is_necessarily_closed()) {
00238
00239
00240 add_zero_columns(1);
00241 set_not_necessarily_closed();
00242 Linear_System::insert(c);
00243 }
00244 else {
00245
00246
00247
00248
00249
00250 const dimension_type new_size = 2 + std::max(c.space_dimension(),
00251 space_dimension());
00252 Constraint tmp_c(c, new_size);
00253 tmp_c.set_not_necessarily_closed();
00254 Linear_System::insert(tmp_c);
00255 }
00256 assert(OK());
00257 }
00258
00259 void
00260 PPL::Constraint_System::insert_pending(const Constraint& c) {
00261 if (topology() == c.topology())
00262 Linear_System::insert_pending(c);
00263 else
00264
00265 if (is_necessarily_closed()) {
00266
00267
00268 add_zero_columns(1);
00269 set_not_necessarily_closed();
00270 Linear_System::insert_pending(c);
00271 }
00272 else {
00273
00274
00275
00276 const dimension_type new_size = 2 + std::max(c.space_dimension(),
00277 space_dimension());
00278 Constraint tmp_c(c, new_size);
00279 tmp_c.set_not_necessarily_closed();
00280 Linear_System::insert_pending(tmp_c);
00281 }
00282 assert(OK());
00283 }
00284
00285 PPL::dimension_type
00286 PPL::Constraint_System::num_inequalities() const {
00287
00288
00289 assert(num_pending_rows() == 0);
00290 const Constraint_System& cs = *this;
00291 dimension_type n = 0;
00292
00293
00294 if (is_sorted())
00295 for (dimension_type i = num_rows(); i > 0 && cs[--i].is_inequality(); )
00296 ++n;
00297 else
00298 for (dimension_type i = num_rows(); i-- > 0 ; )
00299 if (cs[i].is_inequality())
00300 ++n;
00301 return n;
00302 }
00303
00304 PPL::dimension_type
00305 PPL::Constraint_System::num_equalities() const {
00306
00307
00308 assert(num_pending_rows() == 0);
00309 return num_rows() - num_inequalities();
00310 }
00311
00312 void
00313 PPL::Constraint_System::const_iterator::skip_forward() {
00314 const Linear_System::const_iterator csp_end = csp->end();
00315 while (i != csp_end && (*this)->is_tautological())
00316 ++i;
00317 }
00318
00319 bool
00320 PPL::Constraint_System::satisfies_all_constraints(const Generator& g) const {
00321 assert(g.space_dimension() <= space_dimension());
00322
00323
00324
00325
00326 Topology_Adjusted_Scalar_Product_Sign sps(g);
00327
00328 const Constraint_System& cs = *this;
00329 if (cs.is_necessarily_closed()) {
00330 if (g.is_line()) {
00331
00332 for (dimension_type i = cs.num_rows(); i-- > 0; )
00333 if (sps(g, cs[i]) != 0)
00334 return false;
00335 }
00336 else
00337
00338 for (dimension_type i = cs.num_rows(); i-- > 0; ) {
00339 const Constraint& c = cs[i];
00340 const int sp_sign = sps(g, c);
00341 if (c.is_inequality()) {
00342
00343
00344 if (sp_sign < 0)
00345 return false;
00346 }
00347 else
00348
00349 if (sp_sign != 0)
00350 return false;
00351 }
00352 }
00353 else
00354
00355 switch (g.type()) {
00356
00357 case Generator::LINE:
00358
00359 for (dimension_type i = cs.num_rows(); i-- > 0; )
00360 if (sps(g, cs[i]) != 0)
00361 return false;
00362 break;
00363
00364 case Generator::POINT:
00365
00366
00367 for (dimension_type i = cs.num_rows(); i-- > 0; ) {
00368 const Constraint& c = cs[i];
00369 const int sp_sign = sps(g, c);
00370 switch (c.type()) {
00371 case Constraint::EQUALITY:
00372 if (sp_sign != 0)
00373 return false;
00374 break;
00375 case Constraint::NONSTRICT_INEQUALITY:
00376 if (sp_sign < 0)
00377 return false;
00378 break;
00379 case Constraint::STRICT_INEQUALITY:
00380 if (sp_sign <= 0)
00381 return false;
00382 break;
00383 }
00384 }
00385 break;
00386
00387 case Generator::RAY:
00388
00389 case Generator::CLOSURE_POINT:
00390 for (dimension_type i = cs.num_rows(); i-- > 0; ) {
00391 const Constraint& c = cs[i];
00392 const int sp_sign = sps(g, c);
00393 if (c.is_inequality()) {
00394
00395 if (sp_sign < 0)
00396 return false;
00397 }
00398 else
00399
00400 if (sp_sign != 0)
00401 return false;
00402 }
00403 break;
00404 }
00405
00406
00407 return true;
00408 }
00409
00410
00411 void
00412 PPL::Constraint_System
00413 ::affine_preimage(const dimension_type v,
00414 const Linear_Expression& expr,
00415 Coefficient_traits::const_reference denominator) {
00416 Constraint_System& x = *this;
00417
00418
00419
00420 assert(v > 0 && v <= x.space_dimension());
00421 assert(expr.space_dimension() <= x.space_dimension());
00422 assert(denominator > 0);
00423
00424 const dimension_type n_columns = x.num_columns();
00425 const dimension_type n_rows = x.num_rows();
00426 const dimension_type expr_size = expr.size();
00427 const bool not_invertible = (v >= expr_size || expr[v] == 0);
00428
00429 if (denominator != 1)
00430 for (dimension_type i = n_rows; i-- > 0; ) {
00431 Constraint& row = x[i];
00432 Coefficient& row_v = row[v];
00433 if (row_v != 0) {
00434 for (dimension_type j = n_columns; j-- > 0; )
00435 if (j != v) {
00436 Coefficient& row_j = row[j];
00437 row_j *= denominator;
00438 if (j < expr_size)
00439 add_mul_assign(row_j, row_v, expr[j]);
00440 }
00441 if (not_invertible)
00442 row_v = 0;
00443 else
00444 row_v *= expr[v];
00445 }
00446 }
00447 else
00448
00449
00450 for (dimension_type i = n_rows; i-- > 0; ) {
00451 Constraint& row = x[i];
00452 Coefficient& row_v = row[v];
00453 if (row_v != 0) {
00454 for (dimension_type j = expr_size; j-- > 0; )
00455 if (j != v)
00456 add_mul_assign(row[j], row_v, expr[j]);
00457 if (not_invertible)
00458 row_v = 0;
00459 else
00460 row_v *= expr[v];
00461 }
00462 }
00463
00464 x.strong_normalize();
00465 }
00466
00467 void
00468 PPL::Constraint_System::ascii_dump(std::ostream& s) const {
00469 const Constraint_System& x = *this;
00470 const dimension_type x_num_rows = x.num_rows();
00471 const dimension_type x_num_columns = x.num_columns();
00472 s << "topology " << (is_necessarily_closed()
00473 ? "NECESSARILY_CLOSED"
00474 : "NOT_NECESSARILY_CLOSED")
00475 << "\n"
00476 << x_num_rows << " x " << x_num_columns << ' '
00477 << (x.is_sorted() ? "(sorted)" : "(not_sorted)")
00478 << "\n"
00479 << "index_first_pending " << x.first_pending_row()
00480 << "\n";
00481 for (dimension_type i = 0; i < x_num_rows; ++i) {
00482 const Constraint& c = x[i];
00483 for (dimension_type j = 0; j < x_num_columns; ++j)
00484 s << c[j] << ' ';
00485 switch (c.type()) {
00486 case Constraint::EQUALITY:
00487 s << "=";
00488 break;
00489 case Constraint::NONSTRICT_INEQUALITY:
00490 s << ">=";
00491 break;
00492 case Constraint::STRICT_INEQUALITY:
00493 s << ">";
00494 break;
00495 }
00496 s << "\n";
00497 }
00498 }
00499
00500 PPL_OUTPUT_DEFINITIONS(Constraint_System)
00501
00502 bool
00503 PPL::Constraint_System::ascii_load(std::istream& s) {
00504 std::string str;
00505 if (!(s >> str) || str != "topology")
00506 return false;
00507 if (!(s >> str))
00508 return false;
00509 if (str == "NECESSARILY_CLOSED")
00510 set_necessarily_closed();
00511 else {
00512 if (str != "NOT_NECESSARILY_CLOSED")
00513 return false;
00514 set_not_necessarily_closed();
00515 }
00516
00517 dimension_type nrows;
00518 dimension_type ncols;
00519 if (!(s >> nrows))
00520 return false;
00521 if (!(s >> str))
00522 return false;
00523 if (!(s >> ncols))
00524 return false;
00525 resize_no_copy(nrows, ncols);
00526
00527 if (!(s >> str) || (str != "(sorted)" && str != "(not_sorted)"))
00528 return false;
00529 set_sorted(str == "(sorted)");
00530 dimension_type index;
00531 if (!(s >> str) || str != "index_first_pending")
00532 return false;
00533 if (!(s >> index))
00534 return false;
00535 set_index_first_pending_row(index);
00536
00537 Constraint_System& x = *this;
00538 for (dimension_type i = 0; i < x.num_rows(); ++i) {
00539 for (dimension_type j = 0; j < x.num_columns(); ++j)
00540 if (!(s >> x[i][j]))
00541 return false;
00542
00543 if (!(s >> str))
00544 return false;
00545 if (str == "=")
00546 x[i].set_is_equality();
00547 else
00548 x[i].set_is_inequality();
00549
00550
00551 switch (x[i].type()) {
00552 case Constraint::EQUALITY:
00553 if (str == "=")
00554 continue;
00555 break;
00556 case Constraint::NONSTRICT_INEQUALITY:
00557 if (str == ">=")
00558 continue;
00559 break;
00560 case Constraint::STRICT_INEQUALITY:
00561 if (str == ">")
00562 continue;
00563 break;
00564 }
00565
00566 return false;
00567 }
00568
00569 assert(OK());
00570 return true;
00571 }
00572
00573 const PPL::Constraint_System* PPL::Constraint_System::zero_dim_empty_p = 0;
00574
00575 void
00576 PPL::Constraint_System::initialize() {
00577 assert(zero_dim_empty_p == 0);
00578 zero_dim_empty_p
00579 = new Constraint_System(Constraint::zero_dim_false());
00580 }
00581
00582 void
00583 PPL::Constraint_System::finalize() {
00584 assert(zero_dim_empty_p != 0);
00585 delete zero_dim_empty_p;
00586 zero_dim_empty_p = 0;
00587 }
00588
00589 bool
00590 PPL::Constraint_System::OK() const {
00591
00592
00593
00594 if (!Linear_System::OK(false))
00595 return false;
00596
00597
00598 const Constraint_System& x = *this;
00599 for (dimension_type i = num_rows(); i-- > 0; )
00600 if (!x[i].OK())
00601 return false;
00602
00603
00604 return true;
00605 }
00606
00608 std::ostream&
00609 PPL::IO_Operators::operator<<(std::ostream& s, const Constraint_System& cs) {
00610 Constraint_System::const_iterator i = cs.begin();
00611 const Constraint_System::const_iterator cs_end = cs.end();
00612 if (i == cs_end)
00613 s << "true";
00614 else {
00615 while (i != cs_end) {
00616 s << *i++;
00617 if (i != cs_end)
00618 s << ", ";
00619 }
00620 }
00621 return s;
00622 }