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