Parma_Polyhedra_Library::Box< ITV > Class Template Reference
[C++ Language Interface]

A not necessarily closed, iso-oriented hyperrectangle. More...

#include <Box.defs.hh>

Collaboration diagram for Parma_Polyhedra_Library::Box< ITV >:

List of all members.

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 $0$ , if *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 $\mathrm{var}' \relsym \frac{\mathrm{expr}}{\mathrm{denominator}}$ , where $\mathord{\relsym}$ is the relation symbol encoded by relsym.

void generalized_affine_preimage (Variable var, Relation_Symbol relsym, const Linear_Expression &expr, Coefficient_traits::const_reference denominator=Coefficient_one())

Assigns to *this the preimage of *this with respect to the generalized affine relation $\mathrm{var}' \relsym \frac{\mathrm{expr}}{\mathrm{denominator}}$ , where $\mathord{\relsym}$ is the relation symbol encoded by relsym.

void generalized_affine_image (const Linear_Expression &lhs, Relation_Symbol relsym, const Linear_Expression &rhs)

Assigns to *this the image of *this with respect to the generalized affine relation $\mathrm{lhs}' \relsym \mathrm{rhs}$ , where $\mathord{\relsym}$ is the relation symbol encoded by 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 $\mathrm{lhs}' \relsym \mathrm{rhs}$ , where $\mathord{\relsym}$ is the relation symbol encoded by 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 $\frac{\mathrm{lb\_expr}}{\mathrm{denominator}} \leq \mathrm{var}' \leq \frac{\mathrm{ub\_expr}}{\mathrm{denominator}}$ .

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 $\frac{\mathrm{lb\_expr}}{\mathrm{denominator}} \leq \mathrm{var}' \leq \frac{\mathrm{ub\_expr}}{\mathrm{denominator}}$ .

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 $L_\infty$ distance between 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 $L_\infty$ distance between 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

Detailed Description

template<typename ITV>
class Parma_Polyhedra_Library::Box< ITV >

A not necessarily closed, iso-oriented hyperrectangle.

A Box object represents the Cartesian product of $n$ not necessarily closed and possibly unbounded intervals represented by objects of class ITV, where $n$ is the space dimension of the box.

Definition at line 270 of file Box.defs.hh.

Member Typedef Documentation

template<typename ITV>

typedef ITV Parma_Polyhedra_Library::Box< ITV >::interval_type

The type of intervals used to implement the box.

Definition at line 273 of file Box.defs.hh.

template<typename ITV>

typedef std::vector<ITV> Parma_Polyhedra_Library::Box< ITV >::Sequence [private]

The type of sequence used to implement the box.

Definition at line 1528 of file Box.defs.hh.

template<typename ITV>

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.

Constructor & Destructor Documentation

template<typename ITV>

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.

Parameters:

	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 }

template<typename ITV>

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.

00070   : seq(y.seq), status(y.status) {
00071 }

template<typename ITV>

template<typename Other_ITV>

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 }

template<typename ITV>

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.

Parameters:

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 }

template<typename ITV>

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.

Parameters:

	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 }

template<typename ITV>

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.

Exceptions:

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.

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 }

template<typename ITV>

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.

Parameters:

	gs	The generator system describing the polyhedron to be approximated.
	dummy	A dummy tag to syntactically differentiate this one from the other constructors.

Exceptions:

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 }

template<typename ITV>

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.

Parameters:

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 }

template<typename ITV>

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.

Parameters:

	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 }

template<typename ITV>

template<typename T>

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 }

template<typename ITV>

template<typename T>

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 }

template<typename ITV>

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.

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 }

template<typename ITV>

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.

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 }

template<typename ITV>

template<typename D1, typename D2, typename R>

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 }

Member Function Documentation

template<typename ITV>

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 }

template<typename T>

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.

00358                                        {
00359   return false;
00360 }

template<typename T>

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.

00364                                        {
00365   return false;
00366 }

template<typename ITV>

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.

00075                                 {
00076   seq = y.seq;
00077   status = y.status;
00078   return *this;
00079 }

template<typename ITV>

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 }

template<typename ITV>

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.

00121                                 {
00122   return seq.size();
00123 }

template<typename ITV>

