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/ast.hh>
13#include <minizinc/astexception.hh>
14#include <minizinc/flatten_internal.hh>
15#include <minizinc/hash.hh>
16#include <minizinc/iter.hh>
17#include <minizinc/model.hh>
18#include <minizinc/prettyprinter.hh>
19
20namespace MiniZinc {
21
22Location::LocVec* Location::LocVec::a(const ASTString& filename, unsigned int first_line,
23 unsigned int first_column, unsigned int last_line,
24 unsigned int last_column) {
25 static const unsigned int pointerBits = sizeof(IntLit*) * 8;
26 if (pointerBits <= 32) {
27 if (first_line < (1 << 8) && last_line - first_line < (1 << 7) && first_column < (1 << 6) &&
28 last_column < (1 << 7)) {
29 long long int combined = first_line;
30 combined |= (last_line - first_line) << 8;
31 combined |= (first_column) << (8 + 7);
32 combined |= (last_column) << (8 + 7 + 6);
33 LocVec* v = static_cast<LocVec*>(alloc(2));
34 new (v) LocVec(filename, combined);
35 return v;
36 }
37 } else if (pointerBits >= 64) {
38 if (first_line < (1 << 20) && last_line - first_line < (1 << 20) && first_column < (1 << 10) &&
39 last_column < (1 << 10)) {
40 long long int combined = first_line;
41 combined |= (static_cast<unsigned long long int>(last_line - first_line)) << 20;
42 combined |= (static_cast<unsigned long long int>(first_column)) << (20 + 20);
43 combined |= (static_cast<unsigned long long int>(last_column)) << (20 + 20 + 10);
44 LocVec* v = static_cast<LocVec*>(alloc(2));
45 new (v) LocVec(filename, combined);
46 return v;
47 }
48 }
49
50 LocVec* v = static_cast<LocVec*>(alloc(5));
51 new (v) LocVec(filename, first_line, first_column, last_line, last_column);
52 return v;
53}
54
55Location::LocVec::LocVec(const ASTString& filename, IntVal combined) : ASTVec(2) {
56 *(_data + 0) = filename.aststr();
57 *(_data + 1) = IntLit::a(combined);
58}
59
60Location::LocVec::LocVec(const ASTString& filename, unsigned int fl, unsigned int first_column,
61 unsigned int last_line, unsigned int last_column)
62 : ASTVec(5) {
63 *(_data + 0) = filename.aststr();
64 *(_data + 1) = IntLit::a(fl);
65 *(_data + 2) = IntLit::a(last_line);
66 *(_data + 3) = IntLit::a(first_column);
67 *(_data + 4) = IntLit::a(last_column);
68}
69
70Location Location::nonalloc;
71
72Type Type::unboxedint = Type::parint();
73Type Type::unboxedfloat = Type::parfloat();
74
75Annotation Annotation::empty;
76
77std::string Location::toString(void) const {
78 std::ostringstream oss;
79 oss << filename() << ":" << first_line() << "." << first_column();
80 return oss.str();
81}
82
83void Location::mark(void) const {
84 if (lv()) lv()->mark();
85}
86
87Location Location::introduce() const {
88 Location l = *this;
89 if (l._loc_info.lv) {
90 l._loc_info.t |= 1;
91 }
92 return l;
93}
94
95void Expression::addAnnotation(Expression* ann) {
96 if (!isUnboxedVal()) _ann.add(ann);
97}
98void Expression::addAnnotations(std::vector<Expression*> ann) {
99 if (!isUnboxedVal())
100 for (unsigned int i = 0; i < ann.size(); i++)
101 if (ann[i]) _ann.add(ann[i]);
102}
103
104#define pushstack(e) \
105 do { \
106 if (e != NULL) { \
107 stack.push_back(e); \
108 } \
109 } while (0)
110#define pushall(v) \
111 do { \
112 v.mark(); \
113 for (unsigned int i = 0; i < v.size(); i++) \
114 if (v[i] != NULL) { \
115 stack.push_back(v[i]); \
116 } \
117 } while (0)
118#define pushann(a) \
119 do { \
120 for (ExpressionSetIter it = a.begin(); it != a.end(); ++it) { \
121 pushstack(*it); \
122 } \
123 } while (0)
124void Expression::mark(Expression* e) {
125 if (e == NULL || e->isUnboxedVal()) return;
126 std::vector<const Expression*> stack;
127 stack.reserve(1000);
128 stack.push_back(e);
129 while (!stack.empty()) {
130 const Expression* cur = stack.back();
131 stack.pop_back();
132 if (!cur->isUnboxedVal() && cur->_gc_mark == 0) {
133 cur->_gc_mark = 1;
134 cur->loc().mark();
135 pushann(cur->ann());
136 switch (cur->eid()) {
137 case Expression::E_INTLIT:
138 case Expression::E_FLOATLIT:
139 case Expression::E_BOOLLIT:
140 case Expression::E_ANON:
141 break;
142 case Expression::E_SETLIT:
143 if (cur->cast<SetLit>()->isv()) {
144 cur->cast<SetLit>()->isv()->mark();
145 } else if (cur->cast<SetLit>()->fsv()) {
146 cur->cast<SetLit>()->fsv()->mark();
147 } else {
148 pushall(cur->cast<SetLit>()->v());
149 }
150 break;
151 case Expression::E_STRINGLIT:
152 cur->cast<StringLit>()->v().mark();
153 break;
154 case Expression::E_ID:
155 if (cur->cast<Id>()->idn() == -1) cur->cast<Id>()->v().mark();
156 pushstack(cur->cast<Id>()->decl());
157 break;
158 case Expression::E_ARRAYLIT:
159 if (cur->_flag_2) {
160 pushstack(cur->cast<ArrayLit>()->_u._al);
161 } else {
162 pushall(ASTExprVec<Expression>(cur->cast<ArrayLit>()->_u._v));
163 }
164 cur->cast<ArrayLit>()->_dims.mark();
165 break;
166 case Expression::E_ARRAYACCESS:
167 pushstack(cur->cast<ArrayAccess>()->v());
168 pushall(cur->cast<ArrayAccess>()->idx());
169 break;
170 case Expression::E_COMP:
171 pushstack(cur->cast<Comprehension>()->_e);
172 pushall(cur->cast<Comprehension>()->_g);
173 cur->cast<Comprehension>()->_g_idx.mark();
174 break;
175 case Expression::E_ITE:
176 pushstack(cur->cast<ITE>()->e_else());
177 pushall(cur->cast<ITE>()->_e_if_then);
178 break;
179 case Expression::E_BINOP:
180 pushstack(cur->cast<BinOp>()->lhs());
181 pushstack(cur->cast<BinOp>()->rhs());
182 break;
183 case Expression::E_UNOP:
184 pushstack(cur->cast<UnOp>()->e());
185 break;
186 case Expression::E_CALL:
187 cur->cast<Call>()->id().mark();
188 for (unsigned int i = cur->cast<Call>()->n_args(); i--;)
189 pushstack(cur->cast<Call>()->arg(i));
190 if (!cur->cast<Call>()->_u._oneArg->isUnboxedVal() &&
191 !cur->cast<Call>()->_u._oneArg->isTagged())
192 cur->cast<Call>()->_u._args->mark();
193 if (FunctionI* fi = cur->cast<Call>()->decl()) {
194 fi->mark();
195 fi->id().mark();
196 pushstack(fi->ti());
197 pushann(fi->ann());
198 pushstack(fi->e());
199 pushall(fi->params());
200 }
201 break;
202 case Expression::E_VARDECL:
203 pushstack(cur->cast<VarDecl>()->ti());
204 pushstack(cur->cast<VarDecl>()->e());
205 pushstack(cur->cast<VarDecl>()->id());
206 break;
207 case Expression::E_LET:
208 pushall(cur->cast<Let>()->let());
209 pushall(cur->cast<Let>()->_let_orig);
210 pushstack(cur->cast<Let>()->in());
211 break;
212 case Expression::E_TI:
213 pushstack(cur->cast<TypeInst>()->domain());
214 pushall(cur->cast<TypeInst>()->ranges());
215 break;
216 case Expression::E_TIID:
217 cur->cast<TIId>()->v().mark();
218 break;
219 }
220 }
221 }
222}
223#undef pushstack
224#undef pushall
225
226void IntLit::rehash(void) {
227 init_hash();
228 std::hash<IntVal> h;
229 cmb_hash(h(_v));
230}
231
232void FloatLit::rehash(void) {
233 init_hash();
234 std::hash<FloatVal> h;
235 cmb_hash(h(_v));
236}
237
238void SetLit::rehash(void) {
239 init_hash();
240 if (isv()) {
241 std::hash<IntVal> h;
242 for (IntSetRanges r0(isv()); r0(); ++r0) {
243 cmb_hash(h(r0.min()));
244 cmb_hash(h(r0.max()));
245 }
246 } else if (fsv()) {
247 std::hash<FloatVal> h;
248 for (FloatSetRanges r0(fsv()); r0(); ++r0) {
249 cmb_hash(h(r0.min()));
250 cmb_hash(h(r0.max()));
251 }
252 } else {
253 for (unsigned int i = v().size(); i--;) cmb_hash(Expression::hash(_v[i]));
254 }
255}
256
257void BoolLit::rehash(void) {
258 init_hash();
259 std::hash<bool> h;
260 cmb_hash(h(_v));
261}
262
263void StringLit::rehash(void) {
264 init_hash();
265 cmb_hash(_v.hash());
266}
267
268void Id::rehash(void) {
269 init_hash();
270 std::hash<long long int> h;
271 if (idn() == -1)
272 cmb_hash(v().hash());
273 else
274 cmb_hash(h(idn()));
275}
276
277ASTString Id::str() const {
278 if (idn() == -1) return v();
279 std::ostringstream oss;
280 oss << "X_INTRODUCED_" << idn() << "_";
281 return oss.str();
282}
283
284void TIId::rehash(void) {
285 init_hash();
286 cmb_hash(_v.hash());
287}
288
289void AnonVar::rehash(void) { init_hash(); }
290
291int ArrayLit::dims(void) const {
292 return _flag_2 ? ((_dims.size() - 2 * _u._al->dims()) / 2)
293 : (_dims.size() == 0 ? 1 : _dims.size() / 2);
294}
295int ArrayLit::min(int i) const {
296 if (_dims.size() == 0) {
297 assert(i == 0);
298 return 1;
299 }
300 return _dims[2 * i];
301}
302int ArrayLit::max(int i) const {
303 if (_dims.size() == 0) {
304 assert(i == 0);
305 return _u._v->size();
306 }
307 return _dims[2 * i + 1];
308}
309int ArrayLit::length(void) const {
310 if (dims() == 0) return 0;
311 int l = max(0) - min(0) + 1;
312 for (int i = 1; i < dims(); i++) l *= (max(i) - min(i) + 1);
313 return l;
314}
315void ArrayLit::make1d(void) {
316 if (_dims.size() != 0) {
317 GCLock lock;
318 if (_flag_2) {
319 std::vector<int> d(2 + _u._al->dims() * 2);
320 int dimOffset = dims() * 2;
321 d[0] = 1;
322 d[1] = length();
323 for (unsigned int i = 2; i < d.size(); i++) {
324 d[i] = _dims[dimOffset + i];
325 }
326 _dims = ASTIntVec(d);
327 } else {
328 std::vector<int> d(2);
329 d[0] = 1;
330 d[1] = length();
331 _dims = ASTIntVec(d);
332 }
333 }
334}
335
336int ArrayLit::origIdx(int i) const {
337 assert(_flag_2);
338 int curIdx = i;
339 int multiplyer = 1;
340 int oIdx = 0;
341 int sliceOffset = dims() * 2;
342 for (int curDim = _u._al->dims() - 1; curDim >= 0; curDim--) {
343 oIdx +=
344 multiplyer *
345 ((curIdx % (_dims[sliceOffset + curDim * 2 + 1] - _dims[sliceOffset + curDim * 2] + 1)) +
346 (_dims[sliceOffset + curDim * 2] - _u._al->min(curDim)));
347 curIdx = curIdx / (_dims[sliceOffset + curDim * 2 + 1] - _dims[sliceOffset + curDim * 2] + 1);
348 multiplyer *= (_u._al->max(curDim) - _u._al->min(curDim) + 1);
349 }
350 return oIdx;
351}
352
353Expression* ArrayLit::slice_get(int i) const {
354 if (!_flag_2) {
355 assert(_u._v->flag());
356 int off = length() - _u._v->size();
357 return i <= off ? (*_u._v)[0] : (*_u._v)[i - off];
358 } else {
359 assert(_flag_2);
360 return (*_u._al)[origIdx(i)];
361 }
362}
363
364void ArrayLit::slice_set(int i, Expression* e) {
365 if (!_flag_2) {
366 assert(_u._v->flag());
367 int off = length() - _u._v->size();
368 if (i <= off) {
369 (*_u._v)[0] = e;
370 } else {
371 (*_u._v)[i - off] = e;
372 }
373 } else {
374 assert(_flag_2);
375 _u._al->set(origIdx(i), e);
376 }
377}
378
379ArrayLit::ArrayLit(const Location& loc, ArrayLit* v, const std::vector<std::pair<int, int> >& dims,
380 const std::vector<std::pair<int, int> >& slice)
381 : Expression(loc, E_ARRAYLIT, Type()) {
382 _flag_1 = false;
383 _flag_2 = true;
384 _u._al = v;
385 assert(slice.size() == v->dims());
386 std::vector<int> d(dims.size() * 2 + 2 * slice.size());
387 for (unsigned int i = static_cast<unsigned int>(dims.size()); i--;) {
388 d[i * 2] = dims[i].first;
389 d[i * 2 + 1] = dims[i].second;
390 }
391 int sliceOffset = static_cast<int>(2 * dims.size());
392 for (unsigned int i = static_cast<unsigned int>(slice.size()); i--;) {
393 d[sliceOffset + i * 2] = slice[i].first;
394 d[sliceOffset + i * 2 + 1] = slice[i].second;
395 }
396 _dims = ASTIntVec(d);
397}
398
399void ArrayLit::compress(const std::vector<Expression*>& v, const std::vector<int>& dims) {
400 if (v.size() >= 4 && Expression::equal(v[0], v[1]) && Expression::equal(v[1], v[2]) &&
401 Expression::equal(v[2], v[3])) {
402 std::vector<Expression*> compress(v.size());
403 compress[0] = v[0];
404 int k = 4;
405 while (k < v.size() && Expression::equal(v[k], v[0])) {
406 k++;
407 }
408 int i = 1;
409 for (; k < v.size(); k++) {
410 compress[i++] = v[k];
411 }
412 compress.resize(i);
413 _u._v = ASTExprVec<Expression>(compress).vec();
414 _u._v->flag(true);
415 _dims = ASTIntVec(dims);
416 } else {
417 _u._v = ASTExprVec<Expression>(v).vec();
418 if (dims.size() != 2 || dims[0] != 1) {
419 // only allocate dims vector if it is not a 1d array indexed from 1
420 _dims = ASTIntVec(dims);
421 }
422 }
423}
424
425ArrayLit::ArrayLit(const Location& loc, const std::vector<Expression*>& v,
426 const std::vector<std::pair<int, int> >& dims)
427 : Expression(loc, E_ARRAYLIT, Type()) {
428 _flag_1 = false;
429 _flag_2 = false;
430 std::vector<int> d(dims.size() * 2);
431 for (unsigned int i = static_cast<unsigned int>(dims.size()); i--;) {
432 d[i * 2] = dims[i].first;
433 d[i * 2 + 1] = dims[i].second;
434 }
435 compress(v, d);
436 rehash();
437}
438
439void ArrayLit::rehash(void) {
440 init_hash();
441 std::hash<int> h;
442 for (unsigned int i = 0; i < _dims.size(); i++) {
443 cmb_hash(h(_dims[i]));
444 }
445 if (_flag_2) {
446 cmb_hash(Expression::hash(_u._al));
447 } else {
448 for (unsigned int i = _u._v->size(); i--;) {
449 cmb_hash(h(i));
450 cmb_hash(Expression::hash((*_u._v)[i]));
451 }
452 }
453}
454
455void ArrayAccess::rehash(void) {
456 init_hash();
457 cmb_hash(Expression::hash(_v));
458 std::hash<unsigned int> h;
459 cmb_hash(h(_idx.size()));
460 for (unsigned int i = _idx.size(); i--;) cmb_hash(Expression::hash(_idx[i]));
461}
462
463Generator::Generator(const std::vector<ASTString>& v, Expression* in, Expression* where) {
464 std::vector<VarDecl*> vd;
465 Location loc = in == NULL ? where->loc() : in->loc();
466 for (unsigned int i = 0; i < v.size(); i++) {
467 VarDecl* nvd = new VarDecl(loc, new TypeInst(loc, Type::parint()), v[i]);
468 nvd->toplevel(false);
469 vd.push_back(nvd);
470 }
471 _v = vd;
472 _in = in;
473 _where = where;
474}
475Generator::Generator(const std::vector<Id*>& v, Expression* in, Expression* where) {
476 std::vector<VarDecl*> vd;
477 for (unsigned int i = 0; i < v.size(); i++) {
478 VarDecl* nvd = new VarDecl(v[i]->loc(), new TypeInst(v[i]->loc(), Type::parint()), v[i]->v());
479 nvd->toplevel(false);
480 vd.push_back(nvd);
481 }
482 _v = vd;
483 _in = in;
484 _where = where;
485}
486Generator::Generator(const std::vector<std::string>& v, Expression* in, Expression* where) {
487 std::vector<VarDecl*> vd;
488 Location loc = in == NULL ? where->loc() : in->loc();
489 for (unsigned int i = 0; i < v.size(); i++) {
490 VarDecl* nvd = new VarDecl(loc, new TypeInst(loc, Type::parint()), ASTString(v[i]));
491 nvd->toplevel(false);
492 vd.push_back(nvd);
493 }
494 _v = vd;
495 _in = in;
496 _where = where;
497}
498Generator::Generator(const std::vector<VarDecl*>& v, Expression* in, Expression* where) {
499 _v = v;
500 _in = in;
501 _where = where;
502}
503Generator::Generator(int pos, Expression* where) {
504 std::vector<VarDecl*> vd;
505 std::ostringstream oss;
506 oss << "__dummy" << pos;
507 VarDecl* nvd =
508 new VarDecl(Location().introduce(), new TypeInst(Location().introduce(), Type::parint()),
509 ASTString(oss.str()));
510 nvd->toplevel(false);
511 vd.push_back(nvd);
512 _v = vd;
513 _in = new ArrayLit(Location().introduce(), std::vector<Expression*>({IntLit::a(0)}));
514 _where = where;
515}
516
517bool Comprehension::set(void) const { return _flag_1; }
518void Comprehension::rehash(void) {
519 init_hash();
520 std::hash<unsigned int> h;
521 cmb_hash(h(set()));
522 cmb_hash(Expression::hash(_e));
523 cmb_hash(h(_g_idx.size()));
524 for (unsigned int i = _g_idx.size(); i--;) {
525 cmb_hash(h(_g_idx[i]));
526 }
527 cmb_hash(h(_g.size()));
528 for (unsigned int i = _g.size(); i--;) {
529 cmb_hash(Expression::hash(_g[i]));
530 }
531}
532
533int Comprehension::n_generators(void) const { return _g_idx.size() - 1; }
534Expression* Comprehension::in(int i) { return _g[_g_idx[i]]; }
535const Expression* Comprehension::in(int i) const { return _g[_g_idx[i]]; }
536const Expression* Comprehension::where(int i) const { return _g[_g_idx[i] + 1]; }
537Expression* Comprehension::where(int i) { return _g[_g_idx[i] + 1]; }
538
539int Comprehension::n_decls(int i) const { return _g_idx[i + 1] - _g_idx[i] - 2; }
540VarDecl* Comprehension::decl(int gen, int i) { return _g[_g_idx[gen] + 2 + i]->cast<VarDecl>(); }
541const VarDecl* Comprehension::decl(int gen, int i) const {
542 return _g[_g_idx[gen] + 2 + i]->cast<VarDecl>();
543}
544
545void ITE::rehash(void) {
546 init_hash();
547 std::hash<unsigned int> h;
548 cmb_hash(h(_e_if_then.size()));
549 for (unsigned int i = _e_if_then.size(); i--;) {
550 cmb_hash(Expression::hash(_e_if_then[i]));
551 }
552 cmb_hash(Expression::hash(e_else()));
553}
554
555BinOpType BinOp::op(void) const { return static_cast<BinOpType>(_sec_id); }
556void BinOp::rehash(void) {
557 init_hash();
558 std::hash<int> h;
559 cmb_hash(h(static_cast<int>(op())));
560 cmb_hash(Expression::hash(_e0));
561 cmb_hash(Expression::hash(_e1));
562}
563
564namespace {
565
566class OpToString {
567protected:
568 Model* rootSetModel;
569
570public:
571 Id* sBOT_PLUS;
572 Id* sBOT_MINUS;
573 Id* sBOT_MULT;
574 Id* sBOT_DIV;
575 Id* sBOT_IDIV;
576 Id* sBOT_MOD;
577 Id* sBOT_POW;
578 Id* sBOT_LE;
579 Id* sBOT_LQ;
580 Id* sBOT_GR;
581 Id* sBOT_GQ;
582 Id* sBOT_EQ;
583 Id* sBOT_NQ;
584 Id* sBOT_IN;
585 Id* sBOT_SUBSET;
586 Id* sBOT_SUPERSET;
587 Id* sBOT_UNION;
588 Id* sBOT_DIFF;
589 Id* sBOT_SYMDIFF;
590 Id* sBOT_INTERSECT;
591 Id* sBOT_PLUSPLUS;
592 Id* sBOT_EQUIV;
593 Id* sBOT_IMPL;
594 Id* sBOT_RIMPL;
595 Id* sBOT_OR;
596 Id* sBOT_AND;
597 Id* sBOT_XOR;
598 Id* sBOT_DOTDOT;
599 Id* sBOT_NOT;
600
601 OpToString(void) {
602 GCLock lock;
603 rootSetModel = new Model();
604 std::vector<Expression*> rootSet;
605 sBOT_PLUS = new Id(Location(), "'+'", NULL);
606 rootSet.push_back(sBOT_PLUS);
607 sBOT_MINUS = new Id(Location(), "'-'", NULL);
608 rootSet.push_back(sBOT_MINUS);
609 sBOT_MULT = new Id(Location(), "'*'", NULL);
610 rootSet.push_back(sBOT_MULT);
611 sBOT_DIV = new Id(Location(), "'/'", NULL);
612 rootSet.push_back(sBOT_DIV);
613 sBOT_IDIV = new Id(Location(), "'div'", NULL);
614 rootSet.push_back(sBOT_IDIV);
615 sBOT_MOD = new Id(Location(), "'mod'", NULL);
616 rootSet.push_back(sBOT_MOD);
617 sBOT_POW = new Id(Location(), "'^'", NULL);
618 rootSet.push_back(sBOT_POW);
619 sBOT_LE = new Id(Location(), "'<'", NULL);
620 rootSet.push_back(sBOT_LE);
621 sBOT_LQ = new Id(Location(), "'<='", NULL);
622 rootSet.push_back(sBOT_LQ);
623 sBOT_GR = new Id(Location(), "'>'", NULL);
624 rootSet.push_back(sBOT_GR);
625 sBOT_GQ = new Id(Location(), "'>='", NULL);
626 rootSet.push_back(sBOT_GQ);
627 sBOT_EQ = new Id(Location(), "'='", NULL);
628 rootSet.push_back(sBOT_EQ);
629 sBOT_NQ = new Id(Location(), "'!='", NULL);
630 rootSet.push_back(sBOT_NQ);
631 sBOT_IN = new Id(Location(), "'in'", NULL);
632 rootSet.push_back(sBOT_IN);
633 sBOT_SUBSET = new Id(Location(), "'subset'", NULL);
634 rootSet.push_back(sBOT_SUBSET);
635 sBOT_SUPERSET = new Id(Location(), "'superset'", NULL);
636 rootSet.push_back(sBOT_SUPERSET);
637 sBOT_UNION = new Id(Location(), "'union'", NULL);
638 rootSet.push_back(sBOT_UNION);
639 sBOT_DIFF = new Id(Location(), "'diff'", NULL);
640 rootSet.push_back(sBOT_DIFF);
641 sBOT_SYMDIFF = new Id(Location(), "'symdiff'", NULL);
642 rootSet.push_back(sBOT_SYMDIFF);
643 sBOT_INTERSECT = new Id(Location(), "'intersect'", NULL);
644 rootSet.push_back(sBOT_INTERSECT);
645 sBOT_PLUSPLUS = new Id(Location(), "'++'", NULL);
646 rootSet.push_back(sBOT_PLUSPLUS);
647 sBOT_EQUIV = new Id(Location(), "'<->'", NULL);
648 rootSet.push_back(sBOT_EQUIV);
649 sBOT_IMPL = new Id(Location(), "'->'", NULL);
650 rootSet.push_back(sBOT_IMPL);
651 sBOT_RIMPL = new Id(Location(), "'<-'", NULL);
652 rootSet.push_back(sBOT_RIMPL);
653 sBOT_OR = new Id(Location(), "'\\/'", NULL);
654 rootSet.push_back(sBOT_OR);
655 sBOT_AND = new Id(Location(), "'/\\'", NULL);
656 rootSet.push_back(sBOT_AND);
657 sBOT_XOR = new Id(Location(), "'xor'", NULL);
658 rootSet.push_back(sBOT_XOR);
659 sBOT_DOTDOT = new Id(Location(), "'..'", NULL);
660 rootSet.push_back(sBOT_DOTDOT);
661 sBOT_NOT = new Id(Location(), "'not'", NULL);
662 rootSet.push_back(sBOT_NOT);
663 rootSetModel->addItem(new ConstraintI(Location(), new ArrayLit(Location(), rootSet)));
664 }
665
666 static OpToString& o(void) {
667 static OpToString _o;
668 return _o;
669 }
670};
671} // namespace
672
673ASTString BinOp::opToString(void) const {
674 switch (op()) {
675 case BOT_PLUS:
676 return OpToString::o().sBOT_PLUS->v();
677 case BOT_MINUS:
678 return OpToString::o().sBOT_MINUS->v();
679 case BOT_MULT:
680 return OpToString::o().sBOT_MULT->v();
681 case BOT_DIV:
682 return OpToString::o().sBOT_DIV->v();
683 case BOT_IDIV:
684 return OpToString::o().sBOT_IDIV->v();
685 case BOT_MOD:
686 return OpToString::o().sBOT_MOD->v();
687 case BOT_POW:
688 return OpToString::o().sBOT_POW->v();
689 case BOT_LE:
690 return OpToString::o().sBOT_LE->v();
691 case BOT_LQ:
692 return OpToString::o().sBOT_LQ->v();
693 case BOT_GR:
694 return OpToString::o().sBOT_GR->v();
695 case BOT_GQ:
696 return OpToString::o().sBOT_GQ->v();
697 case BOT_EQ:
698 return OpToString::o().sBOT_EQ->v();
699 case BOT_NQ:
700 return OpToString::o().sBOT_NQ->v();
701 case BOT_IN:
702 return OpToString::o().sBOT_IN->v();
703 case BOT_SUBSET:
704 return OpToString::o().sBOT_SUBSET->v();
705 case BOT_SUPERSET:
706 return OpToString::o().sBOT_SUPERSET->v();
707 case BOT_UNION:
708 return OpToString::o().sBOT_UNION->v();
709 case BOT_DIFF:
710 return OpToString::o().sBOT_DIFF->v();
711 case BOT_SYMDIFF:
712 return OpToString::o().sBOT_SYMDIFF->v();
713 case BOT_INTERSECT:
714 return OpToString::o().sBOT_INTERSECT->v();
715 case BOT_PLUSPLUS:
716 return OpToString::o().sBOT_PLUSPLUS->v();
717 case BOT_EQUIV:
718 return OpToString::o().sBOT_EQUIV->v();
719 case BOT_IMPL:
720 return OpToString::o().sBOT_IMPL->v();
721 case BOT_RIMPL:
722 return OpToString::o().sBOT_RIMPL->v();
723 case BOT_OR:
724 return OpToString::o().sBOT_OR->v();
725 case BOT_AND:
726 return OpToString::o().sBOT_AND->v();
727 case BOT_XOR:
728 return OpToString::o().sBOT_XOR->v();
729 case BOT_DOTDOT:
730 return OpToString::o().sBOT_DOTDOT->v();
731 default:
732 assert(false);
733 return ASTString("");
734 }
735}
736
737UnOpType UnOp::op(void) const { return static_cast<UnOpType>(_sec_id); }
738void UnOp::rehash(void) {
739 init_hash();
740 std::hash<int> h;
741 cmb_hash(h(static_cast<int>(_sec_id)));
742 cmb_hash(Expression::hash(_e0));
743}
744
745ASTString UnOp::opToString(void) const {
746 switch (op()) {
747 case UOT_PLUS:
748 return OpToString::o().sBOT_PLUS->v();
749 case UOT_MINUS:
750 return OpToString::o().sBOT_MINUS->v();
751 case UOT_NOT:
752 return OpToString::o().sBOT_NOT->v();
753 default:
754 assert(false);
755 return ASTString("");
756 }
757}
758
759void Call::rehash(void) {
760 init_hash();
761 cmb_hash(id().hash());
762 std::hash<FunctionI*> hf;
763 cmb_hash(hf(decl()));
764 std::hash<unsigned int> hu;
765 cmb_hash(hu(n_args()));
766 for (unsigned int i = 0; i < n_args(); i++) cmb_hash(Expression::hash(arg(i)));
767}
768
769void VarDecl::trail(void) {
770 GC::trail(&_e, e());
771 if (_ti->ranges().size() > 0) {
772 GC::trail(reinterpret_cast<Expression**>(&_ti), _ti);
773 }
774}
775
776void VarDecl::rehash(void) {
777 init_hash();
778 cmb_hash(Expression::hash(_ti));
779 cmb_hash(_id->hash());
780 cmb_hash(Expression::hash(_e));
781}
782
783void Let::rehash(void) {
784 init_hash();
785 cmb_hash(Expression::hash(_in));
786 std::hash<unsigned int> h;
787 cmb_hash(h(_let.size()));
788 for (unsigned int i = _let.size(); i--;) cmb_hash(Expression::hash(_let[i]));
789}
790
791Let::Let(const Location& loc, const std::vector<Expression*>& let, Expression* in)
792 : Expression(loc, E_LET, Type()) {
793 _let = ASTExprVec<Expression>(let);
794 std::vector<Expression*> vde(let.size());
795 for (unsigned int i = 0; i < let.size(); i++) {
796 if (VarDecl* vd = Expression::dyn_cast<VarDecl>(let[i])) {
797 vde[i] = vd->e();
798 } else {
799 vde[i] = NULL;
800 }
801 }
802 _let_orig = ASTExprVec<Expression>(vde);
803 _in = in;
804 rehash();
805}
806
807void Let::pushbindings(void) {
808 GC::mark();
809 for (unsigned int i = _let.size(); i--;) {
810 if (VarDecl* vd = _let[i]->dyn_cast<VarDecl>()) {
811 vd->trail();
812 vd->e(_let_orig[i]);
813 }
814 }
815}
816void Let::popbindings(void) {
817 for (unsigned int i = _let.size(); i--;) {
818 if (VarDecl* vd = _let[i]->dyn_cast<VarDecl>()) {
819 GC::untrail();
820 break;
821 }
822 }
823}
824
825void TypeInst::rehash(void) {
826 init_hash();
827 std::hash<unsigned int> h;
828 unsigned int rsize = _ranges.size();
829 cmb_hash(h(rsize));
830 for (unsigned int i = rsize; i--;) cmb_hash(Expression::hash(_ranges[i]));
831 cmb_hash(Expression::hash(domain()));
832}
833
834void TypeInst::setRanges(const std::vector<TypeInst*>& ranges) {
835 _ranges = ASTExprVec<TypeInst>(ranges);
836 if (ranges.size() == 1 && ranges[0] && ranges[0]->isa<TypeInst>() &&
837 ranges[0]->cast<TypeInst>()->domain() && ranges[0]->cast<TypeInst>()->domain()->isa<TIId>() &&
838 !ranges[0]->cast<TypeInst>()->domain()->cast<TIId>()->v().beginsWith("$"))
839 _type.dim(-1);
840 else
841 _type.dim(static_cast<int>(ranges.size()));
842 rehash();
843}
844
845bool TypeInst::hasTiVariable(void) const {
846 if (domain() && domain()->isa<TIId>()) return true;
847 for (unsigned int i = _ranges.size(); i--;)
848 if (_ranges[i]->isa<TIId>()) return true;
849 return false;
850}
851
852namespace {
853Type getType(Expression* e) { return e->type(); }
854Type getType(const Type& t) { return t; }
855const Location& getLoc(Expression* e, FunctionI*) { return e->loc(); }
856const Location& getLoc(const Type&, FunctionI* fi) { return fi->loc(); }
857
858bool isaTIId(Expression* e) {
859 if (TIId* t = Expression::dyn_cast<TIId>(e)) {
860 return !t->v().beginsWith("$");
861 }
862 return false;
863}
864bool isaEnumTIId(Expression* e) {
865 if (TIId* t = Expression::dyn_cast<TIId>(e)) {
866 return t->v().beginsWith("$");
867 }
868 return false;
869}
870
871template <class T>
872Type return_type(EnvI& env, FunctionI* fi, const std::vector<T>& ta, bool strictEnum) {
873 if (fi->id() == constants().var_redef->id()) return Type::varbool();
874 Type ret = fi->ti()->type();
875 ASTString dh;
876 if (fi->ti()->domain() && fi->ti()->domain()->isa<TIId>())
877 dh = fi->ti()->domain()->cast<TIId>()->v();
878 ASTString rh;
879 if (fi->ti()->ranges().size() == 1 && isaTIId(fi->ti()->ranges()[0]->domain()))
880 rh = fi->ti()->ranges()[0]->domain()->cast<TIId>()->v();
881
882 ASTStringMap<Type>::t tmap;
883 for (unsigned int i = 0; i < ta.size(); i++) {
884 TypeInst* tii = fi->params()[i]->ti();
885 if (tii->domain() && tii->domain()->isa<TIId>()) {
886 ASTString tiid = tii->domain()->cast<TIId>()->v();
887 Type tiit = getType(ta[i]);
888 if (tiit.enumId() != 0 && tiit.dim() > 0) {
889 const std::vector<unsigned int>& enumIds = env.getArrayEnum(tiit.enumId());
890 tiit.enumId(enumIds[enumIds.size() - 1]);
891 }
892 tiit.dim(0);
893 if (tii->type().st() == Type::ST_SET) {
894 tiit.st(Type::ST_PLAIN);
895 }
896 if (isaEnumTIId(tii->domain())) {
897 tiit.st(Type::ST_SET);
898 }
899 ASTStringMap<Type>::t::iterator it = tmap.find(tiid);
900 if (it == tmap.end()) {
901 tmap.insert(std::pair<ASTString, Type>(tiid, tiit));
902 } else {
903 if (it->second.dim() > 0) {
904 throw TypeError(
905 env, getLoc(ta[i], fi),
906 "type-inst variable $" + tiid.str() + " used in both array and non-array position");
907 } else {
908 Type tiit_par = tiit;
909 tiit_par.ti(Type::TI_PAR);
910 tiit_par.ot(Type::OT_PRESENT);
911 Type its_par = it->second;
912 its_par.ti(Type::TI_PAR);
913 its_par.ot(Type::OT_PRESENT);
914 if (tiit_par.bt() == Type::BT_TOP || tiit_par.bt() == Type::BT_BOT) {
915 tiit_par.bt(its_par.bt());
916 }
917 if (its_par.bt() == Type::BT_TOP || its_par.bt() == Type::BT_BOT) {
918 its_par.bt(tiit_par.bt());
919 }
920 if (env.isSubtype(tiit_par, its_par, strictEnum)) {
921 if (it->second.bt() == Type::BT_TOP) it->second.bt(tiit.bt());
922 } else if (env.isSubtype(its_par, tiit_par, strictEnum)) {
923 it->second = tiit_par;
924 } else {
925 throw TypeError(env, getLoc(ta[i], fi),
926 "type-inst variable $" + tiid.str() +
927 " instantiated with different types (" + tiit.toString(env) +
928 " vs " + it->second.toString(env) + ")");
929 }
930 }
931 }
932 }
933 if (tii->ranges().size() == 1 && isaTIId(tii->ranges()[0]->domain())) {
934 ASTString tiid = tii->ranges()[0]->domain()->cast<TIId>()->v();
935 Type orig_tiit = getType(ta[i]);
936 if (orig_tiit.dim() == 0) {
937 throw TypeError(env, getLoc(ta[i], fi),
938 "type-inst variable $" + tiid.str() + " must be an array index");
939 }
940 Type tiit = Type::top(orig_tiit.dim());
941 if (orig_tiit.enumId() != 0) {
942 std::vector<unsigned int> enumIds(tiit.dim() + 1);
943 const std::vector<unsigned int>& orig_enumIds = env.getArrayEnum(orig_tiit.enumId());
944 for (unsigned int i = 0; i < enumIds.size() - 1; i++) {
945 enumIds[i] = orig_enumIds[i];
946 }
947 enumIds[enumIds.size() - 1] = 0;
948 tiit.enumId(env.registerArrayEnum(enumIds));
949 }
950 ASTStringMap<Type>::t::iterator it = tmap.find(tiid);
951 if (it == tmap.end()) {
952 tmap.insert(std::pair<ASTString, Type>(tiid, tiit));
953 } else {
954 if (it->second.dim() == 0) {
955 throw TypeError(
956 env, getLoc(ta[i], fi),
957 "type-inst variable $" + tiid.str() + " used in both array and non-array position");
958 } else if (it->second != tiit) {
959 throw TypeError(env, getLoc(ta[i], fi),
960 "type-inst variable $" + tiid.str() +
961 " instantiated with different types (" + tiit.toString(env) + " vs " +
962 it->second.toString(env) + ")");
963 }
964 }
965 } else if (tii->ranges().size() > 0) {
966 for (unsigned int j = 0; j < tii->ranges().size(); j++) {
967 if (isaEnumTIId(tii->ranges()[j]->domain())) {
968 ASTString enumTIId = tii->ranges()[j]->domain()->cast<TIId>()->v();
969 Type tiit = getType(ta[i]);
970 Type enumIdT;
971 if (tiit.enumId() != 0) {
972 unsigned int enumId = env.getArrayEnum(tiit.enumId())[j];
973 enumIdT = Type::parsetenum(enumId);
974 } else {
975 enumIdT = Type::parsetint();
976 }
977 ASTStringMap<Type>::t::iterator it = tmap.find(enumTIId);
978 // TODO: this may clash if the same enum TIId is used for different types
979 // but the same enum
980 if (it == tmap.end()) {
981 tmap.insert(std::pair<ASTString, Type>(enumTIId, enumIdT));
982 } else {
983 if (it->second.enumId() != enumIdT.enumId()) {
984 throw TypeError(
985 env, getLoc(ta[i], fi),
986 "type-inst variable $" + enumTIId.str() + " used for different enum types");
987 }
988 }
989 }
990 }
991 }
992 }
993 if (dh.size() != 0) {
994 ASTStringMap<Type>::t::iterator it = tmap.find(dh);
995 if (it == tmap.end())
996 throw TypeError(env, fi->loc(), "type-inst variable $" + dh.str() + " used but not defined");
997 if (dh.beginsWith("$")) {
998 // this is an enum
999 ret.bt(Type::BT_INT);
1000 } else {
1001 ret.bt(it->second.bt());
1002 if (ret.st() == Type::ST_PLAIN) ret.st(it->second.st());
1003 }
1004 if (fi->ti()->ranges().size() > 0 && it->second.enumId() != 0) {
1005 std::vector<unsigned int> enumIds(fi->ti()->ranges().size() + 1);
1006 for (unsigned int i = 0; i < fi->ti()->ranges().size(); i++) {
1007 enumIds[i] = 0;
1008 }
1009 enumIds[enumIds.size() - 1] = it->second.enumId();
1010 ret.enumId(env.registerArrayEnum(enumIds));
1011 } else {
1012 ret.enumId(it->second.enumId());
1013 }
1014 }
1015 if (rh.size() != 0) {
1016 ASTStringMap<Type>::t::iterator it = tmap.find(rh);
1017 if (it == tmap.end())
1018 throw TypeError(env, fi->loc(), "type-inst variable $" + rh.str() + " used but not defined");
1019 ret.dim(it->second.dim());
1020 if (it->second.enumId() != 0) {
1021 std::vector<unsigned int> enumIds(it->second.dim() + 1);
1022 const std::vector<unsigned int>& orig_enumIds = env.getArrayEnum(it->second.enumId());
1023 for (unsigned int i = 0; i < enumIds.size() - 1; i++) {
1024 enumIds[i] = orig_enumIds[i];
1025 }
1026 enumIds[enumIds.size() - 1] =
1027 ret.enumId() == 0 ? 0 : env.getArrayEnum(ret.enumId())[enumIds.size() - 1];
1028 ret.enumId(env.registerArrayEnum(enumIds));
1029 }
1030
1031 } else if (fi->ti()->ranges().size() > 0) {
1032 std::vector<unsigned int> enumIds(fi->ti()->ranges().size() + 1);
1033 bool hadRealEnum = false;
1034 if (ret.enumId() == 0) {
1035 enumIds[enumIds.size() - 1] = 0;
1036 } else {
1037 enumIds[enumIds.size() - 1] = env.getArrayEnum(ret.enumId())[enumIds.size() - 1];
1038 hadRealEnum = true;
1039 }
1040
1041 for (unsigned int i = 0; i < fi->ti()->ranges().size(); i++) {
1042 if (isaEnumTIId(fi->ti()->ranges()[i]->domain())) {
1043 ASTString enumTIId = fi->ti()->ranges()[i]->domain()->cast<TIId>()->v();
1044 ASTStringMap<Type>::t::iterator it = tmap.find(enumTIId);
1045 if (it == tmap.end())
1046 throw TypeError(env, fi->loc(),
1047 "type-inst variable $" + enumTIId.str() + " used but not defined");
1048 enumIds[i] = it->second.enumId();
1049 hadRealEnum |= (enumIds[i] != 0);
1050 } else {
1051 enumIds[i] = 0;
1052 }
1053 }
1054 if (hadRealEnum) ret.enumId(env.registerArrayEnum(enumIds));
1055 }
1056 return ret;
1057}
1058} // namespace
1059
1060Type FunctionI::rtype(EnvI& env, const std::vector<Expression*>& ta, bool strictEnums) {
1061 return return_type(env, this, ta, strictEnums);
1062}
1063
1064Type FunctionI::rtype(EnvI& env, const std::vector<Type>& ta, bool strictEnums) {
1065 return return_type(env, this, ta, strictEnums);
1066}
1067
1068Type FunctionI::argtype(EnvI& env, const std::vector<Expression*>& ta, int n) {
1069 TypeInst* tii = params()[n]->ti();
1070 if (tii->domain() && tii->domain()->isa<TIId>()) {
1071 Type ty = ta[n]->type();
1072 ty.st(tii->type().st());
1073 ty.dim(tii->type().dim());
1074 ASTString tv = tii->domain()->cast<TIId>()->v();
1075 for (unsigned int i = 0; i < params().size(); i++) {
1076 if (params()[i]->ti()->domain() && params()[i]->ti()->domain()->isa<TIId>() &&
1077 params()[i]->ti()->domain()->cast<TIId>()->v() == tv) {
1078 Type toCheck = ta[i]->type();
1079 toCheck.st(tii->type().st());
1080 toCheck.dim(tii->type().dim());
1081 if (toCheck != ty) {
1082 if (env.isSubtype(ty, toCheck, true)) {
1083 ty = toCheck;
1084 } else {
1085 Type ty_par = ty;
1086 ty_par.ti(Type::TI_PAR);
1087 Type toCheck_par = toCheck;
1088 toCheck_par.ti(Type::TI_PAR);
1089 if (env.isSubtype(ty_par, toCheck_par, true)) {
1090 ty.bt(toCheck.bt());
1091 }
1092 }
1093 }
1094 }
1095 }
1096 return ty;
1097 } else {
1098 return tii->type();
1099 }
1100}
1101
1102bool Expression::equal_internal(const Expression* e0, const Expression* e1) {
1103 switch (e0->eid()) {
1104 case Expression::E_INTLIT:
1105 return e0->cast<IntLit>()->v() == e1->cast<IntLit>()->v();
1106 case Expression::E_FLOATLIT:
1107 return e0->cast<FloatLit>()->v() == e1->cast<FloatLit>()->v();
1108 case Expression::E_SETLIT: {
1109 const SetLit* s0 = e0->cast<SetLit>();
1110 const SetLit* s1 = e1->cast<SetLit>();
1111 if (s0->isv()) {
1112 if (s1->isv()) {
1113 IntSetRanges r0(s0->isv());
1114 IntSetRanges r1(s1->isv());
1115 return Ranges::equal(r0, r1);
1116 } else {
1117 return false;
1118 }
1119 } else if (s0->fsv()) {
1120 if (s1->fsv()) {
1121 FloatSetRanges r0(s0->fsv());
1122 FloatSetRanges r1(s1->fsv());
1123 return Ranges::equal(r0, r1);
1124 } else {
1125 return false;
1126 }
1127 } else {
1128 if (s1->isv() || s1->fsv()) return false;
1129 if (s0->v().size() != s1->v().size()) return false;
1130 for (unsigned int i = 0; i < s0->v().size(); i++)
1131 if (!Expression::equal(s0->v()[i], s1->v()[i])) return false;
1132 return true;
1133 }
1134 }
1135 case Expression::E_BOOLLIT:
1136 return e0->cast<BoolLit>()->v() == e1->cast<BoolLit>()->v();
1137 case Expression::E_STRINGLIT:
1138 return e0->cast<StringLit>()->v() == e1->cast<StringLit>()->v();
1139 case Expression::E_ID: {
1140 const Id* id0 = e0->cast<Id>();
1141 const Id* id1 = e1->cast<Id>();
1142 if (id0->decl() == NULL || id1->decl() == NULL) {
1143 return id0->v() == id1->v() && id0->idn() == id1->idn();
1144 }
1145 return id0->decl() == id1->decl() ||
1146 (id0->decl()->flat() != NULL && id0->decl()->flat() == id1->decl()->flat());
1147 }
1148 case Expression::E_ANON:
1149 return false;
1150 case Expression::E_ARRAYLIT: {
1151 const ArrayLit* a0 = e0->cast<ArrayLit>();
1152 const ArrayLit* a1 = e1->cast<ArrayLit>();
1153 if (a0->size() != a1->size()) return false;
1154 if (a0->_dims.size() != a1->_dims.size()) return false;
1155 for (unsigned int i = 0; i < a0->_dims.size(); i++) {
1156 if (a0->_dims[i] != a1->_dims[i]) {
1157 return false;
1158 }
1159 }
1160 for (unsigned int i = 0; i < a0->size(); i++) {
1161 if (!Expression::equal((*a0)[i], (*a1)[i])) {
1162 return false;
1163 }
1164 }
1165 return true;
1166 }
1167 case Expression::E_ARRAYACCESS: {
1168 const ArrayAccess* a0 = e0->cast<ArrayAccess>();
1169 const ArrayAccess* a1 = e1->cast<ArrayAccess>();
1170 if (!Expression::equal(a0->v(), a1->v())) return false;
1171 if (a0->idx().size() != a1->idx().size()) return false;
1172 for (unsigned int i = 0; i < a0->idx().size(); i++)
1173 if (!Expression::equal(a0->idx()[i], a1->idx()[i])) return false;
1174 return true;
1175 }
1176 case Expression::E_COMP: {
1177 const Comprehension* c0 = e0->cast<Comprehension>();
1178 const Comprehension* c1 = e1->cast<Comprehension>();
1179 if (c0->set() != c1->set()) return false;
1180 if (!Expression::equal(c0->_e, c1->_e)) return false;
1181 if (c0->_g.size() != c1->_g.size()) return false;
1182 for (unsigned int i = 0; i < c0->_g.size(); i++) {
1183 if (!Expression::equal(c0->_g[i], c1->_g[i])) return false;
1184 }
1185 for (unsigned int i = 0; i < c0->_g_idx.size(); i++) {
1186 if (c0->_g_idx[i] != c1->_g_idx[i]) return false;
1187 }
1188 return true;
1189 }
1190 case Expression::E_ITE: {
1191 const ITE* i0 = e0->cast<ITE>();
1192 const ITE* i1 = e1->cast<ITE>();
1193 if (i0->_e_if_then.size() != i1->_e_if_then.size()) return false;
1194 for (unsigned int i = i0->_e_if_then.size(); i--;) {
1195 if (!Expression::equal(i0->_e_if_then[i], i1->_e_if_then[i])) return false;
1196 }
1197 if (!Expression::equal(i0->e_else(), i1->e_else())) return false;
1198 return true;
1199 }
1200 case Expression::E_BINOP: {
1201 const BinOp* b0 = e0->cast<BinOp>();
1202 const BinOp* b1 = e1->cast<BinOp>();
1203 if (b0->op() != b1->op()) return false;
1204 if (!Expression::equal(b0->lhs(), b1->lhs())) return false;
1205 if (!Expression::equal(b0->rhs(), b1->rhs())) return false;
1206 return true;
1207 }
1208 case Expression::E_UNOP: {
1209 const UnOp* b0 = e0->cast<UnOp>();
1210 const UnOp* b1 = e1->cast<UnOp>();
1211 if (b0->op() != b1->op()) return false;
1212 if (!Expression::equal(b0->e(), b1->e())) return false;
1213 return true;
1214 }
1215 case Expression::E_CALL: {
1216 const Call* c0 = e0->cast<Call>();
1217 const Call* c1 = e1->cast<Call>();
1218 if (c0->id() != c1->id()) return false;
1219 if (c0->decl() != c1->decl()) return false;
1220 if (c0->n_args() != c1->n_args()) return false;
1221 for (unsigned int i = 0; i < c0->n_args(); i++)
1222 if (!Expression::equal(c0->arg(i), c1->arg(i))) return false;
1223 return true;
1224 }
1225 case Expression::E_VARDECL: {
1226 const VarDecl* v0 = e0->cast<VarDecl>();
1227 const VarDecl* v1 = e1->cast<VarDecl>();
1228 if (!Expression::equal(v0->ti(), v1->ti())) return false;
1229 if (!Expression::equal(v0->id(), v1->id())) return false;
1230 if (!Expression::equal(v0->e(), v1->e())) return false;
1231 return true;
1232 }
1233 case Expression::E_LET: {
1234 const Let* l0 = e0->cast<Let>();
1235 const Let* l1 = e1->cast<Let>();
1236 if (!Expression::equal(l0->in(), l1->in())) return false;
1237 if (l0->let().size() != l1->let().size()) return false;
1238 for (unsigned int i = l0->let().size(); i--;)
1239 if (!Expression::equal(l0->let()[i], l1->let()[i])) return false;
1240 return true;
1241 }
1242 case Expression::E_TI: {
1243 const TypeInst* t0 = e0->cast<TypeInst>();
1244 const TypeInst* t1 = e1->cast<TypeInst>();
1245 if (t0->ranges().size() != t1->ranges().size()) return false;
1246 for (unsigned int i = t0->ranges().size(); i--;)
1247 if (!Expression::equal(t0->ranges()[i], t1->ranges()[i])) return false;
1248 if (!Expression::equal(t0->domain(), t1->domain())) return false;
1249 return true;
1250 }
1251 case Expression::E_TIID:
1252 return false;
1253 default:
1254 assert(false);
1255 return false;
1256 }
1257}
1258
1259Constants::Constants(void) {
1260 GCLock lock;
1261 TypeInst* ti = new TypeInst(Location(), Type::parbool());
1262 lit_true = new BoolLit(Location(), true);
1263 var_true = new VarDecl(Location(), ti, "_bool_true", lit_true);
1264 lit_false = new BoolLit(Location(), false);
1265 var_false = new VarDecl(Location(), ti, "_bool_false", lit_false);
1266 var_ignore = new VarDecl(Location(), ti, "_bool_ignore");
1267 absent = new Id(Location(), "_absent", NULL);
1268 Type absent_t;
1269 absent_t.bt(Type::BT_BOT);
1270 absent_t.dim(0);
1271 absent_t.st(Type::ST_PLAIN);
1272 absent_t.ot(Type::OT_OPTIONAL);
1273 absent->type(absent_t);
1274
1275 IntSetVal* isv_infty = IntSetVal::a(-IntVal::infinity(), IntVal::infinity());
1276 infinity = new SetLit(Location(), isv_infty);
1277
1278 ids.forall = ASTString("forall");
1279 ids.forall_reif = ASTString("forall_reif");
1280 ids.exists = ASTString("exists");
1281 ids.clause = ASTString("clause");
1282 ids.bool2int = ASTString("bool2int");
1283 ids.int2float = ASTString("int2float");
1284 ids.bool2float = ASTString("bool2float");
1285 ids.assert = ASTString("assert");
1286 ids.trace = ASTString("trace");
1287
1288 ids.sum = ASTString("sum");
1289 ids.lin_exp = ASTString("lin_exp");
1290 ids.element = ASTString("element");
1291
1292 ids.show = ASTString("show");
1293 ids.output = ASTString("output");
1294 ids.fix = ASTString("fix");
1295
1296 ids.int_.lin_eq = ASTString("int_lin_eq");
1297 ids.int_.lin_le = ASTString("int_lin_le");
1298 ids.int_.lin_ne = ASTString("int_lin_ne");
1299 ids.int_.plus = ASTString("int_plus");
1300 ids.int_.minus = ASTString("int_minus");
1301 ids.int_.times = ASTString("int_times");
1302 ids.int_.div = ASTString("int_div");
1303 ids.int_.mod = ASTString("int_mod");
1304 ids.int_.lt = ASTString("int_lt");
1305 ids.int_.le = ASTString("int_le");
1306 ids.int_.gt = ASTString("int_gt");
1307 ids.int_.ge = ASTString("int_ge");
1308 ids.int_.eq = ASTString("int_eq");
1309 ids.int_.ne = ASTString("int_ne");
1310
1311 ids.int_reif.lin_eq = ASTString("int_lin_eq_reif");
1312 ids.int_reif.lin_le = ASTString("int_lin_le_reif");
1313 ids.int_reif.lin_ne = ASTString("int_lin_ne_reif");
1314 ids.int_reif.plus = ASTString("int_plus_reif");
1315 ids.int_reif.minus = ASTString("int_minus_reif");
1316 ids.int_reif.times = ASTString("int_times_reif");
1317 ids.int_reif.div = ASTString("int_div_reif");
1318 ids.int_reif.mod = ASTString("int_mod_reif");
1319 ids.int_reif.lt = ASTString("int_lt_reif");
1320 ids.int_reif.le = ASTString("int_le_reif");
1321 ids.int_reif.gt = ASTString("int_gt_reif");
1322 ids.int_reif.ge = ASTString("int_ge_reif");
1323 ids.int_reif.eq = ASTString("int_eq_reif");
1324 ids.int_reif.ne = ASTString("int_ne_reif");
1325
1326 ids.float_.lin_eq = ASTString("float_lin_eq");
1327 ids.float_.lin_le = ASTString("float_lin_le");
1328 ids.float_.lin_lt = ASTString("float_lin_lt");
1329 ids.float_.lin_ne = ASTString("float_lin_ne");
1330 ids.float_.plus = ASTString("float_plus");
1331 ids.float_.minus = ASTString("float_minus");
1332 ids.float_.times = ASTString("float_times");
1333 ids.float_.div = ASTString("float_div");
1334 ids.float_.mod = ASTString("float_mod");
1335 ids.float_.lt = ASTString("float_lt");
1336 ids.float_.le = ASTString("float_le");
1337 ids.float_.gt = ASTString("float_gt");
1338 ids.float_.ge = ASTString("float_ge");
1339 ids.float_.eq = ASTString("float_eq");
1340 ids.float_.ne = ASTString("float_ne");
1341 ids.float_.in = ASTString("float_in");
1342 ids.float_.dom = ASTString("float_dom");
1343
1344 ids.float_reif.lin_eq = ASTString("float_lin_eq_reif");
1345 ids.float_reif.lin_le = ASTString("float_lin_le_reif");
1346 ids.float_reif.lin_lt = ASTString("float_lin_lt_reif");
1347 ids.float_reif.lin_ne = ASTString("float_lin_ne_reif");
1348 ids.float_reif.plus = ASTString("float_plus_reif");
1349 ids.float_reif.minus = ASTString("float_minus_reif");
1350 ids.float_reif.times = ASTString("float_times_reif");
1351 ids.float_reif.div = ASTString("float_div_reif");
1352 ids.float_reif.mod = ASTString("float_mod_reif");
1353 ids.float_reif.lt = ASTString("float_lt_reif");
1354 ids.float_reif.le = ASTString("float_le_reif");
1355 ids.float_reif.gt = ASTString("float_gt_reif");
1356 ids.float_reif.ge = ASTString("float_ge_reif");
1357 ids.float_reif.eq = ASTString("float_eq_reif");
1358 ids.float_reif.ne = ASTString("float_ne_reif");
1359 ids.float_reif.in = ASTString("float_in_reif");
1360
1361 ids.bool_eq = ASTString("bool_eq");
1362 ids.bool_eq_reif = ASTString("bool_eq_reif");
1363 ids.bool_clause = ASTString("bool_clause");
1364 ids.bool_clause_reif = ASTString("bool_clause_reif");
1365 ids.bool_xor = ASTString("bool_xor");
1366 ids.array_bool_or = ASTString("array_bool_or");
1367 ids.array_bool_and = ASTString("array_bool_and");
1368 ids.set_eq = ASTString("set_eq");
1369 ids.set_in = ASTString("set_in");
1370 ids.set_card = ASTString("set_card");
1371 ids.pow = ASTString("pow");
1372
1373 ids.introduced_var = ASTString("__INTRODUCED");
1374 ids.anonEnumFromStrings = ASTString("anon_enum");
1375
1376 ctx.root = new Id(Location(), ASTString("ctx_root"), NULL);
1377 ctx.root->type(Type::ann());
1378 ctx.pos = new Id(Location(), ASTString("ctx_pos"), NULL);
1379 ctx.pos->type(Type::ann());
1380 ctx.neg = new Id(Location(), ASTString("ctx_neg"), NULL);
1381 ctx.neg->type(Type::ann());
1382 ctx.mix = new Id(Location(), ASTString("ctx_mix"), NULL);
1383 ctx.mix->type(Type::ann());
1384
1385 ann.output_var = new Id(Location(), ASTString("output_var"), NULL);
1386 ann.output_var->type(Type::ann());
1387 ann.output_only = new Id(Location(), ASTString("output_only"), NULL);
1388 ann.output_only->type(Type::ann());
1389 ann.output_array = ASTString("output_array");
1390 ann.add_to_output = new Id(Location(), ASTString("add_to_output"), NULL);
1391 ann.add_to_output->type(Type::ann());
1392 ann.mzn_check_var = new Id(Location(), ASTString("mzn_check_var"), NULL);
1393 ann.mzn_check_var->type(Type::ann());
1394 ann.mzn_check_enum_var = ASTString("mzn_check_enum_var");
1395 ann.is_defined_var = new Id(Location(), ASTString("is_defined_var"), NULL);
1396 ann.is_defined_var->type(Type::ann());
1397 ann.defines_var = ASTString("defines_var");
1398 ann.is_reverse_map = new Id(Location(), ASTString("is_reverse_map"), NULL);
1399 ann.is_reverse_map->type(Type::ann());
1400 ann.promise_total = new Id(Location(), ASTString("promise_total"), NULL);
1401 ann.promise_total->type(Type::ann());
1402 ann._export = new Id(Location(), ASTString("export"), NULL);
1403 ann._export->type(Type::ann());
1404 ann.maybe_partial = new Id(Location(), ASTString("maybe_partial"), NULL);
1405 ann.maybe_partial->type(Type::ann());
1406 ann.doc_comment = ASTString("doc_comment");
1407 ann.mzn_path = ASTString("mzn_path");
1408 ann.is_introduced = ASTString("is_introduced");
1409 ann.user_cut = new Id(Location(), ASTString("user_cut"), NULL);
1410 ann.user_cut->type(Type::ann());
1411 ann.lazy_constraint = new Id(Location(), ASTString("lazy_constraint"), NULL);
1412 ann.lazy_constraint->type(Type::ann());
1413#ifndef NDEBUG
1414 ann.mzn_break_here = new Id(Location(), ASTString("mzn_break_here"), NULL);
1415 ann.mzn_break_here->type(Type::ann());
1416#endif
1417 ann.rhs_from_assignment = new Id(Location(), ASTString("mzn_rhs_from_assignment"), NULL);
1418 ann.rhs_from_assignment->type(Type::ann());
1419 ann.domain_change_constraint = new Id(Location(), ASTString("domain_change_constraint"), NULL);
1420 ann.domain_change_constraint->type(Type::ann());
1421 ann.global_register = ASTString("global_register");
1422
1423 var_redef = new FunctionI(Location(), "__internal_var_redef",
1424 new TypeInst(Location(), Type::varbool()), std::vector<VarDecl*>());
1425
1426 cli.cmdlineData_short_str = ASTString("-D");
1427 cli.cmdlineData_str = ASTString("--cmdline-data");
1428 cli.datafile_str = ASTString("--data");
1429 cli.datafile_short_str = ASTString("-d");
1430 cli.globalsDir_str = ASTString("--globals-dir");
1431 cli.globalsDir_alt_str = ASTString("--mzn-globals-dir");
1432 cli.globalsDir_short_str = ASTString("-G");
1433 cli.help_str = ASTString("--help");
1434 cli.help_short_str = ASTString("-h");
1435 cli.ignoreStdlib_str = ASTString("--ignore-stdlib");
1436 cli.include_str = ASTString("-I");
1437 cli.inputFromStdin_str = ASTString("--input-from-stdin");
1438 cli.instanceCheckOnly_str = ASTString("--instance-check-only");
1439 cli.newfzn_str = ASTString("--newfzn");
1440 cli.no_optimize_str = ASTString("--no-optimize");
1441 cli.no_optimize_alt_str = ASTString("--no-optimise");
1442 cli.no_outputOzn_str = ASTString("--no-output-ozn");
1443 cli.no_outputOzn_short_str = ASTString("-O-");
1444 cli.no_typecheck_str = ASTString("--no-typecheck");
1445 cli.outputBase_str = ASTString("--output-base");
1446 cli.outputFznToStdout_str = ASTString("--output-to-stdout");
1447 cli.outputFznToStdout_alt_str = ASTString("--output-fzn-to-stdout");
1448 cli.outputOznToFile_str = ASTString("--output-ozn-to-file");
1449 cli.outputOznToStdout_str = ASTString("--output-ozn-to-stdout");
1450 cli.outputFznToFile_alt_str = ASTString("--output-fzn-to-file");
1451 cli.outputFznToFile_short_str = ASTString("-o");
1452 cli.outputFznToFile_str = ASTString("--output-to-file");
1453 cli.rangeDomainsOnly_str = ASTString("--only-range-domains");
1454 cli.statistics_str = ASTString("--statistics");
1455 cli.statistics_short_str = ASTString("-s");
1456 cli.stdlib_str = ASTString("--stdlib-dir");
1457 cli.verbose_str = ASTString("--verbose");
1458 cli.verbose_short_str = ASTString("-v");
1459 cli.version_str = ASTString("--version");
1460 cli.werror_str = ASTString("-Werror");
1461
1462 cli.solver.all_sols_str = ASTString("-a");
1463 cli.solver.fzn_solver_str = ASTString("--solver");
1464
1465 opts.cmdlineData = ASTString("cmdlineData");
1466 opts.datafile = ASTString("datafile");
1467 opts.datafiles = ASTString("datafiles");
1468 opts.fznToFile = ASTString("fznToFile");
1469 opts.fznToStdout = ASTString("fznToStdout");
1470 opts.globalsDir = ASTString("globalsDir");
1471 opts.ignoreStdlib = ASTString("ignoreStdlib");
1472 opts.includeDir = ASTString("includeDir");
1473 opts.includePaths = ASTString("includePaths");
1474 opts.inputFromStdin = ASTString("inputStdin");
1475 opts.instanceCheckOnly = ASTString("instanceCheckOnly");
1476 opts.model = ASTString("model");
1477 opts.newfzn = ASTString("newfzn");
1478 opts.noOznOutput = ASTString("noOznOutput");
1479 opts.optimize = ASTString("optimize");
1480 opts.outputBase = ASTString("outputBase");
1481 opts.oznToFile = ASTString("oznToFile");
1482 opts.oznToStdout = ASTString("oznToStdout");
1483 opts.rangeDomainsOnly = ASTString("rangeDomainsOnly");
1484 opts.statistics = ASTString("statistics");
1485 opts.stdlib = ASTString("stdlib");
1486 opts.typecheck = ASTString("typecheck");
1487 opts.verbose = ASTString("verbose");
1488 opts.werror = ASTString("werror");
1489
1490 opts.solver.allSols = ASTString("allSols");
1491 opts.solver.numSols = ASTString("numSols");
1492 opts.solver.threads = ASTString("threads");
1493 opts.solver.fzn_solver = ASTString("fznsolver");
1494 opts.solver.fzn_flags = ASTString("fzn_flags");
1495 opts.solver.fzn_flag = ASTString("fzn_flag");
1496 opts.solver.fzn_time_limit_ms = ASTString("fzn_time_limit_ms");
1497 opts.solver.fzn_sigint = ASTString("fzn_sigint");
1498
1499 cli_cat.general = ASTString("General Options");
1500 cli_cat.io = ASTString("Input/Output Options");
1501 cli_cat.solver = ASTString("Solver Options");
1502 cli_cat.translation = ASTString("Translation Options");
1503
1504 std::vector<Expression*> v;
1505 v.push_back(ti);
1506 v.push_back(lit_true);
1507 v.push_back(var_true);
1508 v.push_back(lit_false);
1509 v.push_back(var_false);
1510 v.push_back(var_ignore);
1511 v.push_back(absent);
1512 v.push_back(infinity);
1513 v.push_back(new StringLit(Location(), ids.forall));
1514 v.push_back(new StringLit(Location(), ids.exists));
1515 v.push_back(new StringLit(Location(), ids.clause));
1516 v.push_back(new StringLit(Location(), ids.bool2int));
1517 v.push_back(new StringLit(Location(), ids.int2float));
1518 v.push_back(new StringLit(Location(), ids.bool2float));
1519 v.push_back(new StringLit(Location(), ids.sum));
1520 v.push_back(new StringLit(Location(), ids.lin_exp));
1521 v.push_back(new StringLit(Location(), ids.element));
1522 v.push_back(new StringLit(Location(), ids.show));
1523 v.push_back(new StringLit(Location(), ids.output));
1524 v.push_back(new StringLit(Location(), ids.fix));
1525
1526 v.push_back(new StringLit(Location(), ids.int_.lin_eq));
1527 v.push_back(new StringLit(Location(), ids.int_.lin_le));
1528 v.push_back(new StringLit(Location(), ids.int_.lin_ne));
1529 v.push_back(new StringLit(Location(), ids.int_.plus));
1530 v.push_back(new StringLit(Location(), ids.int_.minus));
1531 v.push_back(new StringLit(Location(), ids.int_.times));
1532 v.push_back(new StringLit(Location(), ids.int_.div));
1533 v.push_back(new StringLit(Location(), ids.int_.mod));
1534 v.push_back(new StringLit(Location(), ids.int_.lt));
1535 v.push_back(new StringLit(Location(), ids.int_.le));
1536 v.push_back(new StringLit(Location(), ids.int_.gt));
1537 v.push_back(new StringLit(Location(), ids.int_.ge));
1538 v.push_back(new StringLit(Location(), ids.int_.eq));
1539 v.push_back(new StringLit(Location(), ids.int_.ne));
1540
1541 v.push_back(new StringLit(Location(), ids.int_reif.lin_eq));
1542 v.push_back(new StringLit(Location(), ids.int_reif.lin_le));
1543 v.push_back(new StringLit(Location(), ids.int_reif.lin_ne));
1544 v.push_back(new StringLit(Location(), ids.int_reif.plus));
1545 v.push_back(new StringLit(Location(), ids.int_reif.minus));
1546 v.push_back(new StringLit(Location(), ids.int_reif.times));
1547 v.push_back(new StringLit(Location(), ids.int_reif.div));
1548 v.push_back(new StringLit(Location(), ids.int_reif.mod));
1549 v.push_back(new StringLit(Location(), ids.int_reif.lt));
1550 v.push_back(new StringLit(Location(), ids.int_reif.le));
1551 v.push_back(new StringLit(Location(), ids.int_reif.gt));
1552 v.push_back(new StringLit(Location(), ids.int_reif.ge));
1553 v.push_back(new StringLit(Location(), ids.int_reif.eq));
1554 v.push_back(new StringLit(Location(), ids.int_reif.ne));
1555
1556 v.push_back(new StringLit(Location(), ids.float_.lin_eq));
1557 v.push_back(new StringLit(Location(), ids.float_.lin_le));
1558 v.push_back(new StringLit(Location(), ids.float_.lin_lt));
1559 v.push_back(new StringLit(Location(), ids.float_.lin_ne));
1560 v.push_back(new StringLit(Location(), ids.float_.plus));
1561 v.push_back(new StringLit(Location(), ids.float_.minus));
1562 v.push_back(new StringLit(Location(), ids.float_.times));
1563 v.push_back(new StringLit(Location(), ids.float_.div));
1564 v.push_back(new StringLit(Location(), ids.float_.mod));
1565 v.push_back(new StringLit(Location(), ids.float_.lt));
1566 v.push_back(new StringLit(Location(), ids.float_.le));
1567 v.push_back(new StringLit(Location(), ids.float_.gt));
1568 v.push_back(new StringLit(Location(), ids.float_.ge));
1569 v.push_back(new StringLit(Location(), ids.float_.eq));
1570 v.push_back(new StringLit(Location(), ids.float_.ne));
1571 v.push_back(new StringLit(Location(), ids.float_.in));
1572 v.push_back(new StringLit(Location(), ids.float_.dom));
1573
1574 v.push_back(new StringLit(Location(), ids.float_reif.lin_eq));
1575 v.push_back(new StringLit(Location(), ids.float_reif.lin_le));
1576 v.push_back(new StringLit(Location(), ids.float_reif.lin_lt));
1577 v.push_back(new StringLit(Location(), ids.float_reif.lin_ne));
1578 v.push_back(new StringLit(Location(), ids.float_reif.plus));
1579 v.push_back(new StringLit(Location(), ids.float_reif.minus));
1580 v.push_back(new StringLit(Location(), ids.float_reif.times));
1581 v.push_back(new StringLit(Location(), ids.float_reif.div));
1582 v.push_back(new StringLit(Location(), ids.float_reif.mod));
1583 v.push_back(new StringLit(Location(), ids.float_reif.lt));
1584 v.push_back(new StringLit(Location(), ids.float_reif.le));
1585 v.push_back(new StringLit(Location(), ids.float_reif.gt));
1586 v.push_back(new StringLit(Location(), ids.float_reif.ge));
1587 v.push_back(new StringLit(Location(), ids.float_reif.eq));
1588 v.push_back(new StringLit(Location(), ids.float_reif.ne));
1589 v.push_back(new StringLit(Location(), ids.float_reif.in));
1590
1591 v.push_back(new StringLit(Location(), ids.bool_eq));
1592 v.push_back(new StringLit(Location(), ids.bool_eq_reif));
1593 v.push_back(new StringLit(Location(), ids.bool_clause));
1594 v.push_back(new StringLit(Location(), ids.bool_clause_reif));
1595 v.push_back(new StringLit(Location(), ids.bool_xor));
1596 v.push_back(new StringLit(Location(), ids.array_bool_or));
1597 v.push_back(new StringLit(Location(), ids.array_bool_and));
1598 v.push_back(new StringLit(Location(), ids.set_eq));
1599 v.push_back(new StringLit(Location(), ids.set_in));
1600 v.push_back(new StringLit(Location(), ids.set_card));
1601 v.push_back(new StringLit(Location(), ids.pow));
1602
1603 v.push_back(new StringLit(Location(), ids.assert));
1604 v.push_back(new StringLit(Location(), ids.trace));
1605 v.push_back(new StringLit(Location(), ids.introduced_var));
1606 v.push_back(new StringLit(Location(), ids.anonEnumFromStrings));
1607 v.push_back(ctx.root);
1608 v.push_back(ctx.pos);
1609 v.push_back(ctx.neg);
1610 v.push_back(ctx.mix);
1611 v.push_back(ann.output_var);
1612 v.push_back(ann.output_only);
1613 v.push_back(ann.add_to_output);
1614 v.push_back(ann.mzn_check_var);
1615 v.push_back(new StringLit(Location(), ann.mzn_check_enum_var));
1616 v.push_back(new StringLit(Location(), ann.output_array));
1617 v.push_back(ann.is_defined_var);
1618 v.push_back(new StringLit(Location(), ann.defines_var));
1619 v.push_back(ann.is_reverse_map);
1620 v.push_back(ann.promise_total);
1621 v.push_back(ann._export);
1622 v.push_back(ann.maybe_partial);
1623 v.push_back(new StringLit(Location(), ann.doc_comment));
1624 v.push_back(new StringLit(Location(), ann.mzn_path));
1625 v.push_back(new StringLit(Location(), ann.is_introduced));
1626 v.push_back(ann.user_cut);
1627 v.push_back(ann.lazy_constraint);
1628#ifndef NDEBUG
1629 v.push_back(ann.mzn_break_here);
1630#endif
1631 v.push_back(ann.rhs_from_assignment);
1632 v.push_back(ann.domain_change_constraint);
1633 v.push_back(new StringLit(Location(), ann.global_register));
1634
1635 v.push_back(new StringLit(Location(), cli.cmdlineData_short_str));
1636 v.push_back(new StringLit(Location(), cli.cmdlineData_str));
1637 v.push_back(new StringLit(Location(), cli.datafile_short_str));
1638 v.push_back(new StringLit(Location(), cli.datafile_str));
1639 v.push_back(new StringLit(Location(), cli.globalsDir_alt_str));
1640 v.push_back(new StringLit(Location(), cli.globalsDir_short_str));
1641 v.push_back(new StringLit(Location(), cli.globalsDir_str));
1642 v.push_back(new StringLit(Location(), cli.help_short_str));
1643 v.push_back(new StringLit(Location(), cli.help_str));
1644 v.push_back(new StringLit(Location(), cli.ignoreStdlib_str));
1645 v.push_back(new StringLit(Location(), cli.include_str));
1646 v.push_back(new StringLit(Location(), cli.inputFromStdin_str));
1647 v.push_back(new StringLit(Location(), cli.instanceCheckOnly_str));
1648 v.push_back(new StringLit(Location(), cli.newfzn_str));
1649 v.push_back(new StringLit(Location(), cli.no_optimize_alt_str));
1650 v.push_back(new StringLit(Location(), cli.no_optimize_str));
1651 v.push_back(new StringLit(Location(), cli.no_outputOzn_short_str));
1652 v.push_back(new StringLit(Location(), cli.no_outputOzn_str));
1653 v.push_back(new StringLit(Location(), cli.no_typecheck_str));
1654 v.push_back(new StringLit(Location(), cli.outputBase_str));
1655 v.push_back(new StringLit(Location(), cli.outputFznToStdout_alt_str));
1656 v.push_back(new StringLit(Location(), cli.outputFznToStdout_str));
1657 v.push_back(new StringLit(Location(), cli.outputOznToFile_str));
1658 v.push_back(new StringLit(Location(), cli.outputOznToStdout_str));
1659 v.push_back(new StringLit(Location(), cli.outputFznToFile_alt_str));
1660 v.push_back(new StringLit(Location(), cli.outputFznToFile_short_str));
1661 v.push_back(new StringLit(Location(), cli.outputFznToFile_str));
1662 v.push_back(new StringLit(Location(), cli.rangeDomainsOnly_str));
1663 v.push_back(new StringLit(Location(), cli.statistics_short_str));
1664 v.push_back(new StringLit(Location(), cli.statistics_str));
1665 v.push_back(new StringLit(Location(), cli.stdlib_str));
1666 v.push_back(new StringLit(Location(), cli.verbose_short_str));
1667 v.push_back(new StringLit(Location(), cli.verbose_str));
1668 v.push_back(new StringLit(Location(), cli.version_str));
1669 v.push_back(new StringLit(Location(), cli.werror_str));
1670
1671 v.push_back(new StringLit(Location(), cli.solver.all_sols_str));
1672 v.push_back(new StringLit(Location(), cli.solver.fzn_solver_str));
1673
1674 v.push_back(new StringLit(Location(), opts.cmdlineData));
1675 v.push_back(new StringLit(Location(), opts.datafile));
1676 v.push_back(new StringLit(Location(), opts.datafiles));
1677 v.push_back(new StringLit(Location(), opts.fznToFile));
1678 v.push_back(new StringLit(Location(), opts.fznToStdout));
1679 v.push_back(new StringLit(Location(), opts.globalsDir));
1680 v.push_back(new StringLit(Location(), opts.ignoreStdlib));
1681 v.push_back(new StringLit(Location(), opts.includePaths));
1682 v.push_back(new StringLit(Location(), opts.includeDir));
1683 v.push_back(new StringLit(Location(), opts.inputFromStdin));
1684 v.push_back(new StringLit(Location(), opts.instanceCheckOnly));
1685 v.push_back(new StringLit(Location(), opts.model));
1686 v.push_back(new StringLit(Location(), opts.newfzn));
1687 v.push_back(new StringLit(Location(), opts.noOznOutput));
1688 v.push_back(new StringLit(Location(), opts.optimize));
1689 v.push_back(new StringLit(Location(), opts.outputBase));
1690 v.push_back(new StringLit(Location(), opts.oznToFile));
1691 v.push_back(new StringLit(Location(), opts.oznToStdout));
1692 v.push_back(new StringLit(Location(), opts.rangeDomainsOnly));
1693 v.push_back(new StringLit(Location(), opts.statistics));
1694 v.push_back(new StringLit(Location(), opts.stdlib));
1695 v.push_back(new StringLit(Location(), opts.typecheck));
1696 v.push_back(new StringLit(Location(), opts.verbose));
1697 v.push_back(new StringLit(Location(), opts.werror));
1698
1699 v.push_back(new StringLit(Location(), opts.solver.allSols));
1700 v.push_back(new StringLit(Location(), opts.solver.numSols));
1701 v.push_back(new StringLit(Location(), opts.solver.threads));
1702 v.push_back(new StringLit(Location(), opts.solver.fzn_solver));
1703 v.push_back(new StringLit(Location(), opts.solver.fzn_flags));
1704 v.push_back(new StringLit(Location(), opts.solver.fzn_flag));
1705 v.push_back(new StringLit(Location(), opts.solver.fzn_time_limit_ms));
1706 v.push_back(new StringLit(Location(), opts.solver.fzn_sigint));
1707
1708 v.push_back(new StringLit(Location(), cli_cat.general));
1709 v.push_back(new StringLit(Location(), cli_cat.io));
1710 v.push_back(new StringLit(Location(), cli_cat.solver));
1711 v.push_back(new StringLit(Location(), cli_cat.translation));
1712
1713 m = new Model();
1714 m->addItem(new ConstraintI(Location(), new ArrayLit(Location(), v)));
1715 m->addItem(var_redef);
1716}
1717
1718const int Constants::max_array_size;
1719
1720Constants& constants(void) {
1721 static Constants _c;
1722 return _c;
1723}
1724
1725Annotation::~Annotation(void) { delete _s; }
1726
1727bool Annotation::contains(Expression* e) const { return _s && _s->contains(e); }
1728
1729bool Annotation::isEmpty(void) const { return _s == NULL || _s->isEmpty(); }
1730
1731ExpressionSetIter Annotation::begin(void) const {
1732 return _s == NULL ? ExpressionSetIter(true) : _s->begin();
1733}
1734
1735ExpressionSetIter Annotation::end(void) const {
1736 return _s == NULL ? ExpressionSetIter(true) : _s->end();
1737}
1738
1739void Annotation::add(Expression* e) {
1740 if (_s == NULL) _s = new ExpressionSet;
1741 if (e) _s->insert(e);
1742}
1743
1744void Annotation::add(std::vector<Expression*> e) {
1745 if (_s == NULL) _s = new ExpressionSet;
1746 for (unsigned int i = static_cast<unsigned int>(e.size()); i--;)
1747 if (e[i]) _s->insert(e[i]);
1748}
1749
1750void Annotation::remove(Expression* e) {
1751 if (_s && e) {
1752 _s->remove(e);
1753 }
1754}
1755
1756void Annotation::removeCall(const ASTString& id) {
1757 if (_s == NULL) return;
1758 std::vector<Expression*> toRemove;
1759 for (ExpressionSetIter it = _s->begin(); it != _s->end(); ++it) {
1760 if (Call* c = (*it)->dyn_cast<Call>()) {
1761 if (c->id() == id) toRemove.push_back(*it);
1762 }
1763 }
1764 for (unsigned int i = static_cast<unsigned int>(toRemove.size()); i--;) _s->remove(toRemove[i]);
1765}
1766
1767Call* Annotation::getCall(const ASTString& id) const {
1768 if (_s == NULL) return NULL;
1769 for (ExpressionSetIter it = _s->begin(); it != _s->end(); ++it) {
1770 if (Call* c = (*it)->dyn_cast<Call>()) {
1771 if (c->id() == id) return c;
1772 }
1773 }
1774 return NULL;
1775}
1776
1777bool Annotation::containsCall(const MiniZinc::ASTString& id) const {
1778 if (_s == NULL) return false;
1779 for (ExpressionSetIter it = _s->begin(); it != _s->end(); ++it) {
1780 if (Call* c = (*it)->dyn_cast<Call>()) {
1781 if (c->id() == id) return true;
1782 }
1783 }
1784 return false;
1785}
1786
1787void Annotation::clear(void) {
1788 if (_s) {
1789 _s->clear();
1790 }
1791}
1792
1793void Annotation::merge(const Annotation& ann) {
1794 if (ann._s == NULL) return;
1795 if (_s == NULL) {
1796 _s = new ExpressionSet;
1797 }
1798 for (ExpressionSetIter it = ann.begin(); it != ann.end(); ++it) {
1799 _s->insert(*it);
1800 }
1801}
1802
1803Expression* getAnnotation(const Annotation& ann, std::string str) {
1804 for (ExpressionSetIter i = ann.begin(); i != ann.end(); ++i) {
1805 Expression* e = *i;
1806 if ((e->isa<Id>() && e->cast<Id>()->str().str() == str) ||
1807 (e->isa<Call>() && e->cast<Call>()->id().str() == str))
1808 return e;
1809 }
1810 return NULL;
1811}
1812Expression* getAnnotation(const Annotation& ann, const ASTString& str) {
1813 for (ExpressionSetIter i = ann.begin(); i != ann.end(); ++i) {
1814 Expression* e = *i;
1815 if ((e->isa<Id>() && e->cast<Id>()->str() == str) ||
1816 (e->isa<Call>() && e->cast<Call>()->id() == str))
1817 return e;
1818 }
1819 return NULL;
1820}
1821} // namespace MiniZinc