00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034
00035
00036
00037
00038 #include <cfloat>
00039 #include <algorithm>
00040
00041 #include <gecode/int/rel.hh>
00042 #include <gecode/int/linear.hh>
00043
00044 namespace Gecode { namespace Int { namespace Linear {
00045
00047 const double double_max = 9007199254740991.0;
00049 const double double_min = -9007199254740991.0;
00050
00052 inline void
00053 eliminate(Term<IntView>* t, int &n, double& d) {
00054 for (int i=n; i--; )
00055 if (t[i].x.assigned()) {
00056 d -= t[i].a * static_cast<double>(t[i].x.val());
00057 t[i]=t[--n];
00058 }
00059 if ((d < double_min) || (d > double_max))
00060 throw OutOfLimits("Int::linear");
00061 }
00062
00064 inline void
00065 rewrite(IntRelType &r, double &d,
00066 Term<IntView>* &t_p, int &n_p,
00067 Term<IntView>* &t_n, int &n_n) {
00068 switch (r) {
00069 case IRT_EQ: case IRT_NQ: case IRT_LQ:
00070 break;
00071 case IRT_LE:
00072 d--; r = IRT_LQ; break;
00073 case IRT_GR:
00074 d++;
00075 case IRT_GQ:
00076 r = IRT_LQ;
00077 std::swap(n_p,n_n); std::swap(t_p,t_n); d = -d;
00078 break;
00079 default:
00080 throw UnknownRelation("Int::linear");
00081 }
00082 }
00083
00085 inline bool
00086 precision(Term<IntView>* t_p, int n_p,
00087 Term<IntView>* t_n, int n_n,
00088 double d) {
00089 double sl = 0.0;
00090 double su = 0.0;
00091
00092 for (int i = n_p; i--; ) {
00093 sl += t_p[i].a * static_cast<double>(t_p[i].x.min());
00094 su += t_p[i].a * static_cast<double>(t_p[i].x.max());
00095 }
00096 for (int i = n_n; i--; ) {
00097 sl -= t_n[i].a * static_cast<double>(t_n[i].x.max());
00098 su -= t_n[i].a * static_cast<double>(t_n[i].x.min());
00099 }
00100 sl -= d;
00101 su -= d;
00102
00103 if ((sl < double_min) || (su > double_max))
00104 throw OutOfLimits("Int::linear");
00105
00106 bool is_ip = (sl >= Limits::min) && (su <= Limits::max);
00107
00108 for (int i = n_p; i--; ) {
00109 if (sl - t_p[i].a * static_cast<double>(t_p[i].x.min()) < double_min)
00110 throw OutOfLimits("Int::linear");
00111 if (sl - t_p[i].a * static_cast<double>(t_p[i].x.min()) < Limits::min)
00112 is_ip = false;
00113 if (su - t_p[i].a * static_cast<double>(t_p[i].x.max()) > double_max)
00114 throw OutOfLimits("Int::linear");
00115 if (su - t_p[i].a * static_cast<double>(t_p[i].x.max()) > Limits::max)
00116 is_ip = false;
00117 }
00118 for (int i = n_n; i--; ) {
00119 if (sl + t_n[i].a * static_cast<double>(t_n[i].x.min()) < double_min)
00120 throw OutOfLimits("Int::linear");
00121 if (sl + t_n[i].a * static_cast<double>(t_n[i].x.min()) < Limits::min)
00122 is_ip = false;
00123 if (su + t_n[i].a * static_cast<double>(t_n[i].x.max()) > double_max)
00124 throw OutOfLimits("Int::linear");
00125 if (su + t_n[i].a * static_cast<double>(t_n[i].x.max()) > Limits::max)
00126 is_ip = false;
00127 }
00128 return is_ip;
00129 }
00130
00135 template<class Val, class View>
00136 forceinline void
00137 post_nary(Home home,
00138 ViewArray<View>& x, ViewArray<View>& y, IntRelType r, Val c) {
00139 switch (r) {
00140 case IRT_EQ:
00141 GECODE_ES_FAIL(home,(Eq<Val,View,View >::post(home,x,y,c)));
00142 break;
00143 case IRT_NQ:
00144 GECODE_ES_FAIL(home,(Nq<Val,View,View >::post(home,x,y,c)));
00145 break;
00146 case IRT_LQ:
00147 GECODE_ES_FAIL(home,(Lq<Val,View,View >::post(home,x,y,c)));
00148 break;
00149 default: GECODE_NEVER;
00150 }
00151 }
00152
00153
00155 #define GECODE_INT_PL_BIN(CLASS) \
00156 switch (n_p) { \
00157 case 2: \
00158 GECODE_ES_FAIL(home,(CLASS<int,IntView,IntView>::post \
00159 (home,t_p[0].x,t_p[1].x,c))); \
00160 break; \
00161 case 1: \
00162 GECODE_ES_FAIL(home,(CLASS<int,IntView,MinusView>::post \
00163 (home,t_p[0].x,MinusView(t_n[0].x),c))); \
00164 break; \
00165 case 0: \
00166 GECODE_ES_FAIL(home,(CLASS<int,MinusView,MinusView>::post \
00167 (home,MinusView(t_n[0].x),MinusView(t_n[1].x),c))); \
00168 break; \
00169 default: GECODE_NEVER; \
00170 }
00171
00173 #define GECODE_INT_PL_TER(CLASS) \
00174 switch (n_p) { \
00175 case 3: \
00176 GECODE_ES_FAIL(home,(CLASS<int,IntView,IntView,IntView>::post \
00177 (home,t_p[0].x,t_p[1].x,t_p[2].x,c))); \
00178 break; \
00179 case 2: \
00180 GECODE_ES_FAIL(home,(CLASS<int,IntView,IntView,MinusView>::post \
00181 (home,t_p[0].x,t_p[1].x, \
00182 MinusView(t_n[0].x),c))); \
00183 break; \
00184 case 1: \
00185 GECODE_ES_FAIL(home,(CLASS<int,IntView,MinusView,MinusView>::post \
00186 (home,t_p[0].x, \
00187 MinusView(t_n[0].x),MinusView(t_n[1].x),c))); \
00188 break; \
00189 case 0: \
00190 GECODE_ES_FAIL(home,(CLASS<int,MinusView,MinusView,MinusView>::post \
00191 (home,MinusView(t_n[0].x), \
00192 MinusView(t_n[1].x),MinusView(t_n[2].x),c))); \
00193 break; \
00194 default: GECODE_NEVER; \
00195 }
00196
00197 void
00198 post(Home home, Term<IntView>* t, int n, IntRelType r, int c,
00199 IntConLevel icl) {
00200
00201 Limits::check(c,"Int::linear");
00202
00203 double d = c;
00204
00205 eliminate(t,n,d);
00206
00207 Term<IntView> *t_p, *t_n;
00208 int n_p, n_n;
00209 bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n);
00210
00211 rewrite(r,d,t_p,n_p,t_n,n_n);
00212
00213 if (n == 0) {
00214 switch (r) {
00215 case IRT_EQ: if (d != 0.0) home.fail(); break;
00216 case IRT_NQ: if (d == 0.0) home.fail(); break;
00217 case IRT_LQ: if (d < 0.0) home.fail(); break;
00218 default: GECODE_NEVER;
00219 }
00220 return;
00221 }
00222
00223 if (n == 1) {
00224 if (n_p == 1) {
00225 DoubleScaleView y(t_p[0].a,t_p[0].x);
00226 switch (r) {
00227 case IRT_EQ: GECODE_ME_FAIL(home,y.eq(home,d)); break;
00228 case IRT_NQ: GECODE_ME_FAIL(home,y.nq(home,d)); break;
00229 case IRT_LQ: GECODE_ME_FAIL(home,y.lq(home,d)); break;
00230 default: GECODE_NEVER;
00231 }
00232 } else {
00233 DoubleScaleView y(t_n[0].a,t_n[0].x);
00234 switch (r) {
00235 case IRT_EQ: GECODE_ME_FAIL(home,y.eq(home,-d)); break;
00236 case IRT_NQ: GECODE_ME_FAIL(home,y.nq(home,-d)); break;
00237 case IRT_LQ: GECODE_ME_FAIL(home,y.gq(home,-d)); break;
00238 default: GECODE_NEVER;
00239 }
00240 }
00241 return;
00242 }
00243
00244 bool is_ip = precision(t_p,n_p,t_n,n_n,d);
00245
00246 if (is_unit && is_ip && (icl != ICL_DOM)) {
00247
00248 c = static_cast<int>(d);
00249 if (n == 2) {
00250 switch (r) {
00251 case IRT_EQ: GECODE_INT_PL_BIN(EqBin); break;
00252 case IRT_NQ: GECODE_INT_PL_BIN(NqBin); break;
00253 case IRT_LQ: GECODE_INT_PL_BIN(LqBin); break;
00254 default: GECODE_NEVER;
00255 }
00256 } else if (n == 3) {
00257 switch (r) {
00258 case IRT_EQ: GECODE_INT_PL_TER(EqTer); break;
00259 case IRT_NQ: GECODE_INT_PL_TER(NqTer); break;
00260 case IRT_LQ: GECODE_INT_PL_TER(LqTer); break;
00261 default: GECODE_NEVER;
00262 }
00263 } else {
00264 ViewArray<IntView> x(home,n_p);
00265 for (int i = n_p; i--; )
00266 x[i] = t_p[i].x;
00267 ViewArray<IntView> y(home,n_n);
00268 for (int i = n_n; i--; )
00269 y[i] = t_n[i].x;
00270 post_nary<int,IntView>(home,x,y,r,c);
00271 }
00272 } else if (is_ip) {
00273
00274 c = static_cast<int>(d);
00275 ViewArray<IntScaleView> x(home,n_p);
00276 for (int i = n_p; i--; )
00277 x[i].init(t_p[i].a,t_p[i].x);
00278 ViewArray<IntScaleView> y(home,n_n);
00279 for (int i = n_n; i--; )
00280 y[i].init(t_n[i].a,t_n[i].x);
00281 if ((icl == ICL_DOM) && (r == IRT_EQ)) {
00282 GECODE_ES_FAIL(home,(DomEq<int,IntScaleView>::post(home,x,y,c)));
00283 } else {
00284 post_nary<int,IntScaleView>(home,x,y,r,c);
00285 }
00286 } else {
00287
00288 ViewArray<DoubleScaleView> x(home,n_p);
00289 for (int i = n_p; i--; )
00290 x[i].init(t_p[i].a,t_p[i].x);
00291 ViewArray<DoubleScaleView> y(home,n_n);
00292 for (int i = n_n; i--; )
00293 y[i].init(t_n[i].a,t_n[i].x);
00294 if ((icl == ICL_DOM) && (r == IRT_EQ)) {
00295 GECODE_ES_FAIL(home,(DomEq<double,DoubleScaleView>::post(home,x,y,d)));
00296 } else {
00297 post_nary<double,DoubleScaleView>(home,x,y,r,d);
00298 }
00299 }
00300 }
00301
00302 #undef GECODE_INT_PL_BIN
00303 #undef GECODE_INT_PL_TER
00304
00305
00310 template<class Val, class View>
00311 forceinline void
00312 post_nary(Home home,
00313 ViewArray<View>& x, ViewArray<View>& y,
00314 IntRelType r, Val c, BoolView b) {
00315 switch (r) {
00316 case IRT_EQ:
00317 GECODE_ES_FAIL(home,(ReEq<Val,View,View,BoolView>::post(home,x,y,c,b)));
00318 break;
00319 case IRT_NQ:
00320 {
00321 NegBoolView n(b);
00322 GECODE_ES_FAIL(home,(ReEq<Val,View,View,NegBoolView>::post
00323 (home,x,y,c,n)));
00324 }
00325 break;
00326 case IRT_LQ:
00327 GECODE_ES_FAIL(home,(ReLq<Val,View,View>::post(home,x,y,c,b)));
00328 break;
00329 default: GECODE_NEVER;
00330 }
00331 }
00332
00333 void
00334 post(Home home,
00335 Term<IntView>* t, int n, IntRelType r, int c, BoolView b,
00336 IntConLevel) {
00337
00338 Limits::check(c,"Int::linear");
00339
00340 double d = c;
00341
00342 eliminate(t,n,d);
00343
00344 Term<IntView> *t_p, *t_n;
00345 int n_p, n_n;
00346 bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n);
00347
00348 rewrite(r,d,t_p,n_p,t_n,n_n);
00349
00350 if (n == 0) {
00351 bool fail = false;
00352 switch (r) {
00353 case IRT_EQ: fail = (d != 0.0); break;
00354 case IRT_NQ: fail = (d == 0.0); break;
00355 case IRT_LQ: fail = (0.0 > d); break;
00356 default: GECODE_NEVER;
00357 }
00358 if ((fail ? b.zero(home) : b.one(home)) == ME_INT_FAILED)
00359 home.fail();
00360 return;
00361 }
00362
00363 bool is_ip = precision(t_p,n_p,t_n,n_n,d);
00364
00365 if (is_unit && is_ip) {
00366 c = static_cast<int>(d);
00367 if (n == 1) {
00368 switch (r) {
00369 case IRT_EQ:
00370 if (n_p == 1) {
00371 GECODE_ES_FAIL(home,(Rel::ReEqBndInt<IntView,BoolView>::post
00372 (home,t_p[0].x,c,b)));
00373 } else {
00374 GECODE_ES_FAIL(home,(Rel::ReEqBndInt<IntView,BoolView>::post
00375 (home,t_n[0].x,-c,b)));
00376 }
00377 break;
00378 case IRT_NQ:
00379 {
00380 NegBoolView nb(b);
00381 if (n_p == 1) {
00382 GECODE_ES_FAIL(home,(Rel::ReEqBndInt<IntView,NegBoolView>::post
00383 (home,t_p[0].x,c,nb)));
00384 } else {
00385 GECODE_ES_FAIL(home,(Rel::ReEqBndInt<IntView,NegBoolView>::post
00386 (home,t_n[0].x,-c,nb)));
00387 }
00388 }
00389 break;
00390 case IRT_LQ:
00391 if (n_p == 1) {
00392 GECODE_ES_FAIL(home,(Rel::ReLqInt<IntView,BoolView>::post
00393 (home,t_p[0].x,c,b)));
00394 } else {
00395 NegBoolView nb(b);
00396 GECODE_ES_FAIL(home,(Rel::ReLqInt<IntView,NegBoolView>::post
00397 (home,t_n[0].x,-c-1,nb)));
00398 }
00399 break;
00400 default: GECODE_NEVER;
00401 }
00402 } else if (n == 2) {
00403 switch (r) {
00404 case IRT_EQ:
00405 switch (n_p) {
00406 case 2:
00407 GECODE_ES_FAIL(home,(ReEqBin<int,IntView,IntView,BoolView>::post
00408 (home,t_p[0].x,t_p[1].x,c,b)));
00409 break;
00410 case 1:
00411 GECODE_ES_FAIL(home,(ReEqBin<int,IntView,MinusView,BoolView>::post
00412 (home,t_p[0].x,MinusView(t_n[0].x),c,b)));
00413 break;
00414 case 0:
00415 GECODE_ES_FAIL(home,(ReEqBin<int,IntView,IntView,BoolView>::post
00416 (home,t_n[0].x,t_n[1].x,-c,b)));
00417 break;
00418 default: GECODE_NEVER;
00419 }
00420 break;
00421 case IRT_NQ:
00422 {
00423 NegBoolView nb(b);
00424 switch (n_p) {
00425 case 2:
00426 GECODE_ES_FAIL(home,
00427 (ReEqBin<int,IntView,IntView,NegBoolView>::post
00428 (home,t_p[0].x,t_p[1].x,c,nb)));
00429 break;
00430 case 1:
00431 GECODE_ES_FAIL(home,
00432 (ReEqBin<int,IntView,MinusView,NegBoolView>::post
00433 (home,t_p[0].x,MinusView(t_n[0].x),c,
00434 NegBoolView(b))));
00435 break;
00436 case 0:
00437 GECODE_ES_FAIL(home,
00438 (ReEqBin<int,IntView,IntView,NegBoolView>::post
00439 (home,t_p[0].x,t_p[1].x,-c,NegBoolView(b))));
00440 break;
00441 default: GECODE_NEVER;
00442 }
00443 }
00444 break;
00445 case IRT_LQ:
00446 switch (n_p) {
00447 case 2:
00448 GECODE_ES_FAIL(home,(ReLqBin<int,IntView,IntView>::post
00449 (home,t_p[0].x,t_p[1].x,c,b)));
00450 break;
00451 case 1:
00452 GECODE_ES_FAIL(home,(ReLqBin<int,IntView,MinusView>::post
00453 (home,t_p[0].x,MinusView(t_n[0].x),c,b)));
00454 break;
00455 case 0:
00456 GECODE_ES_FAIL(home,(ReLqBin<int,MinusView,MinusView>::post
00457 (home,MinusView(t_n[0].x),
00458 MinusView(t_n[1].x),c,b)));
00459 break;
00460 default: GECODE_NEVER;
00461 }
00462 break;
00463 default: GECODE_NEVER;
00464 }
00465 } else {
00466 ViewArray<IntView> x(home,n_p);
00467 for (int i = n_p; i--; )
00468 x[i] = t_p[i].x;
00469 ViewArray<IntView> y(home,n_n);
00470 for (int i = n_n; i--; )
00471 y[i] = t_n[i].x;
00472 post_nary<int,IntView>(home,x,y,r,c,b);
00473 }
00474 } else if (is_ip) {
00475
00476 c = static_cast<int>(d);
00477 ViewArray<IntScaleView> x(home,n_p);
00478 for (int i = n_p; i--; )
00479 x[i].init(t_p[i].a,t_p[i].x);
00480 ViewArray<IntScaleView> y(home,n_n);
00481 for (int i = n_n; i--; )
00482 y[i].init(t_n[i].a,t_n[i].x);
00483 post_nary<int,IntScaleView>(home,x,y,r,c,b);
00484 } else {
00485
00486 ViewArray<DoubleScaleView> x(home,n_p);
00487 for (int i = n_p; i--; )
00488 x[i].init(t_p[i].a,t_p[i].x);
00489 ViewArray<DoubleScaleView> y(home,n_n);
00490 for (int i = n_n; i--; )
00491 y[i].init(t_n[i].a,t_n[i].x);
00492 post_nary<double,DoubleScaleView>(home,x,y,r,d,b);
00493 }
00494 }
00495
00496 }}}
00497
00498