1 /* Polyhedron 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_Polyhedron_inlines_hh
25 #define PPL_Polyhedron_inlines_hh 1
26
27 #include "Generator_defs.hh"
28 #include "compiler.hh"
29 #include <algorithm>
30 #include <deque>
31
32 namespace Parma_Polyhedra_Library {
33
34 inline memory_size_type
total_memory_in_bytes() const35 Polyhedron::total_memory_in_bytes() const {
36 return sizeof(*this) + external_memory_in_bytes();
37 }
38
39 inline dimension_type
space_dimension() const40 Polyhedron::space_dimension() const {
41 return space_dim;
42 }
43
44 inline int32_t
hash_code() const45 Polyhedron::hash_code() const {
46 return hash_code_from_dimension(space_dimension());
47 }
48
49 inline dimension_type
max_space_dimension()50 Polyhedron::max_space_dimension() {
51 using std::min;
52 // One dimension is reserved to have a value of type dimension_type
53 // that does not represent a legal dimension.
54 return min(std::numeric_limits<dimension_type>::max() - 1,
55 min(Constraint_System::max_space_dimension(),
56 Generator_System::max_space_dimension()
57 )
58 );
59 }
60
61 inline Topology
topology() const62 Polyhedron::topology() const {
63 // We can check either one of the two matrices.
64 // (`con_sys' is slightly better, since it is placed at offset 0.)
65 return con_sys.topology();
66 }
67
68 inline bool
is_discrete() const69 Polyhedron::is_discrete() const {
70 return affine_dimension() == 0;
71 }
72
73 inline bool
is_necessarily_closed() const74 Polyhedron::is_necessarily_closed() const {
75 // We can check either one of the two matrices.
76 // (`con_sys' is slightly better, since it is placed at offset 0.)
77 return con_sys.is_necessarily_closed();
78 }
79
80 inline void
upper_bound_assign(const Polyhedron & y)81 Polyhedron::upper_bound_assign(const Polyhedron& y) {
82 poly_hull_assign(y);
83 }
84
85 inline void
difference_assign(const Polyhedron & y)86 Polyhedron::difference_assign(const Polyhedron& y) {
87 poly_difference_assign(y);
88 }
89
90 inline void
widening_assign(const Polyhedron & y,unsigned * tp)91 Polyhedron::widening_assign(const Polyhedron& y, unsigned* tp) {
92 H79_widening_assign(y, tp);
93 }
94
95 inline
~Polyhedron()96 Polyhedron::~Polyhedron() {
97 }
98
99 inline void
m_swap(Polyhedron & y)100 Polyhedron::m_swap(Polyhedron& y) {
101 if (topology() != y.topology()) {
102 throw_topology_incompatible("swap(y)", "y", y);
103 }
104 using std::swap;
105 swap(con_sys, y.con_sys);
106 swap(gen_sys, y.gen_sys);
107 swap(sat_c, y.sat_c);
108 swap(sat_g, y.sat_g);
109 swap(status, y.status);
110 swap(space_dim, y.space_dim);
111 }
112
113 /*! \relates Polyhedron */
114 inline void
swap(Polyhedron & x,Polyhedron & y)115 swap(Polyhedron& x, Polyhedron& y) {
116 x.m_swap(y);
117 }
118
119 inline bool
can_recycle_constraint_systems()120 Polyhedron::can_recycle_constraint_systems() {
121 return true;
122 }
123
124 inline bool
can_recycle_congruence_systems()125 Polyhedron::can_recycle_congruence_systems() {
126 return false;
127 }
128
129 inline bool
marked_empty() const130 Polyhedron::marked_empty() const {
131 return status.test_empty();
132 }
133
134 inline bool
constraints_are_up_to_date() const135 Polyhedron::constraints_are_up_to_date() const {
136 return status.test_c_up_to_date();
137 }
138
139 inline bool
generators_are_up_to_date() const140 Polyhedron::generators_are_up_to_date() const {
141 return status.test_g_up_to_date();
142 }
143
144 inline bool
constraints_are_minimized() const145 Polyhedron::constraints_are_minimized() const {
146 return status.test_c_minimized();
147 }
148
149 inline bool
generators_are_minimized() const150 Polyhedron::generators_are_minimized() const {
151 return status.test_g_minimized();
152 }
153
154 inline bool
sat_c_is_up_to_date() const155 Polyhedron::sat_c_is_up_to_date() const {
156 return status.test_sat_c_up_to_date();
157 }
158
159 inline bool
sat_g_is_up_to_date() const160 Polyhedron::sat_g_is_up_to_date() const {
161 return status.test_sat_g_up_to_date();
162 }
163
164 inline bool
has_pending_constraints() const165 Polyhedron::has_pending_constraints() const {
166 return status.test_c_pending();
167 }
168
169 inline bool
has_pending_generators() const170 Polyhedron::has_pending_generators() const {
171 return status.test_g_pending();
172 }
173
174 inline bool
has_something_pending() const175 Polyhedron::has_something_pending() const {
176 return status.test_c_pending() || status.test_g_pending();
177 }
178
179 inline bool
can_have_something_pending() const180 Polyhedron::can_have_something_pending() const {
181 return constraints_are_minimized()
182 && generators_are_minimized()
183 && (sat_c_is_up_to_date() || sat_g_is_up_to_date());
184 }
185
186 inline bool
is_empty() const187 Polyhedron::is_empty() const {
188 if (marked_empty()) {
189 return true;
190 }
191 // Try a fast-fail test: if generators are up-to-date and
192 // there are no pending constraints, then the generator system
193 // (since it is well formed) contains a point.
194 if (generators_are_up_to_date() && !has_pending_constraints()) {
195 return false;
196 }
197 return !minimize();
198 }
199
200 inline void
set_constraints_up_to_date()201 Polyhedron::set_constraints_up_to_date() {
202 status.set_c_up_to_date();
203 }
204
205 inline void
set_generators_up_to_date()206 Polyhedron::set_generators_up_to_date() {
207 status.set_g_up_to_date();
208 }
209
210 inline void
set_constraints_minimized()211 Polyhedron::set_constraints_minimized() {
212 set_constraints_up_to_date();
213 status.set_c_minimized();
214 }
215
216 inline void
set_generators_minimized()217 Polyhedron::set_generators_minimized() {
218 set_generators_up_to_date();
219 status.set_g_minimized();
220 }
221
222 inline void
set_constraints_pending()223 Polyhedron::set_constraints_pending() {
224 status.set_c_pending();
225 }
226
227 inline void
set_generators_pending()228 Polyhedron::set_generators_pending() {
229 status.set_g_pending();
230 }
231
232 inline void
set_sat_c_up_to_date()233 Polyhedron::set_sat_c_up_to_date() {
234 status.set_sat_c_up_to_date();
235 }
236
237 inline void
set_sat_g_up_to_date()238 Polyhedron::set_sat_g_up_to_date() {
239 status.set_sat_g_up_to_date();
240 }
241
242 inline void
clear_empty()243 Polyhedron::clear_empty() {
244 status.reset_empty();
245 }
246
247 inline void
clear_constraints_minimized()248 Polyhedron::clear_constraints_minimized() {
249 status.reset_c_minimized();
250 }
251
252 inline void
clear_generators_minimized()253 Polyhedron::clear_generators_minimized() {
254 status.reset_g_minimized();
255 }
256
257 inline void
clear_pending_constraints()258 Polyhedron::clear_pending_constraints() {
259 status.reset_c_pending();
260 }
261
262 inline void
clear_pending_generators()263 Polyhedron::clear_pending_generators() {
264 status.reset_g_pending();
265 }
266
267 inline void
clear_sat_c_up_to_date()268 Polyhedron::clear_sat_c_up_to_date() {
269 status.reset_sat_c_up_to_date();
270 // Can get rid of sat_c here.
271 }
272
273 inline void
clear_sat_g_up_to_date()274 Polyhedron::clear_sat_g_up_to_date() {
275 status.reset_sat_g_up_to_date();
276 // Can get rid of sat_g here.
277 }
278
279 inline void
clear_constraints_up_to_date()280 Polyhedron::clear_constraints_up_to_date() {
281 clear_pending_constraints();
282 clear_constraints_minimized();
283 clear_sat_c_up_to_date();
284 clear_sat_g_up_to_date();
285 status.reset_c_up_to_date();
286 // Can get rid of con_sys here.
287 }
288
289 inline void
clear_generators_up_to_date()290 Polyhedron::clear_generators_up_to_date() {
291 clear_pending_generators();
292 clear_generators_minimized();
293 clear_sat_c_up_to_date();
294 clear_sat_g_up_to_date();
295 status.reset_g_up_to_date();
296 // Can get rid of gen_sys here.
297 }
298
299 inline bool
process_pending() const300 Polyhedron::process_pending() const {
301 PPL_ASSERT(space_dim > 0 && !marked_empty());
302 PPL_ASSERT(has_something_pending());
303
304 if (has_pending_constraints()) {
305 return process_pending_constraints();
306 }
307
308 PPL_ASSERT(has_pending_generators());
309 process_pending_generators();
310 return true;
311 }
312
313 inline bool
bounds_from_above(const Linear_Expression & expr) const314 Polyhedron::bounds_from_above(const Linear_Expression& expr) const {
315 return bounds(expr, true);
316 }
317
318 inline bool
bounds_from_below(const Linear_Expression & expr) const319 Polyhedron::bounds_from_below(const Linear_Expression& expr) const {
320 return bounds(expr, false);
321 }
322
323 inline bool
maximize(const Linear_Expression & expr,Coefficient & sup_n,Coefficient & sup_d,bool & maximum) const324 Polyhedron::maximize(const Linear_Expression& expr,
325 Coefficient& sup_n, Coefficient& sup_d,
326 bool& maximum) const {
327 Generator g(point());
328 return max_min(expr, true, sup_n, sup_d, maximum, g);
329 }
330
331 inline bool
maximize(const Linear_Expression & expr,Coefficient & sup_n,Coefficient & sup_d,bool & maximum,Generator & g) const332 Polyhedron::maximize(const Linear_Expression& expr,
333 Coefficient& sup_n, Coefficient& sup_d, bool& maximum,
334 Generator& g) const {
335 return max_min(expr, true, sup_n, sup_d, maximum, g);
336 }
337
338 inline bool
minimize(const Linear_Expression & expr,Coefficient & inf_n,Coefficient & inf_d,bool & minimum) const339 Polyhedron::minimize(const Linear_Expression& expr,
340 Coefficient& inf_n, Coefficient& inf_d,
341 bool& minimum) const {
342 Generator g(point());
343 return max_min(expr, false, inf_n, inf_d, minimum, g);
344 }
345
346 inline bool
minimize(const Linear_Expression & expr,Coefficient & inf_n,Coefficient & inf_d,bool & minimum,Generator & g) const347 Polyhedron::minimize(const Linear_Expression& expr,
348 Coefficient& inf_n, Coefficient& inf_d, bool& minimum,
349 Generator& g) const {
350 return max_min(expr, false, inf_n, inf_d, minimum, g);
351 }
352
353 inline Constraint_System
simplified_constraints() const354 Polyhedron::simplified_constraints() const {
355 PPL_ASSERT(constraints_are_up_to_date());
356 Constraint_System cs(con_sys);
357 if (cs.num_pending_rows() > 0) {
358 cs.unset_pending_rows();
359 }
360 if (has_pending_constraints() || !constraints_are_minimized()) {
361 cs.simplify();
362 }
363 return cs;
364 }
365
366 inline Congruence_System
congruences() const367 Polyhedron::congruences() const {
368 return Congruence_System(minimized_constraints());
369 }
370
371 inline Congruence_System
minimized_congruences() const372 Polyhedron::minimized_congruences() const {
373 return Congruence_System(minimized_constraints());
374 }
375
376 inline void
add_recycled_congruences(Congruence_System & cgs)377 Polyhedron::add_recycled_congruences(Congruence_System& cgs) {
378 add_congruences(cgs);
379 }
380
381 template <typename FP_Format, typename Interval_Info>
382 inline void
generalized_refine_with_linear_form_inequality(const Linear_Form<Interval<FP_Format,Interval_Info>> & left,const Linear_Form<Interval<FP_Format,Interval_Info>> & right,const Relation_Symbol relsym)383 Polyhedron::generalized_refine_with_linear_form_inequality(
384 const Linear_Form< Interval<FP_Format, Interval_Info> >& left,
385 const Linear_Form< Interval<FP_Format, Interval_Info> >& right,
386 const Relation_Symbol relsym) {
387 switch (relsym) {
388 case EQUAL:
389 // TODO: see if we can handle this case more efficiently.
390 refine_with_linear_form_inequality(left, right, false);
391 refine_with_linear_form_inequality(right, left, false);
392 break;
393 case LESS_THAN:
394 refine_with_linear_form_inequality(left, right, true);
395 break;
396 case LESS_OR_EQUAL:
397 refine_with_linear_form_inequality(left, right, false);
398 break;
399 case GREATER_THAN:
400 refine_with_linear_form_inequality(right, left, true);
401 break;
402 case GREATER_OR_EQUAL:
403 refine_with_linear_form_inequality(right, left, false);
404 break;
405 case NOT_EQUAL:
406 break;
407 default:
408 PPL_UNREACHABLE;
409 break;
410 }
411 }
412
413 template <typename FP_Format, typename Interval_Info>
414 inline void
415 Polyhedron::
refine_fp_interval_abstract_store(Box<Interval<FP_Format,Interval_Info>> & store) const416 refine_fp_interval_abstract_store(
417 Box< Interval<FP_Format, Interval_Info> >& store) const {
418
419 // Check that FP_Format is indeed a floating point type.
420 PPL_COMPILE_TIME_CHECK(!std::numeric_limits<FP_Format>::is_exact,
421 "Polyhedron::refine_fp_interval_abstract_store:"
422 " T not a floating point type.");
423
424 typedef Interval<FP_Format, Interval_Info> FP_Interval_Type;
425 store.intersection_assign(Box<FP_Interval_Type>(*this));
426
427 }
428
429 /*! \relates Polyhedron */
430 inline bool
operator !=(const Polyhedron & x,const Polyhedron & y)431 operator!=(const Polyhedron& x, const Polyhedron& y) {
432 return !(x == y);
433 }
434
435 inline bool
strictly_contains(const Polyhedron & y) const436 Polyhedron::strictly_contains(const Polyhedron& y) const {
437 const Polyhedron& x = *this;
438 return x.contains(y) && !y.contains(x);
439 }
440
441 inline void
drop_some_non_integer_points(Complexity_Class complexity)442 Polyhedron::drop_some_non_integer_points(Complexity_Class complexity) {
443 const Variables_Set* const p_vs = 0;
444 drop_some_non_integer_points(p_vs, complexity);
445 }
446
447 inline void
drop_some_non_integer_points(const Variables_Set & vars,Complexity_Class complexity)448 Polyhedron::drop_some_non_integer_points(const Variables_Set& vars,
449 Complexity_Class complexity) {
450 drop_some_non_integer_points(&vars, complexity);
451 }
452
453
454 namespace Interfaces {
455
456 inline bool
is_necessarily_closed_for_interfaces(const Polyhedron & ph)457 is_necessarily_closed_for_interfaces(const Polyhedron& ph) {
458 return ph.is_necessarily_closed();
459 }
460
461 } // namespace Interfaces
462
463 } // namespace Parma_Polyhedra_Library
464
465 #endif // !defined(PPL_Polyhedron_inlines_hh)
466