00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023 #ifndef PPL_Interval_Restriction_defs_hh
00024 #define PPL_Interval_Restriction_defs_hh 1
00025
00026 #include "meta_programming.hh"
00027 #include "Slow_Copy.hh"
00028 #include "assign_or_swap.hh"
00029
00030 namespace Parma_Polyhedra_Library {
00031
00032 struct Interval_Base;
00033
00034 template <typename T, typename Enable = void>
00035 struct Boundary_Value {
00036 typedef T type;
00037 };
00038
00039 template <typename T>
00040 struct Boundary_Value<T, typename Enable_If<Is_Same_Or_Derived<Interval_Base, T>::value>::type > {
00041 typedef typename T::boundary_type type;
00042 };
00043
00044 class Interval_Restriction_None_Base {
00045 public:
00046 bool has_restriction() const {
00047 return false;
00048 }
00049 void normalize() const {
00050 }
00051 template <typename T>
00052 Result restrict(T&, Result dir) const {
00053 return dir;
00054 }
00055 };
00056
00057 inline bool
00058 eq_restriction(const Interval_Restriction_None_Base&, const Interval_Restriction_None_Base) {
00059 return true;
00060 }
00061
00062 template <typename T>
00063 inline bool
00064 contains_restriction(const Interval_Restriction_None_Base&, const T&) {
00065 return true;
00066 }
00067
00068 template <typename T>
00069 inline bool
00070 assign_restriction(Interval_Restriction_None_Base&, const T&) {
00071 return true;
00072 }
00073
00074 template <typename T1, typename T2>
00075 inline bool
00076 join_restriction(Interval_Restriction_None_Base&, const T1&, const T2&) {
00077 return true;
00078 }
00079
00080 template <typename T1, typename T2>
00081 inline bool
00082 intersect_restriction(Interval_Restriction_None_Base&, const T1&, const T2&) {
00083 return true;
00084 }
00085
00086 template <typename T1, typename T2>
00087 inline bool
00088 diff_restriction(Interval_Restriction_None_Base&, const T1&, const T2&) {
00089 return true;
00090 }
00091
00092 template <typename T>
00093 inline bool
00094 neg_restriction(Interval_Restriction_None_Base&, const T&) {
00095 return true;
00096 }
00097
00098 template <typename T1, typename T2>
00099 inline bool
00100 add_restriction(Interval_Restriction_None_Base&, const T1&, const T2&) {
00101 return true;
00102 }
00103
00104 template <typename T1, typename T2>
00105 inline bool
00106 sub_restriction(Interval_Restriction_None_Base&, const T1&, const T2&) {
00107 return true;
00108 }
00109
00110 template <typename T1, typename T2>
00111 inline bool
00112 mul_restriction(Interval_Restriction_None_Base&, const T1&, const T2&) {
00113 return true;
00114 }
00115
00116 template <typename T1, typename T2>
00117 inline bool
00118 div_restriction(Interval_Restriction_None_Base&, const T1&, const T2&) {
00119 return true;
00120 }
00121
00122 inline void
00123 output_restriction(std::ostream&, const Interval_Restriction_None_Base&) {
00124 }
00125
00126 template <typename Base>
00127 class Interval_Restriction_None : public Interval_Restriction_None_Base,
00128 public Base {
00129 public:
00130 Interval_Restriction_None() {
00131 };
00132 template <typename T>
00133 Interval_Restriction_None(const T& init)
00134 : Base(init) {
00135 }
00136 };
00137
00138 class Interval_Restriction_Integer_Base {
00139 };
00140
00141 template <typename Base>
00142 class Interval_Restriction_Integer : public Interval_Restriction_Integer_Base, public Base {
00143 public:
00144 Interval_Restriction_Integer() {
00145 }
00146 void set_integer(bool v = true) {
00147 return set_bit(Base::bitset, integer_bit, v);
00148 }
00149 bool get_integer() const {
00150 return get_bit(Base::bitset, integer_bit);
00151 }
00152
00153 const_int_nodef(integer_bit, Base::next_bit);
00154 const_int_nodef(next_bit, integer_bit + 1);
00155 bool has_restriction() const {
00156 return get_integer();
00157 }
00158 void normalize() const {
00159 }
00160 template <typename T>
00161 Result restrict(T& x, Result dir) const {
00162 if (!has_restriction())
00163 return dir;
00164 switch (dir) {
00165 case V_GT:
00166 if (is_integer(x))
00167 return add_assign_r(x, x, static_cast<T>(1), ROUND_DOWN);
00168
00169 case V_GE:
00170 return ceil_assign_r(x, x, ROUND_DOWN);
00171 case V_LT:
00172 if (is_integer(x))
00173 sub_assign_r(x, x, static_cast<T>(1), ROUND_UP);
00174
00175 case V_LE:
00176 return floor_assign_r(x, x, ROUND_UP);
00177 default:
00178 assert(false);
00179 return dir;
00180 }
00181 }
00182 };
00183
00184 class Simple_Restriction_Integer : public Interval_Restriction_Integer_Base {
00185 public:
00186 Simple_Restriction_Integer(bool i)
00187 : integer(i) {
00188 }
00189 bool get_integer() const {
00190 return integer;
00191 }
00192 private:
00193 bool integer;
00194 };
00195
00196 template <typename From, typename Base, typename Enable = void>
00197 struct Restriction_Integer;
00198
00199 template <typename From, typename Base>
00200 struct Restriction_Integer<From, Base, typename Enable_If<Is_Native_Or_Checked<From>::value>::type> {
00201 typedef Simple_Restriction_Integer type;
00202 static type get(const From& x) {
00203 return Simple_Restriction_Integer(is_integer(x));
00204 }
00205 };
00206
00207 template <typename From, typename Base>
00208 struct Restriction_Integer<From, Base, typename Enable_If<Is_Same_Or_Derived<Interval_Restriction_None_Base, typename From::info_type>::value>::type> {
00209 typedef Simple_Restriction_Integer type;
00210 static type get(const From& x) {
00211 return Simple_Restriction_Integer(x.is_singleton() && is_integer(x.lower()));
00212 }
00213 };
00214
00215 template <typename From, typename Base>
00216 struct Restriction_Integer<From, Base, typename Enable_If<Is_Same_Or_Derived<Interval_Restriction_Integer_Base, typename From::info_type>::value>::type> {
00217 typedef Interval_Restriction_Integer<Base> type;
00218 static const type& get(const From& x) {
00219 return x.info();
00220 }
00221 };
00222
00223 template <typename T1, typename T2>
00224 inline typename Enable_If<Is_Same_Or_Derived<Interval_Restriction_Integer_Base, T1>::value && Is_Same_Or_Derived<Interval_Restriction_Integer_Base, T2>::value, bool>::type
00225 eq_restriction(const T1& x, const T2& y) {
00226 return x.get_integer() == y.get_integer();
00227 }
00228
00229 template <typename T1, typename T2>
00230 inline typename Enable_If<Is_Same_Or_Derived<Interval_Restriction_Integer_Base, T1>::value && Is_Same_Or_Derived<Interval_Restriction_Integer_Base, T2>::value, bool>::type
00231 contains_restriction(const T1& x, const T2& y) {
00232 return !x.get_integer() || y.get_integer();
00233 }
00234
00235 template <typename Base, typename From>
00236 inline bool
00237 assign_restriction(Interval_Restriction_Integer<Base>& to, const From& x) {
00238 to.set_integer(Restriction_Integer<From, Base>::get(x).get_integer());
00239 return true;
00240 }
00241
00242 template <typename Base, typename From1, typename From2>
00243 inline bool
00244 join_restriction(Interval_Restriction_Integer<Base>& to, const From1& x, const From2& y) {
00245 to.set_integer(Restriction_Integer<From1, Base>::get(x).get_integer()
00246 && Restriction_Integer<From2, Base>::get(y).get_integer());
00247 return true;
00248 }
00249
00250 template <typename Base, typename From1, typename From2>
00251 inline bool
00252 intersect_restriction(Interval_Restriction_Integer<Base>& to, const From1& x, const From2& y) {
00253 to.set_integer(Restriction_Integer<From1, Base>::get(x).get_integer()
00254 || Restriction_Integer<From2, Base>::get(y).get_integer());
00255 return true;
00256 }
00257
00258 template <typename Base, typename From1, typename From2>
00259 inline bool
00260 diff_restriction(Interval_Restriction_Integer<Base>& to,
00261 const From1& x, const From2&) {
00262 to.set_integer(Restriction_Integer<From1, Base>::get(x).get_integer());
00263 return true;
00264 }
00265
00266 template <typename Base, typename From>
00267 inline bool
00268 neg_restriction(Interval_Restriction_Integer<Base>& to, const From& x) {
00269 to.set_integer(Restriction_Integer<From, Base>::get(x).get_integer());
00270 return true;
00271 }
00272
00273 template <typename Base, typename From1, typename From2>
00274 inline bool
00275 add_restriction(Interval_Restriction_Integer<Base>& to, const From1& x, const From2& y) {
00276 to.set_integer(Restriction_Integer<From1, Base>::get(x).get_integer()
00277 && Restriction_Integer<From2, Base>::get(y).get_integer());
00278 return true;
00279 }
00280
00281 template <typename Base, typename From1, typename From2>
00282 inline bool
00283 sub_restriction(Interval_Restriction_Integer<Base>& to, const From1& x, const From2& y) {
00284 to.set_integer(Restriction_Integer<From1, Base>::get(x).get_integer()
00285 && Restriction_Integer<From2, Base>::get(y).get_integer());
00286 return true;
00287 }
00288
00289 template <typename Base, typename From1, typename From2>
00290 inline bool
00291 mul_restriction(Interval_Restriction_Integer<Base>& to, const From1& x, const From2& y) {
00292 to.set_integer(Restriction_Integer<From1, Base>::get(x).get_integer()
00293 && Restriction_Integer<From2, Base>::get(y).get_integer());
00294 return true;
00295 }
00296
00297 template <typename Base, typename From1, typename From2>
00298 inline bool
00299 div_restriction(Interval_Restriction_Integer<Base>& to, const From1&, const From2&) {
00300 to.set_integer(false);
00301 return true;
00302 }
00303
00304 template <typename Base>
00305 inline void
00306 output_restriction(std::ostream& s, const Interval_Restriction_Integer<Base>& x) {
00307 if (x.get_integer())
00308 s << "i";
00309 }
00310
00311 class Interval_Restriction_Integer_Modulo_Base {
00312 };
00313
00314 template <typename T, typename Base>
00315 class Interval_Restriction_Integer_Modulo : public Interval_Restriction_Integer_Modulo_Base, public Base {
00316 public:
00317 COMPILE_TIME_CHECK(std::numeric_limits<T>::is_exact, "Type for modulo values must be exact.");
00318 Interval_Restriction_Integer_Modulo() {
00319
00320
00321 clear();
00322 }
00323 bool has_restriction() const {
00324 return divisor != 0;
00325 }
00326 void clear() {
00327 remainder = 0;
00328 divisor = 0;
00329 Base::clear();
00330 }
00331 void normalize() const {
00332 }
00333 template <typename V>
00334 Result restrict(V& x, Result dir) const {
00335 if (!has_restriction())
00336 return dir;
00337 DIRTY_TEMP(V, n);
00338 DIRTY_TEMP(V, div);
00339 Result r;
00340 r = assign_r(div, divisor, ROUND_CHECK);
00341 assert(r == V_EQ);
00342 int s;
00343 r = rem_assign_r(n, x, div, ROUND_NOT_NEEDED);
00344 assert(r == V_EQ);
00345 s = sgn(n);
00346 switch (dir) {
00347 case V_GT:
00348 if (s >= 0) {
00349 r = sub_assign_r(n, div, n, ROUND_NOT_NEEDED);
00350 assert(r == V_EQ);
00351 return add_assign_r(x, x, n, ROUND_DOWN);
00352 }
00353 else
00354 return sub_assign_r(x, x, n, ROUND_DOWN);
00355 case V_GE:
00356 if (s > 0) {
00357 r = sub_assign_r(n, div, n, ROUND_NOT_NEEDED);
00358 assert(r == V_EQ);
00359 return add_assign_r(x, x, n, ROUND_DOWN);
00360 }
00361 else if (s < 0)
00362 return sub_assign_r(x, x, n, ROUND_DOWN);
00363 else
00364 return V_EQ;
00365 case V_LT:
00366 if (s <= 0) {
00367 r = add_assign_r(n, div, n, ROUND_NOT_NEEDED);
00368 assert(r == V_EQ);
00369 return sub_assign_r(x, x, n, ROUND_UP);
00370 }
00371 else
00372 return sub_assign_r(x, x, n, ROUND_UP);
00373 case V_LE:
00374 if (s < 0) {
00375 r = add_assign_r(n, div, n, ROUND_NOT_NEEDED);
00376 assert(r == V_EQ);
00377 return sub_assign_r(x, x, n, ROUND_UP);
00378 }
00379 else if (s > 0)
00380 return sub_assign_r(x, x, n, ROUND_UP);
00381 else
00382 return V_EQ;
00383 default:
00384 assert(false);
00385 return dir;
00386 }
00387 }
00388 void assign_or_swap(Interval_Restriction_Integer_Modulo& x) {
00389 Parma_Polyhedra_Library::assign_or_swap(remainder, x.remainder);
00390 Parma_Polyhedra_Library::assign_or_swap(divisor, x.divisor);
00391 }
00392 typedef T modulo_type;
00393 T remainder;
00394 T divisor;
00395 };
00396
00397 template <typename T, typename Base>
00398 struct Slow_Copy<Interval_Restriction_Integer_Modulo<T, Base> > : public Bool<Slow_Copy<T>::value> {};
00399
00400
00401 template <typename From, typename Base>
00402 struct Restriction_Integer<From, Base, typename Enable_If<Is_Same_Or_Derived<Interval_Restriction_Integer_Modulo_Base, typename From::info_type>::value>::type> {
00403 typedef Simple_Restriction_Integer type;
00404 static type get(const From& x) {
00405 return Simple_Restriction_Integer(x.info().divisor != 0);
00406 }
00407 };
00408
00409 template <typename T>
00410 struct Simple_Restriction_Integer_Modulo : public Interval_Restriction_Integer_Modulo_Base {
00411 template <typename From>
00412 Simple_Restriction_Integer_Modulo(const From& r, const From& d)
00413 : remainder(r), divisor(d) {
00414 }
00415 typedef T modulo_type;
00416 T remainder;
00417 T divisor;
00418 };
00419
00420 template <typename From, typename T, typename Base, typename Enable = void>
00421 struct Restriction_Integer_Modulo;
00422
00423 template <typename From, typename T, typename Base>
00424 struct Restriction_Integer_Modulo<From, T, Base, typename Enable_If<Is_Native_Or_Checked<From>::value>::type> {
00425 typedef Simple_Restriction_Integer_Modulo<T> type;
00426 static const type& get(const From& x) {
00427 static const type integer(0, 1);
00428 static const type not_integer(0, 0);
00429 if (is_integer(x))
00430 return integer;
00431 else
00432 return not_integer;
00433 }
00434 };
00435
00436 template <typename From, typename T, typename Base>
00437 struct Restriction_Integer_Modulo<From, T, Base, typename Enable_If<Is_Same_Or_Derived<Interval_Restriction_None_Base, typename From::info_type>::value>::type> {
00438 typedef Simple_Restriction_Integer_Modulo<T> type;
00439 static const type& get(const From& x) {
00440 static const type integer(0, 1);
00441 static const type not_integer(0, 0);
00442 if (x.is_singleton() && is_integer(x.lower()))
00443 return integer;
00444 else
00445 return not_integer;
00446 }
00447 };
00448
00449 template <typename From, typename T, typename Base>
00450 struct Restriction_Integer_Modulo<From, T, Base, typename Enable_If<Is_Same_Or_Derived<Interval_Restriction_Integer_Base, typename From::info_type>::value>::type> {
00451 typedef Simple_Restriction_Integer_Modulo<T> type;
00452 static const type& get(const From& x) {
00453 static const type integer(0, 1);
00454 static const type not_integer(0, 0);
00455 if (x.info().get_integer())
00456 return integer;
00457 else
00458 return not_integer;
00459 }
00460 };
00461
00462 template <typename From, typename T, typename Base>
00463 struct Restriction_Integer_Modulo<From, T, Base, typename Enable_If<Is_Same_Or_Derived<Interval_Restriction_Integer_Modulo_Base, typename From::info_type>::value>::type> {
00464 typedef Interval_Restriction_Integer_Modulo<T, Base> type;
00465 static const type& get(const From& x) {
00466 return x.info();
00467 }
00468 };
00469
00470 template <typename T1, typename T2>
00471 inline typename Enable_If<Is_Same_Or_Derived<Interval_Restriction_Integer_Modulo_Base, T1>::value && Is_Same_Or_Derived<Interval_Restriction_Integer_Modulo_Base, T2>::value, bool>::type
00472 eq_restriction(const T1& x, const T2& y) {
00473 return x.remainder == y.remainder
00474 && x.divisor == y.divisor;
00475 }
00476
00477 template <typename T1, typename T2>
00478 inline typename Enable_If<Is_Same_Or_Derived<Interval_Restriction_Integer_Modulo_Base, T1>::value && Is_Same_Or_Derived<Interval_Restriction_Integer_Modulo_Base, T2>::value, bool>::type
00479 contains_restriction(const T1& x, const T2& y) {
00480 if (x.divisor == 0)
00481 return true;
00482 if (y.divisor == 0)
00483 return false;
00484 if (x.divisor == y.divisor)
00485 return x.remainder == y.remainder;
00486 DIRTY_TEMP(typename T1::modulo_type, v);
00487 Result r;
00488 r = rem_assign_r(v, y.divisor, x.divisor, ROUND_NOT_NEEDED);
00489 assert(r == V_EQ);
00490 if (v != 0)
00491 return false;
00492 r = rem_assign_r(v, y.remainder, x.divisor, ROUND_NOT_NEEDED);
00493 assert(r == V_EQ);
00494 return v == x.remainder;
00495 }
00496
00497 template <typename T, typename Base>
00498 inline bool
00499 set_unrestricted(Interval_Restriction_Integer_Modulo<T, Base>& to) {
00500 to.remainder = 0;
00501 to.divisor = 0;
00502 return true;
00503 }
00504
00505 template <typename T, typename Base>
00506 inline bool
00507 set_integer(Interval_Restriction_Integer_Modulo<T, Base>& to) {
00508 to.remainder = 0;
00509 to.divisor = 1;
00510 return true;
00511 }
00512
00513 template <typename T, typename Base, typename From>
00514 inline bool
00515 assign_restriction(Interval_Restriction_Integer_Modulo<T, Base>& to, const From& x) {
00516 to.remainder = Restriction_Integer_Modulo<From, T, Base>::get(x).remainder;
00517 to.divisor = Restriction_Integer_Modulo<From, T, Base>::get(x).divisor;
00518 return true;
00519 }
00520
00521 template <typename T, typename Base, typename From1, typename From2>
00522 inline bool
00523 join_restriction(Interval_Restriction_Integer_Modulo<T, Base>& to, const From1& x, const From2& y) {
00524 typedef Restriction_Integer_Modulo<From1, T, Base> Rx;
00525 const typename Rx::type& rx = Rx::get(x);
00526 if (rx.divisor == 0)
00527 return set_unrestricted(to);
00528 typedef Restriction_Integer_Modulo<From2, T, Base> Ry;
00529 const typename Ry::type& ry = Ry::get(y);
00530 if (ry.divisor == 0)
00531 return set_unrestricted(to);
00532 else if (rx.divisor == 1 && ry.divisor == 1
00533 && is_singleton(x) && is_singleton(y)) {
00534 DIRTY_TEMP(typename Boundary_Value<From1>::type, a);
00535 DIRTY_TEMP(typename Boundary_Value<From2>::type, b);
00536 Result r;
00537 r = abs_assign_r(a, f_lower(x), ROUND_CHECK);
00538 if (r != V_EQ)
00539 return set_integer(to);
00540 r = abs_assign_r(b, f_lower(y), ROUND_CHECK);
00541 if (r != V_EQ)
00542 return set_integer(to);
00543 if (a > b)
00544 r = sub_assign_r(a, a, b, ROUND_CHECK);
00545 else
00546 r = sub_assign_r(a, b, a, ROUND_CHECK);
00547 if (r != V_EQ)
00548 return set_integer(to);
00549 r = assign_r(to.divisor, a, ROUND_CHECK);
00550 if (r != V_EQ)
00551 return set_integer(to);
00552 r = rem_assign_r(b, b, a, ROUND_CHECK);
00553 if (r != V_EQ)
00554 return set_integer(to);
00555 r = assign_r(to.remainder, b, ROUND_CHECK);
00556 if (r != V_EQ)
00557 return set_integer(to);
00558 }
00559 else if (contains_restriction(rx, ry)) {
00560 to.remainder = rx.remainder;
00561 to.divisor = rx.divisor;
00562 }
00563 else if (contains_restriction(ry, rx)) {
00564 to.remainder = ry.remainder;
00565 to.divisor = ry.divisor;
00566 }
00567 else
00568 return set_integer(to);
00569 return true;
00570 }
00571
00572 template <typename T, typename Base, typename From1, typename From2>
00573 inline bool
00574 intersect_restriction(Interval_Restriction_Integer_Modulo<T, Base>& to, const From1& x, const From2& y) {
00575 typedef Restriction_Integer_Modulo<From1, T, Base> Rx;
00576 const typename Rx::type& rx = Rx::get(x);
00577 typedef Restriction_Integer_Modulo<From2, T, Base> Ry;
00578 const typename Ry::type& ry = Ry::get(y);
00579 if (rx.divisor == 0) {
00580 to.remainder = ry.remainder;
00581 to.divisor = ry.divisor;
00582 return true;
00583 }
00584 if (ry.divisor == 0) {
00585 to.remainder = rx.remainder;
00586 to.divisor = rx.divisor;
00587 return true;
00588 }
00589 DIRTY_TEMP(T, g);
00590 Result r;
00591 r = gcd_assign_r(g, rx.divisor, ry.divisor, ROUND_DIRECT);
00592 if (r != V_EQ)
00593 return set_integer(to);
00594 DIRTY_TEMP(T, d);
00595 if (rx.remainder > ry.remainder)
00596 r = sub_assign_r(d, rx.remainder, ry.remainder, ROUND_DIRECT);
00597 else
00598 r = sub_assign_r(d, ry.remainder, rx.remainder, ROUND_DIRECT);
00599 if (r != V_EQ)
00600 return set_integer(to);
00601 r = div_assign_r(d, d, g, ROUND_DIRECT);
00602 if (r != V_EQ)
00603 return false;
00604 r = lcm_assign_r(to.divisor, rx.divisor, ry.divisor, ROUND_DIRECT);
00605 if (r != V_EQ)
00606 return set_integer(to);
00607
00608 return true;
00609 }
00610
00611 template <typename T, typename Base, typename From1, typename From2>
00612 inline bool
00613 diff_restriction(Interval_Restriction_Integer_Modulo<T, Base>& to,
00614 const From1& x, const From2& y) {
00615
00616 return true;
00617 }
00618
00619 template <typename T, typename Base, typename From>
00620 inline bool
00621 neg_restriction(Interval_Restriction_Integer_Modulo<T, Base>& to, const From& x) {
00622 return assign_restriction(to, x);
00623 }
00624
00625 template <typename T>
00626 inline void
00627 addmod(T& to, const T& x, const T& y, const T& to_m, const T& y_m) {
00628 Result r;
00629 if (std::numeric_limits<T>::is_bounded) {
00630 r = sub_assign_r(to, y_m, y, ROUND_NOT_NEEDED);
00631 assert(r == V_EQ);
00632 if (x <= to) {
00633 r = add_assign_r(to, x, y, ROUND_NOT_NEEDED);
00634 assert(r == V_EQ);
00635 }
00636 else {
00637 r = sub_assign_r(to, x, to, ROUND_NOT_NEEDED);
00638 assert(r == V_EQ);
00639 }
00640 }
00641 else {
00642 r = add_assign_r(to, x, y, ROUND_NOT_NEEDED);
00643 assert(r == V_EQ);
00644 }
00645 r = rem_assign_r(to, to, to_m, ROUND_NOT_NEEDED);
00646 assert(r == V_EQ);
00647 }
00648
00649 template <typename M, typename T>
00650 inline bool
00651 assign_rem(M& rem, const T& n, const M& div) {
00652 DIRTY_TEMP(T, divisor);
00653 DIRTY_TEMP(T, remainder);
00654 Result r;
00655 r = assign_r(divisor, div, ROUND_CHECK);
00656 if (r != V_EQ)
00657 return false;
00658 r = rem_assign_r(remainder, n, divisor, ROUND_CHECK);
00659 if (r != V_EQ)
00660 return false;
00661 if (sgn(remainder) < 0) {
00662 r = add_assign_r(remainder, remainder, divisor, ROUND_CHECK);
00663 if (r != V_EQ)
00664 return false;
00665 }
00666 r = assign_r(rem, remainder, ROUND_CHECK);
00667 return r == V_EQ;
00668 }
00669
00670
00671 template <typename T, typename Base, typename From1, typename From2>
00672 inline bool
00673 add_restriction(Interval_Restriction_Integer_Modulo<T, Base>& to, const From1& x, const From2& y) {
00674 typedef Restriction_Integer_Modulo<From1, T, Base> Rx;
00675 const typename Rx::type& rx = Rx::get(x);
00676 if (rx.divisor == 0)
00677 return set_unrestricted(to);
00678 typedef Restriction_Integer_Modulo<From2, T, Base> Ry;
00679 const typename Ry::type& ry = Ry::get(y);
00680 if (ry.divisor == 0)
00681 return set_unrestricted(to);
00682 Result r;
00683 DIRTY_TEMP(T, rem);
00684 if (is_singleton(x)) {
00685 if (is_singleton(y))
00686 return set_integer(to);
00687 if (!assign_rem(rem, f_lower(x), ry.divisor))
00688 return set_integer(to);
00689 r = assign_r(to.divisor, ry.divisor, ROUND_NOT_NEEDED);
00690 assert(r == V_EQ);
00691 addmod(to.remainder, rem, ry.remainder, to.divisor, ry.divisor);
00692 }
00693 else if (is_singleton(y)) {
00694 if (!assign_rem(rem, f_lower(y), rx.divisor))
00695 return set_integer(to);
00696 r = assign_r(to.divisor, rx.divisor, ROUND_NOT_NEEDED);
00697 assert(r == V_EQ);
00698 addmod(to.remainder, rx.remainder, rem, to.divisor, to.divisor);
00699 }
00700 else {
00701 r = gcd_assign_r(to.divisor, rx.divisor, ry.divisor, ROUND_NOT_NEEDED);
00702 assert(r == V_EQ);
00703 addmod(to.remainder, rx.remainder, ry.remainder, to.divisor, ry.divisor);
00704 }
00705 return true;
00706 }
00707
00708 template <typename T>
00709 inline void
00710 submod(T& to, const T& x, const T& y, const T& to_m, const T& y_m) {
00711 Result r;
00712 if (x >= y) {
00713 r = sub_assign_r(to, x, y, ROUND_NOT_NEEDED);
00714 assert(r == V_EQ);
00715 }
00716 else {
00717 r = sub_assign_r(to, y_m, y, ROUND_NOT_NEEDED);
00718 assert(r == V_EQ);
00719 r = add_assign_r(to, x, to, ROUND_NOT_NEEDED);
00720 assert(r == V_EQ);
00721 }
00722 r = rem_assign_r(to, to, to_m, ROUND_NOT_NEEDED);
00723 assert(r == V_EQ);
00724 }
00725
00726 template <typename T, typename Base, typename From1, typename From2>
00727 inline bool
00728 sub_restriction(Interval_Restriction_Integer_Modulo<T, Base>& to, const From1& x, const From2& y) {
00729 typedef Restriction_Integer_Modulo<From1, T, Base> Rx;
00730 const typename Rx::type& rx = Rx::get(x);
00731 if (rx.divisor == 0)
00732 return set_unrestricted(to);
00733 typedef Restriction_Integer_Modulo<From2, T, Base> Ry;
00734 const typename Ry::type& ry = Ry::get(y);
00735 if (ry.divisor == 0)
00736 return set_unrestricted(to);
00737 Result r;
00738 DIRTY_TEMP(T, rem);
00739 if (is_singleton(x)) {
00740 if (is_singleton(y))
00741 return set_integer(to);
00742 if (!assign_rem(rem, f_lower(x), ry.divisor))
00743 return set_integer(to);
00744 r = assign_r(to.divisor, ry.divisor, ROUND_NOT_NEEDED);
00745 assert(r == V_EQ);
00746 submod(to.remainder, rem, ry.remainder, to.divisor, ry.divisor);
00747 }
00748 else if (is_singleton(y)) {
00749 if (!assign_rem(rem, f_lower(y), rx.divisor))
00750 return set_integer(to);
00751 r = assign_r(to.divisor, rx.divisor, ROUND_NOT_NEEDED);
00752 assert(r == V_EQ);
00753 submod(to.remainder, rx.remainder, rem, to.divisor, to.divisor);
00754 }
00755 else {
00756 r = gcd_assign_r(to.divisor, rx.divisor, ry.divisor, ROUND_NOT_NEEDED);
00757 assert(r == V_EQ);
00758 submod(to.remainder, rx.remainder, ry.remainder, to.divisor, ry.divisor);
00759 }
00760 return true;
00761 }
00762
00763 template <typename T>
00764 inline void
00765 mulmod(T& to, const T& x, const T& y, const T& to_m) {
00766 Result r;
00767 if (std::numeric_limits<T>::is_bounded) {
00768 DIRTY_TEMP0(mpz_class, a);
00769 DIRTY_TEMP0(mpz_class, b);
00770 r = assign_r(a, x, ROUND_NOT_NEEDED);
00771 assert(r == V_EQ);
00772 r = assign_r(b, y, ROUND_NOT_NEEDED);
00773 assert(r == V_EQ);
00774 r = mul_assign_r(a, a, b, ROUND_NOT_NEEDED);
00775 assert(r == V_EQ);
00776 r = assign_r(b, to_m, ROUND_NOT_NEEDED);
00777 assert(r == V_EQ);
00778 r = rem_assign_r(a, a, b, ROUND_NOT_NEEDED);
00779 assert(r == V_EQ);
00780 r = assign_r(to, a, ROUND_NOT_NEEDED);
00781 assert(r == V_EQ);
00782 }
00783 else {
00784 r = mul_assign_r(to, x, y, ROUND_NOT_NEEDED);
00785 assert(r == V_EQ);
00786 r = rem_assign_r(to, to, to_m, ROUND_NOT_NEEDED);
00787 assert(r == V_EQ);
00788 }
00789 }
00790
00791
00792 template <typename T, typename Base, typename From1, typename From2>
00793 inline bool
00794 mul_restriction(Interval_Restriction_Integer_Modulo<T, Base>& to, const From1& x, const From2& y) {
00795 typedef Restriction_Integer_Modulo<From1, T, Base> Rx;
00796 const typename Rx::type& rx = Rx::get(x);
00797 if (rx.divisor == 0)
00798 return set_unrestricted(to);
00799 typedef Restriction_Integer_Modulo<From2, T, Base> Ry;
00800 const typename Ry::type& ry = Ry::get(y);
00801 if (ry.divisor == 0)
00802 return set_unrestricted(to);
00803 Result r;
00804 DIRTY_TEMP(T, mul);
00805 if (is_singleton(x)) {
00806 if (is_singleton(y))
00807 return set_integer(to);
00808 DIRTY_TEMP(typename Boundary_Value<From1>::type, n);
00809 r = abs_assign_r(n, f_lower(x), ROUND_CHECK);
00810 if (r != V_EQ)
00811 return set_integer(to);
00812 r = assign_r(mul, n, ROUND_CHECK);
00813 if (r != V_EQ)
00814 return set_integer(to);
00815 r = mul_assign_r(to.remainder, mul, ry.remainder, ROUND_NOT_NEEDED);
00816 if (r != V_EQ)
00817 return set_integer(to);
00818 r = mul_assign_r(to.divisor, mul, ry.divisor, ROUND_NOT_NEEDED);
00819 if (r != V_EQ)
00820 return set_integer(to);
00821 }
00822 else if (is_singleton(y)) {
00823 DIRTY_TEMP(typename Boundary_Value<From2>::type, n);
00824 r = abs_assign_r(n, f_lower(y), ROUND_CHECK);
00825 if (r != V_EQ)
00826 return set_integer(to);
00827 r = assign_r(mul, n, ROUND_CHECK);
00828 if (r != V_EQ)
00829 return set_integer(to);
00830 r = mul_assign_r(to.remainder, rx.remainder, mul, ROUND_NOT_NEEDED);
00831 if (r != V_EQ)
00832 return set_integer(to);
00833 r = mul_assign_r(to.divisor, rx.divisor, mul, ROUND_NOT_NEEDED);
00834 if (r != V_EQ)
00835 return set_integer(to);
00836 }
00837 else {
00838 r = gcd_assign_r(to.divisor, rx.divisor, ry.divisor, ROUND_NOT_NEEDED);
00839 assert(r == V_EQ);
00840 mulmod(to.remainder, rx.remainder, ry.remainder, to.divisor);
00841 }
00842 return true;
00843 }
00844
00845 template <typename T, typename Base, typename From1, typename From2>
00846 inline bool
00847 div_restriction(Interval_Restriction_Integer_Modulo<T, Base>& to, const From1& x, const From2& y) {
00848 if (is_singleton(y)) {
00849 if (is_singleton(x)) {
00850
00851 }
00852 }
00853 return set_unrestricted(to);
00854 }
00855
00856 template <typename T, typename Base>
00857 inline void
00858 output_restriction(std::ostream& s, const Interval_Restriction_Integer_Modulo<T, Base>& x) {
00859 if (x.divisor == 1)
00860 s << "i";
00861 else if (x.divisor != 0)
00862 s << "{" << x.remainder << "%" << x.divisor << "}";
00863 }
00864
00865 }
00866
00867 #endif // !defined(PPL_Interval_Info_defs_hh)