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

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

#include <Powerset.defs.hh>

Inheritance diagram for Parma_Polyhedra_Library::Powerset< D >:

Inheritance graph
[legend]

List of all members.

Public Types

typedef Sequence::size_type size_type
typedef Sequence::value_type value_type
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.

Private Member Functions

bool check_omega_reduced () const
 Does the hard work of checking whether *this contains non-maximal elements and returns true if and only if it does not.
void collapse (Sequence_iterator sink)
 Replaces the disjunct *sink by an upper bound of itself and all the disjuncts following it.

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.

Classes

class  omega_const_iterator
 A const_iterator on the disjuncts of a Powerset element. More...
class  omega_iterator
 An iterator on the disjuncts of a Powerset element. More...


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.

Definition at line 144 of file Powerset.defs.hh.


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.

Reimplemented in Parma_Polyhedra_Library::Polyhedra_Powerset< PH >.

Definition at line 218 of file Powerset.defs.hh.

template<typename D>
typedef Sequence::iterator Parma_Polyhedra_Library::Powerset< D >::Sequence_iterator [protected]

Alias for the low-level iterator on the disjuncts.

Reimplemented in Parma_Polyhedra_Library::Polyhedra_Powerset< PH >.

Definition at line 221 of file Powerset.defs.hh.

template<typename D>
typedef Sequence::const_iterator Parma_Polyhedra_Library::Powerset< D >::Sequence_const_iterator [protected]

Alias for the low-level const_iterator on the disjuncts.

Reimplemented in Parma_Polyhedra_Library::Polyhedra_Powerset< PH >.

Definition at line 224 of file Powerset.defs.hh.

template<typename D>
typedef Sequence::size_type Parma_Polyhedra_Library::Powerset< D >::size_type

Reimplemented in Parma_Polyhedra_Library::Polyhedra_Powerset< PH >.

Definition at line 234 of file Powerset.defs.hh.

template<typename D>
typedef Sequence::value_type Parma_Polyhedra_Library::Powerset< D >::value_type

Reimplemented in Parma_Polyhedra_Library::Polyhedra_Powerset< PH >.

Definition at line 235 of file Powerset.defs.hh.

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.

Reimplemented in Parma_Polyhedra_Library::Polyhedra_Powerset< PH >.

Definition at line 238 of file Powerset.defs.hh.

A bidirectional const_iterator on the disjuncts of a Powerset element.

Reimplemented in Parma_Polyhedra_Library::Polyhedra_Powerset< PH >.

Definition at line 252 of file Powerset.defs.hh.

template<typename D>
typedef std::reverse_iterator<iterator> Parma_Polyhedra_Library::Powerset< D >::reverse_iterator

The reverse iterator type built from Powerset::iterator.

Reimplemented in Parma_Polyhedra_Library::Polyhedra_Powerset< PH >.

Definition at line 255 of file Powerset.defs.hh.

template<typename D>
typedef std::reverse_iterator<const_iterator> Parma_Polyhedra_Library::Powerset< D >::const_reverse_iterator

The reverse iterator type built from Powerset::const_iterator.

Reimplemented in Parma_Polyhedra_Library::Polyhedra_Powerset< PH >.

Definition at line 257 of file Powerset.defs.hh.


Constructor & Destructor Documentation

template<typename D>
Parma_Polyhedra_Library::Powerset< D >::Powerset (  )  [inline]

Default constructor: builds the bottom of the powerset constraint system (i.e., the empty powerset).

Definition at line 302 of file Powerset.inlines.hh.

00303   : sequence(), reduced(true) {
00304 }

template<typename D>
Parma_Polyhedra_Library::Powerset< D >::Powerset ( const Powerset< D > &  y  )  [inline]

Copy constructor.

Definition at line 281 of file Powerset.inlines.hh.

00282   : sequence(y.sequence), reduced(y.reduced) {
00283 }

template<typename D>
Parma_Polyhedra_Library::Powerset< D >::Powerset ( const D &  d  )  [inline, explicit]

If d is not bottom, builds a powerset containing only d. Builds the empty powerset otherwise.

