this repo has no description
dekker.one
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/astexception.hh>
13#include <minizinc/astiterator.hh>
14#include <minizinc/copy.hh>
15#include <minizinc/eval_par.hh>
16#include <minizinc/flat_exp.hh>
17#include <minizinc/flatten.hh>
18#include <minizinc/flatten_internal.hh>
19#include <minizinc/hash.hh>
20#include <minizinc/optimize.hh>
21#include <minizinc/output.hh>
22
23#include <map>
24#include <unordered_map>
25#include <unordered_set>
26
27namespace MiniZinc {
28
29// Create domain constraints. Return true if successful.
30bool create_explicit_domain_constraints(EnvI& envi, VarDecl* vd, Expression* domain) {
31 std::vector<Call*> calls;
32 Location iloc = Location().introduce();
33
34 if (vd->type().isIntSet()) {
35 assert(domain->type().isint() || domain->type().isIntSet());
36 IntSetVal* isv = eval_intset(envi, domain);
37 calls.push_back(new Call(iloc, constants().ids.set_subset, {vd->id(), new SetLit(iloc, isv)}));
38 } else if (domain->type().isbool()) {
39 calls.push_back(new Call(iloc, constants().ids.bool_eq, {vd->id(), domain}));
40 } else if (domain->type().isBoolSet()) {
41 IntSetVal* bsv = eval_boolset(envi, domain);
42 assert(bsv->size() == 1);
43 if (bsv->min() != bsv->max()) {
44 return true; // Both values are still possible, no change
45 }
46 calls.push_back(
47 new Call(iloc, constants().ids.bool_eq, {vd->id(), constants().boollit(bsv->min() > 0)}));
48 } else if (domain->type().isfloat() || domain->type().isFloatSet()) {
49 FloatSetVal* fsv = eval_floatset(envi, domain);
50 if (fsv->size() == 1) { // Range based
51 if (fsv->min() == fsv->max()) {
52 calls.push_back(
53 new Call(iloc, constants().ids.float_.eq, {vd->id(), FloatLit::a(fsv->min())}));
54 } else {
55 FloatSetVal* cfsv;
56 if (vd->ti()->domain() != nullptr) {
57 cfsv = eval_floatset(envi, vd->ti()->domain());
58 } else {
59 cfsv = FloatSetVal::a(-FloatVal::infinity(), FloatVal::infinity());
60 }
61 if (cfsv->min() < fsv->min()) {
62 calls.push_back(
63 new Call(iloc, constants().ids.float_.le, {FloatLit::a(fsv->min()), vd->id()}));
64 }
65 if (cfsv->max() > fsv->max()) {
66 calls.push_back(
67 new Call(iloc, constants().ids.float_.le, {vd->id(), FloatLit::a(fsv->max())}));
68 }
69 }
70 } else {
71 calls.push_back(new Call(iloc, constants().ids.set_in, {vd->id(), new SetLit(iloc, fsv)}));
72 }
73 } else if (domain->type().isint() || domain->type().isIntSet()) {
74 IntSetVal* isv = eval_intset(envi, domain);
75 if (isv->size() == 1) { // Range based
76 if (isv->min() == isv->max()) {
77 calls.push_back(new Call(iloc, constants().ids.int_.eq, {vd->id(), IntLit::a(isv->min())}));
78 } else {
79 IntSetVal* cisv;
80 if (vd->ti()->domain() != nullptr) {
81 cisv = eval_intset(envi, vd->ti()->domain());
82 } else {
83 cisv = IntSetVal::a(-IntVal::infinity(), IntVal::infinity());
84 }
85 if (cisv->min() < isv->min()) {
86 calls.push_back(
87 new Call(iloc, constants().ids.int_.le, {IntLit::a(isv->min()), vd->id()}));
88 }
89 if (cisv->max() > isv->max()) {
90 calls.push_back(
91 new Call(iloc, constants().ids.int_.le, {vd->id(), IntLit::a(isv->max())}));
92 }
93 }
94 } else {
95 calls.push_back(new Call(iloc, constants().ids.set_in, {vd->id(), new SetLit(iloc, isv)}));
96 }
97 } else {
98 return false;
99 }
100
101 int counter = 0;
102 for (Call* c : calls) {
103 CallStackItem csi(envi, IntLit::a(counter++));
104 c->ann().add(constants().ann.domain_change_constraint);
105 c->type(Type::varbool());
106 c->decl(envi.model->matchFn(envi, c, true));
107 flat_exp(envi, Ctx(), c, constants().varTrue, constants().varTrue);
108 }
109 return true;
110}
111
112void set_computed_domain(EnvI& envi, VarDecl* vd, Expression* domain, bool is_computed) {
113 if (envi.hasReverseMapper(vd->id())) {
114 if (!create_explicit_domain_constraints(envi, vd, domain)) {
115 std::ostringstream ss;
116 ss << "Unable to create domain constraint for reverse mapped variable: " << *vd->id() << " = "
117 << *domain << std::endl;
118 throw EvalError(envi, domain->loc(), ss.str());
119 }
120 vd->ti()->domain(domain);
121 return;
122 }
123 if (envi.fopts.recordDomainChanges && !vd->ann().contains(constants().ann.is_defined_var) &&
124 !vd->introduced() && !(vd->type().dim() > 0)) {
125 if (create_explicit_domain_constraints(envi, vd, domain)) {
126 return;
127 }
128 std::cerr << "Warning: domain change not handled by -g mode: " << *vd->id() << " = " << *domain
129 << std::endl;
130 }
131 vd->ti()->domain(domain);
132 vd->ti()->setComputedDomain(is_computed);
133}
134
135/// Output operator for contexts
136template <class Char, class Traits>
137std::basic_ostream<Char, Traits>& operator<<(std::basic_ostream<Char, Traits>& os, Ctx& ctx) {
138 switch (ctx.b) {
139 case C_ROOT:
140 os << "R";
141 break;
142 case C_POS:
143 os << "+";
144 break;
145 case C_NEG:
146 os << "-";
147 break;
148 case C_MIX:
149 os << "M";
150 break;
151 default:
152 assert(false);
153 break;
154 }
155 switch (ctx.i) {
156 case C_ROOT:
157 os << "R";
158 break;
159 case C_POS:
160 os << "+";
161 break;
162 case C_NEG:
163 os << "-";
164 break;
165 case C_MIX:
166 os << "M";
167 break;
168 default:
169 assert(false);
170 break;
171 }
172 if (ctx.neg) {
173 os << "!";
174 }
175 return os;
176}
177
178BCtx operator+(const BCtx& c) {
179 switch (c) {
180 case C_ROOT:
181 case C_POS:
182 return C_POS;
183 case C_NEG:
184 return C_NEG;
185 case C_MIX:
186 return C_MIX;
187 default:
188 assert(false);
189 return C_ROOT;
190 }
191}
192
193BCtx operator-(const BCtx& c) {
194 switch (c) {
195 case C_ROOT:
196 case C_POS:
197 return C_NEG;
198 case C_NEG:
199 return C_POS;
200 case C_MIX:
201 return C_MIX;
202 default:
203 assert(false);
204 return C_ROOT;
205 }
206}
207
208/// Check if \a c is non-positive
209bool nonpos(const BCtx& c) { return c == C_NEG || c == C_MIX; }
210/// Check if \a c is non-negative
211bool nonneg(const BCtx& c) { return c == C_ROOT || c == C_POS; }
212
213void dump_ee_b(const std::vector<EE>& ee) {
214 for (const auto& i : ee) {
215 std::cerr << *i.b() << "\n";
216 }
217}
218void dump_ee_r(const std::vector<EE>& ee) {
219 for (const auto& i : ee) {
220 std::cerr << *i.r() << "\n";
221 }
222}
223
224std::tuple<BCtx, bool> ann_to_ctx(VarDecl* vd) {
225 if (vd->ann().contains(constants().ctx.root)) {
226 return std::make_tuple(C_ROOT, true);
227 }
228 if (vd->ann().contains(constants().ctx.mix)) {
229 return std::make_tuple(C_MIX, true);
230 }
231 if (vd->ann().contains(constants().ctx.pos)) {
232 return std::make_tuple(C_POS, true);
233 }
234 if (vd->ann().contains(constants().ctx.neg)) {
235 return std::make_tuple(C_NEG, true);
236 }
237 return std::make_tuple(C_MIX, false);
238}
239
240void add_ctx_ann(VarDecl* vd, BCtx& c) {
241 if (vd != nullptr) {
242 Id* ctx_id = nullptr;
243 BCtx nc;
244 bool annotated;
245 std::tie(nc, annotated) = ann_to_ctx(vd);
246 // If previously annotated
247 if (annotated) {
248 // Early exit
249 if (nc == c || nc == C_ROOT || (nc == C_MIX && c != C_ROOT)) {
250 return;
251 }
252 // Remove old annotation
253 switch (nc) {
254 case C_ROOT:
255 vd->ann().remove(constants().ctx.root);
256 break;
257 case C_MIX:
258 vd->ann().remove(constants().ctx.mix);
259 break;
260 case C_POS:
261 vd->ann().remove(constants().ctx.pos);
262 break;
263 case C_NEG:
264 vd->ann().remove(constants().ctx.neg);
265 break;
266 default:
267 assert(false);
268 break;
269 }
270 // Determine new context
271 if (c == C_ROOT) {
272 nc = C_ROOT;
273 } else {
274 nc = C_MIX;
275 }
276 } else {
277 nc = c;
278 }
279 switch (nc) {
280 case C_ROOT:
281 ctx_id = constants().ctx.root;
282 break;
283 case C_POS:
284 ctx_id = constants().ctx.pos;
285 break;
286 case C_NEG:
287 ctx_id = constants().ctx.neg;
288 break;
289 case C_MIX:
290 ctx_id = constants().ctx.mix;
291 break;
292 default:
293 assert(false);
294 break;
295 }
296 vd->addAnnotation(ctx_id);
297 }
298}
299
300void make_defined_var(VarDecl* vd, Call* c) {
301 if (!vd->ann().contains(constants().ann.is_defined_var)) {
302 std::vector<Expression*> args(1);
303 args[0] = vd->id();
304 Call* dv = new Call(Location().introduce(), constants().ann.defines_var, args);
305 dv->type(Type::ann());
306 vd->addAnnotation(constants().ann.is_defined_var);
307 c->addAnnotation(dv);
308 }
309}
310
311bool is_defines_var_ann(Expression* e) {
312 return e->isa<Call>() && e->cast<Call>()->id() == constants().ann.defines_var;
313}
314
315/// Check if \a e is NULL or true
316bool istrue(EnvI& env, Expression* e) {
317 if (e == nullptr) {
318 return true;
319 }
320 if (e->type() == Type::parbool()) {
321 if (e->type().cv()) {
322 Ctx ctx;
323 ctx.b = C_MIX;
324 KeepAlive r = flat_cv_exp(env, ctx, e);
325 return eval_bool(env, r());
326 }
327 GCLock lock;
328 return eval_bool(env, e);
329 }
330 return false;
331}
332/// Check if \a e is non-NULL and false
333bool isfalse(EnvI& env, Expression* e) {
334 if (e == nullptr) {
335 return false;
336 }
337 if (e->type() == Type::parbool()) {
338 if (e->type().cv()) {
339 Ctx ctx;
340 ctx.b = C_MIX;
341 KeepAlive r = flat_cv_exp(env, ctx, e);
342 return !eval_bool(env, r());
343 }
344 GCLock lock;
345 return !eval_bool(env, e);
346 }
347 return false;
348}
349
350/// Use bounds from ovd for vd if they are better.
351/// Returns true if ovd's bounds are better.
352bool update_bounds(EnvI& envi, VarDecl* ovd, VarDecl* vd) {
353 bool tighter = false;
354 bool fixed = false;
355 if ((ovd->ti()->domain() != nullptr) || (ovd->e() != nullptr)) {
356 IntVal intval;
357 FloatVal doubleval;
358 bool boolval;
359
360 if (vd->type().isint()) {
361 IntBounds oldbounds = compute_int_bounds(envi, ovd->id());
362 IntBounds bounds(0, 0, false);
363 if ((vd->ti()->domain() != nullptr) || (vd->e() != nullptr)) {
364 bounds = compute_int_bounds(envi, vd->id());
365 }
366
367 if (((vd->ti()->domain() != nullptr) || (vd->e() != nullptr)) && bounds.valid &&
368 bounds.l.isFinite() && bounds.u.isFinite()) {
369 if (oldbounds.valid && oldbounds.l.isFinite() && oldbounds.u.isFinite()) {
370 fixed = oldbounds.u == oldbounds.l || bounds.u == bounds.l;
371 if (fixed) {
372 tighter = true;
373 intval = oldbounds.u == oldbounds.l ? oldbounds.u : bounds.l;
374 ovd->ti()->domain(new SetLit(ovd->loc(), IntSetVal::a(intval, intval)));
375 } else {
376 IntSetVal* olddom =
377 ovd->ti()->domain() != nullptr ? eval_intset(envi, ovd->ti()->domain()) : nullptr;
378 IntSetVal* newdom =
379 vd->ti()->domain() != nullptr ? eval_intset(envi, vd->ti()->domain()) : nullptr;
380
381 if (olddom != nullptr) {
382 if (newdom == nullptr) {
383 tighter = true;
384 } else {
385 IntSetRanges oisr(olddom);
386 IntSetRanges nisr(newdom);
387 IntSetRanges nisr_card(newdom);
388
389 Ranges::Inter<IntVal, IntSetRanges, IntSetRanges> inter(oisr, nisr);
390
391 if (Ranges::cardinality(inter) < Ranges::cardinality(nisr_card)) {
392 IntSetRanges oisr_inter(olddom);
393 IntSetRanges nisr_inter(newdom);
394 Ranges::Inter<IntVal, IntSetRanges, IntSetRanges> inter_card(oisr_inter,
395 nisr_inter);
396 tighter = true;
397 ovd->ti()->domain(new SetLit(ovd->loc(), IntSetVal::ai(inter_card)));
398 }
399 }
400 }
401 }
402 }
403 } else {
404 if (oldbounds.valid && oldbounds.l.isFinite() && oldbounds.u.isFinite()) {
405 tighter = true;
406 fixed = oldbounds.u == oldbounds.l;
407 if (fixed) {
408 intval = oldbounds.u;
409 ovd->ti()->domain(new SetLit(ovd->loc(), IntSetVal::a(intval, intval)));
410 }
411 }
412 }
413 } else if (vd->type().isfloat()) {
414 FloatBounds oldbounds = compute_float_bounds(envi, ovd->id());
415 FloatBounds bounds(0.0, 0.0, false);
416 if ((vd->ti()->domain() != nullptr) || (vd->e() != nullptr)) {
417 bounds = compute_float_bounds(envi, vd->id());
418 }
419 if (((vd->ti()->domain() != nullptr) || (vd->e() != nullptr)) && bounds.valid) {
420 if (oldbounds.valid) {
421 fixed = oldbounds.u == oldbounds.l || bounds.u == bounds.l;
422 if (fixed) {
423 doubleval = oldbounds.u == oldbounds.l ? oldbounds.u : bounds.l;
424 }
425 tighter = fixed || (oldbounds.u - oldbounds.l < bounds.u - bounds.l);
426 }
427 } else {
428 if (oldbounds.valid) {
429 tighter = true;
430 fixed = oldbounds.u == oldbounds.l;
431 if (fixed) {
432 doubleval = oldbounds.u;
433 }
434 }
435 }
436 } else if (vd->type().isbool()) {
437 if (ovd->ti()->domain() != nullptr) {
438 fixed = tighter = true;
439 boolval = eval_bool(envi, ovd->ti()->domain());
440 } else {
441 fixed = tighter = ((ovd->e() != nullptr) && ovd->e()->isa<BoolLit>());
442 if (fixed) {
443 boolval = ovd->e()->cast<BoolLit>()->v();
444 }
445 }
446 }
447
448 if (tighter) {
449 vd->ti()->domain(ovd->ti()->domain());
450 if (vd->e() == nullptr && fixed) {
451 if (vd->ti()->type().isvarint()) {
452 vd->type(Type::parint());
453 vd->ti(new TypeInst(vd->loc(), Type::parint()));
454 vd->e(IntLit::a(intval));
455 } else if (vd->ti()->type().isvarfloat()) {
456 vd->type(Type::parfloat());
457 vd->ti(new TypeInst(vd->loc(), Type::parfloat()));
458 vd->e(FloatLit::a(doubleval));
459 } else if (vd->ti()->type().isvarbool()) {
460 vd->type(Type::parbool());
461 vd->ti(new TypeInst(vd->loc(), Type::parbool()));
462 vd->ti()->domain(boolval ? constants().literalTrue : constants().literalFalse);
463 vd->e(new BoolLit(vd->loc(), boolval));
464 }
465 }
466 }
467 }
468
469 return tighter;
470}
471
472std::string get_path(EnvI& env) {
473 std::string path;
474 std::stringstream ss;
475 if (env.dumpPath(ss)) {
476 path = ss.str();
477 }
478
479 return path;
480}
481
482inline Location get_loc(EnvI& env, Expression* e1, Expression* e2) {
483 if (e1 != nullptr) {
484 return e1->loc().introduce();
485 }
486 if (e2 != nullptr) {
487 return e2->loc().introduce();
488 }
489 return Location().introduce();
490}
491inline Id* get_id(EnvI& env, Id* origId) {
492 return origId != nullptr ? origId : new Id(Location().introduce(), env.genId(), nullptr);
493}
494
495StringLit* get_longest_mzn_path_annotation(EnvI& env, const Expression* e) {
496 StringLit* sl = nullptr;
497
498 if (const auto* vd = e->dynamicCast<const VarDecl>()) {
499 EnvI::ReversePathMap& reversePathMap = env.getReversePathMap();
500 KeepAlive vd_decl_ka(vd->id()->decl());
501 auto it = reversePathMap.find(vd_decl_ka);
502 if (it != reversePathMap.end()) {
503 sl = new StringLit(Location(), it->second);
504 }
505 } else {
506 for (ExpressionSetIter it = e->ann().begin(); it != e->ann().end(); ++it) {
507 if (Call* ca = (*it)->dynamicCast<Call>()) {
508 if (ca->id() == constants().ann.mzn_path) {
509 auto* sl1 = ca->arg(0)->cast<StringLit>();
510 if (sl != nullptr) {
511 if (sl1->v().size() > sl->v().size()) {
512 sl = sl1;
513 }
514 } else {
515 sl = sl1;
516 }
517 }
518 }
519 }
520 }
521 return sl;
522}
523
524void add_path_annotation(EnvI& env, Expression* e) {
525 if (!(e->type().isAnn() || e->isa<Id>()) && e->type().dim() == 0) {
526 GCLock lock;
527 Annotation& ann = e->ann();
528 if (ann.containsCall(constants().ann.mzn_path)) {
529 return;
530 }
531
532 EnvI::ReversePathMap& reversePathMap = env.getReversePathMap();
533
534 std::vector<Expression*> path_args(1);
535 std::string p;
536 KeepAlive e_ka(e);
537 auto it = reversePathMap.find(e_ka);
538 if (it == reversePathMap.end()) {
539 p = get_path(env);
540 } else {
541 p = it->second;
542 }
543
544 if (!p.empty()) {
545 path_args[0] = new StringLit(Location(), p);
546 Call* path_call = new Call(e->loc(), constants().ann.mzn_path, path_args);
547 path_call->type(Type::ann());
548 e->addAnnotation(path_call);
549 }
550 }
551}
552
553VarDecl* new_vardecl(EnvI& env, const Ctx& ctx, TypeInst* ti, Id* origId, VarDecl* origVd,
554 Expression* rhs) {
555 VarDecl* vd = nullptr;
556
557 // Is this vardecl already in the FlatZinc (for unification)
558 bool hasBeenAdded = false;
559
560 // Don't use paths for arrays or annotations
561 if (ti->type().dim() == 0 && !ti->type().isAnn()) {
562 std::string path = get_path(env);
563 if (!path.empty()) {
564 EnvI::ReversePathMap& reversePathMap = env.getReversePathMap();
565 EnvI::PathMap& pathMap = env.getPathMap();
566 auto it = pathMap.find(path);
567
568 if (it != pathMap.end()) {
569 auto* ovd = Expression::cast<VarDecl>((it->second.decl)());
570 unsigned int ovd_pass = it->second.passNumber;
571
572 if (ovd != nullptr) {
573 // If ovd was introduced during the same pass, we can unify
574 if (env.currentPassNumber == ovd_pass) {
575 vd = ovd;
576 if (origId != nullptr) {
577 origId->decl(vd);
578 }
579 hasBeenAdded = true;
580 } else {
581 vd = new VarDecl(get_loc(env, origVd, rhs), ti, get_id(env, origId));
582 hasBeenAdded = false;
583 update_bounds(env, ovd, vd);
584 }
585
586 // Check whether ovd was unified in a previous pass
587 if (ovd->id() != ovd->id()->decl()->id()) {
588 // We may not have seen the pointed to decl just yet
589 KeepAlive ovd_decl_ka(ovd->id()->decl());
590 auto path2It = reversePathMap.find(ovd_decl_ka);
591 if (path2It != reversePathMap.end()) {
592 std::string path2 = path2It->second;
593 EnvI::PathVar vd_tup{vd, env.currentPassNumber};
594
595 pathMap[path] = vd_tup;
596 pathMap[path2] = vd_tup;
597 KeepAlive vd_ka(vd);
598 reversePathMap.insert(vd_ka, path);
599 }
600 }
601 }
602 } else {
603 // Create new VarDecl and add it to the maps
604 vd = new VarDecl(get_loc(env, origVd, rhs), ti, get_id(env, origId));
605 hasBeenAdded = false;
606 EnvI::PathVar vd_tup{vd, env.currentPassNumber};
607 pathMap[path] = vd_tup;
608 KeepAlive vd_ka(vd);
609 reversePathMap.insert(vd_ka, path);
610 }
611 }
612 }
613 if (vd == nullptr) {
614 vd = new VarDecl(get_loc(env, origVd, rhs), ti, get_id(env, origId));
615 hasBeenAdded = false;
616 }
617
618 // If vd has an e() use bind to turn rhs into a constraint
619 if (vd->e() != nullptr) {
620 if (rhs != nullptr) {
621 bind(env, ctx, vd, rhs);
622 }
623 } else {
624 vd->e(rhs);
625 if ((rhs != nullptr) && hasBeenAdded) {
626 // This variable is being reused, so it won't be added to the model below.
627 // Therefore, we need to register that we changed the RHS, in order
628 // for the reference counts to be accurate.
629 env.voAddExp(vd);
630 }
631 }
632 assert(!vd->type().isbot());
633 if ((origVd != nullptr) && (origVd->id()->idn() != -1 || origVd->toplevel())) {
634 vd->introduced(origVd->introduced());
635 } else {
636 vd->introduced(true);
637 }
638
639 vd->flat(vd);
640
641 // Copy annotations from origVd
642 if (origVd != nullptr) {
643 for (ExpressionSetIter it = origVd->ann().begin(); it != origVd->ann().end(); ++it) {
644 EE ee_ann = flat_exp(env, Ctx(), *it, nullptr, constants().varTrue);
645 vd->addAnnotation(ee_ann.r());
646 }
647 }
648
649 if (!hasBeenAdded) {
650 if (FunctionI* fi = env.model->matchRevMap(env, vd->type())) {
651 // We need to introduce a reverse mapper
652 Call* revmap = new Call(Location().introduce(), fi->id(), {vd->id()});
653 revmap->decl(fi);
654 revmap->type(Type::varbool());
655 env.flatAddItem(new ConstraintI(Location().introduce(), revmap));
656 }
657
658 auto* ni = new VarDeclI(Location().introduce(), vd);
659 env.flatAddItem(ni);
660 EE ee(vd, nullptr);
661 env.cseMapInsert(vd->id(), ee);
662 }
663
664 return vd;
665}
666
667#define MZN_FILL_REIFY_MAP(T, ID) \
668 _reifyMap.insert( \
669 std::pair<ASTString, ASTString>(constants().ids.T.ID, constants().ids.T##reif.ID));
670
671EnvI::EnvI(Model* model0, std::ostream& outstream0, std::ostream& errstream0)
672 : model(model0),
673 originalModel(nullptr),
674 output(new Model),
675 outstream(outstream0),
676 errstream(errstream0),
677 currentPassNumber(0),
678 finalPassNumber(1),
679 maxPathDepth(0),
680 ignorePartial(false),
681 ignoreUnknownIds(false),
682 maxCallStack(0),
683 inRedundantConstraint(0),
684 inMaybePartial(0),
685 inReverseMapVar(false),
686 counters({0, 0, 0, 0}),
687 pathUse(0),
688 _flat(new Model),
689 _failed(false),
690 _ids(0),
691 _collectVardecls(false) {
692 MZN_FILL_REIFY_MAP(int_, lin_eq);
693 MZN_FILL_REIFY_MAP(int_, lin_le);
694 MZN_FILL_REIFY_MAP(int_, lin_ne);
695 MZN_FILL_REIFY_MAP(int_, plus);
696 MZN_FILL_REIFY_MAP(int_, minus);
697 MZN_FILL_REIFY_MAP(int_, times);
698 MZN_FILL_REIFY_MAP(int_, div);
699 MZN_FILL_REIFY_MAP(int_, mod);
700 MZN_FILL_REIFY_MAP(int_, lt);
701 MZN_FILL_REIFY_MAP(int_, le);
702 MZN_FILL_REIFY_MAP(int_, gt);
703 MZN_FILL_REIFY_MAP(int_, ge);
704 MZN_FILL_REIFY_MAP(int_, eq);
705 MZN_FILL_REIFY_MAP(int_, ne);
706 MZN_FILL_REIFY_MAP(float_, lin_eq);
707 MZN_FILL_REIFY_MAP(float_, lin_le);
708 MZN_FILL_REIFY_MAP(float_, lin_lt);
709 MZN_FILL_REIFY_MAP(float_, lin_ne);
710 MZN_FILL_REIFY_MAP(float_, plus);
711 MZN_FILL_REIFY_MAP(float_, minus);
712 MZN_FILL_REIFY_MAP(float_, times);
713 MZN_FILL_REIFY_MAP(float_, div);
714 MZN_FILL_REIFY_MAP(float_, mod);
715 MZN_FILL_REIFY_MAP(float_, lt);
716 MZN_FILL_REIFY_MAP(float_, le);
717 MZN_FILL_REIFY_MAP(float_, gt);
718 MZN_FILL_REIFY_MAP(float_, ge);
719 MZN_FILL_REIFY_MAP(float_, eq);
720 MZN_FILL_REIFY_MAP(float_, ne);
721 _reifyMap.insert(
722 std::pair<ASTString, ASTString>(constants().ids.forall, constants().ids.forallReif));
723 _reifyMap.insert(
724 std::pair<ASTString, ASTString>(constants().ids.bool_eq, constants().ids.bool_eq_reif));
725 _reifyMap.insert(std::pair<ASTString, ASTString>(constants().ids.bool_clause,
726 constants().ids.bool_clause_reif));
727 _reifyMap.insert(
728 std::pair<ASTString, ASTString>(constants().ids.clause, constants().ids.bool_clause_reif));
729 _reifyMap.insert({constants().ids.bool_not, constants().ids.bool_not});
730}
731EnvI::~EnvI() {
732 delete _flat;
733 delete output;
734 delete model;
735 delete originalModel;
736}
737long long int EnvI::genId() { return _ids++; }
738void EnvI::cseMapInsert(Expression* e, const EE& ee) {
739 KeepAlive ka(e);
740 _cseMap.insert(ka, WW(ee.r(), ee.b()));
741 Call* c = e->dynamicCast<Call>();
742 if (c != nullptr && c->decl() != nullptr &&
743 get_annotation(c->decl()->ann(), constants().ann.impure) != nullptr) {
744 return;
745 }
746 if ((c != nullptr) && c->id() == constants().ids.bool_not && c->arg(0)->isa<Id>() &&
747 ee.r()->isa<Id>() && ee.b() == constants().boollit(true)) {
748 Call* neg_c = new Call(Location().introduce(), c->id(), {ee.r()});
749 neg_c->type(c->type());
750 neg_c->decl(c->decl());
751 KeepAlive neg_ka(neg_c);
752 _cseMap.insert(neg_ka, WW(c->arg(0), ee.b()));
753 }
754}
755EnvI::CSEMap::iterator EnvI::cseMapFind(Expression* e) {
756 KeepAlive ka(e);
757 auto it = _cseMap.find(ka);
758 if (it != _cseMap.end()) {
759 if (it->second.r() != nullptr) {
760 VarDecl* it_vd = it->second.r()->isa<Id>() ? it->second.r()->cast<Id>()->decl()
761 : it->second.r()->dynamicCast<VarDecl>();
762 if (it_vd != nullptr) {
763 int idx = varOccurrences.find(it_vd);
764 if (idx == -1 || (*_flat)[idx]->removed()) {
765 return _cseMap.end();
766 }
767 }
768 } else {
769 return _cseMap.end();
770 }
771 }
772 return it;
773}
774void EnvI::cseMapRemove(Expression* e) {
775 KeepAlive ka(e);
776 _cseMap.remove(ka);
777}
778EnvI::CSEMap::iterator EnvI::cseMapEnd() { return _cseMap.end(); }
779void EnvI::dump() {
780 struct EED {
781 static std::string k(Expression* e) {
782 std::ostringstream oss;
783 oss << *e;
784 return oss.str();
785 }
786 static std::string d(const WW& ee) {
787 std::ostringstream oss;
788 oss << *ee.r() << " " << ee.b();
789 return oss.str();
790 }
791 };
792 _cseMap.dump<EED>();
793}
794
795void EnvI::flatAddItem(Item* i) {
796 assert(_flat);
797 if (_failed) {
798 return;
799 }
800 _flat->addItem(i);
801
802 Expression* toAnnotate = nullptr;
803 Expression* toAdd = nullptr;
804 switch (i->iid()) {
805 case Item::II_VD: {
806 auto* vd = i->cast<VarDeclI>();
807 add_path_annotation(*this, vd->e());
808 toAnnotate = vd->e()->e();
809 varOccurrences.addIndex(vd, static_cast<int>(_flat->size()) - 1);
810 toAdd = vd->e();
811 break;
812 }
813 case Item::II_CON: {
814 auto* ci = i->cast<ConstraintI>();
815
816 if (ci->e()->isa<BoolLit>() && !ci->e()->cast<BoolLit>()->v()) {
817 fail();
818 } else {
819 toAnnotate = ci->e();
820 add_path_annotation(*this, ci->e());
821 toAdd = ci->e();
822 }
823 break;
824 }
825 case Item::II_SOL: {
826 auto* si = i->cast<SolveI>();
827 CollectOccurrencesE ce(varOccurrences, si);
828 top_down(ce, si->e());
829 for (ExpressionSetIter it = si->ann().begin(); it != si->ann().end(); ++it) {
830 top_down(ce, *it);
831 }
832 break;
833 }
834 case Item::II_OUT: {
835 auto* si = i->cast<OutputI>();
836 toAdd = si->e();
837 break;
838 }
839 default:
840 break;
841 }
842 if ((toAnnotate != nullptr) && toAnnotate->isa<Call>()) {
843 annotateFromCallStack(toAnnotate);
844 }
845 if (toAdd != nullptr) {
846 CollectOccurrencesE ce(varOccurrences, i);
847 top_down(ce, toAdd);
848 }
849}
850
851void EnvI::annotateFromCallStack(Expression* e) {
852 int prev = !idStack.empty() ? idStack.back() : 0;
853 bool allCalls = true;
854 for (int i = static_cast<int>(callStack.size()) - 1; i >= prev; i--) {
855 Expression* ee = callStack[i]->untag();
856 allCalls = allCalls && (i == callStack.size() - 1 || ee->isa<Call>() || ee->isa<BinOp>());
857 for (ExpressionSetIter it = ee->ann().begin(); it != ee->ann().end(); ++it) {
858 EE ee_ann = flat_exp(*this, Ctx(), *it, nullptr, constants().varTrue);
859 if (allCalls || !is_defines_var_ann(ee_ann.r())) {
860 e->addAnnotation(ee_ann.r());
861 }
862 }
863 }
864}
865
866void EnvI::copyPathMapsAndState(EnvI& env) {
867 finalPassNumber = env.finalPassNumber;
868 maxPathDepth = env.maxPathDepth;
869 currentPassNumber = env.currentPassNumber;
870 _filenameSet = env._filenameSet;
871 maxPathDepth = env.maxPathDepth;
872 _pathMap = env.getPathMap();
873 _reversePathMap = env.getReversePathMap();
874}
875
876void EnvI::flatRemoveExpr(Expression* e, Item* i) {
877 std::vector<VarDecl*> toRemove;
878 CollectDecls cd(varOccurrences, toRemove, i);
879 top_down(cd, e);
880
881 Model& flat = (*_flat);
882 while (!toRemove.empty()) {
883 VarDecl* cur = toRemove.back();
884 toRemove.pop_back();
885 assert(varOccurrences.occurrences(cur) == 0 && CollectDecls::varIsFree(cur));
886
887 auto cur_idx = varOccurrences.idx.find(cur->id());
888 if (cur_idx != varOccurrences.idx.end()) {
889 auto* vdi = flat[cur_idx->second]->cast<VarDeclI>();
890
891 if (!is_output(vdi->e()) && !vdi->removed()) {
892 CollectDecls cd(varOccurrences, toRemove, vdi);
893 top_down(cd, vdi->e()->e());
894 vdi->remove();
895 }
896 }
897 }
898}
899
900void EnvI::flatRemoveItem(ConstraintI* ci) {
901 flatRemoveExpr(ci->e(), ci);
902 ci->e(constants().literalTrue);
903 ci->remove();
904}
905void EnvI::flatRemoveItem(VarDeclI* vdi) {
906 flatRemoveExpr(vdi->e(), vdi);
907 vdi->remove();
908}
909
910void EnvI::fail(const std::string& msg) {
911 if (!_failed) {
912 addWarning(std::string("model inconsistency detected") +
913 (msg.empty() ? std::string() : (": " + msg)));
914 _failed = true;
915 for (auto& i : *_flat) {
916 i->remove();
917 }
918 auto* failedConstraint = new ConstraintI(Location().introduce(), constants().literalFalse);
919 _flat->addItem(failedConstraint);
920 _flat->addItem(SolveI::sat(Location().introduce()));
921 for (auto& i : *output) {
922 i->remove();
923 }
924 output->addItem(
925 new OutputI(Location().introduce(), new ArrayLit(Location(), std::vector<Expression*>())));
926 throw ModelInconsistent(*this, Location().introduce());
927 }
928}
929
930bool EnvI::failed() const { return _failed; }
931
932unsigned int EnvI::registerEnum(VarDeclI* vdi) {
933 auto it = _enumMap.find(vdi);
934 unsigned int ret;
935 if (it == _enumMap.end()) {
936 ret = static_cast<unsigned int>(_enumVarDecls.size());
937 _enumVarDecls.push_back(vdi);
938 _enumMap.insert(std::make_pair(vdi, ret));
939 } else {
940 ret = it->second;
941 }
942 return ret + 1;
943}
944VarDeclI* EnvI::getEnum(unsigned int i) const {
945 assert(i > 0 && i <= _enumVarDecls.size());
946 return _enumVarDecls[i - 1];
947}
948unsigned int EnvI::registerArrayEnum(const std::vector<unsigned int>& arrayEnum) {
949 std::ostringstream oss;
950 for (unsigned int i : arrayEnum) {
951 assert(i <= _enumVarDecls.size());
952 oss << i << ".";
953 }
954 auto it = _arrayEnumMap.find(oss.str());
955 unsigned int ret;
956 if (it == _arrayEnumMap.end()) {
957 ret = static_cast<unsigned int>(_arrayEnumDecls.size());
958 _arrayEnumDecls.push_back(arrayEnum);
959 _arrayEnumMap.insert(std::make_pair(oss.str(), ret));
960 } else {
961 ret = it->second;
962 }
963 return ret + 1;
964}
965const std::vector<unsigned int>& EnvI::getArrayEnum(unsigned int i) const {
966 assert(i > 0 && i <= _arrayEnumDecls.size());
967 return _arrayEnumDecls[i - 1];
968}
969bool EnvI::isSubtype(const Type& t1, const Type& t2, bool strictEnums) const {
970 if (!t1.isSubtypeOf(t2, strictEnums)) {
971 return false;
972 }
973 if (strictEnums && t1.dim() == 0 && t2.dim() != 0 && t2.enumId() != 0) {
974 // set assigned to an array
975 const std::vector<unsigned int>& t2enumIds = getArrayEnum(t2.enumId());
976 if (t2enumIds[t2enumIds.size() - 1] != 0 && t1.enumId() != t2enumIds[t2enumIds.size() - 1]) {
977 return false;
978 }
979 }
980 if (strictEnums && t1.dim() > 0 && t1.enumId() != t2.enumId()) {
981 if (t1.enumId() == 0) {
982 return t1.isbot();
983 }
984 if (t2.enumId() != 0) {
985 const std::vector<unsigned int>& t1enumIds = getArrayEnum(t1.enumId());
986 const std::vector<unsigned int>& t2enumIds = getArrayEnum(t2.enumId());
987 assert(t1enumIds.size() == t2enumIds.size());
988 for (unsigned int i = 0; i < t1enumIds.size() - 1; i++) {
989 if (t2enumIds[i] != 0 && t1enumIds[i] != t2enumIds[i]) {
990 return false;
991 }
992 }
993 if (!t1.isbot() && t2enumIds[t1enumIds.size() - 1] != 0 &&
994 t1enumIds[t1enumIds.size() - 1] != t2enumIds[t2enumIds.size() - 1]) {
995 return false;
996 }
997 }
998 }
999 return true;
1000}
1001
1002void EnvI::collectVarDecls(bool b) { _collectVardecls = b; }
1003void EnvI::voAddExp(VarDecl* vd) {
1004 if ((vd->e() != nullptr) && vd->e()->isa<Call>() && !vd->e()->type().isAnn()) {
1005 int prev = !idStack.empty() ? idStack.back() : 0;
1006 for (int i = static_cast<int>(callStack.size()) - 1; i >= prev; i--) {
1007 Expression* ee = callStack[i]->untag();
1008 for (ExpressionSetIter it = ee->ann().begin(); it != ee->ann().end(); ++it) {
1009 Expression* ann = *it;
1010 if (ann != constants().ann.add_to_output && ann != constants().ann.rhs_from_assignment) {
1011 bool needAnnotation = true;
1012 if (Call* ann_c = ann->dynamicCast<Call>()) {
1013 if (ann_c->id() == constants().ann.defines_var) {
1014 // only add defines_var annotation if vd is the defined variable
1015 if (Id* defined_var = ann_c->arg(0)->dynamicCast<Id>()) {
1016 if (defined_var->decl() != vd->id()->decl()) {
1017 needAnnotation = false;
1018 }
1019 }
1020 }
1021 }
1022 if (needAnnotation) {
1023 EE ee_ann = flat_exp(*this, Ctx(), *it, nullptr, constants().varTrue);
1024 vd->e()->addAnnotation(ee_ann.r());
1025 }
1026 }
1027 }
1028 }
1029 }
1030 int idx = varOccurrences.find(vd);
1031 CollectOccurrencesE ce(varOccurrences, (*_flat)[idx]);
1032 top_down(ce, vd->e());
1033 if (_collectVardecls) {
1034 modifiedVarDecls.push_back(idx);
1035 }
1036}
1037Model* EnvI::flat() { return _flat; }
1038void EnvI::swap() {
1039 Model* tmp = model;
1040 model = _flat;
1041 _flat = tmp;
1042}
1043ASTString EnvI::reifyId(const ASTString& id) {
1044 auto it = _reifyMap.find(id);
1045 if (it == _reifyMap.end()) {
1046 std::ostringstream ss;
1047 ss << id << "_reif";
1048 return {ss.str()};
1049 }
1050 return it->second;
1051}
1052#undef MZN_FILL_REIFY_MAP
1053ASTString EnvI::halfReifyId(const ASTString& id) {
1054 std::ostringstream ss;
1055 ss << id << "_imp";
1056 return {ss.str()};
1057}
1058
1059void EnvI::addWarning(const std::string& msg) {
1060 if (warnings.size() > 20) {
1061 return;
1062 }
1063 if (warnings.size() == 20) {
1064 warnings.emplace_back("Further warnings have been suppressed.\n");
1065 } else {
1066 std::ostringstream oss;
1067 createErrorStack();
1068 dumpStack(oss, true);
1069 warnings.push_back(msg + "\n" + oss.str());
1070 }
1071}
1072
1073void EnvI::createErrorStack() {
1074 errorStack.clear();
1075 for (auto i = static_cast<unsigned int>(callStack.size()); (i--) != 0U;) {
1076 Expression* e = callStack[i]->untag();
1077 bool isCompIter = callStack[i]->isTagged();
1078 KeepAlive ka(e);
1079 errorStack.emplace_back(ka, isCompIter);
1080 }
1081}
1082
1083Call* EnvI::surroundingCall() const {
1084 if (callStack.size() >= 2) {
1085 return callStack[callStack.size() - 2]->untag()->dynamicCast<Call>();
1086 }
1087 return nullptr;
1088}
1089
1090void EnvI::cleanupExceptOutput() {
1091 cmap.clear();
1092 _cseMap.clear();
1093 delete _flat;
1094 delete model;
1095 delete originalModel;
1096 _flat = nullptr;
1097 model = nullptr;
1098}
1099
1100CallStackItem::CallStackItem(EnvI& env0, Expression* e) : env(env0) {
1101 if (e->isa<VarDecl>()) {
1102 env.idStack.push_back(static_cast<int>(env.callStack.size()));
1103 }
1104 if (e->isa<Call>() && e->cast<Call>()->id() == "redundant_constraint") {
1105 env.inRedundantConstraint++;
1106 }
1107 if (e->ann().contains(constants().ann.maybe_partial)) {
1108 env.inMaybePartial++;
1109 }
1110 env.callStack.push_back(e);
1111 env.maxCallStack = std::max(env.maxCallStack, static_cast<unsigned int>(env.callStack.size()));
1112}
1113CallStackItem::CallStackItem(EnvI& env0, Id* ident, IntVal i) : env(env0) {
1114 Expression* ee = ident->tag();
1115 env.callStack.push_back(ee);
1116 env.maxCallStack = std::max(env.maxCallStack, static_cast<unsigned int>(env.callStack.size()));
1117}
1118CallStackItem::~CallStackItem() {
1119 try {
1120 Expression* e = env.callStack.back()->untag();
1121 if (e->isa<VarDecl>()) {
1122 env.idStack.pop_back();
1123 }
1124 if (e->isa<Call>() && e->cast<Call>()->id() == "redundant_constraint") {
1125 env.inRedundantConstraint--;
1126 }
1127 if (e->ann().contains(constants().ann.maybe_partial)) {
1128 env.inMaybePartial--;
1129 }
1130 env.callStack.pop_back();
1131 } catch (std::exception&) {
1132 assert(false); // Invariant: These Env vector operations will never throw an exception
1133 }
1134}
1135
1136FlatteningError::FlatteningError(EnvI& env, const Location& loc, const std::string& msg)
1137 : LocationException(env, loc, msg) {}
1138
1139Env::Env(Model* m, std::ostream& outstream, std::ostream& errstream)
1140 : _e(new EnvI(m, outstream, errstream)) {}
1141Env::~Env() { delete _e; }
1142
1143Model* Env::model() { return _e->model; }
1144void Env::model(Model* m) { _e->model = m; }
1145Model* Env::flat() { return _e->flat(); }
1146void Env::swap() { _e->swap(); }
1147Model* Env::output() { return _e->output; }
1148
1149std::ostream& Env::evalOutput(std::ostream& os, std::ostream& log) {
1150 return _e->evalOutput(os, log);
1151}
1152EnvI& Env::envi() { return *_e; }
1153const EnvI& Env::envi() const { return *_e; }
1154std::ostream& Env::dumpErrorStack(std::ostream& os) { return _e->dumpStack(os, true); }
1155
1156bool EnvI::dumpPath(std::ostream& os, bool force) {
1157 force = force ? force : fopts.collectMznPaths;
1158 if (callStack.size() > maxPathDepth) {
1159 if (!force && currentPassNumber >= finalPassNumber - 1) {
1160 return false;
1161 }
1162 maxPathDepth = static_cast<int>(callStack.size());
1163 }
1164
1165 auto lastError = static_cast<unsigned int>(callStack.size());
1166
1167 std::string major_sep = ";";
1168 std::string minor_sep = "|";
1169 for (unsigned int i = 0; i < lastError; i++) {
1170 Expression* e = callStack[i]->untag();
1171 bool isCompIter = callStack[i]->isTagged();
1172 Location loc = e->loc();
1173 auto findFilename = _filenameSet.find(loc.filename());
1174 if (findFilename == _filenameSet.end()) {
1175 if (!force && currentPassNumber >= finalPassNumber - 1) {
1176 return false;
1177 }
1178 _filenameSet.insert(loc.filename());
1179 }
1180
1181 // If this call is not a dummy StringLit with empty Location (so that deferred compilation
1182 // doesn't drop the paths)
1183 if (e->eid() != Expression::E_STRINGLIT || (loc.firstLine() != 0U) ||
1184 (loc.firstColumn() != 0U) || (loc.lastLine() != 0U) || (loc.lastColumn() != 0U)) {
1185 os << loc.filename() << minor_sep << loc.firstLine() << minor_sep << loc.firstColumn()
1186 << minor_sep << loc.lastLine() << minor_sep << loc.lastColumn() << minor_sep;
1187 switch (e->eid()) {
1188 case Expression::E_INTLIT:
1189 os << "il" << minor_sep << *e;
1190 break;
1191 case Expression::E_FLOATLIT:
1192 os << "fl" << minor_sep << *e;
1193 break;
1194 case Expression::E_SETLIT:
1195 os << "sl" << minor_sep << *e;
1196 break;
1197 case Expression::E_BOOLLIT:
1198 os << "bl" << minor_sep << *e;
1199 break;
1200 case Expression::E_STRINGLIT:
1201 os << "stl" << minor_sep << *e;
1202 break;
1203 case Expression::E_ID:
1204 if (isCompIter) {
1205 // if (e->cast<Id>()->decl()->e()->type().isPar())
1206 os << *e << "=" << *e->cast<Id>()->decl()->e();
1207 // else
1208 // os << *e << "=?";
1209 } else {
1210 os << "id" << minor_sep << *e;
1211 }
1212 break;
1213 case Expression::E_ANON:
1214 os << "anon";
1215 break;
1216 case Expression::E_ARRAYLIT:
1217 os << "al";
1218 break;
1219 case Expression::E_ARRAYACCESS:
1220 os << "aa";
1221 break;
1222 case Expression::E_COMP: {
1223 const Comprehension* cmp = e->cast<Comprehension>();
1224 if (cmp->set()) {
1225 os << "sc";
1226 } else {
1227 os << "ac";
1228 }
1229 } break;
1230 case Expression::E_ITE:
1231 os << "ite";
1232 break;
1233 case Expression::E_BINOP:
1234 os << "bin" << minor_sep << e->cast<BinOp>()->opToString();
1235 break;
1236 case Expression::E_UNOP:
1237 os << "un" << minor_sep << e->cast<UnOp>()->opToString();
1238 break;
1239 case Expression::E_CALL:
1240 if (fopts.onlyToplevelPaths) {
1241 return false;
1242 }
1243 os << "ca" << minor_sep << e->cast<Call>()->id();
1244 break;
1245 case Expression::E_VARDECL:
1246 os << "vd";
1247 break;
1248 case Expression::E_LET:
1249 os << "l";
1250 break;
1251 case Expression::E_TI:
1252 os << "ti";
1253 break;
1254 case Expression::E_TIID:
1255 os << "ty";
1256 break;
1257 default:
1258 assert(false);
1259 os << "unknown expression (internal error)";
1260 break;
1261 }
1262 os << major_sep;
1263 } else {
1264 os << e->cast<StringLit>()->v() << major_sep;
1265 }
1266 }
1267 return true;
1268}
1269
1270std::ostream& EnvI::dumpStack(std::ostream& os, bool errStack) {
1271 int lastError = 0;
1272
1273 std::vector<Expression*> errStackCopy;
1274 if (errStack) {
1275 errStackCopy.resize(errorStack.size());
1276 for (unsigned int i = 0; i < errorStack.size(); i++) {
1277 Expression* e = errorStack[i].first();
1278 if (errorStack[i].second) {
1279 e = e->tag();
1280 }
1281 errStackCopy[i] = e;
1282 }
1283 }
1284
1285 std::vector<Expression*>& stack = errStack ? errStackCopy : callStack;
1286
1287 for (; lastError < stack.size(); lastError++) {
1288 Expression* e = stack[lastError]->untag();
1289 bool isCompIter = stack[lastError]->isTagged();
1290 if (e->loc().isIntroduced()) {
1291 continue;
1292 }
1293 if (!isCompIter && e->isa<Id>()) {
1294 break;
1295 }
1296 }
1297
1298 if (lastError == 0 && !stack.empty() && stack[0]->untag()->isa<Id>()) {
1299 Expression* e = stack[0]->untag();
1300 ASTString newloc_f = e->loc().filename();
1301 if (!e->loc().isIntroduced()) {
1302 unsigned int newloc_l = e->loc().firstLine();
1303 os << " " << newloc_f << ":" << newloc_l << ":" << std::endl;
1304 os << " in variable declaration " << *e << std::endl;
1305 }
1306 } else {
1307 ASTString curloc_f;
1308 long long int curloc_l = -1;
1309
1310 for (int i = lastError - 1; i >= 0; i--) {
1311 Expression* e = stack[i]->untag();
1312 bool isCompIter = stack[i]->isTagged();
1313 ASTString newloc_f = e->loc().filename();
1314 if (e->loc().isIntroduced()) {
1315 continue;
1316 }
1317 auto newloc_l = static_cast<long long int>(e->loc().firstLine());
1318 if (newloc_f != curloc_f || newloc_l != curloc_l) {
1319 os << " " << newloc_f << ":" << newloc_l << ":" << std::endl;
1320 curloc_f = newloc_f;
1321 curloc_l = newloc_l;
1322 }
1323 if (isCompIter) {
1324 os << " with ";
1325 } else {
1326 os << " in ";
1327 }
1328 switch (e->eid()) {
1329 case Expression::E_INTLIT:
1330 os << "integer literal" << std::endl;
1331 break;
1332 case Expression::E_FLOATLIT:
1333 os << "float literal" << std::endl;
1334 break;
1335 case Expression::E_SETLIT:
1336 os << "set literal" << std::endl;
1337 break;
1338 case Expression::E_BOOLLIT:
1339 os << "bool literal" << std::endl;
1340 break;
1341 case Expression::E_STRINGLIT:
1342 os << "string literal" << std::endl;
1343 break;
1344 case Expression::E_ID:
1345 if (isCompIter) {
1346 if ((e->cast<Id>()->decl()->e() != nullptr) &&
1347 e->cast<Id>()->decl()->e()->type().isPar()) {
1348 os << *e << " = " << *e->cast<Id>()->decl()->e() << std::endl;
1349 } else {
1350 os << *e << " = <expression>" << std::endl;
1351 }
1352 } else {
1353 os << "identifier" << *e << std::endl;
1354 }
1355 break;
1356 case Expression::E_ANON:
1357 os << "anonymous variable" << std::endl;
1358 break;
1359 case Expression::E_ARRAYLIT:
1360 os << "array literal" << std::endl;
1361 break;
1362 case Expression::E_ARRAYACCESS:
1363 os << "array access" << std::endl;
1364 break;
1365 case Expression::E_COMP: {
1366 const Comprehension* cmp = e->cast<Comprehension>();
1367 if (cmp->set()) {
1368 os << "set ";
1369 } else {
1370 os << "array ";
1371 }
1372 os << "comprehension expression" << std::endl;
1373 } break;
1374 case Expression::E_ITE:
1375 os << "if-then-else expression" << std::endl;
1376 break;
1377 case Expression::E_BINOP:
1378 os << "binary " << e->cast<BinOp>()->opToString() << " operator expression" << std::endl;
1379 break;
1380 case Expression::E_UNOP:
1381 os << "unary " << e->cast<UnOp>()->opToString() << " operator expression" << std::endl;
1382 break;
1383 case Expression::E_CALL:
1384 os << "call '" << e->cast<Call>()->id() << "'" << std::endl;
1385 break;
1386 case Expression::E_VARDECL: {
1387 GCLock lock;
1388 os << "variable declaration for '" << e->cast<VarDecl>()->id()->str() << "'" << std::endl;
1389 } break;
1390 case Expression::E_LET:
1391 os << "let expression" << std::endl;
1392 break;
1393 case Expression::E_TI:
1394 os << "type-inst expression" << std::endl;
1395 break;
1396 case Expression::E_TIID:
1397 os << "type identifier" << std::endl;
1398 break;
1399 default:
1400 assert(false);
1401 os << "unknown expression (internal error)" << std::endl;
1402 break;
1403 }
1404 }
1405 }
1406 return os;
1407}
1408
1409void populate_output(Env& env) {
1410 EnvI& envi = env.envi();
1411 Model* _flat = envi.flat();
1412 Model* _output = envi.output;
1413 std::vector<Expression*> outputVars;
1414 for (VarDeclIterator it = _flat->vardecls().begin(); it != _flat->vardecls().end(); ++it) {
1415 VarDecl* vd = it->e();
1416 Annotation& ann = vd->ann();
1417 ArrayLit* dims = nullptr;
1418 bool has_output_ann = false;
1419 if (!ann.isEmpty()) {
1420 for (ExpressionSetIter ait = ann.begin(); ait != ann.end(); ++ait) {
1421 if (Call* c = (*ait)->dynamicCast<Call>()) {
1422 if (c->id() == constants().ann.output_array) {
1423 dims = c->arg(0)->cast<ArrayLit>();
1424 has_output_ann = true;
1425 break;
1426 }
1427 } else if ((*ait)->isa<Id>() &&
1428 (*ait)->cast<Id>()->str() == constants().ann.output_var->str()) {
1429 has_output_ann = true;
1430 }
1431 }
1432 if (has_output_ann) {
1433 std::ostringstream s;
1434 s << vd->id()->str() << " = ";
1435
1436 auto* vd_output = copy(env.envi(), vd)->cast<VarDecl>();
1437 Type vd_t = vd_output->type();
1438 vd_t.ti(Type::TI_PAR);
1439 vd_output->type(vd_t);
1440 vd_output->ti()->type(vd_t);
1441
1442 if (dims != nullptr) {
1443 std::vector<TypeInst*> ranges(dims->size());
1444 s << "array" << dims->size() << "d(";
1445 for (unsigned int i = 0; i < dims->size(); i++) {
1446 IntSetVal* idxset = eval_intset(envi, (*dims)[i]);
1447 ranges[i] = new TypeInst(Location().introduce(), Type(),
1448 new SetLit(Location().introduce(), idxset));
1449 s << *idxset << ",";
1450 }
1451 Type t = vd_t;
1452 vd_t.dim(static_cast<int>(dims->size()));
1453 vd_output->type(t);
1454 vd_output->ti(new TypeInst(Location().introduce(), vd_t, ranges));
1455 }
1456 _output->addItem(new VarDeclI(Location().introduce(), vd_output));
1457
1458 auto* sl = new StringLit(Location().introduce(), s.str());
1459 outputVars.push_back(sl);
1460
1461 std::vector<Expression*> showArgs(1);
1462 showArgs[0] = vd_output->id();
1463 Call* show = new Call(Location().introduce(), constants().ids.show, showArgs);
1464 show->type(Type::parstring());
1465 FunctionI* fi = _flat->matchFn(envi, show, false);
1466 assert(fi);
1467 show->decl(fi);
1468 outputVars.push_back(show);
1469 std::string ends = dims != nullptr ? ")" : "";
1470 ends += ";\n";
1471 auto* eol = new StringLit(Location().introduce(), ends);
1472 outputVars.push_back(eol);
1473 }
1474 }
1475 }
1476 auto* newOutputItem =
1477 new OutputI(Location().introduce(), new ArrayLit(Location().introduce(), outputVars));
1478 _output->addItem(newOutputItem);
1479 envi.flat()->mergeStdLib(envi, _output);
1480}
1481
1482std::ostream& EnvI::evalOutput(std::ostream& os, std::ostream& log) {
1483 GCLock lock;
1484 warnings.clear();
1485 ArrayLit* al = eval_array_lit(*this, output->outputItem()->e());
1486 bool fLastEOL = true;
1487 for (unsigned int i = 0; i < al->size(); i++) {
1488 std::string s = eval_string(*this, (*al)[i]);
1489 if (!s.empty()) {
1490 os << s;
1491 fLastEOL = ('\n' == s.back());
1492 }
1493 }
1494 if (!fLastEOL) {
1495 os << '\n';
1496 }
1497 for (auto w : warnings) {
1498 log << " WARNING: " << w << "\n";
1499 }
1500 return os;
1501}
1502
1503const std::vector<std::string>& Env::warnings() { return envi().warnings; }
1504
1505void Env::clearWarnings() { envi().warnings.clear(); }
1506
1507unsigned int Env::maxCallStack() const { return envi().maxCallStack; }
1508
1509void check_index_sets(EnvI& env, VarDecl* vd, Expression* e) {
1510 ASTExprVec<TypeInst> tis = vd->ti()->ranges();
1511 std::vector<TypeInst*> newtis(tis.size());
1512 bool needNewTypeInst = false;
1513 GCLock lock;
1514 switch (e->eid()) {
1515 case Expression::E_ID: {
1516 Id* id = e->cast<Id>();
1517 ASTExprVec<TypeInst> e_tis = id->decl()->ti()->ranges();
1518 assert(tis.size() == e_tis.size());
1519 for (unsigned int i = 0; i < tis.size(); i++) {
1520 if (tis[i]->domain() == nullptr) {
1521 newtis[i] = e_tis[i];
1522 needNewTypeInst = true;
1523 } else {
1524 IntSetVal* isv0 = eval_intset(env, tis[i]->domain());
1525 IntSetVal* isv1 = eval_intset(env, e_tis[i]->domain());
1526 if (!isv0->equal(isv1)) {
1527 std::ostringstream oss;
1528 oss << "Index set mismatch. Declared index " << (tis.size() == 1 ? "set" : "sets");
1529 oss << " of `" << *vd->id() << "' " << (tis.size() == 1 ? "is [" : "are [");
1530 for (unsigned int j = 0; j < tis.size(); j++) {
1531 if (tis[j]->domain() != nullptr) {
1532 oss << *eval_intset(env, tis[j]->domain());
1533 } else {
1534 oss << "int";
1535 }
1536 if (j < tis.size() - 1) {
1537 oss << ", ";
1538 }
1539 }
1540 oss << "], but is assigned to array `" << *id << "' with index "
1541 << (tis.size() == 1 ? "set [" : "sets [");
1542 for (unsigned int j = 0; j < e_tis.size(); j++) {
1543 oss << *eval_intset(env, e_tis[j]->domain());
1544 if (j < e_tis.size() - 1) {
1545 oss << ", ";
1546 }
1547 }
1548 oss << "]. You may need to coerce the index sets using the array" << tis.size()
1549 << "d function.";
1550 throw EvalError(env, vd->loc(), oss.str());
1551 }
1552 newtis[i] = tis[i];
1553 }
1554 }
1555 } break;
1556 case Expression::E_ARRAYLIT: {
1557 auto* al = e->cast<ArrayLit>();
1558 for (unsigned int i = 0; i < tis.size(); i++) {
1559 if (tis[i]->domain() == nullptr) {
1560 newtis[i] = new TypeInst(
1561 Location().introduce(), Type(),
1562 new SetLit(Location().introduce(), IntSetVal::a(al->min(i), al->max(i))));
1563 needNewTypeInst = true;
1564 } else if (i == 0 || al->size() != 0) {
1565 IntSetVal* isv = eval_intset(env, tis[i]->domain());
1566 assert(isv->size() <= 1);
1567 if ((isv->size() == 0 && al->min(i) <= al->max(i)) ||
1568 (isv->size() != 0 && (isv->min(0) != al->min(i) || isv->max(0) != al->max(i)))) {
1569 std::ostringstream oss;
1570 oss << "Index set mismatch. Declared index " << (tis.size() == 1 ? "set" : "sets");
1571 oss << " of `" << *vd->id() << "' " << (tis.size() == 1 ? "is [" : "are [");
1572 for (unsigned int j = 0; j < tis.size(); j++) {
1573 if (tis[j]->domain() != nullptr) {
1574 oss << *eval_intset(env, tis[j]->domain());
1575 } else {
1576 oss << "int";
1577 }
1578 if (j < tis.size() - 1) {
1579 oss << ",";
1580 }
1581 }
1582 oss << "], but is assigned to array with index "
1583 << (tis.size() == 1 ? "set [" : "sets [");
1584 for (unsigned int j = 0; j < al->dims(); j++) {
1585 oss << al->min(j) << ".." << al->max(j);
1586 if (j < al->dims() - 1) {
1587 oss << ", ";
1588 }
1589 }
1590 oss << "]. You may need to coerce the index sets using the array" << tis.size()
1591 << "d function.";
1592 throw EvalError(env, vd->loc(), oss.str());
1593 }
1594 newtis[i] = tis[i];
1595 }
1596 }
1597 } break;
1598 default:
1599 throw InternalError("not supported yet");
1600 }
1601 if (needNewTypeInst) {
1602 auto* tic = copy(env, vd->ti())->cast<TypeInst>();
1603 tic->setRanges(newtis);
1604 vd->ti(tic);
1605 }
1606}
1607
1608/// Turn \a c into domain constraints if possible.
1609/// Return whether \a c is still required in the model.
1610bool check_domain_constraints(EnvI& env, Call* c) {
1611 if (env.fopts.recordDomainChanges) {
1612 return true;
1613 }
1614 if (c->id() == constants().ids.int_.le) {
1615 Expression* e0 = c->arg(0);
1616 Expression* e1 = c->arg(1);
1617 if (e0->type().isPar() && e1->isa<Id>()) {
1618 // greater than
1619 Id* id = e1->cast<Id>();
1620 IntVal lb = eval_int(env, e0);
1621 if (id->decl()->ti()->domain() != nullptr) {
1622 IntSetVal* domain = eval_intset(env, id->decl()->ti()->domain());
1623 if (domain->min() >= lb) {
1624 return false;
1625 }
1626 if (domain->max() < lb) {
1627 env.fail();
1628 return false;
1629 }
1630 IntSetRanges dr(domain);
1631 Ranges::Const<IntVal> cr(lb, IntVal::infinity());
1632 Ranges::Inter<IntVal, IntSetRanges, Ranges::Const<IntVal>> i(dr, cr);
1633 IntSetVal* newibv = IntSetVal::ai(i);
1634 id->decl()->ti()->domain(new SetLit(Location().introduce(), newibv));
1635 id->decl()->ti()->setComputedDomain(false);
1636 } else {
1637 id->decl()->ti()->domain(
1638 new SetLit(Location().introduce(), IntSetVal::a(lb, IntVal::infinity())));
1639 }
1640 return false;
1641 }
1642 if (e1->type().isPar() && e0->isa<Id>()) {
1643 // less than
1644 Id* id = e0->cast<Id>();
1645 IntVal ub = eval_int(env, e1);
1646 if (id->decl()->ti()->domain() != nullptr) {
1647 IntSetVal* domain = eval_intset(env, id->decl()->ti()->domain());
1648 if (domain->max() <= ub) {
1649 return false;
1650 }
1651 if (domain->min() > ub) {
1652 env.fail();
1653 return false;
1654 }
1655 IntSetRanges dr(domain);
1656 Ranges::Const<IntVal> cr(-IntVal::infinity(), ub);
1657 Ranges::Inter<IntVal, IntSetRanges, Ranges::Const<IntVal>> i(dr, cr);
1658 IntSetVal* newibv = IntSetVal::ai(i);
1659 id->decl()->ti()->domain(new SetLit(Location().introduce(), newibv));
1660 id->decl()->ti()->setComputedDomain(false);
1661 } else {
1662 id->decl()->ti()->domain(
1663 new SetLit(Location().introduce(), IntSetVal::a(-IntVal::infinity(), ub)));
1664 }
1665 }
1666 } else if (c->id() == constants().ids.int_.lin_le) {
1667 auto* al_c = follow_id(c->arg(0))->cast<ArrayLit>();
1668 if (al_c->size() == 1) {
1669 auto* al_x = follow_id(c->arg(1))->cast<ArrayLit>();
1670 IntVal coeff = eval_int(env, (*al_c)[0]);
1671 IntVal y = eval_int(env, c->arg(2));
1672 IntVal lb = -IntVal::infinity();
1673 IntVal ub = IntVal::infinity();
1674 IntVal r = y % coeff;
1675 if (coeff >= 0) {
1676 ub = y / coeff;
1677 if (r < 0) {
1678 --ub;
1679 }
1680 } else {
1681 lb = y / coeff;
1682 if (r < 0) {
1683 ++lb;
1684 }
1685 }
1686 if (Id* id = (*al_x)[0]->dynamicCast<Id>()) {
1687 if (id->decl()->ti()->domain() != nullptr) {
1688 IntSetVal* domain = eval_intset(env, id->decl()->ti()->domain());
1689 if (domain->max() <= ub && domain->min() >= lb) {
1690 return false;
1691 }
1692 if (domain->min() > ub || domain->max() < lb) {
1693 env.fail();
1694 return false;
1695 }
1696 IntSetRanges dr(domain);
1697 Ranges::Const<IntVal> cr(lb, ub);
1698 Ranges::Inter<IntVal, IntSetRanges, Ranges::Const<IntVal>> i(dr, cr);
1699 IntSetVal* newibv = IntSetVal::ai(i);
1700 id->decl()->ti()->domain(new SetLit(Location().introduce(), newibv));
1701 id->decl()->ti()->setComputedDomain(false);
1702 } else {
1703 id->decl()->ti()->domain(new SetLit(Location().introduce(), IntSetVal::a(lb, ub)));
1704 }
1705 return false;
1706 }
1707 }
1708 }
1709 return true;
1710}
1711
1712KeepAlive bind(EnvI& env, Ctx ctx, VarDecl* vd, Expression* e) {
1713 assert(e == nullptr || !e->isa<VarDecl>());
1714 if (vd == constants().varIgnore) {
1715 return e;
1716 }
1717 if (Id* ident = e->dynamicCast<Id>()) {
1718 if (ident->decl() != nullptr) {
1719 auto* e_vd = follow_id_to_decl(ident)->cast<VarDecl>();
1720 e = e_vd->id();
1721 if (!env.inReverseMapVar && ctx.b != C_ROOT && e->type() == Type::varbool()) {
1722 add_ctx_ann(e_vd, ctx.b);
1723 if (e_vd != ident->decl()) {
1724 add_ctx_ann(ident->decl(), ctx.b);
1725 }
1726 }
1727 }
1728 }
1729 if (ctx.neg) {
1730 assert(e->type().bt() == Type::BT_BOOL);
1731 if (vd == constants().varTrue) {
1732 if (!isfalse(env, e)) {
1733 if (Id* id = e->dynamicCast<Id>()) {
1734 while (id != nullptr) {
1735 assert(id->decl() != nullptr);
1736 if ((id->decl()->ti()->domain() != nullptr) &&
1737 istrue(env, id->decl()->ti()->domain())) {
1738 GCLock lock;
1739 env.flatAddItem(new ConstraintI(Location().introduce(), constants().literalFalse));
1740 } else {
1741 GCLock lock;
1742 std::vector<Expression*> args(2);
1743 args[0] = id;
1744 args[1] = constants().literalFalse;
1745 Call* c = new Call(Location().introduce(), constants().ids.bool_eq, args);
1746 c->decl(env.model->matchFn(env, c, false));
1747 c->type(c->decl()->rtype(env, args, false));
1748 if (c->decl()->e() != nullptr) {
1749 flat_exp(env, Ctx(), c, constants().varTrue, constants().varTrue);
1750 }
1751 set_computed_domain(env, id->decl(), constants().literalFalse,
1752 id->decl()->ti()->computedDomain());
1753 }
1754 id = id->decl()->e() != nullptr ? id->decl()->e()->dynamicCast<Id>() : nullptr;
1755 }
1756 return constants().literalTrue;
1757 }
1758 GC::lock();
1759 Call* bn = new Call(e->loc(), constants().ids.bool_not, {e});
1760 bn->type(e->type());
1761 bn->decl(env.model->matchFn(env, bn, false));
1762 KeepAlive ka(bn);
1763 GC::unlock();
1764 EE ee = flat_exp(env, Ctx(), bn, vd, constants().varTrue);
1765 return ee.r;
1766 }
1767 return constants().literalTrue;
1768 }
1769 GC::lock();
1770 Call* bn = new Call(e->loc(), constants().ids.bool_not, {e});
1771 bn->type(e->type());
1772 bn->decl(env.model->matchFn(env, bn, false));
1773 KeepAlive ka(bn);
1774 GC::unlock();
1775 EE ee = flat_exp(env, Ctx(), bn, vd, constants().varTrue);
1776 return ee.r;
1777 }
1778 if (vd == constants().varTrue) {
1779 if (!istrue(env, e)) {
1780 if (Id* id = e->dynamicCast<Id>()) {
1781 assert(id->decl() != nullptr);
1782 while (id != nullptr) {
1783 if ((id->decl()->ti()->domain() != nullptr) && isfalse(env, id->decl()->ti()->domain())) {
1784 GCLock lock;
1785 env.flatAddItem(new ConstraintI(Location().introduce(), constants().literalFalse));
1786 } else if (id->decl()->ti()->domain() == nullptr) {
1787 GCLock lock;
1788 std::vector<Expression*> args(2);
1789 args[0] = id;
1790 args[1] = constants().literalTrue;
1791 Call* c = new Call(Location().introduce(), constants().ids.bool_eq, args);
1792 c->decl(env.model->matchFn(env, c, false));
1793 c->type(c->decl()->rtype(env, args, false));
1794 if (c->decl()->e() != nullptr) {
1795 flat_exp(env, Ctx(), c, constants().varTrue, constants().varTrue);
1796 }
1797 set_computed_domain(env, id->decl(), constants().literalTrue,
1798 id->decl()->ti()->computedDomain());
1799 }
1800 id = id->decl()->e() != nullptr ? id->decl()->e()->dynamicCast<Id>() : nullptr;
1801 }
1802 } else {
1803 GCLock lock;
1804 // extract domain information from added constraint if possible
1805 if (!e->isa<Call>() || check_domain_constraints(env, e->cast<Call>())) {
1806 env.flatAddItem(new ConstraintI(Location().introduce(), e));
1807 }
1808 }
1809 }
1810 return constants().literalTrue;
1811 }
1812 if (vd == constants().varFalse) {
1813 if (!isfalse(env, e)) {
1814 throw InternalError("not supported yet");
1815 }
1816 return constants().literalTrue;
1817 }
1818 if (vd == nullptr) {
1819 if (e == nullptr) {
1820 return nullptr;
1821 }
1822 switch (e->eid()) {
1823 case Expression::E_INTLIT:
1824 case Expression::E_FLOATLIT:
1825 case Expression::E_BOOLLIT:
1826 case Expression::E_STRINGLIT:
1827 case Expression::E_ANON:
1828 case Expression::E_ID:
1829 case Expression::E_TIID:
1830 case Expression::E_SETLIT:
1831 case Expression::E_VARDECL:
1832 case Expression::E_BINOP: // TODO: should not happen once operators are evaluated
1833 case Expression::E_UNOP: // TODO: should not happen once operators are evaluated
1834 return e;
1835 case Expression::E_ARRAYACCESS:
1836 case Expression::E_COMP:
1837 case Expression::E_ITE:
1838 case Expression::E_LET:
1839 case Expression::E_TI:
1840 throw InternalError("unevaluated expression");
1841 case Expression::E_ARRAYLIT: {
1842 GCLock lock;
1843 auto* al = e->cast<ArrayLit>();
1844 /// TODO: review if limit of 10 is a sensible choice
1845 if (al->type().bt() == Type::BT_ANN || al->size() <= 10) {
1846 return e;
1847 }
1848
1849 auto it = env.cseMapFind(al);
1850 if (it != env.cseMapEnd()) {
1851 return it->second.r()->cast<VarDecl>()->id();
1852 }
1853
1854 std::vector<TypeInst*> ranges(al->dims());
1855 for (unsigned int i = 0; i < ranges.size(); i++) {
1856 ranges[i] = new TypeInst(
1857 e->loc(), Type(),
1858 new SetLit(Location().introduce(), IntSetVal::a(al->min(i), al->max(i))));
1859 }
1860 ASTExprVec<TypeInst> ranges_v(ranges);
1861 assert(!al->type().isbot());
1862 Expression* domain = nullptr;
1863 if (al->size() > 0 && (*al)[0]->type().isint()) {
1864 IntVal min = IntVal::infinity();
1865 IntVal max = -IntVal::infinity();
1866 for (unsigned int i = 0; i < al->size(); i++) {
1867 IntBounds ib = compute_int_bounds(env, (*al)[i]);
1868 if (!ib.valid) {
1869 min = -IntVal::infinity();
1870 max = IntVal::infinity();
1871 break;
1872 }
1873 min = std::min(min, ib.l);
1874 max = std::max(max, ib.u);
1875 }
1876 if (min != -IntVal::infinity() && max != IntVal::infinity()) {
1877 domain = new SetLit(Location().introduce(), IntSetVal::a(min, max));
1878 }
1879 }
1880 auto* ti = new TypeInst(e->loc(), al->type(), ranges_v, domain);
1881 if (domain != nullptr) {
1882 ti->setComputedDomain(true);
1883 }
1884
1885 VarDecl* nvd = new_vardecl(env, ctx, ti, nullptr, nullptr, al);
1886 EE ee(nvd, nullptr);
1887 env.cseMapInsert(al, ee);
1888 env.cseMapInsert(nvd->e(), ee);
1889 return nvd->id();
1890 }
1891 case Expression::E_CALL: {
1892 if (e->type().isAnn()) {
1893 return e;
1894 }
1895 GCLock lock;
1896 /// TODO: handle array types
1897 auto* ti = new TypeInst(Location().introduce(), e->type());
1898 VarDecl* nvd = new_vardecl(env, ctx, ti, nullptr, nullptr, e);
1899 if (nvd->e()->type().bt() == Type::BT_INT && nvd->e()->type().dim() == 0) {
1900 IntSetVal* ibv = nullptr;
1901 if (nvd->e()->type().isSet()) {
1902 ibv = compute_intset_bounds(env, nvd->e());
1903 } else {
1904 IntBounds ib = compute_int_bounds(env, nvd->e());
1905 if (ib.valid) {
1906 ibv = IntSetVal::a(ib.l, ib.u);
1907 }
1908 }
1909 if (ibv != nullptr) {
1910 Id* id = nvd->id();
1911 while (id != nullptr) {
1912 bool is_computed = id->decl()->ti()->computedDomain();
1913 if (id->decl()->ti()->domain() != nullptr) {
1914 IntSetVal* domain = eval_intset(env, id->decl()->ti()->domain());
1915 IntSetRanges dr(domain);
1916 IntSetRanges ibr(ibv);
1917 Ranges::Inter<IntVal, IntSetRanges, IntSetRanges> i(dr, ibr);
1918 IntSetVal* newibv = IntSetVal::ai(i);
1919 if (ibv->card() == newibv->card()) {
1920 is_computed = true;
1921 } else {
1922 ibv = newibv;
1923 }
1924 } else {
1925 is_computed = true;
1926 }
1927 if (id->type().st() == Type::ST_PLAIN && ibv->size() == 0) {
1928 env.fail();
1929 } else {
1930 set_computed_domain(env, id->decl(), new SetLit(Location().introduce(), ibv),
1931 is_computed);
1932 }
1933 id = id->decl()->e() != nullptr ? id->decl()->e()->dynamicCast<Id>() : nullptr;
1934 }
1935 }
1936 } else if (nvd->e()->type().isbool()) {
1937 add_ctx_ann(nvd, ctx.b);
1938 } else if (nvd->e()->type().bt() == Type::BT_FLOAT && nvd->e()->type().dim() == 0) {
1939 FloatBounds fb = compute_float_bounds(env, nvd->e());
1940 FloatSetVal* ibv = LinearTraits<FloatLit>::intersectDomain(nullptr, fb.l, fb.u);
1941 if (fb.valid) {
1942 Id* id = nvd->id();
1943 while (id != nullptr) {
1944 bool is_computed = id->decl()->ti()->computedDomain();
1945 if (id->decl()->ti()->domain() != nullptr) {
1946 FloatSetVal* domain = eval_floatset(env, id->decl()->ti()->domain());
1947 FloatSetVal* ndomain = LinearTraits<FloatLit>::intersectDomain(domain, fb.l, fb.u);
1948 if ((ibv != nullptr) && ndomain == domain) {
1949 is_computed = true;
1950 } else {
1951 ibv = ndomain;
1952 }
1953 } else {
1954 is_computed = true;
1955 }
1956 if (LinearTraits<FloatLit>::domainEmpty(ibv)) {
1957 env.fail();
1958 } else {
1959 set_computed_domain(env, id->decl(), new SetLit(Location().introduce(), ibv),
1960 is_computed);
1961 }
1962 id = id->decl()->e() != nullptr ? id->decl()->e()->dynamicCast<Id>() : nullptr;
1963 }
1964 }
1965 }
1966
1967 return nvd->id();
1968 }
1969 default:
1970 assert(false);
1971 return nullptr;
1972 }
1973 } else {
1974 if (vd->e() == nullptr) {
1975 Expression* ret = e;
1976 if (e == nullptr || (e->type().isPar() && e->type().isbool())) {
1977 GCLock lock;
1978 bool isTrue = (e == nullptr || eval_bool(env, e));
1979
1980 // Check if redefinition of bool_eq exists, if yes call it
1981 std::vector<Expression*> args(2);
1982 args[0] = vd->id();
1983 args[1] = constants().boollit(isTrue);
1984 Call* c = new Call(Location().introduce(), constants().ids.bool_eq, args);
1985 c->decl(env.model->matchFn(env, c, false));
1986 c->type(c->decl()->rtype(env, args, false));
1987 bool didRewrite = false;
1988 if (c->decl()->e() != nullptr) {
1989 flat_exp(env, Ctx(), c, constants().varTrue, constants().varTrue);
1990 didRewrite = true;
1991 }
1992
1993 vd->e(constants().boollit(isTrue));
1994 if (vd->ti()->domain() != nullptr) {
1995 if (vd->ti()->domain() != vd->e()) {
1996 env.fail();
1997 return vd->id();
1998 }
1999 } else {
2000 set_computed_domain(env, vd, vd->e(), true);
2001 }
2002 if (didRewrite) {
2003 return vd->id();
2004 }
2005 } else {
2006 if (e->type().dim() > 0) {
2007 // Check that index sets match
2008 env.errorStack.clear();
2009 check_index_sets(env, vd, e);
2010 auto* al =
2011 Expression::dynamicCast<ArrayLit>(e->isa<Id>() ? e->cast<Id>()->decl()->e() : e);
2012 if ((al != nullptr) && (vd->ti()->domain() != nullptr) &&
2013 !vd->ti()->domain()->isa<TIId>()) {
2014 if (e->type().bt() == Type::BT_INT) {
2015 IntSetVal* isv = eval_intset(env, vd->ti()->domain());
2016 for (unsigned int i = 0; i < al->size(); i++) {
2017 if (Id* id = (*al)[i]->dynamicCast<Id>()) {
2018 if (id == constants().absent) {
2019 continue;
2020 }
2021 VarDecl* vdi = id->decl();
2022 if (vdi->ti()->domain() == nullptr) {
2023 set_computed_domain(env, vdi, vd->ti()->domain(), vdi->ti()->computedDomain());
2024 } else {
2025 IntSetVal* vdi_dom = eval_intset(env, vdi->ti()->domain());
2026 IntSetRanges isvr(isv);
2027 IntSetRanges vdi_domr(vdi_dom);
2028 Ranges::Inter<IntVal, IntSetRanges, IntSetRanges> inter(isvr, vdi_domr);
2029 IntSetVal* newdom = IntSetVal::ai(inter);
2030 if (newdom->size() == 0) {
2031 env.fail();
2032 } else {
2033 IntSetRanges vdi_domr2(vdi_dom);
2034 IntSetRanges newdomr(newdom);
2035 if (!Ranges::equal(vdi_domr2, newdomr)) {
2036 set_computed_domain(env, vdi, new SetLit(Location().introduce(), newdom),
2037 false);
2038 }
2039 }
2040 }
2041 } else {
2042 // at this point, can only be a constant
2043 assert((*al)[i]->type().isPar());
2044 if (e->type().st() == Type::ST_PLAIN) {
2045 IntVal iv = eval_int(env, (*al)[i]);
2046 if (!isv->contains(iv)) {
2047 std::ostringstream oss;
2048 oss << "value " << iv << " outside declared array domain " << *isv;
2049 env.fail(oss.str());
2050 }
2051 } else {
2052 IntSetVal* aisv = eval_intset(env, (*al)[i]);
2053 IntSetRanges aisv_r(aisv);
2054 IntSetRanges isv_r(isv);
2055 if (!Ranges::subset(aisv_r, isv_r)) {
2056 std::ostringstream oss;
2057 oss << "value " << *aisv << " outside declared array domain " << *isv;
2058 env.fail(oss.str());
2059 }
2060 }
2061 }
2062 }
2063 vd->ti()->setComputedDomain(true);
2064 } else if (e->type().bt() == Type::BT_FLOAT) {
2065 FloatSetVal* fsv = eval_floatset(env, vd->ti()->domain());
2066 for (unsigned int i = 0; i < al->size(); i++) {
2067 if (Id* id = (*al)[i]->dynamicCast<Id>()) {
2068 VarDecl* vdi = id->decl();
2069 if (vdi->ti()->domain() == nullptr) {
2070 set_computed_domain(env, vdi, vd->ti()->domain(), vdi->ti()->computedDomain());
2071 } else {
2072 FloatSetVal* vdi_dom = eval_floatset(env, vdi->ti()->domain());
2073 FloatSetRanges fsvr(fsv);
2074 FloatSetRanges vdi_domr(vdi_dom);
2075 Ranges::Inter<FloatVal, FloatSetRanges, FloatSetRanges> inter(fsvr, vdi_domr);
2076 FloatSetVal* newdom = FloatSetVal::ai(inter);
2077 if (newdom->size() == 0) {
2078 env.fail();
2079 } else {
2080 FloatSetRanges vdi_domr2(vdi_dom);
2081 FloatSetRanges newdomr(newdom);
2082 if (!Ranges::equal(vdi_domr2, newdomr)) {
2083 set_computed_domain(env, vdi, new SetLit(Location().introduce(), newdom),
2084 false);
2085 }
2086 }
2087 }
2088 } else {
2089 // at this point, can only be a constant
2090 assert((*al)[i]->type().isPar());
2091 FloatVal fv = eval_float(env, (*al)[i]);
2092 if (!fsv->contains(fv)) {
2093 std::ostringstream oss;
2094 oss << "value " << fv << " outside declared array domain " << *fsv;
2095 env.fail(oss.str());
2096 }
2097 }
2098 }
2099 vd->ti()->setComputedDomain(true);
2100 }
2101 }
2102 } else if (Id* e_id = e->dynamicCast<Id>()) {
2103 if (e_id == vd->id()) {
2104 ret = vd->id();
2105 } else {
2106 ASTString cid;
2107 if (e->type().isint()) {
2108 if (e->type().isOpt()) {
2109 cid = ASTString("int_opt_eq");
2110 } else {
2111 cid = constants().ids.int_.eq;
2112 }
2113 } else if (e->type().isbool()) {
2114 if (e->type().isOpt()) {
2115 cid = ASTString("bool_opt_eq");
2116 } else {
2117 cid = constants().ids.bool_eq;
2118 }
2119 } else if (e->type().isSet()) {
2120 cid = constants().ids.set_eq;
2121 } else if (e->type().isfloat()) {
2122 cid = constants().ids.float_.eq;
2123 }
2124 if (cid != "" && env.hasReverseMapper(vd->id())) {
2125 GCLock lock;
2126 std::vector<Expression*> args(2);
2127 args[0] = vd->id();
2128 args[1] = e_id;
2129 Call* c = new Call(Location().introduce(), cid, args);
2130 c->decl(env.model->matchFn(env, c, false));
2131 c->type(c->decl()->rtype(env, args, false));
2132 if (c->type().isbool() && ctx.b != C_ROOT) {
2133 add_ctx_ann(vd, ctx.b);
2134 add_ctx_ann(e_id->decl(), ctx.b);
2135 }
2136 if (c->decl()->e() != nullptr) {
2137 flat_exp(env, Ctx(), c, constants().varTrue, constants().varTrue);
2138 ret = vd->id();
2139 vd->e(e);
2140 env.voAddExp(vd);
2141 }
2142 }
2143 }
2144 }
2145
2146 if (ret != vd->id()) {
2147 vd->e(ret);
2148 add_path_annotation(env, ret);
2149 env.voAddExp(vd);
2150 ret = vd->id();
2151 }
2152 Id* vde_id = Expression::dynamicCast<Id>(vd->e());
2153 if (vde_id == constants().absent) {
2154 // no need to do anything
2155 } else if ((vde_id != nullptr) && vde_id->decl()->ti()->domain() == nullptr) {
2156 if (vd->ti()->domain() != nullptr) {
2157 GCLock lock;
2158 Expression* vd_dom = eval_par(env, vd->ti()->domain());
2159 set_computed_domain(env, vde_id->decl(), vd_dom,
2160 vde_id->decl()->ti()->computedDomain());
2161 }
2162 } else if ((vd->e() != nullptr) && vd->e()->type().bt() == Type::BT_INT &&
2163 vd->e()->type().dim() == 0) {
2164 GCLock lock;
2165 IntSetVal* ibv = nullptr;
2166 if (vd->e()->type().isSet()) {
2167 ibv = compute_intset_bounds(env, vd->e());
2168 } else {
2169 IntBounds ib = compute_int_bounds(env, vd->e());
2170 if (ib.valid) {
2171 Call* call = vd->e()->dynamicCast<Call>();
2172 if ((call != nullptr) && call->id() == constants().ids.lin_exp) {
2173 ArrayLit* al = eval_array_lit(env, call->arg(1));
2174 if (al->size() == 1) {
2175 IntBounds check_zeroone = compute_int_bounds(env, (*al)[0]);
2176 if (check_zeroone.l == 0 && check_zeroone.u == 1) {
2177 ArrayLit* coeffs = eval_array_lit(env, call->arg(0));
2178 std::vector<IntVal> newdom(2);
2179 newdom[0] = 0;
2180 newdom[1] = eval_int(env, (*coeffs)[0]) + eval_int(env, call->arg(2));
2181 ibv = IntSetVal::a(newdom);
2182 }
2183 }
2184 }
2185 if (ibv == nullptr) {
2186 ibv = IntSetVal::a(ib.l, ib.u);
2187 }
2188 }
2189 }
2190 if (ibv != nullptr) {
2191 if (vd->ti()->domain() != nullptr) {
2192 IntSetVal* domain = eval_intset(env, vd->ti()->domain());
2193 IntSetRanges dr(domain);
2194 IntSetRanges ibr(ibv);
2195 Ranges::Inter<IntVal, IntSetRanges, IntSetRanges> i(dr, ibr);
2196 IntSetVal* newibv = IntSetVal::ai(i);
2197 if (newibv->card() == 0) {
2198 env.fail();
2199 } else if (ibv->card() == newibv->card()) {
2200 vd->ti()->setComputedDomain(true);
2201 } else {
2202 ibv = newibv;
2203 }
2204 } else {
2205 vd->ti()->setComputedDomain(true);
2206 }
2207 SetLit* ibv_l = nullptr;
2208 if (Id* rhs_ident = vd->e()->dynamicCast<Id>()) {
2209 if (rhs_ident->decl()->ti()->domain() != nullptr) {
2210 IntSetVal* rhs_domain = eval_intset(env, rhs_ident->decl()->ti()->domain());
2211 IntSetRanges dr(rhs_domain);
2212 IntSetRanges ibr(ibv);
2213 Ranges::Inter<IntVal, IntSetRanges, IntSetRanges> i(dr, ibr);
2214 IntSetVal* rhs_newibv = IntSetVal::ai(i);
2215 if (rhs_domain->card() != rhs_newibv->card()) {
2216 ibv_l = new SetLit(Location().introduce(), rhs_newibv);
2217 set_computed_domain(env, rhs_ident->decl(), ibv_l, false);
2218 if (rhs_ident->decl()->type().isOpt()) {
2219 std::vector<Expression*> args(2);
2220 args[0] = rhs_ident;
2221 args[1] = ibv_l;
2222 Call* c = new Call(Location().introduce(), "var_dom", args);
2223 c->type(Type::varbool());
2224 c->decl(env.model->matchFn(env, c, false));
2225 (void)flat_exp(env, Ctx(), c, constants().varTrue, constants().varTrue);
2226 }
2227 } else if (ibv->card() != rhs_newibv->card()) {
2228 ibv_l = new SetLit(Location().introduce(), rhs_newibv);
2229 }
2230 }
2231 }
2232 if (ibv_l == nullptr) {
2233 ibv_l = new SetLit(Location().introduce(), ibv);
2234 }
2235 set_computed_domain(env, vd, ibv_l, vd->ti()->computedDomain());
2236
2237 if (vd->type().isOpt()) {
2238 std::vector<Expression*> args(2);
2239 args[0] = vd->id();
2240 args[1] = ibv_l;
2241 Call* c = new Call(Location().introduce(), "var_dom", args);
2242 c->type(Type::varbool());
2243 c->decl(env.model->matchFn(env, c, false));
2244 (void)flat_exp(env, Ctx(), c, constants().varTrue, constants().varTrue);
2245 }
2246 }
2247 } else if ((vd->e() != nullptr) && vd->e()->type().bt() == Type::BT_FLOAT &&
2248 vd->e()->type().dim() == 0) {
2249 GCLock lock;
2250 FloatSetVal* fbv = nullptr;
2251 FloatBounds fb = compute_float_bounds(env, vd->e());
2252 if (fb.valid) {
2253 fbv = FloatSetVal::a(fb.l, fb.u);
2254 }
2255 if (fbv != nullptr) {
2256 if (vd->ti()->domain() != nullptr) {
2257 FloatSetVal* domain = eval_floatset(env, vd->ti()->domain());
2258 FloatSetRanges dr(domain);
2259 FloatSetRanges fbr(fbv);
2260 Ranges::Inter<FloatVal, FloatSetRanges, FloatSetRanges> i(dr, fbr);
2261 FloatSetVal* newfbv = FloatSetVal::ai(i);
2262 if (newfbv->size() == 0) {
2263 env.fail();
2264 }
2265 FloatSetRanges dr_eq(domain);
2266 FloatSetRanges newfbv_eq(newfbv);
2267 if (Ranges::equal(dr_eq, newfbv_eq)) {
2268 vd->ti()->setComputedDomain(true);
2269 } else {
2270 fbv = newfbv;
2271 }
2272 } else {
2273 vd->ti()->setComputedDomain(true);
2274 }
2275 SetLit* fbv_l = nullptr;
2276 if (Id* rhs_ident = vd->e()->dynamicCast<Id>()) {
2277 if (rhs_ident->decl()->ti()->domain() != nullptr) {
2278 FloatSetVal* rhs_domain = eval_floatset(env, rhs_ident->decl()->ti()->domain());
2279 FloatSetRanges dr(rhs_domain);
2280 FloatSetRanges ibr(fbv);
2281 Ranges::Inter<FloatVal, FloatSetRanges, FloatSetRanges> i(dr, ibr);
2282 FloatSetVal* rhs_newfbv = FloatSetVal::ai(i);
2283 if (rhs_domain->card() != rhs_newfbv->card()) {
2284 fbv_l = new SetLit(Location().introduce(), rhs_newfbv);
2285 set_computed_domain(env, rhs_ident->decl(), fbv_l, false);
2286 if (rhs_ident->decl()->type().isOpt()) {
2287 std::vector<Expression*> args(2);
2288 args[0] = rhs_ident;
2289 args[1] = fbv_l;
2290 Call* c = new Call(Location().introduce(), "var_dom", args);
2291 c->type(Type::varbool());
2292 c->decl(env.model->matchFn(env, c, false));
2293 (void)flat_exp(env, Ctx(), c, constants().varTrue, constants().varTrue);
2294 }
2295 } else if (fbv->card() != rhs_newfbv->card()) {
2296 fbv_l = new SetLit(Location().introduce(), rhs_newfbv);
2297 }
2298 }
2299 }
2300 fbv_l = new SetLit(Location().introduce(), fbv);
2301 set_computed_domain(env, vd, fbv_l, vd->ti()->computedDomain());
2302
2303 if (vd->type().isOpt()) {
2304 std::vector<Expression*> args(2);
2305 args[0] = vd->id();
2306 args[1] = fbv_l;
2307 Call* c = new Call(Location().introduce(), "var_dom", args);
2308 c->type(Type::varbool());
2309 c->decl(env.model->matchFn(env, c, false));
2310 (void)flat_exp(env, Ctx(), c, constants().varTrue, constants().varTrue);
2311 }
2312 }
2313 }
2314 }
2315 return ret;
2316 }
2317 if (vd == e) {
2318 return vd->id();
2319 }
2320 if (vd->e() != e) {
2321 e = follow_id_to_decl(e);
2322 if (vd == e) {
2323 return vd->id();
2324 }
2325 switch (e->eid()) {
2326 case Expression::E_BOOLLIT: {
2327 Id* id = vd->id();
2328 while (id != nullptr) {
2329 if ((id->decl()->ti()->domain() != nullptr) &&
2330 eval_bool(env, id->decl()->ti()->domain()) == e->cast<BoolLit>()->v()) {
2331 return constants().literalTrue;
2332 }
2333 if ((id->decl()->ti()->domain() != nullptr) &&
2334 eval_bool(env, id->decl()->ti()->domain()) != e->cast<BoolLit>()->v()) {
2335 GCLock lock;
2336 env.flatAddItem(new ConstraintI(Location().introduce(), constants().literalFalse));
2337 } else {
2338 GCLock lock;
2339 std::vector<Expression*> args(2);
2340 args[0] = id;
2341 args[1] = e;
2342 Call* c = new Call(Location().introduce(), constants().ids.bool_eq, args);
2343 c->decl(env.model->matchFn(env, c, false));
2344 c->type(c->decl()->rtype(env, args, false));
2345 if (c->decl()->e() != nullptr) {
2346 flat_exp(env, Ctx(), c, constants().varTrue, constants().varTrue);
2347 }
2348 set_computed_domain(env, id->decl(), e, id->decl()->ti()->computedDomain());
2349 }
2350 id = id->decl()->e() != nullptr ? id->decl()->e()->dynamicCast<Id>() : nullptr;
2351 }
2352 return constants().literalTrue;
2353 }
2354 case Expression::E_VARDECL: {
2355 auto* e_vd = e->cast<VarDecl>();
2356 if (vd->e() == e_vd->id() || e_vd->e() == vd->id()) {
2357 return vd->id();
2358 }
2359 if (e->type().dim() != 0) {
2360 throw InternalError("not supported yet");
2361 }
2362 GCLock lock;
2363 ASTString cid;
2364 if (e->type().isint()) {
2365 cid = constants().ids.int_.eq;
2366 } else if (e->type().isbool()) {
2367 cid = constants().ids.bool_eq;
2368 } else if (e->type().isSet()) {
2369 cid = constants().ids.set_eq;
2370 } else if (e->type().isfloat()) {
2371 cid = constants().ids.float_.eq;
2372 } else {
2373 throw InternalError("not yet implemented");
2374 }
2375 std::vector<Expression*> args(2);
2376 args[0] = vd->id();
2377 args[1] = e_vd->id();
2378 Call* c = new Call(vd->loc().introduce(), cid, args);
2379 c->decl(env.model->matchFn(env, c, false));
2380 c->type(c->decl()->rtype(env, args, false));
2381 flat_exp(env, Ctx(), c, constants().varTrue, constants().varTrue);
2382 return vd->id();
2383 }
2384 case Expression::E_CALL: {
2385 Call* c = e->cast<Call>();
2386 GCLock lock;
2387 Call* nc;
2388 std::vector<Expression*> args;
2389 if (c->id() == constants().ids.lin_exp) {
2390 auto* le_c = follow_id(c->arg(0))->cast<ArrayLit>();
2391 std::vector<Expression*> ncoeff(le_c->size());
2392 for (auto i = static_cast<unsigned int>(ncoeff.size()); (i--) != 0U;) {
2393 ncoeff[i] = (*le_c)[i];
2394 }
2395 ncoeff.push_back(IntLit::a(-1));
2396 args.push_back(new ArrayLit(Location().introduce(), ncoeff));
2397 args[0]->type(le_c->type());
2398 auto* le_x = follow_id(c->arg(1))->cast<ArrayLit>();
2399 std::vector<Expression*> nx(le_x->size());
2400 for (auto i = static_cast<unsigned int>(nx.size()); (i--) != 0U;) {
2401 nx[i] = (*le_x)[i];
2402 }
2403 nx.push_back(vd->id());
2404 args.push_back(new ArrayLit(Location().introduce(), nx));
2405 args[1]->type(le_x->type());
2406 args.push_back(c->arg(2));
2407 nc = new Call(c->loc().introduce(), constants().ids.lin_exp, args);
2408 nc->decl(env.model->matchFn(env, nc, false));
2409 if (nc->decl() == nullptr) {
2410 std::ostringstream ss;
2411 ss << "undeclared function or predicate " << nc->id();
2412 throw InternalError(ss.str());
2413 }
2414 nc->type(nc->decl()->rtype(env, args, false));
2415 auto* bop = new BinOp(nc->loc(), nc, BOT_EQ, IntLit::a(0));
2416 bop->type(Type::varbool());
2417 flat_exp(env, Ctx(), bop, constants().varTrue, constants().varTrue);
2418 return vd->id();
2419 }
2420 args.resize(c->argCount());
2421 for (auto i = static_cast<unsigned int>(args.size()); (i--) != 0U;) {
2422 args[i] = c->arg(i);
2423 }
2424 args.push_back(vd->id());
2425 ASTString nid = c->id();
2426
2427 if (c->id() == constants().ids.exists) {
2428 nid = constants().ids.array_bool_or;
2429 } else if (c->id() == constants().ids.forall) {
2430 nid = constants().ids.array_bool_and;
2431 } else if (vd->type().isbool()) {
2432 if (env.fopts.enableHalfReification && vd->ann().contains(constants().ctx.pos)) {
2433 nid = env.halfReifyId(c->id());
2434 if (env.model->matchFn(env, nid, args, false) == nullptr) {
2435 nid = env.reifyId(c->id());
2436 }
2437 } else {
2438 nid = env.reifyId(c->id());
2439 }
2440 }
2441 nc = new Call(c->loc().introduce(), nid, args);
2442 FunctionI* nc_decl = env.model->matchFn(env, nc, false);
2443 if (nc_decl == nullptr) {
2444 std::ostringstream ss;
2445 ss << "undeclared function or predicate " << nc->id();
2446 throw InternalError(ss.str());
2447 }
2448 nc->decl(nc_decl);
2449 nc->type(nc->decl()->rtype(env, args, false));
2450 make_defined_var(vd, nc);
2451 flat_exp(env, Ctx(), nc, constants().varTrue, constants().varTrue);
2452 return vd->id();
2453 } break;
2454 default:
2455 throw InternalError("not supported yet");
2456 }
2457 } else {
2458 return e;
2459 }
2460 }
2461}
2462
2463KeepAlive conj(EnvI& env, VarDecl* b, const Ctx& ctx, const std::vector<EE>& e) {
2464 if (!ctx.neg) {
2465 std::vector<Expression*> nontrue;
2466 for (const auto& i : e) {
2467 if (istrue(env, i.b())) {
2468 continue;
2469 }
2470 if (isfalse(env, i.b())) {
2471 return bind(env, Ctx(), b, constants().literalFalse);
2472 }
2473 nontrue.push_back(i.b());
2474 }
2475 if (nontrue.empty()) {
2476 return bind(env, Ctx(), b, constants().literalTrue);
2477 }
2478 if (nontrue.size() == 1) {
2479 return bind(env, ctx, b, nontrue[0]);
2480 }
2481 if (b == constants().varTrue) {
2482 for (auto& i : nontrue) {
2483 bind(env, ctx, b, i);
2484 }
2485 return constants().literalTrue;
2486 }
2487 GC::lock();
2488 std::vector<Expression*> args;
2489 auto* al = new ArrayLit(Location().introduce(), nontrue);
2490 al->type(Type::varbool(1));
2491 args.push_back(al);
2492 Call* ret = new Call(nontrue[0]->loc().introduce(), constants().ids.forall, args);
2493 ret->decl(env.model->matchFn(env, ret, false));
2494 ret->type(ret->decl()->rtype(env, args, false));
2495 KeepAlive ka(ret);
2496 GC::unlock();
2497 return flat_exp(env, ctx, ret, b, constants().varTrue).r;
2498 }
2499 Ctx nctx = ctx;
2500 nctx.neg = false;
2501 nctx.b = -nctx.b;
2502 // negated
2503 std::vector<Expression*> nonfalse;
2504 for (const auto& i : e) {
2505 if (istrue(env, i.b())) {
2506 continue;
2507 }
2508 if (isfalse(env, i.b())) {
2509 return bind(env, Ctx(), b, constants().literalTrue);
2510 }
2511 nonfalse.push_back(i.b());
2512 }
2513 if (nonfalse.empty()) {
2514 return bind(env, Ctx(), b, constants().literalFalse);
2515 }
2516 if (nonfalse.size() == 1) {
2517 GC::lock();
2518 UnOp* uo = new UnOp(nonfalse[0]->loc(), UOT_NOT, nonfalse[0]);
2519 uo->type(Type::varbool());
2520 KeepAlive ka(uo);
2521 GC::unlock();
2522 return flat_exp(env, nctx, uo, b, constants().varTrue).r;
2523 }
2524 if (b == constants().varFalse) {
2525 for (auto& i : nonfalse) {
2526 bind(env, nctx, b, i);
2527 }
2528 return constants().literalFalse;
2529 }
2530 GC::lock();
2531 std::vector<Expression*> args;
2532 for (auto& i : nonfalse) {
2533 UnOp* uo = new UnOp(i->loc(), UOT_NOT, i);
2534 uo->type(Type::varbool());
2535 i = uo;
2536 }
2537 auto* al = new ArrayLit(Location().introduce(), nonfalse);
2538 al->type(Type::varbool(1));
2539 args.push_back(al);
2540 Call* ret = new Call(Location().introduce(), constants().ids.exists, args);
2541 ret->decl(env.model->matchFn(env, ret, false));
2542 ret->type(ret->decl()->rtype(env, args, false));
2543 assert(ret->decl());
2544 KeepAlive ka(ret);
2545 GC::unlock();
2546 return flat_exp(env, nctx, ret, b, constants().varTrue).r;
2547}
2548
2549TypeInst* eval_typeinst(EnvI& env, const Ctx& ctx, VarDecl* vd) {
2550 bool hasTiVars = (vd->ti()->domain() != nullptr) && vd->ti()->domain()->isa<TIId>();
2551 for (unsigned int i = 0; i < vd->ti()->ranges().size(); i++) {
2552 hasTiVars = hasTiVars || ((vd->ti()->ranges()[i]->domain() != nullptr) &&
2553 vd->ti()->ranges()[i]->domain()->isa<TIId>());
2554 }
2555 if (hasTiVars) {
2556 assert(vd->e());
2557 if (vd->e()->type().dim() == 0) {
2558 return new TypeInst(Location().introduce(), vd->e()->type());
2559 }
2560 ArrayLit* al = eval_array_lit(env, vd->e());
2561 std::vector<TypeInst*> dims(al->dims());
2562 for (unsigned int i = 0; i < dims.size(); i++) {
2563 dims[i] =
2564 new TypeInst(Location().introduce(), Type(),
2565 new SetLit(Location().introduce(), IntSetVal::a(al->min(i), al->max(i))));
2566 }
2567 return new TypeInst(Location().introduce(), vd->e()->type(), dims,
2568 flat_cv_exp(env, ctx, vd->ti()->domain())());
2569 }
2570 std::vector<TypeInst*> dims(vd->ti()->ranges().size());
2571 for (unsigned int i = 0; i < vd->ti()->ranges().size(); i++) {
2572 if (vd->ti()->ranges()[i]->domain() != nullptr) {
2573 KeepAlive range = flat_cv_exp(env, ctx, vd->ti()->ranges()[i]->domain());
2574 IntSetVal* isv = eval_intset(env, range());
2575 if (isv->size() > 1) {
2576 throw EvalError(env, vd->ti()->ranges()[i]->domain()->loc(),
2577 "array index set must be contiguous range");
2578 }
2579 auto* sl = new SetLit(vd->ti()->ranges()[i]->loc(), isv);
2580 sl->type(Type::parsetint());
2581 dims[i] = new TypeInst(vd->ti()->ranges()[i]->loc(), Type(), sl);
2582 } else {
2583 dims[i] = new TypeInst(vd->ti()->ranges()[i]->loc(), Type(), nullptr);
2584 }
2585 }
2586 Type t = ((vd->e() != nullptr) && !vd->e()->type().isbot()) ? vd->e()->type() : vd->ti()->type();
2587 return new TypeInst(vd->ti()->loc(), t, dims, flat_cv_exp(env, ctx, vd->ti()->domain())());
2588}
2589
2590KeepAlive flat_cv_exp(EnvI& env, Ctx ctx, Expression* e) {
2591 if (e == nullptr) {
2592 return nullptr;
2593 }
2594 GCLock lock;
2595 if (e->type().isPar() && !e->type().cv()) {
2596 return eval_par(env, e);
2597 }
2598 if (e->type().isvar()) {
2599 EE ee = flat_exp(env, ctx, e, nullptr, nullptr);
2600 if (isfalse(env, ee.b())) {
2601 throw ResultUndefinedError(env, e->loc(), "");
2602 }
2603 return ee.r();
2604 }
2605 switch (e->eid()) {
2606 case Expression::E_INTLIT:
2607 case Expression::E_FLOATLIT:
2608 case Expression::E_BOOLLIT:
2609 case Expression::E_STRINGLIT:
2610 case Expression::E_TIID:
2611 case Expression::E_VARDECL:
2612 case Expression::E_TI:
2613 case Expression::E_ANON:
2614 assert(false);
2615 return nullptr;
2616 case Expression::E_ID: {
2617 Id* id = e->cast<Id>();
2618 return flat_cv_exp(env, ctx, id->decl()->e());
2619 }
2620 case Expression::E_SETLIT: {
2621 auto* sl = e->cast<SetLit>();
2622 if ((sl->isv() != nullptr) || (sl->fsv() != nullptr)) {
2623 return sl;
2624 }
2625 std::vector<Expression*> es(sl->v().size());
2626 GCLock lock;
2627 for (unsigned int i = 0; i < sl->v().size(); i++) {
2628 es[i] = flat_cv_exp(env, ctx, sl->v()[i])();
2629 }
2630 auto* sl_ret = new SetLit(Location().introduce(), es);
2631 Type t = sl->type();
2632 t.cv(false);
2633 sl_ret->type(t);
2634 return eval_par(env, sl_ret);
2635 }
2636 case Expression::E_ARRAYLIT: {
2637 auto* al = e->cast<ArrayLit>();
2638 std::vector<Expression*> es(al->size());
2639 GCLock lock;
2640 for (unsigned int i = 0; i < al->size(); i++) {
2641 es[i] = flat_cv_exp(env, ctx, (*al)[i])();
2642 }
2643 std::vector<std::pair<int, int>> dims(al->dims());
2644 for (int i = 0; i < al->dims(); i++) {
2645 dims[i] = std::make_pair(al->min(i), al->max(i));
2646 }
2647 Expression* al_ret = eval_par(env, new ArrayLit(Location().introduce(), es, dims));
2648 Type t = al->type();
2649 t.cv(false);
2650 al_ret->type(t);
2651 return al_ret;
2652 }
2653 case Expression::E_ARRAYACCESS: {
2654 auto* aa = e->cast<ArrayAccess>();
2655 GCLock lock;
2656 Expression* av = flat_cv_exp(env, ctx, aa->v())();
2657 std::vector<Expression*> idx(aa->idx().size());
2658 for (unsigned int i = 0; i < aa->idx().size(); i++) {
2659 idx[i] = flat_cv_exp(env, ctx, aa->idx()[i])();
2660 }
2661 auto* aa_ret = new ArrayAccess(Location().introduce(), av, idx);
2662 Type t = aa->type();
2663 t.cv(false);
2664 aa_ret->type(t);
2665 return eval_par(env, aa_ret);
2666 }
2667 case Expression::E_COMP: {
2668 auto* c = e->cast<Comprehension>();
2669 GCLock lock;
2670 class EvalFlatCvExp : public EvalBase {
2671 public:
2672 Ctx ctx;
2673 EvalFlatCvExp(Ctx& ctx0) : ctx(ctx0) {}
2674 typedef Expression* ArrayVal;
2675 Expression* e(EnvI& env, Expression* e) const { return flat_cv_exp(env, ctx, e)(); }
2676 static Expression* exp(Expression* e) { return e; }
2677 static Expression* flatten(EnvI& env, Expression* e0) {
2678 return flat_exp(env, Ctx(), e0, nullptr, constants().varTrue).r();
2679 }
2680
2681 } eval(ctx);
2682 std::vector<Expression*> a = eval_comp<EvalFlatCvExp>(env, eval, c);
2683
2684 Type t = Type::bot();
2685 bool allPar = true;
2686 for (auto& i : a) {
2687 if (t == Type::bot()) {
2688 t = i->type();
2689 }
2690 if (!i->type().isPar()) {
2691 allPar = false;
2692 }
2693 }
2694 if (!allPar) {
2695 t.ti(Type::TI_VAR);
2696 }
2697 if (c->set()) {
2698 t.st(Type::ST_SET);
2699 } else {
2700 t.dim(c->type().dim());
2701 }
2702 t.cv(false);
2703 if (c->set()) {
2704 if (c->type().isPar() && allPar) {
2705 auto* sl = new SetLit(c->loc().introduce(), a);
2706 sl->type(t);
2707 Expression* slr = eval_par(env, sl);
2708 slr->type(t);
2709 return slr;
2710 }
2711 throw InternalError("var set comprehensions not supported yet");
2712 }
2713 auto* alr = new ArrayLit(Location().introduce(), a);
2714 alr->type(t);
2715 alr->flat(true);
2716 return alr;
2717 }
2718 case Expression::E_ITE: {
2719 ITE* ite = e->cast<ITE>();
2720 for (int i = 0; i < ite->size(); i++) {
2721 KeepAlive ka = flat_cv_exp(env, ctx, ite->ifExpr(i));
2722 if (eval_bool(env, ka())) {
2723 return flat_cv_exp(env, ctx, ite->thenExpr(i));
2724 }
2725 }
2726 return flat_cv_exp(env, ctx, ite->elseExpr());
2727 }
2728 case Expression::E_BINOP: {
2729 auto* bo = e->cast<BinOp>();
2730 if (bo->op() == BOT_AND) {
2731 GCLock lock;
2732 Expression* lhs = flat_cv_exp(env, ctx, bo->lhs())();
2733 if (!eval_bool(env, lhs)) {
2734 return constants().literalFalse;
2735 }
2736 return eval_par(env, flat_cv_exp(env, ctx, bo->rhs())());
2737 }
2738 if (bo->op() == BOT_OR) {
2739 GCLock lock;
2740 Expression* lhs = flat_cv_exp(env, ctx, bo->lhs())();
2741 if (eval_bool(env, lhs)) {
2742 return constants().literalTrue;
2743 }
2744 return eval_par(env, flat_cv_exp(env, ctx, bo->rhs())());
2745 }
2746 GCLock lock;
2747 auto* nbo = new BinOp(bo->loc().introduce(), flat_cv_exp(env, ctx, bo->lhs())(), bo->op(),
2748 flat_cv_exp(env, ctx, bo->rhs())());
2749 nbo->type(bo->type());
2750 nbo->decl(bo->decl());
2751 return eval_par(env, nbo);
2752 }
2753 case Expression::E_UNOP: {
2754 UnOp* uo = e->cast<UnOp>();
2755 GCLock lock;
2756 UnOp* nuo = new UnOp(uo->loc(), uo->op(), flat_cv_exp(env, ctx, uo->e())());
2757 nuo->type(uo->type());
2758 return eval_par(env, nuo);
2759 }
2760 case Expression::E_CALL: {
2761 Call* c = e->cast<Call>();
2762 if (c->id() == "mzn_in_root_context") {
2763 return constants().boollit(ctx.b == C_ROOT);
2764 }
2765 if (ctx.b == C_ROOT && (c->decl()->e() != nullptr) && c->decl()->e()->isa<BoolLit>()) {
2766 bool allBool = true;
2767 for (unsigned int i = 0; i < c->argCount(); i++) {
2768 if (c->arg(i)->type().bt() != Type::BT_BOOL) {
2769 allBool = false;
2770 break;
2771 }
2772 }
2773 if (allBool) {
2774 return c->decl()->e();
2775 }
2776 }
2777 std::vector<Expression*> args(c->argCount());
2778 GCLock lock;
2779 for (unsigned int i = 0; i < c->argCount(); i++) {
2780 Ctx c_mix;
2781 c_mix.b = C_MIX;
2782 c_mix.i = C_MIX;
2783 args[i] = flat_cv_exp(env, c_mix, c->arg(i))();
2784 }
2785 Call* nc = new Call(c->loc(), c->id(), args);
2786 nc->decl(c->decl());
2787 Type nct(c->type());
2788 if ((nc->decl()->e() != nullptr) && nc->decl()->e()->type().cv()) {
2789 nct.cv(false);
2790 nct.ti(Type::TI_VAR);
2791 nc->type(nct);
2792 EE ee = flat_exp(env, ctx, nc, nullptr, nullptr);
2793 if (isfalse(env, ee.b())) {
2794 std::ostringstream ss;
2795 ss << "evaluation of `" << nc->id() << "was undefined";
2796 throw ResultUndefinedError(env, e->loc(), ss.str());
2797 }
2798 return ee.r();
2799 }
2800 nc->type(nct);
2801 return eval_par(env, nc);
2802 }
2803 case Expression::E_LET: {
2804 Let* l = e->cast<Let>();
2805 EE ee = flat_exp(env, ctx, l, nullptr, nullptr);
2806 if (isfalse(env, ee.b())) {
2807 throw ResultUndefinedError(env, e->loc(), "evaluation of let expression was undefined");
2808 }
2809 return ee.r();
2810 }
2811 }
2812 throw InternalError("internal error");
2813}
2814
2815class ItemTimer {
2816public:
2817 using TimingMap =
2818 std::map<std::pair<ASTString, unsigned int>, std::chrono::high_resolution_clock::duration>;
2819 ItemTimer(const Location& loc, TimingMap* tm)
2820 : _loc(loc), _tm(tm), _start(std::chrono::high_resolution_clock::now()) {}
2821
2822 ~ItemTimer() {
2823 try {
2824 if (_tm != nullptr) {
2825 std::chrono::high_resolution_clock::time_point end =
2826 std::chrono::high_resolution_clock::now();
2827 unsigned int line = _loc.firstLine();
2828 auto it = _tm->find(std::make_pair(_loc.filename(), line));
2829 if (it != _tm->end()) {
2830 it->second += end - _start;
2831 } else {
2832 _tm->insert(std::make_pair(std::make_pair(_loc.filename(), line), end - _start));
2833 }
2834 }
2835 } catch (std::exception& e) {
2836 assert(false); // Invariant: Operations on the TimingMap will not throw an exception
2837 }
2838 }
2839
2840private:
2841 const Location& _loc;
2842 TimingMap* _tm;
2843 std::chrono::high_resolution_clock::time_point _start;
2844};
2845
2846void flatten(Env& e, FlatteningOptions opt) {
2847 ItemTimer::TimingMap timingMap_o;
2848 ItemTimer::TimingMap* timingMap = opt.detailedTiming ? &timingMap_o : nullptr;
2849 try {
2850 EnvI& env = e.envi();
2851 env.fopts = opt;
2852
2853 bool onlyRangeDomains = false;
2854 if (opt.onlyRangeDomains) {
2855 onlyRangeDomains = true; // compulsory
2856 } else {
2857 GCLock lock;
2858 Call* check_only_range =
2859 new Call(Location(), "mzn_check_only_range_domains", std::vector<Expression*>());
2860 check_only_range->type(Type::parbool());
2861 check_only_range->decl(env.model->matchFn(e.envi(), check_only_range, false));
2862 onlyRangeDomains = eval_bool(e.envi(), check_only_range);
2863 }
2864
2865 bool hadSolveItem = false;
2866 // Flatten main model
2867 class FV : public ItemVisitor {
2868 public:
2869 EnvI& env;
2870 bool& hadSolveItem;
2871 ItemTimer::TimingMap* timingMap;
2872 FV(EnvI& env0, bool& hadSolveItem0, ItemTimer::TimingMap* timingMap0)
2873 : env(env0), hadSolveItem(hadSolveItem0), timingMap(timingMap0) {}
2874 bool enter(Item* i) const { return !(i->isa<ConstraintI>() && env.failed()); }
2875 void vVarDeclI(VarDeclI* v) {
2876 ItemTimer item_timer(v->loc(), timingMap);
2877 v->e()->ann().remove(constants().ann.output_var);
2878 v->e()->ann().removeCall(constants().ann.output_array);
2879 if (v->e()->ann().contains(constants().ann.output_only)) {
2880 return;
2881 }
2882 if (v->e()->type().isPar() && !v->e()->type().isOpt() && !v->e()->type().cv() &&
2883 v->e()->type().dim() > 0 && v->e()->ti()->domain() == nullptr &&
2884 (v->e()->type().bt() == Type::BT_INT || v->e()->type().bt() == Type::BT_FLOAT)) {
2885 // Compute bounds for array literals
2886 CallStackItem csi(env, v->e());
2887 GCLock lock;
2888 ArrayLit* al = eval_array_lit(env, v->e()->e());
2889 v->e()->e(al);
2890 check_index_sets(env, v->e(), v->e()->e());
2891 if (al->size() > 0) {
2892 if (v->e()->type().bt() == Type::BT_INT && v->e()->type().st() == Type::ST_PLAIN) {
2893 IntVal lb = IntVal::infinity();
2894 IntVal ub = -IntVal::infinity();
2895 for (unsigned int i = 0; i < al->size(); i++) {
2896 IntVal vi = eval_int(env, (*al)[i]);
2897 lb = std::min(lb, vi);
2898 ub = std::max(ub, vi);
2899 }
2900 GCLock lock;
2901 set_computed_domain(env, v->e(),
2902 new SetLit(Location().introduce(), IntSetVal::a(lb, ub)), true);
2903 } else if (v->e()->type().bt() == Type::BT_FLOAT &&
2904 v->e()->type().st() == Type::ST_PLAIN) {
2905 FloatVal lb = FloatVal::infinity();
2906 FloatVal ub = -FloatVal::infinity();
2907 for (unsigned int i = 0; i < al->size(); i++) {
2908 FloatVal vi = eval_float(env, (*al)[i]);
2909 lb = std::min(lb, vi);
2910 ub = std::max(ub, vi);
2911 }
2912 GCLock lock;
2913 set_computed_domain(env, v->e(),
2914 new SetLit(Location().introduce(), FloatSetVal::a(lb, ub)), true);
2915 }
2916 }
2917 } else if (v->e()->type().isvar() || v->e()->type().isAnn()) {
2918 (void)flatten_id(env, Ctx(), v->e()->id(), nullptr, constants().varTrue, true);
2919 } else {
2920 if (v->e()->e() == nullptr) {
2921 if (!v->e()->type().isAnn()) {
2922 throw EvalError(env, v->e()->loc(), "Undefined parameter", v->e()->id()->v());
2923 }
2924 } else {
2925 CallStackItem csi(env, v->e());
2926 GCLock lock;
2927 Location v_loc = v->e()->e()->loc();
2928 if (!v->e()->e()->type().cv()) {
2929 v->e()->e(eval_par(env, v->e()->e()));
2930 } else {
2931 EE ee = flat_exp(env, Ctx(), v->e()->e(), nullptr, constants().varTrue);
2932 v->e()->e(ee.r());
2933 }
2934 check_par_declaration(env, v->e());
2935 }
2936 }
2937 }
2938 void vConstraintI(ConstraintI* ci) {
2939 ItemTimer item_timer(ci->loc(), timingMap);
2940 (void)flat_exp(env, Ctx(), ci->e(), constants().varTrue, constants().varTrue);
2941 }
2942 void vSolveI(SolveI* si) {
2943 if (hadSolveItem) {
2944 throw FlatteningError(env, si->loc(), "Only one solve item allowed");
2945 }
2946 ItemTimer item_timer(si->loc(), timingMap);
2947 hadSolveItem = true;
2948 GCLock lock;
2949 SolveI* nsi = nullptr;
2950 switch (si->st()) {
2951 case SolveI::ST_SAT:
2952 nsi = SolveI::sat(Location());
2953 break;
2954 case SolveI::ST_MIN: {
2955 Ctx ctx;
2956 ctx.i = C_NEG;
2957 nsi = SolveI::min(Location().introduce(),
2958 flat_exp(env, ctx, si->e(), nullptr, constants().varTrue).r());
2959 } break;
2960 case SolveI::ST_MAX: {
2961 Ctx ctx;
2962 ctx.i = C_POS;
2963 nsi = SolveI::max(Location().introduce(),
2964 flat_exp(env, Ctx(), si->e(), nullptr, constants().varTrue).r());
2965 } break;
2966 }
2967 for (ExpressionSetIter it = si->ann().begin(); it != si->ann().end(); ++it) {
2968 auto* c = (*it)->dynamicCast<Call>();
2969 if (c != nullptr && c->id() == "on_restart") {
2970 assert(c->argCount() == 1);
2971 auto* pred = c->arg(0)->cast<StringLit>();
2972 Call* nc = new Call(c->loc().introduce(), pred->v(), std::vector<Expression*>());
2973 nc->type(Type::varbool());
2974 FunctionI* decl = env.model->matchFn(env, nc, false);
2975 if (decl == nullptr) {
2976 std::ostringstream ss;
2977 ss << "Unknown predicate `" << pred->v()
2978 << "' found while evaluating on_restart annotation";
2979 throw FlatteningError(env, pred->loc(), ss.str());
2980 }
2981 nc->decl(decl);
2982 env.flatAddItem(new ConstraintI(c->loc().introduce(), nc));
2983 } else {
2984 nsi->ann().add(flat_exp(env, Ctx(), *it, nullptr, constants().varTrue).r());
2985 }
2986 }
2987 env.flatAddItem(nsi);
2988 }
2989 } _fv(env, hadSolveItem, timingMap);
2990 iter_items<FV>(_fv, e.model());
2991
2992 if (!hadSolveItem) {
2993 GCLock lock;
2994 e.envi().flatAddItem(SolveI::sat(Location().introduce()));
2995 }
2996
2997 // Create output model
2998 if (opt.keepOutputInFzn) {
2999 copy_output(env);
3000 } else {
3001 create_output(env, opt.outputMode, opt.outputObjective, opt.outputOutputItem, opt.hasChecker);
3002 }
3003
3004 // Flatten remaining redefinitions
3005 Model& m = *e.flat();
3006 int startItem = 0;
3007 int endItem = static_cast<int>(m.size()) - 1;
3008
3009 FunctionI* int_lin_eq;
3010 {
3011 std::vector<Type> int_lin_eq_t(3);
3012 int_lin_eq_t[0] = Type::parint(1);
3013 int_lin_eq_t[1] = Type::varint(1);
3014 int_lin_eq_t[2] = Type::parint(0);
3015 GCLock lock;
3016 FunctionI* fi = env.model->matchFn(env, constants().ids.int_.lin_eq, int_lin_eq_t, false);
3017 int_lin_eq = ((fi != nullptr) && (fi->e() != nullptr)) ? fi : nullptr;
3018 }
3019 FunctionI* float_lin_eq;
3020 {
3021 std::vector<Type> float_lin_eq_t(3);
3022 float_lin_eq_t[0] = Type::parfloat(1);
3023 float_lin_eq_t[1] = Type::varfloat(1);
3024 float_lin_eq_t[2] = Type::parfloat(0);
3025 GCLock lock;
3026 FunctionI* fi = env.model->matchFn(env, constants().ids.float_.lin_eq, float_lin_eq_t, false);
3027 float_lin_eq = ((fi != nullptr) && (fi->e() != nullptr)) ? fi : nullptr;
3028 }
3029 FunctionI* array_bool_and;
3030 FunctionI* array_bool_or;
3031 FunctionI* array_bool_clause;
3032 FunctionI* array_bool_clause_reif;
3033 FunctionI* bool_xor;
3034 {
3035 std::vector<Type> array_bool_andor_t(2);
3036 array_bool_andor_t[0] = Type::varbool(1);
3037 array_bool_andor_t[1] = Type::varbool(0);
3038 GCLock lock;
3039 FunctionI* fi =
3040 env.model->matchFn(env, ASTString("array_bool_and"), array_bool_andor_t, false);
3041 array_bool_and = ((fi != nullptr) && (fi->e() != nullptr)) ? fi : nullptr;
3042 fi = env.model->matchFn(env, ASTString("array_bool_or"), array_bool_andor_t, false);
3043 array_bool_or = ((fi != nullptr) && (fi->e() != nullptr)) ? fi : nullptr;
3044
3045 array_bool_andor_t[1] = Type::varbool(1);
3046 fi = env.model->matchFn(env, ASTString("bool_clause"), array_bool_andor_t, false);
3047 array_bool_clause = ((fi != nullptr) && (fi->e() != nullptr)) ? fi : nullptr;
3048
3049 array_bool_andor_t.push_back(Type::varbool());
3050 fi = env.model->matchFn(env, ASTString("bool_clause_reif"), array_bool_andor_t, false);
3051 array_bool_clause_reif = ((fi != nullptr) && (fi->e() != nullptr)) ? fi : nullptr;
3052
3053 std::vector<Type> bool_xor_t(3);
3054 bool_xor_t[0] = Type::varbool();
3055 bool_xor_t[1] = Type::varbool();
3056 bool_xor_t[2] = Type::varbool();
3057 fi = env.model->matchFn(env, constants().ids.bool_xor, bool_xor_t, false);
3058 bool_xor = ((fi != nullptr) && (fi->e() != nullptr)) ? fi : nullptr;
3059 }
3060
3061 std::vector<int> convertToRangeDomain;
3062 env.collectVarDecls(true);
3063
3064 while (startItem <= endItem || !env.modifiedVarDecls.empty() || !convertToRangeDomain.empty()) {
3065 if (env.failed()) {
3066 return;
3067 }
3068 std::vector<int> agenda;
3069 for (int i = startItem; i <= endItem; i++) {
3070 agenda.push_back(i);
3071 }
3072 for (int modifiedVarDecl : env.modifiedVarDecls) {
3073 agenda.push_back(modifiedVarDecl);
3074 }
3075 env.modifiedVarDecls.clear();
3076
3077 bool doConvertToRangeDomain = false;
3078 if (agenda.empty()) {
3079 for (auto i : convertToRangeDomain) {
3080 agenda.push_back(i);
3081 }
3082 convertToRangeDomain.clear();
3083 doConvertToRangeDomain = true;
3084 }
3085
3086 for (int i : agenda) {
3087 if (auto* vdi = m[i]->dynamicCast<VarDeclI>()) {
3088 if (vdi->removed()) {
3089 continue;
3090 }
3091 /// Look at constraints
3092 if (!is_output(vdi->e())) {
3093 if (0 < env.varOccurrences.occurrences(vdi->e())) {
3094 const auto it = env.varOccurrences.itemMap.find(vdi->e()->id());
3095 if (env.varOccurrences.itemMap.end() != it) {
3096 bool hasRedundantOccurrenciesOnly = true;
3097 for (const auto& c : it->second) {
3098 if (auto* constrI = c->dynamicCast<ConstraintI>()) {
3099 if (auto* call = constrI->e()->dynamicCast<Call>()) {
3100 if (call->id() == "mzn_reverse_map_var") {
3101 continue; // all good
3102 }
3103 }
3104 }
3105 hasRedundantOccurrenciesOnly = false;
3106 break;
3107 }
3108 if (hasRedundantOccurrenciesOnly) {
3109 env.flatRemoveItem(vdi);
3110 env.varOccurrences.removeAllOccurrences(vdi->e());
3111 for (const auto& c : it->second) {
3112 c->remove();
3113 }
3114 continue;
3115 }
3116 }
3117 } else { // 0 occurrencies
3118 if ((vdi->e()->e() != nullptr) && (vdi->e()->ti()->domain() != nullptr)) {
3119 if (vdi->e()->type().isvar() && vdi->e()->type().isbool() &&
3120 !vdi->e()->type().isOpt() &&
3121 Expression::equal(vdi->e()->ti()->domain(), constants().literalTrue)) {
3122 GCLock lock;
3123 auto* ci = new ConstraintI(vdi->loc(), vdi->e()->e());
3124 if (vdi->e()->introduced()) {
3125 env.flatAddItem(ci);
3126 env.flatRemoveItem(vdi);
3127 continue;
3128 }
3129 vdi->e()->e(nullptr);
3130 env.flatAddItem(ci);
3131 } else if (vdi->e()->type().isPar() || vdi->e()->ti()->computedDomain()) {
3132 env.flatRemoveItem(vdi);
3133 continue;
3134 }
3135 } else {
3136 env.flatRemoveItem(vdi);
3137 continue;
3138 }
3139 }
3140 }
3141 if (vdi->e()->type().dim() > 0 && vdi->e()->type().isvar()) {
3142 vdi->e()->ti()->domain(nullptr);
3143 }
3144 if (vdi->e()->type().isint() && vdi->e()->type().isvar() &&
3145 vdi->e()->ti()->domain() != nullptr) {
3146 GCLock lock;
3147 IntSetVal* dom = eval_intset(env, vdi->e()->ti()->domain());
3148
3149 bool needRangeDomain = onlyRangeDomains;
3150 if (!needRangeDomain && dom->size() > 0) {
3151 if (dom->min(0).isMinusInfinity() || dom->max(dom->size() - 1).isPlusInfinity()) {
3152 needRangeDomain = true;
3153 }
3154 }
3155 if (needRangeDomain) {
3156 if (doConvertToRangeDomain) {
3157 if (dom->min(0).isMinusInfinity() || dom->max(dom->size() - 1).isPlusInfinity()) {
3158 auto* nti = copy(env, vdi->e()->ti())->cast<TypeInst>();
3159 nti->domain(nullptr);
3160 vdi->e()->ti(nti);
3161 if (dom->min(0).isFinite()) {
3162 std::vector<Expression*> args(2);
3163 args[0] = IntLit::a(dom->min(0));
3164 args[1] = vdi->e()->id();
3165 Call* call = new Call(Location().introduce(), constants().ids.int_.le, args);
3166 call->type(Type::varbool());
3167 call->decl(env.model->matchFn(env, call, false));
3168 env.flatAddItem(new ConstraintI(Location().introduce(), call));
3169 } else if (dom->max(dom->size() - 1).isFinite()) {
3170 std::vector<Expression*> args(2);
3171 args[0] = vdi->e()->id();
3172 args[1] = IntLit::a(dom->max(dom->size() - 1));
3173 Call* call = new Call(Location().introduce(), constants().ids.int_.le, args);
3174 call->type(Type::varbool());
3175 call->decl(env.model->matchFn(env, call, false));
3176 env.flatAddItem(new ConstraintI(Location().introduce(), call));
3177 }
3178 } else if (dom->size() > 1) {
3179 auto* newDom = new SetLit(Location().introduce(),
3180 IntSetVal::a(dom->min(0), dom->max(dom->size() - 1)));
3181 auto* nti = copy(env, vdi->e()->ti())->cast<TypeInst>();
3182 nti->domain(newDom);
3183 vdi->e()->ti(nti);
3184 }
3185 if (dom->size() > 1) {
3186 std::vector<Expression*> args(2);
3187 args[0] = vdi->e()->id();
3188 args[1] = new SetLit(vdi->e()->loc(), dom);
3189 Call* call = new Call(vdi->e()->loc(), constants().ids.set_in, args);
3190 call->type(Type::varbool());
3191 call->decl(env.model->matchFn(env, call, false));
3192 // Give distinct call stack
3193 Annotation& ann = vdi->e()->ann();
3194 Expression* tmp = call;
3195 if (Expression* mznpath_ann = ann.getCall(constants().ann.mzn_path)) {
3196 tmp = mznpath_ann->cast<Call>()->arg(0);
3197 }
3198 CallStackItem csi(env, tmp);
3199 env.flatAddItem(new ConstraintI(Location().introduce(), call));
3200 }
3201 } else {
3202 convertToRangeDomain.push_back(i);
3203 }
3204 }
3205 }
3206 if (vdi->e()->type().isfloat() && vdi->e()->type().isvar() &&
3207 vdi->e()->ti()->domain() != nullptr) {
3208 GCLock lock;
3209 FloatSetVal* vdi_dom = eval_floatset(env, vdi->e()->ti()->domain());
3210 FloatVal vmin = vdi_dom->min();
3211 FloatVal vmax = vdi_dom->max();
3212 if (vmin == -FloatVal::infinity() && vmax == FloatVal::infinity()) {
3213 vdi->e()->ti()->domain(nullptr);
3214 } else if (vmin == -FloatVal::infinity()) {
3215 vdi->e()->ti()->domain(nullptr);
3216 std::vector<Expression*> args(2);
3217 args[0] = vdi->e()->id();
3218 args[1] = FloatLit::a(vmax);
3219 Call* call = new Call(Location().introduce(), constants().ids.float_.le, args);
3220 call->type(Type::varbool());
3221 call->decl(env.model->matchFn(env, call, false));
3222 env.flatAddItem(new ConstraintI(Location().introduce(), call));
3223 } else if (vmax == FloatVal::infinity()) {
3224 vdi->e()->ti()->domain(nullptr);
3225 std::vector<Expression*> args(2);
3226 args[0] = FloatLit::a(vmin);
3227 args[1] = vdi->e()->id();
3228 Call* call = new Call(Location().introduce(), constants().ids.float_.le, args);
3229 call->type(Type::varbool());
3230 call->decl(env.model->matchFn(env, call, false));
3231 env.flatAddItem(new ConstraintI(Location().introduce(), call));
3232 } else if (vdi_dom->size() > 1) {
3233 auto* dom_ranges = new BinOp(vdi->e()->ti()->domain()->loc().introduce(),
3234 FloatLit::a(vmin), BOT_DOTDOT, FloatLit::a(vmax));
3235 vdi->e()->ti()->domain(dom_ranges);
3236
3237 std::vector<Expression*> ranges;
3238 for (FloatSetRanges vdi_r(vdi_dom); vdi_r(); ++vdi_r) {
3239 ranges.push_back(FloatLit::a(vdi_r.min()));
3240 ranges.push_back(FloatLit::a(vdi_r.max()));
3241 }
3242 auto* al = new ArrayLit(Location().introduce(), ranges);
3243 al->type(Type::parfloat(1));
3244 std::vector<Expression*> args(2);
3245 args[0] = vdi->e()->id();
3246 args[1] = al;
3247 Call* call = new Call(Location().introduce(), constants().ids.float_.dom, args);
3248 call->type(Type::varbool());
3249 call->decl(env.model->matchFn(env, call, false));
3250 env.flatAddItem(new ConstraintI(Location().introduce(), call));
3251 }
3252 }
3253 }
3254 }
3255
3256 // rewrite some constraints if there are redefinitions
3257 for (int i : agenda) {
3258 if (m[i]->removed()) {
3259 continue;
3260 }
3261 if (auto* vdi = m[i]->dynamicCast<VarDeclI>()) {
3262 VarDecl* vd = vdi->e();
3263 if (vd->e() != nullptr) {
3264 bool isTrueVar = vd->type().isbool() &&
3265 Expression::equal(vd->ti()->domain(), constants().literalTrue);
3266 if (Call* c = vd->e()->dynamicCast<Call>()) {
3267 GCLock lock;
3268 Call* nc = nullptr;
3269 if (c->id() == constants().ids.lin_exp) {
3270 if (c->type().isfloat() && (float_lin_eq != nullptr)) {
3271 std::vector<Expression*> args(c->argCount());
3272 auto* le_c = follow_id(c->arg(0))->cast<ArrayLit>();
3273 std::vector<Expression*> nc_c(le_c->size());
3274 for (auto ii = static_cast<unsigned int>(nc_c.size()); (ii--) != 0U;) {
3275 nc_c[ii] = (*le_c)[ii];
3276 }
3277 nc_c.push_back(FloatLit::a(-1));
3278 args[0] = new ArrayLit(Location().introduce(), nc_c);
3279 args[0]->type(Type::parfloat(1));
3280 auto* le_x = follow_id(c->arg(1))->cast<ArrayLit>();
3281 std::vector<Expression*> nx(le_x->size());
3282 for (auto ii = static_cast<unsigned int>(nx.size()); (ii--) != 0U;) {
3283 nx[ii] = (*le_x)[ii];
3284 }
3285 nx.push_back(vd->id());
3286 args[1] = new ArrayLit(Location().introduce(), nx);
3287 args[1]->type(Type::varfloat(1));
3288 FloatVal d = c->arg(2)->cast<FloatLit>()->v();
3289 args[2] = FloatLit::a(-d);
3290 args[2]->type(Type::parfloat(0));
3291 nc = new Call(c->loc().introduce(), ASTString("float_lin_eq"), args);
3292 nc->type(Type::varbool());
3293 nc->decl(float_lin_eq);
3294 } else if (int_lin_eq != nullptr) {
3295 assert(c->type().isint());
3296 std::vector<Expression*> args(c->argCount());
3297 auto* le_c = follow_id(c->arg(0))->cast<ArrayLit>();
3298 std::vector<Expression*> nc_c(le_c->size());
3299 for (auto ii = static_cast<unsigned int>(nc_c.size()); (ii--) != 0U;) {
3300 nc_c[ii] = (*le_c)[ii];
3301 }
3302 nc_c.push_back(IntLit::a(-1));
3303 args[0] = new ArrayLit(Location().introduce(), nc_c);
3304 args[0]->type(Type::parint(1));
3305 auto* le_x = follow_id(c->arg(1))->cast<ArrayLit>();
3306 std::vector<Expression*> nx(le_x->size());
3307 for (auto ii = static_cast<unsigned int>(nx.size()); (ii--) != 0U;) {
3308 nx[ii] = (*le_x)[ii];
3309 }
3310 nx.push_back(vd->id());
3311 args[1] = new ArrayLit(Location().introduce(), nx);
3312 args[1]->type(Type::varint(1));
3313 IntVal d = c->arg(2)->cast<IntLit>()->v();
3314 args[2] = IntLit::a(-d);
3315 args[2]->type(Type::parint(0));
3316 nc = new Call(c->loc().introduce(), ASTString("int_lin_eq"), args);
3317 nc->type(Type::varbool());
3318 nc->decl(int_lin_eq);
3319 }
3320 } else if (c->id() == constants().ids.exists) {
3321 if (array_bool_or != nullptr) {
3322 std::vector<Expression*> args(2);
3323 args[0] = c->arg(0);
3324 args[1] = vd->id();
3325 nc = new Call(c->loc().introduce(), array_bool_or->id(), args);
3326 nc->type(Type::varbool());
3327 nc->decl(array_bool_or);
3328 }
3329 } else if (!isTrueVar && c->id() == constants().ids.forall) {
3330 if (array_bool_and != nullptr) {
3331 std::vector<Expression*> args(2);
3332 args[0] = c->arg(0);
3333 args[1] = vd->id();
3334 nc = new Call(c->loc().introduce(), array_bool_and->id(), args);
3335 nc->type(Type::varbool());
3336 nc->decl(array_bool_and);
3337 }
3338 } else if (isTrueVar && c->id() == constants().ids.clause &&
3339 (array_bool_clause != nullptr)) {
3340 std::vector<Expression*> args(2);
3341 args[0] = c->arg(0);
3342 args[1] = c->arg(1);
3343 nc = new Call(c->loc().introduce(), array_bool_clause->id(), args);
3344 nc->type(Type::varbool());
3345 nc->decl(array_bool_clause);
3346 } else if (c->id() == constants().ids.clause && (array_bool_clause_reif != nullptr)) {
3347 std::vector<Expression*> args(3);
3348 args[0] = c->arg(0);
3349 args[1] = c->arg(1);
3350 args[2] = vd->id();
3351 nc = new Call(c->loc().introduce(), array_bool_clause_reif->id(), args);
3352 nc->type(Type::varbool());
3353 nc->decl(array_bool_clause_reif);
3354
3355 } else if (c->id() == constants().ids.bool_not && c->argCount() == 1 &&
3356 c->decl()->e() == nullptr) {
3357 bool isFalseVar = Expression::equal(vd->ti()->domain(), constants().literalFalse);
3358 if (c->arg(0) == constants().boollit(true)) {
3359 if (isTrueVar) {
3360 env.fail();
3361 } else {
3362 env.flatRemoveExpr(c, vdi);
3363 env.cseMapRemove(c);
3364 vd->e(constants().literalFalse);
3365 vd->ti()->domain(constants().literalFalse);
3366 }
3367 } else if (c->arg(0) == constants().boollit(false)) {
3368 if (isFalseVar) {
3369 env.fail();
3370 } else {
3371 env.flatRemoveExpr(c, vdi);
3372 env.cseMapRemove(c);
3373 vd->e(constants().literalTrue);
3374 vd->ti()->domain(constants().literalTrue);
3375 }
3376 } else if (c->arg(0)->isa<Id>() && (isTrueVar || isFalseVar)) {
3377 VarDecl* arg_vd = c->arg(0)->cast<Id>()->decl();
3378 if (arg_vd->ti()->domain() == nullptr) {
3379 arg_vd->e(constants().boollit(!isTrueVar));
3380 arg_vd->ti()->domain(constants().boollit(!isTrueVar));
3381 } else if (arg_vd->ti()->domain() == constants().boollit(isTrueVar)) {
3382 env.fail();
3383 } else {
3384 arg_vd->e(arg_vd->ti()->domain());
3385 }
3386 env.flatRemoveExpr(c, vdi);
3387 vd->e(nullptr);
3388 // Need to remove right hand side from CSE map, otherwise
3389 // flattening of nc could assume c has already been flattened
3390 // to vd
3391 env.cseMapRemove(c);
3392 } else {
3393 // don't know how to handle, use bool_not/2
3394 nc = new Call(c->loc().introduce(), c->id(), {c->arg(0), vd->id()});
3395 nc->type(Type::varbool());
3396 nc->decl(env.model->matchFn(env, nc, false));
3397 }
3398 } else {
3399 if (isTrueVar) {
3400 FunctionI* decl = env.model->matchFn(env, c, false);
3401 env.cseMapRemove(c);
3402 if ((decl->e() != nullptr) || c->id() == constants().ids.forall) {
3403 if (decl->e() != nullptr) {
3404 add_path_annotation(env, decl->e());
3405 }
3406 c->decl(decl);
3407 nc = c;
3408 }
3409 } else {
3410 std::vector<Expression*> args(c->argCount());
3411 for (auto i = static_cast<unsigned int>(args.size()); (i--) != 0U;) {
3412 args[i] = c->arg(i);
3413 }
3414 args.push_back(vd->id());
3415 ASTString cid = c->id();
3416 if (cid == constants().ids.clause && (array_bool_clause_reif != nullptr)) {
3417 nc = new Call(c->loc().introduce(), array_bool_clause_reif->id(), args);
3418 nc->type(Type::varbool());
3419 nc->decl(array_bool_clause_reif);
3420 } else {
3421 FunctionI* decl = nullptr;
3422 if (c->type().isbool() && vd->type().isbool()) {
3423 if (env.fopts.enableHalfReification &&
3424 vd->ann().contains(constants().ctx.pos)) {
3425 cid = env.halfReifyId(c->id());
3426 decl = env.model->matchFn(env, cid, args, false);
3427 if (decl == nullptr) {
3428 cid = env.reifyId(c->id());
3429 decl = env.model->matchFn(env, cid, args, false);
3430 }
3431 } else {
3432 cid = env.reifyId(c->id());
3433 decl = env.model->matchFn(env, cid, args, false);
3434 }
3435 if (decl == nullptr) {
3436 std::ostringstream ss;
3437 ss << "'" << c->id()
3438 << "' is used in a reified context but no reified version is "
3439 "available";
3440 throw FlatteningError(env, c->loc(), ss.str());
3441 }
3442 } else {
3443 decl = env.model->matchFn(env, cid, args, false);
3444 }
3445 if ((decl != nullptr) && (decl->e() != nullptr)) {
3446 add_path_annotation(env, decl->e());
3447 nc = new Call(c->loc().introduce(), cid, args);
3448 nc->type(Type::varbool());
3449 nc->decl(decl);
3450 }
3451 }
3452 }
3453 }
3454 if (nc != nullptr) {
3455 // Note: Removal of VarDecl's referenced by c must be delayed
3456 // until nc is flattened
3457 std::vector<VarDecl*> toRemove;
3458 CollectDecls cd(env.varOccurrences, toRemove, vdi);
3459 top_down(cd, c);
3460 vd->e(nullptr);
3461 // Need to remove right hand side from CSE map, otherwise
3462 // flattening of nc could assume c has already been flattened
3463 // to vd
3464 env.cseMapRemove(c);
3465 /// TODO: check if removing variables here makes sense:
3466 // if (!is_output(vd) && env.varOccurrences.occurrences(vd)==0) {
3467 // removedItems.push_back(vdi);
3468 // }
3469 if (nc != c) {
3470 make_defined_var(vd, nc);
3471 for (ExpressionSetIter it = c->ann().begin(); it != c->ann().end(); ++it) {
3472 EE ee_ann = flat_exp(env, Ctx(), *it, nullptr, constants().varTrue);
3473 nc->addAnnotation(ee_ann.r());
3474 }
3475 }
3476 StringLit* vsl = get_longest_mzn_path_annotation(env, vdi->e());
3477 StringLit* csl = get_longest_mzn_path_annotation(env, c);
3478 CallStackItem* vsi = nullptr;
3479 CallStackItem* csi = nullptr;
3480 if (vsl != nullptr) {
3481 vsi = new CallStackItem(env, vsl);
3482 }
3483 if (csl != nullptr) {
3484 csi = new CallStackItem(env, csl);
3485 }
3486 Location orig_loc = nc->loc();
3487 if (csl != nullptr) {
3488 ASTString loc = csl->v();
3489 size_t sep = loc.find('|');
3490 std::string filename = loc.substr(0, sep);
3491 std::string start_line_s = loc.substr(sep + 1, loc.find('|', sep + 1) - sep - 1);
3492 int start_line = std::stoi(start_line_s);
3493 Location new_loc(ASTString(filename), start_line, 0, start_line, 0);
3494 orig_loc = new_loc;
3495 }
3496 ItemTimer item_timer(orig_loc, timingMap);
3497 (void)flat_exp(env, Ctx(), nc, constants().varTrue, constants().varTrue);
3498
3499 delete csi;
3500
3501 delete vsi;
3502
3503 // Remove VarDecls becoming unused through the removal of c
3504 // because they are not used by nc
3505 while (!toRemove.empty()) {
3506 VarDecl* cur = toRemove.back();
3507 toRemove.pop_back();
3508 if (env.varOccurrences.occurrences(cur) == 0 && CollectDecls::varIsFree(cur)) {
3509 auto cur_idx = env.varOccurrences.idx.find(cur->id());
3510 if (cur_idx != env.varOccurrences.idx.end()) {
3511 auto* vdi = m[cur_idx->second]->cast<VarDeclI>();
3512 if (!is_output(cur) && !m[cur_idx->second]->removed()) {
3513 CollectDecls cd(env.varOccurrences, toRemove, vdi);
3514 top_down(cd, vdi->e()->e());
3515 vdi->remove();
3516 }
3517 }
3518 }
3519 }
3520 }
3521 }
3522 }
3523 } else if (auto* ci = m[i]->dynamicCast<ConstraintI>()) {
3524 if (Call* c = ci->e()->dynamicCast<Call>()) {
3525 GCLock lock;
3526 Call* nc = nullptr;
3527 if (c->id() == constants().ids.exists) {
3528 if (array_bool_or != nullptr) {
3529 std::vector<Expression*> args(2);
3530 args[0] = c->arg(0);
3531 args[1] = constants().literalTrue;
3532 nc = new Call(c->loc().introduce(), array_bool_or->id(), args);
3533 nc->type(Type::varbool());
3534 nc->decl(array_bool_or);
3535 }
3536 } else if (c->id() == constants().ids.forall) {
3537 if (array_bool_and != nullptr) {
3538 std::vector<Expression*> args(2);
3539 args[0] = c->arg(0);
3540 args[1] = constants().literalTrue;
3541 nc = new Call(c->loc().introduce(), array_bool_and->id(), args);
3542 nc->type(Type::varbool());
3543 nc->decl(array_bool_and);
3544 }
3545 } else if (c->id() == constants().ids.clause) {
3546 if (array_bool_clause != nullptr) {
3547 std::vector<Expression*> args(2);
3548 args[0] = c->arg(0);
3549 args[1] = c->arg(1);
3550 nc = new Call(c->loc().introduce(), array_bool_clause->id(), args);
3551 nc->type(Type::varbool());
3552 nc->decl(array_bool_clause);
3553 }
3554 } else if (c->id() == constants().ids.bool_xor) {
3555 if (bool_xor != nullptr) {
3556 std::vector<Expression*> args(3);
3557 args[0] = c->arg(0);
3558 args[1] = c->arg(1);
3559 args[2] = c->argCount() == 2 ? constants().literalTrue : c->arg(2);
3560 nc = new Call(c->loc().introduce(), bool_xor->id(), args);
3561 nc->type(Type::varbool());
3562 nc->decl(bool_xor);
3563 }
3564 } else if (c->id() == constants().ids.bool_not && c->argCount() == 1 &&
3565 c->decl()->e() == nullptr) {
3566 if (c->arg(0) == constants().boollit(true)) {
3567 env.fail();
3568 } else if (c->arg(0) == constants().boollit(false)) {
3569 // nothing to do, not false = true
3570 } else if (c->arg(0)->isa<Id>()) {
3571 VarDecl* vd = c->arg(0)->cast<Id>()->decl();
3572 if (vd->ti()->domain() == nullptr) {
3573 vd->ti()->domain(constants().boollit(false));
3574 } else if (vd->ti()->domain() == constants().boollit(true)) {
3575 env.fail();
3576 }
3577 } else {
3578 // don't know how to handle, use bool_not/2
3579 nc =
3580 new Call(c->loc().introduce(), c->id(), {c->arg(0), constants().boollit(true)});
3581 nc->type(Type::varbool());
3582 nc->decl(env.model->matchFn(env, nc, false));
3583 }
3584 if (nc == nullptr) {
3585 env.flatRemoveItem(ci);
3586 }
3587 } else {
3588 FunctionI* decl = env.model->matchFn(env, c, false);
3589 if ((decl != nullptr) && (decl->e() != nullptr)) {
3590 nc = c;
3591 nc->decl(decl);
3592 }
3593 }
3594 if (nc != nullptr) {
3595 if (nc != c) {
3596 for (ExpressionSetIter it = c->ann().begin(); it != c->ann().end(); ++it) {
3597 EE ee_ann = flat_exp(env, Ctx(), *it, nullptr, constants().varTrue);
3598 nc->addAnnotation(ee_ann.r());
3599 }
3600 }
3601 StringLit* sl = get_longest_mzn_path_annotation(env, c);
3602 CallStackItem* csi = nullptr;
3603 if (sl != nullptr) {
3604 csi = new CallStackItem(env, sl);
3605 }
3606 ItemTimer item_timer(nc->loc(), timingMap);
3607 (void)flat_exp(env, Ctx(), nc, constants().varTrue, constants().varTrue);
3608 env.flatRemoveItem(ci);
3609
3610 delete csi;
3611 }
3612 }
3613 }
3614 }
3615
3616 startItem = endItem + 1;
3617 endItem = static_cast<int>(m.size()) - 1;
3618 }
3619
3620 // Add redefinitions for output variables that may have been redefined since create_output
3621 for (unsigned int i = 0; i < env.output->size(); i++) {
3622 if (auto* vdi = (*env.output)[i]->dynamicCast<VarDeclI>()) {
3623 IdMap<KeepAlive>::iterator it;
3624 if (vdi->e()->e() == nullptr &&
3625 (it = env.reverseMappers.find(vdi->e()->id())) != env.reverseMappers.end()) {
3626 GCLock lock;
3627 Call* rhs = copy(env, env.cmap, it->second())->cast<Call>();
3628 check_output_par_fn(env, rhs);
3629 output_vardecls(env, vdi, rhs);
3630
3631 remove_is_output(vdi->e()->flat());
3632 vdi->e()->e(rhs);
3633 }
3634 }
3635 }
3636
3637 if (!opt.keepOutputInFzn) {
3638 finalise_output(env);
3639 }
3640
3641 for (auto& i : m) {
3642 if (auto* ci = i->dynamicCast<ConstraintI>()) {
3643 if (Call* c = ci->e()->dynamicCast<Call>()) {
3644 if (c->decl() == constants().varRedef) {
3645 env.flatRemoveItem(ci);
3646 }
3647 }
3648 }
3649 }
3650
3651 cleanup_output(env);
3652 } catch (ModelInconsistent&) {
3653 }
3654
3655 if (opt.detailedTiming) {
3656 e.envi().outstream << "% Compilation profile (file,line,milliseconds)\n";
3657 if (opt.collectMznPaths) {
3658 e.envi().outstream << "% (time is allocated to toplevel item)\n";
3659 } else {
3660 e.envi().outstream << "% (locations are approximate, use --keep-paths to allocate times to "
3661 "toplevel items)\n";
3662 }
3663 for (auto& entry : *timingMap) {
3664 std::chrono::milliseconds time_taken =
3665 std::chrono::duration_cast<std::chrono::milliseconds>(entry.second);
3666 if (time_taken > std::chrono::milliseconds(0)) {
3667 e.envi().outstream << "%%%mzn-stat: profiling=[\"" << entry.first.first << "\","
3668 << entry.first.second << "," << time_taken.count() << "]\n";
3669 }
3670 }
3671 e.envi().outstream << "%%%mzn-stat-end\n";
3672 }
3673}
3674
3675void clear_internal_annotations(Expression* e, bool keepDefinesVar) {
3676 e->ann().remove(constants().ann.promise_total);
3677 e->ann().remove(constants().ann.maybe_partial);
3678 e->ann().remove(constants().ann.add_to_output);
3679 e->ann().remove(constants().ann.rhs_from_assignment);
3680 e->ann().remove(constants().ann.mzn_was_undefined);
3681 // Remove defines_var(x) annotation where x is par
3682 std::vector<Expression*> removeAnns;
3683 for (ExpressionSetIter anns = e->ann().begin(); anns != e->ann().end(); ++anns) {
3684 if (Call* c = (*anns)->dynamicCast<Call>()) {
3685 if (c->id() == constants().ann.defines_var &&
3686 (!keepDefinesVar || c->arg(0)->type().isPar())) {
3687 removeAnns.push_back(c);
3688 }
3689 }
3690 }
3691 for (auto& removeAnn : removeAnns) {
3692 e->ann().remove(removeAnn);
3693 }
3694}
3695
3696std::vector<Expression*> cleanup_vardecl(EnvI& env, VarDeclI* vdi, VarDecl* vd,
3697 bool keepDefinesVar) {
3698 std::vector<Expression*> added_constraints;
3699
3700 // In FlatZinc par variables have RHSs, not domains
3701 if (vd->type().isPar()) {
3702 vd->ann().clear();
3703 vd->introduced(false);
3704 vd->ti()->domain(nullptr);
3705 }
3706
3707 // In FlatZinc the RHS of a VarDecl must be a literal, Id or empty
3708 // Example:
3709 // var 1..5: x = function(y)
3710 // becomes:
3711 // var 1..5: x;
3712 // relation(x, y);
3713 if (vd->type().isvar() && vd->type().isbool()) {
3714 bool is_fixed = (vd->ti()->domain() != nullptr);
3715 if (Expression::equal(vd->ti()->domain(), constants().literalTrue)) {
3716 // Ex: var true: b = e()
3717
3718 // Store RHS
3719 Expression* ve = vd->e();
3720 vd->e(constants().literalTrue);
3721 vd->ti()->domain(nullptr);
3722 // Ex: var bool: b = true
3723
3724 // If vd had a RHS
3725 if (ve != nullptr) {
3726 if (Call* vcc = ve->dynamicCast<Call>()) {
3727 // Convert functions to relations:
3728 // exists([x]) => array_bool_or([x],true)
3729 // forall([x]) => array_bool_and([x],true)
3730 // clause([x]) => bool_clause([x])
3731 ASTString cid;
3732 std::vector<Expression*> args;
3733 if (vcc->id() == constants().ids.exists) {
3734 cid = constants().ids.array_bool_or;
3735 args.push_back(vcc->arg(0));
3736 args.push_back(constants().literalTrue);
3737 } else if (vcc->id() == constants().ids.forall) {
3738 cid = constants().ids.array_bool_and;
3739 args.push_back(vcc->arg(0));
3740 args.push_back(constants().literalTrue);
3741 } else if (vcc->id() == constants().ids.clause) {
3742 cid = constants().ids.bool_clause;
3743 args.push_back(vcc->arg(0));
3744 args.push_back(vcc->arg(1));
3745 }
3746
3747 if (args.empty()) {
3748 // Post original RHS as stand alone constraint
3749 ve = vcc;
3750 } else {
3751 // Create new call, retain annotations from original RHS
3752 Call* nc = new Call(vcc->loc().introduce(), cid, args);
3753 nc->type(vcc->type());
3754 nc->ann().merge(vcc->ann());
3755 ve = nc;
3756 }
3757 } else if (Id* id = ve->dynamicCast<Id>()) {
3758 if (id->decl()->ti()->domain() != constants().literalTrue) {
3759 // Inconsistent assignment: post bool_eq(y, true)
3760 std::vector<Expression*> args(2);
3761 args[0] = id;
3762 args[1] = constants().literalTrue;
3763 GCLock lock;
3764 ve = new Call(Location().introduce(), constants().ids.bool_eq, args);
3765 } else {
3766 // Don't post this
3767 ve = constants().literalTrue;
3768 }
3769 }
3770 // Post new constraint
3771 if (ve != constants().literalTrue) {
3772 clear_internal_annotations(ve, keepDefinesVar);
3773 added_constraints.push_back(ve);
3774 }
3775 }
3776 } else {
3777 // Ex: var false: b = e()
3778 if (vd->e() != nullptr) {
3779 if (vd->e()->eid() == Expression::E_CALL) {
3780 // Convert functions to relations:
3781 // var false: b = exists([x]) => array_bool_or([x], b)
3782 // var false: b = forall([x]) => array_bool_and([x], b)
3783 // var false: b = clause([x]) => bool_clause_reif([x], b)
3784 const Call* c = vd->e()->cast<Call>();
3785 GCLock lock;
3786 vd->e(nullptr);
3787 ASTString cid;
3788 std::vector<Expression*> args(c->argCount());
3789 for (unsigned int i = args.size(); (i--) != 0U;) {
3790 args[i] = c->arg(i);
3791 }
3792 if (is_fixed) {
3793 args.push_back(constants().literalFalse);
3794 } else {
3795 args.push_back(vd->id());
3796 }
3797 if (c->id() == constants().ids.exists) {
3798 cid = constants().ids.array_bool_or;
3799 } else if (c->id() == constants().ids.forall) {
3800 cid = constants().ids.array_bool_and;
3801 } else if (c->id() == constants().ids.clause) {
3802 cid = constants().ids.bool_clause_reif;
3803 } else {
3804 if (env.fopts.enableHalfReification && vd->ann().contains(constants().ctx.pos)) {
3805 cid = env.halfReifyId(c->id());
3806 if (env.model->matchFn(env, cid, args, false) == nullptr) {
3807 cid = env.reifyId(c->id());
3808 }
3809 } else {
3810 cid = env.reifyId(c->id());
3811 }
3812 }
3813 Call* nc = new Call(c->loc().introduce(), cid, args);
3814 nc->type(c->type());
3815 FunctionI* decl = env.model->matchFn(env, nc, false);
3816 if (decl == nullptr) {
3817 std::ostringstream ss;
3818 ss << "'" << c->id()
3819 << "' is used in a reified context but no reified version is available";
3820 throw FlatteningError(env, c->loc(), ss.str());
3821 }
3822 nc->decl(decl);
3823 if (!is_fixed) {
3824 make_defined_var(vd, nc);
3825 }
3826 nc->ann().merge(c->ann());
3827 clear_internal_annotations(nc, keepDefinesVar);
3828 added_constraints.push_back(nc);
3829 } else {
3830 assert(vd->e()->eid() == Expression::E_ID || vd->e()->eid() == Expression::E_BOOLLIT);
3831 }
3832 }
3833 if (Expression::equal(vd->ti()->domain(), constants().literalFalse)) {
3834 vd->ti()->domain(nullptr);
3835 vd->e(constants().literalFalse);
3836 }
3837 }
3838 if (vdi != nullptr && is_fixed && env.varOccurrences.occurrences(vd) == 0) {
3839 if (is_output(vd)) {
3840 VarDecl* vd_output =
3841 (*env.output)[env.outputFlatVarOccurrences.find(vd)]->cast<VarDeclI>()->e();
3842 if (vd_output->e() == nullptr) {
3843 vd_output->e(vd->e());
3844 }
3845 }
3846 env.flatRemoveItem(vdi);
3847 }
3848 } else if (vd->type().isvar() && vd->type().dim() == 0) {
3849 // Int or Float var
3850 if (vd->e() != nullptr) {
3851 if (const Call* cc = vd->e()->dynamicCast<Call>()) {
3852 // Remove RHS from vd
3853 vd->e(nullptr);
3854
3855 std::vector<Expression*> args(cc->argCount());
3856 ASTString cid;
3857 if (cc->id() == constants().ids.lin_exp) {
3858 // a = lin_exp([1],[b],5) => int_lin_eq([1,-1],[b,a],-5):: defines_var(a)
3859 auto* le_c = follow_id(cc->arg(0))->cast<ArrayLit>();
3860 std::vector<Expression*> nc(le_c->size());
3861 for (auto i = static_cast<unsigned int>(nc.size()); (i--) != 0U;) {
3862 nc[i] = (*le_c)[i];
3863 }
3864 if (le_c->type().bt() == Type::BT_INT) {
3865 cid = constants().ids.int_.lin_eq;
3866 nc.push_back(IntLit::a(-1));
3867 args[0] = new ArrayLit(Location().introduce(), nc);
3868 args[0]->type(Type::parint(1));
3869 auto* le_x = follow_id(cc->arg(1))->cast<ArrayLit>();
3870 std::vector<Expression*> nx(le_x->size());
3871 for (auto i = static_cast<unsigned int>(nx.size()); (i--) != 0U;) {
3872 nx[i] = (*le_x)[i];
3873 }
3874 nx.push_back(vd->id());
3875 args[1] = new ArrayLit(Location().introduce(), nx);
3876 args[1]->type(le_x->type());
3877 IntVal d = cc->arg(2)->cast<IntLit>()->v();
3878 args[2] = IntLit::a(-d);
3879 } else {
3880 // float
3881 cid = constants().ids.float_.lin_eq;
3882 nc.push_back(FloatLit::a(-1.0));
3883 args[0] = new ArrayLit(Location().introduce(), nc);
3884 args[0]->type(Type::parfloat(1));
3885 auto* le_x = follow_id(cc->arg(1))->cast<ArrayLit>();
3886 std::vector<Expression*> nx(le_x->size());
3887 for (auto i = static_cast<unsigned int>(nx.size()); (i--) != 0U;) {
3888 nx[i] = (*le_x)[i];
3889 }
3890 nx.push_back(vd->id());
3891 args[1] = new ArrayLit(Location().introduce(), nx);
3892 args[1]->type(le_x->type());
3893 FloatVal d = cc->arg(2)->cast<FloatLit>()->v();
3894 args[2] = FloatLit::a(-d);
3895 }
3896 } else {
3897 if (cc->id() == "card") {
3898 // card is 'set_card' in old FlatZinc
3899 cid = constants().ids.set_card;
3900 } else {
3901 cid = cc->id();
3902 }
3903 for (auto i = static_cast<unsigned int>(args.size()); (i--) != 0U;) {
3904 args[i] = cc->arg(i);
3905 }
3906 args.push_back(vd->id());
3907 }
3908 Call* nc = new Call(cc->loc().introduce(), cid, args);
3909 nc->type(cc->type());
3910 make_defined_var(vd, nc);
3911 nc->ann().merge(cc->ann());
3912
3913 clear_internal_annotations(nc, keepDefinesVar);
3914 added_constraints.push_back(nc);
3915 } else {
3916 // RHS must be literal or Id
3917 assert(vd->e()->eid() == Expression::E_ID || vd->e()->eid() == Expression::E_INTLIT ||
3918 vd->e()->eid() == Expression::E_FLOATLIT ||
3919 vd->e()->eid() == Expression::E_BOOLLIT || vd->e()->eid() == Expression::E_SETLIT);
3920 }
3921 }
3922 } else if (vd->type().dim() > 0) {
3923 // vd is an array
3924
3925 // If RHS is an Id, follow id to RHS
3926 // a = [1,2,3]; b = a;
3927 // vd = b => vd = [1,2,3]
3928 if (!vd->e()->isa<ArrayLit>()) {
3929 vd->e(follow_id(vd->e()));
3930 }
3931
3932 // If empty array or 1 indexed, continue
3933 if (vd->ti()->ranges().size() == 1 && vd->ti()->ranges()[0]->domain() != nullptr &&
3934 vd->ti()->ranges()[0]->domain()->isa<SetLit>()) {
3935 IntSetVal* isv = vd->ti()->ranges()[0]->domain()->cast<SetLit>()->isv();
3936 if ((isv != nullptr) && (isv->size() == 0 || isv->min(0) == 1)) {
3937 return added_constraints;
3938 }
3939 }
3940
3941 // Array should be 1 indexed since ArrayLit is 1 indexed
3942 assert(vd->e() != nullptr);
3943 ArrayLit* al = nullptr;
3944 Expression* e = vd->e();
3945 while (al == nullptr) {
3946 switch (e->eid()) {
3947 case Expression::E_ARRAYLIT:
3948 al = e->cast<ArrayLit>();
3949 break;
3950 case Expression::E_ID:
3951 e = e->cast<Id>()->decl()->e();
3952 break;
3953 default:
3954 assert(false);
3955 }
3956 }
3957 al->make1d();
3958 IntSetVal* isv = IntSetVal::a(1, al->length());
3959 if (vd->ti()->ranges().size() == 1) {
3960 vd->ti()->ranges()[0]->domain(new SetLit(Location().introduce(), isv));
3961 } else {
3962 std::vector<TypeInst*> r(1);
3963 r[0] = new TypeInst(vd->ti()->ranges()[0]->loc(), vd->ti()->ranges()[0]->type(),
3964 new SetLit(Location().introduce(), isv));
3965 ASTExprVec<TypeInst> ranges(r);
3966 auto* ti = new TypeInst(vd->ti()->loc(), vd->ti()->type(), ranges, vd->ti()->domain());
3967 vd->ti(ti);
3968 }
3969 }
3970
3971 // Remove boolean context annotations used only on compilation
3972 vd->ann().remove(constants().ctx.mix);
3973 vd->ann().remove(constants().ctx.pos);
3974 vd->ann().remove(constants().ctx.neg);
3975 vd->ann().remove(constants().ctx.root);
3976 vd->ann().remove(constants().ann.promise_total);
3977 vd->ann().remove(constants().ann.add_to_output);
3978 vd->ann().remove(constants().ann.mzn_check_var);
3979 vd->ann().remove(constants().ann.rhs_from_assignment);
3980 vd->ann().remove(constants().ann.mzn_was_undefined);
3981 vd->ann().removeCall(constants().ann.mzn_check_enum_var);
3982
3983 return added_constraints;
3984}
3985
3986Expression* cleanup_constraint(EnvI& env, std::unordered_set<Item*>& globals, Expression* ce,
3987 bool keepDefinesVar) {
3988 clear_internal_annotations(ce, keepDefinesVar);
3989
3990 if (Call* vc = ce->dynamicCast<Call>()) {
3991 for (unsigned int i = 0; i < vc->argCount(); i++) {
3992 // Change array indicies to be 1 indexed
3993 if (auto* al = vc->arg(i)->dynamicCast<ArrayLit>()) {
3994 if (al->dims() > 1 || al->min(0) != 1) {
3995 al->make1d();
3996 }
3997 }
3998 }
3999 // Convert functions to relations:
4000 // exists([x]) => array_bool_or([x],true)
4001 // forall([x]) => array_bool_and([x],true)
4002 // clause([x]) => bool_clause([x])
4003 // bool_xor([x],[y]) => bool_xor([x],[y],true)
4004 if (vc->id() == constants().ids.exists) {
4005 GCLock lock;
4006 vc->id(constants().ids.array_bool_or);
4007 std::vector<Expression*> args(2);
4008 args[0] = vc->arg(0);
4009 args[1] = constants().literalTrue;
4010 ASTExprVec<Expression> argsv(args);
4011 vc->args(argsv);
4012 vc->decl(env.model->matchFn(env, vc, false));
4013 } else if (vc->id() == constants().ids.forall) {
4014 GCLock lock;
4015 vc->id(constants().ids.array_bool_and);
4016 std::vector<Expression*> args(2);
4017 args[0] = vc->arg(0);
4018 args[1] = constants().literalTrue;
4019 ASTExprVec<Expression> argsv(args);
4020 vc->args(argsv);
4021 vc->decl(env.model->matchFn(env, vc, false));
4022 } else if (vc->id() == constants().ids.clause) {
4023 GCLock lock;
4024 vc->id(constants().ids.bool_clause);
4025 vc->decl(env.model->matchFn(env, vc, false));
4026 } else if (vc->id() == constants().ids.bool_xor && vc->argCount() == 2) {
4027 GCLock lock;
4028 std::vector<Expression*> args(3);
4029 args[0] = vc->arg(0);
4030 args[1] = vc->arg(1);
4031 args[2] = constants().literalTrue;
4032 ASTExprVec<Expression> argsv(args);
4033 vc->args(argsv);
4034 vc->decl(env.model->matchFn(env, vc, false));
4035 }
4036
4037 // If vc->decl() is a solver builtin and has not been added to the
4038 // FlatZinc, add it
4039 if ((vc->decl() != nullptr) && vc->decl() != constants().varRedef &&
4040 !vc->decl()->fromStdLib() && globals.find(vc->decl()) == globals.end()) {
4041 std::vector<VarDecl*> params(vc->decl()->params().size());
4042 for (unsigned int i = 0; i < params.size(); i++) {
4043 params[i] = vc->decl()->params()[i];
4044 }
4045 GCLock lock;
4046 auto* vc_decl_copy = new FunctionI(vc->decl()->loc(), vc->decl()->id(), vc->decl()->ti(),
4047 params, vc->decl()->e());
4048 env.flatAddItem(vc_decl_copy);
4049 globals.insert(vc->decl());
4050 }
4051 return ce;
4052 }
4053 if (Id* id = ce->dynamicCast<Id>()) {
4054 // Ex: constraint b; => constraint bool_eq(b, true);
4055 std::vector<Expression*> args(2);
4056 args[0] = id;
4057 args[1] = constants().literalTrue;
4058 GCLock lock;
4059 return new Call(Location().introduce(), constants().ids.bool_eq, args);
4060 }
4061 if (auto* bl = ce->dynamicCast<BoolLit>()) {
4062 // Ex: true => delete; false => bool_eq(false, true);
4063 if (!bl->v()) {
4064 GCLock lock;
4065 std::vector<Expression*> args(2);
4066 args[0] = constants().literalFalse;
4067 args[1] = constants().literalTrue;
4068 Call* neq = new Call(Location().introduce(), constants().ids.bool_eq, args);
4069 return neq;
4070 }
4071 return nullptr;
4072 }
4073 return ce;
4074}
4075
4076void oldflatzinc(Env& e) {
4077 Model* m = e.flat();
4078
4079 // Check wheter we need to keep defines_var annotations
4080 bool keepDefinesVar = true;
4081 {
4082 GCLock lock;
4083 Call* c = new Call(Location().introduce(), "mzn_check_annotate_defines_var", {});
4084 c->type(Type::parbool());
4085 FunctionI* fi = e.model()->matchFn(e.envi(), c, true);
4086 if (fi != nullptr) {
4087 c->decl(fi);
4088 keepDefinesVar = eval_bool(e.envi(), c);
4089 }
4090 }
4091
4092 // Mark annotations and optional variables for removal, and clear flags
4093 for (auto& vdi : m->vardecls()) {
4094 if (vdi.e()->type().ot() == Type::OT_OPTIONAL || vdi.e()->type().bt() == Type::BT_ANN) {
4095 vdi.remove();
4096 }
4097 }
4098
4099 EnvI& env = e.envi();
4100
4101 unsigned int msize = m->size();
4102
4103 // Predicate declarations of solver builtins
4104 std::unordered_set<Item*> globals;
4105
4106 // Variables mapped to the index of the constraint that defines them
4107 enum DFS_STATUS { DFS_UNKNOWN, DFS_SEEN, DFS_DONE };
4108 std::unordered_map<VarDecl*, std::pair<int, DFS_STATUS>> definition_map;
4109
4110 // Record indices of VarDeclIs with Id RHS for sorting & unification
4111 std::vector<int> declsWithIds;
4112 for (int i = 0; i < msize; i++) {
4113 if ((*m)[i]->removed()) {
4114 continue;
4115 }
4116 if (auto* vdi = (*m)[i]->dynamicCast<VarDeclI>()) {
4117 GCLock lock;
4118 VarDecl* vd = vdi->e();
4119 std::vector<Expression*> added_constraints =
4120 cleanup_vardecl(e.envi(), vdi, vd, keepDefinesVar);
4121 // Record whether this VarDecl is equal to an Id (aliasing)
4122 if ((vd->e() != nullptr) && vd->e()->isa<Id>()) {
4123 declsWithIds.push_back(i);
4124 vdi->e()->payload(-static_cast<int>(i) - 1);
4125 } else {
4126 vdi->e()->payload(i);
4127 }
4128 for (auto* nc : added_constraints) {
4129 Expression* new_ce = cleanup_constraint(e.envi(), globals, nc, keepDefinesVar);
4130 if (new_ce != nullptr) {
4131 e.envi().flatAddItem(new ConstraintI(Location().introduce(), new_ce));
4132 }
4133 }
4134 } else if (auto* ci = (*m)[i]->dynamicCast<ConstraintI>()) {
4135 Expression* new_ce = cleanup_constraint(e.envi(), globals, ci->e(), keepDefinesVar);
4136 if (new_ce != nullptr) {
4137 ci->e(new_ce);
4138 if (keepDefinesVar) {
4139 if (Call* defines_var = new_ce->ann().getCall(constants().ann.defines_var)) {
4140 if (Id* ident = defines_var->arg(0)->dynamicCast<Id>()) {
4141 if (definition_map.find(ident->decl()) != definition_map.end()) {
4142 // This is the second definition, remove it
4143 new_ce->ann().removeCall(constants().ann.defines_var);
4144 } else {
4145 definition_map.insert({ident->decl(), {i, DFS_UNKNOWN}});
4146 }
4147 }
4148 }
4149 }
4150 } else {
4151 ci->remove();
4152 }
4153 } else if (auto* fi = (*m)[i]->dynamicCast<FunctionI>()) {
4154 if (Let* let = Expression::dynamicCast<Let>(fi->e())) {
4155 GCLock lock;
4156 std::vector<Expression*> new_let;
4157 for (unsigned int i = 0; i < let->let().size(); i++) {
4158 Expression* let_e = let->let()[i];
4159 if (auto* vd = let_e->dynamicCast<VarDecl>()) {
4160 std::vector<Expression*> added_constraints =
4161 cleanup_vardecl(e.envi(), nullptr, vd, keepDefinesVar);
4162 new_let.push_back(vd);
4163 for (auto* nc : added_constraints) {
4164 new_let.push_back(nc);
4165 }
4166 } else {
4167 Expression* new_ce = cleanup_constraint(e.envi(), globals, let_e, keepDefinesVar);
4168 if (new_ce != nullptr) {
4169 new_let.push_back(new_ce);
4170 }
4171 }
4172 }
4173 fi->e(new Let(let->loc(), new_let, let->in()));
4174 }
4175 } else if (auto* si = (*m)[i]->dynamicCast<SolveI>()) {
4176 if ((si->e() != nullptr) && si->e()->type().isPar()) {
4177 // Introduce VarDecl if objective expression is par
4178 GCLock lock;
4179 auto* ti = new TypeInst(Location().introduce(), si->e()->type(), nullptr);
4180 auto* constantobj = new VarDecl(Location().introduce(), ti, e.envi().genId(), si->e());
4181 si->e(constantobj->id());
4182 e.envi().flatAddItem(new VarDeclI(Location().introduce(), constantobj));
4183 }
4184 }
4185 }
4186
4187 if (keepDefinesVar) {
4188 // Detect and break cycles in defines_var annotations
4189 std::vector<VarDecl*> definesStack;
4190 auto checkId = [&definesStack, &definition_map, &m](VarDecl* cur, Id* ident) {
4191 if (cur == ident->decl()) {
4192 // Never push the variable we're currently looking at
4193 return;
4194 }
4195 auto it = definition_map.find(ident->decl());
4196 if (it != definition_map.end()) {
4197 if (it->second.second == 0) {
4198 // not yet visited, push
4199 definesStack.push_back(it->first);
4200 } else if (it->second.second == 1) {
4201 // Found a cycle through variable ident
4202 // Break cycle by removing annotations
4203 ident->decl()->ann().remove(constants().ann.is_defined_var);
4204 Call* c = (*m)[it->second.first]->cast<ConstraintI>()->e()->cast<Call>();
4205 c->ann().removeCall(constants().ann.defines_var);
4206 }
4207 }
4208 };
4209 for (auto& it : definition_map) {
4210 if (it.second.second == 0) {
4211 // not yet visited
4212 definesStack.push_back(it.first);
4213 while (!definesStack.empty()) {
4214 VarDecl* cur = definesStack.back();
4215 if (definition_map[cur].second != DFS_UNKNOWN) {
4216 // already visited (or already finished), now finished
4217 definition_map[cur].second = DFS_DONE;
4218 definesStack.pop_back();
4219 } else {
4220 // now visited and on stack
4221 definition_map[cur].second = DFS_SEEN;
4222 if (Call* c = (*m)[definition_map[cur].first]
4223 ->cast<ConstraintI>()
4224 ->e()
4225 ->dynamicCast<Call>()) {
4226 // Variable is defined by a call, push all arguments
4227 for (unsigned int i = 0; i < c->argCount(); i++) {
4228 if (c->arg(i)->type().isPar()) {
4229 continue;
4230 }
4231 if (Id* ident = c->arg(i)->dynamicCast<Id>()) {
4232 if (ident->type().dim() > 0) {
4233 if (auto* al = Expression::dynamicCast<ArrayLit>(ident->decl()->e())) {
4234 for (auto* e : al->getVec()) {
4235 if (auto* ident = e->dynamicCast<Id>()) {
4236 checkId(cur, ident);
4237 }
4238 }
4239 }
4240 } else if (ident->type().isvar()) {
4241 checkId(cur, ident);
4242 }
4243 } else if (auto* al = c->arg(i)->dynamicCast<ArrayLit>()) {
4244 for (auto* e : al->getVec()) {
4245 if (auto* ident = e->dynamicCast<Id>()) {
4246 checkId(cur, ident);
4247 }
4248 }
4249 }
4250 }
4251 }
4252 }
4253 }
4254 }
4255 }
4256 }
4257
4258 // Sort VarDecls in FlatZinc so that VarDecls are declared before use
4259 std::vector<VarDeclI*> sortedVarDecls(declsWithIds.size());
4260 int vdCount = 0;
4261 for (int declsWithId : declsWithIds) {
4262 VarDecl* cur = (*m)[declsWithId]->cast<VarDeclI>()->e();
4263 std::vector<int> stack;
4264 while ((cur != nullptr) && cur->payload() < 0) {
4265 stack.push_back(cur->payload());
4266 if (Id* id = cur->e()->dynamicCast<Id>()) {
4267 cur = id->decl();
4268 } else {
4269 cur = nullptr;
4270 }
4271 }
4272 for (auto i = static_cast<unsigned int>(stack.size()); (i--) != 0U;) {
4273 auto* vdi = (*m)[-stack[i] - 1]->cast<VarDeclI>();
4274 vdi->e()->payload(-vdi->e()->payload() - 1);
4275 sortedVarDecls[vdCount++] = vdi;
4276 }
4277 }
4278 for (unsigned int i = 0; i < declsWithIds.size(); i++) {
4279 (*m)[declsWithIds[i]] = sortedVarDecls[i];
4280 }
4281
4282 // Remove marked items
4283 m->compact();
4284 e.envi().output->compact();
4285
4286 for (auto& it : env.varOccurrences.itemMap) {
4287 std::vector<Item*> toRemove;
4288 for (auto* iit : it.second) {
4289 if (iit->removed()) {
4290 toRemove.push_back(iit);
4291 }
4292 }
4293 for (auto& i : toRemove) {
4294 it.second.erase(i);
4295 }
4296 }
4297
4298 class Cmp {
4299 public:
4300 bool operator()(Item* i, Item* j) {
4301 if (i->iid() == Item::II_FUN || j->iid() == Item::II_FUN) {
4302 if (i->iid() == j->iid()) {
4303 return false;
4304 }
4305 return i->iid() == Item::II_FUN;
4306 }
4307 if (i->iid() == Item::II_SOL) {
4308 assert(j->iid() != i->iid());
4309 return false;
4310 }
4311 if (j->iid() == Item::II_SOL) {
4312 assert(j->iid() != i->iid());
4313 return true;
4314 }
4315 if (i->iid() == Item::II_VD) {
4316 if (j->iid() != i->iid()) {
4317 return true;
4318 }
4319 if (i->cast<VarDeclI>()->e()->type().isPar() && j->cast<VarDeclI>()->e()->type().isvar()) {
4320 return true;
4321 }
4322 if (j->cast<VarDeclI>()->e()->type().isPar() && i->cast<VarDeclI>()->e()->type().isvar()) {
4323 return false;
4324 }
4325 if (i->cast<VarDeclI>()->e()->type().dim() == 0 &&
4326 j->cast<VarDeclI>()->e()->type().dim() != 0) {
4327 return true;
4328 }
4329 if (i->cast<VarDeclI>()->e()->type().dim() != 0 &&
4330 j->cast<VarDeclI>()->e()->type().dim() == 0) {
4331 return false;
4332 }
4333 if (i->cast<VarDeclI>()->e()->e() == nullptr && j->cast<VarDeclI>()->e()->e() != nullptr) {
4334 return true;
4335 }
4336 if ((i->cast<VarDeclI>()->e()->e() != nullptr) &&
4337 (j->cast<VarDeclI>()->e()->e() != nullptr) &&
4338 !i->cast<VarDeclI>()->e()->e()->isa<Id>() && j->cast<VarDeclI>()->e()->e()->isa<Id>()) {
4339 return true;
4340 }
4341 }
4342 return false;
4343 }
4344 } _cmp;
4345 // Perform final sorting
4346 std::stable_sort(m->begin(), m->end(), _cmp);
4347}
4348
4349FlatModelStatistics statistics(Env& m) {
4350 Model* flat = m.flat();
4351 FlatModelStatistics stats;
4352 stats.n_reif_ct = m.envi().counters.reifConstraints;
4353 stats.n_imp_ct = m.envi().counters.impConstraints;
4354 stats.n_imp_del = m.envi().counters.impDel;
4355 stats.n_lin_del = m.envi().counters.linDel;
4356 for (auto& i : *flat) {
4357 if (!i->removed()) {
4358 if (auto* vdi = i->dynamicCast<VarDeclI>()) {
4359 Type t = vdi->e()->type();
4360 if (t.isvar() && t.dim() == 0) {
4361 if (t.isSet()) {
4362 stats.n_set_vars++;
4363 } else if (t.isint()) {
4364 stats.n_int_vars++;
4365 } else if (t.isbool()) {
4366 stats.n_bool_vars++;
4367 } else if (t.isfloat()) {
4368 stats.n_float_vars++;
4369 }
4370 }
4371 } else if (auto* ci = i->dynamicCast<ConstraintI>()) {
4372 if (Call* call = ci->e()->dynamicCast<Call>()) {
4373 if (call->id().endsWith("_reif")) {
4374 stats.n_reif_ct++;
4375 } else if (call->id().endsWith("_imp")) {
4376 stats.n_imp_ct++;
4377 }
4378 if (call->argCount() > 0) {
4379 Type all_t;
4380 for (unsigned int i = 0; i < call->argCount(); i++) {
4381 Type t = call->arg(i)->type();
4382 if (t.isvar()) {
4383 if (t.st() == Type::ST_SET ||
4384 (t.bt() == Type::BT_FLOAT && all_t.st() != Type::ST_SET) ||
4385 (t.bt() == Type::BT_INT && all_t.bt() != Type::BT_FLOAT &&
4386 all_t.st() != Type::ST_SET) ||
4387 (t.bt() == Type::BT_BOOL && all_t.bt() != Type::BT_INT &&
4388 all_t.bt() != Type::BT_FLOAT && all_t.st() != Type::ST_SET)) {
4389 all_t = t;
4390 }
4391 }
4392 }
4393 if (all_t.isvar()) {
4394 if (all_t.st() == Type::ST_SET) {
4395 stats.n_set_ct++;
4396 } else if (all_t.bt() == Type::BT_INT) {
4397 stats.n_int_ct++;
4398 } else if (all_t.bt() == Type::BT_BOOL) {
4399 stats.n_bool_ct++;
4400 } else if (all_t.bt() == Type::BT_FLOAT) {
4401 stats.n_float_ct++;
4402 }
4403 }
4404 }
4405 }
4406 }
4407 }
4408 }
4409 return stats;
4410}
4411
4412} // namespace MiniZinc