Parma_Polyhedra_Library::BD_Shape< T > Class Template Reference
[C++ Language Interface]

A bounded difference shape. More...

List of all members.

Public Types

typedef T base_type
 The numeric base type upon which bounded differences are built.
typedef N coefficient_type
 The (extended) numeric type of the inhomogeneous term of the inequalities defining a BDS.

Public Member Functions

Constructors, Assignment, Swap and Destructor
 BD_Shape (dimension_type num_dimensions=0, Degenerate_Element kind=UNIVERSE)
 Builds a universe or empty BDS of the specified space dimension.
 BD_Shape (const BD_Shape &y)
 Ordinary copy-constructor.
template<typename U>
 BD_Shape (const BD_Shape< U > &y)
 Builds a conservative, upward approximation of y.
 BD_Shape (const Constraint_System &cs)
 Builds a BDS from the system of constraints cs.
 BD_Shape (const Generator_System &gs)
 Builds a BDS from the system of generators gs.
 BD_Shape (const Polyhedron &ph, Complexity_Class complexity=ANY_COMPLEXITY)
 Builds a BDS from the polyhedron ph.
BD_Shapeoperator= (const BD_Shape &y)
 The assignment operator (*this and y can be dimension-incompatible).
void swap (BD_Shape &y)
 Swaps *this with y (*this and y can be dimension-incompatible).
 ~BD_Shape ()
 Destructor.
Member Functions that Do Not Modify the BD_Shape
dimension_type space_dimension () const
 Returns the dimension of the vector space enclosing *this.
dimension_type affine_dimension () const
 Returns $0$, if *this is empty; otherwise, returns the affine dimension of *this.
Constraint_System constraints () const
 Returns a system of constraints defining *this.
Constraint_System minimized_constraints () const
 Returns a minimized system of constraints defining *this.
bool contains (const BD_Shape &y) const
 Returns true if and only if *this contains y.
bool strictly_contains (const BD_Shape &y) const
 Returns true if and only if *this strictly contains y.
Poly_Con_Relation relation_with (const Constraint &c) const
 Returns the relations holding between *this and the constraint c.
Poly_Gen_Relation relation_with (const Generator &g) const
 Returns the relations holding between *this and the generator g.
bool is_empty () const
 Returns true if and only if *this is an empty BDS.
bool is_universe () const
 Returns true if and only if *this is a universe BDS.
bool OK () const
 Returns true if and only if *this satisfies all its invariants.
Space-Dimension Preserving Member Functions that May Modify the BD_Shape
void add_constraint (const Constraint &c)
 Adds a copy of constraint c to the system of bounded differences defining *this.
bool add_constraint_and_minimize (const Constraint &c)
 Adds a copy of constraint c to the system of bounded differences defining *this.
void add_constraints (const Constraint_System &cs)
 Adds the constraints in cs to the system of bounded differences defining *this.
bool add_constraints_and_minimize (const Constraint_System &cs)
 Adds the constraints in cs to the system of bounded differences defining *this.
void intersection_assign (const BD_Shape &y)
 Assigns to *this the intersection of *this and y.
bool intersection_assign_and_minimize (const BD_Shape &y)
 Assigns to *this the intersection of *this and y.
void bds_hull_assign (const BD_Shape &y)
 Assigns to *this the smallest BDS containing the convex union of *this and y.
bool bds_hull_assign_and_minimize (const BD_Shape &y)
 Assigns to *this the smallest BDS containing the convex union of *this and y.
void upper_bound_assign (const BD_Shape &y)
 Same as bds_hull_assign.
bool bds_hull_assign_if_exact (const BD_Shape &y)
 If the bds-hull of *this and y is exact, it is assigned to *this and true is returned, otherwise false is returned.
bool upper_bound_assign_if_exact (const BD_Shape &y)
 Same as bds_hull_assign_if_exact.
void bds_difference_assign (const BD_Shape &y)
 Assigns to *this the poly-difference of *this and y.
