24 #ifndef PPL_Partially_Reduced_Product_inlines_hh
25 #define PPL_Partially_Reduced_Product_inlines_hh 1
35 template <
typename D1,
typename D2,
typename R>
43 template <
typename D1,
typename D2,
typename R>
50 : (throw_space_dimension_overflow(
"Partially_Reduced_Product(n, k)",
51 "n exceeds the maximum "
52 "allowed space dimension"),
55 d2(num_dimensions, kind) {
59 template <
typename D1,
typename D2,
typename R>
67 template <
typename D1,
typename D2,
typename R>
75 template <
typename D1,
typename D2,
typename R>
83 template <
typename D1,
typename D2,
typename R>
91 template <
typename D1,
typename D2,
typename R>
96 : d1(ph, complexity), d2(ph, complexity) {
100 template <
typename D1,
typename D2,
typename R>
105 : d1(ph, complexity), d2(ph, complexity) {
109 template <
typename D1,
typename D2,
typename R>
117 template <
typename D1,
typename D2,
typename R>
118 template <
typename Interval>
126 template <
typename D1,
typename D2,
typename R>
127 template <
typename U>
135 template <
typename D1,
typename D2,
typename R>
136 template <
typename U>
144 template <
typename D1,
typename D2,
typename R>
149 : d1(y.d1), d2(y.d2) {
153 template <
typename D1,
typename D2,
typename R>
154 template <
typename E1,
typename E2,
typename S>
159 : d1(y.space_dimension()), d2(y.space_dimension()), reduced(false) {
166 template <
typename D1,
typename D2,
typename R>
171 template <
typename D1,
typename D2,
typename R>
174 return d1.external_memory_in_bytes() + d2.external_memory_in_bytes();
177 template <
typename D1,
typename D2,
typename R>
183 template <
typename D1,
typename D2,
typename R>
186 PPL_ASSERT(d1.space_dimension() == d2.space_dimension());
187 return d1.space_dimension();
190 template <
typename D1,
typename D2,
typename R>
196 return std::min(d1_dim, d2_dim);
199 template <
typename D1,
typename D2,
typename R>
208 template <
typename D1,
typename D2,
typename R>
212 d1.unconstrain(vars);
213 d2.unconstrain(vars);
216 template <
typename D1,
typename D2,
typename R>
220 d1.intersection_assign(y.
d1);
221 d2.intersection_assign(y.
d2);
222 clear_reduced_flag();
225 template <
typename D1,
typename D2,
typename R>
231 d1.difference_assign(y.
d1);
232 d2.difference_assign(y.
d2);
233 clear_reduced_flag();
236 template <
typename D1,
typename D2,
typename R>
242 d1.upper_bound_assign(y.
d1);
243 d2.upper_bound_assign(y.
d2);
246 template <
typename D1,
typename D2,
typename R>
253 bool ub_exact = d1_copy.upper_bound_assign_if_exact(y.
d1);
257 ub_exact = d2.upper_bound_assign_if_exact(y.
d2);
266 template <
typename D1,
typename D2,
typename R>
271 Coefficient_traits::const_reference denominator) {
272 d1.affine_image(var, expr, denominator);
273 d2.affine_image(var, expr, denominator);
274 clear_reduced_flag();
277 template <
typename D1,
typename D2,
typename R>
282 Coefficient_traits::const_reference denominator) {
283 d1.affine_preimage(var, expr, denominator);
284 d2.affine_preimage(var, expr, denominator);
285 clear_reduced_flag();
288 template <
typename D1,
typename D2,
typename R>
294 Coefficient_traits::const_reference denominator) {
295 d1.generalized_affine_image(var, relsym, expr, denominator);
296 d2.generalized_affine_image(var, relsym, expr, denominator);
297 clear_reduced_flag();
300 template <
typename D1,
typename D2,
typename R>
306 Coefficient_traits::const_reference denominator) {
307 d1.generalized_affine_preimage(var, relsym, expr, denominator);
308 d2.generalized_affine_preimage(var, relsym, expr, denominator);
309 clear_reduced_flag();
312 template <
typename D1,
typename D2,
typename R>
318 d1.generalized_affine_image(lhs, relsym, rhs);
319 d2.generalized_affine_image(lhs, relsym, rhs);
320 clear_reduced_flag();
323 template <
typename D1,
typename D2,
typename R>
329 d1.generalized_affine_preimage(lhs, relsym, rhs);
330 d2.generalized_affine_preimage(lhs, relsym, rhs);
331 clear_reduced_flag();
335 template <
typename D1,
typename D2,
typename R>
341 Coefficient_traits::const_reference denominator) {
342 d1.bounded_affine_image(var, lb_expr, ub_expr, denominator);
343 d2.bounded_affine_image(var, lb_expr, ub_expr, denominator);
344 clear_reduced_flag();
347 template <
typename D1,
typename D2,
typename R>
353 Coefficient_traits::const_reference denominator) {
354 d1.bounded_affine_preimage(var, lb_expr, ub_expr, denominator);
355 d2.bounded_affine_preimage(var, lb_expr, ub_expr, denominator);
356 clear_reduced_flag();
359 template <
typename D1,
typename D2,
typename R>
365 d1.time_elapse_assign(y.
d1);
366 d2.time_elapse_assign(y.
d2);
367 PPL_ASSERT_HEAVY(OK());
370 template <
typename D1,
typename D2,
typename R>
373 d1.topological_closure_assign();
374 d2.topological_closure_assign();
377 template <
typename D1,
typename D2,
typename R>
386 template <
typename D1,
typename D2,
typename R>
389 d1.add_constraint(c);
390 d2.add_constraint(c);
391 clear_reduced_flag();
394 template <
typename D1,
typename D2,
typename R>
397 d1.refine_with_constraint(c);
398 d2.refine_with_constraint(c);
399 clear_reduced_flag();
402 template <
typename D1,
typename D2,
typename R>
405 d1.add_congruence(cg);
406 d2.add_congruence(cg);
407 clear_reduced_flag();
410 template <
typename D1,
typename D2,
typename R>
413 d1.refine_with_congruence(cg);
414 d2.refine_with_congruence(cg);
415 clear_reduced_flag();
418 template <
typename D1,
typename D2,
typename R>
422 d1.add_constraints(cs);
423 d2.add_constraints(cs);
424 clear_reduced_flag();
427 template <
typename D1,
typename D2,
typename R>
431 d1.refine_with_constraints(cs);
432 d2.refine_with_constraints(cs);
433 clear_reduced_flag();
436 template <
typename D1,
typename D2,
typename R>
440 d1.add_congruences(cgs);
441 d2.add_congruences(cgs);
442 clear_reduced_flag();
445 template <
typename D1,
typename D2,
typename R>
449 d1.refine_with_congruences(cgs);
450 d2.refine_with_congruences(cgs);
451 clear_reduced_flag();
454 template <
typename D1,
typename D2,
typename R>
459 d1.drop_some_non_integer_points(complexity);
460 d2.drop_some_non_integer_points(complexity);
461 clear_reduced_flag();
464 template <
typename D1,
typename D2,
typename R>
470 d1.drop_some_non_integer_points(vars, complexity);
471 d2.drop_some_non_integer_points(vars, complexity);
472 clear_reduced_flag();
475 template <
typename D1,
typename D2,
typename R>
485 template <
typename D1,
typename D2,
typename R>
492 template <
typename D1,
typename D2,
typename R>
499 template <
typename D1,
typename D2,
typename R>
503 return d1.is_empty() || d2.is_empty();
506 template <
typename D1,
typename D2,
typename R>
509 return d1.is_universe() && d2.is_universe();
512 template <
typename D1,
typename D2,
typename R>
516 return d1.is_topologically_closed() && d2.is_topologically_closed();
519 template <
typename D1,
typename D2,
typename R>
525 return d1.is_disjoint_from(y.
d1) || d2.is_disjoint_from(y.
d2);
528 template <
typename D1,
typename D2,
typename R>
532 return d1.is_discrete() || d2.is_discrete();
535 template <
typename D1,
typename D2,
typename R>
539 return d1.is_bounded() || d2.is_bounded();
542 template <
typename D1,
typename D2,
typename R>
547 return d1.bounds_from_above(expr) || d2.bounds_from_above(expr);
550 template <
typename D1,
typename D2,
typename R>
555 return d1.bounds_from_below(expr) || d2.bounds_from_below(expr);
558 template <
typename D1,
typename D2,
typename R>
562 return d1.constrains(var) || d2.constrains(var);
565 template <
typename D1,
typename D2,
typename R>
577 d1.widening_assign(y.
d1, tp);
578 d2.widening_assign(y.
d2, tp);
581 template <
typename D1,
typename D2,
typename R>
585 d1.add_space_dimensions_and_embed(m);
586 d2.add_space_dimensions_and_embed(m);
589 template <
typename D1,
typename D2,
typename R>
593 d1.add_space_dimensions_and_project(m);
594 d2.add_space_dimensions_and_project(m);
597 template <
typename D1,
typename D2,
typename R>
601 d1.concatenate_assign(y.
d1);
602 d2.concatenate_assign(y.
d2);
604 clear_reduced_flag();
608 template <
typename D1,
typename D2,
typename R>
612 d1.remove_space_dimensions(vars);
613 d2.remove_space_dimensions(vars);
616 template <
typename D1,
typename D2,
typename R>
620 d1.remove_higher_space_dimensions(new_dimension);
621 d2.remove_higher_space_dimensions(new_dimension);
624 template <
typename D1,
typename D2,
typename R>
625 template <
typename Partial_Function>
629 d1.map_space_dimensions(pfunc);
630 d2.map_space_dimensions(pfunc);
633 template <
typename D1,
typename D2,
typename R>
637 d1.expand_space_dimension(var, m);
638 d2.expand_space_dimension(var, m);
641 template <
typename D1,
typename D2,
typename R>
646 d1.fold_space_dimensions(vars, dest);
647 d2.fold_space_dimensions(vars, dest);
650 template <
typename D1,
typename D2,
typename R>
656 return d1.contains(y.
d1) && d2.contains(y.
d2);
659 template <
typename D1,
typename D2,
typename R>
665 return (d1.contains(y.
d1) && d2.strictly_contains(y.
d2))
666 || (d2.contains(y.
d2) && d1.strictly_contains(y.
d1));
669 template <
typename D1,
typename D2,
typename R>
678 r.product_reduce(dp.
d1, dp.
d2);
683 template <
typename D1,
typename D2,
typename R>
689 template <
typename D1,
typename D2,
typename R>
695 template <
typename D1,
typename D2,
typename R>
703 template <typename D1, typename D2, typename R>
706 const char yes =
'+';
708 s <<
"Partially_Reduced_Product\n";
709 s << (reduced ? yes :
no) <<
"reduced\n";
716 template <
typename D1,
typename D2,
typename R>
723 template <
typename D1,
typename D2,
typename R>
729 return x.
d1 == y.
d1 && x.
d2 == y.
d2;
733 template <
typename D1,
typename D2,
typename R>
741 template <
typename D1,
typename D2,
typename R>
745 return s <<
"Domain 1:\n"
755 template <
typename D1,
typename D2>
760 template <
typename D1,
typename D2>
764 template <
typename D1,
typename D2>
769 template <
typename D1,
typename D2>
774 template <
typename D1,
typename D2>
779 template <
typename D1,
typename D2>
784 template <
typename D1,
typename D2>
789 template <
typename D1,
typename D2>
794 template <
typename D1,
typename D2>
799 template <
typename D1,
typename D2>
804 template <
typename D1,
typename D2>
810 template <
typename D1,
typename D2,
typename R>
819 #endif // !defined(PPL_Partially_Reduced_Product_inlines_hh)
dimension_type affine_dimension() const
Returns the minimum affine dimension (see also grid affine dimension) of the components of *this...
void expand_space_dimension(Variable var, dimension_type m)
Creates m copies of the space dimension corresponding to var.
void upper_bound_assign(const Partially_Reduced_Product &y)
Assigns to *this an upper bound of *this and y computed on the corresponding components.
Constraints_Reduction()
Default constructor.
bool is_disjoint_from(const Partially_Reduced_Product &y) const
Returns true if and only if *this and y are componentwise disjoint.
bool operator!=(const Partially_Reduced_Product< D1, D2, R > &x, const Partially_Reduced_Product< D1, D2, R > &y)
The partially reduced product of two abstractions.
dimension_type max_space_dimension()
Returns the maximum space dimension this library can handle.
memory_size_type total_memory_in_bytes() const
Returns the total size in bytes of the memory occupied by *this.
void refine_with_constraint(const Constraint &c)
Use the constraint c to refine *this.
A linear equality or inequality.
void topological_closure_assign()
Assigns to *this its topological closure.
void swap(CO_Tree &x, CO_Tree &y)
dimension_type space_dimension() const
Returns the dimension of the vector space enclosing *this.
void swap(Partially_Reduced_Product< D1, D2, R > &x, Partially_Reduced_Product< D1, D2, R > &y)
size_t dimension_type
An unsigned integral type for representing space dimensions.
memory_size_type external_memory_in_bytes() const
Returns the size in bytes of the memory managed by *this.
An std::set of variables' indexes.
~No_Reduction()
Destructor.
Enable_If< Is_Native_Or_Checked< T >::value, void >::type ascii_dump(std::ostream &s, const T &t)
void clear_reduced_flag() const
Clears the reduced flag.
std::ostream & operator<<(std::ostream &s, const Ask_Tell< D > &x)
void refine_with_congruence(const Congruence &cg)
Use the congruence cg to refine *this.
void drop_some_non_integer_points(Complexity_Class complexity=ANY_COMPLEXITY)
Possibly tightens *this by dropping some points with non-integer coordinates.
void product_reduce(D1 &d1, D2 &d2)
The null reduction operator.
bool bounds_from_below(const Linear_Expression &expr) const
Returns true if and only if expr is bounded in *this.
The standard C++ namespace.
bool is_reduced() const
Return true if and only if the reduced flag is set.
void refine_with_congruences(const Congruence_System &cgs)
Use the congruences in cgs to refine *this.
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 ...
void unconstrain(Variable var)
Computes the cylindrification of *this with respect to space dimension var, assigning the result to *...
void add_congruences(const Congruence_System &cgs)
Adds a copy of the congruences in cgs to *this.
void time_elapse_assign(const Partially_Reduced_Product &y)
Assigns to *this the result of computing the time-elapse between *this and y. (See also time-elapse...
bool is_discrete() const
Returns true if and only if a component of *this is discrete.
void bounded_affine_image(Variable var, const Linear_Expression &lb_expr, const Linear_Expression &ub_expr, Coefficient_traits::const_reference denominator=Coefficient_one())
Assigns to *this the image of *this with respect to the bounded affine relation . ...
void generalized_affine_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 ...
Partially_Reduced_Product & operator=(const Partially_Reduced_Product &y)
The assignment operator. (*this and y can be dimension-incompatible.)
void remove_space_dimensions(const Variables_Set &vars)
Removes all the specified dimensions from the vector space.
void add_constraint(const Constraint &c)
Adds constraint c to *this.
void refine_with_constraints(const Constraint_System &cs)
Use the constraints in cs to refine *this.
A dimension of the vector space.
bool is_bounded() const
Returns true if and only if a component of *this is bounded.
void remove_higher_space_dimensions(dimension_type new_dimension)
Removes the higher dimensions of the vector space so that the resulting space will have dimension new...
Complexity_Class
Complexity pseudo-classes.
bool constrains(Variable var) const
Returns true if and only if var is constrained in *this.
D2 d2
The second component.
Smash_Reduction()
Default constructor.
void add_space_dimensions_and_embed(dimension_type m)
Adds m new space dimensions and embeds the components of *this in the new vector space.
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 ...
Relation_Symbol
Relation symbols.
Degenerate_Element
Kinds of degenerate abstract elements.
void add_constraints(const Constraint_System &cs)
Adds a copy of the constraint system in cs to *this.
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 expre...
Partially_Reduced_Product(dimension_type num_dimensions=0, Degenerate_Element kind=UNIVERSE)
Builds an object having the specified properties.
Shape_Preserving_Reduction()
Default constructor.
int32_t hash_code() const
Returns a 32-bit hash code for *this.
Enable_If< Is_Native< T >::value, memory_size_type >::type external_memory_in_bytes(const T &)
For native types, returns the size in bytes of the memory managed by the type of the (unused) paramet...
bool upper_bound_assign_if_exact(const Partially_Reduced_Product &y)
Assigns to *this an upper bound of *this and y computed on the corresponding components. If it is exact on each of the components of *this, true is returned, otherwise false is returned.
void add_space_dimensions_and_project(dimension_type m)
Adds m new space dimensions and does not embed the components in the new vector space.
A not necessarily closed convex polyhedron.
bool contains(const Partially_Reduced_Product &y) const
Returns true if and only if each component of *this contains the corresponding component of y...
~Smash_Reduction()
Destructor.
A not necessarily closed, iso-oriented hyperrectangle.
A closed convex polyhedron.
int32_t hash_code_from_dimension(dimension_type dim)
Returns the hash code for space dimension dim.
~Partially_Reduced_Product()
Destructor.
void difference_assign(const Partially_Reduced_Product &y)
Assigns to *this an approximation of the set-theoretic difference of *this and y. ...
~Congruences_Reduction()
Destructor.
Congruences_Reduction()
Default constructor.
No_Reduction()
Default constructor.
void concatenate_assign(const Partially_Reduced_Product &y)
Assigns to the first (resp., second) component of *this the "concatenation" of the first (resp...
~Shape_Preserving_Reduction()
Destructor.
void fold_space_dimensions(const Variables_Set &vars, Variable dest)
Folds the space dimensions in vars into dest.
bool bounds_from_above(const Linear_Expression &expr) const
Returns true if and only if expr is bounded in *this.
The entire library is confined to this namespace.
const D2 & domain2() const
Returns a constant reference to the second of the pair.
~Constraints_Reduction()
Destructor.
D1 d1
The first component.
A bounded difference shape.
void add_congruence(const Congruence &cg)
Adds a copy of congruence cg to *this.
bool is_universe() const
Returns true if and only if both of the components of *this are the universe.
bool is_empty() const
Returns true if and only if either of the components of *this are empty.
bool reduce() const
Reduce.
void m_swap(Partially_Reduced_Product &y)
Swaps *this with product y. (*this and y can be dimension-incompatible.)
void map_space_dimensions(const Partial_Function &pfunc)
Remaps the dimensions of the vector space according to a partial function.
void set_reduced_flag() const
Sets the reduced flag.
size_t memory_size_type
An unsigned integral type for representing memory size in bytes.
bool reduced
Flag to record whether the components are reduced with respect to each other and the reduction class...
static dimension_type max_space_dimension()
Returns the maximum space dimension this product can handle.
void widening_assign(const Partially_Reduced_Product &y, unsigned *tp=NULL)
Assigns to *this the result of computing the "widening" between *this and y.
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 e...
bool is_topologically_closed() const
Returns true if and only if both of the components of *this are topologically closed subsets of the v...
void intersection_assign(const Partially_Reduced_Product &y)
Assigns to *this the componentwise intersection of *this and y.
bool strictly_contains(const Partially_Reduced_Product &y) const
Returns true if and only if each component of *this strictly contains the corresponding component of ...
#define PPL_OUTPUT_3_PARAM_TEMPLATE_DEFINITIONS(type_symbol1, type_symbol2, type_symbol3, class_prefix)
bool operator==(const Partially_Reduced_Product< D1, D2, R > &x, const Partially_Reduced_Product< D1, D2, R > &y)
const D1 & domain1() const
Returns a constant reference to the first of the pair.