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
16ASTString opToBuiltin(BinOp* op, BinOpType bot) {
17 std::string builtin;
18 if (op->rhs()->type().isint()) {
19 switch (bot) {
20 case BOT_PLUS:
21 return constants().ids.int_.plus;
22 case BOT_MINUS:
23 return constants().ids.int_.minus;
24 case BOT_MULT:
25 return constants().ids.int_.times;
26 case BOT_POW:
27 return constants().ids.pow;
28 case BOT_IDIV:
29 return constants().ids.int_.div;
30 case BOT_MOD:
31 return constants().ids.int_.mod;
32 case BOT_LE:
33 return constants().ids.int_.lt;
34 case BOT_LQ:
35 return constants().ids.int_.le;
36 case BOT_GR:
37 return constants().ids.int_.gt;
38 case BOT_GQ:
39 return constants().ids.int_.ge;
40 case BOT_EQ:
41 return constants().ids.int_.eq;
42 case BOT_NQ:
43 return constants().ids.int_.ne;
44 default:
45 throw InternalError("not yet implemented");
46 }
47 } else if (op->rhs()->type().isbool()) {
48 if (bot == BOT_EQ || bot == BOT_EQUIV) return constants().ids.bool_eq;
49 builtin = "bool_";
50 } else if (op->rhs()->type().is_set()) {
51 builtin = "set_";
52 } else if (op->rhs()->type().isfloat()) {
53 switch (bot) {
54 case BOT_PLUS:
55 return constants().ids.float_.plus;
56 case BOT_MINUS:
57 return constants().ids.float_.minus;
58 case BOT_MULT:
59 return constants().ids.float_.times;
60 case BOT_POW:
61 return constants().ids.pow;
62 case BOT_DIV:
63 return constants().ids.float_.div;
64 case BOT_MOD:
65 return constants().ids.float_.mod;
66 case BOT_LE:
67 return constants().ids.float_.lt;
68 case BOT_LQ:
69 return constants().ids.float_.le;
70 case BOT_GR:
71 return constants().ids.float_.gt;
72 case BOT_GQ:
73 return constants().ids.float_.ge;
74 case BOT_EQ:
75 return constants().ids.float_.eq;
76 case BOT_NQ:
77 return constants().ids.float_.ne;
78 default:
79 throw InternalError("not yet implemented");
80 }
81 } else if (op->rhs()->type().isopt() && (bot == BOT_EQUIV || bot == BOT_EQ)) {
82 /// TODO: extend to all option type operators
83 switch (op->lhs()->type().bt()) {
84 case Type::BT_BOOL:
85 return constants().ids.bool_eq;
86 case Type::BT_FLOAT:
87 return constants().ids.float_.eq;
88 case Type::BT_INT:
89 if (op->lhs()->type().st() == Type::ST_PLAIN)
90 return constants().ids.int_.eq;
91 else
92 return constants().ids.set_eq;
93 default:
94 throw InternalError("not yet implemented");
95 }
96
97 } else {
98 throw InternalError(op->opToString().str() + " not yet implemented");
99 }
100 switch (bot) {
101 case BOT_PLUS:
102 return builtin + "plus";
103 case BOT_MINUS:
104 return builtin + "minus";
105 case BOT_MULT:
106 return builtin + "times";
107 case BOT_DIV:
108 return builtin + "div";
109 case BOT_IDIV:
110 return builtin + "div";
111 case BOT_MOD:
112 return builtin + "mod";
113 case BOT_LE:
114 return builtin + "lt";
115 case BOT_LQ:
116 return builtin + "le";
117 case BOT_GR:
118 return builtin + "gt";
119 case BOT_GQ:
120 return builtin + "ge";
121 case BOT_EQ:
122 return builtin + "eq";
123 case BOT_NQ:
124 return builtin + "ne";
125 case BOT_IN:
126 return constants().ids.set_in;
127 case BOT_SUBSET:
128 return builtin + "subset";
129 case BOT_SUPERSET:
130 return builtin + "superset";
131 case BOT_UNION:
132 return builtin + "union";
133 case BOT_DIFF:
134 return builtin + "diff";
135 case BOT_SYMDIFF:
136 return builtin + "symdiff";
137 case BOT_INTERSECT:
138 return builtin + "intersect";
139 case BOT_PLUSPLUS:
140 case BOT_DOTDOT:
141 throw InternalError("not yet implemented");
142 case BOT_EQUIV:
143 return builtin + "eq";
144 case BOT_IMPL:
145 return builtin + "le";
146 case BOT_RIMPL:
147 return builtin + "ge";
148 case BOT_OR:
149 return builtin + "or";
150 case BOT_AND:
151 return builtin + "and";
152 case BOT_XOR:
153 return constants().ids.bool_xor;
154 default:
155 assert(false);
156 return ASTString("");
157 }
158}
159
160bool isReverseMap(BinOp* e) { return e->ann().contains(constants().ann.is_reverse_map); }
161
162template <class Lit>
163void collectLinExps(EnvI& env, typename LinearTraits<Lit>::Val c, Expression* exp,
164 std::vector<typename LinearTraits<Lit>::Val>& coeffs,
165 std::vector<KeepAlive>& vars, typename LinearTraits<Lit>::Val& constval) {
166 typedef typename LinearTraits<Lit>::Val Val;
167 struct StackItem {
168 Expression* e;
169 Val c;
170 StackItem(Expression* e0, Val c0) : e(e0), c(c0) {}
171 };
172 std::vector<StackItem> stack;
173 stack.push_back(StackItem(exp, c));
174 while (!stack.empty()) {
175 Expression* e = stack.back().e;
176 Val c = stack.back().c;
177 stack.pop_back();
178 if (e == NULL) continue;
179 if (e->type().ispar()) {
180 constval += c * LinearTraits<Lit>::eval(env, e);
181 } else if (Lit* l = e->dyn_cast<Lit>()) {
182 constval += c * l->v();
183 } else if (BinOp* bo = e->dyn_cast<BinOp>()) {
184 switch (bo->op()) {
185 case BOT_PLUS:
186 stack.push_back(StackItem(bo->lhs(), c));
187 stack.push_back(StackItem(bo->rhs(), c));
188 break;
189 case BOT_MINUS:
190 stack.push_back(StackItem(bo->lhs(), c));
191 stack.push_back(StackItem(bo->rhs(), -c));
192 break;
193 case BOT_MULT:
194 if (bo->lhs()->type().ispar()) {
195 stack.push_back(StackItem(bo->rhs(), c * LinearTraits<Lit>::eval(env, bo->lhs())));
196 } else if (bo->rhs()->type().ispar()) {
197 stack.push_back(StackItem(bo->lhs(), c * LinearTraits<Lit>::eval(env, bo->rhs())));
198 } else {
199 coeffs.push_back(c);
200 vars.push_back(e);
201 }
202 break;
203 case BOT_DIV:
204 if (bo->rhs()->isa<FloatLit>() && bo->rhs()->cast<FloatLit>()->v() == 1.0) {
205 stack.push_back(StackItem(bo->lhs(), c));
206 } else {
207 coeffs.push_back(c);
208 vars.push_back(e);
209 }
210 break;
211 case BOT_IDIV:
212 if (bo->rhs()->isa<IntLit>() && bo->rhs()->cast<IntLit>()->v() == 1) {
213 stack.push_back(StackItem(bo->lhs(), c));
214 } else {
215 coeffs.push_back(c);
216 vars.push_back(e);
217 }
218 break;
219 default:
220 coeffs.push_back(c);
221 vars.push_back(e);
222 break;
223 }
224 // } else if (Call* call = e->dyn_cast<Call>()) {
225 // /// TODO! Handle sum, lin_exp (maybe not that important?)
226 } else {
227 coeffs.push_back(c);
228 vars.push_back(e);
229 }
230 }
231}
232
233template <class Lit>
234KeepAlive mklinexp(EnvI& env, typename LinearTraits<Lit>::Val c0,
235 typename LinearTraits<Lit>::Val c1, Expression* e0, Expression* e1) {
236 typedef typename LinearTraits<Lit>::Val Val;
237 GCLock lock;
238
239 std::vector<Val> coeffs;
240 std::vector<KeepAlive> vars;
241 Val constval = 0;
242 collectLinExps<Lit>(env, c0, e0, coeffs, vars, constval);
243 collectLinExps<Lit>(env, c1, e1, coeffs, vars, constval);
244 simplify_lin<Lit>(coeffs, vars, constval);
245 KeepAlive ka;
246 if (coeffs.size() == 0) {
247 ka = LinearTraits<Lit>::newLit(constval);
248 } else if (coeffs.size() == 1 && coeffs[0] == 1 && constval == 0) {
249 ka = vars[0];
250 } else {
251 std::vector<Expression*> coeffs_e(coeffs.size());
252 for (unsigned int i = static_cast<unsigned int>(coeffs.size()); i--;) {
253 if (!LinearTraits<Lit>::finite(coeffs[i])) {
254 throw FlatteningError(
255 env, e0->loc(),
256 "unbounded coefficient in linear expression."
257 " Make sure variables involved in non-linear/logical expressions have finite bounds"
258 " in their definition or via constraints");
259 }
260 coeffs_e[i] = LinearTraits<Lit>::newLit(coeffs[i]);
261 }
262 std::vector<Expression*> vars_e(vars.size());
263 for (unsigned int i = static_cast<unsigned int>(vars.size()); i--;) vars_e[i] = vars[i]();
264
265 std::vector<Expression*> args(3);
266 args[0] = new ArrayLit(e0->loc(), coeffs_e);
267 Type t = coeffs_e[0]->type();
268 t.dim(1);
269 args[0]->type(t);
270 args[1] = new ArrayLit(e0->loc(), vars_e);
271 Type tt = vars_e[0]->type();
272 tt.dim(1);
273 args[1]->type(tt);
274 args[2] = LinearTraits<Lit>::newLit(constval);
275 Call* c = new Call(e0->loc().introduce(), constants().ids.lin_exp, args);
276 addPathAnnotation(env, c);
277 tt = args[1]->type();
278 tt.dim(0);
279 c->decl(env.model->matchFn(env, c, false));
280 if (c->decl() == NULL) {
281 throw FlatteningError(env, c->loc(), "cannot find matching declaration");
282 }
283 c->type(c->decl()->rtype(env, args, false));
284 ka = c;
285 }
286 assert(ka());
287 return ka;
288}
289
290Call* aggregateAndOrOps(EnvI& env, BinOp* bo, bool negateArgs, BinOpType bot) {
291 assert(bot == BOT_AND || bot == BOT_OR);
292 BinOpType negbot = (bot == BOT_AND ? BOT_OR : BOT_AND);
293 typedef std::pair<Expression*, bool> arg_literal;
294 std::vector<arg_literal> bo_args(2);
295 bo_args[0] = arg_literal(bo->lhs(), !negateArgs);
296 bo_args[1] = arg_literal(bo->rhs(), !negateArgs);
297 std::vector<Expression*> output_pos;
298 std::vector<Expression*> output_neg;
299 unsigned int processed = 0;
300 while (processed < bo_args.size()) {
301 BinOp* bo_arg = bo_args[processed].first->dyn_cast<BinOp>();
302 UnOp* uo_arg = bo_args[processed].first->dyn_cast<UnOp>();
303 bool positive = bo_args[processed].second;
304 if (bo_arg && positive && bo_arg->op() == bot) {
305 bo_args[processed].first = bo_arg->lhs();
306 bo_args.push_back(arg_literal(bo_arg->rhs(), true));
307 } else if (bo_arg && !positive && bo_arg->op() == negbot) {
308 bo_args[processed].first = bo_arg->lhs();
309 bo_args.push_back(arg_literal(bo_arg->rhs(), false));
310 } else if (uo_arg && !positive && uo_arg->op() == UOT_NOT) {
311 bo_args[processed].first = uo_arg->e();
312 bo_args[processed].second = true;
313 } else if (bot == BOT_OR && uo_arg && positive && uo_arg->op() == UOT_NOT) {
314 output_neg.push_back(uo_arg->e());
315 processed++;
316 } else {
317 if (positive) {
318 output_pos.push_back(bo_args[processed].first);
319 } else {
320 output_neg.push_back(bo_args[processed].first);
321 }
322 processed++;
323 }
324 }
325 Call* c;
326 std::vector<Expression*> c_args(1);
327 if (bot == BOT_AND) {
328 for (unsigned int i = 0; i < output_neg.size(); i++) {
329 UnOp* neg_arg = new UnOp(output_neg[i]->loc(), UOT_NOT, output_neg[i]);
330 neg_arg->type(output_neg[i]->type());
331 output_pos.push_back(neg_arg);
332 }
333 ArrayLit* al = new ArrayLit(bo->loc().introduce(), output_pos);
334 Type al_t = bo->type();
335 al_t.dim(1);
336 al->type(al_t);
337 env.annotateFromCallStack(al);
338 c_args[0] = al;
339 c = new Call(bo->loc().introduce(),
340 bot == BOT_AND ? constants().ids.forall : constants().ids.exists, c_args);
341 } else {
342 ArrayLit* al_pos = new ArrayLit(bo->loc().introduce(), output_pos);
343 Type al_t = bo->type();
344 al_t.dim(1);
345 al_pos->type(al_t);
346 env.annotateFromCallStack(al_pos);
347 c_args[0] = al_pos;
348 if (output_neg.size() > 0) {
349 ArrayLit* al_neg = new ArrayLit(bo->loc().introduce(), output_neg);
350 al_neg->type(al_t);
351 env.annotateFromCallStack(al_neg);
352 c_args.push_back(al_neg);
353 }
354 c = new Call(bo->loc().introduce(),
355 output_neg.empty() ? constants().ids.exists : constants().ids.clause, c_args);
356 }
357 c->decl(env.model->matchFn(env, c, false));
358 assert(c->decl());
359 Type t = c->decl()->rtype(env, c_args, false);
360 t.cv(bo->type().cv());
361 c->type(t);
362 return c;
363}
364
365/// Return a lin_exp or id if \a e is a lin_exp or id
366template <class Lit>
367Expression* get_linexp(Expression* e) {
368 for (;;) {
369 if (e && e->eid() == Expression::E_ID && e != constants().absent) {
370 if (e->cast<Id>()->decl()->e()) {
371 e = e->cast<Id>()->decl()->e();
372 } else {
373 break;
374 }
375 } else {
376 break;
377 }
378 }
379 if (e && (e->isa<Id>() || e->isa<Lit>() ||
380 (e->isa<Call>() && e->cast<Call>()->id() == constants().ids.lin_exp)))
381 return e;
382 return NULL;
383}
384
385template <class Lit>
386void flatten_linexp_binop(EnvI& env, Ctx ctx, VarDecl* r, VarDecl* b, EE& ret, Expression* le0,
387 Expression* le1, BinOpType& bot, bool doubleNeg, std::vector<EE>& ees,
388 std::vector<KeepAlive>& args, ASTString& callid) {
389 typedef typename LinearTraits<Lit>::Val Val;
390 std::vector<Val> coeffv;
391 std::vector<KeepAlive> alv;
392 Val d = 0;
393 Expression* le[2] = {le0, le1};
394
395 Id* assignTo = NULL;
396 if (bot == BOT_EQ && ctx.b == C_ROOT) {
397 if (le0->isa<Id>()) {
398 assignTo = le0->cast<Id>();
399 } else if (le1->isa<Id>()) {
400 assignTo = le1->cast<Id>();
401 }
402 }
403
404 for (unsigned int i = 0; i < 2; i++) {
405 Val sign = (i == 0 ? 1 : -1);
406 if (Lit* l = le[i]->dyn_cast<Lit>()) {
407 try {
408 d += sign * l->v();
409 } catch (ArithmeticError& e) {
410 throw EvalError(env, l->loc(), e.msg());
411 }
412 } else if (le[i]->isa<Id>()) {
413 coeffv.push_back(sign);
414 alv.push_back(le[i]);
415 } else if (Call* sc = le[i]->dyn_cast<Call>()) {
416 GCLock lock;
417 ArrayLit* sc_coeff = eval_array_lit(env, sc->arg(0));
418 ArrayLit* sc_al = eval_array_lit(env, sc->arg(1));
419 try {
420 d += sign * LinearTraits<Lit>::eval(env, sc->arg(2));
421 for (unsigned int j = 0; j < sc_coeff->size(); j++) {
422 coeffv.push_back(sign * LinearTraits<Lit>::eval(env, (*sc_coeff)[j]));
423 alv.push_back((*sc_al)[j]);
424 }
425 } catch (ArithmeticError& e) {
426 throw EvalError(env, sc->loc(), e.msg());
427 }
428
429 } else {
430 throw EvalError(env, le[i]->loc(),
431 "Internal error, unexpected expression inside linear expression");
432 }
433 }
434 simplify_lin<Lit>(coeffv, alv, d);
435 if (coeffv.size() == 0) {
436 bool result;
437 switch (bot) {
438 case BOT_LE:
439 result = (0 < -d);
440 break;
441 case BOT_LQ:
442 result = (0 <= -d);
443 break;
444 case BOT_GR:
445 result = (0 > -d);
446 break;
447 case BOT_GQ:
448 result = (0 >= -d);
449 break;
450 case BOT_EQ:
451 result = (0 == -d);
452 break;
453 case BOT_NQ:
454 result = (0 != -d);
455 break;
456 default:
457 assert(false);
458 break;
459 }
460 if (doubleNeg) result = !result;
461 ees[2].b = constants().boollit(result);
462 ret.r = conj(env, r, ctx, ees);
463 return;
464 } else if (coeffv.size() == 1 && std::abs(coeffv[0]) == 1) {
465 if (coeffv[0] == -1) {
466 switch (bot) {
467 case BOT_LE:
468 bot = BOT_GR;
469 break;
470 case BOT_LQ:
471 bot = BOT_GQ;
472 break;
473 case BOT_GR:
474 bot = BOT_LE;
475 break;
476 case BOT_GQ:
477 bot = BOT_LQ;
478 break;
479 default:
480 break;
481 }
482 } else {
483 d = -d;
484 }
485 typename LinearTraits<Lit>::Bounds ib = LinearTraits<Lit>::compute_bounds(env, alv[0]());
486 if (ib.valid) {
487 bool failed = false;
488 bool subsumed = false;
489 switch (bot) {
490 case BOT_LE:
491 subsumed = ib.u < d;
492 failed = ib.l >= d;
493 break;
494 case BOT_LQ:
495 subsumed = ib.u <= d;
496 failed = ib.l > d;
497 break;
498 case BOT_GR:
499 subsumed = ib.l > d;
500 failed = ib.u <= d;
501 break;
502 case BOT_GQ:
503 subsumed = ib.l >= d;
504 failed = ib.u < d;
505 break;
506 case BOT_EQ:
507 subsumed = ib.l == d && ib.u == d;
508 failed = ib.u < d || ib.l > d;
509 break;
510 case BOT_NQ:
511 subsumed = ib.u < d || ib.l > d;
512 failed = ib.l == d && ib.u == d;
513 break;
514 default:
515 break;
516 }
517 if (doubleNeg) {
518 std::swap(subsumed, failed);
519 }
520 if (subsumed) {
521 ees[2].b = constants().lit_true;
522 ret.r = conj(env, r, ctx, ees);
523 return;
524 } else if (failed) {
525 ees[2].b = constants().lit_false;
526 ret.r = conj(env, r, ctx, ees);
527 return;
528 }
529 }
530
531 if (ctx.b == C_ROOT && alv[0]()->isa<Id>() && bot == BOT_EQ) {
532 GCLock lock;
533 VarDecl* vd = alv[0]()->cast<Id>()->decl();
534 if (vd->ti()->domain()) {
535 typename LinearTraits<Lit>::Domain domain =
536 LinearTraits<Lit>::eval_domain(env, vd->ti()->domain());
537 if (LinearTraits<Lit>::domain_contains(domain, d)) {
538 if (!LinearTraits<Lit>::domain_equals(domain, d)) {
539 // vd->ti()->setComputedDomain(false);
540 // vd->ti()->domain(LinearTraits<Lit>::new_domain(d));
541 setComputedDomain(env, vd, LinearTraits<Lit>::new_domain(d), false);
542 }
543 ret.r = bind(env, ctx, r, constants().lit_true);
544 } else {
545 ret.r = bind(env, ctx, r, constants().lit_false);
546 }
547 } else {
548 // vd->ti()->setComputedDomain(false);
549 // vd->ti()->domain(LinearTraits<Lit>::new_domain(d));
550 setComputedDomain(env, vd, LinearTraits<Lit>::new_domain(d), false);
551 ret.r = bind(env, ctx, r, constants().lit_true);
552 }
553 } else {
554 GCLock lock;
555 Expression* e0;
556 Expression* e1;
557 BinOpType old_bot = bot;
558 Val old_d = d;
559 switch (bot) {
560 case BOT_LE:
561 e0 = alv[0]();
562 if (e0->type().isint()) {
563 d--;
564 bot = BOT_LQ;
565 }
566 e1 = LinearTraits<Lit>::newLit(d);
567 break;
568 case BOT_GR:
569 e1 = alv[0]();
570 if (e1->type().isint()) {
571 d++;
572 bot = BOT_LQ;
573 } else {
574 bot = BOT_LE;
575 }
576 e0 = LinearTraits<Lit>::newLit(d);
577 break;
578 case BOT_GQ:
579 e0 = LinearTraits<Lit>::newLit(d);
580 e1 = alv[0]();
581 bot = BOT_LQ;
582 break;
583 default:
584 e0 = alv[0]();
585 e1 = LinearTraits<Lit>::newLit(d);
586 }
587 if (ctx.b == C_ROOT && alv[0]()->isa<Id>() && alv[0]()->cast<Id>()->decl()->ti()->domain()) {
588 VarDecl* vd = alv[0]()->cast<Id>()->decl();
589 typename LinearTraits<Lit>::Domain domain =
590 LinearTraits<Lit>::eval_domain(env, vd->ti()->domain());
591 typename LinearTraits<Lit>::Domain ndomain =
592 LinearTraits<Lit>::limit_domain(old_bot, domain, old_d);
593 if (domain && ndomain) {
594 if (LinearTraits<Lit>::domain_empty(ndomain)) {
595 ret.r = bind(env, ctx, r, constants().lit_false);
596 return;
597 } else if (!LinearTraits<Lit>::domain_equals(domain, ndomain)) {
598 ret.r = bind(env, ctx, r, constants().lit_true);
599 // vd->ti()->setComputedDomain(false);
600 // vd->ti()->domain(LinearTraits<Lit>::new_domain(ndomain));
601 setComputedDomain(env, vd, LinearTraits<Lit>::new_domain(ndomain), false);
602
603 if (r == constants().var_true) {
604 BinOp* bo = new BinOp(Location().introduce(), e0, bot, e1);
605 bo->type(Type::varbool());
606 std::vector<Expression*> boargs(2);
607 boargs[0] = e0;
608 boargs[1] = e1;
609 Call* c = new Call(Location(), opToBuiltin(bo, bot), boargs);
610 c->type(Type::varbool());
611 c->decl(env.model->matchFn(env, c, false));
612 EnvI::CSEMap::iterator it = env.cse_map_find(c);
613 if (it != env.cse_map_end()) {
614 if (Id* ident = it->second.r()->template dyn_cast<Id>()) {
615 bind(env, Ctx(), ident->decl(), constants().lit_true);
616 it->second.r = constants().lit_true;
617 }
618 if (Id* ident = it->second.b()->template dyn_cast<Id>()) {
619 bind(env, Ctx(), ident->decl(), constants().lit_true);
620 it->second.b = constants().lit_true;
621 }
622 }
623 }
624 }
625 return;
626 }
627 }
628 args.push_back(e0);
629 args.push_back(e1);
630 }
631 } else if (bot == BOT_EQ && coeffv.size() == 2 && coeffv[0] == -coeffv[1] && d == 0) {
632 Id* id0 = alv[0]()->cast<Id>();
633 Id* id1 = alv[1]()->cast<Id>();
634 if (ctx.b == C_ROOT && r == constants().var_true &&
635 (id0->decl()->e() == NULL || id1->decl()->e() == NULL)) {
636 if (id0->decl()->e())
637 (void)bind(env, ctx, id1->decl(), id0);
638 else
639 (void)bind(env, ctx, id0->decl(), id1);
640 } else {
641 callid = LinearTraits<Lit>::id_eq();
642 args.push_back(alv[0]());
643 args.push_back(alv[1]());
644 }
645 } else {
646 GCLock lock;
647 if (assignTo != NULL) {
648 Val resultCoeff = 0;
649 typename LinearTraits<Lit>::Bounds bounds(d, d, true);
650 for (unsigned int i = static_cast<unsigned int>(coeffv.size()); i--;) {
651 if (alv[i]() == assignTo) {
652 resultCoeff = coeffv[i];
653 continue;
654 }
655 typename LinearTraits<Lit>::Bounds b = LinearTraits<Lit>::compute_bounds(env, alv[i]());
656
657 if (b.valid && LinearTraits<Lit>::finite(b)) {
658 if (coeffv[i] > 0) {
659 bounds.l += coeffv[i] * b.l;
660 bounds.u += coeffv[i] * b.u;
661 } else {
662 bounds.l += coeffv[i] * b.u;
663 bounds.u += coeffv[i] * b.l;
664 }
665 } else {
666 bounds.valid = false;
667 break;
668 }
669 }
670 if (bounds.valid && resultCoeff != 0) {
671 if (resultCoeff < 0) {
672 bounds.l = LinearTraits<Lit>::floor_div(bounds.l, -resultCoeff);
673 bounds.u = LinearTraits<Lit>::ceil_div(bounds.u, -resultCoeff);
674 } else {
675 Val bl = bounds.l;
676 bounds.l = LinearTraits<Lit>::ceil_div(bounds.u, -resultCoeff);
677 bounds.u = LinearTraits<Lit>::floor_div(bl, -resultCoeff);
678 }
679 VarDecl* vd = assignTo->decl();
680 if (vd->ti()->domain()) {
681 typename LinearTraits<Lit>::Domain domain =
682 LinearTraits<Lit>::eval_domain(env, vd->ti()->domain());
683 if (LinearTraits<Lit>::domain_intersects(domain, bounds.l, bounds.u)) {
684 typename LinearTraits<Lit>::Domain new_domain =
685 LinearTraits<Lit>::intersect_domain(domain, bounds.l, bounds.u);
686 if (!LinearTraits<Lit>::domain_equals(domain, new_domain)) {
687 // vd->ti()->setComputedDomain(false);
688 // vd->ti()->domain(LinearTraits<Lit>::new_domain(new_domain));
689 setComputedDomain(env, vd, LinearTraits<Lit>::new_domain(new_domain), false);
690 }
691 } else {
692 ret.r = bind(env, ctx, r, constants().lit_false);
693 }
694 } else {
695 // vd->ti()->setComputedDomain(true);
696 // vd->ti()->domain(LinearTraits<Lit>::new_domain(bounds.l,bounds.u));
697 setComputedDomain(env, vd, LinearTraits<Lit>::new_domain(bounds.l, bounds.u), true);
698 }
699 }
700 }
701
702 int coeff_sign;
703 LinearTraits<Lit>::constructLinBuiltin(bot, callid, coeff_sign, d);
704 std::vector<Expression*> coeff_ev(coeffv.size());
705 for (unsigned int i = static_cast<unsigned int>(coeff_ev.size()); i--;)
706 coeff_ev[i] = LinearTraits<Lit>::newLit(coeff_sign * coeffv[i]);
707 ArrayLit* ncoeff = new ArrayLit(Location().introduce(), coeff_ev);
708 Type t = coeff_ev[0]->type();
709 t.dim(1);
710 ncoeff->type(t);
711 args.push_back(ncoeff);
712 std::vector<Expression*> alv_e(alv.size());
713 Type tt = alv[0]()->type();
714 tt.dim(1);
715 for (unsigned int i = static_cast<unsigned int>(alv.size()); i--;) {
716 if (alv[i]()->type().isvar()) tt.ti(Type::TI_VAR);
717 alv_e[i] = alv[i]();
718 }
719 ArrayLit* nal = new ArrayLit(Location().introduce(), alv_e);
720 nal->type(tt);
721 args.push_back(nal);
722 Lit* il = LinearTraits<Lit>::newLit(-d);
723 args.push_back(il);
724 }
725}
726
727EE flatten_binop(EnvI& env, Ctx ctx, Expression* e, VarDecl* r, VarDecl* b) {
728 CallStackItem _csi(env, e);
729 EE ret;
730 BinOp* bo = e->cast<BinOp>();
731 if (isReverseMap(bo)) {
732 CallArgItem cai(env);
733 Id* id = bo->lhs()->dyn_cast<Id>();
734 if (id == NULL)
735 throw EvalError(env, bo->lhs()->loc(), "Reverse mappers are only defined for identifiers");
736 if (bo->op() != BOT_EQ && bo->op() != BOT_EQUIV)
737 throw EvalError(env, bo->loc(), "Reverse mappers have to use `=` as the operator");
738 Call* c = bo->rhs()->dyn_cast<Call>();
739 if (c == NULL)
740 throw EvalError(env, bo->rhs()->loc(), "Reverse mappers require call on right hand side");
741
742 std::vector<Expression*> args(c->n_args());
743 for (unsigned int i = 0; i < c->n_args(); i++) {
744 Id* idi = c->arg(i)->dyn_cast<Id>();
745 if (idi == NULL)
746 throw EvalError(env, c->arg(i)->loc(),
747 "Reverse mapper calls require identifiers as arguments");
748 EE ee = flat_exp(env, Ctx(), idi, NULL, constants().var_true);
749 args[i] = ee.r();
750 }
751
752 EE ee = flat_exp(env, Ctx(), id, NULL, constants().var_true);
753
754 GCLock lock;
755 Call* revMap = new Call(Location().introduce(), c->id(), args);
756
757 args.push_back(ee.r());
758 Call* keepAlive = new Call(Location().introduce(), constants().var_redef->id(), args);
759 keepAlive->type(Type::varbool());
760 keepAlive->decl(constants().var_redef);
761 ret = flat_exp(env, Ctx(), keepAlive, constants().var_true, constants().var_true);
762
763 if (ee.r()->isa<Id>()) {
764 env.reverseMappers.insert(ee.r()->cast<Id>(), revMap);
765 }
766 return ret;
767 }
768 if ((bo->op() == BOT_EQ || bo->op() == BOT_EQUIV) &&
769 (bo->lhs() == constants().absent || bo->rhs() == constants().absent)) {
770 GCLock lock;
771 std::vector<Expression*> args(1);
772 args[0] = bo->lhs() == constants().absent ? bo->rhs() : bo->lhs();
773 if (args[0] != constants().absent) {
774 Call* cr = new Call(bo->loc().introduce(), "absent", args);
775 cr->decl(env.model->matchFn(env, cr, false));
776 cr->type(cr->decl()->rtype(env, args, false));
777 ret = flat_exp(env, ctx, cr, r, b);
778 } else {
779 ret.b = bind(env, Ctx(), b, constants().lit_true);
780 ret.r = bind(env, ctx, r, constants().lit_true);
781 }
782 return ret;
783 }
784 Ctx ctx0 = ctx;
785 ctx0.neg = false;
786 Ctx ctx1 = ctx;
787 ctx1.neg = false;
788 BinOpType bot = bo->op();
789 if (bo->lhs()->type().isbool()) {
790 switch (bot) {
791 case BOT_EQ:
792 bot = BOT_EQUIV;
793 break;
794 case BOT_NQ:
795 bot = BOT_XOR;
796 break;
797 case BOT_LQ:
798 bot = BOT_IMPL;
799 break;
800 case BOT_GQ:
801 bot = BOT_RIMPL;
802 break;
803 default:
804 break;
805 }
806 }
807 bool negArgs = false;
808 bool doubleNeg = false;
809 if (ctx.neg) {
810 switch (bot) {
811 case BOT_AND:
812 ctx.b = -ctx.b;
813 ctx.neg = false;
814 negArgs = true;
815 bot = BOT_OR;
816 break;
817 case BOT_OR:
818 ctx.b = -ctx.b;
819 ctx.neg = false;
820 negArgs = true;
821 bot = BOT_AND;
822 break;
823 default:
824 break;
825 }
826 }
827 Expression* boe0 = bo->lhs();
828 Expression* boe1 = bo->rhs();
829 bool isBuiltin = bo->decl() == NULL || bo->decl()->e() == NULL;
830 switch (bot) {
831 case BOT_PLUS:
832 if (isBuiltin) {
833 KeepAlive ka;
834 if (boe0->type().isint()) {
835 ka = mklinexp<IntLit>(env, 1, 1, boe0, boe1);
836 } else {
837 ka = mklinexp<FloatLit>(env, 1.0, 1.0, boe0, boe1);
838 }
839 ret = flat_exp(env, ctx, ka(), r, b);
840 break;
841 }
842 case BOT_MINUS:
843 if (isBuiltin) {
844 KeepAlive ka;
845 if (boe0->type().isint()) {
846 ka = mklinexp<IntLit>(env, 1, -1, boe0, boe1);
847 } else {
848 ka = mklinexp<FloatLit>(env, 1.0, -1.0, boe0, boe1);
849 }
850 ret = flat_exp(env, ctx, ka(), r, b);
851 break;
852 }
853 case BOT_MULT:
854 case BOT_IDIV:
855 case BOT_MOD:
856 case BOT_POW:
857 case BOT_DIV:
858 case BOT_UNION:
859 case BOT_DIFF:
860 case BOT_SYMDIFF:
861 case BOT_INTERSECT:
862 case BOT_DOTDOT: {
863 assert(!ctx0.neg);
864 assert(!ctx1.neg);
865 EE e0 = flat_exp(env, ctx0, boe0, NULL, b);
866 EE e1 = flat_exp(env, ctx1, boe1, NULL, b);
867
868 if (e0.r()->type().ispar() && e1.r()->type().ispar()) {
869 GCLock lock;
870 BinOp* parbo = new BinOp(bo->loc(), e0.r(), bo->op(), e1.r());
871 Type tt = bo->type();
872 tt.ti(Type::TI_PAR);
873 parbo->type(tt);
874 try {
875 Expression* res = eval_par(env, parbo);
876 assert(!res->type().isunknown());
877 ret.r = bind(env, ctx, r, res);
878 std::vector<EE> ees(2);
879 ees[0].b = e0.b;
880 ees[1].b = e1.b;
881 ret.b = conj(env, b, Ctx(), ees);
882 } catch (ResultUndefinedError&) {
883 ret.r = createDummyValue(env, e->type());
884 ret.b = bind(env, Ctx(), b, constants().lit_false);
885 }
886 break;
887 }
888
889 if (isBuiltin && bot == BOT_MULT) {
890 Expression* e0r = e0.r();
891 Expression* e1r = e1.r();
892 if (e0r->type().ispar()) std::swap(e0r, e1r);
893 if (e1r->type().ispar() && e1r->type().isint()) {
894 IntVal coeff = eval_int(env, e1r);
895 KeepAlive ka = mklinexp<IntLit>(env, coeff, 0, e0r, NULL);
896 ret = flat_exp(env, ctx, ka(), r, b);
897 break;
898 } else if (e1r->type().ispar() && e1r->type().isfloat()) {
899 FloatVal coeff = eval_float(env, e1r);
900 KeepAlive ka = mklinexp<FloatLit>(env, coeff, 0.0, e0r, NULL);
901 ret = flat_exp(env, ctx, ka(), r, b);
902 break;
903 }
904 } else if (isBuiltin && (bot == BOT_DIV || bot == BOT_IDIV)) {
905 Expression* e0r = e0.r();
906 Expression* e1r = e1.r();
907 if (e1r->type().ispar() && e1r->type().isint()) {
908 IntVal coeff = eval_int(env, e1r);
909 if (coeff == 1) {
910 ret = flat_exp(env, ctx, e0r, r, b);
911 break;
912 }
913 } else if (e1r->type().ispar() && e1r->type().isfloat()) {
914 FloatVal coeff = eval_float(env, e1r);
915 if (coeff == 1.0) {
916 ret = flat_exp(env, ctx, e0r, r, b);
917 break;
918 } else {
919 KeepAlive ka = mklinexp<FloatLit>(env, 1.0 / coeff, 0.0, e0r, NULL);
920 ret = flat_exp(env, ctx, ka(), r, b);
921 break;
922 }
923 }
924 }
925
926 GC::lock();
927 std::vector<Expression*> args(2);
928 args[0] = e0.r();
929 args[1] = e1.r();
930 Call* cc;
931 if (bo->decl()) {
932 cc = new Call(bo->loc().introduce(), bo->opToString(), args);
933 } else {
934 cc = new Call(bo->loc().introduce(), opToBuiltin(bo, bot), args);
935 }
936 cc->type(bo->type());
937 EnvI::CSEMap::iterator cit;
938 if ((cit = env.cse_map_find(cc)) != env.cse_map_end()) {
939 ret.b = bind(env, Ctx(), b, env.ignorePartial ? constants().lit_true : cit->second.b());
940 ret.r = bind(env, ctx, r, cit->second.r());
941 } else {
942 if (FunctionI* fi = env.model->matchFn(env, cc->id(), args, false)) {
943 assert(cc->type() == fi->rtype(env, args, false));
944 cc->decl(fi);
945 cc->type(cc->decl()->rtype(env, args, false));
946 KeepAlive ka(cc);
947 GC::unlock();
948 EE ee = flat_exp(env, ctx, cc, r, NULL);
949 GC::lock();
950 ret.r = ee.r;
951 std::vector<EE> ees(3);
952 ees[0].b = e0.b;
953 ees[1].b = e1.b;
954 ees[2].b = ee.b;
955 ret.b = conj(env, b, Ctx(), ees);
956 } else {
957 addPathAnnotation(env, cc);
958 ret.r = bind(env, ctx, r, cc);
959 std::vector<EE> ees(2);
960 ees[0].b = e0.b;
961 ees[1].b = e1.b;
962 ret.b = conj(env, b, Ctx(), ees);
963 if (!ctx.neg) env.cse_map_insert(cc, ret);
964 }
965 }
966 }
967 GC::unlock();
968 break;
969
970 case BOT_AND: {
971 if (r == constants().var_true) {
972 Ctx nctx;
973 nctx.neg = negArgs;
974 nctx.b = negArgs ? C_NEG : C_ROOT;
975 std::vector<Expression*> todo;
976 todo.push_back(boe1);
977 todo.push_back(boe0);
978 while (!todo.empty()) {
979 Expression* e_todo = todo.back();
980 todo.pop_back();
981 BinOp* e_bo = e_todo->dyn_cast<BinOp>();
982 if (e_bo && e_bo->op() == BOT_AND) {
983 todo.push_back(e_bo->rhs());
984 todo.push_back(e_bo->lhs());
985 } else {
986 (void)flat_exp(env, nctx, e_todo, constants().var_true, constants().var_true);
987 }
988 }
989 ret.r = bind(env, ctx, r, constants().lit_true);
990 break;
991 } else {
992 GC::lock();
993 Call* c = aggregateAndOrOps(env, bo, negArgs, bot);
994 KeepAlive ka(c);
995 GC::unlock();
996 ret = flat_exp(env, ctx, c, r, b);
997 if (Id* id = ret.r()->dyn_cast<Id>()) {
998 addCtxAnn(id->decl(), ctx.b);
999 }
1000 }
1001 break;
1002 }
1003 case BOT_OR: {
1004 GC::lock();
1005 Call* c = aggregateAndOrOps(env, bo, negArgs, bot);
1006 KeepAlive ka(c);
1007 GC::unlock();
1008 ret = flat_exp(env, ctx, c, r, b);
1009 if (Id* id = ret.r()->dyn_cast<Id>()) {
1010 addCtxAnn(id->decl(), ctx.b);
1011 }
1012 } break;
1013 case BOT_RIMPL: {
1014 std::swap(boe0, boe1);
1015 }
1016 // fall through
1017 case BOT_IMPL: {
1018 if (ctx.b == C_ROOT && r == constants().var_true && boe0->type().ispar()) {
1019 bool b;
1020 {
1021 GCLock lock;
1022 b = eval_bool(env, boe0);
1023 }
1024 if (b) {
1025 Ctx nctx = ctx;
1026 nctx.neg = negArgs;
1027 nctx.b = negArgs ? C_NEG : C_ROOT;
1028 ret = flat_exp(env, nctx, boe1, constants().var_true, constants().var_true);
1029 } else {
1030 Ctx nctx = ctx;
1031 nctx.neg = negArgs;
1032 nctx.b = negArgs ? C_NEG : C_ROOT;
1033 ret =
1034 flat_exp(env, nctx, constants().lit_true, constants().var_true, constants().var_true);
1035 }
1036 break;
1037 }
1038 if (ctx.b == C_ROOT && r == constants().var_true && boe1->type().ispar()) {
1039 bool b;
1040 {
1041 GCLock lock;
1042 b = eval_bool(env, boe1);
1043 }
1044 if (b) {
1045 Ctx nctx = ctx;
1046 nctx.neg = negArgs;
1047 nctx.b = negArgs ? C_NEG : C_ROOT;
1048 ret =
1049 flat_exp(env, nctx, constants().lit_true, constants().var_true, constants().var_true);
1050 break;
1051 } else {
1052 Ctx nctx = ctx;
1053 nctx.neg = !negArgs;
1054 nctx.b = !negArgs ? C_NEG : C_ROOT;
1055 ret = flat_exp(env, nctx, boe0, constants().var_true, constants().var_true);
1056 break;
1057 }
1058 }
1059 GC::lock();
1060 std::vector<Expression*> args;
1061 ASTString id;
1062 if (ctx.neg) {
1063 std::vector<Expression*> bo_args(2);
1064 bo_args[0] = boe0;
1065 bo_args[1] = new UnOp(bo->loc(), UOT_NOT, boe1);
1066 bo_args[1]->type(boe1->type());
1067 id = constants().ids.forall;
1068 args.push_back(new ArrayLit(bo->loc(), bo_args));
1069 args[0]->type(Type::varbool(1));
1070 } else {
1071 std::vector<Expression*> clause_pos(1);
1072 clause_pos[0] = boe1;
1073 std::vector<Expression*> clause_neg(1);
1074 clause_neg[0] = boe0;
1075 args.push_back(new ArrayLit(boe1->loc().introduce(), clause_pos));
1076 Type t0 = boe1->type();
1077 t0.dim(1);
1078 args[0]->type(t0);
1079 args.push_back(new ArrayLit(boe0->loc().introduce(), clause_neg));
1080 Type t1 = boe0->type();
1081 t1.dim(1);
1082 args[1]->type(t1);
1083 id = constants().ids.clause;
1084 }
1085 ctx.neg = false;
1086 Call* c = new Call(bo->loc().introduce(), id, args);
1087 c->decl(env.model->matchFn(env, c, false));
1088 if (c->decl() == NULL) {
1089 throw FlatteningError(env, c->loc(), "cannot find matching declaration");
1090 }
1091 c->type(c->decl()->rtype(env, args, false));
1092 KeepAlive ka(c);
1093 GC::unlock();
1094 ret = flat_exp(env, ctx, c, r, b);
1095 if (Id* id = ret.r()->dyn_cast<Id>()) {
1096 addCtxAnn(id->decl(), ctx.b);
1097 }
1098 } break;
1099 case BOT_EQUIV:
1100 if (ctx.neg) {
1101 ctx.neg = false;
1102 ctx.b = -ctx.b;
1103 bot = BOT_XOR;
1104 ctx0.b = ctx1.b = C_MIX;
1105 goto flatten_bool_op;
1106 } else {
1107 if (!boe1->type().isopt() && istrue(env, boe0)) {
1108 return flat_exp(env, ctx, boe1, r, b);
1109 }
1110 if (!boe0->type().isopt() && istrue(env, boe1)) {
1111 return flat_exp(env, ctx, boe0, r, b);
1112 }
1113 if (r && r == constants().var_true) {
1114 if (boe1->type().ispar() || boe1->isa<Id>()) std::swap(boe0, boe1);
1115 if (istrue(env, boe0)) {
1116 return flat_exp(env, ctx1, boe1, r, b);
1117 } else if (isfalse(env, boe0)) {
1118 ctx1.neg = true;
1119 ctx1.b = -ctx1.b;
1120 return flat_exp(env, ctx1, boe1, r, b);
1121 } else {
1122 ctx0.b = C_MIX;
1123 EE e0 = flat_exp(env, ctx0, boe0, NULL, NULL);
1124 if (istrue(env, e0.r())) {
1125 return flat_exp(env, ctx1, boe1, r, b);
1126 } else if (isfalse(env, e0.r())) {
1127 ctx1.neg = true;
1128 ctx1.b = -ctx1.b;
1129 return flat_exp(env, ctx1, boe1, r, b);
1130 } else {
1131 Id* id = e0.r()->cast<Id>();
1132 ctx1.b = C_MIX;
1133 (void)flat_exp(env, ctx1, boe1, id->decl(), constants().var_true);
1134 addCtxAnn(id->decl(), ctx1.b);
1135 ret.b = bind(env, Ctx(), b, constants().lit_true);
1136 ret.r = bind(env, Ctx(), r, constants().lit_true);
1137 }
1138 }
1139 break;
1140 } else {
1141 ctx0.b = ctx1.b = C_MIX;
1142 goto flatten_bool_op;
1143 }
1144 }
1145 case BOT_XOR:
1146 if (ctx.neg) {
1147 ctx.neg = false;
1148 ctx.b = -ctx.b;
1149 bot = BOT_EQUIV;
1150 }
1151 ctx0.b = ctx1.b = C_MIX;
1152 goto flatten_bool_op;
1153 case BOT_LE:
1154 if (ctx.neg) {
1155 doubleNeg = true;
1156 bot = BOT_GQ;
1157 if (boe0->type().bt() == Type::BT_BOOL) {
1158 ctx0.b = +ctx0.b;
1159 ctx1.b = -ctx1.b;
1160 } else if (boe0->type().bt() == Type::BT_INT) {
1161 ctx0.i = +ctx0.b;
1162 ctx1.i = -ctx1.b;
1163 }
1164 } else {
1165 if (boe0->type().bt() == Type::BT_BOOL) {
1166 ctx0.b = -ctx0.b;
1167 ctx1.b = +ctx1.b;
1168 } else if (boe0->type().bt() == Type::BT_INT) {
1169 ctx0.i = -ctx0.b;
1170 ctx1.i = +ctx1.b;
1171 }
1172 }
1173 goto flatten_bool_op;
1174 case BOT_LQ:
1175 if (ctx.neg) {
1176 doubleNeg = true;
1177 bot = BOT_GR;
1178 if (boe0->type().bt() == Type::BT_BOOL) {
1179 ctx0.b = +ctx0.b;
1180 ctx1.b = -ctx1.b;
1181 } else if (boe0->type().bt() == Type::BT_INT) {
1182 ctx0.i = +ctx0.b;
1183 ctx1.i = -ctx1.b;
1184 }
1185 } else {
1186 if (boe0->type().bt() == Type::BT_BOOL) {
1187 ctx0.b = -ctx0.b;
1188 ctx1.b = +ctx1.b;
1189 } else if (boe0->type().bt() == Type::BT_INT) {
1190 ctx0.i = -ctx0.b;
1191 ctx1.i = +ctx1.b;
1192 }
1193 }
1194 goto flatten_bool_op;
1195 case BOT_GR:
1196 if (ctx.neg) {
1197 doubleNeg = true;
1198 bot = BOT_LQ;
1199 if (boe0->type().bt() == Type::BT_BOOL) {
1200 ctx0.b = -ctx0.b;
1201 ctx1.b = +ctx1.b;
1202 } else if (boe0->type().bt() == Type::BT_INT) {
1203 ctx0.i = -ctx0.b;
1204 ctx1.i = +ctx1.b;
1205 }
1206 } else {
1207 if (boe0->type().bt() == Type::BT_BOOL) {
1208 ctx0.b = +ctx0.b;
1209 ctx1.b = -ctx1.b;
1210 } else if (boe0->type().bt() == Type::BT_INT) {
1211 ctx0.i = +ctx0.b;
1212 ctx1.i = -ctx1.b;
1213 }
1214 }
1215 goto flatten_bool_op;
1216 case BOT_GQ:
1217 if (ctx.neg) {
1218 doubleNeg = true;
1219 bot = BOT_LE;
1220 if (boe0->type().bt() == Type::BT_BOOL) {
1221 ctx0.b = -ctx0.b;
1222 ctx1.b = +ctx1.b;
1223 } else if (boe0->type().bt() == Type::BT_INT) {
1224 ctx0.i = -ctx0.b;
1225 ctx1.i = +ctx1.b;
1226 }
1227 } else {
1228 if (boe0->type().bt() == Type::BT_BOOL) {
1229 ctx0.b = +ctx0.b;
1230 ctx1.b = -ctx1.b;
1231 } else if (boe0->type().bt() == Type::BT_INT) {
1232 ctx0.i = +ctx0.b;
1233 ctx1.i = -ctx1.b;
1234 }
1235 }
1236 goto flatten_bool_op;
1237 case BOT_EQ:
1238 if (ctx.neg) {
1239 doubleNeg = true;
1240 bot = BOT_NQ;
1241 }
1242 if (boe0->type().bt() == Type::BT_BOOL) {
1243 ctx0.b = ctx1.b = C_MIX;
1244 } else if (boe0->type().bt() == Type::BT_INT) {
1245 ctx0.i = ctx1.i = C_MIX;
1246 }
1247 goto flatten_bool_op;
1248 case BOT_NQ:
1249 if (ctx.neg) {
1250 doubleNeg = true;
1251 bot = BOT_EQ;
1252 }
1253 if (boe0->type().bt() == Type::BT_BOOL) {
1254 ctx0.b = ctx1.b = C_MIX;
1255 } else if (boe0->type().bt() == Type::BT_INT) {
1256 ctx0.i = ctx1.i = C_MIX;
1257 }
1258 goto flatten_bool_op;
1259 case BOT_IN:
1260 case BOT_SUBSET:
1261 case BOT_SUPERSET:
1262 ctx0.i = ctx1.i = C_MIX;
1263 flatten_bool_op : {
1264 bool inRootCtx = (ctx0.b == ctx1.b && ctx0.b == C_ROOT && b == constants().var_true);
1265 EE e0 = flat_exp(env, ctx0, boe0, NULL, inRootCtx ? b : NULL);
1266 EE e1 = flat_exp(env, ctx1, boe1, NULL, inRootCtx ? b : NULL);
1267
1268 ret.b = bind(env, Ctx(), b, constants().lit_true);
1269
1270 std::vector<EE> ees(3);
1271 ees[0].b = e0.b;
1272 ees[1].b = e1.b;
1273
1274 if (isfalse(env, e0.b()) || isfalse(env, e1.b())) {
1275 ees.resize(2);
1276 ret.r = conj(env, r, ctx, ees);
1277 break;
1278 }
1279
1280 if (e0.r()->type().ispar() && e1.r()->type().ispar()) {
1281 GCLock lock;
1282 BinOp* bo_par = new BinOp(e->loc(), e0.r(), bot, e1.r());
1283 std::vector<Expression*> args({e0.r(), e1.r()});
1284 bo_par->decl(env.model->matchFn(env, bo_par->opToString(), args, false));
1285 if (bo_par->decl() == NULL) {
1286 throw FlatteningError(env, bo_par->loc(), "cannot find matching declaration");
1287 }
1288 bo_par->type(Type::parbool());
1289 bool bo_val = eval_bool(env, bo_par);
1290 if (doubleNeg) bo_val = !bo_val;
1291 ees[2].b = constants().boollit(bo_val);
1292 ret.r = conj(env, r, ctx, ees);
1293 break;
1294 }
1295
1296 if (e0.r()->type().bt() == Type::BT_INT && e1.r()->type().ispar() && e0.r()->isa<Id>() &&
1297 (bot == BOT_IN || bot == BOT_SUBSET)) {
1298 VarDecl* vd = e0.r()->cast<Id>()->decl();
1299 Id* ident = vd->id();
1300 if (ctx.b == C_ROOT && r == constants().var_true) {
1301 if (vd->ti()->domain() == NULL) {
1302 vd->ti()->domain(e1.r());
1303 } else {
1304 GCLock lock;
1305 IntSetVal* newdom = eval_intset(env, e1.r());
1306 while (ident != NULL) {
1307 bool changeDom = false;
1308 if (ident->decl()->ti()->domain()) {
1309 IntSetVal* domain = eval_intset(env, ident->decl()->ti()->domain());
1310 IntSetRanges dr(domain);
1311 IntSetRanges ibr(newdom);
1312 Ranges::Inter<IntVal, IntSetRanges, IntSetRanges> i(dr, ibr);
1313 IntSetVal* newibv = IntSetVal::ai(i);
1314 if (domain->card() != newibv->card()) {
1315 newdom = newibv;
1316 changeDom = true;
1317 }
1318 } else {
1319 changeDom = true;
1320 }
1321 if (ident->type().st() == Type::ST_PLAIN && newdom->size() == 0) {
1322 env.fail();
1323 } else if (changeDom) {
1324 // ident->decl()->ti()->setComputedDomain(false);
1325 // ident->decl()->ti()->domain(new SetLit(Location().introduce(),newdom));
1326 setComputedDomain(env, ident->decl(), new SetLit(Location().introduce(), newdom),
1327 false);
1328 if (ident->decl()->e() == NULL && newdom->min() == newdom->max()) {
1329 ident->decl()->e(IntLit::a(newdom->min()));
1330 }
1331 }
1332 ident = ident->decl()->e() ? ident->decl()->e()->dyn_cast<Id>() : NULL;
1333 }
1334 }
1335 ret.r = bind(env, ctx, r, constants().lit_true);
1336 break;
1337 } else if (vd->ti()->domain() != NULL) {
1338 // check if current domain is already subsumed or falsified by this constraint
1339 GCLock lock;
1340 IntSetVal* check_dom = eval_intset(env, e1.r());
1341 IntSetVal* domain = eval_intset(env, ident->decl()->ti()->domain());
1342 {
1343 IntSetRanges cdr(check_dom);
1344 IntSetRanges dr(domain);
1345 if (Ranges::subset(dr, cdr)) {
1346 // the constraint is subsumed
1347 ret.r = bind(env, ctx, r, constants().lit_true);
1348 break;
1349 }
1350 }
1351 if (vd->type().st() == Type::ST_PLAIN) {
1352 // only for var int (for var set of int, subset can never fail because of the domain)
1353 IntSetRanges cdr(check_dom);
1354 IntSetRanges dr(domain);
1355 if (Ranges::disjoint(cdr, dr)) {
1356 // the constraint is false
1357 ret.r = bind(env, ctx, r, constants().lit_false);
1358 break;
1359 }
1360 }
1361 }
1362 }
1363
1364 std::vector<KeepAlive> args;
1365 ASTString callid;
1366
1367 Expression* le0 = NULL;
1368 Expression* le1 = NULL;
1369
1370 if (boe0->type().isint() && !boe0->type().isopt() && bot != BOT_IN) {
1371 le0 = get_linexp<IntLit>(e0.r());
1372 } else if (boe0->type().isfloat() && !boe0->type().isopt() && bot != BOT_IN) {
1373 le0 = get_linexp<FloatLit>(e0.r());
1374 }
1375 if (le0) {
1376 if (boe0->type().isint() && boe1->type().isint() && !boe1->type().isopt()) {
1377 le1 = get_linexp<IntLit>(e1.r());
1378 } else if (boe0->type().isfloat() && boe1->type().isfloat() && !boe1->type().isopt()) {
1379 le1 = get_linexp<FloatLit>(e1.r());
1380 }
1381 }
1382 if (le1) {
1383 if (boe0->type().isint()) {
1384 flatten_linexp_binop<IntLit>(env, ctx, r, b, ret, le0, le1, bot, doubleNeg, ees, args,
1385 callid);
1386 } else {
1387 flatten_linexp_binop<FloatLit>(env, ctx, r, b, ret, le0, le1, bot, doubleNeg, ees, args,
1388 callid);
1389 }
1390 } else {
1391 if (bo->decl() == NULL) {
1392 switch (bot) {
1393 case BOT_GR:
1394 std::swap(e0, e1);
1395 bot = BOT_LE;
1396 break;
1397 case BOT_GQ:
1398 std::swap(e0, e1);
1399 bot = BOT_LQ;
1400 break;
1401 default:
1402 break;
1403 }
1404 }
1405 args.push_back(e0.r);
1406 args.push_back(e1.r);
1407 }
1408
1409 if (args.size() > 0) {
1410 GC::lock();
1411
1412 if (callid == "") {
1413 if (bo->decl()) {
1414 callid = bo->decl()->id();
1415 } else {
1416 callid = opToBuiltin(bo, bot);
1417 }
1418 }
1419
1420 std::vector<Expression*> args_e(args.size());
1421 for (unsigned int i = static_cast<unsigned int>(args.size()); i--;) args_e[i] = args[i]();
1422 Call* cc = new Call(e->loc().introduce(), callid, args_e);
1423 cc->decl(env.model->matchFn(env, cc->id(), args_e, false));
1424 if (cc->decl() == NULL) {
1425 throw FlatteningError(env, cc->loc(), "cannot find matching declaration");
1426 }
1427 cc->type(cc->decl()->rtype(env, args_e, false));
1428
1429 // add defines_var annotation if applicable
1430 Id* assignTo = NULL;
1431 if (bot == BOT_EQ && ctx.b == C_ROOT) {
1432 if (le0 && le0->isa<Id>()) {
1433 assignTo = le0->cast<Id>();
1434 } else if (le1 && le1->isa<Id>()) {
1435 assignTo = le1->cast<Id>();
1436 }
1437 if (assignTo) {
1438 makeDefinedVar(assignTo->decl()->flat(), cc);
1439 }
1440 }
1441
1442 EnvI::CSEMap::iterator cit = env.cse_map_find(cc);
1443 if (cit != env.cse_map_end()) {
1444 ees[2].b = cit->second.r();
1445 if (doubleNeg) {
1446 Type t = ees[2].b()->type();
1447 ees[2].b = new UnOp(Location().introduce(), UOT_NOT, ees[2].b());
1448 ees[2].b()->type(t);
1449 }
1450 if (Id* id = ees[2].b()->dyn_cast<Id>()) {
1451 addCtxAnn(id->decl(), ctx.b);
1452 }
1453 ret.r = conj(env, r, ctx, ees);
1454 GC::unlock();
1455 } else {
1456 bool singleExp = true;
1457 for (unsigned int i = 0; i < ees.size(); i++) {
1458 if (!istrue(env, ees[i].b())) {
1459 singleExp = false;
1460 break;
1461 }
1462 }
1463 KeepAlive ka(cc);
1464 GC::unlock();
1465 if (singleExp) {
1466 if (doubleNeg) {
1467 ctx.b = -ctx.b;
1468 ctx.neg = !ctx.neg;
1469 }
1470 ret.r = flat_exp(env, ctx, cc, r, NULL).r;
1471 } else {
1472 ees[2].b = flat_exp(env, Ctx(), cc, NULL, NULL).r;
1473 if (doubleNeg) {
1474 GCLock lock;
1475 Type t = ees[2].b()->type();
1476 ees[2].b = new UnOp(Location().introduce(), UOT_NOT, ees[2].b());
1477 ees[2].b()->type(t);
1478 }
1479 if (Id* id = ees[2].b()->dyn_cast<Id>()) {
1480 addCtxAnn(id->decl(), ctx.b);
1481 }
1482 ret.r = conj(env, r, ctx, ees);
1483 }
1484 }
1485 } else {
1486 ret.r = conj(env, r, ctx, ees);
1487 }
1488 } break;
1489
1490 case BOT_PLUSPLUS: {
1491 std::vector<EE> ee(2);
1492 EE eev = flat_exp(env, ctx, boe0, NULL, NULL);
1493 ee[0] = eev;
1494 ArrayLit* al;
1495 if (eev.r()->isa<ArrayLit>()) {
1496 al = eev.r()->cast<ArrayLit>();
1497 } else {
1498 Id* id = eev.r()->cast<Id>();
1499 if (id->decl() == NULL) {
1500 throw InternalError("undefined identifier");
1501 }
1502 if (id->decl()->e() == NULL) {
1503 throw InternalError("array without initialiser not supported");
1504 }
1505 al = follow_id(id)->cast<ArrayLit>();
1506 }
1507 ArrayLit* al0 = al;
1508 eev = flat_exp(env, ctx, boe1, NULL, NULL);
1509 ee[1] = eev;
1510 if (eev.r()->isa<ArrayLit>()) {
1511 al = eev.r()->cast<ArrayLit>();
1512 } else {
1513 Id* id = eev.r()->cast<Id>();
1514 if (id->decl() == NULL) {
1515 throw InternalError("undefined identifier");
1516 }
1517 if (id->decl()->e() == NULL) {
1518 throw InternalError("array without initialiser not supported");
1519 }
1520 al = follow_id(id)->cast<ArrayLit>();
1521 }
1522 ArrayLit* al1 = al;
1523 std::vector<Expression*> v(al0->size() + al1->size());
1524 for (unsigned int i = al0->size(); i--;) v[i] = (*al0)[i];
1525 for (unsigned int i = al1->size(); i--;) v[al0->size() + i] = (*al1)[i];
1526 GCLock lock;
1527 ArrayLit* alret = new ArrayLit(e->loc(), v);
1528 alret->type(e->type());
1529 ret.b = conj(env, b, Ctx(), ee);
1530 ret.r = bind(env, ctx, r, alret);
1531 } break;
1532 }
1533 return ret;
1534}
1535
1536} // namespace MiniZinc