dimension_type Parma_Polyhedra_Library::Box< ITV >::affine_dimension ( ) const [inline]

Returns $0$ , 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 }

template<typename ITV>

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().

00174                          {
00175   return marked_empty() || check_empty();
00176 }

template<typename ITV>

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 }

template<typename ITV>

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 }

template<typename ITV>

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 }

template<typename ITV>

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 }

template<typename ITV>

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 }

template<typename ITV>

bool Parma_Polyhedra_Library::Box< ITV >::constrains ( Variable var ) const [inline]

Returns true if and only if var is constrained in *this.

Exceptions:

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 }

template<typename ITV>

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.

Exceptions:

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

Definition at line 862 of file Box.templates.hh.

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 }

template<typename ITV>

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.

Exceptions:

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

Definition at line 800 of file Box.templates.hh.

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 }

template<typename ITV>

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.

Exceptions:

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

Definition at line 947 of file Box.templates.hh.

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 }

template<typename ITV>

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.

Exceptions:

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 }

template<typename ITV>

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.

Exceptions:

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 }

template<typename ITV>

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.

Parameters:

	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.

Exceptions:

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.

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 }

template<typename ITV>

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.

Parameters:

	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.

Exceptions:

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.

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 }

template<typename ITV>

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.

Parameters:

	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.

Exceptions:

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.

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 }

template<typename ITV>

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.

Parameters:

	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.

Exceptions:

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.

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 }

template<typename ITV>

bool Parma_Polyhedra_Library::Box< ITV >::contains ( const Box< ITV > & y ) const [inline]

Returns true if and only if *this contains y.

Exceptions:

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 }

template<typename ITV>

bool Parma_Polyhedra_Library::Box< ITV >::strictly_contains ( const Box< ITV > & y ) const [inline]

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

Exceptions:

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 }

template<typename ITV>

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.

Exceptions:

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 }

template<typename ITV>

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().

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 }

template<typename ITV>

void Parma_Polyhedra_Library::Box< ITV >::add_constraint ( const Constraint & c ) [inline]

Use the constraint c to refine *this. FIXME: this is not true.

Parameters:

c

The constraint to be added. If it is not an interval constraint, it will be simply ignored.

Exceptions:

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 }

template<typename ITV>

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.

Parameters:

cs

The constraints to be added. Constraints that are not interval constraints will be simply ignored.

Exceptions:

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 }

template<typename T>

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.

Parameters:

cs The constraints to be added. Constraints that are not interval constraints will be simply ignored. The constraints in cs may be recycled.

Exceptions:

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

Warning:: The only assumption that can be made on 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 }

template<typename ITV>

void Parma_Polyhedra_Library::Box< ITV >::add_congruence ( const Congruence & cg ) [inline]

Use the congruence cg to refine *this.

Parameters:

cg

The congruence to be used. If it is not a non-relational equality, the box is not changed.

Exceptions:

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 }

template<typename ITV>

void Parma_Polyhedra_Library::Box< ITV >::add_congruences ( const Congruence_System & cgs ) [inline]

Use the congruences in cgs to refine *this.

Parameters:

cgs

The congruences to be used. Congruences that are not non-relational equalities are not added although their space dimension is checked for compatibility.

Exceptions:

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 }

template<typename T>

void Parma_Polyhedra_Library::Box< T >::add_recycled_congruences ( Congruence_System & cgs ) [inline]

Use the congruences in cgs to refine *this.

Parameters:

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.

Exceptions:

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

Warning:: The only assumption that can be made on 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 }

template<typename ITV>

void Parma_Polyhedra_Library::Box< ITV >::refine_with_constraint ( const Constraint & c ) [inline]

Use the constraint c to refine *this.

Parameters:

c

The constraint to be used for refinement.

Exceptions:

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 }

template<typename ITV>

void Parma_Polyhedra_Library::Box< ITV >::refine_with_constraints ( const Constraint_System & cs ) [inline]

Use the constraints in cs to refine *this.

Parameters:

cs

The constraints to be used for refinement.

Exceptions:

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 }

template<typename ITV>

void Parma_Polyhedra_Library::Box< ITV >::refine_with_congruence ( const Congruence & cg ) [inline]

Use the congruence cg to refine *this.

Parameters:

cg

