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