1 /* Powerset class declaration. 2 Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it> 3 Copyright (C) 2010-2016 BUGSENG srl (http://bugseng.com) 4 5 This file is part of the Parma Polyhedra Library (PPL). 6 7 The PPL is free software; you can redistribute it and/or modify it 8 under the terms of the GNU General Public License as published by the 9 Free Software Foundation; either version 3 of the License, or (at your 10 option) any later version. 11 12 The PPL is distributed in the hope that it will be useful, but WITHOUT 13 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or 14 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License 15 for more details. 16 17 You should have received a copy of the GNU General Public License 18 along with this program; if not, write to the Free Software Foundation, 19 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. 20 21 For the most up-to-date information see the Parma Polyhedra Library 22 site: http://bugseng.com/products/ppl/ . */ 23 24 #ifndef PPL_Powerset_defs_hh 25 #define PPL_Powerset_defs_hh 26 27 #include "Powerset_types.hh" 28 #include "globals_types.hh" 29 #include "iterator_to_const_defs.hh" 30 #include <iosfwd> 31 #include <iterator> 32 #include <list> 33 34 namespace Parma_Polyhedra_Library { 35 36 //! Swaps \p x with \p y. 37 /*! \relates Powerset */ 38 template <typename D> 39 void swap(Powerset<D>& x, Powerset<D>& y); 40 41 //! Returns <CODE>true</CODE> if and only if \p x and \p y are equivalent. 42 /*! \relates Powerset */ 43 template <typename D> 44 bool 45 operator==(const Powerset<D>& x, const Powerset<D>& y); 46 47 //! Returns <CODE>true</CODE> if and only if \p x and \p y are not equivalent. 48 /*! \relates Powerset */ 49 template <typename D> 50 bool 51 operator!=(const Powerset<D>& x, const Powerset<D>& y); 52 53 namespace IO_Operators { 54 55 //! Output operator. 56 /*! \relates Parma_Polyhedra_Library::Powerset */ 57 template <typename D> 58 std::ostream& 59 operator<<(std::ostream& s, const Powerset<D>& x); 60 61 } // namespace IO_Operators 62 63 } // namespace Parma_Polyhedra_Library 64 65 66 //! The powerset construction on a base-level domain. 67 /*! \ingroup PPL_CXX_interface 68 This class offers a generic implementation of a 69 <EM>powerset</EM> domain as defined in Section \ref powerset. 70 71 Besides invoking the available methods on the disjuncts of a Powerset, 72 this class also provides bidirectional iterators that allow for a 73 direct inspection of these disjuncts. For a consistent handling of 74 Omega-reduction, all the iterators are <EM>read-only</EM>, meaning 75 that the disjuncts cannot be overwritten. Rather, by using the class 76 <CODE>iterator</CODE>, it is possible to drop one or more disjuncts 77 (possibly so as to later add back modified versions). As an example 78 of iterator usage, the following template function drops from 79 powerset \p ps all the disjuncts that would have become redundant by 80 the addition of an external element \p d. 81 82 \code 83 template <typename D> 84 void 85 drop_subsumed(Powerset<D>& ps, const D& d) { 86 for (typename Powerset<D>::iterator i = ps.begin(), 87 ps_end = ps.end(), i != ps_end; ) 88 if (i->definitely_entails(d)) 89 i = ps.drop_disjunct(i); 90 else 91 ++i; 92 } 93 \endcode 94 95 The template class D must provide the following methods. 96 \code 97 memory_size_type total_memory_in_bytes() const 98 \endcode 99 Returns a lower bound on the total size in bytes of the memory 100 occupied by the instance of D. 101 \code 102 bool is_top() const 103 \endcode 104 Returns <CODE>true</CODE> if and only if the instance of D is the top 105 element of the domain. 106 \code 107 bool is_bottom() const 108 \endcode 109 Returns <CODE>true</CODE> if and only if the instance of D is the 110 bottom element of the domain. 111 \code 112 bool definitely_entails(const D& y) const 113 \endcode 114 Returns <CODE>true</CODE> if the instance of D definitely entails 115 <CODE>y</CODE>. Returns <CODE>false</CODE> if the instance may not 116 entail <CODE>y</CODE> (i.e., if the instance does not entail 117 <CODE>y</CODE> or if entailment could not be decided). 118 \code 119 void upper_bound_assign(const D& y) 120 \endcode 121 Assigns to the instance of D an upper bound of the instance and 122 <CODE>y</CODE>. 123 \code 124 void meet_assign(const D& y) 125 \endcode 126 Assigns to the instance of D the meet of the instance and 127 <CODE>y</CODE>. 128 \code 129 bool OK() const 130 \endcode 131 Returns <CODE>true</CODE> if the instance of D is in a consistent 132 state, else returns <CODE>false</CODE>. 133 134 The following operators on the template class D must be defined. 135 \code 136 operator<<(std::ostream& s, const D& x) 137 \endcode 138 Writes a textual representation of the instance of D on 139 <CODE>s</CODE>. 140 \code 141 operator==(const D& x, const D& y) 142 \endcode 143 Returns <CODE>true</CODE> if and only if <CODE>x</CODE> and 144 <CODE>y</CODE> are equivalent D's. 145 \code 146 operator!=(const D& x, const D& y) 147 \endcode 148 Returns <CODE>true</CODE> if and only if <CODE>x</CODE> and 149 <CODE>y</CODE> are different D's. 150 */ 151 template <typename D> 152 class Parma_Polyhedra_Library::Powerset { 153 public: 154 //! \name Constructors and Destructor 155 //@{ 156 157 /*! \brief 158 Default constructor: builds the bottom of the powerset constraint 159 system (i.e., the empty powerset). 160 */ 161 Powerset(); 162 163 //! Copy constructor. 164 Powerset(const Powerset& y); 165 166 /*! \brief 167 If \p d is not bottom, builds a powerset containing only \p d. 168 Builds the empty powerset otherwise. 169 */ 170 explicit Powerset(const D& d); 171 172 //! Destructor. 173 ~Powerset(); 174 175 //@} // Constructors and Destructor 176 177 //! \name Member Functions that Do Not Modify the Powerset Object 178 //@{ 179 180 /*! \brief 181 Returns <CODE>true</CODE> if \p *this definitely entails \p y. 182 Returns <CODE>false</CODE> if \p *this may not entail \p y 183 (i.e., if \p *this does not entail \p y or if entailment could 184 not be decided). 185 */ 186 bool definitely_entails(const Powerset& y) const; 187 188 /*! \brief 189 Returns <CODE>true</CODE> if and only if \p *this is the top 190 element of the powerset constraint system (i.e., it represents 191 the universe). 192 */ 193 bool is_top() const; 194 195 /*! \brief 196 Returns <CODE>true</CODE> if and only if \p *this is the bottom 197 element of the powerset constraint system (i.e., it represents 198 the empty set). 199 */ 200 bool is_bottom() const; 201 202 /*! \brief 203 Returns a lower bound to the total size in bytes of the memory 204 occupied by \p *this. 205 */ 206 memory_size_type total_memory_in_bytes() const; 207 208 /*! \brief 209 Returns a lower bound to the size in bytes of the memory 210 managed by \p *this. 211 */ 212 memory_size_type external_memory_in_bytes() const; 213 214 //! Checks if all the invariants are satisfied. 215 // FIXME: document and perhaps use an enum instead of a bool. 216 bool OK(bool disallow_bottom = false) const; 217 218 //@} // Member Functions that Do Not Modify the Powerset Object 219 220 protected: 221 //! A powerset is implemented as a sequence of elements. 222 /*! 223 The particular sequence employed must support efficient deletion 224 in any position and efficient back insertion. 225 */ 226 typedef std::list<D> Sequence; 227 228 //! Alias for the low-level iterator on the disjuncts. 229 typedef typename Sequence::iterator Sequence_iterator; 230 231 //! Alias for the low-level %const_iterator on the disjuncts. 232 typedef typename Sequence::const_iterator Sequence_const_iterator; 233 234 //! The sequence container holding powerset's elements. 235 Sequence sequence; 236 237 //! If <CODE>true</CODE>, \p *this is Omega-reduced. 238 mutable bool reduced; 239 240 public: 241 // Sequence manipulation types, accessors and modifiers 242 typedef typename Sequence::size_type size_type; 243 typedef typename Sequence::value_type value_type; 244 245 /*! \brief 246 Alias for a <EM>read-only</EM> bidirectional %iterator on the 247 disjuncts of a Powerset element. 248 249 By using this iterator type, the disjuncts cannot be overwritten, 250 but they can be removed using methods 251 <CODE>drop_disjunct(iterator position)</CODE> and 252 <CODE>drop_disjuncts(iterator first, iterator last)</CODE>, 253 while still ensuring a correct handling of Omega-reduction. 254 */ 255 typedef iterator_to_const<Sequence> iterator; 256 257 //! A bidirectional %const_iterator on the disjuncts of a Powerset element. 258 typedef const_iterator_to_const<Sequence> const_iterator; 259 260 //! The reverse iterator type built from Powerset::iterator. 261 typedef std::reverse_iterator<iterator> reverse_iterator; 262 263 //! The reverse iterator type built from Powerset::const_iterator. 264 typedef std::reverse_iterator<const_iterator> const_reverse_iterator; 265 266 //! \name Member Functions for the Direct Manipulation of Disjuncts 267 //@{ 268 269 /*! \brief 270 Drops from the sequence of disjuncts in \p *this all the 271 non-maximal elements so that \p *this is non-redundant. 272 273 This method is declared <CODE>const</CODE> because, even though 274 Omega-reduction may change the syntactic representation of \p *this, 275 its semantics will be unchanged. 276 */ 277 void omega_reduce() const; 278 279 //! Returns the number of disjuncts. 280 size_type size() const; 281 282 /*! \brief 283 Returns <CODE>true</CODE> if and only if there are no disjuncts in 284 \p *this. 285 */ 286 bool empty() const; 287 288 /*! \brief 289 Returns an iterator pointing to the first disjunct, if \p *this 290 is not empty; otherwise, returns the past-the-end iterator. 291 */ 292 iterator begin(); 293 294 //! Returns the past-the-end iterator. 295 iterator end(); 296 297 /*! \brief 298 Returns a const_iterator pointing to the first disjunct, if \p *this 299 is not empty; otherwise, returns the past-the-end const_iterator. 300 */ 301 const_iterator begin() const; 302 303 //! Returns the past-the-end const_iterator. 304 const_iterator end() const; 305 306 /*! \brief 307 Returns a reverse_iterator pointing to the last disjunct, if \p *this 308 is not empty; otherwise, returns the before-the-start reverse_iterator. 309 */ 310 reverse_iterator rbegin(); 311 312 //! Returns the before-the-start reverse_iterator. 313 reverse_iterator rend(); 314 315 /*! \brief 316 Returns a const_reverse_iterator pointing to the last disjunct, 317 if \p *this is not empty; otherwise, returns the before-the-start 318 const_reverse_iterator. 319 */ 320 const_reverse_iterator rbegin() const; 321 322 //! Returns the before-the-start const_reverse_iterator. 323 const_reverse_iterator rend() const; 324 325 //! Adds to \p *this the disjunct \p d. 326 void add_disjunct(const D& d); 327 328 /*! \brief 329 Drops the disjunct in \p *this pointed to by \p position, returning 330 an iterator to the disjunct following \p position. 331 */ 332 iterator drop_disjunct(iterator position); 333 334 //! Drops all the disjuncts from \p first to \p last (excluded). 335 void drop_disjuncts(iterator first, iterator last); 336 337 //! Drops all the disjuncts, making \p *this an empty powerset. 338 void clear(); 339 340 //@} // Member Functions for the Direct Manipulation of Disjuncts 341 342 //! \name Member Functions that May Modify the Powerset Object 343 //@{ 344 345 //! The assignment operator. 346 Powerset& operator=(const Powerset& y); 347 348 //! Swaps \p *this with \p y. 349 void m_swap(Powerset& y); 350 351 //! Assigns to \p *this the least upper bound of \p *this and \p y. 352 void least_upper_bound_assign(const Powerset& y); 353 354 //! Assigns to \p *this an upper bound of \p *this and \p y. 355 /*! 356 The result will be the least upper bound of \p *this and \p y. 357 */ 358 void upper_bound_assign(const Powerset& y); 359 360 /*! \brief 361 Assigns to \p *this the least upper bound of \p *this and \p y 362 and returns \c true. 363 364 \exception std::invalid_argument 365 Thrown if \p *this and \p y are dimension-incompatible. 366 */ 367 bool upper_bound_assign_if_exact(const Powerset& y); 368 369 //! Assigns to \p *this the meet of \p *this and \p y. 370 void meet_assign(const Powerset& y); 371 372 /*! \brief 373 If \p *this is not empty (i.e., it is not the bottom element), 374 it is reduced to a singleton obtained by computing an upper-bound 375 of all the disjuncts. 376 */ 377 void collapse(); 378 379 //@} // Member Functions that May Modify the Powerset element 380 381 protected: 382 /*! \brief 383 Returns <CODE>true</CODE> if and only if \p *this does not contain 384 non-maximal elements. 385 */ 386 bool is_omega_reduced() const; 387 388 /*! \brief Upon return, \p *this will contain at most \p 389 max_disjuncts elements; the set of disjuncts in positions greater 390 than or equal to \p max_disjuncts, will be replaced at that 391 position by their upper-bound. 392 */ 393 void collapse(unsigned max_disjuncts); 394 395 /*! \brief 396 Adds to \p *this the disjunct \p d, 397 assuming \p d is not the bottom element and ensuring 398 partial Omega-reduction. 399 400 If \p d is not the bottom element and is not Omega-redundant with 401 respect to elements in positions between \p first and \p last, all 402 elements in these positions that would be made Omega-redundant by the 403 addition of \p d are dropped and \p d is added to the reduced 404 sequence. 405 If \p *this is reduced before an invocation of this method, 406 it will be reduced upon successful return from the method. 407 */ 408 iterator add_non_bottom_disjunct_preserve_reduction(const D& d, 409 iterator first, 410 iterator last); 411 412 /*! \brief 413 Adds to \p *this the disjunct \p d, assuming \p d is not the 414 bottom element and preserving Omega-reduction. 415 416 If \p *this is reduced before an invocation of this method, 417 it will be reduced upon successful return from the method. 418 */ 419 void add_non_bottom_disjunct_preserve_reduction(const D& d); 420 421 /*! \brief 422 Assigns to \p *this the result of applying \p op_assign pairwise 423 to the elements in \p *this and \p y. 424 425 The elements of the powerset result are obtained by applying 426 \p op_assign to each pair of elements whose components are drawn 427 from \p *this and \p y, respectively. 428 */ 429 template <typename Binary_Operator_Assign> 430 void pairwise_apply_assign(const Powerset& y, 431 Binary_Operator_Assign op_assign); 432 433 private: 434 /*! \brief 435 Does the hard work of checking whether \p *this contains non-maximal 436 elements and returns <CODE>true</CODE> if and only if it does not. 437 */ 438 bool check_omega_reduced() const; 439 440 /*! \brief 441 Replaces the disjunct \p *sink by an upper bound of itself and 442 all the disjuncts following it. 443 */ 444 void collapse(Sequence_iterator sink); 445 }; 446 447 #include "Powerset_inlines.hh" 448 #include "Powerset_templates.hh" 449 450 #endif // !defined(PPL_Powerset_defs_hh) 451