void difference_assign (const BD_Shape &y)
 Same as bds_difference_assign.
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 into 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 into 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 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 affine relation $\mathrm{lhs}' \relsym \mathrm{rhs}$, 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 affine relation $\mathrm{var}' \relsym \frac{\mathrm{expr}}{\mathrm{denominator}}$, where $\mathord{\relsym}$ is the relation symbol encoded by relsym.
void time_elapse_assign (const BD_Shape &y)
 Assigns to *this the result of computing the time-elapse between *this and y.
void CC76_extrapolation_assign (const BD_Shape &y, unsigned *tp=0)
 Assigns to *this the result of computing the CC76-extrapolation between *this and y.
template<typename Iterator>
void CC76_extrapolation_assign (const BD_Shape &y, Iterator first, Iterator last, unsigned *tp=0)
 Assigns to *this the result of computing the CC76-extrapolation between *this and y.
void BHMZ05_widening_assign (const BD_Shape &y, unsigned *tp=0)
 Assigns to *this the result of computing the BHMZ05-widening of *this and y.
void limited_BHMZ05_extrapolation_assign (const BD_Shape &y, const Constraint_System &cs, unsigned *tp=0)
 Improves the result of the BHMZ05-widening computation by also enforcing those constraints in cs that are satisfied by all the points of *this.
void CC76_narrowing_assign (const BD_Shape &y)
 Assigns to *this the result of restoring in y the constraints of *this that were lost by CC76-extrapolation applications.
void limited_CC76_extrapolation_assign (const BD_Shape &y, const Constraint_System &cs, unsigned *tp=0)
 Improves the result of the CC76-extrapolation computation by also enforcing those constraints in cs that are satisfied by all the points of *this.
void H79_widening_assign (const BD_Shape &y, unsigned *tp=0)
 Assigns to *this the result of computing the H79-widening between *this and y.
void limited_H79_extrapolation_assign (const BD_Shape &y, const Constraint_System &cs, unsigned *tp=0)
 Improves the result of the H79-widening computation by also enforcing those constraints in cs that are satisfied by all the points of *this.
Member Functions that May Modify the Dimension of the Vector Space
void add_space_dimensions_and_embed (dimension_type m)
 Adds m new dimensions and embeds the old BDS into the new space.
void add_space_dimensions_and_project (dimension_type m)
 Adds m new dimensions to the BDS and does not embed it in the new vector space.
void concatenate_assign (const BD_Shape &y)
 Seeing a BDS as a set of tuples (its points), assigns to *this all the tuples that can be obtained by concatenating, in the order given, a tuple of *this with a tuple of y.
void remove_space_dimensions (const Variables_Set &to_be_removed)
 Removes all the specified dimensions.
void remove_higher_space_dimensions (dimension_type new_dimension)
 Removes the higher dimensions so that the resulting space will have dimension new_dimension.
template<typename PartialFunction>
void map_space_dimensions (const PartialFunction &pfunc)
 Remaps the dimensions of the vector space according to a partial function.

Static Public Member Functions

static dimension_type max_space_dimension ()
 Returns the maximum space dimension that a BDS can handle.

Friends

std::ostream & operator<< (std::ostream &s, const BD_Shape< T > &c)
 Output operator.

Related Functions

(Note that these are not member functions.)

bool operator== (const BD_Shape< T > &x, const BD_Shape< T > &y)
 Returns true if and only if x and y are the same BDS.
bool operator!= (const BD_Shape< T > &x, const BD_Shape< T > &y)
 Returns true if and only if x and y aren't the same BDS.
bool rectilinear_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const BD_Shape< T > &x, const BD_Shape< T > &y, const Rounding_Dir dir)
 Computes the rectilinear (or Manhattan) distance between x and y.
