00001 /* Determinate 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_Determinate_defs_hh 00024 #define PPL_Determinate_defs_hh 00025 00026 #include "Determinate.types.hh" 00027 #include "Constraint_System.types.hh" 00028 #include "Congruence_System.types.hh" 00029 #include "Variable.defs.hh" 00030 #include "globals.types.hh" 00031 #include <iosfwd> 00032 #include <cassert> 00033 00034 namespace Parma_Polyhedra_Library { 00035 00042 template <typename PS> 00043 bool operator==(const Determinate<PS>& x, const Determinate<PS>& y); 00044 00051 template <typename PS> 00052 bool operator!=(const Determinate<PS>& x, const Determinate<PS>& y); 00053 00054 namespace IO_Operators { 00055 00057 00058 template <typename PS> 00059 std::ostream& 00060 operator<<(std::ostream&, const Determinate<PS>&); 00061 00062 } // namespace IO_Operators 00063 00064 } // namespace Parma_Polyhedra_Library 00065 00067 00068 template <typename PS> 00069 class Parma_Polyhedra_Library::Determinate { 00070 public: 00072 00073 00078 Determinate(const PS& p); 00079 00084 Determinate(const Constraint_System& cs); 00085 00089 Determinate(const Congruence_System& cgs); 00090 00092 Determinate(const Determinate& y); 00093 00095 ~Determinate(); 00096 00098 00100 00101 00103 const PS& element() const; 00104 00109 bool is_top() const; 00110 00115 bool is_bottom() const; 00116 00118 bool definitely_entails(const Determinate& y) const; 00119 00124 bool is_definitely_equivalent_to(const Determinate& y) const; 00125 00130 memory_size_type total_memory_in_bytes() const; 00131 00136 memory_size_type external_memory_in_bytes() const; 00137 00142 static bool has_nontrivial_weakening(); 00143 00145 bool OK() const; 00146 00148 00149 00151 00152 00154 void upper_bound_assign(const Determinate& y); 00155 00157 void meet_assign(const Determinate& y); 00158 00160 void weakening_assign(const Determinate& y); 00161 00166 void concatenate_assign(const Determinate& y); 00167 00169 PS& element(); 00170 00171 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 00172 00176 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) 00177 void mutate(); 00178 00180 Determinate& operator=(const Determinate& y); 00181 00183 void swap(Determinate& y); 00184 00186 00187 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 00189 00201 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) 00202 template <typename Binary_Operator_Assign> 00203 class Binary_Operator_Assign_Lifter { 00204 public: 00206 explicit 00207 Binary_Operator_Assign_Lifter(Binary_Operator_Assign op_assign); 00208 00210 void operator()(Determinate& x, const Determinate& y) const; 00211 00212 private: 00214 Binary_Operator_Assign op_assign_; 00215 }; 00216 00217 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 00218 00222 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) 00223 template <typename Binary_Operator_Assign> 00224 static Binary_Operator_Assign_Lifter<Binary_Operator_Assign> 00225 lift_op_assign(Binary_Operator_Assign op_assign); 00226 00227 private: 00229 00234 class Rep { 00235 private: 00242 mutable unsigned long references; 00243 00245 Rep& operator=(const Rep& y); 00246 00248 Rep(const Rep& y); 00249 00251 Rep(); 00252 00253 public: 00255 PS ph; 00256 00261 Rep(dimension_type num_dimensions, Degenerate_Element kind); 00262 00264 Rep(const PS& p); 00265 00267 Rep(const Constraint_System& cs); 00268 00270 Rep(const Congruence_System& cgs); 00271 00273 ~Rep(); 00274 00276 void new_reference() const; 00277 00282 bool del_reference() const; 00283 00285 bool is_shared() const; 00286 00291 memory_size_type total_memory_in_bytes() const; 00292 00297 memory_size_type external_memory_in_bytes() const; 00298 }; 00299 00304 Rep* prep; 00305 00306 friend bool 00307 operator==<PS>(const Determinate<PS>& x, const Determinate<PS>& y); 00308 friend bool 00309 operator!=<PS>(const Determinate<PS>& x, const Determinate<PS>& y); 00310 }; 00311 00312 00313 namespace std { 00314 00316 00317 template <typename PS> 00318 void swap(Parma_Polyhedra_Library::Determinate<PS>& x, 00319 Parma_Polyhedra_Library::Determinate<PS>& y); 00320 00321 } // namespace std 00322 00323 #include "Determinate.inlines.hh" 00324 00325 #endif // !defined(PPL_Determinate_defs_hh)