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

A bounded difference shape. More...

#include <BD_Shape.defs.hh>

Collaboration diagram for Parma_Polyhedra_Library::BD_Shape< T >:

List of all members.

Exception Throwers

void throw_dimension_incompatible (const char *method, const BD_Shape &x) const

void throw_dimension_incompatible (const char *method, dimension_type required_dim) const

void throw_dimension_incompatible (const char *method, const Constraint &c) const

void throw_dimension_incompatible (const char *method, const Generator &g) const

void throw_dimension_incompatible (const char *method, const char *name_row, const Linear_Expression &y) const

static void throw_constraint_incompatible (const char *method)

static void throw_expression_too_complex (const char *method, const Linear_Expression &e)

static void throw_generic (const char *method, const char *reason)

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

void ascii_dump () const

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

void ascii_dump (std::ostream &s) const

Writes to s an ASCII representation of *this.

void print () const

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

bool ascii_load (std::istream &s)

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

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 &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_Shape & operator= (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.

Private Types

typedef Checked_Number< T,
Extended_Number_Policy > N

The (extended) numeric type of the inhomogeneous term of the inequalities defining a BDS.

Private Member Functions

bool marked_empty () const

Returns true if the BDS is known to be empty.

bool marked_shortest_path_closed () const

Returns true if the system of bounded differences is known to be shortest-path closed.

bool marked_shortest_path_reduced () const

Returns true if the system of bounded differences is known to be shortest-path reduced.

void set_empty ()

Turns *this into an empty BDS.

void set_zero_dim_univ ()

Turns *this into an zero-dimensional universe BDS.

void shortest_path_closure_assign () const

Assigns to this->dbm its shortest-path closure.

void shortest_path_reduction_assign () const

Assigns to this->dbm its shortest-path closure and records into this->redundancy_dbm which of the entries in this->dbm are redundant.

bool is_shortest_path_reduced () const

Returns true if and only if this->dbm is shortest-path closed and this->redundancy_dbm correctly flags the redundant entries in this->dbm.

void add_dbm_constraint (dimension_type i, dimension_type j, N k)

Adds the constraint dbm[i][j] <= k.

void add_dbm_constraint (dimension_type i, dimension_type j, Coefficient_traits::const_reference num, Coefficient_traits::const_reference den)

Adds the constraint dbm[i][j] <= num/den.

void forget_all_dbm_constraints (dimension_type v)

Removes all the constraints on row/column v.

void forget_binary_dbm_constraints (dimension_type v)

Removes all binary constraints on row/column v.

void deduce_v_minus_u_bounds (dimension_type v, dimension_type last_v, const Linear_Expression &sc_expr, Coefficient_traits::const_reference sc_den, const N &pos_sum)

An helper function for the computation of affine relations.

void deduce_u_minus_v_bounds (dimension_type v, dimension_type last_v, const Linear_Expression &sc_expr, Coefficient_traits::const_reference sc_den, const N &neg_sum)

An helper function for the computation of affine relations.

void get_limiting_shape (const Constraint_System &cs, BD_Shape &limiting_shape) const

Adds to limiting_shape the bounded differences in cs that are satisfied by *this.

void compute_predecessors (std::vector< dimension_type > &predecessor) const

Compute the (zero-equivalence classes) predecessor relation.

void compute_leaders (std::vector< dimension_type > &leaders) const

Compute the leaders of zero-equivalence classes.

Private Attributes

DB_Matrix< N > dbm

The matrix representing the system of bounded differences.

Status status

The status flags to keep track of the internal state.

std::vector< std::deque< bool > > redundancy_dbm

A matrix of Booleans indicating which constraints are redundant.

Friends

class Parma_Polyhedra_Library::BD_Shape

bool Parma_Polyhedra_Library::operator== (const BD_Shape< T > &x, const BD_Shape< T > &y)

template<typename Temp, typename To, typename U>

bool rectilinear_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const BD_Shape &x, const BD_Shape &y, const Rounding_Dir dir, Temp &tmp0, Temp &tmp1, Temp &tmp2)

template<typename Temp, typename To, typename U>

bool euclidean_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const BD_Shape &x, const BD_Shape &y, const Rounding_Dir dir, Temp &tmp0, Temp &tmp1, Temp &tmp2)

template<typename Temp, typename To, typename U>

bool l_infinity_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const BD_Shape &x, const BD_Shape &y, const Rounding_Dir dir, Temp &tmp0, Temp &tmp1, Temp &tmp2)

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

Output operator.

Related Functions

(Note that these are not member functions.)

template<typename T>

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.

template<typename T>

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.

template<typename To, 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)

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

template<typename Temp, typename To, 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)

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

template<typename To, 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)

Computes the euclidean distance between x and y.

template<typename Temp, typename To, 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)

Computes the euclidean distance between x and y.

template<typename To, 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)

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

template<typename Temp, typename To, 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)

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

template<typename T>

void swap (Parma_Polyhedra_Library::BD_Shape< T > &x, Parma_Polyhedra_Library::BD_Shape< T > &y)

Specializes std::swap.

template<typename T, typename Policy>

void numer_denom (const Checked_Number< T, Policy > &from, Coefficient &num, Coefficient &den)

Extract the numerator and denominator components of from.

template<typename T, typename Policy>

void div_round_up (Checked_Number< T, Policy > &to, Coefficient_traits::const_reference x, Coefficient_traits::const_reference y)

Divides x by y into to, rounding the result towards plus infinity.

template<typename N>

void min_assign (N &x, const N &y)

Assigns to x the minimum between x and y.

template<typename N>

void max_assign (N &x, const N &y)

Assigns to x the maximum between x and y.

bool extract_bounded_difference (const Constraint &c, const dimension_type c_space_dim, dimension_type &c_num_vars, dimension_type &c_first_var, dimension_type &c_second_var, Coefficient &c_coeff)

void compute_leader_indices (const std::vector< dimension_type > &predecessor, std::vector< dimension_type > &indices)

Classes

class Status

A conjunctive assertion about a BD_Shape<T> object. More...

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:

a bounded precision integer type (e.g., int32_t or int64_t);
a bounded precision floating point type (e.g., float or double);
an unbounded integer or rational type, as provided by GMP (i.e., mpz_class or mpq_class).

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:

$x - y \leq 1$ , if T is a (bounded or unbounded) integer type;
$x - y \leq \frac{1}{3}$ , if T is the unbounded rational type mpq_class;
$x - y \leq k$ , where $k > \frac{1}{3}$ , if T is a floating point type (having no exact representation for $\frac{1}{3}$ ).

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);

Definition at line 388 of file BD_Shape.defs.hh.

Member Typedef Documentation

template<typename T>

typedef Checked_Number<T, Extended_Number_Policy> Parma_Polyhedra_Library::BD_Shape< T >::N [private]

The (extended) numeric type of the inhomogeneous term of the inequalities defining a BDS.

Definition at line 394 of file BD_Shape.defs.hh.

template<typename T>

typedef T Parma_Polyhedra_Library::BD_Shape< T >::base_type

The numeric base type upon which bounded differences are built.

Definition at line 398 of file BD_Shape.defs.hh.

template<typename T>

typedef N Parma_Polyhedra_Library::BD_Shape< T >::coefficient_type

The (extended) numeric type of the inhomogeneous term of the inequalities defining a BDS.

Definition at line 404 of file BD_Shape.defs.hh.

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.

Definition at line 144 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::EMPTY, Parma_Polyhedra_Library::BD_Shape< T >::OK(), Parma_Polyhedra_Library::BD_Shape< T >::set_empty(), Parma_Polyhedra_Library::BD_Shape< T >::Status::set_shortest_path_closed(), and Parma_Polyhedra_Library::BD_Shape< T >::status.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape().

00146   : dbm(num_dimensions + 1), status(), redundancy_dbm() {
00147   if (kind == EMPTY)
00148     set_empty();
00149   else {
00150     if (num_dimensions > 0)
00151       // A (non zero-dim) universe BDS is closed.
00152       status.set_shortest_path_closed();
00153   }
00154   assert(OK());
00155 }

template<typename T>

Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape ( const BD_Shape< T > & y ) [inline]

Ordinary copy-constructor.

Definition at line 159 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::marked_shortest_path_reduced(), and Parma_Polyhedra_Library::BD_Shape< T >::redundancy_dbm.

00160   : dbm(y.dbm), status(y.status), redundancy_dbm() {
00161   if (y.marked_shortest_path_reduced())
00162     redundancy_dbm = y.redundancy_dbm;
00163 }

template<typename T>

template<typename U>

Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape ( const BD_Shape & y ) [inline, explicit]

Builds a conservative, upward approximation of y.

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

References Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), Parma_Polyhedra_Library::BD_Shape< T >::set_empty(), Parma_Polyhedra_Library::BD_Shape< T >::set_zero_dim_univ(), Parma_Polyhedra_Library::BD_Shape< T >::status, and Parma_Polyhedra_Library::BD_Shape< T >::Status::test_zero_dim_univ().

00169   : dbm(y.dbm), status(), redundancy_dbm() {
00170   // TODO: handle flags properly, possibly taking special cases into account.
00171   if (y.marked_empty())
00172     set_empty();
00173   else if (y.status.test_zero_dim_univ())
00174     set_zero_dim_univ();
00175 }

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.

Definition at line 204 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::add_constraints(), Parma_Polyhedra_Library::BD_Shape< T >::OK(), Parma_Polyhedra_Library::BD_Shape< T >::Status::set_shortest_path_closed(), Parma_Polyhedra_Library::Constraint_System::space_dimension(), and Parma_Polyhedra_Library::BD_Shape< T >::status.

00205   : dbm(cs.space_dimension() + 1), status(), redundancy_dbm() {
00206   if (cs.space_dimension() > 0)
00207     // A (non zero-dim) universe BDS is shortest-path closed.
00208     status.set_shortest_path_closed();
00209   add_constraints(cs);
00210   assert(OK());
00211 }

template<typename T>

Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape ( const Generator_System & gs ) [inline]

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.

Definition at line 40 of file BD_Shape.templates.hh.

00041   : dbm(gs.space_dimension() + 1), status(), redundancy_dbm() {
00042   using Implementation::BD_Shapes::max_assign;
00043   using Implementation::BD_Shapes::div_round_up;
00044 
00045   const Generator_System::const_iterator gs_begin = gs.begin();
00046   const Generator_System::const_iterator gs_end = gs.end();
00047   if (gs_begin == gs_end) {
00048     // An empty generator system defines the empty polyhedron.
00049     set_empty();
00050     assert(OK());
00051     return;
00052   }
00053 
00054   const dimension_type space_dim = space_dimension();
00055   DB_Row<N>& dbm_0 = dbm[0];
00056   N tmp;
00057 
00058   bool dbm_initialized = false;
00059   bool point_seen = false;
00060   // Going through all the points and closure points.
00061   for (Generator_System::const_iterator i = gs_begin; i != gs_end; ++i) {
00062     const Generator& g = *i;
00063     switch (g.type()) {
00064     case Generator::POINT:
00065       point_seen = true;
00066       // Intentionally fall through.
00067     case Generator::CLOSURE_POINT:
00068       if (!dbm_initialized) {
00069         // When handling the first (closure) point, we initialize the DBM.
00070         dbm_initialized = true;
00071         const Coefficient& d = g.divisor();
00072         for (dimension_type i = space_dim; i > 0; --i) {
00073           const Coefficient& g_i = g.coefficient(Variable(i-1));
00074           DB_Row<N>& dbm_i = dbm[i];
00075           for (dimension_type j = space_dim; j > 0; --j)
00076             if (i != j)
00077               div_round_up(dbm_i[j], g.coefficient(Variable(j-1)) - g_i, d);
00078           div_round_up(dbm_i[0], -g_i, d);
00079         }
00080         for (dimension_type j = space_dim; j > 0; --j)
00081           div_round_up(dbm_0[j], g.coefficient(Variable(j-1)), d);
00082         // Note: no need to initialize the first element of the main diagonal.
00083       }
00084       else {
00085         // This is not the first point: the DBM already contains
00086         // valid values and we must compute maxima.
00087         const Coefficient& d = g.divisor();
00088         for (dimension_type i = space_dim; i > 0; --i) {
00089           const Coefficient& g_i = g.coefficient(Variable(i-1));
00090           DB_Row<N>& dbm_i = dbm[i];
00091           // The loop correctly handles the case when i == j.
00092           for (dimension_type j = space_dim; j > 0; --j) {
00093             div_round_up(tmp, g.coefficient(Variable(j-1)) - g_i, d);
00094             max_assign(dbm_i[j], tmp);
00095           }
00096           div_round_up(tmp, -g_i, d);
00097           max_assign(dbm_i[0], tmp);
00098         }
00099         for (dimension_type j = space_dim; j > 0; --j) {
00100           div_round_up(tmp, g.coefficient(Variable(j-1)), d);
00101           max_assign(dbm_0[j], tmp);
00102         }
00103       }
00104       break;
00105     default:
00106       // Lines and rays temporarily ignored.
00107       break;
00108     }
00109   }
00110 
00111   if (!point_seen)
00112     // The generator system is not empty, but contains no points.
00113     throw std::invalid_argument("PPL::BD_Shape<T>::BD_Shape(gs):\n"
00114                                 "the non-empty generator system gs "
00115                                 "contains no points.");
00116 
00117   // Going through all the lines and rays.
00118   for (Generator_System::const_iterator i = gs_begin; i != gs_end; ++i) {
00119     const Generator& g = *i;
00120     switch (g.type()) {
00121     case Generator::LINE:
00122       for (dimension_type i = space_dim; i > 0; --i) {
00123         const Coefficient& g_i = g.coefficient(Variable(i-1));
00124         DB_Row<N>& dbm_i = dbm[i];
00125         // The loop correctly handles the case when i == j.
00126         for (dimension_type j = space_dim; j > 0; --j)
00127           if (g_i != g.coefficient(Variable(j-1)))
00128             dbm_i[j] = PLUS_INFINITY;
00129         if (g_i != 0)
00130           dbm_i[0] = PLUS_INFINITY;
00131       }
00132       for (dimension_type j = space_dim; j > 0; --j)
00133         if (g.coefficient(Variable(j-1)) != 0)
00134           dbm_0[j] = PLUS_INFINITY;
00135       break;
00136     case Generator::RAY:
00137       for (dimension_type i = space_dim; i > 0; --i) {
00138         const Coefficient& g_i = g.coefficient(Variable(i-1));
00139         DB_Row<N>& dbm_i = dbm[i];
00140         // The loop correctly handles the case when i == j.
00141         for (dimension_type j = space_dim; j > 0; --j)
00142           if (g_i < g.coefficient(Variable(j-1)))
00143             dbm_i[j] = PLUS_INFINITY;
00144         if (g_i < 0)
00145           dbm_i[0] = PLUS_INFINITY;
00146       }
00147       for (dimension_type j = space_dim; j > 0; --j)
00148         if (g.coefficient(Variable(j-1)) > 0)
00149           dbm_0[j] = PLUS_INFINITY;
00150       break;
00151     default:
00152       // Points and closure points already dealt with.
00153       break;
00154     }
00155   }
00156   status.set_shortest_path_closed();
00157   assert(OK());
00158 }

template<typename T>

Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape	(	const Polyhedron &	ph,
		Complexity_Class	complexity = `ANY_COMPLEXITY`
	)			`[inline]`

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.

Definition at line 161 of file BD_Shape.templates.hh.

00162   : dbm(), status(), redundancy_dbm() {
00163   using Implementation::BD_Shapes::div_round_up;
00164   const dimension_type num_dimensions = ph.space_dimension();
00165 
00166   if (ph.marked_empty()) {
00167     *this = BD_Shape(num_dimensions, EMPTY);
00168     return;
00169   }
00170 
00171   if (num_dimensions == 0) {
00172     *this = BD_Shape(num_dimensions, UNIVERSE);
00173     return;
00174   }
00175 
00176   // Build from generators when we do not care about complexity
00177   // or when the process has polynomial complexity.
00178   if (complexity == ANY_COMPLEXITY
00179       || (!ph.has_pending_constraints() && ph.generators_are_up_to_date())) {
00180     *this = BD_Shape(ph.generators());
00181     return;
00182   }
00183 
00184   // We cannot afford exponential complexity, we do not have a complete set
00185   // of generators for the polyhedron, and the polyhedron is not trivially
00186   // empty or zero-dimensional.  Constraints, however, are up to date.
00187   assert(ph.constraints_are_up_to_date());
00188 
00189   if (!ph.has_something_pending() && ph.constraints_are_minimized()) {
00190     // If the constraint system of the polyhedron is minimized,
00191     // the test `is_universe()' has polynomial complexity.
00192     if (ph.is_universe()) {
00193       *this = BD_Shape(num_dimensions, UNIVERSE);
00194       return;
00195     }
00196   }
00197 
00198   // See if there is at least one inconsistent constraint in `ph.con_sys'.
00199   for (Constraint_System::const_iterator i = ph.con_sys.begin(),
00200          cs_end = ph.con_sys.end(); i != cs_end; ++i)
00201     if (i->is_inconsistent()) {
00202       *this = BD_Shape(num_dimensions, EMPTY);
00203       return;
00204     }
00205 
00206   // If `complexity' allows it, use simplex to derive the exact (modulo
00207   // the fact that our BDSs are topologically closed) variable bounds.
00208   if (complexity == SIMPLEX_COMPLEXITY) {
00209     LP_Problem lp;
00210     lp.set_optimization_mode(MAXIMIZATION);
00211 
00212     const Constraint_System& ph_cs = ph.constraints();
00213     if (!ph_cs.has_strict_inequalities())
00214       lp.add_constraints(ph_cs);
00215     else
00216       // Adding to `lp' a topologically closed version of `ph_cs'.
00217       for (Constraint_System::const_iterator i = ph_cs.begin(),
00218              iend = ph_cs.end(); i != iend; ++i) {
00219         const Constraint& c = *i;
00220         lp.add_constraint(c.is_equality()
00221                           ? (Linear_Expression(c) == 0)
00222                           : (Linear_Expression(c) >= 0));
00223       }
00224 
00225     // Check for unsatisfiability.
00226     if (!lp.is_satisfiable()) {
00227       *this = BD_Shape(num_dimensions, EMPTY);
00228       return;
00229     }
00230 
00231     // Get all the upper bounds.
00232     LP_Problem_Status lp_status;
00233     Generator g(point());
00234     TEMP_INTEGER(num);
00235     TEMP_INTEGER(den);
00236     for (dimension_type i = 1; i <= num_dimensions; ++i) {
00237       Variable x(i-1);
00238       // Evaluate optimal upper bound for `x <= ub'.
00239       lp.set_objective_function(x);
00240       lp_status = lp.solve();
00241       if (lp_status == UNBOUNDED_LP_PROBLEM)
00242         dbm[0][i] = PLUS_INFINITY;
00243       else {
00244         assert(lp_status == OPTIMIZED_LP_PROBLEM);
00245         g = lp.optimizing_point();
00246         lp.evaluate_objective_function(g, num, den);
00247         div_round_up(dbm[0][i], num, den);
00248       }
00249       // Evaluate optimal upper bound for `x - y <= ub'.
00250       for (dimension_type j = 1; j <= num_dimensions; ++j) {
00251         if (i == j)
00252           continue;
00253         Variable y(j-1);
00254         lp.set_objective_function(x - y);
00255         lp_status = lp.solve();
00256         if (lp_status == UNBOUNDED_LP_PROBLEM)
00257           dbm[j][i] = PLUS_INFINITY;
00258         else {
00259           assert(lp_status == OPTIMIZED_LP_PROBLEM);
00260           g = lp.optimizing_point();
00261           lp.evaluate_objective_function(g, num, den);
00262           div_round_up(dbm[j][i], num, den);
00263         }
00264       }
00265       // Evaluate optimal upper bound for `-x <= ub'.
00266       lp.set_objective_function(-x);
00267       lp_status = lp.solve();
00268       if (lp_status == UNBOUNDED_LP_PROBLEM)
00269         dbm[i][0] = PLUS_INFINITY;
00270       else {
00271         assert(lp_status == OPTIMIZED_LP_PROBLEM);
00272         g = lp.optimizing_point();
00273         lp.evaluate_objective_function(g, num, den);
00274         div_round_up(dbm[i][0], num, den);
00275       }
00276     }
00277     status.set_shortest_path_closed();
00278     return;
00279   }
00280 
00281   // Extract easy-to-find bounds from constraints.
00282   *this = BD_Shape(ph.con_sys);
00283 }

template<typename T>

Parma_Polyhedra_Library::BD_Shape< T >::~BD_Shape ( ) [inline]

Destructor.

Definition at line 253 of file BD_Shape.inlines.hh.

00253                        {
00254 }

Member Function Documentation

template<typename T>

dimension_type Parma_Polyhedra_Library::BD_Shape< T >::max_space_dimension ( ) [inline, static]

Returns the maximum space dimension that a BDS can handle.

Definition at line 103 of file BD_Shape.inlines.hh.

00103                                  {
00104   // One dimension is reserved to have a value of type dimension_type
00105   // that does not represent a legal dimension.
00106   return std::min(DB_Matrix<N>::max_num_rows() - 1,
00107                   DB_Matrix<N>::max_num_columns() - 1);
00108 }

template<typename T>

BD_Shape< T > & Parma_Polyhedra_Library::BD_Shape< T >::operator= ( const BD_Shape< T > & y ) [inline]

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

Definition at line 243 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::BD_Shape< T >::marked_shortest_path_reduced(), Parma_Polyhedra_Library::BD_Shape< T >::redundancy_dbm, and Parma_Polyhedra_Library::BD_Shape< T >::status.

