00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023 #ifndef PPL_Pointset_Powerset_templates_hh
00024 #define PPL_Pointset_Powerset_templates_hh 1
00025
00026 #include "Constraint.defs.hh"
00027 #include "Constraint_System.defs.hh"
00028 #include "Constraint_System.inlines.hh"
00029 #include "C_Polyhedron.defs.hh"
00030 #include "NNC_Polyhedron.defs.hh"
00031 #include "Variables_Set.defs.hh"
00032 #include <algorithm>
00033 #include <deque>
00034 #include <string>
00035 #include <iostream>
00036 #include <sstream>
00037 #include <stdexcept>
00038
00039 namespace Parma_Polyhedra_Library {
00040
00041 template <typename PS>
00042 void
00043 Pointset_Powerset<PS>::add_disjunct(const PS& ph) {
00044 Pointset_Powerset& x = *this;
00045 if (x.space_dimension() != ph.space_dimension()) {
00046 std::ostringstream s;
00047 s << "PPL::Pointset_Powerset<PS>::add_disjunct(ph):\n"
00048 << "this->space_dimension() == " << x.space_dimension() << ", "
00049 << "ph.space_dimension() == " << ph.space_dimension() << ".";
00050 throw std::invalid_argument(s.str());
00051 }
00052 x.sequence.push_back(Determinate<PS>(ph));
00053 x.reduced = false;
00054 assert(x.OK());
00055 }
00056
00057 template <>
00058 template <typename QH>
00059 Pointset_Powerset<NNC_Polyhedron>
00060 ::Pointset_Powerset(const Pointset_Powerset<QH>& y,
00061 Complexity_Class complexity)
00062 : Base(), space_dim(y.space_dimension()) {
00063 Pointset_Powerset& x = *this;
00064 for (typename Pointset_Powerset<QH>::const_iterator i = y.begin(),
00065 y_end = y.end(); i != y_end; ++i)
00066 x.sequence.push_back(Determinate<NNC_Polyhedron>
00067 (NNC_Polyhedron(i->element(), complexity)));
00068
00069 x.reduced = y.reduced;
00070 assert(x.OK());
00071 }
00072
00073 template <typename PS>
00074 template <typename QH>
00075 Pointset_Powerset<PS>
00076 ::Pointset_Powerset(const Pointset_Powerset<QH>& y,
00077 Complexity_Class complexity)
00078 : Base(), space_dim(y.space_dimension()) {
00079 Pointset_Powerset& x = *this;
00080 for (typename Pointset_Powerset<QH>::const_iterator i = y.begin(),
00081 y_end = y.end(); i != y_end; ++i)
00082 x.sequence.push_back(Determinate<PS>(PS(i->element(), complexity)));
00083
00084
00085
00086 x.reduced = false;
00087 assert(x.OK());
00088 }
00089
00090 template <typename PS>
00091 void
00092 Pointset_Powerset<PS>::concatenate_assign(const Pointset_Powerset& y) {
00093 Pointset_Powerset& x = *this;
00094
00095 x.omega_reduce();
00096 y.omega_reduce();
00097 Pointset_Powerset<PS> new_x(x.space_dim + y.space_dim, EMPTY);
00098 for (const_iterator xi = x.begin(), x_end = x.end(),
00099 y_begin = y.begin(), y_end = y.end(); xi != x_end; ) {
00100 for (const_iterator yi = y_begin; yi != y_end; ++yi) {
00101 CS zi = *xi;
00102 zi.concatenate_assign(*yi);
00103 assert(!zi.is_bottom());
00104 new_x.sequence.push_back(zi);
00105 }
00106 ++xi;
00107 if (abandon_expensive_computations && xi != x_end && y_begin != y_end) {
00108
00109 PS xph = xi->element();
00110 for (++xi; xi != x_end; ++xi)
00111 xph.upper_bound_assign(xi->element());
00112 const_iterator yi = y_begin;
00113 PS yph = yi->element();
00114 for (++yi; yi != y_end; ++yi)
00115 yph.upper_bound_assign(yi->element());
00116 xph.concatenate_assign(yph);
00117 x.swap(new_x);
00118 x.add_disjunct(xph);
00119 assert(x.OK());
00120 return;
00121 }
00122 }
00123 x.swap(new_x);
00124 assert(x.OK());
00125 }
00126
00127 template <typename PS>
00128 void
00129 Pointset_Powerset<PS>::add_constraint(const Constraint& c) {
00130 Pointset_Powerset& x = *this;
00131 for (Sequence_iterator si = x.sequence.begin(),
00132 s_end = x.sequence.end(); si != s_end; ++si)
00133 si->element().add_constraint(c);
00134 x.reduced = false;
00135 assert(x.OK());
00136 }
00137
00138 template <typename PS>
00139 bool
00140 Pointset_Powerset<PS>::add_constraint_and_minimize(const Constraint& c) {
00141 Pointset_Powerset& x = *this;
00142 for (Sequence_iterator si = x.sequence.begin(),
00143 s_end = x.sequence.end(); si != s_end; )
00144 if (!si->element().add_constraint_and_minimize(c))
00145 si = x.sequence.erase(si);
00146 else {
00147 x.reduced = false;
00148 ++si;
00149 }
00150 assert(x.OK());
00151 return !x.empty();
00152 }
00153
00154 template <typename PS>
00155 void
00156 Pointset_Powerset<PS>::refine_with_constraint(const Constraint& c) {
00157 Pointset_Powerset& x = *this;
00158 for (Sequence_iterator si = x.sequence.begin(),
00159 s_end = x.sequence.end(); si != s_end; ++si)
00160 si->element().refine_with_constraint(c);
00161 x.reduced = false;
00162 assert(x.OK());
00163 }
00164
00165 template <typename PS>
00166 void
00167 Pointset_Powerset<PS>::add_constraints(const Constraint_System& cs) {
00168 Pointset_Powerset& x = *this;
00169 for (Sequence_iterator si = x.sequence.begin(),
00170 s_end = x.sequence.end(); si != s_end; ++si)
00171 si->element().add_constraints(cs);
00172 x.reduced = false;
00173 assert(x.OK());
00174 }
00175
00176 template <typename PS>
00177 bool
00178 Pointset_Powerset<PS>::
00179 add_constraints_and_minimize(const Constraint_System& cs) {
00180 Pointset_Powerset& x = *this;
00181 for (Sequence_iterator si = x.sequence.begin(),
00182 s_end = x.sequence.end(); si != s_end; )
00183 if (!si->element().add_constraints_and_minimize(cs))
00184 si = x.sequence.erase(si);
00185 else {
00186 x.reduced = false;
00187 ++si;
00188 }
00189 assert(x.OK());
00190 return !x.empty();
00191 }
00192
00193 template <typename PS>
00194 void
00195 Pointset_Powerset<PS>::refine_with_constraints(const Constraint_System& cs) {
00196 Pointset_Powerset& x = *this;
00197 for (Sequence_iterator si = x.sequence.begin(),
00198 s_end = x.sequence.end(); si != s_end; ++si)
00199 si->element().refine_with_constraints(cs);
00200 x.reduced = false;
00201 assert(x.OK());
00202 }
00203
00204 template <typename PS>
00205 void
00206 Pointset_Powerset<PS>::add_congruence(const Congruence& c) {
00207 Pointset_Powerset& x = *this;
00208 for (Sequence_iterator si = x.sequence.begin(),
00209 s_end = x.sequence.end(); si != s_end; ++si)
00210 si->element().add_congruence(c);
00211 x.reduced = false;
00212 assert(x.OK());
00213 }
00214
00215 template <typename PS>
00216 void
00217 Pointset_Powerset<PS>::refine_with_congruence(const Congruence& cg) {
00218 Pointset_Powerset& x = *this;
00219 for (Sequence_iterator si = x.sequence.begin(),
00220 s_end = x.sequence.end(); si != s_end; ++si)
00221 si->element().refine_with_congruence(cg);
00222 x.reduced = false;
00223 assert(x.OK());
00224 }
00225
00226 template <typename PS>
00227 bool
00228 Pointset_Powerset<PS>::add_congruence_and_minimize(const Congruence& c) {
00229 Pointset_Powerset& x = *this;
00230 for (Sequence_iterator si = x.sequence.begin(),
00231 s_end = x.sequence.end(); si != s_end; )
00232 if (!si->element().add_congruence_and_minimize(c))
00233 si = x.sequence.erase(si);
00234 else {
00235 x.reduced = false;
00236 ++si;
00237 }
00238 assert(x.OK());
00239 return !x.empty();
00240 }
00241
00242 template <typename PS>
00243 void
00244 Pointset_Powerset<PS>::add_congruences(const Congruence_System& cs) {
00245 Pointset_Powerset& x = *this;
00246 for (Sequence_iterator si = x.sequence.begin(),
00247 s_end = x.sequence.end(); si != s_end; ++si)
00248 si->element().add_congruences(cs);
00249 x.reduced = false;
00250 assert(x.OK());
00251 }
00252
00253 template <typename PS>
00254 void
00255 Pointset_Powerset<PS>::refine_with_congruences(const Congruence_System& cgs) {
00256 Pointset_Powerset& x = *this;
00257 for (Sequence_iterator si = x.sequence.begin(),
00258 s_end = x.sequence.end(); si != s_end; ++si)
00259 si->element().refine_with_congruences(cgs);
00260 x.reduced = false;
00261 assert(x.OK());
00262 }
00263
00264 template <typename PS>
00265 bool
00266 Pointset_Powerset<PS>::
00267 add_congruences_and_minimize(const Congruence_System& cs) {
00268 Pointset_Powerset& x = *this;
00269 for (Sequence_iterator si = x.sequence.begin(),
00270 s_end = x.sequence.end(); si != s_end; )
00271 if (!si->element().add_congruences_and_minimize(cs))
00272 si = x.sequence.erase(si);
00273 else {
00274 x.reduced = false;
00275 ++si;
00276 }
00277 assert(x.OK());
00278 return !x.empty();
00279 }
00280
00281 template <typename PS>
00282 void
00283 Pointset_Powerset<PS>::unconstrain(const Variable var) {
00284 Pointset_Powerset& x = *this;
00285 for (Sequence_iterator si = x.sequence.begin(),
00286 s_end = x.sequence.end(); si != s_end; ++si) {
00287 si->element().unconstrain(var);
00288 x.reduced = false;
00289 }
00290 assert(x.OK());
00291 }
00292
00293 template <typename PS>
00294 void
00295 Pointset_Powerset<PS>::unconstrain(const Variables_Set& to_be_unconstrained) {
00296 Pointset_Powerset& x = *this;
00297 for (Sequence_iterator si = x.sequence.begin(),
00298 s_end = x.sequence.end(); si != s_end; ++si) {
00299 si->element().unconstrain(to_be_unconstrained);
00300 x.reduced = false;
00301 }
00302 assert(x.OK());
00303 }
00304
00305 template <typename PS>
00306 void
00307 Pointset_Powerset<PS>::add_space_dimensions_and_embed(dimension_type m) {
00308 Pointset_Powerset& x = *this;
00309 for (Sequence_iterator si = x.sequence.begin(),
00310 s_end = x.sequence.end(); si != s_end; ++si)
00311 si->element().add_space_dimensions_and_embed(m);
00312 x.space_dim += m;
00313 assert(x.OK());
00314 }
00315
00316 template <typename PS>
00317 void
00318 Pointset_Powerset<PS>::add_space_dimensions_and_project(dimension_type m) {
00319 Pointset_Powerset& x = *this;
00320 for (Sequence_iterator si = x.sequence.begin(),
00321 s_end = x.sequence.end(); si != s_end; ++si)
00322 si->element().add_space_dimensions_and_project(m);
00323 x.space_dim += m;
00324 assert(x.OK());
00325 }
00326
00327 template <typename PS>
00328 void
00329 Pointset_Powerset<PS>::
00330 remove_space_dimensions(const Variables_Set& to_be_removed) {
00331 Pointset_Powerset& x = *this;
00332 Variables_Set::size_type num_removed = to_be_removed.size();
00333 if (num_removed > 0) {
00334 for (Sequence_iterator si = x.sequence.begin(),
00335 s_end = x.sequence.end(); si != s_end; ++si) {
00336 si->element().remove_space_dimensions(to_be_removed);
00337 x.reduced = false;
00338 }
00339 x.space_dim -= num_removed;
00340 assert(x.OK());
00341 }
00342 }
00343
00344 template <typename PS>
00345 void
00346 Pointset_Powerset<PS>::remove_higher_space_dimensions(dimension_type
00347 new_dimension) {
00348 Pointset_Powerset& x = *this;
00349 if (new_dimension < x.space_dim) {
00350 for (Sequence_iterator si = x.sequence.begin(),
00351 s_end = x.sequence.end(); si != s_end; ++si) {
00352 si->element().remove_higher_space_dimensions(new_dimension);
00353 x.reduced = false;
00354 }
00355 x.space_dim = new_dimension;
00356 assert(x.OK());
00357 }
00358 }
00359
00360 template <typename PS>
00361 template <typename Partial_Function>
00362 void
00363 Pointset_Powerset<PS>::map_space_dimensions(const Partial_Function& pfunc) {
00364 Pointset_Powerset& x = *this;
00365 if (x.is_bottom()) {
00366 dimension_type n = 0;
00367 for (dimension_type i = x.space_dim; i-- > 0; ) {
00368 dimension_type new_i;
00369 if (pfunc.maps(i, new_i))
00370 ++n;
00371 }
00372 x.space_dim = n;
00373 }
00374 else {
00375 Sequence_iterator s_begin = x.sequence.begin();
00376 for (Sequence_iterator si = s_begin,
00377 s_end = x.sequence.end(); si != s_end; ++si)
00378 si->element().map_space_dimensions(pfunc);
00379 x.space_dim = s_begin->element().space_dimension();
00380 x.reduced = false;
00381 }
00382 assert(x.OK());
00383 }
00384
00385 template <typename PS>
00386 void
00387 Pointset_Powerset<PS>::expand_space_dimension(Variable var,
00388 dimension_type m) {
00389 Pointset_Powerset& x = *this;
00390 for (Sequence_iterator si = x.sequence.begin(),
00391 s_end = x.sequence.end(); si != s_end; ++si)
00392 si->element().expand_space_dimension(var, m);
00393 x.space_dim += m;
00394 assert(x.OK());
00395 }
00396
00397 template <typename PS>
00398 void
00399 Pointset_Powerset<PS>::fold_space_dimensions(const Variables_Set& to_be_folded,
00400 Variable var) {
00401 Pointset_Powerset& x = *this;
00402 Variables_Set::size_type num_folded = to_be_folded.size();
00403 if (num_folded > 0) {
00404 for (Sequence_iterator si = x.sequence.begin(),
00405 s_end = x.sequence.end(); si != s_end; ++si)
00406 si->element().fold_space_dimensions(to_be_folded, var);
00407 }
00408 x.space_dim -= num_folded;
00409 assert(x.OK());
00410 }
00411
00412 template <typename PS>
00413 void
00414 Pointset_Powerset<PS>::affine_image(Variable var,
00415 const Linear_Expression& expr,
00416 Coefficient_traits::const_reference
00417 denominator) {
00418 Pointset_Powerset& x = *this;
00419 for (Sequence_iterator si = x.sequence.begin(),
00420 s_end = x.sequence.end(); si != s_end; ++si) {
00421 si->element().affine_image(var, expr, denominator);
00422
00423
00424
00425 x.reduced = false;
00426 }
00427 assert(x.OK());
00428 }
00429
00430 template <typename PS>
00431 void
00432 Pointset_Powerset<PS>::affine_preimage(Variable var,
00433 const Linear_Expression& expr,
00434 Coefficient_traits::const_reference
00435 denominator) {
00436 Pointset_Powerset& x = *this;
00437 for (Sequence_iterator si = x.sequence.begin(),
00438 s_end = x.sequence.end(); si != s_end; ++si) {
00439 si->element().affine_preimage(var, expr, denominator);
00440
00441
00442
00443 x.reduced = false;
00444 }
00445 assert(x.OK());
00446 }
00447
00448
00449 template <typename PS>
00450 void
00451 Pointset_Powerset<PS>
00452 ::generalized_affine_image(const Linear_Expression& lhs,
00453 const Relation_Symbol relsym,
00454 const Linear_Expression& rhs) {
00455 Pointset_Powerset& x = *this;
00456 for (Sequence_iterator si = x.sequence.begin(),
00457 s_end = x.sequence.end(); si != s_end; ++si) {
00458 si->element().generalized_affine_image(lhs, relsym, rhs);
00459 x.reduced = false;
00460 }
00461 assert(x.OK());
00462 }
00463
00464 template <typename PS>
00465 void
00466 Pointset_Powerset<PS>
00467 ::generalized_affine_preimage(const Linear_Expression& lhs,
00468 const Relation_Symbol relsym,
00469 const Linear_Expression& rhs) {
00470 Pointset_Powerset& x = *this;
00471 for (Sequence_iterator si = x.sequence.begin(),
00472 s_end = x.sequence.end(); si != s_end; ++si) {
00473 si->element().generalized_affine_preimage(lhs, relsym, rhs);
00474 x.reduced = false;
00475 }
00476 assert(x.OK());
00477 }
00478
00479 template <typename PS>
00480 void
00481 Pointset_Powerset<PS>
00482 ::generalized_affine_image(Variable var,
00483 const Relation_Symbol relsym,
00484 const Linear_Expression& expr,
00485 Coefficient_traits::const_reference denominator) {
00486 Pointset_Powerset& x = *this;
00487 for (Sequence_iterator si = x.sequence.begin(),
00488 s_end = x.sequence.end(); si != s_end; ++si) {
00489 si->element().generalized_affine_image(var, relsym, expr, denominator);
00490 x.reduced = false;
00491 }
00492 assert(x.OK());
00493 }
00494
00495 template <typename PS>
00496 void
00497 Pointset_Powerset<PS>
00498 ::generalized_affine_preimage(Variable var,
00499 const Relation_Symbol relsym,
00500 const Linear_Expression& expr,
00501 Coefficient_traits::const_reference denominator) { Pointset_Powerset& x = *this;
00502 for (Sequence_iterator si = x.sequence.begin(),
00503 s_end = x.sequence.end(); si != s_end; ++si) {
00504 si->element().generalized_affine_preimage(var, relsym, expr, denominator);
00505 x.reduced = false;
00506 }
00507 assert(x.OK());
00508 }
00509
00510
00511 template <typename PS>
00512 void
00513 Pointset_Powerset<PS>
00514 ::bounded_affine_image(Variable var,
00515 const Linear_Expression& lb_expr,
00516 const Linear_Expression& ub_expr,
00517 Coefficient_traits::const_reference denominator) {
00518 Pointset_Powerset& x = *this;
00519 for (Sequence_iterator si = x.sequence.begin(),
00520 s_end = x.sequence.end(); si != s_end; ++si) {
00521 si->element().bounded_affine_image(var, lb_expr, ub_expr, denominator);
00522 x.reduced = false;
00523 }
00524 assert(x.OK());
00525 }
00526
00527 template <typename PS>
00528 void
00529 Pointset_Powerset<PS>
00530 ::bounded_affine_preimage(Variable var,
00531 const Linear_Expression& lb_expr,
00532 const Linear_Expression& ub_expr,
00533 Coefficient_traits::const_reference denominator) {
00534 Pointset_Powerset& x = *this;
00535 for (Sequence_iterator si = x.sequence.begin(),
00536 s_end = x.sequence.end(); si != s_end; ++si) {
00537 si->element().bounded_affine_preimage(var, lb_expr, ub_expr,
00538 denominator);
00539 x.reduced = false;
00540 }
00541 assert(x.OK());
00542 }
00543
00544 template <typename PS>
00545 dimension_type
00546 Pointset_Powerset<PS>::affine_dimension() const {
00547
00548
00549 const Pointset_Powerset& x = *this;
00550 C_Polyhedron x_ph(space_dim, EMPTY);
00551
00552 for (Sequence_const_iterator si = x.sequence.begin(),
00553 s_end = x.sequence.end(); si != s_end; ++si) {
00554 PS pi(si->element());
00555 if (!pi.is_empty()) {
00556 C_Polyhedron phi(space_dim);
00557 const Constraint_System& cs = pi.minimized_constraints();
00558 for (Constraint_System::const_iterator i = cs.begin(),
00559 cs_end = cs.end(); i != cs_end; ++i) {
00560 const Constraint& c = *i;
00561 if (c.is_equality())
00562 phi.add_constraint(c);
00563 }
00564 x_ph.poly_hull_assign(phi);
00565 }
00566 }
00567
00568 return x_ph.affine_dimension();
00569 }
00570
00571 template <typename PS>
00572 bool
00573 Pointset_Powerset<PS>::is_universe() const {
00574 const Pointset_Powerset& x = *this;
00575
00576 if (x.is_omega_reduced())
00577 return x.size() == 1 && x.begin()->element().is_universe();
00578
00579
00580 for (const_iterator x_i = x.begin(), x_end = x.end(); x_i != x_end; ++x_i)
00581 if (x_i->element().is_universe()) {
00582
00583 if (x.size() > 1) {
00584 Pointset_Powerset<PS> universe(x.space_dimension(), UNIVERSE);
00585 Pointset_Powerset& xx = const_cast<Pointset_Powerset&>(x);
00586 xx.swap(universe);
00587 }
00588 return true;
00589 }
00590 return false;
00591 }
00592
00593 template <typename PS>
00594 bool
00595 Pointset_Powerset<PS>::is_empty() const {
00596 const Pointset_Powerset& x = *this;
00597 for (Sequence_const_iterator si = x.sequence.begin(),
00598 s_end = x.sequence.end(); si != s_end; ++si)
00599 if (!si->element().is_empty())
00600 return false;
00601 return true;
00602 }
00603
00604 template <typename PS>
00605 bool
00606 Pointset_Powerset<PS>::is_discrete() const {
00607 const Pointset_Powerset& x = *this;
00608 for (Sequence_const_iterator si = x.sequence.begin(),
00609 s_end = x.sequence.end(); si != s_end; ++si)
00610 if (!si->element().is_discrete())
00611 return false;
00612 return true;
00613 }
00614
00615 template <typename PS>
00616 bool
00617 Pointset_Powerset<PS>::is_topologically_closed() const {
00618 const Pointset_Powerset& x = *this;
00619
00620
00621 x.omega_reduce();
00622 for (Sequence_const_iterator si = x.sequence.begin(),
00623 s_end = x.sequence.end(); si != s_end; ++si)
00624 if (!si->element().is_topologically_closed())
00625 return false;
00626 return true;
00627 }
00628
00629 template <typename PS>
00630 bool
00631 Pointset_Powerset<PS>::is_bounded() const {
00632 const Pointset_Powerset& x = *this;
00633 for (Sequence_const_iterator si = x.sequence.begin(),
00634 s_end = x.sequence.end(); si != s_end; ++si)
00635 if (!si->element().is_bounded())
00636 return false;
00637 return true;
00638 }
00639
00640 template <typename PS>
00641 bool
00642 Pointset_Powerset<PS>::constrains(Variable var) const {
00643 const Pointset_Powerset& x = *this;
00644
00645 const dimension_type var_space_dim = var.space_dimension();
00646 if (x.space_dimension() < var_space_dim) {
00647 std::ostringstream s;
00648 s << "PPL::Pointset_Powerset<PS>::constrains(v):\n"
00649 << "this->space_dimension() == " << x.space_dimension() << ", "
00650 << "v.space_dimension() == " << var_space_dim << ".";
00651 throw std::invalid_argument(s.str());
00652 }
00653
00654 x.omega_reduce();
00655
00656 if (x.is_empty())
00657 return true;
00658 for (const_iterator x_i = x.begin(), x_end = x.end(); x_i != x_end; ++x_i)
00659 if (x_i->element().constrains(var))
00660 return true;
00661 return false;
00662 }
00663
00664 template <typename PS>
00665 bool
00666 Pointset_Powerset<PS>::is_disjoint_from(const Pointset_Powerset& y) const {
00667 const Pointset_Powerset& x = *this;
00668 for (Sequence_const_iterator si = x.sequence.begin(),
00669 xs_end = x.sequence.end(); si != xs_end; ++si) {
00670 const PS& pi = si->element();
00671 for (Sequence_const_iterator sj = y.sequence.begin(),
00672 ys_end = y.sequence.end(); sj != ys_end; ++sj) {
00673 const PS& pj = sj->element();
00674 if (!pi.is_disjoint_from(pj))
00675 return false;
00676 }
00677 }
00678 return true;
00679 }
00680
00681 template <typename PS>
00682 void
00683 Pointset_Powerset<PS>::topological_closure_assign() {
00684 Pointset_Powerset& x = *this;
00685 for (Sequence_iterator si = x.sequence.begin(),
00686 s_end = x.sequence.end(); si != s_end; ++si)
00687 si->element().topological_closure_assign();
00688 assert(x.OK());
00689 }
00690
00691 template <typename PS>
00692 bool
00693 Pointset_Powerset<PS>
00694 ::intersection_preserving_enlarge_element(PS& to_be_enlarged) const {
00695
00696 const Pointset_Powerset& context = *this;
00697 assert(context.space_dimension() == to_be_enlarged.space_dimension());
00698 bool nonempty_intersection = false;
00699
00700 PS enlarged(context.space_dimension(), UNIVERSE);
00701 for (Sequence_const_iterator si = context.sequence.begin(),
00702 s_end = context.sequence.end(); si != s_end; ++si) {
00703 PS context_i(si->element());
00704 context_i.intersection_assign(enlarged);
00705 PS enlarged_i(to_be_enlarged);
00706 nonempty_intersection
00707 |= enlarged_i.simplify_using_context_assign(context_i);
00708
00709 enlarged.intersection_assign(enlarged_i);
00710 }
00711 to_be_enlarged.swap(enlarged);
00712 return nonempty_intersection;
00713 }
00714
00715 template <typename PS>
00716 bool
00717 Pointset_Powerset<PS>
00718 ::simplify_using_context_assign(const Pointset_Powerset& y) {
00719 Pointset_Powerset& x = *this;
00720
00721
00722
00723
00724
00725
00726 x.omega_reduce();
00727 if (x.is_empty())
00728 return false;
00729 y.omega_reduce();
00730 if (y.is_empty()) {
00731 x = y;
00732 return false;
00733 }
00734
00735 if (y.size() == 1) {
00736
00737 const PS& y_i = y.sequence.begin()->element();
00738 for (Sequence_iterator si = x.sequence.begin(),
00739 s_end = x.sequence.end(); si != s_end; ) {
00740 PS& x_i = si->element();
00741 if (x_i.simplify_using_context_assign(y_i))
00742 ++si;
00743 else
00744
00745 si = x.sequence.erase(si);
00746 }
00747 }
00748 else {
00749
00750 for (Sequence_iterator si = x.sequence.begin(),
00751 s_end = x.sequence.end(); si != s_end; ) {
00752 if (y.intersection_preserving_enlarge_element(si->element()))
00753 ++si;
00754 else
00755
00756 si = x.sequence.erase(si);
00757 }
00758 }
00759 x.reduced = false;
00760 assert(x.OK());
00761 return !x.sequence.empty();
00762 }
00763
00764 template <typename PS>
00765 bool
00766 Pointset_Powerset<PS>::contains(const Pointset_Powerset& y) const {
00767 const Pointset_Powerset& x = *this;
00768 for (Sequence_const_iterator si = y.sequence.begin(),
00769 ys_end = y.sequence.end(); si != ys_end; ++si) {
00770 const PS& pi = si->element();
00771 bool pi_is_contained = false;
00772 for (Sequence_const_iterator sj = x.sequence.begin(),
00773 xs_end = x.sequence.end();
00774 (sj != xs_end && !pi_is_contained); ++sj) {
00775 const PS& pj = sj->element();
00776 if (pj.contains(pi))
00777 pi_is_contained = true;
00778 }
00779 if (!pi_is_contained)
00780 return false;
00781 }
00782 return true;
00783 }
00784
00785 template <typename PS>
00786 bool
00787 Pointset_Powerset<PS>::strictly_contains(const Pointset_Powerset& y) const {
00788
00789
00790
00791 const Pointset_Powerset& x = *this;
00792 x.omega_reduce();
00793 for (Sequence_const_iterator si = y.sequence.begin(),
00794 ys_end = y.sequence.end(); si != ys_end; ++si) {
00795 const PS& pi = si->element();
00796 bool pi_is_strictly_contained = false;
00797 for (Sequence_const_iterator sj = x.sequence.begin(),
00798 xs_end = x.sequence.end();
00799 (sj != xs_end && !pi_is_strictly_contained); ++sj) {
00800 const PS& pj = sj->element();
00801 if (pj.strictly_contains(pi))
00802 pi_is_strictly_contained = true;
00803 }
00804 if (!pi_is_strictly_contained)
00805 return false;
00806 }
00807 return true;
00808 }
00809
00810 template <typename PS>
00811 Poly_Con_Relation
00812 Pointset_Powerset<PS>::relation_with(const Congruence& cg) const {
00813 const Pointset_Powerset& x = *this;
00814
00815
00816 bool is_included = true;
00817
00818 bool is_disjoint = true;
00819
00820
00821 bool is_strictly_intersecting = false;
00822
00823
00824 bool saturates_once = false;
00825 bool may_saturate = true;
00826 for (Sequence_const_iterator si = x.sequence.begin(),
00827 s_end = x.sequence.end(); si != s_end; ++si) {
00828 Poly_Con_Relation relation_i = si->element().relation_with(cg);
00829 if (!relation_i.implies(Poly_Con_Relation::is_included()))
00830 is_included = false;
00831 if (!relation_i.implies(Poly_Con_Relation::is_disjoint()))
00832 is_disjoint = false;
00833 if (relation_i.implies(Poly_Con_Relation::strictly_intersects()))
00834 is_strictly_intersecting = true;
00835 if (relation_i.implies(Poly_Con_Relation::saturates()))
00836 saturates_once = true;
00837 else if (!relation_i.implies(Poly_Con_Relation::is_disjoint()))
00838 may_saturate = false;
00839 }
00840
00841 Poly_Con_Relation result = Poly_Con_Relation::nothing();
00842 if (is_included)
00843 result = result && Poly_Con_Relation::is_included();
00844 if (is_disjoint)
00845 result = result && Poly_Con_Relation::is_disjoint();
00846 if (is_strictly_intersecting)
00847 result = result && Poly_Con_Relation::strictly_intersects();
00848 if (saturates_once && may_saturate)
00849 result = result && Poly_Con_Relation::saturates();
00850
00851 return result;
00852 }
00853
00854 template <typename PS>
00855 Poly_Con_Relation
00856 Pointset_Powerset<PS>::relation_with(const Constraint& c) const {
00857 const Pointset_Powerset& x = *this;
00858
00859
00860 bool is_included = true;
00861
00862 bool is_disjoint = true;
00863
00864
00865 bool is_strictly_intersecting = false;
00866
00867
00868 bool saturates_once = false;
00869 bool may_saturate = true;
00870 for (Sequence_const_iterator si = x.sequence.begin(),
00871 s_end = x.sequence.end(); si != s_end; ++si) {
00872 Poly_Con_Relation relation_i = si->element().relation_with(c);
00873 if (!relation_i.implies(Poly_Con_Relation::is_included()))
00874 is_included = false;
00875 if (!relation_i.implies(Poly_Con_Relation::is_disjoint()))
00876 is_disjoint = false;
00877 if (relation_i.implies(Poly_Con_Relation::strictly_intersects()))
00878 is_strictly_intersecting = true;
00879 if (relation_i.implies(Poly_Con_Relation::saturates()))
00880 saturates_once = true;
00881 else if (!relation_i.implies(Poly_Con_Relation::is_disjoint()))
00882 may_saturate = false;
00883 }
00884
00885 Poly_Con_Relation result = Poly_Con_Relation::nothing();
00886 if (is_included)
00887 result = result && Poly_Con_Relation::is_included();
00888 if (is_disjoint)
00889 result = result && Poly_Con_Relation::is_disjoint();
00890 if (is_strictly_intersecting)
00891 result = result && Poly_Con_Relation::strictly_intersects();
00892 if (saturates_once && may_saturate)
00893 result = result && Poly_Con_Relation::saturates();
00894
00895 return result;
00896 }
00897
00898 template <typename PS>
00899 Poly_Gen_Relation
00900 Pointset_Powerset<PS>::relation_with(const Generator& g) const {
00901 const Pointset_Powerset& x = *this;
00902
00903 for (Sequence_const_iterator si = x.sequence.begin(),
00904 s_end = x.sequence.end(); si != s_end; ++si) {
00905 Poly_Gen_Relation relation_i = si->element().relation_with(g);
00906 if (relation_i.implies(Poly_Gen_Relation::subsumes()))
00907 return Poly_Gen_Relation::subsumes();
00908 }
00909
00910 return Poly_Gen_Relation::nothing();
00911 }
00912
00913 template <typename PS>
00914 bool
00915 Pointset_Powerset<PS>
00916 ::bounds_from_above(const Linear_Expression& expr) const {
00917 const Pointset_Powerset& x = *this;
00918 x.omega_reduce();
00919 for (Sequence_const_iterator si = x.sequence.begin(),
00920 s_end = x.sequence.end(); si != s_end; ++si)
00921 if (!si->element().bounds_from_above(expr))
00922 return false;
00923 return true;
00924 }
00925
00926 template <typename PS>
00927 bool
00928 Pointset_Powerset<PS>
00929 ::bounds_from_below(const Linear_Expression& expr) const {
00930 const Pointset_Powerset& x = *this;
00931 x.omega_reduce();
00932 for (Sequence_const_iterator si = x.sequence.begin(),
00933 s_end = x.sequence.end(); si != s_end; ++si)
00934 if (!si->element().bounds_from_below(expr))
00935 return false;
00936 return true;
00937 }
00938
00939 template <typename PS>
00940 bool
00941 Pointset_Powerset<PS>::maximize(const Linear_Expression& expr,
00942 Coefficient& sup_n,
00943 Coefficient& sup_d,
00944 bool& maximum) const {
00945 const Pointset_Powerset& x = *this;
00946 x.omega_reduce();
00947 bool first = true;
00948
00949 Coefficient supt_n = 0;
00950 Coefficient supt_d = 1;
00951 bool maxt = 0;
00952
00953 Coefficient supi_n = 0;
00954 Coefficient supi_d = 1;
00955 bool maxi = 0;
00956 TEMP_INTEGER(tmp);
00957
00958 for (Sequence_const_iterator si = x.sequence.begin(),
00959 s_end = x.sequence.end(); si != s_end; ++si) {
00960 if (!si->element().maximize(expr, supi_n, supi_d, maxi))
00961 return false;
00962 else
00963 if (first) {
00964 first = false;
00965 supt_n = supi_n;
00966 supt_d = supi_d;
00967 maxt = maxi;
00968 }
00969 else {
00970 tmp = (supt_n * supi_d) - (supi_n * supt_d);
00971 if (tmp < 0) {
00972 supt_n = supi_n;
00973 supt_d = supi_d;
00974 maxt = maxi;
00975 }
00976 else if (tmp == 0)
00977 maxt = maxt || maxi;
00978 }
00979 }
00980 sup_n = supt_n;
00981 sup_d = supt_d;
00982 maximum = maxt;
00983 return true;
00984 }
00985
00986 template <typename PS>
00987 bool
00988 Pointset_Powerset<PS>::maximize(const Linear_Expression& expr,
00989 Coefficient& sup_n,
00990 Coefficient& sup_d,
00991 bool& maximum,
00992 Generator& g) const {
00993 const Pointset_Powerset& x = *this;
00994 x.omega_reduce();
00995 bool first = true;
00996
00997 Coefficient supt_n = 0;
00998 Coefficient supt_d = 1;
00999 bool maxt = 0;
01000 Generator gt = point();
01001
01002 Coefficient supi_n = 0;
01003 Coefficient supi_d = 1;
01004 bool maxi = 0;
01005 Generator gi = point();
01006 TEMP_INTEGER(tmp);
01007
01008 for (Sequence_const_iterator si = x.sequence.begin(),
01009 s_end = x.sequence.end(); si != s_end; ++si) {
01010 if (!si->element().maximize(expr, supi_n, supi_d, maxi, gi))
01011 return false;
01012 else
01013 if (first) {
01014 first = false;
01015 supt_n = supi_n;
01016 supt_d = supi_d;
01017 maxt = maxi;
01018 gt = gi;
01019 }
01020 else {
01021 tmp = (supt_n * supi_d) - (supi_n * supt_d);
01022 if (tmp < 0) {
01023 supt_n = supi_n;
01024 supt_d = supi_d;
01025 maxt = maxi;
01026 gt = gi;
01027 }
01028 else if (tmp == 0) {
01029 maxt = maxt || maxi;
01030 gt = gi;
01031 }
01032 }
01033 }
01034 sup_n = supt_n;
01035 sup_d = supt_d;
01036 maximum = maxt;
01037 g = gt;
01038 return true;
01039 }
01040
01041 template <typename PS>
01042 bool
01043 Pointset_Powerset<PS>::minimize(const Linear_Expression& expr,
01044 Coefficient& inf_n,
01045 Coefficient& inf_d,
01046 bool& minimum) const {
01047 const Pointset_Powerset& x = *this;
01048 x.omega_reduce();
01049 bool first = true;
01050
01051 Coefficient inft_n = 0;
01052 Coefficient inft_d = 1;
01053 bool mint = 0;
01054
01055 Coefficient infi_n = 0;
01056 Coefficient infi_d = 1;
01057 bool mini = 0;
01058 TEMP_INTEGER(tmp);
01059
01060 for (Sequence_const_iterator si = x.sequence.begin(),
01061 s_end = x.sequence.end(); si != s_end; ++si) {
01062 if (!si->element().minimize(expr, infi_n, infi_d, mini))
01063 return false;
01064 else
01065 if (first) {
01066 first = false;
01067 inft_n = infi_n;
01068 inft_d = infi_d;
01069 mint = mini;
01070 }
01071 else {
01072 tmp = (inft_n * infi_d) - (infi_n * inft_d);
01073 if (tmp > 0) {
01074 inft_n = infi_n;
01075 inft_d = infi_d;
01076 mint = mini;
01077 }
01078 else if (tmp == 0)
01079 mint = mint || mini;
01080 }
01081 }
01082 inf_n = inft_n;
01083 inf_d = inft_d;
01084 minimum = mint;
01085 return true;
01086 }
01087
01088 template <typename PS>
01089 bool
01090 Pointset_Powerset<PS>::minimize(const Linear_Expression& expr,
01091 Coefficient& inf_n,
01092 Coefficient& inf_d,
01093 bool& minimum,
01094 Generator& g) const {
01095 const Pointset_Powerset& x = *this;
01096 x.omega_reduce();
01097 bool first = true;
01098
01099 Coefficient inft_n = 0;
01100 Coefficient inft_d = 1;
01101 bool mint = 0;
01102 Generator gt = point();
01103
01104 Coefficient infi_n = 0;
01105 Coefficient infi_d = 1;
01106 bool mini = 0;
01107 Generator gi = point();
01108 TEMP_INTEGER(tmp);
01109
01110 for (Sequence_const_iterator si = x.sequence.begin(),
01111 s_end = x.sequence.end(); si != s_end; ++si) {
01112 if (!si->element().minimize(expr, infi_n, infi_d, mini, gi))
01113 return false;
01114 else
01115 if (first) {
01116 first = false;
01117 inft_n = infi_n;
01118 inft_d = infi_d;
01119 mint = mini;
01120 gt = gi;
01121 }
01122 else {
01123 tmp = (inft_n * infi_d) - (infi_n * inft_d);
01124 if (tmp > 0) {
01125 inft_n = infi_n;
01126 inft_d = infi_d;
01127 mint = mini;
01128 gt = gi;
01129 }
01130 else if (tmp == 0) {
01131 mint = mint || mini;
01132 gt = gi;
01133 }
01134 }
01135 }
01136 inf_n = inft_n;
01137 inf_d = inft_d;
01138 minimum = mint;
01139 g = gt;
01140 return true;
01141 }
01142
01143 template <typename PS>
01144 bool
01145 Pointset_Powerset<PS>::contains_integer_point() const {
01146 const Pointset_Powerset& x = *this;
01147 for (Sequence_const_iterator si = x.sequence.begin(),
01148 s_end = x.sequence.end(); si != s_end; ++si)
01149 if (si->element().contains_integer_point())
01150 return true;
01151 return false;
01152 }
01153
01154 template <typename PS>
01155 void
01156 Pointset_Powerset<PS>::pairwise_reduce() {
01157 Pointset_Powerset& x = *this;
01158
01159 x.omega_reduce();
01160
01161 size_type n = x.size();
01162 size_type deleted;
01163 do {
01164 Pointset_Powerset new_x(x.space_dim, EMPTY);
01165 std::deque<bool> marked(n, false);
01166 deleted = 0;
01167 Sequence_iterator s_begin = x.sequence.begin();
01168 Sequence_iterator s_end = x.sequence.end();
01169 unsigned si_index = 0;
01170 for (Sequence_iterator si = s_begin; si != s_end; ++si, ++si_index) {
01171 if (marked[si_index])
01172 continue;
01173 PS& pi = si->element();
01174 Sequence_const_iterator sj = si;
01175 unsigned sj_index = si_index;
01176 for (++sj, ++sj_index; sj != s_end; ++sj, ++sj_index) {
01177 if (marked[sj_index])
01178 continue;
01179 const PS& pj = sj->element();
01180 if (pi.upper_bound_assign_if_exact(pj)) {
01181 marked[si_index] = marked[sj_index] = true;
01182
01183
01184 new_x.add_non_bottom_disjunct_preserve_reduction(pi);
01185 ++deleted;
01186 goto next;
01187 }
01188 }
01189 next:
01190 ;
01191 }
01192 iterator nx_begin = new_x.begin();
01193 iterator nx_end = new_x.end();
01194 unsigned xi_index = 0;
01195 for (const_iterator xi = x.begin(),
01196 x_end = x.end(); xi != x_end; ++xi, ++xi_index)
01197 if (!marked[xi_index])
01198 nx_begin = new_x.add_non_bottom_disjunct_preserve_reduction(*xi,
01199 nx_begin,
01200 nx_end);
01201 std::swap(x.sequence, new_x.sequence);
01202 n -= deleted;
01203 } while (deleted > 0);
01204 assert(x.OK());
01205 }
01206
01207 template <typename PS>
01208 template <typename Widening>
01209 void
01210 Pointset_Powerset<PS>::
01211 BGP99_heuristics_assign(const Pointset_Powerset& y, Widening wf) {
01212
01213 Pointset_Powerset& x = *this;
01214
01215 #ifndef NDEBUG
01216 {
01217
01218 const Pointset_Powerset<PS> x_copy = x;
01219 const Pointset_Powerset<PS> y_copy = y;
01220 assert(y_copy.definitely_entails(x_copy));
01221 }
01222 #endif
01223
01224 size_type n = x.size();
01225 Pointset_Powerset new_x(x.space_dim, EMPTY);
01226 std::deque<bool> marked(n, false);
01227 const_iterator x_begin = x.begin();
01228 const_iterator x_end = x.end();
01229 unsigned i_index = 0;
01230 for (const_iterator i = x_begin,
01231 y_begin = y.begin(), y_end = y.end(); i != x_end; ++i, ++i_index)
01232 for (const_iterator j = y_begin; j != y_end; ++j) {
01233 const PS& pi = i->element();
01234 const PS& pj = j->element();
01235 if (pi.contains(pj)) {
01236 PS pi_copy = pi;
01237 wf(pi_copy, pj);
01238
01239
01240 new_x.add_non_bottom_disjunct_preserve_reduction(pi_copy);
01241 marked[i_index] = true;
01242 }
01243 }
01244 iterator nx_begin = new_x.begin();
01245 iterator nx_end = new_x.end();
01246 i_index = 0;
01247 for (const_iterator i = x_begin; i != x_end; ++i, ++i_index)
01248 if (!marked[i_index])
01249 nx_begin = new_x.add_non_bottom_disjunct_preserve_reduction(*i,
01250 nx_begin,
01251 nx_end);
01252 std::swap(x.sequence, new_x.sequence);
01253 assert(x.OK());
01254 assert(x.is_omega_reduced());
01255 }
01256
01257 template <typename PS>
01258 template <typename Widening>
01259 void
01260 Pointset_Powerset<PS>::
01261 BGP99_extrapolation_assign(const Pointset_Powerset& y,
01262 Widening wf,
01263 unsigned max_disjuncts) {
01264
01265 Pointset_Powerset& x = *this;
01266
01267 #ifndef NDEBUG
01268 {
01269
01270 const Pointset_Powerset<PS> x_copy = x;
01271 const Pointset_Powerset<PS> y_copy = y;
01272 assert(y_copy.definitely_entails(x_copy));
01273 }
01274 #endif
01275
01276 x.pairwise_reduce();
01277 if (max_disjuncts != 0)
01278 x.collapse(max_disjuncts);
01279 x.BGP99_heuristics_assign(y, wf);
01280 }
01281
01282 template <typename PS>
01283 template <typename Cert>
01284 void
01285 Pointset_Powerset<PS>::
01286 collect_certificates(std::map<Cert, size_type,
01287 typename Cert::Compare>& cert_ms) const {
01288 const Pointset_Powerset& x = *this;
01289 assert(x.is_omega_reduced());
01290 assert(cert_ms.size() == 0);
01291 for (const_iterator i = x.begin(), end = x.end(); i != end; i++) {
01292 Cert ph_cert(i->element());
01293 ++cert_ms[ph_cert];
01294 }
01295 }
01296
01297 template <typename PS>
01298 template <typename Cert>
01299 bool
01300 Pointset_Powerset<PS>::
01301 is_cert_multiset_stabilizing(const std::map<Cert, size_type,
01302 typename Cert::Compare>& y_cert_ms
01303 ) const {
01304 typedef std::map<Cert, size_type, typename Cert::Compare> Cert_Multiset;
01305 Cert_Multiset x_cert_ms;
01306 collect_certificates(x_cert_ms);
01307 typename Cert_Multiset::const_iterator
01308 xi = x_cert_ms.begin(),
01309 x_cert_ms_end = x_cert_ms.end(),
01310 yi = y_cert_ms.begin(),
01311 y_cert_ms_end = y_cert_ms.end();
01312 while (xi != x_cert_ms_end && yi != y_cert_ms_end) {
01313 const Cert& xi_cert = xi->first;
01314 const Cert& yi_cert = yi->first;
01315 switch (xi_cert.compare(yi_cert)) {
01316 case 0:
01317
01318 {
01319 const size_type& xi_count = xi->second;
01320 const size_type& yi_count = yi->second;
01321 if (xi_count == yi_count) {
01322
01323 ++xi;
01324 ++yi;
01325 }
01326 else
01327
01328 return xi_count < yi_count;
01329 break;
01330 }
01331 case 1:
01332
01333 return false;
01334
01335 case -1:
01336
01337 return true;
01338 }
01339 }
01340
01341
01342 return yi != y_cert_ms_end;
01343 }
01344
01345 template <typename PS>
01346 template <typename Cert, typename Widening>
01347 void
01348 Pointset_Powerset<PS>::BHZ03_widening_assign(const Pointset_Powerset& y,
01349 Widening wf) {
01350
01351 Pointset_Powerset& x = *this;
01352
01353 #ifndef NDEBUG
01354 {
01355
01356 const Pointset_Powerset<PS> x_copy = x;
01357 const Pointset_Powerset<PS> y_copy = y;
01358 assert(y_copy.definitely_entails(x_copy));
01359 }
01360 #endif
01361
01362
01363
01364
01365 assert(x.size() > 0);
01366 if (y.size() == 0)
01367 return;
01368
01369
01370 PS x_hull(x.space_dim, EMPTY);
01371 for (const_iterator i = x.begin(), x_end = x.end(); i != x_end; ++i)
01372 x_hull.upper_bound_assign(i->element());
01373
01374
01375 PS y_hull(y.space_dim, EMPTY);
01376 for (const_iterator i = y.begin(), y_end = y.end(); i != y_end; ++i)
01377 y_hull.upper_bound_assign(i->element());
01378
01379 const Cert y_hull_cert(y_hull);
01380
01381
01382 int hull_stabilization = y_hull_cert.compare(x_hull);
01383 if (hull_stabilization == 1)
01384 return;
01385
01386
01387 const bool y_is_not_a_singleton = y.size() > 1;
01388
01389
01390
01391 typedef std::map<Cert, size_type, typename Cert::Compare> Cert_Multiset;
01392 Cert_Multiset y_cert_ms;
01393 bool y_cert_ms_computed = false;
01394
01395 if (hull_stabilization == 0 && y_is_not_a_singleton) {
01396
01397 y.collect_certificates(y_cert_ms);
01398 y_cert_ms_computed = true;
01399
01400 if (x.is_cert_multiset_stabilizing(y_cert_ms))
01401 return;
01402 }
01403
01404
01405 Pointset_Powerset<PS> bgp99_heuristics = x;
01406 bgp99_heuristics.BGP99_heuristics_assign(y, wf);
01407
01408
01409 PS bgp99_heuristics_hull(x.space_dim, EMPTY);
01410 for (const_iterator i = bgp99_heuristics.begin(),
01411 bh_end = bgp99_heuristics.end(); i != bh_end; ++i)
01412 bgp99_heuristics_hull.upper_bound_assign(i->element());
01413
01414
01415
01416 hull_stabilization = y_hull_cert.compare(bgp99_heuristics_hull);
01417 if (hull_stabilization == 1) {
01418
01419 std::swap(x, bgp99_heuristics);
01420 return;
01421 }
01422 else if (hull_stabilization == 0 && y_is_not_a_singleton) {
01423
01424 if (!y_cert_ms_computed) {
01425 y.collect_certificates(y_cert_ms);
01426 y_cert_ms_computed = true;
01427 }
01428 if (bgp99_heuristics.is_cert_multiset_stabilizing(y_cert_ms)) {
01429 std::swap(x, bgp99_heuristics);
01430 return;
01431 }
01432
01433
01434
01435
01436 Pointset_Powerset<PS> reduced_bgp99_heuristics(bgp99_heuristics);
01437 reduced_bgp99_heuristics.pairwise_reduce();
01438 if (reduced_bgp99_heuristics.is_cert_multiset_stabilizing(y_cert_ms)) {
01439 std::swap(x, reduced_bgp99_heuristics);
01440 return;
01441 }
01442 }
01443
01444
01445
01446 if (bgp99_heuristics_hull.strictly_contains(y_hull)) {
01447
01448 PS ph = bgp99_heuristics_hull;
01449 wf(ph, y_hull);
01450
01451 ph.difference_assign(bgp99_heuristics_hull);
01452 x.add_disjunct(ph);
01453 return;
01454 }
01455
01456
01457 Pointset_Powerset<PS> x_hull_singleton(x.space_dim, EMPTY);
01458 x_hull_singleton.add_disjunct(x_hull);
01459 std::swap(x, x_hull_singleton);
01460 }
01461
01462 template <typename PS>
01463 void
01464 Pointset_Powerset<PS>::ascii_dump(std::ostream& s) const {
01465 const Pointset_Powerset& x = *this;
01466 s << "size " << x.size()
01467 << "\nspace_dim " << x.space_dim
01468 << "\n";
01469 for (const_iterator xi = x.begin(), x_end = x.end(); xi != x_end; ++xi)
01470 xi->element().ascii_dump(s);
01471 }
01472
01473 PPL_OUTPUT_TEMPLATE_DEFINITIONS(PS, Pointset_Powerset<PS>)
01474
01475 template <typename PS>
01476 bool
01477 Pointset_Powerset<PS>::ascii_load(std::istream& s) {
01478 Pointset_Powerset& x = *this;
01479 std::string str;
01480
01481 if (!(s >> str) || str != "size")
01482 return false;
01483
01484 size_type sz;
01485
01486 if (!(s >> sz))
01487 return false;
01488
01489 if (!(s >> str) || str != "space_dim")
01490 return false;
01491
01492 if (!(s >> x.space_dim))
01493 return false;
01494
01495 Pointset_Powerset new_x(x.space_dim, EMPTY);
01496 while (sz-- > 0) {
01497 PS ph;
01498 if (!ph.ascii_load(s))
01499 return false;
01500 new_x.add_disjunct(ph);
01501 }
01502 x.swap(new_x);
01503
01504
01505 assert(x.OK());
01506 return true;
01507 }
01508
01509 template <typename PS>
01510 bool
01511 Pointset_Powerset<PS>::OK() const {
01512 const Pointset_Powerset& x = *this;
01513 for (const_iterator xi = x.begin(), x_end = x.end(); xi != x_end; ++xi) {
01514 const PS& pi = xi->element();
01515 if (pi.space_dimension() != x.space_dim) {
01516 #ifndef NDEBUG
01517 std::cerr << "Space dimension mismatch: is " << pi.space_dimension()
01518 << " in an element of the sequence,\nshould be "
01519 << x.space_dim << "."
01520 << std::endl;
01521 #endif
01522 return false;
01523 }
01524 }
01525 return x.Base::OK();
01526 }
01527
01528 namespace Implementation {
01529
01530 namespace Pointset_Powersets {
01531
01532 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
01534
01539 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
01540 template <typename PS>
01541 void
01542 linear_partition_aux(const Constraint& c,
01543 PS& qq,
01544 Pointset_Powerset<NNC_Polyhedron>& r) {
01545 Linear_Expression le(c);
01546 const Constraint& neg_c = c.is_strict_inequality() ? (le <= 0) : (le < 0);
01547 NNC_Polyhedron qqq(qq);
01548 qqq.add_constraint(neg_c);
01549 if (!qqq.is_empty())
01550 r.add_disjunct(qqq);
01551 qq.add_constraint(c);
01552 }
01553
01554 }
01555
01556 }
01557
01558
01560 template <typename PS>
01561 std::pair<PS, Pointset_Powerset<NNC_Polyhedron> >
01562 linear_partition(const PS& p, const PS& q) {
01563 using Implementation::Pointset_Powersets::linear_partition_aux;
01564
01565 Pointset_Powerset<NNC_Polyhedron> r(p.space_dimension(), EMPTY);
01566 PS qq = q;
01567 const Constraint_System& pcs = p.constraints();
01568 for (Constraint_System::const_iterator i = pcs.begin(),
01569 pcs_end = pcs.end(); i != pcs_end; ++i) {
01570 const Constraint& c = *i;
01571 if (c.is_equality()) {
01572 Linear_Expression le(c);
01573 linear_partition_aux(le <= 0, qq, r);
01574 linear_partition_aux(le >= 0, qq, r);
01575 }
01576 else
01577 linear_partition_aux(c, qq, r);
01578 }
01579 return std::make_pair(qq, r);
01580 }
01581
01582 }
01583
01584 #endif // !defined(PPL_Pointset_Powerset_templates_hh)