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 #ifndef __GECODE_FLATZINC_HH__
00039 #define __GECODE_FLATZINC_HH__
00040
00041 #include <iostream>
00042
00043 #include <gecode/kernel.hh>
00044 #include <gecode/int.hh>
00045 #ifdef GECODE_HAS_SET_VARS
00046 #include <gecode/set.hh>
00047 #endif
00048 #ifdef GECODE_HAS_FLOAT_VARS
00049 #include <gecode/float.hh>
00050 #endif
00051 #include <map>
00052
00053
00054
00055
00056
00057
00058 #if !defined(GECODE_STATIC_LIBS) && \
00059 (defined(__CYGWIN__) || defined(__MINGW32__) || defined(_MSC_VER))
00060
00061 #ifdef GECODE_BUILD_FLATZINC
00062 #define GECODE_FLATZINC_EXPORT __declspec( dllexport )
00063 #else
00064 #define GECODE_FLATZINC_EXPORT __declspec( dllimport )
00065 #endif
00066
00067 #else
00068
00069 #ifdef GECODE_GCC_HAS_CLASS_VISIBILITY
00070
00071 #define GECODE_FLATZINC_EXPORT __attribute__ ((visibility("default")))
00072
00073 #else
00074
00075 #define GECODE_FLATZINC_EXPORT
00076
00077 #endif
00078 #endif
00079
00080
00081 #ifndef GECODE_BUILD_FLATZINC
00082 #define GECODE_LIBRARY_NAME "FlatZinc"
00083 #include <gecode/support/auto-link.hpp>
00084 #endif
00085
00086 #include <gecode/driver.hh>
00087
00088 #include <gecode/flatzinc/conexpr.hh>
00089 #include <gecode/flatzinc/ast.hh>
00090 #include <gecode/flatzinc/varspec.hh>
00091
00101 namespace Gecode { namespace FlatZinc {
00102
00107 class GECODE_FLATZINC_EXPORT Printer {
00108 private:
00110 std::vector<std::string> iv_names;
00112 std::vector<std::string> bv_names;
00113 #ifdef GECODE_HAS_FLOAT_VARS
00114
00115 std::vector<std::string> fv_names;
00116 #endif
00117 #ifdef GECODE_HAS_SET_VARS
00118
00119 std::vector<std::string> sv_names;
00120 #endif
00121 AST::Array* _output;
00122 void printElem(std::ostream& out,
00123 AST::Node* ai,
00124 const Gecode::IntVarArray& iv,
00125 const Gecode::BoolVarArray& bv
00126 #ifdef GECODE_HAS_SET_VARS
00127 ,
00128 const Gecode::SetVarArray& sv
00129 #endif
00130 #ifdef GECODE_HAS_FLOAT_VARS
00131 ,
00132 const Gecode::FloatVarArray& fv
00133 #endif
00134 ) const;
00135 void printElemDiff(std::ostream& out,
00136 AST::Node* ai,
00137 const Gecode::IntVarArray& iv1,
00138 const Gecode::IntVarArray& iv2,
00139 const Gecode::BoolVarArray& bv1,
00140 const Gecode::BoolVarArray& bv2
00141 #ifdef GECODE_HAS_SET_VARS
00142 ,
00143 const Gecode::SetVarArray& sv1,
00144 const Gecode::SetVarArray& sv2
00145 #endif
00146 #ifdef GECODE_HAS_FLOAT_VARS
00147 ,
00148 const Gecode::FloatVarArray& fv1,
00149 const Gecode::FloatVarArray& fv2
00150 #endif
00151 ) const;
00152 public:
00153 Printer(void) : _output(NULL) {}
00154 void init(AST::Array* output);
00155
00156 void print(std::ostream& out,
00157 const Gecode::IntVarArray& iv,
00158 const Gecode::BoolVarArray& bv
00159 #ifdef GECODE_HAS_SET_VARS
00160 ,
00161 const Gecode::SetVarArray& sv
00162 #endif
00163 #ifdef GECODE_HAS_FLOAT_VARS
00164 ,
00165 const Gecode::FloatVarArray& fv
00166 #endif
00167 ) const;
00168
00169 void printDiff(std::ostream& out,
00170 const Gecode::IntVarArray& iv1, const Gecode::IntVarArray& iv2,
00171 const Gecode::BoolVarArray& bv1, const Gecode::BoolVarArray& bv2
00172 #ifdef GECODE_HAS_SET_VARS
00173 ,
00174 const Gecode::SetVarArray& sv1, const Gecode::SetVarArray& sv2
00175 #endif
00176 #ifdef GECODE_HAS_FLOAT_VARS
00177 ,
00178 const Gecode::FloatVarArray& fv1,
00179 const Gecode::FloatVarArray& fv2
00180 #endif
00181 ) const;
00182
00183
00184 ~Printer(void);
00185
00186 void addIntVarName(const std::string& n);
00187 const std::string& intVarName(int i) const { return iv_names[i]; }
00188 void addBoolVarName(const std::string& n);
00189 const std::string& boolVarName(int i) const { return bv_names[i]; }
00190 #ifdef GECODE_HAS_FLOAT_VARS
00191 void addFloatVarName(const std::string& n);
00192 const std::string& floatVarName(int i) const { return fv_names[i]; }
00193 #endif
00194 #ifdef GECODE_HAS_SET_VARS
00195 void addSetVarName(const std::string& n);
00196 const std::string& setVarName(int i) const { return sv_names[i]; }
00197 #endif
00198
00199 void shrinkElement(AST::Node* node,
00200 std::map<int,int>& iv, std::map<int,int>& bv,
00201 std::map<int,int>& sv, std::map<int,int>& fv);
00202
00203 void shrinkArrays(Space& home,
00204 int& optVar, bool optVarIsInt,
00205 Gecode::IntVarArray& iv,
00206 Gecode::BoolVarArray& bv
00207 #ifdef GECODE_HAS_SET_VARS
00208 ,
00209 Gecode::SetVarArray& sv
00210 #endif
00211 #ifdef GECODE_HAS_FLOAT_VARS
00212 ,
00213 Gecode::FloatVarArray& fv
00214 #endif
00215 );
00216
00217 private:
00218 Printer(const Printer&);
00219 Printer& operator=(const Printer&);
00220 };
00221
00226 class FlatZincOptions : public Gecode::BaseOptions {
00227 protected:
00229
00230 Gecode::Driver::IntOption _solutions;
00231 Gecode::Driver::BoolOption _allSolutions;
00232 Gecode::Driver::DoubleOption _threads;
00233 Gecode::Driver::BoolOption _free;
00234 Gecode::Driver::DoubleOption _decay;
00235 Gecode::Driver::UnsignedIntOption _c_d;
00236 Gecode::Driver::UnsignedIntOption _a_d;
00237 Gecode::Driver::UnsignedIntOption _node;
00238 Gecode::Driver::UnsignedIntOption _fail;
00239 Gecode::Driver::UnsignedIntOption _time;
00240 Gecode::Driver::UnsignedIntOption _time_limit;
00241 Gecode::Driver::IntOption _seed;
00242 Gecode::Driver::StringOption _restart;
00243 Gecode::Driver::DoubleOption _r_base;
00244 Gecode::Driver::UnsignedIntOption _r_scale;
00245 Gecode::Driver::BoolOption _nogoods;
00246 Gecode::Driver::UnsignedIntOption _nogoods_limit;
00247 Gecode::Driver::BoolOption _interrupt;
00248 Gecode::Driver::DoubleOption _step;
00249
00250
00252
00253 Gecode::Driver::StringOption _mode;
00254 Gecode::Driver::BoolOption _stat;
00255 Gecode::Driver::StringValueOption _output;
00256
00257 #ifdef GECODE_HAS_CPPROFILER
00258
00259 Gecode::Driver::IntOption _profiler_id;
00260 Gecode::Driver::UnsignedIntOption _profiler_port;
00261 Gecode::Driver::BoolOption _profiler_info;
00262
00263 #endif
00264
00266 public:
00268 FlatZincOptions(const char* s)
00269 : Gecode::BaseOptions(s),
00270 _solutions("n","number of solutions (0 = all, -1 = one/best)",-1),
00271 _allSolutions("a", "return all solutions (equal to -n 0)"),
00272 _threads("p","number of threads (0 = #processing units)",
00273 Gecode::Search::Config::threads),
00274 _free("f", "free search, no need to follow search-specification"),
00275 _decay("decay","decay factor",0.99),
00276 _c_d("c-d","recomputation commit distance",Gecode::Search::Config::c_d),
00277 _a_d("a-d","recomputation adaption distance",Gecode::Search::Config::a_d),
00278 _node("node","node cutoff (0 = none, solution mode)"),
00279 _fail("fail","failure cutoff (0 = none, solution mode)"),
00280 _time("time","time (in ms) cutoff (0 = none, solution mode)"),
00281 _time_limit("t","time (in ms) cutoff (0 = none, solution mode)"),
00282 _seed("r","random seed",0),
00283 _restart("restart","restart sequence type",RM_NONE),
00284 _r_base("restart-base","base for geometric restart sequence",1.5),
00285 _r_scale("restart-scale","scale factor for restart sequence",250),
00286 _nogoods("nogoods","whether to use no-goods from restarts",false),
00287 _nogoods_limit("nogoods-limit","depth limit for no-good extraction",
00288 Search::Config::nogoods_limit),
00289 _interrupt("interrupt","whether to catch Ctrl-C (true) or not (false)",
00290 true),
00291 _step("step","step distance for float optimization",0.0),
00292 _mode("mode","how to execute script",Gecode::SM_SOLUTION),
00293 _stat("s","emit statistics"),
00294 _output("o","file to send output to")
00295
00296 #ifdef GECODE_HAS_CPPROFILER
00297 ,
00298 _profiler_id("cpprofiler-id", "use this execution id with cpprofiler", 0),
00299 _profiler_port("cpprofiler-port", "connect to cpprofiler on this port", 6565),
00300 _profiler_info("cpprofiler-info", "send solution information to cpprofiler", false)
00301
00302 #endif
00303 {
00304 _mode.add(Gecode::SM_SOLUTION, "solution");
00305 _mode.add(Gecode::SM_STAT, "stat");
00306 _mode.add(Gecode::SM_GIST, "gist");
00307 _mode.add(Gecode::SM_CPPROFILER, "cpprofiler");
00308 _restart.add(RM_NONE,"none");
00309 _restart.add(RM_CONSTANT,"constant");
00310 _restart.add(RM_LINEAR,"linear");
00311 _restart.add(RM_LUBY,"luby");
00312 _restart.add(RM_GEOMETRIC,"geometric");
00313
00314 add(_solutions); add(_threads); add(_c_d); add(_a_d);
00315 add(_allSolutions);
00316 add(_free);
00317 add(_decay);
00318 add(_node); add(_fail); add(_time); add(_time_limit); add(_interrupt);
00319 add(_seed);
00320 add(_step);
00321 add(_restart); add(_r_base); add(_r_scale);
00322 add(_nogoods); add(_nogoods_limit);
00323 add(_mode); add(_stat);
00324 add(_output);
00325 #ifdef GECODE_HAS_CPPROFILER
00326 add(_profiler_id);
00327 add(_profiler_port);
00328 add(_profiler_info);
00329 #endif
00330 }
00331
00332 void parse(int& argc, char* argv[]) {
00333 Gecode::BaseOptions::parse(argc,argv);
00334 if (_allSolutions.value() && _solutions.value()==-1) {
00335 _solutions.value(0);
00336 }
00337 if (_time_limit.value()) {
00338 _time.value(_time_limit.value());
00339 }
00340 if (_stat.value())
00341 _mode.value(Gecode::SM_STAT);
00342 }
00343
00344 virtual void help(void) {
00345 std::cerr << "Gecode FlatZinc interpreter" << std::endl
00346 << " - Supported FlatZinc version: " << GECODE_FLATZINC_VERSION
00347 << std::endl << std::endl;
00348 Gecode::BaseOptions::help();
00349 }
00350
00351 int solutions(void) const { return _solutions.value(); }
00352 bool allSolutions(void) const { return _allSolutions.value(); }
00353 double threads(void) const { return _threads.value(); }
00354 bool free(void) const { return _free.value(); }
00355 unsigned int c_d(void) const { return _c_d.value(); }
00356 unsigned int a_d(void) const { return _a_d.value(); }
00357 unsigned int node(void) const { return _node.value(); }
00358 unsigned int fail(void) const { return _fail.value(); }
00359 unsigned int time(void) const { return _time.value(); }
00360 int seed(void) const { return _seed.value(); }
00361 double step(void) const { return _step.value(); }
00362 const char* output(void) const { return _output.value(); }
00363
00364 Gecode::ScriptMode mode(void) const {
00365 return static_cast<Gecode::ScriptMode>(_mode.value());
00366 }
00367
00368 double decay(void) const { return _decay.value(); }
00369 RestartMode restart(void) const {
00370 return static_cast<RestartMode>(_restart.value());
00371 }
00372 void restart(RestartMode rm) {
00373 _restart.value(rm);
00374 }
00375 double restart_base(void) const { return _r_base.value(); }
00376 void restart_base(double d) { _r_base.value(d); }
00377 unsigned int restart_scale(void) const { return _r_scale.value(); }
00378 void restart_scale(int i) { _r_scale.value(i); }
00379 bool nogoods(void) const { return _nogoods.value(); }
00380 unsigned int nogoods_limit(void) const { return _nogoods_limit.value(); }
00381 bool interrupt(void) const { return _interrupt.value(); }
00382
00383 #ifdef GECODE_HAS_CPPROFILER
00384
00385 int profiler_id(void) const { return _profiler_id.value(); }
00386 unsigned int profiler_port(void) const { return _profiler_port.value(); }
00387 bool profiler_info(void) const { return _profiler_info.value(); }
00388
00389 #endif
00390
00391 void allSolutions(bool b) { _allSolutions.value(b); }
00392 };
00393
00394 class BranchInformation : public SharedHandle {
00395 public:
00397 BranchInformation(void);
00399 BranchInformation(const BranchInformation& bi);
00401 void init(void);
00403 void add(BrancherGroup bg,
00404 const std::string& rel0,
00405 const std::string& rel1,
00406 const std::vector<std::string>& n);
00408 void print(const Brancher& b,
00409 unsigned int a, int i, int n, std::ostream& o) const;
00410 #ifdef GECODE_HAS_FLOAT_VARS
00411
00412 void print(const Brancher& b,
00413 unsigned int a, int i, const FloatNumBranch& nl,
00414 std::ostream& o) const;
00415 #endif
00416 };
00417
00419 GECODE_FLATZINC_EXPORT
00420 extern Rnd defrnd;
00421
00422 class FlatZincSpaceInitData;
00423
00428 class GECODE_FLATZINC_EXPORT FlatZincSpace : public Space {
00429 public:
00430 enum Meth {
00431 SAT,
00432 MIN,
00433 MAX
00434 };
00435 protected:
00437 FlatZincSpaceInitData* _initData;
00439 int intVarCount;
00441 int boolVarCount;
00443 int floatVarCount;
00445 int setVarCount;
00446
00448 int _optVar;
00450 bool _optVarIsInt;
00451
00453 Meth _method;
00454
00456 unsigned int _lns;
00457
00459 IntSharedArray _lnsInitialSolution;
00460
00462 Rnd _random;
00463
00465 AST::Array* _solveAnnotations;
00466
00468 FlatZincSpace(FlatZincSpace&);
00469 private:
00471 template<template<class> class Engine>
00472 void
00473 runEngine(std::ostream& out, const Printer& p,
00474 const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00476 template<template<class> class Engine,
00477 template<class, template<class> class> class Meta>
00478 void
00479 runMeta(std::ostream& out, const Printer& p,
00480 const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00481 void
00482 branchWithPlugin(AST::Node* ann);
00483 public:
00485 Gecode::IntVarArray iv;
00487 Gecode::IntVarArray iv_aux;
00488
00490 Gecode::IntVarArray iv_lns;
00491
00493 std::vector<bool> iv_introduced;
00495 int* iv_boolalias;
00497 Gecode::BoolVarArray bv;
00499 Gecode::BoolVarArray bv_aux;
00501 std::vector<bool> bv_introduced;
00502 #ifdef GECODE_HAS_SET_VARS
00503
00504 Gecode::SetVarArray sv;
00506 Gecode::SetVarArray sv_aux;
00508 std::vector<bool> sv_introduced;
00509 #endif
00510 #ifdef GECODE_HAS_FLOAT_VARS
00511
00512 Gecode::FloatVarArray fv;
00514 Gecode::FloatVarArray fv_aux;
00516 std::vector<bool> fv_introduced;
00518 Gecode::FloatNum step;
00519 #endif
00520
00521 bool needAuxVars;
00523 FlatZincSpace(Rnd& random = defrnd);
00524
00526 ~FlatZincSpace(void);
00527
00529 void init(int intVars, int boolVars, int setVars, int floatVars);
00530
00532 void newIntVar(IntVarSpec* vs);
00534 void aliasBool2Int(int iv, int bv);
00536 int aliasBool2Int(int iv);
00538 void newBoolVar(BoolVarSpec* vs);
00540 void newSetVar(SetVarSpec* vs);
00542 void newFloatVar(FloatVarSpec* vs);
00543
00545 void postConstraints(std::vector<ConExpr*>& ces);
00546
00548 void solve(AST::Array* annotation);
00550 void minimize(int var, bool isInt, AST::Array* annotation);
00552 void maximize(int var, bool isInt, AST::Array* annotation);
00553
00555 void run(std::ostream& out, const Printer& p,
00556 const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00557
00559 void print(std::ostream& out, const Printer& p) const;
00560 #ifdef GECODE_HAS_CPPROFILER
00561
00562 std::string getDomains(const Printer& p) const;
00563 #endif
00564
00565
00566 void compare(const Space& s, std::ostream& out) const;
00569 void compare(const FlatZincSpace& s, std::ostream& out,
00570 const Printer& p) const;
00571
00580 void shrinkArrays(Printer& p);
00581
00583 Meth method(void) const;
00584
00586 int optVar(void) const;
00588 bool optVarIsInt(void) const;
00589
00599 void createBranchers(Printer& p, AST::Node* ann,
00600 FlatZincOptions& opt, bool ignoreUnknown,
00601 std::ostream& err = std::cerr);
00602
00604 AST::Array* solveAnnotations(void) const;
00605
00607 BranchInformation branchInfo;
00608
00610 virtual void constrain(const Space& s);
00612 virtual Gecode::Space* copy(void);
00614 virtual bool slave(const MetaInfo& mi);
00615
00617
00618
00619 IntArgs arg2intargs(AST::Node* arg, int offset = 0);
00621 IntSharedArray arg2intsharedarray(AST::Node* arg, int offset = 0);
00623 IntArgs arg2boolargs(AST::Node* arg, int offset = 0);
00625 IntSharedArray arg2boolsharedarray(AST::Node* arg, int offset = 0);
00627 IntSet arg2intset(AST::Node* n);
00629 IntSetArgs arg2intsetargs(AST::Node* arg, int offset = 0);
00631 IntVarArgs arg2intvarargs(AST::Node* arg, int offset = 0);
00633 BoolVarArgs arg2boolvarargs(AST::Node* arg, int offset = 0, int siv=-1);
00635 BoolVar arg2BoolVar(AST::Node* n);
00637 IntVar arg2IntVar(AST::Node* n);
00639 TupleSet arg2tupleset(const IntArgs& a, int noOfVars);
00641 bool isBoolArray(AST::Node* b, int& singleInt);
00642 #ifdef GECODE_HAS_SET_VARS
00643
00644 SetVar arg2SetVar(AST::Node* n);
00646 SetVarArgs arg2setvarargs(AST::Node* arg, int offset = 0, int doffset = 0,
00647 const IntSet& od=IntSet::empty);
00648 #endif
00649 #ifdef GECODE_HAS_FLOAT_VARS
00650
00651 FloatValArgs arg2floatargs(AST::Node* arg, int offset = 0);
00653 FloatVar arg2FloatVar(AST::Node* n);
00655 FloatVarArgs arg2floatvarargs(AST::Node* arg, int offset = 0);
00656 #endif
00657
00658 IntPropLevel ann2ipl(AST::Node* ann);
00660 DFA getSharedDFA(DFA& a);
00662 };
00663
00665 class GECODE_VTABLE_EXPORT Error {
00666 private:
00667 const std::string msg;
00668 public:
00669 Error(const std::string& where, const std::string& what)
00670 : msg(where+": "+what) {}
00671 const std::string& toString(void) const { return msg; }
00672 };
00673
00679 GECODE_FLATZINC_EXPORT
00680 FlatZincSpace* parse(const std::string& fileName,
00681 Printer& p, std::ostream& err = std::cerr,
00682 FlatZincSpace* fzs=NULL, Rnd& rnd=defrnd);
00683
00689 GECODE_FLATZINC_EXPORT
00690 FlatZincSpace* parse(std::istream& is,
00691 Printer& p, std::ostream& err = std::cerr,
00692 FlatZincSpace* fzs=NULL, Rnd& rnd=defrnd);
00693
00694 }}
00695
00696 #endif
00697
00698