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_Determinate_inlines_hh
00024 #define PPL_Determinate_inlines_hh 1
00025
00026 #include <cassert>
00027
00028 namespace Parma_Polyhedra_Library {
00029
00030 template <typename PS>
00031 inline
00032 Determinate<PS>::Rep::Rep(dimension_type num_dimensions,
00033 Degenerate_Element kind)
00034 : references(0), ph(num_dimensions, kind) {
00035 }
00036
00037 template <typename PS>
00038 inline
00039 Determinate<PS>::Rep::Rep(const PS& p)
00040 : references(0), ph(p) {
00041 }
00042
00043 template <typename PS>
00044 inline
00045 Determinate<PS>::Rep::Rep(const Constraint_System& cs)
00046 : references(0), ph(cs) {
00047 }
00048
00049 template <typename PS>
00050 inline
00051 Determinate<PS>::Rep::Rep(const Congruence_System& cgs)
00052 : references(0), ph(cgs) {
00053 }
00054
00055 template <typename PS>
00056 inline
00057 Determinate<PS>::Rep::~Rep() {
00058 assert(references == 0);
00059 }
00060
00061 template <typename PS>
00062 inline void
00063 Determinate<PS>::Rep::new_reference() const {
00064 ++references;
00065 }
00066
00067 template <typename PS>
00068 inline bool
00069 Determinate<PS>::Rep::del_reference() const {
00070 return --references == 0;
00071 }
00072
00073 template <typename PS>
00074 inline bool
00075 Determinate<PS>::Rep::is_shared() const {
00076 return references > 1;
00077 }
00078
00079 template <typename PS>
00080 inline memory_size_type
00081 Determinate<PS>::Rep::external_memory_in_bytes() const {
00082 return ph.external_memory_in_bytes();
00083 }
00084
00085 template <typename PS>
00086 inline memory_size_type
00087 Determinate<PS>::Rep::total_memory_in_bytes() const {
00088 return sizeof(*this) + external_memory_in_bytes();
00089 }
00090
00091 template <typename PS>
00092 inline
00093 Determinate<PS>::Determinate(const PS& ph)
00094 : prep(new Rep(ph)) {
00095 prep->new_reference();
00096 }
00097
00098 template <typename PS>
00099 inline
00100 Determinate<PS>::Determinate(const Constraint_System& cs)
00101 : prep(new Rep(cs)) {
00102 prep->new_reference();
00103 }
00104
00105 template <typename PS>
00106 inline
00107 Determinate<PS>::Determinate(const Congruence_System& cgs)
00108 : prep(new Rep(cgs)) {
00109 prep->new_reference();
00110 }
00111
00112 template <typename PS>
00113 inline
00114 Determinate<PS>::Determinate(const Determinate& y)
00115 : prep(y.prep) {
00116 prep->new_reference();
00117 }
00118
00119 template <typename PS>
00120 inline
00121 Determinate<PS>::~Determinate() {
00122 if (prep->del_reference())
00123 delete prep;
00124 }
00125
00126 template <typename PS>
00127 inline Determinate<PS>&
00128 Determinate<PS>::operator=(const Determinate& y) {
00129 y.prep->new_reference();
00130 if (prep->del_reference())
00131 delete prep;
00132 prep = y.prep;
00133 return *this;
00134 }
00135
00136 template <typename PS>
00137 inline void
00138 Determinate<PS>::swap(Determinate& y) {
00139 std::swap(prep, y.prep);
00140 }
00141
00142 template <typename PS>
00143 inline void
00144 Determinate<PS>::mutate() {
00145 if (prep->is_shared()) {
00146 Rep* new_prep = new Rep(prep->ph);
00147 (void) prep->del_reference();
00148 new_prep->new_reference();
00149 prep = new_prep;
00150 }
00151 }
00152
00153 template <typename PS>
00154 inline const PS&
00155 Determinate<PS>::element() const {
00156 return prep->ph;
00157 }
00158
00159 template <typename PS>
00160 inline PS&
00161 Determinate<PS>::element() {
00162 mutate();
00163 return prep->ph;
00164 }
00165
00166 template <typename PS>
00167 inline void
00168 Determinate<PS>::upper_bound_assign(const Determinate& y) {
00169 element().upper_bound_assign(y.element());
00170 }
00171
00172 template <typename PS>
00173 inline void
00174 Determinate<PS>::meet_assign(const Determinate& y) {
00175 element().intersection_assign(y.element());
00176 }
00177
00178 template <typename PS>
00179 inline bool
00180 Determinate<PS>::has_nontrivial_weakening() {
00181
00182 return true;
00183 }
00184
00185 template <typename PS>
00186 inline void
00187 Determinate<PS>::weakening_assign(const Determinate& y) {
00188
00189 element().difference_assign(y.element());
00190 }
00191
00192 template <typename PS>
00193 inline void
00194 Determinate<PS>::concatenate_assign(const Determinate& y) {
00195 element().concatenate_assign(y.element());
00196 }
00197
00198 template <typename PS>
00199 inline bool
00200 Determinate<PS>::definitely_entails(const Determinate& y) const {
00201 return prep == y.prep || y.prep->ph.contains(prep->ph);
00202 }
00203
00204 template <typename PS>
00205 inline bool
00206 Determinate<PS>::is_definitely_equivalent_to(const Determinate& y) const {
00207 return prep == y.prep || prep->ph == y.prep->ph;
00208 }
00209
00210 template <typename PS>
00211 inline bool
00212 Determinate<PS>::is_top() const {
00213 return prep->ph.is_universe();
00214 }
00215
00216 template <typename PS>
00217 inline bool
00218 Determinate<PS>::is_bottom() const {
00219 return prep->ph.is_empty();
00220 }
00221
00222 template <typename PS>
00223 inline memory_size_type
00224 Determinate<PS>::external_memory_in_bytes() const {
00225 return prep->total_memory_in_bytes();
00226 }
00227
00228 template <typename PS>
00229 inline memory_size_type
00230 Determinate<PS>::total_memory_in_bytes() const {
00231 return sizeof(*this) + external_memory_in_bytes();
00232 }
00233
00234 template <typename PS>
00235 inline bool
00236 Determinate<PS>::OK() const {
00237 return prep->ph.OK();
00238 }
00239
00240 namespace IO_Operators {
00241
00243 template <typename PS>
00244 inline std::ostream&
00245 operator<<(std::ostream& s, const Determinate<PS>& x) {
00246 s << x.element();
00247 return s;
00248 }
00249
00250 }
00251
00253 template <typename PS>
00254 inline bool
00255 operator==(const Determinate<PS>& x, const Determinate<PS>& y) {
00256 return x.prep == y.prep || x.prep->ph == y.prep->ph;
00257 }
00258
00260 template <typename PS>
00261 inline bool
00262 operator!=(const Determinate<PS>& x, const Determinate<PS>& y) {
00263 return x.prep != y.prep && x.prep->ph != y.prep->ph;
00264 }
00265
00266 template <typename PS>
00267 template <typename Binary_Operator_Assign>
00268 inline
00269 Determinate<PS>::Binary_Operator_Assign_Lifter<Binary_Operator_Assign>::
00270 Binary_Operator_Assign_Lifter(Binary_Operator_Assign op_assign)
00271 : op_assign_(op_assign) {
00272 }
00273
00274 template <typename PS>
00275 template <typename Binary_Operator_Assign>
00276 inline void
00277 Determinate<PS>::Binary_Operator_Assign_Lifter<Binary_Operator_Assign>::
00278 operator()(Determinate& x, const Determinate& y) const {
00279 op_assign_(x.element(), y.element());
00280 }
00281
00282 template <typename PS>
00283 template <typename Binary_Operator_Assign>
00284 inline
00285 Determinate<PS>::Binary_Operator_Assign_Lifter<Binary_Operator_Assign>
00286 Determinate<PS>::lift_op_assign(Binary_Operator_Assign op_assign) {
00287 return Binary_Operator_Assign_Lifter<Binary_Operator_Assign>(op_assign);
00288 }
00289
00290 }
00291
00292
00293 namespace std {
00294
00296 template <typename PS>
00297 inline void
00298 swap(Parma_Polyhedra_Library::Determinate<PS>& x,
00299 Parma_Polyhedra_Library::Determinate<PS>& y) {
00300 x.swap(y);
00301 }
00302
00303 }
00304
00305 #endif // !defined(PPL_Determinate_inlines_hh)