A set of benchmarks to compare a new prototype MiniZinc implementation
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#pragma once
14
15#include <minizinc/ast.hh>
16#include <minizinc/interpreter/constraint.hh>
17#include <minizinc/interpreter/cse.hh>
18#include <minizinc/interpreter/values.hh>
19#include <minizinc/support/dtrace.h>
20
21#include <deque>
22#include <iostream>
23#include <map>
24#include <unordered_set>
25#include <vector>
26
27// #define DBG_INTERPRETER(msg) std::cerr << msg
28#define DBG_INTERPRETER(msg) \
29 do { \
30 } while (0)
31#define DBG_TRIM_OUTPUT true
32
33namespace MiniZinc {
34
35class Interpreter;
36
37class RegisterFile {
38protected:
39 std::vector<Val> _r;
40 size_t _size;
41 // Note: It seems that the standard library sometimes tries to be smart when
42 // using resize(n) when n < capacity. We therefore use _r.size() as capacity
43 // and _size as the actual size.
44
45 // FIXME: The RegisterFile is said to always have a given size, but it is
46 // currently unknown how many globals are used. This can trigger an assertion.
47public:
48 RegisterFile(int n = 0) : _r(n), _size(n) {}
49 const Val& operator[](int r) {
50 assert(r < _r.size());
51 return _r[r];
52 }
53 size_t size() { return _size; }
54 void resize(Interpreter* interpreter, size_t n) {
55 if (n >= _r.size()) {
56 _r.resize(_r.size() * 2);
57 }
58 if (n < _size) {
59 for (int i = n; i < _size; ++i) {
60 _r[i].rmRef(interpreter);
61 _r[i] = 0;
62 }
63 }
64 _size = n;
65 }
66 std::vector<Val>::const_iterator cbegin() { return _r.cbegin(); }
67 std::vector<Val>::const_iterator cend() { return _r.cend(); }
68 std::vector<Val>::const_iterator iter_n(size_t n) { return this->cbegin() + n; }
69 void assign(Interpreter* interpreter, int r, const Val& v) {
70 assert(r < size());
71 _r[r].assign(interpreter, v);
72 }
73
74 void cp(Interpreter* interpreter, int r1, int r2) {
75 assert(r1 < size());
76 _r[r2].assign(interpreter, _r[r1]);
77 }
78 void cp(Interpreter* interpreter, int r1, RegisterFile& rf, int r2) {
79 assert(r1 < size());
80 rf._r[r2].assign(interpreter, _r[r1]);
81 }
82 /// Destroy this register file
83 void destroy(Interpreter* interpreter) {
84 for (auto& v : _r) {
85 v.rmRef(interpreter);
86 }
87 }
88 void clear(Interpreter* interpreter) {
89 destroy(interpreter);
90 _r.clear();
91 }
92 void dump(std::ostream& os) {
93 for (unsigned int i = 0; i < size(); i++) {
94 os << " R" << i << " = " << _r[i].toString() << "\n";
95 }
96 }
97};
98
99class AggregationCtx {
100protected:
101 /// Stack of values that need to be aggregated
102 std::vector<Val> stack;
103
104public:
105 /// Earliest time stamp for definitions in the current aggregation
106 int def_ident_start;
107 /// Constraints attached to the computed value
108 std::vector<Constraint*> constraints;
109 /// Type of function represented by this context
110 enum Symbol { VCTX_AND, VCTX_OR, VCTX_VEC, VCTX_OTHER, MAX_SYMBOL = VCTX_OTHER } symbol;
111 static const std::string symbol_to_string[MAX_SYMBOL + 1];
112 /// Nesting depth for this symbol (how many of these are open)
113 int n_symbols;
114 /// Constructor
115 AggregationCtx(Interpreter* interpreter, int s);
116 /// Destructor
117 ~AggregationCtx(void);
118 /// Push value onto aggregation stack
119 void push(Interpreter* interpreter, const Val& v) {
120 assert(stack.empty() || symbol != VCTX_OTHER);
121 stack.push_back(v);
122 stack.back().addRef(interpreter);
123 }
124 void pop(Interpreter* interpreter) {
125 stack.back().rmRef(interpreter);
126 stack.pop_back();
127 }
128 const Val& back(void) const { return stack.back(); }
129 const Val& operator[](int i) const { return stack[i]; }
130 int size(void) const { return stack.size(); }
131 bool empty(void) const { return stack.empty(); }
132 Val createVec(Interpreter* interpreter, int timestamp) const;
133 /// Destroy stack values
134 void destroyStack(Interpreter* interpreter) {
135 for (auto& v : stack) {
136 v.rmRef(interpreter);
137 }
138 }
139};
140
141// Frame information for Common Subexpression Elimination
142class CSEFrame {
143public:
144 int proc;
145 BytecodeProc::Mode mode;
146 int nargs;
147 union KeyUnion {
148 VariadicKey vk;
149 FixedKey<1> f1;
150 FixedKey<2> f2;
151 FixedKey<3> f3;
152 FixedKey<4> f4;
153
154 KeyUnion() { new (&vk) VariadicKey(); }
155 ~KeyUnion() {}
156 } key;
157 size_t stack_size;
158
159 CSEFrame(Interpreter& interpreter, int _proc, BytecodeProc::Mode _mode, arg_iter arg_start,
160 arg_iter arg_end, size_t _nargs, size_t _stack_size)
161 : proc(_proc), mode(_mode), stack_size(_stack_size), nargs(_nargs) {
162 switch (nargs) {
163 case 1: {
164 key.f1 = FixedKey<1>(interpreter, arg_start, arg_end);
165 break;
166 }
167 case 2: {
168 key.f2 = FixedKey<2>(interpreter, arg_start, arg_end);
169 break;
170 }
171 case 3: {
172 key.f3 = FixedKey<3>(interpreter, arg_start, arg_end);
173 break;
174 }
175 case 4: {
176 key.f4 = FixedKey<4>(interpreter, arg_start, arg_end);
177 break;
178 }
179 default: {
180 key.vk = VariadicKey(interpreter, arg_start, arg_end, nargs);
181 break;
182 }
183 }
184 }
185
186 CSEFrame(const CSEFrame& other)
187 : proc(other.proc), mode(other.mode), stack_size(other.stack_size), nargs(other.nargs) {
188 switch (nargs) {
189 case 1: {
190 key.f1 = other.key.f1;
191 break;
192 }
193 case 2: {
194 key.f2 = other.key.f2;
195 break;
196 }
197 case 3: {
198 key.f3 = other.key.f3;
199 break;
200 }
201 case 4: {
202 key.f4 = other.key.f4;
203 break;
204 }
205 default: {
206 key.vk = other.key.vk;
207 break;
208 }
209 }
210 };
211
212 inline void destroy(Interpreter& interpreter) {
213 switch (nargs) {
214 case 1: {
215 key.f1.destroy(interpreter);
216 break;
217 }
218 case 2: {
219 key.f2.destroy(interpreter);
220 break;
221 }
222 case 3: {
223 key.f3.destroy(interpreter);
224 break;
225 }
226 case 4: {
227 key.f4.destroy(interpreter);
228 break;
229 }
230 default: {
231 key.vk.destroy(interpreter);
232 break;
233 }
234 }
235 }
236
237 inline CSEKey& getKey() {
238 switch (nargs) {
239 case 1: {
240 return key.f1;
241 }
242 case 2: {
243 return key.f2;
244 }
245 case 3: {
246 return key.f3;
247 }
248 case 4: {
249 return key.f4;
250 }
251 default: {
252 return key.vk;
253 }
254 }
255 }
256};
257
258class BytecodeFrame {
259public:
260 size_t reg_offset;
261 const BytecodeStream* bs;
262 int pc;
263 int _pred;
264 char _mode;
265 size_t cse_frame_depth = 0;
266
267 BytecodeFrame(const BytecodeStream& bs0, int pred, char mode)
268 : reg_offset(0), bs(&bs0), pc(0), _pred(pred), _mode(mode) {}
269};
270
271class Trail {
272 friend class MznSolver;
273
274protected:
275 std::vector<std::pair<Variable**, Variable*>> var_list_trail;
276 std::vector<RefCountedObject*> obj_trail;
277 // <Definition, procedure, size, arg(0)>
278 std::vector<std::tuple<Variable*, Val>> alias_trail;
279 std::vector<std::pair<Variable*, Vec*>> domain_trail;
280 std::vector<std::tuple<Variable*, Constraint*, bool>> def_trail;
281 // <Var list trail size, Obj trail size, Alias trail size, Domain trail size, Def trail size>
282 std::vector<std::tuple<size_t, size_t, size_t, size_t, size_t>> trail_size;
283 std::vector<int> timestamp_trail;
284 bool last_operation_pop = false;
285
286public:
287 Trail() = default;
288 virtual ~Trail() {
289 for (auto& i : obj_trail) {
290 if (i->rcoType() == RefCountedObject::VAR) {
291 Variable::free(static_cast<Variable*>(i));
292 } else {
293 free(i);
294 }
295 }
296 obj_trail.clear();
297 };
298
299 size_t len() { return trail_size.size(); }
300 inline bool is_trailed(RefCountedObject* rco) {
301 return (!trail_size.empty() && timestamp_trail.back() > rco->timestamp());
302 }
303
304 // Trail hedge pointer change
305 inline bool trail_ptr(Variable* obj, Variable** member) {
306 if (!is_trailed(obj)) {
307 return false;
308 }
309 var_list_trail.emplace_back(member, *member);
310 return true;
311 }
312 // Trail Reference Counted Object removal
313 inline bool trail_removal(RefCountedObject* obj) {
314 if (!is_trailed(obj)) {
315 return false;
316 }
317 obj_trail.push_back(obj);
318 return true;
319 }
320 // Trail variable aliasing
321 inline bool trail_alias(Interpreter* interpreter, Variable* v) {
322 if (!is_trailed(v)) {
323 return false;
324 }
325 v->alias().addMemRef(interpreter);
326 alias_trail.emplace_back(v, v->alias());
327 return true;
328 }
329 // Trail definition domain change
330 inline bool trail_domain(Interpreter* interpreter, Variable* v, Vec* dom) {
331 if (!is_trailed(v)) {
332 return false;
333 }
334 assert(dom);
335 dom->addMemRef(interpreter);
336 domain_trail.emplace_back(v, dom);
337 return true;
338 }
339 bool trail_add_def(Variable* var, Constraint* c) {
340 if (!is_trailed(var)) {
341 return false;
342 }
343 def_trail.emplace_back(var, c, true);
344 return true;
345 }
346 bool trail_rm_def(Variable* var, Constraint* c) {
347 if (!is_trailed(var)) {
348 return false;
349 }
350 def_trail.emplace_back(var, c, false);
351 return true;
352 }
353
354 size_t save_state(Interpreter* interpreter);
355 void untrail(Interpreter* interpreter);
356};
357
358// Structure for active loops
359struct LoopState {
360 LoopState(Vec* vec, int _exit_pc)
361 : pos(reinterpret_cast<intptr_t>(vec->begin())),
362 end(reinterpret_cast<intptr_t>(vec->end())),
363 exit_pc(_exit_pc),
364 is_range(false) {}
365
366 LoopState(int l, int u, int _exit_pc) : pos(l), end(u + 1), exit_pc(_exit_pc), is_range(true) {}
367
368 intptr_t pos;
369 intptr_t end;
370
371 int exit_pc : 31;
372 int is_range : 1;
373};
374
375class Interpreter {
376 friend class Trail;
377 friend class MznSolver;
378
379public:
380 enum Status { ROGER, ABORTED, INCONSISTENT, ERROR, MAX_STATUS = ERROR };
381 static const std::string status_to_string[MAX_STATUS + 1];
382
383protected:
384 RegisterFile _registers;
385 std::vector<BytecodeFrame> _stack;
386 std::vector<CSEFrame> _cse_stack;
387 std::vector<AggregationCtx> _agg;
388 std::vector<LoopState> _loops;
389 std::vector<BytecodeProc>& _procs;
390 int _identCount;
391 std::vector<void*> cse; // Different instantiations of CSETable
392 std::unordered_map<Constraint*, Variable*> delayed_constraints;
393 std::deque<Constraint*> _propQueue;
394 RegisterFile globals;
395 Status _status = ROGER;
396
397 // The root variable. It's fixed to true, all toplevel constraints
398 // are attached to it, and it's the head of the linked list of
399 // all variables
400 Variable* _root_var;
401
402 Vec* infinite_dom;
403 Vec* boolean_dom;
404 Vec* true_dom;
405
406public:
407 Trail trail;
408 std::unordered_map<int, Val> solutions;
409
410 Interpreter(std::vector<BytecodeProc>& procs, const BytecodeFrame& f, int max_globals = -1)
411 : _registers(4096),
412 _procs(procs),
413 _identCount(0),
414 cse(procs.size()),
415 globals(max_globals + 1) {
416 _stack.reserve(32);
417 _cse_stack.reserve(32);
418 _stack.emplace_back(f);
419 _registers.resize(this, f.bs->maxRegister() + 1);
420
421 infinite_dom = Vec::a(this, newIdent(), {-Val::infinity(), Val::infinity()});
422 infinite_dom->addRef(this);
423 boolean_dom = Vec::a(this, newIdent(), {0, 1});
424 boolean_dom->addRef(this);
425 true_dom = Vec::a(this, newIdent(), {1, 1});
426 true_dom->addRef(this);
427 _root_var = Variable::createRoot(this, Val(true_dom), newIdent());
428 _root_var->addRef(this);
429 for (int i = 0; i < cse.size(); ++i) {
430 switch (_procs[i].nargs) {
431 case 1: {
432 cse[i] = new CSETable<FixedKey<1>>();
433 break;
434 }
435 case 2: {
436 cse[i] = new CSETable<FixedKey<2>>();
437 break;
438 }
439 case 3: {
440 cse[i] = new CSETable<FixedKey<3>>();
441 break;
442 }
443 case 4: {
444 cse[i] = new CSETable<FixedKey<4>>();
445 break;
446 }
447 default: {
448 cse[i] = new CSETable<VariadicKey>();
449 break;
450 }
451 }
452 }
453 }
454 ~Interpreter(void);
455 Status status() { return _status; }
456 void run(void);
457 bool runDelayed();
458 void pushAgg(const Val& v, int stackOffset);
459 void pushConstraint(Constraint* d);
460 std::pair<Val, bool> cse_find(int proc, const CSEKey& key, BytecodeProc::Mode& mode);
461 void cse_insert(int proc, CSEKey& key, BytecodeProc::Mode& mode, Val& val);
462 void set_global(int i, const Val& val) { globals.assign(this, i, val); }
463 void clear_globals() { globals.clear(this); }
464 const Val get_global(int i) { return globals[i]; }
465 PropStatus subscribe(Constraint* c);
466 void unsubscribe(Constraint* d);
467 int newIdent(void) { return _identCount++; }
468 int currentIdent(void) const { return _identCount; }
469 void dumpState(std::ostream& os);
470 void dumpState(const BytecodeFrame& bf, std::ostream& os);
471 void dumpState();
472 void schedule(Constraint* d, const Variable::SubscriptionEvent& ev);
473 void deschedule(Constraint* d);
474 void propagate(void);
475 void call(int code, std::vector<Val>&& args);
476
477 const Val& reg(const BytecodeFrame& bf, int r) { return _registers[bf.reg_offset + r]; }
478 void assign(const BytecodeFrame& bf, int r, const Val& v) {
479 _registers.assign(this, bf.reg_offset + r, v);
480 }
481 BytecodeFrame& frame() { return _stack.back(); }
482
483 Val infinite_domain() { return Val(infinite_dom); }
484 Val boolean_domain() { return Val(boolean_dom); }
485 void register_delayed(Constraint* c, Variable* v) { delayed_constraints[c] = v; }
486 void remove_delayed(Constraint* c) { delayed_constraints.erase(c); }
487
488 Variable* root() { return _root_var; }
489
490 /// Perform optimizatin by basic propagation on generated FlatZinc
491 void optimize(void);
492};
493
494inline void RefCountedObject::rmRef(Interpreter* interpreter, RefCountedObject* rco) {
495 assert(rco->_model_ref_count > 0);
496 if (--rco->_model_ref_count == 0) {
497 switch (rco->rcoType()) {
498 case VAR:
499 static_cast<Variable*>(rco)->destroy(interpreter);
500 break;
501 case VEC:
502 static_cast<Vec*>(rco)->destroyModel(interpreter);
503 break;
504 default:
505 assert(false);
506 }
507 if (interpreter->trail.is_trailed(rco)) {
508 interpreter->trail.trail_removal(rco);
509 } else if (rco->_memory_ref_count == 0) {
510 // INVARIANT: All children of a definition are already promoted, cut, or freed.
511 // assert(rco->rcoType() != VAR ||
512 // !static_cast<Variable*>(rco)->constraints().empty());
513 if (rco->rcoType() == VAR) {
514 Variable::free(static_cast<Variable*>(rco));
515 } else {
516 ::free(rco);
517 }
518 }
519 }
520}
521
522inline void RefCountedObject::rmMemRef(Interpreter* interpreter, RefCountedObject* rco) {
523 if (--rco->_memory_ref_count == 0u && !interpreter->trail.is_trailed(rco) &&
524 rco->_model_ref_count == 0u) {
525 // INVARIANT: All children of a definition are already promoted, cut, or freed.
526 // assert(rco->rcoType() != DEF || !static_cast<Definition*>(rco)->defs());
527 if (rco->rcoType() == VEC) {
528 static_cast<Vec*>(rco)->destroyMemory(interpreter);
529 }
530 free(rco);
531 }
532}
533
534inline AggregationCtx::AggregationCtx(Interpreter* interpreter, int s)
535 : def_ident_start(interpreter->currentIdent()), symbol(static_cast<Symbol>(s)), n_symbols(1) {
536 assert(s >= 0 && s <= VCTX_OTHER);
537}
538} // namespace MiniZinc
539
540#include <minizinc/interpreter.hpp>
541#include <minizinc/interpreter/cse.hpp>