Generated on Sat May 25 2013 18:00:32 for Gecode by doxygen 1.8.3.1
flatzinc.hh
Go to the documentation of this file.
1 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2 /*
3  * Main authors:
4  * Guido Tack <tack@gecode.org>
5  *
6  * Contributing authors:
7  * Gabriel Hjort Blindell <gabriel.hjort.blindell@gmail.com>
8  *
9  * Copyright:
10  * Guido Tack, 2007-2012
11  * Gabriel Hjort Blindell, 2012
12  *
13  * Last modified:
14  * $Date: 2013-03-07 20:21:13 +0100 (Thu, 07 Mar 2013) $ by $Author: schulte $
15  * $Revision: 13460 $
16  *
17  * This file is part of Gecode, the generic constraint
18  * development environment:
19  * http://www.gecode.org
20  *
21  * Permission is hereby granted, free of charge, to any person obtaining
22  * a copy of this software and associated documentation files (the
23  * "Software"), to deal in the Software without restriction, including
24  * without limitation the rights to use, copy, modify, merge, publish,
25  * distribute, sublicense, and/or sell copies of the Software, and to
26  * permit persons to whom the Software is furnished to do so, subject to
27  * the following conditions:
28  *
29  * The above copyright notice and this permission notice shall be
30  * included in all copies or substantial portions of the Software.
31  *
32  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
33  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
34  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
35  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
36  * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
37  * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
38  * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
39  *
40  */
41 
42 #ifndef __GECODE_FLATZINC_HH__
43 #define __GECODE_FLATZINC_HH__
44 
45 #include <iostream>
46 
47 #include <gecode/kernel.hh>
48 #include <gecode/int.hh>
49 #ifdef GECODE_HAS_SET_VARS
50 #include <gecode/set.hh>
51 #endif
52 #ifdef GECODE_HAS_FLOAT_VARS
53 #include <gecode/float.hh>
54 #endif
55 #include <map>
56 
57 /*
58  * Support for DLLs under Windows
59  *
60  */
61 
62 #if !defined(GECODE_STATIC_LIBS) && \
63  (defined(__CYGWIN__) || defined(__MINGW32__) || defined(_MSC_VER))
64 
65 #ifdef GECODE_BUILD_FLATZINC
66 #define GECODE_FLATZINC_EXPORT __declspec( dllexport )
67 #else
68 #define GECODE_FLATZINC_EXPORT __declspec( dllimport )
69 #endif
70 
71 #else
72 
73 #ifdef GECODE_GCC_HAS_CLASS_VISIBILITY
74 
75 #define GECODE_FLATZINC_EXPORT __attribute__ ((visibility("default")))
76 
77 #else
78 
79 #define GECODE_FLATZINC_EXPORT
80 
81 #endif
82 #endif
83 
84 // Configure auto-linking
85 #ifndef GECODE_BUILD_FLATZINC
86 #define GECODE_LIBRARY_NAME "FlatZinc"
88 #endif
89 
90 #include <gecode/driver.hh>
91 
93 #include <gecode/flatzinc/ast.hh>
95 
105 namespace Gecode { namespace FlatZinc {
106 
112  private:
113  AST::Array* _output;
114  void printElem(std::ostream& out,
115  AST::Node* ai,
116  const Gecode::IntVarArray& iv,
117  const Gecode::BoolVarArray& bv
118 #ifdef GECODE_HAS_SET_VARS
119  ,
120  const Gecode::SetVarArray& sv
121 #endif
123  ,
124  const Gecode::FloatVarArray& fv
125 #endif
126  ) const;
127  void printElemDiff(std::ostream& out,
128  AST::Node* ai,
129  const Gecode::IntVarArray& iv1,
130  const Gecode::IntVarArray& iv2,
131  const Gecode::BoolVarArray& bv1,
132  const Gecode::BoolVarArray& bv2
133 #ifdef GECODE_HAS_SET_VARS
134  ,
135  const Gecode::SetVarArray& sv1,
136  const Gecode::SetVarArray& sv2
137 #endif
138 #ifdef GECODE_HAS_FLOAT_VARS
139  ,
140  const Gecode::FloatVarArray& fv1,
141  const Gecode::FloatVarArray& fv2
142 #endif
143  ) const;
144  public:
145  Printer(void) : _output(NULL) {}
146  void init(AST::Array* output);
147 
148  void print(std::ostream& out,
149  const Gecode::IntVarArray& iv,
150  const Gecode::BoolVarArray& bv
151 #ifdef GECODE_HAS_SET_VARS
152  ,
153  const Gecode::SetVarArray& sv
154 #endif
155 #ifdef GECODE_HAS_FLOAT_VARS
156  ,
157  const Gecode::FloatVarArray& fv
158 #endif
159  ) const;
160 
161  void printDiff(std::ostream& out,
162  const Gecode::IntVarArray& iv1, const Gecode::IntVarArray& iv2,
163  const Gecode::BoolVarArray& bv1, const Gecode::BoolVarArray& bv2
164 #ifdef GECODE_HAS_SET_VARS
165  ,
166  const Gecode::SetVarArray& sv1, const Gecode::SetVarArray& sv2
167 #endif
168 #ifdef GECODE_HAS_FLOAT_VARS
169  ,
170  const Gecode::FloatVarArray& fv1,
171  const Gecode::FloatVarArray& fv2
172 #endif
173  ) const;
174 
175 
176  ~Printer(void);
177 
178  void shrinkElement(AST::Node* node,
179  std::map<int,int>& iv, std::map<int,int>& bv,
180  std::map<int,int>& sv, std::map<int,int>& fv);
181 
182  void shrinkArrays(Space& home,
183  int& optVar,
186 #ifdef GECODE_HAS_SET_VARS
187  ,
189 #endif
190 #ifdef GECODE_HAS_FLOAT_VARS
191  ,
193 #endif
194  );
195 
196  private:
197  Printer(const Printer&);
198  Printer& operator=(const Printer&);
199  };
200 
206  protected:
208 
224 
225 
227 
231 
232  public:
234  FlatZincOptions(const char* s)
235  : Gecode::BaseOptions(s),
236  _solutions("-n","number of solutions (0 = all)",1),
237  _allSolutions("-a", "return all solutions (equal to -solutions 0)"),
238  _threads("-p","number of threads (0 = #processing units)",
239  Gecode::Search::Config::threads),
240  _free("--free", "no need to follow search-specification"),
241  _decay("-decay","decay factor",1.0),
242  _c_d("-c-d","recomputation commit distance",Gecode::Search::Config::c_d),
243  _a_d("-a-d","recomputation adaption distance",Gecode::Search::Config::a_d),
244  _node("-node","node cutoff (0 = none, solution mode)"),
245  _fail("-fail","failure cutoff (0 = none, solution mode)"),
246  _time("-time","time (in ms) cutoff (0 = none, solution mode)"),
247  _seed("-r","random seed",0),
248  _restart("-restart","restart sequence type",RM_NONE),
249  _r_base("-restart-base","base for geometric restart sequence",1.5),
250  _r_scale("-restart-scale","scale factor for restart sequence",250),
251  _interrupt("-interrupt","whether to catch Ctrl-C (true) or not (false)",
252  true),
253  _mode("-mode","how to execute script",Gecode::SM_SOLUTION),
254  _stat("-s","emit statistics"),
255  _output("-o","file to send output to") {
256 
257  _mode.add(Gecode::SM_SOLUTION, "solution");
258  _mode.add(Gecode::SM_STAT, "stat");
259  _mode.add(Gecode::SM_GIST, "gist");
260  _restart.add(RM_NONE,"none");
261  _restart.add(RM_CONSTANT,"constant");
262  _restart.add(RM_LINEAR,"linear");
263  _restart.add(RM_LUBY,"luby");
264  _restart.add(RM_GEOMETRIC,"geometric");
265 
268  add(_free);
269  add(_decay);
271  add(_seed);
273  add(_mode); add(_stat);
274  add(_output);
275  }
276 
277  void parse(int& argc, char* argv[]) {
278  Gecode::BaseOptions::parse(argc,argv);
279  if (_allSolutions.value()) {
280  _solutions.value(0);
281  }
282  if (_stat.value())
284  }
285 
286  virtual void help(void) {
287  std::cerr << "Gecode FlatZinc interpreter" << std::endl
288  << " - Supported FlatZinc version: " << GECODE_FLATZINC_VERSION
289  << std::endl << std::endl;
291  }
292 
293  unsigned int solutions(void) const { return _solutions.value(); }
294  bool allSolutions(void) const { return _allSolutions.value(); }
295  double threads(void) const { return _threads.value(); }
296  bool free(void) const { return _free.value(); }
297  unsigned int c_d(void) const { return _c_d.value(); }
298  unsigned int a_d(void) const { return _a_d.value(); }
299  unsigned int node(void) const { return _node.value(); }
300  unsigned int fail(void) const { return _fail.value(); }
301  unsigned int time(void) const { return _time.value(); }
302  int seed(void) const { return _seed.value(); }
303  const char* output(void) const { return _output.value(); }
304  Gecode::ScriptMode mode(void) const {
305  return static_cast<Gecode::ScriptMode>(_mode.value());
306  }
307 
308  double decay(void) const { return _decay.value(); }
309  RestartMode restart(void) const {
310  return static_cast<RestartMode>(_restart.value());
311  }
312  double restart_base(void) const { return _r_base.value(); }
313  unsigned int restart_scale(void) const { return _r_scale.value(); }
314  bool interrupt(void) const { return _interrupt.value(); }
315 
316  };
317 
323  public:
324  enum Meth {
325  SAT, //< Solve as satisfaction problem
326  MIN, //< Solve as minimization problem
327  MAX //< Solve as maximization problem
328  };
329  protected:
338 
340  int _optVar;
341 
344 
347 
349  FlatZincSpace(bool share, FlatZincSpace&);
350  private:
352  template<template<class> class Engine>
353  void
354  runEngine(std::ostream& out, const Printer& p,
355  const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
357  template<template<class> class Engine,
358  template<template<class> class,class> class Meta>
359  void
360  runMeta(std::ostream& out, const Printer& p,
361  const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
362  void
363  branchWithPlugin(AST::Node* ann);
364  public:
370  std::vector<bool> iv_introduced;
372  int* iv_boolalias;
378  std::vector<bool> bv_introduced;
379 #ifdef GECODE_HAS_SET_VARS
380 
385  std::vector<bool> sv_introduced;
386 #endif
387 #ifdef GECODE_HAS_FLOAT_VARS
388 
393  std::vector<bool> fv_introduced;
394 #endif
395 
396  bool needAuxVars;
398  FlatZincSpace(void);
399 
401  ~FlatZincSpace(void);
402 
404  void init(int intVars, int boolVars, int setVars, int floatVars);
405 
407  void newIntVar(IntVarSpec* vs);
409  void aliasBool2Int(int iv, int bv);
411  int aliasBool2Int(int iv);
413  void newBoolVar(BoolVarSpec* vs);
415  void newSetVar(SetVarSpec* vs);
417  void newFloatVar(FloatVarSpec* vs);
418 
420  void postConstraint(const ConExpr& ce, AST::Node* annotation);
421 
423  void solve(AST::Array* annotation);
425  void minimize(int var, AST::Array* annotation);
427  void maximize(int var, AST::Array* annotation);
428 
430  void run(std::ostream& out, const Printer& p,
431  const FlatZincOptions& opt, Gecode::Support::Timer& t_total);
432 
434  void print(std::ostream& out, const Printer& p) const;
435 
438  void compare(const Space& s, std::ostream& out) const;
441  void compare(const FlatZincSpace& s, std::ostream& out,
442  const Printer& p) const;
443 
452  void shrinkArrays(Printer& p);
453 
455  Meth method(void) const;
456 
458  int optVar(void) const;
459 
469  void createBranchers(AST::Node* ann,
470  int seed, double decay,
471  bool ignoreUnknown,
472  std::ostream& err = std::cerr);
473 
475  AST::Array* solveAnnotations(void) const;
476 
478  virtual void constrain(const Space& s);
480  virtual Gecode::Space* copy(bool share);
481 
482 
484 
485 
486  IntArgs arg2intargs(AST::Node* arg, int offset = 0);
488  IntArgs arg2boolargs(AST::Node* arg, int offset = 0);
490  IntSet arg2intset(AST::Node* n);
492  IntSetArgs arg2intsetargs(AST::Node* arg, int offset = 0);
494  IntVarArgs arg2intvarargs(AST::Node* arg, int offset = 0);
496  BoolVarArgs arg2boolvarargs(AST::Node* arg, int offset = 0, int siv=-1);
498  BoolVar arg2BoolVar(AST::Node* n);
500  IntVar arg2IntVar(AST::Node* n);
502  bool isBoolArray(AST::Node* b, int& singleInt);
503 #ifdef GECODE_HAS_SET_VARS
504 
505  SetVar arg2SetVar(AST::Node* n);
507  SetVarArgs arg2setvarargs(AST::Node* arg, int offset = 0, int doffset = 0,
508  const IntSet& od=IntSet::empty);
509 #endif
510 #ifdef GECODE_HAS_FLOAT_VARS
511 
512  FloatValArgs arg2floatargs(AST::Node* arg, int offset = 0);
514  FloatVar arg2FloatVar(AST::Node* n);
516  FloatVarArgs arg2floatvarargs(AST::Node* arg, int offset = 0);
517 #endif
518 
519  IntConLevel ann2icl(AST::Node* ann);
521  };
522 
524  class Error {
525  private:
526  const std::string msg;
527  public:
528  Error(const std::string& where, const std::string& what)
529  : msg(where+": "+what) {}
530  const std::string& toString(void) const { return msg; }
531  };
532 
539  FlatZincSpace* parse(const std::string& fileName,
540  Printer& p, std::ostream& err = std::cerr,
541  FlatZincSpace* fzs=NULL);
542 
549  FlatZincSpace* parse(std::istream& is,
550  Printer& p, std::ostream& err = std::cerr,
551  FlatZincSpace* fzs=NULL);
552 
553 }}
554 
555 #endif
556 
557 // STATISTICS: flatzinc-any