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
00039
00040
00041
00042 #include <gecode/flatzinc.hh>
00043 #include <gecode/flatzinc/registry.hh>
00044 #include <gecode/flatzinc/plugin.hh>
00045
00046 #include <gecode/search.hh>
00047
00048 #include <vector>
00049 #include <string>
00050 #include <sstream>
00051 #include <limits>
00052 using namespace std;
00053
00054 namespace Gecode { namespace FlatZinc {
00055
00068 class AuxVarBrancher : public Brancher {
00069 protected:
00071 bool done;
00073 AuxVarBrancher(Home home, TieBreak<IntVarBranch> int_varsel0,
00074 IntValBranch int_valsel0,
00075 TieBreak<IntVarBranch> bool_varsel0,
00076 IntValBranch bool_valsel0
00077 #ifdef GECODE_HAS_SET_VARS
00078 ,
00079 SetVarBranch set_varsel0,
00080 SetValBranch set_valsel0
00081 #endif
00082 #ifdef GECODE_HAS_FLOAT_VARS
00083 ,
00084 TieBreak<FloatVarBranch> float_varsel0,
00085 FloatValBranch float_valsel0
00086 #endif
00087 )
00088 : Brancher(home), done(false),
00089 int_varsel(int_varsel0), int_valsel(int_valsel0),
00090 bool_varsel(bool_varsel0), bool_valsel(bool_valsel0)
00091 #ifdef GECODE_HAS_SET_VARS
00092 , set_varsel(set_varsel0), set_valsel(set_valsel0)
00093 #endif
00094 #ifdef GECODE_HAS_FLOAT_VARS
00095 , float_varsel(float_varsel0), float_valsel(float_valsel0)
00096 #endif
00097 {}
00099 AuxVarBrancher(Space& home, bool share, AuxVarBrancher& b)
00100 : Brancher(home, share, b), done(b.done) {}
00101
00103 class Choice : public Gecode::Choice {
00104 public:
00106 bool fail;
00108 Choice(const Brancher& b, bool fail0)
00109 : Gecode::Choice(b,1), fail(fail0) {}
00111 virtual size_t size(void) const {
00112 return sizeof(Choice);
00113 }
00115 virtual void archive(Archive& e) const {
00116 Gecode::Choice::archive(e);
00117 e.put(fail);
00118 }
00119 };
00120
00121 TieBreak<IntVarBranch> int_varsel;
00122 IntValBranch int_valsel;
00123 TieBreak<IntVarBranch> bool_varsel;
00124 IntValBranch bool_valsel;
00125 #ifdef GECODE_HAS_SET_VARS
00126 SetVarBranch set_varsel;
00127 SetValBranch set_valsel;
00128 #endif
00129 #ifdef GECODE_HAS_FLOAT_VARS
00130 TieBreak<FloatVarBranch> float_varsel;
00131 FloatValBranch float_valsel;
00132 #endif
00133
00134 public:
00136 virtual bool status(const Space& _home) const {
00137 if (done) return false;
00138 const FlatZincSpace& home = static_cast<const FlatZincSpace&>(_home);
00139 for (int i=0; i<home.iv_aux.size(); i++)
00140 if (!home.iv_aux[i].assigned()) return true;
00141 for (int i=0; i<home.bv_aux.size(); i++)
00142 if (!home.bv_aux[i].assigned()) return true;
00143 #ifdef GECODE_HAS_SET_VARS
00144 for (int i=0; i<home.sv_aux.size(); i++)
00145 if (!home.sv_aux[i].assigned()) return true;
00146 #endif
00147 #ifdef GECODE_HAS_FLOAT_VARS
00148 for (int i=0; i<home.fv_aux.size(); i++)
00149 if (!home.fv_aux[i].assigned()) return true;
00150 #endif
00151
00152 return false;
00153 }
00155 virtual Choice* choice(Space& home) {
00156 done = true;
00157 FlatZincSpace& fzs = static_cast<FlatZincSpace&>(*home.clone());
00158 fzs.needAuxVars = false;
00159 branch(fzs,fzs.iv_aux,int_varsel,int_valsel);
00160 branch(fzs,fzs.bv_aux,bool_varsel,bool_valsel);
00161 #ifdef GECODE_HAS_SET_VARS
00162 branch(fzs,fzs.sv_aux,set_varsel,set_valsel);
00163 #endif
00164 #ifdef GECODE_HAS_FLOAT_VARS
00165 branch(fzs,fzs.fv_aux,float_varsel,float_valsel);
00166 #endif
00167 Search::Options opt; opt.clone = false;
00168 FlatZincSpace* sol = dfs(&fzs, opt);
00169 if (sol) {
00170 delete sol;
00171 return new Choice(*this,false);
00172 } else {
00173 return new Choice(*this,true);
00174 }
00175 }
00177 virtual Choice* choice(const Space&, Archive& e) {
00178 bool fail; e >> fail;
00179 return new Choice(*this, fail);
00180 }
00182 virtual ExecStatus commit(Space&, const Gecode::Choice& c, unsigned int) {
00183 return static_cast<const Choice&>(c).fail ? ES_FAILED : ES_OK;
00184 }
00186 virtual void print(const Space&, const Gecode::Choice& c,
00187 unsigned int,
00188 std::ostream& o) const {
00189 o << "FlatZinc("
00190 << (static_cast<const Choice&>(c).fail ? "fail" : "ok")
00191 << ")";
00192 }
00194 virtual Actor* copy(Space& home, bool share) {
00195 return new (home) AuxVarBrancher(home, share, *this);
00196 }
00198 static void post(Home home,
00199 TieBreak<IntVarBranch> int_varsel,
00200 IntValBranch int_valsel,
00201 TieBreak<IntVarBranch> bool_varsel,
00202 IntValBranch bool_valsel
00203 #ifdef GECODE_HAS_SET_VARS
00204 ,
00205 SetVarBranch set_varsel,
00206 SetValBranch set_valsel
00207 #endif
00208 #ifdef GECODE_HAS_FLOAT_VARS
00209 ,
00210 TieBreak<FloatVarBranch> float_varsel,
00211 FloatValBranch float_valsel
00212 #endif
00213 ) {
00214 (void) new (home) AuxVarBrancher(home, int_varsel, int_valsel,
00215 bool_varsel, bool_valsel
00216 #ifdef GECODE_HAS_SET_VARS
00217 , set_varsel, set_valsel
00218 #endif
00219 #ifdef GECODE_HAS_FLOAT_VARS
00220 , float_varsel, float_valsel
00221 #endif
00222 );
00223 }
00225 virtual size_t dispose(Space&) {
00226 return sizeof(*this);
00227 }
00228 };
00229
00230 class BranchInformationO : public SharedHandle::Object {
00231 private:
00232 struct BI {
00233 string r0;
00234 string r1;
00235 vector<string> n;
00236 BI(void) : r0(""), r1(""), n(0) {}
00237 BI(const string& r00, const string& r10, const vector<string>& n0)
00238 : r0(r00), r1(r10), n(n0) {}
00239 };
00240 vector<BI> v;
00241 BranchInformationO(vector<BI> v0) : v(v0) {}
00242 public:
00243 BranchInformationO(void) {}
00244 virtual ~BranchInformationO(void) {}
00245 virtual SharedHandle::Object* copy(void) const {
00246 return new BranchInformationO(v);
00247 }
00249 void add(const BrancherHandle& bh,
00250 const string& rel0,
00251 const string& rel1,
00252 const vector<string>& n) {
00253 v.resize(std::max(static_cast<unsigned int>(v.size()),bh.id()+1));
00254 v[bh.id()] = BI(rel0,rel1,n);
00255 }
00257 void print(const BrancherHandle& bh,
00258 int a, int i, int n, ostream& o) const {
00259 const BI& bi = v[bh.id()];
00260 o << bi.n[i] << " " << (a==0 ? bi.r0 : bi.r1) << " " << n;
00261 }
00262 #ifdef GECODE_HAS_FLOAT_VARS
00263 void print(const BrancherHandle& bh,
00264 int a, int i, const FloatNumBranch& nl, ostream& o) const {
00265 const BI& bi = v[bh.id()];
00266 o << bi.n[i] << " "
00267 << (((a == 0) == nl.l) ? "<=" : ">=") << nl.n;
00268 }
00269 #endif
00270 };
00271
00272 BranchInformation::BranchInformation(void)
00273 : SharedHandle(NULL) {}
00274
00275 BranchInformation::BranchInformation(const BranchInformation& bi)
00276 : SharedHandle(bi) {}
00277
00278 void
00279 BranchInformation::init(void) {
00280 assert(object() == 0);
00281 object(new BranchInformationO());
00282 }
00283
00284 void
00285 BranchInformation::add(const BrancherHandle& bh,
00286 const std::string& rel0,
00287 const std::string& rel1,
00288 const std::vector<std::string>& n) {
00289 static_cast<BranchInformationO*>(object())->add(bh,rel0,rel1,n);
00290 }
00291 void
00292 BranchInformation::print(const BrancherHandle& bh, int a, int i,
00293 int n, std::ostream& o) const {
00294 static_cast<const BranchInformationO*>(object())->print(bh,a,i,n,o);
00295 }
00296 #ifdef GECODE_HAS_FLOAT_VARS
00297 void
00298 BranchInformation::print(const BrancherHandle& bh, int a, int i,
00299 const FloatNumBranch& nl, std::ostream& o) const {
00300 static_cast<const BranchInformationO*>(object())->print(bh,a,i,nl,o);
00301 }
00302 #endif
00303 template<class Var>
00304 void varValPrint(const Space &home, const BrancherHandle& bh,
00305 unsigned int a,
00306 Var, int i, const int& n,
00307 std::ostream& o) {
00308 static_cast<const FlatZincSpace&>(home).branchInfo.print(bh,a,i,n,o);
00309 }
00310
00311 #ifdef GECODE_HAS_FLOAT_VARS
00312 void varValPrintF(const Space &home, const BrancherHandle& bh,
00313 unsigned int a,
00314 FloatVar, int i, const FloatNumBranch& nl,
00315 std::ostream& o) {
00316 static_cast<const FlatZincSpace&>(home).branchInfo.print(bh,a,i,nl,o);
00317 }
00318 #endif
00319
00320 IntSet vs2is(IntVarSpec* vs) {
00321 if (vs->assigned) {
00322 return IntSet(vs->i,vs->i);
00323 }
00324 if (vs->domain()) {
00325 AST::SetLit* sl = vs->domain.some();
00326 if (sl->interval) {
00327 return IntSet(sl->min, sl->max);
00328 } else {
00329 int* newdom = heap.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
00330 for (int i=sl->s.size(); i--;)
00331 newdom[i] = sl->s[i];
00332 IntSet ret(newdom, sl->s.size());
00333 heap.free(newdom, static_cast<unsigned long int>(sl->s.size()));
00334 return ret;
00335 }
00336 }
00337 return IntSet(Int::Limits::min, Int::Limits::max);
00338 }
00339
00340 int vs2bsl(BoolVarSpec* bs) {
00341 if (bs->assigned) {
00342 return bs->i;
00343 }
00344 if (bs->domain()) {
00345 AST::SetLit* sl = bs->domain.some();
00346 assert(sl->interval);
00347 return std::min(1, std::max(0, sl->min));
00348 }
00349 return 0;
00350 }
00351
00352 int vs2bsh(BoolVarSpec* bs) {
00353 if (bs->assigned) {
00354 return bs->i;
00355 }
00356 if (bs->domain()) {
00357 AST::SetLit* sl = bs->domain.some();
00358 assert(sl->interval);
00359 return std::max(0, std::min(1, sl->max));
00360 }
00361 return 1;
00362 }
00363
00364 TieBreak<IntVarBranch> ann2ivarsel(AST::Node* ann, Rnd rnd, double decay) {
00365 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00366 if (s->id == "input_order")
00367 return TieBreak<IntVarBranch>(INT_VAR_NONE());
00368 if (s->id == "first_fail")
00369 return TieBreak<IntVarBranch>(INT_VAR_SIZE_MIN());
00370 if (s->id == "anti_first_fail")
00371 return TieBreak<IntVarBranch>(INT_VAR_SIZE_MAX());
00372 if (s->id == "smallest")
00373 return TieBreak<IntVarBranch>(INT_VAR_MIN_MIN());
00374 if (s->id == "largest")
00375 return TieBreak<IntVarBranch>(INT_VAR_MAX_MAX());
00376 if (s->id == "occurrence")
00377 return TieBreak<IntVarBranch>(INT_VAR_DEGREE_MAX());
00378 if (s->id == "max_regret")
00379 return TieBreak<IntVarBranch>(INT_VAR_REGRET_MIN_MAX());
00380 if (s->id == "most_constrained")
00381 return TieBreak<IntVarBranch>(INT_VAR_SIZE_MIN(),
00382 INT_VAR_DEGREE_MAX());
00383 if (s->id == "random") {
00384 return TieBreak<IntVarBranch>(INT_VAR_RND(rnd));
00385 }
00386 if (s->id == "afc_min")
00387 return TieBreak<IntVarBranch>(INT_VAR_AFC_MIN(decay));
00388 if (s->id == "afc_max")
00389 return TieBreak<IntVarBranch>(INT_VAR_AFC_MAX(decay));
00390 if (s->id == "afc_size_min")
00391 return TieBreak<IntVarBranch>(INT_VAR_AFC_SIZE_MIN(decay));
00392 if (s->id == "afc_size_max") {
00393 return TieBreak<IntVarBranch>(INT_VAR_AFC_SIZE_MAX(decay));
00394 }
00395 if (s->id == "activity_min")
00396 return TieBreak<IntVarBranch>(INT_VAR_ACTIVITY_MIN(decay));
00397 if (s->id == "activity_max")
00398 return TieBreak<IntVarBranch>(INT_VAR_ACTIVITY_MAX(decay));
00399 if (s->id == "activity_size_min")
00400 return TieBreak<IntVarBranch>(INT_VAR_ACTIVITY_SIZE_MIN(decay));
00401 if (s->id == "activity_size_max")
00402 return TieBreak<IntVarBranch>(INT_VAR_ACTIVITY_SIZE_MAX(decay));
00403 }
00404 std::cerr << "Warning, ignored search annotation: ";
00405 ann->print(std::cerr);
00406 std::cerr << std::endl;
00407 return TieBreak<IntVarBranch>(INT_VAR_NONE());
00408 }
00409
00410 IntValBranch ann2ivalsel(AST::Node* ann, std::string& r0, std::string& r1,
00411 Rnd rnd) {
00412 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00413 if (s->id == "indomain_min") {
00414 r0 = "="; r1 = "!=";
00415 return INT_VAL_MIN();
00416 }
00417 if (s->id == "indomain_max") {
00418 r0 = "="; r1 = "!=";
00419 return INT_VAL_MAX();
00420 }
00421 if (s->id == "indomain_median") {
00422 r0 = "="; r1 = "!=";
00423 return INT_VAL_MED();
00424 }
00425 if (s->id == "indomain_split") {
00426 r0 = "<="; r1 = ">";
00427 return INT_VAL_SPLIT_MIN();
00428 }
00429 if (s->id == "indomain_reverse_split") {
00430 r0 = ">"; r1 = "<=";
00431 return INT_VAL_SPLIT_MAX();
00432 }
00433 if (s->id == "indomain_random") {
00434 r0 = "="; r1 = "!=";
00435 return INT_VAL_RND(rnd);
00436 }
00437 if (s->id == "indomain") {
00438 r0 = "="; r1 = "=";
00439 return INT_VALUES_MIN();
00440 }
00441 if (s->id == "indomain_middle") {
00442 std::cerr << "Warning, replacing unsupported annotation "
00443 << "indomain_middle with indomain_median" << std::endl;
00444 r0 = "="; r1 = "!=";
00445 return INT_VAL_MED();
00446 }
00447 if (s->id == "indomain_interval") {
00448 std::cerr << "Warning, replacing unsupported annotation "
00449 << "indomain_interval with indomain_split" << std::endl;
00450 r0 = "<="; r1 = ">";
00451 return INT_VAL_SPLIT_MIN();
00452 }
00453 }
00454 std::cerr << "Warning, ignored search annotation: ";
00455 ann->print(std::cerr);
00456 std::cerr << std::endl;
00457 r0 = "="; r1 = "!=";
00458 return INT_VAL_MIN();
00459 }
00460
00461 IntAssign ann2asnivalsel(AST::Node* ann, Rnd rnd) {
00462 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00463 if (s->id == "indomain_min")
00464 return INT_ASSIGN_MIN();
00465 if (s->id == "indomain_max")
00466 return INT_ASSIGN_MAX();
00467 if (s->id == "indomain_median")
00468 return INT_ASSIGN_MED();
00469 if (s->id == "indomain_random") {
00470 return INT_ASSIGN_RND(rnd);
00471 }
00472 }
00473 std::cerr << "Warning, ignored search annotation: ";
00474 ann->print(std::cerr);
00475 std::cerr << std::endl;
00476 return INT_ASSIGN_MIN();
00477 }
00478
00479 #ifdef GECODE_HAS_SET_VARS
00480 SetVarBranch ann2svarsel(AST::Node* ann, Rnd rnd, double decay) {
00481 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00482 if (s->id == "input_order")
00483 return SET_VAR_NONE();
00484 if (s->id == "first_fail")
00485 return SET_VAR_SIZE_MIN();
00486 if (s->id == "anti_first_fail")
00487 return SET_VAR_SIZE_MAX();
00488 if (s->id == "smallest")
00489 return SET_VAR_MIN_MIN();
00490 if (s->id == "largest")
00491 return SET_VAR_MAX_MAX();
00492 if (s->id == "afc_min")
00493 return SET_VAR_AFC_MIN(decay);
00494 if (s->id == "afc_max")
00495 return SET_VAR_AFC_MAX(decay);
00496 if (s->id == "afc_size_min")
00497 return SET_VAR_AFC_SIZE_MIN(decay);
00498 if (s->id == "afc_size_max")
00499 return SET_VAR_AFC_SIZE_MAX(decay);
00500 if (s->id == "activity_min")
00501 return SET_VAR_ACTIVITY_MIN(decay);
00502 if (s->id == "activity_max")
00503 return SET_VAR_ACTIVITY_MAX(decay);
00504 if (s->id == "activity_size_min")
00505 return SET_VAR_ACTIVITY_SIZE_MIN(decay);
00506 if (s->id == "activity_size_max")
00507 return SET_VAR_ACTIVITY_SIZE_MAX(decay);
00508 if (s->id == "random") {
00509 return SET_VAR_RND(rnd);
00510 }
00511 }
00512 std::cerr << "Warning, ignored search annotation: ";
00513 ann->print(std::cerr);
00514 std::cerr << std::endl;
00515 return SET_VAR_NONE();
00516 }
00517
00518 SetValBranch ann2svalsel(AST::Node* ann, std::string r0, std::string r1,
00519 Rnd rnd) {
00520 (void) rnd;
00521 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00522 if (s->id == "indomain_min") {
00523 r0 = "in"; r1 = "not in";
00524 return SET_VAL_MIN_INC();
00525 }
00526 if (s->id == "indomain_max") {
00527 r0 = "in"; r1 = "not in";
00528 return SET_VAL_MAX_INC();
00529 }
00530 if (s->id == "outdomain_min") {
00531 r1 = "in"; r0 = "not in";
00532 return SET_VAL_MIN_EXC();
00533 }
00534 if (s->id == "outdomain_max") {
00535 r1 = "in"; r0 = "not in";
00536 return SET_VAL_MAX_EXC();
00537 }
00538 }
00539 std::cerr << "Warning, ignored search annotation: ";
00540 ann->print(std::cerr);
00541 std::cerr << std::endl;
00542 r0 = "in"; r1 = "not in";
00543 return SET_VAL_MIN_INC();
00544 }
00545 #endif
00546
00547 #ifdef GECODE_HAS_FLOAT_VARS
00548 TieBreak<FloatVarBranch> ann2fvarsel(AST::Node* ann, Rnd rnd,
00549 double decay) {
00550 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00551 if (s->id == "input_order")
00552 return TieBreak<FloatVarBranch>(FLOAT_VAR_NONE());
00553 if (s->id == "first_fail")
00554 return TieBreak<FloatVarBranch>(FLOAT_VAR_SIZE_MIN());
00555 if (s->id == "anti_first_fail")
00556 return TieBreak<FloatVarBranch>(FLOAT_VAR_SIZE_MAX());
00557 if (s->id == "smallest")
00558 return TieBreak<FloatVarBranch>(FLOAT_VAR_MIN_MIN());
00559 if (s->id == "largest")
00560 return TieBreak<FloatVarBranch>(FLOAT_VAR_MAX_MAX());
00561 if (s->id == "occurrence")
00562 return TieBreak<FloatVarBranch>(FLOAT_VAR_DEGREE_MAX());
00563 if (s->id == "most_constrained")
00564 return TieBreak<FloatVarBranch>(FLOAT_VAR_SIZE_MIN(),
00565 FLOAT_VAR_DEGREE_MAX());
00566 if (s->id == "random") {
00567 return TieBreak<FloatVarBranch>(FLOAT_VAR_RND(rnd));
00568 }
00569 if (s->id == "afc_min")
00570 return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_MIN(decay));
00571 if (s->id == "afc_max")
00572 return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_MAX(decay));
00573 if (s->id == "afc_size_min")
00574 return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_SIZE_MIN(decay));
00575 if (s->id == "afc_size_max")
00576 return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_SIZE_MAX(decay));
00577 if (s->id == "activity_min")
00578 return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTIVITY_MIN(decay));
00579 if (s->id == "activity_max")
00580 return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTIVITY_MAX(decay));
00581 if (s->id == "activity_size_min")
00582 return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTIVITY_SIZE_MIN(decay));
00583 if (s->id == "activity_size_max")
00584 return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTIVITY_SIZE_MAX(decay));
00585 }
00586 std::cerr << "Warning, ignored search annotation: ";
00587 ann->print(std::cerr);
00588 std::cerr << std::endl;
00589 return TieBreak<FloatVarBranch>(FLOAT_VAR_NONE());
00590 }
00591
00592 FloatValBranch ann2fvalsel(AST::Node* ann, std::string r0, std::string r1) {
00593 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00594 if (s->id == "indomain_split") {
00595 r0 = "<="; r1 = ">";
00596 return FLOAT_VAL_SPLIT_MIN();
00597 }
00598 if (s->id == "indomain_reverse_split") {
00599 r1 = "<="; r0 = ">";
00600 return FLOAT_VAL_SPLIT_MAX();
00601 }
00602 }
00603 std::cerr << "Warning, ignored search annotation: ";
00604 ann->print(std::cerr);
00605 std::cerr << std::endl;
00606 r0 = "<="; r1 = ">";
00607 return FLOAT_VAL_SPLIT_MIN();
00608 }
00609
00610 #endif
00611
00612 FlatZincSpace::FlatZincSpace(bool share, FlatZincSpace& f)
00613 : Space(share, f), _solveAnnotations(NULL), iv_boolalias(NULL),
00614 needAuxVars(f.needAuxVars) {
00615 _optVar = f._optVar;
00616 _optVarIsInt = f._optVarIsInt;
00617 _method = f._method;
00618 branchInfo.update(*this, share, f.branchInfo);
00619 iv.update(*this, share, f.iv);
00620 intVarCount = f.intVarCount;
00621
00622 if (needAuxVars) {
00623 IntVarArgs iva;
00624 for (int i=0; i<f.iv_aux.size(); i++) {
00625 if (!f.iv_aux[i].assigned()) {
00626 iva << IntVar();
00627 iva[iva.size()-1].update(*this, share, f.iv_aux[i]);
00628 }
00629 }
00630 iv_aux = IntVarArray(*this, iva);
00631 }
00632
00633 bv.update(*this, share, f.bv);
00634 boolVarCount = f.boolVarCount;
00635 if (needAuxVars) {
00636 BoolVarArgs bva;
00637 for (int i=0; i<f.bv_aux.size(); i++) {
00638 if (!f.bv_aux[i].assigned()) {
00639 bva << BoolVar();
00640 bva[bva.size()-1].update(*this, share, f.bv_aux[i]);
00641 }
00642 }
00643 bv_aux = BoolVarArray(*this, bva);
00644 }
00645
00646 #ifdef GECODE_HAS_SET_VARS
00647 sv.update(*this, share, f.sv);
00648 setVarCount = f.setVarCount;
00649 if (needAuxVars) {
00650 SetVarArgs sva;
00651 for (int i=0; i<f.sv_aux.size(); i++) {
00652 if (!f.sv_aux[i].assigned()) {
00653 sva << SetVar();
00654 sva[sva.size()-1].update(*this, share, f.sv_aux[i]);
00655 }
00656 }
00657 sv_aux = SetVarArray(*this, sva);
00658 }
00659 #endif
00660 #ifdef GECODE_HAS_FLOAT_VARS
00661 fv.update(*this, share, f.fv);
00662 floatVarCount = f.floatVarCount;
00663 if (needAuxVars) {
00664 FloatVarArgs fva;
00665 for (int i=0; i<f.fv_aux.size(); i++) {
00666 if (!f.fv_aux[i].assigned()) {
00667 fva << FloatVar();
00668 fva[fva.size()-1].update(*this, share, f.fv_aux[i]);
00669 }
00670 }
00671 fv_aux = FloatVarArray(*this, fva);
00672 }
00673 #endif
00674 }
00675
00676 FlatZincSpace::FlatZincSpace(void)
00677 : intVarCount(-1), boolVarCount(-1), floatVarCount(-1), setVarCount(-1),
00678 _optVar(-1), _optVarIsInt(true),
00679 _solveAnnotations(NULL), needAuxVars(true) {
00680 branchInfo.init();
00681 }
00682
00683 void
00684 FlatZincSpace::init(int intVars, int boolVars,
00685 int setVars, int floatVars) {
00686 (void) setVars;
00687 (void) floatVars;
00688
00689 intVarCount = 0;
00690 iv = IntVarArray(*this, intVars);
00691 iv_introduced = std::vector<bool>(2*intVars);
00692 iv_boolalias = alloc<int>(intVars+(intVars==0?1:0));
00693 boolVarCount = 0;
00694 bv = BoolVarArray(*this, boolVars);
00695 bv_introduced = std::vector<bool>(2*boolVars);
00696 #ifdef GECODE_HAS_SET_VARS
00697 setVarCount = 0;
00698 sv = SetVarArray(*this, setVars);
00699 sv_introduced = std::vector<bool>(2*setVars);
00700 #endif
00701 #ifdef GECODE_HAS_FLOAT_VARS
00702 floatVarCount = 0;
00703 fv = FloatVarArray(*this, floatVars);
00704 fv_introduced = std::vector<bool>(2*floatVars);
00705 #endif
00706 }
00707
00708 void
00709 FlatZincSpace::newIntVar(IntVarSpec* vs) {
00710 if (vs->alias) {
00711 iv[intVarCount++] = iv[vs->i];
00712 } else {
00713 IntSet dom(vs2is(vs));
00714 if (dom.size()==0) {
00715 fail();
00716 return;
00717 } else {
00718 iv[intVarCount++] = IntVar(*this, dom);
00719 }
00720 }
00721 iv_introduced[2*(intVarCount-1)] = vs->introduced;
00722 iv_introduced[2*(intVarCount-1)+1] = vs->funcDep;
00723 iv_boolalias[intVarCount-1] = -1;
00724 }
00725
00726 void
00727 FlatZincSpace::aliasBool2Int(int iv, int bv) {
00728 iv_boolalias[iv] = bv;
00729 }
00730 int
00731 FlatZincSpace::aliasBool2Int(int iv) {
00732 return iv_boolalias[iv];
00733 }
00734
00735 void
00736 FlatZincSpace::newBoolVar(BoolVarSpec* vs) {
00737 if (vs->alias) {
00738 bv[boolVarCount++] = bv[vs->i];
00739 } else {
00740 bv[boolVarCount++] = BoolVar(*this, vs2bsl(vs), vs2bsh(vs));
00741 }
00742 bv_introduced[2*(boolVarCount-1)] = vs->introduced;
00743 bv_introduced[2*(boolVarCount-1)+1] = vs->funcDep;
00744 }
00745
00746 #ifdef GECODE_HAS_SET_VARS
00747 void
00748 FlatZincSpace::newSetVar(SetVarSpec* vs) {
00749 if (vs->alias) {
00750 sv[setVarCount++] = sv[vs->i];
00751 } else if (vs->assigned) {
00752 assert(vs->upperBound());
00753 AST::SetLit* vsv = vs->upperBound.some();
00754 if (vsv->interval) {
00755 IntSet d(vsv->min, vsv->max);
00756 sv[setVarCount++] = SetVar(*this, d, d);
00757 } else {
00758 int* is = heap.alloc<int>(static_cast<unsigned long int>(vsv->s.size()));
00759 for (int i=vsv->s.size(); i--; )
00760 is[i] = vsv->s[i];
00761 IntSet d(is, vsv->s.size());
00762 heap.free(is,static_cast<unsigned long int>(vsv->s.size()));
00763 sv[setVarCount++] = SetVar(*this, d, d);
00764 }
00765 } else if (vs->upperBound()) {
00766 AST::SetLit* vsv = vs->upperBound.some();
00767 if (vsv->interval) {
00768 IntSet d(vsv->min, vsv->max);
00769 sv[setVarCount++] = SetVar(*this, IntSet::empty, d);
00770 } else {
00771 int* is = heap.alloc<int>(static_cast<unsigned long int>(vsv->s.size()));
00772 for (int i=vsv->s.size(); i--; )
00773 is[i] = vsv->s[i];
00774 IntSet d(is, vsv->s.size());
00775 heap.free(is,static_cast<unsigned long int>(vsv->s.size()));
00776 sv[setVarCount++] = SetVar(*this, IntSet::empty, d);
00777 }
00778 } else {
00779 sv[setVarCount++] = SetVar(*this, IntSet::empty,
00780 IntSet(Set::Limits::min,
00781 Set::Limits::max));
00782 }
00783 sv_introduced[2*(setVarCount-1)] = vs->introduced;
00784 sv_introduced[2*(setVarCount-1)+1] = vs->funcDep;
00785 }
00786 #else
00787 void
00788 FlatZincSpace::newSetVar(SetVarSpec*) {
00789 throw FlatZinc::Error("Gecode", "set variables not supported");
00790 }
00791 #endif
00792
00793 #ifdef GECODE_HAS_FLOAT_VARS
00794 void
00795 FlatZincSpace::newFloatVar(FloatVarSpec* vs) {
00796 if (vs->alias) {
00797 fv[floatVarCount++] = fv[vs->i];
00798 } else {
00799 double dmin, dmax;
00800 if (vs->domain()) {
00801 dmin = vs->domain.some().first;
00802 dmax = vs->domain.some().second;
00803 if (dmin > dmax) {
00804 fail();
00805 return;
00806 }
00807 } else {
00808 dmin = Float::Limits::min;
00809 dmax = Float::Limits::max;
00810 }
00811 fv[floatVarCount++] = FloatVar(*this, dmin, dmax);
00812 }
00813 fv_introduced[2*(floatVarCount-1)] = vs->introduced;
00814 fv_introduced[2*(floatVarCount-1)+1] = vs->funcDep;
00815 }
00816 #else
00817 void
00818 FlatZincSpace::newFloatVar(FloatVarSpec*) {
00819 throw FlatZinc::Error("Gecode", "float variables not supported");
00820 }
00821 #endif
00822
00823 void
00824 FlatZincSpace::postConstraint(const ConExpr& ce, AST::Node* ann) {
00825 try {
00826 registry().post(*this, ce, ann);
00827 } catch (Gecode::Exception& e) {
00828 throw FlatZinc::Error("Gecode", e.what());
00829 } catch (AST::TypeError& e) {
00830 throw FlatZinc::Error("Type error", e.what());
00831 }
00832 }
00833
00834 void flattenAnnotations(AST::Array* ann, std::vector<AST::Node*>& out) {
00835 for (unsigned int i=0; i<ann->a.size(); i++) {
00836 if (ann->a[i]->isCall("seq_search")) {
00837 AST::Call* c = ann->a[i]->getCall();
00838 if (c->args->isArray())
00839 flattenAnnotations(c->args->getArray(), out);
00840 else
00841 out.push_back(c->args);
00842 } else {
00843 out.push_back(ann->a[i]);
00844 }
00845 }
00846 }
00847
00848 void
00849 FlatZincSpace::createBranchers(AST::Node* ann, int seed, double decay,
00850 bool ignoreUnknown,
00851 std::ostream& err) {
00852 Rnd rnd(static_cast<unsigned int>(seed));
00853 TieBreak<IntVarBranch> def_int_varsel = INT_VAR_AFC_SIZE_MAX(0.99);
00854 IntValBranch def_int_valsel = INT_VAL_MIN();
00855 TieBreak<IntVarBranch> def_bool_varsel = INT_VAR_AFC_MAX(0.99);
00856 IntValBranch def_bool_valsel = INT_VAL_MIN();
00857 #ifdef GECODE_HAS_SET_VARS
00858 SetVarBranch def_set_varsel = SET_VAR_AFC_SIZE_MAX(0.99);
00859 SetValBranch def_set_valsel = SET_VAL_MIN_INC();
00860 #endif
00861 #ifdef GECODE_HAS_FLOAT_VARS
00862 TieBreak<FloatVarBranch> def_float_varsel = FLOAT_VAR_SIZE_MIN();
00863 FloatValBranch def_float_valsel = FLOAT_VAL_SPLIT_MIN();
00864 #endif
00865
00866 std::vector<bool> iv_searched(iv.size());
00867 for (unsigned int i=iv.size(); i--;)
00868 iv_searched[i] = false;
00869 std::vector<bool> bv_searched(bv.size());
00870 for (unsigned int i=bv.size(); i--;)
00871 bv_searched[i] = false;
00872 #ifdef GECODE_HAS_SET_VARS
00873 std::vector<bool> sv_searched(sv.size());
00874 for (unsigned int i=sv.size(); i--;)
00875 sv_searched[i] = false;
00876 #endif
00877 #ifdef GECODE_HAS_FLOAT_VARS
00878 std::vector<bool> fv_searched(fv.size());
00879 for (unsigned int i=fv.size(); i--;)
00880 fv_searched[i] = false;
00881 #endif
00882
00883 if (ann) {
00884 std::vector<AST::Node*> flatAnn;
00885 if (ann->isArray()) {
00886 flattenAnnotations(ann->getArray() , flatAnn);
00887 } else {
00888 flatAnn.push_back(ann);
00889 }
00890
00891 for (unsigned int i=0; i<flatAnn.size(); i++) {
00892 if (flatAnn[i]->isCall("gecode_search")) {
00893 AST::Call* c = flatAnn[i]->getCall();
00894 branchWithPlugin(c->args);
00895 } else if (flatAnn[i]->isCall("int_search")) {
00896 AST::Call *call = flatAnn[i]->getCall("int_search");
00897 AST::Array *args = call->getArgs(4);
00898 AST::Array *vars = args->a[0]->getArray();
00899 int k=vars->a.size();
00900 for (int i=vars->a.size(); i--;)
00901 if (vars->a[i]->isInt())
00902 k--;
00903 IntVarArgs va(k);
00904 vector<string> names;
00905 k=0;
00906 for (unsigned int i=0; i<vars->a.size(); i++) {
00907 if (vars->a[i]->isInt())
00908 continue;
00909 va[k++] = iv[vars->a[i]->getIntVar()];
00910 iv_searched[vars->a[i]->getIntVar()] = true;
00911 names.push_back(vars->a[i]->getVarName());
00912 }
00913 std::string r0, r1;
00914 BrancherHandle bh = branch(*this, va,
00915 ann2ivarsel(args->a[1],rnd,decay),
00916 ann2ivalsel(args->a[2],r0,r1,rnd),
00917 NULL,
00918 &varValPrint<IntVar>);
00919 branchInfo.add(bh,r0,r1,names);
00920 } else if (flatAnn[i]->isCall("int_assign")) {
00921 AST::Call *call = flatAnn[i]->getCall("int_assign");
00922 AST::Array *args = call->getArgs(2);
00923 AST::Array *vars = args->a[0]->getArray();
00924 int k=vars->a.size();
00925 for (int i=vars->a.size(); i--;)
00926 if (vars->a[i]->isInt())
00927 k--;
00928 IntVarArgs va(k);
00929 k=0;
00930 for (unsigned int i=0; i<vars->a.size(); i++) {
00931 if (vars->a[i]->isInt())
00932 continue;
00933 va[k++] = iv[vars->a[i]->getIntVar()];
00934 iv_searched[vars->a[i]->getIntVar()] = true;
00935 }
00936 assign(*this, va, ann2asnivalsel(args->a[1],rnd), NULL,
00937 &varValPrint<IntVar>);
00938 } else if (flatAnn[i]->isCall("bool_search")) {
00939 AST::Call *call = flatAnn[i]->getCall("bool_search");
00940 AST::Array *args = call->getArgs(4);
00941 AST::Array *vars = args->a[0]->getArray();
00942 int k=vars->a.size();
00943 for (int i=vars->a.size(); i--;)
00944 if (vars->a[i]->isBool())
00945 k--;
00946 BoolVarArgs va(k);
00947 k=0;
00948 vector<string> names;
00949 for (unsigned int i=0; i<vars->a.size(); i++) {
00950 if (vars->a[i]->isBool())
00951 continue;
00952 va[k++] = bv[vars->a[i]->getBoolVar()];
00953 bv_searched[vars->a[i]->getBoolVar()] = true;
00954 names.push_back(vars->a[i]->getVarName());
00955 }
00956
00957 std::string r0, r1;
00958 BrancherHandle bh = branch(*this, va,
00959 ann2ivarsel(args->a[1],rnd,decay),
00960 ann2ivalsel(args->a[2],r0,r1,rnd), NULL,
00961 &varValPrint<BoolVar>);
00962 branchInfo.add(bh,r0,r1,names);
00963 } else if (flatAnn[i]->isCall("int_default_search")) {
00964 AST::Call *call = flatAnn[i]->getCall("int_default_search");
00965 AST::Array *args = call->getArgs(2);
00966 def_int_varsel = ann2ivarsel(args->a[0],rnd,decay);
00967 std::string r0;
00968 def_int_valsel = ann2ivalsel(args->a[1],r0,r0,rnd);
00969 } else if (flatAnn[i]->isCall("bool_default_search")) {
00970 AST::Call *call = flatAnn[i]->getCall("bool_default_search");
00971 AST::Array *args = call->getArgs(2);
00972 def_bool_varsel = ann2ivarsel(args->a[0],rnd,decay);
00973 std::string r0;
00974 def_bool_valsel = ann2ivalsel(args->a[1],r0,r0,rnd);
00975 } else if (flatAnn[i]->isCall("set_search")) {
00976 #ifdef GECODE_HAS_SET_VARS
00977 AST::Call *call = flatAnn[i]->getCall("set_search");
00978 AST::Array *args = call->getArgs(4);
00979 AST::Array *vars = args->a[0]->getArray();
00980 int k=vars->a.size();
00981 for (int i=vars->a.size(); i--;)
00982 if (vars->a[i]->isSet())
00983 k--;
00984 SetVarArgs va(k);
00985 k=0;
00986 vector<string> names;
00987 for (unsigned int i=0; i<vars->a.size(); i++) {
00988 if (vars->a[i]->isSet())
00989 continue;
00990 va[k++] = sv[vars->a[i]->getSetVar()];
00991 sv_searched[vars->a[i]->getSetVar()] = true;
00992 names.push_back(vars->a[i]->getVarName());
00993 }
00994 std::string r0, r1;
00995 BrancherHandle bh = branch(*this, va,
00996 ann2svarsel(args->a[1],rnd,decay),
00997 ann2svalsel(args->a[2],r0,r1,rnd),
00998 NULL,
00999 &varValPrint<SetVar>);
01000 branchInfo.add(bh,r0,r1,names);
01001 #else
01002 if (!ignoreUnknown) {
01003 err << "Warning, ignored search annotation: ";
01004 flatAnn[i]->print(err);
01005 err << std::endl;
01006 }
01007 #endif
01008 } else if (flatAnn[i]->isCall("set_default_search")) {
01009 #ifdef GECODE_HAS_SET_VARS
01010 AST::Call *call = flatAnn[i]->getCall("set_default_search");
01011 AST::Array *args = call->getArgs(2);
01012 def_set_varsel = ann2svarsel(args->a[0],rnd,decay);
01013 std::string r0;
01014 def_set_valsel = ann2svalsel(args->a[1],r0,r0,rnd);
01015 #else
01016 if (!ignoreUnknown) {
01017 err << "Warning, ignored search annotation: ";
01018 flatAnn[i]->print(err);
01019 err << std::endl;
01020 }
01021 #endif
01022 } else if (flatAnn[i]->isCall("float_default_search")) {
01023 #ifdef GECODE_HAS_FLOAT_VARS
01024 AST::Call *call = flatAnn[i]->getCall("float_default_search");
01025 AST::Array *args = call->getArgs(2);
01026 def_float_varsel = ann2fvarsel(args->a[0],rnd,decay);
01027 std::string r0;
01028 def_float_valsel = ann2fvalsel(args->a[1],r0,r0);
01029 #else
01030 if (!ignoreUnknown) {
01031 err << "Warning, ignored search annotation: ";
01032 flatAnn[i]->print(err);
01033 err << std::endl;
01034 }
01035 #endif
01036 } else if (flatAnn[i]->isCall("float_search")) {
01037 #ifdef GECODE_HAS_FLOAT_VARS
01038 AST::Call *call = flatAnn[i]->getCall("float_search");
01039 AST::Array *args = call->getArgs(5);
01040 AST::Array *vars = args->a[0]->getArray();
01041 int k=vars->a.size();
01042 for (int i=vars->a.size(); i--;)
01043 if (vars->a[i]->isFloat())
01044 k--;
01045 FloatVarArgs va(k);
01046 k=0;
01047 vector<string> names;
01048 for (unsigned int i=0; i<vars->a.size(); i++) {
01049 if (vars->a[i]->isFloat())
01050 continue;
01051 va[k++] = fv[vars->a[i]->getFloatVar()];
01052 fv_searched[vars->a[i]->getFloatVar()] = true;
01053 names.push_back(vars->a[i]->getVarName());
01054 }
01055 std::string r0, r1;
01056 BrancherHandle bh = branch(*this, va,
01057 ann2fvarsel(args->a[2],rnd,decay),
01058 ann2fvalsel(args->a[3],r0,r1),
01059 NULL,
01060 &varValPrintF);
01061 branchInfo.add(bh,r0,r1,names);
01062 #else
01063 if (!ignoreUnknown) {
01064 err << "Warning, ignored search annotation: ";
01065 flatAnn[i]->print(err);
01066 err << std::endl;
01067 }
01068 #endif
01069 } else {
01070 if (!ignoreUnknown) {
01071 err << "Warning, ignored search annotation: ";
01072 flatAnn[i]->print(err);
01073 err << std::endl;
01074 }
01075 }
01076 }
01077 }
01078 int introduced = 0;
01079 int funcdep = 0;
01080 int searched = 0;
01081 for (int i=iv.size(); i--;) {
01082 if (iv_searched[i]) {
01083 searched++;
01084 } else if (iv_introduced[2*i]) {
01085 if (iv_introduced[2*i+1]) {
01086 funcdep++;
01087 } else {
01088 introduced++;
01089 }
01090 }
01091 }
01092 IntVarArgs iv_sol(iv.size()-(introduced+funcdep+searched));
01093 IntVarArgs iv_tmp(introduced);
01094 for (int i=iv.size(), j=0, k=0; i--;) {
01095 if (iv_searched[i])
01096 continue;
01097 if (iv_introduced[2*i]) {
01098 if (!iv_introduced[2*i+1]) {
01099 iv_tmp[j++] = iv[i];
01100 }
01101 } else {
01102 iv_sol[k++] = iv[i];
01103 }
01104 }
01105
01106 introduced = 0;
01107 funcdep = 0;
01108 searched = 0;
01109 for (int i=bv.size(); i--;) {
01110 if (bv_searched[i]) {
01111 searched++;
01112 } else if (bv_introduced[2*i]) {
01113 if (bv_introduced[2*i+1]) {
01114 funcdep++;
01115 } else {
01116 introduced++;
01117 }
01118 }
01119 }
01120 BoolVarArgs bv_sol(bv.size()-(introduced+funcdep+searched));
01121 BoolVarArgs bv_tmp(introduced);
01122 for (int i=bv.size(), j=0, k=0; i--;) {
01123 if (bv_searched[i])
01124 continue;
01125 if (bv_introduced[2*i]) {
01126 if (!bv_introduced[2*i+1]) {
01127 bv_tmp[j++] = bv[i];
01128 }
01129 } else {
01130 bv_sol[k++] = bv[i];
01131 }
01132 }
01133
01134 if (iv_sol.size() > 0)
01135 branch(*this, iv_sol, def_int_varsel, def_int_valsel);
01136 if (bv_sol.size() > 0)
01137 branch(*this, bv_sol, def_bool_varsel, def_bool_valsel);
01138 #ifdef GECODE_HAS_FLOAT_VARS
01139 introduced = 0;
01140 funcdep = 0;
01141 searched = 0;
01142 for (int i=fv.size(); i--;) {
01143 if (fv_searched[i]) {
01144 searched++;
01145 } else if (fv_introduced[2*i]) {
01146 if (fv_introduced[2*i+1]) {
01147 funcdep++;
01148 } else {
01149 introduced++;
01150 }
01151 }
01152 }
01153 FloatVarArgs fv_sol(fv.size()-(introduced+funcdep+searched));
01154 FloatVarArgs fv_tmp(introduced);
01155 for (int i=fv.size(), j=0, k=0; i--;) {
01156 if (fv_searched[i])
01157 continue;
01158 if (fv_introduced[2*i]) {
01159 if (!fv_introduced[2*i+1]) {
01160 fv_tmp[j++] = fv[i];
01161 }
01162 } else {
01163 fv_sol[k++] = fv[i];
01164 }
01165 }
01166
01167 if (fv_sol.size() > 0)
01168 branch(*this, fv_sol, def_float_varsel, def_float_valsel);
01169 #endif
01170 #ifdef GECODE_HAS_SET_VARS
01171 introduced = 0;
01172 funcdep = 0;
01173 searched = 0;
01174 for (int i=sv.size(); i--;) {
01175 if (sv_searched[i]) {
01176 searched++;
01177 } else if (sv_introduced[2*i]) {
01178 if (sv_introduced[2*i+1]) {
01179 funcdep++;
01180 } else {
01181 introduced++;
01182 }
01183 }
01184 }
01185 SetVarArgs sv_sol(sv.size()-(introduced+funcdep+searched));
01186 SetVarArgs sv_tmp(introduced);
01187 for (int i=sv.size(), j=0, k=0; i--;) {
01188 if (sv_searched[i])
01189 continue;
01190 if (sv_introduced[2*i]) {
01191 if (!sv_introduced[2*i+1]) {
01192 sv_tmp[j++] = sv[i];
01193 }
01194 } else {
01195 sv_sol[k++] = sv[i];
01196 }
01197 }
01198
01199 if (sv_sol.size() > 0)
01200 branch(*this, sv_sol, def_set_varsel, def_set_valsel);
01201 #endif
01202 iv_aux = IntVarArray(*this, iv_tmp);
01203 bv_aux = BoolVarArray(*this, bv_tmp);
01204 int n_aux = iv_aux.size() + bv_aux.size();
01205 #ifdef GECODE_HAS_SET_VARS
01206 sv_aux = SetVarArray(*this, sv_tmp);
01207 n_aux += sv_aux.size();
01208 #endif
01209 #ifdef GECODE_HAS_FLOAT_VARS
01210 fv_aux = FloatVarArray(*this, fv_tmp);
01211 n_aux += fv_aux.size();
01212 #endif
01213 if (n_aux > 0) {
01214 AuxVarBrancher::post(*this, def_int_varsel, def_int_valsel,
01215 def_bool_varsel, def_bool_valsel
01216 #ifdef GECODE_HAS_SET_VARS
01217 , def_set_varsel, def_set_valsel
01218 #endif
01219 #ifdef GECODE_HAS_FLOAT_VARS
01220 , def_float_varsel, def_float_valsel
01221 #endif
01222 );
01223 }
01224 }
01225
01226 AST::Array*
01227 FlatZincSpace::solveAnnotations(void) const {
01228 return _solveAnnotations;
01229 }
01230
01231 void
01232 FlatZincSpace::solve(AST::Array* ann) {
01233 _method = SAT;
01234 _solveAnnotations = ann;
01235 }
01236
01237 void
01238 FlatZincSpace::minimize(int var, bool isInt, AST::Array* ann) {
01239 _method = MIN;
01240 _optVar = var;
01241 _optVarIsInt = isInt;
01242
01243 AST::Call* c;
01244 if (isInt) {
01245 AST::Array* args = new AST::Array(4);
01246 args->a[0] = new AST::Array(new AST::IntVar(_optVar));
01247 args->a[1] = new AST::Atom("input_order");
01248 args->a[2] = new AST::Atom("indomain_min");
01249 args->a[3] = new AST::Atom("complete");
01250 c = new AST::Call("int_search", args);
01251 } else {
01252 AST::Array* args = new AST::Array(5);
01253 args->a[0] = new AST::Array(new AST::FloatVar(_optVar));
01254 args->a[1] = new AST::FloatLit(0.0);
01255 args->a[2] = new AST::Atom("input_order");
01256 args->a[3] = new AST::Atom("indomain_split");
01257 args->a[4] = new AST::Atom("complete");
01258 c = new AST::Call("float_search", args);
01259 }
01260 if (!ann)
01261 ann = new AST::Array(c);
01262 else
01263 ann->a.push_back(c);
01264 _solveAnnotations = ann;
01265 }
01266
01267 void
01268 FlatZincSpace::maximize(int var, bool isInt, AST::Array* ann) {
01269 _method = MAX;
01270 _optVar = var;
01271 _optVarIsInt = isInt;
01272
01273 AST::Call* c;
01274 if (isInt) {
01275 AST::Array* args = new AST::Array(4);
01276 args->a[0] = new AST::Array(new AST::IntVar(_optVar));
01277 args->a[1] = new AST::Atom("input_order");
01278 args->a[2] = new AST::Atom("indomain_max");
01279 args->a[3] = new AST::Atom("complete");
01280 c = new AST::Call("int_search", args);
01281 } else {
01282 AST::Array* args = new AST::Array(5);
01283 args->a[0] = new AST::Array(new AST::FloatVar(_optVar));
01284 args->a[1] = new AST::FloatLit(0.0);
01285 args->a[2] = new AST::Atom("input_order");
01286 args->a[3] = new AST::Atom("indomain_split_reverse");
01287 args->a[4] = new AST::Atom("complete");
01288 c = new AST::Call("float_search", args);
01289 }
01290 if (!ann)
01291 ann = new AST::Array(c);
01292 else
01293 ann->a.push_back(c);
01294 _solveAnnotations = ann;
01295 }
01296
01297 FlatZincSpace::~FlatZincSpace(void) {
01298 delete _solveAnnotations;
01299 }
01300
01301 #ifdef GECODE_HAS_GIST
01302
01306 template<class Engine>
01307 class GistEngine {
01308 };
01309
01311 template<typename S>
01312 class GistEngine<DFS<S> > {
01313 public:
01314 static void explore(S* root, const FlatZincOptions& opt,
01315 Gist::Inspector* i, Gist::Comparator* c) {
01316 Gecode::Gist::Options o;
01317 o.c_d = opt.c_d(); o.a_d = opt.a_d();
01318 o.inspect.click(i);
01319 o.inspect.compare(c);
01320 (void) Gecode::Gist::dfs(root, o);
01321 }
01322 };
01323
01325 template<typename S>
01326 class GistEngine<BAB<S> > {
01327 public:
01328 static void explore(S* root, const FlatZincOptions& opt,
01329 Gist::Inspector* i, Gist::Comparator* c) {
01330 Gecode::Gist::Options o;
01331 o.c_d = opt.c_d(); o.a_d = opt.a_d();
01332 o.inspect.click(i);
01333 o.inspect.compare(c);
01334 (void) Gecode::Gist::bab(root, o);
01335 }
01336 };
01337
01339 template<class S>
01340 class FZPrintingInspector
01341 : public Gecode::Gist::TextOutput, public Gecode::Gist::Inspector {
01342 private:
01343 const Printer& p;
01344 public:
01346 FZPrintingInspector(const Printer& p0);
01348 virtual void inspect(const Space& node);
01350 virtual void finalize(void);
01351 };
01352
01353 template<class S>
01354 FZPrintingInspector<S>::FZPrintingInspector(const Printer& p0)
01355 : TextOutput("Gecode/FlatZinc"), p(p0) {}
01356
01357 template<class S>
01358 void
01359 FZPrintingInspector<S>::inspect(const Space& node) {
01360 init();
01361 dynamic_cast<const S&>(node).print(getStream(), p);
01362 getStream() << std::endl;
01363 }
01364
01365 template<class S>
01366 void
01367 FZPrintingInspector<S>::finalize(void) {
01368 Gecode::Gist::TextOutput::finalize();
01369 }
01370
01371 template<class S>
01372 class FZPrintingComparator
01373 : public Gecode::Gist::VarComparator<S> {
01374 private:
01375 const Printer& p;
01376 public:
01378 FZPrintingComparator(const Printer& p0);
01379
01381 virtual void compare(const Space& s0, const Space& s1);
01382 };
01383
01384 template<class S>
01385 FZPrintingComparator<S>::FZPrintingComparator(const Printer& p0)
01386 : Gecode::Gist::VarComparator<S>("Gecode/FlatZinc"), p(p0) {}
01387
01388 template<class S>
01389 void
01390 FZPrintingComparator<S>::compare(const Space& s0, const Space& s1) {
01391 this->init();
01392 try {
01393 dynamic_cast<const S&>(s0).compare(dynamic_cast<const S&>(s1),
01394 this->getStream(), p);
01395 } catch (Exception& e) {
01396 this->getStream() << "Exception: " << e.what();
01397 }
01398 this->getStream() << std::endl;
01399 }
01400
01401 #endif
01402
01403
01404 template<template<class> class Engine>
01405 void
01406 FlatZincSpace::runEngine(std::ostream& out, const Printer& p,
01407 const FlatZincOptions& opt, Support::Timer& t_total) {
01408 if (opt.restart()==RM_NONE) {
01409 runMeta<Engine,Driver::EngineToMeta>(out,p,opt,t_total);
01410 } else {
01411 runMeta<Engine,RBS>(out,p,opt,t_total);
01412 }
01413 }
01414
01415 template<template<class> class Engine,
01416 template<template<class> class,class> class Meta>
01417 void
01418 FlatZincSpace::runMeta(std::ostream& out, const Printer& p,
01419 const FlatZincOptions& opt, Support::Timer& t_total) {
01420 #ifdef GECODE_HAS_GIST
01421 if (opt.mode() == SM_GIST) {
01422 FZPrintingInspector<FlatZincSpace> pi(p);
01423 FZPrintingComparator<FlatZincSpace> pc(p);
01424 (void) GistEngine<Engine<FlatZincSpace> >::explore(this,opt,&pi,&pc);
01425 return;
01426 }
01427 #endif
01428 StatusStatistics sstat;
01429 unsigned int n_p = 0;
01430 Support::Timer t_solve;
01431 t_solve.start();
01432 if (status(sstat) != SS_FAILED) {
01433 n_p = propagators();
01434 }
01435 Search::Options o;
01436 o.stop = Driver::CombinedStop::create(opt.node(), opt.fail(), opt.time(),
01437 true);
01438 o.c_d = opt.c_d();
01439 o.a_d = opt.a_d();
01440 o.threads = opt.threads();
01441 o.nogoods_limit = opt.nogoods() ? opt.nogoods_limit() : 0;
01442 o.cutoff = Driver::createCutoff(opt);
01443 if (opt.interrupt())
01444 Driver::CombinedStop::installCtrlHandler(true);
01445 Meta<Engine,FlatZincSpace> se(this,o);
01446 int noOfSolutions = _method == SAT ? opt.solutions() : 0;
01447 bool printAll = _method == SAT || opt.allSolutions();
01448 int findSol = noOfSolutions;
01449 FlatZincSpace* sol = NULL;
01450 while (FlatZincSpace* next_sol = se.next()) {
01451 delete sol;
01452 sol = next_sol;
01453 if (printAll) {
01454 sol->print(out, p);
01455 out << "----------" << std::endl;
01456 }
01457 if (--findSol==0)
01458 goto stopped;
01459 }
01460 if (sol && !printAll) {
01461 sol->print(out, p);
01462 out << "----------" << std::endl;
01463 }
01464 if (!se.stopped()) {
01465 if (sol) {
01466 out << "==========" << endl;
01467 } else {
01468 out << "=====UNSATISFIABLE=====" << endl;
01469 }
01470 } else if (!sol) {
01471 out << "=====UNKNOWN=====" << endl;
01472 }
01473 delete sol;
01474 stopped:
01475 if (opt.interrupt())
01476 Driver::CombinedStop::installCtrlHandler(false);
01477 if (opt.mode() == SM_STAT) {
01478 Gecode::Search::Statistics stat = se.statistics();
01479 out << endl
01480 << "%% runtime: ";
01481 Driver::stop(t_total,out);
01482 out << endl
01483 << "%% solvetime: ";
01484 Driver::stop(t_solve,out);
01485 out << endl
01486 << "%% solutions: "
01487 << std::abs(noOfSolutions - findSol) << endl
01488 << "%% variables: "
01489 << (intVarCount + boolVarCount + setVarCount) << endl
01490 << "%% propagators: " << n_p << endl
01491 << "%% propagations: " << sstat.propagate+stat.propagate << endl
01492 << "%% nodes: " << stat.node << endl
01493 << "%% failures: " << stat.fail << endl
01494 << "%% restarts: " << stat.restart << endl
01495 << "%% peak depth: " << stat.depth << endl
01496 << endl;
01497 }
01498 delete o.stop;
01499 }
01500
01501 #ifdef GECODE_HAS_QT
01502 void
01503 FlatZincSpace::branchWithPlugin(AST::Node* ann) {
01504 if (AST::Call* c = dynamic_cast<AST::Call*>(ann)) {
01505 QString pluginName(c->id.c_str());
01506 if (QLibrary::isLibrary(pluginName+".dll")) {
01507 pluginName += ".dll";
01508 } else if (QLibrary::isLibrary(pluginName+".dylib")) {
01509 pluginName = "lib" + pluginName + ".dylib";
01510 } else if (QLibrary::isLibrary(pluginName+".so")) {
01511
01512 pluginName = "lib" + pluginName + ".so";
01513 }
01514 QPluginLoader pl(pluginName);
01515 QObject* plugin_o = pl.instance();
01516 if (!plugin_o) {
01517 throw FlatZinc::Error("FlatZinc",
01518 "Error loading plugin "+pluginName.toStdString()+
01519 ": "+pl.errorString().toStdString());
01520 }
01521 BranchPlugin* pb = qobject_cast<BranchPlugin*>(plugin_o);
01522 if (!pb) {
01523 throw FlatZinc::Error("FlatZinc",
01524 "Error loading plugin "+pluginName.toStdString()+
01525 ": does not contain valid PluginBrancher");
01526 }
01527 pb->branch(*this, c);
01528 }
01529 }
01530 #else
01531 void
01532 FlatZincSpace::branchWithPlugin(AST::Node*) {
01533 throw FlatZinc::Error("FlatZinc",
01534 "Branching with plugins not supported (requires Qt support)");
01535 }
01536 #endif
01537
01538 void
01539 FlatZincSpace::run(std::ostream& out, const Printer& p,
01540 const FlatZincOptions& opt, Support::Timer& t_total) {
01541 switch (_method) {
01542 case MIN:
01543 case MAX:
01544 runEngine<BAB>(out,p,opt,t_total);
01545 break;
01546 case SAT:
01547 runEngine<DFS>(out,p,opt,t_total);
01548 break;
01549 }
01550 }
01551
01552 void
01553 FlatZincSpace::constrain(const Space& s) {
01554 if (_optVarIsInt) {
01555 if (_method == MIN)
01556 rel(*this, iv[_optVar], IRT_LE,
01557 static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
01558 else if (_method == MAX)
01559 rel(*this, iv[_optVar], IRT_GR,
01560 static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
01561 } else {
01562 #ifdef GECODE_HAS_FLOAT_VARS
01563 if (_method == MIN)
01564 rel(*this, fv[_optVar], FRT_LE,
01565 static_cast<const FlatZincSpace*>(&s)->fv[_optVar].val());
01566 else if (_method == MAX)
01567 rel(*this, fv[_optVar], FRT_GR,
01568 static_cast<const FlatZincSpace*>(&s)->fv[_optVar].val());
01569 #endif
01570 }
01571 }
01572
01573 Space*
01574 FlatZincSpace::copy(bool share) {
01575 return new FlatZincSpace(share, *this);
01576 }
01577
01578 FlatZincSpace::Meth
01579 FlatZincSpace::method(void) const {
01580 return _method;
01581 }
01582
01583 int
01584 FlatZincSpace::optVar(void) const {
01585 return _optVar;
01586 }
01587
01588 bool
01589 FlatZincSpace::optVarIsInt(void) const {
01590 return _optVarIsInt;
01591 }
01592
01593 void
01594 FlatZincSpace::print(std::ostream& out, const Printer& p) const {
01595 p.print(out, iv, bv
01596 #ifdef GECODE_HAS_SET_VARS
01597 , sv
01598 #endif
01599 #ifdef GECODE_HAS_FLOAT_VARS
01600 , fv
01601 #endif
01602 );
01603 }
01604
01605 void
01606 FlatZincSpace::compare(const Space& s, std::ostream& out) const {
01607 (void) s; (void) out;
01608 #ifdef GECODE_HAS_GIST
01609 const FlatZincSpace& fs = dynamic_cast<const FlatZincSpace&>(s);
01610 for (int i = 0; i < iv.size(); ++i) {
01611 std::stringstream ss;
01612 ss << "iv[" << i << "]";
01613 std::string result(Gecode::Gist::Comparator::compare(ss.str(), iv[i],
01614 fs.iv[i]));
01615 if (result.length() > 0) out << result << std::endl;
01616 }
01617 for (int i = 0; i < bv.size(); ++i) {
01618 std::stringstream ss;
01619 ss << "bv[" << i << "]";
01620 std::string result(Gecode::Gist::Comparator::compare(ss.str(), bv[i],
01621 fs.bv[i]));
01622 if (result.length() > 0) out << result << std::endl;
01623 }
01624 #ifdef GECODE_HAS_SET_VARS
01625 for (int i = 0; i < sv.size(); ++i) {
01626 std::stringstream ss;
01627 ss << "sv[" << i << "]";
01628 std::string result(Gecode::Gist::Comparator::compare(ss.str(), sv[i],
01629 fs.sv[i]));
01630 if (result.length() > 0) out << result << std::endl;
01631 }
01632 #endif
01633 #ifdef GECODE_HAS_FLOAT_VARS
01634 for (int i = 0; i < fv.size(); ++i) {
01635 std::stringstream ss;
01636 ss << "fv[" << i << "]";
01637 std::string result(Gecode::Gist::Comparator::compare(ss.str(), fv[i],
01638 fs.fv[i]));
01639 if (result.length() > 0) out << result << std::endl;
01640 }
01641 #endif
01642 #endif
01643 }
01644
01645 void
01646 FlatZincSpace::compare(const FlatZincSpace& s, std::ostream& out,
01647 const Printer& p) const {
01648 p.printDiff(out, iv, s.iv, bv, s.bv
01649 #ifdef GECODE_HAS_SET_VARS
01650 , sv, s.sv
01651 #endif
01652 #ifdef GECODE_HAS_FLOAT_VARS
01653 , fv, s.fv
01654 #endif
01655 );
01656 }
01657
01658 void
01659 FlatZincSpace::shrinkArrays(Printer& p) {
01660 p.shrinkArrays(*this, _optVar, _optVarIsInt, iv, bv
01661 #ifdef GECODE_HAS_SET_VARS
01662 , sv
01663 #endif
01664 #ifdef GECODE_HAS_FLOAT_VARS
01665 , fv
01666 #endif
01667 );
01668 }
01669
01670 IntArgs
01671 FlatZincSpace::arg2intargs(AST::Node* arg, int offset) {
01672 AST::Array* a = arg->getArray();
01673 IntArgs ia(a->a.size()+offset);
01674 for (int i=offset; i--;)
01675 ia[i] = 0;
01676 for (int i=a->a.size(); i--;)
01677 ia[i+offset] = a->a[i]->getInt();
01678 return ia;
01679 }
01680 IntArgs
01681 FlatZincSpace::arg2boolargs(AST::Node* arg, int offset) {
01682 AST::Array* a = arg->getArray();
01683 IntArgs ia(a->a.size()+offset);
01684 for (int i=offset; i--;)
01685 ia[i] = 0;
01686 for (int i=a->a.size(); i--;)
01687 ia[i+offset] = a->a[i]->getBool();
01688 return ia;
01689 }
01690 IntSet
01691 FlatZincSpace::arg2intset(AST::Node* n) {
01692 AST::SetLit* sl = n->getSet();
01693 IntSet d;
01694 if (sl->interval) {
01695 d = IntSet(sl->min, sl->max);
01696 } else {
01697 Region re(*this);
01698 int* is = re.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
01699 for (int i=sl->s.size(); i--; )
01700 is[i] = sl->s[i];
01701 d = IntSet(is, sl->s.size());
01702 }
01703 return d;
01704 }
01705 IntSetArgs
01706 FlatZincSpace::arg2intsetargs(AST::Node* arg, int offset) {
01707 AST::Array* a = arg->getArray();
01708 if (a->a.size() == 0) {
01709 IntSetArgs emptyIa(0);
01710 return emptyIa;
01711 }
01712 IntSetArgs ia(a->a.size()+offset);
01713 for (int i=offset; i--;)
01714 ia[i] = IntSet::empty;
01715 for (int i=a->a.size(); i--;) {
01716 ia[i+offset] = arg2intset(a->a[i]);
01717 }
01718 return ia;
01719 }
01720 IntVarArgs
01721 FlatZincSpace::arg2intvarargs(AST::Node* arg, int offset) {
01722 AST::Array* a = arg->getArray();
01723 if (a->a.size() == 0) {
01724 IntVarArgs emptyIa(0);
01725 return emptyIa;
01726 }
01727 IntVarArgs ia(a->a.size()+offset);
01728 for (int i=offset; i--;)
01729 ia[i] = IntVar(*this, 0, 0);
01730 for (int i=a->a.size(); i--;) {
01731 if (a->a[i]->isIntVar()) {
01732 ia[i+offset] = iv[a->a[i]->getIntVar()];
01733 } else {
01734 int value = a->a[i]->getInt();
01735 IntVar iv(*this, value, value);
01736 ia[i+offset] = iv;
01737 }
01738 }
01739 return ia;
01740 }
01741 BoolVarArgs
01742 FlatZincSpace::arg2boolvarargs(AST::Node* arg, int offset, int siv) {
01743 AST::Array* a = arg->getArray();
01744 if (a->a.size() == 0) {
01745 BoolVarArgs emptyIa(0);
01746 return emptyIa;
01747 }
01748 BoolVarArgs ia(a->a.size()+offset-(siv==-1?0:1));
01749 for (int i=offset; i--;)
01750 ia[i] = BoolVar(*this, 0, 0);
01751 for (int i=0; i<static_cast<int>(a->a.size()); i++) {
01752 if (i==siv)
01753 continue;
01754 if (a->a[i]->isBool()) {
01755 bool value = a->a[i]->getBool();
01756 BoolVar iv(*this, value, value);
01757 ia[offset++] = iv;
01758 } else if (a->a[i]->isIntVar() &&
01759 aliasBool2Int(a->a[i]->getIntVar()) != -1) {
01760 ia[offset++] = bv[aliasBool2Int(a->a[i]->getIntVar())];
01761 } else {
01762 ia[offset++] = bv[a->a[i]->getBoolVar()];
01763 }
01764 }
01765 return ia;
01766 }
01767 BoolVar
01768 FlatZincSpace::arg2BoolVar(AST::Node* n) {
01769 BoolVar x0;
01770 if (n->isBool()) {
01771 x0 = BoolVar(*this, n->getBool(), n->getBool());
01772 }
01773 else {
01774 x0 = bv[n->getBoolVar()];
01775 }
01776 return x0;
01777 }
01778 IntVar
01779 FlatZincSpace::arg2IntVar(AST::Node* n) {
01780 IntVar x0;
01781 if (n->isIntVar()) {
01782 x0 = iv[n->getIntVar()];
01783 } else {
01784 x0 = IntVar(*this, n->getInt(), n->getInt());
01785 }
01786 return x0;
01787 }
01788 bool
01789 FlatZincSpace::isBoolArray(AST::Node* b, int& singleInt) {
01790 AST::Array* a = b->getArray();
01791 singleInt = -1;
01792 if (a->a.size() == 0)
01793 return true;
01794 for (int i=a->a.size(); i--;) {
01795 if (a->a[i]->isBoolVar() || a->a[i]->isBool()) {
01796 } else if (a->a[i]->isIntVar()) {
01797 if (aliasBool2Int(a->a[i]->getIntVar()) == -1) {
01798 if (singleInt != -1) {
01799 return false;
01800 }
01801 singleInt = i;
01802 }
01803 } else {
01804 return false;
01805 }
01806 }
01807 return singleInt==-1 || a->a.size() > 1;
01808 }
01809 #ifdef GECODE_HAS_SET_VARS
01810 SetVar
01811 FlatZincSpace::arg2SetVar(AST::Node* n) {
01812 SetVar x0;
01813 if (!n->isSetVar()) {
01814 IntSet d = arg2intset(n);
01815 x0 = SetVar(*this, d, d);
01816 } else {
01817 x0 = sv[n->getSetVar()];
01818 }
01819 return x0;
01820 }
01821 SetVarArgs
01822 FlatZincSpace::arg2setvarargs(AST::Node* arg, int offset, int doffset,
01823 const IntSet& od) {
01824 AST::Array* a = arg->getArray();
01825 SetVarArgs ia(a->a.size()+offset);
01826 for (int i=offset; i--;) {
01827 IntSet d = i<doffset ? od : IntSet::empty;
01828 ia[i] = SetVar(*this, d, d);
01829 }
01830 for (int i=a->a.size(); i--;) {
01831 ia[i+offset] = arg2SetVar(a->a[i]);
01832 }
01833 return ia;
01834 }
01835 #endif
01836 #ifdef GECODE_HAS_FLOAT_VARS
01837 FloatValArgs
01838 FlatZincSpace::arg2floatargs(AST::Node* arg, int offset) {
01839 AST::Array* a = arg->getArray();
01840 FloatValArgs fa(a->a.size()+offset);
01841 for (int i=offset; i--;)
01842 fa[i] = 0.0;
01843 for (int i=a->a.size(); i--;)
01844 fa[i+offset] = a->a[i]->getFloat();
01845 return fa;
01846 }
01847 FloatVarArgs
01848 FlatZincSpace::arg2floatvarargs(AST::Node* arg, int offset) {
01849 AST::Array* a = arg->getArray();
01850 if (a->a.size() == 0) {
01851 FloatVarArgs emptyFa(0);
01852 return emptyFa;
01853 }
01854 FloatVarArgs fa(a->a.size()+offset);
01855 for (int i=offset; i--;)
01856 fa[i] = FloatVar(*this, 0.0, 0.0);
01857 for (int i=a->a.size(); i--;) {
01858 if (a->a[i]->isFloatVar()) {
01859 fa[i+offset] = fv[a->a[i]->getFloatVar()];
01860 } else {
01861 double value = a->a[i]->getFloat();
01862 FloatVar fv(*this, value, value);
01863 fa[i+offset] = fv;
01864 }
01865 }
01866 return fa;
01867 }
01868 FloatVar
01869 FlatZincSpace::arg2FloatVar(AST::Node* n) {
01870 FloatVar x0;
01871 if (n->isFloatVar()) {
01872 x0 = fv[n->getFloatVar()];
01873 } else {
01874 x0 = FloatVar(*this, n->getFloat(), n->getFloat());
01875 }
01876 return x0;
01877 }
01878 #endif
01879 IntConLevel
01880 FlatZincSpace::ann2icl(AST::Node* ann) {
01881 if (ann) {
01882 if (ann->hasAtom("val"))
01883 return ICL_VAL;
01884 if (ann->hasAtom("domain"))
01885 return ICL_DOM;
01886 if (ann->hasAtom("bounds") ||
01887 ann->hasAtom("boundsR") ||
01888 ann->hasAtom("boundsD") ||
01889 ann->hasAtom("boundsZ"))
01890 return ICL_BND;
01891 }
01892 return ICL_DEF;
01893 }
01894
01895
01896 void
01897 Printer::init(AST::Array* output) {
01898 _output = output;
01899 }
01900
01901 void
01902 Printer::printElem(std::ostream& out,
01903 AST::Node* ai,
01904 const Gecode::IntVarArray& iv,
01905 const Gecode::BoolVarArray& bv
01906 #ifdef GECODE_HAS_SET_VARS
01907 , const Gecode::SetVarArray& sv
01908 #endif
01909 #ifdef GECODE_HAS_FLOAT_VARS
01910 ,
01911 const Gecode::FloatVarArray& fv
01912 #endif
01913 ) const {
01914 int k;
01915 if (ai->isInt(k)) {
01916 out << k;
01917 } else if (ai->isIntVar()) {
01918 out << iv[ai->getIntVar()];
01919 } else if (ai->isBoolVar()) {
01920 if (bv[ai->getBoolVar()].min() == 1) {
01921 out << "true";
01922 } else if (bv[ai->getBoolVar()].max() == 0) {
01923 out << "false";
01924 } else {
01925 out << "false..true";
01926 }
01927 #ifdef GECODE_HAS_SET_VARS
01928 } else if (ai->isSetVar()) {
01929 if (!sv[ai->getSetVar()].assigned()) {
01930 out << sv[ai->getSetVar()];
01931 return;
01932 }
01933 SetVarGlbRanges svr(sv[ai->getSetVar()]);
01934 if (!svr()) {
01935 out << "{}";
01936 return;
01937 }
01938 int min = svr.min();
01939 int max = svr.max();
01940 ++svr;
01941 if (svr()) {
01942 SetVarGlbValues svv(sv[ai->getSetVar()]);
01943 int i = svv.val();
01944 out << "{" << i;
01945 ++svv;
01946 for (; svv(); ++svv)
01947 out << ", " << svv.val();
01948 out << "}";
01949 } else {
01950 out << min << ".." << max;
01951 }
01952 #endif
01953 #ifdef GECODE_HAS_FLOAT_VARS
01954 } else if (ai->isFloatVar()) {
01955 if (fv[ai->getFloatVar()].assigned()) {
01956 FloatVal vv = fv[ai->getFloatVar()].val();
01957 FloatNum v;
01958 if (vv.singleton())
01959 v = vv.min();
01960 else if (vv < 0.0)
01961 v = vv.max();
01962 else
01963 v = vv.min();
01964 std::ostringstream oss;
01965
01966 oss << std::setprecision(std::numeric_limits<double>::digits10);
01967 oss << v;
01968 if (oss.str().find(".") == std::string::npos)
01969 oss << ".0";
01970 out << oss.str();
01971 } else {
01972 out << fv[ai->getFloatVar()];
01973 }
01974 #endif
01975 } else if (ai->isBool()) {
01976 out << (ai->getBool() ? "true" : "false");
01977 } else if (ai->isSet()) {
01978 AST::SetLit* s = ai->getSet();
01979 if (s->interval) {
01980 out << s->min << ".." << s->max;
01981 } else {
01982 out << "{";
01983 for (unsigned int i=0; i<s->s.size(); i++) {
01984 out << s->s[i] << (i < s->s.size()-1 ? ", " : "}");
01985 }
01986 }
01987 } else if (ai->isString()) {
01988 std::string s = ai->getString();
01989 for (unsigned int i=0; i<s.size(); i++) {
01990 if (s[i] == '\\' && i<s.size()-1) {
01991 switch (s[i+1]) {
01992 case 'n': out << "\n"; break;
01993 case '\\': out << "\\"; break;
01994 case 't': out << "\t"; break;
01995 default: out << "\\" << s[i+1];
01996 }
01997 i++;
01998 } else {
01999 out << s[i];
02000 }
02001 }
02002 }
02003 }
02004
02005 void
02006 Printer::printElemDiff(std::ostream& out,
02007 AST::Node* ai,
02008 const Gecode::IntVarArray& iv1,
02009 const Gecode::IntVarArray& iv2,
02010 const Gecode::BoolVarArray& bv1,
02011 const Gecode::BoolVarArray& bv2
02012 #ifdef GECODE_HAS_SET_VARS
02013 , const Gecode::SetVarArray& sv1,
02014 const Gecode::SetVarArray& sv2
02015 #endif
02016 #ifdef GECODE_HAS_FLOAT_VARS
02017 , const Gecode::FloatVarArray& fv1,
02018 const Gecode::FloatVarArray& fv2
02019 #endif
02020 ) const {
02021 #ifdef GECODE_HAS_GIST
02022 using namespace Gecode::Gist;
02023 int k;
02024 if (ai->isInt(k)) {
02025 out << k;
02026 } else if (ai->isIntVar()) {
02027 std::string res(Comparator::compare("",iv1[ai->getIntVar()],
02028 iv2[ai->getIntVar()]));
02029 if (res.length() > 0) {
02030 res.erase(0, 1);
02031 out << res;
02032 } else {
02033 out << iv1[ai->getIntVar()];
02034 }
02035 } else if (ai->isBoolVar()) {
02036 std::string res(Comparator::compare("",bv1[ai->getBoolVar()],
02037 bv2[ai->getBoolVar()]));
02038 if (res.length() > 0) {
02039 res.erase(0, 1);
02040 out << res;
02041 } else {
02042 out << bv1[ai->getBoolVar()];
02043 }
02044 #ifdef GECODE_HAS_SET_VARS
02045 } else if (ai->isSetVar()) {
02046 std::string res(Comparator::compare("",sv1[ai->getSetVar()],
02047 sv2[ai->getSetVar()]));
02048 if (res.length() > 0) {
02049 res.erase(0, 1);
02050 out << res;
02051 } else {
02052 out << sv1[ai->getSetVar()];
02053 }
02054 #endif
02055 #ifdef GECODE_HAS_FLOAT_VARS
02056 } else if (ai->isFloatVar()) {
02057 std::string res(Comparator::compare("",fv1[ai->getFloatVar()],
02058 fv2[ai->getFloatVar()]));
02059 if (res.length() > 0) {
02060 res.erase(0, 1);
02061 out << res;
02062 } else {
02063 out << fv1[ai->getFloatVar()];
02064 }
02065 #endif
02066 } else if (ai->isBool()) {
02067 out << (ai->getBool() ? "true" : "false");
02068 } else if (ai->isSet()) {
02069 AST::SetLit* s = ai->getSet();
02070 if (s->interval) {
02071 out << s->min << ".." << s->max;
02072 } else {
02073 out << "{";
02074 for (unsigned int i=0; i<s->s.size(); i++) {
02075 out << s->s[i] << (i < s->s.size()-1 ? ", " : "}");
02076 }
02077 }
02078 } else if (ai->isString()) {
02079 std::string s = ai->getString();
02080 for (unsigned int i=0; i<s.size(); i++) {
02081 if (s[i] == '\\' && i<s.size()-1) {
02082 switch (s[i+1]) {
02083 case 'n': out << "\n"; break;
02084 case '\\': out << "\\"; break;
02085 case 't': out << "\t"; break;
02086 default: out << "\\" << s[i+1];
02087 }
02088 i++;
02089 } else {
02090 out << s[i];
02091 }
02092 }
02093 }
02094 #endif
02095 }
02096
02097 void
02098 Printer::print(std::ostream& out,
02099 const Gecode::IntVarArray& iv,
02100 const Gecode::BoolVarArray& bv
02101 #ifdef GECODE_HAS_SET_VARS
02102 ,
02103 const Gecode::SetVarArray& sv
02104 #endif
02105 #ifdef GECODE_HAS_FLOAT_VARS
02106 ,
02107 const Gecode::FloatVarArray& fv
02108 #endif
02109 ) const {
02110 if (_output == NULL)
02111 return;
02112 for (unsigned int i=0; i< _output->a.size(); i++) {
02113 AST::Node* ai = _output->a[i];
02114 if (ai->isArray()) {
02115 AST::Array* aia = ai->getArray();
02116 int size = aia->a.size();
02117 out << "[";
02118 for (int j=0; j<size; j++) {
02119 printElem(out,aia->a[j],iv,bv
02120 #ifdef GECODE_HAS_SET_VARS
02121 ,sv
02122 #endif
02123 #ifdef GECODE_HAS_FLOAT_VARS
02124 ,fv
02125 #endif
02126 );
02127 if (j<size-1)
02128 out << ", ";
02129 }
02130 out << "]";
02131 } else {
02132 printElem(out,ai,iv,bv
02133 #ifdef GECODE_HAS_SET_VARS
02134 ,sv
02135 #endif
02136 #ifdef GECODE_HAS_FLOAT_VARS
02137 ,fv
02138 #endif
02139 );
02140 }
02141 }
02142 }
02143
02144 void
02145 Printer::printDiff(std::ostream& out,
02146 const Gecode::IntVarArray& iv1,
02147 const Gecode::IntVarArray& iv2,
02148 const Gecode::BoolVarArray& bv1,
02149 const Gecode::BoolVarArray& bv2
02150 #ifdef GECODE_HAS_SET_VARS
02151 ,
02152 const Gecode::SetVarArray& sv1,
02153 const Gecode::SetVarArray& sv2
02154 #endif
02155 #ifdef GECODE_HAS_FLOAT_VARS
02156 ,
02157 const Gecode::FloatVarArray& fv1,
02158 const Gecode::FloatVarArray& fv2
02159 #endif
02160 ) const {
02161 if (_output == NULL)
02162 return;
02163 for (unsigned int i=0; i< _output->a.size(); i++) {
02164 AST::Node* ai = _output->a[i];
02165 if (ai->isArray()) {
02166 AST::Array* aia = ai->getArray();
02167 int size = aia->a.size();
02168 out << "[";
02169 for (int j=0; j<size; j++) {
02170 printElemDiff(out,aia->a[j],iv1,iv2,bv1,bv2
02171 #ifdef GECODE_HAS_SET_VARS
02172 ,sv1,sv2
02173 #endif
02174 #ifdef GECODE_HAS_FLOAT_VARS
02175 ,fv1,fv2
02176 #endif
02177 );
02178 if (j<size-1)
02179 out << ", ";
02180 }
02181 out << "]";
02182 } else {
02183 printElemDiff(out,ai,iv1,iv2,bv1,bv2
02184 #ifdef GECODE_HAS_SET_VARS
02185 ,sv1,sv2
02186 #endif
02187 #ifdef GECODE_HAS_FLOAT_VARS
02188 ,fv1,fv2
02189 #endif
02190 );
02191 }
02192 }
02193 }
02194
02195 void
02196 Printer::shrinkElement(AST::Node* node,
02197 std::map<int,int>& iv, std::map<int,int>& bv,
02198 std::map<int,int>& sv, std::map<int,int>& fv) {
02199 if (node->isIntVar()) {
02200 AST::IntVar* x = static_cast<AST::IntVar*>(node);
02201 if (iv.find(x->i) == iv.end()) {
02202 int newi = iv.size();
02203 iv[x->i] = newi;
02204 }
02205 x->i = iv[x->i];
02206 } else if (node->isBoolVar()) {
02207 AST::BoolVar* x = static_cast<AST::BoolVar*>(node);
02208 if (bv.find(x->i) == bv.end()) {
02209 int newi = bv.size();
02210 bv[x->i] = newi;
02211 }
02212 x->i = bv[x->i];
02213 } else if (node->isSetVar()) {
02214 AST::SetVar* x = static_cast<AST::SetVar*>(node);
02215 if (sv.find(x->i) == sv.end()) {
02216 int newi = sv.size();
02217 sv[x->i] = newi;
02218 }
02219 x->i = sv[x->i];
02220 } else if (node->isFloatVar()) {
02221 AST::FloatVar* x = static_cast<AST::FloatVar*>(node);
02222 if (fv.find(x->i) == fv.end()) {
02223 int newi = fv.size();
02224 fv[x->i] = newi;
02225 }
02226 x->i = fv[x->i];
02227 }
02228 }
02229
02230 void
02231 Printer::shrinkArrays(Space& home,
02232 int& optVar, bool optVarIsInt,
02233 Gecode::IntVarArray& iv,
02234 Gecode::BoolVarArray& bv
02235 #ifdef GECODE_HAS_SET_VARS
02236 ,
02237 Gecode::SetVarArray& sv
02238 #endif
02239 #ifdef GECODE_HAS_FLOAT_VARS
02240 ,
02241 Gecode::FloatVarArray& fv
02242 #endif
02243 ) {
02244 if (_output == NULL) {
02245 if (optVarIsInt && optVar != -1) {
02246 IntVar ov = iv[optVar];
02247 iv = IntVarArray(home, 1);
02248 iv[0] = ov;
02249 optVar = 0;
02250 } else {
02251 iv = IntVarArray(home, 0);
02252 }
02253 bv = BoolVarArray(home, 0);
02254 #ifdef GECODE_HAS_SET_VARS
02255 sv = SetVarArray(home, 0);
02256 #endif
02257 #ifdef GECODE_HAS_FLOAT_VARS
02258 if (!optVarIsInt && optVar != -1) {
02259 FloatVar ov = fv[optVar];
02260 fv = FloatVarArray(home, 1);
02261 fv[0] = ov;
02262 optVar = 0;
02263 } else {
02264 fv = FloatVarArray(home,0);
02265 }
02266 #endif
02267 return;
02268 }
02269 std::map<int,int> iv_new;
02270 std::map<int,int> bv_new;
02271 std::map<int,int> sv_new;
02272 std::map<int,int> fv_new;
02273
02274 if (optVar != -1) {
02275 if (optVarIsInt)
02276 iv_new[optVar] = 0;
02277 else
02278 fv_new[optVar] = 0;
02279 optVar = 0;
02280 }
02281
02282 for (unsigned int i=0; i< _output->a.size(); i++) {
02283 AST::Node* ai = _output->a[i];
02284 if (ai->isArray()) {
02285 AST::Array* aia = ai->getArray();
02286 for (unsigned int j=0; j<aia->a.size(); j++) {
02287 shrinkElement(aia->a[j],iv_new,bv_new,sv_new,fv_new);
02288 }
02289 } else {
02290 shrinkElement(ai,iv_new,bv_new,sv_new,fv_new);
02291 }
02292 }
02293
02294 IntVarArgs iva(iv_new.size());
02295 for (map<int,int>::iterator i=iv_new.begin(); i != iv_new.end(); ++i) {
02296 iva[(*i).second] = iv[(*i).first];
02297 }
02298 iv = IntVarArray(home, iva);
02299
02300 BoolVarArgs bva(bv_new.size());
02301 for (map<int,int>::iterator i=bv_new.begin(); i != bv_new.end(); ++i) {
02302 bva[(*i).second] = bv[(*i).first];
02303 }
02304 bv = BoolVarArray(home, bva);
02305
02306 #ifdef GECODE_HAS_SET_VARS
02307 SetVarArgs sva(sv_new.size());
02308 for (map<int,int>::iterator i=sv_new.begin(); i != sv_new.end(); ++i) {
02309 sva[(*i).second] = sv[(*i).first];
02310 }
02311 sv = SetVarArray(home, sva);
02312 #endif
02313
02314 #ifdef GECODE_HAS_FLOAT_VARS
02315 FloatVarArgs fva(fv_new.size());
02316 for (map<int,int>::iterator i=fv_new.begin(); i != fv_new.end(); ++i) {
02317 fva[(*i).second] = fv[(*i).first];
02318 }
02319 fv = FloatVarArray(home, fva);
02320 #endif
02321 }
02322
02323 Printer::~Printer(void) {
02324 delete _output;
02325 }
02326
02327 }}
02328
02329