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_Powerset_defs_hh
00024 #define PPL_Powerset_defs_hh
00025
00026 #include "Powerset.types.hh"
00027 #include <iosfwd>
00028 #include <iterator>
00029 #include <list>
00030
00031 namespace Parma_Polyhedra_Library {
00032
00034
00035 template <typename D>
00036 bool
00037 operator==(const Powerset<D>& x, const Powerset<D>& y);
00038
00040
00041 template <typename D>
00042 bool
00043 operator!=(const Powerset<D>& x, const Powerset<D>& y);
00044
00045 namespace IO_Operators {
00046
00048
00049 template <typename D>
00050 std::ostream&
00051 operator<<(std::ostream& s, const Powerset<D>& x);
00052
00053 }
00054
00055 }
00056
00057
00059
00143 template <typename D>
00144 class Parma_Polyhedra_Library::Powerset {
00145 public:
00147
00148
00153 Powerset();
00154
00156 Powerset(const Powerset& y);
00157
00162 explicit Powerset(const D& d);
00163
00165 ~Powerset();
00166
00168
00170
00171
00178 bool definitely_entails(const Powerset& y) const;
00179
00185 bool is_top() const;
00186
00192 bool is_bottom() const;
00193
00198 memory_size_type total_memory_in_bytes() const;
00199
00204 memory_size_type external_memory_in_bytes() const;
00205
00207
00208 bool OK(bool disallow_bottom = false) const;
00209
00211
00212 protected:
00214
00218 typedef std::list<D> Sequence;
00219
00221 typedef typename Sequence::iterator Sequence_iterator;
00222
00224 typedef typename Sequence::const_iterator Sequence_const_iterator;
00225
00227 Sequence sequence;
00228
00230 mutable bool reduced;
00231
00232 public:
00233
00234 typedef typename Sequence::size_type size_type;
00235 typedef typename Sequence::value_type value_type;
00236
00237 class omega_iterator;
00238 class omega_const_iterator;
00239
00250 typedef omega_iterator iterator;
00252 typedef omega_const_iterator const_iterator;
00253
00255 typedef std::reverse_iterator<iterator> reverse_iterator;
00257 typedef std::reverse_iterator<const_iterator> const_reverse_iterator;
00258
00260
00261
00270 void omega_reduce() const;
00271
00273 size_type size() const;
00274
00276 bool empty() const;
00277
00282 iterator begin();
00283
00285 iterator end();
00286
00291 const_iterator begin() const;
00292
00294 const_iterator end() const;
00295
00300 reverse_iterator rbegin();
00302 reverse_iterator rend();
00308 const_reverse_iterator rbegin() const;
00310 const_reverse_iterator rend() const;
00311
00313 void add_disjunct(const D& d);
00314
00319 iterator drop_disjunct(iterator position);
00320
00322 void drop_disjuncts(iterator first, iterator last);
00323
00325 void clear();
00326
00328
00330
00331
00333 Powerset& operator=(const Powerset& y);
00334
00336 void swap(Powerset& y);
00337
00339 void least_upper_bound_assign(const Powerset& y);
00340
00342
00345 void upper_bound_assign(const Powerset& y);
00346
00348 void meet_assign(const Powerset& y);
00349
00355 void collapse();
00356
00358
00359 protected:
00364 bool is_omega_reduced() const;
00365
00371 void collapse(unsigned max_disjuncts);
00372
00384 iterator add_non_bottom_disjunct(const D& d,
00385 iterator first,
00386 iterator last);
00387
00392 void add_non_bottom_disjunct(const D& d);
00393
00402 template <typename Binary_Operator_Assign>
00403 void pairwise_apply_assign(const Powerset& y,
00404 Binary_Operator_Assign op_assign);
00405
00406 private:
00411 bool check_omega_reduced() const;
00412
00417 void collapse(Sequence_iterator sink);
00418 };
00419
00420 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00422
00426 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00427 template <typename D>
00428 class Parma_Polyhedra_Library::Powerset<D>::omega_const_iterator {
00429 protected:
00431 typedef typename Powerset::Sequence::const_iterator Base;
00432
00434 typedef typename std::iterator_traits<Base> Traits;
00435
00437 Base base;
00438
00440 omega_const_iterator(const Base& b);
00441
00442 friend class Powerset;
00443
00444 public:
00445
00446 typedef typename Traits::iterator_category iterator_category;
00447 typedef typename Traits::value_type value_type;
00448 typedef typename Traits::difference_type difference_type;
00449 typedef typename Traits::pointer pointer;
00450 typedef typename Traits::reference reference;
00451
00453 omega_const_iterator();
00454
00456 omega_const_iterator(const omega_const_iterator& y);
00457
00459 omega_const_iterator(const omega_iterator& y);
00460
00462 reference operator*() const;
00463
00465 pointer operator->() const;
00466
00468 omega_const_iterator& operator++();
00469
00471 omega_const_iterator operator++(int);
00472
00474 omega_const_iterator& operator--();
00475
00477 omega_const_iterator operator--(int);
00478
00483 bool operator==(const omega_const_iterator& y) const;
00484
00489 bool operator!=(const omega_const_iterator& y) const;
00490 };
00491
00492 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00494
00510 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00511 template <typename D>
00512 class Parma_Polyhedra_Library::Powerset<D>::omega_iterator {
00513 protected:
00515 typedef typename Powerset::Sequence::iterator Base;
00516
00518 typedef typename
00519 std::iterator_traits<typename Powerset::Sequence::const_iterator> Traits;
00520
00522 Base base;
00523
00525 omega_iterator(const Base& b);
00526
00527 friend class Powerset;
00528 friend Powerset<D>::omega_const_iterator
00529 ::omega_const_iterator(const omega_iterator& y);
00530
00531 public:
00532
00533
00534 typedef typename Traits::iterator_category iterator_category;
00535 typedef typename Traits::value_type value_type;
00536 typedef typename Traits::difference_type difference_type;
00537 typedef typename Traits::pointer pointer;
00538 typedef typename Traits::reference reference;
00539
00541 omega_iterator();
00542
00544 omega_iterator(const omega_iterator& y);
00545
00547 reference operator*() const;
00548
00550 pointer operator->() const;
00551
00553 omega_iterator& operator++();
00554
00556 omega_iterator operator++(int);
00557
00559 omega_iterator& operator--();
00560
00562 omega_iterator operator--(int);
00563
00568 bool operator==(const omega_iterator& y) const;
00569
00574 bool operator!=(const omega_iterator& y) const;
00575 };
00576
00577 namespace Parma_Polyhedra_Library {
00578
00579 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00580
00586 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00587 template <typename D>
00588 bool
00589 operator==(const typename Powerset<D>::omega_iterator& x,
00590 const typename Powerset<D>::omega_const_iterator& y);
00591
00592 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00593
00599 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00600 template <typename D>
00601 bool
00602 operator!=(const typename Powerset<D>::omega_iterator& x,
00603 const typename Powerset<D>::omega_const_iterator& y);
00604
00605 }
00606
00607 namespace std {
00608
00610
00611 template <typename D>
00612 void swap(Parma_Polyhedra_Library::Powerset<D>& x,
00613 Parma_Polyhedra_Library::Powerset<D>& y);
00614
00615 }
00616
00617 #include "Powerset.inlines.hh"
00618 #include "Powerset.templates.hh"
00619
00620 #endif // !defined(PPL_Powerset_defs_hh)