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/interpreter.hh>
14#include <minizinc/interpreter/primitives.hh>
15#include <minizinc/interpreter/values.hh>
16
17namespace MiniZinc {
18
19std::tuple<std::vector<Val>, std::vector<Val>, Val> simplify_linexp(Val v) {
20 std::vector<Val> coeffs = {Val(1)};
21 std::vector<Val> vars = {v};
22 Val d = 0;
23 simplify_linexp(coeffs, vars, d);
24 return {coeffs, vars, d};
25};
26
27void simplify_linexp(std::vector<Val>& coeffs, std::vector<Val>& vars, Val& d) {
28 assert(coeffs.size() == vars.size());
29 std::vector<std::pair<Val, Val>> defs;
30 defs.reserve(vars.size());
31 for (int j = vars.size() - 1; j >= 0; --j) {
32 if (coeffs[j] != 0) {
33 defs.emplace_back(coeffs[j], vars[j]);
34 }
35 }
36 coeffs.clear();
37 vars.clear();
38
39 std::vector<int> idx;
40 while (!defs.empty()) {
41 Val coeff = defs.back().first;
42 Val stacktop = Val::follow_alias(defs.back().second);
43 defs.pop_back();
44 if (coeff == 0) continue;
45 if (stacktop.isInt()) {
46 d += coeff * stacktop;
47 } else {
48 Variable* cur = stacktop.toVar();
49 if (Constraint* defby = cur->defined_by()) {
50 switch (defby->pred()) {
51 case PrimitiveMap::INT_PLUS: {
52 assert(stacktop == Val::follow_alias(defby->arg(2)));
53 for (int i = 0; i < 2; ++i) {
54 Val arg = Val::follow_alias(defby->arg(i));
55 if (arg.isInt()) {
56 d += coeff * arg;
57 } else {
58 defs.emplace_back(coeff, arg);
59 }
60 }
61 continue;
62 }
63 case PrimitiveMap::INT_MINUS: {
64 assert(stacktop == Val::follow_alias(defby->arg(2)));
65 Val lhs = Val::follow_alias(defby->arg(0));
66 if (lhs.isInt()) {
67 d += coeff * lhs;
68 } else {
69 defs.emplace_back(coeff, lhs);
70 }
71 Val rhs = Val::follow_alias(defby->arg(1));
72 if (rhs.isInt()) {
73 d += coeff * -rhs;
74 } else {
75 defs.emplace_back(-coeff, rhs);
76 }
77 continue;
78 }
79 case PrimitiveMap::INT_SUM: {
80 assert(stacktop == Val::follow_alias(defby->arg(1)));
81 Val arr = defby->arg(0).toVec()->raw_data();
82 for (int i = 0; i < arr.size(); ++i) {
83 Val arg = Val::follow_alias(arr[i]);
84 if (arg.isInt()) {
85 d += coeff * arg;
86 } else {
87 defs.emplace_back(coeff, arg);
88 }
89 }
90 continue;
91 }
92 case PrimitiveMap::INT_TIMES: {
93 assert(stacktop == Val::follow_alias(defby->arg(2)));
94 Val lhs = Val::follow_alias(defby->arg(0));
95 Val rhs = Val::follow_alias(defby->arg(1));
96 if (lhs.isInt()) {
97 if (rhs.isInt()) {
98 // both constants, compute result
99 d += coeff * lhs * rhs;
100 } else {
101 defs.emplace_back(coeff * lhs, rhs);
102 }
103 continue;
104 }
105 if (rhs.isInt()) {
106 defs.emplace_back(coeff * rhs, lhs);
107 continue;
108 }
109 break;
110 }
111 default: {
112 }
113 }
114 }
115 if (coeff != 0) {
116 coeffs.emplace_back(coeff);
117 vars.emplace_back(cur);
118 idx.push_back(idx.size());
119 }
120 }
121 }
122
123 if (coeffs.size() > 1) {
124 // Find and merge duplicate variables
125 class CmpValIdx {
126 public:
127 std::vector<Val>& x;
128 explicit CmpValIdx(std::vector<Val>& x0) : x(x0) {}
129 bool operator()(int i, int j) const { return x[i].timestamp() < x[j].timestamp(); }
130 };
131 std::sort(idx.begin(), idx.end(), CmpValIdx(vars));
132 std::vector<Val> coeffs_simple;
133 coeffs_simple.reserve(coeffs.size());
134 std::vector<Val> vars_simple;
135 vars_simple.reserve(vars.size());
136
137 int ci = 0;
138 coeffs_simple.push_back(coeffs[idx[0]]);
139 vars_simple.push_back(vars[idx[0]]);
140 bool foundDuplicates = false;
141 for (unsigned int i = 1; i < idx.size(); i++) {
142 if (vars[idx[i]].timestamp() == vars_simple[ci].timestamp()) {
143 coeffs_simple[ci] += coeffs[idx[i]];
144 foundDuplicates = true;
145 } else {
146 coeffs_simple.push_back(coeffs[idx[i]]);
147 vars_simple.push_back(vars[idx[i]]);
148 ci++;
149 }
150 }
151 int j = 0;
152 for (unsigned int i = 0; i < coeffs_simple.size(); i++) {
153 if (coeffs_simple[i] != 0) {
154 coeffs[j] = coeffs_simple[i];
155 vars[j++] = vars_simple[i];
156 }
157 }
158 coeffs.resize(j);
159 vars.resize(j);
160 }
161}
162
163std::string Val::toString(bool trim) const {
164 std::ostringstream oss;
165 Val v = follow_alias(*this);
166 if (v.isInt()) {
167 oss << v.toIntVal();
168 } else if (v.isVar()) {
169 if (v.timestamp() >= 0) {
170 oss << "X" << timestamp() << "(";
171 }
172 oss << v.lb().toString() << "," << v.ub().toString();
173 if (v.toVar()->timestamp() >= 0) {
174 oss << ")";
175 }
176 } else {
177 oss << "X" << v.toVec()->timestamp() << "[";
178 if (!trim || v.size() <= 4) {
179 for (size_t i = 0; i < v.size(); i++) {
180 oss << v[i].toString(trim);
181 if (i < v.size() - 1) oss << ",";
182 }
183 } else {
184 oss << "<->";
185 }
186 oss << "]";
187 }
188 return oss.str();
189}
190
191// WARNING: Provide interpreter variable only if v is an uncopied reference
192// with a strong reference count. The reference (and the reference count of
193// the RCO) will be adjusted in case of an alias.
194Val Val::follow_alias(const Val& v, Interpreter* interpreter) {
195 if (v.isVar() && v.toVar()->aliased()) {
196 Val nval = v;
197 while (nval.isVar() && nval.toVar()->aliased()) {
198 nval = nval.toVar()->alias();
199 }
200 if (interpreter && !interpreter->trail.is_trailed(v.toVar())) {
201 Val& mut_v = const_cast<Val&>(v);
202 nval.addRef(interpreter);
203 mut_v.rmRef(interpreter);
204 mut_v._v = nval._v;
205 }
206 return nval;
207 } else {
208 return v;
209 }
210}
211
212Val Val::lb() const {
213 if (isInt()) {
214 return *this;
215 } else if (isVec()) {
216 // Assume it is a set (sorted Vec of integer ranges)
217 assert(operator[](0).isInt());
218 return operator[](0);
219 } else {
220 return toVar()->lb();
221 }
222}
223
224Val Val::ub() const {
225 if (isInt()) {
226 return *this;
227 } else if (isVec()) {
228 // Assume it is a set (sorted Vec of integer ranges)
229 assert(operator[](size() - 1).isInt());
230 return operator[](size() - 1);
231 } else {
232 return toVar()->ub();
233 }
234}
235
236void Val::finalizeLin(Interpreter* interpreter) {
237 if (isInt()) {
238 return;
239 }
240 if (isVar()) {
241 Constraint* c = this->toVar()->defined_by();
242 if (c && c->pred() <= PrimitiveMap::PARTIAL_LINEAR) {
243 // Create linear equation
244 std::vector<Val> coeffs = {Val(1)};
245 std::vector<Val> vars = {*this};
246 Val d = 0;
247 simplify_linexp(coeffs, vars, d);
248
249 Constraint* nc = nullptr;
250 if (vars.empty()) {
251 bool succes = this->toVar()->setVal(interpreter, d);
252 assert(succes);
253 } else if (c->pred() == PrimitiveMap::INT_TIMES && vars.size() == 1 && vars[0] == *this) {
254 // Times operation between two variables. Just leave it as it is.
255 return;
256 } else {
257 assert(std::none_of(vars.begin(), vars.end(), [&](Val v) { return v == *this; }));
258 coeffs.push_back(Val(-1));
259 vars.push_back(*this);
260
261 Vec* ncoeffs = Vec::a(interpreter, interpreter->newIdent(), coeffs);
262 ncoeffs->addRef(interpreter);
263 Vec* nvars = Vec::a(interpreter, interpreter->newIdent(), vars);
264 nvars->addRef(interpreter);
265
266 std::vector<Val> args = {Val(ncoeffs), Val(nvars), Val(-d)};
267 FixedKey<3> cse_key(*interpreter, args);
268 BytecodeProc::Mode mode = BytecodeProc::ROOT;
269 auto lookup = interpreter->cse_find(PrimitiveMap::INT_LIN_EQ, cse_key, mode);
270 if (lookup.second) {
271 // CSE Match found (perform cleanup)
272 assert(lookup.first.isInt());
273 cse_key.destroy(*interpreter);
274
275 // This is the assumption that the linear expression doesn't exist
276 // in negated form in the CSE. If this would happen then the state
277 // should have been marked inconsistent.
278 assert(lookup.first.toInt() == 1);
279 } else {
280 bool b;
281 std::tie(nc, b) = Constraint::a(interpreter, PrimitiveMap::INT_LIN_EQ, mode, args);
282 assert(nc || b);
283 Val cse_val(1);
284 interpreter->cse_insert(PrimitiveMap::INT_LIN_EQ, cse_key, mode, cse_val);
285 }
286
287 RefCountedObject::rmRef(interpreter, ncoeffs);
288 RefCountedObject::rmRef(interpreter, nvars);
289 }
290 // Need to check whether variable still has a definition
291 // (may have been aliased during the construction of nc)
292 c = this->toVar()->defined_by();
293 this->toVar()->_definitions.clear();
294 if (nc) {
295 this->toVar()->addDefinition(interpreter, nc);
296 }
297
298 if (c) {
299 // still had a definition, so destroy it
300 // FIXME: c->destroy will remove a non-existing reference to this.
301 this->toVar()->addRef(interpreter);
302 c->destroy(interpreter);
303 ::free(c);
304 }
305 }
306 } else {
307 this->toVec()->finalizeLin(interpreter);
308 }
309}
310
311} // namespace MiniZinc