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_defs_hh
00024 #define PPL_Box_defs_hh 1
00025
00026 #include "Box.types.hh"
00027 #include "globals.types.hh"
00028 #include "Coefficient.defs.hh"
00029 #include "Variable.types.hh"
00030 #include "Variables_Set.types.hh"
00031 #include "Linear_Expression.types.hh"
00032 #include "Constraint.types.hh"
00033 #include "Constraint.defs.hh"
00034 #include "Constraint_System.types.hh"
00035 #include "Generator.types.hh"
00036 #include "Generator_System.types.hh"
00037 #include "Congruence.types.hh"
00038 #include "Congruence_System.types.hh"
00039 #include "BD_Shape.types.hh"
00040 #include "Octagonal_Shape.types.hh"
00041 #include "Poly_Con_Relation.types.hh"
00042 #include "Poly_Gen_Relation.types.hh"
00043 #include "Polyhedron.types.hh"
00044 #include "Grid.types.hh"
00045 #include "Partially_Reduced_Product.types.hh"
00046 #include <vector>
00047 #include <iosfwd>
00048
00049 namespace Parma_Polyhedra_Library {
00050
00052
00056 template <typename ITV>
00057 bool operator==(const Box<ITV>& x, const Box<ITV>& y);
00058
00060
00064 template <typename ITV>
00065 bool operator!=(const Box<ITV>& x, const Box<ITV>& y);
00066
00067 namespace IO_Operators {
00068
00070
00071 template <typename ITV>
00072 std::ostream& operator<<(std::ostream& s, const Box<ITV>& box);
00073
00074 }
00075
00077
00087 template <typename To, typename ITV>
00088 bool
00089 rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00090 const Box<ITV>& x,
00091 const Box<ITV>& y,
00092 Rounding_Dir dir);
00093
00095
00105 template <typename Temp, typename To, typename ITV>
00106 bool
00107 rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00108 const Box<ITV>& x,
00109 const Box<ITV>& y,
00110 Rounding_Dir dir);
00111
00113
00123 template <typename Temp, typename To, typename ITV>
00124 bool
00125 rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00126 const Box<ITV>& x,
00127 const Box<ITV>& y,
00128 Rounding_Dir dir,
00129 Temp& tmp0,
00130 Temp& tmp1,
00131 Temp& tmp2);
00132
00134
00144 template <typename To, typename ITV>
00145 bool
00146 euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00147 const Box<ITV>& x,
00148 const Box<ITV>& y,
00149 Rounding_Dir dir);
00150
00152
00162 template <typename Temp, typename To, typename ITV>
00163 bool
00164 euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00165 const Box<ITV>& x,
00166 const Box<ITV>& y,
00167 Rounding_Dir dir);
00168
00170
00180 template <typename Temp, typename To, typename ITV>
00181 bool
00182 euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00183 const Box<ITV>& x,
00184 const Box<ITV>& y,
00185 Rounding_Dir dir,
00186 Temp& tmp0,
00187 Temp& tmp1,
00188 Temp& tmp2);
00189
00191
00201 template <typename To, typename ITV>
00202 bool
00203 l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00204 const Box<ITV>& x,
00205 const Box<ITV>& y,
00206 Rounding_Dir dir);
00207
00209
00219 template <typename Temp, typename To, typename ITV>
00220 bool
00221 l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00222 const Box<ITV>& x,
00223 const Box<ITV>& y,
00224 Rounding_Dir dir);
00225
00227
00237 template <typename Temp, typename To, typename ITV>
00238 bool
00239 l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00240 const Box<ITV>& x,
00241 const Box<ITV>& y,
00242 Rounding_Dir dir,
00243 Temp& tmp0,
00244 Temp& tmp1,
00245 Temp& tmp2);
00246
00247 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00248
00251 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
00252 template <typename Specialization,
00253 typename Temp, typename To, typename ITV>
00254 bool
00255 l_m_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
00256 const Box<ITV>& x, const Box<ITV>& y,
00257 Rounding_Dir dir,
00258 Temp& tmp0, Temp& tmp1, Temp& tmp2);
00259
00260 }
00261
00263
00269 template <typename ITV>
00270 class Parma_Polyhedra_Library::Box {
00271 public:
00273 typedef ITV interval_type;
00274
00276 static dimension_type max_space_dimension();
00277
00281 static bool can_recycle_constraint_systems();
00282
00286 static bool can_recycle_congruence_systems();
00287
00289
00290
00292
00299 explicit Box(dimension_type num_dimensions = 0,
00300 Degenerate_Element kind = UNIVERSE);
00301
00303
00306 Box(const Box& y,
00307 Complexity_Class complexity = ANY_COMPLEXITY);
00308
00310
00313 template <typename Other_ITV>
00314 explicit Box(const Box<Other_ITV>& y,
00315 Complexity_Class complexity = ANY_COMPLEXITY);
00316
00318
00327 explicit Box(const Constraint_System& cs);
00328
00330
00343 Box(const Constraint_System& cs, Recycle_Input dummy);
00344
00346
00353 explicit Box(const Generator_System& gs);
00354
00356
00370 Box(const Generator_System& gs, Recycle_Input dummy);
00371
00382 explicit Box(const Congruence_System& cgs);
00383
00398 Box(const Congruence_System& cgs, Recycle_Input dummy);
00399
00401
00405 template <typename T>
00406 explicit Box(const BD_Shape<T>& bds,
00407 Complexity_Class complexity = POLYNOMIAL_COMPLEXITY);
00408
00410
00414 template <typename T>
00415 explicit Box(const Octagonal_Shape<T>& oct,
00416 Complexity_Class complexity = POLYNOMIAL_COMPLEXITY);
00417
00419
00425 explicit Box(const Polyhedron& ph,
00426 Complexity_Class complexity = ANY_COMPLEXITY);
00427
00429
00433 explicit Box(const Grid& ph,
00434 Complexity_Class complexity = POLYNOMIAL_COMPLEXITY);
00435
00437
00441 template <typename D1, typename D2, typename R>
00442 explicit Box(const Partially_Reduced_Product<D1, D2, R>& dp,
00443 Complexity_Class complexity = ANY_COMPLEXITY);
00444
00449 Box& operator=(const Box& y);
00450
00455 void swap(Box& y);
00456
00458
00460
00461
00463 dimension_type space_dimension() const;
00464
00470 dimension_type affine_dimension() const;
00471
00473 bool is_empty() const;
00474
00476 bool is_universe() const;
00477
00482 bool is_topologically_closed() const;
00483
00485 bool is_discrete() const;
00486
00488 bool is_bounded() const;
00489
00494 bool contains_integer_point() const;
00495
00503 bool constrains(Variable var) const;
00504
00506
00510 Poly_Con_Relation relation_with(const Constraint& c) const;
00511
00513
00517 Poly_Con_Relation relation_with(const Congruence& cg) const;
00518
00520
00524 Poly_Gen_Relation relation_with(const Generator& g) const;
00525
00533 bool bounds_from_above(const Linear_Expression& expr) const;
00534
00542 bool bounds_from_below(const Linear_Expression& expr) const;
00543
00568 bool maximize(const Linear_Expression& expr,
00569 Coefficient& sup_n, Coefficient& sup_d, bool& maximum) const;
00570
00599 bool maximize(const Linear_Expression& expr,
00600 Coefficient& sup_n, Coefficient& sup_d, bool& maximum,
00601 Generator& g) const;
00602
00627 bool minimize(const Linear_Expression& expr,
00628 Coefficient& inf_n, Coefficient& inf_d, bool& minimum) const;
00629
00658 bool minimize(const Linear_Expression& expr,
00659 Coefficient& inf_n, Coefficient& inf_d, bool& minimum,
00660 Generator& g) const;
00661
00668 bool contains(const Box&) const;
00669
00676 bool strictly_contains(const Box&) const;
00677
00684 bool is_disjoint_from(const Box& y) const;
00685
00690 bool OK() const;
00691
00693
00695
00696
00708 void add_constraint(const Constraint& c);
00709
00721 void add_constraints(const Constraint_System& cs);
00722
00739 void add_recycled_constraints(Constraint_System& cs);
00740
00751 void add_congruence(const Congruence& cg);
00752
00764 void add_congruences(const Congruence_System& cgs);
00765
00782 void add_recycled_congruences(Congruence_System& cgs);
00783
00793 void refine_with_constraint(const Constraint& c);
00794
00804 void refine_with_constraints(const Constraint_System& cs);
00805
00815 void refine_with_congruence(const Congruence& cg);
00816
00826 void refine_with_congruences(const Congruence_System& cgs);
00827
00837 void propagate_constraint(const Constraint& c);
00838
00848 void propagate_constraints(const Constraint_System& cs);
00849
00860 void unconstrain(Variable var);
00861
00874 void unconstrain(const Variables_Set& to_be_unconstrained);
00875
00877
00881 void intersection_assign(const Box& y);
00882
00890 void upper_bound_assign(const Box& y);
00891
00900 bool upper_bound_assign_if_exact(const Box& y);
00901
00908 void difference_assign(const Box& y);
00909
00919 bool simplify_using_context_assign(const Box& y);
00920
00942 void affine_image(Variable var,
00943 const Linear_Expression& expr,
00944 Coefficient_traits::const_reference denominator
00945 = Coefficient_one());
00946
00967 void affine_preimage(Variable var,
00968 const Linear_Expression& expr,
00969 Coefficient_traits::const_reference denominator
00970 = Coefficient_one());
00971
00996 void generalized_affine_image(Variable var,
00997 Relation_Symbol relsym,
00998 const Linear_Expression& expr,
00999 Coefficient_traits::const_reference denominator
01000 = Coefficient_one());
01001
01026 void
01027 generalized_affine_preimage(Variable var,
01028 Relation_Symbol relsym,
01029 const Linear_Expression& expr,
01030 Coefficient_traits::const_reference denominator
01031 = Coefficient_one());
01032
01051 void generalized_affine_image(const Linear_Expression& lhs,
01052 Relation_Symbol relsym,
01053 const Linear_Expression& rhs);
01054
01073 void generalized_affine_preimage(const Linear_Expression& lhs,
01074 Relation_Symbol relsym,
01075 const Linear_Expression& rhs);
01076
01102 void bounded_affine_image(Variable var,
01103 const Linear_Expression& lb_expr,
01104 const Linear_Expression& ub_expr,
01105 Coefficient_traits::const_reference denominator
01106 = Coefficient_one());
01107
01133 void bounded_affine_preimage(Variable var,
01134 const Linear_Expression& lb_expr,
01135 const Linear_Expression& ub_expr,
01136 Coefficient_traits::const_reference denominator
01137 = Coefficient_one());
01138
01146 void time_elapse_assign(const Box& y);
01147
01149 void topological_closure_assign();
01150
01166 void CC76_widening_assign(const Box& y, unsigned* tp = 0);
01167
01184 template <typename Iterator>
01185 void CC76_widening_assign(const Box& y,
01186 Iterator first, Iterator last);
01187
01189 void widening_assign(const Box& y, unsigned* tp = 0);
01190
01211 void limited_CC76_extrapolation_assign(const Box& y,
01212 const Constraint_System& cs,
01213 unsigned* tp = 0);
01214
01234 void CC76_narrowing_assign(const Box& y);
01235
01237
01239
01240
01242
01259 void add_space_dimensions_and_embed(dimension_type m);
01260
01282 void add_space_dimensions_and_project(dimension_type m);
01283
01307 void concatenate_assign(const Box& y);
01308
01310
01318 void remove_space_dimensions(const Variables_Set& to_be_removed);
01319
01328 void remove_higher_space_dimensions(dimension_type new_dimension);
01329
01367 template <typename Partial_Function>
01368 void map_space_dimensions(const Partial_Function& pfunc);
01369
01371
01391 void expand_space_dimension(Variable var, dimension_type m);
01392
01394
01416 void fold_space_dimensions(const Variables_Set& to_be_folded, Variable var);
01417
01419
01426 const ITV& get_interval(Variable var) const;
01427
01434 void set_interval(Variable var, const ITV& i);
01435
01457 bool get_lower_bound(dimension_type k, bool& closed,
01458 Coefficient& n, Coefficient& d) const;
01459
01478 bool get_upper_bound(dimension_type k, bool& closed,
01479 Coefficient& n, Coefficient& d) const;
01480
01482 Constraint_System constraints() const;
01483
01485 Constraint_System minimized_constraints() const;
01486
01488 Congruence_System congruences() const;
01489
01491 Congruence_System minimized_congruences() const;
01492
01494 memory_size_type total_memory_in_bytes() const;
01495
01497 memory_size_type external_memory_in_bytes() const;
01498
01499 PPL_OUTPUT_DECLARATIONS
01500
01501 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
01502
01507 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
01508 bool ascii_load(std::istream& s);
01509
01510 private:
01511 template <typename Other_ITV>
01512 friend class Parma_Polyhedra_Library::Box;
01513
01514 friend bool
01515 operator==<ITV>(const Box<ITV>& x, const Box<ITV>& y);
01516
01517 friend std::ostream&
01518 Parma_Polyhedra_Library
01519 ::IO_Operators::operator<<<>(std::ostream& s, const Box<ITV>& box);
01520
01521 template <typename Specialization, typename Temp, typename To, typename I>
01522 friend bool Parma_Polyhedra_Library::l_m_distance_assign
01523 (Checked_Number<To, Extended_Number_Policy>& r,
01524 const Box<I>& x, const Box<I>& y, const Rounding_Dir dir,
01525 Temp& tmp0, Temp& tmp1, Temp& tmp2);
01526
01528 typedef std::vector<ITV> Sequence;
01529
01534 typedef ITV Tmp_Interval_Type;
01535
01537 Sequence seq;
01538
01539 #define PPL_IN_Box_CLASS
01540 #include "Box_Status.idefs.hh"
01541 #undef PPL_IN_Box_CLASS
01542
01544 Status status;
01545
01552 bool marked_empty() const;
01553
01554 public:
01556 void set_empty();
01557
01558 private:
01560 void set_nonempty();
01561
01563 void set_empty_up_to_date();
01564
01566 void reset_empty_up_to_date();
01567
01572 bool check_empty() const;
01573
01578 const ITV& operator[](dimension_type k) const;
01579
01583 void
01584 add_interval_constraint_no_check(dimension_type var_id,
01585 Constraint::Type type,
01586 Coefficient_traits::const_reference num,
01587 Coefficient_traits::const_reference den);
01588
01592 void add_constraint_no_check(const Constraint& c);
01593
01597 void add_constraints_no_check(const Constraint_System& cs);
01598
01602 void add_congruence_no_check(const Congruence& cg);
01603
01607 void add_congruences_no_check(const Congruence_System& cgs);
01608
01620 void refine_no_check(const Constraint& c);
01621
01633 void refine_no_check(const Constraint_System& cs);
01634
01646 void refine_no_check(const Congruence& cg);
01647
01659 void refine_no_check(const Congruence_System& cgs);
01660
01821 void propagate_constraint_no_check(const Constraint& c);
01822
01836 void propagate_constraints_no_check(const Constraint_System& cs);
01837
01839
01855 bool bounds(const Linear_Expression& expr, bool from_above) const;
01856
01858
01887 bool max_min(const Linear_Expression& expr,
01888 bool maximize,
01889 Coefficient& ext_n, Coefficient& ext_d, bool& included,
01890 Generator& g) const;
01891
01893
01917 bool max_min(const Linear_Expression& expr,
01918 bool maximize,
01919 Coefficient& ext_n, Coefficient& ext_d, bool& included) const;
01920
01922
01923 void throw_dimension_incompatible(const char* method,
01924 const Box& x) const;
01925
01926 void throw_dimension_incompatible(const char* method,
01927 dimension_type required_dim) const;
01928
01929 void throw_dimension_incompatible(const char* method,
01930 const Constraint& c) const;
01931
01932 void throw_dimension_incompatible(const char* method,
01933 const Congruence& cg) const;
01934
01935 void throw_dimension_incompatible(const char* method,
01936 const Constraint_System& cs) const;
01937
01938 void throw_dimension_incompatible(const char* method,
01939 const Congruence_System& cgs) const;
01940
01941 void throw_dimension_incompatible(const char* method,
01942 const Generator& g) const;
01943
01944 void throw_dimension_incompatible(const char* method,
01945 const char* name_row,
01946 const Linear_Expression& y) const;
01947
01948 static void throw_space_dimension_overflow(const char* method,
01949 const char* reason);
01950
01951 static void throw_constraint_incompatible(const char* method);
01952
01953 static void throw_expression_too_complex(const char* method,
01954 const Linear_Expression& e);
01955
01956 static void throw_generic(const char* method, const char* reason);
01958 };
01959
01960 namespace Parma_Polyhedra_Library {
01961
01962 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
01963
01984 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
01985 template <typename ITV>
01986 Poly_Con_Relation
01987 interval_relation(const ITV& i,
01988 const Constraint::Type constraint_type,
01989 Coefficient_traits::const_reference num,
01990 Coefficient_traits::const_reference den = 1);
01991
01992 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
01994
02017 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
02018 bool extract_interval_constraint(const Constraint& c,
02019 dimension_type c_space_dim,
02020 dimension_type& c_num_vars,
02021 dimension_type& c_only_var);
02022
02023 bool extract_interval_congruence(const Congruence& cg,
02024 dimension_type cg_space_dim,
02025 dimension_type& cg_num_vars,
02026 dimension_type& cg_only_var);
02027
02028 }
02029
02030 #include "Box_Status.inlines.hh"
02031 #include "Box.inlines.hh"
02032 #include "Box.templates.hh"
02033
02034 #endif // !defined(PPL_Box_defs_hh)