#include <BD_Shape.defs.hh>
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 ![]() *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 ![]() ![]() 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 ![]() ![]() 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 ![]() ![]() 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 ![]() 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 ![]() 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... |
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 or
, where the inhomogeneous term
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 , as well as rounding-aware implementations for several arithmetic functions. The value of the type parameter
T
may be one of the following:
int32_t
or int64_t
);float
or double
);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
where and
,
,
are integer coefficients such that
, or
, or
. 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 will be approximated by:
T
is a (bounded or unbounded) integer type;T
is the unbounded rational type mpq_class
;T
is a floating point type (having no exact representation for
On the other hand, a Constraint object encoding 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);
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);
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.
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.
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.
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.
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.
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 }
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 }
Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape | ( | const BD_Shape< U > & | 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 }
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
.
cs | A system of constraints: constraints that are not bounded differences are ignored (even though they may have contributed to the space dimension). |
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 }
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
.
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.
References Parma_Polyhedra_Library::Generator_System::begin(), Parma_Polyhedra_Library::Generator::CLOSURE_POINT, Parma_Polyhedra_Library::Generator::coefficient(), Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::BD_Shape< T >::div_round_up(), Parma_Polyhedra_Library::Generator::divisor(), Parma_Polyhedra_Library::Generator_System::end(), Parma_Polyhedra_Library::Generator::LINE, Parma_Polyhedra_Library::BD_Shape< T >::max_assign(), Parma_Polyhedra_Library::BD_Shape< T >::OK(), Parma_Polyhedra_Library::PLUS_INFINITY, Parma_Polyhedra_Library::Generator::POINT, Parma_Polyhedra_Library::Generator::RAY, Parma_Polyhedra_Library::BD_Shape< T >::set_empty(), Parma_Polyhedra_Library::BD_Shape< T >::Status::set_shortest_path_closed(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::status, and Parma_Polyhedra_Library::Generator::type().
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 }
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.
References Parma_Polyhedra_Library::LP_Problem::add_constraint(), Parma_Polyhedra_Library::LP_Problem::add_constraints(), Parma_Polyhedra_Library::ANY_COMPLEXITY, Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape(), Parma_Polyhedra_Library::Constraint_System::begin(), Parma_Polyhedra_Library::Polyhedron::con_sys, Parma_Polyhedra_Library::Polyhedron::constraints(), Parma_Polyhedra_Library::Polyhedron::constraints_are_minimized(), Parma_Polyhedra_Library::Polyhedron::constraints_are_up_to_date(), Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::BD_Shape< T >::div_round_up(), Parma_Polyhedra_Library::EMPTY, Parma_Polyhedra_Library::Constraint_System::end(), Parma_Polyhedra_Library::LP_Problem::evaluate_objective_function(), Parma_Polyhedra_Library::Polyhedron::generators(), Parma_Polyhedra_Library::Polyhedron::generators_are_up_to_date(), Parma_Polyhedra_Library::Polyhedron::has_pending_constraints(), Parma_Polyhedra_Library::Polyhedron::has_something_pending(), Parma_Polyhedra_Library::Constraint_System::has_strict_inequalities(), Parma_Polyhedra_Library::Constraint::is_equality(), Parma_Polyhedra_Library::LP_Problem::is_satisfiable(), Parma_Polyhedra_Library::Polyhedron::is_universe(), Parma_Polyhedra_Library::Polyhedron::marked_empty(), Parma_Polyhedra_Library::MAXIMIZATION, Parma_Polyhedra_Library::OPTIMIZED_LP_PROBLEM, Parma_Polyhedra_Library::LP_Problem::optimizing_point(), Parma_Polyhedra_Library::PLUS_INFINITY, Parma_Polyhedra_Library::LP_Problem::set_objective_function(), Parma_Polyhedra_Library::LP_Problem::set_optimization_mode(), Parma_Polyhedra_Library::BD_Shape< T >::Status::set_shortest_path_closed(), Parma_Polyhedra_Library::SIMPLEX_COMPLEXITY, Parma_Polyhedra_Library::LP_Problem::solve(), Parma_Polyhedra_Library::Polyhedron::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::status, TEMP_INTEGER, Parma_Polyhedra_Library::UNBOUNDED_LP_PROBLEM, and Parma_Polyhedra_Library::UNIVERSE.
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 }
Parma_Polyhedra_Library::BD_Shape< T >::~BD_Shape | ( | ) | [inline] |
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 }
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 }
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 }
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.
Referenced by Parma_Polyhedra_Library::BD_Shape< T >::add_constraint(), Parma_Polyhedra_Library::BD_Shape< T >::add_dbm_constraint(), Parma_Polyhedra_Library::BD_Shape< T >::add_space_dimensions_and_embed(), Parma_Polyhedra_Library::BD_Shape< T >::add_space_dimensions_and_project(), Parma_Polyhedra_Library::BD_Shape< T >::affine_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::affine_image(), Parma_Polyhedra_Library::BD_Shape< T >::affine_preimage(), Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape(), Parma_Polyhedra_Library::BD_Shape< T >::bds_difference_assign(), Parma_Polyhedra_Library::BD_Shape< T >::bds_hull_assign(), Parma_Polyhedra_Library::BD_Shape< T >::bds_hull_assign_and_minimize(), 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 >::concatenate_assign(), Parma_Polyhedra_Library::BD_Shape< T >::constraints(), Parma_Polyhedra_Library::BD_Shape< T >::contains(), Parma_Polyhedra_Library::BD_Shape< T >::euclidean_distance_assign(), 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(), Parma_Polyhedra_Library::BD_Shape< T >::intersection_assign(), Parma_Polyhedra_Library::BD_Shape< T >::is_shortest_path_reduced(), Parma_Polyhedra_Library::BD_Shape< T >::is_universe(), Parma_Polyhedra_Library::BD_Shape< T >::l_infinity_distance_assign(), Parma_Polyhedra_Library::BD_Shape< T >::limited_BHMZ05_extrapolation_assign(), Parma_Polyhedra_Library::BD_Shape< T >::limited_CC76_extrapolation_assign(), Parma_Polyhedra_Library::BD_Shape< T >::map_space_dimensions(), Parma_Polyhedra_Library::BD_Shape< T >::minimized_constraints(), Parma_Polyhedra_Library::operator==(), Parma_Polyhedra_Library::BD_Shape< T >::rectilinear_distance_assign(), Parma_Polyhedra_Library::BD_Shape< T >::relation_with(), Parma_Polyhedra_Library::BD_Shape< T >::remove_higher_space_dimensions(), Parma_Polyhedra_Library::BD_Shape< T >::remove_space_dimensions(), Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign(), Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_reduction_assign(), Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible(), and Parma_Polyhedra_Library::BD_Shape< T >::time_elapse_assign().
00266 { 00267 return dbm.num_rows() - 1; 00268 }
dimension_type Parma_Polyhedra_Library::BD_Shape< T >::affine_dimension | ( | ) | const [inline] |
Returns , 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 }
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.
References Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::Constraint_System::insert(), 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 >::minimized_constraints(), Parma_Polyhedra_Library::BD_Shape< T >::numer_denom(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), TEMP_INTEGER, and Parma_Polyhedra_Library::Constraint_System::zero_dim_empty().
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 }
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.
References Parma_Polyhedra_Library::BD_Shape< T >::compute_leader_indices(), Parma_Polyhedra_Library::BD_Shape< T >::compute_leaders(), Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::Constraint_System::insert(), Parma_Polyhedra_Library::is_plus_infinity(), Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), Parma_Polyhedra_Library::BD_Shape< T >::numer_denom(), Parma_Polyhedra_Library::BD_Shape< T >::redundancy_dbm, Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_reduction_assign(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), TEMP_INTEGER, and Parma_Polyhedra_Library::Constraint_System::zero_dim_empty().
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 }
bool Parma_Polyhedra_Library::BD_Shape< T >::contains | ( | const BD_Shape< T > & | y | ) | const [inline] |
Returns true
if and only if *this
contains y
.
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 }
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
.
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().
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
.
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.
References Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::BD_Shape< T >::div_round_up(), Parma_Polyhedra_Library::Constraint::EQUALITY, Parma_Polyhedra_Library::BD_Shape< T >::extract_bounded_difference(), Parma_Polyhedra_Library::Constraint::inhomogeneous_term(), Parma_Polyhedra_Library::Poly_Con_Relation::is_disjoint(), Parma_Polyhedra_Library::Constraint::is_equality(), Parma_Polyhedra_Library::Poly_Con_Relation::is_included(), Parma_Polyhedra_Library::Constraint::is_inequality(), Parma_Polyhedra_Library::Constraint::is_strict_inequality(), Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), Parma_Polyhedra_Library::Constraint::NONSTRICT_INEQUALITY, Parma_Polyhedra_Library::Poly_Con_Relation::saturates(), Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), Parma_Polyhedra_Library::Constraint::space_dimension(), Parma_Polyhedra_Library::Constraint::STRICT_INEQUALITY, Parma_Polyhedra_Library::Poly_Con_Relation::strictly_intersects(), TEMP_INTEGER, Parma_Polyhedra_Library::BD_Shape< T >::throw_constraint_incompatible(), Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible(), and Parma_Polyhedra_Library::Constraint::type().
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 }
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
.
std::invalid_argument | Thrown if *this and generator g are dimension-incompatible. |
Definition at line 806 of file BD_Shape.templates.hh.
References Parma_Polyhedra_Library::Generator::coefficient(), Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::Generator::is_line(), Parma_Polyhedra_Library::is_plus_infinity(), Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), Parma_Polyhedra_Library::Poly_Gen_Relation::nothing(), Parma_Polyhedra_Library::Variable::space_dimension(), Parma_Polyhedra_Library::Generator::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), Parma_Polyhedra_Library::Poly_Gen_Relation::subsumes(), and Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible().
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 }
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 }
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 }
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.
References Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::is_minus_infinity(), Parma_Polyhedra_Library::is_plus_infinity(), Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), Parma_Polyhedra_Library::BD_Shape< T >::marked_shortest_path_closed(), Parma_Polyhedra_Library::BD_Shape< T >::marked_shortest_path_reduced(), Parma_Polyhedra_Library::BD_Shape< T >::Status::OK(), Parma_Polyhedra_Library::BD_Shape< T >::redundancy_dbm, Parma_Polyhedra_Library::BD_Shape< T >::Status::reset_shortest_path_closed(), Parma_Polyhedra_Library::BD_Shape< T >::Status::reset_shortest_path_reduced(), Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign(), Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_reduction_assign(), and Parma_Polyhedra_Library::BD_Shape< T >::status.
Referenced by Parma_Polyhedra_Library::BD_Shape< T >::add_constraint(), Parma_Polyhedra_Library::BD_Shape< T >::add_constraints(), Parma_Polyhedra_Library::BD_Shape< T >::add_dbm_constraint(), Parma_Polyhedra_Library::BD_Shape< T >::add_space_dimensions_and_embed(), Parma_Polyhedra_Library::BD_Shape< T >::add_space_dimensions_and_project(), Parma_Polyhedra_Library::BD_Shape< T >::affine_image(), Parma_Polyhedra_Library::BD_Shape< T >::affine_preimage(), Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape(), Parma_Polyhedra_Library::BD_Shape< T >::bds_difference_assign(), Parma_Polyhedra_Library::BD_Shape< T >::bds_hull_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 >::concatenate_assign(), Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_image(), Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_preimage(), Parma_Polyhedra_Library::BD_Shape< T >::H79_widening_assign(), Parma_Polyhedra_Library::BD_Shape< T >::intersection_assign(), Parma_Polyhedra_Library::BD_Shape< T >::limited_BHMZ05_extrapolation_assign(), Parma_Polyhedra_Library::BD_Shape< T >::limited_CC76_extrapolation_assign(), Parma_Polyhedra_Library::BD_Shape< T >::limited_H79_extrapolation_assign(), Parma_Polyhedra_Library::BD_Shape< T >::map_space_dimensions(), Parma_Polyhedra_Library::BD_Shape< T >::remove_higher_space_dimensions(), Parma_Polyhedra_Library::BD_Shape< T >::remove_space_dimensions(), Parma_Polyhedra_Library::BD_Shape< T >::set_empty(), and Parma_Polyhedra_Library::BD_Shape< T >::time_elapse_assign().
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 }
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
.
c | The constraint to be added. If it is not a bounded difference, it will be simply ignored. |
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.
References Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::BD_Shape< T >::div_round_up(), Parma_Polyhedra_Library::BD_Shape< T >::extract_bounded_difference(), Parma_Polyhedra_Library::Constraint::inhomogeneous_term(), Parma_Polyhedra_Library::Constraint::is_equality(), Parma_Polyhedra_Library::Constraint::is_strict_inequality(), 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 >::set_empty(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), Parma_Polyhedra_Library::Constraint::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::status, TEMP_INTEGER, Parma_Polyhedra_Library::BD_Shape< T >::throw_constraint_incompatible(), and Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible().
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 }
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
.
false
if and only if the result is empty.c | The constraint to be added. If it is not a bounded difference, it will be simply ignored. |
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 }
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
.
cs | The constraints that will be added. Constraints that are not bounded differences will be simply ignored. |
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 }
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
.
false
if and only if the result is empty.cs | The constraints that will be added. Constraints that are not bounded differences will be simply ignored. |
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 }
void Parma_Polyhedra_Library::BD_Shape< T >::intersection_assign | ( | const BD_Shape< T > & | y | ) | [inline] |
Assigns to *this
the intersection of *this
and y
.
std::invalid_argument | Thrown if *this and y are dimension-incompatible. |
Definition at line 1415 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 >::Status::reset_shortest_path_closed(), Parma_Polyhedra_Library::BD_Shape< T >::set_empty(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::status, and Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible().
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 }
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
.
false
if and only if the result is empty.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 }
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
.
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 }
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
.
false
if and only if the result is empty.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 }
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 }
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.
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().
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 }
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
.
std::invalid_argument | Thrown if *this and y are dimension-incompatible. |
Definition at line 1118 of file BD_Shape.templates.hh.
References Parma_Polyhedra_Library::BD_Shape< T >::add_constraint_and_minimize(), Parma_Polyhedra_Library::BD_Shape< T >::bds_hull_assign(), Parma_Polyhedra_Library::Constraint_System::begin(), Parma_Polyhedra_Library::BD_Shape< T >::constraints(), Parma_Polyhedra_Library::BD_Shape< T >::contains(), Parma_Polyhedra_Library::EMPTY, Parma_Polyhedra_Library::Constraint_System::end(), Parma_Polyhedra_Library::Poly_Con_Relation::implies(), Parma_Polyhedra_Library::Constraint::is_equality(), Parma_Polyhedra_Library::Poly_Con_Relation::is_included(), Parma_Polyhedra_Library::Constraint::is_nonstrict_inequality(), Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), Parma_Polyhedra_Library::BD_Shape< T >::OK(), Parma_Polyhedra_Library::BD_Shape< T >::relation_with(), Parma_Polyhedra_Library::BD_Shape< T >::set_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 >::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 }
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 }
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
.
var | The variable to which the affine expression is assigned. | |
expr | The numerator of the affine expression. | |
denominator | The denominator of the affine expression. |
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.
References Parma_Polyhedra_Library::BD_Shape< T >::add_dbm_constraint(), Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::Linear_Expression::coefficient(), Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::BD_Shape< T >::deduce_u_minus_v_bounds(), Parma_Polyhedra_Library::BD_Shape< T >::deduce_v_minus_u_bounds(), Parma_Polyhedra_Library::BD_Shape< T >::div_round_up(), Parma_Polyhedra_Library::BD_Shape< T >::forget_all_dbm_constraints(), Parma_Polyhedra_Library::BD_Shape< T >::forget_binary_dbm_constraints(), Parma_Polyhedra_Library::Variable::id(), Parma_Polyhedra_Library::Linear_Expression::inhomogeneous_term(), 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::neg_assign(), Parma_Polyhedra_Library::BD_Shape< T >::OK(), Parma_Polyhedra_Library::BD_Shape< T >::Status::reset_shortest_path_closed(), Parma_Polyhedra_Library::BD_Shape< T >::Status::reset_shortest_path_reduced(), Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign(), Parma_Polyhedra_Library::Linear_Expression::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::status, TEMP_INTEGER, Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible(), and Parma_Polyhedra_Library::BD_Shape< T >::throw_generic().
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 }
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
.
var | The variable to which the affine expression is substituted. | |
expr | The numerator of the affine expression. | |
denominator | The denominator of the affine expression. |
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.
References Parma_Polyhedra_Library::BD_Shape< T >::affine_image(), Parma_Polyhedra_Library::Linear_Expression::coefficient(), Parma_Polyhedra_Library::BD_Shape< T >::forget_all_dbm_constraints(), Parma_Polyhedra_Library::Variable::id(), Parma_Polyhedra_Library::Linear_Expression::inhomogeneous_term(), 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 >::shortest_path_closure_assign(), Parma_Polyhedra_Library::Linear_Expression::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::status, Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible(), and Parma_Polyhedra_Library::BD_Shape< T >::throw_generic().
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 }
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 , where
is the relation symbol encoded by
relsym
.
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. |
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.
References Parma_Polyhedra_Library::BD_Shape< T >::add_dbm_constraint(), Parma_Polyhedra_Library::BD_Shape< T >::affine_image(), Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::Linear_Expression::coefficient(), Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::BD_Shape< T >::deduce_u_minus_v_bounds(), Parma_Polyhedra_Library::BD_Shape< T >::deduce_v_minus_u_bounds(), Parma_Polyhedra_Library::BD_Shape< T >::div_round_up(), Parma_Polyhedra_Library::EQUAL, Parma_Polyhedra_Library::BD_Shape< T >::forget_all_dbm_constraints(), Parma_Polyhedra_Library::BD_Shape< T >::forget_binary_dbm_constraints(), Parma_Polyhedra_Library::GREATER_THAN, Parma_Polyhedra_Library::GREATER_THAN_OR_EQUAL, Parma_Polyhedra_Library::Variable::id(), Parma_Polyhedra_Library::Linear_Expression::inhomogeneous_term(), Parma_Polyhedra_Library::is_plus_infinity(), Parma_Polyhedra_Library::LESS_THAN, Parma_Polyhedra_Library::LESS_THAN_OR_EQUAL, Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), Parma_Polyhedra_Library::BD_Shape< T >::marked_shortest_path_reduced(), Parma_Polyhedra_Library::neg_assign(), Parma_Polyhedra_Library::BD_Shape< T >::OK(), Parma_Polyhedra_Library::PLUS_INFINITY, Parma_Polyhedra_Library::BD_Shape< T >::Status::reset_shortest_path_closed(), Parma_Polyhedra_Library::BD_Shape< T >::Status::reset_shortest_path_reduced(), Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign(), Parma_Polyhedra_Library::Linear_Expression::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::status, TEMP_INTEGER, Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible(), and Parma_Polyhedra_Library::BD_Shape< T >::throw_generic().
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 }
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 , where
is the relation symbol encoded by
relsym
.
lhs | The left hand side affine expression. | |
relsym | The relation symbol. | |
rhs | The right hand side affine expression. |
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.
References Parma_Polyhedra_Library::BD_Shape< T >::add_constraint(), Parma_Polyhedra_Library::BD_Shape< T >::add_space_dimensions_and_embed(), Parma_Polyhedra_Library::BD_Shape< T >::affine_image(), Parma_Polyhedra_Library::Linear_Expression::coefficient(), Parma_Polyhedra_Library::EQUAL, Parma_Polyhedra_Library::BD_Shape< T >::forget_all_dbm_constraints(), Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_image(), Parma_Polyhedra_Library::GREATER_THAN, Parma_Polyhedra_Library::GREATER_THAN_OR_EQUAL, Parma_Polyhedra_Library::Linear_Expression::inhomogeneous_term(), Parma_Polyhedra_Library::LESS_THAN, Parma_Polyhedra_Library::LESS_THAN_OR_EQUAL, Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), Parma_Polyhedra_Library::BD_Shape< T >::OK(), Parma_Polyhedra_Library::BD_Shape< T >::remove_higher_space_dimensions(), Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign(), Parma_Polyhedra_Library::Linear_Expression::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible(), and Parma_Polyhedra_Library::BD_Shape< T >::throw_generic().
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 }
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 , where
is the relation symbol encoded by
relsym
.
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. |
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.
References Parma_Polyhedra_Library::BD_Shape< T >::add_dbm_constraint(), Parma_Polyhedra_Library::BD_Shape< T >::affine_preimage(), Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::Linear_Expression::coefficient(), Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::BD_Shape< T >::deduce_u_minus_v_bounds(), Parma_Polyhedra_Library::BD_Shape< T >::deduce_v_minus_u_bounds(), Parma_Polyhedra_Library::BD_Shape< T >::div_round_up(), Parma_Polyhedra_Library::EQUAL, Parma_Polyhedra_Library::BD_Shape< T >::forget_all_dbm_constraints(), Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_image(), Parma_Polyhedra_Library::GREATER_THAN, Parma_Polyhedra_Library::GREATER_THAN_OR_EQUAL, Parma_Polyhedra_Library::Variable::id(), Parma_Polyhedra_Library::Linear_Expression::inhomogeneous_term(), Parma_Polyhedra_Library::BD_Shape< T >::is_empty(), Parma_Polyhedra_Library::is_plus_infinity(), Parma_Polyhedra_Library::LESS_THAN, Parma_Polyhedra_Library::LESS_THAN_OR_EQUAL, Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), Parma_Polyhedra_Library::BD_Shape< T >::marked_shortest_path_reduced(), Parma_Polyhedra_Library::neg_assign(), Parma_Polyhedra_Library::BD_Shape< T >::OK(), Parma_Polyhedra_Library::BD_Shape< T >::Status::reset_shortest_path_reduced(), Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign(), Parma_Polyhedra_Library::Linear_Expression::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::status, TEMP_INTEGER, Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible(), and Parma_Polyhedra_Library::BD_Shape< T >::throw_generic().
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 }
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
.
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 }
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
.
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). |
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 }
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
.
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). |
std::invalid_argument | Thrown if *this and y are dimension-incompatible. |
Definition at line 1461 of file BD_Shape.templates.hh.
References Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::BD_Shape< T >::CC76_extrapolation_assign(), Parma_Polyhedra_Library::BD_Shape< T >::contains(), Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), Parma_Polyhedra_Library::BD_Shape< T >::OK(), Parma_Polyhedra_Library::PLUS_INFINITY, Parma_Polyhedra_Library::BD_Shape< T >::Status::reset_shortest_path_closed(), Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::status, and Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible().
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 }
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
.
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). |
std::invalid_argument | Thrown if *this and y are dimension-incompatible. |
Definition at line 1641 of file BD_Shape.templates.hh.
References Parma_Polyhedra_Library::BD_Shape< T >::affine_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::BHMZ05_widening_assign(), Parma_Polyhedra_Library::BD_Shape< T >::contains(), 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::PLUS_INFINITY, Parma_Polyhedra_Library::BD_Shape< T >::redundancy_dbm, Parma_Polyhedra_Library::BD_Shape< T >::Status::reset_shortest_path_closed(), Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_reduction_assign(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::status, and Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible().
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 }
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
.
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). |
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.
References Parma_Polyhedra_Library::BD_Shape< T >::BHMZ05_widening_assign(), Parma_Polyhedra_Library::BD_Shape< T >::contains(), Parma_Polyhedra_Library::BD_Shape< T >::get_limiting_shape(), Parma_Polyhedra_Library::Constraint_System::has_strict_inequalities(), Parma_Polyhedra_Library::BD_Shape< T >::intersection_assign(), Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), Parma_Polyhedra_Library::BD_Shape< T >::OK(), Parma_Polyhedra_Library::Constraint_System::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::throw_constraint_incompatible(), Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible(), and Parma_Polyhedra_Library::UNIVERSE.
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 }
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.
y | A BDS that must contain *this . |
std::invalid_argument | Thrown if *this and y are dimension-incompatible. |
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 Definition at line 1762 of file BD_Shape.templates.hh.
References Parma_Polyhedra_Library::BD_Shape< T >::contains(), 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_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 >::shortest_path_closure_assign(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::status, and Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible().
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 }
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
.
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). |
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.
References Parma_Polyhedra_Library::BD_Shape< T >::CC76_extrapolation_assign(), Parma_Polyhedra_Library::BD_Shape< T >::contains(), Parma_Polyhedra_Library::BD_Shape< T >::get_limiting_shape(), Parma_Polyhedra_Library::Constraint_System::has_strict_inequalities(), Parma_Polyhedra_Library::BD_Shape< T >::intersection_assign(), Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), Parma_Polyhedra_Library::BD_Shape< T >::OK(), Parma_Polyhedra_Library::Constraint_System::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::throw_constraint_incompatible(), Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible(), and Parma_Polyhedra_Library::UNIVERSE.
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 }
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
.
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). |
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 }
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
.
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). |
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 }
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.
m | The number of dimensions to add. |
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 }
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.
m | The number of dimensions to add. |
Definition at line 1221 of file BD_Shape.templates.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::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 >::Status::set_shortest_path_closed(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), and Parma_Polyhedra_Library::BD_Shape< T >::status.
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 }
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 and
be the BDSs corresponding, on entry, to
*this
and y
, respectively. Upon successful completion, *this
will represent the BDS such that
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.
References Parma_Polyhedra_Library::BD_Shape< T >::add_space_dimensions_and_embed(), 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 >::Status::reset_shortest_path_closed(), Parma_Polyhedra_Library::BD_Shape< T >::set_empty(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), and Parma_Polyhedra_Library::BD_Shape< T >::status.
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 }
void Parma_Polyhedra_Library::BD_Shape< T >::remove_space_dimensions | ( | const Variables_Set & | to_be_removed | ) | [inline] |
Removes all the specified dimensions.
to_be_removed | The set of Variable objects corresponding to the dimensions to be removed. |
std::invalid_argument | Thrown if *this is dimension-incompatible with one of the Variable objects contained in to_be_removed . |
Definition at line 1267 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 >::set_zero_dim_univ(), Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::status, and Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible().
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 }
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
.
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.
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 >::set_zero_dim_univ(), Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::status, and Parma_Polyhedra_Library::BD_Shape< T >::throw_dimension_incompatible().
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 }
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.
pfunc | The partial function specifying the destiny of each dimension. |
bool has_empty_codomain() const
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
bool maps(dimension_type i, dimension_type& j) const
i
. If j
and true
is returned. If 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.
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 >::remove_higher_space_dimensions(), Parma_Polyhedra_Library::BD_Shape< T >::Status::reset_shortest_path_reduced(), 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 >::status.
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 }
void Parma_Polyhedra_Library::BD_Shape< T >::ascii_dump | ( | ) | const |
Writes to std::cerr
an ASCII representation of *this
.
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 }
void Parma_Polyhedra_Library::BD_Shape< T >::print | ( | ) | const |
Prints *this
to std::cerr
using operator<<
.
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 }
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().
Referenced by Parma_Polyhedra_Library::BD_Shape< T >::add_constraint_and_minimize(), Parma_Polyhedra_Library::BD_Shape< T >::add_constraints_and_minimize(), Parma_Polyhedra_Library::BD_Shape< T >::add_space_dimensions_and_embed(), Parma_Polyhedra_Library::BD_Shape< T >::add_space_dimensions_and_project(), Parma_Polyhedra_Library::BD_Shape< T >::affine_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::affine_image(), Parma_Polyhedra_Library::BD_Shape< T >::affine_preimage(), Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape(), Parma_Polyhedra_Library::BD_Shape< T >::bds_difference_assign(), Parma_Polyhedra_Library::BD_Shape< T >::bds_hull_assign(), Parma_Polyhedra_Library::BD_Shape< T >::bds_hull_assign_and_minimize(), Parma_Polyhedra_Library::BD_Shape< T >::CC76_extrapolation_assign(), Parma_Polyhedra_Library::BD_Shape< T >::CC76_narrowing_assign(), Parma_Polyhedra_Library::BD_Shape< T >::compute_leaders(), Parma_Polyhedra_Library::BD_Shape< T >::compute_predecessors(), Parma_Polyhedra_Library::BD_Shape< T >::concatenate_assign(), Parma_Polyhedra_Library::BD_Shape< T >::constraints(), Parma_Polyhedra_Library::BD_Shape< T >::contains(), Parma_Polyhedra_Library::BD_Shape< T >::euclidean_distance_assign(), Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_image(), Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_preimage(), Parma_Polyhedra_Library::BD_Shape< T >::intersection_assign(), Parma_Polyhedra_Library::BD_Shape< T >::intersection_assign_and_minimize(), Parma_Polyhedra_Library::BD_Shape< T >::is_empty(), Parma_Polyhedra_Library::BD_Shape< T >::is_shortest_path_reduced(), Parma_Polyhedra_Library::BD_Shape< T >::is_universe(), Parma_Polyhedra_Library::BD_Shape< T >::l_infinity_distance_assign(), Parma_Polyhedra_Library::BD_Shape< T >::limited_BHMZ05_extrapolation_assign(), Parma_Polyhedra_Library::BD_Shape< T >::limited_CC76_extrapolation_assign(), Parma_Polyhedra_Library::BD_Shape< T >::map_space_dimensions(), Parma_Polyhedra_Library::BD_Shape< T >::minimized_constraints(), Parma_Polyhedra_Library::BD_Shape< T >::OK(), Parma_Polyhedra_Library::operator==(), Parma_Polyhedra_Library::BD_Shape< T >::rectilinear_distance_assign(), Parma_Polyhedra_Library::BD_Shape< T >::relation_with(), Parma_Polyhedra_Library::BD_Shape< T >::remove_higher_space_dimensions(), Parma_Polyhedra_Library::BD_Shape< T >::remove_space_dimensions(), Parma_Polyhedra_Library::BD_Shape< T >::set_empty(), Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign(), and Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_reduction_assign().
00112 { 00113 return status.test_empty(); 00114 }
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().
Referenced by Parma_Polyhedra_Library::BD_Shape< T >::add_constraint(), Parma_Polyhedra_Library::BD_Shape< T >::add_dbm_constraint(), Parma_Polyhedra_Library::BD_Shape< T >::add_space_dimensions_and_project(), Parma_Polyhedra_Library::BD_Shape< T >::bds_hull_assign(), Parma_Polyhedra_Library::BD_Shape< T >::bds_hull_assign_and_minimize(), Parma_Polyhedra_Library::BD_Shape< T >::BHMZ05_widening_assign(), Parma_Polyhedra_Library::BD_Shape< T >::CC76_narrowing_assign(), Parma_Polyhedra_Library::BD_Shape< T >::compute_leaders(), Parma_Polyhedra_Library::BD_Shape< T >::compute_predecessors(), Parma_Polyhedra_Library::BD_Shape< T >::concatenate_assign(), Parma_Polyhedra_Library::BD_Shape< T >::get_limiting_shape(), Parma_Polyhedra_Library::BD_Shape< T >::intersection_assign(), Parma_Polyhedra_Library::BD_Shape< T >::OK(), and Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign().
00132 { 00133 return status.test_shortest_path_closed(); 00134 }
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().
Referenced by Parma_Polyhedra_Library::BD_Shape< T >::add_space_dimensions_and_embed(), Parma_Polyhedra_Library::BD_Shape< T >::affine_image(), Parma_Polyhedra_Library::BD_Shape< T >::affine_preimage(), Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape(), Parma_Polyhedra_Library::BD_Shape< T >::constraints(), Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_image(), Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_preimage(), Parma_Polyhedra_Library::BD_Shape< T >::is_shortest_path_reduced(), Parma_Polyhedra_Library::BD_Shape< T >::map_space_dimensions(), Parma_Polyhedra_Library::BD_Shape< T >::OK(), Parma_Polyhedra_Library::BD_Shape< T >::operator=(), Parma_Polyhedra_Library::BD_Shape< T >::remove_higher_space_dimensions(), Parma_Polyhedra_Library::BD_Shape< T >::remove_space_dimensions(), and Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_reduction_assign().
00138 { 00139 return status.test_shortest_path_reduced(); 00140 }
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 }
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 }
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.
References Parma_Polyhedra_Library::assign_r(), 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_closed(), Parma_Polyhedra_Library::BD_Shape< T >::min_assign(), Parma_Polyhedra_Library::PLUS_INFINITY, Parma_Polyhedra_Library::BD_Shape< T >::Status::set_empty(), 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 >::add_constraint_and_minimize(), Parma_Polyhedra_Library::BD_Shape< T >::add_constraints_and_minimize(), Parma_Polyhedra_Library::BD_Shape< T >::affine_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::affine_image(), Parma_Polyhedra_Library::BD_Shape< T >::affine_preimage(), Parma_Polyhedra_Library::BD_Shape< T >::bds_difference_assign(), Parma_Polyhedra_Library::BD_Shape< T >::bds_hull_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 >::contains(), Parma_Polyhedra_Library::BD_Shape< T >::euclidean_distance_assign(), Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_image(), Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_preimage(), Parma_Polyhedra_Library::BD_Shape< T >::intersection_assign_and_minimize(), Parma_Polyhedra_Library::BD_Shape< T >::is_empty(), Parma_Polyhedra_Library::BD_Shape< T >::is_shortest_path_reduced(), Parma_Polyhedra_Library::BD_Shape< T >::l_infinity_distance_assign(), Parma_Polyhedra_Library::BD_Shape< T >::map_space_dimensions(), Parma_Polyhedra_Library::BD_Shape< T >::OK(), Parma_Polyhedra_Library::operator==(), Parma_Polyhedra_Library::BD_Shape< T >::rectilinear_distance_assign(), Parma_Polyhedra_Library::BD_Shape< T >::relation_with(), Parma_Polyhedra_Library::BD_Shape< T >::remove_higher_space_dimensions(), Parma_Polyhedra_Library::BD_Shape< T >::remove_space_dimensions(), and Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_reduction_assign().
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 }
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.
References Parma_Polyhedra_Library::BD_Shape< T >::compute_leader_indices(), Parma_Polyhedra_Library::BD_Shape< T >::compute_predecessors(), Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::BD_Shape< T >::is_shortest_path_reduced(), 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 >::Status::set_shortest_path_reduced(), 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 >::status.
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 }
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 }
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 }
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 }
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 }
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 }
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:
q >= 1
, then v - u <= ub_v - ub_u
;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 }
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:
q >= 1
, then u - v <= lb_u - lb_v
;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 }
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.
References Parma_Polyhedra_Library::Constraint_System::begin(), Parma_Polyhedra_Library::BD_Shape< T >::dbm, Parma_Polyhedra_Library::BD_Shape< T >::div_round_up(), Parma_Polyhedra_Library::Constraint_System::end(), Parma_Polyhedra_Library::BD_Shape< T >::extract_bounded_difference(), Parma_Polyhedra_Library::Constraint::inhomogeneous_term(), Parma_Polyhedra_Library::Constraint::is_inequality(), Parma_Polyhedra_Library::BD_Shape< T >::marked_shortest_path_closed(), Parma_Polyhedra_Library::BD_Shape< T >::Status::reset_shortest_path_closed(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), Parma_Polyhedra_Library::Constraint_System::space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::status, and TEMP_INTEGER.
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 }
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 }
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 }
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().
Referenced by Parma_Polyhedra_Library::BD_Shape< T >::add_constraint(), Parma_Polyhedra_Library::BD_Shape< T >::affine_image(), Parma_Polyhedra_Library::BD_Shape< T >::affine_preimage(), Parma_Polyhedra_Library::BD_Shape< T >::bds_difference_assign(), Parma_Polyhedra_Library::BD_Shape< T >::bds_hull_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 >::contains(), Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_image(), Parma_Polyhedra_Library::BD_Shape< T >::generalized_affine_preimage(), Parma_Polyhedra_Library::BD_Shape< T >::intersection_assign(), Parma_Polyhedra_Library::BD_Shape< T >::limited_BHMZ05_extrapolation_assign(), Parma_Polyhedra_Library::BD_Shape< T >::limited_CC76_extrapolation_assign(), Parma_Polyhedra_Library::BD_Shape< T >::relation_with(), Parma_Polyhedra_Library::BD_Shape< T >::remove_higher_space_dimensions(), Parma_Polyhedra_Library::BD_Shape< T >::remove_space_dimensions(), and Parma_Polyhedra_Library::BD_Shape< T >::time_elapse_assign().
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 }
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 }
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 }
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 }
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 }
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 }
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 }
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 }
friend class Parma_Polyhedra_Library::BD_Shape [friend] |
Definition at line 1151 of file BD_Shape.defs.hh.
bool Parma_Polyhedra_Library::operator== | ( | const BD_Shape< T > & | x, | |
const BD_Shape< T > & | y | |||
) | [friend] |
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] |
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] |
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] |
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 }
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 }
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.
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 }
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 }
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 }
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 }
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 distance between
x
and y
.
If the 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 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 }
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 distance between
x
and y
.
If the 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 }
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 }
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 }
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 }
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().
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().
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 }
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 }
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.
Referenced by Parma_Polyhedra_Library::BD_Shape< T >::add_constraint(), Parma_Polyhedra_Library::BD_Shape< T >::add_dbm_constraint(), Parma_Polyhedra_Library::BD_Shape< T >::add_space_dimensions_and_embed(), Parma_Polyhedra_Library::BD_Shape< T >::add_space_dimensions_and_project(), Parma_Polyhedra_Library::BD_Shape< T >::affine_image(), Parma_Polyhedra_Library::BD_Shape< T >::ascii_dump(), Parma_Polyhedra_Library::BD_Shape< T >::ascii_load(), Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape(), Parma_Polyhedra_Library::BD_Shape< T >::bds_hull_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 >::compute_predecessors(), Parma_Polyhedra_Library::BD_Shape< T >::concatenate_assign(), Parma_Polyhedra_Library::BD_Shape< T >::constraints(), Parma_Polyhedra_Library::BD_Shape< T >::contains(), Parma_Polyhedra_Library::BD_Shape< T >::deduce_u_minus_v_bounds(), Parma_Polyhedra_Library::BD_Shape< T >::deduce_v_minus_u_bounds(), Parma_Polyhedra_Library::BD_Shape< T >::euclidean_distance_assign(), Parma_Polyhedra_Library::BD_Shape< T >::forget_all_dbm_constraints(), Parma_Polyhedra_Library::BD_Shape< T >::forget_binary_dbm_constraints(), 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(), Parma_Polyhedra_Library::BD_Shape< T >::intersection_assign(), Parma_Polyhedra_Library::BD_Shape< T >::is_shortest_path_reduced(), Parma_Polyhedra_Library::BD_Shape< T >::is_universe(), Parma_Polyhedra_Library::BD_Shape< T >::l_infinity_distance_assign(), Parma_Polyhedra_Library::BD_Shape< T >::map_space_dimensions(), Parma_Polyhedra_Library::BD_Shape< T >::minimized_constraints(), Parma_Polyhedra_Library::BD_Shape< T >::OK(), Parma_Polyhedra_Library::BD_Shape< T >::operator=(), Parma_Polyhedra_Library::operator==(), Parma_Polyhedra_Library::BD_Shape< T >::rectilinear_distance_assign(), Parma_Polyhedra_Library::BD_Shape< T >::relation_with(), Parma_Polyhedra_Library::BD_Shape< T >::remove_higher_space_dimensions(), Parma_Polyhedra_Library::BD_Shape< T >::remove_space_dimensions(), Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign(), Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_reduction_assign(), Parma_Polyhedra_Library::BD_Shape< T >::space_dimension(), and Parma_Polyhedra_Library::BD_Shape< T >::swap().
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.
Referenced by Parma_Polyhedra_Library::BD_Shape< T >::add_constraint(), Parma_Polyhedra_Library::BD_Shape< T >::add_dbm_constraint(), Parma_Polyhedra_Library::BD_Shape< T >::add_space_dimensions_and_embed(), Parma_Polyhedra_Library::BD_Shape< T >::add_space_dimensions_and_project(), Parma_Polyhedra_Library::BD_Shape< T >::affine_image(), Parma_Polyhedra_Library::BD_Shape< T >::affine_preimage(), Parma_Polyhedra_Library::BD_Shape< T >::ascii_dump(), Parma_Polyhedra_Library::BD_Shape< T >::ascii_load(), Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape(), 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 >::concatenate_assign(), 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(), Parma_Polyhedra_Library::BD_Shape< T >::intersection_assign(), Parma_Polyhedra_Library::BD_Shape< T >::map_space_dimensions(), Parma_Polyhedra_Library::BD_Shape< T >::marked_empty(), Parma_Polyhedra_Library::BD_Shape< T >::marked_shortest_path_closed(), Parma_Polyhedra_Library::BD_Shape< T >::marked_shortest_path_reduced(), Parma_Polyhedra_Library::BD_Shape< T >::OK(), Parma_Polyhedra_Library::BD_Shape< T >::operator=(), Parma_Polyhedra_Library::BD_Shape< T >::remove_higher_space_dimensions(), Parma_Polyhedra_Library::BD_Shape< T >::remove_space_dimensions(), Parma_Polyhedra_Library::BD_Shape< T >::set_empty(), Parma_Polyhedra_Library::BD_Shape< T >::set_zero_dim_univ(), Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign(), Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_reduction_assign(), and Parma_Polyhedra_Library::BD_Shape< T >::swap().
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.
Referenced by Parma_Polyhedra_Library::BD_Shape< T >::ascii_dump(), Parma_Polyhedra_Library::BD_Shape< T >::ascii_load(), Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape(), Parma_Polyhedra_Library::BD_Shape< T >::BHMZ05_widening_assign(), Parma_Polyhedra_Library::BD_Shape< T >::is_shortest_path_reduced(), Parma_Polyhedra_Library::BD_Shape< T >::minimized_constraints(), Parma_Polyhedra_Library::BD_Shape< T >::OK(), Parma_Polyhedra_Library::BD_Shape< T >::operator=(), Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_reduction_assign(), and Parma_Polyhedra_Library::BD_Shape< T >::swap().