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