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