Generated on Sat Oct 20 2018 12:43:45 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  * 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  argmin(s, iv, s.arg2IntVar(ce[1]), true, s.ann2ipl(ann));
1026  }
1027 
1028  void p_maximum_arg(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1029  IntVarArgs iv = s.arg2intvarargs(ce[0]);
1030  argmax(s, iv, s.arg2IntVar(ce[1]), true, s.ann2ipl(ann));
1031  }
1032 
1033  void p_regular(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1034  IntVarArgs iv = s.arg2intvarargs(ce[0]);
1035  int q = ce[1]->getInt();
1036  int symbols = ce[2]->getInt();
1037  IntArgs d = s.arg2intargs(ce[3]);
1038  int q0 = ce[4]->getInt();
1039 
1040  int noOfTrans = 0;
1041  for (int i=1; i<=q; i++) {
1042  for (int j=1; j<=symbols; j++) {
1043  if (d[(i-1)*symbols+(j-1)] > 0)
1044  noOfTrans++;
1045  }
1046  }
1047 
1048  Region re;
1049  DFA::Transition* t = re.alloc<DFA::Transition>(noOfTrans+1);
1050  noOfTrans = 0;
1051  for (int i=1; i<=q; i++) {
1052  for (int j=1; j<=symbols; j++) {
1053  if (d[(i-1)*symbols+(j-1)] > 0) {
1054  t[noOfTrans].i_state = i;
1055  t[noOfTrans].symbol = j;
1056  t[noOfTrans].o_state = d[(i-1)*symbols+(j-1)];
1057  noOfTrans++;
1058  }
1059  }
1060  }
1061  t[noOfTrans].i_state = -1;
1062 
1063  // Final states
1064  AST::SetLit* sl = ce[5]->getSet();
1065  int* f;
1066  if (sl->interval) {
1067  f = static_cast<int*>(heap.ralloc(sizeof(int)*(sl->max-sl->min+2)));
1068  for (int i=sl->min; i<=sl->max; i++)
1069  f[i-sl->min] = i;
1070  f[sl->max-sl->min+1] = -1;
1071  } else {
1072  f = static_cast<int*>(heap.ralloc(sizeof(int)*(sl->s.size()+1)));
1073  for (int j=sl->s.size(); j--; )
1074  f[j] = sl->s[j];
1075  f[sl->s.size()] = -1;
1076  }
1077 
1078  DFA dfa(q0,t,f);
1079  free(f);
1080  unshare(s, iv);
1081  extensional(s, iv, s.getSharedDFA(dfa), s.ann2ipl(ann));
1082  }
1083 
1084  void
1085  p_sort(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1086  IntVarArgs x = s.arg2intvarargs(ce[0]);
1087  IntVarArgs y = s.arg2intvarargs(ce[1]);
1088  IntVarArgs xy(x.size()+y.size());
1089  for (int i=x.size(); i--;)
1090  xy[i] = x[i];
1091  for (int i=y.size(); i--;)
1092  xy[i+x.size()] = y[i];
1093  unshare(s, xy);
1094  for (int i=x.size(); i--;)
1095  x[i] = xy[i];
1096  for (int i=y.size(); i--;)
1097  y[i] = xy[i+x.size()];
1098  sorted(s, x, y, s.ann2ipl(ann));
1099  }
1100 
1101  void
1102  p_inverse_offsets(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1103  IntVarArgs x = s.arg2intvarargs(ce[0]);
1104  unshare(s, x);
1105  int xoff = ce[1]->getInt();
1106  IntVarArgs y = s.arg2intvarargs(ce[2]);
1107  unshare(s, y);
1108  int yoff = ce[3]->getInt();
1109  channel(s, x, xoff, y, yoff, s.ann2ipl(ann));
1110  }
1111 
1112  void
1113  p_increasing_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1114  IntVarArgs x = s.arg2intvarargs(ce[0]);
1115  rel(s,x,IRT_LQ,s.ann2ipl(ann));
1116  }
1117 
1118  void
1119  p_increasing_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1120  BoolVarArgs x = s.arg2boolvarargs(ce[0]);
1121  rel(s,x,IRT_LQ,s.ann2ipl(ann));
1122  }
1123 
1124  void
1125  p_decreasing_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1126  IntVarArgs x = s.arg2intvarargs(ce[0]);
1127  rel(s,x,IRT_GQ,s.ann2ipl(ann));
1128  }
1129 
1130  void
1131  p_decreasing_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1132  BoolVarArgs x = s.arg2boolvarargs(ce[0]);
1133  rel(s,x,IRT_GQ,s.ann2ipl(ann));
1134  }
1135 
1136  void
1137  p_table_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1138  IntVarArgs x = s.arg2intvarargs(ce[0]);
1139  IntArgs tuples = s.arg2intargs(ce[1]);
1140  TupleSet ts = s.arg2tupleset(tuples,x.size());
1141  extensional(s,x,ts,s.ann2ipl(ann));
1142  }
1143 
1144  void
1145  p_table_int_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1146  IntVarArgs x = s.arg2intvarargs(ce[0]);
1147  IntArgs tuples = s.arg2intargs(ce[1]);
1148  TupleSet ts = s.arg2tupleset(tuples,x.size());
1149  extensional(s,x,ts,Reify(s.arg2BoolVar(ce[2]),RM_EQV),s.ann2ipl(ann));
1150  }
1151 
1152  void
1153  p_table_int_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1154  IntVarArgs x = s.arg2intvarargs(ce[0]);
1155  IntArgs tuples = s.arg2intargs(ce[1]);
1156  TupleSet ts = s.arg2tupleset(tuples,x.size());
1157  extensional(s,x,ts,Reify(s.arg2BoolVar(ce[2]),RM_IMP),s.ann2ipl(ann));
1158  }
1159 
1160  void
1161  p_table_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1162  BoolVarArgs x = s.arg2boolvarargs(ce[0]);
1163  IntArgs tuples = s.arg2boolargs(ce[1]);
1164  TupleSet ts = s.arg2tupleset(tuples,x.size());
1165  extensional(s,x,ts,s.ann2ipl(ann));
1166  }
1167 
1168  void
1169  p_table_bool_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1170  BoolVarArgs x = s.arg2boolvarargs(ce[0]);
1171  IntArgs tuples = s.arg2boolargs(ce[1]);
1172  TupleSet ts = s.arg2tupleset(tuples,x.size());
1173  extensional(s,x,ts,Reify(s.arg2BoolVar(ce[2]),RM_EQV),s.ann2ipl(ann));
1174  }
1175 
1176  void
1177  p_table_bool_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1178  BoolVarArgs x = s.arg2boolvarargs(ce[0]);
1179  IntArgs tuples = s.arg2boolargs(ce[1]);
1180  TupleSet ts = s.arg2tupleset(tuples,x.size());
1181  extensional(s,x,ts,Reify(s.arg2BoolVar(ce[2]),RM_IMP),s.ann2ipl(ann));
1182  }
1183 
1184  void p_cumulative_opt(FlatZincSpace& s, const ConExpr& ce,
1185  AST::Node* ann) {
1186  IntVarArgs start = s.arg2intvarargs(ce[0]);
1187  IntArgs duration = s.arg2intargs(ce[1]);
1188  IntArgs height = s.arg2intargs(ce[2]);
1189  BoolVarArgs opt = s.arg2boolvarargs(ce[3]);
1190  int bound = ce[4]->getInt();
1191  unshare(s,start);
1192  cumulative(s,bound,start,duration,height,opt,s.ann2ipl(ann));
1193  }
1194 
1195  void p_cumulatives(FlatZincSpace& s, const ConExpr& ce,
1196  AST::Node* ann) {
1197  IntVarArgs start = s.arg2intvarargs(ce[0]);
1198  IntVarArgs duration = s.arg2intvarargs(ce[1]);
1199  IntVarArgs height = s.arg2intvarargs(ce[2]);
1200  int n = start.size();
1201  IntVar bound = s.arg2IntVar(ce[3]);
1202 
1203  if (n==0)
1204  return;
1205 
1206  if (n == 1) {
1207  rel(s, height[0] <= bound);
1208  return;
1209  }
1210 
1211  int minHeight = std::min(height[0].min(),height[1].min());
1212  int minHeight2 = std::max(height[0].min(),height[1].min());
1213  for (int i=2; i<n; i++) {
1214  if (height[i].min() < minHeight) {
1215  minHeight2 = minHeight;
1216  minHeight = height[i].min();
1217  } else if (height[i].min() < minHeight2) {
1218  minHeight2 = height[i].min();
1219  }
1220  }
1221  bool disjunctive =
1222  (minHeight > bound.max()/2) ||
1223  (minHeight2 > bound.max()/2 && minHeight+minHeight2>bound.max());
1224  if (disjunctive) {
1225  rel(s, bound >= max(height));
1226  // Unary
1227  if (duration.assigned()) {
1228  IntArgs durationI(n);
1229  for (int i=n; i--;)
1230  durationI[i] = duration[i].val();
1231  unshare(s,start);
1232  unary(s,start,durationI);
1233  } else {
1234  IntVarArgs end(n);
1235  for (int i=n; i--;)
1236  end[i] = expr(s,start[i]+duration[i]);
1237  unshare(s,start);
1238  unary(s,start,duration,end);
1239  }
1240  } else if (height.assigned()) {
1241  IntArgs heightI(n);
1242  for (int i=n; i--;)
1243  heightI[i] = height[i].val();
1244  if (duration.assigned()) {
1245  IntArgs durationI(n);
1246  for (int i=n; i--;)
1247  durationI[i] = duration[i].val();
1248  cumulative(s, bound, start, durationI, heightI);
1249  } else {
1250  IntVarArgs end(n);
1251  for (int i = n; i--; )
1252  end[i] = expr(s,start[i]+duration[i]);
1253  cumulative(s, bound, start, duration, end, heightI);
1254  }
1255  } else if (bound.assigned()) {
1256  IntArgs machine = IntArgs::create(n,0,0);
1257  IntArgs limit({bound.val()});
1258  IntVarArgs end(n);
1259  for (int i=n; i--;)
1260  end[i] = expr(s,start[i]+duration[i]);
1261  cumulatives(s, machine, start, duration, end, height, limit, true,
1262  s.ann2ipl(ann));
1263  } else {
1266  IntVarArgs end(start.size());
1267  for (int i = start.size(); i--; ) {
1268  min = std::min(min, start[i].min());
1269  max = std::max(max, start[i].max() + duration[i].max());
1270  end[i] = expr(s, start[i] + duration[i]);
1271  }
1272  for (int time = min; time < max; ++time) {
1273  IntVarArgs x(start.size());
1274  for (int i = start.size(); i--; ) {
1275  IntVar overlaps = channel(s, expr(s, (start[i] <= time) &&
1276  (time < end[i])));
1277  x[i] = expr(s, overlaps * height[i]);
1278  }
1279  linear(s, x, IRT_LQ, bound);
1280  }
1281  }
1282  }
1283 
1284  void p_among_seq_int(FlatZincSpace& s, const ConExpr& ce,
1285  AST::Node* ann) {
1286  IntVarArgs x = s.arg2intvarargs(ce[0]);
1287  IntSet S = s.arg2intset(ce[1]);
1288  int q = ce[2]->getInt();
1289  int l = ce[3]->getInt();
1290  int u = ce[4]->getInt();
1291  unshare(s, x);
1292  sequence(s, x, S, q, l, u, s.ann2ipl(ann));
1293  }
1294 
1295  void p_among_seq_bool(FlatZincSpace& s, const ConExpr& ce,
1296  AST::Node* ann) {
1297  BoolVarArgs x = s.arg2boolvarargs(ce[0]);
1298  bool val = ce[1]->getBool();
1299  int q = ce[2]->getInt();
1300  int l = ce[3]->getInt();
1301  int u = ce[4]->getInt();
1302  IntSet S(val, val);
1303  unshare(s, x);
1304  sequence(s, x, S, q, l, u, s.ann2ipl(ann));
1305  }
1306 
1307  void p_schedule_unary(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
1308  IntVarArgs x = s.arg2intvarargs(ce[0]);
1309  IntArgs p = s.arg2intargs(ce[1]);
1310  unshare(s,x);
1311  unary(s, x, p);
1312  }
1313 
1314  void p_schedule_unary_optional(FlatZincSpace& s, const ConExpr& ce,
1315  AST::Node*) {
1316  IntVarArgs x = s.arg2intvarargs(ce[0]);
1317  IntArgs p = s.arg2intargs(ce[1]);
1318  BoolVarArgs m = s.arg2boolvarargs(ce[2]);
1319  unshare(s,x);
1320  unary(s, x, p, m);
1321  }
1322 
1323  void p_circuit(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
1324  int off = ce[0]->getInt();
1325  IntVarArgs xv = s.arg2intvarargs(ce[1]);
1326  unshare(s,xv);
1327  circuit(s,off,xv,s.ann2ipl(ann));
1328  }
1329  void p_circuit_cost_array(FlatZincSpace& s, const ConExpr& ce,
1330  AST::Node *ann) {
1331  IntArgs c = s.arg2intargs(ce[0]);
1332  IntVarArgs xv = s.arg2intvarargs(ce[1]);
1333  IntVarArgs yv = s.arg2intvarargs(ce[2]);
1334  IntVar z = s.arg2IntVar(ce[3]);
1335  unshare(s,xv);
1336  circuit(s,c,xv,yv,z,s.ann2ipl(ann));
1337  }
1338  void p_circuit_cost(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
1339  IntArgs c = s.arg2intargs(ce[0]);
1340  IntVarArgs xv = s.arg2intvarargs(ce[1]);
1341  IntVar z = s.arg2IntVar(ce[2]);
1342  unshare(s,xv);
1343  circuit(s,c,xv,z,s.ann2ipl(ann));
1344  }
1345 
1346  void p_nooverlap(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
1347  IntVarArgs x0 = s.arg2intvarargs(ce[0]);
1348  IntVarArgs w = s.arg2intvarargs(ce[1]);
1349  IntVarArgs y0 = s.arg2intvarargs(ce[2]);
1350  IntVarArgs h = s.arg2intvarargs(ce[3]);
1351  if (w.assigned() && h.assigned()) {
1352  IntArgs iw(w.size());
1353  for (int i=w.size(); i--;)
1354  iw[i] = w[i].val();
1355  IntArgs ih(h.size());
1356  for (int i=h.size(); i--;)
1357  ih[i] = h[i].val();
1358  nooverlap(s,x0,iw,y0,ih,s.ann2ipl(ann));
1359 
1360  int miny = y0[0].min();
1361  int maxy = y0[0].max();
1362  int maxdy = ih[0];
1363  for (int i=1; i<y0.size(); i++) {
1364  miny = std::min(miny,y0[i].min());
1365  maxy = std::max(maxy,y0[i].max());
1366  maxdy = std::max(maxdy,ih[i]);
1367  }
1368  int minx = x0[0].min();
1369  int maxx = x0[0].max();
1370  int maxdx = iw[0];
1371  for (int i=1; i<x0.size(); i++) {
1372  minx = std::min(minx,x0[i].min());
1373  maxx = std::max(maxx,x0[i].max());
1374  maxdx = std::max(maxdx,iw[i]);
1375  }
1376  if (miny > Int::Limits::min && maxy < Int::Limits::max) {
1377  cumulative(s,maxdy+maxy-miny,x0,iw,ih);
1378  cumulative(s,maxdx+maxx-minx,y0,ih,iw);
1379  }
1380  } else {
1381  IntVarArgs x1(x0.size()), y1(y0.size());
1382  for (int i=x0.size(); i--; )
1383  x1[i] = expr(s, x0[i] + w[i]);
1384  for (int i=y0.size(); i--; )
1385  y1[i] = expr(s, y0[i] + h[i]);
1386  nooverlap(s,x0,w,x1,y0,h,y1,s.ann2ipl(ann));
1387  }
1388  }
1389 
1390  void p_precede(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1391  IntVarArgs x = s.arg2intvarargs(ce[0]);
1392  int p_s = ce[1]->getInt();
1393  int p_t = ce[2]->getInt();
1394  precede(s,x,p_s,p_t,s.ann2ipl(ann));
1395  }
1396 
1397  void p_nvalue(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1398  IntVarArgs x = s.arg2intvarargs(ce[1]);
1399  if (ce[0]->isIntVar()) {
1400  IntVar y = s.arg2IntVar(ce[0]);
1401  nvalues(s,x,IRT_EQ,y,s.ann2ipl(ann));
1402  } else {
1403  nvalues(s,x,IRT_EQ,ce[0]->getInt(),s.ann2ipl(ann));
1404  }
1405  }
1406 
1407  void p_among(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1408  IntVarArgs x = s.arg2intvarargs(ce[1]);
1409  IntSet v = s.arg2intset(ce[2]);
1410  if (ce[0]->isIntVar()) {
1411  IntVar n = s.arg2IntVar(ce[0]);
1412  unshare(s, x);
1413  count(s,x,v,IRT_EQ,n,s.ann2ipl(ann));
1414  } else {
1415  unshare(s, x);
1416  count(s,x,v,IRT_EQ,ce[0]->getInt(),s.ann2ipl(ann));
1417  }
1418  }
1419 
1420  void p_member_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1421  IntVarArgs x = s.arg2intvarargs(ce[0]);
1422  IntVar y = s.arg2IntVar(ce[1]);
1423  member(s,x,y,s.ann2ipl(ann));
1424  }
1425  void p_member_int_reif(FlatZincSpace& s, const ConExpr& ce,
1426  AST::Node* ann) {
1427  IntVarArgs x = s.arg2intvarargs(ce[0]);
1428  IntVar y = s.arg2IntVar(ce[1]);
1429  BoolVar b = s.arg2BoolVar(ce[2]);
1430  member(s,x,y,b,s.ann2ipl(ann));
1431  }
1432  void p_member_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1433  BoolVarArgs x = s.arg2boolvarargs(ce[0]);
1434  BoolVar y = s.arg2BoolVar(ce[1]);
1435  member(s,x,y,s.ann2ipl(ann));
1436  }
1437  void p_member_bool_reif(FlatZincSpace& s, const ConExpr& ce,
1438  AST::Node* ann) {
1439  BoolVarArgs x = s.arg2boolvarargs(ce[0]);
1440  BoolVar y = s.arg2BoolVar(ce[1]);
1441  member(s,x,y,s.arg2BoolVar(ce[2]),s.ann2ipl(ann));
1442  }
1443 
1444  class IntPoster {
1445  public:
1446  IntPoster(void) {
1447  registry().add("all_different_int", &p_distinct);
1448  registry().add("all_different_offset", &p_distinctOffset);
1449  registry().add("all_equal_int", &p_all_equal);
1450  registry().add("int_eq", &p_int_eq);
1451  registry().add("int_ne", &p_int_ne);
1452  registry().add("int_ge", &p_int_ge);
1453  registry().add("int_gt", &p_int_gt);
1454  registry().add("int_le", &p_int_le);
1455  registry().add("int_lt", &p_int_lt);
1456  registry().add("int_eq_reif", &p_int_eq_reif);
1457  registry().add("int_ne_reif", &p_int_ne_reif);
1458  registry().add("int_ge_reif", &p_int_ge_reif);
1459  registry().add("int_gt_reif", &p_int_gt_reif);
1460  registry().add("int_le_reif", &p_int_le_reif);
1461  registry().add("int_lt_reif", &p_int_lt_reif);
1462  registry().add("int_eq_imp", &p_int_eq_imp);
1463  registry().add("int_ne_imp", &p_int_ne_imp);
1464  registry().add("int_ge_imp", &p_int_ge_imp);
1465  registry().add("int_gt_imp", &p_int_gt_imp);
1466  registry().add("int_le_imp", &p_int_le_imp);
1467  registry().add("int_lt_imp", &p_int_lt_imp);
1468  registry().add("int_lin_eq", &p_int_lin_eq);
1469  registry().add("int_lin_eq_reif", &p_int_lin_eq_reif);
1470  registry().add("int_lin_eq_imp", &p_int_lin_eq_imp);
1471  registry().add("int_lin_ne", &p_int_lin_ne);
1472  registry().add("int_lin_ne_reif", &p_int_lin_ne_reif);
1473  registry().add("int_lin_ne_imp", &p_int_lin_ne_imp);
1474  registry().add("int_lin_le", &p_int_lin_le);
1475  registry().add("int_lin_le_reif", &p_int_lin_le_reif);
1476  registry().add("int_lin_le_imp", &p_int_lin_le_imp);
1477  registry().add("int_lin_lt", &p_int_lin_lt);
1478  registry().add("int_lin_lt_reif", &p_int_lin_lt_reif);
1479  registry().add("int_lin_lt_imp", &p_int_lin_lt_imp);
1480  registry().add("int_lin_ge", &p_int_lin_ge);
1481  registry().add("int_lin_ge_reif", &p_int_lin_ge_reif);
1482  registry().add("int_lin_ge_imp", &p_int_lin_ge_imp);
1483  registry().add("int_lin_gt", &p_int_lin_gt);
1484  registry().add("int_lin_gt_reif", &p_int_lin_gt_reif);
1485  registry().add("int_lin_gt_imp", &p_int_lin_gt_imp);
1486  registry().add("int_plus", &p_int_plus);
1487  registry().add("int_minus", &p_int_minus);
1488  registry().add("int_times", &p_int_times);
1489  registry().add("gecode_int_pow", &p_int_pow);
1490  registry().add("int_div", &p_int_div);
1491  registry().add("int_mod", &p_int_mod);
1492  registry().add("int_min", &p_int_min);
1493  registry().add("int_max", &p_int_max);
1494  registry().add("int_abs", &p_abs);
1495  registry().add("int_negate", &p_int_negate);
1496  registry().add("bool_eq", &p_bool_eq);
1497  registry().add("bool_eq_reif", &p_bool_eq_reif);
1498  registry().add("bool_eq_imp", &p_bool_eq_imp);
1499  registry().add("bool_ne", &p_bool_ne);
1500  registry().add("bool_ne_reif", &p_bool_ne_reif);
1501  registry().add("bool_ne_imp", &p_bool_ne_imp);
1502  registry().add("bool_ge", &p_bool_ge);
1503  registry().add("bool_ge_reif", &p_bool_ge_reif);
1504  registry().add("bool_ge_imp", &p_bool_ge_imp);
1505  registry().add("bool_le", &p_bool_le);
1506  registry().add("bool_le_reif", &p_bool_le_reif);
1507  registry().add("bool_le_imp", &p_bool_le_imp);
1508  registry().add("bool_gt", &p_bool_gt);
1509  registry().add("bool_gt_reif", &p_bool_gt_reif);
1510  registry().add("bool_gt_imp", &p_bool_gt_imp);
1511  registry().add("bool_lt", &p_bool_lt);
1512  registry().add("bool_lt_reif", &p_bool_lt_reif);
1513  registry().add("bool_lt_imp", &p_bool_lt_imp);
1514  registry().add("bool_or", &p_bool_or);
1515  registry().add("bool_or_imp", &p_bool_or_imp);
1516  registry().add("bool_and", &p_bool_and);
1517  registry().add("bool_and_imp", &p_bool_and_imp);
1518  registry().add("bool_xor", &p_bool_xor);
1519  registry().add("bool_xor_imp", &p_bool_xor_imp);
1520  registry().add("array_bool_and", &p_array_bool_and);
1521  registry().add("array_bool_and_imp", &p_array_bool_and_imp);
1522  registry().add("array_bool_or", &p_array_bool_or);
1523  registry().add("array_bool_or_imp", &p_array_bool_or_imp);
1524  registry().add("array_bool_xor", &p_array_bool_xor);
1525  registry().add("array_bool_xor_imp", &p_array_bool_xor_imp);
1526  registry().add("bool_clause", &p_array_bool_clause);
1527  registry().add("bool_clause_reif", &p_array_bool_clause_reif);
1528  registry().add("bool_clause_imp", &p_array_bool_clause_imp);
1529  registry().add("bool_left_imp", &p_bool_l_imp);
1530  registry().add("bool_right_imp", &p_bool_r_imp);
1531  registry().add("bool_not", &p_bool_not);
1532  registry().add("array_int_element", &p_array_int_element);
1533  registry().add("array_var_int_element", &p_array_int_element);
1534  registry().add("array_bool_element", &p_array_bool_element);
1535  registry().add("array_var_bool_element", &p_array_bool_element);
1536  registry().add("bool2int", &p_bool2int);
1537  registry().add("int_in", &p_int_in);
1538  registry().add("int_in_reif", &p_int_in_reif);
1539  registry().add("int_in_imp", &p_int_in_imp);
1540 #ifndef GECODE_HAS_SET_VARS
1541  registry().add("set_in", &p_int_in);
1542  registry().add("set_in_reif", &p_int_in_reif);
1543  registry().add("set_in_imp", &p_int_in_imp);
1544 #endif
1545 
1546  registry().add("array_int_lt", &p_array_int_lt);
1547  registry().add("array_int_lq", &p_array_int_lq);
1548  registry().add("array_bool_lt", &p_array_bool_lt);
1549  registry().add("array_bool_lq", &p_array_bool_lq);
1550  registry().add("count", &p_count);
1551  registry().add("count_reif", &p_count_reif);
1552  registry().add("count_imp", &p_count_imp);
1553  registry().add("at_least_int", &p_at_least);
1554  registry().add("at_most_int", &p_at_most);
1555  registry().add("gecode_bin_packing_load", &p_bin_packing_load);
1556  registry().add("gecode_global_cardinality", &p_global_cardinality);
1557  registry().add("gecode_global_cardinality_closed",
1558  &p_global_cardinality_closed);
1559  registry().add("global_cardinality_low_up",
1560  &p_global_cardinality_low_up);
1561  registry().add("global_cardinality_low_up_closed",
1562  &p_global_cardinality_low_up_closed);
1563  registry().add("array_int_minimum", &p_minimum);
1564  registry().add("array_int_maximum", &p_maximum);
1565  registry().add("gecode_minimum_arg_int", &p_minimum_arg);
1566  registry().add("gecode_maximum_arg_int", &p_maximum_arg);
1567  registry().add("array_int_maximum", &p_maximum);
1568  registry().add("gecode_regular", &p_regular);
1569  registry().add("sort", &p_sort);
1570  registry().add("inverse_offsets", &p_inverse_offsets);
1571  registry().add("increasing_int", &p_increasing_int);
1572  registry().add("increasing_bool", &p_increasing_bool);
1573  registry().add("decreasing_int", &p_decreasing_int);
1574  registry().add("decreasing_bool", &p_decreasing_bool);
1575  registry().add("gecode_table_int", &p_table_int);
1576  registry().add("gecode_table_int_reif", &p_table_int_reif);
1577  registry().add("gecode_table_int_imp", &p_table_int_imp);
1578  registry().add("gecode_table_bool", &p_table_bool);
1579  registry().add("gecode_table_bool_reif", &p_table_bool_reif);
1580  registry().add("gecode_table_bool_imp", &p_table_bool_imp);
1581  registry().add("cumulatives", &p_cumulatives);
1582  registry().add("gecode_among_seq_int", &p_among_seq_int);
1583  registry().add("gecode_among_seq_bool", &p_among_seq_bool);
1584 
1585  registry().add("bool_lin_eq", &p_bool_lin_eq);
1586  registry().add("bool_lin_ne", &p_bool_lin_ne);
1587  registry().add("bool_lin_le", &p_bool_lin_le);
1588  registry().add("bool_lin_lt", &p_bool_lin_lt);
1589  registry().add("bool_lin_ge", &p_bool_lin_ge);
1590  registry().add("bool_lin_gt", &p_bool_lin_gt);
1591 
1592  registry().add("bool_lin_eq_reif", &p_bool_lin_eq_reif);
1593  registry().add("bool_lin_eq_imp", &p_bool_lin_eq_imp);
1594  registry().add("bool_lin_ne_reif", &p_bool_lin_ne_reif);
1595  registry().add("bool_lin_ne_imp", &p_bool_lin_ne_imp);
1596  registry().add("bool_lin_le_reif", &p_bool_lin_le_reif);
1597  registry().add("bool_lin_le_imp", &p_bool_lin_le_imp);
1598  registry().add("bool_lin_lt_reif", &p_bool_lin_lt_reif);
1599  registry().add("bool_lin_lt_imp", &p_bool_lin_lt_imp);
1600  registry().add("bool_lin_ge_reif", &p_bool_lin_ge_reif);
1601  registry().add("bool_lin_ge_imp", &p_bool_lin_ge_imp);
1602  registry().add("bool_lin_gt_reif", &p_bool_lin_gt_reif);
1603  registry().add("bool_lin_gt_imp", &p_bool_lin_gt_imp);
1604 
1605  registry().add("gecode_schedule_unary", &p_schedule_unary);
1606  registry().add("gecode_schedule_unary_optional", &p_schedule_unary_optional);
1607  registry().add("gecode_schedule_cumulative_optional", &p_cumulative_opt);
1608 
1609  registry().add("gecode_circuit", &p_circuit);
1610  registry().add("gecode_circuit_cost_array", &p_circuit_cost_array);
1611  registry().add("gecode_circuit_cost", &p_circuit_cost);
1612  registry().add("gecode_nooverlap", &p_nooverlap);
1613  registry().add("gecode_precede", &p_precede);
1614  registry().add("nvalue",&p_nvalue);
1615  registry().add("among",&p_among);
1616  registry().add("member_int",&p_member_int);
1617  registry().add("gecode_member_int_reif",&p_member_int_reif);
1618  registry().add("member_bool",&p_member_bool);
1619  registry().add("gecode_member_bool_reif",&p_member_bool_reif);
1620  }
1621  };
1622  IntPoster __int_poster;
1623 
1624 #ifdef GECODE_HAS_SET_VARS
1625  void p_set_OP(FlatZincSpace& s, SetOpType op,
1626  const ConExpr& ce, AST::Node *) {
1627  rel(s, s.arg2SetVar(ce[0]), op, s.arg2SetVar(ce[1]),
1628  SRT_EQ, s.arg2SetVar(ce[2]));
1629  }
1630  void p_set_union(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
1631  p_set_OP(s, SOT_UNION, ce, ann);
1632  }
1633  void p_set_intersect(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
1634  p_set_OP(s, SOT_INTER, ce, ann);
1635  }
1636  void p_set_diff(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
1637  p_set_OP(s, SOT_MINUS, ce, ann);
1638  }
1639 
1640  void p_set_symdiff(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
1641  SetVar x = s.arg2SetVar(ce[0]);
1642  SetVar y = s.arg2SetVar(ce[1]);
1643 
1644  SetVarLubRanges xub(x);
1645  IntSet xubs(xub);
1646  SetVar x_y(s,IntSet::empty,xubs);
1647  rel(s, x, SOT_MINUS, y, SRT_EQ, x_y);
1648 
1649  SetVarLubRanges yub(y);
1650  IntSet yubs(yub);
1651  SetVar y_x(s,IntSet::empty,yubs);
1652  rel(s, y, SOT_MINUS, x, SRT_EQ, y_x);
1653 
1654  rel(s, x_y, SOT_UNION, y_x, SRT_EQ, s.arg2SetVar(ce[2]));
1655  }
1656 
1657  void p_array_set_OP(FlatZincSpace& s, SetOpType op,
1658  const ConExpr& ce, AST::Node *) {
1659  SetVarArgs xs = s.arg2setvarargs(ce[0]);
1660  rel(s, op, xs, s.arg2SetVar(ce[1]));
1661  }
1662  void p_array_set_union(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
1663  p_array_set_OP(s, SOT_UNION, ce, ann);
1664  }
1665  void p_array_set_partition(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
1666  p_array_set_OP(s, SOT_DUNION, ce, ann);
1667  }
1668 
1669 
1670  void p_set_rel(FlatZincSpace& s, SetRelType srt, const ConExpr& ce) {
1671  rel(s, s.arg2SetVar(ce[0]), srt, s.arg2SetVar(ce[1]));
1672  }
1673 
1674  void p_set_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1675  p_set_rel(s, SRT_EQ, ce);
1676  }
1677  void p_set_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1678  p_set_rel(s, SRT_NQ, ce);
1679  }
1680  void p_set_subset(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1681  p_set_rel(s, SRT_SUB, ce);
1682  }
1683  void p_set_superset(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1684  p_set_rel(s, SRT_SUP, ce);
1685  }
1686  void p_set_le(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1687  p_set_rel(s, SRT_LQ, ce);
1688  }
1689  void p_set_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1690  p_set_rel(s, SRT_LE, ce);
1691  }
1692  void p_set_card(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1693  if (!ce[1]->isIntVar()) {
1694  cardinality(s, s.arg2SetVar(ce[0]), ce[1]->getInt(),
1695  ce[1]->getInt());
1696  } else {
1697  cardinality(s, s.arg2SetVar(ce[0]), s.arg2IntVar(ce[1]));
1698  }
1699  }
1700  void p_set_in(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1701  if (!ce[1]->isSetVar()) {
1702  IntSet d = s.arg2intset(ce[1]);
1703  if (ce[0]->isBoolVar()) {
1704  IntSetRanges dr(d);
1705  Iter::Ranges::Singleton sr(0,1);
1706  Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr);
1707  IntSet d01(i);
1708  if (d01.size() == 0) {
1709  s.fail();
1710  } else {
1711  rel(s, s.arg2BoolVar(ce[0]), IRT_GQ, d01.min());
1712  rel(s, s.arg2BoolVar(ce[0]), IRT_LQ, d01.max());
1713  }
1714  } else {
1715  dom(s, s.arg2IntVar(ce[0]), d);
1716  }
1717  } else {
1718  if (!ce[0]->isIntVar()) {
1719  dom(s, s.arg2SetVar(ce[1]), SRT_SUP, ce[0]->getInt());
1720  } else {
1721  rel(s, s.arg2SetVar(ce[1]), SRT_SUP, s.arg2IntVar(ce[0]));
1722  }
1723  }
1724  }
1725  void p_set_rel_reif(FlatZincSpace& s, SetRelType srt, const ConExpr& ce) {
1726  rel(s, s.arg2SetVar(ce[0]), srt, s.arg2SetVar(ce[1]),
1727  s.arg2BoolVar(ce[2]));
1728  }
1729 
1730  void p_set_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1731  p_set_rel_reif(s,SRT_EQ,ce);
1732  }
1733  void p_set_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1734  p_set_rel_reif(s,SRT_LQ,ce);
1735  }
1736  void p_set_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1737  p_set_rel_reif(s,SRT_LE,ce);
1738  }
1739  void p_set_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1740  p_set_rel_reif(s,SRT_NQ,ce);
1741  }
1742  void p_set_subset_reif(FlatZincSpace& s, const ConExpr& ce,
1743  AST::Node *) {
1744  p_set_rel_reif(s,SRT_SUB,ce);
1745  }
1746  void p_set_superset_reif(FlatZincSpace& s, const ConExpr& ce,
1747  AST::Node *) {
1748  p_set_rel_reif(s,SRT_SUP,ce);
1749  }
1750  void p_set_in_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann, ReifyMode rm) {
1751  if (!ce[1]->isSetVar()) {
1752  if (rm==RM_EQV) {
1753  p_int_in_reif(s,ce,ann);
1754  } else {
1755  assert(rm==RM_IMP);
1756  p_int_in_imp(s,ce,ann);
1757  }
1758  } else {
1759  if (!ce[0]->isIntVar()) {
1760  dom(s, s.arg2SetVar(ce[1]), SRT_SUP, ce[0]->getInt(),
1761  Reify(s.arg2BoolVar(ce[2]),rm));
1762  } else {
1763  rel(s, s.arg2SetVar(ce[1]), SRT_SUP, s.arg2IntVar(ce[0]),
1764  Reify(s.arg2BoolVar(ce[2]),rm));
1765  }
1766  }
1767  }
1768  void p_set_in_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1769  p_set_in_reif(s,ce,ann,RM_EQV);
1770  }
1771  void p_set_in_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1772  p_set_in_reif(s,ce,ann,RM_IMP);
1773  }
1774  void p_set_disjoint(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1775  rel(s, s.arg2SetVar(ce[0]), SRT_DISJ, s.arg2SetVar(ce[1]));
1776  }
1777 
1778  void p_link_set_to_booleans(FlatZincSpace& s, const ConExpr& ce,
1779  AST::Node *) {
1780  SetVar x = s.arg2SetVar(ce[0]);
1781  int idx = ce[2]->getInt();
1782  assert(idx >= 0);
1783  rel(s, x || IntSet(Set::Limits::min,idx-1));
1784  BoolVarArgs y = s.arg2boolvarargs(ce[1],idx);
1785  unshare(s, y);
1786  channel(s, y, x);
1787  }
1788 
1789  void p_array_set_element(FlatZincSpace& s, const ConExpr& ce,
1790  AST::Node*) {
1791  bool isConstant = true;
1792  AST::Array* a = ce[1]->getArray();
1793  for (int i=a->a.size(); i--;) {
1794  if (a->a[i]->isSetVar()) {
1795  isConstant = false;
1796  break;
1797  }
1798  }
1799  IntVar selector = s.arg2IntVar(ce[0]);
1800  rel(s, selector > 0);
1801  if (isConstant) {
1802  IntSetArgs sv = s.arg2intsetargs(ce[1],1);
1803  element(s, sv, selector, s.arg2SetVar(ce[2]));
1804  } else {
1805  SetVarArgs sv = s.arg2setvarargs(ce[1], 1);
1806  element(s, sv, selector, s.arg2SetVar(ce[2]));
1807  }
1808  }
1809 
1810  void p_array_set_element_op(FlatZincSpace& s, const ConExpr& ce,
1811  AST::Node*, SetOpType op,
1812  const IntSet& universe =
1814  bool isConstant = true;
1815  AST::Array* a = ce[1]->getArray();
1816  for (int i=a->a.size(); i--;) {
1817  if (a->a[i]->isSetVar()) {
1818  isConstant = false;
1819  break;
1820  }
1821  }
1822  SetVar selector = s.arg2SetVar(ce[0]);
1823  dom(s, selector, SRT_DISJ, 0);
1824  if (isConstant) {
1825  IntSetArgs sv = s.arg2intsetargs(ce[1], 1);
1826  element(s, op, sv, selector, s.arg2SetVar(ce[2]), universe);
1827  } else {
1828  SetVarArgs sv = s.arg2setvarargs(ce[1], 1);
1829  element(s, op, sv, selector, s.arg2SetVar(ce[2]), universe);
1830  }
1831  }
1832 
1833  void p_array_set_element_union(FlatZincSpace& s, const ConExpr& ce,
1834  AST::Node* ann) {
1835  p_array_set_element_op(s, ce, ann, SOT_UNION);
1836  }
1837 
1838  void p_array_set_element_intersect(FlatZincSpace& s, const ConExpr& ce,
1839  AST::Node* ann) {
1840  p_array_set_element_op(s, ce, ann, SOT_INTER);
1841  }
1842 
1843  void p_array_set_element_intersect_in(FlatZincSpace& s,
1844  const ConExpr& ce,
1845  AST::Node* ann) {
1846  IntSet d = s.arg2intset(ce[3]);
1847  p_array_set_element_op(s, ce, ann, SOT_INTER, d);
1848  }
1849 
1850  void p_array_set_element_partition(FlatZincSpace& s, const ConExpr& ce,
1851  AST::Node* ann) {
1852  p_array_set_element_op(s, ce, ann, SOT_DUNION);
1853  }
1854 
1855  void p_set_convex(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1856  convex(s, s.arg2SetVar(ce[0]));
1857  }
1858 
1859  void p_array_set_seq(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
1860  SetVarArgs sv = s.arg2setvarargs(ce[0]);
1861  sequence(s, sv);
1862  }
1863 
1864  void p_array_set_seq_union(FlatZincSpace& s, const ConExpr& ce,
1865  AST::Node *) {
1866  SetVarArgs sv = s.arg2setvarargs(ce[0]);
1867  sequence(s, sv, s.arg2SetVar(ce[1]));
1868  }
1869 
1870  void p_int_set_channel(FlatZincSpace& s, const ConExpr& ce,
1871  AST::Node *) {
1872  int xoff=ce[1]->getInt();
1873  assert(xoff >= 0);
1874  int yoff=ce[3]->getInt();
1875  assert(yoff >= 0);
1876  IntVarArgs xv = s.arg2intvarargs(ce[0], xoff);
1877  SetVarArgs yv = s.arg2setvarargs(ce[2], yoff, 1, IntSet(0, xoff-1));
1878  IntSet xd(yoff,yv.size()-1);
1879  for (int i=xoff; i<xv.size(); i++) {
1880  dom(s, xv[i], xd);
1881  }
1882  IntSet yd(xoff,xv.size()-1);
1883  for (int i=yoff; i<yv.size(); i++) {
1884  dom(s, yv[i], SRT_SUB, yd);
1885  }
1886  channel(s,xv,yv);
1887  }
1888 
1889  void p_range(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
1890  int xoff=ce[1]->getInt();
1891  assert(xoff >= 0);
1892  IntVarArgs xv = s.arg2intvarargs(ce[0],xoff);
1893  element(s, SOT_UNION, xv, s.arg2SetVar(ce[2]), s.arg2SetVar(ce[3]));
1894  }
1895 
1896  void p_weights(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
1897  IntArgs e = s.arg2intargs(ce[0]);
1898  IntArgs w = s.arg2intargs(ce[1]);
1899  SetVar x = s.arg2SetVar(ce[2]);
1900  IntVar y = s.arg2IntVar(ce[3]);
1901  weights(s,e,w,x,y);
1902  }
1903 
1904  void p_inverse_set(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
1905  int xoff = ce[2]->getInt();
1906  int yoff = ce[3]->getInt();
1907  SetVarArgs x = s.arg2setvarargs(ce[0],xoff);
1908  SetVarArgs y = s.arg2setvarargs(ce[1],yoff);
1909  channel(s, x, y);
1910  }
1911 
1912  void p_precede_set(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
1913  SetVarArgs x = s.arg2setvarargs(ce[0]);
1914  int p_s = ce[1]->getInt();
1915  int p_t = ce[2]->getInt();
1916  precede(s,x,p_s,p_t);
1917  }
1918 
1919  class SetPoster {
1920  public:
1921  SetPoster(void) {
1922  registry().add("set_eq", &p_set_eq);
1923  registry().add("set_le", &p_set_le);
1924  registry().add("set_lt", &p_set_lt);
1925  registry().add("equal", &p_set_eq);
1926  registry().add("set_ne", &p_set_ne);
1927  registry().add("set_union", &p_set_union);
1928  registry().add("array_set_element", &p_array_set_element);
1929  registry().add("array_var_set_element", &p_array_set_element);
1930  registry().add("set_intersect", &p_set_intersect);
1931  registry().add("set_diff", &p_set_diff);
1932  registry().add("set_symdiff", &p_set_symdiff);
1933  registry().add("set_subset", &p_set_subset);
1934  registry().add("set_superset", &p_set_superset);
1935  registry().add("set_card", &p_set_card);
1936  registry().add("set_in", &p_set_in);
1937  registry().add("set_eq_reif", &p_set_eq_reif);
1938  registry().add("set_le_reif", &p_set_le_reif);
1939  registry().add("set_lt_reif", &p_set_lt_reif);
1940  registry().add("equal_reif", &p_set_eq_reif);
1941  registry().add("set_ne_reif", &p_set_ne_reif);
1942  registry().add("set_subset_reif", &p_set_subset_reif);
1943  registry().add("set_superset_reif", &p_set_superset_reif);
1944  registry().add("set_in_reif", &p_set_in_reif);
1945  registry().add("set_in_imp", &p_set_in_imp);
1946  registry().add("disjoint", &p_set_disjoint);
1947  registry().add("gecode_link_set_to_booleans",
1948  &p_link_set_to_booleans);
1949 
1950  registry().add("array_set_union", &p_array_set_union);
1951  registry().add("array_set_partition", &p_array_set_partition);
1952  registry().add("set_convex", &p_set_convex);
1953  registry().add("array_set_seq", &p_array_set_seq);
1954  registry().add("array_set_seq_union", &p_array_set_seq_union);
1955  registry().add("gecode_array_set_element_union",
1956  &p_array_set_element_union);
1957  registry().add("gecode_array_set_element_intersect",
1958  &p_array_set_element_intersect);
1959  registry().add("gecode_array_set_element_intersect_in",
1960  &p_array_set_element_intersect_in);
1961  registry().add("gecode_array_set_element_partition",
1962  &p_array_set_element_partition);
1963  registry().add("gecode_int_set_channel",
1964  &p_int_set_channel);
1965  registry().add("gecode_range",
1966  &p_range);
1967  registry().add("gecode_set_weights",
1968  &p_weights);
1969  registry().add("gecode_inverse_set", &p_inverse_set);
1970  registry().add("gecode_precede_set", &p_precede_set);
1971  }
1972  };
1973  SetPoster __set_poster;
1974 #endif
1975 
1976 #ifdef GECODE_HAS_FLOAT_VARS
1977 
1978  void p_int2float(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
1979  IntVar x0 = s.arg2IntVar(ce[0]);
1980  FloatVar x1 = s.arg2FloatVar(ce[1]);
1981  channel(s, x0, x1);
1982  }
1983 
1984  void p_float_lin_cmp(FlatZincSpace& s, FloatRelType frt,
1985  const ConExpr& ce, AST::Node*) {
1986  FloatValArgs fa = s.arg2floatargs(ce[0]);
1987  FloatVarArgs fv = s.arg2floatvarargs(ce[1]);
1988  linear(s, fa, fv, frt, ce[2]->getFloat());
1989  }
1990  void p_float_lin_cmp_reif(FlatZincSpace& s, FloatRelType frt,
1991  const ConExpr& ce, AST::Node*) {
1992  FloatValArgs fa = s.arg2floatargs(ce[0]);
1993  FloatVarArgs fv = s.arg2floatvarargs(ce[1]);
1994  linear(s, fa, fv, frt, ce[2]->getFloat(), s.arg2BoolVar(ce[3]));
1995  }
1996  void p_float_lin_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
1997  p_float_lin_cmp(s,FRT_EQ,ce,ann);
1998  }
1999  void p_float_lin_eq_reif(FlatZincSpace& s, const ConExpr& ce,
2000  AST::Node* ann) {
2001  p_float_lin_cmp_reif(s,FRT_EQ,ce,ann);
2002  }
2003  void p_float_lin_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
2004  p_float_lin_cmp(s,FRT_LQ,ce,ann);
2005  }
2006  void p_float_lin_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
2007  p_float_lin_cmp(s,FRT_LE,ce,ann);
2008  }
2009  void p_float_lin_le_reif(FlatZincSpace& s, const ConExpr& ce,
2010  AST::Node* ann) {
2011  p_float_lin_cmp_reif(s,FRT_LQ,ce,ann);
2012  }
2013  void p_float_lin_lt_reif(FlatZincSpace& s, const ConExpr& ce,
2014  AST::Node* ann) {
2015  p_float_lin_cmp_reif(s,FRT_LE,ce,ann);
2016  }
2017 
2018  void p_float_times(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2019  FloatVar x = s.arg2FloatVar(ce[0]);
2020  FloatVar y = s.arg2FloatVar(ce[1]);
2021  FloatVar z = s.arg2FloatVar(ce[2]);
2022  mult(s,x,y,z);
2023  }
2024 
2025  void p_float_div(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2026  FloatVar x = s.arg2FloatVar(ce[0]);
2027  FloatVar y = s.arg2FloatVar(ce[1]);
2028  FloatVar z = s.arg2FloatVar(ce[2]);
2029  div(s,x,y,z);
2030  }
2031 
2032  void p_float_plus(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2033  FloatVar x = s.arg2FloatVar(ce[0]);
2034  FloatVar y = s.arg2FloatVar(ce[1]);
2035  FloatVar z = s.arg2FloatVar(ce[2]);
2036  rel(s,x+y==z);
2037  }
2038 
2039  void p_float_sqrt(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2040  FloatVar x = s.arg2FloatVar(ce[0]);
2041  FloatVar y = s.arg2FloatVar(ce[1]);
2042  sqrt(s,x,y);
2043  }
2044 
2045  void p_float_abs(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2046  FloatVar x = s.arg2FloatVar(ce[0]);
2047  FloatVar y = s.arg2FloatVar(ce[1]);
2048  abs(s,x,y);
2049  }
2050 
2051  void p_float_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2052  FloatVar x = s.arg2FloatVar(ce[0]);
2053  FloatVar y = s.arg2FloatVar(ce[1]);
2054  rel(s,x,FRT_EQ,y);
2055  }
2056  void p_float_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2057  FloatVar x = s.arg2FloatVar(ce[0]);
2058  FloatVar y = s.arg2FloatVar(ce[1]);
2059  BoolVar b = s.arg2BoolVar(ce[2]);
2060  rel(s,x,FRT_EQ,y,b);
2061  }
2062  void p_float_le(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2063  FloatVar x = s.arg2FloatVar(ce[0]);
2064  FloatVar y = s.arg2FloatVar(ce[1]);
2065  rel(s,x,FRT_LQ,y);
2066  }
2067  void p_float_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2068  FloatVar x = s.arg2FloatVar(ce[0]);
2069  FloatVar y = s.arg2FloatVar(ce[1]);
2070  BoolVar b = s.arg2BoolVar(ce[2]);
2071  rel(s,x,FRT_LQ,y,b);
2072  }
2073  void p_float_max(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2074  FloatVar x = s.arg2FloatVar(ce[0]);
2075  FloatVar y = s.arg2FloatVar(ce[1]);
2076  FloatVar z = s.arg2FloatVar(ce[2]);
2077  max(s,x,y,z);
2078  }
2079  void p_float_min(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2080  FloatVar x = s.arg2FloatVar(ce[0]);
2081  FloatVar y = s.arg2FloatVar(ce[1]);
2082  FloatVar z = s.arg2FloatVar(ce[2]);
2083  min(s,x,y,z);
2084  }
2085  void p_float_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2086  FloatVar x = s.arg2FloatVar(ce[0]);
2087  FloatVar y = s.arg2FloatVar(ce[1]);
2088  rel(s, x, FRT_LQ, y);
2089  rel(s, x, FRT_EQ, y, BoolVar(s,0,0));
2090  }
2091 
2092  void p_float_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2093  FloatVar x = s.arg2FloatVar(ce[0]);
2094  FloatVar y = s.arg2FloatVar(ce[1]);
2095  BoolVar b = s.arg2BoolVar(ce[2]);
2096  BoolVar b0(s,0,1);
2097  BoolVar b1(s,0,1);
2098  rel(s, b == (b0 && !b1));
2099  rel(s, x, FRT_LQ, y, b0);
2100  rel(s, x, FRT_EQ, y, b1);
2101  }
2102 
2103  void p_float_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2104  FloatVar x = s.arg2FloatVar(ce[0]);
2105  FloatVar y = s.arg2FloatVar(ce[1]);
2106  rel(s, x, FRT_EQ, y, BoolVar(s,0,0));
2107  }
2108 
2109 #ifdef GECODE_HAS_MPFR
2110 #define P_FLOAT_OP(Op) \
2111  void p_float_ ## Op (FlatZincSpace& s, const ConExpr& ce, AST::Node*) {\
2112  FloatVar x = s.arg2FloatVar(ce[0]);\
2113  FloatVar y = s.arg2FloatVar(ce[1]);\
2114  Op(s,x,y);\
2115  }
2116  P_FLOAT_OP(acos)
2117  P_FLOAT_OP(asin)
2118  P_FLOAT_OP(atan)
2119  P_FLOAT_OP(cos)
2120  P_FLOAT_OP(exp)
2121  P_FLOAT_OP(sin)
2122  P_FLOAT_OP(tan)
2123  // P_FLOAT_OP(sinh)
2124  // P_FLOAT_OP(tanh)
2125  // P_FLOAT_OP(cosh)
2126 #undef P_FLOAT_OP
2127 
2128  void p_float_ln(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2129  FloatVar x = s.arg2FloatVar(ce[0]);
2130  FloatVar y = s.arg2FloatVar(ce[1]);
2131  log(s,x,y);
2132  }
2133  void p_float_log10(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2134  FloatVar x = s.arg2FloatVar(ce[0]);
2135  FloatVar y = s.arg2FloatVar(ce[1]);
2136  log(s,10.0,x,y);
2137  }
2138  void p_float_log2(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
2139  FloatVar x = s.arg2FloatVar(ce[0]);
2140  FloatVar y = s.arg2FloatVar(ce[1]);
2141  log(s,2.0,x,y);
2142  }
2143 
2144 #endif
2145 
2146  class FloatPoster {
2147  public:
2148  FloatPoster(void) {
2149  registry().add("int2float",&p_int2float);
2150  registry().add("float_abs",&p_float_abs);
2151  registry().add("float_sqrt",&p_float_sqrt);
2152  registry().add("float_eq",&p_float_eq);
2153  registry().add("float_eq_reif",&p_float_eq_reif);
2154  registry().add("float_le",&p_float_le);
2155  registry().add("float_le_reif",&p_float_le_reif);
2156  registry().add("float_lt",&p_float_lt);
2157  registry().add("float_lt_reif",&p_float_lt_reif);
2158  registry().add("float_ne",&p_float_ne);
2159  registry().add("float_times",&p_float_times);
2160  registry().add("float_div",&p_float_div);
2161  registry().add("float_plus",&p_float_plus);
2162  registry().add("float_max",&p_float_max);
2163  registry().add("float_min",&p_float_min);
2164 
2165  registry().add("float_lin_eq",&p_float_lin_eq);
2166  registry().add("float_lin_eq_reif",&p_float_lin_eq_reif);
2167  registry().add("float_lin_le",&p_float_lin_le);
2168  registry().add("float_lin_lt",&p_float_lin_lt);
2169  registry().add("float_lin_le_reif",&p_float_lin_le_reif);
2170  registry().add("float_lin_lt_reif",&p_float_lin_lt_reif);
2171 
2172 #ifdef GECODE_HAS_MPFR
2173  registry().add("float_acos",&p_float_acos);
2174  registry().add("float_asin",&p_float_asin);
2175  registry().add("float_atan",&p_float_atan);
2176  registry().add("float_cos",&p_float_cos);
2177  // registry().add("float_cosh",&p_float_cosh);
2178  registry().add("float_exp",&p_float_exp);
2179  registry().add("float_ln",&p_float_ln);
2180  registry().add("float_log10",&p_float_log10);
2181  registry().add("float_log2",&p_float_log2);
2182  registry().add("float_sin",&p_float_sin);
2183  // registry().add("float_sinh",&p_float_sinh);
2184  registry().add("float_tan",&p_float_tan);
2185  // registry().add("float_tanh",&p_float_tanh);
2186 #endif
2187  }
2188  } __float_poster;
2189 #endif
2190 
2191  }
2192 }}
2193 
2194 // STATISTICS: flatzinc-any
Bounds propagation.
Definition: int.hh:978
void mod(Home home, IntVar x0, IntVar x1, IntVar x2, IntPropLevel ipl)
Post propagator for .
Definition: arithmetic.cpp:263
static IntArgs create(int n, int start, int inc=1)
Allocate array with n elements such that for all .
Definition: array.hpp:76
Post propagator for SetVar SetOpType op
Definition: set.hh:767
NodeType t
Type of node.
Definition: bool-expr.cpp:230
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:88
IntArgs arg2intargs(AST::Node *arg, int offset=0)
Convert arg (array of integers) to IntArgs.
Definition: flatzinc.cpp:2123
void post(FlatZincSpace &s, const ConExpr &ce)
Post constraint specified by ce.
Definition: registry.cpp:59
NNF * l
Left subtree.
Definition: bool-expr.cpp:240
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
int size(void) const
Return size of array (number of elements)
Definition: array.hpp:1569
const int min
Smallest allowed integer in integer set.
Definition: set.hh:99
Map from constraint identifier to constraint posting functions.
Definition: registry.hh:44
void sequence(Home home, const IntVarArgs &x, const IntSet &s, int q, int l, int u, IntPropLevel)
Post propagator for .
Definition: sequence.cpp:47
void log(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
void channel(Home home, FloatVar x0, IntVar x1)
Post propagator for channeling a float and an integer variable .
Definition: channel.cpp:41
const FloatNum max
Largest allowed float value.
Definition: float.hh:844
void count(Home home, const IntVarArgs &x, int n, IntRelType irt, int m, IntPropLevel)
Post propagator for .
Definition: count.cpp:40
Less or equal ( )
Definition: float.hh:1071
void max(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:49
Gecode::IntVarArray iv
The integer variables.
Definition: flatzinc.hh:485
void abs(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition: arithmetic.cpp:41
Less or equal ( )
Definition: int.hh:928
void pow(Home home, FloatVar x0, int n, FloatVar x1)
Post propagator for for $n 0$.
Definition: arithmetic.cpp:109
Conjunction.
Definition: int.hh:951
void member(Home home, const IntVarArgs &x, IntVar y, IntPropLevel)
Post domain consistent propagator for .
Definition: member.cpp:39
void dom(Home home, FloatVar x, FloatVal n)
Propagates .
Definition: dom.cpp:40
void linear(Home home, const FloatVarArgs &x, FloatRelType frt, FloatVal c)
Post propagator for .
Definition: linear.cpp:41
void * ralloc(size_t s)
Allocate s bytes from heap.
Definition: heap.hpp:357
Implication.
Definition: int.hh:953
std::vector< Node * > a
Definition: ast.hh:233
void circuit(Home home, int offset, const IntVarArgs &x, IntPropLevel ipl)
Post propagator such that x forms a circuit.
Definition: circuit.cpp:41
void argmin(Home home, const IntVarArgs &x, IntVar y, bool tiebreak, IntPropLevel)
Post propagator for .
Definition: arithmetic.cpp:163
Less ( )
Definition: float.hh:1072
SetOpType
Common operations for sets.
Definition: set.hh:660
Greater ( )
Definition: int.hh:931
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:41
const int max
Largest allowed integer in integer set.
Definition: set.hh:97
ArgArray< IntSet > IntSetArgs
Passing set arguments.
Definition: int.hh:619
const int max
Largest allowed integer value.
Definition: int.hh:116
Greater or equal ( )
Definition: int.hh:930
Difference.
Definition: set.hh:664
Exclusive or.
Definition: int.hh:955
const int min
Smallest allowed integer value.
Definition: int.hh:118
Gecode::IntSet d(v, 7)
Gecode::FloatVal c(-8, 8)
int p
Number of positive literals for node type.
Definition: bool-expr.cpp:232
const FloatNum min
Smallest allowed float value.
Definition: float.hh:846
IntRelType neg(IntRelType irt)
Return negated relation type of irt.
Definition: irt.hpp:52
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:234
Equality ( )
Definition: int.hh:926
void unshare(Home home, IntVarArgs &x, IntPropLevel ipl)
Replace multiple variable occurences in x by fresh variables.
Definition: unshare.cpp:136
Options opt
The options.
Definition: test.cpp:97
IntPropLevel ann2ipl(AST::Node *ann)
Convert ann to integer propagation level.
Definition: flatzinc.cpp:2386
Gecode::IntArgs i({1, 2, 3, 4})
void nvalues(Home home, const IntVarArgs &x, IntRelType irt, int y, IntPropLevel)
Post propagator for .
Definition: nvalues.cpp:40
IntRelType
Relation types for integers.
Definition: int.hh:925
IntVar arg2IntVar(AST::Node *n)
Convert n to IntVar.
Definition: flatzinc.cpp:2285
FloatRelType
Relation types for floats.
Definition: float.hh:1068
Less or equal ( )
Definition: set.hh:650
Simple propagation levels.
Definition: int.hh:976
void extensional(Home home, const IntVarArgs &x, DFA dfa, IntPropLevel)
Post domain consistent propagator for extensional constraint described by a DFA.
BoolVarArgs arg2boolvarargs(AST::Node *arg, int offset=0, int siv=-1)
Convert arg to BoolVarArgs.
Definition: flatzinc.cpp:2248
void sqrt(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition: arithmetic.cpp:102
struct Gecode::@593::NNF::@62::@63 b
For binary nodes (and, or, eqv)
Reification specification.
Definition: int.hh:876
void distinct(Home home, const IntVarArgs &x, IntPropLevel ipl)
Post propagator for for all .
Definition: distinct.cpp:46
Subset ( )
Definition: set.hh:646
void argmax(Home home, const IntVarArgs &x, IntVar y, bool tiebreak, IntPropLevel)
Post propagator for .
Definition: arithmetic.cpp:110
#define BOOL_OP(op)
Definition: registry.cpp:564
Intersection
Definition: set.hh:663
Less ( )
Definition: int.hh:929
Post propagator for SetVar SetOpType SetVar SetRelType SetVar z
Definition: set.hh:767
Less ( )
Definition: set.hh:651
Disjunction.
Definition: int.hh:952
IntVarArgs arg2intvarargs(AST::Node *arg, int offset=0)
Convert arg to IntVarArgs.
Definition: flatzinc.cpp:2227
void convex(Home home, SetVar x)
Definition: convex.cpp:41
void asin(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
AST::Array * ann
Constraint annotations.
Definition: conexpr.hh:50
Passing integer variables.
Definition: int.hh:656
bool isBoolArray(AST::Node *b, int &singleInt)
Check if b is array of Booleans (or has a single integer)
Definition: flatzinc.cpp:2295
SharedArray< int > IntSharedArray
Arrays of integers that can be shared among several element constraints.
Definition: int.hh:1476
Passing integer arguments.
Definition: int.hh:628
Passing Boolean variables.
Definition: int.hh:712
Equality ( )
Definition: float.hh:1069
static const IntSet empty
Empty set.
Definition: int.hh:283
BoolVar expr(Home home, const BoolExpr &e, IntPropLevel ipl)
Post Boolean expression and return its value.
Definition: bool-expr.cpp:627
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
union Gecode::@593::NNF::@62 u
Union depending on nodetype t.
LinIntExpr cardinality(const SetExpr &e)
Cardinality of set expression.
Definition: set-expr.cpp:815
Post propagator for SetVar SetOpType SetVar SetRelType r
Definition: set.hh:767
const int v[7]
Definition: distinct.cpp:259
void min(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:67
void cos(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
IntPropLevel
Propagation levels for integer propagators.
Definition: int.hh:974
Union.
Definition: set.hh:661
AST::Array * args
Constraint arguments.
Definition: conexpr.hh:48
Post propagator for f(x \diamond_{\mathit{op}} y) \sim_r z \f$ void rel(Home home
Post propagator for SetVar SetOpType SetVar y
Definition: set.hh:767
void div(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:127
void tan(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Disjoint union.
Definition: set.hh:662
void(* poster)(FlatZincSpace &, const ConExpr &, AST::Node *)
Type of constraint posting function.
Definition: registry.hh:47
void precede(Home home, const IntVarArgs &x, int s, int t, IntPropLevel)
Post propagator that s precedes t in x.
Definition: precede.cpp:43
Integer variables.
Definition: int.hh:371
Heap heap
The single global heap.
Definition: heap.cpp:44
void rel(Home home, FloatVar x0, FloatRelType frt, FloatVal n)
Propagates .
Definition: rel.cpp:43
Exception class for FlatZinc errors
Definition: flatzinc.hh:665
Domain propagation Options: basic versus advanced propagation.
Definition: int.hh:979
Equality ( )
Definition: set.hh:644
Disjoint ( )
Definition: set.hh:648
Post propagator for SetVar x
Definition: set.hh:767
void add(const std::string &id, poster p)
Add posting function p with identifier id.
Definition: registry.cpp:69
#define BOOL_ARRAY_OP(op)
Definition: registry.cpp:573
A space that can be initialized with a FlatZinc model.
Definition: flatzinc.hh:428
Disequality ( )
Definition: set.hh:645
Gecode toplevel namespace
void weights(Home home, IntSharedArray elements, IntSharedArray weights, SetVar x, IntVar y)
Definition: int.cpp:292
Implication for reification.
Definition: int.hh:862
void sin(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
A node in a FlatZinc abstract syntax tree.
Definition: ast.hh:67
Disequality ( )
Definition: int.hh:927
void acos(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
void exp(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
void cumulative(Home home, int c, const TaskTypeArgs &t, const IntVarArgs &s, const IntArgs &p, const IntArgs &u, IntPropLevel ipl)
Post propagators for scheduling tasks on cumulative resources.
Definition: cumulative.cpp:354
ReifyMode
Mode for reification.
Definition: int.hh:848
void unary(Home home, const IntVarArgs &s, const IntArgs &p, IntPropLevel ipl)
Post propagators for scheduling tasks on unary resources.
Definition: unary.cpp:44
struct Gecode::@593::NNF::@62::@64 a
For atomic nodes.
#define P_FLOAT_OP(Op)
Definition: registry.cpp:2110
void element(Home home, IntSharedArray c, IntVar x0, IntVar x1, IntPropLevel)
Post domain consistent propagator for .
Definition: element.cpp:39
Registry & registry(void)
Return global registry object.
Definition: registry.cpp:53
void atan(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
std::string id
Identifier for the constraint.
Definition: conexpr.hh:46
T * a
Element array.
Definition: array.hpp:526
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
Equivalence for reification (default)
Definition: int.hh:855
IntRelType swap(IntRelType irt)
Return swapped relation type of irt.
Definition: irt.hpp:37
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:2274
Abstract representation of a constraint.
Definition: conexpr.hh:43