The powerset construction on a base-level domain. More...

#include <Powerset_defs.hh>

Inheritance diagram for Parma_Polyhedra_Library::Powerset< D >:

Public Types
typedef Sequence::size_type	size_type

typedef Sequence::value_type	value_type

typedef iterator_to_const< Sequence >	iterator
	Alias for a read-only bidirectional iterator on the disjuncts of a Powerset element. More...

typedef const_iterator_to_const< Sequence >	const_iterator
	A bidirectional const_iterator on the disjuncts of a Powerset element. More...

typedef std::reverse_iterator< iterator >	reverse_iterator
	The reverse iterator type built from Powerset::iterator. More...

typedef std::reverse_iterator< const_iterator >	const_reverse_iterator
	The reverse iterator type built from Powerset::const_iterator. More...

Public Member Functions
Constructors and Destructor
	Powerset ()
	Default constructor: builds the bottom of the powerset constraint system (i.e., the empty powerset). More...

	Powerset (const Powerset &y)
	Copy constructor. More...

	Powerset (const D &d)
	If `d` is not bottom, builds a powerset containing only `d`. Builds the empty powerset otherwise. More...

	~Powerset ()
	Destructor. More...

Member Functions that Do Not Modify the Powerset Object
bool	definitely_entails (const Powerset &y) const
	Returns `true` if `this` definitely entails `y`. Returns `false` if `this` may not entail `y` (i.e., if `*this` does not entail `y` or if entailment could not be decided). More...

bool	is_top () const
	Returns `true` if and only if `*this` is the top element of the powerset constraint system (i.e., it represents the universe). More...

bool	is_bottom () const
	Returns `true` if and only if `*this` is the bottom element of the powerset constraint system (i.e., it represents the empty set). More...

memory_size_type	total_memory_in_bytes () const
	Returns a lower bound to the total size in bytes of the memory occupied by `*this`. More...

memory_size_type	external_memory_in_bytes () const
	Returns a lower bound to the size in bytes of the memory managed by `*this`. More...

bool	OK (bool disallow_bottom=false) const
	Checks if all the invariants are satisfied. More...

Member Functions for the Direct Manipulation of Disjuncts
void	omega_reduce () const
	Drops from the sequence of disjuncts in `this` all the non-maximal elements so that `this` is non-redundant. More...

size_type	size () const
	Returns the number of disjuncts. More...

bool	empty () const
	Returns `true` if and only if there are no disjuncts in `*this`. More...

iterator	begin ()
	Returns an iterator pointing to the first disjunct, if `*this` is not empty; otherwise, returns the past-the-end iterator. More...

iterator	end ()
	Returns the past-the-end iterator. More...

const_iterator	begin () const
	Returns a const_iterator pointing to the first disjunct, if `*this` is not empty; otherwise, returns the past-the-end const_iterator. More...

const_iterator	end () const
	Returns the past-the-end const_iterator. More...

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. More...

reverse_iterator	rend ()
	Returns the before-the-start reverse_iterator. More...

const_reverse_iterator	rbegin () const
	Returns a const_reverse_iterator pointing to the last disjunct, if `*this` is not empty; otherwise, returns the before-the-start const_reverse_iterator. More...

const_reverse_iterator	rend () const
	Returns the before-the-start const_reverse_iterator. More...

void	add_disjunct (const D &d)
	Adds to `*this` the disjunct `d`. More...

iterator	drop_disjunct (iterator position)
	Drops the disjunct in `*this` pointed to by `position`, returning an iterator to the disjunct following `position`. More...

void	drop_disjuncts (iterator first, iterator last)
	Drops all the disjuncts from `first` to `last` (excluded). More...

void	clear ()
	Drops all the disjuncts, making `*this` an empty powerset. More...

Member Functions that May Modify the Powerset Object
Powerset &	operator= (const Powerset &y)
	The assignment operator. More...

void	m_swap (Powerset &y)
	Swaps `*this` with `y`. More...

void	least_upper_bound_assign (const Powerset &y)
	Assigns to `this` the least upper bound of `this` and `y`. More...

void	upper_bound_assign (const Powerset &y)
	Assigns to `this` an upper bound of `this` and `y`. More...

bool	upper_bound_assign_if_exact (const Powerset &y)
	Assigns to `this` the least upper bound of `this` and `y` and returns `true`. More...

void	meet_assign (const Powerset &y)
	Assigns to `this` the meet of `this` and `y`. More...

void	collapse ()
	If `*this` is not empty (i.e., it is not the bottom element), it is reduced to a singleton obtained by computing an upper-bound of all the disjuncts. More...

Protected Types
typedef std::list< D >	Sequence
	A powerset is implemented as a sequence of elements. More...

