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