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