typedef Sequence::iterator	Sequence_iterator
	Alias for the low-level iterator on the disjuncts. More...

typedef Sequence::const_iterator	Sequence_const_iterator
	Alias for the low-level const_iterator on the disjuncts. More...

Protected Member Functions
bool	is_omega_reduced () const
	Returns `true` if and only if `*this` does not contain non-maximal elements. More...

void	collapse (unsigned max_disjuncts)
	Upon return, `*this` will contain at most `max_disjuncts` elements; the set of disjuncts in positions greater than or equal to `max_disjuncts`, will be replaced at that position by their upper-bound. More...

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-reduction. More...

void	add_non_bottom_disjunct_preserve_reduction (const D &d)
	Adds to `*this` the disjunct `d`, assuming `d` is not the bottom element and preserving Omega-reduction. More...

template<typename Binary_Operator_Assign >
void	pairwise_apply_assign (const Powerset &y, Binary_Operator_Assign op_assign)
	Assigns to `this` the result of applying `op_assign` pairwise to the elements in `this` and `y`. More...

Protected Attributes
Sequence	sequence
	The sequence container holding powerset's elements. More...

bool	reduced
	If `true`, `*this` is Omega-reduced. More...

Private Member Functions
bool	check_omega_reduced () const
	Does the hard work of checking whether `*this` contains non-maximal elements and returns `true` if and only if it does not. More...

void	collapse (Sequence_iterator sink)
	Replaces the disjunct `*sink` by an upper bound of itself and all the disjuncts following it. More...

Related Functions
(Note that these are not member functions.)
template<typename D >
void	swap (Powerset< D > &x, Powerset< D > &y)
	Swaps `x` with `y`. More...

template<typename D >
bool	operator== (const Powerset< D > &x, const Powerset< D > &y)
	Returns `true` if and only if `x` and `y` are equivalent. More...

template<typename D >
bool	operator!= (const Powerset< D > &x, const Powerset< D > &y)
	Returns `true` if and only if `x` and `y` are not equivalent. More...

template<typename D >
std::ostream &	operator<< (std::ostream &s, const Powerset< D > &x)
	Output operator. More...

template<typename D >
bool	operator!= (const Powerset< D > &x, const Powerset< D > &y)

template<typename D >
void	swap (Powerset< D > &x, Powerset< D > &y)

template<typename D >
bool	operator== (const Powerset< D > &x, const Powerset< D > &y)

template<typename D >
std::ostream &	operator<< (std::ostream &s, const Powerset< D > &x)

Detailed Description

template<typename D>
class Parma_Polyhedra_Library::Powerset< D >

The powerset construction on a base-level domain.

This class offers a generic implementation of a powerset domain as defined in Section The Powerset Construction.

Besides invoking the available methods on the disjuncts of a Powerset, this class also provides bidirectional iterators that allow for a direct inspection of these disjuncts. For a consistent handling of Omega-reduction, all the iterators are read-only, meaning that the disjuncts cannot be overwritten. Rather, by using the class iterator, it is possible to drop one or more disjuncts (possibly so as to later add back modified versions). As an example of iterator usage, the following template function drops from powerset ps all the disjuncts that would have become redundant by the addition of an external element d.

template <typename D>
void
drop_subsumed(Powerset<D>& ps, const D& d) {
  for (typename Powerset<D>::iterator i = ps.begin(),
         ps_end = ps.end(), i != ps_end; )
    if (i->definitely_entails(d))
      i = ps.drop_disjunct(i);
    else
      ++i;
}

The template class D must provide the following methods.

memory_size_type total_memory_in_bytes() const

Returns a lower bound on the total size in bytes of the memory occupied by the instance of D.

bool is_top() const

Returns true if and only if the instance of D is the top element of the domain.

bool is_bottom() const

Returns true if and only if the instance of D is the bottom element of the domain.

bool definitely_entails(const D& y) const

Returns true if the instance of D definitely entails y. Returns false if the instance may not entail y (i.e., if the instance does not entail y or if entailment could not be decided).

void upper_bound_assign(const D& y)

Assigns to the instance of D an upper bound of the instance and y.

void meet_assign(const D& y)

Assigns to the instance of D the meet of the instance and y.

bool OK() const

Returns true if the instance of D is in a consistent state, else returns false.

The following operators on the template class D must be defined.

operator<<(std::ostream& s, const D& x)

Writes a textual representation of the instance of D on s.

operator==(const D& x, const D& y)

Returns true if and only if x and y are equivalent D's.

operator!=(const D& x, const D& y)

Returns true if and only if x and y are different D's.

Definition at line 152 of file Powerset_defs.hh.

