Parma_Polyhedra_Library::Pointset_Powerset< PS > Class Template Reference
[C++ Language Interface]

The powerset construction instantiated on PPL pointset domains. More...

#include <Pointset_Powerset.defs.hh>

Inheritance diagram for Parma_Polyhedra_Library::Pointset_Powerset< PS >:

Inheritance graph
[legend]
Collaboration diagram for Parma_Polyhedra_Library::Pointset_Powerset< PS >:

Collaboration graph
[legend]

List of all members.

Public Types

typedef PS 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(std::ostream&) const) and sets *this accordingly. Returns true if successful, false otherwise.
template<>
 Pointset_Powerset (const Pointset_Powerset< QH > &y, Complexity_Class)
template<>
 Pointset_Powerset (const Pointset_Powerset< C_Polyhedron > &y, Complexity_Class)
template<>
 Pointset_Powerset (const Pointset_Powerset< NNC_Polyhedron > &y, Complexity_Class)
template<>
void difference_assign (const Pointset_Powerset &y)
template<>
void difference_assign (const Pointset_Powerset &y)
template<>
bool geometrically_covers (const Pointset_Powerset &y) const
template<>
bool geometrically_covers (const Pointset_Powerset &y) const
template<>
bool geometrically_equals (const Pointset_Powerset &y) const
template<>
bool geometrically_equals (const Pointset_Powerset &y) const
template<>
 Pointset_Powerset (const Pointset_Powerset< QH > &y, Complexity_Class complexity)
template<>
void difference_assign (const Pointset_Powerset &y)
template<>
bool geometrically_covers (const Pointset_Powerset &y) const
template<>
void difference_assign (const Pointset_Powerset &y)
template<>
bool geometrically_covers (const Pointset_Powerset &y) const
template<>
 Pointset_Powerset (const Pointset_Powerset< C_Polyhedron > &y, Complexity_Class)
template<>
 Pointset_Powerset (const Pointset_Powerset< NNC_Polyhedron > &y, Complexity_Class)
Constructors
 Pointset_Powerset (dimension_type num_dimensions=0, Degenerate_Element kind=UNIVERSE)
 Builds a universe (top) or empty (bottom) Pointset_Powerset.
 Pointset_Powerset (const Pointset_Powerset &y, Complexity_Class complexity=ANY_COMPLEXITY)
 Ordinary copy-constructor.
template<typename QH>
 Pointset_Powerset (const Pointset_Powerset< QH > &y, Complexity_Class complexity=ANY_COMPLEXITY)
 Conversion constructor: the type QH of the disjuncts in the source powerset is different from PS.
template<typename QH1, typename QH2, typename R>
 Pointset_Powerset (const Partially_Reduced_Product< QH1, QH2, R > &prp, Complexity_Class complexity=ANY_COMPLEXITY)
 Creates a Pointset_Powerset from a product This will be craeted as a single disjunct of type PS that approximates the product.
 Pointset_Powerset (const Constraint_System &cs)
 Creates a Pointset_Powerset with a single disjunct approximating the system of constraints cs.
 Pointset_Powerset (const Congruence_System &cgs)
 Creates a Pointset_Powerset with a single disjunct approximating the system of congruences cgs.
 Pointset_Powerset (const C_Polyhedron &ph, Complexity_Class complexity=ANY_COMPLEXITY)
 Builds a pointset_powerset out of a closed polyhedron.
 Pointset_Powerset (const NNC_Polyhedron &ph, Complexity_Class complexity=ANY_COMPLEXITY)
 Builds a pointset_powerset out of an nnc polyhedron.
 Pointset_Powerset (const Grid &gr, Complexity_Class complexity=ANY_COMPLEXITY)
 Builds a pointset_powerset out of a grid.
template<typename T>
 Pointset_Powerset (const Octagonal_Shape< T > &os, Complexity_Class complexity=ANY_COMPLEXITY)
 Builds a pointset_powerset out of an octagonal shape.
template<typename T>
 Pointset_Powerset (const BD_Shape< T > &bds, Complexity_Class complexity=ANY_COMPLEXITY)
 Builds a pointset_powerset out of a bd shape.
template<typename Interval>
 Pointset_Powerset (const Box< Interval > &box, Complexity_Class complexity=ANY_COMPLEXITY)
 Builds a pointset_powerset out of a box.
Member Functions that Do Not Modify the Pointset_Powerset
dimension_type space_dimension () const
 Returns the dimension of the vector space enclosing *this.
dimension_type affine_dimension () const
 Returns the dimension of the vector space enclosing *this.
bool is_empty () const
 Returns true if and only if *this is an empty powerset.
bool is_universe () const
 Returns true if and only if *this is the top element of the powerser lattice.
bool is_topologically_closed () const
 Returns true if and only if all the disjuncts in *this are topologically closed.
bool is_bounded () const
 Returns true if and only if all elements in *this are bounded.
bool is_disjoint_from (const Pointset_Powerset &y) const
 Returns true if and only if *this and y are disjoint.
bool is_discrete () const
 Returns true if and only if *this is discrete.
bool constrains (Variable var) const
 Returns true if and only if var is constrained in *this.
bool bounds_from_above (const Linear_Expression &expr) const
 Returns true if and only if expr is bounded from above in *this.
bool bounds_from_below (const Linear_Expression &expr) const
 Returns true if and only if expr is bounded from below in *this.
bool maximize (const Linear_Expression &expr, Coefficient &sup_n, Coefficient &sup_d, bool &maximum) const
 Returns true if and only if *this is not empty and expr is bounded from above in *this, in which case the supremum value is computed.
bool maximize (const Linear_Expression &expr, Coefficient &sup_n, Coefficient &sup_d, bool &maximum, Generator &g) const
 Returns true if and only if *this is not empty and expr is bounded from above in *this, in which case the supremum value and a point where expr reaches it are computed.
bool minimize (const Linear_Expression &expr, Coefficient &inf_n, Coefficient &inf_d, bool &minimum) const
 Returns true if and only if *this is not empty and expr is bounded from below in *this, in which case the infimum value is computed.
bool minimize (const Linear_Expression &expr, Coefficient &inf_n, Coefficient &inf_d, bool &minimum, Generator &g) const
 Returns true if and only if *this is not empty and expr is bounded from below in *this, in which case the infimum value and a point where expr reaches it are computed.
