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 
27 #include "Constraint_System_defs.hh"
28 #include "Congruence_System_defs.hh"
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
max_space_dimension()37 Partially_Reduced_Product<D1, D2, R>::max_space_dimension() {
38   return (D1::max_space_dimension() < D2::max_space_dimension())
39     ? D1::max_space_dimension()
40     : D2::max_space_dimension();
41 }
42 
43 template <typename D1, typename D2, typename R>
44 inline
45 Partially_Reduced_Product<D1, D2, R>
Partially_Reduced_Product(dimension_type num_dimensions,const Degenerate_Element kind)46 ::Partially_Reduced_Product(dimension_type num_dimensions,
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
61 Partially_Reduced_Product<D1, D2, R>
Partially_Reduced_Product(const Congruence_System & cgs)62 ::Partially_Reduced_Product(const Congruence_System& cgs)
63   : d1(cgs), d2(cgs) {
64   clear_reduced_flag();
65 }
66 
67 template <typename D1, typename D2, typename R>
68 inline
69 Partially_Reduced_Product<D1, D2, R>
Partially_Reduced_Product(Congruence_System & cgs)70 ::Partially_Reduced_Product(Congruence_System& cgs)
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
77 Partially_Reduced_Product<D1, D2, R>
Partially_Reduced_Product(const Constraint_System & cs)78 ::Partially_Reduced_Product(const Constraint_System& cs)
79   : d1(cs), d2(cs) {
80   clear_reduced_flag();
81 }
82 
83 template <typename D1, typename D2, typename R>
84 inline
85 Partially_Reduced_Product<D1, D2, R>
Partially_Reduced_Product(Constraint_System & cs)86 ::Partially_Reduced_Product(Constraint_System& cs)
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
93 Partially_Reduced_Product<D1, D2, R>
Partially_Reduced_Product(const C_Polyhedron & ph,Complexity_Class complexity)94 ::Partially_Reduced_Product(const C_Polyhedron& ph,
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
102 Partially_Reduced_Product<D1, D2, R>
Partially_Reduced_Product(const NNC_Polyhedron & ph,Complexity_Class complexity)103 ::Partially_Reduced_Product(const NNC_Polyhedron& ph,
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
111 Partially_Reduced_Product<D1, D2, R>
Partially_Reduced_Product(const Grid & gr,Complexity_Class)112 ::Partially_Reduced_Product(const Grid& gr, Complexity_Class)
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
120 Partially_Reduced_Product<D1, D2, R>
Partially_Reduced_Product(const Box<Interval> & box,Complexity_Class)121 ::Partially_Reduced_Product(const Box<Interval>& box, Complexity_Class)
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
129 Partially_Reduced_Product<D1, D2, R>
Partially_Reduced_Product(const BD_Shape<U> & bd,Complexity_Class)130 ::Partially_Reduced_Product(const BD_Shape<U>& bd, Complexity_Class)
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
138 Partially_Reduced_Product<D1, D2, R>
Partially_Reduced_Product(const Octagonal_Shape<U> & os,Complexity_Class)139 ::Partially_Reduced_Product(const Octagonal_Shape<U>& os, Complexity_Class)
140   : d1(os), d2(os) {
141   set_reduced_flag();
142 }
143 
144 template <typename D1, typename D2, typename R>
145 inline
146 Partially_Reduced_Product<D1, D2, R>
Partially_Reduced_Product(const Partially_Reduced_Product & y,Complexity_Class)147 ::Partially_Reduced_Product(const Partially_Reduced_Product& y,
148                             Complexity_Class)
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
156 Partially_Reduced_Product<D1, D2, R>
Partially_Reduced_Product(const Partially_Reduced_Product<E1,E2,S> & y,Complexity_Class complexity)157 ::Partially_Reduced_Product(const Partially_Reduced_Product<E1, E2, S>& y,
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
~Partially_Reduced_Product()168 Partially_Reduced_Product<D1, D2, R>::~Partially_Reduced_Product() {
169 }
170 
171 template <typename D1, typename D2, typename R>
172 inline memory_size_type
external_memory_in_bytes() const173 Partially_Reduced_Product<D1, D2, R>::external_memory_in_bytes() const {
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
total_memory_in_bytes() const179 Partially_Reduced_Product<D1, D2, R>::total_memory_in_bytes() const {
180   return sizeof(*this) + external_memory_in_bytes();
181 }
182 
183 template <typename D1, typename D2, typename R>
184 inline dimension_type
space_dimension() const185 Partially_Reduced_Product<D1, D2, R>::space_dimension() const {
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
affine_dimension() const192 Partially_Reduced_Product<D1, D2, R>::affine_dimension() const {
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
201 Partially_Reduced_Product<D1, D2, R>
unconstrain(const Variable var)202 ::unconstrain(const Variable var) {
203   reduce();
204   d1.unconstrain(var);
205   d2.unconstrain(var);
206 }
207 
208 template <typename D1, typename D2, typename R>
209 inline void
unconstrain(const Variables_Set & vars)210 Partially_Reduced_Product<D1, D2, R>::unconstrain(const Variables_Set& vars) {
211   reduce();
212   d1.unconstrain(vars);
213   d2.unconstrain(vars);
214 }
215 
216 template <typename D1, typename D2, typename R>
217 inline void
218 Partially_Reduced_Product<D1, D2, R>
intersection_assign(const Partially_Reduced_Product & y)219 ::intersection_assign(const Partially_Reduced_Product& y) {
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
227 Partially_Reduced_Product<D1, D2, R>
difference_assign(const Partially_Reduced_Product & y)228 ::difference_assign(const Partially_Reduced_Product& y) {
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
238 Partially_Reduced_Product<D1, D2, R>
upper_bound_assign(const Partially_Reduced_Product & y)239 ::upper_bound_assign(const Partially_Reduced_Product& y) {
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
248 Partially_Reduced_Product<D1, D2, R>
upper_bound_assign_if_exact(const Partially_Reduced_Product & y)249 ::upper_bound_assign_if_exact(const Partially_Reduced_Product& y) {
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
268 Partially_Reduced_Product<D1, D2, R>
affine_image(Variable var,const Linear_Expression & expr,Coefficient_traits::const_reference denominator)269 ::affine_image(Variable var,
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
279 Partially_Reduced_Product<D1, D2, R>
affine_preimage(Variable var,const Linear_Expression & expr,Coefficient_traits::const_reference denominator)280 ::affine_preimage(Variable var,
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
290 Partially_Reduced_Product<D1, D2, R>
generalized_affine_image(Variable var,const Relation_Symbol relsym,const Linear_Expression & expr,Coefficient_traits::const_reference denominator)291 ::generalized_affine_image(Variable var,
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
302 Partially_Reduced_Product<D1, D2, R>
generalized_affine_preimage(Variable var,const Relation_Symbol relsym,const Linear_Expression & expr,Coefficient_traits::const_reference denominator)303 ::generalized_affine_preimage(Variable var,
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
314 Partially_Reduced_Product<D1, D2, R>
generalized_affine_image(const Linear_Expression & lhs,const Relation_Symbol relsym,const Linear_Expression & rhs)315 ::generalized_affine_image(const Linear_Expression& lhs,
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
325 Partially_Reduced_Product<D1, D2, R>
generalized_affine_preimage(const Linear_Expression & lhs,const Relation_Symbol relsym,const Linear_Expression & rhs)326 ::generalized_affine_preimage(const Linear_Expression& lhs,
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
337 Partially_Reduced_Product<D1, D2, R>
bounded_affine_image(Variable var,const Linear_Expression & lb_expr,const Linear_Expression & ub_expr,Coefficient_traits::const_reference denominator)338 ::bounded_affine_image(Variable var,
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
349 Partially_Reduced_Product<D1, D2, R>
bounded_affine_preimage(Variable var,const Linear_Expression & lb_expr,const Linear_Expression & ub_expr,Coefficient_traits::const_reference denominator)350 ::bounded_affine_preimage(Variable var,
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
361 Partially_Reduced_Product<D1, D2, R>
time_elapse_assign(const Partially_Reduced_Product & y)362 ::time_elapse_assign(const Partially_Reduced_Product& y) {
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
topological_closure_assign()372 Partially_Reduced_Product<D1, D2, R>::topological_closure_assign() {
373   d1.topological_closure_assign();
374   d2.topological_closure_assign();
375 }
376 
377 template <typename D1, typename D2, typename R>
378 inline void
m_swap(Partially_Reduced_Product & y)379 Partially_Reduced_Product<D1, D2, R>::m_swap(Partially_Reduced_Product& y) {
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
add_constraint(const Constraint & c)388 Partially_Reduced_Product<D1, D2, R>::add_constraint(const Constraint& c) {
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
refine_with_constraint(const Constraint & c)396 Partially_Reduced_Product<D1, D2, R>::refine_with_constraint(const Constraint& c) {
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
add_congruence(const Congruence & cg)404 Partially_Reduced_Product<D1, D2, R>::add_congruence(const Congruence& cg) {
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
refine_with_congruence(const Congruence & cg)412 Partially_Reduced_Product<D1, D2, R>::refine_with_congruence(const Congruence& cg) {
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
420 Partially_Reduced_Product<D1, D2, R>
add_constraints(const Constraint_System & cs)421 ::add_constraints(const Constraint_System& cs) {
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
429 Partially_Reduced_Product<D1, D2, R>
refine_with_constraints(const Constraint_System & cs)430 ::refine_with_constraints(const Constraint_System& cs) {
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
438 Partially_Reduced_Product<D1, D2, R>
add_congruences(const Congruence_System & cgs)439 ::add_congruences(const Congruence_System& cgs) {
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
447 Partially_Reduced_Product<D1, D2, R>
refine_with_congruences(const Congruence_System & cgs)448 ::refine_with_congruences(const Congruence_System& cgs) {
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
456 Partially_Reduced_Product<D1, D2, R>
drop_some_non_integer_points(Complexity_Class complexity)457 ::drop_some_non_integer_points(Complexity_Class complexity) {
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
466 Partially_Reduced_Product<D1, D2, R>
drop_some_non_integer_points(const Variables_Set & vars,Complexity_Class complexity)467 ::drop_some_non_integer_points(const Variables_Set& vars,
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>
476 inline Partially_Reduced_Product<D1, D2, R>&
477 Partially_Reduced_Product<D1, D2, R>
operator =(const Partially_Reduced_Product & y)478 ::operator=(const Partially_Reduced_Product& y) {
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&
domain1() const487 Partially_Reduced_Product<D1, D2, R>::domain1() const {
488   reduce();
489   return d1;
490 }
491 
492 template <typename D1, typename D2, typename R>
493 inline const D2&
domain2() const494 Partially_Reduced_Product<D1, D2, R>::domain2() const {
495   reduce();
496   return d2;
497 }
498 
499 template <typename D1, typename D2, typename R>
500 inline bool
is_empty() const501 Partially_Reduced_Product<D1, D2, R>::is_empty() const {
502   reduce();
503   return d1.is_empty() || d2.is_empty();
504 }
505 
506 template <typename D1, typename D2, typename R>
507 inline bool
is_universe() const508 Partially_Reduced_Product<D1, D2, R>::is_universe() const {
509   return d1.is_universe() && d2.is_universe();
510 }
511 
512 template <typename D1, typename D2, typename R>
513 inline bool
is_topologically_closed() const514 Partially_Reduced_Product<D1, D2, R>::is_topologically_closed() const {
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
521 Partially_Reduced_Product<D1, D2, R>
is_disjoint_from(const Partially_Reduced_Product & y) const522 ::is_disjoint_from(const Partially_Reduced_Product& y) const {
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
is_discrete() const530 Partially_Reduced_Product<D1, D2, R>::is_discrete() const {
531   reduce();
532   return d1.is_discrete() || d2.is_discrete();
533 }
534 
535 template <typename D1, typename D2, typename R>
536 inline bool
is_bounded() const537 Partially_Reduced_Product<D1, D2, R>::is_bounded() const {
538   reduce();
539   return d1.is_bounded() || d2.is_bounded();
540 }
541 
542 template <typename D1, typename D2, typename R>
543 inline bool
544 Partially_Reduced_Product<D1, D2, R>
bounds_from_above(const Linear_Expression & expr) const545 ::bounds_from_above(const Linear_Expression& expr) const {
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
552 Partially_Reduced_Product<D1, D2, R>
bounds_from_below(const Linear_Expression & expr) const553 ::bounds_from_below(const Linear_Expression& expr) const {
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
constrains(Variable var) const560 Partially_Reduced_Product<D1, D2, R>::constrains(Variable var) const {
561   reduce();
562   return d1.constrains(var) || d2.constrains(var);
563 }
564 
565 template <typename D1, typename D2, typename R>
566 inline void
567 Partially_Reduced_Product<D1, D2, R>
widening_assign(const Partially_Reduced_Product & y,unsigned * tp)568 ::widening_assign(const Partially_Reduced_Product& y,
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
583 Partially_Reduced_Product<D1, D2, R>
add_space_dimensions_and_embed(dimension_type m)584 ::add_space_dimensions_and_embed(dimension_type m) {
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
591 Partially_Reduced_Product<D1, D2, R>
add_space_dimensions_and_project(dimension_type m)592 ::add_space_dimensions_and_project(dimension_type m) {
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
599 Partially_Reduced_Product<D1, D2, R>
concatenate_assign(const Partially_Reduced_Product & y)600 ::concatenate_assign(const Partially_Reduced_Product& y) {
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
610 Partially_Reduced_Product<D1, D2, R>
remove_space_dimensions(const Variables_Set & vars)611 ::remove_space_dimensions(const Variables_Set& vars) {
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
618 Partially_Reduced_Product<D1, D2, R>
remove_higher_space_dimensions(dimension_type new_dimension)619 ::remove_higher_space_dimensions(dimension_type new_dimension) {
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
627 Partially_Reduced_Product<D1, D2, R>
map_space_dimensions(const Partial_Function & pfunc)628 ::map_space_dimensions(const Partial_Function& pfunc) {
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
635 Partially_Reduced_Product<D1, D2, R>
expand_space_dimension(Variable var,dimension_type m)636 ::expand_space_dimension(Variable var, dimension_type m) {
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
643 Partially_Reduced_Product<D1, D2, R>
fold_space_dimensions(const Variables_Set & vars,Variable dest)644 ::fold_space_dimensions(const Variables_Set& vars,
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
652 Partially_Reduced_Product<D1, D2, R>
contains(const Partially_Reduced_Product & y) const653 ::contains(const Partially_Reduced_Product& y) const {
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
661 Partially_Reduced_Product<D1, D2, R>
strictly_contains(const Partially_Reduced_Product & y) const662 ::strictly_contains(const Partially_Reduced_Product& y) const {
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
reduce() const671 Partially_Reduced_Product<D1, D2, R>::reduce() const {
672   Partially_Reduced_Product& dp
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
is_reduced() const685 Partially_Reduced_Product<D1, D2, R>::is_reduced() const {
686   return reduced;
687 }
688 
689 template <typename D1, typename D2, typename R>
690 inline void
clear_reduced_flag() const691 Partially_Reduced_Product<D1, D2, R>::clear_reduced_flag() const {
692   const_cast<Partially_Reduced_Product&>(*this).reduced = false;
693 }
694 
695 template <typename D1, typename D2, typename R>
696 inline void
set_reduced_flag() const697 Partially_Reduced_Product<D1, D2, R>::set_reduced_flag() const {
698   const_cast<Partially_Reduced_Product&>(*this).reduced = true;
699 }
700 
PPL_OUTPUT_3_PARAM_TEMPLATE_DEFINITIONS(D1,D2,R,Partially_Reduced_Product)701 PPL_OUTPUT_3_PARAM_TEMPLATE_DEFINITIONS(D1, D2, R, Partially_Reduced_Product)
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
hash_code() const718 Partially_Reduced_Product<D1, D2, R>::hash_code() const {
719   return hash_code_from_dimension(space_dimension());
720 }
721 
722 /*! \relates Parma_Polyhedra_Library::Partially_Reduced_Product */
723 template <typename D1, typename D2, typename R>
724 inline bool
operator ==(const Partially_Reduced_Product<D1,D2,R> & x,const Partially_Reduced_Product<D1,D2,R> & y)725 operator==(const Partially_Reduced_Product<D1, D2, R>& x,
726            const Partially_Reduced_Product<D1, D2, R>& y) {
727   x.reduce();
728   y.reduce();
729   return x.d1 == y.d1 && x.d2 == y.d2;
730 }
731 
732 /*! \relates Parma_Polyhedra_Library::Partially_Reduced_Product */
733 template <typename D1, typename D2, typename R>
734 inline bool
operator !=(const Partially_Reduced_Product<D1,D2,R> & x,const Partially_Reduced_Product<D1,D2,R> & y)735 operator!=(const Partially_Reduced_Product<D1, D2, R>& x,
736            const Partially_Reduced_Product<D1, D2, R>& y) {
737   return !(x == y);
738 }
739 
740 /*! \relates Parma_Polyhedra_Library::Partially_Reduced_Product */
741 template <typename D1, typename D2, typename R>
742 inline std::ostream&
operator <<(std::ostream & s,const Partially_Reduced_Product<D1,D2,R> & dp)743 IO_Operators::operator<<(std::ostream& s,
744                          const Partially_Reduced_Product<D1, D2, R>& dp) {
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
No_Reduction()757 No_Reduction<D1, D2>::No_Reduction() {
758 }
759 
760 template <typename D1, typename D2>
product_reduce(D1 &,D2 &)761 void No_Reduction<D1, D2>::product_reduce(D1&, D2&) {
762 }
763 
764 template <typename D1, typename D2>
765 inline
~No_Reduction()766 No_Reduction<D1, D2>::~No_Reduction() {
767 }
768 
769 template <typename D1, typename D2>
770 inline
Smash_Reduction()771 Smash_Reduction<D1, D2>::Smash_Reduction() {
772 }
773 
774 template <typename D1, typename D2>
775 inline
~Smash_Reduction()776 Smash_Reduction<D1, D2>::~Smash_Reduction() {
777 }
778 
779 template <typename D1, typename D2>
780 inline
Constraints_Reduction()781 Constraints_Reduction<D1, D2>::Constraints_Reduction() {
782 }
783 
784 template <typename D1, typename D2>
785 inline
~Constraints_Reduction()786 Constraints_Reduction<D1, D2>::~Constraints_Reduction() {
787 }
788 
789 template <typename D1, typename D2>
790 inline
Congruences_Reduction()791 Congruences_Reduction<D1, D2>::Congruences_Reduction() {
792 }
793 
794 template <typename D1, typename D2>
795 inline
~Congruences_Reduction()796 Congruences_Reduction<D1, D2>::~Congruences_Reduction() {
797 }
798 
799 template <typename D1, typename D2>
800 inline
Shape_Preserving_Reduction()801 Shape_Preserving_Reduction<D1, D2>::Shape_Preserving_Reduction() {
802 }
803 
804 template <typename D1, typename D2>
805 inline
~Shape_Preserving_Reduction()806 Shape_Preserving_Reduction<D1, D2>::~Shape_Preserving_Reduction() {
807 }
808 
809 /*! \relates Partially_Reduced_Product */
810 template <typename D1, typename D2, typename R>
811 inline void
swap(Partially_Reduced_Product<D1,D2,R> & x,Partially_Reduced_Product<D1,D2,R> & y)812 swap(Partially_Reduced_Product<D1, D2, R>& x,
813      Partially_Reduced_Product<D1, D2, R>& y) {
814   x.m_swap(y);
815 }
816 
817 } // namespace Parma_Polyhedra_Library
818 
819 #endif // !defined(PPL_Partially_Reduced_Product_inlines_hh)
820