Member Typedef Documentation

template<typename D>

typedef const_iterator_to_const<Sequence> Parma_Polyhedra_Library::Powerset< D >::const_iterator

A bidirectional const_iterator on the disjuncts of a Powerset element.

Definition at line 258 of file Powerset_defs.hh.

template<typename D>

typedef std::reverse_iterator<const_iterator> Parma_Polyhedra_Library::Powerset< D >::const_reverse_iterator

The reverse iterator type built from Powerset::const_iterator.

Definition at line 264 of file Powerset_defs.hh.

template<typename D>

typedef iterator_to_const<Sequence> Parma_Polyhedra_Library::Powerset< D >::iterator

Alias for a read-only bidirectional iterator on the disjuncts of a Powerset element.

By using this iterator type, the disjuncts cannot be overwritten, but they can be removed using methods drop_disjunct(iterator position) and drop_disjuncts(iterator first, iterator last), while still ensuring a correct handling of Omega-reduction.

Definition at line 255 of file Powerset_defs.hh.

template<typename D>

typedef std::reverse_iterator<iterator> Parma_Polyhedra_Library::Powerset< D >::reverse_iterator

The reverse iterator type built from Powerset::iterator.

Definition at line 261 of file Powerset_defs.hh.

template<typename D>

typedef std::list<D> Parma_Polyhedra_Library::Powerset< D >::Sequence

protected

A powerset is implemented as a sequence of elements.

The particular sequence employed must support efficient deletion in any position and efficient back insertion.

Definition at line 226 of file Powerset_defs.hh.

template<typename D>

typedef Sequence::const_iterator Parma_Polyhedra_Library::Powerset< D >::Sequence_const_iterator

protected

Alias for the low-level const_iterator on the disjuncts.

Definition at line 232 of file Powerset_defs.hh.

template<typename D>

typedef Sequence::iterator Parma_Polyhedra_Library::Powerset< D >::Sequence_iterator

protected

Alias for the low-level iterator on the disjuncts.

Definition at line 229 of file Powerset_defs.hh.

template<typename D>

typedef Sequence::size_type Parma_Polyhedra_Library::Powerset< D >::size_type

Definition at line 242 of file Powerset_defs.hh.

template<typename D>

typedef Sequence::value_type Parma_Polyhedra_Library::Powerset< D >::value_type

Definition at line 243 of file Powerset_defs.hh.

Constructor & Destructor Documentation

template<typename D >

Parma_Polyhedra_Library::Powerset< D >::Powerset ( )

inline

Default constructor: builds the bottom of the powerset constraint system (i.e., the empty powerset).

Definition at line 133 of file Powerset_inlines.hh.

134 : sequence(), reduced(true) {

135 }

Parma_Polyhedra_Library::Powerset::sequence

Sequence sequence

The sequence container holding powerset's elements.

Definition: Powerset_defs.hh:235

Parma_Polyhedra_Library::Powerset::reduced

bool reduced

If true, *this is Omega-reduced.

Definition: Powerset_defs.hh:238

template<typename D >

Parma_Polyhedra_Library::Powerset< D >::Powerset ( const Powerset< D > & y )

inline

Copy constructor.

Definition at line 112 of file Powerset_inlines.hh.

113 : sequence(y.sequence), reduced(y.reduced) {

114 }

Parma_Polyhedra_Library::Powerset::sequence

Sequence sequence

The sequence container holding powerset's elements.

Definition: Powerset_defs.hh:235

Parma_Polyhedra_Library::Powerset::reduced

bool reduced

If true, *this is Omega-reduced.

Definition: Powerset_defs.hh:238

template<typename D>

Parma_Polyhedra_Library::Powerset< D >::Powerset ( const D & d )

inlineexplicit

If d is not bottom, builds a powerset containing only d. Builds the empty powerset otherwise.

Definition at line 139 of file Powerset_inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::OK(), and Parma_Polyhedra_Library::Powerset< D >::sequence.

   : sequence(), reduced(false) {
   sequence.push_back(d);
   PPL_ASSERT_HEAVY(OK());
 }

template<typename D >

Parma_Polyhedra_Library::Powerset< D >::~Powerset ( )

inline

Destructor.

Definition at line 147 of file Powerset_inlines.hh.

147 {

148 }

Member Function Documentation

template<typename D>

void Parma_Polyhedra_Library::Powerset< D >::add_disjunct ( const D & d )

inline

Adds to *this the disjunct d.

Definition at line 159 of file Powerset_inlines.hh.

                                     {
   sequence.push_back(d);
   reduced = false;
 }

template<typename D>