The congruence to be used for refinement.

Exceptions:

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 }

template<typename ITV>

void Parma_Polyhedra_Library::Box< ITV >::refine_with_congruences ( const Congruence_System & cgs ) [inline]

Use the congruences in cgs to refine *this.

Parameters:

cgs

The congruences to be used for refinement.

Exceptions:

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 }

template<typename ITV>

void Parma_Polyhedra_Library::Box< ITV >::propagate_constraint ( const Constraint & c ) [inline]

Use the constraint c for constraint propagation on *this.

Parameters:

c

The constraint to be used for constraint propagation.

Exceptions:

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 }

template<typename ITV>

void Parma_Polyhedra_Library::Box< ITV >::propagate_constraints ( const Constraint_System & cs ) [inline]

Use the constraints in cs for constraint propagagion on *this.

Parameters:

cs

The constraints to be used for constraint propagation.

Exceptions:

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 }

template<typename ITV>

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.

Parameters:

var

The space dimension that will be unconstrained.

Exceptions:

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 }

template<typename ITV>

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.

Parameters:

to_be_unconstrained

The set of space dimension that will be unconstrained.

Exceptions:

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 }

template<typename ITV>

void Parma_Polyhedra_Library::Box< ITV >::intersection_assign ( const Box< ITV > & y ) [inline]

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

Exceptions:

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

Definition at line 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 }

template<typename ITV>

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.

Exceptions:

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 }

template<typename ITV>

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.

Exceptions:

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

Definition at line 231 of file Box.inlines.hh.

00231                                                 {
00232   // TODO: this must be properly implemented.
00233   return false;
00234 }

template<typename ITV>

void Parma_Polyhedra_Library::Box< ITV >::difference_assign ( const Box< ITV > & y ) [inline]

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

Exceptions:

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 }

template<typename ITV>

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.

Exceptions:

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

Definition at line 1549 of file Box.templates.hh.

01549                                                     {
01550   // FIXME: provide a real implementation.
01551   used(y);
01552   return true;
01553 }

template<typename ITV>

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.

Parameters:

	var	The variable to which the affine expression is assigned;
	expr	The numerator of the affine expression;
	denominator	The denominator of the affine expression (optional argument with default value 1).

Exceptions:

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.

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 }

template<typename ITV>

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.

Parameters:

	var	The variable to which the affine expression is substituted;
	expr	The numerator of the affine expression;
	denominator	The denominator of the affine expression (optional argument with default value 1).

Exceptions:

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.

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 }

template<typename ITV>

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 $\mathrm{var}' \relsym \frac{\mathrm{expr}}{\mathrm{denominator}}$ , where $\mathord{\relsym}$ is the relation symbol encoded by relsym.

Parameters:

	var	The left hand side variable of the generalized affine 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).

Exceptions:

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.

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 }

template<typename ITV>

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 $\mathrm{var}' \relsym \frac{\mathrm{expr}}{\mathrm{denominator}}$ , where $\mathord{\relsym}$ is the relation symbol encoded by relsym.

Parameters:

	var	The left hand side variable of the generalized affine 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).

Exceptions:

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.

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 }

template<typename ITV>

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 $\mathrm{lhs}' \relsym \mathrm{rhs}$ , where $\mathord{\relsym}$ is the relation symbol encoded by relsym.

Parameters:

	lhs	The left hand side affine expression;
	relsym	The relation symbol;
	rhs	The right hand side affine expression.

Exceptions:

std::invalid_argument Thrown if *this is dimension-incompatible with lhs or rhs.

Definition at line 2966 of file Box.templates.hh.

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 }

template<typename ITV>

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 $\mathrm{lhs}' \relsym \mathrm{rhs}$ , where $\mathord{\relsym}$ is the relation symbol encoded by relsym.

Parameters:

	lhs	The left hand side affine expression;
	relsym	The relation symbol;
	rhs	The right hand side affine expression.

Exceptions:

std::invalid_argument Thrown if *this is dimension-incompatible with lhs or rhs.

Definition at line 3175 of file Box.templates.hh.

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 }

template<typename ITV>

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 $\frac{\mathrm{lb\_expr}}{\mathrm{denominator}} \leq \mathrm{var}' \leq \frac{\mathrm{ub\_expr}}{\mathrm{denominator}}$ .

