Generated on Tue Dec 13 2011 10:02:04 for Gecode by doxygen 1.7.4
flatzinc.cpp
Go to the documentation of this file.
00001 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
00002 /*
00003  *  Main authors:
00004  *     Guido Tack <tack@gecode.org>
00005  *
00006  *  Copyright:
00007  *     Guido Tack, 2007
00008  *
00009  *  Last modified:
00010  *     $Date: 2011-09-21 11:18:38 +0200 (Wed, 21 Sep 2011) $ by $Author: tack $
00011  *     $Revision: 12410 $
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/flatzinc.hh>
00039 #include <gecode/flatzinc/registry.hh>
00040 #include <gecode/flatzinc/plugin.hh>
00041 
00042 #include <gecode/search.hh>
00043 
00044 #include <vector>
00045 #include <string>
00046 using namespace std;
00047 
00048 namespace Gecode { namespace FlatZinc {
00049 
00050   IntSet vs2is(IntVarSpec* vs) {
00051     if (vs->assigned) {
00052       return IntSet(vs->i,vs->i);
00053     }
00054     if (vs->domain()) {
00055       AST::SetLit* sl = vs->domain.some();
00056       if (sl->interval) {
00057         return IntSet(sl->min, sl->max);
00058       } else {
00059         int* newdom = heap.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
00060         for (int i=sl->s.size(); i--;)
00061           newdom[i] = sl->s[i];
00062         IntSet ret(newdom, sl->s.size());
00063         heap.free(newdom, static_cast<unsigned long int>(sl->s.size()));
00064         return ret;
00065       }
00066     }
00067     return IntSet(Int::Limits::min, Int::Limits::max);
00068   }
00069 
00070   int vs2bsl(BoolVarSpec* bs) {
00071     if (bs->assigned) {
00072       return bs->i;
00073     }
00074     if (bs->domain()) {
00075       AST::SetLit* sl = bs->domain.some();
00076       assert(sl->interval);
00077       return std::min(1, std::max(0, sl->min));
00078     }
00079     return 0;
00080   }
00081 
00082   int vs2bsh(BoolVarSpec* bs) {
00083     if (bs->assigned) {
00084       return bs->i;
00085     }
00086     if (bs->domain()) {
00087       AST::SetLit* sl = bs->domain.some();
00088       assert(sl->interval);
00089       return std::max(0, std::min(1, sl->max));
00090     }
00091     return 1;
00092   }
00093 
00094   TieBreakVarBranch<IntVarBranch> ann2ivarsel(AST::Node* ann) {
00095     if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00096       if (s->id == "input_order")
00097         return TieBreakVarBranch<IntVarBranch>(INT_VAR_NONE);
00098       if (s->id == "first_fail")
00099         return TieBreakVarBranch<IntVarBranch>(INT_VAR_SIZE_MIN);
00100       if (s->id == "anti_first_fail")
00101         return TieBreakVarBranch<IntVarBranch>(INT_VAR_SIZE_MAX);
00102       if (s->id == "smallest")
00103         return TieBreakVarBranch<IntVarBranch>(INT_VAR_MIN_MIN);
00104       if (s->id == "largest")
00105         return TieBreakVarBranch<IntVarBranch>(INT_VAR_MAX_MAX);
00106       if (s->id == "occurrence")
00107         return TieBreakVarBranch<IntVarBranch>(INT_VAR_DEGREE_MAX);
00108       if (s->id == "max_regret")
00109         return TieBreakVarBranch<IntVarBranch>(INT_VAR_REGRET_MIN_MAX);
00110       if (s->id == "most_constrained")
00111         return TieBreakVarBranch<IntVarBranch>(INT_VAR_SIZE_MIN,
00112           INT_VAR_DEGREE_MAX);
00113       if (s->id == "random")
00114         return TieBreakVarBranch<IntVarBranch>(INT_VAR_RND);
00115       if (s->id == "afc_min")
00116         return TieBreakVarBranch<IntVarBranch>(INT_VAR_AFC_MIN);
00117       if (s->id == "afc_max")
00118         return TieBreakVarBranch<IntVarBranch>(INT_VAR_AFC_MAX);
00119       if (s->id == "size_afc_min")
00120         return TieBreakVarBranch<IntVarBranch>(INT_VAR_SIZE_AFC_MIN);
00121       if (s->id == "size_afc_max")
00122         return TieBreakVarBranch<IntVarBranch>(INT_VAR_SIZE_AFC_MAX);
00123     }
00124     std::cerr << "Warning, ignored search annotation: ";
00125     ann->print(std::cerr);
00126     std::cerr << std::endl;
00127     return TieBreakVarBranch<IntVarBranch>(INT_VAR_NONE);
00128   }
00129 
00130   IntValBranch ann2ivalsel(AST::Node* ann) {
00131     if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00132       if (s->id == "indomain_min")
00133         return INT_VAL_MIN;
00134       if (s->id == "indomain_max")
00135         return INT_VAL_MAX;
00136       if (s->id == "indomain_median")
00137         return INT_VAL_MED;
00138       if (s->id == "indomain_split")
00139         return INT_VAL_SPLIT_MIN;
00140       if (s->id == "indomain_reverse_split")
00141         return INT_VAL_SPLIT_MAX;
00142       if (s->id == "indomain_random")
00143         return INT_VAL_RND;
00144       if (s->id == "indomain")
00145         return INT_VALUES_MIN;
00146       if (s->id == "indomain_middle") {
00147         std::cerr << "Warning, replacing unsupported annotation "
00148                   << "indomain_middle with indomain_median" << std::endl;
00149         return INT_VAL_MED;
00150       }
00151       if (s->id == "indomain_interval") {
00152         std::cerr << "Warning, replacing unsupported annotation "
00153                   << "indomain_interval with indomain_split" << std::endl;
00154         return INT_VAL_SPLIT_MIN;
00155       }
00156     }
00157     std::cerr << "Warning, ignored search annotation: ";
00158     ann->print(std::cerr);
00159     std::cerr << std::endl;
00160     return INT_VAL_MIN;
00161   }
00162 
00163   IntAssign ann2asnivalsel(AST::Node* ann) {
00164     if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00165       if (s->id == "indomain_min")
00166         return INT_ASSIGN_MIN;
00167       if (s->id == "indomain_max")
00168         return INT_ASSIGN_MAX;
00169       if (s->id == "indomain_median")
00170         return INT_ASSIGN_MED;
00171       if (s->id == "indomain_random")
00172         return INT_ASSIGN_RND;
00173     }
00174     std::cerr << "Warning, ignored search annotation: ";
00175     ann->print(std::cerr);
00176     std::cerr << std::endl;
00177     return INT_ASSIGN_MIN;
00178   }
00179 
00180 #ifdef GECODE_HAS_SET_VARS
00181   SetVarBranch ann2svarsel(AST::Node* ann) {
00182     if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00183       if (s->id == "input_order")
00184         return SET_VAR_NONE;
00185       if (s->id == "first_fail")
00186         return SET_VAR_SIZE_MIN;
00187       if (s->id == "anti_first_fail")
00188         return SET_VAR_SIZE_MAX;
00189       if (s->id == "smallest")
00190         return SET_VAR_MIN_MIN;
00191       if (s->id == "largest")
00192         return SET_VAR_MIN_MAX;
00193     }
00194     std::cerr << "Warning, ignored search annotation: ";
00195     ann->print(std::cerr);
00196     std::cerr << std::endl;
00197     return SET_VAR_NONE;
00198   }
00199 
00200   SetValBranch ann2svalsel(AST::Node* ann) {
00201     if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00202       if (s->id == "indomain_min")
00203         return SET_VAL_MIN_INC;
00204       if (s->id == "indomain_max")
00205         return SET_VAL_MAX_INC;
00206       if (s->id == "outdomain_min")
00207         return SET_VAL_MIN_EXC;
00208       if (s->id == "outdomain_max")
00209         return SET_VAL_MAX_EXC;
00210     }
00211     std::cerr << "Warning, ignored search annotation: ";
00212     ann->print(std::cerr);
00213     std::cerr << std::endl;
00214     return SET_VAL_MIN_INC;
00215   }
00216 #endif
00217 
00218   FlatZincSpace::FlatZincSpace(bool share, FlatZincSpace& f)
00219     : Space(share, f), _solveAnnotations(NULL), iv_boolalias(NULL) {
00220       _optVar = f._optVar;
00221       _method = f._method;
00222       iv.update(*this, share, f.iv);
00223       intVarCount = f.intVarCount;
00224       bv.update(*this, share, f.bv);
00225       boolVarCount = f.boolVarCount;
00226 #ifdef GECODE_HAS_SET_VARS
00227       sv.update(*this, share, f.sv);
00228       setVarCount = f.setVarCount;
00229 #endif
00230     }
00231   
00232   FlatZincSpace::FlatZincSpace(void)
00233   : intVarCount(-1), boolVarCount(-1), setVarCount(-1), _optVar(-1),
00234     _solveAnnotations(NULL) {}
00235 
00236   void
00237   FlatZincSpace::init(int intVars, int boolVars,
00238 #ifdef GECODE_HAS_SET_VARS
00239                                  int setVars) {
00240 #else
00241                                  int) {
00242 #endif
00243     intVarCount = 0;
00244     iv = IntVarArray(*this, intVars);
00245     iv_introduced = std::vector<bool>(intVars);
00246     iv_boolalias = alloc<int>(intVars+(intVars==0?1:0));
00247     boolVarCount = 0;
00248     bv = BoolVarArray(*this, boolVars);
00249     bv_introduced = std::vector<bool>(boolVars);
00250 #ifdef GECODE_HAS_SET_VARS
00251     setVarCount = 0;
00252     sv = SetVarArray(*this, setVars);
00253     sv_introduced = std::vector<bool>(setVars);
00254 #endif
00255   }
00256 
00257   void
00258   FlatZincSpace::newIntVar(IntVarSpec* vs) {
00259     if (vs->alias) {
00260       iv[intVarCount++] = iv[vs->i];
00261     } else {
00262       iv[intVarCount++] = IntVar(*this, vs2is(vs));
00263     }
00264     iv_introduced[intVarCount-1] = vs->introduced;
00265     iv_boolalias[intVarCount-1] = -1;
00266   }
00267 
00268   void
00269   FlatZincSpace::aliasBool2Int(int iv, int bv) {
00270     iv_boolalias[iv] = bv;
00271   }
00272   int
00273   FlatZincSpace::aliasBool2Int(int iv) {
00274     return iv_boolalias[iv];
00275   }
00276 
00277   void
00278   FlatZincSpace::newBoolVar(BoolVarSpec* vs) {
00279     if (vs->alias) {
00280       bv[boolVarCount++] = bv[vs->i];
00281     } else {
00282       bv[boolVarCount++] = BoolVar(*this, vs2bsl(vs), vs2bsh(vs));
00283     }
00284     bv_introduced[boolVarCount-1] = vs->introduced;
00285   }
00286 
00287 #ifdef GECODE_HAS_SET_VARS
00288   void
00289   FlatZincSpace::newSetVar(SetVarSpec* vs) {
00290     if (vs->alias) {
00291       sv[setVarCount++] = sv[vs->i];
00292     } else if (vs->assigned) {
00293       assert(vs->upperBound());
00294       AST::SetLit* vsv = vs->upperBound.some();
00295       if (vsv->interval) {
00296         IntSet d(vsv->min, vsv->max);
00297         sv[setVarCount++] = SetVar(*this, d, d);
00298       } else {
00299         int* is = heap.alloc<int>(static_cast<unsigned long int>(vsv->s.size()));
00300         for (int i=vsv->s.size(); i--; )
00301           is[i] = vsv->s[i];
00302         IntSet d(is, vsv->s.size());
00303         heap.free(is,static_cast<unsigned long int>(vsv->s.size()));
00304         sv[setVarCount++] = SetVar(*this, d, d);
00305       }
00306     } else if (vs->upperBound()) {
00307       AST::SetLit* vsv = vs->upperBound.some();
00308       if (vsv->interval) {
00309         IntSet d(vsv->min, vsv->max);
00310         sv[setVarCount++] = SetVar(*this, IntSet::empty, d);
00311       } else {
00312         int* is = heap.alloc<int>(static_cast<unsigned long int>(vsv->s.size()));
00313         for (int i=vsv->s.size(); i--; )
00314           is[i] = vsv->s[i];
00315         IntSet d(is, vsv->s.size());
00316         heap.free(is,static_cast<unsigned long int>(vsv->s.size()));
00317         sv[setVarCount++] = SetVar(*this, IntSet::empty, d);
00318       }
00319     } else {
00320       sv[setVarCount++] = SetVar(*this, IntSet::empty,
00321                                  IntSet(Set::Limits::min, 
00322                                         Set::Limits::max));
00323     }
00324     sv_introduced[setVarCount-1] = vs->introduced;
00325   }
00326 #else
00327   void
00328   FlatZincSpace::newSetVar(SetVarSpec*) {
00329     throw FlatZinc::Error("Gecode", "set variables not supported");
00330   }
00331 #endif
00332 
00333   void
00334   FlatZincSpace::postConstraint(const ConExpr& ce, AST::Node* ann) {
00335     try {
00336       registry().post(*this, ce, ann);
00337     } catch (Gecode::Exception& e) {
00338       throw FlatZinc::Error("Gecode", e.what());
00339     } catch (AST::TypeError& e) {
00340       throw FlatZinc::Error("Type error", e.what());
00341     }
00342   }
00343 
00344   void flattenAnnotations(AST::Array* ann, std::vector<AST::Node*>& out) {
00345       for (unsigned int i=0; i<ann->a.size(); i++) {
00346         if (ann->a[i]->isCall("seq_search")) {
00347           AST::Call* c = ann->a[i]->getCall();
00348           if (c->args->isArray())
00349             flattenAnnotations(c->args->getArray(), out);
00350           else
00351             out.push_back(c->args);
00352         } else {
00353           out.push_back(ann->a[i]);
00354         }
00355       }
00356   }
00357 
00358   void
00359   FlatZincSpace::createBranchers(AST::Node* ann, int seed,
00360                                  bool ignoreUnknown,
00361                                  std::ostream& err) {
00362     VarBranchOptions varbo;
00363     varbo.seed = seed;
00364     ValBranchOptions valbo;
00365     valbo.seed = seed;
00366     if (ann) {
00367       std::vector<AST::Node*> flatAnn;
00368       if (ann->isArray()) {
00369         flattenAnnotations(ann->getArray()  , flatAnn);
00370       } else {
00371         flatAnn.push_back(ann);
00372       }
00373 
00374       for (unsigned int i=0; i<flatAnn.size(); i++) {
00375         if (flatAnn[i]->isCall("gecode_search")) {
00376           AST::Call* c = flatAnn[i]->getCall();
00377           branchWithPlugin(c->args);
00378         } else try {
00379           AST::Call *call = flatAnn[i]->getCall("int_search");
00380           AST::Array *args = call->getArgs(4);
00381           AST::Array *vars = args->a[0]->getArray();
00382           int k=vars->a.size();
00383           for (int i=vars->a.size(); i--;)
00384             if (vars->a[i]->isInt())
00385               k--;
00386           IntVarArgs va(k);
00387           k=0;
00388           for (unsigned int i=0; i<vars->a.size(); i++) {
00389             if (vars->a[i]->isInt())
00390               continue;
00391             va[k++] = iv[vars->a[i]->getIntVar()];
00392           }
00393           branch(*this, va, ann2ivarsel(args->a[1]), ann2ivalsel(args->a[2]),
00394                  varbo,valbo);
00395         } catch (AST::TypeError& e) {
00396         try {
00397           AST::Call *call = flatAnn[i]->getCall("int_assign");
00398           AST::Array *args = call->getArgs(2);
00399           AST::Array *vars = args->a[0]->getArray();
00400           int k=vars->a.size();
00401           for (int i=vars->a.size(); i--;)
00402             if (vars->a[i]->isInt())
00403               k--;
00404           IntVarArgs va(k);
00405           k=0;
00406           for (unsigned int i=0; i<vars->a.size(); i++) {
00407             if (vars->a[i]->isInt())
00408               continue;
00409             va[k++] = iv[vars->a[i]->getIntVar()];
00410           }
00411           assign(*this, va, ann2asnivalsel(args->a[1]));
00412         } catch (AST::TypeError& e) {
00413           (void) e;
00414           try {
00415             AST::Call *call = flatAnn[i]->getCall("bool_search");
00416             AST::Array *args = call->getArgs(4);
00417             AST::Array *vars = args->a[0]->getArray();
00418             int k=vars->a.size();
00419             for (int i=vars->a.size(); i--;)
00420               if (vars->a[i]->isBool())
00421                 k--;
00422             BoolVarArgs va(k);
00423             k=0;
00424             for (unsigned int i=0; i<vars->a.size(); i++) {
00425               if (vars->a[i]->isBool())
00426                 continue;
00427               va[k++] = bv[vars->a[i]->getBoolVar()];
00428             }
00429             branch(*this, va, ann2ivarsel(args->a[1]), 
00430                    ann2ivalsel(args->a[2]), varbo, valbo);
00431           } catch (AST::TypeError& e) {
00432             (void) e;
00433 #ifdef GECODE_HAS_SET_VARS
00434             try {
00435               AST::Call *call = flatAnn[i]->getCall("set_search");
00436               AST::Array *args = call->getArgs(4);
00437               AST::Array *vars = args->a[0]->getArray();
00438               int k=vars->a.size();
00439               for (int i=vars->a.size(); i--;)
00440                 if (vars->a[i]->isSet())
00441                   k--;
00442               SetVarArgs va(k);
00443               k=0;
00444               for (unsigned int i=0; i<vars->a.size(); i++) {
00445                 if (vars->a[i]->isSet())
00446                   continue;
00447                 va[k++] = sv[vars->a[i]->getSetVar()];
00448               }
00449               branch(*this, va, ann2svarsel(args->a[1]), 
00450                      ann2svalsel(args->a[2]), varbo, valbo);
00451             } catch (AST::TypeError& e) {
00452               (void) e;
00453               if (!ignoreUnknown) {
00454                 err << "Warning, ignored search annotation: ";
00455                 flatAnn[i]->print(err);
00456                 err << std::endl;
00457               }
00458             }
00459 #else
00460             if (!ignoreUnknown) {
00461               err << "Warning, ignored search annotation: ";
00462               flatAnn[i]->print(err);
00463               err << std::endl;
00464             }
00465 #endif
00466           }
00467         }
00468         }
00469       }
00470     }
00471     int introduced = 0;
00472     for (int i=iv.size(); i--;)
00473       if (iv_introduced[i])
00474         introduced++;
00475     IntVarArgs iv_sol(iv.size()-introduced);
00476     IntVarArgs iv_tmp(introduced);
00477     for (int i=iv.size(), j=0, k=0; i--;)
00478       if (iv_introduced[i])
00479         iv_tmp[j++] = iv[i];
00480       else
00481         iv_sol[k++] = iv[i];
00482 
00483     introduced = 0;
00484     for (int i=bv.size(); i--;)
00485       if (bv_introduced[i])
00486         introduced++;
00487     BoolVarArgs bv_sol(bv.size()-introduced);
00488     BoolVarArgs bv_tmp(introduced);
00489     for (int i=bv.size(), j=0, k=0; i--;)
00490       if (bv_introduced[i])
00491         bv_tmp[j++] = bv[i];
00492       else
00493         bv_sol[k++] = bv[i];
00494 
00495     branch(*this, iv_sol, INT_VAR_SIZE_AFC_MIN, INT_VAL_MIN);
00496     branch(*this, bv_sol, INT_VAR_AFC_MAX, INT_VAL_MIN);
00497 #ifdef GECODE_HAS_SET_VARS
00498     introduced = 0;
00499     for (int i=sv.size(); i--;)
00500       if (sv_introduced[i])
00501         introduced++;
00502     SetVarArgs sv_sol(sv.size()-introduced);
00503     SetVarArgs sv_tmp(introduced);
00504     for (int i=sv.size(), j=0, k=0; i--;)
00505       if (sv_introduced[i])
00506         sv_tmp[j++] = sv[i];
00507       else
00508         sv_sol[k++] = sv[i];
00509     branch(*this, sv_sol, SET_VAR_SIZE_AFC_MIN, SET_VAL_MIN_INC);
00510 #endif
00511     branch(*this, iv_tmp, INT_VAR_SIZE_AFC_MIN, INT_VAL_MIN);
00512     branch(*this, bv_tmp, INT_VAR_AFC_MAX, INT_VAL_MIN);
00513 #ifdef GECODE_HAS_SET_VARS
00514     branch(*this, sv_tmp, SET_VAR_SIZE_AFC_MIN, SET_VAL_MIN_INC);
00515 #endif
00516   }
00517 
00518   AST::Array*
00519   FlatZincSpace::solveAnnotations(void) const {
00520     return _solveAnnotations;
00521   }
00522 
00523   void
00524   FlatZincSpace::solve(AST::Array* ann) {
00525     _method = SAT;
00526     _solveAnnotations = ann;
00527   }
00528 
00529   void
00530   FlatZincSpace::minimize(int var, AST::Array* ann) {
00531     _method = MIN;
00532     _optVar = var;
00533     _solveAnnotations = ann;
00534     // Branch on optimization variable to ensure that it is given a value.
00535     AST::Array* args = new AST::Array(4);
00536     args->a[0] = new AST::Array(new AST::IntVar(_optVar));
00537     args->a[1] = new AST::Atom("input_order");
00538     args->a[2] = new AST::Atom("indomain_min");
00539     args->a[3] = new AST::Atom("complete");
00540     AST::Call* c = new AST::Call("int_search", args);
00541     if (!ann)
00542       ann = new AST::Array(c);
00543     else
00544       ann->a.push_back(c);
00545   }
00546 
00547   void
00548   FlatZincSpace::maximize(int var, AST::Array* ann) {
00549     _method = MAX;
00550     _optVar = var;
00551     _solveAnnotations = ann;
00552     // Branch on optimization variable to ensure that it is given a value.
00553     AST::Array* args = new AST::Array(4);
00554     args->a[0] = new AST::Array(new AST::IntVar(_optVar));
00555     args->a[1] = new AST::Atom("input_order");
00556     args->a[2] = new AST::Atom("indomain_min");
00557     args->a[3] = new AST::Atom("complete");
00558     AST::Call* c = new AST::Call("int_search", args);
00559     if (!ann)
00560       ann = new AST::Array(c);
00561     else
00562       ann->a.push_back(c);
00563   }
00564 
00565   FlatZincSpace::~FlatZincSpace(void) {
00566     delete _solveAnnotations;
00567   }
00568 
00569 #ifdef GECODE_HAS_GIST
00570 
00574   template<class Engine>
00575   class GistEngine {
00576   };
00577 
00579   template<typename S>
00580   class GistEngine<DFS<S> > {
00581   public:
00582     static void explore(S* root, const FlatZincOptions& opt,
00583                         Gist::Inspector* i) {
00584       Gecode::Gist::Options o;
00585       o.c_d = opt.c_d(); o.a_d = opt.a_d();
00586       o.inspect.click(i);
00587       (void) Gecode::Gist::dfs(root, o);
00588     }
00589   };
00590 
00592   template<typename S>
00593   class GistEngine<BAB<S> > {
00594   public:
00595     static void explore(S* root, const FlatZincOptions& opt,
00596                         Gist::Inspector* i) {
00597       Gecode::Gist::Options o;
00598       o.c_d = opt.c_d(); o.a_d = opt.a_d();
00599       o.inspect.click(i);
00600       (void) Gecode::Gist::bab(root, o);
00601     }
00602   };
00603 
00605   template<typename S>
00606   class GistEngine<Restart<S> > {
00607   public:
00608     static void explore(S* root, const FlatZincOptions& opt,
00609                         Gist::Inspector* i) {
00610       Gecode::Gist::Options o;
00611       o.c_d = opt.c_d(); o.a_d = opt.a_d();
00612       o.inspect.click(i);
00613       (void) Gecode::Gist::bab(root, o);
00614     }
00615   };
00616 
00618   template<class S>
00619   class FZPrintingInspector
00620    : public Gecode::Gist::TextOutput, public Gecode::Gist::Inspector {
00621   private:
00622     const Printer& p;
00623   public:
00625     FZPrintingInspector(const Printer& p0);
00627     virtual void inspect(const Space& node);
00629     virtual void finalize(void);
00630   };
00631 
00632   template<class S>
00633   FZPrintingInspector<S>::FZPrintingInspector(const Printer& p0)
00634   : TextOutput("Gecode/FlatZinc"), p(p0) {}
00635 
00636   template<class S>
00637   void
00638   FZPrintingInspector<S>::inspect(const Space& node) {
00639     init();
00640     dynamic_cast<const S&>(node).print(getStream(), p);
00641     getStream() << std::endl;
00642   }
00643 
00644   template<class S>
00645   void
00646   FZPrintingInspector<S>::finalize(void) {
00647     Gecode::Gist::TextOutput::finalize();
00648   }
00649 
00650 #endif
00651 
00652   template<template<class> class Engine>
00653   void
00654   FlatZincSpace::runEngine(std::ostream& out, const Printer& p,
00655                             const FlatZincOptions& opt, Support::Timer& t_total) {
00656 #ifdef GECODE_HAS_GIST
00657     if (opt.mode() == SM_GIST) {
00658       FZPrintingInspector<FlatZincSpace> pi(p);
00659       (void) GistEngine<Engine<FlatZincSpace> >::explore(this,opt,&pi);
00660       return;
00661     }
00662 #endif
00663     StatusStatistics sstat;
00664     unsigned int n_p = 0;
00665     Support::Timer t_solve;
00666     t_solve.start();
00667     if (status(sstat) != SS_FAILED) {
00668       n_p = propagators();
00669     }
00670     Search::Options o;
00671     o.stop = Driver::Cutoff::create(opt.node(), opt.fail(), opt.time(), 
00672                                     true);
00673     o.c_d = opt.c_d();
00674     o.a_d = opt.a_d();
00675     o.threads = opt.threads();
00676     Driver::Cutoff::installCtrlHandler(true);
00677     Engine<FlatZincSpace> se(this,o);
00678     int noOfSolutions = _method == SAT ? opt.solutions() : 0;
00679     int findSol = noOfSolutions;
00680     FlatZincSpace* sol = NULL;
00681     while (FlatZincSpace* next_sol = se.next()) {
00682       delete sol;
00683       sol = next_sol;
00684       if (opt.print()==0) {
00685         sol->print(out, p);
00686         out << "----------" << std::endl;
00687       }
00688       if (--findSol==0)
00689         goto stopped;
00690     }
00691     if (sol && opt.print()!=0) {
00692       sol->print(out, p);
00693       out << "----------" << std::endl;
00694     }
00695     if (!se.stopped()) {
00696       if (sol) {
00697         out << "==========" << endl;
00698       } else {
00699         out << "=====UNSATISFIABLE=====" << endl;
00700       }
00701     } else if (!sol) {
00702         out << "=====UNKNOWN=====" << endl;
00703     }
00704     delete sol;
00705     stopped:
00706     Driver::Cutoff::installCtrlHandler(false);
00707     if (opt.mode() == SM_STAT) {
00708       Gecode::Search::Statistics stat = se.statistics();
00709       out << endl
00710            << "%%  runtime:       ";
00711       Driver::stop(t_total,out);
00712       out << endl
00713            << "%%  solvetime:     ";
00714       Driver::stop(t_solve,out);
00715       out << endl
00716            << "%%  solutions:     " 
00717            << std::abs(noOfSolutions - findSol) << endl
00718            << "%%  variables:     " 
00719            << (intVarCount + boolVarCount + setVarCount) << endl
00720            << "%%  propagators:   " << n_p << endl
00721            << "%%  propagations:  " << sstat.propagate+stat.propagate << endl
00722            << "%%  nodes:         " << stat.node << endl
00723            << "%%  failures:      " << stat.fail << endl
00724            << "%%  peak depth:    " << stat.depth << endl
00725            << "%%  peak memory:   "
00726            << static_cast<int>((stat.memory+1023) / 1024) << " KB"
00727            << endl;
00728     }
00729   }
00730 
00731 #ifdef GECODE_HAS_QT
00732   void
00733   FlatZincSpace::branchWithPlugin(AST::Node* ann) {
00734     if (AST::Call* c = dynamic_cast<AST::Call*>(ann)) {
00735       QString pluginName(c->id.c_str());
00736       if (QLibrary::isLibrary(pluginName+".dll")) {
00737         pluginName += ".dll";
00738       } else if (QLibrary::isLibrary(pluginName+".dylib")) {
00739         pluginName = "lib" + pluginName + ".dylib";
00740       } else if (QLibrary::isLibrary(pluginName+".so")) {
00741         // Must check .so after .dylib so that Mac OS uses .dylib
00742         pluginName = "lib" + pluginName + ".so";
00743       }
00744       QPluginLoader pl(pluginName);
00745       QObject* plugin_o = pl.instance();
00746       if (!plugin_o) {
00747         throw FlatZinc::Error("FlatZinc",
00748           "Error loading plugin "+pluginName.toStdString()+
00749           ": "+pl.errorString().toStdString());
00750       }
00751       BranchPlugin* pb = qobject_cast<BranchPlugin*>(plugin_o);
00752       if (!pb) {
00753         throw FlatZinc::Error("FlatZinc",
00754         "Error loading plugin "+pluginName.toStdString()+
00755         ": does not contain valid PluginBrancher");
00756       }
00757       pb->branch(*this, c);
00758     }
00759   }
00760 #else
00761   void
00762   FlatZincSpace::branchWithPlugin(AST::Node* ann) {
00763     throw FlatZinc::Error("FlatZinc",
00764       "Branching with plugins not supported (requires Qt support)");
00765   }
00766 #endif
00767 
00768   void
00769   FlatZincSpace::run(std::ostream& out, const Printer& p,
00770                       const FlatZincOptions& opt, Support::Timer& t_total) {
00771     switch (_method) {
00772     case MIN:
00773     case MAX:
00774       if (opt.search() == FlatZincOptions::FZ_SEARCH_BAB)
00775         runEngine<BAB>(out,p,opt,t_total);
00776       else
00777         runEngine<Restart>(out,p,opt,t_total);
00778       break;
00779     case SAT:
00780       runEngine<DFS>(out,p,opt,t_total);
00781       break;
00782     }
00783   }
00784 
00785   void
00786   FlatZincSpace::constrain(const Space& s) {
00787     if (_method == MIN)
00788       rel(*this, iv[_optVar], IRT_LE, 
00789                  static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
00790     else if (_method == MAX)
00791       rel(*this, iv[_optVar], IRT_GR,
00792                  static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
00793   }
00794 
00795   Space*
00796   FlatZincSpace::copy(bool share) {
00797     return new FlatZincSpace(share, *this);
00798   }
00799 
00800   FlatZincSpace::Meth
00801   FlatZincSpace::method(void) const {
00802     return _method;
00803   }
00804 
00805   int
00806   FlatZincSpace::optVar(void) const {
00807     return _optVar;
00808   }
00809 
00810   void
00811   FlatZincSpace::print(std::ostream& out, const Printer& p) const {
00812     p.print(out, iv, bv
00813 #ifdef GECODE_HAS_SET_VARS
00814     , sv
00815 #endif
00816     );
00817   }
00818 
00819   void
00820   FlatZincSpace::shrinkArrays(Printer& p) {
00821     p.shrinkArrays(*this, _optVar, iv, bv
00822 #ifdef GECODE_HAS_SET_VARS
00823     , sv
00824 #endif
00825     );
00826   }
00827 
00828   void
00829   Printer::init(AST::Array* output) {
00830     _output = output;
00831   }
00832 
00833   void
00834   Printer::printElem(std::ostream& out,
00835                        AST::Node* ai,
00836                        const Gecode::IntVarArray& iv,
00837                        const Gecode::BoolVarArray& bv
00838 #ifdef GECODE_HAS_SET_VARS
00839                        , const Gecode::SetVarArray& sv
00840 #endif
00841                        ) const {
00842     int k;
00843     if (ai->isInt(k)) {
00844       out << k;
00845     } else if (ai->isIntVar()) {
00846       out << iv[ai->getIntVar()];
00847     } else if (ai->isBoolVar()) {
00848       if (bv[ai->getBoolVar()].min() == 1) {
00849         out << "true";
00850       } else if (bv[ai->getBoolVar()].max() == 0) {
00851         out << "false";
00852       } else {
00853         out << "false..true";
00854       }
00855 #ifdef GECODE_HAS_SET_VARS
00856     } else if (ai->isSetVar()) {
00857       if (!sv[ai->getSetVar()].assigned()) {
00858         out << sv[ai->getSetVar()];
00859         return;
00860       }
00861       SetVarGlbRanges svr(sv[ai->getSetVar()]);
00862       if (!svr()) {
00863         out << "{}";
00864         return;
00865       }
00866       int min = svr.min();
00867       int max = svr.max();
00868       ++svr;
00869       if (svr()) {
00870         SetVarGlbValues svv(sv[ai->getSetVar()]);
00871         int i = svv.val();
00872         out << "{" << i;
00873         ++svv;
00874         for (; svv(); ++svv)
00875           out << ", " << svv.val();
00876         out << "}";
00877       } else {
00878         out << min << ".." << max;
00879       }
00880 #endif
00881     } else if (ai->isBool()) {
00882       out << (ai->getBool() ? "true" : "false");
00883     } else if (ai->isSet()) {
00884       AST::SetLit* s = ai->getSet();
00885       if (s->interval) {
00886         out << s->min << ".." << s->max;
00887       } else {
00888         out << "{";
00889         for (unsigned int i=0; i<s->s.size(); i++) {
00890           out << s->s[i] << (i < s->s.size()-1 ? ", " : "}");
00891         }
00892       }
00893     } else if (ai->isString()) {
00894       std::string s = ai->getString();
00895       for (unsigned int i=0; i<s.size(); i++) {
00896         if (s[i] == '\\' && i<s.size()-1) {
00897           switch (s[i+1]) {
00898           case 'n': out << "\n"; break;
00899           case '\\': out << "\\"; break;
00900           case 't': out << "\t"; break;
00901           default: out << "\\" << s[i+1];
00902           }
00903           i++;
00904         } else {
00905           out << s[i];
00906         }
00907       }
00908     }
00909   }
00910 
00911   void
00912   Printer::print(std::ostream& out,
00913                    const Gecode::IntVarArray& iv,
00914                    const Gecode::BoolVarArray& bv
00915 #ifdef GECODE_HAS_SET_VARS
00916                    ,
00917                    const Gecode::SetVarArray& sv
00918 #endif
00919                    ) const {
00920     if (_output == NULL)
00921       return;
00922     for (unsigned int i=0; i< _output->a.size(); i++) {
00923       AST::Node* ai = _output->a[i];
00924       if (ai->isArray()) {
00925         AST::Array* aia = ai->getArray();
00926         int size = aia->a.size();
00927         out << "[";
00928         for (int j=0; j<size; j++) {
00929           printElem(out,aia->a[j],iv,bv
00930 #ifdef GECODE_HAS_SET_VARS
00931           ,sv
00932 #endif
00933           );
00934           if (j<size-1)
00935             out << ", ";
00936         }
00937         out << "]";
00938       } else {
00939         printElem(out,ai,iv,bv
00940 #ifdef GECODE_HAS_SET_VARS
00941         ,sv
00942 #endif
00943         );
00944       }
00945     }
00946   }
00947 
00948   void
00949   Printer::shrinkElement(AST::Node* node,
00950                          std::map<int,int>& iv, std::map<int,int>& bv, 
00951                          std::map<int,int>& sv) {
00952     if (node->isIntVar()) {
00953       AST::IntVar* x = static_cast<AST::IntVar*>(node);
00954       if (iv.find(x->i) == iv.end()) {
00955         int newi = iv.size();
00956         iv[x->i] = newi;
00957       }
00958       x->i = iv[x->i];
00959     } else if (node->isBoolVar()) {
00960       AST::BoolVar* x = static_cast<AST::BoolVar*>(node);
00961       if (bv.find(x->i) == bv.end()) {
00962         int newi = bv.size();
00963         bv[x->i] = newi;
00964       }
00965       x->i = bv[x->i];
00966     } else if (node->isSetVar()) {
00967       AST::SetVar* x = static_cast<AST::SetVar*>(node);
00968       if (sv.find(x->i) == sv.end()) {
00969         int newi = sv.size();
00970         sv[x->i] = newi;
00971       }
00972       x->i = sv[x->i];      
00973     }
00974   }
00975 
00976   void
00977   Printer::shrinkArrays(Space& home,
00978                         int& optVar,
00979                         Gecode::IntVarArray& iv,
00980                         Gecode::BoolVarArray& bv
00981 #ifdef GECODE_HAS_SET_VARS
00982                         ,
00983                         Gecode::SetVarArray& sv
00984 #endif
00985                        ) {
00986     if (_output == NULL) {
00987       if (optVar == -1) {
00988         iv = IntVarArray(home, 0);
00989       } else {
00990         IntVar ov = iv[optVar];
00991         iv = IntVarArray(home, 1);
00992         iv[0] = ov;
00993         optVar = 0;
00994       }
00995       bv = BoolVarArray(home, 0);
00996 #ifdef GECODE_HAS_SET_VARS
00997       sv = SetVarArray(home, 0);
00998 #endif
00999       return;
01000     }
01001     std::map<int,int> iv_new;
01002     std::map<int,int> bv_new;
01003     std::map<int,int> sv_new;
01004 
01005     if (optVar != -1) {
01006       iv_new[optVar] = 0;
01007       optVar = 0;
01008     }
01009 
01010     for (unsigned int i=0; i< _output->a.size(); i++) {
01011       AST::Node* ai = _output->a[i];
01012       if (ai->isArray()) {
01013         AST::Array* aia = ai->getArray();
01014         for (unsigned int j=0; j<aia->a.size(); j++) {
01015           shrinkElement(aia->a[j],iv_new,bv_new,sv_new);
01016         }
01017       } else {
01018         shrinkElement(ai,iv_new,bv_new,sv_new);
01019       }
01020     }
01021 
01022     IntVarArgs iva(iv_new.size());
01023     for (map<int,int>::iterator i=iv_new.begin(); i != iv_new.end(); ++i) {
01024       iva[(*i).second] = iv[(*i).first];
01025     }
01026     iv = IntVarArray(home, iva);
01027 
01028     BoolVarArgs bva(bv_new.size());
01029     for (map<int,int>::iterator i=bv_new.begin(); i != bv_new.end(); ++i) {
01030       bva[(*i).second] = bv[(*i).first];
01031     }
01032     bv = BoolVarArray(home, bva);
01033 
01034 #ifdef GECODE_HAS_SET_VARS
01035     SetVarArgs sva(sv_new.size());
01036     for (map<int,int>::iterator i=sv_new.begin(); i != sv_new.end(); ++i) {
01037       sva[(*i).second] = sv[(*i).first];
01038     }
01039     sv = SetVarArray(home, sva);
01040 #endif
01041   }
01042 
01043   Printer::~Printer(void) {
01044     delete _output;
01045   }
01046 
01047 }}
01048 
01049 // STATISTICS: flatzinc-any