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 "Congruence.types.hh"
00031 #include "Linear_Expression.types.hh"
00032 #include "Constraint_System.types.hh"
00033 #include "Generator_System.types.hh"
00034 #include "Congruence_System.types.hh"
00035 #include "Poly_Con_Relation.types.hh"
00036 #include "Poly_Gen_Relation.types.hh"
00037 #include "Polyhedron.types.hh"
00038 #include "Box.types.hh"
00039 #include "Grid.types.hh"
00040 #include "Octagonal_Shape.types.hh"
00041 #include "Variable.defs.hh"
00042 #include "Variables_Set.types.hh"
00043 #include "DB_Matrix.defs.hh"
00044 #include "DB_Row.defs.hh"
00045 #include "Checked_Number.defs.hh"
00046 #include "Bit_Matrix.defs.hh"
00047 #include <cstddef>
00048 #include <iosfwd>
00049 #include <vector>
00050
00051 namespace Parma_Polyhedra_Library {
00052
00053 namespace IO_Operators {
00054
00056
00063 template <typename T>
00064 std::ostream&
00065 operator<<(std::ostream& s, const BD_Shape<T>& bds);
00066
00067 }
00068
00070
00074 template <typename T>
00075 bool operator==(const BD_Shape<T>& x, const BD_Shape<T>& y);
00076
00078
00082 template <typename T>
00083 bool operator!=(const BD_Shape<T>& x, const BD_Shape<T>& y);
00084
00086
00096 template <typename To, typename T>
00097 bool rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00098 const BD_Shape<T>& x,
00099 const BD_Shape<T>& y,
00100 Rounding_Dir dir);
00101
00103
00113 template <typename Temp, typename To, typename T>
00114 bool rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00115 const BD_Shape<T>& x,
00116 const BD_Shape<T>& y,
00117 Rounding_Dir dir);
00118
00120
00130 template <typename Temp, typename To, typename T>
00131 bool rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00132 const BD_Shape<T>& x,
00133 const BD_Shape<T>& y,
00134 Rounding_Dir dir,
00135 Temp& tmp0,
00136 Temp& tmp1,
00137 Temp& tmp2);
00138
00140
00150 template <typename To, typename T>
00151 bool euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00152 const BD_Shape<T>& x,
00153 const BD_Shape<T>& y,
00154 Rounding_Dir dir);
00155
00157
00167 template <typename Temp, typename To, typename T>
00168 bool euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00169 const BD_Shape<T>& x,
00170 const BD_Shape<T>& y,
00171 Rounding_Dir dir);
00172
00174
00184 template <typename Temp, typename To, typename T>
00185 bool euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00186 const BD_Shape<T>& x,
00187 const BD_Shape<T>& y,
00188 Rounding_Dir dir,
00189 Temp& tmp0,
00190 Temp& tmp1,
00191 Temp& tmp2);
00192
00194
00204 template <typename To, typename T>
00205 bool l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00206 const BD_Shape<T>& x,
00207 const BD_Shape<T>& y,
00208 Rounding_Dir dir);
00209
00211
00221 template <typename Temp, typename To, typename T>
00222 bool l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00223 const BD_Shape<T>& x,
00224 const BD_Shape<T>& y,
00225 Rounding_Dir dir);
00226
00228
00238 template <typename Temp, typename To, typename T>
00239 bool l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00240 const BD_Shape<T>& x,
00241 const BD_Shape<T>& y,
00242 Rounding_Dir dir,
00243 Temp& tmp0,
00244 Temp& tmp1,
00245 Temp& tmp2);
00246
00247 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00249
00282 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
00283 bool extract_bounded_difference(const Constraint& c,
00284 dimension_type c_space_dim,
00285 dimension_type& c_num_vars,
00286 dimension_type& c_first_var,
00287 dimension_type& c_second_var,
00288 Coefficient& c_coeff);
00289
00290 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00292
00293 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
00294 void compute_leader_indices(const std::vector<dimension_type>& predecessor,
00295 std::vector<dimension_type>& indices);
00296
00297 }
00298
00300
00391 template <typename T>
00392 class Parma_Polyhedra_Library::BD_Shape {
00393 private:
00398 typedef Checked_Number<T, Extended_Number_Policy> N;
00399
00400 public:
00402 typedef T coefficient_type_base;
00403
00408 typedef N coefficient_type;
00409
00411 static dimension_type max_space_dimension();
00412
00416 static bool can_recycle_constraint_systems();
00417
00421 static bool can_recycle_congruence_systems();
00422
00424
00425
00427
00434 explicit BD_Shape(dimension_type num_dimensions = 0,
00435 Degenerate_Element kind = UNIVERSE);
00436
00438
00441 BD_Shape(const BD_Shape& y,
00442 Complexity_Class complexity = ANY_COMPLEXITY);
00443
00445
00448 template <typename U>
00449 explicit BD_Shape(const BD_Shape<U>& y,
00450 Complexity_Class complexity = ANY_COMPLEXITY);
00451
00453
00465 explicit BD_Shape(const Constraint_System& cs);
00466
00468
00474 explicit BD_Shape(const Congruence_System& cgs);
00475
00477
00484 explicit BD_Shape(const Generator_System& gs);
00485
00487
00493 explicit BD_Shape(const Polyhedron& ph,
00494 Complexity_Class complexity = ANY_COMPLEXITY);
00495
00497
00512 template <typename Interval>
00513 explicit BD_Shape(const Box<Interval>& box,
00514 Complexity_Class complexity = ANY_COMPLEXITY);
00515
00517
00532 explicit BD_Shape(const Grid& grid,
00533 Complexity_Class complexity = ANY_COMPLEXITY);
00534
00536
00551 template <typename U>
00552 explicit BD_Shape(const Octagonal_Shape<U>& os,
00553 Complexity_Class complexity = ANY_COMPLEXITY);
00554
00559 BD_Shape& operator=(const BD_Shape& y);
00560
00565 void swap(BD_Shape& y);
00566
00568 ~BD_Shape();
00569
00571
00573
00574
00576 dimension_type space_dimension() const;
00577
00583 dimension_type affine_dimension() const;
00584
00586 Constraint_System constraints() const;
00587
00589 Constraint_System minimized_constraints() const;
00590
00592 Congruence_System congruences() const;
00593
00598 Congruence_System minimized_congruences() const;
00599
00607 bool bounds_from_above(const Linear_Expression& expr) const;
00608
00616 bool bounds_from_below(const Linear_Expression& expr) const;
00617
00642 bool maximize(const Linear_Expression& expr,
00643 Coefficient& sup_n, Coefficient& sup_d, bool& maximum) const;
00644
00673 bool maximize(const Linear_Expression& expr,
00674 Coefficient& sup_n, Coefficient& sup_d, bool& maximum,
00675 Generator& g) const;
00676
00701 bool minimize(const Linear_Expression& expr,
00702 Coefficient& inf_n, Coefficient& inf_d, bool& minimum) const;
00703
00732 bool minimize(const Linear_Expression& expr,
00733 Coefficient& inf_n, Coefficient& inf_d, bool& minimum,
00734 Generator& g) const;
00735
00737
00741 bool contains(const BD_Shape& y) const;
00742
00744
00748 bool strictly_contains(const BD_Shape& y) const;
00749
00751
00756 bool is_disjoint_from(const BD_Shape& y) const;
00757
00759
00763 Poly_Con_Relation relation_with(const Constraint& c) const;
00764
00766
00770 Poly_Con_Relation relation_with(const Congruence& cg) const;
00771
00773
00777 Poly_Gen_Relation relation_with(const Generator& g) const;
00778
00780 bool is_empty() const;
00781
00783 bool is_universe() const;
00784
00786 bool is_discrete() const;
00787
00792 bool is_topologically_closed() const;
00793
00795 bool is_bounded() const;
00796
00801 bool contains_integer_point() const;
00802
00810 bool constrains(Variable var) const;
00811
00816 bool OK() const;
00817
00819
00821
00822
00835 void add_constraint(const Constraint& c);
00836
00855 bool add_constraint_and_minimize(const Constraint& c);
00856
00868 void add_congruence(const Congruence& cg);
00869
00888 bool add_congruence_and_minimize(const Congruence& cg);
00889
00902 void add_constraints(const Constraint_System& cs);
00903
00920 void add_recycled_constraints(Constraint_System& cs);
00921
00940 bool add_constraints_and_minimize(const Constraint_System& cs);
00941
00964 bool add_recycled_constraints_and_minimize(Constraint_System& cs);
00965
00978 void add_congruences(const Congruence_System& cgs);
00979
00997 bool add_congruences_and_minimize(const Congruence_System& cs);
00998
00999
01015 void add_recycled_congruences(Congruence_System& cgs);
01016
01017
01039 bool add_recycled_congruences_and_minimize(Congruence_System& cgs);
01040
01051 void refine_with_constraint(const Constraint& c);
01052
01064 void refine_with_congruence(const Congruence& cg);
01065
01077 void refine_with_constraints(const Constraint_System& cs);
01078
01090 void refine_with_congruences(const Congruence_System& cgs);
01091
01102 void unconstrain(Variable var);
01103
01116 void unconstrain(const Variables_Set& to_be_unconstrained);
01117
01119
01123 void intersection_assign(const BD_Shape& y);
01124
01126
01136 bool intersection_assign_and_minimize(const BD_Shape& y);
01137
01145 void upper_bound_assign(const BD_Shape& y);
01146
01160 bool upper_bound_assign_and_minimize(const BD_Shape& y);
01161
01170 bool upper_bound_assign_if_exact(const BD_Shape& y);
01171
01179 void difference_assign(const BD_Shape& y);
01180
01190 bool simplify_using_context_assign(const BD_Shape& y);
01191
01211 void affine_image(Variable var,
01212 const Linear_Expression& expr,
01213 Coefficient_traits::const_reference denominator
01214 = Coefficient_one());
01215
01235 void affine_preimage(Variable var,
01236 const Linear_Expression& expr,
01237 Coefficient_traits::const_reference denominator
01238 = Coefficient_one());
01239
01264 void generalized_affine_image(Variable var,
01265 Relation_Symbol relsym,
01266 const Linear_Expression& expr,
01267 Coefficient_traits::const_reference denominator
01268 = Coefficient_one());
01269
01289 void generalized_affine_image(const Linear_Expression& lhs,
01290 Relation_Symbol relsym,
01291 const Linear_Expression& rhs);
01292
01317 void generalized_affine_preimage(Variable var,
01318 Relation_Symbol relsym,
01319 const Linear_Expression& expr,
01320 Coefficient_traits::const_reference
01321 denominator = Coefficient_one());
01322
01342 void generalized_affine_preimage(const Linear_Expression& lhs,
01343 Relation_Symbol relsym,
01344 const Linear_Expression& rhs);
01345
01372 void bounded_affine_image(Variable var,
01373 const Linear_Expression& lb_expr,
01374 const Linear_Expression& ub_expr,
01375 Coefficient_traits::const_reference denominator
01376 = Coefficient_one());
01377
01404 void bounded_affine_preimage(Variable var,
01405 const Linear_Expression& lb_expr,
01406 const Linear_Expression& ub_expr,
01407 Coefficient_traits::const_reference denominator
01408 = Coefficient_one());
01416 void time_elapse_assign(const BD_Shape& y);
01417
01419 void topological_closure_assign();
01420
01436 void CC76_extrapolation_assign(const BD_Shape& y, unsigned* tp = 0);
01437
01459 template <typename Iterator>
01460 void CC76_extrapolation_assign(const BD_Shape& y,
01461 Iterator first, Iterator last,
01462 unsigned* tp = 0);
01463
01479 void BHMZ05_widening_assign(const BD_Shape& y, unsigned* tp = 0);
01480
01501 void limited_BHMZ05_extrapolation_assign(const BD_Shape& y,
01502 const Constraint_System& cs,
01503 unsigned* tp = 0);
01504
01524 void CC76_narrowing_assign(const BD_Shape& y);
01525
01546 void limited_CC76_extrapolation_assign(const BD_Shape& y,
01547 const Constraint_System& cs,
01548 unsigned* tp = 0);
01549
01565 void H79_widening_assign(const BD_Shape& y, unsigned* tp = 0);
01566
01568 void widening_assign(const BD_Shape& y, unsigned* tp = 0);
01569
01589 void limited_H79_extrapolation_assign(const BD_Shape& y,
01590 const Constraint_System& cs,
01591 unsigned* tp = 0);
01592
01594
01596
01597
01599
01616 void add_space_dimensions_and_embed(dimension_type m);
01617
01639 void add_space_dimensions_and_project(dimension_type m);
01640
01649 void concatenate_assign(const BD_Shape& y);
01650
01652
01660 void remove_space_dimensions(const Variables_Set& to_be_removed);
01661
01670 void remove_higher_space_dimensions(dimension_type new_dimension);
01671
01709 template <typename Partial_Function>
01710 void map_space_dimensions(const Partial_Function& pfunc);
01711
01713
01733 void expand_space_dimension(Variable var, dimension_type m);
01734
01736
01758 void fold_space_dimensions(const Variables_Set& to_be_folded, Variable var);
01759
01761
01762 PPL_OUTPUT_DECLARATIONS
01763
01764 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
01765
01770 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
01771 bool ascii_load(std::istream& s);
01772
01774 memory_size_type total_memory_in_bytes() const;
01775
01777 memory_size_type external_memory_in_bytes() const;
01778
01785 int32_t hash_code() const;
01786
01787 friend bool operator==<T>(const BD_Shape<T>& x, const BD_Shape<T>& y);
01788
01789 template <typename Temp, typename To, typename U>
01790 friend bool Parma_Polyhedra_Library::rectilinear_distance_assign
01791 (Checked_Number<To, Extended_Number_Policy>& r,
01792 const BD_Shape<U>& x, const BD_Shape<U>& y, const Rounding_Dir dir,
01793 Temp& tmp0, Temp& tmp1, Temp& tmp2);
01794 template <typename Temp, typename To, typename U>
01795 friend bool Parma_Polyhedra_Library::euclidean_distance_assign
01796 (Checked_Number<To, Extended_Number_Policy>& r,
01797 const BD_Shape<U>& x, const BD_Shape<U>& y, const Rounding_Dir dir,
01798 Temp& tmp0, Temp& tmp1, Temp& tmp2);
01799 template <typename Temp, typename To, typename U>
01800 friend bool Parma_Polyhedra_Library::l_infinity_distance_assign
01801 (Checked_Number<To, Extended_Number_Policy>& r,
01802 const BD_Shape<U>& x, const BD_Shape<U>& y, const Rounding_Dir dir,
01803 Temp& tmp0, Temp& tmp1, Temp& tmp2);
01804
01805 private:
01806 template <typename U> friend class Parma_Polyhedra_Library::BD_Shape;
01807 template <typename Interval> friend class Parma_Polyhedra_Library::Box;
01808
01810 DB_Matrix<N> dbm;
01811
01812 #define PPL_IN_BD_Shape_CLASS
01813 #include "BDS_Status.idefs.hh"
01814 #undef PPL_IN_BD_Shape_CLASS
01815
01817 Status status;
01818
01820 Bit_Matrix redundancy_dbm;
01821
01823 bool marked_zero_dim_univ() const;
01824
01831 bool marked_empty() const;
01832
01840 bool marked_shortest_path_closed() const;
01841
01849 bool marked_shortest_path_reduced() const;
01850
01852 void set_empty();
01853
01855 void set_zero_dim_univ();
01856
01858 void set_shortest_path_closed();
01859
01861 void set_shortest_path_reduced();
01862
01864 void reset_shortest_path_closed();
01865
01867 void reset_shortest_path_reduced();
01868
01870 void shortest_path_closure_assign() const;
01871
01877 void shortest_path_reduction_assign() const;
01878
01884 bool is_shortest_path_reduced() const;
01885
01887
01903 bool bounds(const Linear_Expression& expr, bool from_above) const;
01904
01906
01936 bool max_min(const Linear_Expression& expr,
01937 bool maximize,
01938 Coefficient& ext_n, Coefficient& ext_d, bool& included,
01939 Generator& g) const;
01940
01942
01967 bool max_min(const Linear_Expression& expr,
01968 bool maximize,
01969 Coefficient& ext_n, Coefficient& ext_d, bool& included) const;
01970
01981 void refine_no_check(const Constraint& c);
01982
01995 void refine_no_check(const Congruence& cg);
01996
01998 void add_dbm_constraint(dimension_type i, dimension_type j, const N& k);
01999
02001 void add_dbm_constraint(dimension_type i, dimension_type j,
02002 Coefficient_traits::const_reference num,
02003 Coefficient_traits::const_reference den);
02004
02011 void refine(Variable var, Relation_Symbol relsym,
02012 const Linear_Expression& expr,
02013 Coefficient_traits::const_reference denominator
02014 = Coefficient_one());
02015
02017 void forget_all_dbm_constraints(dimension_type v);
02019 void forget_binary_dbm_constraints(dimension_type v);
02020
02022
02036 void deduce_v_minus_u_bounds(dimension_type v,
02037 dimension_type last_v,
02038 const Linear_Expression& sc_expr,
02039 Coefficient_traits::const_reference sc_den,
02040 const N& ub_v);
02041
02043
02058 void deduce_u_minus_v_bounds(dimension_type v,
02059 dimension_type last_v,
02060 const Linear_Expression& sc_expr,
02061 Coefficient_traits::const_reference sc_den,
02062 const N& minus_lb_v);
02063
02068 void get_limiting_shape(const Constraint_System& cs,
02069 BD_Shape& limiting_shape) const;
02070
02072
02075 void compute_predecessors(std::vector<dimension_type>& predecessor) const;
02076
02078
02081 void compute_leaders(std::vector<dimension_type>& leaders) const;
02082
02083 friend std::ostream&
02084 Parma_Polyhedra_Library::IO_Operators
02085 ::operator<<<>(std::ostream& s, const BD_Shape<T>& c);
02086
02088
02089 void throw_dimension_incompatible(const char* method,
02090 const BD_Shape& x) const;
02091
02092 void throw_dimension_incompatible(const char* method,
02093 dimension_type required_dim) const;
02094
02095 void throw_dimension_incompatible(const char* method,
02096 const Constraint& c) const;
02097
02098 void throw_dimension_incompatible(const char* method,
02099 const Congruence& cg) const;
02100
02101 void throw_dimension_incompatible(const char* method,
02102 const Generator& g) const;
02103
02104 void throw_dimension_incompatible(const char* method,
02105 const char* name_row,
02106 const Linear_Expression& y) const;
02107
02108 static void throw_expression_too_complex(const char* method,
02109 const Linear_Expression& e);
02110
02111 static void throw_generic(const char* method, const char* reason);
02113 };
02114
02115
02116 namespace std {
02117
02119
02120 template <typename T>
02121 void swap(Parma_Polyhedra_Library::BD_Shape<T>& x,
02122 Parma_Polyhedra_Library::BD_Shape<T>& y);
02123
02124 }
02125
02126 #include "BDS_Status.inlines.hh"
02127 #include "BD_Shape.inlines.hh"
02128 #include "BD_Shape.templates.hh"
02129
02130 #endif // !defined(PPL_BD_Shape_defs_hh)