1 /* Declarations for the Interval class and its constituents.
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_Interval_defs_hh
25 #define PPL_Interval_defs_hh 1
26
27 #include "Interval_types.hh"
28 #include "globals_defs.hh"
29 #include "meta_programming.hh"
30 #include "assign_or_swap.hh"
31 #include "intervals_defs.hh"
32 #include "Interval_Info_defs.hh"
33 #include <iosfwd>
34
35 namespace Parma_Polyhedra_Library {
36
37 enum Ternary { T_YES, T_NO, T_MAYBE };
38
39 inline I_Result
combine(Result l,Result u)40 combine(Result l, Result u) {
41 const unsigned res
42 = static_cast<unsigned>(l) | (static_cast<unsigned>(u) << 6);
43 return static_cast<I_Result>(res);
44 }
45
46 struct Interval_Base {
47 };
48
49 using namespace Boundary_NS;
50 using namespace Interval_NS;
51
52 template <typename T, typename Enable = void>
53 struct Is_Singleton : public Is_Native_Or_Checked<T> {};
54
55 template <typename T>
56 struct Is_Interval : public Is_Same_Or_Derived<Interval_Base, T> {};
57
58 //! A generic, not necessarily closed, possibly restricted interval.
59 /*! \ingroup PPL_CXX_interface
60 The class template type parameter \p Boundary represents the type
61 of the interval boundaries, and can be chosen, among other possibilities,
62 within one of the following number families:
63
64 - a bounded precision native integer type (that is,
65 from <CODE>signed char</CODE> to <CODE>long long</CODE>
66 and from <CODE>int8_t</CODE> to <CODE>int64_t</CODE>);
67 - a bounded precision floating point type (<CODE>float</CODE>,
68 <CODE>double</CODE> or <CODE>long double</CODE>);
69 - an unbounded integer or rational type, as provided by the C++ interface
70 of GMP (<CODE>mpz_class</CODE> or <CODE>mpq_class</CODE>).
71
72 The class template type parameter \p Info allows to control a number
73 of features of the class, among which:
74
75 - the ability to support open as well as closed boundaries;
76 - the ability to represent empty intervals in addition to nonempty ones;
77 - the ability to represent intervals of extended number families
78 that contain positive and negative infinities;
79 */
80 template <typename Boundary, typename Info>
81 class Interval : public Interval_Base, private Info {
82 private:
83 PPL_COMPILE_TIME_CHECK(!Info::store_special
84 || !std::numeric_limits<Boundary>::has_infinity,
85 "store_special is meaningless"
86 " when boundary type may contains infinity");
w_info() const87 Info& w_info() const {
88 return const_cast<Interval&>(*this);
89 }
90
91 public:
92 typedef Boundary boundary_type;
93 typedef Info info_type;
94
95 typedef Interval_NS::Property Property;
96
97 template <typename T>
98 typename Enable_If<Is_Singleton<T>::value || Is_Interval<T>::value, Interval&>::type
operator =(const T & x)99 operator=(const T& x) {
100 assign(x);
101 return *this;
102 }
103
104 template <typename T>
105 typename Enable_If<Is_Singleton<T>::value || Is_Interval<T>::value, Interval&>::type
operator +=(const T & x)106 operator+=(const T& x) {
107 add_assign(*this, x);
108 return *this;
109 }
110 template <typename T>
111 typename Enable_If<Is_Singleton<T>::value || Is_Interval<T>::value, Interval&>::type
operator -=(const T & x)112 operator-=(const T& x) {
113 sub_assign(*this, x);
114 return *this;
115 }
116 template <typename T>
117 typename Enable_If<Is_Singleton<T>::value || Is_Interval<T>::value, Interval&>::type
operator *=(const T & x)118 operator*=(const T& x) {
119 mul_assign(*this, x);
120 return *this;
121 }
122 template <typename T>
123 typename Enable_If<Is_Singleton<T>::value || Is_Interval<T>::value, Interval&>::type
operator /=(const T & x)124 operator/=(const T& x) {
125 div_assign(*this, x);
126 return *this;
127 }
128
129 //! Swaps \p *this with \p y.
130 void m_swap(Interval& y);
131
info()132 Info& info() {
133 return *this;
134 }
135
info() const136 const Info& info() const {
137 return *this;
138 }
139
lower()140 Boundary& lower() {
141 return lower_;
142 }
143
lower() const144 const Boundary& lower() const {
145 return lower_;
146 }
147
upper()148 Boundary& upper() {
149 return upper_;
150 }
151
upper() const152 const Boundary& upper() const {
153 return upper_;
154 }
155
lower_constraint() const156 I_Constraint<boundary_type> lower_constraint() const {
157 PPL_ASSERT(!is_empty());
158 if (info().get_boundary_property(LOWER, SPECIAL)) {
159 return I_Constraint<boundary_type>();
160 }
161 return i_constraint(lower_is_open() ? GREATER_THAN : GREATER_OR_EQUAL,
162 lower(), true);
163 }
upper_constraint() const164 I_Constraint<boundary_type> upper_constraint() const {
165 PPL_ASSERT(!is_empty());
166 if (info().get_boundary_property(UPPER, SPECIAL)) {
167 return I_Constraint<boundary_type>();
168 }
169 return i_constraint(upper_is_open() ? LESS_THAN : LESS_OR_EQUAL,
170 upper(), true);
171 }
172
is_empty() const173 bool is_empty() const {
174 return lt(UPPER, upper(), info(), LOWER, lower(), info());
175 }
176
check_empty(I_Result r) const177 bool check_empty(I_Result r) const {
178 return (r & I_ANY) == I_EMPTY
179 || ((r & I_ANY) != I_NOT_EMPTY && is_empty());
180 }
181
is_singleton() const182 bool is_singleton() const {
183 return eq(LOWER, lower(), info(), UPPER, upper(), info());
184 }
185
lower_is_open() const186 bool lower_is_open() const {
187 PPL_ASSERT(OK());
188 return is_open(LOWER, lower(), info());
189 }
190
upper_is_open() const191 bool upper_is_open() const {
192 PPL_ASSERT(OK());
193 return is_open(UPPER, upper(), info());
194 }
195
lower_is_boundary_infinity() const196 bool lower_is_boundary_infinity() const {
197 PPL_ASSERT(OK());
198 return Boundary_NS::is_boundary_infinity(LOWER, lower(), info());
199 }
200
upper_is_boundary_infinity() const201 bool upper_is_boundary_infinity() const {
202 PPL_ASSERT(OK());
203 return Boundary_NS::is_boundary_infinity(UPPER, upper(), info());
204 }
205
lower_is_domain_inf() const206 bool lower_is_domain_inf() const {
207 PPL_ASSERT(OK());
208 return Boundary_NS::is_domain_inf(LOWER, lower(), info());
209 }
210
upper_is_domain_sup() const211 bool upper_is_domain_sup() const {
212 PPL_ASSERT(OK());
213 return Boundary_NS::is_domain_sup(UPPER, upper(), info());
214 }
215
is_bounded() const216 bool is_bounded() const {
217 PPL_ASSERT(OK());
218 return !lower_is_boundary_infinity() && !upper_is_boundary_infinity();
219 }
220
is_universe() const221 bool is_universe() const {
222 PPL_ASSERT(OK());
223 return lower_is_domain_inf() && upper_is_domain_sup();
224 }
225
lower_extend()226 I_Result lower_extend() {
227 info().clear_boundary_properties(LOWER);
228 set_unbounded(LOWER, lower(), info());
229 return I_ANY;
230 }
231
232 template <typename C>
233 typename Enable_If<Is_Same_Or_Derived<I_Constraint_Base, C>::value, I_Result>::type
234 lower_extend(const C& c);
235
upper_extend()236 I_Result upper_extend() {
237 info().clear_boundary_properties(UPPER);
238 set_unbounded(UPPER, upper(), info());
239 return I_ANY;
240 }
241
242 template <typename C>
243 typename Enable_If<Is_Same_Or_Derived<I_Constraint_Base, C>::value, I_Result>::type
244 upper_extend(const C& c);
245
build()246 I_Result build() {
247 return assign(UNIVERSE);
248 }
249
250 template <typename C>
251 typename Enable_If<Is_Same_Or_Derived<I_Constraint_Base, C>::value, I_Result>::type
build(const C & c)252 build(const C& c) {
253 Relation_Symbol rs;
254 switch (c.rel()) {
255 case V_LGE:
256 case V_GT_MINUS_INFINITY:
257 case V_LT_PLUS_INFINITY:
258 return assign(UNIVERSE);
259 default:
260 return assign(EMPTY);
261 case V_LT:
262 case V_LE:
263 case V_GT:
264 case V_GE:
265 case V_EQ:
266 case V_NE:
267 assign(UNIVERSE);
268 rs = static_cast<Relation_Symbol>(c.rel());
269 return refine_existential(rs, c.value());
270 }
271 }
272
273 template <typename C1, typename C2>
274 typename Enable_If<Is_Same_Or_Derived<I_Constraint_Base, C1>::value
275 &&
276 Is_Same_Or_Derived<I_Constraint_Base, C2>::value,
277 I_Result>::type
build(const C1 & c1,const C2 & c2)278 build(const C1& c1, const C2& c2) {
279 switch (c1.rel()) {
280 case V_LGE:
281 return build(c2);
282 case V_NAN:
283 return assign(EMPTY);
284 default:
285 break;
286 }
287 switch (c2.rel()) {
288 case V_LGE:
289 return build(c1);
290 case V_NAN:
291 return assign(EMPTY);
292 default:
293 break;
294 }
295 build(c1);
296 const I_Result r = add_constraint(c2);
297 return r - (I_CHANGED | I_UNCHANGED);
298 }
299
300 template <typename C>
301 typename Enable_If<Is_Same_Or_Derived<I_Constraint_Base, C>::value, I_Result>::type
add_constraint(const C & c)302 add_constraint(const C& c) {
303 Interval x;
304 x.build(c);
305 return intersect_assign(x);
306 }
307
assign(Degenerate_Element e)308 I_Result assign(Degenerate_Element e) {
309 I_Result r;
310 info().clear();
311 switch (e) {
312 case EMPTY:
313 lower_ = 1;
314 upper_ = 0;
315 r = I_EMPTY | I_EXACT;
316 break;
317 case UNIVERSE:
318 set_unbounded(LOWER, lower(), info());
319 set_unbounded(UPPER, upper(), info());
320 r = I_UNIVERSE | I_EXACT;
321 break;
322 default:
323 PPL_UNREACHABLE;
324 r = I_EMPTY;
325 break;
326 }
327 PPL_ASSERT(OK());
328 return r;
329 }
330
331 template <typename From>
332 typename Enable_If<Is_Special<From>::value, I_Result>::type
assign(const From &)333 assign(const From&) {
334 info().clear();
335 Result rl;
336 Result ru;
337 switch (From::vclass) {
338 case VC_MINUS_INFINITY:
339 rl = Boundary_NS::set_minus_infinity(LOWER, lower(), info());
340 ru = Boundary_NS::set_minus_infinity(UPPER, upper(), info());
341 break;
342 case VC_PLUS_INFINITY:
343 rl = Boundary_NS::set_plus_infinity(LOWER, lower(), info());
344 ru = Boundary_NS::set_plus_infinity(UPPER, upper(), info());
345 break;
346 default:
347 PPL_UNREACHABLE;
348 rl = V_NAN;
349 ru = V_NAN;
350 break;
351 }
352 PPL_ASSERT(OK());
353 return combine(rl, ru);
354 }
355
set_infinities()356 I_Result set_infinities() {
357 info().clear();
358 Result rl = Boundary_NS::set_minus_infinity(LOWER, lower(), info());
359 Result ru = Boundary_NS::set_plus_infinity(UPPER, upper(), info());
360 PPL_ASSERT(OK());
361 return combine(rl, ru);
362 }
363
is_always_topologically_closed()364 static bool is_always_topologically_closed() {
365 return !Info::store_open;
366 }
367
is_topologically_closed() const368 bool is_topologically_closed() const {
369 PPL_ASSERT(OK());
370 return is_always_topologically_closed()
371 || is_empty()
372 || ((lower_is_boundary_infinity() || !lower_is_open())
373 && (upper_is_boundary_infinity() || !upper_is_open()));
374 }
375
376 //! Assigns to \p *this its topological closure.
topological_closure_assign()377 void topological_closure_assign() {
378 if (!Info::store_open || is_empty()) {
379 return;
380 }
381 if (lower_is_open() && !lower_is_boundary_infinity()) {
382 info().set_boundary_property(LOWER, OPEN, false);
383 }
384 if (upper_is_open() && !upper_is_boundary_infinity()) {
385 info().set_boundary_property(UPPER, OPEN, false);
386 }
387 }
388
remove_inf()389 void remove_inf() {
390 PPL_ASSERT(!is_empty());
391 if (!Info::store_open) {
392 return;
393 }
394 info().set_boundary_property(LOWER, OPEN, true);
395 }
396
remove_sup()397 void remove_sup() {
398 PPL_ASSERT(!is_empty());
399 if (!Info::store_open) {
400 return;
401 }
402 info().set_boundary_property(UPPER, OPEN, true);
403 }
404
infinity_sign() const405 int infinity_sign() const {
406 PPL_ASSERT(OK());
407 if (is_reverse_infinity(LOWER, lower(), info())) {
408 return 1;
409 }
410 else if (is_reverse_infinity(UPPER, upper(), info())) {
411 return -1;
412 }
413 else {
414 return 0;
415 }
416 }
417
contains_integer_point() const418 bool contains_integer_point() const {
419 PPL_ASSERT(OK());
420 if (is_empty()) {
421 return false;
422 }
423 if (!is_bounded()) {
424 return true;
425 }
426 Boundary l;
427 if (lower_is_open()) {
428 add_assign_r(l, lower(), Boundary(1), ROUND_DOWN);
429 floor_assign_r(l, l, ROUND_DOWN);
430 }
431 else {
432 ceil_assign_r(l, lower(), ROUND_DOWN);
433 }
434 Boundary u;
435 if (upper_is_open()) {
436 sub_assign_r(u, upper(), Boundary(1), ROUND_UP);
437 ceil_assign_r(u, u, ROUND_UP);
438 }
439 else {
440 floor_assign_r(u, upper(), ROUND_UP);
441 }
442 return u >= l;
443 }
444
drop_some_non_integer_points()445 void drop_some_non_integer_points() {
446 if (is_empty()) {
447 return;
448 }
449 if (lower_is_open() && !lower_is_boundary_infinity()) {
450 add_assign_r(lower(), lower(), Boundary(1), ROUND_DOWN);
451 floor_assign_r(lower(), lower(), ROUND_DOWN);
452 info().set_boundary_property(LOWER, OPEN, false);
453 }
454 else {
455 ceil_assign_r(lower(), lower(), ROUND_DOWN);
456 }
457 if (upper_is_open() && !upper_is_boundary_infinity()) {
458 sub_assign_r(upper(), upper(), Boundary(1), ROUND_UP);
459 ceil_assign_r(upper(), upper(), ROUND_UP);
460 info().set_boundary_property(UPPER, OPEN, false);
461 }
462 else {
463 floor_assign_r(upper(), upper(), ROUND_UP);
464 }
465 }
466
467 template <typename From>
468 typename Enable_If<Is_Singleton<From>::value || Is_Interval<From>::value, I_Result>::type
wrap_assign(Bounded_Integer_Type_Width w,Bounded_Integer_Type_Representation r,const From & refinement)469 wrap_assign(Bounded_Integer_Type_Width w,
470 Bounded_Integer_Type_Representation r,
471 const From& refinement) {
472 if (is_empty()) {
473 return I_EMPTY;
474 }
475 if (lower_is_boundary_infinity() || upper_is_boundary_infinity()) {
476 return assign(refinement);
477 }
478 PPL_DIRTY_TEMP(Boundary, u);
479 Result result = sub_2exp_assign_r(u, upper(), w, ROUND_UP);
480 if (result_overflow(result) == 0 && u > lower()) {
481 return assign(refinement);
482 }
483 info().clear();
484 switch (r) {
485 case UNSIGNED:
486 umod_2exp_assign(LOWER, lower(), info(),
487 LOWER, lower(), info(), w);
488 umod_2exp_assign(UPPER, upper(), info(),
489 UPPER, upper(), info(), w);
490 break;
491 case SIGNED_2_COMPLEMENT:
492 smod_2exp_assign(LOWER, lower(), info(),
493 LOWER, lower(), info(), w);
494 smod_2exp_assign(UPPER, upper(), info(),
495 UPPER, upper(), info(), w);
496 break;
497 default:
498 PPL_UNREACHABLE;
499 break;
500 }
501 if (le(LOWER, lower(), info(), UPPER, upper(), info())) {
502 return intersect_assign(refinement);
503 }
504 PPL_DIRTY_TEMP(Interval, tmp);
505 tmp.info().clear();
506 Boundary_NS::assign(LOWER, tmp.lower(), tmp.info(),
507 LOWER, lower(), info());
508 set_unbounded(UPPER, tmp.upper(), tmp.info());
509 tmp.intersect_assign(refinement);
510 lower_extend();
511 intersect_assign(refinement);
512 return join_assign(tmp);
513 }
514
515 //! Returns the total size in bytes of the memory occupied by \p *this.
516 memory_size_type total_memory_in_bytes() const;
517
518 //! Returns the size in bytes of the memory managed by \p *this.
519 memory_size_type external_memory_in_bytes() const;
520
521 void ascii_dump(std::ostream& s) const;
522 bool ascii_load(std::istream& s);
523
OK() const524 bool OK() const {
525 if (!Info::may_be_empty && is_empty()) {
526 #ifndef NDEBUG
527 std::cerr << "The interval is unexpectedly empty.\n";
528 #endif
529 return false;
530 }
531
532 if (is_open(LOWER, lower(), info())) {
533 if (is_plus_infinity(LOWER, lower(), info())) {
534 #ifndef NDEBUG
535 std::cerr << "The lower boundary is +inf open.\n";
536 #endif
537 }
538 }
539 else if (!Info::may_contain_infinity
540 && (is_minus_infinity(LOWER, lower(), info())
541 || is_plus_infinity(LOWER, lower(), info()))) {
542 #ifndef NDEBUG
543 std::cerr << "The lower boundary is unexpectedly infinity.\n";
544 #endif
545 return false;
546 }
547 if (!info().get_boundary_property(LOWER, SPECIAL)) {
548 if (is_not_a_number(lower())) {
549 #ifndef NDEBUG
550 std::cerr << "The lower boundary is not a number.\n";
551 #endif
552 return false;
553 }
554 }
555
556 if (is_open(UPPER, upper(), info())) {
557 if (is_minus_infinity(UPPER, upper(), info())) {
558 #ifndef NDEBUG
559 std::cerr << "The upper boundary is -inf open.\n";
560 #endif
561 }
562 }
563 else if (!Info::may_contain_infinity
564 && (is_minus_infinity(UPPER, upper(), info())
565 || is_plus_infinity(UPPER, upper(), info()))) {
566 #ifndef NDEBUG
567 std::cerr << "The upper boundary is unexpectedly infinity."
568 << std::endl;
569 #endif
570 return false;
571 }
572 if (!info().get_boundary_property(UPPER, SPECIAL)) {
573 if (is_not_a_number(upper())) {
574 #ifndef NDEBUG
575 std::cerr << "The upper boundary is not a number.\n";
576 #endif
577 return false;
578 }
579 }
580
581 // Everything OK.
582 return true;
583 }
584
Interval()585 Interval() {
586 }
587
588 template <typename T>
Interval(const T & x)589 explicit Interval(const T& x) {
590 assign(x);
591 }
592
593 /*! \brief
594 Builds the smallest interval containing the number whose textual
595 representation is contained in \p s.
596 */
597 explicit Interval(const char* s);
598
599 template <typename T>
600 typename Enable_If<Is_Singleton<T>::value
601 || Is_Interval<T>::value, bool>::type
602 contains(const T& y) const;
603
604 template <typename T>
605 typename Enable_If<Is_Singleton<T>::value
606 || Is_Interval<T>::value, bool>::type
607 strictly_contains(const T& y) const;
608
609 template <typename T>
610 typename Enable_If<Is_Singleton<T>::value
611 || Is_Interval<T>::value, bool>::type
612 is_disjoint_from(const T& y) const;
613
614
615 template <typename From>
616 typename Enable_If<Is_Singleton<From>::value
617 || Is_Interval<From>::value, I_Result>::type
618 assign(const From& x);
619
620 template <typename Type>
621 typename Enable_If<Is_Singleton<Type>::value
622 || Is_Interval<Type>::value, bool>::type
623 can_be_exactly_joined_to(const Type& x) const;
624
625 template <typename From>
626 typename Enable_If<Is_Singleton<From>::value
627 || Is_Interval<From>::value, I_Result>::type
628 join_assign(const From& x);
629
630 template <typename From1, typename From2>
631 typename Enable_If<((Is_Singleton<From1>::value
632 || Is_Interval<From1>::value)
633 && (Is_Singleton<From2>::value
634 || Is_Interval<From2>::value)), I_Result>::type
635 join_assign(const From1& x, const From2& y);
636
637 template <typename From>
638 typename Enable_If<Is_Singleton<From>::value
639 || Is_Interval<From>::value, I_Result>::type
640 intersect_assign(const From& x);
641
642 template <typename From1, typename From2>
643 typename Enable_If<((Is_Singleton<From1>::value
644 || Is_Interval<From1>::value)
645 && (Is_Singleton<From2>::value
646 || Is_Interval<From2>::value)), I_Result>::type
647 intersect_assign(const From1& x, const From2& y);
648
649 /*! \brief
650 Assigns to \p *this the smallest interval containing the set-theoretic
651 difference of \p *this and \p x.
652 */
653 template <typename From>
654 typename Enable_If<Is_Singleton<From>::value
655 || Is_Interval<From>::value, I_Result>::type
656 difference_assign(const From& x);
657
658 /*! \brief
659 Assigns to \p *this the smallest interval containing the set-theoretic
660 difference of \p x and \p y.
661 */
662 template <typename From1, typename From2>
663 typename Enable_If<((Is_Singleton<From1>::value
664 || Is_Interval<From1>::value)
665 && (Is_Singleton<From2>::value
666 || Is_Interval<From2>::value)), I_Result>::type
667 difference_assign(const From1& x, const From2& y);
668
669 /*! \brief
670 Assigns to \p *this the largest interval contained in the set-theoretic
671 difference of \p *this and \p x.
672 */
673 template <typename From>
674 typename Enable_If<Is_Singleton<From>::value
675 || Is_Interval<From>::value, I_Result>::type
676 lower_approximation_difference_assign(const From& x);
677
678 /*! \brief
679 Assigns to \p *this a \ref Meet_Preserving_Simplification
680 "meet-preserving simplification" of \p *this with respect to \p y.
681
682 \return
683 \c false if and only if the meet of \p *this and \p y is empty.
684 */
685 template <typename From>
686 typename Enable_If<Is_Interval<From>::value, bool>::type
687 simplify_using_context_assign(const From& y);
688
689 /*! \brief
690 Assigns to \p *this an interval having empty intersection with \p y.
691 The assigned interval should be as large as possible.
692 */
693 template <typename From>
694 typename Enable_If<Is_Interval<From>::value, void>::type
695 empty_intersection_assign(const From& y);
696
697 /*! \brief
698 Refines \p to according to the existential relation \p rel with \p x.
699
700 The \p to interval is restricted to become, upon successful exit,
701 the smallest interval of its type that contains the set
702 \f[
703 \{\,
704 a \in \mathtt{to}
705 \mid
706 \exists b \in \mathtt{x} \st a \mathrel{\mathtt{rel}} b
707 \,\}.
708 \f]
709 \return
710 ???
711 */
712 template <typename From>
713 typename Enable_If<Is_Singleton<From>::value
714 || Is_Interval<From>::value, I_Result>::type
715 refine_existential(Relation_Symbol rel, const From& x);
716
717 /*! \brief
718 Refines \p to so that it satisfies the universal relation \p rel with \p x.
719
720 The \p to interval is restricted to become, upon successful exit,
721 the smallest interval of its type that contains the set
722 \f[
723 \{\,
724 a \in \mathtt{to}
725 \mid
726 \forall b \in \mathtt{x} \itc a \mathrel{\mathtt{rel}} b
727 \,\}.
728 \f]
729 \return
730 ???
731 */
732 template <typename From>
733 typename Enable_If<Is_Singleton<From>::value
734 || Is_Interval<From>::value, I_Result>::type
735 refine_universal(Relation_Symbol rel, const From& x);
736
737 template <typename From>
738 typename Enable_If<Is_Singleton<From>::value
739 || Is_Interval<From>::value, I_Result>::type
740 neg_assign(const From& x);
741
742 template <typename From1, typename From2>
743 typename Enable_If<((Is_Singleton<From1>::value || Is_Interval<From1>::value)
744 && (Is_Singleton<From2>::value || Is_Interval<From2>::value)), I_Result>::type
745 add_assign(const From1& x, const From2& y);
746
747 template <typename From1, typename From2>
748 typename Enable_If<((Is_Singleton<From1>::value || Is_Interval<From1>::value)
749 && (Is_Singleton<From2>::value || Is_Interval<From2>::value)), I_Result>::type
750 sub_assign(const From1& x, const From2& y);
751
752 template <typename From1, typename From2>
753 typename Enable_If<((Is_Singleton<From1>::value || Is_Interval<From1>::value)
754 && (Is_Singleton<From2>::value || Is_Interval<From2>::value)), I_Result>::type
755 mul_assign(const From1& x, const From2& y);
756
757 template <typename From1, typename From2>
758 typename Enable_If<((Is_Singleton<From1>::value || Is_Interval<From1>::value)
759 && (Is_Singleton<From2>::value || Is_Interval<From2>::value)), I_Result>::type
760 div_assign(const From1& x, const From2& y);
761
762 template <typename From, typename Iterator>
763 typename Enable_If<Is_Interval<From>::value, void>::type
764 CC76_widening_assign(const From& y, Iterator first, Iterator last);
765
766 private:
767 Boundary lower_;
768 Boundary upper_;
769 };
770
771 //! Swaps \p x with \p y.
772 /*! \relates Interval */
773 template <typename Boundary, typename Info>
774 void swap(Interval<Boundary, Info>& x, Interval<Boundary, Info>& y);
775
776 } // namespace Parma_Polyhedra_Library
777
778 #include "Interval_inlines.hh"
779 #include "Interval_templates.hh"
780
781 #endif // !defined(PPL_Interval_defs_hh)
782