Powerset< D >::iterator Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct_preserve_reduction	(	const D &	d,
		iterator	first,
		iterator	last
	)

protected

Adds to *this the disjunct d, assuming d is not the bottom element and ensuring partial Omega-reduction.

If d is not the bottom element and is not Omega-redundant with respect to elements in positions between first and last, all elements in these positions that would be made Omega-redundant by the addition of d are dropped and d is added to the reduced sequence. If *this is reduced before an invocation of this method, it will be reduced upon successful return from the method.

Definition at line 168 of file Powerset_templates.hh.

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PSET >::BGP99_heuristics_assign(), and Parma_Polyhedra_Library::Pointset_Powerset< PSET >::pairwise_reduce().

                                                                        {
   PPL_ASSERT_HEAVY(!d.is_bottom());
   for (iterator xi = first; xi != last; ) {
     const D& xv = *xi;
     if (d.definitely_entails(xv)) {
       return first;
     }
     else if (xv.definitely_entails(d)) {
       if (xi == first) {
         ++first;
       }
       xi = drop_disjunct(xi);
     }
     else {
       ++xi;
     }
   }
   sequence.push_back(d);
   PPL_ASSERT_HEAVY(OK());
   return first;
 }

template<typename D>

void Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct_preserve_reduction ( const D & d )

inlineprotected

Adds to *this the disjunct d, assuming d is not the bottom element and preserving Omega-reduction.

If *this is reduced before an invocation of this method, it will be reduced upon successful return from the method.

Definition at line 152 of file Powerset_inlines.hh.

                                                                   {
   // !d.is_bottom() is asserted by the callee.
   add_non_bottom_disjunct_preserve_reduction(d, begin(), end());
 }

template<typename D >

Powerset< D >::iterator Parma_Polyhedra_Library::Powerset< D >::begin ( )

inline

Returns an iterator pointing to the first disjunct, if *this is not empty; otherwise, returns the past-the-end iterator.

Definition at line 34 of file Powerset_inlines.hh.

                    {
   return sequence.begin();
 }

template<typename D >

Powerset< D >::const_iterator Parma_Polyhedra_Library::Powerset< D >::begin ( ) const

inline

Returns a const_iterator pointing to the first disjunct, if *this is not empty; otherwise, returns the past-the-end const_iterator.

Definition at line 46 of file Powerset_inlines.hh.

                          {
   return sequence.begin();
 }

template<typename D >

bool Parma_Polyhedra_Library::Powerset< D >::check_omega_reduced ( ) const

private

Does the hard work of checking whether *this contains non-maximal elements and returns true if and only if it does not.

Definition at line 137 of file Powerset_templates.hh.

                                        {
   for (const_iterator x_begin = begin(), x_end = end(),
          xi = x_begin; xi != x_end; ++xi) {
     const D& xv = *xi;
     if (xv.is_bottom()) {
       return false;
     }
     for (const_iterator yi = x_begin; yi != x_end; ++yi) {
       if (xi == yi) {
         continue;
       }
       const D& yv = *yi;
       if (xv.definitely_entails(yv) || yv.definitely_entails(xv)) {
         return false;
       }
     }
   }
   return true;
 }

template<typename D >

void Parma_Polyhedra_Library::Powerset< D >::clear ( )

inline

Drops all the disjuncts, making *this an empty powerset.

Definition at line 106 of file Powerset_inlines.hh.

                    {
   sequence.clear();
 }

template<typename D >

void Parma_Polyhedra_Library::Powerset< D >::collapse ( )

inline

If *this is not empty (i.e., it is not the bottom element), it is reduced to a singleton obtained by computing an upper-bound of all the disjuncts.

Definition at line 191 of file Powerset_inlines.hh.

References Parma_Polyhedra_Library::Implementation::BD_Shapes::empty.

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PSET >::BGP99_extrapolation_assign(), and Parma_Polyhedra_Library::Powerset< D >::omega_reduce().

                       {
   if (!empty()) {
     collapse(sequence.begin());
   }
 }

template<typename D >

void Parma_Polyhedra_Library::Powerset< D >::collapse ( unsigned max_disjuncts )

protected

Upon return, *this will contain at most max_disjuncts elements; the set of disjuncts in positions greater than or equal to max_disjuncts, will be replaced at that position by their upper-bound.

Definition at line 118 of file Powerset_templates.hh.

References Parma_Polyhedra_Library::iterator_to_const< Container >::base.

                                                   {
   PPL_ASSERT(max_disjuncts > 0);
   // Omega-reduce before counting the number of disjuncts.
   omega_reduce();
   size_type n = size();
   if (n > max_disjuncts) {
     // Let `i' point to the last disjunct that will survive.
     iterator i = begin();
     std::advance(i, max_disjuncts-1);
     // This disjunct will be assigned an upper-bound of itself and of
     // all the disjuncts that follow.
     collapse(i.base);
   }
   PPL_ASSERT_HEAVY(OK());
   PPL_ASSERT(is_omega_reduced());
 }

