Parma_Polyhedra_Library::Polyhedra_Powerset< PH > Class Template Reference
[C++ Language Interface]

The powerset construction instantiated on PPL polyhedra. More...

#include <Polyhedra_Powerset.defs.hh>

Inheritance diagram for Parma_Polyhedra_Library::Polyhedra_Powerset< PH >:

Inheritance graph
[legend]
Collaboration diagram for Parma_Polyhedra_Library::Polyhedra_Powerset< PH >:

Collaboration graph
[legend]

List of all members.

Public Types

typedef PH element_type
typedef Base::size_type size_type
typedef Base::value_type value_type
typedef Base::iterator iterator
 Alias for a read-only bidirectional iterator on the disjuncts of a Powerset element.
typedef Base::const_iterator const_iterator
 A bidirectional const_iterator on the disjuncts of a Powerset element.
typedef Base::reverse_iterator reverse_iterator
 The reverse iterator type built from Powerset::iterator.
typedef
Base::const_reverse_iterator 
const_reverse_iterator
 The reverse iterator type built from Powerset::const_iterator.

Public Member Functions

void ascii_dump () const
 Writes to std::cerr an ASCII representation of *this.
void ascii_dump (std::ostream &s) const
 Writes to s an ASCII representation of *this.
void print () const
 Prints *this to std::cerr using operator<<.
bool ascii_load (std::istream &s)
 Loads from s an ASCII representation (as produced by ascii_dump) and sets *this accordingly. Returns true if successful, false otherwise.
template<>
 Polyhedra_Powerset (const Polyhedra_Powerset< QH > &y)
template<>
 Polyhedra_Powerset (const Polyhedra_Powerset< QH > &y)
template<>
 Polyhedra_Powerset (const Polyhedra_Powerset< C_Polyhedron > &y)
template<>
 Polyhedra_Powerset (const Polyhedra_Powerset< NNC_Polyhedron > &y)
template<>
void poly_difference_assign (const Polyhedra_Powerset &y)
template<>
bool geometrically_covers (const Polyhedra_Powerset &y) const
template<>
 Polyhedra_Powerset (const Polyhedra_Powerset< C_Polyhedron > &y)
template<>
 Polyhedra_Powerset (const Polyhedra_Powerset< NNC_Polyhedron > &y)
template<>
bool geometrically_equals (const Polyhedra_Powerset &y) const
template<>
void poly_difference_assign (const Polyhedra_Powerset &y)
template<>
 Polyhedra_Powerset (const Polyhedra_Powerset< QH > &y)
template<>
 Polyhedra_Powerset (const Polyhedra_Powerset< QH > &y)
template<>
void poly_difference_assign (const Polyhedra_Powerset &y)
template<>
bool geometrically_covers (const Polyhedra_Powerset &y) const
Constructors
 Polyhedra_Powerset (dimension_type num_dimensions=0, Degenerate_Element kind=UNIVERSE)
 Builds a universe (top) or empty (bottom) Polyhedra_Powerset.
 Polyhedra_Powerset (const Polyhedra_Powerset &y)
 Ordinary copy-constructor.
 Polyhedra_Powerset (const PH &ph)
 If ph is nonempty, builds a powerset containing only ph. Builds the empty powerset otherwise.
template<typename QH>
 Polyhedra_Powerset (const Polyhedra_Powerset< QH > &y)
 Copy-constructor allowing a source powerset with elements of a different polyhedron kind.
 Polyhedra_Powerset (const Constraint_System &cs)
 Creates a Polyhedra_Powerset with a single polyhedron with the same information contents as cs.
 Polyhedra_Powerset (const Congruence_System &cgs)
Member Functions that Do Not Modify the Powerset of Polyhedra
dimension_type space_dimension () const
 Returns the dimension of the vector space enclosing *this.
bool geometrically_covers (const Polyhedra_Powerset &y) const
 Returns true if and only if *this geometrically covers y, i.e., if any point (in some element) of y is also a point (of some element) of *this.
bool geometrically_equals (const Polyhedra_Powerset &y) const
 Returns true if and only if *this is geometrically equal to y, i.e., if (the elements of) *this and y contain the same set of points.
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 () const
 Checks if all the invariants are satisfied.
Space Dimension Preserving Member Functions that May Modify the Powerset of Polyhedra
void add_disjunct (const PH &ph)
 Adds to *this the disjunct ph.
void add_constraint (const Constraint &c)
 Intersects *this with constraint c.
bool add_constraint_and_minimize (const Constraint &c)
 Intersects *this with the constraint c, minimizing the result.
void add_constraints (const Constraint_System &cs)
 Intersects *this with the constraints in cs.
bool add_constraints_and_minimize (const Constraint_System &cs)
 Intersects *this with the constraints in cs, minimizing the result.
void pairwise_reduce ()
 Assign to *this the result of (recursively) merging together the pairs of polyhedra whose poly-hull is the same as their set-theoretical union.
template<typename Widening>
void BGP99_extrapolation_assign (const Polyhedra_Powerset &y, Widening wf, unsigned max_disjuncts)
 Assigns to *this the result of applying the BGP99 extrapolation operator to *this and y, using the widening function wf and the cardinality threshold max_disjuncts.
template<typename Cert, typename Widening>
void BHZ03_widening_assign (const Polyhedra_Powerset &y, Widening wf)
 Assigns to *this the result of computing the BHZ03-widening between *this and y, using the widening function wf certified by the convergence certificate Cert.
Member Functions that May Modify the Dimension of the Vector Space
Polyhedra_Powersetoperator= (const Polyhedra_Powerset &y)
 The assignment operator (*this and y can be dimension-incompatible).
template<typename QH>
Polyhedra_Powersetoperator= (const Polyhedra_Powerset< QH > &y)
 Assignment operator allowing a source powerset with elements of a different polyhedron kind (*this and y can be dimension-incompatible).
void swap (Polyhedra_Powerset &y)
 Swaps *this with y.
void add_space_dimensions_and_embed (dimension_type m)
 Adds m new dimensions to the vector space containing *this and embeds each polyhedron in *this in the new space.
void add_space_dimensions_and_project (dimension_type m)
 Adds m new dimensions to the vector space containing *this without embedding the polyhedra in *this in the new space.
void intersection_assign (const Polyhedra_Powerset &y)
 Assigns to *this the intersection of *this and y.
void poly_difference_assign (const Polyhedra_Powerset &y)
 Assigns to *this the difference of *this and y.
void concatenate_assign (const Polyhedra_Powerset &y)
 Assigns to *this the concatenation of *this and y.
void time_elapse_assign (const Polyhedra_Powerset &y)
 Assigns to *this the result of computing the time-elapse between *this and y.
void remove_space_dimensions (const Variables_Set &to_be_removed)
 Removes all the specified space dimensions.
void remove_higher_space_dimensions (dimension_type new_dimension)
 Removes the higher space dimensions so that the resulting space will have dimension new_dimension.
template<typename Partial_Function>
void map_space_dimensions (const Partial_Function &pfunc)
 Remaps the dimensions of the vector space according to a partial function.

Static Public Member Functions

static dimension_type max_space_dimension ()
 Returns the maximum space dimension a Polyhedra_Powerset<PH> can handle.

Private Types

typedef Determinate< PH > CS
typedef Powerset< CSBase
typedef Base::Sequence Sequence
 A powerset is implemented as a sequence of elements.
typedef Base::Sequence_iterator Sequence_iterator
 Alias for the low-level iterator on the disjuncts.
typedef
Base::Sequence_const_iterator 
Sequence_const_iterator
 Alias for the low-level const_iterator on the disjuncts.

Private Member Functions

template<typename Widening>
void BGP99_heuristics_assign (const Polyhedra_Powerset &y, Widening wf)
 Assigns to *this the result of applying the BGP99 heuristics to *this and y, using the widening function wf.
template<typename Cert>
void collect_certificates (std::map< Cert, size_type, typename Cert::Compare > &cert_ms) const
 Records in cert_ms the certificates for this set of polyhedra.
