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_BD_Shape_inlines_hh
00024 #define PPL_BD_Shape_inlines_hh 1
00025
00026 #include "C_Polyhedron.defs.hh"
00027 #include "Poly_Con_Relation.defs.hh"
00028 #include "Poly_Gen_Relation.defs.hh"
00029 #include <cassert>
00030 #include <vector>
00031 #include <iostream>
00032 #include <algorithm>
00033
00034 namespace Parma_Polyhedra_Library {
00035
00036 namespace Implementation {
00037 namespace BD_Shapes {
00038
00039 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00041
00042 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00043 template <typename T, typename Policy>
00044 inline void
00045 numer_denom(const Checked_Number<T, Policy>& from,
00046 Coefficient& num, Coefficient& den) {
00047 assert(!is_not_a_number(from)
00048 && !is_minus_infinity(from)
00049 && !is_plus_infinity(from));
00050 mpq_class q;
00051 assign_r(q, from, ROUND_NOT_NEEDED);
00052 num = q.get_num();
00053 den = q.get_den();
00054 }
00055
00056 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00058
00059 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00060 template <typename T, typename Policy>
00061 inline void
00062 div_round_up(Checked_Number<T, Policy>& to,
00063 Coefficient_traits::const_reference x,
00064 Coefficient_traits::const_reference y) {
00065 mpq_class qx;
00066 mpq_class qy;
00067
00068
00069 assign_r(qx, x, ROUND_NOT_NEEDED);
00070 assign_r(qy, y, ROUND_NOT_NEEDED);
00071 div_assign_r(qx, qx, qy, ROUND_NOT_NEEDED);
00072 assign_r(to, qx, ROUND_UP);
00073 }
00074
00075 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00077
00078 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00079 template <typename N>
00080 inline void
00081 min_assign(N& x, const N& y) {
00082 if (x > y)
00083 x = y;
00084 }
00085
00086 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00088
00089 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00090 template <typename N>
00091 inline void
00092 max_assign(N& x, const N& y) {
00093 if (x < y)
00094 x = y;
00095 }
00096
00097 }
00098 }
00099
00100
00101 template <typename T>
00102 inline dimension_type
00103 BD_Shape<T>::max_space_dimension() {
00104
00105
00106 return std::min(DB_Matrix<N>::max_num_rows() - 1,
00107 DB_Matrix<N>::max_num_columns() - 1);
00108 }
00109
00110 template <typename T>
00111 inline bool
00112 BD_Shape<T>::marked_empty() const {
00113 return status.test_empty();
00114 }
00115
00116 template <typename T>
00117 inline void
00118 BD_Shape<T>::set_empty() {
00119 status.set_empty();
00120 assert(OK());
00121 assert(marked_empty());
00122 }
00123
00124 template <typename T>
00125 inline void
00126 BD_Shape<T>::set_zero_dim_univ() {
00127 status.set_zero_dim_univ();
00128 }
00129
00130 template <typename T>
00131 inline bool
00132 BD_Shape<T>::marked_shortest_path_closed() const {
00133 return status.test_shortest_path_closed();
00134 }
00135
00136 template <typename T>
00137 inline bool
00138 BD_Shape<T>::marked_shortest_path_reduced() const {
00139 return status.test_shortest_path_reduced();
00140 }
00141
00142 template <typename T>
00143 inline
00144 BD_Shape<T>::BD_Shape(const dimension_type num_dimensions,
00145 const Degenerate_Element kind)
00146 : dbm(num_dimensions + 1), status(), redundancy_dbm() {
00147 if (kind == EMPTY)
00148 set_empty();
00149 else {
00150 if (num_dimensions > 0)
00151
00152 status.set_shortest_path_closed();
00153 }
00154 assert(OK());
00155 }
00156
00157 template <typename T>
00158 inline
00159 BD_Shape<T>::BD_Shape(const BD_Shape& y)
00160 : dbm(y.dbm), status(y.status), redundancy_dbm() {
00161 if (y.marked_shortest_path_reduced())
00162 redundancy_dbm = y.redundancy_dbm;
00163 }
00164
00165 template <typename T>
00166 template <typename U>
00167 inline
00168 BD_Shape<T>::BD_Shape(const BD_Shape<U>& y)
00169 : dbm(y.dbm), status(), redundancy_dbm() {
00170
00171 if (y.marked_empty())
00172 set_empty();
00173 else if (y.status.test_zero_dim_univ())
00174 set_zero_dim_univ();
00175 }
00176
00177 template <typename T>
00178 inline bool
00179 BD_Shape<T>::add_constraint_and_minimize(const Constraint& c) {
00180 add_constraint(c);
00181 shortest_path_closure_assign();
00182 return !marked_empty();
00183 }
00184
00185 template <typename T>
00186 inline void
00187 BD_Shape<T>::add_constraints(const Constraint_System& cs) {
00188 for (Constraint_System::const_iterator i = cs.begin(),
00189 iend = cs.end(); i != iend; ++i)
00190 add_constraint(*i);
00191 assert(OK());
00192 }
00193
00194 template <typename T>
00195 inline bool
00196 BD_Shape<T>::add_constraints_and_minimize(const Constraint_System& cs) {
00197 add_constraints(cs);
00198 shortest_path_closure_assign();
00199 return !marked_empty();
00200 }
00201
00202 template <typename T>
00203 inline
00204 BD_Shape<T>::BD_Shape(const Constraint_System& cs)
00205 : dbm(cs.space_dimension() + 1), status(), redundancy_dbm() {
00206 if (cs.space_dimension() > 0)
00207
00208 status.set_shortest_path_closed();
00209 add_constraints(cs);
00210 assert(OK());
00211 }
00212
00213 template <typename T>
00214 inline dimension_type
00215 BD_Shape<T>::affine_dimension() const {
00216 const dimension_type space_dim = space_dimension();
00217
00218
00219
00220 shortest_path_closure_assign();
00221 if (marked_empty())
00222 return 0;
00223
00224
00225
00226
00227 std::vector<dimension_type> predecessor;
00228 compute_predecessors(predecessor);
00229
00230
00231
00232 dimension_type affine_dim = 0;
00233
00234 for (dimension_type i = 1; i <= space_dim; ++i)
00235 if (predecessor[i] == i)
00236 ++affine_dim;
00237
00238 return affine_dim;
00239 }
00240
00241 template <typename T>
00242 inline BD_Shape<T>&
00243 BD_Shape<T>::operator=(const BD_Shape& y) {
00244 dbm = y.dbm;
00245 status = y.status;
00246 if (y.marked_shortest_path_reduced())
00247 redundancy_dbm = y.redundancy_dbm;
00248 return *this;
00249 }
00250
00251 template <typename T>
00252 inline
00253 BD_Shape<T>::~BD_Shape() {
00254 }
00255
00256 template <typename T>
00257 inline void
00258 BD_Shape<T>::swap(BD_Shape& y) {
00259 std::swap(dbm, y.dbm);
00260 std::swap(status, y.status);
00261 std::swap(redundancy_dbm, y.redundancy_dbm);
00262 }
00263
00264 template <typename T>
00265 inline dimension_type
00266 BD_Shape<T>::space_dimension() const {
00267 return dbm.num_rows() - 1;
00268 }
00269
00270 template <typename T>
00271 inline bool
00272 BD_Shape<T>::is_empty() const {
00273 shortest_path_closure_assign();
00274 return marked_empty();
00275 }
00276
00277 template <typename T>
00278 inline bool
00279 operator==(const BD_Shape<T>& x, const BD_Shape<T>& y) {
00280 const dimension_type x_space_dim = x.space_dimension();
00281
00282 if (x_space_dim != y.space_dimension())
00283 return false;
00284
00285
00286 if (x_space_dim == 0)
00287 if (x.marked_empty())
00288 return y.marked_empty();
00289 else
00290 return !y.marked_empty();
00291
00292
00293 x.shortest_path_closure_assign();
00294 y.shortest_path_closure_assign();
00295
00296
00297
00298 if (x.marked_empty())
00299 return y.marked_empty();
00300 if (y.marked_empty())
00301 return false;
00302
00303
00304 return x.dbm == y.dbm;
00305 }
00306
00307 template <typename T>
00308 inline bool
00309 operator!=(const BD_Shape<T>& x, const BD_Shape<T>& y) {
00310 return !(x == y);
00311 }
00312
00314 template <typename Temp, typename To, typename T>
00315 inline bool
00316 rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00317 const BD_Shape<T>& x,
00318 const BD_Shape<T>& y,
00319 const Rounding_Dir dir,
00320 Temp& tmp0,
00321 Temp& tmp1,
00322 Temp& tmp2) {
00323 const dimension_type x_space_dim = x.space_dimension();
00324
00325 if (x_space_dim != y.space_dimension())
00326 return false;
00327
00328
00329 if (x_space_dim == 0) {
00330 if (x.marked_empty() == y.marked_empty())
00331 assign_r(r, 0, ROUND_NOT_NEEDED);
00332 else
00333 r = PLUS_INFINITY;
00334 return true;
00335 }
00336
00337
00338 x.shortest_path_closure_assign();
00339 y.shortest_path_closure_assign();
00340
00341
00342
00343 if (x.marked_empty() || y.marked_empty()) {
00344 if (x.marked_empty() == y.marked_empty())
00345 assign_r(r, 0, ROUND_NOT_NEEDED);
00346 else
00347 r = PLUS_INFINITY;
00348 return true;
00349 }
00350
00351 return rectilinear_distance_assign(r, x.dbm, y.dbm, dir, tmp0, tmp1, tmp2);
00352 }
00353
00355 template <typename Temp, typename To, typename T>
00356 inline bool
00357 rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00358 const BD_Shape<T>& x,
00359 const BD_Shape<T>& y,
00360 const Rounding_Dir dir) {
00361 static Checked_Number<Temp, Extended_Number_Policy> tmp0;
00362 static Checked_Number<Temp, Extended_Number_Policy> tmp1;
00363 static Checked_Number<Temp, Extended_Number_Policy> tmp2;
00364 return rectilinear_distance_assign(r, x, y, dir, tmp0, tmp1, tmp2);
00365 }
00366
00368 template <typename To, typename T>
00369 inline bool
00370 rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00371 const BD_Shape<T>& x,
00372 const BD_Shape<T>& y,
00373 const Rounding_Dir dir) {
00374 return rectilinear_distance_assign<To, To, T>(r, x, y, dir);
00375 }
00376
00378 template <typename Temp, typename To, typename T>
00379 inline bool
00380 euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00381 const BD_Shape<T>& x,
00382 const BD_Shape<T>& y,
00383 const Rounding_Dir dir,
00384 Temp& tmp0,
00385 Temp& tmp1,
00386 Temp& tmp2) {
00387 const dimension_type x_space_dim = x.space_dimension();
00388
00389 if (x_space_dim != y.space_dimension())
00390 return false;
00391
00392
00393 if (x_space_dim == 0) {
00394 if (x.marked_empty() == y.marked_empty())
00395 assign_r(r, 0, ROUND_NOT_NEEDED);
00396 else
00397 r = PLUS_INFINITY;
00398 return true;
00399 }
00400
00401
00402 x.shortest_path_closure_assign();
00403 y.shortest_path_closure_assign();
00404
00405
00406
00407 if (x.marked_empty() || y.marked_empty()) {
00408 if (x.marked_empty() == y.marked_empty())
00409 assign_r(r, 0, ROUND_NOT_NEEDED);
00410 else
00411 r = PLUS_INFINITY;
00412 return true;
00413 }
00414
00415 return euclidean_distance_assign(r, x.dbm, y.dbm, dir, tmp0, tmp1, tmp2);
00416 }
00417
00419 template <typename Temp, typename To, typename T>
00420 inline bool
00421 euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00422 const BD_Shape<T>& x,
00423 const BD_Shape<T>& y,
00424 const Rounding_Dir dir) {
00425 static Checked_Number<Temp, Extended_Number_Policy> tmp0;
00426 static Checked_Number<Temp, Extended_Number_Policy> tmp1;
00427 static Checked_Number<Temp, Extended_Number_Policy> tmp2;
00428 return euclidean_distance_assign(r, x, y, dir, tmp0, tmp1, tmp2);
00429 }
00430
00432 template <typename To, typename T>
00433 inline bool
00434 euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00435 const BD_Shape<T>& x,
00436 const BD_Shape<T>& y,
00437 const Rounding_Dir dir) {
00438 return euclidean_distance_assign<To, To, T>(r, x, y, dir);
00439 }
00440
00442 template <typename Temp, typename To, typename T>
00443 inline bool
00444 l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00445 const BD_Shape<T>& x,
00446 const BD_Shape<T>& y,
00447 const Rounding_Dir dir,
00448 Temp& tmp0,
00449 Temp& tmp1,
00450 Temp& tmp2) {
00451 const dimension_type x_space_dim = x.space_dimension();
00452
00453 if (x_space_dim != y.space_dimension())
00454 return false;
00455
00456
00457 if (x_space_dim == 0) {
00458 if (x.marked_empty() == y.marked_empty())
00459 assign_r(r, 0, ROUND_NOT_NEEDED);
00460 else
00461 r = PLUS_INFINITY;
00462 return true;
00463 }
00464
00465
00466 x.shortest_path_closure_assign();
00467 y.shortest_path_closure_assign();
00468
00469
00470
00471 if (x.marked_empty() || y.marked_empty()) {
00472 if (x.marked_empty() == y.marked_empty())
00473 assign_r(r, 0, ROUND_NOT_NEEDED);
00474 else
00475 r = PLUS_INFINITY;
00476 return true;
00477 }
00478
00479 return l_infinity_distance_assign(r, x.dbm, y.dbm, dir, tmp0, tmp1, tmp2);
00480 }
00481
00483 template <typename Temp, typename To, typename T>
00484 inline bool
00485 l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00486 const BD_Shape<T>& x,
00487 const BD_Shape<T>& y,
00488 const Rounding_Dir dir) {
00489 static Checked_Number<Temp, Extended_Number_Policy> tmp0;
00490 static Checked_Number<Temp, Extended_Number_Policy> tmp1;
00491 static Checked_Number<Temp, Extended_Number_Policy> tmp2;
00492 return l_infinity_distance_assign(r, x, y, dir, tmp0, tmp1, tmp2);
00493 }
00494
00496 template <typename To, typename T>
00497 inline bool
00498 l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00499 const BD_Shape<T>& x,
00500 const BD_Shape<T>& y,
00501 const Rounding_Dir dir) {
00502 return l_infinity_distance_assign<To, To, T>(r, x, y, dir);
00503 }
00504
00505 template <typename T>
00506 inline void
00507 BD_Shape<T>::add_dbm_constraint(const dimension_type i,
00508 const dimension_type j,
00509 N k) {
00510
00511 assert(i <= space_dimension() && j <= space_dimension() && i != j);
00512 N& dbm_ij = dbm[i][j];
00513 if (dbm_ij > k) {
00514 dbm_ij = k;
00515 if (marked_shortest_path_closed())
00516 status.reset_shortest_path_closed();
00517 }
00518 assert(OK());
00519 }
00520
00521 template <typename T>
00522 inline void
00523 BD_Shape<T>::add_dbm_constraint(const dimension_type i,
00524 const dimension_type j,
00525 Coefficient_traits::const_reference num,
00526 Coefficient_traits::const_reference den) {
00527
00528 assert(i <= space_dimension() && j <= space_dimension() && i != j);
00529 assert(den != 0);
00530 N k;
00531 Implementation::BD_Shapes::div_round_up(k, num, den);
00532 add_dbm_constraint(i, j, k);
00533 }
00534
00535 template <typename T>
00536 inline bool
00537 BD_Shape<T>::strictly_contains(const BD_Shape& y) const {
00538 const BD_Shape<T>& x = *this;
00539 return x.contains(y) && !y.contains(x);
00540 }
00541
00542 template <typename T>
00543 inline bool
00544 BD_Shape<T>::bds_hull_assign_and_minimize(const BD_Shape& y) {
00545 bds_hull_assign(y);
00546 assert(marked_empty()
00547 || space_dimension() == 0 || marked_shortest_path_closed());
00548 return !marked_empty();
00549 }
00550
00551 template <typename T>
00552 inline void
00553 BD_Shape<T>::upper_bound_assign(const BD_Shape& y) {
00554 bds_hull_assign(y);
00555 }
00556
00557 template <typename T>
00558 inline bool
00559 BD_Shape<T>::bds_hull_assign_if_exact(const BD_Shape&) {
00560
00561 return false;
00562 }
00563
00564 template <typename T>
00565 inline bool
00566 BD_Shape<T>::upper_bound_assign_if_exact(const BD_Shape& y) {
00567 return bds_hull_assign_if_exact(y);
00568 }
00569
00570 template <typename T>
00571 inline void
00572 BD_Shape<T>::difference_assign(const BD_Shape& y) {
00573 bds_difference_assign(y);
00574 }
00575
00576 template <typename T>
00577 inline void
00578 BD_Shape<T>::remove_higher_space_dimensions(const dimension_type new_dim) {
00579
00580
00581 if (new_dim > space_dimension())
00582 throw_dimension_incompatible("remove_higher_space_dimensions(nd)",
00583 new_dim);
00584
00585
00586
00587
00588 if (new_dim == space_dimension()) {
00589 assert(OK());
00590 return;
00591 }
00592
00593
00594 shortest_path_closure_assign();
00595 dbm.resize_no_copy(new_dim + 1);
00596
00597
00598
00599 if (marked_shortest_path_reduced())
00600 status.reset_shortest_path_reduced();
00601
00602
00603
00604 if (new_dim == 0 && !marked_empty())
00605 set_zero_dim_univ();
00606 assert(OK());
00607 }
00608
00609 template <typename T>
00610 inline bool
00611 BD_Shape<T>::intersection_assign_and_minimize(const BD_Shape& y) {
00612 intersection_assign(y);
00613 shortest_path_closure_assign();
00614 return !marked_empty();
00615 }
00616
00617 template <typename T>
00618 inline void
00619 BD_Shape<T>::CC76_extrapolation_assign(const BD_Shape& y, unsigned* tp) {
00620 static N stop_points[] = {
00621 N(-2, ROUND_UP),
00622 N(-1, ROUND_UP),
00623 N( 0, ROUND_UP),
00624 N( 1, ROUND_UP),
00625 N( 2, ROUND_UP)
00626 };
00627 CC76_extrapolation_assign(y,
00628 stop_points,
00629 stop_points
00630 + sizeof(stop_points)/sizeof(stop_points[0]),
00631 tp);
00632 }
00633
00634 template <typename T>
00635 inline void
00636 BD_Shape<T>::H79_widening_assign(const BD_Shape& y, unsigned* tp) {
00637
00638 C_Polyhedron px(constraints());
00639 C_Polyhedron py(y.constraints());
00640 px.H79_widening_assign(py, tp);
00641 BD_Shape x(px);
00642 swap(x);
00643 assert(OK());
00644 }
00645
00646 template <typename T>
00647 inline void
00648 BD_Shape<T>::limited_H79_extrapolation_assign(const BD_Shape& y,
00649 const Constraint_System& cs,
00650 unsigned* tp) {
00651
00652 C_Polyhedron px(constraints());
00653 C_Polyhedron py(y.constraints());
00654 px.limited_H79_extrapolation_assign(py, cs, tp);
00655 BD_Shape x(px);
00656 swap(x);
00657 assert(OK());
00658 }
00659
00660 template <typename T>
00661 inline void
00662 BD_Shape<T>::time_elapse_assign(const BD_Shape& y) {
00663
00664 if (space_dimension() != y.space_dimension())
00665 throw_dimension_incompatible("time_elapse_assign(y)", y);
00666
00667 C_Polyhedron px(constraints());
00668 C_Polyhedron py(y.constraints());
00669 px.time_elapse_assign(py);
00670 BD_Shape x(px);
00671 swap(x);
00672 assert(OK());
00673 }
00674
00675 template <typename T>
00676 inline void
00677 BD_Shape<T>::forget_all_dbm_constraints(const dimension_type v) {
00678 assert(0 < v && v <= dbm.num_rows());
00679 DB_Row<N>& dbm_v = dbm[v];
00680 for (dimension_type i = dbm.num_rows(); i-- > 0; ) {
00681 dbm_v[i] = PLUS_INFINITY;
00682 dbm[i][v] = PLUS_INFINITY;
00683 }
00684 }
00685
00686 template <typename T>
00687 inline void
00688 BD_Shape<T>::forget_binary_dbm_constraints(const dimension_type v) {
00689 assert(0 < v && v <= dbm.num_rows());
00690 DB_Row<N>& dbm_v = dbm[v];
00691 for (dimension_type i = dbm.num_rows()-1; i > 0; --i) {
00692 dbm_v[i] = PLUS_INFINITY;
00693 dbm[i][v] = PLUS_INFINITY;
00694 }
00695 }
00696
00697 }
00698
00699 namespace std {
00700
00702 template <typename T>
00703 inline void
00704 swap(Parma_Polyhedra_Library::BD_Shape<T>& x,
00705 Parma_Polyhedra_Library::BD_Shape<T>& y) {
00706 x.swap(y);
00707 }
00708
00709 }
00710
00711 #endif // !defined(PPL_BD_Shape_inlines_hh)