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