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 "Variables_Set.types.hh"
00030 #include "Linear_Expression.types.hh"
00031 #include "Constraint_System.defs.hh"
00032 #include "Constraint_System.inlines.hh"
00033 #include "Generator_System.defs.hh"
00034 #include "Generator_System.inlines.hh"
00035 #include "Congruence_System.defs.hh"
00036 #include "Congruence_System.inlines.hh"
00037 #include "Grid_Generator_System.defs.hh"
00038 #include "Grid_Generator_System.inlines.hh"
00039 #include "Bit_Matrix.defs.hh"
00040 #include "Constraint.types.hh"
00041 #include "Generator.types.hh"
00042 #include "Congruence.types.hh"
00043 #include "Poly_Con_Relation.defs.hh"
00044 #include "Poly_Gen_Relation.defs.hh"
00045 #include "BHRZ03_Certificate.types.hh"
00046 #include "H79_Certificate.types.hh"
00047 #include "Box.types.hh"
00048 #include "BD_Shape.types.hh"
00049 #include "Octagonal_Shape.types.hh"
00050 #include <vector>
00051 #include <iosfwd>
00052
00053 namespace Parma_Polyhedra_Library {
00054
00055 namespace IO_Operators {
00056
00058
00066 std::ostream&
00067 operator<<(std::ostream& s, const Polyhedron& ph);
00068
00069 }
00070
00079 bool operator==(const Polyhedron& x, const Polyhedron& y);
00080
00089 bool operator!=(const Polyhedron& x, const Polyhedron& y);
00090
00091 namespace Interfaces {
00092
00093 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00094
00098 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
00099 bool is_necessarily_closed_for_interfaces(const Polyhedron& ph);
00100
00101 }
00102
00103 }
00104
00105
00107
00364 class Parma_Polyhedra_Library::Polyhedron {
00365 public:
00367 typedef Coefficient coefficient_type;
00368
00370 static dimension_type max_space_dimension();
00371
00376 static bool can_recycle_constraint_systems();
00377
00379 static void initialize();
00380
00382 static void finalize();
00383
00387 static bool can_recycle_congruence_systems();
00388
00389 protected:
00391
00401 Polyhedron(Topology topol,
00402 dimension_type num_dimensions,
00403 Degenerate_Element kind);
00404
00406
00409 Polyhedron(const Polyhedron& y,
00410 Complexity_Class complexity = ANY_COMPLEXITY);
00411
00413
00425 Polyhedron(Topology topol, const Constraint_System& cs);
00426
00428
00446 Polyhedron(Topology topol, Constraint_System& cs, Recycle_Input dummy);
00447
00449
00462 Polyhedron(Topology topol, const Generator_System& gs);
00463
00465
00484 Polyhedron(Topology topol, Generator_System& gs, Recycle_Input dummy);
00485
00487
00500 template <typename Interval>
00501 Polyhedron(Topology topol, const Box<Interval>& box,
00502 Complexity_Class complexity = ANY_COMPLEXITY);
00503
00508 Polyhedron& operator=(const Polyhedron& y);
00509
00510 public:
00512
00513
00515 dimension_type space_dimension() const;
00516
00522 dimension_type affine_dimension() const;
00523
00525 const Constraint_System& constraints() const;
00526
00528 const Constraint_System& minimized_constraints() const;
00529
00531 const Generator_System& generators() const;
00532
00534 const Generator_System& minimized_generators() const;
00535
00537 Congruence_System congruences() const;
00538
00544 Congruence_System minimized_congruences() const;
00545
00547 Grid_Generator_System grid_generators() const;
00548
00550 Grid_Generator_System minimized_grid_generators() const;
00551
00559 Poly_Con_Relation relation_with(const Constraint& c) const;
00560
00568 Poly_Gen_Relation relation_with(const Generator& g) const;
00569
00577 Poly_Con_Relation relation_with(const Congruence& cg) const;
00578
00583 bool is_empty() const;
00584
00589 bool is_universe() const;
00590
00595 bool is_topologically_closed() const;
00596
00598
00603 bool is_disjoint_from(const Polyhedron& y) const;
00604
00606 bool is_discrete() const;
00607
00612 bool is_bounded() const;
00613
00618 bool contains_integer_point() const;
00619
00627 bool constrains(Variable var) const;
00628
00636 bool bounds_from_above(const Linear_Expression& expr) const;
00637
00645 bool bounds_from_below(const Linear_Expression& expr) const;
00646
00671 bool maximize(const Linear_Expression& expr,
00672 Coefficient& sup_n, Coefficient& sup_d, bool& maximum) const;
00673
00702 bool maximize(const Linear_Expression& expr,
00703 Coefficient& sup_n, Coefficient& sup_d, bool& maximum,
00704 Generator& g) const;
00705
00730 bool minimize(const Linear_Expression& expr,
00731 Coefficient& inf_n, Coefficient& inf_d, bool& minimum) const;
00732
00761 bool minimize(const Linear_Expression& expr,
00762 Coefficient& inf_n, Coefficient& inf_d, bool& minimum,
00763 Generator& g) const;
00764
00766
00771 bool contains(const Polyhedron& y) const;
00772
00774
00779 bool strictly_contains(const Polyhedron& y) const;
00780
00782
00798 bool OK(bool check_not_empty = false) const;
00799
00801
00803
00804
00817 void add_constraint(const Constraint& c);
00818
00837 bool add_constraint_and_minimize(const Constraint& c);
00838
00848 void add_generator(const Generator& g);
00849
00865 bool add_generator_and_minimize(const Generator& g);
00866
00876 void add_congruence(const Congruence& cg);
00877
00894 bool add_congruence_and_minimize(const Congruence& cg);
00895
00908 void add_constraints(const Constraint_System& cs);
00909
00926 void add_recycled_constraints(Constraint_System& cs);
00927
00946 bool add_constraints_and_minimize(const Constraint_System& cs);
00947
00970 bool add_recycled_constraints_and_minimize(Constraint_System& cs);
00971
00985 void add_generators(const Generator_System& gs);
00986
01004 void add_recycled_generators(Generator_System& gs);
01005
01025 bool add_generators_and_minimize(const Generator_System& gs);
01026
01050 bool add_recycled_generators_and_minimize(Generator_System& gs);
01051
01064 void add_congruences(const Congruence_System& cgs);
01065
01085 bool add_congruences_and_minimize(const Congruence_System& cgs);
01086
01103 void add_recycled_congruences(Congruence_System& cgs);
01104
01128 bool add_recycled_congruences_and_minimize(Congruence_System& cgs);
01129
01136 void refine_with_constraint(const Constraint& c);
01137
01144 void refine_with_congruence(const Congruence& cg);
01145
01156 void refine_with_constraints(const Constraint_System& cs);
01157
01168 void refine_with_congruences(const Congruence_System& cgs);
01169
01180 void unconstrain(Variable var);
01181
01194 void unconstrain(const Variables_Set& to_be_unconstrained);
01195
01204 void intersection_assign(const Polyhedron& y);
01205
01220 bool intersection_assign_and_minimize(const Polyhedron& y);
01221
01230 void poly_hull_assign(const Polyhedron& y);
01231
01246 bool poly_hull_assign_and_minimize(const Polyhedron& y);
01247
01249 void upper_bound_assign(const Polyhedron& y);
01250
01260 void poly_difference_assign(const Polyhedron& y);
01261
01263 void difference_assign(const Polyhedron& y);
01264
01274 bool simplify_using_context_assign(const Polyhedron& y);
01275
01365 void affine_image(Variable var,
01366 const Linear_Expression& expr,
01367 Coefficient_traits::const_reference denominator
01368 = Coefficient_one());
01369
01457 void affine_preimage(Variable var,
01458 const Linear_Expression& expr,
01459 Coefficient_traits::const_reference denominator
01460 = Coefficient_one());
01461
01488 void generalized_affine_image(Variable var,
01489 Relation_Symbol relsym,
01490 const Linear_Expression& expr,
01491 Coefficient_traits::const_reference denominator
01492 = Coefficient_one());
01493
01520 void
01521 generalized_affine_preimage(Variable var,
01522 Relation_Symbol relsym,
01523 const Linear_Expression& expr,
01524 Coefficient_traits::const_reference denominator
01525 = Coefficient_one());
01526
01547 void generalized_affine_image(const Linear_Expression& lhs,
01548 Relation_Symbol relsym,
01549 const Linear_Expression& rhs);
01550
01571 void generalized_affine_preimage(const Linear_Expression& lhs,
01572 Relation_Symbol relsym,
01573 const Linear_Expression& rhs);
01574
01601 void bounded_affine_image(Variable var,
01602 const Linear_Expression& lb_expr,
01603 const Linear_Expression& ub_expr,
01604 Coefficient_traits::const_reference denominator
01605 = Coefficient_one());
01606
01633 void bounded_affine_preimage(Variable var,
01634 const Linear_Expression& lb_expr,
01635 const Linear_Expression& ub_expr,
01636 Coefficient_traits::const_reference denominator
01637 = Coefficient_one());
01638
01647 void time_elapse_assign(const Polyhedron& y);
01648
01650 void topological_closure_assign();
01651
01668 void BHRZ03_widening_assign(const Polyhedron& y, unsigned* tp = 0);
01669
01690 void limited_BHRZ03_extrapolation_assign(const Polyhedron& y,
01691 const Constraint_System& cs,
01692 unsigned* tp = 0);
01693
01716 void bounded_BHRZ03_extrapolation_assign(const Polyhedron& y,
01717 const Constraint_System& cs,
01718 unsigned* tp = 0);
01719
01736 void H79_widening_assign(const Polyhedron& y, unsigned* tp = 0);
01737
01739 void widening_assign(const Polyhedron& y, unsigned* tp = 0);
01740
01761 void limited_H79_extrapolation_assign(const Polyhedron& y,
01762 const Constraint_System& cs,
01763 unsigned* tp = 0);
01764
01787 void bounded_H79_extrapolation_assign(const Polyhedron& y,
01788 const Constraint_System& cs,
01789 unsigned* tp = 0);
01790
01792
01794
01795
01821 void add_space_dimensions_and_embed(dimension_type m);
01822
01848 void add_space_dimensions_and_project(dimension_type m);
01849
01861 void concatenate_assign(const Polyhedron& y);
01862
01864
01873 void remove_space_dimensions(const Variables_Set& to_be_removed);
01874
01883 void remove_higher_space_dimensions(dimension_type new_dimension);
01884
01925 template <typename Partial_Function>
01926 void map_space_dimensions(const Partial_Function& pfunc);
01927
01929
01949 void expand_space_dimension(Variable var, dimension_type m);
01950
01952
01974 void fold_space_dimensions(const Variables_Set& to_be_folded, Variable var);
01975
01977
01978 friend bool operator==(const Polyhedron& x, const Polyhedron& y);
01979
01981
01982
01984 ~Polyhedron();
01985
01993 void swap(Polyhedron& y);
01994
01995 PPL_OUTPUT_DECLARATIONS
01996
01997 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
01998
02003 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
02004 bool ascii_load(std::istream& s);
02005
02007 memory_size_type total_memory_in_bytes() const;
02008
02010 memory_size_type external_memory_in_bytes() const;
02011
02018 int32_t hash_code() const;
02019
02021
02022 private:
02024 Constraint_System con_sys;
02025
02027 Generator_System gen_sys;
02028
02030 Bit_Matrix sat_c;
02031
02033 Bit_Matrix sat_g;
02034
02035 #define PPL_IN_Polyhedron_CLASS
02036 #include "Ph_Status.idefs.hh"
02037 #undef PPL_IN_Polyhedron_CLASS
02038
02040 Status status;
02041
02043 dimension_type space_dim;
02044
02046 Topology topology() const;
02047
02052 bool is_necessarily_closed() const;
02053
02054 friend bool
02055 Parma_Polyhedra_Library::Interfaces
02056 ::is_necessarily_closed_for_interfaces(const Polyhedron&);
02057
02065 void refine_no_check(const Constraint& c);
02066
02068
02069
02071
02075 bool marked_empty() const;
02076
02078 bool constraints_are_up_to_date() const;
02079
02081 bool generators_are_up_to_date() const;
02082
02084
02088 bool constraints_are_minimized() const;
02089
02091
02095 bool generators_are_minimized() const;
02096
02098 bool has_pending_constraints() const;
02099
02101 bool has_pending_generators() const;
02102
02107 bool has_something_pending() const;
02108
02110 bool can_have_something_pending() const;
02111
02116 bool sat_c_is_up_to_date() const;
02117
02122 bool sat_g_is_up_to_date() const;
02123
02125
02127
02128
02133 void set_zero_dim_univ();
02134
02139 void set_empty();
02140
02142 void set_constraints_up_to_date();
02143
02145 void set_generators_up_to_date();
02146
02148 void set_constraints_minimized();
02149
02151 void set_generators_minimized();
02152
02154 void set_constraints_pending();
02155
02157 void set_generators_pending();
02158
02160 void set_sat_c_up_to_date();
02161
02163 void set_sat_g_up_to_date();
02164
02166
02168
02169
02171 void clear_empty();
02172
02174
02178 void clear_constraints_up_to_date();
02179
02181
02185 void clear_generators_up_to_date();
02186
02188 void clear_constraints_minimized();
02189
02191 void clear_generators_minimized();
02192
02194 void clear_pending_constraints();
02195
02197 void clear_pending_generators();
02198
02200 void clear_sat_c_up_to_date();
02201
02203 void clear_sat_g_up_to_date();
02204
02206
02208
02209
02221 bool process_pending() const;
02222
02224
02231 bool process_pending_constraints() const;
02232
02234
02237 void process_pending_generators() const;
02238
02246 void remove_pending_to_obtain_constraints() const;
02247
02259 bool remove_pending_to_obtain_generators() const;
02260
02262
02264
02265
02267
02272 void update_constraints() const;
02273
02275
02286 bool update_generators() const;
02287
02289
02303 void update_sat_c() const;
02304
02306
02320 void update_sat_g() const;
02321
02323
02332 void obtain_sorted_constraints() const;
02333
02335
02344 void obtain_sorted_generators() const;
02345
02347
02354 void obtain_sorted_constraints_with_sat_c() const;
02355
02357
02364 void obtain_sorted_generators_with_sat_g() const;
02365
02367
02369
02370
02372
02380 bool minimize() const;
02381
02383
02388 bool strongly_minimize_constraints() const;
02389
02391
02396 bool strongly_minimize_generators() const;
02397
02399 Constraint_System simplified_constraints() const;
02400
02402
02403 enum Three_Valued_Boolean {
02404 TVB_TRUE,
02405 TVB_FALSE,
02406 TVB_DONT_KNOW
02407 };
02408
02410 Three_Valued_Boolean quick_equivalence_test(const Polyhedron& y) const;
02411
02413 bool is_included_in(const Polyhedron& y) const;
02414
02416
02432 bool bounds(const Linear_Expression& expr, bool from_above) const;
02433
02435
02465 bool max_min(const Linear_Expression& expr,
02466 bool maximize,
02467 Coefficient& ext_n, Coefficient& ext_d, bool& included,
02468 Generator& g) const;
02469
02471
02472
02477 void select_CH78_constraints(const Polyhedron& y,
02478 Constraint_System& cs_selected) const;
02479
02485 void select_H79_constraints(const Polyhedron& y,
02486 Constraint_System& cs_selected,
02487 Constraint_System& cs_not_selected) const;
02488
02489 bool BHRZ03_combining_constraints(const Polyhedron& y,
02490 const BHRZ03_Certificate& y_cert,
02491 const Polyhedron& H79,
02492 const Constraint_System& x_minus_H79_con_sys);
02493
02494 bool BHRZ03_evolving_points(const Polyhedron& y,
02495 const BHRZ03_Certificate& y_cert,
02496 const Polyhedron& H79);
02497
02498 bool BHRZ03_evolving_rays(const Polyhedron& y,
02499 const BHRZ03_Certificate& y_cert,
02500 const Polyhedron& H79);
02501
02503
02505
02530 static void add_space_dimensions(Linear_System& mat1,
02531 Linear_System& mat2,
02532 Bit_Matrix& sat1,
02533 Bit_Matrix& sat2,
02534 dimension_type add_dim);
02535
02537
02538
02540
02541 static bool minimize(bool con_to_gen,
02542 Linear_System& source,
02543 Linear_System& dest,
02544 Bit_Matrix& sat);
02545
02550
02551 static bool add_and_minimize(bool con_to_gen,
02552 Linear_System& source1,
02553 Linear_System& dest,
02554 Bit_Matrix& sat,
02555 const Linear_System& source2);
02556
02561
02562 static bool add_and_minimize(bool con_to_gen,
02563 Linear_System& source,
02564 Linear_System& dest,
02565 Bit_Matrix& sat);
02566
02568
02569 static dimension_type conversion(Linear_System& source,
02570 dimension_type start,
02571 Linear_System& dest,
02572 Bit_Matrix& sat,
02573 dimension_type num_lines_or_equalities);
02574
02579
02580 static dimension_type simplify(Linear_System& mat, Bit_Matrix& sat);
02581
02583
02591 static dimension_type* simplify_num_saturators_p;
02592
02599 static size_t simplify_num_saturators_size;
02600
02601 template <typename Interval> friend class Parma_Polyhedra_Library::Box;
02602 template <typename T> friend class Parma_Polyhedra_Library::BD_Shape;
02603 template <typename T> friend class Parma_Polyhedra_Library::Octagonal_Shape;
02604 friend class Parma_Polyhedra_Library::Grid;
02605 friend class Parma_Polyhedra_Library::BHRZ03_Certificate;
02606 friend class Parma_Polyhedra_Library::H79_Certificate;
02607
02608
02610
02611 protected:
02612 void throw_runtime_error(const char* method) const;
02613 void throw_invalid_argument(const char* method, const char* reason) const;
02614
02615 void throw_topology_incompatible(const char* method,
02616 const char* ph_name,
02617 const Polyhedron& ph) const;
02618 void throw_topology_incompatible(const char* method,
02619 const char* c_name,
02620 const Constraint& c) const;
02621 void throw_topology_incompatible(const char* method,
02622 const char* g_name,
02623 const Generator& g) const;
02624 void throw_topology_incompatible(const char* method,
02625 const char* cs_name,
02626 const Constraint_System& cs) const;
02627 void throw_topology_incompatible(const char* method,
02628 const char* gs_name,
02629 const Generator_System& gs) const;
02630
02631 void throw_dimension_incompatible(const char* method,
02632 const char* other_name,
02633 dimension_type other_dim) const;
02634 void throw_dimension_incompatible(const char* method,
02635 const char* ph_name,
02636 const Polyhedron& ph) const;
02637 void throw_dimension_incompatible(const char* method,
02638 const char* e_name,
02639 const Linear_Expression& e) const;
02640 void throw_dimension_incompatible(const char* method,
02641 const char* c_name,
02642 const Constraint& c) const;
02643 void throw_dimension_incompatible(const char* method,
02644 const char* g_name,
02645 const Generator& g) const;
02646 void throw_dimension_incompatible(const char* method,
02647 const char* cg_name,
02648 const Congruence& cg) const;
02649 void throw_dimension_incompatible(const char* method,
02650 const char* cs_name,
02651 const Constraint_System& cs) const;
02652 void throw_dimension_incompatible(const char* method,
02653 const char* gs_name,
02654 const Generator_System& gs) const;
02655 void throw_dimension_incompatible(const char* method,
02656 const char* cgs_name,
02657 const Congruence_System& cgs) const;
02658 void throw_dimension_incompatible(const char* method,
02659 const char* var_name,
02660 Variable var) const;
02661 void throw_dimension_incompatible(const char* method,
02662 dimension_type required_space_dim) const;
02663
02664
02665
02666 static void throw_space_dimension_overflow(Topology topol,
02667 const char* method,
02668 const char* reason);
02669
02670 void throw_invalid_generator(const char* method,
02671 const char* g_name) const;
02672 void throw_invalid_generators(const char* method,
02673 const char* gs_name) const;
02675
02676 };
02677
02678
02679 namespace std {
02680
02682
02683 void swap(Parma_Polyhedra_Library::Polyhedron& x,
02684 Parma_Polyhedra_Library::Polyhedron& y);
02685
02686 }
02687
02688 #include "Ph_Status.inlines.hh"
02689 #include "Polyhedron.inlines.hh"
02690 #include "Polyhedron.templates.hh"
02691
02692 #endif // !defined(PPL_Polyhedron_defs_hh)