Generated on Tue Mar 5 2013 22:37:13 for Gecode by doxygen 1.8.3.1
registry.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  * Mikael Lagerkvist <lagerkvist@gmail.com>
8  *
9  * Copyright:
10  * Guido Tack, 2007
11  * Mikael Lagerkvist, 2009
12  *
13  * Last modified:
14  * $Date: 2012-03-21 16:25:08 +1100 (Wed, 21 Mar 2012) $ by $Author: tack $
15  * $Revision: 12605 $
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 
43 #include <gecode/kernel.hh>
44 #include <gecode/int.hh>
45 #include <gecode/minimodel.hh>
46 #ifdef GECODE_HAS_SET_VARS
47 #include <gecode/set.hh>
48 #endif
49 #include <gecode/flatzinc.hh>
50 
51 namespace Gecode { namespace FlatZinc {
52 
53  Registry& registry(void) {
54  static Registry r;
55  return r;
56  }
57 
58  void
60  std::map<std::string,poster>::iterator i = r.find(ce.id);
61  if (i == r.end()) {
62  throw FlatZinc::Error("Registry",
63  std::string("Constraint ")+ce.id+" not found");
64  }
65  i->second(s, ce, ann);
66  }
67 
68  void
69  Registry::add(const std::string& id, poster p) {
70  r[id] = p;
71  }
72 
73  namespace {
74 
75  IntConLevel ann2icl(AST::Node* ann) {
76  if (ann) {
77  if (ann->hasAtom("val"))
78  return ICL_VAL;
79  if (ann->hasAtom("domain"))
80  return ICL_DOM;
81  if (ann->hasAtom("bounds") ||
82  ann->hasAtom("boundsR") ||
83  ann->hasAtom("boundsD") ||
84  ann->hasAtom("boundsZ"))
85  return ICL_BND;
86  }
87  return ICL_DEF;
88  }
89 
90  inline IntRelType
91  swap(IntRelType irt) {
92  switch (irt) {
93  case IRT_LQ: return IRT_GQ;
94  case IRT_LE: return IRT_GR;
95  case IRT_GQ: return IRT_LQ;
96  case IRT_GR: return IRT_LE;
97  default: return irt;
98  }
99  }
100 
101  inline IntRelType
102  neg(IntRelType irt) {
103  switch (irt) {
104  case IRT_EQ: return IRT_NQ;
105  case IRT_NQ: return IRT_EQ;
106  case IRT_LQ: return IRT_GR;
107  case IRT_LE: return IRT_GQ;
108  case IRT_GQ: return IRT_LE;
109  case IRT_GR:
110  default:
111  assert(irt == IRT_GR);
112  }
113  return IRT_LQ;
114  }
115 
116  inline IntArgs arg2intargs(AST::Node* arg, int offset = 0) {
117  AST::Array* a = arg->getArray();
118  IntArgs ia(a->a.size()+offset);
119  for (int i=offset; i--;)
120  ia[i] = 0;
121  for (int i=a->a.size(); i--;)
122  ia[i+offset] = a->a[i]->getInt();
123  return ia;
124  }
125 
126  inline IntArgs arg2boolargs(AST::Node* arg, int offset = 0) {
127  AST::Array* a = arg->getArray();
128  IntArgs ia(a->a.size()+offset);
129  for (int i=offset; i--;)
130  ia[i] = 0;
131  for (int i=a->a.size(); i--;)
132  ia[i+offset] = a->a[i]->getBool();
133  return ia;
134  }
135 
136  inline IntSet arg2intset(FlatZincSpace& s, AST::Node* n) {
137  AST::SetLit* sl = n->getSet();
138  IntSet d;
139  if (sl->interval) {
140  d = IntSet(sl->min, sl->max);
141  } else {
142  Region re(s);
143  int* is = re.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
144  for (int i=sl->s.size(); i--; )
145  is[i] = sl->s[i];
146  d = IntSet(is, sl->s.size());
147  }
148  return d;
149  }
150 
151  inline IntSetArgs arg2intsetargs(FlatZincSpace& s,
152  AST::Node* arg, int offset = 0) {
153  AST::Array* a = arg->getArray();
154  if (a->a.size() == 0) {
155  IntSetArgs emptyIa(0);
156  return emptyIa;
157  }
158  IntSetArgs ia(a->a.size()+offset);
159  for (int i=offset; i--;)
160  ia[i] = IntSet::empty;
161  for (int i=a->a.size(); i--;) {
162  ia[i+offset] = arg2intset(s, a->a[i]);
163  }
164  return ia;
165  }
166 
167  inline IntVarArgs arg2intvarargs(FlatZincSpace& s, AST::Node* arg,
168  int offset = 0) {
169  AST::Array* a = arg->getArray();
170  if (a->a.size() == 0) {
171  IntVarArgs emptyIa(0);
172  return emptyIa;
173  }
174  IntVarArgs ia(a->a.size()+offset);
175  for (int i=offset; i--;)
176  ia[i] = IntVar(s, 0, 0);
177  for (int i=a->a.size(); i--;) {
178  if (a->a[i]->isIntVar()) {
179  ia[i+offset] = s.iv[a->a[i]->getIntVar()];
180  } else {
181  int value = a->a[i]->getInt();
182  IntVar iv(s, value, value);
183  ia[i+offset] = iv;
184  }
185  }
186  return ia;
187  }
188 
189  inline BoolVarArgs arg2boolvarargs(FlatZincSpace& s, AST::Node* arg,
190  int offset = 0, int siv=-1) {
191  AST::Array* a = arg->getArray();
192  if (a->a.size() == 0) {
193  BoolVarArgs emptyIa(0);
194  return emptyIa;
195  }
196  BoolVarArgs ia(a->a.size()+offset-(siv==-1?0:1));
197  for (int i=offset; i--;)
198  ia[i] = BoolVar(s, 0, 0);
199  for (int i=0; i<static_cast<int>(a->a.size()); i++) {
200  if (i==siv)
201  continue;
202  if (a->a[i]->isBool()) {
203  bool value = a->a[i]->getBool();
204  BoolVar iv(s, value, value);
205  ia[offset++] = iv;
206  } else if (a->a[i]->isIntVar() &&
207  s.aliasBool2Int(a->a[i]->getIntVar()) != -1) {
208  ia[offset++] = s.bv[s.aliasBool2Int(a->a[i]->getIntVar())];
209  } else {
210  ia[offset++] = s.bv[a->a[i]->getBoolVar()];
211  }
212  }
213  return ia;
214  }
215 
216 #ifdef GECODE_HAS_SET_VARS
217  SetVar getSetVar(FlatZincSpace& s, AST::Node* n) {
218  SetVar x0;
219  if (!n->isSetVar()) {
220  IntSet d = arg2intset(s,n);
221  x0 = SetVar(s, d, d);
222  } else {
223  x0 = s.sv[n->getSetVar()];
224  }
225  return x0;
226  }
227 
228  inline SetVarArgs arg2setvarargs(FlatZincSpace& s, AST::Node* arg,
229  int offset = 0, int doffset = 0,
230  const IntSet& od=IntSet::empty) {
231  AST::Array* a = arg->getArray();
232  SetVarArgs ia(a->a.size()+offset);
233  for (int i=offset; i--;) {
234  IntSet d = i<doffset ? od : IntSet::empty;
235  ia[i] = SetVar(s, d, d);
236  }
237  for (int i=a->a.size(); i--;) {
238  ia[i+offset] = getSetVar(s, a->a[i]);
239  }
240  return ia;
241  }
242 #endif
243 
244  BoolVar getBoolVar(FlatZincSpace& s, AST::Node* n) {
245  BoolVar x0;
246  if (n->isBool()) {
247  x0 = BoolVar(s, n->getBool(), n->getBool());
248  }
249  else {
250  x0 = s.bv[n->getBoolVar()];
251  }
252  return x0;
253  }
254 
255  IntVar getIntVar(FlatZincSpace& s, AST::Node* n) {
256  IntVar x0;
257  if (n->isIntVar()) {
258  x0 = s.iv[n->getIntVar()];
259  } else {
260  x0 = IntVar(s, n->getInt(), n->getInt());
261  }
262  return x0;
263  }
264 
265  bool isBoolArray(FlatZincSpace& s, AST::Node* b, int& singleInt) {
266  AST::Array* a = b->getArray();
267  singleInt = -1;
268  if (a->a.size() == 0)
269  return true;
270  for (int i=a->a.size(); i--;) {
271  if (a->a[i]->isBoolVar() || a->a[i]->isBool()) {
272  } else if (a->a[i]->isIntVar()) {
273  if (s.aliasBool2Int(a->a[i]->getIntVar()) == -1) {
274  if (singleInt != -1) {
275  return false;
276  }
277  singleInt = i;
278  }
279  } else {
280  return false;
281  }
282  }
283  return singleInt==-1 || a->a.size() > 1;
284  }
285 
286  void p_distinct(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
287  IntVarArgs va = arg2intvarargs(s, ce[0]);
288  IntConLevel icl = ann2icl(ann);
289  distinct(s, va, icl == ICL_DEF ? ICL_BND : icl);
290  }
291  void p_distinctOffset(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
292  IntVarArgs va = arg2intvarargs(s, ce[1]);
293  AST::Array* offs = ce.args->a[0]->getArray();
294  IntArgs oa(offs->a.size());
295  for (int i=offs->a.size(); i--; ) {
296  oa[i] = offs->a[i]->getInt();
297  }
298  IntConLevel icl = ann2icl(ann);
299  distinct(s, oa, va, icl == ICL_DEF ? ICL_BND : icl);
300  }
301 
302  void p_all_equal(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
303  IntVarArgs va = arg2intvarargs(s, ce[0]);
304  rel(s, va, IRT_EQ, ann2icl(ann));
305  }
306 
307  void p_int_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
308  AST::Node* ann) {
309  if (ce[0]->isIntVar()) {
310  if (ce[1]->isIntVar()) {
311  rel(s, getIntVar(s, ce[0]), irt, getIntVar(s, ce[1]),
312  ann2icl(ann));
313  } else {
314  rel(s, getIntVar(s, ce[0]), irt, ce[1]->getInt(), ann2icl(ann));
315  }
316  } else {
317  rel(s, getIntVar(s, ce[1]), swap(irt), ce[0]->getInt(),
318  ann2icl(ann));
319  }
320  }
321  void p_int_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
322  p_int_CMP(s, IRT_EQ, ce, ann);
323  }
324  void p_int_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
325  p_int_CMP(s, IRT_NQ, ce, ann);
326  }
327  void p_int_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
328  p_int_CMP(s, IRT_GQ, ce, ann);
329  }
330  void p_int_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
331  p_int_CMP(s, IRT_GR, ce, ann);
332  }
333  void p_int_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
334  p_int_CMP(s, IRT_LQ, ce, ann);
335  }
336  void p_int_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
337  p_int_CMP(s, IRT_LE, ce, ann);
338  }
339  void p_int_CMP_reif(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
340  AST::Node* ann) {
341  if (ce[2]->isBool()) {
342  if (ce[2]->getBool()) {
343  p_int_CMP(s, irt, ce, ann);
344  } else {
345  p_int_CMP(s, neg(irt), ce, ann);
346  }
347  return;
348  }
349  if (ce[0]->isIntVar()) {
350  if (ce[1]->isIntVar()) {
351  rel(s, getIntVar(s, ce[0]), irt, getIntVar(s, ce[1]),
352  getBoolVar(s, ce[2]), ann2icl(ann));
353  } else {
354  rel(s, getIntVar(s, ce[0]), irt, ce[1]->getInt(),
355  getBoolVar(s, ce[2]), ann2icl(ann));
356  }
357  } else {
358  rel(s, getIntVar(s, ce[1]), swap(irt), ce[0]->getInt(),
359  getBoolVar(s, ce[2]), ann2icl(ann));
360  }
361  }
362 
363  /* Comparisons */
364  void p_int_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
365  p_int_CMP_reif(s, IRT_EQ, ce, ann);
366  }
367  void p_int_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
368  p_int_CMP_reif(s, IRT_NQ, ce, ann);
369  }
370  void p_int_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
371  p_int_CMP_reif(s, IRT_GQ, ce, ann);
372  }
373  void p_int_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
374  p_int_CMP_reif(s, IRT_GR, ce, ann);
375  }
376  void p_int_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
377  p_int_CMP_reif(s, IRT_LQ, ce, ann);
378  }
379  void p_int_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
380  p_int_CMP_reif(s, IRT_LE, ce, ann);
381  }
382 
383  /* linear (in-)equations */
384  void p_int_lin_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
385  AST::Node* ann) {
386  IntArgs ia = arg2intargs(ce[0]);
387  int singleIntVar;
388  if (isBoolArray(s,ce[1],singleIntVar)) {
389  if (singleIntVar != -1) {
390  if (std::abs(ia[singleIntVar]) == 1 && ce[2]->getInt() == 0) {
391  IntVar siv = getIntVar(s, ce[1]->getArray()->a[singleIntVar]);
392  BoolVarArgs iv = arg2boolvarargs(s, ce[1], 0, singleIntVar);
393  IntArgs ia_tmp(ia.size()-1);
394  int count = 0;
395  for (int i=0; i<ia.size(); i++) {
396  if (i != singleIntVar)
397  ia_tmp[count++] = ia[singleIntVar] == -1 ? ia[i] : -ia[i];
398  }
399  IntRelType t = (ia[singleIntVar] == -1 ? irt : swap(irt));
400  linear(s, ia_tmp, iv, t, siv, ann2icl(ann));
401  } else {
402  IntVarArgs iv = arg2intvarargs(s, ce[1]);
403  linear(s, ia, iv, irt, ce[2]->getInt(), ann2icl(ann));
404  }
405  } else {
406  BoolVarArgs iv = arg2boolvarargs(s, ce[1]);
407  linear(s, ia, iv, irt, ce[2]->getInt(), ann2icl(ann));
408  }
409  } else {
410  IntVarArgs iv = arg2intvarargs(s, ce[1]);
411  linear(s, ia, iv, irt, ce[2]->getInt(), ann2icl(ann));
412  }
413  }
414  void p_int_lin_CMP_reif(FlatZincSpace& s, IntRelType irt,
415  const ConExpr& ce, AST::Node* ann) {
416  if (ce[2]->isBool()) {
417  if (ce[2]->getBool()) {
418  p_int_lin_CMP(s, irt, ce, ann);
419  } else {
420  p_int_lin_CMP(s, neg(irt), ce, ann);
421  }
422  return;
423  }
424  IntArgs ia = arg2intargs(ce[0]);
425  int singleIntVar;
426  if (isBoolArray(s,ce[1],singleIntVar)) {
427  if (singleIntVar != -1) {
428  if (std::abs(ia[singleIntVar]) == 1 && ce[2]->getInt() == 0) {
429  IntVar siv = getIntVar(s, ce[1]->getArray()->a[singleIntVar]);
430  BoolVarArgs iv = arg2boolvarargs(s, ce[1], 0, singleIntVar);
431  IntArgs ia_tmp(ia.size()-1);
432  int count = 0;
433  for (int i=0; i<ia.size(); i++) {
434  if (i != singleIntVar)
435  ia_tmp[count++] = ia[singleIntVar] == -1 ? ia[i] : -ia[i];
436  }
437  IntRelType t = (ia[singleIntVar] == -1 ? irt : swap(irt));
438  linear(s, ia_tmp, iv, t, siv, getBoolVar(s, ce[3]),
439  ann2icl(ann));
440  } else {
441  IntVarArgs iv = arg2intvarargs(s, ce[1]);
442  linear(s, ia, iv, irt, ce[2]->getInt(),
443  getBoolVar(s, ce[3]), ann2icl(ann));
444  }
445  } else {
446  BoolVarArgs iv = arg2boolvarargs(s, ce[1]);
447  linear(s, ia, iv, irt, ce[2]->getInt(),
448  getBoolVar(s, ce[3]), ann2icl(ann));
449  }
450  } else {
451  IntVarArgs iv = arg2intvarargs(s, ce[1]);
452  linear(s, ia, iv, irt, ce[2]->getInt(), getBoolVar(s, ce[3]),
453  ann2icl(ann));
454  }
455  }
456  void p_int_lin_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
457  p_int_lin_CMP(s, IRT_EQ, ce, ann);
458  }
459  void p_int_lin_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
460  p_int_lin_CMP_reif(s, IRT_EQ, ce, ann);
461  }
462  void p_int_lin_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
463  p_int_lin_CMP(s, IRT_NQ, ce, ann);
464  }
465  void p_int_lin_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
466  p_int_lin_CMP_reif(s, IRT_NQ, ce, ann);
467  }
468  void p_int_lin_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
469  p_int_lin_CMP(s, IRT_LQ, ce, ann);
470  }
471  void p_int_lin_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
472  p_int_lin_CMP_reif(s, IRT_LQ, ce, ann);
473  }
474  void p_int_lin_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
475  p_int_lin_CMP(s, IRT_LE, ce, ann);
476  }
477  void p_int_lin_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
478  p_int_lin_CMP_reif(s, IRT_LE, ce, ann);
479  }
480  void p_int_lin_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
481  p_int_lin_CMP(s, IRT_GQ, ce, ann);
482  }
483  void p_int_lin_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
484  p_int_lin_CMP_reif(s, IRT_GQ, ce, ann);
485  }
486  void p_int_lin_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
487  p_int_lin_CMP(s, IRT_GR, ce, ann);
488  }
489  void p_int_lin_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
490  p_int_lin_CMP_reif(s, IRT_GR, ce, ann);
491  }
492 
493  void p_bool_lin_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
494  AST::Node* ann) {
495  IntArgs ia = arg2intargs(ce[0]);
496  BoolVarArgs iv = arg2boolvarargs(s, ce[1]);
497  if (ce[2]->isIntVar())
498  linear(s, ia, iv, irt, s.iv[ce[2]->getIntVar()], ann2icl(ann));
499  else
500  linear(s, ia, iv, irt, ce[2]->getInt(), ann2icl(ann));
501  }
502  void p_bool_lin_CMP_reif(FlatZincSpace& s, IntRelType irt,
503  const ConExpr& ce, AST::Node* ann) {
504  if (ce[2]->isBool()) {
505  if (ce[2]->getBool()) {
506  p_bool_lin_CMP(s, irt, ce, ann);
507  } else {
508  p_bool_lin_CMP(s, neg(irt), ce, ann);
509  }
510  return;
511  }
512  IntArgs ia = arg2intargs(ce[0]);
513  BoolVarArgs iv = arg2boolvarargs(s, ce[1]);
514  if (ce[2]->isIntVar())
515  linear(s, ia, iv, irt, s.iv[ce[2]->getIntVar()], getBoolVar(s, ce[3]),
516  ann2icl(ann));
517  else
518  linear(s, ia, iv, irt, ce[2]->getInt(), getBoolVar(s, ce[3]),
519  ann2icl(ann));
520  }
521  void p_bool_lin_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
522  p_bool_lin_CMP(s, IRT_EQ, ce, ann);
523  }
524  void p_bool_lin_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
525  {
526  p_bool_lin_CMP_reif(s, IRT_EQ, ce, ann);
527  }
528  void p_bool_lin_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
529  p_bool_lin_CMP(s, IRT_NQ, ce, ann);
530  }
531  void p_bool_lin_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
532  {
533  p_bool_lin_CMP_reif(s, IRT_NQ, ce, ann);
534  }
535  void p_bool_lin_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
536  p_bool_lin_CMP(s, IRT_LQ, ce, ann);
537  }
538  void p_bool_lin_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
539  {
540  p_bool_lin_CMP_reif(s, IRT_LQ, ce, ann);
541  }
542  void p_bool_lin_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
543  {
544  p_bool_lin_CMP(s, IRT_LE, ce, ann);
545  }
546  void p_bool_lin_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
547  {
548  p_bool_lin_CMP_reif(s, IRT_LE, ce, ann);
549  }
550  void p_bool_lin_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
551  p_bool_lin_CMP(s, IRT_GQ, ce, ann);
552  }
553  void p_bool_lin_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
554  {
555  p_bool_lin_CMP_reif(s, IRT_GQ, ce, ann);
556  }
557  void p_bool_lin_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
558  p_bool_lin_CMP(s, IRT_GR, ce, ann);
559  }
560  void p_bool_lin_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
561  {
562  p_bool_lin_CMP_reif(s, IRT_GR, ce, ann);
563  }
564 
565  /* arithmetic constraints */
566 
567  void p_int_plus(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
568  if (!ce[0]->isIntVar()) {
569  rel(s, ce[0]->getInt() + getIntVar(s, ce[1])
570  == getIntVar(s,ce[2]), ann2icl(ann));
571  } else if (!ce[1]->isIntVar()) {
572  rel(s, getIntVar(s,ce[0]) + ce[1]->getInt()
573  == getIntVar(s,ce[2]), ann2icl(ann));
574  } else if (!ce[2]->isIntVar()) {
575  rel(s, getIntVar(s,ce[0]) + getIntVar(s,ce[1])
576  == ce[2]->getInt(), ann2icl(ann));
577  } else {
578  rel(s, getIntVar(s,ce[0]) + getIntVar(s,ce[1])
579  == getIntVar(s,ce[2]), ann2icl(ann));
580  }
581  }
582 
583  void p_int_minus(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
584  if (!ce[0]->isIntVar()) {
585  rel(s, ce[0]->getInt() - getIntVar(s, ce[1])
586  == getIntVar(s,ce[2]), ann2icl(ann));
587  } else if (!ce[1]->isIntVar()) {
588  rel(s, getIntVar(s,ce[0]) - ce[1]->getInt()
589  == getIntVar(s,ce[2]), ann2icl(ann));
590  } else if (!ce[2]->isIntVar()) {
591  rel(s, getIntVar(s,ce[0]) - getIntVar(s,ce[1])
592  == ce[2]->getInt(), ann2icl(ann));
593  } else {
594  rel(s, getIntVar(s,ce[0]) - getIntVar(s,ce[1])
595  == getIntVar(s,ce[2]), ann2icl(ann));
596  }
597  }
598 
599  void p_int_times(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
600  IntVar x0 = getIntVar(s, ce[0]);
601  IntVar x1 = getIntVar(s, ce[1]);
602  IntVar x2 = getIntVar(s, ce[2]);
603  mult(s, x0, x1, x2, ann2icl(ann));
604  }
605  void p_int_div(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
606  IntVar x0 = getIntVar(s, ce[0]);
607  IntVar x1 = getIntVar(s, ce[1]);
608  IntVar x2 = getIntVar(s, ce[2]);
609  div(s,x0,x1,x2, ann2icl(ann));
610  }
611  void p_int_mod(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
612  IntVar x0 = getIntVar(s, ce[0]);
613  IntVar x1 = getIntVar(s, ce[1]);
614  IntVar x2 = getIntVar(s, ce[2]);
615  mod(s,x0,x1,x2, ann2icl(ann));
616  }
617 
618  void p_int_min(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
619  IntVar x0 = getIntVar(s, ce[0]);
620  IntVar x1 = getIntVar(s, ce[1]);
621  IntVar x2 = getIntVar(s, ce[2]);
622  min(s, x0, x1, x2, ann2icl(ann));
623  }
624  void p_int_max(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
625  IntVar x0 = getIntVar(s, ce[0]);
626  IntVar x1 = getIntVar(s, ce[1]);
627  IntVar x2 = getIntVar(s, ce[2]);
628  max(s, x0, x1, x2, ann2icl(ann));
629  }
630  void p_int_negate(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
631  IntVar x0 = getIntVar(s, ce[0]);
632  IntVar x1 = getIntVar(s, ce[1]);
633  rel(s, x0 == -x1, ann2icl(ann));
634  }
635 
636  /* Boolean constraints */
637  void p_bool_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
638  AST::Node* ann) {
639  rel(s, getBoolVar(s, ce[0]), irt, getBoolVar(s, ce[1]),
640  ann2icl(ann));
641  }
642  void p_bool_CMP_reif(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
643  AST::Node* ann) {
644  rel(s, getBoolVar(s, ce[0]), irt, getBoolVar(s, ce[1]),
645  getBoolVar(s, ce[2]), ann2icl(ann));
646  }
647  void p_bool_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
648  p_bool_CMP(s, IRT_EQ, ce, ann);
649  }
650  void p_bool_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
651  p_bool_CMP_reif(s, IRT_EQ, ce, ann);
652  }
653  void p_bool_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
654  p_bool_CMP(s, IRT_NQ, ce, ann);
655  }
656  void p_bool_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
657  p_bool_CMP_reif(s, IRT_NQ, ce, ann);
658  }
659  void p_bool_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
660  p_bool_CMP(s, IRT_GQ, ce, ann);
661  }
662  void p_bool_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
663  p_bool_CMP_reif(s, IRT_GQ, ce, ann);
664  }
665  void p_bool_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
666  p_bool_CMP(s, IRT_LQ, ce, ann);
667  }
668  void p_bool_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
669  p_bool_CMP_reif(s, IRT_LQ, ce, ann);
670  }
671  void p_bool_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
672  p_bool_CMP(s, IRT_GR, ce, ann);
673  }
674  void p_bool_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
675  p_bool_CMP_reif(s, IRT_GR, ce, ann);
676  }
677  void p_bool_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
678  p_bool_CMP(s, IRT_LE, ce, ann);
679  }
680  void p_bool_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
681  p_bool_CMP_reif(s, IRT_LE, ce, ann);
682  }
683 
684 #define BOOL_OP(op) \
685  BoolVar b0 = getBoolVar(s, ce[0]); \
686  BoolVar b1 = getBoolVar(s, ce[1]); \
687  if (ce[2]->isBool()) { \
688  rel(s, b0, op, b1, ce[2]->getBool(), ann2icl(ann)); \
689  } else { \
690  rel(s, b0, op, b1, s.bv[ce[2]->getBoolVar()], ann2icl(ann)); \
691  }
692 
693 #define BOOL_ARRAY_OP(op) \
694  BoolVarArgs bv = arg2boolvarargs(s, ce[0]); \
695  if (ce.size()==1) { \
696  rel(s, op, bv, 1, ann2icl(ann)); \
697  } else if (ce[1]->isBool()) { \
698  rel(s, op, bv, ce[1]->getBool(), ann2icl(ann)); \
699  } else { \
700  rel(s, op, bv, s.bv[ce[1]->getBoolVar()], ann2icl(ann)); \
701  }
702 
703  void p_bool_or(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
704  BOOL_OP(BOT_OR);
705  }
706  void p_bool_and(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
707  BOOL_OP(BOT_AND);
708  }
709  void p_array_bool_and(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
710  {
712  }
713  void p_array_bool_or(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
714  {
716  }
717  void p_array_bool_xor(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
718  {
720  }
721  void p_array_bool_clause(FlatZincSpace& s, const ConExpr& ce,
722  AST::Node* ann) {
723  BoolVarArgs bvp = arg2boolvarargs(s, ce[0]);
724  BoolVarArgs bvn = arg2boolvarargs(s, ce[1]);
725  clause(s, BOT_OR, bvp, bvn, 1, ann2icl(ann));
726  }
727  void p_array_bool_clause_reif(FlatZincSpace& s, const ConExpr& ce,
728  AST::Node* ann) {
729  BoolVarArgs bvp = arg2boolvarargs(s, ce[0]);
730  BoolVarArgs bvn = arg2boolvarargs(s, ce[1]);
731  BoolVar b0 = getBoolVar(s, ce[2]);
732  clause(s, BOT_OR, bvp, bvn, b0, ann2icl(ann));
733  }
734  void p_bool_xor(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
735  BOOL_OP(BOT_XOR);
736  }
737  void p_bool_l_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
738  BoolVar b0 = getBoolVar(s, ce[0]);
739  BoolVar b1 = getBoolVar(s, ce[1]);
740  if (ce[2]->isBool()) {
741  rel(s, b1, BOT_IMP, b0, ce[2]->getBool(), ann2icl(ann));
742  } else {
743  rel(s, b1, BOT_IMP, b0, s.bv[ce[2]->getBoolVar()], ann2icl(ann));
744  }
745  }
746  void p_bool_r_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
747  BOOL_OP(BOT_IMP);
748  }
749  void p_bool_not(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
750  BoolVar x0 = getBoolVar(s, ce[0]);
751  BoolVar x1 = getBoolVar(s, ce[1]);
752  rel(s, x0, BOT_XOR, x1, 1, ann2icl(ann));
753  }
754 
755  /* element constraints */
756  void p_array_int_element(FlatZincSpace& s, const ConExpr& ce,
757  AST::Node* ann) {
758  bool isConstant = true;
759  AST::Array* a = ce[1]->getArray();
760  for (int i=a->a.size(); i--;) {
761  if (!a->a[i]->isInt()) {
762  isConstant = false;
763  break;
764  }
765  }
766  IntVar selector = getIntVar(s, ce[0]);
767  rel(s, selector > 0);
768  if (isConstant) {
769  IntArgs ia = arg2intargs(ce[1], 1);
770  element(s, ia, selector, getIntVar(s, ce[2]), ann2icl(ann));
771  } else {
772  IntVarArgs iv = arg2intvarargs(s, ce[1], 1);
773  element(s, iv, selector, getIntVar(s, ce[2]), ann2icl(ann));
774  }
775  }
776  void p_array_bool_element(FlatZincSpace& s, const ConExpr& ce,
777  AST::Node* ann) {
778  bool isConstant = true;
779  AST::Array* a = ce[1]->getArray();
780  for (int i=a->a.size(); i--;) {
781  if (!a->a[i]->isBool()) {
782  isConstant = false;
783  break;
784  }
785  }
786  IntVar selector = getIntVar(s, ce[0]);
787  rel(s, selector > 0);
788  if (isConstant) {
789  IntArgs ia = arg2boolargs(ce[1], 1);
790  element(s, ia, selector, getBoolVar(s, ce[2]), ann2icl(ann));
791  } else {
792  BoolVarArgs iv = arg2boolvarargs(s, ce[1], 1);
793  element(s, iv, selector, getBoolVar(s, ce[2]), ann2icl(ann));
794  }
795  }
796 
797  /* coercion constraints */
798  void p_bool2int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
799  BoolVar x0 = getBoolVar(s, ce[0]);
800  IntVar x1 = getIntVar(s, ce[1]);
801  if (ce[0]->isBoolVar() && ce[1]->isIntVar()) {
802  s.aliasBool2Int(ce[1]->getIntVar(), ce[0]->getBoolVar());
803  }
804  channel(s, x0, x1, ann2icl(ann));
805  }
806 
807  void p_int_in(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
808  IntSet d = arg2intset(s,ce[1]);
809  if (ce[0]->isBoolVar()) {
810  IntSetRanges dr(d);
811  Iter::Ranges::Singleton sr(0,1);
812  Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr);
813  IntSet d01(i);
814  if (d01.size() == 0) {
815  s.fail();
816  } else {
817  rel(s, getBoolVar(s, ce[0]), IRT_GQ, d01.min());
818  rel(s, getBoolVar(s, ce[0]), IRT_LQ, d01.max());
819  }
820  } else {
821  dom(s, getIntVar(s, ce[0]), d);
822  }
823  }
824  void p_int_in_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
825  IntSet d = arg2intset(s,ce[1]);
826  if (ce[0]->isBoolVar()) {
827  IntSetRanges dr(d);
828  Iter::Ranges::Singleton sr(0,1);
829  Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr);
830  IntSet d01(i);
831  if (d01.size() == 0) {
832  rel(s, getBoolVar(s, ce[2]) == 0);
833  } else if (d01.max() == 0) {
834  rel(s, getBoolVar(s, ce[2]) == !getBoolVar(s, ce[0]));
835  } else if (d01.min() == 1) {
836  rel(s, getBoolVar(s, ce[2]) == getBoolVar(s, ce[0]));
837  } else {
838  rel(s, getBoolVar(s, ce[2]) == 1);
839  }
840  } else {
841  std::cerr << "in_in_reif("<<getIntVar(s, ce[0])<<","<<d<<","<<getBoolVar(s, ce[2])<<")\n";
842  dom(s, getIntVar(s, ce[0]), d, getBoolVar(s, ce[2]));
843  }
844  }
845 
846  /* constraints from the standard library */
847 
848  void p_abs(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
849  IntVar x0 = getIntVar(s, ce[0]);
850  IntVar x1 = getIntVar(s, ce[1]);
851  abs(s, x0, x1, ann2icl(ann));
852  }
853 
854  void p_array_int_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
855  IntVarArgs iv0 = arg2intvarargs(s, ce[0]);
856  IntVarArgs iv1 = arg2intvarargs(s, ce[1]);
857  rel(s, iv0, IRT_LE, iv1, ann2icl(ann));
858  }
859 
860  void p_array_int_lq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
861  IntVarArgs iv0 = arg2intvarargs(s, ce[0]);
862  IntVarArgs iv1 = arg2intvarargs(s, ce[1]);
863  rel(s, iv0, IRT_LQ, iv1, ann2icl(ann));
864  }
865 
866  void p_count(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
867  IntVarArgs iv = arg2intvarargs(s, ce[0]);
868  if (!ce[1]->isIntVar()) {
869  if (!ce[2]->isIntVar()) {
870  count(s, iv, ce[1]->getInt(), IRT_EQ, ce[2]->getInt(),
871  ann2icl(ann));
872  } else {
873  count(s, iv, ce[1]->getInt(), IRT_EQ, getIntVar(s, ce[2]),
874  ann2icl(ann));
875  }
876  } else if (!ce[2]->isIntVar()) {
877  count(s, iv, getIntVar(s, ce[1]), IRT_EQ, ce[2]->getInt(),
878  ann2icl(ann));
879  } else {
880  count(s, iv, getIntVar(s, ce[1]), IRT_EQ, getIntVar(s, ce[2]),
881  ann2icl(ann));
882  }
883  }
884 
885  void count_rel(IntRelType irt,
886  FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
887  IntVarArgs iv = arg2intvarargs(s, ce[1]);
888  count(s, iv, ce[2]->getInt(), irt, ce[0]->getInt(), ann2icl(ann));
889  }
890 
891  void p_at_most(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
892  count_rel(IRT_LQ, s, ce, ann);
893  }
894 
895  void p_at_least(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
896  count_rel(IRT_GQ, s, ce, ann);
897  }
898 
899  void p_bin_packing_load(FlatZincSpace& s, const ConExpr& ce,
900  AST::Node* ann) {
901  int minIdx = ce[3]->getInt();
902  IntVarArgs load = arg2intvarargs(s, ce[0]);
903  IntVarArgs l;
904  IntVarArgs bin = arg2intvarargs(s, ce[1]);
905  for (int i=bin.size(); i--;)
906  rel(s, bin[i] >= minIdx);
907  if (minIdx > 0) {
908  for (int i=minIdx; i--;)
909  l << IntVar(s,0,0);
910  } else if (minIdx < 0) {
911  IntVarArgs bin2(bin.size());
912  for (int i=bin.size(); i--;)
913  bin2[i] = expr(s, bin[i]-minIdx, ann2icl(ann));
914  bin = bin2;
915  }
916  l << load;
917  IntArgs sizes = arg2intargs(ce[2]);
918  binpacking(s, l, bin, sizes, ann2icl(ann));
919  }
920 
921  void p_global_cardinality(FlatZincSpace& s, const ConExpr& ce,
922  AST::Node* ann) {
923  IntVarArgs iv0 = arg2intvarargs(s, ce[0]);
924  IntArgs cover = arg2intargs(ce[1]);
925  IntVarArgs iv1 = arg2intvarargs(s, ce[2]);
926 
927  Region re(s);
928  IntSet cover_s(cover);
929  IntSetRanges cover_r(cover_s);
930  IntVarRanges* iv0_ri = re.alloc<IntVarRanges>(iv0.size());
931  for (int i=iv0.size(); i--;)
932  iv0_ri[i] = IntVarRanges(iv0[i]);
933  Iter::Ranges::NaryUnion iv0_r(re,iv0_ri,iv0.size());
934  Iter::Ranges::Diff<Iter::Ranges::NaryUnion,IntSetRanges>
935  extra_r(iv0_r,cover_r);
936  Iter::Ranges::ToValues<Iter::Ranges::Diff<
937  Iter::Ranges::NaryUnion,IntSetRanges> > extra(extra_r);
938  for (; extra(); ++extra) {
939  cover << extra.val();
940  iv1 << IntVar(s,0,iv0.size());
941  }
942  count(s, iv0, iv1, cover, ann2icl(ann));
943  }
944 
945  void p_global_cardinality_closed(FlatZincSpace& s, const ConExpr& ce,
946  AST::Node* ann) {
947  IntVarArgs iv0 = arg2intvarargs(s, ce[0]);
948  IntArgs cover = arg2intargs(ce[1]);
949  IntVarArgs iv1 = arg2intvarargs(s, ce[2]);
950  count(s, iv0, iv1, cover, ann2icl(ann));
951  }
952 
953  void p_global_cardinality_low_up(FlatZincSpace& s, const ConExpr& ce,
954  AST::Node* ann) {
955  IntVarArgs x = arg2intvarargs(s, ce[0]);
956  IntArgs cover = arg2intargs(ce[1]);
957 
958  IntArgs lbound = arg2intargs(ce[2]);
959  IntArgs ubound = arg2intargs(ce[3]);
960  IntSetArgs y(cover.size());
961  for (int i=cover.size(); i--;)
962  y[i] = IntSet(lbound[i],ubound[i]);
963 
964  IntSet cover_s(cover);
965  Region re(s);
966  IntVarRanges* xrs = re.alloc<IntVarRanges>(x.size());
967  for (int i=x.size(); i--;)
968  xrs[i].init(x[i]);
969  Iter::Ranges::NaryUnion u(re, xrs, x.size());
970  Iter::Ranges::ToValues<Iter::Ranges::NaryUnion> uv(u);
971  for (; uv(); ++uv) {
972  if (!cover_s.in(uv.val())) {
973  cover << uv.val();
974  y << IntSet(0,x.size());
975  }
976  }
977 
978  count(s, x, y, cover, ann2icl(ann));
979  }
980 
981  void p_global_cardinality_low_up_closed(FlatZincSpace& s,
982  const ConExpr& ce,
983  AST::Node* ann) {
984  IntVarArgs x = arg2intvarargs(s, ce[0]);
985  IntArgs cover = arg2intargs(ce[1]);
986 
987  IntArgs lbound = arg2intargs(ce[2]);
988  IntArgs ubound = arg2intargs(ce[3]);
989  IntSetArgs y(cover.size());
990  for (int i=cover.size(); i--;)
991  y[i] = IntSet(lbound[i],ubound[i]);
992 
993  count(s, x, y, cover, ann2icl(ann));
994  }
995 
996  void p_minimum(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
997  IntVarArgs iv = arg2intvarargs(s, ce[1]);
998  min(s, iv, getIntVar(s, ce[0]), ann2icl(ann));
999  }
1000 
1001  void p_maximum(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1002  IntVarArgs iv = arg2intvarargs(s, ce[1]);
1003  max(s, iv, getIntVar(s, ce[0]), ann2icl(ann));
1004  }
1005 
1006  void p_regular(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1007  IntVarArgs iv = arg2intvarargs(s, ce[0]);
1008  int q = ce[1]->getInt();
1009  int symbols = ce[2]->getInt();
1010  IntArgs d = arg2intargs(ce[3]);
1011  int q0 = ce[4]->getInt();
1012 
1013  int noOfTrans = 0;
1014  for (int i=1; i<=q; i++) {
1015  for (int j=1; j<=symbols; j++) {
1016  if (d[(i-1)*symbols+(j-1)] > 0)
1017  noOfTrans++;
1018  }
1019  }
1020 
1021  Region re(s);
1022  DFA::Transition* t = re.alloc<DFA::Transition>(noOfTrans+1);
1023  noOfTrans = 0;
1024  for (int i=1; i<=q; i++) {
1025  for (int j=1; j<=symbols; j++) {
1026  if (d[(i-1)*symbols+(j-1)] > 0) {
1027  t[noOfTrans].i_state = i;
1028  t[noOfTrans].symbol = j;
1029  t[noOfTrans].o_state = d[(i-1)*symbols+(j-1)];
1030  noOfTrans++;
1031  }
1032  }
1033  }
1034  t[noOfTrans].i_state = -1;
1035 
1036  // Final states
1037  AST::SetLit* sl = ce[5]->getSet();
1038  int* f;
1039  if (sl->interval) {
1040  f = static_cast<int*>(malloc(sizeof(int)*(sl->max-sl->min+2)));
1041  for (int i=sl->min; i<=sl->max; i++)
1042  f[i-sl->min] = i;
1043  f[sl->max-sl->min+1] = -1;
1044  } else {
1045  f = static_cast<int*>(malloc(sizeof(int)*(sl->s.size()+1)));
1046  for (int j=sl->s.size(); j--; )
1047  f[j] = sl->s[j];
1048  f[sl->s.size()] = -1;
1049  }
1050 
1051  DFA dfa(q0,t,f);
1052  free(f);
1053  extensional(s, iv, dfa, ann2icl(ann));
1054  }
1055 
1056  void
1057  p_sort(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1058  IntVarArgs x = arg2intvarargs(s, ce[0]);
1059  IntVarArgs y = arg2intvarargs(s, ce[1]);
1060  IntVarArgs xy(x.size()+y.size());
1061  for (int i=x.size(); i--;)
1062  xy[i] = x[i];
1063  for (int i=y.size(); i--;)
1064  xy[i+x.size()] = y[i];
1065  unshare(s, xy);
1066  for (int i=x.size(); i--;)
1067  x[i] = xy[i];
1068  for (int i=y.size(); i--;)
1069  y[i] = xy[i+x.size()];
1070  sorted(s, x, y, ann2icl(ann));
1071  }
1072 
1073  void
1074  p_inverse_offsets(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1075  IntVarArgs x = arg2intvarargs(s, ce[0]);
1076  int xoff = ce[1]->getInt();
1077  IntVarArgs y = arg2intvarargs(s, ce[2]);
1078  int yoff = ce[3]->getInt();
1079  channel(s, x, xoff, y, yoff, ann2icl(ann));
1080  }
1081 
1082  void
1083  p_increasing_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1084  IntVarArgs x = arg2intvarargs(s, ce[0]);
1085  rel(s,x,IRT_LQ,ann2icl(ann));
1086  }
1087 
1088  void
1089  p_increasing_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1090  BoolVarArgs x = arg2boolvarargs(s, ce[0]);
1091  rel(s,x,IRT_LQ,ann2icl(ann));
1092  }
1093 
1094  void
1095  p_decreasing_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1096  IntVarArgs x = arg2intvarargs(s, ce[0]);
1097  rel(s,x,IRT_GQ,ann2icl(ann));
1098  }
1099 
1100  void
1101  p_decreasing_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1102  BoolVarArgs x = arg2boolvarargs(s, ce[0]);
1103  rel(s,x,IRT_GQ,ann2icl(ann));
1104  }
1105 
1106  void
1107  p_table_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1108  IntVarArgs x = arg2intvarargs(s, ce[0]);
1109  IntArgs tuples = arg2intargs(ce[1]);
1110  int noOfVars = x.size();
1111  int noOfTuples = tuples.size()/noOfVars;
1112  TupleSet ts;
1113  for (int i=0; i<noOfTuples; i++) {
1114  IntArgs t(noOfVars);
1115  for (int j=0; j<x.size(); j++) {
1116  t[j] = tuples[i*noOfVars+j];
1117  }
1118  ts.add(t);
1119  }
1120  ts.finalize();
1121  extensional(s,x,ts,EPK_DEF,ann2icl(ann));
1122  }
1123  void
1124  p_table_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1125  BoolVarArgs x = arg2boolvarargs(s, ce[0]);
1126  IntArgs tuples = arg2boolargs(ce[1]);
1127  int noOfVars = x.size();
1128  int noOfTuples = tuples.size()/noOfVars;
1129  TupleSet ts;
1130  for (int i=0; i<noOfTuples; i++) {
1131  IntArgs t(noOfVars);
1132  for (int j=0; j<x.size(); j++) {
1133  t[j] = tuples[i*noOfVars+j];
1134  }
1135  ts.add(t);
1136  }
1137  ts.finalize();
1138  extensional(s,x,ts,EPK_DEF,ann2icl(ann));
1139  }
1140 
1141  void p_cumulatives(FlatZincSpace& s, const ConExpr& ce,
1142  AST::Node* ann) {
1143  IntVarArgs start = arg2intvarargs(s, ce[0]);
1144  IntVarArgs duration = arg2intvarargs(s, ce[1]);
1145  IntVarArgs height = arg2intvarargs(s, ce[2]);
1146  int n = start.size();
1147  IntVar bound = getIntVar(s, ce[3]);
1148 
1149  int minHeight = INT_MAX; int minHeight2 = INT_MAX;
1150  for (int i=n; i--;)
1151  if (height[i].min() < minHeight)
1152  minHeight = height[i].min();
1153  else if (height[i].min() < minHeight2)
1154  minHeight2 = height[i].min();
1155  bool disjunctive =
1156  (minHeight > bound.max()/2) ||
1157  (minHeight2 > bound.max()/2 && minHeight+minHeight2>bound.max());
1158  if (disjunctive) {
1159  rel(s, bound >= max(height));
1160  // Unary
1161  if (duration.assigned()) {
1162  IntArgs durationI(n);
1163  for (int i=n; i--;)
1164  durationI[i] = duration[i].val();
1165  unary(s,start,durationI);
1166  } else {
1167  IntVarArgs end(n);
1168  for (int i=n; i--;)
1169  end[i] = expr(s,start[i]+duration[i]);
1170  unary(s,start,duration,end);
1171  }
1172  } else if (height.assigned()) {
1173  IntArgs heightI(n);
1174  for (int i=n; i--;)
1175  heightI[i] = height[i].val();
1176  if (duration.assigned()) {
1177  IntArgs durationI(n);
1178  for (int i=n; i--;)
1179  durationI[i] = duration[i].val();
1180  cumulative(s, bound, start, durationI, heightI);
1181  } else {
1182  IntVarArgs end(n);
1183  for (int i = n; i--; )
1184  end[i] = expr(s,start[i]+duration[i]);
1185  cumulative(s, bound, start, duration, end, heightI);
1186  }
1187  } else if (bound.assigned()) {
1188  IntArgs machine = IntArgs::create(n,0,0);
1189  IntArgs limit(1, bound.val());
1190  IntVarArgs end(n);
1191  for (int i=n; i--;)
1192  end[i] = expr(s,start[i]+duration[i]);
1193  cumulatives(s, machine, start, duration, end, height, limit, true,
1194  ann2icl(ann));
1195  } else {
1198  IntVarArgs end(start.size());
1199  for (int i = start.size(); i--; ) {
1200  min = std::min(min, start[i].min());
1201  max = std::max(max, start[i].max() + duration[i].max());
1202  end[i] = expr(s, start[i] + duration[i]);
1203  }
1204  for (int time = min; time < max; ++time) {
1205  IntVarArgs x(start.size());
1206  for (int i = start.size(); i--; ) {
1207  IntVar overlaps = channel(s, expr(s, (start[i] <= time) &&
1208  (time < end[i])));
1209  x[i] = expr(s, overlaps * height[i]);
1210  }
1211  linear(s, x, IRT_LQ, bound);
1212  }
1213  }
1214  }
1215 
1216  void p_among_seq_int(FlatZincSpace& s, const ConExpr& ce,
1217  AST::Node* ann) {
1218  IntVarArgs x = arg2intvarargs(s, ce[0]);
1219  IntSet S = arg2intset(s, ce[1]);
1220  int q = ce[2]->getInt();
1221  int l = ce[3]->getInt();
1222  int u = ce[4]->getInt();
1223  sequence(s, x, S, q, l, u, ann2icl(ann));
1224  }
1225 
1226  void p_among_seq_bool(FlatZincSpace& s, const ConExpr& ce,
1227  AST::Node* ann) {
1228  BoolVarArgs x = arg2boolvarargs(s, ce[0]);
1229  bool val = ce[1]->getBool();
1230  int q = ce[2]->getInt();
1231  int l = ce[3]->getInt();
1232  int u = ce[4]->getInt();
1233  IntSet S(val, val);
1234  sequence(s, x, S, q, l, u, ann2icl(ann));
1235  }
1236 
1237  void p_schedule_unary(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
1238  IntVarArgs x = arg2intvarargs(s, ce[0]);
1239  IntArgs p = arg2intargs(ce[1]);
1240  unary(s, x, p);
1241  }
1242 
1243  void p_schedule_unary_optional(FlatZincSpace& s, const ConExpr& ce,
1244  AST::Node*) {
1245  IntVarArgs x = arg2intvarargs(s, ce[0]);
1246  IntArgs p = arg2intargs(ce[1]);
1247  BoolVarArgs m = arg2boolvarargs(s, ce[2]);
1248  unary(s, x, p, m);
1249  }
1250 
1251  void p_circuit(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
1252  IntVarArgs xv = arg2intvarargs(s, ce[0]);
1253  circuit(s,xv,ann2icl(ann));
1254  }
1255  void p_circuit_cost_array(FlatZincSpace& s, const ConExpr& ce,
1256  AST::Node *ann) {
1257  IntArgs c = arg2intargs(ce[0]);
1258  IntVarArgs xv = arg2intvarargs(s, ce[1]);
1259  IntVarArgs yv = arg2intvarargs(s, ce[2]);
1260  IntVar z = getIntVar(s, ce[3]);
1261  circuit(s,c,xv,yv,z,ann2icl(ann));
1262  }
1263  void p_circuit_cost(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
1264  IntArgs c = arg2intargs(ce[0]);
1265  IntVarArgs xv = arg2intvarargs(s, ce[1]);
1266  IntVar z = getIntVar(s, ce[2]);
1267  circuit(s,c,xv,z,ann2icl(ann));
1268  }
1269 
1270  void p_nooverlap(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
1271  IntVarArgs x0 = arg2intvarargs(s, ce[0]);
1272  IntVarArgs w = arg2intvarargs(s, ce[1]);
1273  IntVarArgs y0 = arg2intvarargs(s, ce[2]);
1274  IntVarArgs h = arg2intvarargs(s, ce[3]);
1275  IntVarArgs x1(x0.size()), y1(y0.size());
1276  for (int i=x0.size(); i--; )
1277  x1[i] = expr(s, x0[i] + w[i]);
1278  for (int i=y0.size(); i--; )
1279  y1[i] = expr(s, y0[i] + h[i]);
1280  nooverlap(s,x0,w,x1,y0,h,y1,ann2icl(ann));
1281  }
1282 
1283  void p_precede(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1284  IntVarArgs x = arg2intvarargs(s, ce[0]);
1285  IntArgs c = arg2intargs(ce[1]);
1286  precede(s,x,c,ann2icl(ann));
1287  }
1288 
1289  void p_nvalue(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1290  IntVarArgs x = arg2intvarargs(s, ce[1]);
1291  if (ce[0]->isIntVar()) {
1292  IntVar y = getIntVar(s,ce[0]);
1293  nvalues(s,x,IRT_EQ,y,ann2icl(ann));
1294  } else {
1295  nvalues(s,x,IRT_EQ,ce[0]->getInt(),ann2icl(ann));
1296  }
1297  }
1298 
1299  void p_among(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1300  IntVarArgs x = arg2intvarargs(s, ce[1]);
1301  IntSet v = arg2intset(s, ce[2]);
1302  if (ce[0]->isIntVar()) {
1303  IntVar n = getIntVar(s,ce[0]);
1304  std::cerr << "count " << n << std::endl;
1305  count(s,x,v,IRT_EQ,n,ann2icl(ann));
1306  } else {
1307  std::cerr << "count i " << x << " " << v << " " << ce[0]->getInt() << std::endl;
1308  count(s,x,v,IRT_EQ,ce[0]->getInt(),ann2icl(ann));
1309  }
1310  }
1311 
1312  void p_member_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1313  IntVarArgs x = arg2intvarargs(s, ce[0]);
1314  IntVar y = getIntVar(s, ce[1]);
1315  member(s,x,y,ann2icl(ann));
1316  }
1317  void p_member_int_reif(FlatZincSpace& s, const ConExpr& ce,
1318  AST::Node* ann) {
1319  IntVarArgs x = arg2intvarargs(s, ce[0]);
1320  IntVar y = getIntVar(s, ce[1]);
1321  BoolVar b = getBoolVar(s, ce[2]);
1322  member(s,x,y,b,ann2icl(ann));
1323  }
1324  void p_member_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1325  BoolVarArgs x = arg2boolvarargs(s, ce[0]);
1326  BoolVar y = getBoolVar(s, ce[1]);
1327  member(s,x,y,ann2icl(ann));
1328  }
1329  void p_member_bool_reif(FlatZincSpace& s, const ConExpr& ce,
1330  AST::Node* ann) {
1331  BoolVarArgs x = arg2boolvarargs(s, ce[0]);
1332  BoolVar y = getBoolVar(s, ce[1]);
1333  member(s,x,y,getBoolVar(s, ce[2]),ann2icl(ann));
1334  }
1335 
1336  class IntPoster {
1337  public:
1338  IntPoster(void) {
1339  registry().add("all_different_int", &p_distinct);
1340  registry().add("all_different_offset", &p_distinctOffset);
1341  registry().add("all_equal_int", &p_all_equal);
1342  registry().add("int_eq", &p_int_eq);
1343  registry().add("int_ne", &p_int_ne);
1344  registry().add("int_ge", &p_int_ge);
1345  registry().add("int_gt", &p_int_gt);
1346  registry().add("int_le", &p_int_le);
1347  registry().add("int_lt", &p_int_lt);
1348  registry().add("int_eq_reif", &p_int_eq_reif);
1349  registry().add("int_ne_reif", &p_int_ne_reif);
1350  registry().add("int_ge_reif", &p_int_ge_reif);
1351  registry().add("int_gt_reif", &p_int_gt_reif);
1352  registry().add("int_le_reif", &p_int_le_reif);
1353  registry().add("int_lt_reif", &p_int_lt_reif);
1354  registry().add("int_lin_eq", &p_int_lin_eq);
1355  registry().add("int_lin_eq_reif", &p_int_lin_eq_reif);
1356  registry().add("int_lin_ne", &p_int_lin_ne);
1357  registry().add("int_lin_ne_reif", &p_int_lin_ne_reif);
1358  registry().add("int_lin_le", &p_int_lin_le);
1359  registry().add("int_lin_le_reif", &p_int_lin_le_reif);
1360  registry().add("int_lin_lt", &p_int_lin_lt);
1361  registry().add("int_lin_lt_reif", &p_int_lin_lt_reif);
1362  registry().add("int_lin_ge", &p_int_lin_ge);
1363  registry().add("int_lin_ge_reif", &p_int_lin_ge_reif);
1364  registry().add("int_lin_gt", &p_int_lin_gt);
1365  registry().add("int_lin_gt_reif", &p_int_lin_gt_reif);
1366  registry().add("int_plus", &p_int_plus);
1367  registry().add("int_minus", &p_int_minus);
1368  registry().add("int_times", &p_int_times);
1369  registry().add("int_div", &p_int_div);
1370  registry().add("int_mod", &p_int_mod);
1371  registry().add("int_min", &p_int_min);
1372  registry().add("int_max", &p_int_max);
1373  registry().add("int_abs", &p_abs);
1374  registry().add("int_negate", &p_int_negate);
1375  registry().add("bool_eq", &p_bool_eq);
1376  registry().add("bool_eq_reif", &p_bool_eq_reif);
1377  registry().add("bool_ne", &p_bool_ne);
1378  registry().add("bool_ne_reif", &p_bool_ne_reif);
1379  registry().add("bool_ge", &p_bool_ge);
1380  registry().add("bool_ge_reif", &p_bool_ge_reif);
1381  registry().add("bool_le", &p_bool_le);
1382  registry().add("bool_le_reif", &p_bool_le_reif);
1383  registry().add("bool_gt", &p_bool_gt);
1384  registry().add("bool_gt_reif", &p_bool_gt_reif);
1385  registry().add("bool_lt", &p_bool_lt);
1386  registry().add("bool_lt_reif", &p_bool_lt_reif);
1387  registry().add("bool_or", &p_bool_or);
1388  registry().add("bool_and", &p_bool_and);
1389  registry().add("bool_xor", &p_bool_xor);
1390  registry().add("array_bool_and", &p_array_bool_and);
1391  registry().add("array_bool_or", &p_array_bool_or);
1392  registry().add("array_bool_xor", &p_array_bool_xor);
1393  registry().add("bool_clause", &p_array_bool_clause);
1394  registry().add("bool_clause_reif", &p_array_bool_clause_reif);
1395  registry().add("bool_left_imp", &p_bool_l_imp);
1396  registry().add("bool_right_imp", &p_bool_r_imp);
1397  registry().add("bool_not", &p_bool_not);
1398  registry().add("array_int_element", &p_array_int_element);
1399  registry().add("array_var_int_element", &p_array_int_element);
1400  registry().add("array_bool_element", &p_array_bool_element);
1401  registry().add("array_var_bool_element", &p_array_bool_element);
1402  registry().add("bool2int", &p_bool2int);
1403  registry().add("int_in", &p_int_in);
1404  registry().add("int_in_reif", &p_int_in_reif);
1405 #ifndef GECODE_HAS_SET_VARS
1406  registry().add("set_in", &p_int_in);
1407  registry().add("set_in_reif", &p_int_in_reif);
1408 #endif
1409 
1410  registry().add("array_int_lt", &p_array_int_lt);
1411  registry().add("array_int_lq", &p_array_int_lq);
1412  registry().add("count", &p_count);
1413  registry().add("at_least_int", &p_at_least);
1414  registry().add("at_most_int", &p_at_most);
1415  registry().add("gecode_bin_packing_load", &p_bin_packing_load);
1416  registry().add("global_cardinality", &p_global_cardinality);
1417  registry().add("global_cardinality_closed",
1418  &p_global_cardinality_closed);
1419  registry().add("global_cardinality_low_up",
1420  &p_global_cardinality_low_up);
1421  registry().add("global_cardinality_low_up_closed",
1422  &p_global_cardinality_low_up_closed);
1423  registry().add("minimum_int", &p_minimum);
1424  registry().add("maximum_int", &p_maximum);
1425  registry().add("regular", &p_regular);
1426  registry().add("sort", &p_sort);
1427  registry().add("inverse_offsets", &p_inverse_offsets);
1428  registry().add("increasing_int", &p_increasing_int);
1429  registry().add("increasing_bool", &p_increasing_bool);
1430  registry().add("decreasing_int", &p_decreasing_int);
1431  registry().add("decreasing_bool", &p_decreasing_bool);
1432  registry().add("table_int", &p_table_int);
1433  registry().add("table_bool", &p_table_bool);
1434  registry().add("cumulatives", &p_cumulatives);
1435  registry().add("gecode_among_seq_int", &p_among_seq_int);
1436  registry().add("gecode_among_seq_bool", &p_among_seq_bool);
1437 
1438  registry().add("bool_lin_eq", &p_bool_lin_eq);
1439  registry().add("bool_lin_ne", &p_bool_lin_ne);
1440  registry().add("bool_lin_le", &p_bool_lin_le);
1441  registry().add("bool_lin_lt", &p_bool_lin_lt);
1442  registry().add("bool_lin_ge", &p_bool_lin_ge);
1443  registry().add("bool_lin_gt", &p_bool_lin_gt);
1444 
1445  registry().add("bool_lin_eq_reif", &p_bool_lin_eq_reif);
1446  registry().add("bool_lin_ne_reif", &p_bool_lin_ne_reif);
1447  registry().add("bool_lin_le_reif", &p_bool_lin_le_reif);
1448  registry().add("bool_lin_lt_reif", &p_bool_lin_lt_reif);
1449  registry().add("bool_lin_ge_reif", &p_bool_lin_ge_reif);
1450  registry().add("bool_lin_gt_reif", &p_bool_lin_gt_reif);
1451 
1452  registry().add("gecode_schedule_unary", &p_schedule_unary);
1453  registry().add("gecode_schedule_unary_optional", &p_schedule_unary_optional);
1454 
1455  registry().add("gecode_circuit", &p_circuit);
1456  registry().add("gecode_circuit_cost_array", &p_circuit_cost_array);
1457  registry().add("gecode_circuit_cost", &p_circuit_cost);
1458  registry().add("gecode_nooverlap", &p_nooverlap);
1459  registry().add("gecode_precede", &p_precede);
1460  registry().add("nvalue",&p_nvalue);
1461  registry().add("among",&p_among);
1462  registry().add("member_int",&p_member_int);
1463  registry().add("gecode_member_int_reif",&p_member_int_reif);
1464  registry().add("member_bool",&p_member_bool);
1465  registry().add("gecode_member_bool_reif",&p_member_bool_reif);
1466  }
1467  };
1468  IntPoster __int_poster;
1469 
1470 #ifdef GECODE_HAS_SET_VARS
1471  void p_set_OP(FlatZincSpace& s, SetOpType op,
1472  const ConExpr& ce, AST::Node *) {
1473  rel(s, getSetVar(s, ce[0]), op, getSetVar(s, ce[1]),
1474  SRT_EQ, getSetVar(s, ce[2]));
1475  }
1476  void p_set_union(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
1477  p_set_OP(s, SOT_UNION, ce, ann);
1478  }
1479  void p_set_intersect(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
1480  p_set_OP(s, SOT_INTER, ce, ann);
1481  }
1482  void p_set_diff(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
1483  p_set_OP(s, SOT_MINUS, ce, ann);
1484  }
1485 
1486  void p_set_symdiff(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
1487  SetVar x = getSetVar(s, ce[0]);
1488  SetVar y = getSetVar(s, ce[1]);
1489 
1490  SetVarLubRanges xub(x);
1491  IntSet xubs(xub);
1492  SetVar x_y(s,IntSet::empty,xubs);
1493  rel(s, x, SOT_MINUS, y, SRT_EQ, x_y);
1494 
1495  SetVarLubRanges yub(y);
1496  IntSet yubs(yub);
1497  SetVar y_x(s,IntSet::empty,yubs);
1498  rel(s, y, SOT_MINUS, x, SRT_EQ, y_x);
1499 
1500  rel(s, x_y, SOT_UNION, y_x, SRT_EQ, getSetVar(s, ce[2]));
1501  }
1502 
1503  void p_array_set_OP(FlatZincSpace& s, SetOpType op,
1504  const ConExpr& ce, AST::Node *) {
1505  SetVarArgs xs = arg2setvarargs(s, ce[0]);
1506  rel(s, op, xs, getSetVar(s, ce[1]));
1507  }
1508  void p_array_set_union(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
1509  p_array_set_OP(s, SOT_UNION, ce, ann);
1510  }
1511  void p_array_set_partition(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
1512  p_array_set_OP(s, SOT_DUNION, ce, ann);
1513  }
1514 
1515 
1516  void p_set_rel(FlatZincSpace& s, SetRelType srt, const ConExpr& ce) {
1517  rel(s, getSetVar(s, ce[0]), srt, getSetVar(s, ce[1]));
1518  }
1519 
1520  void p_set_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1521  p_set_rel(s, SRT_EQ, ce);
1522  }
1523  void p_set_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1524  p_set_rel(s, SRT_NQ, ce);
1525  }
1526  void p_set_subset(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1527  p_set_rel(s, SRT_SUB, ce);
1528  }
1529  void p_set_superset(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1530  p_set_rel(s, SRT_SUP, ce);
1531  }
1532  void p_set_le(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1533  p_set_rel(s, SRT_LQ, ce);
1534  }
1535  void p_set_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1536  p_set_rel(s, SRT_LE, ce);
1537  }
1538  void p_set_card(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1539  if (!ce[1]->isIntVar()) {
1540  cardinality(s, getSetVar(s, ce[0]), ce[1]->getInt(),
1541  ce[1]->getInt());
1542  } else {
1543  cardinality(s, getSetVar(s, ce[0]), getIntVar(s, ce[1]));
1544  }
1545  }
1546  void p_set_in(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1547  if (!ce[1]->isSetVar()) {
1548  IntSet d = arg2intset(s,ce[1]);
1549  if (ce[0]->isBoolVar()) {
1550  IntSetRanges dr(d);
1551  Iter::Ranges::Singleton sr(0,1);
1552  Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr);
1553  IntSet d01(i);
1554  if (d01.size() == 0) {
1555  s.fail();
1556  } else {
1557  rel(s, getBoolVar(s, ce[0]), IRT_GQ, d01.min());
1558  rel(s, getBoolVar(s, ce[0]), IRT_LQ, d01.max());
1559  }
1560  } else {
1561  dom(s, getIntVar(s, ce[0]), d);
1562  }
1563  } else {
1564  if (!ce[0]->isIntVar()) {
1565  dom(s, getSetVar(s, ce[1]), SRT_SUP, ce[0]->getInt());
1566  } else {
1567  rel(s, getSetVar(s, ce[1]), SRT_SUP, getIntVar(s, ce[0]));
1568  }
1569  }
1570  }
1571  void p_set_rel_reif(FlatZincSpace& s, SetRelType srt, const ConExpr& ce) {
1572  rel(s, getSetVar(s, ce[0]), srt, getSetVar(s, ce[1]),
1573  getBoolVar(s, ce[2]));
1574  }
1575 
1576  void p_set_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1577  p_set_rel_reif(s,SRT_EQ,ce);
1578  }
1579  void p_set_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1580  p_set_rel_reif(s,SRT_LQ,ce);
1581  }
1582  void p_set_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1583  p_set_rel_reif(s,SRT_LE,ce);
1584  }
1585  void p_set_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1586  p_set_rel_reif(s,SRT_NQ,ce);
1587  }
1588  void p_set_subset_reif(FlatZincSpace& s, const ConExpr& ce,
1589  AST::Node *) {
1590  p_set_rel_reif(s,SRT_SUB,ce);
1591  }
1592  void p_set_superset_reif(FlatZincSpace& s, const ConExpr& ce,
1593  AST::Node *) {
1594  p_set_rel_reif(s,SRT_SUP,ce);
1595  }
1596  void p_set_in_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1597  if (!ce[1]->isSetVar()) {
1598  IntSet d = arg2intset(s,ce[1]);
1599  if (ce[0]->isBoolVar()) {
1600  IntSetRanges dr(d);
1601  Iter::Ranges::Singleton sr(0,1);
1602  Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr);
1603  IntSet d01(i);
1604  if (d01.size() == 0) {
1605  rel(s, getBoolVar(s, ce[2]) == 0);
1606  } else if (d01.max() == 0) {
1607  rel(s, getBoolVar(s, ce[2]) == !getBoolVar(s, ce[0]));
1608  } else if (d01.min() == 1) {
1609  rel(s, getBoolVar(s, ce[2]) == getBoolVar(s, ce[0]));
1610  } else {
1611  rel(s, getBoolVar(s, ce[2]) == 1);
1612  }
1613  } else {
1614  dom(s, getIntVar(s, ce[0]), d, getBoolVar(s, ce[2]));
1615  }
1616  } else {
1617  if (!ce[0]->isIntVar()) {
1618  dom(s, getSetVar(s, ce[1]), SRT_SUP, ce[0]->getInt(),
1619  getBoolVar(s, ce[2]));
1620  } else {
1621  rel(s, getSetVar(s, ce[1]), SRT_SUP, getIntVar(s, ce[0]),
1622  getBoolVar(s, ce[2]));
1623  }
1624  }
1625  }
1626  void p_set_disjoint(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1627  rel(s, getSetVar(s, ce[0]), SRT_DISJ, getSetVar(s, ce[1]));
1628  }
1629 
1630  void p_link_set_to_booleans(FlatZincSpace& s, const ConExpr& ce,
1631  AST::Node *) {
1632  SetVar x = getSetVar(s, ce[0]);
1633  int idx = ce[2]->getInt();
1634  assert(idx >= 0);
1635  rel(s, x || IntSet(Set::Limits::min,idx-1));
1636  BoolVarArgs y = arg2boolvarargs(s,ce[1],idx);
1637  channel(s, y, x);
1638  }
1639 
1640  void p_array_set_element(FlatZincSpace& s, const ConExpr& ce,
1641  AST::Node*) {
1642  bool isConstant = true;
1643  AST::Array* a = ce[1]->getArray();
1644  for (int i=a->a.size(); i--;) {
1645  if (a->a[i]->isSetVar()) {
1646  isConstant = false;
1647  break;
1648  }
1649  }
1650  IntVar selector = getIntVar(s, ce[0]);
1651  rel(s, selector > 0);
1652  if (isConstant) {
1653  IntSetArgs sv = arg2intsetargs(s,ce[1],1);
1654  element(s, sv, selector, getSetVar(s, ce[2]));
1655  } else {
1656  SetVarArgs sv = arg2setvarargs(s, ce[1], 1);
1657  element(s, sv, selector, getSetVar(s, ce[2]));
1658  }
1659  }
1660 
1661  void p_array_set_element_op(FlatZincSpace& s, const ConExpr& ce,
1662  AST::Node*, SetOpType op,
1663  const IntSet& universe =
1665  bool isConstant = true;
1666  AST::Array* a = ce[1]->getArray();
1667  for (int i=a->a.size(); i--;) {
1668  if (a->a[i]->isSetVar()) {
1669  isConstant = false;
1670  break;
1671  }
1672  }
1673  SetVar selector = getSetVar(s, ce[0]);
1674  dom(s, selector, SRT_DISJ, 0);
1675  if (isConstant) {
1676  IntSetArgs sv = arg2intsetargs(s,ce[1], 1);
1677  element(s, op, sv, selector, getSetVar(s, ce[2]), universe);
1678  } else {
1679  SetVarArgs sv = arg2setvarargs(s, ce[1], 1);
1680  element(s, op, sv, selector, getSetVar(s, ce[2]), universe);
1681  }
1682  }
1683 
1684  void p_array_set_element_union(FlatZincSpace& s, const ConExpr& ce,
1685  AST::Node* ann) {
1686  p_array_set_element_op(s, ce, ann, SOT_UNION);
1687  }
1688 
1689  void p_array_set_element_intersect(FlatZincSpace& s, const ConExpr& ce,
1690  AST::Node* ann) {
1691  p_array_set_element_op(s, ce, ann, SOT_INTER);
1692  }
1693 
1694  void p_array_set_element_intersect_in(FlatZincSpace& s,
1695  const ConExpr& ce,
1696  AST::Node* ann) {
1697  IntSet d = arg2intset(s, ce[3]);
1698  p_array_set_element_op(s, ce, ann, SOT_INTER, d);
1699  }
1700 
1701  void p_array_set_element_partition(FlatZincSpace& s, const ConExpr& ce,
1702  AST::Node* ann) {
1703  p_array_set_element_op(s, ce, ann, SOT_DUNION);
1704  }
1705 
1706  void p_set_convex(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1707  convex(s, getSetVar(s, ce[0]));
1708  }
1709 
1710  void p_array_set_seq(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1711  SetVarArgs sv = arg2setvarargs(s, ce[0]);
1712  sequence(s, sv);
1713  }
1714 
1715  void p_array_set_seq_union(FlatZincSpace& s, const ConExpr& ce,
1716  AST::Node *) {
1717  SetVarArgs sv = arg2setvarargs(s, ce[0]);
1718  sequence(s, sv, getSetVar(s, ce[1]));
1719  }
1720 
1721  void p_int_set_channel(FlatZincSpace& s, const ConExpr& ce,
1722  AST::Node *) {
1723  int xoff=ce[1]->getInt();
1724  assert(xoff >= 0);
1725  int yoff=ce[3]->getInt();
1726  assert(yoff >= 0);
1727  IntVarArgs xv = arg2intvarargs(s, ce[0], xoff);
1728  SetVarArgs yv = arg2setvarargs(s, ce[2], yoff, 1, IntSet(0, xoff-1));
1729  IntSet xd(yoff,yv.size()-1);
1730  for (int i=xoff; i<xv.size(); i++) {
1731  dom(s, xv[i], xd);
1732  }
1733  IntSet yd(xoff,xv.size()-1);
1734  for (int i=yoff; i<yv.size(); i++) {
1735  dom(s, yv[i], SRT_SUB, yd);
1736  }
1737  channel(s,xv,yv);
1738  }
1739 
1740  void p_range(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
1741  int xoff=ce[1]->getInt();
1742  assert(xoff >= 0);
1743  IntVarArgs xv = arg2intvarargs(s,ce[0],xoff);
1744  element(s, SOT_UNION, xv, getSetVar(s,ce[2]), getSetVar(s,ce[3]));
1745  }
1746 
1747  void p_weights(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
1748  IntArgs e = arg2intargs(ce[0]);
1749  IntArgs w = arg2intargs(ce[1]);
1750  SetVar x = getSetVar(s,ce[2]);
1751  IntVar y = getIntVar(s,ce[3]);
1752  weights(s,e,w,x,y);
1753  }
1754 
1755  class SetPoster {
1756  public:
1757  SetPoster(void) {
1758  registry().add("set_eq", &p_set_eq);
1759  registry().add("set_le", &p_set_le);
1760  registry().add("set_lt", &p_set_lt);
1761  registry().add("equal", &p_set_eq);
1762  registry().add("set_ne", &p_set_ne);
1763  registry().add("set_union", &p_set_union);
1764  registry().add("array_set_element", &p_array_set_element);
1765  registry().add("array_var_set_element", &p_array_set_element);
1766  registry().add("set_intersect", &p_set_intersect);
1767  registry().add("set_diff", &p_set_diff);
1768  registry().add("set_symdiff", &p_set_symdiff);
1769  registry().add("set_subset", &p_set_subset);
1770  registry().add("set_superset", &p_set_superset);
1771  registry().add("set_card", &p_set_card);
1772  registry().add("set_in", &p_set_in);
1773  registry().add("set_eq_reif", &p_set_eq_reif);
1774  registry().add("set_le_reif", &p_set_le_reif);
1775  registry().add("set_lt_reif", &p_set_lt_reif);
1776  registry().add("equal_reif", &p_set_eq_reif);
1777  registry().add("set_ne_reif", &p_set_ne_reif);
1778  registry().add("set_subset_reif", &p_set_subset_reif);
1779  registry().add("set_superset_reif", &p_set_superset_reif);
1780  registry().add("set_in_reif", &p_set_in_reif);
1781  registry().add("disjoint", &p_set_disjoint);
1782  registry().add("gecode_link_set_to_booleans",
1783  &p_link_set_to_booleans);
1784 
1785  registry().add("array_set_union", &p_array_set_union);
1786  registry().add("array_set_partition", &p_array_set_partition);
1787  registry().add("set_convex", &p_set_convex);
1788  registry().add("array_set_seq", &p_array_set_seq);
1789  registry().add("array_set_seq_union", &p_array_set_seq_union);
1790  registry().add("gecode_array_set_element_union",
1791  &p_array_set_element_union);
1792  registry().add("gecode_array_set_element_intersect",
1793  &p_array_set_element_intersect);
1794  registry().add("gecode_array_set_element_intersect_in",
1795  &p_array_set_element_intersect_in);
1796  registry().add("gecode_array_set_element_partition",
1797  &p_array_set_element_partition);
1798  registry().add("gecode_int_set_channel",
1799  &p_int_set_channel);
1800  registry().add("gecode_range",
1801  &p_range);
1802  registry().add("gecode_set_weights",
1803  &p_weights);
1804  }
1805  };
1806  SetPoster __set_poster;
1807 #endif
1808 
1809  }
1810 }}
1811 
1812 // STATISTICS: flatzinc-any