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 if (s->id == "indomain_middle") {
00147 std::cerr << "Warning, replacing unsupported annotation "
00148 << "indomain_middle with indomain_median" << std::endl;
00149 return INT_VAL_MED;
00150 }
00151 if (s->id == "indomain_interval") {
00152 std::cerr << "Warning, replacing unsupported annotation "
00153 << "indomain_interval with indomain_split" << std::endl;
00154 return INT_VAL_SPLIT_MIN;
00155 }
00156 }
00157 std::cerr << "Warning, ignored search annotation: ";
00158 ann->print(std::cerr);
00159 std::cerr << std::endl;
00160 return INT_VAL_MIN;
00161 }
00162
00163 IntAssign ann2asnivalsel(AST::Node* ann) {
00164 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00165 if (s->id == "indomain_min")
00166 return INT_ASSIGN_MIN;
00167 if (s->id == "indomain_max")
00168 return INT_ASSIGN_MAX;
00169 if (s->id == "indomain_median")
00170 return INT_ASSIGN_MED;
00171 if (s->id == "indomain_random")
00172 return INT_ASSIGN_RND;
00173 }
00174 std::cerr << "Warning, ignored search annotation: ";
00175 ann->print(std::cerr);
00176 std::cerr << std::endl;
00177 return INT_ASSIGN_MIN;
00178 }
00179
00180 #ifdef GECODE_HAS_SET_VARS
00181 SetVarBranch ann2svarsel(AST::Node* ann) {
00182 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00183 if (s->id == "input_order")
00184 return SET_VAR_NONE;
00185 if (s->id == "first_fail")
00186 return SET_VAR_SIZE_MIN;
00187 if (s->id == "anti_first_fail")
00188 return SET_VAR_SIZE_MAX;
00189 if (s->id == "smallest")
00190 return SET_VAR_MIN_MIN;
00191 if (s->id == "largest")
00192 return SET_VAR_MIN_MAX;
00193 }
00194 std::cerr << "Warning, ignored search annotation: ";
00195 ann->print(std::cerr);
00196 std::cerr << std::endl;
00197 return SET_VAR_NONE;
00198 }
00199
00200 SetValBranch ann2svalsel(AST::Node* ann) {
00201 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00202 if (s->id == "indomain_min")
00203 return SET_VAL_MIN_INC;
00204 if (s->id == "indomain_max")
00205 return SET_VAL_MAX_INC;
00206 if (s->id == "outdomain_min")
00207 return SET_VAL_MIN_EXC;
00208 if (s->id == "outdomain_max")
00209 return SET_VAL_MAX_EXC;
00210 }
00211 std::cerr << "Warning, ignored search annotation: ";
00212 ann->print(std::cerr);
00213 std::cerr << std::endl;
00214 return SET_VAL_MIN_INC;
00215 }
00216 #endif
00217
00218 FlatZincSpace::FlatZincSpace(bool share, FlatZincSpace& f)
00219 : Space(share, f), _solveAnnotations(NULL), iv_boolalias(NULL) {
00220 _optVar = f._optVar;
00221 _method = f._method;
00222 iv.update(*this, share, f.iv);
00223 intVarCount = f.intVarCount;
00224 bv.update(*this, share, f.bv);
00225 boolVarCount = f.boolVarCount;
00226 #ifdef GECODE_HAS_SET_VARS
00227 sv.update(*this, share, f.sv);
00228 setVarCount = f.setVarCount;
00229 #endif
00230 }
00231
00232 FlatZincSpace::FlatZincSpace(void)
00233 : intVarCount(-1), boolVarCount(-1), setVarCount(-1), _optVar(-1),
00234 _solveAnnotations(NULL) {}
00235
00236 void
00237 FlatZincSpace::init(int intVars, int boolVars,
00238 #ifdef GECODE_HAS_SET_VARS
00239 int setVars) {
00240 #else
00241 int) {
00242 #endif
00243 intVarCount = 0;
00244 iv = IntVarArray(*this, intVars);
00245 iv_introduced = std::vector<bool>(intVars);
00246 iv_boolalias = alloc<int>(intVars+(intVars==0?1:0));
00247 boolVarCount = 0;
00248 bv = BoolVarArray(*this, boolVars);
00249 bv_introduced = std::vector<bool>(boolVars);
00250 #ifdef GECODE_HAS_SET_VARS
00251 setVarCount = 0;
00252 sv = SetVarArray(*this, setVars);
00253 sv_introduced = std::vector<bool>(setVars);
00254 #endif
00255 }
00256
00257 void
00258 FlatZincSpace::newIntVar(IntVarSpec* vs) {
00259 if (vs->alias) {
00260 iv[intVarCount++] = iv[vs->i];
00261 } else {
00262 iv[intVarCount++] = IntVar(*this, vs2is(vs));
00263 }
00264 iv_introduced[intVarCount-1] = vs->introduced;
00265 iv_boolalias[intVarCount-1] = -1;
00266 }
00267
00268 void
00269 FlatZincSpace::aliasBool2Int(int iv, int bv) {
00270 iv_boolalias[iv] = bv;
00271 }
00272 int
00273 FlatZincSpace::aliasBool2Int(int iv) {
00274 return iv_boolalias[iv];
00275 }
00276
00277 void
00278 FlatZincSpace::newBoolVar(BoolVarSpec* vs) {
00279 if (vs->alias) {
00280 bv[boolVarCount++] = bv[vs->i];
00281 } else {
00282 bv[boolVarCount++] = BoolVar(*this, vs2bsl(vs), vs2bsh(vs));
00283 }
00284 bv_introduced[boolVarCount-1] = vs->introduced;
00285 }
00286
00287 #ifdef GECODE_HAS_SET_VARS
00288 void
00289 FlatZincSpace::newSetVar(SetVarSpec* vs) {
00290 if (vs->alias) {
00291 sv[setVarCount++] = sv[vs->i];
00292 } else if (vs->assigned) {
00293 assert(vs->upperBound());
00294 AST::SetLit* vsv = vs->upperBound.some();
00295 if (vsv->interval) {
00296 IntSet d(vsv->min, vsv->max);
00297 sv[setVarCount++] = SetVar(*this, d, d);
00298 } else {
00299 int* is = heap.alloc<int>(static_cast<unsigned long int>(vsv->s.size()));
00300 for (int i=vsv->s.size(); i--; )
00301 is[i] = vsv->s[i];
00302 IntSet d(is, vsv->s.size());
00303 heap.free(is,static_cast<unsigned long int>(vsv->s.size()));
00304 sv[setVarCount++] = SetVar(*this, d, d);
00305 }
00306 } else if (vs->upperBound()) {
00307 AST::SetLit* vsv = vs->upperBound.some();
00308 if (vsv->interval) {
00309 IntSet d(vsv->min, vsv->max);
00310 sv[setVarCount++] = SetVar(*this, IntSet::empty, d);
00311 } else {
00312 int* is = heap.alloc<int>(static_cast<unsigned long int>(vsv->s.size()));
00313 for (int i=vsv->s.size(); i--; )
00314 is[i] = vsv->s[i];
00315 IntSet d(is, vsv->s.size());
00316 heap.free(is,static_cast<unsigned long int>(vsv->s.size()));
00317 sv[setVarCount++] = SetVar(*this, IntSet::empty, d);
00318 }
00319 } else {
00320 sv[setVarCount++] = SetVar(*this, IntSet::empty,
00321 IntSet(Set::Limits::min,
00322 Set::Limits::max));
00323 }
00324 sv_introduced[setVarCount-1] = vs->introduced;
00325 }
00326 #else
00327 void
00328 FlatZincSpace::newSetVar(SetVarSpec*) {
00329 throw FlatZinc::Error("Gecode", "set variables not supported");
00330 }
00331 #endif
00332
00333 void
00334 FlatZincSpace::postConstraint(const ConExpr& ce, AST::Node* ann) {
00335 try {
00336 registry().post(*this, ce, ann);
00337 } catch (Gecode::Exception& e) {
00338 throw FlatZinc::Error("Gecode", e.what());
00339 } catch (AST::TypeError& e) {
00340 throw FlatZinc::Error("Type error", e.what());
00341 }
00342 }
00343
00344 void flattenAnnotations(AST::Array* ann, std::vector<AST::Node*>& out) {
00345 for (unsigned int i=0; i<ann->a.size(); i++) {
00346 if (ann->a[i]->isCall("seq_search")) {
00347 AST::Call* c = ann->a[i]->getCall();
00348 if (c->args->isArray())
00349 flattenAnnotations(c->args->getArray(), out);
00350 else
00351 out.push_back(c->args);
00352 } else {
00353 out.push_back(ann->a[i]);
00354 }
00355 }
00356 }
00357
00358 void
00359 FlatZincSpace::createBranchers(AST::Node* ann, int seed,
00360 bool ignoreUnknown,
00361 std::ostream& err) {
00362 VarBranchOptions varbo;
00363 varbo.seed = seed;
00364 ValBranchOptions valbo;
00365 valbo.seed = seed;
00366 if (ann) {
00367 std::vector<AST::Node*> flatAnn;
00368 if (ann->isArray()) {
00369 flattenAnnotations(ann->getArray() , flatAnn);
00370 } else {
00371 flatAnn.push_back(ann);
00372 }
00373
00374 for (unsigned int i=0; i<flatAnn.size(); i++) {
00375 if (flatAnn[i]->isCall("gecode_search")) {
00376 AST::Call* c = flatAnn[i]->getCall();
00377 branchWithPlugin(c->args);
00378 } else try {
00379 AST::Call *call = flatAnn[i]->getCall("int_search");
00380 AST::Array *args = call->getArgs(4);
00381 AST::Array *vars = args->a[0]->getArray();
00382 int k=vars->a.size();
00383 for (int i=vars->a.size(); i--;)
00384 if (vars->a[i]->isInt())
00385 k--;
00386 IntVarArgs va(k);
00387 k=0;
00388 for (unsigned int i=0; i<vars->a.size(); i++) {
00389 if (vars->a[i]->isInt())
00390 continue;
00391 va[k++] = iv[vars->a[i]->getIntVar()];
00392 }
00393 branch(*this, va, ann2ivarsel(args->a[1]), ann2ivalsel(args->a[2]),
00394 varbo,valbo);
00395 } catch (AST::TypeError& e) {
00396 try {
00397 AST::Call *call = flatAnn[i]->getCall("int_assign");
00398 AST::Array *args = call->getArgs(2);
00399 AST::Array *vars = args->a[0]->getArray();
00400 int k=vars->a.size();
00401 for (int i=vars->a.size(); i--;)
00402 if (vars->a[i]->isInt())
00403 k--;
00404 IntVarArgs va(k);
00405 k=0;
00406 for (unsigned int i=0; i<vars->a.size(); i++) {
00407 if (vars->a[i]->isInt())
00408 continue;
00409 va[k++] = iv[vars->a[i]->getIntVar()];
00410 }
00411 assign(*this, va, ann2asnivalsel(args->a[1]));
00412 } catch (AST::TypeError& e) {
00413 (void) e;
00414 try {
00415 AST::Call *call = flatAnn[i]->getCall("bool_search");
00416 AST::Array *args = call->getArgs(4);
00417 AST::Array *vars = args->a[0]->getArray();
00418 int k=vars->a.size();
00419 for (int i=vars->a.size(); i--;)
00420 if (vars->a[i]->isBool())
00421 k--;
00422 BoolVarArgs va(k);
00423 k=0;
00424 for (unsigned int i=0; i<vars->a.size(); i++) {
00425 if (vars->a[i]->isBool())
00426 continue;
00427 va[k++] = bv[vars->a[i]->getBoolVar()];
00428 }
00429 branch(*this, va, ann2ivarsel(args->a[1]),
00430 ann2ivalsel(args->a[2]), varbo, valbo);
00431 } catch (AST::TypeError& e) {
00432 (void) e;
00433 #ifdef GECODE_HAS_SET_VARS
00434 try {
00435 AST::Call *call = flatAnn[i]->getCall("set_search");
00436 AST::Array *args = call->getArgs(4);
00437 AST::Array *vars = args->a[0]->getArray();
00438 int k=vars->a.size();
00439 for (int i=vars->a.size(); i--;)
00440 if (vars->a[i]->isSet())
00441 k--;
00442 SetVarArgs va(k);
00443 k=0;
00444 for (unsigned int i=0; i<vars->a.size(); i++) {
00445 if (vars->a[i]->isSet())
00446 continue;
00447 va[k++] = sv[vars->a[i]->getSetVar()];
00448 }
00449 branch(*this, va, ann2svarsel(args->a[1]),
00450 ann2svalsel(args->a[2]), varbo, valbo);
00451 } catch (AST::TypeError& e) {
00452 (void) e;
00453 if (!ignoreUnknown) {
00454 err << "Warning, ignored search annotation: ";
00455 flatAnn[i]->print(err);
00456 err << std::endl;
00457 }
00458 }
00459 #else
00460 if (!ignoreUnknown) {
00461 err << "Warning, ignored search annotation: ";
00462 flatAnn[i]->print(err);
00463 err << std::endl;
00464 }
00465 #endif
00466 }
00467 }
00468 }
00469 }
00470 }
00471 int introduced = 0;
00472 for (int i=iv.size(); i--;)
00473 if (iv_introduced[i])
00474 introduced++;
00475 IntVarArgs iv_sol(iv.size()-introduced);
00476 IntVarArgs iv_tmp(introduced);
00477 for (int i=iv.size(), j=0, k=0; i--;)
00478 if (iv_introduced[i])
00479 iv_tmp[j++] = iv[i];
00480 else
00481 iv_sol[k++] = iv[i];
00482
00483 introduced = 0;
00484 for (int i=bv.size(); i--;)
00485 if (bv_introduced[i])
00486 introduced++;
00487 BoolVarArgs bv_sol(bv.size()-introduced);
00488 BoolVarArgs bv_tmp(introduced);
00489 for (int i=bv.size(), j=0, k=0; i--;)
00490 if (bv_introduced[i])
00491 bv_tmp[j++] = bv[i];
00492 else
00493 bv_sol[k++] = bv[i];
00494
00495 branch(*this, iv_sol, INT_VAR_SIZE_AFC_MIN, INT_VAL_MIN);
00496 branch(*this, bv_sol, INT_VAR_AFC_MAX, INT_VAL_MIN);
00497 #ifdef GECODE_HAS_SET_VARS
00498 introduced = 0;
00499 for (int i=sv.size(); i--;)
00500 if (sv_introduced[i])
00501 introduced++;
00502 SetVarArgs sv_sol(sv.size()-introduced);
00503 SetVarArgs sv_tmp(introduced);
00504 for (int i=sv.size(), j=0, k=0; i--;)
00505 if (sv_introduced[i])
00506 sv_tmp[j++] = sv[i];
00507 else
00508 sv_sol[k++] = sv[i];
00509 branch(*this, sv_sol, SET_VAR_SIZE_AFC_MIN, SET_VAL_MIN_INC);
00510 #endif
00511 branch(*this, iv_tmp, INT_VAR_SIZE_AFC_MIN, INT_VAL_MIN);
00512 branch(*this, bv_tmp, INT_VAR_AFC_MAX, INT_VAL_MIN);
00513 #ifdef GECODE_HAS_SET_VARS
00514 branch(*this, sv_tmp, SET_VAR_SIZE_AFC_MIN, SET_VAL_MIN_INC);
00515 #endif
00516 }
00517
00518 AST::Array*
00519 FlatZincSpace::solveAnnotations(void) const {
00520 return _solveAnnotations;
00521 }
00522
00523 void
00524 FlatZincSpace::solve(AST::Array* ann) {
00525 _method = SAT;
00526 _solveAnnotations = ann;
00527 }
00528
00529 void
00530 FlatZincSpace::minimize(int var, AST::Array* ann) {
00531 _method = MIN;
00532 _optVar = var;
00533 _solveAnnotations = ann;
00534
00535 AST::Array* args = new AST::Array(4);
00536 args->a[0] = new AST::Array(new AST::IntVar(_optVar));
00537 args->a[1] = new AST::Atom("input_order");
00538 args->a[2] = new AST::Atom("indomain_min");
00539 args->a[3] = new AST::Atom("complete");
00540 AST::Call* c = new AST::Call("int_search", args);
00541 if (!ann)
00542 ann = new AST::Array(c);
00543 else
00544 ann->a.push_back(c);
00545 }
00546
00547 void
00548 FlatZincSpace::maximize(int var, AST::Array* ann) {
00549 _method = MAX;
00550 _optVar = var;
00551 _solveAnnotations = ann;
00552
00553 AST::Array* args = new AST::Array(4);
00554 args->a[0] = new AST::Array(new AST::IntVar(_optVar));
00555 args->a[1] = new AST::Atom("input_order");
00556 args->a[2] = new AST::Atom("indomain_min");
00557 args->a[3] = new AST::Atom("complete");
00558 AST::Call* c = new AST::Call("int_search", args);
00559 if (!ann)
00560 ann = new AST::Array(c);
00561 else
00562 ann->a.push_back(c);
00563 }
00564
00565 FlatZincSpace::~FlatZincSpace(void) {
00566 delete _solveAnnotations;
00567 }
00568
00569 #ifdef GECODE_HAS_GIST
00570
00574 template<class Engine>
00575 class GistEngine {
00576 };
00577
00579 template<typename S>
00580 class GistEngine<DFS<S> > {
00581 public:
00582 static void explore(S* root, const FlatZincOptions& opt,
00583 Gist::Inspector* i) {
00584 Gecode::Gist::Options o;
00585 o.c_d = opt.c_d(); o.a_d = opt.a_d();
00586 o.inspect.click(i);
00587 (void) Gecode::Gist::dfs(root, o);
00588 }
00589 };
00590
00592 template<typename S>
00593 class GistEngine<BAB<S> > {
00594 public:
00595 static void explore(S* root, const FlatZincOptions& opt,
00596 Gist::Inspector* i) {
00597 Gecode::Gist::Options o;
00598 o.c_d = opt.c_d(); o.a_d = opt.a_d();
00599 o.inspect.click(i);
00600 (void) Gecode::Gist::bab(root, o);
00601 }
00602 };
00603
00605 template<typename S>
00606 class GistEngine<Restart<S> > {
00607 public:
00608 static void explore(S* root, const FlatZincOptions& opt,
00609 Gist::Inspector* i) {
00610 Gecode::Gist::Options o;
00611 o.c_d = opt.c_d(); o.a_d = opt.a_d();
00612 o.inspect.click(i);
00613 (void) Gecode::Gist::bab(root, o);
00614 }
00615 };
00616
00618 template<class S>
00619 class FZPrintingInspector
00620 : public Gecode::Gist::TextOutput, public Gecode::Gist::Inspector {
00621 private:
00622 const Printer& p;
00623 public:
00625 FZPrintingInspector(const Printer& p0);
00627 virtual void inspect(const Space& node);
00629 virtual void finalize(void);
00630 };
00631
00632 template<class S>
00633 FZPrintingInspector<S>::FZPrintingInspector(const Printer& p0)
00634 : TextOutput("Gecode/FlatZinc"), p(p0) {}
00635
00636 template<class S>
00637 void
00638 FZPrintingInspector<S>::inspect(const Space& node) {
00639 init();
00640 dynamic_cast<const S&>(node).print(getStream(), p);
00641 getStream() << std::endl;
00642 }
00643
00644 template<class S>
00645 void
00646 FZPrintingInspector<S>::finalize(void) {
00647 Gecode::Gist::TextOutput::finalize();
00648 }
00649
00650 #endif
00651
00652 template<template<class> class Engine>
00653 void
00654 FlatZincSpace::runEngine(std::ostream& out, const Printer& p,
00655 const FlatZincOptions& opt, Support::Timer& t_total) {
00656 #ifdef GECODE_HAS_GIST
00657 if (opt.mode() == SM_GIST) {
00658 FZPrintingInspector<FlatZincSpace> pi(p);
00659 (void) GistEngine<Engine<FlatZincSpace> >::explore(this,opt,&pi);
00660 return;
00661 }
00662 #endif
00663 StatusStatistics sstat;
00664 unsigned int n_p = 0;
00665 Support::Timer t_solve;
00666 t_solve.start();
00667 if (status(sstat) != SS_FAILED) {
00668 n_p = propagators();
00669 }
00670 Search::Options o;
00671 o.stop = Driver::Cutoff::create(opt.node(), opt.fail(), opt.time(),
00672 true);
00673 o.c_d = opt.c_d();
00674 o.a_d = opt.a_d();
00675 o.threads = opt.threads();
00676 Driver::Cutoff::installCtrlHandler(true);
00677 Engine<FlatZincSpace> se(this,o);
00678 int noOfSolutions = _method == SAT ? opt.solutions() : 0;
00679 int findSol = noOfSolutions;
00680 FlatZincSpace* sol = NULL;
00681 while (FlatZincSpace* next_sol = se.next()) {
00682 delete sol;
00683 sol = next_sol;
00684 if (opt.print()==0) {
00685 sol->print(out, p);
00686 out << "----------" << std::endl;
00687 }
00688 if (--findSol==0)
00689 goto stopped;
00690 }
00691 if (sol && opt.print()!=0) {
00692 sol->print(out, p);
00693 out << "----------" << std::endl;
00694 }
00695 if (!se.stopped()) {
00696 if (sol) {
00697 out << "==========" << endl;
00698 } else {
00699 out << "=====UNSATISFIABLE=====" << endl;
00700 }
00701 } else if (!sol) {
00702 out << "=====UNKNOWN=====" << endl;
00703 }
00704 delete sol;
00705 stopped:
00706 Driver::Cutoff::installCtrlHandler(false);
00707 if (opt.mode() == SM_STAT) {
00708 Gecode::Search::Statistics stat = se.statistics();
00709 out << endl
00710 << "%% runtime: ";
00711 Driver::stop(t_total,out);
00712 out << endl
00713 << "%% solvetime: ";
00714 Driver::stop(t_solve,out);
00715 out << endl
00716 << "%% solutions: "
00717 << std::abs(noOfSolutions - findSol) << endl
00718 << "%% variables: "
00719 << (intVarCount + boolVarCount + setVarCount) << endl
00720 << "%% propagators: " << n_p << endl
00721 << "%% propagations: " << sstat.propagate+stat.propagate << endl
00722 << "%% nodes: " << stat.node << endl
00723 << "%% failures: " << stat.fail << endl
00724 << "%% peak depth: " << stat.depth << endl
00725 << "%% peak memory: "
00726 << static_cast<int>((stat.memory+1023) / 1024) << " KB"
00727 << endl;
00728 }
00729 }
00730
00731 #ifdef GECODE_HAS_QT
00732 void
00733 FlatZincSpace::branchWithPlugin(AST::Node* ann) {
00734 if (AST::Call* c = dynamic_cast<AST::Call*>(ann)) {
00735 QString pluginName(c->id.c_str());
00736 if (QLibrary::isLibrary(pluginName+".dll")) {
00737 pluginName += ".dll";
00738 } else if (QLibrary::isLibrary(pluginName+".dylib")) {
00739 pluginName = "lib" + pluginName + ".dylib";
00740 } else if (QLibrary::isLibrary(pluginName+".so")) {
00741
00742 pluginName = "lib" + pluginName + ".so";
00743 }
00744 QPluginLoader pl(pluginName);
00745 QObject* plugin_o = pl.instance();
00746 if (!plugin_o) {
00747 throw FlatZinc::Error("FlatZinc",
00748 "Error loading plugin "+pluginName.toStdString()+
00749 ": "+pl.errorString().toStdString());
00750 }
00751 BranchPlugin* pb = qobject_cast<BranchPlugin*>(plugin_o);
00752 if (!pb) {
00753 throw FlatZinc::Error("FlatZinc",
00754 "Error loading plugin "+pluginName.toStdString()+
00755 ": does not contain valid PluginBrancher");
00756 }
00757 pb->branch(*this, c);
00758 }
00759 }
00760 #else
00761 void
00762 FlatZincSpace::branchWithPlugin(AST::Node* ann) {
00763 throw FlatZinc::Error("FlatZinc",
00764 "Branching with plugins not supported (requires Qt support)");
00765 }
00766 #endif
00767
00768 void
00769 FlatZincSpace::run(std::ostream& out, const Printer& p,
00770 const FlatZincOptions& opt, Support::Timer& t_total) {
00771 switch (_method) {
00772 case MIN:
00773 case MAX:
00774 if (opt.search() == FlatZincOptions::FZ_SEARCH_BAB)
00775 runEngine<BAB>(out,p,opt,t_total);
00776 else
00777 runEngine<Restart>(out,p,opt,t_total);
00778 break;
00779 case SAT:
00780 runEngine<DFS>(out,p,opt,t_total);
00781 break;
00782 }
00783 }
00784
00785 void
00786 FlatZincSpace::constrain(const Space& s) {
00787 if (_method == MIN)
00788 rel(*this, iv[_optVar], IRT_LE,
00789 static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
00790 else if (_method == MAX)
00791 rel(*this, iv[_optVar], IRT_GR,
00792 static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
00793 }
00794
00795 Space*
00796 FlatZincSpace::copy(bool share) {
00797 return new FlatZincSpace(share, *this);
00798 }
00799
00800 FlatZincSpace::Meth
00801 FlatZincSpace::method(void) const {
00802 return _method;
00803 }
00804
00805 int
00806 FlatZincSpace::optVar(void) const {
00807 return _optVar;
00808 }
00809
00810 void
00811 FlatZincSpace::print(std::ostream& out, const Printer& p) const {
00812 p.print(out, iv, bv
00813 #ifdef GECODE_HAS_SET_VARS
00814 , sv
00815 #endif
00816 );
00817 }
00818
00819 void
00820 FlatZincSpace::shrinkArrays(Printer& p) {
00821 p.shrinkArrays(*this, _optVar, iv, bv
00822 #ifdef GECODE_HAS_SET_VARS
00823 , sv
00824 #endif
00825 );
00826 }
00827
00828 void
00829 Printer::init(AST::Array* output) {
00830 _output = output;
00831 }
00832
00833 void
00834 Printer::printElem(std::ostream& out,
00835 AST::Node* ai,
00836 const Gecode::IntVarArray& iv,
00837 const Gecode::BoolVarArray& bv
00838 #ifdef GECODE_HAS_SET_VARS
00839 , const Gecode::SetVarArray& sv
00840 #endif
00841 ) const {
00842 int k;
00843 if (ai->isInt(k)) {
00844 out << k;
00845 } else if (ai->isIntVar()) {
00846 out << iv[ai->getIntVar()];
00847 } else if (ai->isBoolVar()) {
00848 if (bv[ai->getBoolVar()].min() == 1) {
00849 out << "true";
00850 } else if (bv[ai->getBoolVar()].max() == 0) {
00851 out << "false";
00852 } else {
00853 out << "false..true";
00854 }
00855 #ifdef GECODE_HAS_SET_VARS
00856 } else if (ai->isSetVar()) {
00857 if (!sv[ai->getSetVar()].assigned()) {
00858 out << sv[ai->getSetVar()];
00859 return;
00860 }
00861 SetVarGlbRanges svr(sv[ai->getSetVar()]);
00862 if (!svr()) {
00863 out << "{}";
00864 return;
00865 }
00866 int min = svr.min();
00867 int max = svr.max();
00868 ++svr;
00869 if (svr()) {
00870 SetVarGlbValues svv(sv[ai->getSetVar()]);
00871 int i = svv.val();
00872 out << "{" << i;
00873 ++svv;
00874 for (; svv(); ++svv)
00875 out << ", " << svv.val();
00876 out << "}";
00877 } else {
00878 out << min << ".." << max;
00879 }
00880 #endif
00881 } else if (ai->isBool()) {
00882 out << (ai->getBool() ? "true" : "false");
00883 } else if (ai->isSet()) {
00884 AST::SetLit* s = ai->getSet();
00885 if (s->interval) {
00886 out << s->min << ".." << s->max;
00887 } else {
00888 out << "{";
00889 for (unsigned int i=0; i<s->s.size(); i++) {
00890 out << s->s[i] << (i < s->s.size()-1 ? ", " : "}");
00891 }
00892 }
00893 } else if (ai->isString()) {
00894 std::string s = ai->getString();
00895 for (unsigned int i=0; i<s.size(); i++) {
00896 if (s[i] == '\\' && i<s.size()-1) {
00897 switch (s[i+1]) {
00898 case 'n': out << "\n"; break;
00899 case '\\': out << "\\"; break;
00900 case 't': out << "\t"; break;
00901 default: out << "\\" << s[i+1];
00902 }
00903 i++;
00904 } else {
00905 out << s[i];
00906 }
00907 }
00908 }
00909 }
00910
00911 void
00912 Printer::print(std::ostream& out,
00913 const Gecode::IntVarArray& iv,
00914 const Gecode::BoolVarArray& bv
00915 #ifdef GECODE_HAS_SET_VARS
00916 ,
00917 const Gecode::SetVarArray& sv
00918 #endif
00919 ) const {
00920 if (_output == NULL)
00921 return;
00922 for (unsigned int i=0; i< _output->a.size(); i++) {
00923 AST::Node* ai = _output->a[i];
00924 if (ai->isArray()) {
00925 AST::Array* aia = ai->getArray();
00926 int size = aia->a.size();
00927 out << "[";
00928 for (int j=0; j<size; j++) {
00929 printElem(out,aia->a[j],iv,bv
00930 #ifdef GECODE_HAS_SET_VARS
00931 ,sv
00932 #endif
00933 );
00934 if (j<size-1)
00935 out << ", ";
00936 }
00937 out << "]";
00938 } else {
00939 printElem(out,ai,iv,bv
00940 #ifdef GECODE_HAS_SET_VARS
00941 ,sv
00942 #endif
00943 );
00944 }
00945 }
00946 }
00947
00948 void
00949 Printer::shrinkElement(AST::Node* node,
00950 std::map<int,int>& iv, std::map<int,int>& bv,
00951 std::map<int,int>& sv) {
00952 if (node->isIntVar()) {
00953 AST::IntVar* x = static_cast<AST::IntVar*>(node);
00954 if (iv.find(x->i) == iv.end()) {
00955 int newi = iv.size();
00956 iv[x->i] = newi;
00957 }
00958 x->i = iv[x->i];
00959 } else if (node->isBoolVar()) {
00960 AST::BoolVar* x = static_cast<AST::BoolVar*>(node);
00961 if (bv.find(x->i) == bv.end()) {
00962 int newi = bv.size();
00963 bv[x->i] = newi;
00964 }
00965 x->i = bv[x->i];
00966 } else if (node->isSetVar()) {
00967 AST::SetVar* x = static_cast<AST::SetVar*>(node);
00968 if (sv.find(x->i) == sv.end()) {
00969 int newi = sv.size();
00970 sv[x->i] = newi;
00971 }
00972 x->i = sv[x->i];
00973 }
00974 }
00975
00976 void
00977 Printer::shrinkArrays(Space& home,
00978 int& optVar,
00979 Gecode::IntVarArray& iv,
00980 Gecode::BoolVarArray& bv
00981 #ifdef GECODE_HAS_SET_VARS
00982 ,
00983 Gecode::SetVarArray& sv
00984 #endif
00985 ) {
00986 if (_output == NULL) {
00987 if (optVar == -1) {
00988 iv = IntVarArray(home, 0);
00989 } else {
00990 IntVar ov = iv[optVar];
00991 iv = IntVarArray(home, 1);
00992 iv[0] = ov;
00993 optVar = 0;
00994 }
00995 bv = BoolVarArray(home, 0);
00996 #ifdef GECODE_HAS_SET_VARS
00997 sv = SetVarArray(home, 0);
00998 #endif
00999 return;
01000 }
01001 std::map<int,int> iv_new;
01002 std::map<int,int> bv_new;
01003 std::map<int,int> sv_new;
01004
01005 if (optVar != -1) {
01006 iv_new[optVar] = 0;
01007 optVar = 0;
01008 }
01009
01010 for (unsigned int i=0; i< _output->a.size(); i++) {
01011 AST::Node* ai = _output->a[i];
01012 if (ai->isArray()) {
01013 AST::Array* aia = ai->getArray();
01014 for (unsigned int j=0; j<aia->a.size(); j++) {
01015 shrinkElement(aia->a[j],iv_new,bv_new,sv_new);
01016 }
01017 } else {
01018 shrinkElement(ai,iv_new,bv_new,sv_new);
01019 }
01020 }
01021
01022 IntVarArgs iva(iv_new.size());
01023 for (map<int,int>::iterator i=iv_new.begin(); i != iv_new.end(); ++i) {
01024 iva[(*i).second] = iv[(*i).first];
01025 }
01026 iv = IntVarArray(home, iva);
01027
01028 BoolVarArgs bva(bv_new.size());
01029 for (map<int,int>::iterator i=bv_new.begin(); i != bv_new.end(); ++i) {
01030 bva[(*i).second] = bv[(*i).first];
01031 }
01032 bv = BoolVarArray(home, bva);
01033
01034 #ifdef GECODE_HAS_SET_VARS
01035 SetVarArgs sva(sv_new.size());
01036 for (map<int,int>::iterator i=sv_new.begin(); i != sv_new.end(); ++i) {
01037 sva[(*i).second] = sv[(*i).first];
01038 }
01039 sv = SetVarArray(home, sva);
01040 #endif
01041 }
01042
01043 Printer::~Printer(void) {
01044 delete _output;
01045 }
01046
01047 }}
01048
01049