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 _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", "use parallel search (equal to -threads 0)"),
00190 _free("--free", "no need to follow search-specification"),
00191 _search("-search","search engine variant", FZ_SEARCH_BAB),
00192 _c_d("-c-d","recomputation commit distance",Gecode::Search::Config::c_d),
00193 _a_d("-a-d","recomputation adaption distance",Gecode::Search::Config::a_d),
00194 _node("-node","node cutoff (0 = none, solution mode)"),
00195 _fail("-fail","failure cutoff (0 = none, solution mode)"),
00196 _time("-time","time (in ms) cutoff (0 = none, solution mode)"),
00197 _mode("-mode","how to execute script",Gecode::SM_SOLUTION),
00198 _print("-print","which solutions to print",0) {
00199
00200 _search.add(FZ_SEARCH_BAB, "bab");
00201 _search.add(FZ_SEARCH_RESTART, "restart");
00202 _mode.add(Gecode::SM_SOLUTION, "solution");
00203 _mode.add(Gecode::SM_STAT, "stat");
00204 _mode.add(Gecode::SM_GIST, "gist");
00205 _print.add(0,"all");
00206 _print.add(1,"last");
00207 add(_solutions); add(_threads); add(_c_d); add(_a_d);
00208 add(_allSolutions);
00209 add(_parallel);
00210 add(_free);
00211 add(_search);
00212 add(_node); add(_fail); add(_time);
00213 add(_mode);
00214 add(_print);
00215 }
00216
00217 void parse(int& argc, char* argv[]) {
00218 Gecode::BaseOptions::parse(argc,argv);
00219 if (_allSolutions.value())
00220 _solutions.value(0);
00221 if (_parallel.value())
00222 _threads.value(0);
00223 }
00224
00225 unsigned int solutions(void) const { return _solutions.value(); }
00226 double threads(void) const { return _threads.value(); }
00227 bool free(void) const { return _free.value(); }
00228 SearchOptions search(void) const {
00229 return static_cast<SearchOptions>(_search.value());
00230 }
00231 unsigned int c_d(void) const { return _c_d.value(); }
00232 unsigned int a_d(void) const { return _a_d.value(); }
00233 unsigned int node(void) const { return _node.value(); }
00234 unsigned int fail(void) const { return _fail.value(); }
00235 unsigned int time(void) const { return _time.value(); }
00236 unsigned int print(void) const { return _print.value(); }
00237 Gecode::ScriptMode mode(void) const {
00238 return static_cast<Gecode::ScriptMode>(_mode.value());
00239 }
00240 };
00241
00246 class GECODE_FLATZINC_EXPORT FlatZincSpace : public Space {
00247 public:
00248 enum Meth {
00249 SAT,
00250 MIN,
00251 MAX
00252 };
00253 protected:
00255 int intVarCount;
00257 int boolVarCount;
00259 int setVarCount;
00260
00262 int _optVar;
00263
00265 Meth _method;
00266
00268 AST::Array* _solveAnnotations;
00269
00271 FlatZincSpace(bool share, FlatZincSpace&);
00272 private:
00274 template<template<class> class Engine>
00275 void
00276 runEngine(std::ostream& out, const Printer& p,
00277 const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00278 void
00279 branchWithPlugin(AST::Node* ann);
00280 public:
00282 Gecode::IntVarArray iv;
00284 std::vector<bool> iv_introduced;
00286 int* iv_boolalias;
00288 Gecode::BoolVarArray bv;
00290 std::vector<bool> bv_introduced;
00291 #ifdef GECODE_HAS_SET_VARS
00292
00293 Gecode::SetVarArray sv;
00295 std::vector<bool> sv_introduced;
00296 #endif
00297
00298 FlatZincSpace(void);
00299
00301 ~FlatZincSpace(void);
00302
00304 void init(int intVars, int boolVars, int setVars);
00305
00307 void newIntVar(IntVarSpec* vs);
00309 void aliasBool2Int(int iv, int bv);
00311 int aliasBool2Int(int iv);
00313 void newBoolVar(BoolVarSpec* vs);
00315 void newSetVar(SetVarSpec* vs);
00316
00318 void postConstraint(const ConExpr& ce, AST::Node* annotation);
00319
00321 void solve(AST::Array* annotation);
00323 void minimize(int var, AST::Array* annotation);
00325 void maximize(int var, AST::Array* annotation);
00326
00328 void run(std::ostream& out, const Printer& p,
00329 const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00330
00332 void print(std::ostream& out, const Printer& p) const;
00333
00342 void shrinkArrays(Printer& p);
00343
00345 Meth method(void) const;
00346
00348 int optVar(void) const;
00349
00356 void createBranchers(AST::Node* ann, bool ignoreUnknown,
00357 std::ostream& err = std::cerr);
00358
00360 AST::Array* solveAnnotations(void) const;
00361
00363 virtual void constrain(const Space& s);
00365 virtual Gecode::Space* copy(bool share);
00366 };
00367
00369 class Error {
00370 private:
00371 const std::string msg;
00372 public:
00373 Error(const std::string& where, const std::string& what)
00374 : msg(where+": "+what) {}
00375 const std::string& toString(void) const { return msg; }
00376 };
00377
00383 GECODE_FLATZINC_EXPORT
00384 FlatZincSpace* parse(const std::string& fileName,
00385 Printer& p, std::ostream& err = std::cerr,
00386 FlatZincSpace* fzs=NULL);
00387
00393 GECODE_FLATZINC_EXPORT
00394 FlatZincSpace* parse(std::istream& is,
00395 Printer& p, std::ostream& err = std::cerr,
00396 FlatZincSpace* fzs=NULL);
00397
00398 }}
00399
00400 #endif
00401
00402