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::IntOption _seed;
00241 Gecode::Driver::StringOption _restart;
00242 Gecode::Driver::DoubleOption _r_base;
00243 Gecode::Driver::UnsignedIntOption _r_scale;
00244 Gecode::Driver::BoolOption _nogoods;
00245 Gecode::Driver::UnsignedIntOption _nogoods_limit;
00246 Gecode::Driver::BoolOption _interrupt;
00247 Gecode::Driver::DoubleOption _step;
00248
00249
00251
00252 Gecode::Driver::StringOption _mode;
00253 Gecode::Driver::BoolOption _stat;
00254 Gecode::Driver::StringValueOption _output;
00255
00256 #ifdef GECODE_HAS_CPPROFILER
00257
00258 Gecode::Driver::IntOption _profiler_id;
00259 Gecode::Driver::UnsignedIntOption _profiler_port;
00260 Gecode::Driver::BoolOption _profiler_info;
00261
00262 #endif
00263
00265 public:
00267 FlatZincOptions(const char* s)
00268 : Gecode::BaseOptions(s),
00269 _solutions("n","number of solutions (0 = all, -1 = one/best)",-1),
00270 _allSolutions("a", "return all solutions (equal to -n 0)"),
00271 _threads("p","number of threads (0 = #processing units)",
00272 Gecode::Search::Config::threads),
00273 _free("f", "free search, no need to follow search-specification"),
00274 _decay("decay","decay factor",0.99),
00275 _c_d("c-d","recomputation commit distance",Gecode::Search::Config::c_d),
00276 _a_d("a-d","recomputation adaption distance",Gecode::Search::Config::a_d),
00277 _node("node","node cutoff (0 = none, solution mode)"),
00278 _fail("fail","failure cutoff (0 = none, solution mode)"),
00279 _time("time","time (in ms) cutoff (0 = none, solution mode)"),
00280 _seed("r","random seed",0),
00281 _restart("restart","restart sequence type",RM_NONE),
00282 _r_base("restart-base","base for geometric restart sequence",1.5),
00283 _r_scale("restart-scale","scale factor for restart sequence",250),
00284 _nogoods("nogoods","whether to use no-goods from restarts",false),
00285 _nogoods_limit("nogoods-limit","depth limit for no-good extraction",
00286 Search::Config::nogoods_limit),
00287 _interrupt("interrupt","whether to catch Ctrl-C (true) or not (false)",
00288 true),
00289 _step("step","step distance for float optimization",0.0),
00290 _mode("mode","how to execute script",Gecode::SM_SOLUTION),
00291 _stat("s","emit statistics"),
00292 _output("o","file to send output to")
00293
00294 #ifdef GECODE_HAS_CPPROFILER
00295 ,
00296 _profiler_id("cpprofiler-id", "use this execution id with cpprofiler", 0),
00297 _profiler_port("cpprofiler-port", "connect to cpprofiler on this port", 6565),
00298 _profiler_info("cpprofiler-info", "send solution information to cpprofiler", false)
00299
00300 #endif
00301 {
00302 _mode.add(Gecode::SM_SOLUTION, "solution");
00303 _mode.add(Gecode::SM_STAT, "stat");
00304 _mode.add(Gecode::SM_GIST, "gist");
00305 _mode.add(Gecode::SM_CPPROFILER, "cpprofiler");
00306 _restart.add(RM_NONE,"none");
00307 _restart.add(RM_CONSTANT,"constant");
00308 _restart.add(RM_LINEAR,"linear");
00309 _restart.add(RM_LUBY,"luby");
00310 _restart.add(RM_GEOMETRIC,"geometric");
00311
00312 add(_solutions); add(_threads); add(_c_d); add(_a_d);
00313 add(_allSolutions);
00314 add(_free);
00315 add(_decay);
00316 add(_node); add(_fail); add(_time); add(_interrupt);
00317 add(_seed);
00318 add(_step);
00319 add(_restart); add(_r_base); add(_r_scale);
00320 add(_nogoods); add(_nogoods_limit);
00321 add(_mode); add(_stat);
00322 add(_output);
00323 #ifdef GECODE_HAS_CPPROFILER
00324 add(_profiler_id);
00325 add(_profiler_port);
00326 add(_profiler_info);
00327 #endif
00328 }
00329
00330 void parse(int& argc, char* argv[]) {
00331 Gecode::BaseOptions::parse(argc,argv);
00332 if (_allSolutions.value() && _solutions.value()==-1) {
00333 _solutions.value(0);
00334 }
00335 if (_stat.value())
00336 _mode.value(Gecode::SM_STAT);
00337 }
00338
00339 virtual void help(void) {
00340 std::cerr << "Gecode FlatZinc interpreter" << std::endl
00341 << " - Supported FlatZinc version: " << GECODE_FLATZINC_VERSION
00342 << std::endl << std::endl;
00343 Gecode::BaseOptions::help();
00344 }
00345
00346 int solutions(void) const { return _solutions.value(); }
00347 bool allSolutions(void) const { return _allSolutions.value(); }
00348 double threads(void) const { return _threads.value(); }
00349 bool free(void) const { return _free.value(); }
00350 unsigned int c_d(void) const { return _c_d.value(); }
00351 unsigned int a_d(void) const { return _a_d.value(); }
00352 unsigned int node(void) const { return _node.value(); }
00353 unsigned int fail(void) const { return _fail.value(); }
00354 unsigned int time(void) const { return _time.value(); }
00355 int seed(void) const { return _seed.value(); }
00356 double step(void) const { return _step.value(); }
00357 const char* output(void) const { return _output.value(); }
00358
00359 Gecode::ScriptMode mode(void) const {
00360 return static_cast<Gecode::ScriptMode>(_mode.value());
00361 }
00362
00363 double decay(void) const { return _decay.value(); }
00364 RestartMode restart(void) const {
00365 return static_cast<RestartMode>(_restart.value());
00366 }
00367 void restart(RestartMode rm) {
00368 _restart.value(rm);
00369 }
00370 double restart_base(void) const { return _r_base.value(); }
00371 void restart_base(double d) { _r_base.value(d); }
00372 unsigned int restart_scale(void) const { return _r_scale.value(); }
00373 void restart_scale(int i) { _r_scale.value(i); }
00374 bool nogoods(void) const { return _nogoods.value(); }
00375 unsigned int nogoods_limit(void) const { return _nogoods_limit.value(); }
00376 bool interrupt(void) const { return _interrupt.value(); }
00377
00378 #ifdef GECODE_HAS_CPPROFILER
00379
00380 int profiler_id(void) const { return _profiler_id.value(); }
00381 unsigned int profiler_port(void) const { return _profiler_port.value(); }
00382 bool profiler_info(void) const { return _profiler_info.value(); }
00383
00384 #endif
00385
00386 void allSolutions(bool b) { _allSolutions.value(b); }
00387 };
00388
00389 class BranchInformation : public SharedHandle {
00390 public:
00392 BranchInformation(void);
00394 BranchInformation(const BranchInformation& bi);
00396 void init(void);
00398 void add(BrancherGroup bg,
00399 const std::string& rel0,
00400 const std::string& rel1,
00401 const std::vector<std::string>& n);
00403 void print(const Brancher& b,
00404 unsigned int a, int i, int n, std::ostream& o) const;
00405 #ifdef GECODE_HAS_FLOAT_VARS
00406
00407 void print(const Brancher& b,
00408 unsigned int a, int i, const FloatNumBranch& nl,
00409 std::ostream& o) const;
00410 #endif
00411 };
00412
00414 GECODE_FLATZINC_EXPORT
00415 extern Rnd defrnd;
00416
00417 class FlatZincSpaceInitData;
00418
00423 class GECODE_FLATZINC_EXPORT FlatZincSpace : public Space {
00424 public:
00425 enum Meth {
00426 SAT,
00427 MIN,
00428 MAX
00429 };
00430 protected:
00432 FlatZincSpaceInitData* _initData;
00434 int intVarCount;
00436 int boolVarCount;
00438 int floatVarCount;
00440 int setVarCount;
00441
00443 int _optVar;
00445 bool _optVarIsInt;
00446
00448 Meth _method;
00449
00451 unsigned int _lns;
00452
00454 IntSharedArray _lnsInitialSolution;
00455
00457 Rnd _random;
00458
00460 AST::Array* _solveAnnotations;
00461
00463 FlatZincSpace(FlatZincSpace&);
00464 private:
00466 template<template<class> class Engine>
00467 void
00468 runEngine(std::ostream& out, const Printer& p,
00469 const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00471 template<template<class> class Engine,
00472 template<class, template<class> class> class Meta>
00473 void
00474 runMeta(std::ostream& out, const Printer& p,
00475 const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00476 void
00477 branchWithPlugin(AST::Node* ann);
00478 public:
00480 Gecode::IntVarArray iv;
00482 Gecode::IntVarArray iv_aux;
00483
00485 Gecode::IntVarArray iv_lns;
00486
00488 std::vector<bool> iv_introduced;
00490 int* iv_boolalias;
00492 Gecode::BoolVarArray bv;
00494 Gecode::BoolVarArray bv_aux;
00496 std::vector<bool> bv_introduced;
00497 #ifdef GECODE_HAS_SET_VARS
00498
00499 Gecode::SetVarArray sv;
00501 Gecode::SetVarArray sv_aux;
00503 std::vector<bool> sv_introduced;
00504 #endif
00505 #ifdef GECODE_HAS_FLOAT_VARS
00506
00507 Gecode::FloatVarArray fv;
00509 Gecode::FloatVarArray fv_aux;
00511 std::vector<bool> fv_introduced;
00513 Gecode::FloatNum step;
00514 #endif
00515
00516 bool needAuxVars;
00518 FlatZincSpace(Rnd& random = defrnd);
00519
00521 ~FlatZincSpace(void);
00522
00524 void init(int intVars, int boolVars, int setVars, int floatVars);
00525
00527 void newIntVar(IntVarSpec* vs);
00529 void aliasBool2Int(int iv, int bv);
00531 int aliasBool2Int(int iv);
00533 void newBoolVar(BoolVarSpec* vs);
00535 void newSetVar(SetVarSpec* vs);
00537 void newFloatVar(FloatVarSpec* vs);
00538
00540 void postConstraints(std::vector<ConExpr*>& ces);
00541
00543 void solve(AST::Array* annotation);
00545 void minimize(int var, bool isInt, AST::Array* annotation);
00547 void maximize(int var, bool isInt, AST::Array* annotation);
00548
00550 void run(std::ostream& out, const Printer& p,
00551 const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00552
00554 void print(std::ostream& out, const Printer& p) const;
00555 #ifdef GECODE_HAS_CPPROFILER
00556
00557 std::string getDomains(const Printer& p) const;
00558 #endif
00559
00560
00561 void compare(const Space& s, std::ostream& out) const;
00564 void compare(const FlatZincSpace& s, std::ostream& out,
00565 const Printer& p) const;
00566
00575 void shrinkArrays(Printer& p);
00576
00578 Meth method(void) const;
00579
00581 int optVar(void) const;
00583 bool optVarIsInt(void) const;
00584
00594 void createBranchers(Printer& p, AST::Node* ann,
00595 FlatZincOptions& opt, bool ignoreUnknown,
00596 std::ostream& err = std::cerr);
00597
00599 AST::Array* solveAnnotations(void) const;
00600
00602 BranchInformation branchInfo;
00603
00605 virtual void constrain(const Space& s);
00607 virtual Gecode::Space* copy(void);
00609 virtual bool slave(const MetaInfo& mi);
00610
00612
00613
00614 IntArgs arg2intargs(AST::Node* arg, int offset = 0);
00616 IntSharedArray arg2intsharedarray(AST::Node* arg, int offset = 0);
00618 IntArgs arg2boolargs(AST::Node* arg, int offset = 0);
00620 IntSharedArray arg2boolsharedarray(AST::Node* arg, int offset = 0);
00622 IntSet arg2intset(AST::Node* n);
00624 IntSetArgs arg2intsetargs(AST::Node* arg, int offset = 0);
00626 IntVarArgs arg2intvarargs(AST::Node* arg, int offset = 0);
00628 BoolVarArgs arg2boolvarargs(AST::Node* arg, int offset = 0, int siv=-1);
00630 BoolVar arg2BoolVar(AST::Node* n);
00632 IntVar arg2IntVar(AST::Node* n);
00634 TupleSet arg2tupleset(AST::Node* n, int noOfVars);
00636 bool isBoolArray(AST::Node* b, int& singleInt);
00637 #ifdef GECODE_HAS_SET_VARS
00638
00639 SetVar arg2SetVar(AST::Node* n);
00641 SetVarArgs arg2setvarargs(AST::Node* arg, int offset = 0, int doffset = 0,
00642 const IntSet& od=IntSet::empty);
00643 #endif
00644 #ifdef GECODE_HAS_FLOAT_VARS
00645
00646 FloatValArgs arg2floatargs(AST::Node* arg, int offset = 0);
00648 FloatVar arg2FloatVar(AST::Node* n);
00650 FloatVarArgs arg2floatvarargs(AST::Node* arg, int offset = 0);
00651 #endif
00652
00653 IntPropLevel ann2ipl(AST::Node* ann);
00655 DFA getSharedDFA(DFA& a);
00657 };
00658
00660 class GECODE_VTABLE_EXPORT Error {
00661 private:
00662 const std::string msg;
00663 public:
00664 Error(const std::string& where, const std::string& what)
00665 : msg(where+": "+what) {}
00666 const std::string& toString(void) const { return msg; }
00667 };
00668
00674 GECODE_FLATZINC_EXPORT
00675 FlatZincSpace* parse(const std::string& fileName,
00676 Printer& p, std::ostream& err = std::cerr,
00677 FlatZincSpace* fzs=NULL, Rnd& rnd=defrnd);
00678
00684 GECODE_FLATZINC_EXPORT
00685 FlatZincSpace* parse(std::istream& is,
00686 Printer& p, std::ostream& err = std::cerr,
00687 FlatZincSpace* fzs=NULL, Rnd& rnd=defrnd);
00688
00689 }}
00690
00691 #endif
00692
00693
