Generated on Mon May 10 06:46:30 2010 for Gecode by doxygen 1.6.3

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