bool rectilinear_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const BD_Shape< T > &x, const BD_Shape< T > &y, const Rounding_Dir dir, Temp &tmp0, Temp &tmp1, Temp &tmp2)
 Computes the rectilinear (or Manhattan) distance between x and y.
bool euclidean_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const BD_Shape< T > &x, const BD_Shape< T > &y, const Rounding_Dir dir)
 Computes the euclidean distance between x and y.
bool euclidean_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const BD_Shape< T > &x, const BD_Shape< T > &y, const Rounding_Dir dir, Temp &tmp0, Temp &tmp1, Temp &tmp2)
 Computes the euclidean distance between x and y.
bool l_infinity_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const BD_Shape< T > &x, const BD_Shape< T > &y, const Rounding_Dir dir)
 Computes the $L_\infty$ distance between x and y.
bool l_infinity_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const BD_Shape< T > &x, const BD_Shape< T > &y, const Rounding_Dir dir, Temp &tmp0, Temp &tmp1, Temp &tmp2)
 Computes the $L_\infty$ distance between x and y.
void swap (Parma_Polyhedra_Library::BD_Shape< T > &x, Parma_Polyhedra_Library::BD_Shape< T > &y)
 Specializes std::swap.


Detailed Description

template<typename T>
class Parma_Polyhedra_Library::BD_Shape< T >

A bounded difference shape.

The class template BD_Shape<T> allows for the efficient representation of a restricted kind of topologically closed convex polyhedra called bounded difference shapes (BDSs, for short). The name comes from the fact that the closed affine half-spaces that characterize the polyhedron can be expressed by constraints of the form $\pm x_i \leq k$ or $x_i - x_j \leq k$, where the inhomogeneous term $k$ is a rational number.

Based on the class template type parameter T, a family of extended numbers is built and used to approximate the inhomogeneous term of bounded differences. These extended numbers provide a representation for the value $+\infty$, as well as rounding-aware implementations for several arithmetic functions. The value of the type parameter T may be one of the following:

The user interface for BDSs is meant to be as similar as possible to the one developed for the polyhedron class C_Polyhedron. At the interface level, bounded differences are specified using objects of type Constraint: such a constraint is a bounded difference if it is of the form

\[ a_i x_i - a_j x_j \relsym b \]

where $\mathord{\relsym} \in \{ \leq, =, \geq \}$ and $a_i$, $a_j$, $b$ are integer coefficients such that $a_i = 0$, or $a_j = 0$, or $a_i = a_j$. The user is warned that the above Constraint object will be mapped into a correct approximation that, depending on the expressive power of the chosen template argument T, may loose some precision. In particular, constraint objects that do not encode a bounded difference will be simply (and safely) ignored.

For instance, a Constraint object encoding $3x - 3y \leq 1$ will be approximated by:

On the other hand, a Constraint object encoding $3x - y \leq 1$ will be safely ignored in all of the above cases.

In the following examples it is assumed that the type argument T is one of the possible instances listed above and that variables x, y and z are defined (where they are used) as follows:

    Variable x(0);
    Variable y(1);
    Variable z(2);

Example 1
The following code builds a BDS corresponding to a cube in $\Rset^3$, given as a system of constraints:
    Constraint_System cs;
    cs.insert(x >= 0);
    cs.insert(x <= 1);
    cs.insert(y >= 0);
    cs.insert(y <= 1);
    cs.insert(z >= 0);
    cs.insert(z <= 1);
    BD_Shape<T> bd(cs);
Since only those constraints having the syntactic form of a bounded difference are considered, the following code will build the same BDS as above (i.e., the constraints 7, 8, and 9 are ignored):
    Constraint_System cs;
    cs.insert(x >= 0);
    cs.insert(x <= 1);
    cs.insert(y >= 0);
    cs.insert(y <= 1);
    cs.insert(z >= 0);
    cs.insert(z <= 1);
    cs.insert(x + y <= 0);      // 7
    cs.insert(x - z + x >= 0);  // 8
    cs.insert(3*z - y <= 1);    // 9
    BD_Shape<T> bd(cs);


