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_defs_hh
00024 #define PPL_BD_Shape_defs_hh 1
00025
00026 #include "BD_Shape.types.hh"
00027 #include "globals.defs.hh"
00028 #include "Constraint.types.hh"
00029 #include "Generator.types.hh"
00030 #include "Linear_Expression.types.hh"
00031 #include "Constraint_System.types.hh"
00032 #include "Generator_System.types.hh"
00033 #include "Poly_Con_Relation.types.hh"
00034 #include "Poly_Gen_Relation.types.hh"
00035 #include "Polyhedron.types.hh"
00036 #include "Variable.defs.hh"
00037 #include "DB_Matrix.defs.hh"
00038 #include "DB_Row.defs.hh"
00039 #include "Checked_Number.defs.hh"
00040 #include <cstddef>
00041 #include <iosfwd>
00042 #include <vector>
00043 #include <deque>
00044
00045
00046 namespace Parma_Polyhedra_Library {
00047
00048 namespace IO_Operators {
00049
00051
00058 template <typename T>
00059 std::ostream&
00060 operator<<(std::ostream& s, const BD_Shape<T>& bds);
00061
00062 }
00063
00065
00070 template <typename T>
00071 bool operator==(const BD_Shape<T>& x, const BD_Shape<T>& y);
00072
00074
00079 template <typename T>
00080 bool operator!=(const BD_Shape<T>& x, const BD_Shape<T>& y);
00081
00083
00093 template <typename To, typename T>
00094 bool rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00095 const BD_Shape<T>& x,
00096 const BD_Shape<T>& y,
00097 const Rounding_Dir dir);
00098
00100
00110 template <typename Temp, typename To, typename T>
00111 bool rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00112 const BD_Shape<T>& x,
00113 const BD_Shape<T>& y,
00114 const Rounding_Dir dir);
00115
00117
00127 template <typename Temp, typename To, typename T>
00128 bool rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00129 const BD_Shape<T>& x,
00130 const BD_Shape<T>& y,
00131 const Rounding_Dir dir,
00132 Temp& tmp0,
00133 Temp& tmp1,
00134 Temp& tmp2);
00135
00137
00147 template <typename To, typename T>
00148 bool euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00149 const BD_Shape<T>& x,
00150 const BD_Shape<T>& y,
00151 const Rounding_Dir dir);
00152
00154
00164 template <typename Temp, typename To, typename T>
00165 bool euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00166 const BD_Shape<T>& x,
00167 const BD_Shape<T>& y,
00168 const Rounding_Dir dir);
00169
00171
00181 template <typename Temp, typename To, typename T>
00182 bool euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00183 const BD_Shape<T>& x,
00184 const BD_Shape<T>& y,
00185 const Rounding_Dir dir,
00186 Temp& tmp0,
00187 Temp& tmp1,
00188 Temp& tmp2);
00189
00191
00201 template <typename To, typename T>
00202 bool l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00203 const BD_Shape<T>& x,
00204 const BD_Shape<T>& y,
00205 const Rounding_Dir dir);
00206
00208
00218 template <typename Temp, typename To, typename T>
00219 bool l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00220 const BD_Shape<T>& x,
00221 const BD_Shape<T>& y,
00222 const Rounding_Dir dir);
00223
00225
00235 template <typename Temp, typename To, typename T>
00236 bool l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00237 const BD_Shape<T>& x,
00238 const BD_Shape<T>& y,
00239 const Rounding_Dir dir,
00240 Temp& tmp0,
00241 Temp& tmp1,
00242 Temp& tmp2);
00243
00244 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00246
00279 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00280 bool extract_bounded_difference(const Constraint& c,
00281 const dimension_type c_space_dim,
00282 dimension_type& c_num_vars,
00283 dimension_type& c_first_var,
00284 dimension_type& c_second_var,
00285 Coefficient& c_coeff);
00286
00287 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00289 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00290 void compute_leader_indices(const std::vector<dimension_type>& predecessor,
00291 std::vector<dimension_type>& indices);
00292
00293 }
00294
00296
00387 template <typename T>
00388 class Parma_Polyhedra_Library::BD_Shape {
00389 private:
00394 typedef Checked_Number<T, Extended_Number_Policy> N;
00395
00396 public:
00398 typedef T base_type;
00399
00404 typedef N coefficient_type;
00405
00407 static dimension_type max_space_dimension();
00408
00410
00411
00413
00420 explicit BD_Shape(dimension_type num_dimensions = 0,
00421 Degenerate_Element kind = UNIVERSE);
00422
00424 BD_Shape(const BD_Shape& y);
00425
00427 template <typename U>
00428 explicit BD_Shape(const BD_Shape<U>& y);
00429
00431
00443 BD_Shape(const Constraint_System& cs);
00444
00446
00453 BD_Shape(const Generator_System& gs);
00454
00456
00462 BD_Shape(const Polyhedron& ph, Complexity_Class complexity = ANY_COMPLEXITY);
00463
00468 BD_Shape& operator=(const BD_Shape& y);
00469
00474 void swap(BD_Shape& y);
00475
00477 ~BD_Shape();
00478
00480
00482
00483
00485 dimension_type space_dimension() const;
00486
00492 dimension_type affine_dimension() const;
00493
00495 Constraint_System constraints() const;
00496
00498 Constraint_System minimized_constraints() const;
00499
00501
00505 bool contains(const BD_Shape& y) const;
00506
00508
00512 bool strictly_contains(const BD_Shape& y) const;
00513
00515
00521 Poly_Con_Relation relation_with(const Constraint& c) const;
00522
00524
00528 Poly_Gen_Relation relation_with(const Generator& g) const;
00529
00531 bool is_empty() const;
00532
00534 bool is_universe() const;
00535
00540 bool OK() const;
00541
00543
00545
00546
00559 void add_constraint(const Constraint& c);
00560
00576 bool add_constraint_and_minimize(const Constraint& c);
00577
00590 void add_constraints(const Constraint_System& cs);
00591
00607 bool add_constraints_and_minimize(const Constraint_System& cs);
00608
00610
00614 void intersection_assign(const BD_Shape& y);
00615
00617
00624 bool intersection_assign_and_minimize(const BD_Shape& y);
00625
00633 void bds_hull_assign(const BD_Shape& y);
00634
00645 bool bds_hull_assign_and_minimize(const BD_Shape& y);
00646
00648 void upper_bound_assign(const BD_Shape& y);
00649
00658 bool bds_hull_assign_if_exact(const BD_Shape& y);
00659
00661 bool upper_bound_assign_if_exact(const BD_Shape& y);
00662
00671 void bds_difference_assign(const BD_Shape& y);
00672
00674 void difference_assign(const BD_Shape& y);
00675
00695 void affine_image(Variable var,
00696 const Linear_Expression& expr,
00697 Coefficient_traits::const_reference denominator
00698 = Coefficient_one());
00699
00719 void affine_preimage(Variable var,
00720 const Linear_Expression& expr,
00721 Coefficient_traits::const_reference denominator
00722 = Coefficient_one());
00723
00748 void generalized_affine_image(Variable var,
00749 Relation_Symbol relsym,
00750 const Linear_Expression& expr,
00751 Coefficient_traits::const_reference denominator
00752 = Coefficient_one());
00753
00773 void generalized_affine_image(const Linear_Expression& lhs,
00774 Relation_Symbol relsym,
00775 const Linear_Expression& rhs);
00776
00801 void generalized_affine_preimage(Variable var,
00802 Relation_Symbol relsym,
00803 const Linear_Expression& expr,
00804 Coefficient_traits::const_reference
00805 denominator = Coefficient_one());
00806
00814 void time_elapse_assign(const BD_Shape& y);
00815
00831 void CC76_extrapolation_assign(const BD_Shape& y, unsigned* tp = 0);
00832
00854 template <typename Iterator>
00855 void CC76_extrapolation_assign(const BD_Shape& y,
00856 Iterator first, Iterator last,
00857 unsigned* tp = 0);
00858
00874 void BHMZ05_widening_assign(const BD_Shape& y, unsigned* tp = 0);
00875
00896 void limited_BHMZ05_extrapolation_assign(const BD_Shape& y,
00897 const Constraint_System& cs,
00898 unsigned* tp = 0);
00899
00919 void CC76_narrowing_assign(const BD_Shape& y);
00920
00941 void limited_CC76_extrapolation_assign(const BD_Shape& y,
00942 const Constraint_System& cs,
00943 unsigned* tp = 0);
00944
00960 void H79_widening_assign(const BD_Shape& y, unsigned* tp = 0);
00961
00981 void limited_H79_extrapolation_assign(const BD_Shape& y,
00982 const Constraint_System& cs,
00983 unsigned* tp = 0);
00984
00986
00988
00989
00991
01008 void add_space_dimensions_and_embed(dimension_type m);
01009
01031 void add_space_dimensions_and_project(dimension_type m);
01032
01056 void concatenate_assign(const BD_Shape& y);
01057
01059
01067 void remove_space_dimensions(const Variables_Set& to_be_removed);
01068
01077 void remove_higher_space_dimensions(dimension_type new_dimension);
01078
01116 template <typename PartialFunction>
01117 void map_space_dimensions(const PartialFunction& pfunc);
01118
01120
01121 PPL_OUTPUT_DECLARATIONS;
01122
01123 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
01124
01129 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
01130 bool ascii_load(std::istream& s);
01131
01132 friend bool Parma_Polyhedra_Library::operator==<T>(const BD_Shape<T>& x,
01133 const BD_Shape<T>& y);
01134 template <typename Temp, typename To, typename U>
01135 friend bool Parma_Polyhedra_Library::rectilinear_distance_assign
01136 (Checked_Number<To, Extended_Number_Policy>& r,
01137 const BD_Shape<U>& x, const BD_Shape<U>& y, const Rounding_Dir dir,
01138 Temp& tmp0, Temp& tmp1, Temp& tmp2);
01139 template <typename Temp, typename To, typename U>
01140 friend bool Parma_Polyhedra_Library::euclidean_distance_assign
01141 (Checked_Number<To, Extended_Number_Policy>& r,
01142 const BD_Shape<U>& x, const BD_Shape<U>& y, const Rounding_Dir dir,
01143 Temp& tmp0, Temp& tmp1, Temp& tmp2);
01144 template <typename Temp, typename To, typename U>
01145 friend bool Parma_Polyhedra_Library::l_infinity_distance_assign
01146 (Checked_Number<To, Extended_Number_Policy>& r,
01147 const BD_Shape<U>& x, const BD_Shape<U>& y, const Rounding_Dir dir,
01148 Temp& tmp0, Temp& tmp1, Temp& tmp2);
01149
01150 private:
01151 template <typename U> friend class Parma_Polyhedra_Library::BD_Shape;
01152
01154 DB_Matrix<N> dbm;
01155
01156 #define PPL_IN_BD_Shape_CLASS
01157 #include "BDS_Status.idefs.hh"
01158 #undef PPL_IN_BD_Shape_CLASS
01159
01161 Status status;
01162
01164 std::vector<std::deque<bool> > redundancy_dbm;
01165
01167
01171 bool marked_empty()const;
01172
01180 bool marked_shortest_path_closed()const;
01181
01189 bool marked_shortest_path_reduced()const;
01190
01192 void set_empty();
01193
01195 void set_zero_dim_univ();
01196
01198 void shortest_path_closure_assign() const;
01199
01205 void shortest_path_reduction_assign() const;
01206
01212 bool is_shortest_path_reduced() const;
01213
01215 void add_dbm_constraint(dimension_type i, dimension_type j, N k);
01217 void add_dbm_constraint(dimension_type i, dimension_type j,
01218 Coefficient_traits::const_reference num,
01219 Coefficient_traits::const_reference den);
01220
01222 void forget_all_dbm_constraints(dimension_type v);
01224 void forget_binary_dbm_constraints(dimension_type v);
01225
01227
01241 void deduce_v_minus_u_bounds(dimension_type v,
01242 dimension_type last_v,
01243 const Linear_Expression& sc_expr,
01244 Coefficient_traits::const_reference sc_den,
01245 const N& pos_sum);
01246
01248
01263 void deduce_u_minus_v_bounds(dimension_type v,
01264 dimension_type last_v,
01265 const Linear_Expression& sc_expr,
01266 Coefficient_traits::const_reference sc_den,
01267 const N& neg_sum);
01268
01273 void get_limiting_shape(const Constraint_System& cs,
01274 BD_Shape& limiting_shape) const;
01275
01277
01280 void compute_predecessors(std::vector<dimension_type>& predecessor) const;
01281
01283
01286 void compute_leaders(std::vector<dimension_type>& leaders) const;
01287
01288 #if !defined(__GNUC__) || __GNUC__ > 3 || (__GNUC__ == 3 && __GNUC_MINOR__ > 3)
01289 friend std::ostream&
01290 Parma_Polyhedra_Library::IO_Operators::operator<<<>(std::ostream& s,
01291 const BD_Shape<T>& c);
01292 #else
01293
01294 template <typename U>
01295 friend std::ostream&
01296 Parma_Polyhedra_Library::IO_Operators::operator<<(std::ostream& s,
01297 const BD_Shape<U>& c);
01298 #endif
01299
01301
01302 void throw_dimension_incompatible(const char* method,
01303 const BD_Shape& x) const;
01304
01305 void throw_dimension_incompatible(const char* method,
01306 dimension_type required_dim) const;
01307
01308 void throw_dimension_incompatible(const char* method,
01309 const Constraint& c) const;
01310
01311 void throw_dimension_incompatible(const char* method,
01312 const Generator& g) const;
01313
01314 void throw_dimension_incompatible(const char* method,
01315 const char* name_row,
01316 const Linear_Expression& y) const;
01317
01318 static void throw_constraint_incompatible(const char* method);
01319
01320 static void throw_expression_too_complex(const char* method,
01321 const Linear_Expression& e);
01322
01323 static void throw_generic(const char* method, const char* reason);
01325 };
01326
01327
01328 namespace std {
01329
01331
01332 template <typename T>
01333 void swap(Parma_Polyhedra_Library::BD_Shape<T>& x,
01334 Parma_Polyhedra_Library::BD_Shape<T>& y);
01335
01336 }
01337
01338 #include "BDS_Status.inlines.hh"
01339 #include "BD_Shape.inlines.hh"
01340 #include "BD_Shape.templates.hh"
01341
01342 #endif // !defined(PPL_BD_Shape_defs_hh)