template<typename Cert>
bool is_cert_multiset_stabilizing (const std::map< Cert, size_type, typename Cert::Compare > &y_cert_ms) const
 Returns true if and only if the current set of polyhedra is stabilizing with respect to the multiset of certificates y_cert_ms.

Private Attributes

dimension_type space_dim
 The number of dimensions of the enclosing vector space.

Friends

class Polyhedra_Powerset

Related Functions

(Note that these are not member functions.)

template<typename PH>
Widening_Function< PH > widen_fun_ref (void(PH::*wm)(const PH &, unsigned *))
 Wraps a widening method into a function object.
template<typename PH, typename CS>
Limited_Widening_Function< PH, CSwiden_fun_ref (void(PH::*lwm)(const PH &, const CS &, unsigned *), const CS &cs)
 Wraps a limited widening method into a function object.
template<typename PH>
std::pair< PH,
Polyhedra_Powerset
< NNC_Polyhedron > > 
linear_partition (const PH &p, const PH &q)
 Partitions q with respect to p.
bool check_containment (const NNC_Polyhedron &ph, const Polyhedra_Powerset< NNC_Polyhedron > &ps)
 Returns true if and only if the union of the NNC polyhedra in ps contains the NNC polyhedron ph.
template<typename PH>
bool check_containment (const PH &ph, const Polyhedra_Powerset< PH > &ps)
 Returns true if and only if the union of the objects in ps contains ph.
template<typename PH>
void swap (Parma_Polyhedra_Library::Polyhedra_Powerset< PH > &x, Parma_Polyhedra_Library::Polyhedra_Powerset< PH > &y)
 Specializes std::swap.
template<>
bool check_containment (const C_Polyhedron &ph, const Polyhedra_Powerset< C_Polyhedron > &ps)
template<typename PH>
void linear_partition_aux (const Constraint &c, PH &qq, Polyhedra_Powerset< NNC_Polyhedron > &r)
 Partitions polyhedron qq according to constraint c.


Detailed Description

template<typename PH>
class Parma_Polyhedra_Library::Polyhedra_Powerset< PH >

The powerset construction instantiated on PPL polyhedra.

Definition at line 46 of file Polyhedra_Powerset.defs.hh.


Member Typedef Documentation

template<typename PH>
typedef PH Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::element_type

Definition at line 50 of file Polyhedra_Powerset.defs.hh.

template<typename PH>
typedef Determinate<PH> Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::CS [private]

Definition at line 53 of file Polyhedra_Powerset.defs.hh.

template<typename PH>
typedef Powerset<CS> Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::Base [private]

Definition at line 54 of file Polyhedra_Powerset.defs.hh.

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 from Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >.

Definition at line 390 of file Polyhedra_Powerset.defs.hh.

A bidirectional const_iterator on the disjuncts of a Powerset element.

Reimplemented from Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >.

Definition at line 391 of file Polyhedra_Powerset.defs.hh.

The reverse iterator type built from Powerset::iterator.

Reimplemented from Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >.

Definition at line 392 of file Polyhedra_Powerset.defs.hh.

The reverse iterator type built from Powerset::const_iterator.

Reimplemented from Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >.

Definition at line 393 of file Polyhedra_Powerset.defs.hh.

template<typename PH>
typedef Base::Sequence Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::Sequence [private]

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 from Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >.

Definition at line 407 of file Polyhedra_Powerset.defs.hh.

Alias for the low-level iterator on the disjuncts.

Reimplemented from Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >.

Definition at line 408 of file Polyhedra_Powerset.defs.hh.

Alias for the low-level const_iterator on the disjuncts.

Reimplemented from Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >.

Definition at line 409 of file Polyhedra_Powerset.defs.hh.


Constructor & Destructor Documentation

template<typename PH>
Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::Polyhedra_Powerset ( dimension_type  num_dimensions = 0,
Degenerate_Element  kind = UNIVERSE 
) [inline, explicit]

Builds a universe (top) or empty (bottom) Polyhedra_Powerset.

Parameters:
num_dimensions The number of dimensions of the vector space enclosing the powerset;
kind Specifies whether the universe or the empty powerset has to be built.

Definition at line 53 of file Polyhedra_Powerset.inlines.hh.

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

00055   : Base(), space_dim(num_dimensions) {
00056   Polyhedra_Powerset& x = *this;
00057   if (kind == UNIVERSE)
00058     x.sequence.push_back(Determinate<PH>(PH(num_dimensions, kind)));
00059   assert(x.OK());
00060 }

template<typename PH>
Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::Polyhedra_Powerset ( const Polyhedra_Powerset< PH > &  y  )  [inline]

Ordinary copy-constructor.

Definition at line 64 of file Polyhedra_Powerset.inlines.hh.

00065   : Base(y), space_dim(y.space_dim) {
00066 }

template<typename PH>
Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::Polyhedra_Powerset ( const PH &  ph  )  [inline, explicit]

If ph is nonempty, builds a powerset containing only ph. Builds the empty powerset otherwise.

Definition at line 70 of file Polyhedra_Powerset.inlines.hh.

00071   : Base(ph), space_dim(ph.space_dimension()) {
00072 }

template<typename PH>
template<typename QH>
Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::Polyhedra_Powerset ( const Polyhedra_Powerset< QH > &  y  )  [inline, explicit]

Copy-constructor allowing a source powerset with elements of a different polyhedron kind.

template<typename PH>
Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::Polyhedra_Powerset ( const Constraint_System cs  )  [inline, explicit]

Creates a Polyhedra_Powerset with a single polyhedron with the same information contents as cs.

Definition at line 120 of file Polyhedra_Powerset.inlines.hh.

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

00121           : calling Base(Determinate<PH>(cs)) will automatically handle
00122   // the flag `reduced', but it will also force a non-emptiness test
00123   // on the constraint system `cs'.
00124   : Base(), space_dim(cs.space_dimension()) {
00125   Polyhedra_Powerset& x = *this;
00126   x.sequence.push_back(Determinate<PH>(cs));
00127   x.reduced = false;
00128   assert(x.OK());
00129 }

template<typename PH>
Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::Polyhedra_Powerset ( const Congruence_System cgs  )  [inline, explicit]

Creates a Polyhedra_Powerset with a single polyhedron with the same information contents as cgs.

Definition at line 133 of file Polyhedra_Powerset.inlines.hh.

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

00134           : calling Base(Determinate<PH>(cgs)) will automatically handle
00135   // the flag `reduced', but it will also force a non-emptiness test
00136   // on the congruence system `cgs'.
00137   : Base(), space_dim(cgs.space_dimension()) {
00138   Polyhedra_Powerset& x = *this;
00139   x.sequence.push_back(Determinate<PH>(cgs));
00140   x.reduced = false;
00141   assert(OK());
00142 }

