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::DoubleOption _parallel;
00163 Gecode::Driver::BoolOption _free;
00164 Gecode::Driver::StringOption _search;
00165 Gecode::Driver::UnsignedIntOption _c_d;
00166 Gecode::Driver::UnsignedIntOption _a_d;
00167 Gecode::Driver::UnsignedIntOption _node;
00168 Gecode::Driver::UnsignedIntOption _fail;
00169 Gecode::Driver::UnsignedIntOption _time;
00170
00171
00173
00174 Gecode::Driver::StringOption _mode;
00175 Gecode::Driver::StringOption _print;
00176
00177 public:
00178 enum SearchOptions {
00179 FZ_SEARCH_BAB,
00180 FZ_SEARCH_RESTART
00181 };
00183 FlatZincOptions(const char* s)
00184 : Gecode::BaseOptions(s),
00185 _solutions("-solutions","number of solutions (0 = all)",1),
00186 _allSolutions("--all", "return all solutions (equal to -solutions 0)"),
00187 _threads("-threads","number of threads (0 = #processing units)",
00188 Gecode::Search::Config::threads),
00189 _parallel("--parallel", "equivalent to -threads",
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 _mode("-mode","how to execute script",Gecode::SM_SOLUTION),
00199 _print("-print","which solutions to print",0) {
00200
00201 _search.add(FZ_SEARCH_BAB, "bab");
00202 _search.add(FZ_SEARCH_RESTART, "restart");
00203 _mode.add(Gecode::SM_SOLUTION, "solution");
00204 _mode.add(Gecode::SM_STAT, "stat");
00205 _mode.add(Gecode::SM_GIST, "gist");
00206 _print.add(0,"all");
00207 _print.add(1,"last");
00208 add(_solutions); add(_threads); add(_c_d); add(_a_d);
00209 add(_allSolutions);
00210 add(_parallel);
00211 add(_free);
00212 add(_search);
00213 add(_node); add(_fail); add(_time);
00214 add(_mode);
00215 add(_print);
00216 }
00217
00218 void parse(int& argc, char* argv[]) {
00219 Gecode::BaseOptions::parse(argc,argv);
00220 if (_allSolutions.value())
00221 _solutions.value(0);
00222 if (_parallel.value() != Gecode::Search::Config::threads &&
00223 _threads.value() == Gecode::Search::Config::threads)
00224 _threads.value(_parallel.value());
00225 }
00226
00227 virtual void help(void) {
00228 std::cerr << "Gecode FlatZinc interpreter" << std::endl
00229 << " - Supported FlatZinc version: " << GECODE_FLATZINC_VERSION
00230 << std::endl << std::endl;
00231 Gecode::BaseOptions::help();
00232 }
00233
00234 unsigned int solutions(void) const { return _solutions.value(); }
00235 double threads(void) const { return _threads.value(); }
00236 bool free(void) const { return _free.value(); }
00237 SearchOptions search(void) const {
00238 return static_cast<SearchOptions>(_search.value());
00239 }
00240 unsigned int c_d(void) const { return _c_d.value(); }
00241 unsigned int a_d(void) const { return _a_d.value(); }
00242 unsigned int node(void) const { return _node.value(); }
00243 unsigned int fail(void) const { return _fail.value(); }
00244 unsigned int time(void) const { return _time.value(); }
00245 unsigned int print(void) const { return _print.value(); }
00246 Gecode::ScriptMode mode(void) const {
00247 return static_cast<Gecode::ScriptMode>(_mode.value());
00248 }
00249 };
00250
00255 class GECODE_FLATZINC_EXPORT FlatZincSpace : public Space {
00256 public:
00257 enum Meth {
00258 SAT,
00259 MIN,
00260 MAX
00261 };
00262 protected:
00264 int intVarCount;
00266 int boolVarCount;
00268 int setVarCount;
00269
00271 int _optVar;
00272
00274 Meth _method;
00275
00277 AST::Array* _solveAnnotations;
00278
00280 FlatZincSpace(bool share, FlatZincSpace&);
00281 private:
00283 template<template<class> class Engine>
00284 void
00285 runEngine(std::ostream& out, const Printer& p,
00286 const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00287 void
00288 branchWithPlugin(AST::Node* ann);
00289 public:
00291 Gecode::IntVarArray iv;
00293 std::vector<bool> iv_introduced;
00295 int* iv_boolalias;
00297 Gecode::BoolVarArray bv;
00299 std::vector<bool> bv_introduced;
00300 #ifdef GECODE_HAS_SET_VARS
00301
00302 Gecode::SetVarArray sv;
00304 std::vector<bool> sv_introduced;
00305 #endif
00306
00307 FlatZincSpace(void);
00308
00310 ~FlatZincSpace(void);
00311
00313 void init(int intVars, int boolVars, int setVars);
00314
00316 void newIntVar(IntVarSpec* vs);
00318 void aliasBool2Int(int iv, int bv);
00320 int aliasBool2Int(int iv);
00322 void newBoolVar(BoolVarSpec* vs);
00324 void newSetVar(SetVarSpec* vs);
00325
00327 void postConstraint(const ConExpr& ce, AST::Node* annotation);
00328
00330 void solve(AST::Array* annotation);
00332 void minimize(int var, AST::Array* annotation);
00334 void maximize(int var, AST::Array* annotation);
00335
00337 void run(std::ostream& out, const Printer& p,
00338 const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00339
00341 void print(std::ostream& out, const Printer& p) const;
00342
00351 void shrinkArrays(Printer& p);
00352
00354 Meth method(void) const;
00355
00357 int optVar(void) const;
00358
00365 void createBranchers(AST::Node* ann, bool ignoreUnknown,
00366 std::ostream& err = std::cerr);
00367
00369 AST::Array* solveAnnotations(void) const;
00370
00372 virtual void constrain(const Space& s);
00374 virtual Gecode::Space* copy(bool share);
00375 };
00376
00378 class Error {
00379 private:
00380 const std::string msg;
00381 public:
00382 Error(const std::string& where, const std::string& what)
00383 : msg(where+": "+what) {}
00384 const std::string& toString(void) const { return msg; }
00385 };
00386
00392 GECODE_FLATZINC_EXPORT
00393 FlatZincSpace* parse(const std::string& fileName,
00394 Printer& p, std::ostream& err = std::cerr,
00395 FlatZincSpace* fzs=NULL);
00396
00402 GECODE_FLATZINC_EXPORT
00403 FlatZincSpace* parse(std::istream& is,
00404 Printer& p, std::ostream& err = std::cerr,
00405 FlatZincSpace* fzs=NULL);
00406
00407 }}
00408
00409 #endif
00410
00411