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_Polyhedron_defs_hh
00024 #define PPL_Polyhedron_defs_hh 1
00025
00026 #include "Polyhedron.types.hh"
00027 #include "globals.types.hh"
00028 #include "Variable.defs.hh"
00029 #include "Linear_Expression.defs.hh"
00030 #include "Constraint_System.defs.hh"
00031 #include "Constraint_System.inlines.hh"
00032 #include "Generator_System.defs.hh"
00033 #include "Generator_System.inlines.hh"
00034 #include "Congruence_System.defs.hh"
00035 #include "Congruence_System.inlines.hh"
00036 #include "Saturation_Matrix.defs.hh"
00037 #include "Generator.types.hh"
00038 #include "Congruence.defs.hh"
00039 #include "Poly_Con_Relation.defs.hh"
00040 #include "Poly_Gen_Relation.defs.hh"
00041 #include "BHRZ03_Certificate.types.hh"
00042 #include "H79_Certificate.types.hh"
00043 #include "BD_Shape.types.hh"
00044 #include <vector>
00045 #include <iosfwd>
00046
00047 namespace Parma_Polyhedra_Library {
00048
00049 namespace IO_Operators {
00050
00052
00060 std::ostream&
00061 operator<<(std::ostream& s, const Polyhedron& ph);
00062
00063 }
00064
00073 bool operator==(const Polyhedron& x, const Polyhedron& y);
00074
00083 bool operator!=(const Polyhedron& x, const Polyhedron& y);
00084
00085 }
00086
00087
00089
00351 class Parma_Polyhedra_Library::Polyhedron {
00352 public:
00354 static dimension_type max_space_dimension();
00355
00356 protected:
00358
00368 Polyhedron(Topology topol,
00369 dimension_type num_dimensions,
00370 Degenerate_Element kind);
00371
00373 Polyhedron(const Polyhedron& y);
00374
00376
00388 Polyhedron(Topology topol, const Constraint_System& cs);
00389
00391
00405 Polyhedron(Topology topol, Constraint_System& cs);
00406
00408
00421 Polyhedron(Topology topol, const Generator_System& gs);
00422
00424
00439 Polyhedron(Topology topol, Generator_System& gs);
00440
00442
00496 template <typename Box>
00497 Polyhedron(Topology topol, const Box& box);
00498
00503 Polyhedron& operator=(const Polyhedron& y);
00504
00505 public:
00507
00508
00510 dimension_type space_dimension() const;
00511
00517 dimension_type affine_dimension() const;
00518
00520 const Constraint_System& constraints() const;
00521
00523 const Constraint_System& minimized_constraints() const;
00524
00526 const Generator_System& generators() const;
00527
00529 const Generator_System& minimized_generators() const;
00530
00538 Poly_Con_Relation relation_with(const Constraint& c) const;
00539
00547 Poly_Gen_Relation relation_with(const Generator& g) const;
00548
00553 bool is_empty() const;
00554
00559 bool is_universe() const;
00560
00565 bool is_topologically_closed() const;
00566
00568
00573 bool is_disjoint_from(const Polyhedron& y) const;
00574
00579 bool is_bounded() const;
00580
00588 bool bounds_from_above(const Linear_Expression& expr) const;
00589
00597 bool bounds_from_below(const Linear_Expression& expr) const;
00598
00623 bool maximize(const Linear_Expression& expr,
00624 Coefficient& sup_n, Coefficient& sup_d, bool& maximum) const;
00625
00654 bool maximize(const Linear_Expression& expr,
00655 Coefficient& sup_n, Coefficient& sup_d, bool& maximum,
00656 Generator& point) const;
00657
00682 bool minimize(const Linear_Expression& expr,
00683 Coefficient& inf_n, Coefficient& inf_d, bool& minimum) const;
00684
00713 bool minimize(const Linear_Expression& expr,
00714 Coefficient& inf_n, Coefficient& inf_d, bool& minimum,
00715 Generator& point) const;
00716
00718
00723 bool contains(const Polyhedron& y) const;
00724
00726
00731 bool strictly_contains(const Polyhedron& y) const;
00732
00798 template <typename Box>
00799 void shrink_bounding_box(Box& box,
00800 Complexity_Class complexity = ANY_COMPLEXITY) const;
00801
00803
00819 bool OK(bool check_not_empty = false) const;
00820
00822
00824
00825
00834 void add_constraint(const Constraint& c);
00835
00847 bool add_constraint_and_minimize(const Constraint& c);
00848
00858 void add_generator(const Generator& g);
00859
00872 bool add_generator_and_minimize(const Generator& g);
00873
00882 void add_congruence(const Congruence& cg);
00883
00896 void add_constraints(const Constraint_System& cs);
00897
00914 void add_recycled_constraints(Constraint_System& cs);
00915
00931 bool add_constraints_and_minimize(const Constraint_System& cs);
00932
00952 bool add_recycled_constraints_and_minimize(Constraint_System& cs);
00953
00967 void add_generators(const Generator_System& gs);
00968
00986 void add_recycled_generators(Generator_System& gs);
00987
01004 bool add_generators_and_minimize(const Generator_System& gs);
01005
01026 bool add_recycled_generators_and_minimize(Generator_System& gs);
01027
01040 void add_congruences(const Congruence_System& cgs);
01041
01050 void intersection_assign(const Polyhedron& y);
01051
01063 bool intersection_assign_and_minimize(const Polyhedron& y);
01064
01073 void poly_hull_assign(const Polyhedron& y);
01074
01086 bool poly_hull_assign_and_minimize(const Polyhedron& y);
01087
01089 void upper_bound_assign(const Polyhedron& y);
01090
01100 void poly_difference_assign(const Polyhedron& y);
01101
01103 void difference_assign(const Polyhedron& y);
01104
01194 void affine_image(Variable var,
01195 const Linear_Expression& expr,
01196 Coefficient_traits::const_reference denominator
01197 = Coefficient_one());
01198
01286 void affine_preimage(Variable var,
01287 const Linear_Expression& expr,
01288 Coefficient_traits::const_reference denominator
01289 = Coefficient_one());
01290
01317 void generalized_affine_image(Variable var,
01318 const Relation_Symbol relsym,
01319 const Linear_Expression& expr,
01320 Coefficient_traits::const_reference denominator
01321 = Coefficient_one());
01322
01349 void
01350 generalized_affine_preimage(Variable var,
01351 const Relation_Symbol relsym,
01352 const Linear_Expression& expr,
01353 Coefficient_traits::const_reference denominator
01354 = Coefficient_one());
01355
01376 void generalized_affine_image(const Linear_Expression& lhs,
01377 const Relation_Symbol relsym,
01378 const Linear_Expression& rhs);
01379
01400 void generalized_affine_preimage(const Linear_Expression& lhs,
01401 const Relation_Symbol relsym,
01402 const Linear_Expression& rhs);
01403
01430 void bounded_affine_image(Variable var,
01431 const Linear_Expression& lb_expr,
01432 const Linear_Expression& ub_expr,
01433 Coefficient_traits::const_reference denominator
01434 = Coefficient_one());
01435
01462 void bounded_affine_preimage(Variable var,
01463 const Linear_Expression& lb_expr,
01464 const Linear_Expression& ub_expr,
01465 Coefficient_traits::const_reference denominator
01466 = Coefficient_one());
01467
01476 void time_elapse_assign(const Polyhedron& y);
01477
01479 void topological_closure_assign();
01480
01497 void BHRZ03_widening_assign(const Polyhedron& y, unsigned* tp = 0);
01498
01519 void limited_BHRZ03_extrapolation_assign(const Polyhedron& y,
01520 const Constraint_System& cs,
01521 unsigned* tp = 0);
01522
01545 void bounded_BHRZ03_extrapolation_assign(const Polyhedron& y,
01546 const Constraint_System& cs,
01547 unsigned* tp = 0);
01548
01565 void H79_widening_assign(const Polyhedron& y, unsigned* tp = 0);
01566
01587 void limited_H79_extrapolation_assign(const Polyhedron& y,
01588 const Constraint_System& cs,
01589 unsigned* tp = 0);
01590
01613 void bounded_H79_extrapolation_assign(const Polyhedron& y,
01614 const Constraint_System& cs,
01615 unsigned* tp = 0);
01616
01618
01620
01621
01647 void add_space_dimensions_and_embed(dimension_type m);
01648
01674 void add_space_dimensions_and_project(dimension_type m);
01675
01687 void concatenate_assign(const Polyhedron& y);
01688
01690
01699 void remove_space_dimensions(const Variables_Set& to_be_removed);
01700
01709 void remove_higher_space_dimensions(dimension_type new_dimension);
01710
01751 template <typename Partial_Function>
01752 void map_space_dimensions(const Partial_Function& pfunc);
01753
01755
01775 void expand_space_dimension(Variable var, dimension_type m);
01776
01778
01800 void fold_space_dimensions(const Variables_Set& to_be_folded, Variable var);
01801
01803
01804 friend bool Parma_Polyhedra_Library::operator==(const Polyhedron& x,
01805 const Polyhedron& y);
01806
01808
01809
01811 ~Polyhedron();
01812
01820 void swap(Polyhedron& y);
01821
01822 PPL_OUTPUT_DECLARATIONS;
01823
01824 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
01825
01830 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
01831 bool ascii_load(std::istream& s);
01832
01834 memory_size_type total_memory_in_bytes() const;
01835
01837 memory_size_type external_memory_in_bytes() const;
01838
01840
01841 private:
01843 Constraint_System con_sys;
01844
01846 Generator_System gen_sys;
01847
01849 Saturation_Matrix sat_c;
01850
01852 Saturation_Matrix sat_g;
01853
01854 #define PPL_IN_Polyhedron_CLASS
01855 #include "Ph_Status.idefs.hh"
01856 #undef PPL_IN_Polyhedron_CLASS
01857
01859 Status status;
01860
01862 dimension_type space_dim;
01863
01865 Topology topology() const;
01866
01871 bool is_necessarily_closed() const;
01872
01874
01875
01877
01881 bool marked_empty() const;
01882
01884 bool constraints_are_up_to_date() const;
01885
01887 bool generators_are_up_to_date() const;
01888
01890
01894 bool constraints_are_minimized() const;
01895
01897
01901 bool generators_are_minimized() const;
01902
01904 bool has_pending_constraints() const;
01905
01907 bool has_pending_generators() const;
01908
01913 bool has_something_pending() const;
01914
01916 bool can_have_something_pending() const;
01917
01922 bool sat_c_is_up_to_date() const;
01923
01928 bool sat_g_is_up_to_date() const;
01929
01931
01933
01934
01939 void set_zero_dim_univ();
01940
01945 void set_empty();
01946
01948 void set_constraints_up_to_date();
01949
01951 void set_generators_up_to_date();
01952
01954 void set_constraints_minimized();
01955
01957 void set_generators_minimized();
01958
01960 void set_constraints_pending();
01961
01963 void set_generators_pending();
01964
01966 void set_sat_c_up_to_date();
01967
01969 void set_sat_g_up_to_date();
01970
01972
01974
01975
01977 void clear_empty();
01978
01980
01984 void clear_constraints_up_to_date();
01985
01987
01991 void clear_generators_up_to_date();
01992
01994 void clear_constraints_minimized();
01995
01997 void clear_generators_minimized();
01998
02000 void clear_pending_constraints();
02001
02003 void clear_pending_generators();
02004
02006 void clear_sat_c_up_to_date();
02007
02009 void clear_sat_g_up_to_date();
02010
02012
02014
02015
02027 bool process_pending() const;
02028
02030
02037 bool process_pending_constraints() const;
02038
02040
02043 void process_pending_generators() const;
02044
02052 void remove_pending_to_obtain_constraints() const;
02053
02065 bool remove_pending_to_obtain_generators() const;
02066
02068
02070
02071
02073
02078 void update_constraints() const;
02079
02081
02092 bool update_generators() const;
02093
02095
02109 void update_sat_c() const;
02110
02112
02126 void update_sat_g() const;
02127
02129
02138 void obtain_sorted_constraints() const;
02139
02141
02150 void obtain_sorted_generators() const;
02151
02153
02160 void obtain_sorted_constraints_with_sat_c() const;
02161
02163
02170 void obtain_sorted_generators_with_sat_g() const;
02171
02173
02175
02176
02178
02186 bool minimize() const;
02187
02189
02194 bool strongly_minimize_constraints() const;
02195
02197
02202 bool strongly_minimize_generators() const;
02203
02205
02206 enum Three_Valued_Boolean {
02207 TVB_TRUE,
02208 TVB_FALSE,
02209 TVB_DONT_KNOW
02210 };
02211
02213 Three_Valued_Boolean quick_equivalence_test(const Polyhedron& y) const;
02214
02216 bool is_included_in(const Polyhedron& y) const;
02217
02219
02235 bool bounds(const Linear_Expression& expr, bool from_above) const;
02236
02238
02268 bool max_min(const Linear_Expression& expr,
02269 const bool maximize,
02270 Coefficient& ext_n, Coefficient& ext_d, bool& included,
02271 Generator& point) const;
02272
02274
02275
02280 void select_CH78_constraints(const Polyhedron& y,
02281 Constraint_System& cs_selected) const;
02282
02288 void select_H79_constraints(const Polyhedron& y,
02289 Constraint_System& cs_selected,
02290 Constraint_System& cs_not_selected) const;
02291
02292 bool BHRZ03_combining_constraints(const Polyhedron& y,
02293 const BHRZ03_Certificate& y_cert,
02294 const Polyhedron& H79,
02295 const Constraint_System& x_minus_H79_con_sys);
02296
02297 bool BHRZ03_evolving_points(const Polyhedron& y,
02298 const BHRZ03_Certificate& y_cert,
02299 const Polyhedron& H79);
02300
02301 bool BHRZ03_evolving_rays(const Polyhedron& y,
02302 const BHRZ03_Certificate& y_cert,
02303 const Polyhedron& H79);
02304
02306
02308
02333 static void add_space_dimensions(Linear_System& mat1,
02334 Linear_System& mat2,
02335 Saturation_Matrix& sat1,
02336 Saturation_Matrix& sat2,
02337 dimension_type add_dim);
02338
02340
02341
02343
02344 static bool minimize(bool con_to_gen,
02345 Linear_System& source,
02346 Linear_System& dest,
02347 Saturation_Matrix& sat);
02348
02353
02354 static bool add_and_minimize(bool con_to_gen,
02355 Linear_System& source1,
02356 Linear_System& dest,
02357 Saturation_Matrix& sat,
02358 const Linear_System& source2);
02359
02364
02365 static bool add_and_minimize(bool con_to_gen,
02366 Linear_System& source,
02367 Linear_System& dest,
02368 Saturation_Matrix& sat);
02369
02371
02372 static dimension_type conversion(Linear_System& source,
02373 dimension_type start,
02374 Linear_System& dest,
02375 Saturation_Matrix& sat,
02376 dimension_type num_lines_or_equalities);
02377
02382
02383 static int simplify(Linear_System& mat, Saturation_Matrix& sat);
02384
02386
02387 template <typename T> friend class Parma_Polyhedra_Library::BD_Shape;
02388 friend class Parma_Polyhedra_Library::BHRZ03_Certificate;
02389 friend class Parma_Polyhedra_Library::H79_Certificate;
02390
02391
02393
02394 protected:
02395 void throw_runtime_error(const char* method) const;
02396 void throw_invalid_argument(const char* method, const char* reason) const;
02397
02398 void throw_topology_incompatible(const char* method,
02399 const char* ph_name,
02400 const Polyhedron& ph) const;
02401 void throw_topology_incompatible(const char* method,
02402 const char* c_name,
02403 const Constraint& c) const;
02404 void throw_topology_incompatible(const char* method,
02405 const char* g_name,
02406 const Generator& g) const;
02407 void throw_topology_incompatible(const char* method,
02408 const char* cs_name,
02409 const Constraint_System& cs) const;
02410 void throw_topology_incompatible(const char* method,
02411 const char* gs_name,
02412 const Generator_System& gs) const;
02413
02414 void throw_dimension_incompatible(const char* method,
02415 const char* other_name,
02416 dimension_type other_dim) const;
02417 void throw_dimension_incompatible(const char* method,
02418 const char* ph_name,
02419 const Polyhedron& ph) const;
02420 void throw_dimension_incompatible(const char* method,
02421 const char* e_name,
02422 const Linear_Expression& e) const;
02423 void throw_dimension_incompatible(const char* method,
02424 const char* c_name,
02425 const Constraint& c) const;
02426 void throw_dimension_incompatible(const char* method,
02427 const char* g_name,
02428 const Generator& g) const;
02429 void throw_dimension_incompatible(const char* method,
02430 const char* cg_name,
02431 const Congruence& cg) const;
02432 void throw_dimension_incompatible(const char* method,
02433 const char* cs_name,
02434 const Constraint_System& cs) const;
02435 void throw_dimension_incompatible(const char* method,
02436 const char* gs_name,
02437 const Generator_System& gs) const;
02438 void throw_dimension_incompatible(const char* method,
02439 const char* cgs_name,
02440 const Congruence_System& cgs) const;
02441 void throw_dimension_incompatible(const char* method,
02442 const char* var_name,
02443 const Variable var) const;
02444 void throw_dimension_incompatible(const char* method,
02445 dimension_type required_space_dim) const;
02446
02447
02448
02449 static void throw_space_dimension_overflow(Topology topol,
02450 const char* method,
02451 const char* reason);
02452
02453 void throw_invalid_generator(const char* method,
02454 const char* g_name) const;
02455 void throw_invalid_generators(const char* method,
02456 const char* gs_name) const;
02458
02459 };
02460
02461
02462 namespace std {
02463
02465
02466 void swap(Parma_Polyhedra_Library::Polyhedron& x,
02467 Parma_Polyhedra_Library::Polyhedron& y);
02468
02469 }
02470
02471 #include "Ph_Status.inlines.hh"
02472 #include "Polyhedron.inlines.hh"
02473 #include "Polyhedron.templates.hh"
02474
02475 #endif // !defined(PPL_Polyhedron_defs_hh)