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
00049 #include <map>
00050
00051
00052
00053
00054
00055
00056 #if !defined(GECODE_STATIC_LIBS) && \
00057 (defined(__CYGWIN__) || defined(__MINGW32__) || defined(_MSC_VER))
00058
00059 #ifdef GECODE_BUILD_FLATZINC
00060 #define GECODE_FLATZINC_EXPORT __declspec( dllexport )
00061 #else
00062 #define GECODE_FLATZINC_EXPORT __declspec( dllimport )
00063 #endif
00064
00065 #else
00066
00067 #ifdef GECODE_GCC_HAS_CLASS_VISIBILITY
00068
00069 #define GECODE_FLATZINC_EXPORT __attribute__ ((visibility("default")))
00070
00071 #else
00072
00073 #define GECODE_FLATZINC_EXPORT
00074
00075 #endif
00076 #endif
00077
00078
00079 #ifndef GECODE_BUILD_FLATZINC
00080 #define GECODE_LIBRARY_NAME "FlatZinc"
00081 #include <gecode/support/auto-link.hpp>
00082 #endif
00083
00084 #include <gecode/driver.hh>
00085
00086 #include <gecode/flatzinc/conexpr.hh>
00087 #include <gecode/flatzinc/ast.hh>
00088 #include <gecode/flatzinc/varspec.hh>
00089
00099 namespace Gecode { namespace FlatZinc {
00100
00105 class GECODE_FLATZINC_EXPORT Printer {
00106 private:
00107 AST::Array* _output;
00108 void printElem(std::ostream& out,
00109 AST::Node* ai,
00110 const Gecode::IntVarArray& iv,
00111 const Gecode::BoolVarArray& bv
00112 #ifdef GECODE_HAS_SET_VARS
00113 ,
00114 const Gecode::SetVarArray& sv
00115 #endif
00116 ) const;
00117 public:
00118 Printer(void) : _output(NULL) {}
00119 void init(AST::Array* output);
00120
00121 void print(std::ostream& out,
00122 const Gecode::IntVarArray& iv,
00123 const Gecode::BoolVarArray& bv
00124 #ifdef GECODE_HAS_SET_VARS
00125 ,
00126 const Gecode::SetVarArray& sv
00127 #endif
00128 ) const;
00129
00130 ~Printer(void);
00131
00132 void shrinkElement(AST::Node* node,
00133 std::map<int,int>& iv, std::map<int,int>& bv,
00134 std::map<int,int>& sv);
00135
00136 void shrinkArrays(Space& home,
00137 int& optVar,
00138 Gecode::IntVarArray& iv,
00139 Gecode::BoolVarArray& bv
00140 #ifdef GECODE_HAS_SET_VARS
00141 ,
00142 Gecode::SetVarArray& sv
00143 #endif
00144 );
00145
00146 private:
00147 Printer(const Printer&);
00148 Printer& operator=(const Printer&);
00149 };
00150
00155 class FlatZincOptions : public Gecode::BaseOptions {
00156 protected:
00158
00159 Gecode::Driver::UnsignedIntOption _solutions;
00160 Gecode::Driver::BoolOption _allSolutions;
00161 Gecode::Driver::DoubleOption _threads;
00162 Gecode::Driver::BoolOption _free;
00163 Gecode::Driver::StringOption _search;
00164 Gecode::Driver::UnsignedIntOption _c_d;
00165 Gecode::Driver::UnsignedIntOption _a_d;
00166 Gecode::Driver::UnsignedIntOption _node;
00167 Gecode::Driver::UnsignedIntOption _fail;
00168 Gecode::Driver::UnsignedIntOption _time;
00169 Gecode::Driver::IntOption _seed;
00170
00171
00173
00174 Gecode::Driver::StringOption _mode;
00175 Gecode::Driver::BoolOption _stat;
00176 Gecode::Driver::StringOption _print;
00177 Gecode::Driver::StringValueOption _output;
00178
00179 public:
00180 enum SearchOptions {
00181 FZ_SEARCH_BAB,
00182 FZ_SEARCH_RESTART
00183 };
00185 FlatZincOptions(const char* s)
00186 : Gecode::BaseOptions(s),
00187 _solutions("-n","number of solutions (0 = all)",1),
00188 _allSolutions("-a", "return all solutions (equal to -solutions 0)"),
00189 _threads("-p","number of threads (0 = #processing units)",
00190 Gecode::Search::Config::threads),
00191 _free("--free", "no need to follow search-specification"),
00192 _search("-search","search engine variant", FZ_SEARCH_BAB),
00193 _c_d("-c-d","recomputation commit distance",Gecode::Search::Config::c_d),
00194 _a_d("-a-d","recomputation adaption distance",Gecode::Search::Config::a_d),
00195 _node("-node","node cutoff (0 = none, solution mode)"),
00196 _fail("-fail","failure cutoff (0 = none, solution mode)"),
00197 _time("-time","time (in ms) cutoff (0 = none, solution mode)"),
00198 _seed("-r","random seed",0),
00199 _mode("-mode","how to execute script",Gecode::SM_SOLUTION),
00200 _stat("-s","emit statistics"),
00201 _print("-print","which solutions to print",0),
00202 _output("-o","file to send output to") {
00203
00204 _search.add(FZ_SEARCH_BAB, "bab");
00205 _search.add(FZ_SEARCH_RESTART, "restart");
00206 _mode.add(Gecode::SM_SOLUTION, "solution");
00207 _mode.add(Gecode::SM_STAT, "stat");
00208 _mode.add(Gecode::SM_GIST, "gist");
00209 _print.add(0,"all");
00210 _print.add(1,"last");
00211 add(_solutions); add(_threads); add(_c_d); add(_a_d);
00212 add(_allSolutions);
00213 add(_free);
00214 add(_search);
00215 add(_node); add(_fail); add(_time);
00216 add(_seed);
00217 add(_mode); add(_stat);
00218 add(_print); add(_output);
00219 }
00220
00221 void parse(int& argc, char* argv[]) {
00222 Gecode::BaseOptions::parse(argc,argv);
00223 if (_allSolutions.value())
00224 _solutions.value(0);
00225 if (_stat.value())
00226 _mode.value(Gecode::SM_STAT);
00227 }
00228
00229 virtual void help(void) {
00230 std::cerr << "Gecode FlatZinc interpreter" << std::endl
00231 << " - Supported FlatZinc version: " << GECODE_FLATZINC_VERSION
00232 << std::endl << std::endl;
00233 Gecode::BaseOptions::help();
00234 }
00235
00236 unsigned int solutions(void) const { return _solutions.value(); }
00237 double threads(void) const { return _threads.value(); }
00238 bool free(void) const { return _free.value(); }
00239 SearchOptions search(void) const {
00240 return static_cast<SearchOptions>(_search.value());
00241 }
00242 unsigned int c_d(void) const { return _c_d.value(); }
00243 unsigned int a_d(void) const { return _a_d.value(); }
00244 unsigned int node(void) const { return _node.value(); }
00245 unsigned int fail(void) const { return _fail.value(); }
00246 unsigned int time(void) const { return _time.value(); }
00247 int seed(void) const { return _seed.value(); }
00248 unsigned int print(void) const { return _print.value(); }
00249 const char* output(void) const { return _output.value(); }
00250 Gecode::ScriptMode mode(void) const {
00251 return static_cast<Gecode::ScriptMode>(_mode.value());
00252 }
00253 };
00254
00259 class GECODE_FLATZINC_EXPORT FlatZincSpace : public Space {
00260 public:
00261 enum Meth {
00262 SAT,
00263 MIN,
00264 MAX
00265 };
00266 protected:
00268 int intVarCount;
00270 int boolVarCount;
00272 int setVarCount;
00273
00275 int _optVar;
00276
00278 Meth _method;
00279
00281 AST::Array* _solveAnnotations;
00282
00284 FlatZincSpace(bool share, FlatZincSpace&);
00285 private:
00287 template<template<class> class Engine>
00288 void
00289 runEngine(std::ostream& out, const Printer& p,
00290 const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00291 void
00292 branchWithPlugin(AST::Node* ann);
00293 public:
00295 Gecode::IntVarArray iv;
00297 std::vector<bool> iv_introduced;
00299 int* iv_boolalias;
00301 Gecode::BoolVarArray bv;
00303 std::vector<bool> bv_introduced;
00304 #ifdef GECODE_HAS_SET_VARS
00305
00306 Gecode::SetVarArray sv;
00308 std::vector<bool> sv_introduced;
00309 #endif
00310
00311 FlatZincSpace(void);
00312
00314 ~FlatZincSpace(void);
00315
00317 void init(int intVars, int boolVars, int setVars);
00318
00320 void newIntVar(IntVarSpec* vs);
00322 void aliasBool2Int(int iv, int bv);
00324 int aliasBool2Int(int iv);
00326 void newBoolVar(BoolVarSpec* vs);
00328 void newSetVar(SetVarSpec* vs);
00329
00331 void postConstraint(const ConExpr& ce, AST::Node* annotation);
00332
00334 void solve(AST::Array* annotation);
00336 void minimize(int var, AST::Array* annotation);
00338 void maximize(int var, AST::Array* annotation);
00339
00341 void run(std::ostream& out, const Printer& p,
00342 const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00343
00345 void print(std::ostream& out, const Printer& p) const;
00346
00355 void shrinkArrays(Printer& p);
00356
00358 Meth method(void) const;
00359
00361 int optVar(void) const;
00362
00372 void createBranchers(AST::Node* ann,
00373 int seed,
00374 bool ignoreUnknown,
00375 std::ostream& err = std::cerr);
00376
00378 AST::Array* solveAnnotations(void) const;
00379
00381 virtual void constrain(const Space& s);
00383 virtual Gecode::Space* copy(bool share);
00384 };
00385
00387 class Error {
00388 private:
00389 const std::string msg;
00390 public:
00391 Error(const std::string& where, const std::string& what)
00392 : msg(where+": "+what) {}
00393 const std::string& toString(void) const { return msg; }
00394 };
00395
00401 GECODE_FLATZINC_EXPORT
00402 FlatZincSpace* parse(const std::string& fileName,
00403 Printer& p, std::ostream& err = std::cerr,
00404 FlatZincSpace* fzs=NULL);
00405
00411 GECODE_FLATZINC_EXPORT
00412 FlatZincSpace* parse(std::istream& is,
00413 Printer& p, std::ostream& err = std::cerr,
00414 FlatZincSpace* fzs=NULL);
00415
00416 }}
00417
00418 #endif
00419
00420