1 /* Helper classes for intervals.
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_intervals_defs_hh
25 #define PPL_intervals_defs_hh 1
26
27 #include "Checked_Number_defs.hh"
28 #include "assertions.hh"
29 #include <cstdlib>
30
31 namespace Parma_Polyhedra_Library {
32
33 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
34 //! The result of an operation on intervals.
35 /*! \ingroup PPL_CXX_interface */
36 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
37 enum I_Result {
38 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
39 //! \hideinitializer Result may be empty.
40 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
41 I_EMPTY = 1U,
42 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
43 //! \hideinitializer Result may have only one value.
44 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
45 I_SINGLETON = 2U,
46 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
47 /*! \brief \hideinitializer
48 Result may have more than one value, but it is not the domain universe.
49 */
50 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
51 I_SOME = 4U,
52 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
53 //! \hideinitializer Result may be the domain universe.
54 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
55 I_UNIVERSE = 8U,
56 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
57 //! \hideinitializer Result is not empty.
58 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
59 I_NOT_EMPTY = I_SINGLETON | I_SOME | I_UNIVERSE,
60 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
61 //! \hideinitializer Result may be empty or not empty.
62 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
63 I_ANY = I_EMPTY | I_NOT_EMPTY,
64 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
65 //! \hideinitializer Result may be empty or not empty.
66 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
67 I_NOT_UNIVERSE = I_EMPTY | I_SINGLETON | I_SOME,
68 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
69 //! \hideinitializer Result is neither empty nor the domain universe.
70 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
71 I_NOT_DEGENERATE = I_SINGLETON | I_SOME,
72 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
73 //! \hideinitializer Result is definitely exact.
74 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
75 I_EXACT = 16,
76 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
77 //! \hideinitializer Result is definitely inexact.
78 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
79 I_INEXACT = 32,
80 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
81 //! \hideinitializer Operation has definitely changed the set.
82 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
83 I_CHANGED = 64,
84 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
85 //! \hideinitializer Operation has left the set definitely unchanged.
86 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
87 I_UNCHANGED = 128,
88 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
89 //! \hideinitializer Operation is undefined for some combination of values.
90 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
91 I_SINGULARITIES = 256
92 };
93
94 inline I_Result
operator |(I_Result a,I_Result b)95 operator|(I_Result a, I_Result b) {
96 return static_cast<I_Result>(static_cast<unsigned>(a)
97 | static_cast<unsigned>(b));
98 }
99
100 inline I_Result
operator &(I_Result a,I_Result b)101 operator&(I_Result a, I_Result b) {
102 return static_cast<I_Result>(static_cast<unsigned>(a)
103 & static_cast<unsigned>(b));
104 }
105
106 inline I_Result
operator -(I_Result a,I_Result b)107 operator-(I_Result a, I_Result b) {
108 return static_cast<I_Result>(static_cast<unsigned>(a)
109 & ~static_cast<unsigned>(b));
110 }
111
112 template <typename Criteria, typename T>
113 struct Use_By_Ref;
114
115 struct Use_Slow_Copy;
116 template <typename T>
117 struct Use_By_Ref<Use_Slow_Copy, T>
118 : public Bool<Slow_Copy<T>::value> {
119 };
120
121 struct By_Value;
122 template <typename T>
123 struct Use_By_Ref<By_Value, T>
124 : public False {
125 };
126
127 struct By_Ref;
128 template <typename T>
129 struct Use_By_Ref<By_Ref, T>
130 : public True {
131 };
132
133 template <typename T, typename Criteria = Use_Slow_Copy, typename Enable = void>
134 class Val_Or_Ref;
135
136 template <typename T, typename Criteria>
137 class Val_Or_Ref<T, Criteria,
138 typename Enable_If<!Use_By_Ref<Criteria, T>::value>::type> {
139 T value;
140 public:
141 typedef T Arg_Type;
142 typedef T Return_Type;
Val_Or_Ref()143 Val_Or_Ref()
144 : value() {
145 }
Val_Or_Ref(Arg_Type v,bool=false)146 explicit Val_Or_Ref(Arg_Type v, bool = false)
147 : value(v) {
148 }
operator =(Arg_Type v)149 Val_Or_Ref& operator=(Arg_Type v) {
150 value = v;
151 return *this;
152 }
set(Arg_Type v,bool=false)153 void set(Arg_Type v, bool = false) {
154 value = v;
155 }
get() const156 Return_Type get() const {
157 return value;
158 }
operator Return_Type() const159 operator Return_Type() const {
160 return get();
161 }
162 };
163
164 template <typename T, typename Criteria>
165 class Val_Or_Ref<T, Criteria,
166 typename Enable_If<Use_By_Ref<Criteria, T>::value>::type> {
167 const T* ptr;
168 public:
169 typedef T& Arg_Type;
170 typedef const T& Return_Type;
Val_Or_Ref()171 Val_Or_Ref()
172 : ptr(0) {
173 }
Val_Or_Ref(Arg_Type v)174 explicit Val_Or_Ref(Arg_Type v)
175 : ptr(&v) {
176 }
Val_Or_Ref(const T & v,bool)177 Val_Or_Ref(const T& v, bool)
178 : ptr(&v) {
179 }
operator =(Arg_Type v)180 Val_Or_Ref& operator=(Arg_Type v) {
181 ptr = &v;
182 return *this;
183 }
set(Arg_Type v)184 void set(Arg_Type v) {
185 ptr = &v;
186 }
set(const T & v,bool)187 void set(const T& v, bool) {
188 ptr = &v;
189 }
get() const190 Return_Type get() const {
191 return *ptr;
192 }
operator Return_Type() const193 operator Return_Type() const {
194 return get();
195 }
196 };
197
198 class I_Constraint_Base {
199 };
200
201 template <typename Derived>
202 class I_Constraint_Common : public I_Constraint_Base {
203 public:
204 template <typename T>
convert_real(T & to) const205 Result convert_real(T& to) const {
206 const Derived& c = static_cast<const Derived&>(*this);
207 Result r = c.rel();
208 switch (r) {
209 case V_EMPTY:
210 case V_LGE:
211 return r;
212 case V_LE:
213 r = assign_r(to, c.value(), (ROUND_UP | ROUND_STRICT_RELATION));
214 r = result_relation_class(r);
215 if (r == V_EQ) {
216 return V_LE;
217 }
218 goto lt;
219 case V_LT:
220 r = assign_r(to, c.value(), ROUND_UP);
221 r = result_relation_class(r);
222 lt:
223 switch (r) {
224 case V_EMPTY:
225 case V_LT_PLUS_INFINITY:
226 case V_EQ_MINUS_INFINITY:
227 return r;
228 case V_LT:
229 case V_LE:
230 case V_EQ:
231 return V_LT;
232 default:
233 break;
234 }
235 break;
236 case V_GE:
237 r = assign_r(to, c.value(), (ROUND_DOWN | ROUND_STRICT_RELATION));
238 r = result_relation_class(r);
239 if (r == V_EQ) {
240 return V_GE;
241 }
242 goto gt;
243 case V_GT:
244 r = assign_r(to, c.value(), ROUND_DOWN);
245 r = result_relation_class(r);
246 gt:
247 switch (r) {
248 case V_EMPTY:
249 case V_GT_MINUS_INFINITY:
250 case V_EQ_PLUS_INFINITY:
251 return r;
252 case V_LT:
253 case V_LE:
254 case V_EQ:
255 return V_GT;
256 default:
257 break;
258 }
259 break;
260 case V_EQ:
261 r = assign_r(to, c.value(), ROUND_CHECK);
262 r = result_relation_class(r);
263 PPL_ASSERT(r != V_LT && r != V_GT);
264 if (r == V_EQ) {
265 return V_EQ;
266 }
267 else {
268 return V_EMPTY;
269 }
270 case V_NE:
271 r = assign_r(to, c.value(), ROUND_CHECK);
272 r = result_relation_class(r);
273 if (r == V_EQ) {
274 return V_NE;
275 }
276 else {
277 return V_LGE;
278 }
279 default:
280 break;
281 }
282 PPL_UNREACHABLE;
283 return V_EMPTY;
284 }
285 template <typename T>
convert_real(T & to1,Result & rel2,T & to2) const286 Result convert_real(T& to1, Result& rel2, T& to2) const {
287 const Derived& c = static_cast<const Derived&>(*this);
288 Result rel1;
289 if (c.rel() != V_EQ) {
290 rel2 = convert(to2);
291 return V_LGE;
292 }
293 rel2 = assign_r(to2, c.value(), ROUND_UP);
294 rel2 = result_relation_class(rel2);
295 switch (rel2) {
296 case V_EMPTY:
297 case V_EQ_MINUS_INFINITY:
298 case V_EQ:
299 return V_LGE;
300 default:
301 break;
302 }
303 rel1 = assign_r(to1, c.value(), ROUND_DOWN);
304 rel1 = result_relation_class(rel1);
305 switch (rel1) {
306 case V_EQ:
307 PPL_ASSERT(rel2 == V_LE);
308 goto eq;
309 case V_EQ_PLUS_INFINITY:
310 case V_EMPTY:
311 rel2 = rel1;
312 return V_LGE;
313 case V_GE:
314 if (rel2 == V_LE && to1 == to2) {
315 eq:
316 rel2 = V_EQ;
317 return V_LGE;
318 }
319 /* Fall through*/
320 case V_GT:
321 case V_GT_MINUS_INFINITY:
322 return rel1;
323 default:
324 PPL_UNREACHABLE;
325 return V_EMPTY;
326 }
327 switch (rel2) {
328 case V_LE:
329 case V_LT:
330 case V_LT_PLUS_INFINITY:
331 return rel1;
332 default:
333 PPL_UNREACHABLE;
334 return V_EMPTY;
335 }
336 }
337 template <typename T>
convert_integer(T & to) const338 Result convert_integer(T& to) const {
339 Result rel = convert_real(to);
340 switch (rel) {
341 case V_LT:
342 if (is_integer(to)) {
343 rel = sub_assign_r(to, to, T(1), (ROUND_UP | ROUND_STRICT_RELATION));
344 rel = result_relation_class(rel);
345 return (rel == V_EQ) ? V_LE : rel;
346 }
347 /* Fall through */
348 case V_LE:
349 rel = floor_assign_r(to, to, ROUND_UP);
350 rel = result_relation_class(rel);
351 PPL_ASSERT(rel == V_EQ);
352 return V_LE;
353 case V_GT:
354 if (is_integer(to)) {
355 rel = add_assign_r(to, to, T(1), (ROUND_DOWN | ROUND_STRICT_RELATION));
356 rel = result_relation_class(rel);
357 return (rel == V_EQ) ? V_GE : rel;
358 }
359 /* Fall through */
360 case V_GE:
361 rel = ceil_assign_r(to, to, ROUND_DOWN);
362 rel = result_relation_class(rel);
363 PPL_ASSERT(rel == V_EQ);
364 return V_GE;
365 case V_EQ:
366 if (is_integer(to)) {
367 return V_EQ;
368 }
369 return V_EMPTY;
370 case V_NE:
371 if (is_integer(to)) {
372 return V_NE;
373 }
374 return V_LGE;
375 default:
376 return rel;
377 }
378 }
379 };
380
381 struct I_Constraint_Rel {
382 Result rel;
I_Constraint_RelParma_Polyhedra_Library::I_Constraint_Rel383 I_Constraint_Rel(Result r)
384 : rel(r) {
385 PPL_ASSERT(result_relation_class(r) == r);
386 }
I_Constraint_RelParma_Polyhedra_Library::I_Constraint_Rel387 I_Constraint_Rel(Relation_Symbol r)
388 : rel(static_cast<Result>(r)) {
389 }
operator ResultParma_Polyhedra_Library::I_Constraint_Rel390 operator Result() const {
391 return rel;
392 }
393 };
394
395 template <typename T, typename Val_Or_Ref_Criteria = Use_Slow_Copy,
396 bool extended = false>
397 class I_Constraint
398 : public I_Constraint_Common<I_Constraint<T, Val_Or_Ref_Criteria,
399 extended> > {
400 typedef Val_Or_Ref<T, Val_Or_Ref_Criteria> Val_Ref;
401 typedef typename Val_Ref::Arg_Type Arg_Type;
402 typedef typename Val_Ref::Return_Type Return_Type;
403 Result rel_;
404 Val_Ref value_;
405 public:
406 typedef T value_type;
I_Constraint()407 explicit I_Constraint()
408 : rel_(V_LGE) {
409 }
I_Constraint(I_Constraint_Rel r,Arg_Type v)410 I_Constraint(I_Constraint_Rel r, Arg_Type v)
411 : rel_(r), value_(v) {
412 }
I_Constraint(I_Constraint_Rel r,const T & v,bool force)413 I_Constraint(I_Constraint_Rel r, const T& v, bool force)
414 : rel_(r), value_(v, force) {
415 }
416 template <typename U>
I_Constraint(I_Constraint_Rel r,const U & v)417 I_Constraint(I_Constraint_Rel r, const U& v)
418 : rel_(r), value_(v) {
419 }
set(I_Constraint_Rel r,Arg_Type v)420 void set(I_Constraint_Rel r, Arg_Type v) {
421 rel_ = r;
422 value_.set(v);
423 }
set(I_Constraint_Rel r,const T & v,bool force)424 void set(I_Constraint_Rel r, const T& v, bool force) {
425 rel_ = r;
426 value_.set(v, force);
427 }
428 template <typename U>
set(I_Constraint_Rel r,const U & v)429 void set(I_Constraint_Rel r, const U& v) {
430 rel_ = r;
431 value_.set(v);
432 }
value() const433 Return_Type value() const {
434 return value_;
435 }
rel() const436 Result rel() const {
437 return rel_;
438 }
439 };
440
441 template <typename T>
442 inline I_Constraint<T>
i_constraint(I_Constraint_Rel rel,const T & v)443 i_constraint(I_Constraint_Rel rel, const T& v) {
444 return I_Constraint<T>(rel, v);
445 }
446
447 template <typename T>
448 inline I_Constraint<T>
i_constraint(I_Constraint_Rel rel,const T & v,bool force)449 i_constraint(I_Constraint_Rel rel, const T& v, bool force) {
450 return I_Constraint<T>(rel, v, force);
451 }
452
453 template <typename T>
454 inline I_Constraint<T>
i_constraint(I_Constraint_Rel rel,T & v)455 i_constraint(I_Constraint_Rel rel, T& v) {
456 return I_Constraint<T>(rel, v);
457 }
458
459 template <typename T, typename Val_Or_Ref_Criteria>
460 inline I_Constraint<T, Val_Or_Ref_Criteria>
i_constraint(I_Constraint_Rel rel,const T & v,const Val_Or_Ref_Criteria &)461 i_constraint(I_Constraint_Rel rel, const T& v, const Val_Or_Ref_Criteria&) {
462 return I_Constraint<T, Val_Or_Ref_Criteria>(rel, v);
463 }
464
465 template <typename T, typename Val_Or_Ref_Criteria>
466 inline I_Constraint<T, Val_Or_Ref_Criteria>
i_constraint(I_Constraint_Rel rel,const T & v,bool force,const Val_Or_Ref_Criteria &)467 i_constraint(I_Constraint_Rel rel, const T& v, bool force,
468 const Val_Or_Ref_Criteria&) {
469 return I_Constraint<T, Val_Or_Ref_Criteria>(rel, v, force);
470 }
471
472 template <typename T, typename Val_Or_Ref_Criteria>
473 inline I_Constraint<T, Val_Or_Ref_Criteria>
i_constraint(I_Constraint_Rel rel,T & v,const Val_Or_Ref_Criteria &)474 i_constraint(I_Constraint_Rel rel, T& v, const Val_Or_Ref_Criteria&) {
475 return I_Constraint<T, Val_Or_Ref_Criteria>(rel, v);
476 }
477
478 } // namespace Parma_Polyhedra_Library
479
480 #endif // !defined(PPL_intervals_defs_hh)
481