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 
16 namespace MiniZinc {
17 
op_to_builtin(Expression * op_lhs,Expression * op_rhs,BinOpType bot)18 ASTString 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 
op_to_id(BinOpType bot)164 ASTString 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 
is_reverse_map(BinOp * e)226 bool is_reverse_map(BinOp* e) { return e->ann().contains(constants().ann.is_reverse_map); }
227 
228 template <class Lit>
collect_linexps(EnvI & env,typename LinearTraits<Lit>::Val in_c,Expression * exp,std::vector<typename LinearTraits<Lit>::Val> & coeffs,std::vector<KeepAlive> & vars,typename LinearTraits<Lit>::Val & constval)229 void 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 
301 template <class Lit>
mklinexp(EnvI & env,typename LinearTraits<Lit>::Val c0,typename LinearTraits<Lit>::Val c1,Expression * e0,Expression * e1)302 KeepAlive 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 
aggregate_and_or_ops(EnvI & env,BinOp * bo,bool negateArgs,BinOpType bot)360 Call* 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
441 template <class Lit>
get_linexp(Expression * e)442 Expression* 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 
461 template <class Lit>
flatten_linexp_binop(EnvI & env,const Ctx & ctx,VarDecl * r,VarDecl * b,EE & ret,Expression * le0,Expression * le1,BinOpType & bot,bool doubleNeg,std::vector<EE> & ees,std::vector<KeepAlive> & args,ASTString & callid)462 void 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 
flatten_binop(EnvI & env,const Ctx & input_ctx,Expression * e,VarDecl * r,VarDecl * b)804 EE 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
1648