00001 /* Powerset class declaration. 00002 Copyright (C) 2001-2008 Roberto Bagnara <bagnara@cs.unipr.it> 00003 00004 This file is part of the Parma Polyhedra Library (PPL). 00005 00006 The PPL is free software; you can redistribute it and/or modify it 00007 under the terms of the GNU General Public License as published by the 00008 Free Software Foundation; either version 3 of the License, or (at your 00009 option) any later version. 00010 00011 The PPL is distributed in the hope that it will be useful, but WITHOUT 00012 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or 00013 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License 00014 for more details. 00015 00016 You should have received a copy of the GNU General Public License 00017 along with this program; if not, write to the Free Software Foundation, 00018 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. 00019 00020 For the most up-to-date information see the Parma Polyhedra Library 00021 site: http://www.cs.unipr.it/ppl/ . */ 00022 00023 #ifndef PPL_Powerset_defs_hh 00024 #define PPL_Powerset_defs_hh 00025 00026 #include "Powerset.types.hh" 00027 #include "iterator_to_const.defs.hh" 00028 #include <iosfwd> 00029 #include <iterator> 00030 #include <list> 00031 00032 namespace Parma_Polyhedra_Library { 00033 00035 00036 template <typename D> 00037 bool 00038 operator==(const Powerset<D>& x, const Powerset<D>& y); 00039 00041 00042 template <typename D> 00043 bool 00044 operator!=(const Powerset<D>& x, const Powerset<D>& y); 00045 00046 namespace IO_Operators { 00047 00049 00050 template <typename D> 00051 std::ostream& 00052 operator<<(std::ostream& s, const Powerset<D>& x); 00053 00054 } // namespace IO_Operators 00055 00056 } // namespace Parma_Polyhedra_Library 00057 00058 00060 00144 template <typename D> 00145 class Parma_Polyhedra_Library::Powerset { 00146 public: 00148 00149 00154 Powerset(); 00155 00157 Powerset(const Powerset& y); 00158 00163 explicit Powerset(const D& d); 00164 00166 ~Powerset(); 00167 00169 00171 00172 00179 bool definitely_entails(const Powerset& y) const; 00180 00186 bool is_top() const; 00187 00193 bool is_bottom() const; 00194 00199 memory_size_type total_memory_in_bytes() const; 00200 00205 memory_size_type external_memory_in_bytes() const; 00206 00208 // FIXME: document and perhaps use an enum instead of a bool. 00209 bool OK(bool disallow_bottom = false) const; 00210 00212 00213 protected: 00215 00219 typedef std::list<D> Sequence; 00220 00222 typedef typename Sequence::iterator Sequence_iterator; 00223 00225 typedef typename Sequence::const_iterator Sequence_const_iterator; 00226 00228 Sequence sequence; 00229 00231 mutable bool reduced; 00232 00233 public: 00234 // Sequence manipulation types, accessors and modifiers 00235 typedef typename Sequence::size_type size_type; 00236 typedef typename Sequence::value_type value_type; 00237 00248 typedef iterator_to_const<Sequence> iterator; 00249 00251 typedef const_iterator_to_const<Sequence> const_iterator; 00252 00254 typedef std::reverse_iterator<iterator> reverse_iterator; 00255 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 00279 bool empty() const; 00280 00285 iterator begin(); 00286 00288 iterator end(); 00289 00294 const_iterator begin() const; 00295 00297 const_iterator end() const; 00298 00303 reverse_iterator rbegin(); 00304 00306 reverse_iterator rend(); 00307 00313 const_reverse_iterator rbegin() const; 00314 00316 const_reverse_iterator rend() const; 00317 00319 void add_disjunct(const D& d); 00320 00325 iterator drop_disjunct(iterator position); 00326 00328 void drop_disjuncts(iterator first, iterator last); 00329 00331 void clear(); 00332 00334 00336 00337 00339 Powerset& operator=(const Powerset& y); 00340 00342 void swap(Powerset& y); 00343 00345 void least_upper_bound_assign(const Powerset& y); 00346 00348 00351 void upper_bound_assign(const Powerset& y); 00352 00360 bool upper_bound_assign_if_exact(const Powerset& y); 00361 00363 void meet_assign(const Powerset& y); 00364 00370 void collapse(); 00371 00373 00374 protected: 00379 bool is_omega_reduced() const; 00380 00386 void collapse(unsigned max_disjuncts); 00387 00401 iterator add_non_bottom_disjunct_preserve_reduction(const D& d, 00402 iterator first, 00403 iterator last); 00404 00412 void add_non_bottom_disjunct_preserve_reduction(const D& d); 00413 00422 template <typename Binary_Operator_Assign> 00423 void pairwise_apply_assign(const Powerset& y, 00424 Binary_Operator_Assign op_assign); 00425 00426 private: 00431 bool check_omega_reduced() const; 00432 00437 void collapse(Sequence_iterator sink); 00438 }; 00439 00440 namespace std { 00441 00443 00444 template <typename D> 00445 void swap(Parma_Polyhedra_Library::Powerset<D>& x, 00446 Parma_Polyhedra_Library::Powerset<D>& y); 00447 00448 } // namespace std 00449 00450 #include "Powerset.inlines.hh" 00451 #include "Powerset.templates.hh" 00452 00453 #endif // !defined(PPL_Powerset_defs_hh)