#include <Polyhedra_Powerset.defs.hh>
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_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. | |
Private Types | |
typedef Determinate< PH > | CS |
typedef Powerset< CS > | Base |
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, 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) |
template<typename PH> | |
void | linear_partition_aux (const Constraint &c, PH &qq, Polyhedra_Powerset< NNC_Polyhedron > &r) |
Partitions polyhedron qq according to constraint c . |
Definition at line 46 of file Polyhedra_Powerset.defs.hh.
typedef PH Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::element_type |
Definition at line 50 of file Polyhedra_Powerset.defs.hh.
typedef Determinate<PH> Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::CS [private] |
Definition at line 53 of file Polyhedra_Powerset.defs.hh.
typedef Powerset<CS> Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::Base [private] |
Definition at line 54 of file Polyhedra_Powerset.defs.hh.
typedef Base::size_type Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::size_type |
Reimplemented from Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >.
Definition at line 388 of file Polyhedra_Powerset.defs.hh.
typedef Base::value_type Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::value_type |
Reimplemented from Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PH > >.
Definition at line 389 of file Polyhedra_Powerset.defs.hh.
typedef Base::iterator Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::iterator |
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.
typedef Base::const_iterator Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::const_iterator |
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.
typedef Base::reverse_iterator Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::reverse_iterator |
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.
typedef Base::const_reverse_iterator Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::const_reverse_iterator |
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.
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.
typedef Base::Sequence_iterator Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::Sequence_iterator [private] |
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.
typedef Base::Sequence_const_iterator Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::Sequence_const_iterator [private] |
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.
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. |
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 }
Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::Polyhedra_Powerset | ( | const Polyhedra_Powerset< PH > & | y | ) | [inline] |
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.
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.
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 }
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 }
Parma_Polyhedra_Library::Polyhedra_Powerset< NNC_Polyhedron >::Polyhedra_Powerset | ( | const Polyhedra_Powerset< QH > & | y | ) | [inline] |
Parma_Polyhedra_Library::Polyhedra_Powerset< C_Polyhedron >::Polyhedra_Powerset | ( | const Polyhedra_Powerset< QH > & | y | ) | [inline] |
Parma_Polyhedra_Library::Polyhedra_Powerset< NNC_Polyhedron >::Polyhedra_Powerset | ( | const Polyhedra_Powerset< C_Polyhedron > & | y | ) | [inline] |
Parma_Polyhedra_Library::Polyhedra_Powerset< C_Polyhedron >::Polyhedra_Powerset | ( | const Polyhedra_Powerset< NNC_Polyhedron > & | y | ) | [inline] |
Parma_Polyhedra_Library::Polyhedra_Powerset< NNC_Polyhedron >::Polyhedra_Powerset | ( | const Polyhedra_Powerset< C_Polyhedron > & | y | ) | [inline] |
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 }
Parma_Polyhedra_Library::Polyhedra_Powerset< C_Polyhedron >::Polyhedra_Powerset | ( | const Polyhedra_Powerset< NNC_Polyhedron > & | y | ) | [inline] |
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 }
Parma_Polyhedra_Library::Polyhedra_Powerset< NNC_Polyhedron >::Polyhedra_Powerset | ( | const Polyhedra_Powerset< QH > & | y | ) | [inline] |
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 }
Parma_Polyhedra_Library::Polyhedra_Powerset< C_Polyhedron >::Polyhedra_Powerset | ( | const Polyhedra_Powerset< QH > & | y | ) | [inline] |
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 }
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.
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 }
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. |
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 }
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. |
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 }
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 }
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 }
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 }
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. |
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 }
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. |
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 }
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. |
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 }
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. |
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 }
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. |
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 }
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 .
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 }
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. |
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 }
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. 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 }
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 }
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 }
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::swap | ( | Polyhedra_Powerset< PH > & | y | ) | [inline] |
Swaps *this
with y
.
Definition at line 155 of file Polyhedra_Powerset.inlines.hh.
References Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::space_dim.
Referenced by Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::ascii_load(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::concatenate_assign(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::operator=(), and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::swap().
00155 { 00156 Polyhedra_Powerset& x = *this; 00157 x.Base::swap(y); 00158 std::swap(x.space_dim, y.space_dim); 00159 }
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 }
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 }
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 }
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().
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 }
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 }
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::remove_space_dimensions | ( | const Variables_Set & | to_be_removed | ) | [inline] |
Removes all the specified space dimensions.
to_be_removed | The set of Variable objects corresponding to the space dimensions to be removed. |
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 }
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 . |
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 }
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 }
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::ascii_dump | ( | ) | const |
Writes to std::cerr
an ASCII representation of *this
.
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 }
void Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::print | ( | ) | const |
Prints *this
to std::cerr
using operator<<
.
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 }
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 }
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 }
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 }
void Parma_Polyhedra_Library::Polyhedra_Powerset< NNC_Polyhedron >::poly_difference_assign | ( | const Polyhedra_Powerset< PH > & | y | ) | [inline] |
bool Parma_Polyhedra_Library::Polyhedra_Powerset< NNC_Polyhedron >::geometrically_covers | ( | const Polyhedra_Powerset< PH > & | y | ) | const [inline] |
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 }
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 }
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 }
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 }
friend class Polyhedra_Powerset [friend] |
Definition at line 443 of file Polyhedra_Powerset.defs.hh.
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. |
Definition at line 59 of file Widening_Function.inlines.hh.
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. |
Definition at line 66 of file Widening_Function.inlines.hh.
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
).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 }
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 }
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
.
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 }
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 }
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 }
dimension_type Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::space_dim [private] |
The number of dimensions of the enclosing vector space.
Definition at line 412 of file Polyhedra_Powerset.defs.hh.
Referenced by 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_dump(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::ascii_load(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::BGP99_heuristics_assign(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::BHZ03_widening_assign(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::concatenate_assign(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::map_space_dimensions(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::OK(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::operator=(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::pairwise_reduce(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::remove_higher_space_dimensions(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::remove_space_dimensions(), Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::space_dimension(), and Parma_Polyhedra_Library::Polyhedra_Powerset< PH >::swap().