Constructor & Destructor Documentation

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

Builds a universe or empty BDS of the specified space dimension.

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

template<typename T>
Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape ( const Constraint_System cs  )  [inline]

Builds a BDS from the system of constraints cs.

The BDS inherits the space dimension of cs.

Parameters:
cs A system of constraints: constraints that are not bounded differences are ignored (even though they may have contributed to the space dimension).
Exceptions:
std::invalid_argument Thrown if the system of constraints cs contains strict inequalities.

template<typename T>
Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape ( const Generator_System gs  ) 

Builds a BDS from the system of generators gs.

Builds the smallest BDS containing the polyhedron defined by gs. The BDS inherits the space dimension of gs.

Exceptions:
std::invalid_argument Thrown if the system of generators is not empty but has no points.

template<typename T>
Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape ( const Polyhedron ph,
Complexity_Class  complexity = ANY_COMPLEXITY 
)

Builds a BDS from the polyhedron ph.

Builds a BDS containing ph using algorithms whose complexity does not exceed the one specified by complexity. If complexity is ANY_COMPLEXITY, then the BDS built is the smallest one containing ph.


Member Function Documentation

template<typename T>
bool Parma_Polyhedra_Library::BD_Shape< T >::contains ( const BD_Shape< T > &  y  )  const

Returns true if and only if *this contains y.

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

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

Returns true if and only if *this strictly contains y.

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

template<typename T>
Poly_Con_Relation Parma_Polyhedra_Library::BD_Shape< T >::relation_with ( const Constraint c  )  const

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

Exceptions:
std::invalid_argument Thrown if *this and constraint c are dimension-incompatible or if c is a strict inequality or if c is not a bounded difference constraint.

template<typename T>
Poly_Gen_Relation Parma_Polyhedra_Library::BD_Shape< T >::relation_with ( const Generator g  )  const

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

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

template<typename T>
void Parma_Polyhedra_Library::BD_Shape< T >::add_constraint ( const Constraint c  ) 

Adds a copy of constraint c to the system of bounded differences defining *this.

Parameters:
c The constraint to be added. If it is not a bounded difference, it will be simply ignored.
Exceptions:
std::invalid_argument Thrown if *this and constraint c are dimension-incompatible, or if c is a strict inequality.

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

Adds a copy of constraint c to the system of bounded differences defining *this.

Returns:
false if and only if the result is empty.
Parameters:
c The constraint to be added. If it is not a bounded difference, it will be simply ignored.
Exceptions:
std::invalid_argument Thrown if *this and constraint c are dimension-incompatible, or if c is a strict inequality.

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

Adds the constraints in cs to the system of bounded differences defining *this.

Parameters:
cs The constraints that will be added. Constraints that are not bounded differences will be simply ignored.
Exceptions:
std::invalid_argument Thrown if *this and cs are dimension-incompatible, or if cs contains a strict inequality.

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

Adds the constraints in cs to the system of bounded differences defining *this.

Returns:
false if and only if the result is empty.
Parameters:
cs The constraints that will be added. Constraints that are not bounded differences will be simply ignored.
Exceptions:
std::invalid_argument Thrown if *this and cs are dimension-incompatible, or if cs contains a strict inequality.

template<typename T>
void Parma_Polyhedra_Library::BD_Shape< T >::intersection_assign ( const BD_Shape< T > &  y  ) 

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

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

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

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

Returns:
false if and only if the result is empty.
Exceptions:
std::invalid_argument Thrown if *this and y are dimension-incompatible.

template<typename T>
void Parma_Polyhedra_Library::BD_Shape< T >::bds_hull_assign ( const BD_Shape< T > &  y  ) 

Assigns to *this the smallest BDS containing the convex union of *this and y.

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

template<typename T>
bool Parma_Polyhedra_Library::BD_Shape< T >::bds_hull_assign_and_minimize ( const BD_Shape< T > &  y  )  [inline]