template<typename D >

void Parma_Polyhedra_Library::Powerset< D >::collapse ( Sequence_iterator sink )

private

Replaces the disjunct *sink by an upper bound of itself and all the disjuncts following it.

Definition at line 36 of file Powerset_templates.hh.

                                                   {
   PPL_ASSERT(sink != sequence.end());
   D& d = *sink;
   iterator x_sink = sink;
   iterator next_x_sink = x_sink;
   ++next_x_sink;
   iterator x_end = end();
   for (const_iterator xi = next_x_sink; xi != x_end; ++xi) {
     d.upper_bound_assign(*xi);
   }
   // Drop the surplus disjuncts.
   drop_disjuncts(next_x_sink, x_end);
 
   // Ensure omega-reduction.
   for (iterator xi = begin(); xi != x_sink; ) {
     if (xi->definitely_entails(d)) {
       xi = drop_disjunct(xi);
     }
     else {
       ++xi;
     }
   }
 
   PPL_ASSERT_HEAVY(OK());
 }

template<typename D >

bool Parma_Polyhedra_Library::Powerset< D >::definitely_entails ( const Powerset< D > & y ) const

Returns true if *this definitely entails y. Returns false if *this may not entail y (i.e., if *this does not entail y or if entailment could not be decided).

Definition at line 194 of file Powerset_templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::definitely_entails(), and Parma_Polyhedra_Library::Powerset< D >::end().

Referenced by Parma_Polyhedra_Library::Powerset< D >::definitely_entails().

                                                        {
   const Powerset<D>& x = *this;
   bool found = true;
   for (const_iterator xi = x.begin(),
          x_end = x.end(); found && xi != x_end; ++xi) {
     found = false;
     for (const_iterator yi = y.begin(),
            y_end = y.end(); !found && yi != y_end; ++yi) {
       found = (*xi).definitely_entails(*yi);
     }
   }
   return found;
 }

template<typename D >

Powerset< D >::iterator Parma_Polyhedra_Library::Powerset< D >::drop_disjunct ( iterator position )

inline

Drops the disjunct in *this pointed to by position, returning an iterator to the disjunct following position.

Definition at line 94 of file Powerset_inlines.hh.

References Parma_Polyhedra_Library::iterator_to_const< Container >::base.

Referenced by Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), and Parma_Polyhedra_Library::Powerset< D >::operator==().

                                             {
   return sequence.erase(position.base);
 }

template<typename D >

void Parma_Polyhedra_Library::Powerset< D >::drop_disjuncts	(	iterator	first,
		iterator	last
	)

inline

Drops all the disjuncts from first to last (excluded).

Definition at line 100 of file Powerset_inlines.hh.

References Parma_Polyhedra_Library::iterator_to_const< Container >::base.

                                                          {
   sequence.erase(first.base, last.base);
 }

template<typename D >

bool Parma_Polyhedra_Library::Powerset< D >::empty ( ) const

inline

Returns true if and only if there are no disjuncts in *this.

Definition at line 88 of file Powerset_inlines.hh.

                          {
   return sequence.empty();
 }

template<typename D >

Powerset< D >::iterator Parma_Polyhedra_Library::Powerset< D >::end ( )

inline

Returns the past-the-end iterator.

Definition at line 40 of file Powerset_inlines.hh.

                  {
   return sequence.end();
 }

template<typename D >

Powerset< D >::const_iterator Parma_Polyhedra_Library::Powerset< D >::end ( ) const

inline

Returns the past-the-end const_iterator.

Definition at line 52 of file Powerset_inlines.hh.

                        {
   return sequence.end();
 }

template<typename D >

memory_size_type Parma_Polyhedra_Library::Powerset< D >::external_memory_in_bytes ( ) const

Returns a lower bound to the size in bytes of the memory managed by *this.

Definition at line 304 of file Powerset_templates.hh.

                                             {
   memory_size_type bytes = 0;
   for (const_iterator xi = begin(), x_end = end(); xi != x_end; ++xi) {
     bytes += xi->total_memory_in_bytes();
     // We assume there is at least a forward and a backward link, and
     // that the pointers implementing them are at least the size of
     // pointers to `D'.
     bytes += 2*sizeof(D*);
   }
   return bytes;
 }

template<typename D >

bool Parma_Polyhedra_Library::Powerset< D >::is_bottom ( ) const

inline

