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