Generated on Wed Nov 5 2014 05:18:16 for Gecode by doxygen 1.7.6.1
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  *  Last modified:
00014  *     $Date: 2013-07-08 14:37:54 +0200 (Mon, 08 Jul 2013) $ by $Author: schulte $
00015  *     $Revision: 13821 $
00016  *
00017  *  This file is part of Gecode, the generic constraint
00018  *  development environment:
00019  *     http://www.gecode.org
00020  *
00021  *  Permission is hereby granted, free of charge, to any person obtaining
00022  *  a copy of this software and associated documentation files (the
00023  *  "Software"), to deal in the Software without restriction, including
00024  *  without limitation the rights to use, copy, modify, merge, publish,
00025  *  distribute, sublicense, and/or sell copies of the Software, and to
00026  *  permit persons to whom the Software is furnished to do so, subject to
00027  *  the following conditions:
00028  *
00029  *  The above copyright notice and this permission notice shall be
00030  *  included in all copies or substantial portions of the Software.
00031  *
00032  *  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
00033  *  EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
00034  *  MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
00035  *  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
00036  *  LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
00037  *  OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
00038  *  WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
00039  *
00040  */
00041 
00042 #ifndef __GECODE_FLATZINC_HH__
00043 #define __GECODE_FLATZINC_HH__
00044 
00045 #include <iostream>
00046 
00047 #include <gecode/kernel.hh>
00048 #include <gecode/int.hh>
00049 #ifdef GECODE_HAS_SET_VARS
00050 #include <gecode/set.hh>
00051 #endif
00052 #ifdef GECODE_HAS_FLOAT_VARS
00053 #include <gecode/float.hh>
00054 #endif
00055 #include <map>
00056 
00057 /*
00058  * Support for DLLs under Windows
00059  *
00060  */
00061 
00062 #if !defined(GECODE_STATIC_LIBS) && \
00063     (defined(__CYGWIN__) || defined(__MINGW32__) || defined(_MSC_VER))
00064 
00065 #ifdef GECODE_BUILD_FLATZINC
00066 #define GECODE_FLATZINC_EXPORT __declspec( dllexport )
00067 #else
00068 #define GECODE_FLATZINC_EXPORT __declspec( dllimport )
00069 #endif
00070 
00071 #else
00072 
00073 #ifdef GECODE_GCC_HAS_CLASS_VISIBILITY
00074 
00075 #define GECODE_FLATZINC_EXPORT __attribute__ ((visibility("default")))
00076 
00077 #else
00078 
00079 #define GECODE_FLATZINC_EXPORT
00080 
00081 #endif
00082 #endif
00083 
00084 // Configure auto-linking
00085 #ifndef GECODE_BUILD_FLATZINC
00086 #define GECODE_LIBRARY_NAME "FlatZinc"
00087 #include <gecode/support/auto-link.hpp>
00088 #endif
00089 
00090 #include <gecode/driver.hh>
00091 
00092 #include <gecode/flatzinc/conexpr.hh>
00093 #include <gecode/flatzinc/ast.hh>
00094 #include <gecode/flatzinc/varspec.hh>
00095 
00105 namespace Gecode { namespace FlatZinc {
00106 
00111   class GECODE_FLATZINC_EXPORT Printer {
00112   private:
00113     AST::Array* _output;
00114     void printElem(std::ostream& out,
00115                    AST::Node* ai,
00116                    const Gecode::IntVarArray& iv,
00117                    const Gecode::BoolVarArray& bv
00118 #ifdef GECODE_HAS_SET_VARS
00119                    ,
00120                    const Gecode::SetVarArray& sv
00121 #endif
00122 #ifdef GECODE_HAS_FLOAT_VARS
00123                   ,
00124                   const Gecode::FloatVarArray& fv
00125 #endif
00126                    ) const;
00127     void printElemDiff(std::ostream& out,
00128                        AST::Node* ai,
00129                        const Gecode::IntVarArray& iv1,
00130                        const Gecode::IntVarArray& iv2,
00131                        const Gecode::BoolVarArray& bv1,
00132                        const Gecode::BoolVarArray& bv2
00133 #ifdef GECODE_HAS_SET_VARS
00134                        ,
00135                        const Gecode::SetVarArray& sv1,
00136                        const Gecode::SetVarArray& sv2
00137 #endif
00138 #ifdef GECODE_HAS_FLOAT_VARS
00139                        ,
00140                        const Gecode::FloatVarArray& fv1,
00141                        const Gecode::FloatVarArray& fv2
00142 #endif
00143                        ) const;
00144   public:
00145     Printer(void) : _output(NULL) {}
00146     void init(AST::Array* output);
00147 
00148     void print(std::ostream& out,
00149                const Gecode::IntVarArray& iv,
00150                const Gecode::BoolVarArray& bv
00151 #ifdef GECODE_HAS_SET_VARS
00152                ,
00153                const Gecode::SetVarArray& sv
00154 #endif
00155 #ifdef GECODE_HAS_FLOAT_VARS
00156                ,
00157                const Gecode::FloatVarArray& fv
00158 #endif
00159                ) const;
00160 
00161     void printDiff(std::ostream& out,
00162                const Gecode::IntVarArray& iv1, const Gecode::IntVarArray& iv2,
00163                const Gecode::BoolVarArray& bv1, const Gecode::BoolVarArray& bv2
00164 #ifdef GECODE_HAS_SET_VARS
00165                ,
00166                const Gecode::SetVarArray& sv1, const Gecode::SetVarArray& sv2
00167 #endif
00168 #ifdef GECODE_HAS_FLOAT_VARS
00169                ,
00170                const Gecode::FloatVarArray& fv1,
00171                const Gecode::FloatVarArray& fv2
00172 #endif
00173                ) const;
00174 
00175   
00176     ~Printer(void);
00177     
00178     void shrinkElement(AST::Node* node,
00179                        std::map<int,int>& iv, std::map<int,int>& bv, 
00180                        std::map<int,int>& sv, std::map<int,int>& fv);
00181 
00182     void shrinkArrays(Space& home,
00183                       int& optVar, bool optVarIsInt,
00184                       Gecode::IntVarArray& iv,
00185                       Gecode::BoolVarArray& bv
00186 #ifdef GECODE_HAS_SET_VARS
00187                       ,
00188                       Gecode::SetVarArray& sv
00189 #endif
00190 #ifdef GECODE_HAS_FLOAT_VARS
00191                       ,
00192                       Gecode::FloatVarArray& fv
00193 #endif
00194                      );
00195     
00196   private:
00197     Printer(const Printer&);
00198     Printer& operator=(const Printer&);
00199   };
00200 
00205   class FlatZincOptions : public Gecode::BaseOptions {
00206   protected:
00208 
00209       Gecode::Driver::UnsignedIntOption _solutions; 
00210       Gecode::Driver::BoolOption        _allSolutions; 
00211       Gecode::Driver::DoubleOption      _threads;   
00212       Gecode::Driver::BoolOption        _free; 
00213       Gecode::Driver::DoubleOption      _decay;       
00214       Gecode::Driver::UnsignedIntOption _c_d;       
00215       Gecode::Driver::UnsignedIntOption _a_d;       
00216       Gecode::Driver::UnsignedIntOption _node;      
00217       Gecode::Driver::UnsignedIntOption _fail;      
00218       Gecode::Driver::UnsignedIntOption _time;      
00219       Gecode::Driver::IntOption         _seed;      
00220       Gecode::Driver::StringOption      _restart;   
00221       Gecode::Driver::DoubleOption      _r_base;    
00222       Gecode::Driver::UnsignedIntOption _r_scale;   
00223       Gecode::Driver::BoolOption        _nogoods;   
00224       Gecode::Driver::UnsignedIntOption _nogoods_limit; 
00225       Gecode::Driver::BoolOption        _interrupt; 
00226 
00227     
00229 
00230       Gecode::Driver::StringOption      _mode;       
00231       Gecode::Driver::BoolOption        _stat;       
00232       Gecode::Driver::StringValueOption _output;     
00233 
00234   public:
00236     FlatZincOptions(const char* s)
00237     : Gecode::BaseOptions(s),
00238       _solutions("-n","number of solutions (0 = all)",1),
00239       _allSolutions("-a", "return all solutions (equal to -solutions 0)"),
00240       _threads("-p","number of threads (0 = #processing units)",
00241                Gecode::Search::Config::threads),
00242       _free("--free", "no need to follow search-specification"),
00243       _decay("-decay","decay factor",0.99),
00244       _c_d("-c-d","recomputation commit distance",Gecode::Search::Config::c_d),
00245       _a_d("-a-d","recomputation adaption distance",Gecode::Search::Config::a_d),
00246       _node("-node","node cutoff (0 = none, solution mode)"),
00247       _fail("-fail","failure cutoff (0 = none, solution mode)"),
00248       _time("-time","time (in ms) cutoff (0 = none, solution mode)"),
00249       _seed("-r","random seed",0),
00250       _restart("-restart","restart sequence type",RM_NONE),
00251       _r_base("-restart-base","base for geometric restart sequence",1.5),
00252       _r_scale("-restart-scale","scale factor for restart sequence",250),
00253       _nogoods("-nogoods","whether to use no-goods from restarts",false),
00254       _nogoods_limit("-nogoods-limit","depth limit for no-good extraction",
00255                      Search::Config::nogoods_limit),
00256       _interrupt("-interrupt","whether to catch Ctrl-C (true) or not (false)",
00257                  true),
00258       _mode("-mode","how to execute script",Gecode::SM_SOLUTION),
00259       _stat("-s","emit statistics"),
00260       _output("-o","file to send output to") {
00261 
00262       _mode.add(Gecode::SM_SOLUTION, "solution");
00263       _mode.add(Gecode::SM_STAT, "stat");
00264       _mode.add(Gecode::SM_GIST, "gist");
00265       _restart.add(RM_NONE,"none");
00266       _restart.add(RM_CONSTANT,"constant");
00267       _restart.add(RM_LINEAR,"linear");
00268       _restart.add(RM_LUBY,"luby");
00269       _restart.add(RM_GEOMETRIC,"geometric");
00270 
00271       add(_solutions); add(_threads); add(_c_d); add(_a_d);
00272       add(_allSolutions);
00273       add(_free);
00274       add(_decay);
00275       add(_node); add(_fail); add(_time); add(_interrupt);
00276       add(_seed);
00277       add(_restart); add(_r_base); add(_r_scale); 
00278       add(_nogoods); add(_nogoods_limit);
00279       add(_mode); add(_stat);
00280       add(_output);
00281     }
00282 
00283     void parse(int& argc, char* argv[]) {
00284       Gecode::BaseOptions::parse(argc,argv);
00285       if (_allSolutions.value()) {
00286         _solutions.value(0);
00287       }
00288       if (_stat.value())
00289         _mode.value(Gecode::SM_STAT);
00290     }
00291   
00292     virtual void help(void) {
00293       std::cerr << "Gecode FlatZinc interpreter" << std::endl
00294                 << " - Supported FlatZinc version: " << GECODE_FLATZINC_VERSION
00295                 << std::endl << std::endl;
00296       Gecode::BaseOptions::help();
00297     }
00298   
00299     unsigned int solutions(void) const { return _solutions.value(); }
00300     bool allSolutions(void) const { return _allSolutions.value(); }
00301     double threads(void) const { return _threads.value(); }
00302     bool free(void) const { return _free.value(); }
00303     unsigned int c_d(void) const { return _c_d.value(); }
00304     unsigned int a_d(void) const { return _a_d.value(); }
00305     unsigned int node(void) const { return _node.value(); }
00306     unsigned int fail(void) const { return _fail.value(); }
00307     unsigned int time(void) const { return _time.value(); }
00308     int seed(void) const { return _seed.value(); }
00309     const char* output(void) const { return _output.value(); }
00310     Gecode::ScriptMode mode(void) const {
00311       return static_cast<Gecode::ScriptMode>(_mode.value());
00312     }
00313 
00314     double decay(void) const { return _decay.value(); }
00315     RestartMode restart(void) const {
00316       return static_cast<RestartMode>(_restart.value());
00317     }
00318     double restart_base(void) const { return _r_base.value(); }
00319     unsigned int restart_scale(void) const { return _r_scale.value(); }
00320     bool nogoods(void) const { return _nogoods.value(); }
00321     unsigned int nogoods_limit(void) const { return _nogoods_limit.value(); }
00322     bool interrupt(void) const { return _interrupt.value(); }
00323 
00324   };
00325 
00326   class BranchInformation : public SharedHandle {
00327   public:
00329     BranchInformation(void);
00331     BranchInformation(const BranchInformation& bi);
00333     void init(void);
00335     void add(const BrancherHandle& bh,
00336              const std::string& rel0,
00337              const std::string& rel1,
00338              const std::vector<std::string>& n);
00340     void print(const BrancherHandle& bh,
00341                int a, int i, int n, std::ostream& o) const;
00342 #ifdef GECODE_HAS_FLOAT_VARS
00343 
00344     void print(const BrancherHandle& bh,
00345                int a, int i, const FloatNumBranch& nl, std::ostream& o) const;
00346 #endif
00347   };
00348 
00353   class GECODE_FLATZINC_EXPORT FlatZincSpace : public Space {
00354   public:
00355     enum Meth {
00356       SAT, //< Solve as satisfaction problem
00357       MIN, //< Solve as minimization problem
00358       MAX  //< Solve as maximization problem
00359     };
00360   protected:
00362     int intVarCount;
00364     int boolVarCount;
00366     int floatVarCount;
00368     int setVarCount;
00369 
00371     int _optVar;
00373     bool _optVarIsInt;
00374   
00376     Meth _method;
00377     
00379     AST::Array* _solveAnnotations;
00380 
00382     FlatZincSpace(bool share, FlatZincSpace&);
00383   private:
00385     template<template<class> class Engine>
00386     void
00387     runEngine(std::ostream& out, const Printer& p, 
00388               const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00390     template<template<class> class Engine,
00391              template<template<class> class,class> class Meta>
00392     void
00393     runMeta(std::ostream& out, const Printer& p, 
00394             const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00395     void
00396     branchWithPlugin(AST::Node* ann);
00397   public:
00399     Gecode::IntVarArray iv;
00401     Gecode::IntVarArray iv_aux;
00403     std::vector<bool> iv_introduced;
00405     int* iv_boolalias;
00407     Gecode::BoolVarArray bv;
00409     Gecode::BoolVarArray bv_aux;
00411     std::vector<bool> bv_introduced;
00412 #ifdef GECODE_HAS_SET_VARS
00413 
00414     Gecode::SetVarArray sv;
00416     Gecode::SetVarArray sv_aux;
00418     std::vector<bool> sv_introduced;
00419 #endif
00420 #ifdef GECODE_HAS_FLOAT_VARS
00421 
00422     Gecode::FloatVarArray fv;
00424     Gecode::FloatVarArray fv_aux;
00426     std::vector<bool> fv_introduced;
00427 #endif
00428 
00429     bool needAuxVars;
00431     FlatZincSpace(void);
00432   
00434     ~FlatZincSpace(void);
00435   
00437     void init(int intVars, int boolVars, int setVars, int floatVars);
00438 
00440     void newIntVar(IntVarSpec* vs);
00442     void aliasBool2Int(int iv, int bv);
00444     int aliasBool2Int(int iv);
00446     void newBoolVar(BoolVarSpec* vs);
00448     void newSetVar(SetVarSpec* vs);
00450     void newFloatVar(FloatVarSpec* vs);
00451   
00453     void postConstraint(const ConExpr& ce, AST::Node* annotation);
00454   
00456     void solve(AST::Array* annotation);
00458     void minimize(int var, bool isInt, AST::Array* annotation);
00460     void maximize(int var, bool isInt, AST::Array* annotation);
00461 
00463     void run(std::ostream& out, const Printer& p, 
00464              const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
00465   
00467     void print(std::ostream& out, const Printer& p) const;
00468 
00471     void compare(const Space& s, std::ostream& out) const;
00474     void compare(const FlatZincSpace& s, std::ostream& out,
00475                  const Printer& p) const;
00476 
00485     void shrinkArrays(Printer& p);
00486 
00488     Meth method(void) const;
00489 
00491     int optVar(void) const;
00493     bool optVarIsInt(void) const;
00494 
00504     void createBranchers(AST::Node* ann,
00505                          int seed, double decay,
00506                          bool ignoreUnknown,
00507                          std::ostream& err = std::cerr);
00508 
00510     AST::Array* solveAnnotations(void) const;
00511 
00513     BranchInformation branchInfo;
00514 
00516     virtual void constrain(const Space& s);
00518     virtual Gecode::Space* copy(bool share);
00519     
00521 
00522 
00523     IntArgs arg2intargs(AST::Node* arg, int offset = 0);
00525     IntArgs arg2boolargs(AST::Node* arg, int offset = 0);
00527     IntSet arg2intset(AST::Node* n);
00529     IntSetArgs arg2intsetargs(AST::Node* arg, int offset = 0);
00531     IntVarArgs arg2intvarargs(AST::Node* arg, int offset = 0);
00533     BoolVarArgs arg2boolvarargs(AST::Node* arg, int offset = 0, int siv=-1);
00535     BoolVar arg2BoolVar(AST::Node* n);
00537     IntVar arg2IntVar(AST::Node* n);
00539     bool isBoolArray(AST::Node* b, int& singleInt);
00540 #ifdef GECODE_HAS_SET_VARS
00541 
00542     SetVar arg2SetVar(AST::Node* n);
00544     SetVarArgs arg2setvarargs(AST::Node* arg, int offset = 0, int doffset = 0,
00545                               const IntSet& od=IntSet::empty);
00546 #endif
00547 #ifdef GECODE_HAS_FLOAT_VARS
00548 
00549     FloatValArgs arg2floatargs(AST::Node* arg, int offset = 0);
00551     FloatVar arg2FloatVar(AST::Node* n);
00553     FloatVarArgs arg2floatvarargs(AST::Node* arg, int offset = 0);
00554 #endif
00555 
00556     IntConLevel ann2icl(AST::Node* ann);
00558   };
00559 
00561   class Error {
00562   private:
00563     const std::string msg;
00564   public:
00565     Error(const std::string& where, const std::string& what)
00566     : msg(where+": "+what) {}
00567     const std::string& toString(void) const { return msg; }
00568   };
00569 
00575   GECODE_FLATZINC_EXPORT
00576   FlatZincSpace* parse(const std::string& fileName,
00577                        Printer& p, std::ostream& err = std::cerr,
00578                        FlatZincSpace* fzs=NULL);
00579 
00585   GECODE_FLATZINC_EXPORT
00586   FlatZincSpace* parse(std::istream& is,
00587                        Printer& p, std::ostream& err = std::cerr,
00588                        FlatZincSpace* fzs=NULL);
00589 
00590 }}
00591 
00592 #endif
00593 
00594 // STATISTICS: flatzinc-any