Returns true if and only if *this is the bottom element of the powerset constraint system (i.e., it represents the empty set).

Definition at line 183 of file Powerset_inlines.hh.

References Parma_Polyhedra_Library::Implementation::BD_Shapes::empty.

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PSET >::map_space_dimensions().

                              {
   // Must perform omega-reduction for correctness.
   omega_reduce();
   return empty();
 }

template<typename D >

bool Parma_Polyhedra_Library::Powerset< D >::is_omega_reduced ( ) const

protected

Returns true if and only if *this does not contain non-maximal elements.

Definition at line 159 of file Powerset_templates.hh.

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PSET >::BGP99_heuristics_assign(), Parma_Polyhedra_Library::Pointset_Powerset< PSET >::collect_certificates(), and Parma_Polyhedra_Library::Pointset_Powerset< PSET >::is_universe().

                                     {
   if (!reduced && check_omega_reduced()) {
     reduced = true;
   }
   return reduced;
 }

template<typename D >

bool Parma_Polyhedra_Library::Powerset< D >::is_top ( ) const

inline

Returns true if and only if *this is the top element of the powerset constraint system (i.e., it represents the universe).

Definition at line 173 of file Powerset_inlines.hh.

                           {
   // Must perform omega-reduction for correctness.
   omega_reduce();
   const_iterator xi = begin();
   const_iterator x_end = end();
   return xi != x_end && xi->is_top() && ++xi == x_end;
 }

template<typename D >

void Parma_Polyhedra_Library::Powerset< D >::least_upper_bound_assign ( const Powerset< D > & y )

Assigns to *this the least upper bound of *this and y.

Definition at line 261 of file Powerset_templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::end(), and Parma_Polyhedra_Library::Powerset< D >::omega_reduce().

                                                        {
   // Ensure omega-reduction here, since what follows has quadratic complexity.
   omega_reduce();
   y.omega_reduce();
   iterator old_begin = begin();
   iterator old_end = end();
   for (const_iterator i = y.begin(), y_end = y.end(); i != y_end; ++i) {
     old_begin = add_non_bottom_disjunct_preserve_reduction(*i,
                                                            old_begin,
                                                            old_end);
   }
   PPL_ASSERT_HEAVY(OK());
 }

template<typename D >

void Parma_Polyhedra_Library::Powerset< D >::m_swap ( Powerset< D > & y )

inline

Swaps *this with y.

Definition at line 126 of file Powerset_inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::reduced, Parma_Polyhedra_Library::Powerset< D >::sequence, and Parma_Polyhedra_Library::swap().

Referenced by Parma_Polyhedra_Library::Powerset< D >::swap().

                                {
   std::swap(sequence, y.sequence);
   std::swap(reduced, y.reduced);
 }

template<typename D >

void Parma_Polyhedra_Library::Powerset< D >::meet_assign ( const Powerset< D > & y )

inline

Assigns to *this the meet of *this and y.

Definition at line 199 of file Powerset_inlines.hh.

                                           {
   pairwise_apply_assign(y, std::mem_fun_ref(&D::meet_assign));
 }

template<typename D >

bool Parma_Polyhedra_Library::Powerset< D >::OK ( bool disallow_bottom = false ) const

Checks if all the invariants are satisfied.

Definition at line 318 of file Powerset_templates.hh.

Referenced by Parma_Polyhedra_Library::Powerset< D >::Powerset().

                                                 {
   for (const_iterator xi = begin(), x_end = end(); xi != x_end; ++xi) {
     if (!xi->OK()) {
       return false;
     }
     if (disallow_bottom && xi->is_bottom()) {
 #ifndef NDEBUG
       std::cerr << "Bottom element in powerset!"
                 << std::endl;
 #endif
       return false;
     }
   }
   if (reduced && !check_omega_reduced()) {
 #ifndef NDEBUG
     std::cerr << "Powerset claims to be reduced, but it is not!"
               << std::endl;
 #endif
     return false;
   }
   return true;
 }

template<typename D >

void Parma_Polyhedra_Library::Powerset< D >::omega_reduce ( ) const

Drops from the sequence of disjuncts in *this all the non-maximal elements so that *this is non-redundant.

This method is declared const because, even though Omega-reduction may change the syntactic representation of *this, its semantics will be unchanged.

Definition at line 64 of file Powerset_templates.hh.

