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.
PowerSet & | operator= (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`.