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

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

Inherits Powerset< Parma_Polyhedra_Library::Determinate< PH > >.

List of all members.

Public Member Functions

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.

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)


Detailed Description

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

The powerset construction instantiated on PPL polyhedra.


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.

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.


Member Function Documentation

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!

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!

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.

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.

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.

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.

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.

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

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

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.

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.

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.

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.

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.

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.

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.

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.


Friends And Related Function Documentation

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.

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.

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

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.

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

Specializes std::swap.

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


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