Definition at line 308 of file Powerset.inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::OK(), and Parma_Polyhedra_Library::Powerset< D >::sequence.

00309   : sequence(), reduced(true) {
00310   if (!d.is_bottom())
00311     sequence.push_back(d);
00312   assert(OK());
00313 }

template<typename D>
Parma_Polyhedra_Library::Powerset< D >::~Powerset (  )  [inline]

Destructor.

Definition at line 317 of file Powerset.inlines.hh.

00317                        {
00318 }


Member Function Documentation

template<typename D>
bool Parma_Polyhedra_Library::Powerset< D >::definitely_entails ( const Powerset< D > &  y  )  const [inline]

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

Definition at line 170 of file Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::begin(), and Parma_Polyhedra_Library::Powerset< D >::end().

00170                                                        {
00171   const Powerset<D>& x = *this;
00172   bool found = true;
00173   for (const_iterator xi = x.begin(),
00174          x_end = x.end(); found && xi != x_end; ++xi) {
00175     found = false;
00176     for (const_iterator yi = y.begin(),
00177            y_end = y.end(); !found && yi != y_end; ++yi)
00178       found = (*xi).definitely_entails(*yi);
00179   }
00180   return found;
00181 }

template<typename D>
bool Parma_Polyhedra_Library::Powerset< D >::is_top (  )  const [inline]

Returns true if and only if *this is the top element of the powerset constraint system (i.e., it represents the universe).

Definition at line 343 of file Powerset.inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::end(), and Parma_Polyhedra_Library::Powerset< D >::omega_reduce().

00343                           {
00344   // Must perform omega-reduction for correctness.
00345   omega_reduce();
00346   const_iterator xi = begin();
00347   const_iterator x_end = end();
00348   return xi != x_end && xi->is_top() && ++xi == x_end;
00349 }

template<typename D>
bool Parma_Polyhedra_Library::Powerset< D >::is_bottom (  )  const [inline]

Returns true if and only if *this is the bottom element of the powerset constraint system (i.e., it represents the empty set).

Definition at line 353 of file Powerset.inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::empty(), and Parma_Polyhedra_Library::Powerset< D >::omega_reduce().

Referenced by Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::map_space_dimensions().

00353                              {
00354   // Must perform omega-reduction for correctness.
00355   omega_reduce();
00356   return empty();
00357 }

template<typename D>
memory_size_type Parma_Polyhedra_Library::Powerset< D >::total_memory_in_bytes (  )  const [inline]

Returns a lower bound to the total size in bytes of the memory occupied by *this.

Reimplemented in Parma_Polyhedra_Library::Polyhedra_Powerset< PH >.

Definition at line 380 of file Powerset.inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::external_memory_in_bytes().

00380                                          {
00381   return sizeof(*this) + external_memory_in_bytes();
00382 }

template<typename D>
memory_size_type Parma_Polyhedra_Library::Powerset< D >::external_memory_in_bytes (  )  const [inline]

Returns a lower bound to the size in bytes of the memory managed by *this.

Reimplemented in Parma_Polyhedra_Library::Polyhedra_Powerset< PH >.

Definition at line 264 of file Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::begin(), and Parma_Polyhedra_Library::Powerset< D >::end().

Referenced by Parma_Polyhedra_Library::Powerset< D >::total_memory_in_bytes().

00264                                             {
00265   memory_size_type bytes = 0;
00266   for (const_iterator xi = begin(), x_end = end(); xi != x_end; ++xi) {
00267     bytes += xi->total_memory_in_bytes();
00268     // We assume there is at least a forward and a backward link, and
00269     // that the pointers implementing them are at least the size of
00270     // pointers to `D'.
00271     bytes += 2*sizeof(D*);
00272   }
00273   return bytes;
00274 }

template<typename D>
bool Parma_Polyhedra_Library::Powerset< D >::OK ( bool  disallow_bottom = false  )  const [inline]

Checks if all the invariants are satisfied.

Definition at line 278 of file Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::check_omega_reduced(), Parma_Polyhedra_Library::Powerset< D >::end(), and Parma_Polyhedra_Library::Powerset< D >::reduced.

