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 . |
This class offers a generic implementation of powerset constraint systems as defined in [Bag98].
|
A powerset is implemented as a sequence of elements. The particular sequence employed must support efficient deletion in any position and efficient back insertion. |
|
Adds to
If |