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

#include <ppl.hh>

Public Types
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.

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

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

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

	Powerset (const Powerset &y)
	Copy constructor.

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

	~Powerset ()
	Destructor.

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

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

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

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

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

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

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.

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

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

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

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.

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

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.

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

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.

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

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

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

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

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

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

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

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

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

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.

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.

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

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

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.

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.

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

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.

Member Typedef Documentation

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.

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.

Member Function Documentation

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.

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.

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.

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.

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.

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.

Friends And Related Function Documentation

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 >

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

template<typename D >

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

template<typename D >

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

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

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

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

ppl.hh

Public Types

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Related Functions

Detailed Description

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

Member Typedef Documentation

Member Function Documentation

Friends And Related Function Documentation

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