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
00050
00051
00052
00053
00054 #if !defined(GECODE_STATIC_LIBS) && \
00055 (defined(__CYGWIN__) || defined(__MINGW32__) || defined(_MSC_VER))
00056
00057 #ifdef GECODE_BUILD_FLATZINC
00058 #define GECODE_FLATZINC_EXPORT __declspec( dllexport )
00059 #else
00060 #define GECODE_FLATZINC_EXPORT __declspec( dllimport )
00061 #endif
00062
00063 #else
00064
00065 #ifdef GECODE_GCC_HAS_CLASS_VISIBILITY
00066
00067 #define GECODE_FLATZINC_EXPORT __attribute__ ((visibility("default")))
00068
00069 #else
00070
00071 #define GECODE_FLATZINC_EXPORT
00072
00073 #endif
00074 #endif
00075
00076
00077 #ifndef GECODE_BUILD_FLATZINC
00078 #define GECODE_LIBRARY_NAME "FlatZinc"
00079 #include <gecode/support/auto-link.hpp>
00080 #endif
00081
00082 #include <gecode/driver.hh>
00083
00084 #include <gecode/flatzinc/conexpr.hh>
00085 #include <gecode/flatzinc/ast.hh>
00086 #include <gecode/flatzinc/varspec.hh>
00087
00097 namespace Gecode { namespace FlatZinc {
00098
00103 class GECODE_FLATZINC_EXPORT Printer {
00104 private:
00105 AST::Array* _output;
00106 void printElem(std::ostream& out,
00107 AST::Node* ai,
00108 const Gecode::IntVarArray& iv,
00109 const Gecode::BoolVarArray& bv
00110 #ifdef GECODE_HAS_SET_VARS
00111 ,
00112 const Gecode::SetVarArray& sv
00113 #endif
00114 ) const;
00115 public:
00116 Printer(void) : _output(NULL) {}
00117 void init(AST::Array* output);
00118
00119 void print(std::ostream& out,
00120 const Gecode::IntVarArray& iv,
00121 const Gecode::BoolVarArray& bv
00122 #ifdef GECODE_HAS_SET_VARS
00123 ,
00124 const Gecode::SetVarArray& sv
00125 #endif
00126 ) const;
00127
00128 ~Printer(void);
00129 private:
00130 Printer(const Printer&);
00131 Printer& operator=(const Printer&);
00132 };
00133
00138 class FlatZincOptions : public Gecode::BaseOptions {
00139 protected:
00141
00142 Gecode::Driver::UnsignedIntOption _solutions;
00143 Gecode::Driver::BoolOption _allSolutions;
00144 Gecode::Driver::DoubleOption _threads;
00145 Gecode::Driver::BoolOption _parallel;
00146 Gecode::Driver::BoolOption _free;
00147 Gecode::Driver::UnsignedIntOption _c_d;
00148 Gecode::Driver::UnsignedIntOption _a_d;
00149 Gecode::Driver::UnsignedIntOption _node;
00150 Gecode::Driver::UnsignedIntOption _fail;
00151 Gecode::Driver::UnsignedIntOption _time;
00152
00153
00155
00156 Gecode::Driver::StringOption _mode;
00157
00158 public:
00160 FlatZincOptions(const char* s)
00161 : Gecode::BaseOptions(s),
00162 _solutions("-solutions","number of solutions (0 = all)",1),
00163 _allSolutions("--all", "return all solutions (equal to -solutions 0)"),
00164 _threads("-threads","number of threads (0 = #processing units)",
00165 Gecode::Search::Config::threads),
00166 _parallel("--parallel", "use parallel search (equal to -threads 0)"),
00167 _free("--free", "no need to follow search-specification"),
00168 _c_d("-c-d","recomputation commit distance",Gecode::Search::Config::c_d),
00169 _a_d("-a-d","recomputation adaption distance",Gecode::Search::Config::a_d),
00170 _node("-node","node cutoff (0 = none, solution mode)"),
00171 _fail("-fail","failure cutoff (0 = none, solution mode)"),
00172 _time("-time","time (in ms) cutoff (0 = none, solution mode)"),
00173 _mode("-mode","how to execute script",Gecode::SM_SOLUTION) {
00174
00175 _mode.add(Gecode::SM_SOLUTION, "solution");
00176 _mode.add(Gecode::SM_STAT, "stat");
00177 _mode.add(Gecode::SM_GIST, "gist");
00178 add(_solutions); add(_threads); add(_c_d); add(_a_d);
00179 add(_allSolutions);
00180 add(_parallel);
00181 add(_free);
00182 add(_node); add(_fail); add(_time);
00183 add(_mode);
00184 }
00185
00186 void parse(int& argc, char* argv[]) {
00187 Gecode::BaseOptions::parse(argc,argv);
00188 if (_allSolutions.value())
00189 _solutions.value(0);
00190 if (_parallel.value())
00191 _threads.value(0);
00192 }
00193
00194 unsigned int solutions(void) const { return _solutions.value(); }
00195 double threads(void) const { return _threads.value(); }
00196 bool free(void) const { return _free.value(); }
00197 unsigned int c_d(void) const { return _c_d.value(); }
00198 unsigned int a_d(void) const { return _a_d.value(); }
00199 unsigned int node(void) const { return _node.value(); }
00200 unsigned int fail(void) const { return _fail.value(); }
00201 unsigned int time(void) const { return _time.value(); }
00202 Gecode::ScriptMode mode(void) const {
00203 return static_cast<Gecode::ScriptMode>(_mode.value());
00204 }
00205 };
00206
00211 class GECODE_FLATZINC_EXPORT FlatZincSpace : public Space {
00212 public:
00213 enum Meth {
00214 SAT,
00215 MIN,
00216 MAX
00217 };
00218 protected:
00220 int intVarCount;
00222 int boolVarCount;
00224 int setVarCount;
00225
00227 int _optVar;
00228
00230 Meth _method;
00231
00233 void parseSolveAnn(AST::Array* ann);
00234
00236 FlatZincSpace(bool share, FlatZincSpace&);
00237 private:
00239 template<template<class> class Engine>
00240 void
00241 runEngine(std::ostream& out, const Printer& p,
00242 const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00243 public:
00245 Gecode::IntVarArray iv;
00247 std::vector<bool> iv_introduced;
00249 Gecode::BoolVarArray bv;
00251 std::vector<bool> bv_introduced;
00252 #ifdef GECODE_HAS_SET_VARS
00254 Gecode::SetVarArray sv;
00256 std::vector<bool> sv_introduced;
00257 #endif
00259 FlatZincSpace(int intVars, int boolVars, int setVars);
00260
00262 void newIntVar(IntVarSpec* vs);
00264 void newBoolVar(BoolVarSpec* vs);
00266 void newSetVar(SetVarSpec* vs);
00267
00269 void postConstraint(const ConExpr& ce, AST::Node* annotation);
00270
00272 void solve(AST::Array* annotation);
00274 void minimize(int var, AST::Array* annotation);
00276 void maximize(int var, AST::Array* annotation);
00277
00279 void run(std::ostream& out, const Printer& p,
00280 const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00281
00283 void print(std::ostream& out, const Printer& p) const;
00284
00286 Meth method(void);
00287
00289 virtual void constrain(const Space& s);
00291 virtual Gecode::Space* copy(bool share);
00292 };
00293
00295 class Error {
00296 private:
00297 const std::string msg;
00298 public:
00299 Error(const std::string& where, const std::string& what)
00300 : msg(where+": "+what) {}
00301 const std::string& toString(void) const { return msg; }
00302 };
00303
00305 GECODE_FLATZINC_EXPORT
00306 FlatZincSpace* solve(const std::string& fileName,
00307 Printer& p, std::ostream& err = std::cerr);
00308
00310 GECODE_FLATZINC_EXPORT
00311 FlatZincSpace* solve(std::istream& is,
00312 Printer& p, std::ostream& err = std::cerr);
00313
00314 }}
00315
00316 #endif
00317
00318