Generated on Sat Feb 7 2015 02:01:13 for Gecode by doxygen 1.8.9.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: 2015-01-19 00:23:36 +0100 (Mon, 19 Jan 2015) $ by $Author: tack $
15  * $Revision: 14367 $
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, 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  unshare(s, va);
111  distinct(s, va, icl == ICL_DEF ? ICL_BND : icl);
112  }
113  void p_distinctOffset(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
114  IntVarArgs va = s.arg2intvarargs(ce[1]);
115  unshare(s, va);
116  AST::Array* offs = ce.args->a[0]->getArray();
117  IntArgs oa(offs->a.size());
118  for (int i=offs->a.size(); i--; ) {
119  oa[i] = offs->a[i]->getInt();
120  }
121  IntConLevel icl = s.ann2icl(ann);
122  distinct(s, oa, va, icl == ICL_DEF ? ICL_BND : icl);
123  }
124 
125  void p_all_equal(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
126  IntVarArgs va = s.arg2intvarargs(ce[0]);
127  rel(s, va, IRT_EQ, s.ann2icl(ann));
128  }
129 
130  void p_int_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
131  AST::Node* ann) {
132  if (ce[0]->isIntVar()) {
133  if (ce[1]->isIntVar()) {
134  rel(s, s.arg2IntVar(ce[0]), irt, s.arg2IntVar(ce[1]),
135  s.ann2icl(ann));
136  } else {
137  rel(s, s.arg2IntVar(ce[0]), irt, ce[1]->getInt(), s.ann2icl(ann));
138  }
139  } else {
140  rel(s, s.arg2IntVar(ce[1]), swap(irt), ce[0]->getInt(),
141  s.ann2icl(ann));
142  }
143  }
144  void p_int_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
145  p_int_CMP(s, IRT_EQ, ce, ann);
146  }
147  void p_int_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
148  p_int_CMP(s, IRT_NQ, ce, ann);
149  }
150  void p_int_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
151  p_int_CMP(s, IRT_GQ, ce, ann);
152  }
153  void p_int_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
154  p_int_CMP(s, IRT_GR, ce, ann);
155  }
156  void p_int_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
157  p_int_CMP(s, IRT_LQ, ce, ann);
158  }
159  void p_int_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
160  p_int_CMP(s, IRT_LE, ce, ann);
161  }
162  void p_int_CMP_reif(FlatZincSpace& s, IntRelType irt, ReifyMode rm,
163  const ConExpr& ce, AST::Node* ann) {
164  if (rm == RM_EQV && ce[2]->isBool()) {
165  if (ce[2]->getBool()) {
166  p_int_CMP(s, irt, ce, ann);
167  } else {
168  p_int_CMP(s, neg(irt), ce, ann);
169  }
170  return;
171  }
172  if (ce[0]->isIntVar()) {
173  if (ce[1]->isIntVar()) {
174  rel(s, s.arg2IntVar(ce[0]), irt, s.arg2IntVar(ce[1]),
175  Reify(s.arg2BoolVar(ce[2]), rm), s.ann2icl(ann));
176  } else {
177  rel(s, s.arg2IntVar(ce[0]), irt, ce[1]->getInt(),
178  Reify(s.arg2BoolVar(ce[2]), rm), s.ann2icl(ann));
179  }
180  } else {
181  rel(s, s.arg2IntVar(ce[1]), swap(irt), ce[0]->getInt(),
182  Reify(s.arg2BoolVar(ce[2]), rm), s.ann2icl(ann));
183  }
184  }
185 
186  /* Comparisons */
187  void p_int_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
188  p_int_CMP_reif(s, IRT_EQ, RM_EQV, ce, ann);
189  }
190  void p_int_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
191  p_int_CMP_reif(s, IRT_NQ, RM_EQV, ce, ann);
192  }
193  void p_int_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
194  p_int_CMP_reif(s, IRT_GQ, RM_EQV, ce, ann);
195  }
196  void p_int_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
197  p_int_CMP_reif(s, IRT_GR, RM_EQV, ce, ann);
198  }
199  void p_int_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
200  p_int_CMP_reif(s, IRT_LQ, RM_EQV, ce, ann);
201  }
202  void p_int_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
203  p_int_CMP_reif(s, IRT_LE, RM_EQV, ce, ann);
204  }
205 
206  void p_int_eq_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
207  p_int_CMP_reif(s, IRT_EQ, RM_IMP, ce, ann);
208  }
209  void p_int_ne_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
210  p_int_CMP_reif(s, IRT_NQ, RM_IMP, ce, ann);
211  }
212  void p_int_ge_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
213  p_int_CMP_reif(s, IRT_GQ, RM_IMP, ce, ann);
214  }
215  void p_int_gt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
216  p_int_CMP_reif(s, IRT_GR, RM_IMP, ce, ann);
217  }
218  void p_int_le_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
219  p_int_CMP_reif(s, IRT_LQ, RM_IMP, ce, ann);
220  }
221  void p_int_lt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
222  p_int_CMP_reif(s, IRT_LE, RM_IMP, ce, ann);
223  }
224 
225  /* linear (in-)equations */
226  void p_int_lin_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
227  AST::Node* ann) {
228  IntArgs ia = s.arg2intargs(ce[0]);
229  int singleIntVar;
230  if (s.isBoolArray(ce[1],singleIntVar)) {
231  if (singleIntVar != -1) {
232  if (std::abs(ia[singleIntVar]) == 1 && ce[2]->getInt() == 0) {
233  IntVar siv = s.arg2IntVar(ce[1]->getArray()->a[singleIntVar]);
234  BoolVarArgs iv = s.arg2boolvarargs(ce[1], 0, singleIntVar);
235  IntArgs ia_tmp(ia.size()-1);
236  int count = 0;
237  for (int i=0; i<ia.size(); i++) {
238  if (i != singleIntVar)
239  ia_tmp[count++] = ia[singleIntVar] == -1 ? ia[i] : -ia[i];
240  }
241  IntRelType t = (ia[singleIntVar] == -1 ? irt : swap(irt));
242  linear(s, ia_tmp, iv, t, siv, s.ann2icl(ann));
243  } else {
244  IntVarArgs iv = s.arg2intvarargs(ce[1]);
245  linear(s, ia, iv, irt, ce[2]->getInt(), s.ann2icl(ann));
246  }
247  } else {
248  BoolVarArgs iv = s.arg2boolvarargs(ce[1]);
249  linear(s, ia, iv, irt, ce[2]->getInt(), s.ann2icl(ann));
250  }
251  } else {
252  IntVarArgs iv = s.arg2intvarargs(ce[1]);
253  linear(s, ia, iv, irt, ce[2]->getInt(), s.ann2icl(ann));
254  }
255  }
256  void p_int_lin_CMP_reif(FlatZincSpace& s, IntRelType irt, ReifyMode rm,
257  const ConExpr& ce, AST::Node* ann) {
258  if (rm == RM_EQV && ce[2]->isBool()) {
259  if (ce[2]->getBool()) {
260  p_int_lin_CMP(s, irt, ce, ann);
261  } else {
262  p_int_lin_CMP(s, neg(irt), ce, ann);
263  }
264  return;
265  }
266  IntArgs ia = s.arg2intargs(ce[0]);
267  int singleIntVar;
268  if (s.isBoolArray(ce[1],singleIntVar)) {
269  if (singleIntVar != -1) {
270  if (std::abs(ia[singleIntVar]) == 1 && ce[2]->getInt() == 0) {
271  IntVar siv = s.arg2IntVar(ce[1]->getArray()->a[singleIntVar]);
272  BoolVarArgs iv = s.arg2boolvarargs(ce[1], 0, singleIntVar);
273  IntArgs ia_tmp(ia.size()-1);
274  int count = 0;
275  for (int i=0; i<ia.size(); i++) {
276  if (i != singleIntVar)
277  ia_tmp[count++] = ia[singleIntVar] == -1 ? ia[i] : -ia[i];
278  }
279  IntRelType t = (ia[singleIntVar] == -1 ? irt : swap(irt));
280  linear(s, ia_tmp, iv, t, siv, Reify(s.arg2BoolVar(ce[3]), rm),
281  s.ann2icl(ann));
282  } else {
283  IntVarArgs iv = s.arg2intvarargs(ce[1]);
284  linear(s, ia, iv, irt, ce[2]->getInt(),
285  Reify(s.arg2BoolVar(ce[3]), rm), s.ann2icl(ann));
286  }
287  } else {
288  BoolVarArgs iv = s.arg2boolvarargs(ce[1]);
289  linear(s, ia, iv, irt, ce[2]->getInt(),
290  Reify(s.arg2BoolVar(ce[3]), rm), s.ann2icl(ann));
291  }
292  } else {
293  IntVarArgs iv = s.arg2intvarargs(ce[1]);
294  linear(s, ia, iv, irt, ce[2]->getInt(),
295  Reify(s.arg2BoolVar(ce[3]), rm),
296  s.ann2icl(ann));
297  }
298  }
299  void p_int_lin_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
300  p_int_lin_CMP(s, IRT_EQ, ce, ann);
301  }
302  void p_int_lin_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
303  p_int_lin_CMP_reif(s, IRT_EQ, RM_EQV, ce, ann);
304  }
305  void p_int_lin_eq_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
306  p_int_lin_CMP_reif(s, IRT_EQ, RM_IMP, ce, ann);
307  }
308  void p_int_lin_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
309  p_int_lin_CMP(s, IRT_NQ, ce, ann);
310  }
311  void p_int_lin_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
312  p_int_lin_CMP_reif(s, IRT_NQ, RM_EQV, ce, ann);
313  }
314  void p_int_lin_ne_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
315  p_int_lin_CMP_reif(s, IRT_NQ, RM_IMP, ce, ann);
316  }
317  void p_int_lin_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
318  p_int_lin_CMP(s, IRT_LQ, ce, ann);
319  }
320  void p_int_lin_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
321  p_int_lin_CMP_reif(s, IRT_LQ, RM_EQV, ce, ann);
322  }
323  void p_int_lin_le_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
324  p_int_lin_CMP_reif(s, IRT_LQ, RM_IMP, ce, ann);
325  }
326  void p_int_lin_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
327  p_int_lin_CMP(s, IRT_LE, ce, ann);
328  }
329  void p_int_lin_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
330  p_int_lin_CMP_reif(s, IRT_LE, RM_EQV, ce, ann);
331  }
332  void p_int_lin_lt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
333  p_int_lin_CMP_reif(s, IRT_LE, RM_IMP, ce, ann);
334  }
335  void p_int_lin_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
336  p_int_lin_CMP(s, IRT_GQ, ce, ann);
337  }
338  void p_int_lin_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
339  p_int_lin_CMP_reif(s, IRT_GQ, RM_EQV, ce, ann);
340  }
341  void p_int_lin_ge_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
342  p_int_lin_CMP_reif(s, IRT_GQ, RM_IMP, ce, ann);
343  }
344  void p_int_lin_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
345  p_int_lin_CMP(s, IRT_GR, ce, ann);
346  }
347  void p_int_lin_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
348  p_int_lin_CMP_reif(s, IRT_GR, RM_EQV, ce, ann);
349  }
350  void p_int_lin_gt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
351  p_int_lin_CMP_reif(s, IRT_GR, RM_IMP, ce, ann);
352  }
353 
354  void p_bool_lin_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
355  AST::Node* ann) {
356  IntArgs ia = s.arg2intargs(ce[0]);
357  BoolVarArgs iv = s.arg2boolvarargs(ce[1]);
358  if (ce[2]->isIntVar())
359  linear(s, ia, iv, irt, s.iv[ce[2]->getIntVar()], s.ann2icl(ann));
360  else
361  linear(s, ia, iv, irt, ce[2]->getInt(), s.ann2icl(ann));
362  }
363  void p_bool_lin_CMP_reif(FlatZincSpace& s, IntRelType irt, ReifyMode rm,
364  const ConExpr& ce, AST::Node* ann) {
365  if (rm == RM_EQV && ce[2]->isBool()) {
366  if (ce[2]->getBool()) {
367  p_bool_lin_CMP(s, irt, ce, ann);
368  } else {
369  p_bool_lin_CMP(s, neg(irt), ce, ann);
370  }
371  return;
372  }
373  IntArgs ia = s.arg2intargs(ce[0]);
374  BoolVarArgs iv = s.arg2boolvarargs(ce[1]);
375  if (ce[2]->isIntVar())
376  linear(s, ia, iv, irt, s.iv[ce[2]->getIntVar()],
377  Reify(s.arg2BoolVar(ce[3]), rm),
378  s.ann2icl(ann));
379  else
380  linear(s, ia, iv, irt, ce[2]->getInt(),
381  Reify(s.arg2BoolVar(ce[3]), rm),
382  s.ann2icl(ann));
383  }
384  void p_bool_lin_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
385  p_bool_lin_CMP(s, IRT_EQ, ce, ann);
386  }
387  void p_bool_lin_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
388  {
389  p_bool_lin_CMP_reif(s, IRT_EQ, RM_EQV, ce, ann);
390  }
391  void p_bool_lin_eq_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
392  {
393  p_bool_lin_CMP_reif(s, IRT_EQ, RM_IMP, ce, ann);
394  }
395  void p_bool_lin_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
396  p_bool_lin_CMP(s, IRT_NQ, ce, ann);
397  }
398  void p_bool_lin_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
399  {
400  p_bool_lin_CMP_reif(s, IRT_NQ, RM_EQV, ce, ann);
401  }
402  void p_bool_lin_ne_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
403  {
404  p_bool_lin_CMP_reif(s, IRT_NQ, RM_IMP, ce, ann);
405  }
406  void p_bool_lin_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
407  p_bool_lin_CMP(s, IRT_LQ, ce, ann);
408  }
409  void p_bool_lin_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
410  {
411  p_bool_lin_CMP_reif(s, IRT_LQ, RM_EQV, ce, ann);
412  }
413  void p_bool_lin_le_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
414  {
415  p_bool_lin_CMP_reif(s, IRT_LQ, RM_IMP, ce, ann);
416  }
417  void p_bool_lin_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
418  {
419  p_bool_lin_CMP(s, IRT_LE, ce, ann);
420  }
421  void p_bool_lin_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
422  {
423  p_bool_lin_CMP_reif(s, IRT_LE, RM_EQV, ce, ann);
424  }
425  void p_bool_lin_lt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
426  {
427  p_bool_lin_CMP_reif(s, IRT_LE, RM_IMP, ce, ann);
428  }
429  void p_bool_lin_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
430  p_bool_lin_CMP(s, IRT_GQ, ce, ann);
431  }
432  void p_bool_lin_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
433  {
434  p_bool_lin_CMP_reif(s, IRT_GQ, RM_EQV, ce, ann);
435  }
436  void p_bool_lin_ge_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
437  {
438  p_bool_lin_CMP_reif(s, IRT_GQ, RM_IMP, ce, ann);
439  }
440  void p_bool_lin_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
441  p_bool_lin_CMP(s, IRT_GR, ce, ann);
442  }
443  void p_bool_lin_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
444  {
445  p_bool_lin_CMP_reif(s, IRT_GR, RM_EQV, ce, ann);
446  }
447  void p_bool_lin_gt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
448  {
449  p_bool_lin_CMP_reif(s, IRT_GR, RM_IMP, ce, ann);
450  }
451 
452  /* arithmetic constraints */
453 
454  void p_int_plus(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
455  if (!ce[0]->isIntVar()) {
456  rel(s, ce[0]->getInt() + s.arg2IntVar(ce[1])
457  == s.arg2IntVar(ce[2]), s.ann2icl(ann));
458  } else if (!ce[1]->isIntVar()) {
459  rel(s, s.arg2IntVar(ce[0]) + ce[1]->getInt()
460  == s.arg2IntVar(ce[2]), s.ann2icl(ann));
461  } else if (!ce[2]->isIntVar()) {
462  rel(s, s.arg2IntVar(ce[0]) + s.arg2IntVar(ce[1])
463  == ce[2]->getInt(), s.ann2icl(ann));
464  } else {
465  rel(s, s.arg2IntVar(ce[0]) + s.arg2IntVar(ce[1])
466  == s.arg2IntVar(ce[2]), s.ann2icl(ann));
467  }
468  }
469 
470  void p_int_minus(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
471  if (!ce[0]->isIntVar()) {
472  rel(s, ce[0]->getInt() - s.arg2IntVar(ce[1])
473  == s.arg2IntVar(ce[2]), s.ann2icl(ann));
474  } else if (!ce[1]->isIntVar()) {
475  rel(s, s.arg2IntVar(ce[0]) - ce[1]->getInt()
476  == s.arg2IntVar(ce[2]), s.ann2icl(ann));
477  } else if (!ce[2]->isIntVar()) {
478  rel(s, s.arg2IntVar(ce[0]) - s.arg2IntVar(ce[1])
479  == ce[2]->getInt(), s.ann2icl(ann));
480  } else {
481  rel(s, s.arg2IntVar(ce[0]) - s.arg2IntVar(ce[1])
482  == s.arg2IntVar(ce[2]), s.ann2icl(ann));
483  }
484  }
485 
486  void p_int_times(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
487  IntVar x0 = s.arg2IntVar(ce[0]);
488  IntVar x1 = s.arg2IntVar(ce[1]);
489  IntVar x2 = s.arg2IntVar(ce[2]);
490  mult(s, x0, x1, x2, s.ann2icl(ann));
491  }
492  void p_int_div(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
493  IntVar x0 = s.arg2IntVar(ce[0]);
494  IntVar x1 = s.arg2IntVar(ce[1]);
495  IntVar x2 = s.arg2IntVar(ce[2]);
496  div(s,x0,x1,x2, s.ann2icl(ann));
497  }
498  void p_int_mod(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
499  IntVar x0 = s.arg2IntVar(ce[0]);
500  IntVar x1 = s.arg2IntVar(ce[1]);
501  IntVar x2 = s.arg2IntVar(ce[2]);
502  mod(s,x0,x1,x2, s.ann2icl(ann));
503  }
504 
505  void p_int_min(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
506  IntVar x0 = s.arg2IntVar(ce[0]);
507  IntVar x1 = s.arg2IntVar(ce[1]);
508  IntVar x2 = s.arg2IntVar(ce[2]);
509  min(s, x0, x1, x2, s.ann2icl(ann));
510  }
511  void p_int_max(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
512  IntVar x0 = s.arg2IntVar(ce[0]);
513  IntVar x1 = s.arg2IntVar(ce[1]);
514  IntVar x2 = s.arg2IntVar(ce[2]);
515  max(s, x0, x1, x2, s.ann2icl(ann));
516  }
517  void p_int_negate(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
518  IntVar x0 = s.arg2IntVar(ce[0]);
519  IntVar x1 = s.arg2IntVar(ce[1]);
520  rel(s, x0 == -x1, s.ann2icl(ann));
521  }
522 
523  /* Boolean constraints */
524  void p_bool_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
525  AST::Node* ann) {
526  rel(s, s.arg2BoolVar(ce[0]), irt, s.arg2BoolVar(ce[1]),
527  s.ann2icl(ann));
528  }
529  void p_bool_CMP_reif(FlatZincSpace& s, IntRelType irt, ReifyMode rm,
530  const ConExpr& ce, AST::Node* ann) {
531  rel(s, s.arg2BoolVar(ce[0]), irt, s.arg2BoolVar(ce[1]),
532  Reify(s.arg2BoolVar(ce[2]), rm), s.ann2icl(ann));
533  }
534  void p_bool_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
535  p_bool_CMP(s, IRT_EQ, ce, ann);
536  }
537  void p_bool_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
538  p_bool_CMP_reif(s, IRT_EQ, RM_EQV, ce, ann);
539  }
540  void p_bool_eq_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
541  p_bool_CMP_reif(s, IRT_EQ, RM_IMP, ce, ann);
542  }
543  void p_bool_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
544  p_bool_CMP(s, IRT_NQ, ce, ann);
545  }
546  void p_bool_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
547  p_bool_CMP_reif(s, IRT_NQ, RM_EQV, ce, ann);
548  }
549  void p_bool_ne_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
550  p_bool_CMP_reif(s, IRT_NQ, RM_IMP, ce, ann);
551  }
552  void p_bool_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
553  p_bool_CMP(s, IRT_GQ, ce, ann);
554  }
555  void p_bool_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
556  p_bool_CMP_reif(s, IRT_GQ, RM_EQV, ce, ann);
557  }
558  void p_bool_ge_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
559  p_bool_CMP_reif(s, IRT_GQ, RM_IMP, ce, ann);
560  }
561  void p_bool_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
562  p_bool_CMP(s, IRT_LQ, ce, ann);
563  }
564  void p_bool_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
565  p_bool_CMP_reif(s, IRT_LQ, RM_EQV, ce, ann);
566  }
567  void p_bool_le_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
568  p_bool_CMP_reif(s, IRT_LQ, RM_IMP, ce, ann);
569  }
570  void p_bool_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
571  p_bool_CMP(s, IRT_GR, ce, ann);
572  }
573  void p_bool_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
574  p_bool_CMP_reif(s, IRT_GR, RM_EQV, ce, ann);
575  }
576  void p_bool_gt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
577  p_bool_CMP_reif(s, IRT_GR, RM_IMP, ce, ann);
578  }
579  void p_bool_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
580  p_bool_CMP(s, IRT_LE, ce, ann);
581  }
582  void p_bool_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
583  p_bool_CMP_reif(s, IRT_LE, RM_EQV, ce, ann);
584  }
585  void p_bool_lt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
586  p_bool_CMP_reif(s, IRT_LE, RM_IMP, ce, ann);
587  }
588 
589 #define BOOL_OP(op) \
590  BoolVar b0 = s.arg2BoolVar(ce[0]); \
591  BoolVar b1 = s.arg2BoolVar(ce[1]); \
592  if (ce[2]->isBool()) { \
593  rel(s, b0, op, b1, ce[2]->getBool(), s.ann2icl(ann)); \
594  } else { \
595  rel(s, b0, op, b1, s.bv[ce[2]->getBoolVar()], s.ann2icl(ann)); \
596  }
597 
598 #define BOOL_ARRAY_OP(op) \
599  BoolVarArgs bv = s.arg2boolvarargs(ce[0]); \
600  if (ce.size()==1) { \
601  rel(s, op, bv, 1, s.ann2icl(ann)); \
602  } else if (ce[1]->isBool()) { \
603  rel(s, op, bv, ce[1]->getBool(), s.ann2icl(ann)); \
604  } else { \
605  rel(s, op, bv, s.bv[ce[1]->getBoolVar()], s.ann2icl(ann)); \
606  }
607 
608  void p_bool_or(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
609  BOOL_OP(BOT_OR);
610  }
611  void p_bool_or_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
612  BoolVar b0 = s.arg2BoolVar(ce[0]);
613  BoolVar b1 = s.arg2BoolVar(ce[1]);
614  BoolVar b2 = s.arg2BoolVar(ce[2]);
615  clause(s, BOT_OR, BoolVarArgs()<<b0<<b1, BoolVarArgs()<<b2, 1,
616  s.ann2icl(ann));
617  }
618  void p_bool_and(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
619  BOOL_OP(BOT_AND);
620  }
621  void p_bool_and_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
622  BoolVar b0 = s.arg2BoolVar(ce[0]);
623  BoolVar b1 = s.arg2BoolVar(ce[1]);
624  BoolVar b2 = s.arg2BoolVar(ce[2]);
625  rel(s, b2, BOT_IMP, b0, 1, s.ann2icl(ann));
626  rel(s, b2, BOT_IMP, b1, 1, s.ann2icl(ann));
627  }
628  void p_array_bool_and(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
629  {
631  }
632  void p_array_bool_and_imp(FlatZincSpace& s, const ConExpr& ce,
633  AST::Node* ann)
634  {
635  BoolVarArgs bv = s.arg2boolvarargs(ce[0]);
636  BoolVar b1 = s.arg2BoolVar(ce[1]);
637  for (unsigned int i=bv.size(); i--;)
638  rel(s, b1, BOT_IMP, bv[i], 1, s.ann2icl(ann));
639  }
640  void p_array_bool_or(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
641  {
643  }
644  void p_array_bool_or_imp(FlatZincSpace& s, const ConExpr& ce,
645  AST::Node* ann)
646  {
647  BoolVarArgs bv = s.arg2boolvarargs(ce[0]);
648  BoolVar b1 = s.arg2BoolVar(ce[1]);
649  clause(s, BOT_OR, bv, BoolVarArgs()<<b1, 1, s.ann2icl(ann));
650  }
651  void p_array_bool_xor(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
652  {
654  }
655  void p_array_bool_xor_imp(FlatZincSpace& s, const ConExpr& ce,
656  AST::Node* ann)
657  {
658  BoolVarArgs bv = s.arg2boolvarargs(ce[0]);
659  BoolVar tmp(s,0,1);
660  rel(s, BOT_XOR, bv, tmp, s.ann2icl(ann));
661  rel(s, s.arg2BoolVar(ce[1]), BOT_IMP, tmp, 1);
662  }
663  void p_array_bool_clause(FlatZincSpace& s, const ConExpr& ce,
664  AST::Node* ann) {
665  BoolVarArgs bvp = s.arg2boolvarargs(ce[0]);
666  BoolVarArgs bvn = s.arg2boolvarargs(ce[1]);
667  clause(s, BOT_OR, bvp, bvn, 1, s.ann2icl(ann));
668  }
669  void p_array_bool_clause_reif(FlatZincSpace& s, const ConExpr& ce,
670  AST::Node* ann) {
671  BoolVarArgs bvp = s.arg2boolvarargs(ce[0]);
672  BoolVarArgs bvn = s.arg2boolvarargs(ce[1]);
673  BoolVar b0 = s.arg2BoolVar(ce[2]);
674  clause(s, BOT_OR, bvp, bvn, b0, s.ann2icl(ann));
675  }
676  void p_array_bool_clause_imp(FlatZincSpace& s, const ConExpr& ce,
677  AST::Node* ann) {
678  BoolVarArgs bvp = s.arg2boolvarargs(ce[0]);
679  BoolVarArgs bvn = s.arg2boolvarargs(ce[1]);
680  BoolVar b0 = s.arg2BoolVar(ce[2]);
681  clause(s, BOT_OR, bvp, bvn, b0, s.ann2icl(ann));
682  }
683  void p_bool_xor(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
684  BOOL_OP(BOT_XOR);
685  }
686  void p_bool_xor_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
687  BoolVar b0 = s.arg2BoolVar(ce[0]);
688  BoolVar b1 = s.arg2BoolVar(ce[1]);
689  BoolVar b2 = s.arg2BoolVar(ce[2]);
690  clause(s, BOT_OR, BoolVarArgs()<<b0<<b1, BoolVarArgs()<<b2, 1,
691  s.ann2icl(ann));
692  clause(s, BOT_OR, BoolVarArgs(), BoolVarArgs()<<b0<<b1<<b2, 1,
693  s.ann2icl(ann));
694  }
695  void p_bool_l_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
696  BoolVar b0 = s.arg2BoolVar(ce[0]);
697  BoolVar b1 = s.arg2BoolVar(ce[1]);
698  if (ce[2]->isBool()) {
699  rel(s, b1, BOT_IMP, b0, ce[2]->getBool(), s.ann2icl(ann));
700  } else {
701  rel(s, b1, BOT_IMP, b0, s.bv[ce[2]->getBoolVar()], s.ann2icl(ann));
702  }
703  }
704  void p_bool_r_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
705  BOOL_OP(BOT_IMP);
706  }
707  void p_bool_not(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
708  BoolVar x0 = s.arg2BoolVar(ce[0]);
709  BoolVar x1 = s.arg2BoolVar(ce[1]);
710  rel(s, x0, BOT_XOR, x1, 1, s.ann2icl(ann));
711  }
712 
713  /* element constraints */
714  void p_array_int_element(FlatZincSpace& s, const ConExpr& ce,
715  AST::Node* ann) {
716  bool isConstant = true;
717  AST::Array* a = ce[1]->getArray();
718  for (int i=a->a.size(); i--;) {
719  if (!a->a[i]->isInt()) {
720  isConstant = false;
721  break;
722  }
723  }
724  IntVar selector = s.arg2IntVar(ce[0]);
725  rel(s, selector > 0);
726  if (isConstant) {
727  IntArgs ia = s.arg2intargs(ce[1], 1);
728  element(s, ia, selector, s.arg2IntVar(ce[2]), s.ann2icl(ann));
729  } else {
730  IntVarArgs iv = s.arg2intvarargs(ce[1], 1);
731  element(s, iv, selector, s.arg2IntVar(ce[2]), s.ann2icl(ann));
732  }
733  }
734  void p_array_bool_element(FlatZincSpace& s, const ConExpr& ce,
735  AST::Node* ann) {
736  bool isConstant = true;
737  AST::Array* a = ce[1]->getArray();
738  for (int i=a->a.size(); i--;) {
739  if (!a->a[i]->isBool()) {
740  isConstant = false;
741  break;
742  }
743  }
744  IntVar selector = s.arg2IntVar(ce[0]);
745  rel(s, selector > 0);
746  if (isConstant) {
747  IntArgs ia = s.arg2boolargs(ce[1], 1);
748  element(s, ia, selector, s.arg2BoolVar(ce[2]), s.ann2icl(ann));
749  } else {
750  BoolVarArgs iv = s.arg2boolvarargs(ce[1], 1);
751  element(s, iv, selector, s.arg2BoolVar(ce[2]), s.ann2icl(ann));
752  }
753  }
754 
755  /* coercion constraints */
756  void p_bool2int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
757  BoolVar x0 = s.arg2BoolVar(ce[0]);
758  IntVar x1 = s.arg2IntVar(ce[1]);
759  if (ce[0]->isBoolVar() && ce[1]->isIntVar()) {
760  s.aliasBool2Int(ce[1]->getIntVar(), ce[0]->getBoolVar());
761  }
762  channel(s, x0, x1, s.ann2icl(ann));
763  }
764 
765  void p_int_in(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
766  IntSet d = s.arg2intset(ce[1]);
767  if (ce[0]->isBoolVar()) {
768  IntSetRanges dr(d);
769  Iter::Ranges::Singleton sr(0,1);
770  Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr);
771  IntSet d01(i);
772  if (d01.size() == 0) {
773  s.fail();
774  } else {
775  rel(s, s.arg2BoolVar(ce[0]), IRT_GQ, d01.min());
776  rel(s, s.arg2BoolVar(ce[0]), IRT_LQ, d01.max());
777  }
778  } else {
779  dom(s, s.arg2IntVar(ce[0]), d);
780  }
781  }
782  void p_int_in_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
783  IntSet d = s.arg2intset(ce[1]);
784  if (ce[0]->isBoolVar()) {
785  IntSetRanges dr(d);
786  Iter::Ranges::Singleton sr(0,1);
787  Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr);
788  IntSet d01(i);
789  if (d01.size() == 0) {
790  rel(s, s.arg2BoolVar(ce[2]) == 0);
791  } else if (d01.max() == 0) {
792  rel(s, s.arg2BoolVar(ce[2]) == !s.arg2BoolVar(ce[0]));
793  } else if (d01.min() == 1) {
794  rel(s, s.arg2BoolVar(ce[2]) == s.arg2BoolVar(ce[0]));
795  } else {
796  rel(s, s.arg2BoolVar(ce[2]) == 1);
797  }
798  } else {
799  dom(s, s.arg2IntVar(ce[0]), d, s.arg2BoolVar(ce[2]));
800  }
801  }
802  void p_int_in_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
803  IntSet d = s.arg2intset(ce[1]);
804  if (ce[0]->isBoolVar()) {
805  IntSetRanges dr(d);
806  Iter::Ranges::Singleton sr(0,1);
807  Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr);
808  IntSet d01(i);
809  if (d01.size() == 0) {
810  rel(s, s.arg2BoolVar(ce[2]) == 0);
811  } else if (d01.max() == 0) {
812  rel(s, s.arg2BoolVar(ce[2]) >> !s.arg2BoolVar(ce[0]));
813  } else if (d01.min() == 1) {
814  rel(s, s.arg2BoolVar(ce[2]) >> s.arg2BoolVar(ce[0]));
815  }
816  } else {
817  dom(s, s.arg2IntVar(ce[0]), d, Reify(s.arg2BoolVar(ce[2]),RM_IMP));
818  }
819  }
820 
821  /* constraints from the standard library */
822 
823  void p_abs(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
824  IntVar x0 = s.arg2IntVar(ce[0]);
825  IntVar x1 = s.arg2IntVar(ce[1]);
826  abs(s, x0, x1, s.ann2icl(ann));
827  }
828 
829  void p_array_int_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
830  IntVarArgs iv0 = s.arg2intvarargs(ce[0]);
831  IntVarArgs iv1 = s.arg2intvarargs(ce[1]);
832  rel(s, iv0, IRT_LE, iv1, s.ann2icl(ann));
833  }
834 
835  void p_array_int_lq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
836  IntVarArgs iv0 = s.arg2intvarargs(ce[0]);
837  IntVarArgs iv1 = s.arg2intvarargs(ce[1]);
838  rel(s, iv0, IRT_LQ, iv1, s.ann2icl(ann));
839  }
840 
841  void p_array_bool_lt(FlatZincSpace& s, const ConExpr& ce,
842  AST::Node* ann) {
843  BoolVarArgs bv0 = s.arg2boolvarargs(ce[0]);
844  BoolVarArgs bv1 = s.arg2boolvarargs(ce[1]);
845  rel(s, bv0, IRT_LE, bv1, s.ann2icl(ann));
846  }
847 
848  void p_array_bool_lq(FlatZincSpace& s, const ConExpr& ce,
849  AST::Node* ann) {
850  BoolVarArgs bv0 = s.arg2boolvarargs(ce[0]);
851  BoolVarArgs bv1 = s.arg2boolvarargs(ce[1]);
852  rel(s, bv0, IRT_LQ, bv1, s.ann2icl(ann));
853  }
854 
855  void p_count(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
856  IntVarArgs iv = s.arg2intvarargs(ce[0]);
857  if (!ce[1]->isIntVar()) {
858  if (!ce[2]->isIntVar()) {
859  count(s, iv, ce[1]->getInt(), IRT_EQ, ce[2]->getInt(),
860  s.ann2icl(ann));
861  } else {
862  count(s, iv, ce[1]->getInt(), IRT_EQ, s.arg2IntVar(ce[2]),
863  s.ann2icl(ann));
864  }
865  } else if (!ce[2]->isIntVar()) {
866  count(s, iv, s.arg2IntVar(ce[1]), IRT_EQ, ce[2]->getInt(),
867  s.ann2icl(ann));
868  } else {
869  count(s, iv, s.arg2IntVar(ce[1]), IRT_EQ, s.arg2IntVar(ce[2]),
870  s.ann2icl(ann));
871  }
872  }
873 
874  void p_count_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
875  IntVarArgs iv = s.arg2intvarargs(ce[0]);
876  IntVar x = s.arg2IntVar(ce[1]);
877  IntVar y = s.arg2IntVar(ce[2]);
878  BoolVar b = s.arg2BoolVar(ce[3]);
879  IntVar c(s,0,Int::Limits::max);
880  count(s,iv,x,IRT_EQ,c,s.ann2icl(ann));
881  rel(s, b == (c==y));
882  }
883  void p_count_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
884  IntVarArgs iv = s.arg2intvarargs(ce[0]);
885  IntVar x = s.arg2IntVar(ce[1]);
886  IntVar y = s.arg2IntVar(ce[2]);
887  BoolVar b = s.arg2BoolVar(ce[3]);
888  IntVar c(s,0,Int::Limits::max);
889  count(s,iv,x,IRT_EQ,c,s.ann2icl(ann));
890  rel(s, b >> (c==y));
891  }
892 
893  void count_rel(IntRelType irt,
894  FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
895  IntVarArgs iv = s.arg2intvarargs(ce[1]);
896  count(s, iv, ce[2]->getInt(), irt, ce[0]->getInt(), s.ann2icl(ann));
897  }
898 
899  void p_at_most(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
900  count_rel(IRT_LQ, s, ce, ann);
901  }
902 
903  void p_at_least(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
904  count_rel(IRT_GQ, s, ce, ann);
905  }
906 
907  void p_bin_packing_load(FlatZincSpace& s, const ConExpr& ce,
908  AST::Node* ann) {
909  int minIdx = ce[3]->getInt();
910  IntVarArgs load = s.arg2intvarargs(ce[0]);
911  IntVarArgs l;
912  IntVarArgs bin = s.arg2intvarargs(ce[1]);
913  for (int i=bin.size(); i--;)
914  rel(s, bin[i] >= minIdx);
915  if (minIdx > 0) {
916  for (int i=minIdx; i--;)
917  l << IntVar(s,0,0);
918  } else if (minIdx < 0) {
919  IntVarArgs bin2(bin.size());
920  for (int i=bin.size(); i--;)
921  bin2[i] = expr(s, bin[i]-minIdx, s.ann2icl(ann));
922  bin = bin2;
923  }
924  l << load;
925  IntArgs sizes = s.arg2intargs(ce[2]);
926 
927  IntVarArgs allvars = l + bin;
928  unshare(s, allvars);
929  binpacking(s, allvars.slice(0,1,l.size()), allvars.slice(l.size(),1,bin.size()),
930  sizes, s.ann2icl(ann));
931  }
932 
933  void p_global_cardinality(FlatZincSpace& s, const ConExpr& ce,
934  AST::Node* ann) {
935  IntVarArgs iv0 = s.arg2intvarargs(ce[0]);
936  IntArgs cover = s.arg2intargs(ce[1]);
937  IntVarArgs iv1 = s.arg2intvarargs(ce[2]);
938 
939  Region re(s);
940  IntSet cover_s(cover);
941  IntSetRanges cover_r(cover_s);
942  IntVarRanges* iv0_ri = re.alloc<IntVarRanges>(iv0.size());
943  for (int i=iv0.size(); i--;)
944  iv0_ri[i] = IntVarRanges(iv0[i]);
945  Iter::Ranges::NaryUnion iv0_r(re,iv0_ri,iv0.size());
946  Iter::Ranges::Diff<Iter::Ranges::NaryUnion,IntSetRanges>
947  extra_r(iv0_r,cover_r);
948  Iter::Ranges::ToValues<Iter::Ranges::Diff<
949  Iter::Ranges::NaryUnion,IntSetRanges> > extra(extra_r);
950  for (; extra(); ++extra) {
951  cover << extra.val();
952  iv1 << IntVar(s,0,iv0.size());
953  }
954  IntConLevel icl = s.ann2icl(ann);
955  if (icl==ICL_DOM) {
956  IntVarArgs allvars = iv0+iv1;
957  unshare(s, allvars);
958  count(s, allvars.slice(0,1,iv0.size()),
959  allvars.slice(iv0.size(),1,iv1.size()),
960  cover, s.ann2icl(ann));
961  } else {
962  unshare(s, iv0);
963  count(s, iv0, iv1, cover, s.ann2icl(ann));
964  }
965  }
966 
967  void p_global_cardinality_closed(FlatZincSpace& s, const ConExpr& ce,
968  AST::Node* ann) {
969  IntVarArgs iv0 = s.arg2intvarargs(ce[0]);
970  IntArgs cover = s.arg2intargs(ce[1]);
971  IntVarArgs iv1 = s.arg2intvarargs(ce[2]);
972  unshare(s, iv0);
973  count(s, iv0, iv1, cover, s.ann2icl(ann));
974  }
975 
976  void p_global_cardinality_low_up(FlatZincSpace& s, const ConExpr& ce,
977  AST::Node* ann) {
978  IntVarArgs x = s.arg2intvarargs(ce[0]);
979  IntArgs cover = s.arg2intargs(ce[1]);
980 
981  IntArgs lbound = s.arg2intargs(ce[2]);
982  IntArgs ubound = s.arg2intargs(ce[3]);
983  IntSetArgs y(cover.size());
984  for (int i=cover.size(); i--;)
985  y[i] = IntSet(lbound[i],ubound[i]);
986 
987  IntSet cover_s(cover);
988  Region re(s);
989  IntVarRanges* xrs = re.alloc<IntVarRanges>(x.size());
990  for (int i=x.size(); i--;)
991  xrs[i].init(x[i]);
992  Iter::Ranges::NaryUnion u(re, xrs, x.size());
993  Iter::Ranges::ToValues<Iter::Ranges::NaryUnion> uv(u);
994  for (; uv(); ++uv) {
995  if (!cover_s.in(uv.val())) {
996  cover << uv.val();
997  y << IntSet(0,x.size());
998  }
999  }
1000  unshare(s, x);
1001  count(s, x, y, cover, s.ann2icl(ann));
1002  }
1003 
1004  void p_global_cardinality_low_up_closed(FlatZincSpace& s,
1005  const ConExpr& ce,
1006  AST::Node* ann) {
1007  IntVarArgs x = s.arg2intvarargs(ce[0]);
1008  IntArgs cover = s.arg2intargs(ce[1]);
1009 
1010  IntArgs lbound = s.arg2intargs(ce[2]);
1011  IntArgs ubound = s.arg2intargs(ce[3]);
1012  IntSetArgs y(cover.size());
1013  for (int i=cover.size(); i--;)
1014  y[i] = IntSet(lbound[i],ubound[i]);
1015  unshare(s, x);
1016  count(s, x, y, cover, s.ann2icl(ann));
1017  }
1018 
1019  void p_minimum(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1020  IntVarArgs iv = s.arg2intvarargs(ce[1]);
1021  min(s, iv, s.arg2IntVar(ce[0]), s.ann2icl(ann));
1022  }
1023 
1024  void p_maximum(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1025  IntVarArgs iv = s.arg2intvarargs(ce[1]);
1026  max(s, iv, s.arg2IntVar(ce[0]), s.ann2icl(ann));
1027  }
1028 
1029  void p_minimum_arg(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1030  IntVarArgs iv = s.arg2intvarargs(ce[0]);
1031  argmin(s, iv, s.arg2IntVar(ce[1]), true, s.ann2icl(ann));
1032  }
1033 
1034  void p_maximum_arg(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1035  IntVarArgs iv = s.arg2intvarargs(ce[0]);
1036  argmax(s, iv, s.arg2IntVar(ce[1]), true, s.ann2icl(ann));
1037  }
1038 
1039  void p_regular(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1040  IntVarArgs iv = s.arg2intvarargs(ce[0]);
1041  int q = ce[1]->getInt();
1042  int symbols = ce[2]->getInt();
1043  IntArgs d = s.arg2intargs(ce[3]);
1044  int q0 = ce[4]->getInt();
1045 
1046  int noOfTrans = 0;
1047  for (int i=1; i<=q; i++) {
1048  for (int j=1; j<=symbols; j++) {
1049  if (d[(i-1)*symbols+(j-1)] > 0)
1050  noOfTrans++;
1051  }
1052  }
1053 
1054  Region re(s);
1055  DFA::Transition* t = re.alloc<DFA::Transition>(noOfTrans+1);
1056  noOfTrans = 0;
1057  for (int i=1; i<=q; i++) {
1058  for (int j=1; j<=symbols; j++) {
1059  if (d[(i-1)*symbols+(j-1)] > 0) {
1060  t[noOfTrans].i_state = i;
1061  t[noOfTrans].symbol = j;
1062  t[noOfTrans].o_state = d[(i-1)*symbols+(j-1)];
1063  noOfTrans++;
1064  }
1065  }
1066  }
1067  t[noOfTrans].i_state = -1;
1068 
1069  // Final states
1070  AST::SetLit* sl = ce[5]->getSet();
1071  int* f;
1072  if (sl->interval) {
1073  f = static_cast<int*>(malloc(sizeof(int)*(sl->max-sl->min+2)));
1074  for (int i=sl->min; i<=sl->max; i++)
1075  f[i-sl->min] = i;
1076  f[sl->max-sl->min+1] = -1;
1077  } else {
1078  f = static_cast<int*>(malloc(sizeof(int)*(sl->s.size()+1)));
1079  for (int j=sl->s.size(); j--; )
1080  f[j] = sl->s[j];
1081  f[sl->s.size()] = -1;
1082  }
1083 
1084  DFA dfa(q0,t,f);
1085  free(f);
1086  unshare(s, iv);
1087  extensional(s, iv, dfa, s.ann2icl(ann));
1088  }
1089 
1090  void
1091  p_sort(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1092  IntVarArgs x = s.arg2intvarargs(ce[0]);
1093  IntVarArgs y = s.arg2intvarargs(ce[1]);
1094  IntVarArgs xy(x.size()+y.size());
1095  for (int i=x.size(); i--;)
1096  xy[i] = x[i];
1097  for (int i=y.size(); i--;)
1098  xy[i+x.size()] = y[i];
1099  unshare(s, xy);
1100  for (int i=x.size(); i--;)
1101  x[i] = xy[i];
1102  for (int i=y.size(); i--;)
1103  y[i] = xy[i+x.size()];
1104  sorted(s, x, y, s.ann2icl(ann));
1105  }
1106 
1107  void
1108  p_inverse_offsets(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1109  IntVarArgs x = s.arg2intvarargs(ce[0]);
1110  unshare(s, x);
1111  int xoff = ce[1]->getInt();
1112  IntVarArgs y = s.arg2intvarargs(ce[2]);
1113  unshare(s, y);
1114  int yoff = ce[3]->getInt();
1115  channel(s, x, xoff, y, yoff, s.ann2icl(ann));
1116  }
1117 
1118  void
1119  p_increasing_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1120  IntVarArgs x = s.arg2intvarargs(ce[0]);
1121  rel(s,x,IRT_LQ,s.ann2icl(ann));
1122  }
1123 
1124  void
1125  p_increasing_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1126  BoolVarArgs x = s.arg2boolvarargs(ce[0]);
1127  rel(s,x,IRT_LQ,s.ann2icl(ann));
1128  }
1129 
1130  void
1131  p_decreasing_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1132  IntVarArgs x = s.arg2intvarargs(ce[0]);
1133  rel(s,x,IRT_GQ,s.ann2icl(ann));
1134  }
1135 
1136  void
1137  p_decreasing_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1138  BoolVarArgs x = s.arg2boolvarargs(ce[0]);
1139  rel(s,x,IRT_GQ,s.ann2icl(ann));
1140  }
1141 
1142  void
1143  p_table_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1144  IntVarArgs x = s.arg2intvarargs(ce[0]);
1145  IntArgs tuples = s.arg2intargs(ce[1]);
1146  int noOfVars = x.size();
1147  int noOfTuples = tuples.size() == 0 ? 0 : (tuples.size()/noOfVars);
1148  TupleSet ts;
1149  for (int i=0; i<noOfTuples; i++) {
1150  IntArgs t(noOfVars);
1151  for (int j=0; j<x.size(); j++) {
1152  t[j] = tuples[i*noOfVars+j];
1153  }
1154  ts.add(t);
1155  }
1156  ts.finalize();
1157  extensional(s,x,ts,EPK_DEF,s.ann2icl(ann));
1158  }
1159  void
1160  p_table_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1161  BoolVarArgs x = s.arg2boolvarargs(ce[0]);
1162  IntArgs tuples = s.arg2boolargs(ce[1]);
1163  int noOfVars = x.size();
1164  int noOfTuples = tuples.size() == 0 ? 0 : (tuples.size()/noOfVars);
1165  TupleSet ts;
1166  for (int i=0; i<noOfTuples; i++) {
1167  IntArgs t(noOfVars);
1168  for (int j=0; j<x.size(); j++) {
1169  t[j] = tuples[i*noOfVars+j];
1170  }
1171  ts.add(t);
1172  }
1173  ts.finalize();
1174  extensional(s,x,ts,EPK_DEF,s.ann2icl(ann));
1175  }
1176 
1177  void p_cumulative_opt(FlatZincSpace& s, const ConExpr& ce,
1178  AST::Node* ann) {
1179  IntVarArgs start = s.arg2intvarargs(ce[0]);
1180  IntArgs duration = s.arg2intargs(ce[1]);
1181  IntArgs height = s.arg2intargs(ce[2]);
1182  BoolVarArgs opt = s.arg2boolvarargs(ce[3]);
1183  int bound = ce[4]->getInt();
1184  unshare(s,start);
1185  cumulative(s,bound,start,duration,height,opt,s.ann2icl(ann));
1186  }
1187 
1188  void p_cumulatives(FlatZincSpace& s, const ConExpr& ce,
1189  AST::Node* ann) {
1190  IntVarArgs start = s.arg2intvarargs(ce[0]);
1191  IntVarArgs duration = s.arg2intvarargs(ce[1]);
1192  IntVarArgs height = s.arg2intvarargs(ce[2]);
1193  int n = start.size();
1194  IntVar bound = s.arg2IntVar(ce[3]);
1195 
1196  if (n==0)
1197  return;
1198 
1199  if (n == 1) {
1200  rel(s, height[0] <= bound);
1201  return;
1202  }
1203 
1204  int minHeight = std::min(height[0].min(),height[1].min());
1205  int minHeight2 = std::max(height[0].min(),height[1].min());
1206  for (int i=2; i<n; i++) {
1207  if (height[i].min() < minHeight) {
1208  minHeight2 = minHeight;
1209  minHeight = height[i].min();
1210  } else if (height[i].min() < minHeight2) {
1211  minHeight2 = height[i].min();
1212  }
1213  }
1214  bool disjunctive =
1215  (minHeight > bound.max()/2) ||
1216  (minHeight2 > bound.max()/2 && minHeight+minHeight2>bound.max());
1217  if (disjunctive) {
1218  rel(s, bound >= max(height));
1219  // Unary
1220  if (duration.assigned()) {
1221  IntArgs durationI(n);
1222  for (int i=n; i--;)
1223  durationI[i] = duration[i].val();
1224  unshare(s,start);
1225  unary(s,start,durationI);
1226  } else {
1227  IntVarArgs end(n);
1228  for (int i=n; i--;)
1229  end[i] = expr(s,start[i]+duration[i]);
1230  unshare(s,start);
1231  unary(s,start,duration,end);
1232  }
1233  } else if (height.assigned()) {
1234  IntArgs heightI(n);
1235  for (int i=n; i--;)
1236  heightI[i] = height[i].val();
1237  if (duration.assigned()) {
1238  IntArgs durationI(n);
1239  for (int i=n; i--;)
1240  durationI[i] = duration[i].val();
1241  cumulative(s, bound, start, durationI, heightI);
1242  } else {
1243  IntVarArgs end(n);
1244  for (int i = n; i--; )
1245  end[i] = expr(s,start[i]+duration[i]);
1246  cumulative(s, bound, start, duration, end, heightI);
1247  }
1248  } else if (bound.assigned()) {
1249  IntArgs machine = IntArgs::create(n,0,0);
1250  IntArgs limit(1, bound.val());
1251  IntVarArgs end(n);
1252  for (int i=n; i--;)
1253  end[i] = expr(s,start[i]+duration[i]);
1254  cumulatives(s, machine, start, duration, end, height, limit, true,
1255  s.ann2icl(ann));
1256  } else {
1259  IntVarArgs end(start.size());
1260  for (int i = start.size(); i--; ) {
1261  min = std::min(min, start[i].min());
1262  max = std::max(max, start[i].max() + duration[i].max());
1263  end[i] = expr(s, start[i] + duration[i]);
1264  }
1265  for (int time = min; time < max; ++time) {
1266  IntVarArgs x(start.size());
1267  for (int i = start.size(); i--; ) {
1268  IntVar overlaps = channel(s, expr(s, (start[i] <= time) &&
1269  (time < end[i])));
1270  x[i] = expr(s, overlaps * height[i]);
1271  }
1272  linear(s, x, IRT_LQ, bound);
1273  }
1274  }
1275  }
1276 
1277  void p_among_seq_int(FlatZincSpace& s, const ConExpr& ce,
1278  AST::Node* ann) {
1279  IntVarArgs x = s.arg2intvarargs(ce[0]);
1280  IntSet S = s.arg2intset(ce[1]);
1281  int q = ce[2]->getInt();
1282  int l = ce[3]->getInt();
1283  int u = ce[4]->getInt();
1284  unshare(s, x);
1285  sequence(s, x, S, q, l, u, s.ann2icl(ann));
1286  }
1287 
1288  void p_among_seq_bool(FlatZincSpace& s, const ConExpr& ce,
1289  AST::Node* ann) {
1290  BoolVarArgs x = s.arg2boolvarargs(ce[0]);
1291  bool val = ce[1]->getBool();
1292  int q = ce[2]->getInt();
1293  int l = ce[3]->getInt();
1294  int u = ce[4]->getInt();
1295  IntSet S(val, val);
1296  unshare(s, x);
1297  sequence(s, x, S, q, l, u, s.ann2icl(ann));
1298  }
1299 
1300  void p_schedule_unary(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
1301  IntVarArgs x = s.arg2intvarargs(ce[0]);
1302  IntArgs p = s.arg2intargs(ce[1]);
1303  unshare(s,x);
1304  unary(s, x, p);
1305  }
1306 
1307  void p_schedule_unary_optional(FlatZincSpace& s, const ConExpr& ce,
1308  AST::Node*) {
1309  IntVarArgs x = s.arg2intvarargs(ce[0]);
1310  IntArgs p = s.arg2intargs(ce[1]);
1311  BoolVarArgs m = s.arg2boolvarargs(ce[2]);
1312  unshare(s,x);
1313  unary(s, x, p, m);
1314  }
1315 
1316  void p_circuit(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
1317  int off = ce[0]->getInt();
1318  IntVarArgs xv = s.arg2intvarargs(ce[1]);
1319  unshare(s,xv);
1320  circuit(s,off,xv,s.ann2icl(ann));
1321  }
1322  void p_circuit_cost_array(FlatZincSpace& s, const ConExpr& ce,
1323  AST::Node *ann) {
1324  IntArgs c = s.arg2intargs(ce[0]);
1325  IntVarArgs xv = s.arg2intvarargs(ce[1]);
1326  IntVarArgs yv = s.arg2intvarargs(ce[2]);
1327  IntVar z = s.arg2IntVar(ce[3]);
1328  unshare(s,xv);
1329  circuit(s,c,xv,yv,z,s.ann2icl(ann));
1330  }
1331  void p_circuit_cost(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
1332  IntArgs c = s.arg2intargs(ce[0]);
1333  IntVarArgs xv = s.arg2intvarargs(ce[1]);
1334  IntVar z = s.arg2IntVar(ce[2]);
1335  unshare(s,xv);
1336  circuit(s,c,xv,z,s.ann2icl(ann));
1337  }
1338 
1339  void p_nooverlap(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
1340  IntVarArgs x0 = s.arg2intvarargs(ce[0]);
1341  IntVarArgs w = s.arg2intvarargs(ce[1]);
1342  IntVarArgs y0 = s.arg2intvarargs(ce[2]);
1343  IntVarArgs h = s.arg2intvarargs(ce[3]);
1344  if (w.assigned() && h.assigned()) {
1345  IntArgs iw(w.size());
1346  for (int i=w.size(); i--;)
1347  iw[i] = w[i].val();
1348  IntArgs ih(h.size());
1349  for (int i=h.size(); i--;)
1350  ih[i] = h[i].val();
1351  nooverlap(s,x0,iw,y0,ih,s.ann2icl(ann));
1352 
1353  int miny = y0[0].min();
1354  int maxy = y0[0].max();
1355  int maxdy = ih[0];
1356  for (int i=1; i<y0.size(); i++) {
1357  miny = std::min(miny,y0[i].min());
1358  maxy = std::max(maxy,y0[i].max());
1359  maxdy = std::max(maxdy,ih[i]);
1360  }
1361  int minx = x0[0].min();
1362  int maxx = x0[0].max();
1363  int maxdx = iw[0];
1364  for (int i=1; i<x0.size(); i++) {
1365  minx = std::min(minx,x0[i].min());
1366  maxx = std::max(maxx,x0[i].max());
1367  maxdx = std::max(maxdx,iw[i]);
1368  }
1369  if (miny > Int::Limits::min && maxy < Int::Limits::max) {
1370  cumulative(s,maxdy+maxy-miny,x0,iw,ih);
1371  cumulative(s,maxdx+maxx-minx,y0,ih,iw);
1372  }
1373  } else {
1374  IntVarArgs x1(x0.size()), y1(y0.size());
1375  for (int i=x0.size(); i--; )
1376  x1[i] = expr(s, x0[i] + w[i]);
1377  for (int i=y0.size(); i--; )
1378  y1[i] = expr(s, y0[i] + h[i]);
1379  nooverlap(s,x0,w,x1,y0,h,y1,s.ann2icl(ann));
1380  }
1381  }
1382 
1383  void p_precede(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1384  IntVarArgs x = s.arg2intvarargs(ce[0]);
1385  int p_s = ce[1]->getInt();
1386  int p_t = ce[2]->getInt();
1387  precede(s,x,p_s,p_t,s.ann2icl(ann));
1388  }
1389 
1390  void p_nvalue(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1391  IntVarArgs x = s.arg2intvarargs(ce[1]);
1392  if (ce[0]->isIntVar()) {
1393  IntVar y = s.arg2IntVar(ce[0]);
1394  nvalues(s,x,IRT_EQ,y,s.ann2icl(ann));
1395  } else {
1396  nvalues(s,x,IRT_EQ,ce[0]->getInt(),s.ann2icl(ann));
1397  }
1398  }
1399 
1400  void p_among(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1401  IntVarArgs x = s.arg2intvarargs(ce[1]);
1402  IntSet v = s.arg2intset(ce[2]);
1403  if (ce[0]->isIntVar()) {
1404  IntVar n = s.arg2IntVar(ce[0]);
1405  unshare(s, x);
1406  count(s,x,v,IRT_EQ,n,s.ann2icl(ann));
1407  } else {
1408  unshare(s, x);
1409  count(s,x,v,IRT_EQ,ce[0]->getInt(),s.ann2icl(ann));
1410  }
1411  }
1412 
1413  void p_member_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1414  IntVarArgs x = s.arg2intvarargs(ce[0]);
1415  IntVar y = s.arg2IntVar(ce[1]);
1416  member(s,x,y,s.ann2icl(ann));
1417  }
1418  void p_member_int_reif(FlatZincSpace& s, const ConExpr& ce,
1419  AST::Node* ann) {
1420  IntVarArgs x = s.arg2intvarargs(ce[0]);
1421  IntVar y = s.arg2IntVar(ce[1]);
1422  BoolVar b = s.arg2BoolVar(ce[2]);
1423  member(s,x,y,b,s.ann2icl(ann));
1424  }
1425  void p_member_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1426  BoolVarArgs x = s.arg2boolvarargs(ce[0]);
1427  BoolVar y = s.arg2BoolVar(ce[1]);
1428  member(s,x,y,s.ann2icl(ann));
1429  }
1430  void p_member_bool_reif(FlatZincSpace& s, const ConExpr& ce,
1431  AST::Node* ann) {
1432  BoolVarArgs x = s.arg2boolvarargs(ce[0]);
1433  BoolVar y = s.arg2BoolVar(ce[1]);
1434  member(s,x,y,s.arg2BoolVar(ce[2]),s.ann2icl(ann));
1435  }
1436 
1437  class IntPoster {
1438  public:
1439  IntPoster(void) {
1440  registry().add("all_different_int", &p_distinct);
1441  registry().add("all_different_offset", &p_distinctOffset);
1442  registry().add("all_equal_int", &p_all_equal);
1443  registry().add("int_eq", &p_int_eq);
1444  registry().add("int_ne", &p_int_ne);
1445  registry().add("int_ge", &p_int_ge);
1446  registry().add("int_gt", &p_int_gt);
1447  registry().add("int_le", &p_int_le);
1448  registry().add("int_lt", &p_int_lt);
1449  registry().add("int_eq_reif", &p_int_eq_reif);
1450  registry().add("int_ne_reif", &p_int_ne_reif);
1451  registry().add("int_ge_reif", &p_int_ge_reif);
1452  registry().add("int_gt_reif", &p_int_gt_reif);
1453  registry().add("int_le_reif", &p_int_le_reif);
1454  registry().add("int_lt_reif", &p_int_lt_reif);
1455  registry().add("int_eq_imp", &p_int_eq_imp);
1456  registry().add("int_ne_imp", &p_int_ne_imp);
1457  registry().add("int_ge_imp", &p_int_ge_imp);
1458  registry().add("int_gt_imp", &p_int_gt_imp);
1459  registry().add("int_le_imp", &p_int_le_imp);
1460  registry().add("int_lt_imp", &p_int_lt_imp);
1461  registry().add("int_lin_eq", &p_int_lin_eq);
1462  registry().add("int_lin_eq_reif", &p_int_lin_eq_reif);
1463  registry().add("int_lin_eq_imp", &p_int_lin_eq_imp);
1464  registry().add("int_lin_ne", &p_int_lin_ne);
1465  registry().add("int_lin_ne_reif", &p_int_lin_ne_reif);
1466  registry().add("int_lin_ne_imp", &p_int_lin_ne_imp);
1467  registry().add("int_lin_le", &p_int_lin_le);
1468  registry().add("int_lin_le_reif", &p_int_lin_le_reif);
1469  registry().add("int_lin_le_imp", &p_int_lin_le_imp);
1470  registry().add("int_lin_lt", &p_int_lin_lt);
1471  registry().add("int_lin_lt_reif", &p_int_lin_lt_reif);
1472  registry().add("int_lin_lt_imp", &p_int_lin_lt_imp);
1473  registry().add("int_lin_ge", &p_int_lin_ge);
1474  registry().add("int_lin_ge_reif", &p_int_lin_ge_reif);
1475  registry().add("int_lin_ge_imp", &p_int_lin_ge_imp);
1476  registry().add("int_lin_gt", &p_int_lin_gt);
1477  registry().add("int_lin_gt_reif", &p_int_lin_gt_reif);
1478  registry().add("int_lin_gt_imp", &p_int_lin_gt_imp);
1479  registry().add("int_plus", &p_int_plus);
1480  registry().add("int_minus", &p_int_minus);
1481  registry().add("int_times", &p_int_times);
1482  registry().add("int_div", &p_int_div);
1483  registry().add("int_mod", &p_int_mod);
1484  registry().add("int_min", &p_int_min);
1485  registry().add("int_max", &p_int_max);
1486  registry().add("int_abs", &p_abs);
1487  registry().add("int_negate", &p_int_negate);
1488  registry().add("bool_eq", &p_bool_eq);
1489  registry().add("bool_eq_reif", &p_bool_eq_reif);
1490  registry().add("bool_eq_imp", &p_bool_eq_imp);
1491  registry().add("bool_ne", &p_bool_ne);
1492  registry().add("bool_ne_reif", &p_bool_ne_reif);
1493  registry().add("bool_ne_imp", &p_bool_ne_imp);
1494  registry().add("bool_ge", &p_bool_ge);
1495  registry().add("bool_ge_reif", &p_bool_ge_reif);
1496  registry().add("bool_ge_imp", &p_bool_ge_imp);
1497  registry().add("bool_le", &p_bool_le);
1498  registry().add("bool_le_reif", &p_bool_le_reif);
1499  registry().add("bool_le_imp", &p_bool_le_imp);
1500  registry().add("bool_gt", &p_bool_gt);
1501  registry().add("bool_gt_reif", &p_bool_gt_reif);
1502  registry().add("bool_gt_imp", &p_bool_gt_imp);
1503  registry().add("bool_lt", &p_bool_lt);
1504  registry().add("bool_lt_reif", &p_bool_lt_reif);
1505  registry().add("bool_lt_imp", &p_bool_lt_imp);
1506  registry().add("bool_or", &p_bool_or);
1507  registry().add("bool_or_imp", &p_bool_or_imp);
1508  registry().add("bool_and", &p_bool_and);
1509  registry().add("bool_and_imp", &p_bool_and_imp);
1510  registry().add("bool_xor", &p_bool_xor);
1511  registry().add("bool_xor_imp", &p_bool_xor_imp);
1512  registry().add("array_bool_and", &p_array_bool_and);
1513  registry().add("array_bool_and_imp", &p_array_bool_and_imp);
1514  registry().add("array_bool_or", &p_array_bool_or);
1515  registry().add("array_bool_or_imp", &p_array_bool_or_imp);
1516  registry().add("array_bool_xor", &p_array_bool_xor);
1517  registry().add("array_bool_xor_imp", &p_array_bool_xor_imp);
1518  registry().add("bool_clause", &p_array_bool_clause);
1519  registry().add("bool_clause_reif", &p_array_bool_clause_reif);
1520  registry().add("bool_clause_imp", &p_array_bool_clause_imp);
1521  registry().add("bool_left_imp", &p_bool_l_imp);
1522  registry().add("bool_right_imp", &p_bool_r_imp);
1523  registry().add("bool_not", &p_bool_not);
1524  registry().add("array_int_element", &p_array_int_element);
1525  registry().add("array_var_int_element", &p_array_int_element);
1526  registry().add("array_bool_element", &p_array_bool_element);
1527  registry().add("array_var_bool_element", &p_array_bool_element);
1528  registry().add("bool2int", &p_bool2int);
1529  registry().add("int_in", &p_int_in);
1530  registry().add("int_in_reif", &p_int_in_reif);
1531  registry().add("int_in_imp", &p_int_in_imp);
1532 #ifndef GECODE_HAS_SET_VARS
1533  registry().add("set_in", &p_int_in);
1534  registry().add("set_in_reif", &p_int_in_reif);
1535  registry().add("set_in_imp", &p_int_in_imp);
1536 #endif
1537 
1538  registry().add("array_int_lt", &p_array_int_lt);
1539  registry().add("array_int_lq", &p_array_int_lq);
1540  registry().add("array_bool_lt", &p_array_bool_lt);
1541  registry().add("array_bool_lq", &p_array_bool_lq);
1542  registry().add("count", &p_count);
1543  registry().add("count_reif", &p_count_reif);
1544  registry().add("count_imp", &p_count_imp);
1545  registry().add("at_least_int", &p_at_least);
1546  registry().add("at_most_int", &p_at_most);
1547  registry().add("gecode_bin_packing_load", &p_bin_packing_load);
1548  registry().add("global_cardinality", &p_global_cardinality);
1549  registry().add("global_cardinality_closed",
1550  &p_global_cardinality_closed);
1551  registry().add("global_cardinality_low_up",
1552  &p_global_cardinality_low_up);
1553  registry().add("global_cardinality_low_up_closed",
1554  &p_global_cardinality_low_up_closed);
1555  registry().add("array_int_minimum", &p_minimum);
1556  registry().add("array_int_maximum", &p_maximum);
1557  registry().add("gecode_minimum_arg_int", &p_minimum_arg);
1558  registry().add("gecode_maximum_arg_int", &p_maximum_arg);
1559  registry().add("array_int_maximum", &p_maximum);
1560  registry().add("regular", &p_regular);
1561  registry().add("sort", &p_sort);
1562  registry().add("inverse_offsets", &p_inverse_offsets);
1563  registry().add("increasing_int", &p_increasing_int);
1564  registry().add("increasing_bool", &p_increasing_bool);
1565  registry().add("decreasing_int", &p_decreasing_int);
1566  registry().add("decreasing_bool", &p_decreasing_bool);
1567  registry().add("table_int", &p_table_int);
1568  registry().add("table_bool", &p_table_bool);
1569  registry().add("cumulatives", &p_cumulatives);
1570  registry().add("gecode_among_seq_int", &p_among_seq_int);
1571  registry().add("gecode_among_seq_bool", &p_among_seq_bool);
1572 
1573  registry().add("bool_lin_eq", &p_bool_lin_eq);
1574  registry().add("bool_lin_ne", &p_bool_lin_ne);
1575  registry().add("bool_lin_le", &p_bool_lin_le);
1576  registry().add("bool_lin_lt", &p_bool_lin_lt);
1577  registry().add("bool_lin_ge", &p_bool_lin_ge);
1578  registry().add("bool_lin_gt", &p_bool_lin_gt);
1579 
1580  registry().add("bool_lin_eq_reif", &p_bool_lin_eq_reif);
1581  registry().add("bool_lin_eq_imp", &p_bool_lin_eq_imp);
1582  registry().add("bool_lin_ne_reif", &p_bool_lin_ne_reif);
1583  registry().add("bool_lin_ne_imp", &p_bool_lin_ne_imp);
1584  registry().add("bool_lin_le_reif", &p_bool_lin_le_reif);
1585  registry().add("bool_lin_le_imp", &p_bool_lin_le_imp);
1586  registry().add("bool_lin_lt_reif", &p_bool_lin_lt_reif);
1587  registry().add("bool_lin_lt_imp", &p_bool_lin_lt_imp);
1588  registry().add("bool_lin_ge_reif", &p_bool_lin_ge_reif);
1589  registry().add("bool_lin_ge_imp", &p_bool_lin_ge_imp);
1590  registry().add("bool_lin_gt_reif", &p_bool_lin_gt_reif);
1591  registry().add("bool_lin_gt_imp", &p_bool_lin_gt_imp);
1592 
1593  registry().add("gecode_schedule_unary", &p_schedule_unary);
1594  registry().add("gecode_schedule_unary_optional", &p_schedule_unary_optional);
1595  registry().add("gecode_schedule_cumulative_optional", &p_cumulative_opt);
1596 
1597  registry().add("gecode_circuit", &p_circuit);
1598  registry().add("gecode_circuit_cost_array", &p_circuit_cost_array);
1599  registry().add("gecode_circuit_cost", &p_circuit_cost);
1600  registry().add("gecode_nooverlap", &p_nooverlap);
1601  registry().add("gecode_precede", &p_precede);
1602  registry().add("nvalue",&p_nvalue);
1603  registry().add("among",&p_among);
1604  registry().add("member_int",&p_member_int);
1605  registry().add("gecode_member_int_reif",&p_member_int_reif);
1606  registry().add("member_bool",&p_member_bool);
1607  registry().add("gecode_member_bool_reif",&p_member_bool_reif);
1608  }
1609  };
1610  IntPoster __int_poster;
1611 
1612 #ifdef GECODE_HAS_SET_VARS
1613  void p_set_OP(FlatZincSpace& s, SetOpType op,
1614  const ConExpr& ce, AST::Node *) {
1615  rel(s, s.arg2SetVar(ce[0]), op, s.arg2SetVar(ce[1]),
1616  SRT_EQ, s.arg2SetVar(ce[2]));
1617  }
1618  void p_set_union(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
1619  p_set_OP(s, SOT_UNION, ce, ann);
1620  }
1621  void p_set_intersect(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
1622  p_set_OP(s, SOT_INTER, ce, ann);
1623  }
1624  void p_set_diff(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
1625  p_set_OP(s, SOT_MINUS, ce, ann);
1626  }
1627 
1628  void p_set_symdiff(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
1629  SetVar x = s.arg2SetVar(ce[0]);
1630  SetVar y = s.arg2SetVar(ce[1]);
1631 
1632  SetVarLubRanges xub(x);
1633  IntSet xubs(xub);
1634  SetVar x_y(s,IntSet::empty,xubs);
1635  rel(s, x, SOT_MINUS, y, SRT_EQ, x_y);
1636 
1637  SetVarLubRanges yub(y);
1638  IntSet yubs(yub);
1639  SetVar y_x(s,IntSet::empty,yubs);
1640  rel(s, y, SOT_MINUS, x, SRT_EQ, y_x);
1641 
1642  rel(s, x_y, SOT_UNION, y_x, SRT_EQ, s.arg2SetVar(ce[2]));
1643  }
1644 
1645  void p_array_set_OP(FlatZincSpace& s, SetOpType op,
1646  const ConExpr& ce, AST::Node *) {
1647  SetVarArgs xs = s.arg2setvarargs(ce[0]);
1648  rel(s, op, xs, s.arg2SetVar(ce[1]));
1649  }
1650  void p_array_set_union(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
1651  p_array_set_OP(s, SOT_UNION, ce, ann);
1652  }
1653  void p_array_set_partition(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
1654  p_array_set_OP(s, SOT_DUNION, ce, ann);
1655  }
1656 
1657 
1658  void p_set_rel(FlatZincSpace& s, SetRelType srt, const ConExpr& ce) {
1659  rel(s, s.arg2SetVar(ce[0]), srt, s.arg2SetVar(ce[1]));
1660  }
1661 
1662  void p_set_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1663  p_set_rel(s, SRT_EQ, ce);
1664  }
1665  void p_set_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1666  p_set_rel(s, SRT_NQ, ce);
1667  }
1668  void p_set_subset(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1669  p_set_rel(s, SRT_SUB, ce);
1670  }
1671  void p_set_superset(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1672  p_set_rel(s, SRT_SUP, ce);
1673  }
1674  void p_set_le(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1675  p_set_rel(s, SRT_LQ, ce);
1676  }
1677  void p_set_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1678  p_set_rel(s, SRT_LE, ce);
1679  }
1680  void p_set_card(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1681  if (!ce[1]->isIntVar()) {
1682  cardinality(s, s.arg2SetVar(ce[0]), ce[1]->getInt(),
1683  ce[1]->getInt());
1684  } else {
1685  cardinality(s, s.arg2SetVar(ce[0]), s.arg2IntVar(ce[1]));
1686  }
1687  }
1688  void p_set_in(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1689  if (!ce[1]->isSetVar()) {
1690  IntSet d = s.arg2intset(ce[1]);
1691  if (ce[0]->isBoolVar()) {
1692  IntSetRanges dr(d);
1693  Iter::Ranges::Singleton sr(0,1);
1694  Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr);
1695  IntSet d01(i);
1696  if (d01.size() == 0) {
1697  s.fail();
1698  } else {
1699  rel(s, s.arg2BoolVar(ce[0]), IRT_GQ, d01.min());
1700  rel(s, s.arg2BoolVar(ce[0]), IRT_LQ, d01.max());
1701  }
1702  } else {
1703  dom(s, s.arg2IntVar(ce[0]), d);
1704  }
1705  } else {
1706  if (!ce[0]->isIntVar()) {
1707  dom(s, s.arg2SetVar(ce[1]), SRT_SUP, ce[0]->getInt());
1708  } else {
1709  rel(s, s.arg2SetVar(ce[1]), SRT_SUP, s.arg2IntVar(ce[0]));
1710  }
1711  }
1712  }
1713  void p_set_rel_reif(FlatZincSpace& s, SetRelType srt, const ConExpr& ce) {
1714  rel(s, s.arg2SetVar(ce[0]), srt, s.arg2SetVar(ce[1]),
1715  s.arg2BoolVar(ce[2]));
1716  }
1717 
1718  void p_set_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1719  p_set_rel_reif(s,SRT_EQ,ce);
1720  }
1721  void p_set_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1722  p_set_rel_reif(s,SRT_LQ,ce);
1723  }
1724  void p_set_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1725  p_set_rel_reif(s,SRT_LE,ce);
1726  }
1727  void p_set_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1728  p_set_rel_reif(s,SRT_NQ,ce);
1729  }
1730  void p_set_subset_reif(FlatZincSpace& s, const ConExpr& ce,
1731  AST::Node *) {
1732  p_set_rel_reif(s,SRT_SUB,ce);
1733  }
1734  void p_set_superset_reif(FlatZincSpace& s, const ConExpr& ce,
1735  AST::Node *) {
1736  p_set_rel_reif(s,SRT_SUP,ce);
1737  }
1738  void p_set_in_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann, ReifyMode rm) {
1739  if (!ce[1]->isSetVar()) {
1740  if (rm==RM_EQV) {
1741  p_int_in_reif(s,ce,ann);
1742  } else {
1743  assert(rm==RM_IMP);
1744  p_int_in_imp(s,ce,ann);
1745  }
1746  } else {
1747  if (!ce[0]->isIntVar()) {
1748  dom(s, s.arg2SetVar(ce[1]), SRT_SUP, ce[0]->getInt(),
1749  Reify(s.arg2BoolVar(ce[2]),rm));
1750  } else {
1751  rel(s, s.arg2SetVar(ce[1]), SRT_SUP, s.arg2IntVar(ce[0]),
1752  Reify(s.arg2BoolVar(ce[2]),rm));
1753  }
1754  }
1755  }
1756  void p_set_in_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1757  p_set_in_reif(s,ce,ann,RM_EQV);
1758  }
1759  void p_set_in_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1760  p_set_in_reif(s,ce,ann,RM_IMP);
1761  }
1762  void p_set_disjoint(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1763  rel(s, s.arg2SetVar(ce[0]), SRT_DISJ, s.arg2SetVar(ce[1]));
1764  }
1765 
1766  void p_link_set_to_booleans(FlatZincSpace& s, const ConExpr& ce,
1767  AST::Node *) {
1768  SetVar x = s.arg2SetVar(ce[0]);
1769  int idx = ce[2]->getInt();
1770  assert(idx >= 0);
1771  rel(s, x || IntSet(Set::Limits::min,idx-1));
1772  BoolVarArgs y = s.arg2boolvarargs(ce[1],idx);
1773  unshare(s, y);
1774  channel(s, y, x);
1775  }
1776 
1777  void p_array_set_element(FlatZincSpace& s, const ConExpr& ce,
1778  AST::Node*) {
1779  bool isConstant = true;
1780  AST::Array* a = ce[1]->getArray();
1781  for (int i=a->a.size(); i--;) {
1782  if (a->a[i]->isSetVar()) {
1783  isConstant = false;
1784  break;
1785  }
1786  }
1787  IntVar selector = s.arg2IntVar(ce[0]);
1788  rel(s, selector > 0);
1789  if (isConstant) {
1790  IntSetArgs sv = s.arg2intsetargs(ce[1],1);
1791  element(s, sv, selector, s.arg2SetVar(ce[2]));
1792  } else {
1793  SetVarArgs sv = s.arg2setvarargs(ce[1], 1);
1794  element(s, sv, selector, s.arg2SetVar(ce[2]));
1795  }
1796  }
1797 
1798  void p_array_set_element_op(FlatZincSpace& s, const ConExpr& ce,
1799  AST::Node*, SetOpType op,
1800  const IntSet& universe =
1802  bool isConstant = true;
1803  AST::Array* a = ce[1]->getArray();
1804  for (int i=a->a.size(); i--;) {
1805  if (a->a[i]->isSetVar()) {
1806  isConstant = false;
1807  break;
1808  }
1809  }
1810  SetVar selector = s.arg2SetVar(ce[0]);
1811  dom(s, selector, SRT_DISJ, 0);
1812  if (isConstant) {
1813  IntSetArgs sv = s.arg2intsetargs(ce[1], 1);
1814  element(s, op, sv, selector, s.arg2SetVar(ce[2]), universe);
1815  } else {
1816  SetVarArgs sv = s.arg2setvarargs(ce[1], 1);
1817  element(s, op, sv, selector, s.arg2SetVar(ce[2]), universe);
1818  }
1819  }
1820 
1821  void p_array_set_element_union(FlatZincSpace& s, const ConExpr& ce,
1822  AST::Node* ann) {
1823  p_array_set_element_op(s, ce, ann, SOT_UNION);
1824  }
1825 
1826  void p_array_set_element_intersect(FlatZincSpace& s, const ConExpr& ce,
1827  AST::Node* ann) {
1828  p_array_set_element_op(s, ce, ann, SOT_INTER);
1829  }
1830 
1831  void p_array_set_element_intersect_in(FlatZincSpace& s,
1832  const ConExpr& ce,
1833  AST::Node* ann) {
1834  IntSet d = s.arg2intset(ce[3]);
1835  p_array_set_element_op(s, ce, ann, SOT_INTER, d);
1836  }
1837 
1838  void p_array_set_element_partition(FlatZincSpace& s, const ConExpr& ce,
1839  AST::Node* ann) {
1840  p_array_set_element_op(s, ce, ann, SOT_DUNION);
1841  }
1842 
1843  void p_set_convex(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1844  convex(s, s.arg2SetVar(ce[0]));
1845  }
1846 
1847  void p_array_set_seq(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1848  SetVarArgs sv = s.arg2setvarargs(ce[0]);
1849  sequence(s, sv);
1850  }
1851 
1852  void p_array_set_seq_union(FlatZincSpace& s, const ConExpr& ce,
1853  AST::Node *) {
1854  SetVarArgs sv = s.arg2setvarargs(ce[0]);
1855  sequence(s, sv, s.arg2SetVar(ce[1]));
1856  }
1857 
1858  void p_int_set_channel(FlatZincSpace& s, const ConExpr& ce,
1859  AST::Node *) {
1860  int xoff=ce[1]->getInt();
1861  assert(xoff >= 0);
1862  int yoff=ce[3]->getInt();
1863  assert(yoff >= 0);
1864  IntVarArgs xv = s.arg2intvarargs(ce[0], xoff);
1865  SetVarArgs yv = s.arg2setvarargs(ce[2], yoff, 1, IntSet(0, xoff-1));
1866  IntSet xd(yoff,yv.size()-1);
1867  for (int i=xoff; i<xv.size(); i++) {
1868  dom(s, xv[i], xd);
1869  }
1870  IntSet yd(xoff,xv.size()-1);
1871  for (int i=yoff; i<yv.size(); i++) {
1872  dom(s, yv[i], SRT_SUB, yd);
1873  }
1874  channel(s,xv,yv);
1875  }
1876 
1877  void p_range(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
1878  int xoff=ce[1]->getInt();
1879  assert(xoff >= 0);
1880  IntVarArgs xv = s.arg2intvarargs(ce[0],xoff);
1881  element(s, SOT_UNION, xv, s.arg2SetVar(ce[2]), s.arg2SetVar(ce[3]));
1882  }
1883 
1884  void p_weights(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
1885  IntArgs e = s.arg2intargs(ce[0]);
1886  IntArgs w = s.arg2intargs(ce[1]);
1887  SetVar x = s.arg2SetVar(ce[2]);
1888  IntVar y = s.arg2IntVar(ce[3]);
1889  weights(s,e,w,x,y);
1890  }
1891 
1892  void p_inverse_set(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
1893  int xoff = ce[2]->getInt();
1894  int yoff = ce[3]->getInt();
1895  SetVarArgs x = s.arg2setvarargs(ce[0],xoff);
1896  SetVarArgs y = s.arg2setvarargs(ce[1],yoff);
1897  channel(s, x, y);
1898  }
1899 
1900  void p_precede_set(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
1901  SetVarArgs x = s.arg2setvarargs(ce[0]);
1902  int p_s = ce[1]->getInt();
1903  int p_t = ce[2]->getInt();
1904  precede(s,x,p_s,p_t);
1905  }
1906 
1907  class SetPoster {
1908  public:
1909  SetPoster(void) {
1910  registry().add("set_eq", &p_set_eq);
1911  registry().add("set_le", &p_set_le);
1912  registry().add("set_lt", &p_set_lt);
1913  registry().add("equal", &p_set_eq);
1914  registry().add("set_ne", &p_set_ne);
1915  registry().add("set_union", &p_set_union);
1916  registry().add("array_set_element", &p_array_set_element);
1917  registry().add("array_var_set_element", &p_array_set_element);
1918  registry().add("set_intersect", &p_set_intersect);
1919  registry().add("set_diff", &p_set_diff);
1920  registry().add("set_symdiff", &p_set_symdiff);
1921  registry().add("set_subset", &p_set_subset);
1922  registry().add("set_superset", &p_set_superset);
1923  registry().add("set_card", &p_set_card);
1924  registry().add("set_in", &p_set_in);
1925  registry().add("set_eq_reif", &p_set_eq_reif);
1926  registry().add("set_le_reif", &p_set_le_reif);
1927  registry().add("set_lt_reif", &p_set_lt_reif);
1928  registry().add("equal_reif", &p_set_eq_reif);
1929  registry().add("set_ne_reif", &p_set_ne_reif);
1930  registry().add("set_subset_reif", &p_set_subset_reif);
1931  registry().add("set_superset_reif", &p_set_superset_reif);
1932  registry().add("set_in_reif", &p_set_in_reif);
1933  registry().add("set_in_imp", &p_set_in_imp);
1934  registry().add("disjoint", &p_set_disjoint);
1935  registry().add("gecode_link_set_to_booleans",
1936  &p_link_set_to_booleans);
1937 
1938  registry().add("array_set_union", &p_array_set_union);
1939  registry().add("array_set_partition", &p_array_set_partition);
1940  registry().add("set_convex", &p_set_convex);
1941  registry().add("array_set_seq", &p_array_set_seq);
1942  registry().add("array_set_seq_union", &p_array_set_seq_union);
1943  registry().add("gecode_array_set_element_union",
1944  &p_array_set_element_union);
1945  registry().add("gecode_array_set_element_intersect",
1946  &p_array_set_element_intersect);
1947  registry().add("gecode_array_set_element_intersect_in",
1948  &p_array_set_element_intersect_in);
1949  registry().add("gecode_array_set_element_partition",
1950  &p_array_set_element_partition);
1951  registry().add("gecode_int_set_channel",
1952  &p_int_set_channel);
1953  registry().add("gecode_range",
1954  &p_range);
1955  registry().add("gecode_set_weights",
1956  &p_weights);
1957  registry().add("gecode_inverse_set", &p_inverse_set);
1958  registry().add("gecode_precede_set", &p_precede_set);
1959  }
1960  };
1961  SetPoster __set_poster;
1962 #endif
1963 
1964 #ifdef GECODE_HAS_FLOAT_VARS
1965 
1966  void p_int2float(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
1967  IntVar x0 = s.arg2IntVar(ce[0]);
1968  FloatVar x1 = s.arg2FloatVar(ce[1]);
1969  channel(s, x0, x1);
1970  }
1971 
1972  void p_float_lin_cmp(FlatZincSpace& s, FloatRelType frt,
1973  const ConExpr& ce, AST::Node*) {
1974  FloatValArgs fa = s.arg2floatargs(ce[0]);
1975  FloatVarArgs fv = s.arg2floatvarargs(ce[1]);
1976  linear(s, fa, fv, frt, ce[2]->getFloat());
1977  }
1978  void p_float_lin_cmp_reif(FlatZincSpace& s, FloatRelType frt,
1979  const ConExpr& ce, AST::Node*) {
1980  FloatValArgs fa = s.arg2floatargs(ce[0]);
1981  FloatVarArgs fv = s.arg2floatvarargs(ce[1]);
1982  linear(s, fa, fv, frt, ce[2]->getFloat(), s.arg2BoolVar(ce[3]));
1983  }
1984  void p_float_lin_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1985  p_float_lin_cmp(s,FRT_EQ,ce,ann);
1986  }
1987  void p_float_lin_eq_reif(FlatZincSpace& s, const ConExpr& ce,
1988  AST::Node* ann) {
1989  p_float_lin_cmp_reif(s,FRT_EQ,ce,ann);
1990  }
1991  void p_float_lin_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1992  p_float_lin_cmp(s,FRT_LQ,ce,ann);
1993  }
1994  void p_float_lin_le_reif(FlatZincSpace& s, const ConExpr& ce,
1995  AST::Node* ann) {
1996  p_float_lin_cmp_reif(s,FRT_LQ,ce,ann);
1997  }
1998 
1999  void p_float_times(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2000  FloatVar x = s.arg2FloatVar(ce[0]);
2001  FloatVar y = s.arg2FloatVar(ce[1]);
2002  FloatVar z = s.arg2FloatVar(ce[2]);
2003  mult(s,x,y,z);
2004  }
2005 
2006  void p_float_div(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2007  FloatVar x = s.arg2FloatVar(ce[0]);
2008  FloatVar y = s.arg2FloatVar(ce[1]);
2009  FloatVar z = s.arg2FloatVar(ce[2]);
2010  div(s,x,y,z);
2011  }
2012 
2013  void p_float_plus(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2014  FloatVar x = s.arg2FloatVar(ce[0]);
2015  FloatVar y = s.arg2FloatVar(ce[1]);
2016  FloatVar z = s.arg2FloatVar(ce[2]);
2017  rel(s,x+y==z);
2018  }
2019 
2020  void p_float_sqrt(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2021  FloatVar x = s.arg2FloatVar(ce[0]);
2022  FloatVar y = s.arg2FloatVar(ce[1]);
2023  sqrt(s,x,y);
2024  }
2025 
2026  void p_float_abs(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2027  FloatVar x = s.arg2FloatVar(ce[0]);
2028  FloatVar y = s.arg2FloatVar(ce[1]);
2029  abs(s,x,y);
2030  }
2031 
2032  void p_float_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2033  FloatVar x = s.arg2FloatVar(ce[0]);
2034  FloatVar y = s.arg2FloatVar(ce[1]);
2035  rel(s,x,FRT_EQ,y);
2036  }
2037  void p_float_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2038  FloatVar x = s.arg2FloatVar(ce[0]);
2039  FloatVar y = s.arg2FloatVar(ce[1]);
2040  BoolVar b = s.arg2BoolVar(ce[2]);
2041  rel(s,x,FRT_EQ,y,b);
2042  }
2043  void p_float_le(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2044  FloatVar x = s.arg2FloatVar(ce[0]);
2045  FloatVar y = s.arg2FloatVar(ce[1]);
2046  rel(s,x,FRT_LQ,y);
2047  }
2048  void p_float_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2049  FloatVar x = s.arg2FloatVar(ce[0]);
2050  FloatVar y = s.arg2FloatVar(ce[1]);
2051  BoolVar b = s.arg2BoolVar(ce[2]);
2052  rel(s,x,FRT_LQ,y,b);
2053  }
2054  void p_float_max(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2055  FloatVar x = s.arg2FloatVar(ce[0]);
2056  FloatVar y = s.arg2FloatVar(ce[1]);
2057  FloatVar z = s.arg2FloatVar(ce[2]);
2058  max(s,x,y,z);
2059  }
2060  void p_float_min(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2061  FloatVar x = s.arg2FloatVar(ce[0]);
2062  FloatVar y = s.arg2FloatVar(ce[1]);
2063  FloatVar z = s.arg2FloatVar(ce[2]);
2064  min(s,x,y,z);
2065  }
2066  void p_float_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2067  FloatVar x = s.arg2FloatVar(ce[0]);
2068  FloatVar y = s.arg2FloatVar(ce[1]);
2069  rel(s, x, FRT_LQ, y);
2070  rel(s, x, FRT_EQ, y, BoolVar(s,0,0));
2071  }
2072 
2073  void p_float_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2074  FloatVar x = s.arg2FloatVar(ce[0]);
2075  FloatVar y = s.arg2FloatVar(ce[1]);
2076  BoolVar b = s.arg2BoolVar(ce[2]);
2077  BoolVar b0(s,0,1);
2078  BoolVar b1(s,0,1);
2079  rel(s, b == (b0 && !b1));
2080  rel(s, x, FRT_LQ, y, b0);
2081  rel(s, x, FRT_EQ, y, b1);
2082  }
2083 
2084  void p_float_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2085  FloatVar x = s.arg2FloatVar(ce[0]);
2086  FloatVar y = s.arg2FloatVar(ce[1]);
2087  rel(s, x, FRT_EQ, y, BoolVar(s,0,0));
2088  }
2089 
2090 #ifdef GECODE_HAS_MPFR
2091 #define P_FLOAT_OP(Op) \
2092  void p_float_ ## Op (FlatZincSpace& s, const ConExpr& ce, AST::Node*) {\
2093  FloatVar x = s.arg2FloatVar(ce[0]);\
2094  FloatVar y = s.arg2FloatVar(ce[1]);\
2095  Op(s,x,y);\
2096  }
2097  P_FLOAT_OP(acos)
2098  P_FLOAT_OP(asin)
2099  P_FLOAT_OP(atan)
2100  P_FLOAT_OP(cos)
2101  P_FLOAT_OP(exp)
2102  P_FLOAT_OP(sin)
2103  P_FLOAT_OP(tan)
2104  // P_FLOAT_OP(sinh)
2105  // P_FLOAT_OP(tanh)
2106  // P_FLOAT_OP(cosh)
2107 #undef P_FLOAT_OP
2108 
2109  void p_float_ln(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2110  FloatVar x = s.arg2FloatVar(ce[0]);
2111  FloatVar y = s.arg2FloatVar(ce[1]);
2112  log(s,x,y);
2113  }
2114  void p_float_log10(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2115  FloatVar x = s.arg2FloatVar(ce[0]);
2116  FloatVar y = s.arg2FloatVar(ce[1]);
2117  log(s,10.0,x,y);
2118  }
2119  void p_float_log2(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2120  FloatVar x = s.arg2FloatVar(ce[0]);
2121  FloatVar y = s.arg2FloatVar(ce[1]);
2122  log(s,2.0,x,y);
2123  }
2124 
2125 #endif
2126 
2127  class FloatPoster {
2128  public:
2129  FloatPoster(void) {
2130  registry().add("int2float",&p_int2float);
2131  registry().add("float_abs",&p_float_abs);
2132  registry().add("float_sqrt",&p_float_sqrt);
2133  registry().add("float_eq",&p_float_eq);
2134  registry().add("float_eq_reif",&p_float_eq_reif);
2135  registry().add("float_le",&p_float_le);
2136  registry().add("float_le_reif",&p_float_le_reif);
2137  registry().add("float_lt",&p_float_lt);
2138  registry().add("float_lt_reif",&p_float_lt_reif);
2139  registry().add("float_ne",&p_float_ne);
2140  registry().add("float_times",&p_float_times);
2141  registry().add("float_div",&p_float_div);
2142  registry().add("float_plus",&p_float_plus);
2143  registry().add("float_max",&p_float_max);
2144  registry().add("float_min",&p_float_min);
2145 
2146  registry().add("float_lin_eq",&p_float_lin_eq);
2147  registry().add("float_lin_eq_reif",&p_float_lin_eq_reif);
2148  registry().add("float_lin_le",&p_float_lin_le);
2149  registry().add("float_lin_le_reif",&p_float_lin_le_reif);
2150 
2151 #ifdef GECODE_HAS_MPFR
2152  registry().add("float_acos",&p_float_acos);
2153  registry().add("float_asin",&p_float_asin);
2154  registry().add("float_atan",&p_float_atan);
2155  registry().add("float_cos",&p_float_cos);
2156  // registry().add("float_cosh",&p_float_cosh);
2157  registry().add("float_exp",&p_float_exp);
2158  registry().add("float_ln",&p_float_ln);
2159  registry().add("float_log10",&p_float_log10);
2160  registry().add("float_log2",&p_float_log2);
2161  registry().add("float_sin",&p_float_sin);
2162  // registry().add("float_sinh",&p_float_sinh);
2163  registry().add("float_tan",&p_float_tan);
2164  // registry().add("float_tanh",&p_float_tanh);
2165 #endif
2166  }
2167  } __float_poster;
2168 #endif
2169 
2170  }
2171 }}
2172 
2173 // STATISTICS: flatzinc-any
static IntArgs create(int n, int start, int inc=1)
Allocate array with n elements such that for all .
Definition: array.hpp:72
void cumulative(Home home, Cap c, const TaskTypeArgs &t, const IntVarArgs &s, const IntArgs &p, const IntArgs &u, IntConLevel icl)
Definition: cumulative.cpp:48
NodeType t
Type of node.
Definition: bool-expr.cpp:234
SetRelType
Common relation types for sets.
Definition: set.hh:644
IntConLevel
Consistency levels for integer propagators.
Definition: int.hh:937
void mult(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:96
void linear(Home home, const FloatVarArgs &x, FloatRelType frt, FloatNum c)
Post propagator for .
Definition: linear.cpp:45
void post(FlatZincSpace &s, const ConExpr &ce)
Post constraint specified by ce.
Definition: registry.cpp:63
NNF * l
Left subtree.
Definition: bool-expr.cpp:244
void mod(Home home, IntVar x0, IntVar x1, IntVar x2, IntConLevel icl)
Post propagator for .
Definition: arithmetic.cpp:213
const int min
Smallest allowed integer in integer set.
Definition: set.hh:101
Map from constraint identifier to constraint posting functions.
Definition: registry.hh:48
void log(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition: arithmetic.cpp:151
void channel(Home home, FloatVar x0, IntVar x1)
Post propagator for channeling a float and an integer variable .
Definition: arithmetic.cpp:218
const FloatNum max
Largest allowed float value.
Definition: float.hh:831
int size(void) const
Return size of array (number of elements)
Definition: array.hpp:1662
Less or equal ( )
Definition: float.hh:1057
void max(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:57
void abs(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition: arithmetic.cpp:49
Less or equal ( )
Definition: int.hh:906
Make a default decision.
Definition: int.hh:1983
Conjunction.
Definition: int.hh:917
void dom(Home home, FloatVar x, FloatVal n)
Propagates .
Definition: dom.cpp:44
Implication.
Definition: int.hh:919
SetOpType
Common operations for sets.
Definition: set.hh:661
Greater ( )
Definition: int.hh:909
Superset ( )
Definition: set.hh:648
const int max
Largest allowed integer in integer set.
Definition: set.hh:99
ArgArray< IntSet > IntSetArgs
Passing set arguments.
Definition: int.hh:598
const int max
Largest allowed integer value.
Definition: int.hh:113
Greater or equal ( )
Definition: int.hh:908
Difference.
Definition: set.hh:665
Exclusive or.
Definition: int.hh:921
const int min
Smallest allowed integer value.
Definition: int.hh:115
void argmin(Home home, const IntVarArgs &x, IntVar y, bool tiebreak, IntConLevel)
Post propagator for .
Definition: arithmetic.cpp:140
Gecode::IntSet d(v, 7)
void sequence(Home home, const IntVarArgs &x, const IntSet &s, int q, int l, int u, IntConLevel)
Post propagator for .
Definition: sequence.cpp:51
void argmax(Home home, const IntVarArgs &x, IntVar y, bool tiebreak, IntConLevel)
Post propagator for .
Definition: arithmetic.cpp:114
Gecode::FloatVal c(-8, 8)
int p
Number of positive literals for node type.
Definition: bool-expr.cpp:236
const FloatNum min
Smallest allowed float value.
Definition: float.hh:833
Gecode::IntArgs i(4, 1, 2, 3, 4)
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:238
Equality ( )
Definition: int.hh:904
Options opt
The options.
Definition: test.cpp:101
IntRelType
Relation types for integers.
Definition: int.hh:903
NNF * r
Right subtree.
Definition: bool-expr.cpp:246
FloatRelType
Relation types for floats.
Definition: float.hh:1054
Less or equal ( )
Definition: set.hh:651
void clause(Home home, BoolOpType o, const BoolVarArgs &x, const BoolVarArgs &y, int n, IntConLevel)
Post domain consistent propagator for Boolean clause with positive variables x and negative variables...
Definition: bool.cpp:824
void sqrt(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition: arithmetic.cpp:110
void unshare(Home home, IntVarArgs &x, IntConLevel icl)
Replace multiple variable occurences in x by fresh variables.
Definition: unshare.cpp:133
Subset ( )
Definition: set.hh:647
void precede(Home home, const IntVarArgs &x, int s, int t, IntConLevel)
Post propagator that s precedes t in x.
Definition: precede.cpp:47
#define BOOL_OP(op)
Definition: registry.cpp:589
Intersection
Definition: set.hh:664
Less ( )
Definition: int.hh:907
void cumulatives(Home home, const IntVarArgs &m, const IntVarArgs &s, const IntVarArgs &p, const IntVarArgs &e, const IntVarArgs &u, const IntArgs &c, bool at_most, IntConLevel cl)
Post propagators for the cumulatives constraint.
Less ( )
Definition: set.hh:652
void element(Home home, IntSharedArray c, IntVar x0, IntVar x1, IntConLevel)
Post domain consistent propagator for .
Definition: element.cpp:43
Disjunction.
Definition: int.hh:918
void asin(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition: arithmetic.cpp:175
AST::Array * ann
Constraint annotations.
Definition: conexpr.hh:54
void sorted(Home home, const IntVarArgs &x, const IntVarArgs &y, const IntVarArgs &z, IntConLevel)
Post propagator that y is x sorted in increasing order.
Definition: sorted.cpp:43
Equality ( )
Definition: float.hh:1055
static const IntSet empty
Empty set.
Definition: int.hh:262
LinIntExpr cardinality(const SetExpr &e)
Cardinality of set expression.
Definition: set-expr.cpp:815
union Gecode::@518::NNF::@57 u
Union depending on nodetype t.
const int v[7]
Definition: distinct.cpp:207
void min(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:75
void extensional(Home home, const IntVarArgs &x, DFA dfa, IntConLevel)
Post domain consistent propagator for extensional constraint described by a DFA.
Definition: extensional.cpp:45
void cos(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition: arithmetic.cpp:196
Union.
Definition: set.hh:662
BoolVar expr(Home home, const BoolExpr &e, IntConLevel icl)
Post Boolean expression and return its value.
Definition: bool-expr.cpp:632
void div(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:135
Node * x
Pointer to corresponding Boolean expression node.
Definition: bool-expr.cpp:253
void tan(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition: arithmetic.cpp:210
void count(Home home, const IntVarArgs &x, int n, IntRelType irt, int m, IntConLevel)
Post propagator for .
Definition: count.cpp:44
Disjoint union.
Definition: set.hh:663
void convex(Home home, SetVar x)
Post propagator that propagates that x is convex.
Definition: convex.cpp:45
void rel(Home home, FloatVar x0, FloatRelType frt, FloatVal n)
Propagates .
Definition: rel.cpp:47
Exception class for FlatZinc errors
Definition: flatzinc.hh:591
The default consistency for a constraint.
Definition: int.hh:941
void weights(Home home, IntSharedArray elements, IntSharedArray weights, SetVar x, IntVar y)
Post propagator for .
Definition: int.cpp:179
Equality ( )
Definition: set.hh:645
Disjoint ( )
Definition: set.hh:649
void distinct(Home home, const IntVarArgs &x, IntConLevel icl)
Post propagator for for all .
Definition: distinct.cpp:47
void add(const std::string &id, poster p)
Add posting function p with identifier id.
Definition: registry.cpp:73
#define BOOL_ARRAY_OP(op)
Definition: registry.cpp:598
A space that can be initialized with a FlatZinc model.
Definition: flatzinc.hh:371
void binpacking(Home home, const IntVarArgs &l, const IntVarArgs &b, const IntArgs &s, IntConLevel)
Post propagator for bin packing.
Definition: bin-packing.cpp:45
Bounds propagation or consistency.
Definition: int.hh:939
Disequality ( )
Definition: set.hh:646
void nooverlap(Home home, const IntVarArgs &x, const IntArgs &w, const IntVarArgs &y, const IntArgs &h, IntConLevel)
Post propagator for rectangle packing.
Definition: no-overlap.cpp:55
struct Gecode::@518::NNF::@57::@58 b
For binary nodes (and, or, eqv)
Gecode toplevel namespace
Implication for reification.
Definition: int.hh:840
void sin(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition: arithmetic.cpp:182
Disequality ( )
Definition: int.hh:905
void acos(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition: arithmetic.cpp:189
void exp(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition: arithmetic.cpp:144
void circuit(Home home, int offset, const IntVarArgs &x, IntConLevel icl)
Post propagator such that x forms a circuit.
Definition: circuit.cpp:45
ReifyMode
Mode for reification.
Definition: int.hh:826
void nvalues(Home home, const IntVarArgs &x, IntRelType irt, int y, IntConLevel)
Post propagator for .
Definition: nvalues.cpp:44
void member(Home home, const IntVarArgs &x, IntVar y, IntConLevel)
Post domain consistent propagator for .
Definition: member.cpp:43
struct Gecode::@518::NNF::@57::@59 a
For atomic nodes.
Domain propagation or consistency.
Definition: int.hh:940
#define P_FLOAT_OP(Op)
Definition: registry.cpp:2091
void unary(Home home, const IntVarArgs &s, const IntArgs &p, IntConLevel icl)
Post propagators for scheduling tasks on unary resources.
Definition: unary.cpp:48
Registry & registry(void)
Return global registry object.
Definition: registry.cpp:57
void atan(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition: arithmetic.cpp:203
std::string id
Identifier for the constraint.
Definition: conexpr.hh:50
T * a
Element array.
Definition: array.hpp:528
bool neg
Is atomic formula negative.
Definition: bool-expr.cpp:251
Equivalence for reification (default)
Definition: int.hh:833
Abstract representation of a constraint.
Definition: conexpr.hh:47