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(Home 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(Home 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(Home 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(Home 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(Home 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(Home home, BoolVar x0, IntRelType r, BoolVar x1, IntConLevel) {
00083 using namespace Int;
00084 if (home.failed()) return;
00085 switch (r) {
00086 case IRT_EQ:
00087 GECODE_ES_FAIL(home,(Bool::Eq<BoolView,BoolView>
00088 ::post(home,x0,x1)));
00089 break;
00090 case IRT_NQ:
00091 {
00092 NegBoolView n1(x1);
00093 GECODE_ES_FAIL(home,(Bool::Eq<BoolView,NegBoolView>
00094 ::post(home,x0,n1)));
00095 }
00096 break;
00097 case IRT_GQ:
00098 GECODE_ES_FAIL(home,Bool::Lq<BoolView>::post(home,x1,x0));
00099 break;
00100 case IRT_LQ:
00101 GECODE_ES_FAIL(home,Bool::Lq<BoolView>::post(home,x0,x1));
00102 break;
00103 case IRT_GR:
00104 GECODE_ES_FAIL(home,Bool::Le<BoolView>::post(home,x1,x0));
00105 break;
00106 case IRT_LE:
00107 GECODE_ES_FAIL(home,Bool::Le<BoolView>::post(home,x0,x1));
00108 break;
00109 default:
00110 throw UnknownRelation("Int::rel");
00111 }
00112 }
00113
00114 void
00115 rel(Home home, BoolVar x0, IntRelType r, int n, IntConLevel) {
00116 using namespace Int;
00117 if (home.failed()) return;
00118 BoolView x(x0);
00119 if (n == 0) {
00120 switch (r) {
00121 case IRT_LQ:
00122 case IRT_EQ:
00123 GECODE_ME_FAIL(home,x.zero(home)); break;
00124 case IRT_NQ:
00125 case IRT_GR:
00126 GECODE_ME_FAIL(home,x.one(home)); break;
00127 case IRT_LE:
00128 home.fail(); break;
00129 case IRT_GQ:
00130 break;
00131 default:
00132 throw UnknownRelation("Int::rel");
00133 }
00134 } else if (n == 1) {
00135 switch (r) {
00136 case IRT_GQ:
00137 case IRT_EQ:
00138 GECODE_ME_FAIL(home,x.one(home)); break;
00139 case IRT_NQ:
00140 case IRT_LE:
00141 GECODE_ME_FAIL(home,x.zero(home)); break;
00142 case IRT_GR:
00143 home.fail(); break;
00144 case IRT_LQ:
00145 break;
00146 default:
00147 throw UnknownRelation("Int::rel");
00148 }
00149 } else {
00150 throw NotZeroOne("Int::rel");
00151 }
00152 }
00153
00154 void
00155 rel(Home home, BoolVar x0, IntRelType r, BoolVar x1, BoolVar b,
00156 IntConLevel) {
00157 using namespace Int;
00158 if (home.failed()) return;
00159 switch (r) {
00160 case IRT_EQ:
00161 GECODE_ES_FAIL(home,(Bool::Eqv<BoolView,BoolView,BoolView>
00162 ::post(home,x0,x1,b)));
00163 break;
00164 case IRT_NQ:
00165 {
00166 NegBoolView n(b);
00167 GECODE_ES_FAIL(home,(Bool::Eqv<BoolView,BoolView,NegBoolView>
00168 ::post(home,x0,x1,n)));
00169 }
00170 break;
00171 case IRT_GQ:
00172 std::swap(x0,x1);
00173 case IRT_LQ:
00174 {
00175 NegBoolView n0(x0);
00176 GECODE_ES_FAIL(home,(Bool::Or<NegBoolView,BoolView,BoolView>
00177 ::post(home,n0,x1,b)));
00178 }
00179 break;
00180 case IRT_GR:
00181 std::swap(x0,x1);
00182 case IRT_LE:
00183 {
00184 NegBoolView n1(x1), n(b);
00185 GECODE_ES_FAIL(home,(Bool::Or<BoolView,NegBoolView,NegBoolView>
00186 ::post(home,x0,n1,n)));
00187 }
00188 break;
00189 default:
00190 throw UnknownRelation("Int::rel");
00191 }
00192 }
00193
00194 void
00195 rel(Home home, BoolVar x0, IntRelType r, int n, BoolVar b,
00196 IntConLevel) {
00197 using namespace Int;
00198 if (home.failed()) return;
00199 BoolView x(x0);
00200 BoolView y(b);
00201 if (n == 0) {
00202 switch (r) {
00203 case IRT_LQ:
00204 case IRT_EQ:
00205 {
00206 NegBoolView z(y);
00207 GECODE_ES_FAIL(home,(Bool::Eq<BoolView,NegBoolView>
00208 ::post(home,x,z)));
00209 }
00210 break;
00211 case IRT_NQ:
00212 case IRT_GR:
00213 GECODE_ES_FAIL(home,(Bool::Eq<BoolView,BoolView>
00214 ::post(home,x,y)));
00215 break;
00216 case IRT_LE:
00217 GECODE_ME_FAIL(home,y.zero(home));
00218 break;
00219 case IRT_GQ:
00220 GECODE_ME_FAIL(home,y.one(home));
00221 break;
00222 default:
00223 throw UnknownRelation("Int::rel");
00224 }
00225 } else if (n == 1) {
00226 switch (r) {
00227 case IRT_GQ:
00228 case IRT_EQ:
00229 GECODE_ES_FAIL(home,(Bool::Eq<BoolView,BoolView>
00230 ::post(home,x,y)));
00231 break;
00232 case IRT_NQ:
00233 case IRT_LE:
00234 {
00235 NegBoolView z(y);
00236 GECODE_ES_FAIL(home,(Bool::Eq<BoolView,NegBoolView>
00237 ::post(home,x,z)));
00238 }
00239 break;
00240 case IRT_GR:
00241 GECODE_ME_FAIL(home,y.zero(home));
00242 break;
00243 case IRT_LQ:
00244 GECODE_ME_FAIL(home,y.one(home));
00245 break;
00246 default:
00247 throw UnknownRelation("Int::rel");
00248 }
00249 } else {
00250 throw NotZeroOne("Int::rel");
00251 }
00252 }
00253
00254 void
00255 rel(Home home, const BoolVarArgs& x, IntRelType r, BoolVar y,
00256 IntConLevel) {
00257 using namespace Int;
00258 if (home.failed()) return;
00259 switch (r) {
00260 case IRT_EQ:
00261 for (int i=x.size(); i--; ) {
00262 GECODE_ES_FAIL(home,(Bool::Eq<BoolView,BoolView>
00263 ::post(home,x[i],y)));
00264 }
00265 break;
00266 case IRT_NQ:
00267 {
00268 NegBoolView n(y);
00269 for (int i=x.size(); i--; ) {
00270 GECODE_ES_FAIL(home,(Bool::Eq<BoolView,NegBoolView>
00271 ::post(home,x[i],n)));
00272 }
00273 }
00274 break;
00275 case IRT_GQ:
00276 for (int i=x.size(); i--; ) {
00277 GECODE_ES_FAIL(home,Bool::Lq<BoolView>::post(home,y,x[i]));
00278 }
00279 break;
00280 case IRT_LQ:
00281 for (int i=x.size(); i--; ) {
00282 GECODE_ES_FAIL(home,Bool::Lq<BoolView>::post(home,x[i],y));
00283 }
00284 break;
00285 case IRT_GR:
00286 for (int i=x.size(); i--; ) {
00287 GECODE_ES_FAIL(home,Bool::Le<BoolView>::post(home,y,x[i]));
00288 }
00289 break;
00290 case IRT_LE:
00291 for (int i=x.size(); i--; ) {
00292 GECODE_ES_FAIL(home,Bool::Le<BoolView>::post(home,x[i],y));
00293 }
00294 break;
00295 default:
00296 throw UnknownRelation("Int::rel");
00297 }
00298 }
00299
00300 void
00301 rel(Home home, const BoolVarArgs& x, IntRelType r, int n,
00302 IntConLevel) {
00303 using namespace Int;
00304 if (home.failed()) return;
00305 if (n == 0) {
00306 switch (r) {
00307 case IRT_LQ:
00308 case IRT_EQ:
00309 for (int i=x.size(); i--; ) {
00310 BoolView xi(x[i]); GECODE_ME_FAIL(home,xi.zero(home));
00311 }
00312 break;
00313 case IRT_NQ:
00314 case IRT_GR:
00315 for (int i=x.size(); i--; ) {
00316 BoolView xi(x[i]); GECODE_ME_FAIL(home,xi.one(home));
00317 }
00318 break;
00319 case IRT_LE:
00320 home.fail(); break;
00321 case IRT_GQ:
00322 break;
00323 default:
00324 throw UnknownRelation("Int::rel");
00325 }
00326 } else if (n == 1) {
00327 switch (r) {
00328 case IRT_GQ:
00329 case IRT_EQ:
00330 for (int i=x.size(); i--; ) {
00331 BoolView xi(x[i]); GECODE_ME_FAIL(home,xi.one(home));
00332 }
00333 break;
00334 case IRT_NQ:
00335 case IRT_LE:
00336 for (int i=x.size(); i--; ) {
00337 BoolView xi(x[i]); GECODE_ME_FAIL(home,xi.zero(home));
00338 }
00339 break;
00340 case IRT_GR:
00341 home.fail(); break;
00342 case IRT_LQ:
00343 break;
00344 default:
00345 throw UnknownRelation("Int::rel");
00346 }
00347 } else {
00348 throw NotZeroOne("Int::rel");
00349 }
00350 }
00351
00352 void
00353 rel(Home home, const BoolVarArgs& x, IntRelType r, IntConLevel) {
00354 using namespace Int;
00355 if (home.failed() || (x.size() < 2)) return;
00356 switch (r) {
00357 case IRT_EQ:
00358 for (int i=x.size()-1; i--; )
00359 GECODE_ES_FAIL(home,(Bool::Eq<BoolView,BoolView>
00360 ::post(home,x[i],x[i+1])));
00361 break;
00362 case IRT_NQ:
00363 if (x.size() == 2) {
00364 NegBoolView n(x[1]);
00365 GECODE_ES_FAIL(home,(Bool::Eq<BoolView,NegBoolView>
00366 ::post(home,x[0],n)));
00367 } else {
00368 home.fail();
00369 }
00370 break;
00371 case IRT_LE:
00372 if (x.size() == 2) {
00373 GECODE_ES_FAIL(home,Bool::Le<BoolView>::post(home,x[0],x[1]));
00374 } else {
00375 home.fail();
00376 }
00377 break;
00378 case IRT_LQ:
00379 for (int i=x.size()-1; i--; )
00380 GECODE_ES_FAIL(home,Bool::Lq<BoolView>::post(home,x[i],x[i+1]));
00381 break;
00382 case IRT_GR:
00383 if (x.size() == 2) {
00384 GECODE_ES_FAIL(home,Bool::Le<BoolView>::post(home,x[1],x[0]));
00385 } else {
00386 home.fail();
00387 }
00388 break;
00389 case IRT_GQ:
00390 for (int i=x.size()-1; i--; )
00391 GECODE_ES_FAIL(home,Bool::Lq<BoolView>::post(home,x[i+1],x[i]));
00392 break;
00393 default:
00394 throw UnknownRelation("Int::rel");
00395 }
00396 }
00397
00398 void
00399 rel(Home home, const BoolVarArgs& x, IntRelType r, const BoolVarArgs& y,
00400 IntConLevel) {
00401 using namespace Int;
00402 if (x.size() != y.size())
00403 throw ArgumentSizeMismatch("Int::rel");
00404 if (home.failed()) return;
00405
00406 switch (r) {
00407 case IRT_GR:
00408 {
00409 ViewArray<BoolView> xv(home,x), yv(home,y);
00410 GECODE_ES_FAIL(home,Rel::Lex<BoolView>::post(home,yv,xv,true));
00411 }
00412 break;
00413 case IRT_LE:
00414 {
00415 ViewArray<BoolView> xv(home,x), yv(home,y);
00416 GECODE_ES_FAIL(home,Rel::Lex<BoolView>::post(home,xv,yv,true));
00417 }
00418 break;
00419 case IRT_GQ:
00420 {
00421 ViewArray<BoolView> xv(home,x), yv(home,y);
00422 GECODE_ES_FAIL(home,Rel::Lex<BoolView>::post(home,yv,xv,false));
00423 }
00424 break;
00425 case IRT_LQ:
00426 {
00427 ViewArray<BoolView> xv(home,x), yv(home,y);
00428 GECODE_ES_FAIL(home,Rel::Lex<BoolView>::post(home,xv,yv,false));
00429 }
00430 break;
00431 case IRT_EQ:
00432 for (int i=x.size(); i--; ) {
00433 GECODE_ES_FAIL(home,(Bool::Eq<BoolView,BoolView>
00434 ::post(home,x[i],y[i])));
00435 }
00436 break;
00437 case IRT_NQ:
00438 {
00439 ViewArray<BoolView> b(home,x.size());
00440 for (int i=x.size(); i--; ) {
00441 BoolVar bi(home,0,1); b[i]=bi;
00442 NegBoolView n(b[i]);
00443 GECODE_ES_FAIL(home,(Bool::Eqv<BoolView,BoolView,NegBoolView>
00444 ::post(home,x[i],y[i],n)));
00445 }
00446 GECODE_ES_FAIL(home,Bool::NaryOrTrue<BoolView>::post(home,b));
00447 }
00448 break;
00449 default:
00450 throw UnknownRelation("Int::rel");
00451 }
00452 }
00453
00454 void
00455 rel(Home home, BoolVar x0, BoolOpType o, BoolVar x1, BoolVar x2,
00456 IntConLevel) {
00457 using namespace Int;
00458 if (home.failed()) return;
00459 switch (o) {
00460 case BOT_AND: post_and(home,x0,x1,x2); break;
00461 case BOT_OR: post_or(home,x0,x1,x2); break;
00462 case BOT_IMP: post_imp(home,x0,x1,x2); break;
00463 case BOT_EQV: post_eqv(home,x0,x1,x2); break;
00464 case BOT_XOR: post_xor(home,x0,x1,x2); break;
00465 default: throw UnknownOperation("Int::rel");
00466 }
00467 }
00468
00469 void
00470 rel(Home home, BoolVar x0, BoolOpType o, BoolVar x1, int n,
00471 IntConLevel) {
00472 using namespace Int;
00473 if (home.failed()) return;
00474 if (n == 0) {
00475 switch (o) {
00476 case BOT_AND:
00477 {
00478 NegBoolView n0(x0); NegBoolView n1(x1);
00479 GECODE_ES_FAIL(home,(Bool::BinOrTrue<NegBoolView,NegBoolView>
00480 ::post(home,n0,n1)));
00481 }
00482 break;
00483 case BOT_OR:
00484 {
00485 BoolView b0(x0); BoolView b1(x1);
00486 GECODE_ME_FAIL(home,b0.zero(home));
00487 GECODE_ME_FAIL(home,b1.zero(home));
00488 }
00489 break;
00490 case BOT_IMP:
00491 {
00492 BoolView b0(x0); BoolView b1(x1);
00493 GECODE_ME_FAIL(home,b0.one(home));
00494 GECODE_ME_FAIL(home,b1.zero(home));
00495 }
00496 break;
00497 case BOT_EQV:
00498 {
00499 NegBoolView n0(x0);
00500 GECODE_ES_FAIL(home,(Bool::Eq<NegBoolView,BoolView>
00501 ::post(home,n0,x1)));
00502 }
00503 break;
00504 case BOT_XOR:
00505 GECODE_ES_FAIL(home,(Bool::Eq<BoolView,BoolView>
00506 ::post(home,x0,x1)));
00507 break;
00508 default:
00509 throw UnknownOperation("Int::rel");
00510 }
00511 } else if (n == 1) {
00512 switch (o) {
00513 case BOT_AND:
00514 {
00515 BoolView b0(x0); BoolView b1(x1);
00516 GECODE_ME_FAIL(home,b0.one(home));
00517 GECODE_ME_FAIL(home,b1.one(home));
00518 }
00519 break;
00520 case BOT_OR:
00521 GECODE_ES_FAIL(home,(Bool::BinOrTrue<BoolView,BoolView>
00522 ::post(home,x0,x1)));
00523 break;
00524 case BOT_IMP:
00525 {
00526 NegBoolView n0(x0);
00527 GECODE_ES_FAIL(home,(Bool::BinOrTrue<NegBoolView,BoolView>
00528 ::post(home,n0,x1)));
00529 }
00530 break;
00531 case BOT_EQV:
00532 GECODE_ES_FAIL(home,(Bool::Eq<BoolView,BoolView>
00533 ::post(home,x0,x1)));
00534 break;
00535 case BOT_XOR:
00536 {
00537 NegBoolView n0(x0);
00538 GECODE_ES_FAIL(home,(Bool::Eq<NegBoolView,BoolView>
00539 ::post(home,n0,x1)));
00540 }
00541 break;
00542 default:
00543 throw UnknownOperation("Int::rel");
00544 }
00545 } else {
00546 throw NotZeroOne("Int::rel");
00547 }
00548 }
00549
00550 void
00551 rel(Home home, BoolOpType o, const BoolVarArgs& x, BoolVar y,
00552 IntConLevel) {
00553 using namespace Int;
00554 if (home.failed()) return;
00555 int m = x.size();
00556 Region r(home);
00557 switch (o) {
00558 case BOT_AND:
00559 {
00560 ViewArray<NegBoolView> b(home,m);
00561 for (int i=m; i--; ) {
00562 NegBoolView nb(x[i]); b[i]=nb;
00563 }
00564 NegBoolView ny(y);
00565 b.unique(home);
00566 GECODE_ES_FAIL(home,(Bool::NaryOr<NegBoolView,NegBoolView>
00567 ::post(home,b,ny)));
00568 }
00569 break;
00570 case BOT_OR:
00571 {
00572 ViewArray<BoolView> b(home,x);
00573 b.unique(home);
00574 GECODE_ES_FAIL(home,(Bool::NaryOr<BoolView,BoolView>::post(home,b,y)));
00575 }
00576 break;
00577 case BOT_IMP:
00578 if (m < 2) {
00579 throw TooFewArguments("Int::rel");
00580 } else {
00581 BoolVar* z = r.alloc<BoolVar>(m);
00582 z[0]=x[0]; z[m-1]=y;
00583 for (int i=1; i<m-1; i++)
00584 z[i].init(home,0,1);
00585 for (int i=1; i<m; i++)
00586 post_imp(home,z[i-1],x[i],z[i]);
00587 }
00588 break;
00589 case BOT_EQV:
00590 if (m < 2) {
00591 throw TooFewArguments("Int::rel");
00592 } else {
00593 BoolVar* z = r.alloc<BoolVar>(m);
00594 z[0]=x[0]; z[m-1]=y;
00595 for (int i=1; i<m-1; i++)
00596 z[i].init(home,0,1);
00597 for (int i=1; i<m; i++)
00598 post_eqv(home,z[i-1],x[i],z[i]);
00599 }
00600 break;
00601 case BOT_XOR:
00602 if (m < 2) {
00603 throw TooFewArguments("Int::rel");
00604 } else {
00605 BoolVar* z = r.alloc<BoolVar>(m);
00606 z[0]=x[0]; z[m-1]=y;
00607 for (int i=1; i<m-1; i++)
00608 z[i].init(home,0,1);
00609 for (int i=1; i<m; i++)
00610 post_xor(home,z[i-1],x[i],z[i]);
00611 }
00612 break;
00613 default:
00614 throw UnknownOperation("Int::rel");
00615 }
00616 }
00617
00618 void
00619 rel(Home home, BoolOpType o, const BoolVarArgs& x, int n,
00620 IntConLevel) {
00621 using namespace Int;
00622 if ((n < 0) || (n > 1))
00623 throw NotZeroOne("Int::rel");
00624 if (home.failed()) return;
00625 int m = x.size();
00626 Region r(home);
00627 switch (o) {
00628 case BOT_AND:
00629 if (n == 0) {
00630 ViewArray<NegBoolView> b(home,m);
00631 for (int i=m; i--; ) {
00632 NegBoolView nb(x[i]); b[i]=nb;
00633 }
00634 b.unique(home);
00635 GECODE_ES_FAIL(home,Bool::NaryOrTrue<NegBoolView>::post(home,b));
00636 } else {
00637 for (int i=m; i--; ) {
00638 BoolView b(x[i]); GECODE_ME_FAIL(home,b.one(home));
00639 }
00640 }
00641 break;
00642 case BOT_OR:
00643 if (n == 0) {
00644 for (int i=m; i--; ) {
00645 BoolView b(x[i]); GECODE_ME_FAIL(home,b.zero(home));
00646 }
00647 } else {
00648 ViewArray<BoolView> b(home,x);
00649 b.unique(home);
00650 GECODE_ES_FAIL(home,Bool::NaryOrTrue<BoolView>::post(home,b));
00651 }
00652 break;
00653 case BOT_IMP:
00654 if (m < 2) {
00655 throw TooFewArguments("Int::rel");
00656 } else {
00657 BoolVar* z = r.alloc<BoolVar>(m);
00658 z[0]=x[0]; z[m-1].init(home,n,n);;
00659 for (int i=1; i<m-1; i++)
00660 z[i].init(home,0,1);
00661 for (int i=1; i<m; i++)
00662 post_imp(home,z[i-1],x[i],z[i]);
00663 }
00664 break;
00665 case BOT_EQV:
00666 if (m < 2) {
00667 throw TooFewArguments("Int::rel");
00668 } else {
00669 BoolVar* z = r.alloc<BoolVar>(m);
00670 z[0]=x[0]; z[m-1].init(home,n,n);
00671 for (int i=1; i<m-1; i++)
00672 z[i].init(home,0,1);
00673 for (int i=1; i<m; i++)
00674 post_eqv(home,z[i-1],x[i],z[i]);
00675 }
00676 break;
00677 case BOT_XOR:
00678 if (m < 2) {
00679 throw TooFewArguments("Int::rel");
00680 } else {
00681 BoolVar* z = r.alloc<BoolVar>(m);
00682 z[0]=x[0]; z[m-1].init(home,n,n);
00683 for (int i=1; i<m-1; i++)
00684 z[i].init(home,0,1);
00685 for (int i=1; i<m; i++)
00686 post_xor(home,z[i-1],x[i],z[i]);
00687 }
00688 break;
00689 default:
00690 throw UnknownOperation("Int::rel");
00691 }
00692 }
00693
00694 void
00695 clause(Home home, BoolOpType o, const BoolVarArgs& x, const BoolVarArgs& y,
00696 int n, IntConLevel) {
00697 using namespace Int;
00698 if ((n < 0) || (n > 1))
00699 throw NotZeroOne("Int::rel");
00700 if (home.failed()) return;
00701 switch (o) {
00702 case BOT_AND:
00703 if (n == 0) {
00704 ViewArray<NegBoolView> xv(home,x.size());
00705 for (int i=x.size(); i--; ) {
00706 NegBoolView n(x[i]); xv[i]=n;
00707 }
00708 ViewArray<BoolView> yv(home,y);
00709 xv.unique(home); yv.unique(home);
00710 GECODE_ES_FAIL(home,(Bool::ClauseTrue<NegBoolView,BoolView>
00711 ::post(home,xv,yv)));
00712 } else {
00713 for (int i=x.size(); i--; ) {
00714 BoolView b(x[i]); GECODE_ME_FAIL(home,b.one(home));
00715 }
00716 for (int i=y.size(); i--; ) {
00717 BoolView b(y[i]); GECODE_ME_FAIL(home,b.zero(home));
00718 }
00719 }
00720 break;
00721 case BOT_OR:
00722 if (n == 0) {
00723 for (int i=x.size(); i--; ) {
00724 BoolView b(x[i]); GECODE_ME_FAIL(home,b.zero(home));
00725 }
00726 for (int i=y.size(); i--; ) {
00727 BoolView b(y[i]); GECODE_ME_FAIL(home,b.one(home));
00728 }
00729 } else {
00730 ViewArray<BoolView> xv(home,x);
00731 ViewArray<NegBoolView> yv(home,y.size());
00732 for (int i=y.size(); i--; ) {
00733 NegBoolView n(y[i]); yv[i]=n;
00734 }
00735 xv.unique(home); yv.unique(home);
00736 GECODE_ES_FAIL(home,(Bool::ClauseTrue<BoolView,NegBoolView>
00737 ::post(home,xv,yv)));
00738 }
00739 break;
00740 default:
00741 throw IllegalOperation("Int::clause");
00742 }
00743 }
00744
00745 void
00746 clause(Home home, BoolOpType o, const BoolVarArgs& x, const BoolVarArgs& y,
00747 BoolVar z, IntConLevel) {
00748 using namespace Int;
00749 if (home.failed()) return;
00750 switch (o) {
00751 case BOT_AND:
00752 {
00753 ViewArray<NegBoolView> xv(home,x.size());
00754 for (int i=x.size(); i--; ) {
00755 NegBoolView n(x[i]); xv[i]=n;
00756 }
00757 ViewArray<BoolView> yv(home,y);
00758 xv.unique(home); yv.unique(home);
00759 NegBoolView nz(z);
00760 GECODE_ES_FAIL(home,(Bool::Clause<NegBoolView,BoolView>
00761 ::post(home,xv,yv,nz)));
00762 }
00763 break;
00764 case BOT_OR:
00765 {
00766 ViewArray<BoolView> xv(home,x);
00767 ViewArray<NegBoolView> yv(home,y.size());
00768 for (int i=y.size(); i--; ) {
00769 NegBoolView n(y[i]); yv[i]=n;
00770 }
00771 xv.unique(home); yv.unique(home);
00772 GECODE_ES_FAIL(home,(Bool::Clause<BoolView,NegBoolView>
00773 ::post(home,xv,yv,z)));
00774 }
00775 break;
00776 default:
00777 throw IllegalOperation("Int::clause");
00778 }
00779 }
00780
00781 }
00782
00783