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