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::UnsignedIntOption _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
00227
00229
00230 Gecode::Driver::StringOption _mode;
00231 Gecode::Driver::BoolOption _stat;
00232 Gecode::Driver::StringValueOption _output;
00233
00234 public:
00236 FlatZincOptions(const char* s)
00237 : Gecode::BaseOptions(s),
00238 _solutions("-n","number of solutions (0 = all)",1),
00239 _allSolutions("-a", "return all solutions (equal to -solutions 0)"),
00240 _threads("-p","number of threads (0 = #processing units)",
00241 Gecode::Search::Config::threads),
00242 _free("--free", "no need to follow search-specification"),
00243 _decay("-decay","decay factor",0.99),
00244 _c_d("-c-d","recomputation commit distance",Gecode::Search::Config::c_d),
00245 _a_d("-a-d","recomputation adaption distance",Gecode::Search::Config::a_d),
00246 _node("-node","node cutoff (0 = none, solution mode)"),
00247 _fail("-fail","failure cutoff (0 = none, solution mode)"),
00248 _time("-time","time (in ms) cutoff (0 = none, solution mode)"),
00249 _seed("-r","random seed",0),
00250 _restart("-restart","restart sequence type",RM_NONE),
00251 _r_base("-restart-base","base for geometric restart sequence",1.5),
00252 _r_scale("-restart-scale","scale factor for restart sequence",250),
00253 _nogoods("-nogoods","whether to use no-goods from restarts",false),
00254 _nogoods_limit("-nogoods-limit","depth limit for no-good extraction",
00255 Search::Config::nogoods_limit),
00256 _interrupt("-interrupt","whether to catch Ctrl-C (true) or not (false)",
00257 true),
00258 _mode("-mode","how to execute script",Gecode::SM_SOLUTION),
00259 _stat("-s","emit statistics"),
00260 _output("-o","file to send output to") {
00261
00262 _mode.add(Gecode::SM_SOLUTION, "solution");
00263 _mode.add(Gecode::SM_STAT, "stat");
00264 _mode.add(Gecode::SM_GIST, "gist");
00265 _restart.add(RM_NONE,"none");
00266 _restart.add(RM_CONSTANT,"constant");
00267 _restart.add(RM_LINEAR,"linear");
00268 _restart.add(RM_LUBY,"luby");
00269 _restart.add(RM_GEOMETRIC,"geometric");
00270
00271 add(_solutions); add(_threads); add(_c_d); add(_a_d);
00272 add(_allSolutions);
00273 add(_free);
00274 add(_decay);
00275 add(_node); add(_fail); add(_time); add(_interrupt);
00276 add(_seed);
00277 add(_restart); add(_r_base); add(_r_scale);
00278 add(_nogoods); add(_nogoods_limit);
00279 add(_mode); add(_stat);
00280 add(_output);
00281 }
00282
00283 void parse(int& argc, char* argv[]) {
00284 Gecode::BaseOptions::parse(argc,argv);
00285 if (_allSolutions.value()) {
00286 _solutions.value(0);
00287 }
00288 if (_stat.value())
00289 _mode.value(Gecode::SM_STAT);
00290 }
00291
00292 virtual void help(void) {
00293 std::cerr << "Gecode FlatZinc interpreter" << std::endl
00294 << " - Supported FlatZinc version: " << GECODE_FLATZINC_VERSION
00295 << std::endl << std::endl;
00296 Gecode::BaseOptions::help();
00297 }
00298
00299 unsigned int solutions(void) const { return _solutions.value(); }
00300 bool allSolutions(void) const { return _allSolutions.value(); }
00301 double threads(void) const { return _threads.value(); }
00302 bool free(void) const { return _free.value(); }
00303 unsigned int c_d(void) const { return _c_d.value(); }
00304 unsigned int a_d(void) const { return _a_d.value(); }
00305 unsigned int node(void) const { return _node.value(); }
00306 unsigned int fail(void) const { return _fail.value(); }
00307 unsigned int time(void) const { return _time.value(); }
00308 int seed(void) const { return _seed.value(); }
00309 const char* output(void) const { return _output.value(); }
00310 Gecode::ScriptMode mode(void) const {
00311 return static_cast<Gecode::ScriptMode>(_mode.value());
00312 }
00313
00314 double decay(void) const { return _decay.value(); }
00315 RestartMode restart(void) const {
00316 return static_cast<RestartMode>(_restart.value());
00317 }
00318 double restart_base(void) const { return _r_base.value(); }
00319 unsigned int restart_scale(void) const { return _r_scale.value(); }
00320 bool nogoods(void) const { return _nogoods.value(); }
00321 unsigned int nogoods_limit(void) const { return _nogoods_limit.value(); }
00322 bool interrupt(void) const { return _interrupt.value(); }
00323
00324 };
00325
00326 class BranchInformation : public SharedHandle {
00327 public:
00329 BranchInformation(void);
00331 BranchInformation(const BranchInformation& bi);
00333 void init(void);
00335 void add(const BrancherHandle& bh,
00336 const std::string& rel0,
00337 const std::string& rel1,
00338 const std::vector<std::string>& n);
00340 void print(const BrancherHandle& bh,
00341 int a, int i, int n, std::ostream& o) const;
00342 #ifdef GECODE_HAS_FLOAT_VARS
00343
00344 void print(const BrancherHandle& bh,
00345 int a, int i, const FloatNumBranch& nl, std::ostream& o) const;
00346 #endif
00347 };
00348
00353 class GECODE_FLATZINC_EXPORT FlatZincSpace : public Space {
00354 public:
00355 enum Meth {
00356 SAT,
00357 MIN,
00358 MAX
00359 };
00360 protected:
00362 int intVarCount;
00364 int boolVarCount;
00366 int floatVarCount;
00368 int setVarCount;
00369
00371 int _optVar;
00373 bool _optVarIsInt;
00374
00376 Meth _method;
00377
00379 AST::Array* _solveAnnotations;
00380
00382 FlatZincSpace(bool share, FlatZincSpace&);
00383 private:
00385 template<template<class> class Engine>
00386 void
00387 runEngine(std::ostream& out, const Printer& p,
00388 const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00390 template<template<class> class Engine,
00391 template<template<class> class,class> class Meta>
00392 void
00393 runMeta(std::ostream& out, const Printer& p,
00394 const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00395 void
00396 branchWithPlugin(AST::Node* ann);
00397 public:
00399 Gecode::IntVarArray iv;
00401 Gecode::IntVarArray iv_aux;
00403 std::vector<bool> iv_introduced;
00405 int* iv_boolalias;
00407 Gecode::BoolVarArray bv;
00409 Gecode::BoolVarArray bv_aux;
00411 std::vector<bool> bv_introduced;
00412 #ifdef GECODE_HAS_SET_VARS
00413
00414 Gecode::SetVarArray sv;
00416 Gecode::SetVarArray sv_aux;
00418 std::vector<bool> sv_introduced;
00419 #endif
00420 #ifdef GECODE_HAS_FLOAT_VARS
00421
00422 Gecode::FloatVarArray fv;
00424 Gecode::FloatVarArray fv_aux;
00426 std::vector<bool> fv_introduced;
00427 #endif
00428
00429 bool needAuxVars;
00431 FlatZincSpace(void);
00432
00434 ~FlatZincSpace(void);
00435
00437 void init(int intVars, int boolVars, int setVars, int floatVars);
00438
00440 void newIntVar(IntVarSpec* vs);
00442 void aliasBool2Int(int iv, int bv);
00444 int aliasBool2Int(int iv);
00446 void newBoolVar(BoolVarSpec* vs);
00448 void newSetVar(SetVarSpec* vs);
00450 void newFloatVar(FloatVarSpec* vs);
00451
00453 void postConstraint(const ConExpr& ce, AST::Node* annotation);
00454
00456 void solve(AST::Array* annotation);
00458 void minimize(int var, bool isInt, AST::Array* annotation);
00460 void maximize(int var, bool isInt, AST::Array* annotation);
00461
00463 void run(std::ostream& out, const Printer& p,
00464 const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00465
00467 void print(std::ostream& out, const Printer& p) const;
00468
00471 void compare(const Space& s, std::ostream& out) const;
00474 void compare(const FlatZincSpace& s, std::ostream& out,
00475 const Printer& p) const;
00476
00485 void shrinkArrays(Printer& p);
00486
00488 Meth method(void) const;
00489
00491 int optVar(void) const;
00493 bool optVarIsInt(void) const;
00494
00504 void createBranchers(AST::Node* ann,
00505 int seed, double decay,
00506 bool ignoreUnknown,
00507 std::ostream& err = std::cerr);
00508
00510 AST::Array* solveAnnotations(void) const;
00511
00513 BranchInformation branchInfo;
00514
00516 virtual void constrain(const Space& s);
00518 virtual Gecode::Space* copy(bool share);
00519
00521
00522
00523 IntArgs arg2intargs(AST::Node* arg, int offset = 0);
00525 IntArgs arg2boolargs(AST::Node* arg, int offset = 0);
00527 IntSet arg2intset(AST::Node* n);
00529 IntSetArgs arg2intsetargs(AST::Node* arg, int offset = 0);
00531 IntVarArgs arg2intvarargs(AST::Node* arg, int offset = 0);
00533 BoolVarArgs arg2boolvarargs(AST::Node* arg, int offset = 0, int siv=-1);
00535 BoolVar arg2BoolVar(AST::Node* n);
00537 IntVar arg2IntVar(AST::Node* n);
00539 bool isBoolArray(AST::Node* b, int& singleInt);
00540 #ifdef GECODE_HAS_SET_VARS
00541
00542 SetVar arg2SetVar(AST::Node* n);
00544 SetVarArgs arg2setvarargs(AST::Node* arg, int offset = 0, int doffset = 0,
00545 const IntSet& od=IntSet::empty);
00546 #endif
00547 #ifdef GECODE_HAS_FLOAT_VARS
00548
00549 FloatValArgs arg2floatargs(AST::Node* arg, int offset = 0);
00551 FloatVar arg2FloatVar(AST::Node* n);
00553 FloatVarArgs arg2floatvarargs(AST::Node* arg, int offset = 0);
00554 #endif
00555
00556 IntConLevel ann2icl(AST::Node* ann);
00558 };
00559
00561 class Error {
00562 private:
00563 const std::string msg;
00564 public:
00565 Error(const std::string& where, const std::string& what)
00566 : msg(where+": "+what) {}
00567 const std::string& toString(void) const { return msg; }
00568 };
00569
00575 GECODE_FLATZINC_EXPORT
00576 FlatZincSpace* parse(const std::string& fileName,
00577 Printer& p, std::ostream& err = std::cerr,
00578 FlatZincSpace* fzs=NULL);
00579
00585 GECODE_FLATZINC_EXPORT
00586 FlatZincSpace* parse(std::istream& is,
00587 Printer& p, std::ostream& err = std::cerr,
00588 FlatZincSpace* fzs=NULL);
00589
00590 }}
00591
00592 #endif
00593
00594