dekker.one
The models, scripts, and results of the benchmarks performed for a Half Reification Journal paper
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 \"" << Printer::escapeStringLit(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 const OutputI& oi = *i->cast<OutputI>();
693 _os << "output ";
694 for (ExpressionSetIter i = oi.ann().begin(); i != oi.ann().end(); ++i) {
695 Call* c = (*i)->dynamicCast<Call>();
696 if (c != nullptr && c->id() == "mzn_output_section") {
697 _os << ":: ";
698 p(c->arg(0));
699 _os << " ";
700 }
701 }
702 p(oi.e());
703 } break;
704 case Item::II_FUN: {
705 const FunctionI& fi = *i->cast<FunctionI>();
706 if (fi.ti()->type().isAnn() && fi.e() == nullptr) {
707 _os << "annotation ";
708 } else if (fi.ti()->type() == Type::parbool()) {
709 _os << "test ";
710 } else if (fi.ti()->type() == Type::varbool()) {
711 _os << "predicate ";
712 } else {
713 _os << "function ";
714 p(fi.ti());
715 _os << " : ";
716 }
717 _os << fi.id();
718 if (fi.paramCount() > 0) {
719 _os << "(";
720 for (unsigned int j = 0; j < fi.paramCount(); j++) {
721 p(fi.param(j));
722 if (j < fi.paramCount() - 1) {
723 _os << ",";
724 }
725 }
726 _os << ")";
727 }
728 if (fi.capturedAnnotationsVar() != nullptr) {
729 _os << " ann : ";
730 p(fi.capturedAnnotationsVar()->id());
731 _os << " ";
732 }
733 p(fi.ann());
734 if (fi.e() != nullptr) {
735 _os << " = ";
736 p(fi.e());
737 }
738 } break;
739 }
740 _os << ";" << std::endl;
741 }
742};
743
744template <class T>
745class ExpressionMapper {
746protected:
747 T& _t;
748
749public:
750 ExpressionMapper(T& t) : _t(t) {}
751 typename T::ret map(const Expression* e) {
752 switch (e->eid()) {
753 case Expression::E_INTLIT:
754 return _t.mapIntLit(*e->cast<IntLit>());
755 case Expression::E_FLOATLIT:
756 return _t.mapFloatLit(*e->cast<FloatLit>());
757 case Expression::E_SETLIT:
758 return _t.mapSetLit(*e->cast<SetLit>());
759 case Expression::E_BOOLLIT:
760 return _t.mapBoolLit(*e->cast<BoolLit>());
761 case Expression::E_STRINGLIT:
762 return _t.mapStringLit(*e->cast<StringLit>());
763 case Expression::E_ID:
764 return _t.mapId(*e->cast<Id>());
765 case Expression::E_ANON:
766 return _t.mapAnonVar(*e->cast<AnonVar>());
767 case Expression::E_ARRAYLIT:
768 return _t.mapArrayLit(*e->cast<ArrayLit>());
769 case Expression::E_ARRAYACCESS:
770 return _t.mapArrayAccess(*e->cast<ArrayAccess>());
771 case Expression::E_COMP:
772 return _t.mapComprehension(*e->cast<Comprehension>());
773 case Expression::E_ITE:
774 return _t.mapITE(*e->cast<ITE>());
775 case Expression::E_BINOP:
776 return _t.mapBinOp(*e->cast<BinOp>());
777 case Expression::E_UNOP:
778 return _t.mapUnOp(*e->cast<UnOp>());
779 case Expression::E_CALL:
780 return _t.mapCall(*e->cast<Call>());
781 case Expression::E_VARDECL:
782 return _t.mapVarDecl(*e->cast<VarDecl>());
783 case Expression::E_LET:
784 return _t.mapLet(*e->cast<Let>());
785 case Expression::E_TI:
786 return _t.mapTypeInst(*e->cast<TypeInst>());
787 case Expression::E_TIID:
788 return _t.mapTIId(*e->cast<TIId>());
789 default:
790 assert(false);
791 return typename T::ret();
792 break;
793 }
794 }
795};
796
797class Document {
798private:
799 int _level;
800
801public:
802 Document() : _level(0) {}
803 virtual ~Document() {}
804 int getLevel() const { return _level; }
805 // Make this object a child of "d".
806 virtual void setParent(Document* d) { _level = d->_level + 1; }
807};
808
809class BreakPoint : public Document {
810private:
811 bool _dontSimplify;
812
813public:
814 BreakPoint() { _dontSimplify = false; }
815 BreakPoint(bool ds) { _dontSimplify = ds; }
816 ~BreakPoint() override {}
817 void setDontSimplify(bool b) { _dontSimplify = b; }
818 bool getDontSimplify() const { return _dontSimplify; }
819};
820
821class StringDocument : public Document {
822private:
823 std::string _stringDocument;
824
825public:
826 StringDocument() {}
827 ~StringDocument() override {}
828
829 StringDocument(std::string s) : _stringDocument(std::move(s)) {}
830
831 std::string getString() { return _stringDocument; }
832 void setString(std::string s) { _stringDocument = std::move(s); }
833};
834
835class DocumentList : public Document {
836private:
837 std::vector<Document*> _docs;
838 std::string _beginToken;
839 std::string _separator;
840 std::string _endToken;
841 bool _unbreakable;
842 bool _alignment;
843
844public:
845 ~DocumentList() override {
846 std::vector<Document*>::iterator it;
847 for (it = _docs.begin(); it != _docs.end(); it++) {
848 delete *it;
849 }
850 }
851 DocumentList(std::string beginToken = "", std::string separator = "", std::string endToken = "",
852 bool alignment = true);
853
854 void addDocumentToList(Document* d) {
855 _docs.push_back(d);
856 d->setParent(this);
857 }
858
859 void setParent(Document* d) override {
860 Document::setParent(d);
861 std::vector<Document*>::iterator it;
862 for (it = _docs.begin(); it != _docs.end(); it++) {
863 (*it)->setParent(this);
864 }
865 }
866
867 void addStringToList(std::string s) { addDocumentToList(new StringDocument(std::move(s))); }
868
869 void addBreakPoint(bool b = false) { addDocumentToList(new BreakPoint(b)); }
870
871 std::vector<Document*> getDocs() { return _docs; }
872
873 void setList(std::vector<Document*> ld) { _docs = std::move(ld); }
874
875 std::string getBeginToken() { return _beginToken; }
876
877 std::string getEndToken() { return _endToken; }
878
879 std::string getSeparator() { return _separator; }
880
881 bool getUnbreakable() const { return _unbreakable; }
882
883 void setUnbreakable(bool b) { _unbreakable = b; }
884
885 bool getAlignment() const { return _alignment; }
886};
887
888DocumentList::DocumentList(std::string beginToken, std::string separator, std::string endToken,
889 bool alignment) {
890 _beginToken = std::move(beginToken);
891 _separator = std::move(separator);
892 _endToken = std::move(endToken);
893 _alignment = alignment;
894 _unbreakable = false;
895}
896
897class Line {
898private:
899 int _indentation;
900 int _lineLength;
901 std::vector<std::string> _text;
902
903public:
904 Line() : _indentation(0), _lineLength(0), _text(0) {}
905 Line(const Line&) = default;
906 Line(const int indent) : _indentation(indent), _lineLength(0), _text(0) {}
907 Line& operator=(const Line&) = default;
908 bool operator==(const Line& l) { return &l == this; }
909
910 void setIndentation(int i) { _indentation = i; }
911
912 int getLength() const { return _lineLength; }
913 int getIndentation() const { return _indentation; }
914 int getSpaceLeft(int maxwidth) const;
915 void addString(const std::string& s);
916 void concatenateLines(Line& l);
917
918 void print(std::ostream& os) const {
919 for (int i = 0; i < getIndentation(); i++) {
920 os << " ";
921 }
922 std::vector<std::string>::const_iterator it;
923 for (it = _text.begin(); it != _text.end(); it++) {
924 os << (*it);
925 }
926 os << "\n";
927 }
928};
929
930int Line::getSpaceLeft(int maxwidth) const { return maxwidth - _lineLength - _indentation; }
931void Line::addString(const std::string& s) {
932 _lineLength += static_cast<int>(s.size());
933 _text.push_back(s);
934}
935void Line::concatenateLines(Line& l) {
936 _text.insert(_text.end(), l._text.begin(), l._text.end());
937 _lineLength += l._lineLength;
938}
939
940class LinesToSimplify {
941private:
942 std::map<int, std::vector<int> > _lines;
943
944 // (i,j) in parent <=> j can only be simplified if i is simplified
945 std::vector<std::pair<int, int> > _parent;
946 /*
947 * if i can't simplify, remove j and his parents
948 */
949 // mostRecentlyAdded[level] = line of the most recently added
950 std::map<int, int> _mostRecentlyAdded;
951
952public:
953 std::vector<int>* getLinesForPriority(int p) {
954 std::map<int, std::vector<int> >::iterator it;
955 for (it = _lines.begin(); it != _lines.end(); it++) {
956 if (it->first == p) {
957 return &(it->second);
958 }
959 }
960 return nullptr;
961 }
962 void addLine(int p, int l, int par = -1) {
963 if (par == -1) {
964 for (int i = p - 1; i >= 0; i--) {
965 auto it = _mostRecentlyAdded.find(i);
966 if (it != _mostRecentlyAdded.end()) {
967 par = it->second;
968 break;
969 }
970 }
971 }
972 if (par != -1) {
973 _parent.emplace_back(l, par);
974 }
975 _mostRecentlyAdded.insert(std::pair<int, int>(p, l));
976 std::map<int, std::vector<int> >::iterator it;
977 for (it = _lines.begin(); it != _lines.end(); it++) {
978 if (it->first == p) {
979 it->second.push_back(l);
980 return;
981 }
982 }
983 std::vector<int> v;
984 v.push_back(l);
985 _lines.insert(std::pair<int, std::vector<int> >(p, v));
986 }
987 void decrementLine(std::vector<int>* vec, int l) {
988 std::vector<int>::iterator vit;
989 if (vec != nullptr) {
990 for (vit = vec->begin(); vit != vec->end(); vit++) {
991 if (*vit >= l) {
992 *vit = *vit - 1;
993 }
994 }
995 }
996 // Now the map
997 std::map<int, std::vector<int> >::iterator it;
998 for (it = _lines.begin(); it != _lines.end(); it++) {
999 for (vit = it->second.begin(); vit != it->second.end(); vit++) {
1000 if (*vit >= l) {
1001 *vit = *vit - 1;
1002 }
1003 }
1004 }
1005 // And the parent table
1006 std::vector<std::pair<int, int> >::iterator vpit;
1007 for (vpit = _parent.begin(); vpit != _parent.end(); vpit++) {
1008 if (vpit->first >= l) {
1009 vpit->first--;
1010 }
1011 if (vpit->second >= l) {
1012 vpit->second--;
1013 }
1014 }
1015 }
1016 void remove(LinesToSimplify& lts) {
1017 std::map<int, std::vector<int> >::iterator it;
1018 for (it = lts._lines.begin(); it != lts._lines.end(); it++) {
1019 std::vector<int>::iterator vit;
1020 for (vit = it->second.begin(); vit != it->second.end(); vit++) {
1021 remove(nullptr, *vit, false);
1022 }
1023 }
1024 }
1025 void remove(std::vector<int>* v, int i, bool success = true) {
1026 if (v != nullptr) {
1027 v->erase(std::remove(v->begin(), v->end(), i), v->end());
1028 }
1029 for (auto& line : _lines) {
1030 std::vector<int>& l = line.second;
1031 l.erase(std::remove(l.begin(), l.end(), i), l.end());
1032 }
1033 // Call on its parent
1034 if (!success) {
1035 std::vector<std::pair<int, int> >::iterator vpit;
1036 for (vpit = _parent.begin(); vpit != _parent.end(); vpit++) {
1037 if (vpit->first == i && vpit->second != i && vpit->second != -1) {
1038 remove(v, vpit->second, false);
1039 }
1040 }
1041 }
1042 }
1043 std::vector<int>* getLinesToSimplify() {
1044 auto* vec = new std::vector<int>();
1045 std::map<int, std::vector<int> >::iterator it;
1046 for (it = _lines.begin(); it != _lines.end(); it++) {
1047 std::vector<int>& svec = it->second;
1048 vec->insert(vec->begin(), svec.begin(), svec.end());
1049 }
1050 return vec;
1051 }
1052};
1053
1054Document* expression_to_document(const Expression* e);
1055Document* annotation_to_document(const Annotation& ann);
1056Document* tiexpression_to_document(const Type& type, const Expression* e) {
1057 auto* dl = new DocumentList("", "", "", false);
1058 switch (type.ti()) {
1059 case Type::TI_PAR:
1060 break;
1061 case Type::TI_VAR:
1062 dl->addStringToList("var ");
1063 break;
1064 }
1065 if (type.ot() == Type::OT_OPTIONAL) {
1066 dl->addStringToList("opt ");
1067 }
1068 if (type.st() == Type::ST_SET) {
1069 dl->addStringToList("set of ");
1070 }
1071 if (e == nullptr) {
1072 switch (type.bt()) {
1073 case Type::BT_INT:
1074 dl->addStringToList("int");
1075 break;
1076 case Type::BT_BOOL:
1077 dl->addStringToList("bool");
1078 break;
1079 case Type::BT_FLOAT:
1080 dl->addStringToList("float");
1081 break;
1082 case Type::BT_STRING:
1083 dl->addStringToList("string");
1084 break;
1085 case Type::BT_ANN:
1086 dl->addStringToList("ann");
1087 break;
1088 case Type::BT_BOT:
1089 dl->addStringToList("bot");
1090 break;
1091 case Type::BT_TOP:
1092 dl->addStringToList("top");
1093 break;
1094 case Type::BT_UNKNOWN:
1095 dl->addStringToList("???");
1096 break;
1097 }
1098 } else {
1099 dl->addDocumentToList(expression_to_document(e));
1100 }
1101 return dl;
1102}
1103
1104class ExpressionDocumentMapper {
1105public:
1106 typedef Document* ret;
1107 static ret mapIntLit(const IntLit& il) {
1108 std::ostringstream oss;
1109 oss << il.v();
1110 return new StringDocument(oss.str());
1111 }
1112 static ret mapFloatLit(const FloatLit& fl) {
1113 std::ostringstream oss;
1114 pp_floatval(oss, fl.v());
1115 return new StringDocument(oss.str());
1116 }
1117 static ret mapSetLit(const SetLit& sl) {
1118 DocumentList* dl;
1119 if (sl.isv() != nullptr) {
1120 if (sl.type().bt() == Type::BT_BOOL) {
1121 if (sl.isv()->size() == 0) {
1122 dl = new DocumentList("true..false", "", "");
1123 } else {
1124 if (sl.isv()->min() == 0) {
1125 if (sl.isv()->max() == 0) {
1126 dl = new DocumentList("{false}", "", "");
1127 } else {
1128 dl = new DocumentList("{false,true}", "", "");
1129 }
1130 } else {
1131 dl = new DocumentList("{true}", "", "");
1132 }
1133 }
1134 } else {
1135 if (sl.isv()->size() == 0) {
1136 dl = new DocumentList("1..0", "", "");
1137 } else if (sl.isv()->size() == 1) {
1138 dl = new DocumentList("", "..", "");
1139 {
1140 std::ostringstream oss;
1141 oss << sl.isv()->min(0);
1142 dl->addDocumentToList(new StringDocument(oss.str()));
1143 }
1144 {
1145 std::ostringstream oss;
1146 oss << sl.isv()->max(0);
1147 dl->addDocumentToList(new StringDocument(oss.str()));
1148 }
1149 } else {
1150 dl = new DocumentList("{", ", ", "}", true);
1151 IntSetRanges isr(sl.isv());
1152 for (Ranges::ToValues<IntSetRanges> isv(isr); isv(); ++isv) {
1153 std::ostringstream oss;
1154 oss << isv.val();
1155 dl->addDocumentToList(new StringDocument(oss.str()));
1156 }
1157 }
1158 }
1159 } else if (sl.fsv() != nullptr) {
1160 if (sl.fsv()->size() == 0) {
1161 dl = new DocumentList("1.0..0.0", "", "");
1162 } else if (sl.fsv()->size() == 1) {
1163 dl = new DocumentList("", "..", "");
1164 {
1165 std::ostringstream oss;
1166 pp_floatval(oss, sl.fsv()->min(0));
1167 dl->addDocumentToList(new StringDocument(oss.str()));
1168 }
1169 {
1170 std::ostringstream oss;
1171 pp_floatval(oss, sl.fsv()->max(0));
1172 dl->addDocumentToList(new StringDocument(oss.str()));
1173 }
1174 } else {
1175 dl = new DocumentList("", " union ", "", true);
1176 FloatSetRanges fsr(sl.fsv());
1177 for (; fsr(); ++fsr) {
1178 std::ostringstream oss;
1179 pp_floatval(oss, fsr.min());
1180 oss << "..";
1181 pp_floatval(oss, fsr.max());
1182 dl->addDocumentToList(new StringDocument(oss.str()));
1183 }
1184 }
1185
1186 } else {
1187 dl = new DocumentList("{", ", ", "}", true);
1188 for (unsigned int i = 0; i < sl.v().size(); i++) {
1189 dl->addDocumentToList(expression_to_document((sl.v()[i])));
1190 }
1191 }
1192 return dl;
1193 }
1194 static ret mapBoolLit(const BoolLit& bl) {
1195 return new StringDocument(std::string(bl.v() ? "true" : "false"));
1196 }
1197 static ret mapStringLit(const StringLit& sl) {
1198 std::ostringstream oss;
1199 oss << "\"" << Printer::escapeStringLit(sl.v()) << "\"";
1200 return new StringDocument(oss.str());
1201 }
1202 static ret mapId(const Id& id) {
1203 if (&id == constants().absent) {
1204 return new StringDocument("<>");
1205 }
1206 if (id.idn() == -1) {
1207 return new StringDocument(std::string(id.v().c_str(), id.v().size()));
1208 }
1209 std::ostringstream oss;
1210 oss << "X_INTRODUCED_" << id.idn() << "_";
1211 return new StringDocument(oss.str());
1212 }
1213 static ret mapTIId(const TIId& id) {
1214 std::ostringstream ss;
1215 ss << "$" << id.v();
1216 return new StringDocument(ss.str());
1217 }
1218 static ret mapAnonVar(const AnonVar& /*v*/) { return new StringDocument("_"); }
1219 static ret mapArrayLit(const ArrayLit& al) {
1220 /// TODO: test multi-dimensional arrays handling
1221 DocumentList* dl;
1222 unsigned int n = al.dims();
1223 if (n == 1 && al.min(0) == 1) {
1224 dl = new DocumentList("[", ", ", "]");
1225 for (unsigned int i = 0; i < al.size(); i++) {
1226 dl->addDocumentToList(expression_to_document(al[i]));
1227 }
1228 } else if (n == 2 && al.min(0) == 1 && al.min(1) == 1) {
1229 dl = new DocumentList("[| ", " | ", " |]");
1230 for (int i = 0; i < al.max(0); i++) {
1231 auto* row = new DocumentList("", ", ", "");
1232 for (int j = 0; j < al.max(1); j++) {
1233 row->addDocumentToList(expression_to_document(al[i * al.max(1) + j]));
1234 }
1235 dl->addDocumentToList(row);
1236 if (i != al.max(0) - 1) {
1237 dl->addBreakPoint(true); // dont simplify
1238 }
1239 }
1240 } else {
1241 dl = new DocumentList("", "", "");
1242 std::stringstream oss;
1243 oss << "array" << n << "d";
1244 dl->addStringToList(oss.str());
1245 auto* args = new DocumentList("(", ", ", ")");
1246
1247 for (int i = 0; i < al.dims(); i++) {
1248 oss.str("");
1249 oss << al.min(i) << ".." << al.max(i);
1250 args->addStringToList(oss.str());
1251 }
1252 auto* array = new DocumentList("[", ", ", "]");
1253 for (unsigned int i = 0; i < al.size(); i++) {
1254 array->addDocumentToList(expression_to_document(al[i]));
1255 }
1256 args->addDocumentToList(array);
1257 dl->addDocumentToList(args);
1258 }
1259 return dl;
1260 }
1261 static ret mapArrayAccess(const ArrayAccess& aa) {
1262 auto* dl = new DocumentList("", "", "");
1263
1264 dl->addDocumentToList(expression_to_document(aa.v()));
1265 auto* args = new DocumentList("[", ", ", "]");
1266 for (unsigned int i = 0; i < aa.idx().size(); i++) {
1267 args->addDocumentToList(expression_to_document(aa.idx()[i]));
1268 }
1269 dl->addDocumentToList(args);
1270 return dl;
1271 }
1272 static ret mapComprehension(const Comprehension& c) {
1273 std::ostringstream oss;
1274 DocumentList* dl;
1275 if (c.set()) {
1276 dl = new DocumentList("{ ", " | ", " }");
1277 } else {
1278 dl = new DocumentList("[ ", " | ", " ]");
1279 }
1280 dl->addDocumentToList(expression_to_document(c.e()));
1281 auto* head = new DocumentList("", " ", "");
1282 auto* generators = new DocumentList("", ", ", "");
1283 for (int i = 0; i < c.numberOfGenerators(); i++) {
1284 auto* gen = new DocumentList("", "", "");
1285 auto* idents = new DocumentList("", ", ", "");
1286 for (int j = 0; j < c.numberOfDecls(i); j++) {
1287 std::ostringstream ss;
1288 Id* ident = c.decl(i, j)->id();
1289 if (ident->idn() == -1) {
1290 ss << ident->v();
1291 } else {
1292 ss << "X_INTRODUCED_" << ident->idn() << "_";
1293 }
1294 idents->addStringToList(ss.str());
1295 }
1296 gen->addDocumentToList(idents);
1297 if (c.in(i) == nullptr) {
1298 gen->addStringToList(" = ");
1299 gen->addDocumentToList(expression_to_document(c.where(i)));
1300 } else {
1301 gen->addStringToList(" in ");
1302 gen->addDocumentToList(expression_to_document(c.in(i)));
1303 if (c.where(i) != nullptr) {
1304 gen->addStringToList(" where ");
1305 gen->addDocumentToList(expression_to_document(c.where(i)));
1306 }
1307 }
1308 generators->addDocumentToList(gen);
1309 }
1310 head->addDocumentToList(generators);
1311 dl->addDocumentToList(head);
1312
1313 return dl;
1314 }
1315 static ret mapITE(const ITE& ite) {
1316 auto* dl = new DocumentList("", "", "");
1317 for (int i = 0; i < ite.size(); i++) {
1318 std::string beg = (i == 0 ? "if " : " elseif ");
1319 dl->addStringToList(beg);
1320 dl->addDocumentToList(expression_to_document(ite.ifExpr(i)));
1321 dl->addStringToList(" then ");
1322
1323 auto* ifdoc = new DocumentList("", "", "", false);
1324 ifdoc->addBreakPoint();
1325 ifdoc->addDocumentToList(expression_to_document(ite.thenExpr(i)));
1326 dl->addDocumentToList(ifdoc);
1327 dl->addStringToList(" ");
1328 }
1329 dl->addBreakPoint();
1330 dl->addStringToList("else ");
1331
1332 auto* elsedoc = new DocumentList("", "", "", false);
1333 elsedoc->addBreakPoint();
1334 elsedoc->addDocumentToList(expression_to_document(ite.elseExpr()));
1335 dl->addDocumentToList(elsedoc);
1336 dl->addStringToList(" ");
1337 dl->addBreakPoint();
1338 dl->addStringToList("endif");
1339
1340 return dl;
1341 }
1342 static ret mapBinOp(const BinOp& bo) {
1343 Parentheses ps = need_parentheses(&bo, bo.lhs(), bo.rhs());
1344 DocumentList* opLeft;
1345 DocumentList* dl;
1346 DocumentList* opRight;
1347 bool linebreak = false;
1348 if ((ps & PN_LEFT) != 0) {
1349 opLeft = new DocumentList("(", " ", ")");
1350 } else {
1351 opLeft = new DocumentList("", " ", "");
1352 }
1353 opLeft->addDocumentToList(expression_to_document(bo.lhs()));
1354 std::string op;
1355 switch (bo.op()) {
1356 case BOT_PLUS:
1357 op = "+";
1358 break;
1359 case BOT_MINUS:
1360 op = "-";
1361 break;
1362 case BOT_MULT:
1363 op = "*";
1364 break;
1365 case BOT_POW:
1366 op = "^";
1367 break;
1368 case BOT_DIV:
1369 op = "/";
1370 break;
1371 case BOT_IDIV:
1372 op = " div ";
1373 break;
1374 case BOT_MOD:
1375 op = " mod ";
1376 break;
1377 case BOT_LE:
1378 op = " < ";
1379 break;
1380 case BOT_LQ:
1381 op = "<=";
1382 break;
1383 case BOT_GR:
1384 op = " > ";
1385 break;
1386 case BOT_GQ:
1387 op = ">=";
1388 break;
1389 case BOT_EQ:
1390 op = "==";
1391 break;
1392 case BOT_NQ:
1393 op = "!=";
1394 break;
1395 case BOT_IN:
1396 op = " in ";
1397 break;
1398 case BOT_SUBSET:
1399 op = " subset ";
1400 break;
1401 case BOT_SUPERSET:
1402 op = " superset ";
1403 break;
1404 case BOT_UNION:
1405 op = " union ";
1406 break;
1407 case BOT_DIFF:
1408 op = " diff ";
1409 break;
1410 case BOT_SYMDIFF:
1411 op = " symdiff ";
1412 break;
1413 case BOT_INTERSECT:
1414 op = " intersect ";
1415 break;
1416 case BOT_PLUSPLUS:
1417 op = "++";
1418 linebreak = true;
1419 break;
1420 case BOT_EQUIV:
1421 op = " <-> ";
1422 break;
1423 case BOT_IMPL:
1424 op = " -> ";
1425 break;
1426 case BOT_RIMPL:
1427 op = " <- ";
1428 break;
1429 case BOT_OR:
1430 op = " \\/ ";
1431 linebreak = true;
1432 break;
1433 case BOT_AND:
1434 op = " /\\ ";
1435 linebreak = true;
1436 break;
1437 case BOT_XOR:
1438 op = " xor ";
1439 break;
1440 case BOT_DOTDOT:
1441 op = "..";
1442 break;
1443 default:
1444 assert(false);
1445 break;
1446 }
1447 dl = new DocumentList("", op, "");
1448
1449 if ((ps & PN_RIGHT) != 0) {
1450 opRight = new DocumentList("(", " ", ")");
1451 } else {
1452 opRight = new DocumentList("", "", "");
1453 }
1454 opRight->addDocumentToList(expression_to_document(bo.rhs()));
1455 dl->addDocumentToList(opLeft);
1456 if (linebreak) {
1457 dl->addBreakPoint();
1458 }
1459 dl->addDocumentToList(opRight);
1460
1461 return dl;
1462 }
1463 static ret mapUnOp(const UnOp& uo) {
1464 auto* dl = new DocumentList("", "", "");
1465 std::string op;
1466 switch (uo.op()) {
1467 case UOT_NOT:
1468 op = "not ";
1469 break;
1470 case UOT_PLUS:
1471 op = "+";
1472 break;
1473 case UOT_MINUS:
1474 op = "-";
1475 break;
1476 default:
1477 assert(false);
1478 break;
1479 }
1480 dl->addStringToList(op);
1481 DocumentList* unop;
1482 bool needParen = (uo.e()->isa<BinOp>() || uo.e()->isa<UnOp>());
1483 if (needParen) {
1484 unop = new DocumentList("(", " ", ")");
1485 } else {
1486 unop = new DocumentList("", " ", "");
1487 }
1488
1489 unop->addDocumentToList(expression_to_document(uo.e()));
1490 dl->addDocumentToList(unop);
1491 return dl;
1492 }
1493 static ret mapCall(const Call& c) {
1494 if (c.argCount() == 1) {
1495 /*
1496 * if we have only one argument, and this is an array comprehension,
1497 * we convert it into the following syntax
1498 * forall (f(i,j) | i in 1..10)
1499 * -->
1500 * forall (i in 1..10) (f(i,j))
1501 */
1502
1503 const Expression* e = c.arg(0);
1504 if (e->isa<Comprehension>()) {
1505 const auto* com = e->cast<Comprehension>();
1506 if (!com->set()) {
1507 auto* dl = new DocumentList("", " ", "");
1508 dl->addStringToList(std::string(c.id().c_str(), c.id().size()));
1509 auto* args = new DocumentList("", " ", "", false);
1510 auto* generators = new DocumentList("", ", ", "");
1511
1512 for (int i = 0; i < com->numberOfGenerators(); i++) {
1513 auto* gen = new DocumentList("", "", "");
1514 auto* idents = new DocumentList("", ", ", "");
1515 for (int j = 0; j < com->numberOfDecls(i); j++) {
1516 idents->addStringToList(std::string(com->decl(i, j)->id()->v().c_str(),
1517 com->decl(i, j)->id()->v().size()));
1518 }
1519 gen->addDocumentToList(idents);
1520 if (com->in(i) == nullptr) {
1521 gen->addStringToList(" = ");
1522 gen->addDocumentToList(expression_to_document(com->where(i)));
1523 } else {
1524 gen->addStringToList(" in ");
1525 gen->addDocumentToList(expression_to_document(com->in(i)));
1526 if (com->where(i) != nullptr) {
1527 gen->addStringToList(" where ");
1528 gen->addDocumentToList(expression_to_document(com->where(i)));
1529 }
1530 }
1531 generators->addDocumentToList(gen);
1532 }
1533
1534 args->addStringToList("(");
1535 args->addDocumentToList(generators);
1536 args->addStringToList(")");
1537
1538 args->addStringToList("(");
1539 args->addBreakPoint();
1540 args->addDocumentToList(expression_to_document(com->e()));
1541
1542 dl->addDocumentToList(args);
1543 dl->addBreakPoint();
1544 dl->addStringToList(")");
1545
1546 return dl;
1547 }
1548 }
1549 }
1550 std::ostringstream beg;
1551 beg << c.id() << "(";
1552 auto* dl = new DocumentList(beg.str(), ", ", ")");
1553 for (unsigned int i = 0; i < c.argCount(); i++) {
1554 dl->addDocumentToList(expression_to_document(c.arg(i)));
1555 }
1556 return dl;
1557 }
1558 static ret mapVarDecl(const VarDecl& vd) {
1559 std::ostringstream oss;
1560 auto* dl = new DocumentList("", "", "");
1561 dl->addDocumentToList(expression_to_document(vd.ti()));
1562 if (vd.id()->idn() == -1) {
1563 if (vd.id()->v().size() != 0) {
1564 oss << ": " << vd.id()->v().c_str();
1565 }
1566 } else {
1567 oss << ": X_INTRODUCED_" << vd.id()->idn() << "_";
1568 }
1569 dl->addStringToList(oss.str());
1570
1571 if (vd.introduced()) {
1572 dl->addStringToList(" ::var_is_introduced ");
1573 }
1574 if (!vd.ann().isEmpty()) {
1575 dl->addDocumentToList(annotation_to_document(vd.ann()));
1576 }
1577 if (vd.e() != nullptr) {
1578 dl->addStringToList(" = ");
1579 dl->addDocumentToList(expression_to_document(vd.e()));
1580 }
1581 return dl;
1582 }
1583 static ret mapLet(const Let& l) {
1584 auto* letin = new DocumentList("", "", "", false);
1585 auto* lets = new DocumentList("", " ", "", true);
1586 auto* inexpr = new DocumentList("", "", "");
1587 bool ds = l.let().size() > 1;
1588
1589 for (unsigned int i = 0; i < l.let().size(); i++) {
1590 if (i != 0) {
1591 lets->addBreakPoint(ds);
1592 }
1593 auto* exp = new DocumentList("", " ", ",");
1594 const Expression* li = l.let()[i];
1595 if (!li->isa<VarDecl>()) {
1596 exp->addStringToList("constraint");
1597 }
1598 exp->addDocumentToList(expression_to_document(li));
1599 lets->addDocumentToList(exp);
1600 }
1601
1602 inexpr->addDocumentToList(expression_to_document(l.in()));
1603 letin->addBreakPoint(ds);
1604 letin->addDocumentToList(lets);
1605
1606 auto* letin2 = new DocumentList("", "", "", false);
1607
1608 letin2->addBreakPoint();
1609 letin2->addDocumentToList(inexpr);
1610
1611 auto* dl = new DocumentList("", "", "");
1612 dl->addStringToList("let {");
1613 dl->addDocumentToList(letin);
1614 dl->addBreakPoint(ds);
1615 dl->addStringToList("} in (");
1616 dl->addDocumentToList(letin2);
1617 // dl->addBreakPoint();
1618 dl->addStringToList(")");
1619 return dl;
1620 }
1621 static ret mapTypeInst(const TypeInst& ti) {
1622 auto* dl = new DocumentList("", "", "");
1623 if (ti.isarray()) {
1624 dl->addStringToList("array [");
1625 auto* ran = new DocumentList("", ", ", "");
1626 for (unsigned int i = 0; i < ti.ranges().size(); i++) {
1627 ran->addDocumentToList(tiexpression_to_document(Type::parint(), ti.ranges()[i]));
1628 }
1629 dl->addDocumentToList(ran);
1630 dl->addStringToList("] of ");
1631 }
1632 dl->addDocumentToList(tiexpression_to_document(ti.type(), ti.domain()));
1633 return dl;
1634 }
1635};
1636
1637Document* annotation_to_document(const Annotation& ann) {
1638 auto* dl = new DocumentList(" :: ", " :: ", "");
1639 for (ExpressionSetIter it = ann.begin(); it != ann.end(); ++it) {
1640 dl->addDocumentToList(expression_to_document(*it));
1641 }
1642 return dl;
1643}
1644
1645Document* expression_to_document(const Expression* e) {
1646 if (e == nullptr) {
1647 return new StringDocument("NULL");
1648 }
1649 ExpressionDocumentMapper esm;
1650 ExpressionMapper<ExpressionDocumentMapper> em(esm);
1651 auto* dl = new DocumentList("", "", "");
1652 Document* s = em.map(e);
1653 dl->addDocumentToList(s);
1654 if (!e->isa<VarDecl>() && !e->ann().isEmpty()) {
1655 dl->addDocumentToList(annotation_to_document(e->ann()));
1656 }
1657 return dl;
1658}
1659
1660class ItemDocumentMapper {
1661public:
1662 typedef Document* ret;
1663 static ret mapIncludeI(const IncludeI& ii) {
1664 std::ostringstream oss;
1665 oss << "include \"" << Printer::escapeStringLit(ii.f()) << "\";";
1666 return new StringDocument(oss.str());
1667 }
1668 static ret mapVarDeclI(const VarDeclI& vi) {
1669 auto* dl = new DocumentList("", " ", ";");
1670 dl->addDocumentToList(expression_to_document(vi.e()));
1671 return dl;
1672 }
1673 static ret mapAssignI(const AssignI& ai) {
1674 auto* dl = new DocumentList("", " = ", ";");
1675 dl->addStringToList(std::string(ai.id().c_str(), ai.id().size()));
1676 dl->addDocumentToList(expression_to_document(ai.e()));
1677 return dl;
1678 }
1679 static ret mapConstraintI(const ConstraintI& ci) {
1680 auto* dl = new DocumentList("constraint ", " ", ";");
1681 dl->addDocumentToList(expression_to_document(ci.e()));
1682 return dl;
1683 }
1684 static ret mapSolveI(const SolveI& si) {
1685 auto* dl = new DocumentList("", "", ";");
1686 dl->addStringToList("solve");
1687 if (!si.ann().isEmpty()) {
1688 dl->addDocumentToList(annotation_to_document(si.ann()));
1689 }
1690 switch (si.st()) {
1691 case SolveI::ST_SAT:
1692 dl->addStringToList(" satisfy");
1693 break;
1694 case SolveI::ST_MIN:
1695 dl->addStringToList(" minimize ");
1696 dl->addDocumentToList(expression_to_document(si.e()));
1697 break;
1698 case SolveI::ST_MAX:
1699 dl->addStringToList(" maximize ");
1700 dl->addDocumentToList(expression_to_document(si.e()));
1701 break;
1702 }
1703 return dl;
1704 }
1705 static ret mapOutputI(const OutputI& oi) {
1706 auto* dl = new DocumentList("", " ", ";");
1707 dl->addStringToList("output ");
1708 for (ExpressionSetIter i = oi.ann().begin(); i != oi.ann().end(); ++i) {
1709 Call* c = (*i)->dynamicCast<Call>();
1710 if (c != nullptr && c->id() == "mzn_output_section") {
1711 dl->addStringToList(":: ");
1712 dl->addDocumentToList(expression_to_document(c->arg(0)));
1713 }
1714 }
1715 if (!oi.ann().isEmpty()) {
1716 dl->addStringToList(" ");
1717 }
1718 dl->addDocumentToList(expression_to_document(oi.e()));
1719 return dl;
1720 }
1721 static ret mapFunctionI(const FunctionI& fi) {
1722 DocumentList* dl;
1723 if (fi.ti()->type().isAnn() && fi.e() == nullptr) {
1724 dl = new DocumentList("annotation ", " ", ";", false);
1725 } else if (fi.ti()->type() == Type::parbool()) {
1726 dl = new DocumentList("test ", "", ";", false);
1727 } else if (fi.ti()->type() == Type::varbool()) {
1728 dl = new DocumentList("predicate ", "", ";", false);
1729 } else {
1730 dl = new DocumentList("function ", "", ";", false);
1731 dl->addDocumentToList(expression_to_document(fi.ti()));
1732 dl->addStringToList(": ");
1733 }
1734 dl->addStringToList(std::string(fi.id().c_str(), fi.id().size()));
1735 if (fi.paramCount() > 0) {
1736 auto* params = new DocumentList("(", ", ", ")");
1737 for (unsigned int i = 0; i < fi.paramCount(); i++) {
1738 auto* par = new DocumentList("", "", "");
1739 par->setUnbreakable(true);
1740 par->addDocumentToList(expression_to_document(fi.param(i)));
1741 params->addDocumentToList(par);
1742 }
1743 dl->addDocumentToList(params);
1744 }
1745 if (fi.capturedAnnotationsVar() != nullptr) {
1746 dl->addStringToList(" ann : ");
1747 dl->addDocumentToList(expression_to_document(fi.capturedAnnotationsVar()->id()));
1748 dl->addStringToList(" ");
1749 }
1750 if (!fi.ann().isEmpty()) {
1751 dl->addDocumentToList(annotation_to_document(fi.ann()));
1752 }
1753 if (fi.e() != nullptr) {
1754 dl->addStringToList(" = ");
1755 dl->addBreakPoint();
1756 dl->addDocumentToList(expression_to_document(fi.e()));
1757 }
1758
1759 return dl;
1760 }
1761};
1762
1763class PrettyPrinter {
1764public:
1765 /*
1766 * \brief Constructor for class Pretty Printer
1767 * \param maxwidth (default 80) : number of rows
1768 * \param indentationBase : spaces that represent the atomic number of spaces
1769 * \param sim : whether we want to simplify the result
1770 * \param deepSimp : whether we want to simplify at each breakpoint or not
1771 */
1772 PrettyPrinter(int _maxwidth = 80, int _indentationBase = 4, bool sim = false,
1773 bool deepSimp = false);
1774
1775 void print(Document* d);
1776 void print(std::ostream& os) const;
1777
1778private:
1779 int _maxwidth;
1780 int _indentationBase;
1781 int _currentLine;
1782 int _currentItem;
1783 std::vector<std::vector<Line> > _items;
1784 std::vector<LinesToSimplify> _linesToSimplify;
1785 std::vector<LinesToSimplify> _linesNotToSimplify;
1786 bool _simp;
1787 bool _deeplySimp;
1788
1789 void addItem();
1790
1791 void addLine(int indentation, bool bp = false, bool simpl = false, int level = 0);
1792 static std::string printSpaces(int n);
1793 const std::vector<Line>& getCurrentItemLines() const;
1794
1795 void printDocument(Document* d, bool alignment, int alignmentCol, const std::string& before = "",
1796 const std::string& after = "");
1797 void printDocList(DocumentList* d, int alignmentCol, const std::string& before = "",
1798 const std::string& after = "");
1799 void printStringDoc(StringDocument* d, bool alignment, int alignmentCol,
1800 const std::string& before = "", const std::string& after = "");
1801 void printString(const std::string& s, bool alignment, int alignmentCol);
1802 bool simplify(int item, int line, std::vector<int>* vec);
1803 void simplifyItem(int item);
1804};
1805
1806void PrettyPrinter::print(Document* d) {
1807 addItem();
1808 addLine(0);
1809 printDocument(d, true, 0);
1810 if (_simp) {
1811 simplifyItem(_currentItem);
1812 }
1813}
1814
1815PrettyPrinter::PrettyPrinter(int maxwidth, int indentationBase, bool sim, bool deepsim) {
1816 _maxwidth = maxwidth;
1817 _indentationBase = indentationBase;
1818 _currentLine = -1;
1819 _currentItem = -1;
1820
1821 _simp = sim;
1822 _deeplySimp = deepsim;
1823}
1824const std::vector<Line>& PrettyPrinter::getCurrentItemLines() const { return _items[_currentItem]; }
1825
1826void PrettyPrinter::addLine(int indentation, bool bp, bool simpl, int level) {
1827 _items[_currentItem].push_back(Line(indentation));
1828 _currentLine++;
1829 if (bp && _deeplySimp) {
1830 _linesToSimplify[_currentItem].addLine(level, _currentLine);
1831 if (!simpl) {
1832 _linesNotToSimplify[_currentItem].addLine(0, _currentLine);
1833 }
1834 }
1835}
1836void PrettyPrinter::addItem() {
1837 _items.emplace_back();
1838 _linesToSimplify.emplace_back();
1839 _linesNotToSimplify.emplace_back();
1840 _currentItem++;
1841 _currentLine = -1;
1842}
1843
1844void PrettyPrinter::print(std::ostream& os) const {
1845 std::vector<Line>::const_iterator it;
1846 int nItems = static_cast<int>(_items.size());
1847 for (int item = 0; item < nItems; item++) {
1848 for (it = _items[item].begin(); it != _items[item].end(); it++) {
1849 it->print(os);
1850 }
1851 // os << std::endl;
1852 }
1853}
1854std::string PrettyPrinter::printSpaces(int n) {
1855 std::string result;
1856 for (int i = 0; i < n; i++) {
1857 result += " ";
1858 }
1859 return result;
1860}
1861
1862void PrettyPrinter::printDocument(Document* d, bool alignment, int alignmentCol,
1863 const std::string& before, const std::string& after) {
1864 if (auto* dl = dynamic_cast<DocumentList*>(d)) {
1865 printDocList(dl, alignmentCol, before, after);
1866 } else if (auto* sd = dynamic_cast<StringDocument*>(d)) {
1867 printStringDoc(sd, alignment, alignmentCol, before, after);
1868 } else if (auto* bp = dynamic_cast<BreakPoint*>(d)) {
1869 printString(before, alignment, alignmentCol);
1870 addLine(alignmentCol, _deeplySimp, !bp->getDontSimplify(), d->getLevel());
1871 printString(after, alignment, alignmentCol);
1872 } else {
1873 throw InternalError("PrettyPrinter::print : Wrong type of document");
1874 }
1875}
1876
1877void PrettyPrinter::printStringDoc(StringDocument* d, bool alignment, int alignmentCol,
1878 const std::string& before, const std::string& after) {
1879 std::string s;
1880 if (d != nullptr) {
1881 s = d->getString();
1882 }
1883 s = before + s + after;
1884 printString(s, alignment, alignmentCol);
1885}
1886
1887void PrettyPrinter::printString(const std::string& s, bool alignment, int alignmentCol) {
1888 Line& l = _items[_currentItem][_currentLine];
1889 int size = static_cast<int>(s.size());
1890 if (size <= l.getSpaceLeft(_maxwidth)) {
1891 l.addString(s);
1892 } else {
1893 int col = alignment && _maxwidth - alignmentCol >= size ? alignmentCol : _indentationBase;
1894 addLine(col);
1895 _items[_currentItem][_currentLine].addString(s);
1896 }
1897}
1898
1899void PrettyPrinter::printDocList(DocumentList* d, int alignmentCol, const std::string& super_before,
1900 const std::string& super_after) {
1901 std::vector<Document*> ld = d->getDocs();
1902 std::string beginToken = d->getBeginToken();
1903 std::string separator = d->getSeparator();
1904 std::string endToken = d->getEndToken();
1905 bool _alignment = d->getAlignment();
1906 if (d->getUnbreakable()) {
1907 addLine(alignmentCol);
1908 }
1909 int currentCol = _items[_currentItem][_currentLine].getIndentation() +
1910 _items[_currentItem][_currentLine].getLength();
1911 int newAlignmentCol =
1912 _alignment ? currentCol + static_cast<int>(beginToken.size()) : alignmentCol;
1913 int vectorSize = static_cast<int>(ld.size());
1914 int lastVisibleElementIndex;
1915 for (int i = 0; i < vectorSize; i++) {
1916 if (dynamic_cast<BreakPoint*>(ld[i]) == nullptr) {
1917 lastVisibleElementIndex = i;
1918 }
1919 }
1920 if (vectorSize == 0) {
1921 printStringDoc(nullptr, true, newAlignmentCol, super_before + beginToken,
1922 endToken + super_after);
1923 }
1924 for (int i = 0; i < vectorSize; i++) {
1925 Document* subdoc = ld[i];
1926 bool bp = false;
1927 if (dynamic_cast<BreakPoint*>(subdoc) != nullptr) {
1928 if (!_alignment) {
1929 newAlignmentCol += _indentationBase;
1930 }
1931 bp = true;
1932 }
1933 std::string af;
1934 std::string be;
1935 if (i != vectorSize - 1) {
1936 if (bp || lastVisibleElementIndex <= i) {
1937 af = "";
1938 } else {
1939 af = separator;
1940 }
1941 } else {
1942 af = endToken + super_after;
1943 }
1944 if (i == 0) {
1945 be = super_before + beginToken;
1946 } else {
1947 be = "";
1948 }
1949 printDocument(subdoc, _alignment, newAlignmentCol, be, af);
1950 }
1951 if (d->getUnbreakable()) {
1952 simplify(_currentItem, _currentLine, nullptr);
1953 }
1954}
1955void PrettyPrinter::simplifyItem(int item) {
1956 _linesToSimplify[item].remove(_linesNotToSimplify[item]);
1957 std::vector<int>* vec = (_linesToSimplify[item].getLinesToSimplify());
1958 while (!vec->empty()) {
1959 if (!simplify(item, (*vec)[0], vec)) {
1960 break;
1961 }
1962 }
1963 delete vec;
1964}
1965
1966bool PrettyPrinter::simplify(int item, int line, std::vector<int>* vec) {
1967 if (line == 0) {
1968 _linesToSimplify[item].remove(vec, line, false);
1969 return false;
1970 }
1971 if (_items[item][line].getLength() > _items[item][line - 1].getSpaceLeft(_maxwidth)) {
1972 _linesToSimplify[item].remove(vec, line, false);
1973 return false;
1974 }
1975 _linesToSimplify[item].remove(vec, line, true);
1976 _items[item][line - 1].concatenateLines(_items[item][line]);
1977 _items[item].erase(_items[item].begin() + line);
1978
1979 _linesToSimplify[item].decrementLine(vec, line);
1980 _currentLine--;
1981
1982 return true;
1983}
1984
1985Printer::Printer(std::ostream& os, int width, bool flatZinc, EnvI* env)
1986 : _env(env), _ism(nullptr), _printer(nullptr), _os(os), _width(width), _flatZinc(flatZinc) {}
1987void Printer::init() {
1988 if (_ism == nullptr) {
1989 _ism = new ItemDocumentMapper();
1990 _printer = new PrettyPrinter(_width, 4, true, true);
1991 }
1992}
1993Printer::~Printer() {
1994 delete _printer;
1995 delete _ism;
1996}
1997
1998void Printer::p(Document* d) {
1999 _printer->print(d);
2000 _printer->print(_os);
2001 delete _printer;
2002 _printer = new PrettyPrinter(_width, 4, true, true);
2003}
2004void Printer::p(const Item* i) {
2005 Document* d;
2006 switch (i->iid()) {
2007 case Item::II_INC:
2008 d = ItemDocumentMapper::mapIncludeI(*i->cast<IncludeI>());
2009 break;
2010 case Item::II_VD:
2011 d = ItemDocumentMapper::mapVarDeclI(*i->cast<VarDeclI>());
2012 break;
2013 case Item::II_ASN:
2014 d = ItemDocumentMapper::mapAssignI(*i->cast<AssignI>());
2015 break;
2016 case Item::II_CON:
2017 d = ItemDocumentMapper::mapConstraintI(*i->cast<ConstraintI>());
2018 break;
2019 case Item::II_SOL:
2020 d = ItemDocumentMapper::mapSolveI(*i->cast<SolveI>());
2021 break;
2022 case Item::II_OUT:
2023 d = ItemDocumentMapper::mapOutputI(*i->cast<OutputI>());
2024 break;
2025 case Item::II_FUN:
2026 d = ItemDocumentMapper::mapFunctionI(*i->cast<FunctionI>());
2027 break;
2028 }
2029 p(d);
2030 delete d;
2031}
2032
2033void Printer::print(const Expression* e) {
2034 if (_width == 0) {
2035 PlainPrinter p(_os, _flatZinc, _env);
2036 p.p(e);
2037 } else {
2038 init();
2039 Document* d = expression_to_document(e);
2040 p(d);
2041 delete d;
2042 }
2043}
2044void Printer::print(const Item* i) {
2045 if (_width == 0) {
2046 PlainPrinter p(_os, _flatZinc, _env);
2047 p.p(i);
2048 } else {
2049 init();
2050 p(i);
2051 }
2052}
2053void Printer::print(const Model* m) {
2054 if (_width == 0) {
2055 PlainPrinter p(_os, _flatZinc, _env);
2056 for (auto* i : *m) {
2057 p.p(i);
2058 }
2059 } else {
2060 init();
2061 for (auto* i : *m) {
2062 p(i);
2063 }
2064 }
2065}
2066
2067} // namespace MiniZinc
2068
2069void debugprint(MiniZinc::Expression* e) { std::cerr << *e << "\n"; }
2070void debugprint(MiniZinc::Item* i) { std::cerr << *i; }
2071void debugprint(MiniZinc::Model* m) {
2072 MiniZinc::Printer p(std::cerr, 0);
2073 p.print(m);
2074}
2075void debugprint(const MiniZinc::Location& loc) { std::cerr << loc << std::endl; }