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