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