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