References Parma_Polyhedra_Library::abandon_expensive_computations, Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::collapse(), Parma_Polyhedra_Library::Powerset< D >::drop_disjunct(), and Parma_Polyhedra_Library::Powerset< D >::end().

                                 {
   if (reduced) {
     return;
   }
   Powerset& x = const_cast<Powerset&>(*this);
   // First remove all bottom elements.
   for (iterator xi = x.begin(), x_end = x.end(); xi != x_end; ) {
     if (xi->is_bottom()) {
       xi = x.drop_disjunct(xi);
     }
     else {
       ++xi;
     }
   }
   // Then remove non-maximal elements.
   for (iterator xi = x.begin(); xi != x.end(); ) {
     const D& xv = *xi;
     bool dropping_xi = false;
     for (iterator yi = x.begin(); yi != x.end(); ) {
       if (xi == yi) {
         ++yi;
       }
       else {
         const D& yv = *yi;
         if (yv.definitely_entails(xv)) {
           yi = x.drop_disjunct(yi);
         }
         else if (xv.definitely_entails(yv)) {
           dropping_xi = true;
           break;
         }
         else {
           ++yi;
         }
       }
     }
     if (dropping_xi) {
       xi = x.drop_disjunct(xi);
     }
     else {
       ++xi;
     }
     if (abandon_expensive_computations != 0 && xi != x.end()) {
       // Hurry up!
       x.collapse(xi.base);
       break;
     }
   }
   reduced = true;
   PPL_ASSERT_HEAVY(OK());
 }

template<typename D >

Powerset< D > & Parma_Polyhedra_Library::Powerset< D >::operator= ( const Powerset< D > & y )

inline

The assignment operator.

Definition at line 118 of file Powerset_inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

                                         {
   sequence = y.sequence;
   reduced = y.reduced;
   return *this;
 }

template<typename D >

template<typename Binary_Operator_Assign >

void Parma_Polyhedra_Library::Powerset< D >::pairwise_apply_assign	(	const Powerset< D > &	y,
		Binary_Operator_Assign	op_assign
	)

protected

Assigns to *this the result of applying op_assign pairwise to the elements in *this and y.

The elements of the powerset result are obtained by applying op_assign to each pair of elements whose components are drawn from *this and y, respectively.

Definition at line 237 of file Powerset_templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), and Parma_Polyhedra_Library::swap().

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PSET >::intersection_assign(), and Parma_Polyhedra_Library::Pointset_Powerset< PSET >::time_elapse_assign().

                                                                      {
   // Ensure omega-reduction here, since what follows has quadratic complexity.
   omega_reduce();
   y.omega_reduce();
   Sequence new_sequence;
   for (const_iterator xi = begin(), x_end = end(),
          y_begin = y.begin(), y_end = y.end(); xi != x_end; ++xi) {
     for (const_iterator yi = y_begin; yi != y_end; ++yi) {
       D zi = *xi;
       op_assign(zi, *yi);
       if (!zi.is_bottom()) {
         new_sequence.push_back(zi);
       }
     }
   }
   // Put the new sequence in place.
   std::swap(sequence, new_sequence);
   reduced = false;
   PPL_ASSERT_HEAVY(OK());
 }

template<typename D >

Powerset< D >::reverse_iterator Parma_Polyhedra_Library::Powerset< D >::rbegin ( )

inline

Returns a reverse_iterator pointing to the last disjunct, if *this is not empty; otherwise, returns the before-the-start reverse_iterator.

Definition at line 58 of file Powerset_inlines.hh.

                     {
   return reverse_iterator(end());
 }

template<typename D >

Powerset< D >::const_reverse_iterator Parma_Polyhedra_Library::Powerset< D >::rbegin ( ) const

inline

Returns a const_reverse_iterator pointing to the last disjunct, if *this is not empty; otherwise, returns the before-the-start const_reverse_iterator.

Definition at line 70 of file Powerset_inlines.hh.

                           {
   return const_reverse_iterator(end());
 }

template<typename D >

Powerset< D >::reverse_iterator Parma_Polyhedra_Library::Powerset< D >::rend ( )

inline

Returns the before-the-start reverse_iterator.

Definition at line 64 of file Powerset_inlines.hh.

                   {
   return reverse_iterator(begin());
 }

template<typename D >

Powerset< D >::const_reverse_iterator Parma_Polyhedra_Library::Powerset< D >::rend ( ) const

inline

Returns the before-the-start const_reverse_iterator.

Definition at line 76 of file Powerset_inlines.hh.

                         {
   return const_reverse_iterator(begin());
 }

template<typename D >

Powerset< D >::size_type Parma_Polyhedra_Library::Powerset< D >::size ( ) const

inline

Returns the number of disjuncts.