00243                                         {
00244   dbm = y.dbm;
00245   status = y.status;
00246   if (y.marked_shortest_path_reduced())
00247     redundancy_dbm = y.redundancy_dbm;
00248   return *this;
00249 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::swap ( BD_Shape< T > & y ) [inline]

Swaps *this with y (*this and y can be dimension-incompatible).

Definition at line 258 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::BD_Shape< T >::redundancy_dbm, and Parma_Polyhedra_Library::BD_Shape< T >::status.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::H79_widening_assign(), Parma_Polyhedra_Library::BD_Shape< T >::limited_H79_extrapolation_assign(), Parma_Polyhedra_Library::BD_Shape< T >::swap(), and Parma_Polyhedra_Library::BD_Shape< T >::time_elapse_assign().

00258                              {
00259   std::swap(dbm, y.dbm);
00260   std::swap(status, y.status);
00261   std::swap(redundancy_dbm, y.redundancy_dbm);
00262 }

template<typename T>

dimension_type Parma_Polyhedra_Library::BD_Shape< T >::space_dimension ( ) const [inline]

Returns the dimension of the vector space enclosing *this.

Definition at line 266 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::dbm.

00266                                    {
00267   return dbm.num_rows() - 1;
00268 }

template<typename T>

dimension_type Parma_Polyhedra_Library::BD_Shape< T >::affine_dimension ( ) const [inline]

Returns $0$ , if *this is empty; otherwise, returns the affine dimension of *this.

Definition at line 215 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::compute_predecessors(), Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign(), and Parma_Polyhedra_Library::BD_Shape< T >::space_dimension().

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::BHMZ05_widening_assign().

00215                                     {
00216   const dimension_type space_dim = space_dimension();
00217 
00218   // Shortest-path closure is necessary to detect emptiness
00219   // and all (possibly implicit) equalities.
00220   shortest_path_closure_assign();
00221   if (marked_empty())
00222     return 0;
00223 
00224   // The vector `predecessor' is used to represent equivalence classes:
00225   // `predecessor[i] == i' if and only if `i' is the leader of its
00226   // equivalence class (i.e., the minimum index in the class);
00227   std::vector<dimension_type> predecessor;
00228   compute_predecessors(predecessor);
00229 
00230   // Due to the fictitious variable `0', the affine dimension is one
00231   // less the number of equivalence classes.
00232   dimension_type affine_dim = 0;
00233   // Note: disregard the first equivalence class.
00234   for (dimension_type i = 1; i <= space_dim; ++i)
00235     if (predecessor[i] == i)
00236       ++affine_dim;
00237 
00238   return affine_dim;
00239 }

template<typename T>

Constraint_System Parma_Polyhedra_Library::BD_Shape< T >::constraints ( ) const [inline]

Returns a system of constraints defining *this.

Definition at line 3273 of file BD_Shape.templates.hh.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::bds_difference_assign(), Parma_Polyhedra_Library::BD_Shape< T >::H79_widening_assign(), Parma_Polyhedra_Library::BD_Shape< T >::limited_H79_extrapolation_assign(), and Parma_Polyhedra_Library::BD_Shape< T >::time_elapse_assign().

03273                                {
03274   using Implementation::BD_Shapes::numer_denom;
03275 
03276   Constraint_System cs;
03277   const dimension_type space_dim = space_dimension();
03278   if (space_dim == 0) {
03279     if (marked_empty())
03280       cs = Constraint_System::zero_dim_empty();
03281   }
03282   else if (marked_empty())
03283     cs.insert(0*Variable(space_dim-1) <= -1);
03284   else if (marked_shortest_path_reduced())
03285     // Disregard redundant constraints.
03286     cs = minimized_constraints();
03287   else {
03288     // KLUDGE: in the future `cs' will be constructed of the right dimension.
03289     // For the time being, we force the dimension with the following line.
03290     cs.insert(0*Variable(space_dim-1) <= 0);
03291 
03292     TEMP_INTEGER(a);
03293     TEMP_INTEGER(b);
03294     // Go through all the unary constraints in `dbm'.
03295     const DB_Row<N>& dbm_0 = dbm[0];
03296     for (dimension_type j = 1; j <= space_dim; ++j) {
03297       const Variable x(j-1);
03298       const N& dbm_0j = dbm_0[j];
03299       const N& dbm_j0 = dbm[j][0];
03300       N negated_dbm_j0;
03301       if (neg_assign_r(negated_dbm_j0, dbm_j0, ROUND_NOT_NEEDED) == V_EQ
03302           && negated_dbm_j0 == dbm_0j) {
03303         // We have a unary equality constraint.
03304         numer_denom(dbm_0j, b, a);
03305         cs.insert(a*x == b);
03306       }
03307       else {
03308         // We have 0, 1 or 2 unary inequality constraints.
03309         if (!is_plus_infinity(dbm_0j)) {
03310           numer_denom(dbm_0j, b, a);
03311           cs.insert(a*x <= b);
03312         }
03313         if (!is_plus_infinity(dbm_j0)) {
03314           numer_denom(dbm_j0, b, a);
03315           cs.insert(-a*x <= b);
03316         }
03317       }
03318     }
03319 
03320     // Go through all the binary constraints in `dbm'.
03321     for (dimension_type i = 1; i <= space_dim; ++i) {
03322       const Variable y(i-1);
03323       const DB_Row<N>& dbm_i = dbm[i];
03324       for (dimension_type j = i + 1; j <= space_dim; ++j) {
03325         const Variable x(j-1);
03326         const N& dbm_ij = dbm_i[j];
03327         const N& dbm_ji = dbm[j][i];
03328         N negated_dbm_ji;
03329         if (neg_assign_r(negated_dbm_ji, dbm_ji, ROUND_NOT_NEEDED) == V_EQ
03330             && negated_dbm_ji == dbm_ij) {
03331           // We have a binary equality constraint.
03332           numer_denom(dbm_ij, b, a);
03333           cs.insert(a*x - a*y == b);
03334         }
03335         else {
03336           // We have 0, 1 or 2 binary inequality constraints.
03337           if (!is_plus_infinity(dbm_ij)) {
03338             numer_denom(dbm_ij, b, a);
03339             cs.insert(a*x - a*y <= b);
03340           }
03341           if (!is_plus_infinity(dbm_ji)) {
03342             numer_denom(dbm_ji, b, a);
03343             cs.insert(a*y - a*x <= b);
03344           }
03345         }
03346       }
03347     }
03348   }
03349   return cs;
03350 }

template<typename T>

Constraint_System Parma_Polyhedra_Library::BD_Shape< T >::minimized_constraints ( ) const [inline]

Returns a minimized system of constraints defining *this.

Definition at line 3354 of file BD_Shape.templates.hh.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::constraints().

03354                                          {
03355   using Implementation::BD_Shapes::numer_denom;
03356 
03357   shortest_path_reduction_assign();
03358   Constraint_System cs;
03359   const dimension_type space_dim = space_dimension();
03360   if (space_dim == 0) {
03361     if (marked_empty())
03362       cs = Constraint_System::zero_dim_empty();
03363   }
03364   else if (marked_empty())
03365     cs.insert(0*Variable(space_dim-1) <= -1);
03366   else {
03367     // KLUDGE: in the future `cs' will be constructed of the right dimension.
03368     // For the time being, we force the dimension with the following line.
03369     cs.insert(0*Variable(space_dim-1) <= 0);
03370 
03371     TEMP_INTEGER(num);
03372     TEMP_INTEGER(den);
03373 
03374     // Compute leader information.
03375     std::vector<dimension_type> leaders;
03376     compute_leaders(leaders);
03377     std::vector<dimension_type> leader_indices;
03378     compute_leader_indices(leaders, leader_indices);
03379     const dimension_type num_leaders = leader_indices.size();
03380 
03381     // Go through the non-leaders to generate equality constraints.
03382     const DB_Row<N>& dbm_0 = dbm[0];
03383     for (dimension_type i = 1; i <= space_dim; ++i) {
03384       const dimension_type leader = leaders[i];
03385       if (i != leader)
03386         // Generate the constraint relating `i' and its leader.
03387         if (leader == 0) {
03388           // A unary equality has to be generated.
03389           assert(!is_plus_infinity(dbm_0[i]));
03390           numer_denom(dbm_0[i], num, den);
03391           cs.insert(den*Variable(i-1) == num);
03392         }
03393         else {
03394           // A binary equality has to be generated.
03395           assert(!is_plus_infinity(dbm[i][leader]));
03396           numer_denom(dbm[i][leader], num, den);
03397           cs.insert(den*Variable(leader-1) - den*Variable(i-1) == num);
03398         }
03399     }
03400 
03401     // Go through the leaders to generate inequality constraints.
03402     // First generate all the unary inequalities.
03403     const std::deque<bool>& red_0 = redundancy_dbm[0];
03404     for (dimension_type l_i = 1; l_i < num_leaders; ++l_i) {
03405       const dimension_type i = leader_indices[l_i];
03406       if (!red_0[i]) {
03407         numer_denom(dbm_0[i], num, den);
03408         cs.insert(den*Variable(i-1) <= num);
03409       }
03410       if (!redundancy_dbm[i][0]) {
03411         numer_denom(dbm[i][0], num, den);
03412         cs.insert(-den*Variable(i-1) <= num);
03413       }
03414     }
03415     // Then generate all the binary inequalities.
03416     for (dimension_type l_i = 1; l_i < num_leaders; ++l_i) {
03417       const dimension_type i = leader_indices[l_i];
03418       const DB_Row<N>& dbm_i = dbm[i];
03419       const std::deque<bool>& red_i = redundancy_dbm[i];
03420       for (dimension_type l_j = l_i + 1; l_j < num_leaders; ++l_j) {
03421         const dimension_type j = leader_indices[l_j];
03422         if (!red_i[j]) {
03423           numer_denom(dbm_i[j], num, den);
03424           cs.insert(den*Variable(j-1) - den*Variable(i-1) <= num);
03425         }
03426         if (!redundancy_dbm[j][i]) {
03427           numer_denom(dbm[j][i], num, den);
03428           cs.insert(den*Variable(i-1) - den*Variable(j-1) <= num);
03429         }
03430       }
03431     }
03432   }
03433   return cs;
03434 }

template<typename T>

bool Parma_Polyhedra_Library::BD_Shape< T >::contains ( const BD_Shape< T > & y ) const [inline]

Returns true if and only if *this contains y.

Exceptions:

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

Definition at line 392 of file BD_Shape.templates.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), and Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible().

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::bds_difference_assign(), Parma_Polyhedra_Library::BD_Shape< T >::BHMZ05_widening_assign(), Parma_Polyhedra_Library::BD_Shape< T >::CC76_extrapolation_assign(), Parma_Polyhedra_Library::BD_Shape< T >::CC76_narrowing_assign(), Parma_Polyhedra_Library::BD_Shape< T >::limited_BHMZ05_extrapolation_assign(), Parma_Polyhedra_Library::BD_Shape< T >::limited_CC76_extrapolation_assign(), and Parma_Polyhedra_Library::BD_Shape< T >::strictly_contains().

00392                                              {
00393   const BD_Shape<T>& x = *this;
00394   const dimension_type x_space_dim = x.space_dimension();
00395 
00396   // Dimension-compatibility check.
00397   if (x_space_dim != y.space_dimension())
00398     throw_dimension_incompatible("contains(y)", y);
00399 
00400   // The zero-dimensional universe shape contains any other
00401   // dimension-compatible shape.
00402   // The zero-dimensional empty shape only contains another
00403   // zero-dimensional empty shape.
00404   if (x_space_dim == 0) {
00405     if (!marked_empty())
00406       return true;
00407     else
00408       return y.marked_empty();
00409   }
00410 
00411   /*
00412     The `y' system of bounded differences need be closed.
00413     In fact if, for example, in `*this' we have the constraints:
00414 
00415     x1 - x2 <= 1;
00416     x1      <= 3;
00417     x2      <= 2;
00418 
00419     in `y' the constraints are:
00420 
00421     x1 - x2 <= 0;
00422     x2      <= 1;
00423 
00424     without closure it returns "false", instead if we close `y' we have
00425     the implicit constraint
00426 
00427     x1      <= 1;
00428 
00429     and so we obtain the right result "true".
00430   */
00431   y.shortest_path_closure_assign();
00432 
00433   // An empty shape is contained in any other dimension-compatible shapes.
00434   if (y.marked_empty())
00435     return true;
00436 
00437   // `*this' contains `y' if and only if every cell of `dbm'
00438   // is greater than or equal to the correspondent one of `y.dbm'.
00439   for (dimension_type i = x_space_dim + 1; i-- > 0; ) {
00440     const DB_Row<N>& x_dbm_i = x.dbm[i];
00441     const DB_Row<N>& y_dbm_i = y.dbm[i];
00442     for (dimension_type j = x_space_dim + 1; j-- > 0; )
00443       if (x_dbm_i[j] < y_dbm_i[j])
00444         return false;
00445   }
00446   return true;
00447 }

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.

Definition at line 537 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::contains().

00537                                                       {
00538   const BD_Shape<T>& x = *this;
00539   return x.contains(y) && !y.contains(x);
00540 }

template<typename T>

Poly_Con_Relation Parma_Polyhedra_Library::BD_Shape< T >::relation_with ( const Constraint & c ) const [inline]

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.

Definition at line 698 of file BD_Shape.templates.hh.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::bds_difference_assign().

00698                                                     {
00699   using Implementation::BD_Shapes::div_round_up;
00700 
00701   const dimension_type c_space_dim = c.space_dimension();
00702   const dimension_type space_dim = space_dimension();
00703 
00704   // Dimension-compatibility check.
00705   if (c_space_dim > space_dim)
00706     throw_dimension_incompatible("relation_with(c)", c);
00707 
00708   shortest_path_closure_assign();
00709 
00710   if (marked_empty())
00711     return Poly_Con_Relation::saturates()
00712       && Poly_Con_Relation::is_included()
00713       && Poly_Con_Relation::is_disjoint();
00714 
00715   if (space_dim == 0) {
00716     if ((c.is_equality() && c.inhomogeneous_term() != 0)
00717         || (c.is_inequality() && c.inhomogeneous_term() < 0))
00718       return Poly_Con_Relation::is_disjoint();
00719     else if (c.is_strict_inequality() && c.inhomogeneous_term() == 0)
00720       // The constraint 0 > 0 implicitly defines the hyperplane 0 = 0;
00721       // thus, the zero-dimensional point also saturates it.
00722       return Poly_Con_Relation::saturates()
00723         && Poly_Con_Relation::is_disjoint();
00724     else if (c.is_equality() || c.inhomogeneous_term() == 0)
00725       return Poly_Con_Relation::saturates()
00726         && Poly_Con_Relation::is_included();
00727     else
00728       // The zero-dimensional point saturates
00729       // neither the positivity constraint 1 >= 0,
00730       // nor the strict positivity constraint 1 > 0.
00731       return Poly_Con_Relation::is_included();
00732   }
00733 
00734   dimension_type num_vars = 0;
00735   dimension_type i = 0;
00736   dimension_type j = 0;
00737   TEMP_INTEGER(coeff);
00738   // Constraints that are not bounded differences are not compatible.
00739   if (!extract_bounded_difference(c, c_space_dim, num_vars, i, j, coeff))
00740     throw_constraint_incompatible("relation_with(c)");
00741 
00742   if (num_vars == 0) {
00743     // Dealing with a trivial constraint.
00744     switch (sgn(c.inhomogeneous_term())) {
00745     case -1:
00746       return Poly_Con_Relation::is_disjoint();
00747     case 0:
00748       if (c.is_strict_inequality())
00749         return Poly_Con_Relation::saturates()
00750           && Poly_Con_Relation::is_disjoint();
00751       else
00752         return Poly_Con_Relation::saturates()
00753           && Poly_Con_Relation::is_included();
00754     case 1:
00755       return Poly_Con_Relation::is_included();
00756     }
00757   }
00758 
00759   // Select the cell to be checked for the "<=" part of the constraint,
00760   // and set `coeff' to the absolute value of itself.
00761   const N& x = (coeff < 0) ? dbm[i][j] : dbm[j][i];
00762   const N& y = (coeff < 0) ? dbm[j][i] : dbm[i][j];
00763   if (coeff < 0)
00764     coeff = -coeff;
00765   N d;
00766   div_round_up(d, c.inhomogeneous_term(), coeff);
00767   N d1;
00768   div_round_up(d1, -c.inhomogeneous_term(), coeff);
00769 
00770   switch (c.type()) {
00771   case Constraint::EQUALITY:
00772     if (d == x && d1 == y)
00773       return Poly_Con_Relation::saturates()
00774         && Poly_Con_Relation::is_included();
00775     else if (d < y && d1 > x)
00776       return Poly_Con_Relation::is_disjoint();
00777     else
00778       return Poly_Con_Relation::strictly_intersects();
00779   case Constraint::NONSTRICT_INEQUALITY:
00780     if (d >= x && d1 >= y)
00781       return Poly_Con_Relation::saturates()
00782         && Poly_Con_Relation::is_included();
00783     else if (d >= x)
00784       return Poly_Con_Relation::is_included();
00785     else if (d < x && d1 > y)
00786       return Poly_Con_Relation::is_disjoint();
00787     else
00788       return Poly_Con_Relation::strictly_intersects();
00789   case Constraint::STRICT_INEQUALITY:
00790     if (d >= x && d1 >= y)
00791       return Poly_Con_Relation::saturates()
00792         && Poly_Con_Relation::is_disjoint();
00793     else if (d > x)
00794       return Poly_Con_Relation::is_included();
00795     else if (d <= x && d1 >= y)
00796       return Poly_Con_Relation::is_disjoint();
00797     else
00798       return Poly_Con_Relation::strictly_intersects();
00799   }
00800   // Quiet a compiler warning: this program point is unreachable.
00801   throw std::runtime_error("PPL internal error");
00802 }

template<typename T>

Poly_Gen_Relation Parma_Polyhedra_Library::BD_Shape< T >::relation_with ( const Generator & g ) const [inline]

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

Exceptions:

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

Definition at line 806 of file BD_Shape.templates.hh.

00806                                                    {
00807   const dimension_type space_dim = space_dimension();
00808   const dimension_type g_space_dim = g.space_dimension();
00809 
00810   // Dimension-compatibility check.
00811   if (space_dim < g_space_dim)
00812     throw_dimension_incompatible("relation_with(g)", g);
00813 
00814   // The empty bdiff cannot subsume a generator.
00815   if (marked_empty())
00816     return Poly_Gen_Relation::nothing();
00817 
00818   // A universe BD shape in a zero-dimensional space subsumes
00819   // all the generators of a zero-dimensional space.
00820   if (space_dim == 0)
00821     return Poly_Gen_Relation::subsumes();
00822 
00823   const bool is_line = g.is_line();
00824 
00825   // The relation between the bdiff and the given generator is obtained
00826   // checking if the generator satisfies all the constraints in the bdiff.
00827   // To check if the generator satisfies all the constraints it's enough
00828   // studying the sign of the scalar product between the generator and
00829   // all the constraints in the bdiff.
00830 
00831   // We find in `*this' all the constraints.
00832   for (dimension_type i = 0; i <= space_dim; ++i) {
00833     for (dimension_type j = i + 1; j <= space_dim; ++j) {
00834       const Variable x(j - 1);
00835       const bool x_dimension_incompatible = x.space_dimension() > g_space_dim;
00836       const N& dbm_ij = dbm[i][j];
00837       const N& dbm_ji = dbm[j][i];
00838       N negated_dbm_ji;
00839       const bool is_equality
00840         = neg_assign_r(negated_dbm_ji, dbm_ji, ROUND_NOT_NEEDED) == V_EQ
00841         && negated_dbm_ji == dbm_ij;
00842       const bool dbm_ij_is_infinity = is_plus_infinity(dbm_ij);
00843       const bool dbm_ji_is_infinity = is_plus_infinity(dbm_ji);
00844       if (i != 0) {
00845         const Variable y(i - 1);
00846         const bool y_dimension_incompatible
00847           = y.space_dimension() > g_space_dim;
00848         const bool is_trivial_zero
00849           = (x_dimension_incompatible && g.coefficient(y) == 0)
00850           || (y_dimension_incompatible && g.coefficient(x) == 0)
00851           || (x_dimension_incompatible && y_dimension_incompatible);
00852         if (is_equality) {
00853           // We have one equality constraint.
00854           // The constraint has form ax - ay = b.
00855           // The scalar product has the form
00856           // 'a * y_i - a * x_j'
00857           // where y_i = g.coefficient(y) and x_j = g.coefficient(x).
00858           // It is not zero when both the coefficients of the
00859           // variables x and y are not zero or when these coefficients
00860           if (!is_trivial_zero && g.coefficient(x) != g.coefficient(y))
00861             return Poly_Gen_Relation::nothing();
00862         }
00863         else
00864           // We have the binary inequality constraints.
00865           if (!dbm_ij_is_infinity) {
00866           // The constraint has form ax - ay <= b.
00867           // The scalar product has the form
00868           // 'a * y_i - a * x_j'
00869             if (is_line
00870                 && !is_trivial_zero
00871                 && g.coefficient(x) != g.coefficient(y))
00872               return Poly_Gen_Relation::nothing();
00873             else
00874               if (g.coefficient(y) < g.coefficient(x))
00875                 return Poly_Gen_Relation::nothing();
00876           }
00877           else if (!dbm_ji_is_infinity) {
00878             // The constraint has form ay - ax <= b.
00879             // The scalar product has the form
00880             // 'a * x_j - a* y_i'.
00881             if (is_line
00882                 && !is_trivial_zero
00883                 && g.coefficient(x) != g.coefficient(y))
00884               return Poly_Gen_Relation::nothing();
00885             else if (g.coefficient(x) < g.coefficient(y))
00886               return Poly_Gen_Relation::nothing();
00887           }
00888       }
00889       else {
00890         // Here i == 0.
00891         if (is_equality) {
00892           // The constraint has form ax = b.
00893           // To satisfy the constraint it's necessary that the scalar product
00894           // is not zero.It happens when the coefficient of the variable 'x'
00895           // in the generator is not zero, because the scalar
00896           // product has the form:
00897           // 'a * x_i' where x_i = g.coefficient(x)..
00898           if (!x_dimension_incompatible && g.coefficient(x) != 0)
00899             return Poly_Gen_Relation::nothing();
00900         }
00901         else
00902           // We have the unary inequality constraints.
00903           if (!dbm_ij_is_infinity) {
00904             // The constraint has form ax <= b.
00905             // The scalar product has the form:
00906             // '-a * x_i' where x_i = g.coefficient(x).
00907             if (is_line
00908                 && !x_dimension_incompatible
00909                 && g.coefficient(x) != 0)
00910               return Poly_Gen_Relation::nothing();
00911             else if (g.coefficient(x) > 0)
00912               return Poly_Gen_Relation::nothing();
00913           }
00914           else if (!dbm_ji_is_infinity) {
00915             // The constraint has form -ax <= b.
00916             // The scalar product has the form:
00917             // 'a * x_i' where x_i = g.coefficient(x).
00918             if (is_line
00919                 && !x_dimension_incompatible
00920                 && g.coefficient(x) != 0)
00921               return Poly_Gen_Relation::nothing();
00922             else if (g.coefficient(x) < 0)
00923               return Poly_Gen_Relation::nothing();
00924           }
00925       }
00926     }
00927   }
00928   return Poly_Gen_Relation::subsumes();
00929 }

template<typename T>

bool Parma_Polyhedra_Library::BD_Shape< T >::is_empty ( ) const [inline]

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

Definition at line 272 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), and Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign().

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_preimage().

00272                             {
00273   shortest_path_closure_assign();
00274   return marked_empty();
00275 }

template<typename T>

bool Parma_Polyhedra_Library::BD_Shape< T >::is_universe ( ) const [inline]

Returns true if and only if *this is a universe BDS.

Definition at line 451 of file BD_Shape.templates.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::is_plus_infinity(), Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), and Parma_Polyhedra_Library::BD_Shape< T >::space_dimension().

00451                                {
00452   if (marked_empty())
00453     return false;
00454 
00455   const dimension_type space_dim = space_dimension();
00456   // If the BDS is non-empty and zero-dimensional,
00457   // then it is necessarily the universe BDS.
00458   if (space_dim == 0)
00459     return true;
00460 
00461   // A system of bounded differences defining the universe BDS can only
00462   // contain trivial constraints.
00463   for (dimension_type i = space_dim + 1; i-- > 0; ) {
00464     const DB_Row<N>& dbm_i = dbm[i];
00465     for (dimension_type j = space_dim + 1; j-- > 0; )
00466       if (!is_plus_infinity(dbm_i[j]))
00467         return false;
00468   }
00469   return true;
00470 }

template<typename T>

bool Parma_Polyhedra_Library::BD_Shape< T >::OK ( ) const [inline]

Returns true if and only if *this satisfies all its invariants.

Definition at line 3595 of file BD_Shape.templates.hh.

03595                       {
03596   // Check whether the difference-bound matrix is well-formed.
03597   if (!dbm.OK())
03598     return false;
03599 
03600   // Check whether the status information is legal.
03601   if (!status.OK())
03602     return false;
03603 
03604   // An empty BDS is OK.
03605   if (marked_empty())
03606     return true;
03607 
03608   // MINUS_INFINITY cannot occur at all.
03609   for (dimension_type i = dbm.num_rows(); i-- > 0; )
03610     for (dimension_type j = dbm.num_rows(); j-- > 0; )
03611     if (is_minus_infinity(dbm[i][j])) {
03612 #ifndef NDEBUG
03613       using namespace Parma_Polyhedra_Library::IO_Operators;
03614       std::cerr << "BD_Shape::dbm[" << i << "][" << i << "] = "
03615                 << dbm[i][i] << "!"
03616                 << std::endl;
03617 #endif
03618       return false;
03619     }
03620 
03621   // On the main diagonal only PLUS_INFINITY can occur.
03622   for (dimension_type i = dbm.num_rows(); i-- > 0; )
03623     if (!is_plus_infinity(dbm[i][i])) {
03624 #ifndef NDEBUG
03625       using namespace Parma_Polyhedra_Library::IO_Operators;
03626       std::cerr << "BD_Shape::dbm[" << i << "][" << i << "] = "
03627                 << dbm[i][i] << "!  (+inf was expected.)"
03628                 << std::endl;
03629 #endif
03630       return false;
03631     }
03632 
03633   // Check whether the shortest-path closure information is legal.
03634   if (marked_shortest_path_closed()) {
03635     BD_Shape x = *this;
03636     x.status.reset_shortest_path_closed();
03637     x.shortest_path_closure_assign();
03638     if (x.dbm != dbm) {
03639 #ifndef NDEBUG
03640       std::cerr << "BD_Shape is marked as closed but it is not!"
03641                 << std::endl;
03642 #endif
03643       return false;
03644     }
03645   }
03646 
03647   // Check whether the shortest-path reduction information is legal.
03648   if (marked_shortest_path_reduced()) {
03649     // A non-redundant constraint cannot be equal to PLUS_INFINITY.
03650     for (dimension_type i = dbm.num_rows(); i-- > 0; )
03651       for (dimension_type j = dbm.num_rows(); j-- > 0; )
03652         if (!redundancy_dbm[i][j] && is_plus_infinity(dbm[i][j])) {
03653 #ifndef NDEBUG
03654           using namespace Parma_Polyhedra_Library::IO_Operators;
03655           std::cerr << "BD_Shape::dbm[" << i << "][" << i << "] = "
03656                     << dbm[i][i] << " is marked as non-redundant!"
03657                     << std::endl;
03658 #endif
03659           return false;
03660         }
03661 
03662     BD_Shape x = *this;
03663     x.status.reset_shortest_path_reduced();
03664     x.shortest_path_reduction_assign();
03665     if (x.redundancy_dbm != redundancy_dbm) {
03666 #ifndef NDEBUG
03667       std::cerr << "BD_Shape is marked as reduced but it is not!"
03668                 << std::endl;
03669 #endif
03670       return false;
03671     }
03672   }
03673 
03674   // All checks passed.
03675   return true;
03676 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::add_constraint ( const Constraint & c ) [inline]

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.

Definition at line 287 of file BD_Shape.templates.hh.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::add_constraint_and_minimize(), Parma_Polyhedra_Library::BD_Shape< T >::add_constraints(), and Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_image().

00287                                                {
00288   using Implementation::BD_Shapes::div_round_up;
00289 
00290   const dimension_type c_space_dim = c.space_dimension();
00291   // Dimension-compatibility check.
00292   if (c_space_dim > space_dimension())
00293     throw_dimension_incompatible("add_constraint(c)", c);
00294   // Strict inequalities are not allowed.
00295   if (c.is_strict_inequality())
00296     throw_constraint_incompatible("add_constraint(c)");
00297 
00298   dimension_type num_vars = 0;
00299   dimension_type i = 0;
00300   dimension_type j = 0;
00301   TEMP_INTEGER(coeff);
00302   // Constraints that are not bounded differences are ignored.
00303   if (!extract_bounded_difference(c, c_space_dim, num_vars, i, j, coeff))
00304     return;
00305 
00306   if (num_vars == 0) {
00307     // Dealing with a trivial constraint.
00308     if (c.inhomogeneous_term() < 0)
00309       set_empty();
00310     return;
00311   }
00312 
00313   // Select the cell to be modified for the "<=" part of the constraint,
00314   // and set `coeff' to the absolute value of itself.
00315   N& x = (coeff < 0) ? dbm[i][j] : dbm[j][i];
00316   N& y = (coeff < 0) ? dbm[j][i] : dbm[i][j];
00317   if (coeff < 0)
00318     coeff = -coeff;
00319 
00320   bool changed = false;
00321   // Compute the bound for `x', rounding towards plus infinity.
00322   N d;
00323   div_round_up(d, c.inhomogeneous_term(), coeff);
00324   if (x > d) {
00325     x = d;
00326     changed = true;
00327   }
00328 
00329   if (c.is_equality()) {
00330     // Also compute the bound for `y', rounding towards plus infinity.
00331     div_round_up(d, -c.inhomogeneous_term(), coeff);
00332     if (y > d) {
00333       y = d;
00334       changed = true;
00335     }
00336   }
00337 
00338   // In general, adding a constraint does not preserve the shortest-path
00339   // closure or reduction of the system of bounded differences.
00340   if (changed && marked_shortest_path_closed())
00341     status.reset_shortest_path_closed();
00342   assert(OK());
00343 }

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.

Definition at line 179 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::add_constraint(), Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), and Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign().

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::bds_difference_assign().

00179                                                             {
00180   add_constraint(c);
00181   shortest_path_closure_assign();
00182   return !marked_empty();
00183 }

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.

Definition at line 187 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::add_constraint(), Parma_Polyhedra_Library::Constraint_System::begin(), Parma_Polyhedra_Library::Constraint_System::end(), and Parma_Polyhedra_Library::BD_Shape< T >::OK().

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::add_constraints_and_minimize(), and Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape().

00187                                                         {
00188   for (Constraint_System::const_iterator i = cs.begin(),
00189          iend = cs.end(); i != iend; ++i)
00190     add_constraint(*i);
00191   assert(OK());
00192 }

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.

Definition at line 196 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::add_constraints(), Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), and Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign().