Parameters:

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

Exceptions:

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.

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 }

template<typename ITV>

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 $\frac{\mathrm{lb\_expr}}{\mathrm{denominator}} \leq \mathrm{var}' \leq \frac{\mathrm{ub\_expr}}{\mathrm{denominator}}$ .

Parameters:

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

Exceptions:

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.

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 }

template<typename ITV>

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.

Exceptions:

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 }

template<typename ITV>

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 }

template<typename ITV>

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.

Parameters:

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

Exceptions:

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 }

template<typename ITV>

template<typename Iterator>

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.

Parameters:

	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.

Exceptions:

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 }

template<typename T>

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 }

template<typename ITV>

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.

Parameters:

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

Exceptions:

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 }

template<typename ITV>

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.

Parameters:

y A Box that must contain *this.

Exceptions:

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

Note:: As was the case for widening operators, the argument y is meant to denote the value computed in the previous iteration step, whereas *this denotes the value computed in the current iteration step (in the decreasing iteration sequence). Hence, the call x.CC76_narrowing_assign(y) will assign to x the result of the computation $\mathtt{y} \Delta \mathtt{x}$ .

Definition at line 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 }

template<typename ITV>

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.

Parameters:

m

The number of dimensions to add.

The new dimensions will be those having the highest indexes in the new box, which is defined by a system of interval constraints in which the variables running through the new dimensions are unconstrained. For instance, when starting from the box $\cB \sseq \Rset^2$ and adding a third dimension, the result will be the box

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

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 }

template<typename ITV>

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.

Parameters:

m

The number of dimensions to add.

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

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

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 }

template<typename ITV>

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 $B \sseq \Rset^n$ and $D \sseq \Rset^m$ be the boxes corresponding, on entry, to *this and y, respectively. Upon successful completion, *this will represent the box $R \sseq \Rset^{n+m}$ such that

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

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

Definition at line 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 }

template<typename ITV>

void Parma_Polyhedra_Library::Box< ITV >::remove_space_dimensions ( const Variables_Set & to_be_removed ) [inline]

Removes all the specified dimensions.

Parameters:

to_be_removed

The set of Variable objects corresponding to the dimensions to be removed.

Exceptions:

std::invalid_argument Thrown if *this is dimension-incompatible with one of the Variable objects contained in to_be_removed.

Definition at line 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 }

template<typename ITV>

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.

Exceptions:

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 }

template<typename ITV>

template<typename Partial_Function>

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.

Parameters:

pfunc

The partial function specifying the destiny of each dimension.

The template class Partial_Function must provide the following methods.

      bool has_empty_codomain() const

returns true if and only if the represented partial function has an empty co-domain (i.e., it is always undefined). The has_empty_codomain() method will always be called before the methods below. However, if has_empty_codomain() returns true, none of the functions below will be called.

      dimension_type max_in_codomain() const

returns the maximum value that belongs to the co-domain of the partial function.

      bool maps(dimension_type i, dimension_type& j) const

Let

be the represented function and $k$

be the value of i. If $f$

is defined in $k$

, then

is assigned to j and true is returned. If $f$

is undefined in $k$

, then false is returned.

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

Definition at line 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 }

template<typename ITV>

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.

Parameters:

	var	The variable corresponding to the space dimension to be replicated;
	m	The number of replicas to be created.

Exceptions:

	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 $n$

, with

, and var has space dimension $k \leq n$ , then the $k$

-th space dimension is expanded to m new space dimensions $n$

,

, $\dots$ , $n+m-1$

.

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 }

template<typename ITV>

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.

Parameters:

	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.

Exceptions:

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.

If *this has space dimension $n$

, with

, var has space dimension $k \leq n$ , to_be_folded is a set of variables whose maximum space dimension is also less than or equal to $n$

, and var is not a member of to_be_folded, then the space dimensions corresponding to variables in to_be_folded are folded into the $k$

-th space dimension.

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 }

template<typename ITV>

const ITV & Parma_Polyhedra_Library::Box< ITV >::get_interval ( Variable var ) const [inline]

Returns a reference the interval that bounds var.

Exceptions:

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 }

template<typename ITV>

