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