bool geometrically_covers (const Pointset_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 Pointset_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.
bool contains (const Pointset_Powerset &y) const
bool strictly_contains (const Pointset_Powerset &y) const
bool contains_integer_point () const
 Returns true if and only if *this contains at least one integer point.
Poly_Con_Relation relation_with (const Constraint &c) const
 Returns the relations holding between the powerset *this and the constraint c.
Poly_Gen_Relation relation_with (const Generator &g) const
 Returns the relations holding between the powerset *this and the generator g.
Poly_Con_Relation relation_with (const Congruence &cg) const
 Returns the relations holding between the powerset *this and the congruence c.
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.
int32_t hash_code () const
 Returns a 32-bit hash code for *this.
bool OK () const
 Checks if all the invariants are satisfied.
Space Dimension Preserving Member Functions that May Modify the Pointset_Powerset
void add_disjunct (const PS &ph)
 Adds to *this the disjunct ph.
void add_constraint (const Constraint &c)
 Intersects *this with constraint c.
void refine_with_constraint (const Constraint &c)
 Use the constraint c to refine *this.
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.
void refine_with_constraints (const Constraint_System &cs)
 Use the constraints in cs to refine *this.
bool add_constraints_and_minimize (const Constraint_System &cs)
 Intersects *this with the constraints in cs, minimizing the result.
void add_congruence (const Congruence &c)
 Intersects *this with congruence c.
void refine_with_congruence (const Congruence &cg)
 Use the congruence cg to refine *this.
bool add_congruence_and_minimize (const Congruence &c)
 Intersects *this with the congruence c, minimizing the result.
void add_congruences (const Congruence_System &cgs)
 Intersects *this with the congruences in cgs.
void refine_with_congruences (const Congruence_System &cgs)
 Use the congruences in cgs to refine *this.
bool add_congruences_and_minimize (const Congruence_System &cs)
 Intersects *this with the congruences in cs, minimizing the result.
void unconstrain (Variable var)
 Computes the cylindrification of *this with respect to space dimension var, assigning the result to *this.
void unconstrain (const Variables_Set &to_be_unconstrained)
 Computes the cylindrification of *this with respect to the set of space dimensions to_be_unconstrained, assigning the result to *this.
void topological_closure_assign ()
 Assigns to *this its topological closure.
void intersection_assign (const Pointset_Powerset &y)
 Assigns to *this the intersection of *this and y.
bool intersection_assign_and_minimize (const Pointset_Powerset &y)
 Assigns to *this the intersection of *this and y.
void difference_assign (const Pointset_Powerset &y)
 Assigns to *this an (a smallest) over-approximation as a powerset of the disjunct domain of the set-theoretical difference of *this and y.
bool simplify_using_context_assign (const Pointset_Powerset &y)
 Assigns to *this a meet-preserving simplification of *this with respect to y. If false is returned, then the intersection is empty.
void affine_image (Variable var, const Linear_Expression &expr, Coefficient_traits::const_reference denominator=Coefficient_one())
 Assigns to *this the affine image of *this under the function mapping variable var to the affine expression specified by expr and denominator.
void affine_preimage (Variable var, const Linear_Expression &expr, Coefficient_traits::const_reference denominator=Coefficient_one())
 Assigns to *this the affine preimage of *this under the function mapping variable var to the affine expression specified by expr and denominator.
void generalized_affine_image (Variable var, Relation_Symbol relsym, const Linear_Expression &expr, Coefficient_traits::const_reference denominator=Coefficient_one())
 Assigns to *this the image of *this with respect to the generalized affine relation $\mathrm{var}' \relsym \frac{\mathrm{expr}}{\mathrm{denominator}}$, where $\mathord{\relsym}$ is the relation symbol encoded by relsym.
void generalized_affine_preimage (Variable var, Relation_Symbol relsym, const Linear_Expression &expr, Coefficient_traits::const_reference denominator=Coefficient_one())
 Assigns to *this the preimage of *this with respect to the generalized affine relation $\mathrm{var}' \relsym \frac{\mathrm{expr}}{\mathrm{denominator}}$, where $\mathord{\relsym}$ is the relation symbol encoded by relsym.
void generalized_affine_image (const Linear_Expression &lhs, Relation_Symbol relsym, const Linear_Expression &rhs)
 Assigns to *this the image of *this with respect to the generalized affine relation $\mathrm{lhs}' \relsym \mathrm{rhs}$, where $\mathord{\relsym}$ is the relation symbol encoded by relsym.
void generalized_affine_preimage (const Linear_Expression &lhs, Relation_Symbol relsym, const Linear_Expression &rhs)
 Assigns to *this the preimage of *this with respect to the generalized affine relation $\mathrm{lhs}' \relsym \mathrm{rhs}$, where $\mathord{\relsym}$ is the relation symbol encoded by relsym.
void bounded_affine_image (Variable var, const Linear_Expression &lb_expr, const Linear_Expression &ub_expr, Coefficient_traits::const_reference denominator=Coefficient_one())
 Assigns to *this the image of *this with respect to the bounded affine relation $\frac{\mathrm{lb\_expr}}{\mathrm{denominator}} \leq \mathrm{var}' \leq \frac{\mathrm{ub\_expr}}{\mathrm{denominator}}$.
void bounded_affine_preimage (Variable var, const Linear_Expression &lb_expr, const Linear_Expression &ub_expr, Coefficient_traits::const_reference denominator=Coefficient_one())
 Assigns to *this the preimage of *this with respect to the bounded affine relation $\frac{\mathrm{lb\_expr}}{\mathrm{denominator}} \leq \mathrm{var}' \leq \frac{\mathrm{ub\_expr}}{\mathrm{denominator}}$.
void time_elapse_assign (const Pointset_Powerset &y)
 Assigns to *this the result of computing the time-elapse between *this and y.
void pairwise_reduce ()
 Assign to *this the result of (recursively) merging together the pairs of disjuncts whose upper-bound is the same as their set-theoretical union.
template<typename Widening>
void BGP99_extrapolation_assign (const Pointset_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 Pointset_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
Pointset_Powersetoperator= (const Pointset_Powerset &y)
 The assignment operator (*this and y can be dimension-incompatible).
template<typename QH>
Pointset_Powersetoperator= (const Pointset_Powerset< QH > &y)
 Conversion assignment: the type QH of the disjuncts in the source powerset is different from PS (*this and y can be dimension-incompatible).
void swap (Pointset_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 disjunct 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 disjuncts in *this in the new space.
void concatenate_assign (const Pointset_Powerset &y)
 Assigns to *this the concatenation of *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.
void expand_space_dimension (Variable var, dimension_type m)
 Creates m copies of the space dimension corresponding to var.
void fold_space_dimensions (const Variables_Set &to_be_folded, Variable var)
 Folds the space dimensions in to_be_folded into var.

Static Public Member Functions

static dimension_type max_space_dimension ()
 Returns the maximum space dimension a Pointset_Powerset<PS> can handle.

Private Types

typedef Determinate< PS > CS
typedef Powerset< CSBase
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

bool intersection_preserving_enlarge_element (PS &to_be_enlarged) const
 Assigns to to_be_enlarged a powerset meet-preserving enlargement of itself with respect to *this. If false is returned, then the intersection is empty.
template<typename Widening>
void BGP99_heuristics_assign (const Pointset_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 disjuncts.
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 dijsuncts 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 Pointset_Powerset< NNC_Polyhedron >

Related Functions

(Note that these are not member functions.)

template<typename PH>
Widening_Function< PH > widen_fun_ref (void(PH::*wm)(const PH &, unsigned *))
 Wraps a widening method into a function object.
template<typename PH, typename CS>
Limited_Widening_Function< PH, CSwiden_fun_ref (void(PH::*lwm)(const PH &, const CS &, unsigned *), const CS &cs)
 Wraps a limited widening method into a function object.
template<typename PS>
std::pair< PS,
Pointset_Powerset
< NNC_Polyhedron > > 
linear_partition (const PS &p, const PS &q)
 Partitions q with respect to p.
bool check_containment (const NNC_Polyhedron &ph, const Pointset_Powerset< NNC_Polyhedron > &ps)
 Returns true if and only if the union of the NNC polyhedra in ps contains the NNC polyhedron ph.
std::pair< Grid,
Pointset_Powerset< Grid > > 
approximate_partition (const Grid &p, const Grid &q, bool &finite_partition)
 Partitions the grid q with respect to grid p if and only if such a partition is finite.
bool check_containment (const Grid &ph, const Pointset_Powerset< Grid > &ps)
 Returns true if and only if the union of the grids ps contains the grid g.
template<typename PS>
bool check_containment (const PS &ph, const Pointset_Powerset< PS > &ps)
 Returns true if and only if the union of the objects in ps contains ph.
template<typename PS>
void swap (Parma_Polyhedra_Library::Pointset_Powerset< PS > &x, Parma_Polyhedra_Library::Pointset_Powerset< PS > &y)
 Specializes std::swap.
template<>
bool check_containment (const C_Polyhedron &ph, const Pointset_Powerset< C_Polyhedron > &ps)
template<typename PS>
void linear_partition_aux (const Constraint &c, PS &qq, Pointset_Powerset< NNC_Polyhedron > &r)
 Partitions polyhedron qq according to constraint c.
bool approximate_partition_aux (const PPL::Congruence &c, PPL::Grid &qq, PPL::Pointset_Powerset< PPL::Grid > &r)
 Uses the congruence c to approximately partition the grid qq.


Detailed Description

template<typename PS>
class Parma_Polyhedra_Library::Pointset_Powerset< PS >

The powerset construction instantiated on PPL pointset domains.

Warning:
At present, the supported instantiations for the disjunct domain template PS are the simple pointset domains: C_Polyhedron, NNC_Polyhedron, Grid, Octagonal_Shape<T>, BD_Shape<T>, Box<T>.

Definition at line 61 of file Pointset_Powerset.defs.hh.


Member Typedef Documentation

template<typename PS>
typedef PS Parma_Polyhedra_Library::Pointset_Powerset< PS >::element_type

Definition at line 65 of file Pointset_Powerset.defs.hh.

template<typename PS>
typedef Determinate<PS> Parma_Polyhedra_Library::Pointset_Powerset< PS >::CS [private]

Definition at line 68 of file Pointset_Powerset.defs.hh.

template<typename PS>
typedef Powerset<CS> Parma_Polyhedra_Library::Pointset_Powerset< PS >::Base [private]

Definition at line 69 of file Pointset_Powerset.defs.hh.

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

Definition at line 1236 of file Pointset_Powerset.defs.hh.

A bidirectional const_iterator on the disjuncts of a Powerset element.

Reimplemented from Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >.

Definition at line 1237 of file Pointset_Powerset.defs.hh.

The reverse iterator type built from Powerset::iterator.

Reimplemented from Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >.

Definition at line 1238 of file Pointset_Powerset.defs.hh.

The reverse iterator type built from Powerset::const_iterator.

Reimplemented from Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >.

Definition at line 1239 of file Pointset_Powerset.defs.hh.

template<typename PS>
typedef Base::Sequence Parma_Polyhedra_Library::Pointset_Powerset< PS >::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< PS > >.

Definition at line 1253 of file Pointset_Powerset.defs.hh.

Alias for the low-level iterator on the disjuncts.

Reimplemented from Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >.

Definition at line 1254 of file Pointset_Powerset.defs.hh.

Alias for the low-level const_iterator on the disjuncts.

Reimplemented from Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >.

Definition at line 1255 of file Pointset_Powerset.defs.hh.


Constructor & Destructor Documentation

template<typename PS>
Parma_Polyhedra_Library::Pointset_Powerset< PS >::Pointset_Powerset ( dimension_type  num_dimensions = 0,
Degenerate_Element  kind = UNIVERSE 
) [inline, explicit]

Builds a universe (top) or empty (bottom) Pointset_Powerset.

Parameters:
num_dimensions The number of dimensions of the vector space enclosing the powerset;
kind Specifies whether the universe or the empty powerset has to be built.

Definition at line 53 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::sequence, and Parma_Polyhedra_Library::UNIVERSE.

00055   : Base(), space_dim(num_dimensions) {
00056   Pointset_Powerset& x = *this;
00057   if (kind == UNIVERSE)
00058     x.sequence.push_back(Determinate<PS>(PS(num_dimensions, kind)));
00059   assert(x.OK());
00060 }

template<typename PS>
Parma_Polyhedra_Library::Pointset_Powerset< PS >::Pointset_Powerset ( const Pointset_Powerset< PS > &  y,
Complexity_Class  complexity = ANY_COMPLEXITY 
) [inline]

Ordinary copy-constructor.

The complexity argument is ignored.

Definition at line 64 of file Pointset_Powerset.inlines.hh.

00066   : Base(y), space_dim(y.space_dim) {
00067 }

template<typename PS>
template<typename QH>
Parma_Polyhedra_Library::Pointset_Powerset< PS >::Pointset_Powerset ( const Pointset_Powerset< QH > &  y,
Complexity_Class  complexity = ANY_COMPLEXITY 
) [inline, explicit]

Conversion constructor: the type QH of the disjuncts in the source powerset is different from PS.

Parameters:
y The powerset to be used to build the new powerset.
complexity The maximal complexity of any algorithms used.

Definition at line 76 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >::begin(), Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >::end(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00078   : Base(), space_dim(y.space_dimension()) {
00079   Pointset_Powerset& x = *this;
00080   for (typename Pointset_Powerset<QH>::const_iterator i = y.begin(),
00081          y_end = y.end(); i != y_end; ++i)
00082     x.sequence.push_back(Determinate<PS>(PS(i->element(), complexity)));
00083   // Note: this might be non-reduced even when `y' is known to be
00084   // omega-reduced, because the constructor of PS may have made
00085   // different QH elements to become comparable.
00086   x.reduced = false;
00087   assert(x.OK());
00088 }

template<typename PS>
template<typename QH1, typename QH2, typename R>
Parma_Polyhedra_Library::Pointset_Powerset< PS >::Pointset_Powerset ( const Partially_Reduced_Product< QH1, QH2, R > &  prp,
Complexity_Class  complexity = ANY_COMPLEXITY 
) [inline, explicit]

Creates a Pointset_Powerset from a product This will be craeted as a single disjunct of type PS that approximates the product.

Definition at line 118 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::ANY_COMPLEXITY, Parma_Polyhedra_Library::Partially_Reduced_Product< D1, D2, R >::is_empty(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00120   : Base(), space_dim(prp.space_dimension()) {
00121   Pointset_Powerset& x = *this;
00122   if (complexity == ANY_COMPLEXITY) {
00123     if (prp.is_empty())
00124       return;
00125   }
00126   else
00127     x.reduced = false;
00128   x.sequence.push_back(Determinate<PS>(PS(prp, complexity)));
00129   x.reduced = false;
00130   assert(OK());
00131 }

template<typename PS>
Parma_Polyhedra_Library::Pointset_Powerset< PS >::Pointset_Powerset ( const Constraint_System cs  )  [inline, explicit]

Creates a Pointset_Powerset with a single disjunct approximating the system of constraints cs.

Definition at line 168 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK().

00169   : Base(Determinate<PS>(cs)), space_dim(cs.space_dimension()) {
00170   assert(OK());
00171 }

template<typename PS>
Parma_Polyhedra_Library::Pointset_Powerset< PS >::Pointset_Powerset ( const Congruence_System cgs  )  [inline, explicit]

Creates a Pointset_Powerset with a single disjunct approximating the system of congruences cgs.

Definition at line 175 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK().

00176   : Base(Determinate<PS>(cgs)), space_dim(cgs.space_dimension()) {
00177   assert(OK());
00178 }

template<typename PS>
Parma_Polyhedra_Library::Pointset_Powerset< PS >::Pointset_Powerset ( const C_Polyhedron ph,
Complexity_Class  complexity = ANY_COMPLEXITY 
) [inline, explicit]

Builds a pointset_powerset out of a closed polyhedron.

Builds a powerset that is either empty (if the polyhedron is found to be empty) or contains a single disjunct approximating the polyhedron; this must only use algorithms that do not exceed the specified complexity. The powerset inherits the space dimension of the polyhedron.

Parameters:
ph The closed polyhedron to be used to build the powerset.
complexity The maximal complexity of any algorithms used.
Exceptions:
std::length_error Thrown if the space dimension of ph exceeds the maximum allowed space dimension.

Definition at line 71 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::ANY_COMPLEXITY, Parma_Polyhedra_Library::Polyhedron::is_empty(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00073   : Base(), space_dim(ph.space_dimension()) {
00074   Pointset_Powerset& x = *this;
00075   if (complexity == ANY_COMPLEXITY) {
00076     if (ph.is_empty())
00077       return;
00078   }
00079   else
00080     x.reduced = false;
00081   x.sequence.push_back(Determinate<PS>(PS(ph, complexity)));
00082   x.reduced = false;
00083   assert(OK());
00084 }

template<typename PS>
Parma_Polyhedra_Library::Pointset_Powerset< PS >::Pointset_Powerset ( const NNC_Polyhedron ph,
Complexity_Class  complexity = ANY_COMPLEXITY 
) [inline, explicit]

Builds a pointset_powerset out of an nnc polyhedron.

Builds a powerset that is either empty (if the polyhedron is found to be empty) or contains a single disjunct approximating the polyhedron; this must only use algorithms that do not exceed the specified complexity. The powerset inherits the space dimension of the polyhedron.

Parameters:
ph The closed polyhedron to be used to build the powerset.
complexity The maximal complexity of any algorithms used.
Exceptions:
std::length_error Thrown if the space dimension of ph exceeds the maximum allowed space dimension.

Definition at line 88 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::ANY_COMPLEXITY, Parma_Polyhedra_Library::Polyhedron::is_empty(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00090   : Base(), space_dim(ph.space_dimension()) {
00091   Pointset_Powerset& x = *this;
00092   if (complexity == ANY_COMPLEXITY) {
00093     if (ph.is_empty())
00094       return;
00095   }
00096   else
00097     x.reduced = false;
00098   x.sequence.push_back(Determinate<PS>(PS(ph, complexity)));
00099   assert(OK());
00100 }

template<typename PS>
Parma_Polyhedra_Library::Pointset_Powerset< PS >::Pointset_Powerset ( const Grid gr,
Complexity_Class  complexity = ANY_COMPLEXITY 
) [inline, explicit]

Builds a pointset_powerset out of a grid.

If the grid is nonempty, builds a powerset containing a single disjunct approximating the grid. Builds the empty powerset otherwise. The powerset inherits the space dimension of the grid.

Parameters:
gr The grid to be used to build the powerset.
complexity This argument is ignored.
Exceptions:
std::length_error Thrown if the space dimension of gr exceeds the maximum allowed space dimension.

Definition at line 104 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Grid::is_empty(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), and Parma_Polyhedra_Library::Powerset< D >::sequence.

00106   : Base(), space_dim(gr.space_dimension()) {
00107   Pointset_Powerset& x = *this;
00108   if (!gr.is_empty()) {
00109     x.sequence.push_back(Determinate<PS>(PS(gr)));
00110   }
00111   assert(OK());
00112 }

template<typename PS>
template<typename T>
Parma_Polyhedra_Library::Pointset_Powerset< PS >::Pointset_Powerset ( const Octagonal_Shape< T > &  os,
Complexity_Class  complexity = ANY_COMPLEXITY 
) [inline, explicit]

Builds a pointset_powerset out of an octagonal shape.

If the octagonal shape is nonempty, builds a powerset containing a single disjunct approximating the octagonal shape. Builds the empty powerset otherwise. The powerset inherits the space dimension of the octagonal shape.

Parameters:
os The octagonal shape to be used to build the powerset.
complexity This argument is ignored.
Exceptions:
std::length_error Thrown if the space dimension of os exceeds the maximum allowed space dimension.

Definition at line 146 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Octagonal_Shape< T >::is_empty(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), and Parma_Polyhedra_Library::Powerset< D >::sequence.

00148   : Base(), space_dim(os.space_dimension()) {
00149   Pointset_Powerset& x = *this;
00150   if (!os.is_empty())
00151     x.sequence.push_back(Determinate<PS>(PS(os)));
00152   assert(OK());
00153 }

template<typename PS>
template<typename T>
Parma_Polyhedra_Library::Pointset_Powerset< PS >::Pointset_Powerset ( const BD_Shape< T > &  bds,
Complexity_Class  complexity = ANY_COMPLEXITY 
) [inline, explicit]

Builds a pointset_powerset out of a bd shape.

If the bd shape is nonempty, builds a powerset containing a single disjunct approximating the bd shape. Builds the empty powerset otherwise. The powerset inherits the space dimension of the bd shape.

Parameters:
bds The bd shape to be used to build the powerset.
complexity This argument is ignored.
Exceptions:
std::length_error Thrown if the space dimension of bdss exceeds the maximum allowed space dimension.

Definition at line 157 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::is_empty(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), and Parma_Polyhedra_Library::Powerset< D >::sequence.

00159   : Base(), space_dim(bds.space_dimension()) {
00160   Pointset_Powerset& x = *this;
00161   if (!bds.is_empty())
00162     x.sequence.push_back(Determinate<PS>(PS(bds)));
00163   assert(OK());
00164 }

template<typename PS>
template<typename Interval>
Parma_Polyhedra_Library::Pointset_Powerset< PS >::Pointset_Powerset ( const Box< Interval > &  box,
Complexity_Class  complexity = ANY_COMPLEXITY 
) [inline, explicit]

Builds a pointset_powerset out of a box.

If the box is nonempty, builds a powerset containing a single disjunct approximating the box. Builds the empty powerset otherwise. The powerset inherits the space dimension of the box.

Parameters:
box The box to be used to build the powerset.
complexity This argument is ignored.
Exceptions:
std::length_error Thrown if the space dimension of box exceeds the maximum allowed space dimension.

Definition at line 135 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), and Parma_Polyhedra_Library::Powerset< D >::sequence.

00137   : Base(), space_dim(box.space_dimension()) {
00138   Pointset_Powerset& x = *this;
00139   if (!box.is_empty())
00140     x.sequence.push_back(Determinate<PS>(PS(box)));
00141   assert(OK());
00142 }

Definition at line 60 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >::begin(), Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >::end(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >::reduced, Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00062   : Base(), space_dim(y.space_dimension()) {
00063   Pointset_Powerset& x = *this;
00064   for (typename Pointset_Powerset<QH>::const_iterator i = y.begin(),
00065          y_end = y.end(); i != y_end; ++i)
00066     x.sequence.push_back(Determinate<NNC_Polyhedron>
00067                          (NNC_Polyhedron(i->element(), complexity)));
00068   // FIXME: the following is a bug!
00069   x.reduced = y.reduced;
00070   assert(x.OK());
00071 }

Definition at line 296 of file Pointset_Powerset.cc.

References Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >::begin(), Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >::end(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >::reduced, Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00298   : Base(), space_dim(y.space_dimension()) {
00299   Pointset_Powerset& x = *this;
00300   for (Pointset_Powerset<C_Polyhedron>::const_iterator i = y.begin(),
00301          y_end = y.end(); i != y_end; ++i)
00302     x.sequence.push_back(Determinate<NNC_Polyhedron>
00303                          (NNC_Polyhedron(i->element())));
00304   x.reduced = y.reduced;
00305   assert(x.OK());
00306 }

Definition at line 311 of file Pointset_Powerset.cc.

References Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >::begin(), Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >::end(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00313   : Base(), space_dim(y.space_dimension()) {
00314   Pointset_Powerset& x = *this;
00315   for (Pointset_Powerset<NNC_Polyhedron>::const_iterator i = y.begin(),
00316          y_end = y.end(); i != y_end; ++i)
00317     x.sequence.push_back(Determinate<C_Polyhedron>
00318                          (C_Polyhedron(i->element())));
00319 
00320   // Note: this might be non-reduced even when `y' is known to be
00321   // omega-reduced, because the constructor of C_Polyhedron, by
00322   // enforcing topological closure, may have made different elements
00323   // comparable.
00324   x.reduced = false;
00325   assert(x.OK());
00326 }


Member Function Documentation

template<typename PS>
dimension_type Parma_Polyhedra_Library::Pointset_Powerset< PS >::max_space_dimension (  )  [inline, static]

Returns the maximum space dimension a Pointset_Powerset<PS> can handle.

Definition at line 47 of file Pointset_Powerset.inlines.hh.

00047                                            {
00048   return PS::max_space_dimension();
00049 }

template<typename PS>
dimension_type Parma_Polyhedra_Library::Pointset_Powerset< PS >::space_dimension (  )  const [inline]

template<typename PS>
dimension_type Parma_Polyhedra_Library::Pointset_Powerset< PS >::affine_dimension (  )  const [inline]

Returns the dimension of the vector space enclosing *this.

Definition at line 546 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Polyhedron::add_constraint(), Parma_Polyhedra_Library::Polyhedron::affine_dimension(), Parma_Polyhedra_Library::Constraint_System::begin(), Parma_Polyhedra_Library::EMPTY, Parma_Polyhedra_Library::Constraint_System::end(), Parma_Polyhedra_Library::Constraint::is_equality(), Parma_Polyhedra_Library::Polyhedron::poly_hull_assign(), Parma_Polyhedra_Library::Powerset< D >::sequence, and Parma_Polyhedra_Library::Pointset_Powerset< PS >::space_dim.

00546                                               {
00547   // The affine dimension of the powerset is the affine dimension of
00548   // the smallest vector space in which it can be embedded.
00549   const Pointset_Powerset& x = *this;
00550   C_Polyhedron x_ph(space_dim, EMPTY);
00551 
00552   for (Sequence_const_iterator si = x.sequence.begin(),
00553          s_end = x.sequence.end(); si != s_end; ++si) {
00554     PS pi(si->element());
00555     if (!pi.is_empty()) {
00556       C_Polyhedron phi(space_dim);
00557       const Constraint_System& cs = pi.minimized_constraints();
00558       for (Constraint_System::const_iterator i = cs.begin(),
00559              cs_end = cs.end(); i != cs_end; ++i) {
00560         const Constraint& c = *i;
00561         if (c.is_equality())
00562           phi.add_constraint(c);
00563       }
00564       x_ph.poly_hull_assign(phi);
00565     }
00566   }
00567 
00568   return x_ph.affine_dimension();
00569 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::is_empty (  )  const [inline]

Returns true if and only if *this is an empty powerset.

Definition at line 595 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::sequence.

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::constrains(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::intersection_assign_and_minimize(), and Parma_Polyhedra_Library::Pointset_Powerset< PS >::simplify_using_context_assign().

00595                                       {
00596   const Pointset_Powerset& x = *this;
00597   for (Sequence_const_iterator si = x.sequence.begin(),
00598          s_end = x.sequence.end(); si != s_end; ++si)
00599     if (!si->element().is_empty())
00600       return false;
00601   return true;
00602 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::is_universe (  )  const [inline]

Returns true if and only if *this is the top element of the powerser lattice.

Definition at line 573 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Powerset< D >::is_omega_reduced(), Parma_Polyhedra_Library::Powerset< D >::size(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::space_dimension(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::swap(), and Parma_Polyhedra_Library::UNIVERSE.

00573                                          {
00574   const Pointset_Powerset& x = *this;
00575   // Exploit omega-reduction, if already computed.
00576   if (x.is_omega_reduced())
00577     return x.size() == 1 && x.begin()->element().is_universe();
00578 
00579   // A powerset is universe iff one of its disjuncts is.
00580   for (const_iterator x_i = x.begin(), x_end = x.end(); x_i != x_end; ++x_i)
00581     if (x_i->element().is_universe()) {
00582       // Speculative omega-reduction, if it is worth.
00583       if (x.size() > 1) {
00584         Pointset_Powerset<PS> universe(x.space_dimension(), UNIVERSE);
00585         Pointset_Powerset& xx = const_cast<Pointset_Powerset&>(x);
00586         xx.swap(universe);
00587       }
00588       return true;
00589     }
00590   return false;
00591 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::is_topologically_closed (  )  const [inline]

Returns true if and only if all the disjuncts in *this are topologically closed.

Definition at line 617 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), and Parma_Polyhedra_Library::Powerset< D >::sequence.

00617                                                      {
00618   const Pointset_Powerset& x = *this;
00619   // The powerset must be omega-reduced before checking
00620   // topological closure.
00621   x.omega_reduce();
00622   for (Sequence_const_iterator si = x.sequence.begin(),
00623          s_end = x.sequence.end(); si != s_end; ++si)
00624     if (!si->element().is_topologically_closed())
00625       return false;
00626   return true;
00627 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::is_bounded (  )  const [inline]

Returns true if and only if all elements in *this are bounded.

Definition at line 631 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::sequence.

00631                                         {
00632   const Pointset_Powerset& x = *this;
00633   for (Sequence_const_iterator si = x.sequence.begin(),
00634          s_end = x.sequence.end(); si != s_end; ++si)
00635     if (!si->element().is_bounded())
00636       return false;
00637   return true;
00638 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::is_disjoint_from ( const Pointset_Powerset< PS > &  y  )  const [inline]

Returns true if and only if *this and y are disjoint.

Exceptions:
std::invalid_argument Thrown if x and y are topology-incompatible or dimension-incompatible.

Definition at line 666 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::sequence.

00666                                                                         {
00667   const Pointset_Powerset& x = *this;
00668   for (Sequence_const_iterator si = x.sequence.begin(),
00669          xs_end = x.sequence.end(); si != xs_end; ++si) {
00670     const PS& pi = si->element();
00671     for (Sequence_const_iterator sj = y.sequence.begin(),
00672            ys_end = y.sequence.end(); sj != ys_end; ++sj) {
00673       const PS& pj = sj->element();
00674       if (!pi.is_disjoint_from(pj))
00675         return false;
00676     }
00677   }
00678   return true;
00679 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::is_discrete (  )  const [inline]

Returns true if and only if *this is discrete.

Definition at line 606 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::sequence.

00606                                          {
00607   const Pointset_Powerset& x = *this;
00608   for (Sequence_const_iterator si = x.sequence.begin(),
00609          s_end = x.sequence.end(); si != s_end; ++si)
00610     if (!si->element().is_discrete())
00611       return false;
00612   return true;
00613 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::constrains ( Variable  var  )  const [inline]

Returns true if and only if var is constrained in *this.

Exceptions:
std::invalid_argument Thrown if var is not a space dimension of *this.
Note:
A variable is constrained if there exists a non-redundant disjunct that is constraining the variable: this definition relies on the powerset lattice structure and may be somewhat different from the geometric intuition. For instance, variable $x$ is constrained in the powerset

\[ \mathit{ps} = \bigl\{ \{ x \geq 0 \}, \{ x \leq 0 \} \bigr\}, \]

even though $\mathit{ps}$ is geometrically equal to the whole vector space.

Definition at line 642 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::is_empty(), Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::space_dimension(), and Parma_Polyhedra_Library::Variable::space_dimension().

00642                                                     {
00643   const Pointset_Powerset& x = *this;
00644   // `var' should be one of the dimensions of the powerset.
00645   const dimension_type var_space_dim = var.space_dimension();
00646   if (x.space_dimension() < var_space_dim) {
00647     std::ostringstream s;
00648     s << "PPL::Pointset_Powerset<PS>::constrains(v):\n"
00649       << "this->space_dimension() == " << x.space_dimension() << ", "
00650       << "v.space_dimension() == " << var_space_dim << ".";
00651     throw std::invalid_argument(s.str());
00652   }
00653   // omega_reduction needed, since a redundant disjunct may constrain var.
00654   x.omega_reduce();
00655   // An empty powerset constrains all variables.
00656   if (x.is_empty())
00657     return true;
00658   for (const_iterator x_i = x.begin(), x_end = x.end(); x_i != x_end; ++x_i)
00659     if (x_i->element().constrains(var))
00660       return true;
00661   return false;
00662 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::bounds_from_above ( const Linear_Expression expr  )  const [inline]

Returns true if and only if expr is bounded from above in *this.

Exceptions:
std::invalid_argument Thrown if expr and *this are dimension-incompatible.

Definition at line 916 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), and Parma_Polyhedra_Library::Powerset< D >::sequence.

00916                                                        {
00917   const Pointset_Powerset& x = *this;
00918   x.omega_reduce();
00919   for (Sequence_const_iterator si = x.sequence.begin(),
00920          s_end = x.sequence.end(); si != s_end; ++si)
00921     if (!si->element().bounds_from_above(expr))
00922       return false;
00923   return true;
00924 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::bounds_from_below ( const Linear_Expression expr  )  const [inline]

Returns true if and only if expr is bounded from below in *this.

Exceptions:
std::invalid_argument Thrown if expr and *this are dimension-incompatible.

Definition at line 929 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), and Parma_Polyhedra_Library::Powerset< D >::sequence.

00929                                                        {
00930   const Pointset_Powerset& x = *this;
00931   x.omega_reduce();
00932   for (Sequence_const_iterator si = x.sequence.begin(),
00933          s_end = x.sequence.end(); si != s_end; ++si)
00934     if (!si->element().bounds_from_below(expr))
00935       return false;
00936   return true;
00937 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::maximize ( const Linear_Expression expr,
Coefficient sup_n,
Coefficient sup_d,
bool &  maximum 
) const [inline]

Returns true if and only if *this is not empty and expr is bounded from above in *this, in which case the supremum value is computed.

Parameters:
expr The linear expression to be maximized subject to *this;
sup_n The numerator of the supremum value;
sup_d The denominator of the supremum value;
maximum true if and only if the supremum is also the maximum value.
Exceptions:
std::invalid_argument Thrown if expr and *this are dimension-incompatible.
If *this is empty or expr is not bounded from above, false is returned and sup_n, sup_d and maximum are left untouched.

Definition at line 941 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), Parma_Polyhedra_Library::Powerset< D >::sequence, and TEMP_INTEGER.

00944                                                      {
00945   const Pointset_Powerset& x = *this;
00946   x.omega_reduce();
00947   bool first = true;
00948 
00949   Coefficient supt_n = 0;
00950   Coefficient supt_d = 1;
00951   bool maxt = 0;
00952 
00953   Coefficient supi_n = 0;
00954   Coefficient supi_d = 1;
00955   bool maxi = 0;
00956   TEMP_INTEGER(tmp);
00957 
00958   for (Sequence_const_iterator si = x.sequence.begin(),
00959          s_end = x.sequence.end(); si != s_end; ++si) {
00960     if (!si->element().maximize(expr, supi_n, supi_d, maxi))
00961       return false;
00962     else
00963       if (first) {
00964         first = false;
00965         supt_n = supi_n;
00966         supt_d = supi_d;
00967         maxt = maxi;
00968       }
00969       else {
00970         tmp = (supt_n * supi_d) - (supi_n * supt_d);
00971         if (tmp < 0) {
00972           supt_n = supi_n;
00973           supt_d = supi_d;
00974           maxt = maxi;
00975         }
00976         else if (tmp == 0)
00977           maxt = maxt || maxi;
00978       }
00979   }
00980   sup_n = supt_n;
00981   sup_d = supt_d;
00982   maximum = maxt;
00983   return true;
00984 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::maximize ( const Linear_Expression expr,
Coefficient sup_n,
Coefficient sup_d,
bool &  maximum,
Generator g 
) const [inline]

Returns true if and only if *this is not empty and expr is bounded from above in *this, in which case the supremum value and a point where expr reaches it are computed.

Parameters:
expr The linear expression to be maximized subject to *this;
sup_n The numerator of the supremum value;
sup_d The denominator of the supremum value;
maximum true if and only if the supremum is also the maximum value;
g When maximization succeeds, will be assigned the point or closure point where expr reaches its supremum value.
Exceptions:
std::invalid_argument Thrown if expr and *this are dimension-incompatible.
If *this is empty or expr is not bounded from above, false is returned and sup_n, sup_d, maximum and g are left untouched.

Definition at line 988 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), Parma_Polyhedra_Library::Powerset< D >::sequence, and TEMP_INTEGER.

00992                                                     {
00993   const Pointset_Powerset& x = *this;
00994   x.omega_reduce();
00995   bool first = true;
00996 
00997   Coefficient supt_n = 0;
00998   Coefficient supt_d = 1;
00999   bool maxt = 0;
01000   Generator gt = point();
01001 
01002   Coefficient supi_n = 0;
01003   Coefficient supi_d = 1;
01004   bool maxi = 0;
01005   Generator gi = point();
01006   TEMP_INTEGER(tmp);
01007 
01008   for (Sequence_const_iterator si = x.sequence.begin(),
01009          s_end = x.sequence.end(); si != s_end; ++si) {
01010     if (!si->element().maximize(expr, supi_n, supi_d, maxi, gi))
01011       return false;
01012     else
01013       if (first) {
01014         first = false;
01015         supt_n = supi_n;
01016         supt_d = supi_d;
01017         maxt = maxi;
01018         gt = gi;
01019       }
01020       else {
01021         tmp = (supt_n * supi_d) - (supi_n * supt_d);
01022         if (tmp < 0) {
01023           supt_n = supi_n;
01024           supt_d = supi_d;
01025           maxt = maxi;
01026           gt = gi;
01027         }
01028         else if (tmp == 0) {
01029           maxt = maxt || maxi;
01030           gt = gi;
01031         }
01032       }
01033   }
01034   sup_n = supt_n;
01035   sup_d = supt_d;
01036   maximum = maxt;
01037   g = gt;
01038   return true;
01039 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::minimize ( const Linear_Expression expr,
Coefficient inf_n,
Coefficient inf_d,
bool &  minimum 
) const [inline]

Returns true if and only if *this is not empty and expr is bounded from below in *this, in which case the infimum value is computed.

Parameters:
expr The linear expression to be minimized subject to *this;
inf_n The numerator of the infimum value;
inf_d The denominator of the infimum value;
minimum true if and only if the infimum is also the minimum value.
Exceptions:
std::invalid_argument Thrown if expr and *this are dimension-incompatible.
If *this is empty or expr is not bounded from below, false is returned and inf_n, inf_d and minimum are left untouched.

Definition at line 1043 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), Parma_Polyhedra_Library::Powerset< D >::sequence, and TEMP_INTEGER.

01046                                                      {
01047   const Pointset_Powerset& x = *this;
01048   x.omega_reduce();
01049   bool first = true;
01050 
01051   Coefficient inft_n = 0;
01052   Coefficient inft_d = 1;
01053   bool mint = 0;
01054 
01055   Coefficient infi_n = 0;
01056   Coefficient infi_d = 1;
01057   bool mini = 0;
01058   TEMP_INTEGER(tmp);
01059 
01060   for (Sequence_const_iterator si = x.sequence.begin(),
01061          s_end = x.sequence.end(); si != s_end; ++si) {
01062     if (!si->element().minimize(expr, infi_n, infi_d, mini))
01063       return false;
01064     else
01065       if (first) {
01066         first = false;
01067         inft_n = infi_n;
01068         inft_d = infi_d;
01069         mint = mini;
01070       }
01071       else {
01072         tmp = (inft_n * infi_d) - (infi_n * inft_d);
01073         if (tmp > 0) {
01074           inft_n = infi_n;
01075           inft_d = infi_d;
01076           mint = mini;
01077         }
01078         else if (tmp == 0)
01079           mint = mint || mini;
01080       }
01081   }
01082   inf_n = inft_n;
01083   inf_d = inft_d;
01084   minimum = mint;
01085   return true;
01086 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::minimize ( const Linear_Expression expr,
Coefficient inf_n,
Coefficient inf_d,
bool &  minimum,
Generator g 
) const [inline]

Returns true if and only if *this is not empty and expr is bounded from below in *this, in which case the infimum value and a point where expr reaches it are computed.

Parameters:
expr The linear expression to be minimized subject to *this;
inf_n The numerator of the infimum value;
inf_d The denominator of the infimum value;
minimum true if and only if the infimum is also the minimum value;
g When minimization succeeds, will be assigned a point or closure point where expr reaches its infimum value.
Exceptions:
std::invalid_argument Thrown if expr and *this are dimension-incompatible.
If *this is empty or expr is not bounded from below, false is returned and inf_n, inf_d, minimum and g are left untouched.

Definition at line 1090 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), Parma_Polyhedra_Library::Powerset< D >::sequence, and TEMP_INTEGER.

01094                                                     {
01095   const Pointset_Powerset& x = *this;
01096   x.omega_reduce();
01097   bool first = true;
01098 
01099   Coefficient inft_n = 0;
01100   Coefficient inft_d = 1;
01101   bool mint = 0;
01102   Generator gt = point();
01103 
01104   Coefficient infi_n = 0;
01105   Coefficient infi_d = 1;
01106   bool mini = 0;
01107   Generator gi = point();
01108   TEMP_INTEGER(tmp);
01109 
01110   for (Sequence_const_iterator si = x.sequence.begin(),
01111          s_end = x.sequence.end(); si != s_end; ++si) {
01112     if (!si->element().minimize(expr, infi_n, infi_d, mini, gi))
01113       return false;
01114     else
01115       if (first) {
01116         first = false;
01117         inft_n = infi_n;
01118         inft_d = infi_d;
01119         mint = mini;
01120         gt = gi;
01121       }
01122       else {
01123         tmp = (inft_n * infi_d) - (infi_n * inft_d);
01124         if (tmp > 0) {
01125           inft_n = infi_n;
01126           inft_d = infi_d;
01127           mint = mini;
01128           gt = gi;
01129         }
01130         else if (tmp == 0) {
01131           mint = mint || mini;
01132           gt = gi;
01133         }
01134       }
01135   }
01136   inf_n = inft_n;
01137   inf_d = inft_d;
01138   minimum = mint;
01139   g = gt;
01140   return true;
01141 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::geometrically_covers ( const Pointset_Powerset< PS > &  y  )  const [inline]

Returns true if and only if *this geometrically covers y, i.e., if any point (in some element) of y is also a point (of some element) of *this.

Exceptions:
std::invalid_argument Thrown if *this and y are dimension-incompatible.
Warning:
This may be really expensive!

Definition at line 234 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::geometrically_covers().

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::geometrically_covers(), and Parma_Polyhedra_Library::Pointset_Powerset< PS >::geometrically_equals().

00234                                                        {
00235   // This code is only used when PS is an abstraction of NNC_Polyhedron.
00236   const Pointset_Powerset<NNC_Polyhedron> xx(*this);
00237   const Pointset_Powerset<NNC_Polyhedron> yy(y);
00238   return xx.geometrically_covers(yy);
00239 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::geometrically_equals ( const Pointset_Powerset< PS > &  y  )  const [inline]

Returns true if and only if *this is geometrically equal to y, i.e., if (the elements of) *this and y contain the same set of points.

Exceptions:
std::invalid_argument Thrown if *this and y are dimension-incompatible.
Warning:
This may be really expensive!

Definition at line 244 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::geometrically_covers().

00244                                                        {
00245   // This code is only used when PS is an abstraction of NNC_Polyhedron.
00246   const Pointset_Powerset<NNC_Polyhedron> xx(*this);
00247   const Pointset_Powerset<NNC_Polyhedron> yy(y);
00248   return xx.geometrically_covers(yy) && yy.geometrically_covers(xx);
00249 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::contains ( const Pointset_Powerset< PS > &  y  )  const [inline]

brief Returns true if and only if each disjunct of y is contained in a disjunct of *this.

Exceptions:
std::invalid_argument Thrown if *this and y are topology-incompatible or dimension-incompatible.

Definition at line 766 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::sequence.

00766                                                                 {
00767   const Pointset_Powerset& x = *this;
00768   for (Sequence_const_iterator si = y.sequence.begin(),
00769          ys_end = y.sequence.end(); si != ys_end; ++si) {
00770     const PS& pi = si->element();
00771     bool pi_is_contained = false;
00772     for (Sequence_const_iterator sj = x.sequence.begin(),
00773            xs_end = x.sequence.end();
00774          (sj != xs_end && !pi_is_contained); ++sj) {
00775       const PS& pj = sj->element();
00776       if (pj.contains(pi))
00777         pi_is_contained = true;
00778     }
00779     if (!pi_is_contained)
00780       return false;
00781   }
00782   return true;
00783 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::strictly_contains ( const Pointset_Powerset< PS > &  y  )  const [inline]

brief Returns true if and only if each disjunct of y is strictly contained in a disjunct of *this.

Exceptions:
std::invalid_argument Thrown if *this and y are topology-incompatible or dimension-incompatible.

Definition at line 787 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), and Parma_Polyhedra_Library::Powerset< D >::sequence.

00787                                                                          {
00788   /* omega reduction ensures that a disjunct of y cannot be strictly
00789      contained in one disjunct and also contained but not strictly
00790      contained in another disjunct of *this */
00791   const Pointset_Powerset& x = *this;
00792   x.omega_reduce();
00793   for (Sequence_const_iterator si = y.sequence.begin(),
00794          ys_end = y.sequence.end(); si != ys_end; ++si) {
00795     const PS& pi = si->element();
00796     bool pi_is_strictly_contained = false;
00797     for (Sequence_const_iterator sj = x.sequence.begin(),
00798            xs_end = x.sequence.end();
00799          (sj != xs_end && !pi_is_strictly_contained); ++sj) {
00800       const PS& pj = sj->element();
00801       if (pj.strictly_contains(pi))
00802         pi_is_strictly_contained = true;
00803     }
00804     if (!pi_is_strictly_contained)
00805       return false;
00806   }
00807   return true;
00808 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::contains_integer_point (  )  const [inline]

Returns true if and only if *this contains at least one integer point.

Definition at line 1145 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::sequence.

01145                                                     {
01146   const Pointset_Powerset& x = *this;
01147   for (Sequence_const_iterator si = x.sequence.begin(),
01148          s_end = x.sequence.end(); si != s_end; ++si)
01149     if (si->element().contains_integer_point())
01150       return true;
01151   return false;
01152 }

template<typename PS>
Poly_Con_Relation Parma_Polyhedra_Library::Pointset_Powerset< PS >::relation_with ( const Constraint c  )  const [inline]

Returns the relations holding between the powerset *this and the constraint c.

Exceptions:
std::invalid_argument Thrown if *this and constraint c are dimension-incompatible.

Definition at line 856 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Poly_Con_Relation::implies(), Parma_Polyhedra_Library::Poly_Con_Relation::is_disjoint(), Parma_Polyhedra_Library::Poly_Con_Relation::is_included(), Parma_Polyhedra_Library::Poly_Con_Relation::nothing(), Parma_Polyhedra_Library::Poly_Con_Relation::saturates(), Parma_Polyhedra_Library::Powerset< D >::sequence, and Parma_Polyhedra_Library::Poly_Con_Relation::strictly_intersects().

00856                                                               {
00857   const Pointset_Powerset& x = *this;
00858 
00859   /* *this is included in c if every disjunct is included in c */
00860   bool is_included = true;
00861   /* *this is disjoint with c if every disjunct is disjoint with c */
00862   bool is_disjoint = true;
00863   /* *this strictly_intersects with c if some disjunct strictly
00864      intersects with c */
00865   bool is_strictly_intersecting = false;
00866   /* *this saturates c if some disjunct saturates c and
00867      every disjunct is either disjoint from c or saturates c */
00868   bool saturates_once = false;
00869   bool may_saturate = true;
00870   for (Sequence_const_iterator si = x.sequence.begin(),
00871          s_end = x.sequence.end(); si != s_end; ++si) {
00872     Poly_Con_Relation relation_i = si->element().relation_with(c);
00873     if (!relation_i.implies(Poly_Con_Relation::is_included()))
00874       is_included = false;
00875     if (!relation_i.implies(Poly_Con_Relation::is_disjoint()))
00876       is_disjoint = false;
00877     if (relation_i.implies(Poly_Con_Relation::strictly_intersects()))
00878       is_strictly_intersecting = true;
00879     if (relation_i.implies(Poly_Con_Relation::saturates()))
00880       saturates_once = true;
00881     else if (!relation_i.implies(Poly_Con_Relation::is_disjoint()))
00882       may_saturate = false;
00883   }
00884 
00885   Poly_Con_Relation result = Poly_Con_Relation::nothing();
00886   if (is_included)
00887     result = result && Poly_Con_Relation::is_included();
00888   if (is_disjoint)
00889     result = result && Poly_Con_Relation::is_disjoint();
00890   if (is_strictly_intersecting)
00891     result = result && Poly_Con_Relation::strictly_intersects();
00892   if (saturates_once && may_saturate)
00893     result = result && Poly_Con_Relation::saturates();
00894 
00895   return result;
00896 }

template<typename PS>
Poly_Gen_Relation Parma_Polyhedra_Library::Pointset_Powerset< PS >::relation_with ( const Generator g  )  const [inline]

Returns the relations holding between the powerset *this and the generator g.

Exceptions:
std::invalid_argument Thrown if *this and generator g are dimension-incompatible.

Definition at line 900 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Poly_Gen_Relation::implies(), Parma_Polyhedra_Library::Poly_Gen_Relation::nothing(), Parma_Polyhedra_Library::Powerset< D >::sequence, and Parma_Polyhedra_Library::Poly_Gen_Relation::subsumes().

00900                                                              {
00901   const Pointset_Powerset& x = *this;
00902 
00903   for (Sequence_const_iterator si = x.sequence.begin(),
00904          s_end = x.sequence.end(); si != s_end; ++si) {
00905     Poly_Gen_Relation relation_i = si->element().relation_with(g);
00906     if (relation_i.implies(Poly_Gen_Relation::subsumes()))
00907       return Poly_Gen_Relation::subsumes();
00908   }
00909 
00910   return Poly_Gen_Relation::nothing();
00911 }

template<typename PS>
Poly_Con_Relation Parma_Polyhedra_Library::Pointset_Powerset< PS >::relation_with ( const Congruence cg  )  const [inline]

Returns the relations holding between the powerset *this and the congruence c.

Exceptions:
std::invalid_argument Thrown if *this and congruence c are dimension-incompatible.

Definition at line 812 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Poly_Con_Relation::implies(), Parma_Polyhedra_Library::Poly_Con_Relation::is_disjoint(), Parma_Polyhedra_Library::Poly_Con_Relation::is_included(), Parma_Polyhedra_Library::Poly_Con_Relation::nothing(), Parma_Polyhedra_Library::Poly_Con_Relation::saturates(), Parma_Polyhedra_Library::Powerset< D >::sequence, and Parma_Polyhedra_Library::Poly_Con_Relation::strictly_intersects().

00812                                                                {
00813   const Pointset_Powerset& x = *this;
00814 
00815   /* *this is included in cg if every disjunct is included in cg */
00816   bool is_included = true;
00817   /* *this is disjoint with cg if every disjunct is disjoint with cg */
00818   bool is_disjoint = true;
00819   /* *this strictly_intersects with cg if some disjunct strictly
00820      intersects with cg */
00821   bool is_strictly_intersecting = false;
00822   /* *this saturates cg if some disjunct saturates cg and
00823      every disjunct is either disjoint from cg or saturates cg */
00824   bool saturates_once = false;
00825   bool may_saturate = true;
00826   for (Sequence_const_iterator si = x.sequence.begin(),
00827          s_end = x.sequence.end(); si != s_end; ++si) {
00828     Poly_Con_Relation relation_i = si->element().relation_with(cg);
00829     if (!relation_i.implies(Poly_Con_Relation::is_included()))
00830       is_included = false;
00831     if (!relation_i.implies(Poly_Con_Relation::is_disjoint()))
00832       is_disjoint = false;
00833     if (relation_i.implies(Poly_Con_Relation::strictly_intersects()))
00834       is_strictly_intersecting = true;
00835     if (relation_i.implies(Poly_Con_Relation::saturates()))
00836       saturates_once = true;
00837     else if (!relation_i.implies(Poly_Con_Relation::is_disjoint()))
00838       may_saturate = false;
00839   }
00840 
00841   Poly_Con_Relation result = Poly_Con_Relation::nothing();
00842   if (is_included)
00843     result = result && Poly_Con_Relation::is_included();
00844   if (is_disjoint)
00845     result = result && Poly_Con_Relation::is_disjoint();
00846   if (is_strictly_intersecting)
00847     result = result && Poly_Con_Relation::strictly_intersects();
00848   if (saturates_once && may_saturate)
00849     result = result && Poly_Con_Relation::saturates();
00850 
00851   return result;
00852 }

template<typename PS>
memory_size_type Parma_Polyhedra_Library::Pointset_Powerset< PS >::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< PS > >.

Definition at line 275 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::external_memory_in_bytes().

00275                                                    {
00276   return sizeof(*this) + external_memory_in_bytes();
00277 }

template<typename PS>
memory_size_type Parma_Polyhedra_Library::Pointset_Powerset< PS >::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< PS > >.

Definition at line 269 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::external_memory_in_bytes().

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::total_memory_in_bytes().

00269                                                       {
00270   return Base::external_memory_in_bytes();
00271 }

template<typename PS>
int32_t Parma_Polyhedra_Library::Pointset_Powerset< PS >::hash_code (  )  const [inline]

Returns a 32-bit hash code for *this.

If x and y are such that x == y, then x.hash_code() == y.hash_code().

Definition at line 281 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::space_dimension().

00281                                        {
00282   return space_dimension() & 0x7fffffff;
00283 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK (  )  const [inline]

Checks if all the invariants are satisfied.

Definition at line 1511 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::end(), and Parma_Polyhedra_Library::Pointset_Powerset< PS >::space_dim.

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_congruence(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_congruence_and_minimize(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_congruences(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_congruences_and_minimize(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_constraint(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_constraint_and_minimize(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_constraints(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_constraints_and_minimize(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_disjunct(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_space_dimensions_and_embed(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_space_dimensions_and_project(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::affine_image(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::affine_preimage(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::ascii_load(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::BGP99_heuristics_assign(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::bounded_affine_image(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::bounded_affine_preimage(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::concatenate_assign(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::difference_assign(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::expand_space_dimension(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::fold_space_dimensions(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::generalized_affine_image(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::generalized_affine_preimage(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::map_space_dimensions(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::pairwise_reduce(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::Pointset_Powerset(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::refine_with_congruence(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::refine_with_congruences(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::refine_with_constraint(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::refine_with_constraints(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::remove_higher_space_dimensions(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::remove_space_dimensions(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::simplify_using_context_assign(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::topological_closure_assign(), and Parma_Polyhedra_Library::Pointset_Powerset< PS >::unconstrain().

01511                                 {
01512   const Pointset_Powerset& x = *this;
01513   for (const_iterator xi = x.begin(), x_end = x.end(); xi != x_end; ++xi) {
01514     const PS& pi = xi->element();
01515     if (pi.space_dimension() != x.space_dim) {
01516 #ifndef NDEBUG
01517       std::cerr << "Space dimension mismatch: is " << pi.space_dimension()
01518                 << " in an element of the sequence,\nshould be "
01519                 << x.space_dim << "."
01520                 << std::endl;
01521 #endif
01522       return false;
01523     }
01524   }
01525   return x.Base::OK();
01526 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_disjunct ( const PS &  ph  )  [inline]

Adds to *this the disjunct ph.

Exceptions:
std::invalid_argument Thrown if *this and ph are dimension-incompatible.

Definition at line 43 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, Parma_Polyhedra_Library::Powerset< D >::sequence, and Parma_Polyhedra_Library::Pointset_Powerset< PS >::space_dimension().

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::approximate_partition_aux(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::ascii_load(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::BHZ03_widening_assign(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::concatenate_assign(), and Parma_Polyhedra_Library::Pointset_Powerset< PS >::linear_partition_aux().

00043                                                 {
00044   Pointset_Powerset& x = *this;
00045   if (x.space_dimension() != ph.space_dimension()) {
00046     std::ostringstream s;
00047     s << "PPL::Pointset_Powerset<PS>::add_disjunct(ph):\n"
00048       << "this->space_dimension() == " << x.space_dimension() << ", "
00049       << "ph.space_dimension() == " << ph.space_dimension() << ".";
00050     throw std::invalid_argument(s.str());
00051   }
00052   x.sequence.push_back(Determinate<PS>(ph));
00053   x.reduced = false;
00054   assert(x.OK());
00055 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_constraint ( const Constraint c  )  [inline]

Intersects *this with constraint c.

Exceptions:
std::invalid_argument Thrown if *this and constraint c are topology-incompatible or dimension-incompatible.

Definition at line 129 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00129                                                          {
00130   Pointset_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 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::refine_with_constraint ( const Constraint c  )  [inline]

Use the constraint c to refine *this.

Parameters:
c The constraint to be used for refinement.
Exceptions:
std::invalid_argument Thrown if *this and c are dimension-incompatible.

Definition at line 156 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00156                                                                  {
00157   Pointset_Powerset& x = *this;
00158   for (Sequence_iterator si = x.sequence.begin(),
00159          s_end = x.sequence.end(); si != s_end; ++si)
00160     si->element().refine_with_constraint(c);
00161   x.reduced = false;
00162   assert(x.OK());
00163 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_constraint_and_minimize ( const Constraint c  )  [inline]

Intersects *this with the constraint c, minimizing the result.

Returns:
false if and only if the result is empty.
Exceptions:
std::invalid_argument Thrown if *this and c are topology-incompatible or dimension-incompatible.
Deprecated:
See A Note on the Implementation of the Operators.

Definition at line 140 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::empty(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00140                                                                       {
00141   Pointset_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 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_constraints ( const Constraint_System cs  )  [inline]

Intersects *this with the constraints in cs.

Parameters:
cs The constraints to intersect with.
Exceptions:
std::invalid_argument Thrown if *this and cs are topology-incompatible or dimension-incompatible.

Definition at line 167 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00167                                                                   {
00168   Pointset_Powerset& x = *this;
00169   for (Sequence_iterator si = x.sequence.begin(),
00170          s_end = x.sequence.end(); si != s_end; ++si)
00171     si->element().add_constraints(cs);
00172   x.reduced = false;
00173   assert(x.OK());
00174 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::refine_with_constraints ( const Constraint_System cs  )  [inline]

Use the constraints in cs to refine *this.

Parameters:
cs The constraints to be used for refinement.
Exceptions:
std::invalid_argument Thrown if *this and cs are dimension-incompatible.

Definition at line 195 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00195                                                                           {
00196   Pointset_Powerset& x = *this;
00197   for (Sequence_iterator si = x.sequence.begin(),
00198          s_end = x.sequence.end(); si != s_end; ++si)
00199     si->element().refine_with_constraints(cs);
00200   x.reduced = false;
00201   assert(x.OK());
00202 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_constraints_and_minimize ( const Constraint_System cs  )  [inline]

Intersects *this with the constraints in cs, minimizing the result.

Returns:
false if and only if the result is empty.
Parameters:
cs The constraints to intersect with.
Exceptions:
std::invalid_argument Thrown if *this and cs are topology-incompatible or dimension-incompatible.
Deprecated:
See A Note on the Implementation of the Operators.

Definition at line 179 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::empty(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00179                                                           {
00180   Pointset_Powerset& x = *this;
00181   for (Sequence_iterator si = x.sequence.begin(),
00182          s_end = x.sequence.end(); si != s_end; )
00183     if (!si->element().add_constraints_and_minimize(cs))
00184       si = x.sequence.erase(si);
00185     else {
00186       x.reduced = false;
00187       ++si;
00188     }
00189   assert(x.OK());
00190   return !x.empty();
00191 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_congruence ( const Congruence c  )  [inline]

Intersects *this with congruence c.

Exceptions:
std::invalid_argument Thrown if *this and congruence c are topology-incompatible or dimension-incompatible.

Definition at line 206 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00206                                                          {
00207   Pointset_Powerset& x = *this;
00208   for (Sequence_iterator si = x.sequence.begin(),
00209          s_end = x.sequence.end(); si != s_end; ++si)
00210     si->element().add_congruence(c);
00211   x.reduced = false;
00212   assert(x.OK());
00213 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::refine_with_congruence ( const Congruence cg  )  [inline]

Use the congruence cg to refine *this.

Parameters:
cg The congruence to be used for refinement.
Exceptions:
std::invalid_argument Thrown if *this and cg are dimension-incompatible.

Definition at line 217 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00217                                                                   {
00218   Pointset_Powerset& x = *this;
00219   for (Sequence_iterator si = x.sequence.begin(),
00220          s_end = x.sequence.end(); si != s_end; ++si)
00221     si->element().refine_with_congruence(cg);
00222   x.reduced = false;
00223   assert(x.OK());
00224 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_congruence_and_minimize ( const Congruence c  )  [inline]

Intersects *this with the congruence c, minimizing the result.

Returns:
false if and only if the result is empty.
Exceptions:
std::invalid_argument Thrown if *this and c are topology-incompatible or dimension-incompatible.
Deprecated:
See A Note on the Implementation of the Operators.

Definition at line 228 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::empty(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00228                                                                       {
00229   Pointset_Powerset& x = *this;
00230   for (Sequence_iterator si = x.sequence.begin(),
00231          s_end = x.sequence.end(); si != s_end; )
00232     if (!si->element().add_congruence_and_minimize(c))
00233       si = x.sequence.erase(si);
00234     else {
00235       x.reduced = false;
00236       ++si;
00237     }
00238   assert(x.OK());
00239   return !x.empty();
00240 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_congruences ( const Congruence_System cgs  )  [inline]

Intersects *this with the congruences in cgs.

Parameters:
cgs The congruences to intersect with.
Exceptions:
std::invalid_argument Thrown if *this and cgs are topology-incompatible or dimension-incompatible.

Definition at line 244 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00244                                                                   {
00245   Pointset_Powerset& x = *this;
00246   for (Sequence_iterator si = x.sequence.begin(),
00247          s_end = x.sequence.end(); si != s_end; ++si)
00248     si->element().add_congruences(cs);
00249   x.reduced = false;
00250   assert(x.OK());
00251 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::refine_with_congruences ( const Congruence_System cgs  )  [inline]

Use the congruences in cgs to refine *this.

Parameters:
cgs The congruences to be used for refinement.
Exceptions:
std::invalid_argument Thrown if *this and cgs are dimension-incompatible.

Definition at line 255 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00255                                                                            {
00256   Pointset_Powerset& x = *this;
00257   for (Sequence_iterator si = x.sequence.begin(),
00258          s_end = x.sequence.end(); si != s_end; ++si)
00259     si->element().refine_with_congruences(cgs);
00260   x.reduced = false;
00261   assert(x.OK());
00262 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_congruences_and_minimize ( const Congruence_System cs  )  [inline]

Intersects *this with the congruences in cs, minimizing the result.

Returns:
false if and only if the result is empty.
Parameters:
cs The congruences to intersect with.
Exceptions:
std::invalid_argument Thrown if *this and cs are topology-incompatible or dimension-incompatible.
Deprecated:
See A Note on the Implementation of the Operators.

Definition at line 267 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::empty(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00267                                                           {
00268   Pointset_Powerset& x = *this;
00269   for (Sequence_iterator si = x.sequence.begin(),
00270          s_end = x.sequence.end(); si != s_end; )
00271     if (!si->element().add_congruences_and_minimize(cs))
00272       si = x.sequence.erase(si);
00273     else {
00274       x.reduced = false;
00275       ++si;
00276     }
00277   assert(x.OK());
00278   return !x.empty();
00279 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::unconstrain ( Variable  var  )  [inline]

Computes the cylindrification of *this with respect to space dimension var, assigning the result to *this.

Parameters:
var The space dimension that will be unconstrained.
Exceptions:
std::invalid_argument Thrown if var is not a space dimension of *this.

Definition at line 283 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00283                                                      {
00284   Pointset_Powerset& x = *this;
00285   for (Sequence_iterator si = x.sequence.begin(),
00286          s_end = x.sequence.end(); si != s_end; ++si) {
00287     si->element().unconstrain(var);
00288     x.reduced = false;
00289   }
00290   assert(x.OK());
00291 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::unconstrain ( const Variables_Set &  to_be_unconstrained  )  [inline]

Computes the cylindrification of *this with respect to the set of space dimensions to_be_unconstrained, assigning the result to *this.

Parameters:
to_be_unconstrained The set of space dimension that will be unconstrained.
Exceptions:
std::invalid_argument Thrown if *this is dimension-incompatible with one of the Variable objects contained in to_be_removed.

Definition at line 295 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00295                                                                            {
00296   Pointset_Powerset& x = *this;
00297   for (Sequence_iterator si = x.sequence.begin(),
00298          s_end = x.sequence.end(); si != s_end; ++si) {
00299     si->element().unconstrain(to_be_unconstrained);
00300     x.reduced = false;
00301   }
00302   assert(x.OK());
00303 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::topological_closure_assign (  )  [inline]

Assigns to *this its topological closure.

Definition at line 683 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), and Parma_Polyhedra_Library::Powerset< D >::sequence.

00683                                                   {
00684   Pointset_Powerset& x = *this;
00685   for (Sequence_iterator si = x.sequence.begin(),
00686          s_end = x.sequence.end(); si != s_end; ++si)
00687     si->element().topological_closure_assign();
00688   assert(x.OK());
00689 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::intersection_assign ( const Pointset_Powerset< PS > &  y  )  [inline]

Assigns to *this the intersection of *this and y.

The result is obtained by intersecting each disjunct in *this with each disjunct in y and collecting all these intersections.

Definition at line 209 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Determinate< PS >::lift_op_assign(), and Parma_Polyhedra_Library::Powerset< D >::pairwise_apply_assign().

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::intersection_assign_and_minimize().

00209                                                                      {
00210   Pointset_Powerset& x = *this;
00211   x.pairwise_apply_assign
00212     (y, CS::lift_op_assign(std::mem_fun_ref(&PS::intersection_assign)));
00213 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::intersection_assign_and_minimize ( const Pointset_Powerset< PS > &  y  )  [inline]

Assigns to *this the intersection of *this and y.

The result is obtained by intersecting each disjunct in *this with each disjunct in y, minimizing the result and collecting all these intersections.

Returns:
false if and only if the result is empty.
Deprecated:
See A Note on the Implementation of the Operators.

Definition at line 218 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::intersection_assign(), and Parma_Polyhedra_Library::Pointset_Powerset< PS >::is_empty().

00218                                                              {
00219   intersection_assign(y);
00220   return !is_empty();
00221 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::difference_assign ( const Pointset_Powerset< PS > &  y  )  [inline]

Assigns to *this an (a smallest) over-approximation as a powerset of the disjunct domain of the set-theoretical difference of *this and y.

Exceptions:
std::invalid_argument Thrown if *this and y are dimension-incompatible.

Definition at line 288 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::difference_assign().

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::difference_assign().

00288                                               {
00289   // This code is only used when PS is an abstraction of NNC_Polyhedron.
00290   Pointset_Powerset<NNC_Polyhedron> nnc_this(*this);
00291   Pointset_Powerset<NNC_Polyhedron> nnc_y(y);
00292   nnc_this.difference_assign(nnc_y);
00293   *this = nnc_this;
00294 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::simplify_using_context_assign ( const Pointset_Powerset< PS > &  y  )  [inline]

Assigns to *this a meet-preserving simplification of *this with respect to y. If false is returned, then the intersection is empty.

Exceptions:
std::invalid_argument Thrown if *this and y are topology-incompatible or dimension-incompatible.

Definition at line 718 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::intersection_preserving_enlarge_element(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::is_empty(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), Parma_Polyhedra_Library::Powerset< D >::reduced, Parma_Polyhedra_Library::Powerset< D >::sequence, and Parma_Polyhedra_Library::Powerset< D >::size().

00718                                                           {
00719   Pointset_Powerset& x = *this;
00720 
00721   // Omega reduction is required.
00722   // TODO: check whether it would be more efficient to Omega-reduce x
00723   // during the simplification process: when examining *si, we check
00724   // if it has been made redundant by any of the elements preceding it
00725   // (which have been already simplified).
00726   x.omega_reduce();
00727   if (x.is_empty())
00728     return false;
00729   y.omega_reduce();
00730   if (y.is_empty()) {
00731     x = y;
00732     return false;
00733   }
00734 
00735   if (y.size() == 1) {
00736     // More efficient, special handling of the singleton context case.
00737     const PS& y_i = y.sequence.begin()->element();
00738     for (Sequence_iterator si = x.sequence.begin(),
00739            s_end = x.sequence.end(); si != s_end; ) {
00740       PS& x_i = si->element();
00741       if (x_i.simplify_using_context_assign(y_i))
00742         ++si;
00743       else
00744         // Intersection is empty: drop the disjunct.
00745         si = x.sequence.erase(si);
00746     }
00747   }
00748   else {
00749     // The context is not a singleton.
00750     for (Sequence_iterator si = x.sequence.begin(),
00751            s_end = x.sequence.end(); si != s_end; ) {
00752       if (y.intersection_preserving_enlarge_element(si->element()))
00753         ++si;
00754       else
00755         // Intersection with `*si' is empty: drop the disjunct.
00756         si = x.sequence.erase(si);
00757     }
00758   }
00759   x.reduced = false;
00760   assert(x.OK());
00761   return !x.sequence.empty();
00762 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::affine_image ( Variable  var,
const Linear_Expression expr,
Coefficient_traits::const_reference  denominator = Coefficient_one() 
) [inline]

Assigns to *this the affine image of *this under the function mapping variable var to the affine expression specified by expr and denominator.

Parameters:
var The variable to which the affine expression is assigned;
expr The numerator of the affine expression;
denominator The denominator of the affine expression (optional argument with default value 1).
Exceptions:
std::invalid_argument Thrown if denominator is zero or if expr and *this are dimension-incompatible or if var is not a space dimension of *this.

Definition at line 414 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00417                                                  {
00418   Pointset_Powerset& x = *this;
00419   for (Sequence_iterator si = x.sequence.begin(),
00420          s_end = x.sequence.end(); si != s_end; ++si) {
00421     si->element().affine_image(var, expr, denominator);
00422     // Note that the underlying domain can apply conservative approximation:
00423     // that is why it would not be correct to make the loss of reduction
00424     // conditional on `var' and `expr'.
00425     x.reduced = false;
00426   }
00427   assert(x.OK());
00428 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::affine_preimage ( Variable  var,
const Linear_Expression expr,
Coefficient_traits::const_reference  denominator = Coefficient_one() 
) [inline]

Assigns to *this the affine preimage of *this under the function mapping variable var to the affine expression specified by expr and denominator.

Parameters:
var The variable to which the affine expression is assigned;
expr The numerator of the affine expression;
denominator The denominator of the affine expression (optional argument with default value 1).
Exceptions:
std::invalid_argument Thrown if denominator is zero or if expr and *this are dimension-incompatible or if var is not a space dimension of *this.

Definition at line 432 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00435                                                     {
00436   Pointset_Powerset& x = *this;
00437   for (Sequence_iterator si = x.sequence.begin(),
00438          s_end = x.sequence.end(); si != s_end; ++si) {
00439     si->element().affine_preimage(var, expr, denominator);
00440     // Note that the underlying domain can apply conservative approximation:
00441     // that is why it would not be correct to make the loss of reduction
00442     // conditional on `var' and `expr'.
00443     x.reduced = false;
00444   }
00445   assert(x.OK());
00446 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::generalized_affine_image ( Variable  var,
Relation_Symbol  relsym,
const Linear_Expression expr,
Coefficient_traits::const_reference  denominator = Coefficient_one() 
) [inline]

Assigns to *this the image of *this with respect to the generalized affine relation $\mathrm{var}' \relsym \frac{\mathrm{expr}}{\mathrm{denominator}}$, where $\mathord{\relsym}$ is the relation symbol encoded by relsym.

Parameters:
var The left hand side variable of the generalized affine relation;
relsym The relation symbol;
expr The numerator of the right hand side affine expression;
denominator The denominator of the right hand side affine expression (optional argument with default value 1).
Exceptions:
std::invalid_argument Thrown if denominator is zero or if expr and *this are dimension-incompatible or if var is not a space dimension of *this or if *this is a C_Polyhedron and relsym is a strict relation symbol.

Definition at line 482 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00485                                                                           {
00486   Pointset_Powerset& x = *this;
00487   for (Sequence_iterator si = x.sequence.begin(),
00488          s_end = x.sequence.end(); si != s_end; ++si) {
00489     si->element().generalized_affine_image(var, relsym, expr, denominator);
00490     x.reduced = false;
00491   }
00492   assert(x.OK());
00493 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::generalized_affine_preimage ( Variable  var,
Relation_Symbol  relsym,
const Linear_Expression expr,
Coefficient_traits::const_reference  denominator = Coefficient_one() 
) [inline]

Assigns to *this the preimage of *this with respect to the generalized affine relation $\mathrm{var}' \relsym \frac{\mathrm{expr}}{\mathrm{denominator}}$, where $\mathord{\relsym}$ is the relation symbol encoded by relsym.

Parameters:
var The left hand side variable of the generalized affine relation;
relsym The relation symbol;
expr The numerator of the right hand side affine expression;
denominator The denominator of the right hand side affine expression (optional argument with default value 1).
Exceptions:
std::invalid_argument Thrown if denominator is zero or if expr and *this are dimension-incompatible or if var is not a space dimension of *this or if *this is a C_Polyhedron and relsym is a strict relation symbol.

Definition at line 498 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00501                                                                              {  Pointset_Powerset& x = *this;
00502   for (Sequence_iterator si = x.sequence.begin(),
00503          s_end = x.sequence.end(); si != s_end; ++si) {
00504     si->element().generalized_affine_preimage(var, relsym, expr, denominator);
00505     x.reduced = false;
00506   }
00507   assert(x.OK());
00508 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::generalized_affine_image ( const Linear_Expression lhs,
Relation_Symbol  relsym,
const Linear_Expression rhs 
) [inline]

Assigns to *this the image of *this with respect to the generalized affine relation $\mathrm{lhs}' \relsym \mathrm{rhs}$, where $\mathord{\relsym}$ is the relation symbol encoded by relsym.

Parameters:
lhs The left hand side affine expression;
relsym The relation symbol;
rhs The right hand side affine expression.
Exceptions:
std::invalid_argument Thrown if *this is dimension-incompatible with lhs or rhs or if *this is a C_Polyhedron and relsym is a strict relation symbol.

Definition at line 452 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00454                                                          {
00455   Pointset_Powerset& x = *this;
00456   for (Sequence_iterator si = x.sequence.begin(),
00457          s_end = x.sequence.end(); si != s_end; ++si) {
00458     si->element().generalized_affine_image(lhs, relsym, rhs);
00459     x.reduced = false;
00460   }
00461   assert(x.OK());
00462 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::generalized_affine_preimage ( const Linear_Expression lhs,
Relation_Symbol  relsym,
const Linear_Expression rhs 
) [inline]

Assigns to *this the preimage of *this with respect to the generalized affine relation $\mathrm{lhs}' \relsym \mathrm{rhs}$, where $\mathord{\relsym}$ is the relation symbol encoded by relsym.

Parameters:
lhs The left hand side affine expression;
relsym The relation symbol;
rhs The right hand side affine expression.
Exceptions:
std::invalid_argument Thrown if *this is dimension-incompatible with lhs or rhs or if *this is a C_Polyhedron and relsym is a strict relation symbol.

Definition at line 467 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00469                                                             {
00470   Pointset_Powerset& x = *this;
00471   for (Sequence_iterator si = x.sequence.begin(),
00472          s_end = x.sequence.end(); si != s_end; ++si) {
00473     si->element().generalized_affine_preimage(lhs, relsym, rhs);
00474     x.reduced = false;
00475   }
00476   assert(x.OK());
00477 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::bounded_affine_image ( Variable  var,
const Linear_Expression lb_expr,
const Linear_Expression ub_expr,
Coefficient_traits::const_reference  denominator = Coefficient_one() 
) [inline]

Assigns to *this the image of *this with respect to the bounded affine relation $\frac{\mathrm{lb\_expr}}{\mathrm{denominator}} \leq \mathrm{var}' \leq \frac{\mathrm{ub\_expr}}{\mathrm{denominator}}$.

Parameters:
var The variable updated by the affine relation;
lb_expr The numerator of the lower bounding affine expression;
ub_expr The numerator of the upper bounding affine expression;
denominator The (common) denominator for the lower and upper bounding affine expressions (optional argument with default value 1).
Exceptions:
std::invalid_argument Thrown if denominator is zero or if lb_expr (resp., ub_expr) and *this are dimension-incompatible or if var is not a space dimension of *this.

Definition at line 514 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00517                                                                       {
00518   Pointset_Powerset& x = *this;
00519   for (Sequence_iterator si = x.sequence.begin(),
00520          s_end = x.sequence.end(); si != s_end; ++si) {
00521     si->element().bounded_affine_image(var, lb_expr, ub_expr, denominator);
00522     x.reduced = false;
00523   }
00524   assert(x.OK());
00525 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::bounded_affine_preimage ( Variable  var,
const Linear_Expression lb_expr,
const Linear_Expression ub_expr,
Coefficient_traits::const_reference  denominator = Coefficient_one() 
) [inline]

Assigns to *this the preimage of *this with respect to the bounded affine relation $\frac{\mathrm{lb\_expr}}{\mathrm{denominator}} \leq \mathrm{var}' \leq \frac{\mathrm{ub\_expr}}{\mathrm{denominator}}$.

Parameters:
var The variable updated by the affine relation;
lb_expr The numerator of the lower bounding affine expression;
ub_expr The numerator of the upper bounding affine expression;
denominator The (common) denominator for the lower and upper bounding affine expressions (optional argument with default value 1).
Exceptions:
std::invalid_argument Thrown if denominator is zero or if lb_expr (resp., ub_expr) and *this are dimension-incompatible or if var is not a space dimension of *this.

Definition at line 530 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, and Parma_Polyhedra_Library::Powerset< D >::sequence.

00533                                                                          {
00534   Pointset_Powerset& x = *this;
00535   for (Sequence_iterator si = x.sequence.begin(),
00536          s_end = x.sequence.end(); si != s_end; ++si) {
00537     si->element().bounded_affine_preimage(var, lb_expr, ub_expr,
00538                                           denominator);
00539     x.reduced = false;
00540   }
00541   assert(x.OK());
00542 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::time_elapse_assign ( const Pointset_Powerset< PS > &  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 disjunct in *this with each disjunct in y.

Definition at line 225 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Determinate< PS >::lift_op_assign(), and Parma_Polyhedra_Library::Powerset< D >::pairwise_apply_assign().

00225                                                                     {
00226   Pointset_Powerset& x = *this;
00227   x.pairwise_apply_assign
00228     (y, CS::lift_op_assign(std::mem_fun_ref(&PS::time_elapse_assign)));
00229 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::pairwise_reduce (  )  [inline]

Assign to *this the result of (recursively) merging together the pairs of disjuncts whose upper-bound is the same as their set-theoretical union.

On exit, for all the pairs $\cP$, $\cQ$ of different disjuncts in *this, we have $\cP \uplus \cQ \neq \cP \union \cQ$.

Definition at line 1156 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct_preserve_reduction(), Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::EMPTY, Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), Parma_Polyhedra_Library::Powerset< D >::sequence, Parma_Polyhedra_Library::Powerset< D >::size(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::space_dim, and Parma_Polyhedra_Library::swap().

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::BGP99_extrapolation_assign(), and Parma_Polyhedra_Library::Pointset_Powerset< PS >::BHZ03_widening_assign().

01156                                        {
01157   Pointset_Powerset& x = *this;
01158   // It is wise to omega-reduce before pairwise-reducing.
01159   x.omega_reduce();
01160 
01161   size_type n = x.size();
01162   size_type deleted;
01163   do {
01164     Pointset_Powerset new_x(x.space_dim, EMPTY);
01165     std::deque<bool> marked(n, false);
01166     deleted = 0;
01167     Sequence_iterator s_begin = x.sequence.begin();
01168     Sequence_iterator s_end = x.sequence.end();
01169     unsigned si_index = 0;
01170     for (Sequence_iterator si = s_begin; si != s_end; ++si, ++si_index) {
01171       if (marked[si_index])
01172         continue;
01173       PS& pi = si->element();
01174       Sequence_const_iterator sj = si;
01175       unsigned sj_index = si_index;
01176       for (++sj, ++sj_index; sj != s_end; ++sj, ++sj_index) {
01177         if (marked[sj_index])
01178           continue;
01179         const PS& pj = sj->element();
01180         if (pi.upper_bound_assign_if_exact(pj)) {
01181           marked[si_index] = marked[sj_index] = true;
01182           // FIXME: check whether the preservation of reduction was
01183           // actually meant here.
01184           new_x.add_non_bottom_disjunct_preserve_reduction(pi);
01185           ++deleted;
01186           goto next;
01187         }
01188       }
01189     next:
01190       ;
01191     }
01192     iterator nx_begin = new_x.begin();
01193     iterator nx_end = new_x.end();
01194     unsigned xi_index = 0;
01195     for (const_iterator xi = x.begin(),
01196            x_end = x.end(); xi != x_end; ++xi, ++xi_index)
01197       if (!marked[xi_index])
01198         nx_begin = new_x.add_non_bottom_disjunct_preserve_reduction(*xi,
01199                                                                     nx_begin,
01200                                                                     nx_end);
01201     std::swap(x.sequence, new_x.sequence);
01202     n -= deleted;
01203   } while (deleted > 0);
01204   assert(x.OK());
01205 }

template<typename PS>
template<typename Widening>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::BGP99_extrapolation_assign ( const Pointset_Powerset< PS > &  y,
Widening  wf,
unsigned  max_disjuncts 
) [inline]

Assigns to *this the result of applying the BGP99 extrapolation operator to *this and y, using the widening function wf and the cardinality threshold max_disjuncts.

Parameters:
y A powerset that must definitely entail *this;
wf The widening function to be used on polyhedra objects. It is obtained from the corresponding widening method by using the helper function Parma_Polyhedra_Library::widen_fun_ref. Legal values are, e.g., widen_fun_ref(&Polyhedron::H79_widening_assign) and widen_fun_ref(&Polyhedron::limited_H79_extrapolation_assign, cs);
max_disjuncts The maximum number of disjuncts occurring in the powerset *this before starting the computation. If this number is exceeded, some of the disjuncts in *this are collapsed (i.e., joined together).
Exceptions:
std::invalid_argument Thrown if *this and y are dimension-incompatible.
For a description of the extrapolation operator, see [BGP99] and [BHZ03b].

Definition at line 1261 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::BGP99_heuristics_assign(), Parma_Polyhedra_Library::Powerset< D >::collapse(), Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >::definitely_entails(), and Parma_Polyhedra_Library::Pointset_Powerset< PS >::pairwise_reduce().

01263                                                    {
01264   // `x' is the current iteration value.
01265   Pointset_Powerset& x = *this;
01266 
01267 #ifndef NDEBUG
01268   {
01269     // We assume that `y' entails `x'.
01270     const Pointset_Powerset<PS> x_copy = x;
01271     const Pointset_Powerset<PS> y_copy = y;
01272     assert(y_copy.definitely_entails(x_copy));
01273   }
01274 #endif
01275 
01276   x.pairwise_reduce();
01277   if (max_disjuncts != 0)
01278     x.collapse(max_disjuncts);
01279   x.BGP99_heuristics_assign(y, wf);
01280 }

template<typename PS>
template<typename Cert, typename Widening>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::BHZ03_widening_assign ( const Pointset_Powerset< PS > &  y,
Widening  wf 
) [inline]

Assigns to *this the result of computing the BHZ03-widening between *this and y, using the widening function wf certified by the convergence certificate Cert.

Parameters:
y The finite powerset computed in the previous iteration step. It must definitely entail *this;
wf The widening function to be used on disjuncts. It is obtained from the corresponding widening method by using the helper function widen_fun_ref. Legal values are, e.g., widen_fun_ref(&Polyhedron::H79_widening_assign) and widen_fun_ref(&Polyhedron::limited_H79_extrapolation_assign, cs).
Exceptions:
std::invalid_argument Thrown if *this and y are dimension-incompatible.
Warning:
In order to obtain a proper widening operator, the template parameter Cert should be a finite convergence certificate for the base-level widening function wf; otherwise, an extrapolation operator is obtained. For a description of the methods that should be provided by Cert, see BHRZ03_Certificate or H79_Certificate.

Definition at line 1348 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_disjunct(), Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >::begin(), Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::BGP99_heuristics_assign(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::collect_certificates(), Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >::definitely_entails(), Parma_Polyhedra_Library::EMPTY, Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >::end(), Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::is_cert_multiset_stabilizing(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::pairwise_reduce(), Parma_Polyhedra_Library::Powerset< D >::size(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::space_dim, and Parma_Polyhedra_Library::swap().

01349                                                           {
01350   // `x' is the current iteration value.
01351   Pointset_Powerset& x = *this;
01352 
01353 #ifndef NDEBUG
01354   {
01355     // We assume that `y' entails `x'.
01356     const Pointset_Powerset<PS> x_copy = x;
01357     const Pointset_Powerset<PS> y_copy = y;
01358     assert(y_copy.definitely_entails(x_copy));
01359   }
01360 #endif
01361 
01362   // First widening technique: do nothing.
01363 
01364   // If `y' is the empty collection, do nothing.
01365   assert(x.size() > 0);
01366   if (y.size() == 0)
01367     return;
01368 
01369   // Compute the poly-hull of `x'.
01370   PS x_hull(x.space_dim, EMPTY);
01371   for (const_iterator i = x.begin(), x_end = x.end(); i != x_end; ++i)
01372     x_hull.upper_bound_assign(i->element());
01373 
01374   // Compute the poly-hull of `y'.
01375   PS y_hull(y.space_dim, EMPTY);
01376   for (const_iterator i = y.begin(), y_end = y.end(); i != y_end; ++i)
01377     y_hull.upper_bound_assign(i->element());
01378   // Compute the certificate for `y_hull'.
01379   const Cert y_hull_cert(y_hull);
01380 
01381   // If the hull is stabilizing, do nothing.
01382   int hull_stabilization = y_hull_cert.compare(x_hull);
01383   if (hull_stabilization == 1)
01384     return;
01385 
01386   // Multiset ordering is only useful when `y' is not a singleton.
01387   const bool y_is_not_a_singleton = y.size() > 1;
01388 
01389   // The multiset certificate for `y':
01390   // we want to be lazy about its computation.
01391   typedef std::map<Cert, size_type, typename Cert::Compare> Cert_Multiset;
01392   Cert_Multiset y_cert_ms;
01393   bool y_cert_ms_computed = false;
01394 
01395   if (hull_stabilization == 0 && y_is_not_a_singleton) {
01396     // Collect the multiset certificate for `y'.
01397     y.collect_certificates(y_cert_ms);
01398     y_cert_ms_computed = true;
01399     // If multiset ordering is stabilizing, do nothing.
01400     if (x.is_cert_multiset_stabilizing(y_cert_ms))
01401       return;
01402   }
01403 
01404   // Second widening technique: try the BGP99 powerset heuristics.
01405   Pointset_Powerset<PS> bgp99_heuristics = x;
01406   bgp99_heuristics.BGP99_heuristics_assign(y, wf);
01407 
01408   // Compute the poly-hull of `bgp99_heuristics'.
01409   PS bgp99_heuristics_hull(x.space_dim, EMPTY);
01410   for (const_iterator i = bgp99_heuristics.begin(),
01411          bh_end = bgp99_heuristics.end(); i != bh_end; ++i)
01412     bgp99_heuristics_hull.upper_bound_assign(i->element());
01413 
01414   // Check for stabilization and, if successful,
01415   // commit to the result of the extrapolation.
01416   hull_stabilization = y_hull_cert.compare(bgp99_heuristics_hull);
01417   if (hull_stabilization == 1) {
01418     // The poly-hull is stabilizing.
01419     std::swap(x, bgp99_heuristics);
01420     return;
01421   }
01422   else if (hull_stabilization == 0 && y_is_not_a_singleton) {
01423     // If not already done, compute multiset certificate for `y'.
01424     if (!y_cert_ms_computed) {
01425       y.collect_certificates(y_cert_ms);
01426       y_cert_ms_computed = true;
01427     }
01428     if (bgp99_heuristics.is_cert_multiset_stabilizing(y_cert_ms)) {
01429       std::swap(x, bgp99_heuristics);
01430       return;
01431     }
01432     // Third widening technique: pairwise-reduction on `bgp99_heuristics'.
01433     // Note that pairwise-reduction does not affect the computation
01434     // of the poly-hulls, so that we only have to check the multiset
01435     // certificate relation.
01436     Pointset_Powerset<PS> reduced_bgp99_heuristics(bgp99_heuristics);
01437     reduced_bgp99_heuristics.pairwise_reduce();
01438     if (reduced_bgp99_heuristics.is_cert_multiset_stabilizing(y_cert_ms)) {
01439       std::swap(x, reduced_bgp99_heuristics);
01440       return;
01441     }
01442   }
01443 
01444   // Fourth widening technique: this is applicable only when
01445   // `y_hull' is a proper subset of `bgp99_heuristics_hull'.
01446   if (bgp99_heuristics_hull.strictly_contains(y_hull)) {
01447     // Compute (y_hull \widen bgp99_heuristics_hull).
01448     PS ph = bgp99_heuristics_hull;
01449     wf(ph, y_hull);
01450     // Compute the difference between `ph' and `bgp99_heuristics_hull'.
01451     ph.difference_assign(bgp99_heuristics_hull);
01452     x.add_disjunct(ph);
01453     return;
01454   }
01455 
01456   // Fall back to the computation of the poly-hull.
01457   Pointset_Powerset<PS> x_hull_singleton(x.space_dim, EMPTY);
01458   x_hull_singleton.add_disjunct(x_hull);
01459   std::swap(x, x_hull_singleton);
01460 }

template<typename PS>
Pointset_Powerset< PS > & Parma_Polyhedra_Library::Pointset_Powerset< PS >::operator= ( const Pointset_Powerset< PS > &  y  )  [inline]

The assignment operator (*this and y can be dimension-incompatible).

Definition at line 182 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::space_dim.

00182                                                            {
00183   Pointset_Powerset& x = *this;
00184   x.Base::operator=(y);
00185   x.space_dim = y.space_dim;
00186   return x;
00187 }

template<typename PS>
template<typename QH>
Pointset_Powerset< PS > & Parma_Polyhedra_Library::Pointset_Powerset< PS >::operator= ( const Pointset_Powerset< QH > &  y  )  [inline]

Conversion assignment: the type QH of the disjuncts in the source powerset is different from PS (*this and y can be dimension-incompatible).

Definition at line 200 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::swap().

00200                                                                {
00201   Pointset_Powerset& x = *this;
00202   Pointset_Powerset<PS> pps(y);
00203   x.swap(pps);
00204   return x;
00205 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::swap ( Pointset_Powerset< PS > &  y  )  [inline]

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_space_dimensions_and_embed ( dimension_type  m  )  [inline]

Adds m new dimensions to the vector space containing *this and embeds each disjunct in *this in the new space.

Definition at line 307 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::sequence, and Parma_Polyhedra_Library::Pointset_Powerset< PS >::space_dim.

00307                                                                       {
00308   Pointset_Powerset& x = *this;
00309   for (Sequence_iterator si = x.sequence.begin(),
00310          s_end = x.sequence.end(); si != s_end; ++si)
00311     si->element().add_space_dimensions_and_embed(m);
00312   x.space_dim += m;
00313   assert(x.OK());
00314 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_space_dimensions_and_project ( dimension_type  m  )  [inline]

Adds m new dimensions to the vector space containing *this without embedding the disjuncts in *this in the new space.

Definition at line 318 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::sequence, and Parma_Polyhedra_Library::Pointset_Powerset< PS >::space_dim.

00318                                                                         {
00319   Pointset_Powerset& x = *this;
00320   for (Sequence_iterator si = x.sequence.begin(),
00321          s_end = x.sequence.end(); si != s_end; ++si)
00322     si->element().add_space_dimensions_and_project(m);
00323   x.space_dim += m;
00324   assert(x.OK());
00325 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::concatenate_assign ( const Pointset_Powerset< PS > &  y  )  [inline]

Assigns to *this the concatenation of *this and y.

The result is obtained by computing the pairwise concatenation of each disjunct in *this with each disjunct in y.

Definition at line 92 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::abandon_expensive_computations, Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_disjunct(), Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Determinate< PS >::concatenate_assign(), Parma_Polyhedra_Library::EMPTY, Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Determinate< PS >::is_bottom(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >::sequence, Parma_Polyhedra_Library::Pointset_Powerset< PS >::space_dim, and Parma_Polyhedra_Library::Pointset_Powerset< PS >::swap().

00092                                                                     {
00093   Pointset_Powerset& x = *this;
00094   // Ensure omega-reduction here, since what follows has quadratic complexity.
00095   x.omega_reduce();
00096   y.omega_reduce();
00097   Pointset_Powerset<PS> 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       PS xph = xi->element();
00110       for (++xi; xi != x_end; ++xi)
00111         xph.upper_bound_assign(xi->element());
00112       const_iterator yi = y_begin;
00113       PS 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 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::remove_space_dimensions ( const Variables_Set &  to_be_removed  )  [inline]

Removes all the specified space dimensions.

Parameters:
to_be_removed The set of Variable objects corresponding to the space dimensions to be removed.
Exceptions:
std::invalid_argument Thrown if *this is dimension-incompatible with one of the Variable objects contained in to_be_removed.

Definition at line 330 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, Parma_Polyhedra_Library::Powerset< D >::sequence, and Parma_Polyhedra_Library::Pointset_Powerset< PS >::space_dim.

00330                                                             {
00331   Pointset_Powerset& x = *this;
00332   Variables_Set::size_type num_removed = to_be_removed.size();
00333   if (num_removed > 0) {
00334     for (Sequence_iterator si = x.sequence.begin(),
00335            s_end = x.sequence.end(); si != s_end; ++si) {
00336       si->element().remove_space_dimensions(to_be_removed);
00337       x.reduced = false;
00338     }
00339     x.space_dim -= num_removed;
00340     assert(x.OK());
00341   }
00342 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::remove_higher_space_dimensions ( dimension_type  new_dimension  )  [inline]

Removes the higher space dimensions so that the resulting space will have dimension new_dimension.

Exceptions:
std::invalid_argument Thrown if new_dimensions is greater than the space dimension of *this.

Definition at line 346 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, Parma_Polyhedra_Library::Powerset< D >::sequence, and Parma_Polyhedra_Library::Pointset_Powerset< PS >::space_dim.

00347                                                                      {
00348   Pointset_Powerset& x = *this;
00349   if (new_dimension < x.space_dim) {
00350     for (Sequence_iterator si = x.sequence.begin(),
00351            s_end = x.sequence.end(); si != s_end; ++si) {
00352       si->element().remove_higher_space_dimensions(new_dimension);
00353       x.reduced = false;
00354     }
00355     x.space_dim = new_dimension;
00356     assert(x.OK());
00357   }
00358 }

template<typename PS>
template<typename Partial_Function>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::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 363 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::is_bottom(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::reduced, Parma_Polyhedra_Library::Powerset< D >::sequence, and Parma_Polyhedra_Library::Pointset_Powerset< PS >::space_dim.

00363                                                                          {
00364   Pointset_Powerset& x = *this;
00365   if (x.is_bottom()) {
00366     dimension_type n = 0;
00367     for (dimension_type i = x.space_dim; i-- > 0; ) {
00368       dimension_type new_i;
00369       if (pfunc.maps(i, new_i))
00370         ++n;
00371     }
00372     x.space_dim = n;
00373   }
00374   else {
00375     Sequence_iterator s_begin = x.sequence.begin();
00376     for (Sequence_iterator si = s_begin,
00377            s_end = x.sequence.end(); si != s_end; ++si)
00378       si->element().map_space_dimensions(pfunc);
00379     x.space_dim = s_begin->element().space_dimension();
00380     x.reduced = false;
00381   }
00382   assert(x.OK());
00383 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::expand_space_dimension ( Variable  var,
dimension_type  m 
) [inline]

Creates m copies of the space dimension corresponding to var.

Parameters:
var The variable corresponding to the space dimension to be replicated;
m The number of replicas to be created.
Exceptions:
std::invalid_argument Thrown if var does not correspond to a dimension of the vector space.
std::length_error Thrown if adding m new space dimensions would cause the vector space to exceed dimension max_space_dimension().
If *this has space dimension $n$, with $n > 0$, and var has space dimension $k \leq n$, then the $k$-th space dimension is expanded to m new space dimensions $n$, $n+1$, $\dots$, $n+m-1$.

Definition at line 387 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::sequence, and Parma_Polyhedra_Library::Pointset_Powerset< PS >::space_dim.

00388                                                                 {
00389   Pointset_Powerset& x = *this;
00390   for (Sequence_iterator si = x.sequence.begin(),
00391          s_end = x.sequence.end(); si != s_end; ++si)
00392     si->element().expand_space_dimension(var, m);
00393   x.space_dim += m;
00394   assert(x.OK());
00395 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::fold_space_dimensions ( const Variables_Set &  to_be_folded,
Variable  var 
) [inline]

Folds the space dimensions in to_be_folded into var.

Parameters:
to_be_folded The set of Variable objects corresponding to the space dimensions to be folded;
var The variable corresponding to the space dimension that is the destination of the folding operation.
Exceptions:
std::invalid_argument Thrown if *this is dimension-incompatible with var or with one of the Variable objects contained in to_be_folded. Also thrown if var is contained in to_be_folded.
If *this has space dimension $n$, with $n > 0$, var has space dimension $k \leq n$, to_be_folded is a set of variables whose maximum space dimension is also less than or equal to $n$, and var is not a member of to_be_folded, then the space dimensions corresponding to variables in to_be_folded are folded into the $k$-th space dimension.

Definition at line 399 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::sequence, and Parma_Polyhedra_Library::Pointset_Powerset< PS >::space_dim.

00400                                                            {
00401   Pointset_Powerset& x = *this;
00402   Variables_Set::size_type num_folded = to_be_folded.size();
00403   if (num_folded > 0) {
00404     for (Sequence_iterator si = x.sequence.begin(),
00405            s_end = x.sequence.end(); si != s_end; ++si)
00406       si->element().fold_space_dimensions(to_be_folded, var);
00407   }
00408   x.space_dim -= num_folded;
00409   assert(x.OK());
00410 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::ascii_dump (  )  const

Writes to std::cerr an ASCII representation of *this.

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::ascii_dump ( std::ostream &  s  )  const [inline]

Writes to s an ASCII representation of *this.

Definition at line 1464 of file Pointset_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::Pointset_Powerset< PS >::space_dim.

01464                                                      {
01465   const Pointset_Powerset& x = *this;
01466   s << "size " << x.size()
01467     << "\nspace_dim " << x.space_dim
01468     << "\n";
01469   for (const_iterator xi = x.begin(), x_end = x.end(); xi != x_end; ++xi)
01470     xi->element().ascii_dump(s);
01471 }

template<typename PS>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::print (  )  const

Prints *this to std::cerr using operator<<.

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::ascii_load ( std::istream &  s  )  [inline]

Loads from s an ASCII representation (as produced by ascii_dump(std::ostream&) const) and sets *this accordingly. Returns true if successful, false otherwise.

Definition at line 1477 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_disjunct(), Parma_Polyhedra_Library::EMPTY, Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::space_dim, and Parma_Polyhedra_Library::Pointset_Powerset< PS >::swap().

01477                                                {
01478   Pointset_Powerset& x = *this;
01479   std::string str;
01480 
01481   if (!(s >> str) || str != "size")
01482     return false;
01483 
01484   size_type sz;
01485 
01486   if (!(s >> sz))
01487     return false;
01488 
01489   if (!(s >> str) || str != "space_dim")
01490     return false;
01491 
01492   if (!(s >> x.space_dim))
01493     return false;
01494 
01495   Pointset_Powerset new_x(x.space_dim, EMPTY);
01496   while (sz-- > 0) {
01497     PS ph;
01498     if (!ph.ascii_load(s))
01499       return false;
01500     new_x.add_disjunct(ph);
01501   }
01502   x.swap(new_x);
01503 
01504   // Check invariants.
01505   assert(x.OK());
01506   return true;
01507 }

template<typename PS>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::intersection_preserving_enlarge_element ( PS &  to_be_enlarged  )  const [inline, private]

Assigns to to_be_enlarged a powerset meet-preserving enlargement of itself with respect to *this. If false is returned, then the intersection is empty.

Note:
It is assumed that *this and to_be_enlarged are topology-compatible and dimension-compatible.

Definition at line 694 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::sequence, Parma_Polyhedra_Library::Pointset_Powerset< PS >::space_dimension(), and Parma_Polyhedra_Library::UNIVERSE.

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::simplify_using_context_assign().

00694                                                                   {
00695   // FIXME: this is just an executable specification.
00696   const Pointset_Powerset& context = *this;
00697   assert(context.space_dimension() == to_be_enlarged.space_dimension());
00698   bool nonempty_intersection = false;
00699   // TODO: maybe use a *sorted* constraint system?
00700   PS enlarged(context.space_dimension(), UNIVERSE);
00701   for (Sequence_const_iterator si = context.sequence.begin(),
00702          s_end = context.sequence.end(); si != s_end; ++si) {
00703     PS context_i(si->element());
00704     context_i.intersection_assign(enlarged);
00705     PS enlarged_i(to_be_enlarged);
00706     nonempty_intersection
00707       |= enlarged_i.simplify_using_context_assign(context_i);
00708     // TODO: merge the sorted constraints of `enlarged' and `enlarged_i'?
00709     enlarged.intersection_assign(enlarged_i);
00710   }
00711   to_be_enlarged.swap(enlarged);
00712   return nonempty_intersection;
00713 }

template<typename PS>
template<typename Widening>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::BGP99_heuristics_assign ( const Pointset_Powerset< PS > &  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 1211 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::add_non_bottom_disjunct_preserve_reduction(), Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >::definitely_entails(), Parma_Polyhedra_Library::EMPTY, Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Powerset< D >::is_omega_reduced(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::sequence, Parma_Polyhedra_Library::Powerset< D >::size(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::space_dim, and Parma_Polyhedra_Library::swap().

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::BGP99_extrapolation_assign(), and Parma_Polyhedra_Library::Pointset_Powerset< PS >::BHZ03_widening_assign().

01211                                                                  {
01212   // `x' is the current iteration value.
01213   Pointset_Powerset& x = *this;
01214 
01215 #ifndef NDEBUG
01216   {
01217     // We assume that `y' entails `x'.
01218     const Pointset_Powerset<PS> x_copy = x;
01219     const Pointset_Powerset<PS> y_copy = y;
01220     assert(y_copy.definitely_entails(x_copy));
01221   }
01222 #endif
01223 
01224   size_type n = x.size();
01225   Pointset_Powerset new_x(x.space_dim, EMPTY);
01226   std::deque<bool> marked(n, false);
01227   const_iterator x_begin = x.begin();
01228   const_iterator x_end = x.end();
01229   unsigned i_index = 0;
01230   for (const_iterator i = x_begin,
01231          y_begin = y.begin(), y_end = y.end(); i != x_end; ++i, ++i_index)
01232     for (const_iterator j = y_begin; j != y_end; ++j) {
01233       const PS& pi = i->element();
01234       const PS& pj = j->element();
01235       if (pi.contains(pj)) {
01236         PS pi_copy = pi;
01237         wf(pi_copy, pj);
01238         // FIXME: check whether the preservation of reduction was
01239         // actually meant here.
01240         new_x.add_non_bottom_disjunct_preserve_reduction(pi_copy);
01241         marked[i_index] = true;
01242       }
01243     }
01244   iterator nx_begin = new_x.begin();
01245   iterator nx_end = new_x.end();
01246   i_index = 0;
01247   for (const_iterator i = x_begin; i != x_end; ++i, ++i_index)
01248     if (!marked[i_index])
01249       nx_begin = new_x.add_non_bottom_disjunct_preserve_reduction(*i,
01250                                                                   nx_begin,
01251                                                                   nx_end);
01252   std::swap(x.sequence, new_x.sequence);
01253   assert(x.OK());
01254   assert(x.is_omega_reduced());
01255 }

template<typename PS>
template<typename Cert>
void Parma_Polyhedra_Library::Pointset_Powerset< PS >::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 disjuncts.

Definition at line 1286 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >::end(), and Parma_Polyhedra_Library::Powerset< D >::is_omega_reduced().

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::BHZ03_widening_assign(), and Parma_Polyhedra_Library::Pointset_Powerset< PS >::is_cert_multiset_stabilizing().

01287                                                            {
01288   const Pointset_Powerset& x = *this;
01289   assert(x.is_omega_reduced());
01290   assert(cert_ms.size() == 0);
01291   for (const_iterator i = x.begin(), end = x.end(); i != end; i++) {
01292     Cert ph_cert(i->element());
01293     ++cert_ms[ph_cert];
01294   }
01295 }

template<typename PS>
template<typename Cert>
bool Parma_Polyhedra_Library::Pointset_Powerset< PS >::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 dijsuncts is stabilizing with respect to the multiset of certificates y_cert_ms.

Definition at line 1301 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::collect_certificates().

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::BHZ03_widening_assign().

01303                                      {
01304   typedef std::map<Cert, size_type, typename Cert::Compare> Cert_Multiset;
01305   Cert_Multiset x_cert_ms;
01306   collect_certificates(x_cert_ms);
01307   typename Cert_Multiset::const_iterator
01308     xi = x_cert_ms.begin(),
01309     x_cert_ms_end = x_cert_ms.end(),
01310     yi = y_cert_ms.begin(),
01311     y_cert_ms_end = y_cert_ms.end();
01312   while (xi != x_cert_ms_end && yi != y_cert_ms_end) {
01313     const Cert& xi_cert = xi->first;
01314     const Cert& yi_cert = yi->first;
01315     switch (xi_cert.compare(yi_cert)) {
01316     case 0:
01317       // xi_cert == yi_cert: check the number of multiset occurrences.
01318       {
01319         const size_type& xi_count = xi->second;
01320         const size_type& yi_count = yi->second;
01321         if (xi_count == yi_count) {
01322           // Same number of occurrences: compare the next pair.
01323           ++xi;
01324           ++yi;
01325         }
01326         else
01327           // Different number of occurrences: can decide ordering.
01328           return xi_count < yi_count;
01329         break;
01330       }
01331     case 1:
01332       // xi_cert > yi_cert: it is not stabilizing.
01333       return false;
01334 
01335     case -1:
01336       // xi_cert < yi_cert: it is stabilizing.
01337       return true;
01338     }
01339   }
01340   // Here xi == x_cert_ms_end or yi == y_cert_ms_end.
01341   // Stabilization is achieved if `y_cert_ms' still has other elements.
01342   return yi != y_cert_ms_end;
01343 }

template<>
void Parma_Polyhedra_Library::Pointset_Powerset< NNC_Polyhedron >::difference_assign ( const Pointset_Powerset< PS > &  y  )  [inline]

template<>
void Parma_Polyhedra_Library::Pointset_Powerset< Grid >::difference_assign ( const Pointset_Powerset< PS > &  y  )  [inline]

template<>
bool Parma_Polyhedra_Library::Pointset_Powerset< NNC_Polyhedron >::geometrically_covers ( const Pointset_Powerset< PS > &  y  )  const [inline]

template<>
bool Parma_Polyhedra_Library::Pointset_Powerset< Grid >::geometrically_covers ( const Pointset_Powerset< PS > &  y  )  const [inline]

template<>
bool Parma_Polyhedra_Library::Pointset_Powerset< Grid >::geometrically_equals ( const Pointset_Powerset< PS > &  y  )  const [inline]

Definition at line 254 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::geometrically_covers().

00254                                                        {
00255   const Pointset_Powerset& x = *this;
00256   return x.geometrically_covers(y) && y.geometrically_covers(x);
00257 }

template<>
bool Parma_Polyhedra_Library::Pointset_Powerset< NNC_Polyhedron >::geometrically_equals ( const Pointset_Powerset< PS > &  y  )  const [inline]

Definition at line 262 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::geometrically_covers().

00262                                                        {
00263   const Pointset_Powerset& x = *this;
00264   return x.geometrically_covers(y) && y.geometrically_covers(x);
00265 }

template<>
void Parma_Polyhedra_Library::Pointset_Powerset< PPL::NNC_Polyhedron >::difference_assign ( const Pointset_Powerset< PS > &  y  )  [inline]

Definition at line 33 of file Pointset_Powerset.cc.

References Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::linear_partition(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), Parma_Polyhedra_Library::Powerset< D >::reduced, Parma_Polyhedra_Library::Powerset< D >::sequence, and Parma_Polyhedra_Library::swap().

00033                                               {
00034   Pointset_Powerset& x = *this;
00035   // Ensure omega-reduction.
00036   x.omega_reduce();
00037   y.omega_reduce();
00038   Sequence new_sequence = x.sequence;
00039   for (const_iterator yi = y.begin(), y_end = y.end(); yi != y_end; ++yi) {
00040     const NNC_Polyhedron& py = yi->element();
00041     Sequence tmp_sequence;
00042     for (Sequence_const_iterator nsi = new_sequence.begin(),
00043            ns_end = new_sequence.end(); nsi != ns_end; ++nsi) {
00044       std::pair<NNC_Polyhedron, Pointset_Powerset<NNC_Polyhedron> > partition
00045         = linear_partition(py, nsi->element());
00046       const Pointset_Powerset<NNC_Polyhedron>& residues = partition.second;
00047       // Append the contents of `residues' to `tmp_sequence'.
00048       std::copy(residues.begin(), residues.end(), back_inserter(tmp_sequence));
00049     }
00050     std::swap(tmp_sequence, new_sequence);
00051   }
00052   std::swap(x.sequence, new_sequence);
00053   x.reduced = false;
00054   assert(x.OK());
00055 }

template<>
bool Parma_Polyhedra_Library::Pointset_Powerset< PPL::NNC_Polyhedron >::geometrically_covers ( const Pointset_Powerset< PS > &  y  )  const [inline]

Definition at line 60 of file Pointset_Powerset.cc.

References Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::check_containment(), and Parma_Polyhedra_Library::Powerset< D >::end().

00060                                                        {
00061   const Pointset_Powerset& x = *this;
00062   for (const_iterator yi = y.begin(), y_end = y.end(); yi != y_end; ++yi)
00063     if (!check_containment(yi->element(), x))
00064       return false;
00065   return true;
00066 }

template<>
void Parma_Polyhedra_Library::Pointset_Powerset< PPL::Grid >::difference_assign ( const Pointset_Powerset< PS > &  y  )  [inline]

Definition at line 257 of file Pointset_Powerset.cc.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::approximate_partition(), Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Powerset< D >::end(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::OK(), Parma_Polyhedra_Library::Powerset< D >::omega_reduce(), Parma_Polyhedra_Library::Powerset< D >::reduced, Parma_Polyhedra_Library::Powerset< D >::sequence, and Parma_Polyhedra_Library::swap().

00257                                               {
00258   Pointset_Powerset& x = *this;
00259   // Ensure omega-reduction.
00260   x.omega_reduce();
00261   y.omega_reduce();
00262   Sequence new_sequence = x.sequence;
00263   for (const_iterator yi = y.begin(), y_end = y.end(); yi != y_end; ++yi) {
00264     const Grid& py = yi->element();
00265     Sequence tmp_sequence;
00266     for (Sequence_const_iterator nsi = new_sequence.begin(),
00267            ns_end = new_sequence.end(); nsi != ns_end; ++nsi) {
00268       bool finite_partition;
00269       std::pair<Grid, Pointset_Powerset<Grid> > partition
00270         = approximate_partition(py, nsi->element(), finite_partition);
00271       const Pointset_Powerset<Grid>& residues = partition.second;
00272       // Append the contents of `residues' to `tmp_sequence'.
00273       std::copy(residues.begin(), residues.end(), back_inserter(tmp_sequence));
00274     }
00275     std::swap(tmp_sequence, new_sequence);
00276   }
00277   std::swap(x.sequence, new_sequence);
00278   x.reduced = false;
00279   assert(x.OK());
00280 }

template<>
bool Parma_Polyhedra_Library::Pointset_Powerset< PPL::Grid >::geometrically_covers ( const Pointset_Powerset< PS > &  y  )  const [inline]

Definition at line 285 of file Pointset_Powerset.cc.

References Parma_Polyhedra_Library::Powerset< D >::begin(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::check_containment(), and Parma_Polyhedra_Library::Powerset< D >::end().

00285                                                        {
00286   const Pointset_Powerset& x = *this;
00287   for (const_iterator yi = y.begin(), y_end = y.end(); yi != y_end; ++yi)
00288     if (!check_containment(yi->element(), x))
00289       return false;
00290   return true;
00291 }


Friends And Related Function Documentation

template<typename PS>
friend class Pointset_Powerset< NNC_Polyhedron > [friend]

Definition at line 1297 of file Pointset_Powerset.defs.hh.

template<typename PH>
Widening_Function< PH > widen_fun_ref ( void(PH::*)(const PH &, unsigned *)  wm  )  [related]

Wraps a widening method into a function object.

Parameters:
wm The widening method.

Definition at line 59 of file Widening_Function.inlines.hh.

00059                                                    {
00060   return Widening_Function<PH>(wm);
00061 }

template<typename PH, typename CS>
Limited_Widening_Function< PH, CS > widen_fun_ref ( void(PH::*)(const PH &, const CS &, unsigned *)  lwm,
const CS cs 
) [related]

Wraps a limited widening method into a function object.

Parameters:
lwm The limited widening method.
cs The constraint system limiting the widening.

Definition at line 66 of file Widening_Function.inlines.hh.

00067                             {
00068   return Limited_Widening_Function<PH, CS>(lwm, cs);
00069 }

template<typename PS>
std::pair< PS, Pointset_Powerset< NNC_Polyhedron > > linear_partition ( const PS &  p,
const PS &  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<PS, Pointset_Powerset<NNC_Polyhedron> > such that

  • r.first is the intersection of p and q;
  • r.second has the property that all its elements are pairwise disjoint and disjoint from p;
  • the set-theoretical union of 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 1562 of file Pointset_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(), Parma_Polyhedra_Library::Checked::le(), and Parma_Polyhedra_Library::Pointset_Powerset< PS >::linear_partition_aux().

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::check_containment(), and Parma_Polyhedra_Library::Pointset_Powerset< PS >::difference_assign().

01562                                            {
01563   using Implementation::Pointset_Powersets::linear_partition_aux;
01564 
01565   Pointset_Powerset<NNC_Polyhedron> r(p.space_dimension(), EMPTY);
01566   PS qq = q;
01567   const Constraint_System& pcs = p.constraints();
01568   for (Constraint_System::const_iterator i = pcs.begin(),
01569          pcs_end = pcs.end(); i != pcs_end; ++i) {
01570     const Constraint& c = *i;
01571     if (c.is_equality()) {
01572       Linear_Expression le(c);
01573       linear_partition_aux(le <= 0, qq, r);
01574       linear_partition_aux(le >= 0, qq, r);
01575     }
01576     else
01577       linear_partition_aux(c, qq, r);
01578   }
01579   return std::make_pair(qq, r);
01580 }

template<typename PS>
bool check_containment ( const NNC_Polyhedron ph,
const Pointset_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 70 of file Pointset_Powerset.cc.

References Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >::begin(), Parma_Polyhedra_Library::Polyhedron::contains(), Parma_Polyhedra_Library::EMPTY, Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >::end(), Parma_Polyhedra_Library::Polyhedron::is_disjoint_from(), Parma_Polyhedra_Library::Polyhedron::is_empty(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::linear_partition(), and Parma_Polyhedra_Library::Polyhedron::space_dimension().

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::check_containment(), and Parma_Polyhedra_Library::Pointset_Powerset< PS >::geometrically_covers().

00071                                                                     {
00072   if (ph.is_empty())
00073     return true;
00074   Pointset_Powerset<NNC_Polyhedron> tmp(ph.space_dimension(), EMPTY);
00075   tmp.add_disjunct(ph);
00076   for (Pointset_Powerset<NNC_Polyhedron>::const_iterator
00077          i = ps.begin(), ps_end = ps.end(); i != ps_end; ++i) {
00078     const NNC_Polyhedron& pi = i->element();
00079     for (Pointset_Powerset<NNC_Polyhedron>::iterator
00080            j = tmp.begin(); j != tmp.end(); ) {
00081       const NNC_Polyhedron& pj = j->element();
00082       if (pi.contains(pj))
00083         j = tmp.drop_disjunct(j);
00084       else
00085         ++j;
00086     }
00087     if (tmp.empty())
00088       return true;
00089     else {
00090       Pointset_Powerset<NNC_Polyhedron> new_disjuncts(ph.space_dimension(),
00091                                                       EMPTY);
00092       for (Pointset_Powerset<NNC_Polyhedron>::iterator
00093              j = tmp.begin(); j != tmp.end(); ) {
00094         const NNC_Polyhedron& pj = j->element();
00095         if (pj.is_disjoint_from(pi))
00096           ++j;
00097         else {
00098           std::pair<NNC_Polyhedron, Pointset_Powerset<NNC_Polyhedron> >
00099             partition = linear_partition(pi, pj);
00100           new_disjuncts.upper_bound_assign(partition.second);
00101           j = tmp.drop_disjunct(j);
00102         }
00103       }
00104       tmp.upper_bound_assign(new_disjuncts);
00105     }
00106   }
00107   return false;
00108 }

template<typename PS>
std::pair< PPL::Grid, PPL::Pointset_Powerset< PPL::Grid > > approximate_partition ( const Grid p,
const Grid q,
bool &  finite_partition 
) [related]

Partitions the grid q with respect to grid p if and only if such a partition is finite.

Let p and q be two grids. The function returns an object r of type std::pair<PS, Pointset_Powerset<Grid> > such that

  • r.first is the intersection of p and q;
  • If there is a finite partition of q wrt p the Boolean finite_partition is set to true and r.second has the property that all its elements are pairwise disjoint and disjoint from p and the set-theoretical union of r.first with all the elements of r.second gives q (i.e., r is the representation of a partition of q).
  • Otherwise the Boolean finite_partition is set to false and the singleton set that contains q is stored in r.secondr.

Definition at line 181 of file Pointset_Powerset.cc.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::approximate_partition_aux(), Parma_Polyhedra_Library::Congruence_System::begin(), Parma_Polyhedra_Library::Grid::congruences(), Parma_Polyhedra_Library::EMPTY, Parma_Polyhedra_Library::Congruence_System::end(), Parma_Polyhedra_Library::Grid::minimized_congruences(), and Parma_Polyhedra_Library::Grid::space_dimension().

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::check_containment(), and Parma_Polyhedra_Library::Pointset_Powerset< PS >::difference_assign().

00182                                                    {
00183   using namespace PPL;
00184   finite_partition = true;
00185   Pointset_Powerset<Grid> r(p.space_dimension(), EMPTY);
00186   // Ensure that the congruence system of q is minimized
00187   // before copying and calling approximate_partition_aux().
00188   (void) q.minimized_congruences();
00189   Grid qq = q;
00190   const Congruence_System& pcs = p.congruences();
00191   for (Congruence_System::const_iterator i = pcs.begin(),
00192          pcs_end = pcs.end(); i != pcs_end; ++i)
00193     if (!approximate_partition_aux(*i, qq, r)) {
00194       finite_partition = false;
00195       Pointset_Powerset<Grid> s(q);
00196       return std::make_pair(qq, s);
00197     }
00198   return std::make_pair(qq, r);
00199 }

template<typename PS>
bool check_containment ( const Grid ph,
const Pointset_Powerset< Grid > &  ps 
) [related]

Returns true if and only if the union of the grids ps contains the grid g.

Definition at line 203 of file Pointset_Powerset.cc.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::approximate_partition(), Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >::begin(), Parma_Polyhedra_Library::Grid::contains(), Parma_Polyhedra_Library::EMPTY, Parma_Polyhedra_Library::Powerset< Parma_Polyhedra_Library::Determinate< PS > >::end(), Parma_Polyhedra_Library::Grid::is_disjoint_from(), Parma_Polyhedra_Library::Grid::is_empty(), and Parma_Polyhedra_Library::Grid::space_dimension().

00204                                                           {
00205   if (ph.is_empty())
00206     return true;
00207   Pointset_Powerset<Grid> tmp(ph.space_dimension(), EMPTY);
00208   tmp.add_disjunct(ph);
00209   for (Pointset_Powerset<Grid>::const_iterator
00210          i = ps.begin(), ps_end = ps.end(); i != ps_end; ++i) {
00211     const Grid& pi = i->element();
00212     for (Pointset_Powerset<Grid>::iterator
00213            j = tmp.begin(); j != tmp.end(); ) {
00214       const Grid& pj = j->element();
00215       if (pi.contains(pj))
00216         j = tmp.drop_disjunct(j);
00217       else
00218         ++j;
00219     }
00220     if (tmp.empty())
00221       return true;
00222     else {
00223       Pointset_Powerset<Grid> new_disjuncts(ph.space_dimension(),
00224                                                       EMPTY);
00225       for (Pointset_Powerset<Grid>::iterator
00226              j = tmp.begin(); j != tmp.end(); ) {
00227         const Grid& pj = j->element();
00228         if (pj.is_disjoint_from(pi))
00229           ++j;
00230         else {
00231           bool finite_partition;
00232           std::pair<Grid, Pointset_Powerset<Grid> >
00233             partition = approximate_partition(pi, pj, finite_partition);
00234 
00235           // If there is a finite partition, then we add the new
00236           // disjuncts to the temporary set of disjuncts and drop pj.
00237           // If there is no finite partition, then by the
00238           // specification of approximate_partition(), we can
00239           // ignore checking the remaining temporary disjuncts as they
00240           // will all have the same lines and equalities and therefore
00241           // also not have a finite partition wrt pi.
00242           if (!finite_partition)
00243             break;
00244           new_disjuncts.upper_bound_assign(partition.second);
00245           j = tmp.drop_disjunct(j);
00246         }
00247       }
00248       tmp.upper_bound_assign(new_disjuncts);
00249     }
00250   }
00251   return false;
00252 }

template<typename PS>
bool check_containment ( const PS &  ph,
const Pointset_Powerset< PS > &  ps 
) [related]

Returns true if and only if the union of the objects in ps contains ph.

Note:
It is assumed that the template parameter PS can be converted without precision loss into an NNC_Polyhedron; otherwise, an incorrect result might be obtained.

Definition at line 299 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::check_containment().

00299                                                                  {
00300   // This code is only used when PS is an abstraction of NNC_Polyhedron.
00301   const NNC_Polyhedron pph = NNC_Polyhedron(ph.constraints());
00302   const Pointset_Powerset<NNC_Polyhedron> pps(ps);
00303   return check_containment(pph, pps);
00304 }

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

Specializes std::swap.

Definition at line 323 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::swap().

00324                                                       {
00325   x.swap(y);
00326 }

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

Definition at line 309 of file Pointset_Powerset.inlines.hh.

References Parma_Polyhedra_Library::Pointset_Powerset< PS >::check_containment().

00310                                                              {
00311   return check_containment(NNC_Polyhedron(ph),
00312                            Pointset_Powerset<NNC_Polyhedron>(ps));
00313 }

template<typename PS>
void linear_partition_aux ( const Constraint c,
PS &  qq,
Pointset_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 1542 of file Pointset_Powerset.templates.hh.

References Parma_Polyhedra_Library::Polyhedron::add_constraint(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_disjunct(), Parma_Polyhedra_Library::Polyhedron::is_empty(), Parma_Polyhedra_Library::Constraint::is_strict_inequality(), and Parma_Polyhedra_Library::Checked::le().

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::linear_partition().

01544                                                            {
01545   Linear_Expression le(c);
01546   const Constraint& neg_c = c.is_strict_inequality() ? (le <= 0) : (le < 0);
01547   NNC_Polyhedron qqq(qq);
01548   qqq.add_constraint(neg_c);
01549   if (!qqq.is_empty())
01550     r.add_disjunct(qqq);
01551   qq.add_constraint(c);
01552 }

template<typename PS>
bool approximate_partition_aux ( const PPL::Congruence c,
PPL::Grid qq,
PPL::Pointset_Powerset< PPL::Grid > &  r 
) [related]

Uses the congruence c to approximately partition the grid qq.

On exit, the intersection of qq and congruence c is stored in qq, whereas a finite set of grids whose set-theoretic union contains the intersection of qq with the negation of c is added, as a set of new disjuncts, to the powerset r.

Definition at line 123 of file Pointset_Powerset.cc.

References Parma_Polyhedra_Library::Grid::add_congruence(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::add_disjunct(), Parma_Polyhedra_Library::Grid::congruences(), Parma_Polyhedra_Library::Congruence::inhomogeneous_term(), Parma_Polyhedra_Library::Grid::is_empty(), Parma_Polyhedra_Library::Checked::le(), Parma_Polyhedra_Library::Congruence::modulus(), Parma_Polyhedra_Library::Congruence_System::num_equalities(), Parma_Polyhedra_Library::Congruence_System::num_proper_congruences(), Parma_Polyhedra_Library::rem_assign(), and TEMP_INTEGER.

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PS >::approximate_partition().

00125                                                             {
00126   using namespace PPL;
00127   const Coefficient& c_modulus = c.modulus();
00128   Grid qq_copy(qq);
00129   qq.add_congruence(c);
00130   if (qq.is_empty()) {
00131     r.add_disjunct(qq_copy);
00132     return true;
00133   }
00134 
00135   Congruence_System cgs = qq.congruences();
00136   Congruence_System cgs_copy = qq_copy.congruences();
00137   // When c is an equality, not satisfied by Grid qq
00138   // then add qq to the set r. There is no finite
00139   // partition in this case.
00140   if (c_modulus == 0) {
00141     if (cgs.num_equalities() != cgs_copy.num_equalities()) {
00142       r.add_disjunct(qq_copy);
00143       return false;
00144     }
00145     return true;
00146   }
00147 
00148   // When c is a proper congruence but, in qq, this direction has
00149   // no congruence, then add qq to the set r. There is no finite
00150   // partition in this case.
00151   if (cgs.num_proper_congruences() != cgs_copy.num_proper_congruences()) {
00152     r.add_disjunct(qq_copy);
00153     return false;
00154   }
00155 
00156   // When  c is a proper congruence and qq also is discrete
00157   // in this direction, then there is a finite partition and that
00158   // is added to r.
00159   const Coefficient& c_inhomogeneous_term = c.inhomogeneous_term();
00160   Linear_Expression le(c);
00161   le -= c_inhomogeneous_term;
00162   TEMP_INTEGER(n);
00163   rem_assign(n, c_inhomogeneous_term, c_modulus);
00164   if (n < 0)
00165     n += c_modulus;
00166   TEMP_INTEGER(i);
00167   for (i = c_modulus; i-- > 0; )
00168     if (i != n) {
00169       Grid qqq(qq_copy);
00170       qqq.add_congruence((le+i %= 0) / c_modulus);
00171       if (!qqq.is_empty())
00172         r.add_disjunct(qqq);
00173     }
00174   return true;
00175 }


Member Data Documentation


The documentation for this class was generated from the following files:

Generated on Sat Oct 11 10:41:14 2008 for PPL by  doxygen 1.5.6