PPL
1.0
|
An octagonal shape. More...
#include <ppl.hh>
Public Types | |
typedef T | coefficient_type_base |
The numeric base type upon which OSs are built. | |
typedef N | coefficient_type |
The (extended) numeric type of the inhomogeneous term of the inequalities defining an OS. |
Public Member Functions | |
void | ascii_dump () const |
Writes to std::cerr an ASCII representation of *this . | |
void | ascii_dump (std::ostream &s) const |
Writes to s an ASCII representation of *this . | |
void | print () const |
Prints *this to std::cerr using operator<< . | |
bool | ascii_load (std::istream &s) |
Loads from s an ASCII representation (as produced by ascii_dump(std::ostream&) const) and sets *this accordingly. Returns true if successful, false otherwise. | |
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 . | |
int32_t | hash_code () const |
Returns a 32-bit hash code for *this . | |
Constructors, Assignment, Swap and Destructor | |
Octagonal_Shape (dimension_type num_dimensions=0, Degenerate_Element kind=UNIVERSE) | |
Builds an universe or empty OS of the specified space dimension. | |
Octagonal_Shape (const Octagonal_Shape &y, Complexity_Class complexity=ANY_COMPLEXITY) | |
Ordinary copy constructor. | |
template<typename U > | |
Octagonal_Shape (const Octagonal_Shape< U > &y, Complexity_Class complexity=ANY_COMPLEXITY) | |
Builds a conservative, upward approximation of y . | |
Octagonal_Shape (const Constraint_System &cs) | |
Builds an OS from the system of constraints cs . | |
Octagonal_Shape (const Congruence_System &cgs) | |
Builds an OS from a system of congruences. | |
Octagonal_Shape (const Generator_System &gs) | |
Builds an OS from the system of generators gs . | |
Octagonal_Shape (const Polyhedron &ph, Complexity_Class complexity=ANY_COMPLEXITY) | |
Builds an OS from the polyhedron ph . | |
template<typename Interval > | |
Octagonal_Shape (const Box< Interval > &box, Complexity_Class complexity=ANY_COMPLEXITY) | |
Builds an OS out of a box. | |
Octagonal_Shape (const Grid &grid, Complexity_Class complexity=ANY_COMPLEXITY) | |
Builds an OS that approximates a grid. | |
template<typename U > | |
Octagonal_Shape (const BD_Shape< U > &bd, Complexity_Class complexity=ANY_COMPLEXITY) | |
Builds an OS from a BD shape. | |
Octagonal_Shape & | operator= (const Octagonal_Shape &y) |
The assignment operator. (*this and y can be dimension-incompatible.) | |
void | m_swap (Octagonal_Shape &y) |
Swaps *this with octagon y . (*this and y can be dimension-incompatible.) | |
~Octagonal_Shape () | |
Destructor. | |
Member Functions that Do Not Modify the Octagonal_Shape | |
dimension_type | space_dimension () const |
Returns the dimension of the vector space enclosing *this . | |
dimension_type | affine_dimension () const |
Returns ![]() *this is empty; otherwise, returns the affine dimension of *this . | |
Constraint_System | constraints () const |
Returns the 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 (equality) congruences satisfied by *this . | |
Congruence_System | minimized_congruences () const |
Returns a minimal system of (equality) congruences satisfied by *this with the same affine dimension as *this . | |
bool | contains (const Octagonal_Shape &y) const |
Returns true if and only if *this contains y . | |
bool | strictly_contains (const Octagonal_Shape &y) const |
Returns true if and only if *this strictly contains y . | |
bool | is_disjoint_from (const Octagonal_Shape &y) const |
Returns true if and only if *this and y are disjoint. | |
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 | is_empty () const |
Returns true if and only if *this is an empty OS. | |
bool | is_universe () const |
Returns true if and only if *this is a universe OS. | |
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 OS. | |
bool | is_topologically_closed () const |
Returns true if and only if *this is a topologically closed subset of the vector space. | |
bool | contains_integer_point () const |
Returns true if and only if *this contains (at least) an integer point. | |
bool | constrains (Variable var) const |
Returns true if and only if var is constrained in *this . | |
bool | bounds_from_above (const Linear_Expression &expr) const |
Returns true if and only if expr is bounded from above in *this . | |
bool | bounds_from_below (const Linear_Expression &expr) const |
Returns true if and only if expr is bounded from below in *this . | |
bool | maximize (const Linear_Expression &expr, Coefficient &sup_n, Coefficient &sup_d, bool &maximum) const |
Returns true if and only if *this is not empty and expr is bounded from above in *this , in which case the supremum value is computed. | |
bool | maximize (const Linear_Expression &expr, Coefficient &sup_n, Coefficient &sup_d, bool &maximum, Generator &g) const |
Returns true if and only if *this is not empty and expr is bounded from above in *this , in which case the supremum value and a point where expr reaches it are computed. | |
bool | minimize (const Linear_Expression &expr, Coefficient &inf_n, Coefficient &inf_d, bool &minimum) const |
Returns true if and only if *this is not empty and expr is bounded from below in *this , in which case the infimum value is computed. | |
bool | minimize (const Linear_Expression &expr, Coefficient &inf_n, Coefficient &inf_d, bool &minimum, Generator &g) const |
Returns true if and only if *this is not empty and expr is bounded from below in *this , in which case the infimum value and a point where expr reaches it are computed. | |
bool | frequency (const Linear_Expression &expr, Coefficient &freq_n, Coefficient &freq_d, Coefficient &val_n, Coefficient &val_d) const |
Returns true if and only if there exist a unique value val such that *this saturates the equality expr = val . | |
bool | OK () const |
Checks if all the invariants are satisfied. | |
Space-Dimension Preserving Member Functions that May Modify the Octagonal_Shape | |
void | add_constraint (const Constraint &c) |
Adds a copy of constraint c to the system of constraints defining *this . | |
void | add_constraints (const Constraint_System &cs) |
Adds the constraints in cs to the system of constraints defining *this . | |
void | add_recycled_constraints (Constraint_System &cs) |
Adds the constraints in cs to the system of constraints of *this . | |
void | add_congruence (const Congruence &cg) |
Adds to *this a constraint equivalent to the congruence cg . | |
void | add_congruences (const Congruence_System &cgs) |
Adds to *this constraints equivalent to the congruences in cgs . | |
void | add_recycled_congruences (Congruence_System &cgs) |
Adds to *this constraints equivalent to the congruences in cgs . | |
void | refine_with_constraint (const Constraint &c) |
Uses a copy of constraint c to refine the system of octagonal constraints defining *this . | |
void | refine_with_congruence (const Congruence &cg) |
Uses a copy of congruence cg to refine the system of octagonal constraints of *this . | |
void | refine_with_constraints (const Constraint_System &cs) |
Uses a copy of the constraints in cs to refine the system of octagonal constraints defining *this . | |
void | refine_with_congruences (const Congruence_System &cgs) |
Uses a copy of the congruences in cgs to refine the system of octagonal constraints defining *this . | |
template<typename Interval_Info > | |
void | refine_with_linear_form_inequality (const Linear_Form< Interval< T, Interval_Info > > &left, const Linear_Form< Interval< T, Interval_Info > > &right) |
Refines the system of octagonal constraints defining *this using the constraint expressed by left ![]() right . | |
template<typename Interval_Info > | |
void | generalized_refine_with_linear_form_inequality (const Linear_Form< Interval< T, Interval_Info > > &left, const Linear_Form< Interval< T, Interval_Info > > &right, Relation_Symbol relsym) |
Refines the system of octagonal constraints defining *this using the constraint expressed by left ![]() right , where ![]() relsym . | |
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 &vars) |
Computes the cylindrification of *this with respect to the set of space dimensions vars , assigning the result to *this . | |
void | intersection_assign (const Octagonal_Shape &y) |
Assigns to *this the intersection of *this and y . | |
void | upper_bound_assign (const Octagonal_Shape &y) |
Assigns to *this the smallest OS that contains the convex union of *this and y . | |
bool | upper_bound_assign_if_exact (const Octagonal_Shape &y) |
If the upper bound of *this and y is exact, it is assigned to *this and true is returned, otherwise false is returned. | |
bool | integer_upper_bound_assign_if_exact (const Octagonal_Shape &y) |
If the integer 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 Octagonal_Shape &y) |
Assigns to *this the smallest octagon containing the set difference of *this and y . | |
bool | simplify_using_context_assign (const Octagonal_Shape &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 into the affine expression specified by expr and denominator . | |
template<typename Interval_Info > | |
void | affine_form_image (Variable var, const Linear_Form< Interval< T, Interval_Info > > &lf) |
Assigns to *this the affine form image of *this under the function mapping variable var into the affine expression(s) specified by lf . | |
void | affine_preimage (Variable var, const Linear_Expression &expr, Coefficient_traits::const_reference denominator=Coefficient_one()) |
Assigns to *this the affine preimage of *this under the function mapping variable var into the affine expression specified by expr and denominator . | |
void | generalized_affine_image (Variable var, Relation_Symbol relsym, const Linear_Expression &expr, Coefficient_traits::const_reference denominator=Coefficient_one()) |
Assigns to *this the image of *this with respect to the generalized affine transfer function ![]() ![]() 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 transfer function ![]() ![]() 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 | generalized_affine_preimage (Variable var, Relation_Symbol relsym, const Linear_Expression &expr, Coefficient_traits::const_reference denominator=Coefficient_one()) |
Assigns to *this the preimage of *this with respect to the affine relation ![]() ![]() relsym . | |
void | 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_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 Octagonal_Shape &y) |
Assigns to *this the result of computing the time-elapse between *this and y . | |
void | wrap_assign (const Variables_Set &vars, Bounded_Integer_Type_Width w, Bounded_Integer_Type_Representation r, Bounded_Integer_Type_Overflow o, const Constraint_System *cs_p=0, unsigned complexity_threshold=16, bool wrap_individually=true) |
Wraps the specified dimensions of the vector space. | |
void | drop_some_non_integer_points (Complexity_Class complexity=ANY_COMPLEXITY) |
Possibly tightens *this by dropping some points with non-integer coordinates. | |
void | drop_some_non_integer_points (const Variables_Set &vars, Complexity_Class complexity=ANY_COMPLEXITY) |
Possibly tightens *this by dropping some points with non-integer coordinates for the space dimensions corresponding to vars . | |
void | topological_closure_assign () |
Assigns to *this its topological closure. | |
void | CC76_extrapolation_assign (const Octagonal_Shape &y, unsigned *tp=0) |
Assigns to *this the result of computing the CC76-extrapolation between *this and y . | |
template<typename Iterator > | |
void | CC76_extrapolation_assign (const Octagonal_Shape &y, Iterator first, Iterator last, unsigned *tp=0) |
Assigns to *this the result of computing the CC76-extrapolation between *this and y . | |
void | BHMZ05_widening_assign (const Octagonal_Shape &y, unsigned *tp=0) |
Assigns to *this the result of computing the BHMZ05-widening between *this and y . | |
void | widening_assign (const Octagonal_Shape &y, unsigned *tp=0) |
Same as BHMZ05_widening_assign(y, tp). | |
void | limited_BHMZ05_extrapolation_assign (const Octagonal_Shape &y, const Constraint_System &cs, unsigned *tp=0) |
Improves the result of the BHMZ05-widening computation by also enforcing those constraints in cs that are satisfied by all the points of *this . | |
void | CC76_narrowing_assign (const Octagonal_Shape &y) |
Restores from y the constraints of *this , lost by CC76-extrapolation applications. | |
void | limited_CC76_extrapolation_assign (const Octagonal_Shape &y, const Constraint_System &cs, unsigned *tp=0) |
Improves the result of the CC76-extrapolation computation by also enforcing those constraints in cs that are satisfied by all the points of *this . | |
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 OS into the new space. | |
void | add_space_dimensions_and_project (dimension_type m) |
Adds m new dimensions to the OS and does not embed it in the new space. | |
void | concatenate_assign (const Octagonal_Shape &y) |
Assigns to *this the concatenation of *this and y , taken in this order. | |
void | remove_space_dimensions (const Variables_Set &vars) |
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 &vars, Variable dest) |
Folds the space dimensions in vars into dest . | |
template<typename U > | |
void | export_interval_constraints (U &dest) const |
Applies to dest the interval constraints embedded in *this . | |
template<typename Interval_Info > | |
void | refine_fp_interval_abstract_store (Box< Interval< T, Interval_Info > > &store) const |
Refines store with the constraints defining *this . |
Static Public Member Functions | |
static dimension_type | max_space_dimension () |
Returns the maximum space dimension that an OS can handle. | |
static bool | can_recycle_constraint_systems () |
Returns false indicating that this domain cannot recycle constraints. | |
static bool | can_recycle_congruence_systems () |
Returns false indicating that this domain cannot recycle congruences. |
Related Functions | |
(Note that these are not member functions.) | |
template<typename T > | |
std::ostream & | operator<< (std::ostream &s, const Octagonal_Shape< T > &oct) |
Output operator. | |
template<typename T > | |
void | swap (Octagonal_Shape< T > &x, Octagonal_Shape< T > &y) |
Swaps x with y . | |
template<typename T > | |
bool | operator== (const Octagonal_Shape< T > &x, const Octagonal_Shape< T > &y) |
Returns true if and only if x and y are the same octagon. | |
template<typename T > | |
bool | operator!= (const Octagonal_Shape< T > &x, const Octagonal_Shape< T > &y) |
Returns true if and only if x and y are different shapes. | |
template<typename To , typename T > | |
bool | rectilinear_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Octagonal_Shape< T > &x, const Octagonal_Shape< T > &y, Rounding_Dir dir) |
Computes the rectilinear (or Manhattan) distance between x and y . | |
template<typename Temp , typename To , typename T > | |
bool | rectilinear_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Octagonal_Shape< T > &x, const Octagonal_Shape< T > &y, Rounding_Dir dir) |
Computes the rectilinear (or Manhattan) distance between x and y . | |
template<typename Temp , typename To , typename T > | |
bool | rectilinear_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Octagonal_Shape< T > &x, const Octagonal_Shape< T > &y, Rounding_Dir dir, Temp &tmp0, Temp &tmp1, Temp &tmp2) |
Computes the rectilinear (or Manhattan) distance between x and y . | |
template<typename To , typename T > | |
bool | euclidean_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Octagonal_Shape< T > &x, const Octagonal_Shape< T > &y, Rounding_Dir dir) |
Computes the euclidean distance between x and y . | |
template<typename Temp , typename To , typename T > | |
bool | euclidean_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Octagonal_Shape< T > &x, const Octagonal_Shape< T > &y, Rounding_Dir dir) |
Computes the euclidean distance between x and y . | |
template<typename Temp , typename To , typename T > | |
bool | euclidean_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Octagonal_Shape< T > &x, const Octagonal_Shape< T > &y, Rounding_Dir dir, Temp &tmp0, Temp &tmp1, Temp &tmp2) |
Computes the euclidean distance between x and y . | |
template<typename To , typename T > | |
bool | l_infinity_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Octagonal_Shape< T > &x, const Octagonal_Shape< T > &y, Rounding_Dir dir) |
Computes the ![]() x and y . | |
template<typename Temp , typename To , typename T > | |
bool | l_infinity_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Octagonal_Shape< T > &x, const Octagonal_Shape< T > &y, Rounding_Dir dir) |
Computes the ![]() x and y . | |
template<typename Temp , typename To , typename T > | |
bool | l_infinity_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Octagonal_Shape< T > &x, const Octagonal_Shape< T > &y, Rounding_Dir dir, Temp &tmp0, Temp &tmp1, Temp &tmp2) |
Computes the ![]() x and y . | |
template<typename T > | |
bool | operator== (const Octagonal_Shape< T > &x, const Octagonal_Shape< T > &y) |
template<typename T > | |
bool | operator!= (const Octagonal_Shape< T > &x, const Octagonal_Shape< T > &y) |
template<typename Temp , typename To , typename T > | |
bool | rectilinear_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Octagonal_Shape< T > &x, const Octagonal_Shape< T > &y, const Rounding_Dir dir, Temp &tmp0, Temp &tmp1, Temp &tmp2) |
template<typename Temp , typename To , typename T > | |
bool | rectilinear_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Octagonal_Shape< T > &x, const Octagonal_Shape< T > &y, const Rounding_Dir dir) |
template<typename To , typename T > | |
bool | rectilinear_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Octagonal_Shape< T > &x, const Octagonal_Shape< T > &y, const Rounding_Dir dir) |
template<typename Temp , typename To , typename T > | |
bool | euclidean_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Octagonal_Shape< T > &x, const Octagonal_Shape< T > &y, const Rounding_Dir dir, Temp &tmp0, Temp &tmp1, Temp &tmp2) |
template<typename Temp , typename To , typename T > | |
bool | euclidean_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Octagonal_Shape< T > &x, const Octagonal_Shape< T > &y, const Rounding_Dir dir) |
template<typename To , typename T > | |
bool | euclidean_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Octagonal_Shape< T > &x, const Octagonal_Shape< T > &y, const Rounding_Dir dir) |
template<typename Temp , typename To , typename T > | |
bool | l_infinity_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Octagonal_Shape< T > &x, const Octagonal_Shape< T > &y, const Rounding_Dir dir, Temp &tmp0, Temp &tmp1, Temp &tmp2) |
template<typename Temp , typename To , typename T > | |
bool | l_infinity_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Octagonal_Shape< T > &x, const Octagonal_Shape< T > &y, const Rounding_Dir dir) |
template<typename To , typename T > | |
bool | l_infinity_distance_assign (Checked_Number< To, Extended_Number_Policy > &r, const Octagonal_Shape< T > &x, const Octagonal_Shape< T > &y, const Rounding_Dir dir) |
template<typename T > | |
void | swap (Octagonal_Shape< T > &x, Octagonal_Shape< T > &y) |
template<typename T > | |
std::ostream & | operator<< (std::ostream &s, const Octagonal_Shape< T > &oct) |
An octagonal shape.
The class template Octagonal_Shape<T> allows for the efficient representation of a restricted kind of topologically closed convex polyhedra called octagonal shapes (OSs, for short). The name comes from the fact that, in a vector space of dimension 2, bounded OSs are polygons with at most eight sides. The closed affine half-spaces that characterize the OS can be expressed by constraints of the form
where and
is a rational number, which are called octagonal constraints.
Based on the class template type parameter T
, a family of extended numbers is built and used to approximate the inhomogeneous term of octagonal constraints. These extended numbers provide a representation for the value , as well as rounding-aware implementations for several arithmetic functions. The value of the type parameter
T
may be one of the following:
int32_t
or int64_t
);float
or double
);mpz_class
or mpq_class
).The user interface for OSs is meant to be as similar as possible to the one developed for the polyhedron class C_Polyhedron.
The OS domain optimally supports:
Depending on the method, using a constraint or congruence that is not optimally supported by the domain will either raise an exception or result in a (possibly non-optimal) upward approximation.
A constraint is octagonal if it has the form
where and
,
,
are integer coefficients such that
, or
, or
. The user is warned that the above octagonal Constraint object will be mapped into a correct and optimal approximation that, depending on the expressive power of the chosen template argument
T
, may loose some precision. Also note that strict constraints are not octagonal.
For instance, a Constraint object encoding will be approximated by:
T
is a (bounded or unbounded) integer type;T
is the unbounded rational type mpq_class
;T
is a floating point type (having no exact representation for On the other hand, depending from the context, a Constraint object encoding will be either upward approximated (e.g., by safely ignoring it) or it will cause an exception.
In the following examples it is assumed that the type argument T
is one of the possible instances listed above and that variables x
, y
and z
are defined (where they are used) as follows:
|
inlineexplicit |
Builds an universe or empty OS of the specified space dimension.
num_dimensions | The number of dimensions of the vector space enclosing the OS; |
kind | Specifies whether the universe or the empty OS has to be built. |
|
inline |
Ordinary copy constructor.
The complexity argument is ignored.
|
inlineexplicit |
Builds a conservative, upward approximation of y
.
The complexity argument is ignored.
|
inlineexplicit |
Builds an OS from the system of constraints cs
.
The OS inherits the space dimension of cs
.
cs | A system of octagonal constraints. |
std::invalid_argument | Thrown if cs contains a constraint which is not optimally supported by the Octagonal shape domain. |
|
inlineexplicit |
Builds an OS from a system of congruences.
The OS inherits the space dimension of cgs
cgs | A system of congruences. |
std::invalid_argument | Thrown if cgs contains a congruence which is not optimally supported by the Octagonal shape domain. |
|
explicit |
Builds an OS from the system of generators gs
.
Builds the smallest OS containing the polyhedron defined by gs
. The OS inherits the space dimension of gs
.
std::invalid_argument | Thrown if the system of generators is not empty but has no points. |
|
explicit |
Builds an OS from the polyhedron ph
.
Builds an OS containing ph
using algorithms whose complexity does not exceed the one specified by complexity
. If complexity
is ANY_COMPLEXITY
, then the OS built is the smallest one containing ph
.
|
inlineexplicit |
Builds an OS out of a box.
The OS inherits the space dimension of the box. The built OS is the most precise OS that includes the box.
box | The box representing the OS to be built. |
complexity | This argument is ignored as the algorithm used has polynomial complexity. |
std::length_error | Thrown if the space dimension of box exceeds the maximum allowed space dimension. |
|
inlineexplicit |
Builds an OS that approximates a grid.
The OS inherits the space dimension of the grid. The built OS is the most precise OS that includes the grid.
grid | The grid used to build the OS. |
complexity | This argument is ignored as the algorithm used has polynomial complexity. |
std::length_error | Thrown if the space dimension of grid exceeds the maximum allowed space dimension. |
|
inlineexplicit |
Builds an OS from a BD shape.
The OS inherits the space dimension of the BD shape. The built OS is the most precise OS that includes the BD shape.
bd | The BD shape used to build the OS. |
complexity | This argument is ignored as the algorithm used has polynomial complexity. |
std::length_error | Thrown if the space dimension of bd exceeds the maximum allowed space dimension. |
bool Parma_Polyhedra_Library::Octagonal_Shape< T >::contains | ( | const Octagonal_Shape< T > & | y | ) | const |
Returns true
if and only if *this
contains y
.
std::invalid_argument | Thrown if *this and y are dimension-incompatible. |
|
inline |
Returns true
if and only if *this
strictly contains y
.
std::invalid_argument | Thrown if *this and y are dimension-incompatible. |
bool Parma_Polyhedra_Library::Octagonal_Shape< T >::is_disjoint_from | ( | const Octagonal_Shape< T > & | y | ) | const |
Returns true
if and only if *this
and y
are disjoint.
std::invalid_argument | Thrown if x and y are topology-incompatible or dimension-incompatible. |
Poly_Con_Relation Parma_Polyhedra_Library::Octagonal_Shape< T >::relation_with | ( | const Constraint & | c | ) | const |
Returns the relations holding between *this
and the constraint c
.
std::invalid_argument | Thrown if *this and constraint c are dimension-incompatible. |
Poly_Con_Relation Parma_Polyhedra_Library::Octagonal_Shape< T >::relation_with | ( | const Congruence & | cg | ) | const |
Returns the relations holding between *this
and the congruence cg
.
std::invalid_argument | Thrown if *this and cg are dimension-incompatible. |
Poly_Gen_Relation Parma_Polyhedra_Library::Octagonal_Shape< T >::relation_with | ( | const Generator & | g | ) | const |
Returns the relations holding between *this
and the generator g
.
std::invalid_argument | Thrown if *this and generator g are dimension-incompatible. |
bool Parma_Polyhedra_Library::Octagonal_Shape< T >::constrains | ( | Variable | var | ) | const |
Returns true
if and only if var
is constrained in *this
.
std::invalid_argument | Thrown if var is not a space dimension of *this . |
|
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. |
|
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. |
|
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. |
If *this
is empty or expr
is not bounded from above, false
is returned and sup_n
, sup_d
and maximum
are left untouched.
|
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. |
If *this
is empty or expr
is not bounded from above, false
is returned and sup_n
, sup_d
, maximum
and g
are left untouched.
|
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. |
If *this
is empty or expr
is not bounded from below, false
is returned and inf_n
, inf_d
and minimum
are left untouched.
|
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. |
If *this
is empty or expr
is not bounded from below, false
is returned and inf_n
, inf_d
, minimum
and g
are left untouched.
bool Parma_Polyhedra_Library::Octagonal_Shape< T >::frequency | ( | const Linear_Expression & | expr, |
Coefficient & | freq_n, | ||
Coefficient & | freq_d, | ||
Coefficient & | val_n, | ||
Coefficient & | val_d | ||
) | const |
Returns true
if and only if there exist a unique value val
such that *this
saturates the equality expr = val
.
expr | The linear expression for which the frequency is needed; |
freq_n | If true is returned, the value is set to ![]() |
freq_d | If true is returned, the value is set to ![]() |
val_n | The numerator of val ; |
val_d | The denominator of val ; |
std::invalid_argument | Thrown if expr and *this are dimension-incompatible. |
If false
is returned, then freq_n
, freq_d
, val_n
and val_d
are left untouched.
void Parma_Polyhedra_Library::Octagonal_Shape< T >::add_constraint | ( | const Constraint & | c | ) |
Adds a copy of constraint c
to the system of constraints defining *this
.
c | The constraint to be added. |
std::invalid_argument | Thrown if *this and constraint c are dimension-incompatible, or c is not optimally supported by the OS domain. |
|
inline |
Adds the constraints in cs
to the system of constraints defining *this
.
cs | The constraints that will be added. |
std::invalid_argument | Thrown if *this and cs are dimension-incompatible, or cs contains a constraint which is not optimally supported by the OS domain. |
|
inline |
Adds the constraints in cs
to the system of constraints of *this
.
cs | The constraint system to be added to *this . The constraints in cs may be recycled. |
std::invalid_argument | Thrown if *this and cs are dimension-incompatible, or cs contains a constraint which is not optimally supported by the OS domain. |
cs
upon successful or exceptional return is that it can be safely destroyed. void Parma_Polyhedra_Library::Octagonal_Shape< T >::add_congruence | ( | const Congruence & | cg | ) |
Adds to *this
a constraint equivalent to the congruence cg
.
cg | The congruence to be added. |
std::invalid_argument | Thrown if *this and congruence cg are dimension-incompatible, or cg is not optimally supported by the OS domain. |
|
inline |
Adds to *this
constraints equivalent to the congruences in cgs
.
cgs | The congruences to be added. |
std::invalid_argument | Thrown if *this and cgs are dimension-incompatible, or cgs contains a congruence which is not optimally supported by the OS domain. |
|
inline |
Adds to *this
constraints equivalent to the congruences in cgs
.
cgs | The congruence system to be added to *this . The congruences in cgs may be recycled. |
std::invalid_argument | Thrown if *this and cgs are dimension-incompatible, or cgs contains a congruence which is not optimally supported by the OS domain. |
cgs
upon successful or exceptional return is that it can be safely destroyed.
|
inline |
Uses a copy of constraint c
to refine the system of octagonal constraints defining *this
.
c | The constraint. If it is not a octagonal constraint, it will be ignored. |
std::invalid_argument | Thrown if *this and constraint c are dimension-incompatible. |
|
inline |
Uses a copy of congruence cg
to refine the system of octagonal constraints of *this
.
cg | The congruence. If it is not a octagonal equality, it will be ignored. |
std::invalid_argument | Thrown if *this and congruence cg are dimension-incompatible. |
|
inline |
Uses a copy of the constraints in cs
to refine the system of octagonal constraints defining *this
.
cs | The constraint system to be used. Constraints that are not octagonal are ignored. |
std::invalid_argument | Thrown if *this and cs are dimension-incompatible. |
void Parma_Polyhedra_Library::Octagonal_Shape< T >::refine_with_congruences | ( | const Congruence_System & | cgs | ) |
Uses a copy of the congruences in cgs
to refine the system of octagonal constraints defining *this
.
cgs | The congruence system to be used. Congruences that are not octagonal equalities are ignored. |
std::invalid_argument | Thrown if *this and cgs are dimension-incompatible. |
void Parma_Polyhedra_Library::Octagonal_Shape< T >::refine_with_linear_form_inequality | ( | const Linear_Form< Interval< T, Interval_Info > > & | left, |
const Linear_Form< Interval< T, Interval_Info > > & | right | ||
) |
Refines the system of octagonal constraints defining *this
using the constraint expressed by left
right
.
left | The linear form on intervals with floating point boundaries that is at the left of the comparison operator. All of its coefficients MUST be bounded. |
right | The linear form on intervals with floating point boundaries that is at the right of the comparison operator. All of its coefficients MUST be bounded. |
std::invalid_argument | Thrown if left (or right ) is dimension-incompatible with *this . |
This function is used in abstract interpretation to model a filter that is generated by a comparison of two expressions that are correctly approximated by left
and right
respectively.
|
inline |
Refines the system of octagonal constraints defining *this
using the constraint expressed by left
right
, where is the relation symbol specified by
relsym
.
left | The linear form on intervals with floating point boundaries that is at the left of the comparison operator. All of its coefficients MUST be bounded. |
right | The linear form on intervals with floating point boundaries that is at the right of the comparison operator. All of its coefficients MUST be bounded. |
relsym | The relation symbol. |
std::invalid_argument | Thrown if left (or right ) is dimension-incompatible with *this . |
std::runtime_error | Thrown if relsym is not a valid relation symbol. |
This function is used in abstract interpretation to model a filter that is generated by a comparison of two expressions that are correctly approximated by left
and right
respectively.
void Parma_Polyhedra_Library::Octagonal_Shape< T >::unconstrain | ( | Variable | var | ) |
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 . |
void Parma_Polyhedra_Library::Octagonal_Shape< T >::unconstrain | ( | const Variables_Set & | vars | ) |
Computes the cylindrification of *this
with respect to the set of space dimensions vars
, assigning the result to *this
.
vars | 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 vars . |
void Parma_Polyhedra_Library::Octagonal_Shape< T >::intersection_assign | ( | const Octagonal_Shape< T > & | y | ) |
Assigns to *this
the intersection of *this
and y
.
std::invalid_argument | Thrown if *this and y are dimension-incompatible. |
void Parma_Polyhedra_Library::Octagonal_Shape< T >::upper_bound_assign | ( | const Octagonal_Shape< T > & | y | ) |
Assigns to *this
the smallest OS that contains the convex union of *this
and y
.
std::invalid_argument | Thrown if *this and y are dimension-incompatible. |
bool Parma_Polyhedra_Library::Octagonal_Shape< T >::upper_bound_assign_if_exact | ( | const Octagonal_Shape< T > & | y | ) |
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. |
Implementation is based on Theorem 6.3 of [BHZ09b].
bool Parma_Polyhedra_Library::Octagonal_Shape< T >::integer_upper_bound_assign_if_exact | ( | const Octagonal_Shape< T > & | y | ) |
If the integer 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. |
T
is bound to an integer data type.Implementation is based on Theorem 6.8 of [BHZ09b].
void Parma_Polyhedra_Library::Octagonal_Shape< T >::difference_assign | ( | const Octagonal_Shape< T > & | y | ) |
Assigns to *this
the smallest octagon containing the set difference of *this
and y
.
std::invalid_argument | Thrown if *this and y are dimension-incompatible. |
bool Parma_Polyhedra_Library::Octagonal_Shape< T >::simplify_using_context_assign | ( | const Octagonal_Shape< T > & | y | ) |
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. |
void Parma_Polyhedra_Library::Octagonal_Shape< T >::affine_image | ( | Variable | var, |
const Linear_Expression & | expr, | ||
Coefficient_traits::const_reference | denominator = Coefficient_one() |
||
) |
Assigns to *this
the affine image of *this
under the function mapping variable var
into the affine expression specified by expr
and denominator
.
var | The variable to which the affine expression is assigned. |
expr | The numerator of the affine expression. |
denominator | The denominator of the affine expression. |
std::invalid_argument | Thrown if denominator is zero or if expr and *this are dimension-incompatible or if var is not a dimension of *this . |
void Parma_Polyhedra_Library::Octagonal_Shape< T >::affine_form_image | ( | Variable | var, |
const Linear_Form< Interval< T, Interval_Info > > & | lf | ||
) |
Assigns to *this
the affine form image of *this
under the function mapping variable var
into the affine expression(s) specified by lf
.
var | The variable to which the affine expression is assigned. |
lf | The linear form on intervals with floating point boundaries that defines the affine expression(s). ALL of its coefficients MUST be bounded. |
std::invalid_argument | Thrown if lf and *this are dimension-incompatible or if var is not a dimension of *this . |
This function is used in abstract interpretation to model an assignment of a value that is correctly overapproximated by lf
to the floating point variable represented by var
.
void Parma_Polyhedra_Library::Octagonal_Shape< T >::affine_preimage | ( | Variable | var, |
const Linear_Expression & | expr, | ||
Coefficient_traits::const_reference | denominator = Coefficient_one() |
||
) |
Assigns to *this
the affine preimage of *this
under the function mapping variable var
into the affine expression specified by expr
and denominator
.
var | The variable to which the affine expression is substituted. |
expr | The numerator of the affine expression. |
denominator | The denominator of the affine expression. |
std::invalid_argument | Thrown if denominator is zero or if expr and *this are dimension-incompatible or if var is not a dimension of *this . |
void Parma_Polyhedra_Library::Octagonal_Shape< T >::generalized_affine_image | ( | Variable | var, |
Relation_Symbol | relsym, | ||
const Linear_Expression & | expr, | ||
Coefficient_traits::const_reference | denominator = Coefficient_one() |
||
) |
Assigns to *this
the image of *this
with respect to the generalized affine transfer function , where
is the relation symbol encoded by
relsym
.
var | The left hand side variable of the generalized affine transfer function. |
relsym | The relation symbol. |
expr | The numerator of the right hand side affine expression. |
denominator | The denominator of the right hand side affine expression. |
std::invalid_argument | Thrown if denominator is zero or if expr and *this are dimension-incompatible or if var is not a dimension of *this or if relsym is a strict relation symbol. |
void Parma_Polyhedra_Library::Octagonal_Shape< T >::generalized_affine_image | ( | const Linear_Expression & | lhs, |
Relation_Symbol | relsym, | ||
const Linear_Expression & | rhs | ||
) |
Assigns to *this
the image of *this
with respect to the generalized affine transfer function , where
is the relation symbol encoded by
relsym
.
lhs | The left hand side affine expression. |
relsym | The relation symbol. |
rhs | The right hand side affine expression. |
std::invalid_argument | Thrown if *this is dimension-incompatible with lhs or rhs or if relsym is a strict relation symbol. |
void Parma_Polyhedra_Library::Octagonal_Shape< T >::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 .
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 . |
void Parma_Polyhedra_Library::Octagonal_Shape< T >::generalized_affine_preimage | ( | Variable | var, |
Relation_Symbol | relsym, | ||
const Linear_Expression & | expr, | ||
Coefficient_traits::const_reference | denominator = Coefficient_one() |
||
) |
Assigns to *this
the preimage of *this
with respect to the affine relation , where
is the relation symbol encoded by
relsym
.
var | The left hand side variable of the generalized affine transfer function. |
relsym | The relation symbol. |
expr | The numerator of the right hand side affine expression. |
denominator | The denominator of the right hand side affine expression. |
std::invalid_argument | Thrown if denominator is zero or if expr and *this are dimension-incompatible or if var is not a dimension of *this or if relsym is a strict relation symbol. |
void Parma_Polyhedra_Library::Octagonal_Shape< T >::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 , where
is the relation symbol encoded by
relsym
.
lhs | The left hand side affine expression; |
relsym | The relation symbol; |
rhs | The right hand side affine expression. |
std::invalid_argument | Thrown if *this is dimension-incompatible with lhs or rhs or if relsym is a strict relation symbol. |
void Parma_Polyhedra_Library::Octagonal_Shape< T >::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 .
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 . |
|
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. |
void Parma_Polyhedra_Library::Octagonal_Shape< T >::wrap_assign | ( | const Variables_Set & | vars, |
Bounded_Integer_Type_Width | w, | ||
Bounded_Integer_Type_Representation | r, | ||
Bounded_Integer_Type_Overflow | o, | ||
const Constraint_System * | cs_p = 0 , |
||
unsigned | complexity_threshold = 16 , |
||
bool | wrap_individually = true |
||
) |
Wraps the specified dimensions of the vector space.
vars | The set of Variable objects corresponding to the space dimensions to be wrapped. |
w | The width of the bounded integer type corresponding to all the dimensions to be wrapped. |
r | The representation of the bounded integer type corresponding to all the dimensions to be wrapped. |
o | The overflow behavior of the bounded integer type corresponding to all the dimensions to be wrapped. |
cs_p | Possibly null pointer to a constraint system whose variables are contained in vars . If *cs_p depends on variables not in vars , the behavior is undefined. When non-null, the pointed-to constraint system is assumed to represent the conditional or looping construct guard with respect to which wrapping is performed. Since wrapping requires the computation of upper bounds and due to non-distributivity of constraint refinement over upper bounds, passing a constraint system in this way can be more precise than refining the result of the wrapping operation with the constraints in *cs_p . |
complexity_threshold | A precision parameter of the wrapping operator: higher values result in possibly improved precision. |
wrap_individually | true if the dimensions should be wrapped individually (something that results in much greater efficiency to the detriment of precision). |
std::invalid_argument | Thrown if *cs_p is dimension-incompatible with vars , or if *this is dimension-incompatible vars or with *cs_p . |
void Parma_Polyhedra_Library::Octagonal_Shape< T >::drop_some_non_integer_points | ( | Complexity_Class | complexity = ANY_COMPLEXITY | ) |
Possibly tightens *this
by dropping some points with non-integer coordinates.
complexity | The maximal complexity of any algorithms used. |
complexity
is ANY_COMPLEXITY
. void Parma_Polyhedra_Library::Octagonal_Shape< T >::drop_some_non_integer_points | ( | const Variables_Set & | vars, |
Complexity_Class | complexity = ANY_COMPLEXITY |
||
) |
Possibly tightens *this
by dropping some points with non-integer coordinates for the space dimensions corresponding to vars
.
vars | Points with non-integer coordinates for these variables/space-dimensions can be discarded. |
complexity | The maximal complexity of any algorithms used. |
complexity
is ANY_COMPLEXITY
.
|
inline |
Assigns to *this
the result of computing the CC76-extrapolation between *this
and y
.
y | An OS 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. |
void Parma_Polyhedra_Library::Octagonal_Shape< T >::CC76_extrapolation_assign | ( | const Octagonal_Shape< T > & | y, |
Iterator | first, | ||
Iterator | last, | ||
unsigned * | tp = 0 |
||
) |
Assigns to *this
the result of computing the CC76-extrapolation between *this
and y
.
y | An OS that must be contained in *this . |
first | An iterator that points to the first stop_point. |
last | An iterator that points to the last stop_point. |
tp | An optional pointer to an unsigned variable storing the number of available tokens (to be used when applying the widening with tokens delay technique). |
std::invalid_argument | Thrown if *this and y are dimension-incompatible. |
void Parma_Polyhedra_Library::Octagonal_Shape< T >::BHMZ05_widening_assign | ( | const Octagonal_Shape< T > & | y, |
unsigned * | tp = 0 |
||
) |
Assigns to *this
the result of computing the BHMZ05-widening between *this
and y
.
y | An OS 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. |
void Parma_Polyhedra_Library::Octagonal_Shape< T >::limited_BHMZ05_extrapolation_assign | ( | const Octagonal_Shape< T > & | y, |
const Constraint_System & | cs, | ||
unsigned * | tp = 0 |
||
) |
Improves the result of the BHMZ05-widening computation by also enforcing those constraints in cs
that are satisfied by all the points of *this
.
y | An OS that must be contained in *this . |
cs | The system of constraints used to improve the widened OS. |
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 there is in cs a strict inequality. |
void Parma_Polyhedra_Library::Octagonal_Shape< T >::CC76_narrowing_assign | ( | const Octagonal_Shape< T > & | y | ) |
Restores from y
the constraints of *this
, lost by CC76-extrapolation applications.
y | An OS that must contain *this . |
std::invalid_argument | Thrown if *this and y are dimension-incompatible. |
void Parma_Polyhedra_Library::Octagonal_Shape< T >::limited_CC76_extrapolation_assign | ( | const Octagonal_Shape< T > & | y, |
const Constraint_System & | cs, | ||
unsigned * | tp = 0 |
||
) |
Improves the result of the CC76-extrapolation computation by also enforcing those constraints in cs
that are satisfied by all the points of *this
.
y | An OS that must be contained in *this . |
cs | The system of constraints used to improve the widened OS. |
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. |
void Parma_Polyhedra_Library::Octagonal_Shape< T >::add_space_dimensions_and_embed | ( | dimension_type | m | ) |
Adds m
new dimensions and embeds the old OS into the new space.
m | The number of dimensions to add. |
The new dimensions will be those having the highest indexes in the new OS, which is characterized by a system of constraints in which the variables running through the new dimensions are not constrained. For instance, when starting from the OS and adding a third dimension, the result will be the OS
void Parma_Polyhedra_Library::Octagonal_Shape< T >::add_space_dimensions_and_project | ( | dimension_type | m | ) |
Adds m
new dimensions to the OS and does not embed it in the new space.
m | The number of dimensions to add. |
The new dimensions will be those having the highest indexes in the new OS, which is characterized by a system of constraints in which the variables running through the new dimensions are all constrained to be equal to 0. For instance, when starting from the OS and adding a third dimension, the result will be the OS
void Parma_Polyhedra_Library::Octagonal_Shape< T >::concatenate_assign | ( | const Octagonal_Shape< T > & | y | ) |
Assigns to *this
the concatenation of *this
and y
, taken in this order.
std::length_error | Thrown if the concatenation would cause the vector space to exceed dimension max_space_dimension() . |
void Parma_Polyhedra_Library::Octagonal_Shape< T >::remove_space_dimensions | ( | const Variables_Set & | vars | ) |
|
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 . |
void Parma_Polyhedra_Library::Octagonal_Shape< T >::map_space_dimensions | ( | const Partial_Function & | pfunc | ) |
Remaps the dimensions of the vector space according to a partial function.
pfunc | The partial function specifying the destiny of each dimension. |
The template type parameter Partial_Function must provide the following methods.
returns true
if and only if the represented partial function has an empty codomain (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.
returns the maximum value that belongs to the codomain of the partial function.
Let be the represented function and
be the value of
i
. If is defined in
, then
is assigned to
j
and true
is returned. If is undefined in
, then
false
is returned.
The result is undefined if pfunc
does not encode a partial function with the properties described in the specification of the mapping operator.
void Parma_Polyhedra_Library::Octagonal_Shape< T >::expand_space_dimension | ( | Variable | var, |
dimension_type | m | ||
) |
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() . |
If *this
has space dimension , with
, and
var
has space dimension , then the
-th space dimension is expanded to
m
new space dimensions ,
,
,
.
void Parma_Polyhedra_Library::Octagonal_Shape< T >::fold_space_dimensions | ( | const Variables_Set & | vars, |
Variable | dest | ||
) |
Folds the space dimensions in vars
into dest
.
vars | The set of Variable objects corresponding to the space dimensions to be folded; |
dest | 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 dest or with one of the Variable objects contained in vars . Also thrown if dest is contained in vars . |
If *this
has space dimension , with
,
dest
has space dimension ,
vars
is a set of variables whose maximum space dimension is also less than or equal to , and
dest
is not a member of vars
, then the space dimensions corresponding to variables in vars
are folded into the -th space dimension.
void Parma_Polyhedra_Library::Octagonal_Shape< T >::export_interval_constraints | ( | U & | dest | ) | const |
Applies to dest
the interval constraints embedded in *this
.
dest | The object to which the constraints will be added. |
std::invalid_argument | Thrown if *this is dimension-incompatible with dest . |
The template type parameter U must provide the following methods.
returns the space dimension of the object.
sets the object to an empty object.
restricts the object by applying the lower bound lb
to the space dimension dim
and returns false
if and only if the object becomes empty.
restricts the object by applying the upper bound ub
to the space dimension dim
and returns false
if and only if the object becomes empty.
|
inline |
Refines store
with the constraints defining *this
.
store | The interval floating point abstract store to refine. |
|
inline |
Returns a 32-bit hash code for *this
.
If x
and y
are such that x == y
, then x.hash_code() == y.hash_code()
.
|
related |
Output operator.
Writes a textual representation of oct
on s:
false
is written if oct
is an empty polyhedron; true
is written if oct
is a universe polyhedron; a system of constraints defining oct
is written otherwise, all constraints separated by ", ".
|
related |
Swaps x
with y
.
|
related |
Returns true
if and only if x
and y
are the same octagon.
Note that x
and y
may be dimension-incompatible shapes: in this case, the value false
is returned.
|
related |
Returns true
if and only if x
and y
are different shapes.
Note that x
and y
may be dimension-incompatible shapes: in this case, the value true
is returned.
|
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>.
|
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<Temp, Extended_Number_Policy>.
|
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
.
|
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>.
|
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<Temp, Extended_Number_Policy>.
|
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
.
|
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>.
|
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<Temp, Extended_Number_Policy>.
|
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
.
|
related |
|
related |
|
related |
|
related |
|
related |
|
related |
|
related |
|
related |
|
related |
|
related |
|
related |
|
related |
|
related |