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_Pointset_Powerset_defs_hh
00024 #define PPL_Pointset_Powerset_defs_hh
00025
00026 #include "Pointset_Powerset.types.hh"
00027 #include "globals.defs.hh"
00028 #include "BHRZ03_Certificate.types.hh"
00029 #include "Constraint.types.hh"
00030 #include "Constraint_System.types.hh"
00031 #include "Congruence.types.hh"
00032 #include "Congruence_System.types.hh"
00033 #include "C_Polyhedron.defs.hh"
00034 #include "NNC_Polyhedron.defs.hh"
00035 #include "Polyhedron.defs.hh"
00036 #include "Grid.defs.hh"
00037 #include "Partially_Reduced_Product.defs.hh"
00038 #include "Variables_Set.types.hh"
00039 #include "Determinate.defs.hh"
00040 #include "Powerset.defs.hh"
00041 #include "Poly_Con_Relation.defs.hh"
00042 #include "Poly_Gen_Relation.defs.hh"
00043 #include <iosfwd>
00044 #include <list>
00045 #include <map>
00046
00048
00060 template <typename PS>
00061 class Parma_Polyhedra_Library::Pointset_Powerset
00062 : public Parma_Polyhedra_Library::Powerset
00063 <Parma_Polyhedra_Library::Determinate<PS> > {
00064 public:
00065 typedef PS element_type;
00066
00067 private:
00068 typedef Determinate<PS> CS;
00069 typedef Powerset<CS> Base;
00070
00071 public:
00073 static dimension_type max_space_dimension();
00074
00076
00077
00079
00086 explicit
00087 Pointset_Powerset(dimension_type num_dimensions = 0,
00088 Degenerate_Element kind = UNIVERSE);
00089
00091
00094 Pointset_Powerset(const Pointset_Powerset& y,
00095 Complexity_Class complexity = ANY_COMPLEXITY);
00096
00107 template <typename QH>
00108 explicit Pointset_Powerset(const Pointset_Powerset<QH>& y,
00109 Complexity_Class complexity = ANY_COMPLEXITY);
00110
00116 template <typename QH1, typename QH2, typename R>
00117 explicit
00118 Pointset_Powerset(const Partially_Reduced_Product<QH1, QH2, R>& prp,
00119 Complexity_Class complexity = ANY_COMPLEXITY);
00120
00125 explicit Pointset_Powerset(const Constraint_System& cs);
00126
00131 explicit Pointset_Powerset(const Congruence_System& cgs);
00132
00133
00135
00152 explicit Pointset_Powerset(const C_Polyhedron& ph,
00153 Complexity_Class complexity = ANY_COMPLEXITY);
00154
00156
00173 explicit Pointset_Powerset(const NNC_Polyhedron& ph,
00174 Complexity_Class complexity = ANY_COMPLEXITY);
00175
00176
00178
00193 explicit Pointset_Powerset(const Grid& gr,
00194 Complexity_Class complexity = ANY_COMPLEXITY);
00195
00197
00213 template <typename T>
00214 explicit Pointset_Powerset(const Octagonal_Shape<T>& os,
00215 Complexity_Class complexity = ANY_COMPLEXITY);
00216
00218
00234 template <typename T>
00235 explicit Pointset_Powerset(const BD_Shape<T>& bds,
00236 Complexity_Class complexity = ANY_COMPLEXITY);
00237
00239
00254 template <typename Interval>
00255 explicit Pointset_Powerset(const Box<Interval>& box,
00256 Complexity_Class complexity = ANY_COMPLEXITY);
00257
00259
00261
00262
00264 dimension_type space_dimension() const;
00265
00267 dimension_type affine_dimension() const;
00268
00273 bool is_empty() const;
00274
00279 bool is_universe() const;
00280
00285 bool is_topologically_closed() const;
00286
00291 bool is_bounded() const;
00292
00294
00299 bool is_disjoint_from(const Pointset_Powerset& y) const;
00300
00302 bool is_discrete() const;
00303
00323 bool constrains(Variable var) const;
00324
00332 bool bounds_from_above(const Linear_Expression& expr) const;
00333
00341 bool bounds_from_below(const Linear_Expression& expr) const;
00342
00367 bool maximize(const Linear_Expression& expr,
00368 Coefficient& sup_n, Coefficient& sup_d, bool& maximum) const;
00369
00398 bool maximize(const Linear_Expression& expr,
00399 Coefficient& sup_n, Coefficient& sup_d, bool& maximum,
00400 Generator& g) const;
00401
00426 bool minimize(const Linear_Expression& expr,
00427 Coefficient& inf_n, Coefficient& inf_d, bool& minimum) const;
00428
00429
00458 bool minimize(const Linear_Expression& expr,
00459 Coefficient& inf_n, Coefficient& inf_d, bool& minimum,
00460 Generator& g) const;
00461
00473 bool geometrically_covers(const Pointset_Powerset& y) const;
00474
00486 bool geometrically_equals(const Pointset_Powerset& y) const;
00487
00496 bool contains(const Pointset_Powerset& y) const;
00497
00506 bool strictly_contains(const Pointset_Powerset& y) const;
00507
00512 bool contains_integer_point() const;
00513
00521 Poly_Con_Relation relation_with(const Constraint& c) const;
00522
00530 Poly_Gen_Relation relation_with(const Generator& g) const;
00531
00539 Poly_Con_Relation relation_with(const Congruence& cg) const;
00540
00545 memory_size_type total_memory_in_bytes() const;
00546
00551 memory_size_type external_memory_in_bytes() const;
00552
00559 int32_t hash_code() const;
00560
00562 bool OK() const;
00563
00565
00567
00568
00570
00574 void add_disjunct(const PS& ph);
00575
00577
00582 void add_constraint(const Constraint& c);
00583
00593 void refine_with_constraint(const Constraint& c);
00594
00596
00607 bool add_constraint_and_minimize(const Constraint& c);
00608
00610
00618 void add_constraints(const Constraint_System& cs);
00619
00629 void refine_with_constraints(const Constraint_System& cs);
00630
00648 bool add_constraints_and_minimize(const Constraint_System& cs);
00649
00651
00656 void add_congruence(const Congruence& c);
00657
00667 void refine_with_congruence(const Congruence& cg);
00668
00670
00681 bool add_congruence_and_minimize(const Congruence& c);
00682
00684
00692 void add_congruences(const Congruence_System& cgs);
00693
00703 void refine_with_congruences(const Congruence_System& cgs);
00704
00722 bool add_congruences_and_minimize(const Congruence_System& cs);
00723
00734 void unconstrain(Variable var);
00735
00748 void unconstrain(const Variables_Set& to_be_unconstrained);
00749
00751 void topological_closure_assign();
00752
00754
00758 void intersection_assign(const Pointset_Powerset& y);
00759
00761
00772 bool intersection_assign_and_minimize(const Pointset_Powerset& y);
00773
00782 void difference_assign(const Pointset_Powerset& y);
00783
00793 bool simplify_using_context_assign(const Pointset_Powerset& y);
00794
00816 void affine_image(Variable var,
00817 const Linear_Expression& expr,
00818 Coefficient_traits::const_reference denominator
00819 = Coefficient_one());
00820
00842 void affine_preimage(Variable var,
00843 const Linear_Expression& expr,
00844 Coefficient_traits::const_reference denominator
00845 = Coefficient_one());
00846
00873 void generalized_affine_image(Variable var,
00874 Relation_Symbol relsym,
00875 const Linear_Expression& expr,
00876 Coefficient_traits::const_reference denominator
00877 = Coefficient_one());
00878
00905 void
00906 generalized_affine_preimage(Variable var,
00907 Relation_Symbol relsym,
00908 const Linear_Expression& expr,
00909 Coefficient_traits::const_reference denominator
00910 = Coefficient_one());
00911
00932 void generalized_affine_image(const Linear_Expression& lhs,
00933 Relation_Symbol relsym,
00934 const Linear_Expression& rhs);
00935
00956 void generalized_affine_preimage(const Linear_Expression& lhs,
00957 Relation_Symbol relsym,
00958 const Linear_Expression& rhs);
00959
00986 void bounded_affine_image(Variable var,
00987 const Linear_Expression& lb_expr,
00988 const Linear_Expression& ub_expr,
00989 Coefficient_traits::const_reference denominator
00990 = Coefficient_one());
00991
01018 void bounded_affine_preimage(Variable var,
01019 const Linear_Expression& lb_expr,
01020 const Linear_Expression& ub_expr,
01021 Coefficient_traits::const_reference denominator
01022 = Coefficient_one());
01023
01032 void time_elapse_assign(const Pointset_Powerset& y);
01033
01042 void pairwise_reduce();
01043
01071 template <typename Widening>
01072 void BGP99_extrapolation_assign(const Pointset_Powerset& y,
01073 Widening wf,
01074 unsigned max_disjuncts);
01075
01104 template <typename Cert, typename Widening>
01105 void BHZ03_widening_assign(const Pointset_Powerset& y, Widening wf);
01106
01108
01110
01111
01116 Pointset_Powerset& operator=(const Pointset_Powerset& y);
01117
01123 template <typename QH>
01124 Pointset_Powerset& operator=(const Pointset_Powerset<QH>& y);
01125
01127 void swap(Pointset_Powerset& y);
01128
01133 void add_space_dimensions_and_embed(dimension_type m);
01134
01139 void add_space_dimensions_and_project(dimension_type m);
01140
01142
01147 void concatenate_assign(const Pointset_Powerset& y);
01148
01150
01159 void remove_space_dimensions(const Variables_Set& to_be_removed);
01160
01169 void remove_higher_space_dimensions(dimension_type new_dimension);
01170
01177 template <typename Partial_Function>
01178 void map_space_dimensions(const Partial_Function& pfunc);
01179
01181
01203 void expand_space_dimension(Variable var, dimension_type m);
01204
01206
01229 void fold_space_dimensions(const Variables_Set& to_be_folded, Variable var);
01230
01232
01233 public:
01234 typedef typename Base::size_type size_type;
01235 typedef typename Base::value_type value_type;
01236 typedef typename Base::iterator iterator;
01237 typedef typename Base::const_iterator const_iterator;
01238 typedef typename Base::reverse_iterator reverse_iterator;
01239 typedef typename Base::const_reverse_iterator const_reverse_iterator;
01240
01241 PPL_OUTPUT_DECLARATIONS
01242
01243 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
01244
01249 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
01250 bool ascii_load(std::istream& s);
01251
01252 private:
01253 typedef typename Base::Sequence Sequence;
01254 typedef typename Base::Sequence_iterator Sequence_iterator;
01255 typedef typename Base::Sequence_const_iterator Sequence_const_iterator;
01256
01258 dimension_type space_dim;
01259
01270 bool intersection_preserving_enlarge_element(PS& to_be_enlarged) const;
01271
01276 template <typename Widening>
01277 void BGP99_heuristics_assign(const Pointset_Powerset& y, Widening wf);
01278
01280 template <typename Cert>
01281 void collect_certificates(std::map<Cert, size_type,
01282 typename Cert::Compare>& cert_ms) const;
01283
01288 template <typename Cert>
01289 bool is_cert_multiset_stabilizing(const std::map<Cert, size_type,
01290 typename Cert::Compare>&
01291 y_cert_ms) const;
01292
01293
01294
01295
01296
01297 friend class Pointset_Powerset<NNC_Polyhedron>;
01298 };
01299
01300 namespace Parma_Polyhedra_Library {
01301
01303
01322 template <typename PS>
01323 std::pair<PS, Pointset_Powerset<NNC_Polyhedron> >
01324 linear_partition(const PS& p, const PS& q);
01325
01332 bool
01333 check_containment(const NNC_Polyhedron& ph,
01334 const Pointset_Powerset<NNC_Polyhedron>& ps);
01335
01336
01358 std::pair<Grid, Pointset_Powerset<Grid> >
01359 approximate_partition(const Grid& p, const Grid& q, bool& finite_partition);
01360
01367 bool
01368 check_containment(const Grid& ph,
01369 const Pointset_Powerset<Grid>& ps);
01370
01381 template <typename PS>
01382 bool
01383 check_containment(const PS& ph, const Pointset_Powerset<PS>& ps);
01384
01385
01386
01387
01388
01389 template <>
01390 template <typename QH>
01391 Pointset_Powerset<NNC_Polyhedron>
01392 ::Pointset_Powerset(const Pointset_Powerset<QH>& y,
01393 Complexity_Class);
01394
01395
01396
01397 template <>
01398 template <>
01399 Pointset_Powerset<NNC_Polyhedron>
01400 ::Pointset_Powerset(const Pointset_Powerset<C_Polyhedron>& y,
01401 Complexity_Class);
01402
01403 template <>
01404 template <>
01405 Pointset_Powerset<C_Polyhedron>
01406 ::Pointset_Powerset(const Pointset_Powerset<NNC_Polyhedron>& y,
01407 Complexity_Class);
01408
01409 template <>
01410 void
01411 Pointset_Powerset<NNC_Polyhedron>
01412 ::difference_assign(const Pointset_Powerset& y);
01413
01414 template <>
01415 void
01416 Pointset_Powerset<Grid>
01417 ::difference_assign(const Pointset_Powerset& y);
01418
01419 template <>
01420 bool
01421 Pointset_Powerset<NNC_Polyhedron>
01422 ::geometrically_covers(const Pointset_Powerset& y) const;
01423
01424 template <>
01425 bool
01426 Pointset_Powerset<Grid>
01427 ::geometrically_covers(const Pointset_Powerset& y) const;
01428
01429 }
01430
01431
01432 namespace std {
01433
01435
01436 template <typename PS>
01437 void swap(Parma_Polyhedra_Library::Pointset_Powerset<PS>& x,
01438 Parma_Polyhedra_Library::Pointset_Powerset<PS>& y);
01439
01440 }
01441
01442 #include "Pointset_Powerset.inlines.hh"
01443 #include "Pointset_Powerset.templates.hh"
01444
01445 #endif // !defined(PPL_Pointset_Powerset_defs_hh)