- Main Page
- Modules
- Namespaces
- Classes
- Related Pages

- Class List
- Class Hierarchy
- Class Members

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

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

Inherits Parma_Polyhedra_Library::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)
| with the same information contents as `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_Powerset & | operator= (const Polyhedra_Powerset &y)
| The assignment operator (`*this` and `y` can be dimension-incompatible).
template<typename QH>
Polyhedra_Powerset & | operator= (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.)
Widening_Function< PH > | widen_fun_ref (void(PH::*wm)(const PH &, unsigned *))
| Wraps a widening method into a function object.
Limited_Widening_Function< PH, CS > | widen_fun_ref (void(PH::*lwm)(const PH &, const CS &, unsigned *), const CS &cs)
| Wraps a limited widening method into a function object.
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`.
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`.
void | swap (Parma_Polyhedra_Library::Polyhedra_Powerset< PH > &x, Parma_Polyhedra_Library::Polyhedra_Powerset< PH > &y)
| Specializes `std::swap`.

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

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

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

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

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

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

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

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 , of different polyhedra in `*this`, we have .

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

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

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

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

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

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

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>

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.