Assigns to *this the smallest BDS containing the convex union of *this and y.

Returns:
false if and only if the result is empty.
Exceptions:
std::invalid_argument Thrown if *this and y are dimension-incompatible.

template<typename T>
bool Parma_Polyhedra_Library::BD_Shape< T >::bds_hull_assign_if_exact ( const BD_Shape< T > &  y  )  [inline]

If the bds-hull of *this and y is exact, it is assigned to *this and true is returned, otherwise false is returned.

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

template<typename T>
void Parma_Polyhedra_Library::BD_Shape< T >::bds_difference_assign ( const BD_Shape< T > &  y  ) 

Assigns to *this the poly-difference of *this and y.

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

template<typename T>
void Parma_Polyhedra_Library::BD_Shape< T >::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 into 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.
Exceptions:
std::invalid_argument Thrown if denominator is zero or if expr and *this are dimension-incompatible or if var is not a dimension of *this.

template<typename T>
void Parma_Polyhedra_Library::BD_Shape< T >::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 into the affine expression specified by expr and denominator.

Parameters:
var The variable to which the affine expression is substituted.
expr The numerator of the affine expression.
denominator The denominator of the affine expression.
Exceptions:
std::invalid_argument Thrown if denominator is zero or if expr and *this are dimension-incompatible or if var is not a dimension of *this.

template<typename T>
void Parma_Polyhedra_Library::BD_Shape< T >::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 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 transfer function.
relsym The relation symbol.
expr The numerator of the right hand side affine expression.
denominator The denominator of the right hand side affine expression.
Exceptions:
std::invalid_argument Thrown if denominator is zero or if expr and *this are dimension-incompatible or if var is not a dimension of *this or if relsym is a strict relation symbol.

template<typename T>
void Parma_Polyhedra_Library::BD_Shape< T >::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 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 relsym is a strict relation symbol.

template<typename T>
void Parma_Polyhedra_Library::BD_Shape< T >::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 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 transfer function.
relsym The relation symbol.
expr The numerator of the right hand side affine expression.
denominator The denominator of the right hand side affine expression.
Exceptions:
std::invalid_argument Thrown if denominator is zero or if expr and *this are dimension-incompatible or if var is not a dimension of *this or if relsym is a strict relation symbol.

template<typename T>
void Parma_Polyhedra_Library::BD_Shape< T >::time_elapse_assign ( const BD_Shape< T > &  y  )  [inline]

Assigns to *this the result of computing the time-elapse between *this and y.

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

template<typename T>
void Parma_Polyhedra_Library::BD_Shape< T >::CC76_extrapolation_assign ( const BD_Shape< T > &  y,
unsigned *  tp = 0 
) [inline]

Assigns to *this the result of computing the CC76-extrapolation between *this and y.

Parameters:
y A BDS that must be contained in *this.
tp An optional pointer to an unsigned variable storing the number of available tokens (to be used when applying the widening with tokens delay technique).
Exceptions:
std::invalid_argument Thrown if *this and y are dimension-incompatible.

template<typename T>
template<typename Iterator>
void Parma_Polyhedra_Library::BD_Shape< T >::CC76_extrapolation_assign ( const BD_Shape< T > &  y,
Iterator  first,
Iterator  last,
unsigned *  tp = 0 
)

Assigns to *this the result of computing the CC76-extrapolation between *this and y.

Parameters:
y A BDS that must be contained in *this.
first An iterator referencing the first stop-point.
last An iterator referencing one past the last stop-point.
tp An optional pointer to an unsigned variable storing the number of available tokens (to be used when applying the widening with tokens delay technique).
Exceptions:
std::invalid_argument Thrown if *this and y are dimension-incompatible.

template<typename T>
void Parma_Polyhedra_Library::BD_Shape< T >::BHMZ05_widening_assign ( const BD_Shape< T > &  y,
unsigned *  tp = 0 
)

