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