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