Assigns to *this the result of computing the BHMZ05-widening of *this and y.

Parameters:
y A BDS that must be contained in *this.
tp An optional pointer to an unsigned variable storing the number of available tokens (to be used when applying the widening with tokens delay technique).
Exceptions:
std::invalid_argument Thrown if *this and y are dimension-incompatible.

template<typename T>
void Parma_Polyhedra_Library::BD_Shape< T >::limited_BHMZ05_extrapolation_assign ( const BD_Shape< T > &  y,
const Constraint_System cs,
unsigned *  tp = 0 
)

Improves the result of the BHMZ05-widening computation by also enforcing those constraints in cs that are satisfied by all the points of *this.

Parameters:
y A BDS that must be contained in *this.
cs The system of constraints used to improve the widened BDS.
tp An optional pointer to an unsigned variable storing the number of available tokens (to be used when applying the widening with tokens delay technique).
Exceptions:
std::invalid_argument Thrown if *this, y and cs are dimension-incompatible or if cs contains a strict inequality.

template<typename T>
void Parma_Polyhedra_Library::BD_Shape< T >::CC76_narrowing_assign ( const BD_Shape< T > &  y  ) 

Assigns to *this the result of restoring in y the constraints of *this that were lost by CC76-extrapolation applications.

Parameters:
y A BDS that must contain *this.
Exceptions:
std::invalid_argument Thrown if *this and y are dimension-incompatible.
Note:
As was the case for widening operators, the argument y is meant to denote the value computed in the previous iteration step, whereas *this denotes the value computed in the current iteration step (in the descreasing iteration sequence). Hence, the call x.CC76_narrowing_assign(y) will assign to x the result of the computation $\mathtt{y} \Delta \mathtt{x}$.

template<typename T>
void Parma_Polyhedra_Library::BD_Shape< T >::limited_CC76_extrapolation_assign ( const BD_Shape< T > &  y,
const Constraint_System cs,
unsigned *  tp = 0 
)

Improves the result of the CC76-extrapolation computation by also enforcing those constraints in cs that are satisfied by all the points of *this.

Parameters:
y A BDS that must be contained in *this.
cs The system of constraints used to improve the widened BDS.
tp An optional pointer to an unsigned variable storing the number of available tokens (to be used when applying the widening with tokens delay technique).
Exceptions:
std::invalid_argument Thrown if *this, y and cs are dimension-incompatible or if cs contains a strict inequality.

template<typename T>
void Parma_Polyhedra_Library::BD_Shape< T >::H79_widening_assign ( const BD_Shape< T > &  y,
unsigned *  tp = 0 
) [inline]

Assigns to *this the result of computing the H79-widening between *this and y.

Parameters:
y A BDS that must be contained in *this.
tp An optional pointer to an unsigned variable storing the number of available tokens (to be used when applying the widening with tokens delay technique).
Exceptions:
std::invalid_argument Thrown if *this and y are dimension-incompatible.

template<typename T>
void Parma_Polyhedra_Library::BD_Shape< T >::limited_H79_extrapolation_assign ( const BD_Shape< T > &  y,
const Constraint_System cs,
unsigned *  tp = 0 
) [inline]

Improves the result of the H79-widening computation by also enforcing those constraints in cs that are satisfied by all the points of *this.

Parameters:
y A BDS that must be contained in *this.
cs The system of constraints used to improve the widened BDS.
tp An optional pointer to an unsigned variable storing the number of available tokens (to be used when applying the widening with tokens delay technique).
Exceptions:
std::invalid_argument Thrown if *this, y and cs are dimension-incompatible.

template<typename T>
void Parma_Polyhedra_Library::BD_Shape< T >::add_space_dimensions_and_embed ( dimension_type  m  ) 

Adds m new dimensions and embeds the old BDS into the new space.

