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 #include <gecode/flatzinc/branch.hh>
00042
00043 #include <gecode/search.hh>
00044
00045 #include <vector>
00046 #include <string>
00047 #include <sstream>
00048 #include <limits>
00049 #include <unordered_set>
00050
00051
00052 namespace std {
00053
00055 template<> struct hash<Gecode::TupleSet> {
00057 forceinline size_t
00058 operator()(const Gecode::TupleSet& x) const {
00059 return x.hash();
00060 }
00061 };
00062
00064 template<> struct hash<Gecode::SharedArray<int> > {
00066 forceinline size_t
00067 operator()(const Gecode::SharedArray<int>& x) const {
00068 size_t seed = static_cast<size_t>(x.size());
00069 for (int i=x.size(); i--; )
00070 Gecode::cmb_hash(seed, x[i]);
00071 return seed;
00072 }
00073 };
00074
00076 template<> struct hash<Gecode::DFA> {
00078 forceinline size_t operator()(const Gecode::DFA& d) const {
00079 return d.hash();
00080 }
00081 };
00082
00083 }
00084
00085 namespace Gecode { namespace FlatZinc {
00086
00087
00088 Rnd defrnd(0);
00089
00102 class AuxVarBrancher : public Brancher {
00103 protected:
00105 bool done;
00107 AuxVarBrancher(Home home, TieBreak<IntVarBranch> int_varsel0,
00108 IntValBranch int_valsel0,
00109 TieBreak<BoolVarBranch> bool_varsel0,
00110 BoolValBranch bool_valsel0
00111 #ifdef GECODE_HAS_SET_VARS
00112 ,
00113 SetVarBranch set_varsel0,
00114 SetValBranch set_valsel0
00115 #endif
00116 #ifdef GECODE_HAS_FLOAT_VARS
00117 ,
00118 TieBreak<FloatVarBranch> float_varsel0,
00119 FloatValBranch float_valsel0
00120 #endif
00121 )
00122 : Brancher(home), done(false),
00123 int_varsel(int_varsel0), int_valsel(int_valsel0),
00124 bool_varsel(bool_varsel0), bool_valsel(bool_valsel0)
00125 #ifdef GECODE_HAS_SET_VARS
00126 , set_varsel(set_varsel0), set_valsel(set_valsel0)
00127 #endif
00128 #ifdef GECODE_HAS_FLOAT_VARS
00129 , float_varsel(float_varsel0), float_valsel(float_valsel0)
00130 #endif
00131 {}
00133 AuxVarBrancher(Space& home, AuxVarBrancher& b)
00134 : Brancher(home, b), done(b.done) {}
00135
00137 class Choice : public Gecode::Choice {
00138 public:
00140 bool fail;
00142 Choice(const Brancher& b, bool fail0)
00143 : Gecode::Choice(b,1), fail(fail0) {}
00145 virtual size_t size(void) const {
00146 return sizeof(Choice);
00147 }
00149 virtual void archive(Archive& e) const {
00150 Gecode::Choice::archive(e);
00151 e.put(fail);
00152 }
00153 };
00154
00155 TieBreak<IntVarBranch> int_varsel;
00156 IntValBranch int_valsel;
00157 TieBreak<BoolVarBranch> bool_varsel;
00158 BoolValBranch bool_valsel;
00159 #ifdef GECODE_HAS_SET_VARS
00160 SetVarBranch set_varsel;
00161 SetValBranch set_valsel;
00162 #endif
00163 #ifdef GECODE_HAS_FLOAT_VARS
00164 TieBreak<FloatVarBranch> float_varsel;
00165 FloatValBranch float_valsel;
00166 #endif
00167
00168 public:
00170 virtual bool status(const Space& _home) const {
00171 if (done) return false;
00172 const FlatZincSpace& home = static_cast<const FlatZincSpace&>(_home);
00173 for (int i=0; i<home.iv_aux.size(); i++)
00174 if (!home.iv_aux[i].assigned()) return true;
00175 for (int i=0; i<home.bv_aux.size(); i++)
00176 if (!home.bv_aux[i].assigned()) return true;
00177 #ifdef GECODE_HAS_SET_VARS
00178 for (int i=0; i<home.sv_aux.size(); i++)
00179 if (!home.sv_aux[i].assigned()) return true;
00180 #endif
00181 #ifdef GECODE_HAS_FLOAT_VARS
00182 for (int i=0; i<home.fv_aux.size(); i++)
00183 if (!home.fv_aux[i].assigned()) return true;
00184 #endif
00185
00186 return false;
00187 }
00189 virtual Choice* choice(Space& home) {
00190 done = true;
00191 FlatZincSpace& fzs = static_cast<FlatZincSpace&>(*home.clone());
00192 fzs.needAuxVars = false;
00193 branch(fzs,fzs.iv_aux,int_varsel,int_valsel);
00194 branch(fzs,fzs.bv_aux,bool_varsel,bool_valsel);
00195 #ifdef GECODE_HAS_SET_VARS
00196 branch(fzs,fzs.sv_aux,set_varsel,set_valsel);
00197 #endif
00198 #ifdef GECODE_HAS_FLOAT_VARS
00199 branch(fzs,fzs.fv_aux,float_varsel,float_valsel);
00200 #endif
00201 Search::Options opt; opt.clone = false;
00202 FlatZincSpace* sol = dfs(&fzs, opt);
00203 if (sol) {
00204 delete sol;
00205 return new Choice(*this,false);
00206 } else {
00207 return new Choice(*this,true);
00208 }
00209 }
00211 virtual Choice* choice(const Space&, Archive& e) {
00212 bool fail; e >> fail;
00213 return new Choice(*this, fail);
00214 }
00216 virtual ExecStatus commit(Space&, const Gecode::Choice& c, unsigned int) {
00217 return static_cast<const Choice&>(c).fail ? ES_FAILED : ES_OK;
00218 }
00220 virtual void print(const Space&, const Gecode::Choice& c,
00221 unsigned int,
00222 std::ostream& o) const {
00223 o << "FlatZinc("
00224 << (static_cast<const Choice&>(c).fail ? "fail" : "ok")
00225 << ")";
00226 }
00228 virtual Actor* copy(Space& home) {
00229 return new (home) AuxVarBrancher(home, *this);
00230 }
00232 static void post(Home home,
00233 TieBreak<IntVarBranch> int_varsel,
00234 IntValBranch int_valsel,
00235 TieBreak<BoolVarBranch> bool_varsel,
00236 BoolValBranch bool_valsel
00237 #ifdef GECODE_HAS_SET_VARS
00238 ,
00239 SetVarBranch set_varsel,
00240 SetValBranch set_valsel
00241 #endif
00242 #ifdef GECODE_HAS_FLOAT_VARS
00243 ,
00244 TieBreak<FloatVarBranch> float_varsel,
00245 FloatValBranch float_valsel
00246 #endif
00247 ) {
00248 (void) new (home) AuxVarBrancher(home, int_varsel, int_valsel,
00249 bool_varsel, bool_valsel
00250 #ifdef GECODE_HAS_SET_VARS
00251 , set_varsel, set_valsel
00252 #endif
00253 #ifdef GECODE_HAS_FLOAT_VARS
00254 , float_varsel, float_valsel
00255 #endif
00256 );
00257 }
00259 virtual size_t dispose(Space&) {
00260 return sizeof(*this);
00261 }
00262 };
00263
00264 class BranchInformationO : public SharedHandle::Object {
00265 private:
00266 struct BI {
00267 std::string r0;
00268 std::string r1;
00269 std::vector<std::string> n;
00270 BI(void) : r0(""), r1(""), n(0) {}
00271 BI(const std::string& r00, const std::string& r10,
00272 const std::vector<std::string>& n0)
00273 : r0(r00), r1(r10), n(n0) {}
00274 };
00275 std::vector<BI> v;
00276 BranchInformationO(std::vector<BI> v0) : v(v0) {}
00277 public:
00278 BranchInformationO(void) {}
00279 virtual ~BranchInformationO(void) {}
00280 virtual SharedHandle::Object* copy(void) const {
00281 return new BranchInformationO(v);
00282 }
00284 void add(BrancherGroup bg,
00285 const std::string& rel0,
00286 const std::string& rel1,
00287 const std::vector<std::string>& n) {
00288 v.resize(std::max(static_cast<unsigned int>(v.size()),bg.id()+1));
00289 v[bg.id()] = BI(rel0,rel1,n);
00290 }
00292 void print(const Brancher& b,
00293 unsigned int a, int i, int n, std::ostream& o) const {
00294 const BI& bi = v[b.group().id()];
00295 o << bi.n[i] << " " << (a==0 ? bi.r0 : bi.r1) << " " << n;
00296 }
00297 #ifdef GECODE_HAS_FLOAT_VARS
00298 void print(const Brancher& b,
00299 unsigned int a, int i, const FloatNumBranch& nl,
00300 std::ostream& o) const {
00301 const BI& bi = v[b.group().id()];
00302 o << bi.n[i] << " "
00303 << (((a == 0) == nl.l) ? "<=" : ">=") << nl.n;
00304 }
00305 #endif
00306 };
00307
00308 BranchInformation::BranchInformation(void)
00309 : SharedHandle(NULL) {}
00310
00311 BranchInformation::BranchInformation(const BranchInformation& bi)
00312 : SharedHandle(bi) {}
00313
00314 void
00315 BranchInformation::init(void) {
00316 assert(object() == NULL);
00317 object(new BranchInformationO());
00318 }
00319
00320 void
00321 BranchInformation::add(BrancherGroup bg,
00322 const std::string& rel0,
00323 const std::string& rel1,
00324 const std::vector<std::string>& n) {
00325 static_cast<BranchInformationO*>(object())->add(bg,rel0,rel1,n);
00326 }
00327 void
00328 BranchInformation::print(const Brancher& b, unsigned int a, int i,
00329 int n, std::ostream& o) const {
00330 static_cast<const BranchInformationO*>(object())->print(b,a,i,n,o);
00331 }
00332 #ifdef GECODE_HAS_FLOAT_VARS
00333 void
00334 BranchInformation::print(const Brancher& b, unsigned int a, int i,
00335 const FloatNumBranch& nl, std::ostream& o) const {
00336 static_cast<const BranchInformationO*>(object())->print(b,a,i,nl,o);
00337 }
00338 #endif
00339 template<class Var>
00340 void varValPrint(const Space &home, const Brancher& b,
00341 unsigned int a,
00342 Var, int i, const int& n,
00343 std::ostream& o) {
00344 static_cast<const FlatZincSpace&>(home).branchInfo.print(b,a,i,n,o);
00345 }
00346
00347 #ifdef GECODE_HAS_FLOAT_VARS
00348 void varValPrintF(const Space &home, const Brancher& b,
00349 unsigned int a,
00350 FloatVar, int i, const FloatNumBranch& nl,
00351 std::ostream& o) {
00352 static_cast<const FlatZincSpace&>(home).branchInfo.print(b,a,i,nl,o);
00353 }
00354 #endif
00355
00356 IntSet vs2is(IntVarSpec* vs) {
00357 if (vs->assigned) {
00358 return IntSet(vs->i,vs->i);
00359 }
00360 if (vs->domain()) {
00361 AST::SetLit* sl = vs->domain.some();
00362 if (sl->interval) {
00363 return IntSet(sl->min, sl->max);
00364 } else {
00365 int* newdom = heap.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
00366 for (int i=sl->s.size(); i--;)
00367 newdom[i] = sl->s[i];
00368 IntSet ret(newdom, sl->s.size());
00369 heap.free(newdom, static_cast<unsigned long int>(sl->s.size()));
00370 return ret;
00371 }
00372 }
00373 return IntSet(Int::Limits::min, Int::Limits::max);
00374 }
00375
00376 int vs2bsl(BoolVarSpec* bs) {
00377 if (bs->assigned) {
00378 return bs->i;
00379 }
00380 if (bs->domain()) {
00381 AST::SetLit* sl = bs->domain.some();
00382 assert(sl->interval);
00383 return std::min(1, std::max(0, sl->min));
00384 }
00385 return 0;
00386 }
00387
00388 int vs2bsh(BoolVarSpec* bs) {
00389 if (bs->assigned) {
00390 return bs->i;
00391 }
00392 if (bs->domain()) {
00393 AST::SetLit* sl = bs->domain.some();
00394 assert(sl->interval);
00395 return std::max(0, std::min(1, sl->max));
00396 }
00397 return 1;
00398 }
00399
00400 TieBreak<IntVarBranch> ann2ivarsel(AST::Node* ann, Rnd rnd, double decay) {
00401 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00402 if (s->id == "input_order")
00403 return TieBreak<IntVarBranch>(INT_VAR_NONE());
00404 if (s->id == "first_fail")
00405 return TieBreak<IntVarBranch>(INT_VAR_SIZE_MIN());
00406 if (s->id == "anti_first_fail")
00407 return TieBreak<IntVarBranch>(INT_VAR_SIZE_MAX());
00408 if (s->id == "smallest")
00409 return TieBreak<IntVarBranch>(INT_VAR_MIN_MIN());
00410 if (s->id == "largest")
00411 return TieBreak<IntVarBranch>(INT_VAR_MAX_MAX());
00412 if (s->id == "occurrence")
00413 return TieBreak<IntVarBranch>(INT_VAR_DEGREE_MAX());
00414 if (s->id == "max_regret")
00415 return TieBreak<IntVarBranch>(INT_VAR_REGRET_MIN_MAX());
00416 if (s->id == "most_constrained")
00417 return TieBreak<IntVarBranch>(INT_VAR_SIZE_MIN(),
00418 INT_VAR_DEGREE_MAX());
00419 if (s->id == "random") {
00420 return TieBreak<IntVarBranch>(INT_VAR_RND(rnd));
00421 }
00422 if (s->id == "dom_w_deg") {
00423 return TieBreak<IntVarBranch>(INT_VAR_AFC_SIZE_MAX(decay));
00424 }
00425 if (s->id == "afc_min")
00426 return TieBreak<IntVarBranch>(INT_VAR_AFC_MIN(decay));
00427 if (s->id == "afc_max")
00428 return TieBreak<IntVarBranch>(INT_VAR_AFC_MAX(decay));
00429 if (s->id == "afc_size_min")
00430 return TieBreak<IntVarBranch>(INT_VAR_AFC_SIZE_MIN(decay));
00431 if (s->id == "afc_size_max") {
00432 return TieBreak<IntVarBranch>(INT_VAR_AFC_SIZE_MAX(decay));
00433 }
00434 if (s->id == "action_min")
00435 return TieBreak<IntVarBranch>(INT_VAR_ACTION_MIN(decay));
00436 if (s->id == "action_max")
00437 return TieBreak<IntVarBranch>(INT_VAR_ACTION_MAX(decay));
00438 if (s->id == "action_size_min")
00439 return TieBreak<IntVarBranch>(INT_VAR_ACTION_SIZE_MIN(decay));
00440 if (s->id == "action_size_max")
00441 return TieBreak<IntVarBranch>(INT_VAR_ACTION_SIZE_MAX(decay));
00442 }
00443 std::cerr << "Warning, ignored search annotation: ";
00444 ann->print(std::cerr);
00445 std::cerr << std::endl;
00446 return TieBreak<IntVarBranch>(INT_VAR_NONE());
00447 }
00448
00449 IntValBranch ann2ivalsel(AST::Node* ann, std::string& r0, std::string& r1,
00450 Rnd rnd) {
00451 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00452 if (s->id == "indomain_min") {
00453 r0 = "="; r1 = "!=";
00454 return INT_VAL_MIN();
00455 }
00456 if (s->id == "indomain_max") {
00457 r0 = "="; r1 = "!=";
00458 return INT_VAL_MAX();
00459 }
00460 if (s->id == "indomain_median") {
00461 r0 = "="; r1 = "!=";
00462 return INT_VAL_MED();
00463 }
00464 if (s->id == "indomain_split") {
00465 r0 = "<="; r1 = ">";
00466 return INT_VAL_SPLIT_MIN();
00467 }
00468 if (s->id == "indomain_reverse_split") {
00469 r0 = ">"; r1 = "<=";
00470 return INT_VAL_SPLIT_MAX();
00471 }
00472 if (s->id == "indomain_random") {
00473 r0 = "="; r1 = "!=";
00474 return INT_VAL_RND(rnd);
00475 }
00476 if (s->id == "indomain") {
00477 r0 = "="; r1 = "=";
00478 return INT_VALUES_MIN();
00479 }
00480 if (s->id == "indomain_middle") {
00481 std::cerr << "Warning, replacing unsupported annotation "
00482 << "indomain_middle with indomain_median" << std::endl;
00483 r0 = "="; r1 = "!=";
00484 return INT_VAL_MED();
00485 }
00486 if (s->id == "indomain_interval") {
00487 std::cerr << "Warning, replacing unsupported annotation "
00488 << "indomain_interval with indomain_split" << std::endl;
00489 r0 = "<="; r1 = ">";
00490 return INT_VAL_SPLIT_MIN();
00491 }
00492 }
00493 std::cerr << "Warning, ignored search annotation: ";
00494 ann->print(std::cerr);
00495 std::cerr << std::endl;
00496 r0 = "="; r1 = "!=";
00497 return INT_VAL_MIN();
00498 }
00499
00500 IntAssign ann2asnivalsel(AST::Node* ann, Rnd rnd) {
00501 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00502 if (s->id == "indomain_min")
00503 return INT_ASSIGN_MIN();
00504 if (s->id == "indomain_max")
00505 return INT_ASSIGN_MAX();
00506 if (s->id == "indomain_median")
00507 return INT_ASSIGN_MED();
00508 if (s->id == "indomain_random") {
00509 return INT_ASSIGN_RND(rnd);
00510 }
00511 }
00512 std::cerr << "Warning, ignored search annotation: ";
00513 ann->print(std::cerr);
00514 std::cerr << std::endl;
00515 return INT_ASSIGN_MIN();
00516 }
00517
00518 TieBreak<BoolVarBranch> ann2bvarsel(AST::Node* ann, Rnd rnd, double decay) {
00519 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00520 if ((s->id == "input_order") ||
00521 (s->id == "first_fail") ||
00522 (s->id == "anti_first_fail") ||
00523 (s->id == "smallest") ||
00524 (s->id == "largest") ||
00525 (s->id == "max_regret"))
00526 return TieBreak<BoolVarBranch>(BOOL_VAR_NONE());
00527 if ((s->id == "occurrence") ||
00528 (s->id == "most_constrained"))
00529 return TieBreak<BoolVarBranch>(BOOL_VAR_DEGREE_MAX());
00530 if (s->id == "random")
00531 return TieBreak<BoolVarBranch>(BOOL_VAR_RND(rnd));
00532 if ((s->id == "afc_min") ||
00533 (s->id == "afc_size_min"))
00534 return TieBreak<BoolVarBranch>(BOOL_VAR_AFC_MIN(decay));
00535 if ((s->id == "afc_max") ||
00536 (s->id == "afc_size_max") ||
00537 (s->id == "dom_w_deg"))
00538 return TieBreak<BoolVarBranch>(BOOL_VAR_AFC_MAX(decay));
00539 if ((s->id == "action_min") &&
00540 (s->id == "action_size_min"))
00541 return TieBreak<BoolVarBranch>(BOOL_VAR_ACTION_MIN(decay));
00542 if ((s->id == "action_max") ||
00543 (s->id == "action_size_max"))
00544 return TieBreak<BoolVarBranch>(BOOL_VAR_ACTION_MAX(decay));
00545 }
00546 std::cerr << "Warning, ignored search annotation: ";
00547 ann->print(std::cerr);
00548 std::cerr << std::endl;
00549 return TieBreak<BoolVarBranch>(BOOL_VAR_NONE());
00550 }
00551
00552 BoolValBranch ann2bvalsel(AST::Node* ann, std::string& r0, std::string& r1,
00553 Rnd rnd) {
00554 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00555 if (s->id == "indomain_min") {
00556 r0 = "="; r1 = "!=";
00557 return BOOL_VAL_MIN();
00558 }
00559 if (s->id == "indomain_max") {
00560 r0 = "="; r1 = "!=";
00561 return BOOL_VAL_MAX();
00562 }
00563 if (s->id == "indomain_median") {
00564 r0 = "="; r1 = "!=";
00565 return BOOL_VAL_MIN();
00566 }
00567 if (s->id == "indomain_split") {
00568 r0 = "<="; r1 = ">";
00569 return BOOL_VAL_MIN();
00570 }
00571 if (s->id == "indomain_reverse_split") {
00572 r0 = ">"; r1 = "<=";
00573 return BOOL_VAL_MAX();
00574 }
00575 if (s->id == "indomain_random") {
00576 r0 = "="; r1 = "!=";
00577 return BOOL_VAL_RND(rnd);
00578 }
00579 if (s->id == "indomain") {
00580 r0 = "="; r1 = "=";
00581 return BOOL_VAL_MIN();
00582 }
00583 if (s->id == "indomain_middle") {
00584 std::cerr << "Warning, replacing unsupported annotation "
00585 << "indomain_middle with indomain_median" << std::endl;
00586 r0 = "="; r1 = "!=";
00587 return BOOL_VAL_MIN();
00588 }
00589 if (s->id == "indomain_interval") {
00590 std::cerr << "Warning, replacing unsupported annotation "
00591 << "indomain_interval with indomain_split" << std::endl;
00592 r0 = "<="; r1 = ">";
00593 return BOOL_VAL_MIN();
00594 }
00595 }
00596 std::cerr << "Warning, ignored search annotation: ";
00597 ann->print(std::cerr);
00598 std::cerr << std::endl;
00599 r0 = "="; r1 = "!=";
00600 return BOOL_VAL_MIN();
00601 }
00602
00603 BoolAssign ann2asnbvalsel(AST::Node* ann, Rnd rnd) {
00604 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00605 if ((s->id == "indomain_min") ||
00606 (s->id == "indomain_median"))
00607 return BOOL_ASSIGN_MIN();
00608 if (s->id == "indomain_max")
00609 return BOOL_ASSIGN_MAX();
00610 if (s->id == "indomain_random") {
00611 return BOOL_ASSIGN_RND(rnd);
00612 }
00613 }
00614 std::cerr << "Warning, ignored search annotation: ";
00615 ann->print(std::cerr);
00616 std::cerr << std::endl;
00617 return BOOL_ASSIGN_MIN();
00618 }
00619
00620 #ifdef GECODE_HAS_SET_VARS
00621 SetVarBranch ann2svarsel(AST::Node* ann, Rnd rnd, double decay) {
00622 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00623 if (s->id == "input_order")
00624 return SET_VAR_NONE();
00625 if (s->id == "first_fail")
00626 return SET_VAR_SIZE_MIN();
00627 if (s->id == "anti_first_fail")
00628 return SET_VAR_SIZE_MAX();
00629 if (s->id == "smallest")
00630 return SET_VAR_MIN_MIN();
00631 if (s->id == "largest")
00632 return SET_VAR_MAX_MAX();
00633 if (s->id == "afc_min")
00634 return SET_VAR_AFC_MIN(decay);
00635 if (s->id == "afc_max")
00636 return SET_VAR_AFC_MAX(decay);
00637 if (s->id == "afc_size_min")
00638 return SET_VAR_AFC_SIZE_MIN(decay);
00639 if (s->id == "afc_size_max")
00640 return SET_VAR_AFC_SIZE_MAX(decay);
00641 if (s->id == "action_min")
00642 return SET_VAR_ACTION_MIN(decay);
00643 if (s->id == "action_max")
00644 return SET_VAR_ACTION_MAX(decay);
00645 if (s->id == "action_size_min")
00646 return SET_VAR_ACTION_SIZE_MIN(decay);
00647 if (s->id == "action_size_max")
00648 return SET_VAR_ACTION_SIZE_MAX(decay);
00649 if (s->id == "random") {
00650 return SET_VAR_RND(rnd);
00651 }
00652 }
00653 std::cerr << "Warning, ignored search annotation: ";
00654 ann->print(std::cerr);
00655 std::cerr << std::endl;
00656 return SET_VAR_NONE();
00657 }
00658
00659 SetValBranch ann2svalsel(AST::Node* ann, std::string r0, std::string r1,
00660 Rnd rnd) {
00661 (void) rnd;
00662 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00663 if (s->id == "indomain_min") {
00664 r0 = "in"; r1 = "not in";
00665 return SET_VAL_MIN_INC();
00666 }
00667 if (s->id == "indomain_max") {
00668 r0 = "in"; r1 = "not in";
00669 return SET_VAL_MAX_INC();
00670 }
00671 if (s->id == "outdomain_min") {
00672 r1 = "in"; r0 = "not in";
00673 return SET_VAL_MIN_EXC();
00674 }
00675 if (s->id == "outdomain_max") {
00676 r1 = "in"; r0 = "not in";
00677 return SET_VAL_MAX_EXC();
00678 }
00679 }
00680 std::cerr << "Warning, ignored search annotation: ";
00681 ann->print(std::cerr);
00682 std::cerr << std::endl;
00683 r0 = "in"; r1 = "not in";
00684 return SET_VAL_MIN_INC();
00685 }
00686 #endif
00687
00688 #ifdef GECODE_HAS_FLOAT_VARS
00689 TieBreak<FloatVarBranch> ann2fvarsel(AST::Node* ann, Rnd rnd,
00690 double decay) {
00691 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00692 if (s->id == "input_order")
00693 return TieBreak<FloatVarBranch>(FLOAT_VAR_NONE());
00694 if (s->id == "first_fail")
00695 return TieBreak<FloatVarBranch>(FLOAT_VAR_SIZE_MIN());
00696 if (s->id == "anti_first_fail")
00697 return TieBreak<FloatVarBranch>(FLOAT_VAR_SIZE_MAX());
00698 if (s->id == "smallest")
00699 return TieBreak<FloatVarBranch>(FLOAT_VAR_MIN_MIN());
00700 if (s->id == "largest")
00701 return TieBreak<FloatVarBranch>(FLOAT_VAR_MAX_MAX());
00702 if (s->id == "occurrence")
00703 return TieBreak<FloatVarBranch>(FLOAT_VAR_DEGREE_MAX());
00704 if (s->id == "most_constrained")
00705 return TieBreak<FloatVarBranch>(FLOAT_VAR_SIZE_MIN(),
00706 FLOAT_VAR_DEGREE_MAX());
00707 if (s->id == "random") {
00708 return TieBreak<FloatVarBranch>(FLOAT_VAR_RND(rnd));
00709 }
00710 if (s->id == "afc_min")
00711 return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_MIN(decay));
00712 if (s->id == "afc_max")
00713 return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_MAX(decay));
00714 if (s->id == "afc_size_min")
00715 return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_SIZE_MIN(decay));
00716 if (s->id == "afc_size_max")
00717 return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_SIZE_MAX(decay));
00718 if (s->id == "action_min")
00719 return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTION_MIN(decay));
00720 if (s->id == "action_max")
00721 return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTION_MAX(decay));
00722 if (s->id == "action_size_min")
00723 return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTION_SIZE_MIN(decay));
00724 if (s->id == "action_size_max")
00725 return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTION_SIZE_MAX(decay));
00726 }
00727 std::cerr << "Warning, ignored search annotation: ";
00728 ann->print(std::cerr);
00729 std::cerr << std::endl;
00730 return TieBreak<FloatVarBranch>(FLOAT_VAR_NONE());
00731 }
00732
00733 FloatValBranch ann2fvalsel(AST::Node* ann, std::string r0, std::string r1) {
00734 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00735 if (s->id == "indomain_split") {
00736 r0 = "<="; r1 = ">";
00737 return FLOAT_VAL_SPLIT_MIN();
00738 }
00739 if (s->id == "indomain_reverse_split") {
00740 r1 = "<="; r0 = ">";
00741 return FLOAT_VAL_SPLIT_MAX();
00742 }
00743 }
00744 std::cerr << "Warning, ignored search annotation: ";
00745 ann->print(std::cerr);
00746 std::cerr << std::endl;
00747 r0 = "<="; r1 = ">";
00748 return FLOAT_VAL_SPLIT_MIN();
00749 }
00750
00751 #endif
00752
00753 class FlatZincSpaceInitData {
00754 public:
00756 typedef std::unordered_set<TupleSet> TupleSetSet;
00758 TupleSetSet tupleSetSet;
00759
00761 typedef std::unordered_set<SharedArray<int> > IntSharedArraySet;
00763 IntSharedArraySet intSharedArraySet;
00764
00766 typedef std::unordered_set<DFA> DFASet;
00768 DFASet dfaSet;
00769
00771 FlatZincSpaceInitData(void) {}
00772 };
00773
00774 FlatZincSpace::FlatZincSpace(FlatZincSpace& f)
00775 : Space(f),
00776 _initData(NULL), _random(f._random),
00777 _solveAnnotations(NULL), iv_boolalias(NULL),
00778 #ifdef GECODE_HAS_FLOAT_VARS
00779 step(f.step),
00780 #endif
00781 needAuxVars(f.needAuxVars) {
00782 _optVar = f._optVar;
00783 _optVarIsInt = f._optVarIsInt;
00784 _method = f._method;
00785 _lns = f._lns;
00786 _lnsInitialSolution = f._lnsInitialSolution;
00787 branchInfo = f.branchInfo;
00788 iv.update(*this, f.iv);
00789 iv_lns.update(*this, f.iv_lns);
00790 intVarCount = f.intVarCount;
00791
00792 if (needAuxVars) {
00793 IntVarArgs iva;
00794 for (int i=0; i<f.iv_aux.size(); i++) {
00795 if (!f.iv_aux[i].assigned()) {
00796 iva << IntVar();
00797 iva[iva.size()-1].update(*this, f.iv_aux[i]);
00798 }
00799 }
00800 iv_aux = IntVarArray(*this, iva);
00801 }
00802
00803 bv.update(*this, f.bv);
00804 boolVarCount = f.boolVarCount;
00805 if (needAuxVars) {
00806 BoolVarArgs bva;
00807 for (int i=0; i<f.bv_aux.size(); i++) {
00808 if (!f.bv_aux[i].assigned()) {
00809 bva << BoolVar();
00810 bva[bva.size()-1].update(*this, f.bv_aux[i]);
00811 }
00812 }
00813 bv_aux = BoolVarArray(*this, bva);
00814 }
00815
00816 #ifdef GECODE_HAS_SET_VARS
00817 sv.update(*this, f.sv);
00818 setVarCount = f.setVarCount;
00819 if (needAuxVars) {
00820 SetVarArgs sva;
00821 for (int i=0; i<f.sv_aux.size(); i++) {
00822 if (!f.sv_aux[i].assigned()) {
00823 sva << SetVar();
00824 sva[sva.size()-1].update(*this, f.sv_aux[i]);
00825 }
00826 }
00827 sv_aux = SetVarArray(*this, sva);
00828 }
00829 #endif
00830 #ifdef GECODE_HAS_FLOAT_VARS
00831 fv.update(*this, f.fv);
00832 floatVarCount = f.floatVarCount;
00833 if (needAuxVars) {
00834 FloatVarArgs fva;
00835 for (int i=0; i<f.fv_aux.size(); i++) {
00836 if (!f.fv_aux[i].assigned()) {
00837 fva << FloatVar();
00838 fva[fva.size()-1].update(*this, f.fv_aux[i]);
00839 }
00840 }
00841 fv_aux = FloatVarArray(*this, fva);
00842 }
00843 #endif
00844 }
00845
00846 FlatZincSpace::FlatZincSpace(Rnd& random)
00847 : _initData(new FlatZincSpaceInitData),
00848 intVarCount(-1), boolVarCount(-1), floatVarCount(-1), setVarCount(-1),
00849 _optVar(-1), _optVarIsInt(true), _lns(0), _lnsInitialSolution(0),
00850 _random(random),
00851 _solveAnnotations(NULL), needAuxVars(true) {
00852 branchInfo.init();
00853 }
00854
00855 void
00856 FlatZincSpace::init(int intVars, int boolVars,
00857 int setVars, int floatVars) {
00858 (void) setVars;
00859 (void) floatVars;
00860
00861 intVarCount = 0;
00862 iv = IntVarArray(*this, intVars);
00863 iv_introduced = std::vector<bool>(2*intVars);
00864 iv_boolalias = alloc<int>(intVars+(intVars==0?1:0));
00865 boolVarCount = 0;
00866 bv = BoolVarArray(*this, boolVars);
00867 bv_introduced = std::vector<bool>(2*boolVars);
00868 #ifdef GECODE_HAS_SET_VARS
00869 setVarCount = 0;
00870 sv = SetVarArray(*this, setVars);
00871 sv_introduced = std::vector<bool>(2*setVars);
00872 #endif
00873 #ifdef GECODE_HAS_FLOAT_VARS
00874 floatVarCount = 0;
00875 fv = FloatVarArray(*this, floatVars);
00876 fv_introduced = std::vector<bool>(2*floatVars);
00877 #endif
00878 }
00879
00880 void
00881 FlatZincSpace::newIntVar(IntVarSpec* vs) {
00882 if (vs->alias) {
00883 iv[intVarCount++] = iv[vs->i];
00884 } else {
00885 IntSet dom(vs2is(vs));
00886 if (dom.size()==0) {
00887 fail();
00888 return;
00889 } else {
00890 iv[intVarCount++] = IntVar(*this, dom);
00891 }
00892 }
00893 iv_introduced[2*(intVarCount-1)] = vs->introduced;
00894 iv_introduced[2*(intVarCount-1)+1] = vs->funcDep;
00895 iv_boolalias[intVarCount-1] = -1;
00896 }
00897
00898 void
00899 FlatZincSpace::aliasBool2Int(int iv, int bv) {
00900 iv_boolalias[iv] = bv;
00901 }
00902 int
00903 FlatZincSpace::aliasBool2Int(int iv) {
00904 return iv_boolalias[iv];
00905 }
00906
00907 void
00908 FlatZincSpace::newBoolVar(BoolVarSpec* vs) {
00909 if (vs->alias) {
00910 bv[boolVarCount++] = bv[vs->i];
00911 } else {
00912 bv[boolVarCount++] = BoolVar(*this, vs2bsl(vs), vs2bsh(vs));
00913 }
00914 bv_introduced[2*(boolVarCount-1)] = vs->introduced;
00915 bv_introduced[2*(boolVarCount-1)+1] = vs->funcDep;
00916 }
00917
00918 #ifdef GECODE_HAS_SET_VARS
00919 void
00920 FlatZincSpace::newSetVar(SetVarSpec* vs) {
00921 if (vs->alias) {
00922 sv[setVarCount++] = sv[vs->i];
00923 } else if (vs->assigned) {
00924 assert(vs->upperBound());
00925 AST::SetLit* vsv = vs->upperBound.some();
00926 if (vsv->interval) {
00927 IntSet d(vsv->min, vsv->max);
00928 sv[setVarCount++] = SetVar(*this, d, d);
00929 } else {
00930 int* is = heap.alloc<int>(static_cast<unsigned long int>(vsv->s.size()));
00931 for (int i=vsv->s.size(); i--; )
00932 is[i] = vsv->s[i];
00933 IntSet d(is, vsv->s.size());
00934 heap.free(is,static_cast<unsigned long int>(vsv->s.size()));
00935 sv[setVarCount++] = SetVar(*this, d, d);
00936 }
00937 } else if (vs->upperBound()) {
00938 AST::SetLit* vsv = vs->upperBound.some();
00939 if (vsv->interval) {
00940 IntSet d(vsv->min, vsv->max);
00941 sv[setVarCount++] = SetVar(*this, IntSet::empty, d);
00942 } else {
00943 int* is = heap.alloc<int>(static_cast<unsigned long int>(vsv->s.size()));
00944 for (int i=vsv->s.size(); i--; )
00945 is[i] = vsv->s[i];
00946 IntSet d(is, vsv->s.size());
00947 heap.free(is,static_cast<unsigned long int>(vsv->s.size()));
00948 sv[setVarCount++] = SetVar(*this, IntSet::empty, d);
00949 }
00950 } else {
00951 sv[setVarCount++] = SetVar(*this, IntSet::empty,
00952 IntSet(Set::Limits::min,
00953 Set::Limits::max));
00954 }
00955 sv_introduced[2*(setVarCount-1)] = vs->introduced;
00956 sv_introduced[2*(setVarCount-1)+1] = vs->funcDep;
00957 }
00958 #else
00959 void
00960 FlatZincSpace::newSetVar(SetVarSpec*) {
00961 throw FlatZinc::Error("Gecode", "set variables not supported");
00962 }
00963 #endif
00964
00965 #ifdef GECODE_HAS_FLOAT_VARS
00966 void
00967 FlatZincSpace::newFloatVar(FloatVarSpec* vs) {
00968 if (vs->alias) {
00969 fv[floatVarCount++] = fv[vs->i];
00970 } else {
00971 double dmin, dmax;
00972 if (vs->domain()) {
00973 dmin = vs->domain.some().first;
00974 dmax = vs->domain.some().second;
00975 if (dmin > dmax) {
00976 fail();
00977 return;
00978 }
00979 } else {
00980 dmin = Float::Limits::min;
00981 dmax = Float::Limits::max;
00982 }
00983 fv[floatVarCount++] = FloatVar(*this, dmin, dmax);
00984 }
00985 fv_introduced[2*(floatVarCount-1)] = vs->introduced;
00986 fv_introduced[2*(floatVarCount-1)+1] = vs->funcDep;
00987 }
00988 #else
00989 void
00990 FlatZincSpace::newFloatVar(FloatVarSpec*) {
00991 throw FlatZinc::Error("Gecode", "float variables not supported");
00992 }
00993 #endif
00994
00995 namespace {
00996 struct ConExprOrder {
00997 bool operator() (ConExpr* ce0, ConExpr* ce1) {
00998 return ce0->args->a.size() < ce1->args->a.size();
00999 }
01000 };
01001 }
01002
01003 void
01004 FlatZincSpace::postConstraints(std::vector<ConExpr*>& ces) {
01005 ConExprOrder ceo;
01006 std::sort(ces.begin(), ces.end(), ceo);
01007
01008 for (unsigned int i=0; i<ces.size(); i++) {
01009 const ConExpr& ce = *ces[i];
01010 try {
01011 registry().post(*this, ce);
01012 } catch (Gecode::Exception& e) {
01013 throw FlatZinc::Error("Gecode", e.what());
01014 } catch (AST::TypeError& e) {
01015 throw FlatZinc::Error("Type error", e.what());
01016 }
01017 delete ces[i];
01018 ces[i] = NULL;
01019 }
01020 }
01021
01022 void flattenAnnotations(AST::Array* ann, std::vector<AST::Node*>& out) {
01023 for (unsigned int i=0; i<ann->a.size(); i++) {
01024 if (ann->a[i]->isCall("seq_search")) {
01025 AST::Call* c = ann->a[i]->getCall();
01026 if (c->args->isArray())
01027 flattenAnnotations(c->args->getArray(), out);
01028 else
01029 out.push_back(c->args);
01030 } else {
01031 out.push_back(ann->a[i]);
01032 }
01033 }
01034 }
01035
01036 void
01037 FlatZincSpace::createBranchers(Printer&p, AST::Node* ann, FlatZincOptions& opt,
01038 bool ignoreUnknown,
01039 std::ostream& err) {
01040 int seed = opt.seed();
01041 double decay = opt.decay();
01042 Rnd rnd(static_cast<unsigned int>(seed));
01043 TieBreak<IntVarBranch> def_int_varsel = INT_VAR_AFC_SIZE_MAX(0.99);
01044 IntBoolVarBranch def_intbool_varsel = INTBOOL_VAR_AFC_SIZE_MAX(0.99);
01045 IntValBranch def_int_valsel = INT_VAL_MIN();
01046 std::string def_int_rel_left = "=";
01047 std::string def_int_rel_right = "!=";
01048 TieBreak<BoolVarBranch> def_bool_varsel = BOOL_VAR_AFC_MAX(0.99);
01049 BoolValBranch def_bool_valsel = BOOL_VAL_MIN();
01050 std::string def_bool_rel_left = "=";
01051 std::string def_bool_rel_right = "!=";
01052 #ifdef GECODE_HAS_SET_VARS
01053 SetVarBranch def_set_varsel = SET_VAR_AFC_SIZE_MAX(0.99);
01054 SetValBranch def_set_valsel = SET_VAL_MIN_INC();
01055 std::string def_set_rel_left = "in";
01056 std::string def_set_rel_right = "not in";
01057 #endif
01058 #ifdef GECODE_HAS_FLOAT_VARS
01059 TieBreak<FloatVarBranch> def_float_varsel = FLOAT_VAR_SIZE_MIN();
01060 FloatValBranch def_float_valsel = FLOAT_VAL_SPLIT_MIN();
01061 std::string def_float_rel_left = "<=";
01062 std::string def_float_rel_right = ">";
01063 #endif
01064
01065 std::vector<bool> iv_searched(iv.size());
01066 for (unsigned int i=iv.size(); i--;)
01067 iv_searched[i] = false;
01068 std::vector<bool> bv_searched(bv.size());
01069 for (unsigned int i=bv.size(); i--;)
01070 bv_searched[i] = false;
01071 #ifdef GECODE_HAS_SET_VARS
01072 std::vector<bool> sv_searched(sv.size());
01073 for (unsigned int i=sv.size(); i--;)
01074 sv_searched[i] = false;
01075 #endif
01076 #ifdef GECODE_HAS_FLOAT_VARS
01077 std::vector<bool> fv_searched(fv.size());
01078 for (unsigned int i=fv.size(); i--;)
01079 fv_searched[i] = false;
01080 #endif
01081
01082 _lns = 0;
01083 if (ann) {
01084 std::vector<AST::Node*> flatAnn;
01085 if (ann->isArray()) {
01086 flattenAnnotations(ann->getArray() , flatAnn);
01087 } else {
01088 flatAnn.push_back(ann);
01089 }
01090
01091 for (unsigned int i=0; i<flatAnn.size(); i++) {
01092 if (flatAnn[i]->isCall("restart_geometric")) {
01093 AST::Call* call = flatAnn[i]->getCall("restart_geometric");
01094 opt.restart(RM_GEOMETRIC);
01095 AST::Array* args = call->getArgs(2);
01096 opt.restart_base(args->a[0]->getFloat());
01097 opt.restart_scale(args->a[1]->getInt());
01098 } else if (flatAnn[i]->isCall("restart_luby")) {
01099 AST::Call* call = flatAnn[i]->getCall("restart_luby");
01100 opt.restart(RM_LUBY);
01101 opt.restart_scale(call->args->getInt());
01102 } else if (flatAnn[i]->isCall("restart_linear")) {
01103 AST::Call* call = flatAnn[i]->getCall("restart_linear");
01104 opt.restart(RM_LINEAR);
01105 opt.restart_scale(call->args->getInt());
01106 } else if (flatAnn[i]->isCall("restart_constant")) {
01107 AST::Call* call = flatAnn[i]->getCall("restart_constant");
01108 opt.restart(RM_CONSTANT);
01109 opt.restart_scale(call->args->getInt());
01110 } else if (flatAnn[i]->isCall("restart_none")) {
01111 opt.restart(RM_NONE);
01112 } else if (flatAnn[i]->isCall("relax_and_reconstruct")) {
01113 if (_lns != 0)
01114 throw FlatZinc::Error("FlatZinc",
01115 "Only one relax_and_reconstruct annotation allowed");
01116 AST::Call *call = flatAnn[i]->getCall("relax_and_reconstruct");
01117 AST::Array* args;
01118 if (call->args->getArray()->a.size()==2) {
01119 args = call->getArgs(2);
01120 } else {
01121 args = call->getArgs(3);
01122 }
01123 _lns = args->a[1]->getInt();
01124 AST::Array *vars = args->a[0]->getArray();
01125 int k=vars->a.size();
01126 for (int i=vars->a.size(); i--;)
01127 if (vars->a[i]->isInt())
01128 k--;
01129 iv_lns = IntVarArray(*this, k);
01130 k = 0;
01131 for (unsigned int i=0; i<vars->a.size(); i++) {
01132 if (vars->a[i]->isInt())
01133 continue;
01134 iv_lns[k++] = iv[vars->a[i]->getIntVar()];
01135 }
01136 if (args->a.size()==3) {
01137 AST::Array *initial = args->a[2]->getArray();
01138 _lnsInitialSolution = IntSharedArray(initial->a.size());
01139 for (unsigned int i=initial->a.size(); i--;)
01140 _lnsInitialSolution[i] = initial->a[i]->getInt();
01141 }
01142 } else if (flatAnn[i]->isCall("gecode_search")) {
01143 AST::Call* c = flatAnn[i]->getCall();
01144 branchWithPlugin(c->args);
01145 } else if (flatAnn[i]->isCall("int_search")) {
01146 AST::Call *call = flatAnn[i]->getCall("int_search");
01147 AST::Array *args = call->getArgs(4);
01148 AST::Array *vars = args->a[0]->getArray();
01149 int k=vars->a.size();
01150 for (int i=vars->a.size(); i--;)
01151 if (vars->a[i]->isInt())
01152 k--;
01153 IntVarArgs va(k);
01154 std::vector<std::string> names;
01155 k=0;
01156 for (unsigned int i=0; i<vars->a.size(); i++) {
01157 if (vars->a[i]->isInt())
01158 continue;
01159 va[k++] = iv[vars->a[i]->getIntVar()];
01160 iv_searched[vars->a[i]->getIntVar()] = true;
01161 names.push_back(vars->a[i]->getVarName());
01162 }
01163 std::string r0, r1;
01164 {
01165 BrancherGroup bg;
01166 branch(bg(*this), va,
01167 ann2ivarsel(args->a[1],rnd,decay),
01168 ann2ivalsel(args->a[2],r0,r1,rnd),
01169 nullptr,
01170 &varValPrint<IntVar>);
01171 branchInfo.add(bg,r0,r1,names);
01172 }
01173 } else if (flatAnn[i]->isCall("int_assign")) {
01174 AST::Call *call = flatAnn[i]->getCall("int_assign");
01175 AST::Array *args = call->getArgs(2);
01176 AST::Array *vars = args->a[0]->getArray();
01177 int k=vars->a.size();
01178 for (int i=vars->a.size(); i--;)
01179 if (vars->a[i]->isInt())
01180 k--;
01181 IntVarArgs va(k);
01182 k=0;
01183 for (unsigned int i=0; i<vars->a.size(); i++) {
01184 if (vars->a[i]->isInt())
01185 continue;
01186 va[k++] = iv[vars->a[i]->getIntVar()];
01187 iv_searched[vars->a[i]->getIntVar()] = true;
01188 }
01189 assign(*this, va, ann2asnivalsel(args->a[1],rnd), nullptr,
01190 &varValPrint<IntVar>);
01191 } else if (flatAnn[i]->isCall("bool_search")) {
01192 AST::Call *call = flatAnn[i]->getCall("bool_search");
01193 AST::Array *args = call->getArgs(4);
01194 AST::Array *vars = args->a[0]->getArray();
01195 int k=vars->a.size();
01196 for (int i=vars->a.size(); i--;)
01197 if (vars->a[i]->isBool())
01198 k--;
01199 BoolVarArgs va(k);
01200 k=0;
01201 std::vector<std::string> names;
01202 for (unsigned int i=0; i<vars->a.size(); i++) {
01203 if (vars->a[i]->isBool())
01204 continue;
01205 va[k++] = bv[vars->a[i]->getBoolVar()];
01206 bv_searched[vars->a[i]->getBoolVar()] = true;
01207 names.push_back(vars->a[i]->getVarName());
01208 }
01209
01210 std::string r0, r1;
01211 {
01212 BrancherGroup bg;
01213 branch(bg(*this), va,
01214 ann2bvarsel(args->a[1],rnd,decay),
01215 ann2bvalsel(args->a[2],r0,r1,rnd),
01216 nullptr,
01217 &varValPrint<BoolVar>);
01218 branchInfo.add(bg,r0,r1,names);
01219 }
01220 } else if (flatAnn[i]->isCall("int_default_search")) {
01221 AST::Call *call = flatAnn[i]->getCall("int_default_search");
01222 AST::Array *args = call->getArgs(2);
01223 def_int_varsel = ann2ivarsel(args->a[0],rnd,decay);
01224 def_int_valsel = ann2ivalsel(args->a[1],
01225 def_int_rel_left,def_int_rel_right,rnd);
01226 } else if (flatAnn[i]->isCall("bool_default_search")) {
01227 AST::Call *call = flatAnn[i]->getCall("bool_default_search");
01228 AST::Array *args = call->getArgs(2);
01229 def_bool_varsel = ann2bvarsel(args->a[0],rnd,decay);
01230 def_bool_valsel = ann2bvalsel(args->a[1],
01231 def_bool_rel_left,def_bool_rel_right,
01232 rnd);
01233 } else if (flatAnn[i]->isCall("set_search")) {
01234 #ifdef GECODE_HAS_SET_VARS
01235 AST::Call *call = flatAnn[i]->getCall("set_search");
01236 AST::Array *args = call->getArgs(4);
01237 AST::Array *vars = args->a[0]->getArray();
01238 int k=vars->a.size();
01239 for (int i=vars->a.size(); i--;)
01240 if (vars->a[i]->isSet())
01241 k--;
01242 SetVarArgs va(k);
01243 k=0;
01244 std::vector<std::string> names;
01245 for (unsigned int i=0; i<vars->a.size(); i++) {
01246 if (vars->a[i]->isSet())
01247 continue;
01248 va[k++] = sv[vars->a[i]->getSetVar()];
01249 sv_searched[vars->a[i]->getSetVar()] = true;
01250 names.push_back(vars->a[i]->getVarName());
01251 }
01252 std::string r0, r1;
01253 {
01254 BrancherGroup bg;
01255 branch(bg(*this), va,
01256 ann2svarsel(args->a[1],rnd,decay),
01257 ann2svalsel(args->a[2],r0,r1,rnd),
01258 nullptr,
01259 &varValPrint<SetVar>);
01260 branchInfo.add(bg,r0,r1,names);
01261 }
01262 #else
01263 if (!ignoreUnknown) {
01264 err << "Warning, ignored search annotation: ";
01265 flatAnn[i]->print(err);
01266 err << std::endl;
01267 }
01268 #endif
01269 } else if (flatAnn[i]->isCall("set_default_search")) {
01270 #ifdef GECODE_HAS_SET_VARS
01271 AST::Call *call = flatAnn[i]->getCall("set_default_search");
01272 AST::Array *args = call->getArgs(2);
01273 def_set_varsel = ann2svarsel(args->a[0],rnd,decay);
01274 def_set_valsel = ann2svalsel(args->a[1],
01275 def_set_rel_left,def_set_rel_right,rnd);
01276 #else
01277 if (!ignoreUnknown) {
01278 err << "Warning, ignored search annotation: ";
01279 flatAnn[i]->print(err);
01280 err << std::endl;
01281 }
01282 #endif
01283 } else if (flatAnn[i]->isCall("float_default_search")) {
01284 #ifdef GECODE_HAS_FLOAT_VARS
01285 AST::Call *call = flatAnn[i]->getCall("float_default_search");
01286 AST::Array *args = call->getArgs(2);
01287 def_float_varsel = ann2fvarsel(args->a[0],rnd,decay);
01288 def_float_valsel = ann2fvalsel(args->a[1],
01289 def_float_rel_left,def_float_rel_right);
01290 #else
01291 if (!ignoreUnknown) {
01292 err << "Warning, ignored search annotation: ";
01293 flatAnn[i]->print(err);
01294 err << std::endl;
01295 }
01296 #endif
01297 } else if (flatAnn[i]->isCall("float_search")) {
01298 #ifdef GECODE_HAS_FLOAT_VARS
01299 AST::Call *call = flatAnn[i]->getCall("float_search");
01300 AST::Array *args = call->getArgs(5);
01301 AST::Array *vars = args->a[0]->getArray();
01302 int k=vars->a.size();
01303 for (int i=vars->a.size(); i--;)
01304 if (vars->a[i]->isFloat())
01305 k--;
01306 FloatVarArgs va(k);
01307 k=0;
01308 std::vector<std::string> names;
01309 for (unsigned int i=0; i<vars->a.size(); i++) {
01310 if (vars->a[i]->isFloat())
01311 continue;
01312 va[k++] = fv[vars->a[i]->getFloatVar()];
01313 fv_searched[vars->a[i]->getFloatVar()] = true;
01314 names.push_back(vars->a[i]->getVarName());
01315 }
01316 std::string r0, r1;
01317 {
01318 BrancherGroup bg;
01319 branch(bg(*this), va,
01320 ann2fvarsel(args->a[2],rnd,decay),
01321 ann2fvalsel(args->a[3],r0,r1),
01322 nullptr,
01323 &varValPrintF);
01324 branchInfo.add(bg,r0,r1,names);
01325 }
01326 #else
01327 if (!ignoreUnknown) {
01328 err << "Warning, ignored search annotation: ";
01329 flatAnn[i]->print(err);
01330 err << std::endl;
01331 }
01332 #endif
01333 } else {
01334 if (!ignoreUnknown) {
01335 err << "Warning, ignored search annotation: ";
01336 flatAnn[i]->print(err);
01337 err << std::endl;
01338 }
01339 }
01340 }
01341 }
01342 int introduced = 0;
01343 int funcdep = 0;
01344 int searched = 0;
01345 for (int i=iv.size(); i--;) {
01346 if (iv_searched[i] || (_method != SAT && _optVarIsInt && _optVar==i)) {
01347 searched++;
01348 } else if (iv_introduced[2*i]) {
01349 if (iv_introduced[2*i+1]) {
01350 funcdep++;
01351 } else {
01352 introduced++;
01353 }
01354 }
01355 }
01356 std::vector<std::string> iv_sol_names(iv.size()-(introduced+funcdep+searched));
01357 IntVarArgs iv_sol(iv.size()-(introduced+funcdep+searched));
01358 std::vector<std::string> iv_tmp_names(introduced);
01359 IntVarArgs iv_tmp(introduced);
01360 for (int i=iv.size(), j=0, k=0; i--;) {
01361 if (iv_searched[i] || (_method != SAT && _optVarIsInt && _optVar==i))
01362 continue;
01363 if (iv_introduced[2*i]) {
01364 if (!iv_introduced[2*i+1]) {
01365 iv_tmp_names[j] = p.intVarName(i);
01366 iv_tmp[j++] = iv[i];
01367 }
01368 } else {
01369 iv_sol_names[k] = p.intVarName(i);
01370 iv_sol[k++] = iv[i];
01371 }
01372 }
01373
01374 introduced = 0;
01375 funcdep = 0;
01376 searched = 0;
01377 for (int i=bv.size(); i--;) {
01378 if (bv_searched[i]) {
01379 searched++;
01380 } else if (bv_introduced[2*i]) {
01381 if (bv_introduced[2*i+1]) {
01382 funcdep++;
01383 } else {
01384 introduced++;
01385 }
01386 }
01387 }
01388 std::vector<std::string> bv_sol_names(bv.size()-(introduced+funcdep+searched));
01389 BoolVarArgs bv_sol(bv.size()-(introduced+funcdep+searched));
01390 BoolVarArgs bv_tmp(introduced);
01391 std::vector<std::string> bv_tmp_names(introduced);
01392 for (int i=bv.size(), j=0, k=0; i--;) {
01393 if (bv_searched[i])
01394 continue;
01395 if (bv_introduced[2*i]) {
01396 if (!bv_introduced[2*i+1]) {
01397 bv_tmp_names[j] = p.boolVarName(i);
01398 bv_tmp[j++] = bv[i];
01399 }
01400 } else {
01401 bv_sol_names[k] = p.boolVarName(i);
01402 bv_sol[k++] = bv[i];
01403 }
01404 }
01405
01406 if (iv_sol.size() > 0 && bv_sol.size() > 0) {
01407 branch(*this, iv_sol, bv_sol, def_intbool_varsel, def_int_valsel);
01408 } else if (iv_sol.size() > 0) {
01409 BrancherGroup bg;
01410 branch(bg(*this), iv_sol, def_int_varsel, def_int_valsel, nullptr,
01411 &varValPrint<IntVar>);
01412 branchInfo.add(bg,def_int_rel_left,def_int_rel_right,iv_sol_names);
01413 } else if (bv_sol.size() > 0) {
01414 BrancherGroup bg;
01415 branch(bg(*this), bv_sol, def_bool_varsel, def_bool_valsel, nullptr,
01416 &varValPrint<BoolVar>);
01417 branchInfo.add(bg,def_bool_rel_left,def_bool_rel_right,bv_sol_names);
01418 }
01419 #ifdef GECODE_HAS_FLOAT_VARS
01420 introduced = 0;
01421 funcdep = 0;
01422 searched = 0;
01423 for (int i=fv.size(); i--;) {
01424 if (fv_searched[i] || (_method != SAT && !_optVarIsInt && _optVar==i)) {
01425 searched++;
01426 } else if (fv_introduced[2*i]) {
01427 if (fv_introduced[2*i+1]) {
01428 funcdep++;
01429 } else {
01430 introduced++;
01431 }
01432 }
01433 }
01434 std::vector<std::string> fv_sol_names(fv.size()-(introduced+funcdep+searched));
01435 FloatVarArgs fv_sol(fv.size()-(introduced+funcdep+searched));
01436 FloatVarArgs fv_tmp(introduced);
01437 std::vector<std::string> fv_tmp_names(introduced);
01438 for (int i=fv.size(), j=0, k=0; i--;) {
01439 if (fv_searched[i] || (_method != SAT && !_optVarIsInt && _optVar==i))
01440 continue;
01441 if (fv_introduced[2*i]) {
01442 if (!fv_introduced[2*i+1]) {
01443 fv_tmp_names[j] = p.floatVarName(i);
01444 fv_tmp[j++] = fv[i];
01445 }
01446 } else {
01447 fv_sol_names[k] = p.floatVarName(i);
01448 fv_sol[k++] = fv[i];
01449 }
01450 }
01451
01452 if (fv_sol.size() > 0) {
01453 BrancherGroup bg;
01454 branch(bg(*this), fv_sol, def_float_varsel, def_float_valsel, nullptr,
01455 &varValPrintF);
01456 branchInfo.add(bg,def_float_rel_left,def_float_rel_right,fv_sol_names);
01457 }
01458 #endif
01459 #ifdef GECODE_HAS_SET_VARS
01460 introduced = 0;
01461 funcdep = 0;
01462 searched = 0;
01463 for (int i=sv.size(); i--;) {
01464 if (sv_searched[i]) {
01465 searched++;
01466 } else if (sv_introduced[2*i]) {
01467 if (sv_introduced[2*i+1]) {
01468 funcdep++;
01469 } else {
01470 introduced++;
01471 }
01472 }
01473 }
01474 std::vector<std::string> sv_sol_names(sv.size()-(introduced+funcdep+searched));
01475 SetVarArgs sv_sol(sv.size()-(introduced+funcdep+searched));
01476 SetVarArgs sv_tmp(introduced);
01477 std::vector<std::string> sv_tmp_names(introduced);
01478 for (int i=sv.size(), j=0, k=0; i--;) {
01479 if (sv_searched[i])
01480 continue;
01481 if (sv_introduced[2*i]) {
01482 if (!sv_introduced[2*i+1]) {
01483 sv_tmp_names[j] = p.setVarName(i);
01484 sv_tmp[j++] = sv[i];
01485 }
01486 } else {
01487 sv_sol_names[k] = p.setVarName(i);
01488 sv_sol[k++] = sv[i];
01489 }
01490 }
01491
01492 if (sv_sol.size() > 0) {
01493 BrancherGroup bg;
01494 branch(bg(*this), sv_sol, def_set_varsel, def_set_valsel, nullptr,
01495 &varValPrint<SetVar>);
01496 branchInfo.add(bg,def_set_rel_left,def_set_rel_right,sv_sol_names);
01497
01498 }
01499 #endif
01500 iv_aux = IntVarArray(*this, iv_tmp);
01501 bv_aux = BoolVarArray(*this, bv_tmp);
01502 int n_aux = iv_aux.size() + bv_aux.size();
01503 #ifdef GECODE_HAS_SET_VARS
01504 sv_aux = SetVarArray(*this, sv_tmp);
01505 n_aux += sv_aux.size();
01506 #endif
01507 #ifdef GECODE_HAS_FLOAT_VARS
01508 fv_aux = FloatVarArray(*this, fv_tmp);
01509 n_aux += fv_aux.size();
01510 #endif
01511
01512 if (n_aux > 0) {
01513 if (_method == SAT) {
01514 AuxVarBrancher::post(*this, def_int_varsel, def_int_valsel,
01515 def_bool_varsel, def_bool_valsel
01516 #ifdef GECODE_HAS_SET_VARS
01517 , def_set_varsel, def_set_valsel
01518 #endif
01519 #ifdef GECODE_HAS_FLOAT_VARS
01520 , def_float_varsel, def_float_valsel
01521 #endif
01522 );
01523 } else {
01524 {
01525 BrancherGroup bg;
01526 branch(bg(*this),iv_aux,def_int_varsel,def_int_valsel, nullptr,
01527 &varValPrint<IntVar>);
01528 branchInfo.add(bg,def_int_rel_left,def_int_rel_right,iv_tmp_names);
01529 }
01530 {
01531 BrancherGroup bg;
01532 branch(bg(*this),bv_aux,def_bool_varsel,def_bool_valsel, nullptr,
01533 &varValPrint<BoolVar>);
01534 branchInfo.add(bg,def_bool_rel_left,def_bool_rel_right,bv_tmp_names);
01535 }
01536 #ifdef GECODE_HAS_SET_VARS
01537 {
01538 BrancherGroup bg;
01539 branch(bg(*this),sv_aux,def_set_varsel,def_set_valsel, nullptr,
01540 &varValPrint<SetVar>);
01541 branchInfo.add(bg,def_set_rel_left,def_set_rel_right,sv_tmp_names);
01542 }
01543 #endif
01544 #ifdef GECODE_HAS_FLOAT_VARS
01545 {
01546 BrancherGroup bg;
01547 branch(bg(*this),fv_aux,def_float_varsel,def_float_valsel, nullptr,
01548 &varValPrintF);
01549 branchInfo.add(bg,def_float_rel_left,def_float_rel_right,fv_tmp_names);
01550 }
01551 #endif
01552
01553 }
01554 }
01555
01556 if (_method == MIN) {
01557 if (_optVarIsInt) {
01558 std::vector<std::string> names(1);
01559 names[0] = p.intVarName(_optVar);
01560 BrancherGroup bg;
01561 branch(bg(*this), iv[_optVar], INT_VAL_MIN(),
01562 &varValPrint<IntVar>);
01563 branchInfo.add(bg,"=","!=",names);
01564 } else {
01565 #ifdef GECODE_HAS_FLOAT_VARS
01566 std::vector<std::string> names(1);
01567 names[0] = p.floatVarName(_optVar);
01568 BrancherGroup bg;
01569 branch(bg(*this), fv[_optVar], FLOAT_VAL_SPLIT_MIN(),
01570 &varValPrintF);
01571 branchInfo.add(bg,"<=",">",names);
01572 #endif
01573 }
01574 } else if (_method == MAX) {
01575 if (_optVarIsInt) {
01576 std::vector<std::string> names(1);
01577 names[0] = p.intVarName(_optVar);
01578 BrancherGroup bg;
01579 branch(bg(*this), iv[_optVar], INT_VAL_MAX(),
01580 &varValPrint<IntVar>);
01581 branchInfo.add(bg,"=","!=",names);
01582 } else {
01583 #ifdef GECODE_HAS_FLOAT_VARS
01584 std::vector<std::string> names(1);
01585 names[0] = p.floatVarName(_optVar);
01586 BrancherGroup bg;
01587 branch(bg(*this), fv[_optVar], FLOAT_VAL_SPLIT_MAX(),
01588 &varValPrintF);
01589 branchInfo.add(bg,"<=",">",names);
01590 #endif
01591 }
01592 }
01593
01594 }
01595
01596 AST::Array*
01597 FlatZincSpace::solveAnnotations(void) const {
01598 return _solveAnnotations;
01599 }
01600
01601 void
01602 FlatZincSpace::solve(AST::Array* ann) {
01603 _method = SAT;
01604 _solveAnnotations = ann;
01605 }
01606
01607 void
01608 FlatZincSpace::minimize(int var, bool isInt, AST::Array* ann) {
01609 _method = MIN;
01610 _optVar = var;
01611 _optVarIsInt = isInt;
01612 _solveAnnotations = ann;
01613 }
01614
01615 void
01616 FlatZincSpace::maximize(int var, bool isInt, AST::Array* ann) {
01617 _method = MAX;
01618 _optVar = var;
01619 _optVarIsInt = isInt;
01620 _solveAnnotations = ann;
01621 }
01622
01623 FlatZincSpace::~FlatZincSpace(void) {
01624 delete _initData;
01625 delete _solveAnnotations;
01626 }
01627
01628 #ifdef GECODE_HAS_GIST
01629
01633 template<class Engine>
01634 class GistEngine {
01635 };
01636
01638 template<typename S>
01639 class GistEngine<DFS<S> > {
01640 public:
01641 static void explore(S* root, const FlatZincOptions& opt,
01642 Gist::Inspector* i, Gist::Comparator* c) {
01643 Gecode::Gist::Options o;
01644 o.c_d = opt.c_d(); o.a_d = opt.a_d();
01645 o.inspect.click(i);
01646 o.inspect.compare(c);
01647 (void) Gecode::Gist::dfs(root, o);
01648 }
01649 };
01650
01652 template<typename S>
01653 class GistEngine<BAB<S> > {
01654 public:
01655 static void explore(S* root, const FlatZincOptions& opt,
01656 Gist::Inspector* i, Gist::Comparator* c) {
01657 Gecode::Gist::Options o;
01658 o.c_d = opt.c_d(); o.a_d = opt.a_d();
01659 o.inspect.click(i);
01660 o.inspect.compare(c);
01661 (void) Gecode::Gist::bab(root, o);
01662 }
01663 };
01664
01666 template<class S>
01667 class FZPrintingInspector
01668 : public Gecode::Gist::TextOutput, public Gecode::Gist::Inspector {
01669 private:
01670 const Printer& p;
01671 public:
01673 FZPrintingInspector(const Printer& p0);
01675 virtual void inspect(const Space& node);
01677 virtual void finalize(void);
01678 };
01679
01680 template<class S>
01681 FZPrintingInspector<S>::FZPrintingInspector(const Printer& p0)
01682 : TextOutput("Gecode/FlatZinc"), p(p0) {}
01683
01684 template<class S>
01685 void
01686 FZPrintingInspector<S>::inspect(const Space& node) {
01687 init();
01688 dynamic_cast<const S&>(node).print(getStream(), p);
01689 getStream() << std::endl;
01690 }
01691
01692 template<class S>
01693 void
01694 FZPrintingInspector<S>::finalize(void) {
01695 Gecode::Gist::TextOutput::finalize();
01696 }
01697
01698 template<class S>
01699 class FZPrintingComparator
01700 : public Gecode::Gist::VarComparator<S> {
01701 private:
01702 const Printer& p;
01703 public:
01705 FZPrintingComparator(const Printer& p0);
01706
01708 virtual void compare(const Space& s0, const Space& s1);
01709 };
01710
01711 template<class S>
01712 FZPrintingComparator<S>::FZPrintingComparator(const Printer& p0)
01713 : Gecode::Gist::VarComparator<S>("Gecode/FlatZinc"), p(p0) {}
01714
01715 template<class S>
01716 void
01717 FZPrintingComparator<S>::compare(const Space& s0, const Space& s1) {
01718 this->init();
01719 try {
01720 dynamic_cast<const S&>(s0).compare(dynamic_cast<const S&>(s1),
01721 this->getStream(), p);
01722 } catch (Exception& e) {
01723 this->getStream() << "Exception: " << e.what();
01724 }
01725 this->getStream() << std::endl;
01726 }
01727
01728 #endif
01729
01730 template<template<class> class Engine>
01731 void
01732 FlatZincSpace::runEngine(std::ostream& out, const Printer& p,
01733 const FlatZincOptions& opt, Support::Timer& t_total) {
01734 if (opt.restart()==RM_NONE) {
01735 runMeta<Engine,Driver::EngineToMeta>(out,p,opt,t_total);
01736 } else {
01737 runMeta<Engine,RBS>(out,p,opt,t_total);
01738 }
01739 }
01740
01741 #ifdef GECODE_HAS_CPPROFILER
01742
01743 class FlatZincGetInfo : public CPProfilerSearchTracer::GetInfo {
01744 public:
01745 const Printer& p;
01746 FlatZincGetInfo(const Printer& printer) : p(printer) {}
01747 virtual std::string
01748 getInfo(const Space& space) const {
01749 std::stringstream ss;
01750 if (const FlatZincSpace* fz_space = dynamic_cast<const FlatZincSpace*>(&space)) {
01751 ss << "{\n\t\"domains\": \"";
01752 ss << fz_space->getDomains(p);
01753 ss << "\"\n}";
01754 }
01755 return ss.str();
01756 }
01757 ~FlatZincGetInfo(void) {};
01758 };
01759
01760 void printIntVar(std::ostream& os, const std::string name, const Int::IntView& x) {
01761 os << "var ";
01762 if (x.assigned()) {
01763 os << "int: " << name << " = " << x.val() << ";";
01764 } else if (x.range()) {
01765 os << x.min() << ".." << x.max() << ": " << name << ";";
01766 } else {
01767 os << "array_union([";
01768 Gecode::Int::ViewRanges<Int::IntView> r(x);
01769 while (true) {
01770 os << r.min() << ".." << r.max();
01771 ++r;
01772 if (!r()) break;
01773 os << ',';
01774 }
01775 os << "]): " << name << ";";
01776 }
01777 os << "\n";
01778 }
01779 void printBoolVar(std::ostream& os, const std::string name, const BoolVar& b) {
01780 os << "var bool: " << name;
01781 if(b.assigned())
01782 os << " = " << (b.val() ? "true" : "false");
01783 os << ";\n";
01784 }
01785 #ifdef GECODE_HAS_FLOAT_VARS
01786 void printFloatVar(std::ostream& os, const std::string name, const Float::FloatView& f) {
01787 os << "var ";
01788 if(f.assigned())
01789 os << "float: " << name << " = " << f.med() << ";";
01790 else
01791 os << f.min() << ".." << f.max() << ": " << name << ";";
01792 os << "\n";
01793 }
01794 #endif
01795 std::string FlatZincSpace::getDomains(const Printer& p) const {
01796 std::ostringstream oss;
01797
01798 for (int i = 0; i < iv.size(); i++)
01799 printIntVar(oss, p.intVarName(i), iv[i]);
01800
01801 for (int i = 0; i < bv.size(); i++)
01802 printBoolVar(oss, p.boolVarName(i), bv[i]);
01803
01804 #ifdef GECODE_HAS_FLOAT_VARS
01805 for (int i = 0; i < fv.size(); i++)
01806 printFloatVar(oss, p.floatVarName(i), fv[i]);
01807 #endif
01808 #ifdef GECODE_HAS_SET_VARS
01809 for (int i = 0; i < sv.size(); i++)
01810 oss << "var " << sv[i] << ": " << p.setVarName(i) << ";" << std::endl;
01811 #endif
01812
01813 return oss.str();
01814 }
01815
01816 #endif
01817
01818 template<template<class> class Engine,
01819 template<class,template<class> class> class Meta>
01820 void
01821 FlatZincSpace::runMeta(std::ostream& out, const Printer& p,
01822 const FlatZincOptions& opt, Support::Timer& t_total) {
01823 #ifdef GECODE_HAS_GIST
01824 if (opt.mode() == SM_GIST) {
01825 FZPrintingInspector<FlatZincSpace> pi(p);
01826 FZPrintingComparator<FlatZincSpace> pc(p);
01827 (void) GistEngine<Engine<FlatZincSpace> >::explore(this,opt,&pi,&pc);
01828 return;
01829 }
01830 #endif
01831 StatusStatistics sstat;
01832 unsigned int n_p = 0;
01833 Support::Timer t_solve;
01834 t_solve.start();
01835 if (status(sstat) != SS_FAILED) {
01836 n_p = PropagatorGroup::all.size(*this);
01837 }
01838 Search::Options o;
01839 o.stop = Driver::CombinedStop::create(opt.node(), opt.fail(), opt.time(),
01840 true);
01841 o.c_d = opt.c_d();
01842 o.a_d = opt.a_d();
01843
01844 #ifdef GECODE_HAS_CPPROFILER
01845
01846 if (opt.mode() == SM_CPPROFILER) {
01847 FlatZincGetInfo* getInfo = nullptr;
01848 if (opt.profiler_info())
01849 getInfo = new FlatZincGetInfo(p);
01850 o.tracer = new CPProfilerSearchTracer(opt.profiler_id(),
01851 opt.name(), opt.profiler_port(),
01852 getInfo);
01853 }
01854
01855 #endif
01856
01857 #ifdef GECODE_HAS_FLOAT_VARS
01858 step = opt.step();
01859 #endif
01860 o.threads = opt.threads();
01861 o.nogoods_limit = opt.nogoods() ? opt.nogoods_limit() : 0;
01862 o.cutoff = new Search::CutoffAppend(new Search::CutoffConstant(0), 1, Driver::createCutoff(opt));
01863 if (opt.interrupt())
01864 Driver::CombinedStop::installCtrlHandler(true);
01865 {
01866 Meta<FlatZincSpace,Engine> se(this,o);
01867 int noOfSolutions = opt.solutions();
01868 if (noOfSolutions == -1) {
01869 noOfSolutions = (_method == SAT) ? 1 : 0;
01870 }
01871 bool printAll = _method == SAT || opt.allSolutions() || noOfSolutions != 0;
01872 int findSol = noOfSolutions;
01873 FlatZincSpace* sol = NULL;
01874 while (FlatZincSpace* next_sol = se.next()) {
01875 delete sol;
01876 sol = next_sol;
01877 if (printAll) {
01878 sol->print(out, p);
01879 out << "----------" << std::endl;
01880 }
01881 if (--findSol==0)
01882 goto stopped;
01883 }
01884 if (sol && !printAll) {
01885 sol->print(out, p);
01886 out << "----------" << std::endl;
01887 }
01888 if (!se.stopped()) {
01889 if (sol) {
01890 out << "==========" << std::endl;
01891 } else {
01892 out << "=====UNSATISFIABLE=====" << std::endl;
01893 }
01894 } else if (!sol) {
01895 out << "=====UNKNOWN=====" << std::endl;
01896 }
01897 delete sol;
01898 stopped:
01899 if (opt.interrupt())
01900 Driver::CombinedStop::installCtrlHandler(false);
01901 if (opt.mode() == SM_STAT) {
01902 Gecode::Search::Statistics stat = se.statistics();
01903 double totalTime = (t_total.stop() / 1000.0);
01904 double solveTime = (t_solve.stop() / 1000.0);
01905 double initTime = totalTime - solveTime;
01906 out << std::endl
01907 << "%%%mzn-stat: initTime=" << initTime
01908 << std::endl;
01909 out << "%%%mzn-stat: solveTime=" << solveTime
01910 << std::endl;
01911 out << "%%%mzn-stat: solutions="
01912 << std::abs(noOfSolutions - findSol) << std::endl
01913 << "%%%mzn-stat: variables="
01914 << (intVarCount + boolVarCount + setVarCount) << std::endl
01915 << "%%%mzn-stat: propagators=" << n_p << std::endl
01916 << "%%%mzn-stat: propagations=" << sstat.propagate+stat.propagate << std::endl
01917 << "%%%mzn-stat: nodes=" << stat.node << std::endl
01918 << "%%%mzn-stat: failures=" << stat.fail << std::endl
01919 << "%%%mzn-stat: restarts=" << stat.restart << std::endl
01920 << "%%%mzn-stat: peakDepth=" << stat.depth << std::endl
01921 << "%%%mzn-stat-end" << std::endl
01922 << std::endl;
01923 }
01924 }
01925 delete o.stop;
01926 delete o.tracer;
01927 }
01928
01929 #ifdef GECODE_HAS_QT
01930 void
01931 FlatZincSpace::branchWithPlugin(AST::Node* ann) {
01932 if (AST::Call* c = dynamic_cast<AST::Call*>(ann)) {
01933 QString pluginName(c->id.c_str());
01934 if (QLibrary::isLibrary(pluginName+".dll")) {
01935 pluginName += ".dll";
01936 } else if (QLibrary::isLibrary(pluginName+".dylib")) {
01937 pluginName = "lib" + pluginName + ".dylib";
01938 } else if (QLibrary::isLibrary(pluginName+".so")) {
01939
01940 pluginName = "lib" + pluginName + ".so";
01941 }
01942 QPluginLoader pl(pluginName);
01943 QObject* plugin_o = pl.instance();
01944 if (!plugin_o) {
01945 throw FlatZinc::Error("FlatZinc",
01946 "Error loading plugin "+pluginName.toStdString()+
01947 ": "+pl.errorString().toStdString());
01948 }
01949 BranchPlugin* pb = qobject_cast<BranchPlugin*>(plugin_o);
01950 if (!pb) {
01951 throw FlatZinc::Error("FlatZinc",
01952 "Error loading plugin "+pluginName.toStdString()+
01953 ": does not contain valid PluginBrancher");
01954 }
01955 pb->branch(*this, c);
01956 }
01957 }
01958 #else
01959 void
01960 FlatZincSpace::branchWithPlugin(AST::Node*) {
01961 throw FlatZinc::Error("FlatZinc",
01962 "Branching with plugins not supported (requires Qt support)");
01963 }
01964 #endif
01965
01966 void
01967 FlatZincSpace::run(std::ostream& out, const Printer& p,
01968 const FlatZincOptions& opt, Support::Timer& t_total) {
01969 switch (_method) {
01970 case MIN:
01971 case MAX:
01972 runEngine<BAB>(out,p,opt,t_total);
01973 break;
01974 case SAT:
01975 runEngine<DFS>(out,p,opt,t_total);
01976 break;
01977 }
01978 }
01979
01980 void
01981 FlatZincSpace::constrain(const Space& s) {
01982 if (_optVarIsInt) {
01983 if (_method == MIN)
01984 rel(*this, iv[_optVar], IRT_LE,
01985 static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
01986 else if (_method == MAX)
01987 rel(*this, iv[_optVar], IRT_GR,
01988 static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
01989 } else {
01990 #ifdef GECODE_HAS_FLOAT_VARS
01991 if (_method == MIN)
01992 rel(*this, fv[_optVar], FRT_LE,
01993 static_cast<const FlatZincSpace*>(&s)->fv[_optVar].val()-step);
01994 else if (_method == MAX)
01995 rel(*this, fv[_optVar], FRT_GR,
01996 static_cast<const FlatZincSpace*>(&s)->fv[_optVar].val()+step);
01997 #endif
01998 }
01999 }
02000
02001 bool
02002 FlatZincSpace::slave(const MetaInfo& mi) {
02003 if ((mi.type() == MetaInfo::RESTART) && (mi.restart() != 0) &&
02004 (_lns > 0) && (mi.last()==NULL) && (_lnsInitialSolution.size()>0)) {
02005 for (unsigned int i=iv_lns.size(); i--;) {
02006 if (_random(99) <= _lns) {
02007 rel(*this, iv_lns[i], IRT_EQ, _lnsInitialSolution[i]);
02008 }
02009 }
02010 return false;
02011 } else if ((mi.type() == MetaInfo::RESTART) && (mi.restart() != 0) &&
02012 (_lns > 0) && mi.last()) {
02013 const FlatZincSpace& last =
02014 static_cast<const FlatZincSpace&>(*mi.last());
02015 for (unsigned int i=iv_lns.size(); i--;) {
02016 if (_random(99) <= _lns) {
02017 rel(*this, iv_lns[i], IRT_EQ, last.iv_lns[i]);
02018 }
02019 }
02020 return false;
02021 }
02022 return true;
02023 }
02024
02025 Space*
02026 FlatZincSpace::copy(void) {
02027 return new FlatZincSpace(*this);
02028 }
02029
02030 FlatZincSpace::Meth
02031 FlatZincSpace::method(void) const {
02032 return _method;
02033 }
02034
02035 int
02036 FlatZincSpace::optVar(void) const {
02037 return _optVar;
02038 }
02039
02040 bool
02041 FlatZincSpace::optVarIsInt(void) const {
02042 return _optVarIsInt;
02043 }
02044
02045 void
02046 FlatZincSpace::print(std::ostream& out, const Printer& p) const {
02047 p.print(out, iv, bv
02048 #ifdef GECODE_HAS_SET_VARS
02049 , sv
02050 #endif
02051 #ifdef GECODE_HAS_FLOAT_VARS
02052 , fv
02053 #endif
02054 );
02055 }
02056
02057 void
02058 FlatZincSpace::compare(const Space& s, std::ostream& out) const {
02059 (void) s; (void) out;
02060 #ifdef GECODE_HAS_GIST
02061 const FlatZincSpace& fs = dynamic_cast<const FlatZincSpace&>(s);
02062 for (int i = 0; i < iv.size(); ++i) {
02063 std::stringstream ss;
02064 ss << "iv[" << i << "]";
02065 std::string result(Gecode::Gist::Comparator::compare(ss.str(), iv[i],
02066 fs.iv[i]));
02067 if (result.length() > 0) out << result << std::endl;
02068 }
02069 for (int i = 0; i < bv.size(); ++i) {
02070 std::stringstream ss;
02071 ss << "bv[" << i << "]";
02072 std::string result(Gecode::Gist::Comparator::compare(ss.str(), bv[i],
02073 fs.bv[i]));
02074 if (result.length() > 0) out << result << std::endl;
02075 }
02076 #ifdef GECODE_HAS_SET_VARS
02077 for (int i = 0; i < sv.size(); ++i) {
02078 std::stringstream ss;
02079 ss << "sv[" << i << "]";
02080 std::string result(Gecode::Gist::Comparator::compare(ss.str(), sv[i],
02081 fs.sv[i]));
02082 if (result.length() > 0) out << result << std::endl;
02083 }
02084 #endif
02085 #ifdef GECODE_HAS_FLOAT_VARS
02086 for (int i = 0; i < fv.size(); ++i) {
02087 std::stringstream ss;
02088 ss << "fv[" << i << "]";
02089 std::string result(Gecode::Gist::Comparator::compare(ss.str(), fv[i],
02090 fs.fv[i]));
02091 if (result.length() > 0) out << result << std::endl;
02092 }
02093 #endif
02094 #endif
02095 }
02096
02097 void
02098 FlatZincSpace::compare(const FlatZincSpace& s, std::ostream& out,
02099 const Printer& p) const {
02100 p.printDiff(out, iv, s.iv, bv, s.bv
02101 #ifdef GECODE_HAS_SET_VARS
02102 , sv, s.sv
02103 #endif
02104 #ifdef GECODE_HAS_FLOAT_VARS
02105 , fv, s.fv
02106 #endif
02107 );
02108 }
02109
02110 void
02111 FlatZincSpace::shrinkArrays(Printer& p) {
02112 p.shrinkArrays(*this, _optVar, _optVarIsInt, iv, bv
02113 #ifdef GECODE_HAS_SET_VARS
02114 , sv
02115 #endif
02116 #ifdef GECODE_HAS_FLOAT_VARS
02117 , fv
02118 #endif
02119 );
02120 }
02121
02122 IntArgs
02123 FlatZincSpace::arg2intargs(AST::Node* arg, int offset) {
02124 AST::Array* a = arg->getArray();
02125 IntArgs ia(a->a.size()+offset);
02126 for (int i=offset; i--;)
02127 ia[i] = 0;
02128 for (int i=a->a.size(); i--;)
02129 ia[i+offset] = a->a[i]->getInt();
02130 return ia;
02131 }
02132 TupleSet
02133 FlatZincSpace::arg2tupleset(const IntArgs& a, int noOfVars) {
02134 int noOfTuples = a.size() == 0 ? 0 : (a.size()/noOfVars);
02135
02136
02137 TupleSet ts(noOfVars);
02138 for (int i=0; i<noOfTuples; i++) {
02139 IntArgs t(noOfVars);
02140 for (int j=0; j<noOfVars; j++) {
02141 t[j] = a[i*noOfVars+j];
02142 }
02143 ts.add(t);
02144 }
02145 ts.finalize();
02146
02147 if (_initData) {
02148 FlatZincSpaceInitData::TupleSetSet::iterator it = _initData->tupleSetSet.find(ts);
02149 if (it != _initData->tupleSetSet.end()) {
02150 return *it;
02151 }
02152 _initData->tupleSetSet.insert(ts);
02153 }
02154
02155
02156 return ts;
02157 }
02158 IntSharedArray
02159 FlatZincSpace::arg2intsharedarray(AST::Node* arg, int offset) {
02160 IntArgs ia(arg2intargs(arg,offset));
02161 SharedArray<int> sia(ia);
02162 if (_initData) {
02163 FlatZincSpaceInitData::IntSharedArraySet::iterator it = _initData->intSharedArraySet.find(sia);
02164 if (it != _initData->intSharedArraySet.end()) {
02165 return *it;
02166 }
02167 _initData->intSharedArraySet.insert(sia);
02168 }
02169
02170 return sia;
02171 }
02172 IntArgs
02173 FlatZincSpace::arg2boolargs(AST::Node* arg, int offset) {
02174 AST::Array* a = arg->getArray();
02175 IntArgs ia(a->a.size()+offset);
02176 for (int i=offset; i--;)
02177 ia[i] = 0;
02178 for (int i=a->a.size(); i--;)
02179 ia[i+offset] = a->a[i]->getBool();
02180 return ia;
02181 }
02182 IntSharedArray
02183 FlatZincSpace::arg2boolsharedarray(AST::Node* arg, int offset) {
02184 IntArgs ia(arg2boolargs(arg,offset));
02185 SharedArray<int> sia(ia);
02186 if (_initData) {
02187 FlatZincSpaceInitData::IntSharedArraySet::iterator it = _initData->intSharedArraySet.find(sia);
02188 if (it != _initData->intSharedArraySet.end()) {
02189 return *it;
02190 }
02191 _initData->intSharedArraySet.insert(sia);
02192 }
02193
02194 return sia;
02195 }
02196 IntSet
02197 FlatZincSpace::arg2intset(AST::Node* n) {
02198 AST::SetLit* sl = n->getSet();
02199 IntSet d;
02200 if (sl->interval) {
02201 d = IntSet(sl->min, sl->max);
02202 } else {
02203 Region re;
02204 int* is = re.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
02205 for (int i=sl->s.size(); i--; )
02206 is[i] = sl->s[i];
02207 d = IntSet(is, sl->s.size());
02208 }
02209 return d;
02210 }
02211 IntSetArgs
02212 FlatZincSpace::arg2intsetargs(AST::Node* arg, int offset) {
02213 AST::Array* a = arg->getArray();
02214 if (a->a.size() == 0) {
02215 IntSetArgs emptyIa(0);
02216 return emptyIa;
02217 }
02218 IntSetArgs ia(a->a.size()+offset);
02219 for (int i=offset; i--;)
02220 ia[i] = IntSet::empty;
02221 for (int i=a->a.size(); i--;) {
02222 ia[i+offset] = arg2intset(a->a[i]);
02223 }
02224 return ia;
02225 }
02226 IntVarArgs
02227 FlatZincSpace::arg2intvarargs(AST::Node* arg, int offset) {
02228 AST::Array* a = arg->getArray();
02229 if (a->a.size() == 0) {
02230 IntVarArgs emptyIa(0);
02231 return emptyIa;
02232 }
02233 IntVarArgs ia(a->a.size()+offset);
02234 for (int i=offset; i--;)
02235 ia[i] = IntVar(*this, 0, 0);
02236 for (int i=a->a.size(); i--;) {
02237 if (a->a[i]->isIntVar()) {
02238 ia[i+offset] = iv[a->a[i]->getIntVar()];
02239 } else {
02240 int value = a->a[i]->getInt();
02241 IntVar iv(*this, value, value);
02242 ia[i+offset] = iv;
02243 }
02244 }
02245 return ia;
02246 }
02247 BoolVarArgs
02248 FlatZincSpace::arg2boolvarargs(AST::Node* arg, int offset, int siv) {
02249 AST::Array* a = arg->getArray();
02250 if (a->a.size() == 0) {
02251 BoolVarArgs emptyIa(0);
02252 return emptyIa;
02253 }
02254 BoolVarArgs ia(a->a.size()+offset-(siv==-1?0:1));
02255 for (int i=offset; i--;)
02256 ia[i] = BoolVar(*this, 0, 0);
02257 for (int i=0; i<static_cast<int>(a->a.size()); i++) {
02258 if (i==siv)
02259 continue;
02260 if (a->a[i]->isBool()) {
02261 bool value = a->a[i]->getBool();
02262 BoolVar iv(*this, value, value);
02263 ia[offset++] = iv;
02264 } else if (a->a[i]->isIntVar() &&
02265 aliasBool2Int(a->a[i]->getIntVar()) != -1) {
02266 ia[offset++] = bv[aliasBool2Int(a->a[i]->getIntVar())];
02267 } else {
02268 ia[offset++] = bv[a->a[i]->getBoolVar()];
02269 }
02270 }
02271 return ia;
02272 }
02273 BoolVar
02274 FlatZincSpace::arg2BoolVar(AST::Node* n) {
02275 BoolVar x0;
02276 if (n->isBool()) {
02277 x0 = BoolVar(*this, n->getBool(), n->getBool());
02278 }
02279 else {
02280 x0 = bv[n->getBoolVar()];
02281 }
02282 return x0;
02283 }
02284 IntVar
02285 FlatZincSpace::arg2IntVar(AST::Node* n) {
02286 IntVar x0;
02287 if (n->isIntVar()) {
02288 x0 = iv[n->getIntVar()];
02289 } else {
02290 x0 = IntVar(*this, n->getInt(), n->getInt());
02291 }
02292 return x0;
02293 }
02294 bool
02295 FlatZincSpace::isBoolArray(AST::Node* b, int& singleInt) {
02296 AST::Array* a = b->getArray();
02297 singleInt = -1;
02298 if (a->a.size() == 0)
02299 return true;
02300 for (int i=a->a.size(); i--;) {
02301 if (a->a[i]->isBoolVar() || a->a[i]->isBool()) {
02302 } else if (a->a[i]->isIntVar()) {
02303 if (aliasBool2Int(a->a[i]->getIntVar()) == -1) {
02304 if (singleInt != -1) {
02305 return false;
02306 }
02307 singleInt = i;
02308 }
02309 } else {
02310 return false;
02311 }
02312 }
02313 return singleInt==-1 || a->a.size() > 1;
02314 }
02315 #ifdef GECODE_HAS_SET_VARS
02316 SetVar
02317 FlatZincSpace::arg2SetVar(AST::Node* n) {
02318 SetVar x0;
02319 if (!n->isSetVar()) {
02320 IntSet d = arg2intset(n);
02321 x0 = SetVar(*this, d, d);
02322 } else {
02323 x0 = sv[n->getSetVar()];
02324 }
02325 return x0;
02326 }
02327 SetVarArgs
02328 FlatZincSpace::arg2setvarargs(AST::Node* arg, int offset, int doffset,
02329 const IntSet& od) {
02330 AST::Array* a = arg->getArray();
02331 SetVarArgs ia(a->a.size()+offset);
02332 for (int i=offset; i--;) {
02333 IntSet d = i<doffset ? od : IntSet::empty;
02334 ia[i] = SetVar(*this, d, d);
02335 }
02336 for (int i=a->a.size(); i--;) {
02337 ia[i+offset] = arg2SetVar(a->a[i]);
02338 }
02339 return ia;
02340 }
02341 #endif
02342 #ifdef GECODE_HAS_FLOAT_VARS
02343 FloatValArgs
02344 FlatZincSpace::arg2floatargs(AST::Node* arg, int offset) {
02345 AST::Array* a = arg->getArray();
02346 FloatValArgs fa(a->a.size()+offset);
02347 for (int i=offset; i--;)
02348 fa[i] = 0.0;
02349 for (int i=a->a.size(); i--;)
02350 fa[i+offset] = a->a[i]->getFloat();
02351 return fa;
02352 }
02353 FloatVarArgs
02354 FlatZincSpace::arg2floatvarargs(AST::Node* arg, int offset) {
02355 AST::Array* a = arg->getArray();
02356 if (a->a.size() == 0) {
02357 FloatVarArgs emptyFa(0);
02358 return emptyFa;
02359 }
02360 FloatVarArgs fa(a->a.size()+offset);
02361 for (int i=offset; i--;)
02362 fa[i] = FloatVar(*this, 0.0, 0.0);
02363 for (int i=a->a.size(); i--;) {
02364 if (a->a[i]->isFloatVar()) {
02365 fa[i+offset] = fv[a->a[i]->getFloatVar()];
02366 } else {
02367 double value = a->a[i]->getFloat();
02368 FloatVar fv(*this, value, value);
02369 fa[i+offset] = fv;
02370 }
02371 }
02372 return fa;
02373 }
02374 FloatVar
02375 FlatZincSpace::arg2FloatVar(AST::Node* n) {
02376 FloatVar x0;
02377 if (n->isFloatVar()) {
02378 x0 = fv[n->getFloatVar()];
02379 } else {
02380 x0 = FloatVar(*this, n->getFloat(), n->getFloat());
02381 }
02382 return x0;
02383 }
02384 #endif
02385 IntPropLevel
02386 FlatZincSpace::ann2ipl(AST::Node* ann) {
02387 if (ann) {
02388 if (ann->hasAtom("val"))
02389 return IPL_VAL;
02390 if (ann->hasAtom("domain"))
02391 return IPL_DOM;
02392 if (ann->hasAtom("bounds") ||
02393 ann->hasAtom("boundsR") ||
02394 ann->hasAtom("boundsD") ||
02395 ann->hasAtom("boundsZ"))
02396 return IPL_BND;
02397 }
02398 return IPL_DEF;
02399 }
02400
02401 DFA
02402 FlatZincSpace::getSharedDFA(DFA& a) {
02403 if (_initData) {
02404 FlatZincSpaceInitData::DFASet::iterator it = _initData->dfaSet.find(a);
02405 if (it != _initData->dfaSet.end()) {
02406 return *it;
02407 }
02408 _initData->dfaSet.insert(a);
02409 }
02410 return a;
02411 }
02412
02413 void
02414 Printer::init(AST::Array* output) {
02415 _output = output;
02416 }
02417
02418 void
02419 Printer::printElem(std::ostream& out,
02420 AST::Node* ai,
02421 const Gecode::IntVarArray& iv,
02422 const Gecode::BoolVarArray& bv
02423 #ifdef GECODE_HAS_SET_VARS
02424 , const Gecode::SetVarArray& sv
02425 #endif
02426 #ifdef GECODE_HAS_FLOAT_VARS
02427 ,
02428 const Gecode::FloatVarArray& fv
02429 #endif
02430 ) const {
02431 int k;
02432 if (ai->isInt(k)) {
02433 out << k;
02434 } else if (ai->isIntVar()) {
02435 out << iv[ai->getIntVar()];
02436 } else if (ai->isBoolVar()) {
02437 if (bv[ai->getBoolVar()].min() == 1) {
02438 out << "true";
02439 } else if (bv[ai->getBoolVar()].max() == 0) {
02440 out << "false";
02441 } else {
02442 out << "false..true";
02443 }
02444 #ifdef GECODE_HAS_SET_VARS
02445 } else if (ai->isSetVar()) {
02446 if (!sv[ai->getSetVar()].assigned()) {
02447 out << sv[ai->getSetVar()];
02448 return;
02449 }
02450 SetVarGlbRanges svr(sv[ai->getSetVar()]);
02451 if (!svr()) {
02452 out << "{}";
02453 return;
02454 }
02455 int min = svr.min();
02456 int max = svr.max();
02457 ++svr;
02458 if (svr()) {
02459 SetVarGlbValues svv(sv[ai->getSetVar()]);
02460 int i = svv.val();
02461 out << "{" << i;
02462 ++svv;
02463 for (; svv(); ++svv)
02464 out << ", " << svv.val();
02465 out << "}";
02466 } else {
02467 out << min << ".." << max;
02468 }
02469 #endif
02470 #ifdef GECODE_HAS_FLOAT_VARS
02471 } else if (ai->isFloatVar()) {
02472 if (fv[ai->getFloatVar()].assigned()) {
02473 FloatVal vv = fv[ai->getFloatVar()].val();
02474 FloatNum v;
02475 if (vv.singleton())
02476 v = vv.min();
02477 else if (vv < 0.0)
02478 v = vv.max();
02479 else
02480 v = vv.min();
02481 std::ostringstream oss;
02482
02483 oss << std::setprecision(std::numeric_limits<double>::digits10);
02484 oss << v;
02485 if (oss.str().find(".") == std::string::npos)
02486 oss << ".0";
02487 out << oss.str();
02488 } else {
02489 out << fv[ai->getFloatVar()];
02490 }
02491 #endif
02492 } else if (ai->isBool()) {
02493 out << (ai->getBool() ? "true" : "false");
02494 } else if (ai->isSet()) {
02495 AST::SetLit* s = ai->getSet();
02496 if (s->interval) {
02497 out << s->min << ".." << s->max;
02498 } else {
02499 out << "{";
02500 for (unsigned int i=0; i<s->s.size(); i++) {
02501 out << s->s[i] << (i < s->s.size()-1 ? ", " : "}");
02502 }
02503 }
02504 } else if (ai->isString()) {
02505 std::string s = ai->getString();
02506 for (unsigned int i=0; i<s.size(); i++) {
02507 if (s[i] == '\\' && i<s.size()-1) {
02508 switch (s[i+1]) {
02509 case 'n': out << "\n"; break;
02510 case '\\': out << "\\"; break;
02511 case 't': out << "\t"; break;
02512 default: out << "\\" << s[i+1];
02513 }
02514 i++;
02515 } else {
02516 out << s[i];
02517 }
02518 }
02519 }
02520 }
02521
02522 void
02523 Printer::printElemDiff(std::ostream& out,
02524 AST::Node* ai,
02525 const Gecode::IntVarArray& iv1,
02526 const Gecode::IntVarArray& iv2,
02527 const Gecode::BoolVarArray& bv1,
02528 const Gecode::BoolVarArray& bv2
02529 #ifdef GECODE_HAS_SET_VARS
02530 , const Gecode::SetVarArray& sv1,
02531 const Gecode::SetVarArray& sv2
02532 #endif
02533 #ifdef GECODE_HAS_FLOAT_VARS
02534 , const Gecode::FloatVarArray& fv1,
02535 const Gecode::FloatVarArray& fv2
02536 #endif
02537 ) const {
02538 #ifdef GECODE_HAS_GIST
02539 using namespace Gecode::Gist;
02540 int k;
02541 if (ai->isInt(k)) {
02542 out << k;
02543 } else if (ai->isIntVar()) {
02544 std::string res(Comparator::compare("",iv1[ai->getIntVar()],
02545 iv2[ai->getIntVar()]));
02546 if (res.length() > 0) {
02547 res.erase(0, 1);
02548 out << res;
02549 } else {
02550 out << iv1[ai->getIntVar()];
02551 }
02552 } else if (ai->isBoolVar()) {
02553 std::string res(Comparator::compare("",bv1[ai->getBoolVar()],
02554 bv2[ai->getBoolVar()]));
02555 if (res.length() > 0) {
02556 res.erase(0, 1);
02557 out << res;
02558 } else {
02559 out << bv1[ai->getBoolVar()];
02560 }
02561 #ifdef GECODE_HAS_SET_VARS
02562 } else if (ai->isSetVar()) {
02563 std::string res(Comparator::compare("",sv1[ai->getSetVar()],
02564 sv2[ai->getSetVar()]));
02565 if (res.length() > 0) {
02566 res.erase(0, 1);
02567 out << res;
02568 } else {
02569 out << sv1[ai->getSetVar()];
02570 }
02571 #endif
02572 #ifdef GECODE_HAS_FLOAT_VARS
02573 } else if (ai->isFloatVar()) {
02574 std::string res(Comparator::compare("",fv1[ai->getFloatVar()],
02575 fv2[ai->getFloatVar()]));
02576 if (res.length() > 0) {
02577 res.erase(0, 1);
02578 out << res;
02579 } else {
02580 out << fv1[ai->getFloatVar()];
02581 }
02582 #endif
02583 } else if (ai->isBool()) {
02584 out << (ai->getBool() ? "true" : "false");
02585 } else if (ai->isSet()) {
02586 AST::SetLit* s = ai->getSet();
02587 if (s->interval) {
02588 out << s->min << ".." << s->max;
02589 } else {
02590 out << "{";
02591 for (unsigned int i=0; i<s->s.size(); i++) {
02592 out << s->s[i] << (i < s->s.size()-1 ? ", " : "}");
02593 }
02594 }
02595 } else if (ai->isString()) {
02596 std::string s = ai->getString();
02597 for (unsigned int i=0; i<s.size(); i++) {
02598 if (s[i] == '\\' && i<s.size()-1) {
02599 switch (s[i+1]) {
02600 case 'n': out << "\n"; break;
02601 case '\\': out << "\\"; break;
02602 case 't': out << "\t"; break;
02603 default: out << "\\" << s[i+1];
02604 }
02605 i++;
02606 } else {
02607 out << s[i];
02608 }
02609 }
02610 }
02611 #else
02612 (void) out;
02613 (void) ai;
02614 (void) iv1;
02615 (void) iv2;
02616 (void) bv1;
02617 (void) bv2;
02618 #ifdef GECODE_HAS_SET_VARS
02619 (void) sv1;
02620 (void) sv2;
02621 #endif
02622 #ifdef GECODE_HAS_FLOAT_VARS
02623 (void) fv1;
02624 (void) fv2;
02625 #endif
02626
02627 #endif
02628 }
02629
02630 void
02631 Printer::print(std::ostream& out,
02632 const Gecode::IntVarArray& iv,
02633 const Gecode::BoolVarArray& bv
02634 #ifdef GECODE_HAS_SET_VARS
02635 ,
02636 const Gecode::SetVarArray& sv
02637 #endif
02638 #ifdef GECODE_HAS_FLOAT_VARS
02639 ,
02640 const Gecode::FloatVarArray& fv
02641 #endif
02642 ) const {
02643 if (_output == NULL)
02644 return;
02645 for (unsigned int i=0; i< _output->a.size(); i++) {
02646 AST::Node* ai = _output->a[i];
02647 if (ai->isArray()) {
02648 AST::Array* aia = ai->getArray();
02649 int size = aia->a.size();
02650 out << "[";
02651 for (int j=0; j<size; j++) {
02652 printElem(out,aia->a[j],iv,bv
02653 #ifdef GECODE_HAS_SET_VARS
02654 ,sv
02655 #endif
02656 #ifdef GECODE_HAS_FLOAT_VARS
02657 ,fv
02658 #endif
02659 );
02660 if (j<size-1)
02661 out << ", ";
02662 }
02663 out << "]";
02664 } else {
02665 printElem(out,ai,iv,bv
02666 #ifdef GECODE_HAS_SET_VARS
02667 ,sv
02668 #endif
02669 #ifdef GECODE_HAS_FLOAT_VARS
02670 ,fv
02671 #endif
02672 );
02673 }
02674 }
02675 }
02676
02677 void
02678 Printer::printDiff(std::ostream& out,
02679 const Gecode::IntVarArray& iv1,
02680 const Gecode::IntVarArray& iv2,
02681 const Gecode::BoolVarArray& bv1,
02682 const Gecode::BoolVarArray& bv2
02683 #ifdef GECODE_HAS_SET_VARS
02684 ,
02685 const Gecode::SetVarArray& sv1,
02686 const Gecode::SetVarArray& sv2
02687 #endif
02688 #ifdef GECODE_HAS_FLOAT_VARS
02689 ,
02690 const Gecode::FloatVarArray& fv1,
02691 const Gecode::FloatVarArray& fv2
02692 #endif
02693 ) const {
02694 if (_output == NULL)
02695 return;
02696 for (unsigned int i=0; i< _output->a.size(); i++) {
02697 AST::Node* ai = _output->a[i];
02698 if (ai->isArray()) {
02699 AST::Array* aia = ai->getArray();
02700 int size = aia->a.size();
02701 out << "[";
02702 for (int j=0; j<size; j++) {
02703 printElemDiff(out,aia->a[j],iv1,iv2,bv1,bv2
02704 #ifdef GECODE_HAS_SET_VARS
02705 ,sv1,sv2
02706 #endif
02707 #ifdef GECODE_HAS_FLOAT_VARS
02708 ,fv1,fv2
02709 #endif
02710 );
02711 if (j<size-1)
02712 out << ", ";
02713 }
02714 out << "]";
02715 } else {
02716 printElemDiff(out,ai,iv1,iv2,bv1,bv2
02717 #ifdef GECODE_HAS_SET_VARS
02718 ,sv1,sv2
02719 #endif
02720 #ifdef GECODE_HAS_FLOAT_VARS
02721 ,fv1,fv2
02722 #endif
02723 );
02724 }
02725 }
02726 }
02727
02728 void
02729 Printer::addIntVarName(const std::string& n) {
02730 iv_names.push_back(n);
02731 }
02732 void
02733 Printer::addBoolVarName(const std::string& n) {
02734 bv_names.push_back(n);
02735 }
02736 #ifdef GECODE_HAS_FLOAT_VARS
02737 void
02738 Printer::addFloatVarName(const std::string& n) {
02739 fv_names.push_back(n);
02740 }
02741 #endif
02742 #ifdef GECODE_HAS_SET_VARS
02743 void
02744 Printer::addSetVarName(const std::string& n) {
02745 sv_names.push_back(n);
02746 }
02747 #endif
02748
02749 void
02750 Printer::shrinkElement(AST::Node* node,
02751 std::map<int,int>& iv, std::map<int,int>& bv,
02752 std::map<int,int>& sv, std::map<int,int>& fv) {
02753 if (node->isIntVar()) {
02754 AST::IntVar* x = static_cast<AST::IntVar*>(node);
02755 if (iv.find(x->i) == iv.end()) {
02756 int newi = iv.size();
02757 iv[x->i] = newi;
02758 }
02759 x->i = iv[x->i];
02760 } else if (node->isBoolVar()) {
02761 AST::BoolVar* x = static_cast<AST::BoolVar*>(node);
02762 if (bv.find(x->i) == bv.end()) {
02763 int newi = bv.size();
02764 bv[x->i] = newi;
02765 }
02766 x->i = bv[x->i];
02767 } else if (node->isSetVar()) {
02768 AST::SetVar* x = static_cast<AST::SetVar*>(node);
02769 if (sv.find(x->i) == sv.end()) {
02770 int newi = sv.size();
02771 sv[x->i] = newi;
02772 }
02773 x->i = sv[x->i];
02774 } else if (node->isFloatVar()) {
02775 AST::FloatVar* x = static_cast<AST::FloatVar*>(node);
02776 if (fv.find(x->i) == fv.end()) {
02777 int newi = fv.size();
02778 fv[x->i] = newi;
02779 }
02780 x->i = fv[x->i];
02781 }
02782 }
02783
02784 void
02785 Printer::shrinkArrays(Space& home,
02786 int& optVar, bool optVarIsInt,
02787 Gecode::IntVarArray& iv,
02788 Gecode::BoolVarArray& bv
02789 #ifdef GECODE_HAS_SET_VARS
02790 ,
02791 Gecode::SetVarArray& sv
02792 #endif
02793 #ifdef GECODE_HAS_FLOAT_VARS
02794 ,
02795 Gecode::FloatVarArray& fv
02796 #endif
02797 ) {
02798 if (_output == NULL) {
02799 if (optVarIsInt && optVar != -1) {
02800 IntVar ov = iv[optVar];
02801 iv = IntVarArray(home, 1);
02802 iv[0] = ov;
02803 optVar = 0;
02804 } else {
02805 iv = IntVarArray(home, 0);
02806 }
02807 bv = BoolVarArray(home, 0);
02808 #ifdef GECODE_HAS_SET_VARS
02809 sv = SetVarArray(home, 0);
02810 #endif
02811 #ifdef GECODE_HAS_FLOAT_VARS
02812 if (!optVarIsInt && optVar != -1) {
02813 FloatVar ov = fv[optVar];
02814 fv = FloatVarArray(home, 1);
02815 fv[0] = ov;
02816 optVar = 0;
02817 } else {
02818 fv = FloatVarArray(home,0);
02819 }
02820 #endif
02821 return;
02822 }
02823 std::map<int,int> iv_new;
02824 std::map<int,int> bv_new;
02825 std::map<int,int> sv_new;
02826 std::map<int,int> fv_new;
02827
02828 if (optVar != -1) {
02829 if (optVarIsInt)
02830 iv_new[optVar] = 0;
02831 else
02832 fv_new[optVar] = 0;
02833 optVar = 0;
02834 }
02835
02836 for (unsigned int i=0; i< _output->a.size(); i++) {
02837 AST::Node* ai = _output->a[i];
02838 if (ai->isArray()) {
02839 AST::Array* aia = ai->getArray();
02840 for (unsigned int j=0; j<aia->a.size(); j++) {
02841 shrinkElement(aia->a[j],iv_new,bv_new,sv_new,fv_new);
02842 }
02843 } else {
02844 shrinkElement(ai,iv_new,bv_new,sv_new,fv_new);
02845 }
02846 }
02847
02848 IntVarArgs iva(iv_new.size());
02849 for (std::map<int,int>::iterator i=iv_new.begin(); i != iv_new.end(); ++i) {
02850 iva[(*i).second] = iv[(*i).first];
02851 }
02852 iv = IntVarArray(home, iva);
02853
02854 BoolVarArgs bva(bv_new.size());
02855 for (std::map<int,int>::iterator i=bv_new.begin(); i != bv_new.end(); ++i) {
02856 bva[(*i).second] = bv[(*i).first];
02857 }
02858 bv = BoolVarArray(home, bva);
02859
02860 #ifdef GECODE_HAS_SET_VARS
02861 SetVarArgs sva(sv_new.size());
02862 for (std::map<int,int>::iterator i=sv_new.begin(); i != sv_new.end(); ++i) {
02863 sva[(*i).second] = sv[(*i).first];
02864 }
02865 sv = SetVarArray(home, sva);
02866 #endif
02867
02868 #ifdef GECODE_HAS_FLOAT_VARS
02869 FloatVarArgs fva(fv_new.size());
02870 for (std::map<int,int>::iterator i=fv_new.begin(); i != fv_new.end(); ++i) {
02871 fva[(*i).second] = fv[(*i).first];
02872 }
02873 fv = FloatVarArray(home, fva);
02874 #endif
02875 }
02876
02877 Printer::~Printer(void) {
02878 delete _output;
02879 }
02880
02881 }}
02882
02883
