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 * Guido Tack <guido.tack@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/astiterator.hh>
13#include <minizinc/output.hh>
14#include <minizinc/typecheck.hh>
15
16namespace MiniZinc {
17
18namespace {
19
20// Test if all parameters and the return type are par
21bool is_completely_par(EnvI& env, FunctionI* fi, const std::vector<Type>& tv) {
22 if (fi->e() != nullptr) {
23 // This is not a builtin, so check parameters
24 for (int i = 0; i < fi->paramCount(); i++) {
25 if (fi->param(i)->type().isvar()) {
26 return false;
27 }
28 }
29 }
30 return fi->rtype(env, tv, false).isPar();
31}
32
33} // namespace
34
35void check_output_par_fn(EnvI& env, Call* rhs) {
36 std::vector<Type> tv(rhs->argCount());
37 for (unsigned int i = rhs->argCount(); (i--) != 0U;) {
38 tv[i] = rhs->arg(i)->type();
39 tv[i].ti(Type::TI_PAR);
40 }
41 FunctionI* decl = env.output->matchFn(env, rhs->id(), tv, false);
42 if (decl == nullptr) {
43 FunctionI* origdecl = env.model->matchFn(env, rhs->id(), tv, false);
44 if (origdecl == nullptr || !is_completely_par(env, origdecl, tv)) {
45 std::ostringstream ss;
46 ss << "function " << rhs->id() << " is used in output, par version needed";
47 throw FlatteningError(env, rhs->loc(), ss.str());
48 }
49 if (!origdecl->fromStdLib()) {
50 decl = copy(env, env.cmap, origdecl)->cast<FunctionI>();
51 CollectOccurrencesE ce(env.outputVarOccurrences, decl);
52 top_down(ce, decl->e());
53 top_down(ce, decl->ti());
54 for (unsigned int i = decl->paramCount(); (i--) != 0U;) {
55 top_down(ce, decl->param(i));
56 }
57 (void)env.output->registerFn(env, decl, true);
58 env.output->addItem(decl);
59 } else {
60 decl = origdecl;
61 }
62 }
63 rhs->type(decl->rtype(env, tv, false));
64 rhs->decl(decl);
65}
66
67bool cannot_use_rhs_for_output(EnvI& env, Expression* e,
68 std::unordered_set<FunctionI*>& seen_functions) {
69 if (e == nullptr) {
70 return true;
71 }
72
73 class V : public EVisitor {
74 public:
75 EnvI& env;
76 std::unordered_set<FunctionI*>& seenFunctions;
77 bool success;
78 V(EnvI& env0, std::unordered_set<FunctionI*>& seenFunctions0)
79 : env(env0), seenFunctions(seenFunctions0), success(true) {}
80 /// Visit anonymous variable
81 void vAnonVar(const AnonVar& /*v*/) { success = false; }
82 /// Visit array literal
83 void vArrayLit(const ArrayLit& /*al*/) {}
84 /// Visit array access
85 void vArrayAccess(const ArrayAccess& /*aa*/) {}
86 /// Visit array comprehension
87 void vComprehension(const Comprehension& /*c*/) {}
88 /// Visit if-then-else
89 void vITE(const ITE& /*ite*/) {}
90 /// Visit binary operator
91 void vBinOp(const BinOp& /*bo*/) {}
92 /// Visit unary operator
93 void vUnOp(const UnOp& /*uo*/) {}
94 /// Visit call
95 void vCall(Call& c) {
96 std::vector<Type> tv(c.argCount());
97 for (unsigned int i = c.argCount(); (i--) != 0U;) {
98 tv[i] = c.arg(i)->type();
99 tv[i].ti(Type::TI_PAR);
100 }
101 FunctionI* decl = env.output->matchFn(env, c.id(), tv, false);
102 Type t;
103 if (decl == nullptr) {
104 FunctionI* origdecl = env.model->matchFn(env, c.id(), tv, false);
105 if (origdecl == nullptr) {
106 std::ostringstream ss;
107 ss << "function " << c.id() << " is used in output, par version needed";
108 throw FlatteningError(env, c.loc(), ss.str());
109 }
110 bool seen = (seenFunctions.find(origdecl) != seenFunctions.end());
111 if (seen) {
112 success = false;
113 } else {
114 seenFunctions.insert(origdecl);
115 if ((origdecl->e() != nullptr) &&
116 cannot_use_rhs_for_output(env, origdecl->e(), seenFunctions)) {
117 success = false;
118 } else {
119 if (!origdecl->fromStdLib()) {
120 decl = copy(env, env.cmap, origdecl)->cast<FunctionI>();
121 CollectOccurrencesE ce(env.outputVarOccurrences, decl);
122 top_down(ce, decl->e());
123 top_down(ce, decl->ti());
124 for (unsigned int i = decl->paramCount(); (i--) != 0U;) {
125 top_down(ce, decl->param(i));
126 }
127 (void)env.output->registerFn(env, decl, true);
128 env.output->addItem(decl);
129 output_vardecls(env, origdecl, decl->e());
130 output_vardecls(env, origdecl, decl->ti());
131 } else {
132 decl = origdecl;
133 }
134 c.decl(decl);
135 }
136 }
137 }
138 if (success) {
139 t = decl->rtype(env, tv, false);
140 if (!t.isPar()) {
141 success = false;
142 }
143 }
144 }
145 void vId(const Id& /*id*/) {}
146 /// Visit let
147 void vLet(const Let& /*let*/) { success = false; }
148 /// Visit variable declaration
149 void vVarDecl(const VarDecl& /*vd*/) {}
150 /// Visit type inst
151 void vTypeInst(const TypeInst& /*ti*/) {}
152 /// Visit TIId
153 void vTIId(const TIId& /*tiid*/) {}
154 /// Determine whether to enter node
155 bool enter(Expression* /*e*/) const { return success; }
156 } _v(env, seen_functions);
157 top_down(_v, e);
158
159 return !_v.success;
160}
161
162bool cannot_use_rhs_for_output(EnvI& env, Expression* e) {
163 std::unordered_set<FunctionI*> seen_functions;
164 return cannot_use_rhs_for_output(env, e, seen_functions);
165}
166
167void remove_is_output(VarDecl* vd) {
168 if (vd == nullptr) {
169 return;
170 }
171 vd->ann().remove(constants().ann.output_var);
172 vd->ann().removeCall(constants().ann.output_array);
173}
174
175void copy_output(EnvI& e) {
176 struct CopyOutput : public EVisitor {
177 EnvI& env;
178 CopyOutput(EnvI& env0) : env(env0) {}
179 static void vId(Id& _id) { _id.decl(_id.decl()->flat()); }
180 void vCall(Call& c) {
181 std::vector<Type> tv(c.argCount());
182 for (unsigned int i = c.argCount(); (i--) != 0U;) {
183 tv[i] = c.arg(i)->type();
184 tv[i].ti(Type::TI_PAR);
185 }
186 FunctionI* decl = c.decl();
187 if (!decl->fromStdLib()) {
188 env.flatAddItem(decl);
189 }
190 }
191 };
192
193 if (OutputI* oi = e.model->outputItem()) {
194 GCLock lock;
195 auto* noi = copy(e, oi)->cast<OutputI>();
196 CopyOutput co(e);
197 top_down(co, noi->e());
198 e.flatAddItem(noi);
199 }
200}
201
202void cleanup_output(EnvI& env) {
203 for (auto& i : *env.output) {
204 if (auto* vdi = i->dynamicCast<VarDeclI>()) {
205 vdi->e()->flat(nullptr);
206 }
207 }
208}
209
210void make_par(EnvI& env, Expression* e) {
211 class OutputJSON : public EVisitor {
212 public:
213 EnvI& env;
214 OutputJSON(EnvI& env0) : env(env0) {}
215 void vCall(Call& c) {
216 if (c.id() == "outputJSON") {
217 bool outputObjective = (c.argCount() == 1 && eval_bool(env, c.arg(0)));
218 c.id(ASTString("array1d"));
219 Expression* json =
220 copy(env, env.cmap, create_json_output(env, outputObjective, false, false));
221 std::vector<Expression*> new_args({json});
222 new_args[0]->type(Type::parstring(1));
223 c.args(new_args);
224 }
225 }
226 } _outputJSON(env);
227 top_down(_outputJSON, e);
228 class Par : public EVisitor {
229 public:
230 /// Visit variable declaration
231 static void vVarDecl(VarDecl& vd) { vd.ti()->type(vd.type()); }
232 /// Determine whether to enter node
233 static bool enter(Expression* e) {
234 Type t = e->type();
235 t.ti(Type::TI_PAR);
236 t.cv(false);
237 e->type(t);
238 return true;
239 }
240 } _par;
241 top_down(_par, e);
242 class Decls : public EVisitor {
243 public:
244 EnvI& env;
245 Decls(EnvI& env0) : env(env0) {}
246 void vCall(Call& c) {
247 if (c.id() == "format" || c.id() == "show" || c.id() == "showDzn" || c.id() == "showJSON") {
248 unsigned int enumId = c.arg(c.argCount() - 1)->type().enumId();
249 if (enumId != 0U && c.arg(c.argCount() - 1)->type().dim() != 0) {
250 const std::vector<unsigned int>& enumIds = env.getArrayEnum(enumId);
251 enumId = enumIds[enumIds.size() - 1];
252 }
253 if (enumId > 0) {
254 GCLock lock;
255 Expression* obj = c.arg(c.argCount() - 1);
256 Id* ti_id = env.getEnum(enumId)->e()->id();
257 std::string enumName = create_enum_to_string_name(ti_id, "_toString_");
258 bool is_json = c.id() == "showJSON";
259 const int dimensions = obj->type().dim();
260 if (is_json && dimensions > 1) {
261 // Create generators for dimensions selection
262 std::vector<Expression*> slice_dimensions(dimensions);
263 std::vector<Generator> generators;
264 generators.reserve(dimensions - 1);
265 auto* idx_ti = new TypeInst(Location().introduce(), Type::parint());
266 for (int i = 0; i < dimensions - 1; ++i) {
267 auto* idx_i = new VarDecl(Location().introduce(), idx_ti, env.genId());
268 idx_i->toplevel(false);
269 Call* index_set_xx = new Call(
270 Location().introduce(),
271 "index_set_" + std::to_string(i + 1) + "of" + std::to_string(dimensions), {obj});
272 index_set_xx->type(Type::parsetint());
273 generators.push_back(Generator({idx_i}, index_set_xx, nullptr));
274 slice_dimensions[i] =
275 new BinOp(Location().introduce(), idx_i->id(), BOT_DOTDOT, idx_i->id());
276 slice_dimensions[i]->type(Type::parsetint());
277 }
278
279 // Construct innermost slicing operation
280 Call* index_set_n = new Call(
281 Location().introduce(),
282 "index_set_" + std::to_string(dimensions) + "of" + std::to_string(dimensions),
283 {obj});
284 index_set_n->type(Type::parsetint());
285 slice_dimensions[dimensions - 1] = index_set_n;
286 auto* al_slice_dim = new ArrayLit(Location().introduce(), slice_dimensions);
287 al_slice_dim->type(Type::parsetint(1));
288
289 auto* slice_call =
290 new Call(Location().introduce(), "slice_1d", {obj, al_slice_dim, index_set_n});
291 Type tt = obj->type();
292 tt.dim(1);
293 slice_call->type(tt);
294 Call* _toString_ENUM =
295 new Call(Location().introduce(), enumName,
296 {slice_call, constants().boollit(false), constants().boollit(true)});
297 _toString_ENUM->type(Type::parstring());
298
299 // Build multi-level JSON Array string
300 auto* comma = new StringLit(Location().introduce(), ", ");
301 comma->type(Type::parstring());
302 auto join = [&](Expression* expr, Generator gen) -> Expression* {
303 Generators generators;
304 generators.g.push_back(gen);
305 auto* comp = new Comprehension(Location().introduce(), expr, generators, false);
306 comp->type(Type::parstring(1));
307 Call* cc = new Call(Location().introduce(), "join", {comma, comp});
308 cc->type(Type::parstring());
309 return cc;
310 };
311 auto* sl_open = new StringLit(Location().introduce(), "[");
312 sl_open->type(Type::parstring());
313 auto* sl_close = new StringLit(Location().introduce(), "]");
314 sl_close->type(Type::parstring());
315
316 auto* al_concat = new ArrayLit(
317 Location().introduce(),
318 std::vector<Expression*>(
319 {sl_open, join(_toString_ENUM, generators[dimensions - 2]), sl_close}));
320 al_concat->type(Type::parstring(1));
321 for (int i = dimensions - 3; i >= 0; --i) {
322 Call* concat = new Call(Location().introduce(), "concat", {al_concat});
323 concat->type(Type::parstring());
324 al_concat = new ArrayLit(
325 Location().introduce(),
326 std::vector<Expression*>({sl_open, join(concat, generators[i]), sl_close}));
327 al_concat->type(Type::parstring(1));
328 }
329 std::vector<Expression*> args = {al_concat};
330 c.args(args);
331 c.id(ASTString("concat"));
332 } else {
333 std::vector<Expression*> args = {obj, constants().boollit(c.id() == "showDzn"),
334 constants().boollit(is_json)};
335 c.args(args);
336 c.id(ASTString(enumName));
337 }
338 }
339 if (c.id() == "showDzn" || (c.id() == "showJSON" && enumId > 0)) {
340 c.id(constants().ids.show);
341 }
342 }
343 c.decl(env.model->matchFn(env, &c, false));
344 }
345 void vBinOp(BinOp& bo) {
346 std::vector<Expression*> args = {bo.lhs(), bo.rhs()};
347 bo.decl(env.model->matchFn(env, bo.opToString(), args, false));
348 }
349 void vUnop(UnOp& uo) {
350 std::vector<Expression*> args = {uo.e()};
351 uo.decl(env.model->matchFn(env, uo.opToString(), args, false));
352 }
353 } _decls(env);
354 top_down(_decls, e);
355}
356
357void check_rename_var(EnvI& e, VarDecl* vd) {
358 if (vd->id()->idn() != vd->flat()->id()->idn()) {
359 auto* vd_rename_ti = copy(e, e.cmap, vd->ti())->cast<TypeInst>();
360 auto* vd_rename =
361 new VarDecl(Location().introduce(), vd_rename_ti, vd->flat()->id()->idn(), nullptr);
362 vd_rename->flat(vd->flat());
363 make_par(e, vd_rename);
364 vd->e(vd_rename->id());
365 e.output->addItem(new VarDeclI(Location().introduce(), vd_rename));
366 }
367}
368
369class ClearAnnotations {
370public:
371 /// Push all elements of \a v onto \a stack
372 template <class E>
373 static void pushVec(std::vector<Expression*>& stack, ASTExprVec<E> v) {
374 for (unsigned int i = 0; i < v.size(); i++) {
375 stack.push_back(v[i]);
376 }
377 }
378
379 static void run(Expression* root) {
380 std::vector<Expression*> stack;
381 stack.push_back(root);
382 while (!stack.empty()) {
383 Expression* e = stack.back();
384 stack.pop_back();
385 if (e == nullptr) {
386 continue;
387 }
388 e->ann().clear();
389 switch (e->eid()) {
390 case Expression::E_INTLIT:
391 case Expression::E_FLOATLIT:
392 case Expression::E_BOOLLIT:
393 case Expression::E_STRINGLIT:
394 case Expression::E_ID:
395 case Expression::E_ANON:
396 case Expression::E_TIID:
397 break;
398 case Expression::E_SETLIT:
399 pushVec(stack, e->template cast<SetLit>()->v());
400 break;
401 case Expression::E_ARRAYLIT:
402 for (unsigned int i = 0; i < e->cast<ArrayLit>()->size(); i++) {
403 stack.push_back((*e->cast<ArrayLit>())[i]);
404 }
405 break;
406 case Expression::E_ARRAYACCESS:
407 pushVec(stack, e->template cast<ArrayAccess>()->idx());
408 stack.push_back(e->template cast<ArrayAccess>()->v());
409 break;
410 case Expression::E_COMP: {
411 auto* comp = e->template cast<Comprehension>();
412 for (unsigned int i = comp->numberOfGenerators(); (i--) != 0U;) {
413 stack.push_back(comp->where(i));
414 stack.push_back(comp->in(i));
415 for (unsigned int j = comp->numberOfDecls(i); (j--) != 0U;) {
416 stack.push_back(comp->decl(i, j));
417 }
418 }
419 stack.push_back(comp->e());
420 } break;
421 case Expression::E_ITE: {
422 ITE* ite = e->template cast<ITE>();
423 stack.push_back(ite->elseExpr());
424 for (int i = 0; i < ite->size(); i++) {
425 stack.push_back(ite->ifExpr(i));
426 stack.push_back(ite->thenExpr(i));
427 }
428 } break;
429 case Expression::E_BINOP:
430 stack.push_back(e->template cast<BinOp>()->rhs());
431 stack.push_back(e->template cast<BinOp>()->lhs());
432 break;
433 case Expression::E_UNOP:
434 stack.push_back(e->template cast<UnOp>()->e());
435 break;
436 case Expression::E_CALL:
437 for (unsigned int i = 0; i < e->template cast<Call>()->argCount(); i++) {
438 stack.push_back(e->template cast<Call>()->arg(i));
439 }
440 break;
441 case Expression::E_VARDECL:
442 stack.push_back(e->template cast<VarDecl>()->e());
443 stack.push_back(e->template cast<VarDecl>()->ti());
444 break;
445 case Expression::E_LET:
446 stack.push_back(e->template cast<Let>()->in());
447 pushVec(stack, e->template cast<Let>()->let());
448 break;
449 case Expression::E_TI:
450 stack.push_back(e->template cast<TypeInst>()->domain());
451 pushVec(stack, e->template cast<TypeInst>()->ranges());
452 break;
453 }
454 }
455 }
456};
457
458void output_vardecls(EnvI& env, Item* ci, Expression* e) {
459 class O : public EVisitor {
460 public:
461 EnvI& env;
462 Item* ci;
463 O(EnvI& env0, Item* ci0) : env(env0), ci(ci0) {}
464 void vId(Id& id) {
465 if (&id == constants().absent) {
466 return;
467 }
468 if (!id.decl()->toplevel()) {
469 return;
470 }
471 VarDecl* vd = id.decl();
472 VarDecl* reallyFlat = vd->flat();
473 while (reallyFlat != nullptr && reallyFlat != reallyFlat->flat()) {
474 reallyFlat = reallyFlat->flat();
475 }
476 auto idx = reallyFlat != nullptr ? env.outputFlatVarOccurrences.idx.find(reallyFlat->id())
477 : env.outputFlatVarOccurrences.idx.end();
478 auto idx2 = env.outputVarOccurrences.idx.find(vd->id());
479 if (idx == env.outputFlatVarOccurrences.idx.end() &&
480 idx2 == env.outputVarOccurrences.idx.end()) {
481 auto* nvi = new VarDeclI(Location().introduce(), copy(env, env.cmap, vd)->cast<VarDecl>());
482 Type t = nvi->e()->ti()->type();
483 if (t.ti() != Type::TI_PAR) {
484 t.ti(Type::TI_PAR);
485 }
486 make_par(env, nvi->e());
487 nvi->e()->ti()->domain(nullptr);
488 nvi->e()->flat(vd->flat());
489 ClearAnnotations::run(nvi->e());
490 nvi->e()->introduced(false);
491 if (reallyFlat != nullptr) {
492 env.outputFlatVarOccurrences.addIndex(reallyFlat, static_cast<int>(env.output->size()));
493 }
494 env.outputVarOccurrences.addIndex(nvi, static_cast<int>(env.output->size()));
495 env.outputVarOccurrences.add(nvi->e(), ci);
496 env.output->addItem(nvi);
497
498 IdMap<KeepAlive>::iterator it;
499 if ((it = env.reverseMappers.find(nvi->e()->id())) != env.reverseMappers.end()) {
500 Call* rhs = copy(env, env.cmap, it->second())->cast<Call>();
501 check_output_par_fn(env, rhs);
502 output_vardecls(env, nvi, it->second());
503 nvi->e()->e(rhs);
504 } else if ((reallyFlat != nullptr) && cannot_use_rhs_for_output(env, reallyFlat->e())) {
505 assert(nvi->e()->flat());
506 nvi->e()->e(nullptr);
507 if (nvi->e()->type().dim() == 0) {
508 reallyFlat->addAnnotation(constants().ann.output_var);
509 } else {
510 std::vector<Expression*> args(reallyFlat->e()->type().dim());
511 for (unsigned int i = 0; i < args.size(); i++) {
512 if (nvi->e()->ti()->ranges()[i]->domain() == nullptr) {
513 args[i] = new SetLit(Location().introduce(),
514 eval_intset(env, reallyFlat->ti()->ranges()[i]->domain()));
515 } else {
516 args[i] = new SetLit(Location().introduce(),
517 eval_intset(env, nvi->e()->ti()->ranges()[i]->domain()));
518 }
519 }
520 auto* al = new ArrayLit(Location().introduce(), args);
521 args.resize(1);
522 args[0] = al;
523 reallyFlat->addAnnotation(
524 new Call(Location().introduce(), constants().ann.output_array, args));
525 }
526 check_rename_var(env, nvi->e());
527 } else {
528 output_vardecls(env, nvi, nvi->e()->ti());
529 output_vardecls(env, nvi, nvi->e()->e());
530 }
531 CollectOccurrencesE ce(env.outputVarOccurrences, nvi);
532 top_down(ce, nvi->e());
533 }
534 }
535 } _o(env, ci);
536 top_down(_o, e);
537}
538
539void process_deletions(EnvI& e) {
540 std::vector<VarDecl*> deletedVarDecls;
541 for (unsigned int i = 0; i < e.output->size(); i++) {
542 if (auto* vdi = (*e.output)[i]->dynamicCast<VarDeclI>()) {
543 if (!vdi->removed() && e.outputVarOccurrences.occurrences(vdi->e()) == 0 &&
544 !vdi->e()->ann().contains(constants().ann.mzn_check_var) &&
545 !(vdi->e()->id()->idn() == -1 && (vdi->e()->id()->v() == "_mzn_solution_checker" ||
546 vdi->e()->id()->v() == "_mzn_stats_checker"))) {
547 CollectDecls cd(e.outputVarOccurrences, deletedVarDecls, vdi);
548 top_down(cd, vdi->e()->e());
549 remove_is_output(vdi->e()->flat());
550 if (e.outputVarOccurrences.find(vdi->e()) != -1) {
551 e.outputVarOccurrences.remove(vdi->e());
552 }
553 vdi->remove();
554 }
555 }
556 }
557 while (!deletedVarDecls.empty()) {
558 VarDecl* cur = deletedVarDecls.back();
559 deletedVarDecls.pop_back();
560 if (e.outputVarOccurrences.occurrences(cur) == 0) {
561 auto cur_idx = e.outputVarOccurrences.idx.find(cur->id());
562 if (cur_idx != e.outputVarOccurrences.idx.end()) {
563 auto* vdi = (*e.output)[cur_idx->second]->cast<VarDeclI>();
564 if (!vdi->removed()) {
565 CollectDecls cd(e.outputVarOccurrences, deletedVarDecls, vdi);
566 top_down(cd, cur->e());
567 remove_is_output(vdi->e()->flat());
568 if (e.outputVarOccurrences.find(vdi->e()) != -1) {
569 e.outputVarOccurrences.remove(vdi->e());
570 }
571 vdi->remove();
572 }
573 }
574 }
575 }
576
577 for (auto& it : e.outputVarOccurrences.itemMap) {
578 std::vector<Item*> toRemove;
579 for (auto* iit : it.second) {
580 if (iit->removed()) {
581 toRemove.push_back(iit);
582 }
583 }
584 for (auto& i : toRemove) {
585 it.second.erase(i);
586 }
587 }
588}
589
590void create_dzn_output_item(EnvI& e, bool outputObjective, bool includeOutputItem, bool hasChecker,
591 bool outputForChecker) {
592 std::vector<Expression*> outputVars;
593
594 class DZNOVisitor : public ItemVisitor {
595 protected:
596 EnvI& _e;
597 bool _outputObjective;
598 bool _includeOutputItem;
599 bool _outputForChecker;
600 std::vector<Expression*>& _outputVars;
601 bool _hadAddToOutput;
602
603 public:
604 DZNOVisitor(EnvI& e, bool outputObjective, bool includeOutputItem, bool outputForChecker,
605 std::vector<Expression*>& outputVars)
606 : _e(e),
607 _outputObjective(outputObjective),
608 _includeOutputItem(includeOutputItem),
609 _outputForChecker(outputForChecker),
610 _outputVars(outputVars),
611 _hadAddToOutput(false) {}
612 void vVarDeclI(VarDeclI* vdi) {
613 VarDecl* vd = vdi->e();
614 bool process_var = false;
615 if (_outputForChecker) {
616 if (vd->ann().contains(constants().ann.mzn_check_var)) {
617 process_var = true;
618 }
619 } else {
620 if (_outputObjective && vd->id()->idn() == -1 && vd->id()->v() == "_objective") {
621 process_var = true;
622 } else {
623 if (vd->ann().contains(constants().ann.add_to_output)) {
624 if (!_hadAddToOutput) {
625 _outputVars.clear();
626 }
627 _hadAddToOutput = true;
628 process_var = true;
629 } else {
630 if (!_hadAddToOutput) {
631 process_var = false;
632 if (vd->type().isvar()) {
633 if (vd->e() != nullptr) {
634 if (auto* al = vd->e()->dynamicCast<ArrayLit>()) {
635 for (unsigned int i = 0; i < al->size(); i++) {
636 if ((*al)[i]->isa<AnonVar>()) {
637 process_var = true;
638 break;
639 }
640 }
641 } else if (vd->ann().contains(constants().ann.rhs_from_assignment)) {
642 process_var = true;
643 }
644 } else {
645 process_var = true;
646 }
647 }
648 }
649 }
650 }
651 }
652 if (process_var) {
653 std::ostringstream s;
654 s << vd->id()->str() << " = ";
655 bool needArrayXd = false;
656 if (vd->type().dim() > 0) {
657 ArrayLit* al = nullptr;
658 if (!vd->ann().contains(constants().ann.output_only)) {
659 if ((vd->flat() != nullptr) && (vd->flat()->e() != nullptr)) {
660 al = eval_array_lit(_e, vd->flat()->e());
661 } else if (vd->e() != nullptr) {
662 al = eval_array_lit(_e, vd->e());
663 }
664 }
665 if (al == nullptr || al->size() > 0) {
666 needArrayXd = true;
667 s << "array" << vd->type().dim() << "d(";
668 for (int i = 0; i < vd->type().dim(); i++) {
669 unsigned int enumId =
670 (vd->type().enumId() != 0 ? _e.getArrayEnum(vd->type().enumId())[i] : 0);
671 if (enumId != 0) {
672 s << _e.getEnum(enumId)->e()->id()->str() << ", ";
673 } else if (al != nullptr) {
674 s << al->min(i) << ".." << al->max(i) << ", ";
675 } else if (vd->ti()->ranges()[i]->domain() != nullptr) {
676 IntSetVal* idxset = eval_intset(_e, vd->ti()->ranges()[i]->domain());
677 s << *idxset << ", ";
678 } else {
679 // Don't know index set range - have to compute in solns2out
680 auto* sl = new StringLit(Location().introduce(), s.str());
681 _outputVars.push_back(sl);
682
683 std::string index_set_fn = "index_set";
684 if (vd->type().dim() > 1) {
685 index_set_fn +=
686 "_" + std::to_string(i + 1) + "of" + std::to_string(vd->type().dim());
687 }
688 auto* index_set_xx = new Call(Location().introduce(), index_set_fn, {vd->id()});
689 index_set_xx->type(Type::parsetint());
690 auto* i_fi = _e.model->matchFn(_e, index_set_xx, false);
691 assert(i_fi);
692 index_set_xx->decl(i_fi);
693
694 auto* show = new Call(Location().introduce(), constants().ids.show, {index_set_xx});
695 show->type(Type::parstring());
696 FunctionI* s_fi = _e.model->matchFn(_e, show, false);
697 assert(s_fi);
698 show->decl(s_fi);
699
700 _outputVars.push_back(show);
701 s.str(", ");
702 }
703 }
704 }
705 }
706 auto* sl = new StringLit(Location().introduce(), s.str());
707 _outputVars.push_back(sl);
708
709 std::vector<Expression*> showArgs(1);
710 showArgs[0] = vd->id();
711 Call* show = new Call(Location().introduce(), ASTString("showDzn"), showArgs);
712 show->type(Type::parstring());
713 FunctionI* fi = _e.model->matchFn(_e, show, false);
714 assert(fi);
715 show->decl(fi);
716 _outputVars.push_back(show);
717 std::string ends = needArrayXd ? ")" : "";
718 ends += ";\n";
719 auto* eol = new StringLit(Location().introduce(), ends);
720 _outputVars.push_back(eol);
721 }
722 }
723 void vOutputI(OutputI* oi) {
724 if (_includeOutputItem) {
725 _outputVars.push_back(new StringLit(Location().introduce(), "_output = "));
726 Call* concat = new Call(Location().introduce(), ASTString("concat"), {oi->e()});
727 concat->type(Type::parstring());
728 FunctionI* fi = _e.model->matchFn(_e, concat, false);
729 assert(fi);
730 concat->decl(fi);
731 Call* show = new Call(Location().introduce(), ASTString("showDzn"), {concat});
732 show->type(Type::parstring());
733 fi = _e.model->matchFn(_e, show, false);
734 assert(fi);
735 show->decl(fi);
736 _outputVars.push_back(show);
737 _outputVars.push_back(new StringLit(Location().introduce(), ";\n"));
738 }
739
740 oi->remove();
741 }
742 } dznov(e, outputObjective, includeOutputItem, outputForChecker, outputVars);
743
744 iter_items(dznov, e.model);
745
746 if (hasChecker && !outputForChecker) {
747 outputVars.push_back(new StringLit(Location().introduce(), "_checker = "));
748 auto* checker_output = new Call(Location().introduce(), ASTString("showCheckerOutput"), {});
749 checker_output->type(Type::parstring());
750 FunctionI* fi = e.model->matchFn(e, checker_output, false);
751 assert(fi);
752 checker_output->decl(fi);
753 auto* show = new Call(Location().introduce(), ASTString("showDzn"), {checker_output});
754 show->type(Type::parstring());
755 fi = e.model->matchFn(e, show, false);
756 assert(fi);
757 show->decl(fi);
758 outputVars.push_back(show);
759 outputVars.push_back(new StringLit(Location().introduce(), ";\n"));
760 }
761
762 auto* newOutputItem =
763 new OutputI(Location().introduce(), new ArrayLit(Location().introduce(), outputVars));
764 e.model->addItem(newOutputItem);
765}
766
767ArrayLit* create_json_output(EnvI& e, bool outputObjective, bool includeOutputItem,
768 bool hasChecker) {
769 std::vector<Expression*> outputVars;
770 outputVars.push_back(new StringLit(Location().introduce(), "{\n"));
771
772 class JSONOVisitor : public ItemVisitor {
773 protected:
774 EnvI& _e;
775 bool _outputObjective;
776 bool _includeOutputItem;
777 std::vector<Expression*>& _outputVars;
778 bool _hadAddToOutput;
779
780 public:
781 bool firstVar;
782 JSONOVisitor(EnvI& e, bool outputObjective, bool includeOutputItem,
783 std::vector<Expression*>& outputVars)
784 : _e(e),
785 _outputObjective(outputObjective),
786 _outputVars(outputVars),
787 _includeOutputItem(includeOutputItem),
788 _hadAddToOutput(false),
789 firstVar(true) {}
790 void vVarDeclI(VarDeclI* vdi) {
791 VarDecl* vd = vdi->e();
792 bool process_var = false;
793 if (_outputObjective && vd->id()->idn() == -1 && vd->id()->v() == "_objective") {
794 process_var = true;
795 } else {
796 if (vd->ann().contains(constants().ann.add_to_output)) {
797 if (!_hadAddToOutput) {
798 _outputVars.clear();
799 _outputVars.push_back(new StringLit(Location().introduce(), "{\n"));
800 firstVar = true;
801 }
802 _hadAddToOutput = true;
803 process_var = true;
804 } else {
805 if (!_hadAddToOutput) {
806 process_var =
807 vd->type().isvar() &&
808 (vd->e() == nullptr || vd->ann().contains(constants().ann.rhs_from_assignment));
809 }
810 }
811 }
812 if (process_var) {
813 std::ostringstream s;
814 if (firstVar) {
815 firstVar = false;
816 } else {
817 s << ",\n";
818 }
819 s << " \"" << vd->id()->str() << "\""
820 << " : ";
821 auto* sl = new StringLit(Location().introduce(), s.str());
822 _outputVars.push_back(sl);
823
824 std::vector<Expression*> showArgs(1);
825 showArgs[0] = vd->id();
826 Call* show = new Call(Location().introduce(), "showJSON", showArgs);
827 show->type(Type::parstring());
828 FunctionI* fi = _e.model->matchFn(_e, show, false);
829 assert(fi);
830 show->decl(fi);
831 _outputVars.push_back(show);
832 }
833 }
834 void vOutputI(OutputI* oi) {
835 if (_includeOutputItem) {
836 std::ostringstream s;
837 if (firstVar) {
838 firstVar = false;
839 } else {
840 s << ",\n";
841 }
842 s << " \"_output\""
843 << " : ";
844 auto* sl = new StringLit(Location().introduce(), s.str());
845 _outputVars.push_back(sl);
846 Call* concat = new Call(Location().introduce(), ASTString("concat"), {oi->e()});
847 concat->type(Type::parstring());
848 FunctionI* fi = _e.model->matchFn(_e, concat, false);
849 assert(fi);
850 concat->decl(fi);
851 Call* show = new Call(Location().introduce(), ASTString("showJSON"), {concat});
852 show->type(Type::parstring());
853 fi = _e.model->matchFn(_e, show, false);
854 assert(fi);
855 show->decl(fi);
856 _outputVars.push_back(show);
857 }
858
859 oi->remove();
860 }
861 } jsonov(e, outputObjective, includeOutputItem, outputVars);
862
863 iter_items(jsonov, e.model);
864
865 if (hasChecker) {
866 std::ostringstream s;
867 if (jsonov.firstVar) {
868 jsonov.firstVar = false;
869 } else {
870 s << ",\n";
871 }
872 s << " \"_checker\""
873 << " : ";
874 auto* sl = new StringLit(Location().introduce(), s.str());
875 outputVars.push_back(sl);
876 Call* checker_output = new Call(Location().introduce(), ASTString("showCheckerOutput"), {});
877 checker_output->type(Type::parstring());
878 FunctionI* fi = e.model->matchFn(e, checker_output, false);
879 assert(fi);
880 checker_output->decl(fi);
881 Call* show = new Call(Location().introduce(), ASTString("showJSON"), {checker_output});
882 show->type(Type::parstring());
883 fi = e.model->matchFn(e, show, false);
884 assert(fi);
885 show->decl(fi);
886 outputVars.push_back(show);
887 }
888
889 outputVars.push_back(new StringLit(Location().introduce(), "\n}\n"));
890 return new ArrayLit(Location().introduce(), outputVars);
891}
892void create_json_output_item(EnvI& e, bool outputObjective, bool includeOutputItem,
893 bool hasChecker) {
894 auto* newOutputItem =
895 new OutputI(Location().introduce(),
896 create_json_output(e, outputObjective, includeOutputItem, hasChecker));
897 e.model->addItem(newOutputItem);
898}
899
900void create_output(EnvI& e, FlatteningOptions::OutputMode outputMode, bool outputObjective,
901 bool includeOutputItem, bool hasChecker) {
902 // Create new output model
903 OutputI* outputItem = nullptr;
904 GCLock lock;
905
906 switch (outputMode) {
907 case FlatteningOptions::OUTPUT_DZN:
908 create_dzn_output_item(e, outputObjective, includeOutputItem, hasChecker, false);
909 break;
910 case FlatteningOptions::OUTPUT_JSON:
911 create_json_output_item(e, outputObjective, includeOutputItem, hasChecker);
912 break;
913 case FlatteningOptions::OUTPUT_CHECKER:
914 create_dzn_output_item(e, outputObjective, includeOutputItem, hasChecker, true);
915 break;
916 default:
917 if (e.model->outputItem() == nullptr) {
918 create_dzn_output_item(e, outputObjective, false, false, false);
919 }
920 break;
921 }
922
923 // Copy output item from model into output model
924 outputItem = copy(e, e.cmap, e.model->outputItem())->cast<OutputI>();
925 make_par(e, outputItem->e());
926 e.output->addItem(outputItem);
927
928 // Copy all function definitions that are required for output into the output model
929 class CollectFunctions : public EVisitor {
930 public:
931 EnvI& env;
932 CollectFunctions(EnvI& env0) : env(env0) {}
933 static bool enter(Expression* e) {
934 if (e->type().isvar()) {
935 Type t = e->type();
936 t.ti(Type::TI_PAR);
937 e->type(t);
938 }
939 return true;
940 }
941 void vId(Id& i) {
942 // Also collect functions from output_only variables we depend on
943 if ((i.decl() != nullptr) && i.decl()->ann().contains(constants().ann.output_only)) {
944 top_down(*this, i.decl()->e());
945 }
946 }
947 void vCall(Call& c) {
948 std::vector<Type> tv(c.argCount());
949 for (unsigned int i = c.argCount(); (i--) != 0U;) {
950 tv[i] = c.arg(i)->type();
951 tv[i].ti(Type::TI_PAR);
952 }
953 FunctionI* decl = env.output->matchFn(env, c.id(), tv, false);
954 FunctionI* origdecl = env.model->matchFn(env, c.id(), tv, false);
955 bool canReuseDecl = (decl != nullptr);
956 if (canReuseDecl && (origdecl != nullptr)) {
957 // Check if this is the exact same overloaded declaration as in the model
958 for (unsigned int i = 0; i < decl->paramCount(); i++) {
959 if (decl->param(i)->type() != origdecl->param(i)->type()) {
960 // no, the types don't match, so we have to copy the original decl
961 canReuseDecl = false;
962 break;
963 }
964 }
965 }
966 Type t;
967 if (!canReuseDecl) {
968 if (origdecl == nullptr || !is_completely_par(env, origdecl, tv)) {
969 std::ostringstream ss;
970 ss << "function " << c.id() << " is used in output, par version needed";
971 throw FlatteningError(env, c.loc(), ss.str());
972 }
973 if (!origdecl->fromStdLib()) {
974 auto* decl_copy = copy(env, env.cmap, origdecl)->cast<FunctionI>();
975 if (decl_copy != decl) {
976 decl = decl_copy;
977 (void)env.output->registerFn(env, decl, true);
978 env.output->addItem(decl);
979 if (decl->e() != nullptr) {
980 make_par(env, decl->e());
981 top_down(*this, decl->e());
982 }
983 CollectOccurrencesE ce(env.outputVarOccurrences, decl);
984 top_down(ce, decl->e());
985 top_down(ce, decl->ti());
986 for (unsigned int i = decl->paramCount(); (i--) != 0U;) {
987 top_down(ce, decl->param(i));
988 }
989 }
990 } else {
991 decl = origdecl;
992 }
993 }
994 c.decl(decl);
995 }
996 } _cf(e);
997 top_down(_cf, outputItem->e());
998
999 // If we are checking solutions using a checker model, all parameters of the checker model
1000 // have to be made available in the output model
1001 class OV1 : public ItemVisitor {
1002 public:
1003 EnvI& env;
1004 CollectFunctions& cf;
1005 OV1(EnvI& env0, CollectFunctions& cf0) : env(env0), cf(cf0) {}
1006 void vVarDeclI(VarDeclI* vdi) {
1007 if (vdi->e()->ann().contains(constants().ann.mzn_check_var)) {
1008 auto* output_vd = copy(env, env.cmap, vdi->e())->cast<VarDecl>();
1009 top_down(cf, output_vd);
1010 }
1011 }
1012 } _ov1(e, _cf);
1013 iter_items(_ov1, e.model);
1014
1015 // Copying the output item and the functions it depends on has created copies
1016 // of all dependent VarDecls. However the output model does not contain VarDeclIs for
1017 // these VarDecls yet. This iterator processes all variable declarations of the
1018 // original model, and if they were copied (i.e., if the output model depends on them),
1019 // the corresponding VarDeclI is created in the output model.
1020 class OV2 : public ItemVisitor {
1021 public:
1022 EnvI& env;
1023 OV2(EnvI& env0) : env(env0) {}
1024 void vVarDeclI(VarDeclI* vdi) {
1025 auto idx = env.outputVarOccurrences.idx.find(vdi->e()->id());
1026 if (idx != env.outputVarOccurrences.idx.end()) {
1027 return;
1028 }
1029 if (Expression* vd_e = env.cmap.find(vdi->e())) {
1030 // We found a copied VarDecl, now need to create a VarDeclI
1031 auto* vd = vd_e->cast<VarDecl>();
1032 auto* vdi_copy = copy(env, env.cmap, vdi)->cast<VarDeclI>();
1033
1034 Type t = vdi_copy->e()->ti()->type();
1035 t.ti(Type::TI_PAR);
1036 vdi_copy->e()->ti()->domain(nullptr);
1037 vdi_copy->e()->flat(vdi->e()->flat());
1038 bool isCheckVar = vdi_copy->e()->ann().contains(constants().ann.mzn_check_var);
1039 Call* checkVarEnum = vdi_copy->e()->ann().getCall(constants().ann.mzn_check_enum_var);
1040 vdi_copy->e()->ann().clear();
1041 if (isCheckVar) {
1042 vdi_copy->e()->ann().add(constants().ann.mzn_check_var);
1043 }
1044 if (checkVarEnum != nullptr) {
1045 vdi_copy->e()->ann().add(checkVarEnum);
1046 }
1047 vdi_copy->e()->introduced(false);
1048 IdMap<KeepAlive>::iterator it;
1049 if (!vdi->e()->type().isPar()) {
1050 if (vd->flat() == nullptr && vdi->e()->e() != nullptr && vdi->e()->e()->type().isPar()) {
1051 // Don't have a flat version of this variable, but the original has a right hand
1052 // side that is par, so we can use that.
1053 Expression* flate = eval_par(env, vdi->e()->e());
1054 output_vardecls(env, vdi_copy, flate);
1055 vd->e(flate);
1056 } else {
1057 vd = follow_id_to_decl(vd->id())->cast<VarDecl>();
1058 VarDecl* reallyFlat = vd->flat();
1059 while ((reallyFlat != nullptr) && reallyFlat != reallyFlat->flat()) {
1060 reallyFlat = reallyFlat->flat();
1061 }
1062 if (reallyFlat == nullptr) {
1063 // The variable doesn't have a flat version. This can only happen if
1064 // the original variable had type-inst var, but a right-hand-side that
1065 // was par, so follow_id_to_decl lead to a par variable.
1066 assert(vd->e() && vd->e()->type().isPar());
1067 Expression* flate = eval_par(env, vd->e());
1068 output_vardecls(env, vdi_copy, flate);
1069 vd->e(flate);
1070 } else if ((vd->flat()->e() != nullptr) && vd->flat()->e()->type().isPar()) {
1071 // We can use the right hand side of the flat version of this variable
1072 Expression* flate = copy(env, env.cmap, follow_id(reallyFlat->id()));
1073 output_vardecls(env, vdi_copy, flate);
1074 vd->e(flate);
1075 } else if ((it = env.reverseMappers.find(vd->id())) != env.reverseMappers.end()) {
1076 // Found a reverse mapper, so we need to add the mapping function to the
1077 // output model to map the FlatZinc value back to the model variable.
1078 Call* rhs = copy(env, env.cmap, it->second())->cast<Call>();
1079 check_output_par_fn(env, rhs);
1080 output_vardecls(env, vdi_copy, rhs);
1081 vd->e(rhs);
1082 } else if (cannot_use_rhs_for_output(env, vd->e())) {
1083 // If the VarDecl does not have a usable right hand side, it needs to be
1084 // marked as output in the FlatZinc
1085 vd->e(nullptr);
1086 assert(vd->flat());
1087 if (vd->type().dim() == 0) {
1088 vd->flat()->addAnnotation(constants().ann.output_var);
1089 check_rename_var(env, vd);
1090 } else {
1091 bool needOutputAnn = true;
1092 if ((reallyFlat->e() != nullptr) && reallyFlat->e()->isa<ArrayLit>()) {
1093 auto* al = reallyFlat->e()->cast<ArrayLit>();
1094 for (unsigned int i = 0; i < al->size(); i++) {
1095 if (Id* id = (*al)[i]->dynamicCast<Id>()) {
1096 if (env.reverseMappers.find(id) != env.reverseMappers.end()) {
1097 needOutputAnn = false;
1098 break;
1099 }
1100 }
1101 }
1102 if (!needOutputAnn) {
1103 output_vardecls(env, vdi_copy, al);
1104 vd->e(copy(env, env.cmap, al));
1105 }
1106 }
1107 if (needOutputAnn) {
1108 std::vector<Expression*> args(vdi->e()->type().dim());
1109 for (unsigned int i = 0; i < args.size(); i++) {
1110 if (vdi->e()->ti()->ranges()[i]->domain() == nullptr) {
1111 args[i] =
1112 new SetLit(Location().introduce(),
1113 eval_intset(env, vd->flat()->ti()->ranges()[i]->domain()));
1114 } else {
1115 args[i] = new SetLit(Location().introduce(),
1116 eval_intset(env, vd->ti()->ranges()[i]->domain()));
1117 }
1118 }
1119 auto* al = new ArrayLit(Location().introduce(), args);
1120 args.resize(1);
1121 args[0] = al;
1122 vd->flat()->addAnnotation(
1123 new Call(Location().introduce(), constants().ann.output_array, args));
1124 check_rename_var(env, vd);
1125 }
1126 }
1127 }
1128 if ((reallyFlat != nullptr) && env.outputFlatVarOccurrences.find(reallyFlat) == -1) {
1129 env.outputFlatVarOccurrences.addIndex(reallyFlat,
1130 static_cast<int>(env.output->size()));
1131 }
1132 }
1133 } else {
1134 if (vd->flat() == nullptr && vdi->e()->e() != nullptr) {
1135 // Need to process right hand side of variable, since it may contain
1136 // identifiers that are only in the FlatZinc and that we would
1137 // therefore fail to copy into the output model
1138 output_vardecls(env, vdi_copy, vdi->e()->e());
1139 }
1140 }
1141 make_par(env, vdi_copy->e());
1142 env.outputVarOccurrences.addIndex(vdi_copy, static_cast<int>(env.output->size()));
1143 CollectOccurrencesE ce(env.outputVarOccurrences, vdi_copy);
1144 top_down(ce, vdi_copy->e());
1145 env.output->addItem(vdi_copy);
1146 }
1147 }
1148 } _ov2(e);
1149 iter_items(_ov2, e.model);
1150
1151 CollectOccurrencesE ce(e.outputVarOccurrences, outputItem);
1152 top_down(ce, outputItem->e());
1153
1154 e.model->mergeStdLib(e, e.output);
1155 process_deletions(e);
1156}
1157
1158Expression* is_fixed_domain(EnvI& env, VarDecl* vd) {
1159 if (vd->type() != Type::varbool() && vd->type() != Type::varint() &&
1160 vd->type() != Type::varfloat()) {
1161 return nullptr;
1162 }
1163 Expression* e = vd->ti()->domain();
1164 if (e == constants().literalTrue || e == constants().literalFalse) {
1165 return e;
1166 }
1167 if (auto* sl = Expression::dynamicCast<SetLit>(e)) {
1168 if (sl->type().bt() == Type::BT_INT) {
1169 IntSetVal* isv = eval_intset(env, sl);
1170 return isv->min() == isv->max() ? IntLit::a(isv->min()) : nullptr;
1171 }
1172 if (sl->type().bt() == Type::BT_FLOAT) {
1173 FloatSetVal* fsv = eval_floatset(env, sl);
1174 return fsv->min() == fsv->max() ? FloatLit::a(fsv->min()) : nullptr;
1175 }
1176 }
1177 return nullptr;
1178}
1179
1180void finalise_output(EnvI& e) {
1181 if (e.output->size() > 0) {
1182 // Adapt existing output model
1183 // (generated by repeated flattening)
1184 e.outputVarOccurrences.clear();
1185 for (unsigned int i = 0; i < e.output->size(); i++) {
1186 Item* item = (*e.output)[i];
1187 if (item->removed()) {
1188 continue;
1189 }
1190 switch (item->iid()) {
1191 case Item::II_VD: {
1192 VarDecl* vd = item->cast<VarDeclI>()->e();
1193 IdMap<KeepAlive>::iterator it;
1194 GCLock lock;
1195 VarDecl* reallyFlat = vd->flat();
1196 while ((reallyFlat != nullptr) && reallyFlat != reallyFlat->flat()) {
1197 reallyFlat = reallyFlat->flat();
1198 }
1199 if (vd->e() == nullptr) {
1200 if (((vd->flat()->e() != nullptr) && vd->flat()->e()->type().isPar()) ||
1201 (is_fixed_domain(e, vd->flat()) != nullptr)) {
1202 VarDecl* reallyFlat = vd->flat();
1203 while (reallyFlat != reallyFlat->flat()) {
1204 reallyFlat = reallyFlat->flat();
1205 }
1206 remove_is_output(reallyFlat);
1207 Expression* flate;
1208 if (Expression* fd = is_fixed_domain(e, vd->flat())) {
1209 flate = fd;
1210 } else {
1211 flate = copy(e, e.cmap, follow_id(reallyFlat->id()));
1212 }
1213 output_vardecls(e, item, flate);
1214 vd->e(flate);
1215 } else if ((it = e.reverseMappers.find(vd->id())) != e.reverseMappers.end()) {
1216 Call* rhs = copy(e, e.cmap, it->second())->cast<Call>();
1217 check_output_par_fn(e, rhs);
1218 remove_is_output(reallyFlat);
1219
1220 output_vardecls(e, item, it->second()->cast<Call>());
1221 vd->e(rhs);
1222
1223 if (e.varOccurrences.occurrences(reallyFlat) == 0 && reallyFlat->e() == nullptr) {
1224 auto it = e.varOccurrences.idx.find(reallyFlat->id());
1225 assert(it != e.varOccurrences.idx.end());
1226 e.flatRemoveItem((*e.flat())[it->second]->cast<VarDeclI>());
1227 }
1228 } else {
1229 // If the VarDecl does not have a usable right hand side, it needs to be
1230 // marked as output in the FlatZinc
1231 assert(vd->flat());
1232
1233 bool needOutputAnn = true;
1234 if ((reallyFlat->e() != nullptr) && reallyFlat->e()->isa<Id>()) {
1235 Id* ident = reallyFlat->e()->cast<Id>();
1236 if (e.reverseMappers.find(ident) != e.reverseMappers.end()) {
1237 needOutputAnn = false;
1238 remove_is_output(vd);
1239 remove_is_output(reallyFlat);
1240
1241 vd->e(copy(e, e.cmap, ident));
1242 Type al_t(vd->e()->type());
1243 al_t.ti(Type::TI_PAR);
1244 vd->e()->type(al_t);
1245
1246 output_vardecls(e, item, ident);
1247
1248 if (e.varOccurrences.occurrences(reallyFlat) == 0) {
1249 auto it = e.varOccurrences.idx.find(reallyFlat->id());
1250 assert(it != e.varOccurrences.idx.end());
1251 e.flatRemoveItem((*e.flat())[it->second]->cast<VarDeclI>());
1252 }
1253 }
1254 } else if ((reallyFlat->e() != nullptr) && reallyFlat->e()->isa<ArrayLit>()) {
1255 auto* al = reallyFlat->e()->cast<ArrayLit>();
1256 for (unsigned int i = 0; i < al->size(); i++) {
1257 if (Id* ident = follow_id_to_value((*al)[i])->dynamicCast<Id>()) {
1258 if (e.reverseMappers.find(ident) != e.reverseMappers.end()) {
1259 needOutputAnn = false;
1260 break;
1261 }
1262 }
1263 }
1264 if (!needOutputAnn) {
1265 remove_is_output(vd);
1266 remove_is_output(reallyFlat);
1267 if (e.varOccurrences.occurrences(reallyFlat) == 0) {
1268 auto it = e.varOccurrences.idx.find(reallyFlat->id());
1269 assert(it != e.varOccurrences.idx.end());
1270 e.flatRemoveItem((*e.flat())[it->second]->cast<VarDeclI>());
1271 }
1272
1273 output_vardecls(e, item, al);
1274 vd->e(copy(e, e.cmap, al));
1275 Type al_t(vd->e()->type());
1276 al_t.ti(Type::TI_PAR);
1277 vd->e()->type(al_t);
1278 }
1279 }
1280 if (needOutputAnn) {
1281 if (!is_output(vd->flat())) {
1282 GCLock lock;
1283 if (vd->type().dim() == 0) {
1284 vd->flat()->addAnnotation(constants().ann.output_var);
1285 } else {
1286 std::vector<Expression*> args(vd->type().dim());
1287 for (unsigned int i = 0; i < args.size(); i++) {
1288 if (vd->ti()->ranges()[i]->domain() == nullptr) {
1289 args[i] =
1290 new SetLit(Location().introduce(),
1291 eval_intset(e, vd->flat()->ti()->ranges()[i]->domain()));
1292 } else {
1293 args[i] = new SetLit(Location().introduce(),
1294 eval_intset(e, vd->ti()->ranges()[i]->domain()));
1295 }
1296 }
1297 auto* al = new ArrayLit(Location().introduce(), args);
1298 args.resize(1);
1299 args[0] = al;
1300 vd->flat()->addAnnotation(
1301 new Call(Location().introduce(), constants().ann.output_array, args));
1302 }
1303 check_rename_var(e, vd);
1304 }
1305 }
1306 }
1307 vd->flat(nullptr);
1308 // Remove enum type
1309 Type vdt = vd->type();
1310 vdt.enumId(0);
1311 vd->type(vdt);
1312 vd->ti()->type(vdt);
1313 }
1314 e.outputVarOccurrences.addIndex(item->cast<VarDeclI>(), static_cast<int>(i));
1315 CollectOccurrencesE ce(e.outputVarOccurrences, item);
1316 top_down(ce, vd);
1317 } break;
1318 case Item::II_OUT: {
1319 CollectOccurrencesE ce(e.outputVarOccurrences, item);
1320 top_down(ce, item->cast<OutputI>()->e());
1321 } break;
1322 case Item::II_FUN: {
1323 CollectOccurrencesE ce(e.outputVarOccurrences, item);
1324 top_down(ce, item->cast<FunctionI>()->e());
1325 top_down(ce, item->cast<FunctionI>()->ti());
1326 for (unsigned int i = item->cast<FunctionI>()->paramCount(); (i--) != 0U;) {
1327 top_down(ce, item->cast<FunctionI>()->param(i));
1328 }
1329 } break;
1330 default:
1331 throw FlatteningError(e, item->loc(), "invalid item in output model");
1332 }
1333 }
1334 }
1335 process_deletions(e);
1336}
1337} // namespace MiniZinc