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 "gecode/int/bool.hh"
00039 #include "gecode/int/rel.hh"
00040
00041 namespace Gecode {
00042
00043 namespace {
00044
00045 forceinline void
00046 post_and(Space* home, BoolVar x0, BoolVar x1, BoolVar x2) {
00047 using namespace Int;
00048 NegBoolView n0(x0); NegBoolView n1(x1); NegBoolView n2(x2);
00049 GECODE_ES_FAIL(home,(Bool::Or<NegBoolView,NegBoolView,NegBoolView>
00050 ::post(home,n0,n1,n2)));
00051 }
00052 forceinline void
00053 post_or(Space* home, BoolVar x0, BoolVar x1, BoolVar x2) {
00054 using namespace Int;
00055 GECODE_ES_FAIL(home,(Bool::Or<BoolView,BoolView,BoolView>
00056 ::post(home,x0,x1,x2)));
00057 }
00058 forceinline void
00059 post_imp(Space* home, BoolVar x0, BoolVar x1, BoolVar x2) {
00060 using namespace Int;
00061 NegBoolView n0(x0);
00062 GECODE_ES_FAIL(home,(Bool::Or<NegBoolView,BoolView,BoolView>
00063 ::post(home,n0,x1,x2)));
00064 }
00065 forceinline void
00066 post_eqv(Space* home, BoolVar x0, BoolVar x1, BoolVar x2) {
00067 using namespace Int;
00068 GECODE_ES_FAIL(home,(Bool::Eqv<BoolView,BoolView,BoolView>
00069 ::post(home,x0,x1,x2)));
00070 }
00071 forceinline void
00072 post_xor(Space* home, BoolVar x0, BoolVar x1, BoolVar x2) {
00073 using namespace Int;
00074 NegBoolView n2(x2);
00075 GECODE_ES_FAIL(home,(Bool::Eqv<BoolView,BoolView,NegBoolView>
00076 ::post(home,x0,x1,n2)));
00077 }
00078
00079 }
00080
00081 void
00082 rel(Space* home, BoolVar x0, IntRelType r, BoolVar x1,
00083 IntConLevel, PropKind) {
00084 using namespace Int;
00085 if (home->failed()) return;
00086 switch (r) {
00087 case IRT_EQ:
00088 GECODE_ES_FAIL(home,(Bool::Eq<BoolView,BoolView>
00089 ::post(home,x0,x1)));
00090 break;
00091 case IRT_NQ:
00092 {
00093 NegBoolView n1(x1);
00094 GECODE_ES_FAIL(home,(Bool::Eq<BoolView,NegBoolView>
00095 ::post(home,x0,n1)));
00096 }
00097 break;
00098 case IRT_GQ:
00099 GECODE_ES_FAIL(home,Bool::Lq<BoolView>::post(home,x1,x0));
00100 break;
00101 case IRT_LQ:
00102 GECODE_ES_FAIL(home,Bool::Lq<BoolView>::post(home,x0,x1));
00103 break;
00104 case IRT_GR:
00105 GECODE_ES_FAIL(home,Bool::Le<BoolView>::post(home,x1,x0));
00106 break;
00107 case IRT_LE:
00108 GECODE_ES_FAIL(home,Bool::Le<BoolView>::post(home,x0,x1));
00109 break;
00110 default:
00111 throw UnknownRelation("Int::rel");
00112 }
00113 }
00114
00115 void
00116 rel(Space* home, const BoolVarArgs& x, IntRelType r, BoolVar y,
00117 IntConLevel, PropKind) {
00118 using namespace Int;
00119 if (home->failed()) return;
00120 switch (r) {
00121 case IRT_EQ:
00122 for (int i=x.size(); i--; ) {
00123 GECODE_ES_FAIL(home,(Bool::Eq<BoolView,BoolView>
00124 ::post(home,x[i],y)));
00125 }
00126 break;
00127 case IRT_NQ:
00128 {
00129 NegBoolView n(y);
00130 for (int i=x.size(); i--; ) {
00131 GECODE_ES_FAIL(home,(Bool::Eq<BoolView,NegBoolView>
00132 ::post(home,x[i],n)));
00133 }
00134 }
00135 break;
00136 case IRT_GQ:
00137 for (int i=x.size(); i--; ) {
00138 GECODE_ES_FAIL(home,Bool::Lq<BoolView>::post(home,y,x[i]));
00139 }
00140 break;
00141 case IRT_LQ:
00142 for (int i=x.size(); i--; ) {
00143 GECODE_ES_FAIL(home,Bool::Lq<BoolView>::post(home,x[i],y));
00144 }
00145 break;
00146 case IRT_GR:
00147 for (int i=x.size(); i--; ) {
00148 GECODE_ES_FAIL(home,Bool::Le<BoolView>::post(home,y,x[i]));
00149 }
00150 break;
00151 case IRT_LE:
00152 for (int i=x.size(); i--; ) {
00153 GECODE_ES_FAIL(home,Bool::Le<BoolView>::post(home,x[i],y));
00154 }
00155 break;
00156 default:
00157 throw UnknownRelation("Int::rel");
00158 }
00159 }
00160
00161 void
00162 rel(Space* home, BoolVar x0, IntRelType r, int n, IntConLevel, PropKind) {
00163 using namespace Int;
00164 if (home->failed()) return;
00165 BoolView x(x0);
00166 if (n == 0) {
00167 switch (r) {
00168 case IRT_LQ:
00169 case IRT_EQ:
00170 GECODE_ME_FAIL(home,x.zero(home)); break;
00171 case IRT_NQ:
00172 case IRT_GR:
00173 GECODE_ME_FAIL(home,x.one(home)); break;
00174 case IRT_LE:
00175 home->fail(); break;
00176 case IRT_GQ:
00177 break;
00178 default:
00179 throw UnknownRelation("Int::rel");
00180 }
00181 } else if (n == 1) {
00182 switch (r) {
00183 case IRT_GQ:
00184 case IRT_EQ:
00185 GECODE_ME_FAIL(home,x.one(home)); break;
00186 case IRT_NQ:
00187 case IRT_LE:
00188 GECODE_ME_FAIL(home,x.zero(home)); break;
00189 case IRT_GR:
00190 home->fail(); break;
00191 case IRT_LQ:
00192 break;
00193 default:
00194 throw UnknownRelation("Int::rel");
00195 }
00196 } else {
00197 throw NotZeroOne("Int::rel");
00198 }
00199 }
00200
00201 void
00202 rel(Space* home, const BoolVarArgs& x, IntRelType r, int n,
00203 IntConLevel, PropKind) {
00204 using namespace Int;
00205 if (home->failed()) return;
00206 if (n == 0) {
00207 switch (r) {
00208 case IRT_LQ:
00209 case IRT_EQ:
00210 for (int i=x.size(); i--; ) {
00211 BoolView xi(x[i]); GECODE_ME_FAIL(home,xi.zero(home));
00212 }
00213 break;
00214 case IRT_NQ:
00215 case IRT_GR:
00216 for (int i=x.size(); i--; ) {
00217 BoolView xi(x[i]); GECODE_ME_FAIL(home,xi.one(home));
00218 }
00219 break;
00220 case IRT_LE:
00221 home->fail(); break;
00222 case IRT_GQ:
00223 break;
00224 default:
00225 throw UnknownRelation("Int::rel");
00226 }
00227 } else if (n == 1) {
00228 switch (r) {
00229 case IRT_GQ:
00230 case IRT_EQ:
00231 for (int i=x.size(); i--; ) {
00232 BoolView xi(x[i]); GECODE_ME_FAIL(home,xi.one(home));
00233 }
00234 break;
00235 case IRT_NQ:
00236 case IRT_LE:
00237 for (int i=x.size(); i--; ) {
00238 BoolView xi(x[i]); GECODE_ME_FAIL(home,xi.zero(home));
00239 }
00240 break;
00241 case IRT_GR:
00242 home->fail(); break;
00243 case IRT_LQ:
00244 break;
00245 default:
00246 throw UnknownRelation("Int::rel");
00247 }
00248 } else {
00249 throw NotZeroOne("Int::rel");
00250 }
00251 }
00252
00253 void
00254 rel(Space* home, const BoolVarArgs& x, IntRelType r, IntConLevel, PropKind) {
00255 using namespace Int;
00256 if (home->failed() || (x.size() < 2)) return;
00257 switch (r) {
00258 case IRT_EQ:
00259 for (int i=x.size()-1; i--; )
00260 GECODE_ES_FAIL(home,(Bool::Eq<BoolView,BoolView>
00261 ::post(home,x[i],x[i+1])));
00262 break;
00263 case IRT_NQ:
00264 if (x.size() == 2) {
00265 NegBoolView n(x[1]);
00266 GECODE_ES_FAIL(home,(Bool::Eq<BoolView,NegBoolView>
00267 ::post(home,x[0],n)));
00268 } else {
00269 home->fail();
00270 }
00271 break;
00272 case IRT_LE:
00273 if (x.size() == 2) {
00274 GECODE_ES_FAIL(home,Bool::Le<BoolView>::post(home,x[0],x[1]));
00275 } else {
00276 home->fail();
00277 }
00278 break;
00279 case IRT_LQ:
00280 for (int i=x.size()-1; i--; )
00281 GECODE_ES_FAIL(home,Bool::Lq<BoolView>::post(home,x[i],x[i+1]));
00282 break;
00283 case IRT_GR:
00284 if (x.size() == 2) {
00285 GECODE_ES_FAIL(home,Bool::Le<BoolView>::post(home,x[1],x[0]));
00286 } else {
00287 home->fail();
00288 }
00289 break;
00290 case IRT_GQ:
00291 for (int i=x.size()-1; i--; )
00292 GECODE_ES_FAIL(home,Bool::Lq<BoolView>::post(home,x[i+1],x[i]));
00293 break;
00294 default:
00295 throw UnknownRelation("Int::rel");
00296 }
00297 }
00298
00299 void
00300 rel(Space* home, const BoolVarArgs& x, IntRelType r, const BoolVarArgs& y,
00301 IntConLevel, PropKind) {
00302 using namespace Int;
00303 if (x.size() != y.size())
00304 throw ArgumentSizeMismatch("Int::rel");
00305 if (home->failed()) return;
00306
00307 switch (r) {
00308 case IRT_GR:
00309 {
00310 ViewArray<ViewTuple<BoolView,2> > xy(home,x.size());
00311 for (int i = x.size(); i--; ) {
00312 xy[i][0]=y[i]; xy[i][1]=x[i];
00313 }
00314 GECODE_ES_FAIL(home,Rel::Lex<BoolView>::post(home,xy,true));
00315 }
00316 break;
00317 case IRT_LE:
00318 {
00319 ViewArray<ViewTuple<BoolView,2> > xy(home,x.size());
00320 for (int i = x.size(); i--; ) {
00321 xy[i][0]=x[i]; xy[i][1]=y[i];
00322 }
00323 GECODE_ES_FAIL(home,Rel::Lex<BoolView>::post(home,xy,true));
00324 }
00325 break;
00326 case IRT_GQ:
00327 {
00328 ViewArray<ViewTuple<BoolView,2> > xy(home,x.size());
00329 for (int i = x.size(); i--; ) {
00330 xy[i][0]=y[i]; xy[i][1]=x[i];
00331 }
00332 GECODE_ES_FAIL(home,Rel::Lex<BoolView>::post(home,xy,false));
00333 }
00334 break;
00335 case IRT_LQ:
00336 {
00337 ViewArray<ViewTuple<BoolView,2> > xy(home,x.size());
00338 for (int i = x.size(); i--; ) {
00339 xy[i][0]=x[i]; xy[i][1]=y[i];
00340 }
00341 GECODE_ES_FAIL(home,Rel::Lex<BoolView>::post(home,xy,false));
00342 }
00343 break;
00344 case IRT_EQ:
00345 for (int i=x.size(); i--; ) {
00346 GECODE_ES_FAIL(home,(Bool::Eq<BoolView,BoolView>
00347 ::post(home,x[i],y[i])));
00348 }
00349 break;
00350 case IRT_NQ:
00351 {
00352 ViewArray<ViewTuple<BoolView,2> > xy(home,x.size());
00353 for (int i = x.size(); i--; ) {
00354 xy[i][0]=x[i]; xy[i][1]=y[i];
00355 }
00356 GECODE_ES_FAIL(home,Rel::NaryNq<BoolView>::post(home,xy));
00357 }
00358 break;
00359 default:
00360 throw UnknownRelation("Int::rel");
00361 }
00362 }
00363
00364 void
00365 rel(Space* home, BoolVar x0, BoolOpType o, BoolVar x1, BoolVar x2,
00366 IntConLevel, PropKind) {
00367 using namespace Int;
00368 if (home->failed()) return;
00369 switch (o) {
00370 case BOT_AND: post_and(home,x0,x1,x2); break;
00371 case BOT_OR: post_or(home,x0,x1,x2); break;
00372 case BOT_IMP: post_imp(home,x0,x1,x2); break;
00373 case BOT_EQV: post_eqv(home,x0,x1,x2); break;
00374 case BOT_XOR: post_xor(home,x0,x1,x2); break;
00375 default: throw UnknownBoolOp("Int::rel");
00376 }
00377 }
00378
00379 void
00380 rel(Space* home, BoolVar x0, BoolOpType o, BoolVar x1, int n,
00381 IntConLevel, PropKind) {
00382 using namespace Int;
00383 if (home->failed()) return;
00384 if (n == 0) {
00385 switch (o) {
00386 case BOT_AND:
00387 {
00388 NegBoolView n0(x0); NegBoolView n1(x1);
00389 GECODE_ES_FAIL(home,(Bool::BinOrTrue<NegBoolView,NegBoolView>
00390 ::post(home,n0,n1)));
00391 }
00392 break;
00393 case BOT_OR:
00394 {
00395 BoolView b0(x0); BoolView b1(x1);
00396 GECODE_ME_FAIL(home,b0.zero(home));
00397 GECODE_ME_FAIL(home,b1.zero(home));
00398 }
00399 break;
00400 case BOT_IMP:
00401 {
00402 BoolView b0(x0); BoolView b1(x1);
00403 GECODE_ME_FAIL(home,b0.one(home));
00404 GECODE_ME_FAIL(home,b1.zero(home));
00405 }
00406 break;
00407 case BOT_EQV:
00408 {
00409 NegBoolView n0(x0);
00410 GECODE_ES_FAIL(home,(Bool::Eq<NegBoolView,BoolView>
00411 ::post(home,n0,x1)));
00412 }
00413 break;
00414 case BOT_XOR:
00415 GECODE_ES_FAIL(home,(Bool::Eq<BoolView,BoolView>
00416 ::post(home,x0,x1)));
00417 break;
00418 default:
00419 throw UnknownBoolOp("Int::rel");
00420 }
00421 } else if (n == 1) {
00422 switch (o) {
00423 case BOT_AND:
00424 {
00425 BoolView b0(x0); BoolView b1(x1);
00426 GECODE_ME_FAIL(home,b0.one(home));
00427 GECODE_ME_FAIL(home,b1.one(home));
00428 }
00429 break;
00430 case BOT_OR:
00431 GECODE_ES_FAIL(home,(Bool::BinOrTrue<BoolView,BoolView>
00432 ::post(home,x0,x1)));
00433 break;
00434 case BOT_IMP:
00435 {
00436 NegBoolView n0(x0);
00437 GECODE_ES_FAIL(home,(Bool::BinOrTrue<NegBoolView,BoolView>
00438 ::post(home,n0,x1)));
00439 }
00440 break;
00441 case BOT_EQV:
00442 GECODE_ES_FAIL(home,(Bool::Eq<BoolView,BoolView>
00443 ::post(home,x0,x1)));
00444 break;
00445 case BOT_XOR:
00446 {
00447 NegBoolView n0(x0);
00448 GECODE_ES_FAIL(home,(Bool::Eq<NegBoolView,BoolView>
00449 ::post(home,n0,x1)));
00450 }
00451 break;
00452 default:
00453 throw UnknownBoolOp("Int::rel");
00454 }
00455 } else {
00456 throw NotZeroOne("Int::rel");
00457 }
00458 }
00459
00460 void
00461 rel(Space* home, BoolOpType o, const BoolVarArgs& x, BoolVar y,
00462 IntConLevel, PropKind) {
00463 using namespace Int;
00464 if (home->failed()) return;
00465 int m = x.size();
00466 switch (o) {
00467 case BOT_AND:
00468 {
00469 ViewArray<NegBoolView> b(home,m);
00470 for (int i=m; i--; ) {
00471 NegBoolView nb(x[i]); b[i]=nb;
00472 }
00473 NegBoolView ny(y);
00474 b.unique();
00475 GECODE_ES_FAIL(home,Bool::NaryOr<NegBoolView>::post(home,b,ny));
00476 }
00477 break;
00478 case BOT_OR:
00479 {
00480 ViewArray<BoolView> b(home,x);
00481 b.unique();
00482 GECODE_ES_FAIL(home,Bool::NaryOr<BoolView>::post(home,b,y));
00483 }
00484 break;
00485 case BOT_IMP:
00486 if (m < 2) {
00487 throw TooFewArguments("Int::rel");
00488 } else {
00489 GECODE_AUTOARRAY(BoolVar,z,m);
00490 z[0]=x[0]; z[m-1]=y;
00491 for (int i=1; i<m-1; i++)
00492 z[i].init(home,0,1);
00493 for (int i=1; i<m; i++)
00494 post_imp(home,z[i-1],x[i],z[i]);
00495 }
00496 break;
00497 case BOT_EQV:
00498 if (m < 2) {
00499 throw TooFewArguments("Int::rel");
00500 } else {
00501 GECODE_AUTOARRAY(BoolVar,z,m);
00502 z[0]=x[0]; z[m-1]=y;
00503 for (int i=1; i<m-1; i++)
00504 z[i].init(home,0,1);
00505 for (int i=1; i<m; i++)
00506 post_eqv(home,z[i-1],x[i],z[i]);
00507 }
00508 break;
00509 case BOT_XOR:
00510 if (m < 2) {
00511 throw TooFewArguments("Int::rel");
00512 } else {
00513 GECODE_AUTOARRAY(BoolVar,z,m);
00514 z[0]=x[0]; z[m-1]=y;
00515 for (int i=1; i<m-1; i++)
00516 z[i].init(home,0,1);
00517 for (int i=1; i<m; i++)
00518 post_xor(home,z[i-1],x[i],z[i]);
00519 }
00520 break;
00521 default:
00522 throw UnknownBoolOp("Int::rel");
00523 }
00524 }
00525
00526 void
00527 rel(Space* home, BoolOpType o, const BoolVarArgs& x, int n,
00528 IntConLevel, PropKind) {
00529 using namespace Int;
00530 if ((n < 0) || (n > 1))
00531 throw NotZeroOne("Int::rel");
00532 if (home->failed()) return;
00533 int m = x.size();
00534 switch (o) {
00535 case BOT_AND:
00536 if (n == 0) {
00537 ViewArray<NegBoolView> b(home,m);
00538 for (int i=m; i--; ) {
00539 NegBoolView nb(x[i]); b[i]=nb;
00540 }
00541 b.unique();
00542 GECODE_ES_FAIL(home,Bool::NaryOrTrue<NegBoolView>::post(home,b));
00543 } else {
00544 for (int i=m; i--; ) {
00545 BoolView b(x[i]); GECODE_ME_FAIL(home,b.one(home));
00546 }
00547 }
00548 break;
00549 case BOT_OR:
00550 if (n == 0) {
00551 for (int i=m; i--; ) {
00552 BoolView b(x[i]); GECODE_ME_FAIL(home,b.zero(home));
00553 }
00554 } else {
00555 ViewArray<BoolView> b(home,x);
00556 b.unique();
00557 GECODE_ES_FAIL(home,Bool::NaryOrTrue<BoolView>::post(home,b));
00558 }
00559 break;
00560 case BOT_IMP:
00561 if (m < 2) {
00562 throw TooFewArguments("Int::rel");
00563 } else {
00564 GECODE_AUTOARRAY(BoolVar,z,m);
00565 z[0]=x[0]; z[m-1].init(home,n,n);;
00566 for (int i=1; i<m-1; i++)
00567 z[i].init(home,0,1);
00568 for (int i=1; i<m; i++)
00569 post_imp(home,z[i-1],x[i],z[i]);
00570 }
00571 break;
00572 case BOT_EQV:
00573 if (m < 2) {
00574 throw TooFewArguments("Int::rel");
00575 } else {
00576 GECODE_AUTOARRAY(BoolVar,z,m);
00577 z[0]=x[0]; z[m-1].init(home,n,n);
00578 for (int i=1; i<m-1; i++)
00579 z[i].init(home,0,1);
00580 for (int i=1; i<m; i++)
00581 post_eqv(home,z[i-1],x[i],z[i]);
00582 }
00583 break;
00584 case BOT_XOR:
00585 if (m < 2) {
00586 throw TooFewArguments("Int::rel");
00587 } else {
00588 GECODE_AUTOARRAY(BoolVar,z,m);
00589 z[0]=x[0]; z[m-1].init(home,n,n);
00590 for (int i=1; i<m-1; i++)
00591 z[i].init(home,0,1);
00592 for (int i=1; i<m; i++)
00593 post_xor(home,z[i-1],x[i],z[i]);
00594 }
00595 break;
00596 default:
00597 throw UnknownBoolOp("Int::rel");
00598 }
00599 }
00600
00601 namespace {
00602 using namespace Int;
00603 GECODE_REGISTER2(Bool::BinOrTrue<NegBoolView, BoolView>);
00604 GECODE_REGISTER2(Bool::BinOrTrue<NegBoolView, NegBoolView>);
00605 GECODE_REGISTER2(Bool::BinOrTrue<BoolView, BoolView>);
00606
00607 GECODE_REGISTER2(Bool::Eq<NegBoolView, BoolView>);
00608 GECODE_REGISTER2(Bool::Eq<NegBoolView, NegBoolView>);
00609 GECODE_REGISTER2(Bool::Eq<BoolView, NegBoolView>);
00610 GECODE_REGISTER2(Bool::Eq<BoolView, BoolView>);
00611 GECODE_REGISTER1(Bool::NaryEq<BoolView>);
00612
00613 GECODE_REGISTER3(Bool::Eqv<BoolView, BoolView, NegBoolView>);
00614 GECODE_REGISTER3(Bool::Eqv<BoolView, BoolView, BoolView>);
00615
00616 GECODE_REGISTER1(Bool::Lq<BoolView>);
00617
00618 GECODE_REGISTER1(Bool::NaryOr<NegBoolView>);
00619 GECODE_REGISTER1(Bool::NaryOr<BoolView>);
00620
00621 GECODE_REGISTER1(Bool::NaryOrTrue<NegBoolView>);
00622 GECODE_REGISTER1(Bool::NaryOrTrue<BoolView>);
00623
00624 GECODE_REGISTER3(Bool::Or<NegBoolView, BoolView, BoolView>);
00625 GECODE_REGISTER3(Bool::Or<NegBoolView, NegBoolView, NegBoolView>);
00626 GECODE_REGISTER3(Bool::Or<BoolView, BoolView, BoolView>);
00627
00628 GECODE_REGISTER1(Bool::OrTrueSubsumed<NegBoolView>);
00629 GECODE_REGISTER1(Bool::OrTrueSubsumed<BoolView>);
00630
00631 GECODE_REGISTER1(Bool::QuadOrTrue<NegBoolView>);
00632 GECODE_REGISTER1(Bool::QuadOrTrue<BoolView>);
00633
00634 GECODE_REGISTER1(Bool::TerOrTrue<NegBoolView>);
00635 GECODE_REGISTER1(Bool::TerOrTrue<BoolView>);
00636 }
00637
00638 }
00639
00640
00641
00642