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_Polyhedra_Powerset_defs_hh
00024 #define PPL_Polyhedra_Powerset_defs_hh
00025
00026 #include "Polyhedra_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.types.hh"
00034 #include "NNC_Polyhedron.types.hh"
00035 #include "Polyhedron.defs.hh"
00036 #include "Variable.defs.hh"
00037 #include "Determinate.defs.hh"
00038 #include "Powerset.defs.hh"
00039 #include <iosfwd>
00040 #include <list>
00041 #include <map>
00042
00044
00045 template <typename PH>
00046 class Parma_Polyhedra_Library::Polyhedra_Powerset
00047 : public Parma_Polyhedra_Library::Powerset
00048 <Parma_Polyhedra_Library::Determinate<PH> > {
00049 public:
00050 typedef PH element_type;
00051
00052 private:
00053 typedef Determinate<PH> CS;
00054 typedef Powerset<CS> Base;
00055
00056 public:
00058 static dimension_type max_space_dimension();
00059
00061
00062
00064
00071 explicit
00072 Polyhedra_Powerset(dimension_type num_dimensions = 0,
00073 Degenerate_Element kind = UNIVERSE);
00074
00076 Polyhedra_Powerset(const Polyhedra_Powerset& y);
00077
00082 explicit Polyhedra_Powerset(const PH& ph);
00083
00088 template <typename QH>
00089 explicit Polyhedra_Powerset(const Polyhedra_Powerset<QH>& y);
00090
00095 explicit Polyhedra_Powerset(const Constraint_System& cs);
00096
00099 explicit Polyhedra_Powerset(const Congruence_System& cgs);
00100
00102
00104
00105
00107 dimension_type space_dimension() const;
00108
00121 bool geometrically_covers(const Polyhedra_Powerset& y) const;
00122
00135 bool geometrically_equals(const Polyhedra_Powerset& y) const;
00136
00141 memory_size_type total_memory_in_bytes() const;
00142
00147 memory_size_type external_memory_in_bytes() const;
00148
00150 bool OK() const;
00151
00153
00155
00156
00158
00162 void add_disjunct(const PH& ph);
00163
00165
00170 void add_constraint(const Constraint& c);
00171
00173
00181 bool add_constraint_and_minimize(const Constraint& c);
00182
00184
00192 void add_constraints(const Constraint_System& cs);
00193
00208 bool add_constraints_and_minimize(const Constraint_System& cs);
00209
00218 void pairwise_reduce();
00219
00249 template <typename Widening>
00250 void BGP99_extrapolation_assign(const Polyhedra_Powerset& y,
00251 Widening wf,
00252 unsigned max_disjuncts);
00253
00283 template <typename Cert, typename Widening>
00284 void BHZ03_widening_assign(const Polyhedra_Powerset& y, Widening wf);
00285
00287
00289
00290
00295 Polyhedra_Powerset& operator=(const Polyhedra_Powerset& y);
00296
00302 template <typename QH>
00303 Polyhedra_Powerset& operator=(const Polyhedra_Powerset<QH>& y);
00304
00306 void swap(Polyhedra_Powerset& y);
00307
00312 void add_space_dimensions_and_embed(dimension_type m);
00313
00318 void add_space_dimensions_and_project(dimension_type m);
00319
00321
00325 void intersection_assign(const Polyhedra_Powerset& y);
00326
00328
00334 void poly_difference_assign(const Polyhedra_Powerset& y);
00335
00337
00342 void concatenate_assign(const Polyhedra_Powerset& y);
00343
00352 void time_elapse_assign(const Polyhedra_Powerset& y);
00353
00355
00364 void remove_space_dimensions(const Variables_Set& to_be_removed);
00365
00374 void remove_higher_space_dimensions(dimension_type new_dimension);
00375
00382 template <typename Partial_Function>
00383 void map_space_dimensions(const Partial_Function& pfunc);
00384
00386
00387 public:
00388 typedef typename Base::size_type size_type;
00389 typedef typename Base::value_type value_type;
00390 typedef typename Base::iterator iterator;
00391 typedef typename Base::const_iterator const_iterator;
00392 typedef typename Base::reverse_iterator reverse_iterator;
00393 typedef typename Base::const_reverse_iterator const_reverse_iterator;
00394
00395 PPL_OUTPUT_DECLARATIONS;
00396
00397 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00398
00403 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00404 bool ascii_load(std::istream& s);
00405
00406 private:
00407 typedef typename Base::Sequence Sequence;
00408 typedef typename Base::Sequence_iterator Sequence_iterator;
00409 typedef typename Base::Sequence_const_iterator Sequence_const_iterator;
00410
00412 dimension_type space_dim;
00413
00418 template <typename Widening>
00419 void BGP99_heuristics_assign(const Polyhedra_Powerset& y, Widening wf);
00420
00422 template <typename Cert>
00423 void collect_certificates(std::map<Cert, size_type,
00424 typename Cert::Compare>& cert_ms) const;
00425
00430 template <typename Cert>
00431 bool is_cert_multiset_stabilizing(const std::map<Cert, size_type,
00432 typename Cert::Compare>&
00433 y_cert_ms) const;
00434
00435
00436
00437
00438
00439
00440
00441
00442
00443 template <typename QH> friend class Polyhedra_Powerset;
00444 };
00445
00446
00447 namespace Parma_Polyhedra_Library {
00448
00450
00469 template <typename PH>
00470 std::pair<PH, Polyhedra_Powerset<NNC_Polyhedron> >
00471 linear_partition(const PH& p, const PH& q);
00472
00479 bool
00480 check_containment(const NNC_Polyhedron& ph,
00481 const Polyhedra_Powerset<NNC_Polyhedron>& ps);
00482
00493 template <typename PH>
00494 bool
00495 check_containment(const PH& ph, const Polyhedra_Powerset<PH>& ps);
00496
00497
00498
00499
00500
00501 template <>
00502 template <typename QH>
00503 Polyhedra_Powerset<NNC_Polyhedron>
00504 ::Polyhedra_Powerset(const Polyhedra_Powerset<QH>& y);
00505
00506
00507
00508
00509
00510 template <>
00511 template <typename QH>
00512 Polyhedra_Powerset<C_Polyhedron>
00513 ::Polyhedra_Powerset(const Polyhedra_Powerset<QH>& y);
00514
00515
00516
00517 template <>
00518 template <>
00519 Polyhedra_Powerset<NNC_Polyhedron>
00520 ::Polyhedra_Powerset(const Polyhedra_Powerset<C_Polyhedron>& y);
00521
00522 template <>
00523 template <>
00524 Polyhedra_Powerset<C_Polyhedron>
00525 ::Polyhedra_Powerset(const Polyhedra_Powerset<NNC_Polyhedron>& y);
00526
00527 template <>
00528 void
00529 Polyhedra_Powerset<NNC_Polyhedron>
00530 ::poly_difference_assign(const Polyhedra_Powerset& y);
00531
00532 template <>
00533 bool
00534 Polyhedra_Powerset<NNC_Polyhedron>
00535 ::geometrically_covers(const Polyhedra_Powerset& y) const;
00536
00537 }
00538
00539
00540 namespace std {
00541
00543
00544 template <typename PH>
00545 void swap(Parma_Polyhedra_Library::Polyhedra_Powerset<PH>& x,
00546 Parma_Polyhedra_Library::Polyhedra_Powerset<PH>& y);
00547
00548 }
00549
00550 #include "Polyhedra_Powerset.inlines.hh"
00551 #include "Polyhedra_Powerset.templates.hh"
00552
00553 #endif // !defined(PPL_Polyhedra_Powerset_defs_hh)