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 * Guido Tack <guido.tack@monash.edu>
7 */
8
9/* This Source Code Form is subject to the terms of the Mozilla Public
10 * License, v. 2.0. If a copy of the MPL was not distributed with this
11 * file, You can obtain one at http://mozilla.org/MPL/2.0/. */
12
13#include <minizinc/eval_par.hh>
14#include <minizinc/interpreter.hh>
15#include <minizinc/interpreter/primitives.hh>
16#include <minizinc/iter.hh>
17#include <minizinc/model.hh>
18#include <minizinc/solver_instance_base.hh>
19
20#include <fstream>
21#include <iostream>
22#include <streambuf>
23#include <unordered_map>
24
25// #define DBG_CALLTRACE(msg) std::cerr << msg
26#define DBG_CALLTRACE(msg) \
27 do { \
28 } while (0)
29
30namespace MiniZinc {
31
32Val AggregationCtx::createVec(Interpreter* interpreter, int timestamp) const {
33 return Val(Vec::a(interpreter, timestamp, stack));
34}
35
36AggregationCtx::~AggregationCtx(void) {
37 /// TODO
38}
39
40const std::string AggregationCtx::symbol_to_string[] = {"AND", "OR", "VEC", "OTHER"};
41
42const std::string Interpreter::status_to_string[] = {"Roger", "Aborted", "Inconsistent", "Error"};
43
44void Interpreter::pushAgg(const Val& v, int stackOffset) {
45 assert(stackOffset < 0);
46 assert(_agg.size() + stackOffset >= 0);
47 // push value onto surrounding context
48 _agg[_agg.size() + stackOffset].push(this, v);
49}
50
51void Interpreter::pushConstraint(Constraint* c) { _agg.back().constraints.push_back(c); }
52
53PropStatus Interpreter::subscribe(Constraint* c) {
54 // TODO: This disables propagation after trailing, this shouldn't be necessary if we can correctly
55 // communicate with the solvers
56 if (trail.is_trailed(_root_var)) {
57 return PS_OK;
58 }
59 if (c->pred() < primitiveMap().size()) {
60 return primitiveMap()[c->pred()]->subscribe(*this, c);
61 }
62 return PS_OK;
63}
64
65void Interpreter::unsubscribe(Constraint* c) {
66 if (c->pred() < primitiveMap().size()) {
67 primitiveMap()[c->pred()]->unsubscribe(*this, c);
68 }
69}
70
71void Interpreter::schedule(Constraint* c, const Variable::SubscriptionEvent& ev) {
72 if (!c->scheduled()) {
73 _propQueue.push_back(c);
74 c->scheduled(true);
75 }
76}
77
78void Interpreter::deschedule(Constraint* c) {
79 /// TODO: is this required? seems to be unused
80 if (c->scheduled()) {
81 auto it = std::find(_propQueue.begin(), _propQueue.end(), c);
82 if (it != _propQueue.end()) {
83 _propQueue.erase(it);
84 }
85 }
86}
87
88void Interpreter::propagate(void) {
89 while (!_propQueue.empty()) {
90 Constraint* c = _propQueue.front();
91 _propQueue.pop_front();
92 c->scheduled(false);
93 auto ps = primitiveMap()[c->pred()]->propagate(*this, c);
94 switch (ps) {
95 case PS_OK:
96 break;
97 case PS_FAILED:
98 _status = INCONSISTENT;
99 return;
100 case PS_ENTAILED:
101 // TODO: remove constraint
102 break;
103 }
104 }
105}
106
107void Interpreter::run(void) {
108 if (_status != ROGER) {
109 return;
110 }
111 for (;;) {
112 DBG_INTERPRETER(frame().pc << " ");
113 switch (frame().bs->instr(frame().pc)) {
114 case BytecodeStream::ADDI: {
115 if (frame().pc > 130) {
116 DBG_INTERPRETER("NOOOOO!\n");
117 }
118 int r1 = frame().bs->reg(frame().pc);
119 int r2 = frame().bs->reg(frame().pc);
120 int r3 = frame().bs->reg(frame().pc);
121 DBG_INTERPRETER("ADDI R" << r1 << "(" << reg(frame(), r1).toString() << ")"
122 << " R" << r2 << "(" << reg(frame(), r2).toString() << ")");
123 assign(frame(), r3, reg(frame(), r1) + reg(frame(), r2));
124 DBG_INTERPRETER(" R" << r3 << "(" << reg(frame(), r3).toString() << ")"
125 << "\n");
126 } break;
127 case BytecodeStream::SUBI: {
128 int r1 = frame().bs->reg(frame().pc);
129 int r2 = frame().bs->reg(frame().pc);
130 int r3 = frame().bs->reg(frame().pc);
131 DBG_INTERPRETER("SUBI R" << r1 << "(" << reg(frame(), r1).toString() << ")"
132 << " R" << r2 << "(" << reg(frame(), r2).toString() << ")");
133 assign(frame(), r3, reg(frame(), r1) - reg(frame(), r2));
134 DBG_INTERPRETER(" R" << r3 << "(" << reg(frame(), r3).toString() << ")"
135 << "\n");
136 } break;
137 case BytecodeStream::MULI: {
138 int r1 = frame().bs->reg(frame().pc);
139 int r2 = frame().bs->reg(frame().pc);
140 int r3 = frame().bs->reg(frame().pc);
141 DBG_INTERPRETER("MULI R" << r1 << "(" << reg(frame(), r1).toString() << ")"
142 << " R" << r2 << "(" << reg(frame(), r2).toString() << ")");
143 assign(frame(), r3, reg(frame(), r1) * reg(frame(), r2));
144 DBG_INTERPRETER(" R" << r3 << "(" << reg(frame(), r3).toString() << ")"
145 << "\n");
146 } break;
147 case BytecodeStream::DIVI: {
148 int r1 = frame().bs->reg(frame().pc);
149 int r2 = frame().bs->reg(frame().pc);
150 int r3 = frame().bs->reg(frame().pc);
151 if (reg(frame(), r2) == 0)
152 frame().pc = frame().bs->size() - 1;
153 else
154 assign(frame(), r3, reg(frame(), r1) / reg(frame(), r2));
155 assign(frame(), r3, reg(frame(), r1) / reg(frame(), r2));
156 DBG_INTERPRETER("DIVI R" << r1 << "(" << reg(frame(), r1).toString() << ")"
157 << " R" << r2 << "(" << reg(frame(), r2).toString() << ")"
158 << " " << r3 << "(" << reg(frame(), r3).toString() << ")"
159 << "\n");
160 } break;
161 case BytecodeStream::MODI: {
162 int r1 = frame().bs->reg(frame().pc);
163 int r2 = frame().bs->reg(frame().pc);
164 int r3 = frame().bs->reg(frame().pc);
165 if (reg(frame(), r2) == 0)
166 frame().pc = frame().bs->size() - 1;
167 else
168 assign(frame(), r3, reg(frame(), r1) % reg(frame(), r2));
169 DBG_INTERPRETER("MODI R" << r1 << "(" << reg(frame(), r1).toString() << ")"
170 << " R" << r2 << "(" << reg(frame(), r2).toString() << ")"
171 << " " << r3 << "(" << reg(frame(), r3).toString() << ")"
172 << "\n");
173 } break;
174 case BytecodeStream::INCI: {
175 int r1 = frame().bs->reg(frame().pc);
176 assign(frame(), r1, reg(frame(), r1) + 1);
177 DBG_INTERPRETER("INCI R" << r1 << "(" << reg(frame(), r1).toString() << ")"
178 << "\n");
179 } break;
180 case BytecodeStream::DECI: {
181 int r1 = frame().bs->reg(frame().pc);
182 DBG_INTERPRETER("DECI R" << r1 << "(" << reg(frame(), r1).toString() << ")"
183 << "\n");
184 assign(frame(), r1, reg(frame(), r1) - 1);
185 } break;
186 case BytecodeStream::IMMI: {
187 Val i = frame().bs->intval(frame().pc);
188 int r1 = frame().bs->reg(frame().pc);
189 assign(frame(), r1, i);
190 DBG_INTERPRETER("IMMI " << i.toString() << " R" << r1 << "(" << reg(frame(), r1).toString()
191 << ")"
192 << "\n");
193 } break;
194 case BytecodeStream::CLEAR: {
195 int r1 = frame().bs->reg(frame().pc);
196 int r2 = frame().bs->reg(frame().pc);
197 assert(r1 <= r2);
198 for (int i = r1; i <= r2; i++) {
199 assign(frame(), i, 0);
200 }
201 DBG_INTERPRETER("CLEAR "
202 << " R" << r1 << " " << r2 << "\n");
203 } break;
204 case BytecodeStream::LOAD_GLOBAL: {
205 int i = frame().bs->reg(frame().pc);
206 int r1 = frame().bs->reg(frame().pc);
207 globals.cp(this, i, _registers, frame().reg_offset + r1);
208 DBG_INTERPRETER("LOAD_GLOBAL " << i << " R" << r1 << "("
209 << reg(frame(), r1).toString(DBG_TRIM_OUTPUT) << ")"
210 << "\n");
211 } break;
212 case BytecodeStream::STORE_GLOBAL: {
213 int r1 = frame().bs->reg(frame().pc);
214 int i = frame().bs->reg(frame().pc);
215 _registers.cp(this, frame().reg_offset + r1, globals, i);
216 DBG_INTERPRETER("STORE_GLOBAL R" << r1 << "(" << reg(frame(), r1).toString(DBG_TRIM_OUTPUT)
217 << ")"
218 << " " << i << "\n");
219 } break;
220 case BytecodeStream::MOV: {
221 int r1 = frame().bs->reg(frame().pc);
222 int r2 = frame().bs->reg(frame().pc);
223 DBG_INTERPRETER("MOV R" << r1 << "(" << reg(frame(), r1).toString(DBG_TRIM_OUTPUT) << ")");
224 _registers.cp(this, frame().reg_offset + r1, frame().reg_offset + r2);
225 DBG_INTERPRETER(" R" << r2 << "(" << reg(frame(), r2).toString(DBG_TRIM_OUTPUT) << ")"
226 << "\n");
227 } break;
228 case BytecodeStream::JMP: {
229 int i = frame().bs->reg(frame().pc);
230 DBG_INTERPRETER("JMP " << i << "\n");
231 frame().pc = i;
232 } break;
233 case BytecodeStream::JMPIF: {
234 int r0 = frame().bs->reg(frame().pc);
235 int i = frame().bs->reg(frame().pc);
236 DBG_INTERPRETER("JMPIF R" << r0 << "(" << reg(frame(), r0).toString() << ")"
237 << " " << i << "\n");
238 if (reg(frame(), r0) != 0) {
239 frame().pc = i;
240 }
241 } break;
242 case BytecodeStream::JMPIFNOT: {
243 int r0 = frame().bs->reg(frame().pc);
244 int i = frame().bs->reg(frame().pc);
245 DBG_INTERPRETER("JMPIFNOT R" << r0 << "(" << reg(frame(), r0).toString() << ")"
246 << " " << i << "\n");
247 if (reg(frame(), r0) == 0) {
248 frame().pc = i;
249 }
250 } break;
251 case BytecodeStream::EQI: {
252 int r1 = frame().bs->reg(frame().pc);
253 int r2 = frame().bs->reg(frame().pc);
254 int r3 = frame().bs->reg(frame().pc);
255 DBG_INTERPRETER("EQI R" << r1 << "(" << reg(frame(), r1).toString() << ")"
256 << " R" << r2 << "(" << reg(frame(), r2).toString() << ")");
257 assert(reg(frame(), r1) == reg(frame(), r2) ||
258 reg(frame(), r1).toInt() != reg(frame(), r2).toInt());
259 assign(frame(), r3, reg(frame(), r1) == reg(frame(), r2));
260 DBG_INTERPRETER(" R" << r3 << "(" << reg(frame(), r3).toString() << ")"
261 << "\n");
262 } break;
263 case BytecodeStream::LTI: {
264 int r1 = frame().bs->reg(frame().pc);
265 int r2 = frame().bs->reg(frame().pc);
266 int r3 = frame().bs->reg(frame().pc);
267 DBG_INTERPRETER("LTI R" << r1 << "(" << reg(frame(), r1).toString() << ")"
268 << " R" << r2 << "(" << reg(frame(), r2).toString() << ")");
269 assign(frame(), r3, (reg(frame(), r1) < reg(frame(), r2)));
270 DBG_INTERPRETER(" R" << r3 << "(" << reg(frame(), r3).toString() << ")"
271 << "\n");
272 } break;
273 case BytecodeStream::LEI: {
274 int r1 = frame().bs->reg(frame().pc);
275 int r2 = frame().bs->reg(frame().pc);
276 int r3 = frame().bs->reg(frame().pc);
277 DBG_INTERPRETER("LEI R" << r1 << "(" << reg(frame(), r1).toString() << ")"
278 << " R" << r2 << "(" << reg(frame(), r2).toString() << ")");
279 assign(frame(), r3, (reg(frame(), r1) <= reg(frame(), r2)));
280 DBG_INTERPRETER(" R" << r3 << "(" << reg(frame(), r3).toString() << ")"
281 << "\n");
282 } break;
283 case BytecodeStream::AND: {
284 int r1 = frame().bs->reg(frame().pc);
285 int r2 = frame().bs->reg(frame().pc);
286 int r3 = frame().bs->reg(frame().pc);
287 DBG_INTERPRETER("AND R" << r1 << "(" << reg(frame(), r1).toString() << ")"
288 << " R" << r2 << "(" << reg(frame(), r2).toString() << ")");
289 assign(frame(), r3, (reg(frame(), r1) != 0 && reg(frame(), r2) != 0));
290 DBG_INTERPRETER(" " << r3 << "(" << reg(frame(), r3).toString() << ")"
291 << "\n");
292 } break;
293 case BytecodeStream::OR: {
294 int r1 = frame().bs->reg(frame().pc);
295 int r2 = frame().bs->reg(frame().pc);
296 int r3 = frame().bs->reg(frame().pc);
297 DBG_INTERPRETER("OR R" << r1 << "(" << reg(frame(), r1).toString() << ")"
298 << " R" << r2 << "(" << reg(frame(), r2).toString() << ")");
299 assign(frame(), r3, (reg(frame(), r1) != 0 || reg(frame(), r2) != 0));
300 DBG_INTERPRETER(" " << r3 << "(" << reg(frame(), r3).toString() << ")"
301 << "\n");
302 } break;
303 case BytecodeStream::NOT: {
304 int r1 = frame().bs->reg(frame().pc);
305 int r2 = frame().bs->reg(frame().pc);
306 DBG_INTERPRETER("NOT R" << r1);
307 assign(frame(), r2, (reg(frame(), r1) == 0));
308 DBG_INTERPRETER(" R" << r2 << "(" << reg(frame(), r2).toString() << ")"
309 << "\n");
310 } break;
311 case BytecodeStream::XOR: {
312 int r1 = frame().bs->reg(frame().pc);
313 int r2 = frame().bs->reg(frame().pc);
314 int r3 = frame().bs->reg(frame().pc);
315 DBG_INTERPRETER("XOR R" << r1 << "(" << reg(frame(), r1).toString() << ")"
316 << " R" << r2 << "(" << reg(frame(), r2).toString() << ")");
317 assign(frame(), r3, ((reg(frame(), r1) != 0) ^ (reg(frame(), r2) != 0)));
318 DBG_INTERPRETER(" R" << r3 << "(" << reg(frame(), r3).toString() << ")"
319 << "\n");
320 } break;
321 case BytecodeStream::ISPAR: {
322 int r1 = frame().bs->reg(frame().pc);
323 int r2 = frame().bs->reg(frame().pc);
324 DBG_INTERPRETER("ISPAR R" << r1 << "(" << reg(frame(), r1).toString(DBG_TRIM_OUTPUT)
325 << ")");
326 Val v = Val::follow_alias(reg(frame(), r1), this);
327 if (v.isInt()) {
328 assign(frame(), r2, 1);
329 } else if (v.isVar()) {
330 assign(frame(), r2, 0);
331 } else {
332 assert(v.isVec());
333 Val ret = v.toVec()->isPar();
334 assign(frame(), r2, ret);
335 }
336 DBG_INTERPRETER(" R" << r2 << "(" << reg(frame(), r2).toString() << ")"
337 << "\n");
338 } break;
339 case BytecodeStream::ISEMPTY: {
340 int r1 = frame().bs->reg(frame().pc);
341 int r2 = frame().bs->reg(frame().pc);
342 DBG_INTERPRETER("ISEMPTY R" << r1 << "(" << reg(frame(), r1).toString(DBG_TRIM_OUTPUT)
343 << ")");
344 assert(reg(frame(), r1).isInt() || reg(frame(), r1).isVec());
345 assign(frame(), r2, (reg(frame(), r1).isInt() || reg(frame(), r1).size() == 0));
346 DBG_INTERPRETER(" R" << r2 << "(" << reg(frame(), r2).toString() << ")"
347 << "\n");
348 } break;
349 case BytecodeStream::LENGTH: {
350 int r1 = frame().bs->reg(frame().pc);
351 int r2 = frame().bs->reg(frame().pc);
352 DBG_INTERPRETER("LENGTH R" << r1 << "(" << reg(frame(), r1).toString(DBG_TRIM_OUTPUT)
353 << ")");
354 assert(reg(frame(), r1).isVec());
355 if (!reg(frame(), r1).toVec()->hasIndexSet()) {
356 assign(frame(), r2, reg(frame(), r1).size());
357 } else {
358 assign(frame(), r2, reg(frame(), r1)[0].size());
359 }
360 DBG_INTERPRETER(" R" << r2 << "(" << reg(frame(), r2).toString() << ")"
361 << "\n");
362 } break;
363 case BytecodeStream::GET_VEC: {
364 int r1 = frame().bs->reg(frame().pc);
365 int r2 = frame().bs->reg(frame().pc);
366 int r3 = frame().bs->reg(frame().pc);
367 DBG_INTERPRETER("GET_VEC R" << r1 << "(" << reg(frame(), r1).toString(DBG_TRIM_OUTPUT)
368 << ")"
369 << " R" << r2 << "(" << reg(frame(), r2).toString() << ")");
370 assert(reg(frame(), r1).isVec());
371 assert(reg(frame(), r2).isInt());
372 assert(reg(frame(), r2) > 0 && reg(frame(), r2) <= reg(frame(), r1).size());
373 Val v = Val::follow_alias(reg(frame(), r1)[reg(frame(), r2).toInt() - 1], this);
374 assign(frame(), r3, v);
375 DBG_INTERPRETER(" R" << r3 << "(" << v.toString(DBG_TRIM_OUTPUT) << ")"
376 << "\n");
377 } break;
378 case BytecodeStream::GET_ARRAY: {
379 Val n = frame().bs->intval(frame().pc);
380 int r1 = frame().bs->reg(frame().pc);
381 DBG_INTERPRETER("GET_ARRAY " << n.toString() << " R" << r1 << "("
382 << reg(frame(), r1).toString(DBG_TRIM_OUTPUT) << ")");
383 std::vector<Val> idx(n.toInt());
384 for (int i = 0; i < n; i++) {
385 int rr = frame().bs->reg(frame().pc);
386 DBG_INTERPRETER(" R" << rr << "(" << reg(frame(), rr).toString(DBG_TRIM_OUTPUT) << ")");
387 idx[i] = reg(frame(), rr);
388 }
389 int r_res = frame().bs->reg(frame().pc);
390 int r_cond = frame().bs->reg(frame().pc);
391 assert(reg(frame(), r1).isVec());
392
393 bool success = true;
394 Val v = Val(-2000);
395
396 Val content = reg(frame(), r1).toVec()->raw_data();
397 if (reg(frame(), r1).toVec()->hasIndexSet()) {
398 // N-Dimensional array representation
399 Val index_set = reg(frame(), r1).toVec()->index_set();
400 std::vector<std::pair<Val, Val>> dimensions;
401 Val realdim = 1;
402 for (int i = 0; i < index_set.size(); i += 2) {
403 Val a = index_set[i];
404 Val b = index_set[i + 1];
405 dimensions.emplace_back(a, b);
406 realdim *= b - a + 1;
407 }
408
409 Val realidx = 0;
410 for (int i = 0; i < idx.size(); i++) {
411 Val ix = idx[i];
412 if (ix < dimensions[i].first || ix > dimensions[i].second) {
413 success = false;
414 break;
415 }
416 realdim /= dimensions[i].second - dimensions[i].first + 1;
417 realidx += (ix - dimensions[i].first) * realdim;
418 }
419 assert(realidx >= 0 && realidx < content.size());
420
421 if (success) {
422 v = Val::follow_alias(content[realidx.toInt()], this);
423 }
424 } else {
425 // Compact array representation (index set 1..n)
426 success = 1 <= idx[0] && idx[0] <= reg(frame(), r1).size();
427 if (success) {
428 v = Val::follow_alias(content[idx[0].toInt() - 1], this);
429 }
430 }
431
432 assign(frame(), r_res, v);
433 assign(frame(), r_cond, Val(success));
434 DBG_INTERPRETER(" R" << r_res << "(" << v.toString(DBG_TRIM_OUTPUT) << ") R" << r_cond
435 << "(" << Val(success).toString(DBG_TRIM_OUTPUT) << ")"
436 << "\n");
437 } break;
438 case BytecodeStream::LB: {
439 int r1 = frame().bs->reg(frame().pc);
440 int r2 = frame().bs->reg(frame().pc);
441 DBG_INTERPRETER("LB R" << r1 << "(" << reg(frame(), r1).toString(DBG_TRIM_OUTPUT) << ")");
442 Val v = Val::follow_alias(reg(frame(), r1), this);
443 assign(frame(), r2, v.lb());
444 DBG_INTERPRETER(" R" << r2 << "(" << reg(frame(), r2).toString(DBG_TRIM_OUTPUT) << ")"
445 << "\n");
446 } break;
447 case BytecodeStream::UB: {
448 int r1 = frame().bs->reg(frame().pc);
449 int r2 = frame().bs->reg(frame().pc);
450 DBG_INTERPRETER("UB R" << r1 << "(" << reg(frame(), r1).toString(DBG_TRIM_OUTPUT) << ")");
451 Val v = Val::follow_alias(reg(frame(), r1), this);
452 assign(frame(), r2, v.ub());
453 DBG_INTERPRETER(" R" << r2 << "(" << reg(frame(), r2).toString(DBG_TRIM_OUTPUT) << ")"
454 << "\n");
455 } break;
456 case BytecodeStream::DOM: {
457 int r1 = frame().bs->reg(frame().pc);
458 int r2 = frame().bs->reg(frame().pc);
459 DBG_INTERPRETER("DOM R" << r1 << "(" << reg(frame(), r1).toString(DBG_TRIM_OUTPUT) << ")");
460 Val v = Val::follow_alias(reg(frame(), r1), this);
461 if (v.isInt()) {
462 assign(frame(), r2, Val(Vec::a(this, newIdent(), {v, v})));
463 } else if (v.isVar()) {
464 Variable* var = v.toVar();
465 assign(frame(), r2, Val(var->domain()));
466 } else {
467 throw Error("Error: dom on invalid type");
468 }
469 DBG_INTERPRETER(" R" << r2 << "(" << reg(frame(), r2).toString(DBG_TRIM_OUTPUT) << ")"
470 << "\n");
471 } break;
472 case BytecodeStream::MAKE_SET: {
473 int r1 = frame().bs->reg(frame().pc);
474 int r2 = frame().bs->reg(frame().pc);
475 DBG_INTERPRETER("MAKE_SET R" << r1 << "(" << reg(frame(), r1).toString(DBG_TRIM_OUTPUT)
476 << ")");
477 Val v1 = Val::follow_alias(reg(frame(), r1), this);
478 assert(reg(frame(), r1).isVec());
479 Vec* a1 = v1.toVec();
480
481 std::vector<Val> result;
482 if (a1->size() > 0) {
483 std::vector<Val> vals(a1->size());
484 for (int i = 0; i < a1->size(); i++) vals[i] = (*a1)[i];
485
486 std::sort(vals.begin(), vals.end());
487 Val l(vals[0]);
488 Val u(vals[0]);
489 for (int i = 1; i < vals.size(); ++i) {
490 if (u + 1 < vals[i]) {
491 result.emplace_back(l);
492 result.emplace_back(u);
493 l = vals[i];
494 }
495 u = vals[i];
496 }
497 result.emplace_back(l);
498 result.emplace_back(u);
499 }
500 Val result_val(Vec::a(this, newIdent(), result));
501 assign(frame(), r2, result_val);
502 DBG_INTERPRETER(" R" << r2 << "(" << result_val.toString(DBG_TRIM_OUTPUT) << ")"
503 << "\n");
504 } break;
505 case BytecodeStream::INTERSECTION: {
506 int r1 = frame().bs->reg(frame().pc);
507 int r2 = frame().bs->reg(frame().pc);
508 int r3 = frame().bs->reg(frame().pc);
509 DBG_INTERPRETER("INTERSECTION R" << r1 << "(" << reg(frame(), r1).toString(DBG_TRIM_OUTPUT)
510 << ") R" << r2 << "("
511 << reg(frame(), r2).toString(DBG_TRIM_OUTPUT) << ")");
512 Val v1 = Val::follow_alias(reg(frame(), r1), this);
513 Val v2 = Val::follow_alias(reg(frame(), r2), this);
514 Val result_val;
515 if (v1.isInt()) {
516 result_val = v2;
517 } else if (v2.isInt()) {
518 result_val = v1;
519 } else {
520 Vec* s1 = v1.toVec();
521 Vec* s2 = v2.toVec();
522 VecSetRanges vsr1(s1);
523 VecSetRanges vsr2(s2);
524 Ranges::Inter<Val, VecSetRanges, VecSetRanges> inter(vsr1, vsr2);
525 std::vector<Val> result;
526 for (; inter(); ++inter) {
527 result.emplace_back(inter.min());
528 result.emplace_back(inter.max());
529 }
530 result_val = Val(Vec::a(this, newIdent(), result));
531 }
532 assign(frame(), r3, result_val);
533 DBG_INTERPRETER(" R" << r3 << "(" << result_val.toString(DBG_TRIM_OUTPUT) << ")"
534 << "\n");
535 } break;
536 case BytecodeStream::UNION: {
537 int r1 = frame().bs->reg(frame().pc);
538 int r2 = frame().bs->reg(frame().pc);
539 int r3 = frame().bs->reg(frame().pc);
540 DBG_INTERPRETER("UNION R" << r1 << "(" << reg(frame(), r1).toString(DBG_TRIM_OUTPUT)
541 << ") R" << r2 << "("
542 << reg(frame(), r2).toString(DBG_TRIM_OUTPUT) << ")");
543 Val v1 = Val::follow_alias(reg(frame(), r1), this);
544 Val v2 = Val::follow_alias(reg(frame(), r2), this);
545 Val result_val;
546 if (v1.isInt()) {
547 result_val = v1;
548 } else if (v2.isInt()) {
549 result_val = v2;
550 } else {
551 Vec* s1 = v1.toVec();
552 Vec* s2 = v2.toVec();
553 VecSetRanges vsr1(s1);
554 VecSetRanges vsr2(s2);
555 Ranges::Union<Val, VecSetRanges, VecSetRanges> union_r(vsr1, vsr2);
556 std::vector<Val> result;
557 for (; union_r(); ++union_r) {
558 result.emplace_back(union_r.min());
559 result.emplace_back(union_r.max());
560 }
561 result_val = Val(Vec::a(this, newIdent(), result));
562 }
563 assign(frame(), r3, result_val);
564 DBG_INTERPRETER(" R" << r3 << "(" << result_val.toString(DBG_TRIM_OUTPUT) << ")"
565 << "\n");
566 } break;
567 case BytecodeStream::DIFF: {
568 int r1 = frame().bs->reg(frame().pc);
569 int r2 = frame().bs->reg(frame().pc);
570 int r3 = frame().bs->reg(frame().pc);
571 DBG_INTERPRETER("DIFF R" << r1 << "(" << reg(frame(), r1).toString(DBG_TRIM_OUTPUT) << ") R"
572 << r2 << "(" << reg(frame(), r2).toString(DBG_TRIM_OUTPUT) << ")");
573 Val v1 = Val::follow_alias(reg(frame(), r1), this);
574 Val v2 = Val::follow_alias(reg(frame(), r2), this);
575 Val result_val;
576 Vec* s1 = v1.toVec();
577 Vec* s2 = v2.toVec();
578 VecSetRanges vsr1(s1);
579 VecSetRanges vsr2(s2);
580 Ranges::Diff<Val, VecSetRanges, VecSetRanges> diff_r(vsr1, vsr2);
581 std::vector<Val> result;
582 for (; diff_r(); ++diff_r) {
583 result.emplace_back(diff_r.min());
584 result.emplace_back(diff_r.max());
585 }
586 result_val = Val(Vec::a(this, newIdent(), result));
587 assign(frame(), r3, result_val);
588 DBG_INTERPRETER(" R" << r3 << "(" << result_val.toString(DBG_TRIM_OUTPUT) << ")"
589 << "\n");
590 } break;
591 case BytecodeStream::INTERSECT_DOMAIN: {
592 int r1 = frame().bs->reg(frame().pc);
593 int r2 = frame().bs->reg(frame().pc);
594 int r3 = frame().bs->reg(frame().pc);
595 DBG_INTERPRETER("INTERSECT_DOMAIN R"
596 << r1 << "(" << reg(frame(), r1).toString(DBG_TRIM_OUTPUT) << ") R" << r2
597 << "(" << reg(frame(), r2).toString(DBG_TRIM_OUTPUT) << ")");
598 Val v1 = Val::follow_alias(reg(frame(), r1), this);
599 Val v2 = reg(frame(), r2);
600 assert(v2.isVec());
601
602 Val result_val;
603 Vec* s2 = v2.toVec();
604 if (v1.isVar()) {
605 Vec* s1 = v1.toVar()->domain();
606 VecSetRanges vsr1(s1);
607 VecSetRanges vsr2(s2);
608 Ranges::Inter<Val, VecSetRanges, VecSetRanges> inter(vsr1, vsr2);
609 std::vector<Val> result;
610 for (; inter(); ++inter) {
611 result.emplace_back(inter.min());
612 result.emplace_back(inter.max());
613 }
614 if (result.empty()) {
615 _status = INCONSISTENT;
616 // Invariant: Last instruction in the frame is always an ABORT instruction
617 frame().pc = frame().bs->size() - 1;
618 break;
619 }
620 v1.toVar()->domain(this, result, true);
621 Val v1a = Val::follow_alias(v1);
622 if (v1a.isVar()) {
623 result_val = Val(v1a.toVar()->domain());
624 } else {
625 result_val = Val(Vec::a(this, newIdent(), {v1a, v1a}));
626 }
627 } else {
628 Ranges::Const<Val> vsr1(v1, v1);
629 VecSetRanges vsr2(s2);
630 if (Ranges::subset(vsr1, vsr2)) {
631 result_val = Val(Vec::a(this, newIdent(), {v1, v1}));
632 } else {
633 _status = INCONSISTENT;
634 // Invariant: Last instruction in the frame is always an ABORT instruction
635 frame().pc = frame().bs->size() - 1;
636 break;
637 }
638 }
639 assign(frame(), r3, result_val);
640 DBG_INTERPRETER(" R" << r3 << "(" << result_val.toString(DBG_TRIM_OUTPUT) << ")"
641 << "\n");
642 } break;
643 case BytecodeStream::RET: {
644 DBG_INTERPRETER("RET");
645 if (frame().cse_frame_depth < _cse_stack.size()) {
646 CSEFrame& info = _cse_stack.back();
647 DBG_INTERPRETER(" %-- " << info.proc << " (" << _procs[info.proc].name << ") "
648 << BytecodeProc::mode_to_string[info.mode]);
649 }
650 DBG_INTERPRETER("\n");
651 assert(!_stack.empty());
652 execute_ret:
653 if (_stack.size() == 1) {
654 // Always leave final frame on the stack
655 // Copy remaining constraints into toplevel
656 assert(_agg.size() == 1);
657 for (Constraint* c : _agg[0].constraints) {
658 root()->addDefinition(this, c);
659 }
660 _agg[0].constraints.clear();
661 return;
662 }
663
664 DBG_CALLTRACE("<");
665 for (size_t i = 0; i < _stack.size() - 1; ++i) {
666 DBG_CALLTRACE("--");
667 }
668 DBG_CALLTRACE(" " << (_stack.back()._mode == BytecodeProc::ROOT ||
669 _stack.back()._mode == BytecodeProc::ROOT_NEG
670 ? "POSTED"
671 : (_cse_stack.back().stack_size == _agg.back().size() - 1
672 ? _agg[_agg.size() - 1].back().toString(DBG_TRIM_OUTPUT)
673 : ""))
674 << "\n");
675
676 while (_cse_stack.size() > frame().cse_frame_depth) {
677 CSEFrame& entry = _cse_stack.back();
678 int nargs = _procs[entry.proc].nargs;
679 if (entry.mode == BytecodeProc::ROOT || entry.mode == BytecodeProc::ROOT_NEG) {
680 Val v = Val(1);
681 cse_insert(entry.proc, entry.getKey(), entry.mode, v);
682 } else if (entry.stack_size == _agg.back().size() - 1) {
683 Val ret = _agg[_agg.size() - 1].back();
684 cse_insert(entry.proc, entry.getKey(), entry.mode, ret);
685 } else {
686 entry.destroy(*this);
687 }
688 _cse_stack.pop_back();
689 }
690
691 _registers.resize(this, frame().reg_offset);
692 _stack.pop_back();
693 } break;
694 case BytecodeStream::CALL: {
695 char mode_c = frame().bs->chr(frame().pc);
696 int code = frame().bs->reg(frame().pc);
697 bool cse = frame().bs->chr(frame().pc);
698 assert(code >= 0);
699 assert(code < _procs.size());
700 assert(mode_c >= 0);
701 assert(mode_c <= BytecodeProc::MAX_MODE);
702 auto mode = static_cast<BytecodeProc::Mode>(mode_c);
703 int n = _procs[code].nargs;
704 DBG_INTERPRETER("CALL " << BytecodeProc::mode_to_string[mode] << " " << code << "("
705 << _procs[code].name << ")" << (cse ? "" : " no_cse"));
706 for (size_t i = 0; i < _stack.size(); ++i) {
707 DBG_CALLTRACE("--");
708 }
709 DBG_CALLTRACE("> " << _procs[code].name << "(");
710
711 // Allocate new frame on the stack
712 _stack.emplace_back(_procs[code].mode[mode], code, mode);
713 frame().reg_offset = _registers.size();
714 _registers.resize(this, frame().reg_offset + frame().bs->maxRegister() + 1);
715 // Copy arguments
716 for (int i = 0; i < n; i++) {
717 int r = _stack[_stack.size() - 2].bs->reg(_stack[_stack.size() - 2].pc);
718 assign(frame(), i, reg(_stack[_stack.size() - 2], r));
719 DBG_INTERPRETER(" R" << r << "(" << reg(frame(), i).toString(DBG_TRIM_OUTPUT) << ")"
720 << ((i + 1 < n) ? "" : "\n"));
721 DBG_CALLTRACE(reg(frame(), i).toString(DBG_TRIM_OUTPUT) << ((i + 1 < n) ? ", " : ")\n"));
722 }
723
724 auto immediate_return = [&] {
725 _registers.resize(this, frame().reg_offset);
726 _stack.pop_back();
727 };
728
729 // Lookup for Common Subexpression Elimination
730 size_t cse_depth = _cse_stack.size();
731 if (cse) {
732 _cse_stack.emplace_back(*this, code, mode, _registers.iter_n(frame().reg_offset),
733 _registers.iter_n(frame().reg_offset + n), n, _agg.back().size());
734 // Lookup item in CSE
735 auto lookup = cse_find(code, _cse_stack.back().getKey(), mode);
736 if (lookup.second) {
737 _cse_stack.back().destroy(*this);
738 _cse_stack.pop_back();
739 if (mode == BytecodeProc::ROOT || mode == BytecodeProc::ROOT_NEG) {
740 assert(lookup.first.isInt());
741 if (lookup.first.toInt() != 1) {
742 _status = INCONSISTENT;
743 // Invariant: Last instruction in the frame is always an ABORT instruction
744 frame().pc = frame().bs->size() - 1;
745 }
746 } else {
747 pushAgg(lookup.first, -1);
748 }
749 immediate_return();
750 break;
751 }
752 }
753
754 if (_procs[code].mode[mode].size() == 0 || _procs[code].delay) {
755 DBG_INTERPRETER((_procs[code].delay ? "--- Delayed CALL\n" : "--- FZN Builtin\n"));
756 DBG_CALLTRACE("<");
757 for (size_t i = 0; i < _stack.size(); ++i) {
758 DBG_CALLTRACE("--");
759 }
760 // this is a FlatZinc builtin
761 if (code == PrimitiveMap::MK_INTVAR) {
762 assert(mode == BytecodeProc::ROOT);
763 Variable* v = Variable::a(this, _registers[frame().reg_offset], true, newIdent());
764 pushAgg(Val(v), -1);
765 DBG_CALLTRACE(" " << Val(v).toString() << "\n");
766 } else {
767 assert(mode == BytecodeProc::ROOT || mode == BytecodeProc::ROOT_NEG);
768 auto c = Constraint::a(this, code, mode, _registers.iter_n(frame().reg_offset),
769 _registers.iter_n(frame().reg_offset + n), n);
770 if (!(c.first || c.second)) {
771 // Propagation failed
772 _status = INCONSISTENT;
773 // Invariant: Last instruction in the frame is always an ABORT instruction
774 frame().pc = frame().bs->size() - 1;
775 break;
776 }
777 if (c.first) {
778 pushConstraint(c.first);
779 }
780 if (cse) {
781 Val ret(c.second);
782 cse_insert(code, _cse_stack.back().getKey(), mode, ret);
783 _cse_stack.pop_back();
784 }
785 DBG_CALLTRACE(" POSTED\n");
786 /// TODO: delayed calls
787 // if (_procs[code].delay) {
788 // delayed_calls.push_back(c);
789 // }
790 }
791 immediate_return();
792 }
793 } break;
794 case BytecodeStream::BUILTIN: {
795 int code = frame().bs->reg(frame().pc);
796 assert(code >= 0);
797 DBG_INTERPRETER("BUILTIN " << code << "(" << _procs[code].name << ")");
798 assert(code < primitiveMap().size());
799 // this is a Interpreter builtin
800 int n = _procs[code].nargs;
801 std::vector<Val> args(n);
802 for (int i = 0; i < n; i++) {
803 int r = frame().bs->reg(frame().pc);
804 // Do not increase the reference count. Vector is destroyed after
805 // BUILTIN execution without cleanup
806 args[i] = reg(frame(), r);
807 DBG_INTERPRETER(" R" << r << "(" << args[i].toString(DBG_TRIM_OUTPUT) << ")");
808 }
809 DBG_INTERPRETER("\n");
810 primitiveMap()[code]->execute(*this, args);
811 } break;
812 case BytecodeStream::TCALL: {
813 char mode_c = frame().bs->chr(frame().pc);
814 int code = frame().bs->reg(frame().pc);
815 bool cse = frame().bs->chr(frame().pc);
816 assert(code >= 0);
817 assert(code < _procs.size());
818 assert(mode_c >= 0);
819 assert(mode_c <= BytecodeProc::MAX_MODE);
820 auto mode = static_cast<BytecodeProc::Mode>(mode_c);
821 DBG_INTERPRETER("TCALL " << BytecodeProc::mode_to_string[mode] << " " << code << "("
822 << _procs[code].name << ")" << (cse ? "" : " no_cse") << "\n");
823 for (size_t i = 0; i < _stack.size() - 1; ++i) {
824 DBG_CALLTRACE("==");
825 }
826 DBG_CALLTRACE("> " << _procs[code].name << "(");
827 int nargs = _procs[code].nargs;
828 for (int i = 0; i < nargs; ++i) {
829 DBG_CALLTRACE(reg(frame(), i).toString(DBG_TRIM_OUTPUT)
830 << ((i + 1 < nargs) ? ", " : ")\n"));
831 }
832
833 if (cse) {
834 _cse_stack.emplace_back(*this, code, mode, _registers.iter_n(frame().reg_offset),
835 _registers.iter_n(frame().reg_offset + nargs), nargs,
836 _agg.back().size());
837 bool found;
838 Val ret;
839 std::tie(ret, found) = cse_find(code, _cse_stack.back().getKey(), mode);
840 if (found) {
841 _cse_stack.back().destroy(*this);
842 _cse_stack.pop_back();
843 // RET with CSE found value
844 if (mode == BytecodeProc::ROOT || mode == BytecodeProc::ROOT_NEG) {
845 assert(ret.isInt());
846 if (ret.toInt() != 1) {
847 _status = INCONSISTENT;
848 // Invariant: Last instruction in the frame is always an ABORT instruction
849 frame().pc = frame().bs->size() - 1;
850 }
851 } else {
852 pushAgg(ret, -1);
853 }
854 // TODO: Does this actually "return" correctly?? It seems the code would continue;
855 while (_cse_stack.size() > frame().cse_frame_depth) {
856 CSEFrame& entry = _cse_stack.back();
857 int nargs = _procs[entry.proc].nargs;
858 cse_insert(entry.proc, entry.getKey(), entry.mode, ret);
859 _cse_stack.pop_back();
860 }
861 _registers.resize(this, frame().reg_offset);
862 _stack.pop_back();
863 break;
864 }
865 }
866 if (_procs[code].mode[mode].size() == 0 || _procs[code].delay) {
867 DBG_INTERPRETER((_procs[code].delay ? "--- Delayed CALL\n" : "--- FZN Builtin\n"));
868 // this is a FlatZinc builtin
869 assert(mode == BytecodeProc::ROOT || mode == BytecodeProc::ROOT_NEG);
870 auto c = Constraint::a(this, code, mode, _registers.iter_n(frame().reg_offset),
871 _registers.iter_n(frame().reg_offset + nargs), nargs);
872 if (!(c.first || c.second)) {
873 // Propagation failed
874 _status = INCONSISTENT;
875 // Invariant: Last instruction in the frame is always an ABORT instruction
876 frame().pc = frame().bs->size() - 1;
877 break;
878 }
879 if (c.first) {
880 pushConstraint(c.first);
881 }
882 if (cse) {
883 Val ret(c.second);
884 // TODO: Does this actually "return" correctly?? It seems this would not set all
885 // necessary values in the _cse_stack
886 cse_insert(code, _cse_stack.back().getKey(), mode, ret);
887 _cse_stack.pop_back();
888 }
889 /// TODO: delayed calls
890 // if (_procs[code].delay) {
891 // delayed_calls.push_back(def);
892 // }
893 goto execute_ret;
894 } else {
895 // Replace frame with new procedure
896 frame()._pred = code;
897 frame()._mode = mode;
898 frame().bs = &_procs[code].mode[mode];
899 _registers.resize(this, frame().reg_offset + frame().bs->maxRegister() + 1);
900 frame().pc = 0;
901 }
902 } break;
903 case BytecodeStream::ITER_ARRAY: {
904 int r1 = frame().bs->reg(frame().pc);
905 int l = frame().bs->reg(frame().pc);
906 DBG_INTERPRETER("ITER_ARRAY " << r1 << " " << l << "\n");
907 assert(reg(frame(), r1).isVec());
908 if (reg(frame(), r1).toVec()->hasIndexSet()) {
909 assert(reg(frame(), r1).size() == 2);
910 assert(reg(frame(), r1)[0].isVec());
911
912 Vec* v(reg(frame(), r1)[0].toVec());
913 _loops.push_back(LoopState(v, l));
914 } else {
915 // Compact array representation (index set 1..n)
916 Vec* v(reg(frame(), r1).toVec());
917 _loops.push_back(LoopState(v, l));
918 }
919 } break;
920 case BytecodeStream::ITER_VEC: {
921 int r1 = frame().bs->reg(frame().pc);
922 int l = frame().bs->reg(frame().pc);
923 DBG_INTERPRETER("ITER_VEC " << r1 << " " << l << "\n");
924 assert(reg(frame(), r1).isVec());
925 Vec* v(reg(frame(), r1).toVec());
926 _loops.push_back(LoopState(v, l));
927 } break;
928 case BytecodeStream::ITER_RANGE: {
929 int r1 = frame().bs->reg(frame().pc);
930 int r2 = frame().bs->reg(frame().pc);
931 int lbl = frame().bs->reg(frame().pc);
932
933 Val lb = Val::follow_alias(reg(frame(), r1), this);
934 Val ub = Val::follow_alias(reg(frame(), r2), this);
935 assert(lb.isInt());
936 assert(ub.isInt());
937 DBG_INTERPRETER("ITER_RANGE " << r1 << " " << r2 << " " << lbl << "\n");
938 _loops.push_back(LoopState(lb.toInt(), ub.toInt(), lbl));
939 } break;
940 case BytecodeStream::ITER_NEXT: {
941 int r1 = frame().bs->reg(frame().pc);
942 DBG_INTERPRETER("ITER_NEXT");
943 assert(_loops.size() > 0);
944 LoopState& outer(_loops.back());
945 if (outer.pos < outer.end) {
946 Val v;
947 if (outer.is_range) {
948 v = outer.pos;
949 outer.pos++;
950 } else {
951 Val* ptr(reinterpret_cast<Val*>(outer.pos));
952 v = Val::follow_alias(*ptr);
953 outer.pos += sizeof(Val*);
954 }
955 assign(frame(), r1, v);
956 DBG_INTERPRETER(" R" << r1 << "(" << v.toString(DBG_TRIM_OUTPUT) << ")"
957 << "\n");
958 } else {
959 frame().pc = outer.exit_pc;
960 _loops.pop_back();
961 DBG_INTERPRETER(" (EXIT " << outer.exit_pc << ")\n");
962 }
963 } break;
964 case BytecodeStream::ITER_BREAK: {
965 int num = frame().bs->intval(frame().pc).toInt();
966 DBG_INTERPRETER("ITER_BREAK " << num << "\n");
967 assert(_loops.size() >= num);
968 auto it(_loops.end() - num);
969 frame().pc = it->exit_pc;
970 _loops.erase(it, _loops.end());
971 } break;
972 case BytecodeStream::TRACE: {
973 int r = frame().bs->reg(frame().pc);
974 DBG_INTERPRETER("TRACE " << r << "\n");
975 std::cerr << reg(frame(), r).toString() << "\n";
976 // std::cerr << frame().reg.e(r)->cast<StringLit>();
977 // std::cerr << frame()().reg.e(r) << "\n";
978 } break;
979 case BytecodeStream::ABORT: {
980 DBG_INTERPRETER("ABORT\n");
981
982 _registers.resize(this, 0);
983 _stack.clear();
984 // TODO: Should the Aggregation stack be emptied?
985
986 if (_status == ROGER) {
987 _status = ABORTED;
988 }
989 return;
990 }
991 case BytecodeStream::PUSH: {
992 int r = frame().bs->reg(frame().pc);
993 DBG_INTERPRETER("PUSH R" << r << " (" << reg(frame(), r).toString(DBG_TRIM_OUTPUT)
994 << ")\n");
995 assert(!_agg.empty());
996 _agg.back().push(this, reg(frame(), r));
997 } break;
998 case BytecodeStream::POP: {
999 int r = frame().bs->reg(frame().pc);
1000 assert(!_agg.empty());
1001 assert(!_agg.back().empty());
1002 assign(frame(), r, _agg.back().back());
1003 DBG_INTERPRETER("POP R" << r << " (" << reg(frame(), r).toString(DBG_TRIM_OUTPUT) << ")\n");
1004 _agg.back().pop(this);
1005 } break;
1006 case BytecodeStream::POST: {
1007 int r = frame().bs->reg(frame().pc);
1008 DBG_INTERPRETER("POST R" << r << " (" << reg(frame(), r).toString(DBG_TRIM_OUTPUT)
1009 << ")\n");
1010 Val v1 = Val::follow_alias(reg(frame(), r), this);
1011 if (v1.isInt()) {
1012 if (v1 == 0) {
1013 _status = INCONSISTENT;
1014 // Invariant: Last instruction in the frame is always an ABORT instruction
1015 frame().pc = frame().bs->size() - 1;
1016 }
1017 } else {
1018 bool success = v1.toVar()->setVal(this, 1);
1019 if (!success) {
1020 _status = INCONSISTENT;
1021 // Invariant: Last instruction in the frame is always an ABORT instruction
1022 frame().pc = frame().bs->size() - 1;
1023 }
1024 /// TODO: check why this is adding a ref
1025 /// Shouldn't be necessary
1026 // v1.toVar()->addRef(this);
1027 }
1028 } break;
1029 case BytecodeStream::OPEN_AGGREGATION: {
1030 int r = frame().bs->chr(frame().pc);
1031 DBG_INTERPRETER("OPEN_AGGREGATION " << AggregationCtx::symbol_to_string[r] << ", depth "
1032 << _agg.size() + 1 << "\n");
1033 assert(r >= 0 && r <= AggregationCtx::VCTX_OTHER);
1034 if (r == AggregationCtx::VCTX_OTHER || r == AggregationCtx::VCTX_VEC || _agg.empty() ||
1035 _agg.back().symbol != r) {
1036 // Push a new aggregation context
1037 _agg.emplace_back(this, r);
1038 } else {
1039 // Increment depth counter for current aggregation context
1040 _agg.back().n_symbols++;
1041 }
1042 } break;
1043 case BytecodeStream::SIMPLIFY_LIN: {
1044 DBG_INTERPRETER("SIMPLIFY_LIN");
1045
1046 int r0 = frame().bs->reg(frame().pc);
1047 int r1 = frame().bs->reg(frame().pc);
1048 Val i = frame().bs->intval(frame().pc);
1049 DBG_INTERPRETER(" R" << r0 << "(" << reg(frame(), r0).toString(DBG_TRIM_OUTPUT) << ")");
1050 DBG_INTERPRETER(" R" << r1 << "(" << reg(frame(), r1).toString(DBG_TRIM_OUTPUT) << ")");
1051 DBG_INTERPRETER(" " << i.toString());
1052 int r2 = frame().bs->reg(frame().pc);
1053 int r3 = frame().bs->reg(frame().pc);
1054 int r4 = frame().bs->reg(frame().pc);
1055
1056 std::vector<Val> coeffs({1, -1});
1057 std::vector<Val> vars({reg(frame(), r0), reg(frame(), r1)});
1058 Val d = i;
1059
1060 simplify_linexp(coeffs, vars, d);
1061
1062 Val coeffs_v = Val(Vec::a(this, newIdent(), coeffs));
1063 Val vars_v = Val(Vec::a(this, newIdent(), vars));
1064 assign(frame(), r2, coeffs_v);
1065 assign(frame(), r3, vars_v);
1066 assign(frame(), r4, -d);
1067 DBG_INTERPRETER(" R" << r2 << "(" << reg(frame(), r2).toString(DBG_TRIM_OUTPUT) << ")");
1068 DBG_INTERPRETER(" R" << r3 << "(" << reg(frame(), r3).toString(DBG_TRIM_OUTPUT) << ")\n");
1069 DBG_INTERPRETER(" R" << r4 << "(" << reg(frame(), r4).toString(DBG_TRIM_OUTPUT) << ")\n");
1070 } break;
1071 case BytecodeStream::CLOSE_AGGREGATION: {
1072 DBG_INTERPRETER("CLOSE_AGGREGATION ("
1073 << AggregationCtx::symbol_to_string[_agg.back().symbol] << ", depth "
1074 << _agg.size() << ")\n");
1075 assert(!_agg.empty());
1076 // Decrement depth counter for current aggregation context
1077 _agg.back().n_symbols--;
1078 if (_agg.back().n_symbols == 0) {
1079 // Result produced by this aggregation
1080 Variable* result = nullptr;
1081
1082 assert(_agg.size() >= 2);
1083 switch (_agg.back().symbol) {
1084 case AggregationCtx::VCTX_AND: {
1085 // Create a conjunction on the definition stack
1086 std::vector<Val> args;
1087 args.reserve(_agg.back().size());
1088 bool isFalse = false;
1089 for (int i = 0; i < _agg.back().size(); i++) {
1090 const Val& v = _agg.back()[i];
1091 if (v.isInt()) {
1092 if (v == 0) {
1093 // Disjunction is constant false
1094 isFalse = true;
1095 break;
1096 }
1097 } else {
1098 args.push_back(v);
1099 }
1100 }
1101 if (isFalse || args.empty()) {
1102 /// TODO: check, what if _agg.size()==2 as below?
1103 // Conjunction is constant true or false
1104 pushAgg(!isFalse, -2);
1105 } else if (_agg.size() == 2) {
1106 // Push into root context
1107 for (Val v : args) {
1108 auto success = v.toVar()->setVal(this, 1);
1109 // FIXME: Deal with unsuccessful setVal
1110 assert(success);
1111 }
1112 pushAgg(1, -2);
1113
1114 // Why do we need a definition? If this is in ROOT, then all arguments should be
1115 // true
1116 /* Definition* d =
1117 * Definition::a(this,boolean_domain(),false,PrimitiveMap::FORALL,BytecodeProc::ROOT,
1118 */
1119 /* {Val(Vec::a(this,newIdent(),args))},-1); */
1120 /* if (defs) { */
1121 /* d->appendBefore(this, defs); */
1122 /* } else { */
1123 /* defs = d; */
1124 /* } */
1125 } else if (args.size() == 1) {
1126 pushAgg(args[0], -2);
1127 } else {
1128 Vec* arr = Vec::a(this, newIdent(), args);
1129 result = Variable::a(this, boolean_domain(), false, newIdent());
1130 auto def_c = Constraint::a(this, PrimitiveMap::FORALL, BytecodeProc::ROOT,
1131 {Val(arr), Val(result)});
1132 assert(def_c.first);
1133 result->addRef(this);
1134 result->addDefinition(this, def_c.first);
1135 pushAgg(Val(result), -2);
1136 RefCountedObject::rmRef(this, result);
1137 }
1138 } break;
1139 case AggregationCtx::VCTX_OR: {
1140 // Create a clause on the definition stack, and push a reference
1141 // to it onto the aggregation stack
1142 std::vector<Val> pos;
1143 std::vector<Val> neg;
1144 bool isTrue = false;
1145 for (int i = 0; i < _agg.back().size(); i++) {
1146 const Val& v = Val::follow_alias(_agg.back()[i]);
1147 if (v.isInt()) {
1148 if (v != 0) {
1149 // Disjunction is constant true
1150 isTrue = true;
1151 break;
1152 }
1153 } else {
1154 Variable* cur = v.toVar();
1155 if (Constraint* defby = cur->defined_by()) {
1156 if (defby->pred() == PrimitiveMap::BOOLNOT) {
1157 if (Val::follow_alias(defby->arg(0)) == v) {
1158 neg.push_back(Val::follow_alias(defby->arg(1)));
1159 } else {
1160 neg.push_back(Val::follow_alias(defby->arg(0)));
1161 }
1162 continue;
1163 }
1164 }
1165 pos.push_back(v);
1166 }
1167 }
1168 if (isTrue || (pos.empty() && neg.empty())) {
1169 // Disjunction is constant true or false
1170 pushAgg(isTrue, -2);
1171 } else if (pos.size() == 1 && neg.empty()) {
1172 if (_agg.size() == 2) {
1173 auto success = pos[0].toVar()->setVal(this, 1);
1174 // FIXME: Deal with unsuccessful setVal
1175 assert(success);
1176 pushAgg(1, -2);
1177 } else {
1178 pushAgg(pos[0], -2);
1179 }
1180 } else {
1181 // Push into root context
1182 Vec* vpos = Vec::a(this, newIdent(), pos);
1183 Vec* vneg = Vec::a(this, newIdent(), neg);
1184 if (_agg.size() == 2) {
1185 auto c = Constraint::a(this, PrimitiveMap::CLAUSE, BytecodeProc::ROOT,
1186 {Val(vpos), Val(vneg)}, 0, 1, true);
1187 assert(c.first);
1188 root()->addDefinition(this, c.first);
1189 pushAgg(1, -2);
1190 } else {
1191 result = Variable::a(this, boolean_domain(), false, newIdent());
1192 auto def_c = Constraint::a(this, PrimitiveMap::CLAUSE_REIF, BytecodeProc::ROOT,
1193 {Val(vpos), Val(vneg), Val(result)}, 0, 1, true);
1194 assert(def_c.first);
1195 result->addRef(this);
1196 result->addDefinition(this, def_c.first);
1197 pushAgg(Val(result), -2);
1198 RefCountedObject::rmRef(this, result);
1199 }
1200 }
1201 } break;
1202 case AggregationCtx::VCTX_VEC: {
1203 // Create a vector on the aggregation stack
1204 _agg[_agg.size() - 2].push(this, _agg.back().createVec(this, newIdent()));
1205 } break;
1206 case AggregationCtx::VCTX_OTHER:
1207 // When closing a VCTX_OTHER context, it should contain at most one value
1208 assert(_agg.back().size() <= 1);
1209 if (_agg.back().size() == 1) {
1210 if (_agg.back()[0].isVar()) {
1211 result = _agg.back()[0].toVar();
1212 }
1213 // push value onto surrounding context
1214 pushAgg(_agg.back()[0], -2);
1215 }
1216 break;
1217 }
1218
1219 _agg.back().destroyStack(this);
1220 if (result && !_agg.back().constraints.empty()) {
1221 // Aggregation produced constraints and exactly one return value, which is a variable
1222 if (result->timestamp() >= _agg.back().def_ident_start) {
1223 // the definition was produced by the current frame, so
1224 // attach all constraints to it
1225 for (Constraint* c : _agg.back().constraints) {
1226 result->addDefinition(this, c);
1227 }
1228 _agg.back().constraints.clear();
1229 // INVARIANT: The result of aggregation is not referenced by any of the registers.
1230 assert(std::none_of(_registers.cbegin() + frame().reg_offset, _registers.cend(),
1231 [result](Val v) { return v.contains(Val(result)); }));
1232 result->binding(this, false);
1233 }
1234 }
1235 if (!_agg.back().constraints.empty()) {
1236 if (_agg.size() == 2) {
1237 // only one frame left, so move all constraints into root context
1238 for (Constraint* c : _agg.back().constraints) {
1239 root()->addDefinition(this, c);
1240 }
1241 } else {
1242 // Move definitions to parent aggregation
1243 for (Constraint* c : _agg.back().constraints) {
1244 _agg[_agg.size() - 2].constraints.push_back(c);
1245 }
1246 }
1247 _agg.back().constraints.clear();
1248 }
1249 _agg.pop_back();
1250 }
1251 } break;
1252 }
1253 assert(!frame().bs->eos(frame().pc));
1254 }
1255}
1256
1257void Interpreter::dumpState(std::ostream& os) {
1258 Variable::dump(root(), _procs, os);
1259 // if (!_agg.empty()) {
1260 // Definition::dump(_agg.back().def_stack, _procs, os, true);
1261 // }
1262}
1263void Interpreter::dumpState(const BytecodeFrame& bf, std::ostream& os) {
1264 for (unsigned int i = bf.reg_offset; i < bf.reg_offset + bf.bs->maxRegister(); i++) {
1265 os << " R" << i << " = " << _registers[i].toString() << "\n";
1266 }
1267}
1268
1269void Interpreter::dumpState() { dumpState(std::cerr); }
1270
1271Interpreter::~Interpreter(void) {
1272 globals.destroy(this);
1273 _registers.resize(this, 0);
1274 _stack.clear();
1275 for (auto& a : _agg) {
1276 a.destroyStack(this);
1277 // a.destroyDef(this); /// TODO: replace with what? Just delete all constraints?
1278 }
1279 assert(cse.size() == _procs.size());
1280 for (int i = 0; i < _procs.size(); ++i) {
1281 switch (_procs[i].nargs) {
1282 case 1: {
1283 auto table = static_cast<CSETable<FixedKey<1>>*>(cse[i]);
1284 table->destroy(this);
1285 break;
1286 }
1287 case 2: {
1288 auto table = static_cast<CSETable<FixedKey<2>>*>(cse[i]);
1289 table->destroy(this);
1290 break;
1291 }
1292 case 3: {
1293 auto table = static_cast<CSETable<FixedKey<3>>*>(cse[i]);
1294 table->destroy(this);
1295 break;
1296 }
1297 case 4: {
1298 auto table = static_cast<CSETable<FixedKey<4>>*>(cse[i]);
1299 table->destroy(this);
1300 break;
1301 }
1302 default: {
1303 auto table = static_cast<CSETable<VariadicKey>*>(cse[i]);
1304 table->destroy(this);
1305 break;
1306 }
1307 }
1308 }
1309 RefCountedObject::rmRef(this, infinite_dom);
1310 RefCountedObject::rmRef(this, boolean_dom);
1311 RefCountedObject::rmRef(this, true_dom);
1312}
1313
1314void Interpreter::call(int code, std::vector<Val>&& args) {
1315 if (_status != ROGER) {
1316 return;
1317 }
1318 assert(code >= 0);
1319 assert(code < _procs.size());
1320 int n = _procs[code].nargs;
1321 const bool cse = true;
1322 BytecodeProc::Mode mode = BytecodeProc::ROOT;
1323 DBG_INTERPRETER("Interpreter::call " << BytecodeProc::mode_to_string[mode] << " " << code << "("
1324 << _procs[code].name << ")" << (cse ? "" : " no_cse"));
1325 DBG_CALLTRACE("\n> " << _procs[code].name << "(");
1326 assert(n == args.size());
1327 for (int i = 0; i < n; i++) {
1328 DBG_INTERPRETER(" R" << i << "(" << args[i].toString(DBG_TRIM_OUTPUT) << ")");
1329 DBG_CALLTRACE(args[i].toString(DBG_TRIM_OUTPUT) << ((i + 1 < n) ? ", " : ")\n"));
1330 }
1331 DBG_INTERPRETER("\n");
1332
1333 // Lookup for Common Subexpression Elimination
1334 size_t cse_depth = _cse_stack.size();
1335 if (cse) {
1336 _cse_stack.emplace_back(*this, code, mode, args.cbegin(), args.cend(), n, _agg.back().size());
1337 // Lookup item in CSE
1338 auto lookup = cse_find(code, _cse_stack.back().getKey(), mode);
1339 if (lookup.second) {
1340 _cse_stack.back().destroy(*this);
1341 _cse_stack.pop_back();
1342 if (mode == BytecodeProc::ROOT || mode == BytecodeProc::ROOT_NEG) {
1343 assert(lookup.first.isInt());
1344 if (lookup.first.toInt() != 1) {
1345 _status = INCONSISTENT;
1346 // Invariant: Last instruction in the frame is always an ABORT instruction
1347 return;
1348 }
1349 } else {
1350 // pushAgg(lookup.first, -1);
1351 assert(false); // Delayed calls can only be ROOT mode
1352 }
1353 return;
1354 }
1355 }
1356
1357 if (_procs[code].mode[mode].size() == 0) {
1358 DBG_INTERPRETER("--- FZN Builtin\n");
1359 // this is a FlatZinc builtin
1360 assert(code != PrimitiveMap::MK_INTVAR);
1361 assert(mode == BytecodeProc::ROOT || mode == BytecodeProc::ROOT_NEG);
1362 auto c = Constraint::a(this, code, mode, args);
1363 if (!(c.first || c.second)) {
1364 // Propagation failed
1365 _status = INCONSISTENT;
1366 return;
1367 }
1368 if (c.first) {
1369 pushConstraint(c.first);
1370 }
1371 if (cse) {
1372 Val ret(c.second);
1373 cse_insert(code, _cse_stack.back().getKey(), mode, ret);
1374 _cse_stack.pop_back();
1375 }
1376 return;
1377 }
1378
1379 // Make the next instruction RET
1380 _stack.back().pc--;
1381 _stack.emplace_back(_procs[code].mode[mode], code, mode);
1382 BytecodeFrame& newFrame = _stack.back();
1383 newFrame.reg_offset = _registers.size();
1384 _registers.resize(this, newFrame.reg_offset + newFrame.bs->maxRegister() + 1);
1385 for (int i = 0; i < args.size(); i++) {
1386 assign(newFrame, i, args[i]);
1387 }
1388 newFrame.cse_frame_depth = cse_depth;
1389
1390 return run();
1391}
1392
1393bool Interpreter::runDelayed() {
1394 std::unordered_map<Constraint*, Variable*> wave = std::move(delayed_constraints);
1395 delayed_constraints.clear();
1396 for (auto pair : wave) {
1397 // Only run delayed constraints that have a definition.
1398 Constraint* c = pair.first;
1399 assert(c->delayed());
1400 if (_procs[c->pred()].mode[BytecodeProc::ROOT].size() == 0) {
1401 continue;
1402 }
1403
1404 // Remove placeholder constraint from variable
1405 Val alias = Val::follow_alias(Val(pair.second));
1406 Variable* v = alias.isVar() ? alias.toVar() : root();
1407 // TODO: This might be quite expensive. Should we store _definitions differently?
1408 auto pos = std::find(std::begin(v->_definitions), std::end(v->_definitions), c);
1409 assert(pos != v->_definitions.end());
1410 v->_definitions.erase(pos);
1411
1412 // Copy arguments into vector
1413 std::vector<Val> args(c->size());
1414 for (int i = 0; i < c->size(); ++i) {
1415 args[i] = c->arg(i);
1416 }
1417
1418 // Execute constraint
1419 std::swap(v, _root_var);
1420 call(c->pred(), std::move(args));
1421 std::swap(v, _root_var);
1422
1423 // Stop if execution caused an error
1424 if (_status != ROGER) {
1425 break;
1426 }
1427 }
1428 return !delayed_constraints.empty();
1429}
1430
1431size_t Trail::save_state(MiniZinc::Interpreter* interpreter) {
1432 trail_size.emplace_back(var_list_trail.size(), obj_trail.size(), alias_trail.size(),
1433 domain_trail.size(), def_trail.size());
1434 timestamp_trail.push_back(interpreter->_identCount);
1435 for (int i = 0; i < interpreter->_procs.size(); ++i) {
1436 switch (interpreter->_procs[i].nargs) {
1437 case 1: {
1438 auto table = static_cast<CSETable<FixedKey<1>>*>(interpreter->cse[i]);
1439 table->push(interpreter, !last_operation_pop);
1440 break;
1441 }
1442 case 2: {
1443 auto table = static_cast<CSETable<FixedKey<2>>*>(interpreter->cse[i]);
1444 table->push(interpreter, !last_operation_pop);
1445 break;
1446 }
1447 case 3: {
1448 auto table = static_cast<CSETable<FixedKey<3>>*>(interpreter->cse[i]);
1449 table->push(interpreter, !last_operation_pop);
1450 break;
1451 }
1452 case 4: {
1453 auto table = static_cast<CSETable<FixedKey<4>>*>(interpreter->cse[i]);
1454 table->push(interpreter, !last_operation_pop);
1455 break;
1456 }
1457 default: {
1458 auto table = static_cast<CSETable<VariadicKey>*>(interpreter->cse[i]);
1459 table->push(interpreter, !last_operation_pop);
1460 break;
1461 }
1462 }
1463 }
1464 last_operation_pop = false;
1465 return len();
1466}
1467
1468void Trail::untrail(MiniZinc::Interpreter* interpreter) {
1469 assert(len() > 0);
1470 assert(interpreter->_stack.size() == 1);
1471 size_t vlt_size, ot_size, at_size, dt_size, deft_size;
1472 std::tie(vlt_size, ot_size, at_size, dt_size, deft_size) = trail_size.back();
1473 trail_size.pop_back();
1474 int timestamp = timestamp_trail.back();
1475 timestamp_trail.pop_back();
1476 // Reconstruct destroyed items
1477 while (obj_trail.size() > ot_size) {
1478 auto obj = obj_trail.back();
1479 switch (obj->rcoType()) {
1480 case RefCountedObject::VAR:
1481 static_cast<Variable*>(obj)->reconstruct(interpreter);
1482 break;
1483 case RefCountedObject::VEC:
1484 static_cast<Vec*>(obj)->reconstruct(interpreter);
1485 break;
1486 default:
1487 assert(false);
1488 }
1489 obj_trail.pop_back();
1490 }
1491 // Restore hedge pointers back to their previous versions
1492 while (var_list_trail.size() > vlt_size) {
1493 auto entry = var_list_trail.back();
1494 *entry.first = entry.second;
1495 var_list_trail.pop_back();
1496 }
1497 // Restore original definitions for created aliases
1498 while (alias_trail.size() > at_size) {
1499 Variable* var;
1500 Val dom;
1501 std::tie(var, dom) = alias_trail.back();
1502 var->unalias(interpreter, dom);
1503 dom.rmMemRef(interpreter);
1504 alias_trail.pop_back();
1505 }
1506 // Restore original domains
1507 while (domain_trail.size() > dt_size) {
1508 Variable* var;
1509 Vec* dom;
1510 std::tie(var, dom) = domain_trail.back();
1511 Val nd(dom);
1512 nd.addRef(interpreter);
1513 var->_domain.rmRef(interpreter);
1514 var->_domain = nd;
1515 RefCountedObject::rmMemRef(interpreter, dom);
1516 domain_trail.pop_back();
1517 }
1518 // Remove all additions/changes to the CSE table
1519 for (int i = 0; i < interpreter->_procs.size(); ++i) {
1520 switch (interpreter->_procs[i].nargs) {
1521 case 1: {
1522 auto table = static_cast<CSETable<FixedKey<1>>*>(interpreter->cse[i]);
1523 table->pop(interpreter);
1524 break;
1525 }
1526 case 2: {
1527 auto table = static_cast<CSETable<FixedKey<2>>*>(interpreter->cse[i]);
1528 table->pop(interpreter);
1529 break;
1530 }
1531 case 3: {
1532 auto table = static_cast<CSETable<FixedKey<3>>*>(interpreter->cse[i]);
1533 table->pop(interpreter);
1534 break;
1535 }
1536 case 4: {
1537 auto table = static_cast<CSETable<FixedKey<4>>*>(interpreter->cse[i]);
1538 table->pop(interpreter);
1539 break;
1540 }
1541 default: {
1542 auto table = static_cast<CSETable<VariadicKey>*>(interpreter->cse[i]);
1543 table->pop(interpreter);
1544 break;
1545 }
1546 }
1547 }
1548 // Undo all changes to definitions
1549 while (def_trail.size() > deft_size) {
1550 Variable* var;
1551 Constraint* con;
1552 bool remove;
1553 std::tie(var, con, remove) = def_trail.back();
1554 if (remove) {
1555 assert(var->definitions().back() == con);
1556 var->_definitions.pop_back();
1557 } else {
1558 var->_definitions.push_back(con);
1559 }
1560 def_trail.pop_back();
1561 }
1562 // Remove all newly created variables
1563 Variable* back = interpreter->root()->prev();
1564 while (back->timestamp() > timestamp) {
1565 Variable* rem = back;
1566 back = back->prev();
1567 rem->destroy(interpreter);
1568 Variable::free(rem);
1569 }
1570 // TODO: Should we remove newly created propagators??
1571 // Reset the timestamp count to its previous value
1572 interpreter->_identCount = timestamp;
1573 last_operation_pop = true;
1574}
1575
1576void Interpreter::optimize(void) {}
1577
1578} // namespace MiniZinc