Generated on Thu Apr 11 13:59:01 2019 for Gecode by doxygen 1.6.3

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