Generated on Tue Mar 5 2013 22:37:13 for Gecode by doxygen 1.8.3.1
flatzinc.cpp
Go to the documentation of this file.
1 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2 /*
3  * Main authors:
4  * Guido Tack <tack@gecode.org>
5  *
6  * Copyright:
7  * Guido Tack, 2007
8  *
9  * Last modified:
10  * $Date: 2012-03-21 16:25:08 +1100 (Wed, 21 Mar 2012) $ by $Author: tack $
11  * $Revision: 12605 $
12  *
13  * This file is part of Gecode, the generic constraint
14  * development environment:
15  * http://www.gecode.org
16  *
17  * Permission is hereby granted, free of charge, to any person obtaining
18  * a copy of this software and associated documentation files (the
19  * "Software"), to deal in the Software without restriction, including
20  * without limitation the rights to use, copy, modify, merge, publish,
21  * distribute, sublicense, and/or sell copies of the Software, and to
22  * permit persons to whom the Software is furnished to do so, subject to
23  * the following conditions:
24  *
25  * The above copyright notice and this permission notice shall be
26  * included in all copies or substantial portions of the Software.
27  *
28  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
29  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
30  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
31  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
32  * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
33  * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
34  * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
35  *
36  */
37 
38 #include <gecode/flatzinc.hh>
41 
42 #include <gecode/search.hh>
43 
44 #include <vector>
45 #include <string>
46 using namespace std;
47 
48 namespace Gecode { namespace FlatZinc {
49 
51  if (vs->assigned) {
52  return IntSet(vs->i,vs->i);
53  }
54  if (vs->domain()) {
55  AST::SetLit* sl = vs->domain.some();
56  if (sl->interval) {
57  return IntSet(sl->min, sl->max);
58  } else {
59  int* newdom = heap.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
60  for (int i=sl->s.size(); i--;)
61  newdom[i] = sl->s[i];
62  IntSet ret(newdom, sl->s.size());
63  heap.free(newdom, static_cast<unsigned long int>(sl->s.size()));
64  return ret;
65  }
66  }
68  }
69 
70  int vs2bsl(BoolVarSpec* bs) {
71  if (bs->assigned) {
72  return bs->i;
73  }
74  if (bs->domain()) {
75  AST::SetLit* sl = bs->domain.some();
76  assert(sl->interval);
77  return std::min(1, std::max(0, sl->min));
78  }
79  return 0;
80  }
81 
82  int vs2bsh(BoolVarSpec* bs) {
83  if (bs->assigned) {
84  return bs->i;
85  }
86  if (bs->domain()) {
87  AST::SetLit* sl = bs->domain.some();
88  assert(sl->interval);
89  return std::max(0, std::min(1, sl->max));
90  }
91  return 1;
92  }
93 
95  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
96  if (s->id == "input_order")
98  if (s->id == "first_fail")
100  if (s->id == "anti_first_fail")
102  if (s->id == "smallest")
104  if (s->id == "largest")
106  if (s->id == "occurrence")
108  if (s->id == "max_regret")
110  if (s->id == "most_constrained")
113  if (s->id == "random")
115  if (s->id == "afc_min")
117  if (s->id == "afc_max")
119  if (s->id == "size_afc_min")
121  if (s->id == "size_afc_max")
123  }
124  std::cerr << "Warning, ignored search annotation: ";
125  ann->print(std::cerr);
126  std::cerr << std::endl;
128  }
129 
131  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
132  if (s->id == "indomain_min")
133  return INT_VAL_MIN;
134  if (s->id == "indomain_max")
135  return INT_VAL_MAX;
136  if (s->id == "indomain_median")
137  return INT_VAL_MED;
138  if (s->id == "indomain_split")
139  return INT_VAL_SPLIT_MIN;
140  if (s->id == "indomain_reverse_split")
141  return INT_VAL_SPLIT_MAX;
142  if (s->id == "indomain_random")
143  return INT_VAL_RND;
144  if (s->id == "indomain")
145  return INT_VALUES_MIN;
146  if (s->id == "indomain_middle") {
147  std::cerr << "Warning, replacing unsupported annotation "
148  << "indomain_middle with indomain_median" << std::endl;
149  return INT_VAL_MED;
150  }
151  if (s->id == "indomain_interval") {
152  std::cerr << "Warning, replacing unsupported annotation "
153  << "indomain_interval with indomain_split" << std::endl;
154  return INT_VAL_SPLIT_MIN;
155  }
156  }
157  std::cerr << "Warning, ignored search annotation: ";
158  ann->print(std::cerr);
159  std::cerr << std::endl;
160  return INT_VAL_MIN;
161  }
162 
164  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
165  if (s->id == "indomain_min")
166  return INT_ASSIGN_MIN;
167  if (s->id == "indomain_max")
168  return INT_ASSIGN_MAX;
169  if (s->id == "indomain_median")
170  return INT_ASSIGN_MED;
171  if (s->id == "indomain_random")
172  return INT_ASSIGN_RND;
173  }
174  std::cerr << "Warning, ignored search annotation: ";
175  ann->print(std::cerr);
176  std::cerr << std::endl;
177  return INT_ASSIGN_MIN;
178  }
179 
180 #ifdef GECODE_HAS_SET_VARS
182  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
183  if (s->id == "input_order")
184  return SET_VAR_NONE;
185  if (s->id == "first_fail")
186  return SET_VAR_SIZE_MIN;
187  if (s->id == "anti_first_fail")
188  return SET_VAR_SIZE_MAX;
189  if (s->id == "smallest")
190  return SET_VAR_MIN_MIN;
191  if (s->id == "largest")
192  return SET_VAR_MAX_MAX;
193  }
194  std::cerr << "Warning, ignored search annotation: ";
195  ann->print(std::cerr);
196  std::cerr << std::endl;
197  return SET_VAR_NONE;
198  }
199 
201  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
202  if (s->id == "indomain_min")
203  return SET_VAL_MIN_INC;
204  if (s->id == "indomain_max")
205  return SET_VAL_MAX_INC;
206  if (s->id == "outdomain_min")
207  return SET_VAL_MIN_EXC;
208  if (s->id == "outdomain_max")
209  return SET_VAL_MAX_EXC;
210  }
211  std::cerr << "Warning, ignored search annotation: ";
212  ann->print(std::cerr);
213  std::cerr << std::endl;
214  return SET_VAL_MIN_INC;
215  }
216 #endif
217 
218  FlatZincSpace::FlatZincSpace(bool share, FlatZincSpace& f)
219  : Space(share, f), _solveAnnotations(NULL), iv_boolalias(NULL) {
220  _optVar = f._optVar;
221  _method = f._method;
222  iv.update(*this, share, f.iv);
224  bv.update(*this, share, f.bv);
226 #ifdef GECODE_HAS_SET_VARS
227  sv.update(*this, share, f.sv);
229 #endif
230  }
231 
233  : intVarCount(-1), boolVarCount(-1), setVarCount(-1), _optVar(-1),
234  _solveAnnotations(NULL) {}
235 
236  void
237  FlatZincSpace::init(int intVars, int boolVars,
238 #ifdef GECODE_HAS_SET_VARS
239  int setVars) {
240 #else
241  int) {
242 #endif
243  intVarCount = 0;
244  iv = IntVarArray(*this, intVars);
245  iv_introduced = std::vector<bool>(intVars);
246  iv_boolalias = alloc<int>(intVars+(intVars==0?1:0));
247  boolVarCount = 0;
248  bv = BoolVarArray(*this, boolVars);
249  bv_introduced = std::vector<bool>(boolVars);
250 #ifdef GECODE_HAS_SET_VARS
251  setVarCount = 0;
252  sv = SetVarArray(*this, setVars);
253  sv_introduced = std::vector<bool>(setVars);
254 #endif
255  }
256 
257  void
259  if (vs->alias) {
260  iv[intVarCount++] = iv[vs->i];
261  } else {
262  IntSet dom(vs2is(vs));
263  if (dom.size()==0) {
264  fail();
265  return;
266  } else {
267  iv[intVarCount++] = IntVar(*this, dom);
268  }
269  }
271  iv_boolalias[intVarCount-1] = -1;
272  }
273 
274  void
276  iv_boolalias[iv] = bv;
277  }
278  int
280  return iv_boolalias[iv];
281  }
282 
283  void
285  if (vs->alias) {
286  bv[boolVarCount++] = bv[vs->i];
287  } else {
288  bv[boolVarCount++] = BoolVar(*this, vs2bsl(vs), vs2bsh(vs));
289  }
291  }
292 
293 #ifdef GECODE_HAS_SET_VARS
294  void
296  if (vs->alias) {
297  sv[setVarCount++] = sv[vs->i];
298  } else if (vs->assigned) {
299  assert(vs->upperBound());
300  AST::SetLit* vsv = vs->upperBound.some();
301  if (vsv->interval) {
302  IntSet d(vsv->min, vsv->max);
303  sv[setVarCount++] = SetVar(*this, d, d);
304  } else {
305  int* is = heap.alloc<int>(static_cast<unsigned long int>(vsv->s.size()));
306  for (int i=vsv->s.size(); i--; )
307  is[i] = vsv->s[i];
308  IntSet d(is, vsv->s.size());
309  heap.free(is,static_cast<unsigned long int>(vsv->s.size()));
310  sv[setVarCount++] = SetVar(*this, d, d);
311  }
312  } else if (vs->upperBound()) {
313  AST::SetLit* vsv = vs->upperBound.some();
314  if (vsv->interval) {
315  IntSet d(vsv->min, vsv->max);
316  sv[setVarCount++] = SetVar(*this, IntSet::empty, d);
317  } else {
318  int* is = heap.alloc<int>(static_cast<unsigned long int>(vsv->s.size()));
319  for (int i=vsv->s.size(); i--; )
320  is[i] = vsv->s[i];
321  IntSet d(is, vsv->s.size());
322  heap.free(is,static_cast<unsigned long int>(vsv->s.size()));
323  sv[setVarCount++] = SetVar(*this, IntSet::empty, d);
324  }
325  } else {
326  sv[setVarCount++] = SetVar(*this, IntSet::empty,
329  }
331  }
332 #else
333  void
335  throw FlatZinc::Error("Gecode", "set variables not supported");
336  }
337 #endif
338 
339  void
341  try {
342  registry().post(*this, ce, ann);
343  } catch (Gecode::Exception& e) {
344  throw FlatZinc::Error("Gecode", e.what());
345  } catch (AST::TypeError& e) {
346  throw FlatZinc::Error("Type error", e.what());
347  }
348  }
349 
350  void flattenAnnotations(AST::Array* ann, std::vector<AST::Node*>& out) {
351  for (unsigned int i=0; i<ann->a.size(); i++) {
352  if (ann->a[i]->isCall("seq_search")) {
353  AST::Call* c = ann->a[i]->getCall();
354  if (c->args->isArray())
355  flattenAnnotations(c->args->getArray(), out);
356  else
357  out.push_back(c->args);
358  } else {
359  out.push_back(ann->a[i]);
360  }
361  }
362  }
363 
364  void
366  bool ignoreUnknown,
367  std::ostream& err) {
368  VarBranchOptions varbo;
369  varbo.seed = seed;
370  ValBranchOptions valbo;
371  valbo.seed = seed;
372  if (ann) {
373  std::vector<AST::Node*> flatAnn;
374  if (ann->isArray()) {
375  flattenAnnotations(ann->getArray() , flatAnn);
376  } else {
377  flatAnn.push_back(ann);
378  }
379 
380  for (unsigned int i=0; i<flatAnn.size(); i++) {
381  if (flatAnn[i]->isCall("gecode_search")) {
382  AST::Call* c = flatAnn[i]->getCall();
383  branchWithPlugin(c->args);
384  } else try {
385  AST::Call *call = flatAnn[i]->getCall("int_search");
386  AST::Array *args = call->getArgs(4);
387  AST::Array *vars = args->a[0]->getArray();
388  int k=vars->a.size();
389  for (int i=vars->a.size(); i--;)
390  if (vars->a[i]->isInt())
391  k--;
392  IntVarArgs va(k);
393  k=0;
394  for (unsigned int i=0; i<vars->a.size(); i++) {
395  if (vars->a[i]->isInt())
396  continue;
397  va[k++] = iv[vars->a[i]->getIntVar()];
398  }
399  branch(*this, va, ann2ivarsel(args->a[1]), ann2ivalsel(args->a[2]),
400  varbo,valbo);
401  } catch (AST::TypeError& e) {
402  try {
403  AST::Call *call = flatAnn[i]->getCall("int_assign");
404  AST::Array *args = call->getArgs(2);
405  AST::Array *vars = args->a[0]->getArray();
406  int k=vars->a.size();
407  for (int i=vars->a.size(); i--;)
408  if (vars->a[i]->isInt())
409  k--;
410  IntVarArgs va(k);
411  k=0;
412  for (unsigned int i=0; i<vars->a.size(); i++) {
413  if (vars->a[i]->isInt())
414  continue;
415  va[k++] = iv[vars->a[i]->getIntVar()];
416  }
417  assign(*this, va, ann2asnivalsel(args->a[1]));
418  } catch (AST::TypeError& e) {
419  (void) e;
420  try {
421  AST::Call *call = flatAnn[i]->getCall("bool_search");
422  AST::Array *args = call->getArgs(4);
423  AST::Array *vars = args->a[0]->getArray();
424  int k=vars->a.size();
425  for (int i=vars->a.size(); i--;)
426  if (vars->a[i]->isBool())
427  k--;
428  BoolVarArgs va(k);
429  k=0;
430  for (unsigned int i=0; i<vars->a.size(); i++) {
431  if (vars->a[i]->isBool())
432  continue;
433  va[k++] = bv[vars->a[i]->getBoolVar()];
434  }
435  branch(*this, va, ann2ivarsel(args->a[1]),
436  ann2ivalsel(args->a[2]), varbo, valbo);
437  } catch (AST::TypeError& e) {
438  (void) e;
439 #ifdef GECODE_HAS_SET_VARS
440  try {
441  AST::Call *call = flatAnn[i]->getCall("set_search");
442  AST::Array *args = call->getArgs(4);
443  AST::Array *vars = args->a[0]->getArray();
444  int k=vars->a.size();
445  for (int i=vars->a.size(); i--;)
446  if (vars->a[i]->isSet())
447  k--;
448  SetVarArgs va(k);
449  k=0;
450  for (unsigned int i=0; i<vars->a.size(); i++) {
451  if (vars->a[i]->isSet())
452  continue;
453  va[k++] = sv[vars->a[i]->getSetVar()];
454  }
455  branch(*this, va, ann2svarsel(args->a[1]),
456  ann2svalsel(args->a[2]), varbo, valbo);
457  } catch (AST::TypeError& e) {
458  (void) e;
459  if (!ignoreUnknown) {
460  err << "Warning, ignored search annotation: ";
461  flatAnn[i]->print(err);
462  err << std::endl;
463  }
464  }
465 #else
466  if (!ignoreUnknown) {
467  err << "Warning, ignored search annotation: ";
468  flatAnn[i]->print(err);
469  err << std::endl;
470  }
471 #endif
472  }
473  }
474  }
475  }
476  }
477  int introduced = 0;
478  for (int i=iv.size(); i--;)
479  if (iv_introduced[i])
480  introduced++;
481  IntVarArgs iv_sol(iv.size()-introduced);
482  IntVarArgs iv_tmp(introduced);
483  for (int i=iv.size(), j=0, k=0; i--;)
484  if (iv_introduced[i])
485  iv_tmp[j++] = iv[i];
486  else
487  iv_sol[k++] = iv[i];
488 
489  introduced = 0;
490  for (int i=bv.size(); i--;)
491  if (bv_introduced[i])
492  introduced++;
493  BoolVarArgs bv_sol(bv.size()-introduced);
494  BoolVarArgs bv_tmp(introduced);
495  for (int i=bv.size(), j=0, k=0; i--;)
496  if (bv_introduced[i])
497  bv_tmp[j++] = bv[i];
498  else
499  bv_sol[k++] = bv[i];
500 
501  branch(*this, iv_sol, INT_VAR_SIZE_AFC_MIN, INT_VAL_MIN);
502  branch(*this, bv_sol, INT_VAR_AFC_MAX, INT_VAL_MIN);
503 #ifdef GECODE_HAS_SET_VARS
504  introduced = 0;
505  for (int i=sv.size(); i--;)
506  if (sv_introduced[i])
507  introduced++;
508  SetVarArgs sv_sol(sv.size()-introduced);
509  SetVarArgs sv_tmp(introduced);
510  for (int i=sv.size(), j=0, k=0; i--;)
511  if (sv_introduced[i])
512  sv_tmp[j++] = sv[i];
513  else
514  sv_sol[k++] = sv[i];
516 #endif
517  branch(*this, iv_tmp, INT_VAR_SIZE_AFC_MIN, INT_VAL_MIN);
518  branch(*this, bv_tmp, INT_VAR_AFC_MAX, INT_VAL_MIN);
519 #ifdef GECODE_HAS_SET_VARS
521 #endif
522  }
523 
524  AST::Array*
526  return _solveAnnotations;
527  }
528 
529  void
531  _method = SAT;
532  _solveAnnotations = ann;
533  }
534 
535  void
537  _method = MIN;
538  _optVar = var;
539  _solveAnnotations = ann;
540  // Branch on optimization variable to ensure that it is given a value.
541  AST::Array* args = new AST::Array(4);
542  args->a[0] = new AST::Array(new AST::IntVar(_optVar));
543  args->a[1] = new AST::Atom("input_order");
544  args->a[2] = new AST::Atom("indomain_min");
545  args->a[3] = new AST::Atom("complete");
546  AST::Call* c = new AST::Call("int_search", args);
547  if (!ann)
548  ann = new AST::Array(c);
549  else
550  ann->a.push_back(c);
551  }
552 
553  void
555  _method = MAX;
556  _optVar = var;
557  _solveAnnotations = ann;
558  // Branch on optimization variable to ensure that it is given a value.
559  AST::Array* args = new AST::Array(4);
560  args->a[0] = new AST::Array(new AST::IntVar(_optVar));
561  args->a[1] = new AST::Atom("input_order");
562  args->a[2] = new AST::Atom("indomain_min");
563  args->a[3] = new AST::Atom("complete");
564  AST::Call* c = new AST::Call("int_search", args);
565  if (!ann)
566  ann = new AST::Array(c);
567  else
568  ann->a.push_back(c);
569  }
570 
572  delete _solveAnnotations;
573  }
574 
575 #ifdef GECODE_HAS_GIST
576 
580  template<class Engine>
581  class GistEngine {
582  };
583 
585  template<typename S>
586  class GistEngine<DFS<S> > {
587  public:
588  static void explore(S* root, const FlatZincOptions& opt,
589  Gist::Inspector* i) {
591  o.c_d = opt.c_d(); o.a_d = opt.a_d();
592  o.inspect.click(i);
593  (void) Gecode::Gist::dfs(root, o);
594  }
595  };
596 
598  template<typename S>
599  class GistEngine<BAB<S> > {
600  public:
601  static void explore(S* root, const FlatZincOptions& opt,
602  Gist::Inspector* i) {
604  o.c_d = opt.c_d(); o.a_d = opt.a_d();
605  o.inspect.click(i);
606  (void) Gecode::Gist::bab(root, o);
607  }
608  };
609 
611  template<typename S>
612  class GistEngine<Restart<S> > {
613  public:
614  static void explore(S* root, const FlatZincOptions& opt,
615  Gist::Inspector* i) {
617  o.c_d = opt.c_d(); o.a_d = opt.a_d();
618  o.inspect.click(i);
619  (void) Gecode::Gist::bab(root, o);
620  }
621  };
622 
624  template<class S>
625  class FZPrintingInspector
627  private:
628  const Printer& p;
629  public:
631  FZPrintingInspector(const Printer& p0);
633  virtual void inspect(const Space& node);
635  virtual void finalize(void);
636  };
637 
638  template<class S>
639  FZPrintingInspector<S>::FZPrintingInspector(const Printer& p0)
640  : TextOutput("Gecode/FlatZinc"), p(p0) {}
641 
642  template<class S>
643  void
644  FZPrintingInspector<S>::inspect(const Space& node) {
645  init();
646  dynamic_cast<const S&>(node).print(getStream(), p);
647  getStream() << std::endl;
648  }
649 
650  template<class S>
651  void
652  FZPrintingInspector<S>::finalize(void) {
654  }
655 
656 #endif
657 
658  template<template<class> class Engine>
659  void
660  FlatZincSpace::runEngine(std::ostream& out, const Printer& p,
661  const FlatZincOptions& opt, Support::Timer& t_total) {
662 #ifdef GECODE_HAS_GIST
663  if (opt.mode() == SM_GIST) {
664  FZPrintingInspector<FlatZincSpace> pi(p);
665  (void) GistEngine<Engine<FlatZincSpace> >::explore(this,opt,&pi);
666  return;
667  }
668 #endif
669  StatusStatistics sstat;
670  unsigned int n_p = 0;
671  Support::Timer t_solve;
672  t_solve.start();
673  if (status(sstat) != SS_FAILED) {
674  n_p = propagators();
675  }
676  Search::Options o;
677  o.stop = Driver::Cutoff::create(opt.node(), opt.fail(), opt.time(),
678  true);
679  o.c_d = opt.c_d();
680  o.a_d = opt.a_d();
681  o.threads = opt.threads();
683  Engine<FlatZincSpace> se(this,o);
684  int noOfSolutions = _method == SAT ? opt.solutions() : 0;
685  bool printAll = _method == SAT || opt.allSolutions();
686  int findSol = noOfSolutions;
687  FlatZincSpace* sol = NULL;
688  while (FlatZincSpace* next_sol = se.next()) {
689  delete sol;
690  sol = next_sol;
691  if (printAll) {
692  sol->print(out, p);
693  out << "----------" << std::endl;
694  }
695  if (--findSol==0)
696  goto stopped;
697  }
698  if (sol && !printAll) {
699  sol->print(out, p);
700  out << "----------" << std::endl;
701  }
702  if (!se.stopped()) {
703  if (sol) {
704  out << "==========" << endl;
705  } else {
706  out << "=====UNSATISFIABLE=====" << endl;
707  }
708  } else if (!sol) {
709  out << "=====UNKNOWN=====" << endl;
710  }
711  delete sol;
712  stopped:
714  if (opt.mode() == SM_STAT) {
715  Gecode::Search::Statistics stat = se.statistics();
716  out << endl
717  << "%% runtime: ";
718  Driver::stop(t_total,out);
719  out << endl
720  << "%% solvetime: ";
721  Driver::stop(t_solve,out);
722  out << endl
723  << "%% solutions: "
724  << std::abs(noOfSolutions - findSol) << endl
725  << "%% variables: "
726  << (intVarCount + boolVarCount + setVarCount) << endl
727  << "%% propagators: " << n_p << endl
728  << "%% propagations: " << sstat.propagate+stat.propagate << endl
729  << "%% nodes: " << stat.node << endl
730  << "%% failures: " << stat.fail << endl
731  << "%% peak depth: " << stat.depth << endl
732  << "%% peak memory: "
733  << static_cast<int>((stat.memory+1023) / 1024) << " KB"
734  << endl;
735  }
736  }
737 
738 #ifdef GECODE_HAS_QT
739  void
740  FlatZincSpace::branchWithPlugin(AST::Node* ann) {
741  if (AST::Call* c = dynamic_cast<AST::Call*>(ann)) {
742  QString pluginName(c->id.c_str());
743  if (QLibrary::isLibrary(pluginName+".dll")) {
744  pluginName += ".dll";
745  } else if (QLibrary::isLibrary(pluginName+".dylib")) {
746  pluginName = "lib" + pluginName + ".dylib";
747  } else if (QLibrary::isLibrary(pluginName+".so")) {
748  // Must check .so after .dylib so that Mac OS uses .dylib
749  pluginName = "lib" + pluginName + ".so";
750  }
751  QPluginLoader pl(pluginName);
752  QObject* plugin_o = pl.instance();
753  if (!plugin_o) {
754  throw FlatZinc::Error("FlatZinc",
755  "Error loading plugin "+pluginName.toStdString()+
756  ": "+pl.errorString().toStdString());
757  }
758  BranchPlugin* pb = qobject_cast<BranchPlugin*>(plugin_o);
759  if (!pb) {
760  throw FlatZinc::Error("FlatZinc",
761  "Error loading plugin "+pluginName.toStdString()+
762  ": does not contain valid PluginBrancher");
763  }
764  pb->branch(*this, c);
765  }
766  }
767 #else
768  void
769  FlatZincSpace::branchWithPlugin(AST::Node* ann) {
770  throw FlatZinc::Error("FlatZinc",
771  "Branching with plugins not supported (requires Qt support)");
772  }
773 #endif
774 
775  void
776  FlatZincSpace::run(std::ostream& out, const Printer& p,
777  const FlatZincOptions& opt, Support::Timer& t_total) {
778  switch (_method) {
779  case MIN:
780  case MAX:
782  runEngine<BAB>(out,p,opt,t_total);
783  else
784  runEngine<Restart>(out,p,opt,t_total);
785  break;
786  case SAT:
787  runEngine<DFS>(out,p,opt,t_total);
788  break;
789  }
790  }
791 
792  void
794  if (_method == MIN)
795  rel(*this, iv[_optVar], IRT_LE,
796  static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
797  else if (_method == MAX)
798  rel(*this, iv[_optVar], IRT_GR,
799  static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
800  }
801 
802  Space*
803  FlatZincSpace::copy(bool share) {
804  return new FlatZincSpace(share, *this);
805  }
806 
808  FlatZincSpace::method(void) const {
809  return _method;
810  }
811 
812  int
813  FlatZincSpace::optVar(void) const {
814  return _optVar;
815  }
816 
817  void
818  FlatZincSpace::print(std::ostream& out, const Printer& p) const {
819  p.print(out, iv, bv
820 #ifdef GECODE_HAS_SET_VARS
821  , sv
822 #endif
823  );
824  }
825 
826  void
828  p.shrinkArrays(*this, _optVar, iv, bv
829 #ifdef GECODE_HAS_SET_VARS
830  , sv
831 #endif
832  );
833  }
834 
835  void
837  _output = output;
838  }
839 
840  void
841  Printer::printElem(std::ostream& out,
842  AST::Node* ai,
843  const Gecode::IntVarArray& iv,
844  const Gecode::BoolVarArray& bv
845 #ifdef GECODE_HAS_SET_VARS
846  , const Gecode::SetVarArray& sv
847 #endif
848  ) const {
849  int k;
850  if (ai->isInt(k)) {
851  out << k;
852  } else if (ai->isIntVar()) {
853  out << iv[ai->getIntVar()];
854  } else if (ai->isBoolVar()) {
855  if (bv[ai->getBoolVar()].min() == 1) {
856  out << "true";
857  } else if (bv[ai->getBoolVar()].max() == 0) {
858  out << "false";
859  } else {
860  out << "false..true";
861  }
862 #ifdef GECODE_HAS_SET_VARS
863  } else if (ai->isSetVar()) {
864  if (!sv[ai->getSetVar()].assigned()) {
865  out << sv[ai->getSetVar()];
866  return;
867  }
868  SetVarGlbRanges svr(sv[ai->getSetVar()]);
869  if (!svr()) {
870  out << "{}";
871  return;
872  }
873  int min = svr.min();
874  int max = svr.max();
875  ++svr;
876  if (svr()) {
877  SetVarGlbValues svv(sv[ai->getSetVar()]);
878  int i = svv.val();
879  out << "{" << i;
880  ++svv;
881  for (; svv(); ++svv)
882  out << ", " << svv.val();
883  out << "}";
884  } else {
885  out << min << ".." << max;
886  }
887 #endif
888  } else if (ai->isBool()) {
889  out << (ai->getBool() ? "true" : "false");
890  } else if (ai->isSet()) {
891  AST::SetLit* s = ai->getSet();
892  if (s->interval) {
893  out << s->min << ".." << s->max;
894  } else {
895  out << "{";
896  for (unsigned int i=0; i<s->s.size(); i++) {
897  out << s->s[i] << (i < s->s.size()-1 ? ", " : "}");
898  }
899  }
900  } else if (ai->isString()) {
901  std::string s = ai->getString();
902  for (unsigned int i=0; i<s.size(); i++) {
903  if (s[i] == '\\' && i<s.size()-1) {
904  switch (s[i+1]) {
905  case 'n': out << "\n"; break;
906  case '\\': out << "\\"; break;
907  case 't': out << "\t"; break;
908  default: out << "\\" << s[i+1];
909  }
910  i++;
911  } else {
912  out << s[i];
913  }
914  }
915  }
916  }
917 
918  void
919  Printer::print(std::ostream& out,
920  const Gecode::IntVarArray& iv,
921  const Gecode::BoolVarArray& bv
922 #ifdef GECODE_HAS_SET_VARS
923  ,
924  const Gecode::SetVarArray& sv
925 #endif
926  ) const {
927  if (_output == NULL)
928  return;
929  for (unsigned int i=0; i< _output->a.size(); i++) {
930  AST::Node* ai = _output->a[i];
931  if (ai->isArray()) {
932  AST::Array* aia = ai->getArray();
933  int size = aia->a.size();
934  out << "[";
935  for (int j=0; j<size; j++) {
936  printElem(out,aia->a[j],iv,bv
937 #ifdef GECODE_HAS_SET_VARS
938  ,sv
939 #endif
940  );
941  if (j<size-1)
942  out << ", ";
943  }
944  out << "]";
945  } else {
946  printElem(out,ai,iv,bv
947 #ifdef GECODE_HAS_SET_VARS
948  ,sv
949 #endif
950  );
951  }
952  }
953  }
954 
955  void
957  std::map<int,int>& iv, std::map<int,int>& bv,
958  std::map<int,int>& sv) {
959  if (node->isIntVar()) {
960  AST::IntVar* x = static_cast<AST::IntVar*>(node);
961  if (iv.find(x->i) == iv.end()) {
962  int newi = iv.size();
963  iv[x->i] = newi;
964  }
965  x->i = iv[x->i];
966  } else if (node->isBoolVar()) {
967  AST::BoolVar* x = static_cast<AST::BoolVar*>(node);
968  if (bv.find(x->i) == bv.end()) {
969  int newi = bv.size();
970  bv[x->i] = newi;
971  }
972  x->i = bv[x->i];
973  } else if (node->isSetVar()) {
974  AST::SetVar* x = static_cast<AST::SetVar*>(node);
975  if (sv.find(x->i) == sv.end()) {
976  int newi = sv.size();
977  sv[x->i] = newi;
978  }
979  x->i = sv[x->i];
980  }
981  }
982 
983  void
985  int& optVar,
988 #ifdef GECODE_HAS_SET_VARS
989  ,
991 #endif
992  ) {
993  if (_output == NULL) {
994  if (optVar == -1) {
995  iv = IntVarArray(home, 0);
996  } else {
997  IntVar ov = iv[optVar];
998  iv = IntVarArray(home, 1);
999  iv[0] = ov;
1000  optVar = 0;
1001  }
1002  bv = BoolVarArray(home, 0);
1003 #ifdef GECODE_HAS_SET_VARS
1004  sv = SetVarArray(home, 0);
1005 #endif
1006  return;
1007  }
1008  std::map<int,int> iv_new;
1009  std::map<int,int> bv_new;
1010  std::map<int,int> sv_new;
1011 
1012  if (optVar != -1) {
1013  iv_new[optVar] = 0;
1014  optVar = 0;
1015  }
1016 
1017  for (unsigned int i=0; i< _output->a.size(); i++) {
1018  AST::Node* ai = _output->a[i];
1019  if (ai->isArray()) {
1020  AST::Array* aia = ai->getArray();
1021  for (unsigned int j=0; j<aia->a.size(); j++) {
1022  shrinkElement(aia->a[j],iv_new,bv_new,sv_new);
1023  }
1024  } else {
1025  shrinkElement(ai,iv_new,bv_new,sv_new);
1026  }
1027  }
1028 
1029  IntVarArgs iva(iv_new.size());
1030  for (map<int,int>::iterator i=iv_new.begin(); i != iv_new.end(); ++i) {
1031  iva[(*i).second] = iv[(*i).first];
1032  }
1033  iv = IntVarArray(home, iva);
1034 
1035  BoolVarArgs bva(bv_new.size());
1036  for (map<int,int>::iterator i=bv_new.begin(); i != bv_new.end(); ++i) {
1037  bva[(*i).second] = bv[(*i).first];
1038  }
1039  bv = BoolVarArray(home, bva);
1040 
1041 #ifdef GECODE_HAS_SET_VARS
1042  SetVarArgs sva(sv_new.size());
1043  for (map<int,int>::iterator i=sv_new.begin(); i != sv_new.end(); ++i) {
1044  sva[(*i).second] = sv[(*i).first];
1045  }
1046  sv = SetVarArray(home, sva);
1047 #endif
1048  }
1049 
1051  delete _output;
1052  }
1053 
1054 }}
1055 
1056 // STATISTICS: flatzinc-any