1 /* Determinate 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_Determinate_defs_hh 25 #define PPL_Determinate_defs_hh 26 27 #include "Determinate_types.hh" 28 #include "Constraint_System_types.hh" 29 #include "Congruence_System_types.hh" 30 #include "Variable_defs.hh" 31 #include "globals_types.hh" 32 #include <iosfwd> 33 34 namespace Parma_Polyhedra_Library { 35 36 //! Swaps \p x with \p y. 37 /*! \relates Determinate */ 38 template <typename PSET> 39 void swap(Determinate<PSET>& x, Determinate<PSET>& y); 40 41 /*! \brief 42 Returns <CODE>true</CODE> if and only if \p x and \p y are the same 43 COW-wrapped pointset. 44 45 \relates Determinate 46 */ 47 template <typename PSET> 48 bool operator==(const Determinate<PSET>& x, const Determinate<PSET>& y); 49 50 /*! \brief 51 Returns <CODE>true</CODE> if and only if \p x and \p y are different 52 COW-wrapped pointsets. 53 54 \relates Determinate 55 */ 56 template <typename PSET> 57 bool operator!=(const Determinate<PSET>& x, const Determinate<PSET>& y); 58 59 namespace IO_Operators { 60 61 //! Output operator. 62 /*! \relates Parma_Polyhedra_Library::Determinate */ 63 template <typename PSET> 64 std::ostream& 65 operator<<(std::ostream&, const Determinate<PSET>&); 66 67 } // namespace IO_Operators 68 69 } // namespace Parma_Polyhedra_Library 70 71 /*! \brief 72 A wrapper for PPL pointsets, providing them with a 73 <EM>determinate constraint system</EM> interface, as defined 74 in \ref Bag98 "[Bag98]". 75 76 The implementation uses a copy-on-write optimization, making the 77 class suitable for constructions, like the <EM>finite powerset</EM> 78 and <EM>ask-and-tell</EM> of \ref Bag98 "[Bag98]", that are likely 79 to perform many copies. 80 81 \ingroup PPL_CXX_interface 82 */ 83 template <typename PSET> 84 class Parma_Polyhedra_Library::Determinate { 85 public: 86 //! \name Constructors and Destructor 87 //@{ 88 89 /*! \brief 90 Constructs a COW-wrapped object corresponding to the pointset \p pset. 91 */ 92 Determinate(const PSET& pset); 93 94 /*! \brief 95 Constructs a COW-wrapped object corresponding to the pointset 96 defined by \p cs. 97 */ 98 Determinate(const Constraint_System& cs); 99 100 /*! \brief 101 Constructs a COW-wrapped object corresponding to the pointset 102 defined by \p cgs. 103 */ 104 Determinate(const Congruence_System& cgs); 105 106 //! Copy constructor. 107 Determinate(const Determinate& y); 108 109 //! Destructor. 110 ~Determinate(); 111 112 //@} // Constructors and Destructor 113 114 //! \name Member Functions that Do Not Modify the Domain Element 115 //@{ 116 117 //! Returns a const reference to the embedded pointset. 118 const PSET& pointset() const; 119 120 /*! \brief 121 Returns <CODE>true</CODE> if and only if \p *this embeds the universe 122 element \p PSET. 123 */ 124 bool is_top() const; 125 126 /*! \brief 127 Returns <CODE>true</CODE> if and only if \p *this embeds the empty 128 element of \p PSET. 129 */ 130 bool is_bottom() const; 131 132 //! Returns <CODE>true</CODE> if and only if \p *this entails \p y. 133 bool definitely_entails(const Determinate& y) const; 134 135 /*! \brief 136 Returns <CODE>true</CODE> if and only if \p *this and \p y 137 are definitely equivalent. 138 */ 139 bool is_definitely_equivalent_to(const Determinate& y) const; 140 141 /*! \brief 142 Returns a lower bound to the total size in bytes of the memory 143 occupied by \p *this. 144 */ 145 memory_size_type total_memory_in_bytes() const; 146 147 /*! \brief 148 Returns a lower bound to the size in bytes of the memory 149 managed by \p *this. 150 */ 151 memory_size_type external_memory_in_bytes() const; 152 153 /*! 154 Returns <CODE>true</CODE> if and only if this domain 155 has a nontrivial weakening operator. 156 */ 157 static bool has_nontrivial_weakening(); 158 159 //! Checks if all the invariants are satisfied. 160 bool OK() const; 161 162 //@} // Member Functions that Do Not Modify the Domain Element 163 164 165 //! \name Member Functions that May Modify the Domain Element 166 //@{ 167 168 //! Assigns to \p *this the upper bound of \p *this and \p y. 169 void upper_bound_assign(const Determinate& y); 170 171 //! Assigns to \p *this the meet of \p *this and \p y. 172 void meet_assign(const Determinate& y); 173 174 //! Assigns to \p *this the result of weakening \p *this with \p y. 175 void weakening_assign(const Determinate& y); 176 177 /*! \brief 178 Assigns to \p *this the \ref Concatenating_Polyhedra "concatenation" 179 of \p *this and \p y, taken in this order. 180 */ 181 void concatenate_assign(const Determinate& y); 182 183 //! Returns a reference to the embedded element. 184 PSET& pointset(); 185 186 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 187 /*! \brief 188 On return from this method, the representation of \p *this 189 is not shared by different Determinate objects. 190 */ 191 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) 192 void mutate(); 193 194 //! Assignment operator. 195 Determinate& operator=(const Determinate& y); 196 197 //! Swaps \p *this with \p y. 198 void m_swap(Determinate& y); 199 200 //@} // Member Functions that May Modify the Domain Element 201 202 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 203 //! A function adapter for the Determinate class. 204 /*! \ingroup PPL_CXX_interface 205 It lifts a Binary_Operator_Assign function object, taking arguments 206 of type PSET, producing the corresponding function object taking 207 arguments of type Determinate<PSET>. 208 209 The template parameter Binary_Operator_Assign is supposed to 210 implement an <EM>apply and assign</EM> function, i.e., a function 211 having signature <CODE>void foo(PSET& x, const PSET& y)</CODE> that 212 applies an operator to \c x and \c y and assigns the result to \c x. 213 For instance, such a function object is obtained by 214 <CODE>std::mem_fun_ref(&C_Polyhedron::intersection_assign)</CODE>. 215 */ 216 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) 217 template <typename Binary_Operator_Assign> 218 class Binary_Operator_Assign_Lifter { 219 public: 220 //! Explicit unary constructor. 221 explicit 222 Binary_Operator_Assign_Lifter(Binary_Operator_Assign op_assign); 223 224 //! Function-application operator. 225 void operator()(Determinate& x, const Determinate& y) const; 226 227 private: 228 //! The function object to be lifted. 229 Binary_Operator_Assign op_assign_; 230 }; 231 232 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 233 /*! \brief 234 Helper function returning a Binary_Operator_Assign_Lifter object, 235 also allowing for the deduction of template arguments. 236 */ 237 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) 238 template <typename Binary_Operator_Assign> 239 static Binary_Operator_Assign_Lifter<Binary_Operator_Assign> 240 lift_op_assign(Binary_Operator_Assign op_assign); 241 242 private: 243 //! The possibly shared representation of a Determinate object. 244 /*! \ingroup PPL_CXX_interface 245 By adopting the <EM>copy-on-write</EM> technique, a single 246 representation of the base-level object may be shared by more than 247 one object of the class Determinate. 248 */ 249 class Rep { 250 private: 251 /*! \brief 252 Count the number of references: 253 - 0: leaked, \p pset is non-const; 254 - 1: one reference, \p pset is non-const; 255 - > 1: more than one reference, \p pset is const. 256 */ 257 mutable unsigned long references; 258 259 //! Private and unimplemented: assignment not allowed. 260 Rep& operator=(const Rep& y); 261 262 //! Private and unimplemented: copies not allowed. 263 Rep(const Rep& y); 264 265 //! Private and unimplemented: default construction not allowed. 266 Rep(); 267 268 public: 269 //! The possibly shared, embedded pointset. 270 PSET pset; 271 272 /*! \brief 273 Builds a new representation by creating a pointset 274 of the specified kind, in the specified vector space. 275 */ 276 Rep(dimension_type num_dimensions, Degenerate_Element kind); 277 278 //! Builds a new representation by copying the pointset \p p. 279 Rep(const PSET& p); 280 281 //! Builds a new representation by copying the constraints in \p cs. 282 Rep(const Constraint_System& cs); 283 284 //! Builds a new representation by copying the constraints in \p cgs. 285 Rep(const Congruence_System& cgs); 286 287 //! Destructor. 288 ~Rep(); 289 290 //! Registers a new reference. 291 void new_reference() const; 292 293 /*! \brief 294 Unregisters one reference; returns <CODE>true</CODE> if and only if 295 the representation has become unreferenced. 296 */ 297 bool del_reference() const; 298 299 //! True if and only if this representation is currently shared. 300 bool is_shared() const; 301 302 /*! \brief 303 Returns a lower bound to the total size in bytes of the memory 304 occupied by \p *this. 305 */ 306 memory_size_type total_memory_in_bytes() const; 307 308 /*! \brief 309 Returns a lower bound to the size in bytes of the memory 310 managed by \p *this. 311 */ 312 memory_size_type external_memory_in_bytes() const; 313 }; 314 315 /*! \brief 316 A pointer to the possibly shared representation of 317 the base-level domain element. 318 */ 319 Rep* prep; 320 321 friend bool 322 operator==<PSET>(const Determinate<PSET>& x, const Determinate<PSET>& y); 323 324 friend bool 325 operator!=<PSET>(const Determinate<PSET>& x, const Determinate<PSET>& y); 326 }; 327 328 #include "Determinate_inlines.hh" 329 330 #endif // !defined(PPL_Determinate_defs_hh) 331