00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034
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
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
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
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