PPL  1.2
Powerset_inlines.hh
Go to the documentation of this file.
1 /* Powerset class implementation: inline functions.
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_inlines_hh
25 #define PPL_Powerset_inlines_hh 1
26 
27 #include "assertions.hh"
28 #include <algorithm>
29 
30 namespace Parma_Polyhedra_Library {
31 
32 template <typename D>
33 inline typename Powerset<D>::iterator
35  return sequence.begin();
36 }
37 
38 template <typename D>
39 inline typename Powerset<D>::iterator
41  return sequence.end();
42 }
43 
44 template <typename D>
45 inline typename Powerset<D>::const_iterator
47  return sequence.begin();
48 }
49 
50 template <typename D>
51 inline typename Powerset<D>::const_iterator
53  return sequence.end();
54 }
55 
56 template <typename D>
57 inline typename Powerset<D>::reverse_iterator
59  return reverse_iterator(end());
60 }
61 
62 template <typename D>
63 inline typename Powerset<D>::reverse_iterator
65  return reverse_iterator(begin());
66 }
67 
68 template <typename D>
71  return const_reverse_iterator(end());
72 }
73 
74 template <typename D>
77  return const_reverse_iterator(begin());
78 }
79 
80 template <typename D>
81 inline typename Powerset<D>::size_type
83  return sequence.size();
84 }
85 
86 template <typename D>
87 inline bool
89  return sequence.empty();
90 }
91 
92 template <typename D>
93 inline typename Powerset<D>::iterator
95  return sequence.erase(position.base);
96 }
97 
98 template <typename D>
99 inline void
101  sequence.erase(first.base, last.base);
102 }
103 
104 template <typename D>
105 inline void
107  sequence.clear();
108 }
109 
110 template <typename D>
111 inline
113  : sequence(y.sequence), reduced(y.reduced) {
114 }
115 
116 template <typename D>
117 inline Powerset<D>&
119  sequence = y.sequence;
120  reduced = y.reduced;
121  return *this;
122 }
123 
124 template <typename D>
125 inline void
127  std::swap(sequence, y.sequence);
128  std::swap(reduced, y.reduced);
129 }
130 
131 template <typename D>
132 inline
134  : sequence(), reduced(true) {
135 }
136 
137 template <typename D>
138 inline
140  : sequence(), reduced(false) {
141  sequence.push_back(d);
142  PPL_ASSERT_HEAVY(OK());
143 }
144 
145 template <typename D>
146 inline
148 }
149 
150 template <typename D>
151 inline void
153  // !d.is_bottom() is asserted by the callee.
154  add_non_bottom_disjunct_preserve_reduction(d, begin(), end());
155 }
156 
157 template <typename D>
158 inline void
160  sequence.push_back(d);
161  reduced = false;
162 }
163 
165 template <typename D>
166 inline
167 bool operator!=(const Powerset<D>& x, const Powerset<D>& y) {
168  return !(x == y);
169 }
170 
171 template <typename D>
172 inline bool
174  // Must perform omega-reduction for correctness.
175  omega_reduce();
176  const_iterator xi = begin();
177  const_iterator x_end = end();
178  return xi != x_end && xi->is_top() && ++xi == x_end;
179 }
180 
181 template <typename D>
182 inline bool
184  // Must perform omega-reduction for correctness.
185  omega_reduce();
186  return empty();
187 }
188 
189 template <typename D>
190 inline void
192  if (!empty()) {
193  collapse(sequence.begin());
194  }
195 }
196 
197 template <typename D>
198 inline void
200  pairwise_apply_assign(y, std::mem_fun_ref(&D::meet_assign));
201 }
202 
203 template <typename D>
204 inline void
206  least_upper_bound_assign(y);
207 }
208 
209 template <typename D>
210 inline bool
212  least_upper_bound_assign(y);
213  return true;
214 }
215 
216 template <typename D>
217 inline memory_size_type
219  return sizeof(*this) + external_memory_in_bytes();
220 }
221 
223 template <typename D>
224 inline void
226  x.m_swap(y);
227 }
228 
229 } // namespace Parma_Polyhedra_Library
230 
231 #endif // !defined(PPL_Powerset_inlines_hh)
size_type size() const
Returns the number of disjuncts.
void upper_bound_assign(const Powerset &y)
Assigns to *this an upper bound of *this and y.
void swap(CO_Tree &x, CO_Tree &y)
bool is_bottom() const
Returns true if and only if *this is the bottom element of the powerset constraint system (i...
Sequence sequence
The sequence container holding powerset's elements.
std::reverse_iterator< const_iterator > const_reverse_iterator
The reverse iterator type built from Powerset::const_iterator.
iterator add_non_bottom_disjunct_preserve_reduction(const D &d, iterator first, iterator last)
Adds to *this the disjunct d, assuming d is not the bottom element and ensuring partial Omega-reducti...
iterator drop_disjunct(iterator position)
Drops the disjunct in *this pointed to by position, returning an iterator to the disjunct following p...
memory_size_type total_memory_in_bytes() const
Returns a lower bound to the total size in bytes of the memory occupied by *this. ...
void clear()
Drops all the disjuncts, making *this an empty powerset.
reverse_iterator rbegin()
Returns a reverse_iterator pointing to the last disjunct, if *this is not empty; otherwise, returns the before-the-start reverse_iterator.
bool OK(bool disallow_bottom=false) const
Checks if all the invariants are satisfied.
iterator begin()
Returns an iterator pointing to the first disjunct, if *this is not empty; otherwise, returns the past-the-end iterator.
The powerset construction on a base-level domain.
bool operator!=(const Powerset< D > &x, const Powerset< D > &y)
bool reduced
If true, *this is Omega-reduced.
reverse_iterator rend()
Returns the before-the-start reverse_iterator.
Enable_If< Is_Native< T >::value, memory_size_type >::type external_memory_in_bytes(const T &)
For native types, returns the size in bytes of the memory managed by the type of the (unused) paramet...
Powerset()
Default constructor: builds the bottom of the powerset constraint system (i.e., the empty powerset)...
void m_swap(Powerset &y)
Swaps *this with y.
iterator end()
Returns the past-the-end iterator.
Base base
A (mutable) iterator on the sequence of elements.
A const_iterator on a sequence of read-only objects.
void meet_assign(const Powerset &y)
Assigns to *this the meet of *this and y.
void collapse()
If *this is not empty (i.e., it is not the bottom element), it is reduced to a singleton obtained by ...
The entire library is confined to this namespace.
Definition: version.hh:61
void add_disjunct(const D &d)
Adds to *this the disjunct d.
bool empty() const
Returns true if and only if there are no disjuncts in *this.
bool is_top() const
Returns true if and only if *this is the top element of the powerset constraint system (i...
std::reverse_iterator< iterator > reverse_iterator
The reverse iterator type built from Powerset::iterator.
An iterator on a sequence of read-only objects.
size_t memory_size_type
An unsigned integral type for representing memory size in bytes.
bool upper_bound_assign_if_exact(const Powerset &y)
Assigns to *this the least upper bound of *this and y and returns true.
Powerset & operator=(const Powerset &y)
The assignment operator.
void drop_disjuncts(iterator first, iterator last)
Drops all the disjuncts from first to last (excluded).
void swap(Powerset< D > &x, Powerset< D > &y)