00196                                                                      {
00197   add_constraints(cs);
00198   shortest_path_closure_assign();
00199   return !marked_empty();
00200 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::intersection_assign ( const BD_Shape< T > & y ) [inline]

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

Exceptions:

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

Definition at line 1415 of file BD_Shape.templates.hh.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::intersection_assign_and_minimize(), Parma_Polyhedra_Library::BD_Shape< T >::limited_BHMZ05_extrapolation_assign(), and Parma_Polyhedra_Library::BD_Shape< T >::limited_CC76_extrapolation_assign().

01415                                                   {
01416   const dimension_type space_dim = space_dimension();
01417 
01418   // Dimension-compatibility check.
01419   if (space_dim != y.space_dimension())
01420     throw_dimension_incompatible("intersection_assign(y)", y);
01421 
01422   // If one of the two systems of bounded differences is empty,
01423   // the intersection is empty.
01424   if (marked_empty())
01425     return;
01426   if (y.marked_empty()) {
01427     set_empty();
01428     return;
01429   }
01430 
01431   // If both systems of bounded differences are zero-dimensional,
01432   // then at this point they are necessarily non-empty,
01433   // so that their intersection is non-empty too.
01434   if (space_dim == 0)
01435     return;
01436 
01437   // To intersect two systems of bounded differences we compare
01438   // the constraints and we choose the less values.
01439   bool changed = false;
01440   for (dimension_type i = space_dim + 1; i-- > 0; ) {
01441     DB_Row<N>& dbm_i = dbm[i];
01442     const DB_Row<N>& y_dbm_i = y.dbm[i];
01443     for (dimension_type j = space_dim + 1; j-- > 0; ) {
01444       N& dbm_ij = dbm_i[j];
01445       const N& y_dbm_ij = y_dbm_i[j];
01446       if (dbm_ij > y_dbm_ij) {
01447         dbm_ij = y_dbm_ij;
01448         changed = true;
01449       }
01450     }
01451   }
01452 
01453   if (changed && marked_shortest_path_closed())
01454     status.reset_shortest_path_closed();
01455   assert(OK());
01456 }

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.

Definition at line 611 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::intersection_assign(), Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), and Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign().

00611                                                                {
00612   intersection_assign(y);
00613   shortest_path_closure_assign();
00614   return !marked_empty();
00615 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::bds_hull_assign ( const BD_Shape< T > & y ) [inline]

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.

Definition at line 1082 of file BD_Shape.templates.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), Parma_Polyhedra_Library::BD_Shape< T >::marked_shortest_path_closed(), Parma_Polyhedra_Library::BD_Shape< T >::OK(), Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), and Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible().

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::bds_difference_assign(), Parma_Polyhedra_Library::BD_Shape< T >::bds_hull_assign_and_minimize(), and Parma_Polyhedra_Library::BD_Shape< T >::upper_bound_assign().

01082                                               {
01083   const dimension_type space_dim = space_dimension();
01084 
01085   // Dimension-compatibility check.
01086   if (space_dim != y.space_dimension())
01087     throw_dimension_incompatible("bds_hull_assign(y)", y);
01088 
01089   // The poly-hull of a polyhedron `bd' with an empty polyhedron is `bd'.
01090   y.shortest_path_closure_assign();
01091   if (y.marked_empty())
01092     return;
01093   shortest_path_closure_assign();
01094   if (marked_empty()) {
01095     *this = y;
01096     return;
01097   }
01098 
01099   // The bds-hull consists in constructing `*this' with the maximum
01100   // elements selected from `*this' and `y'.
01101   assert(space_dim == 0 || marked_shortest_path_closed());
01102   for (dimension_type i = space_dim + 1; i-- > 0; ) {
01103     DB_Row<N>& dbm_i = dbm[i];
01104     const DB_Row<N>& y_dbm_i = y.dbm[i];
01105     for (dimension_type j = space_dim + 1; j-- > 0; ) {
01106       N& dbm_ij = dbm_i[j];
01107       const N& y_dbm_ij = y_dbm_i[j];
01108       if (dbm_ij < y_dbm_ij)
01109         dbm_ij = y_dbm_ij;
01110     }
01111   }
01112   // The result is still closed.
01113   assert(OK());
01114 }

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.

Definition at line 544 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::bds_hull_assign(), Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), Parma_Polyhedra_Library::BD_Shape< T >::marked_shortest_path_closed(), and Parma_Polyhedra_Library::BD_Shape< T >::space_dimension().

