Generated on Thu Apr 11 13:58:54 2019 for Gecode by doxygen 1.6.3

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  *  Contributing authors:
00007  *     Gabriel Hjort Blindell <gabriel.hjort.blindell@gmail.com>
00008  *
00009  *  Copyright:
00010  *     Guido Tack, 2007-2012
00011  *     Gabriel Hjort Blindell, 2012
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 #ifdef GECODE_HAS_FLOAT_VARS
00049 #include <gecode/float.hh>
00050 #endif
00051 #include <map>
00052 
00053 /*
00054  * Support for DLLs under Windows
00055  *
00056  */
00057 
00058 #if !defined(GECODE_STATIC_LIBS) && \
00059     (defined(__CYGWIN__) || defined(__MINGW32__) || defined(_MSC_VER))
00060 
00061 #ifdef GECODE_BUILD_FLATZINC
00062 #define GECODE_FLATZINC_EXPORT __declspec( dllexport )
00063 #else
00064 #define GECODE_FLATZINC_EXPORT __declspec( dllimport )
00065 #endif
00066 
00067 #else
00068 
00069 #ifdef GECODE_GCC_HAS_CLASS_VISIBILITY
00070 
00071 #define GECODE_FLATZINC_EXPORT __attribute__ ((visibility("default")))
00072 
00073 #else
00074 
00075 #define GECODE_FLATZINC_EXPORT
00076 
00077 #endif
00078 #endif
00079 
00080 // Configure auto-linking
00081 #ifndef GECODE_BUILD_FLATZINC
00082 #define GECODE_LIBRARY_NAME "FlatZinc"
00083 #include <gecode/support/auto-link.hpp>
00084 #endif
00085 
00086 #include <gecode/driver.hh>
00087 
00088 #include <gecode/flatzinc/conexpr.hh>
00089 #include <gecode/flatzinc/ast.hh>
00090 #include <gecode/flatzinc/varspec.hh>
00091 
00101 namespace Gecode { namespace FlatZinc {
00102 
00107   class GECODE_FLATZINC_EXPORT Printer {
00108   private:
00110     std::vector<std::string> iv_names;
00112     std::vector<std::string> bv_names;
00113 #ifdef GECODE_HAS_FLOAT_VARS
00114 
00115     std::vector<std::string> fv_names;
00116 #endif
00117 #ifdef GECODE_HAS_SET_VARS
00118 
00119     std::vector<std::string> sv_names;
00120 #endif
00121     AST::Array* _output;
00122     void printElem(std::ostream& out,
00123                    AST::Node* ai,
00124                    const Gecode::IntVarArray& iv,
00125                    const Gecode::BoolVarArray& bv
00126 #ifdef GECODE_HAS_SET_VARS
00127                    ,
00128                    const Gecode::SetVarArray& sv
00129 #endif
00130 #ifdef GECODE_HAS_FLOAT_VARS
00131                   ,
00132                   const Gecode::FloatVarArray& fv
00133 #endif
00134                    ) const;
00135     void printElemDiff(std::ostream& out,
00136                        AST::Node* ai,
00137                        const Gecode::IntVarArray& iv1,
00138                        const Gecode::IntVarArray& iv2,
00139                        const Gecode::BoolVarArray& bv1,
00140                        const Gecode::BoolVarArray& bv2
00141 #ifdef GECODE_HAS_SET_VARS
00142                        ,
00143                        const Gecode::SetVarArray& sv1,
00144                        const Gecode::SetVarArray& sv2
00145 #endif
00146 #ifdef GECODE_HAS_FLOAT_VARS
00147                        ,
00148                        const Gecode::FloatVarArray& fv1,
00149                        const Gecode::FloatVarArray& fv2
00150 #endif
00151                        ) const;
00152   public:
00153     Printer(void) : _output(NULL) {}
00154     void init(AST::Array* output);
00155 
00156     void print(std::ostream& out,
00157                const Gecode::IntVarArray& iv,
00158                const Gecode::BoolVarArray& bv
00159 #ifdef GECODE_HAS_SET_VARS
00160                ,
00161                const Gecode::SetVarArray& sv
00162 #endif
00163 #ifdef GECODE_HAS_FLOAT_VARS
00164                ,
00165                const Gecode::FloatVarArray& fv
00166 #endif
00167                ) const;
00168 
00169     void printDiff(std::ostream& out,
00170                const Gecode::IntVarArray& iv1, const Gecode::IntVarArray& iv2,
00171                const Gecode::BoolVarArray& bv1, const Gecode::BoolVarArray& bv2
00172 #ifdef GECODE_HAS_SET_VARS
00173                ,
00174                const Gecode::SetVarArray& sv1, const Gecode::SetVarArray& sv2
00175 #endif
00176 #ifdef GECODE_HAS_FLOAT_VARS
00177                ,
00178                const Gecode::FloatVarArray& fv1,
00179                const Gecode::FloatVarArray& fv2
00180 #endif
00181                ) const;
00182 
00183 
00184     ~Printer(void);
00185 
00186     void addIntVarName(const std::string& n);
00187     const std::string& intVarName(int i) const { return iv_names[i]; }
00188     void addBoolVarName(const std::string& n);
00189     const std::string& boolVarName(int i) const { return bv_names[i]; }
00190 #ifdef GECODE_HAS_FLOAT_VARS
00191     void addFloatVarName(const std::string& n);
00192     const std::string& floatVarName(int i) const { return fv_names[i]; }
00193 #endif
00194 #ifdef GECODE_HAS_SET_VARS
00195     void addSetVarName(const std::string& n);
00196     const std::string& setVarName(int i) const { return sv_names[i]; }
00197 #endif
00198 
00199     void shrinkElement(AST::Node* node,
00200                        std::map<int,int>& iv, std::map<int,int>& bv,
00201                        std::map<int,int>& sv, std::map<int,int>& fv);
00202 
00203     void shrinkArrays(Space& home,
00204                       int& optVar, bool optVarIsInt,
00205                       Gecode::IntVarArray& iv,
00206                       Gecode::BoolVarArray& bv
00207 #ifdef GECODE_HAS_SET_VARS
00208                       ,
00209                       Gecode::SetVarArray& sv
00210 #endif
00211 #ifdef GECODE_HAS_FLOAT_VARS
00212                       ,
00213                       Gecode::FloatVarArray& fv
00214 #endif
00215                      );
00216 
00217   private:
00218     Printer(const Printer&);
00219     Printer& operator=(const Printer&);
00220   };
00221 
00226   class FlatZincOptions : public Gecode::BaseOptions {
00227   protected:
00229 
00230       Gecode::Driver::IntOption         _solutions; 
00231       Gecode::Driver::BoolOption        _allSolutions; 
00232       Gecode::Driver::DoubleOption      _threads;   
00233       Gecode::Driver::BoolOption        _free; 
00234       Gecode::Driver::DoubleOption      _decay;       
00235       Gecode::Driver::UnsignedIntOption _c_d;       
00236       Gecode::Driver::UnsignedIntOption _a_d;       
00237       Gecode::Driver::UnsignedIntOption _node;      
00238       Gecode::Driver::UnsignedIntOption _fail;      
00239       Gecode::Driver::UnsignedIntOption _time;      
00240       Gecode::Driver::UnsignedIntOption _time_limit;  
00241       Gecode::Driver::IntOption         _seed;      
00242       Gecode::Driver::StringOption      _restart;   
00243       Gecode::Driver::DoubleOption      _r_base;    
00244       Gecode::Driver::UnsignedIntOption _r_scale;   
00245       Gecode::Driver::BoolOption        _nogoods;   
00246       Gecode::Driver::UnsignedIntOption _nogoods_limit; 
00247       Gecode::Driver::BoolOption        _interrupt; 
00248       Gecode::Driver::DoubleOption      _step;        
00249 
00250 
00252 
00253       Gecode::Driver::StringOption      _mode;       
00254       Gecode::Driver::BoolOption        _stat;       
00255       Gecode::Driver::StringValueOption _output;     
00256 
00257 #ifdef GECODE_HAS_CPPROFILER
00258 
00259       Gecode::Driver::IntOption         _profiler_id; 
00260       Gecode::Driver::UnsignedIntOption _profiler_port; 
00261       Gecode::Driver::BoolOption        _profiler_info; 
00262 
00263 #endif
00264 
00266   public:
00268     FlatZincOptions(const char* s)
00269     : Gecode::BaseOptions(s),
00270       _solutions("n","number of solutions (0 = all, -1 = one/best)",-1),
00271       _allSolutions("a", "return all solutions (equal to -n 0)"),
00272       _threads("p","number of threads (0 = #processing units)",
00273                Gecode::Search::Config::threads),
00274       _free("f", "free search, no need to follow search-specification"),
00275       _decay("decay","decay factor",0.99),
00276       _c_d("c-d","recomputation commit distance",Gecode::Search::Config::c_d),
00277       _a_d("a-d","recomputation adaption distance",Gecode::Search::Config::a_d),
00278       _node("node","node cutoff (0 = none, solution mode)"),
00279       _fail("fail","failure cutoff (0 = none, solution mode)"),
00280       _time("time","time (in ms) cutoff (0 = none, solution mode)"),
00281       _time_limit("t","time (in ms) cutoff (0 = none, solution mode)"),
00282       _seed("r","random seed",0),
00283       _restart("restart","restart sequence type",RM_NONE),
00284       _r_base("restart-base","base for geometric restart sequence",1.5),
00285       _r_scale("restart-scale","scale factor for restart sequence",250),
00286       _nogoods("nogoods","whether to use no-goods from restarts",false),
00287       _nogoods_limit("nogoods-limit","depth limit for no-good extraction",
00288                      Search::Config::nogoods_limit),
00289       _interrupt("interrupt","whether to catch Ctrl-C (true) or not (false)",
00290                  true),
00291       _step("step","step distance for float optimization",0.0),
00292       _mode("mode","how to execute script",Gecode::SM_SOLUTION),
00293       _stat("s","emit statistics"),
00294       _output("o","file to send output to")
00295 
00296 #ifdef GECODE_HAS_CPPROFILER
00297       ,
00298       _profiler_id("cpprofiler-id", "use this execution id with cpprofiler", 0),
00299       _profiler_port("cpprofiler-port", "connect to cpprofiler on this port", 6565),
00300       _profiler_info("cpprofiler-info", "send solution information to cpprofiler", false)
00301 
00302 #endif
00303     {
00304       _mode.add(Gecode::SM_SOLUTION, "solution");
00305       _mode.add(Gecode::SM_STAT, "stat");
00306       _mode.add(Gecode::SM_GIST, "gist");
00307       _mode.add(Gecode::SM_CPPROFILER, "cpprofiler");
00308       _restart.add(RM_NONE,"none");
00309       _restart.add(RM_CONSTANT,"constant");
00310       _restart.add(RM_LINEAR,"linear");
00311       _restart.add(RM_LUBY,"luby");
00312       _restart.add(RM_GEOMETRIC,"geometric");
00313 
00314       add(_solutions); add(_threads); add(_c_d); add(_a_d);
00315       add(_allSolutions);
00316       add(_free);
00317       add(_decay);
00318       add(_node); add(_fail); add(_time); add(_time_limit); add(_interrupt);
00319       add(_seed);
00320       add(_step);
00321       add(_restart); add(_r_base); add(_r_scale);
00322       add(_nogoods); add(_nogoods_limit);
00323       add(_mode); add(_stat);
00324       add(_output);
00325 #ifdef GECODE_HAS_CPPROFILER
00326       add(_profiler_id);
00327       add(_profiler_port);
00328       add(_profiler_info);
00329 #endif
00330     }
00331 
00332     void parse(int& argc, char* argv[]) {
00333       Gecode::BaseOptions::parse(argc,argv);
00334       if (_allSolutions.value() && _solutions.value()==-1) {
00335         _solutions.value(0);
00336       }
00337       if (_time_limit.value()) {
00338         _time.value(_time_limit.value());
00339       }
00340       if (_stat.value())
00341         _mode.value(Gecode::SM_STAT);
00342     }
00343 
00344     virtual void help(void) {
00345       std::cerr << "Gecode FlatZinc interpreter" << std::endl
00346                 << " - Supported FlatZinc version: " << GECODE_FLATZINC_VERSION
00347                 << std::endl << std::endl;
00348       Gecode::BaseOptions::help();
00349     }
00350 
00351     int solutions(void) const { return _solutions.value(); }
00352     bool allSolutions(void) const { return _allSolutions.value(); }
00353     double threads(void) const { return _threads.value(); }
00354     bool free(void) const { return _free.value(); }
00355     unsigned int c_d(void) const { return _c_d.value(); }
00356     unsigned int a_d(void) const { return _a_d.value(); }
00357     unsigned int node(void) const { return _node.value(); }
00358     unsigned int fail(void) const { return _fail.value(); }
00359     unsigned int time(void) const { return _time.value(); }
00360     int seed(void) const { return _seed.value(); }
00361     double step(void) const { return _step.value(); }
00362     const char* output(void) const { return _output.value(); }
00363 
00364     Gecode::ScriptMode mode(void) const {
00365       return static_cast<Gecode::ScriptMode>(_mode.value());
00366     }
00367 
00368     double decay(void) const { return _decay.value(); }
00369     RestartMode restart(void) const {
00370       return static_cast<RestartMode>(_restart.value());
00371     }
00372     void restart(RestartMode rm) {
00373       _restart.value(rm);
00374     }
00375     double restart_base(void) const { return _r_base.value(); }
00376     void restart_base(double d) { _r_base.value(d); }
00377     unsigned int restart_scale(void) const { return _r_scale.value(); }
00378     void restart_scale(int i) { _r_scale.value(i); }
00379     bool nogoods(void) const { return _nogoods.value(); }
00380     unsigned int nogoods_limit(void) const { return _nogoods_limit.value(); }
00381     bool interrupt(void) const { return _interrupt.value(); }
00382 
00383 #ifdef GECODE_HAS_CPPROFILER
00384 
00385     int profiler_id(void) const { return _profiler_id.value(); }
00386     unsigned int profiler_port(void) const { return _profiler_port.value(); }
00387     bool profiler_info(void) const { return _profiler_info.value(); }
00388 
00389 #endif
00390 
00391     void allSolutions(bool b) { _allSolutions.value(b); }
00392   };
00393 
00394   class BranchInformation : public SharedHandle {
00395   public:
00397     BranchInformation(void);
00399     BranchInformation(const BranchInformation& bi);
00401     void init(void);
00403     void add(BrancherGroup bg,
00404              const std::string& rel0,
00405              const std::string& rel1,
00406              const std::vector<std::string>& n);
00408     void print(const Brancher& b,
00409                unsigned int a, int i, int n, std::ostream& o) const;
00410 #ifdef GECODE_HAS_FLOAT_VARS
00411 
00412     void print(const Brancher& b,
00413                unsigned int a, int i, const FloatNumBranch& nl,
00414                std::ostream& o) const;
00415 #endif
00416   };
00417 
00419   GECODE_FLATZINC_EXPORT
00420   extern Rnd defrnd;
00421 
00422   class FlatZincSpaceInitData;
00423 
00428   class GECODE_FLATZINC_EXPORT FlatZincSpace : public Space {
00429   public:
00430     enum Meth {
00431       SAT, //< Solve as satisfaction problem
00432       MIN, //< Solve as minimization problem
00433       MAX  //< Solve as maximization problem
00434     };
00435   protected:
00437     FlatZincSpaceInitData* _initData;
00439     int intVarCount;
00441     int boolVarCount;
00443     int floatVarCount;
00445     int setVarCount;
00446 
00448     int _optVar;
00450     bool _optVarIsInt;
00451 
00453     Meth _method;
00454 
00456     unsigned int _lns;
00457 
00459     IntSharedArray _lnsInitialSolution;
00460 
00462     Rnd _random;
00463 
00465     AST::Array* _solveAnnotations;
00466 
00468     FlatZincSpace(FlatZincSpace&);
00469   private:
00471     template<template<class> class Engine>
00472     void
00473     runEngine(std::ostream& out, const Printer& p,
00474               const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00476     template<template<class> class Engine,
00477              template<class, template<class> class> class Meta>
00478     void
00479     runMeta(std::ostream& out, const Printer& p,
00480             const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00481     void
00482     branchWithPlugin(AST::Node* ann);
00483   public:
00485     Gecode::IntVarArray iv;
00487     Gecode::IntVarArray iv_aux;
00488 
00490     Gecode::IntVarArray iv_lns;
00491 
00493     std::vector<bool> iv_introduced;
00495     int* iv_boolalias;
00497     Gecode::BoolVarArray bv;
00499     Gecode::BoolVarArray bv_aux;
00501     std::vector<bool> bv_introduced;
00502 #ifdef GECODE_HAS_SET_VARS
00503 
00504     Gecode::SetVarArray sv;
00506     Gecode::SetVarArray sv_aux;
00508     std::vector<bool> sv_introduced;
00509 #endif
00510 #ifdef GECODE_HAS_FLOAT_VARS
00511 
00512     Gecode::FloatVarArray fv;
00514     Gecode::FloatVarArray fv_aux;
00516     std::vector<bool> fv_introduced;
00518     Gecode::FloatNum step;
00519 #endif
00520 
00521     bool needAuxVars;
00523     FlatZincSpace(Rnd& random = defrnd);
00524 
00526     ~FlatZincSpace(void);
00527 
00529     void init(int intVars, int boolVars, int setVars, int floatVars);
00530 
00532     void newIntVar(IntVarSpec* vs);
00534     void aliasBool2Int(int iv, int bv);
00536     int aliasBool2Int(int iv);
00538     void newBoolVar(BoolVarSpec* vs);
00540     void newSetVar(SetVarSpec* vs);
00542     void newFloatVar(FloatVarSpec* vs);
00543 
00545     void postConstraints(std::vector<ConExpr*>& ces);
00546 
00548     void solve(AST::Array* annotation);
00550     void minimize(int var, bool isInt, AST::Array* annotation);
00552     void maximize(int var, bool isInt, AST::Array* annotation);
00553 
00555     void run(std::ostream& out, const Printer& p,
00556              const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00557 
00559     void print(std::ostream& out, const Printer& p) const;
00560 #ifdef GECODE_HAS_CPPROFILER
00561 
00562     std::string getDomains(const Printer& p) const;
00563 #endif
00564 
00565 
00566     void compare(const Space& s, std::ostream& out) const;
00569     void compare(const FlatZincSpace& s, std::ostream& out,
00570                  const Printer& p) const;
00571 
00580     void shrinkArrays(Printer& p);
00581 
00583     Meth method(void) const;
00584 
00586     int optVar(void) const;
00588     bool optVarIsInt(void) const;
00589 
00599     void createBranchers(Printer& p, AST::Node* ann,
00600                          FlatZincOptions& opt, bool ignoreUnknown,
00601                          std::ostream& err = std::cerr);
00602 
00604     AST::Array* solveAnnotations(void) const;
00605 
00607     BranchInformation branchInfo;
00608 
00610     virtual void constrain(const Space& s);
00612     virtual Gecode::Space* copy(void);
00614     virtual bool slave(const MetaInfo& mi);
00615 
00617 
00618 
00619     IntArgs arg2intargs(AST::Node* arg, int offset = 0);
00621     IntSharedArray arg2intsharedarray(AST::Node* arg, int offset = 0);
00623     IntArgs arg2boolargs(AST::Node* arg, int offset = 0);
00625     IntSharedArray arg2boolsharedarray(AST::Node* arg, int offset = 0);
00627     IntSet arg2intset(AST::Node* n);
00629     IntSetArgs arg2intsetargs(AST::Node* arg, int offset = 0);
00631     IntVarArgs arg2intvarargs(AST::Node* arg, int offset = 0);
00633     BoolVarArgs arg2boolvarargs(AST::Node* arg, int offset = 0, int siv=-1);
00635     BoolVar arg2BoolVar(AST::Node* n);
00637     IntVar arg2IntVar(AST::Node* n);
00639     TupleSet arg2tupleset(const IntArgs& a, int noOfVars);
00641     bool isBoolArray(AST::Node* b, int& singleInt);
00642 #ifdef GECODE_HAS_SET_VARS
00643 
00644     SetVar arg2SetVar(AST::Node* n);
00646     SetVarArgs arg2setvarargs(AST::Node* arg, int offset = 0, int doffset = 0,
00647                               const IntSet& od=IntSet::empty);
00648 #endif
00649 #ifdef GECODE_HAS_FLOAT_VARS
00650 
00651     FloatValArgs arg2floatargs(AST::Node* arg, int offset = 0);
00653     FloatVar arg2FloatVar(AST::Node* n);
00655     FloatVarArgs arg2floatvarargs(AST::Node* arg, int offset = 0);
00656 #endif
00657 
00658     IntPropLevel ann2ipl(AST::Node* ann);
00660     DFA getSharedDFA(DFA& a);
00662   };
00663 
00665   class GECODE_VTABLE_EXPORT Error {
00666   private:
00667     const std::string msg;
00668   public:
00669     Error(const std::string& where, const std::string& what)
00670     : msg(where+": "+what) {}
00671     const std::string& toString(void) const { return msg; }
00672   };
00673 
00679   GECODE_FLATZINC_EXPORT
00680   FlatZincSpace* parse(const std::string& fileName,
00681                        Printer& p, std::ostream& err = std::cerr,
00682                        FlatZincSpace* fzs=NULL, Rnd& rnd=defrnd);
00683 
00689   GECODE_FLATZINC_EXPORT
00690   FlatZincSpace* parse(std::istream& is,
00691                        Printer& p, std::ostream& err = std::cerr,
00692                        FlatZincSpace* fzs=NULL, Rnd& rnd=defrnd);
00693 
00694 }}
00695 
00696 #endif
00697 
00698 // STATISTICS: flatzinc-any