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
00041
00042 #include "test/float.hh"
00043
00044 #include <algorithm>
00045
00046 namespace Test { namespace Float {
00047
00048
00049
00050
00051
00052 void
00053 CpltAssignment::operator++(void) {
00054 using namespace Gecode;
00055 int i = n-1;
00056 while (true) {
00057 FloatNum ns = dsv[i].min() + step;
00058 dsv[i] = FloatVal(ns,nextafter(ns,ns+1));
00059 if ((dsv[i].max() < d.max()) || (i == 0))
00060 return;
00061 dsv[i--] = FloatVal(d.min(),nextafter(d.min(),d.max()));
00062 }
00063 }
00064
00065
00066
00067
00068
00069 void
00070 ExtAssignment::operator++(void) {
00071 using namespace Gecode;
00072 assert(n > 1);
00073 int i = n-2;
00074 while (true) {
00075 FloatNum ns = dsv[i].min() + step;
00076 dsv[i] = FloatVal(ns,nextafter(ns,ns+1));
00077 if ((dsv[i].max() < d.max()) || (i == 0)) {
00078 if (curPb->extendAssignement(*this)) return;
00079 if ((dsv[i].max() >= d.max()) && (i == 0)) return;
00080 continue;
00081 }
00082 dsv[i--] = FloatVal(d.min(),nextafter(d.min(),d.max()));
00083 }
00084 }
00085
00086
00087
00088
00089
00090
00091 void
00092 RandomAssignment::operator++(void) {
00093 for (int i = n; i--; )
00094 vals[i]=randval();
00095 a--;
00096 }
00097
00098 }}
00099
00100 std::ostream&
00101 operator<<(std::ostream& os, const Test::Float::Assignment& a) {
00102 int n = a.size();
00103 os << "{";
00104 for (int i=0; i<n; i++)
00105 os << "[" << a[i].min() << "," << a[i].max() << "]" << ((i!=n-1) ? "," : "}");
00106 return os;
00107 }
00108
00109 namespace Test { namespace Float {
00110
00111 Gecode::FloatNum randFValDown(Gecode::FloatNum l, Gecode::FloatNum u) {
00112 using namespace Gecode;
00113 using namespace Gecode::Float;
00114 Rounding r;
00115 return
00116 r.add_down(
00117 l,
00118 r.mul_down(
00119 r.div_down(
00120 Base::rand(static_cast<unsigned int>(Int::Limits::max)),
00121 static_cast<FloatNum>(Int::Limits::max)
00122 ),
00123 r.sub_down(u,l)
00124 )
00125 );
00126 }
00127
00128 Gecode::FloatNum randFValUp(Gecode::FloatNum l, Gecode::FloatNum u) {
00129 using namespace Gecode;
00130 using namespace Gecode::Float;
00131 Rounding r;
00132 return
00133 r.sub_up(
00134 u,
00135 r.mul_down(
00136 r.div_down(
00137 Base::rand(static_cast<unsigned int>(Int::Limits::max)),
00138 static_cast<FloatNum>(Int::Limits::max)
00139 ),
00140 r.sub_down(u,l)
00141 )
00142 );
00143 }
00144
00145
00146 TestSpace::TestSpace(int n, Gecode::FloatVal& d0, Gecode::FloatNum s,
00147 Test* t)
00148 : d(d0), step(s),
00149 x(*this,n,Gecode::Float::Limits::min,Gecode::Float::Limits::max),
00150 test(t), reified(false) {
00151 Gecode::FloatVarArgs _x(*this,n,d.min(),d.max());
00152 if (x.size() == 1)
00153 Gecode::dom(*this,x[0],_x[0]);
00154 else
00155 Gecode::dom(*this,x,_x);
00156 Gecode::BoolVar b(*this,0,1);
00157 r = Gecode::Reify(b,Gecode::RM_EQV);
00158 if (opt.log)
00159 olog << ind(2) << "Initial: x[]=" << x
00160 << std::endl;
00161 }
00162
00163 TestSpace::TestSpace(int n, Gecode::FloatVal& d0, Gecode::FloatNum s,
00164 Test* t, Gecode::ReifyMode rm)
00165 : d(d0), step(s), x(*this,n,d.min(),d.max()), test(t), reified(true) {
00166 Gecode::BoolVar b(*this,0,1);
00167 r = Gecode::Reify(b,rm);
00168 if (opt.log)
00169 olog << ind(2) << "Initial: x[]=" << x
00170 << " b=" << r.var()
00171 << std::endl;
00172 }
00173
00174 TestSpace::TestSpace(bool share, TestSpace& s)
00175 : Gecode::Space(share,s), d(s.d), step(s.step), test(s.test), reified(s.reified) {
00176 x.update(*this, share, s.x);
00177 Gecode::BoolVar b;
00178 Gecode::BoolVar sr(s.r.var());
00179 b.update(*this, share, sr);
00180 r.var(b); r.mode(s.r.mode());
00181 }
00182
00183 Gecode::Space*
00184 TestSpace::copy(bool share) {
00185 return new TestSpace(share,*this);
00186 }
00187
00188 void
00189 TestSpace::dropUntil(const Assignment& a) {
00190 for (int i = x.size(); i--; )
00191 Gecode::rel(*this, x[i], Gecode::FRT_GQ, a[i].min());
00192 }
00193
00194 bool
00195 TestSpace::assigned(void) const {
00196 for (int i=x.size(); i--; )
00197 if (!x[i].assigned())
00198 return false;
00199 return true;
00200 }
00201
00202 bool
00203 TestSpace::matchAssignment(const Assignment& a) const {
00204 for (int i=x.size(); i--; )
00205 if ((x[i].min() != a[i].min()) || (x[i].max() != a[i].max()))
00206 return false;
00207 return true;
00208 }
00209
00210 void
00211 TestSpace::post(void) {
00212 if (reified){
00213 test->post(*this,x,r);
00214 if (opt.log)
00215 olog << ind(3) << "Posting reified propagator" << std::endl;
00216 } else {
00217 test->post(*this,x);
00218 if (opt.log)
00219 olog << ind(3) << "Posting propagator" << std::endl;
00220 }
00221 }
00222
00223 bool
00224 TestSpace::failed(void) {
00225 if (opt.log) {
00226 olog << ind(3) << "Fixpoint: " << x;
00227 bool f=(status() == Gecode::SS_FAILED);
00228 olog << std::endl << ind(3) << " --> " << x << std::endl;
00229 return f;
00230 } else {
00231 return status() == Gecode::SS_FAILED;
00232 }
00233 }
00234
00235 void
00236 TestSpace::rel(int i, Gecode::FloatRelType frt, Gecode::FloatVal n) {
00237 if (opt.log) {
00238 olog << ind(4) << "x[" << i << "] ";
00239 switch (frt) {
00240 case Gecode::FRT_EQ: olog << "="; break;
00241 case Gecode::FRT_NQ: olog << "!="; break;
00242 case Gecode::FRT_LQ: olog << "<="; break;
00243 case Gecode::FRT_LE: olog << "<"; break;
00244 case Gecode::FRT_GQ: olog << ">="; break;
00245 case Gecode::FRT_GR: olog << ">"; break;
00246 }
00247 olog << " [" << n.min() << "," << n.max() << "]" << std::endl;
00248 }
00249 Gecode::rel(*this, x[i], frt, n);
00250 }
00251
00252 void
00253 TestSpace::rel(bool sol) {
00254 int n = sol ? 1 : 0;
00255 assert(reified);
00256 if (opt.log)
00257 olog << ind(4) << "b = " << n << std::endl;
00258 Gecode::rel(*this, r.var(), Gecode::IRT_EQ, n);
00259 }
00260
00261 void
00262 TestSpace::assign(const Assignment& a, MaybeType& sol, bool skip) {
00263 using namespace Gecode;
00264 int i = skip ? static_cast<int>(Base::rand(a.size())) : -1;
00265
00266 for (int j=a.size(); j--; )
00267 if (i != j) {
00268 if ((x[j].min() == a[j].max()) || (x[j].max() == a[j].min()))
00269 {
00270 sol = MT_MAYBE;
00271 return;
00272 }
00273 rel(j, FRT_EQ, a[j]);
00274 if (Base::fixpoint() && failed())
00275 return;
00276 }
00277 }
00278
00279 void
00280 TestSpace::bound(void) {
00281 using namespace Gecode;
00282
00283 int i = Base::rand(x.size());
00284 while (x[i].assigned()) {
00285 i = (i+1) % x.size();
00286 }
00287 bool min = Base::rand(2);
00288 if (min)
00289 rel(i, FRT_LQ, nextafter(x[i].min(), x[i].max()));
00290 else
00291 rel(i, FRT_GQ, nextafter(x[i].max(), x[i].min()));
00292 }
00293
00294 Gecode::FloatNum
00295 TestSpace::cut(int* cutDirections) {
00296 using namespace Gecode;
00297 using namespace Gecode::Float;
00298
00299 int i = 0;
00300 while (x[i].assigned()) i++;
00301 for (int j=x.size(); j--; ) {
00302 if (!x[j].assigned() && (x[j].size() > x[i].size())) i = j;
00303 }
00304 Rounding r;
00305 if (cutDirections[i]) {
00306 FloatNum m = r.div_up(r.add_up(x[i].min(),x[i].max()),2);
00307 FloatNum n = nextafter(x[i].min(), x[i].max());
00308 if (m > n)
00309 rel(i, FRT_LQ, m);
00310 else
00311 rel(i, FRT_LQ, n);
00312 } else {
00313 FloatNum m = r.div_down(r.add_down(x[i].min(),x[i].max()),2);
00314 FloatNum n = nextafter(x[i].max(), x[i].min());
00315 if (m < n)
00316 rel(i, FRT_GQ, m);
00317 else
00318 rel(i, FRT_GQ, n);
00319 }
00320 return x[i].size();
00321 }
00322
00323 void
00324 TestSpace::prune(int i) {
00325 using namespace Gecode;
00326
00327 if (Base::rand(2) && !x[i].assigned()) {
00328 Gecode::FloatNum v=randFValUp(x[i].min(),x[i].max());
00329 assert((v >= x[i].min()) && (v <= x[i].max()));
00330 rel(i, Gecode::FRT_LQ, v);
00331 }
00332 if (Base::rand(2) && !x[i].assigned()) {
00333 Gecode::FloatNum v=randFValDown(x[i].min(),x[i].max());
00334 assert((v <= x[i].max()) && (v >= x[i].min()));
00335 rel(i, Gecode::FRT_GQ, v);
00336 }
00337 }
00338
00339 void
00340 TestSpace::prune(void) {
00341 using namespace Gecode;
00342
00343 int i = Base::rand(x.size());
00344 while (x[i].assigned()) {
00345 i = (i+1) % x.size();
00346 }
00347 prune(i);
00348 }
00349
00350 bool
00351 TestSpace::prune(const Assignment& a, bool testfix) {
00352
00353 int i = Base::rand(x.size());
00354 while (x[i].assigned())
00355 i = (i+1) % x.size();
00356
00357 switch (Base::rand(2)) {
00358 case 0:
00359 if (a[i].max() < x[i].max()) {
00360 Gecode::FloatNum v=randFValDown(a[i].max(),x[i].max());
00361 assert((v >= a[i].max()) && (v <= x[i].max()));
00362 rel(i, Gecode::FRT_LQ, v);
00363 }
00364 break;
00365 case 1:
00366 if (a[i].min() > x[i].min()) {
00367 Gecode::FloatNum v=randFValUp(x[i].min(),a[i].min());
00368 assert((v <= a[i].min()) && (v >= x[i].min()));
00369 rel(i, Gecode::FRT_GQ, v);
00370 }
00371 break;
00372 }
00373 if (Base::fixpoint()) {
00374 if (failed() || !testfix)
00375 return true;
00376 TestSpace* c = static_cast<TestSpace*>(clone());
00377 if (opt.log)
00378 olog << ind(3) << "Testing fixpoint on copy" << std::endl;
00379 c->post();
00380 if (c->failed()) {
00381 delete c; return false;
00382 }
00383 for (int i=x.size(); i--; )
00384 if (x[i].size() != c->x[i].size()) {
00385 delete c; return false;
00386 }
00387 if (reified && (r.var().size() != c->r.var().size())) {
00388 delete c; return false;
00389 }
00390 if (opt.log)
00391 olog << ind(3) << "Finished testing fixpoint on copy" << std::endl;
00392 delete c;
00393 }
00394 return true;
00395 }
00396
00397
00398 const Gecode::FloatRelType FloatRelTypes::frts[] =
00399 {Gecode::FRT_EQ,Gecode::FRT_NQ,Gecode::FRT_LQ,Gecode::FRT_LE,
00400 Gecode::FRT_GQ,Gecode::FRT_GR};
00401
00402 Assignment*
00403 Test::assignment(void) const {
00404 switch (assigmentType) {
00405 case CPLT_ASSIGNMENT:
00406 return new CpltAssignment(arity,dom,step);
00407 case RANDOM_ASSIGNMENT:
00408 return new RandomAssignment(arity,dom,step);
00409 case EXTEND_ASSIGNMENT:
00410 return new ExtAssignment(arity,dom,step,this);
00411 default :
00412 GECODE_NEVER;
00413 }
00414 return NULL;
00415 }
00416
00417 bool
00418 Test::extendAssignement(Assignment&) const {
00419 GECODE_NEVER;
00420 return false;
00421 }
00422
00423 bool
00424 Test::subsumed(const TestSpace& ts) const {
00425 if (!testsubsumed) return true;
00426 if (ts.propagators()==0) return true;
00427 if (assigmentType == EXTEND_ASSIGNMENT) return true;
00428 return false;
00429 }
00430
00432 #define CHECK_TEST(T,M) \
00433 if (opt.log) \
00434 olog << ind(3) << "Check: " << (M) << std::endl; \
00435 if (!(T)) { \
00436 problem = (M); delete s; goto failed; \
00437 }
00438
00440 #define START_TEST(T) \
00441 if (opt.log) { \
00442 olog.str(""); \
00443 olog << ind(2) << "Testing: " << (T) << std::endl; \
00444 } \
00445 test = (T);
00446
00447 bool
00448 Test::ignore(const Assignment&) const {
00449 return false;
00450 }
00451
00452 void
00453 Test::post(Gecode::Space&, Gecode::FloatVarArray&,
00454 Gecode::Reify) {}
00455
00456 bool
00457 Test::run(void) {
00458 using namespace Gecode;
00459 const char* test = "NONE";
00460 const char* problem = "NONE";
00461
00462
00463 Assignment* ap = assignment();
00464 Assignment& a = *ap;
00465
00466
00467 TestSpace* search_s = new TestSpace(arity,dom,step,this);
00468 post(*search_s,search_s->x);
00469 branch(*search_s,search_s->x,FLOAT_VAR_NONE(),FLOAT_VAL_SPLIT_MIN());
00470 Search::Options search_o;
00471 search_o.threads = 1;
00472 DFS<TestSpace> * e_s = new DFS<TestSpace>(search_s,search_o);
00473 while (a()) {
00474 MaybeType sol = solution(a);
00475 if (opt.log) {
00476 olog << ind(1) << "Assignment: " << a;
00477 switch (sol) {
00478 case MT_TRUE: olog << " (solution)"; break;
00479 case MT_FALSE: olog << " (no solution)"; break;
00480 case MT_MAYBE: olog << " (maybe)"; break;
00481 }
00482 olog << std::endl;
00483 }
00484 START_TEST("Assignment (after posting)");
00485 {
00486 TestSpace* s = new TestSpace(arity,dom,step,this);
00487 TestSpace* sc = NULL;
00488 s->post();
00489 switch (Base::rand(3)) {
00490 case 0:
00491 if (opt.log)
00492 olog << ind(3) << "No copy" << std::endl;
00493 sc = s;
00494 s = NULL;
00495 break;
00496 case 1:
00497 if (opt.log)
00498 olog << ind(3) << "Unshared copy" << std::endl;
00499 if (s->status() != SS_FAILED) {
00500 sc = static_cast<TestSpace*>(s->clone(false));
00501 } else {
00502 sc = s; s = NULL;
00503 }
00504 break;
00505 case 2:
00506 if (opt.log)
00507 olog << ind(3) << "Shared copy" << std::endl;
00508 if (s->status() != SS_FAILED) {
00509 sc = static_cast<TestSpace*>(s->clone(true));
00510 } else {
00511 sc = s; s = NULL;
00512 }
00513 break;
00514 default: assert(false);
00515 }
00516 sc->assign(a,sol);
00517 if (sol == MT_TRUE) {
00518 CHECK_TEST(!sc->failed(), "Failed on solution");
00519 CHECK_TEST(subsumed(*sc), "No subsumption");
00520 } else if (sol == MT_FALSE) {
00521 CHECK_TEST(sc->failed(), "Solved on non-solution");
00522 }
00523 delete s; delete sc;
00524 }
00525 START_TEST("Partial assignment (after posting)");
00526 {
00527 TestSpace* s = new TestSpace(arity,dom,step,this);
00528 s->post();
00529 s->assign(a,sol,true);
00530 (void) s->failed();
00531 s->assign(a,sol);
00532 if (sol == MT_TRUE) {
00533 CHECK_TEST(!s->failed(), "Failed on solution");
00534 CHECK_TEST(subsumed(*s), "No subsumption");
00535 } else if (sol == MT_FALSE) {
00536 CHECK_TEST(s->failed(), "Solved on non-solution");
00537 }
00538 delete s;
00539 }
00540 START_TEST("Assignment (before posting)");
00541 {
00542 TestSpace* s = new TestSpace(arity,dom,step,this);
00543 s->assign(a,sol);
00544 s->post();
00545 if (sol == MT_TRUE) {
00546 CHECK_TEST(!s->failed(), "Failed on solution");
00547 CHECK_TEST(subsumed(*s), "No subsumption");
00548 } else if (sol == MT_FALSE) {
00549 CHECK_TEST(s->failed(), "Solved on non-solution");
00550 }
00551 delete s;
00552 }
00553 START_TEST("Partial assignment (before posting)");
00554 {
00555 TestSpace* s = new TestSpace(arity,dom,step,this);
00556 s->assign(a,sol,true);
00557 s->post();
00558 (void) s->failed();
00559 s->assign(a,sol);
00560 if (sol == MT_TRUE) {
00561 CHECK_TEST(!s->failed(), "Failed on solution");
00562 CHECK_TEST(subsumed(*s), "No subsumption");
00563 } else if (sol == MT_FALSE) {
00564 CHECK_TEST(s->failed(), "Solved on non-solution");
00565 }
00566 delete s;
00567 }
00568 START_TEST("Prune");
00569 {
00570 TestSpace* s = new TestSpace(arity,dom,step,this);
00571 s->post();
00572 while (!s->failed() && !s->assigned() && !s->matchAssignment(a))
00573 if (!s->prune(a,testfix)) {
00574 problem = "No fixpoint";
00575 delete s;
00576 goto failed;
00577 }
00578 s->assign(a,sol);
00579 if (sol == MT_TRUE) {
00580 CHECK_TEST(!s->failed(), "Failed on solution");
00581 CHECK_TEST(subsumed(*s), "No subsumption");
00582 } else if (sol == MT_FALSE) {
00583 CHECK_TEST(s->failed(), "Solved on non-solution");
00584 }
00585 delete s;
00586 }
00587
00588 if (reified && !ignore(a) && (sol != MT_MAYBE)) {
00589 if (eqv()) {
00590 START_TEST("Assignment reified (rewrite after post, <=>)");
00591 TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
00592 s->post();
00593 s->rel(sol == MT_TRUE);
00594 s->assign(a,sol);
00595 CHECK_TEST(!s->failed(), "Failed");
00596 CHECK_TEST(subsumed(*s), "No subsumption");
00597 delete s;
00598 }
00599 if (imp()) {
00600 START_TEST("Assignment reified (rewrite after post, =>)");
00601 TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
00602 s->post();
00603 s->rel(sol == MT_TRUE);
00604 s->assign(a,sol);
00605 CHECK_TEST(!s->failed(), "Failed");
00606 CHECK_TEST(subsumed(*s), "No subsumption");
00607 delete s;
00608 }
00609 if (pmi()) {
00610 START_TEST("Assignment reified (rewrite after post, <=)");
00611 TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
00612 s->post();
00613 s->rel(sol == MT_TRUE);
00614 s->assign(a,sol);
00615 CHECK_TEST(!s->failed(), "Failed");
00616 CHECK_TEST(subsumed(*s), "No subsumption");
00617 delete s;
00618 }
00619 if (eqv()) {
00620 START_TEST("Assignment reified (immediate rewrite, <=>)");
00621 TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
00622 s->rel(sol == MT_TRUE);
00623 s->post();
00624 s->assign(a,sol);
00625 CHECK_TEST(!s->failed(), "Failed");
00626 CHECK_TEST(subsumed(*s), "No subsumption");
00627 delete s;
00628 }
00629 if (imp()) {
00630 START_TEST("Assignment reified (immediate rewrite, =>)");
00631 TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
00632 s->rel(sol == MT_TRUE);
00633 s->post();
00634 s->assign(a,sol);
00635 CHECK_TEST(!s->failed(), "Failed");
00636 CHECK_TEST(subsumed(*s), "No subsumption");
00637 delete s;
00638 }
00639 if (pmi()) {
00640 START_TEST("Assignment reified (immediate rewrite, <=)");
00641 TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
00642 s->rel(sol == MT_TRUE);
00643 s->post();
00644 s->assign(a,sol);
00645 CHECK_TEST(!s->failed(), "Failed");
00646 CHECK_TEST(subsumed(*s), "No subsumption");
00647 delete s;
00648 }
00649 if (eqv()) {
00650 START_TEST("Assignment reified (before posting, <=>)");
00651 TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
00652 s->assign(a,sol);
00653 s->post();
00654 CHECK_TEST(!s->failed(), "Failed");
00655 CHECK_TEST(subsumed(*s), "No subsumption");
00656 if (s->r.var().assigned()) {
00657 if (sol == MT_TRUE) {
00658 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
00659 } else if (sol == MT_FALSE) {
00660 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
00661 }
00662 }
00663 delete s;
00664 }
00665 if (imp()) {
00666 START_TEST("Assignment reified (before posting, =>)");
00667 TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
00668 s->assign(a,sol);
00669 s->post();
00670 CHECK_TEST(!s->failed(), "Failed");
00671 CHECK_TEST(subsumed(*s), "No subsumption");
00672 if (sol == MT_TRUE) {
00673 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
00674 } else if ((sol = MT_FALSE) && s->r.var().assigned()) {
00675 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
00676 }
00677 delete s;
00678 }
00679 if (pmi()) {
00680 START_TEST("Assignment reified (before posting, <=)");
00681 TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
00682 s->assign(a,sol);
00683 s->post();
00684 CHECK_TEST(!s->failed(), "Failed");
00685 CHECK_TEST(subsumed(*s), "No subsumption");
00686 if (sol == MT_TRUE) {
00687 if (s->r.var().assigned()) {
00688 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
00689 }
00690 } else if (sol == MT_FALSE) {
00691 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
00692 }
00693 delete s;
00694 }
00695 if (eqv()) {
00696 START_TEST("Assignment reified (after posting, <=>)");
00697 TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
00698 s->post();
00699 s->assign(a,sol);
00700 CHECK_TEST(!s->failed(), "Failed");
00701 CHECK_TEST(subsumed(*s), "No subsumption");
00702 if (s->r.var().assigned()) {
00703 if (sol == MT_TRUE) {
00704 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
00705 } else if (sol == MT_FALSE) {
00706 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
00707 }
00708 }
00709 delete s;
00710 }
00711 if (imp()) {
00712 START_TEST("Assignment reified (after posting, =>)");
00713 TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
00714 s->post();
00715 s->assign(a,sol);
00716 CHECK_TEST(!s->failed(), "Failed");
00717 CHECK_TEST(subsumed(*s), "No subsumption");
00718 if (sol == MT_TRUE) {
00719 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
00720 } else if (s->r.var().assigned()) {
00721 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
00722 }
00723 delete s;
00724 }
00725 if (pmi()) {
00726 START_TEST("Assignment reified (after posting, <=)");
00727 TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
00728 s->post();
00729 s->assign(a,sol);
00730 CHECK_TEST(!s->failed(), "Failed");
00731 CHECK_TEST(subsumed(*s), "No subsumption");
00732 if (sol == MT_TRUE) {
00733 if (s->r.var().assigned()) {
00734 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
00735 }
00736 } else if (sol == MT_FALSE) {
00737 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
00738 }
00739 delete s;
00740 }
00741 if (eqv()) {
00742 START_TEST("Prune reified, <=>");
00743 TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
00744 s->post();
00745 while (!s->failed() && !s->matchAssignment(a) &&
00746 (!s->assigned() || !s->r.var().assigned()))
00747 if (!s->prune(a,testfix)) {
00748 problem = "No fixpoint";
00749 delete s;
00750 goto failed;
00751 }
00752 CHECK_TEST(!s->failed(), "Failed");
00753 CHECK_TEST(subsumed(*s), "No subsumption");
00754 if (s->r.var().assigned()) {
00755 if (sol == MT_TRUE) {
00756 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
00757 } else if (sol == MT_FALSE) {
00758 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
00759 }
00760 }
00761 delete s;
00762 }
00763 if (imp()) {
00764 START_TEST("Prune reified, =>");
00765 TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
00766 s->post();
00767 while (!s->failed() && !s->matchAssignment(a) &&
00768 (!s->assigned() || ((sol == MT_FALSE) &&
00769 !s->r.var().assigned())))
00770 if (!s->prune(a,testfix)) {
00771 problem = "No fixpoint";
00772 delete s;
00773 goto failed;
00774 }
00775 CHECK_TEST(!s->failed(), "Failed");
00776 CHECK_TEST(subsumed(*s), "No subsumption");
00777 if (sol == MT_TRUE) {
00778 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
00779 } else if ((sol == MT_FALSE) && s->r.var().assigned()) {
00780 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
00781 }
00782 delete s;
00783 }
00784 if (pmi()) {
00785 START_TEST("Prune reified, <=");
00786 TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
00787 s->post();
00788 while (!s->failed() && !s->matchAssignment(a) &&
00789 (!s->assigned() || ((sol == MT_TRUE) &&
00790 !s->r.var().assigned())))
00791 if (!s->prune(a,testfix)) {
00792 problem = "No fixpoint";
00793 delete s;
00794 goto failed;
00795 }
00796 CHECK_TEST(!s->failed(), "Failed");
00797 CHECK_TEST(subsumed(*s), "No subsumption");
00798 if ((sol == MT_TRUE) && s->r.var().assigned()) {
00799 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
00800 } else if (sol == MT_FALSE) {
00801 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
00802 }
00803 delete s;
00804 }
00805 }
00806
00807 if (testsearch) {
00808 if (sol == MT_TRUE) {
00809 START_TEST("Search");
00810 if (!search_s->failed()) {
00811 TestSpace* ss = static_cast<TestSpace*>(search_s->clone(false));
00812 ss->dropUntil(a);
00813 delete e_s;
00814 e_s = new DFS<TestSpace>(ss,search_o);
00815 delete ss;
00816 }
00817 TestSpace* s = e_s->next();
00818 CHECK_TEST(s != NULL, "Solutions exhausted");
00819 CHECK_TEST(subsumed(*s), "No subsumption");
00820 for (int i=a.size(); i--; ) {
00821 CHECK_TEST(s->x[i].assigned(), "Unassigned variable");
00822 CHECK_TEST(Gecode::Float::overlap(a[i], s->x[i].val()), "Wrong value in solution");
00823 }
00824 delete s;
00825 }
00826 }
00827
00828 ++a;
00829 }
00830
00831 if (testsearch) {
00832 test = "Search";
00833 if (!search_s->failed()) {
00834 TestSpace* ss = static_cast<TestSpace*>(search_s->clone(false));
00835 ss->dropUntil(a);
00836 delete e_s;
00837 e_s = new DFS<TestSpace>(ss,search_o);
00838 delete ss;
00839 }
00840 if (e_s->next() != NULL) {
00841 problem = "Excess solutions";
00842 goto failed;
00843 }
00844 }
00845
00846 delete ap;
00847 delete search_s;
00848 delete e_s;
00849 return true;
00850
00851 failed:
00852 if (opt.log)
00853 olog << "FAILURE" << std::endl
00854 << ind(1) << "Test: " << test << std::endl
00855 << ind(1) << "Problem: " << problem << std::endl;
00856 if (a() && opt.log)
00857 olog << ind(1) << "Assignment: " << a << std::endl;
00858 delete ap;
00859 delete search_s;
00860 delete e_s;
00861
00862 return false;
00863 }
00864
00865 }}
00866
00867 #undef START_TEST
00868 #undef CHECK_TEST
00869
00870