Generated on Wed Jan 1 2020 10:37:59 for Gecode by doxygen 1.8.16
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  * This file is part of Gecode, the generic constraint
14  * development environment:
15  * http://www.gecode.org
16  *
17  * Permission is hereby granted, free of charge, to any person obtaining
18  * a copy of this software and associated documentation files (the
19  * "Software"), to deal in the Software without restriction, including
20  * without limitation the rights to use, copy, modify, merge, publish,
21  * distribute, sublicense, and/or sell copies of the Software, and to
22  * permit persons to whom the Software is furnished to do so, subject to
23  * the following conditions:
24  *
25  * The above copyright notice and this permission notice shall be
26  * included in all copies or substantial portions of the Software.
27  *
28  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
29  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
30  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
31  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
32  * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
33  * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
34  * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
35  *
36  */
37 
38 #include <gecode/flatzinc.hh>
42 
43 #include <gecode/search.hh>
44 
45 #include <vector>
46 #include <string>
47 #include <sstream>
48 #include <limits>
49 #include <unordered_set>
50 
51 
52 namespace std {
53 
55  template<> struct hash<Gecode::TupleSet> {
57  forceinline size_t
58  operator()(const Gecode::TupleSet& x) const {
59  return x.hash();
60  }
61  };
62 
64  template<> struct hash<Gecode::SharedArray<int> > {
66  forceinline size_t
68  size_t seed = static_cast<size_t>(x.size());
69  for (int i=x.size(); i--; )
70  Gecode::cmb_hash(seed, x[i]);
71  return seed;
72  }
73  };
74 
76  template<> struct hash<Gecode::DFA> {
78  forceinline size_t operator()(const Gecode::DFA& d) const {
79  return d.hash();
80  }
81  };
82 
83 }
84 
85 namespace Gecode { namespace FlatZinc {
86 
87  // Default random number generator
88  Rnd defrnd(0);
89 
102  class AuxVarBrancher : public Brancher {
103  protected:
105  bool done;
108  IntValBranch int_valsel0,
109  TieBreak<BoolVarBranch> bool_varsel0,
110  BoolValBranch bool_valsel0
111 #ifdef GECODE_HAS_SET_VARS
112  ,
113  SetVarBranch set_varsel0,
114  SetValBranch set_valsel0
115 #endif
117  ,
118  TieBreak<FloatVarBranch> float_varsel0,
119  FloatValBranch float_valsel0
120 #endif
121  )
122  : Brancher(home), done(false),
123  int_varsel(int_varsel0), int_valsel(int_valsel0),
124  bool_varsel(bool_varsel0), bool_valsel(bool_valsel0)
125 #ifdef GECODE_HAS_SET_VARS
126  , set_varsel(set_varsel0), set_valsel(set_valsel0)
127 #endif
129  , float_varsel(float_varsel0), float_valsel(float_valsel0)
130 #endif
131  {}
134  : Brancher(home, b), done(b.done) {}
135 
137  class Choice : public Gecode::Choice {
138  public:
140  bool fail;
142  Choice(const Brancher& b, bool fail0)
143  : Gecode::Choice(b,1), fail(fail0) {}
145  virtual size_t size(void) const {
146  return sizeof(Choice);
147  }
149  virtual void archive(Archive& e) const {
151  e.put(fail);
152  }
153  };
154 
159 #ifdef GECODE_HAS_SET_VARS
162 #endif
163 #ifdef GECODE_HAS_FLOAT_VARS
166 #endif
167 
168  public:
170  virtual bool status(const Space& _home) const {
171  if (done) return false;
172  const FlatZincSpace& home = static_cast<const FlatZincSpace&>(_home);
173  for (int i=0; i<home.iv_aux.size(); i++)
174  if (!home.iv_aux[i].assigned()) return true;
175  for (int i=0; i<home.bv_aux.size(); i++)
176  if (!home.bv_aux[i].assigned()) return true;
177 #ifdef GECODE_HAS_SET_VARS
178  for (int i=0; i<home.sv_aux.size(); i++)
179  if (!home.sv_aux[i].assigned()) return true;
180 #endif
181 #ifdef GECODE_HAS_FLOAT_VARS
182  for (int i=0; i<home.fv_aux.size(); i++)
183  if (!home.fv_aux[i].assigned()) return true;
184 #endif
185  // No non-assigned variables left
186  return false;
187  }
189  virtual Choice* choice(Space& home) {
190  done = true;
191  FlatZincSpace& fzs = static_cast<FlatZincSpace&>(*home.clone());
192  fzs.needAuxVars = false;
195 #ifdef GECODE_HAS_SET_VARS
197 #endif
198 #ifdef GECODE_HAS_FLOAT_VARS
200 #endif
201  Search::Options opt; opt.clone = false;
202  FlatZincSpace* sol = dfs(&fzs, opt);
203  if (sol) {
204  delete sol;
205  return new Choice(*this,false);
206  } else {
207  return new Choice(*this,true);
208  }
209  }
211  virtual Choice* choice(const Space&, Archive& e) {
212  bool fail; e >> fail;
213  return new Choice(*this, fail);
214  }
216  virtual ExecStatus commit(Space&, const Gecode::Choice& c, unsigned int) {
217  return static_cast<const Choice&>(c).fail ? ES_FAILED : ES_OK;
218  }
220  virtual void print(const Space&, const Gecode::Choice& c,
221  unsigned int,
222  std::ostream& o) const {
223  o << "FlatZinc("
224  << (static_cast<const Choice&>(c).fail ? "fail" : "ok")
225  << ")";
226  }
228  virtual Actor* copy(Space& home) {
229  return new (home) AuxVarBrancher(home, *this);
230  }
232  static void post(Home home,
237 #ifdef GECODE_HAS_SET_VARS
238  ,
241 #endif
243  ,
246 #endif
247  ) {
248  (void) new (home) AuxVarBrancher(home, int_varsel, int_valsel,
250 #ifdef GECODE_HAS_SET_VARS
252 #endif
255 #endif
256  );
257  }
259  virtual size_t dispose(Space&) {
260  return sizeof(*this);
261  }
262  };
263 
265  private:
266  struct BI {
267  std::string r0;
268  std::string r1;
269  std::vector<std::string> n;
270  BI(void) : r0(""), r1(""), n(0) {}
271  BI(const std::string& r00, const std::string& r10,
272  const std::vector<std::string>& n0)
273  : r0(r00), r1(r10), n(n0) {}
274  };
275  std::vector<BI> v;
276  BranchInformationO(std::vector<BI> v0) : v(v0) {}
277  public:
279  virtual ~BranchInformationO(void) {}
280  virtual SharedHandle::Object* copy(void) const {
281  return new BranchInformationO(v);
282  }
285  const std::string& rel0,
286  const std::string& rel1,
287  const std::vector<std::string>& n) {
288  v.resize(std::max(static_cast<unsigned int>(v.size()),bg.id()+1));
289  v[bg.id()] = BI(rel0,rel1,n);
290  }
292  void print(const Brancher& b,
293  unsigned int a, int i, int n, std::ostream& o) const {
294  const BI& bi = v[b.group().id()];
295  o << bi.n[i] << " " << (a==0 ? bi.r0 : bi.r1) << " " << n;
296  }
297 #ifdef GECODE_HAS_FLOAT_VARS
298  void print(const Brancher& b,
299  unsigned int a, int i, const FloatNumBranch& nl,
300  std::ostream& o) const {
301  const BI& bi = v[b.group().id()];
302  o << bi.n[i] << " "
303  << (((a == 0) == nl.l) ? "<=" : ">=") << nl.n;
304  }
305 #endif
306  };
307 
309  : SharedHandle(NULL) {}
310 
312  : SharedHandle(bi) {}
313 
314  void
316  assert(object() == NULL);
317  object(new BranchInformationO());
318  }
319 
320  void
322  const std::string& rel0,
323  const std::string& rel1,
324  const std::vector<std::string>& n) {
325  static_cast<BranchInformationO*>(object())->add(bg,rel0,rel1,n);
326  }
327  void
328  BranchInformation::print(const Brancher& b, unsigned int a, int i,
329  int n, std::ostream& o) const {
330  static_cast<const BranchInformationO*>(object())->print(b,a,i,n,o);
331  }
332 #ifdef GECODE_HAS_FLOAT_VARS
333  void
334  BranchInformation::print(const Brancher& b, unsigned int a, int i,
335  const FloatNumBranch& nl, std::ostream& o) const {
336  static_cast<const BranchInformationO*>(object())->print(b,a,i,nl,o);
337  }
338 #endif
339  template<class Var>
340  void varValPrint(const Space &home, const Brancher& b,
341  unsigned int a,
342  Var, int i, const int& n,
343  std::ostream& o) {
344  static_cast<const FlatZincSpace&>(home).branchInfo.print(b,a,i,n,o);
345  }
346 
347 #ifdef GECODE_HAS_FLOAT_VARS
348  void varValPrintF(const Space &home, const Brancher& b,
349  unsigned int a,
350  FloatVar, int i, const FloatNumBranch& nl,
351  std::ostream& o) {
352  static_cast<const FlatZincSpace&>(home).branchInfo.print(b,a,i,nl,o);
353  }
354 #endif
355 
357  if (vs->assigned) {
358  return IntSet(vs->i,vs->i);
359  }
360  if (vs->domain()) {
361  AST::SetLit* sl = vs->domain.some();
362  if (sl->interval) {
363  return IntSet(sl->min, sl->max);
364  } else {
365  int* newdom = heap.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
366  for (int i=sl->s.size(); i--;)
367  newdom[i] = sl->s[i];
368  IntSet ret(newdom, sl->s.size());
369  heap.free(newdom, static_cast<unsigned long int>(sl->s.size()));
370  return ret;
371  }
372  }
374  }
375 
376  int vs2bsl(BoolVarSpec* bs) {
377  if (bs->assigned) {
378  return bs->i;
379  }
380  if (bs->domain()) {
381  AST::SetLit* sl = bs->domain.some();
382  assert(sl->interval);
383  return std::min(1, std::max(0, sl->min));
384  }
385  return 0;
386  }
387 
388  int vs2bsh(BoolVarSpec* bs) {
389  if (bs->assigned) {
390  return bs->i;
391  }
392  if (bs->domain()) {
393  AST::SetLit* sl = bs->domain.some();
394  assert(sl->interval);
395  return std::max(0, std::min(1, sl->max));
396  }
397  return 1;
398  }
399 
400  TieBreak<IntVarBranch> ann2ivarsel(AST::Node* ann, Rnd rnd, double decay) {
401  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
402  if (s->id == "input_order")
404  if (s->id == "first_fail")
406  if (s->id == "anti_first_fail")
408  if (s->id == "smallest")
410  if (s->id == "largest")
412  if (s->id == "occurrence")
414  if (s->id == "max_regret")
416  if (s->id == "most_constrained")
419  if (s->id == "random") {
420  return TieBreak<IntVarBranch>(INT_VAR_RND(rnd));
421  }
422  if (s->id == "dom_w_deg") {
424  }
425  if (s->id == "afc_min")
427  if (s->id == "afc_max")
429  if (s->id == "afc_size_min")
431  if (s->id == "afc_size_max") {
433  }
434  if (s->id == "action_min")
436  if (s->id == "action_max")
438  if (s->id == "action_size_min")
440  if (s->id == "action_size_max")
442  }
443  std::cerr << "Warning, ignored search annotation: ";
444  ann->print(std::cerr);
445  std::cerr << std::endl;
447  }
448 
449  IntValBranch ann2ivalsel(AST::Node* ann, std::string& r0, std::string& r1,
450  Rnd rnd) {
451  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
452  if (s->id == "indomain_min") {
453  r0 = "="; r1 = "!=";
454  return INT_VAL_MIN();
455  }
456  if (s->id == "indomain_max") {
457  r0 = "="; r1 = "!=";
458  return INT_VAL_MAX();
459  }
460  if (s->id == "indomain_median") {
461  r0 = "="; r1 = "!=";
462  return INT_VAL_MED();
463  }
464  if (s->id == "indomain_split") {
465  r0 = "<="; r1 = ">";
466  return INT_VAL_SPLIT_MIN();
467  }
468  if (s->id == "indomain_reverse_split") {
469  r0 = ">"; r1 = "<=";
470  return INT_VAL_SPLIT_MAX();
471  }
472  if (s->id == "indomain_random") {
473  r0 = "="; r1 = "!=";
474  return INT_VAL_RND(rnd);
475  }
476  if (s->id == "indomain") {
477  r0 = "="; r1 = "=";
478  return INT_VALUES_MIN();
479  }
480  if (s->id == "indomain_middle") {
481  std::cerr << "Warning, replacing unsupported annotation "
482  << "indomain_middle with indomain_median" << std::endl;
483  r0 = "="; r1 = "!=";
484  return INT_VAL_MED();
485  }
486  if (s->id == "indomain_interval") {
487  std::cerr << "Warning, replacing unsupported annotation "
488  << "indomain_interval with indomain_split" << std::endl;
489  r0 = "<="; r1 = ">";
490  return INT_VAL_SPLIT_MIN();
491  }
492  }
493  std::cerr << "Warning, ignored search annotation: ";
494  ann->print(std::cerr);
495  std::cerr << std::endl;
496  r0 = "="; r1 = "!=";
497  return INT_VAL_MIN();
498  }
499 
501  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
502  if (s->id == "indomain_min")
503  return INT_ASSIGN_MIN();
504  if (s->id == "indomain_max")
505  return INT_ASSIGN_MAX();
506  if (s->id == "indomain_median")
507  return INT_ASSIGN_MED();
508  if (s->id == "indomain_random") {
509  return INT_ASSIGN_RND(rnd);
510  }
511  }
512  std::cerr << "Warning, ignored search annotation: ";
513  ann->print(std::cerr);
514  std::cerr << std::endl;
515  return INT_ASSIGN_MIN();
516  }
517 
519  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
520  if ((s->id == "input_order") ||
521  (s->id == "first_fail") ||
522  (s->id == "anti_first_fail") ||
523  (s->id == "smallest") ||
524  (s->id == "largest") ||
525  (s->id == "max_regret"))
527  if ((s->id == "occurrence") ||
528  (s->id == "most_constrained"))
530  if (s->id == "random")
532  if ((s->id == "afc_min") ||
533  (s->id == "afc_size_min"))
535  if ((s->id == "afc_max") ||
536  (s->id == "afc_size_max") ||
537  (s->id == "dom_w_deg"))
539  if ((s->id == "action_min") &&
540  (s->id == "action_size_min"))
542  if ((s->id == "action_max") ||
543  (s->id == "action_size_max"))
545  }
546  std::cerr << "Warning, ignored search annotation: ";
547  ann->print(std::cerr);
548  std::cerr << std::endl;
550  }
551 
552  BoolValBranch ann2bvalsel(AST::Node* ann, std::string& r0, std::string& r1,
553  Rnd rnd) {
554  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
555  if (s->id == "indomain_min") {
556  r0 = "="; r1 = "!=";
557  return BOOL_VAL_MIN();
558  }
559  if (s->id == "indomain_max") {
560  r0 = "="; r1 = "!=";
561  return BOOL_VAL_MAX();
562  }
563  if (s->id == "indomain_median") {
564  r0 = "="; r1 = "!=";
565  return BOOL_VAL_MIN();
566  }
567  if (s->id == "indomain_split") {
568  r0 = "<="; r1 = ">";
569  return BOOL_VAL_MIN();
570  }
571  if (s->id == "indomain_reverse_split") {
572  r0 = ">"; r1 = "<=";
573  return BOOL_VAL_MAX();
574  }
575  if (s->id == "indomain_random") {
576  r0 = "="; r1 = "!=";
577  return BOOL_VAL_RND(rnd);
578  }
579  if (s->id == "indomain") {
580  r0 = "="; r1 = "=";
581  return BOOL_VAL_MIN();
582  }
583  if (s->id == "indomain_middle") {
584  std::cerr << "Warning, replacing unsupported annotation "
585  << "indomain_middle with indomain_median" << std::endl;
586  r0 = "="; r1 = "!=";
587  return BOOL_VAL_MIN();
588  }
589  if (s->id == "indomain_interval") {
590  std::cerr << "Warning, replacing unsupported annotation "
591  << "indomain_interval with indomain_split" << std::endl;
592  r0 = "<="; r1 = ">";
593  return BOOL_VAL_MIN();
594  }
595  }
596  std::cerr << "Warning, ignored search annotation: ";
597  ann->print(std::cerr);
598  std::cerr << std::endl;
599  r0 = "="; r1 = "!=";
600  return BOOL_VAL_MIN();
601  }
602 
604  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
605  if ((s->id == "indomain_min") ||
606  (s->id == "indomain_median"))
607  return BOOL_ASSIGN_MIN();
608  if (s->id == "indomain_max")
609  return BOOL_ASSIGN_MAX();
610  if (s->id == "indomain_random") {
611  return BOOL_ASSIGN_RND(rnd);
612  }
613  }
614  std::cerr << "Warning, ignored search annotation: ";
615  ann->print(std::cerr);
616  std::cerr << std::endl;
617  return BOOL_ASSIGN_MIN();
618  }
619 
620 #ifdef GECODE_HAS_SET_VARS
621  SetVarBranch ann2svarsel(AST::Node* ann, Rnd rnd, double decay) {
622  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
623  if (s->id == "input_order")
624  return SET_VAR_NONE();
625  if (s->id == "first_fail")
626  return SET_VAR_SIZE_MIN();
627  if (s->id == "anti_first_fail")
628  return SET_VAR_SIZE_MAX();
629  if (s->id == "smallest")
630  return SET_VAR_MIN_MIN();
631  if (s->id == "largest")
632  return SET_VAR_MAX_MAX();
633  if (s->id == "afc_min")
634  return SET_VAR_AFC_MIN(decay);
635  if (s->id == "afc_max")
636  return SET_VAR_AFC_MAX(decay);
637  if (s->id == "afc_size_min")
638  return SET_VAR_AFC_SIZE_MIN(decay);
639  if (s->id == "afc_size_max")
640  return SET_VAR_AFC_SIZE_MAX(decay);
641  if (s->id == "action_min")
642  return SET_VAR_ACTION_MIN(decay);
643  if (s->id == "action_max")
644  return SET_VAR_ACTION_MAX(decay);
645  if (s->id == "action_size_min")
646  return SET_VAR_ACTION_SIZE_MIN(decay);
647  if (s->id == "action_size_max")
648  return SET_VAR_ACTION_SIZE_MAX(decay);
649  if (s->id == "random") {
650  return SET_VAR_RND(rnd);
651  }
652  }
653  std::cerr << "Warning, ignored search annotation: ";
654  ann->print(std::cerr);
655  std::cerr << std::endl;
656  return SET_VAR_NONE();
657  }
658 
659  SetValBranch ann2svalsel(AST::Node* ann, std::string r0, std::string r1,
660  Rnd rnd) {
661  (void) rnd;
662  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
663  if (s->id == "indomain_min") {
664  r0 = "in"; r1 = "not in";
665  return SET_VAL_MIN_INC();
666  }
667  if (s->id == "indomain_max") {
668  r0 = "in"; r1 = "not in";
669  return SET_VAL_MAX_INC();
670  }
671  if (s->id == "outdomain_min") {
672  r1 = "in"; r0 = "not in";
673  return SET_VAL_MIN_EXC();
674  }
675  if (s->id == "outdomain_max") {
676  r1 = "in"; r0 = "not in";
677  return SET_VAL_MAX_EXC();
678  }
679  }
680  std::cerr << "Warning, ignored search annotation: ";
681  ann->print(std::cerr);
682  std::cerr << std::endl;
683  r0 = "in"; r1 = "not in";
684  return SET_VAL_MIN_INC();
685  }
686 #endif
687 
688 #ifdef GECODE_HAS_FLOAT_VARS
690  double decay) {
691  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
692  if (s->id == "input_order")
694  if (s->id == "first_fail")
696  if (s->id == "anti_first_fail")
698  if (s->id == "smallest")
700  if (s->id == "largest")
702  if (s->id == "occurrence")
704  if (s->id == "most_constrained")
707  if (s->id == "random") {
709  }
710  if (s->id == "afc_min")
712  if (s->id == "afc_max")
714  if (s->id == "afc_size_min")
716  if (s->id == "afc_size_max")
718  if (s->id == "action_min")
720  if (s->id == "action_max")
722  if (s->id == "action_size_min")
724  if (s->id == "action_size_max")
726  }
727  std::cerr << "Warning, ignored search annotation: ";
728  ann->print(std::cerr);
729  std::cerr << std::endl;
731  }
732 
733  FloatValBranch ann2fvalsel(AST::Node* ann, std::string r0, std::string r1) {
734  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
735  if (s->id == "indomain_split") {
736  r0 = "<="; r1 = ">";
737  return FLOAT_VAL_SPLIT_MIN();
738  }
739  if (s->id == "indomain_reverse_split") {
740  r1 = "<="; r0 = ">";
741  return FLOAT_VAL_SPLIT_MAX();
742  }
743  }
744  std::cerr << "Warning, ignored search annotation: ";
745  ann->print(std::cerr);
746  std::cerr << std::endl;
747  r0 = "<="; r1 = ">";
748  return FLOAT_VAL_SPLIT_MIN();
749  }
750 
751 #endif
752 
754  public:
756  typedef std::unordered_set<TupleSet> TupleSetSet;
759 
761  typedef std::unordered_set<SharedArray<int> > IntSharedArraySet;
764 
766  typedef std::unordered_set<DFA> DFASet;
769 
772  };
773 
775  : Space(f),
776  _initData(NULL), _random(f._random),
777  _solveAnnotations(NULL), iv_boolalias(NULL),
779  step(f.step),
780 #endif
781  needAuxVars(f.needAuxVars) {
782  _optVar = f._optVar;
783  _optVarIsInt = f._optVarIsInt;
784  _method = f._method;
785  _lns = f._lns;
786  _lnsInitialSolution = f._lnsInitialSolution;
787  branchInfo = f.branchInfo;
788  iv.update(*this, f.iv);
789  iv_lns.update(*this, f.iv_lns);
790  intVarCount = f.intVarCount;
791 
792  if (needAuxVars) {
793  IntVarArgs iva;
794  for (int i=0; i<f.iv_aux.size(); i++) {
795  if (!f.iv_aux[i].assigned()) {
796  iva << IntVar();
797  iva[iva.size()-1].update(*this, f.iv_aux[i]);
798  }
799  }
800  iv_aux = IntVarArray(*this, iva);
801  }
802 
803  bv.update(*this, f.bv);
804  boolVarCount = f.boolVarCount;
805  if (needAuxVars) {
806  BoolVarArgs bva;
807  for (int i=0; i<f.bv_aux.size(); i++) {
808  if (!f.bv_aux[i].assigned()) {
809  bva << BoolVar();
810  bva[bva.size()-1].update(*this, f.bv_aux[i]);
811  }
812  }
813  bv_aux = BoolVarArray(*this, bva);
814  }
815 
816 #ifdef GECODE_HAS_SET_VARS
817  sv.update(*this, f.sv);
818  setVarCount = f.setVarCount;
819  if (needAuxVars) {
820  SetVarArgs sva;
821  for (int i=0; i<f.sv_aux.size(); i++) {
822  if (!f.sv_aux[i].assigned()) {
823  sva << SetVar();
824  sva[sva.size()-1].update(*this, f.sv_aux[i]);
825  }
826  }
827  sv_aux = SetVarArray(*this, sva);
828  }
829 #endif
830 #ifdef GECODE_HAS_FLOAT_VARS
831  fv.update(*this, f.fv);
832  floatVarCount = f.floatVarCount;
833  if (needAuxVars) {
834  FloatVarArgs fva;
835  for (int i=0; i<f.fv_aux.size(); i++) {
836  if (!f.fv_aux[i].assigned()) {
837  fva << FloatVar();
838  fva[fva.size()-1].update(*this, f.fv_aux[i]);
839  }
840  }
841  fv_aux = FloatVarArray(*this, fva);
842  }
843 #endif
844  }
845 
847  : _initData(new FlatZincSpaceInitData),
848  intVarCount(-1), boolVarCount(-1), floatVarCount(-1), setVarCount(-1),
849  _optVar(-1), _optVarIsInt(true), _lns(0), _lnsInitialSolution(0),
850  _random(random),
851  _solveAnnotations(NULL), needAuxVars(true) {
852  branchInfo.init();
853  }
854 
855  void
856  FlatZincSpace::init(int intVars, int boolVars,
857  int setVars, int floatVars) {
858  (void) setVars;
859  (void) floatVars;
860 
861  intVarCount = 0;
862  iv = IntVarArray(*this, intVars);
863  iv_introduced = std::vector<bool>(2*intVars);
864  iv_boolalias = alloc<int>(intVars+(intVars==0?1:0));
865  boolVarCount = 0;
866  bv = BoolVarArray(*this, boolVars);
867  bv_introduced = std::vector<bool>(2*boolVars);
868 #ifdef GECODE_HAS_SET_VARS
869  setVarCount = 0;
870  sv = SetVarArray(*this, setVars);
871  sv_introduced = std::vector<bool>(2*setVars);
872 #endif
873 #ifdef GECODE_HAS_FLOAT_VARS
874  floatVarCount = 0;
875  fv = FloatVarArray(*this, floatVars);
876  fv_introduced = std::vector<bool>(2*floatVars);
877 #endif
878  }
879 
880  void
882  if (vs->alias) {
883  iv[intVarCount++] = iv[vs->i];
884  } else {
885  IntSet dom(vs2is(vs));
886  if (dom.size()==0) {
887  fail();
888  return;
889  } else {
890  iv[intVarCount++] = IntVar(*this, dom);
891  }
892  }
893  iv_introduced[2*(intVarCount-1)] = vs->introduced;
894  iv_introduced[2*(intVarCount-1)+1] = vs->funcDep;
895  iv_boolalias[intVarCount-1] = -1;
896  }
897 
898  void
900  iv_boolalias[iv] = bv;
901  }
902  int
904  return iv_boolalias[iv];
905  }
906 
907  void
909  if (vs->alias) {
910  bv[boolVarCount++] = bv[vs->i];
911  } else {
912  bv[boolVarCount++] = BoolVar(*this, vs2bsl(vs), vs2bsh(vs));
913  }
915  bv_introduced[2*(boolVarCount-1)+1] = vs->funcDep;
916  }
917 
918 #ifdef GECODE_HAS_SET_VARS
919  void
921  if (vs->alias) {
922  sv[setVarCount++] = sv[vs->i];
923  } else if (vs->assigned) {
924  assert(vs->upperBound());
925  AST::SetLit* vsv = vs->upperBound.some();
926  if (vsv->interval) {
927  IntSet d(vsv->min, vsv->max);
928  sv[setVarCount++] = SetVar(*this, d, d);
929  } else {
930  int* is = heap.alloc<int>(static_cast<unsigned long int>(vsv->s.size()));
931  for (int i=vsv->s.size(); i--; )
932  is[i] = vsv->s[i];
933  IntSet d(is, vsv->s.size());
934  heap.free(is,static_cast<unsigned long int>(vsv->s.size()));
935  sv[setVarCount++] = SetVar(*this, d, d);
936  }
937  } else if (vs->upperBound()) {
938  AST::SetLit* vsv = vs->upperBound.some();
939  if (vsv->interval) {
940  IntSet d(vsv->min, vsv->max);
941  sv[setVarCount++] = SetVar(*this, IntSet::empty, d);
942  } else {
943  int* is = heap.alloc<int>(static_cast<unsigned long int>(vsv->s.size()));
944  for (int i=vsv->s.size(); i--; )
945  is[i] = vsv->s[i];
946  IntSet d(is, vsv->s.size());
947  heap.free(is,static_cast<unsigned long int>(vsv->s.size()));
948  sv[setVarCount++] = SetVar(*this, IntSet::empty, d);
949  }
950  } else {
951  sv[setVarCount++] = SetVar(*this, IntSet::empty,
954  }
955  sv_introduced[2*(setVarCount-1)] = vs->introduced;
956  sv_introduced[2*(setVarCount-1)+1] = vs->funcDep;
957  }
958 #else
959  void
961  throw FlatZinc::Error("Gecode", "set variables not supported");
962  }
963 #endif
964 
965 #ifdef GECODE_HAS_FLOAT_VARS
966  void
968  if (vs->alias) {
969  fv[floatVarCount++] = fv[vs->i];
970  } else {
971  double dmin, dmax;
972  if (vs->domain()) {
973  dmin = vs->domain.some().first;
974  dmax = vs->domain.some().second;
975  if (dmin > dmax) {
976  fail();
977  return;
978  }
979  } else {
980  dmin = Float::Limits::min;
981  dmax = Float::Limits::max;
982  }
983  fv[floatVarCount++] = FloatVar(*this, dmin, dmax);
984  }
986  fv_introduced[2*(floatVarCount-1)+1] = vs->funcDep;
987  }
988 #else
989  void
991  throw FlatZinc::Error("Gecode", "float variables not supported");
992  }
993 #endif
994 
995  namespace {
996  struct ConExprOrder {
997  bool operator() (ConExpr* ce0, ConExpr* ce1) {
998  return ce0->args->a.size() < ce1->args->a.size();
999  }
1000  };
1001  }
1002 
1003  void
1004  FlatZincSpace::postConstraints(std::vector<ConExpr*>& ces) {
1005  ConExprOrder ceo;
1006  std::sort(ces.begin(), ces.end(), ceo);
1007 
1008  for (unsigned int i=0; i<ces.size(); i++) {
1009  const ConExpr& ce = *ces[i];
1010  try {
1011  registry().post(*this, ce);
1012  } catch (Gecode::Exception& e) {
1013  throw FlatZinc::Error("Gecode", e.what());
1014  } catch (AST::TypeError& e) {
1015  throw FlatZinc::Error("Type error", e.what());
1016  }
1017  delete ces[i];
1018  ces[i] = NULL;
1019  }
1020  }
1021 
1022  void flattenAnnotations(AST::Array* ann, std::vector<AST::Node*>& out) {
1023  for (unsigned int i=0; i<ann->a.size(); i++) {
1024  if (ann->a[i]->isCall("seq_search")) {
1025  AST::Call* c = ann->a[i]->getCall();
1026  if (c->args->isArray())
1027  flattenAnnotations(c->args->getArray(), out);
1028  else
1029  out.push_back(c->args);
1030  } else {
1031  out.push_back(ann->a[i]);
1032  }
1033  }
1034  }
1035 
1036  void
1038  bool ignoreUnknown,
1039  std::ostream& err) {
1040  int seed = opt.seed();
1041  double decay = opt.decay();
1042  Rnd rnd(static_cast<unsigned int>(seed));
1043  TieBreak<IntVarBranch> def_int_varsel = INT_VAR_AFC_SIZE_MAX(0.99);
1044  IntBoolVarBranch def_intbool_varsel = INTBOOL_VAR_AFC_SIZE_MAX(0.99);
1045  IntValBranch def_int_valsel = INT_VAL_MIN();
1046  std::string def_int_rel_left = "=";
1047  std::string def_int_rel_right = "!=";
1048  TieBreak<BoolVarBranch> def_bool_varsel = BOOL_VAR_AFC_MAX(0.99);
1049  BoolValBranch def_bool_valsel = BOOL_VAL_MIN();
1050  std::string def_bool_rel_left = "=";
1051  std::string def_bool_rel_right = "!=";
1052 #ifdef GECODE_HAS_SET_VARS
1053  SetVarBranch def_set_varsel = SET_VAR_AFC_SIZE_MAX(0.99);
1054  SetValBranch def_set_valsel = SET_VAL_MIN_INC();
1055  std::string def_set_rel_left = "in";
1056  std::string def_set_rel_right = "not in";
1057 #endif
1058 #ifdef GECODE_HAS_FLOAT_VARS
1059  TieBreak<FloatVarBranch> def_float_varsel = FLOAT_VAR_SIZE_MIN();
1060  FloatValBranch def_float_valsel = FLOAT_VAL_SPLIT_MIN();
1061  std::string def_float_rel_left = "<=";
1062  std::string def_float_rel_right = ">";
1063 #endif
1064 
1065  std::vector<bool> iv_searched(iv.size());
1066  for (unsigned int i=iv.size(); i--;)
1067  iv_searched[i] = false;
1068  std::vector<bool> bv_searched(bv.size());
1069  for (unsigned int i=bv.size(); i--;)
1070  bv_searched[i] = false;
1071 #ifdef GECODE_HAS_SET_VARS
1072  std::vector<bool> sv_searched(sv.size());
1073  for (unsigned int i=sv.size(); i--;)
1074  sv_searched[i] = false;
1075 #endif
1076 #ifdef GECODE_HAS_FLOAT_VARS
1077  std::vector<bool> fv_searched(fv.size());
1078  for (unsigned int i=fv.size(); i--;)
1079  fv_searched[i] = false;
1080 #endif
1081 
1082  _lns = 0;
1083  if (ann) {
1084  std::vector<AST::Node*> flatAnn;
1085  if (ann->isArray()) {
1086  flattenAnnotations(ann->getArray() , flatAnn);
1087  } else {
1088  flatAnn.push_back(ann);
1089  }
1090 
1091  for (unsigned int i=0; i<flatAnn.size(); i++) {
1092  if (flatAnn[i]->isCall("restart_geometric")) {
1093  AST::Call* call = flatAnn[i]->getCall("restart_geometric");
1094  opt.restart(RM_GEOMETRIC);
1095  AST::Array* args = call->getArgs(2);
1096  opt.restart_base(args->a[0]->getFloat());
1097  opt.restart_scale(args->a[1]->getInt());
1098  } else if (flatAnn[i]->isCall("restart_luby")) {
1099  AST::Call* call = flatAnn[i]->getCall("restart_luby");
1100  opt.restart(RM_LUBY);
1101  opt.restart_scale(call->args->getInt());
1102  } else if (flatAnn[i]->isCall("restart_linear")) {
1103  AST::Call* call = flatAnn[i]->getCall("restart_linear");
1104  opt.restart(RM_LINEAR);
1105  opt.restart_scale(call->args->getInt());
1106  } else if (flatAnn[i]->isCall("restart_constant")) {
1107  AST::Call* call = flatAnn[i]->getCall("restart_constant");
1108  opt.restart(RM_CONSTANT);
1109  opt.restart_scale(call->args->getInt());
1110  } else if (flatAnn[i]->isCall("restart_none")) {
1111  opt.restart(RM_NONE);
1112  } else if (flatAnn[i]->isCall("relax_and_reconstruct")) {
1113  if (_lns != 0)
1114  throw FlatZinc::Error("FlatZinc",
1115  "Only one relax_and_reconstruct annotation allowed");
1116  AST::Call *call = flatAnn[i]->getCall("relax_and_reconstruct");
1117  AST::Array* args;
1118  if (call->args->getArray()->a.size()==2) {
1119  args = call->getArgs(2);
1120  } else {
1121  args = call->getArgs(3);
1122  }
1123  _lns = args->a[1]->getInt();
1124  AST::Array *vars = args->a[0]->getArray();
1125  int k=vars->a.size();
1126  for (int i=vars->a.size(); i--;)
1127  if (vars->a[i]->isInt())
1128  k--;
1129  iv_lns = IntVarArray(*this, k);
1130  k = 0;
1131  for (unsigned int i=0; i<vars->a.size(); i++) {
1132  if (vars->a[i]->isInt())
1133  continue;
1134  iv_lns[k++] = iv[vars->a[i]->getIntVar()];
1135  }
1136  if (args->a.size()==3) {
1137  AST::Array *initial = args->a[2]->getArray();
1138  _lnsInitialSolution = IntSharedArray(initial->a.size());
1139  for (unsigned int i=initial->a.size(); i--;)
1140  _lnsInitialSolution[i] = initial->a[i]->getInt();
1141  }
1142  } else if (flatAnn[i]->isCall("gecode_search")) {
1143  AST::Call* c = flatAnn[i]->getCall();
1144  branchWithPlugin(c->args);
1145  } else if (flatAnn[i]->isCall("int_search")) {
1146  AST::Call *call = flatAnn[i]->getCall("int_search");
1147  AST::Array *args = call->getArgs(4);
1148  AST::Array *vars = args->a[0]->getArray();
1149  int k=vars->a.size();
1150  for (int i=vars->a.size(); i--;)
1151  if (vars->a[i]->isInt())
1152  k--;
1153  IntVarArgs va(k);
1154  std::vector<std::string> names;
1155  k=0;
1156  for (unsigned int i=0; i<vars->a.size(); i++) {
1157  if (vars->a[i]->isInt())
1158  continue;
1159  va[k++] = iv[vars->a[i]->getIntVar()];
1160  iv_searched[vars->a[i]->getIntVar()] = true;
1161  names.push_back(vars->a[i]->getVarName());
1162  }
1163  std::string r0, r1;
1164  {
1165  BrancherGroup bg;
1166  branch(bg(*this), va,
1167  ann2ivarsel(args->a[1],rnd,decay),
1168  ann2ivalsel(args->a[2],r0,r1,rnd),
1169  nullptr,
1170  &varValPrint<IntVar>);
1171  branchInfo.add(bg,r0,r1,names);
1172  }
1173  } else if (flatAnn[i]->isCall("int_assign")) {
1174  AST::Call *call = flatAnn[i]->getCall("int_assign");
1175  AST::Array *args = call->getArgs(2);
1176  AST::Array *vars = args->a[0]->getArray();
1177  int k=vars->a.size();
1178  for (int i=vars->a.size(); i--;)
1179  if (vars->a[i]->isInt())
1180  k--;
1181  IntVarArgs va(k);
1182  k=0;
1183  for (unsigned int i=0; i<vars->a.size(); i++) {
1184  if (vars->a[i]->isInt())
1185  continue;
1186  va[k++] = iv[vars->a[i]->getIntVar()];
1187  iv_searched[vars->a[i]->getIntVar()] = true;
1188  }
1189  assign(*this, va, ann2asnivalsel(args->a[1],rnd), nullptr,
1190  &varValPrint<IntVar>);
1191  } else if (flatAnn[i]->isCall("bool_search")) {
1192  AST::Call *call = flatAnn[i]->getCall("bool_search");
1193  AST::Array *args = call->getArgs(4);
1194  AST::Array *vars = args->a[0]->getArray();
1195  int k=vars->a.size();
1196  for (int i=vars->a.size(); i--;)
1197  if (vars->a[i]->isBool())
1198  k--;
1199  BoolVarArgs va(k);
1200  k=0;
1201  std::vector<std::string> names;
1202  for (unsigned int i=0; i<vars->a.size(); i++) {
1203  if (vars->a[i]->isBool())
1204  continue;
1205  va[k++] = bv[vars->a[i]->getBoolVar()];
1206  bv_searched[vars->a[i]->getBoolVar()] = true;
1207  names.push_back(vars->a[i]->getVarName());
1208  }
1209 
1210  std::string r0, r1;
1211  {
1212  BrancherGroup bg;
1213  branch(bg(*this), va,
1214  ann2bvarsel(args->a[1],rnd,decay),
1215  ann2bvalsel(args->a[2],r0,r1,rnd),
1216  nullptr,
1217  &varValPrint<BoolVar>);
1218  branchInfo.add(bg,r0,r1,names);
1219  }
1220  } else if (flatAnn[i]->isCall("int_default_search")) {
1221  AST::Call *call = flatAnn[i]->getCall("int_default_search");
1222  AST::Array *args = call->getArgs(2);
1223  def_int_varsel = ann2ivarsel(args->a[0],rnd,decay);
1224  def_int_valsel = ann2ivalsel(args->a[1],
1225  def_int_rel_left,def_int_rel_right,rnd);
1226  } else if (flatAnn[i]->isCall("bool_default_search")) {
1227  AST::Call *call = flatAnn[i]->getCall("bool_default_search");
1228  AST::Array *args = call->getArgs(2);
1229  def_bool_varsel = ann2bvarsel(args->a[0],rnd,decay);
1230  def_bool_valsel = ann2bvalsel(args->a[1],
1231  def_bool_rel_left,def_bool_rel_right,
1232  rnd);
1233  } else if (flatAnn[i]->isCall("set_search")) {
1234 #ifdef GECODE_HAS_SET_VARS
1235  AST::Call *call = flatAnn[i]->getCall("set_search");
1236  AST::Array *args = call->getArgs(4);
1237  AST::Array *vars = args->a[0]->getArray();
1238  int k=vars->a.size();
1239  for (int i=vars->a.size(); i--;)
1240  if (vars->a[i]->isSet())
1241  k--;
1242  SetVarArgs va(k);
1243  k=0;
1244  std::vector<std::string> names;
1245  for (unsigned int i=0; i<vars->a.size(); i++) {
1246  if (vars->a[i]->isSet())
1247  continue;
1248  va[k++] = sv[vars->a[i]->getSetVar()];
1249  sv_searched[vars->a[i]->getSetVar()] = true;
1250  names.push_back(vars->a[i]->getVarName());
1251  }
1252  std::string r0, r1;
1253  {
1254  BrancherGroup bg;
1255  branch(bg(*this), va,
1256  ann2svarsel(args->a[1],rnd,decay),
1257  ann2svalsel(args->a[2],r0,r1,rnd),
1258  nullptr,
1259  &varValPrint<SetVar>);
1260  branchInfo.add(bg,r0,r1,names);
1261  }
1262 #else
1263  if (!ignoreUnknown) {
1264  err << "Warning, ignored search annotation: ";
1265  flatAnn[i]->print(err);
1266  err << std::endl;
1267  }
1268 #endif
1269  } else if (flatAnn[i]->isCall("set_default_search")) {
1270 #ifdef GECODE_HAS_SET_VARS
1271  AST::Call *call = flatAnn[i]->getCall("set_default_search");
1272  AST::Array *args = call->getArgs(2);
1273  def_set_varsel = ann2svarsel(args->a[0],rnd,decay);
1274  def_set_valsel = ann2svalsel(args->a[1],
1275  def_set_rel_left,def_set_rel_right,rnd);
1276 #else
1277  if (!ignoreUnknown) {
1278  err << "Warning, ignored search annotation: ";
1279  flatAnn[i]->print(err);
1280  err << std::endl;
1281  }
1282 #endif
1283  } else if (flatAnn[i]->isCall("float_default_search")) {
1284 #ifdef GECODE_HAS_FLOAT_VARS
1285  AST::Call *call = flatAnn[i]->getCall("float_default_search");
1286  AST::Array *args = call->getArgs(2);
1287  def_float_varsel = ann2fvarsel(args->a[0],rnd,decay);
1288  def_float_valsel = ann2fvalsel(args->a[1],
1289  def_float_rel_left,def_float_rel_right);
1290 #else
1291  if (!ignoreUnknown) {
1292  err << "Warning, ignored search annotation: ";
1293  flatAnn[i]->print(err);
1294  err << std::endl;
1295  }
1296 #endif
1297  } else if (flatAnn[i]->isCall("float_search")) {
1298 #ifdef GECODE_HAS_FLOAT_VARS
1299  AST::Call *call = flatAnn[i]->getCall("float_search");
1300  AST::Array *args = call->getArgs(5);
1301  AST::Array *vars = args->a[0]->getArray();
1302  int k=vars->a.size();
1303  for (int i=vars->a.size(); i--;)
1304  if (vars->a[i]->isFloat())
1305  k--;
1306  FloatVarArgs va(k);
1307  k=0;
1308  std::vector<std::string> names;
1309  for (unsigned int i=0; i<vars->a.size(); i++) {
1310  if (vars->a[i]->isFloat())
1311  continue;
1312  va[k++] = fv[vars->a[i]->getFloatVar()];
1313  fv_searched[vars->a[i]->getFloatVar()] = true;
1314  names.push_back(vars->a[i]->getVarName());
1315  }
1316  std::string r0, r1;
1317  {
1318  BrancherGroup bg;
1319  branch(bg(*this), va,
1320  ann2fvarsel(args->a[2],rnd,decay),
1321  ann2fvalsel(args->a[3],r0,r1),
1322  nullptr,
1323  &varValPrintF);
1324  branchInfo.add(bg,r0,r1,names);
1325  }
1326 #else
1327  if (!ignoreUnknown) {
1328  err << "Warning, ignored search annotation: ";
1329  flatAnn[i]->print(err);
1330  err << std::endl;
1331  }
1332 #endif
1333  } else {
1334  if (!ignoreUnknown) {
1335  err << "Warning, ignored search annotation: ";
1336  flatAnn[i]->print(err);
1337  err << std::endl;
1338  }
1339  }
1340  }
1341  }
1342  int introduced = 0;
1343  int funcdep = 0;
1344  int searched = 0;
1345  for (int i=iv.size(); i--;) {
1346  if (iv_searched[i] || (_method != SAT && _optVarIsInt && _optVar==i)) {
1347  searched++;
1348  } else if (iv_introduced[2*i]) {
1349  if (iv_introduced[2*i+1]) {
1350  funcdep++;
1351  } else {
1352  introduced++;
1353  }
1354  }
1355  }
1356  std::vector<std::string> iv_sol_names(iv.size()-(introduced+funcdep+searched));
1357  IntVarArgs iv_sol(iv.size()-(introduced+funcdep+searched));
1358  std::vector<std::string> iv_tmp_names(introduced);
1359  IntVarArgs iv_tmp(introduced);
1360  for (int i=iv.size(), j=0, k=0; i--;) {
1361  if (iv_searched[i] || (_method != SAT && _optVarIsInt && _optVar==i))
1362  continue;
1363  if (iv_introduced[2*i]) {
1364  if (!iv_introduced[2*i+1]) {
1365  iv_tmp_names[j] = p.intVarName(i);
1366  iv_tmp[j++] = iv[i];
1367  }
1368  } else {
1369  iv_sol_names[k] = p.intVarName(i);
1370  iv_sol[k++] = iv[i];
1371  }
1372  }
1373 
1374  introduced = 0;
1375  funcdep = 0;
1376  searched = 0;
1377  for (int i=bv.size(); i--;) {
1378  if (bv_searched[i]) {
1379  searched++;
1380  } else if (bv_introduced[2*i]) {
1381  if (bv_introduced[2*i+1]) {
1382  funcdep++;
1383  } else {
1384  introduced++;
1385  }
1386  }
1387  }
1388  std::vector<std::string> bv_sol_names(bv.size()-(introduced+funcdep+searched));
1389  BoolVarArgs bv_sol(bv.size()-(introduced+funcdep+searched));
1390  BoolVarArgs bv_tmp(introduced);
1391  std::vector<std::string> bv_tmp_names(introduced);
1392  for (int i=bv.size(), j=0, k=0; i--;) {
1393  if (bv_searched[i])
1394  continue;
1395  if (bv_introduced[2*i]) {
1396  if (!bv_introduced[2*i+1]) {
1397  bv_tmp_names[j] = p.boolVarName(i);
1398  bv_tmp[j++] = bv[i];
1399  }
1400  } else {
1401  bv_sol_names[k] = p.boolVarName(i);
1402  bv_sol[k++] = bv[i];
1403  }
1404  }
1405 
1406  if (iv_sol.size() > 0 && bv_sol.size() > 0) {
1407  branch(*this, iv_sol, bv_sol, def_intbool_varsel, def_int_valsel);
1408  } else if (iv_sol.size() > 0) {
1409  BrancherGroup bg;
1410  branch(bg(*this), iv_sol, def_int_varsel, def_int_valsel, nullptr,
1411  &varValPrint<IntVar>);
1412  branchInfo.add(bg,def_int_rel_left,def_int_rel_right,iv_sol_names);
1413  } else if (bv_sol.size() > 0) {
1414  BrancherGroup bg;
1415  branch(bg(*this), bv_sol, def_bool_varsel, def_bool_valsel, nullptr,
1416  &varValPrint<BoolVar>);
1417  branchInfo.add(bg,def_bool_rel_left,def_bool_rel_right,bv_sol_names);
1418  }
1419 #ifdef GECODE_HAS_FLOAT_VARS
1420  introduced = 0;
1421  funcdep = 0;
1422  searched = 0;
1423  for (int i=fv.size(); i--;) {
1424  if (fv_searched[i] || (_method != SAT && !_optVarIsInt && _optVar==i)) {
1425  searched++;
1426  } else if (fv_introduced[2*i]) {
1427  if (fv_introduced[2*i+1]) {
1428  funcdep++;
1429  } else {
1430  introduced++;
1431  }
1432  }
1433  }
1434  std::vector<std::string> fv_sol_names(fv.size()-(introduced+funcdep+searched));
1435  FloatVarArgs fv_sol(fv.size()-(introduced+funcdep+searched));
1436  FloatVarArgs fv_tmp(introduced);
1437  std::vector<std::string> fv_tmp_names(introduced);
1438  for (int i=fv.size(), j=0, k=0; i--;) {
1439  if (fv_searched[i] || (_method != SAT && !_optVarIsInt && _optVar==i))
1440  continue;
1441  if (fv_introduced[2*i]) {
1442  if (!fv_introduced[2*i+1]) {
1443  fv_tmp_names[j] = p.floatVarName(i);
1444  fv_tmp[j++] = fv[i];
1445  }
1446  } else {
1447  fv_sol_names[k] = p.floatVarName(i);
1448  fv_sol[k++] = fv[i];
1449  }
1450  }
1451 
1452  if (fv_sol.size() > 0) {
1453  BrancherGroup bg;
1454  branch(bg(*this), fv_sol, def_float_varsel, def_float_valsel, nullptr,
1455  &varValPrintF);
1456  branchInfo.add(bg,def_float_rel_left,def_float_rel_right,fv_sol_names);
1457  }
1458 #endif
1459 #ifdef GECODE_HAS_SET_VARS
1460  introduced = 0;
1461  funcdep = 0;
1462  searched = 0;
1463  for (int i=sv.size(); i--;) {
1464  if (sv_searched[i]) {
1465  searched++;
1466  } else if (sv_introduced[2*i]) {
1467  if (sv_introduced[2*i+1]) {
1468  funcdep++;
1469  } else {
1470  introduced++;
1471  }
1472  }
1473  }
1474  std::vector<std::string> sv_sol_names(sv.size()-(introduced+funcdep+searched));
1475  SetVarArgs sv_sol(sv.size()-(introduced+funcdep+searched));
1476  SetVarArgs sv_tmp(introduced);
1477  std::vector<std::string> sv_tmp_names(introduced);
1478  for (int i=sv.size(), j=0, k=0; i--;) {
1479  if (sv_searched[i])
1480  continue;
1481  if (sv_introduced[2*i]) {
1482  if (!sv_introduced[2*i+1]) {
1483  sv_tmp_names[j] = p.setVarName(i);
1484  sv_tmp[j++] = sv[i];
1485  }
1486  } else {
1487  sv_sol_names[k] = p.setVarName(i);
1488  sv_sol[k++] = sv[i];
1489  }
1490  }
1491 
1492  if (sv_sol.size() > 0) {
1493  BrancherGroup bg;
1494  branch(bg(*this), sv_sol, def_set_varsel, def_set_valsel, nullptr,
1495  &varValPrint<SetVar>);
1496  branchInfo.add(bg,def_set_rel_left,def_set_rel_right,sv_sol_names);
1497 
1498  }
1499 #endif
1500  iv_aux = IntVarArray(*this, iv_tmp);
1501  bv_aux = BoolVarArray(*this, bv_tmp);
1502  int n_aux = iv_aux.size() + bv_aux.size();
1503 #ifdef GECODE_HAS_SET_VARS
1504  sv_aux = SetVarArray(*this, sv_tmp);
1505  n_aux += sv_aux.size();
1506 #endif
1507 #ifdef GECODE_HAS_FLOAT_VARS
1508  fv_aux = FloatVarArray(*this, fv_tmp);
1509  n_aux += fv_aux.size();
1510 #endif
1511 
1512  if (n_aux > 0) {
1513  if (_method == SAT) {
1514  AuxVarBrancher::post(*this, def_int_varsel, def_int_valsel,
1515  def_bool_varsel, def_bool_valsel
1516 #ifdef GECODE_HAS_SET_VARS
1517  , def_set_varsel, def_set_valsel
1518 #endif
1519 #ifdef GECODE_HAS_FLOAT_VARS
1520  , def_float_varsel, def_float_valsel
1521 #endif
1522  );
1523  } else {
1524  {
1525  BrancherGroup bg;
1526  branch(bg(*this),iv_aux,def_int_varsel,def_int_valsel, nullptr,
1527  &varValPrint<IntVar>);
1528  branchInfo.add(bg,def_int_rel_left,def_int_rel_right,iv_tmp_names);
1529  }
1530  {
1531  BrancherGroup bg;
1532  branch(bg(*this),bv_aux,def_bool_varsel,def_bool_valsel, nullptr,
1533  &varValPrint<BoolVar>);
1534  branchInfo.add(bg,def_bool_rel_left,def_bool_rel_right,bv_tmp_names);
1535  }
1536  #ifdef GECODE_HAS_SET_VARS
1537  {
1538  BrancherGroup bg;
1539  branch(bg(*this),sv_aux,def_set_varsel,def_set_valsel, nullptr,
1540  &varValPrint<SetVar>);
1541  branchInfo.add(bg,def_set_rel_left,def_set_rel_right,sv_tmp_names);
1542  }
1543  #endif
1544  #ifdef GECODE_HAS_FLOAT_VARS
1545  {
1546  BrancherGroup bg;
1547  branch(bg(*this),fv_aux,def_float_varsel,def_float_valsel, nullptr,
1548  &varValPrintF);
1549  branchInfo.add(bg,def_float_rel_left,def_float_rel_right,fv_tmp_names);
1550  }
1551  #endif
1552 
1553  }
1554  }
1555 
1556  if (_method == MIN) {
1557  if (_optVarIsInt) {
1558  std::vector<std::string> names(1);
1559  names[0] = p.intVarName(_optVar);
1560  BrancherGroup bg;
1561  branch(bg(*this), iv[_optVar], INT_VAL_MIN(),
1562  &varValPrint<IntVar>);
1563  branchInfo.add(bg,"=","!=",names);
1564  } else {
1565 #ifdef GECODE_HAS_FLOAT_VARS
1566  std::vector<std::string> names(1);
1567  names[0] = p.floatVarName(_optVar);
1568  BrancherGroup bg;
1569  branch(bg(*this), fv[_optVar], FLOAT_VAL_SPLIT_MIN(),
1570  &varValPrintF);
1571  branchInfo.add(bg,"<=",">",names);
1572 #endif
1573  }
1574  } else if (_method == MAX) {
1575  if (_optVarIsInt) {
1576  std::vector<std::string> names(1);
1577  names[0] = p.intVarName(_optVar);
1578  BrancherGroup bg;
1579  branch(bg(*this), iv[_optVar], INT_VAL_MAX(),
1580  &varValPrint<IntVar>);
1581  branchInfo.add(bg,"=","!=",names);
1582  } else {
1583 #ifdef GECODE_HAS_FLOAT_VARS
1584  std::vector<std::string> names(1);
1585  names[0] = p.floatVarName(_optVar);
1586  BrancherGroup bg;
1587  branch(bg(*this), fv[_optVar], FLOAT_VAL_SPLIT_MAX(),
1588  &varValPrintF);
1589  branchInfo.add(bg,"<=",">",names);
1590 #endif
1591  }
1592  }
1593 
1594  }
1595 
1596  AST::Array*
1598  return _solveAnnotations;
1599  }
1600 
1601  void
1603  _method = SAT;
1604  _solveAnnotations = ann;
1605  }
1606 
1607  void
1608  FlatZincSpace::minimize(int var, bool isInt, AST::Array* ann) {
1609  _method = MIN;
1610  _optVar = var;
1611  _optVarIsInt = isInt;
1612  _solveAnnotations = ann;
1613  }
1614 
1615  void
1616  FlatZincSpace::maximize(int var, bool isInt, AST::Array* ann) {
1617  _method = MAX;
1618  _optVar = var;
1619  _optVarIsInt = isInt;
1620  _solveAnnotations = ann;
1621  }
1622 
1624  delete _initData;
1625  delete _solveAnnotations;
1626  }
1627 
1628 #ifdef GECODE_HAS_GIST
1629 
1633  template<class Engine>
1634  class GistEngine {
1635  };
1636 
1638  template<typename S>
1639  class GistEngine<DFS<S> > {
1640  public:
1641  static void explore(S* root, const FlatZincOptions& opt,
1644  o.c_d = opt.c_d(); o.a_d = opt.a_d();
1645  o.inspect.click(i);
1646  o.inspect.compare(c);
1647  (void) Gecode::Gist::dfs(root, o);
1648  }
1649  };
1650 
1652  template<typename S>
1653  class GistEngine<BAB<S> > {
1654  public:
1655  static void explore(S* root, const FlatZincOptions& opt,
1658  o.c_d = opt.c_d(); o.a_d = opt.a_d();
1659  o.inspect.click(i);
1660  o.inspect.compare(c);
1661  (void) Gecode::Gist::bab(root, o);
1662  }
1663  };
1664 
1666  template<class S>
1669  private:
1670  const Printer& p;
1671  public:
1673  FZPrintingInspector(const Printer& p0);
1675  virtual void inspect(const Space& node);
1677  virtual void finalize(void);
1678  };
1679 
1680  template<class S>
1682  : TextOutput("Gecode/FlatZinc"), p(p0) {}
1683 
1684  template<class S>
1685  void
1687  init();
1688  dynamic_cast<const S&>(node).print(getStream(), p);
1689  getStream() << std::endl;
1690  }
1691 
1692  template<class S>
1693  void
1696  }
1697 
1698  template<class S>
1700  : public Gecode::Gist::VarComparator<S> {
1701  private:
1702  const Printer& p;
1703  public:
1705  FZPrintingComparator(const Printer& p0);
1706 
1708  virtual void compare(const Space& s0, const Space& s1);
1709  };
1710 
1711  template<class S>
1713  : Gecode::Gist::VarComparator<S>("Gecode/FlatZinc"), p(p0) {}
1714 
1715  template<class S>
1716  void
1718  this->init();
1719  try {
1720  dynamic_cast<const S&>(s0).compare(dynamic_cast<const S&>(s1),
1721  this->getStream(), p);
1722  } catch (Exception& e) {
1723  this->getStream() << "Exception: " << e.what();
1724  }
1725  this->getStream() << std::endl;
1726  }
1727 
1728 #endif
1729 
1730  template<template<class> class Engine>
1731  void
1732  FlatZincSpace::runEngine(std::ostream& out, const Printer& p,
1733  const FlatZincOptions& opt, Support::Timer& t_total) {
1734  if (opt.restart()==RM_NONE) {
1735  runMeta<Engine,Driver::EngineToMeta>(out,p,opt,t_total);
1736  } else {
1737  runMeta<Engine,RBS>(out,p,opt,t_total);
1738  }
1739  }
1740 
1741 #ifdef GECODE_HAS_CPPROFILER
1742 
1744  public:
1745  const Printer& p;
1746  FlatZincGetInfo(const Printer& printer) : p(printer) {}
1747  virtual std::string
1748  getInfo(const Space& space) const {
1749  std::stringstream ss;
1750  if (const FlatZincSpace* fz_space = dynamic_cast<const FlatZincSpace*>(&space)) {
1751  ss << "{\n\t\"domains\": \"";
1752  ss << fz_space->getDomains(p);
1753  ss << "\"\n}";
1754  }
1755  return ss.str();
1756  }
1758  };
1759 
1760  void printIntVar(std::ostream& os, const std::string name, const Int::IntView& x) {
1761  os << "var ";
1762  if (x.assigned()) {
1763  os << "int: " << name << " = " << x.val() << ";";
1764  } else if (x.range()) {
1765  os << x.min() << ".." << x.max() << ": " << name << ";";
1766  } else {
1767  os << "array_union([";
1769  while (true) {
1770  os << r.min() << ".." << r.max();
1771  ++r;
1772  if (!r()) break;
1773  os << ',';
1774  }
1775  os << "]): " << name << ";";
1776  }
1777  os << "\n";
1778  }
1779  void printBoolVar(std::ostream& os, const std::string name, const BoolVar& b) {
1780  os << "var bool: " << name;
1781  if(b.assigned())
1782  os << " = " << (b.val() ? "true" : "false");
1783  os << ";\n";
1784  }
1785 #ifdef GECODE_HAS_FLOAT_VARS
1786  void printFloatVar(std::ostream& os, const std::string name, const Float::FloatView& f) {
1787  os << "var ";
1788  if(f.assigned())
1789  os << "float: " << name << " = " << f.med() << ";";
1790  else
1791  os << f.min() << ".." << f.max() << ": " << name << ";";
1792  os << "\n";
1793  }
1794 #endif
1795  std::string FlatZincSpace::getDomains(const Printer& p) const {
1796  std::ostringstream oss;
1797 
1798  for (int i = 0; i < iv.size(); i++)
1799  printIntVar(oss, p.intVarName(i), iv[i]);
1800 
1801  for (int i = 0; i < bv.size(); i++)
1802  printBoolVar(oss, p.boolVarName(i), bv[i]);
1803 
1804 #ifdef GECODE_HAS_FLOAT_VARS
1805  for (int i = 0; i < fv.size(); i++)
1806  printFloatVar(oss, p.floatVarName(i), fv[i]);
1807 #endif
1808 #ifdef GECODE_HAS_SET_VARS
1809  for (int i = 0; i < sv.size(); i++)
1810  oss << "var " << sv[i] << ": " << p.setVarName(i) << ";" << std::endl;
1811 #endif
1812 
1813  return oss.str();
1814  }
1815 
1816 #endif
1817 
1818  template<template<class> class Engine,
1819  template<class,template<class> class> class Meta>
1820  void
1821  FlatZincSpace::runMeta(std::ostream& out, const Printer& p,
1822  const FlatZincOptions& opt, Support::Timer& t_total) {
1823 #ifdef GECODE_HAS_GIST
1824  if (opt.mode() == SM_GIST) {
1827  (void) GistEngine<Engine<FlatZincSpace> >::explore(this,opt,&pi,&pc);
1828  return;
1829  }
1830 #endif
1831  StatusStatistics sstat;
1832  unsigned int n_p = 0;
1833  Support::Timer t_solve;
1834  t_solve.start();
1835  if (status(sstat) != SS_FAILED) {
1836  n_p = PropagatorGroup::all.size(*this);
1837  }
1838  Search::Options o;
1839  o.stop = Driver::CombinedStop::create(opt.node(), opt.fail(), opt.time(),
1840  true);
1841  o.c_d = opt.c_d();
1842  o.a_d = opt.a_d();
1843 
1844 #ifdef GECODE_HAS_CPPROFILER
1845 
1846  if (opt.mode() == SM_CPPROFILER) {
1847  FlatZincGetInfo* getInfo = nullptr;
1848  if (opt.profiler_info())
1849  getInfo = new FlatZincGetInfo(p);
1850  o.tracer = new CPProfilerSearchTracer(opt.profiler_id(),
1851  opt.name(), opt.profiler_port(),
1852  getInfo);
1853  }
1854 
1855 #endif
1856 
1857 #ifdef GECODE_HAS_FLOAT_VARS
1858  step = opt.step();
1859 #endif
1860  o.threads = opt.threads();
1861  o.nogoods_limit = opt.nogoods() ? opt.nogoods_limit() : 0;
1862  o.cutoff = new Search::CutoffAppend(new Search::CutoffConstant(0), 1, Driver::createCutoff(opt));
1863  if (opt.interrupt())
1865  {
1866  Meta<FlatZincSpace,Engine> se(this,o);
1867  int noOfSolutions = opt.solutions();
1868  if (noOfSolutions == -1) {
1869  noOfSolutions = (_method == SAT) ? 1 : 0;
1870  }
1871  bool printAll = _method == SAT || opt.allSolutions() || noOfSolutions != 0;
1872  int findSol = noOfSolutions;
1873  FlatZincSpace* sol = NULL;
1874  while (FlatZincSpace* next_sol = se.next()) {
1875  delete sol;
1876  sol = next_sol;
1877  if (printAll) {
1878  sol->print(out, p);
1879  out << "----------" << std::endl;
1880  }
1881  if (--findSol==0)
1882  goto stopped;
1883  }
1884  if (sol && !printAll) {
1885  sol->print(out, p);
1886  out << "----------" << std::endl;
1887  }
1888  if (!se.stopped()) {
1889  if (sol) {
1890  out << "==========" << std::endl;
1891  } else {
1892  out << "=====UNSATISFIABLE=====" << std::endl;
1893  }
1894  } else if (!sol) {
1895  out << "=====UNKNOWN=====" << std::endl;
1896  }
1897  delete sol;
1898  stopped:
1899  if (opt.interrupt())
1901  if (opt.mode() == SM_STAT) {
1902  Gecode::Search::Statistics stat = se.statistics();
1903  double totalTime = (t_total.stop() / 1000.0);
1904  double solveTime = (t_solve.stop() / 1000.0);
1905  double initTime = totalTime - solveTime;
1906  out << std::endl
1907  << "%%%mzn-stat: initTime=" << initTime
1908  << std::endl;
1909  out << "%%%mzn-stat: solveTime=" << solveTime
1910  << std::endl;
1911  out << "%%%mzn-stat: solutions="
1912  << std::abs(noOfSolutions - findSol) << std::endl
1913  << "%%%mzn-stat: variables="
1914  << (intVarCount + boolVarCount + setVarCount) << std::endl
1915  << "%%%mzn-stat: propagators=" << n_p << std::endl
1916  << "%%%mzn-stat: propagations=" << sstat.propagate+stat.propagate << std::endl
1917  << "%%%mzn-stat: nodes=" << stat.node << std::endl
1918  << "%%%mzn-stat: failures=" << stat.fail << std::endl
1919  << "%%%mzn-stat: restarts=" << stat.restart << std::endl
1920  << "%%%mzn-stat: peakDepth=" << stat.depth << std::endl
1921  << "%%%mzn-stat-end" << std::endl
1922  << std::endl;
1923  }
1924  }
1925  delete o.stop;
1926  delete o.tracer;
1927  }
1928 
1929 #ifdef GECODE_HAS_QT
1930  void
1931  FlatZincSpace::branchWithPlugin(AST::Node* ann) {
1932  if (AST::Call* c = dynamic_cast<AST::Call*>(ann)) {
1933  QString pluginName(c->id.c_str());
1934  if (QLibrary::isLibrary(pluginName+".dll")) {
1935  pluginName += ".dll";
1936  } else if (QLibrary::isLibrary(pluginName+".dylib")) {
1937  pluginName = "lib" + pluginName + ".dylib";
1938  } else if (QLibrary::isLibrary(pluginName+".so")) {
1939  // Must check .so after .dylib so that Mac OS uses .dylib
1940  pluginName = "lib" + pluginName + ".so";
1941  }
1942  QPluginLoader pl(pluginName);
1943  QObject* plugin_o = pl.instance();
1944  if (!plugin_o) {
1945  throw FlatZinc::Error("FlatZinc",
1946  "Error loading plugin "+pluginName.toStdString()+
1947  ": "+pl.errorString().toStdString());
1948  }
1949  BranchPlugin* pb = qobject_cast<BranchPlugin*>(plugin_o);
1950  if (!pb) {
1951  throw FlatZinc::Error("FlatZinc",
1952  "Error loading plugin "+pluginName.toStdString()+
1953  ": does not contain valid PluginBrancher");
1954  }
1955  pb->branch(*this, c);
1956  }
1957  }
1958 #else
1959  void
1960  FlatZincSpace::branchWithPlugin(AST::Node*) {
1961  throw FlatZinc::Error("FlatZinc",
1962  "Branching with plugins not supported (requires Qt support)");
1963  }
1964 #endif
1965 
1966  void
1967  FlatZincSpace::run(std::ostream& out, const Printer& p,
1968  const FlatZincOptions& opt, Support::Timer& t_total) {
1969  switch (_method) {
1970  case MIN:
1971  case MAX:
1972  runEngine<BAB>(out,p,opt,t_total);
1973  break;
1974  case SAT:
1975  runEngine<DFS>(out,p,opt,t_total);
1976  break;
1977  }
1978  }
1979 
1980  void
1982  if (_optVarIsInt) {
1983  if (_method == MIN)
1984  rel(*this, iv[_optVar], IRT_LE,
1985  static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
1986  else if (_method == MAX)
1987  rel(*this, iv[_optVar], IRT_GR,
1988  static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
1989  } else {
1990 #ifdef GECODE_HAS_FLOAT_VARS
1991  if (_method == MIN)
1992  rel(*this, fv[_optVar], FRT_LE,
1993  static_cast<const FlatZincSpace*>(&s)->fv[_optVar].val()-step);
1994  else if (_method == MAX)
1995  rel(*this, fv[_optVar], FRT_GR,
1996  static_cast<const FlatZincSpace*>(&s)->fv[_optVar].val()+step);
1997 #endif
1998  }
1999  }
2000 
2001  bool
2003  if ((mi.type() == MetaInfo::RESTART) && (mi.restart() != 0) &&
2004  (_lns > 0) && (mi.last()==NULL) && (_lnsInitialSolution.size()>0)) {
2005  for (unsigned int i=iv_lns.size(); i--;) {
2006  if (_random(99) <= _lns) {
2007  rel(*this, iv_lns[i], IRT_EQ, _lnsInitialSolution[i]);
2008  }
2009  }
2010  return false;
2011  } else if ((mi.type() == MetaInfo::RESTART) && (mi.restart() != 0) &&
2012  (_lns > 0) && mi.last()) {
2013  const FlatZincSpace& last =
2014  static_cast<const FlatZincSpace&>(*mi.last());
2015  for (unsigned int i=iv_lns.size(); i--;) {
2016  if (_random(99) <= _lns) {
2017  rel(*this, iv_lns[i], IRT_EQ, last.iv_lns[i]);
2018  }
2019  }
2020  return false;
2021  }
2022  return true;
2023  }
2024 
2025  Space*
2027  return new FlatZincSpace(*this);
2028  }
2029 
2032  return _method;
2033  }
2034 
2035  int
2037  return _optVar;
2038  }
2039 
2040  bool
2042  return _optVarIsInt;
2043  }
2044 
2045  void
2046  FlatZincSpace::print(std::ostream& out, const Printer& p) const {
2047  p.print(out, iv, bv
2048 #ifdef GECODE_HAS_SET_VARS
2049  , sv
2050 #endif
2051 #ifdef GECODE_HAS_FLOAT_VARS
2052  , fv
2053 #endif
2054  );
2055  }
2056 
2057  void
2058  FlatZincSpace::compare(const Space& s, std::ostream& out) const {
2059  (void) s; (void) out;
2060 #ifdef GECODE_HAS_GIST
2061  const FlatZincSpace& fs = dynamic_cast<const FlatZincSpace&>(s);
2062  for (int i = 0; i < iv.size(); ++i) {
2063  std::stringstream ss;
2064  ss << "iv[" << i << "]";
2065  std::string result(Gecode::Gist::Comparator::compare(ss.str(), iv[i],
2066  fs.iv[i]));
2067  if (result.length() > 0) out << result << std::endl;
2068  }
2069  for (int i = 0; i < bv.size(); ++i) {
2070  std::stringstream ss;
2071  ss << "bv[" << i << "]";
2072  std::string result(Gecode::Gist::Comparator::compare(ss.str(), bv[i],
2073  fs.bv[i]));
2074  if (result.length() > 0) out << result << std::endl;
2075  }
2076 #ifdef GECODE_HAS_SET_VARS
2077  for (int i = 0; i < sv.size(); ++i) {
2078  std::stringstream ss;
2079  ss << "sv[" << i << "]";
2080  std::string result(Gecode::Gist::Comparator::compare(ss.str(), sv[i],
2081  fs.sv[i]));
2082  if (result.length() > 0) out << result << std::endl;
2083  }
2084 #endif
2085 #ifdef GECODE_HAS_FLOAT_VARS
2086  for (int i = 0; i < fv.size(); ++i) {
2087  std::stringstream ss;
2088  ss << "fv[" << i << "]";
2089  std::string result(Gecode::Gist::Comparator::compare(ss.str(), fv[i],
2090  fs.fv[i]));
2091  if (result.length() > 0) out << result << std::endl;
2092  }
2093 #endif
2094 #endif
2095  }
2096 
2097  void
2098  FlatZincSpace::compare(const FlatZincSpace& s, std::ostream& out,
2099  const Printer& p) const {
2100  p.printDiff(out, iv, s.iv, bv, s.bv
2101 #ifdef GECODE_HAS_SET_VARS
2102  , sv, s.sv
2103 #endif
2104 #ifdef GECODE_HAS_FLOAT_VARS
2105  , fv, s.fv
2106 #endif
2107  );
2108  }
2109 
2110  void
2112  p.shrinkArrays(*this, _optVar, _optVarIsInt, iv, bv
2113 #ifdef GECODE_HAS_SET_VARS
2114  , sv
2115 #endif
2116 #ifdef GECODE_HAS_FLOAT_VARS
2117  , fv
2118 #endif
2119  );
2120  }
2121 
2122  IntArgs
2124  AST::Array* a = arg->getArray();
2125  IntArgs ia(a->a.size()+offset);
2126  for (int i=offset; i--;)
2127  ia[i] = 0;
2128  for (int i=a->a.size(); i--;)
2129  ia[i+offset] = a->a[i]->getInt();
2130  return ia;
2131  }
2132  TupleSet
2133  FlatZincSpace::arg2tupleset(const IntArgs& a, int noOfVars) {
2134  int noOfTuples = a.size() == 0 ? 0 : (a.size()/noOfVars);
2135 
2136  // Build TupleSet
2137  TupleSet ts(noOfVars);
2138  for (int i=0; i<noOfTuples; i++) {
2139  IntArgs t(noOfVars);
2140  for (int j=0; j<noOfVars; j++) {
2141  t[j] = a[i*noOfVars+j];
2142  }
2143  ts.add(t);
2144  }
2145  ts.finalize();
2146 
2147  if (_initData) {
2148  FlatZincSpaceInitData::TupleSetSet::iterator it = _initData->tupleSetSet.find(ts);
2149  if (it != _initData->tupleSetSet.end()) {
2150  return *it;
2151  }
2152  _initData->tupleSetSet.insert(ts);
2153  }
2154 
2155 
2156  return ts;
2157  }
2160  IntArgs ia(arg2intargs(arg,offset));
2161  SharedArray<int> sia(ia);
2162  if (_initData) {
2163  FlatZincSpaceInitData::IntSharedArraySet::iterator it = _initData->intSharedArraySet.find(sia);
2164  if (it != _initData->intSharedArraySet.end()) {
2165  return *it;
2166  }
2167  _initData->intSharedArraySet.insert(sia);
2168  }
2169 
2170  return sia;
2171  }
2172  IntArgs
2174  AST::Array* a = arg->getArray();
2175  IntArgs ia(a->a.size()+offset);
2176  for (int i=offset; i--;)
2177  ia[i] = 0;
2178  for (int i=a->a.size(); i--;)
2179  ia[i+offset] = a->a[i]->getBool();
2180  return ia;
2181  }
2184  IntArgs ia(arg2boolargs(arg,offset));
2185  SharedArray<int> sia(ia);
2186  if (_initData) {
2187  FlatZincSpaceInitData::IntSharedArraySet::iterator it = _initData->intSharedArraySet.find(sia);
2188  if (it != _initData->intSharedArraySet.end()) {
2189  return *it;
2190  }
2191  _initData->intSharedArraySet.insert(sia);
2192  }
2193 
2194  return sia;
2195  }
2196  IntSet
2198  AST::SetLit* sl = n->getSet();
2199  IntSet d;
2200  if (sl->interval) {
2201  d = IntSet(sl->min, sl->max);
2202  } else {
2203  Region re;
2204  int* is = re.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
2205  for (int i=sl->s.size(); i--; )
2206  is[i] = sl->s[i];
2207  d = IntSet(is, sl->s.size());
2208  }
2209  return d;
2210  }
2211  IntSetArgs
2213  AST::Array* a = arg->getArray();
2214  if (a->a.size() == 0) {
2215  IntSetArgs emptyIa(0);
2216  return emptyIa;
2217  }
2218  IntSetArgs ia(a->a.size()+offset);
2219  for (int i=offset; i--;)
2220  ia[i] = IntSet::empty;
2221  for (int i=a->a.size(); i--;) {
2222  ia[i+offset] = arg2intset(a->a[i]);
2223  }
2224  return ia;
2225  }
2226  IntVarArgs
2228  AST::Array* a = arg->getArray();
2229  if (a->a.size() == 0) {
2230  IntVarArgs emptyIa(0);
2231  return emptyIa;
2232  }
2233  IntVarArgs ia(a->a.size()+offset);
2234  for (int i=offset; i--;)
2235  ia[i] = IntVar(*this, 0, 0);
2236  for (int i=a->a.size(); i--;) {
2237  if (a->a[i]->isIntVar()) {
2238  ia[i+offset] = iv[a->a[i]->getIntVar()];
2239  } else {
2240  int value = a->a[i]->getInt();
2241  IntVar iv(*this, value, value);
2242  ia[i+offset] = iv;
2243  }
2244  }
2245  return ia;
2246  }
2247  BoolVarArgs
2248  FlatZincSpace::arg2boolvarargs(AST::Node* arg, int offset, int siv) {
2249  AST::Array* a = arg->getArray();
2250  if (a->a.size() == 0) {
2251  BoolVarArgs emptyIa(0);
2252  return emptyIa;
2253  }
2254  BoolVarArgs ia(a->a.size()+offset-(siv==-1?0:1));
2255  for (int i=offset; i--;)
2256  ia[i] = BoolVar(*this, 0, 0);
2257  for (int i=0; i<static_cast<int>(a->a.size()); i++) {
2258  if (i==siv)
2259  continue;
2260  if (a->a[i]->isBool()) {
2261  bool value = a->a[i]->getBool();
2262  BoolVar iv(*this, value, value);
2263  ia[offset++] = iv;
2264  } else if (a->a[i]->isIntVar() &&
2265  aliasBool2Int(a->a[i]->getIntVar()) != -1) {
2266  ia[offset++] = bv[aliasBool2Int(a->a[i]->getIntVar())];
2267  } else {
2268  ia[offset++] = bv[a->a[i]->getBoolVar()];
2269  }
2270  }
2271  return ia;
2272  }
2273  BoolVar
2275  BoolVar x0;
2276  if (n->isBool()) {
2277  x0 = BoolVar(*this, n->getBool(), n->getBool());
2278  }
2279  else {
2280  x0 = bv[n->getBoolVar()];
2281  }
2282  return x0;
2283  }
2284  IntVar
2286  IntVar x0;
2287  if (n->isIntVar()) {
2288  x0 = iv[n->getIntVar()];
2289  } else {
2290  x0 = IntVar(*this, n->getInt(), n->getInt());
2291  }
2292  return x0;
2293  }
2294  bool
2296  AST::Array* a = b->getArray();
2297  singleInt = -1;
2298  if (a->a.size() == 0)
2299  return true;
2300  for (int i=a->a.size(); i--;) {
2301  if (a->a[i]->isBoolVar() || a->a[i]->isBool()) {
2302  } else if (a->a[i]->isIntVar()) {
2303  if (aliasBool2Int(a->a[i]->getIntVar()) == -1) {
2304  if (singleInt != -1) {
2305  return false;
2306  }
2307  singleInt = i;
2308  }
2309  } else {
2310  return false;
2311  }
2312  }
2313  return singleInt==-1 || a->a.size() > 1;
2314  }
2315 #ifdef GECODE_HAS_SET_VARS
2316  SetVar
2318  SetVar x0;
2319  if (!n->isSetVar()) {
2320  IntSet d = arg2intset(n);
2321  x0 = SetVar(*this, d, d);
2322  } else {
2323  x0 = sv[n->getSetVar()];
2324  }
2325  return x0;
2326  }
2327  SetVarArgs
2328  FlatZincSpace::arg2setvarargs(AST::Node* arg, int offset, int doffset,
2329  const IntSet& od) {
2330  AST::Array* a = arg->getArray();
2331  SetVarArgs ia(a->a.size()+offset);
2332  for (int i=offset; i--;) {
2333  IntSet d = i<doffset ? od : IntSet::empty;
2334  ia[i] = SetVar(*this, d, d);
2335  }
2336  for (int i=a->a.size(); i--;) {
2337  ia[i+offset] = arg2SetVar(a->a[i]);
2338  }
2339  return ia;
2340  }
2341 #endif
2342 #ifdef GECODE_HAS_FLOAT_VARS
2343  FloatValArgs
2345  AST::Array* a = arg->getArray();
2346  FloatValArgs fa(a->a.size()+offset);
2347  for (int i=offset; i--;)
2348  fa[i] = 0.0;
2349  for (int i=a->a.size(); i--;)
2350  fa[i+offset] = a->a[i]->getFloat();
2351  return fa;
2352  }
2353  FloatVarArgs
2355  AST::Array* a = arg->getArray();
2356  if (a->a.size() == 0) {
2357  FloatVarArgs emptyFa(0);
2358  return emptyFa;
2359  }
2360  FloatVarArgs fa(a->a.size()+offset);
2361  for (int i=offset; i--;)
2362  fa[i] = FloatVar(*this, 0.0, 0.0);
2363  for (int i=a->a.size(); i--;) {
2364  if (a->a[i]->isFloatVar()) {
2365  fa[i+offset] = fv[a->a[i]->getFloatVar()];
2366  } else {
2367  double value = a->a[i]->getFloat();
2368  FloatVar fv(*this, value, value);
2369  fa[i+offset] = fv;
2370  }
2371  }
2372  return fa;
2373  }
2374  FloatVar
2376  FloatVar x0;
2377  if (n->isFloatVar()) {
2378  x0 = fv[n->getFloatVar()];
2379  } else {
2380  x0 = FloatVar(*this, n->getFloat(), n->getFloat());
2381  }
2382  return x0;
2383  }
2384 #endif
2385  IntPropLevel
2387  if (ann) {
2388  if (ann->hasAtom("val"))
2389  return IPL_VAL;
2390  if (ann->hasAtom("domain"))
2391  return IPL_DOM;
2392  if (ann->hasAtom("bounds") ||
2393  ann->hasAtom("boundsR") ||
2394  ann->hasAtom("boundsD") ||
2395  ann->hasAtom("boundsZ"))
2396  return IPL_BND;
2397  }
2398  return IPL_DEF;
2399  }
2400 
2401  DFA
2403  if (_initData) {
2404  FlatZincSpaceInitData::DFASet::iterator it = _initData->dfaSet.find(a);
2405  if (it != _initData->dfaSet.end()) {
2406  return *it;
2407  }
2408  _initData->dfaSet.insert(a);
2409  }
2410  return a;
2411  }
2412 
2413  void
2415  _output = output;
2416  }
2417 
2418  void
2419  Printer::printElem(std::ostream& out,
2420  AST::Node* ai,
2421  const Gecode::IntVarArray& iv,
2422  const Gecode::BoolVarArray& bv
2423 #ifdef GECODE_HAS_SET_VARS
2424  , const Gecode::SetVarArray& sv
2425 #endif
2426 #ifdef GECODE_HAS_FLOAT_VARS
2427  ,
2428  const Gecode::FloatVarArray& fv
2429 #endif
2430  ) const {
2431  int k;
2432  if (ai->isInt(k)) {
2433  out << k;
2434  } else if (ai->isIntVar()) {
2435  out << iv[ai->getIntVar()];
2436  } else if (ai->isBoolVar()) {
2437  if (bv[ai->getBoolVar()].min() == 1) {
2438  out << "true";
2439  } else if (bv[ai->getBoolVar()].max() == 0) {
2440  out << "false";
2441  } else {
2442  out << "false..true";
2443  }
2444 #ifdef GECODE_HAS_SET_VARS
2445  } else if (ai->isSetVar()) {
2446  if (!sv[ai->getSetVar()].assigned()) {
2447  out << sv[ai->getSetVar()];
2448  return;
2449  }
2450  SetVarGlbRanges svr(sv[ai->getSetVar()]);
2451  if (!svr()) {
2452  out << "{}";
2453  return;
2454  }
2455  int min = svr.min();
2456  int max = svr.max();
2457  ++svr;
2458  if (svr()) {
2459  SetVarGlbValues svv(sv[ai->getSetVar()]);
2460  int i = svv.val();
2461  out << "{" << i;
2462  ++svv;
2463  for (; svv(); ++svv)
2464  out << ", " << svv.val();
2465  out << "}";
2466  } else {
2467  out << min << ".." << max;
2468  }
2469 #endif
2470 #ifdef GECODE_HAS_FLOAT_VARS
2471  } else if (ai->isFloatVar()) {
2472  if (fv[ai->getFloatVar()].assigned()) {
2473  FloatVal vv = fv[ai->getFloatVar()].val();
2474  FloatNum v;
2475  if (vv.singleton())
2476  v = vv.min();
2477  else if (vv < 0.0)
2478  v = vv.max();
2479  else
2480  v = vv.min();
2481  std::ostringstream oss;
2482  // oss << std::scientific;
2483  oss << std::setprecision(std::numeric_limits<double>::digits10);
2484  oss << v;
2485  if (oss.str().find(".") == std::string::npos)
2486  oss << ".0";
2487  out << oss.str();
2488  } else {
2489  out << fv[ai->getFloatVar()];
2490  }
2491 #endif
2492  } else if (ai->isBool()) {
2493  out << (ai->getBool() ? "true" : "false");
2494  } else if (ai->isSet()) {
2495  AST::SetLit* s = ai->getSet();
2496  if (s->interval) {
2497  out << s->min << ".." << s->max;
2498  } else {
2499  out << "{";
2500  for (unsigned int i=0; i<s->s.size(); i++) {
2501  out << s->s[i] << (i < s->s.size()-1 ? ", " : "}");
2502  }
2503  }
2504  } else if (ai->isString()) {
2505  std::string s = ai->getString();
2506  for (unsigned int i=0; i<s.size(); i++) {
2507  if (s[i] == '\\' && i<s.size()-1) {
2508  switch (s[i+1]) {
2509  case 'n': out << "\n"; break;
2510  case '\\': out << "\\"; break;
2511  case 't': out << "\t"; break;
2512  default: out << "\\" << s[i+1];
2513  }
2514  i++;
2515  } else {
2516  out << s[i];
2517  }
2518  }
2519  }
2520  }
2521 
2522  void
2523  Printer::printElemDiff(std::ostream& out,
2524  AST::Node* ai,
2525  const Gecode::IntVarArray& iv1,
2526  const Gecode::IntVarArray& iv2,
2527  const Gecode::BoolVarArray& bv1,
2528  const Gecode::BoolVarArray& bv2
2529 #ifdef GECODE_HAS_SET_VARS
2530  , const Gecode::SetVarArray& sv1,
2531  const Gecode::SetVarArray& sv2
2532 #endif
2533 #ifdef GECODE_HAS_FLOAT_VARS
2534  , const Gecode::FloatVarArray& fv1,
2535  const Gecode::FloatVarArray& fv2
2536 #endif
2537  ) const {
2538 #ifdef GECODE_HAS_GIST
2539  using namespace Gecode::Gist;
2540  int k;
2541  if (ai->isInt(k)) {
2542  out << k;
2543  } else if (ai->isIntVar()) {
2544  std::string res(Comparator::compare("",iv1[ai->getIntVar()],
2545  iv2[ai->getIntVar()]));
2546  if (res.length() > 0) {
2547  res.erase(0, 1); // Remove '='
2548  out << res;
2549  } else {
2550  out << iv1[ai->getIntVar()];
2551  }
2552  } else if (ai->isBoolVar()) {
2553  std::string res(Comparator::compare("",bv1[ai->getBoolVar()],
2554  bv2[ai->getBoolVar()]));
2555  if (res.length() > 0) {
2556  res.erase(0, 1); // Remove '='
2557  out << res;
2558  } else {
2559  out << bv1[ai->getBoolVar()];
2560  }
2561 #ifdef GECODE_HAS_SET_VARS
2562  } else if (ai->isSetVar()) {
2563  std::string res(Comparator::compare("",sv1[ai->getSetVar()],
2564  sv2[ai->getSetVar()]));
2565  if (res.length() > 0) {
2566  res.erase(0, 1); // Remove '='
2567  out << res;
2568  } else {
2569  out << sv1[ai->getSetVar()];
2570  }
2571 #endif
2572 #ifdef GECODE_HAS_FLOAT_VARS
2573  } else if (ai->isFloatVar()) {
2574  std::string res(Comparator::compare("",fv1[ai->getFloatVar()],
2575  fv2[ai->getFloatVar()]));
2576  if (res.length() > 0) {
2577  res.erase(0, 1); // Remove '='
2578  out << res;
2579  } else {
2580  out << fv1[ai->getFloatVar()];
2581  }
2582 #endif
2583  } else if (ai->isBool()) {
2584  out << (ai->getBool() ? "true" : "false");
2585  } else if (ai->isSet()) {
2586  AST::SetLit* s = ai->getSet();
2587  if (s->interval) {
2588  out << s->min << ".." << s->max;
2589  } else {
2590  out << "{";
2591  for (unsigned int i=0; i<s->s.size(); i++) {
2592  out << s->s[i] << (i < s->s.size()-1 ? ", " : "}");
2593  }
2594  }
2595  } else if (ai->isString()) {
2596  std::string s = ai->getString();
2597  for (unsigned int i=0; i<s.size(); i++) {
2598  if (s[i] == '\\' && i<s.size()-1) {
2599  switch (s[i+1]) {
2600  case 'n': out << "\n"; break;
2601  case '\\': out << "\\"; break;
2602  case 't': out << "\t"; break;
2603  default: out << "\\" << s[i+1];
2604  }
2605  i++;
2606  } else {
2607  out << s[i];
2608  }
2609  }
2610  }
2611 #else
2612  (void) out;
2613  (void) ai;
2614  (void) iv1;
2615  (void) iv2;
2616  (void) bv1;
2617  (void) bv2;
2618 #ifdef GECODE_HAS_SET_VARS
2619  (void) sv1;
2620  (void) sv2;
2621 #endif
2622 #ifdef GECODE_HAS_FLOAT_VARS
2623  (void) fv1;
2624  (void) fv2;
2625 #endif
2626 
2627 #endif
2628  }
2629 
2630  void
2631  Printer::print(std::ostream& out,
2632  const Gecode::IntVarArray& iv,
2633  const Gecode::BoolVarArray& bv
2634 #ifdef GECODE_HAS_SET_VARS
2635  ,
2636  const Gecode::SetVarArray& sv
2637 #endif
2638 #ifdef GECODE_HAS_FLOAT_VARS
2639  ,
2640  const Gecode::FloatVarArray& fv
2641 #endif
2642  ) const {
2643  if (_output == NULL)
2644  return;
2645  for (unsigned int i=0; i< _output->a.size(); i++) {
2646  AST::Node* ai = _output->a[i];
2647  if (ai->isArray()) {
2648  AST::Array* aia = ai->getArray();
2649  int size = aia->a.size();
2650  out << "[";
2651  for (int j=0; j<size; j++) {
2652  printElem(out,aia->a[j],iv,bv
2653 #ifdef GECODE_HAS_SET_VARS
2654  ,sv
2655 #endif
2656 #ifdef GECODE_HAS_FLOAT_VARS
2657  ,fv
2658 #endif
2659  );
2660  if (j<size-1)
2661  out << ", ";
2662  }
2663  out << "]";
2664  } else {
2665  printElem(out,ai,iv,bv
2666 #ifdef GECODE_HAS_SET_VARS
2667  ,sv
2668 #endif
2669 #ifdef GECODE_HAS_FLOAT_VARS
2670  ,fv
2671 #endif
2672  );
2673  }
2674  }
2675  }
2676 
2677  void
2678  Printer::printDiff(std::ostream& out,
2679  const Gecode::IntVarArray& iv1,
2680  const Gecode::IntVarArray& iv2,
2681  const Gecode::BoolVarArray& bv1,
2682  const Gecode::BoolVarArray& bv2
2683 #ifdef GECODE_HAS_SET_VARS
2684  ,
2685  const Gecode::SetVarArray& sv1,
2686  const Gecode::SetVarArray& sv2
2687 #endif
2688 #ifdef GECODE_HAS_FLOAT_VARS
2689  ,
2690  const Gecode::FloatVarArray& fv1,
2691  const Gecode::FloatVarArray& fv2
2692 #endif
2693  ) const {
2694  if (_output == NULL)
2695  return;
2696  for (unsigned int i=0; i< _output->a.size(); i++) {
2697  AST::Node* ai = _output->a[i];
2698  if (ai->isArray()) {
2699  AST::Array* aia = ai->getArray();
2700  int size = aia->a.size();
2701  out << "[";
2702  for (int j=0; j<size; j++) {
2703  printElemDiff(out,aia->a[j],iv1,iv2,bv1,bv2
2704 #ifdef GECODE_HAS_SET_VARS
2705  ,sv1,sv2
2706 #endif
2707 #ifdef GECODE_HAS_FLOAT_VARS
2708  ,fv1,fv2
2709 #endif
2710  );
2711  if (j<size-1)
2712  out << ", ";
2713  }
2714  out << "]";
2715  } else {
2716  printElemDiff(out,ai,iv1,iv2,bv1,bv2
2717 #ifdef GECODE_HAS_SET_VARS
2718  ,sv1,sv2
2719 #endif
2720 #ifdef GECODE_HAS_FLOAT_VARS
2721  ,fv1,fv2
2722 #endif
2723  );
2724  }
2725  }
2726  }
2727 
2728  void
2729  Printer::addIntVarName(const std::string& n) {
2730  iv_names.push_back(n);
2731  }
2732  void
2733  Printer::addBoolVarName(const std::string& n) {
2734  bv_names.push_back(n);
2735  }
2736 #ifdef GECODE_HAS_FLOAT_VARS
2737  void
2738  Printer::addFloatVarName(const std::string& n) {
2739  fv_names.push_back(n);
2740  }
2741 #endif
2742 #ifdef GECODE_HAS_SET_VARS
2743  void
2744  Printer::addSetVarName(const std::string& n) {
2745  sv_names.push_back(n);
2746  }
2747 #endif
2748 
2749  void
2751  std::map<int,int>& iv, std::map<int,int>& bv,
2752  std::map<int,int>& sv, std::map<int,int>& fv) {
2753  if (node->isIntVar()) {
2754  AST::IntVar* x = static_cast<AST::IntVar*>(node);
2755  if (iv.find(x->i) == iv.end()) {
2756  int newi = iv.size();
2757  iv[x->i] = newi;
2758  }
2759  x->i = iv[x->i];
2760  } else if (node->isBoolVar()) {
2761  AST::BoolVar* x = static_cast<AST::BoolVar*>(node);
2762  if (bv.find(x->i) == bv.end()) {
2763  int newi = bv.size();
2764  bv[x->i] = newi;
2765  }
2766  x->i = bv[x->i];
2767  } else if (node->isSetVar()) {
2768  AST::SetVar* x = static_cast<AST::SetVar*>(node);
2769  if (sv.find(x->i) == sv.end()) {
2770  int newi = sv.size();
2771  sv[x->i] = newi;
2772  }
2773  x->i = sv[x->i];
2774  } else if (node->isFloatVar()) {
2775  AST::FloatVar* x = static_cast<AST::FloatVar*>(node);
2776  if (fv.find(x->i) == fv.end()) {
2777  int newi = fv.size();
2778  fv[x->i] = newi;
2779  }
2780  x->i = fv[x->i];
2781  }
2782  }
2783 
2784  void
2786  int& optVar, bool optVarIsInt,
2787  Gecode::IntVarArray& iv,
2789 #ifdef GECODE_HAS_SET_VARS
2790  ,
2792 #endif
2793 #ifdef GECODE_HAS_FLOAT_VARS
2794  ,
2796 #endif
2797  ) {
2798  if (_output == NULL) {
2799  if (optVarIsInt && optVar != -1) {
2800  IntVar ov = iv[optVar];
2801  iv = IntVarArray(home, 1);
2802  iv[0] = ov;
2803  optVar = 0;
2804  } else {
2805  iv = IntVarArray(home, 0);
2806  }
2807  bv = BoolVarArray(home, 0);
2808 #ifdef GECODE_HAS_SET_VARS
2809  sv = SetVarArray(home, 0);
2810 #endif
2811 #ifdef GECODE_HAS_FLOAT_VARS
2812  if (!optVarIsInt && optVar != -1) {
2813  FloatVar ov = fv[optVar];
2814  fv = FloatVarArray(home, 1);
2815  fv[0] = ov;
2816  optVar = 0;
2817  } else {
2818  fv = FloatVarArray(home,0);
2819  }
2820 #endif
2821  return;
2822  }
2823  std::map<int,int> iv_new;
2824  std::map<int,int> bv_new;
2825  std::map<int,int> sv_new;
2826  std::map<int,int> fv_new;
2827 
2828  if (optVar != -1) {
2829  if (optVarIsInt)
2830  iv_new[optVar] = 0;
2831  else
2832  fv_new[optVar] = 0;
2833  optVar = 0;
2834  }
2835 
2836  for (unsigned int i=0; i< _output->a.size(); i++) {
2837  AST::Node* ai = _output->a[i];
2838  if (ai->isArray()) {
2839  AST::Array* aia = ai->getArray();
2840  for (unsigned int j=0; j<aia->a.size(); j++) {
2841  shrinkElement(aia->a[j],iv_new,bv_new,sv_new,fv_new);
2842  }
2843  } else {
2844  shrinkElement(ai,iv_new,bv_new,sv_new,fv_new);
2845  }
2846  }
2847 
2848  IntVarArgs iva(iv_new.size());
2849  for (std::map<int,int>::iterator i=iv_new.begin(); i != iv_new.end(); ++i) {
2850  iva[(*i).second] = iv[(*i).first];
2851  }
2852  iv = IntVarArray(home, iva);
2853 
2854  BoolVarArgs bva(bv_new.size());
2855  for (std::map<int,int>::iterator i=bv_new.begin(); i != bv_new.end(); ++i) {
2856  bva[(*i).second] = bv[(*i).first];
2857  }
2858  bv = BoolVarArray(home, bva);
2859 
2860 #ifdef GECODE_HAS_SET_VARS
2861  SetVarArgs sva(sv_new.size());
2862  for (std::map<int,int>::iterator i=sv_new.begin(); i != sv_new.end(); ++i) {
2863  sva[(*i).second] = sv[(*i).first];
2864  }
2865  sv = SetVarArray(home, sva);
2866 #endif
2867 
2868 #ifdef GECODE_HAS_FLOAT_VARS
2869  FloatVarArgs fva(fv_new.size());
2870  for (std::map<int,int>::iterator i=fv_new.begin(); i != fv_new.end(); ++i) {
2871  fva[(*i).second] = fv[(*i).first];
2872  }
2873  fv = FloatVarArray(home, fva);
2874 #endif
2875  }
2876 
2878  delete _output;
2879  }
2880 
2881 }}
2882 
2883 // STATISTICS: flatzinc-any
IntVarBranch INT_VAR_SIZE_MAX(BranchTbl tbl)
Select variable with largest domain size.
Definition: var.hpp:211
Less ( )
Definition: float.hh:1072
struct Gecode::@602::NNF::@65::@66 b
For binary nodes (and, or, eqv)
Definition: flatzinc.hh:394
Timer
Definition: timer.hpp:51
Which integer or Boolean variable to select for branching.
Definition: branch.hh:44
An inspector for printing simple text output.
Definition: flatzinc.cpp:1667
bool fail
Whether brancher should fail.
Definition: flatzinc.cpp:140
IntVarBranch INT_VAR_ACTION_MAX(double d, BranchTbl tbl)
Select variable with highest action with decay factor d.
Definition: var.hpp:156
Passing float variables.
Definition: float.hh:979
bool isSetVar(void)
Test if node is a set variable node.
Definition: ast.hh:478
IntArgs arg2intargs(AST::Node *arg, int offset=0)
Convert arg (array of integers) to IntArgs.
Definition: flatzinc.cpp:2123
A node in a FlatZinc abstract syntax tree.
Definition: ast.hh:67
void post(FlatZincSpace &s, const ConExpr &ce)
Post constraint specified by ce.
Definition: registry.cpp:59
FZPrintingComparator(const Printer &p0)
Constructor.
Definition: flatzinc.cpp:1712
bool l
Whether to try the lower or upper half first.
Definition: float.hh:1467
Definition: flatzinc.hh:432
void print(const Brancher &b, unsigned int a, int i, int n, std::ostream &o) const
Output branch information.
Definition: flatzinc.cpp:292
bool isArray(void)
Test if node is an array node.
Definition: ast.hh:506
void compare(Comparator *c)
Add comparator.
Definition: gist.hpp:182
Post propagator for SetVar x
Definition: set.hh:767
SetVarBranch SET_VAR_ACTION_MIN(double d, BranchTbl tbl)
Definition: var.hpp:146
Exception signaling type error
Definition: ast.hh:55
bool isIntVar(void)
Test if node is an integer variable node.
Definition: ast.hh:470
BoolValBranch bool_valsel
Definition: flatzinc.cpp:158
const Gecode::FloatNum step
Definition: arithmetic.cpp:785
FloatVarArgs arg2floatvarargs(AST::Node *arg, int offset=0)
Convert n to FloatVarArgs.
Definition: flatzinc.cpp:2354
Option< std::pair< double, double > > domain
Definition: varspec.hh:121
TupleSet & add(const IntArgs &t)
Add tuple t to tuple set.
Definition: tuple-set.hpp:142
std::string what(void) const
Definition: ast.hh:61
BoolVar arg2BoolVar(AST::Node *n)
Convert n to BoolVar.
Definition: flatzinc.cpp:2274
BoolAssign BOOL_ASSIGN_RND(Rnd r)
Select random value.
Definition: assign.hpp:110
void shrinkArrays(Printer &p)
Remove all variables not needed for output.
Definition: flatzinc.cpp:2111
BoolAssign BOOL_ASSIGN_MIN(void)
Select smallest value.
Definition: assign.hpp:100
Gecode::SetVarArray sv_aux
The introduced set variables.
Definition: flatzinc.hh:506
std::unordered_set< TupleSet > TupleSetSet
Hash table of tuple sets.
Definition: flatzinc.cpp:756
bool hasAtom(const std::string &id)
Test if node has atom with id.
Definition: ast.hh:321
size_t operator()(const Gecode::SharedArray< int > &x) const
Return hash key for x.
Definition: flatzinc.cpp:67
Combine variable selection criteria for tie-breaking.
Definition: tiebreak.hpp:38
IntVarBranch INT_VAR_RND(Rnd r)
Select random variable (uniform distribution, for tie breaking)
Definition: var.hpp:101
void put(unsigned int i)
Add i to the contents.
Definition: archive.hpp:174
Node * args
Definition: ast.hh:258
Choice(const Brancher &b, bool fail0)
Initialize choice for brancher b.
Definition: flatzinc.cpp:142
SetLit * getSet(void)
Cast this node to a set literal node.
Definition: ast.hh:458
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:227
void max(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:49
const int * pi[]
Definition: photo.cpp:14262
Abstract base class for comparators.
Definition: gist.hh:119
Definition: flatzinc.cpp:264
Which values to select for branching first.
Definition: set.hh:1447
Search engine options
Definition: search.hh:746
FlatZincSpaceInitData(void)
Initialize.
Definition: flatzinc.cpp:771
DFASet dfaSet
Hash table of DFAs.
Definition: flatzinc.cpp:768
IntVarBranch INT_VAR_NONE(void)
Select first unassigned variable.
Definition: var.hpp:96
Depth-first branch-and-bound search engine.
Definition: search.hh:1070
virtual void inspect(const Space &node)
Use the print method of the template class S to print a space.
Definition: flatzinc.cpp:1686
void click(Inspector *i)
Add inspector that reacts on node double clicks.
Definition: gist.hpp:170
void printBoolVar(std::ostream &os, const std::string name, const BoolVar &b)
Definition: flatzinc.cpp:1779
BranchInformation branchInfo
Information for printing branches.
Definition: flatzinc.hh:607
void compare(const Space &s, std::ostream &out) const
Compare this space with space s and print the differences on out.
Definition: flatzinc.cpp:2058
Output support class for FlatZinc interpreter.
Definition: flatzinc.hh:107
IntValBranch int_valsel
Definition: flatzinc.cpp:156
A space that can be initialized with a FlatZinc model.
Definition: flatzinc.hh:428
TieBreak< BoolVarBranch > ann2bvarsel(AST::Node *ann, Rnd rnd, double decay)
Definition: flatzinc.cpp:518
int boolVarCount
Number of Boolean variables.
Definition: flatzinc.hh:441
IntVarBranch INT_VAR_MIN_MIN(BranchTbl tbl)
Select variable with smallest min.
Definition: var.hpp:186
virtual const char * what(void) const
Return information.
Definition: exception.cpp:55
T * dfs(T *s, const Search::Options &o)
Invoke depth-first search engine for subclass T of space s with options o.
Definition: dfs.hpp:73
Passing integer variables.
Definition: int.hh:656
unsigned int size(I &i)
Size of all ranges of range iterator i.
std::vector< bool > sv_introduced
Indicates whether a set variable is introduced by mzn2fzn.
Definition: flatzinc.hh:508
Array node
Definition: ast.hh:231
unsigned long int fail
Number of failed nodes in search tree.
Definition: search.hh:150
static const IntSet empty
Empty set.
Definition: int.hh:283
Array * getArgs(unsigned int n)
Definition: ast.hh:265
Less ( )
Definition: int.hh:929
FloatVarBranch FLOAT_VAR_AFC_MAX(double d, BranchTbl tbl)
Select variable with largest accumulated failure count with decay factor d.
Definition: var.hpp:137
std::vector< Node * > a
Definition: ast.hh:233
void postConstraints(std::vector< ConExpr * > &ces)
Post a constraint specified by ce.
Definition: flatzinc.cpp:1004
void minimize(int var, bool isInt, AST::Array *annotation)
Post that integer variable var should be minimized.
Definition: flatzinc.cpp:1608
Gecode::BoolVarArray bv
The Boolean variables.
Definition: flatzinc.hh:497
const int min
Smallest allowed integer in integer set.
Definition: set.hh:99
Call * getCall(void)
Return function call.
Definition: ast.hh:343
void branch(Home home, const IntVarArgs &x, const BoolVarArgs &y, IntBoolVarBranch vars, IntValBranch vals)
Branch function for integer and Boolean variables.
Definition: branch.cpp:120
Which values to select for branching first.
Definition: float.hh:1820
unsigned int size(Space &home) const
Return number of propagators in a group.
Definition: core.cpp:955
size_t operator()(const Gecode::DFA &d) const
Return hash key for d.
Definition: flatzinc.cpp:78
void flattenAnnotations(AST::Array *ann, std::vector< AST::Node * > &out)
Definition: flatzinc.cpp:1022
Meth _method
Whether to solve as satisfaction or optimization problem.
Definition: flatzinc.hh:453
double stop(void)
Get time since start of timer.
Definition: timer.hpp:76
friend class Choice
Definition: core.hpp:1445
IntValBranch INT_VAL_MED(void)
Select greatest value not greater than the median.
Definition: val.hpp:60
~Printer(void)
Definition: flatzinc.cpp:2877
TieBreak< IntVarBranch > int_varsel
Definition: flatzinc.cpp:155
virtual void finalize(void)
Finalize when Gist exits.
Definition: flatzinc.cpp:1694
void newIntVar(IntVarSpec *vs)
Create new integer variable from specification.
Definition: flatzinc.cpp:881
int getBoolVar(void)
Cast this node to a Boolean variable node.
Definition: ast.hh:422
Archive representation
Definition: archive.hpp:42
virtual void compare(const Space &s0, const Space &s1)=0
Call-back function.
Passing set variables.
Definition: set.hh:488
bool isBoolVar(void)
Test if node is a Boolean variable node.
Definition: ast.hh:474
SetValBranch SET_VAL_MIN_EXC(void)
Definition: val.hpp:60
T * alloc(long unsigned int n)
Allocate block of n objects of type T from region.
Definition: region.hpp:386
void init(int intVars, int boolVars, int setVars, int floatVars)
Initialize space with given number of variables.
Definition: flatzinc.cpp:856
SharedHandle::Object * object(void) const
Access to the shared object.
Gecode::IntVarArray iv
The integer variables.
Definition: flatzinc.hh:485
NodeType t
Type of node.
Definition: bool-expr.cpp:230
BoolVarBranch BOOL_VAR_ACTION_MAX(double d, BranchTbl tbl)
Select variable with highest action with decay factor d.
Definition: var.hpp:424
Meth method(void) const
Return whether to solve a satisfaction or optimization problem.
Definition: flatzinc.cpp:2031
Value propagation.
Definition: int.hh:977
FloatVarBranch FLOAT_VAR_NONE(void)
Select first unassigned variable.
Definition: var.hpp:97
virtual void print(std::ostream &)=0
Output string representation.
const FloatNum min
Smallest allowed float value.
Definition: float.hh:846
FloatValBranch FLOAT_VAL_SPLIT_MAX(void)
Select values greater than mean of smallest and largest value.
Definition: val.hpp:60
virtual size_t dispose(Space &)
Delete brancher and return its size.
Definition: flatzinc.cpp:259
Passing float arguments.
Definition: float.hh:950
SetVarBranch SET_VAR_MIN_MIN(BranchTbl tbl)
Definition: var.hpp:186
The shared object.
Abstract base class for inspectors.
Definition: gist.hh:99
IntPropLevel
Propagation levels for integer propagators.
Definition: int.hh:974
Computation spaces.
Definition: core.hpp:1742
Which values to select for branching first.
Definition: int.hh:4854
bool isInt(int &i)
Test if node is int, if yes set i to the value.
Definition: ast.hh:364
A simple comparator.
Definition: gist.hh:211
IntSharedArray arg2intsharedarray(AST::Node *arg, int offset=0)
Convert arg (array of integers) to IntSharedArray.
Definition: flatzinc.cpp:2159
iterator end(void)
Return an iterator past the end of the array.
Definition: array.hpp:1639
Base-class for both propagators and branchers.
Definition: core.hpp:628
IntValBranch INT_VAL_MIN(void)
Select smallest value.
Definition: val.hpp:55
bool optVarIsInt(void) const
Return whether variable used for optimization is integer (or float)
Definition: flatzinc.cpp:2041
Depth-first search engine.
Definition: search.hh:1036
bool isString(void)
Test if node is a string node.
Definition: ast.hh:502
int getIntVar(void)
Cast this node to an integer variable node.
Definition: ast.hh:416
bool isSet(void)
Test if node is a set literal node.
Definition: ast.hh:498
TupleSet arg2tupleset(const IntArgs &a, int noOfVars)
Convert a to TupleSet.
Definition: flatzinc.cpp:2133
Greater ( )
Definition: float.hh:1074
Definition: flatzinc.cpp:1743
#define GECODE_HAS_FLOAT_VARS
Definition: config.hpp:35
SetVarBranch SET_VAR_NONE(void)
Definition: var.hpp:96
virtual Gecode::Space * copy(void)
Copy function.
Definition: flatzinc.cpp:2026
virtual ~BranchInformationO(void)
Definition: flatzinc.cpp:279
const Space * last(void) const
Return last solution found (possibly NULL)
Definition: core.hpp:3101
BoolValBranch BOOL_VAL_RND(Rnd r)
Select random value.
Definition: val.hpp:140
bool assigned(void) const
Test whether view is assigned.
Definition: var.hpp:111
FloatVarBranch FLOAT_VAR_SIZE_MIN(BranchTbl tbl)
Select variable with smallest domain size.
Definition: var.hpp:207
std::vector< bool > iv_introduced
Indicates whether an integer variable is introduced by mzn2fzn.
Definition: flatzinc.hh:493
Integer variable array.
Definition: int.hh:763
static void explore(S *root, const FlatZincOptions &opt, Gist::Inspector *i, Gist::Comparator *c)
Definition: flatzinc.cpp:1641
TupleSetSet tupleSetSet
Hash table of tuple sets.
Definition: flatzinc.cpp:758
SetVarBranch SET_VAR_AFC_SIZE_MAX(double d, BranchTbl tbl)
Definition: var.hpp:236
virtual bool status(const Space &_home) const
Check status of brancher, return true if alternatives left.
Definition: flatzinc.cpp:170
static void installCtrlHandler(bool install, bool force=false)
Install handler for catching Ctrl-C.
Definition: script.hpp:116
SetVarBranch SET_VAR_AFC_SIZE_MIN(double d, BranchTbl tbl)
Definition: var.hpp:226
SetVarBranch SET_VAR_AFC_MIN(double d, BranchTbl tbl)
Definition: var.hpp:126
Restart with Luby sequence.
Definition: driver.hh:110
SetVarBranch SET_VAR_AFC_MAX(double d, BranchTbl tbl)
Definition: var.hpp:136
void newBoolVar(BoolVarSpec *vs)
Create new Boolean variable from specification.
Definition: flatzinc.cpp:908
unsigned long int depth
Maximum depth of search stack.
Definition: search.hh:154
bool isBool(void)
Test if node is a Boolean node.
Definition: ast.hh:490
T * alloc(long unsigned int n)
Allocate block of n objects of type T from heap.
Definition: heap.hpp:431
int size(void) const
Return size of array (number of elements)
Definition: array.hpp:926
Restart with linear sequence.
Definition: driver.hh:109
void printFloatVar(std::ostream &os, const std::string name, const Float::FloatView &f)
Definition: flatzinc.cpp:1786
Meth
Definition: flatzinc.hh:430
int optVar(void) const
Return index of variable used for optimization.
Definition: flatzinc.cpp:2036
bool isFloatVar(void)
Test if node is a float variable node.
Definition: ast.hh:482
Gecode::FloatVarArray fv
The float variables.
Definition: flatzinc.hh:512
void print(const Brancher &b, unsigned int a, int i, int n, std::ostream &o) const
Output branch information.
Definition: flatzinc.cpp:328
bool assigned(void) const
Test if all variables are assigned.
Definition: array.hpp:1026
Options for running FlatZinc models
Definition: flatzinc.hh:226
std::vector< bool > fv_introduced
Indicates whether a float variable is introduced by mzn2fzn.
Definition: flatzinc.hh:516
IntPropLevel ann2ipl(AST::Node *ann)
Convert ann to integer propagation level.
Definition: flatzinc.cpp:2386
int dfs(Space *root, const Gist::Options &opt)
Create a new stand-alone Gist for root.
Definition: gist.hpp:203
IntBoolVarBranch INTBOOL_VAR_AFC_SIZE_MAX(double d=1.0)
Select variable with largest accumulated failure count divided by domain size.
Definition: branch.hpp:138
Base class for variables.
Definition: var.hpp:40
struct Gecode::Space::@61::@63 c
Data available only during copying.
Gecode toplevel namespace
SetValBranch SET_VAL_MAX_INC(void)
Definition: val.hpp:75
unsigned long int node
Number of nodes expanded.
Definition: search.hh:152
void newSetVar(SetVarSpec *vs)
Create new set variable from specification.
Definition: flatzinc.cpp:920
Specification for integer variables.
Definition: varspec.hh:72
Group of branchers.
Definition: core.hpp:799
TieBreak< FloatVarBranch > ann2fvarsel(AST::Node *ann, Rnd rnd, double decay)
Definition: flatzinc.cpp:689
Space * clone(CloneStatistics &stat=unused_clone) const
Clone space.
Definition: core.hpp:3224
FlatZincGetInfo(const Printer &printer)
Definition: flatzinc.cpp:1746
int _optVar
Index of the variable to optimize.
Definition: flatzinc.hh:448
Node representing an atom
Definition: ast.hh:290
IntValBranch ann2ivalsel(AST::Node *ann, std::string &r0, std::string &r1, Rnd rnd)
Definition: flatzinc.cpp:449
Restart with geometric sequence.
Definition: driver.hh:111
virtual ExecStatus commit(Space &, const Gecode::Choice &c, unsigned int)
Perform commit for choice c.
Definition: flatzinc.cpp:216
bool done
Flag whether brancher is done.
Definition: flatzinc.cpp:105
Integer sets.
Definition: int.hh:174
FloatVarBranch FLOAT_VAR_MAX_MAX(BranchTbl tbl)
Select variable with largest max.
Definition: var.hpp:202
IntVar arg2IntVar(AST::Node *n)
Convert n to IntVar.
Definition: flatzinc.cpp:2285
unsigned int a_d
Create a clone during recomputation if distance is greater than a_d (adaptive distance)
Definition: search.hh:755
const int max
Largest allowed integer in integer set.
Definition: set.hh:97
IntSharedArray arg2boolsharedarray(AST::Node *arg, int offset=0)
Convert arg (array of integers) to IntSharedArray.
Definition: flatzinc.cpp:2183
bool alias
Whether the variable aliases another variable.
Definition: varspec.hh:59
Float view for float variables.
Definition: view.hpp:52
SetVar arg2SetVar(AST::Node *n)
Convert n to SetVar.
Definition: flatzinc.cpp:2317
Option< AST::SetLit * > domain
Definition: varspec.hh:74
DFA getSharedDFA(DFA &a)
Share DFA a if possible.
Definition: flatzinc.cpp:2402
Boolean variable array.
Definition: int.hh:808
struct Gecode::@602::NNF::@65::@67 a
For atomic nodes.
Print statistics for script.
Definition: driver.hh:97
Node * x
Pointer to corresponding Boolean expression node.
Definition: bool-expr.cpp:249
Options opt
The options.
Definition: test.cpp:97
Options for Gist
Definition: gist.hh:234
Argument array for non-primitive types.
Definition: array.hpp:656
Which values to select for assignment.
Definition: int.hh:4971
BoolVarArgs arg2boolvarargs(AST::Node *arg, int offset=0, int siv=-1)
Convert arg to BoolVarArgs.
Definition: flatzinc.cpp:2248
virtual std::string getInfo(const Space &space) const
Return info for a space.
Definition: flatzinc.cpp:1748
void finalize(void)
Finalize tuple set.
Definition: tuple-set.hpp:155
static PropagatorGroup all
Group of all propagators.
Definition: core.hpp:789
struct Gecode::Space::@61::@62 p
Data only available during propagation or branching.
Base-class for branchers.
Definition: core.hpp:1442
Registry & registry(void)
Return global registry object.
Definition: registry.cpp:53
void varValPrintF(const Space &home, const Brancher &b, unsigned int a, FloatVar, int i, const FloatNumBranch &nl, std::ostream &o)
Definition: flatzinc.cpp:348
Passing Boolean variables.
Definition: int.hh:712
Home class for posting propagators
Definition: core.hpp:856
Gecode::BoolVarArray bv_aux
The introduced Boolean variables.
Definition: flatzinc.hh:499
FloatValBranch FLOAT_VAL_SPLIT_MIN(void)
Select values not greater than mean of smallest and largest value.
Definition: val.hpp:55
void print(const Brancher &b, unsigned int a, int i, const FloatNumBranch &nl, std::ostream &o) const
Definition: flatzinc.cpp:298
IntValBranch INT_VALUES_MIN(void)
Try all values starting from smallest.
Definition: val.hpp:100
AuxVarBrancher(Home home, TieBreak< IntVarBranch > int_varsel0, IntValBranch int_valsel0, TieBreak< BoolVarBranch > bool_varsel0, BoolValBranch bool_valsel0, SetVarBranch set_varsel0, SetValBranch set_valsel0, TieBreak< FloatVarBranch > float_varsel0, FloatValBranch float_valsel0)
Construct brancher.
Definition: flatzinc.cpp:107
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:226
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:2631
Handle to region.
Definition: region.hpp:55
SetValBranch ann2svalsel(AST::Node *ann, std::string r0, std::string r1, Rnd rnd)
Definition: flatzinc.cpp:659
IntSet vs2is(IntVarSpec *vs)
Definition: flatzinc.cpp:356
Specification for Boolean variables.
Definition: varspec.hh:97
void createBranchers(Printer &p, AST::Node *ann, FlatZincOptions &opt, bool ignoreUnknown, std::ostream &err=std::cerr)
Create branchers corresponding to the solve item annotations.
Definition: flatzinc.cpp:1037
FZPrintingInspector(const Printer &p0)
Constructor.
Definition: flatzinc.cpp:1681
Array * getArray(void)
Cast this node to an array node.
Definition: ast.hh:396
BoolVarBranch BOOL_VAR_DEGREE_MAX(BranchTbl tbl)
Select variable with largest degree.
Definition: var.hpp:389
IntVarBranch INT_VAR_REGRET_MIN_MAX(BranchTbl tbl)
Select variable with largest min-regret.
Definition: var.hpp:291
#define GECODE_HAS_SET_VARS
Definition: config.hpp:56
Specification for floating point variables.
Definition: varspec.hh:119
void dom(Home home, FloatVar x, FloatVal n)
Propagates .
Definition: dom.cpp:40
Abstract representation of a constraint.
Definition: conexpr.hh:43
Post propagator for SetVar SetOpType SetVar SetRelType r
Definition: set.hh:767
double FloatNum
Floating point number base type.
Definition: float.hh:106
~FlatZincGetInfo(void)
Definition: flatzinc.cpp:1757
Boolean integer variables.
Definition: int.hh:512
Domain propagation Options: basic versus advanced propagation.
Definition: int.hh:979
Set variable node
Definition: ast.hh:222
virtual void constrain(const Space &s)
Implement optimization.
Definition: flatzinc.cpp:1981
class Gecode::Gist::Options::_I inspect
SetValBranch SET_VAL_MIN_INC(void)
Definition: val.hpp:55
Set variables
Definition: set.hh:127
void sort(TaskViewArray< TaskView > &t)
Sort task view array t according to sto and inc (increasing or decreasing)
Definition: sort.hpp:133
Traits class for search engines.
Definition: flatzinc.cpp:1634
virtual Choice * choice(const Space &, Archive &e)
Return choice.
Definition: flatzinc.cpp:211
std::vector< int > s
Definition: ast.hh:175
int getSetVar(void)
Cast this node to a set variable node.
Definition: ast.hh:434
void newFloatVar(FloatVarSpec *vs)
Create new float variable from specification.
Definition: flatzinc.cpp:967
Information is provided by a restart-based engine.
Definition: core.hpp:1618
size_t operator()(const Gecode::TupleSet &x) const
Return hash key for x.
Definition: flatzinc.cpp:58
unsigned int id(void) const
Return a unique id for the group.
Definition: core.hpp:4974
Value description class for branching.
Definition: float.hh:1462
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:2750
FloatNum n
The middle value for branching.
Definition: float.hh:1465
void add(BrancherGroup bg, const std::string &rel0, const std::string &rel1, const std::vector< std::string > &n)
Add new brancher information.
Definition: flatzinc.cpp:321
Restart with constant sequence.
Definition: driver.hh:108
unsigned int c_d
Create a clone after every c_d commits (commit distance)
Definition: search.hh:753
void assign(Home home, const FloatVarArgs &x, FloatVarBranch vars, FloatAssign vals, FloatBranchFilter bf, FloatVarValPrint vvp)
Assign all x with variable selection vars and value selection vals.
Definition: branch.cpp:111
FloatVarBranch FLOAT_VAR_AFC_MIN(double d, BranchTbl tbl)
Select variable with smallest accumulated failure count with decay factor d.
Definition: var.hpp:127
Run script in Gist.
Definition: driver.hh:98
const int max
Largest allowed integer value.
Definition: int.hh:116
Definition: flatzinc.hh:433
BranchInformation(void)
Constructor.
Definition: flatzinc.cpp:308
IntVarBranch INT_VAR_DEGREE_MAX(BranchTbl tbl)
Select variable with largest degree.
Definition: var.hpp:121
Random number generator.
Definition: rnd.hpp:42
IntSet arg2intset(AST::Node *n)
Convert n to IntSet.
Definition: flatzinc.cpp:2197
IntAssign INT_ASSIGN_MAX(void)
Select largest value.
Definition: assign.hpp:65
bool _optVarIsInt
Whether variable to optimize is integer (or float)
Definition: flatzinc.hh:450
Integer variables.
Definition: int.hh:371
Gecode::FloatVarArray fv_aux
The introduced float variables.
Definition: flatzinc.hh:514
BoolValBranch BOOL_VAL_MAX(void)
Select largest value.
Definition: val.hpp:135
FlatZincSpaceInitData * _initData
Initialisation data (only used for posting constraints)
Definition: flatzinc.hh:437
virtual bool slave(const MetaInfo &mi)
Slave function for restarts.
Definition: flatzinc.cpp:2002
virtual size_t size(void) const
Report size occupied.
Definition: flatzinc.cpp:145
virtual void archive(Archive &e) const
Archive into e.
Definition: flatzinc.cpp:149
void addSetVarName(const std::string &n)
Definition: flatzinc.cpp:2744
IntAssign INT_ASSIGN_RND(Rnd r)
Select random value.
Definition: assign.hpp:70
SetVarBranch SET_VAR_ACTION_MAX(double d, BranchTbl tbl)
Definition: var.hpp:156
bool funcDep
Whether the variable functionally depends on another variable.
Definition: varspec.hh:65
BoolValBranch BOOL_VAL_MIN(void)
Select smallest value.
Definition: val.hpp:130
virtual Actor * copy(Space &home)
Copy brancher.
Definition: flatzinc.cpp:228
Class represeting a set of tuples.
Definition: int.hh:2191
Integer variable node.
Definition: ast.hh:206
static void explore(S *root, const FlatZincOptions &opt, Gist::Inspector *i, Gist::Comparator *c)
Definition: flatzinc.cpp:1655
BoolVarBranch BOOL_VAR_AFC_MIN(double d, BranchTbl tbl)
Select variable with smallest accumulated failure count with decay factor d.
Definition: var.hpp:394
Bounds propagation.
Definition: int.hh:978
Specification for set variables.
Definition: varspec.hh:139
IntVarArgs arg2intvarargs(AST::Node *arg, int offset=0)
Convert arg to IntVarArgs.
Definition: flatzinc.cpp:2227
FloatVarBranch FLOAT_VAR_MIN_MIN(BranchTbl tbl)
Select variable with smallest min.
Definition: var.hpp:187
void abs(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition: arithmetic.cpp:41
void print(std::ostream &out, const Printer &p) const
Produce output on out using p.
Definition: flatzinc.cpp:2046
std::unordered_set< SharedArray< int > > IntSharedArraySet
Hash table of shared integer arrays.
Definition: flatzinc.cpp:761
int explore(Space *root, bool bab, const Options &opt)
Create a new stand-alone Gist for root using bab.
Definition: gist.cpp:102
BoolVarBranch BOOL_VAR_AFC_MAX(double d, BranchTbl tbl)
Select variable with largest accumulated failure count with decay factor d.
Definition: var.hpp:404
IntVarBranch INT_VAR_ACTION_SIZE_MIN(double d, BranchTbl tbl)
Select variable with smallest action divided by domain size with decay factor d.
Definition: var.hpp:246
bool isBoolArray(AST::Node *b, int &singleInt)
Check if b is array of Booleans (or has a single integer)
Definition: flatzinc.cpp:2295
std::vector< bool > bv_introduced
Indicates whether a Boolean variable is introduced by mzn2fzn.
Definition: flatzinc.hh:501
Heap heap
The single global heap.
Definition: heap.cpp:44
Definition: flatzinc.cpp:1699
Choice that only signals failure or success
Definition: flatzinc.cpp:137
void cmb_hash(std::size_t &seed, const T h)
Combine hash value h into seed.
Definition: hash.hpp:44
Type type(void) const
Return type of information.
Definition: core.hpp:3082
TieBreak< BoolVarBranch > bool_varsel
Definition: flatzinc.cpp:157
Search::Cutoff * createCutoff(const Options &o)
Create cutoff object from options.
Definition: script.hpp:153
Set literal node
Definition: ast.hh:171
Exception class for FlatZinc errors
Definition: flatzinc.hh:665
void fail(void)
Fail space.
Definition: core.hpp:4030
FlatZincSpace(FlatZincSpace &)
Copy constructor.
Definition: flatzinc.cpp:774
static void post(Home home, TieBreak< IntVarBranch > int_varsel, IntValBranch int_valsel, TieBreak< BoolVarBranch > bool_varsel, BoolValBranch bool_valsel, SetVarBranch set_varsel, SetValBranch set_valsel, TieBreak< FloatVarBranch > float_varsel, FloatValBranch float_valsel)
Post brancher.
Definition: flatzinc.cpp:232
IntVarBranch INT_VAR_SIZE_MIN(BranchTbl tbl)
Select variable with smallest domain size.
Definition: var.hpp:206
FloatVarBranch FLOAT_VAR_SIZE_MAX(BranchTbl tbl)
Select variable with largest domain size.
Definition: var.hpp:212
SetVarBranch SET_VAR_SIZE_MAX(BranchTbl tbl)
Definition: var.hpp:211
bool assigned
Whether the variable is assigned.
Definition: varspec.hh:61
Deterministic finite automaton (DFA)
Definition: int.hh:2049
unsigned long int propagate
Number of propagator executions.
Definition: core.hpp:1694
const int v[7]
Definition: distinct.cpp:259
void rel(Home home, FloatVar x0, FloatRelType frt, FloatVal n)
Propagates .
Definition: rel.cpp:43
Float variables.
Definition: float.hh:870
Rnd defrnd(0)
Uninitialized default random number generator.
Definition: flatzinc.hh:420
void printIntVar(std::ostream &os, const std::string name, const Int::IntView &x)
Definition: flatzinc.cpp:1760
static Search::Stop * create(unsigned int node, unsigned int fail, unsigned int time, bool intr)
Create appropriate stop-object.
Definition: script.hpp:90
AST::Array * _solveAnnotations
Annotations on the solve item.
Definition: flatzinc.hh:465
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:2678
const Printer & p
Definition: flatzinc.cpp:1745
SetVarBranch SET_VAR_RND(Rnd r)
Definition: var.hpp:101
int size(void) const
Return size of array (number of elements)
Definition: array.hpp:1607
SetVarBranch SET_VAR_ACTION_SIZE_MAX(double d, BranchTbl tbl)
Definition: var.hpp:256
Simple propagation levels.
Definition: int.hh:976
bool needAuxVars
Whether the introduced variables still need to be copied.
Definition: flatzinc.hh:521
AuxVarBrancher(Space &home, AuxVarBrancher &b)
Copy constructor.
Definition: flatzinc.cpp:133
Float variable node.
Definition: ast.hh:214
Run script with CP-profiler.
Definition: driver.hh:99
Branching on the introduced variables.
Definition: flatzinc.cpp:102
SharedArray< int > IntSharedArray
Arrays of integers that can be shared among several element constraints.
Definition: int.hh:1477
BoolValBranch ann2bvalsel(AST::Node *ann, std::string &r0, std::string &r1, Rnd rnd)
Definition: flatzinc.cpp:552
Gecode::IntSet d(v, 7)
void add(BrancherGroup bg, const std::string &rel0, const std::string &rel1, const std::vector< std::string > &n)
Add new brancher information.
Definition: flatzinc.cpp:284
Definition: flatzinc.cpp:52
AST::Array * solveAnnotations(void) const
Return the solve item annotations.
Definition: flatzinc.cpp:1597
IntVarBranch INT_VAR_MAX_MAX(BranchTbl tbl)
Select variable with largest max.
Definition: var.hpp:201
void start(void)
Start timer.
Definition: timer.hpp:66
void free(T *b, long unsigned int n)
Delete n objects starting at b.
Definition: heap.hpp:457
IntAssign INT_ASSIGN_MED(void)
Select greatest value not greater than the median.
Definition: assign.hpp:60
int i
Variable index.
Definition: varspec.hh:57
void aliasBool2Int(int iv, int bv)
Link integer variable iv to Boolean variable bv.
Definition: flatzinc.cpp:899
Statistics for execution of status
Definition: core.hpp:1691
Integer view for integer variables.
Definition: view.hpp:129
IntVarBranch INT_VAR_AFC_MIN(double d, BranchTbl tbl)
Select variable with smallest accumulated failure count with decay factor d.
Definition: var.hpp:126
BoolAssign BOOL_ASSIGN_MAX(void)
Select largest value.
Definition: assign.hpp:105
void addBoolVarName(const std::string &n)
Definition: flatzinc.cpp:2733
BoolVarBranch BOOL_VAR_ACTION_MIN(double d, BranchTbl tbl)
Select variable with lowest action with decay factor d.
Definition: var.hpp:414
Float variable array.
Definition: float.hh:1030
void init(void)
Initialise for use.
Definition: flatzinc.cpp:315
SetVarBranch ann2svarsel(AST::Node *ann, Rnd rnd, double decay)
Definition: flatzinc.cpp:621
FloatVarBranch FLOAT_VAR_ACTION_MIN(double d, BranchTbl tbl)
Select variable with lowest action with decay factor d.
Definition: var.hpp:147
void run(std::ostream &out, const Printer &p, const FlatZincOptions &opt, Gecode::Support::Timer &t_total)
Run the search.
Definition: flatzinc.cpp:1967
FloatVarBranch FLOAT_VAR_DEGREE_MAX(BranchTbl tbl)
Select variable with largest degree.
Definition: var.hpp:122
int getFloatVar(void)
Cast this node to a Float variable node.
Definition: ast.hh:428
void varValPrint(const Space &home, const Brancher &b, unsigned int a, Var, int i, const int &n, std::ostream &o)
Definition: flatzinc.cpp:340
void maximize(int var, bool isInt, AST::Array *annotation)
Post that integer variable var should be maximized.
Definition: flatzinc.cpp:1616
SetVarBranch SET_VAR_MAX_MAX(BranchTbl tbl)
Definition: var.hpp:201
SetValBranch SET_VAL_MAX_EXC(void)
Definition: val.hpp:80
int setVarCount
Number of set variables.
Definition: flatzinc.hh:445
Node representing a function call
Definition: ast.hh:255
int intVarCount
Number of integer variables.
Definition: flatzinc.hh:439
Definition: flatzinc.hh:431
const int min
Smallest allowed integer value.
Definition: int.hh:118
#define forceinline
Definition: config.hpp:185
int bab(Space *root, const Gist::Options &opt)
Create a new stand-alone Gist for branch-and-bound search of root.
Definition: gist.hpp:208
Boolean variable node.
Definition: ast.hh:197
int max
Definition: ast.hh:174
~FlatZincSpace(void)
Destructor.
Definition: flatzinc.cpp:1623
Option< AST::SetLit * > domain
Definition: varspec.hh:99
int vs2bsl(BoolVarSpec *bs)
Definition: flatzinc.cpp:376
Equality ( )
Definition: int.hh:926
Information passed by meta search engines.
Definition: core.hpp:1613
IntVarBranch INT_VAR_ACTION_SIZE_MAX(double d, BranchTbl tbl)
Select variable with largest action divided by domain size with decay factor d.
Definition: var.hpp:256
void solve(AST::Array *annotation)
Post the solve item.
Definition: flatzinc.cpp:1602
IntValBranch INT_VAL_SPLIT_MIN(void)
Select values not greater than mean of smallest and largest value.
Definition: val.hpp:75
void addFloatVarName(const std::string &n)
Definition: flatzinc.cpp:2738
SetVarBranch SET_VAR_SIZE_MIN(BranchTbl tbl)
Definition: var.hpp:206
virtual void print(const Space &, const Gecode::Choice &c, unsigned int, std::ostream &o) const
Print explanation.
Definition: flatzinc.cpp:220
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:236
The Gecode Interactive Search Tool.
int size(void) const
Return number of elements.
IntAssign ann2asnivalsel(AST::Node *ann, Rnd rnd)
Definition: flatzinc.cpp:500
The shared handle.
void min(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:67
Gecode::SetVarArray sv
The set variables.
Definition: flatzinc.hh:504
Gecode::FloatNum step
Step by which a next solution has to have lower cost.
Definition: flatzinc.hh:518
Option< AST::SetLit * > upperBound
Definition: varspec.hh:141
Post propagator for f(x \diamond_{\mathit{op}} y) \sim_r z \f$ void rel(Home home
Which values to select for assignment.
Definition: int.hh:5000
unsigned long int restart
Number of restarts.
Definition: search.hh:156
FloatVarBranch FLOAT_VAR_ACTION_SIZE_MIN(double d, BranchTbl tbl)
Select variable with smallest action divided by domain size with decay factor d.
Definition: var.hpp:247
FloatValBranch float_valsel
Definition: flatzinc.cpp:165
Rnd _random
Random number generator.
Definition: flatzinc.hh:462
Gecode::FloatVal c(-8, 8)
SetVarBranch set_varsel
Definition: flatzinc.cpp:160
Gecode::IntVarArray iv_aux
The introduced integer variables.
Definition: flatzinc.hh:487
Set variable array
Definition: set.hh:570
void shrinkArrays(Space &home, int &optVar, bool optVarIsInt, Gecode::IntVarArray &iv, Gecode::BoolVarArray &bv, Gecode::SetVarArray &sv, Gecode::FloatVarArray &fv)
Definition: flatzinc.cpp:2785
BranchInformationO(void)
Definition: flatzinc.cpp:278
BoolAssign ann2asnbvalsel(AST::Node *ann, Rnd rnd)
Definition: flatzinc.cpp:603
TieBreak< IntVarBranch > ann2ivarsel(AST::Node *ann, Rnd rnd, double decay)
Definition: flatzinc.cpp:400
FloatValBranch ann2fvalsel(AST::Node *ann, std::string r0, std::string r1)
Definition: flatzinc.cpp:733
IntSharedArraySet intSharedArraySet
Hash table of shared integer arrays.
Definition: flatzinc.cpp:763
No restarts.
Definition: driver.hh:107
virtual Choice * choice(Space &home)
Return choice.
Definition: flatzinc.cpp:189
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:234
Gecode::IntVarArray iv_lns
The integer variables used in LNS.
Definition: flatzinc.hh:490
FloatVar arg2FloatVar(AST::Node *n)
Convert n to FloatVar.
Definition: flatzinc.cpp:2375
Choice for performing commit
Definition: core.hpp:1412
Execution has resulted in failure.
Definition: core.hpp:474
IntSharedArray _lnsInitialSolution
Initial solution to start the LNS (or NULL for no LNS)
Definition: flatzinc.hh:459
int vs2bsh(BoolVarSpec *bs)
Definition: flatzinc.cpp:388
std::unordered_set< DFA > DFASet
Hash table of DFAs.
Definition: flatzinc.cpp:766
int * iv_boolalias
Indicates whether an integer variable aliases a Boolean variable.
Definition: flatzinc.hh:495
Greater ( )
Definition: int.hh:931
int getInt(void)
Cast this node to an integer node.
Definition: ast.hh:440
void addIntVarName(const std::string &n)
Definition: flatzinc.cpp:2729
unsigned long int restart(void) const
Return number of restarts.
Definition: core.hpp:3086
Passing integer arguments.
Definition: int.hh:628
CompareStatus compare(I &i, J &j)
Check whether range iterator i is a subset of j, or whether they are disjoint.
bool interval
Definition: ast.hh:173
FloatValArgs arg2floatargs(AST::Node *arg, int offset=0)
Convert n to FloatValArgs.
Definition: flatzinc.cpp:2344
const Val & some(void) const
Definition: option.hh:47
SetVarArgs arg2setvarargs(AST::Node *arg, int offset=0, int doffset=0, const IntSet &od=IntSet::empty)
Convert n to SetVarArgs.
Definition: flatzinc.cpp:2328
SetVarBranch SET_VAR_ACTION_SIZE_MIN(double d, BranchTbl tbl)
Definition: var.hpp:246
Gecode::IntArgs i({1, 2, 3, 4})
FloatVarBranch FLOAT_VAR_RND(Rnd r)
Select random variable (uniform distribution, for tie breaking)
Definition: var.hpp:112
IntArgs arg2boolargs(AST::Node *arg, int offset=0)
Convert arg (array of Booleans) to IntArgs.
Definition: flatzinc.cpp:2173
std::string getString(void)
Cast this node to a string node.
Definition: ast.hh:464
int min
Definition: ast.hh:174
Search engine statistics
Definition: search.hh:147
bool getBool(void)
Cast this node to a Boolean node.
Definition: ast.hh:446
Execution is okay.
Definition: core.hpp:476
Space is failed
Definition: core.hpp:1682
const BoolInstr * bi[]
Definition: mm-bool.cpp:4169
int p
Number of positive literals for node type.
Definition: bool-expr.cpp:232
unsigned int _lns
Percentage of variables to keep in LNS (or 0 for no LNS)
Definition: flatzinc.hh:456
BoolVarBranch BOOL_VAR_NONE(void)
Select first unassigned variable.
Definition: var.hpp:364
IntSetArgs arg2intsetargs(AST::Node *arg, int offset=0)
Convert arg to IntSetArgs.
Definition: flatzinc.cpp:2212
Definition: flatzinc.cpp:753
void init(AST::Array *output)
Definition: flatzinc.cpp:2414
virtual void archive(Archive &e) const
Archive into e.
Definition: core.cpp:891
const FloatNum max
Largest allowed float value.
Definition: float.hh:844
iterator begin(void)
Return an iterator at the beginning of the array.
Definition: array.hpp:1627
virtual void compare(const Space &s0, const Space &s1)
Use the compare method of the template class S to compare two spaces.
Definition: flatzinc.cpp:1717
IntValBranch INT_VAL_MAX(void)
Select largest value.
Definition: val.hpp:65
TieBreak< FloatVarBranch > float_varsel
Definition: flatzinc.cpp:164
virtual SharedHandle::Object * copy(void) const
Definition: flatzinc.cpp:280
BoolVarBranch BOOL_VAR_RND(Rnd r)
Select random variable (uniform distribution, for tie breaking)
Definition: var.hpp:369
SetValBranch set_valsel
Definition: flatzinc.cpp:161
FloatVarBranch FLOAT_VAR_ACTION_SIZE_MAX(double d, BranchTbl tbl)
Select variable with largest action divided by domain size with decay factor d.
Definition: var.hpp:257
std::string getDomains(const Printer &p) const
Get string representing the domains of variables (for cpprofiler)
Definition: flatzinc.cpp:1795
void update(Space &home, VarArray< Var > &a)
Update array to be a clone of array a.
Definition: array.hpp:1013
int floatVarCount
Number of float variables.
Definition: flatzinc.hh:443
unsigned int seed
The random seed to be used.
Definition: test.hh:79
Which variable to select for branching.
Definition: set.hh:1296
Class to send solution information to CPProfiler.
Definition: search.hh:423
IntValBranch INT_VAL_SPLIT_MAX(void)
Select values greater than mean of smallest and largest value.
Definition: val.hpp:80
An window for simple text output.
Definition: gist.hh:160
Exception: Base-class for exceptions
Definition: exception.hpp:42
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:237
bool introduced
Whether the variable was introduced in the mzn2fzn translation.
Definition: varspec.hh:63
void finalize(void)
Clean up when Gist exits.
Definition: gist.cpp:64
ExecStatus
Definition: core.hpp:472
IntVarBranch INT_VAR_AFC_MAX(double d, BranchTbl tbl)
Select variable with largest accumulated failure count with decay factor d.
Definition: var.hpp:136
Which values to select for branching first.
Definition: int.hh:4889
IntValBranch INT_VAL_RND(Rnd r)
Select random value.
Definition: val.hpp:70
IntAssign INT_ASSIGN_MIN(void)
Select smallest value.
Definition: assign.hpp:55
FloatVarBranch FLOAT_VAR_ACTION_MAX(double d, BranchTbl tbl)
Select variable with highest action with decay factor d.
Definition: var.hpp:157
IntVarBranch INT_VAR_ACTION_MIN(double d, BranchTbl tbl)
Select variable with lowest action with decay factor d.
Definition: var.hpp:146