00544                                                            {
00545   bds_hull_assign(y);
00546   assert(marked_empty()
00547          || space_dimension() == 0 || marked_shortest_path_closed());
00548   return !marked_empty();
00549 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::upper_bound_assign ( const BD_Shape< T > & y ) [inline]

Same as bds_hull_assign.

Definition at line 553 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::bds_hull_assign().

00553                                                  {
00554   bds_hull_assign(y);
00555 }

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.

Definition at line 559 of file BD_Shape.inlines.hh.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::upper_bound_assign_if_exact().

00559                                                      {
00560   // TODO: this must be properly implemented.
00561   return false;
00562 }

template<typename T>

bool Parma_Polyhedra_Library::BD_Shape< T >::upper_bound_assign_if_exact ( const BD_Shape< T > & y ) [inline]

Same as bds_hull_assign_if_exact.

Definition at line 566 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::bds_hull_assign_if_exact().

00566                                                           {
00567   return bds_hull_assign_if_exact(y);
00568 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::bds_difference_assign ( const BD_Shape< T > & y ) [inline]

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

Exceptions:

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

Definition at line 1118 of file BD_Shape.templates.hh.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::difference_assign().

01118                                                     {
01119   const dimension_type space_dim = space_dimension();
01120 
01121   // Dimension-compatibility check.
01122   if (space_dim != y.space_dimension())
01123     throw_dimension_incompatible("bds_difference_assign(y)", y);
01124 
01125   BD_Shape new_bdiffs(space_dim, EMPTY);
01126 
01127   BD_Shape& x = *this;
01128 
01129   x.shortest_path_closure_assign();
01130   // The difference of an empty system of bounded differences
01131   // and of a system of bounded differences `p' is empty.
01132   if (x.marked_empty())
01133     return;
01134   y.shortest_path_closure_assign();
01135   // The difference of a system of bounded differences `p'
01136   // and an empty system of bounded differences is `p'.
01137   if (y.marked_empty())
01138     return;
01139 
01140   // If both systems of bounded differences are zero-dimensional,
01141   // then at this point they are necessarily universe system of
01142   // bounded differences, so that their difference is empty.
01143   if (space_dim == 0) {
01144     x.set_empty();
01145     return;
01146   }
01147 
01148   // TODO: This is just an executable specification.
01149   //       Have to find a more efficient method.
01150   if (y.contains(x)) {
01151     x.set_empty();
01152     return;
01153   }
01154 
01155   // We take a constraint of the system y at the time and we
01156   // consider its complementary. Then we intersect the union
01157   // of these complementaries with the system x.
01158   const Constraint_System& y_cs = y.constraints();
01159   for (Constraint_System::const_iterator i = y_cs.begin(),
01160          y_cs_end = y_cs.end(); i != y_cs_end; ++i) {
01161     const Constraint& c = *i;
01162     // If the system of bounded differences `x' is included
01163     // in the system of bounded differences defined by `c',
01164     // then `c' _must_ be skipped, as adding its complement to `x'
01165     // would result in the empty system of bounded differences,
01166     // and as we would obtain a result that is less precise
01167     // than the bds-difference.
01168     if (x.relation_with(c).implies(Poly_Con_Relation::is_included()))
01169       continue;
01170     BD_Shape z = x;
01171     const Linear_Expression e = Linear_Expression(c);
01172     bool change = false;
01173     if (c.is_nonstrict_inequality())
01174       change = z.add_constraint_and_minimize(e <= 0);
01175     if (c.is_equality()) {
01176       BD_Shape w = x;
01177       if (w.add_constraint_and_minimize(e <= 0))
01178         new_bdiffs.bds_hull_assign(w);
01179       change = z.add_constraint_and_minimize(e >= 0);
01180     }
01181     if (change)
01182       new_bdiffs.bds_hull_assign(z);
01183   }
01184   *this = new_bdiffs;
01185   // The result is still closed, because both bds_hull_assign() and
01186   // add_constraint_and_minimize() preserve closure.
01187   assert(OK());
01188 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::difference_assign ( const BD_Shape< T > & y ) [inline]

Same as bds_difference_assign.

Definition at line 572 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::bds_difference_assign().

00572                                                 {
00573   bds_difference_assign(y);
00574 }

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()`
	)			`[inline]`

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.

Definition at line 1931 of file BD_Shape.templates.hh.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::affine_preimage(), and Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_image().

01933                                                                          {
01934   using Implementation::BD_Shapes::div_round_up;
01935 
01936   // The denominator cannot be zero.
01937   if (denominator == 0)
01938     throw_generic("affine_image(v, e, d)", "d == 0");
01939 
01940   // Dimension-compatibility checks.
01941   // The dimension of `expr' should not be greater than the dimension
01942   // of `*this'.
01943   const dimension_type space_dim = space_dimension();
01944   const dimension_type expr_space_dim = expr.space_dimension();
01945   if (space_dim < expr_space_dim)
01946     throw_dimension_incompatible("affine_image(v, e, d)", "e", expr);
01947 
01948   // `var' should be one of the dimensions of the shape.
01949   const dimension_type v = var.id() + 1;
01950   if (v > space_dim)
01951     throw_dimension_incompatible("affine_image(v, e, d)", var.id());
01952 
01953   // The image of an empty BDS is empty too.
01954   shortest_path_closure_assign();
01955   if (marked_empty())
01956     return;
01957 
01958   const Coefficient& b = expr.inhomogeneous_term();
01959   // Number of non-zero coefficients in `expr': will be set to
01960   // 0, 1, or 2, the latter value meaning any value greater than 1.
01961   dimension_type t = 0;
01962   // Index of the last non-zero coefficient in `expr', if any.
01963   dimension_type w = 0;
01964   // Get information about the number of non-zero coefficients in `expr'.
01965   for (dimension_type i = expr_space_dim; i-- > 0; )
01966     if (expr.coefficient(Variable(i)) != 0)
01967       if (t++ == 1)
01968         break;
01969       else
01970         w = i+1;
01971 
01972   // Now we know the form of `expr':
01973   // - If t == 0, then expr == b, with `b' a constant;
01974   // - If t == 1, then expr == a*w + b, where `w' can be `v' or another
01975   //   variable; in this second case we have to check whether `a' is
01976   //   equal to `denominator' or `-denominator', since otherwise we have
01977   //   to fall back on the general form;
01978   // - If t == 2, the `expr' is of the general form.
01979   TEMP_INTEGER(minus_den);
01980   neg_assign(minus_den, denominator);
01981 
01982   if (t == 0) {
01983     // Case 1: expr == b.
01984     // Remove all constraints on `var'.
01985     forget_all_dbm_constraints(v);
01986     // Shortest-path closure is preserved, but not reduction.
01987     if (marked_shortest_path_reduced())
01988       status.reset_shortest_path_reduced();
01989     // Add the constraint `var == b/denominator'.
01990     add_dbm_constraint(0, v, b, denominator);
01991     add_dbm_constraint(v, 0, b, minus_den);
01992     assert(OK());
01993     return;
01994   }
01995 
01996   if (t == 1) {
01997     // Value of the one and only non-zero coefficient in `expr'.
01998     const Coefficient& a = expr.coefficient(Variable(w-1));
01999     if (a == denominator || a == minus_den) {
02000       // Case 2: expr == a*w + b, with a == +/- denominator.
02001       if (w == v) {
02002         // `expr' is of the form: a*v + b.
02003         if (a == denominator) {
02004           if (b == 0)
02005             // The transformation is the identity function.
02006             return;
02007           else {
02008             // Translate all the constraints on `var',
02009             // adding or subtracting the value `b/denominator'.
02010             N d;
02011             div_round_up(d, b, denominator);
02012             N c;
02013             div_round_up(c, b, minus_den);
02014             DB_Row<N>& dbm_v = dbm[v];
02015             for (dimension_type i = space_dim + 1; i-- > 0; ) {
02016               N& dbm_vi = dbm_v[i];
02017               add_assign_r(dbm_vi, dbm_vi, c, ROUND_UP);
02018               N& dbm_iv = dbm[i][v];
02019               add_assign_r(dbm_iv, dbm_iv, d, ROUND_UP);
02020             }
02021             // Both shortest-path closure and reduction are preserved.
02022           }
02023         }
02024         else {
02025           // Here `a == -denominator'.
02026           // Remove the binary constraints on `var'.
02027           forget_binary_dbm_constraints(v);
02028           // Swap the unary constraints on `var'.
02029           std::swap(dbm[v][0], dbm[0][v]);
02030           // Shortest-path closure is not preserved.
02031           status.reset_shortest_path_closed();
02032           if (b != 0) {
02033             // Translate the unary constraints on `var',
02034             // adding or subtracting the value `b/denominator'.
02035             N c;
02036             div_round_up(c, b, minus_den);
02037             N& dbm_v0 = dbm[v][0];
02038             add_assign_r(dbm_v0, dbm_v0, c, ROUND_UP);
02039             N d;
02040             div_round_up(d, b, denominator);
02041             N& dbm_0v = dbm[0][v];
02042             add_assign_r(dbm_0v, dbm_0v, d, ROUND_UP);
02043           }
02044         }
02045       }
02046       else {
02047         // Here `w != v', so that `expr' is of the form
02048         // +/-denominator * w + b.
02049         // Remove all constraints on `var'.
02050         forget_all_dbm_constraints(v);
02051         // Shortest-path closure is preserved, but not reduction.
02052         if (marked_shortest_path_reduced())
02053           status.reset_shortest_path_reduced();
02054         if (a == denominator) {
02055           // Add the new constraint `v - w == b/denominator'.
02056           add_dbm_constraint(w, v, b, denominator);
02057           add_dbm_constraint(v, w, b, minus_den);
02058         }
02059         else {
02060           // Here a == -denominator, so that we should be adding
02061           // the constraint `v + w == b/denominator'.
02062           // Approximate it by computing lower and upper bounds for `w'.
02063           const N& dbm_w0 = dbm[w][0];
02064           if (!is_plus_infinity(dbm_w0)) {
02065             // Add the constraint `v <= b/denominator - lower_w'.
02066             N d;
02067             div_round_up(d, b, denominator);
02068             add_assign_r(dbm[0][v], d, dbm_w0, ROUND_UP);
02069             status.reset_shortest_path_closed();
02070           }
02071           const N& dbm_0w = dbm[0][w];
02072           if (!is_plus_infinity(dbm_0w)) {
02073             // Add the constraint `v >= b/denominator - upper_w'.
02074             N c;
02075             div_round_up(c, b, minus_den);
02076             add_assign_r(dbm[v][0], dbm_0w, c, ROUND_UP);
02077             status.reset_shortest_path_closed();
02078           }
02079         }
02080       }
02081       assert(OK());
02082       return;
02083     }
02084   }
02085 
02086   // General case.
02087   // Either t == 2, so that
02088   // expr == a_1*x_1 + a_2*x_2 + ... + a_n*x_n + b, where n >= 2,
02089   // or t == 1, expr == a*w + b, but a <> +/- denominator.
02090   // We will remove all the constraints on `var' and add back
02091   // constraints providing upper and lower bounds for `var'.
02092 
02093   // Compute upper approximations for `expr' and `-expr'
02094   // into `pos_sum' and `neg_sum', respectively, taking into account
02095   // the sign of `denominator'.
02096   // Note: approximating `-expr' from above and then negating the
02097   // result is the same as approximating `expr' from below.
02098   const bool is_sc = (denominator > 0);
02099   TEMP_INTEGER(minus_b);
02100   neg_assign(minus_b, b);
02101   const Coefficient& sc_b = is_sc ? b : minus_b;
02102   const Coefficient& minus_sc_b = is_sc ? minus_b : b;
02103   const Coefficient& sc_den = is_sc ? denominator : minus_den;
02104   const Coefficient& minus_sc_den = is_sc ? minus_den : denominator;
02105   // NOTE: here, for optimization purposes, `minus_expr' is only assigned
02106   // when `denominator' is negative. Do not use it unless you are sure
02107   // it has been correctly assigned.
02108   Linear_Expression minus_expr;
02109   if (!is_sc)
02110     minus_expr = -expr;
02111   const Linear_Expression& sc_expr = is_sc ? expr : minus_expr;
02112 
02113   N pos_sum;
02114   N neg_sum;
02115   // Indices of the variables that are unbounded in `this->dbm'.
02116   // (The initializations are just to quiet a compiler warning.)
02117   dimension_type pos_pinf_index = 0;
02118   dimension_type neg_pinf_index = 0;
02119   // Number of unbounded variables found.
02120   dimension_type pos_pinf_count = 0;
02121   dimension_type neg_pinf_count = 0;
02122 
02123   // Approximate the inhomogeneous term.
02124   assign_r(pos_sum, sc_b, ROUND_UP);
02125   assign_r(neg_sum, minus_sc_b, ROUND_UP);
02126 
02127   // Approximate the homogeneous part of `sc_expr'.
02128   // Note: indices above `w' can be disregarded, as they all have
02129   // a zero coefficient in `sc_expr'.
02130   const DB_Row<N>& dbm_0 = dbm[0];
02131   for (dimension_type i = w; i > 0; --i) {
02132     const Coefficient& sc_i = sc_expr.coefficient(Variable(i-1));
02133     const int sign_i = sgn(sc_i);
02134     if (sign_i > 0) {
02135       N coeff_i;
02136       assign_r(coeff_i, sc_i, ROUND_UP);
02137       // Approximating `sc_expr'.
02138       if (pos_pinf_count <= 1) {
02139         const N& up_approx_i = dbm_0[i];
02140         if (!is_plus_infinity(up_approx_i))
02141           add_mul_assign_r(pos_sum, coeff_i, up_approx_i, ROUND_UP);
02142         else {
02143           ++pos_pinf_count;
02144           pos_pinf_index = i;
02145         }
02146       }
02147       // Approximating `-sc_expr'.
02148       if (neg_pinf_count <= 1) {
02149         const N& up_approx_minus_i = dbm[i][0];
02150         if (!is_plus_infinity(up_approx_minus_i))
02151           add_mul_assign_r(neg_sum, coeff_i, up_approx_minus_i, ROUND_UP);
02152         else {
02153           ++neg_pinf_count;
02154           neg_pinf_index = i;
02155         }
02156       }
02157     }
02158     else if (sign_i < 0) {
02159       TEMP_INTEGER(minus_sc_i);
02160       neg_assign(minus_sc_i, sc_i);
02161       N minus_coeff_i;
02162       assign_r(minus_coeff_i, minus_sc_i, ROUND_UP);
02163       // Approximating `sc_expr'.
02164       if (pos_pinf_count <= 1) {
02165         const N& up_approx_minus_i = dbm[i][0];
02166         if (!is_plus_infinity(up_approx_minus_i))
02167           add_mul_assign_r(pos_sum,
02168                            minus_coeff_i, up_approx_minus_i, ROUND_UP);
02169         else {
02170           ++pos_pinf_count;
02171           pos_pinf_index = i;
02172         }
02173       }
02174       // Approximating `-sc_expr'.
02175       if (neg_pinf_count <= 1) {
02176         const N& up_approx_i = dbm_0[i];
02177         if (!is_plus_infinity(up_approx_i))
02178           add_mul_assign_r(neg_sum, minus_coeff_i, up_approx_i, ROUND_UP);
02179         else {
02180           ++neg_pinf_count;
02181           neg_pinf_index = i;
02182         }
02183       }
02184     }
02185   }
02186 
02187   // Remove all constraints on 'v'.
02188   forget_all_dbm_constraints(v);
02189   // Shortest-path closure is maintained, but not reduction.
02190   if (marked_shortest_path_reduced())
02191     status.reset_shortest_path_reduced();
02192   // Return immediately if no approximation could be computed.
02193   if (pos_pinf_count > 1 && neg_pinf_count > 1) {
02194     assert(OK());
02195     return;
02196   }
02197 
02198   // In the following, shortest-path closure will be definitely lost.
02199   status.reset_shortest_path_closed();
02200 
02201   // Before computing quotients, the denominator should be approximated
02202   // towards zero. Since `sc_den' is known to be positive, this amounts to
02203   // rounding downwards, which is achieved as usual by rounding upwards
02204   // `minus_sc_den' and negating again the result.
02205   N down_sc_den;
02206   assign_r(down_sc_den, minus_sc_den, ROUND_UP);
02207   neg_assign_r(down_sc_den, down_sc_den, ROUND_UP);
02208 
02209   // Exploit the upper approximation, if possible.
02210   if (pos_pinf_count <= 1) {
02211     // Compute quotient (if needed).
02212     if (down_sc_den != 1)
02213       div_assign_r(pos_sum, pos_sum, down_sc_den, ROUND_UP);
02214     // Add the upper bound constraint, if meaningful.
02215     if (pos_pinf_count == 0) {
02216       // Add the constraint `v <= pos_sum'.
02217       DB_Row<N>& dbm_0 = dbm[0];
02218       assign_r(dbm_0[v], pos_sum, ROUND_UP);
02219       // Deduce constraints of the form `v - u', where `u != v'.
02220       deduce_v_minus_u_bounds(v, w, sc_expr, sc_den, pos_sum);
02221     }
02222     else
02223       // Here `pos_pinf_count == 1'.
02224       if (pos_pinf_index != v
02225           && sc_expr.coefficient(Variable(pos_pinf_index-1)) == sc_den)
02226         // Add the constraint `v - pos_pinf_index <= pos_sum'.
02227         assign_r(dbm[pos_pinf_index][v], pos_sum, ROUND_UP);
02228   }
02229 
02230   // Exploit the lower approximation, if possible.
02231   if (neg_pinf_count <= 1) {
02232     // Compute quotient (if needed).
02233     if (down_sc_den != 1)
02234       div_assign_r(neg_sum, neg_sum, down_sc_den, ROUND_UP);
02235     // Add the lower bound constraint, if meaningful.
02236     if (neg_pinf_count == 0) {
02237       // Add the constraint `v >= -neg_sum', i.e., `-v <= neg_sum'.
02238       DB_Row<N>& dbm_v = dbm[v];
02239       assign_r(dbm_v[0], neg_sum, ROUND_UP);
02240       // Deduce constraints of the form `u - v', where `u != v'.
02241       deduce_u_minus_v_bounds(v, w, sc_expr, sc_den, neg_sum);
02242     }
02243     else
02244       // Here `neg_pinf_count == 1'.
02245       if (neg_pinf_index != v
02246           && sc_expr.coefficient(Variable(neg_pinf_index-1)) == sc_den)
02247         // Add the constraint `v - neg_pinf_index >= -neg_sum',
02248         // i.e., `neg_pinf_index - v <= neg_sum'.
02249         assign_r(dbm[v][neg_pinf_index], neg_sum, ROUND_UP);
02250   }
02251 
02252   assert(OK());
02253 }

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()`
	)			`[inline]`

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.

Definition at line 2257 of file BD_Shape.templates.hh.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_preimage().

02259                                                                             {
02260   // The denominator cannot be zero.
02261   if (denominator == 0)
02262     throw_generic("affine_preimage(v, e, d)", "d == 0");
02263 
02264   // Dimension-compatibility checks.
02265   // The dimension of `expr' should not be greater than the dimension
02266   // of `*this'.
02267   const dimension_type space_dim = space_dimension();
02268   const dimension_type expr_space_dim = expr.space_dimension();
02269   if (space_dim < expr_space_dim)
02270     throw_dimension_incompatible("affine_preimage(v, e, d)", "e", expr);
02271 
02272   // `var' should be one of the dimensions of
02273   // the systems of bounded differences.
02274   const dimension_type v = var.id() + 1;
02275   if (v > space_dim)
02276     throw_dimension_incompatible("affine_preimage(v, e, d)", var.id());
02277 
02278   // The image of an empty BDS is empty too.
02279   shortest_path_closure_assign();
02280   if (marked_empty())
02281     return;
02282 
02283   const Coefficient& b = expr.inhomogeneous_term();
02284   // Number of non-zero coefficients in `expr': will be set to
02285   // 0, 1, or 2, the latter value meaning any value greater than 1.
02286   dimension_type t = 0;
02287   // Index of the last non-zero coefficient in `expr', if any.
02288   dimension_type j = 0;
02289   // Get information about the number of non-zero coefficients in `expr'.
02290   for (dimension_type i = expr_space_dim; i-- > 0; )
02291     if (expr.coefficient(Variable(i)) != 0)
02292       if (t++ == 1)
02293         break;
02294       else
02295         j = i;
02296 
02297   // Now we know the form of `expr':
02298   // - If t == 0, then expr = b, with `b' a constant;
02299   // - If t == 1, then expr = a*w + b, where `w' can be `v' or another
02300   //   variable; in this second case we have to check whether `a' is
02301   //   equal to `denominator' or `-denominator', since otherwise we have
02302   //   to fall back on the general form;
02303   // - If t > 1, the `expr' is of the general form.
02304   if (t == 0) {
02305     // Case 1: expr = n; remove all constraints on `var'.
02306     forget_all_dbm_constraints(v);
02307     // Shortest-path closure is preserved, but not reduction.
02308     if (marked_shortest_path_reduced())
02309       status.reset_shortest_path_reduced();
02310     assert(OK());
02311     return;
02312   }
02313 
02314   if (t == 1) {
02315     // Value of the one and only non-zero coefficient in `expr'.
02316     const Coefficient& a = expr.coefficient(Variable(j));
02317     if (a == denominator || a == -denominator) {
02318       // Case 2: expr = a*w + b, with a = +/- denominator.
02319       if (j == var.id())
02320         // Apply affine_image() on the inverse of this transformation.
02321         affine_image(var, a*var - b, denominator);
02322       else {
02323         // `expr == a*w + b', where `w != v'.
02324         // Remove all constraints on `var'.
02325         forget_all_dbm_constraints(v);
02326         // Shortest-path closure is preserved, but not reduction.
02327         if (marked_shortest_path_reduced())
02328           status.reset_shortest_path_reduced();
02329       }
02330       assert(OK());
02331       return;
02332     }
02333   }
02334 
02335   // General case.
02336   // Either t == 2, so that
02337   // expr = a_1*x_1 + a_2*x_2 + ... + a_n*x_n + b, where n >= 2,
02338   // or t = 1, expr = a*w + b, but a <> +/- denominator.
02339   const Coefficient& expr_v = expr.coefficient(var);
02340   if (expr_v != 0) {
02341     // The transformation is invertible.
02342     Linear_Expression inverse((expr_v + denominator)*var);
02343     inverse -= expr;
02344     affine_image(var, inverse, expr_v);
02345   }
02346   else {
02347     // Transformation not invertible: all constraints on `var' are lost.
02348     forget_all_dbm_constraints(v);
02349     // Shortest-path closure is preserved, but not reduction.
02350     if (marked_shortest_path_reduced())
02351       status.reset_shortest_path_reduced();
02352   }
02353   assert(OK());
02354 }

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()`
	)			`[inline]`

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.

Definition at line 2358 of file BD_Shape.templates.hh.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_image(), and Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_preimage().

02362                                                    {
02363   using Implementation::BD_Shapes::div_round_up;
02364 
02365   // The denominator cannot be zero.
02366   if (denominator == 0)
02367     throw_generic("generalized_affine_image(v, r, e, d)", "d == 0");
02368 
02369   // Dimension-compatibility checks.
02370   // The dimension of `expr' should not be greater than the dimension
02371   // of `*this'.
02372   const dimension_type space_dim = space_dimension();
02373   const dimension_type expr_space_dim = expr.space_dimension();
02374   if (space_dim < expr_space_dim)
02375     throw_dimension_incompatible("generalized_affine_image(v, r, e, d)",
02376                                  "e", expr);
02377 
02378   // `var' should be one of the dimensions of the BDS.
02379   const dimension_type v = var.id() + 1;
02380   if (v > space_dim)
02381     throw_dimension_incompatible("generalized_affine_image(v, r, e, d)",
02382                                  var.id());
02383 
02384   // The relation symbol cannot be a strict relation symbol.
02385   if (relsym == LESS_THAN || relsym == GREATER_THAN)
02386     throw_generic("generalized_affine_image(v, r, e, d)",
02387                   "r is a strict relation symbol and "
02388                   "*this is a BD_Shape");
02389 
02390   if (relsym == EQUAL) {
02391     // The relation symbol is "==":
02392     // this is just an affine image computation.
02393     affine_image(var, expr, denominator);
02394     assert(OK());
02395     return;
02396   }
02397 
02398   // The image of an empty BDS is empty too.
02399   shortest_path_closure_assign();
02400   if (marked_empty())
02401     return;
02402 
02403   const Coefficient& b = expr.inhomogeneous_term();
02404   // Number of non-zero coefficients in `expr': will be set to
02405   // 0, 1, or 2, the latter value meaning any value greater than 1.
02406   dimension_type t = 0;
02407   // Index of the last non-zero coefficient in `expr', if any.
02408   dimension_type w = 0;
02409   // Get information about the number of non-zero coefficients in `expr'.
02410   for (dimension_type i = expr_space_dim; i-- > 0; )
02411     if (expr.coefficient(Variable(i)) != 0)
02412       if (t++ == 1)
02413         break;
02414       else
02415         w = i+1;
02416 
02417   // Now we know the form of `expr':
02418   // - If t == 0, then expr == b, with `b' a constant;
02419   // - If t == 1, then expr == a*w + b, where `w' can be `v' or another
02420   //   variable; in this second case we have to check whether `a' is
02421   //   equal to `denominator' or `-denominator', since otherwise we have
02422   //   to fall back on the general form;
02423   // - If t == 2, the `expr' is of the general form.
02424   DB_Row<N>& dbm_0 = dbm[0];
02425   DB_Row<N>& dbm_v = dbm[v];
02426   TEMP_INTEGER(minus_den);
02427   neg_assign(minus_den, denominator);
02428 
02429   if (t == 0) {
02430     // Case 1: expr == b.
02431     // Remove all constraints on `var'.
02432     forget_all_dbm_constraints(v);
02433     // Both shortest-path closure and reduction are lost.
02434     status.reset_shortest_path_closed();
02435     switch (relsym) {
02436     case LESS_THAN_OR_EQUAL:
02437       // Add the constraint `var <= b/denominator'.
02438       add_dbm_constraint(0, v, b, denominator);
02439       break;
02440     case GREATER_THAN_OR_EQUAL:
02441       // Add the constraint `var >= b/denominator',
02442       // i.e., `-var <= -b/denominator',
02443       add_dbm_constraint(v, 0, b, minus_den);
02444       break;
02445     default:
02446       // We already dealt with the other cases.
02447       throw std::runtime_error("PPL internal error");
02448       break;
02449     }
02450     assert(OK());
02451     return;
02452   }
02453 
02454   if (t == 1) {
02455     // Value of the one and only non-zero coefficient in `expr'.
02456     const Coefficient& a = expr.coefficient(Variable(w-1));
02457     if (a == denominator || a == minus_den) {
02458       // Case 2: expr == a*w + b, with a == +/- denominator.
02459       N d;
02460       switch (relsym) {
02461       case LESS_THAN_OR_EQUAL:
02462         div_round_up(d, b, denominator);
02463         if (w == v) {
02464           // `expr' is of the form: a*v + b.
02465           // Shortest-path closure and reduction are not preserved.
02466           status.reset_shortest_path_closed();
02467           if (a == denominator) {
02468             // Translate each constraint `v - w <= dbm_wv'
02469             // into the constraint `v - w <= dbm_wv + b/denominator';
02470             // forget each constraint `w - v <= dbm_vw'.
02471             for (dimension_type i = space_dim + 1; i-- > 0; ) {
02472               N& dbm_iv = dbm[i][v];
02473               add_assign_r(dbm_iv, dbm_iv, d, ROUND_UP);
02474               dbm_v[i] = PLUS_INFINITY;
02475             }
02476           }
02477           else {
02478             // Here `a == -denominator'.
02479             // Translate the constraint `0 - v <= dbm_v0'
02480             // into the constraint `0 - v <= dbm_v0 + b/denominator'.
02481             N& dbm_v0 = dbm_v[0];
02482             add_assign_r(dbm_0[v], dbm_v0, d, ROUND_UP);
02483             // Forget all the other constraints on `v'.
02484             dbm_v0 = PLUS_INFINITY;
02485             forget_binary_dbm_constraints(v);
02486           }
02487         }
02488         else {
02489           // Here `w != v', so that `expr' is of the form
02490           // +/-denominator * w + b, with `w != v'.
02491           // Remove all constraints on `v'.
02492           forget_all_dbm_constraints(v);
02493           // Shortest-path closure is preserved, but not reduction.
02494           if (marked_shortest_path_reduced())
02495             status.reset_shortest_path_reduced();
02496           if (a == denominator)
02497             // Add the new constraint `v - w <= b/denominator'.
02498             add_dbm_constraint(w, v, d);
02499           else {
02500             // Here a == -denominator, so that we should be adding
02501             // the constraint `v <= b/denominator - w'.
02502             // Approximate it by computing a lower bound for `w'.
02503             const N& dbm_w0 = dbm[w][0];
02504             if (!is_plus_infinity(dbm_w0)) {
02505               // Add the constraint `v <= b/denominator - lb_w'.
02506               add_assign_r(dbm_0[v], d, dbm_w0, ROUND_UP);
02507               // Shortest-path closure is not preserved.
02508               status.reset_shortest_path_closed();
02509             }
02510           }
02511         }
02512         break;
02513 
02514       case GREATER_THAN_OR_EQUAL:
02515         div_round_up(d, b, minus_den);
02516         if (w == v) {
02517           // `expr' is of the form: a*w + b.
02518           // Shortest-path closure and reduction are not preserved.
02519           status.reset_shortest_path_closed();
02520           if (a == denominator) {
02521             // Translate each constraint `w - v <= dbm_vw'
02522             // into the constraint `w - v <= dbm_vw - b/denominator';
02523             // forget each constraint `v - w <= dbm_wv'.
02524             for (dimension_type i = space_dim + 1; i-- > 0; ) {
02525               N& dbm_vi = dbm_v[i];
02526               add_assign_r(dbm_vi, dbm_vi, d, ROUND_UP);
02527               dbm[i][v] = PLUS_INFINITY;
02528             }
02529           }
02530           else {
02531             // Here `a == -denominator'.
02532             // Translate the constraint `0 - v <= dbm_v0'
02533             // into the constraint `0 - v <= dbm_0v - b/denominator'.
02534             N& dbm_0v = dbm_0[v];
02535             add_assign_r(dbm_v[0], dbm_0v, d, ROUND_UP);
02536             // Forget all the other constraints on `v'.
02537             dbm_0v = PLUS_INFINITY;
02538             forget_binary_dbm_constraints(v);
02539           }
02540         }
02541         else {
02542           // Here `w != v', so that `expr' is of the form
02543           // +/-denominator * w + b, with `w != v'.
02544           // Remove all constraints on `v'.
02545           forget_all_dbm_constraints(v);
02546           // Shortest-path closure is preserved, but not reduction.
02547           if (marked_shortest_path_reduced())
02548             status.reset_shortest_path_reduced();
02549           if (a == denominator)
02550             // Add the new constraint `v - w >= b/denominator',
02551             // i.e., `w - v <= -b/denominator'.
02552             add_dbm_constraint(v, w, d);
02553           else {
02554             // Here a == -denominator, so that we should be adding
02555             // the constraint `v >= -w + b/denominator',
02556             // i.e., `-v <= w - b/denominator'.
02557             // Approximate it by computing an upper bound for `w'.
02558             const N& dbm_0w = dbm_0[w];
02559             if (!is_plus_infinity(dbm_0w)) {
02560               // Add the constraint `-v <= ub_w - b/denominator'.
02561               add_assign_r(dbm_v[0], dbm_0w, d, ROUND_UP);
02562               // Shortest-path closure is not preserved.
02563               status.reset_shortest_path_closed();
02564             }
02565           }
02566         }
02567         break;
02568 
02569       default:
02570         // We already dealt with the other cases.
02571         throw std::runtime_error("PPL internal error");
02572         break;
02573       }
02574       assert(OK());
02575       return;
02576     }
02577   }
02578 
02579   // General case.
02580   // Either t == 2, so that
02581   // expr == a_1*x_1 + a_2*x_2 + ... + a_n*x_n + b, where n >= 2,
02582   // or t == 1, expr == a*w + b, but a <> +/- denominator.
02583   // We will remove all the constraints on `v' and add back
02584   // a constraint providing an upper or a lower bound for `v'
02585   // (depending on `relsym').
02586   const bool is_sc = (denominator > 0);
02587   TEMP_INTEGER(minus_b);
02588   neg_assign(minus_b, b);
02589   const Coefficient& sc_b = is_sc ? b : minus_b;
02590   const Coefficient& minus_sc_b = is_sc ? minus_b : b;
02591   const Coefficient& sc_den = is_sc ? denominator : minus_den;
02592   const Coefficient& minus_sc_den = is_sc ? minus_den : denominator;
02593   // NOTE: here, for optimization purposes, `minus_expr' is only assigned
02594   // when `denominator' is negative. Do not use it unless you are sure
02595   // it has been correctly assigned.
02596   Linear_Expression minus_expr;
02597   if (!is_sc)
02598     minus_expr = -expr;
02599   const Linear_Expression& sc_expr = is_sc ? expr : minus_expr;
02600 
02601   N sum;
02602   // Index of variable that is unbounded in `this->dbm'.
02603   // (The initialization is just to quiet a compiler warning.)
02604   dimension_type pinf_index = 0;
02605   // Number of unbounded variables found.
02606   dimension_type pinf_count = 0;
02607 
02608   switch (relsym) {
02609   case LESS_THAN_OR_EQUAL:
02610     // Compute an upper approximation for `sc_expr' into `sum'.
02611 
02612     // Approximate the inhomogeneous term.
02613     assign_r(sum, sc_b, ROUND_UP);
02614     // Approximate the homogeneous part of `sc_expr'.
02615     // Note: indices above `w' can be disregarded, as they all have
02616     // a zero coefficient in `sc_expr'.
02617     for (dimension_type i = w; i > 0; --i) {
02618       const Coefficient& sc_i = sc_expr.coefficient(Variable(i-1));
02619       const int sign_i = sgn(sc_i);
02620       if (sign_i == 0)
02621         continue;
02622       // Choose carefully: we are approximating `sc_expr'.
02623       const N& approx_i = (sign_i > 0) ? dbm_0[i] : dbm[i][0];
02624       if (is_plus_infinity(approx_i)) {
02625         if (++pinf_count > 1)
02626           break;
02627         pinf_index = i;
02628         continue;
02629       }
02630       N coeff_i;
02631       if (sign_i > 0)
02632         assign_r(coeff_i, sc_i, ROUND_UP);
02633       else {
02634         TEMP_INTEGER(minus_sc_i);
02635         neg_assign(minus_sc_i, sc_i);
02636         assign_r(coeff_i, minus_sc_i, ROUND_UP);
02637       }
02638       add_mul_assign_r(sum, coeff_i, approx_i, ROUND_UP);
02639     }
02640 
02641     // Remove all constraints on `v'.
02642     forget_all_dbm_constraints(v);
02643     // Shortest-path closure is preserved, but not reduction.
02644     if (marked_shortest_path_reduced())
02645       status.reset_shortest_path_reduced();
02646     // Return immediately if no approximation could be computed.
02647     if (pinf_count > 1) {
02648       assert(OK());
02649       return;
02650     }
02651 
02652     // Divide by the (sign corrected) denominator (if needed).
02653     if (sc_den != 1) {
02654       // Before computing the quotient, the denominator should be approximated
02655       // towards zero. Since `sc_den' is known to be positive, this amounts to
02656       // rounding downwards, which is achieved as usual by rounding upwards
02657       // `minus_sc_den' and negating again the result.
02658       N down_sc_den;
02659       assign_r(down_sc_den, minus_sc_den, ROUND_UP);
02660       neg_assign_r(down_sc_den, down_sc_den, ROUND_UP);
02661       div_assign_r(sum, sum, down_sc_den, ROUND_UP);
02662     }
02663 
02664     if (pinf_count == 0) {
02665       // Add the constraint `v <= sum'.
02666       add_dbm_constraint(0, v, sum);
02667       // Deduce constraints of the form `v - u', where `u != v'.
02668       deduce_v_minus_u_bounds(v, w, sc_expr, sc_den, sum);
02669     }
02670     else if (pinf_count == 1)
02671       if (pinf_index != v
02672           && expr.coefficient(Variable(pinf_index-1)) == denominator)
02673         // Add the constraint `v - pinf_index <= sum'.
02674         add_dbm_constraint(pinf_index, v, sum);
02675     break;
02676 
02677   case GREATER_THAN_OR_EQUAL:
02678     // Compute an upper approximation for `-sc_expr' into `sum'.
02679     // Note: approximating `-sc_expr' from above and then negating the
02680     // result is the same as approximating `sc_expr' from below.
02681 
02682     // Approximate the inhomogeneous term.
02683     assign_r(sum, minus_sc_b, ROUND_UP);
02684     // Approximate the homogeneous part of `-sc_expr'.
02685     for (dimension_type i = expr_space_dim + 1; i > 0; --i) {
02686       const Coefficient& sc_i = sc_expr.coefficient(Variable(i-1));
02687       const int sign_i = sgn(sc_i);
02688       if (sign_i == 0)
02689         continue;
02690       // Choose carefully: we are approximating `-sc_expr'.
02691       const N& approx_i = (sign_i > 0) ? dbm[i][0] : dbm_0[i];
02692       if (is_plus_infinity(approx_i)) {
02693         if (++pinf_count > 1)
02694           break;
02695         pinf_index = i;
02696         continue;
02697       }
02698       N coeff_i;
02699       if (sign_i > 0)
02700         assign_r(coeff_i, sc_i, ROUND_UP);
02701       else {
02702         TEMP_INTEGER(minus_sc_i);
02703         neg_assign(minus_sc_i, sc_i);
02704         assign_r(coeff_i, minus_sc_i, ROUND_UP);
02705       }
02706       add_mul_assign_r(sum, coeff_i, approx_i, ROUND_UP);
02707     }
02708 
02709     // Remove all constraints on `var'.
02710     forget_all_dbm_constraints(v);
02711     // Shortest-path closure is preserved, but not reduction.
02712     if (marked_shortest_path_reduced())
02713       status.reset_shortest_path_reduced();
02714     // Return immediately if no approximation could be computed.
02715     if (pinf_count > 1) {
02716       assert(OK());
02717       return;
02718     }
02719 
02720     // Divide by the (sign corrected) denominator (if needed).
02721     if (sc_den != 1) {
02722       // Before computing the quotient, the denominator should be approximated
02723       // towards zero. Since `sc_den' is known to be positive, this amounts to
02724       // rounding downwards, which is achieved as usual by rounding upwards
02725       // `minus_sc_den' and negating again the result.
02726       N down_sc_den;
02727       assign_r(down_sc_den, minus_sc_den, ROUND_UP);
02728       neg_assign_r(down_sc_den, down_sc_den, ROUND_UP);
02729       div_assign_r(sum, sum, down_sc_den, ROUND_UP);
02730     }
02731 
02732     if (pinf_count == 0) {
02733       // Add the constraint `v >= -sum', i.e., `-v <= sum'.
02734       add_dbm_constraint(v, 0, sum);
02735       // Deduce constraints of the form `u - v', where `u != v'.
02736       deduce_u_minus_v_bounds(v, w, sc_expr, sc_den, sum);
02737     }
02738     else if (pinf_count == 1)
02739       if (pinf_index != v
02740           && expr.coefficient(Variable(pinf_index-1)) == denominator)
02741         // Add the constraint `v - pinf_index >= -sum',
02742         // i.e., `pinf_index - v <= sum'.
02743         add_dbm_constraint(v, pinf_index, sum);
02744     break;
02745 
02746   default:
02747     // We already dealt with the other cases.
02748     throw std::runtime_error("PPL internal error");
02749     break;
02750   }
02751   assert(OK());
02752 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::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 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.

Definition at line 2756 of file BD_Shape.templates.hh.

02758                                                                     {
02759   // Dimension-compatibility checks.
02760   // The dimension of `lhs' should not be greater than the dimension
02761   // of `*this'.
02762   const dimension_type space_dim = space_dimension();
02763   const dimension_type lhs_space_dim = lhs.space_dimension();
02764   if (space_dim < lhs_space_dim)
02765     throw_dimension_incompatible("generalized_affine_image(e1, r, e2)",
02766                                  "e1", lhs);
02767 
02768   // The dimension of `rhs' should not be greater than the dimension
02769   // of `*this'.
02770   const dimension_type rhs_space_dim = rhs.space_dimension();
02771   if (space_dim < rhs_space_dim)
02772     throw_dimension_incompatible("generalized_affine_image(e1, r, e2)",
02773                                  "e2", rhs);
02774 
02775   // Strict relation symbols are not admitted for BDSs.
02776   if (relsym == LESS_THAN || relsym == GREATER_THAN)
02777     throw_generic("generalized_affine_image(e1, r, e2)",
02778                   "r is a strict relation symbol and "
02779                   "*this is a BD_Shape");
02780 
02781   // The image of an empty BDS is empty.
02782   shortest_path_closure_assign();
02783   if (marked_empty())
02784     return;
02785 
02786   // Number of non-zero coefficients in `lhs': will be set to
02787   // 0, 1, or 2, the latter value meaning any value greater than 1.
02788   dimension_type t_lhs = 0;
02789   // Index of the last non-zero coefficient in `lhs', if any.
02790   dimension_type j_lhs = 0;
02791   // Compute the number of the non-zero components of `lhs'.
02792   for (dimension_type i = lhs_space_dim; i-- > 0; )
02793     if (lhs.coefficient(Variable(i)) != 0)
02794       if (t_lhs++ == 1)
02795         break;
02796       else
02797         j_lhs = i;
02798 
02799   const Coefficient& b_lhs = lhs.inhomogeneous_term();
02800 
02801   if (t_lhs == 0) {
02802     // `lhs' is a constant.
02803     // In principle, it is sufficient to add the constraint `lhs relsym rhs'.
02804     // Note that this constraint is a bounded difference if `t_rhs <= 1'
02805     // or `t_rhs > 1' and `rhs == a*v - a*w + b_rhs'. If `rhs' is of a
02806     // more general form, it will be simply ignored.
02807     // TODO: if it is not a bounded difference, should we compute
02808     // approximations for this constraint?
02809     switch (relsym) {
02810     case LESS_THAN_OR_EQUAL:
02811       add_constraint(lhs <= rhs);
02812       break;
02813     case EQUAL:
02814       add_constraint(lhs == rhs);
02815       break;
02816     case GREATER_THAN_OR_EQUAL:
02817       add_constraint(lhs >= rhs);
02818       break;
02819     default:
02820       // We already dealt with the other cases.
02821       throw std::runtime_error("PPL internal error");
02822       break;
02823     }
02824   }
02825   else if (t_lhs == 1) {
02826     // Here `lhs == a_lhs * v + b_lhs'.
02827     // Independently from the form of `rhs', we can exploit the
02828     // method computing generalized affine images for a single variable.
02829     Variable v(j_lhs);
02830     // Compute a sign-corrected relation symbol.
02831     const Coefficient& den = lhs.coefficient(v);
02832     Relation_Symbol new_relsym = relsym;
02833     if (den < 0)
02834       if (relsym == LESS_THAN_OR_EQUAL)
02835         new_relsym = GREATER_THAN_OR_EQUAL;
02836       else if (relsym == GREATER_THAN_OR_EQUAL)
02837         new_relsym = LESS_THAN_OR_EQUAL;
02838     Linear_Expression expr = rhs - b_lhs;
02839     generalized_affine_image(v, new_relsym, expr, den);
02840   }
02841   else {
02842     // Here `lhs' is of the general form, having at least two variables.
02843     // Compute the set of variables occurring in `lhs'.
02844     bool lhs_vars_intersects_rhs_vars = false;
02845     std::vector<Variable> lhs_vars;
02846     for (dimension_type i = lhs_space_dim; i-- > 0; )
02847       if (lhs.coefficient(Variable(i)) != 0) {
02848         lhs_vars.push_back(Variable(i));
02849         if (rhs.coefficient(Variable(i)) != 0)
02850           lhs_vars_intersects_rhs_vars = true;
02851       }
02852 
02853     if (!lhs_vars_intersects_rhs_vars) {
02854       // `lhs' and `rhs' variables are disjoint.
02855       // Cylindrificate on all variables in the lhs.
02856       for (dimension_type i = lhs_vars.size(); i-- > 0; )
02857         forget_all_dbm_constraints(lhs_vars[i].id() + 1);
02858       // Constrain the left hand side expression so that it is related to
02859       // the right hand side expression as dictated by `relsym'.
02860       // TODO: if the following constraint is NOT a bounded difference,
02861       // it will be simply ignored. Should we compute approximations for it?
02862       switch (relsym) {
02863       case LESS_THAN_OR_EQUAL:
02864         add_constraint(lhs <= rhs);
02865         break;
02866       case EQUAL:
02867         add_constraint(lhs == rhs);
02868         break;
02869       case GREATER_THAN_OR_EQUAL:
02870         add_constraint(lhs >= rhs);
02871         break;
02872       default:
02873         // We already dealt with the other cases.
02874         throw std::runtime_error("PPL internal error");
02875         break;
02876       }
02877     }
02878     else {
02879       // Some variables in `lhs' also occur in `rhs'.
02880 
02881 #if 1 // Simplified computation (see the TODO note below).
02882 
02883       for (dimension_type i = lhs_vars.size(); i-- > 0; )
02884         forget_all_dbm_constraints(lhs_vars[i].id() + 1);
02885 
02886 #else // Currently unnecessarily complex computation.
02887 
02888       // More accurate computation that is worth doing only if
02889       // the following TODO note is accurately dealt with.
02890 
02891       // To ease the computation, we add an additional dimension.
02892       const Variable new_var = Variable(space_dim);
02893       add_space_dimensions_and_embed(1);
02894       // Constrain the new dimension to be equal to `rhs'.
02895       // NOTE: calling affine_image() instead of add_constraint()
02896       // ensures some approximation is tried even when the constraint
02897       // is not a bounded difference.
02898       affine_image(new_var, rhs);
02899       // Cylindrificate on all variables in the lhs.
02900       // NOTE: enforce shortest-path closure for precision.
02901       shortest_path_closure_assign();
02902       assert(!marked_empty());
02903       for (dimension_type i = lhs_vars.size(); i-- > 0; )
02904         forget_all_dbm_constraints(lhs_vars[i].id() + 1);
02905       // Constrain the new dimension so that it is related to
02906       // the left hand side as dictated by `relsym'.
02907       // TODO: each one of the following constraints is definitely NOT
02908       // a bounded differences (since it has 3 variables at least).
02909       // Thus, the method add_constraint() will simply ignore it.
02910       // Should we compute approximations for this constraint?
02911       switch (relsym) {
02912       case LESS_THAN_OR_EQUAL:
02913         add_constraint(lhs <= new_var);
02914         break;
02915       case EQUAL:
02916         add_constraint(lhs == new_var);
02917         break;
02918       case GREATER_THAN_OR_EQUAL:
02919         add_constraint(lhs >= new_var);
02920         break;
02921       default:
02922         // We already dealt with the other cases.
02923         throw std::runtime_error("PPL internal error");
02924         break;
02925       }
02926       // Remove the temporarily added dimension.
02927       remove_higher_space_dimensions(space_dim-1);
02928 #endif // Currently unnecessarily complex computation.
02929     }
02930   }
02931 
02932   assert(OK());
02933 }

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()`
	)			`[inline]`

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.

Definition at line 2937 of file BD_Shape.templates.hh.

02941                                                       {
02942   using Implementation::BD_Shapes::div_round_up;
02943 
02944   // The denominator cannot be zero.
02945   if (denominator == 0)
02946     throw_generic("generalized_affine_preimage(v, r, e, d)", "d == 0");
02947 
02948   // Dimension-compatibility checks.
02949   // The dimension of `expr' should not be greater than the dimension
02950   // of `*this'.
02951   const dimension_type space_dim = space_dimension();
02952   const dimension_type expr_space_dim = expr.space_dimension();
02953   if (space_dim < expr_space_dim)
02954     throw_dimension_incompatible("generalized_affine_preimage(v, r, e, d)",
02955                                  "e", expr);
02956 
02957   // `var' should be one of the dimensions of the BDS.
02958   const dimension_type v = var.id() + 1;
02959   if (v > space_dim)
02960     throw_dimension_incompatible("generalized_affine_preimage(v, r, e, d)",
02961                                  var.id());
02962 
02963   // The relation symbol cannot be a strict relation symbol.
02964   if (relsym == LESS_THAN || relsym == GREATER_THAN)
02965     throw_generic("generalized_affine_preimage(v, r, e, d)",
02966                   "r is a strict relation symbol and "
02967                   "*this is a BD_Shape");
02968 
02969   if (relsym == EQUAL) {
02970     // The relation symbol is "==":
02971     // this is just an affine preimage computation.
02972     affine_preimage(var, expr, denominator);
02973     assert(OK());
02974     return;
02975   }
02976 
02977   // The image of an empty BDS is empty too.
02978   shortest_path_closure_assign();
02979   if (marked_empty())
02980     return;
02981 
02982   // Check whether the preimage of this affine relation can be easily
02983   // computed as the image of its inverse relation.
02984   const Coefficient& expr_v = expr.coefficient(var);
02985   if (expr_v != 0) {
02986     const Relation_Symbol reversed_relsym = (relsym == LESS_THAN_OR_EQUAL)
02987       ? GREATER_THAN_OR_EQUAL : LESS_THAN_OR_EQUAL;
02988     const Linear_Expression inverse
02989       = expr - (expr_v + denominator)*var;
02990     TEMP_INTEGER(inverse_den);
02991     neg_assign(inverse_den, expr_v);
02992     const Relation_Symbol inverse_relsym
02993       = (sgn(denominator) == sgn(inverse_den)) ? relsym : reversed_relsym;
02994     generalized_affine_image(var, inverse_relsym, inverse, inverse_den);
02995     return;
02996   }
02997 
02998   // Here `var_coefficient == 0', so that the preimage cannot
02999   // be easily computed by inverting the affine relation.
03000   // Shrink the BD shape by adding the constraint induced
03001   // by the affine relation.
03002   const Coefficient& b = expr.inhomogeneous_term();
03003   // Number of non-zero coefficients in `expr': will be set to
03004   // 0, 1, or 2, the latter value meaning any value greater than 1.
03005   dimension_type t = 0;
03006   // Index of the last non-zero coefficient in `expr', if any.
03007   dimension_type j = 0;
03008   // Get information about the number of non-zero coefficients in `expr'.
03009   for (dimension_type i = expr_space_dim; i-- > 0; )
03010     if (expr.coefficient(Variable(i)) != 0)
03011       if (t++ == 1)
03012         break;
03013       else
03014         j = i+1;
03015 
03016   // Now we know the form of `expr':
03017   // - If t == 0, then expr == b, with `b' a constant;
03018   // - If t == 1, then expr == a*j + b, where `j != v';
03019   // - If t == 2, the `expr' is of the general form.
03020   DB_Row<N>& dbm_0 = dbm[0];
03021 
03022   if (t == 0) {
03023     // Case 1: expr == b.
03024     switch (relsym) {
03025     case LESS_THAN_OR_EQUAL:
03026       // Add the constraint `var <= b/denominator'.
03027       add_dbm_constraint(0, v, b, denominator);
03028       break;
03029     case GREATER_THAN_OR_EQUAL:
03030       // Add the constraint `var >= b/denominator',
03031       // i.e., `-var <= -b/denominator',
03032       add_dbm_constraint(v, 0, -b, denominator);
03033       break;
03034     default:
03035       // We already dealt with the other cases.
03036       throw std::runtime_error("PPL internal error");
03037       break;
03038     }
03039   }
03040   else if (t == 1) {
03041     // Value of the one and only non-zero coefficient in `expr'.
03042     const Coefficient& expr_j = expr.coefficient(Variable(j-1));
03043     N d;
03044     switch (relsym) {
03045     case LESS_THAN_OR_EQUAL:
03046       div_round_up(d, b, denominator);
03047       // Note that: `j != v', so that `expr' is of the form
03048       // expr_j * j + b, with `j != v'.
03049       if (expr_j == denominator)
03050         // Add the new constraint `v - j <= b/denominator'.
03051         add_dbm_constraint(j, v, d);
03052       else {
03053         // Here expr_j != denominator, so that we should be adding
03054         // the constraint `v <= b/denominator - j'.
03055         N sum;
03056         // Approximate the homogeneous part of `expr'.
03057         const int sign_j = sgn(expr_j);
03058         const N& approx_j = (sign_j > 0) ? dbm_0[j] : dbm[j][0];
03059         if (!is_plus_infinity(approx_j)) {
03060           N coeff_j;
03061           if (sign_j > 0)
03062             assign_r(coeff_j, expr_j, ROUND_UP);
03063           else {
03064             TEMP_INTEGER(minus_expr_j);
03065             neg_assign(minus_expr_j, expr_j);
03066             assign_r(coeff_j, minus_expr_j, ROUND_UP);
03067           }
03068           add_mul_assign_r(sum, coeff_j, approx_j, ROUND_UP);
03069           add_dbm_constraint(0, v, sum);
03070         }
03071       }
03072       break;
03073 
03074     case GREATER_THAN_OR_EQUAL:
03075       div_round_up(d, -b, denominator);
03076       // Note that: `j != v', so that `expr' is of the form
03077       // expr_j * j + b, with `j != v'.
03078       if (expr_j == denominator)
03079         // Add the new constraint `v - j >= b/denominator'.
03080         add_dbm_constraint(j, v, d);
03081       else {
03082         // Here expr_j != denominator, so that we should be adding
03083         // the constraint `v <= b/denominator - j'.
03084         N sum;
03085         // Approximate the homogeneous part of `expr_j'.
03086         const int sign_j = sgn(expr_j);
03087         const N& approx_j = (sign_j > 0) ? dbm_0[j] : dbm[j][0];
03088         if (!is_plus_infinity(approx_j)) {
03089           N coeff_j;
03090           if (sign_j > 0)
03091             assign_r(coeff_j, expr_j, ROUND_UP);
03092           else {
03093             TEMP_INTEGER(minus_expr_j);
03094             neg_assign(minus_expr_j, expr_j);
03095             assign_r(coeff_j, minus_expr_j, ROUND_UP);
03096           }
03097           add_mul_assign_r(sum, coeff_j, approx_j, ROUND_UP);
03098           add_dbm_constraint(0, v, sum);
03099         }
03100       }
03101       break;
03102 
03103     default:
03104       // We already dealt with the other cases.
03105       throw std::runtime_error("PPL internal error");
03106       break;
03107     }
03108   }
03109   else {
03110     // Here t == 2, so that
03111     // expr == a_1*x_1 + a_2*x_2 + ... + a_n*x_n + b, where n >= 2.
03112     const bool is_sc = (denominator > 0);
03113     TEMP_INTEGER(minus_b);
03114     neg_assign(minus_b, b);
03115     const Coefficient& sc_b = is_sc ? b : minus_b;
03116     const Coefficient& minus_sc_b = is_sc ? minus_b : b;
03117     TEMP_INTEGER(minus_den);
03118     neg_assign(minus_den, denominator);
03119     const Coefficient& sc_den = is_sc ? denominator : minus_den;
03120     const Coefficient& minus_sc_den = is_sc ? minus_den : denominator;
03121     // NOTE: here, for optimization purposes, `minus_expr' is only assigned
03122     // when `denominator' is negative. Do not use it unless you are sure
03123     // it has been correctly assigned.
03124     Linear_Expression minus_expr;
03125     if (!is_sc)
03126       minus_expr = -expr;
03127     const Linear_Expression& sc_expr = is_sc ? expr : minus_expr;
03128 
03129     N sum;
03130     // Index of variable that is unbounded in `this->dbm'.
03131     // (The initialization is just to quiet a compiler warning.)
03132     dimension_type pinf_index = 0;
03133     // Number of unbounded variables found.
03134     dimension_type pinf_count = 0;
03135 
03136     switch (relsym) {
03137     case LESS_THAN_OR_EQUAL:
03138       // Compute an upper approximation for `expr' into `sum',
03139       // taking into account the sign of `denominator'.
03140 
03141       // Approximate the inhomogeneous term.
03142       assign_r(sum, sc_b, ROUND_UP);
03143 
03144       // Approximate the homogeneous part of `sc_expr'.
03145       // Note: indices above `w' can be disregarded, as they all have
03146       // a zero coefficient in `expr'.
03147       for (dimension_type i = j; i > 0; --i) {
03148         const Coefficient& sc_i = sc_expr.coefficient(Variable(i-1));
03149         const int sign_i = sgn(sc_i);
03150         if (sign_i == 0)
03151           continue;
03152         // Choose carefully: we are approximating `sc_expr'.
03153         const N& approx_i = (sign_i > 0) ? dbm_0[i] : dbm[i][0];
03154         if (is_plus_infinity(approx_i)) {
03155           if (++pinf_count > 1)
03156             break;
03157           pinf_index = i;
03158           continue;
03159         }
03160         N coeff_i;
03161         if (sign_i > 0)
03162           assign_r(coeff_i, sc_i, ROUND_UP);
03163         else {
03164           TEMP_INTEGER(minus_sc_i);
03165           neg_assign(minus_sc_i, sc_i);
03166           assign_r(coeff_i, minus_sc_i, ROUND_UP);
03167         }
03168         add_mul_assign_r(sum, coeff_i, approx_i, ROUND_UP);
03169       }
03170 
03171       // Divide by the (sign corrected) denominator (if needed).
03172       if (sc_den != 1) {
03173         // Before computing the quotient, the denominator should be
03174         // approximated towards zero. Since `sc_den' is known to be
03175         // positive, this amounts to rounding downwards, which is achieved
03176         // by rounding upwards `minus_sc-den' and negating again the result.
03177         N down_sc_den;
03178         assign_r(down_sc_den, minus_sc_den, ROUND_UP);
03179         neg_assign_r(down_sc_den, down_sc_den, ROUND_UP);
03180         div_assign_r(sum, sum, down_sc_den, ROUND_UP);
03181       }
03182 
03183       if (pinf_count == 0) {
03184         // Add the constraint `v <= sum'.
03185         add_dbm_constraint(0, v, sum);
03186         // Deduce constraints of the form `v - u', where `u != v'.
03187         deduce_v_minus_u_bounds(v, j, sc_expr, sc_den, sum);
03188       }
03189       else if (pinf_count == 1)
03190         if (expr.coefficient(Variable(pinf_index-1)) == denominator)
03191           // Add the constraint `v - pinf_index <= sum'.
03192           add_dbm_constraint(pinf_index, v, sum);
03193       break;
03194 
03195     case GREATER_THAN_OR_EQUAL:
03196       // Compute an upper approximation for `-sc_expr' into `sum'.
03197       // Note: approximating `-sc_expr' from above and then negating the
03198       // result is the same as approximating `sc_expr' from below.
03199 
03200       // Approximate the inhomogeneous term.
03201       assign_r(sum, minus_sc_b, ROUND_UP);
03202 
03203       // Approximate the homogeneous part of `-sc_expr'.
03204       for (dimension_type i = j; i > 0; --i) {
03205         const Coefficient& sc_i = sc_expr.coefficient(Variable(i-1));
03206         const int sign_i = sgn(sc_i);
03207         if (sign_i == 0)
03208           continue;
03209         // Choose carefully: we are approximating `-sc_expr'.
03210         const N& approx_i = (sign_i > 0) ? dbm[i][0] : dbm_0[i];
03211         if (is_plus_infinity(approx_i)) {
03212           if (++pinf_count > 1)
03213             break;
03214           pinf_index = i;
03215           continue;
03216         }
03217         N coeff_i;
03218         if (sign_i > 0)
03219           assign_r(coeff_i, sc_i, ROUND_UP);
03220         else {
03221           TEMP_INTEGER(minus_sc_i);
03222           neg_assign(minus_sc_i, sc_i);
03223           assign_r(coeff_i, minus_sc_i, ROUND_UP);
03224         }
03225         add_mul_assign_r(sum, coeff_i, approx_i, ROUND_UP);
03226       }
03227 
03228       // Divide by the (sign corrected) denominator (if needed).
03229       if (sc_den != 1) {
03230         // Before computing the quotient, the denominator should be
03231         // approximated towards zero. Since `sc_den' is known to be positive,
03232         // this amounts to rounding downwards, which is achieved by rounding
03233         // upwards `minus_sc_den' and negating again the result.
03234         N down_sc_den;
03235         assign_r(down_sc_den, minus_sc_den, ROUND_UP);
03236         neg_assign_r(down_sc_den, down_sc_den, ROUND_UP);
03237         div_assign_r(sum, sum, down_sc_den, ROUND_UP);
03238       }
03239 
03240       if (pinf_count == 0) {
03241         // Add the constraint `v >= -sum', i.e., `-v <= sum'.
03242         add_dbm_constraint(v, 0, sum);
03243         // Deduce constraints of the form `u - v', where `u != v'.
03244         deduce_u_minus_v_bounds(v, j, sc_expr, sc_den, sum);
03245       }
03246       else if (pinf_count == 1)
03247         if (pinf_index != v
03248             && expr.coefficient(Variable(pinf_index-1)) == denominator)
03249           // Add the constraint `v - pinf_index >= -sum',
03250           // i.e., `pinf_index - v <= sum'.
03251           add_dbm_constraint(v, pinf_index, sum);
03252       break;
03253 
03254     default:
03255       // We already dealt with the other cases.
03256       throw std::runtime_error("PPL internal error");
03257       break;
03258     }
03259   }
03260 
03261   // If the shrunk BD_Shape is empty, its preimage is empty too.
03262   if (is_empty())
03263     return;
03264   forget_all_dbm_constraints(v);
03265   // Shortest-path closure is preserved, but not reduction.
03266   if (marked_shortest_path_reduced())
03267     status.reset_shortest_path_reduced();
03268   assert(OK());
03269 }

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.

