#include <Box.defs.hh>
Exception Throwers | |
void | throw_dimension_incompatible (const char *method, const Box &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 Congruence &cg) const |
void | throw_dimension_incompatible (const char *method, const Constraint_System &cs) const |
void | throw_dimension_incompatible (const char *method, const Congruence_System &cgs) 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_space_dimension_overflow (const char *method, const char *reason) |
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 ITV | interval_type |
The type of intervals used to implement the box. | |
Public Member Functions | |
const ITV & | get_interval (Variable var) const |
Returns a reference the interval that bounds var . | |
void | set_interval (Variable var, const ITV &i) |
Sets to i the interval that bounds var . | |
bool | get_lower_bound (dimension_type k, bool &closed, Coefficient &n, Coefficient &d) const |
If the k -th space dimension is unbounded below, returns false . Otherwise returns true and set closed , n and d accordingly. | |
bool | get_upper_bound (dimension_type k, bool &closed, Coefficient &n, Coefficient &d) const |
If the k -th space dimension is unbounded above, returns false . Otherwise returns true and set closed , n and d accordingly. | |
Constraint_System | constraints () const |
Returns a system of constraints defining *this . | |
Constraint_System | minimized_constraints () const |
Returns a minimized system of constraints defining *this . | |
Congruence_System | congruences () const |
Returns a system of congruences approximating *this . | |
Congruence_System | minimized_congruences () const |
Returns a minimized system of congruences approximating *this . | |
memory_size_type | total_memory_in_bytes () const |
Returns the total size in bytes of the memory occupied by *this . | |
memory_size_type | external_memory_in_bytes () const |
Returns the size in bytes of the memory managed by *this . | |
void | ascii_dump () const |
Writes to std::cerr an ASCII representation of *this . | |
void | ascii_dump (std::ostream &s) const |
Writes to s an ASCII representation of *this . | |
void | print () const |
Prints *this to std::cerr using operator<< . | |
bool | ascii_load (std::istream &s) |
Loads from s an ASCII representation (as produced by ascii_dump(std::ostream&) const) and sets *this accordingly. Returns true if successful, false otherwise. | |
void | set_empty () |
Causes the box to become empty, i.e., to represent the empty set. | |
Constructors, Assignment, Swap and Destructor | |
Box (dimension_type num_dimensions=0, Degenerate_Element kind=UNIVERSE) | |
Builds a universe or empty box of the specified space dimension. | |
Box (const Box &y, Complexity_Class complexity=ANY_COMPLEXITY) | |
Ordinary copy-constructor. | |
template<typename Other_ITV> | |
Box (const Box< Other_ITV > &y, Complexity_Class complexity=ANY_COMPLEXITY) | |
Builds a conservative, upward approximation of y . | |
Box (const Constraint_System &cs) | |
Builds a box from the system of constraints cs . | |
Box (const Constraint_System &cs, Recycle_Input dummy) | |
Builds a box recycling a system of constraints cs . | |
Box (const Generator_System &gs) | |
Builds a box from the system of generators gs . | |
Box (const Generator_System &gs, Recycle_Input dummy) | |
Builds a box recycling the system of generators gs . | |
Box (const Congruence_System &cgs) | |
Box (const Congruence_System &cgs, Recycle_Input dummy) | |
template<typename T> | |
Box (const BD_Shape< T > &bds, Complexity_Class complexity=POLYNOMIAL_COMPLEXITY) | |
Builds a box containing the BDS bds . | |
template<typename T> | |
Box (const Octagonal_Shape< T > &oct, Complexity_Class complexity=POLYNOMIAL_COMPLEXITY) | |
Builds a box containing the octagonal shape oct . | |
Box (const Polyhedron &ph, Complexity_Class complexity=ANY_COMPLEXITY) | |
Builds a box containing the polyhedron ph . | |
Box (const Grid &ph, Complexity_Class complexity=POLYNOMIAL_COMPLEXITY) | |
Builds a box containing the grid gr . | |
template<typename D1, typename D2, typename R> | |
Box (const Partially_Reduced_Product< D1, D2, R > &dp, Complexity_Class complexity=ANY_COMPLEXITY) | |
Builds a box containing the partially reduced product dp . | |
Box & | operator= (const Box &y) |
The assignment operator (*this and y can be dimension-incompatible). | |
void | swap (Box &y) |
Swaps *this with y (*this and y can be dimension-incompatible). | |
Member Functions that Do Not Modify the Box | |
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 . | |
bool | is_empty () const |
Returns true if and only if *this is an empty box. | |
bool | is_universe () const |
Returns true if and only if *this is a universe box. | |
bool | is_topologically_closed () const |
Returns true if and only if *this is a topologically closed subset of the vector space. | |
bool | is_discrete () const |
Returns true if and only if *this is discrete. | |
bool | is_bounded () const |
Returns true if and only if *this is a bounded box. | |
bool | contains_integer_point () const |
Returns true if and only if *this contains at least one integer point. | |
bool | constrains (Variable var) const |
Returns true if and only if var is constrained in *this . | |
Poly_Con_Relation | relation_with (const Constraint &c) const |
Returns the relations holding between *this and the constraint c . | |
Poly_Con_Relation | relation_with (const Congruence &cg) const |
Returns the relations holding between *this and the congruence cg . | |
Poly_Gen_Relation | relation_with (const Generator &g) const |
Returns the relations holding between *this and the generator g . | |
bool | bounds_from_above (const Linear_Expression &expr) const |
Returns true if and only if expr is bounded from above in *this . | |
bool | bounds_from_below (const Linear_Expression &expr) const |
Returns true if and only if expr is bounded from below in *this . | |
bool | maximize (const Linear_Expression &expr, Coefficient &sup_n, Coefficient &sup_d, bool &maximum) const |
Returns true if and only if *this is not empty and expr is bounded from above in *this , in which case the supremum value is computed. | |
bool | maximize (const Linear_Expression &expr, Coefficient &sup_n, Coefficient &sup_d, bool &maximum, Generator &g) const |
Returns true if and only if *this is not empty and expr is bounded from above in *this , in which case the supremum value and a point where expr reaches it are computed. | |
bool | minimize (const Linear_Expression &expr, Coefficient &inf_n, Coefficient &inf_d, bool &minimum) const |
Returns true if and only if *this is not empty and expr is bounded from below in *this , in which case the infimum value is computed. | |
bool | minimize (const Linear_Expression &expr, Coefficient &inf_n, Coefficient &inf_d, bool &minimum, Generator &g) const |
Returns true if and only if *this is not empty and expr is bounded from below in *this , in which case the infimum value and a point where expr reaches it are computed. | |
bool | contains (const Box &) const |
Returns true if and only if *this contains y . | |
bool | strictly_contains (const Box &) const |
Returns true if and only if *this strictly contains y . | |
bool | is_disjoint_from (const Box &y) const |
Returns true if and only if *this and y are disjoint. | |
bool | OK () const |
Returns true if and only if *this satisfies all its invariants. | |
Space-Dimension Preserving Member Functions that May Modify the Box | |
void | add_constraint (const Constraint &c) |
Use the constraint c to refine *this . FIXME: this is not true. | |
void | add_constraints (const Constraint_System &cs) |
Use the constraints in cs to refine *this . FIXME: this is not true. | |
void | add_recycled_constraints (Constraint_System &cs) |
Use the constraints in cs to refine *this . FIXME: this is not true. | |
void | add_congruence (const Congruence &cg) |
Use the congruence cg to refine *this . | |
void | add_congruences (const Congruence_System &cgs) |
Use the congruences in cgs to refine *this . | |
void | add_recycled_congruences (Congruence_System &cgs) |
Use the congruences in cgs to refine *this . | |
void | refine_with_constraint (const Constraint &c) |
Use the constraint c to refine *this . | |
void | refine_with_constraints (const Constraint_System &cs) |
Use the constraints in cs to refine *this . | |
void | refine_with_congruence (const Congruence &cg) |
Use the congruence cg to refine *this . | |
void | refine_with_congruences (const Congruence_System &cgs) |
Use the congruences in cgs to refine *this . | |
void | propagate_constraint (const Constraint &c) |
Use the constraint c for constraint propagation on *this . | |
void | propagate_constraints (const Constraint_System &cs) |
Use the constraints in cs for constraint propagagion on *this . | |
void | unconstrain (Variable var) |
Computes the cylindrification of *this with respect to space dimension var , assigning the result to *this . | |
void | unconstrain (const Variables_Set &to_be_unconstrained) |
Computes the cylindrification of *this with respect to the set of space dimensions to_be_unconstrained , assigning the result to *this . | |
void | intersection_assign (const Box &y) |
Assigns to *this the intersection of *this and y . | |
void | upper_bound_assign (const Box &y) |
Assigns to *this the smallest box containing the union of *this and y . | |
bool | upper_bound_assign_if_exact (const Box &y) |
If the upper bound of *this and y is exact, it is assigned to *this and true is returned, otherwise false is returned. | |
void | difference_assign (const Box &y) |
Assigns to *this the difference of *this and y . | |
bool | simplify_using_context_assign (const Box &y) |
Assigns to *this a meet-preserving simplification of *this with respect to y . If false is returned, then the intersection is empty. | |
void | affine_image (Variable var, const Linear_Expression &expr, Coefficient_traits::const_reference denominator=Coefficient_one()) |
Assigns to *this the affine image of *this under the function mapping variable var to the affine expression specified by expr and denominator . | |
void | affine_preimage (Variable var, const Linear_Expression &expr, Coefficient_traits::const_reference denominator=Coefficient_one()) |
Assigns to *this the affine preimage of *this under the function mapping variable var to the affine expression specified by expr and denominator . | |
void | generalized_affine_image (Variable var, Relation_Symbol relsym, const Linear_Expression &expr, Coefficient_traits::const_reference denominator=Coefficient_one()) |
Assigns to *this the image of *this with respect to the generalized affine relation ![]() ![]() relsym . | |
void | generalized_affine_preimage (Variable var, Relation_Symbol relsym, const Linear_Expression &expr, Coefficient_traits::const_reference denominator=Coefficient_one()) |
Assigns to *this the preimage of *this with respect to the generalized affine relation ![]() ![]() relsym . | |
void | generalized_affine_image (const Linear_Expression &lhs, Relation_Symbol relsym, const Linear_Expression &rhs) |
Assigns to *this the image of *this with respect to the generalized affine relation ![]() ![]() relsym . | |
void | generalized_affine_preimage (const Linear_Expression &lhs, Relation_Symbol relsym, const Linear_Expression &rhs) |
Assigns to *this the preimage of *this with respect to the generalized affine relation ![]() ![]() relsym . | |
void | bounded_affine_image (Variable var, const Linear_Expression &lb_expr, const Linear_Expression &ub_expr, Coefficient_traits::const_reference denominator=Coefficient_one()) |
Assigns to *this the image of *this with respect to the bounded affine relation ![]() | |
void | bounded_affine_preimage (Variable var, const Linear_Expression &lb_expr, const Linear_Expression &ub_expr, Coefficient_traits::const_reference denominator=Coefficient_one()) |
Assigns to *this the preimage of *this with respect to the bounded affine relation ![]() | |
void | time_elapse_assign (const Box &y) |
Assigns to *this the result of computing the time-elapse between *this and y . | |
void | topological_closure_assign () |
Assigns to *this its topological closure. | |
void | CC76_widening_assign (const Box &y, unsigned *tp=0) |
Assigns to *this the result of computing the CC76-widening between *this and y . | |
template<typename Iterator> | |
void | CC76_widening_assign (const Box &y, Iterator first, Iterator last) |
Assigns to *this the result of computing the CC76-widening between *this and y . | |
void | widening_assign (const Box &y, unsigned *tp=0) |
Same as CC76_widening_assign(y, tp). | |
void | limited_CC76_extrapolation_assign (const Box &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 | CC76_narrowing_assign (const Box &y) |
Assigns to *this the result of restoring in y the constraints of *this that were lost by CC76-extrapolation applications. | |
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 box into the new space. | |
void | add_space_dimensions_and_project (dimension_type m) |
Adds m new dimensions to the box and does not embed it in the new vector space. | |
void | concatenate_assign (const Box &y) |
Seeing a box 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 Partial_Function> | |
void | map_space_dimensions (const Partial_Function &pfunc) |
Remaps the dimensions of the vector space according to a partial function. | |
void | expand_space_dimension (Variable var, dimension_type m) |
Creates m copies of the space dimension corresponding to var . | |
void | fold_space_dimensions (const Variables_Set &to_be_folded, Variable var) |
Folds the space dimensions in to_be_folded into var . | |
Static Public Member Functions | |
static dimension_type | max_space_dimension () |
Returns the maximum space dimension that a Box can handle. | |
static bool | can_recycle_constraint_systems () |
Returns false indicating that this domain does not recycle constraints. | |
static bool | can_recycle_congruence_systems () |
Returns false indicating that this domain does not recycle congruences. | |
Private Types | |
typedef std::vector< ITV > | Sequence |
The type of sequence used to implement the box. | |
typedef ITV | Tmp_Interval_Type |
The type of intervals used by inner computations when trying to limit the cumulative effect of approximation errors. | |
Private Member Functions | |
bool | marked_empty () const |
Returns true if and only if the box is known to be empty. | |
void | set_nonempty () |
Marks *this as definitely not empty. | |
void | set_empty_up_to_date () |
Asserts the validity of the empty flag of *this . | |
void | reset_empty_up_to_date () |
Invalidates empty flag of *this . | |
bool | check_empty () const |
Checks the hard way whether *this is an empty box: returns true if and only if it is so. | |
const ITV & | operator[] (dimension_type k) const |
Returns a reference the interval that bounds the box on the k -th space dimension. | |
void | add_interval_constraint_no_check (dimension_type var_id, Constraint::Type type, Coefficient_traits::const_reference num, Coefficient_traits::const_reference den) |
WRITE ME. | |
void | add_constraint_no_check (const Constraint &c) |
WRITE ME. | |
void | add_constraints_no_check (const Constraint_System &cs) |
WRITE ME. | |
void | add_congruence_no_check (const Congruence &cg) |
WRITE ME. | |
void | add_congruences_no_check (const Congruence_System &cgs) |
WRITE ME. | |
void | refine_no_check (const Constraint &c) |
Uses the constraint c to refine *this . | |
void | refine_no_check (const Constraint_System &cs) |
Uses the constraints in cs to refine *this . | |
void | refine_no_check (const Congruence &cg) |
Uses the congruence cg to refine *this . | |
void | refine_no_check (const Congruence_System &cgs) |
Uses the congruences in cgs to refine *this . | |
void | propagate_constraint_no_check (const Constraint &c) |
Propagates the constraint c to refine *this . | |
void | propagate_constraints_no_check (const Constraint_System &cs) |
Propagates the constraints in cs to refine *this . | |
bool | bounds (const Linear_Expression &expr, bool from_above) const |
Checks if and how expr is bounded in *this . | |
bool | max_min (const Linear_Expression &expr, bool maximize, Coefficient &ext_n, Coefficient &ext_d, bool &included, Generator &g) const |
Maximizes or minimizes expr subject to *this . | |
bool | max_min (const Linear_Expression &expr, bool maximize, Coefficient &ext_n, Coefficient &ext_d, bool &included) const |
Maximizes or minimizes expr subject to *this . | |
Private Attributes | |
Sequence | seq |
A sequence of intervals, one for each dimension of the vector space. | |
Status | status |
The status flags to keep track of the internal state. | |
Friends | |
class | Parma_Polyhedra_Library::Box |
bool | operator== (const Box< ITV > &x, const Box< ITV > &y) |
Returns true if and only if x and y are the same box. | |
std::ostream & | operator<< (std::ostream &s, const Box< ITV > &box) |
Output operator. | |
template<typename Specialization, typename Temp, typename To, typename I> | |
bool | l_m_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Box< I > &x, const Box< I > &y, const Rounding_Dir dir, Temp &tmp0, Temp &tmp1, Temp &tmp2) |
Related Functions | |
(Note that these are not member functions.) | |
template<typename ITV> | |
bool | operator!= (const Box< ITV > &x, const Box< ITV > &y) |
Returns true if and only if x and y aren't the same box. | |
template<typename To, typename ITV> | |
bool | rectilinear_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Box< ITV > &x, const Box< ITV > &y, Rounding_Dir dir) |
Computes the rectilinear (or Manhattan) distance between x and y . | |
template<typename Temp, typename To, typename ITV> | |
bool | rectilinear_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Box< ITV > &x, const Box< ITV > &y, Rounding_Dir dir, Temp &tmp0, Temp &tmp1, Temp &tmp2) |
Computes the rectilinear (or Manhattan) distance between x and y . | |
template<typename To, typename ITV> | |
bool | euclidean_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Box< ITV > &x, const Box< ITV > &y, Rounding_Dir dir) |
Computes the euclidean distance between x and y . | |
template<typename Temp, typename To, typename ITV> | |
bool | euclidean_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Box< ITV > &x, const Box< ITV > &y, Rounding_Dir dir, Temp &tmp0, Temp &tmp1, Temp &tmp2) |
Computes the euclidean distance between x and y . | |
template<typename To, typename ITV> | |
bool | l_infinity_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Box< ITV > &x, const Box< ITV > &y, Rounding_Dir dir) |
Computes the ![]() x and y . | |
template<typename Temp, typename To, typename ITV> | |
bool | l_infinity_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Box< ITV > &x, const Box< ITV > &y, Rounding_Dir dir, Temp &tmp0, Temp &tmp1, Temp &tmp2) |
Computes the ![]() x and y . | |
template<typename Specialization, typename Temp, typename To, typename ITV> | |
bool | l_m_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Box< ITV > &x, const Box< ITV > &y, Rounding_Dir dir, Temp &tmp0, Temp &tmp1, Temp &tmp2) |
bool | extract_interval_constraint (const Constraint &c, dimension_type c_space_dim, dimension_type &c_num_vars, dimension_type &c_only_var) |
Decodes the constraint c as an interval constraint. | |
Classes | |
class | Status |
A Box object represents the Cartesian product of not necessarily closed and possibly unbounded intervals represented by objects of class
ITV
, where is the space dimension of the box.
Definition at line 270 of file Box.defs.hh.
typedef ITV Parma_Polyhedra_Library::Box< ITV >::interval_type |
typedef std::vector<ITV> Parma_Polyhedra_Library::Box< ITV >::Sequence [private] |
typedef ITV Parma_Polyhedra_Library::Box< ITV >::Tmp_Interval_Type [private] |
The type of intervals used by inner computations when trying to limit the cumulative effect of approximation errors.
Definition at line 1534 of file Box.defs.hh.
Parma_Polyhedra_Library::Box< ITV >::Box | ( | dimension_type | num_dimensions = 0 , |
|
Degenerate_Element | kind = UNIVERSE | |||
) | [inline, explicit] |
Builds a universe or empty box of the specified space dimension.
num_dimensions | The number of dimensions of the vector space enclosing the box; | |
kind | Specifies whether the universe or the empty box has to be built. |
Definition at line 45 of file Box.templates.hh.
References assign(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::set_empty(), Parma_Polyhedra_Library::Box< ITV >::set_empty_up_to_date(), and Parma_Polyhedra_Library::UNIVERSE.
00046 : seq(num_dimensions <= max_space_dimension() 00047 ? num_dimensions 00048 : (throw_space_dimension_overflow("Box(n, k)", 00049 "n exceeds the maximum " 00050 "allowed space dimension"), 00051 num_dimensions)), 00052 status() { 00053 // In a box that is marked empty the intervals are completely 00054 // meaningless: we exploit this by avoiding their initialization. 00055 if (kind == UNIVERSE) { 00056 for (dimension_type i = num_dimensions; i-- > 0; ) 00057 seq[i].assign(UNIVERSE); 00058 set_empty_up_to_date(); 00059 } 00060 else 00061 set_empty(); 00062 assert(OK()); 00063 }
Parma_Polyhedra_Library::Box< ITV >::Box | ( | const Box< ITV > & | y, | |
Complexity_Class | complexity = ANY_COMPLEXITY | |||
) | [inline] |
Ordinary copy-constructor.
The complexity argument is ignored.
Definition at line 69 of file Box.inlines.hh.
Parma_Polyhedra_Library::Box< ITV >::Box | ( | const Box< Other_ITV > & | y, | |
Complexity_Class | complexity = ANY_COMPLEXITY | |||
) | [inline, explicit] |
Builds a conservative, upward approximation of y
.
The complexity argument is ignored.
Definition at line 100 of file Box.templates.hh.
References assign(), Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::set_empty(), and Parma_Polyhedra_Library::Box< ITV >::space_dimension().
00101 : seq(y.space_dimension()), 00102 // FIXME: why the following does not work? 00103 // status(y.status) { 00104 status() { 00105 // FIXME: remove when the above is fixed. 00106 if (y.marked_empty()) 00107 set_empty(); 00108 00109 if (!y.marked_empty()) 00110 for (dimension_type k = y.space_dimension(); k-- > 0; ) 00111 seq[k].assign(y.seq[k]); 00112 assert(OK()); 00113 }
Parma_Polyhedra_Library::Box< ITV >::Box | ( | const Constraint_System & | cs | ) | [inline, explicit] |
Builds a box from the system of constraints cs
.
The box inherits the space dimension of cs
.
cs | A system of constraints: constraints that are not interval constraints are ignored (even though they may have contributed to the space dimension). |
Definition at line 67 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::add_constraints_no_check(), assign(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Constraint_System::space_dimension(), and Parma_Polyhedra_Library::UNIVERSE.
00068 : seq(cs.space_dimension() <= max_space_dimension() 00069 ? cs.space_dimension() 00070 : (throw_space_dimension_overflow("Box(cs)", 00071 "cs exceeds the maximum " 00072 "allowed space dimension"), 00073 cs.space_dimension())), 00074 status() { 00075 // FIXME: check whether we can avoid the double initialization. 00076 for (dimension_type i = cs.space_dimension(); i-- > 0; ) 00077 seq[i].assign(UNIVERSE); 00078 add_constraints_no_check(cs); 00079 }
Parma_Polyhedra_Library::Box< ITV >::Box | ( | const Constraint_System & | cs, | |
Recycle_Input | dummy | |||
) | [inline] |
Builds a box recycling a system of constraints cs
.
The box inherits the space dimension of cs
.
cs | A system of constraints: constraints that are not interval constraints are ignored (even though they may have contributed to the space dimension). | |
dummy | A dummy tag to syntactically differentiate this one from the other constructors. |
Definition at line 91 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::swap().
00091 { 00092 // Recycling is useless: just delegate. 00093 Box<ITV> tmp(cs); 00094 this->swap(tmp); 00095 }
Parma_Polyhedra_Library::Box< ITV >::Box | ( | const Generator_System & | gs | ) | [inline, explicit] |
Builds a box from the system of generators gs
.
Builds the smallest box containing the polyhedron defined by gs
. The box 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 116 of file Box.templates.hh.
References assign(), Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::Generator_System::begin(), Parma_Polyhedra_Library::Generator::CLOSURE_POINT, Parma_Polyhedra_Library::Generator::coefficient(), Parma_Polyhedra_Library::Generator::divisor(), Parma_Polyhedra_Library::Generator_System::end(), Parma_Polyhedra_Library::Generator::is_point(), Parma_Polyhedra_Library::Generator::LINE, Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Generator::RAY, Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::set_empty(), Parma_Polyhedra_Library::Box< ITV >::set_empty_up_to_date(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Generator::type(), and Parma_Polyhedra_Library::UNIVERSE.
00117 : seq(gs.space_dimension() <= max_space_dimension() 00118 ? gs.space_dimension() 00119 : (throw_space_dimension_overflow("Box(gs)", 00120 "gs exceeds the maximum " 00121 "allowed space dimension"), 00122 gs.space_dimension())), 00123 status() { 00124 const Generator_System::const_iterator gs_begin = gs.begin(); 00125 const Generator_System::const_iterator gs_end = gs.end(); 00126 if (gs_begin == gs_end) { 00127 // An empty generator system defines the empty box. 00128 set_empty(); 00129 return; 00130 } 00131 00132 // The empty flag will be meaningful, whatever happens from now on. 00133 set_empty_up_to_date(); 00134 00135 const dimension_type space_dim = space_dimension(); 00136 DIRTY_TEMP0(mpq_class, q); 00137 bool point_seen = false; 00138 // Going through all the points. 00139 for (Generator_System::const_iterator 00140 gs_i = gs_begin; gs_i != gs_end; ++gs_i) { 00141 const Generator& g = *gs_i; 00142 if (g.is_point()) { 00143 const Coefficient& d = g.divisor(); 00144 if (point_seen) { 00145 // This is not the first point: `seq' already contains valid values. 00146 for (dimension_type i = space_dim; i-- > 0; ) { 00147 assign_r(q.get_num(), g.coefficient(Variable(i)), ROUND_NOT_NEEDED); 00148 assign_r(q.get_den(), d, ROUND_NOT_NEEDED); 00149 q.canonicalize(); 00150 seq[i].join_assign(q); 00151 } 00152 } 00153 else { 00154 // This is the first point seen: initialize `seq'. 00155 point_seen = true; 00156 for (dimension_type i = space_dim; i-- > 0; ) { 00157 assign_r(q.get_num(), g.coefficient(Variable(i)), ROUND_NOT_NEEDED); 00158 assign_r(q.get_den(), d, ROUND_NOT_NEEDED); 00159 q.canonicalize(); 00160 seq[i].assign(q); 00161 } 00162 } 00163 } 00164 } 00165 00166 if (!point_seen) 00167 // The generator system is not empty, but contains no points. 00168 throw std::invalid_argument("PPL::Box<ITV>::Box(gs):\n" 00169 "the non-empty generator system gs " 00170 "contains no points."); 00171 00172 // Going through all the lines, rays and closure points. 00173 ITV q_interval; 00174 for (Generator_System::const_iterator gs_i = gs_begin; 00175 gs_i != gs_end; ++gs_i) { 00176 const Generator& g = *gs_i; 00177 switch (g.type()) { 00178 case Generator::LINE: 00179 for (dimension_type i = space_dim; i-- > 0; ) 00180 if (g.coefficient(Variable(i)) != 0) 00181 seq[i].assign(UNIVERSE); 00182 break; 00183 case Generator::RAY: 00184 for (dimension_type i = space_dim; i-- > 0; ) 00185 switch (sgn(g.coefficient(Variable(i)))) { 00186 case 1: 00187 seq[i].upper_set(UNBOUNDED); 00188 break; 00189 case -1: 00190 seq[i].lower_set(UNBOUNDED); 00191 break; 00192 default: 00193 break; 00194 } 00195 break; 00196 case Generator::CLOSURE_POINT: 00197 { 00198 const Coefficient& d = g.divisor(); 00199 for (dimension_type i = space_dim; i-- > 0; ) { 00200 assign_r(q.get_num(), g.coefficient(Variable(i)), ROUND_NOT_NEEDED); 00201 assign_r(q.get_den(), d, ROUND_NOT_NEEDED); 00202 q.canonicalize(); 00203 ITV& seq_i = seq[i]; 00204 seq_i.lower_widen(q, true); 00205 seq_i.upper_widen(q, true); 00206 } 00207 } 00208 break; 00209 default: 00210 // Points already dealt with. 00211 break; 00212 } 00213 } 00214 assert(OK()); 00215 }
Parma_Polyhedra_Library::Box< ITV >::Box | ( | const Generator_System & | gs, | |
Recycle_Input | dummy | |||
) | [inline] |
Builds a box recycling the system of generators gs
.
Builds the smallest box containing the polyhedron defined by gs
. The box inherits the space dimension of gs
.
gs | The generator system describing the polyhedron to be approximated. | |
dummy | A dummy tag to syntactically differentiate this one from the other constructors. |
std::invalid_argument | Thrown if the system of generators is not empty but has no points. |
Definition at line 99 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::swap().
00099 { 00100 // Recycling is useless: just delegate. 00101 Box<ITV> tmp(gs); 00102 this->swap(tmp); 00103 }
Parma_Polyhedra_Library::Box< ITV >::Box | ( | const Congruence_System & | cgs | ) | [inline, explicit] |
Builds the smallest box containing the grid defined by a system of congruences cgs
. The box inherits the space dimension of cgs
.
cgs | A system of congruences: congruences that are not non-relational equality constraints are ignored (though they may have contributed to the space dimension). |
Definition at line 83 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::add_congruences_no_check(), assign(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Congruence_System::space_dimension(), and Parma_Polyhedra_Library::UNIVERSE.
00084 : seq(cgs.space_dimension() <= max_space_dimension() 00085 ? cgs.space_dimension() 00086 : (throw_space_dimension_overflow("Box(cgs)", 00087 "cgs exceeds the maximum " 00088 "allowed space dimension"), 00089 cgs.space_dimension())), 00090 status() { 00091 // FIXME: check whether we can avoid the double initialization. 00092 for (dimension_type i = cgs.space_dimension(); i-- > 0; ) 00093 seq[i].assign(UNIVERSE); 00094 add_congruences_no_check(cgs); 00095 }
Parma_Polyhedra_Library::Box< ITV >::Box | ( | const Congruence_System & | cgs, | |
Recycle_Input | dummy | |||
) | [inline] |
Builds the smallest box containing the grid defined by a system of congruences cgs
, recycling cgs
. The box inherits the space dimension of cgs
.
cgs | A system of congruences: congruences that are not non-relational equality constraints are ignored (though they will contribute to the space dimension). | |
dummy | A dummy tag to syntactically differentiate this one from the other constructors. |
Definition at line 107 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::swap().
00107 { 00108 // Recycling is useless: just delegate. 00109 Box<ITV> tmp(cgs); 00110 this->swap(tmp); 00111 }
Parma_Polyhedra_Library::Box< ITV >::Box | ( | const BD_Shape< T > & | bds, | |
Complexity_Class | complexity = POLYNOMIAL_COMPLEXITY | |||
) | [inline, explicit] |
Builds a box containing the BDS bds
.
Builds the smallest box containing bds
using a polynomial algorithm. The complexity
argument is ignored.
Definition at line 219 of file Box.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::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::set_empty(), Parma_Polyhedra_Library::Box< ITV >::set_empty_up_to_date(), Parma_Polyhedra_Library::BD_Shape< T >::shortest_path_closure_assign(), and Parma_Polyhedra_Library::Box< ITV >::space_dimension().
00220 : seq(bds.space_dimension() <= max_space_dimension() 00221 ? bds.space_dimension() 00222 : (throw_space_dimension_overflow("Box(bds)", 00223 "bds exceeds the maximum " 00224 "allowed space dimension"), 00225 bds.space_dimension())), 00226 status() { 00227 // Expose all the interval constraints. 00228 bds.shortest_path_closure_assign(); 00229 if (bds.marked_empty()) { 00230 set_empty(); 00231 assert(OK()); 00232 return; 00233 } 00234 00235 // The empty flag will be meaningful, whatever happens from now on. 00236 set_empty_up_to_date(); 00237 00238 const dimension_type space_dim = space_dimension(); 00239 if (space_dim == 0) { 00240 assert(OK()); 00241 return; 00242 } 00243 00244 DIRTY_TEMP(typename BD_Shape<T>::coefficient_type, tmp); 00245 const DB_Row<typename BD_Shape<T>::coefficient_type>& dbm_0 = bds.dbm[0]; 00246 for (dimension_type i = space_dim; i-- > 0; ) { 00247 ITV& seq_i = seq[i]; 00248 // Set the upper bound. 00249 const typename BD_Shape<T>::coefficient_type& u = dbm_0[i+1]; 00250 if (is_plus_infinity(u)) 00251 seq_i.upper_set_uninit(UNBOUNDED); 00252 else 00253 seq_i.upper_set_uninit(u); 00254 00255 // Set the lower bound. 00256 const typename BD_Shape<T>::coefficient_type& negated_l = bds.dbm[i+1][0]; 00257 if (is_plus_infinity(negated_l)) 00258 seq_i.lower_set_uninit(UNBOUNDED); 00259 else { 00260 neg_assign_r(tmp, negated_l, ROUND_DOWN); 00261 seq_i.lower_set_uninit(tmp); 00262 } 00263 00264 // Complete the interval initialization. 00265 seq_i.complete_init(); 00266 } 00267 assert(OK()); 00268 }
Parma_Polyhedra_Library::Box< ITV >::Box | ( | const Octagonal_Shape< T > & | oct, | |
Complexity_Class | complexity = POLYNOMIAL_COMPLEXITY | |||
) | [inline, explicit] |
Builds a box containing the octagonal shape oct
.
Builds the smallest box containing oct
using a polynomial algorithm. The complexity
argument is ignored.
Definition at line 272 of file Box.templates.hh.
References Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::is_plus_infinity(), Parma_Polyhedra_Library::Octagonal_Shape< T >::marked_empty(), Parma_Polyhedra_Library::Octagonal_Shape< T >::matrix, Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::set_empty(), Parma_Polyhedra_Library::Box< ITV >::set_empty_up_to_date(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Octagonal_Shape< T >::strong_closure_assign().
00273 : seq(oct.space_dimension() <= max_space_dimension() 00274 ? oct.space_dimension() 00275 : (throw_space_dimension_overflow("Box(oct)", 00276 "oct exceeds the maximum " 00277 "allowed space dimension"), 00278 oct.space_dimension())), 00279 status() { 00280 // Expose all the interval constraints. 00281 oct.strong_closure_assign(); 00282 if (oct.marked_empty()) { 00283 set_empty(); 00284 return; 00285 } 00286 00287 // The empty flag will be meaningful, whatever happens from now on. 00288 set_empty_up_to_date(); 00289 00290 const dimension_type space_dim = space_dimension(); 00291 if (space_dim == 0) 00292 return; 00293 00294 DIRTY_TEMP0(mpq_class, bound); 00295 for (dimension_type i = space_dim; i-- > 0; ) { 00296 ITV& seq_i = seq[i]; 00297 const dimension_type ii = 2*i; 00298 const dimension_type cii = ii + 1; 00299 00300 // Set the upper bound. 00301 const typename Octagonal_Shape<T>::coefficient_type& twice_ub 00302 = oct.matrix[cii][ii]; 00303 if (!is_plus_infinity(twice_ub)) { 00304 assign_r(bound, twice_ub, ROUND_NOT_NEEDED); 00305 div2exp_assign_r(bound, bound, 1, ROUND_NOT_NEEDED); 00306 seq_i.upper_set_uninit(bound); 00307 } 00308 else 00309 seq_i.upper_set_uninit(UNBOUNDED); 00310 00311 // Set the lower bound. 00312 const typename Octagonal_Shape<T>::coefficient_type& twice_lb 00313 = oct.matrix[ii][cii]; 00314 if (!is_plus_infinity(twice_lb)) { 00315 assign_r(bound, twice_lb, ROUND_NOT_NEEDED); 00316 neg_assign_r(bound, bound, ROUND_NOT_NEEDED); 00317 div2exp_assign_r(bound, bound, 1, ROUND_NOT_NEEDED); 00318 seq_i.lower_set_uninit(bound); 00319 } 00320 else 00321 seq_i.lower_set_uninit(UNBOUNDED); 00322 seq_i.complete_init(); 00323 } 00324 }
Parma_Polyhedra_Library::Box< ITV >::Box | ( | const Polyhedron & | ph, | |
Complexity_Class | complexity = ANY_COMPLEXITY | |||
) | [inline, explicit] |
Builds a box containing the polyhedron ph
.
Builds a box containing ph
using algorithms whose complexity does not exceed the one specified by complexity
. If complexity
is ANY_COMPLEXITY
, then the built box is the smallest one containing ph
.
Definition at line 327 of file Box.templates.hh.
References Parma_Polyhedra_Library::MIP_Problem::add_constraint(), Parma_Polyhedra_Library::MIP_Problem::add_constraints(), Parma_Polyhedra_Library::ANY_COMPLEXITY, assign(), Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::Constraint_System::begin(), Parma_Polyhedra_Library::Polyhedron::constraints(), Parma_Polyhedra_Library::Polyhedron::constraints_are_up_to_date(), Parma_Polyhedra_Library::Constraint_System::end(), Parma_Polyhedra_Library::MIP_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::Constraint_System::has_strict_inequalities(), Parma_Polyhedra_Library::is_canonical(), Parma_Polyhedra_Library::Polyhedron::is_empty(), Parma_Polyhedra_Library::MIP_Problem::is_satisfiable(), Parma_Polyhedra_Library::Constraint::is_strict_inequality(), Parma_Polyhedra_Library::Polyhedron::marked_empty(), Parma_Polyhedra_Library::MAXIMIZATION, Parma_Polyhedra_Library::MINIMIZATION, Parma_Polyhedra_Library::OPTIMIZED_MIP_PROBLEM, Parma_Polyhedra_Library::MIP_Problem::optimizing_point(), Parma_Polyhedra_Library::POLYNOMIAL_COMPLEXITY, Parma_Polyhedra_Library::Box< ITV >::refine_with_constraints(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::set_empty(), Parma_Polyhedra_Library::Box< ITV >::set_empty_up_to_date(), Parma_Polyhedra_Library::MIP_Problem::set_objective_function(), Parma_Polyhedra_Library::MIP_Problem::set_optimization_mode(), Parma_Polyhedra_Library::SIMPLEX_COMPLEXITY, Parma_Polyhedra_Library::Polyhedron::simplified_constraints(), Parma_Polyhedra_Library::MIP_Problem::solve(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Polyhedron::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::swap(), and Parma_Polyhedra_Library::UNIVERSE.
00328 : seq(ph.space_dimension() <= max_space_dimension() 00329 ? ph.space_dimension() 00330 : (throw_space_dimension_overflow("Box(ph)", 00331 "ph exceeds the maximum " 00332 "allowed space dimension"), 00333 ph.space_dimension())), 00334 status() { 00335 // The empty flag will be meaningful, whatever happens from now on. 00336 set_empty_up_to_date(); 00337 00338 // We do not need to bother about `complexity' if: 00339 // a) the polyhedron is already marked empty; or ... 00340 if (ph.marked_empty()) { 00341 set_empty(); 00342 return; 00343 } 00344 00345 // b) the polyhedron is zero-dimensional; or ... 00346 const dimension_type space_dim = ph.space_dimension(); 00347 if (space_dim == 0) 00348 return; 00349 00350 // c) the polyhedron is already described by a generator system. 00351 if (ph.generators_are_up_to_date() && !ph.has_pending_constraints()) { 00352 Box tmp(ph.generators()); 00353 swap(tmp); 00354 return; 00355 } 00356 00357 // Here generators are not up-to-date or there are pending constraints. 00358 assert(ph.constraints_are_up_to_date()); 00359 00360 if (complexity == POLYNOMIAL_COMPLEXITY) { 00361 // FIXME: is there a way to avoid this initialization? 00362 for (dimension_type i = space_dimension(); i-- > 0; ) 00363 seq[i].assign(UNIVERSE); 00364 // Extract easy-to-find bounds from constraints. 00365 refine_with_constraints(ph.simplified_constraints()); 00366 } 00367 else if (complexity == SIMPLEX_COMPLEXITY) { 00368 MIP_Problem lp(space_dim); 00369 const Constraint_System& ph_cs = ph.constraints(); 00370 if (!ph_cs.has_strict_inequalities()) 00371 lp.add_constraints(ph_cs); 00372 else 00373 // Adding to `lp' a topologically closed version of `ph_cs'. 00374 for (Constraint_System::const_iterator i = ph_cs.begin(), 00375 ph_cs_end = ph_cs.end(); i != ph_cs_end; ++i) { 00376 const Constraint& c = *i; 00377 if (c.is_strict_inequality()) 00378 lp.add_constraint(Linear_Expression(c) >= 0); 00379 else 00380 lp.add_constraint(c); 00381 } 00382 // Check for unsatisfiability. 00383 if (!lp.is_satisfiable()) { 00384 set_empty(); 00385 return; 00386 } 00387 // Get all the bounds for the space dimensions. 00388 Generator g(point()); 00389 DIRTY_TEMP0(mpq_class, bound); 00390 DIRTY_TEMP(Coefficient, bound_num); 00391 DIRTY_TEMP(Coefficient, bound_den); 00392 for (dimension_type i = space_dim; i-- > 0; ) { 00393 ITV& seq_i = seq[i]; 00394 lp.set_objective_function(Variable(i)); 00395 // Evaluate upper bound. 00396 lp.set_optimization_mode(MAXIMIZATION); 00397 if (lp.solve() == OPTIMIZED_MIP_PROBLEM) { 00398 g = lp.optimizing_point(); 00399 lp.evaluate_objective_function(g, bound_num, bound_den); 00400 assign_r(bound.get_num(), bound_num, ROUND_NOT_NEEDED); 00401 assign_r(bound.get_den(), bound_den, ROUND_NOT_NEEDED); 00402 assert(is_canonical(bound)); 00403 seq_i.upper_set_uninit(bound); 00404 } 00405 else 00406 seq_i.upper_set_uninit(UNBOUNDED); 00407 // Evaluate optimal lower bound. 00408 lp.set_optimization_mode(MINIMIZATION); 00409 if (lp.solve() == OPTIMIZED_MIP_PROBLEM) { 00410 g = lp.optimizing_point(); 00411 lp.evaluate_objective_function(g, bound_num, bound_den); 00412 assign_r(bound.get_num(), bound_num, ROUND_NOT_NEEDED); 00413 assign_r(bound.get_den(), bound_den, ROUND_NOT_NEEDED); 00414 assert(is_canonical(bound)); 00415 seq_i.lower_set_uninit(bound); 00416 } 00417 else 00418 seq_i.lower_set_uninit(UNBOUNDED); 00419 seq_i.complete_init(); 00420 } 00421 } 00422 else { 00423 assert(complexity == ANY_COMPLEXITY); 00424 if (ph.is_empty()) 00425 set_empty(); 00426 else { 00427 Box tmp(ph.generators()); 00428 swap(tmp); 00429 } 00430 } 00431 }
Parma_Polyhedra_Library::Box< ITV >::Box | ( | const Grid & | ph, | |
Complexity_Class | complexity = POLYNOMIAL_COMPLEXITY | |||
) | [inline, explicit] |
Builds a box containing the grid gr
.
Builds the smallest box containing gr
using a polynomial algorithm. The complexity
argument is ignored.
Definition at line 434 of file Box.templates.hh.
References Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::Grid_Generator_System::begin(), Parma_Polyhedra_Library::Grid_Generator::divisor(), Parma_Polyhedra_Library::Grid_Generator_System::empty(), Parma_Polyhedra_Library::Grid_Generator_System::end(), Parma_Polyhedra_Library::Grid::gen_sys, Parma_Polyhedra_Library::Grid::generators_are_up_to_date(), Parma_Polyhedra_Library::Grid_Generator::is_point(), Parma_Polyhedra_Library::Grid::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Grid_Generator::set_divisor(), Parma_Polyhedra_Library::Box< ITV >::set_empty(), Parma_Polyhedra_Library::Box< ITV >::set_empty_up_to_date(), Parma_Polyhedra_Library::Grid::space_dimension(), Parma_Polyhedra_Library::UNIVERSE, and Parma_Polyhedra_Library::Grid::update_generators().
00435 : seq(gr.space_dimension() <= max_space_dimension() 00436 ? gr.space_dimension() 00437 : (throw_space_dimension_overflow("Box(gr)", 00438 "gr exceeds the maximum " 00439 "allowed space dimension"), 00440 gr.space_dimension())), 00441 status() { 00442 00443 // FIXME: here we are not taking advantage of intervals with restrictions! 00444 00445 if (gr.marked_empty()) { 00446 set_empty(); 00447 return; 00448 } 00449 00450 // The empty flag will be meaningful, whatever happens from now on. 00451 set_empty_up_to_date(); 00452 00453 const dimension_type space_dim = gr.space_dimension(); 00454 00455 if (space_dim == 0) 00456 return; 00457 00458 if (!gr.generators_are_up_to_date() && !gr.update_generators()) { 00459 // Updating found the grid empty. 00460 set_empty(); 00461 return; 00462 } 00463 00464 assert(!gr.gen_sys.empty()); 00465 00466 // Create a vector to record which dimensions are bounded. 00467 std::vector<bool> bounded_interval(space_dim, true); 00468 00469 const Grid_Generator *first_point = 0; 00470 // Clear the bound flag in `bounded_interval' for all dimensions in 00471 // which a line or sequence of points extends away from a single 00472 // value in the dimension. 00473 // FIXME: this computation should be provided by the Grid class. 00474 // FIXME: remove the declaration making Box a friend of Grid_Generator 00475 // when this is done. 00476 for (Grid_Generator_System::const_iterator gs_i = gr.gen_sys.begin(), 00477 gs_end = gr.gen_sys.end(); gs_i != gs_end; ++gs_i) { 00478 Grid_Generator& g = const_cast<Grid_Generator&>(*gs_i); 00479 if (g.is_point()) { 00480 if (first_point == 0) { 00481 first_point = &g; 00482 continue; 00483 } 00484 const Grid_Generator& point = *first_point; 00485 // Convert the point `g' to a parameter. 00486 for (dimension_type dim = space_dim; dim-- > 0; ) 00487 g[dim] -= point[dim]; 00488 g.set_divisor(point.divisor()); 00489 } 00490 for (dimension_type col = space_dim; col > 0; ) 00491 if (g[col--] != 0) 00492 bounded_interval[col] = false; 00493 } 00494 00495 // For each dimension that is bounded by the grid, set both bounds 00496 // of the interval to the value of the associated coefficient in a 00497 // generator point. 00498 assert(first_point != 0); 00499 const Grid_Generator& point = *first_point; 00500 DIRTY_TEMP0(mpq_class, bound); 00501 const Coefficient& divisor = point.divisor(); 00502 for (dimension_type i = space_dim; i-- > 0; ) { 00503 ITV& seq_i = seq[i]; 00504 if (bounded_interval[i]) { 00505 assign_r(bound.get_num(), point[i+1], ROUND_NOT_NEEDED); 00506 assign_r(bound.get_den(), divisor, ROUND_NOT_NEEDED); 00507 bound.canonicalize(); 00508 seq_i.assign(bound); 00509 } 00510 else 00511 seq_i.assign(UNIVERSE); 00512 } 00513 }
Parma_Polyhedra_Library::Box< ITV >::Box | ( | const Partially_Reduced_Product< D1, D2, R > & | dp, | |
Complexity_Class | complexity = ANY_COMPLEXITY | |||
) | [inline, explicit] |
Builds a box containing the partially reduced product dp
.
Builds a box containing ph
using algorithms whose complexity does not exceed the one specified by complexity
.
Definition at line 517 of file Box.templates.hh.
References Parma_Polyhedra_Library::Partially_Reduced_Product< D1, D2, R >::domain1(), Parma_Polyhedra_Library::Partially_Reduced_Product< D1, D2, R >::domain2(), Parma_Polyhedra_Library::Box< ITV >::max_space_dimension(), Parma_Polyhedra_Library::Partially_Reduced_Product< D1, D2, R >::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::swap(), and Parma_Polyhedra_Library::Box< ITV >::throw_space_dimension_overflow().
00519 : seq(), status() { 00520 if (dp.space_dimension() > max_space_dimension()) 00521 throw_space_dimension_overflow("Box(dp)", 00522 "dp exceeds the maximum " 00523 "allowed space dimension"); 00524 Box tmp1(dp.domain1(), complexity); 00525 Box tmp2(dp.domain2(), complexity); 00526 tmp1.intersection_assign(tmp2); 00527 swap(tmp1); 00528 }
dimension_type Parma_Polyhedra_Library::Box< ITV >::max_space_dimension | ( | ) | [inline, static] |
Returns the maximum space dimension that a Box can handle.
Definition at line 127 of file Box.inlines.hh.
Referenced by Parma_Polyhedra_Library::Box< ITV >::Box(), and Parma_Polyhedra_Library::Box< ITV >::expand_space_dimension().
00127 { 00128 // One dimension is reserved to have a value of type dimension_type 00129 // that does not represent a legal dimension. 00130 return Sequence().max_size() - 1; 00131 }
bool Parma_Polyhedra_Library::Box< T >::can_recycle_constraint_systems | ( | ) | [inline, static] |
Returns false indicating that this domain does not recycle constraints.
Definition at line 358 of file Box.inlines.hh.
bool Parma_Polyhedra_Library::Box< T >::can_recycle_congruence_systems | ( | ) | [inline, static] |
Returns false indicating that this domain does not recycle congruences.
Definition at line 364 of file Box.inlines.hh.
Box< ITV > & Parma_Polyhedra_Library::Box< ITV >::operator= | ( | const Box< ITV > & | y | ) | [inline] |
The assignment operator (*this
and y
can be dimension-incompatible).
Definition at line 75 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::seq, and Parma_Polyhedra_Library::Box< ITV >::status.
void Parma_Polyhedra_Library::Box< ITV >::swap | ( | Box< ITV > & | y | ) | [inline] |
Swaps *this
with y
(*this
and y
can be dimension-incompatible).
Definition at line 83 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::status, and Parma_Polyhedra_Library::swap().
Referenced by Parma_Polyhedra_Library::Box< ITV >::Box(), Parma_Polyhedra_Library::Grid::get_covering_box(), and Parma_Polyhedra_Library::Box< ITV >::map_space_dimensions().
00083 { 00084 Box& x = *this; 00085 std::swap(x.seq, y.seq); 00086 std::swap(x.status, y.status); 00087 }
dimension_type Parma_Polyhedra_Library::Box< ITV >::space_dimension | ( | ) | const [inline] |
Returns the dimension of the vector space enclosing *this
.
Definition at line 121 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::seq.
Referenced by Parma_Polyhedra_Library::Box< ITV >::add_congruence(), Parma_Polyhedra_Library::Box< ITV >::add_congruence_no_check(), Parma_Polyhedra_Library::Box< ITV >::add_congruences(), Parma_Polyhedra_Library::Box< ITV >::add_congruences_no_check(), Parma_Polyhedra_Library::Box< ITV >::add_constraint(), Parma_Polyhedra_Library::Box< ITV >::add_constraint_no_check(), Parma_Polyhedra_Library::Box< ITV >::add_constraints(), Parma_Polyhedra_Library::Box< ITV >::add_constraints_no_check(), Parma_Polyhedra_Library::Box< ITV >::add_interval_constraint_no_check(), Parma_Polyhedra_Library::Box< ITV >::affine_dimension(), Parma_Polyhedra_Library::Box< ITV >::affine_image(), Parma_Polyhedra_Library::Box< ITV >::affine_preimage(), Parma_Polyhedra_Library::Box< ITV >::ascii_dump(), Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape(), Parma_Polyhedra_Library::Box< ITV >::bounded_affine_image(), Parma_Polyhedra_Library::Box< ITV >::bounded_affine_preimage(), Parma_Polyhedra_Library::Box< ITV >::bounds(), Parma_Polyhedra_Library::Box< ITV >::Box(), Parma_Polyhedra_Library::Box< ITV >::CC76_narrowing_assign(), Parma_Polyhedra_Library::Box< ITV >::concatenate_assign(), Parma_Polyhedra_Library::Box< ITV >::congruences(), Parma_Polyhedra_Library::Box< ITV >::constrains(), Parma_Polyhedra_Library::Box< ITV >::constraints(), Parma_Polyhedra_Library::Box< ITV >::contains(), Parma_Polyhedra_Library::Box< ITV >::difference_assign(), Parma_Polyhedra_Library::Box< ITV >::expand_space_dimension(), Parma_Polyhedra_Library::Box< ITV >::fold_space_dimensions(), Parma_Polyhedra_Library::Box< ITV >::generalized_affine_image(), Parma_Polyhedra_Library::Box< ITV >::generalized_affine_preimage(), Parma_Polyhedra_Library::Grid::get_covering_box(), Parma_Polyhedra_Library::Box< ITV >::get_interval(), Parma_Polyhedra_Library::Grid::Grid(), Parma_Polyhedra_Library::Box< ITV >::intersection_assign(), Parma_Polyhedra_Library::Box< ITV >::is_disjoint_from(), Parma_Polyhedra_Library::Box< ITV >::l_m_distance_assign(), Parma_Polyhedra_Library::Box< ITV >::map_space_dimensions(), Parma_Polyhedra_Library::Box< ITV >::max_min(), Parma_Polyhedra_Library::Box< ITV >::minimized_constraints(), Parma_Polyhedra_Library::Octagonal_Shape< T >::Octagonal_Shape(), Parma_Polyhedra_Library::operator==(), Parma_Polyhedra_Library::Polyhedron::Polyhedron(), Parma_Polyhedra_Library::Box< ITV >::propagate_constraint(), Parma_Polyhedra_Library::Box< ITV >::propagate_constraint_no_check(), Parma_Polyhedra_Library::Box< ITV >::propagate_constraints(), Parma_Polyhedra_Library::Box< ITV >::propagate_constraints_no_check(), Parma_Polyhedra_Library::Box< ITV >::refine_no_check(), Parma_Polyhedra_Library::Box< ITV >::refine_with_congruence(), Parma_Polyhedra_Library::Box< ITV >::refine_with_congruences(), Parma_Polyhedra_Library::Box< ITV >::refine_with_constraint(), Parma_Polyhedra_Library::Box< ITV >::refine_with_constraints(), Parma_Polyhedra_Library::Box< ITV >::relation_with(), Parma_Polyhedra_Library::Box< ITV >::remove_higher_space_dimensions(), Parma_Polyhedra_Library::Box< ITV >::remove_space_dimensions(), Parma_Polyhedra_Library::Box< ITV >::set_interval(), Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible(), Parma_Polyhedra_Library::Box< ITV >::time_elapse_assign(), Parma_Polyhedra_Library::Box< ITV >::unconstrain(), and Parma_Polyhedra_Library::Box< ITV >::upper_bound_assign().
00121 { 00122 return seq.size(); 00123 }
dimension_type Parma_Polyhedra_Library::Box< ITV >::affine_dimension | ( | ) | const [inline] |
Returns , if
*this
is empty; otherwise, returns the affine dimension of *this
.
Definition at line 1250 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::Box< ITV >::seq, and Parma_Polyhedra_Library::Box< ITV >::space_dimension().
01250 { 01251 dimension_type d = space_dimension(); 01252 // A zero-space-dim box always has affine dimension zero. 01253 if (d == 0) 01254 return 0; 01255 01256 // An empty box has affine dimension zero. 01257 if (is_empty()) 01258 return 0; 01259 01260 for (dimension_type k = d; k-- > 0; ) 01261 if (seq[k].is_singleton()) 01262 --d; 01263 01264 return d; 01265 }
bool Parma_Polyhedra_Library::Box< ITV >::is_empty | ( | ) | const [inline] |
Returns true
if and only if *this
is an empty box.
Definition at line 174 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::check_empty(), and Parma_Polyhedra_Library::Box< ITV >::marked_empty().
Referenced by Parma_Polyhedra_Library::Box< ITV >::affine_dimension(), Parma_Polyhedra_Library::Box< ITV >::affine_image(), Parma_Polyhedra_Library::Box< ITV >::affine_preimage(), Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape(), Parma_Polyhedra_Library::Box< ITV >::bounded_affine_image(), Parma_Polyhedra_Library::Box< ITV >::bounds(), Parma_Polyhedra_Library::Box< ITV >::CC76_narrowing_assign(), Parma_Polyhedra_Library::Box< ITV >::CC76_widening_assign(), Parma_Polyhedra_Library::Box< ITV >::check_empty(), Parma_Polyhedra_Library::Box< ITV >::congruences(), Parma_Polyhedra_Library::Box< ITV >::constrains(), Parma_Polyhedra_Library::Box< ITV >::contains(), Parma_Polyhedra_Library::Box< ITV >::difference_assign(), Parma_Polyhedra_Library::Box< ITV >::fold_space_dimensions(), Parma_Polyhedra_Library::Box< ITV >::generalized_affine_image(), Parma_Polyhedra_Library::Box< ITV >::generalized_affine_preimage(), Parma_Polyhedra_Library::Box< ITV >::get_interval(), Parma_Polyhedra_Library::Grid::Grid(), Parma_Polyhedra_Library::Box< ITV >::is_bounded(), Parma_Polyhedra_Library::Box< ITV >::is_discrete(), Parma_Polyhedra_Library::Box< ITV >::is_topologically_closed(), Parma_Polyhedra_Library::Box< ITV >::l_m_distance_assign(), Parma_Polyhedra_Library::Box< ITV >::map_space_dimensions(), Parma_Polyhedra_Library::Box< ITV >::max_min(), Parma_Polyhedra_Library::Box< ITV >::minimized_constraints(), Parma_Polyhedra_Library::Octagonal_Shape< T >::Octagonal_Shape(), Parma_Polyhedra_Library::operator==(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::Pointset_Powerset(), Parma_Polyhedra_Library::Polyhedron::Polyhedron(), Parma_Polyhedra_Library::Box< ITV >::relation_with(), Parma_Polyhedra_Library::Box< ITV >::remove_space_dimensions(), Parma_Polyhedra_Library::Box< ITV >::set_interval(), Parma_Polyhedra_Library::Box< ITV >::time_elapse_assign(), and Parma_Polyhedra_Library::Box< ITV >::topological_closure_assign().
00174 { 00175 return marked_empty() || check_empty(); 00176 }
bool Parma_Polyhedra_Library::Box< ITV >::is_universe | ( | ) | const [inline] |
Returns true
if and only if *this
is a universe box.
Definition at line 1283 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::marked_empty(), and Parma_Polyhedra_Library::Box< ITV >::seq.
Referenced by Parma_Polyhedra_Library::Box< ITV >::constrains().
01283 { 01284 if (marked_empty()) 01285 return false; 01286 for (dimension_type k = seq.size(); k-- > 0; ) 01287 if (!seq[k].is_universe()) 01288 return false; 01289 return true; 01290 }
bool Parma_Polyhedra_Library::Box< ITV >::is_topologically_closed | ( | ) | const [inline] |
Returns true
if and only if *this
is a topologically closed subset of the vector space.
Definition at line 1294 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::is_empty(), and Parma_Polyhedra_Library::Box< ITV >::seq.
01294 { 01295 if (!ITV::info_type::store_open || is_empty()) 01296 return true; 01297 01298 for (dimension_type k = seq.size(); k-- > 0; ) 01299 if (!seq[k].is_topologically_closed()) 01300 return false; 01301 return true; 01302 }
bool Parma_Polyhedra_Library::Box< ITV >::is_discrete | ( | ) | const [inline] |
Returns true
if and only if *this
is discrete.
Definition at line 1306 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::is_empty(), and Parma_Polyhedra_Library::Box< ITV >::seq.
01306 { 01307 if (is_empty()) 01308 return true; 01309 for (dimension_type k = seq.size(); k-- > 0; ) 01310 if (!seq[k].is_singleton()) 01311 return false; 01312 return true; 01313 }
bool Parma_Polyhedra_Library::Box< ITV >::is_bounded | ( | ) | const [inline] |
Returns true
if and only if *this
is a bounded box.
Definition at line 1317 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::is_empty(), and Parma_Polyhedra_Library::Box< ITV >::seq.
01317 { 01318 if (is_empty()) 01319 return true; 01320 for (dimension_type k = seq.size(); k-- > 0; ) 01321 if (seq[k].is_unbounded()) 01322 return false; 01323 return true; 01324 }
bool Parma_Polyhedra_Library::Box< ITV >::contains_integer_point | ( | ) | const [inline] |
Returns true
if and only if *this
contains at least one integer point.
Definition at line 1328 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::marked_empty(), and Parma_Polyhedra_Library::Box< ITV >::seq.
01328 { 01329 if (marked_empty()) 01330 return false; 01331 for (dimension_type k = seq.size(); k-- > 0; ) 01332 if (!seq[k].contains_integer_point()) 01333 return false; 01334 return true; 01335 }
bool Parma_Polyhedra_Library::Box< ITV >::constrains | ( | Variable | var | ) | const [inline] |
Returns true
if and only if var
is constrained in *this
.
std::invalid_argument | Thrown if var is not a space dimension of *this . |
Definition at line 1339 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::Box< ITV >::is_universe(), Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Variable::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
01339 { 01340 // `var' should be one of the dimensions of the polyhedron. 01341 const dimension_type var_space_dim = var.space_dimension(); 01342 if (space_dimension() < var_space_dim) 01343 throw_dimension_incompatible("constrains(v)", "v", var); 01344 01345 if (marked_empty() || !seq[var_space_dim-1].is_universe()) 01346 return true; 01347 // Now force an emptiness check. 01348 return is_empty(); 01349 }
Poly_Con_Relation Parma_Polyhedra_Library::Box< ITV >::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. |
Definition at line 862 of file Box.templates.hh.
References Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::Constraint::coefficient(), Parma_Polyhedra_Library::Box< ITV >::extract_interval_constraint(), Parma_Polyhedra_Library::Constraint::inhomogeneous_term(), Parma_Polyhedra_Library::interval_relation(), Parma_Polyhedra_Library::Poly_Con_Relation::is_disjoint(), Parma_Polyhedra_Library::Box< ITV >::is_empty(), 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::Poly_Con_Relation::saturates(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Constraint::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible(), and Parma_Polyhedra_Library::Constraint::type().
Referenced by Parma_Polyhedra_Library::Box< ITV >::relation_with().
00862 { 00863 const dimension_type c_space_dim = c.space_dimension(); 00864 const dimension_type space_dim = space_dimension(); 00865 00866 // Dimension-compatibility check. 00867 if (c_space_dim > space_dim) 00868 throw_dimension_incompatible("relation_with(c)", c); 00869 00870 if (is_empty()) 00871 return Poly_Con_Relation::saturates() 00872 && Poly_Con_Relation::is_included() 00873 && Poly_Con_Relation::is_disjoint(); 00874 00875 if (space_dim == 0) { 00876 if ((c.is_equality() && c.inhomogeneous_term() != 0) 00877 || (c.is_inequality() && c.inhomogeneous_term() < 0)) 00878 return Poly_Con_Relation::is_disjoint(); 00879 else if (c.is_strict_inequality() && c.inhomogeneous_term() == 0) 00880 // The constraint 0 > 0 implicitly defines the hyperplane 0 = 0; 00881 // thus, the zero-dimensional point also saturates it. 00882 return Poly_Con_Relation::saturates() 00883 && Poly_Con_Relation::is_disjoint(); 00884 else if (c.is_equality() || c.inhomogeneous_term() == 0) 00885 return Poly_Con_Relation::saturates() 00886 && Poly_Con_Relation::is_included(); 00887 else 00888 // The zero-dimensional point saturates 00889 // neither the positivity constraint 1 >= 0, 00890 // nor the strict positivity constraint 1 > 0. 00891 return Poly_Con_Relation::is_included(); 00892 } 00893 00894 dimension_type c_num_vars = 0; 00895 dimension_type c_only_var = 0; 00896 00897 if (extract_interval_constraint(c, c_space_dim, c_num_vars, c_only_var)) 00898 if (c_num_vars == 0) 00899 // c is a trivial constraint. 00900 switch (sgn(c.inhomogeneous_term())) { 00901 case -1: 00902 return Poly_Con_Relation::is_disjoint(); 00903 case 0: 00904 if (c.is_strict_inequality()) 00905 return Poly_Con_Relation::saturates() 00906 && Poly_Con_Relation::is_disjoint(); 00907 else 00908 return Poly_Con_Relation::saturates() 00909 && Poly_Con_Relation::is_included(); 00910 case 1: 00911 return Poly_Con_Relation::is_included(); 00912 } 00913 else { 00914 // c is an interval constraint. 00915 return interval_relation(seq[c_only_var], 00916 c.type(), 00917 c.inhomogeneous_term(), 00918 c.coefficient(Variable(c_only_var))); 00919 } 00920 else { 00921 // Deal with a non-trivial and non-interval constraint. 00922 DIRTY_TEMP0(Rational_Interval, r); 00923 DIRTY_TEMP0(Rational_Interval, t); 00924 DIRTY_TEMP0(mpq_class, m); 00925 r = 0; 00926 for (dimension_type i = c.space_dimension(); i-- > 0; ) { 00927 const Coefficient& c_i = c.coefficient(Variable(i)); 00928 if (sgn(c_i) != 0) { 00929 assign_r(m, c_i, ROUND_NOT_NEEDED); 00930 // FIXME: an add_mul_assign() method would come handy here. 00931 t = seq[i]; 00932 t *= m; 00933 r += t; 00934 } 00935 } 00936 return interval_relation(r, 00937 c.type(), 00938 c.inhomogeneous_term()); 00939 } 00940 00941 // Quiet a compiler warning: this program point is unreachable. 00942 throw std::runtime_error("PPL internal error"); 00943 }
Poly_Con_Relation Parma_Polyhedra_Library::Box< ITV >::relation_with | ( | const Congruence & | cg | ) | const [inline] |
Returns the relations holding between *this
and the congruence cg
.
std::invalid_argument | Thrown if *this and constraint cg are dimension-incompatible. |
Definition at line 800 of file Box.templates.hh.
References Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::Congruence::coefficient(), Parma_Polyhedra_Library::Constraint::EQUALITY, Parma_Polyhedra_Library::Congruence::inhomogeneous_term(), Parma_Polyhedra_Library::interval_relation(), Parma_Polyhedra_Library::Poly_Con_Relation::is_disjoint(), Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::Congruence::is_equality(), Parma_Polyhedra_Library::Poly_Con_Relation::is_included(), Parma_Polyhedra_Library::Congruence::is_inconsistent(), Parma_Polyhedra_Library::lower(), Parma_Polyhedra_Library::Congruence::modulus(), Parma_Polyhedra_Library::Box< ITV >::relation_with(), Parma_Polyhedra_Library::Poly_Con_Relation::saturates(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Congruence::space_dimension(), Parma_Polyhedra_Library::Poly_Con_Relation::strictly_intersects(), TEMP_INTEGER, and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
00800 { 00801 const dimension_type cg_space_dim = cg.space_dimension(); 00802 const dimension_type space_dim = space_dimension(); 00803 00804 // Dimension-compatibility check. 00805 if (cg_space_dim > space_dim) 00806 throw_dimension_incompatible("relation_with(cg)", cg); 00807 00808 if (is_empty()) 00809 return Poly_Con_Relation::saturates() 00810 && Poly_Con_Relation::is_included() 00811 && Poly_Con_Relation::is_disjoint(); 00812 00813 if (space_dim == 0) { 00814 if (cg.is_inconsistent()) 00815 return Poly_Con_Relation::is_disjoint(); 00816 else 00817 return Poly_Con_Relation::saturates() 00818 && Poly_Con_Relation::is_included(); 00819 } 00820 00821 if (cg.is_equality()) { 00822 const Constraint c(cg); 00823 return relation_with(c); 00824 } 00825 00826 DIRTY_TEMP0(Rational_Interval, r); 00827 DIRTY_TEMP0(Rational_Interval, t); 00828 DIRTY_TEMP0(mpq_class, m); 00829 r = 0; 00830 for (dimension_type i = cg.space_dimension(); i-- > 0; ) { 00831 const Coefficient& cg_i = cg.coefficient(Variable(i)); 00832 if (sgn(cg_i) != 0) { 00833 assign_r(m, cg_i, ROUND_NOT_NEEDED); 00834 // FIXME: an add_mul_assign() method would come handy here. 00835 t = seq[i]; 00836 t *= m; 00837 r += t; 00838 } 00839 } 00840 00841 if (r.lower_is_unbounded() || r.upper_is_unbounded()) 00842 return Poly_Con_Relation::strictly_intersects(); 00843 00844 00845 // Find the value that satisfies the congruence and is 00846 // nearest to the lower bound such that the point lies on or above it. 00847 00848 TEMP_INTEGER(lower); 00849 TEMP_INTEGER(mod); 00850 TEMP_INTEGER(v); 00851 mod = cg.modulus(); 00852 v = cg.inhomogeneous_term() % mod; 00853 assign_r(lower, r.lower(), ROUND_DOWN); 00854 v -= ((lower / mod) * mod); 00855 if (v + lower > 0) 00856 v -= mod; 00857 return interval_relation(r, Constraint::EQUALITY, v); 00858 }
Poly_Gen_Relation Parma_Polyhedra_Library::Box< ITV >::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 947 of file Box.templates.hh.
References Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::Generator::coefficient(), Parma_Polyhedra_Library::Generator::divisor(), Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::Generator::is_line(), Parma_Polyhedra_Library::Generator::is_line_or_ray(), Parma_Polyhedra_Library::Generator::is_point(), Parma_Polyhedra_Library::Generator::is_ray(), Parma_Polyhedra_Library::Poly_Gen_Relation::nothing(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Generator::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Poly_Gen_Relation::subsumes(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
00947 { 00948 const dimension_type space_dim = space_dimension(); 00949 const dimension_type g_space_dim = g.space_dimension(); 00950 00951 // Dimension-compatibility check. 00952 if (space_dim < g_space_dim) 00953 throw_dimension_incompatible("relation_with(g)", g); 00954 00955 // The empty box cannot subsume a generator. 00956 if (is_empty()) 00957 return Poly_Gen_Relation::nothing(); 00958 00959 // A universe box in a zero-dimensional space subsumes 00960 // all the generators of a zero-dimensional space. 00961 if (space_dim == 0) 00962 return Poly_Gen_Relation::subsumes(); 00963 00964 if (g.is_line_or_ray()) { 00965 if (g.is_line()) { 00966 for (dimension_type i = g_space_dim; i-- > 0; ) 00967 if (g.coefficient(Variable(i)) != 0 && !seq[i].is_universe()) 00968 return Poly_Gen_Relation::nothing(); 00969 return Poly_Gen_Relation::subsumes(); 00970 } 00971 else { 00972 assert(g.is_ray()); 00973 for (dimension_type i = g_space_dim; i-- > 0; ) 00974 switch (sgn(g.coefficient(Variable(i)))) { 00975 case 1: 00976 if (!seq[i].upper_is_unbounded()) 00977 return Poly_Gen_Relation::nothing(); 00978 break; 00979 case 0: 00980 break; 00981 case -1: 00982 if (!seq[i].lower_is_unbounded()) 00983 return Poly_Gen_Relation::nothing(); 00984 break; 00985 } 00986 return Poly_Gen_Relation::subsumes(); 00987 } 00988 } 00989 00990 // Here `g' is a point or closure point. 00991 const Coefficient& g_divisor = g.divisor(); 00992 DIRTY_TEMP0(mpq_class, g_coord); 00993 DIRTY_TEMP0(mpq_class, bound); 00994 for (dimension_type i = g_space_dim; i-- > 0; ) { 00995 const ITV& seq_i = seq[i]; 00996 if (seq_i.is_universe()) 00997 continue; 00998 assign_r(g_coord.get_num(), g.coefficient(Variable(i)), ROUND_NOT_NEEDED); 00999 assign_r(g_coord.get_den(), g_divisor, ROUND_NOT_NEEDED); 01000 g_coord.canonicalize(); 01001 // Check lower bound. 01002 if (!seq_i.lower_is_unbounded()) { 01003 assign_r(bound, seq_i.lower(), ROUND_NOT_NEEDED); 01004 if (g_coord <= bound) { 01005 if (seq_i.lower_is_open()) { 01006 if (g.is_point() || g_coord != bound) 01007 return Poly_Gen_Relation::nothing(); 01008 } 01009 else if (g_coord != bound) 01010 return Poly_Gen_Relation::nothing(); 01011 } 01012 } 01013 // Check upper bound. 01014 if (!seq_i.upper_is_unbounded()) { 01015 assign_r(bound, seq_i.upper(), ROUND_NOT_NEEDED); 01016 if (g_coord >= bound) { 01017 if (seq_i.upper_is_open()) { 01018 if (g.is_point() || g_coord != bound) 01019 return Poly_Gen_Relation::nothing(); 01020 } 01021 else if (g_coord != bound) 01022 return Poly_Gen_Relation::nothing(); 01023 } 01024 } 01025 } 01026 return Poly_Gen_Relation::subsumes(); 01027 }
bool Parma_Polyhedra_Library::Box< ITV >::bounds_from_above | ( | const Linear_Expression & | expr | ) | const [inline] |
Returns true
if and only if expr
is bounded from above in *this
.
std::invalid_argument | Thrown if expr and *this are dimension-incompatible. |
Definition at line 180 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::bounds().
00180 { 00181 return bounds(expr, true); 00182 }
bool Parma_Polyhedra_Library::Box< ITV >::bounds_from_below | ( | const Linear_Expression & | expr | ) | const [inline] |
Returns true
if and only if expr
is bounded from below in *this
.
std::invalid_argument | Thrown if expr and *this are dimension-incompatible. |
Definition at line 186 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::bounds().
00186 { 00187 return bounds(expr, false); 00188 }
bool Parma_Polyhedra_Library::Box< ITV >::maximize | ( | const Linear_Expression & | expr, | |
Coefficient & | sup_n, | |||
Coefficient & | sup_d, | |||
bool & | maximum | |||
) | const [inline] |
Returns true
if and only if *this
is not empty and expr
is bounded from above in *this
, in which case the supremum value is computed.
expr | The linear expression to be maximized subject to *this ; | |
sup_n | The numerator of the supremum value; | |
sup_d | The denominator of the supremum value; | |
maximum | true if and only if the supremum is also the maximum value. |
std::invalid_argument | Thrown if expr and *this are dimension-incompatible. |
*this
is empty or expr
is not bounded from above, false
is returned and sup_n
, sup_d
and maximum
are left untouched.
Definition at line 192 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::max_min().
Referenced by Parma_Polyhedra_Library::Box< ITV >::bounded_affine_image(), Parma_Polyhedra_Library::Box< ITV >::bounded_affine_preimage(), Parma_Polyhedra_Library::Box< ITV >::generalized_affine_image(), and Parma_Polyhedra_Library::Box< ITV >::generalized_affine_preimage().
00194 { 00195 return max_min(expr, true, sup_n, sup_d, maximum); 00196 }
bool Parma_Polyhedra_Library::Box< ITV >::maximize | ( | const Linear_Expression & | expr, | |
Coefficient & | sup_n, | |||
Coefficient & | sup_d, | |||
bool & | maximum, | |||
Generator & | g | |||
) | const [inline] |
Returns true
if and only if *this
is not empty and expr
is bounded from above in *this
, in which case the supremum value and a point where expr
reaches it are computed.
expr | The linear expression to be maximized subject to *this ; | |
sup_n | The numerator of the supremum value; | |
sup_d | The denominator of the supremum value; | |
maximum | true if and only if the supremum is also the maximum value; | |
g | When maximization succeeds, will be assigned the point or closure point where expr reaches its supremum value. |
std::invalid_argument | Thrown if expr and *this are dimension-incompatible. |
*this
is empty or expr
is not bounded from above, false
is returned and sup_n
, sup_d
, maximum
and g
are left untouched.
Definition at line 200 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::max_min().
00202 { 00203 return max_min(expr, true, sup_n, sup_d, maximum, g); 00204 }
bool Parma_Polyhedra_Library::Box< ITV >::minimize | ( | const Linear_Expression & | expr, | |
Coefficient & | inf_n, | |||
Coefficient & | inf_d, | |||
bool & | minimum | |||
) | const [inline] |
Returns true
if and only if *this
is not empty and expr
is bounded from below in *this
, in which case the infimum value is computed.
expr | The linear expression to be minimized subject to *this ; | |
inf_n | The numerator of the infimum value; | |
inf_d | The denominator of the infimum value; | |
minimum | true if and only if the infimum is also the minimum value. |
std::invalid_argument | Thrown if expr and *this are dimension-incompatible. |
*this
is empty or expr
is not bounded from below, false
is returned and inf_n
, inf_d
and minimum
are left untouched.
Definition at line 208 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::max_min().
Referenced by Parma_Polyhedra_Library::Box< ITV >::bounded_affine_image(), Parma_Polyhedra_Library::Box< ITV >::bounded_affine_preimage(), Parma_Polyhedra_Library::Box< ITV >::generalized_affine_image(), and Parma_Polyhedra_Library::Box< ITV >::generalized_affine_preimage().
00210 { 00211 return max_min(expr, false, inf_n, inf_d, minimum); 00212 }
bool Parma_Polyhedra_Library::Box< ITV >::minimize | ( | const Linear_Expression & | expr, | |
Coefficient & | inf_n, | |||
Coefficient & | inf_d, | |||
bool & | minimum, | |||
Generator & | g | |||
) | const [inline] |
Returns true
if and only if *this
is not empty and expr
is bounded from below in *this
, in which case the infimum value and a point where expr
reaches it are computed.
expr | The linear expression to be minimized subject to *this ; | |
inf_n | The numerator of the infimum value; | |
inf_d | The denominator of the infimum value; | |
minimum | true if and only if the infimum is also the minimum value; | |
g | When minimization succeeds, will be assigned a point or closure point where expr reaches its infimum value. |
std::invalid_argument | Thrown if expr and *this are dimension-incompatible. |
*this
is empty or expr
is not bounded from below, false
is returned and inf_n
, inf_d
, minimum
and g
are left untouched.
Definition at line 216 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::max_min().
00218 { 00219 return max_min(expr, false, inf_n, inf_d, minimum, g); 00220 }
bool Parma_Polyhedra_Library::Box< ITV >::contains | ( | const Box< ITV > & | y | ) | const [inline] |
Returns true
if and only if *this
contains y
.
std::invalid_argument | Thrown if x and y are dimension-incompatible. |
Definition at line 1182 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
Referenced by Parma_Polyhedra_Library::Box< ITV >::CC76_narrowing_assign(), Parma_Polyhedra_Library::Box< ITV >::CC76_widening_assign(), and Parma_Polyhedra_Library::Box< ITV >::strictly_contains().
01182 { 01183 const Box& x = *this; 01184 // Dimension-compatibility check. 01185 if (x.space_dimension() != y.space_dimension()) 01186 x.throw_dimension_incompatible("contains(y)", y); 01187 01188 // If `y' is empty, then `x' contains `y'. 01189 if (y.is_empty()) 01190 return true; 01191 01192 // If `x' is empty, then `x' cannot contain `y'. 01193 if (x.is_empty()) 01194 return false; 01195 01196 for (dimension_type k = x.seq.size(); k-- > 0; ) 01197 // FIXME: fix this name qualification issue. 01198 if (!x.seq[k].contains(y.seq[k])) 01199 return false; 01200 return true; 01201 }
bool Parma_Polyhedra_Library::Box< ITV >::strictly_contains | ( | const Box< ITV > & | y | ) | const [inline] |
Returns true
if and only if *this
strictly contains y
.
std::invalid_argument | Thrown if x and y are dimension-incompatible. |
Definition at line 224 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::contains().
00224 { 00225 const Box& x = *this; 00226 return x.contains(y) && !y.contains(x); 00227 }
bool Parma_Polyhedra_Library::Box< ITV >::is_disjoint_from | ( | const Box< ITV > & | y | ) | const [inline] |
Returns true
if and only if *this
and y
are disjoint.
std::invalid_argument | Thrown if x and y are dimension-incompatible. |
Definition at line 1205 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
01205 { 01206 const Box& x = *this; 01207 // Dimension-compatibility check. 01208 if (x.space_dimension() != y.space_dimension()) 01209 x.throw_dimension_incompatible("is_disjoint_from(y)", y); 01210 01211 // If any of `x' or `y' is marked empty, then they are disjoint. 01212 // Note: no need to use `is_empty', as the following loop is anyway correct. 01213 if (x.marked_empty() || y.marked_empty()) 01214 return true; 01215 01216 for (dimension_type k = x.seq.size(); k-- > 0; ) 01217 // FIXME: fix this name qualification issue. 01218 if (x.seq[k].is_disjoint_from(y.seq[k])) 01219 return true; 01220 return false; 01221 }
bool Parma_Polyhedra_Library::Box< ITV >::OK | ( | ) | const [inline] |
Returns true
if and only if *this
satisfies all its invariants.
Definition at line 1225 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::check_empty(), Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::reset_empty_up_to_date(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::status, Parma_Polyhedra_Library::Box< ITV >::Status::test_empty(), and Parma_Polyhedra_Library::Box< ITV >::Status::test_empty_up_to_date().
Referenced by Parma_Polyhedra_Library::Box< ITV >::add_congruences_no_check(), Parma_Polyhedra_Library::Box< ITV >::add_constraints_no_check(), Parma_Polyhedra_Library::Box< ITV >::add_interval_constraint_no_check(), Parma_Polyhedra_Library::Box< ITV >::add_space_dimensions_and_embed(), Parma_Polyhedra_Library::Box< ITV >::add_space_dimensions_and_project(), Parma_Polyhedra_Library::Box< ITV >::affine_image(), Parma_Polyhedra_Library::Box< ITV >::affine_preimage(), Parma_Polyhedra_Library::Box< ITV >::ascii_load(), Parma_Polyhedra_Library::Box< ITV >::bounded_affine_image(), Parma_Polyhedra_Library::Box< ITV >::bounded_affine_preimage(), Parma_Polyhedra_Library::Box< ITV >::Box(), Parma_Polyhedra_Library::Box< ITV >::CC76_narrowing_assign(), Parma_Polyhedra_Library::Box< ITV >::CC76_widening_assign(), Parma_Polyhedra_Library::Box< ITV >::concatenate_assign(), Parma_Polyhedra_Library::Box< ITV >::difference_assign(), Parma_Polyhedra_Library::Box< ITV >::expand_space_dimension(), Parma_Polyhedra_Library::Box< ITV >::generalized_affine_image(), Parma_Polyhedra_Library::Box< ITV >::generalized_affine_preimage(), Parma_Polyhedra_Library::Box< ITV >::intersection_assign(), Parma_Polyhedra_Library::Box< ITV >::map_space_dimensions(), Parma_Polyhedra_Library::Box< ITV >::refine_no_check(), Parma_Polyhedra_Library::Box< ITV >::remove_higher_space_dimensions(), Parma_Polyhedra_Library::Box< ITV >::remove_space_dimensions(), Parma_Polyhedra_Library::Box< ITV >::set_interval(), Parma_Polyhedra_Library::Box< ITV >::time_elapse_assign(), Parma_Polyhedra_Library::Box< ITV >::unconstrain(), and Parma_Polyhedra_Library::Box< ITV >::upper_bound_assign().
01225 { 01226 if (status.test_empty_up_to_date() && !status.test_empty()) { 01227 Box tmp = *this; 01228 tmp.reset_empty_up_to_date(); 01229 if (tmp.check_empty()) { 01230 #ifndef NDEBUG 01231 std::cerr << "The box is empty, but it is marked as non-empty." 01232 << std::endl; 01233 #endif // NDEBUG 01234 return false; 01235 } 01236 } 01237 01238 // A box that is not marked empty must have meaningful intervals. 01239 if (!marked_empty()) { 01240 for (dimension_type k = seq.size(); k-- > 0; ) 01241 if (!seq[k].OK()) 01242 return false; 01243 } 01244 01245 return true; 01246 }
void Parma_Polyhedra_Library::Box< ITV >::add_constraint | ( | const Constraint & | c | ) | [inline] |
Use the constraint c
to refine *this
. FIXME: this is not true.
c | The constraint to be added. If it is not an interval constraint, it will be simply ignored. |
std::invalid_argument | Thrown if *this and c are dimension-incompatible. |
Definition at line 306 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::add_constraint_no_check(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Constraint::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
00306 { 00307 const dimension_type c_space_dim = c.space_dimension(); 00308 // Dimension-compatibility check. 00309 if (c_space_dim > space_dimension()) 00310 throw_dimension_incompatible("add_constraint(c)", c); 00311 00312 add_constraint_no_check(c); 00313 }
void Parma_Polyhedra_Library::Box< ITV >::add_constraints | ( | const Constraint_System & | cs | ) | [inline] |
Use the constraints in cs
to refine *this
. FIXME: this is not true.
cs | The constraints to be added. Constraints that are not interval constraints will be simply ignored. |
std::invalid_argument | Thrown if *this and cs are dimension-incompatible. |
Definition at line 317 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::add_constraints_no_check(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Constraint_System::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
Referenced by Parma_Polyhedra_Library::Box< ITV >::add_recycled_constraints().
00317 { 00318 // Dimension-compatibility check. 00319 if (cs.space_dimension() > space_dimension()) 00320 throw_dimension_incompatible("add_constraints(cs)", cs); 00321 00322 add_constraints_no_check(cs); 00323 }
void Parma_Polyhedra_Library::Box< T >::add_recycled_constraints | ( | Constraint_System & | cs | ) | [inline] |
Use the constraints in cs
to refine *this
. FIXME: this is not true.
cs | The constraints to be added. Constraints that are not interval constraints will be simply ignored. The constraints in cs may be recycled. |
std::invalid_argument | Thrown if *this and cs are dimension-incompatible. |
cs
upon successful or exceptional return is that it can be safely destroyed. Definition at line 327 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::add_constraints().
00327 { 00328 add_constraints(cs); 00329 }
void Parma_Polyhedra_Library::Box< ITV >::add_congruence | ( | const Congruence & | cg | ) | [inline] |
Use the congruence cg
to refine *this
.
cg | The congruence to be used. If it is not a non-relational equality, the box is not changed. |
std::invalid_argument | Thrown if *this and cg are dimension-incompatible. |
Definition at line 333 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::add_congruence_no_check(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Congruence::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
00333 { 00334 const dimension_type cg_space_dim = cg.space_dimension(); 00335 // Dimension-compatibility check. 00336 if (cg_space_dim > space_dimension()) 00337 throw_dimension_incompatible("add_congruence(cg)", cg); 00338 00339 add_congruence_no_check(cg); 00340 }
void Parma_Polyhedra_Library::Box< ITV >::add_congruences | ( | const Congruence_System & | cgs | ) | [inline] |
Use the congruences in cgs
to refine *this
.
cgs | The congruences to be used. Congruences that are not non-relational equalities are not added although their space dimension is checked for compatibility. |
std::invalid_argument | Thrown if *this and cgs are dimension-incompatible. |
Definition at line 344 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::add_congruences_no_check(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Congruence_System::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
Referenced by Parma_Polyhedra_Library::Box< ITV >::add_recycled_congruences().
00344 { 00345 if (cgs.space_dimension() > space_dimension()) 00346 throw_dimension_incompatible("add_congruences(cgs)", cgs); 00347 add_congruences_no_check(cgs); 00348 }
void Parma_Polyhedra_Library::Box< T >::add_recycled_congruences | ( | Congruence_System & | cgs | ) | [inline] |
Use the congruences in cgs
to refine *this
.
cgs | The congruences to be used. Congruences that are not non-relational equalities are not added although their space dimension is checked for compatibility. The congruences in cgs may be recycled. |
std::invalid_argument | Thrown if *this and cgs are dimension-incompatible. |
cgs
upon successful or exceptional return is that it can be safely destroyed. Definition at line 352 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::add_congruences().
00352 { 00353 add_congruences(cgs); 00354 }
void Parma_Polyhedra_Library::Box< ITV >::refine_with_constraint | ( | const Constraint & | c | ) | [inline] |
Use the constraint c
to refine *this
.
c | The constraint to be used for refinement. |
std::invalid_argument | Thrown if *this and c are dimension-incompatible. |
Definition at line 426 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::refine_no_check(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Constraint::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
Referenced by Parma_Polyhedra_Library::Box< ITV >::bounded_affine_image(), Parma_Polyhedra_Library::Box< ITV >::bounded_affine_preimage(), Parma_Polyhedra_Library::Box< ITV >::generalized_affine_image(), and Parma_Polyhedra_Library::Box< ITV >::generalized_affine_preimage().
00426 { 00427 const dimension_type c_space_dim = c.space_dimension(); 00428 // Dimension-compatibility check. 00429 if (c_space_dim > space_dimension()) 00430 throw_dimension_incompatible("refine_with_constraint(c)", c); 00431 00432 // If the box is already empty, there is nothing left to do. 00433 if (marked_empty()) 00434 return; 00435 00436 refine_no_check(c); 00437 }
void Parma_Polyhedra_Library::Box< ITV >::refine_with_constraints | ( | const Constraint_System & | cs | ) | [inline] |
Use the constraints in cs
to refine *this
.
cs | The constraints to be used for refinement. |
std::invalid_argument | Thrown if *this and cs are dimension-incompatible. |
Definition at line 441 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::refine_no_check(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Constraint_System::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
Referenced by Parma_Polyhedra_Library::Box< ITV >::Box().
00441 { 00442 // Dimension-compatibility check. 00443 if (cs.space_dimension() > space_dimension()) 00444 throw_dimension_incompatible("refine_with_constraints(cs)", cs); 00445 00446 // If the box is already empty, there is nothing left to do. 00447 if (marked_empty()) 00448 return; 00449 00450 refine_no_check(cs); 00451 }
void Parma_Polyhedra_Library::Box< ITV >::refine_with_congruence | ( | const Congruence & | cg | ) | [inline] |
Use the congruence cg
to refine *this
.
cg | The congruence to be used for refinement. |
std::invalid_argument | Thrown if *this and cg are dimension-incompatible. |
Definition at line 455 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::refine_no_check(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Congruence::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
00455 { 00456 const dimension_type cg_space_dim = cg.space_dimension(); 00457 // Dimension-compatibility check. 00458 if (cg_space_dim > space_dimension()) 00459 throw_dimension_incompatible("refine_with_congruence(cg)", cg); 00460 00461 // If the box is already empty, there is nothing left to do. 00462 if (marked_empty()) 00463 return; 00464 00465 refine_no_check(cg); 00466 }
void Parma_Polyhedra_Library::Box< ITV >::refine_with_congruences | ( | const Congruence_System & | cgs | ) | [inline] |
Use the congruences in cgs
to refine *this
.
cgs | The congruences to be used for refinement. |
std::invalid_argument | Thrown if *this and cgs are dimension-incompatible. |
Definition at line 470 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::refine_no_check(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Congruence_System::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
00470 { 00471 // Dimension-compatibility check. 00472 if (cgs.space_dimension() > space_dimension()) 00473 throw_dimension_incompatible("refine_with_congruences(cgs)", cgs); 00474 00475 // If the box is already empty, there is nothing left to do. 00476 if (marked_empty()) 00477 return; 00478 00479 refine_no_check(cgs); 00480 }
void Parma_Polyhedra_Library::Box< ITV >::propagate_constraint | ( | const Constraint & | c | ) | [inline] |
Use the constraint c
for constraint propagation on *this
.
c | The constraint to be used for constraint propagation. |
std::invalid_argument | Thrown if *this and c are dimension-incompatible. |
Definition at line 484 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::propagate_constraint_no_check(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Constraint::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
00484 { 00485 const dimension_type c_space_dim = c.space_dimension(); 00486 // Dimension-compatibility check. 00487 if (c_space_dim > space_dimension()) 00488 throw_dimension_incompatible("propagate_constraint(c)", c); 00489 00490 // If the box is already empty, there is nothing left to do. 00491 if (marked_empty()) 00492 return; 00493 00494 propagate_constraint_no_check(c); 00495 }
void Parma_Polyhedra_Library::Box< ITV >::propagate_constraints | ( | const Constraint_System & | cs | ) | [inline] |
Use the constraints in cs
for constraint propagagion on *this
.
cs | The constraints to be used for constraint propagation. |
std::invalid_argument | Thrown if *this and cs are dimension-incompatible. |
Definition at line 499 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::propagate_constraints_no_check(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Constraint_System::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
00499 { 00500 // Dimension-compatibility check. 00501 if (cs.space_dimension() > space_dimension()) 00502 throw_dimension_incompatible("propagate_constraints(cs)", cs); 00503 00504 // If the box is already empty, there is nothing left to do. 00505 if (marked_empty()) 00506 return; 00507 00508 propagate_constraints_no_check(cs); 00509 }
void Parma_Polyhedra_Library::Box< ITV >::unconstrain | ( | Variable | var | ) | [inline] |
Computes the cylindrification of *this
with respect to space dimension var
, assigning the result to *this
.
var | The space dimension that will be unconstrained. |
std::invalid_argument | Thrown if var is not a space dimension of *this . |
Definition at line 513 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Variable::id(), Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::set_empty(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible(), and Parma_Polyhedra_Library::UNIVERSE.
00513 { 00514 const dimension_type dim = var.id(); 00515 // Dimension-compatibility check. 00516 if (dim > space_dimension()) 00517 throw_dimension_incompatible("unconstrain(var)", dim); 00518 00519 // If the box is already empty, there is nothing left to do. 00520 if (marked_empty()) 00521 return; 00522 // Here the box might still be empty (but we haven't detected it yet): 00523 // check emptiness of the interval for `var' before cylindrification. 00524 ITV& seq_var = seq[dim]; 00525 if (seq_var.is_empty()) 00526 set_empty(); 00527 else 00528 seq_var.assign(UNIVERSE); 00529 assert(OK()); 00530 }
void Parma_Polyhedra_Library::Box< ITV >::unconstrain | ( | const Variables_Set & | to_be_unconstrained | ) | [inline] |
Computes the cylindrification of *this
with respect to the set of space dimensions to_be_unconstrained
, assigning the result to *this
.
to_be_unconstrained | The set of space dimension that will be unconstrained. |
std::invalid_argument | Thrown if *this is dimension-incompatible with one of the Variable objects contained in to_be_removed . |
Definition at line 1353 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::set_empty(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible(), and Parma_Polyhedra_Library::UNIVERSE.
01353 { 01354 // The cylindrification wrt no dimensions is a no-op. 01355 // This case also captures the only legal cylindrification 01356 // of a box in a 0-dim space. 01357 if (to_be_unconstrained.empty()) 01358 return; 01359 01360 // Dimension-compatibility check. 01361 const dimension_type min_space_dim = to_be_unconstrained.space_dimension(); 01362 if (space_dimension() < min_space_dim) 01363 throw_dimension_incompatible("unconstrain(vs)", min_space_dim); 01364 01365 // If the box is already empty, there is nothing left to do. 01366 if (marked_empty()) 01367 return; 01368 01369 // Here the box might still be empty (but we haven't detected it yet): 01370 // check emptiness of the interval for each of the variables in 01371 // `to_be_unconstrained' before cylindrification. 01372 for (Variables_Set::const_iterator tbu = to_be_unconstrained.begin(), 01373 tbu_end = to_be_unconstrained.end(); tbu != tbu_end; ++tbu) { 01374 ITV& seq_tbu = seq[*tbu]; 01375 if (!seq_tbu.is_empty()) 01376 seq_tbu.assign(UNIVERSE); 01377 else { 01378 set_empty(); 01379 break; 01380 } 01381 } 01382 assert(OK()); 01383 }
void Parma_Polyhedra_Library::Box< ITV >::intersection_assign | ( | const Box< ITV > & | 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 1397 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::reset_empty_up_to_date(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::set_empty(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
01397 { 01398 Box& x = *this; 01399 const dimension_type space_dim = space_dimension(); 01400 01401 // Dimension-compatibility check. 01402 if (space_dim != y.space_dimension()) 01403 x.throw_dimension_incompatible("intersection_assign(y)", y); 01404 01405 // If one of the two boxes is empty, the intersection is empty. 01406 if (x.marked_empty()) 01407 return; 01408 if (y.marked_empty()) { 01409 x.set_empty(); 01410 return; 01411 } 01412 01413 // If both boxes are zero-dimensional, then at this point they are 01414 // necessarily non-empty, so that their intersection is non-empty too. 01415 if (space_dim == 0) 01416 return; 01417 01418 // FIXME: here we may conditionally exploit a capability of the 01419 // underlying interval to eagerly detect empty results. 01420 reset_empty_up_to_date(); 01421 01422 for (dimension_type k = space_dim; k-- > 0; ) 01423 x.seq[k].intersect_assign(y.seq[k]); 01424 01425 assert(x.OK()); 01426 }
void Parma_Polyhedra_Library::Box< ITV >::upper_bound_assign | ( | const Box< ITV > & | y | ) | [inline] |
Assigns to *this
the smallest box containing the union of *this
and y
.
std::invalid_argument | Thrown if *this and y are dimension-incompatible. |
Definition at line 1430 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
01430 { 01431 Box& x = *this; 01432 01433 // Dimension-compatibility check. 01434 if (x.space_dimension() != y.space_dimension()) 01435 x.throw_dimension_incompatible("upper_bound_assign(y)", y); 01436 01437 // The lub of a box with an empty box is equal to the first box. 01438 if (y.marked_empty()) 01439 return; 01440 if (x.marked_empty()) { 01441 x = y; 01442 return; 01443 } 01444 01445 for (dimension_type k = x.seq.size(); k-- > 0; ) 01446 x.seq[k].join_assign(y.seq[k]); 01447 01448 assert(x.OK()); 01449 }
bool Parma_Polyhedra_Library::Box< ITV >::upper_bound_assign_if_exact | ( | const Box< ITV > & | y | ) | [inline] |
If the upper bound 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 231 of file Box.inlines.hh.
void Parma_Polyhedra_Library::Box< ITV >::difference_assign | ( | const Box< ITV > & | y | ) | [inline] |
Assigns to *this
the difference of *this
and y
.
std::invalid_argument | Thrown if *this and y are dimension-incompatible. |
Definition at line 1490 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::set_empty(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
01490 { 01491 const dimension_type space_dim = space_dimension(); 01492 01493 // Dimension-compatibility check. 01494 if (space_dim != y.space_dimension()) 01495 throw_dimension_incompatible("difference_assign(y)", y); 01496 01497 Box& x = *this; 01498 if (x.is_empty() || y.is_empty()) 01499 return; 01500 01501 switch (space_dim) { 01502 case 0: 01503 // If `x' is zero-dimensional, then at this point both `x' and `y' 01504 // are the universe box, so that their difference is empty. 01505 x.set_empty(); 01506 break; 01507 01508 case 1: 01509 x.seq[0].difference_assign(y.seq[0]); 01510 if (x.seq[0].is_empty()) 01511 x.set_empty(); 01512 break; 01513 01514 default: 01515 { 01516 dimension_type index_non_contained = space_dim; 01517 dimension_type number_non_contained = 0; 01518 for (dimension_type i = space_dim; i-- > 0; ) 01519 if (!y.seq[i].contains(x.seq[i])) { 01520 if (++number_non_contained == 1) 01521 index_non_contained = i; 01522 else 01523 break; 01524 } 01525 01526 switch (number_non_contained) { 01527 case 0: 01528 // `y' covers `x': the difference is empty. 01529 x.set_empty(); 01530 break; 01531 case 1: 01532 x.seq[index_non_contained] 01533 .difference_assign(y.seq[index_non_contained]); 01534 if (x.seq[index_non_contained].is_empty()) 01535 x.set_empty(); 01536 break; 01537 default: 01538 // Nothing to do: the difference is `x'. 01539 break; 01540 } 01541 } 01542 break; 01543 } 01544 assert(OK()); 01545 }
bool Parma_Polyhedra_Library::Box< ITV >::simplify_using_context_assign | ( | const Box< ITV > & | y | ) | [inline] |
Assigns to *this
a meet-preserving simplification of *this
with respect to y
. If false
is returned, then the intersection is empty.
std::invalid_argument | Thrown if *this and y are topology-incompatible or dimension-incompatible. |
Definition at line 1549 of file Box.templates.hh.
void Parma_Polyhedra_Library::Box< ITV >::affine_image | ( | Variable | var, | |
const Linear_Expression & | expr, | |||
Coefficient_traits::const_reference | denominator = Coefficient_one() | |||
) | [inline] |
Assigns to *this
the affine image of *this
under the function mapping variable var
to the affine expression specified by expr
and denominator
.
var | The variable to which the affine expression is assigned; | |
expr | The numerator of the affine expression; | |
denominator | The denominator of the affine expression (optional argument with default value 1). |
std::invalid_argument | Thrown if denominator is zero or if expr and *this are dimension-incompatible or if var is not a space dimension of *this . |
Definition at line 2343 of file Box.templates.hh.
References Parma_Polyhedra_Library::Linear_Expression::coefficient(), Parma_Polyhedra_Library::Variable::id(), Parma_Polyhedra_Library::Linear_Expression::inhomogeneous_term(), Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Variable::space_dimension(), Parma_Polyhedra_Library::Linear_Expression::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible(), and Parma_Polyhedra_Library::Box< ITV >::throw_generic().
Referenced by Parma_Polyhedra_Library::Box< ITV >::affine_preimage(), and Parma_Polyhedra_Library::Box< ITV >::generalized_affine_image().
02345 { 02346 // The denominator cannot be zero. 02347 if (denominator == 0) 02348 throw_generic("affine_image(v, e, d)", "d == 0"); 02349 02350 // Dimension-compatibility checks. 02351 const dimension_type space_dim = space_dimension(); 02352 const dimension_type expr_space_dim = expr.space_dimension(); 02353 if (space_dim < expr_space_dim) 02354 throw_dimension_incompatible("affine_image(v, e, d)", "e", expr); 02355 // `var' should be one of the dimensions of the polyhedron. 02356 const dimension_type var_space_dim = var.space_dimension(); 02357 if (space_dim < var_space_dim) 02358 throw_dimension_incompatible("affine_image(v, e, d)", "v", var); 02359 02360 if (is_empty()) 02361 return; 02362 02363 Tmp_Interval_Type expr_value, temp0, temp1; 02364 expr_value.assign(expr.inhomogeneous_term()); 02365 for (dimension_type i = expr_space_dim; i-- > 0; ) { 02366 const Coefficient& coeff = expr.coefficient(Variable(i)); 02367 if (coeff != 0) { 02368 temp0.assign(coeff); 02369 temp1.assign(seq[i]); 02370 temp0.mul_assign(temp0, temp1); 02371 expr_value.add_assign(expr_value, temp0); 02372 } 02373 } 02374 if (denominator != 1) { 02375 temp0.assign(denominator); 02376 expr_value.div_assign(expr_value, temp0); 02377 } 02378 seq[var.id()].assign(expr_value); 02379 02380 assert(OK()); 02381 }
void Parma_Polyhedra_Library::Box< ITV >::affine_preimage | ( | Variable | var, | |
const Linear_Expression & | expr, | |||
Coefficient_traits::const_reference | denominator = Coefficient_one() | |||
) | [inline] |
Assigns to *this
the affine preimage of *this
under the function mapping variable var
to the affine expression specified by expr
and denominator
.
var | The variable to which the affine expression is substituted; | |
expr | The numerator of the affine expression; | |
denominator | The denominator of the affine expression (optional argument with default value 1). |
std::invalid_argument | Thrown if denominator is zero or if expr and *this are dimension-incompatible or if var is not a space dimension of *this . |
Definition at line 2385 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::affine_image(), Parma_Polyhedra_Library::Linear_Expression::coefficient(), Parma_Polyhedra_Library::Variable::id(), Parma_Polyhedra_Library::Linear_Expression::inhomogeneous_term(), Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::set_empty(), Parma_Polyhedra_Library::Variable::space_dimension(), Parma_Polyhedra_Library::Linear_Expression::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible(), Parma_Polyhedra_Library::Box< ITV >::throw_generic(), and Parma_Polyhedra_Library::UNIVERSE.
Referenced by Parma_Polyhedra_Library::Box< ITV >::generalized_affine_preimage().
02388 { 02389 // The denominator cannot be zero. 02390 if (denominator == 0) 02391 throw_generic("affine_preimage(v, e, d)", "d == 0"); 02392 02393 // Dimension-compatibility checks. 02394 const dimension_type x_space_dim = space_dimension(); 02395 const dimension_type expr_space_dim = expr.space_dimension(); 02396 if (x_space_dim < expr_space_dim) 02397 throw_dimension_incompatible("affine_preimage(v, e, d)", "e", expr); 02398 // `var' should be one of the dimensions of the polyhedron. 02399 const dimension_type var_space_dim = var.space_dimension(); 02400 if (x_space_dim < var_space_dim) 02401 throw_dimension_incompatible("affine_preimage(v, e, d)", "v", var); 02402 02403 if (is_empty()) 02404 return; 02405 02406 const Coefficient& expr_v = expr.coefficient(var); 02407 const bool invertible = (expr_v != 0); 02408 if (!invertible) { 02409 Tmp_Interval_Type expr_value, temp0, temp1; 02410 expr_value.assign(expr.inhomogeneous_term()); 02411 for (dimension_type i = expr_space_dim; i-- > 0; ) { 02412 const Coefficient& coeff = expr.coefficient(Variable(i)); 02413 if (coeff != 0) { 02414 temp0.assign(coeff); 02415 temp1.assign(seq[i]); 02416 temp0.mul_assign(temp0, temp1); 02417 expr_value.add_assign(expr_value, temp0); 02418 } 02419 } 02420 if (denominator != 1) { 02421 temp0.assign(denominator); 02422 expr_value.div_assign(expr_value, temp0); 02423 } 02424 ITV& x_seq_v = seq[var.id()]; 02425 expr_value.intersect_assign(x_seq_v); 02426 if (expr_value.is_empty()) 02427 set_empty(); 02428 else 02429 x_seq_v.assign(UNIVERSE); 02430 } 02431 else { 02432 // The affine transformation is invertible. 02433 // CHECKME: for efficiency, would it be meaningful to avoid 02434 // the computation of inverse by partially evaluating the call 02435 // to affine_image? 02436 Linear_Expression inverse; 02437 inverse -= expr; 02438 inverse += (expr_v + denominator) * var; 02439 affine_image(var, inverse, expr_v); 02440 } 02441 assert(OK()); 02442 }
void Parma_Polyhedra_Library::Box< ITV >::generalized_affine_image | ( | Variable | var, | |
Relation_Symbol | relsym, | |||
const Linear_Expression & | expr, | |||
Coefficient_traits::const_reference | denominator = Coefficient_one() | |||
) | [inline] |
Assigns to *this
the image of *this
with respect to the generalized affine relation , where
is the relation symbol encoded by
relsym
.
var | The left hand side variable of the generalized affine relation; | |
relsym | The relation symbol; | |
expr | The numerator of the right hand side affine expression; | |
denominator | The denominator of the right hand side affine expression (optional argument with default value 1). |
std::invalid_argument | Thrown if denominator is zero or if expr and *this are dimension-incompatible or if var is not a space dimension of *this . |
Definition at line 2755 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::affine_image(), Parma_Polyhedra_Library::EQUAL, Parma_Polyhedra_Library::GREATER_OR_EQUAL, Parma_Polyhedra_Library::GREATER_THAN, Parma_Polyhedra_Library::Variable::id(), Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::LESS_OR_EQUAL, Parma_Polyhedra_Library::LESS_THAN, Parma_Polyhedra_Library::NOT_EQUAL, Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Variable::space_dimension(), Parma_Polyhedra_Library::Linear_Expression::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible(), and Parma_Polyhedra_Library::Box< ITV >::throw_generic().
Referenced by Parma_Polyhedra_Library::Box< ITV >::bounded_affine_image(), and Parma_Polyhedra_Library::Box< ITV >::generalized_affine_preimage().
02758 { 02759 // The denominator cannot be zero. 02760 if (denominator == 0) 02761 throw_generic("generalized_affine_image(v, r, e, d)", "d == 0"); 02762 02763 // Dimension-compatibility checks. 02764 const dimension_type space_dim = space_dimension(); 02765 // The dimension of `expr' should not be greater than the dimension 02766 // of `*this'. 02767 if (space_dim < expr.space_dimension()) 02768 throw_dimension_incompatible("generalized_affine_image(v, r, e, d)", 02769 "e", expr); 02770 // `var' should be one of the dimensions of the box. 02771 const dimension_type var_space_dim = var.space_dimension(); 02772 if (space_dim < var_space_dim) 02773 throw_dimension_incompatible("generalized_affine_image(v, r, e, d)", 02774 "v", var); 02775 02776 // The relation symbol cannot be a disequality. 02777 if (relsym == NOT_EQUAL) 02778 throw_generic("generalized_affine_image(v, r, e, d)", 02779 "r is the disequality relation symbol"); 02780 02781 // First compute the affine image. 02782 affine_image(var, expr, denominator); 02783 02784 if (relsym == EQUAL) 02785 // The affine relation is indeed an affine function. 02786 return; 02787 02788 // Any image of an empty box is empty. 02789 if (is_empty()) 02790 return; 02791 02792 ITV& seq_var = seq[var.id()]; 02793 switch (relsym) { 02794 case LESS_OR_EQUAL: 02795 seq_var.lower_set(UNBOUNDED); 02796 break; 02797 case LESS_THAN: 02798 seq_var.lower_set(UNBOUNDED); 02799 if (!seq_var.upper_is_unbounded()) 02800 seq_var.refine_existential(LESS_THAN, seq_var.upper()); 02801 break; 02802 case GREATER_OR_EQUAL: 02803 seq_var.upper_set(UNBOUNDED); 02804 break; 02805 case GREATER_THAN: 02806 seq_var.upper_set(UNBOUNDED); 02807 if (!seq_var.lower_is_unbounded()) 02808 seq_var.refine_existential(GREATER_THAN, seq_var.lower()); 02809 break; 02810 default: 02811 // The EQUAL and NOT_EQUAL cases have been already dealt with. 02812 throw std::runtime_error("PPL internal error"); 02813 } 02814 assert(OK()); 02815 }
void Parma_Polyhedra_Library::Box< ITV >::generalized_affine_preimage | ( | Variable | var, | |
Relation_Symbol | relsym, | |||
const Linear_Expression & | expr, | |||
Coefficient_traits::const_reference | denominator = Coefficient_one() | |||
) | [inline] |
Assigns to *this
the preimage of *this
with respect to the generalized affine relation , where
is the relation symbol encoded by
relsym
.
var | The left hand side variable of the generalized affine relation; | |
relsym | The relation symbol; | |
expr | The numerator of the right hand side affine expression; | |
denominator | The denominator of the right hand side affine expression (optional argument with default value 1). |
std::invalid_argument | Thrown if denominator is zero or if expr and *this are dimension-incompatible or if var is not a space dimension of *this . |
Definition at line 2820 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::affine_preimage(), Parma_Polyhedra_Library::Linear_Expression::coefficient(), Parma_Polyhedra_Library::EQUAL, Parma_Polyhedra_Library::Box< ITV >::generalized_affine_image(), Parma_Polyhedra_Library::GREATER_OR_EQUAL, Parma_Polyhedra_Library::GREATER_THAN, Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::LESS_OR_EQUAL, Parma_Polyhedra_Library::LESS_THAN, Parma_Polyhedra_Library::Box< ITV >::maximize(), Parma_Polyhedra_Library::Box< ITV >::minimize(), Parma_Polyhedra_Library::neg_assign(), Parma_Polyhedra_Library::NOT_EQUAL, Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::refine_with_constraint(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Variable::space_dimension(), Parma_Polyhedra_Library::Linear_Expression::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), TEMP_INTEGER, Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible(), and Parma_Polyhedra_Library::Box< ITV >::throw_generic().
02824 { 02825 // The denominator cannot be zero. 02826 if (denominator == 0) 02827 throw_generic("generalized_affine_preimage(v, r, e, d)", 02828 "d == 0"); 02829 02830 // Dimension-compatibility checks. 02831 const dimension_type space_dim = space_dimension(); 02832 // The dimension of `expr' should not be greater than the dimension 02833 // of `*this'. 02834 if (space_dim < expr.space_dimension()) 02835 throw_dimension_incompatible("generalized_affine_preimage(v, r, e, d)", 02836 "e", expr); 02837 // `var' should be one of the dimensions of the box. 02838 const dimension_type var_space_dim = var.space_dimension(); 02839 if (space_dim < var_space_dim) 02840 throw_dimension_incompatible("generalized_affine_preimage(v, r, e, d)", 02841 "v", var); 02842 // The relation symbol cannot be a disequality. 02843 if (relsym == NOT_EQUAL) 02844 throw_generic("generalized_affine_preimage(v, r, e, d)", 02845 "r is the disequality relation symbol"); 02846 02847 // Check whether the affine relation is indeed an affine function. 02848 if (relsym == EQUAL) { 02849 affine_preimage(var, expr, denominator); 02850 return; 02851 } 02852 02853 // Compute the reversed relation symbol to simplify later coding. 02854 Relation_Symbol reversed_relsym; 02855 switch (relsym) { 02856 case LESS_THAN: 02857 reversed_relsym = GREATER_THAN; 02858 break; 02859 case LESS_OR_EQUAL: 02860 reversed_relsym = GREATER_OR_EQUAL; 02861 break; 02862 case GREATER_OR_EQUAL: 02863 reversed_relsym = LESS_OR_EQUAL; 02864 break; 02865 case GREATER_THAN: 02866 reversed_relsym = LESS_THAN; 02867 break; 02868 default: 02869 // The EQUAL and NOT_EQUAL cases have been already dealt with. 02870 throw std::runtime_error("PPL internal error"); 02871 } 02872 02873 // Check whether the preimage of this affine relation can be easily 02874 // computed as the image of its inverse relation. 02875 const Coefficient& var_coefficient = expr.coefficient(var); 02876 if (var_coefficient != 0) { 02877 Linear_Expression inverse_expr 02878 = expr - (denominator + var_coefficient) * var; 02879 TEMP_INTEGER(inverse_denominator); 02880 neg_assign(inverse_denominator, var_coefficient); 02881 Relation_Symbol inverse_relsym 02882 = (sgn(denominator) == sgn(inverse_denominator)) 02883 ? relsym : reversed_relsym; 02884 generalized_affine_image(var, inverse_relsym, inverse_expr, 02885 inverse_denominator); 02886 return; 02887 } 02888 02889 // Here `var_coefficient == 0', so that the preimage cannot 02890 // be easily computed by inverting the affine relation. 02891 // Shrink the box by adding the constraint induced 02892 // by the affine relation. 02893 // First, compute the maximum and minimum value reached by 02894 // `denominator*var' on the box as we need to use non-relational 02895 // expressions. 02896 DIRTY_TEMP(Coefficient, max_num); 02897 DIRTY_TEMP(Coefficient, max_den); 02898 bool max_included; 02899 bool bound_above = maximize(denominator*var, max_num, max_den, max_included); 02900 DIRTY_TEMP(Coefficient, min_num); 02901 DIRTY_TEMP(Coefficient, min_den); 02902 bool min_included; 02903 bool bound_below = minimize(denominator*var, min_num, min_den, min_included); 02904 // Use the correct relation symbol 02905 const Relation_Symbol corrected_relsym 02906 = (denominator > 0) ? relsym : reversed_relsym; 02907 // Revise the expression to take into account the denominator of the 02908 // maximum/minimim value for `var'. 02909 DIRTY_TEMP(Linear_Expression, revised_expr); 02910 dimension_type dim = space_dim; 02911 TEMP_INTEGER(d); 02912 if (corrected_relsym == LESS_THAN || corrected_relsym == LESS_OR_EQUAL) { 02913 if (bound_below) { 02914 for ( ; dim > 0; dim--) { 02915 d = min_den * expr.coefficient(Variable(dim - 1)); 02916 revised_expr += d * Variable(dim - 1); 02917 } 02918 } 02919 } 02920 else { 02921 if (bound_above) { 02922 for ( ; dim > 0; dim--) { 02923 d = max_den * expr.coefficient(Variable(dim - 1)); 02924 revised_expr += d * Variable(dim - 1); 02925 } 02926 } 02927 } 02928 02929 switch (corrected_relsym) { 02930 case LESS_THAN: 02931 if (bound_below) 02932 refine_with_constraint(min_num < revised_expr); 02933 break; 02934 case LESS_OR_EQUAL: 02935 if (bound_below) 02936 (min_included) 02937 ? refine_with_constraint(min_num <= revised_expr) 02938 : refine_with_constraint(min_num < revised_expr); 02939 break; 02940 case GREATER_OR_EQUAL: 02941 if (bound_above) 02942 (max_included) 02943 ? refine_with_constraint(max_num >= revised_expr) 02944 : refine_with_constraint(max_num > revised_expr); 02945 break; 02946 case GREATER_THAN: 02947 if (bound_above) 02948 refine_with_constraint(max_num > revised_expr); 02949 break; 02950 default: 02951 // The EQUAL and NOT_EQUAL cases have been already dealt with. 02952 throw std::runtime_error("PPL internal error"); 02953 } 02954 // If the shrunk box is empty, its preimage is empty too. 02955 if (is_empty()) 02956 return; 02957 ITV& seq_v = seq[var.id()]; 02958 seq_v.lower_set(UNBOUNDED); 02959 seq_v.upper_set(UNBOUNDED); 02960 assert(OK()); 02961 }
void Parma_Polyhedra_Library::Box< ITV >::generalized_affine_image | ( | const Linear_Expression & | lhs, | |
Relation_Symbol | relsym, | |||
const Linear_Expression & | rhs | |||
) | [inline] |
Assigns to *this
the image of *this
with respect to the generalized affine relation , 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 . |
Definition at line 2966 of file Box.templates.hh.
References Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::Linear_Expression::coefficient(), Parma_Polyhedra_Library::EQUAL, Parma_Polyhedra_Library::GREATER_OR_EQUAL, Parma_Polyhedra_Library::GREATER_THAN, Parma_Polyhedra_Library::Linear_Expression::inhomogeneous_term(), Parma_Polyhedra_Library::LESS_OR_EQUAL, Parma_Polyhedra_Library::LESS_THAN, Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::maximize(), Parma_Polyhedra_Library::Box< ITV >::minimize(), Parma_Polyhedra_Library::NOT_EQUAL, Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::refine_with_constraint(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Linear_Expression::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible(), and Parma_Polyhedra_Library::Box< ITV >::throw_generic().
02968 { 02969 // Dimension-compatibility checks. 02970 // The dimension of `lhs' should not be greater than the dimension 02971 // of `*this'. 02972 dimension_type lhs_space_dim = lhs.space_dimension(); 02973 const dimension_type space_dim = space_dimension(); 02974 if (space_dim < lhs_space_dim) 02975 throw_dimension_incompatible("generalized_affine_image(e1, r, e2)", 02976 "e1", lhs); 02977 // The dimension of `rhs' should not be greater than the dimension 02978 // of `*this'. 02979 const dimension_type rhs_space_dim = rhs.space_dimension(); 02980 if (space_dim < rhs_space_dim) 02981 throw_dimension_incompatible("generalized_affine_image(e1, r, e2)", 02982 "e2", rhs); 02983 02984 // The relation symbol cannot be a disequality. 02985 if (relsym == NOT_EQUAL) 02986 throw_generic("generalized_affine_image(e1, r, e2)", 02987 "r is the disequality relation symbol"); 02988 02989 // Any image of an empty box is empty. 02990 if (marked_empty()) 02991 return; 02992 02993 // Compute the maximum and minimum value reached by the rhs on the box. 02994 DIRTY_TEMP(Coefficient, max_num); 02995 DIRTY_TEMP(Coefficient, max_den); 02996 bool max_included; 02997 bool max_rhs = maximize(rhs, max_num, max_den, max_included); 02998 DIRTY_TEMP(Coefficient, min_num); 02999 DIRTY_TEMP(Coefficient, min_den); 03000 bool min_included; 03001 bool min_rhs = minimize(rhs, min_num, min_den, min_included); 03002 03003 // Check whether there is 0, 1 or more than one variable in the lhs 03004 // and record the variable with the highest dimension; set the box 03005 // intervals to be unbounded for all other dimensions with non-zero 03006 // coefficients in the lhs. 03007 bool has_var = false; 03008 bool has_more_than_one_var = false; 03009 // Initialization is just to avoid an annoying warning. 03010 dimension_type has_var_id = 0; 03011 for ( ; lhs_space_dim > 0; --lhs_space_dim) 03012 if (lhs.coefficient(Variable(lhs_space_dim - 1)) != 0) { 03013 if (has_var) { 03014 ITV& seq_i = seq[lhs_space_dim - 1]; 03015 seq_i.lower_set(UNBOUNDED); 03016 seq_i.upper_set(UNBOUNDED); 03017 has_more_than_one_var = true; 03018 } 03019 else { 03020 has_var = true; 03021 has_var_id = lhs_space_dim - 1; 03022 } 03023 } 03024 03025 if (has_more_than_one_var) { 03026 // There is more than one dimension with non-zero coefficient, so 03027 // we cannot have any information about the dimensions in the lhs. 03028 // Since all but the highest dimension with non-zero coefficient 03029 // in the lhs have been set unbounded, it remains to set the 03030 // highest dimension in the lhs unbounded. 03031 ITV& seq_var = seq[has_var_id]; 03032 seq_var.lower_set(UNBOUNDED); 03033 seq_var.upper_set(UNBOUNDED); 03034 assert(OK()); 03035 return; 03036 } 03037 03038 if (has_var) { 03039 // There is exactly one dimension with non-zero coefficient. 03040 ITV& seq_var = seq[has_var_id]; 03041 03042 // Compute the new bounds for this dimension defined by the rhs 03043 // expression. 03044 const Coefficient& inhomo = lhs.inhomogeneous_term(); 03045 const Coefficient& coeff = lhs.coefficient(Variable(has_var_id)); 03046 DIRTY_TEMP0(mpq_class, q_max); 03047 DIRTY_TEMP0(mpq_class, q_min); 03048 if (max_rhs) { 03049 max_num -= inhomo * max_den; 03050 max_den *= coeff; 03051 assign_r(q_max.get_num(), max_num, ROUND_NOT_NEEDED); 03052 assign_r(q_max.get_den(), max_den, ROUND_NOT_NEEDED); 03053 q_max.canonicalize(); 03054 } 03055 if (min_rhs) { 03056 min_num -= inhomo * min_den; 03057 min_den *= coeff; 03058 assign_r(q_min.get_num(), min_num, ROUND_NOT_NEEDED); 03059 assign_r(q_min.get_den(), min_den, ROUND_NOT_NEEDED); 03060 q_min.canonicalize(); 03061 } 03062 03063 // The choice as to which bounds should be set depends on the sign 03064 // of the coefficient of the dimension `has_var_id' in the lhs. 03065 if (coeff > 0) 03066 // The coefficient of the dimension in the lhs is +ve. 03067 switch (relsym) { 03068 case LESS_OR_EQUAL: 03069 seq_var.lower_set(UNBOUNDED); 03070 max_rhs 03071 ? seq_var.upper_set(q_max, !max_included) 03072 : seq_var.upper_set(UNBOUNDED); 03073 break; 03074 case LESS_THAN: 03075 seq_var.lower_set(UNBOUNDED); 03076 max_rhs 03077 ? seq_var.upper_set(q_max, true) 03078 : seq_var.upper_set(UNBOUNDED); 03079 break; 03080 case EQUAL: 03081 max_rhs 03082 ? seq_var.upper_set(q_max, !max_included) 03083 : seq_var.upper_set(UNBOUNDED); 03084 min_rhs 03085 ? seq_var.lower_set(q_min, !min_included) 03086 : seq_var.lower_set(UNBOUNDED); 03087 break; 03088 case GREATER_OR_EQUAL: 03089 seq_var.upper_set(UNBOUNDED); 03090 min_rhs 03091 ? seq_var.lower_set(q_min, !min_included) 03092 : seq_var.lower_set(UNBOUNDED); 03093 break; 03094 case GREATER_THAN: 03095 seq_var.upper_set(UNBOUNDED); 03096 min_rhs 03097 ? seq_var.lower_set(q_min, true) 03098 : seq_var.lower_set(UNBOUNDED); 03099 break; 03100 default: 03101 // The NOT_EQUAL case has been already dealt with. 03102 throw std::runtime_error("PPL internal error"); 03103 } 03104 else 03105 // The coefficient of the dimension in the lhs is -ve. 03106 switch (relsym) { 03107 case GREATER_OR_EQUAL: 03108 seq_var.lower_set(UNBOUNDED); 03109 min_rhs 03110 ? seq_var.upper_set(q_min, !min_included) 03111 : seq_var.upper_set(UNBOUNDED); 03112 break; 03113 case GREATER_THAN: 03114 seq_var.lower_set(UNBOUNDED); 03115 min_rhs 03116 ? seq_var.upper_set(q_min, true) 03117 : seq_var.upper_set(UNBOUNDED); 03118 break; 03119 case EQUAL: 03120 max_rhs 03121 ? seq_var.lower_set(q_max, !max_included) 03122 : seq_var.lower_set(UNBOUNDED); 03123 min_rhs 03124 ? seq_var.upper_set(q_min, !min_included) 03125 : seq_var.upper_set(UNBOUNDED); 03126 break; 03127 case LESS_OR_EQUAL: 03128 seq_var.upper_set(UNBOUNDED); 03129 max_rhs 03130 ? seq_var.lower_set(q_max, !max_included) 03131 : seq_var.lower_set(UNBOUNDED); 03132 break; 03133 case LESS_THAN: 03134 seq_var.upper_set(UNBOUNDED); 03135 max_rhs 03136 ? seq_var.lower_set(q_max, true) 03137 : seq_var.lower_set(UNBOUNDED); 03138 break; 03139 default: 03140 // The NOT_EQUAL case has been already dealt with. 03141 throw std::runtime_error("PPL internal error"); 03142 } 03143 } 03144 03145 else { 03146 // The lhs is a constant value, so we just need to add the 03147 // appropriate constraint. 03148 const Coefficient& inhomo = lhs.inhomogeneous_term(); 03149 switch (relsym) { 03150 case LESS_THAN: 03151 refine_with_constraint(inhomo < rhs); 03152 break; 03153 case LESS_OR_EQUAL: 03154 refine_with_constraint(inhomo <= rhs); 03155 break; 03156 case EQUAL: 03157 refine_with_constraint(inhomo == rhs); 03158 break; 03159 case GREATER_OR_EQUAL: 03160 refine_with_constraint(inhomo >= rhs); 03161 break; 03162 case GREATER_THAN: 03163 refine_with_constraint(inhomo > rhs); 03164 break; 03165 default: 03166 // The NOT_EQUAL case has been already dealt with. 03167 throw std::runtime_error("PPL internal error"); 03168 } 03169 } 03170 assert(OK()); 03171 }
void Parma_Polyhedra_Library::Box< ITV >::generalized_affine_preimage | ( | const Linear_Expression & | lhs, | |
Relation_Symbol | relsym, | |||
const Linear_Expression & | rhs | |||
) | [inline] |
Assigns to *this
the preimage of *this
with respect to the generalized affine relation , 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 . |
Definition at line 3175 of file Box.templates.hh.
References Parma_Polyhedra_Library::Linear_Expression::coefficient(), Parma_Polyhedra_Library::Box< ITV >::generalized_affine_image(), Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::NOT_EQUAL, Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Linear_Expression::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible(), and Parma_Polyhedra_Library::Box< ITV >::throw_generic().
03177 { 03178 // Dimension-compatibility checks. 03179 // The dimension of `lhs' should not be greater than the dimension 03180 // of `*this'. 03181 dimension_type lhs_space_dim = lhs.space_dimension(); 03182 const dimension_type space_dim = space_dimension(); 03183 if (space_dim < lhs_space_dim) 03184 throw_dimension_incompatible("generalized_affine_image(e1, r, e2)", 03185 "e1", lhs); 03186 // The dimension of `rhs' should not be greater than the dimension 03187 // of `*this'. 03188 const dimension_type rhs_space_dim = rhs.space_dimension(); 03189 if (space_dim < rhs_space_dim) 03190 throw_dimension_incompatible("generalized_affine_image(e1, r, e2)", 03191 "e2", rhs); 03192 03193 // The relation symbol cannot be a disequality. 03194 if (relsym == NOT_EQUAL) 03195 throw_generic("generalized_affine_image(e1, r, e2)", 03196 "r is the disequality relation symbol"); 03197 03198 // Any image of an empty box is empty. 03199 if (marked_empty()) 03200 return; 03201 03202 // For any dimension occurring in the lhs, swap and change the sign 03203 // of this component for the rhs and lhs. Then use these in a call 03204 // to generalized_affine_image/3. 03205 Linear_Expression revised_lhs = lhs; 03206 Linear_Expression revised_rhs = rhs; 03207 for (dimension_type d = lhs_space_dim; d-- > 0; ) { 03208 const Variable& var = Variable(d); 03209 if (lhs.coefficient(var) != 0) { 03210 DIRTY_TEMP(Coefficient, temp); 03211 temp = rhs.coefficient(var) + lhs.coefficient(var); 03212 revised_rhs -= temp * var; 03213 revised_lhs -= temp * var; 03214 } 03215 } 03216 generalized_affine_image(revised_lhs, relsym, revised_rhs); 03217 assert(OK()); 03218 }
void Parma_Polyhedra_Library::Box< ITV >::bounded_affine_image | ( | Variable | var, | |
const Linear_Expression & | lb_expr, | |||
const Linear_Expression & | ub_expr, | |||
Coefficient_traits::const_reference | denominator = Coefficient_one() | |||
) | [inline] |
Assigns to *this
the image of *this
with respect to the bounded affine relation .
var | The variable updated by the affine relation; | |
lb_expr | The numerator of the lower bounding affine expression; | |
ub_expr | The numerator of the upper bounding affine expression; | |
denominator | The (common) denominator for the lower and upper bounding affine expressions (optional argument with default value 1). |
std::invalid_argument | Thrown if denominator is zero or if lb_expr (resp., ub_expr ) and *this are dimension-incompatible or if var is not a space dimension of *this . |
Definition at line 2447 of file Box.templates.hh.
References Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::Linear_Expression::coefficient(), Parma_Polyhedra_Library::Box< ITV >::generalized_affine_image(), Parma_Polyhedra_Library::GREATER_OR_EQUAL, Parma_Polyhedra_Library::Variable::id(), Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::LESS_OR_EQUAL, Parma_Polyhedra_Library::Box< ITV >::maximize(), Parma_Polyhedra_Library::Box< ITV >::minimize(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::refine_with_constraint(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Variable::space_dimension(), Parma_Polyhedra_Library::Linear_Expression::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible(), and Parma_Polyhedra_Library::Box< ITV >::throw_generic().
02450 { 02451 // The denominator cannot be zero. 02452 if (denominator == 0) 02453 throw_generic("bounded_affine_image(v, lb, ub, d)", "d == 0"); 02454 02455 // Dimension-compatibility checks. 02456 const dimension_type space_dim = space_dimension(); 02457 // The dimension of `lb_expr' and `ub_expr' should not be 02458 // greater than the dimension of `*this'. 02459 const dimension_type lb_space_dim = lb_expr.space_dimension(); 02460 if (space_dim < lb_space_dim) 02461 throw_dimension_incompatible("bounded_affine_image(v, lb, ub, d)", 02462 "lb", lb_expr); 02463 const dimension_type ub_space_dim = ub_expr.space_dimension(); 02464 if (space_dim < ub_space_dim) 02465 throw_dimension_incompatible("bounded_affine_image(v, lb, ub, d)", 02466 "ub", ub_expr); 02467 // `var' should be one of the dimensions of the box. 02468 const dimension_type var_space_dim = var.space_dimension(); 02469 if (space_dim < var_space_dim) 02470 throw_dimension_incompatible("affine_image(v, e, d)", "v", var); 02471 02472 // Any image of an empty box is empty. 02473 if (is_empty()) 02474 return; 02475 02476 // Add the constraint implied by the `lb_expr' and `ub_expr'. 02477 if (denominator > 0) 02478 refine_with_constraint(lb_expr <= ub_expr); 02479 else 02480 refine_with_constraint(lb_expr >= ub_expr); 02481 02482 // Check whether `var' occurs in `lb_expr' and/or `ub_expr'. 02483 if (lb_expr.coefficient(var) == 0) { 02484 // Here `var' can only occur in `ub_expr'. 02485 generalized_affine_image(var, 02486 LESS_OR_EQUAL, 02487 ub_expr, 02488 denominator); 02489 if (denominator > 0) 02490 refine_with_constraint(lb_expr <= denominator*var); 02491 else 02492 refine_with_constraint(denominator*var <= lb_expr); 02493 } 02494 else if (ub_expr.coefficient(var) == 0) { 02495 // Here `var' can only occur in `lb_expr'. 02496 generalized_affine_image(var, 02497 GREATER_OR_EQUAL, 02498 lb_expr, 02499 denominator); 02500 if (denominator > 0) 02501 refine_with_constraint(denominator*var <= ub_expr); 02502 else 02503 refine_with_constraint(ub_expr <= denominator*var); 02504 } 02505 else { 02506 // Here `var' occurs in both `lb_expr' and `ub_expr'. As boxes 02507 // can only use the non-relational constraints, we find the 02508 // maximum/minimum values `ub_expr' and `lb_expr' obtain with the 02509 // box and use these instead of the `ub-expr' and `lb-expr'. 02510 DIRTY_TEMP(Coefficient, max_num); 02511 DIRTY_TEMP(Coefficient, max_den); 02512 bool max_included; 02513 DIRTY_TEMP(Coefficient, min_num); 02514 DIRTY_TEMP(Coefficient, min_den); 02515 bool min_included; 02516 ITV& seq_v = seq[var.id()]; 02517 if (maximize(ub_expr, max_num, max_den, max_included)) { 02518 if (minimize(lb_expr, min_num, min_den, min_included)) { 02519 // The `ub_expr' has a maximum value and the `lb_expr' 02520 // has a minimum value for the box. 02521 // Set the bounds for `var' using the minimum for `lb_expr'. 02522 min_den *= denominator; 02523 DIRTY_TEMP0(mpq_class, q); 02524 assign_r(q.get_num(), min_num, ROUND_NOT_NEEDED); 02525 assign_r(q.get_den(), min_den, ROUND_NOT_NEEDED); 02526 q.canonicalize(); 02527 (denominator > 0) 02528 ? seq_v.lower_set(q, !min_included) 02529 : seq_v.upper_set(q, !min_included); 02530 // Now make the maximum of lb_expr the upper bound. If the 02531 // maximum is not at a box point, then inequality is strict. 02532 max_den *= denominator; 02533 assign_r(q.get_num(), max_num, ROUND_NOT_NEEDED); 02534 assign_r(q.get_den(), max_den, ROUND_NOT_NEEDED); 02535 q.canonicalize(); 02536 (denominator > 0) 02537 ? seq_v.upper_set(q, !max_included) 02538 : seq_v.lower_set(q, !max_included); 02539 } 02540 else { 02541 // The `ub_expr' has a maximum value but the `lb_expr' 02542 // has no minimum value for the box. 02543 // Set the bounds for `var' using the maximum for `lb_expr'. 02544 DIRTY_TEMP0(mpq_class, q); 02545 max_den *= denominator; 02546 assign_r(q.get_num(), max_num, ROUND_NOT_NEEDED); 02547 assign_r(q.get_den(), max_den, ROUND_NOT_NEEDED); 02548 q.canonicalize(); 02549 if (denominator > 0) { 02550 seq_v.lower_set(UNBOUNDED); 02551 seq_v.upper_set(q, !max_included); 02552 } 02553 else { 02554 seq_v.upper_set(UNBOUNDED); 02555 seq_v.lower_set(q, !max_included); 02556 } 02557 } 02558 } 02559 else if (minimize(lb_expr, min_num, min_den, min_included)) { 02560 // The `ub_expr' has no maximum value but the `lb_expr' 02561 // has a minimum value for the box. 02562 // Set the bounds for `var' using the minimum for `lb_expr'. 02563 min_den *= denominator; 02564 DIRTY_TEMP0(mpq_class, q); 02565 assign_r(q.get_num(), min_num, ROUND_NOT_NEEDED); 02566 assign_r(q.get_den(), min_den, ROUND_NOT_NEEDED); 02567 q.canonicalize(); 02568 if (denominator > 0) { 02569 seq_v.upper_set(UNBOUNDED); 02570 seq_v.lower_set(q, !min_included); 02571 } 02572 else { 02573 seq_v.lower_set(UNBOUNDED); 02574 seq_v.upper_set(q, !min_included); 02575 } 02576 } 02577 else { 02578 // The `ub_expr' has no maximum value and the `lb_expr' 02579 // has no minimum value for the box. 02580 // So we set the bounds to be unbounded. 02581 seq_v.upper_set(UNBOUNDED); 02582 seq_v.lower_set(UNBOUNDED); 02583 } 02584 } 02585 assert(OK()); 02586 }
void Parma_Polyhedra_Library::Box< ITV >::bounded_affine_preimage | ( | Variable | var, | |
const Linear_Expression & | lb_expr, | |||
const Linear_Expression & | ub_expr, | |||
Coefficient_traits::const_reference | denominator = Coefficient_one() | |||
) | [inline] |
Assigns to *this
the preimage of *this
with respect to the bounded affine relation .
var | The variable updated by the affine relation; | |
lb_expr | The numerator of the lower bounding affine expression; | |
ub_expr | The numerator of the upper bounding affine expression; | |
denominator | The (common) denominator for the lower and upper bounding affine expressions (optional argument with default value 1). |
std::invalid_argument | Thrown if denominator is zero or if lb_expr (resp., ub_expr ) and *this are dimension-incompatible or if var is not a space dimension of *this . |
Definition at line 2591 of file Box.templates.hh.
References Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::Linear_Expression::coefficient(), Parma_Polyhedra_Library::Variable::id(), Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::maximize(), Parma_Polyhedra_Library::Box< ITV >::minimize(), Parma_Polyhedra_Library::neg_assign(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::refine_with_constraint(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::set_empty(), Parma_Polyhedra_Library::Linear_Expression::space_dimension(), Parma_Polyhedra_Library::Variable::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), TEMP_INTEGER, Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible(), and Parma_Polyhedra_Library::Box< ITV >::throw_generic().
02594 { 02595 // The denominator cannot be zero. 02596 const dimension_type space_dim = space_dimension(); 02597 if (denominator == 0) 02598 throw_generic("bounded_affine_preimage(v, lb, ub, d)", "d == 0"); 02599 02600 // Dimension-compatibility checks. 02601 // `var' should be one of the dimensions of the polyhedron. 02602 const dimension_type var_space_dim = var.space_dimension(); 02603 if (space_dim < var_space_dim) 02604 throw_dimension_incompatible("bounded_affine_preimage(v, lb, ub, d)", 02605 "v", var); 02606 // The dimension of `lb_expr' and `ub_expr' should not be 02607 // greater than the dimension of `*this'. 02608 const dimension_type lb_space_dim = lb_expr.space_dimension(); 02609 if (space_dim < lb_space_dim) 02610 throw_dimension_incompatible("bounded_affine_preimage(v, lb, ub)", 02611 "lb", lb_expr); 02612 const dimension_type ub_space_dim = ub_expr.space_dimension(); 02613 if (space_dim < ub_space_dim) 02614 throw_dimension_incompatible("bounded_affine_preimage(v, lb, ub)", 02615 "ub", ub_expr); 02616 02617 // Any preimage of an empty polyhedron is empty. 02618 if (marked_empty()) 02619 return; 02620 02621 const bool negative_denom = (denominator < 0); 02622 const Coefficient& lb_var_coeff = lb_expr.coefficient(var); 02623 const Coefficient& ub_var_coeff = ub_expr.coefficient(var); 02624 02625 // If the implied constraint between `ub_expr and `lb_expr' is 02626 // independent of `var', then impose it now. 02627 if (lb_var_coeff == ub_var_coeff) { 02628 if (negative_denom) 02629 refine_with_constraint(lb_expr >= ub_expr); 02630 else 02631 refine_with_constraint(lb_expr <= ub_expr); 02632 } 02633 02634 ITV& seq_var = seq[var.id()]; 02635 if (!seq_var.is_universe()) { 02636 // We want to work with a positive denominator, 02637 // so the sign and its (unsigned) value are separated. 02638 TEMP_INTEGER(pos_denominator); 02639 pos_denominator = denominator; 02640 if (negative_denom) 02641 neg_assign(pos_denominator, pos_denominator); 02642 // Store all the information about the upper and lower bounds 02643 // for `var' before making this interval unbounded. 02644 bool open_lower = seq_var.lower_is_open(); 02645 bool unbounded_lower = seq_var.lower_is_unbounded(); 02646 DIRTY_TEMP0(mpq_class, q_seq_var_lower); 02647 DIRTY_TEMP(Coefficient, num_lower); 02648 DIRTY_TEMP(Coefficient, den_lower); 02649 if (!unbounded_lower) { 02650 assign_r(q_seq_var_lower, seq_var.lower(), ROUND_NOT_NEEDED); 02651 assign_r(num_lower, q_seq_var_lower.get_num(), ROUND_NOT_NEEDED); 02652 assign_r(den_lower, q_seq_var_lower.get_den(), ROUND_NOT_NEEDED); 02653 if (negative_denom) 02654 neg_assign(den_lower, den_lower); 02655 num_lower *= pos_denominator; 02656 seq_var.lower_set(UNBOUNDED); 02657 } 02658 bool open_upper = seq_var.upper_is_open(); 02659 bool unbounded_upper = seq_var.upper_is_unbounded(); 02660 DIRTY_TEMP0(mpq_class, q_seq_var_upper); 02661 DIRTY_TEMP(Coefficient, num_upper); 02662 DIRTY_TEMP(Coefficient, den_upper); 02663 if (!unbounded_upper) { 02664 assign_r(q_seq_var_upper, seq_var.upper(), ROUND_NOT_NEEDED); 02665 assign_r(num_upper, q_seq_var_upper.get_num(), ROUND_NOT_NEEDED); 02666 assign_r(den_upper, q_seq_var_upper.get_den(), ROUND_NOT_NEEDED); 02667 if (negative_denom) 02668 neg_assign(den_upper, den_upper); 02669 num_upper *= pos_denominator; 02670 seq_var.upper_set(UNBOUNDED); 02671 } 02672 02673 if (!unbounded_lower) { 02674 // `lb_expr' is revised by removing the `var' component, 02675 // multiplying by `-' denominator of the lower bound for `var', 02676 // and adding the lower bound for `var' to the inhomogeneous term. 02677 Linear_Expression revised_lb_expr(ub_expr); 02678 revised_lb_expr -= ub_var_coeff * var; 02679 DIRTY_TEMP(Coefficient, d); 02680 neg_assign(d, den_lower); 02681 revised_lb_expr *= d; 02682 revised_lb_expr += num_lower; 02683 02684 // Find the minimum value for the revised lower bound expression 02685 // and use this to refine the appropriate bound. 02686 bool included; 02687 DIRTY_TEMP(Coefficient, den); 02688 if (minimize(revised_lb_expr, num_lower, den, included)) { 02689 den_lower *= (den * ub_var_coeff); 02690 DIRTY_TEMP0(mpq_class, q); 02691 assign_r(q.get_num(), num_lower, ROUND_NOT_NEEDED); 02692 assign_r(q.get_den(), den_lower, ROUND_NOT_NEEDED); 02693 q.canonicalize(); 02694 open_lower |= !included; 02695 if ((ub_var_coeff >= 0) ? !negative_denom : negative_denom) 02696 seq_var.lower_narrow(q, open_lower); 02697 else 02698 seq_var.upper_narrow(q, open_lower); 02699 if (seq_var.is_empty()) { 02700 set_empty(); 02701 return; 02702 } 02703 } 02704 } 02705 02706 if (!unbounded_upper) { 02707 // `ub_expr' is revised by removing the `var' component, 02708 // multiplying by `-' denominator of the upper bound for `var', 02709 // and adding the upper bound for `var' to the inhomogeneous term. 02710 Linear_Expression revised_ub_expr(lb_expr); 02711 revised_ub_expr -= lb_var_coeff * var; 02712 DIRTY_TEMP(Coefficient, d); 02713 neg_assign(d, den_upper); 02714 revised_ub_expr *= d; 02715 revised_ub_expr += num_upper; 02716 02717 // Find the maximum value for the revised upper bound expression 02718 // and use this to refine the appropriate bound. 02719 bool included; 02720 DIRTY_TEMP(Coefficient, den); 02721 if (maximize(revised_ub_expr, num_upper, den, included)) { 02722 den_upper *= (den * lb_var_coeff); 02723 DIRTY_TEMP0(mpq_class, q); 02724 assign_r(q.get_num(), num_upper, ROUND_NOT_NEEDED); 02725 assign_r(q.get_den(), den_upper, ROUND_NOT_NEEDED); 02726 q.canonicalize(); 02727 open_upper |= !included; 02728 if ((lb_var_coeff >= 0) ? !negative_denom : negative_denom) 02729 seq_var.upper_narrow(q, open_upper); 02730 else 02731 seq_var.lower_narrow(q, open_upper); 02732 if (seq_var.is_empty()) { 02733 set_empty(); 02734 return; 02735 } 02736 } 02737 } 02738 } 02739 02740 // If the implied constraint between `ub_expr and `lb_expr' is 02741 // dependent on `var', then impose on the new box. 02742 if (lb_var_coeff != ub_var_coeff) { 02743 if (denominator > 0) 02744 refine_with_constraint(lb_expr <= ub_expr); 02745 else 02746 refine_with_constraint(lb_expr >= ub_expr); 02747 } 02748 02749 assert(OK()); 02750 }
void Parma_Polyhedra_Library::Box< ITV >::time_elapse_assign | ( | const Box< ITV > & | 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 1557 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::set_empty(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
01557 { 01558 Box& x = *this; 01559 const dimension_type x_space_dim = x.space_dimension(); 01560 01561 // Dimension-compatibility check. 01562 if (x_space_dim != y.space_dimension()) 01563 x.throw_dimension_incompatible("time_elapse_assign(y)", y); 01564 01565 // Dealing with the zero-dimensional case. 01566 if (x_space_dim == 0) { 01567 if (y.marked_empty()) 01568 x.set_empty(); 01569 return; 01570 } 01571 01572 // If either one of `x' or `y' is empty, the result is empty too. 01573 // Note: if possible, avoid cost of checking for emptiness. 01574 if (x.marked_empty() || y.marked_empty() 01575 || x.is_empty() || y.is_empty()) { 01576 x.set_empty(); 01577 return; 01578 } 01579 01580 for (dimension_type i = x_space_dim; i-- > 0; ) { 01581 ITV& x_seq_i = x.seq[i]; 01582 const ITV& y_seq_i = y.seq[i]; 01583 if (!x_seq_i.lower_is_unbounded()) 01584 if (y_seq_i.lower_is_unbounded() || y_seq_i.lower() < 0) 01585 x_seq_i.lower_set(UNBOUNDED); 01586 if (!x_seq_i.upper_is_unbounded()) 01587 if (y_seq_i.upper_is_unbounded() || y_seq_i.upper() > 0) 01588 x_seq_i.upper_set(UNBOUNDED); 01589 } 01590 assert(x.OK()); 01591 }
void Parma_Polyhedra_Library::Box< ITV >::topological_closure_assign | ( | ) | [inline] |
Assigns to *this
its topological closure.
Definition at line 1387 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::is_empty(), and Parma_Polyhedra_Library::Box< ITV >::seq.
01387 { 01388 if (!ITV::info_type::store_open || is_empty()) 01389 return; 01390 01391 for (dimension_type k = seq.size(); k-- > 0; ) 01392 seq[k].topological_closure_assign(); 01393 }
void Parma_Polyhedra_Library::Box< ITV >::CC76_widening_assign | ( | const Box< ITV > & | y, | |
unsigned * | tp = 0 | |||
) | [inline] |
Assigns to *this
the result of computing the CC76-widening between *this
and y
.
y | A box 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 3235 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::CC76_widening_assign(), and Parma_Polyhedra_Library::Box< ITV >::contains().
Referenced by Parma_Polyhedra_Library::Box< ITV >::CC76_widening_assign(), Parma_Polyhedra_Library::Box< ITV >::limited_CC76_extrapolation_assign(), and Parma_Polyhedra_Library::Box< ITV >::widening_assign().
03235 { 03236 static typename ITV::boundary_type stop_points[] = { 03237 typename ITV::boundary_type(-2), 03238 typename ITV::boundary_type(-1), 03239 typename ITV::boundary_type(0), 03240 typename ITV::boundary_type(1), 03241 typename ITV::boundary_type(2) 03242 }; 03243 03244 Box& x = *this; 03245 // If there are tokens available, work on a temporary copy. 03246 if (tp != 0 && *tp > 0) { 03247 Box<ITV> x_tmp(x); 03248 x_tmp.CC76_widening_assign(y, 0); 03249 // If the widening was not precise, use one of the available tokens. 03250 if (!x.contains(x_tmp)) 03251 --(*tp); 03252 return; 03253 } 03254 x.CC76_widening_assign(y, 03255 stop_points, 03256 stop_points 03257 + sizeof(stop_points)/sizeof(stop_points[0])); 03258 }
void Parma_Polyhedra_Library::Box< ITV >::CC76_widening_assign | ( | const Box< ITV > & | y, | |
Iterator | first, | |||
Iterator | last | |||
) | [inline] |
Assigns to *this
the result of computing the CC76-widening between *this
and y
.
y | A box that must be contained in *this . | |
first | An iterator that points to the first stop-point. | |
last | An iterator that points one past the last stop-point. |
std::invalid_argument | Thrown if *this and y are dimension-incompatible. |
Definition at line 3223 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::CC76_widening_assign(), Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::Box< ITV >::OK(), and Parma_Polyhedra_Library::Box< ITV >::seq.
03223 { 03224 if (y.is_empty()) 03225 return; 03226 03227 for (dimension_type i = seq.size(); i-- > 0; ) 03228 seq[i].CC76_widening_assign(y.seq[i], first, last); 03229 03230 assert(OK()); 03231 }
void Parma_Polyhedra_Library::Box< T >::widening_assign | ( | const Box< ITV > & | y, | |
unsigned * | tp = 0 | |||
) | [inline] |
Same as CC76_widening_assign(y, tp).
Definition at line 370 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::CC76_widening_assign().
00370 { 00371 CC76_widening_assign(y, tp); 00372 }
void Parma_Polyhedra_Library::Box< ITV >::limited_CC76_extrapolation_assign | ( | const Box< ITV > & | 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 box that must be contained in *this . | |
cs | The system of constraints used to improve the widened box. | |
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 3262 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::CC76_widening_assign().
03264 { 03265 // FIXME: should take into account cs. 03266 used(cs); 03267 Box& x = *this; 03268 x.CC76_widening_assign(y, tp); 03269 }
void Parma_Polyhedra_Library::Box< ITV >::CC76_narrowing_assign | ( | const Box< ITV > & | y | ) | [inline] |
Assigns to *this
the result of restoring in y
the constraints of *this
that were lost by CC76-extrapolation applications.
y | A Box 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 decreasing iteration sequence). Hence, the call x.CC76_narrowing_assign(y)
will assign to x
the result of the computation Definition at line 3273 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::contains(), Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
03273 { 03274 const dimension_type space_dim = space_dimension(); 03275 03276 // Dimension-compatibility check. 03277 if (space_dim != y.space_dimension()) 03278 throw_dimension_incompatible("CC76_narrowing_assign(y)", y); 03279 03280 #ifndef NDEBUG 03281 { 03282 // We assume that `*this' is contained in or equal to `y'. 03283 const Box x_copy = *this; 03284 const Box y_copy = y; 03285 assert(y_copy.contains(x_copy)); 03286 } 03287 #endif 03288 03289 // If both boxes are zero-dimensional, 03290 // since `y' contains `*this', we simply return `*this'. 03291 if (space_dim == 0) 03292 return; 03293 03294 // If `y' is empty, since `y' contains `this', `*this' is empty too. 03295 if (y.is_empty()) 03296 return; 03297 // If `*this' is empty, we return. 03298 if (is_empty()) 03299 return; 03300 03301 // Replace each constraint in `*this' by the corresponding constraint 03302 // in `y' if the corresponding inhomogeneous terms are both finite. 03303 for (dimension_type i = space_dim; i-- > 0; ) { 03304 ITV& x_i = seq[i]; 03305 const ITV& y_i = y.seq[i]; 03306 if (!x_i.lower_is_unbounded() 03307 && !y_i.lower_is_unbounded() 03308 && x_i.lower() != y_i.lower()) 03309 x_i.lower() = y_i.lower(); 03310 if (!x_i.upper_is_unbounded() 03311 && !y_i.upper_is_unbounded() 03312 && x_i.upper() != y_i.upper()) 03313 x_i.upper() = y_i.upper(); 03314 } 03315 assert(OK()); 03316 }
void Parma_Polyhedra_Library::Box< ITV >::add_space_dimensions_and_embed | ( | dimension_type | m | ) | [inline] |
Adds m
new dimensions and embeds the old box into the new space.
m | The number of dimensions to add. |
Definition at line 532 of file Box.templates.hh.
References assign(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::seq, and Parma_Polyhedra_Library::UNIVERSE.
00532 { 00533 // Adding no dimensions is a no-op. 00534 if (m == 0) 00535 return; 00536 00537 // To embed an n-dimension space box in a (n+m)-dimension space, 00538 // we just add `m' new universe elements to the sequence. 00539 seq.insert(seq.end(), m, ITV()); 00540 for (dimension_type sz = seq.size(), i = sz - m; i < sz; ++i) 00541 seq[i].assign(UNIVERSE); 00542 assert(OK()); 00543 }
void Parma_Polyhedra_Library::Box< ITV >::add_space_dimensions_and_project | ( | dimension_type | m | ) | [inline] |
Adds m
new dimensions to the box and does not embed it in the new vector space.
m | The number of dimensions to add. |
Definition at line 547 of file Box.templates.hh.
References assign(), Parma_Polyhedra_Library::Box< ITV >::OK(), and Parma_Polyhedra_Library::Box< ITV >::seq.
00547 { 00548 // Adding no dimensions is a no-op. 00549 if (m == 0) 00550 return; 00551 00552 // A add `m' new zero elements to the sequence. 00553 seq.insert(seq.end(), m, ITV()); 00554 for (dimension_type sz = seq.size(), i = sz - m; i < sz; ++i) 00555 seq[i].assign(0); 00556 00557 assert(OK()); 00558 }
void Parma_Polyhedra_Library::Box< ITV >::concatenate_assign | ( | const Box< ITV > & | y | ) | [inline] |
Seeing a box 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 boxes corresponding, on entry, to
*this
and y
, respectively. Upon successful completion, *this
will represent the box 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 1453 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::reset_empty_up_to_date(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::set_empty(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::status, and Parma_Polyhedra_Library::Box< ITV >::Status::test_empty_up_to_date().
01453 { 01454 Box& x = *this; 01455 const dimension_type x_space_dim = x.space_dimension(); 01456 const dimension_type y_space_dim = y.space_dimension(); 01457 01458 // If `y' is marked empty, the result will be empty too. 01459 if (y.marked_empty()) 01460 x.set_empty(); 01461 01462 // If `y' is a 0-dim space box, there is nothing left to do. 01463 if (y_space_dim == 0) 01464 return; 01465 01466 // Here `y_space_dim > 0', so that a non-trivial concatenation will occur: 01467 // make sure that reallocation will occur once at most. 01468 x.seq.reserve(x_space_dim + y_space_dim); 01469 01470 // If `x' is marked empty, then it is sufficient to adjust 01471 // the dimension of the vector space. 01472 if (x.marked_empty()) { 01473 x.seq.insert(x.seq.end(), y_space_dim, ITV()); 01474 assert(x.OK()); 01475 return; 01476 } 01477 01478 // Here neither `x' nor `y' are marked empty: concatenate them. 01479 std::copy(y.seq.begin(), y.seq.end(), 01480 std::back_insert_iterator<Sequence>(x.seq)); 01481 // Update the `empty_up_to_date' flag. 01482 if (!y.status.test_empty_up_to_date()) 01483 reset_empty_up_to_date(); 01484 01485 assert(x.OK()); 01486 }
void Parma_Polyhedra_Library::Box< ITV >::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 1595 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
Referenced by Parma_Polyhedra_Library::Box< ITV >::fold_space_dimensions().
01595 { 01596 // The removal of no dimensions from any box is a no-op. 01597 // Note that this case also captures the only legal removal of 01598 // space dimensions from a box in a zero-dimensional space. 01599 if (to_be_removed.empty()) { 01600 assert(OK()); 01601 return; 01602 } 01603 01604 const dimension_type old_space_dim = space_dimension(); 01605 01606 // Dimension-compatibility check. 01607 const dimension_type tbr_space_dim = to_be_removed.space_dimension(); 01608 if (old_space_dim < tbr_space_dim) 01609 throw_dimension_incompatible("remove_space_dimensions(vs)", 01610 tbr_space_dim); 01611 01612 const dimension_type new_space_dim = old_space_dim - to_be_removed.size(); 01613 01614 // If the box is empty (this must be detected), then resizing is all 01615 // what is needed. If it is not empty and we are removing _all_ the 01616 // dimensions then, again, resizing suffices. 01617 if (is_empty() || new_space_dim == 0) { 01618 seq.resize(new_space_dim); 01619 assert(OK()); 01620 return; 01621 } 01622 01623 // For each variable to be removed, we fill the corresponding interval 01624 // by shifting left those intervals that will not be removed. 01625 Variables_Set::const_iterator tbr = to_be_removed.begin(); 01626 Variables_Set::const_iterator tbr_end = to_be_removed.end(); 01627 dimension_type dst = *tbr; 01628 dimension_type src = dst + 1; 01629 for (++tbr; tbr != tbr_end; ++tbr) { 01630 const dimension_type tbr_next = *tbr; 01631 // All intervals in between are moved to the left. 01632 while (src < tbr_next) 01633 seq[dst++].swap(seq[src++]); 01634 ++src; 01635 } 01636 // Moving the remaining intervals. 01637 while (src < old_space_dim) 01638 seq[dst++].swap(seq[src++]); 01639 01640 assert(dst == new_space_dim); 01641 seq.resize(new_space_dim); 01642 01643 assert(OK()); 01644 }
void Parma_Polyhedra_Library::Box< ITV >::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 1648 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
Referenced by Parma_Polyhedra_Library::Box< ITV >::map_space_dimensions().
01648 { 01649 // Dimension-compatibility check: the variable having 01650 // maximum index is the one occurring last in the set. 01651 const dimension_type old_dim = space_dimension(); 01652 if (new_dim > old_dim) 01653 throw_dimension_incompatible("remove_higher_space_dimensions(nd)", 01654 new_dim); 01655 01656 // The removal of no dimensions from any box is a no-op. 01657 // Note that this case also captures the only legal removal of 01658 // dimensions from a zero-dim space box. 01659 if (new_dim == old_dim) { 01660 assert(OK()); 01661 return; 01662 } 01663 01664 seq.erase(seq.begin() + new_dim, seq.end()); 01665 assert(OK()); 01666 }
void Parma_Polyhedra_Library::Box< ITV >::map_space_dimensions | ( | const Partial_Function & | 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 1671 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::remove_higher_space_dimensions(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::swap().
01671 { 01672 const dimension_type space_dim = space_dimension(); 01673 if (space_dim == 0) 01674 return; 01675 01676 if (pfunc.has_empty_codomain()) { 01677 // All dimensions vanish: the box becomes zero_dimensional. 01678 remove_higher_space_dimensions(0); 01679 return; 01680 } 01681 01682 const dimension_type new_space_dim = pfunc.max_in_codomain() + 1; 01683 // If the box is empty, then simply adjust the space dimension. 01684 if (is_empty()) { 01685 remove_higher_space_dimensions(new_space_dim); 01686 return; 01687 } 01688 01689 // We create a new Box with the new space dimension. 01690 Box<ITV> tmp(new_space_dim); 01691 // Map the intervals, exchanging the indexes. 01692 for (dimension_type i = 0; i < space_dim; ++i) { 01693 dimension_type new_i; 01694 if (pfunc.maps(i, new_i)) 01695 seq[i].swap(tmp.seq[new_i]); 01696 } 01697 swap(tmp); 01698 assert(OK()); 01699 }
void Parma_Polyhedra_Library::Box< ITV >::expand_space_dimension | ( | Variable | var, | |
dimension_type | m | |||
) | [inline] |
Creates m
copies of the space dimension corresponding to var
.
var | The variable corresponding to the space dimension to be replicated; | |
m | The number of replicas to be created. |
std::invalid_argument | Thrown if var does not correspond to a dimension of the vector space. | |
std::length_error | Thrown if adding m new space dimensions would cause the vector space to exceed dimension max_space_dimension() . |
*this
has space dimension var
has space dimension m
new space dimensions Definition at line 238 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Variable::id(), Parma_Polyhedra_Library::Box< ITV >::max_space_dimension(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Variable::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible(), and Parma_Polyhedra_Library::Box< ITV >::throw_generic().
00239 { 00240 const dimension_type space_dim = space_dimension(); 00241 // `var' should be one of the dimensions of the vector space. 00242 if (var.space_dimension() > space_dim) 00243 throw_dimension_incompatible("expand_space_dimension(v, m)", "v", var); 00244 00245 // The space dimension of the resulting Box should not 00246 // overflow the maximum allowed space dimension. 00247 if (m > max_space_dimension() - space_dim) 00248 throw_generic("expand_dimension(v, m)", 00249 "adding m new space dimensions exceeds " 00250 "the maximum allowed space dimension"); 00251 00252 // To expand the space dimension corresponding to variable `var', 00253 // we append to the box `m' copies of the corresponding interval. 00254 seq.insert(seq.end(), m, seq[var.id()]); 00255 assert(OK()); 00256 }
void Parma_Polyhedra_Library::Box< ITV >::fold_space_dimensions | ( | const Variables_Set & | to_be_folded, | |
Variable | var | |||
) | [inline] |
Folds the space dimensions in to_be_folded
into var
.
to_be_folded | The set of Variable objects corresponding to the space dimensions to be folded; | |
var | The variable corresponding to the space dimension that is the destination of the folding operation. |
std::invalid_argument | Thrown if *this is dimension-incompatible with var or with one of the Variable objects contained in to_be_folded . Also thrown if var is contained in to_be_folded . |
*this
has space dimension var
has space dimension to_be_folded
is a set of variables whose maximum space dimension is also less than or equal to var
is not a member of to_be_folded
, then the space dimensions corresponding to variables in to_be_folded
are folded into the Definition at line 1703 of file Box.templates.hh.
References Parma_Polyhedra_Library::Variable::id(), Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::Box< ITV >::remove_space_dimensions(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Variable::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible(), and Parma_Polyhedra_Library::Box< ITV >::throw_generic().
01704 { 01705 const dimension_type space_dim = space_dimension(); 01706 // `var' should be one of the dimensions of the box. 01707 if (var.space_dimension() > space_dim) 01708 throw_dimension_incompatible("fold_space_dimensions(tbf, v)", "v", var); 01709 01710 // The folding of no dimensions is a no-op. 01711 if (to_be_folded.empty()) 01712 return; 01713 01714 // All variables in `to_be_folded' should be dimensions of the box. 01715 if (to_be_folded.space_dimension() > space_dim) 01716 throw_dimension_incompatible("fold_space_dimensions(tbf, ...)", 01717 to_be_folded.space_dimension()); 01718 01719 // Moreover, `var.id()' should not occur in `to_be_folded'. 01720 if (to_be_folded.find(var.id()) != to_be_folded.end()) 01721 throw_generic("fold_space_dimensions(tbf, v)", 01722 "v should not occur in tbf"); 01723 01724 // Note: the check for emptiness is needed for correctness. 01725 if (!is_empty()) { 01726 // Join the interval corresponding to variable `var' with the intervals 01727 // corresponding to the variables in `to_be_folded'. 01728 ITV& seq_v = seq[var.id()]; 01729 for (Variables_Set::const_iterator i = to_be_folded.begin(), 01730 tbf_end = to_be_folded.end(); i != tbf_end; ++i) 01731 seq_v.join_assign(seq[*i]); 01732 } 01733 remove_space_dimensions(to_be_folded); 01734 }
const ITV & Parma_Polyhedra_Library::Box< ITV >::get_interval | ( | Variable | var | ) | const [inline] |
Returns a reference the interval that bounds var
.
std::invalid_argument | Thrown if var is not a space dimension of *this . |
Definition at line 142 of file Box.inlines.hh.
References Parma_Polyhedra_Library::EMPTY, Parma_Polyhedra_Library::Variable::id(), Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Variable::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
00142 { 00143 if (space_dimension() < var.space_dimension()) 00144 throw_dimension_incompatible("get_interval(v)", "v", var); 00145 00146 if (is_empty()) { 00147 static ITV empty_interval(EMPTY); 00148 return empty_interval; 00149 } 00150 00151 return seq[var.id()]; 00152 }
void Parma_Polyhedra_Library::Box< ITV >::set_interval | ( | Variable | var, | |
const ITV & | i | |||
) | [inline] |
Sets to i
the interval that bounds var
.
std::invalid_argument | Thrown if var is not a space dimension of *this . |
Definition at line 156 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Variable::id(), Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::reset_empty_up_to_date(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Variable::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
00156 { 00157 const dimension_type space_dim = space_dimension(); 00158 if (space_dim < var.space_dimension()) 00159 throw_dimension_incompatible("set_interval(v, i)", "v", var); 00160 00161 if (is_empty() && space_dim >= 2) 00162 // If the box is empty, and has dimension >= 2, setting only one 00163 // interval will not make it non-empty. 00164 return; 00165 00166 seq[var.id()] = i; 00167 reset_empty_up_to_date(); 00168 00169 assert(OK()); 00170 }
bool Parma_Polyhedra_Library::Box< ITV >::get_lower_bound | ( | dimension_type | k, | |
bool & | closed, | |||
Coefficient & | n, | |||
Coefficient & | d | |||
) | const [inline] |
If the k
-th space dimension is unbounded below, returns false
. Otherwise returns true
and set closed
, n
and d
accordingly.
Let the interval corresponding to the
k
-th space dimension. If is not bounded from below, simply return
false
. Otherwise, set closed
, n
and d
as follows: closed
is set to true
if the the lower boundary of is closed and is set to
false
otherwise; n
and d
are assigned the integers and
such that the canonical fraction
corresponds to the greatest lower bound of
. The fraction
is in canonical form if and only if
and
have no common factors and
is positive,
being the unique representation for zero.
An undefined behavior is obtained if k
is greater than or equal to the space dimension of *this
.
Definition at line 266 of file Box.inlines.hh.
References Parma_Polyhedra_Library::assign_r(), and Parma_Polyhedra_Library::Box< ITV >::seq.
Referenced by Parma_Polyhedra_Library::Box< ITV >::congruences(), Parma_Polyhedra_Library::Box< ITV >::constraints(), Parma_Polyhedra_Library::Grid::Grid(), Parma_Polyhedra_Library::Box< ITV >::minimized_constraints(), and Parma_Polyhedra_Library::Polyhedron::Polyhedron().
00267 { 00268 assert(k < seq.size()); 00269 const ITV& seq_k = seq[k]; 00270 00271 if (seq_k.lower_is_unbounded()) 00272 return false; 00273 00274 closed = !seq_k.lower_is_open(); 00275 00276 DIRTY_TEMP0(mpq_class, lr); 00277 assign_r(lr, seq_k.lower(), ROUND_NOT_NEEDED); 00278 n = lr.get_num(); 00279 d = lr.get_den(); 00280 00281 return true; 00282 }
bool Parma_Polyhedra_Library::Box< ITV >::get_upper_bound | ( | dimension_type | k, | |
bool & | closed, | |||
Coefficient & | n, | |||
Coefficient & | d | |||
) | const [inline] |
If the k
-th space dimension is unbounded above, returns false
. Otherwise returns true
and set closed
, n
and d
accordingly.
Let the interval corresponding to the
k
-th space dimension. If is not bounded from above, simply return
false
. Otherwise, set closed
, n
and d
as follows: closed
is set to true
if the the upper boundary of is closed and is set to
false
otherwise; n
and d
are assigned the integers and
such that the canonical fraction
corresponds to the least upper bound of
.
An undefined behavior is obtained if k
is greater than or equal to the space dimension of *this
.
Definition at line 286 of file Box.inlines.hh.
References Parma_Polyhedra_Library::assign_r(), and Parma_Polyhedra_Library::Box< ITV >::seq.
Referenced by Parma_Polyhedra_Library::Box< ITV >::constraints(), Parma_Polyhedra_Library::Grid::Grid(), Parma_Polyhedra_Library::Box< ITV >::minimized_constraints(), and Parma_Polyhedra_Library::Polyhedron::Polyhedron().
00287 { 00288 assert(k < seq.size()); 00289 const ITV& seq_k = seq[k]; 00290 00291 if (seq_k.upper_is_unbounded()) 00292 return false; 00293 00294 closed = !seq_k.upper_is_open(); 00295 00296 DIRTY_TEMP0(mpq_class, ur); 00297 assign_r(ur, seq_k.upper(), ROUND_NOT_NEEDED); 00298 n = ur.get_num(); 00299 d = ur.get_den(); 00300 00301 return true; 00302 }
Constraint_System Parma_Polyhedra_Library::Box< ITV >::constraints | ( | ) | const [inline] |
Returns a system of constraints defining *this
.
Definition at line 3320 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::get_lower_bound(), Parma_Polyhedra_Library::Box< ITV >::get_upper_bound(), Parma_Polyhedra_Library::Constraint_System::insert(), Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Constraint_System::zero_dim_empty().
Referenced by Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape(), and Parma_Polyhedra_Library::Octagonal_Shape< T >::Octagonal_Shape().
03320 { 03321 Constraint_System cs; 03322 const dimension_type space_dim = space_dimension(); 03323 if (space_dim == 0) { 03324 if (marked_empty()) 03325 cs = Constraint_System::zero_dim_empty(); 03326 } 03327 else if (marked_empty()) 03328 cs.insert(0*Variable(space_dim-1) <= -1); 03329 else { 03330 // KLUDGE: in the future `cs' will be constructed of the right dimension. 03331 // For the time being, we force the dimension with the following line. 03332 cs.insert(0*Variable(space_dim-1) <= 0); 03333 03334 for (dimension_type k = 0; k < space_dim; ++k) { 03335 bool closed = false; 03336 DIRTY_TEMP(Coefficient, n); 03337 DIRTY_TEMP(Coefficient, d); 03338 if (get_lower_bound(k, closed, n, d)) { 03339 if (closed) 03340 cs.insert(d*Variable(k) >= n); 03341 else 03342 cs.insert(d*Variable(k) > n); 03343 } 03344 if (get_upper_bound(k, closed, n, d)) { 03345 if (closed) 03346 cs.insert(d*Variable(k) <= n); 03347 else 03348 cs.insert(d*Variable(k) < n); 03349 } 03350 } 03351 } 03352 return cs; 03353 }
Constraint_System Parma_Polyhedra_Library::Box< ITV >::minimized_constraints | ( | ) | const [inline] |
Returns a minimized system of constraints defining *this
.
Definition at line 3357 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::get_lower_bound(), Parma_Polyhedra_Library::Box< ITV >::get_upper_bound(), Parma_Polyhedra_Library::Constraint_System::insert(), Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Constraint_System::zero_dim_empty().
03357 { 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 // Make sure emptiness is detected. 03365 else if (is_empty()) 03366 cs.insert(0*Variable(space_dim-1) <= -1); 03367 else { 03368 // KLUDGE: in the future `cs' will be constructed of the right dimension. 03369 // For the time being, we force the dimension with the following line. 03370 cs.insert(0*Variable(space_dim-1) <= 0); 03371 03372 for (dimension_type k = 0; k < space_dim; ++k) { 03373 bool closed = false; 03374 DIRTY_TEMP(Coefficient, n); 03375 DIRTY_TEMP(Coefficient, d); 03376 if (get_lower_bound(k, closed, n, d)) { 03377 if (closed) 03378 // Make sure equality constraints are detected. 03379 if (seq[k].is_singleton()) { 03380 cs.insert(d*Variable(k) == n); 03381 continue; 03382 } 03383 else 03384 cs.insert(d*Variable(k) >= n); 03385 else 03386 cs.insert(d*Variable(k) > n); 03387 } 03388 if (get_upper_bound(k, closed, n, d)) { 03389 if (closed) 03390 cs.insert(d*Variable(k) <= n); 03391 else 03392 cs.insert(d*Variable(k) < n); 03393 } 03394 } 03395 } 03396 return cs; 03397 }
Congruence_System Parma_Polyhedra_Library::Box< ITV >::congruences | ( | ) | const [inline] |
Returns a system of congruences approximating *this
.
Definition at line 3401 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::get_lower_bound(), Parma_Polyhedra_Library::Congruence_System::insert(), Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Congruence_System::zero_dim_empty().
Referenced by Parma_Polyhedra_Library::Box< ITV >::minimized_congruences().
03401 { 03402 Congruence_System cgs; 03403 const dimension_type space_dim = space_dimension(); 03404 if (space_dim == 0) { 03405 if (marked_empty()) 03406 cgs = Congruence_System::zero_dim_empty(); 03407 } 03408 // Make sure emptiness is detected. 03409 else if (is_empty()) 03410 cgs.insert((0*Variable(space_dim-1) %= -1) / 0); 03411 else { 03412 // KLUDGE: in the future `cgs' will be constructed of the right dimension. 03413 // For the time being, we force the dimension with the following line. 03414 cgs.insert(0*Variable(space_dim-1) %= 0); 03415 03416 for (dimension_type k = 0; k < space_dim; ++k) { 03417 bool closed = false; 03418 DIRTY_TEMP(Coefficient, n); 03419 DIRTY_TEMP(Coefficient, d); 03420 if (get_lower_bound(k, closed, n, d) && closed) 03421 // Make sure equality congruences are detected. 03422 if (seq[k].is_singleton()) 03423 cgs.insert((d*Variable(k) %= n) / 0); 03424 } 03425 } 03426 return cgs; 03427 }
Congruence_System Parma_Polyhedra_Library::Box< ITV >::minimized_congruences | ( | ) | const [inline] |
Returns a minimized system of congruences approximating *this
.
Definition at line 376 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::congruences().
00376 { 00377 // Only equalities can be congruences and these are already minimized. 00378 return congruences(); 00379 }
memory_size_type Parma_Polyhedra_Library::Box< ITV >::total_memory_in_bytes | ( | ) | const [inline] |
Returns the total size in bytes of the memory occupied by *this
.
Definition at line 115 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::external_memory_in_bytes().
00115 { 00116 return sizeof(*this) + external_memory_in_bytes(); 00117 }
memory_size_type Parma_Polyhedra_Library::Box< ITV >::external_memory_in_bytes | ( | ) | const [inline] |
Returns the size in bytes of the memory managed by *this
.
Definition at line 3431 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::seq.
Referenced by Parma_Polyhedra_Library::Box< ITV >::total_memory_in_bytes().
03431 { 03432 memory_size_type n = seq.capacity() * sizeof(ITV); 03433 for (dimension_type k = seq.size(); k-- > 0; ) 03434 n += seq[k].external_memory_in_bytes(); 03435 return n; 03436 }
void Parma_Polyhedra_Library::Box< ITV >::ascii_dump | ( | ) | const |
Writes to std::cerr
an ASCII representation of *this
.
Referenced by Parma_Polyhedra_Library::Box< ITV >::ascii_dump().
void Parma_Polyhedra_Library::Box< ITV >::ascii_dump | ( | std::ostream & | s | ) | const [inline] |
Writes to s
an ASCII representation of *this
.
Definition at line 3461 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::ascii_dump(), Parma_Polyhedra_Library::Box< ITV >::Status::ascii_dump(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::status.
03461 { 03462 const char separator = ' '; 03463 status.ascii_dump(s); 03464 const dimension_type space_dim = space_dimension(); 03465 s << "space_dim" << separator << space_dim; 03466 s << "\n"; 03467 for (dimension_type i = 0; i < space_dim; ++i) 03468 seq[i].ascii_dump(s); 03469 }
void Parma_Polyhedra_Library::Box< ITV >::print | ( | ) | const |
Prints *this
to std::cerr
using operator<<
.
bool Parma_Polyhedra_Library::Box< ITV >::ascii_load | ( | std::istream & | s | ) | [inline] |
Loads from s
an ASCII representation (as produced by ascii_dump(std::ostream&) const) and sets *this
accordingly. Returns true
if successful, false
otherwise.
Definition at line 3475 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::Status::ascii_load(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::seq, and Parma_Polyhedra_Library::Box< ITV >::status.
03475 { 03476 if (!status.ascii_load(s)) 03477 return false; 03478 03479 std::string str; 03480 dimension_type space_dim; 03481 if (!(s >> str) || str != "space_dim") 03482 return false; 03483 if (!(s >> space_dim)) 03484 return false; 03485 03486 seq.clear(); 03487 ITV seq_i; 03488 for (dimension_type i = 0; i < space_dim; ++i) { 03489 if (seq_i.ascii_load(s)) 03490 seq.push_back(seq_i); 03491 else 03492 return false; 03493 } 03494 03495 // Check invariants. 03496 assert(OK()); 03497 return true; 03498 }
bool Parma_Polyhedra_Library::Box< ITV >::marked_empty | ( | ) | const [inline, private] |
Returns true
if and only if the box is known to be empty.
The return value false
does not necessarily implies that *this
is non-empty.
Definition at line 37 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::status, Parma_Polyhedra_Library::Box< ITV >::Status::test_empty(), and Parma_Polyhedra_Library::Box< ITV >::Status::test_empty_up_to_date().
Referenced by Parma_Polyhedra_Library::Box< ITV >::add_congruence_no_check(), Parma_Polyhedra_Library::Box< ITV >::add_constraint_no_check(), Parma_Polyhedra_Library::Box< ITV >::add_interval_constraint_no_check(), Parma_Polyhedra_Library::Box< ITV >::bounded_affine_preimage(), Parma_Polyhedra_Library::Box< ITV >::Box(), Parma_Polyhedra_Library::Box< ITV >::check_empty(), Parma_Polyhedra_Library::Box< ITV >::concatenate_assign(), Parma_Polyhedra_Library::Box< ITV >::congruences(), Parma_Polyhedra_Library::Box< ITV >::constrains(), Parma_Polyhedra_Library::Box< ITV >::constraints(), Parma_Polyhedra_Library::Box< ITV >::contains_integer_point(), Parma_Polyhedra_Library::Box< ITV >::generalized_affine_image(), Parma_Polyhedra_Library::Box< ITV >::generalized_affine_preimage(), Parma_Polyhedra_Library::Box< ITV >::intersection_assign(), Parma_Polyhedra_Library::Box< ITV >::is_disjoint_from(), Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::Box< ITV >::is_universe(), Parma_Polyhedra_Library::Box< ITV >::l_m_distance_assign(), Parma_Polyhedra_Library::Box< ITV >::max_min(), Parma_Polyhedra_Library::Box< ITV >::minimized_constraints(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::propagate_constraint(), Parma_Polyhedra_Library::Box< ITV >::propagate_constraints(), Parma_Polyhedra_Library::Box< ITV >::refine_no_check(), Parma_Polyhedra_Library::Box< ITV >::refine_with_congruence(), Parma_Polyhedra_Library::Box< ITV >::refine_with_congruences(), Parma_Polyhedra_Library::Box< ITV >::refine_with_constraint(), Parma_Polyhedra_Library::Box< ITV >::refine_with_constraints(), Parma_Polyhedra_Library::Box< ITV >::time_elapse_assign(), Parma_Polyhedra_Library::Box< ITV >::unconstrain(), and Parma_Polyhedra_Library::Box< ITV >::upper_bound_assign().
00037 { 00038 return status.test_empty_up_to_date() && status.test_empty(); 00039 }
void Parma_Polyhedra_Library::Box< ITV >::set_empty | ( | ) | [inline] |
Causes the box to become empty, i.e., to represent the empty set.
Definition at line 43 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::Status::set_empty(), Parma_Polyhedra_Library::Box< ITV >::Status::set_empty_up_to_date(), and Parma_Polyhedra_Library::Box< ITV >::status.
Referenced by Parma_Polyhedra_Library::Box< ITV >::add_congruence_no_check(), Parma_Polyhedra_Library::Box< ITV >::add_constraint_no_check(), Parma_Polyhedra_Library::Box< ITV >::affine_preimage(), Parma_Polyhedra_Library::Box< ITV >::bounded_affine_preimage(), Parma_Polyhedra_Library::Box< ITV >::Box(), Parma_Polyhedra_Library::Box< ITV >::check_empty(), Parma_Polyhedra_Library::Box< ITV >::concatenate_assign(), Parma_Polyhedra_Library::Box< ITV >::difference_assign(), Parma_Polyhedra_Library::Grid::get_covering_box(), Parma_Polyhedra_Library::Box< ITV >::intersection_assign(), Parma_Polyhedra_Library::Box< ITV >::propagate_constraint_no_check(), Parma_Polyhedra_Library::Box< ITV >::refine_no_check(), Parma_Polyhedra_Library::Box< ITV >::time_elapse_assign(), and Parma_Polyhedra_Library::Box< ITV >::unconstrain().
00043 { 00044 status.set_empty(); 00045 status.set_empty_up_to_date(); 00046 }
void Parma_Polyhedra_Library::Box< ITV >::set_nonempty | ( | ) | [inline, private] |
Marks *this
as definitely not empty.
Definition at line 50 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::Status::reset_empty(), Parma_Polyhedra_Library::Box< ITV >::Status::set_empty_up_to_date(), and Parma_Polyhedra_Library::Box< ITV >::status.
Referenced by Parma_Polyhedra_Library::Box< ITV >::check_empty().
00050 { 00051 status.reset_empty(); 00052 status.set_empty_up_to_date(); 00053 }
void Parma_Polyhedra_Library::Box< ITV >::set_empty_up_to_date | ( | ) | [inline, private] |
Asserts the validity of the empty flag of *this
.
Definition at line 57 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::Status::set_empty_up_to_date(), and Parma_Polyhedra_Library::Box< ITV >::status.
Referenced by Parma_Polyhedra_Library::Box< ITV >::Box().
00057 { 00058 status.set_empty_up_to_date(); 00059 }
void Parma_Polyhedra_Library::Box< ITV >::reset_empty_up_to_date | ( | ) | [inline, private] |
Invalidates empty flag of *this
.
Definition at line 63 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::Status::reset_empty_up_to_date(), and Parma_Polyhedra_Library::Box< ITV >::status.
Referenced by Parma_Polyhedra_Library::Box< ITV >::add_interval_constraint_no_check(), Parma_Polyhedra_Library::Box< ITV >::concatenate_assign(), Parma_Polyhedra_Library::Box< ITV >::intersection_assign(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::propagate_constraint_no_check(), and Parma_Polyhedra_Library::Box< ITV >::set_interval().
00063 { 00064 return status.reset_empty_up_to_date(); 00065 }
bool Parma_Polyhedra_Library::Box< ITV >::check_empty | ( | ) | const [inline, private] |
Checks the hard way whether *this
is an empty box: returns true
if and only if it is so.
Definition at line 1269 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::set_empty(), and Parma_Polyhedra_Library::Box< ITV >::set_nonempty().
Referenced by Parma_Polyhedra_Library::Box< ITV >::is_empty(), and Parma_Polyhedra_Library::Box< ITV >::OK().
01269 { 01270 assert(!marked_empty()); 01271 Box<ITV>& x = const_cast<Box<ITV>&>(*this); 01272 for (dimension_type k = seq.size(); k-- > 0; ) 01273 if (seq[k].is_empty()) { 01274 x.set_empty(); 01275 return true; 01276 } 01277 x.set_nonempty();; 01278 return false; 01279 }
const ITV & Parma_Polyhedra_Library::Box< ITV >::operator[] | ( | dimension_type | k | ) | const [inline, private] |
Returns a reference the interval that bounds the box on the k
-th space dimension.
Definition at line 135 of file Box.inlines.hh.
References Parma_Polyhedra_Library::Box< ITV >::seq.
void Parma_Polyhedra_Library::Box< ITV >::add_interval_constraint_no_check | ( | dimension_type | var_id, | |
Constraint::Type | type, | |||
Coefficient_traits::const_reference | num, | |||
Coefficient_traits::const_reference | den | |||
) | [inline, private] |
WRITE ME.
Definition at line 384 of file Box.inlines.hh.
References Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::EQUAL, Parma_Polyhedra_Library::Constraint::EQUALITY, Parma_Polyhedra_Library::GREATER_OR_EQUAL, Parma_Polyhedra_Library::GREATER_THAN, Parma_Polyhedra_Library::LESS_OR_EQUAL, Parma_Polyhedra_Library::LESS_THAN, Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Constraint::NONSTRICT_INEQUALITY, Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::reset_empty_up_to_date(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Constraint::STRICT_INEQUALITY.
Referenced by Parma_Polyhedra_Library::Box< ITV >::add_congruence_no_check(), Parma_Polyhedra_Library::Box< ITV >::add_constraint_no_check(), and Parma_Polyhedra_Library::Box< ITV >::refine_no_check().
00387 { 00388 assert(!marked_empty()); 00389 assert(var_id < space_dimension()); 00390 assert(den != 0); 00391 00392 // The interval constraint is of the form 00393 // `Variable(var_id) + num / den rel 0', where 00394 // `rel' is either the relation `==', `>=', or `>'. 00395 // For the purpose of refining the interval, this is 00396 // (morally) turned into `Variable(var_id) rel -num/den'. 00397 DIRTY_TEMP0(mpq_class, q); 00398 assign_r(q.get_num(), num, ROUND_NOT_NEEDED); 00399 assign_r(q.get_den(), den, ROUND_NOT_NEEDED); 00400 q.canonicalize(); 00401 // Turn `num/den' into `-num/den'. 00402 q = -q; 00403 00404 ITV& seq_v = seq[var_id]; 00405 switch (type) { 00406 case Constraint::EQUALITY: 00407 seq_v.refine_existential(EQUAL, q); 00408 break; 00409 case Constraint::NONSTRICT_INEQUALITY: 00410 seq_v.refine_existential((den > 0) ? GREATER_OR_EQUAL : LESS_OR_EQUAL, q); 00411 // FIXME: this assertion fails due to a bug in refine. 00412 assert(seq_v.OK()); 00413 break; 00414 case Constraint::STRICT_INEQUALITY: 00415 seq_v.refine_existential((den > 0) ? GREATER_THAN : LESS_THAN, q); 00416 break; 00417 } 00418 // FIXME: do check the value returned by `refine_existential' and 00419 // set `empty' and `empty_up_to_date' as appropriate. 00420 reset_empty_up_to_date(); 00421 assert(OK()); 00422 }
void Parma_Polyhedra_Library::Box< ITV >::add_constraint_no_check | ( | const Constraint & | c | ) | [inline, private] |
WRITE ME.
Definition at line 1738 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::add_interval_constraint_no_check(), Parma_Polyhedra_Library::Constraint::coefficient(), Parma_Polyhedra_Library::Box< ITV >::extract_interval_constraint(), Parma_Polyhedra_Library::Constraint::inhomogeneous_term(), Parma_Polyhedra_Library::Constraint::is_equality(), Parma_Polyhedra_Library::Constraint::is_strict_inequality(), Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::set_empty(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Constraint::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::throw_generic(), and Parma_Polyhedra_Library::Constraint::type().
Referenced by Parma_Polyhedra_Library::Box< ITV >::add_constraint(), and Parma_Polyhedra_Library::Box< ITV >::add_constraints_no_check().
01738 { 01739 const dimension_type c_space_dim = c.space_dimension(); 01740 assert(c_space_dim <= space_dimension()); 01741 01742 dimension_type c_num_vars = 0; 01743 dimension_type c_only_var = 0; 01744 // Throw an exception if c is not an interval constraints. 01745 if (!extract_interval_constraint(c, c_space_dim, c_num_vars, c_only_var)) 01746 throw_generic("add_constraint(c)", "c is not an interval constraint"); 01747 01748 // Throw an exception if c is a nontrivial strict constraint 01749 // and ITV does not support open boundaries. 01750 if (c.is_strict_inequality() && c_num_vars != 0 01751 && !Box::interval_type::info_type::store_open) 01752 throw_generic("add_constraint(c)", "c is a nontrivial strict constraint"); 01753 01754 // Avoid doing useless work if the box is known to be empty. 01755 if (marked_empty()) 01756 return; 01757 01758 const Coefficient& n = c.inhomogeneous_term(); 01759 if (c_num_vars == 0) { 01760 // Dealing with a trivial constraint. 01761 if (n < 0 01762 || (c.is_equality() && n != 0) 01763 || (c.is_strict_inequality() && n == 0)) 01764 set_empty(); 01765 return; 01766 } 01767 01768 assert(c_num_vars == 1); 01769 const Coefficient& d = c.coefficient(Variable(c_only_var)); 01770 add_interval_constraint_no_check(c_only_var, c.type(), n, d); 01771 }
void Parma_Polyhedra_Library::Box< ITV >::add_constraints_no_check | ( | const Constraint_System & | cs | ) | [inline, private] |
WRITE ME.
Definition at line 1775 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::add_constraint_no_check(), Parma_Polyhedra_Library::Constraint_System::begin(), Parma_Polyhedra_Library::Constraint_System::end(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Constraint_System::space_dimension().
Referenced by Parma_Polyhedra_Library::Box< ITV >::add_constraints(), and Parma_Polyhedra_Library::Box< ITV >::Box().
01775 { 01776 assert(cs.space_dimension() <= space_dimension()); 01777 // Note: even when the box is known to be empty, we need to go 01778 // through all the constraints to fulfill the method's contract 01779 // for what concerns exception throwing. 01780 for (Constraint_System::const_iterator i = cs.begin(), 01781 cs_end = cs.end(); i != cs_end; ++i) 01782 add_constraint_no_check(*i); 01783 assert(OK()); 01784 }
void Parma_Polyhedra_Library::Box< ITV >::add_congruence_no_check | ( | const Congruence & | cg | ) | [inline, private] |
WRITE ME.
Definition at line 1788 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::add_interval_constraint_no_check(), Parma_Polyhedra_Library::Congruence::coefficient(), Parma_Polyhedra_Library::Constraint::EQUALITY, Parma_Polyhedra_Library::extract_interval_congruence(), Parma_Polyhedra_Library::Congruence::inhomogeneous_term(), Parma_Polyhedra_Library::Congruence::is_equality(), Parma_Polyhedra_Library::Congruence::is_inconsistent(), Parma_Polyhedra_Library::Congruence::is_proper_congruence(), Parma_Polyhedra_Library::Congruence::is_tautological(), Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::set_empty(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Congruence::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_generic().
Referenced by Parma_Polyhedra_Library::Box< ITV >::add_congruence(), and Parma_Polyhedra_Library::Box< ITV >::add_congruences_no_check().
01788 { 01789 const dimension_type cg_space_dim = cg.space_dimension(); 01790 assert(cg_space_dim <= space_dimension()); 01791 01792 // Set aside the case of proper congruences. 01793 if (cg.is_proper_congruence()) { 01794 if (cg.is_inconsistent()) { 01795 set_empty(); 01796 return; 01797 } 01798 else if (cg.is_tautological()) 01799 return; 01800 else 01801 // FIXME: what about intervals with restrictions? 01802 throw_generic("add_congruence(cg)", 01803 "cg is a nontrivial proper congruence"); 01804 } 01805 01806 assert(cg.is_equality()); 01807 dimension_type cg_num_vars = 0; 01808 dimension_type cg_only_var = 0; 01809 // Throw an exception if c is not an interval congruence. 01810 if (!extract_interval_congruence(cg, cg_space_dim, cg_num_vars, cg_only_var)) 01811 throw_generic("add_congruence(cg)", "cg is not an interval congruence"); 01812 01813 // Avoid doing useless work if the box is known to be empty. 01814 if (marked_empty()) 01815 return; 01816 01817 const Coefficient& n = cg.inhomogeneous_term(); 01818 if (cg_num_vars == 0) { 01819 // Dealing with a trivial equality congruence. 01820 if (n != 0) 01821 set_empty(); 01822 return; 01823 } 01824 01825 assert(cg_num_vars == 1); 01826 const Coefficient& d = cg.coefficient(Variable(cg_only_var)); 01827 add_interval_constraint_no_check(cg_only_var, Constraint::EQUALITY, n, d); 01828 }
void Parma_Polyhedra_Library::Box< ITV >::add_congruences_no_check | ( | const Congruence_System & | cgs | ) | [inline, private] |
WRITE ME.
Definition at line 1832 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::add_congruence_no_check(), Parma_Polyhedra_Library::Congruence_System::begin(), Parma_Polyhedra_Library::Congruence_System::end(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Congruence_System::space_dimension().
Referenced by Parma_Polyhedra_Library::Box< ITV >::add_congruences(), and Parma_Polyhedra_Library::Box< ITV >::Box().
01832 { 01833 assert(cgs.space_dimension() <= space_dimension()); 01834 // Note: even when the box is known to be empty, we need to go 01835 // through all the congruences to fulfill the method's contract 01836 // for what concerns exception throwing. 01837 for (Congruence_System::const_iterator i = cgs.begin(), 01838 cgs_end = cgs.end(); i != cgs_end; ++i) 01839 add_congruence_no_check(*i); 01840 assert(OK()); 01841 }
void Parma_Polyhedra_Library::Box< ITV >::refine_no_check | ( | const Constraint & | c | ) | [inline, private] |
Uses the constraint c
to refine *this
.
c | The constraint to be added. Non-interval constraints are ignored. |
c
and *this
are dimension-incompatible, the behavior is undefined. Definition at line 1845 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::add_interval_constraint_no_check(), Parma_Polyhedra_Library::Constraint::coefficient(), Parma_Polyhedra_Library::Box< ITV >::extract_interval_constraint(), Parma_Polyhedra_Library::Constraint::inhomogeneous_term(), Parma_Polyhedra_Library::Constraint::is_equality(), Parma_Polyhedra_Library::Constraint::is_strict_inequality(), Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::set_empty(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Constraint::space_dimension(), and Parma_Polyhedra_Library::Constraint::type().
Referenced by Parma_Polyhedra_Library::Box< ITV >::refine_no_check(), Parma_Polyhedra_Library::Box< ITV >::refine_with_congruence(), Parma_Polyhedra_Library::Box< ITV >::refine_with_congruences(), Parma_Polyhedra_Library::Box< ITV >::refine_with_constraint(), and Parma_Polyhedra_Library::Box< ITV >::refine_with_constraints().
01845 { 01846 const dimension_type c_space_dim = c.space_dimension(); 01847 assert(c_space_dim <= space_dimension()); 01848 assert(!marked_empty()); 01849 01850 dimension_type c_num_vars = 0; 01851 dimension_type c_only_var = 0; 01852 // Non-interval constraints are ignored. 01853 if (!extract_interval_constraint(c, c_space_dim, c_num_vars, c_only_var)) 01854 return; 01855 01856 const Coefficient& n = c.inhomogeneous_term(); 01857 if (c_num_vars == 0) { 01858 // Dealing with a trivial constraint. 01859 if (n < 0 01860 || (c.is_equality() && n != 0) 01861 || (c.is_strict_inequality() && n == 0)) 01862 set_empty(); 01863 return; 01864 } 01865 01866 assert(c_num_vars == 1); 01867 const Coefficient& d = c.coefficient(Variable(c_only_var)); 01868 add_interval_constraint_no_check(c_only_var, c.type(), n, d); 01869 }
void Parma_Polyhedra_Library::Box< ITV >::refine_no_check | ( | const Constraint_System & | cs | ) | [inline, private] |
Uses the constraints in cs
to refine *this
.
cs | The constraints to be added. Non-interval constraints are ignored. |
cs
and *this
are dimension-incompatible, the behavior is undefined. Definition at line 1873 of file Box.templates.hh.
References Parma_Polyhedra_Library::Constraint_System::begin(), Parma_Polyhedra_Library::Constraint_System::end(), Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::refine_no_check(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Constraint_System::space_dimension().
01873 { 01874 assert(cs.space_dimension() <= space_dimension()); 01875 for (Constraint_System::const_iterator i = cs.begin(), 01876 cs_end = cs.end(); !marked_empty() && i != cs_end; ++i) 01877 refine_no_check(*i); 01878 assert(OK()); 01879 }
void Parma_Polyhedra_Library::Box< ITV >::refine_no_check | ( | const Congruence & | cg | ) | [inline, private] |
Uses the congruence cg
to refine *this
.
cg | The congruence to be added. Nontrivial proper congruences are ignored. |
cg
and *this
are dimension-incompatible, the behavior is undefined. Definition at line 1883 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::add_interval_constraint_no_check(), Parma_Polyhedra_Library::Congruence::coefficient(), Parma_Polyhedra_Library::Constraint::EQUALITY, Parma_Polyhedra_Library::extract_interval_congruence(), Parma_Polyhedra_Library::Congruence::inhomogeneous_term(), Parma_Polyhedra_Library::Congruence::is_equality(), Parma_Polyhedra_Library::Congruence::is_inconsistent(), Parma_Polyhedra_Library::Congruence::is_proper_congruence(), Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::set_empty(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Congruence::space_dimension().
01883 { 01884 assert(!marked_empty()); 01885 01886 const dimension_type cg_space_dim = cg.space_dimension(); 01887 assert(cg_space_dim <= space_dimension()); 01888 01889 if (cg.is_proper_congruence()) { 01890 // FIXME: also deal with the case of interval with restrictions. 01891 // A proper congruences is also an interval constraint 01892 // if and only if it is trivial. 01893 if (cg.is_inconsistent()) 01894 set_empty(); 01895 return; 01896 } 01897 01898 assert(cg.is_equality()); 01899 dimension_type cg_num_vars = 0; 01900 dimension_type cg_only_var = 0; 01901 // Congruences that are not interval congruences are ignored. 01902 if (!extract_interval_congruence(cg, cg_space_dim, cg_num_vars, cg_only_var)) 01903 return; 01904 01905 if (cg_num_vars == 0) { 01906 // Dealing with a trivial congruence. 01907 if (cg.inhomogeneous_term() != 0) 01908 set_empty(); 01909 return; 01910 } 01911 01912 assert(cg_num_vars == 1); 01913 const Coefficient& n = cg.inhomogeneous_term(); 01914 const Coefficient& d = cg.coefficient(Variable(cg_only_var)); 01915 add_interval_constraint_no_check(cg_only_var, Constraint::EQUALITY, n, d); 01916 }
void Parma_Polyhedra_Library::Box< ITV >::refine_no_check | ( | const Congruence_System & | cgs | ) | [inline, private] |
Uses the congruences in cgs
to refine *this
.
cgs | The congruences to be added. Nontrivial proper congruences are ignored. |
cgs
and *this
are dimension-incompatible, the behavior is undefined. Definition at line 1920 of file Box.templates.hh.
References Parma_Polyhedra_Library::Congruence_System::begin(), Parma_Polyhedra_Library::Congruence_System::end(), Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::refine_no_check(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Congruence_System::space_dimension().
01920 { 01921 assert(cgs.space_dimension() <= space_dimension()); 01922 for (Congruence_System::const_iterator i = cgs.begin(), 01923 cgs_end = cgs.end(); !marked_empty() && i != cgs_end; ++i) 01924 refine_no_check(*i); 01925 assert(OK()); 01926 }
void Parma_Polyhedra_Library::Box< ITV >::propagate_constraint_no_check | ( | const Constraint & | c | ) | [inline, private] |
Propagates the constraint c
to refine *this
.
c | The constraint to be propagated. |
c
and *this
are dimension-incompatible, the behavior is undefined.This method may lead to non-termination.
Consider a constraint of the general form
where ,
is a set of indices,
with
for each
, and
. The set
is subdivided into the disjoint sets
and
such that, for each
,
if
and
if
. Suppose that, for each
a variation interval
is known for
and that the infimum and the supremum of
are denoted, respectively, by
and
, where
.
For each , we have
Thus, if for each
and
for each
, we have
and, if ,
for each
and
for each
,
In the first inequality, the relation is strict if , or if
for some
, or if
for some
, or if the computation is inexact. In the second inequality, the relation is strict if
for some
, or if
for some
, or if the computation is inexact.
For each , we have
Thus, if for each
and
for each
, we have
and, if ,
for each
and
for each
,
In the first inequality, the relation is strict if , or if
for some
, or if
for some
, or if the computation is inexact. In the second inequality, the relation is strict if
for some
, or if
for some
, or if the computation is inexact.
Definition at line 1960 of file Box.templates.hh.
References Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::Constraint::coefficient(), Parma_Polyhedra_Library::Constraint::EQUALITY, Parma_Polyhedra_Library::Constraint::inhomogeneous_term(), Parma_Polyhedra_Library::Constraint::NONSTRICT_INEQUALITY, Parma_Polyhedra_Library::propagate_constraint_check_result(), Parma_Polyhedra_Library::Box< ITV >::reset_empty_up_to_date(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::set_empty(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Constraint::space_dimension(), Parma_Polyhedra_Library::Constraint::STRICT_INEQUALITY, Parma_Polyhedra_Library::T_MAYBE, Parma_Polyhedra_Library::T_NO, Parma_Polyhedra_Library::T_YES, and Parma_Polyhedra_Library::Constraint::type().
Referenced by Parma_Polyhedra_Library::Box< ITV >::propagate_constraint(), and Parma_Polyhedra_Library::Box< ITV >::propagate_constraints_no_check().
01960 { 01961 assert(c.space_dimension() <= space_dimension()); 01962 01963 typedef 01964 typename Select_Temp_Boundary_Type<typename ITV::boundary_type>::type 01965 Temp_Boundary_Type; 01966 01967 const dimension_type c_space_dim = c.space_dimension(); 01968 const Constraint::Type c_type = c.type(); 01969 const Coefficient& c_inhomogeneous_term = c.inhomogeneous_term(); 01970 01971 // Find a space dimension having a non-zero coefficient (if any). 01972 dimension_type last_k = c_space_dim; 01973 for (dimension_type k = c_space_dim; k-- > 0; ) { 01974 if (c.coefficient(Variable(k)) != 0) { 01975 last_k = k; 01976 break; 01977 } 01978 } 01979 if (last_k == c_space_dim) { 01980 // Constraint c is trivial: check if it is inconsistent. 01981 if (c_inhomogeneous_term < 0 01982 || (c_inhomogeneous_term == 0 01983 && c_type != Constraint::NONSTRICT_INEQUALITY)) 01984 set_empty(); 01985 return; 01986 } 01987 01988 // Here constraint c is non-trivial. 01989 assert(last_k < c_space_dim); 01990 Result r; 01991 Temp_Boundary_Type t_bound; 01992 Temp_Boundary_Type t_a; 01993 Temp_Boundary_Type t_x; 01994 Ternary open; 01995 for (dimension_type k = last_k+1; k-- > 0; ) { 01996 const Coefficient& a_k = c.coefficient(Variable(k)); 01997 int sgn_a_k = sgn(a_k); 01998 if (sgn_a_k == 0) 01999 continue; 02000 if (sgn_a_k > 0) { 02001 open = (c_type == Constraint::STRICT_INEQUALITY) ? T_YES : T_NO; 02002 if (open == T_NO) 02003 maybe_reset_fpu_inexact<Temp_Boundary_Type>(); 02004 r = assign_r(t_bound, c_inhomogeneous_term, ROUND_UP); 02005 if (propagate_constraint_check_result(r, open)) 02006 goto maybe_refine_upper_1; 02007 r = neg_assign_r(t_bound, t_bound, ROUND_DOWN); 02008 if (propagate_constraint_check_result(r, open)) 02009 goto maybe_refine_upper_1; 02010 for (dimension_type i = last_k+1; i-- > 0; ) { 02011 if (i == k) 02012 continue; 02013 const Coefficient& a_i = c.coefficient(Variable(i)); 02014 int sgn_a_i = sgn(a_i); 02015 if (sgn_a_i == 0) 02016 continue; 02017 ITV& x_i = seq[i]; 02018 if (sgn_a_i < 0) { 02019 if (x_i.lower_is_unbounded()) 02020 goto maybe_refine_upper_1; 02021 r = assign_r(t_a, a_i, ROUND_DOWN); 02022 if (propagate_constraint_check_result(r, open)) 02023 goto maybe_refine_upper_1; 02024 r = assign_r(t_x, x_i.lower(), ROUND_DOWN); 02025 if (propagate_constraint_check_result(r, open)) 02026 goto maybe_refine_upper_1; 02027 if (x_i.lower_is_open()) 02028 open = T_YES; 02029 r = sub_mul_assign_r(t_bound, t_a, t_x, ROUND_DOWN); 02030 if (propagate_constraint_check_result(r, open)) 02031 goto maybe_refine_upper_1; 02032 } 02033 else { 02034 assert(sgn_a_i > 0); 02035 if (x_i.upper_is_unbounded()) 02036 goto maybe_refine_upper_1; 02037 r = assign_r(t_a, a_i, ROUND_UP); 02038 if (propagate_constraint_check_result(r, open)) 02039 goto maybe_refine_upper_1; 02040 r = assign_r(t_x, x_i.upper(), ROUND_UP); 02041 if (propagate_constraint_check_result(r, open)) 02042 goto maybe_refine_upper_1; 02043 if (x_i.upper_is_open()) 02044 open = T_YES; 02045 r = sub_mul_assign_r(t_bound, t_a, t_x, ROUND_DOWN); 02046 if (propagate_constraint_check_result(r, open)) 02047 goto maybe_refine_upper_1; 02048 } 02049 } 02050 r = assign_r(t_a, a_k, ROUND_UP); 02051 if (propagate_constraint_check_result(r, open)) 02052 goto maybe_refine_upper_1; 02053 r = div_assign_r(t_bound, t_bound, t_a, ROUND_DOWN); 02054 if (propagate_constraint_check_result(r, open)) 02055 goto maybe_refine_upper_1; 02056 02057 // Refine the lower bound of `seq[k]' with `t_bound'. 02058 if (open == T_MAYBE 02059 && maybe_check_fpu_inexact<Temp_Boundary_Type>() == 1) 02060 open = T_YES; 02061 seq[k].lower_narrow(t_bound, open == T_YES); 02062 reset_empty_up_to_date(); 02063 maybe_refine_upper_1: 02064 if (c_type != Constraint::EQUALITY) 02065 continue; 02066 open = T_NO; 02067 maybe_reset_fpu_inexact<Temp_Boundary_Type>(); 02068 r = assign_r(t_bound, c_inhomogeneous_term, ROUND_DOWN); 02069 if (propagate_constraint_check_result(r, open)) 02070 goto next_k; 02071 r = neg_assign_r(t_bound, t_bound, ROUND_UP); 02072 if (propagate_constraint_check_result(r, open)) 02073 goto next_k; 02074 for (dimension_type i = c_space_dim; i-- > 0; ) { 02075 if (i == k) 02076 continue; 02077 const Coefficient& a_i = c.coefficient(Variable(i)); 02078 int sgn_a_i = sgn(a_i); 02079 if (sgn_a_i == 0) 02080 continue; 02081 ITV& x_i = seq[i]; 02082 if (sgn_a_i < 0) { 02083 if (x_i.upper_is_unbounded()) 02084 goto next_k; 02085 r = assign_r(t_a, a_i, ROUND_UP); 02086 if (propagate_constraint_check_result(r, open)) 02087 goto next_k; 02088 r = assign_r(t_x, x_i.upper(), ROUND_UP); 02089 if (propagate_constraint_check_result(r, open)) 02090 goto next_k; 02091 if (x_i.upper_is_open()) 02092 open = T_YES; 02093 r = sub_mul_assign_r(t_bound, t_a, t_x, ROUND_UP); 02094 if (propagate_constraint_check_result(r, open)) 02095 goto next_k; 02096 } 02097 else { 02098 assert(sgn_a_i > 0); 02099 if (x_i.lower_is_unbounded()) 02100 goto next_k; 02101 r = assign_r(t_a, a_i, ROUND_DOWN); 02102 if (propagate_constraint_check_result(r, open)) 02103 goto next_k; 02104 r = assign_r(t_x, x_i.lower(), ROUND_DOWN); 02105 if (propagate_constraint_check_result(r, open)) 02106 goto next_k; 02107 if (x_i.lower_is_open()) 02108 open = T_YES; 02109 r = sub_mul_assign_r(t_bound, t_a, t_x, ROUND_UP); 02110 if (propagate_constraint_check_result(r, open)) 02111 goto next_k; 02112 } 02113 } 02114 r = assign_r(t_a, a_k, ROUND_DOWN); 02115 if (propagate_constraint_check_result(r, open)) 02116 goto next_k; 02117 r = div_assign_r(t_bound, t_bound, t_a, ROUND_UP); 02118 if (propagate_constraint_check_result(r, open)) 02119 goto next_k; 02120 02121 // Refine the upper bound of seq[k] with t_bound. 02122 if (open == T_MAYBE 02123 && maybe_check_fpu_inexact<Temp_Boundary_Type>() == 1) 02124 open = T_YES; 02125 seq[k].upper_narrow(t_bound, open == T_YES); 02126 reset_empty_up_to_date(); 02127 } 02128 else { 02129 assert(sgn_a_k < 0); 02130 open = (c_type == Constraint::STRICT_INEQUALITY) ? T_YES : T_NO; 02131 if (open == T_NO) 02132 maybe_reset_fpu_inexact<Temp_Boundary_Type>(); 02133 r = assign_r(t_bound, c_inhomogeneous_term, ROUND_UP); 02134 if (propagate_constraint_check_result(r, open)) 02135 goto maybe_refine_upper_2; 02136 r = neg_assign_r(t_bound, t_bound, ROUND_DOWN); 02137 if (propagate_constraint_check_result(r, open)) 02138 goto maybe_refine_upper_2; 02139 for (dimension_type i = c_space_dim; i-- > 0; ) { 02140 if (i == k) 02141 continue; 02142 const Coefficient& a_i = c.coefficient(Variable(i)); 02143 int sgn_a_i = sgn(a_i); 02144 if (sgn_a_i == 0) 02145 continue; 02146 ITV& x_i = seq[i]; 02147 if (sgn_a_i < 0) { 02148 if (x_i.lower_is_unbounded()) 02149 goto maybe_refine_upper_2; 02150 r = assign_r(t_a, a_i, ROUND_DOWN); 02151 if (propagate_constraint_check_result(r, open)) 02152 goto maybe_refine_upper_2; 02153 r = assign_r(t_x, x_i.lower(), ROUND_DOWN); 02154 if (propagate_constraint_check_result(r, open)) 02155 goto maybe_refine_upper_2; 02156 if (x_i.lower_is_open()) 02157 open = T_YES; 02158 r = sub_mul_assign_r(t_bound, t_a, t_x, ROUND_UP); 02159 if (propagate_constraint_check_result(r, open)) 02160 goto maybe_refine_upper_2; 02161 } 02162 else { 02163 assert(sgn_a_i > 0); 02164 if (x_i.upper_is_unbounded()) 02165 goto maybe_refine_upper_2; 02166 r = assign_r(t_a, a_i, ROUND_UP); 02167 if (propagate_constraint_check_result(r, open)) 02168 goto maybe_refine_upper_2; 02169 r = assign_r(t_x, x_i.upper(), ROUND_UP); 02170 if (propagate_constraint_check_result(r, open)) 02171 goto maybe_refine_upper_2; 02172 if (x_i.upper_is_open()) 02173 open = T_YES; 02174 r = sub_mul_assign_r(t_bound, t_a, t_x, ROUND_UP); 02175 if (propagate_constraint_check_result(r, open)) 02176 goto maybe_refine_upper_2; 02177 } 02178 } 02179 r = assign_r(t_a, a_k, ROUND_UP); 02180 if (propagate_constraint_check_result(r, open)) 02181 goto maybe_refine_upper_2; 02182 r = div_assign_r(t_bound, t_bound, t_a, ROUND_UP); 02183 if (propagate_constraint_check_result(r, open)) 02184 goto maybe_refine_upper_2; 02185 02186 // Refine the upper bound of seq[k] with t_bound. 02187 if (open == T_MAYBE 02188 && maybe_check_fpu_inexact<Temp_Boundary_Type>() == 1) 02189 open = T_YES; 02190 seq[k].upper_narrow(t_bound, open == T_YES); 02191 reset_empty_up_to_date(); 02192 maybe_refine_upper_2: 02193 if (c_type != Constraint::EQUALITY) 02194 continue; 02195 open = T_NO; 02196 maybe_reset_fpu_inexact<Temp_Boundary_Type>(); 02197 r = assign_r(t_bound, c_inhomogeneous_term, ROUND_DOWN); 02198 if (propagate_constraint_check_result(r, open)) 02199 goto next_k; 02200 r = neg_assign_r(t_bound, t_bound, ROUND_UP); 02201 if (propagate_constraint_check_result(r, open)) 02202 goto next_k; 02203 for (dimension_type i = c_space_dim; i-- > 0; ) { 02204 if (i == k) 02205 continue; 02206 const Coefficient& a_i = c.coefficient(Variable(i)); 02207 int sgn_a_i = sgn(a_i); 02208 if (sgn_a_i == 0) 02209 continue; 02210 ITV& x_i = seq[i]; 02211 if (sgn_a_i < 0) { 02212 if (x_i.upper_is_unbounded()) 02213 goto next_k; 02214 r = assign_r(t_a, a_i, ROUND_UP); 02215 if (propagate_constraint_check_result(r, open)) 02216 goto next_k; 02217 r = assign_r(t_x, x_i.upper(), ROUND_UP); 02218 if (propagate_constraint_check_result(r, open)) 02219 goto next_k; 02220 if (x_i.upper_is_open()) 02221 open = T_YES; 02222 r = sub_mul_assign_r(t_bound, t_a, t_x, ROUND_UP); 02223 if (propagate_constraint_check_result(r, open)) 02224 goto next_k; 02225 } 02226 else { 02227 assert(sgn_a_i > 0); 02228 if (x_i.lower_is_unbounded()) 02229 goto next_k; 02230 r = assign_r(t_a, a_i, ROUND_DOWN); 02231 if (propagate_constraint_check_result(r, open)) 02232 goto next_k; 02233 r = assign_r(t_x, x_i.lower(), ROUND_DOWN); 02234 if (propagate_constraint_check_result(r, open)) 02235 goto next_k; 02236 if (x_i.lower_is_open()) 02237 open = T_YES; 02238 r = sub_mul_assign_r(t_bound, t_a, t_x, ROUND_UP); 02239 if (propagate_constraint_check_result(r, open)) 02240 goto next_k; 02241 } 02242 } 02243 r = assign_r(t_a, a_k, ROUND_DOWN); 02244 if (propagate_constraint_check_result(r, open)) 02245 goto next_k; 02246 r = div_assign_r(t_bound, t_bound, t_a, ROUND_DOWN); 02247 if (propagate_constraint_check_result(r, open)) 02248 goto next_k; 02249 02250 // Refine the lower bound of seq[k] with t_bound. 02251 if (open == T_MAYBE 02252 && maybe_check_fpu_inexact<Temp_Boundary_Type>() == 1) 02253 open = T_YES; 02254 seq[k].lower_narrow(t_bound, open == T_YES); 02255 reset_empty_up_to_date(); 02256 } 02257 next_k: 02258 ; 02259 } 02260 }
void Parma_Polyhedra_Library::Box< ITV >::propagate_constraints_no_check | ( | const Constraint_System & | cs | ) | [inline, private] |
Propagates the constraints in cs
to refine *this
.
cs | The constraints to be propagated. |
cs
and *this
are dimension-incompatible, the behavior is undefined.This method may lead to non-termination.
Definition at line 2322 of file Box.templates.hh.
References Parma_Polyhedra_Library::Constraint_System::begin(), Parma_Polyhedra_Library::Constraint_System::end(), Parma_Polyhedra_Library::maybe_abandon(), Parma_Polyhedra_Library::Box< ITV >::propagate_constraint_no_check(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Constraint_System::space_dimension().
Referenced by Parma_Polyhedra_Library::Box< ITV >::propagate_constraints().
02322 { 02323 assert(cs.space_dimension() <= space_dimension()); 02324 02325 bool changed; 02326 do { 02327 Sequence copy(seq); 02328 for (Constraint_System::const_iterator i = cs.begin(), 02329 cs_end = cs.end(); i != cs_end; ++i) 02330 propagate_constraint_no_check(*i); 02331 02332 // Check if the client has requested abandoning all expensive 02333 // computations. If so, the exception specified by the client 02334 // is thrown now. 02335 maybe_abandon(); 02336 02337 changed = (copy != seq); 02338 } while (changed); 02339 }
bool Parma_Polyhedra_Library::Box< ITV >::bounds | ( | const Linear_Expression & | expr, | |
bool | from_above | |||
) | const [inline, private] |
Checks if and how expr
is bounded in *this
.
Returns true
if and only if from_above
is true
and expr
is bounded from above in *this
, or from_above
is false
and expr
is bounded from below in *this
.
expr | The linear expression to test; | |
from_above | true if and only if the boundedness of interest is "from above". |
std::invalid_argument | Thrown if expr and *this are dimension-incompatible. |
Definition at line 581 of file Box.templates.hh.
References Parma_Polyhedra_Library::Linear_Expression::coefficient(), Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Linear_Expression::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
Referenced by Parma_Polyhedra_Library::Box< ITV >::bounds_from_above(), and Parma_Polyhedra_Library::Box< ITV >::bounds_from_below().
00581 { 00582 // `expr' should be dimension-compatible with `*this'. 00583 const dimension_type expr_space_dim = expr.space_dimension(); 00584 const dimension_type space_dim = space_dimension(); 00585 if (space_dim < expr_space_dim) 00586 throw_dimension_incompatible((from_above 00587 ? "bounds_from_above(e)" 00588 : "bounds_from_below(e)"), "e", expr); 00589 // A zero-dimensional or empty Box bounds everything. 00590 if (space_dim == 0 || is_empty()) 00591 return true; 00592 00593 const int from_above_sign = from_above ? 1 : -1; 00594 for (dimension_type i = expr_space_dim; i-- > 0; ) 00595 switch (sgn(expr.coefficient(Variable(i))) * from_above_sign) { 00596 case 1: 00597 if (seq[i].upper_is_unbounded()) 00598 return false; 00599 break; 00600 case 0: 00601 // Nothing to do. 00602 break; 00603 case -1: 00604 if (seq[i].lower_is_unbounded()) 00605 return false; 00606 break; 00607 } 00608 return true; 00609 }
bool Parma_Polyhedra_Library::Box< ITV >::max_min | ( | const Linear_Expression & | expr, | |
bool | maximize, | |||
Coefficient & | ext_n, | |||
Coefficient & | ext_d, | |||
bool & | included, | |||
Generator & | g | |||
) | const [inline, private] |
Maximizes or minimizes expr
subject to *this
.
expr | The linear expression to be maximized or minimized subject to *this ; | |
maximize | true if maximization is what is wanted; | |
ext_n | The numerator of the extremum value; | |
ext_d | The denominator of the extremum value; | |
included | true if and only if the extremum of expr can actually be reached in *this ; | |
g | When maximization or minimization succeeds, will be assigned a point or closure point where expr reaches the corresponding extremum value. |
std::invalid_argument | Thrown if expr and *this are dimension-incompatible. |
*this
is empty or expr
is not bounded in the appropriate direction, false
is returned and ext_n
, ext_d
, included
and g
are left untouched.
Definition at line 1100 of file Box.templates.hh.
References Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::Linear_Expression::coefficient(), Parma_Polyhedra_Library::exact_div_assign(), Parma_Polyhedra_Library::lcm_assign(), Parma_Polyhedra_Library::Generator::point(), Parma_Polyhedra_Library::Box< ITV >::seq, and Parma_Polyhedra_Library::Box< ITV >::space_dimension().
Referenced by Parma_Polyhedra_Library::Box< ITV >::maximize(), and Parma_Polyhedra_Library::Box< ITV >::minimize().
01104 { 01105 if (!max_min(expr, maximize, ext_n, ext_d, included)) 01106 return false; 01107 01108 // Compute generator `g'. 01109 Linear_Expression g_expr; 01110 DIRTY_TEMP(Coefficient, g_divisor); 01111 g_divisor = 1; 01112 const int maximize_sign = maximize ? 1 : -1; 01113 DIRTY_TEMP0(mpq_class, g_coord); 01114 DIRTY_TEMP(Coefficient, num); 01115 DIRTY_TEMP(Coefficient, den); 01116 DIRTY_TEMP(Coefficient, lcm); 01117 DIRTY_TEMP(Coefficient, factor); 01118 for (dimension_type i = space_dimension(); i-- > 0; ) { 01119 const ITV& seq_i = seq[i]; 01120 switch (sgn(expr.coefficient(Variable(i))) * maximize_sign) { 01121 case 1: 01122 assign_r(g_coord, seq_i.upper(), ROUND_NOT_NEEDED); 01123 break; 01124 case 0: 01125 // If 0 belongs to the interval, choose it 01126 // (and directly proceed to the next iteration). 01127 // FIXME: name qualification issue. 01128 if (seq_i.contains(0)) 01129 continue; 01130 if (!seq_i.lower_is_unbounded()) 01131 if (seq_i.lower_is_open()) 01132 if (!seq_i.upper_is_unbounded()) 01133 if (seq_i.upper_is_open()) { 01134 // Bounded and open interval: compute middle point. 01135 assign_r(g_coord, seq_i.lower(), ROUND_NOT_NEEDED); 01136 DIRTY_TEMP0(mpq_class, q_seq_i_upper); 01137 assign_r(q_seq_i_upper, seq_i.upper(), ROUND_NOT_NEEDED); 01138 g_coord += q_seq_i_upper; 01139 g_coord /= 2; 01140 } 01141 else 01142 // The upper bound is in the interval. 01143 assign_r(g_coord, seq_i.upper(), ROUND_NOT_NEEDED); 01144 else { 01145 // Lower is open, upper is unbounded. 01146 assign_r(g_coord, seq_i.lower(), ROUND_NOT_NEEDED); 01147 ++g_coord; 01148 } 01149 else 01150 // The lower bound is in the interval. 01151 assign_r(g_coord, seq_i.lower(), ROUND_NOT_NEEDED); 01152 else { 01153 // Lower is unbounded, hence upper is bounded 01154 // (since we know that 0 does not belong to the interval). 01155 assert(!seq_i.upper_is_unbounded()); 01156 assign_r(g_coord, seq_i.upper(), ROUND_NOT_NEEDED); 01157 if (seq_i.upper_is_open()) 01158 --g_coord; 01159 } 01160 break; 01161 case -1: 01162 assign_r(g_coord, seq_i.lower(), ROUND_NOT_NEEDED); 01163 break; 01164 } 01165 // Add g_coord * Variable(i) to the generator. 01166 assign_r(den, g_coord.get_den(), ROUND_NOT_NEEDED); 01167 lcm_assign(lcm, g_divisor, den); 01168 exact_div_assign(factor, lcm, g_divisor); 01169 g_expr *= factor; 01170 exact_div_assign(factor, lcm, den); 01171 assign_r(num, g_coord.get_num(), ROUND_NOT_NEEDED); 01172 num *= factor; 01173 g_expr += num * Variable(i); 01174 g_divisor = lcm; 01175 } 01176 g = Generator::point(g_expr, g_divisor); 01177 return true; 01178 }
bool Parma_Polyhedra_Library::Box< ITV >::max_min | ( | const Linear_Expression & | expr, | |
bool | maximize, | |||
Coefficient & | ext_n, | |||
Coefficient & | ext_d, | |||
bool & | included | |||
) | const [inline, private] |
Maximizes or minimizes expr
subject to *this
.
expr | The linear expression to be maximized or minimized subject to *this ; | |
maximize | true if maximization is what is wanted; | |
ext_n | The numerator of the extremum value; | |
ext_d | The denominator of the extremum value; | |
included | true if and only if the extremum of expr can actually be reached in * this; |
std::invalid_argument | Thrown if expr and *this are dimension-incompatible. |
*this
is empty or expr
is not bounded in the appropriate direction, false
is returned and ext_n
, ext_d
, included
and point
are left untouched.
Definition at line 1032 of file Box.templates.hh.
References Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::Linear_Expression::coefficient(), Parma_Polyhedra_Library::Linear_Expression::inhomogeneous_term(), Parma_Polyhedra_Library::is_canonical(), Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::seq, Parma_Polyhedra_Library::Linear_Expression::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().
01035 { 01036 // `expr' should be dimension-compatible with `*this'. 01037 const dimension_type space_dim = space_dimension(); 01038 const dimension_type expr_space_dim = expr.space_dimension(); 01039 if (space_dim < expr_space_dim) 01040 throw_dimension_incompatible((maximize 01041 ? "maximize(e, ...)" 01042 : "minimize(e, ...)"), "e", expr); 01043 // Deal with zero-dim Box first. 01044 if (space_dim == 0) { 01045 if (marked_empty()) 01046 return false; 01047 else { 01048 ext_n = expr.inhomogeneous_term(); 01049 ext_d = 1; 01050 included = true; 01051 return true; 01052 } 01053 } 01054 01055 // For an empty Box we simply return false. 01056 if (is_empty()) 01057 return false; 01058 01059 DIRTY_TEMP0(mpq_class, result); 01060 assign_r(result, expr.inhomogeneous_term(), ROUND_NOT_NEEDED); 01061 bool is_included = true; 01062 const int maximize_sign = maximize ? 1 : -1; 01063 DIRTY_TEMP0(mpq_class, bound_i); 01064 DIRTY_TEMP0(mpq_class, expr_i); 01065 for (dimension_type i = expr_space_dim; i-- > 0; ) { 01066 const ITV& seq_i = seq[i]; 01067 assign_r(expr_i, expr.coefficient(Variable(i)), ROUND_NOT_NEEDED); 01068 switch (sgn(expr_i) * maximize_sign) { 01069 case 1: 01070 if (seq_i.upper_is_unbounded()) 01071 return false; 01072 assign_r(bound_i, seq_i.upper(), ROUND_NOT_NEEDED); 01073 add_mul_assign_r(result, bound_i, expr_i, ROUND_NOT_NEEDED); 01074 if (seq_i.upper_is_open()) 01075 is_included = false; 01076 break; 01077 case 0: 01078 // Nothing to do. 01079 break; 01080 case -1: 01081 if (seq_i.lower_is_unbounded()) 01082 return false; 01083 assign_r(bound_i, seq_i.lower(), ROUND_NOT_NEEDED); 01084 add_mul_assign_r(result, bound_i, expr_i, ROUND_NOT_NEEDED); 01085 if (seq_i.lower_is_open()) 01086 is_included = false; 01087 break; 01088 } 01089 } 01090 // Extract output info. 01091 assert(is_canonical(result)); 01092 ext_n = result.get_num(); 01093 ext_d = result.get_den(); 01094 included = is_included; 01095 return true; 01096 }
void Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible | ( | const char * | method, | |
const Box< ITV > & | x | |||
) | const [inline, private] |
Definition at line 3502 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::space_dimension().
Referenced by Parma_Polyhedra_Library::Box< ITV >::add_congruence(), Parma_Polyhedra_Library::Box< ITV >::add_congruences(), Parma_Polyhedra_Library::Box< ITV >::add_constraint(), Parma_Polyhedra_Library::Box< ITV >::add_constraints(), Parma_Polyhedra_Library::Box< ITV >::affine_image(), Parma_Polyhedra_Library::Box< ITV >::affine_preimage(), Parma_Polyhedra_Library::Box< ITV >::bounded_affine_image(), Parma_Polyhedra_Library::Box< ITV >::bounded_affine_preimage(), Parma_Polyhedra_Library::Box< ITV >::bounds(), Parma_Polyhedra_Library::Box< ITV >::CC76_narrowing_assign(), Parma_Polyhedra_Library::Box< ITV >::constrains(), Parma_Polyhedra_Library::Box< ITV >::contains(), Parma_Polyhedra_Library::Box< ITV >::difference_assign(), Parma_Polyhedra_Library::Box< ITV >::expand_space_dimension(), Parma_Polyhedra_Library::Box< ITV >::fold_space_dimensions(), Parma_Polyhedra_Library::Box< ITV >::generalized_affine_image(), Parma_Polyhedra_Library::Box< ITV >::generalized_affine_preimage(), Parma_Polyhedra_Library::Box< ITV >::get_interval(), Parma_Polyhedra_Library::Box< ITV >::intersection_assign(), Parma_Polyhedra_Library::Box< ITV >::is_disjoint_from(), Parma_Polyhedra_Library::Box< ITV >::max_min(), Parma_Polyhedra_Library::Box< ITV >::propagate_constraint(), Parma_Polyhedra_Library::Box< ITV >::propagate_constraints(), Parma_Polyhedra_Library::Box< ITV >::refine_with_congruence(), Parma_Polyhedra_Library::Box< ITV >::refine_with_congruences(), Parma_Polyhedra_Library::Box< ITV >::refine_with_constraint(), Parma_Polyhedra_Library::Box< ITV >::refine_with_constraints(), Parma_Polyhedra_Library::Box< ITV >::relation_with(), Parma_Polyhedra_Library::Box< ITV >::remove_higher_space_dimensions(), Parma_Polyhedra_Library::Box< ITV >::remove_space_dimensions(), Parma_Polyhedra_Library::Box< ITV >::set_interval(), Parma_Polyhedra_Library::Box< ITV >::time_elapse_assign(), Parma_Polyhedra_Library::Box< ITV >::unconstrain(), and Parma_Polyhedra_Library::Box< ITV >::upper_bound_assign().
03503 { 03504 std::ostringstream s; 03505 s << "PPL::Box::" << method << ":" << std::endl 03506 << "this->space_dimension() == " << this->space_dimension() 03507 << ", y->space_dimension() == " << y.space_dimension() << "."; 03508 throw std::invalid_argument(s.str()); 03509 }
void Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible | ( | const char * | method, | |
dimension_type | required_dim | |||
) | const [inline, private] |
Definition at line 3514 of file Box.templates.hh.
References Parma_Polyhedra_Library::Box< ITV >::space_dimension().
03515 { 03516 std::ostringstream s; 03517 s << "PPL::Box::" << method << ":" << std::endl 03518 << "this->space_dimension() == " << space_dimension() 03519 << ", required dimension == " << required_dim << "."; 03520 throw std::invalid_argument(s.str()); 03521 }
void Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible | ( | const char * | method, | |
const Constraint & | c | |||
) | const [inline, private] |
Definition at line 3525 of file Box.templates.hh.
References Parma_Polyhedra_Library::Constraint::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::space_dimension().
03526 { 03527 std::ostringstream s; 03528 s << "PPL::Box::" << method << ":" << std::endl 03529 << "this->space_dimension() == " << space_dimension() 03530 << ", c->space_dimension == " << c.space_dimension() << "."; 03531 throw std::invalid_argument(s.str()); 03532 }
void Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible | ( | const char * | method, | |
const Congruence & | cg | |||
) | const [inline, private] |
Definition at line 3536 of file Box.templates.hh.
References Parma_Polyhedra_Library::Congruence::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::space_dimension().
03537 { 03538 std::ostringstream s; 03539 s << "PPL::Box::" << method << ":" << std::endl 03540 << "this->space_dimension() == " << space_dimension() 03541 << ", cg->space_dimension == " << cg.space_dimension() << "."; 03542 throw std::invalid_argument(s.str()); 03543 }
void Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible | ( | const char * | method, | |
const Constraint_System & | cs | |||
) | const [inline, private] |
Definition at line 3547 of file Box.templates.hh.
References Parma_Polyhedra_Library::Constraint_System::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::space_dimension().
03548 { 03549 std::ostringstream s; 03550 s << "PPL::Box::" << method << ":" << std::endl 03551 << "this->space_dimension() == " << space_dimension() 03552 << ", cs->space_dimension == " << cs.space_dimension() << "."; 03553 throw std::invalid_argument(s.str()); 03554 }
void Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible | ( | const char * | method, | |
const Congruence_System & | cgs | |||
) | const [inline, private] |
Definition at line 3558 of file Box.templates.hh.
References Parma_Polyhedra_Library::Congruence_System::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::space_dimension().
03559 { 03560 std::ostringstream s; 03561 s << "PPL::Box::" << method << ":" << std::endl 03562 << "this->space_dimension() == " << space_dimension() 03563 << ", cgs->space_dimension == " << cgs.space_dimension() << "."; 03564 throw std::invalid_argument(s.str()); 03565 }
void Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible | ( | const char * | method, | |
const Generator & | g | |||
) | const [inline, private] |
Definition at line 3569 of file Box.templates.hh.
References Parma_Polyhedra_Library::Generator::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::space_dimension().
03570 { 03571 std::ostringstream s; 03572 s << "PPL::Box::" << method << ":" << std::endl 03573 << "this->space_dimension() == " << space_dimension() 03574 << ", g->space_dimension == " << g.space_dimension() << "."; 03575 throw std::invalid_argument(s.str()); 03576 }
void Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible | ( | const char * | method, | |
const char * | name_row, | |||
const Linear_Expression & | y | |||
) | const [inline, private] |
Definition at line 3600 of file Box.templates.hh.
References Parma_Polyhedra_Library::Linear_Expression::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::space_dimension().
03602 { 03603 std::ostringstream s; 03604 s << "PPL::Box::" << method << ":" << std::endl 03605 << "this->space_dimension() == " << space_dimension() 03606 << ", " << name_row << "->space_dimension() == " 03607 << e.space_dimension() << "."; 03608 throw std::invalid_argument(s.str()); 03609 }
void Parma_Polyhedra_Library::Box< ITV >::throw_space_dimension_overflow | ( | const char * | method, | |
const char * | reason | |||
) | [inline, static, private] |
Definition at line 3622 of file Box.templates.hh.
Referenced by Parma_Polyhedra_Library::Box< ITV >::Box().
03623 { 03624 std::ostringstream s; 03625 s << "PPL::Box::" << method << ":" << std::endl 03626 << reason; 03627 throw std::length_error(s.str()); 03628 }
void Parma_Polyhedra_Library::Box< ITV >::throw_constraint_incompatible | ( | const char * | method | ) | [inline, static, private] |
Definition at line 3580 of file Box.templates.hh.
03580 { 03581 std::ostringstream s; 03582 s << "PPL::Box::" << method << ":" << std::endl 03583 << "the constraint is incompatible."; 03584 throw std::invalid_argument(s.str()); 03585 }
void Parma_Polyhedra_Library::Box< ITV >::throw_expression_too_complex | ( | const char * | method, | |
const Linear_Expression & | e | |||
) | [inline, static, private] |
Definition at line 3589 of file Box.templates.hh.
03590 { 03591 using namespace IO_Operators; 03592 std::ostringstream s; 03593 s << "PPL::Box::" << method << ":" << std::endl 03594 << e << " is too complex."; 03595 throw std::invalid_argument(s.str()); 03596 }
void Parma_Polyhedra_Library::Box< ITV >::throw_generic | ( | const char * | method, | |
const char * | reason | |||
) | [inline, static, private] |
Definition at line 3613 of file Box.templates.hh.
Referenced by Parma_Polyhedra_Library::Box< ITV >::add_congruence_no_check(), Parma_Polyhedra_Library::Box< ITV >::add_constraint_no_check(), Parma_Polyhedra_Library::Box< ITV >::affine_image(), Parma_Polyhedra_Library::Box< ITV >::affine_preimage(), Parma_Polyhedra_Library::Box< ITV >::bounded_affine_image(), Parma_Polyhedra_Library::Box< ITV >::bounded_affine_preimage(), Parma_Polyhedra_Library::Box< ITV >::expand_space_dimension(), Parma_Polyhedra_Library::Box< ITV >::fold_space_dimensions(), Parma_Polyhedra_Library::Box< ITV >::generalized_affine_image(), and Parma_Polyhedra_Library::Box< ITV >::generalized_affine_preimage().
03613 { 03614 std::ostringstream s; 03615 s << "PPL::Box::" << method << ":" << std::endl 03616 << reason; 03617 throw std::invalid_argument(s.str()); 03618 }
friend class Parma_Polyhedra_Library::Box [friend] |
Definition at line 1512 of file Box.defs.hh.
Returns true
if and only if x
and y
are the same box.
Note that x
and y
may be dimension-incompatible boxes: in this case, the value false
is returned.
Definition at line 562 of file Box.templates.hh.
00562 { 00563 const dimension_type x_space_dim = x.space_dimension(); 00564 if (x_space_dim != y.space_dimension()) 00565 return false; 00566 00567 if (x.is_empty()) 00568 return y.is_empty(); 00569 00570 if (y.is_empty()) 00571 return x.is_empty(); 00572 00573 for (dimension_type k = x_space_dim; k-- > 0; ) 00574 if (x.seq[k] != y.seq[k]) 00575 return false; 00576 return true; 00577 }
std::ostream & operator<< | ( | std::ostream & | s, | |
const Box< ITV > & | box | |||
) | [friend] |
Output operator.
Definition at line 3441 of file Box.templates.hh.
03441 { 03442 if (box.is_empty()) 03443 s << "false"; 03444 else if (box.is_universe()) 03445 s << "true"; 03446 else 03447 for (dimension_type k = 0, 03448 space_dim = box.space_dimension(); k < space_dim; ) { 03449 s << Variable(k) << " in " << box[k]; 03450 ++k; 03451 if (k < space_dim) 03452 s << ", "; 03453 else 03454 break; 03455 } 03456 return s; 03457 }
bool l_m_distance_assign | ( | Checked_Number< To, Extended_Number_Policy > & | r, | |
const Box< I > & | x, | |||
const Box< I > & | y, | |||
const Rounding_Dir | dir, | |||
Temp & | tmp0, | |||
Temp & | tmp1, | |||
Temp & | tmp2 | |||
) | [friend] |
Returns true
if and only if x
and y
aren't the same box.
Note that x
and y
may be dimension-incompatible boxes: in this case, the value true
is returned.
Definition at line 260 of file Box.inlines.hh.
bool rectilinear_distance_assign | ( | Checked_Number< To, Extended_Number_Policy > & | r, | |
const Box< ITV > & | x, | |||
const Box< ITV > & | y, | |||
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 549 of file Box.inlines.hh.
00552 { 00553 typedef Checked_Number<Temp, Extended_Number_Policy> Checked_Temp; 00554 DIRTY_TEMP(Checked_Temp, tmp0); 00555 DIRTY_TEMP(Checked_Temp, tmp1); 00556 DIRTY_TEMP(Checked_Temp, tmp2); 00557 return rectilinear_distance_assign(r, x, y, dir, tmp0, tmp1, tmp2); 00558 }
bool rectilinear_distance_assign | ( | Checked_Number< To, Extended_Number_Policy > & | r, | |
const Box< ITV > & | x, | |||
const Box< ITV > & | y, | |||
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 535 of file Box.inlines.hh.
00541 { 00542 return l_m_distance_assign<Rectilinear_Distance_Specialization<Temp> > 00543 (r, x, y, dir, tmp0, tmp1, tmp2); 00544 }
bool euclidean_distance_assign | ( | Checked_Number< To, Extended_Number_Policy > & | r, | |
const Box< ITV > & | x, | |||
const Box< ITV > & | y, | |||
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 587 of file Box.inlines.hh.
00590 { 00591 typedef Checked_Number<Temp, Extended_Number_Policy> Checked_Temp; 00592 DIRTY_TEMP(Checked_Temp, tmp0); 00593 DIRTY_TEMP(Checked_Temp, tmp1); 00594 DIRTY_TEMP(Checked_Temp, tmp2); 00595 return euclidean_distance_assign(r, x, y, dir, tmp0, tmp1, tmp2); 00596 }
bool euclidean_distance_assign | ( | Checked_Number< To, Extended_Number_Policy > & | r, | |
const Box< ITV > & | x, | |||
const Box< ITV > & | y, | |||
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 573 of file Box.inlines.hh.
00579 { 00580 return l_m_distance_assign<Euclidean_Distance_Specialization<Temp> > 00581 (r, x, y, dir, tmp0, tmp1, tmp2); 00582 }
bool l_infinity_distance_assign | ( | Checked_Number< To, Extended_Number_Policy > & | r, | |
const Box< ITV > & | x, | |||
const Box< ITV > & | y, | |||
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 625 of file Box.inlines.hh.
00628 { 00629 typedef Checked_Number<Temp, Extended_Number_Policy> Checked_Temp; 00630 DIRTY_TEMP(Checked_Temp, tmp0); 00631 DIRTY_TEMP(Checked_Temp, tmp1); 00632 DIRTY_TEMP(Checked_Temp, tmp2); 00633 return l_infinity_distance_assign(r, x, y, dir, tmp0, tmp1, tmp2); 00634 }
bool l_infinity_distance_assign | ( | Checked_Number< To, Extended_Number_Policy > & | r, | |
const Box< ITV > & | x, | |||
const Box< ITV > & | y, | |||
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 611 of file Box.inlines.hh.
00617 { 00618 return l_m_distance_assign<L_Infinity_Distance_Specialization<Temp> > 00619 (r, x, y, dir, tmp0, tmp1, tmp2); 00620 }
bool l_m_distance_assign | ( | Checked_Number< To, Extended_Number_Policy > & | r, | |
const Box< ITV > & | x, | |||
const Box< ITV > & | y, | |||
Rounding_Dir | dir, | |||
Temp & | tmp0, | |||
Temp & | tmp1, | |||
Temp & | tmp2 | |||
) | [related] |
Helper function for computing distances.
Definition at line 3636 of file Box.templates.hh.
References Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::combine(), Parma_Polyhedra_Library::finalize(), Parma_Polyhedra_Library::Box< ITV >::is_empty(), Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::maybe_assign(), PLUS_INFINITY, Parma_Polyhedra_Library::Box< ITV >::seq, and Parma_Polyhedra_Library::Box< ITV >::space_dimension().
03639 { 03640 const dimension_type x_space_dim = x.space_dimension(); 03641 // Dimension-compatibility check. 03642 if (x_space_dim != y.space_dimension()) 03643 return false; 03644 03645 // Zero-dim boxes are equal if and only if they are both empty or universe. 03646 if (x_space_dim == 0) { 03647 if (x.marked_empty() == y.marked_empty()) 03648 assign_r(r, 0, ROUND_NOT_NEEDED); 03649 else 03650 assign_r(r, PLUS_INFINITY, ROUND_NOT_NEEDED); 03651 return true; 03652 } 03653 03654 // The distance computation requires a check for emptiness. 03655 (void) x.is_empty(); 03656 (void) y.is_empty(); 03657 // If one of two boxes is empty, then they are equal if and only if 03658 // the other box is empty too. 03659 if (x.marked_empty() || y.marked_empty()) { 03660 if (x.marked_empty() == y.marked_empty()) { 03661 assign_r(r, 0, ROUND_NOT_NEEDED); 03662 return true; 03663 } 03664 else 03665 goto pinf; 03666 } 03667 03668 assign_r(tmp0, 0, ROUND_NOT_NEEDED); 03669 for (dimension_type i = x_space_dim; i-- > 0; ) { 03670 const ITV& x_i = x.seq[i]; 03671 const ITV& y_i = y.seq[i]; 03672 // Dealing with the lower bounds. 03673 if (x_i.lower_is_unbounded()) { 03674 if (!y_i.lower_is_unbounded()) 03675 goto pinf; 03676 } 03677 else if (y_i.lower_is_unbounded()) 03678 goto pinf; 03679 else { 03680 const Temp* tmp1p; 03681 const Temp* tmp2p; 03682 if (x_i.lower() > y_i.lower()) { 03683 maybe_assign(tmp1p, tmp1, x_i.lower(), dir); 03684 maybe_assign(tmp2p, tmp2, y_i.lower(), inverse(dir)); 03685 } 03686 else { 03687 maybe_assign(tmp1p, tmp1, y_i.lower(), dir); 03688 maybe_assign(tmp2p, tmp2, x_i.lower(), inverse(dir)); 03689 } 03690 sub_assign_r(tmp1, *tmp1p, *tmp2p, dir); 03691 assert(sgn(tmp1) >= 0); 03692 Specialization::combine(tmp0, tmp1, dir); 03693 } 03694 // Dealing with the lower bounds. 03695 if (x_i.upper_is_unbounded()) 03696 if (y_i.upper_is_unbounded()) 03697 continue; 03698 else 03699 goto pinf; 03700 else if (y_i.upper_is_unbounded()) 03701 goto pinf; 03702 else { 03703 const Temp* tmp1p; 03704 const Temp* tmp2p; 03705 if (x_i.upper() > y_i.upper()) { 03706 maybe_assign(tmp1p, tmp1, x_i.upper(), dir); 03707 maybe_assign(tmp2p, tmp2, y_i.upper(), inverse(dir)); 03708 } 03709 else { 03710 maybe_assign(tmp1p, tmp1, y_i.upper(), dir); 03711 maybe_assign(tmp2p, tmp2, x_i.upper(), inverse(dir)); 03712 } 03713 sub_assign_r(tmp1, *tmp1p, *tmp2p, dir); 03714 assert(sgn(tmp1) >= 0); 03715 Specialization::combine(tmp0, tmp1, dir); 03716 } 03717 } 03718 Specialization::finalize(tmp0, dir); 03719 assign_r(r, tmp0, dir); 03720 return true; 03721 03722 pinf: 03723 assign_r(r, PLUS_INFINITY, ROUND_NOT_NEEDED); 03724 return true; 03725 }
bool extract_interval_constraint | ( | const Constraint & | c, | |
dimension_type | c_space_dim, | |||
dimension_type & | c_num_vars, | |||
dimension_type & | c_only_var | |||
) | [related] |
Decodes the constraint c
as an interval constraint.
true
if the constraint c
is an interval constraint; false
otherwise.c | The constraint to be decoded. | |
c_space_dim | The space dimension of the constraint c (it is assumed to match the actual space dimension of c ). | |
c_num_vars | If true is returned, then it will be set to the number of variables having a non-zero coefficient. The only legal values will therefore be 0 and 1. | |
c_only_var | If true is returned and if c_num_vars is not set to 0, then it will be set to the index of the only variable having a non-zero coefficient in c . |
Definition at line 32 of file Box.cc.
References Parma_Polyhedra_Library::Constraint::coefficient(), and Parma_Polyhedra_Library::Constraint::space_dimension().
Referenced by Parma_Polyhedra_Library::Box< ITV >::add_constraint_no_check(), Parma_Polyhedra_Library::Box< ITV >::refine_no_check(), and Parma_Polyhedra_Library::Box< ITV >::relation_with().
00035 { 00036 // Check for preconditions. 00037 assert(c.space_dimension() == c_space_dim); 00038 assert(c_num_vars == 0 && c_only_var == 0); 00039 // Collect the non-zero components of `c'. 00040 for (dimension_type i = c_space_dim; i-- > 0; ) 00041 if (c.coefficient(Variable(i)) != 0) { 00042 if (c_num_vars == 0) { 00043 c_only_var = i; 00044 ++c_num_vars; 00045 } 00046 else 00047 // Constraint `c' is not an interval constraint. 00048 return false; 00049 } 00050 return true; 00051 }
Sequence Parma_Polyhedra_Library::Box< ITV >::seq [private] |
A sequence of intervals, one for each dimension of the vector space.
Definition at line 1537 of file Box.defs.hh.
Referenced by Parma_Polyhedra_Library::Box< ITV >::add_interval_constraint_no_check(), Parma_Polyhedra_Library::Box< ITV >::add_space_dimensions_and_embed(), Parma_Polyhedra_Library::Box< ITV >::add_space_dimensions_and_project(), Parma_Polyhedra_Library::Box< ITV >::affine_dimension(), Parma_Polyhedra_Library::Box< ITV >::affine_image(), Parma_Polyhedra_Library::Box< ITV >::affine_preimage(), Parma_Polyhedra_Library::Box< ITV >::ascii_dump(), Parma_Polyhedra_Library::Box< ITV >::ascii_load(), Parma_Polyhedra_Library::Box< ITV >::bounded_affine_image(), Parma_Polyhedra_Library::Box< ITV >::bounded_affine_preimage(), Parma_Polyhedra_Library::Box< ITV >::bounds(), Parma_Polyhedra_Library::Box< ITV >::Box(), Parma_Polyhedra_Library::Box< ITV >::CC76_narrowing_assign(), Parma_Polyhedra_Library::Box< ITV >::CC76_widening_assign(), Parma_Polyhedra_Library::Box< ITV >::check_empty(), Parma_Polyhedra_Library::Box< ITV >::concatenate_assign(), Parma_Polyhedra_Library::Box< ITV >::congruences(), Parma_Polyhedra_Library::Box< ITV >::constrains(), Parma_Polyhedra_Library::Box< ITV >::contains(), Parma_Polyhedra_Library::Box< ITV >::contains_integer_point(), Parma_Polyhedra_Library::Box< ITV >::difference_assign(), Parma_Polyhedra_Library::Box< ITV >::expand_space_dimension(), Parma_Polyhedra_Library::Box< ITV >::external_memory_in_bytes(), Parma_Polyhedra_Library::Box< ITV >::fold_space_dimensions(), Parma_Polyhedra_Library::Box< ITV >::generalized_affine_image(), Parma_Polyhedra_Library::Box< ITV >::generalized_affine_preimage(), Parma_Polyhedra_Library::Box< ITV >::get_interval(), Parma_Polyhedra_Library::Box< ITV >::get_lower_bound(), Parma_Polyhedra_Library::Box< ITV >::get_upper_bound(), Parma_Polyhedra_Library::Box< ITV >::intersection_assign(), Parma_Polyhedra_Library::Box< ITV >::is_bounded(), Parma_Polyhedra_Library::Box< ITV >::is_discrete(), Parma_Polyhedra_Library::Box< ITV >::is_disjoint_from(), Parma_Polyhedra_Library::Box< ITV >::is_topologically_closed(), Parma_Polyhedra_Library::Box< ITV >::is_universe(), Parma_Polyhedra_Library::Box< ITV >::l_m_distance_assign(), Parma_Polyhedra_Library::Box< ITV >::map_space_dimensions(), Parma_Polyhedra_Library::Box< ITV >::max_min(), Parma_Polyhedra_Library::Box< ITV >::minimized_constraints(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::operator=(), Parma_Polyhedra_Library::operator==(), Parma_Polyhedra_Library::Box< ITV >::operator[](), Parma_Polyhedra_Library::Box< ITV >::propagate_constraint_no_check(), Parma_Polyhedra_Library::Box< ITV >::propagate_constraints_no_check(), Parma_Polyhedra_Library::Box< ITV >::relation_with(), Parma_Polyhedra_Library::Box< ITV >::remove_higher_space_dimensions(), Parma_Polyhedra_Library::Box< ITV >::remove_space_dimensions(), Parma_Polyhedra_Library::Box< ITV >::set_interval(), Parma_Polyhedra_Library::Box< ITV >::space_dimension(), Parma_Polyhedra_Library::Box< ITV >::swap(), Parma_Polyhedra_Library::Box< ITV >::time_elapse_assign(), Parma_Polyhedra_Library::Box< ITV >::topological_closure_assign(), Parma_Polyhedra_Library::Box< ITV >::unconstrain(), and Parma_Polyhedra_Library::Box< ITV >::upper_bound_assign().
Status Parma_Polyhedra_Library::Box< ITV >::status [private] |
The status flags to keep track of the internal state.
Definition at line 1657 of file Box.defs.hh.
Referenced by Parma_Polyhedra_Library::Box< ITV >::ascii_dump(), Parma_Polyhedra_Library::Box< ITV >::ascii_load(), Parma_Polyhedra_Library::Box< ITV >::concatenate_assign(), Parma_Polyhedra_Library::Box< ITV >::marked_empty(), Parma_Polyhedra_Library::Box< ITV >::OK(), Parma_Polyhedra_Library::Box< ITV >::operator=(), Parma_Polyhedra_Library::Box< ITV >::reset_empty_up_to_date(), Parma_Polyhedra_Library::Box< ITV >::set_empty(), Parma_Polyhedra_Library::Box< ITV >::set_empty_up_to_date(), Parma_Polyhedra_Library::Box< ITV >::set_nonempty(), and Parma_Polyhedra_Library::Box< ITV >::swap().