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_Octagonal_Shape_defs_hh
00024 #define PPL_Octagonal_Shape_defs_hh 1
00025
00026 #include "Octagonal_Shape.types.hh"
00027 #include "globals.types.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 "OR_Matrix.defs.hh"
00036 #include "Poly_Con_Relation.defs.hh"
00037 #include "Poly_Gen_Relation.defs.hh"
00038 #include "Polyhedron.types.hh"
00039 #include "Box.types.hh"
00040 #include "Grid.types.hh"
00041 #include "BD_Shape.types.hh"
00042 #include "Variable.defs.hh"
00043 #include "Variables_Set.types.hh"
00044 #include "Checked_Number.defs.hh"
00045 #include <vector>
00046 #include <cstddef>
00047 #include <climits>
00048 #include <iosfwd>
00049
00050 namespace Parma_Polyhedra_Library {
00051
00052 namespace IO_Operators {
00053
00055
00062 template <typename T>
00063 std::ostream&
00064 operator<<(std::ostream& s, const Octagonal_Shape<T>& oct);
00065
00066 }
00067
00075 template <typename T>
00076 bool operator==(const Octagonal_Shape<T>& x, const Octagonal_Shape<T>& y);
00077
00085 template <typename T>
00086 bool operator!=(const Octagonal_Shape<T>& x, const Octagonal_Shape<T>& y);
00087
00089
00099 template <typename To, typename T>
00100 bool rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00101 const Octagonal_Shape<T>& x,
00102 const Octagonal_Shape<T>& y,
00103 Rounding_Dir dir);
00104
00106
00116 template <typename Temp, typename To, typename T>
00117 bool rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00118 const Octagonal_Shape<T>& x,
00119 const Octagonal_Shape<T>& y,
00120 Rounding_Dir dir);
00121
00123
00133 template <typename Temp, typename To, typename T>
00134 bool rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00135 const Octagonal_Shape<T>& x,
00136 const Octagonal_Shape<T>& y,
00137 Rounding_Dir dir,
00138 Temp& tmp0,
00139 Temp& tmp1,
00140 Temp& tmp2);
00141
00143
00153 template <typename To, typename T>
00154 bool euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00155 const Octagonal_Shape<T>& x,
00156 const Octagonal_Shape<T>& y,
00157 Rounding_Dir dir);
00158
00160
00170 template <typename Temp, typename To, typename T>
00171 bool euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00172 const Octagonal_Shape<T>& x,
00173 const Octagonal_Shape<T>& y,
00174 Rounding_Dir dir);
00175
00177
00187 template <typename Temp, typename To, typename T>
00188 bool euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00189 const Octagonal_Shape<T>& x,
00190 const Octagonal_Shape<T>& y,
00191 Rounding_Dir dir,
00192 Temp& tmp0,
00193 Temp& tmp1,
00194 Temp& tmp2);
00195
00197
00207 template <typename To, typename T>
00208 bool l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00209 const Octagonal_Shape<T>& x,
00210 const Octagonal_Shape<T>& y,
00211 Rounding_Dir dir);
00212
00214
00224 template <typename Temp, typename To, typename T>
00225 bool l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00226 const Octagonal_Shape<T>& x,
00227 const Octagonal_Shape<T>& y,
00228 Rounding_Dir dir);
00229
00231
00241 template <typename Temp, typename To, typename T>
00242 bool l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00243 const Octagonal_Shape<T>& x,
00244 const Octagonal_Shape<T>& y,
00245 Rounding_Dir dir,
00246 Temp& tmp0,
00247 Temp& tmp1,
00248 Temp& tmp2);
00249
00250 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00252
00289 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
00290 bool extract_octagonal_difference(const Constraint& c,
00291 dimension_type c_space_dim,
00292 dimension_type& c_num_vars,
00293 dimension_type& c_first_var,
00294 dimension_type& c_second_var,
00295 Coefficient& c_coeff,
00296 Coefficient& c_term);
00297
00298 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00300
00301 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
00302 dimension_type coherent_index(dimension_type i);
00303
00304 }
00305
00307
00403 template <typename T>
00404 class Parma_Polyhedra_Library::Octagonal_Shape {
00405 private:
00410 #ifndef NDEBUG
00411 typedef Checked_Number<T, Extended_Number_Policy> N;
00412 #else
00413 typedef Checked_Number<T, WRD_Extended_Number_Policy> N;
00414 #endif
00415
00416 public:
00418 typedef T coefficient_type_base;
00419
00424 typedef N coefficient_type;
00425
00427 static dimension_type max_space_dimension();
00428
00432 static bool can_recycle_constraint_systems();
00433
00437 static bool can_recycle_congruence_systems();
00438
00440
00441
00443
00450 explicit Octagonal_Shape(dimension_type num_dimensions = 0,
00451 Degenerate_Element kind = UNIVERSE);
00452
00454
00457 Octagonal_Shape(const Octagonal_Shape& x,
00458 Complexity_Class complexity = ANY_COMPLEXITY);
00459
00461
00464 template <typename U>
00465 explicit Octagonal_Shape(const Octagonal_Shape<U>& y,
00466 Complexity_Class complexity = ANY_COMPLEXITY);
00467
00469
00481 explicit Octagonal_Shape(const Constraint_System& cs);
00482
00484
00490 explicit Octagonal_Shape(const Congruence_System& cgs);
00491
00493
00500 explicit Octagonal_Shape(const Generator_System& gs);
00501
00503
00509 explicit Octagonal_Shape(const Polyhedron& ph,
00510 Complexity_Class complexity = ANY_COMPLEXITY);
00511
00513
00528 template <typename Interval>
00529 explicit Octagonal_Shape(const Box<Interval>& box,
00530 Complexity_Class complexity = ANY_COMPLEXITY);
00531
00533
00548 explicit Octagonal_Shape(const Grid& grid,
00549 Complexity_Class complexity = ANY_COMPLEXITY);
00550
00552
00567 template <typename U>
00568 explicit Octagonal_Shape(const BD_Shape<U>& bd,
00569 Complexity_Class complexity = ANY_COMPLEXITY);
00570
00575 Octagonal_Shape& operator=(const Octagonal_Shape& y);
00576
00581 void swap(Octagonal_Shape& y);
00582
00584 ~Octagonal_Shape();
00585
00587
00589
00590
00592 dimension_type space_dimension() const;
00593
00599 dimension_type affine_dimension() const;
00600
00602 Constraint_System constraints() const;
00603
00605 Constraint_System minimized_constraints() const;
00606
00608 Congruence_System congruences() const;
00609
00614 Congruence_System minimized_congruences() const;
00615
00617
00621 bool contains(const Octagonal_Shape& y) const;
00622
00624
00628 bool strictly_contains(const Octagonal_Shape& y) const;
00629
00631
00636 bool is_disjoint_from(const Octagonal_Shape& y) const;
00637
00644 Poly_Con_Relation relation_with(const Constraint& c) const;
00645
00652 Poly_Con_Relation relation_with(const Congruence& cg) const;
00653
00660 Poly_Gen_Relation relation_with(const Generator& g) const;
00661
00663 bool is_empty() const;
00664
00666 bool is_universe() const;
00667
00669 bool is_discrete() const;
00670
00675 bool is_bounded() const;
00676
00681 bool is_topologically_closed() const;
00682
00687 bool contains_integer_point() const;
00688
00696 bool constrains(Variable var) const;
00697
00705 bool bounds_from_above(const Linear_Expression& expr) const;
00706
00714 bool bounds_from_below(const Linear_Expression& expr) const;
00715
00740 bool maximize(const Linear_Expression& expr,
00741 Coefficient& sup_n, Coefficient& sup_d, bool& maximum) const;
00742
00771 bool maximize(const Linear_Expression& expr,
00772 Coefficient& sup_n, Coefficient& sup_d, bool& maximum,
00773 Generator& g) const;
00774
00799 bool minimize(const Linear_Expression& expr,
00800 Coefficient& inf_n, Coefficient& inf_d, bool& minimum) const;
00801
00830 bool minimize(const Linear_Expression& expr,
00831 Coefficient& inf_n, Coefficient& inf_d, bool& minimum,
00832 Generator& g) const;
00833
00835 bool OK() const;
00836
00838
00840
00841
00854 void add_constraint(const Constraint& c);
00855
00868 void add_constraints(const Constraint_System& cs);
00869
00886 void add_recycled_constraints(Constraint_System& cs);
00887
00895 void add_congruence(const Congruence& cg);
00896
00909 void add_congruences(const Congruence_System& cgs);
00910
00911
00927 void add_recycled_congruences(Congruence_System& cgs);
00928
00939 void refine_with_constraint(const Constraint& c);
00940
00952 void refine_with_congruence(const Congruence& cg);
00953
00965 void refine_with_constraints(const Constraint_System& cs);
00966
00978 void refine_with_congruences(const Congruence_System& cgs);
00979
00990 void unconstrain(Variable var);
00991
01004 void unconstrain(const Variables_Set& to_be_unconstrained);
01005
01007
01011 void intersection_assign(const Octagonal_Shape& y);
01012
01020 void upper_bound_assign(const Octagonal_Shape& y);
01021
01030 bool upper_bound_assign_if_exact(const Octagonal_Shape& y);
01031
01039 void difference_assign(const Octagonal_Shape& y);
01040
01050 bool simplify_using_context_assign(const Octagonal_Shape& y);
01051
01070 void affine_image(Variable var,
01071 const Linear_Expression& expr,
01072 Coefficient_traits::const_reference denominator
01073 = Coefficient_one());
01074
01093 void affine_preimage(Variable var,
01094 const Linear_Expression& expr,
01095 Coefficient_traits::const_reference denominator
01096 = Coefficient_one());
01097
01122 void generalized_affine_image(Variable var,
01123 Relation_Symbol relsym,
01124 const Linear_Expression& expr,
01125 Coefficient_traits::const_reference denominator
01126 = Coefficient_one());
01127
01147 void generalized_affine_image(const Linear_Expression& lhs,
01148 Relation_Symbol relsym,
01149 const Linear_Expression& rhs);
01150
01177 void bounded_affine_image(Variable var,
01178 const Linear_Expression& lb_expr,
01179 const Linear_Expression& ub_expr,
01180 Coefficient_traits::const_reference denominator
01181 = Coefficient_one());
01182
01207 void generalized_affine_preimage(Variable var,
01208 Relation_Symbol relsym,
01209 const Linear_Expression& expr,
01210 Coefficient_traits::const_reference
01211 denominator = Coefficient_one());
01212
01232 void generalized_affine_preimage(const Linear_Expression& lhs,
01233 Relation_Symbol relsym,
01234 const Linear_Expression& rhs);
01235
01262 void bounded_affine_preimage(Variable var,
01263 const Linear_Expression& lb_expr,
01264 const Linear_Expression& ub_expr,
01265 Coefficient_traits::const_reference denominator
01266 = Coefficient_one());
01267
01275 void time_elapse_assign(const Octagonal_Shape& y);
01276
01278 void topological_closure_assign();
01279
01295 void CC76_extrapolation_assign(const Octagonal_Shape& y, unsigned* tp = 0);
01296
01318 template <typename Iterator>
01319 void CC76_extrapolation_assign(const Octagonal_Shape& y,
01320 Iterator first, Iterator last,
01321 unsigned* tp = 0);
01322
01338 void BHMZ05_widening_assign(const Octagonal_Shape& y, unsigned* tp = 0);
01339
01341 void widening_assign(const Octagonal_Shape& y, unsigned* tp = 0);
01342
01363 void limited_BHMZ05_extrapolation_assign(const Octagonal_Shape& y,
01364 const Constraint_System& cs,
01365 unsigned* tp = 0);
01366
01377 void CC76_narrowing_assign(const Octagonal_Shape& y);
01378
01399 void limited_CC76_extrapolation_assign(const Octagonal_Shape& y,
01400 const Constraint_System& cs,
01401 unsigned* tp = 0);
01402
01404
01406
01407
01409
01426 void add_space_dimensions_and_embed(dimension_type m);
01427
01449 void add_space_dimensions_and_project(dimension_type m);
01450
01459 void concatenate_assign(const Octagonal_Shape& y);
01460
01462
01470 void remove_space_dimensions(const Variables_Set& to_be_removed);
01471
01480 void remove_higher_space_dimensions(dimension_type new_dimension);
01481
01518 template <typename Partial_Function>
01519 void map_space_dimensions(const Partial_Function& pfunc);
01520
01522
01542 void expand_space_dimension(Variable var, dimension_type m);
01543
01545
01567 void fold_space_dimensions(const Variables_Set& to_be_folded, Variable var);
01568
01570
01571 PPL_OUTPUT_DECLARATIONS
01572
01573 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
01574
01579 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
01580 bool ascii_load(std::istream& s);
01581
01583 memory_size_type total_memory_in_bytes() const;
01584
01586 memory_size_type external_memory_in_bytes() const;
01587
01594 int32_t hash_code() const;
01595
01596 friend bool
01597 operator==<T>(const Octagonal_Shape<T>& x, const Octagonal_Shape<T>& y);
01598
01599 template <typename Temp, typename To, typename U>
01600 friend bool Parma_Polyhedra_Library::rectilinear_distance_assign
01601 (Checked_Number<To, Extended_Number_Policy>& r,
01602 const Octagonal_Shape<U>& x, const Octagonal_Shape<U>& y,
01603 const Rounding_Dir dir, Temp& tmp0, Temp& tmp1, Temp& tmp2);
01604 template <typename Temp, typename To, typename U>
01605 friend bool Parma_Polyhedra_Library::euclidean_distance_assign
01606 (Checked_Number<To, Extended_Number_Policy>& r,
01607 const Octagonal_Shape<U>& x, const Octagonal_Shape<U>& y,
01608 const Rounding_Dir dir, Temp& tmp0, Temp& tmp1, Temp& tmp2);
01609 template <typename Temp, typename To, typename U>
01610 friend bool Parma_Polyhedra_Library::l_infinity_distance_assign
01611 (Checked_Number<To, Extended_Number_Policy>& r,
01612 const Octagonal_Shape<U>& x, const Octagonal_Shape<U>& y,
01613 const Rounding_Dir dir, Temp& tmp0, Temp& tmp1, Temp& tmp2);
01614
01615 private:
01616 template <typename U> friend class Parma_Polyhedra_Library::Octagonal_Shape;
01617 template <typename Interval> friend class Parma_Polyhedra_Library::Box;
01618
01620 OR_Matrix<N> matrix;
01621
01623 dimension_type space_dim;
01624
01625
01626
01627
01628
01629
01630
01631 #define PPL_IN_Octagonal_Shape_CLASS
01632 #include "Og_Status.idefs.hh"
01633 #undef PPL_IN_Octagonal_Shape_CLASS
01634
01636 Status status;
01637
01639 bool marked_zero_dim_univ() const;
01640
01642
01646 bool marked_empty() const;
01647
01655 bool marked_strongly_closed() const;
01656
01658 void set_zero_dim_univ();
01659
01661 void set_empty();
01662
01664 void set_strongly_closed();
01665
01667 void reset_strongly_closed();
01668
01669 N& matrix_at(dimension_type i, dimension_type j);
01670 const N& matrix_at(dimension_type i, dimension_type j) const;
01671
01682 void refine_no_check(const Constraint& c);
01683
01696 void refine_no_check(const Congruence& cg);
01697
01699 void add_octagonal_constraint(dimension_type i,
01700 dimension_type j,
01701 const N& k);
01702
01704 void add_octagonal_constraint(dimension_type i,
01705 dimension_type j,
01706 Coefficient_traits::const_reference num,
01707 Coefficient_traits::const_reference den);
01708
01715 void refine(Variable var,
01716 Relation_Symbol relsym,
01717 const Linear_Expression& expr,
01718 Coefficient_traits::const_reference denominator
01719 = Coefficient_one());
01720
01722 void forget_all_octagonal_constraints(dimension_type v_id);
01723
01725 void forget_binary_octagonal_constraints(dimension_type v_id);
01726
01728
01754 void deduce_v_pm_u_bounds(dimension_type v_id,
01755 dimension_type last_id,
01756 const Linear_Expression& sc_expr,
01757 Coefficient_traits::const_reference sc_den,
01758 const N& ub_v);
01759
01761
01788 void deduce_minus_v_pm_u_bounds(dimension_type v,
01789 dimension_type last_v,
01790 const Linear_Expression& sc_expr,
01791 Coefficient_traits::const_reference sc_den,
01792 const N& minus_lb_v);
01793
01798 void get_limiting_octagon(const Constraint_System& cs,
01799 Octagonal_Shape& limiting_octagon) const;
01801
01804 void compute_successors(std::vector<dimension_type>& successor) const;
01805
01807
01810 void compute_leaders(std::vector<dimension_type>& successor,
01811 std::vector<dimension_type>& no_sing_leaders,
01812 bool& exist_sing_class,
01813 dimension_type& sing_leader) const;
01814
01816
01819 void compute_leaders(std::vector<dimension_type>& leaders) const;
01820
01822 void strong_reduction_assign() const;
01823
01828 bool is_strongly_reduced() const;
01829
01834 bool is_strong_coherent() const;
01835
01836 bool tight_coherence_would_make_empty() const;
01837
01839
01845 void strong_closure_assign() const;
01846
01848 void strong_coherence_assign();
01849
01851
01859 void incremental_strong_closure_assign(Variable var) const;
01860
01862
01878 bool bounds(const Linear_Expression& expr, bool from_above) const;
01879
01881
01906 bool max_min(const Linear_Expression& expr,
01907 bool maximize,
01908 Coefficient& ext_n, Coefficient& ext_d, bool& included) const;
01909
01911
01941 bool max_min(const Linear_Expression& expr,
01942 bool maximize,
01943 Coefficient& ext_n, Coefficient& ext_d, bool& included,
01944 Generator& g) const;
01945
01946
01947 friend std::ostream&
01948 Parma_Polyhedra_Library::IO_Operators
01949 ::operator<<<>(std::ostream& s, const Octagonal_Shape<T>& c);
01950
01952
01953 void throw_dimension_incompatible(const char* method,
01954 const Octagonal_Shape& x) const;
01955
01956 void throw_dimension_incompatible(const char* method,
01957 dimension_type required_dim) const;
01958
01959 void throw_dimension_incompatible(const char* method,
01960 const Constraint& c) const;
01961
01962 void throw_dimension_incompatible(const char* method,
01963 const Congruence& cg) const;
01964
01965 void throw_dimension_incompatible(const char* method,
01966 const Generator& g) const;
01967
01968 void throw_dimension_incompatible(const char* method,
01969 const char* name_row,
01970 const Linear_Expression& y) const;
01971
01972 void throw_constraint_incompatible(const char* method) const;
01973
01974 void throw_expression_too_complex(const char* method,
01975 const Linear_Expression& e) const;
01976
01977 void throw_generic(const char* method, const char* reason) const;
01979
01980 static T default_stop_points[];
01981 };
01982
01983 namespace std {
01984
01986
01987 template <typename T>
01988 void swap(Parma_Polyhedra_Library::Octagonal_Shape<T>& x,
01989 Parma_Polyhedra_Library::Octagonal_Shape<T>& y);
01990
01991 }
01992
01993 #include "Og_Status.inlines.hh"
01994 #include "Octagonal_Shape.inlines.hh"
01995 #include "Octagonal_Shape.templates.hh"
01996
01997 #endif // !defined(PPL_Octagonal_Shape_defs_hh)