void Parma_Polyhedra_Library::Box< ITV >::set_interval	(	Variable	var,
		const ITV &	i
	)			`[inline]`

Sets to i the interval that bounds var.

Exceptions:

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 }

template<typename ITV>

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 $I$ the interval corresponding to the k-th space dimension. If $I$ 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 $I$ is closed and is set to false otherwise; n and d are assigned the integers $n$ and $d$ such that the canonical fraction $n/d$ corresponds to the greatest lower bound of $I$ . The fraction $n/d$ is in canonical form if and only if $n$ and $d$ have no common factors and $d$ is positive, $0/1$ 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 }

template<typename ITV>

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 $I$ the interval corresponding to the k-th space dimension. If $I$ 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 $I$ is closed and is set to false otherwise; n and d are assigned the integers $n$ and $d$ such that the canonical fraction $n/d$ corresponds to the least upper bound of $I$ .

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 }

template<typename ITV>

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 }

template<typename ITV>

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 }

template<typename ITV>

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 }

template<typename ITV>

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 }

template<typename ITV>

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 }

template<typename ITV>

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 }

template<typename ITV>

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().

template<typename ITV>

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 }

template<typename ITV>

void Parma_Polyhedra_Library::Box< ITV >::print ( ) const

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

template<typename ITV>

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 }

template<typename ITV>

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().

00037                              {
00038   return status.test_empty_up_to_date() && status.test_empty();
00039 }

template<typename ITV>

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.

00043                     {
00044   status.set_empty();
00045   status.set_empty_up_to_date();
00046 }

template<typename ITV>

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 }

template<typename ITV>

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 }

template<typename ITV>

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 }

template<typename ITV>

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 }

template<typename ITV>

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.

00135                                                  {
00136   assert(k < seq.size());
00137   return seq[k];
00138 }

template<typename ITV>

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.

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 }

template<typename ITV>

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.

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 }

template<typename ITV>

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 }

template<typename ITV>

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.

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 }

template<typename ITV>

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 }

template<typename ITV>

void Parma_Polyhedra_Library::Box< ITV >::refine_no_check ( const Constraint & c ) [inline, private]

Uses the constraint c to refine *this.

Parameters:

c

The constraint to be added. Non-interval constraints are ignored.

Warning:: If c and *this are dimension-incompatible, the behavior is undefined.

Definition at line 1845 of file Box.templates.hh.

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 }

template<typename ITV>

void Parma_Polyhedra_Library::Box< ITV >::refine_no_check ( const Constraint_System & cs ) [inline, private]

Uses the constraints in cs to refine *this.

Parameters:

cs

The constraints to be added. Non-interval constraints are ignored.

Warning:: If 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 }

template<typename ITV>

void Parma_Polyhedra_Library::Box< ITV >::refine_no_check ( const Congruence & cg ) [inline, private]

Uses the congruence cg to refine *this.

Parameters:

cg

The congruence to be added. Nontrivial proper congruences are ignored.

Warning:: If cg and *this are dimension-incompatible, the behavior is undefined.

Definition at line 1883 of file Box.templates.hh.

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 }

template<typename ITV>

void Parma_Polyhedra_Library::Box< ITV >::refine_no_check ( const Congruence_System & cgs ) [inline, private]

Uses the congruences in cgs to refine *this.

Parameters:

cgs

The congruences to be added. Nontrivial proper congruences are ignored.

Warning:: If 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 }

template<typename ITV>

void Parma_Polyhedra_Library::Box< ITV >::propagate_constraint_no_check ( const Constraint & c ) [inline, private]

Propagates the constraint c to refine *this.

Parameters:

c

The constraint to be propagated.

Warning:: If c and *this are dimension-incompatible, the behavior is undefined.
This method may lead to non-termination.

For any expression $e$

, we denote by $\left\uparrow e \right\uparrow$ (resp., $\left\downarrow e \right\downarrow$ ) the result of any computation that is guaranteed to yield an upper (resp., lower) approximation of $e$

. So there exists $\epsilon \in \Rset$ with $\epsilon \geq 0$ such that $\left\uparrow e \right\uparrow = e + \epsilon$ . If $\epsilon = 0$ we say that the computation of $\left\uparrow e \right\uparrow$ is exact; we say it is inexact otherwise. Similarly for $\left\downarrow e \right\downarrow$ .

