Generated on Tue Sep 16 2014 20:36:42 for Gecode by doxygen 1.8.8
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: 2013-08-29 02:46:26 +0200 (Thu, 29 Aug 2013) $ by $Author: tack $
15  * $Revision: 13990 $
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() == false);
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 
321  if (vs->assigned) {
322  return IntSet(vs->i,vs->i);
323  }
324  if (vs->domain()) {
325  AST::SetLit* sl = vs->domain.some();
326  if (sl->interval) {
327  return IntSet(sl->min, sl->max);
328  } else {
329  int* newdom = heap.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
330  for (int i=sl->s.size(); i--;)
331  newdom[i] = sl->s[i];
332  IntSet ret(newdom, sl->s.size());
333  heap.free(newdom, static_cast<unsigned long int>(sl->s.size()));
334  return ret;
335  }
336  }
338  }
339 
340  int vs2bsl(BoolVarSpec* bs) {
341  if (bs->assigned) {
342  return bs->i;
343  }
344  if (bs->domain()) {
345  AST::SetLit* sl = bs->domain.some();
346  assert(sl->interval);
347  return std::min(1, std::max(0, sl->min));
348  }
349  return 0;
350  }
351 
352  int vs2bsh(BoolVarSpec* bs) {
353  if (bs->assigned) {
354  return bs->i;
355  }
356  if (bs->domain()) {
357  AST::SetLit* sl = bs->domain.some();
358  assert(sl->interval);
359  return std::max(0, std::min(1, sl->max));
360  }
361  return 1;
362  }
363 
364  TieBreak<IntVarBranch> ann2ivarsel(AST::Node* ann, Rnd rnd, double decay) {
365  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
366  if (s->id == "input_order")
368  if (s->id == "first_fail")
370  if (s->id == "anti_first_fail")
372  if (s->id == "smallest")
374  if (s->id == "largest")
376  if (s->id == "occurrence")
378  if (s->id == "max_regret")
380  if (s->id == "most_constrained")
383  if (s->id == "random") {
384  return TieBreak<IntVarBranch>(INT_VAR_RND(rnd));
385  }
386  if (s->id == "afc_min")
388  if (s->id == "afc_max")
390  if (s->id == "afc_size_min")
392  if (s->id == "afc_size_max") {
394  }
395  if (s->id == "activity_min")
397  if (s->id == "activity_max")
399  if (s->id == "activity_size_min")
401  if (s->id == "activity_size_max")
403  }
404  std::cerr << "Warning, ignored search annotation: ";
405  ann->print(std::cerr);
406  std::cerr << std::endl;
408  }
409 
410  IntValBranch ann2ivalsel(AST::Node* ann, std::string& r0, std::string& r1,
411  Rnd rnd) {
412  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
413  if (s->id == "indomain_min") {
414  r0 = "="; r1 = "!=";
415  return INT_VAL_MIN();
416  }
417  if (s->id == "indomain_max") {
418  r0 = "="; r1 = "!=";
419  return INT_VAL_MAX();
420  }
421  if (s->id == "indomain_median") {
422  r0 = "="; r1 = "!=";
423  return INT_VAL_MED();
424  }
425  if (s->id == "indomain_split") {
426  r0 = "<="; r1 = ">";
427  return INT_VAL_SPLIT_MIN();
428  }
429  if (s->id == "indomain_reverse_split") {
430  r0 = ">"; r1 = "<=";
431  return INT_VAL_SPLIT_MAX();
432  }
433  if (s->id == "indomain_random") {
434  r0 = "="; r1 = "!=";
435  return INT_VAL_RND(rnd);
436  }
437  if (s->id == "indomain") {
438  r0 = "="; r1 = "=";
439  return INT_VALUES_MIN();
440  }
441  if (s->id == "indomain_middle") {
442  std::cerr << "Warning, replacing unsupported annotation "
443  << "indomain_middle with indomain_median" << std::endl;
444  r0 = "="; r1 = "!=";
445  return INT_VAL_MED();
446  }
447  if (s->id == "indomain_interval") {
448  std::cerr << "Warning, replacing unsupported annotation "
449  << "indomain_interval with indomain_split" << std::endl;
450  r0 = "<="; r1 = ">";
451  return INT_VAL_SPLIT_MIN();
452  }
453  }
454  std::cerr << "Warning, ignored search annotation: ";
455  ann->print(std::cerr);
456  std::cerr << std::endl;
457  r0 = "="; r1 = "!=";
458  return INT_VAL_MIN();
459  }
460 
462  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
463  if (s->id == "indomain_min")
464  return INT_ASSIGN_MIN();
465  if (s->id == "indomain_max")
466  return INT_ASSIGN_MAX();
467  if (s->id == "indomain_median")
468  return INT_ASSIGN_MED();
469  if (s->id == "indomain_random") {
470  return INT_ASSIGN_RND(rnd);
471  }
472  }
473  std::cerr << "Warning, ignored search annotation: ";
474  ann->print(std::cerr);
475  std::cerr << std::endl;
476  return INT_ASSIGN_MIN();
477  }
478 
479 #ifdef GECODE_HAS_SET_VARS
480  SetVarBranch ann2svarsel(AST::Node* ann, Rnd rnd, double decay) {
481  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
482  if (s->id == "input_order")
483  return SET_VAR_NONE();
484  if (s->id == "first_fail")
485  return SET_VAR_SIZE_MIN();
486  if (s->id == "anti_first_fail")
487  return SET_VAR_SIZE_MAX();
488  if (s->id == "smallest")
489  return SET_VAR_MIN_MIN();
490  if (s->id == "largest")
491  return SET_VAR_MAX_MAX();
492  if (s->id == "afc_min")
493  return SET_VAR_AFC_MIN(decay);
494  if (s->id == "afc_max")
495  return SET_VAR_AFC_MAX(decay);
496  if (s->id == "afc_size_min")
497  return SET_VAR_AFC_SIZE_MIN(decay);
498  if (s->id == "afc_size_max")
499  return SET_VAR_AFC_SIZE_MAX(decay);
500  if (s->id == "activity_min")
501  return SET_VAR_ACTIVITY_MIN(decay);
502  if (s->id == "activity_max")
503  return SET_VAR_ACTIVITY_MAX(decay);
504  if (s->id == "activity_size_min")
505  return SET_VAR_ACTIVITY_SIZE_MIN(decay);
506  if (s->id == "activity_size_max")
507  return SET_VAR_ACTIVITY_SIZE_MAX(decay);
508  if (s->id == "random") {
509  return SET_VAR_RND(rnd);
510  }
511  }
512  std::cerr << "Warning, ignored search annotation: ";
513  ann->print(std::cerr);
514  std::cerr << std::endl;
515  return SET_VAR_NONE();
516  }
517 
518  SetValBranch ann2svalsel(AST::Node* ann, std::string r0, std::string r1,
519  Rnd rnd) {
520  (void) rnd;
521  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
522  if (s->id == "indomain_min") {
523  r0 = "in"; r1 = "not in";
524  return SET_VAL_MIN_INC();
525  }
526  if (s->id == "indomain_max") {
527  r0 = "in"; r1 = "not in";
528  return SET_VAL_MAX_INC();
529  }
530  if (s->id == "outdomain_min") {
531  r1 = "in"; r0 = "not in";
532  return SET_VAL_MIN_EXC();
533  }
534  if (s->id == "outdomain_max") {
535  r1 = "in"; r0 = "not in";
536  return SET_VAL_MAX_EXC();
537  }
538  }
539  std::cerr << "Warning, ignored search annotation: ";
540  ann->print(std::cerr);
541  std::cerr << std::endl;
542  r0 = "in"; r1 = "not in";
543  return SET_VAL_MIN_INC();
544  }
545 #endif
546 
547 #ifdef GECODE_HAS_FLOAT_VARS
549  double decay) {
550  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
551  if (s->id == "input_order")
553  if (s->id == "first_fail")
555  if (s->id == "anti_first_fail")
557  if (s->id == "smallest")
559  if (s->id == "largest")
561  if (s->id == "occurrence")
563  if (s->id == "most_constrained")
566  if (s->id == "random") {
568  }
569  if (s->id == "afc_min")
571  if (s->id == "afc_max")
573  if (s->id == "afc_size_min")
575  if (s->id == "afc_size_max")
577  if (s->id == "activity_min")
579  if (s->id == "activity_max")
581  if (s->id == "activity_size_min")
583  if (s->id == "activity_size_max")
585  }
586  std::cerr << "Warning, ignored search annotation: ";
587  ann->print(std::cerr);
588  std::cerr << std::endl;
590  }
591 
592  FloatValBranch ann2fvalsel(AST::Node* ann, std::string r0, std::string r1) {
593  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
594  if (s->id == "indomain_split") {
595  r0 = "<="; r1 = ">";
596  return FLOAT_VAL_SPLIT_MIN();
597  }
598  if (s->id == "indomain_reverse_split") {
599  r1 = "<="; r0 = ">";
600  return FLOAT_VAL_SPLIT_MAX();
601  }
602  }
603  std::cerr << "Warning, ignored search annotation: ";
604  ann->print(std::cerr);
605  std::cerr << std::endl;
606  r0 = "<="; r1 = ">";
607  return FLOAT_VAL_SPLIT_MIN();
608  }
609 
610 #endif
611 
613  : Space(share, f), _solveAnnotations(NULL), iv_boolalias(NULL),
614  needAuxVars(f.needAuxVars) {
615  _optVar = f._optVar;
617  _method = f._method;
618  branchInfo.update(*this, share, f.branchInfo);
619  iv.update(*this, share, f.iv);
621 
622  if (needAuxVars) {
623  IntVarArgs iva;
624  for (int i=0; i<f.iv_aux.size(); i++) {
625  if (!f.iv_aux[i].assigned()) {
626  iva << IntVar();
627  iva[iva.size()-1].update(*this, share, f.iv_aux[i]);
628  }
629  }
630  iv_aux = IntVarArray(*this, iva);
631  }
632 
633  bv.update(*this, share, f.bv);
635  if (needAuxVars) {
636  BoolVarArgs bva;
637  for (int i=0; i<f.bv_aux.size(); i++) {
638  if (!f.bv_aux[i].assigned()) {
639  bva << BoolVar();
640  bva[bva.size()-1].update(*this, share, f.bv_aux[i]);
641  }
642  }
643  bv_aux = BoolVarArray(*this, bva);
644  }
645 
646 #ifdef GECODE_HAS_SET_VARS
647  sv.update(*this, share, f.sv);
649  if (needAuxVars) {
650  SetVarArgs sva;
651  for (int i=0; i<f.sv_aux.size(); i++) {
652  if (!f.sv_aux[i].assigned()) {
653  sva << SetVar();
654  sva[sva.size()-1].update(*this, share, f.sv_aux[i]);
655  }
656  }
657  sv_aux = SetVarArray(*this, sva);
658  }
659 #endif
660 #ifdef GECODE_HAS_FLOAT_VARS
661  fv.update(*this, share, f.fv);
663  if (needAuxVars) {
664  FloatVarArgs fva;
665  for (int i=0; i<f.fv_aux.size(); i++) {
666  if (!f.fv_aux[i].assigned()) {
667  fva << FloatVar();
668  fva[fva.size()-1].update(*this, share, f.fv_aux[i]);
669  }
670  }
671  fv_aux = FloatVarArray(*this, fva);
672  }
673 #endif
674  }
675 
677  : intVarCount(-1), boolVarCount(-1), floatVarCount(-1), setVarCount(-1),
678  _optVar(-1), _optVarIsInt(true),
679  _solveAnnotations(NULL), needAuxVars(true) {
680  branchInfo.init();
681  }
682 
683  void
684  FlatZincSpace::init(int intVars, int boolVars,
685  int setVars, int floatVars) {
686  (void) setVars;
687  (void) floatVars;
688 
689  intVarCount = 0;
690  iv = IntVarArray(*this, intVars);
691  iv_introduced = std::vector<bool>(2*intVars);
692  iv_boolalias = alloc<int>(intVars+(intVars==0?1:0));
693  boolVarCount = 0;
694  bv = BoolVarArray(*this, boolVars);
695  bv_introduced = std::vector<bool>(2*boolVars);
696 #ifdef GECODE_HAS_SET_VARS
697  setVarCount = 0;
698  sv = SetVarArray(*this, setVars);
699  sv_introduced = std::vector<bool>(2*setVars);
700 #endif
701 #ifdef GECODE_HAS_FLOAT_VARS
702  floatVarCount = 0;
703  fv = FloatVarArray(*this, floatVars);
704  fv_introduced = std::vector<bool>(2*floatVars);
705 #endif
706  }
707 
708  void
710  if (vs->alias) {
711  iv[intVarCount++] = iv[vs->i];
712  } else {
713  IntSet dom(vs2is(vs));
714  if (dom.size()==0) {
715  fail();
716  return;
717  } else {
718  iv[intVarCount++] = IntVar(*this, dom);
719  }
720  }
721  iv_introduced[2*(intVarCount-1)] = vs->introduced;
722  iv_introduced[2*(intVarCount-1)+1] = vs->funcDep;
723  iv_boolalias[intVarCount-1] = -1;
724  }
725 
726  void
728  iv_boolalias[iv] = bv;
729  }
730  int
732  return iv_boolalias[iv];
733  }
734 
735  void
737  if (vs->alias) {
738  bv[boolVarCount++] = bv[vs->i];
739  } else {
740  bv[boolVarCount++] = BoolVar(*this, vs2bsl(vs), vs2bsh(vs));
741  }
743  bv_introduced[2*(boolVarCount-1)+1] = vs->funcDep;
744  }
745 
746 #ifdef GECODE_HAS_SET_VARS
747  void
749  if (vs->alias) {
750  sv[setVarCount++] = sv[vs->i];
751  } else if (vs->assigned) {
752  assert(vs->upperBound());
753  AST::SetLit* vsv = vs->upperBound.some();
754  if (vsv->interval) {
755  IntSet d(vsv->min, vsv->max);
756  sv[setVarCount++] = SetVar(*this, d, d);
757  } else {
758  int* is = heap.alloc<int>(static_cast<unsigned long int>(vsv->s.size()));
759  for (int i=vsv->s.size(); i--; )
760  is[i] = vsv->s[i];
761  IntSet d(is, vsv->s.size());
762  heap.free(is,static_cast<unsigned long int>(vsv->s.size()));
763  sv[setVarCount++] = SetVar(*this, d, d);
764  }
765  } else if (vs->upperBound()) {
766  AST::SetLit* vsv = vs->upperBound.some();
767  if (vsv->interval) {
768  IntSet d(vsv->min, vsv->max);
769  sv[setVarCount++] = SetVar(*this, IntSet::empty, d);
770  } else {
771  int* is = heap.alloc<int>(static_cast<unsigned long int>(vsv->s.size()));
772  for (int i=vsv->s.size(); i--; )
773  is[i] = vsv->s[i];
774  IntSet d(is, vsv->s.size());
775  heap.free(is,static_cast<unsigned long int>(vsv->s.size()));
776  sv[setVarCount++] = SetVar(*this, IntSet::empty, d);
777  }
778  } else {
779  sv[setVarCount++] = SetVar(*this, IntSet::empty,
782  }
783  sv_introduced[2*(setVarCount-1)] = vs->introduced;
784  sv_introduced[2*(setVarCount-1)+1] = vs->funcDep;
785  }
786 #else
787  void
789  throw FlatZinc::Error("Gecode", "set variables not supported");
790  }
791 #endif
792 
793 #ifdef GECODE_HAS_FLOAT_VARS
794  void
796  if (vs->alias) {
797  fv[floatVarCount++] = fv[vs->i];
798  } else {
799  double dmin, dmax;
800  if (vs->domain()) {
801  dmin = vs->domain.some().first;
802  dmax = vs->domain.some().second;
803  if (dmin > dmax) {
804  fail();
805  return;
806  }
807  } else {
808  dmin = Float::Limits::min;
809  dmax = Float::Limits::max;
810  }
811  fv[floatVarCount++] = FloatVar(*this, dmin, dmax);
812  }
814  fv_introduced[2*(floatVarCount-1)+1] = vs->funcDep;
815  }
816 #else
817  void
819  throw FlatZinc::Error("Gecode", "float variables not supported");
820  }
821 #endif
822 
823  void
825  try {
826  registry().post(*this, ce, ann);
827  } catch (Gecode::Exception& e) {
828  throw FlatZinc::Error("Gecode", e.what());
829  } catch (AST::TypeError& e) {
830  throw FlatZinc::Error("Type error", e.what());
831  }
832  }
833 
834  void flattenAnnotations(AST::Array* ann, std::vector<AST::Node*>& out) {
835  for (unsigned int i=0; i<ann->a.size(); i++) {
836  if (ann->a[i]->isCall("seq_search")) {
837  AST::Call* c = ann->a[i]->getCall();
838  if (c->args->isArray())
839  flattenAnnotations(c->args->getArray(), out);
840  else
841  out.push_back(c->args);
842  } else {
843  out.push_back(ann->a[i]);
844  }
845  }
846  }
847 
848  void
849  FlatZincSpace::createBranchers(AST::Node* ann, int seed, double decay,
850  bool ignoreUnknown,
851  std::ostream& err) {
852  Rnd rnd(static_cast<unsigned int>(seed));
853  TieBreak<IntVarBranch> def_int_varsel = INT_VAR_AFC_SIZE_MAX(0.99);
854  IntValBranch def_int_valsel = INT_VAL_MIN();
855  TieBreak<IntVarBranch> def_bool_varsel = INT_VAR_AFC_MAX(0.99);
856  IntValBranch def_bool_valsel = INT_VAL_MIN();
857 #ifdef GECODE_HAS_SET_VARS
858  SetVarBranch def_set_varsel = SET_VAR_AFC_SIZE_MAX(0.99);
859  SetValBranch def_set_valsel = SET_VAL_MIN_INC();
860 #endif
861 #ifdef GECODE_HAS_FLOAT_VARS
862  TieBreak<FloatVarBranch> def_float_varsel = FLOAT_VAR_SIZE_MIN();
863  FloatValBranch def_float_valsel = FLOAT_VAL_SPLIT_MIN();
864 #endif
865 
866  std::vector<bool> iv_searched(iv.size());
867  for (unsigned int i=iv.size(); i--;)
868  iv_searched[i] = false;
869  std::vector<bool> bv_searched(bv.size());
870  for (unsigned int i=bv.size(); i--;)
871  bv_searched[i] = false;
872 #ifdef GECODE_HAS_SET_VARS
873  std::vector<bool> sv_searched(sv.size());
874  for (unsigned int i=sv.size(); i--;)
875  sv_searched[i] = false;
876 #endif
877 #ifdef GECODE_HAS_FLOAT_VARS
878  std::vector<bool> fv_searched(fv.size());
879  for (unsigned int i=fv.size(); i--;)
880  fv_searched[i] = false;
881 #endif
882 
883  if (ann) {
884  std::vector<AST::Node*> flatAnn;
885  if (ann->isArray()) {
886  flattenAnnotations(ann->getArray() , flatAnn);
887  } else {
888  flatAnn.push_back(ann);
889  }
890 
891  for (unsigned int i=0; i<flatAnn.size(); i++) {
892  if (flatAnn[i]->isCall("gecode_search")) {
893  AST::Call* c = flatAnn[i]->getCall();
894  branchWithPlugin(c->args);
895  } else if (flatAnn[i]->isCall("int_search")) {
896  AST::Call *call = flatAnn[i]->getCall("int_search");
897  AST::Array *args = call->getArgs(4);
898  AST::Array *vars = args->a[0]->getArray();
899  int k=vars->a.size();
900  for (int i=vars->a.size(); i--;)
901  if (vars->a[i]->isInt())
902  k--;
903  IntVarArgs va(k);
904  vector<string> names;
905  k=0;
906  for (unsigned int i=0; i<vars->a.size(); i++) {
907  if (vars->a[i]->isInt())
908  continue;
909  va[k++] = iv[vars->a[i]->getIntVar()];
910  iv_searched[vars->a[i]->getIntVar()] = true;
911  names.push_back(vars->a[i]->getVarName());
912  }
913  std::string r0, r1;
914  BrancherHandle bh = branch(*this, va,
915  ann2ivarsel(args->a[1],rnd,decay),
916  ann2ivalsel(args->a[2],r0,r1,rnd),
917  NULL,
918  &varValPrint<IntVar>);
919  branchInfo.add(bh,r0,r1,names);
920  } else if (flatAnn[i]->isCall("int_assign")) {
921  AST::Call *call = flatAnn[i]->getCall("int_assign");
922  AST::Array *args = call->getArgs(2);
923  AST::Array *vars = args->a[0]->getArray();
924  int k=vars->a.size();
925  for (int i=vars->a.size(); i--;)
926  if (vars->a[i]->isInt())
927  k--;
928  IntVarArgs va(k);
929  k=0;
930  for (unsigned int i=0; i<vars->a.size(); i++) {
931  if (vars->a[i]->isInt())
932  continue;
933  va[k++] = iv[vars->a[i]->getIntVar()];
934  iv_searched[vars->a[i]->getIntVar()] = true;
935  }
936  assign(*this, va, ann2asnivalsel(args->a[1],rnd), NULL,
937  &varValPrint<IntVar>);
938  } else if (flatAnn[i]->isCall("bool_search")) {
939  AST::Call *call = flatAnn[i]->getCall("bool_search");
940  AST::Array *args = call->getArgs(4);
941  AST::Array *vars = args->a[0]->getArray();
942  int k=vars->a.size();
943  for (int i=vars->a.size(); i--;)
944  if (vars->a[i]->isBool())
945  k--;
946  BoolVarArgs va(k);
947  k=0;
948  vector<string> names;
949  for (unsigned int i=0; i<vars->a.size(); i++) {
950  if (vars->a[i]->isBool())
951  continue;
952  va[k++] = bv[vars->a[i]->getBoolVar()];
953  bv_searched[vars->a[i]->getBoolVar()] = true;
954  names.push_back(vars->a[i]->getVarName());
955  }
956 
957  std::string r0, r1;
958  BrancherHandle bh = branch(*this, va,
959  ann2ivarsel(args->a[1],rnd,decay),
960  ann2ivalsel(args->a[2],r0,r1,rnd), NULL,
961  &varValPrint<BoolVar>);
962  branchInfo.add(bh,r0,r1,names);
963  } else if (flatAnn[i]->isCall("int_default_search")) {
964  AST::Call *call = flatAnn[i]->getCall("int_default_search");
965  AST::Array *args = call->getArgs(2);
966  def_int_varsel = ann2ivarsel(args->a[0],rnd,decay);
967  std::string r0;
968  def_int_valsel = ann2ivalsel(args->a[1],r0,r0,rnd);
969  } else if (flatAnn[i]->isCall("bool_default_search")) {
970  AST::Call *call = flatAnn[i]->getCall("bool_default_search");
971  AST::Array *args = call->getArgs(2);
972  def_bool_varsel = ann2ivarsel(args->a[0],rnd,decay);
973  std::string r0;
974  def_bool_valsel = ann2ivalsel(args->a[1],r0,r0,rnd);
975  } else if (flatAnn[i]->isCall("set_search")) {
976 #ifdef GECODE_HAS_SET_VARS
977  AST::Call *call = flatAnn[i]->getCall("set_search");
978  AST::Array *args = call->getArgs(4);
979  AST::Array *vars = args->a[0]->getArray();
980  int k=vars->a.size();
981  for (int i=vars->a.size(); i--;)
982  if (vars->a[i]->isSet())
983  k--;
984  SetVarArgs va(k);
985  k=0;
986  vector<string> names;
987  for (unsigned int i=0; i<vars->a.size(); i++) {
988  if (vars->a[i]->isSet())
989  continue;
990  va[k++] = sv[vars->a[i]->getSetVar()];
991  sv_searched[vars->a[i]->getSetVar()] = true;
992  names.push_back(vars->a[i]->getVarName());
993  }
994  std::string r0, r1;
995  BrancherHandle bh = branch(*this, va,
996  ann2svarsel(args->a[1],rnd,decay),
997  ann2svalsel(args->a[2],r0,r1,rnd),
998  NULL,
999  &varValPrint<SetVar>);
1000  branchInfo.add(bh,r0,r1,names);
1001 #else
1002  if (!ignoreUnknown) {
1003  err << "Warning, ignored search annotation: ";
1004  flatAnn[i]->print(err);
1005  err << std::endl;
1006  }
1007 #endif
1008  } else if (flatAnn[i]->isCall("set_default_search")) {
1009 #ifdef GECODE_HAS_SET_VARS
1010  AST::Call *call = flatAnn[i]->getCall("set_default_search");
1011  AST::Array *args = call->getArgs(2);
1012  def_set_varsel = ann2svarsel(args->a[0],rnd,decay);
1013  std::string r0;
1014  def_set_valsel = ann2svalsel(args->a[1],r0,r0,rnd);
1015 #else
1016  if (!ignoreUnknown) {
1017  err << "Warning, ignored search annotation: ";
1018  flatAnn[i]->print(err);
1019  err << std::endl;
1020  }
1021 #endif
1022  } else if (flatAnn[i]->isCall("float_default_search")) {
1023 #ifdef GECODE_HAS_FLOAT_VARS
1024  AST::Call *call = flatAnn[i]->getCall("float_default_search");
1025  AST::Array *args = call->getArgs(2);
1026  def_float_varsel = ann2fvarsel(args->a[0],rnd,decay);
1027  std::string r0;
1028  def_float_valsel = ann2fvalsel(args->a[1],r0,r0);
1029 #else
1030  if (!ignoreUnknown) {
1031  err << "Warning, ignored search annotation: ";
1032  flatAnn[i]->print(err);
1033  err << std::endl;
1034  }
1035 #endif
1036  } else if (flatAnn[i]->isCall("float_search")) {
1037 #ifdef GECODE_HAS_FLOAT_VARS
1038  AST::Call *call = flatAnn[i]->getCall("float_search");
1039  AST::Array *args = call->getArgs(5);
1040  AST::Array *vars = args->a[0]->getArray();
1041  int k=vars->a.size();
1042  for (int i=vars->a.size(); i--;)
1043  if (vars->a[i]->isFloat())
1044  k--;
1045  FloatVarArgs va(k);
1046  k=0;
1047  vector<string> names;
1048  for (unsigned int i=0; i<vars->a.size(); i++) {
1049  if (vars->a[i]->isFloat())
1050  continue;
1051  va[k++] = fv[vars->a[i]->getFloatVar()];
1052  fv_searched[vars->a[i]->getFloatVar()] = true;
1053  names.push_back(vars->a[i]->getVarName());
1054  }
1055  std::string r0, r1;
1056  BrancherHandle bh = branch(*this, va,
1057  ann2fvarsel(args->a[2],rnd,decay),
1058  ann2fvalsel(args->a[3],r0,r1),
1059  NULL,
1060  &varValPrintF);
1061  branchInfo.add(bh,r0,r1,names);
1062 #else
1063  if (!ignoreUnknown) {
1064  err << "Warning, ignored search annotation: ";
1065  flatAnn[i]->print(err);
1066  err << std::endl;
1067  }
1068 #endif
1069  } else {
1070  if (!ignoreUnknown) {
1071  err << "Warning, ignored search annotation: ";
1072  flatAnn[i]->print(err);
1073  err << std::endl;
1074  }
1075  }
1076  }
1077  }
1078  int introduced = 0;
1079  int funcdep = 0;
1080  int searched = 0;
1081  for (int i=iv.size(); i--;) {
1082  if (iv_searched[i]) {
1083  searched++;
1084  } else if (iv_introduced[2*i]) {
1085  if (iv_introduced[2*i+1]) {
1086  funcdep++;
1087  } else {
1088  introduced++;
1089  }
1090  }
1091  }
1092  IntVarArgs iv_sol(iv.size()-(introduced+funcdep+searched));
1093  IntVarArgs iv_tmp(introduced);
1094  for (int i=iv.size(), j=0, k=0; i--;) {
1095  if (iv_searched[i])
1096  continue;
1097  if (iv_introduced[2*i]) {
1098  if (!iv_introduced[2*i+1]) {
1099  iv_tmp[j++] = iv[i];
1100  }
1101  } else {
1102  iv_sol[k++] = iv[i];
1103  }
1104  }
1105 
1106  introduced = 0;
1107  funcdep = 0;
1108  searched = 0;
1109  for (int i=bv.size(); i--;) {
1110  if (bv_searched[i]) {
1111  searched++;
1112  } else if (bv_introduced[2*i]) {
1113  if (bv_introduced[2*i+1]) {
1114  funcdep++;
1115  } else {
1116  introduced++;
1117  }
1118  }
1119  }
1120  BoolVarArgs bv_sol(bv.size()-(introduced+funcdep+searched));
1121  BoolVarArgs bv_tmp(introduced);
1122  for (int i=bv.size(), j=0, k=0; i--;) {
1123  if (bv_searched[i])
1124  continue;
1125  if (bv_introduced[2*i]) {
1126  if (!bv_introduced[2*i+1]) {
1127  bv_tmp[j++] = bv[i];
1128  }
1129  } else {
1130  bv_sol[k++] = bv[i];
1131  }
1132  }
1133 
1134  if (iv_sol.size() > 0)
1135  branch(*this, iv_sol, def_int_varsel, def_int_valsel);
1136  if (bv_sol.size() > 0)
1137  branch(*this, bv_sol, def_bool_varsel, def_bool_valsel);
1138 #ifdef GECODE_HAS_FLOAT_VARS
1139  introduced = 0;
1140  funcdep = 0;
1141  searched = 0;
1142  for (int i=fv.size(); i--;) {
1143  if (fv_searched[i]) {
1144  searched++;
1145  } else if (fv_introduced[2*i]) {
1146  if (fv_introduced[2*i+1]) {
1147  funcdep++;
1148  } else {
1149  introduced++;
1150  }
1151  }
1152  }
1153  FloatVarArgs fv_sol(fv.size()-(introduced+funcdep+searched));
1154  FloatVarArgs fv_tmp(introduced);
1155  for (int i=fv.size(), j=0, k=0; i--;) {
1156  if (fv_searched[i])
1157  continue;
1158  if (fv_introduced[2*i]) {
1159  if (!fv_introduced[2*i+1]) {
1160  fv_tmp[j++] = fv[i];
1161  }
1162  } else {
1163  fv_sol[k++] = fv[i];
1164  }
1165  }
1166 
1167  if (fv_sol.size() > 0)
1168  branch(*this, fv_sol, def_float_varsel, def_float_valsel);
1169 #endif
1170 #ifdef GECODE_HAS_SET_VARS
1171  introduced = 0;
1172  funcdep = 0;
1173  searched = 0;
1174  for (int i=sv.size(); i--;) {
1175  if (sv_searched[i]) {
1176  searched++;
1177  } else if (sv_introduced[2*i]) {
1178  if (sv_introduced[2*i+1]) {
1179  funcdep++;
1180  } else {
1181  introduced++;
1182  }
1183  }
1184  }
1185  SetVarArgs sv_sol(sv.size()-(introduced+funcdep+searched));
1186  SetVarArgs sv_tmp(introduced);
1187  for (int i=sv.size(), j=0, k=0; i--;) {
1188  if (sv_searched[i])
1189  continue;
1190  if (sv_introduced[2*i]) {
1191  if (!sv_introduced[2*i+1]) {
1192  sv_tmp[j++] = sv[i];
1193  }
1194  } else {
1195  sv_sol[k++] = sv[i];
1196  }
1197  }
1198 
1199  if (sv_sol.size() > 0)
1200  branch(*this, sv_sol, def_set_varsel, def_set_valsel);
1201 #endif
1202  iv_aux = IntVarArray(*this, iv_tmp);
1203  bv_aux = BoolVarArray(*this, bv_tmp);
1204  int n_aux = iv_aux.size() + bv_aux.size();
1205 #ifdef GECODE_HAS_SET_VARS
1206  sv_aux = SetVarArray(*this, sv_tmp);
1207  n_aux += sv_aux.size();
1208 #endif
1209 #ifdef GECODE_HAS_FLOAT_VARS
1210  fv_aux = FloatVarArray(*this, fv_tmp);
1211  n_aux += fv_aux.size();
1212 #endif
1213  if (n_aux > 0) {
1214  AuxVarBrancher::post(*this, def_int_varsel, def_int_valsel,
1215  def_bool_varsel, def_bool_valsel
1216 #ifdef GECODE_HAS_SET_VARS
1217  , def_set_varsel, def_set_valsel
1218 #endif
1219 #ifdef GECODE_HAS_FLOAT_VARS
1220  , def_float_varsel, def_float_valsel
1221 #endif
1222  );
1223  }
1224  }
1225 
1226  AST::Array*
1228  return _solveAnnotations;
1229  }
1230 
1231  void
1233  _method = SAT;
1234  _solveAnnotations = ann;
1235  }
1236 
1237  void
1238  FlatZincSpace::minimize(int var, bool isInt, AST::Array* ann) {
1239  _method = MIN;
1240  _optVar = var;
1241  _optVarIsInt = isInt;
1242  // Branch on optimization variable to ensure that it is given a value.
1243  AST::Call* c;
1244  if (isInt) {
1245  AST::Array* args = new AST::Array(4);
1246  args->a[0] = new AST::Array(new AST::IntVar(_optVar));
1247  args->a[1] = new AST::Atom("input_order");
1248  args->a[2] = new AST::Atom("indomain_min");
1249  args->a[3] = new AST::Atom("complete");
1250  c = new AST::Call("int_search", args);
1251  } else {
1252  AST::Array* args = new AST::Array(5);
1253  args->a[0] = new AST::Array(new AST::FloatVar(_optVar));
1254  args->a[1] = new AST::FloatLit(0.0);
1255  args->a[2] = new AST::Atom("input_order");
1256  args->a[3] = new AST::Atom("indomain_split");
1257  args->a[4] = new AST::Atom("complete");
1258  c = new AST::Call("float_search", args);
1259  }
1260  if (!ann)
1261  ann = new AST::Array(c);
1262  else
1263  ann->a.push_back(c);
1264  _solveAnnotations = ann;
1265  }
1266 
1267  void
1268  FlatZincSpace::maximize(int var, bool isInt, AST::Array* ann) {
1269  _method = MAX;
1270  _optVar = var;
1271  _optVarIsInt = isInt;
1272  // Branch on optimization variable to ensure that it is given a value.
1273  AST::Call* c;
1274  if (isInt) {
1275  AST::Array* args = new AST::Array(4);
1276  args->a[0] = new AST::Array(new AST::IntVar(_optVar));
1277  args->a[1] = new AST::Atom("input_order");
1278  args->a[2] = new AST::Atom("indomain_max");
1279  args->a[3] = new AST::Atom("complete");
1280  c = new AST::Call("int_search", args);
1281  } else {
1282  AST::Array* args = new AST::Array(5);
1283  args->a[0] = new AST::Array(new AST::FloatVar(_optVar));
1284  args->a[1] = new AST::FloatLit(0.0);
1285  args->a[2] = new AST::Atom("input_order");
1286  args->a[3] = new AST::Atom("indomain_split_reverse");
1287  args->a[4] = new AST::Atom("complete");
1288  c = new AST::Call("float_search", args);
1289  }
1290  if (!ann)
1291  ann = new AST::Array(c);
1292  else
1293  ann->a.push_back(c);
1294  _solveAnnotations = ann;
1295  }
1296 
1298  delete _solveAnnotations;
1299  }
1300 
1301 #ifdef GECODE_HAS_GIST
1302 
1306  template<class Engine>
1307  class GistEngine {
1308  };
1309 
1311  template<typename S>
1312  class GistEngine<DFS<S> > {
1313  public:
1314  static void explore(S* root, const FlatZincOptions& opt,
1317  o.c_d = opt.c_d(); o.a_d = opt.a_d();
1318  o.inspect.click(i);
1319  o.inspect.compare(c);
1320  (void) Gecode::Gist::dfs(root, o);
1321  }
1322  };
1323 
1325  template<typename S>
1326  class GistEngine<BAB<S> > {
1327  public:
1328  static void explore(S* root, const FlatZincOptions& opt,
1329  Gist::Inspector* i, Gist::Comparator* c) {
1331  o.c_d = opt.c_d(); o.a_d = opt.a_d();
1332  o.inspect.click(i);
1333  o.inspect.compare(c);
1334  (void) Gecode::Gist::bab(root, o);
1335  }
1336  };
1337 
1339  template<class S>
1340  class FZPrintingInspector
1342  private:
1343  const Printer& p;
1344  public:
1346  FZPrintingInspector(const Printer& p0);
1348  virtual void inspect(const Space& node);
1350  virtual void finalize(void);
1351  };
1352 
1353  template<class S>
1354  FZPrintingInspector<S>::FZPrintingInspector(const Printer& p0)
1355  : TextOutput("Gecode/FlatZinc"), p(p0) {}
1356 
1357  template<class S>
1358  void
1359  FZPrintingInspector<S>::inspect(const Space& node) {
1360  init();
1361  dynamic_cast<const S&>(node).print(getStream(), p);
1362  getStream() << std::endl;
1363  }
1364 
1365  template<class S>
1366  void
1367  FZPrintingInspector<S>::finalize(void) {
1369  }
1370 
1371  template<class S>
1372  class FZPrintingComparator
1373  : public Gecode::Gist::VarComparator<S> {
1374  private:
1375  const Printer& p;
1376  public:
1378  FZPrintingComparator(const Printer& p0);
1379 
1381  virtual void compare(const Space& s0, const Space& s1);
1382  };
1383 
1384  template<class S>
1385  FZPrintingComparator<S>::FZPrintingComparator(const Printer& p0)
1386  : Gecode::Gist::VarComparator<S>("Gecode/FlatZinc"), p(p0) {}
1387 
1388  template<class S>
1389  void
1390  FZPrintingComparator<S>::compare(const Space& s0, const Space& s1) {
1391  this->init();
1392  try {
1393  dynamic_cast<const S&>(s0).compare(dynamic_cast<const S&>(s1),
1394  this->getStream(), p);
1395  } catch (Exception& e) {
1396  this->getStream() << "Exception: " << e.what();
1397  }
1398  this->getStream() << std::endl;
1399  }
1400 
1401 #endif
1402 
1403 
1404  template<template<class> class Engine>
1405  void
1406  FlatZincSpace::runEngine(std::ostream& out, const Printer& p,
1407  const FlatZincOptions& opt, Support::Timer& t_total) {
1408  if (opt.restart()==RM_NONE) {
1409  runMeta<Engine,Driver::EngineToMeta>(out,p,opt,t_total);
1410  } else {
1411  runMeta<Engine,RBS>(out,p,opt,t_total);
1412  }
1413  }
1414 
1415  template<template<class> class Engine,
1416  template<template<class> class,class> class Meta>
1417  void
1418  FlatZincSpace::runMeta(std::ostream& out, const Printer& p,
1419  const FlatZincOptions& opt, Support::Timer& t_total) {
1420 #ifdef GECODE_HAS_GIST
1421  if (opt.mode() == SM_GIST) {
1422  FZPrintingInspector<FlatZincSpace> pi(p);
1423  FZPrintingComparator<FlatZincSpace> pc(p);
1424  (void) GistEngine<Engine<FlatZincSpace> >::explore(this,opt,&pi,&pc);
1425  return;
1426  }
1427 #endif
1428  StatusStatistics sstat;
1429  unsigned int n_p = 0;
1430  Support::Timer t_solve;
1431  t_solve.start();
1432  if (status(sstat) != SS_FAILED) {
1433  n_p = propagators();
1434  }
1435  Search::Options o;
1436  o.stop = Driver::CombinedStop::create(opt.node(), opt.fail(), opt.time(),
1437  true);
1438  o.c_d = opt.c_d();
1439  o.a_d = opt.a_d();
1440  o.threads = opt.threads();
1441  o.nogoods_limit = opt.nogoods() ? opt.nogoods_limit() : 0;
1442  o.cutoff = Driver::createCutoff(opt);
1443  if (opt.interrupt())
1445  Meta<Engine,FlatZincSpace> se(this,o);
1446  int noOfSolutions = _method == SAT ? opt.solutions() : 0;
1447  bool printAll = _method == SAT || opt.allSolutions();
1448  int findSol = noOfSolutions;
1449  FlatZincSpace* sol = NULL;
1450  while (FlatZincSpace* next_sol = se.next()) {
1451  delete sol;
1452  sol = next_sol;
1453  if (printAll) {
1454  sol->print(out, p);
1455  out << "----------" << std::endl;
1456  }
1457  if (--findSol==0)
1458  goto stopped;
1459  }
1460  if (sol && !printAll) {
1461  sol->print(out, p);
1462  out << "----------" << std::endl;
1463  }
1464  if (!se.stopped()) {
1465  if (sol) {
1466  out << "==========" << endl;
1467  } else {
1468  out << "=====UNSATISFIABLE=====" << endl;
1469  }
1470  } else if (!sol) {
1471  out << "=====UNKNOWN=====" << endl;
1472  }
1473  delete sol;
1474  stopped:
1475  if (opt.interrupt())
1477  if (opt.mode() == SM_STAT) {
1478  Gecode::Search::Statistics stat = se.statistics();
1479  out << endl
1480  << "%% runtime: ";
1481  Driver::stop(t_total,out);
1482  out << endl
1483  << "%% solvetime: ";
1484  Driver::stop(t_solve,out);
1485  out << endl
1486  << "%% solutions: "
1487  << std::abs(noOfSolutions - findSol) << endl
1488  << "%% variables: "
1489  << (intVarCount + boolVarCount + setVarCount) << endl
1490  << "%% propagators: " << n_p << endl
1491  << "%% propagations: " << sstat.propagate+stat.propagate << endl
1492  << "%% nodes: " << stat.node << endl
1493  << "%% failures: " << stat.fail << endl
1494  << "%% restarts: " << stat.restart << endl
1495  << "%% peak depth: " << stat.depth << endl
1496  << endl;
1497  }
1498  delete o.stop;
1499  }
1500 
1501 #ifdef GECODE_HAS_QT
1502  void
1503  FlatZincSpace::branchWithPlugin(AST::Node* ann) {
1504  if (AST::Call* c = dynamic_cast<AST::Call*>(ann)) {
1505  QString pluginName(c->id.c_str());
1506  if (QLibrary::isLibrary(pluginName+".dll")) {
1507  pluginName += ".dll";
1508  } else if (QLibrary::isLibrary(pluginName+".dylib")) {
1509  pluginName = "lib" + pluginName + ".dylib";
1510  } else if (QLibrary::isLibrary(pluginName+".so")) {
1511  // Must check .so after .dylib so that Mac OS uses .dylib
1512  pluginName = "lib" + pluginName + ".so";
1513  }
1514  QPluginLoader pl(pluginName);
1515  QObject* plugin_o = pl.instance();
1516  if (!plugin_o) {
1517  throw FlatZinc::Error("FlatZinc",
1518  "Error loading plugin "+pluginName.toStdString()+
1519  ": "+pl.errorString().toStdString());
1520  }
1521  BranchPlugin* pb = qobject_cast<BranchPlugin*>(plugin_o);
1522  if (!pb) {
1523  throw FlatZinc::Error("FlatZinc",
1524  "Error loading plugin "+pluginName.toStdString()+
1525  ": does not contain valid PluginBrancher");
1526  }
1527  pb->branch(*this, c);
1528  }
1529  }
1530 #else
1531  void
1532  FlatZincSpace::branchWithPlugin(AST::Node*) {
1533  throw FlatZinc::Error("FlatZinc",
1534  "Branching with plugins not supported (requires Qt support)");
1535  }
1536 #endif
1537 
1538  void
1539  FlatZincSpace::run(std::ostream& out, const Printer& p,
1540  const FlatZincOptions& opt, Support::Timer& t_total) {
1541  switch (_method) {
1542  case MIN:
1543  case MAX:
1544  runEngine<BAB>(out,p,opt,t_total);
1545  break;
1546  case SAT:
1547  runEngine<DFS>(out,p,opt,t_total);
1548  break;
1549  }
1550  }
1551 
1552  void
1554  if (_optVarIsInt) {
1555  if (_method == MIN)
1556  rel(*this, iv[_optVar], IRT_LE,
1557  static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
1558  else if (_method == MAX)
1559  rel(*this, iv[_optVar], IRT_GR,
1560  static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
1561  } else {
1562 #ifdef GECODE_HAS_FLOAT_VARS
1563  if (_method == MIN)
1564  rel(*this, fv[_optVar], FRT_LE,
1565  static_cast<const FlatZincSpace*>(&s)->fv[_optVar].val());
1566  else if (_method == MAX)
1567  rel(*this, fv[_optVar], FRT_GR,
1568  static_cast<const FlatZincSpace*>(&s)->fv[_optVar].val());
1569 #endif
1570  }
1571  }
1572 
1573  Space*
1574  FlatZincSpace::copy(bool share) {
1575  return new FlatZincSpace(share, *this);
1576  }
1577 
1580  return _method;
1581  }
1582 
1583  int
1585  return _optVar;
1586  }
1587 
1588  bool
1590  return _optVarIsInt;
1591  }
1592 
1593  void
1594  FlatZincSpace::print(std::ostream& out, const Printer& p) const {
1595  p.print(out, iv, bv
1596 #ifdef GECODE_HAS_SET_VARS
1597  , sv
1598 #endif
1599 #ifdef GECODE_HAS_FLOAT_VARS
1600  , fv
1601 #endif
1602  );
1603  }
1604 
1605  void
1606  FlatZincSpace::compare(const Space& s, std::ostream& out) const {
1607  (void) s; (void) out;
1608 #ifdef GECODE_HAS_GIST
1609  const FlatZincSpace& fs = dynamic_cast<const FlatZincSpace&>(s);
1610  for (int i = 0; i < iv.size(); ++i) {
1611  std::stringstream ss;
1612  ss << "iv[" << i << "]";
1613  std::string result(Gecode::Gist::Comparator::compare(ss.str(), iv[i],
1614  fs.iv[i]));
1615  if (result.length() > 0) out << result << std::endl;
1616  }
1617  for (int i = 0; i < bv.size(); ++i) {
1618  std::stringstream ss;
1619  ss << "bv[" << i << "]";
1620  std::string result(Gecode::Gist::Comparator::compare(ss.str(), bv[i],
1621  fs.bv[i]));
1622  if (result.length() > 0) out << result << std::endl;
1623  }
1624 #ifdef GECODE_HAS_SET_VARS
1625  for (int i = 0; i < sv.size(); ++i) {
1626  std::stringstream ss;
1627  ss << "sv[" << i << "]";
1628  std::string result(Gecode::Gist::Comparator::compare(ss.str(), sv[i],
1629  fs.sv[i]));
1630  if (result.length() > 0) out << result << std::endl;
1631  }
1632 #endif
1633 #ifdef GECODE_HAS_FLOAT_VARS
1634  for (int i = 0; i < fv.size(); ++i) {
1635  std::stringstream ss;
1636  ss << "fv[" << i << "]";
1637  std::string result(Gecode::Gist::Comparator::compare(ss.str(), fv[i],
1638  fs.fv[i]));
1639  if (result.length() > 0) out << result << std::endl;
1640  }
1641 #endif
1642 #endif
1643  }
1644 
1645  void
1646  FlatZincSpace::compare(const FlatZincSpace& s, std::ostream& out,
1647  const Printer& p) const {
1648  p.printDiff(out, iv, s.iv, bv, s.bv
1649 #ifdef GECODE_HAS_SET_VARS
1650  , sv, s.sv
1651 #endif
1652 #ifdef GECODE_HAS_FLOAT_VARS
1653  , fv, s.fv
1654 #endif
1655  );
1656  }
1657 
1658  void
1660  p.shrinkArrays(*this, _optVar, _optVarIsInt, iv, bv
1661 #ifdef GECODE_HAS_SET_VARS
1662  , sv
1663 #endif
1664 #ifdef GECODE_HAS_FLOAT_VARS
1665  , fv
1666 #endif
1667  );
1668  }
1669 
1670  IntArgs
1672  AST::Array* a = arg->getArray();
1673  IntArgs ia(a->a.size()+offset);
1674  for (int i=offset; i--;)
1675  ia[i] = 0;
1676  for (int i=a->a.size(); i--;)
1677  ia[i+offset] = a->a[i]->getInt();
1678  return ia;
1679  }
1680  IntArgs
1682  AST::Array* a = arg->getArray();
1683  IntArgs ia(a->a.size()+offset);
1684  for (int i=offset; i--;)
1685  ia[i] = 0;
1686  for (int i=a->a.size(); i--;)
1687  ia[i+offset] = a->a[i]->getBool();
1688  return ia;
1689  }
1690  IntSet
1692  AST::SetLit* sl = n->getSet();
1693  IntSet d;
1694  if (sl->interval) {
1695  d = IntSet(sl->min, sl->max);
1696  } else {
1697  Region re(*this);
1698  int* is = re.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
1699  for (int i=sl->s.size(); i--; )
1700  is[i] = sl->s[i];
1701  d = IntSet(is, sl->s.size());
1702  }
1703  return d;
1704  }
1705  IntSetArgs
1707  AST::Array* a = arg->getArray();
1708  if (a->a.size() == 0) {
1709  IntSetArgs emptyIa(0);
1710  return emptyIa;
1711  }
1712  IntSetArgs ia(a->a.size()+offset);
1713  for (int i=offset; i--;)
1714  ia[i] = IntSet::empty;
1715  for (int i=a->a.size(); i--;) {
1716  ia[i+offset] = arg2intset(a->a[i]);
1717  }
1718  return ia;
1719  }
1720  IntVarArgs
1722  AST::Array* a = arg->getArray();
1723  if (a->a.size() == 0) {
1724  IntVarArgs emptyIa(0);
1725  return emptyIa;
1726  }
1727  IntVarArgs ia(a->a.size()+offset);
1728  for (int i=offset; i--;)
1729  ia[i] = IntVar(*this, 0, 0);
1730  for (int i=a->a.size(); i--;) {
1731  if (a->a[i]->isIntVar()) {
1732  ia[i+offset] = iv[a->a[i]->getIntVar()];
1733  } else {
1734  int value = a->a[i]->getInt();
1735  IntVar iv(*this, value, value);
1736  ia[i+offset] = iv;
1737  }
1738  }
1739  return ia;
1740  }
1741  BoolVarArgs
1742  FlatZincSpace::arg2boolvarargs(AST::Node* arg, int offset, int siv) {
1743  AST::Array* a = arg->getArray();
1744  if (a->a.size() == 0) {
1745  BoolVarArgs emptyIa(0);
1746  return emptyIa;
1747  }
1748  BoolVarArgs ia(a->a.size()+offset-(siv==-1?0:1));
1749  for (int i=offset; i--;)
1750  ia[i] = BoolVar(*this, 0, 0);
1751  for (int i=0; i<static_cast<int>(a->a.size()); i++) {
1752  if (i==siv)
1753  continue;
1754  if (a->a[i]->isBool()) {
1755  bool value = a->a[i]->getBool();
1756  BoolVar iv(*this, value, value);
1757  ia[offset++] = iv;
1758  } else if (a->a[i]->isIntVar() &&
1759  aliasBool2Int(a->a[i]->getIntVar()) != -1) {
1760  ia[offset++] = bv[aliasBool2Int(a->a[i]->getIntVar())];
1761  } else {
1762  ia[offset++] = bv[a->a[i]->getBoolVar()];
1763  }
1764  }
1765  return ia;
1766  }
1767  BoolVar
1769  BoolVar x0;
1770  if (n->isBool()) {
1771  x0 = BoolVar(*this, n->getBool(), n->getBool());
1772  }
1773  else {
1774  x0 = bv[n->getBoolVar()];
1775  }
1776  return x0;
1777  }
1778  IntVar
1780  IntVar x0;
1781  if (n->isIntVar()) {
1782  x0 = iv[n->getIntVar()];
1783  } else {
1784  x0 = IntVar(*this, n->getInt(), n->getInt());
1785  }
1786  return x0;
1787  }
1788  bool
1790  AST::Array* a = b->getArray();
1791  singleInt = -1;
1792  if (a->a.size() == 0)
1793  return true;
1794  for (int i=a->a.size(); i--;) {
1795  if (a->a[i]->isBoolVar() || a->a[i]->isBool()) {
1796  } else if (a->a[i]->isIntVar()) {
1797  if (aliasBool2Int(a->a[i]->getIntVar()) == -1) {
1798  if (singleInt != -1) {
1799  return false;
1800  }
1801  singleInt = i;
1802  }
1803  } else {
1804  return false;
1805  }
1806  }
1807  return singleInt==-1 || a->a.size() > 1;
1808  }
1809 #ifdef GECODE_HAS_SET_VARS
1810  SetVar
1812  SetVar x0;
1813  if (!n->isSetVar()) {
1814  IntSet d = arg2intset(n);
1815  x0 = SetVar(*this, d, d);
1816  } else {
1817  x0 = sv[n->getSetVar()];
1818  }
1819  return x0;
1820  }
1821  SetVarArgs
1822  FlatZincSpace::arg2setvarargs(AST::Node* arg, int offset, int doffset,
1823  const IntSet& od) {
1824  AST::Array* a = arg->getArray();
1825  SetVarArgs ia(a->a.size()+offset);
1826  for (int i=offset; i--;) {
1827  IntSet d = i<doffset ? od : IntSet::empty;
1828  ia[i] = SetVar(*this, d, d);
1829  }
1830  for (int i=a->a.size(); i--;) {
1831  ia[i+offset] = arg2SetVar(a->a[i]);
1832  }
1833  return ia;
1834  }
1835 #endif
1836 #ifdef GECODE_HAS_FLOAT_VARS
1837  FloatValArgs
1839  AST::Array* a = arg->getArray();
1840  FloatValArgs fa(a->a.size()+offset);
1841  for (int i=offset; i--;)
1842  fa[i] = 0.0;
1843  for (int i=a->a.size(); i--;)
1844  fa[i+offset] = a->a[i]->getFloat();
1845  return fa;
1846  }
1847  FloatVarArgs
1849  AST::Array* a = arg->getArray();
1850  if (a->a.size() == 0) {
1851  FloatVarArgs emptyFa(0);
1852  return emptyFa;
1853  }
1854  FloatVarArgs fa(a->a.size()+offset);
1855  for (int i=offset; i--;)
1856  fa[i] = FloatVar(*this, 0.0, 0.0);
1857  for (int i=a->a.size(); i--;) {
1858  if (a->a[i]->isFloatVar()) {
1859  fa[i+offset] = fv[a->a[i]->getFloatVar()];
1860  } else {
1861  double value = a->a[i]->getFloat();
1862  FloatVar fv(*this, value, value);
1863  fa[i+offset] = fv;
1864  }
1865  }
1866  return fa;
1867  }
1868  FloatVar
1870  FloatVar x0;
1871  if (n->isFloatVar()) {
1872  x0 = fv[n->getFloatVar()];
1873  } else {
1874  x0 = FloatVar(*this, n->getFloat(), n->getFloat());
1875  }
1876  return x0;
1877  }
1878 #endif
1879  IntConLevel
1881  if (ann) {
1882  if (ann->hasAtom("val"))
1883  return ICL_VAL;
1884  if (ann->hasAtom("domain"))
1885  return ICL_DOM;
1886  if (ann->hasAtom("bounds") ||
1887  ann->hasAtom("boundsR") ||
1888  ann->hasAtom("boundsD") ||
1889  ann->hasAtom("boundsZ"))
1890  return ICL_BND;
1891  }
1892  return ICL_DEF;
1893  }
1894 
1895 
1896  void
1898  _output = output;
1899  }
1900 
1901  void
1902  Printer::printElem(std::ostream& out,
1903  AST::Node* ai,
1904  const Gecode::IntVarArray& iv,
1905  const Gecode::BoolVarArray& bv
1906 #ifdef GECODE_HAS_SET_VARS
1907  , const Gecode::SetVarArray& sv
1908 #endif
1909 #ifdef GECODE_HAS_FLOAT_VARS
1910  ,
1911  const Gecode::FloatVarArray& fv
1912 #endif
1913  ) const {
1914  int k;
1915  if (ai->isInt(k)) {
1916  out << k;
1917  } else if (ai->isIntVar()) {
1918  out << iv[ai->getIntVar()];
1919  } else if (ai->isBoolVar()) {
1920  if (bv[ai->getBoolVar()].min() == 1) {
1921  out << "true";
1922  } else if (bv[ai->getBoolVar()].max() == 0) {
1923  out << "false";
1924  } else {
1925  out << "false..true";
1926  }
1927 #ifdef GECODE_HAS_SET_VARS
1928  } else if (ai->isSetVar()) {
1929  if (!sv[ai->getSetVar()].assigned()) {
1930  out << sv[ai->getSetVar()];
1931  return;
1932  }
1933  SetVarGlbRanges svr(sv[ai->getSetVar()]);
1934  if (!svr()) {
1935  out << "{}";
1936  return;
1937  }
1938  int min = svr.min();
1939  int max = svr.max();
1940  ++svr;
1941  if (svr()) {
1942  SetVarGlbValues svv(sv[ai->getSetVar()]);
1943  int i = svv.val();
1944  out << "{" << i;
1945  ++svv;
1946  for (; svv(); ++svv)
1947  out << ", " << svv.val();
1948  out << "}";
1949  } else {
1950  out << min << ".." << max;
1951  }
1952 #endif
1953 #ifdef GECODE_HAS_FLOAT_VARS
1954  } else if (ai->isFloatVar()) {
1955  if (fv[ai->getFloatVar()].assigned()) {
1956  FloatVal vv = fv[ai->getFloatVar()].val();
1957  FloatNum v;
1958  if (vv.singleton())
1959  v = vv.min();
1960  else if (vv < 0.0)
1961  v = vv.max();
1962  else
1963  v = vv.min();
1964  std::ostringstream oss;
1965  // oss << std::scientific;
1966  oss << std::setprecision(std::numeric_limits<double>::digits10);
1967  oss << v;
1968  if (oss.str().find(".") == std::string::npos)
1969  oss << ".0";
1970  out << oss.str();
1971  } else {
1972  out << fv[ai->getFloatVar()];
1973  }
1974 #endif
1975  } else if (ai->isBool()) {
1976  out << (ai->getBool() ? "true" : "false");
1977  } else if (ai->isSet()) {
1978  AST::SetLit* s = ai->getSet();
1979  if (s->interval) {
1980  out << s->min << ".." << s->max;
1981  } else {
1982  out << "{";
1983  for (unsigned int i=0; i<s->s.size(); i++) {
1984  out << s->s[i] << (i < s->s.size()-1 ? ", " : "}");
1985  }
1986  }
1987  } else if (ai->isString()) {
1988  std::string s = ai->getString();
1989  for (unsigned int i=0; i<s.size(); i++) {
1990  if (s[i] == '\\' && i<s.size()-1) {
1991  switch (s[i+1]) {
1992  case 'n': out << "\n"; break;
1993  case '\\': out << "\\"; break;
1994  case 't': out << "\t"; break;
1995  default: out << "\\" << s[i+1];
1996  }
1997  i++;
1998  } else {
1999  out << s[i];
2000  }
2001  }
2002  }
2003  }
2004 
2005  void
2006  Printer::printElemDiff(std::ostream& out,
2007  AST::Node* ai,
2008  const Gecode::IntVarArray& iv1,
2009  const Gecode::IntVarArray& iv2,
2010  const Gecode::BoolVarArray& bv1,
2011  const Gecode::BoolVarArray& bv2
2012 #ifdef GECODE_HAS_SET_VARS
2013  , const Gecode::SetVarArray& sv1,
2014  const Gecode::SetVarArray& sv2
2015 #endif
2016 #ifdef GECODE_HAS_FLOAT_VARS
2017  , const Gecode::FloatVarArray& fv1,
2018  const Gecode::FloatVarArray& fv2
2019 #endif
2020  ) const {
2021 #ifdef GECODE_HAS_GIST
2022  using namespace Gecode::Gist;
2023  int k;
2024  if (ai->isInt(k)) {
2025  out << k;
2026  } else if (ai->isIntVar()) {
2027  std::string res(Comparator::compare("",iv1[ai->getIntVar()],
2028  iv2[ai->getIntVar()]));
2029  if (res.length() > 0) {
2030  res.erase(0, 1); // Remove '='
2031  out << res;
2032  } else {
2033  out << iv1[ai->getIntVar()];
2034  }
2035  } else if (ai->isBoolVar()) {
2036  std::string res(Comparator::compare("",bv1[ai->getBoolVar()],
2037  bv2[ai->getBoolVar()]));
2038  if (res.length() > 0) {
2039  res.erase(0, 1); // Remove '='
2040  out << res;
2041  } else {
2042  out << bv1[ai->getBoolVar()];
2043  }
2044 #ifdef GECODE_HAS_SET_VARS
2045  } else if (ai->isSetVar()) {
2046  std::string res(Comparator::compare("",sv1[ai->getSetVar()],
2047  sv2[ai->getSetVar()]));
2048  if (res.length() > 0) {
2049  res.erase(0, 1); // Remove '='
2050  out << res;
2051  } else {
2052  out << sv1[ai->getSetVar()];
2053  }
2054 #endif
2055 #ifdef GECODE_HAS_FLOAT_VARS
2056  } else if (ai->isFloatVar()) {
2057  std::string res(Comparator::compare("",fv1[ai->getFloatVar()],
2058  fv2[ai->getFloatVar()]));
2059  if (res.length() > 0) {
2060  res.erase(0, 1); // Remove '='
2061  out << res;
2062  } else {
2063  out << fv1[ai->getFloatVar()];
2064  }
2065 #endif
2066  } else if (ai->isBool()) {
2067  out << (ai->getBool() ? "true" : "false");
2068  } else if (ai->isSet()) {
2069  AST::SetLit* s = ai->getSet();
2070  if (s->interval) {
2071  out << s->min << ".." << s->max;
2072  } else {
2073  out << "{";
2074  for (unsigned int i=0; i<s->s.size(); i++) {
2075  out << s->s[i] << (i < s->s.size()-1 ? ", " : "}");
2076  }
2077  }
2078  } else if (ai->isString()) {
2079  std::string s = ai->getString();
2080  for (unsigned int i=0; i<s.size(); i++) {
2081  if (s[i] == '\\' && i<s.size()-1) {
2082  switch (s[i+1]) {
2083  case 'n': out << "\n"; break;
2084  case '\\': out << "\\"; break;
2085  case 't': out << "\t"; break;
2086  default: out << "\\" << s[i+1];
2087  }
2088  i++;
2089  } else {
2090  out << s[i];
2091  }
2092  }
2093  }
2094 #endif
2095  }
2096 
2097  void
2098  Printer::print(std::ostream& out,
2099  const Gecode::IntVarArray& iv,
2100  const Gecode::BoolVarArray& bv
2101 #ifdef GECODE_HAS_SET_VARS
2102  ,
2103  const Gecode::SetVarArray& sv
2104 #endif
2105 #ifdef GECODE_HAS_FLOAT_VARS
2106  ,
2107  const Gecode::FloatVarArray& fv
2108 #endif
2109  ) const {
2110  if (_output == NULL)
2111  return;
2112  for (unsigned int i=0; i< _output->a.size(); i++) {
2113  AST::Node* ai = _output->a[i];
2114  if (ai->isArray()) {
2115  AST::Array* aia = ai->getArray();
2116  int size = aia->a.size();
2117  out << "[";
2118  for (int j=0; j<size; j++) {
2119  printElem(out,aia->a[j],iv,bv
2120 #ifdef GECODE_HAS_SET_VARS
2121  ,sv
2122 #endif
2123 #ifdef GECODE_HAS_FLOAT_VARS
2124  ,fv
2125 #endif
2126  );
2127  if (j<size-1)
2128  out << ", ";
2129  }
2130  out << "]";
2131  } else {
2132  printElem(out,ai,iv,bv
2133 #ifdef GECODE_HAS_SET_VARS
2134  ,sv
2135 #endif
2136 #ifdef GECODE_HAS_FLOAT_VARS
2137  ,fv
2138 #endif
2139  );
2140  }
2141  }
2142  }
2143 
2144  void
2145  Printer::printDiff(std::ostream& out,
2146  const Gecode::IntVarArray& iv1,
2147  const Gecode::IntVarArray& iv2,
2148  const Gecode::BoolVarArray& bv1,
2149  const Gecode::BoolVarArray& bv2
2150 #ifdef GECODE_HAS_SET_VARS
2151  ,
2152  const Gecode::SetVarArray& sv1,
2153  const Gecode::SetVarArray& sv2
2154 #endif
2155 #ifdef GECODE_HAS_FLOAT_VARS
2156  ,
2157  const Gecode::FloatVarArray& fv1,
2158  const Gecode::FloatVarArray& fv2
2159 #endif
2160  ) const {
2161  if (_output == NULL)
2162  return;
2163  for (unsigned int i=0; i< _output->a.size(); i++) {
2164  AST::Node* ai = _output->a[i];
2165  if (ai->isArray()) {
2166  AST::Array* aia = ai->getArray();
2167  int size = aia->a.size();
2168  out << "[";
2169  for (int j=0; j<size; j++) {
2170  printElemDiff(out,aia->a[j],iv1,iv2,bv1,bv2
2171 #ifdef GECODE_HAS_SET_VARS
2172  ,sv1,sv2
2173 #endif
2174 #ifdef GECODE_HAS_FLOAT_VARS
2175  ,fv1,fv2
2176 #endif
2177  );
2178  if (j<size-1)
2179  out << ", ";
2180  }
2181  out << "]";
2182  } else {
2183  printElemDiff(out,ai,iv1,iv2,bv1,bv2
2184 #ifdef GECODE_HAS_SET_VARS
2185  ,sv1,sv2
2186 #endif
2187 #ifdef GECODE_HAS_FLOAT_VARS
2188  ,fv1,fv2
2189 #endif
2190  );
2191  }
2192  }
2193  }
2194 
2195  void
2197  std::map<int,int>& iv, std::map<int,int>& bv,
2198  std::map<int,int>& sv, std::map<int,int>& fv) {
2199  if (node->isIntVar()) {
2200  AST::IntVar* x = static_cast<AST::IntVar*>(node);
2201  if (iv.find(x->i) == iv.end()) {
2202  int newi = iv.size();
2203  iv[x->i] = newi;
2204  }
2205  x->i = iv[x->i];
2206  } else if (node->isBoolVar()) {
2207  AST::BoolVar* x = static_cast<AST::BoolVar*>(node);
2208  if (bv.find(x->i) == bv.end()) {
2209  int newi = bv.size();
2210  bv[x->i] = newi;
2211  }
2212  x->i = bv[x->i];
2213  } else if (node->isSetVar()) {
2214  AST::SetVar* x = static_cast<AST::SetVar*>(node);
2215  if (sv.find(x->i) == sv.end()) {
2216  int newi = sv.size();
2217  sv[x->i] = newi;
2218  }
2219  x->i = sv[x->i];
2220  } else if (node->isFloatVar()) {
2221  AST::FloatVar* x = static_cast<AST::FloatVar*>(node);
2222  if (fv.find(x->i) == fv.end()) {
2223  int newi = fv.size();
2224  fv[x->i] = newi;
2225  }
2226  x->i = fv[x->i];
2227  }
2228  }
2229 
2230  void
2232  int& optVar, bool optVarIsInt,
2233  Gecode::IntVarArray& iv,
2235 #ifdef GECODE_HAS_SET_VARS
2236  ,
2238 #endif
2239 #ifdef GECODE_HAS_FLOAT_VARS
2240  ,
2242 #endif
2243  ) {
2244  if (_output == NULL) {
2245  if (optVarIsInt && optVar != -1) {
2246  IntVar ov = iv[optVar];
2247  iv = IntVarArray(home, 1);
2248  iv[0] = ov;
2249  optVar = 0;
2250  } else {
2251  iv = IntVarArray(home, 0);
2252  }
2253  bv = BoolVarArray(home, 0);
2254 #ifdef GECODE_HAS_SET_VARS
2255  sv = SetVarArray(home, 0);
2256 #endif
2257 #ifdef GECODE_HAS_FLOAT_VARS
2258  if (!optVarIsInt && optVar != -1) {
2259  FloatVar ov = fv[optVar];
2260  fv = FloatVarArray(home, 1);
2261  fv[0] = ov;
2262  optVar = 0;
2263  } else {
2264  fv = FloatVarArray(home,0);
2265  }
2266 #endif
2267  return;
2268  }
2269  std::map<int,int> iv_new;
2270  std::map<int,int> bv_new;
2271  std::map<int,int> sv_new;
2272  std::map<int,int> fv_new;
2273 
2274  if (optVar != -1) {
2275  if (optVarIsInt)
2276  iv_new[optVar] = 0;
2277  else
2278  fv_new[optVar] = 0;
2279  optVar = 0;
2280  }
2281 
2282  for (unsigned int i=0; i< _output->a.size(); i++) {
2283  AST::Node* ai = _output->a[i];
2284  if (ai->isArray()) {
2285  AST::Array* aia = ai->getArray();
2286  for (unsigned int j=0; j<aia->a.size(); j++) {
2287  shrinkElement(aia->a[j],iv_new,bv_new,sv_new,fv_new);
2288  }
2289  } else {
2290  shrinkElement(ai,iv_new,bv_new,sv_new,fv_new);
2291  }
2292  }
2293 
2294  IntVarArgs iva(iv_new.size());
2295  for (map<int,int>::iterator i=iv_new.begin(); i != iv_new.end(); ++i) {
2296  iva[(*i).second] = iv[(*i).first];
2297  }
2298  iv = IntVarArray(home, iva);
2299 
2300  BoolVarArgs bva(bv_new.size());
2301  for (map<int,int>::iterator i=bv_new.begin(); i != bv_new.end(); ++i) {
2302  bva[(*i).second] = bv[(*i).first];
2303  }
2304  bv = BoolVarArray(home, bva);
2305 
2306 #ifdef GECODE_HAS_SET_VARS
2307  SetVarArgs sva(sv_new.size());
2308  for (map<int,int>::iterator i=sv_new.begin(); i != sv_new.end(); ++i) {
2309  sva[(*i).second] = sv[(*i).first];
2310  }
2311  sv = SetVarArray(home, sva);
2312 #endif
2313 
2314 #ifdef GECODE_HAS_FLOAT_VARS
2315  FloatVarArgs fva(fv_new.size());
2316  for (map<int,int>::iterator i=fv_new.begin(); i != fv_new.end(); ++i) {
2317  fva[(*i).second] = fv[(*i).first];
2318  }
2319  fv = FloatVarArray(home, fva);
2320 #endif
2321  }
2322 
2324  delete _output;
2325  }
2326 
2327 }}
2328 
2329 // 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:1659
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:416
SetVarBranch SET_VAR_AFC_MIN(double d, BranchTbl tbl)
Select variable with smallest accumulated failure count with decay factor d.
Definition: var.hpp:123
void postConstraint(const ConExpr &ce, AST::Node *annotation)
Post a constraint specified by ce.
Definition: flatzinc.cpp:824
int floatVarCount
Number of float variables.
Definition: flatzinc.hh:366
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:320
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:2145
IntConLevel
Consistency levels for integer propagators.
Definition: int.hh:935
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:1671
FloatValBranch FLOAT_VAL_SPLIT_MAX(void)
Select values greater than mean of smallest and largest value.
Definition: val.hpp:64
Float literal node.
Definition: ast.hh:166
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:849
Search engine statistics
Definition: search.hh:136
std::string what(void) const
Definition: ast.hh:65
Boolean variable node.
Definition: ast.hh:200
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:1848
bool isBool(void)
Test if node is a Boolean node.
Definition: ast.hh:493
virtual Gecode::Space * copy(bool share)
Copy function.
Definition: flatzinc.cpp:1574
std::vector< bool > sv_introduced
Indicates whether a set variable is introduced by mzn2fzn.
Definition: flatzinc.hh:418
bool getBool(void)
Cast this node to a Boolean node.
Definition: ast.hh:449
const FloatNum max
Largest allowed float value.
Definition: float.hh:831
#define GECODE_HAS_SET_VARS
Definition: config.hpp:44
Gecode::BoolVarArray bv
The Boolean variables.
Definition: flatzinc.hh:407
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:376
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:2777
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:518
Which values to select for branching first.
Definition: int.hh:3909
Search engine options
Definition: search.hh:204
SetLit * getSet(void)
Cast this node to a set literal node.
Definition: ast.hh:461
void newIntVar(IntVarSpec *vs)
Create new integer variable from specification.
Definition: flatzinc.cpp:709
Abstract base class for comparators.
Definition: gist.hh:123
Call * getCall(void)
Return function call.
Definition: ast.hh:346
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:936
int getFloatVar(void)
Cast this node to a Float variable node.
Definition: ast.hh:431
Gecode::IntVarArray iv
The integer variables.
Definition: flatzinc.hh:399
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:513
int boolVarCount
Number of Boolean variables.
Definition: flatzinc.hh:364
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
void update(Space &, bool share, VarArray< Var > &a)
Update array to be a clone of array a.
Definition: array.hpp:1072
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 minimize(int var, bool isInt, AST::Array *annotation)
Post that integer variable var should be minimized.
Definition: flatzinc.cpp:1238
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:481
bool isBoolVar(void)
Test if node is a Boolean variable node.
Definition: ast.hh:477
void compare(const Space &s, std::ostream &out) const
Compare this space with space s and print the differences on out.
Definition: flatzinc.cpp:1606
std::vector< Node * > a
Definition: ast.hh:236
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:364
Integer variable array.
Definition: int.hh:739
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:592
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:352
void init(int intVars, int boolVars, int setVars, int floatVars)
Initialize space with given number of variables.
Definition: flatzinc.cpp:684
Handle to region.
Definition: region.hpp:61
Greater ( )
Definition: int.hh:907
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:1276
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:399
const int max
Largest allowed integer value.
Definition: int.hh:111
Float variable array.
Definition: float.hh:1016
int vs2bsl(BoolVarSpec *bs)
Definition: flatzinc.cpp:340
Computation spaces.
Definition: core.hpp:1325
Abstract base class for inspectors.
Definition: gist.hh:103
FlatZincSpace(void)
Construct empty space.
Definition: flatzinc.cpp:676
FloatVarBranch FLOAT_VAR_NONE(void)
Select first unassigned variable.
Definition: var.hpp:92
const int min
Smallest allowed integer value.
Definition: int.hh:113
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:1880
void newSetVar(SetVarSpec *vs)
Create new set variable from specification.
Definition: flatzinc.cpp:748
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:403
Gecode::IntSet d(v, 7)
TieBreak< IntVarBranch > bool_varsel
Definition: flatzinc.cpp:123
unsigned int id(void) const
Return brancher id.
Definition: core.hpp:3013
void newBoolVar(BoolVarSpec *vs)
Create new Boolean variable from specification.
Definition: flatzinc.cpp:736
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:480
void post(FlatZincSpace &s, const ConExpr &ce, AST::Node *ann)
Post constraint specified by ce.
Definition: registry.cpp:63
SetVar arg2SetVar(AST::Node *n)
Convert n to SetVar.
Definition: flatzinc.cpp:1811
int optVar(void) const
Return index of variable used for optimization.
Definition: flatzinc.cpp:1584
int getSetVar(void)
Cast this node to a set variable node.
Definition: ast.hh:437
double getFloat(void)
Cast this node to a Float node.
Definition: ast.hh:455
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:2098
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:422
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:461
Base-class for branchers.
Definition: core.hpp:1071
FloatNum n
The middle value for branching.
Definition: float.hh:1375
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:238
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:426
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:293
int _optVar
Index of the variable to optimize.
Definition: flatzinc.hh:371
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:419
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:1779
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
int getBoolVar(void)
Cast this node to a Boolean variable node.
Definition: ast.hh:425
The Gecode Interactive Search Tool.
bool isSet(void)
Test if node is a set literal node.
Definition: ast.hh:501
std::vector< int > s
Definition: ast.hh:179
void fail(void)
Fail space.
Definition: core.hpp:3351
BoolVarArgs arg2boolvarargs(AST::Node *arg, int offset=0, int siv=-1)
Convert arg to BoolVarArgs.
Definition: flatzinc.cpp:1742
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:664
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:795
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:2196
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:1589
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:409
bool clone
Whether engines create a clone when being initialized.
Definition: search.hh:207
Array * getArgs(unsigned int n)
Definition: ast.hh:268
void print(std::ostream &out, const Printer &p) const
Produce output on out using p.
Definition: flatzinc.cpp:1594
SetValBranch SET_VAL_MAX_INC(void)
Include largest element.
Definition: val.hpp:79
Argument array for non-primitive types.
Definition: array.hpp:727
SetVarBranch SET_VAR_MAX_MAX(BranchTbl tbl)
Select variable with largest maximum unknown element.
Definition: var.hpp:178
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:905
Integer sets.
Definition: int.hh:169
Float variable node.
Definition: ast.hh:217
virtual void compare(const Space &s0, const Space &s1)=0
Call-back function.
Set variable node
Definition: ast.hh:225
Choice that only signals failure or success
Definition: flatzinc.cpp:103
struct Gecode::@512::NNF::@54::@55 b
For binary nodes (and, or, eqv)
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
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:1721
virtual void constrain(const Space &s)
Implement optimization.
Definition: flatzinc.cpp:1553
bool isIntVar(void)
Test if node is an integer variable node.
Definition: ast.hh:473
bool assigned(void) const
Test if all variables are assigned.
Definition: array.hpp:1085
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:634
bool isBoolArray(AST::Node *b, int &singleInt)
Check if b is array of Booleans (or has a single integer)
Definition: flatzinc.cpp:1789
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:411
bool done
Flag whether brancher is done.
Definition: flatzinc.cpp:71
Passing integer arguments.
Definition: int.hh:605
Passing Boolean variables.
Definition: int.hh:688
static const IntSet empty
Empty set.
Definition: int.hh:260
int size(void) const
Return size of array (number of elements)
Definition: array.hpp:985
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:367
bool _optVarIsInt
Whether variable to optimize is integer (or float)
Definition: flatzinc.hh:373
IntSet arg2intset(AST::Node *n)
Convert n to IntSet.
Definition: flatzinc.cpp:1691
Gecode::FloatVarArray fv_aux
The introduced float variables.
Definition: flatzinc.hh:424
SetValBranch SET_VAL_MIN_EXC(void)
Exclude smallest element.
Definition: val.hpp:64
Boolean variable array.
Definition: int.hh:784
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:489
bool isString(void)
Test if node is a string node.
Definition: ast.hh:505
const int v[7]
Definition: distinct.cpp:206
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:2613
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:443
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:209
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:324
SharedHandle::Object * object(void) const
Access to the shared object.
Definition: core.hpp:2576
bool isFloatVar(void)
Test if node is a float variable node.
Definition: ast.hh:485
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:348
Which values to select for assignment.
Definition: int.hh:4009
void rel(Home home, FloatVar x0, FloatRelType frt, FloatVal n)
Propagates .
Definition: rel.cpp:47
Exception class for FlatZinc errors
Definition: flatzinc.hh:561
Specification for floating point variables.
Definition: varspec.hh:123
TieBreak< FloatVarBranch > ann2fvarsel(AST::Node *ann, Rnd rnd, double decay)
Definition: flatzinc.cpp:548
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:834
The default consistency for a constraint.
Definition: int.hh:939
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:379
IntValBranch INT_VAL_MED(void)
Select greatest value not greater than the median.
Definition: val.hpp:73
struct Gecode::Space::@49::@51 c
Data available only during copying.
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:1297
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:429
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:1232
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:23
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:509
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:727
A space that can be initialized with a FlatZinc model.
Definition: flatzinc.hh:353
Gecode::IntVarArray iv_aux
The introduced integer variables.
Definition: flatzinc.hh:401
struct Gecode::Space::@49::@50 p
Data only available during propagation.
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:2231
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:937
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
void run(std::ostream &out, const Printer &p, const FlatZincOptions &opt, Gecode::Support::Timer &t_total)
Run the search.
Definition: flatzinc.cpp:1539
Gecode toplevel namespace
int * iv_boolalias
Indicates whether an integer variable aliases a Boolean variable.
Definition: flatzinc.hh:405
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:1268
int setVarCount
Number of set variables.
Definition: flatzinc.hh:368
Node representing a function call
Definition: ast.hh:258
int intVarCount
Number of integer variables.
Definition: flatzinc.hh:362
IntValBranch ann2ivalsel(AST::Node *ann, std::string &r0, std::string &r1, Rnd rnd)
Definition: flatzinc.cpp:410
SetVarArgs arg2setvarargs(AST::Node *arg, int offset=0, int doffset=0, const IntSet &od=IntSet::empty)
Convert n to SetVarArgs.
Definition: flatzinc.cpp:1822
A node in a FlatZinc abstract syntax tree.
Definition: ast.hh:71
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
IntArgs arg2boolargs(AST::Node *arg, int offset=0)
Convert arg (array of Booleans) to IntArgs.
Definition: flatzinc.cpp:1681
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
struct Gecode::@512::NNF::@54::@56 a
For atomic nodes.
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:1264
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:414
Home class for posting propagators
Definition: core.hpp:717
Options for Gist
Definition: gist.hh:238
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:467
FloatVarBranch FLOAT_VAR_AFC_MAX(double d, BranchTbl tbl)
Select variable with largest accumulated failure count with decay factor d.
Definition: var.hpp:134
FloatVar arg2FloatVar(AST::Node *n)
Convert n to FloatVar.
Definition: flatzinc.cpp:1869
Domain propagation or consistency.
Definition: int.hh:938
Depth-first search engine.
Definition: search.hh:489
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:1579
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:1838
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:1227
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:1897
BoolVar arg2BoolVar(AST::Node *n)
Convert n to BoolVar.
Definition: flatzinc.cpp:1768
IntSetArgs arg2intsetargs(AST::Node *arg, int offset=0)
Convert arg to IntSetArgs.
Definition: flatzinc.cpp:1706
Abstract representation of a constraint.
Definition: conexpr.hh:47