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