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/flat_exp.hh>
13 
14 namespace MiniZinc {
15 
to_exp_vec(std::vector<KeepAlive> & v)16 std::vector<Expression*> to_exp_vec(std::vector<KeepAlive>& v) {
17   std::vector<Expression*> r(v.size());
18   for (auto i = static_cast<unsigned int>(v.size()); (i--) != 0U;) {
19     r[i] = v[i]();
20   }
21   return r;
22 }
23 
is_total(FunctionI * fi)24 bool is_total(FunctionI* fi) { return fi->ann().contains(constants().ann.promise_total); }
25 
same_call(EnvI & env,Expression * e,const ASTString & id)26 Call* same_call(EnvI& env, Expression* e, const ASTString& id) {
27   assert(GC::locked());
28   Expression* ce = follow_id(e);
29   Call* c = Expression::dynamicCast<Call>(ce);
30   if (c != nullptr) {
31     if (c->id() == id) {
32       return ce->cast<Call>();
33     }
34     if (c->id() == constants().ids.int2float) {
35       Expression* i2f = follow_id(c->arg(0));
36       Call* i2fc = Expression::dynamicCast<Call>(i2f);
37       if ((i2fc != nullptr) && i2fc->id() == id && id == constants().ids.lin_exp) {
38         ArrayLit* coeffs = eval_array_lit(env, i2fc->arg(0));
39         std::vector<Expression*> ncoeff_v(coeffs->size());
40         for (unsigned int i = 0; i < coeffs->size(); i++) {
41           ncoeff_v[i] = FloatLit::a(eval_int(env, (*coeffs)[i]));
42         }
43         auto* ncoeff = new ArrayLit(coeffs->loc().introduce(), ncoeff_v);
44         ncoeff->type(Type::parfloat(1));
45         ArrayLit* vars = eval_array_lit(env, i2fc->arg(1));
46         std::vector<Expression*> n_vars_v(vars->size());
47         for (unsigned int i = 0; i < vars->size(); i++) {
48           Call* f2i =
49               new Call((*vars)[i]->loc().introduce(), constants().ids.int2float, {(*vars)[i]});
50           f2i->decl(env.model->matchFn(env, f2i, false));
51           assert(f2i->decl());
52           f2i->type(Type::varfloat());
53           EE ee = flat_exp(env, Ctx(), f2i, nullptr, constants().varTrue);
54           n_vars_v[i] = ee.r();
55         }
56         auto* nvars = new ArrayLit(vars->loc().introduce(), n_vars_v);
57         nvars->type(Type::varfloat(1));
58         FloatVal c = eval_int(env, i2fc->arg(2));
59         Call* nlinexp = new Call(i2fc->loc().introduce(), constants().ids.lin_exp,
60                                  {ncoeff, nvars, FloatLit::a(c)});
61         nlinexp->decl(env.model->matchFn(env, nlinexp, false));
62         assert(nlinexp->decl());
63         nlinexp->type(Type::varfloat());
64         return nlinexp;
65       }
66     }
67   }
68   return nullptr;
69 }
70 
71 class CmpExp {
72 public:
operator ()(const KeepAlive & i,const KeepAlive & j) const73   bool operator()(const KeepAlive& i, const KeepAlive& j) const {
74     if (Expression::equal(i(), j())) {
75       return false;
76     }
77     return i() < j();
78   }
79 };
80 
remove_dups(std::vector<KeepAlive> & x,bool identity)81 bool remove_dups(std::vector<KeepAlive>& x, bool identity) {
82   for (auto& i : x) {
83     i = follow_id_to_value(i());
84   }
85   std::sort(x.begin(), x.end(), CmpExp());
86   int ci = 0;
87   Expression* prev = nullptr;
88   for (unsigned int i = 0; i < x.size(); i++) {
89     if (!Expression::equal(x[i](), prev)) {
90       prev = x[i]();
91       if (x[i]()->isa<BoolLit>()) {
92         if (x[i]()->cast<BoolLit>()->v() == identity) {
93           // skip
94         } else {
95           return true;
96         }
97       } else {
98         x[ci++] = x[i];
99       }
100     }
101   }
102   x.resize(ci);
103   return false;
104 }
contains_dups(std::vector<KeepAlive> & x,std::vector<KeepAlive> & y)105 bool contains_dups(std::vector<KeepAlive>& x, std::vector<KeepAlive>& y) {
106   if (x.empty() || y.empty()) {
107     return false;
108   }
109   unsigned int ix = 0;
110   unsigned int iy = 0;
111   for (;;) {
112     if (x[ix]() == y[iy]()) {
113       return true;
114     }
115     if (x[ix]() < y[iy]()) {
116       ix++;
117     } else {
118       iy++;
119     }
120     if (ix == x.size() || iy == y.size()) {
121       return false;
122     }
123   }
124 }
125 
126 template <class Lit>
flatten_linexp_call(EnvI & env,Ctx ctx,const Ctx & nctx,ASTString & cid,Call * c,EE & ret,VarDecl * b,VarDecl * r,std::vector<EE> & args_ee,std::vector<KeepAlive> & args)127 void flatten_linexp_call(EnvI& env, Ctx ctx, const Ctx& nctx, ASTString& cid, Call* c, EE& ret,
128                          VarDecl* b, VarDecl* r, std::vector<EE>& args_ee,
129                          std::vector<KeepAlive>& args) {
130   typedef typename LinearTraits<Lit>::Val Val;
131   Expression* al_arg = (cid == constants().ids.sum ? args_ee[0].r() : args_ee[1].r());
132   EE flat_al = flat_exp(env, nctx, al_arg, nullptr, nullptr);
133   auto* al = follow_id(flat_al.r())->template cast<ArrayLit>();
134   KeepAlive al_ka = al;
135   if (al->dims() > 1) {
136     Type alt = al->type();
137     alt.dim(1);
138     GCLock lock;
139     al = new ArrayLit(al->loc(), *al);
140     al->type(alt);
141     al_ka = al;
142   }
143   Val d = (cid == constants().ids.sum ? Val(0) : LinearTraits<Lit>::eval(env, args_ee[2].r()));
144 
145   std::vector<Val> c_coeff(al->size());
146   if (cid == constants().ids.sum) {
147     for (unsigned int i = al->size(); i--;) {
148       c_coeff[i] = 1;
149     }
150   } else {
151     EE flat_coeff = flat_exp(env, nctx, args_ee[0].r(), nullptr, nullptr);
152     auto* coeff = follow_id(flat_coeff.r())->template cast<ArrayLit>();
153     for (unsigned int i = coeff->size(); i--;) {
154       c_coeff[i] = LinearTraits<Lit>::eval(env, (*coeff)[i]);
155     }
156   }
157   cid = constants().ids.lin_exp;
158   std::vector<Val> coeffv;
159   std::vector<KeepAlive> alv;
160   for (unsigned int i = 0; i < al->size(); i++) {
161     GCLock lock;
162     if (Call* sc = Expression::dynamicCast<Call>(same_call(env, (*al)[i], cid))) {
163       if (auto* alvi_decl = follow_id_to_decl((*al)[i])->template dynamicCast<VarDecl>()) {
164         if (alvi_decl->ti()->domain()) {
165           // Test if the variable has tighter declared bounds than what can be inferred
166           // from its RHS. If yes, keep the variable (don't aggregate), because the tighter
167           // bounds are actually a constraint
168           typename LinearTraits<Lit>::Domain sc_dom =
169               LinearTraits<Lit>::evalDomain(env, alvi_decl->ti()->domain());
170           typename LinearTraits<Lit>::Bounds sc_bounds = LinearTraits<Lit>::computeBounds(env, sc);
171           if (LinearTraits<Lit>::domainTighter(sc_dom, sc_bounds)) {
172             coeffv.push_back(c_coeff[i]);
173             alv.emplace_back((*al)[i]);
174             continue;
175           }
176         }
177       }
178 
179       Val cd = c_coeff[i];
180       ArrayLit* sc_coeff = eval_array_lit(env, sc->arg(0));
181       ArrayLit* sc_al = eval_array_lit(env, sc->arg(1));
182       Val sc_d = LinearTraits<Lit>::eval(env, sc->arg(2));
183       assert(sc_coeff->size() == sc_al->size());
184       for (unsigned int j = 0; j < sc_coeff->size(); j++) {
185         coeffv.push_back(cd * LinearTraits<Lit>::eval(env, (*sc_coeff)[j]));
186         alv.emplace_back((*sc_al)[j]);
187       }
188       d += cd * sc_d;
189     } else {
190       coeffv.push_back(c_coeff[i]);
191       alv.emplace_back((*al)[i]);
192     }
193   }
194   simplify_lin<Lit>(coeffv, alv, d);
195   if (coeffv.empty()) {
196     GCLock lock;
197     ret.b = conj(env, b, Ctx(), args_ee);
198     ret.r = bind(env, ctx, r, LinearTraits<Lit>::newLit(d));
199     return;
200   }
201   if (coeffv.size() == 1 && coeffv[0] == 1 && d == 0) {
202     ret.b = conj(env, b, Ctx(), args_ee);
203     ret.r = bind(env, ctx, r, alv[0]());
204     return;
205   }
206   GCLock lock;
207   std::vector<Expression*> coeff_ev(coeffv.size());
208   for (auto i = static_cast<unsigned int>(coeff_ev.size()); i--;) {
209     coeff_ev[i] = LinearTraits<Lit>::newLit(coeffv[i]);
210   }
211   auto* ncoeff = new ArrayLit(Location().introduce(), coeff_ev);
212   Type t = coeff_ev[0]->type();
213   t.dim(1);
214   ncoeff->type(t);
215   args.emplace_back(ncoeff);
216   std::vector<Expression*> alv_e(alv.size());
217   bool al_same_as_before = alv.size() == al->size();
218   for (auto i = static_cast<unsigned int>(alv.size()); i--;) {
219     alv_e[i] = alv[i]();
220     al_same_as_before = al_same_as_before && Expression::equal(alv_e[i], (*al)[i]);
221   }
222   if (al_same_as_before) {
223     Expression* rd = follow_id_to_decl(flat_al.r());
224     if (rd->isa<VarDecl>()) {
225       rd = rd->cast<VarDecl>()->id();
226     }
227     if (rd->type().dim() > 1) {
228       ArrayLit* al = eval_array_lit(env, rd);
229       std::vector<std::pair<int, int> > dims(1);
230       dims[0].first = 1;
231       dims[0].second = al->size();
232       rd = new ArrayLit(al->loc(), *al, dims);
233       Type t = al->type();
234       t.dim(1);
235       rd->type(t);
236     }
237     args.emplace_back(rd);
238   } else {
239     auto* nal = new ArrayLit(al->loc(), alv_e);
240     nal->type(al->type());
241     args.emplace_back(nal);
242   }
243   Lit* il = LinearTraits<Lit>::newLit(d);
244   args.push_back(il);
245 }
246 
247 /// Special form of disjunction for SCIP
is_totaladd_bounds_disj(EnvI & env,Expression * arg,Call * c_orig)248 bool is_totaladd_bounds_disj(EnvI& env, Expression* arg, Call* c_orig) {
249   auto* pArrayLit = arg->dynamicCast<ArrayLit>();
250   if (nullptr == pArrayLit) {
251     return false;
252   }
253   // integer bounds and vars
254   std::vector<Expression*> isUBI;
255   std::vector<Expression*> bndI;
256   std::vector<Expression*> varI;
257   // float bounds and vars
258   std::vector<Expression*> isUBF;
259   std::vector<Expression*> bndF;
260   std::vector<Expression*> varF;
261   for (unsigned int i = pArrayLit->size(); (i--) != 0U;) {
262     auto* pId = pArrayLit->operator[](i)->dynamicCast<Id>();
263     if (nullptr == pId) {
264       return false;
265     }
266     auto* pDecl = follow_id_to_decl(pId)->dynamicCast<VarDecl>();
267     /// Checking the rhs
268     auto* pRhs = pDecl->e();
269     if (nullptr == pRhs) {
270       return false;  // not checking this boolean
271     }
272     auto* pCall = pRhs->dynamicCast<Call>();
273     if (nullptr == pCall) {
274       return false;
275     }
276     if (constants().ids.int_.le != pCall->id() && constants().ids.float_.le != pCall->id()) {
277       return false;
278     }
279     /// See if one is a constant and one a variable
280     Expression* pConst = nullptr;
281     Expression* pVar = nullptr;
282     bool fFloat = false;
283     bool isUB = false;
284     for (unsigned int j = pCall->argCount(); (j--) != 0U;) {
285       if (auto* pF = pCall->arg(j)->dynamicCast<FloatLit>()) {
286         pConst = pF;
287         fFloat = true;
288         isUB = (1 == j);
289       } else if (auto* pF = pCall->arg(j)->dynamicCast<IntLit>()) {
290         pConst = pF;
291         fFloat = false;
292         isUB = (1 == j);
293       } else if (auto* pId = pCall->arg(j)->dynamicCast<Id>()) {
294         if (nullptr != pVar) {
295           return false;  // 2 variables, exit
296         }
297         pVar = pId;
298       }
299     }
300     /// All good, add them
301     if (fFloat) {
302       isUBF.push_back(constants().boollit(isUB));
303       bndF.push_back(pConst);
304       varF.push_back(pVar);
305     } else {
306       isUBI.push_back(constants().boollit(isUB));
307       bndI.push_back(pConst);
308       varI.push_back(pVar);
309     }
310   }
311   /// Create new call
312   GCLock lock;
313   auto loc = c_orig->loc().introduce();
314   std::vector<Expression*> args = {new ArrayLit(loc, isUBI), new ArrayLit(loc, bndI),
315                                    new ArrayLit(loc, varI),  new ArrayLit(loc, isUBF),
316                                    new ArrayLit(loc, bndF),  new ArrayLit(loc, varF)};
317 
318   Call* c =
319       new Call(c_orig->loc().introduce(), env.model->getFnDecls().boundsDisj.second->id(), args);
320   c->type(Type::varbool());
321   c->decl(env.model->getFnDecls().boundsDisj.second);
322   env.flatAddItem(new ConstraintI(c_orig->loc().introduce(), c));
323   return true;
324 }
325 
326 class IgnorePartial {
327 public:
328   EnvI& env;
329   bool ignorePartial;
IgnorePartial(EnvI & env0,Call * c)330   IgnorePartial(EnvI& env0, Call* c) : env(env0), ignorePartial(env.ignorePartial) {
331     if (c->id().endsWith("_reif") || c->id().endsWith("_imp")) {
332       env.ignorePartial = true;
333     }
334   }
~IgnorePartial()335   ~IgnorePartial() { env.ignorePartial = ignorePartial; }
336 };
337 
338 // NOLINTNEXTLINE(readability-function-size): TODO??
flatten_call(EnvI & env,const Ctx & input_ctx,Expression * e,VarDecl * r,VarDecl * b)339 EE flatten_call(EnvI& env, const Ctx& input_ctx, Expression* e, VarDecl* r, VarDecl* b) {
340   EE ret;
341   Call* c = e->cast<Call>();
342   IgnorePartial ignorePartial(env, c);
343   if (c->id().endsWith("_reif")) {
344     env.counters.reifConstraints++;
345   } else if (c->id().endsWith("_imp")) {
346     env.counters.impConstraints++;
347   }
348   FunctionI* decl = env.model->matchFn(env, c, false);
349   if (decl == nullptr) {
350     std::ostringstream ss;
351     ss << "undeclared function or predicate " << c->id();
352     throw InternalError(ss.str());
353   }
354 
355   Ctx ctx = input_ctx;
356   Ctx nctx = ctx;
357   nctx.neg = false;
358   ASTString cid = c->id();
359   CallStackItem _csi(env, e);
360 
361   if (cid == constants().ids.bool2int && c->type().dim() == 0) {
362     if (ctx.neg) {
363       ctx.neg = false;
364       nctx.neg = true;
365       nctx.b = -ctx.i;
366     } else {
367       nctx.b = ctx.i;
368     }
369   } else if (cid == constants().ids.forall) {
370     nctx.b = +nctx.b;
371     if (ctx.neg) {
372       ctx.neg = false;
373       nctx.neg = true;
374       cid = constants().ids.exists;
375     }
376   } else if (cid == constants().ids.exists) {
377     nctx.b = +nctx.b;
378     if (ctx.neg) {
379       ctx.neg = false;
380       nctx.neg = true;
381       cid = constants().ids.forall;
382     }
383   } else if (decl->e() == nullptr &&
384              (cid == constants().ids.assert || cid == constants().ids.trace ||
385               cid == constants().ids.mzn_symmetry_breaking_constraint ||
386               cid == constants().ids.mzn_redundant_constraint ||
387               cid == constants().ids.mzn_deprecate)) {
388     if (cid == constants().ids.assert && c->argCount() == 2) {
389       (void)decl->builtins.b(env, c);
390       ret = flat_exp(env, ctx, constants().literalTrue, r, b);
391     } else {
392       KeepAlive callres = decl->builtins.e(env, c);
393       ret = flat_exp(env, ctx, callres(), r, b);
394       // This is all we need to do for assert, so break out of the E_CALL
395     }
396     return ret;
397   } else if ((decl->e() != nullptr) && ctx.b == C_ROOT && decl->e()->isa<BoolLit>() &&
398              eval_bool(env, decl->e())) {
399     bool allBool = true;
400     for (unsigned int i = 0; i < c->argCount(); i++) {
401       if (c->arg(i)->type().bt() != Type::BT_BOOL) {
402         allBool = false;
403         break;
404       }
405     }
406     if (allBool) {
407       ret.r = bind(env, ctx, r, constants().literalTrue);
408       ret.b = bind(env, ctx, b, constants().literalTrue);
409       return ret;
410     }
411   }
412 
413   if (ctx.b == C_ROOT && decl->e() == nullptr && cid == constants().ids.forall &&
414       r == constants().varTrue) {
415     ret.b = bind(env, ctx, b, constants().literalTrue);
416     ArrayLit* al;
417     if (c->arg(0)->isa<ArrayLit>()) {
418       al = c->arg(0)->cast<ArrayLit>();
419     } else {
420       EE flat_al = flat_exp(env, Ctx(), c->arg(0), constants().varIgnore, constants().varTrue);
421       al = follow_id(flat_al.r())->cast<ArrayLit>();
422     }
423     nctx.b = C_ROOT;
424     for (unsigned int i = 0; i < al->size(); i++) {
425       (void)flat_exp(env, nctx, (*al)[i], r, b);
426     }
427     ret.r = bind(env, ctx, r, constants().literalTrue);
428   } else {
429     if ((decl->e() != nullptr) && decl->params().size() == 1 && decl->e()->isa<Id>() &&
430         decl->params()[0]->ti()->domain() == nullptr &&
431         decl->e()->cast<Id>()->decl() == decl->params()[0]) {
432       Expression* arg = c->arg(0);
433       for (ExpressionSetIter esi = decl->e()->ann().begin(); esi != decl->e()->ann().end(); ++esi) {
434         arg->addAnnotation(*esi);
435       }
436       for (ExpressionSetIter esi = c->ann().begin(); esi != c->ann().end(); ++esi) {
437         arg->addAnnotation(*esi);
438       }
439       ret = flat_exp(env, ctx, c->arg(0), r, b);
440       return ret;
441     }
442 
443     std::vector<EE> args_ee(c->argCount());
444     bool isPartial = false;
445 
446     if (cid == constants().ids.lin_exp && c->type().isint()) {
447       // Linear expressions need special context handling:
448       // the context of a variable expression depends on the corresponding coefficient
449 
450       // flatten the coefficient array
451       Expression* tmp = follow_id_to_decl(c->arg(0));
452       ArrayLit* coeffs;
453       if (auto* vd = tmp->dynamicCast<VarDecl>()) {
454         tmp = vd->id();
455       }
456       {
457         CallArgItem cai(env);
458         args_ee[0] = flat_exp(env, nctx, tmp, nullptr, nullptr);
459         isPartial |= isfalse(env, args_ee[0].b());
460         coeffs = eval_array_lit(env, args_ee[0].r());
461       }
462 
463       ArrayLit* vars = eval_array_lit(env, c->arg(1));
464       if (vars->flat()) {
465         args_ee[1].r = vars;
466         args_ee[1].b = constants().varTrue;
467       } else {
468         CallArgItem cai(env);
469         CallStackItem _csi(env, c->arg(1));
470         std::vector<EE> elems_ee(vars->size());
471         for (unsigned int i = vars->size(); (i--) != 0U;) {
472           Ctx argctx = nctx;
473           argctx.i = eval_int(env, (*coeffs)[i]) < 0 ? -nctx.i : +nctx.i;
474           elems_ee[i] = flat_exp(env, argctx, (*vars)[i], nullptr, nullptr);
475         }
476         std::vector<Expression*> elems(elems_ee.size());
477         for (auto i = static_cast<unsigned int>(elems.size()); (i--) != 0U;) {
478           elems[i] = elems_ee[i].r();
479         }
480         KeepAlive ka;
481         {
482           GCLock lock;
483           auto* alr = new ArrayLit(Location().introduce(), elems);
484           alr->type(vars->type());
485           alr->flat(true);
486           ka = alr;
487         }
488         args_ee[1].r = ka();
489         args_ee[1].b = conj(env, b, Ctx(), elems_ee);
490       }
491 
492       {
493         Expression* constant = follow_id_to_decl(c->arg(2));
494         if (auto* vd = constant->dynamicCast<VarDecl>()) {
495           constant = vd->id();
496         }
497         CallArgItem cai(env);
498         args_ee[2] = flat_exp(env, nctx, constant, nullptr, nullptr);
499         isPartial |= isfalse(env, args_ee[2].b());
500       }
501 
502     } else {
503       bool mixContext =
504           (cid != constants().ids.forall && cid != constants().ids.exists &&
505            (cid != constants().ids.bool2int || c->type().dim() > 0) && cid != constants().ids.sum &&
506            cid != "assert" && cid != constants().varRedef->id() && cid != "mzn_reverse_map_var");
507       if (cid == "mzn_reverse_map_var") {
508         env.inReverseMapVar = true;
509       }
510       if (cid == constants().ids.clause && c->arg(0)->isa<ArrayLit>() &&
511           c->arg(1)->isa<ArrayLit>()) {
512         Ctx argctx = nctx;
513 
514         // handle negated args first, try to make them positive
515 
516         if (mixContext) {
517           argctx.b = -nctx.b;
518         }
519         std::vector<KeepAlive> neg_args;
520         std::vector<KeepAlive> pos_args;
521         std::vector<KeepAlive> newPositives;
522         bool is_subsumed = false;
523         auto* al_neg = c->arg(1)->cast<ArrayLit>();
524         {
525           CallArgItem cai(env);
526           for (unsigned int i = 0; i < al_neg->size(); i++) {
527             auto* bo = (*al_neg)[i]->dynamicCast<BinOp>();
528             Call* co = (*al_neg)[i]->dynamicCast<Call>();
529             if ((bo != nullptr) || ((co != nullptr) && (co->id() == constants().ids.forall ||
530                                                         co->id() == constants().ids.exists ||
531                                                         co->id() == constants().ids.clause))) {
532               GCLock lock;
533               UnOp* notBoe0 = new UnOp(Location().introduce(), UOT_NOT, (*al_neg)[i]);
534               notBoe0->type(Type::varbool());
535               newPositives.emplace_back(notBoe0);
536             } else {
537               EE res = flat_exp(env, argctx, (*al_neg)[i], nullptr, constants().varTrue);
538               if (res.r()->type().isPar()) {
539                 if (eval_bool(env, res.r())) {
540                   // this element is irrelevant
541                 } else {
542                   // this element subsumes all other elements
543                   neg_args = {res.r()};
544                   pos_args = {};
545                   is_subsumed = true;
546                   break;
547                 }
548               } else {
549                 neg_args.emplace_back(res.r());
550               }
551             }
552           }
553         }
554 
555         // Now process new and previous positive arguments
556         if (mixContext) {
557           argctx.b = +nctx.b;
558         }
559         auto* al_pos = c->arg(0)->cast<ArrayLit>();
560         for (unsigned int i = 0; i < al_pos->size(); i++) {
561           newPositives.emplace_back((*al_pos)[i]);
562         }
563         {
564           CallArgItem cai(env);
565           for (auto& newPositive : newPositives) {
566             EE res = flat_exp(env, argctx, newPositive(), nullptr, constants().varTrue);
567             if (res.r()->type().isPar()) {
568               if (!eval_bool(env, res.r())) {
569                 // this element is irrelevant
570               } else {
571                 // this element subsumes all other elements
572                 pos_args = {res.r()};
573                 neg_args = {};
574                 is_subsumed = true;
575                 break;
576               }
577             } else {
578               pos_args.emplace_back(res.r());
579             }
580           }
581         }
582 
583         GCLock lock;
584         auto* al_new_pos = new ArrayLit(al_pos->loc(), to_exp_vec(pos_args));
585         al_new_pos->type(Type::varbool(1));
586         al_new_pos->flat(true);
587         args_ee[0] = EE(al_new_pos, constants().literalTrue);
588         auto* al_new_neg = new ArrayLit(al_neg->loc(), to_exp_vec(neg_args));
589         al_new_neg->flat(true);
590         al_new_neg->type(Type::varbool(1));
591         args_ee[1] = EE(al_new_neg, constants().literalTrue);
592       } else if ((cid == constants().ids.forall || cid == constants().ids.exists) &&
593                  c->arg(0)->isa<ArrayLit>()) {
594         bool is_conj = (cid == constants().ids.forall);
595         Ctx argctx = nctx;
596         if (mixContext) {
597           argctx.b = C_MIX;
598         }
599         auto* al = c->arg(0)->cast<ArrayLit>();
600         ArrayLit* al_new;
601         if (al->flat()) {
602           al_new = al;
603         } else {
604           std::vector<KeepAlive> flat_args;
605           CallArgItem cai(env);
606           for (unsigned int i = 0; i < al->size(); i++) {
607             EE res = flat_exp(env, argctx, (*al)[i], nullptr, constants().varTrue);
608             if (res.r()->type().isPar()) {
609               if (eval_bool(env, res.r()) == is_conj) {
610                 // this element is irrelevant
611               } else {
612                 // this element subsumes all other elements
613                 flat_args = {res.r()};
614                 break;
615               }
616             } else {
617               flat_args.emplace_back(res.r());
618             }
619           }
620           GCLock lock;
621           al_new = new ArrayLit(al->loc(), to_exp_vec(flat_args));
622           al_new->type(Type::varbool(1));
623           al_new->flat(true);
624         }
625         args_ee[0] = EE(al_new, constants().literalTrue);
626       } else {
627         for (unsigned int i = c->argCount(); (i--) != 0U;) {
628           Ctx argctx = nctx;
629           if (mixContext) {
630             if (cid == constants().ids.clause) {
631               argctx.b = (i == 0 ? +nctx.b : -nctx.b);
632             } else if (c->arg(i)->type().bt() == Type::BT_BOOL) {
633               argctx.b = C_MIX;
634             } else if (c->arg(i)->type().bt() == Type::BT_INT) {
635               argctx.i = C_MIX;
636             }
637           } else if (cid == constants().ids.sum && c->arg(i)->type().bt() == Type::BT_BOOL) {
638             argctx.b = argctx.i;
639           }
640           Expression* tmp = follow_id_to_decl(c->arg(i));
641           if (auto* vd = tmp->dynamicCast<VarDecl>()) {
642             tmp = vd->id();
643           }
644           CallArgItem cai(env);
645           args_ee[i] = flat_exp(env, argctx, tmp, nullptr, nullptr);
646           isPartial |= isfalse(env, args_ee[i].b());
647         }
648       }
649     }
650     if (isPartial && c->type().isbool() && !c->type().isOpt()) {
651       ret.b = bind(env, Ctx(), b, constants().literalTrue);
652       args_ee.resize(1);
653       args_ee[0] = EE(nullptr, constants().literalFalse);
654       ret.r = conj(env, r, ctx, args_ee);
655       return ret;
656     }
657 
658     std::vector<KeepAlive> args;
659     if (decl->e() == nullptr && (cid == constants().ids.exists || cid == constants().ids.clause)) {
660       std::vector<KeepAlive> pos_alv;
661       std::vector<KeepAlive> neg_alv;
662 
663       std::vector<Expression*> pos_stack;
664       std::vector<Expression*> neg_stack;
665 
666       auto* al_pos = follow_id(args_ee[0].r())->cast<ArrayLit>();
667       for (unsigned int i = 0; i < al_pos->size(); i++) {
668         pos_stack.push_back((*al_pos)[i]);
669       }
670       if (cid == constants().ids.clause) {
671         auto* al_neg = follow_id(args_ee[1].r())->cast<ArrayLit>();
672         for (unsigned int i = 0; i < al_neg->size(); i++) {
673           neg_stack.push_back((*al_neg)[i]);
674         }
675       }
676 
677       std::unordered_set<Expression*> seen;
678 
679       while (!pos_stack.empty() || !neg_stack.empty()) {
680         while (!pos_stack.empty()) {
681           Expression* cur = pos_stack.back();
682           pos_stack.pop_back();
683           if (cur->isa<Id>() && seen.find(cur) != seen.end()) {
684             pos_alv.emplace_back(cur);
685           } else {
686             seen.insert(cur);
687             GCLock lock;
688             if (Call* sc =
689                     Expression::dynamicCast<Call>(same_call(env, cur, constants().ids.exists))) {
690               GCLock lock;
691               ArrayLit* sc_c = eval_array_lit(env, sc->arg(0));
692               for (unsigned int j = 0; j < sc_c->size(); j++) {
693                 pos_stack.push_back((*sc_c)[j]);
694               }
695             } else if (Call* sc = Expression::dynamicCast<Call>(
696                            same_call(env, cur, constants().ids.clause))) {
697               GCLock lock;
698               ArrayLit* sc_c = eval_array_lit(env, sc->arg(0));
699               for (unsigned int j = 0; j < sc_c->size(); j++) {
700                 pos_stack.push_back((*sc_c)[j]);
701               }
702               sc_c = eval_array_lit(env, sc->arg(1));
703               for (unsigned int j = 0; j < sc_c->size(); j++) {
704                 neg_stack.push_back((*sc_c)[j]);
705               }
706             } else {
707               Call* eq_call =
708                   Expression::dynamicCast<Call>(same_call(env, cur, constants().ids.bool_eq));
709               Call* not_call =
710                   Expression::dynamicCast<Call>(same_call(env, cur, constants().ids.bool_not));
711               if ((eq_call != nullptr) &&
712                   Expression::equal(eq_call->arg(1), constants().literalFalse)) {
713                 neg_stack.push_back(eq_call->arg(0));
714               } else if ((eq_call != nullptr) &&
715                          Expression::equal(eq_call->arg(0), constants().literalFalse)) {
716                 neg_stack.push_back(eq_call->arg(1));
717               } else if ((eq_call != nullptr) &&
718                          Expression::equal(eq_call->arg(1), constants().literalTrue)) {
719                 pos_stack.push_back(eq_call->arg(0));
720               } else if ((eq_call != nullptr) &&
721                          Expression::equal(eq_call->arg(0), constants().literalTrue)) {
722                 pos_stack.push_back(eq_call->arg(1));
723               } else if ((not_call != nullptr) && not_call->argCount() == 1) {
724                 neg_stack.push_back(not_call->arg(0));
725               } else if (Id* ident = cur->dynamicCast<Id>()) {
726                 if (ident->decl()->ti()->domain() != constants().literalFalse) {
727                   pos_alv.emplace_back(ident);
728                 }
729               } else {
730                 pos_alv.emplace_back(cur);
731               }
732             }
733           }
734         }
735 
736         while (!neg_stack.empty()) {
737           GCLock lock;
738           Expression* cur = neg_stack.back();
739           neg_stack.pop_back();
740           if (cur->isa<Id>() && seen.find(cur) != seen.end()) {
741             neg_alv.emplace_back(cur);
742           } else {
743             seen.insert(cur);
744             if (Call* sc =
745                     Expression::dynamicCast<Call>(same_call(env, cur, constants().ids.forall))) {
746               GCLock lock;
747               ArrayLit* sc_c = eval_array_lit(env, sc->arg(0));
748               for (unsigned int j = 0; j < sc_c->size(); j++) {
749                 neg_stack.push_back((*sc_c)[j]);
750               }
751             } else {
752               Call* eq_call =
753                   Expression::dynamicCast<Call>(same_call(env, cur, constants().ids.bool_eq));
754               Call* not_call =
755                   Expression::dynamicCast<Call>(same_call(env, cur, constants().ids.bool_not));
756               if ((eq_call != nullptr) &&
757                   Expression::equal(eq_call->arg(1), constants().literalFalse)) {
758                 pos_stack.push_back(eq_call->arg(0));
759               } else if ((eq_call != nullptr) &&
760                          Expression::equal(eq_call->arg(0), constants().literalFalse)) {
761                 pos_stack.push_back(eq_call->arg(1));
762               } else if ((eq_call != nullptr) &&
763                          Expression::equal(eq_call->arg(1), constants().literalTrue)) {
764                 neg_stack.push_back(eq_call->arg(0));
765               } else if ((eq_call != nullptr) &&
766                          Expression::equal(eq_call->arg(0), constants().literalTrue)) {
767                 neg_stack.push_back(eq_call->arg(1));
768               } else if ((not_call != nullptr) && not_call->argCount() == 1) {
769                 pos_stack.push_back(not_call->arg(0));
770               } else if (Id* ident = cur->dynamicCast<Id>()) {
771                 if (ident->decl()->ti()->domain() != constants().literalTrue) {
772                   neg_alv.emplace_back(ident);
773                 }
774               } else {
775                 neg_alv.emplace_back(cur);
776               }
777             }
778           }
779         }
780       }
781 
782       bool subsumed = remove_dups(pos_alv, false);
783       subsumed = subsumed || remove_dups(neg_alv, true);
784       subsumed = subsumed || contains_dups(pos_alv, neg_alv);
785       if (subsumed) {
786         ret.b = bind(env, Ctx(), b, constants().literalTrue);
787         ret.r = bind(env, ctx, r, constants().literalTrue);
788         return ret;
789       }
790       if (neg_alv.empty()) {
791         if (pos_alv.empty()) {
792           ret.b = bind(env, Ctx(), b, constants().literalTrue);
793           ret.r = bind(env, ctx, r, constants().literalFalse);
794           return ret;
795         }
796         if (pos_alv.size() == 1) {
797           ret.b = bind(env, Ctx(), b, constants().literalTrue);
798           ret.r = bind(env, ctx, r, pos_alv[0]());
799           return ret;
800         }
801         GCLock lock;
802         auto* nal = new ArrayLit(Location().introduce(), to_exp_vec(pos_alv));
803         nal->type(Type::varbool(1));
804         args.emplace_back(nal);
805         cid = constants().ids.exists;
806       } else {
807         if (pos_alv.empty() && neg_alv.size() == 1) {
808           ret.b = bind(env, Ctx(), b, constants().literalTrue);
809           Ctx nctx = ctx;
810           nctx.neg = !nctx.neg;
811           nctx.b = -nctx.b;
812           ret.r = bind(env, nctx, r, neg_alv[0]());
813           return ret;
814         }
815         GCLock lock;
816         auto* pos_al = new ArrayLit(Location().introduce(), to_exp_vec(pos_alv));
817         pos_al->type(Type::varbool(1));
818         auto* neg_al = new ArrayLit(Location().introduce(), to_exp_vec(neg_alv));
819         neg_al->type(Type::varbool(1));
820         cid = constants().ids.clause;
821         args.emplace_back(pos_al);
822         args.emplace_back(neg_al);
823       }
824       if (C_ROOT == ctx.b && cid == constants().ids.exists) {
825         /// Check the special bounds disjunction for SCIP
826         /// Only in root context
827         if (!env.model->getFnDecls().boundsDisj.first) {
828           env.model->getFnDecls().boundsDisj.first = true;
829           std::vector<Type> bj_t = {Type::parbool(1), Type::parint(1),   Type::varint(1),
830                                     Type::parbool(1), Type::parfloat(1), Type::varfloat(1)};
831           GCLock lock;
832           env.model->getFnDecls().boundsDisj.second =
833               env.model->matchFn(env, ASTString("bounds_disj"), bj_t, false);
834         }
835         /// When the SCIP predicate is declared only
836         bool fBoundsDisj_Maybe = (nullptr != env.model->getFnDecls().boundsDisj.second);
837         if (fBoundsDisj_Maybe) {
838           if (is_totaladd_bounds_disj(env, args[0](), c)) {
839             ret.b = bind(env, Ctx(), b, constants().literalTrue);
840             ret.r = bind(env, ctx, r, constants().literalTrue);
841             return ret;
842           }
843         }
844       }
845 
846     } else if (decl->e() == nullptr && cid == constants().ids.forall) {
847       auto* al = follow_id(args_ee[0].r())->cast<ArrayLit>();
848       std::vector<KeepAlive> alv;
849       for (unsigned int i = 0; i < al->size(); i++) {
850         GCLock lock;
851         if (Call* sc = Expression::dynamicCast<Call>(same_call(env, (*al)[i], cid))) {
852           GCLock lock;
853           ArrayLit* sc_c = eval_array_lit(env, sc->arg(0));
854           for (unsigned int j = 0; j < sc_c->size(); j++) {
855             alv.emplace_back((*sc_c)[j]);
856           }
857         } else {
858           alv.emplace_back((*al)[i]);
859         }
860       }
861       bool subsumed = remove_dups(alv, true);
862       if (subsumed) {
863         ret.b = bind(env, Ctx(), b, constants().literalTrue);
864         ret.r = bind(env, ctx, r, constants().literalFalse);
865         return ret;
866       }
867       if (alv.empty()) {
868         ret.b = bind(env, Ctx(), b, constants().literalTrue);
869         ret.r = bind(env, ctx, r, constants().literalTrue);
870         return ret;
871       }
872       if (alv.size() == 1) {
873         ret.b = bind(env, Ctx(), b, constants().literalTrue);
874         ret.r = bind(env, ctx, r, alv[0]());
875         return ret;
876       }
877       GCLock lock;
878       auto* nal = new ArrayLit(al->loc(), to_exp_vec(alv));
879       nal->type(al->type());
880       args.emplace_back(nal);
881     } else if (decl->e() == nullptr &&
882                (cid == constants().ids.lin_exp || cid == constants().ids.sum)) {
883       if (e->type().isint()) {
884         flatten_linexp_call<IntLit>(env, ctx, nctx, cid, c, ret, b, r, args_ee, args);
885       } else {
886         flatten_linexp_call<FloatLit>(env, ctx, nctx, cid, c, ret, b, r, args_ee, args);
887       }
888       if (args.empty()) {
889         return ret;
890       }
891     } else {
892       for (auto& i : args_ee) {
893         args.emplace_back(i.r());
894       }
895     }
896     bool hadImplementation = (decl->e() != nullptr);
897     KeepAlive cr;
898     {
899       GCLock lock;
900       std::vector<Expression*> e_args = to_exp_vec(args);
901       Call* cr_c = new Call(c->loc().introduce(), cid, e_args);
902       decl = env.model->matchFn(env, cr_c, false);
903       if (decl == nullptr) {
904         throw FlatteningError(env, cr_c->loc(), "cannot find matching declaration");
905       }
906       cr_c->type(decl->rtype(env, e_args, false));
907       assert(decl);
908       cr_c->decl(decl);
909       cr = cr_c;
910     }
911     if (hadImplementation && decl->e() == nullptr &&
912         (cid == constants().ids.lin_exp || cid == constants().ids.sum)) {
913       args.clear();
914       if (e->type().isint()) {
915         flatten_linexp_call<IntLit>(env, ctx, nctx, cid, cr()->cast<Call>(), ret, b, r, args_ee,
916                                     args);
917       } else {
918         flatten_linexp_call<FloatLit>(env, ctx, nctx, cid, cr()->cast<Call>(), ret, b, r, args_ee,
919                                       args);
920       }
921       if (args.empty()) {
922         return ret;
923       }
924       GCLock lock;
925       std::vector<Expression*> e_args = to_exp_vec(args);
926       Call* cr_c = new Call(c->loc().introduce(), cid, e_args);
927       decl = env.model->matchFn(env, cr_c, false);
928       if (decl == nullptr) {
929         throw FlatteningError(env, cr_c->loc(), "cannot find matching declaration");
930       }
931       cr_c->type(decl->rtype(env, e_args, false));
932       assert(decl);
933       cr_c->decl(decl);
934       cr = cr_c;
935     }
936     auto cit = env.cseMapFind(cr());
937     if (cit != env.cseMapEnd()) {
938       if (env.ignorePartial) {
939         ret.b = bind(env, Ctx(), b, constants().literalTrue);
940       } else {
941         args_ee.emplace_back(nullptr, cit->second.b());
942         ret.b = conj(env, b, Ctx(), args_ee);
943       }
944       ret.r = bind(env, ctx, r, cit->second.r());
945     } else {
946       for (unsigned int i = 0; i < decl->params().size(); i++) {
947         if (decl->params()[i]->type().dim() > 0) {
948           // Check array index sets
949           auto* al = follow_id(args[i]())->cast<ArrayLit>();
950           VarDecl* pi = decl->params()[i];
951           for (unsigned int j = 0; j < pi->ti()->ranges().size(); j++) {
952             TypeInst* range_ti = pi->ti()->ranges()[j];
953             if ((range_ti->domain() != nullptr) && !range_ti->domain()->isa<TIId>()) {
954               GCLock lock;
955               IntSetVal* isv = eval_intset(env, range_ti->domain());
956               if (isv->min() != al->min(j) || isv->max() != al->max(j)) {
957                 std::ostringstream oss;
958                 oss << "array index set " << (j + 1) << " of argument " << (i + 1)
959                     << " does not match declared index set";
960                 throw FlatteningError(env, e->loc(), oss.str());
961               }
962             }
963           }
964         }
965         if (Expression* dom = decl->params()[i]->ti()->domain()) {
966           if (!dom->isa<TIId>()) {
967             // May have to constrain actual argument
968             if (args[i]()->type().bt() == Type::BT_INT) {
969               GCLock lock;
970               IntSetVal* isv = eval_intset(env, dom);
971               BinOpType bot;
972               bool needToConstrain;
973               if (args[i]()->type().st() == Type::ST_SET) {
974                 bot = BOT_SUBSET;
975                 needToConstrain = true;
976               } else {
977                 bot = BOT_IN;
978                 if (args[i]()->type().dim() > 0) {
979                   needToConstrain = true;
980                 } else {
981                   IntBounds ib = compute_int_bounds(env, args[i]());
982                   needToConstrain = !ib.valid || isv->size() == 0 || ib.l < isv->min(0) ||
983                                     ib.u > isv->max(isv->size() - 1);
984                 }
985               }
986               if (needToConstrain) {
987                 GCLock lock;
988                 Expression* domconstraint;
989                 if (args[i]()->type().dim() > 0) {
990                   std::vector<Expression*> domargs(2);
991                   domargs[0] = args[i]();
992                   domargs[1] = dom;
993                   Call* c = new Call(Location().introduce(), "var_dom", domargs);
994                   c->type(Type::varbool());
995                   c->decl(env.model->matchFn(env, c, false));
996                   if (c->decl() == nullptr) {
997                     throw InternalError("no matching declaration found for var_dom");
998                   }
999                   domconstraint = c;
1000                 } else {
1001                   domconstraint = new BinOp(Location().introduce(), args[i](), bot, dom);
1002                 }
1003                 domconstraint->type(args[i]()->type().isPar() ? Type::parbool() : Type::varbool());
1004                 if (ctx.b == C_ROOT) {
1005                   (void)flat_exp(env, Ctx(), domconstraint, constants().varTrue,
1006                                  constants().varTrue);
1007                 } else {
1008                   EE ee = flat_exp(env, Ctx(), domconstraint, nullptr, constants().varTrue);
1009                   ee.b = ee.r;
1010                   args_ee.push_back(ee);
1011                 }
1012               }
1013             } else if (args[i]()->type().bt() == Type::BT_FLOAT) {
1014               GCLock lock;
1015 
1016               FloatSetVal* fsv = eval_floatset(env, dom);
1017               bool needToConstrain;
1018               if (args[i]()->type().dim() > 0) {
1019                 needToConstrain = true;
1020               } else {
1021                 FloatBounds fb = compute_float_bounds(env, args[i]());
1022                 needToConstrain = !fb.valid || fsv->size() == 0 || fb.l < fsv->min(0) ||
1023                                   fb.u > fsv->max(fsv->size() - 1);
1024               }
1025 
1026               if (needToConstrain) {
1027                 GCLock lock;
1028                 Expression* domconstraint;
1029                 if (args[i]()->type().dim() > 0) {
1030                   std::vector<Expression*> domargs(2);
1031                   domargs[0] = args[i]();
1032                   domargs[1] = dom;
1033                   Call* c = new Call(Location().introduce(), "var_dom", domargs);
1034                   c->type(Type::varbool());
1035                   c->decl(env.model->matchFn(env, c, false));
1036                   if (c->decl() == nullptr) {
1037                     throw InternalError("no matching declaration found for var_dom");
1038                   }
1039                   domconstraint = c;
1040                 } else {
1041                   domconstraint = new BinOp(Location().introduce(), args[i](), BOT_IN, dom);
1042                 }
1043                 domconstraint->type(args[i]()->type().isPar() ? Type::parbool() : Type::varbool());
1044                 if (ctx.b == C_ROOT) {
1045                   (void)flat_exp(env, Ctx(), domconstraint, constants().varTrue,
1046                                  constants().varTrue);
1047                 } else {
1048                   EE ee = flat_exp(env, Ctx(), domconstraint, nullptr, constants().varTrue);
1049                   ee.b = ee.r;
1050                   args_ee.push_back(ee);
1051                 }
1052               }
1053             } else if (args[i]()->type().bt() == Type::BT_BOT) {
1054               // Nothing to be done for empty arrays/sets
1055             } else {
1056               throw EvalError(env, decl->params()[i]->loc(),
1057                               "domain restrictions other than int and float not supported yet");
1058             }
1059           }
1060         }
1061       }
1062       if (cr()->type().isbool() && !cr()->type().isPar() && !cr()->type().isOpt() &&
1063           (ctx.b != C_ROOT || r != constants().varTrue)) {
1064         std::vector<Type> argtypes(args.size());
1065         for (unsigned int i = 0; i < args.size(); i++) {
1066           argtypes[i] = args[i]()->type();
1067         }
1068         argtypes.push_back(Type::varbool());
1069         GCLock lock;
1070         ASTString r_cid = env.reifyId(cid);
1071         FunctionI* reif_decl = env.model->matchFn(env, r_cid, argtypes, false);
1072         if ((reif_decl != nullptr) && (reif_decl->e() != nullptr)) {
1073           add_path_annotation(env, reif_decl->e());
1074           VarDecl* reif_b;
1075           if (r == nullptr || (r != nullptr && r->e() != nullptr)) {
1076             reif_b = new_vardecl(env, Ctx(), new TypeInst(Location().introduce(), Type::varbool()),
1077                                  nullptr, nullptr, nullptr);
1078             add_ctx_ann(reif_b, ctx.b);
1079             if (reif_b->ti()->domain() != nullptr) {
1080               if (reif_b->ti()->domain() == constants().literalTrue) {
1081                 bind(env, ctx, r, constants().literalTrue);
1082                 r = constants().varTrue;
1083                 ctx.b = C_ROOT;
1084                 goto call_nonreif;
1085               } else {
1086                 std::vector<Expression*> args_e(args.size() + 1);
1087                 for (unsigned int i = 0; i < args.size(); i++) {
1088                   args_e[i] = args[i]();
1089                 }
1090                 args_e[args.size()] = constants().literalFalse;
1091                 Call* reif_call = new Call(Location().introduce(), r_cid, args_e);
1092                 reif_call->type(Type::varbool());
1093                 reif_call->decl(reif_decl);
1094                 flat_exp(env, Ctx(), reif_call, constants().varTrue, constants().varTrue);
1095                 args_ee.emplace_back(nullptr, constants().literalFalse);
1096                 ret.r = conj(env, r, ctx, args_ee);
1097                 ret.b = bind(env, ctx, b, constants().literalTrue);
1098                 return ret;
1099               }
1100             }
1101           } else {
1102             reif_b = r;
1103           }
1104           // Annotate cr() with get_path()
1105           add_path_annotation(env, cr());
1106           reif_b->e(cr());
1107           if (r != nullptr && r->e() != nullptr) {
1108             Ctx reif_ctx;
1109             reif_ctx.neg = ctx.neg;
1110             bind(env, reif_ctx, r, reif_b->id());
1111           }
1112           env.voAddExp(reif_b);
1113           ret.b = bind(env, Ctx(), b, constants().literalTrue);
1114           args_ee.emplace_back(nullptr, reif_b->id());
1115           ret.r = conj(env, nullptr, ctx, args_ee);
1116           if (!ctx.neg && !cr()->type().isAnn()) {
1117             env.cseMapInsert(cr(), ret);
1118           }
1119           return ret;
1120         }
1121       }
1122     call_nonreif:
1123       if (decl->e() == nullptr ||
1124           (cr()->type().isPar() && !cr()->type().isAnn() && !decl->e()->type().cv())) {
1125         Call* cr_c = cr()->cast<Call>();
1126         /// All builtins are total
1127         std::vector<Type> argt(cr_c->argCount());
1128         for (auto i = static_cast<unsigned int>(argt.size()); (i--) != 0U;) {
1129           argt[i] = cr_c->arg(i)->type();
1130         }
1131         Type callt = decl->rtype(env, argt, false);
1132         if (callt.isPar() && callt.bt() != Type::BT_ANN) {
1133           GCLock lock;
1134           try {
1135             ret.r = bind(env, ctx, r, eval_par(env, cr_c));
1136             ret.b = conj(env, b, Ctx(), args_ee);
1137           } catch (ResultUndefinedError&) {
1138             ret.r = create_dummy_value(env, cr_c->type());
1139             ret.b = bind(env, Ctx(), b, constants().literalFalse);
1140             return ret;
1141           }
1142           // Do not insert into map, since par results will quickly become
1143           // garbage anyway and then disappear from the map
1144         } else if (decl->builtins.e != nullptr) {
1145           KeepAlive callres;
1146           {
1147             GCLock lock;
1148             callres = decl->builtins.e(env, cr_c);
1149           }
1150           EE res = flat_exp(env, ctx, callres(), r, b);
1151           args_ee.push_back(res);
1152           ret.b = conj(env, b, Ctx(), args_ee);
1153           add_path_annotation(env, res.r());
1154           ret.r = bind(env, ctx, r, res.r());
1155           if (!ctx.neg && !cr_c->type().isAnn()) {
1156             env.cseMapInsert(cr_c, ret);
1157           }
1158         } else {
1159           GCLock lock;
1160           ret.b = conj(env, b, Ctx(), args_ee);
1161           add_path_annotation(env, cr_c);
1162           ret.r = bind(env, ctx, r, cr_c);
1163           if (!ctx.neg && !cr_c->type().isAnn()) {
1164             env.cseMapInsert(cr_c, ret);
1165           }
1166         }
1167       } else {
1168         std::vector<KeepAlive> previousParameters(decl->params().size());
1169         for (unsigned int i = decl->params().size(); (i--) != 0U;) {
1170           VarDecl* vd = decl->params()[i];
1171           previousParameters[i] = vd->e();
1172           vd->flat(vd);
1173           vd->e(args[i]());
1174         }
1175 
1176         if (decl->e()->type().isbool() && !decl->e()->type().isOpt()) {
1177           ret.b = bind(env, Ctx(), b, constants().literalTrue);
1178           if (ctx.b == C_ROOT && r == constants().varTrue) {
1179             (void)flat_exp(env, Ctx(), decl->e(), r, constants().varTrue);
1180           } else {
1181             Ctx nctx;
1182             if (!is_total(decl)) {
1183               nctx = ctx;
1184               nctx.neg = false;
1185             }
1186             EE ee = flat_exp(env, nctx, decl->e(), nullptr, constants().varTrue);
1187             ee.b = ee.r;
1188             args_ee.push_back(ee);
1189           }
1190           ret.r = conj(env, r, ctx, args_ee);
1191         } else {
1192           if (is_total(decl)) {
1193             EE ee = flat_exp(env, Ctx(), decl->e(), r, constants().varTrue);
1194             ret.r = bind(env, ctx, r, ee.r());
1195           } else {
1196             ret = flat_exp(env, ctx, decl->e(), r, nullptr);
1197             args_ee.push_back(ret);
1198             if (decl->e()->type().dim() > 0) {
1199               auto* al = follow_id(ret.r())->cast<ArrayLit>();
1200               assert(al->dims() == decl->e()->type().dim());
1201               for (unsigned int i = 0; i < decl->ti()->ranges().size(); i++) {
1202                 if ((decl->ti()->ranges()[i]->domain() != nullptr) &&
1203                     !decl->ti()->ranges()[i]->domain()->isa<TIId>()) {
1204                   GCLock lock;
1205                   IntSetVal* isv = eval_intset(env, decl->ti()->ranges()[i]->domain());
1206                   if (al->min(i) != isv->min() || al->max(i) != isv->max()) {
1207                     EE ee;
1208                     ee.b = constants().literalFalse;
1209                     args_ee.push_back(ee);
1210                   }
1211                 }
1212               }
1213             }
1214             if ((decl->ti()->domain() != nullptr) && !decl->ti()->domain()->isa<TIId>()) {
1215               BinOpType bot;
1216               if (ret.r()->type().st() == Type::ST_SET) {
1217                 bot = BOT_SUBSET;
1218               } else {
1219                 bot = BOT_IN;
1220               }
1221 
1222               KeepAlive domconstraint;
1223               if (decl->e()->type().dim() > 0) {
1224                 GCLock lock;
1225                 std::vector<Expression*> domargs(2);
1226                 domargs[0] = ret.r();
1227                 domargs[1] = decl->ti()->domain();
1228                 Call* c = new Call(Location().introduce(), "var_dom", domargs);
1229                 c->type(Type::varbool());
1230                 c->decl(env.model->matchFn(env, c, false));
1231                 if (c->decl() == nullptr) {
1232                   throw InternalError("no matching declaration found for var_dom");
1233                 }
1234                 domconstraint = c;
1235               } else {
1236                 GCLock lock;
1237                 domconstraint =
1238                     new BinOp(Location().introduce(), ret.r(), bot, decl->ti()->domain());
1239               }
1240               domconstraint()->type(ret.r()->type().isPar() ? Type::parbool() : Type::varbool());
1241               if (ctx.b == C_ROOT) {
1242                 (void)flat_exp(env, Ctx(), domconstraint(), constants().varTrue,
1243                                constants().varTrue);
1244               } else {
1245                 EE ee = flat_exp(env, Ctx(), domconstraint(), nullptr, constants().varTrue);
1246                 ee.b = ee.r;
1247                 args_ee.push_back(ee);
1248               }
1249             }
1250           }
1251           ret.b = conj(env, b, Ctx(), args_ee);
1252         }
1253         if (!ctx.neg && !cr()->type().isAnn()) {
1254           env.cseMapInsert(cr(), ret);
1255         }
1256 
1257         // Restore previous mapping
1258         for (unsigned int i = decl->params().size(); (i--) != 0U;) {
1259           VarDecl* vd = decl->params()[i];
1260           vd->e(previousParameters[i]());
1261           vd->flat(vd->e() != nullptr ? vd : nullptr);
1262         }
1263       }
1264     }
1265   }
1266   if (cid == "mzn_reverse_map_var") {
1267     env.inReverseMapVar = false;
1268   }
1269   return ret;
1270 }
1271 }  // namespace MiniZinc
1272