Inherits Parma_Polyhedra_Library::PowerSet< Parma_Polyhedra_Library::Determinate< PH > >.
Public Member Functions | |
Constructors | |
| Polyhedra_PowerSet (dimension_type num_dimensions=0, Polyhedron::Degenerate_Kind kind=Polyhedron::UNIVERSE) | |
| Builds a universe (top) or empty (bottom) Polyhedra_PowerSet. | |
| Polyhedra_PowerSet (const Polyhedra_PowerSet &y) | |
| Ordinary copy-constructor. | |
| Polyhedra_PowerSet (const ConSys &cs) | |
Creates a Polyhedra_PowerSet with the same information contents as cs. | |
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 | semantically_contains (const Polyhedra_PowerSet &y) const |
Returns true if and only if *this semantically (i.e., geometrically) contains y. | |
| bool | semantically_equals (const Polyhedra_PowerSet &y) const |
Returns true if and only if *this is semantically (i.e., geometrically) equal to y. | |
| bool | OK () const |
| Checks if all the invariants are satisfied. | |
Space-Dimension Preserving Member Functions that May Modify the Powerset of Polyhedra | |
| 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 ConSys &cs) |
Intersects *this with the constraints in cs. | |
| bool | add_constraints_and_minimize (const ConSys &cs) |
Intersects *this with the constraints in cs, minimizing the result. | |
| 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. | |
| template<typename Widening> void | BHZ03_widening_assign (const Polyhedra_PowerSet &y, Widening wf) |
An instance of the BHZ03 framework using the widening function wf certified by BHRZ03_Certificate. | |
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). | |
| void | swap (Polyhedra_PowerSet &y) |
Swaps *this with y. | |
| void | add_dimensions_and_embed (dimension_type m) |
Adds m new dimensions and embeds the old polyhedron in the new space. | |
| void | add_dimensions_and_project (dimension_type m) |
Adds m new dimensions to the polyhedron and does not embed it in the new space. | |
| void | concatenate_assign (const Polyhedra_PowerSet &y) |
Assigns to *this the concatenation of *this and y. | |
| void | remove_dimensions (const Variables_Set &to_be_removed) |
| Removes all the specified dimensions. | |
| void | remove_higher_dimensions (dimension_type new_dimension) |
Removes the higher dimensions so that the resulting space will have dimension new_dimension. | |
| template<typename PartialFunction> void | map_dimensions (const PartialFunction &pfunc) |
| Remaps the dimensions of the vector space according to a partial function. | |
Static Public Member Functions | |
| 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 (void(PH::*wm)(const PH &, unsigned *)) |
| Wraps a widening method into a function object. | |
|
Limited_Widening_Function< PH > | widen_fun (void(PH::*lwm)(const PH &, const ConSys &, unsigned *), const ConSys &cs) |
| Wraps a limited widening method into a function object. | |
| void | swap (Parma_Polyhedra_Library::Polyhedra_PowerSet< PH > &x, Parma_Polyhedra_Library::Polyhedra_PowerSet< PH > &y) |
Specializes std::swap. | |
| std::pair< PH, Polyhedra_PowerSet< NNC_Polyhedron > > | linear_partition (const PH &p, const PH &q) |
Partitions q with respect to p. | |
|
||||||||||||||||
|
Builds a universe (top) or empty (bottom) Polyhedra_PowerSet.
|
|
||||||||||
|
Returns
|
|
||||||||||
|
Returns
|
|
||||||||||
|
Intersects
|
|
||||||||||
|
Intersects
|
|
||||||||||
|
Intersects
|
|
||||||||||
|
Intersects
|
|
||||||||||||||||||||||||
|
Assigns to
|
|
||||||||||||||||||||
|
Assigns to
Cert, then an attempt is made to apply the base-level widening wf to the poly-hulls of *this and y, possibly improving the result using Polyhedron::poly_difference_assign. For more details and a justification of the overall approach, see [BHZ03b] and [BHZ04].
|
|
||||||||||
|
Assigns to
Seeing a powerset as a set of tuples, this method assigns to
Intuitively, the result is obtained by computing the pair-wise concatenation of each polyhedron in |
|
||||||||||
|
Removes all the specified dimensions.
|
|
||||||||||
|
Removes the higher dimensions so that the resulting space will have dimension
|
|
||||||||||||||
|
Remaps the dimensions of the vector space according to a partial function. See also Polyhedron::map_dimensions. |
|
||||||||||||||||
|
Partitions
Let
|
1.3.8-20040812