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