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
00273 c = static_cast<int>(d);
00274 ViewArray<IntScaleView> x(home,n_p);
00275 for (int i = n_p; i--; )
00276 x[i].init(t_p[i].a,t_p[i].x);
00277 ViewArray<IntScaleView> y(home,n_n);
00278 for (int i = n_n; i--; )
00279 y[i].init(t_n[i].a,t_n[i].x);
00280 if ((icl == ICL_DOM) && (r == IRT_EQ)) {
00281 GECODE_ES_FAIL((DomEq<int,IntScaleView>::post(home,x,y,c)));
00282 } else {
00283 post_nary<int,IntScaleView>(home,x,y,r,c);
00284 }
00285 } else {
00286
00287 ViewArray<DoubleScaleView> x(home,n_p);
00288 for (int i = n_p; i--; )
00289 x[i].init(t_p[i].a,t_p[i].x);
00290 ViewArray<DoubleScaleView> y(home,n_n);
00291 for (int i = n_n; i--; )
00292 y[i].init(t_n[i].a,t_n[i].x);
00293 if ((icl == ICL_DOM) && (r == IRT_EQ)) {
00294 GECODE_ES_FAIL((DomEq<double,DoubleScaleView>::post(home,x,y,d)));
00295 } else {
00296 post_nary<double,DoubleScaleView>(home,x,y,r,d);
00297 }
00298 }
00299 }
00300
00301 #undef GECODE_INT_PL_BIN
00302 #undef GECODE_INT_PL_TER
00303
00304
00309 template<class Val, class View>
00310 forceinline void
00311 post_nary(Home home,
00312 ViewArray<View>& x, ViewArray<View>& y,
00313 IntRelType r, Val c, BoolView b) {
00314 switch (r) {
00315 case IRT_EQ:
00316 GECODE_ES_FAIL((ReEq<Val,View,View,BoolView>::post(home,x,y,c,b)));
00317 break;
00318 case IRT_NQ:
00319 {
00320 NegBoolView n(b);
00321 GECODE_ES_FAIL((ReEq<Val,View,View,NegBoolView>::post
00322 (home,x,y,c,n)));
00323 }
00324 break;
00325 case IRT_LQ:
00326 GECODE_ES_FAIL((ReLq<Val,View,View>::post(home,x,y,c,b)));
00327 break;
00328 default: GECODE_NEVER;
00329 }
00330 }
00331
00332 void
00333 post(Home home,
00334 Term<IntView>* t, int n, IntRelType r, int c, BoolView b,
00335 IntConLevel) {
00336
00337 Limits::check(c,"Int::linear");
00338
00339 double d = c;
00340
00341 eliminate(t,n,d);
00342
00343 Term<IntView> *t_p, *t_n;
00344 int n_p, n_n;
00345 bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n);
00346
00347 rewrite(r,d,t_p,n_p,t_n,n_n);
00348
00349 if (n == 0) {
00350 bool fail = false;
00351 switch (r) {
00352 case IRT_EQ: fail = (d != 0.0); break;
00353 case IRT_NQ: fail = (d == 0.0); break;
00354 case IRT_LQ: fail = (0.0 > d); break;
00355 default: GECODE_NEVER;
00356 }
00357 if ((fail ? b.zero(home) : b.one(home)) == ME_INT_FAILED)
00358 home.fail();
00359 return;
00360 }
00361
00362 bool is_ip = precision(t_p,n_p,t_n,n_n,d);
00363
00364 if (is_unit && is_ip) {
00365 c = static_cast<int>(d);
00366 if (n == 1) {
00367 switch (r) {
00368 case IRT_EQ:
00369 if (n_p == 1) {
00370 GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,BoolView>::post
00371 (home,t_p[0].x,c,b)));
00372 } else {
00373 GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,BoolView>::post
00374 (home,t_n[0].x,-c,b)));
00375 }
00376 break;
00377 case IRT_NQ:
00378 {
00379 NegBoolView nb(b);
00380 if (n_p == 1) {
00381 GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,NegBoolView>::post
00382 (home,t_p[0].x,c,nb)));
00383 } else {
00384 GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,NegBoolView>::post
00385 (home,t_n[0].x,-c,nb)));
00386 }
00387 }
00388 break;
00389 case IRT_LQ:
00390 if (n_p == 1) {
00391 GECODE_ES_FAIL((Rel::ReLqInt<IntView,BoolView>::post
00392 (home,t_p[0].x,c,b)));
00393 } else {
00394 NegBoolView nb(b);
00395 GECODE_ES_FAIL((Rel::ReLqInt<IntView,NegBoolView>::post
00396 (home,t_n[0].x,-c-1,nb)));
00397 }
00398 break;
00399 default: GECODE_NEVER;
00400 }
00401 } else if (n == 2) {
00402 switch (r) {
00403 case IRT_EQ:
00404 switch (n_p) {
00405 case 2:
00406 GECODE_ES_FAIL((ReEqBin<int,IntView,IntView,BoolView>::post
00407 (home,t_p[0].x,t_p[1].x,c,b)));
00408 break;
00409 case 1:
00410 GECODE_ES_FAIL((ReEqBin<int,IntView,MinusView,BoolView>::post
00411 (home,t_p[0].x,MinusView(t_n[0].x),c,b)));
00412 break;
00413 case 0:
00414 GECODE_ES_FAIL((ReEqBin<int,IntView,IntView,BoolView>::post
00415 (home,t_n[0].x,t_n[1].x,-c,b)));
00416 break;
00417 default: GECODE_NEVER;
00418 }
00419 break;
00420 case IRT_NQ:
00421 {
00422 NegBoolView nb(b);
00423 switch (n_p) {
00424 case 2:
00425 GECODE_ES_FAIL(
00426 (ReEqBin<int,IntView,IntView,NegBoolView>::post
00427 (home,t_p[0].x,t_p[1].x,c,nb)));
00428 break;
00429 case 1:
00430 GECODE_ES_FAIL(
00431 (ReEqBin<int,IntView,MinusView,NegBoolView>::post
00432 (home,t_p[0].x,MinusView(t_n[0].x),c,
00433 NegBoolView(b))));
00434 break;
00435 case 0:
00436 GECODE_ES_FAIL(
00437 (ReEqBin<int,IntView,IntView,NegBoolView>::post
00438 (home,t_p[0].x,t_p[1].x,-c,NegBoolView(b))));
00439 break;
00440 default: GECODE_NEVER;
00441 }
00442 }
00443 break;
00444 case IRT_LQ:
00445 switch (n_p) {
00446 case 2:
00447 GECODE_ES_FAIL((ReLqBin<int,IntView,IntView>::post
00448 (home,t_p[0].x,t_p[1].x,c,b)));
00449 break;
00450 case 1:
00451 GECODE_ES_FAIL((ReLqBin<int,IntView,MinusView>::post
00452 (home,t_p[0].x,MinusView(t_n[0].x),c,b)));
00453 break;
00454 case 0:
00455 GECODE_ES_FAIL((ReLqBin<int,MinusView,MinusView>::post
00456 (home,MinusView(t_n[0].x),
00457 MinusView(t_n[1].x),c,b)));
00458 break;
00459 default: GECODE_NEVER;
00460 }
00461 break;
00462 default: GECODE_NEVER;
00463 }
00464 } else {
00465 ViewArray<IntView> x(home,n_p);
00466 for (int i = n_p; i--; )
00467 x[i] = t_p[i].x;
00468 ViewArray<IntView> y(home,n_n);
00469 for (int i = n_n; i--; )
00470 y[i] = t_n[i].x;
00471 post_nary<int,IntView>(home,x,y,r,c,b);
00472 }
00473 } else if (is_ip) {
00474
00475 c = static_cast<int>(d);
00476 ViewArray<IntScaleView> x(home,n_p);
00477 for (int i = n_p; i--; )
00478 x[i].init(t_p[i].a,t_p[i].x);
00479 ViewArray<IntScaleView> y(home,n_n);
00480 for (int i = n_n; i--; )
00481 y[i].init(t_n[i].a,t_n[i].x);
00482 post_nary<int,IntScaleView>(home,x,y,r,c,b);
00483 } else {
00484
00485 ViewArray<DoubleScaleView> x(home,n_p);
00486 for (int i = n_p; i--; )
00487 x[i].init(t_p[i].a,t_p[i].x);
00488 ViewArray<DoubleScaleView> y(home,n_n);
00489 for (int i = n_n; i--; )
00490 y[i].init(t_n[i].a,t_n[i].x);
00491 post_nary<double,DoubleScaleView>(home,x,y,r,d,b);
00492 }
00493 }
00494
00495 }}}
00496
00497