Definition at line 662 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::constraints(), Parma_Polyhedra_Library::BD_Shape< T >::OK(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::swap(), Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible(), and Parma_Polyhedra_Library::Polyhedron::time_elapse_assign().

00662                                                  {
00663   // Dimension-compatibility check.
00664   if (space_dimension() != y.space_dimension())
00665     throw_dimension_incompatible("time_elapse_assign(y)", y);
00666   // See the documentation for polyhedra.
00667   C_Polyhedron px(constraints());
00668   C_Polyhedron py(y.constraints());
00669   px.time_elapse_assign(py);
00670   BD_Shape x(px);
00671   swap(x);
00672   assert(OK());
00673 }

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.

Definition at line 619 of file BD_Shape.inlines.hh.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::CC76_extrapolation_assign(), and Parma_Polyhedra_Library::BD_Shape< T >::limited_CC76_extrapolation_assign().

00619                                                                       {
00620   static N stop_points[] = {
00621     N(-2, ROUND_UP),
00622     N(-1, ROUND_UP),
00623     N( 0, ROUND_UP),
00624     N( 1, ROUND_UP),
00625     N( 2, ROUND_UP)
00626   };
00627   CC76_extrapolation_assign(y,
00628                             stop_points,
00629                             stop_points
00630                             + sizeof(stop_points)/sizeof(stop_points[0]),
00631                             tp);
00632 }

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`
	)			`[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`.
	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.

Definition at line 1461 of file BD_Shape.templates.hh.

01463                                                      {
01464   const dimension_type space_dim = space_dimension();
01465 
01466   // Dimension-compatibility check.
01467   if (space_dim != y.space_dimension())
01468     throw_dimension_incompatible("CC76_extrapolation_assign(y)", y);
01469 
01470 #ifndef NDEBUG
01471   {
01472     // We assume that `y' is contained in or equal to `*this'.
01473     const BD_Shape x_copy = *this;
01474     const BD_Shape y_copy = y;
01475     assert(x_copy.contains(y_copy));
01476   }
01477 #endif
01478 
01479   // If both systems of bounded differences are zero-dimensional,
01480   // since `*this' contains `y', we simply return `*this'.
01481   if (space_dim == 0)
01482     return;
01483 
01484   shortest_path_closure_assign();
01485   // If `*this' is empty, since `*this' contains `y', `y' is empty too.
01486   if (marked_empty())
01487     return;
01488   y.shortest_path_closure_assign();
01489   // If `y' is empty, we return.
01490   if (y.marked_empty())
01491     return;
01492 
01493   // If there are tokens available, work on a temporary copy.
01494   if (tp != 0 && *tp > 0) {
01495     BD_Shape<T> x_tmp(*this);
01496     x_tmp.CC76_extrapolation_assign(y, first, last, 0);
01497     // If the widening was not precise, use one of the available tokens.
01498     if (!contains(x_tmp))
01499       --(*tp);
01500     return;
01501   }
01502 
01503   // Compare each constraint in `y' to the corresponding one in `*this'.
01504   // The constraint in `*this' is kept as is if it is stronger than or
01505   // equal to the constraint in `y'; otherwise, the inhomogeneous term
01506   // of the constraint in `*this' is further compared with elements taken
01507   // from a sorted container (the stop-points, provided by the user), and
01508   // is replaced by the first entry, if any, which is greater than or equal
01509   // to the inhomogeneous term. If no such entry exists, the constraint
01510   // is removed altogether.
01511   for (dimension_type i = space_dim + 1; i-- > 0; ) {
01512     DB_Row<N>& dbm_i = dbm[i];
01513     const DB_Row<N>& y_dbm_i = y.dbm[i];
01514     for (dimension_type j = space_dim + 1; j-- > 0; ) {
01515       N& dbm_ij = dbm_i[j];
01516       const N& y_dbm_ij = y_dbm_i[j];
01517       if (y_dbm_ij < dbm_ij) {
01518         Iterator k = std::lower_bound(first, last, dbm_ij);
01519         if (k != last) {
01520           if (dbm_ij < *k)
01521             assign_r(dbm_ij, *k, ROUND_UP);
01522         }
01523         else
01524           dbm_ij = PLUS_INFINITY;
01525       }
01526     }
01527   }
01528   status.reset_shortest_path_closed();
01529   assert(OK());
01530 }

template<typename T>

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

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.

Definition at line 1641 of file BD_Shape.templates.hh.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::BHMZ05_widening_assign(), and Parma_Polyhedra_Library::BD_Shape< T >::limited_BHMZ05_extrapolation_assign().

01641                                                                    {
01642   const dimension_type space_dim = space_dimension();
01643 
01644   // Dimension-compatibility check.
01645   if (space_dim != y.space_dimension())
01646     throw_dimension_incompatible("BHMZ05_widening_assign(y)", y);
01647 
01648 #ifndef NDEBUG
01649   {
01650     // We assume that `y' is contained in or equal to `*this'.
01651     const BD_Shape x_copy = *this;
01652     const BD_Shape y_copy = y;
01653     assert(x_copy.contains(y_copy));
01654   }
01655 #endif
01656 
01657   // Compute the affine dimension of `y'.
01658   const dimension_type y_affine_dim = y.affine_dimension();
01659   // If the affine dimension of `y' is zero, then either `y' is
01660   // zero-dimensional, or it is empty, or it is a singleton.
01661   // In all cases, due to the inclusion hypothesis, the result is `*this'.
01662   if (y_affine_dim == 0)
01663     return;
01664 
01665   // If the affine dimension has changed, due to the inclusion hypothesis,
01666   // the result is `*this'.
01667   const dimension_type x_affine_dim = affine_dimension();
01668   assert(x_affine_dim >= y_affine_dim);
01669   if (x_affine_dim != y_affine_dim)
01670     return;
01671 
01672   // If there are tokens available, work on a temporary copy.
01673   if (tp != 0 && *tp > 0) {
01674     BD_Shape<T> x_tmp(*this);
01675     x_tmp.BHMZ05_widening_assign(y, 0);
01676     // If the widening was not precise, use one of the available tokens.
01677     if (!contains(x_tmp))
01678       --(*tp);
01679     return;
01680   }
01681 
01682   // Here no token is available.
01683   assert(marked_shortest_path_closed() && y.marked_shortest_path_closed());
01684   // Minimize `y'.
01685   y.shortest_path_reduction_assign();
01686 
01687   // Extrapolate unstable bounds, taking into account redundancy in `y'.
01688   for (dimension_type i = space_dim + 1; i-- > 0; ) {
01689     DB_Row<N>& dbm_i = dbm[i];
01690     const DB_Row<N>& y_dbm_i = y.dbm[i];
01691     const std::deque<bool>& y_redundancy_i = y.redundancy_dbm[i];
01692     for (dimension_type j = space_dim + 1; j-- > 0; ) {
01693       N& dbm_ij = dbm_i[j];
01694       // Note: in the following line the use of `!=' (as opposed to
01695       // the use of `<' that would seem -but is not- equivalent) is
01696       // intentional.
01697       if (y_redundancy_i[j] || y_dbm_i[j] != dbm_ij)
01698         dbm_ij = PLUS_INFINITY;
01699     }
01700   }
01701   // NOTE: this will also reset the shortest-path reduction flag,
01702   // even though the dbm is still in reduced form. However, the
01703   // current implementation invariant requires that any reduced dbm
01704   // is closed too.
01705   status.reset_shortest_path_closed();
01706   assert(OK());
01707 }

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`
	)			`[inline]`

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.

Definition at line 1711 of file BD_Shape.templates.hh.

01713                                                                {
01714   // Dimension-compatibility check.
01715   const dimension_type space_dim = space_dimension();
01716   if (space_dim != y.space_dimension())
01717     throw_dimension_incompatible("limited_BHMZ05_extrapolation_assign(y, cs)",
01718                                  y);
01719   // `cs' must be dimension-compatible with the two systems
01720   // of bounded differences.
01721   const dimension_type cs_space_dim = cs.space_dimension();
01722   if (space_dim < cs_space_dim)
01723     throw_constraint_incompatible("limited_BHMZ05_extrapolation_assign"
01724                                   "(y, cs)");
01725 
01726   // Strict inequalities are not allowed.
01727   if (cs.has_strict_inequalities())
01728     throw_constraint_incompatible("limited_BHMZ05_extrapolation_assign"
01729                                   "(y, cs)");
01730 
01731   // The limited BHMZ05-extrapolation between two systems of bounded
01732   // differences in a zero-dimensional space is a system of bounded
01733   // differences in a zero-dimensional space, too.
01734   if (space_dim == 0)
01735     return;
01736 
01737 #ifndef NDEBUG
01738   {
01739     // We assume that `y' is contained in or equal to `*this'.
01740     const BD_Shape x_copy = *this;
01741     const BD_Shape y_copy = y;
01742     assert(x_copy.contains(y_copy));
01743   }
01744 #endif
01745 
01746   // If `*this' is empty, since `*this' contains `y', `y' is empty too.
01747   if (marked_empty())
01748     return;
01749   // If `y' is empty, we return.
01750   if (y.marked_empty())
01751     return;
01752 
01753   BD_Shape<T> limiting_shape(space_dim, UNIVERSE);
01754   get_limiting_shape(cs, limiting_shape);
01755   BHMZ05_widening_assign(y, tp);
01756   intersection_assign(limiting_shape);
01757   assert(OK());
01758 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::CC76_narrowing_assign ( const BD_Shape< T > & y ) [inline]

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}$ .

Definition at line 1762 of file BD_Shape.templates.hh.

01762                                                     {
01763   const dimension_type space_dim = space_dimension();
01764 
01765   // Dimension-compatibility check.
01766   if (space_dim != y.space_dimension())
01767     throw_dimension_incompatible("CC76_narrowing_assign(y)", y);
01768 
01769 #ifndef NDEBUG
01770   {
01771     // We assume that `*this' is contained in or equal to `y'.
01772     const BD_Shape x_copy = *this;
01773     const BD_Shape y_copy = y;
01774     assert(y_copy.contains(x_copy));
01775   }
01776 #endif
01777 
01778   // If both systems of bounded differences are zero-dimensional,
01779   // since `y' contains `*this', we simply return `*this'.
01780   if (space_dim == 0)
01781     return;
01782 
01783   y.shortest_path_closure_assign();
01784   // If `y' is empty, since `y' contains `this', `*this' is empty too.
01785   if (y.marked_empty())
01786     return;
01787   shortest_path_closure_assign();
01788   // If `*this' is empty, we return.
01789   if (marked_empty())
01790     return;
01791 
01792   // Replace each constraint in `*this' by the corresponding constraint
01793   // in `y' if the corresponding inhomogeneous terms are both finite.
01794   bool changed = false;
01795   for (dimension_type i = space_dim + 1; i-- > 0; ) {
01796     DB_Row<N>& dbm_i = dbm[i];
01797     const DB_Row<N>& y_dbm_i = y.dbm[i];
01798     for (dimension_type j = space_dim + 1; j-- > 0; ) {
01799       N& dbm_ij = dbm_i[j];
01800       const N& y_dbm_ij = y_dbm_i[j];
01801       if (!is_plus_infinity(dbm_ij)
01802           && !is_plus_infinity(y_dbm_ij)
01803           && dbm_ij != y_dbm_ij) {
01804         dbm_ij = y_dbm_ij;
01805         changed = true;
01806       }
01807     }
01808   }
01809   if (changed && marked_shortest_path_closed())
01810     status.reset_shortest_path_closed();
01811   assert(OK());
01812 }

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`
	)			`[inline]`

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.

Definition at line 1591 of file BD_Shape.templates.hh.

01593                                                              {
01594   // Dimension-compatibility check.
01595   const dimension_type space_dim = space_dimension();
01596   if (space_dim != y.space_dimension())
01597     throw_dimension_incompatible("limited_CC76_extrapolation_assign(y, cs)",
01598                                  y);
01599 
01600   // `cs' must be dimension-compatible with the two systems
01601   // of bounded differences.
01602   const dimension_type cs_space_dim = cs.space_dimension();
01603   if (space_dim < cs_space_dim)
01604     throw_constraint_incompatible("limited_CC76_extrapolation_assign(y, cs)");
01605 
01606   // Strict inequalities not allowed.
01607   if (cs.has_strict_inequalities())
01608     throw_constraint_incompatible("limited_CC76_extrapolation_assign(y, cs)");
01609 
01610   // The limited CC76-extrapolation between two systems of bounded
01611   // differences in a zero-dimensional space is a system of bounded
01612   // differences in a zero-dimensional space, too.
01613   if (space_dim == 0)
01614     return;
01615 
01616 #ifndef NDEBUG
01617   {
01618     // We assume that `y' is contained in or equal to `*this'.
01619     const BD_Shape x_copy = *this;
01620     const BD_Shape y_copy = y;
01621     assert(x_copy.contains(y_copy));
01622   }
01623 #endif
01624 
01625   // If `*this' is empty, since `*this' contains `y', `y' is empty too.
01626   if (marked_empty())
01627     return;
01628   // If `y' is empty, we return.
01629   if (y.marked_empty())
01630     return;
01631 
01632   BD_Shape<T> limiting_shape(space_dim, UNIVERSE);
01633   get_limiting_shape(cs, limiting_shape);
01634   CC76_extrapolation_assign(y, tp);
01635   intersection_assign(limiting_shape);
01636   assert(OK());
01637 }

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.

Definition at line 636 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::constraints(), Parma_Polyhedra_Library::Polyhedron::H79_widening_assign(), Parma_Polyhedra_Library::BD_Shape< T >::OK(), and Parma_Polyhedra_Library::BD_Shape< T >::swap().

