Inherits Powerset< Parma_Polyhedra_Library::Determinate< PH > >.
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_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.) | |
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, CS > | widen_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) |
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.
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. |
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
.
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
.
std::invalid_argument | Thrown if *this and y are topology-incompatible or dimension-incompatible. |
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.
std::invalid_argument | Thrown if *this and y are topology-incompatible or dimension-incompatible. |
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::add_disjunct | ( | const PH & | ph | ) | [inline] |
Adds to *this
the disjunct ph
.
std::invalid_argument | Thrown if *this and ph are dimension-incompatible. |
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::add_constraint | ( | const Constraint & | c | ) | [inline] |
Intersects *this
with constraint c
.
std::invalid_argument | Thrown if *this and constraint c are topology-incompatible or dimension-incompatible. |
bool Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::add_constraint_and_minimize | ( | const Constraint & | c | ) | [inline] |
Intersects *this
with the constraint c
, minimizing the result.
false
if and only if the result is empty.std::invalid_argument | Thrown if *this and c are topology-incompatible or dimension-incompatible. |
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::add_constraints | ( | const Constraint_System & | cs | ) | [inline] |
Intersects *this
with the constraints in cs
.
cs | The constraints to intersect with. |
std::invalid_argument | Thrown if *this and cs are topology-incompatible or dimension-incompatible. |
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.
false
if and only if the result is empty.cs | The constraints to intersect with. |
std::invalid_argument | Thrown if *this and cs are topology-incompatible or dimension-incompatible. |
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 ,
of different polyhedra in
*this
, we have .
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
.
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). |
std::invalid_argument | Thrown if *this and y are topology-incompatible or dimension-incompatible. |
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
.
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) . |
std::invalid_argument | Thrown if *this and y are topology-incompatible or dimension-incompatible. |
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. 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.
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.
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
.
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
.
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::remove_space_dimensions | ( | const Variables_Set & | to_be_removed | ) | [inline] |
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
.
std::invalid_argument | Thrown if new_dimensions is greater than the space dimension of *this . |
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.
Widening_Function< PH > widen_fun_ref | ( | void(PH::*)(const PH &, unsigned *) | wm | ) | [related] |
Wraps a widening method into a function object.
wm | The widening method. |
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.
lwm | The limited widening method. | |
cs | The constraint system limiting the widening. |
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
;r.first
with all the elements of r.second
gives q
(i.e., r
is the representation of a partition of q
).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
.
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] |