flatzinc.hh
Go to the documentation of this file.
00001 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */ 00002 /* 00003 * Main authors: 00004 * Guido Tack <tack@gecode.org> 00005 * 00006 * Copyright: 00007 * Guido Tack, 2007 00008 * 00009 * Last modified: 00010 * $Date: 2011-01-13 22:42:12 +0100 (Thu, 13 Jan 2011) $ by $Author: tack $ 00011 * $Revision: 11531 $ 00012 * 00013 * This file is part of Gecode, the generic constraint 00014 * development environment: 00015 * http://www.gecode.org 00016 * 00017 * Permission is hereby granted, free of charge, to any person obtaining 00018 * a copy of this software and associated documentation files (the 00019 * "Software"), to deal in the Software without restriction, including 00020 * without limitation the rights to use, copy, modify, merge, publish, 00021 * distribute, sublicense, and/or sell copies of the Software, and to 00022 * permit persons to whom the Software is furnished to do so, subject to 00023 * the following conditions: 00024 * 00025 * The above copyright notice and this permission notice shall be 00026 * included in all copies or substantial portions of the Software. 00027 * 00028 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, 00029 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 00030 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND 00031 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE 00032 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION 00033 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION 00034 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. 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 * Support for DLLs under Windows 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 // Configure auto-linking 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, //< Branch-and-bound search 00180 FZ_SEARCH_RESTART //< Restart search 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, //< Solve as satisfaction problem 00259 MIN, //< Solve as minimization problem 00260 MAX //< Solve as maximization problem 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 // STATISTICS: flatzinc-any