Generated on Sat May 25 2013 18:00:32 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  * Contributing authors:
7  * Gabriel Hjort Blindell <gabriel.hjort.blindell@gmail.com>
8  *
9  * Copyright:
10  * Guido Tack, 2007-2012
11  * Gabriel Hjort Blindell, 2012
12  *
13  * Last modified:
14  * $Date: 2013-03-07 20:40:42 +0100 (Thu, 07 Mar 2013) $ by $Author: schulte $
15  * $Revision: 13462 $
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 using namespace std;
51 
52 namespace Gecode { namespace FlatZinc {
53 
66  class AuxVarBrancher : public Brancher {
67  protected:
69  bool done;
71  AuxVarBrancher(Home home) : Brancher(home), done(false) {}
73  AuxVarBrancher(Space& home, bool share, AuxVarBrancher& b)
74  : Brancher(home, share, b), done(b.done) {}
75 
77  class Choice : public Gecode::Choice {
78  public:
80  bool fail;
82  Choice(const Brancher& b, bool fail0)
83  : Gecode::Choice(b,1), fail(fail0) {}
85  virtual size_t size(void) const {
86  return sizeof(Choice);
87  }
89  virtual void archive(Archive& e) const {
91  e.put(fail);
92  }
93  };
94 
95 
96  public:
98  virtual bool status(const Space& _home) const {
99  if (done) return false;
100  const FlatZincSpace& home = static_cast<const FlatZincSpace&>(_home);
101  for (int i=0; i<home.iv_aux.size(); i++)
102  if (!home.iv_aux[i].assigned()) return true;
103  for (int i=0; i<home.bv_aux.size(); i++)
104  if (!home.bv_aux[i].assigned()) return true;
105 #ifdef GECODE_HAS_SET_VARS
106  for (int i=0; i<home.sv_aux.size(); i++)
107  if (!home.sv_aux[i].assigned()) return true;
108 #endif
109 #ifdef GECODE_HAS_FLOAT_VARS
110  for (int i=0; i<home.fv_aux.size(); i++)
111  if (!home.fv_aux[i].assigned()) return true;
112 #endif
113  // No non-assigned variables left
114  return false;
115  }
117  virtual Choice* choice(Space& home) {
118  done = true;
119  FlatZincSpace& fzs = static_cast<FlatZincSpace&>(*home.clone());
120  fzs.needAuxVars = false;
123 #ifdef GECODE_HAS_SET_VARS
125 #endif
126 #ifdef GECODE_HAS_FLOAT_VARS
128 #endif
129  Search::Options opt; opt.clone = false;
130  FlatZincSpace* sol = dfs(&fzs, opt);
131  if (sol) {
132  delete sol;
133  return new Choice(*this,false);
134  } else {
135  return new Choice(*this,true);
136  }
137  }
139  virtual Choice* choice(const Space&, Archive& e) {
140  bool fail; e >> fail;
141  return new Choice(*this, fail);
142  }
144  virtual ExecStatus commit(Space&, const Gecode::Choice& c, unsigned int) {
145  return static_cast<const Choice&>(c).fail ? ES_FAILED : ES_OK;
146  }
148  virtual Actor* copy(Space& home, bool share) {
149  return new (home) AuxVarBrancher(home, share, *this);
150  }
152  static void post(Home home) {
153  (void) new (home) AuxVarBrancher(home);
154  }
156  virtual size_t dispose(Space&) {
157  return sizeof(*this);
158  }
159  };
160 
161 
163  if (vs->assigned) {
164  return IntSet(vs->i,vs->i);
165  }
166  if (vs->domain()) {
167  AST::SetLit* sl = vs->domain.some();
168  if (sl->interval) {
169  return IntSet(sl->min, sl->max);
170  } else {
171  int* newdom = heap.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
172  for (int i=sl->s.size(); i--;)
173  newdom[i] = sl->s[i];
174  IntSet ret(newdom, sl->s.size());
175  heap.free(newdom, static_cast<unsigned long int>(sl->s.size()));
176  return ret;
177  }
178  }
180  }
181 
182  int vs2bsl(BoolVarSpec* bs) {
183  if (bs->assigned) {
184  return bs->i;
185  }
186  if (bs->domain()) {
187  AST::SetLit* sl = bs->domain.some();
188  assert(sl->interval);
189  return std::min(1, std::max(0, sl->min));
190  }
191  return 0;
192  }
193 
194  int vs2bsh(BoolVarSpec* bs) {
195  if (bs->assigned) {
196  return bs->i;
197  }
198  if (bs->domain()) {
199  AST::SetLit* sl = bs->domain.some();
200  assert(sl->interval);
201  return std::max(0, std::min(1, sl->max));
202  }
203  return 1;
204  }
205 
206  TieBreak<IntVarBranch> ann2ivarsel(AST::Node* ann, int seed, double decay) {
207  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
208  if (s->id == "input_order")
210  if (s->id == "first_fail")
212  if (s->id == "anti_first_fail")
214  if (s->id == "smallest")
216  if (s->id == "largest")
218  if (s->id == "occurrence")
220  if (s->id == "max_regret")
222  if (s->id == "most_constrained")
225  if (s->id == "random") {
226  Rnd r(static_cast<unsigned int>(seed));
228  }
229  if (s->id == "afc_min")
231  if (s->id == "afc_max")
233  if (s->id == "afc_size_min")
235  if (s->id == "afc_size_max") {
237  }
238  if (s->id == "activity_min")
240  if (s->id == "activity_max")
242  if (s->id == "activity_size_min")
244  if (s->id == "activity_size_max")
246  }
247  std::cerr << "Warning, ignored search annotation: ";
248  ann->print(std::cerr);
249  std::cerr << std::endl;
251  }
252 
254  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
255  if (s->id == "indomain_min")
256  return INT_VAL_MIN();
257  if (s->id == "indomain_max")
258  return INT_VAL_MAX();
259  if (s->id == "indomain_median")
260  return INT_VAL_MED();
261  if (s->id == "indomain_split")
262  return INT_VAL_SPLIT_MIN();
263  if (s->id == "indomain_reverse_split")
264  return INT_VAL_SPLIT_MAX();
265  if (s->id == "indomain_random") {
266  Rnd r(static_cast<unsigned int>(seed));
267  return INT_VAL_RND(r);
268  }
269  if (s->id == "indomain")
270  return INT_VALUES_MIN();
271  if (s->id == "indomain_middle") {
272  std::cerr << "Warning, replacing unsupported annotation "
273  << "indomain_middle with indomain_median" << std::endl;
274  return INT_VAL_MED();
275  }
276  if (s->id == "indomain_interval") {
277  std::cerr << "Warning, replacing unsupported annotation "
278  << "indomain_interval with indomain_split" << std::endl;
279  return INT_VAL_SPLIT_MIN();
280  }
281  }
282  std::cerr << "Warning, ignored search annotation: ";
283  ann->print(std::cerr);
284  std::cerr << std::endl;
285  return INT_VAL_MIN();
286  }
287 
289  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
290  if (s->id == "indomain_min")
291  return INT_ASSIGN_MIN();
292  if (s->id == "indomain_max")
293  return INT_ASSIGN_MAX();
294  if (s->id == "indomain_median")
295  return INT_ASSIGN_MED();
296  if (s->id == "indomain_random") {
297  Rnd r(static_cast<unsigned int>(seed));
298  return INT_ASSIGN_RND(r);
299  }
300  }
301  std::cerr << "Warning, ignored search annotation: ";
302  ann->print(std::cerr);
303  std::cerr << std::endl;
304  return INT_ASSIGN_MIN();
305  }
306 
307 #ifdef GECODE_HAS_SET_VARS
308  SetVarBranch ann2svarsel(AST::Node* ann, int seed, double decay) {
309  (void) seed;
310  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
311  if (s->id == "input_order")
312  return SET_VAR_NONE();
313  if (s->id == "first_fail")
314  return SET_VAR_SIZE_MIN();
315  if (s->id == "anti_first_fail")
316  return SET_VAR_SIZE_MAX();
317  if (s->id == "smallest")
318  return SET_VAR_MIN_MIN();
319  if (s->id == "largest")
320  return SET_VAR_MAX_MAX();
321  if (s->id == "afc_min")
322  return SET_VAR_AFC_MIN(decay);
323  if (s->id == "afc_max")
324  return SET_VAR_AFC_MAX(decay);
325  if (s->id == "afc_size_min")
326  return SET_VAR_AFC_SIZE_MIN(decay);
327  if (s->id == "afc_size_max")
328  return SET_VAR_AFC_SIZE_MAX(decay);
329  if (s->id == "activity_min")
330  return SET_VAR_ACTIVITY_MIN(decay);
331  if (s->id == "activity_max")
332  return SET_VAR_ACTIVITY_MAX(decay);
333  if (s->id == "activity_size_min")
334  return SET_VAR_ACTIVITY_SIZE_MIN(decay);
335  if (s->id == "activity_size_max")
336  return SET_VAR_ACTIVITY_SIZE_MAX(decay);
337  }
338  std::cerr << "Warning, ignored search annotation: ";
339  ann->print(std::cerr);
340  std::cerr << std::endl;
341  return SET_VAR_NONE();
342  }
343 
345  (void) seed;
346  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
347  if (s->id == "indomain_min")
348  return SET_VAL_MIN_INC();
349  if (s->id == "indomain_max")
350  return SET_VAL_MAX_INC();
351  if (s->id == "outdomain_min")
352  return SET_VAL_MIN_EXC();
353  if (s->id == "outdomain_max")
354  return SET_VAL_MAX_EXC();
355  }
356  std::cerr << "Warning, ignored search annotation: ";
357  ann->print(std::cerr);
358  std::cerr << std::endl;
359  return SET_VAL_MIN_INC();
360  }
361 #endif
362 
363 #ifdef GECODE_HAS_FLOAT_VARS
364  TieBreak<FloatVarBranch> ann2fvarsel(AST::Node* ann, int seed, double decay) {
365  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
366  if (s->id == "input_order")
368  if (s->id == "first_fail")
370  if (s->id == "anti_first_fail")
372  if (s->id == "smallest")
374  if (s->id == "largest")
376  if (s->id == "occurrence")
378  if (s->id == "most_constrained")
381  if (s->id == "random") {
382  Rnd r(static_cast<unsigned int>(seed));
384  }
385  if (s->id == "afc_min")
387  if (s->id == "afc_max")
389  if (s->id == "afc_size_min")
391  if (s->id == "afc_size_max")
393  if (s->id == "activity_min")
395  if (s->id == "activity_max")
397  if (s->id == "activity_size_min")
399  if (s->id == "activity_size_max")
401  }
402  std::cerr << "Warning, ignored search annotation: ";
403  ann->print(std::cerr);
404  std::cerr << std::endl;
406  }
407 
409  if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
410  if (s->id == "indomain_split")
411  return FLOAT_VAL_SPLIT_MIN();
412  if (s->id == "indomain_reverse_split")
413  return FLOAT_VAL_SPLIT_MAX();
414  }
415  std::cerr << "Warning, ignored search annotation: ";
416  ann->print(std::cerr);
417  std::cerr << std::endl;
418  return FLOAT_VAL_SPLIT_MIN();
419  }
420 
421 #endif
422 
423  FlatZincSpace::FlatZincSpace(bool share, FlatZincSpace& f)
424  : Space(share, f), _solveAnnotations(NULL), iv_boolalias(NULL),
425  needAuxVars(f.needAuxVars) {
426  _optVar = f._optVar;
427  _method = f._method;
428  iv.update(*this, share, f.iv);
430 
431  if (needAuxVars) {
432  IntVarArgs iva;
433  for (int i=0; i<f.iv_aux.size(); i++) {
434  if (!f.iv_aux[i].assigned()) {
435  iva << IntVar();
436  iva[iva.size()-1].update(*this, share, f.iv_aux[i]);
437  }
438  }
439  iv_aux = IntVarArray(*this, iva);
440  }
441 
442  bv.update(*this, share, f.bv);
444  if (needAuxVars) {
445  BoolVarArgs bva;
446  for (int i=0; i<f.bv_aux.size(); i++) {
447  if (!f.bv_aux[i].assigned()) {
448  bva << BoolVar();
449  bva[bva.size()-1].update(*this, share, f.bv_aux[i]);
450  }
451  }
452  bv_aux = BoolVarArray(*this, bva);
453  }
454 
455 #ifdef GECODE_HAS_SET_VARS
456  sv.update(*this, share, f.sv);
458  if (needAuxVars) {
459  SetVarArgs sva;
460  for (int i=0; i<f.sv_aux.size(); i++) {
461  if (!f.sv_aux[i].assigned()) {
462  sva << SetVar();
463  sva[sva.size()-1].update(*this, share, f.sv_aux[i]);
464  }
465  }
466  sv_aux = SetVarArray(*this, sva);
467  }
468 #endif
469 #ifdef GECODE_HAS_FLOAT_VARS
470  fv.update(*this, share, f.fv);
472  if (needAuxVars) {
473  FloatVarArgs fva;
474  for (int i=0; i<f.fv_aux.size(); i++) {
475  if (!f.fv_aux[i].assigned()) {
476  fva << FloatVar();
477  fva[fva.size()-1].update(*this, share, f.fv_aux[i]);
478  }
479  }
480  fv_aux = FloatVarArray(*this, fva);
481  }
482 #endif
483  }
484 
486  : intVarCount(-1), boolVarCount(-1), floatVarCount(-1), setVarCount(-1),
487  _optVar(-1), _solveAnnotations(NULL), needAuxVars(true) {}
488 
489  void
490  FlatZincSpace::init(int intVars, int boolVars,
491  int setVars, int floatVars) {
492  (void) setVars;
493  (void) floatVars;
494 
495  intVarCount = 0;
496  iv = IntVarArray(*this, intVars);
497  iv_introduced = std::vector<bool>(2*intVars);
498  iv_boolalias = alloc<int>(intVars+(intVars==0?1:0));
499  boolVarCount = 0;
500  bv = BoolVarArray(*this, boolVars);
501  bv_introduced = std::vector<bool>(2*boolVars);
502 #ifdef GECODE_HAS_SET_VARS
503  setVarCount = 0;
504  sv = SetVarArray(*this, setVars);
505  sv_introduced = std::vector<bool>(2*setVars);
506 #endif
507 #ifdef GECODE_HAS_FLOAT_VARS
508  floatVarCount = 0;
509  fv = FloatVarArray(*this, floatVars);
510  fv_introduced = std::vector<bool>(2*floatVars);
511 #endif
512  }
513 
514  void
516  if (vs->alias) {
517  iv[intVarCount++] = iv[vs->i];
518  } else {
519  IntSet dom(vs2is(vs));
520  if (dom.size()==0) {
521  fail();
522  return;
523  } else {
524  iv[intVarCount++] = IntVar(*this, dom);
525  }
526  }
527  iv_introduced[2*(intVarCount-1)] = vs->introduced;
528  iv_introduced[2*(intVarCount-1)+1] = vs->funcDep;
529  iv_boolalias[intVarCount-1] = -1;
530  }
531 
532  void
534  iv_boolalias[iv] = bv;
535  }
536  int
538  return iv_boolalias[iv];
539  }
540 
541  void
543  if (vs->alias) {
544  bv[boolVarCount++] = bv[vs->i];
545  } else {
546  bv[boolVarCount++] = BoolVar(*this, vs2bsl(vs), vs2bsh(vs));
547  }
549  bv_introduced[2*(boolVarCount-1)+1] = vs->funcDep;
550  }
551 
552 #ifdef GECODE_HAS_SET_VARS
553  void
555  if (vs->alias) {
556  sv[setVarCount++] = sv[vs->i];
557  } else if (vs->assigned) {
558  assert(vs->upperBound());
559  AST::SetLit* vsv = vs->upperBound.some();
560  if (vsv->interval) {
561  IntSet d(vsv->min, vsv->max);
562  sv[setVarCount++] = SetVar(*this, d, d);
563  } else {
564  int* is = heap.alloc<int>(static_cast<unsigned long int>(vsv->s.size()));
565  for (int i=vsv->s.size(); i--; )
566  is[i] = vsv->s[i];
567  IntSet d(is, vsv->s.size());
568  heap.free(is,static_cast<unsigned long int>(vsv->s.size()));
569  sv[setVarCount++] = SetVar(*this, d, d);
570  }
571  } else if (vs->upperBound()) {
572  AST::SetLit* vsv = vs->upperBound.some();
573  if (vsv->interval) {
574  IntSet d(vsv->min, vsv->max);
575  sv[setVarCount++] = SetVar(*this, IntSet::empty, d);
576  } else {
577  int* is = heap.alloc<int>(static_cast<unsigned long int>(vsv->s.size()));
578  for (int i=vsv->s.size(); i--; )
579  is[i] = vsv->s[i];
580  IntSet d(is, vsv->s.size());
581  heap.free(is,static_cast<unsigned long int>(vsv->s.size()));
582  sv[setVarCount++] = SetVar(*this, IntSet::empty, d);
583  }
584  } else {
585  sv[setVarCount++] = SetVar(*this, IntSet::empty,
588  }
589  sv_introduced[2*(setVarCount-1)] = vs->introduced;
590  sv_introduced[2*(setVarCount-1)+1] = vs->funcDep;
591  }
592 #else
593  void
595  throw FlatZinc::Error("Gecode", "set variables not supported");
596  }
597 #endif
598 
599 #ifdef GECODE_HAS_FLOAT_VARS
600  void
602  if (vs->alias) {
603  fv[floatVarCount++] = fv[vs->i];
604  } else {
605  double dmin, dmax;
606  if (vs->domain()) {
607  dmin = vs->domain.some().first;
608  dmax = vs->domain.some().second;
609  if (dmin > dmax) {
610  fail();
611  return;
612  }
613  } else {
614  dmin = Float::Limits::min;
615  dmax = Float::Limits::max;
616  }
617  fv[floatVarCount++] = FloatVar(*this, dmin, dmax);
618  }
620  fv_introduced[2*(floatVarCount-1)+1] = vs->funcDep;
621  }
622 #else
623  void
625  throw FlatZinc::Error("Gecode", "float variables not supported");
626  }
627 #endif
628 
629  void
631  try {
632  registry().post(*this, ce, ann);
633  } catch (Gecode::Exception& e) {
634  throw FlatZinc::Error("Gecode", e.what());
635  } catch (AST::TypeError& e) {
636  throw FlatZinc::Error("Type error", e.what());
637  }
638  }
639 
640  void flattenAnnotations(AST::Array* ann, std::vector<AST::Node*>& out) {
641  for (unsigned int i=0; i<ann->a.size(); i++) {
642  if (ann->a[i]->isCall("seq_search")) {
643  AST::Call* c = ann->a[i]->getCall();
644  if (c->args->isArray())
645  flattenAnnotations(c->args->getArray(), out);
646  else
647  out.push_back(c->args);
648  } else {
649  out.push_back(ann->a[i]);
650  }
651  }
652  }
653 
654  void
655  FlatZincSpace::createBranchers(AST::Node* ann, int seed, double decay,
656  bool ignoreUnknown,
657  std::ostream& err) {
658  if (ann) {
659  std::vector<AST::Node*> flatAnn;
660  if (ann->isArray()) {
661  flattenAnnotations(ann->getArray() , flatAnn);
662  } else {
663  flatAnn.push_back(ann);
664  }
665 
666  for (unsigned int i=0; i<flatAnn.size(); i++) {
667  if (flatAnn[i]->isCall("gecode_search")) {
668  AST::Call* c = flatAnn[i]->getCall();
669  branchWithPlugin(c->args);
670  } else if (flatAnn[i]->isCall("int_search")) {
671  AST::Call *call = flatAnn[i]->getCall("int_search");
672  AST::Array *args = call->getArgs(4);
673  AST::Array *vars = args->a[0]->getArray();
674  int k=vars->a.size();
675  for (int i=vars->a.size(); i--;)
676  if (vars->a[i]->isInt())
677  k--;
678  IntVarArgs va(k);
679  k=0;
680  for (unsigned int i=0; i<vars->a.size(); i++) {
681  if (vars->a[i]->isInt())
682  continue;
683  va[k++] = iv[vars->a[i]->getIntVar()];
684  }
685  branch(*this, va,
686  ann2ivarsel(args->a[1],seed,decay),
687  ann2ivalsel(args->a[2],seed));
688  } else if (flatAnn[i]->isCall("int_assign")) {
689  AST::Call *call = flatAnn[i]->getCall("int_assign");
690  AST::Array *args = call->getArgs(2);
691  AST::Array *vars = args->a[0]->getArray();
692  int k=vars->a.size();
693  for (int i=vars->a.size(); i--;)
694  if (vars->a[i]->isInt())
695  k--;
696  IntVarArgs va(k);
697  k=0;
698  for (unsigned int i=0; i<vars->a.size(); i++) {
699  if (vars->a[i]->isInt())
700  continue;
701  va[k++] = iv[vars->a[i]->getIntVar()];
702  }
703  assign(*this, va, ann2asnivalsel(args->a[1],seed));
704  } else if (flatAnn[i]->isCall("bool_search")) {
705  AST::Call *call = flatAnn[i]->getCall("bool_search");
706  AST::Array *args = call->getArgs(4);
707  AST::Array *vars = args->a[0]->getArray();
708  int k=vars->a.size();
709  for (int i=vars->a.size(); i--;)
710  if (vars->a[i]->isBool())
711  k--;
712  BoolVarArgs va(k);
713  k=0;
714  for (unsigned int i=0; i<vars->a.size(); i++) {
715  if (vars->a[i]->isBool())
716  continue;
717  va[k++] = bv[vars->a[i]->getBoolVar()];
718  }
719  branch(*this, va,
720  ann2ivarsel(args->a[1],seed,decay),
721  ann2ivalsel(args->a[2],seed));
722  } else if (flatAnn[i]->isCall("set_search")) {
723 #ifdef GECODE_HAS_SET_VARS
724  AST::Call *call = flatAnn[i]->getCall("set_search");
725  AST::Array *args = call->getArgs(4);
726  AST::Array *vars = args->a[0]->getArray();
727  int k=vars->a.size();
728  for (int i=vars->a.size(); i--;)
729  if (vars->a[i]->isSet())
730  k--;
731  SetVarArgs va(k);
732  k=0;
733  for (unsigned int i=0; i<vars->a.size(); i++) {
734  if (vars->a[i]->isSet())
735  continue;
736  va[k++] = sv[vars->a[i]->getSetVar()];
737  }
738  branch(*this, va,
739  ann2svarsel(args->a[1],seed,decay),
740  ann2svalsel(args->a[2],seed));
741 #else
742  if (!ignoreUnknown) {
743  err << "Warning, ignored search annotation: ";
744  flatAnn[i]->print(err);
745  err << std::endl;
746  }
747 #endif
748  }
749 #ifdef GECODE_HAS_FLOAT_VARS
750  else if (flatAnn[i]->isCall("float_search")) {
751  AST::Call *call = flatAnn[i]->getCall("float_search");
752  AST::Array *args = call->getArgs(5);
753  AST::Array *vars = args->a[0]->getArray();
754  int k=vars->a.size();
755  for (int i=vars->a.size(); i--;)
756  if (vars->a[i]->isFloat())
757  k--;
758  FloatVarArgs va(k);
759  k=0;
760  for (unsigned int i=0; i<vars->a.size(); i++) {
761  if (vars->a[i]->isFloat())
762  continue;
763  va[k++] = fv[vars->a[i]->getFloatVar()];
764  }
765  branch(*this, va,
766  ann2fvarsel(args->a[2],seed,decay),
767  ann2fvalsel(args->a[3]));
768  }
769 #endif
770  else {
771  if (!ignoreUnknown) {
772  err << "Warning, ignored search annotation: ";
773  flatAnn[i]->print(err);
774  err << std::endl;
775  }
776  }
777  }
778  }
779  int introduced = 0;
780  int funcdep = 0;
781  for (int i=iv.size(); i--;)
782  if (iv_introduced[2*i]) {
783  if (iv_introduced[2*i+1]) {
784  funcdep++;
785  } else {
786  introduced++;
787  }
788  }
789  IntVarArgs iv_sol(iv.size()-(introduced+funcdep));
790  IntVarArgs iv_tmp(introduced);
791  for (int i=iv.size(), j=0, k=0; i--;)
792  if (iv_introduced[2*i]) {
793  if (!iv_introduced[2*i+1]) {
794  iv_tmp[j++] = iv[i];
795  }
796  } else {
797  iv_sol[k++] = iv[i];
798  }
799 
800  introduced = 0;
801  funcdep = 0;
802  for (int i=bv.size(); i--;)
803  if (bv_introduced[2*i]) {
804  if (bv_introduced[2*i+1]) {
805  funcdep++;
806  } else {
807  introduced++;
808  }
809  }
810  BoolVarArgs bv_sol(bv.size()-(introduced+funcdep));
811  BoolVarArgs bv_tmp(introduced);
812  for (int i=bv.size(), j=0, k=0; i--;)
813  if (bv_introduced[2*i]) {
814  if (!bv_introduced[2*i+1]) {
815  bv_tmp[j++] = bv[i];
816  }
817  } else {
818  bv_sol[k++] = bv[i];
819  }
820 
821  branch(*this, iv_sol, INT_VAR_AFC_SIZE_MAX(0.99), INT_VAL_MIN());
822  branch(*this, bv_sol, INT_VAR_AFC_MAX(0.99), INT_VAL_MIN());
823 #ifdef GECODE_HAS_FLOAT_VARS
824  introduced = 0;
825  funcdep = 0;
826  for (int i=fv.size(); i--;)
827  if (fv_introduced[2*i]) {
828  if (fv_introduced[2*i+1]) {
829  funcdep++;
830  } else {
831  introduced++;
832  }
833  }
834  FloatVarArgs fv_sol(fv.size()-(introduced+funcdep));
835  FloatVarArgs fv_tmp(introduced);
836  for (int i=fv.size(), j=0, k=0; i--;)
837  if (fv_introduced[2*i]) {
838  if (!fv_introduced[2*i+1]) {
839  fv_tmp[j++] = fv[i];
840  }
841  } else {
842  fv_sol[k++] = fv[i];
843  }
844 
845  branch(*this, fv_sol, FLOAT_VAR_SIZE_MIN(), FLOAT_VAL_SPLIT_MIN());
846 #endif
847 #ifdef GECODE_HAS_SET_VARS
848  introduced = 0;
849  funcdep = 0;
850  for (int i=sv.size(); i--;)
851  if (sv_introduced[2*i]) {
852  if (sv_introduced[2*i+1]) {
853  funcdep++;
854  } else {
855  introduced++;
856  }
857  }
858  SetVarArgs sv_sol(sv.size()-(introduced+funcdep));
859  SetVarArgs sv_tmp(introduced);
860  for (int i=sv.size(), j=0, k=0; i--;)
861  if (sv_introduced[2*i]) {
862  if (!sv_introduced[2*i+1]) {
863  sv_tmp[j++] = sv[i];
864  }
865  } else {
866  sv_sol[k++] = sv[i];
867  }
868 
869  branch(*this, sv_sol, SET_VAR_AFC_SIZE_MAX(0.99), SET_VAL_MIN_INC());
870 #endif
871  iv_aux = IntVarArray(*this, iv_tmp);
872  bv_aux = BoolVarArray(*this, bv_tmp);
873 #ifdef GECODE_HAS_SET_VARS
874  sv_aux = SetVarArray(*this, sv_tmp);
875 #endif
876 #ifdef GECODE_HAS_FLOAT_VARS
877  fv_aux = FloatVarArray(*this, fv_tmp);
878 #endif
879  AuxVarBrancher::post(*this);
880  }
881 
882  AST::Array*
884  return _solveAnnotations;
885  }
886 
887  void
889  _method = SAT;
890  _solveAnnotations = ann;
891  }
892 
893  void
895  _method = MIN;
896  _optVar = var;
897  _solveAnnotations = ann;
898  // Branch on optimization variable to ensure that it is given a value.
899  AST::Array* args = new AST::Array(4);
900  args->a[0] = new AST::Array(new AST::IntVar(_optVar));
901  args->a[1] = new AST::Atom("input_order");
902  args->a[2] = new AST::Atom("indomain_min");
903  args->a[3] = new AST::Atom("complete");
904  AST::Call* c = new AST::Call("int_search", args);
905  if (!ann)
906  ann = new AST::Array(c);
907  else
908  ann->a.push_back(c);
909  }
910 
911  void
913  _method = MAX;
914  _optVar = var;
915  _solveAnnotations = ann;
916  // Branch on optimization variable to ensure that it is given a value.
917  AST::Array* args = new AST::Array(4);
918  args->a[0] = new AST::Array(new AST::IntVar(_optVar));
919  args->a[1] = new AST::Atom("input_order");
920  args->a[2] = new AST::Atom("indomain_min");
921  args->a[3] = new AST::Atom("complete");
922  AST::Call* c = new AST::Call("int_search", args);
923  if (!ann)
924  ann = new AST::Array(c);
925  else
926  ann->a.push_back(c);
927  }
928 
930  delete _solveAnnotations;
931  }
932 
933 #ifdef GECODE_HAS_GIST
934 
938  template<class Engine>
939  class GistEngine {
940  };
941 
943  template<typename S>
944  class GistEngine<DFS<S> > {
945  public:
946  static void explore(S* root, const FlatZincOptions& opt,
949  o.c_d = opt.c_d(); o.a_d = opt.a_d();
950  o.inspect.click(i);
951  o.inspect.compare(c);
952  (void) Gecode::Gist::dfs(root, o);
953  }
954  };
955 
957  template<typename S>
958  class GistEngine<BAB<S> > {
959  public:
960  static void explore(S* root, const FlatZincOptions& opt,
961  Gist::Inspector* i, Gist::Comparator* c) {
963  o.c_d = opt.c_d(); o.a_d = opt.a_d();
964  o.inspect.click(i);
965  o.inspect.compare(c);
966  (void) Gecode::Gist::bab(root, o);
967  }
968  };
969 
971  template<class S>
972  class FZPrintingInspector
974  private:
975  const Printer& p;
976  public:
978  FZPrintingInspector(const Printer& p0);
980  virtual void inspect(const Space& node);
982  virtual void finalize(void);
983  };
984 
985  template<class S>
986  FZPrintingInspector<S>::FZPrintingInspector(const Printer& p0)
987  : TextOutput("Gecode/FlatZinc"), p(p0) {}
988 
989  template<class S>
990  void
991  FZPrintingInspector<S>::inspect(const Space& node) {
992  init();
993  dynamic_cast<const S&>(node).print(getStream(), p);
994  getStream() << std::endl;
995  }
996 
997  template<class S>
998  void
999  FZPrintingInspector<S>::finalize(void) {
1001  }
1002 
1003  template<class S>
1004  class FZPrintingComparator
1005  : public Gecode::Gist::VarComparator<S> {
1006  private:
1007  const Printer& p;
1008  public:
1010  FZPrintingComparator(const Printer& p0);
1011 
1013  virtual void compare(const Space& s0, const Space& s1);
1014  };
1015 
1016  template<class S>
1017  FZPrintingComparator<S>::FZPrintingComparator(const Printer& p0)
1018  : Gecode::Gist::VarComparator<S>("Gecode/FlatZinc"), p(p0) {}
1019 
1020  template<class S>
1021  void
1022  FZPrintingComparator<S>::compare(const Space& s0, const Space& s1) {
1023  this->init();
1024  try {
1025  dynamic_cast<const S&>(s0).compare(dynamic_cast<const S&>(s1),
1026  this->getStream(), p);
1027  } catch (Exception& e) {
1028  this->getStream() << "Exception: " << e.what();
1029  }
1030  this->getStream() << std::endl;
1031  }
1032 
1033 #endif
1034 
1035 
1036  template<template<class> class Engine>
1037  void
1038  FlatZincSpace::runEngine(std::ostream& out, const Printer& p,
1039  const FlatZincOptions& opt, Support::Timer& t_total) {
1040  if (opt.restart()==RM_NONE) {
1041  runMeta<Engine,Driver::EngineToMeta>(out,p,opt,t_total);
1042  } else {
1043  runMeta<Engine,RBS>(out,p,opt,t_total);
1044  }
1045  }
1046 
1047  template<template<class> class Engine,
1048  template<template<class> class,class> class Meta>
1049  void
1050  FlatZincSpace::runMeta(std::ostream& out, const Printer& p,
1051  const FlatZincOptions& opt, Support::Timer& t_total) {
1052 #ifdef GECODE_HAS_GIST
1053  if (opt.mode() == SM_GIST) {
1054  FZPrintingInspector<FlatZincSpace> pi(p);
1055  FZPrintingComparator<FlatZincSpace> pc(p);
1056  (void) GistEngine<Engine<FlatZincSpace> >::explore(this,opt,&pi,&pc);
1057  return;
1058  }
1059 #endif
1060  StatusStatistics sstat;
1061  unsigned int n_p = 0;
1062  Support::Timer t_solve;
1063  t_solve.start();
1064  if (status(sstat) != SS_FAILED) {
1065  n_p = propagators();
1066  }
1067  Search::Options o;
1068  o.stop = Driver::CombinedStop::create(opt.node(), opt.fail(), opt.time(),
1069  true);
1070  o.c_d = opt.c_d();
1071  o.a_d = opt.a_d();
1072  o.threads = opt.threads();
1073  o.cutoff = Driver::createCutoff(opt);
1074  if (opt.interrupt())
1076  Meta<Engine,FlatZincSpace> se(this,o);
1077  int noOfSolutions = _method == SAT ? opt.solutions() : 0;
1078  bool printAll = _method == SAT || opt.allSolutions();
1079  int findSol = noOfSolutions;
1080  FlatZincSpace* sol = NULL;
1081  while (FlatZincSpace* next_sol = se.next()) {
1082  delete sol;
1083  sol = next_sol;
1084  if (printAll) {
1085  sol->print(out, p);
1086  out << "----------" << std::endl;
1087  }
1088  if (--findSol==0)
1089  goto stopped;
1090  }
1091  if (sol && !printAll) {
1092  sol->print(out, p);
1093  out << "----------" << std::endl;
1094  }
1095  if (!se.stopped()) {
1096  if (sol) {
1097  out << "==========" << endl;
1098  } else {
1099  out << "=====UNSATISFIABLE=====" << endl;
1100  }
1101  } else if (!sol) {
1102  out << "=====UNKNOWN=====" << endl;
1103  }
1104  delete sol;
1105  stopped:
1106  if (opt.interrupt())
1108  if (opt.mode() == SM_STAT) {
1109  Gecode::Search::Statistics stat = se.statistics();
1110  out << endl
1111  << "%% runtime: ";
1112  Driver::stop(t_total,out);
1113  out << endl
1114  << "%% solvetime: ";
1115  Driver::stop(t_solve,out);
1116  out << endl
1117  << "%% solutions: "
1118  << std::abs(noOfSolutions - findSol) << endl
1119  << "%% variables: "
1120  << (intVarCount + boolVarCount + setVarCount) << endl
1121  << "%% propagators: " << n_p << endl
1122  << "%% propagations: " << sstat.propagate+stat.propagate << endl
1123  << "%% nodes: " << stat.node << endl
1124  << "%% failures: " << stat.fail << endl
1125  << "%% restarts: " << stat.restart << endl
1126  << "%% peak depth: " << stat.depth << endl
1127  << "%% peak memory: "
1128  << static_cast<int>((stat.memory+1023) / 1024) << " KB"
1129  << endl;
1130  }
1131  }
1132 
1133 #ifdef GECODE_HAS_QT
1134  void
1135  FlatZincSpace::branchWithPlugin(AST::Node* ann) {
1136  if (AST::Call* c = dynamic_cast<AST::Call*>(ann)) {
1137  QString pluginName(c->id.c_str());
1138  if (QLibrary::isLibrary(pluginName+".dll")) {
1139  pluginName += ".dll";
1140  } else if (QLibrary::isLibrary(pluginName+".dylib")) {
1141  pluginName = "lib" + pluginName + ".dylib";
1142  } else if (QLibrary::isLibrary(pluginName+".so")) {
1143  // Must check .so after .dylib so that Mac OS uses .dylib
1144  pluginName = "lib" + pluginName + ".so";
1145  }
1146  QPluginLoader pl(pluginName);
1147  QObject* plugin_o = pl.instance();
1148  if (!plugin_o) {
1149  throw FlatZinc::Error("FlatZinc",
1150  "Error loading plugin "+pluginName.toStdString()+
1151  ": "+pl.errorString().toStdString());
1152  }
1153  BranchPlugin* pb = qobject_cast<BranchPlugin*>(plugin_o);
1154  if (!pb) {
1155  throw FlatZinc::Error("FlatZinc",
1156  "Error loading plugin "+pluginName.toStdString()+
1157  ": does not contain valid PluginBrancher");
1158  }
1159  pb->branch(*this, c);
1160  }
1161  }
1162 #else
1163  void
1164  FlatZincSpace::branchWithPlugin(AST::Node*) {
1165  throw FlatZinc::Error("FlatZinc",
1166  "Branching with plugins not supported (requires Qt support)");
1167  }
1168 #endif
1169 
1170  void
1171  FlatZincSpace::run(std::ostream& out, const Printer& p,
1172  const FlatZincOptions& opt, Support::Timer& t_total) {
1173  switch (_method) {
1174  case MIN:
1175  case MAX:
1176  runEngine<BAB>(out,p,opt,t_total);
1177  break;
1178  case SAT:
1179  runEngine<DFS>(out,p,opt,t_total);
1180  break;
1181  }
1182  }
1183 
1184  void
1186  if (_method == MIN)
1187  rel(*this, iv[_optVar], IRT_LE,
1188  static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
1189  else if (_method == MAX)
1190  rel(*this, iv[_optVar], IRT_GR,
1191  static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
1192  }
1193 
1194  Space*
1195  FlatZincSpace::copy(bool share) {
1196  return new FlatZincSpace(share, *this);
1197  }
1198 
1201  return _method;
1202  }
1203 
1204  int
1206  return _optVar;
1207  }
1208 
1209  void
1210  FlatZincSpace::print(std::ostream& out, const Printer& p) const {
1211  p.print(out, iv, bv
1212 #ifdef GECODE_HAS_SET_VARS
1213  , sv
1214 #endif
1215 #ifdef GECODE_HAS_FLOAT_VARS
1216  , fv
1217 #endif
1218  );
1219  }
1220 
1221  void
1222  FlatZincSpace::compare(const Space& s, std::ostream& out) const {
1223  (void) s; (void) out;
1224 #ifdef GECODE_HAS_GIST
1225  const FlatZincSpace& fs = dynamic_cast<const FlatZincSpace&>(s);
1226  for (int i = 0; i < iv.size(); ++i) {
1227  std::stringstream ss;
1228  ss << "iv[" << i << "]";
1229  std::string result(Gecode::Gist::Comparator::compare(ss.str(), iv[i],
1230  fs.iv[i]));
1231  if (result.length() > 0) out << result << std::endl;
1232  }
1233  for (int i = 0; i < bv.size(); ++i) {
1234  std::stringstream ss;
1235  ss << "bv[" << i << "]";
1236  std::string result(Gecode::Gist::Comparator::compare(ss.str(), bv[i],
1237  fs.bv[i]));
1238  if (result.length() > 0) out << result << std::endl;
1239  }
1240 #ifdef GECODE_HAS_SET_VARS
1241  for (int i = 0; i < sv.size(); ++i) {
1242  std::stringstream ss;
1243  ss << "sv[" << i << "]";
1244  std::string result(Gecode::Gist::Comparator::compare(ss.str(), sv[i],
1245  fs.sv[i]));
1246  if (result.length() > 0) out << result << std::endl;
1247  }
1248 #endif
1249 #ifdef GECODE_HAS_FLOAT_VARS
1250  for (int i = 0; i < fv.size(); ++i) {
1251  std::stringstream ss;
1252  ss << "fv[" << i << "]";
1253  std::string result(Gecode::Gist::Comparator::compare(ss.str(), fv[i],
1254  fs.fv[i]));
1255  if (result.length() > 0) out << result << std::endl;
1256  }
1257 #endif
1258 #endif
1259  }
1260 
1261  void
1262  FlatZincSpace::compare(const FlatZincSpace& s, std::ostream& out,
1263  const Printer& p) const {
1264  p.printDiff(out, iv, s.iv, bv, s.bv
1265 #ifdef GECODE_HAS_SET_VARS
1266  , sv, s.sv
1267 #endif
1268 #ifdef GECODE_HAS_FLOAT_VARS
1269  , fv, s.fv
1270 #endif
1271  );
1272  }
1273 
1274  void
1276  p.shrinkArrays(*this, _optVar, iv, bv
1277 #ifdef GECODE_HAS_SET_VARS
1278  , sv
1279 #endif
1280 #ifdef GECODE_HAS_FLOAT_VARS
1281  , fv
1282 #endif
1283  );
1284  }
1285 
1286  IntArgs
1288  AST::Array* a = arg->getArray();
1289  IntArgs ia(a->a.size()+offset);
1290  for (int i=offset; i--;)
1291  ia[i] = 0;
1292  for (int i=a->a.size(); i--;)
1293  ia[i+offset] = a->a[i]->getInt();
1294  return ia;
1295  }
1296  IntArgs
1298  AST::Array* a = arg->getArray();
1299  IntArgs ia(a->a.size()+offset);
1300  for (int i=offset; i--;)
1301  ia[i] = 0;
1302  for (int i=a->a.size(); i--;)
1303  ia[i+offset] = a->a[i]->getBool();
1304  return ia;
1305  }
1306  IntSet
1308  AST::SetLit* sl = n->getSet();
1309  IntSet d;
1310  if (sl->interval) {
1311  d = IntSet(sl->min, sl->max);
1312  } else {
1313  Region re(*this);
1314  int* is = re.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
1315  for (int i=sl->s.size(); i--; )
1316  is[i] = sl->s[i];
1317  d = IntSet(is, sl->s.size());
1318  }
1319  return d;
1320  }
1321  IntSetArgs
1323  AST::Array* a = arg->getArray();
1324  if (a->a.size() == 0) {
1325  IntSetArgs emptyIa(0);
1326  return emptyIa;
1327  }
1328  IntSetArgs ia(a->a.size()+offset);
1329  for (int i=offset; i--;)
1330  ia[i] = IntSet::empty;
1331  for (int i=a->a.size(); i--;) {
1332  ia[i+offset] = arg2intset(a->a[i]);
1333  }
1334  return ia;
1335  }
1336  IntVarArgs
1338  AST::Array* a = arg->getArray();
1339  if (a->a.size() == 0) {
1340  IntVarArgs emptyIa(0);
1341  return emptyIa;
1342  }
1343  IntVarArgs ia(a->a.size()+offset);
1344  for (int i=offset; i--;)
1345  ia[i] = IntVar(*this, 0, 0);
1346  for (int i=a->a.size(); i--;) {
1347  if (a->a[i]->isIntVar()) {
1348  ia[i+offset] = iv[a->a[i]->getIntVar()];
1349  } else {
1350  int value = a->a[i]->getInt();
1351  IntVar iv(*this, value, value);
1352  ia[i+offset] = iv;
1353  }
1354  }
1355  return ia;
1356  }
1357  BoolVarArgs
1358  FlatZincSpace::arg2boolvarargs(AST::Node* arg, int offset, int siv) {
1359  AST::Array* a = arg->getArray();
1360  if (a->a.size() == 0) {
1361  BoolVarArgs emptyIa(0);
1362  return emptyIa;
1363  }
1364  BoolVarArgs ia(a->a.size()+offset-(siv==-1?0:1));
1365  for (int i=offset; i--;)
1366  ia[i] = BoolVar(*this, 0, 0);
1367  for (int i=0; i<static_cast<int>(a->a.size()); i++) {
1368  if (i==siv)
1369  continue;
1370  if (a->a[i]->isBool()) {
1371  bool value = a->a[i]->getBool();
1372  BoolVar iv(*this, value, value);
1373  ia[offset++] = iv;
1374  } else if (a->a[i]->isIntVar() &&
1375  aliasBool2Int(a->a[i]->getIntVar()) != -1) {
1376  ia[offset++] = bv[aliasBool2Int(a->a[i]->getIntVar())];
1377  } else {
1378  ia[offset++] = bv[a->a[i]->getBoolVar()];
1379  }
1380  }
1381  return ia;
1382  }
1383  BoolVar
1385  BoolVar x0;
1386  if (n->isBool()) {
1387  x0 = BoolVar(*this, n->getBool(), n->getBool());
1388  }
1389  else {
1390  x0 = bv[n->getBoolVar()];
1391  }
1392  return x0;
1393  }
1394  IntVar
1396  IntVar x0;
1397  if (n->isIntVar()) {
1398  x0 = iv[n->getIntVar()];
1399  } else {
1400  x0 = IntVar(*this, n->getInt(), n->getInt());
1401  }
1402  return x0;
1403  }
1404  bool
1406  AST::Array* a = b->getArray();
1407  singleInt = -1;
1408  if (a->a.size() == 0)
1409  return true;
1410  for (int i=a->a.size(); i--;) {
1411  if (a->a[i]->isBoolVar() || a->a[i]->isBool()) {
1412  } else if (a->a[i]->isIntVar()) {
1413  if (aliasBool2Int(a->a[i]->getIntVar()) == -1) {
1414  if (singleInt != -1) {
1415  return false;
1416  }
1417  singleInt = i;
1418  }
1419  } else {
1420  return false;
1421  }
1422  }
1423  return singleInt==-1 || a->a.size() > 1;
1424  }
1425 #ifdef GECODE_HAS_SET_VARS
1426  SetVar
1428  SetVar x0;
1429  if (!n->isSetVar()) {
1430  IntSet d = arg2intset(n);
1431  x0 = SetVar(*this, d, d);
1432  } else {
1433  x0 = sv[n->getSetVar()];
1434  }
1435  return x0;
1436  }
1437  SetVarArgs
1438  FlatZincSpace::arg2setvarargs(AST::Node* arg, int offset, int doffset,
1439  const IntSet& od) {
1440  AST::Array* a = arg->getArray();
1441  SetVarArgs ia(a->a.size()+offset);
1442  for (int i=offset; i--;) {
1443  IntSet d = i<doffset ? od : IntSet::empty;
1444  ia[i] = SetVar(*this, d, d);
1445  }
1446  for (int i=a->a.size(); i--;) {
1447  ia[i+offset] = arg2SetVar(a->a[i]);
1448  }
1449  return ia;
1450  }
1451 #endif
1452 #ifdef GECODE_HAS_FLOAT_VARS
1453  FloatValArgs
1455  AST::Array* a = arg->getArray();
1456  FloatValArgs fa(a->a.size()+offset);
1457  for (int i=offset; i--;)
1458  fa[i] = 0.0;
1459  for (int i=a->a.size(); i--;)
1460  fa[i+offset] = a->a[i]->getFloat();
1461  return fa;
1462  }
1463  FloatVarArgs
1465  AST::Array* a = arg->getArray();
1466  if (a->a.size() == 0) {
1467  FloatVarArgs emptyFa(0);
1468  return emptyFa;
1469  }
1470  FloatVarArgs fa(a->a.size()+offset);
1471  for (int i=offset; i--;)
1472  fa[i] = FloatVar(*this, 0.0, 0.0);
1473  for (int i=a->a.size(); i--;) {
1474  if (a->a[i]->isFloatVar()) {
1475  fa[i+offset] = fv[a->a[i]->getFloatVar()];
1476  } else {
1477  double value = a->a[i]->getFloat();
1478  FloatVar fv(*this, value, value);
1479  fa[i+offset] = fv;
1480  }
1481  }
1482  return fa;
1483  }
1484  FloatVar
1486  FloatVar x0;
1487  if (n->isFloatVar()) {
1488  x0 = fv[n->getFloatVar()];
1489  } else {
1490  x0 = FloatVar(*this, n->getFloat(), n->getFloat());
1491  }
1492  return x0;
1493  }
1494 #endif
1495  IntConLevel
1497  if (ann) {
1498  if (ann->hasAtom("val"))
1499  return ICL_VAL;
1500  if (ann->hasAtom("domain"))
1501  return ICL_DOM;
1502  if (ann->hasAtom("bounds") ||
1503  ann->hasAtom("boundsR") ||
1504  ann->hasAtom("boundsD") ||
1505  ann->hasAtom("boundsZ"))
1506  return ICL_BND;
1507  }
1508  return ICL_DEF;
1509  }
1510 
1511 
1512  void
1514  _output = output;
1515  }
1516 
1517  void
1518  Printer::printElem(std::ostream& out,
1519  AST::Node* ai,
1520  const Gecode::IntVarArray& iv,
1521  const Gecode::BoolVarArray& bv
1522 #ifdef GECODE_HAS_SET_VARS
1523  , const Gecode::SetVarArray& sv
1524 #endif
1525 #ifdef GECODE_HAS_FLOAT_VARS
1526  ,
1527  const Gecode::FloatVarArray& fv
1528 #endif
1529  ) const {
1530  int k;
1531  if (ai->isInt(k)) {
1532  out << k;
1533  } else if (ai->isIntVar()) {
1534  out << iv[ai->getIntVar()];
1535  } else if (ai->isBoolVar()) {
1536  if (bv[ai->getBoolVar()].min() == 1) {
1537  out << "true";
1538  } else if (bv[ai->getBoolVar()].max() == 0) {
1539  out << "false";
1540  } else {
1541  out << "false..true";
1542  }
1543 #ifdef GECODE_HAS_SET_VARS
1544  } else if (ai->isSetVar()) {
1545  if (!sv[ai->getSetVar()].assigned()) {
1546  out << sv[ai->getSetVar()];
1547  return;
1548  }
1549  SetVarGlbRanges svr(sv[ai->getSetVar()]);
1550  if (!svr()) {
1551  out << "{}";
1552  return;
1553  }
1554  int min = svr.min();
1555  int max = svr.max();
1556  ++svr;
1557  if (svr()) {
1558  SetVarGlbValues svv(sv[ai->getSetVar()]);
1559  int i = svv.val();
1560  out << "{" << i;
1561  ++svv;
1562  for (; svv(); ++svv)
1563  out << ", " << svv.val();
1564  out << "}";
1565  } else {
1566  out << min << ".." << max;
1567  }
1568 #endif
1569 #ifdef GECODE_HAS_FLOAT_VARS
1570  } else if (ai->isFloatVar()) {
1571  out << fv[ai->getFloatVar()];
1572 #endif
1573  } else if (ai->isBool()) {
1574  out << (ai->getBool() ? "true" : "false");
1575  } else if (ai->isSet()) {
1576  AST::SetLit* s = ai->getSet();
1577  if (s->interval) {
1578  out << s->min << ".." << s->max;
1579  } else {
1580  out << "{";
1581  for (unsigned int i=0; i<s->s.size(); i++) {
1582  out << s->s[i] << (i < s->s.size()-1 ? ", " : "}");
1583  }
1584  }
1585  } else if (ai->isString()) {
1586  std::string s = ai->getString();
1587  for (unsigned int i=0; i<s.size(); i++) {
1588  if (s[i] == '\\' && i<s.size()-1) {
1589  switch (s[i+1]) {
1590  case 'n': out << "\n"; break;
1591  case '\\': out << "\\"; break;
1592  case 't': out << "\t"; break;
1593  default: out << "\\" << s[i+1];
1594  }
1595  i++;
1596  } else {
1597  out << s[i];
1598  }
1599  }
1600  }
1601  }
1602 
1603  void
1604  Printer::printElemDiff(std::ostream& out,
1605  AST::Node* ai,
1606  const Gecode::IntVarArray& iv1,
1607  const Gecode::IntVarArray& iv2,
1608  const Gecode::BoolVarArray& bv1,
1609  const Gecode::BoolVarArray& bv2
1610 #ifdef GECODE_HAS_SET_VARS
1611  , const Gecode::SetVarArray& sv1,
1612  const Gecode::SetVarArray& sv2
1613 #endif
1614 #ifdef GECODE_HAS_FLOAT_VARS
1615  , const Gecode::FloatVarArray& fv1,
1616  const Gecode::FloatVarArray& fv2
1617 #endif
1618  ) const {
1619 #ifdef GECODE_HAS_GIST
1620  using namespace Gecode::Gist;
1621  int k;
1622  if (ai->isInt(k)) {
1623  out << k;
1624  } else if (ai->isIntVar()) {
1625  std::string res(Comparator::compare("",iv1[ai->getIntVar()],
1626  iv2[ai->getIntVar()]));
1627  if (res.length() > 0) {
1628  res.erase(0, 1); // Remove '='
1629  out << res;
1630  } else {
1631  out << iv1[ai->getIntVar()];
1632  }
1633  } else if (ai->isBoolVar()) {
1634  std::string res(Comparator::compare("",bv1[ai->getBoolVar()],
1635  bv2[ai->getBoolVar()]));
1636  if (res.length() > 0) {
1637  res.erase(0, 1); // Remove '='
1638  out << res;
1639  } else {
1640  out << bv1[ai->getBoolVar()];
1641  }
1642 #ifdef GECODE_HAS_SET_VARS
1643  } else if (ai->isSetVar()) {
1644  std::string res(Comparator::compare("",sv1[ai->getSetVar()],
1645  sv2[ai->getSetVar()]));
1646  if (res.length() > 0) {
1647  res.erase(0, 1); // Remove '='
1648  out << res;
1649  } else {
1650  out << sv1[ai->getSetVar()];
1651  }
1652 #endif
1653 #ifdef GECODE_HAS_FLOAT_VARS
1654  } else if (ai->isFloatVar()) {
1655  std::string res(Comparator::compare("",fv1[ai->getFloatVar()],
1656  fv2[ai->getFloatVar()]));
1657  if (res.length() > 0) {
1658  res.erase(0, 1); // Remove '='
1659  out << res;
1660  } else {
1661  out << fv1[ai->getFloatVar()];
1662  }
1663 #endif
1664  } else if (ai->isBool()) {
1665  out << (ai->getBool() ? "true" : "false");
1666  } else if (ai->isSet()) {
1667  AST::SetLit* s = ai->getSet();
1668  if (s->interval) {
1669  out << s->min << ".." << s->max;
1670  } else {
1671  out << "{";
1672  for (unsigned int i=0; i<s->s.size(); i++) {
1673  out << s->s[i] << (i < s->s.size()-1 ? ", " : "}");
1674  }
1675  }
1676  } else if (ai->isString()) {
1677  std::string s = ai->getString();
1678  for (unsigned int i=0; i<s.size(); i++) {
1679  if (s[i] == '\\' && i<s.size()-1) {
1680  switch (s[i+1]) {
1681  case 'n': out << "\n"; break;
1682  case '\\': out << "\\"; break;
1683  case 't': out << "\t"; break;
1684  default: out << "\\" << s[i+1];
1685  }
1686  i++;
1687  } else {
1688  out << s[i];
1689  }
1690  }
1691  }
1692 #endif
1693  }
1694 
1695  void
1696  Printer::print(std::ostream& out,
1697  const Gecode::IntVarArray& iv,
1698  const Gecode::BoolVarArray& bv
1699 #ifdef GECODE_HAS_SET_VARS
1700  ,
1701  const Gecode::SetVarArray& sv
1702 #endif
1703 #ifdef GECODE_HAS_FLOAT_VARS
1704  ,
1705  const Gecode::FloatVarArray& fv
1706 #endif
1707  ) const {
1708  if (_output == NULL)
1709  return;
1710  for (unsigned int i=0; i< _output->a.size(); i++) {
1711  AST::Node* ai = _output->a[i];
1712  if (ai->isArray()) {
1713  AST::Array* aia = ai->getArray();
1714  int size = aia->a.size();
1715  out << "[";
1716  for (int j=0; j<size; j++) {
1717  printElem(out,aia->a[j],iv,bv
1718 #ifdef GECODE_HAS_SET_VARS
1719  ,sv
1720 #endif
1721 #ifdef GECODE_HAS_FLOAT_VARS
1722  ,fv
1723 #endif
1724  );
1725  if (j<size-1)
1726  out << ", ";
1727  }
1728  out << "]";
1729  } else {
1730  printElem(out,ai,iv,bv
1731 #ifdef GECODE_HAS_SET_VARS
1732  ,sv
1733 #endif
1734 #ifdef GECODE_HAS_FLOAT_VARS
1735  ,fv
1736 #endif
1737  );
1738  }
1739  }
1740  }
1741 
1742  void
1743  Printer::printDiff(std::ostream& out,
1744  const Gecode::IntVarArray& iv1,
1745  const Gecode::IntVarArray& iv2,
1746  const Gecode::BoolVarArray& bv1,
1747  const Gecode::BoolVarArray& bv2
1748 #ifdef GECODE_HAS_SET_VARS
1749  ,
1750  const Gecode::SetVarArray& sv1,
1751  const Gecode::SetVarArray& sv2
1752 #endif
1753 #ifdef GECODE_HAS_FLOAT_VARS
1754  ,
1755  const Gecode::FloatVarArray& fv1,
1756  const Gecode::FloatVarArray& fv2
1757 #endif
1758  ) const {
1759  if (_output == NULL)
1760  return;
1761  for (unsigned int i=0; i< _output->a.size(); i++) {
1762  AST::Node* ai = _output->a[i];
1763  if (ai->isArray()) {
1764  AST::Array* aia = ai->getArray();
1765  int size = aia->a.size();
1766  out << "[";
1767  for (int j=0; j<size; j++) {
1768  printElemDiff(out,aia->a[j],iv1,iv2,bv1,bv2
1769 #ifdef GECODE_HAS_SET_VARS
1770  ,sv1,sv2
1771 #endif
1772 #ifdef GECODE_HAS_FLOAT_VARS
1773  ,fv1,fv2
1774 #endif
1775  );
1776  if (j<size-1)
1777  out << ", ";
1778  }
1779  out << "]";
1780  } else {
1781  printElemDiff(out,ai,iv1,iv2,bv1,bv2
1782 #ifdef GECODE_HAS_SET_VARS
1783  ,sv1,sv2
1784 #endif
1785 #ifdef GECODE_HAS_FLOAT_VARS
1786  ,fv1,fv2
1787 #endif
1788  );
1789  }
1790  }
1791  }
1792 
1793  void
1795  std::map<int,int>& iv, std::map<int,int>& bv,
1796  std::map<int,int>& sv, std::map<int,int>& fv) {
1797  if (node->isIntVar()) {
1798  AST::IntVar* x = static_cast<AST::IntVar*>(node);
1799  if (iv.find(x->i) == iv.end()) {
1800  int newi = iv.size();
1801  iv[x->i] = newi;
1802  }
1803  x->i = iv[x->i];
1804  } else if (node->isBoolVar()) {
1805  AST::BoolVar* x = static_cast<AST::BoolVar*>(node);
1806  if (bv.find(x->i) == bv.end()) {
1807  int newi = bv.size();
1808  bv[x->i] = newi;
1809  }
1810  x->i = bv[x->i];
1811  } else if (node->isSetVar()) {
1812  AST::SetVar* x = static_cast<AST::SetVar*>(node);
1813  if (sv.find(x->i) == sv.end()) {
1814  int newi = sv.size();
1815  sv[x->i] = newi;
1816  }
1817  x->i = sv[x->i];
1818  } else if (node->isFloatVar()) {
1819  AST::FloatVar* x = static_cast<AST::FloatVar*>(node);
1820  if (fv.find(x->i) == fv.end()) {
1821  int newi = fv.size();
1822  fv[x->i] = newi;
1823  }
1824  x->i = fv[x->i];
1825  }
1826  }
1827 
1828  void
1830  int& optVar,
1831  Gecode::IntVarArray& iv,
1833 #ifdef GECODE_HAS_SET_VARS
1834  ,
1836 #endif
1837 #ifdef GECODE_HAS_FLOAT_VARS
1838  ,
1840 #endif
1841  ) {
1842  if (_output == NULL) {
1843  if (optVar == -1) {
1844  iv = IntVarArray(home, 0);
1845  } else {
1846  IntVar ov = iv[optVar];
1847  iv = IntVarArray(home, 1);
1848  iv[0] = ov;
1849  optVar = 0;
1850  }
1851  bv = BoolVarArray(home, 0);
1852 #ifdef GECODE_HAS_SET_VARS
1853  sv = SetVarArray(home, 0);
1854 #endif
1855 #ifdef GECODE_HAS_FLOAT_VARS
1856  fv = FloatVarArray(home,0);
1857 #endif
1858  return;
1859  }
1860  std::map<int,int> iv_new;
1861  std::map<int,int> bv_new;
1862  std::map<int,int> sv_new;
1863  std::map<int,int> fv_new;
1864 
1865  if (optVar != -1) {
1866  iv_new[optVar] = 0;
1867  optVar = 0;
1868  }
1869 
1870  for (unsigned int i=0; i< _output->a.size(); i++) {
1871  AST::Node* ai = _output->a[i];
1872  if (ai->isArray()) {
1873  AST::Array* aia = ai->getArray();
1874  for (unsigned int j=0; j<aia->a.size(); j++) {
1875  shrinkElement(aia->a[j],iv_new,bv_new,sv_new,fv_new);
1876  }
1877  } else {
1878  shrinkElement(ai,iv_new,bv_new,sv_new,fv_new);
1879  }
1880  }
1881 
1882  IntVarArgs iva(iv_new.size());
1883  for (map<int,int>::iterator i=iv_new.begin(); i != iv_new.end(); ++i) {
1884  iva[(*i).second] = iv[(*i).first];
1885  }
1886  iv = IntVarArray(home, iva);
1887 
1888  BoolVarArgs bva(bv_new.size());
1889  for (map<int,int>::iterator i=bv_new.begin(); i != bv_new.end(); ++i) {
1890  bva[(*i).second] = bv[(*i).first];
1891  }
1892  bv = BoolVarArray(home, bva);
1893 
1894 #ifdef GECODE_HAS_SET_VARS
1895  SetVarArgs sva(sv_new.size());
1896  for (map<int,int>::iterator i=sv_new.begin(); i != sv_new.end(); ++i) {
1897  sva[(*i).second] = sv[(*i).first];
1898  }
1899  sv = SetVarArray(home, sva);
1900 #endif
1901 
1902 #ifdef GECODE_HAS_FLOAT_VARS
1903  FloatVarArgs fva(fv_new.size());
1904  for (map<int,int>::iterator i=fv_new.begin(); i != fv_new.end(); ++i) {
1905  fva[(*i).second] = fv[(*i).first];
1906  }
1907  fv = FloatVarArray(home, fva);
1908 #endif
1909  }
1910 
1912  delete _output;
1913  }
1914 
1915 }}
1916 
1917 // STATISTICS: flatzinc-any