Parameters:
m The number of dimensions to add.
The new dimensions will be those having the highest indexes in the new BDS, which is defined by a system of bounded differences in which the variables running through the new dimensions are unconstrained. For instance, when starting from the BDS $\cB \sseq \Rset^2$ and adding a third dimension, the result will be the BDS

\[ \bigl\{\, (x, y, z)^\transpose \in \Rset^3 \bigm| (x, y)^\transpose \in \cB \,\bigr\}. \]

template<typename T>
void Parma_Polyhedra_Library::BD_Shape< T >::add_space_dimensions_and_project ( dimension_type  m  ) 

Adds m new dimensions to the BDS and does not embed it in the new vector space.

Parameters:
m The number of dimensions to add.
The new dimensions will be those having the highest indexes in the new BDS, which is defined by a system of bounded differences in which the variables running through the new dimensions are all constrained to be equal to 0. For instance, when starting from the BDS $\cB \sseq \Rset^2$ and adding a third dimension, the result will be the BDS

\[ \bigl\{\, (x, y, 0)^\transpose \in \Rset^3 \bigm| (x, y)^\transpose \in \cB \,\bigr\}. \]

template<typename T>
void Parma_Polyhedra_Library::BD_Shape< T >::concatenate_assign ( const BD_Shape< T > &  y  ) 

Seeing a BDS as a set of tuples (its points), assigns to *this all the tuples that can be obtained by concatenating, in the order given, a tuple of *this with a tuple of y.

Let $B \sseq \Rset^n$ and $D \sseq \Rset^m$ be the BDSs corresponding, on entry, to *this and y, respectively. Upon successful completion, *this will represent the BDS $R \sseq \Rset^{n+m}$ such that

\[ R \defeq \Bigl\{\, (x_1, \ldots, x_n, y_1, \ldots, y_m)^\transpose \Bigm| (x_1, \ldots, x_n)^\transpose \in B, (y_1, \ldots, y_m)^\transpose \in D \,\Bigl\}. \]

Another way of seeing it is as follows: first increases the space dimension of *this by adding y.space_dimension() new dimensions; then adds to the system of constraints of *this a renamed-apart version of the constraints of y.

template<typename T>
void Parma_Polyhedra_Library::BD_Shape< T >::remove_space_dimensions ( const Variables_Set to_be_removed  ) 

Removes all the specified dimensions.

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

template<typename T>
void Parma_Polyhedra_Library::BD_Shape< T >::remove_higher_space_dimensions ( dimension_type  new_dimension  )  [inline]

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

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

template<typename T>
template<typename PartialFunction>
void Parma_Polyhedra_Library::BD_Shape< T >::map_space_dimensions ( const PartialFunction &  pfunc  ) 

Remaps the dimensions of the vector space according to a partial function.

Parameters:
pfunc The partial function specifying the destiny of each dimension.
The template class PartialFunction must provide the following methods.
      bool has_empty_codomain() const
returns true if and only if the represented partial function has an empty co-domain (i.e., it is always undefined). The has_empty_codomain() method will always be called before the methods below. However, if has_empty_codomain() returns true, none of the functions below will be called.
      dimension_type max_in_codomain() const
returns the maximum value that belongs to the co-domain of the partial function.
      bool maps(dimension_type i, dimension_type& j) const
Let $f$ be the represented function and $k$ be the value of i. If $f$ is defined in $k$, then $f(k)$ is assigned to j and true is returned. If $f$ is undefined in $k$, then false is returned.

The result is undefined if pfunc does not encode a partial function with the properties described in the specification of the mapping operator.


Friends And Related Function Documentation

template<typename T>
std::ostream & operator<< ( std::ostream &  s,
const BD_Shape< T > &  c 
) [friend]

Output operator.

Writes a textual representation of bds on s: false is written if bds is an empty polyhedron; true is written if bds is the universe polyhedron; a system of constraints defining bds is written otherwise, all constraints separated by ", ".

template<typename T>
bool operator== ( const BD_Shape< T > &  x,
const BD_Shape< T > &  y 
) [related]