Consider a constraint of the general form

$z + \sum_{i \in I}{a_ix_i} \relsym 0,$

where $z \in \Zset$ , $I$ is a set of indices, $a_i \in \Zset$ with $a_i \neq 0$ for each $i \in I$ , and $\mathord{\relsym} \in \{ \mathord{\geq}, \mathord{>}, \mathord{=} \}$ . The set $I$ is subdivided into the disjoint sets $P$ and $N$ such that, for each $i \in I$ , $a_i > 0$ if $i \in P$ and $a_i < 0$ if $i \in N$ . Suppose that, for each $i \in P \union N$ a variation interval $\chi_i \sseq \Rset$ is known for $x_i$ and that the infimum and the supremum of $\chi_i$ are denoted, respectively, by $\chi_i^\mathrm{l}$ and $\chi_i^\mathrm{u}$ , where $\chi_i^\mathrm{l}, \chi_i^\mathrm{u} \in \Rset \union \{ -\infty, +\infty \}$ .

For each $k \in P$ , we have

$x_k \relsym \frac{1}{a_k} \Biggl( - z - \sum_{i \in N}{a_ix_i} - \sum_{\genfrac{}{}{0pt}{} {\scriptstyle i \in P} {\scriptstyle i \neq k}}{a_ix_i} \Biggr).$

Thus, if $\chi_i^\mathrm{l} \in \Rset$ for each $i \in N$ and $\chi_i^\mathrm{u} \in \Rset$ for each $i \in P \setdiff \{ k \}$ , we have

$x_k \geq \Biggl\downarrow \frac{1}{a_k} \Biggl( - z - \sum_{i \in N}{a_i\chi_i^\mathrm{l}} - \sum_{\genfrac{}{}{0pt}{} {\scriptstyle i \in P} {\scriptstyle i \neq k}}{a_i\chi_i^\mathrm{u}} \Biggr) \Biggr\downarrow$

and, if $\mathord{\relsym} \in \{ \mathord{=} \}$ , $\chi_i^\mathrm{u} \in \Rset$ for each $i \in N$ and $\chi_i^\mathrm{l} \in \Rset$ for each $P \setdiff \{ k \}$ ,

$x_k \leq \Biggl\uparrow \frac{1}{a_k} \Biggl( - z - \sum_{i \in N}{a_i\chi_i^\mathrm{u}} - \sum_{\genfrac{}{}{0pt}{} {\scriptstyle i \in P} {\scriptstyle i \neq k}}{a_i\chi_i^\mathrm{l}} \Biggr) \Biggl\uparrow.$

In the first inequality, the relation is strict if $\mathord{\relsym} \in \{ \mathord{>} \}$ , or if $\chi_i^\mathrm{l} \notin \chi_i$ for some $i \in N$ , or if $\chi_i^\mathrm{u} \notin \chi_i$ for some $i \in P \setdiff \{ k \}$ , or if the computation is inexact. In the second inequality, the relation is strict if $\chi_i^\mathrm{u} \notin \chi_i$ for some $i \in N$ , or if $\chi_i^\mathrm{l} \notin \chi_i$ for some $i \in P \setdiff \{ k \}$ , or if the computation is inexact.

For each $k \in N$ , we have

$\frac{1}{a_k} \Biggl( - z - \sum_{\genfrac{}{}{0pt}{} {\scriptstyle i \in N} {\scriptstyle i \neq k}}{a_ix_i} - \sum_{i \in P}{a_ix_i} \Biggr) \relsym x_k.$

Thus, if $\chi_i^\mathrm{l} \in \Rset$ for each $i \in N \setdiff \{ k \}$ and $\chi_i^\mathrm{u} \in \Rset$ for each $i \in P$ , we have

$\Biggl\uparrow \frac{1}{a_k} \Biggl( - z - \sum_{\genfrac{}{}{0pt}{} {\scriptstyle i \in N} {\scriptstyle i \neq k}}{a_i\chi_i^\mathrm{l}} - \sum_{i \in P}{a_i\chi_i^\mathrm{u}} \Biggr) \Biggl\uparrow \geq x_k$

