PPL  1.2
Partially_Reduced_Product_inlines.hh
Go to the documentation of this file.
1 /* Partially_Reduced_Product class implementation: inline functions.
2  Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it>
3  Copyright (C) 2010-2016 BUGSENG srl (http://bugseng.com)
4 
5 This file is part of the Parma Polyhedra Library (PPL).
6 
7 The PPL is free software; you can redistribute it and/or modify it
8 under the terms of the GNU General Public License as published by the
9 Free Software Foundation; either version 3 of the License, or (at your
10 option) any later version.
11 
12 The PPL is distributed in the hope that it will be useful, but WITHOUT
13 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
14 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
15 for more details.
16 
17 You should have received a copy of the GNU General Public License
18 along with this program; if not, write to the Free Software Foundation,
19 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA.
20 
21 For the most up-to-date information see the Parma Polyhedra Library
22 site: http://bugseng.com/products/ppl/ . */
23 
24 #ifndef PPL_Partially_Reduced_Product_inlines_hh
25 #define PPL_Partially_Reduced_Product_inlines_hh 1
26 
29 #include "C_Polyhedron_defs.hh"
30 #include "NNC_Polyhedron_defs.hh"
31 #include "Grid_defs.hh"
32 
33 namespace Parma_Polyhedra_Library {
34 
35 template <typename D1, typename D2, typename R>
36 inline dimension_type
41 }
42 
43 template <typename D1, typename D2, typename R>
44 inline
47  const Degenerate_Element kind)
48  : d1(num_dimensions <= max_space_dimension()
49  ? num_dimensions
50  : (throw_space_dimension_overflow("Partially_Reduced_Product(n, k)",
51  "n exceeds the maximum "
52  "allowed space dimension"),
53  num_dimensions),
54  kind),
55  d2(num_dimensions, kind) {
56  set_reduced_flag();
57 }
58 
59 template <typename D1, typename D2, typename R>
60 inline
63  : d1(cgs), d2(cgs) {
64  clear_reduced_flag();
65 }
66 
67 template <typename D1, typename D2, typename R>
68 inline
71  : d1(const_cast<const Congruence_System&>(cgs)), d2(cgs) {
72  clear_reduced_flag();
73 }
74 
75 template <typename D1, typename D2, typename R>
76 inline
79  : d1(cs), d2(cs) {
80  clear_reduced_flag();
81 }
82 
83 template <typename D1, typename D2, typename R>
84 inline
87  : d1(const_cast<const Constraint_System&>(cs)), d2(cs) {
88  clear_reduced_flag();
89 }
90 
91 template <typename D1, typename D2, typename R>
92 inline
95  Complexity_Class complexity)
96  : d1(ph, complexity), d2(ph, complexity) {
97  set_reduced_flag();
98 }
99 
100 template <typename D1, typename D2, typename R>
101 inline
104  Complexity_Class complexity)
105  : d1(ph, complexity), d2(ph, complexity) {
106  set_reduced_flag();
107 }
108 
109 template <typename D1, typename D2, typename R>
110 inline
113  : d1(gr), d2(gr) {
114  set_reduced_flag();
115 }
116 
117 template <typename D1, typename D2, typename R>
118 template <typename Interval>
119 inline
122  : d1(box), d2(box) {
123  set_reduced_flag();
124 }
125 
126 template <typename D1, typename D2, typename R>
127 template <typename U>
128 inline
131  : d1(bd), d2(bd) {
132  set_reduced_flag();
133 }
134 
135 template <typename D1, typename D2, typename R>
136 template <typename U>
137 inline
140  : d1(os), d2(os) {
141  set_reduced_flag();
142 }
143 
144 template <typename D1, typename D2, typename R>
145 inline
149  : d1(y.d1), d2(y.d2) {
150  reduced = y.reduced;
151 }
152 
153 template <typename D1, typename D2, typename R>
154 template <typename E1, typename E2, typename S>
155 inline
158  Complexity_Class complexity)
159  : d1(y.space_dimension()), d2(y.space_dimension()), reduced(false) {
160  Partially_Reduced_Product<D1, D2, R> pg1(y.domain1(), complexity);
161  Partially_Reduced_Product<D1, D2, R> pg2(y.domain2(), complexity);
162  pg1.intersection_assign(pg2);
163  m_swap(pg1);
164 }
165 
166 template <typename D1, typename D2, typename R>
167 inline
169 }
170 
171 template <typename D1, typename D2, typename R>
172 inline memory_size_type
174  return d1.external_memory_in_bytes() + d2.external_memory_in_bytes();
175 }
176 
177 template <typename D1, typename D2, typename R>
178 inline memory_size_type
180  return sizeof(*this) + external_memory_in_bytes();
181 }
182 
183 template <typename D1, typename D2, typename R>
184 inline dimension_type
186  PPL_ASSERT(d1.space_dimension() == d2.space_dimension());
187  return d1.space_dimension();
188 }
189 
190 template <typename D1, typename D2, typename R>
191 inline dimension_type
193  reduce();
194  const dimension_type d1_dim = d1.affine_dimension();
195  const dimension_type d2_dim = d2.affine_dimension();
196  return std::min(d1_dim, d2_dim);
197 }
198 
199 template <typename D1, typename D2, typename R>
200 inline void
203  reduce();
204  d1.unconstrain(var);
205  d2.unconstrain(var);
206 }
207 
208 template <typename D1, typename D2, typename R>
209 inline void
211  reduce();
212  d1.unconstrain(vars);
213  d2.unconstrain(vars);
214 }
215 
216 template <typename D1, typename D2, typename R>
217 inline void
220  d1.intersection_assign(y.d1);
221  d2.intersection_assign(y.d2);
222  clear_reduced_flag();
223 }
224 
225 template <typename D1, typename D2, typename R>
226 inline void
229  reduce();
230  y.reduce();
231  d1.difference_assign(y.d1);
232  d2.difference_assign(y.d2);
233  clear_reduced_flag();
234 }
235 
236 template <typename D1, typename D2, typename R>
237 inline void
240  reduce();
241  y.reduce();
242  d1.upper_bound_assign(y.d1);
243  d2.upper_bound_assign(y.d2);
244 }
245 
246 template <typename D1, typename D2, typename R>
247 inline bool
250  reduce();
251  y.reduce();
252  D1 d1_copy = d1;
253  bool ub_exact = d1_copy.upper_bound_assign_if_exact(y.d1);
254  if (!ub_exact) {
255  return false;
256  }
257  ub_exact = d2.upper_bound_assign_if_exact(y.d2);
258  if (!ub_exact) {
259  return false;
260  }
261  using std::swap;
262  swap(d1, d1_copy);
263  return true;
264 }
265 
266 template <typename D1, typename D2, typename R>
267 inline void
270  const Linear_Expression& expr,
271  Coefficient_traits::const_reference denominator) {
272  d1.affine_image(var, expr, denominator);
273  d2.affine_image(var, expr, denominator);
274  clear_reduced_flag();
275 }
276 
277 template <typename D1, typename D2, typename R>
278 inline void
281  const Linear_Expression& expr,
282  Coefficient_traits::const_reference denominator) {
283  d1.affine_preimage(var, expr, denominator);
284  d2.affine_preimage(var, expr, denominator);
285  clear_reduced_flag();
286 }
287 
288 template <typename D1, typename D2, typename R>
289 inline void
292  const Relation_Symbol relsym,
293  const Linear_Expression& expr,
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();
298 }
299 
300 template <typename D1, typename D2, typename R>
301 inline void
304  const Relation_Symbol relsym,
305  const Linear_Expression& expr,
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();
310 }
311 
312 template <typename D1, typename D2, typename R>
313 inline void
316  const Relation_Symbol relsym,
317  const Linear_Expression& rhs) {
318  d1.generalized_affine_image(lhs, relsym, rhs);
319  d2.generalized_affine_image(lhs, relsym, rhs);
320  clear_reduced_flag();
321 }
322 
323 template <typename D1, typename D2, typename R>
324 inline void
327  const Relation_Symbol relsym,
328  const Linear_Expression& rhs) {
329  d1.generalized_affine_preimage(lhs, relsym, rhs);
330  d2.generalized_affine_preimage(lhs, relsym, rhs);
331  clear_reduced_flag();
332 }
333 
334 
335 template <typename D1, typename D2, typename R>
336 inline void
339  const Linear_Expression& lb_expr,
340  const Linear_Expression& ub_expr,
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();
345 }
346 
347 template <typename D1, typename D2, typename R>
348 inline void
351  const Linear_Expression& lb_expr,
352  const Linear_Expression& ub_expr,
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();
357 }
358 
359 template <typename D1, typename D2, typename R>
360 inline void
363  reduce();
364  y.reduce();
365  d1.time_elapse_assign(y.d1);
366  d2.time_elapse_assign(y.d2);
367  PPL_ASSERT_HEAVY(OK());
368 }
369 
370 template <typename D1, typename D2, typename R>
371 inline void
373  d1.topological_closure_assign();
374  d2.topological_closure_assign();
375 }
376 
377 template <typename D1, typename D2, typename R>
378 inline void
380  using std::swap;
381  swap(d1, y.d1);
382  swap(d2, y.d2);
383  swap(reduced, y.reduced);
384 }
385 
386 template <typename D1, typename D2, typename R>
387 inline void
389  d1.add_constraint(c);
390  d2.add_constraint(c);
391  clear_reduced_flag();
392 }
393 
394 template <typename D1, typename D2, typename R>
395 inline void
397  d1.refine_with_constraint(c);
398  d2.refine_with_constraint(c);
399  clear_reduced_flag();
400 }
401 
402 template <typename D1, typename D2, typename R>
403 inline void
405  d1.add_congruence(cg);
406  d2.add_congruence(cg);
407  clear_reduced_flag();
408 }
409 
410 template <typename D1, typename D2, typename R>
411 inline void
413  d1.refine_with_congruence(cg);
414  d2.refine_with_congruence(cg);
415  clear_reduced_flag();
416 }
417 
418 template <typename D1, typename D2, typename R>
419 inline void
422  d1.add_constraints(cs);
423  d2.add_constraints(cs);
424  clear_reduced_flag();
425 }
426 
427 template <typename D1, typename D2, typename R>
428 inline void
431  d1.refine_with_constraints(cs);
432  d2.refine_with_constraints(cs);
433  clear_reduced_flag();
434 }
435 
436 template <typename D1, typename D2, typename R>
437 inline void
440  d1.add_congruences(cgs);
441  d2.add_congruences(cgs);
442  clear_reduced_flag();
443 }
444 
445 template <typename D1, typename D2, typename R>
446 inline void
449  d1.refine_with_congruences(cgs);
450  d2.refine_with_congruences(cgs);
451  clear_reduced_flag();
452 }
453 
454 template <typename D1, typename D2, typename R>
455 inline void
458  reduce();
459  d1.drop_some_non_integer_points(complexity);
460  d2.drop_some_non_integer_points(complexity);
461  clear_reduced_flag();
462 }
463 
464 template <typename D1, typename D2, typename R>
465 inline void
468  Complexity_Class complexity) {
469  reduce();
470  d1.drop_some_non_integer_points(vars, complexity);
471  d2.drop_some_non_integer_points(vars, complexity);
472  clear_reduced_flag();
473 }
474 
475 template <typename D1, typename D2, typename R>
479  d1 = y.d1;
480  d2 = y.d2;
481  reduced = y.reduced;
482  return *this;
483 }
484 
485 template <typename D1, typename D2, typename R>
486 inline const D1&
488  reduce();
489  return d1;
490 }
491 
492 template <typename D1, typename D2, typename R>
493 inline const D2&
495  reduce();
496  return d2;
497 }
498 
499 template <typename D1, typename D2, typename R>
500 inline bool
502  reduce();
503  return d1.is_empty() || d2.is_empty();
504 }
505 
506 template <typename D1, typename D2, typename R>
507 inline bool
509  return d1.is_universe() && d2.is_universe();
510 }
511 
512 template <typename D1, typename D2, typename R>
513 inline bool
515  reduce();
516  return d1.is_topologically_closed() && d2.is_topologically_closed();
517 }
518 
519 template <typename D1, typename D2, typename R>
520 inline bool
523  reduce();
524  y.reduce();
525  return d1.is_disjoint_from(y.d1) || d2.is_disjoint_from(y.d2);
526 }
527 
528 template <typename D1, typename D2, typename R>
529 inline bool
531  reduce();
532  return d1.is_discrete() || d2.is_discrete();
533 }
534 
535 template <typename D1, typename D2, typename R>
536 inline bool
538  reduce();
539  return d1.is_bounded() || d2.is_bounded();
540 }
541 
542 template <typename D1, typename D2, typename R>
543 inline bool
546  reduce();
547  return d1.bounds_from_above(expr) || d2.bounds_from_above(expr);
548 }
549 
550 template <typename D1, typename D2, typename R>
551 inline bool
554  reduce();
555  return d1.bounds_from_below(expr) || d2.bounds_from_below(expr);
556 }
557 
558 template <typename D1, typename D2, typename R>
559 inline bool
561  reduce();
562  return d1.constrains(var) || d2.constrains(var);
563 }
564 
565 template <typename D1, typename D2, typename R>
566 inline void
569  unsigned* tp) {
570  // FIXME(0.10.1): In general this is _NOT_ a widening since the reduction
571  // may mean that the sequence does not satisfy the ascending
572  // chain condition.
573  // However, for the direct, smash and constraints product
574  // it may be ok - but this still needs checking.
575  reduce();
576  y.reduce();
577  d1.widening_assign(y.d1, tp);
578  d2.widening_assign(y.d2, tp);
579 }
580 
581 template <typename D1, typename D2, typename R>
582 inline void
585  d1.add_space_dimensions_and_embed(m);
586  d2.add_space_dimensions_and_embed(m);
587 }
588 
589 template <typename D1, typename D2, typename R>
590 inline void
593  d1.add_space_dimensions_and_project(m);
594  d2.add_space_dimensions_and_project(m);
595 }
596 
597 template <typename D1, typename D2, typename R>
598 inline void
601  d1.concatenate_assign(y.d1);
602  d2.concatenate_assign(y.d2);
603  if (!is_reduced() || !y.is_reduced()) {
604  clear_reduced_flag();
605  }
606 }
607 
608 template <typename D1, typename D2, typename R>
609 inline void
612  d1.remove_space_dimensions(vars);
613  d2.remove_space_dimensions(vars);
614 }
615 
616 template <typename D1, typename D2, typename R>
617 inline void
620  d1.remove_higher_space_dimensions(new_dimension);
621  d2.remove_higher_space_dimensions(new_dimension);
622 }
623 
624 template <typename D1, typename D2, typename R>
625 template <typename Partial_Function>
626 inline void
629  d1.map_space_dimensions(pfunc);
630  d2.map_space_dimensions(pfunc);
631 }
632 
633 template <typename D1, typename D2, typename R>
634 inline void
637  d1.expand_space_dimension(var, m);
638  d2.expand_space_dimension(var, m);
639 }
640 
641 template <typename D1, typename D2, typename R>
642 inline void
645  Variable dest) {
646  d1.fold_space_dimensions(vars, dest);
647  d2.fold_space_dimensions(vars, dest);
648 }
649 
650 template <typename D1, typename D2, typename R>
651 inline bool
654  reduce();
655  y.reduce();
656  return d1.contains(y.d1) && d2.contains(y.d2);
657 }
658 
659 template <typename D1, typename D2, typename R>
660 inline bool
663  reduce();
664  y.reduce();
665  return (d1.contains(y.d1) && d2.strictly_contains(y.d2))
666  || (d2.contains(y.d2) && d1.strictly_contains(y.d1));
667 }
668 
669 template <typename D1, typename D2, typename R>
670 inline bool
673  = const_cast<Partially_Reduced_Product&>(*this);
674  if (dp.is_reduced()) {
675  return false;
676  }
677  R r;
678  r.product_reduce(dp.d1, dp.d2);
679  set_reduced_flag();
680  return true;
681 }
682 
683 template <typename D1, typename D2, typename R>
684 inline bool
686  return reduced;
687 }
688 
689 template <typename D1, typename D2, typename R>
690 inline void
692  const_cast<Partially_Reduced_Product&>(*this).reduced = false;
693 }
694 
695 template <typename D1, typename D2, typename R>
696 inline void
698  const_cast<Partially_Reduced_Product&>(*this).reduced = true;
699 }
700 
702 
703 template <typename D1, typename D2, typename R>
704 inline void
705 Partially_Reduced_Product<D1, D2, R>::ascii_dump(std::ostream& s) const {
706  const char yes = '+';
707  const char no = '-';
708  s << "Partially_Reduced_Product\n";
709  s << (reduced ? yes : no) << "reduced\n";
710  s << "Domain 1:\n";
711  d1.ascii_dump(s);
712  s << "Domain 2:\n";
713  d2.ascii_dump(s);
714 }
715 
716 template <typename D1, typename D2, typename R>
717 inline int32_t
719  return hash_code_from_dimension(space_dimension());
720 }
721 
723 template <typename D1, typename D2, typename R>
724 inline bool
727  x.reduce();
728  y.reduce();
729  return x.d1 == y.d1 && x.d2 == y.d2;
730 }
731 
733 template <typename D1, typename D2, typename R>
734 inline bool
737  return !(x == y);
738 }
739 
741 template <typename D1, typename D2, typename R>
742 inline std::ostream&
743 IO_Operators::operator<<(std::ostream& s,
745  return s << "Domain 1:\n"
746  << dp.d1
747  << "Domain 2:\n"
748  << dp.d2;
749 }
750 
751 } // namespace Parma_Polyhedra_Library
752 
753 namespace Parma_Polyhedra_Library {
754 
755 template <typename D1, typename D2>
756 inline
758 }
759 
760 template <typename D1, typename D2>
762 }
763 
764 template <typename D1, typename D2>
765 inline
767 }
768 
769 template <typename D1, typename D2>
770 inline
772 }
773 
774 template <typename D1, typename D2>
775 inline
777 }
778 
779 template <typename D1, typename D2>
780 inline
782 }
783 
784 template <typename D1, typename D2>
785 inline
787 }
788 
789 template <typename D1, typename D2>
790 inline
792 }
793 
794 template <typename D1, typename D2>
795 inline
797 }
798 
799 template <typename D1, typename D2>
800 inline
802 }
803 
804 template <typename D1, typename D2>
805 inline
807 }
808 
810 template <typename D1, typename D2, typename R>
811 inline void
814  x.m_swap(y);
815 }
816 
817 } // namespace Parma_Polyhedra_Library
818 
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.
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.
Enable_If< Is_Native_Or_Checked< T >::value, void >::type ascii_dump(std::ostream &s, const T &t)
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.
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.
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...
A not necessarily closed, iso-oriented hyperrectangle.
Definition: Box_defs.hh:299
A closed convex polyhedron.
int32_t hash_code_from_dimension(dimension_type dim)
Returns the hash code for space dimension dim.
void difference_assign(const Partially_Reduced_Product &y)
Assigns to *this an approximation of the set-theoretic difference of *this and y. ...
void concatenate_assign(const Partially_Reduced_Product &y)
Assigns to the first (resp., second) component of *this the "concatenation" of the first (resp...
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.
Definition: version.hh:61
const D2 & domain2() const
Returns a constant reference to the second of the pair.
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.
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.
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...
Coefficient c
Definition: PIP_Tree.cc:64
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.