this repo has no description
dekker.one
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2
3/*
4 * Main authors:
5 * Jip J. Dekker <jip.dekker@monash.edu>
6 */
7
8/* This Source Code Form is subject to the terms of the Mozilla Public
9 * License, v. 2.0. If a copy of the MPL was not distributed with this
10 * file, You can obtain one at http://mozilla.org/MPL/2.0/. */
11
12#include <minizinc/ast.hh>
13#include <minizinc/astiterator.hh>
14#include <minizinc/chain_compressor.hh>
15#include <minizinc/flatten_internal.hh>
16
17namespace MiniZinc {
18
19void ChainCompressor::removeItem(Item* i) {
20 CollectDecls cd(_env.varOccurrences, _deletedVarDecls, i);
21 if (auto* ci = i->dynamicCast<ConstraintI>()) {
22 top_down(cd, ci->e());
23 } else if (auto* vdi = i->dynamicCast<VarDeclI>()) {
24 top_down(cd, vdi->e());
25 } else {
26 assert(false); // CURRENTLY NOT SUPPORTED
27 }
28 i->remove();
29}
30
31int ChainCompressor::addItem(Item* i) {
32 _env.flatAddItem(i);
33 int item_idx = static_cast<int>(_env.flat()->size()) - 1;
34 trackItem(i);
35 return item_idx;
36}
37
38void ChainCompressor::updateCount() {
39 for (auto it = _items.begin(); it != _items.end();) {
40 if (it->second->removed()) {
41 it = _items.erase(it);
42 } else {
43 ++it;
44 }
45 }
46}
47
48void ChainCompressor::replaceCallArgument(Item* i, Call* c, unsigned int n, Expression* e) {
49 CollectDecls cd(_env.varOccurrences, _deletedVarDecls, i);
50 top_down(cd, c->arg(n));
51 c->arg(n, e);
52 CollectOccurrencesE ce(_env.varOccurrences, i);
53 top_down(ce, e);
54}
55
56bool ImpCompressor::trackItem(Item* i) {
57 if (i->removed()) {
58 return false;
59 }
60 if (auto* ci = i->dynamicCast<ConstraintI>()) {
61 if (auto* c = ci->e()->dynamicCast<Call>()) {
62 // clause([y], [x]); i.e. x -> y
63 if (c->id() == constants().ids.clause) {
64 auto* positive = c->arg(0)->cast<ArrayLit>();
65 auto* negative = c->arg(1)->cast<ArrayLit>();
66 if (positive->length() == 1 && negative->length() == 1) {
67 auto* var = (*negative)[0]->cast<Id>();
68 storeItem(var->decl(), i);
69 return true;
70 }
71 } else if (c->id() == "mzn_reverse_map_var") {
72 auto* control = c->arg(0)->cast<Id>();
73 assert(control->type().isvarbool());
74 storeItem(control->decl(), i);
75 return true;
76 // pred_imp(..., b); i.e. b -> pred(...)
77 } else if (c->id().endsWith("_imp")) {
78 auto* control = c->arg(c->argCount() - 1)->cast<Id>();
79 assert(control->type().isvarbool());
80 storeItem(control->decl(), i);
81 return true;
82 }
83 }
84 } else if (auto* vdi = i->dynamicCast<VarDeclI>()) {
85 if (vdi->e()->type().isvarbool() && (vdi->e() != nullptr) && (vdi->e()->e() != nullptr)) {
86 if (auto* c = vdi->e()->e()->dynamicCast<Call>()) {
87 // x = forall([y,z,...]); potentially: x -> (y /\ z /\ ...)
88 if (c->id() == constants().ids.forall) {
89 storeItem(vdi->e(), i);
90 return true;
91 // x ::ctx_pos = pred(...); potentially: pred_imp(..., x); i.e. x -> pred(...)
92 }
93 if (_env.fopts.enableHalfReification && vdi->e()->ann().contains(constants().ctx.pos)) {
94 GCLock lock;
95 auto cid = EnvI::halfReifyId(c->id());
96 std::vector<Type> args;
97 args.reserve(c->argCount() + 1);
98 for (int j = 0; j < c->argCount(); ++j) {
99 args.push_back(c->arg(j)->type());
100 }
101 args.push_back(Type::varbool());
102 FunctionI* decl = _env.model->matchFn(_env, cid, args, false);
103
104 if (decl != nullptr) {
105 storeItem(vdi->e(), i);
106 return true;
107 }
108 }
109 }
110 }
111 }
112 return false;
113}
114
115void ImpCompressor::compress() {
116 for (auto it = _items.begin(); it != _items.end();) {
117 VarDecl* lhs = nullptr;
118 VarDecl* rhs = nullptr;
119 // Check if compression is possible
120 if (auto* ci = it->second->dynamicCast<ConstraintI>()) {
121 auto* c = ci->e()->cast<Call>();
122 if (c->id() == constants().ids.clause) {
123 auto* positive = c->arg(0)->cast<ArrayLit>();
124 auto* var = (*positive)[0]->cast<Id>();
125 bool output_var = var->decl()->ann().contains(constants().ann.output_var);
126 auto usages = _env.varOccurrences.usages(var->decl());
127 output_var = output_var || usages.second;
128 int occurrences = usages.first;
129 unsigned long lhs_occurences = count(var->decl());
130
131 // Compress if:
132 // - There is one occurrence on the RHS of a clause and the others are on the LHS of a
133 // clause
134 // - There is one occurrence on the RHS of a clause, that Id is a reified forall that has no
135 // other occurrences
136 // - There is one occurrence on the RHS of a clause, that Id is a reification in a positive
137 // context, and all other occurrences are on the LHS of a clause
138 bool compress = !output_var && lhs_occurences > 0;
139 if ((var->decl()->e() != nullptr) && (var->decl()->e()->dynamicCast<Call>() != nullptr)) {
140 auto* call = var->decl()->e()->cast<Call>();
141 if (call->id() == constants().ids.forall) {
142 compress = compress && (occurrences == 1 && lhs_occurences == 1);
143 } else {
144 compress = compress && (occurrences == lhs_occurences);
145 }
146 } else {
147 compress = compress && (occurrences == lhs_occurences + 1);
148 }
149 if (compress) {
150 rhs = var->decl();
151 auto* negative = c->arg(1)->cast<ArrayLit>();
152 lhs = (*negative)[0]->cast<Id>()->decl();
153 if (lhs == rhs) {
154 continue;
155 }
156 }
157 // TODO: Detect equivalences for output variables.
158 }
159 }
160
161 if ((lhs != nullptr) && (rhs != nullptr)) {
162 assert(count(rhs) > 0);
163
164 auto range = find(rhs);
165 std::vector<Item*> to_process;
166 for (auto match = range.first; match != range.second; ++match) {
167 to_process.push_back(match->second);
168 }
169 _items.erase(range.first, range.second);
170 for (auto* item : to_process) {
171 bool success = compressItem(item, lhs);
172 assert(success);
173 _env.counters.impDel++;
174 }
175
176 assert(!rhs->ann().contains(constants().ann.output_var));
177 removeItem(it->second);
178 it = _items.erase(it);
179 } else {
180 ++it;
181 }
182 }
183}
184
185bool ImpCompressor::compressItem(Item* i, VarDecl* newLHS) {
186 GCLock lock;
187 if (auto* ci = i->dynamicCast<ConstraintI>()) {
188 auto* c = ci->e()->cast<Call>();
189 // Given (x -> y) /\ (y -> z), produce x -> z
190 if (c->id() == constants().ids.clause) {
191 auto* positive = c->arg(0)->cast<ArrayLit>();
192 auto* rhs = (*positive)[0]->cast<Id>();
193 if (rhs->decl() != newLHS) {
194 ConstraintI* nci = constructClause(positive, newLHS->id());
195 _boolConstraints.push_back(addItem(nci));
196 }
197 removeItem(i);
198 return true;
199 // Given (x -> y) /\ (y -> pred(...)), produce x -> pred(...)
200 }
201 if (c->id() == "mzn_reverse_map_var") {
202 return true;
203 }
204 if (c->id().endsWith("_imp")) {
205 replaceCallArgument(i, c, c->argCount() - 1, newLHS->id());
206 trackItem(i);
207 return true;
208 }
209 } else if (auto* vdi = i->dynamicCast<VarDeclI>()) {
210 auto* c = vdi->e()->e()->dynamicCast<Call>();
211 // Given: (x -> y) /\ (y -> (a /\ b /\ ...)), produce (x -> a) /\ (x -> b) /\ ...
212 if (c->id() == constants().ids.forall) {
213 auto* exprs = c->arg(0)->cast<ArrayLit>();
214 for (int j = 0; j < exprs->size(); ++j) {
215 auto* rhs = (*exprs)[j]->cast<Id>();
216 if (rhs->decl() != newLHS) {
217 ConstraintI* nci = constructClause(rhs, newLHS->id());
218 _boolConstraints.push_back(addItem(nci));
219 }
220 }
221 return true;
222 // x ::ctx_pos = pred(...); potentially: pred_imp(..., x); i.e. x -> pred(...)
223 }
224 if (vdi->e()->ann().contains(constants().ctx.pos)) {
225 ConstraintI* nci = constructHalfReif(c, newLHS->id());
226 assert(nci);
227 addItem(nci);
228 return true;
229 }
230 }
231 return false;
232}
233
234ConstraintI* ImpCompressor::constructClause(Expression* pos, Expression* neg) {
235 assert(GC::locked());
236 std::vector<Expression*> args(2);
237 if (pos->dynamicCast<ArrayLit>() != nullptr) {
238 args[0] = pos;
239 } else {
240 assert(neg->type().isbool());
241 std::vector<Expression*> eVec(1);
242 eVec[0] = pos;
243 args[0] = new ArrayLit(pos->loc().introduce(), eVec);
244 args[0]->type(Type::varbool(1));
245 }
246 if (neg->dynamicCast<ArrayLit>() != nullptr) {
247 args[1] = neg;
248 } else {
249 assert(neg->type().isbool());
250 std::vector<Expression*> eVec(1);
251 eVec[0] = neg;
252 args[1] = new ArrayLit(neg->loc().introduce(), eVec);
253 args[1]->type(Type::varbool(1));
254 }
255 // NEVER CREATE (a -> a)
256 assert((*args[0]->dynamicCast<ArrayLit>())[0]->dynamicCast<Id>()->decl() !=
257 (*args[1]->dynamicCast<ArrayLit>())[0]->dynamicCast<Id>()->decl());
258 auto* nc = new Call(MiniZinc::Location().introduce(), constants().ids.clause, args);
259 nc->type(Type::varbool());
260 nc->decl(_env.model->matchFn(_env, nc, false));
261 assert(nc->decl());
262
263 return new ConstraintI(MiniZinc::Location().introduce(), nc);
264}
265
266ConstraintI* ImpCompressor::constructHalfReif(Call* call, Id* control) {
267 assert(_env.fopts.enableHalfReification);
268 assert(GC::locked());
269 auto cid = EnvI::halfReifyId(call->id());
270 std::vector<Expression*> args(call->argCount());
271 for (int i = 0; i < call->argCount(); ++i) {
272 args[i] = call->arg(i);
273 }
274 args.push_back(control);
275 FunctionI* decl = _env.model->matchFn(_env, cid, args, false);
276 if (decl != nullptr) {
277 auto* nc = new Call(call->loc().introduce(), cid, args);
278 nc->decl(decl);
279 nc->type(Type::varbool());
280 return new ConstraintI(call->loc().introduce(), nc);
281 }
282 return nullptr;
283}
284
285bool LECompressor::trackItem(Item* i) {
286 if (i->removed()) {
287 return false;
288 }
289 bool added = false;
290 if (auto* ci = i->dynamicCast<ConstraintI>()) {
291 if (auto* call = ci->e()->dynamicCast<Call>()) {
292 // {int,float}_lin_le([c1,c2,...], [x, y,...], 0);
293 if (call->id() == constants().ids.int_.lin_le ||
294 call->id() == constants().ids.float_.lin_le) {
295 auto* as = follow_id(call->arg(0))->cast<ArrayLit>();
296 auto* bs = follow_id(call->arg(1))->cast<ArrayLit>();
297 assert(as->size() == bs->size());
298
299 for (int j = 0; j < as->size(); ++j) {
300 if (as->type().isIntArray()) {
301 if (follow_id((*as)[j])->cast<IntLit>()->v() > IntVal(0)) {
302 // Check if left hand side is a variable (could be constant)
303 if (auto* decl = follow_id_to_decl((*bs)[j])->dynamicCast<VarDecl>()) {
304 storeItem(decl, i);
305 added = true;
306 }
307 }
308 } else {
309 if (follow_id((*as)[j])->cast<FloatLit>()->v() > FloatVal(0)) {
310 // Check if left hand side is a variable (could be constant)
311 if (auto* decl = follow_id_to_decl((*bs)[j])->dynamicCast<VarDecl>()) {
312 storeItem(decl, i);
313 added = true;
314 }
315 }
316 }
317 }
318 }
319 assert(call->id() != constants().ids.int2float);
320 }
321 } else if (auto* vdi = i->dynamicCast<VarDeclI>()) {
322 assert(vdi->e());
323 if (Expression* vde = vdi->e()->e()) {
324 if (auto* call = vde->dynamicCast<Call>()) {
325 if (call->id() == constants().ids.int2float) {
326 if (auto* vd = follow_id_to_decl(call->arg(0))->dynamicCast<VarDecl>()) {
327 auto* alias = follow_id_to_decl(vdi->e())->cast<VarDecl>();
328 _aliasMap[vd] = alias;
329 }
330 }
331 }
332 }
333 }
334 return added;
335}
336
337void LECompressor::compress() {
338 for (auto it = _items.begin(); it != _items.end();) {
339 VarDecl* lhs = nullptr;
340 VarDecl* rhs = nullptr;
341 VarDecl* alias = nullptr;
342
343 // Check if compression is possible
344 if (auto* ci = it->second->dynamicCast<ConstraintI>()) {
345 auto* call = ci->e()->cast<Call>();
346 if (call->id() == constants().ids.int_.lin_le) {
347 auto* as = follow_id(call->arg(0))->cast<ArrayLit>();
348 auto* bs = follow_id(call->arg(1))->cast<ArrayLit>();
349 auto* c = follow_id(call->arg(2))->cast<IntLit>();
350
351 if (bs->size() == 2 && c->v() == IntVal(0)) {
352 auto a0 = follow_id((*as)[0])->cast<IntLit>()->v();
353 auto a1 = follow_id((*as)[1])->cast<IntLit>()->v();
354 if (a0 == -a1 && eqBounds((*bs)[0], (*bs)[1])) {
355 int i = a0 < a1 ? 0 : 1;
356 if (!(*bs)[i]->isa<Id>()) {
357 break;
358 }
359 auto* neg = follow_id_to_decl((*bs)[i])->cast<VarDecl>();
360 bool output_var = neg->ann().contains(constants().ann.output_var);
361
362 auto usages = _env.varOccurrences.usages(neg);
363 int occurrences = usages.first;
364 output_var = output_var || usages.second;
365 unsigned long lhs_occurences = count(neg);
366 bool compress = !output_var;
367 auto search = _aliasMap.find(neg);
368
369 if (search != _aliasMap.end()) {
370 alias = search->second;
371 auto alias_usages = _env.varOccurrences.usages(alias);
372 int alias_occ = alias_usages.first;
373 compress = compress && (!alias_usages.second);
374 unsigned long alias_lhs_occ = count(alias);
375 // neg is only allowed to occur:
376 // - once in the "implication"
377 // - once in the aliasing
378 // - on a lhs of other expressions
379 // alias is only allowed to occur on a lhs of an expression.
380 compress = compress && (lhs_occurences + alias_lhs_occ > 0) &&
381 (occurrences == lhs_occurences + 2) && (alias_occ == alias_lhs_occ);
382 } else {
383 // neg is only allowed to occur:
384 // - once in the "implication"
385 // - on a lhs of other expressions
386 compress = compress && (lhs_occurences > 0) && (occurrences == lhs_occurences + 1);
387 }
388
389 auto* pos = follow_id_to_decl((*bs)[1 - i])->dynamicCast<VarDecl>();
390 if ((pos != nullptr) && compress) {
391 rhs = neg;
392 lhs = pos;
393 assert(lhs != rhs);
394 }
395 // TODO: Detect equivalences for output variables.
396 }
397 }
398 }
399 }
400
401 if ((lhs != nullptr) && (rhs != nullptr)) {
402 assert(count(rhs) + count(alias) > 0);
403
404 auto range = find(rhs);
405
406 {
407 std::vector<Item*> to_process;
408 for (auto match = range.first; match != range.second; ++match) {
409 to_process.push_back(match->second);
410 }
411 _items.erase(range.first, range.second);
412 for (auto* item : to_process) {
413 leReplaceVar<IntLit>(item, rhs, lhs);
414 }
415 }
416 if (alias != nullptr) {
417 VarDecl* i2f_lhs;
418
419 auto search = _aliasMap.find(lhs);
420 if (search != _aliasMap.end()) {
421 i2f_lhs = search->second;
422 } else {
423 // Create new int2float
424 Call* i2f = new Call(lhs->loc().introduce(), constants().ids.int2float, {lhs->id()});
425 i2f->decl(_env.model->matchFn(_env, i2f, false));
426 assert(i2f->decl());
427 i2f->type(Type::varfloat());
428 auto* domain =
429 new SetLit(lhs->loc().introduce(), eval_floatset(_env, lhs->ti()->domain()));
430 auto* i2f_ti = new TypeInst(lhs->loc().introduce(), Type::varfloat(), domain);
431 i2f_lhs = new VarDecl(lhs->loc().introduce(), i2f_ti, _env.genId(), i2f);
432 i2f_lhs->type(Type::varfloat());
433 addItem(new VarDeclI(lhs->loc().introduce(), i2f_lhs));
434 }
435
436 auto arange = find(alias);
437 {
438 std::vector<Item*> to_process;
439 for (auto match = arange.first; match != arange.second; ++match) {
440 to_process.push_back(match->second);
441 }
442 _items.erase(arange.first, arange.second);
443 for (auto* item : to_process) {
444 leReplaceVar<FloatLit>(item, alias, i2f_lhs);
445 }
446 }
447 }
448
449 assert(!rhs->ann().contains(constants().ann.output_var));
450 removeItem(it->second);
451 _env.counters.linDel++;
452 it = _items.erase(it);
453 } else {
454 ++it;
455 }
456 }
457}
458
459template <class Lit>
460void LECompressor::leReplaceVar(Item* i, VarDecl* oldVar, VarDecl* newVar) {
461 typedef typename LinearTraits<Lit>::Val Val;
462 GCLock lock;
463
464 auto* ci = i->cast<ConstraintI>();
465 auto* call = ci->e()->cast<Call>();
466 assert(call->id() == constants().ids.int_.lin_le || call->id() == constants().ids.float_.lin_le);
467
468 // Remove old occurrences
469 CollectDecls cd(_env.varOccurrences, _deletedVarDecls, i);
470 top_down(cd, ci->e());
471
472 ArrayLit* al_c = eval_array_lit(_env, call->arg(0));
473 std::vector<Val> coeffs(al_c->size());
474 for (int j = 0; j < al_c->size(); j++) {
475 coeffs[j] = LinearTraits<Lit>::eval(_env, (*al_c)[j]);
476 }
477 ArrayLit* al_x = eval_array_lit(_env, call->arg(1));
478 std::vector<KeepAlive> x(al_x->size());
479 for (int j = 0; j < al_x->size(); j++) {
480 Expression* decl = follow_id_to_decl((*al_x)[j]);
481 if (decl && decl->cast<VarDecl>() == oldVar) {
482 x[j] = newVar->id();
483 } else {
484 x[j] = (*al_x)[j];
485 }
486 }
487 Val d = LinearTraits<Lit>::eval(_env, call->arg(2));
488
489 simplify_lin<Lit>(coeffs, x, d);
490 if (coeffs.empty()) {
491 i->remove();
492 _env.counters.linDel++;
493 return;
494 }
495 std::vector<Expression*> coeffs_e(coeffs.size());
496 std::vector<Expression*> x_e(coeffs.size());
497 for (unsigned int j = 0; j < coeffs.size(); j++) {
498 coeffs_e[j] = Lit::a(coeffs[j]);
499 x_e[j] = x[j]();
500 Expression* decl = follow_id_to_decl(x_e[j]);
501 if (decl && decl->cast<VarDecl>() == newVar) {
502 storeItem(newVar, i);
503 }
504 }
505
506 if (auto* arg0 = call->arg(0)->dynamicCast<ArrayLit>()) {
507 arg0->setVec(coeffs_e);
508 } else {
509 auto* al_c_new = new ArrayLit(al_c->loc().introduce(), coeffs_e);
510 al_c_new->type(al_c->type());
511 call->arg(0, al_c_new);
512 }
513
514 if (auto* arg1 = call->arg(1)->dynamicCast<ArrayLit>()) {
515 arg1->setVec(x_e);
516 } else {
517 auto* al_x_new = new ArrayLit(al_x->loc().introduce(), x_e);
518 al_x_new->type(al_x->type());
519 call->arg(1, al_x_new);
520 }
521
522 call->arg(2, Lit::a(d));
523
524 // Add new occurences
525 CollectOccurrencesE ce(_env.varOccurrences, i);
526 top_down(ce, ci->e());
527}
528
529bool LECompressor::eqBounds(Expression* a, Expression* b) {
530 // TODO: (To optimise) Check lb(lhs) >= lb(rhs) and enforce ub(lhs) <= ub(rhs)
531 IntSetVal* dom_a = nullptr;
532 IntSetVal* dom_b = nullptr;
533
534 if (auto* a_decl = follow_id_to_decl(a)->dynamicCast<VarDecl>()) {
535 if (a_decl->ti()->domain() != nullptr) {
536 dom_a = eval_intset(_env, a_decl->ti()->domain());
537 }
538 } else {
539 assert(a->dynamicCast<IntLit>());
540 auto* a_val = a->cast<IntLit>();
541 dom_a = IntSetVal::a(a_val->v(), a_val->v());
542 }
543
544 if (auto* b_decl = follow_id_to_decl(b)->dynamicCast<VarDecl>()) {
545 if (b_decl->ti()->domain() != nullptr) {
546 dom_b = eval_intset(_env, b_decl->ti()->domain());
547 }
548 } else {
549 assert(b->dynamicCast<IntLit>());
550 auto* b_val = b->cast<IntLit>();
551 dom_b = IntSetVal::a(b_val->v(), b_val->v());
552 }
553
554 return ((dom_a != nullptr) && (dom_b != nullptr) && (dom_a->min() == dom_b->min()) &&
555 (dom_a->max() == dom_b->max())) ||
556 ((dom_a == nullptr) && (dom_b == nullptr));
557}
558
559} // namespace MiniZinc