Definition at line 82 of file Polyhedra_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >::begin(), Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >::end(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::OK(), Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >::reduced, Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00083   : Base(), space_dim(y.space_dimension()) {
00084   Polyhedra_Powerset& x = *this;
00085   for (Polyhedra_Powerset<C_Polyhedron>::const_iterator i = y.begin(),
00086          y_end = y.end(); i != y_end; ++i)
00087     x.sequence.push_back(Determinate<NNC_Polyhedron>(
00088                            NNC_Polyhedron(i->element()))
00089                          );
00090   x.reduced = y.reduced;
00091   assert(x.OK());
00092 }

Definition at line 102 of file Polyhedra_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >::begin(), Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >::end(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00103   : Base(), space_dim(y.space_dimension()) {
00104   Polyhedra_Powerset& x = *this;
00105   for (Polyhedra_Powerset<NNC_Polyhedron>::const_iterator i = y.begin(),
00106          y_end = y.end(); i != y_end; ++i)
00107     x.sequence.push_back(Determinate<C_Polyhedron>(
00108                            C_Polyhedron(i->element()))
00109                          );
00110   // Note: this might be non-reduced even when `y' is known to be
00111   // omega-reduced, because the constructor of C_Polyhedron, by
00112   // enforcing topological closure, may have made different elements
00113   // comparable.
00114   x.reduced = false;
00115   assert(x.OK());
00116 }

Definition at line 59 of file Polyhedra_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >::begin(), Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >::end(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::OK(), Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >::reduced, Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00060   : Base(), space_dim(y.space_dimension()) {
00061   Polyhedra_Powerset& x = *this;
00062   for (typename Polyhedra_Powerset<QH>::const_iterator i = y.begin(),
00063          y_end = y.end(); i != y_end; ++i)
00064     x.sequence.push_back(Determinate<NNC_Polyhedron>(
00065                            NNC_Polyhedron(i->element().constraints()))
00066                          );
00067   x.reduced = y.reduced;
00068   assert(x.OK());
00069 }

Definition at line 74 of file Polyhedra_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >::begin(), Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >::end(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00075   : Base(), space_dim(y.space_dimension()) {
00076   Polyhedra_Powerset& x = *this;
00077   for (typename Polyhedra_Powerset<QH>::const_iterator i = y.begin(),
00078          y_end = y.end(); i != y_end; ++i)
00079     x.sequence.push_back(Determinate<C_Polyhedron>(
00080                            C_Polyhedron(i->element().constraints()))
00081                          );
00082   // Note: this might be non-reduced even when `y' is known to be
00083   // omega-reduced, because the constructor of C_Polyhedron, by
00084   // enforcing topological closure, may have made different elements
00085   // comparable.
00086   x.reduced = false;
00087   assert(x.OK());
00088 }


Member Function Documentation

template<typename PH>
dimension_type Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::max_space_dimension (  )  [inline, static]

Returns the maximum space dimension a Polyhedra_Powerset<PH> can handle.

Definition at line 47 of file Polyhedra_Powerset.inlines.hh.

00047                                             {
00048   return PH::max_space_dimension();
00049 }

template<typename PH>
dimension_type Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::space_dimension (  )  const [inline]

Returns the dimension of the vector space enclosing *this.

Definition at line 41 of file Polyhedra_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::space_dim.

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

00041                                               {
00042   return space_dim;
00043 }

template<typename PH>
bool Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::geometrically_covers ( const Polyhedra_Powerset< PH > &  y  )  const [inline]

Returns true if and only if *this geometrically covers y, i.e., if any point (in some element) of y is also a point (of some element) of *this.

Exceptions:
std::invalid_argument Thrown if *this and y are topology-incompatible or dimension-incompatible.
Warning:
This may be really expensive!

Definition at line 190 of file Polyhedra_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::geometrically_covers().

Referenced by Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::geometrically_covers(), and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::geometrically_equals().

00190                                                         {
00191   const Polyhedra_Powerset<NNC_Polyhedron> xx(*this);
00192   const Polyhedra_Powerset<NNC_Polyhedron> yy(y);
00193   return xx.geometrically_covers(yy);
00194 }

template<typename PH>
bool Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::geometrically_equals ( const Polyhedra_Powerset< PH > &  y  )  const [inline]

Returns true if and only if *this is geometrically equal to y, i.e., if (the elements of) *this and y contain the same set of points.

Exceptions:
std::invalid_argument Thrown if *this and y are topology-incompatible or dimension-incompatible.
Warning:
This may be really expensive!

Definition at line 199 of file Polyhedra_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::geometrically_covers().

00199                                                         {
00200   const Polyhedra_Powerset<NNC_Polyhedron> xx(*this);
00201   const Polyhedra_Powerset<NNC_Polyhedron> yy(y);
00202   return xx.geometrically_covers(yy) && yy.geometrically_covers(xx);
00203 }

template<typename PH>
memory_size_type Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::total_memory_in_bytes (  )  const [inline]

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

Reimplemented from Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >.

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

References Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::external_memory_in_bytes().

00221                                                     {
00222   return sizeof(*this) + external_memory_in_bytes();
00223 }

template<typename PH>
memory_size_type Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::external_memory_in_bytes (  )  const [inline]

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

Reimplemented from Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >.

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

References Parma_Polyhedra_Library::Checked::external_memory_in_bytes().

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

00215                                                        {
00216   return Base::external_memory_in_bytes();
00217 }

template<typename PH>
bool Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::OK (  )  const [inline]

Checks if all the invariants are satisfied.

Definition at line 611 of file Polyhedra_Powerset.templates.hh.

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

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::Polyhedra_Powerset< PH >::add_space_dimensions_and_embed(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::add_space_dimensions_and_project(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::ascii_load(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::BGP99_heuristics_assign(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::concatenate_assign(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::map_space_dimensions(), 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::Polyhedra_Powerset< PH >::remove_higher_space_dimensions(), and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::remove_space_dimensions().

00611                                  {
00612   const Polyhedra_Powerset& x = *this;
00613   for (const_iterator xi = x.begin(), x_end = x.end(); xi != x_end; ++xi) {
00614     const PH& pi = xi->element();
00615     if (pi.space_dimension() != x.space_dim) {
00616 #ifndef NDEBUG
00617       std::cerr << "Space dimension mismatch: is " << pi.space_dimension()
00618                 << " in an element of the sequence,\nshould be "
00619                 << x.space_dim << "."
00620                 << std::endl;
00621 #endif
00622       return false;
00623     }
00624   }
00625   return x.Base::OK();
00626 }

template<typename PH>
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::add_disjunct ( const PH &  ph  )  [inline]

Adds to *this the disjunct ph.

Exceptions:
std::invalid_argument Thrown if *this and ph are dimension-incompatible.

Definition at line 42 of file Polyhedra_Powerset.templates.hh.

References Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, Parma_Polyhedra_Library::Powerset< D >::sequence, and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::space_dimension().

Referenced by Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::ascii_load(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::BHZ03_widening_assign(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::concatenate_assign(), and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::linear_partition_aux().

00042                                                  {
00043   Polyhedra_Powerset& x = *this;
00044   if (x.space_dimension() != ph.space_dimension()) {
00045     std::ostringstream s;
00046     s << "PPL::Polyhedra_Powerset<PH>::add_disjunct(ph):\n"
00047       << "this->space_dimension() == " << x.space_dimension() << ", "
00048       << "ph.space_dimension() == " << ph.space_dimension() << ".";
00049     throw std::invalid_argument(s.str());
00050   }
00051   x.sequence.push_back(Determinate<PH>(ph));
00052   x.reduced = false;
00053   assert(x.OK());
00054 }

template<typename PH>
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::add_constraint ( const Constraint c  )  [inline]

Intersects *this with constraint c.

Exceptions:
std::invalid_argument Thrown if *this and constraint c are topology-incompatible or dimension-incompatible.

Definition at line 129 of file Polyhedra_Powerset.templates.hh.

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

00129                                                           {
00130   Polyhedra_Powerset& x = *this;
00131   for (Sequence_iterator si = x.sequence.begin(),
00132          s_end = x.sequence.end(); si != s_end; ++si)
00133     si->element().add_constraint(c);
00134   x.reduced = false;
00135   assert(x.OK());
00136 }

template<typename PH>
bool Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::add_constraint_and_minimize ( const Constraint c  )  [inline]

Intersects *this with the constraint c, minimizing the result.

Returns:
false if and only if the result is empty.
Exceptions:
std::invalid_argument Thrown if *this and c are topology-incompatible or dimension-incompatible.

Definition at line 140 of file Polyhedra_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::empty(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00140                                                                        {
00141   Polyhedra_Powerset& x = *this;
00142   for (Sequence_iterator si = x.sequence.begin(),
00143          s_end = x.sequence.end(); si != s_end; )
00144     if (!si->element().add_constraint_and_minimize(c))
00145       si = x.sequence.erase(si);
00146     else {
00147       x.reduced = false;
00148       ++si;
00149     }
00150   assert(x.OK());
00151   return !x.empty();
00152 }

template<typename PH>
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::add_constraints ( const Constraint_System cs  )  [inline]

Intersects *this with the constraints in cs.

Parameters:
cs The constraints to intersect with.
Exceptions:
std::invalid_argument Thrown if *this and cs are topology-incompatible or dimension-incompatible.

Definition at line 156 of file Polyhedra_Powerset.templates.hh.

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

00156                                                                    {
00157   Polyhedra_Powerset& x = *this;
00158   for (Sequence_iterator si = x.sequence.begin(),
00159          s_end = x.sequence.end(); si != s_end; ++si)
00160     si->element().add_constraints(cs);
00161   x.reduced = false;
00162   assert(x.OK());
00163 }

template<typename PH>
bool Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::add_constraints_and_minimize ( const Constraint_System cs  )  [inline]

Intersects *this with the constraints in cs, minimizing the result.

Returns:
false if and only if the result is empty.
Parameters:
cs The constraints to intersect with.
Exceptions:
std::invalid_argument Thrown if *this and cs are topology-incompatible or dimension-incompatible.

Definition at line 168 of file Polyhedra_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::empty(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00168                                                           {
00169   Polyhedra_Powerset& x = *this;
00170   for (Sequence_iterator si = x.sequence.begin(),
00171          s_end = x.sequence.end(); si != s_end; )
00172     if (!si->element().add_constraints_and_minimize(cs))
00173       si = x.sequence.erase(si);
00174     else {
00175       x.reduced = false;
00176       ++si;
00177     }
00178   assert(x.OK());
00179   return !x.empty();
00180 }

template<typename PH>
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::pairwise_reduce (  )  [inline]

Assign to *this the result of (recursively) merging together the pairs of polyhedra whose poly-hull is the same as their set-theoretical union.

On exit, for all the pairs $\cP$, $\cQ$ of different polyhedra in *this, we have $\cP \uplus \cQ \neq \cP \union \cQ$.

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

References Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct(), Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::EMPTY, Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::OK(), Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), Parma_Polyhedra_Library::Powerset< D >::sequence, Parma_Polyhedra_Library::Powerset< D >::size(), and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::space_dim.

Referenced by Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::BGP99_extrapolation_assign(), and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::BHZ03_widening_assign().

00264                                         {
00265   Polyhedra_Powerset& x = *this;
00266   // It is wise to omega-reduce before pairwise-reducing.
00267   x.omega_reduce();
00268 
00269   size_type n = x.size();
00270   size_type deleted;
00271   do {
00272     Polyhedra_Powerset new_x(x.space_dim, EMPTY);
00273     std::deque<bool> marked(n, false);
00274     deleted = 0;
00275     Sequence_iterator s_begin = x.sequence.begin();
00276     Sequence_iterator s_end = x.sequence.end();
00277     unsigned si_index = 0;
00278     for (Sequence_iterator si = s_begin; si != s_end; ++si, ++si_index) {
00279       if (marked[si_index])
00280         continue;
00281       PH& pi = si->element();
00282       Sequence_const_iterator sj = si;
00283       unsigned sj_index = si_index;
00284       for (++sj, ++sj_index; sj != s_end; ++sj, ++sj_index) {
00285         if (marked[sj_index])
00286           continue;
00287         const PH& pj = sj->element();
00288         if (pi.upper_bound_assign_if_exact(pj)) {
00289           marked[si_index] = marked[sj_index] = true;
00290           new_x.add_non_bottom_disjunct(pi);
00291           ++deleted;
00292           goto next;
00293         }
00294       }
00295     next:
00296       ;
00297     }
00298     iterator nx_begin = new_x.begin();
00299     iterator nx_end = new_x.end();
00300     unsigned xi_index = 0;
00301     for (const_iterator xi = x.begin(),
00302            x_end = x.end(); xi != x_end; ++xi, ++xi_index)
00303       if (!marked[xi_index])
00304         nx_begin = new_x.add_non_bottom_disjunct(*xi, nx_begin, nx_end);
00305     std::swap(x.sequence, new_x.sequence);
00306     n -= deleted;
00307   } while (deleted > 0);
00308   assert(x.OK());
00309 }

template<typename PH>
template<typename Widening>
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::BGP99_extrapolation_assign ( const Polyhedra_Powerset< PH > &  y,
Widening  wf,
unsigned  max_disjuncts 
) [inline]

Assigns to *this the result of applying the BGP99 extrapolation operator to *this and y, using the widening function wf and the cardinality threshold max_disjuncts.

Parameters:
y A finite powerset of polyhedra. It must definitely entail *this;
wf The widening function to be used on polyhedra objects. It is obtained from the corresponding widening method by using the helper function Parma_Polyhedra_Library::widen_fun_ref. Legal values are, e.g., widen_fun_ref(&Polyhedron::H79_widening_assign) and widen_fun_ref(&Polyhedron::limited_H79_extrapolation_assign, cs);
max_disjuncts The maximum number of disjuncts occurring in the powerset *this before starting the computation. If this number is exceeded, some of the disjuncts in *this are collapsed (i.e., joined together).
Exceptions:
std::invalid_argument Thrown if *this and y are topology-incompatible or dimension-incompatible.
For a description of the extrapolation operator, see [BGP99] and [BHZ03b].

Definition at line 361 of file Polyhedra_Powerset.templates.hh.

References Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::BGP99_heuristics_assign(), Parma_Polyhedra_Library::Powerset< D >::collapse(), Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >::definitely_entails(), and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::pairwise_reduce().

00363                                                    {
00364   // `x' is the current iteration value.
00365   Polyhedra_Powerset& x = *this;
00366 
00367 #ifndef NDEBUG
00368   {
00369     // We assume that `y' entails `x'.
00370     const Polyhedra_Powerset<PH> x_copy = x;
00371     const Polyhedra_Powerset<PH> y_copy = y;
00372     assert(y_copy.definitely_entails(x_copy));
00373   }
00374 #endif
00375 
00376   x.pairwise_reduce();
00377   if (max_disjuncts != 0)
00378     x.collapse(max_disjuncts);
00379   x.BGP99_heuristics_assign(y, wf);
00380 }

template<typename PH>
template<typename Cert, typename Widening>
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::BHZ03_widening_assign ( const Polyhedra_Powerset< PH > &  y,
Widening  wf 
) [inline]

Assigns to *this the result of computing the BHZ03-widening between *this and y, using the widening function wf certified by the convergence certificate Cert.

Parameters:
y The finite powerset of polyhedra computed in the previous iteration step. It must definitely entail *this;
wf The widening function to be used on polyhedra objects. It is obtained from the corresponding widening method by using the helper function widen_fun_ref. Legal values are, e.g., widen_fun_ref(&Polyhedron::H79_widening_assign) and widen_fun_ref(&Polyhedron::limited_H79_extrapolation_assign, cs).
Exceptions:
std::invalid_argument Thrown if *this and y are topology-incompatible or dimension-incompatible.
Warning:
In order to obtain a proper widening operator, the template parameter Cert should be a finite convergence certificate for the base-level widening function wf; otherwise, an extrapolation operator is obtained. For a description of the methods that should be provided by Cert, see BHRZ03_Certificate or H79_Certificate.

Definition at line 448 of file Polyhedra_Powerset.templates.hh.

References Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::add_disjunct(), Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >::begin(), Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::BGP99_heuristics_assign(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::collect_certificates(), Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >::definitely_entails(), Parma_Polyhedra_Library::EMPTY, Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >::end(), Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::is_cert_multiset_stabilizing(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::pairwise_reduce(), Parma_Polyhedra_Library::Powerset< D >::size(), and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::space_dim.

00449                                                            {
00450   // `x' is the current iteration value.
00451   Polyhedra_Powerset& x = *this;
00452 
00453 #ifndef NDEBUG
00454   {
00455     // We assume that `y' entails `x'.
00456     const Polyhedra_Powerset<PH> x_copy = x;
00457     const Polyhedra_Powerset<PH> y_copy = y;
00458     assert(y_copy.definitely_entails(x_copy));
00459   }
00460 #endif
00461 
00462   // First widening technique: do nothing.
00463 
00464   // If `y' is the empty collection, do nothing.
00465   assert(x.size() > 0);
00466   if (y.size() == 0)
00467     return;
00468 
00469   // Compute the poly-hull of `x'.
00470   PH x_hull(x.space_dim, EMPTY);
00471   for (const_iterator i = x.begin(), x_end = x.end(); i != x_end; ++i)
00472     x_hull.upper_bound_assign(i->element());
00473 
00474   // Compute the poly-hull of `y'.
00475   PH y_hull(y.space_dim, EMPTY);
00476   for (const_iterator i = y.begin(), y_end = y.end(); i != y_end; ++i)
00477     y_hull.upper_bound_assign(i->element());
00478   // Compute the certificate for `y_hull'.
00479   const Cert y_hull_cert(y_hull);
00480 
00481   // If the hull is stabilizing, do nothing.
00482   int hull_stabilization = y_hull_cert.compare(x_hull);
00483   if (hull_stabilization == 1)
00484     return;
00485 
00486   // Multiset ordering is only useful when `y' is not a singleton.
00487   const bool y_is_not_a_singleton = y.size() > 1;
00488 
00489   // The multiset certificate for `y':
00490   // we want to be lazy about its computation.
00491   typedef std::map<Cert, size_type, typename Cert::Compare> Cert_Multiset;
00492   Cert_Multiset y_cert_ms;
00493   bool y_cert_ms_computed = false;
00494 
00495   if (hull_stabilization == 0 && y_is_not_a_singleton) {
00496     // Collect the multiset certificate for `y'.
00497     y.collect_certificates(y_cert_ms);
00498     y_cert_ms_computed = true;
00499     // If multiset ordering is stabilizing, do nothing.
00500     if (x.is_cert_multiset_stabilizing(y_cert_ms))
00501       return;
00502   }
00503 
00504   // Second widening technique: try the BGP99 powerset heuristics.
00505   Polyhedra_Powerset<PH> bgp99_heuristics = x;
00506   bgp99_heuristics.BGP99_heuristics_assign(y, wf);
00507 
00508   // Compute the poly-hull of `bgp99_heuristics'.
00509   PH bgp99_heuristics_hull(x.space_dim, EMPTY);
00510   for (const_iterator i = bgp99_heuristics.begin(),
00511          bh_end = bgp99_heuristics.end(); i != bh_end; ++i)
00512     bgp99_heuristics_hull.upper_bound_assign(i->element());
00513 
00514   // Check for stabilization and, if successful,
00515   // commit to the result of the extrapolation.
00516   hull_stabilization = y_hull_cert.compare(bgp99_heuristics_hull);
00517   if (hull_stabilization == 1) {
00518     // The poly-hull is stabilizing.
00519     std::swap(x, bgp99_heuristics);
00520     return;
00521   }
00522   else if (hull_stabilization == 0 && y_is_not_a_singleton) {
00523     // If not already done, compute multiset certificate for `y'.
00524     if (!y_cert_ms_computed) {
00525       y.collect_certificates(y_cert_ms);
00526       y_cert_ms_computed = true;
00527     }
00528     if (bgp99_heuristics.is_cert_multiset_stabilizing(y_cert_ms)) {
00529       std::swap(x, bgp99_heuristics);
00530       return;
00531     }
00532     // Third widening technique: pairwise-reduction on `bgp99_heuristics'.
00533     // Note that pairwise-reduction does not affect the computation
00534     // of the poly-hulls, so that we only have to check the multiset
00535     // certificate relation.
00536     Polyhedra_Powerset<PH> reduced_bgp99_heuristics(bgp99_heuristics);
00537     reduced_bgp99_heuristics.pairwise_reduce();
00538     if (reduced_bgp99_heuristics.is_cert_multiset_stabilizing(y_cert_ms)) {
00539       std::swap(x, reduced_bgp99_heuristics);
00540       return;
00541     }
00542   }
00543 
00544   // Fourth widening technique: this is applicable only when
00545   // `y_hull' is a proper subset of `bgp99_heuristics_hull'.
00546   if (bgp99_heuristics_hull.strictly_contains(y_hull)) {
00547     // Compute (y_hull \widen bgp99_heuristics_hull).
00548     PH ph = bgp99_heuristics_hull;
00549     wf(ph, y_hull);
00550     // Compute the difference between `ph' and `bgp99_heuristics_hull'.
00551     ph.difference_assign(bgp99_heuristics_hull);
00552     x.add_disjunct(ph);
00553     return;
00554   }
00555 
00556   // Fall back to the computation of the poly-hull.
00557   Polyhedra_Powerset<PH> x_hull_singleton(x.space_dim, EMPTY);
00558   x_hull_singleton.add_disjunct(x_hull);
00559   std::swap(x, x_hull_singleton);
00560 }

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

The assignment operator (*this and y can be dimension-incompatible).

Definition at line 146 of file Polyhedra_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::space_dim.

00146                                                              {
00147   Polyhedra_Powerset& x = *this;
00148   x.Base::operator=(y);
00149   x.space_dim = y.space_dim;
00150   return x;
00151 }

template<typename PH>
template<typename QH>
Polyhedra_Powerset< PH > & Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::operator= ( const Polyhedra_Powerset< QH > &  y  )  [inline]

Assignment operator allowing a source powerset with elements of a different polyhedron kind (*this and y can be dimension-incompatible).

Definition at line 164 of file Polyhedra_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::swap().

00164                                                                  {
00165   Polyhedra_Powerset& x = *this;
00166   Polyhedra_Powerset<PH> pps(y);
00167   x.swap(pps);
00168   return x;
00169 }

template<typename PH>
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::swap ( Polyhedra_Powerset< PH > &  y  )  [inline]

template<typename PH>
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::add_space_dimensions_and_embed ( dimension_type  m  )  [inline]

Adds m new dimensions to the vector space containing *this and embeds each polyhedron in *this in the new space.

Definition at line 184 of file Polyhedra_Powerset.templates.hh.

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

00184                                                                        {
00185   Polyhedra_Powerset& x = *this;
00186   for (Sequence_iterator si = x.sequence.begin(),
00187          s_end = x.sequence.end(); si != s_end; ++si)
00188     si->element().add_space_dimensions_and_embed(m);
00189   x.space_dim += m;
00190   assert(x.OK());
00191 }

template<typename PH>
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::add_space_dimensions_and_project ( dimension_type  m  )  [inline]

Adds m new dimensions to the vector space containing *this without embedding the polyhedra in *this in the new space.

Definition at line 195 of file Polyhedra_Powerset.templates.hh.

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

00195                                                                          {
00196   Polyhedra_Powerset& x = *this;
00197   for (Sequence_iterator si = x.sequence.begin(),
00198          s_end = x.sequence.end(); si != s_end; ++si)
00199     si->element().add_space_dimensions_and_project(m);
00200   x.space_dim += m;
00201   assert(x.OK());
00202 }

template<typename PH>
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::intersection_assign ( const Polyhedra_Powerset< PH > &  y  )  [inline]

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

The result is obtained by intersecting each polyhedron in *this with each polyhedron in y and collecting all these intersections.

Definition at line 173 of file Polyhedra_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Determinate< PH >::lift_op_assign(), and Parma_Polyhedra_Library::Powerset< D >::pairwise_apply_assign().

00173                                                                        {
00174   Polyhedra_Powerset& x = *this;
00175   x.pairwise_apply_assign
00176     (y, CS::lift_op_assign(std::mem_fun_ref(&PH::intersection_assign)));
00177 }

template<typename PH>
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::poly_difference_assign ( const Polyhedra_Powerset< PH > &  y  ) 

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

The result is obtained by computing the poly-difference of each polyhedron in *this with each polyhedron in y and collecting all these differences.

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

template<typename PH>
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::concatenate_assign ( const Polyhedra_Powerset< PH > &  y  )  [inline]

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

The result is obtained by computing the pairwise concatenation of each polyhedron in *this with each polyhedron in y.

Definition at line 92 of file Polyhedra_Powerset.templates.hh.

References Parma_Polyhedra_Library::abandon_expensive_computations, Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::add_disjunct(), Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Determinate< PH >::concatenate_assign(), Parma_Polyhedra_Library::EMPTY, Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Determinate< PH >::is_bottom(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::OK(), Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >::sequence, Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::space_dim, and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::swap().

00092                                                                       {
00093   Polyhedra_Powerset& x = *this;
00094   // Ensure omega-reduction here, since what follows has quadratic complexity.
00095   x.omega_reduce();
00096   y.omega_reduce();
00097   Polyhedra_Powerset<PH> new_x(x.space_dim + y.space_dim, EMPTY);
00098   for (const_iterator xi = x.begin(), x_end = x.end(),
00099          y_begin = y.begin(), y_end = y.end(); xi != x_end; ) {
00100     for (const_iterator yi = y_begin; yi != y_end; ++yi) {
00101       CS zi = *xi;
00102       zi.concatenate_assign(*yi);
00103       assert(!zi.is_bottom());
00104       new_x.sequence.push_back(zi);
00105     }
00106     ++xi;
00107     if (abandon_expensive_computations && xi != x_end && y_begin != y_end) {
00108       // Hurry up!
00109       PH xph = xi->element();
00110       for (++xi; xi != x_end; ++xi)
00111         xph.upper_bound_assign(xi->element());
00112       const_iterator yi = y_begin;
00113       PH yph = yi->element();
00114       for (++yi; yi != y_end; ++yi)
00115         yph.upper_bound_assign(yi->element());
00116       xph.concatenate_assign(yph);
00117       x.swap(new_x);
00118       x.add_disjunct(xph);
00119       assert(x.OK());
00120       return;
00121     }
00122   }
00123   x.swap(new_x);
00124   assert(x.OK());
00125 }

template<typename PH>
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::time_elapse_assign ( const Polyhedra_Powerset< PH > &  y  )  [inline]

Assigns to *this the result of computing the time-elapse between *this and y.

The result is obtained by computing the pairwise time elapse of each polyhedron in *this with each polyhedron in y.

Definition at line 181 of file Polyhedra_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Determinate< PH >::lift_op_assign(), and Parma_Polyhedra_Library::Powerset< D >::pairwise_apply_assign().

00181                                                                       {
00182   Polyhedra_Powerset& x = *this;
00183   x.pairwise_apply_assign
00184     (y, CS::lift_op_assign(std::mem_fun_ref(&PH::time_elapse_assign)));
00185 }

template<typename PH>
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::remove_space_dimensions ( const Variables_Set to_be_removed  )  [inline]

Removes all the specified space dimensions.

Parameters:
to_be_removed The set of Variable objects corresponding to the space dimensions to be removed.
Exceptions:
std::invalid_argument Thrown if *this is dimension-incompatible with one of the Variable objects contained in to_be_removed.

Definition at line 207 of file Polyhedra_Powerset.templates.hh.

References Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, Parma_Polyhedra_Library::Powerset< D >::sequence, and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::space_dim.

00207                                                             {
00208   Polyhedra_Powerset& x = *this;
00209   Variables_Set::size_type num_removed = to_be_removed.size();
00210   if (num_removed > 0) {
00211     for (Sequence_iterator si = x.sequence.begin(),
00212            s_end = x.sequence.end(); si != s_end; ++si) {
00213       si->element().remove_space_dimensions(to_be_removed);
00214       x.reduced = false;
00215     }
00216     x.space_dim -= num_removed;
00217     assert(x.OK());
00218   }
00219 }

template<typename PH>
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::remove_higher_space_dimensions ( dimension_type  new_dimension  )  [inline]

Removes the higher space dimensions so that the resulting space will have dimension new_dimension.

Exceptions:
std::invalid_argument Thrown if new_dimensions is greater than the space dimension of *this.

Definition at line 223 of file Polyhedra_Powerset.templates.hh.

References Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, Parma_Polyhedra_Library::Powerset< D >::sequence, and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::space_dim.

00224                                                                       {
00225   Polyhedra_Powerset& x = *this;
00226   if (new_dimension < x.space_dim) {
00227     for (Sequence_iterator si = x.sequence.begin(),
00228            s_end = x.sequence.end(); si != s_end; ++si) {
00229       si->element().remove_higher_space_dimensions(new_dimension);
00230       x.reduced = false;
00231     }
00232     x.space_dim = new_dimension;
00233     assert(x.OK());
00234   }
00235 }

template<typename PH>
template<typename Partial_Function>
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::map_space_dimensions ( const Partial_Function &  pfunc  )  [inline]

Remaps the dimensions of the vector space according to a partial function.

See also Polyhedron::map_space_dimensions.

Definition at line 240 of file Polyhedra_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::is_bottom(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, Parma_Polyhedra_Library::Powerset< D >::sequence, and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::space_dim.

00240                                                                           {
00241   Polyhedra_Powerset& x = *this;
00242   if (x.is_bottom()) {
00243     dimension_type n = 0;
00244     for (dimension_type i = x.space_dim; i-- > 0; ) {
00245       dimension_type new_i;
00246       if (pfunc.maps(i, new_i))
00247         ++n;
00248     }
00249     x.space_dim = n;
00250   }
00251   else {
00252     Sequence_iterator s_begin = x.sequence.begin();
00253     for (Sequence_iterator si = s_begin,
00254            s_end = x.sequence.end(); si != s_end; ++si)
00255       si->element().map_space_dimensions(pfunc);
00256     x.space_dim = s_begin->element().space_dimension();
00257     x.reduced = false;
00258   }
00259   assert(x.OK());
00260 }

template<typename PH>
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::ascii_dump (  )  const

Writes to std::cerr an ASCII representation of *this.

template<typename PH>
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::ascii_dump ( std::ostream &  s  )  const [inline]

Writes to s an ASCII representation of *this.

Definition at line 564 of file Polyhedra_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Powerset< D >::size(), and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::space_dim.

00564                                                       {
00565   const Polyhedra_Powerset& x = *this;
00566   s << "size " << x.size()
00567     << "\nspace_dim " << x.space_dim
00568     << "\n";
00569   for (const_iterator xi = x.begin(), x_end = x.end(); xi != x_end; ++xi)
00570     xi->element().ascii_dump(s);
00571 }

template<typename PH>
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::print (  )  const

Prints *this to std::cerr using operator<<.

template<typename PH>
bool Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::ascii_load ( std::istream &  s  )  [inline]

Loads from s an ASCII representation (as produced by ascii_dump) and sets *this accordingly. Returns true if successful, false otherwise.

Definition at line 577 of file Polyhedra_Powerset.templates.hh.

References Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::add_disjunct(), Parma_Polyhedra_Library::EMPTY, Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::OK(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::space_dim, and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::swap().

00577                                                 {
00578   Polyhedra_Powerset& x = *this;
00579   std::string str;
00580 
00581   if (!(s >> str) || str != "size")
00582     return false;
00583 
00584   size_type sz;
00585 
00586   if (!(s >> sz))
00587     return false;
00588 
00589   if (!(s >> str) || str != "space_dim")
00590     return false;
00591 
00592   if (!(s >> x.space_dim))
00593     return false;
00594 
00595   Polyhedra_Powerset new_x(x.space_dim, EMPTY);
00596   while (sz-- > 0) {
00597     PH ph;
00598     if (!ph.ascii_load(s))
00599       return false;
00600     new_x.add_disjunct(ph);
00601   }
00602   x.swap(new_x);
00603 
00604   // Check for well-formedness.
00605   assert(x.OK());
00606   return true;
00607 }

template<typename PH>
template<typename Widening>
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::BGP99_heuristics_assign ( const Polyhedra_Powerset< PH > &  y,
Widening  wf 
) [inline, private]

Assigns to *this the result of applying the BGP99 heuristics to *this and y, using the widening function wf.

Definition at line 315 of file Polyhedra_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct(), Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >::definitely_entails(), Parma_Polyhedra_Library::EMPTY, Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Powerset< D >::is_omega_reduced(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::OK(), Parma_Polyhedra_Library::Powerset< D >::sequence, Parma_Polyhedra_Library::Powerset< D >::size(), and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::space_dim.

Referenced by Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::BGP99_extrapolation_assign(), and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::BHZ03_widening_assign().

00315                                                                   {
00316   // `x' is the current iteration value.
00317   Polyhedra_Powerset& x = *this;
00318 
00319 #ifndef NDEBUG
00320   {
00321     // We assume that `y' entails `x'.
00322     const Polyhedra_Powerset<PH> x_copy = x;
00323     const Polyhedra_Powerset<PH> y_copy = y;
00324     assert(y_copy.definitely_entails(x_copy));
00325   }
00326 #endif
00327 
00328   size_type n = x.size();
00329   Polyhedra_Powerset new_x(x.space_dim, EMPTY);
00330   std::deque<bool> marked(n, false);
00331   const_iterator x_begin = x.begin();
00332   const_iterator x_end = x.end();
00333   unsigned i_index = 0;
00334   for (const_iterator i = x_begin,
00335          y_begin = y.begin(), y_end = y.end(); i != x_end; ++i, ++i_index)
00336     for (const_iterator j = y_begin; j != y_end; ++j) {
00337       const PH& pi = i->element();
00338       const PH& pj = j->element();
00339       if (pi.contains(pj)) {
00340         PH pi_copy = pi;
00341         wf(pi_copy, pj);
00342         new_x.add_non_bottom_disjunct(pi_copy);
00343         marked[i_index] = true;
00344       }
00345     }
00346   iterator nx_begin = new_x.begin();
00347   iterator nx_end = new_x.end();
00348   i_index = 0;
00349   for (const_iterator i = x_begin; i != x_end; ++i, ++i_index)
00350     if (!marked[i_index])
00351       nx_begin = new_x.add_non_bottom_disjunct(*i, nx_begin, nx_end);
00352   std::swap(x.sequence, new_x.sequence);
00353   assert(x.OK());
00354   assert(x.is_omega_reduced());
00355 }

template<typename PH>
template<typename Cert>
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::collect_certificates ( std::map< Cert, size_type, typename Cert::Compare > &  cert_ms  )  const [inline, private]

Records in cert_ms the certificates for this set of polyhedra.

Definition at line 386 of file Polyhedra_Powerset.templates.hh.

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

Referenced by Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::BHZ03_widening_assign(), and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::is_cert_multiset_stabilizing().

00387                                                                     {
00388   const Polyhedra_Powerset& x = *this;
00389   assert(x.is_omega_reduced());
00390   assert(cert_ms.size() == 0);
00391   for (const_iterator i = x.begin(), end = x.end(); i != end; i++) {
00392     Cert ph_cert(i->element());
00393     ++cert_ms[ph_cert];
00394   }
00395 }

template<typename PH>
template<typename Cert>
bool Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::is_cert_multiset_stabilizing ( const std::map< Cert, size_type, typename Cert::Compare > &  y_cert_ms  )  const [inline, private]

Returns true if and only if the current set of polyhedra is stabilizing with respect to the multiset of certificates y_cert_ms.

Definition at line 401 of file Polyhedra_Powerset.templates.hh.

References Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::collect_certificates().

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

00403                                      {
00404   typedef std::map<Cert, size_type, typename Cert::Compare> Cert_Multiset;
00405   Cert_Multiset x_cert_ms;
00406   collect_certificates(x_cert_ms);
00407   typename Cert_Multiset::const_iterator
00408     xi = x_cert_ms.begin(),
00409     xend = x_cert_ms.end(),
00410     yi = y_cert_ms.begin(),
00411     yend = y_cert_ms.end();
00412   while (xi != xend && yi != yend) {
00413     const Cert& xi_cert = xi->first;
00414     const Cert& yi_cert = yi->first;
00415     switch (xi_cert.compare(yi_cert)) {
00416     case 0:
00417       // xi_cert == yi_cert: check the number of multiset occurrences.
00418       {
00419         const size_type& xi_count = xi->second;
00420         const size_type& yi_count = yi->second;
00421         if (xi_count == yi_count) {
00422           // Same number of occurrences: compare the next pair.
00423           ++xi;
00424           ++yi;
00425         }
00426         else
00427           // Different number of occurrences: can decide ordering.
00428           return xi_count < yi_count;
00429         break;
00430       }
00431     case 1:
00432       // xi_cert > yi_cert: it is not stabilizing.
00433       return false;
00434 
00435     case -1:
00436       // xi_cert < yi_cert: it is stabilizing.
00437       return true;
00438     }
00439   }
00440   // Here xi == xend or yi == yend.
00441   // Stabilization is achieved if `y_cert_ms' still has other elements.
00442   return yi != yend;
00443 }

template<>
void Parma_Polyhedra_Library::Polyhedra_Powerset< NNC_Polyhedron >::poly_difference_assign ( const Polyhedra_Powerset< PH > &  y  )  [inline]

template<>
bool Parma_Polyhedra_Library::Polyhedra_Powerset< NNC_Polyhedron >::geometrically_covers ( const Polyhedra_Powerset< PH > &  y  )  const [inline]

template<>
bool Parma_Polyhedra_Library::Polyhedra_Powerset< NNC_Polyhedron >::geometrically_equals ( const Polyhedra_Powerset< PH > &  y  )  const [inline]

Definition at line 208 of file Polyhedra_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::geometrically_covers().

00208                                                         {
00209   const Polyhedra_Powerset& x = *this;
00210   return x.geometrically_covers(y) && y.geometrically_covers(x);
00211 }

template<>
void Parma_Polyhedra_Library::Polyhedra_Powerset< C_Polyhedron >::poly_difference_assign ( const Polyhedra_Powerset< PH > &  y  )  [inline]

Definition at line 228 of file Polyhedra_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::poly_difference_assign().

00228                                                     {
00229   Polyhedra_Powerset<NNC_Polyhedron> nnc_this(*this);
00230   Polyhedra_Powerset<NNC_Polyhedron> nnc_y(y);
00231   nnc_this.poly_difference_assign(nnc_y);
00232   *this = nnc_this;
00233 }

template<>
void Parma_Polyhedra_Library::Polyhedra_Powerset< PPL::NNC_Polyhedron >::poly_difference_assign ( const Polyhedra_Powerset< PH > &  y  )  [inline]

Definition at line 70 of file Polyhedra_Powerset.cc.

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

00070                                                     {
00071   Polyhedra_Powerset& x = *this;
00072   // Ensure omega-reduction.
00073   x.omega_reduce();
00074   y.omega_reduce();
00075   Sequence new_sequence = x.sequence;
00076   for (const_iterator yi = y.begin(), y_end = y.end(); yi != y_end; ++yi) {
00077     const NNC_Polyhedron& py = yi->element();
00078     Sequence tmp_sequence;
00079     for (Sequence_const_iterator nsi = new_sequence.begin(),
00080            ns_end = new_sequence.end(); nsi != ns_end; ++nsi) {
00081       std::pair<NNC_Polyhedron, Polyhedra_Powerset<NNC_Polyhedron> > partition
00082         = linear_partition(py, nsi->element());
00083       const Polyhedra_Powerset<NNC_Polyhedron>& residues = partition.second;
00084       // Append the contents of `residues' to `tmp_sequence'.
00085       std::copy(residues.begin(), residues.end(), back_inserter(tmp_sequence));
00086     }
00087     std::swap(tmp_sequence, new_sequence);
00088   }
00089   std::swap(x.sequence, new_sequence);
00090   x.reduced = false;
00091   assert(x.OK());
00092 }

template<>
bool Parma_Polyhedra_Library::Polyhedra_Powerset< PPL::NNC_Polyhedron >::geometrically_covers ( const Polyhedra_Powerset< PH > &  y  )  const [inline]

Definition at line 97 of file Polyhedra_Powerset.cc.

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

00097                                                         {
00098   const Polyhedra_Powerset& x = *this;
00099   for (const_iterator yi = y.begin(), y_end = y.end(); yi != y_end; ++yi)
00100     if (!check_containment(yi->element(), x))
00101       return false;
00102   return true;
00103 }


Friends And Related Function Documentation

template<typename PH>
friend class Polyhedra_Powerset [friend]

Definition at line 443 of file Polyhedra_Powerset.defs.hh.

template<typename PH>
Widening_Function< PH > widen_fun_ref ( void(PH::*)(const PH &, unsigned *)  wm  )  [related]

Wraps a widening method into a function object.

Parameters:
wm The widening method.

Definition at line 59 of file Widening_Function.inlines.hh.

00059                                                    {
00060   return Widening_Function<PH>(wm);
00061 }

template<typename PH, typename CS>
Limited_Widening_Function< PH, CS > widen_fun_ref ( void(PH::*)(const PH &, const CS &, unsigned *)  lwm,
const CS cs 
) [related]

Wraps a limited widening method into a function object.

Parameters:
lwm The limited widening method.
cs The constraint system limiting the widening.

Definition at line 66 of file Widening_Function.inlines.hh.

00067                             {
00068   return Limited_Widening_Function<PH, CS>(lwm, cs);
00069 }

template<typename PH>
std::pair< PH, Polyhedra_Powerset< NNC_Polyhedron > > linear_partition ( const PH &  p,
const PH &  q 
) [related]

Partitions q with respect to p.

Let p and q be two polyhedra. The function returns an object r of type std::pair<PH, Polyhedra_Powerset<NNC_Polyhedron> > such that

  • r.first is the intersection of p and q;
  • r.second has the property that all its elements are pairwise disjoint and disjoint from p;
  • the union of r.first with all the elements of r.second gives q (i.e., r is the representation of a partition of q).

See this paper for more information about the implementation.

Definition at line 662 of file Polyhedra_Powerset.templates.hh.

References Parma_Polyhedra_Library::Constraint_System::begin(), Parma_Polyhedra_Library::EMPTY, Parma_Polyhedra_Library::Constraint_System::end(), Parma_Polyhedra_Library::Constraint::is_equality(), and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::linear_partition_aux().

Referenced by Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::check_containment(), and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::poly_difference_assign().

00662                                            {
00663   using Implementation::Polyhedra_Powersets::linear_partition_aux;
00664 
00665   Polyhedra_Powerset<NNC_Polyhedron> r(p.space_dimension(), EMPTY);
00666   PH qq = q;
00667   const Constraint_System& pcs = p.constraints();
00668   for (Constraint_System::const_iterator i = pcs.begin(),
00669          pcs_end = pcs.end(); i != pcs_end; ++i) {
00670     const Constraint c = *i;
00671     if (c.is_equality()) {
00672       Linear_Expression le(c);
00673       linear_partition_aux(le <= 0, qq, r);
00674       linear_partition_aux(le >= 0, qq, r);
00675     }
00676     else
00677       linear_partition_aux(c, qq, r);
00678   }
00679   return std::pair<PH, Polyhedra_Powerset<NNC_Polyhedron> >(qq, r);
00680 }

template<typename PH>
bool check_containment ( const NNC_Polyhedron ph,
const Polyhedra_Powerset< NNC_Polyhedron > &  ps 
) [related]

Returns true if and only if the union of the NNC polyhedra in ps contains the NNC polyhedron ph.

Definition at line 107 of file Polyhedra_Powerset.cc.

References Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >::begin(), Parma_Polyhedra_Library::Polyhedron::contains(), Parma_Polyhedra_Library::EMPTY, Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >::end(), Parma_Polyhedra_Library::Polyhedron::is_disjoint_from(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::linear_partition(), and Parma_Polyhedra_Library::Polyhedron::space_dimension().

Referenced by Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::check_containment(), and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::geometrically_covers().

00108                                                                      {
00109   Polyhedra_Powerset<NNC_Polyhedron> tmp(ph.space_dimension(), EMPTY);
00110   tmp.add_disjunct(ph);
00111   for (Polyhedra_Powerset<NNC_Polyhedron>::const_iterator
00112          i = ps.begin(), ps_end = ps.end(); i != ps_end; ++i) {
00113     const NNC_Polyhedron& pi = i->element();
00114     for (Polyhedra_Powerset<NNC_Polyhedron>::iterator
00115            j = tmp.begin(); j != tmp.end(); ) {
00116       const NNC_Polyhedron& pj = j->element();
00117       if (pi.contains(pj))
00118         j = tmp.drop_disjunct(j);
00119       else
00120         ++j;
00121     }
00122     if (tmp.empty())
00123       return true;
00124     else {
00125       Polyhedra_Powerset<NNC_Polyhedron> new_disjuncts(ph.space_dimension(),
00126                                                        EMPTY);
00127       for (Polyhedra_Powerset<NNC_Polyhedron>::iterator
00128              j = tmp.begin(); j != tmp.end(); ) {
00129         const NNC_Polyhedron& pj = j->element();
00130         if (pj.is_disjoint_from(pi))
00131           ++j;
00132         else {
00133           std::pair<NNC_Polyhedron, Polyhedra_Powerset<NNC_Polyhedron> >
00134             partition = linear_partition(pi, pj);
00135           new_disjuncts.upper_bound_assign(partition.second);
00136           j = tmp.drop_disjunct(j);
00137         }
00138       }
00139       tmp.upper_bound_assign(new_disjuncts);
00140     }
00141   }
00142   return false;
00143 }

template<typename PH>
bool check_containment ( const PH &  ph,
const Polyhedra_Powerset< PH > &  ps 
) [related]

Returns true if and only if the union of the objects in ps contains ph.

Note:
It is assumed that the template parameter PH can be converted without precision loss into an NNC_Polyhedron; otherwise, an incorrect result might be obtained.

Definition at line 238 of file Polyhedra_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::check_containment().

00238                                                                   {
00239   const NNC_Polyhedron pph = NNC_Polyhedron(ph.constraints());
00240   const Polyhedra_Powerset<NNC_Polyhedron> pps(ps);
00241   return check_containment(pph, pps);
00242 }

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

Specializes std::swap.

Definition at line 261 of file Polyhedra_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::swap().

00262                                                        {
00263   x.swap(y);
00264 }

bool check_containment ( const C_Polyhedron ph,
const Polyhedra_Powerset< C_Polyhedron > &  ps 
) [related]

Definition at line 247 of file Polyhedra_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::check_containment().

00248                                                               {
00249   return check_containment(NNC_Polyhedron(ph),
00250                            Polyhedra_Powerset<NNC_Polyhedron>(ps));
00251 }

template<typename PH>
void linear_partition_aux ( const Constraint c,
PH &  qq,
Polyhedra_Powerset< NNC_Polyhedron > &  r 
) [related]

Partitions polyhedron qq according to constraint c.

On exit, the intersection of qq and constraint c is stored in qq, whereas the intersection of qq with the negation of c is added as a new disjunct of the powerset r.

Definition at line 643 of file Polyhedra_Powerset.templates.hh.

References Parma_Polyhedra_Library::Polyhedron::add_constraint_and_minimize(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::add_disjunct(), and Parma_Polyhedra_Library::Constraint::is_strict_inequality().

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

00645                                                             {
00646   Linear_Expression le(c);
00647   Constraint neg_c = c.is_strict_inequality() ? (le <= 0) : (le < 0);
00648   NNC_Polyhedron qqq(qq);
00649   if (qqq.add_constraint_and_minimize(neg_c))
00650     r.add_disjunct(qqq);
00651   qq.add_constraint(c);
00652 }


Member Data Documentation


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

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