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.solver_data()
26#define SOL SI.solver()
27#define STATE SI.currentState()
28#define EXPR(X) call->arg(X)
29#define BOOL(X) GeasSolverInstance::asBool(EXPR(X))
30#define BOOLARRAY(X) SI.asBoolVec(ARRAY(X))
31#define BOOLVAR(X) SI.asBoolVar(EXPR(X))
32#define BOOLVARARRAY(X) SI.asBoolVarVec(ARRAY(X))
33#define INT(X) GeasSolverInstance::asInt(EXPR(X))
34#define INTARRAY(X) SI.asIntVec(ARRAY(X))
35#define INTVAR(X) SI.asIntVar(EXPR(X))
36#define INTVARARRAY(X) SI.asIntVarVec(ARRAY(X))
37#define PAR(X) call->arg(X).isInt()
38#define ARRAY(X) call->arg(X)
39
40geas::patom_t lit_and(geas::solver& s, geas::patom_t a, geas::patom_t b) {
41 if (a == geas::at_False || b == geas::at_False) {
42 return geas::at_False;
43 } else if (a == geas::at_True) {
44 return b;
45 } else if (b == geas::at_True) {
46 return a;
47 } else {
48 geas::patom_t var = s.new_boolvar();
49 geas::add_clause(s.data, ~var, a);
50 geas::add_clause(s.data, ~var, b);
51 geas::add_clause(s.data, var, ~a, ~b);
52 return var;
53 }
54}
55
56void p_mk_intvar(SolverInstanceBase& s, const Definition* def) {
57 assert(STATE == geas::at_True);
58 assert(static_cast<BytecodeProc::Mode>(def->mode()) == BytecodeProc::RAW);
59 assert(def->timestamp() != -1);
60 assert(def->domain().isVec());
61
62 const Val& dom = def->domain();
63 assert(dom.size() == 2);
64
65 auto var = SOL.new_intvar(static_cast<geas::intvar::val_t>(dom[0]().toInt()),
66 static_cast<geas::intvar::val_t>(dom[1]().toInt()));
67 // if (isv->size() > 1) {
68 // vec<int> vals(static_cast<int>(isv->card().toInt()));
69 // int i = 0;
70 // for (int j = 0; j < isv->size(); ++j) {
71 // for (auto k = isv->min(i).toInt(); k <= isv->max(j).toInt(); ++k) {
72 // vals[i++] = static_cast<int>(k);
73 // }
74 // }
75 // assert(i == isv->card().toInt());
76 // auto res = geas::make_sparse(var, vals);
77 // assert(res);
78 // }
79 SI.insertVar(def, GeasVariable(var));
80}
81
82void p_int_eq(SolverInstanceBase& s, const Definition* call) {
83 auto m = static_cast<BytecodeProc::Mode>(call->mode());
84 switch (m) {
85 case BytecodeProc::ROOT:
86 geas::int_eq(SD, INTVAR(0), INTVAR(1), STATE);
87 break;
88 case BytecodeProc::ROOT_NEG:
89 geas::int_ne(SD, INTVAR(0), INTVAR(1), STATE);
90 break;
91 case BytecodeProc::FUN:
92 if (call->domain().isInt()) {
93 if (GeasSolverInstance::asBool(call->domain())) {
94 geas::int_eq(SD, INTVAR(0), INTVAR(1), STATE);
95 } else {
96 geas::int_ne(SD, INTVAR(0), INTVAR(1), STATE);
97 }
98 } else {
99 auto var = SOL.new_boolvar();
100 SI.insertVar(call, GeasVariable(var));
101 geas::int_eq(SD, INTVAR(0), INTVAR(1), lit_and(SOL, STATE, var));
102 geas::int_ne(SD, INTVAR(0), INTVAR(1), lit_and(SOL, STATE, ~var));
103 }
104 break;
105 case BytecodeProc::FUN_NEG:
106 if (call->domain().isInt()) {
107 if (GeasSolverInstance::asBool(call->domain())) {
108 geas::int_ne(SD, INTVAR(0), INTVAR(1), STATE);
109 } else {
110 geas::int_eq(SD, INTVAR(0), INTVAR(1), STATE);
111 }
112 } else {
113 auto var = SOL.new_boolvar();
114 SI.insertVar(call, GeasVariable(var));
115 geas::int_ne(SD, INTVAR(0), INTVAR(1), lit_and(SOL, STATE, var));
116 geas::int_eq(SD, INTVAR(0), INTVAR(1), lit_and(SOL, STATE, ~var));
117 }
118 break;
119 case BytecodeProc::IMP:
120 if (call->domain().isInt()) {
121 if (GeasSolverInstance::asBool(call->domain())) {
122 geas::int_eq(SD, INTVAR(0), INTVAR(1), STATE);
123 }
124 } else {
125 auto var = SOL.new_boolvar();
126 SI.insertVar(call, GeasVariable(var));
127 geas::int_eq(SD, INTVAR(0), INTVAR(1), lit_and(SOL, STATE, var));
128 }
129 case BytecodeProc::IMP_NEG:
130 if (call->domain().isInt()) {
131 if (GeasSolverInstance::asBool(call->domain())) {
132 geas::int_ne(SD, INTVAR(0), INTVAR(1), STATE);
133 }
134 } else {
135 auto var = SOL.new_boolvar();
136 SI.insertVar(call, GeasVariable(var));
137 geas::int_ne(SD, INTVAR(0), INTVAR(1), lit_and(SOL, STATE, var));
138 }
139 break;
140 case BytecodeProc::RAW:
141 assert(false);
142 break;
143 }
144}
145
146void p_int_le(SolverInstanceBase& s, const Definition* call) {
147 assert(STATE == geas::at_True);
148 auto m = static_cast<BytecodeProc::Mode>(call->mode());
149 switch (m) {
150 case BytecodeProc::ROOT:
151 geas::int_le(SD, INTVAR(0), INTVAR(1), 0, STATE);
152 break;
153 case BytecodeProc::ROOT_NEG:
154 geas::int_le(SD, INTVAR(1), INTVAR(0), -1, STATE);
155 break;
156 case BytecodeProc::FUN:
157 if (call->domain().isInt()) {
158 if (GeasSolverInstance::asBool(call->domain())) {
159 geas::int_le(SD, INTVAR(0), INTVAR(1), 0, STATE);
160 } else {
161 geas::int_le(SD, INTVAR(1), INTVAR(0), -1, STATE);
162 }
163 } else {
164 auto var = SOL.new_boolvar();
165 SI.insertVar(call, GeasVariable(var));
166 geas::int_le(SD, INTVAR(0), INTVAR(1), 0, lit_and(SOL, STATE, var));
167 geas::int_le(SD, INTVAR(1), INTVAR(0), -1, lit_and(SOL, STATE, ~var));
168 }
169 break;
170 case BytecodeProc::FUN_NEG:
171 if (call->domain().isInt()) {
172 if (GeasSolverInstance::asBool(call->domain())) {
173 geas::int_le(SD, INTVAR(1), INTVAR(0), -1, STATE);
174 } else {
175 geas::int_le(SD, INTVAR(0), INTVAR(1), 0, STATE);
176 }
177 } else {
178 auto var = SOL.new_boolvar();
179 SI.insertVar(call, GeasVariable(var));
180 geas::int_le(SD, INTVAR(1), INTVAR(0), -1, lit_and(SOL, STATE, var));
181 geas::int_le(SD, INTVAR(0), INTVAR(1), 0, lit_and(SOL, STATE, ~var));
182 }
183 break;
184 case BytecodeProc::IMP:
185 if (call->domain().isInt()) {
186 if (GeasSolverInstance::asBool(call->domain())) {
187 geas::int_le(SD, INTVAR(0), INTVAR(1), 0, STATE);
188 }
189 } else {
190 auto var = SOL.new_boolvar();
191 SI.insertVar(call, GeasVariable(var));
192 geas::int_le(SD, INTVAR(0), INTVAR(1), 0, lit_and(SOL, STATE, var));
193 }
194 case BytecodeProc::IMP_NEG:
195 if (call->domain().isInt()) {
196 if (GeasSolverInstance::asBool(call->domain())) {
197 geas::int_le(SD, INTVAR(1), INTVAR(0), -1, STATE);
198 }
199 } else {
200 auto var = SOL.new_boolvar();
201 SI.insertVar(call, GeasVariable(var));
202 geas::int_le(SD, INTVAR(1), INTVAR(0), -1, lit_and(SOL, STATE, var));
203 }
204 break;
205 case BytecodeProc::RAW:
206 assert(false);
207 break;
208 }
209}
210
211void p_int_lt(SolverInstanceBase& s, const Definition* call) {
212 assert(STATE == geas::at_True);
213 auto m = static_cast<BytecodeProc::Mode>(call->mode());
214 switch (m) {
215 case BytecodeProc::ROOT:
216 geas::int_le(SD, INTVAR(0), INTVAR(1), -1, STATE);
217 break;
218 case BytecodeProc::ROOT_NEG:
219 geas::int_le(SD, INTVAR(1), INTVAR(0), 0, STATE);
220 break;
221 case BytecodeProc::FUN:
222 if (call->domain().isInt()) {
223 if (GeasSolverInstance::asBool(call->domain())) {
224 geas::int_le(SD, INTVAR(0), INTVAR(1), -1, STATE);
225 } else {
226 geas::int_le(SD, INTVAR(1), INTVAR(0), 0, STATE);
227 }
228 } else {
229 auto var = SOL.new_boolvar();
230 SI.insertVar(call, GeasVariable(var));
231 geas::int_le(SD, INTVAR(0), INTVAR(1), -1, lit_and(SOL, STATE, var));
232 geas::int_le(SD, INTVAR(1), INTVAR(0), 0, lit_and(SOL, STATE, ~var));
233 }
234 break;
235 case BytecodeProc::FUN_NEG:
236 if (call->domain().isInt()) {
237 if (GeasSolverInstance::asBool(call->domain())) {
238 geas::int_le(SD, INTVAR(1), INTVAR(0), 0, STATE);
239 } else {
240 geas::int_le(SD, INTVAR(0), INTVAR(1), -1, STATE);
241 }
242 } else {
243 auto var = SOL.new_boolvar();
244 SI.insertVar(call, GeasVariable(var));
245 geas::int_le(SD, INTVAR(1), INTVAR(0), 0, lit_and(SOL, STATE, var));
246 geas::int_le(SD, INTVAR(0), INTVAR(1), -1, lit_and(SOL, STATE, ~var));
247 }
248 break;
249 case BytecodeProc::IMP:
250 if (call->domain().isInt()) {
251 if (GeasSolverInstance::asBool(call->domain())) {
252 geas::int_le(SD, INTVAR(0), INTVAR(1), -1, STATE);
253 }
254 } else {
255 auto var = SOL.new_boolvar();
256 SI.insertVar(call, GeasVariable(var));
257 geas::int_le(SD, INTVAR(0), INTVAR(1), -1, lit_and(SOL, STATE, var));
258 }
259 case BytecodeProc::IMP_NEG:
260 if (call->domain().isInt()) {
261 if (GeasSolverInstance::asBool(call->domain())) {
262 geas::int_le(SD, INTVAR(1), INTVAR(0), 0, STATE);
263 }
264 } else {
265 auto var = SOL.new_boolvar();
266 SI.insertVar(call, GeasVariable(var));
267 geas::int_le(SD, INTVAR(1), INTVAR(0), 0, lit_and(SOL, STATE, var));
268 }
269 break;
270 case BytecodeProc::RAW:
271 assert(false);
272 break;
273 }
274}
275
276void p_int_abs(SolverInstanceBase& s, const Definition* call) {
277 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
278 geas::int_abs(SD, INTVAR(1), INTVAR(0), STATE);
279}
280
281void p_int_times(SolverInstanceBase& s, const Definition* call) {
282 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
283 geas::int_mul(SD, INTVAR(0), INTVAR(1), INTVAR(2), STATE);
284}
285
286void p_int_div(SolverInstanceBase& s, const Definition* call) {
287 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
288 geas::int_div(SD, INTVAR(2), INTVAR(0), INTVAR(1), STATE);
289}
290
291void p_int_max(SolverInstanceBase& s, const Definition* call) {
292 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
293 vec<geas::intvar> vars = {INTVAR(0), INTVAR(1)};
294 geas::int_max(SD, INTVAR(2), vars, STATE);
295}
296
297void p_int_min(SolverInstanceBase& s, const Definition* call) {
298 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
299 vec<geas::intvar> vars = {-INTVAR(0), -INTVAR(1)};
300 geas::int_max(SD, -INTVAR(2), vars, STATE);
301}
302
303void p_int_lin_eq(SolverInstanceBase& s, const Definition* call) {
304 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
305 vec<int> pos = INTARRAY(0);
306 vec<int> neg(pos.size());
307 for (int i = 0; i < neg.size(); ++i) {
308 neg[i] = -pos[i];
309 }
310 vec<geas::intvar> vars = INTVARARRAY(1);
311 // TODO: Rewrite using MiniZinc Library??
312 geas::linear_le(SD, pos, vars, INT(2), STATE);
313 geas::linear_le(SD, neg, vars, -INT(2), STATE);
314}
315
316void p_int_lin_ne(SolverInstanceBase& s, const Definition* call) {
317 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
318 vec<int> cons = INTARRAY(0);
319 vec<geas::intvar> vars = INTVARARRAY(1);
320 geas::linear_ne(SD, cons, vars, INT(2), STATE);
321}
322
323void p_int_lin_le(SolverInstanceBase& s, const Definition* call) {
324 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
325 vec<int> cons = INTARRAY(0);
326 vec<geas::intvar> vars = INTVARARRAY(1);
327 geas::linear_le(SD, cons, vars, INT(2), STATE);
328}
329
330void p_int_lin_eq_imp(SolverInstanceBase& s, const Definition* call) {
331 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
332 vec<int> pos = INTARRAY(0);
333 vec<int> neg(pos.size());
334 for (int i = 0; i < neg.size(); ++i) {
335 neg[i] = -pos[i];
336 }
337 vec<geas::intvar> vars = INTVARARRAY(1);
338 // TODO: Rewrite using MiniZinc Library??
339 geas::linear_le(SD, pos, vars, INT(2), lit_and(SOL, STATE, BOOLVAR(3)));
340 geas::linear_le(SD, neg, vars, -INT(2), lit_and(SOL, STATE, BOOLVAR(3)));
341}
342
343void p_int_lin_ne_imp(SolverInstanceBase& s, const Definition* call) {
344 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
345 vec<int> cons = INTARRAY(0);
346 vec<geas::intvar> vars = INTVARARRAY(1);
347 geas::linear_ne(SD, cons, vars, INT(2), lit_and(SOL, STATE, BOOLVAR(3)));
348}
349
350void p_int_lin_le_imp(SolverInstanceBase& s, const Definition* call) {
351 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
352 vec<int> cons = INTARRAY(0);
353 vec<geas::intvar> vars = INTVARARRAY(1);
354 geas::linear_le(SD, cons, vars, INT(2), lit_and(SOL, STATE, BOOLVAR(3)));
355}
356
357void p_int_lin_eq_reif(SolverInstanceBase& s, const Definition* call) {
358 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
359 vec<int> pos = INTARRAY(0);
360 vec<int> neg(pos.size());
361 for (int i = 0; i < neg.size(); ++i) {
362 neg[i] = -pos[i];
363 }
364 vec<geas::intvar> vars = INTVARARRAY(1);
365 // TODO: Rewrite using MiniZinc Library??
366 geas::linear_le(SD, pos, vars, INT(2), lit_and(SOL, STATE, BOOLVAR(3)));
367 geas::linear_le(SD, neg, vars, -INT(2), lit_and(SOL, STATE, BOOLVAR(3)));
368 geas::linear_ne(SD, pos, vars, INT(2), lit_and(SOL, STATE, ~BOOLVAR(3)));
369}
370
371void p_int_lin_ne_reif(SolverInstanceBase& s, const Definition* call) {
372 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
373 vec<int> pos = INTARRAY(0);
374 vec<int> neg(pos.size());
375 for (int i = 0; i < neg.size(); ++i) {
376 neg[i] = -pos[i];
377 }
378 vec<geas::intvar> vars = INTVARARRAY(1);
379 // TODO: Rewrite using MiniZinc Library??
380 geas::linear_ne(SD, pos, vars, INT(2), lit_and(SOL, STATE, BOOLVAR(3)));
381 geas::linear_le(SD, pos, vars, INT(2), lit_and(SOL, STATE, ~BOOLVAR(3)));
382 geas::linear_le(SD, neg, vars, -INT(2), lit_and(SOL, STATE, ~BOOLVAR(3)));
383}
384
385void p_int_lin_le_reif(SolverInstanceBase& s, const Definition* call) {
386 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
387 vec<int> pos = INTARRAY(0);
388 vec<int> neg(pos.size());
389 for (int i = 0; i < neg.size(); ++i) {
390 neg[i] = -pos[i];
391 }
392 vec<geas::intvar> vars = INTVARARRAY(1);
393 geas::linear_le(SD, pos, vars, INT(2), lit_and(SOL, STATE, BOOLVAR(3)));
394 geas::linear_le(SD, neg, vars, -INT(2) - 1, lit_and(SOL, STATE, ~BOOLVAR(3)));
395}
396
397void p_bool_eq(SolverInstanceBase& s, const Definition* call) {
398 assert(STATE == geas::at_True);
399 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
400 if (PAR(0)) {
401 SOL.post(BOOL(0) ? BOOLVAR(1) : ~BOOLVAR(1));
402 } else if (PAR(2)) {
403 SOL.post(BOOL(1) ? BOOLVAR(0) : ~BOOLVAR(0));
404 } else {
405 geas::add_clause(SD, BOOLVAR(0), ~BOOLVAR(1));
406 geas::add_clause(SD, ~BOOLVAR(0), BOOLVAR(1));
407 }
408}
409
410void p_bool_ne(SolverInstanceBase& s, const Definition* call) {
411 assert(STATE == geas::at_True);
412 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
413 if (PAR(0)) {
414 SOL.post(BOOL(0) ? ~BOOLVAR(1) : BOOLVAR(1));
415 } else if (PAR(1)) {
416 SOL.post(BOOL(1) ? ~BOOLVAR(0) : BOOLVAR(0));
417 } else {
418 geas::add_clause(SD, BOOLVAR(0), BOOLVAR(1));
419 geas::add_clause(SD, ~BOOLVAR(0), ~BOOLVAR(1));
420 }
421}
422
423void p_bool_le(SolverInstanceBase& s, const Definition* call) {
424 assert(STATE == geas::at_True);
425 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
426 if (PAR(0)) {
427 if (BOOL(0)) {
428 SOL.post(BOOLVAR(1));
429 }
430 } else if (PAR(1)) {
431 if (!BOOL(1)) {
432 SOL.post(~BOOLVAR(0));
433 }
434 } else {
435 geas::add_clause(SD, ~BOOLVAR(0), BOOLVAR(1));
436 }
437}
438
439void p_bool_lt(SolverInstanceBase& s, const Definition* call) {
440 assert(STATE == geas::at_True);
441 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
442 SOL.post(~BOOLVAR(0));
443 SOL.post(BOOLVAR(1));
444}
445
446void p_bool_eq_imp(SolverInstanceBase& s, const Definition* call) {
447 assert(STATE == geas::at_True);
448 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
449 if (PAR(2)) {
450 if (BOOL(2)) {
451 p_bool_eq(s, call);
452 }
453 } else {
454 geas::add_clause(SD, ~BOOLVAR(2), ~BOOLVAR(0), BOOLVAR(1));
455 geas::add_clause(SD, ~BOOLVAR(2), BOOLVAR(0), ~BOOLVAR(1));
456 }
457}
458
459void p_bool_ne_imp(SolverInstanceBase& s, const Definition* call) {
460 assert(STATE == geas::at_True);
461 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
462 if (PAR(2)) {
463 if (BOOL(2)) {
464 p_bool_ne(s, call);
465 }
466 } else {
467 geas::add_clause(SD, ~BOOLVAR(2), BOOLVAR(0), BOOLVAR(1));
468 geas::add_clause(SD, ~BOOLVAR(2), ~BOOLVAR(0), ~BOOLVAR(1));
469 }
470}
471
472void p_bool_le_imp(SolverInstanceBase& s, const Definition* call) {
473 assert(STATE == geas::at_True);
474 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
475 if (PAR(2)) {
476 if (BOOL(2)) {
477 p_bool_le(s, call);
478 }
479 } else {
480 geas::add_clause(SD, ~BOOLVAR(2), ~BOOLVAR(0), BOOLVAR(1));
481 }
482}
483
484void p_bool_lt_imp(SolverInstanceBase& s, const Definition* call) {
485 assert(STATE == geas::at_True);
486 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
487 if (PAR(2)) {
488 if (BOOL(2)) {
489 p_bool_lt(s, call);
490 }
491 } else {
492 geas::add_clause(SD, ~BOOLVAR(2), ~BOOLVAR(0));
493 geas::add_clause(SD, ~BOOLVAR(2), BOOLVAR(1));
494 }
495}
496
497void p_bool_eq_reif(SolverInstanceBase& s, const Definition* call) {
498 assert(STATE == geas::at_True);
499 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
500 if (PAR(2)) {
501 if (BOOL(2)) {
502 p_bool_eq(s, call);
503 } else {
504 p_bool_ne(s, call);
505 }
506 } else {
507 geas::add_clause(SD, BOOLVAR(2), BOOLVAR(0), BOOLVAR(1));
508 geas::add_clause(SD, BOOLVAR(2), ~BOOLVAR(0), ~BOOLVAR(1));
509 geas::add_clause(SD, ~BOOLVAR(2), ~BOOLVAR(0), BOOLVAR(1));
510 geas::add_clause(SD, ~BOOLVAR(2), BOOLVAR(0), ~BOOLVAR(1));
511 }
512}
513
514void p_bool_ne_reif(SolverInstanceBase& s, const Definition* call) {
515 assert(STATE == geas::at_True);
516 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
517 if (PAR(2)) {
518 if (BOOL(2)) {
519 p_bool_ne(s, call);
520 } else {
521 p_bool_eq(s, call);
522 }
523 } else {
524 geas::add_clause(SD, BOOLVAR(2), ~BOOLVAR(0), BOOLVAR(1));
525 geas::add_clause(SD, BOOLVAR(2), BOOLVAR(0), ~BOOLVAR(1));
526 geas::add_clause(SD, ~BOOLVAR(2), BOOLVAR(0), BOOLVAR(1));
527 geas::add_clause(SD, ~BOOLVAR(2), ~BOOLVAR(0), ~BOOLVAR(1));
528 }
529}
530
531void p_bool_le_reif(SolverInstanceBase& s, const Definition* call) {
532 assert(STATE == geas::at_True);
533 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
534 if (PAR(2)) {
535 if (BOOL(2)) {
536 p_bool_le(s, call);
537 } else {
538 // auto nc = new Call(Location().introduce(), call->id(), {call->arg(1),
539 // call->arg(0)}); p_bool_lt(s, nc);
540 }
541 } else {
542 geas::add_clause(SD, BOOLVAR(2), ~BOOLVAR(1));
543 geas::add_clause(SD, BOOLVAR(2), BOOLVAR(0));
544 geas::add_clause(SD, ~BOOLVAR(2), ~BOOLVAR(0), BOOLVAR(1));
545 }
546}
547
548void p_bool_lt_reif(SolverInstanceBase& s, const Definition* call) {
549 assert(STATE == geas::at_True);
550 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
551 if (PAR(2)) {
552 if (BOOL(2)) {
553 p_int_lt(s, call);
554 } else {
555 // auto nc = new Call(Location().introduce(), call->id(), {call->arg(1),
556 // call->arg(0)}); p_int_le(s, nc);
557 }
558 } else {
559 geas::add_clause(SD, ~BOOLVAR(2), ~BOOLVAR(0));
560 geas::add_clause(SD, ~BOOLVAR(2), BOOLVAR(1));
561 geas::add_clause(SD, BOOLVAR(2), BOOLVAR(0), ~BOOLVAR(1));
562 }
563}
564
565void p_bool_or(SolverInstanceBase& s, const Definition* call) {
566 assert(STATE == geas::at_True);
567 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
568 geas::add_clause(SD, BOOLVAR(2), ~BOOLVAR(0));
569 geas::add_clause(SD, BOOLVAR(2), ~BOOLVAR(1));
570 geas::add_clause(SD, ~BOOLVAR(2), BOOLVAR(0), BOOLVAR(1));
571}
572
573void p_bool_and(SolverInstanceBase& s, const Definition* call) {
574 assert(STATE == geas::at_True);
575 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
576 geas::add_clause(SD, ~BOOLVAR(2), BOOLVAR(0));
577 geas::add_clause(SD, ~BOOLVAR(2), BOOLVAR(1));
578 geas::add_clause(SD, BOOLVAR(2), ~BOOLVAR(0), ~BOOLVAR(1));
579}
580
581void p_bool_xor(SolverInstanceBase& s, const Definition* call) {
582 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
583 if (call->size() == 2) {
584 p_bool_ne(s, call);
585 } else {
586 p_bool_ne_reif(s, call);
587 }
588}
589
590void p_bool_not(SolverInstanceBase& s, const Definition* call) {
591 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
592 p_bool_ne(s, call);
593}
594
595void p_bool_or_imp(SolverInstanceBase& s, const Definition* call) {
596 assert(STATE == geas::at_True);
597 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
598 geas::add_clause(SD, ~BOOLVAR(2), BOOLVAR(0), BOOLVAR(1));
599}
600
601void p_bool_and_imp(SolverInstanceBase& s, const Definition* call) {
602 assert(STATE == geas::at_True);
603 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
604 geas::add_clause(SD, ~BOOLVAR(2), BOOLVAR(0));
605 geas::add_clause(SD, ~BOOLVAR(2), BOOLVAR(1));
606}
607
608void p_bool_xor_imp(SolverInstanceBase& s, const Definition* call) {
609 assert(STATE == geas::at_True);
610 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
611 p_bool_ne_imp(s, call);
612}
613
614void p_bool_clause(SolverInstanceBase& s, const Definition* call) {
615 assert(STATE == geas::at_True);
616 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
617 auto& gi = static_cast<GeasSolverInstance&>(s);
618 auto pos = ARRAY(0);
619 auto neg = ARRAY(1);
620 vec<geas::clause_elt> clause;
621 for (int i = 0; i < pos.size(); ++i) {
622 clause.push(SI.asBoolVar(pos[i]));
623 }
624 for (int j = 0; j < neg.size(); ++j) {
625 clause.push(~SI.asBoolVar(neg[j]));
626 }
627 geas::add_clause(*SD, clause);
628}
629
630void p_array_bool_or(SolverInstanceBase& s, const Definition* call) {
631 assert(STATE == geas::at_True);
632 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
633 auto arr = ARRAY(0);
634 vec<geas::clause_elt> clause;
635 clause.push(~BOOLVAR(1));
636 for (int i = 0; i < arr.size(); ++i) {
637 geas::patom_t elem = SI.asBoolVar(arr[i]);
638 geas::add_clause(SD, BOOLVAR(1), ~elem);
639 clause.push(elem);
640 }
641 geas::add_clause(*SD, clause);
642}
643
644void p_array_bool_and(SolverInstanceBase& s, const Definition* call) {
645 assert(STATE == geas::at_True);
646 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
647 auto arr = ARRAY(0);
648 vec<geas::clause_elt> clause;
649 clause.push(BOOLVAR(1));
650 for (int i = 0; i < arr.size(); ++i) {
651 geas::patom_t elem = SI.asBoolVar(arr[i]);
652 geas::add_clause(SD, ~BOOLVAR(1), elem);
653 clause.push(~elem);
654 }
655 geas::add_clause(*SD, clause);
656}
657
658void p_bool_clause_imp(SolverInstanceBase& s, const Definition* call) {
659 assert(STATE == geas::at_True);
660 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
661 auto pos = ARRAY(0);
662 auto neg = ARRAY(1);
663 vec<geas::clause_elt> clause;
664 clause.push(~BOOLVAR(2));
665 for (int i = 0; i < pos.size(); ++i) {
666 clause.push(SI.asBoolVar(pos[i]));
667 }
668 for (int j = 0; j < neg.size(); ++j) {
669 clause.push(~SI.asBoolVar(neg[j]));
670 }
671 geas::add_clause(*SD, clause);
672}
673
674void p_array_bool_or_imp(SolverInstanceBase& s, const Definition* call) {
675 assert(STATE == geas::at_True);
676 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
677 auto arr = ARRAY(0);
678 vec<geas::clause_elt> clause;
679 clause.push(~BOOLVAR(1));
680 for (int i = 0; i < arr.size(); ++i) {
681 geas::patom_t elem = SI.asBoolVar(arr[i]);
682 clause.push(elem);
683 }
684 geas::add_clause(*SD, clause);
685}
686
687void p_array_bool_and_imp(SolverInstanceBase& s, const Definition* call) {
688 assert(STATE == geas::at_True);
689 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
690 auto arr = ARRAY(0);
691 for (int i = 0; i < arr.size(); ++i) {
692 geas::add_clause(SD, ~BOOLVAR(1), SI.asBoolVar(arr[i]));
693 }
694}
695
696void p_bool_clause_reif(SolverInstanceBase& s, const Definition* call) {
697 assert(STATE == geas::at_True);
698 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
699 auto pos = ARRAY(0);
700 auto neg = ARRAY(1);
701 vec<geas::clause_elt> clause;
702 clause.push(~BOOLVAR(2));
703 for (int i = 0; i < pos.size(); ++i) {
704 geas::patom_t elem = SI.asBoolVar(pos[i]);
705 geas::add_clause(SD, BOOLVAR(2), ~elem);
706 clause.push(elem);
707 }
708 for (int j = 0; j < neg.size(); ++j) {
709 geas::patom_t elem = SI.asBoolVar(neg[j]);
710 geas::add_clause(SD, BOOLVAR(2), elem);
711 clause.push(~elem);
712 }
713 geas::add_clause(*SD, clause);
714}
715
716void p_bool_lin_eq(SolverInstanceBase& s, const Definition* call) {
717 assert(STATE == geas::at_True);
718 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
719 vec<int> cons = INTARRAY(0);
720 vec<geas::patom_t> vars = BOOLVARARRAY(1);
721 // TODO: Rewrite using MiniZinc Library??
722 geas::bool_linear_le(SD, geas::at_True, SI.zero, cons, vars, -INT(2));
723 geas::bool_linear_ge(SD, geas::at_True, SI.zero, cons, vars, -INT(2));
724}
725
726void p_bool_lin_ne(SolverInstanceBase& s, const Definition* call) {
727 assert(STATE == geas::at_True);
728 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
729 vec<int> cons = INTARRAY(0);
730 vec<geas::patom_t> vars = BOOLVARARRAY(1);
731 geas::bool_linear_ne(SD, cons, vars, INT(2));
732}
733
734void p_bool_lin_le(SolverInstanceBase& s, const Definition* call) {
735 assert(STATE == geas::at_True);
736 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
737 vec<int> cons = INTARRAY(0);
738 vec<geas::patom_t> vars = BOOLVARARRAY(1);
739 geas::bool_linear_le(SD, geas::at_True, SI.zero, cons, vars, -INT(2));
740}
741
742void p_bool_lin_eq_imp(SolverInstanceBase& s, const Definition* call) {
743 assert(STATE == geas::at_True);
744 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
745 vec<int> cons = INTARRAY(0);
746 vec<geas::patom_t> vars = BOOLVARARRAY(1);
747 // TODO: Rewrite using MiniZinc Library??
748 geas::bool_linear_le(SD, BOOLVAR(3), SI.zero, cons, vars, -INT(2));
749 geas::bool_linear_ge(SD, BOOLVAR(3), SI.zero, cons, vars, -INT(2));
750}
751
752void p_bool_lin_ne_imp(SolverInstanceBase& s, const Definition* call) {
753 assert(STATE == geas::at_True);
754 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
755 vec<int> cons = INTARRAY(0);
756 vec<geas::patom_t> vars = BOOLVARARRAY(1);
757 geas::bool_linear_ne(SD, cons, vars, INT(2), BOOLVAR(3));
758}
759
760void p_bool_lin_le_imp(SolverInstanceBase& s, const Definition* call) {
761 assert(STATE == geas::at_True);
762 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
763 vec<int> cons = INTARRAY(0);
764 vec<geas::patom_t> vars = BOOLVARARRAY(1);
765 geas::bool_linear_le(SD, BOOLVAR(3), SI.zero, cons, vars, -INT(2));
766}
767
768void p_bool_lin_eq_reif(SolverInstanceBase& s, const Definition* call) {
769 assert(STATE == geas::at_True);
770 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
771 vec<int> cons = INTARRAY(0);
772 vec<geas::patom_t> vars = BOOLVARARRAY(1);
773 // TODO: Rewrite using MiniZinc Library??
774 geas::bool_linear_le(SD, BOOLVAR(3), SI.zero, cons, vars, -INT(2));
775 geas::bool_linear_ge(SD, BOOLVAR(3), SI.zero, cons, vars, -INT(2));
776 geas::bool_linear_ne(SD, cons, vars, INT(2), ~BOOLVAR(3));
777}
778
779void p_bool_lin_ne_reif(SolverInstanceBase& s, const Definition* call) {
780 assert(STATE == geas::at_True);
781 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
782 vec<int> cons = INTARRAY(0);
783 vec<geas::patom_t> vars = BOOLVARARRAY(1);
784 // TODO: Rewrite using MiniZinc Library??
785 geas::bool_linear_ne(SD, cons, vars, INT(2), BOOLVAR(3));
786 geas::bool_linear_le(SD, ~BOOLVAR(3), SI.zero, cons, vars, -INT(2));
787 geas::bool_linear_ge(SD, ~BOOLVAR(3), SI.zero, cons, vars, -INT(2));
788}
789
790void p_bool_lin_le_reif(SolverInstanceBase& s, const Definition* call) {
791 assert(STATE == geas::at_True);
792 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
793 vec<int> cons = INTARRAY(0);
794 vec<geas::patom_t> vars = BOOLVARARRAY(1);
795 // TODO: Rewrite using MiniZinc Library??
796 geas::bool_linear_le(SD, BOOLVAR(3), SI.zero, cons, vars, -INT(2));
797 geas::bool_linear_ge(SD, ~BOOLVAR(3), SI.zero, cons, vars, -INT(2) - 1);
798}
799
800void p_bool2int(SolverInstanceBase& s, const Definition* call) {
801 assert(STATE == geas::at_True);
802 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
803 geas::add_clause(SD, BOOLVAR(0), INTVAR(1) <= 0);
804 geas::add_clause(SD, ~BOOLVAR(0), INTVAR(1) >= 1);
805}
806
807void p_array_int_element(SolverInstanceBase& s, const Definition* call) {
808 assert(STATE == geas::at_True);
809 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
810 // assert(ARRAY(1)->min(0) == 1 && ARRAY(1)->max(0) == ARRAY(1)->size()+1);
811 vec<int> vals = INTARRAY(1);
812 if (PAR(0)) {
813 SOL.post(INTVAR(2) == vals[INT(0) - 1]);
814 } else if (PAR(2)) {
815 for (int j = 0; j < vals.size(); ++j) {
816 if (vals[j] != INT(2)) {
817 SOL.post(INTVAR(0) != j + 1);
818 }
819 }
820 } else {
821 geas::int_element(SD, INTVAR(2), INTVAR(0), vals);
822 }
823}
824
825void p_array_bool_element(SolverInstanceBase& s, const Definition* call) {
826 assert(STATE == geas::at_True);
827 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
828 // assert(ARRAY(1)->min(0) == 1 && ARRAY(1)->max(0) == ARRAY(1)->size()+1);
829 vec<bool> vals = BOOLARRAY(1);
830 if (PAR(0)) {
831 SOL.post(vals[INT(0) - 1] ? BOOLVAR(2) : ~BOOLVAR(2));
832 } else if (PAR(2)) {
833 for (int j = 0; j < vals.size(); ++j) {
834 if (vals[j] != BOOL(2)) {
835 SOL.post(INTVAR(0) != j + 1);
836 }
837 }
838 } else {
839 for (int j = 0; j < vals.size(); ++j) {
840 geas::add_clause(SD, INTVAR(0) != j + 1, vals[j] ? BOOLVAR(2) : ~BOOLVAR(2));
841 }
842 }
843}
844
845void p_array_var_int_element(SolverInstanceBase& s, const Definition* call) {
846 assert(STATE == geas::at_True);
847 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
848 // assert(ARRAY(1)->min(0) == 1 && ARRAY(1)->max(0) == ARRAY(1)->size()+1);
849 if (PAR(1)) {
850 return p_array_int_element(s, call);
851 }
852 if (PAR(0) && PAR(2)) {
853 SOL.post(SI.asIntVar(ARRAY(1)[INT(0) - 1]) == INT(2));
854 } else if (PAR(0)) {
855 Val elem = ARRAY(1)[INT(0) - 1];
856 if (elem.isInt()) {
857 return p_array_int_element(s, call);
858 } else {
859 geas::int_eq(SD, SI.asIntVar(elem), INTVAR(2));
860 }
861 } else if (PAR(2)) {
862 for (int j = 0; j < ARRAY(1).size(); ++j) {
863 Val elem = ARRAY(1)[j];
864 if (elem.isDef()) {
865 geas::add_clause(SD, INTVAR(0) != j + 1, SI.asIntVar(elem) == INT(2));
866 } else {
867 if (SI.asInt(elem) != INT(2)) {
868 SOL.post(INTVAR(0) != j + 1);
869 }
870 }
871 }
872 } else {
873 vec<geas::intvar> vals = INTVARARRAY(1);
874 geas::var_int_element(SD, INTVAR(2), INTVAR(0), vals);
875 }
876}
877
878void p_array_var_bool_element(SolverInstanceBase& s, const Definition* call) {
879 assert(STATE == geas::at_True);
880 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
881 // assert(ARRAY(1)->min(0) == 1 && ARRAY(1)->max(0) == ARRAY(1)->size()+1);
882 if (PAR(1)) {
883 return p_array_bool_element(s, call);
884 }
885 if (PAR(0) && PAR(2)) {
886 SOL.post(BOOL(2) ? SI.asBoolVar(ARRAY(1)[INT(0) - 1]) : ~SI.asBoolVar(ARRAY(1)[INT(0) - 1]));
887 } else if (PAR(0)) {
888 Val elem = ARRAY(1)[INT(0) - 1];
889 if (elem.isInt()) {
890 return p_array_bool_element(s, call);
891 } else {
892 geas::add_clause(SD, BOOLVAR(2), ~SI.asBoolVar(elem));
893 geas::add_clause(SD, ~BOOLVAR(2), SI.asBoolVar(elem));
894 }
895 } else if (PAR(2)) {
896 for (int j = 0; j < ARRAY(1).size(); ++j) {
897 Val elem = ARRAY(1)[j];
898 if (elem.isDef()) {
899 geas::add_clause(SD, INTVAR(0) != j + 1, INT(2) ? SI.asBoolVar(elem) : ~SI.asBoolVar(elem));
900 } else {
901 if (SI.asBool(elem) != INT(2)) {
902 SOL.post(INTVAR(0) != j + 1);
903 }
904 }
905 }
906 } else {
907 auto vars = BOOLVARARRAY(1);
908 for (int j = 0; j < vars.size(); ++j) {
909 geas::add_clause(SD, INTVAR(0) != j + 1, ~vars[j], BOOLVAR(2));
910 geas::add_clause(SD, INTVAR(0) != j + 1, vars[j], ~BOOLVAR(2));
911 }
912 }
913}
914
915void p_all_different(SolverInstanceBase& s, const Definition* call) {
916 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
917 vec<geas::intvar> vars = INTVARARRAY(0);
918 geas::all_different_int(SD, vars, STATE);
919}
920
921void p_all_different_except_0(SolverInstanceBase& s, const Definition* call) {
922 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
923 vec<geas::intvar> vars = INTVARARRAY(0);
924 geas::all_different_except_0(SD, vars, STATE);
925}
926
927void p_at_most(SolverInstanceBase& s, const Definition* call) {
928 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
929 vec<geas::intvar> ivars = INTVARARRAY(1);
930 vec<geas::patom_t> bvars;
931 for (auto& ivar : ivars) {
932 bvars.push(ivar == INT(2));
933 }
934
935 if (INT(0) == 1) {
936 geas::atmost_1(SD, bvars, STATE);
937 } else {
938 geas::atmost_k(SD, bvars, INT(0), STATE);
939 }
940}
941
942void p_at_most1(SolverInstanceBase& s, const Definition* call) {
943 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
944 vec<geas::intvar> ivars = INTVARARRAY(0);
945 vec<geas::patom_t> bvars;
946 for (auto& ivar : ivars) {
947 bvars.push(ivar == INT(1));
948 }
949 geas::atmost_1(SD, bvars, STATE);
950}
951
952void p_cumulative(SolverInstanceBase& s, const Definition* call) {
953 assert(STATE == geas::at_True);
954 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
955 vec<geas::intvar> st = INTVARARRAY(0);
956 if (PAR(1) && PAR(2) && PAR(3)) {
957 vec<int> d = INTARRAY(1);
958 vec<int> r = INTARRAY(2);
959 geas::cumulative(SD, st, d, r, INT(3));
960 } else {
961 vec<geas::intvar> d = INTVARARRAY(1);
962 vec<geas::intvar> r = INTVARARRAY(2);
963 geas::cumulative_var(SD, st, d, r, INTVAR(3));
964 }
965}
966
967void p_disjunctive(SolverInstanceBase& s, const Definition* call) {
968 assert(STATE == geas::at_True);
969 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
970 vec<geas::intvar> st = INTVARARRAY(0);
971 if (PAR(1)) {
972 vec<int> d = INTARRAY(1);
973 geas::disjunctive_int(SD, st, d);
974 } else {
975 vec<geas::intvar> d = INTVARARRAY(1);
976 geas::disjunctive_var(SD, st, d);
977 }
978}
979
980void p_global_cardinality(SolverInstanceBase& s, const Definition* call) {
981 assert(STATE == geas::at_True);
982 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
983 vec<geas::intvar> x = INTVARARRAY(0);
984 vec<int> cover = INTARRAY(1);
985 vec<int> count = INTARRAY(2);
986
987 vec<int> srcs(x.size(), 1);
988 vec<geas::bflow> flows;
989 for (int i = 0; i < x.size(); ++i) {
990 for (int j = 0; j < cover.size(); ++j) {
991 if (x[i].lb(SD) <= cover[j] && cover[j] <= x[i].ub(SD)) {
992 flows.push({i, j, x[i] == cover[j]});
993 }
994 }
995 }
996 geas::bipartite_flow(SD, srcs, count, flows);
997}
998
999void p_table_int(SolverInstanceBase& s, const Definition* call) {
1000 assert(STATE == geas::at_True);
1001 assert(static_cast<BytecodeProc::Mode>(call->mode()) == BytecodeProc::ROOT);
1002 auto& gi = static_cast<GeasSolverInstance&>(s);
1003 vec<geas::intvar> vars = INTVARARRAY(0);
1004 vec<int> tmp = INTARRAY(1);
1005 assert(tmp.size() % vars.size() == 0);
1006 vec<vec<int>> table(tmp.size() / vars.size());
1007 for (int i = 0; i < table.size(); ++i) {
1008 vec<int> row(vars.size());
1009 for (int j = 0; j < vars.size(); ++j) {
1010 row[j] = tmp[i * vars.size() + j];
1011 }
1012 table.push(row);
1013 }
1014 geas::table_id id = geas::table::build(SD, table);
1015 // TODO: Annotations for table versions
1016 geas::table::post(SD, id, vars);
1017}
1018
1019} // namespace GeasConstraints
1020} // namespace MiniZinc
1021
1022#pragma clang diagnostic pop