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_Box_inlines_hh
00024 #define PPL_Box_inlines_hh 1
00025
00026 #include "Boundary.defs.hh"
00027 #include "Constraint_System.defs.hh"
00028 #include "Constraint_System.inlines.hh"
00029 #include "Congruence_System.defs.hh"
00030 #include "Congruence_System.inlines.hh"
00031 #include "distances.defs.hh"
00032
00033 namespace Parma_Polyhedra_Library {
00034
00035 template <typename ITV>
00036 inline bool
00037 Box<ITV>::marked_empty() const {
00038 return status.test_empty_up_to_date() && status.test_empty();
00039 }
00040
00041 template <typename ITV>
00042 inline void
00043 Box<ITV>::set_empty() {
00044 status.set_empty();
00045 status.set_empty_up_to_date();
00046 }
00047
00048 template <typename ITV>
00049 inline void
00050 Box<ITV>::set_nonempty() {
00051 status.reset_empty();
00052 status.set_empty_up_to_date();
00053 }
00054
00055 template <typename ITV>
00056 inline void
00057 Box<ITV>::set_empty_up_to_date() {
00058 status.set_empty_up_to_date();
00059 }
00060
00061 template <typename ITV>
00062 inline void
00063 Box<ITV>::reset_empty_up_to_date() {
00064 return status.reset_empty_up_to_date();
00065 }
00066
00067 template <typename ITV>
00068 inline
00069 Box<ITV>::Box(const Box& y, Complexity_Class)
00070 : seq(y.seq), status(y.status) {
00071 }
00072
00073 template <typename ITV>
00074 inline Box<ITV>&
00075 Box<ITV>::operator=(const Box& y) {
00076 seq = y.seq;
00077 status = y.status;
00078 return *this;
00079 }
00080
00081 template <typename ITV>
00082 inline void
00083 Box<ITV>::swap(Box& y) {
00084 Box& x = *this;
00085 std::swap(x.seq, y.seq);
00086 std::swap(x.status, y.status);
00087 }
00088
00089 template <typename ITV>
00090 inline
00091 Box<ITV>::Box(const Constraint_System& cs, Recycle_Input) {
00092
00093 Box<ITV> tmp(cs);
00094 this->swap(tmp);
00095 }
00096
00097 template <typename ITV>
00098 inline
00099 Box<ITV>::Box(const Generator_System& gs, Recycle_Input) {
00100
00101 Box<ITV> tmp(gs);
00102 this->swap(tmp);
00103 }
00104
00105 template <typename ITV>
00106 inline
00107 Box<ITV>::Box(const Congruence_System& cgs, Recycle_Input) {
00108
00109 Box<ITV> tmp(cgs);
00110 this->swap(tmp);
00111 }
00112
00113 template <typename ITV>
00114 inline memory_size_type
00115 Box<ITV>::total_memory_in_bytes() const {
00116 return sizeof(*this) + external_memory_in_bytes();
00117 }
00118
00119 template <typename ITV>
00120 inline dimension_type
00121 Box<ITV>::space_dimension() const {
00122 return seq.size();
00123 }
00124
00125 template <typename ITV>
00126 inline dimension_type
00127 Box<ITV>::max_space_dimension() {
00128
00129
00130 return Sequence().max_size() - 1;
00131 }
00132
00133 template <typename ITV>
00134 inline const ITV&
00135 Box<ITV>::operator[](const dimension_type k) const {
00136 assert(k < seq.size());
00137 return seq[k];
00138 }
00139
00140 template <typename ITV>
00141 inline const ITV&
00142 Box<ITV>::get_interval(const Variable var) const {
00143 if (space_dimension() < var.space_dimension())
00144 throw_dimension_incompatible("get_interval(v)", "v", var);
00145
00146 if (is_empty()) {
00147 static ITV empty_interval(EMPTY);
00148 return empty_interval;
00149 }
00150
00151 return seq[var.id()];
00152 }
00153
00154 template <typename ITV>
00155 inline void
00156 Box<ITV>::set_interval(const Variable var, const ITV& i) {
00157 const dimension_type space_dim = space_dimension();
00158 if (space_dim < var.space_dimension())
00159 throw_dimension_incompatible("set_interval(v, i)", "v", var);
00160
00161 if (is_empty() && space_dim >= 2)
00162
00163
00164 return;
00165
00166 seq[var.id()] = i;
00167 reset_empty_up_to_date();
00168
00169 assert(OK());
00170 }
00171
00172 template <typename ITV>
00173 inline bool
00174 Box<ITV>::is_empty() const {
00175 return marked_empty() || check_empty();
00176 }
00177
00178 template <typename ITV>
00179 inline bool
00180 Box<ITV>::bounds_from_above(const Linear_Expression& expr) const {
00181 return bounds(expr, true);
00182 }
00183
00184 template <typename ITV>
00185 inline bool
00186 Box<ITV>::bounds_from_below(const Linear_Expression& expr) const {
00187 return bounds(expr, false);
00188 }
00189
00190 template <typename ITV>
00191 inline bool
00192 Box<ITV>::maximize(const Linear_Expression& expr,
00193 Coefficient& sup_n, Coefficient& sup_d,
00194 bool& maximum) const {
00195 return max_min(expr, true, sup_n, sup_d, maximum);
00196 }
00197
00198 template <typename ITV>
00199 inline bool
00200 Box<ITV>::maximize(const Linear_Expression& expr,
00201 Coefficient& sup_n, Coefficient& sup_d, bool& maximum,
00202 Generator& g) const {
00203 return max_min(expr, true, sup_n, sup_d, maximum, g);
00204 }
00205
00206 template <typename ITV>
00207 inline bool
00208 Box<ITV>::minimize(const Linear_Expression& expr,
00209 Coefficient& inf_n, Coefficient& inf_d,
00210 bool& minimum) const {
00211 return max_min(expr, false, inf_n, inf_d, minimum);
00212 }
00213
00214 template <typename ITV>
00215 inline bool
00216 Box<ITV>::minimize(const Linear_Expression& expr,
00217 Coefficient& inf_n, Coefficient& inf_d, bool& minimum,
00218 Generator& g) const {
00219 return max_min(expr, false, inf_n, inf_d, minimum, g);
00220 }
00221
00222 template <typename ITV>
00223 inline bool
00224 Box<ITV>::strictly_contains(const Box& y) const {
00225 const Box& x = *this;
00226 return x.contains(y) && !y.contains(x);
00227 }
00228
00229 template <typename ITV>
00230 inline bool
00231 Box<ITV>::upper_bound_assign_if_exact(const Box&) {
00232
00233 return false;
00234 }
00235
00236 template <typename ITV>
00237 inline void
00238 Box<ITV>::expand_space_dimension(const Variable var,
00239 const dimension_type m) {
00240 const dimension_type space_dim = space_dimension();
00241
00242 if (var.space_dimension() > space_dim)
00243 throw_dimension_incompatible("expand_space_dimension(v, m)", "v", var);
00244
00245
00246
00247 if (m > max_space_dimension() - space_dim)
00248 throw_generic("expand_dimension(v, m)",
00249 "adding m new space dimensions exceeds "
00250 "the maximum allowed space dimension");
00251
00252
00253
00254 seq.insert(seq.end(), m, seq[var.id()]);
00255 assert(OK());
00256 }
00257
00258 template <typename ITV>
00259 inline bool
00260 operator!=(const Box<ITV>& x, const Box<ITV>& y) {
00261 return !(x == y);
00262 }
00263
00264 template <typename ITV>
00265 inline bool
00266 Box<ITV>::get_lower_bound(const dimension_type k, bool& closed,
00267 Coefficient& n, Coefficient& d) const {
00268 assert(k < seq.size());
00269 const ITV& seq_k = seq[k];
00270
00271 if (seq_k.lower_is_unbounded())
00272 return false;
00273
00274 closed = !seq_k.lower_is_open();
00275
00276 DIRTY_TEMP0(mpq_class, lr);
00277 assign_r(lr, seq_k.lower(), ROUND_NOT_NEEDED);
00278 n = lr.get_num();
00279 d = lr.get_den();
00280
00281 return true;
00282 }
00283
00284 template <typename ITV>
00285 inline bool
00286 Box<ITV>::get_upper_bound(const dimension_type k, bool& closed,
00287 Coefficient& n, Coefficient& d) const {
00288 assert(k < seq.size());
00289 const ITV& seq_k = seq[k];
00290
00291 if (seq_k.upper_is_unbounded())
00292 return false;
00293
00294 closed = !seq_k.upper_is_open();
00295
00296 DIRTY_TEMP0(mpq_class, ur);
00297 assign_r(ur, seq_k.upper(), ROUND_NOT_NEEDED);
00298 n = ur.get_num();
00299 d = ur.get_den();
00300
00301 return true;
00302 }
00303
00304 template <typename ITV>
00305 inline void
00306 Box<ITV>::add_constraint(const Constraint& c) {
00307 const dimension_type c_space_dim = c.space_dimension();
00308
00309 if (c_space_dim > space_dimension())
00310 throw_dimension_incompatible("add_constraint(c)", c);
00311
00312 add_constraint_no_check(c);
00313 }
00314
00315 template <typename ITV>
00316 inline void
00317 Box<ITV>::add_constraints(const Constraint_System& cs) {
00318
00319 if (cs.space_dimension() > space_dimension())
00320 throw_dimension_incompatible("add_constraints(cs)", cs);
00321
00322 add_constraints_no_check(cs);
00323 }
00324
00325 template <typename T>
00326 inline void
00327 Box<T>::add_recycled_constraints(Constraint_System& cs) {
00328 add_constraints(cs);
00329 }
00330
00331 template <typename ITV>
00332 inline void
00333 Box<ITV>::add_congruence(const Congruence& cg) {
00334 const dimension_type cg_space_dim = cg.space_dimension();
00335
00336 if (cg_space_dim > space_dimension())
00337 throw_dimension_incompatible("add_congruence(cg)", cg);
00338
00339 add_congruence_no_check(cg);
00340 }
00341
00342 template <typename ITV>
00343 inline void
00344 Box<ITV>::add_congruences(const Congruence_System& cgs) {
00345 if (cgs.space_dimension() > space_dimension())
00346 throw_dimension_incompatible("add_congruences(cgs)", cgs);
00347 add_congruences_no_check(cgs);
00348 }
00349
00350 template <typename T>
00351 inline void
00352 Box<T>::add_recycled_congruences(Congruence_System& cgs) {
00353 add_congruences(cgs);
00354 }
00355
00356 template <typename T>
00357 inline bool
00358 Box<T>::can_recycle_constraint_systems() {
00359 return false;
00360 }
00361
00362 template <typename T>
00363 inline bool
00364 Box<T>::can_recycle_congruence_systems() {
00365 return false;
00366 }
00367
00368 template <typename T>
00369 inline void
00370 Box<T>::widening_assign(const Box& y, unsigned* tp) {
00371 CC76_widening_assign(y, tp);
00372 }
00373
00374 template <typename ITV>
00375 inline Congruence_System
00376 Box<ITV>::minimized_congruences() const {
00377
00378 return congruences();
00379 }
00380
00381 template <typename ITV>
00382 inline void
00383 Box<ITV>
00384 ::add_interval_constraint_no_check(const dimension_type var_id,
00385 const Constraint::Type type,
00386 Coefficient_traits::const_reference num,
00387 Coefficient_traits::const_reference den) {
00388 assert(!marked_empty());
00389 assert(var_id < space_dimension());
00390 assert(den != 0);
00391
00392
00393
00394
00395
00396
00397 DIRTY_TEMP0(mpq_class, q);
00398 assign_r(q.get_num(), num, ROUND_NOT_NEEDED);
00399 assign_r(q.get_den(), den, ROUND_NOT_NEEDED);
00400 q.canonicalize();
00401
00402 q = -q;
00403
00404 ITV& seq_v = seq[var_id];
00405 switch (type) {
00406 case Constraint::EQUALITY:
00407 seq_v.refine_existential(EQUAL, q);
00408 break;
00409 case Constraint::NONSTRICT_INEQUALITY:
00410 seq_v.refine_existential((den > 0) ? GREATER_OR_EQUAL : LESS_OR_EQUAL, q);
00411
00412 assert(seq_v.OK());
00413 break;
00414 case Constraint::STRICT_INEQUALITY:
00415 seq_v.refine_existential((den > 0) ? GREATER_THAN : LESS_THAN, q);
00416 break;
00417 }
00418
00419
00420 reset_empty_up_to_date();
00421 assert(OK());
00422 }
00423
00424 template <typename ITV>
00425 inline void
00426 Box<ITV>::refine_with_constraint(const Constraint& c) {
00427 const dimension_type c_space_dim = c.space_dimension();
00428
00429 if (c_space_dim > space_dimension())
00430 throw_dimension_incompatible("refine_with_constraint(c)", c);
00431
00432
00433 if (marked_empty())
00434 return;
00435
00436 refine_no_check(c);
00437 }
00438
00439 template <typename ITV>
00440 inline void
00441 Box<ITV>::refine_with_constraints(const Constraint_System& cs) {
00442
00443 if (cs.space_dimension() > space_dimension())
00444 throw_dimension_incompatible("refine_with_constraints(cs)", cs);
00445
00446
00447 if (marked_empty())
00448 return;
00449
00450 refine_no_check(cs);
00451 }
00452
00453 template <typename ITV>
00454 inline void
00455 Box<ITV>::refine_with_congruence(const Congruence& cg) {
00456 const dimension_type cg_space_dim = cg.space_dimension();
00457
00458 if (cg_space_dim > space_dimension())
00459 throw_dimension_incompatible("refine_with_congruence(cg)", cg);
00460
00461
00462 if (marked_empty())
00463 return;
00464
00465 refine_no_check(cg);
00466 }
00467
00468 template <typename ITV>
00469 inline void
00470 Box<ITV>::refine_with_congruences(const Congruence_System& cgs) {
00471
00472 if (cgs.space_dimension() > space_dimension())
00473 throw_dimension_incompatible("refine_with_congruences(cgs)", cgs);
00474
00475
00476 if (marked_empty())
00477 return;
00478
00479 refine_no_check(cgs);
00480 }
00481
00482 template <typename ITV>
00483 inline void
00484 Box<ITV>::propagate_constraint(const Constraint& c) {
00485 const dimension_type c_space_dim = c.space_dimension();
00486
00487 if (c_space_dim > space_dimension())
00488 throw_dimension_incompatible("propagate_constraint(c)", c);
00489
00490
00491 if (marked_empty())
00492 return;
00493
00494 propagate_constraint_no_check(c);
00495 }
00496
00497 template <typename ITV>
00498 inline void
00499 Box<ITV>::propagate_constraints(const Constraint_System& cs) {
00500
00501 if (cs.space_dimension() > space_dimension())
00502 throw_dimension_incompatible("propagate_constraints(cs)", cs);
00503
00504
00505 if (marked_empty())
00506 return;
00507
00508 propagate_constraints_no_check(cs);
00509 }
00510
00511 template <typename ITV>
00512 inline void
00513 Box<ITV>::unconstrain(const Variable var) {
00514 const dimension_type dim = var.id();
00515
00516 if (dim > space_dimension())
00517 throw_dimension_incompatible("unconstrain(var)", dim);
00518
00519
00520 if (marked_empty())
00521 return;
00522
00523
00524 ITV& seq_var = seq[dim];
00525 if (seq_var.is_empty())
00526 set_empty();
00527 else
00528 seq_var.assign(UNIVERSE);
00529 assert(OK());
00530 }
00531
00533 template <typename Temp, typename To, typename ITV>
00534 inline bool
00535 rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00536 const Box<ITV>& x,
00537 const Box<ITV>& y,
00538 const Rounding_Dir dir,
00539 Temp& tmp0,
00540 Temp& tmp1,
00541 Temp& tmp2) {
00542 return l_m_distance_assign<Rectilinear_Distance_Specialization<Temp> >
00543 (r, x, y, dir, tmp0, tmp1, tmp2);
00544 }
00545
00547 template <typename Temp, typename To, typename ITV>
00548 inline bool
00549 rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00550 const Box<ITV>& x,
00551 const Box<ITV>& y,
00552 const Rounding_Dir dir) {
00553 typedef Checked_Number<Temp, Extended_Number_Policy> Checked_Temp;
00554 DIRTY_TEMP(Checked_Temp, tmp0);
00555 DIRTY_TEMP(Checked_Temp, tmp1);
00556 DIRTY_TEMP(Checked_Temp, tmp2);
00557 return rectilinear_distance_assign(r, x, y, dir, tmp0, tmp1, tmp2);
00558 }
00559
00561 template <typename To, typename ITV>
00562 inline bool
00563 rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00564 const Box<ITV>& x,
00565 const Box<ITV>& y,
00566 const Rounding_Dir dir) {
00567 return rectilinear_distance_assign<To, To, ITV>(r, x, y, dir);
00568 }
00569
00571 template <typename Temp, typename To, typename ITV>
00572 inline bool
00573 euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00574 const Box<ITV>& x,
00575 const Box<ITV>& y,
00576 const Rounding_Dir dir,
00577 Temp& tmp0,
00578 Temp& tmp1,
00579 Temp& tmp2) {
00580 return l_m_distance_assign<Euclidean_Distance_Specialization<Temp> >
00581 (r, x, y, dir, tmp0, tmp1, tmp2);
00582 }
00583
00585 template <typename Temp, typename To, typename ITV>
00586 inline bool
00587 euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00588 const Box<ITV>& x,
00589 const Box<ITV>& y,
00590 const Rounding_Dir dir) {
00591 typedef Checked_Number<Temp, Extended_Number_Policy> Checked_Temp;
00592 DIRTY_TEMP(Checked_Temp, tmp0);
00593 DIRTY_TEMP(Checked_Temp, tmp1);
00594 DIRTY_TEMP(Checked_Temp, tmp2);
00595 return euclidean_distance_assign(r, x, y, dir, tmp0, tmp1, tmp2);
00596 }
00597
00599 template <typename To, typename ITV>
00600 inline bool
00601 euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00602 const Box<ITV>& x,
00603 const Box<ITV>& y,
00604 const Rounding_Dir dir) {
00605 return euclidean_distance_assign<To, To, ITV>(r, x, y, dir);
00606 }
00607
00609 template <typename Temp, typename To, typename ITV>
00610 inline bool
00611 l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00612 const Box<ITV>& x,
00613 const Box<ITV>& y,
00614 const Rounding_Dir dir,
00615 Temp& tmp0,
00616 Temp& tmp1,
00617 Temp& tmp2) {
00618 return l_m_distance_assign<L_Infinity_Distance_Specialization<Temp> >
00619 (r, x, y, dir, tmp0, tmp1, tmp2);
00620 }
00621
00623 template <typename Temp, typename To, typename ITV>
00624 inline bool
00625 l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00626 const Box<ITV>& x,
00627 const Box<ITV>& y,
00628 const Rounding_Dir dir) {
00629 typedef Checked_Number<Temp, Extended_Number_Policy> Checked_Temp;
00630 DIRTY_TEMP(Checked_Temp, tmp0);
00631 DIRTY_TEMP(Checked_Temp, tmp1);
00632 DIRTY_TEMP(Checked_Temp, tmp2);
00633 return l_infinity_distance_assign(r, x, y, dir, tmp0, tmp1, tmp2);
00634 }
00635
00637 template <typename To, typename ITV>
00638 inline bool
00639 l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00640 const Box<ITV>& x,
00641 const Box<ITV>& y,
00642 const Rounding_Dir dir) {
00643 return l_infinity_distance_assign<To, To, ITV>(r, x, y, dir);
00644 }
00645
00646 }
00647
00648 #endif // !defined(PPL_Box_inlines_hh)