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 #ifndef __GECODE_FLATZINC_HH__
00043 #define __GECODE_FLATZINC_HH__
00044
00045 #include <iostream>
00046
00047 #include <gecode/kernel.hh>
00048 #include <gecode/int.hh>
00049 #ifdef GECODE_HAS_SET_VARS
00050 #include <gecode/set.hh>
00051 #endif
00052 #ifdef GECODE_HAS_FLOAT_VARS
00053 #include <gecode/float.hh>
00054 #endif
00055 #include <map>
00056
00057
00058
00059
00060
00061
00062 #if !defined(GECODE_STATIC_LIBS) && \
00063 (defined(__CYGWIN__) || defined(__MINGW32__) || defined(_MSC_VER))
00064
00065 #ifdef GECODE_BUILD_FLATZINC
00066 #define GECODE_FLATZINC_EXPORT __declspec( dllexport )
00067 #else
00068 #define GECODE_FLATZINC_EXPORT __declspec( dllimport )
00069 #endif
00070
00071 #else
00072
00073 #ifdef GECODE_GCC_HAS_CLASS_VISIBILITY
00074
00075 #define GECODE_FLATZINC_EXPORT __attribute__ ((visibility("default")))
00076
00077 #else
00078
00079 #define GECODE_FLATZINC_EXPORT
00080
00081 #endif
00082 #endif
00083
00084
00085 #ifndef GECODE_BUILD_FLATZINC
00086 #define GECODE_LIBRARY_NAME "FlatZinc"
00087 #include <gecode/support/auto-link.hpp>
00088 #endif
00089
00090 #include <gecode/driver.hh>
00091
00092 #include <gecode/flatzinc/conexpr.hh>
00093 #include <gecode/flatzinc/ast.hh>
00094 #include <gecode/flatzinc/varspec.hh>
00095
00105 namespace Gecode { namespace FlatZinc {
00106
00111 class GECODE_FLATZINC_EXPORT Printer {
00112 private:
00113 AST::Array* _output;
00114 void printElem(std::ostream& out,
00115 AST::Node* ai,
00116 const Gecode::IntVarArray& iv,
00117 const Gecode::BoolVarArray& bv
00118 #ifdef GECODE_HAS_SET_VARS
00119 ,
00120 const Gecode::SetVarArray& sv
00121 #endif
00122 #ifdef GECODE_HAS_FLOAT_VARS
00123 ,
00124 const Gecode::FloatVarArray& fv
00125 #endif
00126 ) const;
00127 void printElemDiff(std::ostream& out,
00128 AST::Node* ai,
00129 const Gecode::IntVarArray& iv1,
00130 const Gecode::IntVarArray& iv2,
00131 const Gecode::BoolVarArray& bv1,
00132 const Gecode::BoolVarArray& bv2
00133 #ifdef GECODE_HAS_SET_VARS
00134 ,
00135 const Gecode::SetVarArray& sv1,
00136 const Gecode::SetVarArray& sv2
00137 #endif
00138 #ifdef GECODE_HAS_FLOAT_VARS
00139 ,
00140 const Gecode::FloatVarArray& fv1,
00141 const Gecode::FloatVarArray& fv2
00142 #endif
00143 ) const;
00144 public:
00145 Printer(void) : _output(NULL) {}
00146 void init(AST::Array* output);
00147
00148 void print(std::ostream& out,
00149 const Gecode::IntVarArray& iv,
00150 const Gecode::BoolVarArray& bv
00151 #ifdef GECODE_HAS_SET_VARS
00152 ,
00153 const Gecode::SetVarArray& sv
00154 #endif
00155 #ifdef GECODE_HAS_FLOAT_VARS
00156 ,
00157 const Gecode::FloatVarArray& fv
00158 #endif
00159 ) const;
00160
00161 void printDiff(std::ostream& out,
00162 const Gecode::IntVarArray& iv1, const Gecode::IntVarArray& iv2,
00163 const Gecode::BoolVarArray& bv1, const Gecode::BoolVarArray& bv2
00164 #ifdef GECODE_HAS_SET_VARS
00165 ,
00166 const Gecode::SetVarArray& sv1, const Gecode::SetVarArray& sv2
00167 #endif
00168 #ifdef GECODE_HAS_FLOAT_VARS
00169 ,
00170 const Gecode::FloatVarArray& fv1,
00171 const Gecode::FloatVarArray& fv2
00172 #endif
00173 ) const;
00174
00175
00176 ~Printer(void);
00177
00178 void shrinkElement(AST::Node* node,
00179 std::map<int,int>& iv, std::map<int,int>& bv,
00180 std::map<int,int>& sv, std::map<int,int>& fv);
00181
00182 void shrinkArrays(Space& home,
00183 int& optVar, bool optVarIsInt,
00184 Gecode::IntVarArray& iv,
00185 Gecode::BoolVarArray& bv
00186 #ifdef GECODE_HAS_SET_VARS
00187 ,
00188 Gecode::SetVarArray& sv
00189 #endif
00190 #ifdef GECODE_HAS_FLOAT_VARS
00191 ,
00192 Gecode::FloatVarArray& fv
00193 #endif
00194 );
00195
00196 private:
00197 Printer(const Printer&);
00198 Printer& operator=(const Printer&);
00199 };
00200
00205 class FlatZincOptions : public Gecode::BaseOptions {
00206 protected:
00208
00209 Gecode::Driver::IntOption _solutions;
00210 Gecode::Driver::BoolOption _allSolutions;
00211 Gecode::Driver::DoubleOption _threads;
00212 Gecode::Driver::BoolOption _free;
00213 Gecode::Driver::DoubleOption _decay;
00214 Gecode::Driver::UnsignedIntOption _c_d;
00215 Gecode::Driver::UnsignedIntOption _a_d;
00216 Gecode::Driver::UnsignedIntOption _node;
00217 Gecode::Driver::UnsignedIntOption _fail;
00218 Gecode::Driver::UnsignedIntOption _time;
00219 Gecode::Driver::IntOption _seed;
00220 Gecode::Driver::StringOption _restart;
00221 Gecode::Driver::DoubleOption _r_base;
00222 Gecode::Driver::UnsignedIntOption _r_scale;
00223 Gecode::Driver::BoolOption _nogoods;
00224 Gecode::Driver::UnsignedIntOption _nogoods_limit;
00225 Gecode::Driver::BoolOption _interrupt;
00226 Gecode::Driver::DoubleOption _step;
00227
00228
00230
00231 Gecode::Driver::StringOption _mode;
00232 Gecode::Driver::BoolOption _stat;
00233 Gecode::Driver::StringValueOption _output;
00234
00235 public:
00237 FlatZincOptions(const char* s)
00238 : Gecode::BaseOptions(s),
00239 _solutions("-n","number of solutions (0 = all, -1 = one/best)",-1),
00240 _allSolutions("-a", "return all solutions (equal to -n 0)"),
00241 _threads("-p","number of threads (0 = #processing units)",
00242 Gecode::Search::Config::threads),
00243 _free("-f", "free search, no need to follow search-specification"),
00244 _decay("-decay","decay factor",0.99),
00245 _c_d("-c-d","recomputation commit distance",Gecode::Search::Config::c_d),
00246 _a_d("-a-d","recomputation adaption distance",Gecode::Search::Config::a_d),
00247 _node("-node","node cutoff (0 = none, solution mode)"),
00248 _fail("-fail","failure cutoff (0 = none, solution mode)"),
00249 _time("-time","time (in ms) cutoff (0 = none, solution mode)"),
00250 _seed("-r","random seed",0),
00251 _restart("-restart","restart sequence type",RM_NONE),
00252 _r_base("-restart-base","base for geometric restart sequence",1.5),
00253 _r_scale("-restart-scale","scale factor for restart sequence",250),
00254 _nogoods("-nogoods","whether to use no-goods from restarts",false),
00255 _nogoods_limit("-nogoods-limit","depth limit for no-good extraction",
00256 Search::Config::nogoods_limit),
00257 _interrupt("-interrupt","whether to catch Ctrl-C (true) or not (false)",
00258 true),
00259 _step("-step","step distance for float optimization",0.0),
00260 _mode("-mode","how to execute script",Gecode::SM_SOLUTION),
00261 _stat("-s","emit statistics"),
00262 _output("-o","file to send output to") {
00263
00264 _mode.add(Gecode::SM_SOLUTION, "solution");
00265 _mode.add(Gecode::SM_STAT, "stat");
00266 _mode.add(Gecode::SM_GIST, "gist");
00267 _restart.add(RM_NONE,"none");
00268 _restart.add(RM_CONSTANT,"constant");
00269 _restart.add(RM_LINEAR,"linear");
00270 _restart.add(RM_LUBY,"luby");
00271 _restart.add(RM_GEOMETRIC,"geometric");
00272
00273 add(_solutions); add(_threads); add(_c_d); add(_a_d);
00274 add(_allSolutions);
00275 add(_free);
00276 add(_decay);
00277 add(_node); add(_fail); add(_time); add(_interrupt);
00278 add(_seed);
00279 add(_step);
00280 add(_restart); add(_r_base); add(_r_scale);
00281 add(_nogoods); add(_nogoods_limit);
00282 add(_mode); add(_stat);
00283 add(_output);
00284 }
00285
00286 void parse(int& argc, char* argv[]) {
00287 Gecode::BaseOptions::parse(argc,argv);
00288 if (_allSolutions.value() && _solutions.value()==-1) {
00289 _solutions.value(0);
00290 }
00291 if (_stat.value())
00292 _mode.value(Gecode::SM_STAT);
00293 }
00294
00295 virtual void help(void) {
00296 std::cerr << "Gecode FlatZinc interpreter" << std::endl
00297 << " - Supported FlatZinc version: " << GECODE_FLATZINC_VERSION
00298 << std::endl << std::endl;
00299 Gecode::BaseOptions::help();
00300 }
00301
00302 int solutions(void) const { return _solutions.value(); }
00303 bool allSolutions(void) const { return _allSolutions.value(); }
00304 double threads(void) const { return _threads.value(); }
00305 bool free(void) const { return _free.value(); }
00306 unsigned int c_d(void) const { return _c_d.value(); }
00307 unsigned int a_d(void) const { return _a_d.value(); }
00308 unsigned int node(void) const { return _node.value(); }
00309 unsigned int fail(void) const { return _fail.value(); }
00310 unsigned int time(void) const { return _time.value(); }
00311 int seed(void) const { return _seed.value(); }
00312 double step(void) const { return _step.value(); }
00313 const char* output(void) const { return _output.value(); }
00314 Gecode::ScriptMode mode(void) const {
00315 return static_cast<Gecode::ScriptMode>(_mode.value());
00316 }
00317
00318 double decay(void) const { return _decay.value(); }
00319 RestartMode restart(void) const {
00320 return static_cast<RestartMode>(_restart.value());
00321 }
00322 double restart_base(void) const { return _r_base.value(); }
00323 unsigned int restart_scale(void) const { return _r_scale.value(); }
00324 bool nogoods(void) const { return _nogoods.value(); }
00325 unsigned int nogoods_limit(void) const { return _nogoods_limit.value(); }
00326 bool interrupt(void) const { return _interrupt.value(); }
00327
00328 void allSolutions(bool b) { _allSolutions.value(b); }
00329 };
00330
00331 class BranchInformation : public SharedHandle {
00332 public:
00334 BranchInformation(void);
00336 BranchInformation(const BranchInformation& bi);
00338 void init(void);
00340 void add(const BrancherHandle& bh,
00341 const std::string& rel0,
00342 const std::string& rel1,
00343 const std::vector<std::string>& n);
00345 void print(const BrancherHandle& bh,
00346 int a, int i, int n, std::ostream& o) const;
00347 #ifdef GECODE_HAS_FLOAT_VARS
00348
00349 void print(const BrancherHandle& bh,
00350 int a, int i, const FloatNumBranch& nl, std::ostream& o) const;
00351 #endif
00352 };
00353
00358 class GECODE_FLATZINC_EXPORT FznRnd {
00359 protected:
00361 Gecode::Support::RandomGenerator random;
00363 Gecode::Support::Mutex mutex;
00364 public:
00366 FznRnd(unsigned int s=1);
00368 unsigned int operator ()(unsigned int n);
00369 };
00370
00375 class GECODE_FLATZINC_EXPORT FlatZincSpace : public Space {
00376 public:
00377 enum Meth {
00378 SAT,
00379 MIN,
00380 MAX
00381 };
00382 protected:
00384 int intVarCount;
00386 int boolVarCount;
00388 int floatVarCount;
00390 int setVarCount;
00391
00393 int _optVar;
00395 bool _optVarIsInt;
00396
00398 Meth _method;
00399
00401 unsigned int _lns;
00402
00404 FznRnd* _random;
00405
00407 AST::Array* _solveAnnotations;
00408
00410 FlatZincSpace(bool share, FlatZincSpace&);
00411 private:
00413 template<template<class> class Engine>
00414 void
00415 runEngine(std::ostream& out, const Printer& p,
00416 const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00418 template<template<class> class Engine,
00419 template<template<class> class,class> class Meta>
00420 void
00421 runMeta(std::ostream& out, const Printer& p,
00422 const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00423 void
00424 branchWithPlugin(AST::Node* ann);
00425 public:
00427 Gecode::IntVarArray iv;
00429 Gecode::IntVarArray iv_aux;
00430
00432 Gecode::IntVarArray iv_lns;
00433
00435 std::vector<bool> iv_introduced;
00437 int* iv_boolalias;
00439 Gecode::BoolVarArray bv;
00441 Gecode::BoolVarArray bv_aux;
00443 std::vector<bool> bv_introduced;
00444 #ifdef GECODE_HAS_SET_VARS
00445
00446 Gecode::SetVarArray sv;
00448 Gecode::SetVarArray sv_aux;
00450 std::vector<bool> sv_introduced;
00451 #endif
00452 #ifdef GECODE_HAS_FLOAT_VARS
00453
00454 Gecode::FloatVarArray fv;
00456 Gecode::FloatVarArray fv_aux;
00458 std::vector<bool> fv_introduced;
00460 Gecode::FloatNum step;
00461 #endif
00462
00463 bool needAuxVars;
00465 FlatZincSpace(FznRnd* random = NULL);
00466
00468 ~FlatZincSpace(void);
00469
00471 void init(int intVars, int boolVars, int setVars, int floatVars);
00472
00474 void newIntVar(IntVarSpec* vs);
00476 void aliasBool2Int(int iv, int bv);
00478 int aliasBool2Int(int iv);
00480 void newBoolVar(BoolVarSpec* vs);
00482 void newSetVar(SetVarSpec* vs);
00484 void newFloatVar(FloatVarSpec* vs);
00485
00487 void postConstraints(std::vector<ConExpr*>& ces);
00488
00490 void solve(AST::Array* annotation);
00492 void minimize(int var, bool isInt, AST::Array* annotation);
00494 void maximize(int var, bool isInt, AST::Array* annotation);
00495
00497 void run(std::ostream& out, const Printer& p,
00498 const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00499
00501 void print(std::ostream& out, const Printer& p) const;
00502
00505 void compare(const Space& s, std::ostream& out) const;
00508 void compare(const FlatZincSpace& s, std::ostream& out,
00509 const Printer& p) const;
00510
00519 void shrinkArrays(Printer& p);
00520
00522 Meth method(void) const;
00523
00525 int optVar(void) const;
00527 bool optVarIsInt(void) const;
00528
00538 void createBranchers(AST::Node* ann,
00539 int seed, double decay,
00540 bool ignoreUnknown,
00541 std::ostream& err = std::cerr);
00542
00544 AST::Array* solveAnnotations(void) const;
00545
00547 BranchInformation branchInfo;
00548
00550 virtual void constrain(const Space& s);
00552 virtual Gecode::Space* copy(bool share);
00553
00554 virtual bool slave(const CRI& cri);
00555
00557
00558
00559 IntArgs arg2intargs(AST::Node* arg, int offset = 0);
00561 IntArgs arg2boolargs(AST::Node* arg, int offset = 0);
00563 IntSet arg2intset(AST::Node* n);
00565 IntSetArgs arg2intsetargs(AST::Node* arg, int offset = 0);
00567 IntVarArgs arg2intvarargs(AST::Node* arg, int offset = 0);
00569 BoolVarArgs arg2boolvarargs(AST::Node* arg, int offset = 0, int siv=-1);
00571 BoolVar arg2BoolVar(AST::Node* n);
00573 IntVar arg2IntVar(AST::Node* n);
00575 bool isBoolArray(AST::Node* b, int& singleInt);
00576 #ifdef GECODE_HAS_SET_VARS
00577
00578 SetVar arg2SetVar(AST::Node* n);
00580 SetVarArgs arg2setvarargs(AST::Node* arg, int offset = 0, int doffset = 0,
00581 const IntSet& od=IntSet::empty);
00582 #endif
00583 #ifdef GECODE_HAS_FLOAT_VARS
00584
00585 FloatValArgs arg2floatargs(AST::Node* arg, int offset = 0);
00587 FloatVar arg2FloatVar(AST::Node* n);
00589 FloatVarArgs arg2floatvarargs(AST::Node* arg, int offset = 0);
00590 #endif
00591
00592 IntConLevel ann2icl(AST::Node* ann);
00594 };
00595
00597 class GECODE_VTABLE_EXPORT Error {
00598 private:
00599 const std::string msg;
00600 public:
00601 Error(const std::string& where, const std::string& what)
00602 : msg(where+": "+what) {}
00603 const std::string& toString(void) const { return msg; }
00604 };
00605
00611 GECODE_FLATZINC_EXPORT
00612 FlatZincSpace* parse(const std::string& fileName,
00613 Printer& p, std::ostream& err = std::cerr,
00614 FlatZincSpace* fzs=NULL, FznRnd* rnd=NULL);
00615
00621 GECODE_FLATZINC_EXPORT
00622 FlatZincSpace* parse(std::istream& is,
00623 Printer& p, std::ostream& err = std::cerr,
00624 FlatZincSpace* fzs=NULL, FznRnd* rnd=NULL);
00625
00626 }}
00627
00628 #endif
00629
00630