Referenced by Parma_Polyhedra_Library::Powerset< D >::collapse(), Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), and Parma_Polyhedra_Library::Powerset< D >::Powerset().

00278                                                 {
00279   for (const_iterator xi = begin(), x_end = end(); xi != x_end; ++xi) {
00280     if (!xi->OK())
00281       return false;
00282     if (disallow_bottom && xi->is_bottom()) {
00283 #ifndef NDEBUG
00284       std::cerr << "Bottom element in powerset!"
00285                 << std::endl;
00286 #endif
00287       return false;
00288     }
00289   }
00290   if (reduced && !check_omega_reduced()) {
00291 #ifndef NDEBUG
00292     std::cerr << "Powerset claims to be reduced, but it is not!"
00293               << std::endl;
00294 #endif
00295     return false;
00296   }
00297   return true;
00298 }

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.

Definition at line 58 of file Powerset.templates.hh.

References Parma_Polyhedra_Library::abandon_expensive_computations, Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::collapse(), Parma_Polyhedra_Library::Powerset< D >::drop_disjunct(), Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Powerset< D >::OK(), and Parma_Polyhedra_Library::Powerset< D >::reduced.

Referenced by Parma_Polyhedra_Library::Powerset< D >::collapse(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::concatenate_assign(), Parma_Polyhedra_Library::Powerset< D >::is_bottom(), Parma_Polyhedra_Library::Powerset< D >::is_top(), Parma_Polyhedra_Library::Powerset< D >::least_upper_bound_assign(), Parma_Polyhedra_Library::Powerset< D >::operator==(), Parma_Polyhedra_Library::Powerset< D >::pairwise_apply_assign(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::pairwise_reduce(), and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::poly_difference_assign().

00058                                 {
00059   if (reduced)
00060     return;
00061 
00062   Powerset& x = const_cast<Powerset&>(*this);
00063   // First remove all bottom elements.
00064   for (iterator xi = x.begin(), x_end = x.end(); xi != x_end; )
00065     if (xi->is_bottom())
00066       xi = x.drop_disjunct(xi);
00067     else
00068       ++xi;
00069   // Then remove non-maximal elements.
00070   for (iterator xi = x.begin(); xi != x.end(); ) {
00071     const D& xv = *xi;
00072     bool dropping_xi = false;
00073     for (iterator yi = x.begin(); yi != x.end(); )
00074       if (xi == yi)
00075         ++yi;
00076       else {
00077         const D& yv = *yi;
00078         if (yv.definitely_entails(xv))
00079           yi = x.drop_disjunct(yi);
00080         else if (xv.definitely_entails(yv)) {
00081           dropping_xi = true;
00082           break;
00083         }
00084         else
00085           ++yi;
00086       }
00087     if (dropping_xi)
00088       xi = x.drop_disjunct(xi);
00089     else
00090       ++xi;
00091     if (abandon_expensive_computations && xi != x.end()) {
00092       // Hurry up!
00093       x.collapse(xi.base);
00094       break;
00095     }
00096   }
00097   reduced = true;
00098   assert(OK());
00099 }

template<typename D>
Powerset< D >::size_type Parma_Polyhedra_Library::Powerset< D >::size (  )  const [inline]

template<typename D>
bool Parma_Polyhedra_Library::Powerset< D >::empty (  )  const [inline]

template<typename D>
Powerset< D >::iterator Parma_Polyhedra_Library::Powerset< D >::begin (  )  [inline]

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

Definition at line 203 of file Powerset.inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::sequence.

Referenced by Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::ascii_dump(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::BGP99_heuristics_assign(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::BHZ03_widening_assign(), Parma_Polyhedra_Library::Powerset< D >::check_omega_reduced(), Parma_Polyhedra_Library::Powerset< D >::collapse(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::collect_certificates(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::concatenate_assign(), Parma_Polyhedra_Library::Powerset< D >::definitely_entails(), Parma_Polyhedra_Library::Powerset< D >::external_memory_in_bytes(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::geometrically_covers(), Parma_Polyhedra_Library::Powerset< D >::is_top(), Parma_Polyhedra_Library::Powerset< D >::least_upper_bound_assign(), Parma_Polyhedra_Library::Powerset< D >::OK(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::OK(), Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), Parma_Polyhedra_Library::Powerset< D >::operator==(), Parma_Polyhedra_Library::Powerset< D >::pairwise_apply_assign(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::pairwise_reduce(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::poly_difference_assign(), and Parma_Polyhedra_Library::Powerset< D >::rend().

00203                    {
00204   return sequence.begin();
00205 }

template<typename D>
Powerset< D >::iterator Parma_Polyhedra_Library::Powerset< D >::end (  )  [inline]

Returns the past-the-end iterator.

Definition at line 209 of file Powerset.inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::sequence.

Referenced by Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::ascii_dump(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::BGP99_heuristics_assign(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::BHZ03_widening_assign(), Parma_Polyhedra_Library::Powerset< D >::check_omega_reduced(), Parma_Polyhedra_Library::Powerset< D >::collapse(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::collect_certificates(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::concatenate_assign(), Parma_Polyhedra_Library::Powerset< D >::definitely_entails(), Parma_Polyhedra_Library::Powerset< D >::external_memory_in_bytes(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::geometrically_covers(), Parma_Polyhedra_Library::Powerset< D >::is_top(), Parma_Polyhedra_Library::Powerset< D >::least_upper_bound_assign(), Parma_Polyhedra_Library::Powerset< D >::OK(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::OK(), Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), Parma_Polyhedra_Library::Powerset< D >::operator==(), Parma_Polyhedra_Library::Powerset< D >::pairwise_apply_assign(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::pairwise_reduce(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::poly_difference_assign(), and Parma_Polyhedra_Library::Powerset< D >::rbegin().

00209                  {
00210   return sequence.end();
00211 }

template<typename D>
Powerset< D >::const_iterator Parma_Polyhedra_Library::Powerset< D >::begin (  )  const [inline]

Returns a const_iterator pointing to the first disjunct, if *this is not empty; otherwise, returns the past-the-end const_iterator.

Definition at line 215 of file Powerset.inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::sequence.

00215                          {
00216   return sequence.begin();
00217 }

template<typename D>
Powerset< D >::const_iterator Parma_Polyhedra_Library::Powerset< D >::end (  )  const [inline]

Returns the past-the-end const_iterator.

Definition at line 221 of file Powerset.inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::sequence.

00221                        {
00222   return sequence.end();
00223 }

template<typename D>
Powerset< D >::reverse_iterator Parma_Polyhedra_Library::Powerset< D >::rbegin (  )  [inline]

Returns a reverse_iterator pointing to the last disjunct, if *this is not empty; otherwise, returns the before-the-start reverse_iterator.

Definition at line 227 of file Powerset.inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::end().

00227                     {
00228   return reverse_iterator(end());
00229 }

template<typename D>
Powerset< D >::reverse_iterator Parma_Polyhedra_Library::Powerset< D >::rend (  )  [inline]

Returns the before-the-start reverse_iterator.

Definition at line 233 of file Powerset.inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::begin().

00233                   {
00234   return reverse_iterator(begin());
00235 }

template<typename D>
Powerset< D >::const_reverse_iterator Parma_Polyhedra_Library::Powerset< D >::rbegin (  )  const [inline]

Returns a const_reverse_iterator pointing to the last disjunct, if *this is not empty; otherwise, returns the before-the-start const_reverse_iterator.

Definition at line 239 of file Powerset.inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::end().

00239                           {
00240   return const_reverse_iterator(end());
00241 }

template<typename D>
Powerset< D >::const_reverse_iterator Parma_Polyhedra_Library::Powerset< D >::rend (  )  const [inline]

Returns the before-the-start const_reverse_iterator.

Definition at line 245 of file Powerset.inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::begin().

00245                         {
00246   return const_reverse_iterator(begin());
00247 }

template<typename D>
void Parma_Polyhedra_Library::Powerset< D >::add_disjunct ( const D &  d  )  [inline]

Adds to *this the disjunct d.

Definition at line 329 of file Powerset.inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct().

00329                                     {
00330   if (!d.is_bottom())
00331     add_non_bottom_disjunct(d);
00332 }

template<typename D>
Powerset< D >::iterator Parma_Polyhedra_Library::Powerset< D >::drop_disjunct ( iterator  position  )  [inline]

template<typename D>
void Parma_Polyhedra_Library::Powerset< D >::drop_disjuncts ( iterator  first,
iterator  last 
) [inline]

Drops all the disjuncts from first to last (excluded).

Definition at line 269 of file Powerset.inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::omega_iterator::base, and Parma_Polyhedra_Library::Powerset< D >::sequence.

Referenced by Parma_Polyhedra_Library::Powerset< D >::collapse().

00269                                                          {
00270   sequence.erase(first.base, last.base);
00271 }

template<typename D>
void Parma_Polyhedra_Library::Powerset< D >::clear (  )  [inline]

Drops all the disjuncts, making *this an empty powerset.

Definition at line 275 of file Powerset.inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::sequence.

00275                    {
00276   sequence.clear();
00277 }

template<typename D>
Powerset< D > & Parma_Polyhedra_Library::Powerset< D >::operator= ( const Powerset< D > &  y  )  [inline]

The assignment operator.

Definition at line 287 of file Powerset.inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00287                                         {
00288   sequence = y.sequence;
00289   reduced = y.reduced;
00290   return *this;
00291 }

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

Swaps *this with y.

Definition at line 295 of file Powerset.inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

Referenced by Parma_Polyhedra_Library::Powerset< D >::swap().

00295                              {
00296   std::swap(sequence, y.sequence);
00297   std::swap(reduced, y.reduced);
00298 }

template<typename D>
void Parma_Polyhedra_Library::Powerset< D >::least_upper_bound_assign ( const Powerset< D > &  y  )  [inline]

Assigns to *this the least upper bound of *this and y.

Definition at line 230 of file Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct(), Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::end(), and Parma_Polyhedra_Library::Powerset< D >::omega_reduce().

Referenced by Parma_Polyhedra_Library::Powerset< D >::upper_bound_assign().

00230                                                        {
00231   // Ensure omega-reduction here, since what follows has quadratic complexity.
00232   omega_reduce();
00233   y.omega_reduce();
00234   iterator old_begin = begin();
00235   iterator old_end = end();
00236   for (const_iterator i = y.begin(), y_end = y.end(); i != y_end; ++i)
00237     old_begin = add_non_bottom_disjunct(*i, old_begin, old_end);
00238 }

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.

Definition at line 374 of file Powerset.inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::least_upper_bound_assign().

00374                                                  {
00375   least_upper_bound_assign(y);
00376 }

template<typename D>
void Parma_Polyhedra_Library::Powerset< D >::meet_assign ( const Powerset< D > &  y  )  [inline]

Assigns to *this the meet of *this and y.

Definition at line 368 of file Powerset.inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::pairwise_apply_assign().

00368                                           {
00369   pairwise_apply_assign(y, std::mem_fun_ref(&D::meet_assign));
00370 }

template<typename D>
void Parma_Polyhedra_Library::Powerset< D >::collapse (  )  [inline]

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.

Definition at line 361 of file Powerset.inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::empty(), and Parma_Polyhedra_Library::Powerset< D >::sequence.

Referenced by Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::BGP99_extrapolation_assign(), Parma_Polyhedra_Library::Powerset< D >::collapse(), and Parma_Polyhedra_Library::Powerset< D >::omega_reduce().

00361                       {
00362   if (!empty())
00363     collapse(sequence.begin());
00364 }

template<typename D>
bool Parma_Polyhedra_Library::Powerset< D >::is_omega_reduced (  )  const [inline, protected]

template<typename D>
void Parma_Polyhedra_Library::Powerset< D >::collapse ( unsigned  max_disjuncts  )  [inline, protected]

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.

Definition at line 103 of file Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::omega_iterator::base, Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::collapse(), Parma_Polyhedra_Library::Powerset< D >::is_omega_reduced(), Parma_Polyhedra_Library::Powerset< D >::OK(), Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), and Parma_Polyhedra_Library::Powerset< D >::size().

00103                                                   {
00104   assert(max_disjuncts > 0);
00105   // Omega-reduce before counting the number of disjuncts.
00106   omega_reduce();
00107   size_type n = size();
00108   if (n > max_disjuncts) {
00109     // Let `i' point to the last disjunct that will survive.
00110     iterator i = begin();
00111     std::advance(i, max_disjuncts-1);
00112     // This disjunct will be assigned an upper-bound of itself and of
00113     // all the disjuncts that follow.
00114     collapse(i.base);
00115   }
00116   assert(OK());
00117   assert(is_omega_reduced());
00118 }

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.

Definition at line 149 of file Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::drop_disjunct(), and Parma_Polyhedra_Library::Powerset< D >::sequence.

Referenced by Parma_Polyhedra_Library::Powerset< D >::add_disjunct(), Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::BGP99_heuristics_assign(), Parma_Polyhedra_Library::Powerset< D >::least_upper_bound_assign(), and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::pairwise_reduce().

00151                                                      {
00152   for (iterator xi = first; xi != last; ) {
00153     const D& xv = *xi;
00154     if (d.definitely_entails(xv))
00155       return first;
00156     else if (xv.definitely_entails(d)) {
00157       if (xi == first)
00158         ++first;
00159       xi = drop_disjunct(xi);
00160     }
00161     else
00162       ++xi;
00163   }
00164   sequence.push_back(d);
00165   return first;
00166 }

template<typename D>
void Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct ( const D &  d  )  [inline, protected]

Adds to *this the disjunct d, assuming d is not the bottom element.

Definition at line 322 of file Powerset.inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct(), Parma_Polyhedra_Library::Powerset< D >::begin(), and Parma_Polyhedra_Library::Powerset< D >::end().

00322                                                {
00323   assert(!d.is_bottom());
00324   add_non_bottom_disjunct(d, begin(), end());
00325 }

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.

Definition at line 209 of file Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

Referenced by Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::intersection_assign(), Parma_Polyhedra_Library::Powerset< D >::meet_assign(), and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::time_elapse_assign().

00210                                                                       {
00211   // Ensure omega-reduction here, since what follows has quadratic complexity.
00212   omega_reduce();
00213   y.omega_reduce();
00214   Sequence new_sequence;
00215   for (const_iterator xi = begin(), x_end = end(),
00216          y_begin = y.begin(), y_end = y.end(); xi != x_end; ++xi)
00217     for (const_iterator yi = y_begin; yi != y_end; ++yi) {
00218       D zi = *xi;
00219       op_assign(zi, *yi);
00220       if (!zi.is_bottom())
00221         new_sequence.push_back(zi);
00222     }
00223   // Put the new sequence in place.
00224   std::swap(sequence, new_sequence);
00225   reduced = false;
00226 }

template<typename D>
bool Parma_Polyhedra_Library::Powerset< D >::check_omega_reduced (  )  const [inline, private]

Does the hard work of checking whether *this contains non-maximal elements and returns true if and only if it does not.

Definition at line 122 of file Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::begin(), and Parma_Polyhedra_Library::Powerset< D >::end().

Referenced by Parma_Polyhedra_Library::Powerset< D >::is_omega_reduced(), and Parma_Polyhedra_Library::Powerset< D >::OK().

00122                                        {
00123   for (const_iterator x_begin = begin(), x_end = end(),
00124          xi = x_begin; xi != x_end; ++xi) {
00125     const D& xv = *xi;
00126     if (xv.is_bottom())
00127       return false;
00128     for (const_iterator yi = x_begin; yi != x_end; ++yi) {
00129       if (xi == yi)
00130         continue;
00131       const D& yv = *yi;
00132       if (xv.definitely_entails(yv) || yv.definitely_entails(xv))
00133         return false;
00134     }
00135   }
00136   return true;
00137 }

template<typename D>
void Parma_Polyhedra_Library::Powerset< D >::collapse ( Sequence_iterator  sink  )  [inline, private]

Replaces the disjunct *sink by an upper bound of itself and all the disjuncts following it.

Definition at line 34 of file Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::drop_disjunct(), Parma_Polyhedra_Library::Powerset< D >::drop_disjuncts(), Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Powerset< D >::OK(), and Parma_Polyhedra_Library::Powerset< D >::sequence.

00034                                                   {
00035   assert(sink != sequence.end());
00036   D& d = *sink;
00037   iterator x_sink = sink;
00038   iterator next_x_sink = x_sink;
00039   ++next_x_sink;
00040   iterator x_end = end();
00041   for (const_iterator xi = next_x_sink; xi != x_end; ++xi)
00042     d.upper_bound_assign(*xi);
00043   // Drop the surplus disjuncts.
00044   drop_disjuncts(next_x_sink, x_end);
00045 
00046   // Ensure omega-reduction.
00047   for (iterator xi = begin(); xi != x_sink; )
00048     if (xi->definitely_entails(d))
00049       xi = drop_disjunct(xi);
00050     else
00051       ++xi;
00052 
00053   assert(OK());
00054 }


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.

Definition at line 186 of file Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::drop_disjunct(), Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), and Parma_Polyhedra_Library::Powerset< D >::size().

00186                                                        {
00187   x.omega_reduce();
00188   y.omega_reduce();
00189   if (x.size() != y.size())
00190     return false;
00191   // Take a copy of `y' and work with it.
00192   Powerset<D> yy = y;
00193   for (typename Powerset<D>::const_iterator xi = x.begin(),
00194          x_end = x.end(); xi != x_end; ++xi) {
00195     typename Powerset<D>::iterator yyi = yy.begin();
00196     typename Powerset<D>::iterator yy_end = yy.end();
00197     yyi = std::find(yyi, yy_end, *xi);
00198     if (yyi == yy_end)
00199       return false;
00200     else
00201       yy.drop_disjunct(yyi);
00202   }
00203   return true;
00204 }

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.

Definition at line 337 of file Powerset.inlines.hh.

00337                                                             {
00338   return !(x == y);
00339 }

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

Output operator.

Definition at line 245 of file Powerset.templates.hh.

00245                                                 {
00246   if (x.is_bottom())
00247     s << "false";
00248   else if (x.is_top())
00249     s << "true";
00250   else
00251     for (typename Powerset<D>::const_iterator i = x.begin(),
00252            x_end = x.end(); i != x_end; ) {
00253       s << "{ " << *i++ << " }";
00254       if (i != x_end)
00255         s << ", ";
00256     }
00257   return s;
00258 }

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

Specializes std::swap.

Definition at line 392 of file Powerset.inlines.hh.

References Parma_Polyhedra_Library::Powerset< D >::swap().

00393                                             {
00394   x.swap(y);
00395 }


Member Data Documentation

template<typename D>
Sequence Parma_Polyhedra_Library::Powerset< D >::sequence [protected]

The sequence container holding powerset's elements.

Definition at line 227 of file Powerset.defs.hh.

Referenced by Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::add_constraint(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::add_constraint_and_minimize(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::add_constraints(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::add_constraints_and_minimize(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::add_disjunct(), Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::add_space_dimensions_and_embed(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::add_space_dimensions_and_project(), Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::BGP99_heuristics_assign(), Parma_Polyhedra_Library::Powerset< D >::clear(), Parma_Polyhedra_Library::Powerset< D >::collapse(), Parma_Polyhedra_Library::Powerset< D >::drop_disjunct(), Parma_Polyhedra_Library::Powerset< D >::drop_disjuncts(), Parma_Polyhedra_Library::Powerset< D >::empty(), Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::map_space_dimensions(), Parma_Polyhedra_Library::Powerset< D >::operator=(), Parma_Polyhedra_Library::Powerset< D >::pairwise_apply_assign(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::pairwise_reduce(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::poly_difference_assign(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::Polyhedra_Powerset(), Parma_Polyhedra_Library::Powerset< D >::Powerset(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::remove_higher_space_dimensions(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::remove_space_dimensions(), Parma_Polyhedra_Library::Powerset< D >::size(), and Parma_Polyhedra_Library::Powerset< D >::swap().

template<typename D>
bool Parma_Polyhedra_Library::Powerset< D >::reduced [mutable, protected]


The documentation for this class was generated from the following files:

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