Definition at line 82 of file Powerset_inlines.hh.

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PSET >::ascii_dump(), Parma_Polyhedra_Library::Pointset_Powerset< PSET >::BGP99_heuristics_assign(), Parma_Polyhedra_Library::Pointset_Powerset< PSET >::BHZ03_widening_assign(), Parma_Polyhedra_Library::Pointset_Powerset< PSET >::is_universe(), Parma_Polyhedra_Library::Powerset< D >::operator==(), Parma_Polyhedra_Library::Pointset_Powerset< PSET >::pairwise_reduce(), and Parma_Polyhedra_Library::Pointset_Powerset< PSET >::simplify_using_context_assign().

                         {
   return sequence.size();
 }

template<typename D >

memory_size_type Parma_Polyhedra_Library::Powerset< D >::total_memory_in_bytes ( ) const

inline

Returns a lower bound to the total size in bytes of the memory occupied by *this.

Definition at line 218 of file Powerset_inlines.hh.

References Parma_Polyhedra_Library::external_memory_in_bytes().

                                          {
   return sizeof(*this) + external_memory_in_bytes();
 }

template<typename D >

void Parma_Polyhedra_Library::Powerset< D >::upper_bound_assign ( const Powerset< D > & y )

inline

Assigns to *this an upper bound of *this and y.

The result will be the least upper bound of *this and y.

Definition at line 205 of file Powerset_inlines.hh.

                                                  {
   least_upper_bound_assign(y);
 }

template<typename D >

bool Parma_Polyhedra_Library::Powerset< D >::upper_bound_assign_if_exact ( const Powerset< D > & y )

inline

Assigns to *this the least upper bound of *this and y and returns true.

Exceptions

std::invalid_argument Thrown if *this and y are dimension-incompatible.

Definition at line 211 of file Powerset_inlines.hh.

                                                           {
   least_upper_bound_assign(y);
   return true;
 }

Friends And Related Function Documentation

template<typename D >

bool operator!=	(	const Powerset< D > &	x,
		const Powerset< D > &	y
	)

template<typename D >

bool operator!=	(	const Powerset< D > &	x,
		const Powerset< D > &	y
	)

                                                             {
   return !(x == y);
 }

template<typename D >

std::ostream & operator<<	(	std::ostream &	s,
		const Powerset< D > &	x
	)

template<typename D >

std::ostream & operator<<	(	std::ostream &	s,
		const Powerset< D > &	x
	)

                                                 {
   if (x.is_bottom()) {
     s << "false";
   }
   else if (x.is_top()) {
     s << "true";
   }
   else {
     for (typename Powerset<D>::const_iterator i = x.begin(),
            x_end = x.end(); i != x_end; ) {
       s << "{ " << *i << " }";
       ++i;
       if (i != x_end) {
         s << ", ";
       }
     }
   }
   return s;
 }

template<typename D >

bool operator==	(	const Powerset< D > &	x,
		const Powerset< D > &	y
	)

template<typename D >

bool operator==	(	const Powerset< D > &	x,
		const Powerset< D > &	y
	)

References Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::drop_disjunct(), Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), and Parma_Polyhedra_Library::Powerset< D >::size().

                                                        {
   x.omega_reduce();
   y.omega_reduce();
   if (x.size() != y.size()) {
     return false;
   }
   // Take a copy of `y' and work with it.
   Powerset<D> z = y;
   for (typename Powerset<D>::const_iterator xi = x.begin(),
          x_end = x.end(); xi != x_end; ++xi) {
     typename Powerset<D>::iterator zi = z.begin();
     typename Powerset<D>::iterator z_end = z.end();
     zi = std::find(zi, z_end, *xi);
     if (zi == z_end) {
       return false;
     }
     else {
       z.drop_disjunct(zi);
     }
   }
   return true;
 }

template<typename D >

void swap	(	Powerset< D > &	x,
		Powerset< D > &	y
	)

template<typename D >

void swap	(	Powerset< D > &	x,
		Powerset< D > &	y
	)

References Parma_Polyhedra_Library::Powerset< D >::m_swap().

                                      {
   x.m_swap(y);
 }

Member Data Documentation

template<typename D>

bool Parma_Polyhedra_Library::Powerset< D >::reduced

mutableprotected

If true, *this is Omega-reduced.

Definition at line 238 of file Powerset_defs.hh.

template<typename D>

Sequence Parma_Polyhedra_Library::Powerset< D >::sequence

protected

The sequence container holding powerset's elements.

Definition at line 235 of file Powerset_defs.hh.

The documentation for this class was generated from the following files:

Public Types

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Private Member Functions

Related Functions

Detailed Description

template<typename D> class Parma_Polyhedra_Library::Powerset< D >

Member Typedef Documentation

Constructor & Destructor Documentation

Member Function Documentation

Friends And Related Function Documentation

Member Data Documentation

template<typename D>
class Parma_Polyhedra_Library::Powerset< D >