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