Generated on Wed Jul 27 2011 15:08:34 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: 2010-10-09 13:58:12 +0200 (Sat, 09 Oct 2010) $ by $Author: schulte $
00011  *     $Revision: 11498 $
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<BAB<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::bab(root, o);
00585     }
00586   };
00587 
00589   template<typename S>
00590   class GistEngine<Restart<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<class S>
00603   class FZPrintingInspector
00604    : public Gecode::Gist::TextOutput, public Gecode::Gist::Inspector {
00605   private:
00606     const Printer& p;
00607   public:
00609     FZPrintingInspector(const Printer& p0);
00611     virtual void inspect(const Space& node);
00613     virtual void finalize(void);
00614   };
00615 
00616   template<class S>
00617   FZPrintingInspector<S>::FZPrintingInspector(const Printer& p0)
00618   : TextOutput("Gecode/FlatZinc"), p(p0) {}
00619 
00620   template<class S>
00621   void
00622   FZPrintingInspector<S>::inspect(const Space& node) {
00623     init();
00624     dynamic_cast<const S&>(node).print(getStream(), p);
00625     getStream() << std::endl;
00626   }
00627 
00628   template<class S>
00629   void
00630   FZPrintingInspector<S>::finalize(void) {
00631     Gecode::Gist::TextOutput::finalize();
00632   }
00633 
00634 #endif
00635 
00636   template<template<class> class Engine>
00637   void
00638   FlatZincSpace::runEngine(std::ostream& out, const Printer& p,
00639                             const FlatZincOptions& opt, Support::Timer& t_total) {
00640 #ifdef GECODE_HAS_GIST
00641     if (opt.mode() == SM_GIST) {
00642       FZPrintingInspector<FlatZincSpace> pi(p);
00643       (void) GistEngine<Engine<FlatZincSpace> >::explore(this,opt,&pi);
00644       return;
00645     }
00646 #endif
00647     StatusStatistics sstat;
00648     unsigned int n_p = 0;
00649     Support::Timer t_solve;
00650     t_solve.start();
00651     if (status(sstat) != SS_FAILED) {
00652       n_p = propagators();
00653     }
00654     Search::Options o;
00655     o.stop = Driver::Cutoff::create(opt.node(), opt.fail(), opt.time(), 
00656                                     true);
00657     o.c_d = opt.c_d();
00658     o.a_d = opt.a_d();
00659     o.threads = opt.threads();
00660     Driver::Cutoff::installCtrlHandler(true);
00661     Engine<FlatZincSpace> se(this,o);
00662     int noOfSolutions = _method == SAT ? opt.solutions() : 0;
00663     int findSol = noOfSolutions;
00664     FlatZincSpace* sol = NULL;
00665     while (FlatZincSpace* next_sol = se.next()) {
00666       delete sol;
00667       sol = next_sol;
00668       if (opt.print()==0) {
00669         sol->print(out, p);
00670         out << "----------" << std::endl;
00671       }
00672       if (--findSol==0)
00673         goto stopped;
00674     }
00675     if (sol && opt.print()!=0) {
00676       sol->print(out, p);
00677       out << "----------" << std::endl;
00678     }
00679     if (!se.stopped()) {
00680       if (sol) {
00681         out << "==========" << endl;
00682       } else {
00683         out << "=====UNSATISFIABLE=====" << endl;
00684       }
00685     } else if (!sol) {
00686         out << "=====UNKNOWN=====" << endl;
00687     }
00688     delete sol;
00689     stopped:
00690     Driver::Cutoff::installCtrlHandler(false);
00691     if (opt.mode() == SM_STAT) {
00692       Gecode::Search::Statistics stat = se.statistics();
00693       out << endl
00694            << "%%  runtime:       ";
00695       Driver::stop(t_total,out);
00696       out << endl
00697            << "%%  solvetime:     ";
00698       Driver::stop(t_solve,out);
00699       out << endl
00700            << "%%  solutions:     " 
00701            << std::abs(noOfSolutions - findSol) << endl
00702            << "%%  variables:     " 
00703            << (intVarCount + boolVarCount + setVarCount) << endl
00704            << "%%  propagators:   " << n_p << endl
00705            << "%%  propagations:  " << sstat.propagate+stat.propagate << endl
00706            << "%%  nodes:         " << stat.node << endl
00707            << "%%  failures:      " << stat.fail << endl
00708            << "%%  peak depth:    " << stat.depth << endl
00709            << "%%  peak memory:   "
00710            << static_cast<int>((stat.memory+1023) / 1024) << " KB"
00711            << endl;
00712     }
00713   }
00714 
00715 #ifdef GECODE_HAS_QT
00716   void
00717   FlatZincSpace::branchWithPlugin(AST::Node* ann) {
00718     if (AST::Call* c = dynamic_cast<AST::Call*>(ann)) {
00719       QString pluginName(c->id.c_str());
00720       if (QLibrary::isLibrary(pluginName+".dll")) {
00721         pluginName += ".dll";
00722       } else if (QLibrary::isLibrary(pluginName+".dylib")) {
00723         pluginName = "lib" + pluginName + ".dylib";
00724       } else if (QLibrary::isLibrary(pluginName+".so")) {
00725         // Must check .so after .dylib so that Mac OS uses .dylib
00726         pluginName = "lib" + pluginName + ".so";
00727       }
00728       QPluginLoader pl(pluginName);
00729       QObject* plugin_o = pl.instance();
00730       if (!plugin_o) {
00731         throw FlatZinc::Error("FlatZinc",
00732           "Error loading plugin "+pluginName.toStdString()+
00733           ": "+pl.errorString().toStdString());
00734       }
00735       BranchPlugin* pb = qobject_cast<BranchPlugin*>(plugin_o);
00736       if (!pb) {
00737         throw FlatZinc::Error("FlatZinc",
00738         "Error loading plugin "+pluginName.toStdString()+
00739         ": does not contain valid PluginBrancher");
00740       }
00741       pb->branch(*this, c);
00742     }
00743   }
00744 #else
00745   void
00746   FlatZincSpace::branchWithPlugin(AST::Node* ann) {
00747     throw FlatZinc::Error("FlatZinc",
00748       "Branching with plugins not supported (requires Qt support)");
00749   }
00750 #endif
00751 
00752   void
00753   FlatZincSpace::run(std::ostream& out, const Printer& p,
00754                       const FlatZincOptions& opt, Support::Timer& t_total) {
00755     switch (_method) {
00756     case MIN:
00757     case MAX:
00758       if (opt.search() == FlatZincOptions::FZ_SEARCH_BAB)
00759         runEngine<BAB>(out,p,opt,t_total);
00760       else
00761         runEngine<Restart>(out,p,opt,t_total);
00762       break;
00763     case SAT:
00764       runEngine<DFS>(out,p,opt,t_total);
00765       break;
00766     }
00767   }
00768 
00769   void
00770   FlatZincSpace::constrain(const Space& s) {
00771     if (_method == MIN)
00772       rel(*this, iv[_optVar], IRT_LE, 
00773                  static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
00774     else if (_method == MAX)
00775       rel(*this, iv[_optVar], IRT_GR,
00776                  static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
00777   }
00778 
00779   Space*
00780   FlatZincSpace::copy(bool share) {
00781     return new FlatZincSpace(share, *this);
00782   }
00783 
00784   FlatZincSpace::Meth
00785   FlatZincSpace::method(void) const {
00786     return _method;
00787   }
00788 
00789   int
00790   FlatZincSpace::optVar(void) const {
00791     return _optVar;
00792   }
00793 
00794   void
00795   FlatZincSpace::print(std::ostream& out, const Printer& p) const {
00796     p.print(out, iv, bv
00797 #ifdef GECODE_HAS_SET_VARS
00798     , sv
00799 #endif
00800     );
00801   }
00802 
00803   void
00804   FlatZincSpace::shrinkArrays(Printer& p) {
00805     p.shrinkArrays(*this, _optVar, iv, bv
00806 #ifdef GECODE_HAS_SET_VARS
00807     , sv
00808 #endif
00809     );
00810   }
00811 
00812   void
00813   Printer::init(AST::Array* output) {
00814     _output = output;
00815   }
00816 
00817   void
00818   Printer::printElem(std::ostream& out,
00819                        AST::Node* ai,
00820                        const Gecode::IntVarArray& iv,
00821                        const Gecode::BoolVarArray& bv
00822 #ifdef GECODE_HAS_SET_VARS
00823                        , const Gecode::SetVarArray& sv
00824 #endif
00825                        ) const {
00826     int k;
00827     if (ai->isInt(k)) {
00828       out << k;
00829     } else if (ai->isIntVar()) {
00830       out << iv[ai->getIntVar()];
00831     } else if (ai->isBoolVar()) {
00832       if (bv[ai->getBoolVar()].min() == 1) {
00833         out << "true";
00834       } else if (bv[ai->getBoolVar()].max() == 0) {
00835         out << "false";
00836       } else {
00837         out << "false..true";
00838       }
00839 #ifdef GECODE_HAS_SET_VARS
00840     } else if (ai->isSetVar()) {
00841       if (!sv[ai->getSetVar()].assigned()) {
00842         out << sv[ai->getSetVar()];
00843         return;
00844       }
00845       SetVarGlbRanges svr(sv[ai->getSetVar()]);
00846       if (!svr()) {
00847         out << "{}";
00848         return;
00849       }
00850       int min = svr.min();
00851       int max = svr.max();
00852       ++svr;
00853       if (svr()) {
00854         SetVarGlbValues svv(sv[ai->getSetVar()]);
00855         int i = svv.val();
00856         out << "{" << i;
00857         ++svv;
00858         for (; svv(); ++svv)
00859           out << ", " << svv.val();
00860         out << "}";
00861       } else {
00862         out << min << ".." << max;
00863       }
00864 #endif
00865     } else if (ai->isBool()) {
00866       out << (ai->getBool() ? "true" : "false");
00867     } else if (ai->isSet()) {
00868       AST::SetLit* s = ai->getSet();
00869       if (s->interval) {
00870         out << s->min << ".." << s->max;
00871       } else {
00872         out << "{";
00873         for (unsigned int i=0; i<s->s.size(); i++) {
00874           out << s->s[i] << (i < s->s.size()-1 ? ", " : "}");
00875         }
00876       }
00877     } else if (ai->isString()) {
00878       std::string s = ai->getString();
00879       for (unsigned int i=0; i<s.size(); i++) {
00880         if (s[i] == '\\' && i<s.size()-1) {
00881           switch (s[i+1]) {
00882           case 'n': out << "\n"; break;
00883           case '\\': out << "\\"; break;
00884           case 't': out << "\t"; break;
00885           default: out << "\\" << s[i+1];
00886           }
00887           i++;
00888         } else {
00889           out << s[i];
00890         }
00891       }
00892     }
00893   }
00894 
00895   void
00896   Printer::print(std::ostream& out,
00897                    const Gecode::IntVarArray& iv,
00898                    const Gecode::BoolVarArray& bv
00899 #ifdef GECODE_HAS_SET_VARS
00900                    ,
00901                    const Gecode::SetVarArray& sv
00902 #endif
00903                    ) const {
00904     if (_output == NULL)
00905       return;
00906     for (unsigned int i=0; i< _output->a.size(); i++) {
00907       AST::Node* ai = _output->a[i];
00908       if (ai->isArray()) {
00909         AST::Array* aia = ai->getArray();
00910         int size = aia->a.size();
00911         out << "[";
00912         for (int j=0; j<size; j++) {
00913           printElem(out,aia->a[j],iv,bv
00914 #ifdef GECODE_HAS_SET_VARS
00915           ,sv
00916 #endif
00917           );
00918           if (j<size-1)
00919             out << ", ";
00920         }
00921         out << "]";
00922       } else {
00923         printElem(out,ai,iv,bv
00924 #ifdef GECODE_HAS_SET_VARS
00925         ,sv
00926 #endif
00927         );
00928       }
00929     }
00930   }
00931 
00932   void
00933   Printer::shrinkElement(AST::Node* node,
00934                          std::map<int,int>& iv, std::map<int,int>& bv, 
00935                          std::map<int,int>& sv) {
00936     if (node->isIntVar()) {
00937       AST::IntVar* x = static_cast<AST::IntVar*>(node);
00938       if (iv.find(x->i) == iv.end()) {
00939         int newi = iv.size();
00940         iv[x->i] = newi;
00941       }
00942       x->i = iv[x->i];
00943     } else if (node->isBoolVar()) {
00944       AST::BoolVar* x = static_cast<AST::BoolVar*>(node);
00945       if (bv.find(x->i) == bv.end()) {
00946         int newi = bv.size();
00947         bv[x->i] = newi;
00948       }
00949       x->i = bv[x->i];
00950     } else if (node->isSetVar()) {
00951       AST::SetVar* x = static_cast<AST::SetVar*>(node);
00952       if (sv.find(x->i) == sv.end()) {
00953         int newi = sv.size();
00954         sv[x->i] = newi;
00955       }
00956       x->i = sv[x->i];      
00957     }
00958   }
00959 
00960   void
00961   Printer::shrinkArrays(Space& home,
00962                         int& optVar,
00963                         Gecode::IntVarArray& iv,
00964                         Gecode::BoolVarArray& bv
00965 #ifdef GECODE_HAS_SET_VARS
00966                         ,
00967                         Gecode::SetVarArray& sv
00968 #endif
00969                        ) {
00970     if (_output == NULL) {
00971       if (optVar == -1) {
00972         iv = IntVarArray(home, 0);
00973       } else {
00974         IntVar ov = iv[optVar];
00975         iv = IntVarArray(home, 1);
00976         iv[0] = ov;
00977         optVar = 0;
00978       }
00979       bv = BoolVarArray(home, 0);
00980 #ifdef GECODE_HAS_SET_VARS
00981       sv = SetVarArray(home, 0);
00982 #endif
00983       return;
00984     }
00985     std::map<int,int> iv_new;
00986     std::map<int,int> bv_new;
00987     std::map<int,int> sv_new;
00988 
00989     if (optVar != -1) {
00990       iv_new[optVar] = 0;
00991       optVar = 0;
00992     }
00993 
00994     for (unsigned int i=0; i< _output->a.size(); i++) {
00995       AST::Node* ai = _output->a[i];
00996       if (ai->isArray()) {
00997         AST::Array* aia = ai->getArray();
00998         for (unsigned int j=0; j<aia->a.size(); j++) {
00999           shrinkElement(aia->a[j],iv_new,bv_new,sv_new);
01000         }
01001       } else {
01002         shrinkElement(ai,iv_new,bv_new,sv_new);
01003       }
01004     }
01005 
01006     IntVarArgs iva(iv_new.size());
01007     for (map<int,int>::iterator i=iv_new.begin(); i != iv_new.end(); ++i) {
01008       iva[(*i).second] = iv[(*i).first];
01009     }
01010     iv = IntVarArray(home, iva);
01011 
01012     BoolVarArgs bva(bv_new.size());
01013     for (map<int,int>::iterator i=bv_new.begin(); i != bv_new.end(); ++i) {
01014       bva[(*i).second] = bv[(*i).first];
01015     }
01016     bv = BoolVarArray(home, bva);
01017 
01018 #ifdef GECODE_HAS_SET_VARS
01019     SetVarArgs sva(sv_new.size());
01020     for (map<int,int>::iterator i=sv_new.begin(); i != sv_new.end(); ++i) {
01021       sva[(*i).second] = sv[(*i).first];
01022     }
01023     sv = SetVarArray(home, sva);
01024 #endif
01025   }
01026 
01027   Printer::~Printer(void) {
01028     delete _output;
01029   }
01030 
01031 }}
01032 
01033 // STATISTICS: flatzinc-any