bool.cpp
Go to the documentation of this file.
00001 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */ 00002 /* 00003 * Main authors: 00004 * Christian Schulte <schulte@gecode.org> 00005 * 00006 * Copyright: 00007 * Christian Schulte, 2002 00008 * 00009 * Last modified: 00010 * $Date: 2010-06-04 16:13:00 +0200 (Fri, 04 Jun 2010) $ by $Author: schulte $ 00011 * $Revision: 11028 $ 00012 * 00013 * This file is part of Gecode, the generic constraint 00014 * development environment: 00015 * http://www.gecode.org 00016 * 00017 * Permission is hereby granted, free of charge, to any person obtaining 00018 * a copy of this software and associated documentation files (the 00019 * "Software"), to deal in the Software without restriction, including 00020 * without limitation the rights to use, copy, modify, merge, publish, 00021 * distribute, sublicense, and/or sell copies of the Software, and to 00022 * permit persons to whom the Software is furnished to do so, subject to 00023 * the following conditions: 00024 * 00025 * The above copyright notice and this permission notice shall be 00026 * included in all copies or substantial portions of the Software. 00027 * 00028 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, 00029 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 00030 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND 00031 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE 00032 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION 00033 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION 00034 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. 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((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((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((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((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((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((Bool::Eq<BoolView,BoolView> 00088 ::post(home,x0,x1))); 00089 break; 00090 case IRT_NQ: 00091 { 00092 NegBoolView n1(x1); 00093 GECODE_ES_FAIL((Bool::Eq<BoolView,NegBoolView> 00094 ::post(home,x0,n1))); 00095 } 00096 break; 00097 case IRT_GQ: 00098 GECODE_ES_FAIL(Bool::Lq<BoolView>::post(home,x1,x0)); 00099 break; 00100 case IRT_LQ: 00101 GECODE_ES_FAIL(Bool::Lq<BoolView>::post(home,x0,x1)); 00102 break; 00103 case IRT_GR: 00104 GECODE_ES_FAIL(Bool::Le<BoolView>::post(home,x1,x0)); 00105 break; 00106 case IRT_LE: 00107 GECODE_ES_FAIL(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(x.zero(home)); break; 00124 case IRT_NQ: 00125 case IRT_GR: 00126 GECODE_ME_FAIL(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(x.one(home)); break; 00139 case IRT_NQ: 00140 case IRT_LE: 00141 GECODE_ME_FAIL(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((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((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((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((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((Bool::Eq<BoolView,NegBoolView> 00208 ::post(home,x,z))); 00209 } 00210 break; 00211 case IRT_NQ: 00212 case IRT_GR: 00213 GECODE_ES_FAIL((Bool::Eq<BoolView,BoolView> 00214 ::post(home,x,y))); 00215 break; 00216 case IRT_LE: 00217 GECODE_ME_FAIL(y.zero(home)); 00218 break; 00219 case IRT_GQ: 00220 GECODE_ME_FAIL(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((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((Bool::Eq<BoolView,NegBoolView> 00237 ::post(home,x,z))); 00238 } 00239 break; 00240 case IRT_GR: 00241 GECODE_ME_FAIL(y.zero(home)); 00242 break; 00243 case IRT_LQ: 00244 GECODE_ME_FAIL(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((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((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(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(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(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(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(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(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(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(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((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((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(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(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(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(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(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(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(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(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((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((Bool::Eqv<BoolView,BoolView,NegBoolView> 00444 ::post(home,x[i],y[i],n))); 00445 } 00446 GECODE_ES_FAIL(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((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(b0.zero(home)); 00487 GECODE_ME_FAIL(b1.zero(home)); 00488 } 00489 break; 00490 case BOT_IMP: 00491 { 00492 BoolView b0(x0); BoolView b1(x1); 00493 GECODE_ME_FAIL(b0.one(home)); 00494 GECODE_ME_FAIL(b1.zero(home)); 00495 } 00496 break; 00497 case BOT_EQV: 00498 { 00499 NegBoolView n0(x0); 00500 GECODE_ES_FAIL((Bool::Eq<NegBoolView,BoolView> 00501 ::post(home,n0,x1))); 00502 } 00503 break; 00504 case BOT_XOR: 00505 GECODE_ES_FAIL((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(b0.one(home)); 00517 GECODE_ME_FAIL(b1.one(home)); 00518 } 00519 break; 00520 case BOT_OR: 00521 GECODE_ES_FAIL((Bool::BinOrTrue<BoolView,BoolView> 00522 ::post(home,x0,x1))); 00523 break; 00524 case BOT_IMP: 00525 { 00526 NegBoolView n0(x0); 00527 GECODE_ES_FAIL((Bool::BinOrTrue<NegBoolView,BoolView> 00528 ::post(home,n0,x1))); 00529 } 00530 break; 00531 case BOT_EQV: 00532 GECODE_ES_FAIL((Bool::Eq<BoolView,BoolView> 00533 ::post(home,x0,x1))); 00534 break; 00535 case BOT_XOR: 00536 { 00537 NegBoolView n0(x0); 00538 GECODE_ES_FAIL((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((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((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] = BoolVar(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] = BoolVar(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] = BoolVar(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(Bool::NaryOrTrue<NegBoolView>::post(home,b)); 00636 } else { 00637 for (int i=m; i--; ) { 00638 BoolView b(x[i]); GECODE_ME_FAIL(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(b.zero(home)); 00646 } 00647 } else { 00648 ViewArray<BoolView> b(home,x); 00649 b.unique(home); 00650 GECODE_ES_FAIL(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] = BoolVar(home,n,n);; 00659 for (int i=1; i<m-1; i++) 00660 z[i] = BoolVar(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] = BoolVar(home,n,n); 00671 for (int i=1; i<m-1; i++) 00672 z[i] = BoolVar(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] = BoolVar(home,n,n); 00683 for (int i=1; i<m-1; i++) 00684 z[i] = BoolVar(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((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(b.one(home)); 00715 } 00716 for (int i=y.size(); i--; ) { 00717 BoolView b(y[i]); GECODE_ME_FAIL(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(b.zero(home)); 00725 } 00726 for (int i=y.size(); i--; ) { 00727 BoolView b(y[i]); GECODE_ME_FAIL(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((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((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((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 // STATISTICS: int-post