24 #ifndef PPL_Powerset_inlines_hh
25 #define PPL_Powerset_inlines_hh 1
27 #include "assertions.hh"
33 inline typename Powerset<D>::iterator
35 return sequence.begin();
41 return sequence.end();
47 return sequence.begin();
53 return sequence.end();
83 return sequence.size();
89 return sequence.empty();
95 return sequence.erase(position.
base);
101 sequence.erase(first.
base, last.
base);
104 template <
typename D>
110 template <
typename D>
113 : sequence(y.sequence), reduced(y.reduced) {
116 template <
typename D>
124 template <
typename D>
131 template <
typename D>
134 : sequence(), reduced(true) {
137 template <
typename D>
140 : sequence(), reduced(false) {
142 PPL_ASSERT_HEAVY(
OK());
145 template <
typename D>
150 template <
typename D>
154 add_non_bottom_disjunct_preserve_reduction(d, begin(), end());
157 template <
typename D>
160 sequence.push_back(d);
165 template <
typename D>
171 template <
typename D>
178 return xi != x_end && xi->is_top() && ++xi == x_end;
181 template <
typename D>
189 template <
typename D>
193 collapse(sequence.begin());
197 template <
typename D>
200 pairwise_apply_assign(y, std::mem_fun_ref(&D::meet_assign));
203 template <
typename D>
206 least_upper_bound_assign(y);
209 template <
typename D>
212 least_upper_bound_assign(y);
216 template <
typename D>
223 template <
typename D>
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.
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.
Sequence::size_type size_type
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)