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
00039
00040 #include <gecode/int/linear.hh>
00041
00042 namespace Gecode { namespace Int { namespace Linear {
00043
00045 inline IntRelType
00046 inverse(const IntRelType r) {
00047 switch (r) {
00048 case IRT_EQ: return IRT_NQ; break;
00049 case IRT_NQ: return IRT_EQ; break;
00050 case IRT_GQ: return IRT_LE; break;
00051 case IRT_LQ: return IRT_GR; break;
00052 case IRT_LE: return IRT_GQ; break;
00053 case IRT_GR: return IRT_LQ; break;
00054 default: GECODE_NEVER;
00055 }
00056 throw UnknownRelation("Int::linear");
00057 }
00058
00060 inline void
00061 eliminate(Term<BoolView>* t, int &n, double& d) {
00062 for (int i=n; i--; )
00063 if (t[i].x.one()) {
00064 d -= t[i].a; t[i]=t[--n];
00065 } else if (t[i].x.zero()) {
00066 t[i]=t[--n];
00067 }
00068
00069 Limits::check(d,"Int::linear");
00070 }
00071
00073 inline void
00074 rewrite(IntRelType &r, double &d) {
00075 switch (r) {
00076 case IRT_EQ: case IRT_NQ: case IRT_LQ: case IRT_GQ:
00077 break;
00078 case IRT_LE:
00079 d--; r = IRT_LQ; break;
00080 case IRT_GR:
00081 d++; r = IRT_GQ; break;
00082 default:
00083 throw UnknownRelation("Int::linear");
00084 }
00085 }
00086
00087 void
00088 post_pos_unit(Home home,
00089 Term<BoolView>* t_p, int n_p,
00090 IntRelType r, IntView y, int c) {
00091 switch (r) {
00092 case IRT_EQ:
00093 {
00094 ViewArray<BoolView> x(home,n_p);
00095 for (int i=n_p; i--; )
00096 x[i]=t_p[i].x;
00097 GECODE_ES_FAIL((EqBoolView<BoolView,IntView>
00098 ::post(home,x,y,c)));
00099 }
00100 break;
00101 case IRT_NQ:
00102 {
00103 ViewArray<BoolView> x(home,n_p);
00104 for (int i=n_p; i--; )
00105 x[i]=t_p[i].x;
00106 GECODE_ES_FAIL((NqBoolView<BoolView,IntView>
00107 ::post(home,x,y,c)));
00108 }
00109 break;
00110 case IRT_GQ:
00111 {
00112 ViewArray<BoolView> x(home,n_p);
00113 for (int i=n_p; i--; )
00114 x[i]=t_p[i].x;
00115 GECODE_ES_FAIL((GqBoolView<BoolView,IntView>
00116 ::post(home,x,y,c)));
00117 }
00118 break;
00119 case IRT_LQ:
00120 {
00121 ViewArray<NegBoolView> x(home,n_p);
00122 for (int i=n_p; i--; )
00123 x[i]=NegBoolView(t_p[i].x);
00124 MinusView z(y);
00125 GECODE_ES_FAIL((GqBoolView<NegBoolView,MinusView>
00126 ::post(home,x,z,n_p-c)));
00127 }
00128 break;
00129 default: GECODE_NEVER;
00130 }
00131 }
00132
00133 void
00134 post_pos_unit(Home home,
00135 Term<BoolView>* t_p, int n_p,
00136 IntRelType r, ZeroIntView, int c) {
00137 switch (r) {
00138 case IRT_EQ:
00139 {
00140 ViewArray<BoolView> x(home,n_p);
00141 for (int i=n_p; i--; )
00142 x[i]=t_p[i].x;
00143 GECODE_ES_FAIL((EqBoolInt<BoolView>::post(home,x,c)));
00144 }
00145 break;
00146 case IRT_NQ:
00147 {
00148 ViewArray<BoolView> x(home,n_p);
00149 for (int i=n_p; i--; )
00150 x[i]=t_p[i].x;
00151 GECODE_ES_FAIL((NqBoolInt<BoolView>::post(home,x,c)));
00152 }
00153 break;
00154 case IRT_GQ:
00155 {
00156 ViewArray<BoolView> x(home,n_p);
00157 for (int i=n_p; i--; )
00158 x[i]=t_p[i].x;
00159 GECODE_ES_FAIL((GqBoolInt<BoolView>::post(home,x,c)));
00160 }
00161 break;
00162 case IRT_LQ:
00163 {
00164 ViewArray<NegBoolView> x(home,n_p);
00165 for (int i=n_p; i--; )
00166 x[i]=NegBoolView(t_p[i].x);
00167 GECODE_ES_FAIL((GqBoolInt<NegBoolView>::post(home,x,n_p-c)));
00168 }
00169 break;
00170 default: GECODE_NEVER;
00171 }
00172 }
00173
00174 void
00175 post_pos_unit(Home home,
00176 Term<BoolView>* t_p, int n_p,
00177 IntRelType r, int c, BoolView b,
00178 IntConLevel) {
00179 switch (r) {
00180 case IRT_EQ:
00181 {
00182 ViewArray<BoolView> x(home,n_p);
00183 for (int i=n_p; i--; )
00184 x[i]=t_p[i].x;
00185 GECODE_ES_FAIL((ReEqBoolInt<BoolView,BoolView>::post(home,x,c,b)));
00186 }
00187 break;
00188 case IRT_NQ:
00189 {
00190 ViewArray<BoolView> x(home,n_p);
00191 for (int i=n_p; i--; )
00192 x[i]=t_p[i].x;
00193 NegBoolView nb(b);
00194 GECODE_ES_FAIL((ReEqBoolInt<BoolView,NegBoolView>::post(home,x,c,nb)));
00195 }
00196 break;
00197 case IRT_GQ:
00198 {
00199 ViewArray<BoolView> x(home,n_p);
00200 for (int i=n_p; i--; )
00201 x[i]=t_p[i].x;
00202 GECODE_ES_FAIL((ReGqBoolInt<BoolView,BoolView>::post(home,x,c,b)));
00203 }
00204 break;
00205 case IRT_LQ:
00206 {
00207 ViewArray<NegBoolView> x(home,n_p);
00208 for (int i=n_p; i--; )
00209 x[i]=NegBoolView(t_p[i].x);
00210 GECODE_ES_FAIL((ReGqBoolInt<NegBoolView,BoolView>::post(home,x,n_p-c,b)));
00211 }
00212 break;
00213 default: GECODE_NEVER;
00214 }
00215 }
00216
00217 void
00218 post_neg_unit(Home home,
00219 Term<BoolView>* t_n, int n_n,
00220 IntRelType r, IntView y, int c) {
00221 switch (r) {
00222 case IRT_EQ:
00223 {
00224 ViewArray<BoolView> x(home,n_n);
00225 for (int i=n_n; i--; )
00226 x[i]=t_n[i].x;
00227 MinusView z(y);
00228 GECODE_ES_FAIL((EqBoolView<BoolView,MinusView>
00229 ::post(home,x,z,-c)));
00230 }
00231 break;
00232 case IRT_NQ:
00233 {
00234 ViewArray<BoolView> x(home,n_n);
00235 for (int i=n_n; i--; )
00236 x[i]=t_n[i].x;
00237 MinusView z(y);
00238 GECODE_ES_FAIL((NqBoolView<BoolView,MinusView>
00239 ::post(home,x,z,-c)));
00240 }
00241 break;
00242 case IRT_GQ:
00243 {
00244 ViewArray<NegBoolView> x(home,n_n);
00245 for (int i=n_n; i--; )
00246 x[i]=NegBoolView(t_n[i].x);
00247 GECODE_ES_FAIL((GqBoolView<NegBoolView,IntView>
00248 ::post(home,x,y,n_n+c)));
00249 }
00250 break;
00251 case IRT_LQ:
00252 {
00253 ViewArray<BoolView> x(home,n_n);
00254 for (int i=n_n; i--; )
00255 x[i]=t_n[i].x;
00256 MinusView z(y);
00257 GECODE_ES_FAIL((GqBoolView<BoolView,MinusView>
00258 ::post(home,x,z,-c)));
00259 }
00260 break;
00261 default: GECODE_NEVER;
00262 }
00263 }
00264
00265 void
00266 post_neg_unit(Home home,
00267 Term<BoolView>* t_n, int n_n,
00268 IntRelType r, ZeroIntView, int c) {
00269 switch (r) {
00270 case IRT_EQ:
00271 {
00272 ViewArray<BoolView> x(home,n_n);
00273 for (int i=n_n; i--; )
00274 x[i]=t_n[i].x;
00275 GECODE_ES_FAIL((EqBoolInt<BoolView>::post(home,x,-c)));
00276 }
00277 break;
00278 case IRT_NQ:
00279 {
00280 ViewArray<BoolView> x(home,n_n);
00281 for (int i=n_n; i--; )
00282 x[i]=t_n[i].x;
00283 GECODE_ES_FAIL((NqBoolInt<BoolView>::post(home,x,-c)));
00284 }
00285 break;
00286 case IRT_GQ:
00287 {
00288 ViewArray<NegBoolView> x(home,n_n);
00289 for (int i=n_n; i--; )
00290 x[i]=NegBoolView(t_n[i].x);
00291 GECODE_ES_FAIL((GqBoolInt<NegBoolView>::post(home,x,n_n+c)));
00292 }
00293 break;
00294 case IRT_LQ:
00295 {
00296 ViewArray<BoolView> x(home,n_n);
00297 for (int i=n_n; i--; )
00298 x[i]=t_n[i].x;
00299 GECODE_ES_FAIL((GqBoolInt<BoolView>::post(home,x,-c)));
00300 }
00301 break;
00302 default: GECODE_NEVER;
00303 }
00304 }
00305
00306 void
00307 post_neg_unit(Home home,
00308 Term<BoolView>* t_n, int n_n,
00309 IntRelType r, int c, BoolView b,
00310 IntConLevel) {
00311 switch (r) {
00312 case IRT_EQ:
00313 {
00314 ViewArray<BoolView> x(home,n_n);
00315 for (int i=n_n; i--; )
00316 x[i]=t_n[i].x;
00317 GECODE_ES_FAIL((ReEqBoolInt<BoolView,BoolView>::post(home,x,-c,b)));
00318 }
00319 break;
00320 case IRT_NQ:
00321 {
00322 ViewArray<BoolView> x(home,n_n);
00323 for (int i=n_n; i--; )
00324 x[i]=t_n[i].x;
00325 NegBoolView nb(b);
00326 GECODE_ES_FAIL((ReEqBoolInt<BoolView,NegBoolView>::post(home,x,-c,nb)));
00327 }
00328 break;
00329 case IRT_GQ:
00330 {
00331 ViewArray<NegBoolView> x(home,n_n);
00332 for (int i=n_n; i--; )
00333 x[i]=NegBoolView(t_n[i].x);
00334 GECODE_ES_FAIL((ReGqBoolInt<NegBoolView,BoolView>::post(home,x,n_n+c,b)));
00335 }
00336 break;
00337 case IRT_LQ:
00338 {
00339 ViewArray<BoolView> x(home,n_n);
00340 for (int i=n_n; i--; )
00341 x[i]=t_n[i].x;
00342 GECODE_ES_FAIL((ReGqBoolInt<BoolView,BoolView>::post(home,x,-c,b)));
00343 }
00344 break;
00345 default: GECODE_NEVER;
00346 }
00347 }
00348
00349 void
00350 post_mixed(Home home,
00351 Term<BoolView>* t_p, int n_p,
00352 Term<BoolView>* t_n, int n_n,
00353 IntRelType r, IntView y, int c) {
00354 ScaleBoolArray b_p(home,n_p);
00355 {
00356 ScaleBool* f=b_p.fst();
00357 for (int i=n_p; i--; ) {
00358 f[i].x=t_p[i].x; f[i].a=t_p[i].a;
00359 }
00360 }
00361 ScaleBoolArray b_n(home,n_n);
00362 {
00363 ScaleBool* f=b_n.fst();
00364 for (int i=n_n; i--; ) {
00365 f[i].x=t_n[i].x; f[i].a=t_n[i].a;
00366 }
00367 }
00368 switch (r) {
00369 case IRT_EQ:
00370 GECODE_ES_FAIL(
00371 (EqBoolScale<ScaleBoolArray,ScaleBoolArray,IntView>
00372 ::post(home,b_p,b_n,y,c)));
00373 break;
00374 case IRT_NQ:
00375 GECODE_ES_FAIL(
00376 (NqBoolScale<ScaleBoolArray,ScaleBoolArray,IntView>
00377 ::post(home,b_p,b_n,y,c)));
00378 break;
00379 case IRT_LQ:
00380 GECODE_ES_FAIL(
00381 (LqBoolScale<ScaleBoolArray,ScaleBoolArray,IntView>
00382 ::post(home,b_p,b_n,y,c)));
00383 break;
00384 case IRT_GQ:
00385 {
00386 MinusView m(y);
00387 GECODE_ES_FAIL(
00388 (LqBoolScale<ScaleBoolArray,ScaleBoolArray,MinusView>
00389 ::post(home,b_n,b_p,m,-c)));
00390 }
00391 break;
00392 default:
00393 GECODE_NEVER;
00394 }
00395 }
00396
00397
00398 void
00399 post_mixed(Home home,
00400 Term<BoolView>* t_p, int n_p,
00401 Term<BoolView>* t_n, int n_n,
00402 IntRelType r, ZeroIntView y, int c) {
00403 ScaleBoolArray b_p(home,n_p);
00404 {
00405 ScaleBool* f=b_p.fst();
00406 for (int i=n_p; i--; ) {
00407 f[i].x=t_p[i].x; f[i].a=t_p[i].a;
00408 }
00409 }
00410 ScaleBoolArray b_n(home,n_n);
00411 {
00412 ScaleBool* f=b_n.fst();
00413 for (int i=n_n; i--; ) {
00414 f[i].x=t_n[i].x; f[i].a=t_n[i].a;
00415 }
00416 }
00417 switch (r) {
00418 case IRT_EQ:
00419 GECODE_ES_FAIL(
00420 (EqBoolScale<ScaleBoolArray,ScaleBoolArray,ZeroIntView>
00421 ::post(home,b_p,b_n,y,c)));
00422 break;
00423 case IRT_NQ:
00424 GECODE_ES_FAIL(
00425 (NqBoolScale<ScaleBoolArray,ScaleBoolArray,ZeroIntView>
00426 ::post(home,b_p,b_n,y,c)));
00427 break;
00428 case IRT_LQ:
00429 GECODE_ES_FAIL(
00430 (LqBoolScale<ScaleBoolArray,ScaleBoolArray,ZeroIntView>
00431 ::post(home,b_p,b_n,y,c)));
00432 break;
00433 case IRT_GQ:
00434 GECODE_ES_FAIL(
00435 (LqBoolScale<ScaleBoolArray,ScaleBoolArray,ZeroIntView>
00436 ::post(home,b_n,b_p,y,-c)));
00437 break;
00438 default:
00439 GECODE_NEVER;
00440 }
00441 }
00442
00443 template<class View>
00444 forceinline void
00445 post_all(Home home,
00446 Term<BoolView>* t, int n,
00447 IntRelType r, View x, int c) {
00448
00449 Limits::check(c,"Int::linear");
00450
00451 double d = c;
00452
00453 eliminate(t,n,d);
00454
00455 rewrite(r,d);
00456
00457 c = static_cast<int>(d);
00458
00459 Term<BoolView> *t_p, *t_n;
00460 int n_p, n_n;
00461 bool unit = normalize<BoolView>(t,n,t_p,n_p,t_n,n_n);
00462
00463 if (n == 0) {
00464 switch (r) {
00465 case IRT_EQ: GECODE_ME_FAIL(x.eq(home,-c)); break;
00466 case IRT_NQ: GECODE_ME_FAIL(x.nq(home,-c)); break;
00467 case IRT_GQ: GECODE_ME_FAIL(x.lq(home,-c)); break;
00468 case IRT_LQ: GECODE_ME_FAIL(x.gq(home,-c)); break;
00469 default: GECODE_NEVER;
00470 }
00471 return;
00472 }
00473
00474
00475 {
00476 double sl = x.max()+c;
00477 double su = x.min()+c;
00478 for (int i=n_p; i--; )
00479 su -= t_p[i].a;
00480 for (int i=n_n; i--; )
00481 sl += t_n[i].a;
00482 Limits::check(sl,"Int::linear");
00483 Limits::check(su,"Int::linear");
00484 }
00485
00486 if (unit && (n_n == 0)) {
00488 post_pos_unit(home,t_p,n_p,r,x,c);
00489 } else if (unit && (n_p == 0)) {
00490
00491 post_neg_unit(home,t_n,n_n,r,x,c);
00492 } else {
00493
00494 post_mixed(home,t_p,n_p,t_n,n_n,r,x,c);
00495 }
00496 }
00497
00498
00499 void
00500 post(Home home,
00501 Term<BoolView>* t, int n, IntRelType r, IntView x, int c,
00502 IntConLevel) {
00503 post_all(home,t,n,r,x,c);
00504 }
00505
00506 void
00507 post(Home home,
00508 Term<BoolView>* t, int n, IntRelType r, int c,
00509 IntConLevel) {
00510 ZeroIntView x;
00511 post_all(home,t,n,r,x,c);
00512 }
00513
00514 void
00515 post(Home home,
00516 Term<BoolView>* t, int n, IntRelType r, IntView x, BoolView b,
00517 IntConLevel icl) {
00518 int l, u;
00519 estimate(t,n,0,l,u);
00520 IntVar z(home,l,u); IntView zv(z);
00521 post_all(home,t,n,IRT_EQ,zv,0);
00522 rel(home,z,r,x,b,icl);
00523 }
00524
00525 void
00526 post(Home home,
00527 Term<BoolView>* t, int n, IntRelType r, int c, BoolView b,
00528 IntConLevel icl) {
00529
00530 if (b.one())
00531 return post(home,t,n,r,c,icl);
00532 if (b.zero())
00533 return post(home,t,n,inverse(r),c,icl);
00534
00535 Limits::check(c,"Int::linear");
00536
00537 double d = c;
00538
00539 eliminate(t,n,d);
00540
00541 rewrite(r,d);
00542
00543 c = static_cast<int>(d);
00544
00545 if (n == 0) {
00546 bool fail = false;
00547 switch (r) {
00548 case IRT_EQ: fail = (0 != c); break;
00549 case IRT_NQ: fail = (0 == c); break;
00550 case IRT_GQ: fail = (0 < c); break;
00551 case IRT_LQ: fail = (0 > c); break;
00552 default: GECODE_NEVER;
00553 }
00554 if ((fail ? b.zero(home) : b.one(home)) == ME_INT_FAILED)
00555 home.fail();
00556 return;
00557 }
00558
00559 Term<BoolView> *t_p, *t_n;
00560 int n_p, n_n;
00561 bool unit = normalize<BoolView>(t,n,t_p,n_p,t_n,n_n);
00562
00563
00564 {
00565 double sl = c;
00566 double su = c;
00567 for (int i=n_p; i--; )
00568 su -= t_p[i].a;
00569 for (int i=n_n; i--; )
00570 sl += t_n[i].a;
00571 Limits::check(sl,"Int::linear");
00572 Limits::check(su,"Int::linear");
00573 }
00574
00575 if (unit && (n_n == 0)) {
00577 post_pos_unit(home,t_p,n_p,r,c,b,icl);
00578 } else if (unit && (n_p == 0)) {
00579
00580 post_neg_unit(home,t_n,n_n,r,c,b,icl);
00581 } else {
00582
00583
00584
00585
00586
00587 for (int i=n_n; i--; )
00588 t_n[i].a = -t_n[i].a;
00589
00590
00591 int l, u;
00592 estimate(t,n,0,l,u);
00593 IntVar z(home,l,u); IntView zv(z);
00594 post_all(home,t,n,IRT_EQ,zv,0);
00595 rel(home,z,r,c,b,icl);
00596 }
00597 }
00598
00599 }}}
00600
00601
00602