this repo has no description
dekker.one
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2
3/*
4 * Main authors:
5 * Pierre Wilke <wilke.pierre@gmail.com>
6 * Guido Tack <guido.tack@monash.edu>
7 */
8
9/* This Source Code Form is subject to the terms of the Mozilla Public
10 * License, v. 2.0. If a copy of the MPL was not distributed with this
11 * file, You can obtain one at http://mozilla.org/MPL/2.0/. */
12
13#include <minizinc/astexception.hh>
14#include <minizinc/hash.hh>
15#include <minizinc/iter.hh>
16#include <minizinc/model.hh>
17#include <minizinc/prettyprinter.hh>
18
19#include <iomanip>
20#include <limits>
21#include <map>
22#include <sstream>
23#include <string>
24#include <utility>
25#include <vector>
26
27namespace MiniZinc {
28
29int precedence(const Expression* e) {
30 if (const auto* bo = e->dynamicCast<BinOp>()) {
31 switch (bo->op()) {
32 case BOT_EQUIV:
33 return 1200;
34 case BOT_IMPL:
35 case BOT_RIMPL:
36 return 1100;
37 case BOT_OR:
38 case BOT_XOR:
39 return 1000;
40 case BOT_AND:
41 return 900;
42 case BOT_LE:
43 case BOT_LQ:
44 case BOT_GR:
45 case BOT_GQ:
46 case BOT_EQ:
47 case BOT_NQ:
48 return 800;
49 case BOT_IN:
50 case BOT_SUBSET:
51 case BOT_SUPERSET:
52 return 700;
53 case BOT_UNION:
54 case BOT_DIFF:
55 case BOT_SYMDIFF:
56 return 600;
57 case BOT_DOTDOT:
58 return 500;
59 case BOT_PLUS:
60 case BOT_MINUS:
61 return 400;
62 case BOT_MULT:
63 case BOT_IDIV:
64 case BOT_MOD:
65 case BOT_DIV:
66 case BOT_INTERSECT:
67 return 300;
68 case BOT_POW:
69 case BOT_PLUSPLUS:
70 return 200;
71 default:
72 assert(false);
73 return -1;
74 }
75
76 } else if (e->isa<Let>()) {
77 return 1300;
78
79 } else {
80 return 0;
81 }
82}
83
84enum Assoc { AS_LEFT, AS_RIGHT, AS_NONE };
85
86Assoc assoc(const BinOp* bo) {
87 switch (bo->op()) {
88 case BOT_LE:
89 case BOT_LQ:
90 case BOT_GR:
91 case BOT_GQ:
92 case BOT_NQ:
93 case BOT_EQ:
94 case BOT_IN:
95 case BOT_SUBSET:
96 case BOT_SUPERSET:
97 case BOT_DOTDOT:
98 return AS_NONE;
99 case BOT_PLUSPLUS:
100 return AS_RIGHT;
101 default:
102 return AS_LEFT;
103 }
104}
105
106enum Parentheses { PN_LEFT = 1, PN_RIGHT = 2 };
107
108Parentheses need_parentheses(const BinOp* bo, const Expression* left, const Expression* right) {
109 int pbo = precedence(bo);
110 int pl = precedence(left);
111 int pr = precedence(right);
112 int ret = static_cast<int>((pbo < pl) || (pbo == pl && assoc(bo) != AS_LEFT));
113 ret += 2 * static_cast<int>((pbo < pr) || (pbo == pr && assoc(bo) != AS_RIGHT));
114 return static_cast<Parentheses>(ret);
115}
116
117void pp_floatval(std::ostream& os, const FloatVal& fv, bool hexFloat) {
118 std::ostringstream oss;
119 if (fv.isFinite()) {
120 if (hexFloat) {
121 throw InternalError("disabled due to hexfloat being not supported by g++ 4.9");
122 // std::hexfloat(oss);
123 oss << fv.toDouble();
124 os << oss.str();
125 }
126 oss << std::setprecision(std::numeric_limits<double>::digits10 + 1);
127 oss << fv;
128 if (oss.str().find('e') == std::string::npos && oss.str().find('.') == std::string::npos) {
129 oss << ".0";
130 }
131 os << oss.str();
132
133 } else {
134 if (fv.isPlusInfinity()) {
135 os << "infinity";
136 } else {
137 os << "-infinity";
138 }
139 }
140}
141
142class PlainPrinter {
143private:
144 bool _flatZinc;
145 EnvI* _env;
146 std::ostream& _os;
147
148public:
149 PlainPrinter(std::ostream& os, bool flatZinc, EnvI* env)
150 : _env(env), _os(os), _flatZinc(flatZinc) {}
151
152 void p(const Type& type, const Expression* e) {
153 switch (type.ti()) {
154 case Type::TI_PAR:
155 break;
156 case Type::TI_VAR:
157 _os << "var ";
158 break;
159 }
160 if (type.ot() == Type::OT_OPTIONAL) {
161 _os << "opt ";
162 }
163 if (type.st() == Type::ST_SET) {
164 _os << "set of ";
165 }
166 if (e == nullptr) {
167 switch (type.bt()) {
168 case Type::BT_INT:
169 _os << "int";
170 break;
171 case Type::BT_BOOL:
172 _os << "bool";
173 break;
174 case Type::BT_FLOAT:
175 _os << "float";
176 break;
177 case Type::BT_STRING:
178 _os << "string";
179 break;
180 case Type::BT_ANN:
181 _os << "ann";
182 break;
183 case Type::BT_BOT:
184 _os << "bot";
185 break;
186 case Type::BT_TOP:
187 _os << "top";
188 break;
189 case Type::BT_UNKNOWN:
190 _os << "???";
191 break;
192 }
193 } else {
194 p(e);
195 }
196 }
197
198 void p(const Annotation& ann) {
199 for (ExpressionSetIter it = ann.begin(); it != ann.end(); ++it) {
200 _os << ":: ";
201 p(*it);
202 }
203 }
204
205 void p(const Expression* e) {
206 if (e == nullptr) {
207 return;
208 }
209 switch (e->eid()) {
210 case Expression::E_INTLIT:
211 _os << e->cast<IntLit>()->v();
212 break;
213 case Expression::E_FLOATLIT: {
214 pp_floatval(_os, e->cast<FloatLit>()->v());
215 } break;
216 case Expression::E_SETLIT: {
217 const SetLit& sl = *e->cast<SetLit>();
218 if (sl.isv() != nullptr) {
219 if (sl.type().bt() == Type::BT_BOOL) {
220 if (sl.isv()->size() == 0) {
221 _os << (_flatZinc ? "true..false" : "{}");
222 } else {
223 _os << "{";
224 if (sl.isv()->min() == 0) {
225 if (sl.isv()->max() == 0) {
226 _os << "false";
227 } else {
228 _os << "false,true";
229 }
230 } else {
231 _os << "true";
232 }
233 _os << "}";
234 }
235 } else {
236 if (sl.isv()->size() == 0) {
237 _os << (_flatZinc ? "1..0" : "{}");
238 } else if (sl.isv()->size() == 1) {
239 _os << sl.isv()->min(0) << ".." << sl.isv()->max(0);
240 } else {
241 if (!sl.isv()->min(0).isFinite()) {
242 _os << sl.isv()->min(0) << ".." << sl.isv()->max(0) << " union ";
243 }
244 _os << "{";
245 bool first = true;
246 for (IntSetRanges isr(sl.isv()); isr(); ++isr) {
247 if (isr.min().isFinite() && isr.max().isFinite()) {
248 for (IntVal i = isr.min(); i <= isr.max(); i++) {
249 if (!first) {
250 _os << ",";
251 }
252 first = false;
253 _os << i;
254 }
255 }
256 }
257 _os << "}";
258 if (!sl.isv()->max(sl.isv()->size() - 1).isFinite()) {
259 _os << " union " << sl.isv()->min(sl.isv()->size() - 1) << ".."
260 << sl.isv()->max(sl.isv()->size() - 1);
261 }
262 }
263 }
264 } else if (sl.fsv() != nullptr) {
265 if (sl.fsv()->size() == 0) {
266 _os << (_flatZinc ? "1.0..0.0" : "{}");
267 } else if (sl.fsv()->size() == 1) {
268 pp_floatval(_os, sl.fsv()->min(0));
269 _os << "..";
270 pp_floatval(_os, sl.fsv()->max(0));
271 } else {
272 bool allSingleton = true;
273 for (FloatSetRanges isr(sl.fsv()); isr(); ++isr) {
274 if (isr.min() != isr.max()) {
275 allSingleton = false;
276 break;
277 }
278 }
279 if (allSingleton) {
280 _os << "{";
281 bool first = true;
282 for (FloatSetRanges isr(sl.fsv()); isr(); ++isr) {
283 if (!first) {
284 _os << ",";
285 }
286 first = false;
287 pp_floatval(_os, isr.min());
288 }
289 _os << "}";
290 } else {
291 bool first = true;
292 for (FloatSetRanges isr(sl.fsv()); isr(); ++isr) {
293 if (!first) {
294 _os << " union ";
295 }
296 first = false;
297 pp_floatval(_os, isr.min());
298 _os << "..";
299 pp_floatval(_os, isr.max());
300 }
301 }
302 }
303 } else {
304 _os << "{";
305 for (unsigned int i = 0; i < sl.v().size(); i++) {
306 p(sl.v()[i]);
307 if (i < sl.v().size() - 1) {
308 _os << ",";
309 }
310 }
311 _os << "}";
312 }
313 } break;
314 case Expression::E_BOOLLIT:
315 _os << (e->cast<BoolLit>()->v() ? "true" : "false");
316 break;
317 case Expression::E_STRINGLIT:
318 _os << "\"" << Printer::escapeStringLit(e->cast<StringLit>()->v()) << "\"";
319 break;
320 case Expression::E_ID: {
321 if (e == constants().absent) {
322 _os << "<>";
323 } else {
324 const Id* id = e->cast<Id>();
325 if (id->decl() != nullptr) {
326 id = id->decl()->id();
327 }
328 if (id->idn() == -1) {
329 _os << id->v();
330 } else {
331 _os << "X_INTRODUCED_" << id->idn() << "_";
332 }
333 }
334 } break;
335 case Expression::E_TIID:
336 _os << "$" << e->cast<TIId>()->v();
337 break;
338 case Expression::E_ANON:
339 _os << "_";
340 break;
341 case Expression::E_ARRAYLIT: {
342 const ArrayLit& al = *e->cast<ArrayLit>();
343 unsigned int n = al.dims();
344 if (n == 1 && al.min(0) == 1) {
345 _os << "[";
346 for (unsigned int i = 0; i < al.size(); i++) {
347 p(al[i]);
348 if (i < al.size() - 1) {
349 _os << ",";
350 }
351 }
352 _os << "]";
353 } else if (n == 2 && al.min(0) == 1 && al.min(1) == 1 && al.max(1) != 0) {
354 _os << "[|";
355 for (int i = 0; i < al.max(0); i++) {
356 for (int j = 0; j < al.max(1); j++) {
357 p(al[i * al.max(1) + j]);
358 if (j < al.max(1) - 1) {
359 _os << ",";
360 }
361 }
362 if (i < al.max(0) - 1) {
363 _os << "|";
364 }
365 }
366 _os << "|]";
367 } else {
368 _os << "array" << n << "d(";
369 for (int i = 0; i < al.dims(); i++) {
370 _os << al.min(i) << ".." << al.max(i);
371 _os << ",";
372 }
373 _os << "[";
374 for (unsigned int i = 0; i < al.size(); i++) {
375 p(al[i]);
376 if (i < al.size() - 1) {
377 _os << ",";
378 }
379 }
380 _os << "])";
381 }
382 } break;
383 case Expression::E_ARRAYACCESS: {
384 const ArrayAccess& aa = *e->cast<ArrayAccess>();
385 p(aa.v());
386 _os << "[";
387 for (unsigned int i = 0; i < aa.idx().size(); i++) {
388 p(aa.idx()[i]);
389 if (i < aa.idx().size() - 1) {
390 _os << ",";
391 }
392 }
393 _os << "]";
394 } break;
395 case Expression::E_COMP: {
396 const Comprehension& c = *e->cast<Comprehension>();
397 _os << (c.set() ? "{" : "[");
398 p(c.e());
399 _os << " | ";
400 for (int i = 0; i < c.numberOfGenerators(); i++) {
401 for (int j = 0; j < c.numberOfDecls(i); j++) {
402 auto* ident = c.decl(i, j)->id();
403 if (ident->idn() == -1) {
404 _os << ident->v();
405 } else {
406 _os << "X_INTRODUCED_" << ident->idn() << "_";
407 }
408 if (j < c.numberOfDecls(i) - 1) {
409 _os << ",";
410 }
411 }
412 if (c.in(i) == nullptr) {
413 _os << " = ";
414 p(c.where(i));
415 } else {
416 _os << " in ";
417 p(c.in(i));
418 if (c.where(i) != nullptr) {
419 _os << " where ";
420 p(c.where(i));
421 }
422 }
423 if (i < c.numberOfGenerators()) {
424 _os << ", ";
425 }
426 }
427 _os << (c.set() ? "}" : "]");
428 } break;
429 case Expression::E_ITE: {
430 const ITE& ite = *e->cast<ITE>();
431 for (int i = 0; i < ite.size(); i++) {
432 _os << (i == 0 ? "if " : " elseif ");
433 p(ite.ifExpr(i));
434 _os << " then ";
435 p(ite.thenExpr(i));
436 }
437 if (ite.elseExpr() != nullptr) {
438 _os << " else ";
439 p(ite.elseExpr());
440 }
441 _os << " endif";
442 } break;
443 case Expression::E_BINOP: {
444 const BinOp& bo = *e->cast<BinOp>();
445 Parentheses ps = need_parentheses(&bo, bo.lhs(), bo.rhs());
446 if ((ps & PN_LEFT) != 0) {
447 _os << "(";
448 }
449 p(bo.lhs());
450 if ((ps & PN_LEFT) != 0) {
451 _os << ")";
452 }
453 switch (bo.op()) {
454 case BOT_PLUS:
455 _os << "+";
456 break;
457 case BOT_MINUS:
458 _os << "-";
459 break;
460 case BOT_MULT:
461 _os << "*";
462 break;
463 case BOT_POW:
464 _os << "^";
465 break;
466 case BOT_DIV:
467 _os << "/";
468 break;
469 case BOT_IDIV:
470 _os << " div ";
471 break;
472 case BOT_MOD:
473 _os << " mod ";
474 break;
475 case BOT_LE:
476 _os << " < ";
477 break;
478 case BOT_LQ:
479 _os << "<=";
480 break;
481 case BOT_GR:
482 _os << " > ";
483 break;
484 case BOT_GQ:
485 _os << ">=";
486 break;
487 case BOT_EQ:
488 _os << "==";
489 break;
490 case BOT_NQ:
491 _os << "!=";
492 break;
493 case BOT_IN:
494 _os << " in ";
495 break;
496 case BOT_SUBSET:
497 _os << " subset ";
498 break;
499 case BOT_SUPERSET:
500 _os << " superset ";
501 break;
502 case BOT_UNION:
503 _os << " union ";
504 break;
505 case BOT_DIFF:
506 _os << " diff ";
507 break;
508 case BOT_SYMDIFF:
509 _os << " symdiff ";
510 break;
511 case BOT_INTERSECT:
512 _os << " intersect ";
513 break;
514 case BOT_PLUSPLUS:
515 _os << "++";
516 break;
517 case BOT_EQUIV:
518 _os << " <-> ";
519 break;
520 case BOT_IMPL:
521 _os << " -> ";
522 break;
523 case BOT_RIMPL:
524 _os << " <- ";
525 break;
526 case BOT_OR:
527 _os << " \\/ ";
528 break;
529 case BOT_AND:
530 _os << " /\\ ";
531 break;
532 case BOT_XOR:
533 _os << " xor ";
534 break;
535 case BOT_DOTDOT:
536 _os << "..";
537 break;
538 default:
539 assert(false);
540 break;
541 }
542
543 if ((ps & PN_RIGHT) != 0) {
544 _os << "(";
545 }
546 p(bo.rhs());
547 if ((ps & PN_RIGHT) != 0) {
548 _os << ")";
549 }
550 } break;
551 case Expression::E_UNOP: {
552 const UnOp& uo = *e->cast<UnOp>();
553 switch (uo.op()) {
554 case UOT_NOT:
555 _os << "not ";
556 break;
557 case UOT_PLUS:
558 _os << "+";
559 break;
560 case UOT_MINUS:
561 _os << "-";
562 break;
563 default:
564 assert(false);
565 break;
566 }
567 bool needParen = (uo.e()->isa<BinOp>() || uo.e()->isa<UnOp>() || !uo.ann().isEmpty());
568 if (needParen) {
569 _os << "(";
570 }
571 p(uo.e());
572 if (needParen) {
573 _os << ")";
574 }
575 } break;
576 case Expression::E_CALL: {
577 const Call& c = *e->cast<Call>();
578 _os << c.id() << "(";
579 for (unsigned int i = 0; i < c.argCount(); i++) {
580 p(c.arg(i));
581 if (i < c.argCount() - 1) {
582 _os << ",";
583 }
584 }
585 _os << ")";
586 } break;
587 case Expression::E_VARDECL: {
588 const VarDecl& vd = *e->cast<VarDecl>();
589 p(vd.ti());
590 if (!vd.ti()->isEnum() && (vd.id()->idn() != -1 || vd.id()->v().size() > 0)) {
591 _os << ":";
592 }
593 if (vd.id()->idn() != -1) {
594 _os << " X_INTRODUCED_" << vd.id()->idn() << "_";
595 } else if (vd.id()->v().size() != 0) {
596 _os << " " << vd.id()->v();
597 }
598 if (vd.introduced()) {
599 _os << " ::var_is_introduced ";
600 }
601 p(vd.ann());
602 if (vd.e() != nullptr) {
603 _os << " = ";
604 p(vd.e());
605 }
606 } break;
607 case Expression::E_LET: {
608 const Let& l = *e->cast<Let>();
609 _os << "let {";
610
611 for (unsigned int i = 0; i < l.let().size(); i++) {
612 const Expression* li = l.let()[i];
613 if (!li->isa<VarDecl>()) {
614 _os << "constraint ";
615 }
616 p(li);
617 if (i < l.let().size() - 1) {
618 _os << ", ";
619 }
620 }
621 _os << "} in (";
622 p(l.in());
623 _os << ")";
624 } break;
625 case Expression::E_TI: {
626 const TypeInst& ti = *e->cast<TypeInst>();
627 if (ti.isEnum()) {
628 _os << "enum";
629 } else if (_env != nullptr) {
630 _os << ti.type().toString(*_env);
631 } else {
632 if (ti.isarray()) {
633 _os << "array [";
634 for (unsigned int i = 0; i < ti.ranges().size(); i++) {
635 p(Type::parint(), ti.ranges()[i]);
636 if (i < ti.ranges().size() - 1) {
637 _os << ",";
638 }
639 }
640 _os << "] of ";
641 }
642 p(ti.type(), ti.domain());
643 }
644 }
645 }
646 if (!e->isa<VarDecl>()) {
647 p(e->ann());
648 }
649 }
650
651 void p(const Item* i) {
652 if (i == nullptr) {
653 return;
654 }
655 if (i->removed()) {
656 _os << "% ";
657 }
658 switch (i->iid()) {
659 case Item::II_INC:
660 _os << "include \"" << i->cast<IncludeI>()->f() << "\"";
661 break;
662 case Item::II_VD:
663 p(i->cast<VarDeclI>()->e());
664 break;
665 case Item::II_ASN:
666 _os << i->cast<AssignI>()->id() << " = ";
667 p(i->cast<AssignI>()->e());
668 break;
669 case Item::II_CON:
670 _os << "constraint ";
671 p(i->cast<ConstraintI>()->e());
672 break;
673 case Item::II_SOL: {
674 const auto* si = i->cast<SolveI>();
675 _os << "solve ";
676 p(si->ann());
677 switch (si->st()) {
678 case SolveI::ST_SAT:
679 _os << " satisfy";
680 break;
681 case SolveI::ST_MIN:
682 _os << " minimize ";
683 p(si->e());
684 break;
685 case SolveI::ST_MAX:
686 _os << " maximize ";
687 p(si->e());
688 break;
689 }
690 } break;
691 case Item::II_OUT:
692 _os << "output ";
693 p(i->cast<OutputI>()->e());
694 break;
695 case Item::II_FUN: {
696 const FunctionI& fi = *i->cast<FunctionI>();
697 if (fi.ti()->type().isAnn() && fi.e() == nullptr) {
698 _os << "annotation ";
699 } else if (fi.ti()->type() == Type::parbool()) {
700 _os << "test ";
701 } else if (fi.ti()->type() == Type::varbool()) {
702 _os << "predicate ";
703 } else {
704 _os << "function ";
705 p(fi.ti());
706 _os << " : ";
707 }
708 _os << fi.id();
709 if (fi.params().size() > 0) {
710 _os << "(";
711 for (unsigned int j = 0; j < fi.params().size(); j++) {
712 p(fi.params()[j]);
713 if (j < fi.params().size() - 1) {
714 _os << ",";
715 }
716 }
717 _os << ")";
718 }
719 p(fi.ann());
720 if (fi.e() != nullptr) {
721 _os << " = ";
722 p(fi.e());
723 }
724 } break;
725 }
726 _os << ";" << std::endl;
727 }
728};
729
730template <class T>
731class ExpressionMapper {
732protected:
733 T& _t;
734
735public:
736 ExpressionMapper(T& t) : _t(t) {}
737 typename T::ret map(const Expression* e) {
738 switch (e->eid()) {
739 case Expression::E_INTLIT:
740 return _t.mapIntLit(*e->cast<IntLit>());
741 case Expression::E_FLOATLIT:
742 return _t.mapFloatLit(*e->cast<FloatLit>());
743 case Expression::E_SETLIT:
744 return _t.mapSetLit(*e->cast<SetLit>());
745 case Expression::E_BOOLLIT:
746 return _t.mapBoolLit(*e->cast<BoolLit>());
747 case Expression::E_STRINGLIT:
748 return _t.mapStringLit(*e->cast<StringLit>());
749 case Expression::E_ID:
750 return _t.mapId(*e->cast<Id>());
751 case Expression::E_ANON:
752 return _t.mapAnonVar(*e->cast<AnonVar>());
753 case Expression::E_ARRAYLIT:
754 return _t.mapArrayLit(*e->cast<ArrayLit>());
755 case Expression::E_ARRAYACCESS:
756 return _t.mapArrayAccess(*e->cast<ArrayAccess>());
757 case Expression::E_COMP:
758 return _t.mapComprehension(*e->cast<Comprehension>());
759 case Expression::E_ITE:
760 return _t.mapITE(*e->cast<ITE>());
761 case Expression::E_BINOP:
762 return _t.mapBinOp(*e->cast<BinOp>());
763 case Expression::E_UNOP:
764 return _t.mapUnOp(*e->cast<UnOp>());
765 case Expression::E_CALL:
766 return _t.mapCall(*e->cast<Call>());
767 case Expression::E_VARDECL:
768 return _t.mapVarDecl(*e->cast<VarDecl>());
769 case Expression::E_LET:
770 return _t.mapLet(*e->cast<Let>());
771 case Expression::E_TI:
772 return _t.mapTypeInst(*e->cast<TypeInst>());
773 case Expression::E_TIID:
774 return _t.mapTIId(*e->cast<TIId>());
775 default:
776 assert(false);
777 return typename T::ret();
778 break;
779 }
780 }
781};
782
783class Document {
784private:
785 int _level;
786
787public:
788 Document() : _level(0) {}
789 virtual ~Document() {}
790 int getLevel() const { return _level; }
791 // Make this object a child of "d".
792 virtual void setParent(Document* d) { _level = d->_level + 1; }
793};
794
795class BreakPoint : public Document {
796private:
797 bool _dontSimplify;
798
799public:
800 BreakPoint() { _dontSimplify = false; }
801 BreakPoint(bool ds) { _dontSimplify = ds; }
802 ~BreakPoint() override {}
803 void setDontSimplify(bool b) { _dontSimplify = b; }
804 bool getDontSimplify() const { return _dontSimplify; }
805};
806
807class StringDocument : public Document {
808private:
809 std::string _stringDocument;
810
811public:
812 StringDocument() {}
813 ~StringDocument() override {}
814
815 StringDocument(std::string s) : _stringDocument(std::move(s)) {}
816
817 std::string getString() { return _stringDocument; }
818 void setString(std::string s) { _stringDocument = std::move(s); }
819};
820
821class DocumentList : public Document {
822private:
823 std::vector<Document*> _docs;
824 std::string _beginToken;
825 std::string _separator;
826 std::string _endToken;
827 bool _unbreakable;
828 bool _alignment;
829
830public:
831 ~DocumentList() override {
832 std::vector<Document*>::iterator it;
833 for (it = _docs.begin(); it != _docs.end(); it++) {
834 delete *it;
835 }
836 }
837 DocumentList(std::string beginToken = "", std::string separator = "", std::string endToken = "",
838 bool alignment = true);
839
840 void addDocumentToList(Document* d) {
841 _docs.push_back(d);
842 d->setParent(this);
843 }
844
845 void setParent(Document* d) override {
846 Document::setParent(d);
847 std::vector<Document*>::iterator it;
848 for (it = _docs.begin(); it != _docs.end(); it++) {
849 (*it)->setParent(this);
850 }
851 }
852
853 void addStringToList(std::string s) { addDocumentToList(new StringDocument(std::move(s))); }
854
855 void addBreakPoint(bool b = false) { addDocumentToList(new BreakPoint(b)); }
856
857 std::vector<Document*> getDocs() { return _docs; }
858
859 void setList(std::vector<Document*> ld) { _docs = std::move(ld); }
860
861 std::string getBeginToken() { return _beginToken; }
862
863 std::string getEndToken() { return _endToken; }
864
865 std::string getSeparator() { return _separator; }
866
867 bool getUnbreakable() const { return _unbreakable; }
868
869 void setUnbreakable(bool b) { _unbreakable = b; }
870
871 bool getAlignment() const { return _alignment; }
872};
873
874DocumentList::DocumentList(std::string beginToken, std::string separator, std::string endToken,
875 bool alignment) {
876 _beginToken = std::move(beginToken);
877 _separator = std::move(separator);
878 _endToken = std::move(endToken);
879 _alignment = alignment;
880 _unbreakable = false;
881}
882
883class Line {
884private:
885 int _indentation;
886 int _lineLength;
887 std::vector<std::string> _text;
888
889public:
890 Line() : _indentation(0), _lineLength(0), _text(0) {}
891 Line(const Line&) = default;
892 Line(const int indent) : _indentation(indent), _lineLength(0), _text(0) {}
893 Line& operator=(const Line&) = default;
894 bool operator==(const Line& l) { return &l == this; }
895
896 void setIndentation(int i) { _indentation = i; }
897
898 int getLength() const { return _lineLength; }
899 int getIndentation() const { return _indentation; }
900 int getSpaceLeft(int maxwidth) const;
901 void addString(const std::string& s);
902 void concatenateLines(Line& l);
903
904 void print(std::ostream& os) const {
905 for (int i = 0; i < getIndentation(); i++) {
906 os << " ";
907 }
908 std::vector<std::string>::const_iterator it;
909 for (it = _text.begin(); it != _text.end(); it++) {
910 os << (*it);
911 }
912 os << "\n";
913 }
914};
915
916int Line::getSpaceLeft(int maxwidth) const { return maxwidth - _lineLength - _indentation; }
917void Line::addString(const std::string& s) {
918 _lineLength += static_cast<int>(s.size());
919 _text.push_back(s);
920}
921void Line::concatenateLines(Line& l) {
922 _text.insert(_text.end(), l._text.begin(), l._text.end());
923 _lineLength += l._lineLength;
924}
925
926class LinesToSimplify {
927private:
928 std::map<int, std::vector<int> > _lines;
929
930 // (i,j) in parent <=> j can only be simplified if i is simplified
931 std::vector<std::pair<int, int> > _parent;
932 /*
933 * if i can't simplify, remove j and his parents
934 */
935 // mostRecentlyAdded[level] = line of the most recently added
936 std::map<int, int> _mostRecentlyAdded;
937
938public:
939 std::vector<int>* getLinesForPriority(int p) {
940 std::map<int, std::vector<int> >::iterator it;
941 for (it = _lines.begin(); it != _lines.end(); it++) {
942 if (it->first == p) {
943 return &(it->second);
944 }
945 }
946 return nullptr;
947 }
948 void addLine(int p, int l, int par = -1) {
949 if (par == -1) {
950 for (int i = p - 1; i >= 0; i--) {
951 auto it = _mostRecentlyAdded.find(i);
952 if (it != _mostRecentlyAdded.end()) {
953 par = it->second;
954 break;
955 }
956 }
957 }
958 if (par != -1) {
959 _parent.emplace_back(l, par);
960 }
961 _mostRecentlyAdded.insert(std::pair<int, int>(p, l));
962 std::map<int, std::vector<int> >::iterator it;
963 for (it = _lines.begin(); it != _lines.end(); it++) {
964 if (it->first == p) {
965 it->second.push_back(l);
966 return;
967 }
968 }
969 std::vector<int> v;
970 v.push_back(l);
971 _lines.insert(std::pair<int, std::vector<int> >(p, v));
972 }
973 void decrementLine(std::vector<int>* vec, int l) {
974 std::vector<int>::iterator vit;
975 if (vec != nullptr) {
976 for (vit = vec->begin(); vit != vec->end(); vit++) {
977 if (*vit >= l) {
978 *vit = *vit - 1;
979 }
980 }
981 }
982 // Now the map
983 std::map<int, std::vector<int> >::iterator it;
984 for (it = _lines.begin(); it != _lines.end(); it++) {
985 for (vit = it->second.begin(); vit != it->second.end(); vit++) {
986 if (*vit >= l) {
987 *vit = *vit - 1;
988 }
989 }
990 }
991 // And the parent table
992 std::vector<std::pair<int, int> >::iterator vpit;
993 for (vpit = _parent.begin(); vpit != _parent.end(); vpit++) {
994 if (vpit->first >= l) {
995 vpit->first--;
996 }
997 if (vpit->second >= l) {
998 vpit->second--;
999 }
1000 }
1001 }
1002 void remove(LinesToSimplify& lts) {
1003 std::map<int, std::vector<int> >::iterator it;
1004 for (it = lts._lines.begin(); it != lts._lines.end(); it++) {
1005 std::vector<int>::iterator vit;
1006 for (vit = it->second.begin(); vit != it->second.end(); vit++) {
1007 remove(nullptr, *vit, false);
1008 }
1009 }
1010 }
1011 void remove(std::vector<int>* v, int i, bool success = true) {
1012 if (v != nullptr) {
1013 v->erase(std::remove(v->begin(), v->end(), i), v->end());
1014 }
1015 for (auto& line : _lines) {
1016 std::vector<int>& l = line.second;
1017 l.erase(std::remove(l.begin(), l.end(), i), l.end());
1018 }
1019 // Call on its parent
1020 if (!success) {
1021 std::vector<std::pair<int, int> >::iterator vpit;
1022 for (vpit = _parent.begin(); vpit != _parent.end(); vpit++) {
1023 if (vpit->first == i && vpit->second != i && vpit->second != -1) {
1024 remove(v, vpit->second, false);
1025 }
1026 }
1027 }
1028 }
1029 std::vector<int>* getLinesToSimplify() {
1030 auto* vec = new std::vector<int>();
1031 std::map<int, std::vector<int> >::iterator it;
1032 for (it = _lines.begin(); it != _lines.end(); it++) {
1033 std::vector<int>& svec = it->second;
1034 vec->insert(vec->begin(), svec.begin(), svec.end());
1035 }
1036 return vec;
1037 }
1038};
1039
1040Document* expression_to_document(const Expression* e);
1041Document* annotation_to_document(const Annotation& ann);
1042Document* tiexpression_to_document(const Type& type, const Expression* e) {
1043 auto* dl = new DocumentList("", "", "", false);
1044 switch (type.ti()) {
1045 case Type::TI_PAR:
1046 break;
1047 case Type::TI_VAR:
1048 dl->addStringToList("var ");
1049 break;
1050 }
1051 if (type.ot() == Type::OT_OPTIONAL) {
1052 dl->addStringToList("opt ");
1053 }
1054 if (type.st() == Type::ST_SET) {
1055 dl->addStringToList("set of ");
1056 }
1057 if (e == nullptr) {
1058 switch (type.bt()) {
1059 case Type::BT_INT:
1060 dl->addStringToList("int");
1061 break;
1062 case Type::BT_BOOL:
1063 dl->addStringToList("bool");
1064 break;
1065 case Type::BT_FLOAT:
1066 dl->addStringToList("float");
1067 break;
1068 case Type::BT_STRING:
1069 dl->addStringToList("string");
1070 break;
1071 case Type::BT_ANN:
1072 dl->addStringToList("ann");
1073 break;
1074 case Type::BT_BOT:
1075 dl->addStringToList("bot");
1076 break;
1077 case Type::BT_TOP:
1078 dl->addStringToList("top");
1079 break;
1080 case Type::BT_UNKNOWN:
1081 dl->addStringToList("???");
1082 break;
1083 }
1084 } else {
1085 dl->addDocumentToList(expression_to_document(e));
1086 }
1087 return dl;
1088}
1089
1090class ExpressionDocumentMapper {
1091public:
1092 typedef Document* ret;
1093 static ret mapIntLit(const IntLit& il) {
1094 std::ostringstream oss;
1095 oss << il.v();
1096 return new StringDocument(oss.str());
1097 }
1098 static ret mapFloatLit(const FloatLit& fl) {
1099 std::ostringstream oss;
1100 pp_floatval(oss, fl.v());
1101 return new StringDocument(oss.str());
1102 }
1103 static ret mapSetLit(const SetLit& sl) {
1104 DocumentList* dl;
1105 if (sl.isv() != nullptr) {
1106 if (sl.type().bt() == Type::BT_BOOL) {
1107 if (sl.isv()->size() == 0) {
1108 dl = new DocumentList("true..false", "", "");
1109 } else {
1110 if (sl.isv()->min() == 0) {
1111 if (sl.isv()->max() == 0) {
1112 dl = new DocumentList("{false}", "", "");
1113 } else {
1114 dl = new DocumentList("{false,true}", "", "");
1115 }
1116 } else {
1117 dl = new DocumentList("{true}", "", "");
1118 }
1119 }
1120 } else {
1121 if (sl.isv()->size() == 0) {
1122 dl = new DocumentList("1..0", "", "");
1123 } else if (sl.isv()->size() == 1) {
1124 dl = new DocumentList("", "..", "");
1125 {
1126 std::ostringstream oss;
1127 oss << sl.isv()->min(0);
1128 dl->addDocumentToList(new StringDocument(oss.str()));
1129 }
1130 {
1131 std::ostringstream oss;
1132 oss << sl.isv()->max(0);
1133 dl->addDocumentToList(new StringDocument(oss.str()));
1134 }
1135 } else {
1136 dl = new DocumentList("{", ", ", "}", true);
1137 IntSetRanges isr(sl.isv());
1138 for (Ranges::ToValues<IntSetRanges> isv(isr); isv(); ++isv) {
1139 std::ostringstream oss;
1140 oss << isv.val();
1141 dl->addDocumentToList(new StringDocument(oss.str()));
1142 }
1143 }
1144 }
1145 } else if (sl.fsv() != nullptr) {
1146 if (sl.fsv()->size() == 0) {
1147 dl = new DocumentList("1.0..0.0", "", "");
1148 } else if (sl.fsv()->size() == 1) {
1149 dl = new DocumentList("", "..", "");
1150 {
1151 std::ostringstream oss;
1152 pp_floatval(oss, sl.fsv()->min(0));
1153 dl->addDocumentToList(new StringDocument(oss.str()));
1154 }
1155 {
1156 std::ostringstream oss;
1157 pp_floatval(oss, sl.fsv()->max(0));
1158 dl->addDocumentToList(new StringDocument(oss.str()));
1159 }
1160 } else {
1161 dl = new DocumentList("", " union ", "", true);
1162 FloatSetRanges fsr(sl.fsv());
1163 for (; fsr(); ++fsr) {
1164 std::ostringstream oss;
1165 pp_floatval(oss, fsr.min());
1166 oss << "..";
1167 pp_floatval(oss, fsr.max());
1168 dl->addDocumentToList(new StringDocument(oss.str()));
1169 }
1170 }
1171
1172 } else {
1173 dl = new DocumentList("{", ", ", "}", true);
1174 for (unsigned int i = 0; i < sl.v().size(); i++) {
1175 dl->addDocumentToList(expression_to_document((sl.v()[i])));
1176 }
1177 }
1178 return dl;
1179 }
1180 static ret mapBoolLit(const BoolLit& bl) {
1181 return new StringDocument(std::string(bl.v() ? "true" : "false"));
1182 }
1183 static ret mapStringLit(const StringLit& sl) {
1184 std::ostringstream oss;
1185 oss << "\"" << Printer::escapeStringLit(sl.v()) << "\"";
1186 return new StringDocument(oss.str());
1187 }
1188 static ret mapId(const Id& id) {
1189 if (&id == constants().absent) {
1190 return new StringDocument("<>");
1191 }
1192 if (id.idn() == -1) {
1193 return new StringDocument(std::string(id.v().c_str(), id.v().size()));
1194 }
1195 std::ostringstream oss;
1196 oss << "X_INTRODUCED_" << id.idn() << "_";
1197 return new StringDocument(oss.str());
1198 }
1199 static ret mapTIId(const TIId& id) {
1200 std::ostringstream ss;
1201 ss << "$" << id.v();
1202 return new StringDocument(ss.str());
1203 }
1204 static ret mapAnonVar(const AnonVar& /*v*/) { return new StringDocument("_"); }
1205 static ret mapArrayLit(const ArrayLit& al) {
1206 /// TODO: test multi-dimensional arrays handling
1207 DocumentList* dl;
1208 unsigned int n = al.dims();
1209 if (n == 1 && al.min(0) == 1) {
1210 dl = new DocumentList("[", ", ", "]");
1211 for (unsigned int i = 0; i < al.size(); i++) {
1212 dl->addDocumentToList(expression_to_document(al[i]));
1213 }
1214 } else if (n == 2 && al.min(0) == 1 && al.min(1) == 1) {
1215 dl = new DocumentList("[| ", " | ", " |]");
1216 for (int i = 0; i < al.max(0); i++) {
1217 auto* row = new DocumentList("", ", ", "");
1218 for (int j = 0; j < al.max(1); j++) {
1219 row->addDocumentToList(expression_to_document(al[i * al.max(1) + j]));
1220 }
1221 dl->addDocumentToList(row);
1222 if (i != al.max(0) - 1) {
1223 dl->addBreakPoint(true); // dont simplify
1224 }
1225 }
1226 } else {
1227 dl = new DocumentList("", "", "");
1228 std::stringstream oss;
1229 oss << "array" << n << "d";
1230 dl->addStringToList(oss.str());
1231 auto* args = new DocumentList("(", ", ", ")");
1232
1233 for (int i = 0; i < al.dims(); i++) {
1234 oss.str("");
1235 oss << al.min(i) << ".." << al.max(i);
1236 args->addStringToList(oss.str());
1237 }
1238 auto* array = new DocumentList("[", ", ", "]");
1239 for (unsigned int i = 0; i < al.size(); i++) {
1240 array->addDocumentToList(expression_to_document(al[i]));
1241 }
1242 args->addDocumentToList(array);
1243 dl->addDocumentToList(args);
1244 }
1245 return dl;
1246 }
1247 static ret mapArrayAccess(const ArrayAccess& aa) {
1248 auto* dl = new DocumentList("", "", "");
1249
1250 dl->addDocumentToList(expression_to_document(aa.v()));
1251 auto* args = new DocumentList("[", ", ", "]");
1252 for (unsigned int i = 0; i < aa.idx().size(); i++) {
1253 args->addDocumentToList(expression_to_document(aa.idx()[i]));
1254 }
1255 dl->addDocumentToList(args);
1256 return dl;
1257 }
1258 static ret mapComprehension(const Comprehension& c) {
1259 std::ostringstream oss;
1260 DocumentList* dl;
1261 if (c.set()) {
1262 dl = new DocumentList("{ ", " | ", " }");
1263 } else {
1264 dl = new DocumentList("[ ", " | ", " ]");
1265 }
1266 dl->addDocumentToList(expression_to_document(c.e()));
1267 auto* head = new DocumentList("", " ", "");
1268 auto* generators = new DocumentList("", ", ", "");
1269 for (int i = 0; i < c.numberOfGenerators(); i++) {
1270 auto* gen = new DocumentList("", "", "");
1271 auto* idents = new DocumentList("", ", ", "");
1272 for (int j = 0; j < c.numberOfDecls(i); j++) {
1273 std::ostringstream ss;
1274 Id* ident = c.decl(i, j)->id();
1275 if (ident->idn() == -1) {
1276 ss << ident->v();
1277 } else {
1278 ss << "X_INTRODUCED_" << ident->idn() << "_";
1279 }
1280 idents->addStringToList(ss.str());
1281 }
1282 gen->addDocumentToList(idents);
1283 if (c.in(i) == nullptr) {
1284 gen->addStringToList(" = ");
1285 gen->addDocumentToList(expression_to_document(c.where(i)));
1286 } else {
1287 gen->addStringToList(" in ");
1288 gen->addDocumentToList(expression_to_document(c.in(i)));
1289 if (c.where(i) != nullptr) {
1290 gen->addStringToList(" where ");
1291 gen->addDocumentToList(expression_to_document(c.where(i)));
1292 }
1293 }
1294 generators->addDocumentToList(gen);
1295 }
1296 head->addDocumentToList(generators);
1297 dl->addDocumentToList(head);
1298
1299 return dl;
1300 }
1301 static ret mapITE(const ITE& ite) {
1302 auto* dl = new DocumentList("", "", "");
1303 for (int i = 0; i < ite.size(); i++) {
1304 std::string beg = (i == 0 ? "if " : " elseif ");
1305 dl->addStringToList(beg);
1306 dl->addDocumentToList(expression_to_document(ite.ifExpr(i)));
1307 dl->addStringToList(" then ");
1308
1309 auto* ifdoc = new DocumentList("", "", "", false);
1310 ifdoc->addBreakPoint();
1311 ifdoc->addDocumentToList(expression_to_document(ite.thenExpr(i)));
1312 dl->addDocumentToList(ifdoc);
1313 dl->addStringToList(" ");
1314 }
1315 dl->addBreakPoint();
1316 dl->addStringToList("else ");
1317
1318 auto* elsedoc = new DocumentList("", "", "", false);
1319 elsedoc->addBreakPoint();
1320 elsedoc->addDocumentToList(expression_to_document(ite.elseExpr()));
1321 dl->addDocumentToList(elsedoc);
1322 dl->addStringToList(" ");
1323 dl->addBreakPoint();
1324 dl->addStringToList("endif");
1325
1326 return dl;
1327 }
1328 static ret mapBinOp(const BinOp& bo) {
1329 Parentheses ps = need_parentheses(&bo, bo.lhs(), bo.rhs());
1330 DocumentList* opLeft;
1331 DocumentList* dl;
1332 DocumentList* opRight;
1333 bool linebreak = false;
1334 if ((ps & PN_LEFT) != 0) {
1335 opLeft = new DocumentList("(", " ", ")");
1336 } else {
1337 opLeft = new DocumentList("", " ", "");
1338 }
1339 opLeft->addDocumentToList(expression_to_document(bo.lhs()));
1340 std::string op;
1341 switch (bo.op()) {
1342 case BOT_PLUS:
1343 op = "+";
1344 break;
1345 case BOT_MINUS:
1346 op = "-";
1347 break;
1348 case BOT_MULT:
1349 op = "*";
1350 break;
1351 case BOT_POW:
1352 op = "^";
1353 break;
1354 case BOT_DIV:
1355 op = "/";
1356 break;
1357 case BOT_IDIV:
1358 op = " div ";
1359 break;
1360 case BOT_MOD:
1361 op = " mod ";
1362 break;
1363 case BOT_LE:
1364 op = " < ";
1365 break;
1366 case BOT_LQ:
1367 op = "<=";
1368 break;
1369 case BOT_GR:
1370 op = " > ";
1371 break;
1372 case BOT_GQ:
1373 op = ">=";
1374 break;
1375 case BOT_EQ:
1376 op = "==";
1377 break;
1378 case BOT_NQ:
1379 op = "!=";
1380 break;
1381 case BOT_IN:
1382 op = " in ";
1383 break;
1384 case BOT_SUBSET:
1385 op = " subset ";
1386 break;
1387 case BOT_SUPERSET:
1388 op = " superset ";
1389 break;
1390 case BOT_UNION:
1391 op = " union ";
1392 break;
1393 case BOT_DIFF:
1394 op = " diff ";
1395 break;
1396 case BOT_SYMDIFF:
1397 op = " symdiff ";
1398 break;
1399 case BOT_INTERSECT:
1400 op = " intersect ";
1401 break;
1402 case BOT_PLUSPLUS:
1403 op = "++";
1404 linebreak = true;
1405 break;
1406 case BOT_EQUIV:
1407 op = " <-> ";
1408 break;
1409 case BOT_IMPL:
1410 op = " -> ";
1411 break;
1412 case BOT_RIMPL:
1413 op = " <- ";
1414 break;
1415 case BOT_OR:
1416 op = " \\/ ";
1417 linebreak = true;
1418 break;
1419 case BOT_AND:
1420 op = " /\\ ";
1421 linebreak = true;
1422 break;
1423 case BOT_XOR:
1424 op = " xor ";
1425 break;
1426 case BOT_DOTDOT:
1427 op = "..";
1428 break;
1429 default:
1430 assert(false);
1431 break;
1432 }
1433 dl = new DocumentList("", op, "");
1434
1435 if ((ps & PN_RIGHT) != 0) {
1436 opRight = new DocumentList("(", " ", ")");
1437 } else {
1438 opRight = new DocumentList("", "", "");
1439 }
1440 opRight->addDocumentToList(expression_to_document(bo.rhs()));
1441 dl->addDocumentToList(opLeft);
1442 if (linebreak) {
1443 dl->addBreakPoint();
1444 }
1445 dl->addDocumentToList(opRight);
1446
1447 return dl;
1448 }
1449 static ret mapUnOp(const UnOp& uo) {
1450 auto* dl = new DocumentList("", "", "");
1451 std::string op;
1452 switch (uo.op()) {
1453 case UOT_NOT:
1454 op = "not ";
1455 break;
1456 case UOT_PLUS:
1457 op = "+";
1458 break;
1459 case UOT_MINUS:
1460 op = "-";
1461 break;
1462 default:
1463 assert(false);
1464 break;
1465 }
1466 dl->addStringToList(op);
1467 DocumentList* unop;
1468 bool needParen = (uo.e()->isa<BinOp>() || uo.e()->isa<UnOp>());
1469 if (needParen) {
1470 unop = new DocumentList("(", " ", ")");
1471 } else {
1472 unop = new DocumentList("", " ", "");
1473 }
1474
1475 unop->addDocumentToList(expression_to_document(uo.e()));
1476 dl->addDocumentToList(unop);
1477 return dl;
1478 }
1479 static ret mapCall(const Call& c) {
1480 if (c.argCount() == 1) {
1481 /*
1482 * if we have only one argument, and this is an array comprehension,
1483 * we convert it into the following syntax
1484 * forall (f(i,j) | i in 1..10)
1485 * -->
1486 * forall (i in 1..10) (f(i,j))
1487 */
1488
1489 const Expression* e = c.arg(0);
1490 if (e->isa<Comprehension>()) {
1491 const auto* com = e->cast<Comprehension>();
1492 if (!com->set()) {
1493 auto* dl = new DocumentList("", " ", "");
1494 dl->addStringToList(std::string(c.id().c_str(), c.id().size()));
1495 auto* args = new DocumentList("", " ", "", false);
1496 auto* generators = new DocumentList("", ", ", "");
1497
1498 for (int i = 0; i < com->numberOfGenerators(); i++) {
1499 auto* gen = new DocumentList("", "", "");
1500 auto* idents = new DocumentList("", ", ", "");
1501 for (int j = 0; j < com->numberOfDecls(i); j++) {
1502 idents->addStringToList(std::string(com->decl(i, j)->id()->v().c_str(),
1503 com->decl(i, j)->id()->v().size()));
1504 }
1505 gen->addDocumentToList(idents);
1506 if (com->in(i) == nullptr) {
1507 gen->addStringToList(" = ");
1508 gen->addDocumentToList(expression_to_document(com->where(i)));
1509 } else {
1510 gen->addStringToList(" in ");
1511 gen->addDocumentToList(expression_to_document(com->in(i)));
1512 if (com->where(i) != nullptr) {
1513 gen->addStringToList(" where ");
1514 gen->addDocumentToList(expression_to_document(com->where(i)));
1515 }
1516 }
1517 generators->addDocumentToList(gen);
1518 }
1519
1520 args->addStringToList("(");
1521 args->addDocumentToList(generators);
1522 args->addStringToList(")");
1523
1524 args->addStringToList("(");
1525 args->addBreakPoint();
1526 args->addDocumentToList(expression_to_document(com->e()));
1527
1528 dl->addDocumentToList(args);
1529 dl->addBreakPoint();
1530 dl->addStringToList(")");
1531
1532 return dl;
1533 }
1534 }
1535 }
1536 std::ostringstream beg;
1537 beg << c.id() << "(";
1538 auto* dl = new DocumentList(beg.str(), ", ", ")");
1539 for (unsigned int i = 0; i < c.argCount(); i++) {
1540 dl->addDocumentToList(expression_to_document(c.arg(i)));
1541 }
1542 return dl;
1543 }
1544 static ret mapVarDecl(const VarDecl& vd) {
1545 std::ostringstream oss;
1546 auto* dl = new DocumentList("", "", "");
1547 dl->addDocumentToList(expression_to_document(vd.ti()));
1548 if (vd.id()->idn() == -1) {
1549 if (vd.id()->v().size() != 0) {
1550 oss << ": " << vd.id()->v().c_str();
1551 }
1552 } else {
1553 oss << ": X_INTRODUCED_" << vd.id()->idn() << "_";
1554 }
1555 dl->addStringToList(oss.str());
1556
1557 if (vd.introduced()) {
1558 dl->addStringToList(" ::var_is_introduced ");
1559 }
1560 if (!vd.ann().isEmpty()) {
1561 dl->addDocumentToList(annotation_to_document(vd.ann()));
1562 }
1563 if (vd.e() != nullptr) {
1564 dl->addStringToList(" = ");
1565 dl->addDocumentToList(expression_to_document(vd.e()));
1566 }
1567 return dl;
1568 }
1569 static ret mapLet(const Let& l) {
1570 auto* letin = new DocumentList("", "", "", false);
1571 auto* lets = new DocumentList("", " ", "", true);
1572 auto* inexpr = new DocumentList("", "", "");
1573 bool ds = l.let().size() > 1;
1574
1575 for (unsigned int i = 0; i < l.let().size(); i++) {
1576 if (i != 0) {
1577 lets->addBreakPoint(ds);
1578 }
1579 auto* exp = new DocumentList("", " ", ",");
1580 const Expression* li = l.let()[i];
1581 if (!li->isa<VarDecl>()) {
1582 exp->addStringToList("constraint");
1583 }
1584 exp->addDocumentToList(expression_to_document(li));
1585 lets->addDocumentToList(exp);
1586 }
1587
1588 inexpr->addDocumentToList(expression_to_document(l.in()));
1589 letin->addBreakPoint(ds);
1590 letin->addDocumentToList(lets);
1591
1592 auto* letin2 = new DocumentList("", "", "", false);
1593
1594 letin2->addBreakPoint();
1595 letin2->addDocumentToList(inexpr);
1596
1597 auto* dl = new DocumentList("", "", "");
1598 dl->addStringToList("let {");
1599 dl->addDocumentToList(letin);
1600 dl->addBreakPoint(ds);
1601 dl->addStringToList("} in (");
1602 dl->addDocumentToList(letin2);
1603 // dl->addBreakPoint();
1604 dl->addStringToList(")");
1605 return dl;
1606 }
1607 static ret mapTypeInst(const TypeInst& ti) {
1608 auto* dl = new DocumentList("", "", "");
1609 if (ti.isarray()) {
1610 dl->addStringToList("array [");
1611 auto* ran = new DocumentList("", ", ", "");
1612 for (unsigned int i = 0; i < ti.ranges().size(); i++) {
1613 ran->addDocumentToList(tiexpression_to_document(Type::parint(), ti.ranges()[i]));
1614 }
1615 dl->addDocumentToList(ran);
1616 dl->addStringToList("] of ");
1617 }
1618 dl->addDocumentToList(tiexpression_to_document(ti.type(), ti.domain()));
1619 return dl;
1620 }
1621};
1622
1623Document* annotation_to_document(const Annotation& ann) {
1624 auto* dl = new DocumentList(" :: ", " :: ", "");
1625 for (ExpressionSetIter it = ann.begin(); it != ann.end(); ++it) {
1626 dl->addDocumentToList(expression_to_document(*it));
1627 }
1628 return dl;
1629}
1630
1631Document* expression_to_document(const Expression* e) {
1632 if (e == nullptr) {
1633 return new StringDocument("NULL");
1634 }
1635 ExpressionDocumentMapper esm;
1636 ExpressionMapper<ExpressionDocumentMapper> em(esm);
1637 auto* dl = new DocumentList("", "", "");
1638 Document* s = em.map(e);
1639 dl->addDocumentToList(s);
1640 if (!e->isa<VarDecl>() && !e->ann().isEmpty()) {
1641 dl->addDocumentToList(annotation_to_document(e->ann()));
1642 }
1643 return dl;
1644}
1645
1646class ItemDocumentMapper {
1647public:
1648 typedef Document* ret;
1649 static ret mapIncludeI(const IncludeI& ii) {
1650 std::ostringstream oss;
1651 oss << "include \"" << ii.f() << "\";";
1652 return new StringDocument(oss.str());
1653 }
1654 static ret mapVarDeclI(const VarDeclI& vi) {
1655 auto* dl = new DocumentList("", " ", ";");
1656 dl->addDocumentToList(expression_to_document(vi.e()));
1657 return dl;
1658 }
1659 static ret mapAssignI(const AssignI& ai) {
1660 auto* dl = new DocumentList("", " = ", ";");
1661 dl->addStringToList(std::string(ai.id().c_str(), ai.id().size()));
1662 dl->addDocumentToList(expression_to_document(ai.e()));
1663 return dl;
1664 }
1665 static ret mapConstraintI(const ConstraintI& ci) {
1666 auto* dl = new DocumentList("constraint ", " ", ";");
1667 dl->addDocumentToList(expression_to_document(ci.e()));
1668 return dl;
1669 }
1670 static ret mapSolveI(const SolveI& si) {
1671 auto* dl = new DocumentList("", "", ";");
1672 dl->addStringToList("solve");
1673 if (!si.ann().isEmpty()) {
1674 dl->addDocumentToList(annotation_to_document(si.ann()));
1675 }
1676 switch (si.st()) {
1677 case SolveI::ST_SAT:
1678 dl->addStringToList(" satisfy");
1679 break;
1680 case SolveI::ST_MIN:
1681 dl->addStringToList(" minimize ");
1682 dl->addDocumentToList(expression_to_document(si.e()));
1683 break;
1684 case SolveI::ST_MAX:
1685 dl->addStringToList(" maximize ");
1686 dl->addDocumentToList(expression_to_document(si.e()));
1687 break;
1688 }
1689 return dl;
1690 }
1691 static ret mapOutputI(const OutputI& oi) {
1692 auto* dl = new DocumentList("output ", " ", ";");
1693 dl->addDocumentToList(expression_to_document(oi.e()));
1694 return dl;
1695 }
1696 static ret mapFunctionI(const FunctionI& fi) {
1697 DocumentList* dl;
1698 if (fi.ti()->type().isAnn() && fi.e() == nullptr) {
1699 dl = new DocumentList("annotation ", " ", ";", false);
1700 } else if (fi.ti()->type() == Type::parbool()) {
1701 dl = new DocumentList("test ", "", ";", false);
1702 } else if (fi.ti()->type() == Type::varbool()) {
1703 dl = new DocumentList("predicate ", "", ";", false);
1704 } else {
1705 dl = new DocumentList("function ", "", ";", false);
1706 dl->addDocumentToList(expression_to_document(fi.ti()));
1707 dl->addStringToList(": ");
1708 }
1709 dl->addStringToList(std::string(fi.id().c_str(), fi.id().size()));
1710 if (fi.params().size() > 0) {
1711 auto* params = new DocumentList("(", ", ", ")");
1712 for (unsigned int i = 0; i < fi.params().size(); i++) {
1713 auto* par = new DocumentList("", "", "");
1714 par->setUnbreakable(true);
1715 par->addDocumentToList(expression_to_document(fi.params()[i]));
1716 params->addDocumentToList(par);
1717 }
1718 dl->addDocumentToList(params);
1719 }
1720 if (!fi.ann().isEmpty()) {
1721 dl->addDocumentToList(annotation_to_document(fi.ann()));
1722 }
1723 if (fi.e() != nullptr) {
1724 dl->addStringToList(" = ");
1725 dl->addBreakPoint();
1726 dl->addDocumentToList(expression_to_document(fi.e()));
1727 }
1728
1729 return dl;
1730 }
1731};
1732
1733class PrettyPrinter {
1734public:
1735 /*
1736 * \brief Constructor for class Pretty Printer
1737 * \param maxwidth (default 80) : number of rows
1738 * \param indentationBase : spaces that represent the atomic number of spaces
1739 * \param sim : whether we want to simplify the result
1740 * \param deepSimp : whether we want to simplify at each breakpoint or not
1741 */
1742 PrettyPrinter(int _maxwidth = 80, int _indentationBase = 4, bool sim = false,
1743 bool deepSimp = false);
1744
1745 void print(Document* d);
1746 void print(std::ostream& os) const;
1747
1748private:
1749 int _maxwidth;
1750 int _indentationBase;
1751 int _currentLine;
1752 int _currentItem;
1753 std::vector<std::vector<Line> > _items;
1754 std::vector<LinesToSimplify> _linesToSimplify;
1755 std::vector<LinesToSimplify> _linesNotToSimplify;
1756 bool _simp;
1757 bool _deeplySimp;
1758
1759 void addItem();
1760
1761 void addLine(int indentation, bool bp = false, bool simpl = false, int level = 0);
1762 static std::string printSpaces(int n);
1763 const std::vector<Line>& getCurrentItemLines() const;
1764
1765 void printDocument(Document* d, bool alignment, int alignmentCol, const std::string& before = "",
1766 const std::string& after = "");
1767 void printDocList(DocumentList* d, int alignmentCol, const std::string& before = "",
1768 const std::string& after = "");
1769 void printStringDoc(StringDocument* d, bool alignment, int alignmentCol,
1770 const std::string& before = "", const std::string& after = "");
1771 void printString(const std::string& s, bool alignment, int alignmentCol);
1772 bool simplify(int item, int line, std::vector<int>* vec);
1773 void simplifyItem(int item);
1774};
1775
1776void PrettyPrinter::print(Document* d) {
1777 addItem();
1778 addLine(0);
1779 printDocument(d, true, 0);
1780 if (_simp) {
1781 simplifyItem(_currentItem);
1782 }
1783}
1784
1785PrettyPrinter::PrettyPrinter(int maxwidth, int indentationBase, bool sim, bool deepsim) {
1786 _maxwidth = maxwidth;
1787 _indentationBase = indentationBase;
1788 _currentLine = -1;
1789 _currentItem = -1;
1790
1791 _simp = sim;
1792 _deeplySimp = deepsim;
1793}
1794const std::vector<Line>& PrettyPrinter::getCurrentItemLines() const { return _items[_currentItem]; }
1795
1796void PrettyPrinter::addLine(int indentation, bool bp, bool simpl, int level) {
1797 _items[_currentItem].push_back(Line(indentation));
1798 _currentLine++;
1799 if (bp && _deeplySimp) {
1800 _linesToSimplify[_currentItem].addLine(level, _currentLine);
1801 if (!simpl) {
1802 _linesNotToSimplify[_currentItem].addLine(0, _currentLine);
1803 }
1804 }
1805}
1806void PrettyPrinter::addItem() {
1807 _items.emplace_back();
1808 _linesToSimplify.emplace_back();
1809 _linesNotToSimplify.emplace_back();
1810 _currentItem++;
1811 _currentLine = -1;
1812}
1813
1814void PrettyPrinter::print(std::ostream& os) const {
1815 std::vector<Line>::const_iterator it;
1816 int nItems = static_cast<int>(_items.size());
1817 for (int item = 0; item < nItems; item++) {
1818 for (it = _items[item].begin(); it != _items[item].end(); it++) {
1819 it->print(os);
1820 }
1821 // os << std::endl;
1822 }
1823}
1824std::string PrettyPrinter::printSpaces(int n) {
1825 std::string result;
1826 for (int i = 0; i < n; i++) {
1827 result += " ";
1828 }
1829 return result;
1830}
1831
1832void PrettyPrinter::printDocument(Document* d, bool alignment, int alignmentCol,
1833 const std::string& before, const std::string& after) {
1834 if (auto* dl = dynamic_cast<DocumentList*>(d)) {
1835 printDocList(dl, alignmentCol, before, after);
1836 } else if (auto* sd = dynamic_cast<StringDocument*>(d)) {
1837 printStringDoc(sd, alignment, alignmentCol, before, after);
1838 } else if (auto* bp = dynamic_cast<BreakPoint*>(d)) {
1839 printString(before, alignment, alignmentCol);
1840 addLine(alignmentCol, _deeplySimp, !bp->getDontSimplify(), d->getLevel());
1841 printString(after, alignment, alignmentCol);
1842 } else {
1843 throw InternalError("PrettyPrinter::print : Wrong type of document");
1844 }
1845}
1846
1847void PrettyPrinter::printStringDoc(StringDocument* d, bool alignment, int alignmentCol,
1848 const std::string& before, const std::string& after) {
1849 std::string s;
1850 if (d != nullptr) {
1851 s = d->getString();
1852 }
1853 s = before + s + after;
1854 printString(s, alignment, alignmentCol);
1855}
1856
1857void PrettyPrinter::printString(const std::string& s, bool alignment, int alignmentCol) {
1858 Line& l = _items[_currentItem][_currentLine];
1859 int size = static_cast<int>(s.size());
1860 if (size <= l.getSpaceLeft(_maxwidth)) {
1861 l.addString(s);
1862 } else {
1863 int col = alignment && _maxwidth - alignmentCol >= size ? alignmentCol : _indentationBase;
1864 addLine(col);
1865 _items[_currentItem][_currentLine].addString(s);
1866 }
1867}
1868
1869void PrettyPrinter::printDocList(DocumentList* d, int alignmentCol, const std::string& super_before,
1870 const std::string& super_after) {
1871 std::vector<Document*> ld = d->getDocs();
1872 std::string beginToken = d->getBeginToken();
1873 std::string separator = d->getSeparator();
1874 std::string endToken = d->getEndToken();
1875 bool _alignment = d->getAlignment();
1876 if (d->getUnbreakable()) {
1877 addLine(alignmentCol);
1878 }
1879 int currentCol = _items[_currentItem][_currentLine].getIndentation() +
1880 _items[_currentItem][_currentLine].getLength();
1881 int newAlignmentCol =
1882 _alignment ? currentCol + static_cast<int>(beginToken.size()) : alignmentCol;
1883 int vectorSize = static_cast<int>(ld.size());
1884 int lastVisibleElementIndex;
1885 for (int i = 0; i < vectorSize; i++) {
1886 if (dynamic_cast<BreakPoint*>(ld[i]) == nullptr) {
1887 lastVisibleElementIndex = i;
1888 }
1889 }
1890 if (vectorSize == 0) {
1891 printStringDoc(nullptr, true, newAlignmentCol, super_before + beginToken,
1892 endToken + super_after);
1893 }
1894 for (int i = 0; i < vectorSize; i++) {
1895 Document* subdoc = ld[i];
1896 bool bp = false;
1897 if (dynamic_cast<BreakPoint*>(subdoc) != nullptr) {
1898 if (!_alignment) {
1899 newAlignmentCol += _indentationBase;
1900 }
1901 bp = true;
1902 }
1903 std::string af;
1904 std::string be;
1905 if (i != vectorSize - 1) {
1906 if (bp || lastVisibleElementIndex <= i) {
1907 af = "";
1908 } else {
1909 af = separator;
1910 }
1911 } else {
1912 af = endToken + super_after;
1913 }
1914 if (i == 0) {
1915 be = super_before + beginToken;
1916 } else {
1917 be = "";
1918 }
1919 printDocument(subdoc, _alignment, newAlignmentCol, be, af);
1920 }
1921 if (d->getUnbreakable()) {
1922 simplify(_currentItem, _currentLine, nullptr);
1923 }
1924}
1925void PrettyPrinter::simplifyItem(int item) {
1926 _linesToSimplify[item].remove(_linesNotToSimplify[item]);
1927 std::vector<int>* vec = (_linesToSimplify[item].getLinesToSimplify());
1928 while (!vec->empty()) {
1929 if (!simplify(item, (*vec)[0], vec)) {
1930 break;
1931 }
1932 }
1933 delete vec;
1934}
1935
1936bool PrettyPrinter::simplify(int item, int line, std::vector<int>* vec) {
1937 if (line == 0) {
1938 _linesToSimplify[item].remove(vec, line, false);
1939 return false;
1940 }
1941 if (_items[item][line].getLength() > _items[item][line - 1].getSpaceLeft(_maxwidth)) {
1942 _linesToSimplify[item].remove(vec, line, false);
1943 return false;
1944 }
1945 _linesToSimplify[item].remove(vec, line, true);
1946 _items[item][line - 1].concatenateLines(_items[item][line]);
1947 _items[item].erase(_items[item].begin() + line);
1948
1949 _linesToSimplify[item].decrementLine(vec, line);
1950 _currentLine--;
1951
1952 return true;
1953}
1954
1955Printer::Printer(std::ostream& os, int width, bool flatZinc, EnvI* env)
1956 : _env(env), _ism(nullptr), _printer(nullptr), _os(os), _width(width), _flatZinc(flatZinc) {}
1957void Printer::init() {
1958 if (_ism == nullptr) {
1959 _ism = new ItemDocumentMapper();
1960 _printer = new PrettyPrinter(_width, 4, true, true);
1961 }
1962}
1963Printer::~Printer() {
1964 delete _printer;
1965 delete _ism;
1966}
1967
1968void Printer::p(Document* d) {
1969 _printer->print(d);
1970 _printer->print(_os);
1971 delete _printer;
1972 _printer = new PrettyPrinter(_width, 4, true, true);
1973}
1974void Printer::p(const Item* i) {
1975 Document* d;
1976 switch (i->iid()) {
1977 case Item::II_INC:
1978 d = ItemDocumentMapper::mapIncludeI(*i->cast<IncludeI>());
1979 break;
1980 case Item::II_VD:
1981 d = ItemDocumentMapper::mapVarDeclI(*i->cast<VarDeclI>());
1982 break;
1983 case Item::II_ASN:
1984 d = ItemDocumentMapper::mapAssignI(*i->cast<AssignI>());
1985 break;
1986 case Item::II_CON:
1987 d = ItemDocumentMapper::mapConstraintI(*i->cast<ConstraintI>());
1988 break;
1989 case Item::II_SOL:
1990 d = ItemDocumentMapper::mapSolveI(*i->cast<SolveI>());
1991 break;
1992 case Item::II_OUT:
1993 d = ItemDocumentMapper::mapOutputI(*i->cast<OutputI>());
1994 break;
1995 case Item::II_FUN:
1996 d = ItemDocumentMapper::mapFunctionI(*i->cast<FunctionI>());
1997 break;
1998 }
1999 p(d);
2000 delete d;
2001}
2002
2003void Printer::print(const Expression* e) {
2004 if (_width == 0) {
2005 PlainPrinter p(_os, _flatZinc, _env);
2006 p.p(e);
2007 } else {
2008 init();
2009 Document* d = expression_to_document(e);
2010 p(d);
2011 delete d;
2012 }
2013}
2014void Printer::print(const Item* i) {
2015 if (_width == 0) {
2016 PlainPrinter p(_os, _flatZinc, _env);
2017 p.p(i);
2018 } else {
2019 init();
2020 p(i);
2021 }
2022}
2023void Printer::print(const Model* m) {
2024 if (_width == 0) {
2025 PlainPrinter p(_os, _flatZinc, _env);
2026 for (auto* i : *m) {
2027 p.p(i);
2028 }
2029 } else {
2030 init();
2031 for (auto* i : *m) {
2032 p(i);
2033 }
2034 }
2035}
2036
2037} // namespace MiniZinc
2038
2039void debugprint(MiniZinc::Expression* e) { std::cerr << *e << "\n"; }
2040void debugprint(MiniZinc::Item* i) { std::cerr << *i; }
2041void debugprint(MiniZinc::Model* m) {
2042 MiniZinc::Printer p(std::cerr, 0);
2043 p.print(m);
2044}
2045void debugprint(const MiniZinc::Location& loc) { std::cerr << loc << std::endl; }