this repo has no description
dekker.one
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2
3/*
4 * Main authors:
5 * Jip J. Dekker <jip.dekker@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#pragma clang diagnostic push
13#pragma ide diagnostic ignored "cppcoreguidelines-pro-type-static-cast-downcast"
14
15#include <minizinc/solvers/geas/geas_constraints.hh>
16#include <minizinc/solvers/geas_solverinstance.hh>
17
18#include <geas/constraints/builtins.h>
19#include <geas/constraints/flow/flow.h>
20
21namespace MiniZinc {
22namespace GeasConstraints {
23
24#define SI (static_cast<GeasSolverInstance&>(s))
25#define SD SI.solverData()
26#define SOL SI.solver()
27#define EXPR(X) call->arg(X)
28#define BOOL(X) SI.asBool(EXPR(X))
29#define BOOLARRAY(X) SI.asBool(ARRAY(X))
30#define BOOLVAR(X) SI.asBoolVar(EXPR(X))
31#define BOOLVARARRAY(X) SI.asBoolVar(ARRAY(X))
32#define INT(X) SI.asInt(EXPR(X))
33#define INTARRAY(X) SI.asInt(ARRAY(X))
34#define INTVAR(X) SI.asIntVar(EXPR(X))
35#define INTVARARRAY(X) SI.asIntVar(ARRAY(X))
36#define PAR(X) call->arg(X)->type().isPar()
37#define ARRAY(X) eval_array_lit(s.env().envi(), call->arg(X))
38
39void p_int_eq(SolverInstanceBase& s, const Call* call) { geas::int_eq(SD, INTVAR(0), INTVAR(1)); }
40
41void p_int_ne(SolverInstanceBase& s, const Call* call) { geas::int_ne(SD, INTVAR(0), INTVAR(1)); }
42
43void p_int_le(SolverInstanceBase& s, const Call* call) {
44 geas::int_le(SD, INTVAR(0), INTVAR(1), 0);
45}
46
47void p_int_lt(SolverInstanceBase& s, const Call* call) {
48 geas::int_le(SD, INTVAR(0), INTVAR(1), -1);
49}
50
51void p_int_eq_imp(SolverInstanceBase& s, const Call* call) {
52 if (PAR(2)) {
53 if (BOOL(2)) {
54 p_int_eq(s, call);
55 }
56 } else {
57 geas::int_eq(SD, INTVAR(0), INTVAR(1), BOOLVAR(2));
58 }
59}
60
61void p_int_ne_imp(SolverInstanceBase& s, const Call* call) {
62 if (PAR(2)) {
63 if (BOOL(2)) {
64 p_int_ne(s, call);
65 }
66 } else {
67 geas::int_ne(SD, INTVAR(0), INTVAR(1), BOOLVAR(2));
68 }
69}
70
71void p_int_le_imp(SolverInstanceBase& s, const Call* call) {
72 if (PAR(2)) {
73 if (BOOL(2)) {
74 p_int_le(s, call);
75 }
76 } else {
77 geas::int_le(SD, INTVAR(0), INTVAR(1), 0, BOOLVAR(2));
78 }
79}
80
81void p_int_lt_imp(SolverInstanceBase& s, const Call* call) {
82 if (PAR(2)) {
83 if (BOOL(2)) {
84 p_int_lt(s, call);
85 }
86 } else {
87 geas::int_le(SD, INTVAR(0), INTVAR(1), -1, BOOLVAR(2));
88 }
89}
90
91void p_int_eq_reif(SolverInstanceBase& s, const Call* call) {
92 if (PAR(2)) {
93 if (BOOL(2)) {
94 p_int_eq(s, call);
95 } else {
96 p_int_ne(s, call);
97 }
98 } else {
99 geas::int_eq(SD, INTVAR(0), INTVAR(1), BOOLVAR(2));
100 geas::int_ne(SD, INTVAR(0), INTVAR(1), ~BOOLVAR(2));
101 }
102}
103
104void p_int_ne_reif(SolverInstanceBase& s, const Call* call) {
105 if (PAR(2)) {
106 if (BOOL(2)) {
107 p_int_ne(s, call);
108 } else {
109 p_int_eq(s, call);
110 }
111 } else {
112 geas::int_ne(SD, INTVAR(0), INTVAR(1), BOOLVAR(2));
113 geas::int_eq(SD, INTVAR(0), INTVAR(1), ~BOOLVAR(2));
114 }
115}
116
117void p_int_le_reif(SolverInstanceBase& s, const Call* call) {
118 if (PAR(2)) {
119 if (BOOL(2)) {
120 p_int_le(s, call);
121 } else {
122 auto* nc = new Call(Location().introduce(), call->id(), {call->arg(1), call->arg(0)});
123 p_int_lt(s, nc);
124 }
125 } else {
126 geas::int_le(SD, INTVAR(0), INTVAR(1), 0, BOOLVAR(2));
127 geas::int_le(SD, INTVAR(1), INTVAR(0), -1, ~BOOLVAR(2));
128 }
129}
130
131void p_int_lt_reif(SolverInstanceBase& s, const Call* call) {
132 if (PAR(2)) {
133 if (BOOL(2)) {
134 p_int_lt(s, call);
135 } else {
136 auto* nc = new Call(Location().introduce(), call->id(), {call->arg(1), call->arg(0)});
137 p_int_le(s, nc);
138 }
139 } else {
140 geas::int_le(SD, INTVAR(0), INTVAR(1), -1, BOOLVAR(2));
141 geas::int_le(SD, INTVAR(1), INTVAR(0), 0, ~BOOLVAR(2));
142 }
143}
144
145void p_int_abs(SolverInstanceBase& s, const Call* call) { geas::int_abs(SD, INTVAR(1), INTVAR(0)); }
146
147void p_int_times(SolverInstanceBase& s, const Call* call) {
148 geas::int_mul(SD, INTVAR(2), INTVAR(0), INTVAR(1));
149}
150
151void p_int_div(SolverInstanceBase& s, const Call* call) {
152 geas::int_div(SD, INTVAR(2), INTVAR(0), INTVAR(1));
153}
154
155void p_int_max(SolverInstanceBase& s, const Call* call) {
156 vec<geas::intvar> vars = {INTVAR(0), INTVAR(1)};
157 geas::int_max(SD, INTVAR(2), vars);
158}
159
160void p_int_min(SolverInstanceBase& s, const Call* call) {
161 vec<geas::intvar> vars = {-INTVAR(0), -INTVAR(1)};
162 geas::int_max(SD, -INTVAR(2), vars);
163}
164
165void p_int_lin_eq(SolverInstanceBase& s, const Call* call) {
166 vec<int> pos = INTARRAY(0);
167 vec<int> neg(pos.size());
168 for (int i = 0; i < neg.size(); ++i) {
169 neg[i] = -pos[i];
170 }
171 vec<geas::intvar> vars = INTVARARRAY(1);
172 // TODO: Rewrite using MiniZinc Library??
173 geas::linear_le(SD, pos, vars, INT(2));
174 geas::linear_le(SD, neg, vars, -INT(2));
175}
176
177void p_int_lin_ne(SolverInstanceBase& s, const Call* call) {
178 vec<int> cons = INTARRAY(0);
179 vec<geas::intvar> vars = INTVARARRAY(1);
180 geas::linear_ne(SD, cons, vars, INT(2));
181}
182
183void p_int_lin_le(SolverInstanceBase& s, const Call* call) {
184 vec<int> cons = INTARRAY(0);
185 vec<geas::intvar> vars = INTVARARRAY(1);
186 geas::linear_le(SD, cons, vars, INT(2));
187}
188
189void p_int_lin_eq_imp(SolverInstanceBase& s, const Call* call) {
190 vec<int> pos = INTARRAY(0);
191 vec<int> neg(pos.size());
192 for (int i = 0; i < neg.size(); ++i) {
193 neg[i] = -pos[i];
194 }
195 vec<geas::intvar> vars = INTVARARRAY(1);
196 // TODO: Rewrite using MiniZinc Library??
197 geas::linear_le(SD, pos, vars, INT(2), BOOLVAR(3));
198 geas::linear_le(SD, neg, vars, -INT(2), BOOLVAR(3));
199}
200
201void p_int_lin_ne_imp(SolverInstanceBase& s, const Call* call) {
202 vec<int> cons = INTARRAY(0);
203 vec<geas::intvar> vars = INTVARARRAY(1);
204 geas::linear_ne(SD, cons, vars, INT(2), BOOLVAR(3));
205}
206
207void p_int_lin_le_imp(SolverInstanceBase& s, const Call* call) {
208 vec<int> cons = INTARRAY(0);
209 vec<geas::intvar> vars = INTVARARRAY(1);
210 geas::linear_le(SD, cons, vars, INT(2), BOOLVAR(3));
211}
212
213void p_int_lin_eq_reif(SolverInstanceBase& s, const Call* call) {
214 vec<int> pos = INTARRAY(0);
215 vec<int> neg(pos.size());
216 for (int i = 0; i < neg.size(); ++i) {
217 neg[i] = -pos[i];
218 }
219 vec<geas::intvar> vars = INTVARARRAY(1);
220 // TODO: Rewrite using MiniZinc Library??
221 geas::linear_le(SD, pos, vars, INT(2), BOOLVAR(3));
222 geas::linear_le(SD, neg, vars, -INT(2), BOOLVAR(3));
223 geas::linear_ne(SD, pos, vars, INT(2), ~BOOLVAR(3));
224}
225
226void p_int_lin_ne_reif(SolverInstanceBase& s, const Call* call) {
227 vec<int> pos = INTARRAY(0);
228 vec<int> neg(pos.size());
229 for (int i = 0; i < neg.size(); ++i) {
230 neg[i] = -pos[i];
231 }
232 vec<geas::intvar> vars = INTVARARRAY(1);
233 // TODO: Rewrite using MiniZinc Library??
234 geas::linear_ne(SD, pos, vars, INT(2), BOOLVAR(3));
235 geas::linear_le(SD, pos, vars, INT(2), ~BOOLVAR(3));
236 geas::linear_le(SD, neg, vars, -INT(2), ~BOOLVAR(3));
237}
238
239void p_int_lin_le_reif(SolverInstanceBase& s, const Call* call) {
240 vec<int> pos = INTARRAY(0);
241 vec<int> neg(pos.size());
242 for (int i = 0; i < neg.size(); ++i) {
243 neg[i] = -pos[i];
244 }
245 vec<geas::intvar> vars = INTVARARRAY(1);
246 geas::linear_le(SD, pos, vars, INT(2), BOOLVAR(3));
247 geas::linear_le(SD, neg, vars, -INT(2) - 1, ~BOOLVAR(3));
248}
249
250void p_bool_eq(SolverInstanceBase& s, const Call* call) {
251 if (PAR(0)) {
252 SOL.post(BOOL(0) ? BOOLVAR(1) : ~BOOLVAR(1));
253 } else if (PAR(2)) {
254 SOL.post(BOOL(1) ? BOOLVAR(0) : ~BOOLVAR(0));
255 } else {
256 geas::add_clause(SD, BOOLVAR(0), ~BOOLVAR(1));
257 geas::add_clause(SD, ~BOOLVAR(0), BOOLVAR(1));
258 }
259}
260
261void p_bool_ne(SolverInstanceBase& s, const Call* call) {
262 if (PAR(0)) {
263 SOL.post(BOOL(0) ? ~BOOLVAR(1) : BOOLVAR(1));
264 } else if (PAR(1)) {
265 SOL.post(BOOL(1) ? ~BOOLVAR(0) : BOOLVAR(0));
266 } else {
267 geas::add_clause(SD, BOOLVAR(0), BOOLVAR(1));
268 geas::add_clause(SD, ~BOOLVAR(0), ~BOOLVAR(1));
269 }
270}
271
272void p_bool_le(SolverInstanceBase& s, const Call* call) {
273 if (PAR(0)) {
274 if (BOOL(0)) {
275 SOL.post(BOOLVAR(1));
276 }
277 } else if (PAR(1)) {
278 if (!BOOL(1)) {
279 SOL.post(~BOOLVAR(0));
280 }
281 } else {
282 geas::add_clause(SD, ~BOOLVAR(0), BOOLVAR(1));
283 }
284}
285
286void p_bool_lt(SolverInstanceBase& s, const Call* call) {
287 SOL.post(~BOOLVAR(0));
288 SOL.post(BOOLVAR(1));
289}
290
291void p_bool_eq_imp(SolverInstanceBase& s, const Call* call) {
292 if (PAR(2)) {
293 if (BOOL(2)) {
294 p_bool_eq(s, call);
295 }
296 } else {
297 geas::add_clause(SD, ~BOOLVAR(2), ~BOOLVAR(0), BOOLVAR(1));
298 geas::add_clause(SD, ~BOOLVAR(2), BOOLVAR(0), ~BOOLVAR(1));
299 }
300}
301
302void p_bool_ne_imp(SolverInstanceBase& s, const Call* call) {
303 if (PAR(2)) {
304 if (BOOL(2)) {
305 p_bool_ne(s, call);
306 }
307 } else {
308 geas::add_clause(SD, ~BOOLVAR(2), BOOLVAR(0), BOOLVAR(1));
309 geas::add_clause(SD, ~BOOLVAR(2), ~BOOLVAR(0), ~BOOLVAR(1));
310 }
311}
312
313void p_bool_le_imp(SolverInstanceBase& s, const Call* call) {
314 if (PAR(2)) {
315 if (BOOL(2)) {
316 p_bool_le(s, call);
317 }
318 } else {
319 geas::add_clause(SD, ~BOOLVAR(2), ~BOOLVAR(0), BOOLVAR(1));
320 }
321}
322
323void p_bool_lt_imp(SolverInstanceBase& s, const Call* call) {
324 if (PAR(2)) {
325 if (BOOL(2)) {
326 p_bool_lt(s, call);
327 }
328 } else {
329 geas::add_clause(SD, ~BOOLVAR(2), ~BOOLVAR(0));
330 geas::add_clause(SD, ~BOOLVAR(2), BOOLVAR(1));
331 }
332}
333
334void p_bool_eq_reif(SolverInstanceBase& s, const Call* call) {
335 if (PAR(2)) {
336 if (BOOL(2)) {
337 p_bool_eq(s, call);
338 } else {
339 p_bool_ne(s, call);
340 }
341 } else {
342 geas::add_clause(SD, BOOLVAR(2), BOOLVAR(0), BOOLVAR(1));
343 geas::add_clause(SD, BOOLVAR(2), ~BOOLVAR(0), ~BOOLVAR(1));
344 geas::add_clause(SD, ~BOOLVAR(2), ~BOOLVAR(0), BOOLVAR(1));
345 geas::add_clause(SD, ~BOOLVAR(2), BOOLVAR(0), ~BOOLVAR(1));
346 }
347}
348
349void p_bool_ne_reif(SolverInstanceBase& s, const Call* call) {
350 if (PAR(2)) {
351 if (BOOL(2)) {
352 p_bool_ne(s, call);
353 } else {
354 p_bool_eq(s, call);
355 }
356 } else {
357 geas::add_clause(SD, BOOLVAR(2), ~BOOLVAR(0), BOOLVAR(1));
358 geas::add_clause(SD, BOOLVAR(2), BOOLVAR(0), ~BOOLVAR(1));
359 geas::add_clause(SD, ~BOOLVAR(2), BOOLVAR(0), BOOLVAR(1));
360 geas::add_clause(SD, ~BOOLVAR(2), ~BOOLVAR(0), ~BOOLVAR(1));
361 }
362}
363
364void p_bool_le_reif(SolverInstanceBase& s, const Call* call) {
365 if (PAR(2)) {
366 if (BOOL(2)) {
367 p_bool_le(s, call);
368 } else {
369 auto* nc = new Call(Location().introduce(), call->id(), {call->arg(1), call->arg(0)});
370 p_bool_lt(s, nc);
371 }
372 } else {
373 geas::add_clause(SD, BOOLVAR(2), ~BOOLVAR(1));
374 geas::add_clause(SD, BOOLVAR(2), BOOLVAR(0));
375 geas::add_clause(SD, ~BOOLVAR(2), ~BOOLVAR(0), BOOLVAR(1));
376 }
377}
378
379void p_bool_lt_reif(SolverInstanceBase& s, const Call* call) {
380 if (PAR(2)) {
381 if (BOOL(2)) {
382 p_int_lt(s, call);
383 } else {
384 auto* nc = new Call(Location().introduce(), call->id(), {call->arg(1), call->arg(0)});
385 p_int_le(s, nc);
386 }
387 } else {
388 geas::add_clause(SD, ~BOOLVAR(2), ~BOOLVAR(0));
389 geas::add_clause(SD, ~BOOLVAR(2), BOOLVAR(1));
390 geas::add_clause(SD, BOOLVAR(2), BOOLVAR(0), ~BOOLVAR(1));
391 }
392}
393
394void p_bool_or(SolverInstanceBase& s, const Call* call) {
395 geas::add_clause(SD, BOOLVAR(2), ~BOOLVAR(0));
396 geas::add_clause(SD, BOOLVAR(2), ~BOOLVAR(1));
397 geas::add_clause(SD, ~BOOLVAR(2), BOOLVAR(0), BOOLVAR(1));
398}
399
400void p_bool_and(SolverInstanceBase& s, const Call* call) {
401 geas::add_clause(SD, ~BOOLVAR(2), BOOLVAR(0));
402 geas::add_clause(SD, ~BOOLVAR(2), BOOLVAR(1));
403 geas::add_clause(SD, BOOLVAR(2), ~BOOLVAR(0), ~BOOLVAR(1));
404}
405
406void p_bool_xor(SolverInstanceBase& s, const Call* call) {
407 if (call->argCount() == 2) {
408 p_bool_ne(s, call);
409 } else {
410 p_bool_ne_reif(s, call);
411 }
412}
413
414void p_bool_not(SolverInstanceBase& s, const Call* call) { p_bool_ne(s, call); }
415
416void p_bool_or_imp(SolverInstanceBase& s, const Call* call) {
417 geas::add_clause(SD, ~BOOLVAR(2), BOOLVAR(0), BOOLVAR(1));
418}
419
420void p_bool_and_imp(SolverInstanceBase& s, const Call* call) {
421 geas::add_clause(SD, ~BOOLVAR(2), BOOLVAR(0));
422 geas::add_clause(SD, ~BOOLVAR(2), BOOLVAR(1));
423}
424
425void p_bool_xor_imp(SolverInstanceBase& s, const Call* call) { p_bool_ne_imp(s, call); }
426
427void p_bool_clause(SolverInstanceBase& s, const Call* call) {
428 auto& gi = static_cast<GeasSolverInstance&>(s);
429 auto* pos = ARRAY(0);
430 auto* neg = ARRAY(1);
431 vec<geas::clause_elt> clause;
432 for (int i = 0; i < pos->size(); ++i) {
433 clause.push(SI.asBoolVar((*pos)[i]));
434 }
435 for (int j = 0; j < neg->size(); ++j) {
436 clause.push(~SI.asBoolVar((*neg)[j]));
437 }
438 geas::add_clause(*SD, clause);
439}
440
441void p_array_bool_or(SolverInstanceBase& s, const Call* call) {
442 auto* arr = ARRAY(0);
443 vec<geas::clause_elt> clause;
444 clause.push(~BOOLVAR(1));
445 for (int i = 0; i < arr->size(); ++i) {
446 geas::patom_t elem = SI.asBoolVar((*arr)[i]);
447 geas::add_clause(SD, BOOLVAR(1), ~elem);
448 clause.push(elem);
449 }
450 geas::add_clause(*SD, clause);
451}
452
453void p_array_bool_and(SolverInstanceBase& s, const Call* call) {
454 auto* arr = ARRAY(0);
455 vec<geas::clause_elt> clause;
456 clause.push(BOOLVAR(1));
457 for (int i = 0; i < arr->size(); ++i) {
458 geas::patom_t elem = SI.asBoolVar((*arr)[i]);
459 geas::add_clause(SD, ~BOOLVAR(1), elem);
460 clause.push(~elem);
461 }
462 geas::add_clause(*SD, clause);
463}
464
465void p_bool_clause_imp(SolverInstanceBase& s, const Call* call) {
466 auto* pos = ARRAY(0);
467 auto* neg = ARRAY(1);
468 vec<geas::clause_elt> clause;
469 clause.push(~BOOLVAR(2));
470 for (int i = 0; i < pos->size(); ++i) {
471 clause.push(SI.asBoolVar((*pos)[i]));
472 }
473 for (int j = 0; j < neg->size(); ++j) {
474 clause.push(~SI.asBoolVar((*neg)[j]));
475 }
476 geas::add_clause(*SD, clause);
477}
478
479void p_array_bool_or_imp(SolverInstanceBase& s, const Call* call) {
480 auto* arr = ARRAY(0);
481 vec<geas::clause_elt> clause;
482 clause.push(~BOOLVAR(1));
483 for (int i = 0; i < arr->size(); ++i) {
484 geas::patom_t elem = SI.asBoolVar((*arr)[i]);
485 clause.push(elem);
486 }
487 geas::add_clause(*SD, clause);
488}
489
490void p_array_bool_and_imp(SolverInstanceBase& s, const Call* call) {
491 auto* arr = ARRAY(0);
492 for (int i = 0; i < arr->size(); ++i) {
493 geas::add_clause(SD, ~BOOLVAR(1), SI.asBoolVar((*arr)[i]));
494 }
495}
496
497void p_bool_clause_reif(SolverInstanceBase& s, const Call* call) {
498 auto* pos = ARRAY(0);
499 auto* neg = ARRAY(1);
500 vec<geas::clause_elt> clause;
501 clause.push(~BOOLVAR(2));
502 for (int i = 0; i < pos->size(); ++i) {
503 geas::patom_t elem = SI.asBoolVar((*pos)[i]);
504 geas::add_clause(SD, BOOLVAR(2), ~elem);
505 clause.push(elem);
506 }
507 for (int j = 0; j < neg->size(); ++j) {
508 geas::patom_t elem = SI.asBoolVar((*neg)[j]);
509 geas::add_clause(SD, BOOLVAR(2), elem);
510 clause.push(~elem);
511 }
512 geas::add_clause(*SD, clause);
513}
514
515void p_bool_lin_eq(SolverInstanceBase& s, const Call* call) {
516 vec<int> cons = INTARRAY(0);
517 vec<geas::patom_t> vars = BOOLVARARRAY(1);
518 // TODO: Rewrite using MiniZinc Library??
519 geas::bool_linear_le(SD, geas::at_True, SI.zero, cons, vars, -INT(2));
520 geas::bool_linear_ge(SD, geas::at_True, SI.zero, cons, vars, -INT(2));
521}
522
523void p_bool_lin_ne(SolverInstanceBase& s, const Call* call) {
524 vec<int> cons = INTARRAY(0);
525 vec<geas::patom_t> vars = BOOLVARARRAY(1);
526 geas::bool_linear_ne(SD, cons, vars, INT(2));
527}
528
529void p_bool_lin_le(SolverInstanceBase& s, const Call* call) {
530 vec<int> cons = INTARRAY(0);
531 vec<geas::patom_t> vars = BOOLVARARRAY(1);
532 geas::bool_linear_ge(SD, geas::at_True, SI.zero, cons, vars, -INT(2));
533}
534
535void p_bool_lin_eq_imp(SolverInstanceBase& s, const Call* call) {
536 vec<int> cons = INTARRAY(0);
537 vec<geas::patom_t> vars = BOOLVARARRAY(1);
538 // TODO: Rewrite using MiniZinc Library??
539 geas::bool_linear_le(SD, BOOLVAR(3), SI.zero, cons, vars, -INT(2));
540 geas::bool_linear_ge(SD, BOOLVAR(3), SI.zero, cons, vars, -INT(2));
541}
542
543void p_bool_lin_ne_imp(SolverInstanceBase& s, const Call* call) {
544 vec<int> cons = INTARRAY(0);
545 vec<geas::patom_t> vars = BOOLVARARRAY(1);
546 geas::bool_linear_ne(SD, cons, vars, INT(2), BOOLVAR(3));
547}
548
549void p_bool_lin_le_imp(SolverInstanceBase& s, const Call* call) {
550 vec<int> cons = INTARRAY(0);
551 vec<geas::patom_t> vars = BOOLVARARRAY(1);
552 geas::bool_linear_ge(SD, BOOLVAR(3), SI.zero, cons, vars, -INT(2));
553}
554
555void p_bool_lin_eq_reif(SolverInstanceBase& s, const Call* call) {
556 vec<int> cons = INTARRAY(0);
557 vec<geas::patom_t> vars = BOOLVARARRAY(1);
558 // TODO: Rewrite using MiniZinc Library??
559 geas::bool_linear_le(SD, BOOLVAR(3), SI.zero, cons, vars, -INT(2));
560 geas::bool_linear_ge(SD, BOOLVAR(3), SI.zero, cons, vars, -INT(2));
561 geas::bool_linear_ne(SD, cons, vars, INT(2), ~BOOLVAR(3));
562}
563
564void p_bool_lin_ne_reif(SolverInstanceBase& s, const Call* call) {
565 vec<int> cons = INTARRAY(0);
566 vec<geas::patom_t> vars = BOOLVARARRAY(1);
567 // TODO: Rewrite using MiniZinc Library??
568 geas::bool_linear_ne(SD, cons, vars, INT(2), BOOLVAR(3));
569 geas::bool_linear_le(SD, ~BOOLVAR(3), SI.zero, cons, vars, -INT(2));
570 geas::bool_linear_ge(SD, ~BOOLVAR(3), SI.zero, cons, vars, -INT(2));
571}
572
573void p_bool_lin_le_reif(SolverInstanceBase& s, const Call* call) {
574 vec<int> cons = INTARRAY(0);
575 vec<geas::patom_t> vars = BOOLVARARRAY(1);
576 // TODO: Rewrite using MiniZinc Library??
577 geas::bool_linear_ge(SD, BOOLVAR(3), SI.zero, cons, vars, -INT(2));
578 geas::bool_linear_le(SD, ~BOOLVAR(3), SI.zero, cons, vars, -INT(2) - 1);
579}
580
581void p_bool2int(SolverInstanceBase& s, const Call* call) {
582 geas::add_clause(SD, BOOLVAR(0), INTVAR(1) <= 0);
583 geas::add_clause(SD, ~BOOLVAR(0), INTVAR(1) >= 1);
584}
585
586void p_array_int_element(SolverInstanceBase& s, const Call* call) {
587 assert(ARRAY(1)->min(0) == 1 && ARRAY(1)->max(0) == ARRAY(1)->size() + 1);
588 vec<int> vals = INTARRAY(1);
589 if (PAR(0)) {
590 SOL.post(INTVAR(2) == vals[INT(0) - 1]);
591 } else if (PAR(2)) {
592 for (int j = 0; j < vals.size(); ++j) {
593 if (vals[j] != INT(2)) {
594 SOL.post(INTVAR(0) != j + 1);
595 }
596 }
597 } else {
598 geas::int_element(SD, INTVAR(2), INTVAR(0), vals);
599 }
600}
601
602void p_array_bool_element(SolverInstanceBase& s, const Call* call) {
603 assert(ARRAY(1)->min(0) == 1 && ARRAY(1)->max(0) == ARRAY(1)->size() + 1);
604 vec<bool> vals = BOOLARRAY(1);
605 if (PAR(0)) {
606 SOL.post(vals[INT(0) - 1] ? BOOLVAR(2) : ~BOOLVAR(2));
607 } else if (PAR(2)) {
608 for (int j = 0; j < vals.size(); ++j) {
609 if (static_cast<int>(vals[j]) != BOOL(2)) {
610 SOL.post(INTVAR(0) != j + 1);
611 }
612 }
613 } else {
614 for (int j = 0; j < vals.size(); ++j) {
615 geas::add_clause(SD, INTVAR(0) != j + 1, vals[j] ? BOOLVAR(2) : ~BOOLVAR(2));
616 }
617 }
618}
619
620void p_array_var_int_element(SolverInstanceBase& s, const Call* call) {
621 assert(ARRAY(1)->min(0) == 1 && ARRAY(1)->max(0) == ARRAY(1)->size() + 1);
622 if (PAR(1)) {
623 return p_array_int_element(s, call);
624 }
625 if (PAR(0) && PAR(2)) {
626 SOL.post(SI.asIntVar((*ARRAY(1))[INT(0) - 1]) == INT(2));
627 } else if (PAR(0)) {
628 Expression* elem = (*ARRAY(1))[INT(0) - 1];
629 if (elem->type().isPar()) {
630 return p_array_int_element(s, call);
631 }
632 geas::int_eq(SD, SI.asIntVar(elem), INTVAR(2));
633
634 } else if (PAR(2)) {
635 for (int j = 0; j < ARRAY(1)->size(); ++j) {
636 Expression* elem = (*ARRAY(1))[j];
637 if (elem->type().isvar()) {
638 geas::add_clause(SD, INTVAR(0) != j + 1, SI.asIntVar(elem) == INT(2));
639 } else {
640 if (SI.asInt(elem) != INT(2)) {
641 SOL.post(INTVAR(0) != j + 1);
642 }
643 }
644 }
645 } else {
646 vec<geas::intvar> vals = INTVARARRAY(1);
647 geas::var_int_element(SD, INTVAR(2), INTVAR(0), vals);
648 }
649}
650
651void p_array_var_bool_element(SolverInstanceBase& s, const Call* call) {
652 assert(ARRAY(1)->min(0) == 1 && ARRAY(1)->max(0) == ARRAY(1)->size() + 1);
653 if (PAR(1)) {
654 return p_array_bool_element(s, call);
655 }
656 if (PAR(0) && PAR(2)) {
657 SOL.post(BOOL(2) ? SI.asBoolVar((*ARRAY(1))[INT(0) - 1])
658 : ~SI.asBoolVar((*ARRAY(1))[INT(0) - 1]));
659 } else if (PAR(0)) {
660 Expression* elem = (*ARRAY(1))[INT(0) - 1];
661 if (elem->type().isPar()) {
662 return p_array_bool_element(s, call);
663 }
664 geas::add_clause(SD, BOOLVAR(2), ~SI.asBoolVar(elem));
665 geas::add_clause(SD, ~BOOLVAR(2), SI.asBoolVar(elem));
666
667 } else if (PAR(2)) {
668 for (int j = 0; j < ARRAY(1)->size(); ++j) {
669 Expression* elem = (*ARRAY(1))[j];
670 if (elem->type().isvar()) {
671 geas::add_clause(SD, INTVAR(0) != j + 1, INT(2) ? SI.asBoolVar(elem) : ~SI.asBoolVar(elem));
672 } else {
673 if (SI.asBool(elem) != INT(2)) {
674 SOL.post(INTVAR(0) != j + 1);
675 }
676 }
677 }
678 } else {
679 auto vars = BOOLVARARRAY(1);
680 for (int j = 0; j < vars.size(); ++j) {
681 geas::add_clause(SD, INTVAR(0) != j + 1, ~vars[j], BOOLVAR(2));
682 geas::add_clause(SD, INTVAR(0) != j + 1, vars[j], ~BOOLVAR(2));
683 }
684 }
685}
686
687void p_all_different(SolverInstanceBase& s, const Call* call) {
688 vec<geas::intvar> vars = INTVARARRAY(0);
689 geas::all_different_int(SD, vars);
690}
691
692void p_all_different_except_0(SolverInstanceBase& s, const Call* call) {
693 vec<geas::intvar> vars = INTVARARRAY(0);
694 geas::all_different_except_0(SD, vars);
695}
696
697void p_at_most(SolverInstanceBase& s, const Call* call) {
698 vec<geas::intvar> ivars = INTVARARRAY(1);
699 vec<geas::patom_t> bvars;
700 for (auto& ivar : ivars) {
701 bvars.push(ivar == INT(2));
702 }
703
704 if (INT(0) == 1) {
705 geas::atmost_1(SD, bvars);
706 } else {
707 geas::atmost_k(SD, bvars, INT(0));
708 }
709}
710
711void p_at_most1(SolverInstanceBase& s, const Call* call) {
712 vec<geas::intvar> ivars = INTVARARRAY(0);
713 vec<geas::patom_t> bvars;
714 for (auto& ivar : ivars) {
715 bvars.push(ivar == INT(1));
716 }
717 geas::atmost_1(SD, bvars);
718}
719
720void p_cumulative(SolverInstanceBase& s, const Call* call) {
721 vec<geas::intvar> st = INTVARARRAY(0);
722 if (PAR(1) && PAR(2) && PAR(3)) {
723 vec<int> d = INTARRAY(1);
724 vec<int> r = INTARRAY(2);
725 geas::cumulative(SD, st, d, r, INT(3));
726 } else {
727 vec<geas::intvar> d = INTVARARRAY(1);
728 vec<geas::intvar> r = INTVARARRAY(2);
729 geas::cumulative_var(SD, st, d, r, INTVAR(3));
730 }
731}
732
733void p_disjunctive(SolverInstanceBase& s, const Call* call) {
734 vec<geas::intvar> st = INTVARARRAY(0);
735 if (PAR(1)) {
736 vec<int> d = INTARRAY(1);
737 geas::disjunctive_int(SD, st, d);
738 } else {
739 vec<geas::intvar> d = INTVARARRAY(1);
740 geas::disjunctive_var(SD, st, d);
741 }
742}
743
744void p_global_cardinality(SolverInstanceBase& s, const Call* call) {
745 vec<geas::intvar> x = INTVARARRAY(0);
746 vec<int> cover = INTARRAY(1);
747 vec<int> count = INTARRAY(2);
748
749 vec<int> srcs(x.size(), 1);
750 vec<geas::bflow> flows;
751 for (int i = 0; i < x.size(); ++i) {
752 for (int j = 0; j < cover.size(); ++j) {
753 if (x[i].lb(SD) <= cover[j] && cover[j] <= x[i].ub(SD)) {
754 flows.push({i, j, x[i] == cover[j]});
755 }
756 }
757 }
758 geas::bipartite_flow(SD, srcs, count, flows);
759}
760
761void p_table_int(SolverInstanceBase& s, const Call* call) {
762 auto& gi = static_cast<GeasSolverInstance&>(s);
763 vec<geas::intvar> vars = INTVARARRAY(0);
764 vec<int> tmp = INTARRAY(1);
765 assert(tmp.size() % vars.size() == 0);
766 vec<vec<int>> table(tmp.size() == 0 ? 0 : tmp.size() / vars.size());
767 for (int i = 0; i < table.size(); ++i) {
768 table[i].growTo(vars.size());
769 for (int j = 0; j < vars.size(); ++j) {
770 table[i][j] = tmp[i * vars.size() + j];
771 }
772 }
773 geas::table_id id = geas::table::build(SD, table);
774 // TODO: Annotations for table versions
775 geas::table::post(SD, id, vars);
776}
777
778} // namespace GeasConstraints
779} // namespace MiniZinc
780
781#pragma clang diagnostic pop