1 /* Polyhedron class implementation: non-inline template 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_Polyhedron_templates_hh
25 #define PPL_Polyhedron_templates_hh 1
26
27 #include "Generator_defs.hh"
28 #include "MIP_Problem_defs.hh"
29 #include "Interval_defs.hh"
30 #include "Linear_Form_defs.hh"
31 // For static method overflows.
32 #include "Floating_Point_Expression_defs.hh"
33 #include <algorithm>
34 #include <deque>
35
36 namespace Parma_Polyhedra_Library {
37
38 template <typename Interval>
Polyhedron(Topology topol,const Box<Interval> & box,Complexity_Class)39 Polyhedron::Polyhedron(Topology topol,
40 const Box<Interval>& box,
41 Complexity_Class)
42 : con_sys(topol, default_con_sys_repr),
43 gen_sys(topol, default_gen_sys_repr),
44 sat_c(),
45 sat_g() {
46 // Initialize the space dimension as indicated by the box.
47 space_dim = box.space_dimension();
48
49 // Check for emptiness.
50 if (box.is_empty()) {
51 set_empty();
52 return;
53 }
54
55 // Zero-dim universe polyhedron.
56 if (space_dim == 0) {
57 set_zero_dim_univ();
58 return;
59 }
60
61 // Properly set the space dimension of `con_sys'.
62 con_sys.set_space_dimension(space_dim);
63
64 PPL_DIRTY_TEMP_COEFFICIENT(l_n);
65 PPL_DIRTY_TEMP_COEFFICIENT(l_d);
66 PPL_DIRTY_TEMP_COEFFICIENT(u_n);
67 PPL_DIRTY_TEMP_COEFFICIENT(u_d);
68
69 if (topol == NECESSARILY_CLOSED) {
70 for (dimension_type k = space_dim; k-- > 0; ) {
71 const Variable v_k = Variable(k);
72 // See if we have a valid lower bound.
73 bool l_closed = false;
74 bool l_bounded = box.has_lower_bound(v_k, l_n, l_d, l_closed);
75 // See if we have a valid upper bound.
76 bool u_closed = false;
77 bool u_bounded = box.has_upper_bound(v_k, u_n, u_d, u_closed);
78
79 // See if we have an implicit equality constraint.
80 if (l_bounded && u_bounded
81 && l_closed && u_closed
82 && l_n == u_n && l_d == u_d) {
83 // Add the constraint `l_d*v_k == l_n'.
84 con_sys.insert(l_d * v_k == l_n);
85 }
86 else {
87 if (l_bounded) {
88 // Add the constraint `l_d*v_k >= l_n'.
89 con_sys.insert(l_d * v_k >= l_n);
90 }
91 if (u_bounded) {
92 // Add the constraint `u_d*v_k <= u_n'.
93 con_sys.insert(u_d * v_k <= u_n);
94 }
95 }
96 }
97 }
98 else {
99 // topol == NOT_NECESSARILY_CLOSED
100 for (dimension_type k = space_dim; k-- > 0; ) {
101 const Variable v_k = Variable(k);
102 // See if we have a valid lower bound.
103 bool l_closed = false;
104 bool l_bounded = box.has_lower_bound(v_k, l_n, l_d, l_closed);
105 // See if we have a valid upper bound.
106 bool u_closed = false;
107 bool u_bounded = box.has_upper_bound(v_k, u_n, u_d, u_closed);
108
109 // See if we have an implicit equality constraint.
110 if (l_bounded && u_bounded
111 && l_closed && u_closed
112 && l_n == u_n && l_d == u_d) {
113 // Add the constraint `l_d*v_k == l_n'.
114 con_sys.insert(l_d * v_k == l_n);
115 }
116 else {
117 // Check if a lower bound constraint is required.
118 if (l_bounded) {
119 if (l_closed) {
120 // Add the constraint `l_d*v_k >= l_n'.
121 con_sys.insert(l_d * v_k >= l_n);
122 }
123 else {
124 // Add the constraint `l_d*v_k > l_n'.
125 con_sys.insert(l_d * v_k > l_n);
126 }
127 }
128 // Check if an upper bound constraint is required.
129 if (u_bounded) {
130 if (u_closed) {
131 // Add the constraint `u_d*v_k <= u_n'.
132 con_sys.insert(u_d * v_k <= u_n);
133 }
134 else {
135 // Add the constraint `u_d*v_k < u_n'.
136 con_sys.insert(u_d * v_k < u_n);
137 }
138 }
139 }
140 }
141 }
142
143 // Adding the low-level constraints.
144 con_sys.add_low_level_constraints();
145
146 // Constraints are up-to-date.
147 set_constraints_up_to_date();
148 PPL_ASSERT_HEAVY(OK());
149 }
150
151 template <typename Partial_Function>
152 void
map_space_dimensions(const Partial_Function & pfunc)153 Polyhedron::map_space_dimensions(const Partial_Function& pfunc) {
154 if (space_dim == 0) {
155 return;
156 }
157 if (pfunc.has_empty_codomain()) {
158 // All dimensions vanish: the polyhedron becomes zero_dimensional.
159 if (marked_empty()
160 || (has_pending_constraints()
161 && !remove_pending_to_obtain_generators())
162 || (!generators_are_up_to_date() && !update_generators())) {
163 // Removing all dimensions from the empty polyhedron.
164 space_dim = 0;
165 con_sys.clear();
166 }
167 else {
168 // Removing all dimensions from a non-empty polyhedron.
169 set_zero_dim_univ();
170 }
171
172 PPL_ASSERT_HEAVY(OK());
173 return;
174 }
175
176 const dimension_type new_space_dimension = pfunc.max_in_codomain() + 1;
177
178 if (new_space_dimension == space_dim) {
179 // The partial function `pfunc' is indeed total and thus specifies
180 // a permutation, that is, a renaming of the dimensions. For
181 // maximum efficiency, we will simply permute the columns of the
182 // constraint system and/or the generator system.
183
184 std::vector<Variable> cycle;
185 cycle.reserve(space_dim);
186
187 // Used to mark elements as soon as they are inserted in a cycle.
188 std::deque<bool> visited(space_dim);
189
190 for (dimension_type i = space_dim; i-- > 0; ) {
191 if (visited[i]) {
192 continue;
193 }
194
195 dimension_type j = i;
196 do {
197 visited[j] = true;
198 // The following initialization is only to make the compiler happy.
199 dimension_type k = 0;
200 if (!pfunc.maps(j, k)) {
201 throw_invalid_argument("map_space_dimensions(pfunc)",
202 " pfunc is inconsistent");
203 }
204 if (k == j) {
205 break;
206 }
207
208 cycle.push_back(Variable(j));
209 // Go along the cycle.
210 j = k;
211 } while (!visited[j]);
212
213 // End of cycle.
214
215 // Permute all that is up-to-date. Notice that the contents of
216 // the saturation matrices is unaffected by the permutation of
217 // columns: they remain valid, if they were so.
218 if (constraints_are_up_to_date()) {
219 con_sys.permute_space_dimensions(cycle);
220 }
221
222 if (generators_are_up_to_date()) {
223 gen_sys.permute_space_dimensions(cycle);
224 }
225
226 cycle.clear();
227 }
228
229 PPL_ASSERT_HEAVY(OK());
230 return;
231 }
232
233 // If control gets here, then `pfunc' is not a permutation and some
234 // dimensions must be projected away.
235
236 // If there are pending constraints, using `generators()' we process them.
237 const Generator_System& old_gensys = generators();
238
239 if (old_gensys.has_no_rows()) {
240 // The polyhedron is empty.
241 Polyhedron new_polyhedron(topology(), new_space_dimension, EMPTY);
242 m_swap(new_polyhedron);
243 PPL_ASSERT_HEAVY(OK());
244 return;
245 }
246
247 // Make a local copy of the partial function.
248 std::vector<dimension_type> pfunc_maps(space_dim, not_a_dimension());
249 for (dimension_type j = space_dim; j-- > 0; ) {
250 dimension_type pfunc_j;
251 if (pfunc.maps(j, pfunc_j)) {
252 pfunc_maps[j] = pfunc_j;
253 }
254 }
255
256 Generator_System new_gensys;
257 for (Generator_System::const_iterator i = old_gensys.begin(),
258 old_gensys_end = old_gensys.end(); i != old_gensys_end; ++i) {
259 const Generator& old_g = *i;
260 const Generator::expr_type old_e = old_g.expression();
261 Linear_Expression expr;
262 expr.set_space_dimension(new_space_dimension);
263 bool all_zeroes = true;
264 for (Generator::expr_type::const_iterator j = old_e.begin(),
265 j_end = old_e.end(); j != j_end; ++j) {
266 const dimension_type mapped_id = pfunc_maps[j.variable().id()];
267 if (mapped_id != not_a_dimension()) {
268 add_mul_assign(expr, *j, Variable(mapped_id));
269 all_zeroes = false;
270 }
271 }
272 switch (old_g.type()) {
273 case Generator::LINE:
274 if (!all_zeroes) {
275 new_gensys.insert(line(expr));
276 }
277 break;
278 case Generator::RAY:
279 if (!all_zeroes) {
280 new_gensys.insert(ray(expr));
281 }
282 break;
283 case Generator::POINT:
284 // A point in the origin has all zero homogeneous coefficients.
285 new_gensys.insert(point(expr, old_g.divisor()));
286 break;
287 case Generator::CLOSURE_POINT:
288 // A closure point in the origin has all zero homogeneous coefficients.
289 new_gensys.insert(closure_point(expr, old_g.divisor()));
290 break;
291 }
292 }
293 Polyhedron new_polyhedron(topology(), new_gensys);
294 m_swap(new_polyhedron);
295 PPL_ASSERT_HEAVY(OK(true));
296 }
297
298 template <typename FP_Format, typename Interval_Info>
299 void
refine_with_linear_form_inequality(const Linear_Form<Interval<FP_Format,Interval_Info>> & left,const Linear_Form<Interval<FP_Format,Interval_Info>> & right,const bool is_strict)300 Polyhedron::refine_with_linear_form_inequality(
301 const Linear_Form< Interval<FP_Format, Interval_Info> >& left,
302 const Linear_Form< Interval<FP_Format, Interval_Info> >& right,
303 const bool is_strict) {
304
305 // Check that FP_Format is indeed a floating point type.
306 PPL_COMPILE_TIME_CHECK(!std::numeric_limits<FP_Format>::is_exact,
307 "Polyhedron::refine_with_linear_form_inequality:"
308 " FP_Format not a floating point type.");
309
310 // Dimension compatibility checks.
311 // The dimensions of left and right should not be greater than the
312 // dimension of *this.
313 const dimension_type left_space_dim = left.space_dimension();
314 if (space_dim < left_space_dim) {
315 throw_dimension_incompatible(
316 "refine_with_linear_form_inequality(l1, l2, s)", "l1", left);
317 }
318
319 const dimension_type right_space_dim = right.space_dimension();
320 if (space_dim < right_space_dim) {
321 throw_dimension_incompatible(
322 "refine_with_linear_form_inequality(l1, l2, s)", "l2", right);
323 }
324
325 // We assume that the analyzer will not refine an unreachable test.
326 PPL_ASSERT(!marked_empty());
327
328 typedef Interval<FP_Format, Interval_Info> FP_Interval_Type;
329 typedef Linear_Form<FP_Interval_Type> FP_Linear_Form;
330
331 if (Floating_Point_Expression<FP_Interval_Type, float_ieee754_single>::
332 overflows(left)) {
333 return;
334 }
335
336 if (Floating_Point_Expression<FP_Interval_Type, float_ieee754_single>::
337 overflows(right)) {
338 return;
339 }
340
341 // Overapproximate left - right.
342 FP_Linear_Form left_minus_right(left);
343 left_minus_right -= right;
344 if (Floating_Point_Expression<FP_Interval_Type, float_ieee754_single>::
345 overflows(left_minus_right)) {
346 return;
347 }
348
349 dimension_type lf_space_dim = left_minus_right.space_dimension();
350 FP_Linear_Form lf_approx;
351 overapproximate_linear_form(left_minus_right, lf_space_dim, lf_approx);
352 if (Floating_Point_Expression<FP_Interval_Type, float_ieee754_single>::
353 overflows(lf_approx)) {
354 return;
355 }
356
357 // Normalize left - right.
358 Linear_Expression lf_approx_le;
359 convert_to_integer_expression(lf_approx, lf_space_dim, lf_approx_le);
360
361 // Finally, do the refinement.
362 if (!is_strict || is_necessarily_closed()) {
363 refine_with_constraint(lf_approx_le <= 0);
364 }
365 else {
366 refine_with_constraint(lf_approx_le < 0);
367 }
368 }
369
370 template <typename FP_Format, typename Interval_Info>
371 void
affine_form_image(const Variable var,const Linear_Form<Interval<FP_Format,Interval_Info>> & lf)372 Polyhedron::affine_form_image(const Variable var,
373 const Linear_Form<Interval <FP_Format, Interval_Info> >& lf) {
374
375 // Check that FP_Format is indeed a floating point type.
376 PPL_COMPILE_TIME_CHECK(!std::numeric_limits<FP_Format>::is_exact,
377 "Polyhedron::affine_form_image:"
378 " FP_Format not a floating point type.");
379
380 // Dimension compatibility checks.
381 // The dimension of lf should not be greater than the dimension of *this.
382 const dimension_type lf_space_dim = lf.space_dimension();
383 if (space_dim < lf_space_dim) {
384 throw_dimension_incompatible("affine_form_image(v, l, s)", "l", lf);
385 }
386
387 // `var' should be one of the dimensions of the polyhedron.
388 const dimension_type var_id = var.id();
389 if (space_dim < var_id + 1) {
390 throw_dimension_incompatible("affine_form_image(v, l, s)", "v", var);
391 }
392
393 // We assume that the analyzer will not perform an unreachable assignment.
394 PPL_ASSERT(!marked_empty());
395
396 typedef Interval<FP_Format, Interval_Info> FP_Interval_Type;
397 typedef Linear_Form<FP_Interval_Type> FP_Linear_Form;
398
399 if (Floating_Point_Expression<FP_Interval_Type, float_ieee754_single>::
400 overflows(lf)) {
401 *this = Polyhedron(topology(), space_dim, UNIVERSE);
402 return;
403 }
404
405 // Overapproximate lf.
406 FP_Linear_Form lf_approx;
407 overapproximate_linear_form(lf, lf_space_dim, lf_approx);
408
409 if (Floating_Point_Expression<FP_Interval_Type, float_ieee754_single>::
410 overflows(lf_approx)) {
411 *this = Polyhedron(topology(), space_dim, UNIVERSE);
412 return;
413 }
414
415 // Normalize lf.
416 Linear_Expression lf_approx_le;
417 PPL_DIRTY_TEMP_COEFFICIENT(lo_coeff);
418 PPL_DIRTY_TEMP_COEFFICIENT(hi_coeff);
419 PPL_DIRTY_TEMP_COEFFICIENT(denominator);
420 convert_to_integer_expressions(lf_approx, lf_space_dim, lf_approx_le,
421 lo_coeff, hi_coeff, denominator);
422
423 // Finally, do the assignment.
424 bounded_affine_image(var, lf_approx_le + lo_coeff, lf_approx_le + hi_coeff,
425 denominator);
426 }
427
428 template <typename FP_Format, typename Interval_Info>
429 void
430 Polyhedron
overapproximate_linear_form(const Linear_Form<Interval<FP_Format,Interval_Info>> & lf,const dimension_type lf_dimension,Linear_Form<Interval<FP_Format,Interval_Info>> & result)431 ::overapproximate_linear_form(const Linear_Form<Interval <FP_Format, Interval_Info> >& lf,
432 const dimension_type lf_dimension,
433 Linear_Form<Interval <FP_Format, Interval_Info> >& result) {
434
435 // Check that FP_Format is indeed a floating point type.
436 PPL_COMPILE_TIME_CHECK(!std::numeric_limits<FP_Format>::is_exact,
437 "Polyhedron::overapproximate_linear_form:"
438 " FP_Format not a floating point type.");
439
440 typedef Interval<FP_Format, Interval_Info> FP_Interval_Type;
441 typedef Linear_Form<FP_Interval_Type> FP_Linear_Form;
442
443 // Build a Box from the Polyhedron so that we can extract upper and
444 // lower bounds of variables easily.
445 Box<FP_Interval_Type> box(*this);
446
447 result = FP_Linear_Form(lf.inhomogeneous_term());
448 // FIXME: this may not be policy-neutral.
449 const FP_Interval_Type aux_divisor1(static_cast<FP_Format>(0.5));
450 FP_Interval_Type aux_divisor2(aux_divisor1);
451 aux_divisor2.lower() = static_cast<FP_Format>(-0.5);
452
453 for (dimension_type i = 0; i < lf_dimension; ++i) {
454 Variable curr_var(i);
455 const FP_Interval_Type& curr_coeff = lf.coefficient(curr_var);
456 PPL_ASSERT(curr_coeff.is_bounded());
457 FP_Format curr_lb = curr_coeff.lower();
458 FP_Format curr_ub = curr_coeff.upper();
459 if (curr_lb != 0 || curr_ub != 0) {
460 const FP_Interval_Type& curr_int = box.get_interval(curr_var);
461 FP_Interval_Type curr_addend(curr_ub - curr_lb);
462 curr_addend *= aux_divisor2;
463 curr_addend *= curr_int;
464 result += curr_addend;
465 curr_addend = FP_Interval_Type(curr_lb + curr_ub);
466 curr_addend *= aux_divisor1;
467 FP_Linear_Form curr_addend_lf(curr_var);
468 curr_addend_lf *= curr_addend;
469 result += curr_addend_lf;
470 }
471 }
472 }
473
474 template <typename FP_Format, typename Interval_Info>
475 void
convert_to_integer_expression(const Linear_Form<Interval<FP_Format,Interval_Info>> & lf,const dimension_type lf_dimension,Linear_Expression & result)476 Polyhedron::convert_to_integer_expression(
477 const Linear_Form<Interval <FP_Format, Interval_Info> >& lf,
478 const dimension_type lf_dimension,
479 Linear_Expression& result) {
480 result = Linear_Expression();
481
482 typedef Interval<FP_Format, Interval_Info> FP_Interval_Type;
483 std::vector<Coefficient> numerators(lf_dimension+1);
484 std::vector<Coefficient> denominators(lf_dimension+1);
485
486 // Convert each floating point number to a pair <numerator, denominator>
487 // and compute the lcm of all denominators.
488 PPL_DIRTY_TEMP_COEFFICIENT(lcm);
489 lcm = 1;
490 const FP_Interval_Type& b = lf.inhomogeneous_term();
491 // FIXME: are these checks numerator[i] != 0 really necessary?
492 numer_denom(b.lower(), numerators[lf_dimension],
493 denominators[lf_dimension]);
494 if (numerators[lf_dimension] != 0) {
495 lcm_assign(lcm, lcm, denominators[lf_dimension]);
496 }
497
498 for (dimension_type i = 0; i < lf_dimension; ++i) {
499 const FP_Interval_Type& curr_int = lf.coefficient(Variable(i));
500 numer_denom(curr_int.lower(), numerators[i], denominators[i]);
501 if (numerators[i] != 0) {
502 lcm_assign(lcm, lcm, denominators[i]);
503 }
504 }
505
506 for (dimension_type i = 0; i < lf_dimension; ++i) {
507 if (numerators[i] != 0) {
508 exact_div_assign(denominators[i], lcm, denominators[i]);
509 numerators[i] *= denominators[i];
510 result += numerators[i] * Variable(i);
511 }
512 }
513
514 if (numerators[lf_dimension] != 0) {
515 exact_div_assign(denominators[lf_dimension],
516 lcm, denominators[lf_dimension]);
517 numerators[lf_dimension] *= denominators[lf_dimension];
518 result += numerators[lf_dimension];
519 }
520 }
521
522 template <typename FP_Format, typename Interval_Info>
523 void
convert_to_integer_expressions(const Linear_Form<Interval<FP_Format,Interval_Info>> & lf,const dimension_type lf_dimension,Linear_Expression & res,Coefficient & res_low_coeff,Coefficient & res_hi_coeff,Coefficient & denominator)524 Polyhedron::convert_to_integer_expressions(
525 const Linear_Form<Interval <FP_Format, Interval_Info> >& lf,
526 const dimension_type lf_dimension, Linear_Expression& res,
527 Coefficient& res_low_coeff, Coefficient& res_hi_coeff,
528 Coefficient& denominator) {
529 res = Linear_Expression();
530
531 typedef Interval<FP_Format, Interval_Info> FP_Interval_Type;
532 std::vector<Coefficient> numerators(lf_dimension+2);
533 std::vector<Coefficient> denominators(lf_dimension+2);
534
535 // Convert each floating point number to a pair <numerator, denominator>
536 // and compute the lcm of all denominators.
537 Coefficient& lcm = denominator;
538 lcm = 1;
539 const FP_Interval_Type& b = lf.inhomogeneous_term();
540 numer_denom(b.lower(), numerators[lf_dimension], denominators[lf_dimension]);
541 // FIXME: are these checks numerator[i] != 0 really necessary?
542 if (numerators[lf_dimension] != 0) {
543 lcm_assign(lcm, lcm, denominators[lf_dimension]);
544 }
545
546 numer_denom(b.upper(), numerators[lf_dimension+1],
547 denominators[lf_dimension+1]);
548 if (numerators[lf_dimension+1] != 0) {
549 lcm_assign(lcm, lcm, denominators[lf_dimension+1]);
550 }
551
552 for (dimension_type i = 0; i < lf_dimension; ++i) {
553 const FP_Interval_Type& curr_int = lf.coefficient(Variable(i));
554 numer_denom(curr_int.lower(), numerators[i], denominators[i]);
555 if (numerators[i] != 0) {
556 lcm_assign(lcm, lcm, denominators[i]);
557 }
558 }
559
560 for (dimension_type i = 0; i < lf_dimension; ++i) {
561 if (numerators[i] != 0) {
562 exact_div_assign(denominators[i], lcm, denominators[i]);
563 numerators[i] *= denominators[i];
564 res += numerators[i] * Variable(i);
565 }
566 }
567
568 if (numerators[lf_dimension] != 0) {
569 exact_div_assign(denominators[lf_dimension],
570 lcm, denominators[lf_dimension]);
571 numerators[lf_dimension] *= denominators[lf_dimension];
572 res_low_coeff = numerators[lf_dimension];
573 }
574 else {
575 res_low_coeff = 0;
576 }
577
578 if (numerators[lf_dimension+1] != 0) {
579 exact_div_assign(denominators[lf_dimension+1],
580 lcm, denominators[lf_dimension+1]);
581 numerators[lf_dimension+1] *= denominators[lf_dimension+1];
582 res_hi_coeff = numerators[lf_dimension+1];
583 }
584 else {
585 res_hi_coeff = 0;
586 }
587 }
588
589 template <typename C>
590 void
throw_dimension_incompatible(const char * method,const char * lf_name,const Linear_Form<C> & lf) const591 Polyhedron::throw_dimension_incompatible(const char* method,
592 const char* lf_name,
593 const Linear_Form<C>& lf) const {
594 throw_dimension_incompatible(method, lf_name, lf.space_dimension());
595 }
596
597 template <typename Input>
598 Input&
check_obj_space_dimension_overflow(Input & input,const Topology topol,const char * method,const char * reason)599 Polyhedron::check_obj_space_dimension_overflow(Input& input,
600 const Topology topol,
601 const char* method,
602 const char* reason) {
603 check_space_dimension_overflow(input.space_dimension(),
604 max_space_dimension(),
605 topol, method, reason);
606 return input;
607 }
608
609 } // namespace Parma_Polyhedra_Library
610
611 #endif // !defined(PPL_Polyhedron_templates_hh)
612