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