Generated on Sat Feb 7 2015 02:01:13 for Gecode by doxygen 1.8.9.1
flatzinc.cpp
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: 2015-01-05 07:33:06 +0100 (Mon, 05 Jan 2015) $ by $Author: tack $
15  * $Revision: 14337 $
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 #include <gecode/flatzinc.hh>
45 
46 #include <gecode/search.hh>
47 
48 #include <vector>
49 #include <string>
50 #include <sstream>
51 #include <limits>
52 using namespace std;
53 
54 namespace Gecode { namespace FlatZinc {
55 
68  class AuxVarBrancher : public Brancher {
69  protected:
71  bool done;
74  IntValBranch int_valsel0,
75  TieBreak<IntVarBranch> bool_varsel0,
76  IntValBranch bool_valsel0
78  ,
79  SetVarBranch set_varsel0,
80  SetValBranch set_valsel0
81 #endif
83  ,
84  TieBreak<FloatVarBranch> float_varsel0,
85  FloatValBranch float_valsel0
86 #endif
87  )
88  : Brancher(home), done(false),
89  int_varsel(int_varsel0), int_valsel(int_valsel0),
90  bool_varsel(bool_varsel0), bool_valsel(bool_valsel0)
91 #ifdef GECODE_HAS_SET_VARS
92  , set_varsel(set_varsel0), set_valsel(set_valsel0)
93 #endif
94 #ifdef GECODE_HAS_FLOAT_VARS
95  , float_varsel(float_varsel0), float_valsel(float_valsel0)
96 #endif
97  {}
99  AuxVarBrancher(Space& home, bool share, AuxVarBrancher& b)
100  : Brancher(home, share, b), done(b.done) {}
101 
103  class Choice : public Gecode::Choice {
104  public:
106  bool fail;
108  Choice(const Brancher& b, bool fail0)
109  : Gecode::Choice(b,1), fail(fail0) {}
111  virtual size_t size(void) const {
112  return sizeof(Choice);
113  }
115  virtual void archive(Archive& e) const {
117  e.put(fail);
118  }
119  };
120 
125 #ifdef GECODE_HAS_SET_VARS
128 #endif
129 #ifdef GECODE_HAS_FLOAT_VARS
132 #endif
133 
134  public:
136  virtual bool status(const Space& _home) const {
137  if (done) return false;
138  const FlatZincSpace& home = static_cast<const FlatZincSpace&>(_home);
139  for (int i=0; i<home.iv_aux.size(); i++)
140  if (!home.iv_aux[i].assigned()) return true;
141  for (int i=0; i<home.bv_aux.size(); i++)
142  if (!home.bv_aux[i].assigned()) return true;
143 #ifdef GECODE_HAS_SET_VARS
144  for (int i=0; i<home.sv_aux.size(); i++)
145  if (!home.sv_aux[i].assigned()) return true;
146 #endif
147 #ifdef GECODE_HAS_FLOAT_VARS
148  for (int i=0; i<home.fv_aux.size(); i++)
149  if (!home.fv_aux[i].assigned()) return true;
150 #endif
151  // No non-assigned variables left
152  return false;
153  }
155  virtual Choice* choice(Space& home) {
156  done = true;
157  FlatZincSpace& fzs = static_cast<FlatZincSpace&>(*home.clone());
158  fzs.needAuxVars = false;
159  branch(fzs,fzs.iv_aux,int_varsel,int_valsel);
160  branch(fzs,fzs.bv_aux,bool_varsel,bool_valsel);
161 #ifdef GECODE_HAS_SET_VARS
162  branch(fzs,fzs.sv_aux,set_varsel,set_valsel);
163 #endif
164 #ifdef GECODE_HAS_FLOAT_VARS
165  branch(fzs,fzs.fv_aux,float_varsel,float_valsel);
166 #endif
167  Search::Options opt; opt.clone = false;
168  FlatZincSpace* sol = dfs(&fzs, opt);
169  if (sol) {
170  delete sol;
171  return new Choice(*this,false);
172  } else {
173  return new Choice(*this,true);
174  }
175  }
177  virtual Choice* choice(const Space&, Archive& e) {
178  bool fail; e >> fail;
179  return new Choice(*this, fail);
180  }
182  virtual ExecStatus commit(Space&, const Gecode::Choice& c, unsigned int) {
183  return static_cast<const Choice&>(c).fail ? ES_FAILED : ES_OK;
184  }
186  virtual void print(const Space&, const Gecode::Choice& c,
187  unsigned int,
188  std::ostream& o) const {
189  o << "FlatZinc("
190  << (static_cast<const Choice&>(c).fail ? "fail" : "ok")
191  << ")";
192  }
194  virtual Actor* copy(Space& home, bool share) {
195  return new (home) AuxVarBrancher(home, share, *this);
196  }
198  static void post(Home home,
199  TieBreak<IntVarBranch> int_varsel,
200  IntValBranch int_valsel,
201  TieBreak<IntVarBranch> bool_varsel,
202  IntValBranch bool_valsel
203 #ifdef GECODE_HAS_SET_VARS
204  ,
205  SetVarBranch set_varsel,
206  SetValBranch set_valsel
207 #endif
209  ,
210  TieBreak<FloatVarBranch> float_varsel,
211  FloatValBranch float_valsel
212 #endif
213  ) {
214  (void) new (home) AuxVarBrancher(home, int_varsel, int_valsel,
215  bool_varsel, bool_valsel
216 #ifdef GECODE_HAS_SET_VARS
217  , set_varsel, set_valsel
218 #endif
219 #ifdef GECODE_HAS_FLOAT_VARS
220  , float_varsel, float_valsel
221 #endif
222  );
223  }
225  virtual size_t dispose(Space&) {
226  return sizeof(*this);
227  }
228  };
229 
231  private:
232  struct BI {
233  string r0;
234  string r1;
235  vector<string> n;
236  BI(void) : r0(""), r1(""), n(0) {}
237  BI(const string& r00, const string& r10, const vector<string>& n0)
238  : r0(r00), r1(r10), n(n0) {}
239  };
240  vector<BI> v;
241  BranchInformationO(vector<BI> v0) : v(v0) {}
242  public:
244  virtual ~BranchInformationO(void) {}
245  virtual SharedHandle::Object* copy(void) const {
246  return new BranchInformationO(v);
247  }
249  void add(const BrancherHandle& bh,
250  const string& rel0,
251  const string& rel1,
252  const vector<string>& n) {
253  v.resize(std::max(static_cast<unsigned int>(v.size()),bh.id()+1));
254  v[bh.id()] = BI(rel0,rel1,n);
255  }
257  void print(const BrancherHandle& bh,
258  int a, int i, int n, ostream& o) const {
259  const BI& bi = v[bh.id()];
260  o << bi.n[i] << " " << (a==0 ? bi.r0 : bi.r1) << " " << n;
261  }
262 #ifdef GECODE_HAS_FLOAT_VARS
263  void print(const BrancherHandle& bh,
264  int a, int i, const FloatNumBranch& nl, ostream& o) const {
265  const BI& bi = v[bh.id()];
266  o << bi.n[i] << " "
267  << (((a == 0) == nl.l) ? "<=" : ">=") << nl.n;
268  }
269 #endif
270  };
271 
272  BranchInformation::BranchInformation(void)
273  : SharedHandle(NULL) {}
274 
276  : SharedHandle(bi) {}
277 
278  void
280  assert(object() == NULL);
281  object(new BranchInformationO());
282  }
283 
284  void
286  const std::string& rel0,
287  const std::string& rel1,
288  const std::vector<std::string>& n) {
289  static_cast<BranchInformationO*>(object())->add(bh,rel0,rel1,n);
290  }
291  void
293  int n, std::ostream& o) const {
294  static_cast<const BranchInformationO*>(object())->print(bh,a,i,n,o);
295  }
296 #ifdef GECODE_HAS_FLOAT_VARS
297  void
299  const FloatNumBranch& nl, std::ostream& o) const {
300  static_cast<const BranchInformationO*>(object())->print(bh,a,i,nl,o);
301  }
302 #endif
303  template<class Var>
304  void varValPrint(const Space &home, const BrancherHandle& bh,
305  unsigned int a,
306  Var, int i, const int& n,
307  std::ostream& o) {
308  static_cast<const FlatZincSpace&>(home).branchInfo.print(bh,a,i,n,o);
309  }
310 
311 #ifdef GECODE_HAS_FLOAT_VARS
312  void varValPrintF(const Space &home, const BrancherHandle& bh,
313  unsigned int a,
314  FloatVar, int i, const FloatNumBranch& nl,
315  std::ostream& o) {
316  static_cast<const FlatZincSpace&>(home).branchInfo.print(bh,a,i,nl,o);
317  }
318 #endif
319 
320  FznRnd::FznRnd(unsigned int s) : random(s) {}
321 
322  unsigned int
323  FznRnd::operator ()(unsigned int n) {
324  Support::Lock lock(mutex);
325  return random(n);
326  }
327 
329  if (vs->assigned) {
330  return IntSet(vs->i,vs->i);
331  }
332  if (vs->domain()) {
333  AST::SetLit* sl = vs->domain.some();
334  if (sl->interval) {
335  return IntSet(sl->min, sl->max);
336  } else {
337  int* newdom = heap.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
338  for (int i=sl->s.size(); i--;)
339  newdom[i] = sl->s[i];
340  IntSet ret(newdom, sl->s.size());
341  heap.free(newdom, static_cast<unsigned long int>(sl->s.size()));
342  return ret;
343  }
344  }
346  }
347 
348  int vs2bsl(BoolVarSpec* bs) {
349  if (bs->assigned) {
350  return bs->i;
351  }
352  if (bs->domain()) {
353  AST::SetLit* sl = bs->domain.some();
354  assert(sl->interval);
355  return std::min(1, std::max(0, sl->min));
356  }
357  return 0;
358  }
359 
360  int vs2bsh(BoolVarSpec* bs) {
361  if (bs->assigned) {
362  return bs->i;
363  }
364  if (bs->domain()) {
365  AST::SetLit* sl = bs->domain.some();
366  assert(sl->interval);
367  return std::max(0, std::min(1, sl->max));
368  }
369  return 1;
370  }
371 
372  TieBreak<IntVarBranch> ann2ivarsel(AST::Node* ann, Rnd rnd, double decay) {
373  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
374  if (s->id == "input_order")
376  if (s->id == "first_fail")
378  if (s->id == "anti_first_fail")
380  if (s->id == "smallest")
382  if (s->id == "largest")
384  if (s->id == "occurrence")
386  if (s->id == "max_regret")
388  if (s->id == "most_constrained")
391  if (s->id == "random") {
392  return TieBreak<IntVarBranch>(INT_VAR_RND(rnd));
393  }
394  if (s->id == "dom_w_deg") {
396  }
397  if (s->id == "afc_min")
399  if (s->id == "afc_max")
401  if (s->id == "afc_size_min")
403  if (s->id == "afc_size_max") {
405  }
406  if (s->id == "activity_min")
408  if (s->id == "activity_max")
410  if (s->id == "activity_size_min")
412  if (s->id == "activity_size_max")
414  }
415  std::cerr << "Warning, ignored search annotation: ";
416  ann->print(std::cerr);
417  std::cerr << std::endl;
419  }
420 
421  IntValBranch ann2ivalsel(AST::Node* ann, std::string& r0, std::string& r1,
422  Rnd rnd) {
423  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
424  if (s->id == "indomain_min") {
425  r0 = "="; r1 = "!=";
426  return INT_VAL_MIN();
427  }
428  if (s->id == "indomain_max") {
429  r0 = "="; r1 = "!=";
430  return INT_VAL_MAX();
431  }
432  if (s->id == "indomain_median") {
433  r0 = "="; r1 = "!=";
434  return INT_VAL_MED();
435  }
436  if (s->id == "indomain_split") {
437  r0 = "<="; r1 = ">";
438  return INT_VAL_SPLIT_MIN();
439  }
440  if (s->id == "indomain_reverse_split") {
441  r0 = ">"; r1 = "<=";
442  return INT_VAL_SPLIT_MAX();
443  }
444  if (s->id == "indomain_random") {
445  r0 = "="; r1 = "!=";
446  return INT_VAL_RND(rnd);
447  }
448  if (s->id == "indomain") {
449  r0 = "="; r1 = "=";
450  return INT_VALUES_MIN();
451  }
452  if (s->id == "indomain_middle") {
453  std::cerr << "Warning, replacing unsupported annotation "
454  << "indomain_middle with indomain_median" << std::endl;
455  r0 = "="; r1 = "!=";
456  return INT_VAL_MED();
457  }
458  if (s->id == "indomain_interval") {
459  std::cerr << "Warning, replacing unsupported annotation "
460  << "indomain_interval with indomain_split" << std::endl;
461  r0 = "<="; r1 = ">";
462  return INT_VAL_SPLIT_MIN();
463  }
464  }
465  std::cerr << "Warning, ignored search annotation: ";
466  ann->print(std::cerr);
467  std::cerr << std::endl;
468  r0 = "="; r1 = "!=";
469  return INT_VAL_MIN();
470  }
471 
473  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
474  if (s->id == "indomain_min")
475  return INT_ASSIGN_MIN();
476  if (s->id == "indomain_max")
477  return INT_ASSIGN_MAX();
478  if (s->id == "indomain_median")
479  return INT_ASSIGN_MED();
480  if (s->id == "indomain_random") {
481  return INT_ASSIGN_RND(rnd);
482  }
483  }
484  std::cerr << "Warning, ignored search annotation: ";
485  ann->print(std::cerr);
486  std::cerr << std::endl;
487  return INT_ASSIGN_MIN();
488  }
489 
490 #ifdef GECODE_HAS_SET_VARS
491  SetVarBranch ann2svarsel(AST::Node* ann, Rnd rnd, double decay) {
492  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
493  if (s->id == "input_order")
494  return SET_VAR_NONE();
495  if (s->id == "first_fail")
496  return SET_VAR_SIZE_MIN();
497  if (s->id == "anti_first_fail")
498  return SET_VAR_SIZE_MAX();
499  if (s->id == "smallest")
500  return SET_VAR_MIN_MIN();
501  if (s->id == "largest")
502  return SET_VAR_MAX_MAX();
503  if (s->id == "afc_min")
504  return SET_VAR_AFC_MIN(decay);
505  if (s->id == "afc_max")
506  return SET_VAR_AFC_MAX(decay);
507  if (s->id == "afc_size_min")
508  return SET_VAR_AFC_SIZE_MIN(decay);
509  if (s->id == "afc_size_max")
510  return SET_VAR_AFC_SIZE_MAX(decay);
511  if (s->id == "activity_min")
512  return SET_VAR_ACTIVITY_MIN(decay);
513  if (s->id == "activity_max")
514  return SET_VAR_ACTIVITY_MAX(decay);
515  if (s->id == "activity_size_min")
516  return SET_VAR_ACTIVITY_SIZE_MIN(decay);
517  if (s->id == "activity_size_max")
518  return SET_VAR_ACTIVITY_SIZE_MAX(decay);
519  if (s->id == "random") {
520  return SET_VAR_RND(rnd);
521  }
522  }
523  std::cerr << "Warning, ignored search annotation: ";
524  ann->print(std::cerr);
525  std::cerr << std::endl;
526  return SET_VAR_NONE();
527  }
528 
529  SetValBranch ann2svalsel(AST::Node* ann, std::string r0, std::string r1,
530  Rnd rnd) {
531  (void) rnd;
532  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
533  if (s->id == "indomain_min") {
534  r0 = "in"; r1 = "not in";
535  return SET_VAL_MIN_INC();
536  }
537  if (s->id == "indomain_max") {
538  r0 = "in"; r1 = "not in";
539  return SET_VAL_MAX_INC();
540  }
541  if (s->id == "outdomain_min") {
542  r1 = "in"; r0 = "not in";
543  return SET_VAL_MIN_EXC();
544  }
545  if (s->id == "outdomain_max") {
546  r1 = "in"; r0 = "not in";
547  return SET_VAL_MAX_EXC();
548  }
549  }
550  std::cerr << "Warning, ignored search annotation: ";
551  ann->print(std::cerr);
552  std::cerr << std::endl;
553  r0 = "in"; r1 = "not in";
554  return SET_VAL_MIN_INC();
555  }
556 #endif
557 
558 #ifdef GECODE_HAS_FLOAT_VARS
560  double decay) {
561  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
562  if (s->id == "input_order")
564  if (s->id == "first_fail")
566  if (s->id == "anti_first_fail")
568  if (s->id == "smallest")
570  if (s->id == "largest")
572  if (s->id == "occurrence")
574  if (s->id == "most_constrained")
577  if (s->id == "random") {
579  }
580  if (s->id == "afc_min")
582  if (s->id == "afc_max")
584  if (s->id == "afc_size_min")
586  if (s->id == "afc_size_max")
588  if (s->id == "activity_min")
590  if (s->id == "activity_max")
592  if (s->id == "activity_size_min")
594  if (s->id == "activity_size_max")
596  }
597  std::cerr << "Warning, ignored search annotation: ";
598  ann->print(std::cerr);
599  std::cerr << std::endl;
601  }
602 
603  FloatValBranch ann2fvalsel(AST::Node* ann, std::string r0, std::string r1) {
604  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
605  if (s->id == "indomain_split") {
606  r0 = "<="; r1 = ">";
607  return FLOAT_VAL_SPLIT_MIN();
608  }
609  if (s->id == "indomain_reverse_split") {
610  r1 = "<="; r0 = ">";
611  return FLOAT_VAL_SPLIT_MAX();
612  }
613  }
614  std::cerr << "Warning, ignored search annotation: ";
615  ann->print(std::cerr);
616  std::cerr << std::endl;
617  r0 = "<="; r1 = ">";
618  return FLOAT_VAL_SPLIT_MIN();
619  }
620 
621 #endif
622 
624  : Space(share, f), _random(f._random),
625  _solveAnnotations(NULL), iv_boolalias(NULL),
626  needAuxVars(f.needAuxVars) {
627  _optVar = f._optVar;
629  _method = f._method;
630  _lns = f._lns;
631  branchInfo.update(*this, share, f.branchInfo);
632  iv.update(*this, share, f.iv);
633  iv_lns.update(*this, share, f.iv_lns);
635 
636  if (needAuxVars) {
637  IntVarArgs iva;
638  for (int i=0; i<f.iv_aux.size(); i++) {
639  if (!f.iv_aux[i].assigned()) {
640  iva << IntVar();
641  iva[iva.size()-1].update(*this, share, f.iv_aux[i]);
642  }
643  }
644  iv_aux = IntVarArray(*this, iva);
645  }
646 
647  bv.update(*this, share, f.bv);
649  if (needAuxVars) {
650  BoolVarArgs bva;
651  for (int i=0; i<f.bv_aux.size(); i++) {
652  if (!f.bv_aux[i].assigned()) {
653  bva << BoolVar();
654  bva[bva.size()-1].update(*this, share, f.bv_aux[i]);
655  }
656  }
657  bv_aux = BoolVarArray(*this, bva);
658  }
659 
660 #ifdef GECODE_HAS_SET_VARS
661  sv.update(*this, share, f.sv);
663  if (needAuxVars) {
664  SetVarArgs sva;
665  for (int i=0; i<f.sv_aux.size(); i++) {
666  if (!f.sv_aux[i].assigned()) {
667  sva << SetVar();
668  sva[sva.size()-1].update(*this, share, f.sv_aux[i]);
669  }
670  }
671  sv_aux = SetVarArray(*this, sva);
672  }
673 #endif
674 #ifdef GECODE_HAS_FLOAT_VARS
675  fv.update(*this, share, f.fv);
677  if (needAuxVars) {
678  FloatVarArgs fva;
679  for (int i=0; i<f.fv_aux.size(); i++) {
680  if (!f.fv_aux[i].assigned()) {
681  fva << FloatVar();
682  fva[fva.size()-1].update(*this, share, f.fv_aux[i]);
683  }
684  }
685  fv_aux = FloatVarArray(*this, fva);
686  }
687 #endif
688  }
689 
691  : intVarCount(-1), boolVarCount(-1), floatVarCount(-1), setVarCount(-1),
692  _optVar(-1), _optVarIsInt(true), _lns(0), _random(random),
693  _solveAnnotations(NULL), needAuxVars(true) {
694  branchInfo.init();
695  }
696 
697  void
698  FlatZincSpace::init(int intVars, int boolVars,
699  int setVars, int floatVars) {
700  (void) setVars;
701  (void) floatVars;
702 
703  intVarCount = 0;
704  iv = IntVarArray(*this, intVars);
705  iv_introduced = std::vector<bool>(2*intVars);
706  iv_boolalias = alloc<int>(intVars+(intVars==0?1:0));
707  boolVarCount = 0;
708  bv = BoolVarArray(*this, boolVars);
709  bv_introduced = std::vector<bool>(2*boolVars);
710 #ifdef GECODE_HAS_SET_VARS
711  setVarCount = 0;
712  sv = SetVarArray(*this, setVars);
713  sv_introduced = std::vector<bool>(2*setVars);
714 #endif
715 #ifdef GECODE_HAS_FLOAT_VARS
716  floatVarCount = 0;
717  fv = FloatVarArray(*this, floatVars);
718  fv_introduced = std::vector<bool>(2*floatVars);
719 #endif
720  }
721 
722  void
724  if (vs->alias) {
725  iv[intVarCount++] = iv[vs->i];
726  } else {
727  IntSet dom(vs2is(vs));
728  if (dom.size()==0) {
729  fail();
730  return;
731  } else {
732  iv[intVarCount++] = IntVar(*this, dom);
733  }
734  }
735  iv_introduced[2*(intVarCount-1)] = vs->introduced;
736  iv_introduced[2*(intVarCount-1)+1] = vs->funcDep;
737  iv_boolalias[intVarCount-1] = -1;
738  }
739 
740  void
742  iv_boolalias[iv] = bv;
743  }
744  int
746  return iv_boolalias[iv];
747  }
748 
749  void
751  if (vs->alias) {
752  bv[boolVarCount++] = bv[vs->i];
753  } else {
754  bv[boolVarCount++] = BoolVar(*this, vs2bsl(vs), vs2bsh(vs));
755  }
757  bv_introduced[2*(boolVarCount-1)+1] = vs->funcDep;
758  }
759 
760 #ifdef GECODE_HAS_SET_VARS
761  void
763  if (vs->alias) {
764  sv[setVarCount++] = sv[vs->i];
765  } else if (vs->assigned) {
766  assert(vs->upperBound());
767  AST::SetLit* vsv = vs->upperBound.some();
768  if (vsv->interval) {
769  IntSet d(vsv->min, vsv->max);
770  sv[setVarCount++] = SetVar(*this, d, d);
771  } else {
772  int* is = heap.alloc<int>(static_cast<unsigned long int>(vsv->s.size()));
773  for (int i=vsv->s.size(); i--; )
774  is[i] = vsv->s[i];
775  IntSet d(is, vsv->s.size());
776  heap.free(is,static_cast<unsigned long int>(vsv->s.size()));
777  sv[setVarCount++] = SetVar(*this, d, d);
778  }
779  } else if (vs->upperBound()) {
780  AST::SetLit* vsv = vs->upperBound.some();
781  if (vsv->interval) {
782  IntSet d(vsv->min, vsv->max);
783  sv[setVarCount++] = SetVar(*this, IntSet::empty, d);
784  } else {
785  int* is = heap.alloc<int>(static_cast<unsigned long int>(vsv->s.size()));
786  for (int i=vsv->s.size(); i--; )
787  is[i] = vsv->s[i];
788  IntSet d(is, vsv->s.size());
789  heap.free(is,static_cast<unsigned long int>(vsv->s.size()));
790  sv[setVarCount++] = SetVar(*this, IntSet::empty, d);
791  }
792  } else {
793  sv[setVarCount++] = SetVar(*this, IntSet::empty,
796  }
797  sv_introduced[2*(setVarCount-1)] = vs->introduced;
798  sv_introduced[2*(setVarCount-1)+1] = vs->funcDep;
799  }
800 #else
801  void
803  throw FlatZinc::Error("Gecode", "set variables not supported");
804  }
805 #endif
806 
807 #ifdef GECODE_HAS_FLOAT_VARS
808  void
810  if (vs->alias) {
811  fv[floatVarCount++] = fv[vs->i];
812  } else {
813  double dmin, dmax;
814  if (vs->domain()) {
815  dmin = vs->domain.some().first;
816  dmax = vs->domain.some().second;
817  if (dmin > dmax) {
818  fail();
819  return;
820  }
821  } else {
822  dmin = Float::Limits::min;
823  dmax = Float::Limits::max;
824  }
825  fv[floatVarCount++] = FloatVar(*this, dmin, dmax);
826  }
828  fv_introduced[2*(floatVarCount-1)+1] = vs->funcDep;
829  }
830 #else
831  void
833  throw FlatZinc::Error("Gecode", "float variables not supported");
834  }
835 #endif
836 
837  namespace {
838  struct ConExprOrder {
839  bool operator() (ConExpr* ce0, ConExpr* ce1) {
840  return ce0->args->a.size() < ce1->args->a.size();
841  }
842  };
843  }
844 
845  void
846  FlatZincSpace::postConstraints(std::vector<ConExpr*>& ces) {
847  ConExprOrder ceo;
848  std::sort(ces.begin(), ces.end(), ceo);
849 
850  for (unsigned int i=0; i<ces.size(); i++) {
851  const ConExpr& ce = *ces[i];
852  try {
853  registry().post(*this, ce);
854  } catch (Gecode::Exception& e) {
855  throw FlatZinc::Error("Gecode", e.what());
856  } catch (AST::TypeError& e) {
857  throw FlatZinc::Error("Type error", e.what());
858  }
859  delete ces[i];
860  ces[i] = NULL;
861  }
862  }
863 
864  void flattenAnnotations(AST::Array* ann, std::vector<AST::Node*>& out) {
865  for (unsigned int i=0; i<ann->a.size(); i++) {
866  if (ann->a[i]->isCall("seq_search")) {
867  AST::Call* c = ann->a[i]->getCall();
868  if (c->args->isArray())
869  flattenAnnotations(c->args->getArray(), out);
870  else
871  out.push_back(c->args);
872  } else {
873  out.push_back(ann->a[i]);
874  }
875  }
876  }
877 
878  void
879  FlatZincSpace::createBranchers(AST::Node* ann, int seed, double decay,
880  bool ignoreUnknown,
881  std::ostream& err) {
882  Rnd rnd(static_cast<unsigned int>(seed));
883  TieBreak<IntVarBranch> def_int_varsel = INT_VAR_AFC_SIZE_MAX(0.99);
884  IntValBranch def_int_valsel = INT_VAL_MIN();
885  TieBreak<IntVarBranch> def_bool_varsel = INT_VAR_AFC_MAX(0.99);
886  IntValBranch def_bool_valsel = INT_VAL_MIN();
887 #ifdef GECODE_HAS_SET_VARS
888  SetVarBranch def_set_varsel = SET_VAR_AFC_SIZE_MAX(0.99);
889  SetValBranch def_set_valsel = SET_VAL_MIN_INC();
890 #endif
891 #ifdef GECODE_HAS_FLOAT_VARS
892  TieBreak<FloatVarBranch> def_float_varsel = FLOAT_VAR_SIZE_MIN();
893  FloatValBranch def_float_valsel = FLOAT_VAL_SPLIT_MIN();
894 #endif
895 
896  std::vector<bool> iv_searched(iv.size());
897  for (unsigned int i=iv.size(); i--;)
898  iv_searched[i] = false;
899  std::vector<bool> bv_searched(bv.size());
900  for (unsigned int i=bv.size(); i--;)
901  bv_searched[i] = false;
902 #ifdef GECODE_HAS_SET_VARS
903  std::vector<bool> sv_searched(sv.size());
904  for (unsigned int i=sv.size(); i--;)
905  sv_searched[i] = false;
906 #endif
907 #ifdef GECODE_HAS_FLOAT_VARS
908  std::vector<bool> fv_searched(fv.size());
909  for (unsigned int i=fv.size(); i--;)
910  fv_searched[i] = false;
911 #endif
912 
913  _lns = 0;
914  if (ann) {
915  std::vector<AST::Node*> flatAnn;
916  if (ann->isArray()) {
917  flattenAnnotations(ann->getArray() , flatAnn);
918  } else {
919  flatAnn.push_back(ann);
920  }
921 
922  for (unsigned int i=0; i<flatAnn.size(); i++) {
923  if (flatAnn[i]->isCall("relax_and_reconstruct")) {
924  if (_lns != 0)
925  throw FlatZinc::Error("FlatZinc",
926  "Only one relax_and_reconstruct annotation allowed");
927  AST::Call *call = flatAnn[i]->getCall("relax_and_reconstruct");
928  AST::Array *args = call->getArgs(2);
929  _lns = args->a[1]->getInt();
930  AST::Array *vars = args->a[0]->getArray();
931  int k=vars->a.size();
932  for (int i=vars->a.size(); i--;)
933  if (vars->a[i]->isInt())
934  k--;
935  iv_lns = IntVarArray(*this, k);
936  k = 0;
937  for (unsigned int i=0; i<vars->a.size(); i++) {
938  if (vars->a[i]->isInt())
939  continue;
940  iv_lns[k++] = iv[vars->a[i]->getIntVar()];
941  }
942  } else if (flatAnn[i]->isCall("gecode_search")) {
943  AST::Call* c = flatAnn[i]->getCall();
944  branchWithPlugin(c->args);
945  } else if (flatAnn[i]->isCall("int_search")) {
946  AST::Call *call = flatAnn[i]->getCall("int_search");
947  AST::Array *args = call->getArgs(4);
948  AST::Array *vars = args->a[0]->getArray();
949  int k=vars->a.size();
950  for (int i=vars->a.size(); i--;)
951  if (vars->a[i]->isInt())
952  k--;
953  IntVarArgs va(k);
954  vector<string> names;
955  k=0;
956  for (unsigned int i=0; i<vars->a.size(); i++) {
957  if (vars->a[i]->isInt())
958  continue;
959  va[k++] = iv[vars->a[i]->getIntVar()];
960  iv_searched[vars->a[i]->getIntVar()] = true;
961  names.push_back(vars->a[i]->getVarName());
962  }
963  std::string r0, r1;
964  BrancherHandle bh = branch(*this, va,
965  ann2ivarsel(args->a[1],rnd,decay),
966  ann2ivalsel(args->a[2],r0,r1,rnd),
967  NULL,
968  &varValPrint<IntVar>);
969  branchInfo.add(bh,r0,r1,names);
970  } else if (flatAnn[i]->isCall("int_assign")) {
971  AST::Call *call = flatAnn[i]->getCall("int_assign");
972  AST::Array *args = call->getArgs(2);
973  AST::Array *vars = args->a[0]->getArray();
974  int k=vars->a.size();
975  for (int i=vars->a.size(); i--;)
976  if (vars->a[i]->isInt())
977  k--;
978  IntVarArgs va(k);
979  k=0;
980  for (unsigned int i=0; i<vars->a.size(); i++) {
981  if (vars->a[i]->isInt())
982  continue;
983  va[k++] = iv[vars->a[i]->getIntVar()];
984  iv_searched[vars->a[i]->getIntVar()] = true;
985  }
986  assign(*this, va, ann2asnivalsel(args->a[1],rnd), NULL,
987  &varValPrint<IntVar>);
988  } else if (flatAnn[i]->isCall("bool_search")) {
989  AST::Call *call = flatAnn[i]->getCall("bool_search");
990  AST::Array *args = call->getArgs(4);
991  AST::Array *vars = args->a[0]->getArray();
992  int k=vars->a.size();
993  for (int i=vars->a.size(); i--;)
994  if (vars->a[i]->isBool())
995  k--;
996  BoolVarArgs va(k);
997  k=0;
998  vector<string> names;
999  for (unsigned int i=0; i<vars->a.size(); i++) {
1000  if (vars->a[i]->isBool())
1001  continue;
1002  va[k++] = bv[vars->a[i]->getBoolVar()];
1003  bv_searched[vars->a[i]->getBoolVar()] = true;
1004  names.push_back(vars->a[i]->getVarName());
1005  }
1006 
1007  std::string r0, r1;
1008  BrancherHandle bh = branch(*this, va,
1009  ann2ivarsel(args->a[1],rnd,decay),
1010  ann2ivalsel(args->a[2],r0,r1,rnd), NULL,
1011  &varValPrint<BoolVar>);
1012  branchInfo.add(bh,r0,r1,names);
1013  } else if (flatAnn[i]->isCall("int_default_search")) {
1014  AST::Call *call = flatAnn[i]->getCall("int_default_search");
1015  AST::Array *args = call->getArgs(2);
1016  def_int_varsel = ann2ivarsel(args->a[0],rnd,decay);
1017  std::string r0;
1018  def_int_valsel = ann2ivalsel(args->a[1],r0,r0,rnd);
1019  } else if (flatAnn[i]->isCall("bool_default_search")) {
1020  AST::Call *call = flatAnn[i]->getCall("bool_default_search");
1021  AST::Array *args = call->getArgs(2);
1022  def_bool_varsel = ann2ivarsel(args->a[0],rnd,decay);
1023  std::string r0;
1024  def_bool_valsel = ann2ivalsel(args->a[1],r0,r0,rnd);
1025  } else if (flatAnn[i]->isCall("set_search")) {
1026 #ifdef GECODE_HAS_SET_VARS
1027  AST::Call *call = flatAnn[i]->getCall("set_search");
1028  AST::Array *args = call->getArgs(4);
1029  AST::Array *vars = args->a[0]->getArray();
1030  int k=vars->a.size();
1031  for (int i=vars->a.size(); i--;)
1032  if (vars->a[i]->isSet())
1033  k--;
1034  SetVarArgs va(k);
1035  k=0;
1036  vector<string> names;
1037  for (unsigned int i=0; i<vars->a.size(); i++) {
1038  if (vars->a[i]->isSet())
1039  continue;
1040  va[k++] = sv[vars->a[i]->getSetVar()];
1041  sv_searched[vars->a[i]->getSetVar()] = true;
1042  names.push_back(vars->a[i]->getVarName());
1043  }
1044  std::string r0, r1;
1045  BrancherHandle bh = branch(*this, va,
1046  ann2svarsel(args->a[1],rnd,decay),
1047  ann2svalsel(args->a[2],r0,r1,rnd),
1048  NULL,
1049  &varValPrint<SetVar>);
1050  branchInfo.add(bh,r0,r1,names);
1051 #else
1052  if (!ignoreUnknown) {
1053  err << "Warning, ignored search annotation: ";
1054  flatAnn[i]->print(err);
1055  err << std::endl;
1056  }
1057 #endif
1058  } else if (flatAnn[i]->isCall("set_default_search")) {
1059 #ifdef GECODE_HAS_SET_VARS
1060  AST::Call *call = flatAnn[i]->getCall("set_default_search");
1061  AST::Array *args = call->getArgs(2);
1062  def_set_varsel = ann2svarsel(args->a[0],rnd,decay);
1063  std::string r0;
1064  def_set_valsel = ann2svalsel(args->a[1],r0,r0,rnd);
1065 #else
1066  if (!ignoreUnknown) {
1067  err << "Warning, ignored search annotation: ";
1068  flatAnn[i]->print(err);
1069  err << std::endl;
1070  }
1071 #endif
1072  } else if (flatAnn[i]->isCall("float_default_search")) {
1073 #ifdef GECODE_HAS_FLOAT_VARS
1074  AST::Call *call = flatAnn[i]->getCall("float_default_search");
1075  AST::Array *args = call->getArgs(2);
1076  def_float_varsel = ann2fvarsel(args->a[0],rnd,decay);
1077  std::string r0;
1078  def_float_valsel = ann2fvalsel(args->a[1],r0,r0);
1079 #else
1080  if (!ignoreUnknown) {
1081  err << "Warning, ignored search annotation: ";
1082  flatAnn[i]->print(err);
1083  err << std::endl;
1084  }
1085 #endif
1086  } else if (flatAnn[i]->isCall("float_search")) {
1087 #ifdef GECODE_HAS_FLOAT_VARS
1088  AST::Call *call = flatAnn[i]->getCall("float_search");
1089  AST::Array *args = call->getArgs(5);
1090  AST::Array *vars = args->a[0]->getArray();
1091  int k=vars->a.size();
1092  for (int i=vars->a.size(); i--;)
1093  if (vars->a[i]->isFloat())
1094  k--;
1095  FloatVarArgs va(k);
1096  k=0;
1097  vector<string> names;
1098  for (unsigned int i=0; i<vars->a.size(); i++) {
1099  if (vars->a[i]->isFloat())
1100  continue;
1101  va[k++] = fv[vars->a[i]->getFloatVar()];
1102  fv_searched[vars->a[i]->getFloatVar()] = true;
1103  names.push_back(vars->a[i]->getVarName());
1104  }
1105  std::string r0, r1;
1106  BrancherHandle bh = branch(*this, va,
1107  ann2fvarsel(args->a[2],rnd,decay),
1108  ann2fvalsel(args->a[3],r0,r1),
1109  NULL,
1110  &varValPrintF);
1111  branchInfo.add(bh,r0,r1,names);
1112 #else
1113  if (!ignoreUnknown) {
1114  err << "Warning, ignored search annotation: ";
1115  flatAnn[i]->print(err);
1116  err << std::endl;
1117  }
1118 #endif
1119  } else {
1120  if (!ignoreUnknown) {
1121  err << "Warning, ignored search annotation: ";
1122  flatAnn[i]->print(err);
1123  err << std::endl;
1124  }
1125  }
1126  }
1127  }
1128  int introduced = 0;
1129  int funcdep = 0;
1130  int searched = 0;
1131  for (int i=iv.size(); i--;) {
1132  if (iv_searched[i] || (_method != SAT && _optVarIsInt && _optVar==i)) {
1133  searched++;
1134  } else if (iv_introduced[2*i]) {
1135  if (iv_introduced[2*i+1]) {
1136  funcdep++;
1137  } else {
1138  introduced++;
1139  }
1140  }
1141  }
1142  IntVarArgs iv_sol(iv.size()-(introduced+funcdep+searched));
1143  IntVarArgs iv_tmp(introduced);
1144  for (int i=iv.size(), j=0, k=0; i--;) {
1145  if (iv_searched[i] || (_method != SAT && _optVarIsInt && _optVar==i))
1146  continue;
1147  if (iv_introduced[2*i]) {
1148  if (!iv_introduced[2*i+1]) {
1149  iv_tmp[j++] = iv[i];
1150  }
1151  } else {
1152  iv_sol[k++] = iv[i];
1153  }
1154  }
1155 
1156  introduced = 0;
1157  funcdep = 0;
1158  searched = 0;
1159  for (int i=bv.size(); i--;) {
1160  if (bv_searched[i]) {
1161  searched++;
1162  } else if (bv_introduced[2*i]) {
1163  if (bv_introduced[2*i+1]) {
1164  funcdep++;
1165  } else {
1166  introduced++;
1167  }
1168  }
1169  }
1170  BoolVarArgs bv_sol(bv.size()-(introduced+funcdep+searched));
1171  BoolVarArgs bv_tmp(introduced);
1172  for (int i=bv.size(), j=0, k=0; i--;) {
1173  if (bv_searched[i])
1174  continue;
1175  if (bv_introduced[2*i]) {
1176  if (!bv_introduced[2*i+1]) {
1177  bv_tmp[j++] = bv[i];
1178  }
1179  } else {
1180  bv_sol[k++] = bv[i];
1181  }
1182  }
1183 
1184  if (iv_sol.size() > 0) {
1185  branch(*this, iv_sol, def_int_varsel, def_int_valsel);
1186  }
1187  if (bv_sol.size() > 0)
1188  branch(*this, bv_sol, def_bool_varsel, def_bool_valsel);
1189 #ifdef GECODE_HAS_FLOAT_VARS
1190  introduced = 0;
1191  funcdep = 0;
1192  searched = 0;
1193  for (int i=fv.size(); i--;) {
1194  if (fv_searched[i] || (_method != SAT && !_optVarIsInt && _optVar==i)) {
1195  searched++;
1196  } else if (fv_introduced[2*i]) {
1197  if (fv_introduced[2*i+1]) {
1198  funcdep++;
1199  } else {
1200  introduced++;
1201  }
1202  }
1203  }
1204  FloatVarArgs fv_sol(fv.size()-(introduced+funcdep+searched));
1205  FloatVarArgs fv_tmp(introduced);
1206  for (int i=fv.size(), j=0, k=0; i--;) {
1207  if (fv_searched[i] || (_method != SAT && !_optVarIsInt && _optVar==i))
1208  continue;
1209  if (fv_introduced[2*i]) {
1210  if (!fv_introduced[2*i+1]) {
1211  fv_tmp[j++] = fv[i];
1212  }
1213  } else {
1214  fv_sol[k++] = fv[i];
1215  }
1216  }
1217 
1218  if (fv_sol.size() > 0)
1219  branch(*this, fv_sol, def_float_varsel, def_float_valsel);
1220 #endif
1221 #ifdef GECODE_HAS_SET_VARS
1222  introduced = 0;
1223  funcdep = 0;
1224  searched = 0;
1225  for (int i=sv.size(); i--;) {
1226  if (sv_searched[i]) {
1227  searched++;
1228  } else if (sv_introduced[2*i]) {
1229  if (sv_introduced[2*i+1]) {
1230  funcdep++;
1231  } else {
1232  introduced++;
1233  }
1234  }
1235  }
1236  SetVarArgs sv_sol(sv.size()-(introduced+funcdep+searched));
1237  SetVarArgs sv_tmp(introduced);
1238  for (int i=sv.size(), j=0, k=0; i--;) {
1239  if (sv_searched[i])
1240  continue;
1241  if (sv_introduced[2*i]) {
1242  if (!sv_introduced[2*i+1]) {
1243  sv_tmp[j++] = sv[i];
1244  }
1245  } else {
1246  sv_sol[k++] = sv[i];
1247  }
1248  }
1249 
1250  if (sv_sol.size() > 0)
1251  branch(*this, sv_sol, def_set_varsel, def_set_valsel);
1252 #endif
1253  iv_aux = IntVarArray(*this, iv_tmp);
1254  bv_aux = BoolVarArray(*this, bv_tmp);
1255  int n_aux = iv_aux.size() + bv_aux.size();
1256 #ifdef GECODE_HAS_SET_VARS
1257  sv_aux = SetVarArray(*this, sv_tmp);
1258  n_aux += sv_aux.size();
1259 #endif
1260 #ifdef GECODE_HAS_FLOAT_VARS
1261  fv_aux = FloatVarArray(*this, fv_tmp);
1262  n_aux += fv_aux.size();
1263 #endif
1264 
1265  if (_method == MIN) {
1266  if (_optVarIsInt) {
1267  branch(*this, iv[_optVar], INT_VAL_MIN());
1268  } else {
1269 #ifdef GECODE_HAS_FLOAT_VARS
1270  branch(*this, fv[_optVar], FLOAT_VAL_SPLIT_MIN());
1271 #endif
1272  }
1273  } else if (_method == MAX) {
1274  if (_optVarIsInt) {
1275  branch(*this, iv[_optVar], INT_VAL_MAX());
1276  } else {
1277 #ifdef GECODE_HAS_FLOAT_VARS
1278  branch(*this, fv[_optVar], FLOAT_VAL_SPLIT_MAX());
1279 #endif
1280  }
1281  }
1282 
1283  if (n_aux > 0) {
1284  if (_method == SAT) {
1285  AuxVarBrancher::post(*this, def_int_varsel, def_int_valsel,
1286  def_bool_varsel, def_bool_valsel
1287 #ifdef GECODE_HAS_SET_VARS
1288  , def_set_varsel, def_set_valsel
1289 #endif
1290 #ifdef GECODE_HAS_FLOAT_VARS
1291  , def_float_varsel, def_float_valsel
1292 #endif
1293  );
1294  } else {
1295  branch(*this,iv_aux,def_int_varsel,def_int_valsel);
1296  branch(*this,bv_aux,def_bool_varsel,def_bool_valsel);
1297  #ifdef GECODE_HAS_SET_VARS
1298  branch(*this,sv_aux,def_set_varsel,def_set_valsel);
1299  #endif
1300  #ifdef GECODE_HAS_FLOAT_VARS
1301  branch(*this,fv_aux,def_float_varsel,def_float_valsel);
1302  #endif
1303 
1304  }
1305  }
1306  }
1307 
1308  AST::Array*
1310  return _solveAnnotations;
1311  }
1312 
1313  void
1315  _method = SAT;
1316  _solveAnnotations = ann;
1317  }
1318 
1319  void
1320  FlatZincSpace::minimize(int var, bool isInt, AST::Array* ann) {
1321  _method = MIN;
1322  _optVar = var;
1323  _optVarIsInt = isInt;
1324  _solveAnnotations = ann;
1325  }
1326 
1327  void
1328  FlatZincSpace::maximize(int var, bool isInt, AST::Array* ann) {
1329  _method = MAX;
1330  _optVar = var;
1331  _optVarIsInt = isInt;
1332  _solveAnnotations = ann;
1333  }
1334 
1336  delete _solveAnnotations;
1337  }
1338 
1339 #ifdef GECODE_HAS_GIST
1340 
1344  template<class Engine>
1345  class GistEngine {
1346  };
1347 
1349  template<typename S>
1350  class GistEngine<DFS<S> > {
1351  public:
1352  static void explore(S* root, const FlatZincOptions& opt,
1355  o.c_d = opt.c_d(); o.a_d = opt.a_d();
1356  o.inspect.click(i);
1357  o.inspect.compare(c);
1358  (void) Gecode::Gist::dfs(root, o);
1359  }
1360  };
1361 
1363  template<typename S>
1364  class GistEngine<BAB<S> > {
1365  public:
1366  static void explore(S* root, const FlatZincOptions& opt,
1367  Gist::Inspector* i, Gist::Comparator* c) {
1369  o.c_d = opt.c_d(); o.a_d = opt.a_d();
1370  o.inspect.click(i);
1371  o.inspect.compare(c);
1372  (void) Gecode::Gist::bab(root, o);
1373  }
1374  };
1375 
1377  template<class S>
1378  class FZPrintingInspector
1380  private:
1381  const Printer& p;
1382  public:
1384  FZPrintingInspector(const Printer& p0);
1386  virtual void inspect(const Space& node);
1388  virtual void finalize(void);
1389  };
1390 
1391  template<class S>
1392  FZPrintingInspector<S>::FZPrintingInspector(const Printer& p0)
1393  : TextOutput("Gecode/FlatZinc"), p(p0) {}
1394 
1395  template<class S>
1396  void
1397  FZPrintingInspector<S>::inspect(const Space& node) {
1398  init();
1399  dynamic_cast<const S&>(node).print(getStream(), p);
1400  getStream() << std::endl;
1401  }
1402 
1403  template<class S>
1404  void
1405  FZPrintingInspector<S>::finalize(void) {
1407  }
1408 
1409  template<class S>
1410  class FZPrintingComparator
1411  : public Gecode::Gist::VarComparator<S> {
1412  private:
1413  const Printer& p;
1414  public:
1416  FZPrintingComparator(const Printer& p0);
1417 
1419  virtual void compare(const Space& s0, const Space& s1);
1420  };
1421 
1422  template<class S>
1423  FZPrintingComparator<S>::FZPrintingComparator(const Printer& p0)
1424  : Gecode::Gist::VarComparator<S>("Gecode/FlatZinc"), p(p0) {}
1425 
1426  template<class S>
1427  void
1428  FZPrintingComparator<S>::compare(const Space& s0, const Space& s1) {
1429  this->init();
1430  try {
1431  dynamic_cast<const S&>(s0).compare(dynamic_cast<const S&>(s1),
1432  this->getStream(), p);
1433  } catch (Exception& e) {
1434  this->getStream() << "Exception: " << e.what();
1435  }
1436  this->getStream() << std::endl;
1437  }
1438 
1439 #endif
1440 
1441 
1442  template<template<class> class Engine>
1443  void
1444  FlatZincSpace::runEngine(std::ostream& out, const Printer& p,
1445  const FlatZincOptions& opt, Support::Timer& t_total) {
1446  if (opt.restart()==RM_NONE) {
1447  runMeta<Engine,Driver::EngineToMeta>(out,p,opt,t_total);
1448  } else {
1449  runMeta<Engine,RBS>(out,p,opt,t_total);
1450  }
1451  }
1452 
1453  template<template<class> class Engine,
1454  template<template<class> class,class> class Meta>
1455  void
1456  FlatZincSpace::runMeta(std::ostream& out, const Printer& p,
1457  const FlatZincOptions& opt, Support::Timer& t_total) {
1458 #ifdef GECODE_HAS_GIST
1459  if (opt.mode() == SM_GIST) {
1460  FZPrintingInspector<FlatZincSpace> pi(p);
1461  FZPrintingComparator<FlatZincSpace> pc(p);
1462  (void) GistEngine<Engine<FlatZincSpace> >::explore(this,opt,&pi,&pc);
1463  return;
1464  }
1465 #endif
1466  StatusStatistics sstat;
1467  unsigned int n_p = 0;
1468  Support::Timer t_solve;
1469  t_solve.start();
1470  if (status(sstat) != SS_FAILED) {
1471  n_p = propagators();
1472  }
1473  Search::Options o;
1474  o.stop = Driver::CombinedStop::create(opt.node(), opt.fail(), opt.time(),
1475  true);
1476  o.c_d = opt.c_d();
1477  o.a_d = opt.a_d();
1478  o.threads = opt.threads();
1479  o.nogoods_limit = opt.nogoods() ? opt.nogoods_limit() : 0;
1480  o.cutoff = Driver::createCutoff(opt);
1481  if (opt.interrupt())
1483  Meta<Engine,FlatZincSpace> se(this,o);
1484  int noOfSolutions = opt.solutions();
1485  if (noOfSolutions == -1) {
1486  noOfSolutions = (_method == SAT) ? 1 : 0;
1487  }
1488  bool printAll = _method == SAT || opt.allSolutions() || noOfSolutions != 0;
1489  int findSol = noOfSolutions;
1490  FlatZincSpace* sol = NULL;
1491  while (FlatZincSpace* next_sol = se.next()) {
1492  delete sol;
1493  sol = next_sol;
1494  if (printAll) {
1495  sol->print(out, p);
1496  out << "----------" << std::endl;
1497  }
1498  if (--findSol==0)
1499  goto stopped;
1500  }
1501  if (sol && !printAll) {
1502  sol->print(out, p);
1503  out << "----------" << std::endl;
1504  }
1505  if (!se.stopped()) {
1506  if (sol) {
1507  out << "==========" << endl;
1508  } else {
1509  out << "=====UNSATISFIABLE=====" << endl;
1510  }
1511  } else if (!sol) {
1512  out << "=====UNKNOWN=====" << endl;
1513  }
1514  delete sol;
1515  stopped:
1516  if (opt.interrupt())
1518  if (opt.mode() == SM_STAT) {
1519  Gecode::Search::Statistics stat = se.statistics();
1520  out << endl
1521  << "%% runtime: ";
1522  Driver::stop(t_total,out);
1523  out << endl
1524  << "%% solvetime: ";
1525  Driver::stop(t_solve,out);
1526  out << endl
1527  << "%% solutions: "
1528  << std::abs(noOfSolutions - findSol) << endl
1529  << "%% variables: "
1530  << (intVarCount + boolVarCount + setVarCount) << endl
1531  << "%% propagators: " << n_p << endl
1532  << "%% propagations: " << sstat.propagate+stat.propagate << endl
1533  << "%% nodes: " << stat.node << endl
1534  << "%% failures: " << stat.fail << endl
1535  << "%% restarts: " << stat.restart << endl
1536  << "%% peak depth: " << stat.depth << endl
1537  << endl;
1538  }
1539  delete o.stop;
1540  }
1541 
1542 #ifdef GECODE_HAS_QT
1543  void
1544  FlatZincSpace::branchWithPlugin(AST::Node* ann) {
1545  if (AST::Call* c = dynamic_cast<AST::Call*>(ann)) {
1546  QString pluginName(c->id.c_str());
1547  if (QLibrary::isLibrary(pluginName+".dll")) {
1548  pluginName += ".dll";
1549  } else if (QLibrary::isLibrary(pluginName+".dylib")) {
1550  pluginName = "lib" + pluginName + ".dylib";
1551  } else if (QLibrary::isLibrary(pluginName+".so")) {
1552  // Must check .so after .dylib so that Mac OS uses .dylib
1553  pluginName = "lib" + pluginName + ".so";
1554  }
1555  QPluginLoader pl(pluginName);
1556  QObject* plugin_o = pl.instance();
1557  if (!plugin_o) {
1558  throw FlatZinc::Error("FlatZinc",
1559  "Error loading plugin "+pluginName.toStdString()+
1560  ": "+pl.errorString().toStdString());
1561  }
1562  BranchPlugin* pb = qobject_cast<BranchPlugin*>(plugin_o);
1563  if (!pb) {
1564  throw FlatZinc::Error("FlatZinc",
1565  "Error loading plugin "+pluginName.toStdString()+
1566  ": does not contain valid PluginBrancher");
1567  }
1568  pb->branch(*this, c);
1569  }
1570  }
1571 #else
1572  void
1573  FlatZincSpace::branchWithPlugin(AST::Node*) {
1574  throw FlatZinc::Error("FlatZinc",
1575  "Branching with plugins not supported (requires Qt support)");
1576  }
1577 #endif
1578 
1579  void
1580  FlatZincSpace::run(std::ostream& out, const Printer& p,
1581  const FlatZincOptions& opt, Support::Timer& t_total) {
1582  switch (_method) {
1583  case MIN:
1584  case MAX:
1585  runEngine<BAB>(out,p,opt,t_total);
1586  break;
1587  case SAT:
1588  runEngine<DFS>(out,p,opt,t_total);
1589  break;
1590  }
1591  }
1592 
1593  void
1595  if (_optVarIsInt) {
1596  if (_method == MIN)
1597  rel(*this, iv[_optVar], IRT_LE,
1598  static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
1599  else if (_method == MAX)
1600  rel(*this, iv[_optVar], IRT_GR,
1601  static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
1602  } else {
1603 #ifdef GECODE_HAS_FLOAT_VARS
1604  if (_method == MIN)
1605  rel(*this, fv[_optVar], FRT_LE,
1606  static_cast<const FlatZincSpace*>(&s)->fv[_optVar].val());
1607  else if (_method == MAX)
1608  rel(*this, fv[_optVar], FRT_GR,
1609  static_cast<const FlatZincSpace*>(&s)->fv[_optVar].val());
1610 #endif
1611  }
1612  }
1613 
1614  bool
1616  if (cri.restart() != 0 && _lns > 0) {
1617  const FlatZincSpace& last = static_cast<const FlatZincSpace&>(*cri.last());
1618  for (unsigned int i=iv_lns.size(); i--;) {
1619  if ((*_random)(99) <= _lns) {
1620  rel(*this, iv_lns[i], IRT_EQ, last.iv_lns[i]);
1621  }
1622  }
1623  return false;
1624  }
1625  return true;
1626  }
1627 
1628  Space*
1629  FlatZincSpace::copy(bool share) {
1630  return new FlatZincSpace(share, *this);
1631  }
1632 
1635  return _method;
1636  }
1637 
1638  int
1640  return _optVar;
1641  }
1642 
1643  bool
1645  return _optVarIsInt;
1646  }
1647 
1648  void
1649  FlatZincSpace::print(std::ostream& out, const Printer& p) const {
1650  p.print(out, iv, bv
1651 #ifdef GECODE_HAS_SET_VARS
1652  , sv
1653 #endif
1654 #ifdef GECODE_HAS_FLOAT_VARS
1655  , fv
1656 #endif
1657  );
1658  }
1659 
1660  void
1661  FlatZincSpace::compare(const Space& s, std::ostream& out) const {
1662  (void) s; (void) out;
1663 #ifdef GECODE_HAS_GIST
1664  const FlatZincSpace& fs = dynamic_cast<const FlatZincSpace&>(s);
1665  for (int i = 0; i < iv.size(); ++i) {
1666  std::stringstream ss;
1667  ss << "iv[" << i << "]";
1668  std::string result(Gecode::Gist::Comparator::compare(ss.str(), iv[i],
1669  fs.iv[i]));
1670  if (result.length() > 0) out << result << std::endl;
1671  }
1672  for (int i = 0; i < bv.size(); ++i) {
1673  std::stringstream ss;
1674  ss << "bv[" << i << "]";
1675  std::string result(Gecode::Gist::Comparator::compare(ss.str(), bv[i],
1676  fs.bv[i]));
1677  if (result.length() > 0) out << result << std::endl;
1678  }
1679 #ifdef GECODE_HAS_SET_VARS
1680  for (int i = 0; i < sv.size(); ++i) {
1681  std::stringstream ss;
1682  ss << "sv[" << i << "]";
1683  std::string result(Gecode::Gist::Comparator::compare(ss.str(), sv[i],
1684  fs.sv[i]));
1685  if (result.length() > 0) out << result << std::endl;
1686  }
1687 #endif
1688 #ifdef GECODE_HAS_FLOAT_VARS
1689  for (int i = 0; i < fv.size(); ++i) {
1690  std::stringstream ss;
1691  ss << "fv[" << i << "]";
1692  std::string result(Gecode::Gist::Comparator::compare(ss.str(), fv[i],
1693  fs.fv[i]));
1694  if (result.length() > 0) out << result << std::endl;
1695  }
1696 #endif
1697 #endif
1698  }
1699 
1700  void
1701  FlatZincSpace::compare(const FlatZincSpace& s, std::ostream& out,
1702  const Printer& p) const {
1703  p.printDiff(out, iv, s.iv, bv, s.bv
1704 #ifdef GECODE_HAS_SET_VARS
1705  , sv, s.sv
1706 #endif
1707 #ifdef GECODE_HAS_FLOAT_VARS
1708  , fv, s.fv
1709 #endif
1710  );
1711  }
1712 
1713  void
1715  p.shrinkArrays(*this, _optVar, _optVarIsInt, iv, bv
1716 #ifdef GECODE_HAS_SET_VARS
1717  , sv
1718 #endif
1719 #ifdef GECODE_HAS_FLOAT_VARS
1720  , fv
1721 #endif
1722  );
1723  }
1724 
1725  IntArgs
1727  AST::Array* a = arg->getArray();
1728  IntArgs ia(a->a.size()+offset);
1729  for (int i=offset; i--;)
1730  ia[i] = 0;
1731  for (int i=a->a.size(); i--;)
1732  ia[i+offset] = a->a[i]->getInt();
1733  return ia;
1734  }
1735  IntArgs
1737  AST::Array* a = arg->getArray();
1738  IntArgs ia(a->a.size()+offset);
1739  for (int i=offset; i--;)
1740  ia[i] = 0;
1741  for (int i=a->a.size(); i--;)
1742  ia[i+offset] = a->a[i]->getBool();
1743  return ia;
1744  }
1745  IntSet
1747  AST::SetLit* sl = n->getSet();
1748  IntSet d;
1749  if (sl->interval) {
1750  d = IntSet(sl->min, sl->max);
1751  } else {
1752  Region re(*this);
1753  int* is = re.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
1754  for (int i=sl->s.size(); i--; )
1755  is[i] = sl->s[i];
1756  d = IntSet(is, sl->s.size());
1757  }
1758  return d;
1759  }
1760  IntSetArgs
1762  AST::Array* a = arg->getArray();
1763  if (a->a.size() == 0) {
1764  IntSetArgs emptyIa(0);
1765  return emptyIa;
1766  }
1767  IntSetArgs ia(a->a.size()+offset);
1768  for (int i=offset; i--;)
1769  ia[i] = IntSet::empty;
1770  for (int i=a->a.size(); i--;) {
1771  ia[i+offset] = arg2intset(a->a[i]);
1772  }
1773  return ia;
1774  }
1775  IntVarArgs
1777  AST::Array* a = arg->getArray();
1778  if (a->a.size() == 0) {
1779  IntVarArgs emptyIa(0);
1780  return emptyIa;
1781  }
1782  IntVarArgs ia(a->a.size()+offset);
1783  for (int i=offset; i--;)
1784  ia[i] = IntVar(*this, 0, 0);
1785  for (int i=a->a.size(); i--;) {
1786  if (a->a[i]->isIntVar()) {
1787  ia[i+offset] = iv[a->a[i]->getIntVar()];
1788  } else {
1789  int value = a->a[i]->getInt();
1790  IntVar iv(*this, value, value);
1791  ia[i+offset] = iv;
1792  }
1793  }
1794  return ia;
1795  }
1796  BoolVarArgs
1797  FlatZincSpace::arg2boolvarargs(AST::Node* arg, int offset, int siv) {
1798  AST::Array* a = arg->getArray();
1799  if (a->a.size() == 0) {
1800  BoolVarArgs emptyIa(0);
1801  return emptyIa;
1802  }
1803  BoolVarArgs ia(a->a.size()+offset-(siv==-1?0:1));
1804  for (int i=offset; i--;)
1805  ia[i] = BoolVar(*this, 0, 0);
1806  for (int i=0; i<static_cast<int>(a->a.size()); i++) {
1807  if (i==siv)
1808  continue;
1809  if (a->a[i]->isBool()) {
1810  bool value = a->a[i]->getBool();
1811  BoolVar iv(*this, value, value);
1812  ia[offset++] = iv;
1813  } else if (a->a[i]->isIntVar() &&
1814  aliasBool2Int(a->a[i]->getIntVar()) != -1) {
1815  ia[offset++] = bv[aliasBool2Int(a->a[i]->getIntVar())];
1816  } else {
1817  ia[offset++] = bv[a->a[i]->getBoolVar()];
1818  }
1819  }
1820  return ia;
1821  }
1822  BoolVar
1824  BoolVar x0;
1825  if (n->isBool()) {
1826  x0 = BoolVar(*this, n->getBool(), n->getBool());
1827  }
1828  else {
1829  x0 = bv[n->getBoolVar()];
1830  }
1831  return x0;
1832  }
1833  IntVar
1835  IntVar x0;
1836  if (n->isIntVar()) {
1837  x0 = iv[n->getIntVar()];
1838  } else {
1839  x0 = IntVar(*this, n->getInt(), n->getInt());
1840  }
1841  return x0;
1842  }
1843  bool
1845  AST::Array* a = b->getArray();
1846  singleInt = -1;
1847  if (a->a.size() == 0)
1848  return true;
1849  for (int i=a->a.size(); i--;) {
1850  if (a->a[i]->isBoolVar() || a->a[i]->isBool()) {
1851  } else if (a->a[i]->isIntVar()) {
1852  if (aliasBool2Int(a->a[i]->getIntVar()) == -1) {
1853  if (singleInt != -1) {
1854  return false;
1855  }
1856  singleInt = i;
1857  }
1858  } else {
1859  return false;
1860  }
1861  }
1862  return singleInt==-1 || a->a.size() > 1;
1863  }
1864 #ifdef GECODE_HAS_SET_VARS
1865  SetVar
1867  SetVar x0;
1868  if (!n->isSetVar()) {
1869  IntSet d = arg2intset(n);
1870  x0 = SetVar(*this, d, d);
1871  } else {
1872  x0 = sv[n->getSetVar()];
1873  }
1874  return x0;
1875  }
1876  SetVarArgs
1877  FlatZincSpace::arg2setvarargs(AST::Node* arg, int offset, int doffset,
1878  const IntSet& od) {
1879  AST::Array* a = arg->getArray();
1880  SetVarArgs ia(a->a.size()+offset);
1881  for (int i=offset; i--;) {
1882  IntSet d = i<doffset ? od : IntSet::empty;
1883  ia[i] = SetVar(*this, d, d);
1884  }
1885  for (int i=a->a.size(); i--;) {
1886  ia[i+offset] = arg2SetVar(a->a[i]);
1887  }
1888  return ia;
1889  }
1890 #endif
1891 #ifdef GECODE_HAS_FLOAT_VARS
1892  FloatValArgs
1894  AST::Array* a = arg->getArray();
1895  FloatValArgs fa(a->a.size()+offset);
1896  for (int i=offset; i--;)
1897  fa[i] = 0.0;
1898  for (int i=a->a.size(); i--;)
1899  fa[i+offset] = a->a[i]->getFloat();
1900  return fa;
1901  }
1902  FloatVarArgs
1904  AST::Array* a = arg->getArray();
1905  if (a->a.size() == 0) {
1906  FloatVarArgs emptyFa(0);
1907  return emptyFa;
1908  }
1909  FloatVarArgs fa(a->a.size()+offset);
1910  for (int i=offset; i--;)
1911  fa[i] = FloatVar(*this, 0.0, 0.0);
1912  for (int i=a->a.size(); i--;) {
1913  if (a->a[i]->isFloatVar()) {
1914  fa[i+offset] = fv[a->a[i]->getFloatVar()];
1915  } else {
1916  double value = a->a[i]->getFloat();
1917  FloatVar fv(*this, value, value);
1918  fa[i+offset] = fv;
1919  }
1920  }
1921  return fa;
1922  }
1923  FloatVar
1925  FloatVar x0;
1926  if (n->isFloatVar()) {
1927  x0 = fv[n->getFloatVar()];
1928  } else {
1929  x0 = FloatVar(*this, n->getFloat(), n->getFloat());
1930  }
1931  return x0;
1932  }
1933 #endif
1934  IntConLevel
1936  if (ann) {
1937  if (ann->hasAtom("val"))
1938  return ICL_VAL;
1939  if (ann->hasAtom("domain"))
1940  return ICL_DOM;
1941  if (ann->hasAtom("bounds") ||
1942  ann->hasAtom("boundsR") ||
1943  ann->hasAtom("boundsD") ||
1944  ann->hasAtom("boundsZ"))
1945  return ICL_BND;
1946  }
1947  return ICL_DEF;
1948  }
1949 
1950 
1951  void
1953  _output = output;
1954  }
1955 
1956  void
1957  Printer::printElem(std::ostream& out,
1958  AST::Node* ai,
1959  const Gecode::IntVarArray& iv,
1960  const Gecode::BoolVarArray& bv
1961 #ifdef GECODE_HAS_SET_VARS
1962  , const Gecode::SetVarArray& sv
1963 #endif
1964 #ifdef GECODE_HAS_FLOAT_VARS
1965  ,
1966  const Gecode::FloatVarArray& fv
1967 #endif
1968  ) const {
1969  int k;
1970  if (ai->isInt(k)) {
1971  out << k;
1972  } else if (ai->isIntVar()) {
1973  out << iv[ai->getIntVar()];
1974  } else if (ai->isBoolVar()) {
1975  if (bv[ai->getBoolVar()].min() == 1) {
1976  out << "true";
1977  } else if (bv[ai->getBoolVar()].max() == 0) {
1978  out << "false";
1979  } else {
1980  out << "false..true";
1981  }
1982 #ifdef GECODE_HAS_SET_VARS
1983  } else if (ai->isSetVar()) {
1984  if (!sv[ai->getSetVar()].assigned()) {
1985  out << sv[ai->getSetVar()];
1986  return;
1987  }
1988  SetVarGlbRanges svr(sv[ai->getSetVar()]);
1989  if (!svr()) {
1990  out << "{}";
1991  return;
1992  }
1993  int min = svr.min();
1994  int max = svr.max();
1995  ++svr;
1996  if (svr()) {
1997  SetVarGlbValues svv(sv[ai->getSetVar()]);
1998  int i = svv.val();
1999  out << "{" << i;
2000  ++svv;
2001  for (; svv(); ++svv)
2002  out << ", " << svv.val();
2003  out << "}";
2004  } else {
2005  out << min << ".." << max;
2006  }
2007 #endif
2008 #ifdef GECODE_HAS_FLOAT_VARS
2009  } else if (ai->isFloatVar()) {
2010  if (fv[ai->getFloatVar()].assigned()) {
2011  FloatVal vv = fv[ai->getFloatVar()].val();
2012  FloatNum v;
2013  if (vv.singleton())
2014  v = vv.min();
2015  else if (vv < 0.0)
2016  v = vv.max();
2017  else
2018  v = vv.min();
2019  std::ostringstream oss;
2020  // oss << std::scientific;
2021  oss << std::setprecision(std::numeric_limits<double>::digits10);
2022  oss << v;
2023  if (oss.str().find(".") == std::string::npos)
2024  oss << ".0";
2025  out << oss.str();
2026  } else {
2027  out << fv[ai->getFloatVar()];
2028  }
2029 #endif
2030  } else if (ai->isBool()) {
2031  out << (ai->getBool() ? "true" : "false");
2032  } else if (ai->isSet()) {
2033  AST::SetLit* s = ai->getSet();
2034  if (s->interval) {
2035  out << s->min << ".." << s->max;
2036  } else {
2037  out << "{";
2038  for (unsigned int i=0; i<s->s.size(); i++) {
2039  out << s->s[i] << (i < s->s.size()-1 ? ", " : "}");
2040  }
2041  }
2042  } else if (ai->isString()) {
2043  std::string s = ai->getString();
2044  for (unsigned int i=0; i<s.size(); i++) {
2045  if (s[i] == '\\' && i<s.size()-1) {
2046  switch (s[i+1]) {
2047  case 'n': out << "\n"; break;
2048  case '\\': out << "\\"; break;
2049  case 't': out << "\t"; break;
2050  default: out << "\\" << s[i+1];
2051  }
2052  i++;
2053  } else {
2054  out << s[i];
2055  }
2056  }
2057  }
2058  }
2059 
2060  void
2061  Printer::printElemDiff(std::ostream& out,
2062  AST::Node* ai,
2063  const Gecode::IntVarArray& iv1,
2064  const Gecode::IntVarArray& iv2,
2065  const Gecode::BoolVarArray& bv1,
2066  const Gecode::BoolVarArray& bv2
2067 #ifdef GECODE_HAS_SET_VARS
2068  , const Gecode::SetVarArray& sv1,
2069  const Gecode::SetVarArray& sv2
2070 #endif
2071 #ifdef GECODE_HAS_FLOAT_VARS
2072  , const Gecode::FloatVarArray& fv1,
2073  const Gecode::FloatVarArray& fv2
2074 #endif
2075  ) const {
2076 #ifdef GECODE_HAS_GIST
2077  using namespace Gecode::Gist;
2078  int k;
2079  if (ai->isInt(k)) {
2080  out << k;
2081  } else if (ai->isIntVar()) {
2082  std::string res(Comparator::compare("",iv1[ai->getIntVar()],
2083  iv2[ai->getIntVar()]));
2084  if (res.length() > 0) {
2085  res.erase(0, 1); // Remove '='
2086  out << res;
2087  } else {
2088  out << iv1[ai->getIntVar()];
2089  }
2090  } else if (ai->isBoolVar()) {
2091  std::string res(Comparator::compare("",bv1[ai->getBoolVar()],
2092  bv2[ai->getBoolVar()]));
2093  if (res.length() > 0) {
2094  res.erase(0, 1); // Remove '='
2095  out << res;
2096  } else {
2097  out << bv1[ai->getBoolVar()];
2098  }
2099 #ifdef GECODE_HAS_SET_VARS
2100  } else if (ai->isSetVar()) {
2101  std::string res(Comparator::compare("",sv1[ai->getSetVar()],
2102  sv2[ai->getSetVar()]));
2103  if (res.length() > 0) {
2104  res.erase(0, 1); // Remove '='
2105  out << res;
2106  } else {
2107  out << sv1[ai->getSetVar()];
2108  }
2109 #endif
2110 #ifdef GECODE_HAS_FLOAT_VARS
2111  } else if (ai->isFloatVar()) {
2112  std::string res(Comparator::compare("",fv1[ai->getFloatVar()],
2113  fv2[ai->getFloatVar()]));
2114  if (res.length() > 0) {
2115  res.erase(0, 1); // Remove '='
2116  out << res;
2117  } else {
2118  out << fv1[ai->getFloatVar()];
2119  }
2120 #endif
2121  } else if (ai->isBool()) {
2122  out << (ai->getBool() ? "true" : "false");
2123  } else if (ai->isSet()) {
2124  AST::SetLit* s = ai->getSet();
2125  if (s->interval) {
2126  out << s->min << ".." << s->max;
2127  } else {
2128  out << "{";
2129  for (unsigned int i=0; i<s->s.size(); i++) {
2130  out << s->s[i] << (i < s->s.size()-1 ? ", " : "}");
2131  }
2132  }
2133  } else if (ai->isString()) {
2134  std::string s = ai->getString();
2135  for (unsigned int i=0; i<s.size(); i++) {
2136  if (s[i] == '\\' && i<s.size()-1) {
2137  switch (s[i+1]) {
2138  case 'n': out << "\n"; break;
2139  case '\\': out << "\\"; break;
2140  case 't': out << "\t"; break;
2141  default: out << "\\" << s[i+1];
2142  }
2143  i++;
2144  } else {
2145  out << s[i];
2146  }
2147  }
2148  }
2149 #else
2150  (void) out;
2151  (void) ai;
2152  (void) iv1;
2153  (void) iv2;
2154  (void) bv1;
2155  (void) bv2;
2156 #ifdef GECODE_HAS_SET_VARS
2157  (void) sv1;
2158  (void) sv2;
2159 #endif
2160 #ifdef GECODE_HAS_FLOAT_VARS
2161  (void) fv1;
2162  (void) fv2;
2163 #endif
2164 
2165 #endif
2166  }
2167 
2168  void
2169  Printer::print(std::ostream& out,
2170  const Gecode::IntVarArray& iv,
2171  const Gecode::BoolVarArray& bv
2172 #ifdef GECODE_HAS_SET_VARS
2173  ,
2174  const Gecode::SetVarArray& sv
2175 #endif
2176 #ifdef GECODE_HAS_FLOAT_VARS
2177  ,
2178  const Gecode::FloatVarArray& fv
2179 #endif
2180  ) const {
2181  if (_output == NULL)
2182  return;
2183  for (unsigned int i=0; i< _output->a.size(); i++) {
2184  AST::Node* ai = _output->a[i];
2185  if (ai->isArray()) {
2186  AST::Array* aia = ai->getArray();
2187  int size = aia->a.size();
2188  out << "[";
2189  for (int j=0; j<size; j++) {
2190  printElem(out,aia->a[j],iv,bv
2191 #ifdef GECODE_HAS_SET_VARS
2192  ,sv
2193 #endif
2194 #ifdef GECODE_HAS_FLOAT_VARS
2195  ,fv
2196 #endif
2197  );
2198  if (j<size-1)
2199  out << ", ";
2200  }
2201  out << "]";
2202  } else {
2203  printElem(out,ai,iv,bv
2204 #ifdef GECODE_HAS_SET_VARS
2205  ,sv
2206 #endif
2207 #ifdef GECODE_HAS_FLOAT_VARS
2208  ,fv
2209 #endif
2210  );
2211  }
2212  }
2213  }
2214 
2215  void
2216  Printer::printDiff(std::ostream& out,
2217  const Gecode::IntVarArray& iv1,
2218  const Gecode::IntVarArray& iv2,
2219  const Gecode::BoolVarArray& bv1,
2220  const Gecode::BoolVarArray& bv2
2221 #ifdef GECODE_HAS_SET_VARS
2222  ,
2223  const Gecode::SetVarArray& sv1,
2224  const Gecode::SetVarArray& sv2
2225 #endif
2226 #ifdef GECODE_HAS_FLOAT_VARS
2227  ,
2228  const Gecode::FloatVarArray& fv1,
2229  const Gecode::FloatVarArray& fv2
2230 #endif
2231  ) const {
2232  if (_output == NULL)
2233  return;
2234  for (unsigned int i=0; i< _output->a.size(); i++) {
2235  AST::Node* ai = _output->a[i];
2236  if (ai->isArray()) {
2237  AST::Array* aia = ai->getArray();
2238  int size = aia->a.size();
2239  out << "[";
2240  for (int j=0; j<size; j++) {
2241  printElemDiff(out,aia->a[j],iv1,iv2,bv1,bv2
2242 #ifdef GECODE_HAS_SET_VARS
2243  ,sv1,sv2
2244 #endif
2245 #ifdef GECODE_HAS_FLOAT_VARS
2246  ,fv1,fv2
2247 #endif
2248  );
2249  if (j<size-1)
2250  out << ", ";
2251  }
2252  out << "]";
2253  } else {
2254  printElemDiff(out,ai,iv1,iv2,bv1,bv2
2255 #ifdef GECODE_HAS_SET_VARS
2256  ,sv1,sv2
2257 #endif
2258 #ifdef GECODE_HAS_FLOAT_VARS
2259  ,fv1,fv2
2260 #endif
2261  );
2262  }
2263  }
2264  }
2265 
2266  void
2268  std::map<int,int>& iv, std::map<int,int>& bv,
2269  std::map<int,int>& sv, std::map<int,int>& fv) {
2270  if (node->isIntVar()) {
2271  AST::IntVar* x = static_cast<AST::IntVar*>(node);
2272  if (iv.find(x->i) == iv.end()) {
2273  int newi = iv.size();
2274  iv[x->i] = newi;
2275  }
2276  x->i = iv[x->i];
2277  } else if (node->isBoolVar()) {
2278  AST::BoolVar* x = static_cast<AST::BoolVar*>(node);
2279  if (bv.find(x->i) == bv.end()) {
2280  int newi = bv.size();
2281  bv[x->i] = newi;
2282  }
2283  x->i = bv[x->i];
2284  } else if (node->isSetVar()) {
2285  AST::SetVar* x = static_cast<AST::SetVar*>(node);
2286  if (sv.find(x->i) == sv.end()) {
2287  int newi = sv.size();
2288  sv[x->i] = newi;
2289  }
2290  x->i = sv[x->i];
2291  } else if (node->isFloatVar()) {
2292  AST::FloatVar* x = static_cast<AST::FloatVar*>(node);
2293  if (fv.find(x->i) == fv.end()) {
2294  int newi = fv.size();
2295  fv[x->i] = newi;
2296  }
2297  x->i = fv[x->i];
2298  }
2299  }
2300 
2301  void
2303  int& optVar, bool optVarIsInt,
2304  Gecode::IntVarArray& iv,
2306 #ifdef GECODE_HAS_SET_VARS
2307  ,
2309 #endif
2310 #ifdef GECODE_HAS_FLOAT_VARS
2311  ,
2313 #endif
2314  ) {
2315  if (_output == NULL) {
2316  if (optVarIsInt && optVar != -1) {
2317  IntVar ov = iv[optVar];
2318  iv = IntVarArray(home, 1);
2319  iv[0] = ov;
2320  optVar = 0;
2321  } else {
2322  iv = IntVarArray(home, 0);
2323  }
2324  bv = BoolVarArray(home, 0);
2325 #ifdef GECODE_HAS_SET_VARS
2326  sv = SetVarArray(home, 0);
2327 #endif
2328 #ifdef GECODE_HAS_FLOAT_VARS
2329  if (!optVarIsInt && optVar != -1) {
2330  FloatVar ov = fv[optVar];
2331  fv = FloatVarArray(home, 1);
2332  fv[0] = ov;
2333  optVar = 0;
2334  } else {
2335  fv = FloatVarArray(home,0);
2336  }
2337 #endif
2338  return;
2339  }
2340  std::map<int,int> iv_new;
2341  std::map<int,int> bv_new;
2342  std::map<int,int> sv_new;
2343  std::map<int,int> fv_new;
2344 
2345  if (optVar != -1) {
2346  if (optVarIsInt)
2347  iv_new[optVar] = 0;
2348  else
2349  fv_new[optVar] = 0;
2350  optVar = 0;
2351  }
2352 
2353  for (unsigned int i=0; i< _output->a.size(); i++) {
2354  AST::Node* ai = _output->a[i];
2355  if (ai->isArray()) {
2356  AST::Array* aia = ai->getArray();
2357  for (unsigned int j=0; j<aia->a.size(); j++) {
2358  shrinkElement(aia->a[j],iv_new,bv_new,sv_new,fv_new);
2359  }
2360  } else {
2361  shrinkElement(ai,iv_new,bv_new,sv_new,fv_new);
2362  }
2363  }
2364 
2365  IntVarArgs iva(iv_new.size());
2366  for (map<int,int>::iterator i=iv_new.begin(); i != iv_new.end(); ++i) {
2367  iva[(*i).second] = iv[(*i).first];
2368  }
2369  iv = IntVarArray(home, iva);
2370 
2371  BoolVarArgs bva(bv_new.size());
2372  for (map<int,int>::iterator i=bv_new.begin(); i != bv_new.end(); ++i) {
2373  bva[(*i).second] = bv[(*i).first];
2374  }
2375  bv = BoolVarArray(home, bva);
2376 
2377 #ifdef GECODE_HAS_SET_VARS
2378  SetVarArgs sva(sv_new.size());
2379  for (map<int,int>::iterator i=sv_new.begin(); i != sv_new.end(); ++i) {
2380  sva[(*i).second] = sv[(*i).first];
2381  }
2382  sv = SetVarArray(home, sva);
2383 #endif
2384 
2385 #ifdef GECODE_HAS_FLOAT_VARS
2386  FloatVarArgs fva(fv_new.size());
2387  for (map<int,int>::iterator i=fv_new.begin(); i != fv_new.end(); ++i) {
2388  fva[(*i).second] = fv[(*i).first];
2389  }
2390  fv = FloatVarArray(home, fva);
2391 #endif
2392  }
2393 
2395  delete _output;
2396  }
2397 
2398 }}
2399 
2400 // STATISTICS: flatzinc-any
void click(Inspector *i)
Add inspector that reacts on node double clicks.
Definition: gist.hpp:174
SetVarBranch SET_VAR_SIZE_MIN(BranchTbl tbl)
Select variable with smallest unknown set.
Definition: var.hpp:183
void shrinkArrays(Printer &p)
Remove all variables not needed for output.
Definition: flatzinc.cpp:1714
static void post(Home home, TieBreak< IntVarBranch > int_varsel, IntValBranch int_valsel, TieBreak< IntVarBranch > bool_varsel, IntValBranch bool_valsel, SetVarBranch set_varsel, SetValBranch set_valsel, TieBreak< FloatVarBranch > float_varsel, FloatValBranch float_valsel)
Post brancher.
Definition: flatzinc.cpp:198
unsigned int a_d
Create a clone during recomputation if distance is greater than a_d (adaptive distance) ...
Definition: search.hh:213
Which values to select for branching first.
Definition: set.hh:1382
Gecode::SetVarArray sv_aux
The introduced set variables.
Definition: flatzinc.hh:444
SetVarBranch SET_VAR_AFC_MIN(double d, BranchTbl tbl)
Select variable with smallest accumulated failure count with decay factor d.
Definition: var.hpp:123
int floatVarCount
Number of float variables.
Definition: flatzinc.hh:384
Passing float arguments.
Definition: float.hh:937
void varValPrintF(const Space &home, const BrancherHandle &bh, unsigned int a, FloatVar, int i, const FloatNumBranch &nl, std::ostream &o)
Definition: flatzinc.cpp:312
Option< AST::SetLit * > domain
Definition: varspec.hh:78
Options for running FlatZinc models
Definition: flatzinc.hh:205
FloatVarBranch FLOAT_VAR_DEGREE_MAX(BranchTbl tbl)
Select variable with largest degree.
Definition: var.hpp:119
virtual Choice * choice(Space &home)
Return choice.
Definition: flatzinc.cpp:155
IntVarBranch INT_VAR_NONE(void)
Select first unassigned variable.
Definition: var.hpp:108
Combine variable selection criteria for tie-breaking.
IntSet vs2is(IntVarSpec *vs)
Definition: flatzinc.cpp:328
Gecode::Support::RandomGenerator random
The actual random number generator.
Definition: flatzinc.hh:357
Which values to select for branching first.
Definition: float.hh:1646
void printDiff(std::ostream &out, const Gecode::IntVarArray &iv1, const Gecode::IntVarArray &iv2, const Gecode::BoolVarArray &bv1, const Gecode::BoolVarArray &bv2, const Gecode::SetVarArray &sv1, const Gecode::SetVarArray &sv2, const Gecode::FloatVarArray &fv1, const Gecode::FloatVarArray &fv2) const
Definition: flatzinc.cpp:2216
IntConLevel
Consistency levels for integer propagators.
Definition: int.hh:937
The shared handle.
Definition: core.hpp:79
IntArgs arg2intargs(AST::Node *arg, int offset=0)
Convert arg (array of integers) to IntArgs.
Definition: flatzinc.cpp:1726
void post(FlatZincSpace &s, const ConExpr &ce)
Post constraint specified by ce.
Definition: registry.cpp:63
FloatValBranch FLOAT_VAL_SPLIT_MAX(void)
Select values greater than mean of smallest and largest value.
Definition: val.hpp:64
SetVarBranch SET_VAR_NONE(void)
Select first unassigned variable.
Definition: var.hpp:91
void createBranchers(AST::Node *ann, int seed, double decay, bool ignoreUnknown, std::ostream &err=std::cerr)
Create branchers corresponding to the solve item annotations.
Definition: flatzinc.cpp:879
Search engine statistics
Definition: search.hh:136
std::string what(void) const
Definition: ast.hh:65
Boolean variable node.
Definition: ast.hh:201
const int min
Smallest allowed integer in integer set.
Definition: set.hh:101
FloatVarArgs arg2floatvarargs(AST::Node *arg, int offset=0)
Convert n to FloatVarArgs.
Definition: flatzinc.cpp:1903
bool isBool(void)
Test if node is a Boolean node.
Definition: ast.hh:494
virtual Gecode::Space * copy(bool share)
Copy function.
Definition: flatzinc.cpp:1629
std::vector< bool > sv_introduced
Indicates whether a set variable is introduced by mzn2fzn.
Definition: flatzinc.hh:446
bool getBool(void)
Cast this node to a Boolean node.
Definition: ast.hh:450
const FloatNum max
Largest allowed float value.
Definition: float.hh:831
#define GECODE_HAS_SET_VARS
Definition: config.hpp:78
Gecode::BoolVarArray bv
The Boolean variables.
Definition: flatzinc.hh:435
void put(unsigned int i)
Add i to the contents.
Definition: archive.hpp:177
int size(void) const
Return size of array (number of elements)
Definition: array.hpp:1662
Meth _method
Whether to solve as satisfaction or optimization problem.
Definition: flatzinc.hh:394
unsigned int c_d
Create a clone after every c_d commits (commit distance)
Definition: search.hh:211
Space * clone(bool share=true, CloneStatistics &stat=unused_clone) const
Clone space.
Definition: core.hpp:2854
T * alloc(long unsigned int n)
Allocate block of n objects of type T from region.
Definition: region.hpp:326
SetValBranch ann2svalsel(AST::Node *ann, std::string r0, std::string r1, Rnd rnd)
Definition: flatzinc.cpp:529
Which values to select for branching first.
Definition: int.hh:3981
Search engine options
Definition: search.hh:204
SetLit * getSet(void)
Cast this node to a set literal node.
Definition: ast.hh:462
void newIntVar(IntVarSpec *vs)
Create new integer variable from specification.
Definition: flatzinc.cpp:723
Abstract base class for comparators.
Definition: gist.hh:123
Call * getCall(void)
Return function call.
Definition: ast.hh:347
void max(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:57
Value propagation or consistency (naive)
Definition: int.hh:938
int getFloatVar(void)
Cast this node to a Float variable node.
Definition: ast.hh:432
Gecode::IntVarArray iv
The integer variables.
Definition: flatzinc.hh:423
SetVarBranch SET_VAR_ACTIVITY_MIN(double d, BranchTbl tbl)
Select variable with lowest activity with decay factor d.
Definition: var.hpp:143
void abs(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition: arithmetic.cpp:49
void stop(Support::Timer &timer, std::ostream &os)
Get time since start of timer and print user friendly time information.
Definition: script.cpp:46
IntAssign INT_ASSIGN_MED(void)
Select greatest value not greater than the median.
Definition: assign.hpp:64
Handle for brancher.
Definition: core.hpp:1157
Passing float variables.
Definition: float.hh:966
Specification for set variables.
Definition: varspec.hh:143
BranchInformation branchInfo
Information for printing branches.
Definition: flatzinc.hh:541
int boolVarCount
Number of Boolean variables.
Definition: flatzinc.hh:382
SetValBranch SET_VAL_MIN_INC(void)
Include smallest element.
Definition: val.hpp:59
SetVarBranch SET_VAR_ACTIVITY_SIZE_MIN(double d, BranchTbl tbl)
Select variable with smallest activity divided by domain size with decay factor d.
Definition: var.hpp:223
virtual const char * what(void) const
Return information.
Definition: exception.cpp:59
void dom(Home home, FloatVar x, FloatVal n)
Propagates .
Definition: dom.cpp:44
IntVarBranch INT_VAR_SIZE_MIN(BranchTbl tbl)
Select variable with smallest domain size.
Definition: var.hpp:212
void postConstraints(std::vector< ConExpr * > &ces)
Post a constraint specified by ce.
Definition: flatzinc.cpp:846
void minimize(int var, bool isInt, AST::Array *annotation)
Post that integer variable var should be minimized.
Definition: flatzinc.cpp:1320
IntVarBranch INT_VAR_MIN_MIN(BranchTbl tbl)
Select variable with smallest min.
Definition: var.hpp:192
unsigned long int fail
Number of failed nodes in search tree.
Definition: search.hh:139
const Val & some(void) const
Definition: option.hh:51
bool isSetVar(void)
Test if node is a set variable node.
Definition: ast.hh:482
bool isBoolVar(void)
Test if node is a Boolean variable node.
Definition: ast.hh:478
void compare(const Space &s, std::ostream &out) const
Compare this space with space s and print the differences on out.
Definition: flatzinc.cpp:1661
std::vector< Node * > a
Definition: ast.hh:237
unsigned long int depth
Maximum depth of search stack.
Definition: search.hh:143
void print(const BrancherHandle &bh, int a, int i, const FloatNumBranch &nl, ostream &o) const
Definition: flatzinc.cpp:263
TieBreak< IntVarBranch > ann2ivarsel(AST::Node *ann, Rnd rnd, double decay)
Definition: flatzinc.cpp:372
Integer variable array.
Definition: int.hh:741
FloatVarBranch FLOAT_VAR_AFC_MIN(double d, BranchTbl tbl)
Select variable with smallest accumulated failure count with decay factor d.
Definition: var.hpp:124
FloatValBranch ann2fvalsel(AST::Node *ann, std::string r0, std::string r1)
Definition: flatzinc.cpp:603
No restarts.
Definition: driver.hh:110
FloatVarBranch FLOAT_VAR_ACTIVITY_SIZE_MAX(double d, BranchTbl tbl)
Select variable with largest activity divided by domain size with decay factor d. ...
Definition: var.hpp:234
Less ( )
Definition: float.hh:1058
IntVarBranch INT_VAR_ACTIVITY_MAX(double d, BranchTbl tbl)
Select variable with highest activity with decay factor d.
Definition: var.hpp:182
int vs2bsh(BoolVarSpec *bs)
Definition: flatzinc.cpp:360
void init(int intVars, int boolVars, int setVars, int floatVars)
Initialize space with given number of variables.
Definition: flatzinc.cpp:698
Handle to region.
Definition: region.hpp:61
Greater ( )
Definition: int.hh:909
AuxVarBrancher(Space &home, bool share, AuxVarBrancher &b)
Copy constructor.
Definition: flatzinc.cpp:99
FloatVarBranch FLOAT_VAR_ACTIVITY_MAX(double d, BranchTbl tbl)
Select variable with highest activity with decay factor d.
Definition: var.hpp:154
unsigned long int propagate
Number of propagator executions.
Definition: core.hpp:1313
Search::Cutoff * createCutoff(const Options &o)
Create cutoff object from options.
Definition: script.hpp:157
const int max
Largest allowed integer in integer set.
Definition: set.hh:99
Array * getArray(void)
Cast this node to an array node.
Definition: ast.hh:400
A thread-safe random number generator.
Definition: flatzinc.hh:354
const int max
Largest allowed integer value.
Definition: int.hh:113
Float variable array.
Definition: float.hh:1016
int vs2bsl(BoolVarSpec *bs)
Definition: flatzinc.cpp:348
Current restart information during search.
Definition: core.hpp:1265
Computation spaces.
Definition: core.hpp:1362
Abstract base class for inspectors.
Definition: gist.hh:103
FloatVarBranch FLOAT_VAR_NONE(void)
Select first unassigned variable.
Definition: var.hpp:92
const int min
Smallest allowed integer value.
Definition: int.hh:115
IntVarBranch INT_VAR_REGRET_MIN_MAX(BranchTbl tbl)
Select variable with largest min-regret.
Definition: var.hpp:277
Base-class for both propagators and branchers.
Definition: core.hpp:666
virtual SharedHandle::Object * copy(void) const
Return fresh copy for update.
Definition: flatzinc.cpp:245
SetVarBranch SET_VAR_SIZE_MAX(BranchTbl tbl)
Select variable with largest unknown set.
Definition: var.hpp:188
IntConLevel ann2icl(AST::Node *ann)
Convert ann to IntConLevel.
Definition: flatzinc.cpp:1935
void newSetVar(SetVarSpec *vs)
Create new set variable from specification.
Definition: flatzinc.cpp:762
IntAssign INT_ASSIGN_MIN(void)
Select smallest value.
Definition: assign.hpp:59
IntValBranch INT_VAL_RND(Rnd r)
Select random value.
Definition: val.hpp:83
virtual Choice * choice(const Space &, Archive &e)
Return choice.
Definition: flatzinc.cpp:177
Heap heap
The single global heap.
Definition: heap.cpp:49
std::vector< bool > iv_introduced
Indicates whether an integer variable is introduced by mzn2fzn.
Definition: flatzinc.hh:431
Gecode::IntSet d(v, 7)
TieBreak< IntVarBranch > bool_varsel
Definition: flatzinc.cpp:123
unsigned int id(void) const
Return brancher id.
Definition: core.hpp:3090
void newBoolVar(BoolVarSpec *vs)
Create new Boolean variable from specification.
Definition: flatzinc.cpp:750
Gecode::Support::Mutex mutex
A mutex for the random number generator.
Definition: flatzinc.hh:359
void update(Space &, bool share, VarArray< Var > &a)
Update array to be a clone of array a.
Definition: array.hpp:1072
const BoolInstr * bi[]
Definition: mm-bool.cpp:4169
bool alias
Whether the variable aliases another variable.
Definition: varspec.hh:63
SetVarBranch ann2svarsel(AST::Node *ann, Rnd rnd, double decay)
Definition: flatzinc.cpp:491
SetVar arg2SetVar(AST::Node *n)
Convert n to SetVar.
Definition: flatzinc.cpp:1866
int optVar(void) const
Return index of variable used for optimization.
Definition: flatzinc.cpp:1639
int getSetVar(void)
Cast this node to a set variable node.
Definition: ast.hh:438
double getFloat(void)
Cast this node to a Float node.
Definition: ast.hh:456
Gecode::FloatVal c(-8, 8)
void print(std::ostream &out, const Gecode::IntVarArray &iv, const Gecode::BoolVarArray &bv, const Gecode::SetVarArray &sv, const Gecode::FloatVarArray &fv) const
Definition: flatzinc.cpp:2169
void sort(TaskViewArray< TaskView > &t)
Sort task view array t according to sto and inc (increasing or decreasing)
Definition: sort.hpp:137
FloatVarBranch FLOAT_VAR_AFC_SIZE_MAX(double d, BranchTbl tbl)
Select variable with largest accumulated failure count divided by domain size with decay factor d...
Definition: var.hpp:214
int p
Number of positive literals for node type.
Definition: bool-expr.cpp:236
T * alloc(long unsigned int n)
Allocate block of n objects of type T from heap.
Definition: heap.hpp:400
IntVarBranch INT_VAR_AFC_MAX(double d, BranchTbl tbl)
Select variable with largest accumulated failure count with decay factor d.
Definition: var.hpp:162
Gecode::FloatVarArray fv
The float variables.
Definition: flatzinc.hh:450
const FloatNum min
Smallest allowed float value.
Definition: float.hh:833
Gecode::IntArgs i(4, 1, 2, 3, 4)
IntAssign ann2asnivalsel(AST::Node *ann, Rnd rnd)
Definition: flatzinc.cpp:472
Base-class for branchers.
Definition: core.hpp:1071
FloatNum n
The middle value for branching.
Definition: float.hh:1375
const Space * last(void) const
Return last solution found (possibly NULL)
Definition: core.hpp:2721
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:238
Equality ( )
Definition: int.hh:904
IntVarBranch INT_VAR_DEGREE_MAX(BranchTbl tbl)
Select variable with largest degree.
Definition: var.hpp:147
std::vector< bool > fv_introduced
Indicates whether a float variable is introduced by mzn2fzn.
Definition: flatzinc.hh:454
Argument array for non-primitive types.
Definition: array.hpp:727
Options opt
The options.
Definition: test.cpp:101
Option< std::pair< double, double > > domain
Definition: varspec.hh:125
IntVarBranch INT_VAR_ACTIVITY_MIN(double d, BranchTbl tbl)
Select variable with lowest activity with decay factor d.
Definition: var.hpp:172
void add(const BrancherHandle &bh, const string &rel0, const string &rel1, const vector< string > &n)
Add new brancher information.
Definition: flatzinc.cpp:249
int dfs(Space *root, const Gist::Options &opt)
Create a new stand-alone Gist for root.
Definition: gist.hpp:207
FloatVarBranch FLOAT_VAR_AFC_SIZE_MIN(double d, BranchTbl tbl)
Select variable with smalllest accumulated failure count divided by domain size with decay factor d...
Definition: var.hpp:204
IntAssign INT_ASSIGN_RND(Rnd r)
Select random value.
Definition: assign.hpp:74
Execution has resulted in failure.
Definition: core.hpp:525
Specification for Boolean variables.
Definition: varspec.hh:101
Value description class for branching.
Definition: float.hh:1372
Node representing an atom
Definition: ast.hh:294
A lock as a scoped frontend for a mutex.
Definition: thread.hpp:199
int _optVar
Index of the variable to optimize.
Definition: flatzinc.hh:389
virtual void archive(Archive &e) const
Archive into e.
Definition: flatzinc.cpp:115
int getIntVar(void)
Cast this node to an integer variable node.
Definition: ast.hh:420
void finalize(void)
Clean up when Gist exits.
Definition: gist.cpp:67
Output support class for FlatZinc interpreter.
Definition: flatzinc.hh:111
IntVar arg2IntVar(AST::Node *n)
Convert n to IntVar.
Definition: flatzinc.cpp:1834
Choice(const Brancher &b, bool fail0)
Initialize choice for brancher b.
Definition: flatzinc.cpp:108
static void installCtrlHandler(bool install, bool force=false)
Install handler for catching Ctrl-C.
Definition: script.hpp:120
static Search::Stop * create(unsigned int node, unsigned int fail, unsigned int time, bool intr)
Create appropriate stop-object.
Definition: script.hpp:94
IntAssign INT_ASSIGN_MAX(void)
Select largest value.
Definition: assign.hpp:69
SetVarBranch SET_VAR_ACTIVITY_MAX(double d, BranchTbl tbl)
Select variable with highest activity with decay factor d.
Definition: var.hpp:153
unsigned int operator()(unsigned int n)
Returns a random integer from the interval [0..n)
Definition: flatzinc.cpp:323
int getBoolVar(void)
Cast this node to a Boolean variable node.
Definition: ast.hh:426
The Gecode Interactive Search Tool.
bool isSet(void)
Test if node is a set literal node.
Definition: ast.hh:502
std::vector< int > s
Definition: ast.hh:179
void fail(void)
Fail space.
Definition: core.hpp:3428
FznRnd * _random
Random number generator.
Definition: flatzinc.hh:400
BoolVarArgs arg2boolvarargs(AST::Node *arg, int offset=0, int siv=-1)
Convert arg to BoolVarArgs.
Definition: flatzinc.cpp:1797
void print(const BrancherHandle &bh, int a, int i, int n, std::ostream &o) const
Output branch information.
Definition: flatzinc.cpp:292
IntValBranch INT_VAL_MIN(void)
Select smallest value.
Definition: val.hpp:68
virtual void archive(Archive &e) const
Archive into e.
Definition: core.cpp:670
unsigned int size(I &i)
Size of all ranges of range iterator i.
void newFloatVar(FloatVarSpec *vs)
Create new float variable from specification.
Definition: flatzinc.cpp:809
virtual ExecStatus commit(Space &, const Gecode::Choice &c, unsigned int)
Perform commit for choice c.
Definition: flatzinc.cpp:182
IntValBranch INT_VAL_SPLIT_MAX(void)
Select values greater than mean of smallest and largest value.
Definition: val.hpp:93
IntVarBranch INT_VAR_MAX_MAX(BranchTbl tbl)
Select variable with largest max.
Definition: var.hpp:207
void shrinkElement(AST::Node *node, std::map< int, int > &iv, std::map< int, int > &bv, std::map< int, int > &sv, std::map< int, int > &fv)
Definition: flatzinc.cpp:2267
bool l
Whether to try the lower or upper half first.
Definition: float.hh:1377
bool optVarIsInt(void) const
Return whether variable used for optimization is integer (or float)
Definition: flatzinc.cpp:1644
IntVarBranch INT_VAR_RND(Rnd r)
Select random variable (uniform distribution, for tie breaking)
Definition: var.hpp:113
IntVarBranch INT_VAR_AFC_MIN(double d, BranchTbl tbl)
Select variable with smallest accumulated failure count with decay factor d.
Definition: var.hpp:152
SetValBranch SET_VAL_MAX_EXC(void)
Exclude largest element.
Definition: val.hpp:84
IntVarBranch INT_VAR_ACTIVITY_SIZE_MAX(double d, BranchTbl tbl)
Select variable with largest activity divided by domain size with decay factor d. ...
Definition: var.hpp:262
Gecode::BoolVarArray bv_aux
The introduced Boolean variables.
Definition: flatzinc.hh:437
bool clone
Whether engines create a clone when being initialized.
Definition: search.hh:207
FznRnd(unsigned int s=1)
Constructor.
Definition: flatzinc.cpp:320
Array * getArgs(unsigned int n)
Definition: ast.hh:269
void print(std::ostream &out, const Printer &p) const
Produce output on out using p.
Definition: flatzinc.cpp:1649
SetValBranch SET_VAL_MAX_INC(void)
Include largest element.
Definition: val.hpp:79
SetVarBranch SET_VAR_MAX_MAX(BranchTbl tbl)
Select variable with largest maximum unknown element.
Definition: var.hpp:178
struct Gecode::Space::@52::@53 p
Data only available during propagation.
FloatValBranch FLOAT_VAL_SPLIT_MIN(void)
Select values not greater than mean of smallest and largest value.
Definition: val.hpp:59
bool funcDep
Whether the variable functionally depends on another variable.
Definition: varspec.hh:69
Less ( )
Definition: int.hh:907
Integer sets.
Definition: int.hh:171
Float variable node.
Definition: ast.hh:218
virtual void compare(const Space &s0, const Space &s1)=0
Call-back function.
Set variable node
Definition: ast.hh:226
Choice that only signals failure or success
Definition: flatzinc.cpp:103
SetVarBranch SET_VAR_AFC_SIZE_MIN(double d, BranchTbl tbl)
Select variable with smallest accumulated failure count divided by domain size with decay factor d...
Definition: var.hpp:203
A simple comparator.
Definition: gist.hh:215
Option< AST::SetLit * > domain
Definition: varspec.hh:103
FlatZincSpace(bool share, FlatZincSpace &)
Copy constructor.
Definition: flatzinc.cpp:623
FloatVarBranch FLOAT_VAR_MAX_MAX(BranchTbl tbl)
Select variable with largest max.
Definition: var.hpp:179
IntVarArgs arg2intvarargs(AST::Node *arg, int offset=0)
Convert arg to IntVarArgs.
Definition: flatzinc.cpp:1776
virtual void constrain(const Space &s)
Implement optimization.
Definition: flatzinc.cpp:1594
unsigned long int restart(void) const
Return number of restarts.
Definition: core.hpp:2709
bool isIntVar(void)
Test if node is an integer variable node.
Definition: ast.hh:474
FloatVarBranch FLOAT_VAR_RND(Rnd r)
Select random variable (uniform distribution, for tie breaking)
Definition: var.hpp:109
unsigned int size(void) const
Return size (cardinality) of set.
Definition: int-set-1.hpp:161
Passing integer variables.
Definition: int.hh:636
bool isBoolArray(AST::Node *b, int &singleInt)
Check if b is array of Booleans (or has a single integer)
Definition: flatzinc.cpp:1844
virtual void print(const Space &, const Gecode::Choice &c, unsigned int, std::ostream &o) const
Print explanation.
Definition: flatzinc.cpp:186
std::vector< bool > bv_introduced
Indicates whether a Boolean variable is introduced by mzn2fzn.
Definition: flatzinc.hh:439
bool done
Flag whether brancher is done.
Definition: flatzinc.cpp:71
Passing integer arguments.
Definition: int.hh:607
Passing Boolean variables.
Definition: int.hh:690
struct Gecode::Space::@52::@54 c
Data available only during copying.
static const IntSet empty
Empty set.
Definition: int.hh:262
IntVarBranch INT_VAR_AFC_SIZE_MIN(double d, BranchTbl tbl)
Select variable with smallest accumulated failure count divided by domain size with decay factor d...
Definition: var.hpp:232
bool isInt(int &i)
Test if node is int, if yes set i to the value.
Definition: ast.hh:368
bool _optVarIsInt
Whether variable to optimize is integer (or float)
Definition: flatzinc.hh:391
IntSet arg2intset(AST::Node *n)
Convert n to IntSet.
Definition: flatzinc.cpp:1746
Gecode::FloatVarArray fv_aux
The introduced float variables.
Definition: flatzinc.hh:452
SetValBranch SET_VAL_MIN_EXC(void)
Exclude smallest element.
Definition: val.hpp:64
Boolean variable array.
Definition: int.hh:786
Greater ( )
Definition: float.hh:1060
SetVarBranch SET_VAR_AFC_SIZE_MAX(double d, BranchTbl tbl)
Select variable with largest accumulated failure count divided by domain size with decay factor d...
Definition: var.hpp:213
Boolean integer variables.
Definition: int.hh:491
bool isString(void)
Test if node is a string node.
Definition: ast.hh:506
const int v[7]
Definition: distinct.cpp:207
void min(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:75
BrancherHandle bh
bool assigned
Whether the variable is assigned.
Definition: varspec.hh:65
AuxVarBrancher(Home home, TieBreak< IntVarBranch > int_varsel0, IntValBranch int_valsel0, TieBreak< IntVarBranch > bool_varsel0, IntValBranch bool_valsel0, SetVarBranch set_varsel0, SetValBranch set_valsel0, TieBreak< FloatVarBranch > float_varsel0, FloatValBranch float_valsel0)
Construct brancher.
Definition: flatzinc.cpp:73
void update(Space &home, bool share, SharedHandle &sh)
Updating during cloning.
Definition: core.hpp:2656
IntValBranch INT_VAL_MAX(void)
Select largest value.
Definition: val.hpp:78
int getInt(void)
Cast this node to an integer node.
Definition: ast.hh:444
void print(std::basic_ostream< Char, Traits > &s, bool assigned, IL &lb, IU &ub, unsigned int cardMin, unsigned int cardMax)
Print set view.
Definition: print.hpp:67
Integer variable node.
Definition: ast.hh:210
Passing set variables.
Definition: set.hh:490
virtual size_t size(void) const
Report size occupied.
Definition: flatzinc.cpp:111
Exception: Base-class for exceptions
Definition: exception.hpp:46
Print statistics for script.
Definition: driver.hh:101
SetVarBranch SET_VAR_RND(Rnd r)
Select random variable (uniform distribution, for tie breaking)
Definition: var.hpp:96
Base class for variables.
Definition: var.hpp:44
IntValBranch INT_VALUES_MIN(void)
Try all values starting from smallest.
Definition: val.hpp:120
void free(T *b, long unsigned int n)
Delete n objects starting at b.
Definition: heap.hpp:426
BrancherHandle assign(Home home, const FloatVarArgs &x, FloatAssign fa, FloatBranchFilter bf, FloatVarValPrint vvp)
Assign all x with value selection vals.
Definition: branch.cpp:113
virtual void print(std::ostream &)=0
Output string representation.
BranchInformation(void)
Constructor.
Definition: flatzinc.cpp:272
Exception signaling type error
Definition: ast.hh:59
Node * x
Pointer to corresponding Boolean expression node.
Definition: bool-expr.cpp:253
FloatVarBranch FLOAT_VAR_MIN_MIN(BranchTbl tbl)
Select variable with smallest min.
Definition: var.hpp:164
Set variables
Definition: set.hh:129
Choice for performing commit
Definition: core.hpp:1036
bool hasAtom(const std::string &id)
Test if node has atom with id.
Definition: ast.hh:325
SharedHandle::Object * object(void) const
Access to the shared object.
Definition: core.hpp:2619
bool isFloatVar(void)
Test if node is a float variable node.
Definition: ast.hh:486
Archive representation
Definition: archive.hpp:45
int i
Variable index.
Definition: varspec.hh:61
Set literal node
Definition: ast.hh:175
void init(void)
Initialise for use.
Definition: flatzinc.cpp:279
ExecStatus
Definition: core.hpp:523
Integer variables.
Definition: int.hh:350
Which values to select for assignment.
Definition: int.hh:4081
void rel(Home home, FloatVar x0, FloatRelType frt, FloatVal n)
Propagates .
Definition: rel.cpp:47
Exception class for FlatZinc errors
Definition: flatzinc.hh:591
Specification for floating point variables.
Definition: varspec.hh:123
TieBreak< FloatVarBranch > ann2fvarsel(AST::Node *ann, Rnd rnd, double decay)
Definition: flatzinc.cpp:559
IntVarBranch INT_VAR_AFC_SIZE_MAX(double d, BranchTbl tbl)
Select variable with largest accumulated failure count divided by domain size with decay factor d...
Definition: var.hpp:242
void flattenAnnotations(AST::Array *ann, std::vector< AST::Node * > &out)
Definition: flatzinc.cpp:864
The default consistency for a constraint.
Definition: int.hh:941
int bab(Space *root, const Gist::Options &opt)
Create a new stand-alone Gist for branch-and-bound search of root.
Definition: gist.hpp:212
AST::Array * _solveAnnotations
Annotations on the solve item.
Definition: flatzinc.hh:403
IntValBranch INT_VAL_MED(void)
Select greatest value not greater than the median.
Definition: val.hpp:73
IntVarBranch INT_VAR_ACTIVITY_SIZE_MIN(double d, BranchTbl tbl)
Select variable with smallest activity divided by domain size with decay factor d.
Definition: var.hpp:252
~FlatZincSpace(void)
Destructor.
Definition: flatzinc.cpp:1335
An window for simple text output.
Definition: gist.hh:164
Run script in Gist.
Definition: driver.hh:102
bool needAuxVars
Whether the introduced variables still need to be copied.
Definition: flatzinc.hh:457
void print(const BrancherHandle &bh, int a, int i, int n, ostream &o) const
Output branch information.
Definition: flatzinc.cpp:257
virtual bool status(const Space &_home) const
Check status of brancher, return true if alternatives left.
Definition: flatzinc.cpp:136
void solve(AST::Array *annotation)
Post the solve item.
Definition: flatzinc.cpp:1314
The shared object.
Definition: core.hpp:88
Execution is okay.
Definition: core.hpp:527
unsigned long int restart
Number of restarts.
Definition: search.hh:145
#define GECODE_HAS_FLOAT_VARS
Definition: config.hpp:57
void varValPrint(const Space &home, const BrancherHandle &bh, unsigned int a, Var, int i, const int &n, std::ostream &o)
Definition: flatzinc.cpp:304
TieBreak< FloatVarBranch > float_varsel
Definition: flatzinc.cpp:130
bool isArray(void)
Test if node is an array node.
Definition: ast.hh:510
Float variables.
Definition: float.hh:857
virtual Actor * copy(Space &home, bool share)
Copy brancher.
Definition: flatzinc.cpp:194
void aliasBool2Int(int iv, int bv)
Link integer variable iv to Boolean variable bv.
Definition: flatzinc.cpp:741
A space that can be initialized with a FlatZinc model.
Definition: flatzinc.hh:371
Gecode::IntVarArray iv_aux
The introduced integer variables.
Definition: flatzinc.hh:425
Set variable array
Definition: set.hh:571
void shrinkArrays(Space &home, int &optVar, bool optVarIsInt, Gecode::IntVarArray &iv, Gecode::BoolVarArray &bv, Gecode::SetVarArray &sv, Gecode::FloatVarArray &fv)
Definition: flatzinc.cpp:2302
CompareStatus compare(I &i, J &j)
Check whether range iterator i is a subset of j, or whether they are disjoint.
Bounds propagation or consistency.
Definition: int.hh:939
Stop * stop
Stop object for stopping search.
Definition: search.hh:217
class Gecode::Gist::Options::_I inspect
IntValBranch INT_VAL_SPLIT_MIN(void)
Select values not greater than mean of smallest and largest value.
Definition: val.hpp:88
int explore(Space *root, bool bab, const Options &opt)
Create a new stand-alone Gist for root using bab.
Definition: gist.cpp:105
struct Gecode::@518::NNF::@57::@58 b
For binary nodes (and, or, eqv)
void run(std::ostream &out, const Printer &p, const FlatZincOptions &opt, Gecode::Support::Timer &t_total)
Run the search.
Definition: flatzinc.cpp:1580
Gecode toplevel namespace
int * iv_boolalias
Indicates whether an integer variable aliases a Boolean variable.
Definition: flatzinc.hh:433
unsigned long int node
Number of nodes expanded.
Definition: search.hh:141
void maximize(int var, bool isInt, AST::Array *annotation)
Post that integer variable var should be maximized.
Definition: flatzinc.cpp:1328
int setVarCount
Number of set variables.
Definition: flatzinc.hh:386
Node representing a function call
Definition: ast.hh:259
int intVarCount
Number of integer variables.
Definition: flatzinc.hh:380
IntValBranch ann2ivalsel(AST::Node *ann, std::string &r0, std::string &r1, Rnd rnd)
Definition: flatzinc.cpp:421
SetVarArgs arg2setvarargs(AST::Node *arg, int offset=0, int doffset=0, const IntSet &od=IntSet::empty)
Convert n to SetVarArgs.
Definition: flatzinc.cpp:1877
A node in a FlatZinc abstract syntax tree.
Definition: ast.hh:71
virtual bool slave(const CRI &cri)
Slave configuration function for restart meta search engine.
Definition: flatzinc.cpp:1615
SetVarBranch SET_VAR_ACTIVITY_SIZE_MAX(double d, BranchTbl tbl)
Select variable with largest activity divided by domain size with decay factor d. ...
Definition: var.hpp:233
bool assigned(void) const
Test if all variables are assigned.
Definition: array.hpp:1085
IntArgs arg2boolargs(AST::Node *arg, int offset=0)
Convert arg (array of Booleans) to IntArgs.
Definition: flatzinc.cpp:1736
BrancherHandle branch(Home home, const FloatVarArgs &x, FloatVarBranch vars, FloatValBranch vals, FloatBranchFilter bf, FloatVarValPrint vvp)
Branch over x with variable selection vars and value selection vals.
Definition: branch.cpp:43
Which variable to select for branching.
Definition: set.hh:1253
Random number generator.
Definition: rnd.hpp:46
FloatVarBranch FLOAT_VAR_ACTIVITY_MIN(double d, BranchTbl tbl)
Select variable with lowest activity with decay factor d.
Definition: var.hpp:144
SetVarBranch SET_VAR_MIN_MIN(BranchTbl tbl)
Select variable with smallest minimum unknown element.
Definition: var.hpp:163
FloatVarBranch FLOAT_VAR_ACTIVITY_SIZE_MIN(double d, BranchTbl tbl)
Select variable with smallest activity divided by domain size with decay factor d.
Definition: var.hpp:224
Space is failed
Definition: core.hpp:1301
unsigned int _lns
Percentage of variables to keep in LNS (or 0 for no LNS)
Definition: flatzinc.hh:397
FloatVarBranch FLOAT_VAR_SIZE_MAX(BranchTbl tbl)
Select variable with largest domain size.
Definition: var.hpp:189
Gecode::SetVarArray sv
The set variables.
Definition: flatzinc.hh:442
Home class for posting propagators
Definition: core.hpp:717
Options for Gist
Definition: gist.hh:238
int size(void) const
Return size of array (number of elements)
Definition: array.hpp:985
double FloatNum
Floating point number base type.
Definition: float.hh:108
Specification for integer variables.
Definition: varspec.hh:76
void compare(Comparator *c)
Add comparator.
Definition: gist.hpp:186
SetVarBranch SET_VAR_AFC_MAX(double d, BranchTbl tbl)
Select variable with largest accumulated failure count with decay factor d.
Definition: var.hpp:133
bool introduced
Whether the variable was introduced in the mzn2fzn translation.
Definition: varspec.hh:67
std::string getString(void)
Cast this node to a string node.
Definition: ast.hh:468
struct Gecode::@518::NNF::@57::@59 a
For atomic nodes.
FloatVarBranch FLOAT_VAR_AFC_MAX(double d, BranchTbl tbl)
Select variable with largest accumulated failure count with decay factor d.
Definition: var.hpp:134
Gecode::IntVarArray iv_lns
The integer variables used in LNS.
Definition: flatzinc.hh:428
FloatVar arg2FloatVar(AST::Node *n)
Convert n to FloatVar.
Definition: flatzinc.cpp:1924
Domain propagation or consistency.
Definition: int.hh:940
Depth-first search engine.
Definition: search.hh:494
Branching on the introduced variables.
Definition: flatzinc.cpp:68
IntVarBranch INT_VAR_SIZE_MAX(BranchTbl tbl)
Select variable with largest domain size.
Definition: var.hpp:217
Meth method(void) const
Return whether to solve a satisfaction or optimization problem.
Definition: flatzinc.cpp:1634
void add(const BrancherHandle &bh, const std::string &rel0, const std::string &rel1, const std::vector< std::string > &n)
Add new brancher information.
Definition: flatzinc.cpp:285
Registry & registry(void)
Return global registry object.
Definition: registry.cpp:57
FloatValArgs arg2floatargs(AST::Node *arg, int offset=0)
Convert n to FloatValArgs.
Definition: flatzinc.cpp:1893
Option< AST::SetLit * > upperBound
Definition: varspec.hh:145
virtual size_t dispose(Space &)
Delete brancher and return its size.
Definition: flatzinc.cpp:225
AST::Array * solveAnnotations(void) const
Return the solve item annotations.
Definition: flatzinc.cpp:1309
bool fail
Whether brancher should fail.
Definition: flatzinc.cpp:106
TieBreak< IntVarBranch > int_varsel
Definition: flatzinc.cpp:121
FloatVarBranch FLOAT_VAR_SIZE_MIN(BranchTbl tbl)
Select variable with smallest domain size.
Definition: var.hpp:184
void init(AST::Array *output)
Definition: flatzinc.cpp:1952
BoolVar arg2BoolVar(AST::Node *n)
Convert n to BoolVar.
Definition: flatzinc.cpp:1823
IntSetArgs arg2intsetargs(AST::Node *arg, int offset=0)
Convert arg to IntSetArgs.
Definition: flatzinc.cpp:1761
Abstract representation of a constraint.
Definition: conexpr.hh:47