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