00636                                                                 {
00637   // See the documentation for polyhedra.
00638   C_Polyhedron px(constraints());
00639   C_Polyhedron py(y.constraints());
00640   px.H79_widening_assign(py, tp);
00641   BD_Shape x(px);
00642   swap(x);
00643   assert(OK());
00644 }

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.

Definition at line 648 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::constraints(), Parma_Polyhedra_Library::Polyhedron::limited_H79_extrapolation_assign(), Parma_Polyhedra_Library::BD_Shape< T >::OK(), and Parma_Polyhedra_Library::BD_Shape< T >::swap().

00650                                                             {
00651   // See the documentation for polyhedra.
00652   C_Polyhedron px(constraints());
00653   C_Polyhedron py(y.constraints());
00654   px.limited_H79_extrapolation_assign(py, cs, tp);
00655   BD_Shape x(px);
00656   swap(x);
00657   assert(OK());
00658 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::add_space_dimensions_and_embed ( dimension_type m ) [inline]

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\}.$

Definition at line 1192 of file BD_Shape.templates.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), Parma_Polyhedra_Library::BD_Shape< T >::marked_shortest_path_reduced(), Parma_Polyhedra_Library::BD_Shape< T >::OK(), Parma_Polyhedra_Library::BD_Shape< T >::Status::reset_shortest_path_reduced(), Parma_Polyhedra_Library::BD_Shape< T >::Status::set_shortest_path_closed(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), and Parma_Polyhedra_Library::BD_Shape< T >::status.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::concatenate_assign(), and Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_image().

01192                                                                   {
01193   // Adding no dimensions is a no-op.
01194   if (m == 0)
01195     return;
01196 
01197   const dimension_type space_dim = space_dimension();
01198   const dimension_type new_space_dim = space_dim + m;
01199   const bool was_zero_dim_univ = (!marked_empty() && space_dim == 0);
01200 
01201   // To embed an n-dimension space BDS in a (n+m)-dimension space,
01202   // we just add `m' rows and columns in the system of bounded differences,
01203   // initialized to PLUS_INFINITY.
01204   dbm.grow(new_space_dim + 1);
01205 
01206   // Shortest-path closure is maintained (if it was holding).
01207   // TODO: see whether reduction can be (efficiently!) maintained too.
01208   if (marked_shortest_path_reduced())
01209     status.reset_shortest_path_reduced();
01210 
01211   // If `*this' was the zero-dim space universe BDS,
01212   // the we can set the shortest-path closure flag.
01213   if (was_zero_dim_univ)
01214     status.set_shortest_path_closed();
01215 
01216   assert(OK());
01217 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::add_space_dimensions_and_project ( dimension_type m ) [inline]

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\}.$

Definition at line 1221 of file BD_Shape.templates.hh.

