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/values.hh>
16#include <minizinc/interpreter/variable.hh>
17
18namespace MiniZinc {
19
20Variable::Variable(Interpreter* interpreter, Val domain, int ident)
21 : RefCountedObject(RefCountedObject::VAR, ident),
22 _prev(this),
23 _next(this),
24 _domain(domain),
25 _binding(true),
26 _aliased(false) {
27 assert(_domain.isVec());
28 _domain.addRef(interpreter);
29 _ann.addRef(interpreter);
30 addRef(interpreter);
31}
32
33Variable::Variable(Interpreter* interpreter, Val domain, bool binding, int ident, Val ann)
34 : RefCountedObject(RefCountedObject::VAR, ident),
35 _prev(this),
36 _next(this),
37 _domain(domain),
38 _ann(ann),
39 _binding(binding),
40 _aliased(false) {
41 assert(_domain.isVec());
42 _domain.addRef(interpreter);
43 _ann.addRef(interpreter);
44 if (binding) addRef(interpreter);
45 // insert into root variable list
46 Variable* v = interpreter->root();
47 interpreter->trail.trail_ptr(this, &_prev);
48 _prev = v->_prev;
49 interpreter->trail.trail_ptr(this, &_next);
50 _next = v;
51 interpreter->trail.trail_ptr(v->_prev, &v->_prev->_next);
52 v->_prev->_next = this;
53 interpreter->trail.trail_ptr(v, &v->_prev);
54 v->_prev = this;
55}
56
57bool Variable::setMin(Interpreter* interpreter, Val i, bool binding) {
58 assert(!aliased());
59 assert(_domain.isVec());
60 assert(_domain.size() % 2 == 0);
61 size_t j = 0;
62 while (j < _domain.size() && _domain[j] < i) {
63 ++j;
64 }
65 if (j == 0) {
66 return true;
67 }
68 if (j == _domain.size()) {
69 Val ndom(Vec::a(interpreter, interpreter->newIdent(), {}));
70 ndom.addRef(interpreter);
71 domain(interpreter, ndom, binding);
72 ndom.rmRef(interpreter);
73 return false;
74 }
75 std::vector<Val> dom;
76 if (j % 2 == 1) {
77 dom.emplace_back(i);
78 }
79 for (; j < _domain.size(); ++j) {
80 dom.push_back(_domain[j]);
81 }
82 Val ndom(Vec::a(interpreter, interpreter->newIdent(), dom));
83 ndom.addRef(interpreter);
84 domain(interpreter, ndom, binding);
85 ndom.rmRef(interpreter);
86 return true;
87}
88
89bool Variable::setMax(Interpreter* interpreter, Val i, bool binding) {
90 assert(!aliased());
91 assert(_domain.isVec());
92 assert(_domain.size() % 2 == 0);
93 int j = _domain.size() - 1;
94 while (j >= 0 && _domain[j] > i) {
95 --j;
96 }
97 if (j == _domain.size() - 1) {
98 return true;
99 }
100 if (j < 0) {
101 Val ndom(Vec::a(interpreter, interpreter->newIdent(), {}));
102 ndom.addRef(interpreter);
103 domain(interpreter, ndom, binding);
104 ndom.rmRef(interpreter);
105 return false;
106 }
107 std::vector<Val> dom;
108 for (size_t k = 0; k <= j; ++k) {
109 dom.push_back(_domain[k]);
110 }
111 if (j % 2 == 0) {
112 dom.emplace_back(i);
113 }
114 Val ndom(Vec::a(interpreter, interpreter->newIdent(), dom));
115 ndom.addRef(interpreter);
116 domain(interpreter, ndom, binding);
117 ndom.rmRef(interpreter);
118 return true;
119}
120
121bool Variable::setVal(Interpreter* interpreter, Val i, bool binding) {
122 assert(!aliased());
123 assert(_domain.isVec());
124 assert(_domain.size() % 2 == 0);
125 for (int j = 0; j < _domain.size(); j += 2) {
126 if (_domain[j] <= i && i <= _domain[j + 1]) {
127 this->binding(interpreter, binding);
128 alias(interpreter, i);
129 return true;
130 }
131 }
132 Val ndom(Vec::a(interpreter, interpreter->newIdent(), {}));
133 ndom.addRef(interpreter);
134 domain(interpreter, ndom, binding);
135 ndom.rmRef(interpreter);
136 return false;
137}
138
139bool Variable::intersectDom(Interpreter* interpreter, const std::vector<Val>& dom, bool binding) {
140 if (!isBounded()) {
141 Val ndom(Vec::a(interpreter, interpreter->newIdent(), dom));
142 ndom.addRef(interpreter);
143 domain(interpreter, ndom, binding);
144 ndom.rmRef(interpreter);
145 return true;
146 }
147 assert(!aliased());
148 assert(_domain.isVec());
149 assert(_domain.size() % 2 == 0);
150 VecSetRanges vsr1(_domain.toVec());
151 StdVecSetRanges vsr2(&dom);
152 Ranges::Inter<Val, VecSetRanges, StdVecSetRanges> inter(vsr1, vsr2);
153 std::vector<Val> result;
154 for (; inter(); ++inter) {
155 result.emplace_back(inter.min());
156 result.emplace_back(inter.max());
157 }
158 Val ndom(Vec::a(interpreter, interpreter->newIdent(), result));
159 ndom.addRef(interpreter);
160 domain(interpreter, ndom, binding);
161 ndom.rmRef(interpreter);
162 return !result.empty();
163}
164
165bool Variable::intersectDom(Interpreter* interpreter, Val dom, bool binding) {
166 assert(!dom.isVar());
167 if (dom.isInt()) {
168 return setVal(interpreter, dom);
169 }
170 // TODO: Allocation is not really necessary;
171 std::vector<Val> vdom(dom.size());
172 for (int i = 0; i < dom.size(); ++i) {
173 vdom[i] = dom[i];
174 }
175 return intersectDom(interpreter, vdom, binding);
176}
177
178void Variable::domain(Interpreter* interpreter, const Val& newDomain, bool binding0) {
179 assert(!aliased());
180 assert(!newDomain.isRCO() || newDomain.toRCO()->alive());
181 assert(_domain.isVec());
182 interpreter->trail.trail_domain(interpreter, this, _domain.toVec());
183 SubscriptionEvent sev;
184 if (newDomain.isInt()) {
185 alias(interpreter, newDomain);
186 sev = SEV_VAL;
187 } else if (newDomain.size() == 2 && newDomain[0] == newDomain[1]) {
188 alias(interpreter, newDomain[0]);
189 sev = SEV_VAL;
190 } else {
191 Val nd = newDomain;
192 nd.addRef(interpreter);
193 _domain.rmRef(interpreter);
194 _domain = newDomain;
195 sev = SEV_DOM;
196 }
197 for (auto& s : _subscriptions) {
198 if (sev == SEV_VAL || s.second == SES_ANY) {
199 interpreter->schedule(s.first, sev);
200 }
201 }
202 binding(interpreter, binding0);
203}
204void Variable::domain(Interpreter* interpreter, const std::vector<Val>& newDomain, bool binding0) {
205 if (!isBounded()) {
206 Val ndom(Vec::a(interpreter, interpreter->newIdent(), newDomain));
207 ndom.addRef(interpreter);
208 domain(interpreter, ndom, binding0);
209 ndom.rmRef(interpreter);
210 } else {
211 bool did_update = false;
212 if (newDomain.size() != _domain.size()) {
213 did_update = true;
214 } else {
215 for (int i = 0; i < newDomain.size(); i++) {
216 if (newDomain[i] != _domain[i]) {
217 did_update = true;
218 break;
219 }
220 }
221 }
222 if (did_update) {
223 Val ndv(Vec::a(interpreter, interpreter->newIdent(), newDomain));
224 ndv.addRef(interpreter);
225 domain(interpreter, ndv, binding0);
226 ndv.rmRef(interpreter);
227 }
228 }
229}
230
231void Variable::destroy(MiniZinc::Interpreter* interpreter) {
232 _model_ref_count = (1u << 31u) - 1u;
233 _domain.rmRef(interpreter);
234 _ann.rmRef(interpreter);
235 interpreter->trail.trail_ptr(_prev, &(_prev->_next));
236 _prev->_next = _next;
237 interpreter->trail.trail_ptr(_next, &(_next->_prev));
238 _next->_prev = _prev;
239 interpreter->trail.trail_ptr(this, &_next);
240 _next = this;
241 interpreter->trail.trail_ptr(this, &_prev);
242 _prev = this;
243
244 for (auto c : _definitions) {
245 c->destroy(interpreter);
246 }
247 _model_ref_count = 0;
248}
249
250void Variable::reconstruct(Interpreter* interpreter) {
251 /// TODO: what about subscriptions?
252 assert(_model_ref_count == 0);
253 _ann.addRef(interpreter);
254 _domain.addRef(interpreter);
255 for (auto c : _definitions) {
256 c->reconstruct(interpreter);
257 }
258 _model_ref_count = 0;
259}
260
261void Variable::addDefinition(Interpreter* interpreter, Constraint* c) {
262 _definitions.push_back(c);
263 if (this != interpreter->root()) {
264 // Remove reference counts for this variable from each argument in c
265 for (int i = 0; i < c->size(); i++) {
266 if (c->arg(i).isVar()) {
267 if (c->arg(i).timestamp() == _timestamp) {
268 RefCountedObject::rmRef(interpreter, this);
269 }
270 } else if (c->arg(i).isVec()) {
271 Val content = c->arg(i).toVec()->raw_data();
272 bool hasVar = false;
273 for (int j = 0; j < content.size(); j++) {
274 if (content[j].isVar() && content[j].timestamp() == _timestamp) {
275 hasVar = true;
276 break;
277 }
278 }
279 if (hasVar) {
280 if (!c->arg(i).unique() || !content.unique()) {
281 // make vectors unique so that we can safely decrement reference counts
282 std::vector<Val> vals(content.size());
283 for (int i = 0; i < vals.size(); i++) {
284 vals[i] = content[i];
285 }
286 Val v = Val(Vec::a(interpreter, interpreter->newIdent(), vals));
287 if (c->arg(i).toVec()->hasIndexSet()) {
288 v = Val(Vec::a(interpreter, interpreter->newIdent(),
289 {v, c->arg(i).toVec()->index_set()}));
290 }
291 c->arg(interpreter, i, Val(v));
292 }
293 for (int j = 0; j < content.size(); j++) {
294 if (content[j].timestamp() == _timestamp) {
295 RefCountedObject::rmRef(interpreter, this);
296 }
297 }
298 }
299 }
300 }
301 }
302 if (c->delayed()) {
303 interpreter->register_delayed(c, this);
304 }
305 interpreter->trail.trail_add_def(this, c);
306}
307
308void Variable::alias(Interpreter* interpreter, Val v) {
309 assert(!_aliased);
310 assert(!v.isVar() || v.toVar() != this);
311 // Move defining constraints to current context
312
313 for (Constraint* c : _definitions) {
314 for (int i = 0; i < c->size(); ++i) {
315 Val arg = c->arg(i);
316 if (arg.isVec()) {
317 _model_ref_count += arg.toVec()->count(Val(this));
318 } else {
319 _model_ref_count += (arg == Val(this));
320 }
321 }
322 interpreter->trail.trail_rm_def(this, c);
323 interpreter->pushConstraint(c);
324 }
325 _definitions.clear();
326
327 // Destroy old domain
328 _domain.rmRef(interpreter);
329 _ann.rmRef(interpreter);
330 _ann = 0;
331
332 // Reset reference count for binding status
333 // TODO: this may be incorrect if we are aliasing a variable with
334 // TODO: binding domain to one with non-binding domain
335 binding(interpreter, false);
336
337 // Transfer subscriptions to new value and schedule propagators
338 for (auto& s : _subscriptions) {
339 if (v.isVar()) {
340 v.toVar()->subscribe(s.first, s.second);
341 }
342 if (s.second == SES_VALUNIFY || s.second == SES_ANY) {
343 interpreter->schedule(s.first, SEV_UNIFY);
344 }
345 }
346 _subscriptions.clear();
347
348 // Set Alias
349 _aliased = true;
350 _domain = v;
351 v.addRef(interpreter);
352 interpreter->trail.trail_alias(interpreter, this);
353}
354
355void Variable::unalias(Interpreter* interpreter, Val dom) {
356 /// TODO!!!
357 // auto ref_count = _ref_count;
358 // _pred = proc;
359 // _size = size;
360 // _args[0].destroy(interpreter);
361 // _args[0] = arg0;
362 // for (int i = 0; i < _size; ++i) {
363 // _args[i].construct(interpreter);
364 // }
365 // // TODO: Transfer back subscriptions moved on aliasing?
366 // interpreter->subscribe(this);
367 // _ann.construct(interpreter);
368 // _domain->addRef(interpreter);
369 // _ref_count = ref_count;
370}
371
372void Variable::binding(Interpreter* interpreter, bool f) {
373 if (!_binding && f) {
374 addRef(interpreter);
375 } else if (_binding && !f) {
376 RefCountedObject::rmRef(interpreter, this);
377 }
378 _binding = f;
379}
380
381void Variable::subscribe(Constraint* c, const SubscriptionEventSet& events) {
382 Variable* sub = this;
383 while (sub && sub->aliased()) {
384 if (sub->_domain.isVar()) {
385 sub = sub->_domain.toVar();
386 } else {
387 sub = nullptr;
388 }
389 }
390 if (sub) {
391 sub->_subscriptions.insert(std::make_pair(c, events));
392 }
393}
394void Variable::unsubscribe(Constraint* c) {
395 Variable* sub = this;
396 while (sub && sub->aliased()) {
397 if (sub->_domain.isVar()) {
398 sub = sub->_domain.toVar();
399 } else {
400 sub = nullptr;
401 }
402 }
403 if (sub) {
404 sub->_subscriptions.erase(c);
405 }
406}
407
408void Variable::dump(Variable* head, const std::vector<BytecodeProc>& bs, std::ostream& os) {
409 Variable* d = head;
410 do {
411 d = d->next();
412 if (d != head) {
413 if (d->timestamp() >= 0) {
414 os << d->timestamp() << "(";
415 }
416 os << d << "." << d->_model_ref_count;
417 if (d->timestamp() >= 0) {
418 os << ")";
419 }
420 os << ":\t";
421 if (d->aliased()) {
422 os << " alias " << d->alias().toString() << "\n";
423 } else {
424 if (d->domain()) {
425 if (d->_binding) {
426 os << " binding";
427 }
428 os << " domain: " << Val(d->domain()).toString();
429 }
430 }
431 os << "\n";
432 if (!d->_subscriptions.empty()) {
433 os << " subscriptions: ";
434 for (auto& s : d->_subscriptions) {
435 os << s.first << " ";
436 }
437 os << "\n";
438 }
439 }
440 for (Constraint* c : d->_definitions) {
441 if (d != head) {
442 os << " ";
443 }
444 os << c << " " << bs[c->pred()].name << "(";
445 for (int i = 0; i < c->size(); i++) {
446 os << c->arg(i).toString();
447 if (i < c->size() - 1) os << ", ";
448 }
449 os << ")\n";
450 }
451 } while (d != head);
452}
453
454} // namespace MiniZinc