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 #include "test/int.hh"
00035
00036 #include <gecode/minimodel.hh>
00037
00038 namespace Test { namespace Int {
00039
00041 namespace Bool {
00042
00043 inline int
00044 check(int x0, Gecode::BoolOpType op, int x1) {
00045 switch (op) {
00046 case Gecode::BOT_AND: return x0 & x1;
00047 case Gecode::BOT_OR: return x0 | x1;
00048 case Gecode::BOT_IMP: return !x0 | x1;
00049 case Gecode::BOT_EQV: return x0 == x1;
00050 case Gecode::BOT_XOR: return x0 != x1;
00051 default: GECODE_NEVER;
00052 }
00053 GECODE_NEVER;
00054 return 0;
00055 }
00056
00062
00063 class BinXYZ : public Test {
00064 protected:
00066 Gecode::BoolOpType op;
00067 public:
00069 BinXYZ(Gecode::BoolOpType op0)
00070 : Test("Bool::Bin::XYZ::"+str(op0),3,0,1), op(op0) {}
00072 virtual bool solution(const Assignment& x) const {
00073 return check(x[0],op,x[1]) == x[2];
00074 }
00076 virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00077 using namespace Gecode;
00078 rel(home,
00079 channel(home,x[0]), op, channel(home,x[1]),
00080 channel(home,x[2]));
00081 }
00082 };
00083
00085 class BinXXY : public Test {
00086 protected:
00088 Gecode::BoolOpType op;
00089 public:
00091 BinXXY(Gecode::BoolOpType op0)
00092 : Test("Bool::Bin::XXY::"+str(op0),2,0,1), op(op0) {}
00094 virtual bool solution(const Assignment& x) const {
00095 return check(x[0],op,x[0]) == x[1];
00096 }
00098 virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00099 using namespace Gecode;
00100 BoolVar b = channel(home,x[0]);
00101 rel(home, b, op, b, channel(home,x[1]));
00102 }
00103 };
00104
00106 class BinXYX : public Test {
00107 protected:
00109 Gecode::BoolOpType op;
00110 public:
00112 BinXYX(Gecode::BoolOpType op0)
00113 : Test("Bool::Bin::XYX::"+str(op0),2,0,1), op(op0) {}
00115 virtual bool solution(const Assignment& x) const {
00116 return check(x[0],op,x[1]) == x[0];
00117 }
00119 virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00120 using namespace Gecode;
00121 BoolVar b = channel(home,x[0]);
00122 rel(home, b, op, channel(home,x[1]), b);
00123 }
00124 };
00125
00127 class BinXYY : public Test {
00128 protected:
00130 Gecode::BoolOpType op;
00131 public:
00133 BinXYY(Gecode::BoolOpType op0)
00134 : Test("Bool::Bin::XYY::"+str(op0),2,0,1), op(op0) {}
00136 virtual bool solution(const Assignment& x) const {
00137 return check(x[0],op,x[1]) == x[1];
00138 }
00140 virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00141 using namespace Gecode;
00142 BoolVar b = channel(home,x[1]);
00143 rel(home, channel(home,x[0]), op, b, b);
00144 }
00145 };
00146
00148 class BinXXX : public Test {
00149 protected:
00151 Gecode::BoolOpType op;
00152 public:
00154 BinXXX(Gecode::BoolOpType op0)
00155 : Test("Bool::Bin::XXX::"+str(op0),1,0,1), op(op0) {}
00157 virtual bool solution(const Assignment& x) const {
00158 return check(x[0],op,x[0]) == x[0];
00159 }
00161 virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00162 using namespace Gecode;
00163 BoolVar b = channel(home,x[0]);
00164 rel(home, b, op, b, b);
00165 }
00166 };
00167
00169 class BinConstXY : public Test {
00170 protected:
00172 Gecode::BoolOpType op;
00174 int c;
00175 public:
00177 BinConstXY(Gecode::BoolOpType op0, int c0)
00178 : Test("Bool::Bin::XY::"+str(op0)+"::"+str(c0),2,0,1),
00179 op(op0), c(c0) {}
00181 virtual bool solution(const Assignment& x) const {
00182 return check(x[0],op,x[1]) == c;
00183 }
00185 virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00186 using namespace Gecode;
00187 rel(home, channel(home,x[0]), op, channel(home,x[1]), c);
00188 }
00189 };
00190
00192 class BinConstXX : public Test {
00193 protected:
00195 Gecode::BoolOpType op;
00197 int c;
00198 public:
00200 BinConstXX(Gecode::BoolOpType op0, int c0)
00201 : Test("Bool::Bin::XX::"+str(op0)+"::"+str(c0),1,0,1),
00202 op(op0), c(c0) {}
00204 virtual bool solution(const Assignment& x) const {
00205 return check(x[0],op,x[0]) == c;
00206 }
00208 virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00209 using namespace Gecode;
00210 BoolVar b = channel(home,x[0]);
00211 rel(home, b, op, b, c);
00212 }
00213 };
00214
00216 class Nary : public Test {
00217 protected:
00219 Gecode::BoolOpType op;
00220 public:
00222 Nary(Gecode::BoolOpType op0, int n)
00223 : Test("Bool::Nary::"+str(op0)+"::"+str(n),n+1,0,1), op(op0) {}
00225 virtual bool solution(const Assignment& x) const {
00226 int n = x.size()-1;
00227 int b = check(x[n-2],op,x[n-1]);
00228 for (int i=0; i<n-2; i++)
00229 b = check(x[i],op,b);
00230 return b == x[n];
00231 }
00233 virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00234 using namespace Gecode;
00235 BoolVarArgs b(x.size()-1);
00236 for (int i=x.size()-1; i--; )
00237 b[i]=channel(home,x[i]);
00238 rel(home, op, b, channel(home,x[x.size()-1]));
00239 }
00240 };
00241
00243 class NaryShared : public Test {
00244 protected:
00246 Gecode::BoolOpType op;
00247 public:
00249 NaryShared(Gecode::BoolOpType op0, int n)
00250 : Test("Bool::Nary::Shared::"+str(op0)+"::"+str(n),n,0,1),
00251 op(op0) {
00252 if ((op == Gecode::BOT_EQV) || (op == Gecode::BOT_XOR))
00253 testfix = false;
00254 }
00256 virtual bool solution(const Assignment& x) const {
00257 int n = x.size();
00258 int b = check(x[n-2],op,x[n-1]);
00259 for (int i=0; i<n-2; i++)
00260 b = check(x[i],op,b);
00261 return b == x[n-1];
00262 }
00264 virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00265 using namespace Gecode;
00266 BoolVarArgs b(x.size());
00267 for (int i=x.size(); i--; )
00268 b[i]=channel(home,x[i]);
00269 rel(home, op, b, b[x.size()-1]);
00270 }
00271 };
00272
00274 class NaryConst : public Test {
00275 protected:
00277 Gecode::BoolOpType op;
00279 int c;
00280 public:
00282 NaryConst(Gecode::BoolOpType op0, int n, int c0)
00283 : Test("Bool::Nary::"+str(op0)+"::"+str(n)+"::"+str(c0),n,0,1),
00284 op(op0), c(c0) {}
00286 virtual bool solution(const Assignment& x) const {
00287 int n = x.size();
00288 int b = check(x[n-2],op,x[n-1]);
00289 for (int i=0; i<n-2; i++)
00290 b = check(x[i],op,b);
00291 return b == c;
00292 }
00294 virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00295 using namespace Gecode;
00296 BoolVarArgs b(x.size());
00297 for (int i=x.size(); i--; )
00298 b[i]=channel(home,x[i]);
00299 rel(home, op, b, c);
00300 }
00301 };
00302
00303
00305 class ClauseXYZ : public Test {
00306 protected:
00308 Gecode::BoolOpType op;
00309 public:
00311 ClauseXYZ(Gecode::BoolOpType op0, int n)
00312 : Test("Bool::Clause::XYZ::"+str(op0)+"::"+str(n),n+1,0,1), op(op0) {}
00314 virtual bool solution(const Assignment& x) const {
00315 int n = (x.size()-1) / 2;
00316 int b;
00317 if (n == 1) {
00318 b = check(x[0],op,!x[1]);
00319 } else {
00320 b = check(x[0],op,!x[n]);
00321 for (int i=1; i<n; i++)
00322 b = check(b,op,check(x[i],op,!x[n+i]));
00323 }
00324 return b == x[x.size()-1];
00325 }
00327 virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00328 using namespace Gecode;
00329 int n = (x.size()-1) / 2;
00330 BoolVarArgs a(n), b(n);
00331 for (int i=n; i--; ) {
00332 a[i]=channel(home,x[i]);
00333 b[i]=channel(home,x[i+n]);
00334 }
00335 clause(home, op, a, b, channel(home,x[x.size()-1]));
00336 }
00337 };
00338
00340 class ClauseXXYYX : public Test {
00341 protected:
00343 Gecode::BoolOpType op;
00344 public:
00346 ClauseXXYYX(Gecode::BoolOpType op0, int n)
00347 : Test("Bool::Clause::XXYYX::"+str(op0)+"::"+str(n),n,0,1),
00348 op(op0) {}
00350 virtual bool solution(const Assignment& x) const {
00351 int n = x.size() / 2;
00352 int b;
00353 if (n == 1) {
00354 b = check(x[0],op,!x[1]);
00355 } else {
00356 b = check(x[0],op,!x[n]);
00357 for (int i=1; i<n; i++)
00358 b = check(b,op,check(x[i],op,!x[n+i]));
00359 }
00360 return b == x[0];
00361 }
00363 virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00364 using namespace Gecode;
00365 int n = x.size() / 2;
00366 BoolVarArgs a(2*n), b(2*n);
00367 for (int i=n; i--; ) {
00368 a[i]=a[i+n]=channel(home,x[i]);
00369 b[i]=b[i+n]=channel(home,x[i+n]);
00370 }
00371 clause(home, op, a, b, a[0]);
00372 }
00373 };
00374
00376 class ClauseXXY : public Test {
00377 protected:
00379 Gecode::BoolOpType op;
00380 public:
00382 ClauseXXY(Gecode::BoolOpType op0, int n)
00383 : Test("Bool::Clause::XXY::"+str(op0)+"::"+str(n),n,0,1),
00384 op(op0) {}
00386 virtual bool solution(const Assignment& x) const {
00387 return (x[0] == 1) == (op == Gecode::BOT_OR);
00388 }
00390 virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00391 using namespace Gecode;
00392 int n = x.size() / 2;
00393 BoolVarArgs a(2*n), b(2*n);
00394 for (int i=n; i--; ) {
00395 a[i]=b[i+n]=channel(home,x[i]);
00396 b[i]=a[i+n]=channel(home,x[i+n]);
00397 }
00398 clause(home, op, a, b, a[0]);
00399 }
00400 };
00401
00403 class ClauseConst : public Test {
00404 protected:
00406 Gecode::BoolOpType op;
00408 int c;
00409 public:
00411 ClauseConst(Gecode::BoolOpType op0, int n, int c0)
00412 : Test("Bool::Clause::"+str(op0)+"::"+str(n)+"::"+str(c0),n,0,1),
00413 op(op0), c(c0) {}
00415 virtual bool solution(const Assignment& x) const {
00416 int n = x.size() / 2;
00417 int b;
00418 if (n == 1) {
00419 b = check(x[0],op,!x[1]);
00420 } else {
00421 b = check(x[0],op,!x[n]);
00422 for (int i=1; i<n; i++)
00423 b = check(b,op,check(x[i],op,!x[n+i]));
00424 }
00425 return b == c;
00426 }
00428 virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00429 using namespace Gecode;
00430 int n = x.size() / 2;
00431 BoolVarArgs a(n), b(n);
00432 for (int i=n; i--; ) {
00433 a[i]=channel(home,x[i]);
00434 b[i]=channel(home,x[i+n]);
00435 }
00436 clause(home, op, a, b, c);
00437 }
00438 };
00439
00441 class ITEInt : public Test {
00442 public:
00444 ITEInt(Gecode::IntPropLevel ipl)
00445 : Test("ITE::Int::"+str(ipl),4,-4,4,false,ipl) {}
00447 virtual bool solution(const Assignment& x) const {
00448 if ((x[0] < 0) || (x[0] > 1))
00449 return false;
00450 if (x[0] == 1)
00451 return x[1] == x[3];
00452 else
00453 return x[2] == x[3];
00454 }
00456 virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00457 using namespace Gecode;
00458 if (Base::rand(2) != 0)
00459 ite(home,channel(home,x[0]),x[1],x[2],x[3]);
00460 else
00461 rel(home, ite(channel(home,x[0]),x[1],x[2]) == x[3]);
00462 }
00463 };
00464
00466 class ITEBool : public Test {
00467 public:
00469 ITEBool(void)
00470 : Test("ITE::Bool",4,0,1,false) {}
00472 virtual bool solution(const Assignment& x) const {
00473 if (x[0] == 1)
00474 return x[1] == x[3];
00475 else
00476 return x[2] == x[3];
00477 }
00479 virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00480 using namespace Gecode;
00481 ite(home,channel(home,x[0]),channel(home,x[1]),
00482 channel(home,x[2]),channel(home,x[3]));
00483 }
00484 };
00485
00487 class Create {
00488 public:
00490 Create(void) {
00491 using namespace Gecode;
00492 for (BoolOpTypes bots; bots(); ++bots) {
00493 (void) new BinXYZ(bots.bot());
00494 (void) new BinXXY(bots.bot());
00495 (void) new BinXYX(bots.bot());
00496 (void) new BinXYY(bots.bot());
00497 (void) new BinXXX(bots.bot());
00498 (void) new BinConstXY(bots.bot(),0);
00499 (void) new BinConstXY(bots.bot(),1);
00500 (void) new BinConstXX(bots.bot(),0);
00501 (void) new BinConstXX(bots.bot(),1);
00502 (void) new Nary(bots.bot(),2);
00503 (void) new Nary(bots.bot(),6);
00504 (void) new Nary(bots.bot(),10);
00505 (void) new NaryShared(bots.bot(),2);
00506 (void) new NaryShared(bots.bot(),6);
00507 (void) new NaryShared(bots.bot(),10);
00508 (void) new NaryConst(bots.bot(),2,0);
00509 (void) new NaryConst(bots.bot(),6,0);
00510 (void) new NaryConst(bots.bot(),10,0);
00511 (void) new NaryConst(bots.bot(),2,1);
00512 (void) new NaryConst(bots.bot(),6,1);
00513 (void) new NaryConst(bots.bot(),10,1);
00514 if ((bots.bot() == BOT_AND) || (bots.bot() == BOT_OR)) {
00515 (void) new ClauseXYZ(bots.bot(),2);
00516 (void) new ClauseXYZ(bots.bot(),6);
00517 (void) new ClauseXYZ(bots.bot(),10);
00518 (void) new ClauseXXYYX(bots.bot(),2);
00519 (void) new ClauseXXYYX(bots.bot(),6);
00520 (void) new ClauseXXYYX(bots.bot(),10);
00521 (void) new ClauseXXY(bots.bot(),2);
00522 (void) new ClauseXXY(bots.bot(),6);
00523 (void) new ClauseXXY(bots.bot(),10);
00524 (void) new ClauseConst(bots.bot(),2,0);
00525 (void) new ClauseConst(bots.bot(),6,0);
00526 (void) new ClauseConst(bots.bot(),10,0);
00527 (void) new ClauseConst(bots.bot(),2,1);
00528 (void) new ClauseConst(bots.bot(),6,1);
00529 (void) new ClauseConst(bots.bot(),10,1);
00530 }
00531 }
00532 }
00533 };
00534
00535 Create c;
00536 ITEInt itebnd(Gecode::IPL_BND);
00537 ITEInt itedom(Gecode::IPL_DOM);
00538 ITEBool itebool;
00539
00541
00542 }
00543 }}
00544
00545
00546