01221                                                                     {
01222   // Adding no dimensions is a no-op.
01223   if (m == 0)
01224     return;
01225 
01226   const dimension_type space_dim = space_dimension();
01227 
01228   // If `*this' was zero-dimensional, then we add `m' rows and columns.
01229   // If it also was non-empty, then we zero all the added elements
01230   // and set the flag for shortest-path closure.
01231   if (space_dim == 0) {
01232     dbm.grow(m + 1);
01233     if (!marked_empty()) {
01234       for (dimension_type i = m + 1; i-- > 0; ) {
01235         DB_Row<N>& dbm_i = dbm[i];
01236         for (dimension_type j = m + 1; j-- > 0; )
01237           if (i != j)
01238             assign_r(dbm_i[j], 0, ROUND_NOT_NEEDED);
01239       }
01240       status.set_shortest_path_closed();
01241     }
01242     assert(OK());
01243     return;
01244   }
01245 
01246   // To project an n-dimension space system of bounded differences
01247   // in a (n+m)-dimension space, we add `m' rows and columns.
01248   // In the first row and column of the matrix we add `zero' from
01249   // the (n+1)-th position to the end.
01250   const dimension_type new_space_dim = space_dim + m;
01251   dbm.grow(new_space_dim + 1);
01252 
01253   // Bottom of the matrix and first row.
01254   DB_Row<N>& dbm_0 = dbm[0];
01255   for (dimension_type i = space_dim + 1; i <= new_space_dim; ++i) {
01256     assign_r(dbm[i][0], 0, ROUND_NOT_NEEDED);
01257     assign_r(dbm_0[i], 0, ROUND_NOT_NEEDED);
01258   }
01259 
01260   if (marked_shortest_path_closed())
01261     status.reset_shortest_path_closed();
01262   assert(OK());
01263 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::concatenate_assign ( const BD_Shape< T > & y ) [inline]

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.

Definition at line 347 of file BD_Shape.templates.hh.

00347                                                  {
00348   BD_Shape& x = *this;
00349 
00350   const dimension_type x_space_dim = x.space_dimension();
00351   const dimension_type y_space_dim = y.space_dimension();
00352 
00353   // If `y' is an empty 0-dim space system of bounded differences,
00354   // let `*this' become empty.
00355   if (y_space_dim == 0 && y.marked_empty()) {
00356     set_empty();
00357     assert(OK());
00358     return;
00359   }
00360 
00361   // If `x' is an empty 0-dim space BDS, then it is sufficient to adjust
00362   // the dimension of the vector space.
00363   if (x_space_dim == 0 && marked_empty()) {
00364     dbm.grow(y_space_dim + 1);
00365     assert(OK());
00366     return;
00367   }
00368   // First we increase the space dimension of `x' by adding
00369   // `y.space_dimension()' new dimensions.
00370   // The matrix for the new system of constraints is obtained
00371   // by leaving the old system of constraints in the upper left-hand side
00372   // and placing the constraints of `y' in the lower right-hand side,
00373   // except the constraints as `y(i) >= cost' or `y(i) <= cost', that are
00374   // placed in the right position on the new matrix.
00375   add_space_dimensions_and_embed(y_space_dim);
00376   const dimension_type new_space_dim = x_space_dim + y_space_dim;
00377   for (dimension_type i = x_space_dim + 1; i <= new_space_dim; ++i) {
00378     DB_Row<N>& dbm_i = dbm[i];
00379     dbm_i[0] = y.dbm[i - x_space_dim][0];
00380     dbm[0][i] = y.dbm[0][i - x_space_dim];
00381     for (dimension_type j = x_space_dim + 1; j <= new_space_dim; ++j)
00382       dbm_i[j] = y.dbm[i - x_space_dim][j - x_space_dim];
00383   }
00384 
00385   if (marked_shortest_path_closed())
00386     status.reset_shortest_path_closed();
00387   assert(OK());
00388 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::remove_space_dimensions ( const Variables_Set & to_be_removed ) [inline]

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.

Definition at line 1267 of file BD_Shape.templates.hh.

01267                                                                        {
01268   // The removal of no dimensions from any BDS is a no-op.
01269   // Note that this case also captures the only legal removal of
01270   // space dimensions from a BDS in a 0-dim space.
01271   if (to_be_removed.empty()) {
01272     assert(OK());
01273     return;
01274   }
01275 
01276   // Dimension-compatibility check: the variable having
01277   // maximum cardinality is the one occurring last in the set.
01278   const dimension_type max_dim_to_be_removed = to_be_removed.rbegin()->id();
01279   const dimension_type old_space_dim = space_dimension();
01280   if (max_dim_to_be_removed >= old_space_dim)
01281     throw_dimension_incompatible("remove_space_dimensions(vs)",
01282                                  max_dim_to_be_removed);
01283 
01284   // Shortest-path closure is necessary to keep precision.
01285   shortest_path_closure_assign();
01286 
01287   // When removing _all_ dimensions from a BDS,
01288   // we obtain the zero-dimensional BDS.
01289   const dimension_type new_space_dim = old_space_dim - to_be_removed.size();
01290   if (new_space_dim == 0) {
01291     dbm.resize_no_copy(1);
01292     if (!marked_empty())
01293       // We set the zero_dim_univ flag.
01294       set_zero_dim_univ();
01295     assert(OK());
01296     return;
01297   }
01298 
01299   // Shortest-path closure is maintained.
01300   // TODO: see whether reduction can be (efficiently!) maintained too.
01301   if (marked_shortest_path_reduced())
01302     status.reset_shortest_path_reduced();
01303 
01304   // For each variable to remove, we erase the corresponding column and
01305   // row by shifting the other columns and rows, than are not removed,
01306   // respectively left and above.
01307   Variables_Set::const_iterator tbr = to_be_removed.begin();
01308   Variables_Set::const_iterator tbr_end = to_be_removed.end();
01309   dimension_type dst = tbr->id() + 1;
01310   dimension_type src = dst + 1;
01311   for (++tbr; tbr != tbr_end; ++tbr) {
01312     const dimension_type tbr_next = tbr->id() + 1;
01313     // All other columns and rows are moved respectively to the left
01314     // and above.
01315     while (src < tbr_next) {
01316       dbm[dst] = dbm[src];
01317       for (dimension_type i = old_space_dim + 1; i-- > 0; ) {
01318         DB_Row<N>& dbm_i = dbm[i];
01319         dbm_i[dst] = dbm_i[src];
01320       }
01321       ++dst;
01322       ++src;
01323     }
01324     ++src;
01325   }
01326 
01327   // Moving the remaining rows and columns.
01328   while (src <= old_space_dim) {
01329     dbm[dst] = dbm[src];
01330     for (dimension_type i = old_space_dim + 1; i-- > 0; ) {
01331       DB_Row<N>& dbm_i = dbm[i];
01332       dbm_i[dst] = dbm_i[src];
01333     }
01334     ++src;
01335     ++dst;
01336   }
01337 
01338   // Update the space dimension.
01339   dbm.resize_no_copy(new_space_dim + 1);
01340   assert(OK());
01341 }

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.

Definition at line 578 of file BD_Shape.inlines.hh.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_image(), and Parma_Polyhedra_Library::BD_Shape< T >::map_space_dimensions().

00578                                                                         {
00579   // Dimension-compatibility check: the variable having
00580   // maximum index is the one occurring last in the set.
00581   if (new_dim > space_dimension())
00582     throw_dimension_incompatible("remove_higher_space_dimensions(nd)",
00583                                  new_dim);
00584 
00585   // The removal of no dimensions from any BDS is a no-op.
00586   // Note that this case also captures the only legal removal of
00587   // dimensions from a zero-dim space BDS.
00588   if (new_dim == space_dimension()) {
00589     assert(OK());
00590     return;
00591   }
00592 
00593   // Shortest-path closure is necessary as in remove_space_dimensions().
00594   shortest_path_closure_assign();
00595   dbm.resize_no_copy(new_dim + 1);
00596 
00597   // Shortest-path closure is maintained.
00598   // TODO: see whether or not reduction can be (efficiently!) maintained too.
00599   if (marked_shortest_path_reduced())
00600     status.reset_shortest_path_reduced();
00601 
00602   // If we removed _all_ dimensions from a non-empty BDS,
00603   // the zero-dim universe BDS has been obtained.
00604   if (new_dim == 0 && !marked_empty())
00605     set_zero_dim_univ();
00606   assert(OK());
00607 }

template<typename T>

template<typename PartialFunction>

void Parma_Polyhedra_Library::BD_Shape< T >::map_space_dimensions ( const PartialFunction & pfunc ) [inline]

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

be the represented function and $k$

be the value of i. If $f$

is defined in $k$

, then

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.

Definition at line 1346 of file BD_Shape.templates.hh.

01346                                                               {
01347   const dimension_type space_dim = space_dimension();
01348   // TODO: this implementation is just an executable specification.
01349   if (space_dim == 0)
01350     return;
01351 
01352   if (pfunc.has_empty_codomain()) {
01353     // All dimensions vanish: the BDS becomes zero_dimensional.
01354     remove_higher_space_dimensions(0);
01355     assert(OK());
01356     return;
01357   }
01358 
01359   const dimension_type new_space_dim = pfunc.max_in_codomain() + 1;
01360   // If we are going to actually reduce the space dimension,
01361   // then shortest-path closure is required to keep precision.
01362   if (new_space_dim < space_dim)
01363     shortest_path_closure_assign();
01364 
01365   // If the BDS is empty, then it is sufficient to adjust the
01366   // space dimension of the system of bounded differences.
01367   if (marked_empty()) {
01368     remove_higher_space_dimensions(new_space_dim);
01369     return;
01370   }
01371 
01372   // Shortest-path closure is maintained (if it was holding).
01373   // TODO: see whether reduction can be (efficiently!) maintained too.
01374   if (marked_shortest_path_reduced())
01375     status.reset_shortest_path_reduced();
01376 
01377   // We create a new matrix with the new space dimension.
01378   DB_Matrix<N> x(new_space_dim+1);
01379   // First of all we must map the unary constraints, because
01380   // there is the fictitious variable `zero', that can't be mapped
01381   // at all.
01382   const DB_Row<N>& dbm_0 = dbm[0];
01383   DB_Row<N>& x_0 = x[0];
01384   for (dimension_type j = 1; j <= space_dim; ++j) {
01385     dimension_type new_j;
01386     if (pfunc.maps(j - 1, new_j)) {
01387       x_0[new_j + 1] = dbm_0[j];
01388       x[new_j + 1][0] = dbm[j][0];
01389     }
01390   }
01391   // Now we map the binary constraints, exchanging the indexes.
01392   for (dimension_type i = 1; i <= space_dim; ++i) {
01393     dimension_type new_i;
01394     if (pfunc.maps(i - 1, new_i)) {
01395       const DB_Row<N>& dbm_i = dbm[i];
01396       ++new_i;
01397       DB_Row<N>& x_new_i = x[new_i];
01398       for (dimension_type j = i+1; j <= space_dim; ++j) {
01399         dimension_type new_j;
01400         if (pfunc.maps(j - 1, new_j)) {
01401           ++new_j;
01402           x_new_i[new_j] = dbm_i[j];
01403           x[new_j][new_i] = dbm[j][i];
01404         }
01405       }
01406     }
01407   }
01408 
01409   std::swap(dbm, x);
01410   assert(OK());
01411 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::ascii_dump ( ) const

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

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::ascii_dump ( std::ostream & s ) const [inline]

Writes to s an ASCII representation of *this.

Definition at line 3552 of file BD_Shape.templates.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::Status::ascii_dump(), Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::BD_Shape< T >::redundancy_dbm, and Parma_Polyhedra_Library::BD_Shape< T >::status.

03552                                            {
03553   status.ascii_dump(s);
03554   s << "\n";
03555   dbm.ascii_dump(s);
03556   // Redundancy info.
03557   s << "\n";
03558   const char separator = ' ';
03559   const dimension_type nrows = redundancy_dbm.size();
03560   s << nrows << separator << "\n";
03561   for (dimension_type i = 0; i < nrows;  ++i) {
03562     for (dimension_type j = 0; j < nrows; ++j)
03563       s << redundancy_dbm[i][j] << separator;
03564     s << "\n";
03565   }
03566 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::print ( ) const

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

template<typename T>

bool Parma_Polyhedra_Library::BD_Shape< T >::ascii_load ( std::istream & s ) [inline]

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

Definition at line 3572 of file BD_Shape.templates.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::Status::ascii_load(), Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::BD_Shape< T >::redundancy_dbm, and Parma_Polyhedra_Library::BD_Shape< T >::status.

03572                                      {
03573   if (!status.ascii_load(s))
03574     return false;
03575   if (!dbm.ascii_load(s))
03576     return false;
03577   // Load redundancy info.
03578   dimension_type nrows;
03579    if (!(s >> nrows))
03580     return false;
03581   redundancy_dbm.clear();
03582   redundancy_dbm.reserve(nrows);
03583   std::deque<bool> redundancy_row(nrows, false);
03584   for (dimension_type i = 0; i < nrows;  ++i) {
03585     for (dimension_type j = 0; j < nrows; ++j)
03586       if (!(s >> redundancy_row[j]))
03587         return false;
03588     redundancy_dbm.push_back(redundancy_row);
03589   }
03590   return true;
03591 }

template<typename T>

bool Parma_Polyhedra_Library::BD_Shape< T >::marked_empty ( ) const [inline, private]

Returns true if the BDS is known to be empty.

The return value false does not necessarily implies that *this is non-empty.

Definition at line 112 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::status, and Parma_Polyhedra_Library::BD_Shape< T >::Status::test_empty().

00112                                 {
00113   return status.test_empty();
00114 }

template<typename T>

bool Parma_Polyhedra_Library::BD_Shape< T >::marked_shortest_path_closed ( ) const [inline, private]

Returns true if the system of bounded differences is known to be shortest-path closed.

The return value false does not necessarily implies that this->dbm is not shortest-path closed.

Definition at line 132 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::status, and Parma_Polyhedra_Library::BD_Shape< T >::Status::test_shortest_path_closed().

00132                                                {
00133   return status.test_shortest_path_closed();
00134 }

template<typename T>

bool Parma_Polyhedra_Library::BD_Shape< T >::marked_shortest_path_reduced ( ) const [inline, private]

Returns true if the system of bounded differences is known to be shortest-path reduced.

The return value false does not necessarily implies that this->dbm is not shortest-path reduced.

Definition at line 138 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::status, and Parma_Polyhedra_Library::BD_Shape< T >::Status::test_shortest_path_reduced().

00138                                                 {
00139   return status.test_shortest_path_reduced();
00140 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::set_empty ( ) [inline, private]

Turns *this into an empty BDS.

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

References Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), Parma_Polyhedra_Library::BD_Shape< T >::OK(), Parma_Polyhedra_Library::BD_Shape< T >::Status::set_empty(), and Parma_Polyhedra_Library::BD_Shape< T >::status.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::add_constraint(), Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape(), Parma_Polyhedra_Library::BD_Shape< T >::bds_difference_assign(), Parma_Polyhedra_Library::BD_Shape< T >::concatenate_assign(), and Parma_Polyhedra_Library::BD_Shape< T >::intersection_assign().

00118                        {
00119   status.set_empty();
00120   assert(OK());
00121   assert(marked_empty());
00122 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::set_zero_dim_univ ( ) [inline, private]

Turns *this into an zero-dimensional universe BDS.

Definition at line 126 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::Status::set_zero_dim_univ(), and Parma_Polyhedra_Library::BD_Shape< T >::status.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape(), Parma_Polyhedra_Library::BD_Shape< T >::remove_higher_space_dimensions(), and Parma_Polyhedra_Library::BD_Shape< T >::remove_space_dimensions().

00126                                {
00127   status.set_zero_dim_univ();
00128 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign ( ) const [inline, private]

Assigns to this->dbm its shortest-path closure.

Definition at line 933 of file BD_Shape.templates.hh.

00933                                                 {
00934   using Implementation::BD_Shapes::min_assign;
00935 
00936   // Do something only if necessary.
00937   if (marked_empty() || marked_shortest_path_closed())
00938     return;
00939   const dimension_type num_dimensions = space_dimension();
00940   // Zero-dimensional BDSs are necessarily shortest-path closed.
00941   if (num_dimensions == 0)
00942     return;
00943 
00944   // Even though the BDS will not change, its internal representation
00945   // is going to be modified by the Floyd-Warshall algorithm.
00946   BD_Shape& x = const_cast<BD_Shape<T>&>(*this);
00947 
00948   // Fill the main diagonal with zeros.
00949   for (dimension_type h = num_dimensions + 1; h-- > 0; ) {
00950     assert(is_plus_infinity(x.dbm[h][h]));
00951     assign_r(x.dbm[h][h], 0, ROUND_NOT_NEEDED);
00952   }
00953 
00954   N sum;
00955   for (dimension_type k = num_dimensions + 1; k-- > 0; ) {
00956     const DB_Row<N>& xdbm_k = x.dbm[k];
00957     for (dimension_type i = num_dimensions + 1; i-- > 0; ) {
00958       DB_Row<N>& xdbm_i = x.dbm[i];
00959       const N& xdbm_i_k = xdbm_i[k];
00960       if (!is_plus_infinity(xdbm_i_k))
00961         for (dimension_type j = num_dimensions + 1; j-- > 0; ) {
00962           const N& xdbm_k_j = xdbm_k[j];
00963           if (!is_plus_infinity(xdbm_k_j)) {
00964             // Rounding upward for correctness.
00965             add_assign_r(sum, xdbm_i_k, xdbm_k_j, ROUND_UP);
00966             min_assign(xdbm_i[j], sum);
00967           }
00968         }
00969     }
00970   }
00971 
00972   // Check for emptyness: the BDS is empty if and only if there is a
00973   // negative value on the main diagonal of `dbm'.
00974   for (dimension_type h = num_dimensions + 1; h-- > 0; ) {
00975     N& x_dbm_hh = x.dbm[h][h];
00976     if (x_dbm_hh < 0) {
00977       x.status.set_empty();
00978       return;
00979     }
00980     else {
00981       assert(x_dbm_hh == 0);
00982       // Restore PLUS_INFINITY on the main diagonal.
00983       x_dbm_hh = PLUS_INFINITY;
00984     }
00985   }
00986 
00987   // The BDS is not empty and it is now shortest-path closed.
00988   x.status.set_shortest_path_closed();
00989 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_reduction_assign ( ) const [inline, private]

Assigns to this->dbm its shortest-path closure and records into this->redundancy_dbm which of the entries in this->dbm are redundant.

Definition at line 993 of file BD_Shape.templates.hh.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::BHMZ05_widening_assign(), Parma_Polyhedra_Library::BD_Shape< T >::minimized_constraints(), and Parma_Polyhedra_Library::BD_Shape< T >::OK().

00993                                                   {
00994   // Do something only if necessary.
00995   if (marked_shortest_path_reduced())
00996     return;
00997 
00998   // First find the tighest constraints for this BDS.
00999   shortest_path_closure_assign();
01000 
01001   // If `*this' is empty, then there is nothing to reduce.
01002   if (marked_empty())
01003     return;
01004 
01005   // Step 1: compute zero-equivalence classes.
01006   // Variables corresponding to indices `i' and `j' are zero-equivalent
01007   // if they lie on a zero-weight loop; since the matrix is shortest-path
01008   // closed, this happens if and only if dbm[i][j] == -dbm[j][i].
01009   std::vector<dimension_type> predecessor;
01010   compute_predecessors(predecessor);
01011   std::vector<dimension_type> leaders;
01012   compute_leader_indices(predecessor, leaders);
01013   const dimension_type num_leaders = leaders.size();
01014 
01015   const dimension_type space_dim = space_dimension();
01016   // TODO: directly work on `redundancy_dbm' so as to minimize allocations.
01017   std::deque<bool> redundancy_row(space_dim + 1, true);
01018   std::vector<std::deque<bool> > redundancy(space_dim + 1, redundancy_row);
01019 
01020   // Step 2: flag non-redundant constraints in the (zero-cycle-free)
01021   // subsystem of bounded differences having only leaders as variables.
01022   N c;
01023   for (dimension_type l_i = 0; l_i < num_leaders; ++l_i) {
01024     const dimension_type i = leaders[l_i];
01025     const DB_Row<N>& dbm_i = dbm[i];
01026     std::deque<bool>& redundancy_i = redundancy[i];
01027     for (dimension_type l_j = 0; l_j < num_leaders; ++l_j) {
01028       const dimension_type j = leaders[l_j];
01029       if (redundancy_i[j]) {
01030         const N& dbm_i_j = dbm_i[j];
01031         redundancy_i[j] = false;
01032         for (dimension_type l_k = 0; l_k < num_leaders; ++l_k) {
01033           const dimension_type k = leaders[l_k];
01034           add_assign_r(c, dbm_i[k], dbm[k][j], ROUND_UP);
01035           if (dbm_i_j >= c) {
01036             redundancy_i[j] = true;
01037             break;
01038           }
01039         }
01040       }
01041     }
01042   }
01043 
01044   // Step 3: flag non-redundant constraints in zero-equivalence classes.
01045   // Each equivalence class must have a single 0-cycle connecting
01046   // all the equivalent variables in increasing order.
01047   std::deque<bool> dealt_with(space_dim + 1, false);
01048   for (dimension_type i = space_dim + 1; i-- > 0; )
01049     // We only need to deal with non-singleton zero-equivalence classes
01050     // that haven't already been dealt with.
01051     if (i != predecessor[i] && !dealt_with[i]) {
01052       dimension_type j = i;
01053       while (true) {
01054         const dimension_type pred_j = predecessor[j];
01055         if (j == pred_j) {
01056           // We finally found the leader of `i'.
01057           assert(redundancy[i][j]);
01058           redundancy[i][j] = false;
01059           // Here we dealt with `j' (i.e., `pred_j'), but it is useless
01060           // to update `dealt_with' because `j' is a leader.
01061           break;
01062         }
01063         // We haven't found the leader of `i' yet.
01064         assert(redundancy[pred_j][j]);
01065         redundancy[pred_j][j] = false;
01066         dealt_with[pred_j] = true;
01067         j = pred_j;
01068       }
01069     }
01070 
01071   // Even though shortest-path reduction is not going to change the BDS,
01072   // it might change its internal representation.
01073   BD_Shape<T>& x = const_cast<BD_Shape<T>&>(*this);
01074   std::swap(x.redundancy_dbm, redundancy);
01075   x.status.set_shortest_path_reduced();
01076 
01077   assert(is_shortest_path_reduced());
01078 }

template<typename T>

bool Parma_Polyhedra_Library::BD_Shape< T >::is_shortest_path_reduced ( ) const [inline, private]

Returns true if and only if this->dbm is shortest-path closed and this->redundancy_dbm correctly flags the redundant entries in this->dbm.

Definition at line 527 of file BD_Shape.templates.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::is_plus_infinity(), Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), Parma_Polyhedra_Library::BD_Shape< T >::marked_shortest_path_reduced(), Parma_Polyhedra_Library::BD_Shape< T >::redundancy_dbm, Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign(), and Parma_Polyhedra_Library::BD_Shape< T >::space_dimension().

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_reduction_assign().

00527                                             {
00528   // If the BDS is empty, it is also reduced.
00529   if (marked_empty())
00530     return true;
00531 
00532   // A shortest-path reduced dbm is just a dbm with an indication of
00533   // those constraints that are redundant. If there is no indication
00534   // of the redundant constraints, then it cannot be reduced.
00535   if (!marked_shortest_path_reduced())
00536     return false;
00537 
00538   const BD_Shape x_copy = *this;
00539   const dimension_type x_space_dim = x_copy.space_dimension();
00540   x_copy.shortest_path_closure_assign();
00541   // If we just discovered emptyness, it cannot be reduced.
00542   if (x_copy.marked_empty())
00543     return false;
00544 
00545   // The vector `leader' is used to indicate which variables are equivalent.
00546   std::vector<dimension_type> leader(x_space_dim + 1);
00547 
00548   // We store the leader.
00549   for (dimension_type i = x_space_dim + 1; i-- > 0; )
00550     leader[i] = i;
00551 
00552   // Step 1: we store really the leader with the corrected value.
00553   // We search for the equivalent or zero-equivalent variables.
00554   // The variable(i-1) and variable(j-1) are equivalent if and only if
00555   // m_i_j == -(m_j_i).
00556   for (dimension_type i = 0; i < x_space_dim; ++i) {
00557     const DB_Row<N>& xdbm_i = x_copy.dbm[i];
00558     for (dimension_type j = i + 1; j <= x_space_dim; ++j) {
00559       N negated_xdbm_ji;
00560       if (neg_assign_r(negated_xdbm_ji, x_copy.dbm[j][i],
00561                        ROUND_NOT_NEEDED) == V_EQ
00562           && negated_xdbm_ji == xdbm_i[j])
00563         // Two equivalent variables have got the same leader
00564         // (the smaller variable).
00565         leader[j] = leader[i];
00566     }
00567   }
00568 
00569   // Step 2: we check if there are redundant constraints in the zero_cycle
00570   // free systems of bounded differences, considering only the leaders.
00571   // A constraint `c' is redundant, when there are two constraints such that
00572   // their sum is the same constraint with the inhomogeneous term
00573   // less than or equal to the `c' one.
00574   N c;
00575   for (dimension_type k = 0; k <= x_space_dim; ++k)
00576     if (leader[k] == k) {
00577       const DB_Row<N>& x_k = x_copy.dbm[k];
00578       for (dimension_type i = 0; i <= x_space_dim; ++i)
00579         if (leader[i] == i) {
00580           const DB_Row<N>& x_i = x_copy.dbm[i];
00581           const std::deque<bool>& redundancy_i = redundancy_dbm[i];
00582           const N& x_i_k = x_i[k];
00583           for (dimension_type j = 0; j <= x_space_dim; ++j)
00584             if (leader[j] == j) {
00585               const N& x_i_j = x_i[j];
00586               if (!is_plus_infinity(x_i_j)) {
00587                 add_assign_r(c, x_i_k, x_k[j], ROUND_UP);
00588                 if (x_i_j >= c && !redundancy_i[j])
00589                   return false;
00590               }
00591             }
00592         }
00593     }
00594 
00595   // The vector `var_conn' is used to check if there is a single cycle
00596   // that connected all zero-equivalent variables between them.
00597   // The value `space_dim + 1' is used to indicate that the equivalence
00598   // class contains a single variable.
00599   std::vector<dimension_type> var_conn(x_space_dim + 1);
00600   for (dimension_type i = x_space_dim + 1; i-- > 0; )
00601     var_conn[i] = x_space_dim + 1;
00602 
00603   // Step 3: we store really the `var_conn' with the right value, putting
00604   // the variable with the selected variable is connected:
00605   // we check the row of each variable:
00606   // a- each leader could be connected with only zero-equivalent one,
00607   // b- each no-leader with only another zero-equivalent one.
00608   for (dimension_type i = 0; i <= x_space_dim; ++i) {
00609     // It count with how many variables the selected variable is
00610     // connected.
00611     dimension_type t = 0;
00612     dimension_type ld_i = leader[i];
00613     // Case a: leader.
00614     if (ld_i == i) {
00615       for (dimension_type j = 0; j <= x_space_dim; ++j) {
00616         dimension_type ld_j = leader[j];
00617         // Only the connectedness with equivalent variables
00618         // is considered.
00619         if (j != ld_j)
00620           if (!redundancy_dbm[i][j]) {
00621             if (t == 1)
00622               // Two no-leaders couldn't connected with the same leader.
00623               return false;
00624             else
00625               if (ld_j != i)
00626                 // The variables isn't in the same equivalence class.
00627                 return false;
00628               else {
00629                 ++t;
00630                 var_conn[i] = j;
00631               }
00632           }
00633       }
00634     }
00635     // Case b: no-leader.
00636     else {
00637       for (dimension_type j = 0; j <= x_space_dim; ++j) {
00638         if (!redundancy_dbm[i][j]) {
00639           dimension_type ld_j = leader[j];
00640           if (ld_i != ld_j)
00641             // The variables isn't in the same equivalence class.
00642             return false;
00643           else {
00644             if (t == 1)
00645               // Two variables couldn't connected with the same leader.
00646               return false;
00647             else {
00648               ++t;
00649               var_conn[i] = j;
00650             }
00651           }
00652           // A no-leader must be connected with
00653           // another variable.
00654           if (t == 0)
00655             return false;
00656         }
00657       }
00658     }
00659   }
00660 
00661   // The vector `just_checked' is used to check if
00662   // a variable is already checked.
00663   std::vector<bool> just_checked(x_space_dim + 1);
00664   for (dimension_type i = x_space_dim + 1; i-- > 0; )
00665     just_checked[i] = false;
00666 
00667   // Step 4: we check if there are single cycles that
00668   // connected all the zero-equivalent variables between them.
00669   for (dimension_type i = 0; i <= x_space_dim; ++i) {
00670     bool jc_i = just_checked[i];
00671     // We do not re-check the already considered single cycles.
00672     if (!jc_i) {
00673       dimension_type v_con = var_conn[i];
00674       // We consider only the equivalence classes with
00675       // 2 or plus variables.
00676       if (v_con != x_space_dim + 1) {
00677         // There is a single cycle if taken a variable,
00678         // we return to this same variable.
00679         while (v_con != i) {
00680           just_checked[v_con] = true;
00681           v_con = var_conn[v_con];
00682           // If we re-pass to an already considered variable,
00683           // then we haven't a single cycle.
00684           if (just_checked[v_con])
00685             return false;
00686         }
00687       }
00688     }
00689     just_checked[i] = true;
00690   }
00691 
00692   // The system bounded differences is just reduced.
00693   return true;
00694 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::add_dbm_constraint	(	dimension_type	i,
		dimension_type	j,
		N	k
	)			`[inline, private]`

Adds the constraint dbm[i][j] <= k.

Definition at line 507 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::BD_Shape< T >::marked_shortest_path_closed(), Parma_Polyhedra_Library::BD_Shape< T >::OK(), Parma_Polyhedra_Library::BD_Shape< T >::Status::reset_shortest_path_closed(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), and Parma_Polyhedra_Library::BD_Shape< T >::status.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::add_dbm_constraint(), Parma_Polyhedra_Library::BD_Shape< T >::affine_image(), Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_image(), and Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_preimage().

00509                                      {
00510   // Private method: the caller has to ensure the following.
00511   assert(i <= space_dimension() && j <= space_dimension() && i != j);
00512   N& dbm_ij = dbm[i][j];
00513   if (dbm_ij > k) {
00514     dbm_ij = k;
00515     if (marked_shortest_path_closed())
00516       status.reset_shortest_path_closed();
00517   }
00518   assert(OK());
00519 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::add_dbm_constraint	(	dimension_type	i,
		dimension_type	j,
		Coefficient_traits::const_reference	num,
		Coefficient_traits::const_reference	den
	)			`[inline, private]`

Adds the constraint dbm[i][j] <= num/den.

Definition at line 523 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::add_dbm_constraint(), and Parma_Polyhedra_Library::BD_Shape< T >::space_dimension().

00526                                                                        {
00527   // Private method: the caller has to ensure the following.
00528   assert(i <= space_dimension() && j <= space_dimension() && i != j);
00529   assert(den != 0);
00530   N k;
00531   Implementation::BD_Shapes::div_round_up(k, num, den);
00532   add_dbm_constraint(i, j, k);
00533 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::forget_all_dbm_constraints ( dimension_type v ) [inline, private]

Removes all the constraints on row/column v.

Definition at line 677 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::dbm, and Parma_Polyhedra_Library::PLUS_INFINITY.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::affine_image(), Parma_Polyhedra_Library::BD_Shape< T >::affine_preimage(), Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_image(), and Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_preimage().

00677                                                               {
00678   assert(0 < v && v <= dbm.num_rows());
00679   DB_Row<N>& dbm_v = dbm[v];
00680   for (dimension_type i = dbm.num_rows(); i-- > 0; ) {
00681     dbm_v[i] = PLUS_INFINITY;
00682     dbm[i][v] = PLUS_INFINITY;
00683   }
00684 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::forget_binary_dbm_constraints ( dimension_type v ) [inline, private]

Removes all binary constraints on row/column v.

Definition at line 688 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::dbm, and Parma_Polyhedra_Library::PLUS_INFINITY.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::affine_image(), and Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_image().

00688                                                                  {
00689   assert(0 < v && v <= dbm.num_rows());
00690   DB_Row<N>& dbm_v = dbm[v];
00691   for (dimension_type i = dbm.num_rows()-1; i > 0; --i) {
00692     dbm_v[i] = PLUS_INFINITY;
00693     dbm[i][v] = PLUS_INFINITY;
00694   }
00695 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::deduce_v_minus_u_bounds	(	dimension_type	v,
		dimension_type	last_v,
		const Linear_Expression &	sc_expr,
		Coefficient_traits::const_reference	sc_den,
		const N &	pos_sum
	)			`[inline, private]`

An helper function for the computation of affine relations.

For each dbm index u (less than or equal to last_v and different from v), deduce constraints of the form v - u <= c, starting from pos_sum which is an upper bound for v.

The shortest-path closure is able to deduce the constraint v - u <= ub_v - lb_u. We can be more precise if variable u played an active role in the computation of the upper bound for v, i.e., if the corresponding coefficient q == sc_expr[u]/sc_den is greater than zero. In particular:

if q >= 1, then v - u <= ub_v - ub_u;
if 0 < q < 1, then v - u <= ub_v - (q*ub_u + (1-q)*lb_u).

Definition at line 1817 of file BD_Shape.templates.hh.

References Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::Linear_Expression::coefficient(), Parma_Polyhedra_Library::BD_Shape< T >::dbm, and Parma_Polyhedra_Library::is_plus_infinity().

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::affine_image(), Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_image(), and Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_preimage().

01821                                             {
01822   // Deduce constraints of the form `v - u', where `u != v'.
01823   // Note: the shortest-path closure is able to deduce the constraint
01824   // `v - u <= ub_v - lb_u'. We can be more precise if variable `u'
01825   // played an active role in the computation of the upper bound for `v',
01826   // i.e., if the corresponding coefficient `q == expr_u/den' is
01827   // greater than zero. In particular:
01828   // if `q >= 1',    then `v - u <= ub_v - ub_u';
01829   // if `0 < q < 1', then `v - u <= ub_v - (q*ub_u + (1-q)*lb_u)'.
01830   mpq_class mpq_sc_den;
01831   assign_r(mpq_sc_den, sc_den, ROUND_NOT_NEEDED);
01832   const DB_Row<N>& dbm_0 = dbm[0];
01833   // No need to consider indices greater than `last_v'.
01834   for (dimension_type u = last_v; u > 0; --u)
01835     if (u != v) {
01836       const Coefficient& expr_u = sc_expr.coefficient(Variable(u-1));
01837       if (expr_u > 0)
01838         if (expr_u >= sc_den)
01839           // Deducing `v - u <= ub_v - ub_u'.
01840           sub_assign_r(dbm[u][v], pos_sum, dbm_0[u], ROUND_UP);
01841         else {
01842           DB_Row<N>& dbm_u = dbm[u];
01843           const N& dbm_u0 = dbm_u[0];
01844           if (!is_plus_infinity(dbm_u0)) {
01845             // Let `ub_u' and `lb_u' be the known upper and lower bound
01846             // for `u', respectively. Letting `q = expr_u/sc_den' be the
01847             // rational coefficient of `u' in `sc_expr/sc_den',
01848             // the upper bound for `v - u' is computed as
01849             // `ub_v - (q * ub_u + (1-q) * lb_u)', i.e.,
01850             // `pos_sum + (-lb_u) - q * (ub_u + (-lb_u))'.
01851             mpq_class minus_lb_u;
01852             assign_r(minus_lb_u, dbm_u0, ROUND_NOT_NEEDED);
01853             mpq_class q;
01854             assign_r(q, expr_u, ROUND_NOT_NEEDED);
01855             div_assign_r(q, q, mpq_sc_den, ROUND_NOT_NEEDED);
01856             mpq_class ub_u;
01857             assign_r(ub_u, dbm_0[u], ROUND_NOT_NEEDED);
01858             // Compute `ub_u - lb_u'.
01859             add_assign_r(ub_u, ub_u, minus_lb_u, ROUND_NOT_NEEDED);
01860             // Compute `(-lb_u) - q * (ub_u - lb_u)'.
01861             sub_mul_assign_r(minus_lb_u, q, ub_u, ROUND_NOT_NEEDED);
01862             N up_approx;
01863             assign_r(up_approx, minus_lb_u, ROUND_UP);
01864             // Deducing `v - u <= ub_v - (q * ub_u + (1-q) * lb_u)'.
01865             add_assign_r(dbm_u[v], pos_sum, up_approx, ROUND_UP);
01866           }
01867         }
01868     }
01869 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::deduce_u_minus_v_bounds	(	dimension_type	v,
		dimension_type	last_v,
		const Linear_Expression &	sc_expr,
		Coefficient_traits::const_reference	sc_den,
		const N &	neg_sum
	)			`[inline, private]`

An helper function for the computation of affine relations.

For each dbm index u (less than or equal to last_v and different from v), deduce constraints of the form u - v <= c, starting from neg_sum which is a lower bound for v.

The shortest-path closure is able to deduce the constraint u - v <= ub_u - lb_v. We can be more precise if variable u played an active role in the computation of the lower bound for v, i.e., if the corresponding coefficient q == sc_expr[u]/sc_den is greater than zero. In particular:

if q >= 1, then u - v <= lb_u - lb_v;
if 0 < q < 1, then u - v <= (q*lb_u + (1-q)*ub_u) - lb_v.

Definition at line 1874 of file BD_Shape.templates.hh.

References Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::Linear_Expression::coefficient(), Parma_Polyhedra_Library::BD_Shape< T >::dbm, and Parma_Polyhedra_Library::is_plus_infinity().

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::affine_image(), Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_image(), and Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_preimage().

01878                                             {
01879   // Deduce constraints of the form `u - v', where `u != v'.
01880   // Note: the shortest-path closure is able to deduce the constraint
01881   // `u - v <= ub_u - lb_v'. We can be more precise if variable `u'
01882   // played an active role in the computation of the lower bound for `v',
01883   // i.e., if the corresponding coefficient `q == expr_u/den' is
01884   // greater than zero. In particular:
01885   // if `q >= 1',    then `u - v <= lb_u - lb_v';
01886   // if `0 < q < 1', then `u - v <= (q*lb_u + (1-q)*ub_u) - lb_v'.
01887   mpq_class mpq_sc_den;
01888   assign_r(mpq_sc_den, sc_den, ROUND_NOT_NEEDED);
01889   DB_Row<N>& dbm_0 = dbm[0];
01890   DB_Row<N>& dbm_v = dbm[v];
01891   // No need to consider indices greater than `last_v'.
01892   for (dimension_type u = last_v; u > 0; --u)
01893     if (u != v) {
01894       const Coefficient& expr_u = sc_expr.coefficient(Variable(u-1));
01895       if (expr_u > 0)
01896         if (expr_u >= sc_den)
01897           // Deducing `u - v <= lb_u - lb_v',
01898           // i.e., `u - v <= (-lb_v) - (-lb_u)'.
01899           sub_assign_r(dbm_v[u], neg_sum, dbm[u][0], ROUND_UP);
01900         else {
01901           const N& dbm_0u = dbm_0[u];
01902           if (!is_plus_infinity(dbm_0u)) {
01903             // Let `ub_u' and `lb_u' be the known upper and lower bound
01904             // for `u', respectively. Letting `q = expr_u/sc_den' be the
01905             // rational coefficient of `u' in `sc_expr/sc_den',
01906             // the upper bound for `u - v' is computed as
01907             // `(q * lb_u + (1-q) * ub_u) - lb_v', i.e.,
01908             // `ub_u - q * (ub_u + (-lb_u)) + neg_sum'.
01909             mpq_class ub_u;
01910             assign_r(ub_u, dbm_0u, ROUND_NOT_NEEDED);
01911             mpq_class q;
01912             assign_r(q, expr_u, ROUND_NOT_NEEDED);
01913             div_assign_r(q, q, mpq_sc_den, ROUND_NOT_NEEDED);
01914             mpq_class minus_lb_u;
01915             assign_r(minus_lb_u, dbm[u][0], ROUND_NOT_NEEDED);
01916             // Compute `ub_u - lb_u'.
01917             add_assign_r(minus_lb_u, minus_lb_u, ub_u, ROUND_NOT_NEEDED);
01918             // Compute `ub_u - q * (ub_u - lb_u)'.
01919             sub_mul_assign_r(ub_u, q, minus_lb_u, ROUND_NOT_NEEDED);
01920             N up_approx;
01921             assign_r(up_approx, ub_u, ROUND_UP);
01922             // Deducing `u - v <= (q*lb_u + (1-q)*ub_u) - lb_v'.
01923             add_assign_r(dbm_v[u], up_approx, neg_sum, ROUND_UP);
01924           }
01925         }
01926     }
01927 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::get_limiting_shape	(	const Constraint_System &	cs,
		BD_Shape< T > &	limiting_shape
	)			const `[inline, private]`

Adds to limiting_shape the bounded differences in cs that are satisfied by *this.

Definition at line 1534 of file BD_Shape.templates.hh.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::limited_BHMZ05_extrapolation_assign(), and Parma_Polyhedra_Library::BD_Shape< T >::limited_CC76_extrapolation_assign().

01535                                                                 {
01536   using Implementation::BD_Shapes::div_round_up;
01537 
01538   const dimension_type cs_space_dim = cs.space_dimension();
01539   // Private method: the caller has to ensure the following.
01540   assert(cs_space_dim <= space_dimension());
01541 
01542   bool changed = false;
01543   for (Constraint_System::const_iterator i = cs.begin(),
01544          iend = cs.end(); i != iend; ++i) {
01545     const Constraint& c = *i;
01546     dimension_type num_vars = 0;
01547     dimension_type i = 0;
01548     dimension_type j = 0;
01549     TEMP_INTEGER(coeff);
01550     // Constraints that are not bounded differences are ignored.
01551     if (extract_bounded_difference(c, cs_space_dim, num_vars, i, j, coeff)) {
01552       // Select the cell to be modified for the "<=" part of the constraint,
01553       // and set `coeff' to the absolute value of itself.
01554       const N& x = (coeff < 0) ? dbm[i][j] : dbm[j][i];
01555       const N& y = (coeff < 0) ? dbm[j][i] : dbm[i][j];
01556       DB_Matrix<N>& ls_dbm = limiting_shape.dbm;
01557       N& ls_x = (coeff < 0) ? ls_dbm[i][j] : ls_dbm[j][i];
01558       N& ls_y = (coeff < 0) ? ls_dbm[j][i] : ls_dbm[i][j];
01559       if (coeff < 0)
01560         coeff = -coeff;
01561       // Compute the bound for `x', rounding towards plus infinity.
01562       N d;
01563       div_round_up(d, c.inhomogeneous_term(), coeff);
01564       if (x <= d)
01565         if (c.is_inequality())
01566           if (ls_x > d) {
01567             ls_x = d;
01568             changed = true;
01569           }
01570         else {
01571           // Compute the bound for `y', rounding towards plus infinity.
01572           div_round_up(d, -c.inhomogeneous_term(), coeff);
01573           if (y <= d)
01574             if (ls_y > d) {
01575               ls_y = d;
01576               changed = true;
01577             }
01578 
01579         }
01580     }
01581   }
01582 
01583   // In general, adding a constraint does not preserve the shortest-path
01584   // closure of the system of bounded differences.
01585   if (changed && limiting_shape.marked_shortest_path_closed())
01586     limiting_shape.status.reset_shortest_path_closed();
01587 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::compute_predecessors ( std::vector< dimension_type > & predecessor ) const [inline, private]

Compute the (zero-equivalence classes) predecessor relation.

It is assumed that the BDS is not empty and shortest-path closed.

Definition at line 475 of file BD_Shape.templates.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), and Parma_Polyhedra_Library::BD_Shape< T >::marked_shortest_path_closed().

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::affine_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::compute_leaders(), and Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_reduction_assign().

00475                                                                    {
00476   assert(!marked_empty() && marked_shortest_path_closed());
00477   assert(predecessor.size() == 0);
00478   // Variables are ordered according to their index.
00479   // The vector `predecessor' is used to indicate which variable
00480   // immediately precedes a given one in the corresponding equivalence class.
00481   // The `leader' of an equivalence class is the element having minimum
00482   // index: leaders are their own predecessors.
00483   const dimension_type pred_size = dbm.num_rows();
00484   // Initially, each variable is leader of its own zero-equivalence class.
00485   predecessor.reserve(pred_size);
00486   for (dimension_type i = 0; i < pred_size; ++i)
00487     predecessor.push_back(i);
00488   // Now compute actual predecessors.
00489   for (dimension_type i = pred_size; i-- > 1; )
00490     if (i == predecessor[i]) {
00491       const DB_Row<N>& dbm_i = dbm[i];
00492       for (dimension_type j = i; j-- > 0; )
00493         if (j == predecessor[j]) {
00494           N negated_dbm_ji;
00495           if (neg_assign_r(negated_dbm_ji, dbm[j][i], ROUND_NOT_NEEDED) == V_EQ
00496               && negated_dbm_ji == dbm_i[j]) {
00497             // Choose as predecessor the variable having the smaller index.
00498             predecessor[i] = j;
00499             break;
00500           }
00501         }
00502     }
00503 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::compute_leaders ( std::vector< dimension_type > & leaders ) const [inline, private]

Compute the leaders of zero-equivalence classes.

It is assumed that the BDS is not empty and shortest-path closed.

Definition at line 507 of file BD_Shape.templates.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::compute_predecessors(), Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), and Parma_Polyhedra_Library::BD_Shape< T >::marked_shortest_path_closed().

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::minimized_constraints().

00507                                                                      {
00508   assert(!marked_empty() && marked_shortest_path_closed());
00509   assert(leaders.size() == 0);
00510   // Compute predecessor information.
00511   compute_predecessors(leaders);
00512   // Flatten the predecessor chains so as to obtain leaders.
00513   assert(leaders[0] == 0);
00514   for (dimension_type i = 1, iend = leaders.size(); i != iend; ++i) {
00515     const dimension_type l_i = leaders[i];
00516     assert(l_i <= i);
00517     if (l_i != i) {
00518       const dimension_type ll_i = leaders[l_i];
00519       assert(ll_i == leaders[ll_i]);
00520       leaders[i] = ll_i;
00521     }
00522   }
00523 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible	(	const char *	method,
		const BD_Shape< T > &	x
	)			const `[inline, private]`

Definition at line 3680 of file BD_Shape.templates.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::space_dimension().

03681                                                                    {
03682   std::ostringstream s;
03683   s << "PPL::";
03684   s << "BD_Shape::" << method << ":" << std::endl
03685     << "this->space_dimension() == " << space_dimension()
03686     << ", y->space_dimension() == " << y.space_dimension() << ".";
03687   throw std::invalid_argument(s.str());
03688 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible	(	const char *	method,
		dimension_type	required_dim
	)			const `[inline, private]`

Definition at line 3692 of file BD_Shape.templates.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::space_dimension().

03693                                                                              {
03694   std::ostringstream s;
03695   s << "PPL::";
03696   s << "BD_Shape::" << method << ":" << std::endl
03697     << "this->space_dimension() == " << space_dimension()
03698     << ", required dimension == " << required_dim << ".";
03699   throw std::invalid_argument(s.str());
03700 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible	(	const char *	method,
		const Constraint &	c
	)			const `[inline, private]`

Definition at line 3704 of file BD_Shape.templates.hh.

References Parma_Polyhedra_Library::Constraint::space_dimension(), and Parma_Polyhedra_Library::BD_Shape< T >::space_dimension().

03705                                                                      {
03706   std::ostringstream s;
03707   s << "PPL::";
03708   s << "BD_Shape::" << method << ":" << std::endl
03709     << "this->space_dimension() == " << space_dimension()
03710     << ", c->space_dimension == " << c.space_dimension() << ".";
03711   throw std::invalid_argument(s.str());
03712 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible	(	const char *	method,
		const Generator &	g
	)			const `[inline, private]`

Definition at line 3716 of file BD_Shape.templates.hh.

References Parma_Polyhedra_Library::Generator::space_dimension(), and Parma_Polyhedra_Library::BD_Shape< T >::space_dimension().

03717                                                                     {
03718   std::ostringstream s;
03719   s << "PPL::";
03720   s << "BD_Shape::" << method << ":" << std::endl
03721     << "this->space_dimension() == " << space_dimension()
03722     << ", g->space_dimension == " << g.space_dimension() << ".";
03723   throw std::invalid_argument(s.str());
03724 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible	(	const char *	method,
		const char *	name_row,
		const Linear_Expression &	y
	)			const `[inline, private]`

Definition at line 3749 of file BD_Shape.templates.hh.

References Parma_Polyhedra_Library::Linear_Expression::space_dimension(), and Parma_Polyhedra_Library::BD_Shape< T >::space_dimension().

03751                                                                             {
03752   std::ostringstream s;
03753   s << "PPL::";
03754   s << "BD_Shape::" << method << ":" << std::endl
03755     << "this->space_dimension() == " << space_dimension()
03756     << ", " << name_row << "->space_dimension() == "
03757     << y.space_dimension() << ".";
03758   throw std::invalid_argument(s.str());
03759 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::throw_constraint_incompatible ( const char * method ) [inline, static, private]

Definition at line 3728 of file BD_Shape.templates.hh.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::add_constraint(), Parma_Polyhedra_Library::BD_Shape< T >::limited_BHMZ05_extrapolation_assign(), Parma_Polyhedra_Library::BD_Shape< T >::limited_CC76_extrapolation_assign(), and Parma_Polyhedra_Library::BD_Shape< T >::relation_with().

03728                                                              {
03729   std::ostringstream s;
03730   s << "PPL::BD_Shape::" << method << ":" << std::endl
03731     << "the constraint is incompatible.";
03732   throw std::invalid_argument(s.str());
03733 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::throw_expression_too_complex	(	const char *	method,
		const Linear_Expression &	e
	)			`[inline, static, private]`

Definition at line 3737 of file BD_Shape.templates.hh.

03738                                                                       {
03739   using namespace IO_Operators;
03740   std::ostringstream s;
03741   s << "PPL::BD_Shape::" << method << ":" << std::endl
03742     << e << " is too complex.";
03743   throw std::invalid_argument(s.str());
03744 }

template<typename T>

void Parma_Polyhedra_Library::BD_Shape< T >::throw_generic	(	const char *	method,
		const char *	reason
	)			`[inline, static, private]`

Definition at line 3764 of file BD_Shape.templates.hh.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::affine_image(), Parma_Polyhedra_Library::BD_Shape< T >::affine_preimage(), Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_image(), and Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_preimage().

03764                                                                  {
03765   std::ostringstream s;
03766   s << "PPL::";
03767   s << "BD_Shape::" << method << ":" << std::endl
03768     << reason;
03769   throw std::invalid_argument(s.str());
03770 }

Friends And Related Function Documentation

template<typename T>

friend class Parma_Polyhedra_Library::BD_Shape [friend]

Definition at line 1151 of file BD_Shape.defs.hh.

template<typename T>

bool Parma_Polyhedra_Library::operator==	(	const BD_Shape< T > &	x,
		const BD_Shape< T > &	y
	)			`[friend]`

template<typename T>

template<typename Temp, typename To, typename U>

bool rectilinear_distance_assign	(	Checked_Number< To, Extended_Number_Policy > &	r,
		const BD_Shape< U > &	x,
		const BD_Shape< U > &	y,
		const Rounding_Dir	dir,
		Temp &	tmp0,
		Temp &	tmp1,
		Temp &	tmp2
	)			`[friend]`

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::rectilinear_distance_assign().

template<typename T>

template<typename Temp, typename To, typename U>

bool euclidean_distance_assign	(	Checked_Number< To, Extended_Number_Policy > &	r,
		const BD_Shape< U > &	x,
		const BD_Shape< U > &	y,
		const Rounding_Dir	dir,
		Temp &	tmp0,
		Temp &	tmp1,
		Temp &	tmp2
	)			`[friend]`

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::euclidean_distance_assign().

template<typename T>

template<typename Temp, typename To, typename U>

bool l_infinity_distance_assign	(	Checked_Number< To, Extended_Number_Policy > &	r,
		const BD_Shape< U > &	x,
		const BD_Shape< U > &	y,
		const Rounding_Dir	dir,
		Temp &	tmp0,
		Temp &	tmp1,
		Temp &	tmp2
	)			`[friend]`

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::l_infinity_distance_assign().

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 ", ".

Definition at line 3439 of file BD_Shape.templates.hh.

03439                                                             {
03440   typedef typename BD_Shape<T>::coefficient_type N;
03441   if (c.is_universe())
03442     s << "true";
03443   else {
03444     // We control empty system of bounded differences.
03445     dimension_type n = c.space_dimension();
03446     if (c.marked_empty())
03447       s << "false";
03448     else {
03449       bool first = true;
03450       for (dimension_type i = 0; i <= n; ++i)
03451         for (dimension_type j = i + 1; j <= n; ++j) {
03452           const N& c_i_j = c.dbm[i][j];
03453           const N& c_j_i = c.dbm[j][i];
03454           N negated_c_ji;
03455           if (neg_assign_r(negated_c_ji, c_j_i, ROUND_NOT_NEEDED) == V_EQ
03456               && negated_c_ji == c_i_j) {
03457             // We will print an equality.
03458             if (first)
03459               first = false;
03460             else
03461               s << ", ";
03462             if (i == 0) {
03463               // We have got a equality constraint with one Variable.
03464               s << Variable(j - 1);
03465               s << " == " << c_i_j;
03466             }
03467             else {
03468               // We have got a equality constraint with two Variables.
03469               if (c_i_j >= 0) {
03470                 s << Variable(j - 1);
03471                 s << " - ";
03472                 s << Variable(i - 1);
03473                 s << " == " << c_i_j;
03474               }
03475               else {
03476                 s << Variable(i - 1);
03477                 s << " - ";
03478                 s << Variable(j - 1);
03479                 s << " == " << c_j_i;
03480               }
03481             }
03482           }
03483           else {
03484             // We will print a non-strict inequality.
03485             if (!is_plus_infinity(c_j_i)) {
03486               if (first)
03487                 first = false;
03488               else
03489                 s << ", ";
03490               if (i == 0) {
03491                 // We have got a constraint with an only Variable.
03492                 s << Variable(j - 1);
03493                 N v;
03494                 neg_assign_r(v, c_j_i, ROUND_DOWN);
03495                 s << " >= " << v;
03496               }
03497               else {
03498                 // We have got a constraint with two Variables.
03499                 if (c_j_i >= 0) {
03500                   s << Variable(i - 1);
03501                   s << " - ";
03502                   s << Variable(j - 1);
03503                   s << " <= " << c_j_i;
03504                 }
03505                 else {
03506                   s << Variable(j - 1);
03507                   s << " - ";
03508                   s << Variable(i - 1);
03509                   N v;
03510                   neg_assign_r(v, c_j_i, ROUND_DOWN);
03511                   s << " >= " << v;
03512                 }
03513               }
03514             }
03515             if (!is_plus_infinity(c_i_j)) {
03516               if (first)
03517                 first = false;
03518               else
03519                 s << ", ";
03520               if (i == 0) {
03521                 // We have got a constraint with an only Variable.
03522                 s << Variable(j - 1);
03523                 s << " <= " << c_i_j;
03524               }
03525               else {
03526                 // We have got a constraint with two Variables.
03527                 if (c_i_j >= 0) {
03528                   s << Variable(j - 1);
03529                   s << " - ";
03530                   s << Variable(i - 1);
03531                   s << " <= " << c_i_j;
03532                 }
03533                 else {
03534                   s << Variable(i - 1);
03535                   s << " - ";
03536                   s << Variable(j - 1);
03537                   N v;
03538                   neg_assign_r(v, c_i_j, ROUND_DOWN);
03539                   s << " >= " << v;
03540                 }
03541               }
03542             }
03543           }
03544         }
03545     }
03546   }
03547   return s;
03548 }

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.

Definition at line 279 of file BD_Shape.inlines.hh.

00279                                                        {
00280   const dimension_type x_space_dim = x.space_dimension();
00281   // Dimension-compatibility check.
00282   if (x_space_dim != y.space_dimension())
00283     return false;
00284 
00285   // Zero-dim BDSs are equal if and only if they are both empty or universe.
00286   if (x_space_dim == 0)
00287     if (x.marked_empty())
00288       return y.marked_empty();
00289     else
00290       return !y.marked_empty();
00291 
00292   // The exact equivalence test requires shortest-path closure.
00293   x.shortest_path_closure_assign();
00294   y.shortest_path_closure_assign();
00295 
00296   // If one of two BDSs is empty, then they are equal
00297   // if and only if the other BDS is empty too.
00298   if (x.marked_empty())
00299     return y.marked_empty();
00300   if (y.marked_empty())
00301     return false;
00302   // Check for syntactic equivalence of the two (shortest-path closed)
00303   // systems of bounded differences.
00304   return x.dbm == y.dbm;
00305 }

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.

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

00309                                                        {
00310   return !(x == y);
00311 }

template<typename To, 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>.

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<Temp, Extended_Number_Policy>.

Definition at line 357 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::rectilinear_distance_assign.

00360                                                     {
00361   static Checked_Number<Temp, Extended_Number_Policy> tmp0;
00362   static Checked_Number<Temp, Extended_Number_Policy> tmp1;
00363   static Checked_Number<Temp, Extended_Number_Policy> tmp2;
00364   return rectilinear_distance_assign(r, x, y, dir, tmp0, tmp1, tmp2);
00365 }

template<typename Temp, typename To, 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.

Definition at line 316 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), Parma_Polyhedra_Library::PLUS_INFINITY, Parma_Polyhedra_Library::BD_Shape< T >::rectilinear_distance_assign, Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign(), and Parma_Polyhedra_Library::BD_Shape< T >::space_dimension().

00322                                         {
00323   const dimension_type x_space_dim = x.space_dimension();
00324   // Dimension-compatibility check.
00325   if (x_space_dim != y.space_dimension())
00326     return false;
00327 
00328   // Zero-dim BDSs are equal if and only if they are both empty or universe.
00329   if (x_space_dim == 0) {
00330     if (x.marked_empty() == y.marked_empty())
00331       assign_r(r, 0, ROUND_NOT_NEEDED);
00332     else
00333       r = PLUS_INFINITY;
00334     return true;
00335   }
00336 
00337   // The distance computation requires shortest-path closure.
00338   x.shortest_path_closure_assign();
00339   y.shortest_path_closure_assign();
00340 
00341   // If one of two BDSs is empty, then they are equal if and only if
00342   // the other BDS is empty too.
00343   if (x.marked_empty() ||  y.marked_empty()) {
00344    if (x.marked_empty() == y.marked_empty())
00345       assign_r(r, 0, ROUND_NOT_NEEDED);
00346     else
00347       r = PLUS_INFINITY;
00348    return true;
00349   }
00350 
00351   return rectilinear_distance_assign(r, x.dbm, y.dbm, dir, tmp0, tmp1, tmp2);
00352 }

template<typename To, 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>.

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<Temp, Extended_Number_Policy>.

Definition at line 421 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::euclidean_distance_assign.

00424                                                   {
00425   static Checked_Number<Temp, Extended_Number_Policy> tmp0;
00426   static Checked_Number<Temp, Extended_Number_Policy> tmp1;
00427   static Checked_Number<Temp, Extended_Number_Policy> tmp2;
00428   return euclidean_distance_assign(r, x, y, dir, tmp0, tmp1, tmp2);
00429 }

template<typename Temp, typename To, 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.

Definition at line 380 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::BD_Shape< T >::euclidean_distance_assign, Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), Parma_Polyhedra_Library::PLUS_INFINITY, Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign(), and Parma_Polyhedra_Library::BD_Shape< T >::space_dimension().

00386                                       {
00387   const dimension_type x_space_dim = x.space_dimension();
00388   // Dimension-compatibility check.
00389   if (x_space_dim != y.space_dimension())
00390     return false;
00391 
00392   // Zero-dim BDSs are equal if and only if they are both empty or universe.
00393   if (x_space_dim == 0) {
00394     if (x.marked_empty() == y.marked_empty())
00395       assign_r(r, 0, ROUND_NOT_NEEDED);
00396     else
00397       r = PLUS_INFINITY;
00398     return true;
00399   }
00400 
00401   // The distance computation requires shortest-path closure.
00402   x.shortest_path_closure_assign();
00403   y.shortest_path_closure_assign();
00404 
00405   // If one of two BDSs is empty, then they are equal if and only if
00406   // the other BDS is empty too.
00407   if (x.marked_empty() ||  y.marked_empty()) {
00408    if (x.marked_empty() == y.marked_empty())
00409       assign_r(r, 0, ROUND_NOT_NEEDED);
00410     else
00411       r = PLUS_INFINITY;
00412    return true;
00413   }
00414 
00415   return euclidean_distance_assign(r, x.dbm, y.dbm, dir, tmp0, tmp1, tmp2);
00416 }

template<typename To, 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>.

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<Temp, Extended_Number_Policy>.

Definition at line 485 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::l_infinity_distance_assign.

00488                                                    {
00489   static Checked_Number<Temp, Extended_Number_Policy> tmp0;
00490   static Checked_Number<Temp, Extended_Number_Policy> tmp1;
00491   static Checked_Number<Temp, Extended_Number_Policy> tmp2;
00492   return l_infinity_distance_assign(r, x, y, dir, tmp0, tmp1, tmp2);
00493 }

template<typename Temp, typename To, 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.

Definition at line 444 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::BD_Shape< T >::l_infinity_distance_assign, Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), Parma_Polyhedra_Library::PLUS_INFINITY, Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign(), and Parma_Polyhedra_Library::BD_Shape< T >::space_dimension().

00450                                        {
00451   const dimension_type x_space_dim = x.space_dimension();
00452   // Dimension-compatibility check.
00453   if (x_space_dim != y.space_dimension())
00454     return false;
00455 
00456   // Zero-dim BDSs are equal if and only if they are both empty or universe.
00457   if (x_space_dim == 0) {
00458     if (x.marked_empty() == y.marked_empty())
00459       assign_r(r, 0, ROUND_NOT_NEEDED);
00460     else
00461       r = PLUS_INFINITY;
00462     return true;
00463   }
00464 
00465   // The distance computation requires shortest-path closure.
00466   x.shortest_path_closure_assign();
00467   y.shortest_path_closure_assign();
00468 
00469   // If one of two BDSs is empty, then they are equal if and only if
00470   // the other BDS is empty too.
00471   if (x.marked_empty() ||  y.marked_empty()) {
00472    if (x.marked_empty() == y.marked_empty())
00473       assign_r(r, 0, ROUND_NOT_NEEDED);
00474     else
00475       r = PLUS_INFINITY;
00476    return true;
00477   }
00478 
00479   return l_infinity_distance_assign(r, x.dbm, y.dbm, dir, tmp0, tmp1, tmp2);
00480 }

template<typename T>

void swap	(	Parma_Polyhedra_Library::BD_Shape< T > &	x,
		Parma_Polyhedra_Library::BD_Shape< T > &	y
	)			`[related]`

Specializes std::swap.

Definition at line 704 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::swap().

00705                                             {
00706   x.swap(y);
00707 }

template<typename T, typename Policy>

void numer_denom	(	const Checked_Number< T, Policy > &	from,
		Coefficient &	num,
		Coefficient &	den
	)			`[related]`

Extract the numerator and denominator components of from.

Definition at line 45 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::is_minus_infinity(), Parma_Polyhedra_Library::is_not_a_number(), and Parma_Polyhedra_Library::is_plus_infinity().

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::constraints(), and Parma_Polyhedra_Library::BD_Shape< T >::minimized_constraints().

00046                                                 {
00047   assert(!is_not_a_number(from)
00048          && !is_minus_infinity(from)
00049          && !is_plus_infinity(from));
00050   mpq_class q;
00051   assign_r(q, from, ROUND_NOT_NEEDED);
00052   num = q.get_num();
00053   den = q.get_den();
00054 }

template<typename T, typename Policy>

void div_round_up	(	Checked_Number< T, Policy > &	to,
		Coefficient_traits::const_reference	x,
		Coefficient_traits::const_reference	y
	)			`[related]`

Divides x by y into to, rounding the result towards plus infinity.

Definition at line 62 of file BD_Shape.inlines.hh.

References Parma_Polyhedra_Library::assign_r().

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::add_constraint(), Parma_Polyhedra_Library::BD_Shape< T >::affine_image(), Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape(), Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_image(), Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_preimage(), Parma_Polyhedra_Library::BD_Shape< T >::get_limiting_shape(), and Parma_Polyhedra_Library::BD_Shape< T >::relation_with().

00064                                                   {
00065   mpq_class qx;
00066   mpq_class qy;
00067   // Note: this code assumes that a Coefficient is always convertible
00068   // to an mpq_class without loss of precision.
00069   assign_r(qx, x, ROUND_NOT_NEEDED);
00070   assign_r(qy, y, ROUND_NOT_NEEDED);
00071   div_assign_r(qx, qx, qy, ROUND_NOT_NEEDED);
00072   assign_r(to, qx, ROUND_UP);
00073 }

template<typename N>

void min_assign	(	N &	x,
		const N &	y
	)			`[related]`

Assigns to x the minimum between x and y.

Definition at line 81 of file BD_Shape.inlines.hh.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign().

00081                              {
00082   if (x > y)
00083     x = y;
00084 }

template<typename N>

void max_assign	(	N &	x,
		const N &	y
	)			`[related]`

Assigns to x the maximum between x and y.

Definition at line 92 of file BD_Shape.inlines.hh.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape().

00092                              {
00093   if (x < y)
00094     x = y;
00095 }

template<typename T>

bool extract_bounded_difference	(	const Constraint &	c,
		const dimension_type	c_space_dim,
		dimension_type &	c_num_vars,
		dimension_type &	c_first_var,
		dimension_type &	c_second_var,
		Coefficient &	c_coeff
	)			`[related]`

Definition at line 32 of file BD_Shape.cc.

References Parma_Polyhedra_Library::Constraint::coefficient(), and Parma_Polyhedra_Library::Constraint::space_dimension().

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::add_constraint(), Parma_Polyhedra_Library::BD_Shape< T >::get_limiting_shape(), and Parma_Polyhedra_Library::BD_Shape< T >::relation_with().

00037                                                       {
00038   // Check for preconditions.
00039   assert(c.space_dimension() == c_space_dim);
00040   assert(c_num_vars == 0 && c_first_var == 0 && c_second_var == 0);
00041   // Store the indices of the non-zero components of `c',
00042   dimension_type non_zero_index[2] = { 0, 0 };
00043   // Collect the non-zero components of `c'.
00044   for (dimension_type i = c_space_dim; i-- > 0; )
00045     if (c.coefficient(Variable(i)) != 0)
00046       if (c_num_vars <= 1)
00047         non_zero_index[c_num_vars++] = i + 1;
00048       else
00049         // Constraint `c' is not a bounded difference.
00050         return false;
00051 
00052   // Make sure that `c' is indeed a bounded difference,
00053   // i.e., it has one of the following forms:
00054   //           0 <=/= b, if c_num_vars == 0;
00055   //   a*x       <=/= b, if c_num_vars == 1;
00056   //   a*x - a*y <=/= b, if c_num_vars == 2.
00057   switch (c_num_vars) {
00058   case 2:
00059     {
00060       const Coefficient& c0 = c.coefficient(Variable(non_zero_index[0]-1));
00061       const Coefficient& c1 = c.coefficient(Variable(non_zero_index[1]-1));
00062       if (sgn(c0) == sgn(c1) || c0 != -c1)
00063         // Constraint `c' is not a bounded difference.
00064         return false;
00065       c_coeff = c1;
00066     }
00067     c_first_var = non_zero_index[0];
00068     c_second_var = non_zero_index[1];
00069     break;
00070   case 1:
00071     c_coeff = -c.coefficient(Variable(non_zero_index[0]-1));
00072     c_first_var = non_zero_index[0];
00073     break;
00074   default:
00075     assert(c_num_vars == 0);
00076     break;
00077   }
00078   return true;
00079 }

template<typename T>

void compute_leader_indices	(	const std::vector< dimension_type > &	predecessor,
		std::vector< dimension_type > &	indices
	)			`[related]`

Definition at line 85 of file BD_Shape.cc.

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::minimized_constraints(), and Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_reduction_assign().

00086                                                                 {
00087   // The vector `indices' contains one entry for each equivalence
00088   // class, storing the index of the corresponding leader in
00089   // increasing order: it is used to avoid repeated tests for leadership.
00090   assert(indices.size() == 0);
00091   assert(0 == predecessor[0]);
00092   indices.push_back(0);
00093   for (dimension_type i = 1, iend = predecessor.size(); i != iend; ++i)
00094     if (i == predecessor[i])
00095       indices.push_back(i);
00096 }

Member Data Documentation

template<typename T>

DB_Matrix<N> Parma_Polyhedra_Library::BD_Shape< T >::dbm [private]

The matrix representing the system of bounded differences.

Definition at line 1154 of file BD_Shape.defs.hh.

template<typename T>

Status Parma_Polyhedra_Library::BD_Shape< T >::status [private]

The status flags to keep track of the internal state.

Definition at line 1276 of file BD_Shape.defs.hh.

template<typename T>

std::vector<std::deque<bool> > Parma_Polyhedra_Library::BD_Shape< T >::redundancy_dbm [private]

A matrix of Booleans indicating which constraints are redundant.

Definition at line 1279 of file BD_Shape.defs.hh.

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


Exception Throwers
void	throw_dimension_incompatible (const char *method, const BD_Shape &x) const
void	throw_dimension_incompatible (const char *method, dimension_type required_dim) const
void	throw_dimension_incompatible (const char *method, const Constraint &c) const
void	throw_dimension_incompatible (const char *method, const Generator &g) const
void	throw_dimension_incompatible (const char method, const char name_row, const Linear_Expression &y) const
static void	throw_constraint_incompatible (const char *method)
static void	throw_expression_too_complex (const char *method, const Linear_Expression &e)
static void	throw_generic (const char method, const char reason)
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
void	ascii_dump () const
	Writes to `std::cerr` an ASCII representation of `*this`.
void	ascii_dump (std::ostream &s) const
	Writes to `s` an ASCII representation of `*this`.
void	print () const
	Prints `*this` to `std::cerr` using `operator<<`.
bool	ascii_load (std::istream &s)
	Loads from `s` an ASCII representation (as produced by ascii_dump) and sets `*this` accordingly. Returns `true` if successful, `false` otherwise.
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_Shape &	operator= (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 , 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.
Private Types
typedef Checked_Number< T, Extended_Number_Policy >	N
	The (extended) numeric type of the inhomogeneous term of the inequalities defining a BDS.
Private Member Functions
bool	marked_empty () const
	Returns `true` if the BDS is known to be empty.
bool	marked_shortest_path_closed () const
	Returns `true` if the system of bounded differences is known to be shortest-path closed.
bool	marked_shortest_path_reduced () const
	Returns `true` if the system of bounded differences is known to be shortest-path reduced.
void	set_empty ()
	Turns `*this` into an empty BDS.
void	set_zero_dim_univ ()
	Turns `*this` into an zero-dimensional universe BDS.
void	shortest_path_closure_assign () const
	Assigns to `this->dbm` its shortest-path closure.
void	shortest_path_reduction_assign () const
	Assigns to `this->dbm` its shortest-path closure and records into `this->redundancy_dbm` which of the entries in `this->dbm` are redundant.
bool	is_shortest_path_reduced () const
	Returns `true` if and only if `this->dbm` is shortest-path closed and `this->redundancy_dbm` correctly flags the redundant entries in `this->dbm`.
void	add_dbm_constraint (dimension_type i, dimension_type j, N k)
	Adds the constraint `dbm[i][j] <= k`.
void	add_dbm_constraint (dimension_type i, dimension_type j, Coefficient_traits::const_reference num, Coefficient_traits::const_reference den)
	Adds the constraint `dbm[i][j] <= num/den`.
void	forget_all_dbm_constraints (dimension_type v)
	Removes all the constraints on row/column `v`.
void	forget_binary_dbm_constraints (dimension_type v)
	Removes all binary constraints on row/column `v`.
void	deduce_v_minus_u_bounds (dimension_type v, dimension_type last_v, const Linear_Expression &sc_expr, Coefficient_traits::const_reference sc_den, const N &pos_sum)
	An helper function for the computation of affine relations.
void	deduce_u_minus_v_bounds (dimension_type v, dimension_type last_v, const Linear_Expression &sc_expr, Coefficient_traits::const_reference sc_den, const N &neg_sum)
	An helper function for the computation of affine relations.
void	get_limiting_shape (const Constraint_System &cs, BD_Shape &limiting_shape) const
	Adds to `limiting_shape` the bounded differences in `cs` that are satisfied by `*this`.
void	compute_predecessors (std::vector< dimension_type > &predecessor) const
	Compute the (zero-equivalence classes) predecessor relation.
void	compute_leaders (std::vector< dimension_type > &leaders) const
	Compute the leaders of zero-equivalence classes.
Private Attributes
DB_Matrix< N >	dbm
	The matrix representing the system of bounded differences.
Status	status
	The status flags to keep track of the internal state.
std::vector< std::deque< bool > >	redundancy_dbm
	A matrix of Booleans indicating which constraints are redundant.
Friends
class	Parma_Polyhedra_Library::BD_Shape
bool	Parma_Polyhedra_Library::operator== (const BD_Shape< T > &x, const BD_Shape< T > &y)
template<typename Temp, typename To, typename U>
bool	rectilinear_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const BD_Shape< U > &x, const BD_Shape< U > &y, const Rounding_Dir dir, Temp &tmp0, Temp &tmp1, Temp &tmp2)
template<typename Temp, typename To, typename U>
bool	euclidean_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const BD_Shape< U > &x, const BD_Shape< U > &y, const Rounding_Dir dir, Temp &tmp0, Temp &tmp1, Temp &tmp2)
template<typename Temp, typename To, typename U>
bool	l_infinity_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const BD_Shape< U > &x, const BD_Shape< U > &y, const Rounding_Dir dir, Temp &tmp0, Temp &tmp1, Temp &tmp2)
std::ostream &	operator<< (std::ostream &s, const BD_Shape< T > &c)
	Output operator.
Related Functions
(Note that these are not member functions.)
template<typename T>
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.
template<typename T>
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.
template<typename To, 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)
	Computes the rectilinear (or Manhattan) distance between `x` and `y`.
template<typename Temp, typename To, 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)
	Computes the rectilinear (or Manhattan) distance between `x` and `y`.
template<typename To, 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)
	Computes the euclidean distance between `x` and `y`.
template<typename Temp, typename To, 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)
	Computes the euclidean distance between `x` and `y`.
template<typename To, 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)
	Computes the $L_\infty$ distance between `x` and `y`.
template<typename Temp, typename To, 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)
	Computes the $L_\infty$ distance between `x` and `y`.
template<typename T>
void	swap (Parma_Polyhedra_Library::BD_Shape< T > &x, Parma_Polyhedra_Library::BD_Shape< T > &y)
	Specializes `std::swap`.
template<typename T, typename Policy>
void	numer_denom (const Checked_Number< T, Policy > &from, Coefficient &num, Coefficient &den)
	Extract the numerator and denominator components of `from`.
template<typename T, typename Policy>
void	div_round_up (Checked_Number< T, Policy > &to, Coefficient_traits::const_reference x, Coefficient_traits::const_reference y)
	Divides `x` by `y` into `to`, rounding the result towards plus infinity.
template<typename N>
void	min_assign (N &x, const N &y)
	Assigns to `x` the minimum between `x` and `y`.
template<typename N>
void	max_assign (N &x, const N &y)
	Assigns to `x` the maximum between `x` and `y`.
bool	extract_bounded_difference (const Constraint &c, const dimension_type c_space_dim, dimension_type &c_num_vars, dimension_type &c_first_var, dimension_type &c_second_var, Coefficient &c_coeff)
void	compute_leader_indices (const std::vector< dimension_type > &predecessor, std::vector< dimension_type > &indices)
Classes
class	Status
	A conjunctive assertion about a BD_Shape<T> object. More...

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

Exception Throwers

Public Types

Public Member Functions

Static Public Member Functions

Private Types

Private Member Functions

Private Attributes

Friends

Related Functions

Classes

Detailed Description

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

Member Typedef Documentation

Constructor & Destructor Documentation

Member Function Documentation

Friends And Related Function Documentation

Member Data Documentation

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

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