Main Page | Modules | Namespace List | Class Hierarchy | Class List | Namespace Members | Class Members | Related Pages

Parma_Polyhedra_Library::PowerSet< CS > Class Template Reference

The powerset construction on constraint systems. More...

List of all members.

Public Member Functions

 PowerSet ()
 Default constructor.
 PowerSet (const PowerSet &y)
 Ordinary copy-constructor.
PowerSetoperator= (const PowerSet &y)
 The assignment operator.
void swap (PowerSet &y)
 Swaps *this with y.
void add_disjunct (const CS &d)
 Adds to *this the disjunct d.
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.
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).
bool OK (bool disallow_bottom=false) const
 Checks if all the invariants are satisfied.
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< CS > Sequence
 A powerset is implemented as a sequence of elements.

Protected Member Functions

void omega_reduce () const
 Erase from *this all the non-maximal elements.
bool is_omega_reduced () const
 Returns true if and only if *this does not contain non-maximal elements.

Static Protected Member Functions

void add_non_bottom_disjunct (Sequence &s, const CS &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 (Sequence &s, const CS &d)
 Adds to *this the disjunct d, assuming d is not the bottom element.

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

bool operator== (const PowerSet< CS > &x, const PowerSet< CS > &y)
 Returns true if and only if x and y are equivalent.
bool operator!= (const PowerSet< CS > &x, const PowerSet< CS > &y)
 Returns true if and only if x and y are not equivalent.
std::ostream & operator<< (std::ostream &s, const PowerSet< CS > &x)
 Output operator.
void swap (Parma_Polyhedra_Library::PowerSet< CS > &x, Parma_Polyhedra_Library::PowerSet< CS > &y)
 Specializes std::swap.


Detailed Description

template<typename CS>
class Parma_Polyhedra_Library::PowerSet< CS >

The powerset construction on constraint systems.

This class offers a generic implementation of powerset constraint systems as defined in [Bag98].


Member Typedef Documentation

template<typename CS>
typedef std::list<CS> Parma_Polyhedra_Library::PowerSet< CS >::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.


Member Function Documentation

template<typename CS>
void Parma_Polyhedra_Library::PowerSet< CS >::add_non_bottom_disjunct Sequence s,
const CS &  d,
iterator &  first,
iterator  last
[static, 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 redundant with respect to the elements in positions between first and last, adds to *this the disjunct d, erasing all the elements in the above mentioned positions that are made omega-redundant by the addition of d.


Generated on Fri Aug 20 20:04:45 2004 for PPL by doxygen 1.3.8-20040812