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