Generated on Tue Jul 27 2010 21:59:09 for Gecode by doxygen 1.7.1

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-05-11 12:33:38 +0200 (Tue, 11 May 2010) $ by $Author: tack $
00011  *     $Revision: 10940 $
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     if (ann) {
00352       std::vector<AST::Node*> flatAnn;
00353       if (ann->isArray()) {
00354         flattenAnnotations(ann->getArray()  , flatAnn);
00355       } else {
00356         flatAnn.push_back(ann);
00357       }
00358 
00359       for (unsigned int i=0; i<flatAnn.size(); i++) {
00360         if (flatAnn[i]->isCall("gecode_search")) {
00361           AST::Call* c = flatAnn[i]->getCall();
00362           branchWithPlugin(c->args);
00363         } else try {
00364           AST::Call *call = flatAnn[i]->getCall("int_search");
00365           AST::Array *args = call->getArgs(4);
00366           AST::Array *vars = args->a[0]->getArray();
00367           int k=vars->a.size();
00368           for (int i=vars->a.size(); i--;)
00369             if (vars->a[i]->isInt())
00370               k--;
00371           IntVarArgs va(k);
00372           k=0;
00373           for (unsigned int i=0; i<vars->a.size(); i++) {
00374             if (vars->a[i]->isInt())
00375               continue;
00376             va[k++] = iv[vars->a[i]->getIntVar()];
00377           }
00378           branch(*this, va, ann2ivarsel(args->a[1]), ann2ivalsel(args->a[2]));
00379         } catch (AST::TypeError& e) {
00380         try {
00381           AST::Call *call = flatAnn[i]->getCall("int_assign");
00382           AST::Array *args = call->getArgs(2);
00383           AST::Array *vars = args->a[0]->getArray();
00384           int k=vars->a.size();
00385           for (int i=vars->a.size(); i--;)
00386             if (vars->a[i]->isInt())
00387               k--;
00388           IntVarArgs va(k);
00389           k=0;
00390           for (unsigned int i=0; i<vars->a.size(); i++) {
00391             if (vars->a[i]->isInt())
00392               continue;
00393             va[k++] = iv[vars->a[i]->getIntVar()];
00394           }
00395           assign(*this, va, ann2asnivalsel(args->a[1]));
00396         } catch (AST::TypeError& e) {
00397           (void) e;
00398           try {
00399             AST::Call *call = flatAnn[i]->getCall("bool_search");
00400             AST::Array *args = call->getArgs(4);
00401             AST::Array *vars = args->a[0]->getArray();
00402             int k=vars->a.size();
00403             for (int i=vars->a.size(); i--;)
00404               if (vars->a[i]->isBool())
00405                 k--;
00406             BoolVarArgs va(k);
00407             k=0;
00408             for (unsigned int i=0; i<vars->a.size(); i++) {
00409               if (vars->a[i]->isBool())
00410                 continue;
00411               va[k++] = bv[vars->a[i]->getBoolVar()];
00412             }
00413             branch(*this, va, ann2ivarsel(args->a[1]), 
00414                    ann2ivalsel(args->a[2]));        
00415           } catch (AST::TypeError& e) {
00416             (void) e;
00417 #ifdef GECODE_HAS_SET_VARS
00418             try {
00419               AST::Call *call = flatAnn[i]->getCall("set_search");
00420               AST::Array *args = call->getArgs(4);
00421               AST::Array *vars = args->a[0]->getArray();
00422               int k=vars->a.size();
00423               for (int i=vars->a.size(); i--;)
00424                 if (vars->a[i]->isSet())
00425                   k--;
00426               SetVarArgs va(k);
00427               k=0;
00428               for (unsigned int i=0; i<vars->a.size(); i++) {
00429                 if (vars->a[i]->isSet())
00430                   continue;
00431                 va[k++] = sv[vars->a[i]->getSetVar()];
00432               }
00433               branch(*this, va, ann2svarsel(args->a[1]), 
00434                                ann2svalsel(args->a[2]));        
00435             } catch (AST::TypeError& e) {
00436               (void) e;
00437               if (!ignoreUnknown) {
00438                 err << "Warning, ignored search annotation: ";
00439                 flatAnn[i]->print(err);
00440                 err << std::endl;
00441               }
00442             }
00443 #else
00444             if (!ignoreUnknown) {
00445               err << "Warning, ignored search annotation: ";
00446               flatAnn[i]->print(err);
00447               err << std::endl;
00448             }
00449 #endif
00450           }
00451         }
00452         }
00453       }
00454     }
00455     int introduced = 0;
00456     for (int i=iv.size(); i--;)
00457       if (iv_introduced[i])
00458         introduced++;
00459     IntVarArgs iv_sol(iv.size()-introduced);
00460     IntVarArgs iv_tmp(introduced);
00461     for (int i=iv.size(), j=0, k=0; i--;)
00462       if (iv_introduced[i])
00463         iv_tmp[j++] = iv[i];
00464       else
00465         iv_sol[k++] = iv[i];
00466 
00467     introduced = 0;
00468     for (int i=bv.size(); i--;)
00469       if (bv_introduced[i])
00470         introduced++;
00471     BoolVarArgs bv_sol(bv.size()-introduced);
00472     BoolVarArgs bv_tmp(introduced);
00473     for (int i=bv.size(), j=0, k=0; i--;)
00474       if (bv_introduced[i])
00475         bv_tmp[j++] = bv[i];
00476       else
00477         bv_sol[k++] = bv[i];
00478 
00479     branch(*this, iv_sol, INT_VAR_SIZE_AFC_MIN, INT_VAL_MIN);
00480     branch(*this, bv_sol, INT_VAR_AFC_MIN, INT_VAL_MIN);
00481 #ifdef GECODE_HAS_SET_VARS
00482     introduced = 0;
00483     for (int i=sv.size(); i--;)
00484       if (sv_introduced[i])
00485         introduced++;
00486     SetVarArgs sv_sol(sv.size()-introduced);
00487     SetVarArgs sv_tmp(introduced);
00488     for (int i=sv.size(), j=0, k=0; i--;)
00489       if (sv_introduced[i])
00490         sv_tmp[j++] = sv[i];
00491       else
00492         sv_sol[k++] = sv[i];
00493     branch(*this, sv_sol, SET_VAR_SIZE_AFC_MIN, SET_VAL_MIN_INC);
00494 #endif
00495     branch(*this, iv_tmp, INT_VAR_SIZE_AFC_MIN, INT_VAL_MIN);
00496     branch(*this, bv_tmp, INT_VAR_AFC_MIN, INT_VAL_MIN);
00497 #ifdef GECODE_HAS_SET_VARS
00498     branch(*this, sv_tmp, SET_VAR_SIZE_AFC_MIN, SET_VAL_MIN_INC);
00499 #endif
00500   }
00501 
00502   AST::Array*
00503   FlatZincSpace::solveAnnotations(void) const {
00504     return _solveAnnotations;
00505   }
00506 
00507   void
00508   FlatZincSpace::solve(AST::Array* ann) {
00509     _method = SAT;
00510     _solveAnnotations = ann;
00511   }
00512 
00513   void
00514   FlatZincSpace::minimize(int var, AST::Array* ann) {
00515     _method = MIN;
00516     _optVar = var;
00517     _solveAnnotations = ann;
00518     // Branch on optimization variable to ensure that it is given a value.
00519     AST::Array* args = new AST::Array(4);
00520     args->a[0] = new AST::Array(new AST::IntVar(_optVar));
00521     args->a[1] = new AST::Atom("input_order");
00522     args->a[2] = new AST::Atom("indomain_min");
00523     args->a[3] = new AST::Atom("complete");
00524     AST::Call* c = new AST::Call("int_search", args);
00525     if (!ann)
00526       ann = new AST::Array(c);
00527     else
00528       ann->a.push_back(c);
00529   }
00530 
00531   void
00532   FlatZincSpace::maximize(int var, AST::Array* ann) {
00533     _method = MAX;
00534     _optVar = var;
00535     _solveAnnotations = ann;
00536     // Branch on optimization variable to ensure that it is given a value.
00537     AST::Array* args = new AST::Array(4);
00538     args->a[0] = new AST::Array(new AST::IntVar(_optVar));
00539     args->a[1] = new AST::Atom("input_order");
00540     args->a[2] = new AST::Atom("indomain_min");
00541     args->a[3] = new AST::Atom("complete");
00542     AST::Call* c = new AST::Call("int_search", args);
00543     if (!ann)
00544       ann = new AST::Array(c);
00545     else
00546       ann->a.push_back(c);
00547   }
00548 
00549   FlatZincSpace::~FlatZincSpace(void) {
00550     delete _solveAnnotations;
00551   }
00552 
00553 #ifdef GECODE_HAS_GIST
00554 
00558   template<class Engine>
00559   class GistEngine {
00560   };
00561 
00563   template<typename S>
00564   class GistEngine<DFS<S> > {
00565   public:
00566     static void explore(S* root, const FlatZincOptions& opt,
00567                         Gist::Inspector* i) {
00568       Gecode::Gist::Options o;
00569       o.c_d = opt.c_d(); o.a_d = opt.a_d();
00570       o.inspect.click(i);
00571       (void) Gecode::Gist::dfs(root, o);
00572     }
00573   };
00574 
00576   template<typename S>
00577   class GistEngine<LDS<S> > {
00578   public:
00579     static void explore(S* root, const FlatZincOptions& opt,
00580                         Gist::Inspector* i) {
00581       Gecode::Gist::Options o;
00582       o.c_d = opt.c_d(); o.a_d = opt.a_d();
00583       o.inspect.click(i);
00584       (void) Gecode::Gist::dfs(root, o);
00585     }
00586   };
00587 
00589   template<typename S>
00590   class GistEngine<BAB<S> > {
00591   public:
00592     static void explore(S* root, const FlatZincOptions& opt,
00593                         Gist::Inspector* i) {
00594       Gecode::Gist::Options o;
00595       o.c_d = opt.c_d(); o.a_d = opt.a_d();
00596       o.inspect.click(i);
00597       (void) Gecode::Gist::bab(root, o);
00598     }
00599   };
00600 
00602   template<typename S>
00603   class GistEngine<Restart<S> > {
00604   public:
00605     static void explore(S* root, const FlatZincOptions& opt,
00606                         Gist::Inspector* i) {
00607       Gecode::Gist::Options o;
00608       o.c_d = opt.c_d(); o.a_d = opt.a_d();
00609       o.inspect.click(i);
00610       (void) Gecode::Gist::bab(root, o);
00611     }
00612   };
00613 
00615   template<class S>
00616   class FZPrintingInspector
00617    : public Gecode::Gist::TextOutput, public Gecode::Gist::Inspector {
00618   private:
00619     const Printer& p;
00620   public:
00622     FZPrintingInspector(const Printer& p0);
00624     virtual void inspect(const Space& node);
00626     virtual void finalize(void);
00627   };
00628 
00629   template<class S>
00630   FZPrintingInspector<S>::FZPrintingInspector(const Printer& p0)
00631   : TextOutput("Gecode/FlatZinc"), p(p0) {}
00632 
00633   template<class S>
00634   void
00635   FZPrintingInspector<S>::inspect(const Space& node) {
00636     init();
00637     dynamic_cast<const S&>(node).print(getStream(), p);
00638     getStream() << std::endl;
00639   }
00640 
00641   template<class S>
00642   void
00643   FZPrintingInspector<S>::finalize(void) {
00644     Gecode::Gist::TextOutput::finalize();
00645   }
00646 
00647 #endif
00648 
00649   template<template<class> class Engine>
00650   void
00651   FlatZincSpace::runEngine(std::ostream& out, const Printer& p,
00652                             const FlatZincOptions& opt, Support::Timer& t_total) {
00653 #ifdef GECODE_HAS_GIST
00654     if (opt.mode() == SM_GIST) {
00655       FZPrintingInspector<FlatZincSpace> pi(p);
00656       (void) GistEngine<Engine<FlatZincSpace> >::explore(this,opt,&pi);
00657       return;
00658     }
00659 #endif
00660     StatusStatistics sstat;
00661     unsigned int n_p = 0;
00662     Support::Timer t_solve;
00663     t_solve.start();
00664     if (status(sstat) != SS_FAILED) {
00665       n_p = propagators();
00666     }
00667     Search::Options o;
00668     o.stop = Driver::Cutoff::create(opt.node(), opt.fail(), opt.time(), 
00669                                     true);
00670     o.c_d = opt.c_d();
00671     o.a_d = opt.a_d();
00672     o.threads = opt.threads();
00673     Driver::Cutoff::installCtrlHandler(true);
00674     Engine<FlatZincSpace> se(this,o);
00675     int noOfSolutions = _method == SAT ? opt.solutions() : 0;
00676     int findSol = noOfSolutions;
00677     FlatZincSpace* sol = NULL;
00678     while (FlatZincSpace* next_sol = se.next()) {
00679       delete sol;
00680       sol = next_sol;
00681       if (opt.print()==0) {
00682         sol->print(out, p);
00683         out << "----------" << std::endl;
00684       }
00685       if (--findSol==0)
00686         goto stopped;
00687     }
00688     if (sol && opt.print()!=0) {
00689       sol->print(out, p);
00690       out << "----------" << std::endl;
00691     }
00692     if (!se.stopped()) {
00693       if (sol) {
00694         out << "==========" << endl;
00695       } else {
00696         out << "=====UNSATISFIABLE=====" << endl;
00697       }
00698     } else if (!sol) {
00699         out << "=====UNKNOWN=====" << endl;
00700     }
00701     delete sol;
00702     stopped:
00703     Driver::Cutoff::installCtrlHandler(false);
00704     if (opt.mode() == SM_STAT) {
00705       Gecode::Search::Statistics stat = se.statistics();
00706       out << endl
00707            << "%%  runtime:       ";
00708       Driver::stop(t_total,out);
00709       out << endl
00710            << "%%  solvetime:     ";
00711       Driver::stop(t_solve,out);
00712       out << endl
00713            << "%%  solutions:     " 
00714            << std::abs(noOfSolutions - findSol) << endl
00715            << "%%  variables:     " 
00716            << (intVarCount + boolVarCount + setVarCount) << endl
00717            << "%%  propagators:   " << n_p << endl
00718            << "%%  propagations:  " << sstat.propagate+stat.propagate << endl
00719            << "%%  nodes:         " << stat.node << endl
00720            << "%%  failures:      " << stat.fail << endl
00721            << "%%  peak depth:    " << stat.depth << endl
00722            << "%%  peak memory:   "
00723            << static_cast<int>((stat.memory+1023) / 1024) << " KB"
00724            << endl;
00725     }
00726   }
00727 
00728 #ifdef GECODE_HAS_QT
00729   void
00730   FlatZincSpace::branchWithPlugin(AST::Node* ann) {
00731     if (AST::Call* c = dynamic_cast<AST::Call*>(ann)) {
00732       QString pluginName(c->id.c_str());
00733       if (QLibrary::isLibrary(pluginName+".dll")) {
00734         pluginName += ".dll";
00735       } else if (QLibrary::isLibrary(pluginName+".dylib")) {
00736         pluginName = "lib" + pluginName + ".dylib";
00737       } else if (QLibrary::isLibrary(pluginName+".so")) {
00738         // Must check .so after .dylib so that Mac OS uses .dylib
00739         pluginName = "lib" + pluginName + ".so";
00740       }
00741       QPluginLoader pl(pluginName);
00742       QObject* plugin_o = pl.instance();
00743       if (!plugin_o) {
00744         throw FlatZinc::Error("FlatZinc",
00745           "Error loading plugin "+pluginName.toStdString()+
00746           ": "+pl.errorString().toStdString());
00747       }
00748       BranchPlugin* pb = qobject_cast<BranchPlugin*>(plugin_o);
00749       if (!pb) {
00750         throw FlatZinc::Error("FlatZinc",
00751         "Error loading plugin "+pluginName.toStdString()+
00752         ": does not contain valid PluginBrancher");
00753       }
00754       pb->branch(*this, c);
00755     }
00756   }
00757 #else
00758   void
00759   FlatZincSpace::branchWithPlugin(AST::Node* ann) {
00760     throw FlatZinc::Error("FlatZinc",
00761       "Branching with plugins not supported (requires Qt support)");
00762   }
00763 #endif
00764 
00765   void
00766   FlatZincSpace::run(std::ostream& out, const Printer& p,
00767                       const FlatZincOptions& opt, Support::Timer& t_total) {
00768     switch (_method) {
00769     case MIN:
00770     case MAX:
00771       if (opt.search() == FlatZincOptions::FZ_SEARCH_BAB)
00772         runEngine<BAB>(out,p,opt,t_total);
00773       else
00774         runEngine<Restart>(out,p,opt,t_total);
00775       break;
00776     case SAT:
00777       runEngine<DFS>(out,p,opt,t_total);
00778       break;
00779     }
00780   }
00781 
00782   void
00783   FlatZincSpace::constrain(const Space& s) {
00784     if (_method == MIN)
00785       rel(*this, iv[_optVar], IRT_LE, 
00786                  static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
00787     else if (_method == MAX)
00788       rel(*this, iv[_optVar], IRT_GR,
00789                  static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
00790   }
00791 
00792   Space*
00793   FlatZincSpace::copy(bool share) {
00794     return new FlatZincSpace(share, *this);
00795   }
00796 
00797   FlatZincSpace::Meth
00798   FlatZincSpace::method(void) const {
00799     return _method;
00800   }
00801 
00802   int
00803   FlatZincSpace::optVar(void) const {
00804     return _optVar;
00805   }
00806 
00807   void
00808   FlatZincSpace::print(std::ostream& out, const Printer& p) const {
00809     p.print(out, iv, bv
00810 #ifdef GECODE_HAS_SET_VARS
00811     , sv
00812 #endif
00813     );
00814   }
00815 
00816   void
00817   FlatZincSpace::shrinkArrays(Printer& p) {
00818     p.shrinkArrays(*this, _optVar, iv, bv
00819 #ifdef GECODE_HAS_SET_VARS
00820     , sv
00821 #endif
00822     );
00823   }
00824 
00825   void
00826   Printer::init(AST::Array* output) {
00827     _output = output;
00828   }
00829 
00830   void
00831   Printer::printElem(std::ostream& out,
00832                        AST::Node* ai,
00833                        const Gecode::IntVarArray& iv,
00834                        const Gecode::BoolVarArray& bv
00835 #ifdef GECODE_HAS_SET_VARS
00836                        , const Gecode::SetVarArray& sv
00837 #endif
00838                        ) const {
00839     int k;
00840     if (ai->isInt(k)) {
00841       out << k;
00842     } else if (ai->isIntVar()) {
00843       out << iv[ai->getIntVar()];
00844     } else if (ai->isBoolVar()) {
00845       if (bv[ai->getBoolVar()].min() == 1) {
00846         out << "true";
00847       } else if (bv[ai->getBoolVar()].max() == 0) {
00848         out << "false";
00849       } else {
00850         out << "false..true";
00851       }
00852 #ifdef GECODE_HAS_SET_VARS
00853     } else if (ai->isSetVar()) {
00854       if (!sv[ai->getSetVar()].assigned()) {
00855         out << sv[ai->getSetVar()];
00856         return;
00857       }
00858       SetVarGlbRanges svr(sv[ai->getSetVar()]);
00859       if (!svr()) {
00860         out << "{}";
00861         return;
00862       }
00863       int min = svr.min();
00864       int max = svr.max();
00865       ++svr;
00866       if (svr()) {
00867         SetVarGlbValues svv(sv[ai->getSetVar()]);
00868         int i = svv.val();
00869         out << "{" << i;
00870         ++svv;
00871         for (; svv(); ++svv)
00872           out << ", " << svv.val();
00873         out << "}";
00874       } else {
00875         out << min << ".." << max;
00876       }
00877 #endif
00878     } else if (ai->isBool()) {
00879       out << (ai->getBool() ? "true" : "false");
00880     } else if (ai->isSet()) {
00881       AST::SetLit* s = ai->getSet();
00882       if (s->interval) {
00883         out << s->min << ".." << s->max;
00884       } else {
00885         out << "{";
00886         for (unsigned int i=0; i<s->s.size(); i++) {
00887           out << s->s[i] << (i < s->s.size()-1 ? ", " : "}");
00888         }
00889       }
00890     } else if (ai->isString()) {
00891       std::string s = ai->getString();
00892       for (unsigned int i=0; i<s.size(); i++) {
00893         if (s[i] == '\\' && i<s.size()-1) {
00894           switch (s[i+1]) {
00895           case 'n': out << "\n"; break;
00896           case '\\': out << "\\"; break;
00897           case 't': out << "\t"; break;
00898           default: out << "\\" << s[i+1];
00899           }
00900           i++;
00901         } else {
00902           out << s[i];
00903         }
00904       }
00905     }
00906   }
00907 
00908   void
00909   Printer::print(std::ostream& out,
00910                    const Gecode::IntVarArray& iv,
00911                    const Gecode::BoolVarArray& bv
00912 #ifdef GECODE_HAS_SET_VARS
00913                    ,
00914                    const Gecode::SetVarArray& sv
00915 #endif
00916                    ) const {
00917     if (_output == NULL)
00918       return;
00919     for (unsigned int i=0; i< _output->a.size(); i++) {
00920       AST::Node* ai = _output->a[i];
00921       if (ai->isArray()) {
00922         AST::Array* aia = ai->getArray();
00923         int size = aia->a.size();
00924         out << "[";
00925         for (int j=0; j<size; j++) {
00926           printElem(out,aia->a[j],iv,bv
00927 #ifdef GECODE_HAS_SET_VARS
00928           ,sv
00929 #endif
00930           );
00931           if (j<size-1)
00932             out << ", ";
00933         }
00934         out << "]";
00935       } else {
00936         printElem(out,ai,iv,bv
00937 #ifdef GECODE_HAS_SET_VARS
00938         ,sv
00939 #endif
00940         );
00941       }
00942     }
00943   }
00944 
00945   void
00946   Printer::shrinkElement(AST::Node* node,
00947                          std::map<int,int>& iv, std::map<int,int>& bv, 
00948                          std::map<int,int>& sv) {
00949     if (node->isIntVar()) {
00950       AST::IntVar* x = static_cast<AST::IntVar*>(node);
00951       if (iv.find(x->i) == iv.end()) {
00952         int newi = iv.size();
00953         iv[x->i] = newi;
00954       }
00955       x->i = iv[x->i];
00956     } else if (node->isBoolVar()) {
00957       AST::BoolVar* x = static_cast<AST::BoolVar*>(node);
00958       if (bv.find(x->i) == bv.end()) {
00959         int newi = bv.size();
00960         bv[x->i] = newi;
00961       }
00962       x->i = bv[x->i];
00963     } else if (node->isSetVar()) {
00964       AST::SetVar* x = static_cast<AST::SetVar*>(node);
00965       if (sv.find(x->i) == sv.end()) {
00966         int newi = sv.size();
00967         sv[x->i] = newi;
00968       }
00969       x->i = sv[x->i];      
00970     }
00971   }
00972 
00973   void
00974   Printer::shrinkArrays(Space& home,
00975                         int& optVar,
00976                         Gecode::IntVarArray& iv,
00977                         Gecode::BoolVarArray& bv
00978 #ifdef GECODE_HAS_SET_VARS
00979                         ,
00980                         Gecode::SetVarArray& sv
00981 #endif
00982                        ) {
00983     if (_output == NULL) {
00984       if (optVar == -1) {
00985         iv = IntVarArray(home, 0);
00986       } else {
00987         IntVar ov = iv[optVar];
00988         iv = IntVarArray(home, 1);
00989         iv[0] = ov;
00990         optVar = 0;
00991       }
00992       bv = BoolVarArray(home, 0);
00993 #ifdef GECODE_HAS_SET_VARS
00994       sv = SetVarArray(home, 0);
00995 #endif
00996       return;
00997     }
00998     std::map<int,int> iv_new;
00999     std::map<int,int> bv_new;
01000     std::map<int,int> sv_new;
01001 
01002     if (optVar != -1) {
01003       iv_new[optVar] = 0;
01004       optVar = 0;
01005     }
01006 
01007     for (unsigned int i=0; i< _output->a.size(); i++) {
01008       AST::Node* ai = _output->a[i];
01009       if (ai->isArray()) {
01010         AST::Array* aia = ai->getArray();
01011         for (unsigned int j=0; j<aia->a.size(); j++) {
01012           shrinkElement(aia->a[j],iv_new,bv_new,sv_new);
01013         }
01014       } else {
01015         shrinkElement(ai,iv_new,bv_new,sv_new);
01016       }
01017     }
01018 
01019     IntVarArgs iva(iv_new.size());
01020     for (map<int,int>::iterator i=iv_new.begin(); i != iv_new.end(); ++i) {
01021       iva[(*i).second] = iv[(*i).first];
01022     }
01023     iv = IntVarArray(home, iva);
01024 
01025     BoolVarArgs bva(bv_new.size());
01026     for (map<int,int>::iterator i=bv_new.begin(); i != bv_new.end(); ++i) {
01027       bva[(*i).second] = bv[(*i).first];
01028     }
01029     bv = BoolVarArray(home, bva);
01030 
01031 #ifdef GECODE_HAS_SET_VARS
01032     SetVarArgs sva(sv_new.size());
01033     for (map<int,int>::iterator i=sv_new.begin(); i != sv_new.end(); ++i) {
01034       sva[(*i).second] = sv[(*i).first];
01035     }
01036     sv = SetVarArray(home, sva);
01037 #endif
01038   }
01039 
01040   Printer::~Printer(void) {
01041     delete _output;
01042   }
01043 
01044 }}
01045 
01046 // STATISTICS: flatzinc-any