Parma_Polyhedra_Library::Powerset< D > Class Template Reference
[C++ Language Interface]

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

List of all members.

Public Types

typedef omega_iterator iterator
 Alias for a read-only bidirectional iterator on the disjuncts of a Powerset element.
typedef omega_const_iterator 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 Element
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.
size_type size () const
 Returns the number of disjuncts.
bool empty () const
 Returns true if and only if there are no disjuncts.
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 Element
Powersetoperator= (const Powerset &y)
 The assignment operator.
void 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.
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.
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 (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.
void add_non_bottom_disjunct (const D &d)
 Adds to *this the disjunct d, assuming d is not the bottom element.
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.

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>
bool operator== (const Powerset< D > &x, const Powerset< D > &y)
 Returns true if and only if x and y are equivalent.
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.
template<typename D>
std::ostream & operator<< (std::ostream &s, const Powerset< D > &x)
 Output operator.
template<typename D>
void swap (Parma_Polyhedra_Library::Powerset< D > &x, Parma_Polyhedra_Library::Powerset< D > &y)
 Specializes std::swap.


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 templatic 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 omega_iterator 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 [inline]

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>
Powerset< D >::iterator Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct ( const D &  d,
iterator  first,
iterator  last 
) [inline, 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.

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 
) [inline, 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>
bool operator== ( const Powerset< D > &  x,
const Powerset< D > &  y 
) [related]

Returns true if and only if x and y are equivalent.

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

Returns true if and only if x and y are not equivalent.

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

Output operator.

template<typename D>
void swap ( Parma_Polyhedra_Library::Powerset< D > &  x,
Parma_Polyhedra_Library::Powerset< D > &  y 
) [related]

Specializes std::swap.


Generated on Wed Jul 16 22:51:12 2008 for PPL by  doxygen 1.5.6