this repo has no description
dekker.one
1/*
2 * Main authors:
3 * Kevin Leo <kevin.leo@monash.edu>
4 * Andrea Rendl <andrea.rendl@nicta.com.au>
5 * Guido Tack <guido.tack@monash.edu>
6 */
7
8/* This Source Code Form is subject to the terms of the Mozilla Public
9 * License, v. 2.0. If a copy of the MPL was not distributed with this
10 * file, You can obtain one at http://mozilla.org/MPL/2.0/. */
11
12#include <minizinc/eval_par.hh>
13#include <minizinc/solvers/gecode/fzn_space.hh>
14#include <minizinc/solvers/gecode/gecode_constraints.hh>
15#include <minizinc/solvers/gecode_solverinstance.hh>
16
17using namespace Gecode;
18
19namespace MiniZinc {
20namespace GecodeConstraints {
21
22void p_distinct(SolverInstanceBase& s, const Call* call) {
23 auto& gi = static_cast<GecodeSolverInstance&>(s);
24 IntVarArgs va = gi.arg2intvarargs(call->arg(0));
25 MZ_IntConLevel icl = GecodeSolverInstance::ann2icl(call->ann());
26 unshare(*gi.currentSpace, va);
27 distinct(*gi.currentSpace, va, icl == MZ_ICL_DEF ? MZ_ICL_DOM : icl);
28}
29
30void p_distinct_offset(SolverInstanceBase& s, const Call* call) {
31 auto& gi = static_cast<GecodeSolverInstance&>(s);
32 IntVarArgs va = gi.arg2intvarargs(call->arg(1));
33 unshare(*gi.currentSpace, va);
34 IntArgs oa = GecodeSolverInstance::arg2intargs(call->arg(0));
35 MZ_IntConLevel icl = GecodeSolverInstance::ann2icl(call->ann());
36 distinct(*gi.currentSpace, oa, va, icl == MZ_ICL_DEF ? MZ_ICL_DOM : icl);
37}
38
39void p_all_equal(SolverInstanceBase& s, const Call* call) {
40 auto& gi = static_cast<GecodeSolverInstance&>(s);
41 IntVarArgs va = gi.arg2intvarargs(call->arg(0));
42 rel(*gi.currentSpace, va, IRT_EQ, GecodeSolverInstance::ann2icl(call->ann()));
43}
44
45void p_int_cmp(GecodeSolverInstance& s, IntRelType irt, const Call* ce) {
46 const Annotation& ann = ce->ann();
47 Expression* lhs = ce->arg(0);
48 Expression* rhs = ce->arg(1);
49 if (lhs->type().isvarint()) {
50 if (rhs->type().isvarint()) {
51 rel(*s.currentSpace, s.arg2intvar(lhs), irt, s.arg2intvar(rhs),
52 GecodeSolverInstance::ann2icl(ann));
53 } else {
54 rel(*s.currentSpace, s.arg2intvar(lhs), irt,
55 static_cast<int>(rhs->cast<IntLit>()->v().toInt()), GecodeSolverInstance::ann2icl(ann));
56 }
57 } else {
58 rel(*s.currentSpace, s.arg2intvar(rhs), swap(irt),
59 static_cast<int>(lhs->cast<IntLit>()->v().toInt()), GecodeSolverInstance::ann2icl(ann));
60 }
61}
62
63void p_int_eq(SolverInstanceBase& s, const Call* call) {
64 p_int_cmp(static_cast<GecodeSolverInstance&>(s), IRT_EQ, call);
65}
66void p_int_ne(SolverInstanceBase& s, const Call* call) {
67 p_int_cmp(static_cast<GecodeSolverInstance&>(s), IRT_NQ, call);
68}
69void p_int_ge(SolverInstanceBase& s, const Call* call) {
70 p_int_cmp(static_cast<GecodeSolverInstance&>(s), IRT_GQ, call);
71}
72void p_int_gt(SolverInstanceBase& s, const Call* call) {
73 p_int_cmp(static_cast<GecodeSolverInstance&>(s), IRT_GR, call);
74}
75void p_int_le(SolverInstanceBase& s, const Call* call) {
76 p_int_cmp(static_cast<GecodeSolverInstance&>(s), IRT_LQ, call);
77}
78void p_int_lt(SolverInstanceBase& s, const Call* call) {
79 p_int_cmp(static_cast<GecodeSolverInstance&>(s), IRT_LE, call);
80}
81void p_int_cmp_reif(GecodeSolverInstance& s, IntRelType irt, ReifyMode rm, const Call* call) {
82 const Annotation& ann = call->ann();
83 if (rm == RM_EQV && !call->arg(2)->type().isvar()) {
84 if (call->arg(2)->cast<BoolLit>()->v()) {
85 p_int_cmp(s, irt, call);
86 } else {
87 p_int_cmp(s, neg(irt), call);
88 }
89 return;
90 }
91 if (call->arg(0)->type().isvarint()) {
92 if (call->arg(1)->type().isvarint()) {
93 rel(*s.currentSpace, s.arg2intvar(call->arg(0)), irt, s.arg2intvar(call->arg(1)),
94 Reify(s.arg2boolvar(call->arg(2)), rm), GecodeSolverInstance::ann2icl(ann));
95 } else {
96 rel(*s.currentSpace, s.arg2intvar(call->arg(0)), irt,
97 static_cast<int>(call->arg(1)->cast<IntLit>()->v().toInt()),
98 Reify(s.arg2boolvar(call->arg(2)), rm), GecodeSolverInstance::ann2icl(ann));
99 }
100 } else {
101 rel(*s.currentSpace, s.arg2intvar(call->arg(1)), swap(irt),
102 static_cast<int>(call->arg(0)->cast<IntLit>()->v().toInt()),
103 Reify(s.arg2boolvar(call->arg(2)), rm), GecodeSolverInstance::ann2icl(ann));
104 }
105}
106
107///* Comparisons */
108void p_int_eq_reif(SolverInstanceBase& s, const Call* call) {
109 p_int_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_EQ, RM_EQV, call);
110}
111void p_int_ne_reif(SolverInstanceBase& s, const Call* call) {
112 p_int_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_NQ, RM_EQV, call);
113}
114void p_int_ge_reif(SolverInstanceBase& s, const Call* call) {
115 p_int_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_GQ, RM_EQV, call);
116}
117void p_int_gt_reif(SolverInstanceBase& s, const Call* call) {
118 p_int_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_GR, RM_EQV, call);
119}
120void p_int_le_reif(SolverInstanceBase& s, const Call* call) {
121 p_int_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_LQ, RM_EQV, call);
122}
123void p_int_lt_reif(SolverInstanceBase& s, const Call* call) {
124 p_int_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_LE, RM_EQV, call);
125}
126
127void p_int_eq_imp(SolverInstanceBase& s, const Call* call) {
128 p_int_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_EQ, RM_IMP, call);
129}
130void p_int_ne_imp(SolverInstanceBase& s, const Call* call) {
131 p_int_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_NQ, RM_IMP, call);
132}
133void p_int_ge_imp(SolverInstanceBase& s, const Call* call) {
134 p_int_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_GQ, RM_IMP, call);
135}
136void p_int_gt_imp(SolverInstanceBase& s, const Call* call) {
137 p_int_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_GR, RM_IMP, call);
138}
139void p_int_le_imp(SolverInstanceBase& s, const Call* call) {
140 p_int_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_LQ, RM_IMP, call);
141}
142void p_int_lt_imp(SolverInstanceBase& s, const Call* call) {
143 p_int_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_LE, RM_IMP, call);
144}
145
146void p_int_lin_cmp(GecodeSolverInstance& s, IntRelType irt, const Call* call) {
147 const Annotation& ann = call->ann();
148 IntArgs ia = GecodeSolverInstance::arg2intargs(call->arg(0));
149 ArrayLit* vars = s.arg2arraylit(call->arg(1));
150 int singleIntVar;
151 if (s.isBoolArray(vars, singleIntVar)) {
152 if (singleIntVar != -1) {
153 if (std::abs(ia[singleIntVar]) == 1 && call->arg(2)->cast<IntLit>()->v().toInt() == 0) {
154 IntVar siv = s.arg2intvar((*vars)[singleIntVar]);
155 BoolVarArgs iv = s.arg2boolvarargs(vars, 0, singleIntVar);
156 IntArgs ia_tmp(ia.size() - 1);
157 int count = 0;
158 for (int i = 0; i < ia.size(); i++) {
159 if (i != singleIntVar) {
160 ia_tmp[count++] = ia[singleIntVar] == -1 ? ia[i] : -ia[i];
161 }
162 }
163 IntRelType t = (ia[singleIntVar] == -1 ? irt : swap(irt));
164 linear(*s.currentSpace, ia_tmp, iv, t, siv, GecodeSolverInstance::ann2icl(ann));
165 } else {
166 IntVarArgs iv = s.arg2intvarargs(vars);
167 linear(*s.currentSpace, ia, iv, irt,
168 static_cast<int>(call->arg(2)->cast<IntLit>()->v().toInt()),
169 GecodeSolverInstance::ann2icl(ann));
170 }
171 } else {
172 BoolVarArgs iv = s.arg2boolvarargs(vars);
173 linear(*s.currentSpace, ia, iv, irt,
174 static_cast<int>(call->arg(2)->cast<IntLit>()->v().toInt()),
175 GecodeSolverInstance::ann2icl(ann));
176 }
177 } else {
178 IntVarArgs iv = s.arg2intvarargs(vars);
179 linear(*s.currentSpace, ia, iv, irt,
180 static_cast<int>(call->arg(2)->cast<IntLit>()->v().toInt()),
181 GecodeSolverInstance::ann2icl(ann));
182 }
183}
184void p_int_lin_cmp_reif(GecodeSolverInstance& s, IntRelType irt, ReifyMode rm, const Call* call) {
185 const Annotation& ann = call->ann();
186 if (rm == RM_EQV && call->arg(2)->type().isbool()) {
187 if (call->arg(2)->cast<BoolLit>()->v()) {
188 p_int_lin_cmp(s, irt, call);
189 } else {
190 p_int_lin_cmp(s, neg(irt), call);
191 }
192 return;
193 }
194 IntArgs ia = GecodeSolverInstance::arg2intargs(call->arg(0));
195 ArrayLit* vars = s.arg2arraylit(call->arg(1));
196 int singleIntVar;
197 if (s.isBoolArray(vars, singleIntVar)) {
198 if (singleIntVar != -1) {
199 if (std::abs(ia[singleIntVar]) == 1 && call->arg(2)->cast<IntLit>()->v().toInt() == 0) {
200 IntVar siv = s.arg2intvar((*vars)[singleIntVar]);
201 BoolVarArgs iv = s.arg2boolvarargs(vars, 0, singleIntVar);
202 IntArgs ia_tmp(ia.size() - 1);
203 int count = 0;
204 for (int i = 0; i < ia.size(); i++) {
205 if (i != singleIntVar) {
206 ia_tmp[count++] = ia[singleIntVar] == -1 ? ia[i] : -ia[i];
207 }
208 }
209 IntRelType t = (ia[singleIntVar] == -1 ? irt : swap(irt));
210 linear(*s.currentSpace, ia_tmp, iv, t, siv, Reify(s.arg2boolvar(call->arg(3)), rm),
211 GecodeSolverInstance::ann2icl(ann));
212 } else {
213 IntVarArgs iv = s.arg2intvarargs(vars);
214 linear(*s.currentSpace, ia, iv, irt,
215 static_cast<int>(call->arg(2)->cast<IntLit>()->v().toInt()),
216 Reify(s.arg2boolvar(call->arg(3)), rm), GecodeSolverInstance::ann2icl(ann));
217 }
218 } else {
219 BoolVarArgs iv = s.arg2boolvarargs(vars);
220 linear(*s.currentSpace, ia, iv, irt,
221 static_cast<int>(call->arg(2)->cast<IntLit>()->v().toInt()),
222 Reify(s.arg2boolvar(call->arg(3)), rm), GecodeSolverInstance::ann2icl(ann));
223 }
224 } else {
225 IntVarArgs iv = s.arg2intvarargs(vars);
226 linear(*s.currentSpace, ia, iv, irt,
227 static_cast<int>(call->arg(2)->cast<IntLit>()->v().toInt()),
228 Reify(s.arg2boolvar(call->arg(3)), rm), GecodeSolverInstance::ann2icl(ann));
229 }
230}
231
232void p_int_lin_eq(SolverInstanceBase& s, const Call* call) {
233 p_int_lin_cmp(static_cast<GecodeSolverInstance&>(s), IRT_EQ, call);
234}
235void p_int_lin_eq_reif(SolverInstanceBase& s, const Call* call) {
236 p_int_lin_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_EQ, RM_EQV, call);
237}
238void p_int_lin_eq_imp(SolverInstanceBase& s, const Call* call) {
239 p_int_lin_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_EQ, RM_IMP, call);
240}
241void p_int_lin_ne(SolverInstanceBase& s, const Call* call) {
242 p_int_lin_cmp(static_cast<GecodeSolverInstance&>(s), IRT_NQ, call);
243}
244void p_int_lin_ne_reif(SolverInstanceBase& s, const Call* call) {
245 p_int_lin_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_NQ, RM_EQV, call);
246}
247void p_int_lin_ne_imp(SolverInstanceBase& s, const Call* call) {
248 p_int_lin_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_NQ, RM_IMP, call);
249}
250void p_int_lin_le(SolverInstanceBase& s, const Call* call) {
251 p_int_lin_cmp(static_cast<GecodeSolverInstance&>(s), IRT_LQ, call);
252}
253void p_int_lin_le_reif(SolverInstanceBase& s, const Call* call) {
254 p_int_lin_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_LQ, RM_EQV, call);
255}
256void p_int_lin_le_imp(SolverInstanceBase& s, const Call* call) {
257 p_int_lin_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_LQ, RM_IMP, call);
258}
259void p_int_lin_lt(SolverInstanceBase& s, const Call* call) {
260 p_int_lin_cmp(static_cast<GecodeSolverInstance&>(s), IRT_LE, call);
261}
262void p_int_lin_lt_reif(SolverInstanceBase& s, const Call* call) {
263 p_int_lin_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_LE, RM_EQV, call);
264}
265void p_int_lin_lt_imp(SolverInstanceBase& s, const Call* call) {
266 p_int_lin_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_LE, RM_IMP, call);
267}
268void p_int_lin_ge(SolverInstanceBase& s, const Call* call) {
269 p_int_lin_cmp(static_cast<GecodeSolverInstance&>(s), IRT_GQ, call);
270}
271void p_int_lin_ge_reif(SolverInstanceBase& s, const Call* call) {
272 p_int_lin_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_GQ, RM_EQV, call);
273}
274void p_int_lin_ge_imp(SolverInstanceBase& s, const Call* call) {
275 p_int_lin_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_GQ, RM_IMP, call);
276}
277void p_int_lin_gt(SolverInstanceBase& s, const Call* call) {
278 p_int_lin_cmp(static_cast<GecodeSolverInstance&>(s), IRT_GR, call);
279}
280void p_int_lin_gt_reif(SolverInstanceBase& s, const Call* call) {
281 p_int_lin_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_GR, RM_EQV, call);
282}
283void p_int_lin_gt_imp(SolverInstanceBase& s, const Call* call) {
284 p_int_lin_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_GR, RM_IMP, call);
285}
286
287void p_bool_lin_cmp(GecodeSolverInstance& s, IntRelType irt, const Call* call) {
288 const Annotation& ann = call->ann();
289 IntArgs ia = GecodeSolverInstance::arg2intargs(call->arg(0));
290 BoolVarArgs iv = s.arg2boolvarargs(call->arg(1));
291 if (call->arg(2)->type().isvarint()) {
292 linear(*s.currentSpace, ia, iv, irt,
293 s.resolveVar(call->arg(2)->cast<Id>()->decl()).intVar(s.currentSpace),
294 GecodeSolverInstance::ann2icl(ann));
295 } else {
296 linear(*s.currentSpace, ia, iv, irt,
297 static_cast<int>(call->arg(2)->cast<IntLit>()->v().toInt()),
298 GecodeSolverInstance::ann2icl(ann));
299 }
300}
301void p_bool_lin_cmp_reif(GecodeSolverInstance& s, IntRelType irt, ReifyMode rm, const Call* call) {
302 const Annotation& ann = call->ann();
303 if (rm == RM_EQV && call->arg(2)->type().isbool()) {
304 if (call->arg(2)->cast<BoolLit>()->v()) {
305 p_bool_lin_cmp(s, irt, call);
306 } else {
307 p_bool_lin_cmp(s, neg(irt), call);
308 }
309 return;
310 }
311 IntArgs ia = GecodeSolverInstance::arg2intargs(call->arg(0));
312 BoolVarArgs iv = s.arg2boolvarargs(call->arg(1));
313 if (call->arg(2)->type().isvarint()) {
314 linear(*s.currentSpace, ia, iv, irt,
315 s.resolveVar(call->arg(2)->cast<Id>()->decl()).intVar(s.currentSpace),
316 Reify(s.arg2boolvar(call->arg(3)), rm), GecodeSolverInstance::ann2icl(ann));
317 } else {
318 linear(*s.currentSpace, ia, iv, irt,
319 static_cast<int>(call->arg(2)->cast<IntLit>()->v().toInt()),
320 Reify(s.arg2boolvar(call->arg(3)), rm), GecodeSolverInstance::ann2icl(ann));
321 }
322}
323void p_bool_lin_eq(SolverInstanceBase& s, const Call* call) {
324 p_bool_lin_cmp(static_cast<GecodeSolverInstance&>(s), IRT_EQ, call);
325}
326void p_bool_lin_eq_reif(SolverInstanceBase& s, const Call* call) {
327 p_bool_lin_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_EQ, RM_EQV, call);
328}
329void p_bool_lin_eq_imp(SolverInstanceBase& s, const Call* call) {
330 p_bool_lin_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_EQ, RM_IMP, call);
331}
332void p_bool_lin_ne(SolverInstanceBase& s, const Call* call) {
333 p_bool_lin_cmp(static_cast<GecodeSolverInstance&>(s), IRT_NQ, call);
334}
335void p_bool_lin_ne_reif(SolverInstanceBase& s, const Call* call) {
336 p_bool_lin_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_NQ, RM_EQV, call);
337}
338void p_bool_lin_ne_imp(SolverInstanceBase& s, const Call* call) {
339 p_bool_lin_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_NQ, RM_IMP, call);
340}
341void p_bool_lin_le(SolverInstanceBase& s, const Call* call) {
342 p_bool_lin_cmp(static_cast<GecodeSolverInstance&>(s), IRT_LQ, call);
343}
344void p_bool_lin_le_reif(SolverInstanceBase& s, const Call* call) {
345 p_bool_lin_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_LQ, RM_EQV, call);
346}
347void p_bool_lin_le_imp(SolverInstanceBase& s, const Call* call) {
348 p_bool_lin_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_LQ, RM_IMP, call);
349}
350void p_bool_lin_lt(SolverInstanceBase& s, const Call* call) {
351 p_bool_lin_cmp(static_cast<GecodeSolverInstance&>(s), IRT_LE, call);
352}
353void p_bool_lin_lt_reif(SolverInstanceBase& s, const Call* call) {
354 p_bool_lin_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_LE, RM_EQV, call);
355}
356void p_bool_lin_lt_imp(SolverInstanceBase& s, const Call* call) {
357 p_bool_lin_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_LE, RM_IMP, call);
358}
359void p_bool_lin_ge(SolverInstanceBase& s, const Call* call) {
360 p_bool_lin_cmp(static_cast<GecodeSolverInstance&>(s), IRT_GQ, call);
361}
362void p_bool_lin_ge_reif(SolverInstanceBase& s, const Call* call) {
363 p_bool_lin_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_GQ, RM_EQV, call);
364}
365void p_bool_lin_ge_imp(SolverInstanceBase& s, const Call* call) {
366 p_bool_lin_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_GQ, RM_IMP, call);
367}
368void p_bool_lin_gt(SolverInstanceBase& s, const Call* call) {
369 p_bool_lin_cmp(static_cast<GecodeSolverInstance&>(s), IRT_GR, call);
370}
371void p_bool_lin_gt_reif(SolverInstanceBase& s, const Call* call) {
372 p_bool_lin_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_GR, RM_EQV, call);
373}
374void p_bool_lin_gt_imp(SolverInstanceBase& s, const Call* call) {
375 p_bool_lin_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_GR, RM_IMP, call);
376}
377
378///* arithmetic constraints */
379
380void p_int_plus(SolverInstanceBase& s, const Call* call) {
381 auto& gi = static_cast<GecodeSolverInstance&>(s);
382 if (!call->arg(0)->type().isvarint()) {
383 rel(*gi.currentSpace,
384 static_cast<int>(call->arg(0)->cast<IntLit>()->v().toInt()) + gi.arg2intvar(call->arg(1)) ==
385 gi.arg2intvar(call->arg(2)),
386 GecodeSolverInstance::ann2icl(call->ann()));
387 } else if (!call->arg(1)->type().isvarint()) {
388 rel(*gi.currentSpace,
389 gi.arg2intvar(call->arg(0)) + static_cast<int>(call->arg(1)->cast<IntLit>()->v().toInt()) ==
390 gi.arg2intvar(call->arg(2)),
391 GecodeSolverInstance::ann2icl(call->ann()));
392 } else if (!call->arg(2)->type().isvarint()) {
393 rel(*gi.currentSpace,
394 gi.arg2intvar(call->arg(0)) + gi.arg2intvar(call->arg(1)) ==
395 static_cast<int>(call->arg(2)->cast<IntLit>()->v().toInt()),
396 GecodeSolverInstance::ann2icl(call->ann()));
397 } else {
398 rel(*gi.currentSpace,
399 gi.arg2intvar(call->arg(0)) + gi.arg2intvar(call->arg(1)) == gi.arg2intvar(call->arg(2)),
400 GecodeSolverInstance::ann2icl(call->ann()));
401 }
402}
403
404void p_int_minus(SolverInstanceBase& s, const Call* call) {
405 auto& gi = static_cast<GecodeSolverInstance&>(s);
406 if (!call->arg(0)->type().isvarint()) {
407 rel(*gi.currentSpace,
408 static_cast<int>(call->arg(0)->cast<IntLit>()->v().toInt()) - gi.arg2intvar(call->arg(1)) ==
409 gi.arg2intvar(call->arg(2)),
410 GecodeSolverInstance::ann2icl(call->ann()));
411 } else if (!call->arg(1)->type().isvarint()) {
412 rel(*gi.currentSpace,
413 gi.arg2intvar(call->arg(0)) - static_cast<int>(call->arg(1)->cast<IntLit>()->v().toInt()) ==
414 gi.arg2intvar(call->arg(2)),
415 GecodeSolverInstance::ann2icl(call->ann()));
416 } else if (!call->arg(2)->type().isvarint()) {
417 rel(*gi.currentSpace,
418 gi.arg2intvar(call->arg(0)) - gi.arg2intvar(call->arg(1)) ==
419 static_cast<int>(call->arg(2)->cast<IntLit>()->v().toInt()),
420 GecodeSolverInstance::ann2icl(call->ann()));
421 } else {
422 rel(*gi.currentSpace,
423 gi.arg2intvar(call->arg(0)) - gi.arg2intvar(call->arg(1)) == gi.arg2intvar(call->arg(2)),
424 GecodeSolverInstance::ann2icl(call->ann()));
425 }
426}
427
428void p_int_times(SolverInstanceBase& s, const Call* call) {
429 auto& gi = static_cast<GecodeSolverInstance&>(s);
430 IntVar x0 = gi.arg2intvar(call->arg(0));
431 IntVar x1 = gi.arg2intvar(call->arg(1));
432 IntVar x2 = gi.arg2intvar(call->arg(2));
433 mult(*gi.currentSpace, x0, x1, x2, GecodeSolverInstance::ann2icl(call->ann()));
434}
435void p_int_div(SolverInstanceBase& s, const Call* call) {
436 auto& gi = static_cast<GecodeSolverInstance&>(s);
437 IntVar x0 = gi.arg2intvar(call->arg(0));
438 IntVar x1 = gi.arg2intvar(call->arg(1));
439 IntVar x2 = gi.arg2intvar(call->arg(2));
440 div(*gi.currentSpace, x0, x1, x2, GecodeSolverInstance::ann2icl(call->ann()));
441}
442void p_int_mod(SolverInstanceBase& s, const Call* call) {
443 auto& gi = static_cast<GecodeSolverInstance&>(s);
444 IntVar x0 = gi.arg2intvar(call->arg(0));
445 IntVar x1 = gi.arg2intvar(call->arg(1));
446 IntVar x2 = gi.arg2intvar(call->arg(2));
447 mod(*gi.currentSpace, x0, x1, x2, GecodeSolverInstance::ann2icl(call->ann()));
448}
449
450void p_int_min(SolverInstanceBase& s, const Call* call) {
451 auto& gi = static_cast<GecodeSolverInstance&>(s);
452 IntVar x0 = gi.arg2intvar(call->arg(0));
453 IntVar x1 = gi.arg2intvar(call->arg(1));
454 IntVar x2 = gi.arg2intvar(call->arg(2));
455 min(*gi.currentSpace, x0, x1, x2, GecodeSolverInstance::ann2icl(call->ann()));
456}
457void p_int_max(SolverInstanceBase& s, const Call* call) {
458 auto& gi = static_cast<GecodeSolverInstance&>(s);
459 IntVar x0 = gi.arg2intvar(call->arg(0));
460 IntVar x1 = gi.arg2intvar(call->arg(1));
461 IntVar x2 = gi.arg2intvar(call->arg(2));
462 max(*gi.currentSpace, x0, x1, x2, GecodeSolverInstance::ann2icl(call->ann()));
463}
464void p_int_negate(SolverInstanceBase& s, const Call* call) {
465 auto& gi = static_cast<GecodeSolverInstance&>(s);
466 IntVar x0 = gi.arg2intvar(call->arg(0));
467 IntVar x1 = gi.arg2intvar(call->arg(1));
468 rel(*gi.currentSpace, x0 == -x1, GecodeSolverInstance::ann2icl(call->ann()));
469}
470
471///* Boolean constraints */
472void p_bool_cmp(GecodeSolverInstance& s, IntRelType irt, const Call* call) {
473 const Annotation& ann = call->ann();
474 rel(*s.currentSpace, s.arg2boolvar(call->arg(0)), irt, s.arg2boolvar(call->arg(1)),
475 GecodeSolverInstance::ann2icl(ann));
476}
477void p_bool_cmp_reif(GecodeSolverInstance& s, IntRelType irt, ReifyMode rm, const Call* call) {
478 const Annotation& ann = call->ann();
479 rel(*s.currentSpace, s.arg2boolvar(call->arg(0)), irt, s.arg2boolvar(call->arg(1)),
480 Reify(s.arg2boolvar(call->arg(2)), rm), GecodeSolverInstance::ann2icl(ann));
481}
482void p_bool_eq(SolverInstanceBase& s, const Call* call) {
483 p_bool_cmp(static_cast<GecodeSolverInstance&>(s), IRT_EQ, call);
484}
485void p_bool_eq_reif(SolverInstanceBase& s, const Call* call) {
486 p_bool_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_EQ, RM_EQV, call);
487}
488void p_bool_eq_imp(SolverInstanceBase& s, const Call* call) {
489 p_bool_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_EQ, RM_IMP, call);
490}
491void p_bool_ne(SolverInstanceBase& s, const Call* call) {
492 p_bool_cmp(static_cast<GecodeSolverInstance&>(s), IRT_NQ, call);
493}
494void p_bool_ne_reif(SolverInstanceBase& s, const Call* call) {
495 p_bool_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_NQ, RM_EQV, call);
496}
497void p_bool_ne_imp(SolverInstanceBase& s, const Call* call) {
498 p_bool_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_NQ, RM_IMP, call);
499}
500void p_bool_ge(SolverInstanceBase& s, const Call* call) {
501 p_bool_cmp(static_cast<GecodeSolverInstance&>(s), IRT_GQ, call);
502}
503void p_bool_ge_reif(SolverInstanceBase& s, const Call* call) {
504 p_bool_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_GQ, RM_EQV, call);
505}
506void p_bool_ge_imp(SolverInstanceBase& s, const Call* call) {
507 p_bool_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_GQ, RM_IMP, call);
508}
509void p_bool_le(SolverInstanceBase& s, const Call* call) {
510 p_bool_cmp(static_cast<GecodeSolverInstance&>(s), IRT_LQ, call);
511}
512void p_bool_le_reif(SolverInstanceBase& s, const Call* call) {
513 p_bool_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_LQ, RM_EQV, call);
514}
515void p_bool_le_imp(SolverInstanceBase& s, const Call* call) {
516 p_bool_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_LQ, RM_IMP, call);
517}
518void p_bool_gt(SolverInstanceBase& s, const Call* call) {
519 p_bool_cmp(static_cast<GecodeSolverInstance&>(s), IRT_GR, call);
520}
521void p_bool_gt_reif(SolverInstanceBase& s, const Call* call) {
522 p_bool_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_GR, RM_EQV, call);
523}
524void p_bool_gt_imp(SolverInstanceBase& s, const Call* call) {
525 p_bool_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_GR, RM_IMP, call);
526}
527void p_bool_lt(SolverInstanceBase& s, const Call* call) {
528 p_bool_cmp(static_cast<GecodeSolverInstance&>(s), IRT_LE, call);
529}
530void p_bool_lt_reif(SolverInstanceBase& s, const Call* call) {
531 p_bool_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_LE, RM_EQV, call);
532}
533void p_bool_lt_imp(SolverInstanceBase& s, const Call* call) {
534 p_bool_cmp_reif(static_cast<GecodeSolverInstance&>(s), IRT_LE, RM_IMP, call);
535}
536
537#define BOOL_OP(op) \
538 BoolVar b0 = gi.arg2boolvar(call->arg(0)); \
539 BoolVar b1 = gi.arg2boolvar(call->arg(1)); \
540 if (!call->arg(2)->type().isvar() && call->arg(2)->type().isbool()) { \
541 rel(*gi.currentSpace, b0, op, b1, call->arg(2)->cast<BoolLit>()->v(), gi.ann2icl(ann)); \
542 } else { \
543 rel(*gi.currentSpace, b0, op, b1, \
544 gi.resolveVar(gi.getVarDecl(call->arg(2))).boolVar(gi.currentSpace), gi.ann2icl(ann)); \
545 }
546
547#define BOOL_ARRAY_OP(op) \
548 BoolVarArgs bv = gi.arg2boolvarargs(call->arg(0)); \
549 if (call->argCount() == 1) { \
550 rel(*gi.currentSpace, op, bv, 1, gi.ann2icl(ann)); \
551 } else if (!call->arg(1)->type().isvar() && call->arg(1)->type().isbool()) { \
552 rel(*gi.currentSpace, op, bv, call->arg(1)->cast<BoolLit>()->v(), gi.ann2icl(ann)); \
553 } else { \
554 rel(*gi.currentSpace, op, bv, \
555 gi.resolveVar(gi.getVarDecl(call->arg(1))).boolVar(gi.currentSpace), gi.ann2icl(ann)); \
556 }
557
558void p_bool_or(SolverInstanceBase& s, const Call* call) {
559 const Annotation& ann = call->ann();
560 auto& gi = static_cast<GecodeSolverInstance&>(s);
561 BOOL_OP(BoolOpType::BOT_OR);
562}
563void p_bool_or_imp(SolverInstanceBase& s, const Call* call) {
564 const Annotation& ann = call->ann();
565 auto& gi = static_cast<GecodeSolverInstance&>(s);
566 BoolVar b0 = gi.arg2boolvar(call->arg(0));
567 BoolVar b1 = gi.arg2boolvar(call->arg(1));
568 BoolVar b2 = gi.arg2boolvar(call->arg(2));
569 clause(*gi.currentSpace, BoolOpType::BOT_OR, BoolVarArgs() << b0 << b1, BoolVarArgs() << b2, 1,
570 GecodeSolverInstance::ann2icl(ann));
571}
572void p_bool_and(SolverInstanceBase& s, const Call* call) {
573 const Annotation& ann = call->ann();
574 auto& gi = static_cast<GecodeSolverInstance&>(s);
575 BOOL_OP(BoolOpType::BOT_AND);
576}
577void p_bool_and_imp(SolverInstanceBase& s, const Call* call) {
578 const Annotation& ann = call->ann();
579 auto& gi = static_cast<GecodeSolverInstance&>(s);
580 BoolVar b0 = gi.arg2boolvar(call->arg(0));
581 BoolVar b1 = gi.arg2boolvar(call->arg(1));
582 BoolVar b2 = gi.arg2boolvar(call->arg(2));
583 rel(*gi.currentSpace, b2, BoolOpType::BOT_IMP, b0, 1, GecodeSolverInstance::ann2icl(ann));
584 rel(*gi.currentSpace, b2, BoolOpType::BOT_IMP, b1, 1, GecodeSolverInstance::ann2icl(ann));
585}
586void p_array_bool_and(SolverInstanceBase& s, const Call* call) {
587 const Annotation& ann = call->ann();
588 auto& gi = static_cast<GecodeSolverInstance&>(s);
589 BOOL_ARRAY_OP(Gecode::BoolOpType::BOT_AND);
590}
591void p_array_bool_and_imp(SolverInstanceBase& s, const Call* call) {
592 const Annotation& ann = call->ann();
593 auto& gi = static_cast<GecodeSolverInstance&>(s);
594 BoolVarArgs bv = gi.arg2boolvarargs(call->arg(0));
595 BoolVar b1 = gi.arg2boolvar(call->arg(1));
596 for (int i = static_cast<int>(bv.size()); (i--) != 0;) {
597 rel(*gi.currentSpace, b1, Gecode::BoolOpType::BOT_IMP, bv[i], 1,
598 GecodeSolverInstance::ann2icl(ann));
599 }
600}
601void p_array_bool_or(SolverInstanceBase& s, const Call* call) {
602 const Annotation& ann = call->ann();
603 auto& gi = static_cast<GecodeSolverInstance&>(s);
604 BOOL_ARRAY_OP(BoolOpType::BOT_OR);
605}
606void p_array_bool_or_imp(SolverInstanceBase& s, const Call* call) {
607 const Annotation& ann = call->ann();
608 auto& gi = static_cast<GecodeSolverInstance&>(s);
609 BoolVarArgs bv = gi.arg2boolvarargs(call->arg(0));
610 BoolVar b1 = gi.arg2boolvar(call->arg(1));
611 clause(*gi.currentSpace, BoolOpType::BOT_OR, bv, BoolVarArgs() << b1, 1,
612 GecodeSolverInstance::ann2icl(ann));
613}
614void p_array_bool_xor(SolverInstanceBase& s, const Call* call) {
615 const Annotation& ann = call->ann();
616 auto& gi = static_cast<GecodeSolverInstance&>(s);
617 BOOL_ARRAY_OP(BoolOpType::BOT_XOR);
618}
619void p_array_bool_xor_imp(SolverInstanceBase& s, const Call* call) {
620 const Annotation& ann = call->ann();
621 auto& gi = static_cast<GecodeSolverInstance&>(s);
622 BoolVarArgs bv = gi.arg2boolvarargs(call->arg(0));
623 BoolVar tmp(*gi.currentSpace, 0, 1);
624 rel(*gi.currentSpace, BoolOpType::BOT_XOR, bv, tmp, GecodeSolverInstance::ann2icl(ann));
625 rel(*gi.currentSpace, gi.arg2boolvar(call->arg(1)), BoolOpType::BOT_IMP, tmp, 1);
626}
627void p_array_bool_clause(SolverInstanceBase& s, const Call* call) {
628 const Annotation& ann = call->ann();
629 auto& gi = static_cast<GecodeSolverInstance&>(s);
630 BoolVarArgs bvp = gi.arg2boolvarargs(call->arg(0));
631 BoolVarArgs bvn = gi.arg2boolvarargs(call->arg(1));
632 clause(*gi.currentSpace, BoolOpType::BOT_OR, bvp, bvn, 1, GecodeSolverInstance::ann2icl(ann));
633}
634void p_array_bool_clause_reif(SolverInstanceBase& s, const Call* call) {
635 const Annotation& ann = call->ann();
636 auto& gi = static_cast<GecodeSolverInstance&>(s);
637 BoolVarArgs bvp = gi.arg2boolvarargs(call->arg(0));
638 BoolVarArgs bvn = gi.arg2boolvarargs(call->arg(1));
639 BoolVar b0 = gi.arg2boolvar(call->arg(2));
640 clause(*gi.currentSpace, BoolOpType::BOT_OR, bvp, bvn, b0, GecodeSolverInstance::ann2icl(ann));
641}
642void p_array_bool_clause_imp(SolverInstanceBase& s, const Call* call) {
643 const Annotation& ann = call->ann();
644 auto& gi = static_cast<GecodeSolverInstance&>(s);
645 BoolVarArgs bvp = gi.arg2boolvarargs(call->arg(0));
646 BoolVarArgs bvn = gi.arg2boolvarargs(call->arg(1));
647 BoolVar b0 = gi.arg2boolvar(call->arg(2));
648 clause(*gi.currentSpace, BoolOpType::BOT_OR, bvp, bvn, b0, GecodeSolverInstance::ann2icl(ann));
649}
650void p_bool_xor(SolverInstanceBase& s, const Call* call) {
651 const Annotation& ann = call->ann();
652 auto& gi = static_cast<GecodeSolverInstance&>(s);
653 BOOL_OP(BoolOpType::BOT_XOR);
654}
655void p_bool_xor_imp(SolverInstanceBase& s, const Call* call) {
656 const Annotation& ann = call->ann();
657 auto& gi = static_cast<GecodeSolverInstance&>(s);
658 BoolVar b0 = gi.arg2boolvar(call->arg(0));
659 BoolVar b1 = gi.arg2boolvar(call->arg(1));
660 BoolVar b2 = gi.arg2boolvar(call->arg(2));
661 clause(*gi.currentSpace, BoolOpType::BOT_OR, BoolVarArgs() << b0 << b1, BoolVarArgs() << b2, 1,
662 GecodeSolverInstance::ann2icl(ann));
663 clause(*gi.currentSpace, BoolOpType::BOT_OR, BoolVarArgs(), BoolVarArgs() << b0 << b1 << b2, 1,
664 GecodeSolverInstance::ann2icl(ann));
665}
666void p_bool_l_imp(SolverInstanceBase& s, const Call* call) {
667 const Annotation& ann = call->ann();
668 auto& gi = static_cast<GecodeSolverInstance&>(s);
669 BoolVar b0 = gi.arg2boolvar(call->arg(0));
670 BoolVar b1 = gi.arg2boolvar(call->arg(1));
671 if (call->arg(2)->type().isbool()) {
672 rel(*gi.currentSpace, b1, BoolOpType::BOT_IMP, b0,
673 static_cast<int>(call->arg(2)->cast<BoolLit>()->v()), GecodeSolverInstance::ann2icl(ann));
674 } else {
675 rel(*gi.currentSpace, b1, BoolOpType::BOT_IMP, b0,
676 gi.resolveVar(call->arg(2)->cast<Id>()->decl()).boolVar(gi.currentSpace),
677 GecodeSolverInstance::ann2icl(ann));
678 }
679}
680void p_bool_r_imp(SolverInstanceBase& s, const Call* call) {
681 const Annotation& ann = call->ann();
682 auto& gi = static_cast<GecodeSolverInstance&>(s);
683 BOOL_OP(BoolOpType::BOT_IMP);
684}
685void p_bool_not(SolverInstanceBase& s, const Call* call) {
686 const Annotation& ann = call->ann();
687 auto& gi = static_cast<GecodeSolverInstance&>(s);
688 BoolVar x0 = gi.arg2boolvar(call->arg(0));
689 BoolVar x1 = gi.arg2boolvar(call->arg(1));
690 rel(*gi.currentSpace, x0, BoolOpType::BOT_XOR, x1, 1, GecodeSolverInstance::ann2icl(ann));
691}
692
693///* element constraints */
694void p_array_int_element(SolverInstanceBase& s, const Call* call) {
695 const Annotation& ann = call->ann();
696 auto& gi = static_cast<GecodeSolverInstance&>(s);
697 IntVar selector = gi.arg2intvar(call->arg(0));
698 rel(*gi.currentSpace, selector > 0);
699 if (call->arg(1)->type().isvar()) {
700 IntVarArgs iv = gi.arg2intvarargs(call->arg(1), 1);
701 element(*gi.currentSpace, iv, selector, gi.arg2intvar(call->arg(2)),
702 GecodeSolverInstance::ann2icl(ann));
703 } else {
704 IntArgs ia = GecodeSolverInstance::arg2intargs(call->arg(1), 1);
705 element(*gi.currentSpace, ia, selector, gi.arg2intvar(call->arg(2)),
706 GecodeSolverInstance::ann2icl(ann));
707 }
708}
709void p_array_bool_element(SolverInstanceBase& s, const Call* call) {
710 const Annotation& ann = call->ann();
711 auto& gi = static_cast<GecodeSolverInstance&>(s);
712 IntVar selector = gi.arg2intvar(call->arg(0));
713 rel(*gi.currentSpace, selector > 0);
714 if (call->arg(1)->type().isvar()) {
715 BoolVarArgs iv = gi.arg2boolvarargs(call->arg(1), 1);
716 element(*gi.currentSpace, iv, selector, gi.arg2boolvar(call->arg(2)),
717 GecodeSolverInstance::ann2icl(ann));
718 } else {
719 IntArgs ia = GecodeSolverInstance::arg2boolargs(call->arg(1), 1);
720 element(*gi.currentSpace, ia, selector, gi.arg2boolvar(call->arg(2)),
721 GecodeSolverInstance::ann2icl(ann));
722 }
723}
724
725///* coercion constraints */
726void p_bool2int(SolverInstanceBase& s, const Call* call) {
727 const Annotation& ann = call->ann();
728 auto& gi = static_cast<GecodeSolverInstance&>(s);
729 BoolVar x0 = gi.arg2boolvar(call->arg(0));
730 IntVar x1 = gi.arg2intvar(call->arg(1));
731 if (call->arg(0)->type().isvarbool() && call->arg(1)->type().isvarint()) {
732 unsigned int index = gi.resolveVar(call->arg(0)->cast<Id>()->decl()).index();
733 gi.resolveVar(call->arg(1)->cast<Id>()->decl()).setBoolAliasIndex(index);
734 }
735 channel(*gi.currentSpace, x0, x1, GecodeSolverInstance::ann2icl(ann));
736}
737
738void p_int_in(SolverInstanceBase& s, const Call* call) {
739 auto& gi = static_cast<GecodeSolverInstance&>(s);
740 IntSet d = gi.arg2intset(s.env().envi(), call->arg(1));
741 if (call->arg(0)->type().isvarbool()) {
742 Gecode::IntSetRanges dr(d);
743 Iter::Ranges::Singleton sr(0, 1);
744 Iter::Ranges::Inter<Gecode::IntSetRanges, Iter::Ranges::Singleton> i(dr, sr);
745 IntSet d01(i);
746 if (d01.size() == 0) {
747 gi.currentSpace->fail();
748 } else {
749 rel(*gi.currentSpace, gi.arg2boolvar(call->arg(0)), IRT_GQ, d01.min());
750 rel(*gi.currentSpace, gi.arg2boolvar(call->arg(0)), IRT_LQ, d01.max());
751 }
752 } else {
753 dom(*gi.currentSpace, gi.arg2intvar(call->arg(0)), d);
754 }
755}
756void p_int_in_reif(SolverInstanceBase& s, const Call* call) {
757 auto& gi = static_cast<GecodeSolverInstance&>(s);
758 IntSet d = gi.arg2intset(s.env().envi(), call->arg(1));
759 if (call->arg(0)->type().isvarbool()) {
760 Gecode::IntSetRanges dr(d);
761 Iter::Ranges::Singleton sr(0, 1);
762 Iter::Ranges::Inter<Gecode::IntSetRanges, Iter::Ranges::Singleton> i(dr, sr);
763 IntSet d01(i);
764 if (d01.size() == 0) {
765 rel(*gi.currentSpace, gi.arg2boolvar(call->arg(2)) == 0);
766 } else if (d01.max() == 0) {
767 rel(*gi.currentSpace, gi.arg2boolvar(call->arg(2)) == !gi.arg2boolvar(call->arg(0)));
768 } else if (d01.min() == 1) {
769 rel(*gi.currentSpace, gi.arg2boolvar(call->arg(2)) == gi.arg2boolvar(call->arg(0)));
770 } else {
771 rel(*gi.currentSpace, gi.arg2boolvar(call->arg(2)) == 1);
772 }
773 } else {
774 dom(*gi.currentSpace, gi.arg2intvar(call->arg(0)), d, gi.arg2boolvar(call->arg(2)));
775 }
776}
777void p_int_in_imp(SolverInstanceBase& s, const Call* call) {
778 auto& gi = static_cast<GecodeSolverInstance&>(s);
779 IntSet d = gi.arg2intset(s.env().envi(), call->arg(1));
780 if (call->arg(0)->type().isvarbool()) {
781 Gecode::IntSetRanges dr(d);
782 Iter::Ranges::Singleton sr(0, 1);
783 Iter::Ranges::Inter<Gecode::IntSetRanges, Iter::Ranges::Singleton> i(dr, sr);
784 IntSet d01(i);
785 if (d01.size() == 0) {
786 rel(*gi.currentSpace, gi.arg2boolvar(call->arg(2)) == 0);
787 } else if (d01.max() == 0) {
788 rel(*gi.currentSpace, gi.arg2boolvar(call->arg(2)) >> !gi.arg2boolvar(call->arg(0)));
789 } else if (d01.min() == 1) {
790 rel(*gi.currentSpace, gi.arg2boolvar(call->arg(2)) >> gi.arg2boolvar(call->arg(0)));
791 }
792 } else {
793 dom(*gi.currentSpace, gi.arg2intvar(call->arg(0)), d,
794 Reify(gi.arg2boolvar(call->arg(2)), RM_IMP));
795 }
796}
797
798///* constraints from the standard library */
799
800void p_abs(SolverInstanceBase& s, const Call* call) {
801 const Annotation& ann = call->ann();
802 auto& gi = static_cast<GecodeSolverInstance&>(s);
803 IntVar x0 = gi.arg2intvar(call->arg(0));
804 IntVar x1 = gi.arg2intvar(call->arg(1));
805 abs(*gi.currentSpace, x0, x1, GecodeSolverInstance::ann2icl(ann));
806}
807
808void p_array_int_lt(SolverInstanceBase& s, const Call* call) {
809 const Annotation& ann = call->ann();
810 auto& gi = static_cast<GecodeSolverInstance&>(s);
811 IntVarArgs iv0 = gi.arg2intvarargs(call->arg(0));
812 IntVarArgs iv1 = gi.arg2intvarargs(call->arg(1));
813 rel(*gi.currentSpace, iv0, IRT_LE, iv1, GecodeSolverInstance::ann2icl(ann));
814}
815
816void p_array_int_lq(SolverInstanceBase& s, const Call* call) {
817 const Annotation& ann = call->ann();
818 auto& gi = static_cast<GecodeSolverInstance&>(s);
819 IntVarArgs iv0 = gi.arg2intvarargs(call->arg(0));
820 IntVarArgs iv1 = gi.arg2intvarargs(call->arg(1));
821 rel(*gi.currentSpace, iv0, IRT_LQ, iv1, GecodeSolverInstance::ann2icl(ann));
822}
823
824void p_array_bool_lt(SolverInstanceBase& s, const Call* call) {
825 const Annotation& ann = call->ann();
826 auto& gi = static_cast<GecodeSolverInstance&>(s);
827 BoolVarArgs bv0 = gi.arg2boolvarargs(call->arg(0));
828 BoolVarArgs bv1 = gi.arg2boolvarargs(call->arg(1));
829 rel(*gi.currentSpace, bv0, IRT_LE, bv1, GecodeSolverInstance::ann2icl(ann));
830}
831
832void p_array_bool_lq(SolverInstanceBase& s, const Call* call) {
833 const Annotation& ann = call->ann();
834 auto& gi = static_cast<GecodeSolverInstance&>(s);
835 BoolVarArgs bv0 = gi.arg2boolvarargs(call->arg(0));
836 BoolVarArgs bv1 = gi.arg2boolvarargs(call->arg(1));
837 rel(*gi.currentSpace, bv0, IRT_LQ, bv1, GecodeSolverInstance::ann2icl(ann));
838}
839
840void p_count(SolverInstanceBase& s, const Call* call) {
841 const Annotation& ann = call->ann();
842 auto& gi = static_cast<GecodeSolverInstance&>(s);
843 IntVarArgs iv = gi.arg2intvarargs(call->arg(0));
844 if (!call->arg(1)->type().isvarint()) {
845 if (!call->arg(2)->type().isvarint()) {
846 count(*gi.currentSpace, iv, static_cast<int>(call->arg(1)->cast<IntLit>()->v().toInt()),
847 IRT_EQ, static_cast<int>(call->arg(2)->cast<IntLit>()->v().toInt()),
848 GecodeSolverInstance::ann2icl(ann));
849 } else {
850 count(*gi.currentSpace, iv, static_cast<int>(call->arg(1)->cast<IntLit>()->v().toInt()),
851 IRT_EQ, gi.arg2intvar(call->arg(2)), GecodeSolverInstance::ann2icl(ann));
852 }
853 } else if (!call->arg(2)->type().isvarint()) {
854 count(*gi.currentSpace, iv, gi.arg2intvar(call->arg(1)), IRT_EQ,
855 static_cast<int>(call->arg(2)->cast<IntLit>()->v().toInt()),
856 GecodeSolverInstance::ann2icl(ann));
857 } else {
858 count(*gi.currentSpace, iv, gi.arg2intvar(call->arg(1)), IRT_EQ, gi.arg2intvar(call->arg(2)),
859 GecodeSolverInstance::ann2icl(ann));
860 }
861}
862
863void p_count_reif(SolverInstanceBase& s, const Call* call) {
864 const Annotation& ann = call->ann();
865 auto& gi = static_cast<GecodeSolverInstance&>(s);
866 IntVarArgs iv = gi.arg2intvarargs(call->arg(0));
867 IntVar x = gi.arg2intvar(call->arg(1));
868 IntVar y = gi.arg2intvar(call->arg(2));
869 BoolVar b = gi.arg2boolvar(call->arg(3));
870 IntVar c(*gi.currentSpace, 0, Int::Limits::max);
871 count(*gi.currentSpace, iv, x, IRT_EQ, c, GecodeSolverInstance::ann2icl(ann));
872 rel(*gi.currentSpace, b == (c == y));
873}
874void p_count_imp(SolverInstanceBase& s, const Call* call) {
875 const Annotation& ann = call->ann();
876 auto& gi = static_cast<GecodeSolverInstance&>(s);
877 IntVarArgs iv = gi.arg2intvarargs(call->arg(0));
878 IntVar x = gi.arg2intvar(call->arg(1));
879 IntVar y = gi.arg2intvar(call->arg(2));
880 BoolVar b = gi.arg2boolvar(call->arg(3));
881 IntVar c(*gi.currentSpace, 0, Int::Limits::max);
882 count(*gi.currentSpace, iv, x, IRT_EQ, c, GecodeSolverInstance::ann2icl(ann));
883 rel(*gi.currentSpace, b >> (c == y));
884}
885
886void count_rel(IntRelType irt, SolverInstanceBase& s, const Call* call) {
887 const Annotation& ann = call->ann();
888 auto& gi = static_cast<GecodeSolverInstance&>(s);
889 IntVarArgs iv = gi.arg2intvarargs(call->arg(1));
890 count(*gi.currentSpace, iv, static_cast<int>(call->arg(2)->cast<IntLit>()->v().toInt()), irt,
891 static_cast<int>(call->arg(0)->cast<IntLit>()->v().toInt()),
892 GecodeSolverInstance::ann2icl(ann));
893}
894
895void p_at_most(SolverInstanceBase& s, const Call* call) { count_rel(IRT_LQ, s, call); }
896
897void p_at_least(SolverInstanceBase& s, const Call* call) { count_rel(IRT_GQ, s, call); }
898
899void p_bin_packing_load(SolverInstanceBase& s, const Call* call) {
900 const Annotation& ann = call->ann();
901 auto& gi = static_cast<GecodeSolverInstance&>(s);
902 int minIdx = static_cast<int>(call->arg(3)->cast<IntLit>()->v().toInt());
903 IntVarArgs load = gi.arg2intvarargs(call->arg(0));
904 IntVarArgs l;
905 IntVarArgs bin = gi.arg2intvarargs(call->arg(1));
906 for (int i = bin.size(); (i--) != 0;) {
907 rel(*gi.currentSpace, bin[i] >= minIdx);
908 }
909 if (minIdx > 0) {
910 for (int i = minIdx; (i--) != 0;) {
911 l << IntVar(*gi.currentSpace, 0, 0);
912 }
913 } else if (minIdx < 0) {
914 IntVarArgs bin2(bin.size());
915 for (int i = bin.size(); (i--) != 0;) {
916 bin2[i] = expr(*gi.currentSpace, bin[i] - minIdx, GecodeSolverInstance::ann2icl(ann));
917 }
918 bin = bin2;
919 }
920 l << load;
921 IntArgs sizes = GecodeSolverInstance::arg2intargs(call->arg(2));
922
923 IntVarArgs allvars = l + bin;
924 unshare(*gi.currentSpace, allvars);
925 binpacking(*gi.currentSpace, allvars.slice(0, 1, l.size()),
926 allvars.slice(l.size(), 1, bin.size()), sizes, GecodeSolverInstance::ann2icl(ann));
927}
928
929void p_global_cardinality(SolverInstanceBase& s, const Call* call) {
930 const Annotation& ann = call->ann();
931 auto& gi = static_cast<GecodeSolverInstance&>(s);
932 IntVarArgs iv0 = gi.arg2intvarargs(call->arg(0));
933 IntArgs cover = GecodeSolverInstance::arg2intargs(call->arg(1));
934 IntVarArgs iv1 = gi.arg2intvarargs(call->arg(2));
935
936 Region re;
937 IntSet cover_s(cover);
938 Gecode::IntSetRanges cover_r(cover_s);
939 auto* iv0_ri = re.alloc<Gecode::IntVarRanges>(iv0.size());
940 for (int i = iv0.size(); (i--) != 0;) {
941 iv0_ri[i] = Gecode::IntVarRanges(iv0[i]);
942 }
943 Iter::Ranges::NaryUnion iv0_r(re, iv0_ri, iv0.size());
944 Iter::Ranges::Diff<Iter::Ranges::NaryUnion, Gecode::IntSetRanges> extra_r(iv0_r, cover_r);
945 Iter::Ranges::ToValues<Iter::Ranges::Diff<Iter::Ranges::NaryUnion, Gecode::IntSetRanges> > extra(
946 extra_r);
947 for (; extra(); ++extra) {
948 cover << extra.val();
949 iv1 << IntVar(*gi.currentSpace, 0, iv0.size());
950 }
951
952 MZ_IntConLevel icl = GecodeSolverInstance::ann2icl(ann);
953 if (icl == MZ_ICL_DOM) {
954 IntVarArgs allvars = iv0 + iv1;
955 unshare(*gi.currentSpace, allvars);
956 count(*gi.currentSpace, allvars.slice(0, 1, iv0.size()),
957 allvars.slice(iv0.size(), 1, iv1.size()), cover, GecodeSolverInstance::ann2icl(ann));
958 } else {
959 unshare(*gi.currentSpace, iv0);
960 count(*gi.currentSpace, iv0, iv1, cover, GecodeSolverInstance::ann2icl(ann));
961 }
962}
963
964void p_global_cardinality_closed(SolverInstanceBase& s, const Call* call) {
965 const Annotation& ann = call->ann();
966 auto& gi = static_cast<GecodeSolverInstance&>(s);
967 IntVarArgs iv0 = gi.arg2intvarargs(call->arg(0));
968 IntArgs cover = GecodeSolverInstance::arg2intargs(call->arg(1));
969 IntVarArgs iv1 = gi.arg2intvarargs(call->arg(2));
970 unshare(*gi.currentSpace, iv0);
971 count(*gi.currentSpace, iv0, iv1, cover, GecodeSolverInstance::ann2icl(ann));
972}
973
974void p_global_cardinality_low_up(SolverInstanceBase& s, const Call* call) {
975 const Annotation& ann = call->ann();
976 auto& gi = static_cast<GecodeSolverInstance&>(s);
977 IntVarArgs x = gi.arg2intvarargs(call->arg(0));
978 IntArgs cover = GecodeSolverInstance::arg2intargs(call->arg(1));
979
980 IntArgs lbound = GecodeSolverInstance::arg2intargs(call->arg(2));
981 IntArgs ubound = GecodeSolverInstance::arg2intargs(call->arg(3));
982 IntSetArgs y(cover.size());
983 for (int i = cover.size(); (i--) != 0;) {
984 y[i] = IntSet(lbound[i], ubound[i]);
985 }
986
987 IntSet cover_s(cover);
988 Region re;
989 auto* xrs = re.alloc<IntVarRanges>(x.size());
990 for (int i = x.size(); (i--) != 0;) {
991 xrs[i].init(x[i]);
992 }
993 Iter::Ranges::NaryUnion u(re, xrs, x.size());
994 Iter::Ranges::ToValues<Iter::Ranges::NaryUnion> uv(u);
995 for (; uv(); ++uv) {
996 if (!cover_s.in(uv.val())) {
997 cover << uv.val();
998 y << IntSet(0, x.size());
999 }
1000 }
1001
1002 unshare(*gi.currentSpace, x);
1003 count(*gi.currentSpace, x, y, cover, GecodeSolverInstance::ann2icl(ann));
1004}
1005
1006void p_global_cardinality_low_up_closed(SolverInstanceBase& s, const Call* call) {
1007 const Annotation& ann = call->ann();
1008 auto& gi = static_cast<GecodeSolverInstance&>(s);
1009 IntVarArgs x = gi.arg2intvarargs(call->arg(0));
1010 IntArgs cover = GecodeSolverInstance::arg2intargs(call->arg(1));
1011
1012 IntArgs lbound = GecodeSolverInstance::arg2intargs(call->arg(2));
1013 IntArgs ubound = GecodeSolverInstance::arg2intargs(call->arg(3));
1014 IntSetArgs y(cover.size());
1015 for (int i = cover.size(); (i--) != 0;) {
1016 y[i] = IntSet(lbound[i], ubound[i]);
1017 }
1018
1019 unshare(*gi.currentSpace, x);
1020 count(*gi.currentSpace, x, y, cover, GecodeSolverInstance::ann2icl(ann));
1021}
1022
1023void p_minimum(SolverInstanceBase& s, const Call* call) {
1024 const Annotation& ann = call->ann();
1025 auto& gi = static_cast<GecodeSolverInstance&>(s);
1026 IntVarArgs iv = gi.arg2intvarargs(call->arg(1));
1027 min(*gi.currentSpace, iv, gi.arg2intvar(call->arg(0)), GecodeSolverInstance::ann2icl(ann));
1028}
1029
1030void p_maximum(SolverInstanceBase& s, const Call* call) {
1031 const Annotation& ann = call->ann();
1032 auto& gi = static_cast<GecodeSolverInstance&>(s);
1033 IntVarArgs iv = gi.arg2intvarargs(call->arg(1));
1034 max(*gi.currentSpace, iv, gi.arg2intvar(call->arg(0)), GecodeSolverInstance::ann2icl(ann));
1035}
1036
1037void p_maximum_arg(SolverInstanceBase& s, const Call* call) {
1038 const Annotation& ann = call->ann();
1039 auto& gi = static_cast<GecodeSolverInstance&>(s);
1040 IntVarArgs iv = gi.arg2intvarargs(call->arg(0));
1041 argmax(*gi.currentSpace, iv, gi.arg2intvar(call->arg(1)), true,
1042 GecodeSolverInstance::ann2icl(ann));
1043}
1044
1045void p_minimum_arg(SolverInstanceBase& s, const Call* call) {
1046 const Annotation& ann = call->ann();
1047 auto& gi = static_cast<GecodeSolverInstance&>(s);
1048 IntVarArgs iv = gi.arg2intvarargs(call->arg(0));
1049 argmin(*gi.currentSpace, iv, gi.arg2intvar(call->arg(1)), true,
1050 GecodeSolverInstance::ann2icl(ann));
1051}
1052
1053void p_regular(SolverInstanceBase& s, const Call* call) {
1054 const Annotation& ann = call->ann();
1055 auto& gi = static_cast<GecodeSolverInstance&>(s);
1056 IntVarArgs iv = gi.arg2intvarargs(call->arg(0));
1057 int q = static_cast<int>(call->arg(1)->cast<IntLit>()->v().toInt());
1058 int symbols = static_cast<int>(call->arg(2)->cast<IntLit>()->v().toInt());
1059 IntArgs d = GecodeSolverInstance::arg2intargs(call->arg(3));
1060 int q0 = static_cast<int>(call->arg(4)->cast<IntLit>()->v().toInt());
1061
1062 int noOfTrans = 0;
1063 for (int i = 1; i <= q; i++) {
1064 for (int j = 1; j <= symbols; j++) {
1065 if (d[(i - 1) * symbols + (j - 1)] > 0) {
1066 noOfTrans++;
1067 }
1068 }
1069 }
1070
1071 Region re;
1072 auto* t = re.alloc<DFA::Transition>(noOfTrans + 1);
1073 noOfTrans = 0;
1074 for (int i = 1; i <= q; i++) {
1075 for (int j = 1; j <= symbols; j++) {
1076 if (d[(i - 1) * symbols + (j - 1)] > 0) {
1077 t[noOfTrans].i_state = i;
1078 t[noOfTrans].symbol = j;
1079 t[noOfTrans].o_state = d[(i - 1) * symbols + (j - 1)];
1080 noOfTrans++;
1081 }
1082 }
1083 }
1084 t[noOfTrans].i_state = -1;
1085
1086 // Final states
1087 IntSetVal* isv = eval_intset(s.env().envi(), call->arg(5));
1088 IntSetRanges isr(isv);
1089
1090 int* f = static_cast<int*>(malloc(sizeof(int) * (isv->card().toInt()) + 1));
1091 int i = 0;
1092 for (Ranges::ToValues<IntSetRanges> val_iter(isr); val_iter(); ++val_iter, ++i) {
1093 f[i] = static_cast<int>(val_iter.val().toInt());
1094 }
1095 f[i] = -1;
1096
1097 DFA dfa(q0, t, f);
1098 free(f);
1099 unshare(*gi.currentSpace, iv);
1100 extensional(*gi.currentSpace, iv, dfa, GecodeSolverInstance::ann2icl(ann));
1101}
1102
1103void p_sort(SolverInstanceBase& s, const Call* call) {
1104 const Annotation& ann = call->ann();
1105 auto& gi = static_cast<GecodeSolverInstance&>(s);
1106 IntVarArgs x = gi.arg2intvarargs(call->arg(0));
1107 IntVarArgs y = gi.arg2intvarargs(call->arg(1));
1108 IntVarArgs xy(x.size() + y.size());
1109 for (int i = x.size(); (i--) != 0;) {
1110 xy[i] = x[i];
1111 }
1112 for (int i = y.size(); (i--) != 0;) {
1113 xy[i + x.size()] = y[i];
1114 }
1115 unshare(*gi.currentSpace, xy);
1116 for (int i = x.size(); (i--) != 0;) {
1117 x[i] = xy[i];
1118 }
1119 for (int i = y.size(); (i--) != 0;) {
1120 y[i] = xy[i + x.size()];
1121 }
1122 sorted(*gi.currentSpace, x, y, GecodeSolverInstance::ann2icl(ann));
1123}
1124
1125void p_inverse_offsets(SolverInstanceBase& s, const Call* call) {
1126 auto& gi = static_cast<GecodeSolverInstance&>(s);
1127 IntVarArgs x = gi.arg2intvarargs(call->arg(0));
1128 unshare(*gi.currentSpace, x);
1129 int xoff = static_cast<int>(call->arg(1)->cast<IntLit>()->v().toInt());
1130 IntVarArgs y = gi.arg2intvarargs(call->arg(2));
1131 unshare(*gi.currentSpace, y);
1132 int yoff = static_cast<int>(call->arg(3)->cast<IntLit>()->v().toInt());
1133 MZ_IntConLevel icl = GecodeSolverInstance::ann2icl(call->ann());
1134 channel(*gi.currentSpace, x, xoff, y, yoff, icl == MZ_ICL_DEF ? MZ_ICL_DOM : icl);
1135}
1136
1137void p_increasing_int(SolverInstanceBase& s, const Call* call) {
1138 const Annotation& ann = call->ann();
1139 auto& gi = static_cast<GecodeSolverInstance&>(s);
1140 IntVarArgs x = gi.arg2intvarargs(call->arg(0));
1141 rel(*gi.currentSpace, x, IRT_LQ, GecodeSolverInstance::ann2icl(ann));
1142}
1143
1144void p_increasing_bool(SolverInstanceBase& s, const Call* call) {
1145 const Annotation& ann = call->ann();
1146 auto& gi = static_cast<GecodeSolverInstance&>(s);
1147 BoolVarArgs x = gi.arg2boolvarargs(call->arg(0));
1148 rel(*gi.currentSpace, x, IRT_LQ, GecodeSolverInstance::ann2icl(ann));
1149}
1150
1151void p_decreasing_int(SolverInstanceBase& s, const Call* call) {
1152 const Annotation& ann = call->ann();
1153 auto& gi = static_cast<GecodeSolverInstance&>(s);
1154 IntVarArgs x = gi.arg2intvarargs(call->arg(0));
1155 rel(*gi.currentSpace, x, IRT_GQ, GecodeSolverInstance::ann2icl(ann));
1156}
1157
1158void p_decreasing_bool(SolverInstanceBase& s, const Call* call) {
1159 const Annotation& ann = call->ann();
1160 auto& gi = static_cast<GecodeSolverInstance&>(s);
1161 BoolVarArgs x = gi.arg2boolvarargs(call->arg(0));
1162 rel(*gi.currentSpace, x, IRT_GQ, GecodeSolverInstance::ann2icl(ann));
1163}
1164
1165void p_table_int(SolverInstanceBase& s, const Call* call) {
1166 const Annotation& ann = call->ann();
1167 auto& gi = static_cast<GecodeSolverInstance&>(s);
1168 IntVarArgs x = gi.arg2intvarargs(call->arg(0));
1169 IntArgs tuples = GecodeSolverInstance::arg2intargs(call->arg(1));
1170 int noOfVars = x.size();
1171 int noOfTuples = tuples.size() == 0 ? 0 : (tuples.size() / noOfVars);
1172 TupleSet ts(noOfVars);
1173 for (int i = 0; i < noOfTuples; i++) {
1174 IntArgs t(noOfVars);
1175 for (int j = 0; j < x.size(); j++) {
1176 t[j] = tuples[i * noOfVars + j];
1177 }
1178 ts.add(t);
1179 }
1180 ts.finalize();
1181 extensional(*gi.currentSpace, x, ts, GecodeSolverInstance::ann2icl(ann));
1182}
1183void p_table_bool(SolverInstanceBase& s, const Call* call) {
1184 const Annotation& ann = call->ann();
1185 auto& gi = static_cast<GecodeSolverInstance&>(s);
1186 BoolVarArgs x = gi.arg2boolvarargs(call->arg(0));
1187 IntArgs tuples = GecodeSolverInstance::arg2boolargs(call->arg(1));
1188 int noOfVars = x.size();
1189 int noOfTuples = tuples.size() == 0 ? 0 : (tuples.size() / noOfVars);
1190 TupleSet ts(noOfVars);
1191 for (int i = 0; i < noOfTuples; i++) {
1192 IntArgs t(noOfVars);
1193 for (int j = 0; j < x.size(); j++) {
1194 t[j] = tuples[i * noOfVars + j];
1195 }
1196 ts.add(t);
1197 }
1198 ts.finalize();
1199 extensional(*gi.currentSpace, x, ts, GecodeSolverInstance::ann2icl(ann));
1200}
1201
1202void p_cumulatives(SolverInstanceBase& s, const Call* call) {
1203 const Annotation& ann = call->ann();
1204 auto& gi = static_cast<GecodeSolverInstance&>(s);
1205 IntVarArgs start = gi.arg2intvarargs(call->arg(0));
1206 IntVarArgs duration = gi.arg2intvarargs(call->arg(1));
1207 IntVarArgs height = gi.arg2intvarargs(call->arg(2));
1208 int n = start.size();
1209 IntVar bound = gi.arg2intvar(call->arg(3));
1210
1211 int minHeight = INT_MAX;
1212 int minHeight2 = INT_MAX;
1213 for (int i = n; (i--) != 0;) {
1214 if (height[i].min() < minHeight) {
1215 minHeight = height[i].min();
1216 } else if (height[i].min() < minHeight2) {
1217 minHeight2 = height[i].min();
1218 }
1219 }
1220 bool disjunctive = (minHeight > bound.max() / 2) ||
1221 (minHeight2 > bound.max() / 2 && minHeight + minHeight2 > bound.max());
1222 if (disjunctive) {
1223 rel(*gi.currentSpace, bound >= max(height));
1224 // Unary
1225 if (duration.assigned()) {
1226 IntArgs durationI(n);
1227 for (int i = n; (i--) != 0;) {
1228 durationI[i] = duration[i].val();
1229 }
1230 unshare(*gi.currentSpace, start);
1231 unary(*gi.currentSpace, start, durationI);
1232 } else {
1233 IntVarArgs end(n);
1234 for (int i = n; (i--) != 0;) {
1235 end[i] = expr(*gi.currentSpace, start[i] + duration[i]);
1236 }
1237 unshare(*gi.currentSpace, start);
1238 unary(*gi.currentSpace, start, duration, end);
1239 }
1240 } else if (height.assigned()) {
1241 IntArgs heightI(n);
1242 for (int i = n; (i--) != 0;) {
1243 heightI[i] = height[i].val();
1244 }
1245 if (duration.assigned()) {
1246 IntArgs durationI(n);
1247 for (int i = n; (i--) != 0;) {
1248 durationI[i] = duration[i].val();
1249 }
1250 cumulative(*gi.currentSpace, bound, start, durationI, heightI);
1251 } else {
1252 IntVarArgs end(n);
1253 for (int i = n; (i--) != 0;) {
1254 end[i] = expr(*gi.currentSpace, start[i] + duration[i]);
1255 }
1256 cumulative(*gi.currentSpace, bound, start, duration, end, heightI);
1257 }
1258 } else if (bound.assigned()) {
1259 IntArgs machine = IntArgs::create(n, 0, 0);
1260 IntArgs limit({bound.val()});
1261 IntVarArgs end(n);
1262 for (int i = n; (i--) != 0;) {
1263 end[i] = expr(*gi.currentSpace, start[i] + duration[i]);
1264 }
1265 cumulatives(*gi.currentSpace, machine, start, duration, end, height, limit, true,
1266 GecodeSolverInstance::ann2icl(ann));
1267 } else {
1268 int min = Gecode::Int::Limits::max;
1269 int max = Gecode::Int::Limits::min;
1270 IntVarArgs end(start.size());
1271 for (int i = start.size(); (i--) != 0;) {
1272 min = std::min(min, start[i].min());
1273 max = std::max(max, start[i].max() + duration[i].max());
1274 end[i] = expr(*gi.currentSpace, start[i] + duration[i]);
1275 }
1276 for (int time = min; time < max; ++time) {
1277 IntVarArgs x(start.size());
1278 for (int i = start.size(); (i--) != 0;) {
1279 IntVar overlaps = channel(*gi.currentSpace,
1280 expr(*gi.currentSpace, (start[i] <= time) && (time < end[i])));
1281 x[i] = expr(*gi.currentSpace, overlaps * height[i]);
1282 }
1283 linear(*gi.currentSpace, x, IRT_LQ, bound);
1284 }
1285 }
1286}
1287
1288void p_among_seq_int(SolverInstanceBase& s, const Call* call) {
1289 const Annotation& ann = call->ann();
1290 auto& gi = static_cast<GecodeSolverInstance&>(s);
1291 Gecode::IntVarArgs x = gi.arg2intvarargs(call->arg(0));
1292 IntSet S = gi.arg2intset(s.env().envi(), call->arg(1));
1293 int q = static_cast<int>(call->arg(2)->cast<IntLit>()->v().toInt());
1294 int l = static_cast<int>(call->arg(3)->cast<IntLit>()->v().toInt());
1295 int u = static_cast<int>(call->arg(4)->cast<IntLit>()->v().toInt());
1296 unshare(*gi.currentSpace, x);
1297 sequence(*gi.currentSpace, x, S, q, l, u, GecodeSolverInstance::ann2icl(ann));
1298}
1299
1300void p_among_seq_bool(SolverInstanceBase& s, const Call* call) {
1301 const Annotation& ann = call->ann();
1302 auto& gi = static_cast<GecodeSolverInstance&>(s);
1303 BoolVarArgs x = gi.arg2boolvarargs(call->arg(0));
1304 bool val = call->arg(1)->cast<BoolLit>()->v();
1305 int q = static_cast<int>(call->arg(2)->cast<IntLit>()->v().toInt());
1306 int l = static_cast<int>(call->arg(3)->cast<IntLit>()->v().toInt());
1307 int u = static_cast<int>(call->arg(4)->cast<IntLit>()->v().toInt());
1308 IntSet S(static_cast<int>(val), static_cast<int>(val));
1309 unshare(*gi.currentSpace, x);
1310 sequence(*gi.currentSpace, x, S, q, l, u, GecodeSolverInstance::ann2icl(ann));
1311}
1312
1313void p_schedule_unary(SolverInstanceBase& s, const Call* call) {
1314 auto& gi = static_cast<GecodeSolverInstance&>(s);
1315 IntVarArgs x = gi.arg2intvarargs(call->arg(0));
1316 IntArgs p = GecodeSolverInstance::arg2intargs(call->arg(1));
1317 unshare(*gi.currentSpace, x);
1318 unary(*gi.currentSpace, x, p);
1319}
1320
1321void p_schedule_unary_optional(SolverInstanceBase& s, const Call* call) {
1322 auto& gi = static_cast<GecodeSolverInstance&>(s);
1323 IntVarArgs x = gi.arg2intvarargs(call->arg(0));
1324 IntArgs p = GecodeSolverInstance::arg2intargs(call->arg(1));
1325 BoolVarArgs m = gi.arg2boolvarargs(call->arg(2));
1326 unshare(*gi.currentSpace, x);
1327 unary(*gi.currentSpace, x, p, m);
1328}
1329
1330void p_cumulative_opt(SolverInstanceBase& s, const Call* ce) {
1331 const Annotation& ann = ce->ann();
1332 auto& gi = static_cast<GecodeSolverInstance&>(s);
1333 IntVarArgs start = gi.arg2intvarargs(ce->arg(0));
1334 IntArgs duration = GecodeSolverInstance::arg2intargs(ce->arg(1));
1335 IntArgs height = GecodeSolverInstance::arg2intargs(ce->arg(2));
1336 BoolVarArgs opt = gi.arg2boolvarargs(ce->arg(3));
1337 int bound = static_cast<int>(ce->arg(4)->cast<IntLit>()->v().toInt());
1338 unshare(*gi.currentSpace, start);
1339 cumulative(*gi.currentSpace, bound, start, duration, height, opt,
1340 GecodeSolverInstance::ann2icl(ann));
1341}
1342
1343void p_circuit(SolverInstanceBase& s, const Call* call) {
1344 const Annotation& ann = call->ann();
1345 auto& gi = static_cast<GecodeSolverInstance&>(s);
1346 int off = static_cast<int>(call->arg(0)->cast<IntLit>()->v().toInt());
1347 IntVarArgs xv = gi.arg2intvarargs(call->arg(1));
1348 unshare(*gi.currentSpace, xv);
1349 circuit(*gi.currentSpace, off, xv, GecodeSolverInstance::ann2icl(ann));
1350}
1351void p_circuit_cost_array(SolverInstanceBase& s, const Call* call) {
1352 const Annotation& ann = call->ann();
1353 auto& gi = static_cast<GecodeSolverInstance&>(s);
1354 IntArgs c = GecodeSolverInstance::arg2intargs(call->arg(0));
1355 IntVarArgs xv = gi.arg2intvarargs(call->arg(1));
1356 IntVarArgs yv = gi.arg2intvarargs(call->arg(2));
1357 IntVar z = gi.arg2intvar(call->arg(3));
1358 unshare(*gi.currentSpace, xv);
1359 circuit(*gi.currentSpace, c, xv, yv, z, GecodeSolverInstance::ann2icl(ann));
1360}
1361void p_circuit_cost(SolverInstanceBase& s, const Call* call) {
1362 const Annotation& ann = call->ann();
1363 auto& gi = static_cast<GecodeSolverInstance&>(s);
1364 IntArgs c = GecodeSolverInstance::arg2intargs(call->arg(0));
1365 IntVarArgs xv = gi.arg2intvarargs(call->arg(1));
1366 IntVar z = gi.arg2intvar(call->arg(2));
1367 unshare(*gi.currentSpace, xv);
1368 circuit(*gi.currentSpace, c, xv, z, GecodeSolverInstance::ann2icl(ann));
1369}
1370
1371void p_nooverlap(SolverInstanceBase& s, const Call* call) {
1372 const Annotation& ann = call->ann();
1373 auto& gi = static_cast<GecodeSolverInstance&>(s);
1374 IntVarArgs x0 = gi.arg2intvarargs(call->arg(0));
1375 IntVarArgs w = gi.arg2intvarargs(call->arg(1));
1376 IntVarArgs y0 = gi.arg2intvarargs(call->arg(2));
1377 IntVarArgs h = gi.arg2intvarargs(call->arg(3));
1378 if (w.assigned() && h.assigned()) {
1379 IntArgs iw(w.size());
1380 for (int i = w.size(); (i--) != 0;) {
1381 iw[i] = w[i].val();
1382 }
1383 IntArgs ih(h.size());
1384 for (int i = h.size(); (i--) != 0;) {
1385 ih[i] = h[i].val();
1386 }
1387 nooverlap(*gi.currentSpace, x0, iw, y0, ih, GecodeSolverInstance::ann2icl(ann));
1388 } else {
1389 IntVarArgs x1(x0.size());
1390 IntVarArgs y1(y0.size());
1391 for (int i = x0.size(); (i--) != 0;) {
1392 x1[i] = expr(*gi.currentSpace, x0[i] + w[i]);
1393 }
1394 for (int i = y0.size(); (i--) != 0;) {
1395 y1[i] = expr(*gi.currentSpace, y0[i] + h[i]);
1396 }
1397 nooverlap(*gi.currentSpace, x0, w, x1, y0, h, y1, GecodeSolverInstance::ann2icl(ann));
1398 }
1399}
1400
1401void p_precede(SolverInstanceBase& s, const Call* call) {
1402 const Annotation& ann = call->ann();
1403 auto& gi = static_cast<GecodeSolverInstance&>(s);
1404 IntVarArgs x = gi.arg2intvarargs(call->arg(0));
1405 int p_s = static_cast<int>(call->arg(1)->cast<IntLit>()->v().toInt());
1406 int p_t = static_cast<int>(call->arg(2)->cast<IntLit>()->v().toInt());
1407 precede(*gi.currentSpace, x, p_s, p_t, GecodeSolverInstance::ann2icl(ann));
1408}
1409
1410void p_nvalue(SolverInstanceBase& s, const Call* call) {
1411 const Annotation& ann = call->ann();
1412 auto& gi = static_cast<GecodeSolverInstance&>(s);
1413 IntVarArgs x = gi.arg2intvarargs(call->arg(1));
1414 if (call->arg(0)->type().isvarint()) {
1415 IntVar y = gi.arg2intvar(call->arg(0));
1416 nvalues(*gi.currentSpace, x, IRT_EQ, y, GecodeSolverInstance::ann2icl(ann));
1417 } else {
1418 nvalues(*gi.currentSpace, x, IRT_EQ,
1419 static_cast<int>(call->arg(0)->cast<IntLit>()->v().toInt()),
1420 GecodeSolverInstance::ann2icl(ann));
1421 }
1422}
1423
1424void p_among(SolverInstanceBase& s, const Call* call) {
1425 const Annotation& ann = call->ann();
1426 auto& gi = static_cast<GecodeSolverInstance&>(s);
1427 IntVarArgs x = gi.arg2intvarargs(call->arg(1));
1428 IntSet v = gi.arg2intset(s.env().envi(), call->arg(2));
1429 if (call->arg(0)->type().isvarint()) {
1430 IntVar n = gi.arg2intvar(call->arg(0));
1431 unshare(*gi.currentSpace, x);
1432 count(*gi.currentSpace, x, v, IRT_EQ, n, GecodeSolverInstance::ann2icl(ann));
1433 } else {
1434 unshare(*gi.currentSpace, x);
1435 count(*gi.currentSpace, x, v, IRT_EQ,
1436 static_cast<int>(call->arg(0)->cast<IntLit>()->v().toInt()),
1437 GecodeSolverInstance::ann2icl(ann));
1438 }
1439}
1440
1441void p_member_int(SolverInstanceBase& s, const Call* call) {
1442 const Annotation& ann = call->ann();
1443 auto& gi = static_cast<GecodeSolverInstance&>(s);
1444 IntVarArgs x = gi.arg2intvarargs(call->arg(0));
1445 IntVar y = gi.arg2intvar(call->arg(1));
1446 member(*gi.currentSpace, x, y, GecodeSolverInstance::ann2icl(ann));
1447}
1448void p_member_int_reif(SolverInstanceBase& s, const Call* call) {
1449 const Annotation& ann = call->ann();
1450 auto& gi = static_cast<GecodeSolverInstance&>(s);
1451 IntVarArgs x = gi.arg2intvarargs(call->arg(0));
1452 IntVar y = gi.arg2intvar(call->arg(1));
1453 BoolVar b = gi.arg2boolvar(call->arg(2));
1454 member(*gi.currentSpace, x, y, b, GecodeSolverInstance::ann2icl(ann));
1455}
1456void p_member_bool(SolverInstanceBase& s, const Call* call) {
1457 const Annotation& ann = call->ann();
1458 auto& gi = static_cast<GecodeSolverInstance&>(s);
1459 BoolVarArgs x = gi.arg2boolvarargs(call->arg(0));
1460 BoolVar y = gi.arg2boolvar(call->arg(1));
1461 member(*gi.currentSpace, x, y, GecodeSolverInstance::ann2icl(ann));
1462}
1463void p_member_bool_reif(SolverInstanceBase& s, const Call* call) {
1464 const Annotation& ann = call->ann();
1465 auto& gi = static_cast<GecodeSolverInstance&>(s);
1466 BoolVarArgs x = gi.arg2boolvarargs(call->arg(0));
1467 BoolVar y = gi.arg2boolvar(call->arg(1));
1468 member(*gi.currentSpace, x, y, gi.arg2boolvar(call->arg(2)), GecodeSolverInstance::ann2icl(ann));
1469}
1470
1471// FLOAT CONSTRAINTS
1472#ifdef GECODE_HAS_FLOAT_VARS
1473
1474void p_int2float(SolverInstanceBase& s, const Call* ce) {
1475 auto& gi = static_cast<GecodeSolverInstance&>(s);
1476 IntVar x0 = gi.arg2intvar(ce->arg(0));
1477 FloatVar x1 = gi.arg2floatvar(ce->arg(1));
1478 channel(*gi.currentSpace, x0, x1);
1479}
1480
1481void p_float_lin_cmp(GecodeSolverInstance& s, FloatRelType frt, const Call* ce) {
1482 FloatValArgs fa = GecodeSolverInstance::arg2floatargs(ce->arg(0));
1483 FloatVarArgs fv = s.arg2floatvarargs(ce->arg(1));
1484 linear(*s.currentSpace, fa, fv, frt, ce->arg(2)->cast<FloatLit>()->v().toDouble());
1485}
1486void p_float_lin_cmp_reif(GecodeSolverInstance& s, FloatRelType frt, const Call* ce) {
1487 FloatValArgs fa = GecodeSolverInstance::arg2floatargs(ce->arg(0));
1488 FloatVarArgs fv = s.arg2floatvarargs(ce->arg(1));
1489 linear(*s.currentSpace, fa, fv, frt, ce->arg(2)->cast<FloatLit>()->v().toDouble(),
1490 s.arg2boolvar(ce->arg(3)));
1491}
1492void p_float_lin_eq(SolverInstanceBase& s, const Call* ce) {
1493 auto& gi = static_cast<GecodeSolverInstance&>(s);
1494 p_float_lin_cmp(gi, FRT_EQ, ce);
1495}
1496void p_float_lin_eq_reif(SolverInstanceBase& s, const Call* ce) {
1497 auto& gi = static_cast<GecodeSolverInstance&>(s);
1498 p_float_lin_cmp_reif(gi, FRT_EQ, ce);
1499}
1500void p_float_lin_le(SolverInstanceBase& s, const Call* ce) {
1501 auto& gi = static_cast<GecodeSolverInstance&>(s);
1502 p_float_lin_cmp(gi, FRT_LQ, ce);
1503}
1504void p_float_lin_le_reif(SolverInstanceBase& s, const Call* ce) {
1505 auto& gi = static_cast<GecodeSolverInstance&>(s);
1506 p_float_lin_cmp_reif(gi, FRT_LQ, ce);
1507}
1508
1509void p_float_times(SolverInstanceBase& s, const Call* ce) {
1510 auto& gi = static_cast<GecodeSolverInstance&>(s);
1511 FloatVar x = gi.arg2floatvar(ce->arg(0));
1512 FloatVar y = gi.arg2floatvar(ce->arg(1));
1513 FloatVar z = gi.arg2floatvar(ce->arg(2));
1514 mult(*gi.currentSpace, x, y, z);
1515}
1516
1517void p_float_div(SolverInstanceBase& s, const Call* ce) {
1518 auto& gi = static_cast<GecodeSolverInstance&>(s);
1519 FloatVar x = gi.arg2floatvar(ce->arg(0));
1520 FloatVar y = gi.arg2floatvar(ce->arg(1));
1521 FloatVar z = gi.arg2floatvar(ce->arg(2));
1522 div(*gi.currentSpace, x, y, z);
1523}
1524
1525void p_float_plus(SolverInstanceBase& s, const Call* ce) {
1526 auto& gi = static_cast<GecodeSolverInstance&>(s);
1527 FloatVar x = gi.arg2floatvar(ce->arg(0));
1528 FloatVar y = gi.arg2floatvar(ce->arg(1));
1529 FloatVar z = gi.arg2floatvar(ce->arg(2));
1530 rel(*gi.currentSpace, x + y == z);
1531}
1532
1533void p_float_sqrt(SolverInstanceBase& s, const Call* ce) {
1534 auto& gi = static_cast<GecodeSolverInstance&>(s);
1535 FloatVar x = gi.arg2floatvar(ce->arg(0));
1536 FloatVar y = gi.arg2floatvar(ce->arg(1));
1537 sqrt(*gi.currentSpace, x, y);
1538}
1539
1540void p_float_abs(SolverInstanceBase& s, const Call* ce) {
1541 auto& gi = static_cast<GecodeSolverInstance&>(s);
1542 FloatVar x = gi.arg2floatvar(ce->arg(0));
1543 FloatVar y = gi.arg2floatvar(ce->arg(1));
1544 abs(*gi.currentSpace, x, y);
1545}
1546
1547void p_float_eq(SolverInstanceBase& s, const Call* ce) {
1548 auto& gi = static_cast<GecodeSolverInstance&>(s);
1549 FloatVar x = gi.arg2floatvar(ce->arg(0));
1550 FloatVar y = gi.arg2floatvar(ce->arg(1));
1551 rel(*gi.currentSpace, x, FRT_EQ, y);
1552}
1553void p_float_eq_reif(SolverInstanceBase& s, const Call* ce) {
1554 auto& gi = static_cast<GecodeSolverInstance&>(s);
1555 FloatVar x = gi.arg2floatvar(ce->arg(0));
1556 FloatVar y = gi.arg2floatvar(ce->arg(1));
1557 BoolVar b = gi.arg2boolvar(ce->arg(2));
1558 rel(*gi.currentSpace, x, FRT_EQ, y, b);
1559}
1560void p_float_le(SolverInstanceBase& s, const Call* ce) {
1561 auto& gi = static_cast<GecodeSolverInstance&>(s);
1562 FloatVar x = gi.arg2floatvar(ce->arg(0));
1563 FloatVar y = gi.arg2floatvar(ce->arg(1));
1564 rel(*gi.currentSpace, x, FRT_LQ, y);
1565}
1566void p_float_le_reif(SolverInstanceBase& s, const Call* ce) {
1567 auto& gi = static_cast<GecodeSolverInstance&>(s);
1568 FloatVar x = gi.arg2floatvar(ce->arg(0));
1569 FloatVar y = gi.arg2floatvar(ce->arg(1));
1570 BoolVar b = gi.arg2boolvar(ce->arg(2));
1571 rel(*gi.currentSpace, x, FRT_LQ, y, b);
1572}
1573void p_float_max(SolverInstanceBase& s, const Call* ce) {
1574 auto& gi = static_cast<GecodeSolverInstance&>(s);
1575 FloatVar x = gi.arg2floatvar(ce->arg(0));
1576 FloatVar y = gi.arg2floatvar(ce->arg(1));
1577 FloatVar z = gi.arg2floatvar(ce->arg(2));
1578 max(*gi.currentSpace, x, y, z);
1579}
1580void p_float_min(SolverInstanceBase& s, const Call* ce) {
1581 auto& gi = static_cast<GecodeSolverInstance&>(s);
1582 FloatVar x = gi.arg2floatvar(ce->arg(0));
1583 FloatVar y = gi.arg2floatvar(ce->arg(1));
1584 FloatVar z = gi.arg2floatvar(ce->arg(2));
1585 min(*gi.currentSpace, x, y, z);
1586}
1587void p_float_lt(SolverInstanceBase& s, const Call* ce) {
1588 auto& gi = static_cast<GecodeSolverInstance&>(s);
1589 FloatVar x = gi.arg2floatvar(ce->arg(0));
1590 FloatVar y = gi.arg2floatvar(ce->arg(1));
1591 rel(*gi.currentSpace, x, FRT_LQ, y);
1592 rel(*gi.currentSpace, x, FRT_EQ, y, BoolVar(*gi.currentSpace, 0, 0));
1593}
1594
1595void p_float_lt_reif(SolverInstanceBase& s, const Call* ce) {
1596 auto& gi = static_cast<GecodeSolverInstance&>(s);
1597 FloatVar x = gi.arg2floatvar(ce->arg(0));
1598 FloatVar y = gi.arg2floatvar(ce->arg(1));
1599 BoolVar b = gi.arg2boolvar(ce->arg(2));
1600 BoolVar b0(*gi.currentSpace, 0, 1);
1601 BoolVar b1(*gi.currentSpace, 0, 1);
1602 rel(*gi.currentSpace, b == (b0 && !b1));
1603 rel(*gi.currentSpace, x, FRT_LQ, y, b0);
1604 rel(*gi.currentSpace, x, FRT_EQ, y, b1);
1605}
1606
1607void p_float_ne(SolverInstanceBase& s, const Call* ce) {
1608 auto& gi = static_cast<GecodeSolverInstance&>(s);
1609 FloatVar x = gi.arg2floatvar(ce->arg(0));
1610 FloatVar y = gi.arg2floatvar(ce->arg(1));
1611 rel(*gi.currentSpace, x, FRT_EQ, y, BoolVar(*gi.currentSpace, 0, 0));
1612}
1613
1614#ifdef GECODE_HAS_MPFR
1615#define P_FLOAT_OP(Op) \
1616 void p_float_##Op(SolverInstanceBase& s, const Call* ce) { \
1617 GecodeSolverInstance& gi = static_cast<GecodeSolverInstance&>(s); \
1618 FloatVar x = gi.arg2floatvar(ce->arg(0)); \
1619 FloatVar y = gi.arg2floatvar(ce->arg(1)); \
1620 Op(*gi.currentSpace, x, y); \
1621 }
1622P_FLOAT_OP(acos)
1623P_FLOAT_OP(asin)
1624P_FLOAT_OP(atan)
1625P_FLOAT_OP(cos)
1626P_FLOAT_OP(exp)
1627P_FLOAT_OP(sin)
1628P_FLOAT_OP(tan)
1629// P_FLOAT_OP(sinh)
1630// P_FLOAT_OP(tanh)
1631// P_FLOAT_OP(cosh)
1632#undef P_FLOAT_OP
1633
1634void p_float_ln(SolverInstanceBase& s, const Call* ce) {
1635 GecodeSolverInstance& gi = static_cast<GecodeSolverInstance&>(s);
1636 FloatVar x = gi.arg2floatvar(ce->arg(0));
1637 FloatVar y = gi.arg2floatvar(ce->arg(1));
1638 log(*gi.currentSpace, x, y);
1639}
1640void p_float_log10(SolverInstanceBase& s, const Call* ce) {
1641 GecodeSolverInstance& gi = static_cast<GecodeSolverInstance&>(s);
1642 FloatVar x = gi.arg2floatvar(ce->arg(0));
1643 FloatVar y = gi.arg2floatvar(ce->arg(1));
1644 log(*gi.currentSpace, 10.0, x, y);
1645}
1646void p_float_log2(SolverInstanceBase& s, const Call* ce) {
1647 GecodeSolverInstance& gi = static_cast<GecodeSolverInstance&>(s);
1648 FloatVar x = gi.arg2floatvar(ce->arg(0));
1649 FloatVar y = gi.arg2floatvar(ce->arg(1));
1650 log(*gi.currentSpace, 2.0, x, y);
1651}
1652
1653#endif
1654#endif
1655
1656#ifdef GECODE_HAS_SET_VARS
1657void p_set_op(SolverInstanceBase& s, SetOpType op, const Call* ce) {
1658 auto& gi = static_cast<GecodeSolverInstance&>(s);
1659 rel(*gi.currentSpace, gi.arg2setvar(ce->arg(0)), op, gi.arg2setvar(ce->arg(1)), SRT_EQ,
1660 gi.arg2setvar(ce->arg(2)));
1661}
1662void p_set_union(SolverInstanceBase& s, const Call* ce) { p_set_op(s, SOT_UNION, ce); }
1663void p_set_intersect(SolverInstanceBase& s, const Call* ce) { p_set_op(s, SOT_INTER, ce); }
1664void p_set_diff(SolverInstanceBase& s, const Call* ce) { p_set_op(s, SOT_MINUS, ce); }
1665
1666void p_set_symdiff(SolverInstanceBase& s, const Call* ce) {
1667 auto& gi = static_cast<GecodeSolverInstance&>(s);
1668 SetVar x = gi.arg2setvar(ce->arg(0));
1669 SetVar y = gi.arg2setvar(ce->arg(1));
1670
1671 SetVarLubRanges xub(x);
1672 IntSet xubs(xub);
1673 SetVar x_y(*gi.currentSpace, IntSet::empty, xubs);
1674 rel(*gi.currentSpace, x, SOT_MINUS, y, SRT_EQ, x_y);
1675
1676 SetVarLubRanges yub(y);
1677 IntSet yubs(yub);
1678 SetVar y_x(*gi.currentSpace, IntSet::empty, yubs);
1679 rel(*gi.currentSpace, y, SOT_MINUS, x, SRT_EQ, y_x);
1680
1681 rel(*gi.currentSpace, x_y, SOT_UNION, y_x, SRT_EQ, gi.arg2setvar(ce->arg(2)));
1682}
1683
1684void p_array_set_op(SolverInstanceBase& s, SetOpType op, const Call* ce) {
1685 auto& gi = static_cast<GecodeSolverInstance&>(s);
1686 SetVarArgs xs = gi.arg2setvarargs(ce->arg(0));
1687 rel(*gi.currentSpace, op, xs, gi.arg2setvar(ce->arg(1)));
1688}
1689void p_array_set_union(SolverInstanceBase& s, const Call* ce) { p_array_set_op(s, SOT_UNION, ce); }
1690void p_array_set_partition(SolverInstanceBase& s, const Call* ce) {
1691 p_array_set_op(s, SOT_DUNION, ce);
1692}
1693
1694void p_set_rel(SolverInstanceBase& s, SetRelType srt, const Call* ce) {
1695 auto& gi = static_cast<GecodeSolverInstance&>(s);
1696 rel(*gi.currentSpace, gi.arg2setvar(ce->arg(0)), srt, gi.arg2setvar(ce->arg(1)));
1697}
1698
1699void p_set_eq(SolverInstanceBase& s, const Call* ce) { p_set_rel(s, SRT_EQ, ce); }
1700void p_set_ne(SolverInstanceBase& s, const Call* ce) { p_set_rel(s, SRT_NQ, ce); }
1701void p_set_subset(SolverInstanceBase& s, const Call* ce) { p_set_rel(s, SRT_SUB, ce); }
1702void p_set_superset(SolverInstanceBase& s, const Call* ce) { p_set_rel(s, SRT_SUP, ce); }
1703void p_set_le(SolverInstanceBase& s, const Call* ce) { p_set_rel(s, SRT_LQ, ce); }
1704void p_set_lt(SolverInstanceBase& s, const Call* ce) { p_set_rel(s, SRT_LE, ce); }
1705void p_set_card(SolverInstanceBase& s, const Call* ce) {
1706 auto& gi = static_cast<GecodeSolverInstance&>(s);
1707 if (!ce->arg(1)->type().isvar()) {
1708 IntVal i = ce->arg(1)->cast<IntLit>()->v().toInt();
1709 assert(i >= 0 && i <= Gecode::Int::Limits::max);
1710 auto ui = static_cast<unsigned int>(i.toInt());
1711 cardinality(*gi.currentSpace, gi.arg2setvar(ce->arg(0)), ui, ui);
1712 } else {
1713 cardinality(*gi.currentSpace, gi.arg2setvar(ce->arg(0)), gi.arg2intvar(ce->arg(1)));
1714 }
1715}
1716void p_set_in(SolverInstanceBase& s, const Call* ce) {
1717 auto& gi = static_cast<GecodeSolverInstance&>(s);
1718 if (!ce->arg(1)->type().isvar()) {
1719 IntSet d = gi.arg2intset(s.env().envi(), ce->arg(1));
1720 if (ce->arg(0)->type().isvar()) {
1721 Gecode::IntSetRanges dr(d);
1722 Iter::Ranges::Singleton sr(0, 1);
1723 Iter::Ranges::Inter<Gecode::IntSetRanges, Iter::Ranges::Singleton> i(dr, sr);
1724 IntSet d01(i);
1725 if (d01.size() == 0) {
1726 gi.currentSpace->fail();
1727 } else {
1728 rel(*gi.currentSpace, gi.arg2boolvar(ce->arg(0)), IRT_GQ, d01.min());
1729 rel(*gi.currentSpace, gi.arg2boolvar(ce->arg(0)), IRT_LQ, d01.max());
1730 }
1731 } else {
1732 dom(*gi.currentSpace, gi.arg2intvar(ce->arg(0)), d);
1733 }
1734 } else {
1735 if (!ce->arg(0)->type().isvar()) {
1736 dom(*gi.currentSpace, gi.arg2setvar(ce->arg(1)), SRT_SUP,
1737 static_cast<int>(ce->arg(0)->cast<IntLit>()->v().toInt()));
1738 } else {
1739 rel(*gi.currentSpace, gi.arg2setvar(ce->arg(1)), SRT_SUP, gi.arg2intvar(ce->arg(0)));
1740 }
1741 }
1742}
1743void p_set_rel_reif(SolverInstanceBase& s, SetRelType srt, const Call* ce) {
1744 auto& gi = static_cast<GecodeSolverInstance&>(s);
1745 rel(*gi.currentSpace, gi.arg2setvar(ce->arg(0)), srt, gi.arg2setvar(ce->arg(1)),
1746 gi.arg2boolvar(ce->arg(2)));
1747}
1748
1749void p_set_eq_reif(SolverInstanceBase& s, const Call* ce) { p_set_rel_reif(s, SRT_EQ, ce); }
1750void p_set_le_reif(SolverInstanceBase& s, const Call* ce) { p_set_rel_reif(s, SRT_LQ, ce); }
1751void p_set_lt_reif(SolverInstanceBase& s, const Call* ce) { p_set_rel_reif(s, SRT_LE, ce); }
1752void p_set_ne_reif(SolverInstanceBase& s, const Call* ce) { p_set_rel_reif(s, SRT_NQ, ce); }
1753void p_set_subset_reif(SolverInstanceBase& s, const Call* ce) { p_set_rel_reif(s, SRT_SUB, ce); }
1754void p_set_superset_reif(SolverInstanceBase& s, const Call* ce) { p_set_rel_reif(s, SRT_SUP, ce); }
1755void p_set_in_reif(SolverInstanceBase& s, const Call* ce, ReifyMode rm) {
1756 auto& gi = static_cast<GecodeSolverInstance&>(s);
1757 if (!ce->arg(1)->type().isvar()) {
1758 if (rm == RM_EQV) {
1759 p_int_in_reif(s, ce);
1760 } else {
1761 assert(rm == RM_IMP);
1762 p_int_in_imp(s, ce);
1763 }
1764 } else {
1765 if (!ce->arg(0)->type().isvar()) {
1766 dom(*gi.currentSpace, gi.arg2setvar(ce->arg(1)), SRT_SUP,
1767 static_cast<int>(ce->arg(0)->cast<IntLit>()->v().toInt()),
1768 Reify(gi.arg2boolvar(ce->arg(2)), rm));
1769 } else {
1770 rel(*gi.currentSpace, gi.arg2setvar(ce->arg(1)), SRT_SUP, gi.arg2intvar(ce->arg(0)),
1771 Reify(gi.arg2boolvar(ce->arg(2)), rm));
1772 }
1773 }
1774}
1775void p_set_in_reif(SolverInstanceBase& s, const Call* ce) { p_set_in_reif(s, ce, RM_EQV); }
1776void p_set_in_imp(SolverInstanceBase& s, const Call* ce) { p_set_in_reif(s, ce, RM_IMP); }
1777void p_set_disjoint(SolverInstanceBase& s, const Call* ce) {
1778 auto& gi = static_cast<GecodeSolverInstance&>(s);
1779 rel(*gi.currentSpace, gi.arg2setvar(ce->arg(0)), SRT_DISJ, gi.arg2setvar(ce->arg(1)));
1780}
1781
1782void p_link_set_to_booleans(SolverInstanceBase& s, const Call* ce) {
1783 auto& gi = static_cast<GecodeSolverInstance&>(s);
1784 SetVar x = gi.arg2setvar(ce->arg(0));
1785 int idx = static_cast<int>(ce->arg(2)->cast<IntLit>()->v().toInt());
1786 assert(idx >= 0);
1787 rel(*gi.currentSpace, x || IntSet(Set::Limits::min, idx - 1));
1788 BoolVarArgs y = gi.arg2boolvarargs(ce->arg(1), idx);
1789 unshare(*gi.currentSpace, y);
1790 channel(*gi.currentSpace, y, x);
1791}
1792
1793void p_array_set_element(SolverInstanceBase& s, const Call* ce) {
1794 auto& gi = static_cast<GecodeSolverInstance&>(s);
1795 bool isConstant = true;
1796 ArrayLit* a = gi.arg2arraylit(ce->arg(1));
1797 for (unsigned int i = a->size(); (i--) != 0U;) {
1798 if ((*a)[i]->type().isvar()) {
1799 isConstant = false;
1800 break;
1801 }
1802 }
1803 IntVar selector = gi.arg2intvar(ce->arg(0));
1804 rel(*gi.currentSpace, selector > 0);
1805 if (isConstant) {
1806 IntSetArgs sv = gi.arg2intsetargs(gi.env().envi(), ce->arg(1), 1);
1807 element(*gi.currentSpace, sv, selector, gi.arg2setvar(ce->arg(2)));
1808 } else {
1809 SetVarArgs sv = gi.arg2setvarargs(ce->arg(1), 1);
1810 element(*gi.currentSpace, sv, selector, gi.arg2setvar(ce->arg(2)));
1811 }
1812}
1813
1814void p_array_set_element_op(SolverInstanceBase& s, const Call* ce, SetOpType op,
1815 const IntSet& universe = IntSet(Set::Limits::min, Set::Limits::max)) {
1816 auto& gi = static_cast<GecodeSolverInstance&>(s);
1817 bool isConstant = true;
1818 ArrayLit* a = gi.arg2arraylit(ce->arg(1));
1819 for (unsigned int i = a->size(); (i--) != 0;) {
1820 if ((*a)[i]->type().isvar()) {
1821 isConstant = false;
1822 break;
1823 }
1824 }
1825 SetVar selector = gi.arg2setvar(ce->arg(0));
1826 dom(*gi.currentSpace, selector, SRT_DISJ, 0);
1827 if (isConstant) {
1828 IntSetArgs sv = gi.arg2intsetargs(gi.env().envi(), ce->arg(1), 1);
1829 element(*gi.currentSpace, op, sv, selector, gi.arg2setvar(ce->arg(2)), universe);
1830 } else {
1831 SetVarArgs sv = gi.arg2setvarargs(ce->arg(1), 1);
1832 element(*gi.currentSpace, op, sv, selector, gi.arg2setvar(ce->arg(2)), universe);
1833 }
1834}
1835
1836void p_array_set_element_union(SolverInstanceBase& s, const Call* ce) {
1837 p_array_set_element_op(s, ce, SOT_UNION);
1838}
1839
1840void p_array_set_element_intersect(SolverInstanceBase& s, const Call* ce) {
1841 p_array_set_element_op(s, ce, SOT_INTER);
1842}
1843
1844void p_array_set_element_intersect_in(SolverInstanceBase& s, const Call* ce) {
1845 auto& gi = static_cast<GecodeSolverInstance&>(s);
1846 IntSet d = gi.arg2intset(gi.env().envi(), ce->arg(3));
1847 p_array_set_element_op(s, ce, SOT_INTER, d);
1848}
1849
1850void p_array_set_element_partition(SolverInstanceBase& s, const Call* ce) {
1851 p_array_set_element_op(s, ce, SOT_DUNION);
1852}
1853
1854void p_set_convex(SolverInstanceBase& s, const Call* ce) {
1855 auto& gi = static_cast<GecodeSolverInstance&>(s);
1856 convex(*gi.currentSpace, gi.arg2setvar(ce->arg(0)));
1857}
1858
1859void p_array_set_seq(SolverInstanceBase& s, const Call* ce) {
1860 auto& gi = static_cast<GecodeSolverInstance&>(s);
1861 SetVarArgs sv = gi.arg2setvarargs(ce->arg(0));
1862 sequence(*gi.currentSpace, sv);
1863}
1864
1865void p_array_set_seq_union(SolverInstanceBase& s, const Call* ce) {
1866 auto& gi = static_cast<GecodeSolverInstance&>(s);
1867 SetVarArgs sv = gi.arg2setvarargs(ce->arg(0));
1868 sequence(*gi.currentSpace, sv, gi.arg2setvar(ce->arg(1)));
1869}
1870
1871void p_int_set_channel(SolverInstanceBase& s, const Call* ce) {
1872 auto& gi = static_cast<GecodeSolverInstance&>(s);
1873 int xoff = static_cast<int>(ce->arg(1)->cast<IntLit>()->v().toInt());
1874 assert(xoff >= 0);
1875 int yoff = static_cast<int>(ce->arg(3)->cast<IntLit>()->v().toInt());
1876 assert(yoff >= 0);
1877 IntVarArgs xv = gi.arg2intvarargs(ce->arg(0), xoff);
1878 SetVarArgs yv = gi.arg2setvarargs(ce->arg(2), yoff, 1, IntSet(0, xoff - 1));
1879 IntSet xd(yoff, yv.size() - 1);
1880 for (int i = xoff; i < xv.size(); i++) {
1881 dom(*gi.currentSpace, xv[i], xd);
1882 }
1883 IntSet yd(xoff, xv.size() - 1);
1884 for (int i = yoff; i < yv.size(); i++) {
1885 dom(*gi.currentSpace, yv[i], SRT_SUB, yd);
1886 }
1887 channel(*gi.currentSpace, xv, yv);
1888}
1889
1890void p_range(SolverInstanceBase& s, const Call* ce) {
1891 auto& gi = static_cast<GecodeSolverInstance&>(s);
1892 int xoff = static_cast<int>(ce->arg(1)->cast<IntLit>()->v().toInt());
1893 assert(xoff >= 0);
1894 IntVarArgs xv = gi.arg2intvarargs(ce->arg(0), xoff);
1895 element(*gi.currentSpace, SOT_UNION, xv, gi.arg2setvar(ce->arg(2)), gi.arg2setvar(ce->arg(3)));
1896}
1897
1898void p_weights(SolverInstanceBase& s, const Call* ce) {
1899 auto& gi = static_cast<GecodeSolverInstance&>(s);
1900 IntArgs e = GecodeSolverInstance::arg2intargs(ce->arg(0));
1901 IntArgs w = GecodeSolverInstance::arg2intargs(ce->arg(1));
1902 SetVar x = gi.arg2setvar(ce->arg(2));
1903 IntVar y = gi.arg2intvar(ce->arg(3));
1904 weights(*gi.currentSpace, e, w, x, y);
1905}
1906
1907void p_inverse_set(SolverInstanceBase& s, const Call* ce) {
1908 auto& gi = static_cast<GecodeSolverInstance&>(s);
1909 int xoff = static_cast<int>(ce->arg(2)->cast<IntLit>()->v().toInt());
1910 int yoff = static_cast<int>(ce->arg(3)->cast<IntLit>()->v().toInt());
1911 SetVarArgs x = gi.arg2setvarargs(ce->arg(0), xoff);
1912 SetVarArgs y = gi.arg2setvarargs(ce->arg(1), yoff);
1913 channel(*gi.currentSpace, x, y);
1914}
1915
1916void p_precede_set(SolverInstanceBase& s, const Call* ce) {
1917 auto& gi = static_cast<GecodeSolverInstance&>(s);
1918 SetVarArgs x = gi.arg2setvarargs(ce->arg(0));
1919 int p_s = static_cast<int>(ce->arg(1)->cast<IntLit>()->v().toInt());
1920 int p_t = static_cast<int>(ce->arg(2)->cast<IntLit>()->v().toInt());
1921 precede(*gi.currentSpace, x, p_s, p_t);
1922}
1923#endif
1924
1925} // namespace GecodeConstraints
1926
1927} // namespace MiniZinc