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/astexception.hh>
13#include <minizinc/astiterator.hh>
14#include <minizinc/copy.hh>
15#include <minizinc/eval_par.hh>
16#include <minizinc/flatten.hh>
17#include <minizinc/hash.hh>
18#include <minizinc/iter.hh>
19
20#include <cmath>
21
22namespace MiniZinc {
23
24bool checkParDomain(EnvI& env, Expression* e, Expression* domain) {
25 if (e->type() == Type::parint()) {
26 IntSetVal* isv = eval_intset(env, domain);
27 if (!isv->contains(eval_int(env, e))) return false;
28 } else if (e->type() == Type::parfloat()) {
29 FloatSetVal* fsv = eval_floatset(env, domain);
30 if (!fsv->contains(eval_float(env, e))) return false;
31 } else if (e->type() == Type::parsetint()) {
32 IntSetVal* isv = eval_intset(env, domain);
33 IntSetRanges ir(isv);
34 IntSetVal* rsv = eval_intset(env, e);
35 IntSetRanges rr(rsv);
36 if (!Ranges::subset(rr, ir)) return false;
37 } else if (e->type() == Type::parsetfloat()) {
38 FloatSetVal* fsv = eval_floatset(env, domain);
39 FloatSetRanges fr(fsv);
40 FloatSetVal* rsv = eval_floatset(env, e);
41 FloatSetRanges rr(rsv);
42 if (!Ranges::subset(rr, fr)) return false;
43 }
44 return true;
45}
46
47template <class E>
48typename E::Val eval_id(EnvI& env, Expression* e) {
49 Id* id = e->cast<Id>();
50 if (id->decl() == NULL) throw EvalError(env, e->loc(), "undeclared identifier", id->str().str());
51 VarDecl* vd = id->decl();
52 while (vd->flat() && vd->flat() != vd) vd = vd->flat();
53 if (vd->e() == NULL)
54 throw EvalError(env, vd->loc(), "cannot evaluate expression", id->str().str());
55 typename E::Val r = E::e(env, vd->e());
56 if (!vd->evaluated() && (vd->toplevel() || vd->type().dim() > 0)) {
57 Expression* ne = E::exp(r);
58 vd->e(ne);
59 vd->evaluated(true);
60 }
61 return r;
62}
63
64class EvalIntLit {
65public:
66 typedef IntLit* Val;
67 typedef Expression* ArrayVal;
68 static IntLit* e(EnvI& env, Expression* e) { return IntLit::a(eval_int(env, e)); }
69 static Expression* exp(IntLit* e) { return e; }
70 Expression* flatten(EnvI&, Expression*) {
71 throw InternalError("evaluating var assignment generator inside par expression not supported");
72 }
73};
74class EvalIntVal {
75public:
76 typedef IntVal Val;
77 typedef IntVal ArrayVal;
78 static IntVal e(EnvI& env, Expression* e) { return eval_int(env, e); }
79 static Expression* exp(IntVal e) { return IntLit::a(e); }
80 static void checkRetVal(EnvI& env, Val v, FunctionI* fi) {
81 if (fi->ti()->domain() && !fi->ti()->domain()->isa<TIId>()) {
82 IntSetVal* isv = eval_intset(env, fi->ti()->domain());
83 if (!isv->contains(v)) {
84 throw ResultUndefinedError(env, Location().introduce(),
85 "function result violates function type-inst");
86 }
87 }
88 }
89 Expression* flatten(EnvI&, Expression*) {
90 throw InternalError("evaluating var assignment generator inside par expression not supported");
91 }
92};
93class EvalFloatVal {
94public:
95 typedef FloatVal Val;
96 typedef FloatVal ArrayVal;
97 static FloatVal e(EnvI& env, Expression* e) { return eval_float(env, e); }
98 static Expression* exp(FloatVal e) { return FloatLit::a(e); }
99 static void checkRetVal(EnvI& env, Val v, FunctionI* fi) {
100 if (fi->ti()->domain() && !fi->ti()->domain()->isa<TIId>()) {
101 FloatSetVal* fsv = eval_floatset(env, fi->ti()->domain());
102 if (!fsv->contains(v)) {
103 throw ResultUndefinedError(env, Location().introduce(),
104 "function result violates function type-inst");
105 }
106 }
107 }
108 Expression* flatten(EnvI&, Expression*) {
109 throw InternalError("evaluating var assignment generator inside par expression not supported");
110 }
111};
112class EvalFloatLit {
113public:
114 typedef FloatLit* Val;
115 typedef Expression* ArrayVal;
116 static FloatLit* e(EnvI& env, Expression* e) { return FloatLit::a(eval_float(env, e)); }
117 static Expression* exp(Expression* e) { return e; }
118 Expression* flatten(EnvI&, Expression*) {
119 throw InternalError("evaluating var assignment generator inside par expression not supported");
120 }
121};
122class EvalString {
123public:
124 typedef std::string Val;
125 typedef std::string ArrayVal;
126 static std::string e(EnvI& env, Expression* e) { return eval_string(env, e); }
127 static Expression* exp(const std::string& e) { return new StringLit(Location(), e); }
128 static void checkRetVal(EnvI& env, Val v, FunctionI* fi) {}
129 Expression* flatten(EnvI&, Expression*) {
130 throw InternalError("evaluating var assignment generator inside par expression not supported");
131 }
132};
133class EvalStringLit {
134public:
135 typedef StringLit* Val;
136 typedef Expression* ArrayVal;
137 static StringLit* e(EnvI& env, Expression* e) {
138 return new StringLit(Location(), eval_string(env, e));
139 }
140 static Expression* exp(Expression* e) { return e; }
141 Expression* flatten(EnvI&, Expression*) {
142 throw InternalError("evaluating var assignment generator inside par expression not supported");
143 }
144};
145class EvalBoolLit {
146public:
147 typedef BoolLit* Val;
148 typedef Expression* ArrayVal;
149 static BoolLit* e(EnvI& env, Expression* e) { return constants().boollit(eval_bool(env, e)); }
150 static Expression* exp(Expression* e) { return e; }
151 Expression* flatten(EnvI&, Expression*) {
152 throw InternalError("evaluating var assignment generator inside par expression not supported");
153 }
154};
155class EvalBoolVal {
156public:
157 typedef bool Val;
158 static bool e(EnvI& env, Expression* e) { return eval_bool(env, e); }
159 static Expression* exp(bool e) { return constants().boollit(e); }
160 static void checkRetVal(EnvI& env, Val v, FunctionI* fi) {}
161 Expression* flatten(EnvI&, Expression*) {
162 throw InternalError("evaluating var assignment generator inside par expression not supported");
163 }
164};
165class EvalArrayLit {
166public:
167 typedef ArrayLit* Val;
168 typedef Expression* ArrayVal;
169 static ArrayLit* e(EnvI& env, Expression* e) { return eval_array_lit(env, e); }
170 static Expression* exp(Expression* e) { return e; }
171 Expression* flatten(EnvI&, Expression*) {
172 throw InternalError("evaluating var assignment generator inside par expression not supported");
173 }
174};
175class EvalArrayLitCopy {
176public:
177 typedef ArrayLit* Val;
178 typedef Expression* ArrayVal;
179 static ArrayLit* e(EnvI& env, Expression* e) {
180 return copy(env, eval_array_lit(env, e), true)->cast<ArrayLit>();
181 }
182 static Expression* exp(Expression* e) { return e; }
183 static void checkRetVal(EnvI& env, Val v, FunctionI* fi) {
184 for (unsigned int i = 0; i < fi->ti()->ranges().size(); i++) {
185 if (fi->ti()->ranges()[i]->domain() && !fi->ti()->ranges()[i]->domain()->isa<TIId>()) {
186 IntSetVal* isv = eval_intset(env, fi->ti()->ranges()[i]->domain());
187 bool bothEmpty = isv->min() > isv->max() && v->min(i) > v->max(i);
188 if (!bothEmpty && (v->min(i) != isv->min() || v->max(i) != isv->max())) {
189 std::ostringstream oss;
190 oss << "array index set " << (i + 1) << " of function result violates function type-inst";
191 throw ResultUndefinedError(env, fi->e()->loc(), oss.str());
192 }
193 }
194 }
195 if (fi->ti()->domain() && !fi->ti()->domain()->isa<TIId>() &&
196 fi->ti()->type().ti() == Type::TI_PAR) {
197 Type base_t = fi->ti()->type();
198 if (base_t.bt() == Type::BT_INT) {
199 IntSetVal* isv = eval_intset(env, fi->ti()->domain());
200 if (base_t.st() == Type::ST_PLAIN) {
201 for (unsigned int i = 0; i < v->size(); i++) {
202 IntVal iv = eval_int(env, (*v)[i]);
203 if (!isv->contains(iv)) {
204 std::ostringstream oss;
205 oss << "array contains value " << iv << " which is not contained in " << *isv;
206 throw ResultUndefinedError(
207 env, fi->e()->loc(), "function result violates function type-inst, " + oss.str());
208 }
209 }
210 } else {
211 for (unsigned int i = 0; i < v->size(); i++) {
212 IntSetVal* iv = eval_intset(env, (*v)[i]);
213 IntSetRanges isv_r(isv);
214 IntSetRanges v_r(iv);
215 if (!Ranges::subset(v_r, isv_r)) {
216 std::ostringstream oss;
217 oss << "array contains value " << *iv << " which is not a subset of " << *isv;
218 throw ResultUndefinedError(
219 env, fi->e()->loc(), "function result violates function type-inst, " + oss.str());
220 }
221 }
222 }
223 } else if (base_t.bt() == Type::BT_FLOAT) {
224 FloatSetVal* fsv = eval_floatset(env, fi->ti()->domain());
225 if (base_t.st() == Type::ST_PLAIN) {
226 for (unsigned int i = 0; i < v->size(); i++) {
227 FloatVal fv = eval_float(env, (*v)[i]);
228 if (!fsv->contains(fv)) {
229 std::ostringstream oss;
230 oss << "array contains value " << fv << " which is not contained in " << *fsv;
231 throw ResultUndefinedError(
232 env, fi->e()->loc(), "function result violates function type-inst, " + oss.str());
233 }
234 }
235 } else {
236 for (unsigned int i = 0; i < v->size(); i++) {
237 FloatSetVal* fv = eval_floatset(env, (*v)[i]);
238 FloatSetRanges fsv_r(fsv);
239 FloatSetRanges v_r(fv);
240 if (!Ranges::subset(v_r, fsv_r)) {
241 std::ostringstream oss;
242 oss << "array contains value " << *fv << " which is not a subset of " << *fsv;
243 throw ResultUndefinedError(
244 env, fi->e()->loc(), "function result violates function type-inst, " + oss.str());
245 }
246 }
247 }
248 }
249 }
250 }
251 Expression* flatten(EnvI&, Expression*) {
252 throw InternalError("evaluating var assignment generator inside par expression not supported");
253 }
254};
255class EvalIntSet {
256public:
257 typedef IntSetVal* Val;
258 static IntSetVal* e(EnvI& env, Expression* e) { return eval_intset(env, e); }
259 static Expression* exp(IntSetVal* e) { return new SetLit(Location(), e); }
260 static void checkRetVal(EnvI& env, Val v, FunctionI* fi) {
261 if (fi->ti()->domain() && !fi->ti()->domain()->isa<TIId>()) {
262 IntSetVal* isv = eval_intset(env, fi->ti()->domain());
263 IntSetRanges isv_r(isv);
264 IntSetRanges v_r(v);
265 if (!Ranges::subset(v_r, isv_r)) {
266 throw ResultUndefinedError(env, Location().introduce(),
267 "function result violates function type-inst");
268 }
269 }
270 }
271 Expression* flatten(EnvI&, Expression*) {
272 throw InternalError("evaluating var assignment generator inside par expression not supported");
273 }
274};
275class EvalFloatSet {
276public:
277 typedef FloatSetVal* Val;
278 static FloatSetVal* e(EnvI& env, Expression* e) { return eval_floatset(env, e); }
279 static Expression* exp(FloatSetVal* e) { return new SetLit(Location(), e); }
280 static void checkRetVal(EnvI& env, Val v, FunctionI* fi) {
281 if (fi->ti()->domain() && !fi->ti()->domain()->isa<TIId>()) {
282 FloatSetVal* fsv = eval_floatset(env, fi->ti()->domain());
283 FloatSetRanges fsv_r(fsv);
284 FloatSetRanges v_r(v);
285 if (!Ranges::subset(v_r, fsv_r)) {
286 throw ResultUndefinedError(env, Location().introduce(),
287 "function result violates function type-inst");
288 }
289 }
290 }
291 Expression* flatten(EnvI&, Expression*) {
292 throw InternalError("evaluating var assignment generator inside par expression not supported");
293 }
294};
295class EvalBoolSet {
296public:
297 typedef IntSetVal* Val;
298 static IntSetVal* e(EnvI& env, Expression* e) { return eval_boolset(env, e); }
299 static Expression* exp(IntSetVal* e) { return new SetLit(Location(), e); }
300 static void checkRetVal(EnvI& env, Val v, FunctionI* fi) {}
301 Expression* flatten(EnvI&, Expression*) {
302 throw InternalError("evaluating var assignment generator inside par expression not supported");
303 }
304};
305class EvalSetLit {
306public:
307 typedef SetLit* Val;
308 typedef Expression* ArrayVal;
309 static SetLit* e(EnvI& env, Expression* e) { return new SetLit(e->loc(), eval_intset(env, e)); }
310 static Expression* exp(Expression* e) { return e; }
311 Expression* flatten(EnvI&, Expression*) {
312 throw InternalError("evaluating var assignment generator inside par expression not supported");
313 }
314};
315class EvalFloatSetLit {
316public:
317 typedef SetLit* Val;
318 typedef Expression* ArrayVal;
319 static SetLit* e(EnvI& env, Expression* e) { return new SetLit(e->loc(), eval_floatset(env, e)); }
320 static Expression* exp(Expression* e) { return e; }
321 Expression* flatten(EnvI&, Expression*) {
322 throw InternalError("evaluating var assignment generator inside par expression not supported");
323 }
324};
325class EvalBoolSetLit {
326public:
327 typedef SetLit* Val;
328 typedef Expression* ArrayVal;
329 static SetLit* e(EnvI& env, Expression* e) { return new SetLit(e->loc(), eval_boolset(env, e)); }
330 static Expression* exp(Expression* e) { return e; }
331 Expression* flatten(EnvI&, Expression*) {
332 throw InternalError("evaluating var assignment generator inside par expression not supported");
333 }
334};
335class EvalCopy {
336public:
337 typedef Expression* Val;
338 typedef Expression* ArrayVal;
339 static Expression* e(EnvI& env, Expression* e) { return copy(env, e, true); }
340 static Expression* exp(Expression* e) { return e; }
341 Expression* flatten(EnvI&, Expression*) {
342 throw InternalError("evaluating var assignment generator inside par expression not supported");
343 }
344};
345class EvalPar {
346public:
347 typedef Expression* Val;
348 typedef Expression* ArrayVal;
349 static Expression* e(EnvI& env, Expression* e) { return eval_par(env, e); }
350 static Expression* exp(Expression* e) { return e; }
351 static void checkRetVal(EnvI& env, Val v, FunctionI* fi) {}
352 Expression* flatten(EnvI&, Expression*) {
353 throw InternalError("evaluating var assignment generator inside par expression not supported");
354 }
355};
356
357void checkDom(EnvI& env, Id* arg, IntSetVal* dom, Expression* e) {
358 bool oob = false;
359 if (!e->type().isopt()) {
360 if (e->type().isintset()) {
361 IntSetVal* ev = eval_intset(env, e);
362 IntSetRanges ev_r(ev);
363 IntSetRanges dom_r(dom);
364 oob = !Ranges::subset(ev_r, dom_r);
365 } else {
366 oob = !dom->contains(eval_int(env, e));
367 }
368 }
369 if (oob) {
370 std::ostringstream oss;
371 oss << "value for argument `" << *arg << "' out of bounds";
372 throw EvalError(env, e->loc(), oss.str());
373 }
374}
375
376void checkDom(EnvI& env, Id* arg, FloatVal dom_min, FloatVal dom_max, Expression* e) {
377 if (!e->type().isopt()) {
378 FloatVal ev = eval_float(env, e);
379 if (ev < dom_min || ev > dom_max) {
380 std::ostringstream oss;
381 oss << "value for argument `" << *arg << "' out of bounds";
382 throw EvalError(env, e->loc(), oss.str());
383 }
384 }
385}
386
387template <class Eval, class CallClass = Call>
388typename Eval::Val eval_call(EnvI& env, CallClass* ce) {
389 std::vector<Expression*> previousParameters(ce->decl()->params().size());
390 std::vector<Expression*> params(ce->decl()->params().size());
391 for (unsigned int i = 0; i < ce->decl()->params().size(); i++) {
392 params[i] = eval_par(env, ce->arg(i));
393 }
394 for (unsigned int i = ce->decl()->params().size(); i--;) {
395 VarDecl* vd = ce->decl()->params()[i];
396 if (vd->type().dim() > 0) {
397 // Check array index sets
398 ArrayLit* al = params[i]->cast<ArrayLit>();
399 for (unsigned int j = 0; j < vd->ti()->ranges().size(); j++) {
400 TypeInst* range_ti = vd->ti()->ranges()[j];
401 if (range_ti->domain() && !range_ti->domain()->isa<TIId>()) {
402 IntSetVal* isv = eval_intset(env, range_ti->domain());
403 if (isv->min() != al->min(j) || isv->max() != al->max(j)) {
404 std::ostringstream oss;
405 oss << "array index set " << (j + 1) << " of argument " << (i + 1)
406 << " does not match declared index set";
407 throw EvalError(env, ce->loc(), oss.str());
408 }
409 }
410 }
411 }
412 previousParameters[i] = vd->e();
413 vd->flat(vd);
414 vd->e(params[i]);
415 if (vd->e()->type().ispar()) {
416 if (Expression* dom = vd->ti()->domain()) {
417 if (!dom->isa<TIId>()) {
418 if (vd->e()->type().bt() == Type::BT_INT) {
419 IntSetVal* isv = eval_intset(env, dom);
420 if (vd->e()->type().dim() > 0) {
421 ArrayLit* al = eval_array_lit(env, vd->e());
422 for (unsigned int i = 0; i < al->size(); i++) {
423 checkDom(env, vd->id(), isv, (*al)[i]);
424 }
425 } else {
426 checkDom(env, vd->id(), isv, vd->e());
427 }
428 } else if (vd->e()->type().bt() == Type::BT_FLOAT) {
429 GCLock lock;
430 FloatSetVal* fsv = eval_floatset(env, dom);
431 FloatVal dom_min = fsv->min();
432 FloatVal dom_max = fsv->max();
433 checkDom(env, vd->id(), dom_min, dom_max, vd->e());
434 }
435 }
436 }
437 }
438 }
439 typename Eval::Val ret = Eval::e(env, ce->decl()->e());
440 Eval::checkRetVal(env, ret, ce->decl());
441 for (unsigned int i = ce->decl()->params().size(); i--;) {
442 VarDecl* vd = ce->decl()->params()[i];
443 vd->e(previousParameters[i]);
444 vd->flat(vd->e() ? vd : NULL);
445 }
446 return ret;
447}
448
449ArrayLit* eval_array_comp(EnvI& env, Comprehension* e) {
450 ArrayLit* ret;
451 if (e->type() == Type::parint(1)) {
452 std::vector<Expression*> a = eval_comp<EvalIntLit>(env, e);
453 ret = new ArrayLit(e->loc(), a);
454 } else if (e->type() == Type::parbool(1)) {
455 std::vector<Expression*> a = eval_comp<EvalBoolLit>(env, e);
456 ret = new ArrayLit(e->loc(), a);
457 } else if (e->type() == Type::parfloat(1)) {
458 std::vector<Expression*> a = eval_comp<EvalFloatLit>(env, e);
459 ret = new ArrayLit(e->loc(), a);
460 } else if (e->type() == Type::parsetint(1)) {
461 std::vector<Expression*> a = eval_comp<EvalSetLit>(env, e);
462 ret = new ArrayLit(e->loc(), a);
463 } else if (e->type() == Type::parstring(1)) {
464 std::vector<Expression*> a = eval_comp<EvalStringLit>(env, e);
465 ret = new ArrayLit(e->loc(), a);
466 } else {
467 std::vector<Expression*> a = eval_comp<EvalCopy>(env, e);
468 ret = new ArrayLit(e->loc(), a);
469 }
470 ret->type(e->type());
471 return ret;
472}
473
474ArrayLit* eval_array_lit(EnvI& env, Expression* e) {
475 CallStackItem csi(env, e);
476 switch (e->eid()) {
477 case Expression::E_INTLIT:
478 case Expression::E_FLOATLIT:
479 case Expression::E_BOOLLIT:
480 case Expression::E_STRINGLIT:
481 case Expression::E_SETLIT:
482 case Expression::E_ANON:
483 case Expression::E_TI:
484 case Expression::E_TIID:
485 case Expression::E_VARDECL:
486 throw EvalError(env, e->loc(), "not an array expression");
487 case Expression::E_ID:
488 return eval_id<EvalArrayLit>(env, e);
489 case Expression::E_ARRAYLIT:
490 return e->cast<ArrayLit>();
491 case Expression::E_ARRAYACCESS:
492 throw EvalError(env, e->loc(), "arrays of arrays not supported");
493 case Expression::E_COMP:
494 return eval_array_comp(env, e->cast<Comprehension>());
495 case Expression::E_ITE: {
496 ITE* ite = e->cast<ITE>();
497 for (int i = 0; i < ite->size(); i++) {
498 if (eval_bool(env, ite->e_if(i))) return eval_array_lit(env, ite->e_then(i));
499 }
500 return eval_array_lit(env, ite->e_else());
501 }
502 case Expression::E_BINOP: {
503 BinOp* bo = e->cast<BinOp>();
504 if (bo->op() == BOT_PLUSPLUS) {
505 ArrayLit* al0 = eval_array_lit(env, bo->lhs());
506 ArrayLit* al1 = eval_array_lit(env, bo->rhs());
507 std::vector<Expression*> v(al0->size() + al1->size());
508 for (unsigned int i = al0->size(); i--;) v[i] = (*al0)[i];
509 for (unsigned int i = al1->size(); i--;) v[al0->size() + i] = (*al1)[i];
510 ArrayLit* ret = new ArrayLit(e->loc(), v);
511 ret->flat(al0->flat() && al1->flat());
512 ret->type(e->type());
513 return ret;
514 } else {
515 if (bo->decl() && bo->decl()->e()) {
516 return eval_call<EvalArrayLitCopy, BinOp>(env, bo);
517 }
518 throw EvalError(env, e->loc(), "not an array expression", bo->opToString());
519 }
520 } break;
521 case Expression::E_UNOP: {
522 UnOp* uo = e->cast<UnOp>();
523 if (uo->decl() && uo->decl()->e()) {
524 return eval_call<EvalArrayLitCopy, UnOp>(env, uo);
525 }
526 throw EvalError(env, e->loc(), "not an array expression");
527 }
528 case Expression::E_CALL: {
529 Call* ce = e->cast<Call>();
530 if (ce->decl() == NULL) throw EvalError(env, e->loc(), "undeclared function", ce->id());
531
532 if (ce->decl()->_builtins.e) return eval_array_lit(env, ce->decl()->_builtins.e(env, ce));
533
534 if (ce->decl()->e() == NULL)
535 throw EvalError(env, ce->loc(), "internal error: missing builtin '" + ce->id().str() + "'");
536
537 return eval_call<EvalArrayLitCopy>(env, ce);
538 }
539 case Expression::E_LET: {
540 Let* l = e->cast<Let>();
541 l->pushbindings();
542 for (unsigned int i = 0; i < l->let().size(); i++) {
543 // Evaluate all variable declarations
544 if (VarDecl* vdi = l->let()[i]->dyn_cast<VarDecl>()) {
545 vdi->e(eval_par(env, vdi->e()));
546 if (vdi->ti()->domain()) {
547 if (!checkParDomain(env, vdi->e(), vdi->ti()->domain())) {
548 throw ResultUndefinedError(env, l->let()[i]->loc(),
549 "domain constraint in let failed");
550 }
551 }
552 } else {
553 // This is a constraint item. Since the let is par,
554 // it can only be a par bool expression. If it evaluates
555 // to false, it means that the value of this let is undefined.
556 if (!eval_bool(env, l->let()[i])) {
557 throw ResultUndefinedError(env, l->let()[i]->loc(), "constraint in let failed");
558 }
559 }
560 }
561 ArrayLit* l_in = eval_array_lit(env, l->in());
562 ArrayLit* ret = copy(env, l_in, true)->cast<ArrayLit>();
563 ret->flat(l_in->flat());
564 l->popbindings();
565 return ret;
566 }
567 }
568 assert(false);
569 return NULL;
570}
571
572Expression* eval_arrayaccess(EnvI& env, ArrayLit* al, const std::vector<IntVal>& dims,
573 bool& success) {
574 success = true;
575 assert(al->dims() == dims.size());
576 IntVal realidx = 0;
577 int realdim = 1;
578 for (int i = 0; i < al->dims(); i++) realdim *= al->max(i) - al->min(i) + 1;
579 for (int i = 0; i < al->dims(); i++) {
580 IntVal ix = dims[i];
581 if (ix < al->min(i) || ix > al->max(i)) {
582 success = false;
583 Type t = al->type();
584 t.dim(0);
585 if (t.isint()) return IntLit::a(0);
586 if (t.isbool()) return constants().lit_false;
587 if (t.isfloat()) return FloatLit::a(0.0);
588 if (t.st() == Type::ST_SET || t.isbot()) {
589 SetLit* ret = new SetLit(Location(), std::vector<Expression*>());
590 ret->type(t);
591 return ret;
592 }
593 if (t.isstring()) return new StringLit(Location(), "");
594 throw EvalError(env, al->loc(), "Internal error: unexpected type in array access expression");
595 }
596 realdim /= al->max(i) - al->min(i) + 1;
597 realidx += (ix - al->min(i)) * realdim;
598 }
599 assert(realidx >= 0 && realidx <= al->size());
600 return (*al)[static_cast<unsigned int>(realidx.toInt())];
601}
602Expression* eval_arrayaccess(EnvI& env, ArrayAccess* e, bool& success) {
603 ArrayLit* al = eval_array_lit(env, e->v());
604 std::vector<IntVal> dims(e->idx().size());
605 for (unsigned int i = e->idx().size(); i--;) {
606 dims[i] = eval_int(env, e->idx()[i]);
607 }
608 return eval_arrayaccess(env, al, dims, success);
609}
610Expression* eval_arrayaccess(EnvI& env, ArrayAccess* e) {
611 bool success;
612 Expression* ret = eval_arrayaccess(env, e, success);
613 if (success)
614 return ret;
615 else
616 throw ResultUndefinedError(env, e->loc(), "array access out of bounds");
617}
618
619IntSetVal* eval_intset(EnvI& env, Expression* e) {
620 if (SetLit* sl = e->dyn_cast<SetLit>()) {
621 if (sl->isv()) return sl->isv();
622 }
623 CallStackItem csi(env, e);
624 switch (e->eid()) {
625 case Expression::E_SETLIT: {
626 SetLit* sl = e->cast<SetLit>();
627 std::vector<IntVal> vals(sl->v().size());
628 for (unsigned int i = 0; i < sl->v().size(); i++) vals[i] = eval_int(env, sl->v()[i]);
629 return IntSetVal::a(vals);
630 }
631 case Expression::E_BOOLLIT:
632 case Expression::E_INTLIT:
633 case Expression::E_FLOATLIT:
634 case Expression::E_STRINGLIT:
635 case Expression::E_ANON:
636 case Expression::E_TIID:
637 case Expression::E_VARDECL:
638 case Expression::E_TI:
639 throw EvalError(env, e->loc(), "not a set of int expression");
640 break;
641 case Expression::E_ARRAYLIT: {
642 ArrayLit* al = e->cast<ArrayLit>();
643 std::vector<IntVal> vals(al->size());
644 for (unsigned int i = 0; i < al->size(); i++) vals[i] = eval_int(env, (*al)[i]);
645 return IntSetVal::a(vals);
646 } break;
647 case Expression::E_COMP: {
648 Comprehension* c = e->cast<Comprehension>();
649 std::vector<IntVal> a = eval_comp<EvalIntVal>(env, c);
650 return IntSetVal::a(a);
651 }
652 case Expression::E_ID: {
653 GCLock lock;
654 return eval_id<EvalSetLit>(env, e)->isv();
655 } break;
656 case Expression::E_ARRAYACCESS: {
657 GCLock lock;
658 return eval_intset(env, eval_arrayaccess(env, e->cast<ArrayAccess>()));
659 } break;
660 case Expression::E_ITE: {
661 ITE* ite = e->cast<ITE>();
662 for (int i = 0; i < ite->size(); i++) {
663 if (eval_bool(env, ite->e_if(i))) return eval_intset(env, ite->e_then(i));
664 }
665 return eval_intset(env, ite->e_else());
666 } break;
667 case Expression::E_BINOP: {
668 BinOp* bo = e->cast<BinOp>();
669 if (bo->decl() && bo->decl()->e()) {
670 return eval_call<EvalIntSet, BinOp>(env, bo);
671 }
672 Expression* lhs = eval_par(env, bo->lhs());
673 Expression* rhs = eval_par(env, bo->rhs());
674 if (lhs->type().isintset() && rhs->type().isintset()) {
675 IntSetVal* v0 = eval_intset(env, lhs);
676 IntSetVal* v1 = eval_intset(env, rhs);
677 IntSetRanges ir0(v0);
678 IntSetRanges ir1(v1);
679 switch (bo->op()) {
680 case BOT_UNION: {
681 Ranges::Union<IntVal, IntSetRanges, IntSetRanges> u(ir0, ir1);
682 return IntSetVal::ai(u);
683 }
684 case BOT_DIFF: {
685 Ranges::Diff<IntVal, IntSetRanges, IntSetRanges> u(ir0, ir1);
686 return IntSetVal::ai(u);
687 }
688 case BOT_SYMDIFF: {
689 Ranges::Union<IntVal, IntSetRanges, IntSetRanges> u(ir0, ir1);
690 Ranges::Inter<IntVal, IntSetRanges, IntSetRanges> i(ir0, ir1);
691 Ranges::Diff<IntVal, Ranges::Union<IntVal, IntSetRanges, IntSetRanges>,
692 Ranges::Inter<IntVal, IntSetRanges, IntSetRanges>>
693 sd(u, i);
694 return IntSetVal::ai(sd);
695 }
696 case BOT_INTERSECT: {
697 Ranges::Inter<IntVal, IntSetRanges, IntSetRanges> u(ir0, ir1);
698 return IntSetVal::ai(u);
699 }
700 default:
701 throw EvalError(env, e->loc(), "not a set of int expression", bo->opToString());
702 }
703 } else if (lhs->type().isint() && rhs->type().isint()) {
704 if (bo->op() != BOT_DOTDOT)
705 throw EvalError(env, e->loc(), "not a set of int expression", bo->opToString());
706 return IntSetVal::a(eval_int(env, lhs), eval_int(env, rhs));
707 } else {
708 throw EvalError(env, e->loc(), "not a set of int expression", bo->opToString());
709 }
710 } break;
711 case Expression::E_UNOP: {
712 UnOp* uo = e->cast<UnOp>();
713 if (uo->decl() && uo->decl()->e()) {
714 return eval_call<EvalIntSet, UnOp>(env, uo);
715 }
716 throw EvalError(env, e->loc(), "not a set of int expression");
717 }
718 case Expression::E_CALL: {
719 Call* ce = e->cast<Call>();
720 if (ce->decl() == NULL) throw EvalError(env, e->loc(), "undeclared function", ce->id());
721
722 if (ce->decl()->_builtins.s) return ce->decl()->_builtins.s(env, ce);
723
724 if (ce->decl()->_builtins.e) return eval_intset(env, ce->decl()->_builtins.e(env, ce));
725
726 if (ce->decl()->e() == NULL)
727 throw EvalError(env, ce->loc(), "internal error: missing builtin '" + ce->id().str() + "'");
728
729 return eval_call<EvalIntSet>(env, ce);
730 } break;
731 case Expression::E_LET: {
732 Let* l = e->cast<Let>();
733 l->pushbindings();
734 for (unsigned int i = 0; i < l->let().size(); i++) {
735 // Evaluate all variable declarations
736 if (VarDecl* vdi = l->let()[i]->dyn_cast<VarDecl>()) {
737 vdi->e(eval_par(env, vdi->e()));
738 if (vdi->ti()->domain()) {
739 if (!checkParDomain(env, vdi->e(), vdi->ti()->domain())) {
740 throw ResultUndefinedError(env, l->let()[i]->loc(),
741 "domain constraint in let failed");
742 }
743 }
744 } else {
745 // This is a constraint item. Since the let is par,
746 // it can only be a par bool expression. If it evaluates
747 // to false, it means that the value of this let is undefined.
748 if (!eval_bool(env, l->let()[i])) {
749 throw ResultUndefinedError(env, l->let()[i]->loc(), "constraint in let failed");
750 }
751 }
752 }
753 IntSetVal* ret = eval_intset(env, l->in());
754 l->popbindings();
755 return ret;
756 } break;
757 default:
758 assert(false);
759 return NULL;
760 }
761}
762
763FloatSetVal* eval_floatset(EnvI& env, Expression* e) {
764 if (SetLit* sl = e->dyn_cast<SetLit>()) {
765 if (sl->fsv()) return sl->fsv();
766 }
767 CallStackItem csi(env, e);
768 switch (e->eid()) {
769 case Expression::E_SETLIT: {
770 SetLit* sl = e->cast<SetLit>();
771 std::vector<FloatVal> vals(sl->v().size());
772 for (unsigned int i = 0; i < sl->v().size(); i++) vals[i] = eval_float(env, sl->v()[i]);
773 return FloatSetVal::a(vals);
774 }
775 case Expression::E_BOOLLIT:
776 case Expression::E_INTLIT:
777 case Expression::E_FLOATLIT:
778 case Expression::E_STRINGLIT:
779 case Expression::E_ANON:
780 case Expression::E_TIID:
781 case Expression::E_VARDECL:
782 case Expression::E_TI:
783 throw EvalError(env, e->loc(), "not a set of float expression");
784 break;
785 case Expression::E_ARRAYLIT: {
786 ArrayLit* al = e->cast<ArrayLit>();
787 std::vector<FloatVal> vals(al->size());
788 for (unsigned int i = 0; i < al->size(); i++) vals[i] = eval_float(env, (*al)[i]);
789 return FloatSetVal::a(vals);
790 } break;
791 case Expression::E_COMP: {
792 Comprehension* c = e->cast<Comprehension>();
793 std::vector<FloatVal> a = eval_comp<EvalFloatVal>(env, c);
794 return FloatSetVal::a(a);
795 }
796 case Expression::E_ID: {
797 GCLock lock;
798 return eval_floatset(env, eval_id<EvalFloatSetLit>(env, e));
799 } break;
800 case Expression::E_ARRAYACCESS: {
801 GCLock lock;
802 return eval_floatset(env, eval_arrayaccess(env, e->cast<ArrayAccess>()));
803 } break;
804 case Expression::E_ITE: {
805 ITE* ite = e->cast<ITE>();
806 for (int i = 0; i < ite->size(); i++) {
807 if (eval_bool(env, ite->e_if(i))) return eval_floatset(env, ite->e_then(i));
808 }
809 return eval_floatset(env, ite->e_else());
810 } break;
811 case Expression::E_BINOP: {
812 BinOp* bo = e->cast<BinOp>();
813 if (bo->decl() && bo->decl()->e()) {
814 return eval_call<EvalFloatSet, BinOp>(env, bo);
815 }
816 Expression* lhs = eval_par(env, bo->lhs());
817 Expression* rhs = eval_par(env, bo->rhs());
818 if (lhs->type().isfloatset() && rhs->type().isfloatset()) {
819 FloatSetVal* v0 = eval_floatset(env, lhs);
820 FloatSetVal* v1 = eval_floatset(env, rhs);
821 FloatSetRanges fr0(v0);
822 FloatSetRanges fr1(v1);
823 switch (bo->op()) {
824 case BOT_UNION: {
825 Ranges::Union<FloatVal, FloatSetRanges, FloatSetRanges> u(fr0, fr1);
826 return FloatSetVal::ai(u);
827 }
828 case BOT_DIFF: {
829 Ranges::Diff<FloatVal, FloatSetRanges, FloatSetRanges> u(fr0, fr1);
830 return FloatSetVal::ai(u);
831 }
832 case BOT_SYMDIFF: {
833 Ranges::Union<FloatVal, FloatSetRanges, FloatSetRanges> u(fr0, fr1);
834 Ranges::Inter<FloatVal, FloatSetRanges, FloatSetRanges> i(fr0, fr1);
835 Ranges::Diff<FloatVal, Ranges::Union<FloatVal, FloatSetRanges, FloatSetRanges>,
836 Ranges::Inter<FloatVal, FloatSetRanges, FloatSetRanges>>
837 sd(u, i);
838 return FloatSetVal::ai(sd);
839 }
840 case BOT_INTERSECT: {
841 Ranges::Inter<FloatVal, FloatSetRanges, FloatSetRanges> u(fr0, fr1);
842 return FloatSetVal::ai(u);
843 }
844 default:
845 throw EvalError(env, e->loc(), "not a set of int expression", bo->opToString());
846 }
847 } else if (lhs->type().isfloat() && rhs->type().isfloat()) {
848 if (bo->op() != BOT_DOTDOT)
849 throw EvalError(env, e->loc(), "not a set of float expression", bo->opToString());
850 return FloatSetVal::a(eval_float(env, lhs), eval_float(env, rhs));
851 } else {
852 throw EvalError(env, e->loc(), "not a set of float expression", bo->opToString());
853 }
854 } break;
855 case Expression::E_UNOP: {
856 UnOp* uo = e->cast<UnOp>();
857 if (uo->decl() && uo->decl()->e()) {
858 return eval_call<EvalFloatSet, UnOp>(env, uo);
859 }
860 throw EvalError(env, e->loc(), "not a set of float expression");
861 }
862 case Expression::E_CALL: {
863 Call* ce = e->cast<Call>();
864 if (ce->decl() == NULL) throw EvalError(env, e->loc(), "undeclared function", ce->id());
865
866 if (ce->decl()->_builtins.e) return eval_floatset(env, ce->decl()->_builtins.e(env, ce));
867
868 if (ce->decl()->e() == NULL)
869 throw EvalError(env, ce->loc(), "internal error: missing builtin '" + ce->id().str() + "'");
870
871 return eval_call<EvalFloatSet>(env, ce);
872 } break;
873 case Expression::E_LET: {
874 Let* l = e->cast<Let>();
875 l->pushbindings();
876 for (unsigned int i = 0; i < l->let().size(); i++) {
877 // Evaluate all variable declarations
878 if (VarDecl* vdi = l->let()[i]->dyn_cast<VarDecl>()) {
879 vdi->e(eval_par(env, vdi->e()));
880 if (vdi->ti()->domain()) {
881 if (!checkParDomain(env, vdi->e(), vdi->ti()->domain())) {
882 throw ResultUndefinedError(env, l->let()[i]->loc(),
883 "domain constraint in let failed");
884 }
885 }
886 } else {
887 // This is a constraint item. Since the let is par,
888 // it can only be a par bool expression. If it evaluates
889 // to false, it means that the value of this let is undefined.
890 if (!eval_bool(env, l->let()[i])) {
891 throw ResultUndefinedError(env, l->let()[i]->loc(), "constraint in let failed");
892 }
893 }
894 }
895 FloatSetVal* ret = eval_floatset(env, l->in());
896 l->popbindings();
897 return ret;
898 } break;
899 default:
900 assert(false);
901 return NULL;
902 }
903}
904
905bool eval_bool(EnvI& env, Expression* e) {
906 CallStackItem csi(env, e);
907 try {
908 if (BoolLit* bl = e->dyn_cast<BoolLit>()) {
909 return bl->v();
910 }
911 CallStackItem csi(env, e);
912 switch (e->eid()) {
913 case Expression::E_INTLIT:
914 case Expression::E_FLOATLIT:
915 case Expression::E_STRINGLIT:
916 case Expression::E_ANON:
917 case Expression::E_TIID:
918 case Expression::E_SETLIT:
919 case Expression::E_ARRAYLIT:
920 case Expression::E_COMP:
921 case Expression::E_VARDECL:
922 case Expression::E_TI:
923 assert(false);
924 throw EvalError(env, e->loc(), "not a bool expression");
925 break;
926 case Expression::E_ID: {
927 GCLock lock;
928 return eval_id<EvalBoolLit>(env, e)->v();
929 } break;
930 case Expression::E_ARRAYACCESS: {
931 GCLock lock;
932 return eval_bool(env, eval_arrayaccess(env, e->cast<ArrayAccess>()));
933 } break;
934 case Expression::E_ITE: {
935 ITE* ite = e->cast<ITE>();
936 for (int i = 0; i < ite->size(); i++) {
937 if (eval_bool(env, ite->e_if(i))) return eval_bool(env, ite->e_then(i));
938 }
939 return eval_bool(env, ite->e_else());
940 } break;
941 case Expression::E_BINOP: {
942 BinOp* bo = e->cast<BinOp>();
943 Expression* lhs = bo->lhs();
944 if (lhs->type().bt() == Type::BT_TOP) lhs = eval_par(env, lhs);
945 Expression* rhs = bo->rhs();
946 if (rhs->type().bt() == Type::BT_TOP) rhs = eval_par(env, rhs);
947 if (bo->op() == BOT_EQ && (lhs->type().isopt() || rhs->type().isopt())) {
948 if (lhs == constants().absent || rhs == constants().absent) return lhs == rhs;
949 }
950 if (bo->decl() && bo->decl()->e()) {
951 return eval_call<EvalBoolVal, BinOp>(env, bo);
952 }
953
954 if (lhs->type().isbool() && rhs->type().isbool()) {
955 try {
956 switch (bo->op()) {
957 case BOT_LE:
958 return eval_bool(env, lhs) < eval_bool(env, rhs);
959 case BOT_LQ:
960 return eval_bool(env, lhs) <= eval_bool(env, rhs);
961 case BOT_GR:
962 return eval_bool(env, lhs) > eval_bool(env, rhs);
963 case BOT_GQ:
964 return eval_bool(env, lhs) >= eval_bool(env, rhs);
965 case BOT_EQ:
966 return eval_bool(env, lhs) == eval_bool(env, rhs);
967 case BOT_NQ:
968 return eval_bool(env, lhs) != eval_bool(env, rhs);
969 case BOT_EQUIV:
970 return eval_bool(env, lhs) == eval_bool(env, rhs);
971 case BOT_IMPL:
972 return (!eval_bool(env, lhs)) || eval_bool(env, rhs);
973 case BOT_RIMPL:
974 return (!eval_bool(env, rhs)) || eval_bool(env, lhs);
975 case BOT_OR:
976 return eval_bool(env, lhs) || eval_bool(env, rhs);
977 case BOT_AND:
978 return eval_bool(env, lhs) && eval_bool(env, rhs);
979 case BOT_XOR:
980 return eval_bool(env, lhs) ^ eval_bool(env, rhs);
981 default:
982 assert(false);
983 throw EvalError(env, e->loc(), "not a bool expression", bo->opToString());
984 }
985 } catch (ResultUndefinedError&) {
986 return false;
987 }
988 } else if (lhs->type().isint() && rhs->type().isint()) {
989 try {
990 IntVal v0 = eval_int(env, lhs);
991 IntVal v1 = eval_int(env, rhs);
992 switch (bo->op()) {
993 case BOT_LE:
994 return v0 < v1;
995 case BOT_LQ:
996 return v0 <= v1;
997 case BOT_GR:
998 return v0 > v1;
999 case BOT_GQ:
1000 return v0 >= v1;
1001 case BOT_EQ:
1002 return v0 == v1;
1003 case BOT_NQ:
1004 return v0 != v1;
1005 default:
1006 assert(false);
1007 throw EvalError(env, e->loc(), "not a bool expression", bo->opToString());
1008 }
1009 } catch (ResultUndefinedError&) {
1010 return false;
1011 }
1012 } else if (lhs->type().isfloat() && rhs->type().isfloat()) {
1013 try {
1014 FloatVal v0 = eval_float(env, lhs);
1015 FloatVal v1 = eval_float(env, rhs);
1016 switch (bo->op()) {
1017 case BOT_LE:
1018 return v0 < v1;
1019 case BOT_LQ:
1020 return v0 <= v1;
1021 case BOT_GR:
1022 return v0 > v1;
1023 case BOT_GQ:
1024 return v0 >= v1;
1025 case BOT_EQ:
1026 return v0 == v1;
1027 case BOT_NQ:
1028 return v0 != v1;
1029 default:
1030 assert(false);
1031 throw EvalError(env, e->loc(), "not a bool expression", bo->opToString());
1032 }
1033 } catch (ResultUndefinedError&) {
1034 return false;
1035 }
1036 } else if (lhs->type().isint() && rhs->type().isintset()) {
1037 try {
1038 IntVal v0 = eval_int(env, lhs);
1039 GCLock lock;
1040 IntSetVal* v1 = eval_intset(env, rhs);
1041 switch (bo->op()) {
1042 case BOT_IN:
1043 return v1->contains(v0);
1044 default:
1045 assert(false);
1046 throw EvalError(env, e->loc(), "not a bool expression", bo->opToString());
1047 }
1048 } catch (ResultUndefinedError&) {
1049 return false;
1050 }
1051 } else if (lhs->type().isfloat() && rhs->type().isfloatset()) {
1052 try {
1053 FloatVal v0 = eval_float(env, lhs);
1054 GCLock lock;
1055 FloatSetVal* v1 = eval_floatset(env, rhs);
1056 switch (bo->op()) {
1057 case BOT_IN:
1058 return v1->contains(v0);
1059 default:
1060 assert(false);
1061 throw EvalError(env, e->loc(), "not a bool expression", bo->opToString());
1062 }
1063 } catch (ResultUndefinedError&) {
1064 return false;
1065 }
1066 } else if (lhs->type().is_set() && rhs->type().is_set()) {
1067 try {
1068 GCLock lock;
1069 IntSetVal* v0 = eval_intset(env, lhs);
1070 IntSetVal* v1 = eval_intset(env, rhs);
1071 IntSetRanges ir0(v0);
1072 IntSetRanges ir1(v1);
1073 switch (bo->op()) {
1074 case BOT_LE:
1075 return Ranges::less(ir0, ir1);
1076 case BOT_LQ:
1077 return Ranges::lessEq(ir0, ir1);
1078 case BOT_GR:
1079 return Ranges::less(ir1, ir0);
1080 case BOT_GQ:
1081 return Ranges::lessEq(ir1, ir0);
1082 case BOT_EQ:
1083 return Ranges::equal(ir0, ir1);
1084 case BOT_NQ:
1085 return !Ranges::equal(ir0, ir1);
1086 case BOT_SUBSET:
1087 return Ranges::subset(ir0, ir1);
1088 case BOT_SUPERSET:
1089 return Ranges::subset(ir1, ir0);
1090 default:
1091 throw EvalError(env, e->loc(), "not a bool expression", bo->opToString());
1092 }
1093 } catch (ResultUndefinedError&) {
1094 return false;
1095 }
1096 } else if (lhs->type().isstring() && rhs->type().isstring()) {
1097 try {
1098 GCLock lock;
1099 std::string s0 = eval_string(env, lhs);
1100 std::string s1 = eval_string(env, rhs);
1101 switch (bo->op()) {
1102 case BOT_EQ:
1103 return s0 == s1;
1104 case BOT_NQ:
1105 return s0 != s1;
1106 case BOT_LE:
1107 return s0 < s1;
1108 case BOT_LQ:
1109 return s0 <= s1;
1110 case BOT_GR:
1111 return s0 > s1;
1112 case BOT_GQ:
1113 return s0 >= s1;
1114 default:
1115 throw EvalError(env, e->loc(), "not a bool expression", bo->opToString());
1116 }
1117 } catch (ResultUndefinedError&) {
1118 return false;
1119 }
1120 } else if (bo->op() == BOT_EQ && lhs->type().isann()) {
1121 return Expression::equal(lhs, rhs);
1122 } else if (bo->op() == BOT_EQ && lhs->type().dim() > 0 && rhs->type().dim() > 0) {
1123 try {
1124 ArrayLit* al0 = eval_array_lit(env, lhs);
1125 ArrayLit* al1 = eval_array_lit(env, rhs);
1126 if (al0->size() != al1->size()) return false;
1127 for (unsigned int i = 0; i < al0->size(); i++) {
1128 if (!Expression::equal(eval_par(env, (*al0)[i]), eval_par(env, (*al1)[i]))) {
1129 return false;
1130 }
1131 }
1132 return true;
1133 } catch (ResultUndefinedError&) {
1134 return false;
1135 }
1136 } else {
1137 throw EvalError(env, e->loc(), "not a bool expression", bo->opToString());
1138 }
1139 } break;
1140 case Expression::E_UNOP: {
1141 UnOp* uo = e->cast<UnOp>();
1142 if (uo->decl() && uo->decl()->e()) {
1143 return eval_call<EvalBoolVal, UnOp>(env, uo);
1144 }
1145 bool v0 = eval_bool(env, uo->e());
1146 switch (uo->op()) {
1147 case UOT_NOT:
1148 return !v0;
1149 default:
1150 assert(false);
1151 throw EvalError(env, e->loc(), "not a bool expression", uo->opToString());
1152 }
1153 } break;
1154 case Expression::E_CALL: {
1155 try {
1156 Call* ce = e->cast<Call>();
1157 if (ce->decl() == NULL) throw EvalError(env, e->loc(), "undeclared function", ce->id());
1158
1159 if (ce->decl()->_builtins.b) return ce->decl()->_builtins.b(env, ce);
1160
1161 if (ce->decl()->_builtins.e) return eval_bool(env, ce->decl()->_builtins.e(env, ce));
1162
1163 if (ce->decl()->e() == NULL)
1164 throw EvalError(env, ce->loc(),
1165 "internal error: missing builtin '" + ce->id().str() + "'");
1166
1167 return eval_call<EvalBoolVal>(env, ce);
1168 } catch (ResultUndefinedError&) {
1169 return false;
1170 }
1171 } break;
1172 case Expression::E_LET: {
1173 Let* l = e->cast<Let>();
1174 l->pushbindings();
1175 bool ret = true;
1176 for (unsigned int i = 0; i < l->let().size(); i++) {
1177 // Evaluate all variable declarations
1178 if (VarDecl* vdi = l->let()[i]->dyn_cast<VarDecl>()) {
1179 vdi->e(eval_par(env, vdi->e()));
1180 if (vdi->ti()->domain()) {
1181 if (!checkParDomain(env, vdi->e(), vdi->ti()->domain())) {
1182 if (vdi->ann().contains(constants().ann.maybe_partial)) {
1183 ret = false;
1184 } else {
1185 throw ResultUndefinedError(env, l->let()[i]->loc(),
1186 "domain constraint in let failed");
1187 }
1188 }
1189 }
1190 } else {
1191 // This is a constraint item. Since the let is par,
1192 // it can only be a par bool expression. If it evaluates
1193 // to false, it means that the value of this let is false.
1194 if (!eval_bool(env, l->let()[i])) {
1195 if (l->let()[i]->ann().contains(constants().ann.maybe_partial)) {
1196 ret = false;
1197 } else {
1198 throw ResultUndefinedError(env, l->let()[i]->loc(),
1199 "domain constraint in let failed");
1200 }
1201 }
1202 }
1203 }
1204 ret = ret && eval_bool(env, l->in());
1205 l->popbindings();
1206 return ret;
1207 } break;
1208 default:
1209 assert(false);
1210 return false;
1211 }
1212 } catch (ResultUndefinedError&) {
1213 // undefined means false
1214 return false;
1215 }
1216}
1217
1218IntSetVal* eval_boolset(EnvI& env, Expression* e) {
1219 CallStackItem csi(env, e);
1220 switch (e->eid()) {
1221 case Expression::E_SETLIT: {
1222 SetLit* sl = e->cast<SetLit>();
1223 if (sl->isv()) return sl->isv();
1224 std::vector<IntVal> vals(sl->v().size());
1225 for (unsigned int i = 0; i < sl->v().size(); i++) vals[i] = eval_bool(env, sl->v()[i]);
1226 return IntSetVal::a(vals);
1227 }
1228 case Expression::E_BOOLLIT:
1229 case Expression::E_INTLIT:
1230 case Expression::E_FLOATLIT:
1231 case Expression::E_STRINGLIT:
1232 case Expression::E_ANON:
1233 case Expression::E_TIID:
1234 case Expression::E_VARDECL:
1235 case Expression::E_TI:
1236 throw EvalError(env, e->loc(), "not a set of bool expression");
1237 break;
1238 case Expression::E_ARRAYLIT: {
1239 ArrayLit* al = e->cast<ArrayLit>();
1240 std::vector<IntVal> vals(al->size());
1241 for (unsigned int i = 0; i < al->size(); i++) vals[i] = eval_bool(env, (*al)[i]);
1242 return IntSetVal::a(vals);
1243 } break;
1244 case Expression::E_COMP: {
1245 Comprehension* c = e->cast<Comprehension>();
1246 std::vector<IntVal> a = eval_comp<EvalIntVal>(env, c);
1247 return IntSetVal::a(a);
1248 }
1249 case Expression::E_ID: {
1250 GCLock lock;
1251 return eval_id<EvalBoolSetLit>(env, e)->isv();
1252 } break;
1253 case Expression::E_ARRAYACCESS: {
1254 GCLock lock;
1255 return eval_boolset(env, eval_arrayaccess(env, e->cast<ArrayAccess>()));
1256 } break;
1257 case Expression::E_ITE: {
1258 ITE* ite = e->cast<ITE>();
1259 for (int i = 0; i < ite->size(); i++) {
1260 if (eval_bool(env, ite->e_if(i))) return eval_boolset(env, ite->e_then(i));
1261 }
1262 return eval_boolset(env, ite->e_else());
1263 } break;
1264 case Expression::E_BINOP: {
1265 BinOp* bo = e->cast<BinOp>();
1266 if (bo->decl() && bo->decl()->e()) {
1267 return eval_call<EvalBoolSet, BinOp>(env, bo);
1268 }
1269 Expression* lhs = eval_par(env, bo->lhs());
1270 Expression* rhs = eval_par(env, bo->rhs());
1271 if (lhs->type().isintset() && rhs->type().isintset()) {
1272 IntSetVal* v0 = eval_boolset(env, lhs);
1273 IntSetVal* v1 = eval_boolset(env, rhs);
1274 IntSetRanges ir0(v0);
1275 IntSetRanges ir1(v1);
1276 switch (bo->op()) {
1277 case BOT_UNION: {
1278 Ranges::Union<IntVal, IntSetRanges, IntSetRanges> u(ir0, ir1);
1279 return IntSetVal::ai(u);
1280 }
1281 case BOT_DIFF: {
1282 Ranges::Diff<IntVal, IntSetRanges, IntSetRanges> u(ir0, ir1);
1283 return IntSetVal::ai(u);
1284 }
1285 case BOT_SYMDIFF: {
1286 Ranges::Union<IntVal, IntSetRanges, IntSetRanges> u(ir0, ir1);
1287 Ranges::Inter<IntVal, IntSetRanges, IntSetRanges> i(ir0, ir1);
1288 Ranges::Diff<IntVal, Ranges::Union<IntVal, IntSetRanges, IntSetRanges>,
1289 Ranges::Inter<IntVal, IntSetRanges, IntSetRanges>>
1290 sd(u, i);
1291 return IntSetVal::ai(sd);
1292 }
1293 case BOT_INTERSECT: {
1294 Ranges::Inter<IntVal, IntSetRanges, IntSetRanges> u(ir0, ir1);
1295 return IntSetVal::ai(u);
1296 }
1297 default:
1298 throw EvalError(env, e->loc(), "not a set of bool expression", bo->opToString());
1299 }
1300 } else if (lhs->type().isbool() && rhs->type().isbool()) {
1301 if (bo->op() != BOT_DOTDOT)
1302 throw EvalError(env, e->loc(), "not a set of bool expression", bo->opToString());
1303 return IntSetVal::a(eval_bool(env, lhs), eval_bool(env, rhs));
1304 } else {
1305 throw EvalError(env, e->loc(), "not a set of bool expression", bo->opToString());
1306 }
1307 } break;
1308 case Expression::E_UNOP: {
1309 UnOp* uo = e->cast<UnOp>();
1310 if (uo->decl() && uo->decl()->e()) {
1311 return eval_call<EvalBoolSet, UnOp>(env, uo);
1312 }
1313 throw EvalError(env, e->loc(), "not a set of bool expression");
1314 }
1315 case Expression::E_CALL: {
1316 Call* ce = e->cast<Call>();
1317 if (ce->decl() == NULL) throw EvalError(env, e->loc(), "undeclared function", ce->id());
1318
1319 if (ce->decl()->_builtins.s) return ce->decl()->_builtins.s(env, ce);
1320
1321 if (ce->decl()->_builtins.e) return eval_boolset(env, ce->decl()->_builtins.e(env, ce));
1322
1323 if (ce->decl()->e() == NULL)
1324 throw EvalError(env, ce->loc(), "internal error: missing builtin '" + ce->id().str() + "'");
1325
1326 return eval_call<EvalBoolSet>(env, ce);
1327 } break;
1328 case Expression::E_LET: {
1329 Let* l = e->cast<Let>();
1330 l->pushbindings();
1331 for (unsigned int i = 0; i < l->let().size(); i++) {
1332 // Evaluate all variable declarations
1333 if (VarDecl* vdi = l->let()[i]->dyn_cast<VarDecl>()) {
1334 vdi->e(eval_par(env, vdi->e()));
1335 if (vdi->ti()->domain()) {
1336 if (!checkParDomain(env, vdi->e(), vdi->ti()->domain())) {
1337 throw ResultUndefinedError(env, l->let()[i]->loc(),
1338 "domain constraint in let failed");
1339 }
1340 }
1341 } else {
1342 // This is a constraint item. Since the let is par,
1343 // it can only be a par bool expression. If it evaluates
1344 // to false, it means that the value of this let is undefined.
1345 if (!eval_bool(env, l->let()[i])) {
1346 throw ResultUndefinedError(env, l->let()[i]->loc(), "constraint in let failed");
1347 }
1348 }
1349 }
1350 IntSetVal* ret = eval_boolset(env, l->in());
1351 l->popbindings();
1352 return ret;
1353 } break;
1354 default:
1355 assert(false);
1356 return NULL;
1357 }
1358}
1359
1360IntVal eval_int(EnvI& env, Expression* e) {
1361 if (e->type().isbool()) {
1362 return eval_bool(env, e);
1363 }
1364 if (IntLit* il = e->dyn_cast<IntLit>()) {
1365 return il->v();
1366 }
1367 CallStackItem csi(env, e);
1368 try {
1369 switch (e->eid()) {
1370 case Expression::E_FLOATLIT:
1371 case Expression::E_BOOLLIT:
1372 case Expression::E_STRINGLIT:
1373 case Expression::E_ANON:
1374 case Expression::E_TIID:
1375 case Expression::E_SETLIT:
1376 case Expression::E_ARRAYLIT:
1377 case Expression::E_COMP:
1378 case Expression::E_VARDECL:
1379 case Expression::E_TI:
1380 throw EvalError(env, e->loc(), "not an integer expression");
1381 break;
1382 case Expression::E_ID: {
1383 GCLock lock;
1384 return eval_id<EvalIntLit>(env, e)->v();
1385 } break;
1386 case Expression::E_ARRAYACCESS: {
1387 GCLock lock;
1388 return eval_int(env, eval_arrayaccess(env, e->cast<ArrayAccess>()));
1389 } break;
1390 case Expression::E_ITE: {
1391 ITE* ite = e->cast<ITE>();
1392 for (int i = 0; i < ite->size(); i++) {
1393 if (eval_bool(env, ite->e_if(i))) return eval_int(env, ite->e_then(i));
1394 }
1395 return eval_int(env, ite->e_else());
1396 } break;
1397 case Expression::E_BINOP: {
1398 BinOp* bo = e->cast<BinOp>();
1399 if (bo->decl() && bo->decl()->e()) {
1400 return eval_call<EvalIntVal, BinOp>(env, bo);
1401 }
1402 IntVal v0 = eval_int(env, bo->lhs());
1403 IntVal v1 = eval_int(env, bo->rhs());
1404 switch (bo->op()) {
1405 case BOT_PLUS:
1406 return v0 + v1;
1407 case BOT_MINUS:
1408 return v0 - v1;
1409 case BOT_MULT:
1410 return v0 * v1;
1411 case BOT_POW:
1412 return v0.pow(v1);
1413 case BOT_IDIV:
1414 if (v1 == 0) throw ResultUndefinedError(env, e->loc(), "division by zero");
1415 return v0 / v1;
1416 case BOT_MOD:
1417 if (v1 == 0) throw ResultUndefinedError(env, e->loc(), "division by zero");
1418 return v0 % v1;
1419 default:
1420 throw EvalError(env, e->loc(), "not an integer expression", bo->opToString());
1421 }
1422 } break;
1423 case Expression::E_UNOP: {
1424 UnOp* uo = e->cast<UnOp>();
1425 if (uo->decl() && uo->decl()->e()) {
1426 return eval_call<EvalIntVal, UnOp>(env, uo);
1427 }
1428 IntVal v0 = eval_int(env, uo->e());
1429 switch (uo->op()) {
1430 case UOT_PLUS:
1431 return v0;
1432 case UOT_MINUS:
1433 return -v0;
1434 default:
1435 throw EvalError(env, e->loc(), "not an integer expression", uo->opToString());
1436 }
1437 } break;
1438 case Expression::E_CALL: {
1439 Call* ce = e->cast<Call>();
1440 if (ce->decl() == NULL) throw EvalError(env, e->loc(), "undeclared function", ce->id());
1441 if (ce->decl()->_builtins.i) return ce->decl()->_builtins.i(env, ce);
1442
1443 if (ce->decl()->_builtins.e) return eval_int(env, ce->decl()->_builtins.e(env, ce));
1444
1445 if (ce->decl()->e() == NULL)
1446 throw EvalError(env, ce->loc(),
1447 "internal error: missing builtin '" + ce->id().str() + "'");
1448
1449 return eval_call<EvalIntVal>(env, ce);
1450 } break;
1451 case Expression::E_LET: {
1452 Let* l = e->cast<Let>();
1453 l->pushbindings();
1454 for (unsigned int i = 0; i < l->let().size(); i++) {
1455 // Evaluate all variable declarations
1456 if (VarDecl* vdi = l->let()[i]->dyn_cast<VarDecl>()) {
1457 vdi->e(eval_par(env, vdi->e()));
1458 if (vdi->ti()->domain()) {
1459 if (!checkParDomain(env, vdi->e(), vdi->ti()->domain())) {
1460 throw ResultUndefinedError(env, l->let()[i]->loc(),
1461 "domain constraint in let failed");
1462 }
1463 }
1464 } else {
1465 // This is a constraint item. Since the let is par,
1466 // it can only be a par bool expression. If it evaluates
1467 // to false, it means that the value of this let is undefined.
1468 if (!eval_bool(env, l->let()[i])) {
1469 throw ResultUndefinedError(env, l->let()[i]->loc(), "constraint in let failed");
1470 }
1471 }
1472 }
1473 IntVal ret = eval_int(env, l->in());
1474 l->popbindings();
1475 return ret;
1476 } break;
1477 default:
1478 assert(false);
1479 return 0;
1480 }
1481 } catch (ArithmeticError& err) {
1482 throw EvalError(env, e->loc(), err.msg());
1483 }
1484}
1485
1486FloatVal eval_float(EnvI& env, Expression* e) {
1487 CallStackItem csi(env, e);
1488 try {
1489 if (e->type().isint()) {
1490 return FloatVal(eval_int(env, e).toInt());
1491 } else if (e->type().isbool()) {
1492 return eval_bool(env, e);
1493 }
1494 if (FloatLit* fl = e->dyn_cast<FloatLit>()) {
1495 return fl->v();
1496 }
1497 CallStackItem csi(env, e);
1498 switch (e->eid()) {
1499 case Expression::E_INTLIT:
1500 case Expression::E_BOOLLIT:
1501 case Expression::E_STRINGLIT:
1502 case Expression::E_ANON:
1503 case Expression::E_TIID:
1504 case Expression::E_SETLIT:
1505 case Expression::E_ARRAYLIT:
1506 case Expression::E_COMP:
1507 case Expression::E_VARDECL:
1508 case Expression::E_TI:
1509 throw EvalError(env, e->loc(), "not a float expression");
1510 break;
1511 case Expression::E_ID: {
1512 GCLock lock;
1513 return eval_id<EvalFloatLit>(env, e)->v();
1514 } break;
1515 case Expression::E_ARRAYACCESS: {
1516 GCLock lock;
1517 return eval_float(env, eval_arrayaccess(env, e->cast<ArrayAccess>()));
1518 } break;
1519 case Expression::E_ITE: {
1520 ITE* ite = e->cast<ITE>();
1521 for (int i = 0; i < ite->size(); i++) {
1522 if (eval_bool(env, ite->e_if(i))) return eval_float(env, ite->e_then(i));
1523 }
1524 return eval_float(env, ite->e_else());
1525 } break;
1526 case Expression::E_BINOP: {
1527 BinOp* bo = e->cast<BinOp>();
1528 if (bo->decl() && bo->decl()->e()) {
1529 return eval_call<EvalFloatVal, BinOp>(env, bo);
1530 }
1531 FloatVal v0 = eval_float(env, bo->lhs());
1532 FloatVal v1 = eval_float(env, bo->rhs());
1533 switch (bo->op()) {
1534 case BOT_PLUS:
1535 return v0 + v1;
1536 case BOT_MINUS:
1537 return v0 - v1;
1538 case BOT_MULT:
1539 return v0 * v1;
1540 case BOT_POW:
1541 return std::pow(v0.toDouble(), v1.toDouble());
1542 case BOT_DIV:
1543 if (v1 == 0.0) throw ResultUndefinedError(env, e->loc(), "division by zero");
1544 return v0 / v1;
1545 default:
1546 throw EvalError(env, e->loc(), "not a float expression", bo->opToString());
1547 }
1548 } break;
1549 case Expression::E_UNOP: {
1550 UnOp* uo = e->cast<UnOp>();
1551 if (uo->decl() && uo->decl()->e()) {
1552 return eval_call<EvalFloatVal, UnOp>(env, uo);
1553 }
1554 FloatVal v0 = eval_float(env, uo->e());
1555 switch (uo->op()) {
1556 case UOT_PLUS:
1557 return v0;
1558 case UOT_MINUS:
1559 return -v0;
1560 default:
1561 throw EvalError(env, e->loc(), "not a float expression", uo->opToString());
1562 }
1563 } break;
1564 case Expression::E_CALL: {
1565 Call* ce = e->cast<Call>();
1566 if (ce->decl() == NULL) throw EvalError(env, e->loc(), "undeclared function", ce->id());
1567 if (ce->decl()->_builtins.f) return ce->decl()->_builtins.f(env, ce);
1568
1569 if (ce->decl()->_builtins.e) return eval_float(env, ce->decl()->_builtins.e(env, ce));
1570
1571 if (ce->decl()->e() == NULL)
1572 throw EvalError(env, ce->loc(),
1573 "internal error: missing builtin '" + ce->id().str() + "'");
1574
1575 return eval_call<EvalFloatVal>(env, ce);
1576 } break;
1577 case Expression::E_LET: {
1578 Let* l = e->cast<Let>();
1579 l->pushbindings();
1580 for (unsigned int i = 0; i < l->let().size(); i++) {
1581 // Evaluate all variable declarations
1582 if (VarDecl* vdi = l->let()[i]->dyn_cast<VarDecl>()) {
1583 vdi->e(eval_par(env, vdi->e()));
1584 if (vdi->ti()->domain()) {
1585 if (!checkParDomain(env, vdi->e(), vdi->ti()->domain())) {
1586 throw ResultUndefinedError(env, l->let()[i]->loc(),
1587 "domain constraint in let failed");
1588 }
1589 }
1590 } else {
1591 // This is a constraint item. Since the let is par,
1592 // it can only be a par bool expression. If it evaluates
1593 // to false, it means that the value of this let is undefined.
1594 if (!eval_bool(env, l->let()[i])) {
1595 throw ResultUndefinedError(env, l->let()[i]->loc(), "constraint in let failed");
1596 }
1597 }
1598 }
1599 FloatVal ret = eval_float(env, l->in());
1600 l->popbindings();
1601 return ret;
1602 } break;
1603 default:
1604 assert(false);
1605 return 0.0;
1606 }
1607 } catch (ArithmeticError& err) {
1608 throw EvalError(env, e->loc(), err.msg());
1609 }
1610}
1611
1612std::string eval_string(EnvI& env, Expression* e) {
1613 CallStackItem csi(env, e);
1614 switch (e->eid()) {
1615 case Expression::E_STRINGLIT:
1616 return e->cast<StringLit>()->v().str();
1617 case Expression::E_FLOATLIT:
1618 case Expression::E_INTLIT:
1619 case Expression::E_BOOLLIT:
1620 case Expression::E_ANON:
1621 case Expression::E_TIID:
1622 case Expression::E_SETLIT:
1623 case Expression::E_ARRAYLIT:
1624 case Expression::E_COMP:
1625 case Expression::E_VARDECL:
1626 case Expression::E_TI:
1627 throw EvalError(env, e->loc(), "not a string expression");
1628 break;
1629 case Expression::E_ID: {
1630 GCLock lock;
1631 return eval_id<EvalStringLit>(env, e)->v().str();
1632 } break;
1633 case Expression::E_ARRAYACCESS: {
1634 GCLock lock;
1635 return eval_string(env, eval_arrayaccess(env, e->cast<ArrayAccess>()));
1636 } break;
1637 case Expression::E_ITE: {
1638 ITE* ite = e->cast<ITE>();
1639 for (int i = 0; i < ite->size(); i++) {
1640 if (eval_bool(env, ite->e_if(i))) return eval_string(env, ite->e_then(i));
1641 }
1642 return eval_string(env, ite->e_else());
1643 } break;
1644 case Expression::E_BINOP: {
1645 BinOp* bo = e->cast<BinOp>();
1646 if (bo->decl() && bo->decl()->e()) {
1647 return eval_call<EvalString, BinOp>(env, bo);
1648 }
1649 std::string v0 = eval_string(env, bo->lhs());
1650 std::string v1 = eval_string(env, bo->rhs());
1651 switch (bo->op()) {
1652 case BOT_PLUSPLUS:
1653 return v0 + v1;
1654 default:
1655 throw EvalError(env, e->loc(), "not a string expression", bo->opToString());
1656 }
1657 } break;
1658 case Expression::E_UNOP: {
1659 UnOp* uo = e->cast<UnOp>();
1660 if (uo->decl() && uo->decl()->e()) {
1661 return eval_call<EvalString, UnOp>(env, uo);
1662 }
1663 throw EvalError(env, e->loc(), "not a string expression");
1664 } break;
1665 case Expression::E_CALL: {
1666 Call* ce = e->cast<Call>();
1667 if (ce->decl() == NULL) throw EvalError(env, e->loc(), "undeclared function", ce->id());
1668
1669 if (ce->decl()->_builtins.str) return ce->decl()->_builtins.str(env, ce);
1670 if (ce->decl()->_builtins.e) return eval_string(env, ce->decl()->_builtins.e(env, ce));
1671
1672 if (ce->decl()->e() == NULL)
1673 throw EvalError(env, ce->loc(), "internal error: missing builtin '" + ce->id().str() + "'");
1674
1675 return eval_call<EvalString>(env, ce);
1676 } break;
1677 case Expression::E_LET: {
1678 Let* l = e->cast<Let>();
1679 l->pushbindings();
1680 for (unsigned int i = 0; i < l->let().size(); i++) {
1681 // Evaluate all variable declarations
1682 if (VarDecl* vdi = l->let()[i]->dyn_cast<VarDecl>()) {
1683 vdi->e(eval_par(env, vdi->e()));
1684 if (vdi->ti()->domain()) {
1685 if (!checkParDomain(env, vdi->e(), vdi->ti()->domain())) {
1686 throw ResultUndefinedError(env, l->let()[i]->loc(),
1687 "domain constraint in let failed");
1688 }
1689 }
1690 } else {
1691 // This is a constraint item. Since the let is par,
1692 // it can only be a par bool expression. If it evaluates
1693 // to false, it means that the value of this let is undefined.
1694 if (!eval_bool(env, l->let()[i])) {
1695 throw ResultUndefinedError(env, l->let()[i]->loc(), "constraint in let failed");
1696 }
1697 }
1698 }
1699 std::string ret = eval_string(env, l->in());
1700 l->popbindings();
1701 return ret;
1702 } break;
1703 default:
1704 assert(false);
1705 return NULL;
1706 }
1707}
1708
1709Expression* eval_par(EnvI& env, Expression* e) {
1710 if (e == NULL) return NULL;
1711 switch (e->eid()) {
1712 case Expression::E_ANON:
1713 case Expression::E_TIID: {
1714 return e;
1715 }
1716 case Expression::E_COMP:
1717 if (e->cast<Comprehension>()->set()) return EvalSetLit::e(env, e);
1718 // fall through
1719 case Expression::E_ARRAYLIT: {
1720 ArrayLit* al = eval_array_lit(env, e);
1721 std::vector<Expression*> args(al->size());
1722 for (unsigned int i = al->size(); i--;) args[i] = eval_par(env, (*al)[i]);
1723 std::vector<std::pair<int, int>> dims(al->dims());
1724 for (unsigned int i = al->dims(); i--;) {
1725 dims[i].first = al->min(i);
1726 dims[i].second = al->max(i);
1727 }
1728 ArrayLit* ret = new ArrayLit(al->loc(), args, dims);
1729 Type t = al->type();
1730 if (t.isbot() && ret->size() > 0) {
1731 t.bt((*ret)[0]->type().bt());
1732 }
1733 ret->type(t);
1734 return ret;
1735 }
1736 case Expression::E_VARDECL: {
1737 VarDecl* vd = e->cast<VarDecl>();
1738 throw EvalError(env, vd->loc(), "cannot evaluate variable declaration", vd->id()->v());
1739 }
1740 case Expression::E_TI: {
1741 TypeInst* t = e->cast<TypeInst>();
1742 ASTExprVec<TypeInst> r;
1743 if (t->ranges().size() > 0) {
1744 std::vector<TypeInst*> rv(t->ranges().size());
1745 for (unsigned int i = t->ranges().size(); i--;)
1746 rv[i] = static_cast<TypeInst*>(eval_par(env, t->ranges()[i]));
1747 r = ASTExprVec<TypeInst>(rv);
1748 }
1749 return new TypeInst(Location(), t->type(), r, eval_par(env, t->domain()));
1750 }
1751 case Expression::E_ID: {
1752 if (e == constants().absent) return e;
1753 Id* id = e->cast<Id>();
1754 if (id->decl() == NULL) throw EvalError(env, e->loc(), "undefined identifier", id->v());
1755 if (id->decl()->ti()->domain()) {
1756 if (BoolLit* bl = id->decl()->ti()->domain()->dyn_cast<BoolLit>()) return bl;
1757 if (id->decl()->ti()->type().isint()) {
1758 if (SetLit* sl = id->decl()->ti()->domain()->dyn_cast<SetLit>()) {
1759 if (sl->isv() && sl->isv()->min() == sl->isv()->max()) {
1760 return IntLit::a(sl->isv()->min());
1761 }
1762 }
1763 } else if (id->decl()->ti()->type().isfloat()) {
1764 if (id->decl()->ti()->domain()) {
1765 FloatSetVal* fsv = eval_floatset(env, id->decl()->ti()->domain());
1766 if (fsv->min() == fsv->max()) {
1767 return FloatLit::a(fsv->min());
1768 }
1769 }
1770 }
1771 }
1772 if (id->decl()->e() == NULL) {
1773 return id;
1774 } else {
1775 return eval_par(env, id->decl()->e());
1776 }
1777 }
1778 case Expression::E_STRINGLIT:
1779 return e;
1780 default: {
1781 if (e->type().dim() != 0) {
1782 ArrayLit* al = eval_array_lit(env, e);
1783 std::vector<Expression*> args(al->size());
1784 for (unsigned int i = al->size(); i--;) args[i] = eval_par(env, (*al)[i]);
1785 std::vector<std::pair<int, int>> dims(al->dims());
1786 for (unsigned int i = al->dims(); i--;) {
1787 dims[i].first = al->min(i);
1788 dims[i].second = al->max(i);
1789 }
1790 ArrayLit* ret = new ArrayLit(al->loc(), args, dims);
1791 Type t = al->type();
1792 if ((t.bt() == Type::BT_BOT || t.bt() == Type::BT_TOP) && ret->size() > 0) {
1793 t.bt((*ret)[0]->type().bt());
1794 }
1795 ret->type(t);
1796 return ret;
1797 }
1798 if (e->type().ispar()) {
1799 if (e->type().isintset()) {
1800 return EvalSetLit::e(env, e);
1801 }
1802 if (e->type().isfloatset()) {
1803 return EvalFloatSetLit::e(env, e);
1804 }
1805 if (e->type().isboolset()) {
1806 return EvalBoolSetLit::e(env, e);
1807 }
1808 if (e->type() == Type::parint()) {
1809 return EvalIntLit::e(env, e);
1810 }
1811 if (e->type() == Type::parbool()) {
1812 return EvalBoolLit::e(env, e);
1813 }
1814 if (e->type() == Type::parfloat()) {
1815 return EvalFloatLit::e(env, e);
1816 }
1817 if (e->type() == Type::parstring()) {
1818 return EvalStringLit::e(env, e);
1819 }
1820 }
1821 switch (e->eid()) {
1822 case Expression::E_ITE: {
1823 ITE* ite = e->cast<ITE>();
1824 for (int i = 0; i < ite->size(); i++) {
1825 if (ite->e_if(i)->type() == Type::parbool()) {
1826 if (eval_bool(env, ite->e_if(i))) return eval_par(env, ite->e_then(i));
1827 } else {
1828 std::vector<Expression*> e_ifthen(ite->size() * 2);
1829 for (int i = 0; i < ite->size(); i++) {
1830 e_ifthen[2 * i] = eval_par(env, ite->e_if(i));
1831 e_ifthen[2 * i + 1] = eval_par(env, ite->e_then(i));
1832 }
1833 ITE* n_ite = new ITE(ite->loc(), e_ifthen, eval_par(env, ite->e_else()));
1834 n_ite->type(ite->type());
1835 return n_ite;
1836 }
1837 }
1838 return eval_par(env, ite->e_else());
1839 }
1840 case Expression::E_CALL: {
1841 Call* c = e->cast<Call>();
1842 if (c->decl()) {
1843 if (c->decl()->_builtins.e) {
1844 return eval_par(env, c->decl()->_builtins.e(env, c));
1845 } else {
1846 if (c->decl()->e() == NULL) {
1847 if (c->id() == "deopt" && Expression::equal(c->arg(0), constants().absent))
1848 throw ResultUndefinedError(env, e->loc(), "deopt(<>) is undefined");
1849 return c;
1850 }
1851 return eval_call<EvalPar>(env, c);
1852 }
1853 } else {
1854 std::vector<Expression*> args(c->n_args());
1855 for (unsigned int i = 0; i < args.size(); i++) {
1856 args[i] = eval_par(env, c->arg(i));
1857 }
1858 Call* nc = new Call(c->loc(), c->id(), args);
1859 nc->type(c->type());
1860 return nc;
1861 }
1862 }
1863 case Expression::E_BINOP: {
1864 BinOp* bo = e->cast<BinOp>();
1865 BinOp* nbo =
1866 new BinOp(e->loc(), eval_par(env, bo->lhs()), bo->op(), eval_par(env, bo->rhs()));
1867 nbo->type(bo->type());
1868 return nbo;
1869 }
1870 case Expression::E_UNOP: {
1871 UnOp* uo = e->cast<UnOp>();
1872 UnOp* nuo = new UnOp(e->loc(), uo->op(), eval_par(env, uo->e()));
1873 nuo->type(uo->type());
1874 return nuo;
1875 }
1876 case Expression::E_ARRAYACCESS: {
1877 ArrayAccess* aa = e->cast<ArrayAccess>();
1878 for (unsigned int i = 0; i < aa->idx().size(); i++) {
1879 if (!aa->idx()[i]->type().ispar()) {
1880 std::vector<Expression*> idx(aa->idx().size());
1881 for (unsigned int j = 0; j < aa->idx().size(); j++) {
1882 idx[j] = eval_par(env, aa->idx()[j]);
1883 }
1884 ArrayAccess* aa_new = new ArrayAccess(e->loc(), eval_par(env, aa->v()), idx);
1885 aa_new->type(aa->type());
1886 return aa_new;
1887 }
1888 }
1889 return eval_par(env, eval_arrayaccess(env, aa));
1890 }
1891 default:
1892 return e;
1893 }
1894 }
1895 }
1896}
1897
1898class ComputeIntBounds : public EVisitor {
1899public:
1900 typedef std::pair<IntVal, IntVal> Bounds;
1901 std::vector<Bounds> _bounds;
1902 bool valid;
1903 EnvI& env;
1904 ComputeIntBounds(EnvI& env0) : valid(true), env(env0) {}
1905 bool enter(Expression* e) {
1906 if (e->type().isann()) return false;
1907 if (e->isa<VarDecl>()) return false;
1908 if (e->type().dim() > 0) return false;
1909 if (e->type().ispar()) {
1910 if (e->type().isint()) {
1911 IntVal v = eval_int(env, e);
1912 _bounds.push_back(Bounds(v, v));
1913 } else {
1914 valid = false;
1915 }
1916 return false;
1917 }
1918 if (e->type().isint()) {
1919 if (ITE* ite = e->dyn_cast<ITE>()) {
1920 Bounds itebounds(IntVal::infinity(), -IntVal::infinity());
1921 for (int i = 0; i < ite->size(); i++) {
1922 if (ite->e_if(i)->type().ispar() && ite->e_if(i)->type().cv() == Type::CV_NO) {
1923 if (eval_bool(env, ite->e_if(i))) {
1924 BottomUpIterator<ComputeIntBounds> cbi(*this);
1925 cbi.run(ite->e_then(i));
1926 Bounds& back = _bounds.back();
1927 back.first = std::min(itebounds.first, back.first);
1928 back.second = std::max(itebounds.second, back.second);
1929 return false;
1930 }
1931 } else {
1932 BottomUpIterator<ComputeIntBounds> cbi(*this);
1933 cbi.run(ite->e_then(i));
1934 Bounds back = _bounds.back();
1935 _bounds.pop_back();
1936 itebounds.first = std::min(itebounds.first, back.first);
1937 itebounds.second = std::max(itebounds.second, back.second);
1938 }
1939 }
1940 BottomUpIterator<ComputeIntBounds> cbi(*this);
1941 cbi.run(ite->e_else());
1942 Bounds& back = _bounds.back();
1943 back.first = std::min(itebounds.first, back.first);
1944 back.second = std::max(itebounds.second, back.second);
1945 return false;
1946 }
1947 return true;
1948 }
1949 return false;
1950 }
1951 /// Visit integer literal
1952 void vIntLit(const IntLit& i) { _bounds.push_back(Bounds(i.v(), i.v())); }
1953 /// Visit floating point literal
1954 void vFloatLit(const FloatLit&) {
1955 valid = false;
1956 _bounds.push_back(Bounds(0, 0));
1957 }
1958 /// Visit Boolean literal
1959 void vBoolLit(const BoolLit&) {
1960 valid = false;
1961 _bounds.push_back(Bounds(0, 0));
1962 }
1963 /// Visit set literal
1964 void vSetLit(const SetLit&) {
1965 valid = false;
1966 _bounds.push_back(Bounds(0, 0));
1967 }
1968 /// Visit string literal
1969 void vStringLit(const StringLit&) {
1970 valid = false;
1971 _bounds.push_back(Bounds(0, 0));
1972 }
1973 /// Visit identifier
1974 void vId(const Id& id) {
1975 VarDecl* vd = id.decl();
1976 while (vd->flat() && vd->flat() != vd) vd = vd->flat();
1977 if (vd->ti()->domain()) {
1978 GCLock lock;
1979 IntSetVal* isv = eval_intset(env, vd->ti()->domain());
1980 if (isv->size() == 0) {
1981 valid = false;
1982 _bounds.push_back(Bounds(0, 0));
1983 } else {
1984 _bounds.push_back(Bounds(isv->min(0), isv->max(isv->size() - 1)));
1985 }
1986 } else {
1987 if (vd->e()) {
1988 BottomUpIterator<ComputeIntBounds> cbi(*this);
1989 cbi.run(vd->e());
1990 } else {
1991 _bounds.push_back(Bounds(-IntVal::infinity(), IntVal::infinity()));
1992 }
1993 }
1994 }
1995 /// Visit anonymous variable
1996 void vAnonVar(const AnonVar& v) {
1997 valid = false;
1998 _bounds.push_back(Bounds(0, 0));
1999 }
2000 /// Visit array literal
2001 void vArrayLit(const ArrayLit& al) {}
2002 /// Visit array access
2003 void vArrayAccess(ArrayAccess& aa) {
2004 bool parAccess = true;
2005 for (unsigned int i = aa.idx().size(); i--;) {
2006 _bounds.pop_back();
2007 if (!aa.idx()[i]->type().ispar()) {
2008 parAccess = false;
2009 }
2010 }
2011 if (Id* id = aa.v()->dyn_cast<Id>()) {
2012 while (id->decl()->e() && id->decl()->e()->isa<Id>()) {
2013 id = id->decl()->e()->cast<Id>();
2014 }
2015 if (parAccess && id->decl()->e()) {
2016 bool success;
2017 Expression* e = eval_arrayaccess(env, &aa, success);
2018 if (success) {
2019 BottomUpIterator<ComputeIntBounds> cbi(*this);
2020 cbi.run(e);
2021 return;
2022 }
2023 }
2024 if (id->decl()->ti()->domain()) {
2025 GCLock lock;
2026 IntSetVal* isv = eval_intset(env, id->decl()->ti()->domain());
2027 if (isv->size() > 0) {
2028 _bounds.push_back(Bounds(isv->min(0), isv->max(isv->size() - 1)));
2029 return;
2030 }
2031 }
2032 }
2033 valid = false;
2034 _bounds.push_back(Bounds(0, 0));
2035 }
2036 /// Visit array comprehension
2037 void vComprehension(const Comprehension& c) {
2038 valid = false;
2039 _bounds.push_back(Bounds(0, 0));
2040 }
2041 /// Visit if-then-else
2042 void vITE(const ITE& ite) {
2043 valid = false;
2044 _bounds.push_back(Bounds(0, 0));
2045 }
2046 /// Visit binary operator
2047 void vBinOp(const BinOp& bo) {
2048 Bounds b1 = _bounds.back();
2049 _bounds.pop_back();
2050 Bounds b0 = _bounds.back();
2051 _bounds.pop_back();
2052 if (!b1.first.isFinite() || !b1.second.isFinite() || !b0.first.isFinite() ||
2053 !b0.second.isFinite()) {
2054 valid = false;
2055 _bounds.push_back(Bounds(0, 0));
2056 } else {
2057 switch (bo.op()) {
2058 case BOT_PLUS:
2059 _bounds.push_back(Bounds(b0.first + b1.first, b0.second + b1.second));
2060 break;
2061 case BOT_MINUS:
2062 _bounds.push_back(Bounds(b0.first - b1.second, b0.second - b1.first));
2063 break;
2064 case BOT_MULT: {
2065 IntVal x0 = b0.first * b1.first;
2066 IntVal x1 = b0.first * b1.second;
2067 IntVal x2 = b0.second * b1.first;
2068 IntVal x3 = b0.second * b1.second;
2069 IntVal m = std::min(x0, std::min(x1, std::min(x2, x3)));
2070 IntVal n = std::max(x0, std::max(x1, std::max(x2, x3)));
2071 _bounds.push_back(Bounds(m, n));
2072 } break;
2073 case BOT_IDIV: {
2074 IntVal b0f = b0.first == 0 ? 1 : b0.first;
2075 IntVal b0s = b0.second == 0 ? -1 : b0.second;
2076 IntVal b1f = b1.first == 0 ? 1 : b1.first;
2077 IntVal b1s = b1.second == 0 ? -1 : b1.second;
2078 IntVal x0 = b0f / b1f;
2079 IntVal x1 = b0f / b1s;
2080 IntVal x2 = b0s / b1f;
2081 IntVal x3 = b0s / b1s;
2082 IntVal m = std::min(x0, std::min(x1, std::min(x2, x3)));
2083 IntVal n = std::max(x0, std::max(x1, std::max(x2, x3)));
2084 _bounds.push_back(Bounds(m, n));
2085 } break;
2086 case BOT_MOD: {
2087 IntVal b0f = b0.first == 0 ? 1 : b0.first;
2088 IntVal b0s = b0.second == 0 ? -1 : b0.second;
2089 IntVal b1f = b1.first == 0 ? 1 : b1.first;
2090 IntVal b1s = b1.second == 0 ? -1 : b1.second;
2091 IntVal x0 = b0f % b1f;
2092 IntVal x1 = b0f % b1s;
2093 IntVal x2 = b0s % b1f;
2094 IntVal x3 = b0s % b1s;
2095 IntVal m = std::min(x0, std::min(x1, std::min(x2, x3)));
2096 IntVal n = std::max(x0, std::max(x1, std::max(x2, x3)));
2097 _bounds.push_back(Bounds(m, n));
2098 } break;
2099 case BOT_POW: {
2100 IntVal exp_min = std::min(0, b1.first);
2101 IntVal exp_max = std::min(0, b1.second);
2102
2103 IntVal x0 = b0.first.pow(exp_min);
2104 IntVal x1 = b0.first.pow(exp_max);
2105 IntVal x2 = b0.second.pow(exp_min);
2106 IntVal x3 = b0.second.pow(exp_max);
2107 IntVal m = std::min(x0, std::min(x1, std::min(x2, x3)));
2108 IntVal n = std::max(x0, std::max(x1, std::max(x2, x3)));
2109 _bounds.push_back(Bounds(m, n));
2110 } break;
2111 case BOT_DIV:
2112 case BOT_LE:
2113 case BOT_LQ:
2114 case BOT_GR:
2115 case BOT_GQ:
2116 case BOT_EQ:
2117 case BOT_NQ:
2118 case BOT_IN:
2119 case BOT_SUBSET:
2120 case BOT_SUPERSET:
2121 case BOT_UNION:
2122 case BOT_DIFF:
2123 case BOT_SYMDIFF:
2124 case BOT_INTERSECT:
2125 case BOT_PLUSPLUS:
2126 case BOT_EQUIV:
2127 case BOT_IMPL:
2128 case BOT_RIMPL:
2129 case BOT_OR:
2130 case BOT_AND:
2131 case BOT_XOR:
2132 case BOT_DOTDOT:
2133 valid = false;
2134 _bounds.push_back(Bounds(0, 0));
2135 }
2136 }
2137 }
2138 /// Visit unary operator
2139 void vUnOp(const UnOp& uo) {
2140 switch (uo.op()) {
2141 case UOT_PLUS:
2142 break;
2143 case UOT_MINUS:
2144 _bounds.back().first = -_bounds.back().first;
2145 _bounds.back().second = -_bounds.back().second;
2146 std::swap(_bounds.back().first, _bounds.back().second);
2147 break;
2148 case UOT_NOT:
2149 valid = false;
2150 }
2151 }
2152 /// Visit call
2153 void vCall(Call& c) {
2154 if (c.id() == constants().ids.lin_exp || c.id() == constants().ids.sum) {
2155 bool le = c.id() == constants().ids.lin_exp;
2156 ArrayLit* coeff = le ? eval_array_lit(env, c.arg(0)) : NULL;
2157 if (c.arg(le ? 1 : 0)->type().isopt()) {
2158 valid = false;
2159 _bounds.push_back(Bounds(0, 0));
2160 return;
2161 }
2162 ArrayLit* al = eval_array_lit(env, c.arg(le ? 1 : 0));
2163 if (le) {
2164 _bounds.pop_back(); // remove constant (third arg) from stack
2165 }
2166
2167 IntVal d = le ? c.arg(2)->cast<IntLit>()->v() : 0;
2168 int stacktop = static_cast<int>(_bounds.size());
2169 for (unsigned int i = al->size(); i--;) {
2170 BottomUpIterator<ComputeIntBounds> cbi(*this);
2171 cbi.run((*al)[i]);
2172 if (!valid) {
2173 for (unsigned int j = al->size() - 1; j > i; j--) _bounds.pop_back();
2174 return;
2175 }
2176 }
2177 assert(stacktop + al->size() == _bounds.size());
2178 IntVal lb = d;
2179 IntVal ub = d;
2180 for (unsigned int i = 0; i < al->size(); i++) {
2181 Bounds b = _bounds.back();
2182 _bounds.pop_back();
2183 IntVal cv = le ? eval_int(env, (*coeff)[i]) : 1;
2184 if (cv > 0) {
2185 if (b.first.isFinite()) {
2186 if (lb.isFinite()) {
2187 lb += cv * b.first;
2188 }
2189 } else {
2190 lb = b.first;
2191 }
2192 if (b.second.isFinite()) {
2193 if (ub.isFinite()) {
2194 ub += cv * b.second;
2195 }
2196 } else {
2197 ub = b.second;
2198 }
2199 } else {
2200 if (b.second.isFinite()) {
2201 if (lb.isFinite()) {
2202 lb += cv * b.second;
2203 }
2204 } else {
2205 lb = -b.second;
2206 }
2207 if (b.first.isFinite()) {
2208 if (ub.isFinite()) {
2209 ub += cv * b.first;
2210 }
2211 } else {
2212 ub = -b.first;
2213 }
2214 }
2215 }
2216 _bounds.push_back(Bounds(lb, ub));
2217 } else if (c.id() == "card") {
2218 if (IntSetVal* isv = compute_intset_bounds(env, c.arg(0))) {
2219 IntSetRanges isr(isv);
2220 _bounds.push_back(Bounds(0, Ranges::cardinality(isr)));
2221 } else {
2222 valid = false;
2223 _bounds.push_back(Bounds(0, 0));
2224 }
2225 } else if (c.id() == "int_times") {
2226 Bounds b1 = _bounds.back();
2227 _bounds.pop_back();
2228 Bounds b0 = _bounds.back();
2229 _bounds.pop_back();
2230 if (!b1.first.isFinite() || !b1.second.isFinite() || !b0.first.isFinite() ||
2231 !b0.second.isFinite()) {
2232 valid = false;
2233 _bounds.push_back(Bounds(0, 0));
2234 } else {
2235 IntVal x0 = b0.first * b1.first;
2236 IntVal x1 = b0.first * b1.second;
2237 IntVal x2 = b0.second * b1.first;
2238 IntVal x3 = b0.second * b1.second;
2239 IntVal m = std::min(x0, std::min(x1, std::min(x2, x3)));
2240 IntVal n = std::max(x0, std::max(x1, std::max(x2, x3)));
2241 _bounds.push_back(Bounds(m, n));
2242 }
2243 } else if (c.id() == constants().ids.bool2int) {
2244 _bounds.push_back(Bounds(0, 1));
2245 } else if (c.id() == "abs") {
2246 Bounds b0 = _bounds.back();
2247 if (b0.first < 0) {
2248 _bounds.pop_back();
2249 if (b0.second < 0)
2250 _bounds.push_back(Bounds(-b0.second, -b0.first));
2251 else
2252 _bounds.push_back(Bounds(0, std::max(-b0.first, b0.second)));
2253 }
2254 } else if (c.decl() && c.decl()->ti()->domain() && !c.decl()->ti()->domain()->isa<TIId>()) {
2255 for (int i = 0; i < c.n_args(); i++) {
2256 if (c.arg(i)->type().isint()) {
2257 assert(_bounds.size() > 0);
2258 _bounds.pop_back();
2259 }
2260 }
2261 IntSetVal* isv = eval_intset(env, c.decl()->ti()->domain());
2262 _bounds.push_back(Bounds(isv->min(), isv->max()));
2263 } else {
2264 valid = false;
2265 _bounds.push_back(Bounds(0, 0));
2266 }
2267 }
2268 /// Visit let
2269 void vLet(const Let& l) {
2270 valid = false;
2271 _bounds.push_back(Bounds(0, 0));
2272 }
2273 /// Visit variable declaration
2274 void vVarDecl(const VarDecl& vd) {
2275 valid = false;
2276 _bounds.push_back(Bounds(0, 0));
2277 }
2278 /// Visit annotation
2279 void vAnnotation(const Annotation& e) {
2280 valid = false;
2281 _bounds.push_back(Bounds(0, 0));
2282 }
2283 /// Visit type inst
2284 void vTypeInst(const TypeInst& e) {
2285 valid = false;
2286 _bounds.push_back(Bounds(0, 0));
2287 }
2288 /// Visit TIId
2289 void vTIId(const TIId& e) {
2290 valid = false;
2291 _bounds.push_back(Bounds(0, 0));
2292 }
2293};
2294
2295IntBounds compute_int_bounds(EnvI& env, Expression* e) {
2296 try {
2297 ComputeIntBounds cb(env);
2298 BottomUpIterator<ComputeIntBounds> cbi(cb);
2299 cbi.run(e);
2300 if (cb.valid) {
2301 assert(cb._bounds.size() == 1);
2302 return IntBounds(cb._bounds.back().first, cb._bounds.back().second, true);
2303 } else {
2304 return IntBounds(0, 0, false);
2305 }
2306 } catch (ResultUndefinedError&) {
2307 return IntBounds(0, 0, false);
2308 }
2309}
2310
2311class ComputeFloatBounds : public EVisitor {
2312protected:
2313 typedef std::pair<FloatVal, FloatVal> FBounds;
2314
2315public:
2316 std::vector<FBounds> _bounds;
2317 bool valid;
2318 EnvI& env;
2319 ComputeFloatBounds(EnvI& env0) : valid(true), env(env0) {}
2320 bool enter(Expression* e) {
2321 if (e->type().isann()) return false;
2322 if (e->isa<VarDecl>()) return false;
2323 if (e->type().dim() > 0) return false;
2324 if (e->type().ispar()) {
2325 if (e->type().isfloat()) {
2326 FloatVal v = eval_float(env, e);
2327 _bounds.push_back(FBounds(v, v));
2328 }
2329 return false;
2330 } else {
2331 return e->type().isfloat();
2332 }
2333 }
2334 /// Visit integer literal
2335 void vIntLit(const IntLit& i) {
2336 valid = false;
2337 _bounds.push_back(FBounds(0.0, 0.0));
2338 }
2339 /// Visit floating point literal
2340 void vFloatLit(const FloatLit& f) { _bounds.push_back(FBounds(f.v(), f.v())); }
2341 /// Visit Boolean literal
2342 void vBoolLit(const BoolLit&) {
2343 valid = false;
2344 _bounds.push_back(FBounds(0.0, 0.0));
2345 }
2346 /// Visit set literal
2347 void vSetLit(const SetLit&) {
2348 valid = false;
2349 _bounds.push_back(FBounds(0.0, 0.0));
2350 }
2351 /// Visit string literal
2352 void vStringLit(const StringLit&) {
2353 valid = false;
2354 _bounds.push_back(FBounds(0.0, 0.0));
2355 }
2356 /// Visit identifier
2357 void vId(const Id& id) {
2358 VarDecl* vd = id.decl();
2359 while (vd->flat() && vd->flat() != vd) vd = vd->flat();
2360 if (vd->ti()->domain()) {
2361 FloatSetVal* fsv = eval_floatset(env, vd->ti()->domain());
2362 _bounds.push_back(FBounds(fsv->min(), fsv->max()));
2363 } else {
2364 if (vd->e()) {
2365 BottomUpIterator<ComputeFloatBounds> cbi(*this);
2366 cbi.run(vd->e());
2367 } else {
2368 valid = false;
2369 _bounds.push_back(FBounds(0, 0));
2370 }
2371 }
2372 }
2373 /// Visit anonymous variable
2374 void vAnonVar(const AnonVar& v) {
2375 valid = false;
2376 _bounds.push_back(FBounds(0.0, 0.0));
2377 }
2378 /// Visit array literal
2379 void vArrayLit(const ArrayLit& al) {}
2380 /// Visit array access
2381 void vArrayAccess(ArrayAccess& aa) {
2382 bool parAccess = true;
2383 for (unsigned int i = aa.idx().size(); i--;) {
2384 if (!aa.idx()[i]->type().ispar()) {
2385 parAccess = false;
2386 }
2387 }
2388 if (Id* id = aa.v()->dyn_cast<Id>()) {
2389 while (id->decl()->e() && id->decl()->e()->isa<Id>()) {
2390 id = id->decl()->e()->cast<Id>();
2391 }
2392 if (parAccess && id->decl()->e()) {
2393 bool success;
2394 Expression* e = eval_arrayaccess(env, &aa, success);
2395 if (success) {
2396 BottomUpIterator<ComputeFloatBounds> cbi(*this);
2397 cbi.run(e);
2398 return;
2399 }
2400 }
2401 if (id->decl()->ti()->domain()) {
2402 FloatSetVal* fsv = eval_floatset(env, id->decl()->ti()->domain());
2403 FBounds b(fsv->min(), fsv->max());
2404 _bounds.push_back(b);
2405 return;
2406 }
2407 }
2408 valid = false;
2409 _bounds.push_back(FBounds(0.0, 0.0));
2410 }
2411 /// Visit array comprehension
2412 void vComprehension(const Comprehension& c) {
2413 valid = false;
2414 _bounds.push_back(FBounds(0.0, 0.0));
2415 }
2416 /// Visit if-then-else
2417 void vITE(const ITE& ite) {
2418 valid = false;
2419 _bounds.push_back(FBounds(0.0, 0.0));
2420 }
2421 /// Visit binary operator
2422 void vBinOp(const BinOp& bo) {
2423 FBounds b1 = _bounds.back();
2424 _bounds.pop_back();
2425 FBounds b0 = _bounds.back();
2426 _bounds.pop_back();
2427 if (!b1.first.isFinite() || !b1.second.isFinite() || !b0.first.isFinite() ||
2428 !b0.second.isFinite()) {
2429 valid = false;
2430 _bounds.push_back(FBounds(0.0, 0.0));
2431 } else {
2432 switch (bo.op()) {
2433 case BOT_PLUS:
2434 _bounds.push_back(FBounds(b0.first + b1.first, b0.second + b1.second));
2435 break;
2436 case BOT_MINUS:
2437 _bounds.push_back(FBounds(b0.first - b1.second, b0.second - b1.first));
2438 break;
2439 case BOT_MULT: {
2440 FloatVal x0 = b0.first * b1.first;
2441 FloatVal x1 = b0.first * b1.second;
2442 FloatVal x2 = b0.second * b1.first;
2443 FloatVal x3 = b0.second * b1.second;
2444 FloatVal m = std::min(x0, std::min(x1, std::min(x2, x3)));
2445 FloatVal n = std::max(x0, std::max(x1, std::max(x2, x3)));
2446 _bounds.push_back(FBounds(m, n));
2447 } break;
2448 case BOT_POW: {
2449 FloatVal x0 = std::pow(b0.first.toDouble(), b1.first.toDouble());
2450 FloatVal x1 = std::pow(b0.first.toDouble(), b1.second.toDouble());
2451 FloatVal x2 = std::pow(b0.second.toDouble(), b1.first.toDouble());
2452 FloatVal x3 = std::pow(b0.second.toDouble(), b1.second.toDouble());
2453 FloatVal m = std::min(x0, std::min(x1, std::min(x2, x3)));
2454 FloatVal n = std::max(x0, std::max(x1, std::max(x2, x3)));
2455 _bounds.push_back(FBounds(m, n));
2456 } break;
2457 case BOT_DIV:
2458 case BOT_IDIV:
2459 case BOT_MOD:
2460 case BOT_LE:
2461 case BOT_LQ:
2462 case BOT_GR:
2463 case BOT_GQ:
2464 case BOT_EQ:
2465 case BOT_NQ:
2466 case BOT_IN:
2467 case BOT_SUBSET:
2468 case BOT_SUPERSET:
2469 case BOT_UNION:
2470 case BOT_DIFF:
2471 case BOT_SYMDIFF:
2472 case BOT_INTERSECT:
2473 case BOT_PLUSPLUS:
2474 case BOT_EQUIV:
2475 case BOT_IMPL:
2476 case BOT_RIMPL:
2477 case BOT_OR:
2478 case BOT_AND:
2479 case BOT_XOR:
2480 case BOT_DOTDOT:
2481 valid = false;
2482 _bounds.push_back(FBounds(0.0, 0.0));
2483 }
2484 }
2485 }
2486 /// Visit unary operator
2487 void vUnOp(const UnOp& uo) {
2488 switch (uo.op()) {
2489 case UOT_PLUS:
2490 break;
2491 case UOT_MINUS:
2492 _bounds.back().first = -_bounds.back().first;
2493 _bounds.back().second = -_bounds.back().second;
2494 break;
2495 case UOT_NOT:
2496 valid = false;
2497 _bounds.push_back(FBounds(0.0, 0.0));
2498 }
2499 }
2500 /// Visit call
2501 void vCall(Call& c) {
2502 if (c.id() == constants().ids.lin_exp || c.id() == constants().ids.sum) {
2503 bool le = c.id() == constants().ids.lin_exp;
2504 ArrayLit* coeff = le ? eval_array_lit(env, c.arg(0)) : NULL;
2505 if (le) {
2506 _bounds.pop_back(); // remove constant (third arg) from stack
2507 }
2508 if (c.arg(le ? 1 : 0)->type().isopt()) {
2509 valid = false;
2510 _bounds.push_back(FBounds(0.0, 0.0));
2511 return;
2512 }
2513 ArrayLit* al = eval_array_lit(env, c.arg(le ? 1 : 0));
2514 FloatVal d = le ? c.arg(2)->cast<FloatLit>()->v() : 0.0;
2515 int stacktop = static_cast<int>(_bounds.size());
2516 for (unsigned int i = al->size(); i--;) {
2517 BottomUpIterator<ComputeFloatBounds> cbi(*this);
2518 cbi.run((*al)[i]);
2519 if (!valid) return;
2520 }
2521 assert(stacktop + al->size() == _bounds.size());
2522 FloatVal lb = d;
2523 FloatVal ub = d;
2524 for (unsigned int i = 0; i < (*al).size(); i++) {
2525 FBounds b = _bounds.back();
2526 _bounds.pop_back();
2527 FloatVal cv = le ? eval_float(env, (*coeff)[i]) : 1.0;
2528
2529 if (cv > 0) {
2530 if (b.first.isFinite()) {
2531 if (lb.isFinite()) {
2532 lb += cv * b.first;
2533 }
2534 } else {
2535 lb = b.first;
2536 }
2537 if (b.second.isFinite()) {
2538 if (ub.isFinite()) {
2539 ub += cv * b.second;
2540 }
2541 } else {
2542 ub = b.second;
2543 }
2544 } else {
2545 if (b.second.isFinite()) {
2546 if (lb.isFinite()) {
2547 lb += cv * b.second;
2548 }
2549 } else {
2550 lb = -b.second;
2551 }
2552 if (b.first.isFinite()) {
2553 if (ub.isFinite()) {
2554 ub += cv * b.first;
2555 }
2556 } else {
2557 ub = -b.first;
2558 }
2559 }
2560 }
2561 _bounds.push_back(FBounds(lb, ub));
2562 } else if (c.id() == "float_times") {
2563 BottomUpIterator<ComputeFloatBounds> cbi(*this);
2564 cbi.run(c.arg(0));
2565 cbi.run(c.arg(1));
2566 FBounds b1 = _bounds.back();
2567 _bounds.pop_back();
2568 FBounds b0 = _bounds.back();
2569 _bounds.pop_back();
2570 if (!b1.first.isFinite() || !b1.second.isFinite() || !b0.first.isFinite() ||
2571 !b0.second.isFinite()) {
2572 valid = false;
2573 _bounds.push_back(FBounds(0, 0));
2574 } else {
2575 FloatVal x0 = b0.first * b1.first;
2576 FloatVal x1 = b0.first * b1.second;
2577 FloatVal x2 = b0.second * b1.first;
2578 FloatVal x3 = b0.second * b1.second;
2579 FloatVal m = std::min(x0, std::min(x1, std::min(x2, x3)));
2580 FloatVal n = std::max(x0, std::max(x1, std::max(x2, x3)));
2581 _bounds.push_back(FBounds(m, n));
2582 }
2583 } else if (c.id() == "int2float") {
2584 ComputeIntBounds ib(env);
2585 BottomUpIterator<ComputeIntBounds> cbi(ib);
2586 cbi.run(c.arg(0));
2587 if (!ib.valid) valid = false;
2588 ComputeIntBounds::Bounds result = ib._bounds.back();
2589 if (!result.first.isFinite() || !result.second.isFinite()) {
2590 valid = false;
2591 _bounds.push_back(FBounds(0.0, 0.0));
2592 } else {
2593 _bounds.push_back(FBounds(static_cast<double>(result.first.toInt()),
2594 static_cast<double>(result.second.toInt())));
2595 }
2596 } else if (c.id() == "abs") {
2597 BottomUpIterator<ComputeFloatBounds> cbi(*this);
2598 cbi.run(c.arg(0));
2599 FBounds b0 = _bounds.back();
2600 if (b0.first < 0) {
2601 _bounds.pop_back();
2602 if (b0.second < 0)
2603 _bounds.push_back(FBounds(-b0.second, -b0.first));
2604 else
2605 _bounds.push_back(FBounds(0.0, std::max(-b0.first, b0.second)));
2606 }
2607 } else if (c.decl() && c.decl()->ti()->domain() && !c.decl()->ti()->domain()->isa<TIId>()) {
2608 for (int i = 0; i < c.n_args(); i++) {
2609 if (c.arg(i)->type().isfloat()) {
2610 assert(_bounds.size() > 0);
2611 _bounds.pop_back();
2612 }
2613 }
2614 FloatSetVal* fsv = eval_floatset(env, c.decl()->ti()->domain());
2615 _bounds.push_back(FBounds(fsv->min(), fsv->max()));
2616 } else {
2617 valid = false;
2618 _bounds.push_back(FBounds(0.0, 0.0));
2619 }
2620 }
2621 /// Visit let
2622 void vLet(const Let& l) {
2623 valid = false;
2624 _bounds.push_back(FBounds(0.0, 0.0));
2625 }
2626 /// Visit variable declaration
2627 void vVarDecl(const VarDecl& vd) {
2628 valid = false;
2629 _bounds.push_back(FBounds(0.0, 0.0));
2630 }
2631 /// Visit annotation
2632 void vAnnotation(const Annotation& e) {
2633 valid = false;
2634 _bounds.push_back(FBounds(0.0, 0.0));
2635 }
2636 /// Visit type inst
2637 void vTypeInst(const TypeInst& e) {
2638 valid = false;
2639 _bounds.push_back(FBounds(0.0, 0.0));
2640 }
2641 /// Visit TIId
2642 void vTIId(const TIId& e) {
2643 valid = false;
2644 _bounds.push_back(FBounds(0.0, 0.0));
2645 }
2646};
2647
2648FloatBounds compute_float_bounds(EnvI& env, Expression* e) {
2649 try {
2650 ComputeFloatBounds cb(env);
2651 BottomUpIterator<ComputeFloatBounds> cbi(cb);
2652 cbi.run(e);
2653 if (cb.valid) {
2654 assert(cb._bounds.size() > 0);
2655 return FloatBounds(cb._bounds.back().first, cb._bounds.back().second, true);
2656 } else {
2657 return FloatBounds(0.0, 0.0, false);
2658 }
2659 } catch (ResultUndefinedError&) {
2660 return FloatBounds(0.0, 0.0, false);
2661 }
2662}
2663
2664class ComputeIntSetBounds : public EVisitor {
2665public:
2666 std::vector<IntSetVal*> _bounds;
2667 bool valid;
2668 EnvI& env;
2669 ComputeIntSetBounds(EnvI& env0) : valid(true), env(env0) {}
2670 bool enter(Expression* e) {
2671 if (e->type().isann()) return false;
2672 if (e->isa<VarDecl>()) return false;
2673 if (e->type().dim() > 0) return false;
2674 if (!e->type().isintset()) return false;
2675 if (e->type().ispar()) {
2676 _bounds.push_back(eval_intset(env, e));
2677 return false;
2678 } else {
2679 return true;
2680 }
2681 }
2682 /// Visit set literal
2683 void vSetLit(const SetLit& sl) {
2684 assert(sl.type().isvar());
2685 assert(sl.isv() == NULL);
2686
2687 IntSetVal* isv = IntSetVal::a();
2688 for (unsigned int i = 0; i < sl.v().size(); i++) {
2689 IntSetRanges i0(isv);
2690 IntBounds ib = compute_int_bounds(env, sl.v()[i]);
2691 if (!ib.valid || !ib.l.isFinite() || !ib.u.isFinite()) {
2692 valid = false;
2693 _bounds.push_back(NULL);
2694 return;
2695 }
2696 Ranges::Const<IntVal> cr(ib.l, ib.u);
2697 Ranges::Union<IntVal, IntSetRanges, Ranges::Const<IntVal>> u(i0, cr);
2698 isv = IntSetVal::ai(u);
2699 }
2700 _bounds.push_back(isv);
2701 }
2702 /// Visit identifier
2703 void vId(const Id& id) {
2704 if (id.decl()->ti()->domain() && !id.decl()->ti()->domain()->isa<TIId>()) {
2705 _bounds.push_back(eval_intset(env, id.decl()->ti()->domain()));
2706 } else {
2707 if (id.decl()->e()) {
2708 BottomUpIterator<ComputeIntSetBounds> cbi(*this);
2709 cbi.run(id.decl()->e());
2710 } else {
2711 valid = false;
2712 _bounds.push_back(NULL);
2713 }
2714 }
2715 }
2716 /// Visit anonymous variable
2717 void vAnonVar(const AnonVar& v) {
2718 valid = false;
2719 _bounds.push_back(NULL);
2720 }
2721 /// Visit array access
2722 void vArrayAccess(ArrayAccess& aa) {
2723 bool parAccess = true;
2724 for (unsigned int i = aa.idx().size(); i--;) {
2725 if (!aa.idx()[i]->type().ispar()) {
2726 parAccess = false;
2727 break;
2728 }
2729 }
2730 if (Id* id = aa.v()->dyn_cast<Id>()) {
2731 while (id->decl()->e() && id->decl()->e()->isa<Id>()) {
2732 id = id->decl()->e()->cast<Id>();
2733 }
2734 if (parAccess && id->decl()->e()) {
2735 bool success;
2736 Expression* e = eval_arrayaccess(env, &aa, success);
2737 if (success) {
2738 BottomUpIterator<ComputeIntSetBounds> cbi(*this);
2739 cbi.run(e);
2740 return;
2741 }
2742 }
2743 if (id->decl()->ti()->domain()) {
2744 _bounds.push_back(eval_intset(env, id->decl()->ti()->domain()));
2745 return;
2746 }
2747 }
2748 valid = false;
2749 _bounds.push_back(NULL);
2750 }
2751 /// Visit array comprehension
2752 void vComprehension(const Comprehension& c) {
2753 valid = false;
2754 _bounds.push_back(NULL);
2755 }
2756 /// Visit if-then-else
2757 void vITE(const ITE& ite) {
2758 valid = false;
2759 _bounds.push_back(NULL);
2760 }
2761 /// Visit binary operator
2762 void vBinOp(const BinOp& bo) {
2763 if (bo.op() == BOT_DOTDOT) {
2764 IntBounds lb = compute_int_bounds(env, bo.lhs());
2765 IntBounds ub = compute_int_bounds(env, bo.rhs());
2766 valid = valid && lb.valid && ub.valid;
2767 _bounds.push_back(IntSetVal::a(lb.l, ub.u));
2768 } else {
2769 IntSetVal* b1 = _bounds.back();
2770 _bounds.pop_back();
2771 IntSetVal* b0 = _bounds.back();
2772 _bounds.pop_back();
2773 switch (bo.op()) {
2774 case BOT_INTERSECT:
2775 case BOT_UNION: {
2776 IntSetRanges b0r(b0);
2777 IntSetRanges b1r(b1);
2778 Ranges::Union<IntVal, IntSetRanges, IntSetRanges> u(b0r, b1r);
2779 _bounds.push_back(IntSetVal::ai(u));
2780 } break;
2781 case BOT_DIFF: {
2782 _bounds.push_back(b0);
2783 } break;
2784 case BOT_SYMDIFF:
2785 valid = false;
2786 _bounds.push_back(NULL);
2787 break;
2788 case BOT_PLUS:
2789 case BOT_MINUS:
2790 case BOT_MULT:
2791 case BOT_POW:
2792 case BOT_DIV:
2793 case BOT_IDIV:
2794 case BOT_MOD:
2795 case BOT_LE:
2796 case BOT_LQ:
2797 case BOT_GR:
2798 case BOT_GQ:
2799 case BOT_EQ:
2800 case BOT_NQ:
2801 case BOT_IN:
2802 case BOT_SUBSET:
2803 case BOT_SUPERSET:
2804 case BOT_PLUSPLUS:
2805 case BOT_EQUIV:
2806 case BOT_IMPL:
2807 case BOT_RIMPL:
2808 case BOT_OR:
2809 case BOT_AND:
2810 case BOT_XOR:
2811 case BOT_DOTDOT:
2812 valid = false;
2813 _bounds.push_back(NULL);
2814 }
2815 }
2816 }
2817 /// Visit unary operator
2818 void vUnOp(const UnOp& uo) {
2819 valid = false;
2820 _bounds.push_back(NULL);
2821 }
2822 /// Visit call
2823 void vCall(Call& c) {
2824 if (valid && (c.id() == "set_intersect" || c.id() == "set_union")) {
2825 IntSetVal* b0 = _bounds.back();
2826 _bounds.pop_back();
2827 IntSetVal* b1 = _bounds.back();
2828 _bounds.pop_back();
2829 IntSetRanges b0r(b0);
2830 IntSetRanges b1r(b1);
2831 Ranges::Union<IntVal, IntSetRanges, IntSetRanges> u(b0r, b1r);
2832 _bounds.push_back(IntSetVal::ai(u));
2833 } else if (valid && c.id() == "set_diff") {
2834 IntSetVal* b0 = _bounds.back();
2835 _bounds.pop_back();
2836 _bounds.pop_back(); // don't need bounds of right hand side
2837 _bounds.push_back(b0);
2838 } else if (c.decl() && c.decl()->ti()->domain() && !c.decl()->ti()->domain()->isa<TIId>()) {
2839 for (int i = 0; i < c.n_args(); i++) {
2840 if (c.arg(i)->type().isintset()) {
2841 assert(_bounds.size() > 0);
2842 _bounds.pop_back();
2843 }
2844 }
2845 IntSetVal* fsv = eval_intset(env, c.decl()->ti()->domain());
2846 _bounds.push_back(fsv);
2847 } else {
2848 valid = false;
2849 _bounds.push_back(NULL);
2850 }
2851 }
2852 /// Visit let
2853 void vLet(const Let& l) {
2854 valid = false;
2855 _bounds.push_back(NULL);
2856 }
2857 /// Visit variable declaration
2858 void vVarDecl(const VarDecl& vd) {
2859 valid = false;
2860 _bounds.push_back(NULL);
2861 }
2862 /// Visit annotation
2863 void vAnnotation(const Annotation& e) {
2864 valid = false;
2865 _bounds.push_back(NULL);
2866 }
2867 /// Visit type inst
2868 void vTypeInst(const TypeInst& e) {
2869 valid = false;
2870 _bounds.push_back(NULL);
2871 }
2872 /// Visit TIId
2873 void vTIId(const TIId& e) {
2874 valid = false;
2875 _bounds.push_back(NULL);
2876 }
2877};
2878
2879IntSetVal* compute_intset_bounds(EnvI& env, Expression* e) {
2880 try {
2881 ComputeIntSetBounds cb(env);
2882 BottomUpIterator<ComputeIntSetBounds> cbi(cb);
2883 cbi.run(e);
2884 if (cb.valid)
2885 return cb._bounds.back();
2886 else
2887 return NULL;
2888 } catch (ResultUndefinedError&) {
2889 return NULL;
2890 }
2891}
2892
2893Expression* follow_id(Expression* e) {
2894 for (;;) {
2895 if (e == NULL) return NULL;
2896 if (e->eid() == Expression::E_ID && e != constants().absent) {
2897 e = e->cast<Id>()->decl()->e();
2898 } else {
2899 return e;
2900 }
2901 }
2902}
2903
2904Expression* follow_id_to_decl(Expression* e) {
2905 for (;;) {
2906 if (e == NULL) return NULL;
2907 if (e == constants().absent) return e;
2908 switch (e->eid()) {
2909 case Expression::E_ID:
2910 e = e->cast<Id>()->decl();
2911 break;
2912 case Expression::E_VARDECL:
2913 if (e->cast<VarDecl>()->e() && e->cast<VarDecl>()->e()->isa<Id>())
2914 e = e->cast<VarDecl>()->e();
2915 else
2916 return e;
2917 break;
2918 default:
2919 return e;
2920 }
2921 }
2922}
2923
2924Expression* follow_id_to_value(Expression* e) {
2925 Expression* decl = follow_id_to_decl(e);
2926 if (VarDecl* vd = decl->dyn_cast<VarDecl>()) {
2927 if (vd->e() && vd->e()->type().ispar()) return vd->e();
2928 return vd->id();
2929 } else {
2930 return decl;
2931 }
2932}
2933
2934} // namespace MiniZinc