and, if $\mathord{\relsym} \in \{ \mathord{=} \}$ , $\chi_i^\mathrm{u} \in \Rset$ for each $i \in N \setdiff \{ k \}$ and $\chi_i^\mathrm{l} \in \Rset$ for each $i \in P$ ,

$\Biggl\downarrow \frac{1}{a_k} \Biggl( - z - \sum_{\genfrac{}{}{0pt}{} {\scriptstyle i \in N} {\scriptstyle i \neq k}}{a_i\chi_i^\mathrm{u}} - \sum_{i \in P}{a_i\chi_i^\mathrm{l}} \Biggr) \Biggl\downarrow \leq x_k.$

In the first inequality, the relation is strict if $\mathord{\relsym} \in \{ \mathord{>} \}$ , or if $\chi_i^\mathrm{u} \notin \chi_i$ for some $i \in P$ , or if $\chi_i^\mathrm{l} \notin \chi_i$ for some $i \in N \setdiff \{ k \}$ , or if the computation is inexact. In the second inequality, the relation is strict if $\chi_i^\mathrm{l} \notin \chi_i$ for some $i \in P$ , or if $\chi_i^\mathrm{u} \notin \chi_i$ for some $i \in N \setdiff \{ k \}$ , or if the computation is inexact.

Definition at line 1960 of file Box.templates.hh.

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 }

template<typename ITV>

void Parma_Polyhedra_Library::Box< ITV >::propagate_constraints_no_check ( const Constraint_System & cs ) [inline, private]

Propagates the constraints in cs to refine *this.

Parameters:

cs

The constraints to be propagated.

Warning:: If 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 }

template<typename ITV>

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.

Parameters:

	expr	The linear expression to test;
	from_above	`true` if and only if the boundedness of interest is "from above".

Exceptions:

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 }

template<typename ITV>

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.

Parameters:

	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.

Exceptions:

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

If *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 }

template<typename ITV>

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.

Parameters:

	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;

Exceptions:

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

If *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.

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 }

template<typename ITV>

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().

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 }

template<typename ITV>

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 }

template<typename ITV>

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 }

template<typename ITV>

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 }

template<typename ITV>

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 }

template<typename ITV>

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 }

template<typename ITV>

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 }

template<typename ITV>

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 }

template<typename ITV>

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 }

template<typename ITV>

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 }

template<typename ITV>

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 }

template<typename ITV>

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.

03613                                                               {
03614   std::ostringstream s;
03615   s << "PPL::Box::" << method << ":" << std::endl
03616     << reason;
03617   throw std::invalid_argument(s.str());
03618 }

Friends And Related Function Documentation

template<typename ITV>

friend class Parma_Polyhedra_Library::Box [friend]

Definition at line 1512 of file Box.defs.hh.

template<typename ITV>

bool operator==	(	const Box< ITV > &	x,
		const Box< ITV > &	y
	)			`[friend]`

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 }

template<typename ITV>

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 }

template<typename ITV>

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

template<typename ITV>

bool operator!=	(	const Box< ITV > &	x,
		const Box< ITV > &	y
	)			`[related]`

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.

00260                                                  {
00261   return !(x == y);
00262 }

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

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

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

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

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

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

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

The direction of the approximation is specified by dir.

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

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

The direction of the approximation is specified by dir.

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

Definition at line 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 }

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

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

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

The direction of the approximation is specified by dir.

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

Definition at line 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 }

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

template<typename ITV>

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.

Returns:: true if the constraint c is an interval constraint; false otherwise.

Parameters:

	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 }

Member Data Documentation

template<typename ITV>

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.

template<typename ITV>

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.

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

Parma_Polyhedra_Library::Box< ITV > Class Template Reference [C++ Language Interface]

Exception Throwers

Public Types

Public Member Functions

Static Public Member Functions

Private Types

Private Member Functions

Private Attributes

Friends

Related Functions

Classes

Detailed Description

template<typename ITV> class Parma_Polyhedra_Library::Box< ITV >

Member Typedef Documentation

Constructor & Destructor Documentation

Member Function Documentation

Friends And Related Function Documentation

Member Data Documentation

Parma_Polyhedra_Library::Box< ITV > Class Template Reference
[C++ Language Interface]

template<typename ITV>
class Parma_Polyhedra_Library::Box< ITV >