Returns true if and only if x and y are the same BDS.

Note that x and y may be dimension-incompatible shapes: in this case, the value false is returned.

template<typename T>
bool operator!= ( const BD_Shape< T > &  x,
const BD_Shape< T > &  y 
) [related]

Returns true if and only if x and y aren't the same BDS.

Note that x and y may be dimension-incompatible shapes: in this case, the value true is returned.

template<typename T>
bool rectilinear_distance_assign ( Checked_Number< To, Extended_Number_Policy > &  r,
const BD_Shape< T > &  x,
const BD_Shape< T > &  y,
const Rounding_Dir  dir 
) [related]

Computes the rectilinear (or Manhattan) distance between x and y.

If the rectilinear distance between x and y is defined, stores an approximation of it into r and returns true; returns false otherwise.

The direction of the approximation is specified by dir.

All computations are performed using variables of type Checked_Number<To, Extended_Number_Policy>.

template<typename T>
bool rectilinear_distance_assign ( Checked_Number< To, Extended_Number_Policy > &  r,
const BD_Shape< T > &  x,
const BD_Shape< T > &  y,
const Rounding_Dir  dir,
Temp &  tmp0,
Temp &  tmp1,
Temp &  tmp2 
) [related]

Computes the rectilinear (or Manhattan) distance between x and y.

If the rectilinear distance between x and y is defined, stores an approximation of it into r and returns true; returns false otherwise.

The direction of the approximation is specified by dir.

All computations are performed using the temporary variables tmp0, tmp1 and tmp2.

template<typename T>
bool euclidean_distance_assign ( Checked_Number< To, Extended_Number_Policy > &  r,
const BD_Shape< T > &  x,
const BD_Shape< T > &  y,
const Rounding_Dir  dir 
) [related]

Computes the euclidean distance between x and y.

If the euclidean distance between x and y is defined, stores an approximation of it into r and returns true; returns false otherwise.

The direction of the approximation is specified by dir.

All computations are performed using variables of type Checked_Number<To, Extended_Number_Policy>.

template<typename T>
bool euclidean_distance_assign ( Checked_Number< To, Extended_Number_Policy > &  r,
const BD_Shape< T > &  x,
const BD_Shape< T > &  y,
const Rounding_Dir  dir,
Temp &  tmp0,
Temp &  tmp1,
Temp &  tmp2 
) [related]

Computes the euclidean distance between x and y.

If the euclidean distance between x and y is defined, stores an approximation of it into r and returns true; returns false otherwise.

The direction of the approximation is specified by dir.

All computations are performed using the temporary variables tmp0, tmp1 and tmp2.

template<typename T>
bool l_infinity_distance_assign ( Checked_Number< To, Extended_Number_Policy > &  r,
const BD_Shape< T > &  x,
const BD_Shape< T > &  y,
const Rounding_Dir  dir 
) [related]

Computes the $L_\infty$ distance between x and y.

If the $L_\infty$ distance between x and y is defined, stores an approximation of it into r and returns true; returns false otherwise.

The direction of the approximation is specified by dir.

All computations are performed using variables of type Checked_Number<To, Extended_Number_Policy>.

template<typename T>
bool l_infinity_distance_assign ( Checked_Number< To, Extended_Number_Policy > &  r,
const BD_Shape< T > &  x,
const BD_Shape< T > &  y,
const Rounding_Dir  dir,
Temp &  tmp0,
Temp &  tmp1,
Temp &  tmp2 
) [related]

Computes the $L_\infty$ distance between x and y.

If the $L_\infty$ distance between x and y is defined, stores an approximation of it into r and returns true; returns false otherwise.

The direction of the approximation is specified by dir.

All computations are performed using the temporary variables tmp0, tmp1 and tmp2.


Generated on Sun Mar 12 09:14:32 2006 for PPL by  doxygen 1.4.6-20060227