1 /*********************                                                        */
2 /*! \file cvc_printer.cpp
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Morgan Deters, Dejan Jovanovic, Tim King
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
8  ** in the top-level source directory) and their institutional affiliations.
9  ** All rights reserved.  See the file COPYING in the top-level source
10  ** directory for licensing information.\endverbatim
11  **
12  ** \brief The pretty-printer interface for the CVC output language
13  **
14  ** The pretty-printer interface for the CVC output language.
15  **/
16 
17 #include "printer/cvc/cvc_printer.h"
18 
19 #include <algorithm>
20 #include <iostream>
21 #include <iterator>
22 #include <stack>
23 #include <string>
24 #include <typeinfo>
25 #include <vector>
26 
27 #include "expr/expr.h" // for ExprSetDepth etc..
28 #include "expr/node_manager_attributes.h" // for VarNameAttr
29 #include "options/language.h" // for LANG_AST
30 #include "printer/dagification_visitor.h"
31 #include "options/smt_options.h"
32 #include "smt/command.h"
33 #include "smt/smt_engine.h"
34 #include "smt_util/node_visitor.h"
35 #include "theory/arrays/theory_arrays_rewriter.h"
36 #include "theory/substitutions.h"
37 #include "theory/theory_model.h"
38 
39 using namespace std;
40 
41 namespace CVC4 {
42 namespace printer {
43 namespace cvc {
44 
toStream(std::ostream & out,TNode n,int toDepth,bool types,size_t dag) const45 void CvcPrinter::toStream(
46     std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const
47 {
48   if(dag != 0) {
49     DagificationVisitor dv(dag);
50     NodeVisitor<DagificationVisitor> visitor;
51     visitor.run(dv, n);
52     const theory::SubstitutionMap& lets = dv.getLets();
53     if(!lets.empty()) {
54       out << "LET ";
55       bool first = true;
56       for(theory::SubstitutionMap::const_iterator i = lets.begin();
57           i != lets.end();
58           ++i) {
59         if(! first) {
60           out << ", ";
61         } else {
62           first = false;
63         }
64         toStream(out, (*i).second, toDepth, types, false);
65         out << " = ";
66         toStream(out, (*i).first, toDepth, types, false);
67       }
68       out << " IN ";
69     }
70     Node body = dv.getDagifiedBody();
71     toStream(out, body, toDepth, types, false);
72   } else {
73     toStream(out, n, toDepth, types, false);
74   }
75 }
76 
toStreamRational(std::ostream & out,Node n,bool forceRational)77 void toStreamRational(std::ostream& out, Node n, bool forceRational)
78 {
79   Assert(n.getKind() == kind::CONST_RATIONAL);
80   const Rational& rat = n.getConst<Rational>();
81   if (rat.isIntegral() && !forceRational)
82   {
83     out << rat.getNumerator();
84   }
85   else
86   {
87     out << '(' << rat.getNumerator() << '/' << rat.getDenominator() << ')';
88   }
89 }
90 
toStream(std::ostream & out,TNode n,int depth,bool types,bool bracket) const91 void CvcPrinter::toStream(
92     std::ostream& out, TNode n, int depth, bool types, bool bracket) const
93 {
94   if (depth == 0) {
95     out << "(...)";
96   } else {
97     --depth;
98   }
99 
100   // null
101   if(n.getKind() == kind::NULL_EXPR) {
102     out << "null";
103     return;
104   }
105 
106   // variables
107   if(n.isVar()) {
108     string s;
109     if(n.getAttribute(expr::VarNameAttr(), s)) {
110       out << s;
111     } else {
112       if(n.getKind() == kind::VARIABLE) {
113         out << "var_";
114       } else {
115         out << n.getKind() << '_';
116       }
117       out << n.getId();
118     }
119     if(types) {
120       // print the whole type, but not *its* type
121       out << ":";
122       n.getType().toStream(out, language::output::LANG_CVC4);
123     }
124     return;
125   }
126   if(n.isNullaryOp()) {
127     if( n.getKind() == kind::UNIVERSE_SET ){
128       out << "UNIVERSE :: " << n.getType();
129     }else{
130       //unknown printer
131       out << n.getKind();
132     }
133     return;
134   }
135 
136   // constants
137   if(n.getMetaKind() == kind::metakind::CONSTANT) {
138     switch(n.getKind()) {
139     case kind::BITVECTOR_TYPE:
140       out << "BITVECTOR(" << n.getConst<BitVectorSize>().size << ")";
141       break;
142     case kind::CONST_BITVECTOR: {
143       const BitVector& bv = n.getConst<BitVector>();
144       const Integer& x = bv.getValue();
145       out << "0bin";
146       unsigned n = bv.getSize();
147       while(n-- > 0) {
148         out << (x.testBit(n) ? '1' : '0');
149       }
150       break;
151     }
152     case kind::CONST_BOOLEAN:
153       // the default would print "1" or "0" for bool, that's not correct
154       // for our purposes
155       out << (n.getConst<bool>() ? "TRUE" : "FALSE");
156       break;
157     case kind::CONST_RATIONAL: {
158       toStreamRational(out, n, false);
159       break;
160     }
161     case kind::TYPE_CONSTANT:
162       switch(TypeConstant tc = n.getConst<TypeConstant>()) {
163       case REAL_TYPE:
164         out << "REAL";
165         break;
166       case INTEGER_TYPE:
167         out << "INT";
168         break;
169       case BOOLEAN_TYPE:
170         out << "BOOLEAN";
171         break;
172       case STRING_TYPE:
173         out << "STRING";
174         break;
175       default:
176         out << tc;
177         break;
178       }
179       break;
180 
181     case kind::DATATYPE_TYPE: {
182       const Datatype& dt = (NodeManager::currentNM()->getDatatypeForIndex( n.getConst< DatatypeIndexConstant >().getIndex() ));
183       if( dt.isTuple() ){
184         out << '[';
185         for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) {
186           if (i > 0) {
187             out << ", ";
188           }
189           Type t = ((SelectorType)dt[0][i].getSelector().getType()).getRangeType();
190           out << t;
191         }
192         out << ']';
193       }else if( dt.isRecord() ){
194         out << "[# ";
195         for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) {
196           if (i > 0) {
197             out << ", ";
198           }
199           Type t = ((SelectorType)dt[0][i].getSelector().getType()).getRangeType();
200           out << dt[0][i].getSelector() << ":" << t;
201         }
202         out << " #]";
203       }else{
204         out << dt.getName();
205       }
206     }
207       break;
208 
209     case kind::EMPTYSET:
210       out << "{} :: " << n.getConst<EmptySet>().getType();
211       break;
212 
213     case kind::STORE_ALL: {
214       const ArrayStoreAll& asa = n.getConst<ArrayStoreAll>();
215       out << "ARRAY(" << asa.getType().getIndexType() << " OF "
216           << asa.getType().getConstituentType() << ") : " << asa.getExpr();
217       break;
218     }
219 
220     default:
221       // Fall back to whatever operator<< does on underlying type; we
222       // might luck out and print something reasonable.
223       kind::metakind::NodeValueConstPrinter::toStream(out, n);
224     }
225 
226     return;
227   }
228 
229   enum OpType {
230     PREFIX,
231     INFIX,
232     POSTFIX
233   } opType;
234 
235   //The default operation type is PREFIX
236   opType = PREFIX;
237 
238   stringstream op;       // operation (such as '+')
239 
240   switch(n.getKind()) {
241 
242     // BUILTIN
243     case kind::EQUAL:
244       if( n[0].getType().isBoolean() ){
245         op << "<=>";
246       }else{
247         op << '=';
248       }
249       opType = INFIX;
250       break;
251     case kind::ITE:
252       out << "IF ";
253       toStream(out, n[0], depth, types, true);
254       out << " THEN ";
255       toStream(out, n[1], depth, types, true);
256       out << " ELSE ";
257       toStream(out, n[2], depth, types, true);
258       out << " ENDIF";
259       return;
260       break;
261     case kind::SEXPR_TYPE:
262       out << '[';
263       for (unsigned i = 0; i < n.getNumChildren(); ++ i) {
264         if (i > 0) {
265           out << ", ";
266         }
267         toStream(out, n[i], depth, types, false);
268       }
269       out << ']';
270       return;
271       break;
272     case kind::SEXPR:
273       // no-op
274       break;
275     case kind::LAMBDA:
276       out << "(LAMBDA";
277       toStream(out, n[0], depth, types, true);
278       out << ": ";
279       toStream(out, n[1], depth, types, true);
280       out << ")";
281       return;
282       break;
283     case kind::APPLY:
284       toStream(op, n.getOperator(), depth, types, true);
285       break;
286     case kind::CHAIN:
287     case kind::DISTINCT: // chain and distinct not supported directly in CVC4, blast them away with the rewriter
288       toStream(out, theory::Rewriter::rewrite(n), depth, types, true);
289       return;
290     case kind::SORT_TYPE:
291     {
292       string name;
293       if(n.getAttribute(expr::VarNameAttr(), name)) {
294         out << name;
295         return;
296       }
297     }
298     break;
299 
300     // BOOL
301     case kind::AND:
302       op << "AND";
303       opType = INFIX;
304       break;
305     case kind::OR:
306       op << "OR";
307       opType = INFIX;
308       break;
309     case kind::NOT:
310       op << "NOT";
311       opType = PREFIX;
312       break;
313     case kind::XOR:
314       op << "XOR";
315       opType = INFIX;
316       break;
317     case kind::IMPLIES:
318       op << "=>";
319       opType = INFIX;
320       break;
321 
322     // UF
323     case kind::APPLY_UF:
324       toStream(op, n.getOperator(), depth, types, false);
325       break;
326     case kind::CARDINALITY_CONSTRAINT:
327     case kind::COMBINED_CARDINALITY_CONSTRAINT:
328       out << "CARDINALITY_CONSTRAINT";
329       break;
330 
331     case kind::FUNCTION_TYPE:
332       if (n.getNumChildren() > 1) {
333         if (n.getNumChildren() > 2) {
334           out << '(';
335         }
336         for (unsigned i = 1; i < n.getNumChildren(); ++i) {
337           if (i > 1) {
338             out << ", ";
339           }
340           toStream(out, n[i - 1], depth, types, false);
341         }
342         if (n.getNumChildren() > 2) {
343           out << ')';
344         }
345       }
346       out << " -> ";
347       toStream(out, n[n.getNumChildren() - 1], depth, types, false);
348       return;
349       break;
350 
351     // DATATYPES
352     case kind::PARAMETRIC_DATATYPE: {
353         const Datatype & dt = (NodeManager::currentNM()->getDatatypeForIndex( n[0].getConst< DatatypeIndexConstant >().getIndex() ));
354         out << dt.getName() << '[';
355         for(unsigned i = 1; i < n.getNumChildren(); ++i) {
356           if(i > 1) {
357             out << ',';
358           }
359           out << n[i];
360         }
361         out << ']';
362       }
363       return;
364       break;
365     case kind::APPLY_TYPE_ASCRIPTION: {
366         toStream(out, n[0], depth, types, false);
367         out << "::";
368         TypeNode t = TypeNode::fromType(n.getOperator().getConst<AscriptionType>().getType());
369         out << (t.isFunctionLike() ? t.getRangeType() : t);
370       }
371       return;
372       break;
373     case kind::APPLY_CONSTRUCTOR: {
374         TypeNode t = n.getType();
375         if( t.isTuple() ){
376           if( n.getNumChildren()==1 ){
377             out << "TUPLE";
378           }
379         }else if( t.isRecord() ){
380           const Record& rec = t.getRecord();
381           out << "(# ";
382           TNode::iterator i = n.begin();
383           bool first = true;
384           const Record::FieldVector& fields = rec.getFields();
385           for(Record::FieldVector::const_iterator j = fields.begin(); j != fields.end(); ++i, ++j) {
386             if(!first) {
387               out << ", ";
388             }
389             out << (*j).first << " := ";
390             toStream(out, *i, depth, types, false);
391             first = false;
392           }
393           out << " #)";
394           return;
395         }else{
396           toStream(op, n.getOperator(), depth, types, false);
397           if (n.getNumChildren() == 0)
398           {
399             // for datatype constants d, we print "d" and not "d()"
400             out << op.str();
401             return;
402           }
403         }
404       }
405       break;
406     case kind::APPLY_SELECTOR:
407     case kind::APPLY_SELECTOR_TOTAL: {
408         TypeNode t = n[0].getType();
409         Node opn = n.getOperator();
410         if (t.isTuple() || t.isRecord())
411         {
412           toStream(out, n[0], depth, types, true);
413           out << '.';
414           const Datatype& dt = ((DatatypeType)t.toType()).getDatatype();
415           if (t.isTuple())
416           {
417             int sindex;
418             if (n.getKind() == kind::APPLY_SELECTOR)
419             {
420               sindex = Datatype::indexOf(opn.toExpr());
421             }
422             else
423             {
424               sindex = dt[0].getSelectorIndexInternal(opn.toExpr());
425             }
426             Assert(sindex >= 0);
427             out << sindex;
428           }
429           else
430           {
431             toStream(out, opn, depth, types, false);
432           }
433           return;
434         }else{
435           toStream(op, opn, depth, types, false);
436         }
437       }
438       break;
439     case kind::APPLY_TESTER: {
440       Assert( !n.getType().isTuple() && !n.getType().isRecord() );
441       op << "is_";
442       unsigned cindex = Datatype::indexOf(n.getOperator().toExpr());
443       const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
444       toStream(op, Node::fromExpr(dt[cindex].getConstructor()), depth, types, false);
445     }
446       break;
447     case kind::CONSTRUCTOR_TYPE:
448     case kind::SELECTOR_TYPE:
449       if(n.getNumChildren() > 1) {
450         if(n.getNumChildren() > 2) {
451           out << '(';
452         }
453         for(unsigned i = 0; i < n.getNumChildren() - 1; ++i) {
454           if(i > 0) {
455             out << ", ";
456           }
457           toStream(out, n[i], depth, types, false);
458         }
459         if(n.getNumChildren() > 2) {
460           out << ')';
461         }
462         out << " -> ";
463       }
464       toStream(out, n[n.getNumChildren() - 1], depth, types, false);
465       return;
466     case kind::TESTER_TYPE:
467       toStream(out, n[0], depth, types, false);
468       out << " -> BOOLEAN";
469       return;
470       break;
471     case kind::TUPLE_UPDATE:
472       toStream(out, n[0], depth, types, true);
473       out << " WITH ." << n.getOperator().getConst<TupleUpdate>().getIndex() << " := ";
474       toStream(out, n[1], depth, types, true);
475       return;
476       break;
477     case kind::RECORD_UPDATE:
478       toStream(out, n[0], depth, types, true);
479       out << " WITH ." << n.getOperator().getConst<RecordUpdate>().getField() << " := ";
480       toStream(out, n[1], depth, types, true);
481       return;
482       break;
483 
484     // ARRAYS
485     case kind::ARRAY_TYPE:
486       out << "ARRAY ";
487       toStream(out, n[0], depth, types, false);
488       out << " OF ";
489       toStream(out, n[1], depth, types, false);
490       return;
491       break;
492     case kind::SELECT:
493       toStream(out, n[0], depth, types, true);
494       out << '[';
495       toStream(out, n[1], depth, types, false);
496       out << ']';
497       return;
498       break;
499     case kind::STORE: {
500       stack<TNode> stk;
501       stk.push(n);
502       while(stk.top()[0].getKind() == kind::STORE) {
503         stk.push(stk.top()[0]);
504       }
505       if (bracket) {
506         out << '(';
507       }
508       TNode x = stk.top();
509       toStream(out, x[0], depth, types, false);
510       out << " WITH [";
511       toStream(out, x[1], depth, types, false);
512       out << "] := ";
513       toStream(out, x[2], depth, types, false);
514       stk.pop();
515       while(!stk.empty()) {
516         x = stk.top();
517         out << ", [";
518         toStream(out, x[1], depth, types, false);
519         out << "] := ";
520         toStream(out, x[2], depth, types, false);
521         stk.pop();
522       }
523       if (bracket) {
524         out << ')';
525       }
526       return;
527       break;
528     }
529 
530     // ARITHMETIC
531     case kind::PLUS:
532       op << '+';
533       opType = INFIX;
534       break;
535     case kind::MULT:
536     case kind::NONLINEAR_MULT:
537       op << '*';
538       opType = INFIX;
539       break;
540     case kind::MINUS:
541       op << '-';
542       opType = INFIX;
543       break;
544     case kind::UMINUS:
545       op << '-';
546       opType = PREFIX;
547       break;
548     case kind::DIVISION:
549     case kind::DIVISION_TOTAL:
550       op << '/';
551       opType = INFIX;
552       break;
553     case kind::INTS_DIVISION:
554     case kind::INTS_DIVISION_TOTAL:
555       op << "DIV";
556       opType = INFIX;
557       break;
558     case kind::INTS_MODULUS:
559     case kind::INTS_MODULUS_TOTAL:
560       op << "MOD";
561       opType = INFIX;
562       break;
563     case kind::LT:
564       op << '<';
565       opType = INFIX;
566       break;
567     case kind::LEQ:
568       op << "<=";
569       opType = INFIX;
570       break;
571     case kind::GT:
572       op << '>';
573       opType = INFIX;
574       break;
575     case kind::GEQ:
576       op << ">=";
577       opType = INFIX;
578       break;
579     case kind::POW:
580       op << '^';
581       opType = INFIX;
582       break;
583     case kind::ABS:
584       op << "ABS";
585       opType = PREFIX;
586       break;
587     case kind::IS_INTEGER:
588       op << "IS_INTEGER";
589       opType = PREFIX;
590       break;
591     case kind::TO_INTEGER:
592       op << "FLOOR";
593       opType = PREFIX;
594       break;
595     case kind::TO_REAL:
596       if (n[0].getKind() == kind::CONST_RATIONAL)
597       {
598         // print the constant as a rational
599         toStreamRational(out, n[0], true);
600       }
601       else
602       {
603         // ignore, there is no to-real in CVC language
604         toStream(out, n[0], depth, types, false);
605       }
606       return;
607     case kind::DIVISIBLE:
608       out << "DIVISIBLE(";
609       toStream(out, n[0], depth, types, false);
610       out << ", " << n.getOperator().getConst<Divisible>().k << ")";
611       return;
612 
613     // BITVECTORS
614     case kind::BITVECTOR_XOR:
615       op << "BVXOR";
616       break;
617     case kind::BITVECTOR_NAND:
618       op << "BVNAND";
619       break;
620     case kind::BITVECTOR_NOR:
621       op << "BVNOR";
622       break;
623     case kind::BITVECTOR_XNOR:
624       op << "BVXNOR";
625       break;
626     case kind::BITVECTOR_COMP:
627       op << "BVCOMP";
628       break;
629     case kind::BITVECTOR_UDIV:
630       op << "BVUDIV";
631       break;
632     case kind::BITVECTOR_UDIV_TOTAL:
633       op << "BVUDIV_TOTAL";
634       break;
635     case kind::BITVECTOR_UREM:
636       op << "BVUREM";
637       break;
638     case kind::BITVECTOR_UREM_TOTAL:
639       op << "BVUREM_TOTAL";
640       break;
641     case kind::BITVECTOR_SDIV:
642       op << "BVSDIV";
643       break;
644     case kind::BITVECTOR_SREM:
645       op << "BVSREM";
646       break;
647     case kind::BITVECTOR_SMOD:
648       op << "BVSMOD";
649       break;
650     case kind::BITVECTOR_SHL:
651       op << "BVSHL";
652       break;
653     case kind::BITVECTOR_LSHR:
654       op << "BVLSHR";
655       break;
656     case kind::BITVECTOR_ASHR:
657       op << "BVASHR";
658       break;
659     case kind::BITVECTOR_ULT:
660       op << "BVLT";
661       break;
662     case kind::BITVECTOR_ULE:
663       op << "BVLE";
664       break;
665     case kind::BITVECTOR_UGT:
666       op << "BVGT";
667       break;
668     case kind::BITVECTOR_UGE:
669       op << "BVGE";
670       break;
671     case kind::BITVECTOR_SLT:
672       op << "BVSLT";
673       break;
674     case kind::BITVECTOR_SLE:
675       op << "BVSLE";
676       break;
677     case kind::BITVECTOR_SGT:
678       op << "BVSGT";
679       break;
680     case kind::BITVECTOR_SGE:
681       op << "BVSGE";
682       break;
683     case kind::BITVECTOR_NEG:
684       op << "BVUMINUS";
685       break;
686     case kind::BITVECTOR_NOT:
687       op << "~";
688       break;
689     case kind::BITVECTOR_AND:
690       op << "&";
691       opType = INFIX;
692       break;
693     case kind::BITVECTOR_OR:
694       op << "|";
695       opType = INFIX;
696       break;
697     case kind::BITVECTOR_CONCAT:
698       op << "@";
699       opType = INFIX;
700       break;
701     case kind::BITVECTOR_PLUS: {
702       // This interprets a BITVECTOR_PLUS as a bvadd in SMT-LIB
703       Assert(n.getType().isBitVector());
704       unsigned numc = n.getNumChildren()-2;
705       unsigned child = 0;
706       while (child < numc) {
707         out << "BVPLUS(";
708         out << BitVectorType(n.getType().toType()).getSize();
709         out << ',';
710         toStream(out, n[child], depth, types, false);
711         out << ',';
712         ++child;
713       }
714       out << "BVPLUS(";
715       out << BitVectorType(n.getType().toType()).getSize();
716       out << ',';
717       toStream(out, n[child], depth, types, false);
718       out << ',';
719       toStream(out, n[child + 1], depth, types, false);
720       while (child > 0) {
721         out << ')';
722         --child;
723       }
724       out << ')';
725       return;
726       break;
727     }
728     case kind::BITVECTOR_SUB:
729       out << "BVSUB(";
730       Assert(n.getType().isBitVector());
731       out << BitVectorType(n.getType().toType()).getSize();
732       out << ',';
733       toStream(out, n[0], depth, types, false);
734       out << ',';
735       toStream(out, n[1], depth, types, false);
736       out << ')';
737       return;
738       break;
739     case kind::BITVECTOR_MULT: {
740       Assert(n.getType().isBitVector());
741       unsigned numc = n.getNumChildren()-2;
742       unsigned child = 0;
743       while (child < numc) {
744         out << "BVMULT(";
745         out << BitVectorType(n.getType().toType()).getSize();
746         out << ',';
747         toStream(out, n[child], depth, types, false);
748         out << ',';
749         ++child;
750         }
751       out << "BVMULT(";
752       out << BitVectorType(n.getType().toType()).getSize();
753       out << ',';
754       toStream(out, n[child], depth, types, false);
755       out << ',';
756       toStream(out, n[child + 1], depth, types, false);
757       while (child > 0) {
758         out << ')';
759         --child;
760       }
761       out << ')';
762       return;
763       break;
764     }
765     case kind::BITVECTOR_EXTRACT:
766       op << n.getOperator().getConst<BitVectorExtract>();
767       opType = POSTFIX;
768       break;
769     case kind::BITVECTOR_BITOF:
770       op << n.getOperator().getConst<BitVectorBitOf>();
771       opType = POSTFIX;
772       break;
773     case kind::BITVECTOR_REPEAT:
774       out << "BVREPEAT(";
775       toStream(out, n[0], depth, types, false);
776       out << ", " << n.getOperator().getConst<BitVectorRepeat>() << ')';
777       return;
778       break;
779     case kind::BITVECTOR_ZERO_EXTEND:
780       out << "BVZEROEXTEND(";
781       toStream(out, n[0], depth, types, false);
782       out << ", " << n.getOperator().getConst<BitVectorZeroExtend>() << ')';
783       return;
784       break;
785     case kind::BITVECTOR_SIGN_EXTEND:
786       out << "SX(";
787       toStream(out, n[0], depth, types, false);
788       out << ", " << BitVectorType(n.getType().toType()).getSize() << ')';
789       return;
790       break;
791     case kind::BITVECTOR_ROTATE_LEFT:
792       out << "BVROTL(";
793       toStream(out, n[0], depth, types, false);
794       out << ", " << n.getOperator().getConst<BitVectorRotateLeft>() << ')';
795       return;
796       break;
797     case kind::BITVECTOR_ROTATE_RIGHT:
798       out << "BVROTR(";
799       toStream(out, n[0], depth, types, false);
800       out << ", " << n.getOperator().getConst<BitVectorRotateRight>() << ')';
801       return;
802       break;
803 
804     // SETS
805     case kind::SET_TYPE:
806       out << "SET OF ";
807       toStream(out, n[0], depth, types, false);
808       return;
809       break;
810     case kind::UNION:
811       op << '|';
812       opType = INFIX;
813       break;
814     case kind::INTERSECTION:
815       op << '&';
816       opType = INFIX;
817       break;
818     case kind::SETMINUS:
819       op << '-';
820       opType = INFIX;
821       break;
822     case kind::SUBSET:
823       op << "<=";
824       opType = INFIX;
825       break;
826     case kind::MEMBER:
827       op << "IS_IN";
828       opType = INFIX;
829       break;
830     case kind::COMPLEMENT:
831       op << "~";
832       opType = PREFIX;
833       break;
834     case kind::PRODUCT:
835       op << "PRODUCT";
836       opType = INFIX;
837       break;
838     case kind::JOIN:
839       op << "JOIN";
840       opType = INFIX;
841       break;
842     case kind::TRANSPOSE:
843       op << "TRANSPOSE";
844       opType = PREFIX;
845       break;
846     case kind::TCLOSURE:
847       op << "TCLOSURE";
848       opType = PREFIX;
849       break;
850     case kind::IDEN:
851       op << "IDEN";
852       opType = PREFIX;
853       break;
854     case kind::JOIN_IMAGE:
855       op << "JOIN_IMAGE";
856       opType = INFIX;
857       break;
858     case kind::SINGLETON:
859       out << "{";
860       toStream(out, n[0], depth, types, false);
861       out << "}";
862       return;
863       break;
864     case kind::INSERT: {
865       if(bracket) {
866         out << '(';
867       }
868       out << '{';
869       size_t i = 0;
870       toStream(out, n[i++], depth, types, false);
871       for(;i+1 < n.getNumChildren(); ++i) {
872         out << ", ";
873         toStream(out, n[i], depth, types, false);
874       }
875       out << "} | ";
876       toStream(out, n[i], depth, types, true);
877       if(bracket) {
878         out << ')';
879       }
880       return;
881       break;
882     }
883     case kind::CARD: {
884       out << "CARD(";
885       toStream(out, n[0], depth, types, false);
886       out << ")";
887       return;
888       break;
889     }
890 
891     // Quantifiers
892     case kind::FORALL:
893       out << "(FORALL";
894       toStream(out, n[0], depth, types, false);
895       out << " : ";
896       toStream(out, n[1], depth, types, false);
897       out << ')';
898       // TODO: user patterns?
899       return;
900     case kind::EXISTS:
901       out << "(EXISTS";
902       toStream(out, n[0], depth, types, false);
903       out << " : ";
904       toStream(out, n[1], depth, types, false);
905       out << ')';
906       // TODO: user patterns?
907       return;
908     case kind::INST_CONSTANT:
909       out << "INST_CONSTANT";
910       break;
911     case kind::BOUND_VAR_LIST:
912       out << '(';
913       for(size_t i = 0; i < n.getNumChildren(); ++i) {
914         if(i > 0) {
915           out << ", ";
916         }
917         toStream(out, n[i], -1, true, false); // ascribe types
918       }
919       out << ')';
920       return;
921     case kind::INST_PATTERN:
922       out << "INST_PATTERN";
923       break;
924     case kind::INST_PATTERN_LIST:
925       out << "INST_PATTERN_LIST";
926       break;
927 
928     // string operators
929     case kind::STRING_CONCAT:
930       out << "CONCAT";
931       break;
932     case kind::STRING_CHARAT:
933       out << "CHARAT";
934       break;
935     case kind::STRING_LENGTH:
936       out << "LENGTH";
937       break;
938     case kind::STRING_SUBSTR: out << "SUBSTR"; break;
939 
940     default:
941       Warning() << "Kind printing not implemented for the case of " << n.getKind() << endl;
942       break;
943   }
944 
945   switch (opType) {
946   case PREFIX:
947     out << op.str();
948     if (n.getNumChildren() > 0)
949     {
950       out << '(';
951     }
952     break;
953   case INFIX:
954     if (bracket) {
955       out << '(';
956     }
957     break;
958   case POSTFIX:
959     out << '(';
960     break;
961   }
962 
963   for (unsigned i = 0; i < n.getNumChildren(); ++ i) {
964     if (i > 0) {
965       if (opType == INFIX) {
966         out << ' ' << op.str() << ' ';
967       } else {
968         out << ", ";
969       }
970     }
971     toStream(out, n[i], depth, types, opType == INFIX);
972   }
973 
974   switch (opType) {
975     case PREFIX:
976       if (n.getNumChildren() > 0)
977       {
978         out << ')';
979       }
980       break;
981     case INFIX:
982       if (bracket) {
983         out << ')';
984       }
985       break;
986     case POSTFIX:
987       out << ')' << op.str();
988       break;
989   }
990 
991 }/* CvcPrinter::toStream(TNode) */
992 
993 template <class T>
994 static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode);
995 
toStream(std::ostream & out,const Command * c,int toDepth,bool types,size_t dag) const996 void CvcPrinter::toStream(std::ostream& out,
997                           const Command* c,
998                           int toDepth,
999                           bool types,
1000                           size_t dag) const
1001 {
1002   expr::ExprSetDepth::Scope sdScope(out, toDepth);
1003   expr::ExprPrintTypes::Scope ptScope(out, types);
1004   expr::ExprDag::Scope dagScope(out, dag);
1005 
1006   if(tryToStream<AssertCommand>(out, c, d_cvc3Mode) ||
1007      tryToStream<PushCommand>(out, c, d_cvc3Mode) ||
1008      tryToStream<PopCommand>(out, c, d_cvc3Mode) ||
1009      tryToStream<CheckSatCommand>(out, c, d_cvc3Mode) ||
1010      tryToStream<CheckSatAssumingCommand>(out, c, d_cvc3Mode) ||
1011      tryToStream<QueryCommand>(out, c, d_cvc3Mode) ||
1012      tryToStream<ResetCommand>(out, c, d_cvc3Mode) ||
1013      tryToStream<ResetAssertionsCommand>(out, c, d_cvc3Mode) ||
1014      tryToStream<QuitCommand>(out, c, d_cvc3Mode) ||
1015      tryToStream<DeclarationSequence>(out, c, d_cvc3Mode) ||
1016      tryToStream<CommandSequence>(out, c, d_cvc3Mode) ||
1017      tryToStream<DeclareFunctionCommand>(out, c, d_cvc3Mode) ||
1018      tryToStream<DeclareTypeCommand>(out, c, d_cvc3Mode) ||
1019      tryToStream<DefineTypeCommand>(out, c, d_cvc3Mode) ||
1020      tryToStream<DefineNamedFunctionCommand>(out, c, d_cvc3Mode) ||
1021      tryToStream<DefineFunctionCommand>(out, c, d_cvc3Mode) ||
1022      tryToStream<SimplifyCommand>(out, c, d_cvc3Mode) ||
1023      tryToStream<GetValueCommand>(out, c, d_cvc3Mode) ||
1024      tryToStream<GetModelCommand>(out, c, d_cvc3Mode) ||
1025      tryToStream<GetAssignmentCommand>(out, c, d_cvc3Mode) ||
1026      tryToStream<GetAssertionsCommand>(out, c, d_cvc3Mode) ||
1027      tryToStream<GetProofCommand>(out, c, d_cvc3Mode) ||
1028      tryToStream<GetUnsatCoreCommand>(out, c, d_cvc3Mode) ||
1029      tryToStream<SetBenchmarkStatusCommand>(out, c, d_cvc3Mode) ||
1030      tryToStream<SetBenchmarkLogicCommand>(out, c, d_cvc3Mode) ||
1031      tryToStream<SetInfoCommand>(out, c, d_cvc3Mode) ||
1032      tryToStream<GetInfoCommand>(out, c, d_cvc3Mode) ||
1033      tryToStream<SetOptionCommand>(out, c, d_cvc3Mode) ||
1034      tryToStream<GetOptionCommand>(out, c, d_cvc3Mode) ||
1035      tryToStream<DatatypeDeclarationCommand>(out, c, d_cvc3Mode) ||
1036      tryToStream<CommentCommand>(out, c, d_cvc3Mode) ||
1037      tryToStream<EmptyCommand>(out, c, d_cvc3Mode) ||
1038      tryToStream<EchoCommand>(out, c, d_cvc3Mode)) {
1039     return;
1040   }
1041 
1042   out << "ERROR: don't know how to print a Command of class: "
1043       << typeid(*c).name() << endl;
1044 
1045 }/* CvcPrinter::toStream(Command*) */
1046 
1047 template <class T>
1048 static bool tryToStream(std::ostream& out,
1049                         const CommandStatus* s,
1050                         bool cvc3Mode);
1051 
toStream(std::ostream & out,const CommandStatus * s) const1052 void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const
1053 {
1054   if(tryToStream<CommandSuccess>(out, s, d_cvc3Mode) ||
1055      tryToStream<CommandFailure>(out, s, d_cvc3Mode) ||
1056      tryToStream<CommandUnsupported>(out, s, d_cvc3Mode) ||
1057      tryToStream<CommandInterrupted>(out, s, d_cvc3Mode)) {
1058     return;
1059   }
1060 
1061   out << "ERROR: don't know how to print a CommandStatus of class: "
1062       << typeid(*s).name() << endl;
1063 
1064 }/* CvcPrinter::toStream(CommandStatus*) */
1065 
1066 namespace {
1067 
DeclareTypeCommandToStream(std::ostream & out,const theory::TheoryModel & model,const DeclareTypeCommand & command)1068 void DeclareTypeCommandToStream(std::ostream& out,
1069                                 const theory::TheoryModel& model,
1070                                 const DeclareTypeCommand& command)
1071 {
1072   TypeNode type_node = TypeNode::fromType(command.getType());
1073   const std::vector<Node>* type_reps =
1074       model.getRepSet()->getTypeRepsOrNull(type_node);
1075   if (options::modelUninterpDtEnum() && type_node.isSort()
1076       && type_reps != nullptr)
1077   {
1078     out << "DATATYPE" << std::endl;
1079     out << "  " << command.getSymbol() << " = ";
1080     for (size_t i = 0; i < type_reps->size(); i++)
1081     {
1082       if (i > 0)
1083       {
1084         out << "| ";
1085       }
1086       out << (*type_reps)[i] << " ";
1087     }
1088     out << std::endl << "END;" << std::endl;
1089   }
1090   else if (type_node.isSort() && type_reps != nullptr)
1091   {
1092     out << "% cardinality of " << type_node << " is " << type_reps->size()
1093         << std::endl;
1094     out << command << std::endl;
1095     for (Node type_rep : *type_reps)
1096     {
1097       if (type_rep.isVar())
1098       {
1099         out << type_rep << " : " << type_node << ";" << std::endl;
1100       }
1101       else
1102       {
1103         out << "% rep: " << type_rep << std::endl;
1104       }
1105     }
1106   }
1107   else
1108   {
1109     out << command << std::endl;
1110   }
1111 }
1112 
DeclareFunctionCommandToStream(std::ostream & out,const theory::TheoryModel & model,const DeclareFunctionCommand & command)1113 void DeclareFunctionCommandToStream(std::ostream& out,
1114                                     const theory::TheoryModel& model,
1115                                     const DeclareFunctionCommand& command)
1116 {
1117   Node n = Node::fromExpr(command.getFunction());
1118   if (n.getKind() == kind::SKOLEM)
1119   {
1120     // don't print out internal stuff
1121     return;
1122   }
1123   TypeNode tn = n.getType();
1124   out << n << " : ";
1125   if (tn.isFunction() || tn.isPredicate())
1126   {
1127     out << "(";
1128     for (size_t i = 0; i < tn.getNumChildren() - 1; i++)
1129     {
1130       if (i > 0)
1131       {
1132         out << ", ";
1133       }
1134       out << tn[i];
1135     }
1136     out << ") -> " << tn.getRangeType();
1137   }
1138   else
1139   {
1140     out << tn;
1141   }
1142   Node val = Node::fromExpr(model.getSmtEngine()->getValue(n.toExpr()));
1143   if (options::modelUninterpDtEnum() && val.getKind() == kind::STORE)
1144   {
1145     TypeNode type_node = val[1].getType();
1146     if (tn.isSort())
1147     {
1148       if (const std::vector<Node>* type_reps =
1149               model.getRepSet()->getTypeRepsOrNull(type_node))
1150       {
1151         Cardinality indexCard(type_reps->size());
1152         val = theory::arrays::TheoryArraysRewriter::normalizeConstant(
1153             val, indexCard);
1154       }
1155     }
1156   }
1157   out << " = " << val << ";" << std::endl;
1158 }
1159 
1160 }  // namespace
1161 
toStream(std::ostream & out,const Model & model,const Command * command) const1162 void CvcPrinter::toStream(std::ostream& out,
1163                           const Model& model,
1164                           const Command* command) const
1165 {
1166   const auto* theory_model = dynamic_cast<const theory::TheoryModel*>(&model);
1167   AlwaysAssert(theory_model != nullptr);
1168   if (const auto* declare_type_command =
1169           dynamic_cast<const DeclareTypeCommand*>(command))
1170   {
1171     DeclareTypeCommandToStream(out, *theory_model, *declare_type_command);
1172   }
1173   else if (const auto* dfc =
1174                dynamic_cast<const DeclareFunctionCommand*>(command))
1175   {
1176     DeclareFunctionCommandToStream(out, *theory_model, *dfc);
1177   }
1178   else
1179   {
1180     out << command << std::endl;
1181   }
1182 }
1183 
toStream(std::ostream & out,const AssertCommand * c,bool cvc3Mode)1184 static void toStream(std::ostream& out, const AssertCommand* c, bool cvc3Mode)
1185 {
1186   out << "ASSERT " << c->getExpr() << ";";
1187 }
1188 
toStream(std::ostream & out,const PushCommand * c,bool cvc3Mode)1189 static void toStream(std::ostream& out, const PushCommand* c, bool cvc3Mode)
1190 {
1191   out << "PUSH;";
1192 }
1193 
toStream(std::ostream & out,const PopCommand * c,bool cvc3Mode)1194 static void toStream(std::ostream& out, const PopCommand* c, bool cvc3Mode)
1195 {
1196   out << "POP;";
1197 }
1198 
toStream(std::ostream & out,const CheckSatCommand * c,bool cvc3Mode)1199 static void toStream(std::ostream& out, const CheckSatCommand* c, bool cvc3Mode)
1200 {
1201   Expr e = c->getExpr();
1202   if(cvc3Mode) {
1203     out << "PUSH; ";
1204   }
1205   if(!e.isNull()) {
1206     out << "CHECKSAT " << e << ";";
1207   } else {
1208     out << "CHECKSAT;";
1209   }
1210   if(cvc3Mode) {
1211     out << " POP;";
1212   }
1213 }
1214 
toStream(std::ostream & out,const CheckSatAssumingCommand * c,bool cvc3Mode)1215 static void toStream(std::ostream& out,
1216                      const CheckSatAssumingCommand* c,
1217                      bool cvc3Mode)
1218 {
1219   const vector<Expr>& exprs = c->getTerms();
1220   if (cvc3Mode)
1221   {
1222     out << "PUSH; ";
1223   }
1224   out << "CHECKSAT";
1225   if (exprs.size() > 0)
1226   {
1227     out << " " << exprs[0];
1228     for (size_t i = 1, n = exprs.size(); i < n; ++i)
1229     {
1230       out << " AND " << exprs[i];
1231     }
1232   }
1233   out << ";";
1234   if (cvc3Mode)
1235   {
1236     out << " POP;";
1237   }
1238 }
1239 
toStream(std::ostream & out,const QueryCommand * c,bool cvc3Mode)1240 static void toStream(std::ostream& out, const QueryCommand* c, bool cvc3Mode)
1241 {
1242   Expr e = c->getExpr();
1243   if(cvc3Mode) {
1244     out << "PUSH; ";
1245   }
1246   if(!e.isNull()) {
1247     out << "QUERY " << e << ";";
1248   } else {
1249     out << "QUERY TRUE;";
1250   }
1251   if(cvc3Mode) {
1252     out << " POP;";
1253   }
1254 }
1255 
toStream(std::ostream & out,const ResetCommand * c,bool cvc3Mode)1256 static void toStream(std::ostream& out, const ResetCommand* c, bool cvc3Mode)
1257 {
1258   out << "RESET;";
1259 }
1260 
toStream(std::ostream & out,const ResetAssertionsCommand * c,bool cvc3Mode)1261 static void toStream(std::ostream& out,
1262                      const ResetAssertionsCommand* c,
1263                      bool cvc3Mode)
1264 {
1265   out << "RESET ASSERTIONS;";
1266 }
1267 
toStream(std::ostream & out,const QuitCommand * c,bool cvc3Mode)1268 static void toStream(std::ostream& out, const QuitCommand* c, bool cvc3Mode)
1269 {
1270   //out << "EXIT;";
1271 }
1272 
toStream(std::ostream & out,const CommandSequence * c,bool cvc3Mode)1273 static void toStream(std::ostream& out, const CommandSequence* c, bool cvc3Mode)
1274 {
1275   for(CommandSequence::const_iterator i = c->begin();
1276       i != c->end();
1277       ++i) {
1278     out << *i << endl;
1279   }
1280 }
1281 
toStream(std::ostream & out,const DeclarationSequence * c,bool cvc3Mode)1282 static void toStream(std::ostream& out,
1283                      const DeclarationSequence* c,
1284                      bool cvc3Mode)
1285 {
1286   DeclarationSequence::const_iterator i = c->begin();
1287   for(;;) {
1288     DeclarationDefinitionCommand* dd =
1289       static_cast<DeclarationDefinitionCommand*>(*i++);
1290     if(i != c->end()) {
1291       out << dd->getSymbol() << ", ";
1292     } else {
1293       out << *dd;
1294       break;
1295     }
1296   }
1297 }
1298 
toStream(std::ostream & out,const DeclareFunctionCommand * c,bool cvc3Mode)1299 static void toStream(std::ostream& out,
1300                      const DeclareFunctionCommand* c,
1301                      bool cvc3Mode)
1302 {
1303   out << c->getSymbol() << " : " << c->getType() << ";";
1304 }
1305 
toStream(std::ostream & out,const DefineFunctionCommand * c,bool cvc3Mode)1306 static void toStream(std::ostream& out,
1307                      const DefineFunctionCommand* c,
1308                      bool cvc3Mode)
1309 {
1310   Expr func = c->getFunction();
1311   const vector<Expr>& formals = c->getFormals();
1312   Expr formula = c->getFormula();
1313   out << func << " : " << func.getType() << " = ";
1314   if(formals.size() > 0) {
1315     out << "LAMBDA(";
1316     vector<Expr>::const_iterator i = formals.begin();
1317     while(i != formals.end()) {
1318       out << (*i) << ":" << (*i).getType();
1319       if(++i != formals.end()) {
1320         out << ", ";
1321       }
1322     }
1323     out << "): ";
1324   }
1325   out << formula << ";";
1326 }
1327 
toStream(std::ostream & out,const DeclareTypeCommand * c,bool cvc3Mode)1328 static void toStream(std::ostream& out,
1329                      const DeclareTypeCommand* c,
1330                      bool cvc3Mode)
1331 {
1332   if(c->getArity() > 0) {
1333     //TODO?
1334     out << "ERROR: Don't know how to print parameterized type declaration "
1335            "in CVC language." << endl;
1336   } else {
1337     out << c->getSymbol() << " : TYPE;";
1338   }
1339 }
1340 
toStream(std::ostream & out,const DefineTypeCommand * c,bool cvc3Mode)1341 static void toStream(std::ostream& out,
1342                      const DefineTypeCommand* c,
1343                      bool cvc3Mode)
1344 {
1345   if(c->getParameters().size() > 0) {
1346     out << "ERROR: Don't know how to print parameterized type definition "
1347            "in CVC language:" << endl << c->toString() << endl;
1348   } else {
1349     out << c->getSymbol() << " : TYPE = " << c->getType() << ";";
1350   }
1351 }
1352 
toStream(std::ostream & out,const DefineNamedFunctionCommand * c,bool cvc3Mode)1353 static void toStream(std::ostream& out,
1354                      const DefineNamedFunctionCommand* c,
1355                      bool cvc3Mode)
1356 {
1357   toStream(out, static_cast<const DefineFunctionCommand*>(c), cvc3Mode);
1358 }
1359 
toStream(std::ostream & out,const SimplifyCommand * c,bool cvc3Mode)1360 static void toStream(std::ostream& out, const SimplifyCommand* c, bool cvc3Mode)
1361 {
1362   out << "TRANSFORM " << c->getTerm() << ";";
1363 }
1364 
toStream(std::ostream & out,const GetValueCommand * c,bool cvc3Mode)1365 static void toStream(std::ostream& out, const GetValueCommand* c, bool cvc3Mode)
1366 {
1367   const vector<Expr>& terms = c->getTerms();
1368   Assert(!terms.empty());
1369   out << "GET_VALUE ";
1370   copy(terms.begin(), terms.end() - 1, ostream_iterator<Expr>(out, ";\nGET_VALUE "));
1371   out << terms.back() << ";";
1372 }
1373 
toStream(std::ostream & out,const GetModelCommand * c,bool cvc3Mode)1374 static void toStream(std::ostream& out, const GetModelCommand* c, bool cvc3Mode)
1375 {
1376   out << "COUNTERMODEL;";
1377 }
1378 
toStream(std::ostream & out,const GetAssignmentCommand * c,bool cvc3Mode)1379 static void toStream(std::ostream& out,
1380                      const GetAssignmentCommand* c,
1381                      bool cvc3Mode)
1382 {
1383   out << "% (get-assignment)";
1384 }
1385 
toStream(std::ostream & out,const GetAssertionsCommand * c,bool cvc3Mode)1386 static void toStream(std::ostream& out,
1387                      const GetAssertionsCommand* c,
1388                      bool cvc3Mode)
1389 {
1390   out << "WHERE;";
1391 }
1392 
toStream(std::ostream & out,const GetProofCommand * c,bool cvc3Mode)1393 static void toStream(std::ostream& out, const GetProofCommand* c, bool cvc3Mode)
1394 {
1395   out << "DUMP_PROOF;";
1396 }
1397 
toStream(std::ostream & out,const GetUnsatCoreCommand * c,bool cvc3Mode)1398 static void toStream(std::ostream& out,
1399                      const GetUnsatCoreCommand* c,
1400                      bool cvc3Mode)
1401 {
1402   out << "DUMP_UNSAT_CORE;";
1403 }
1404 
toStream(std::ostream & out,const SetBenchmarkStatusCommand * c,bool cvc3Mode)1405 static void toStream(std::ostream& out,
1406                      const SetBenchmarkStatusCommand* c,
1407                      bool cvc3Mode)
1408 {
1409   out << "% (set-info :status " << c->getStatus() << ")";
1410 }
1411 
toStream(std::ostream & out,const SetBenchmarkLogicCommand * c,bool cvc3Mode)1412 static void toStream(std::ostream& out,
1413                      const SetBenchmarkLogicCommand* c,
1414                      bool cvc3Mode)
1415 {
1416   out << "OPTION \"logic\" \"" << c->getLogic() << "\";";
1417 }
1418 
toStream(std::ostream & out,const SetInfoCommand * c,bool cvc3Mode)1419 static void toStream(std::ostream& out, const SetInfoCommand* c, bool cvc3Mode)
1420 {
1421   out << "% (set-info " << c->getFlag() << " ";
1422   OutputLanguage language =
1423       cvc3Mode ? language::output::LANG_CVC3 : language::output::LANG_CVC4;
1424   SExpr::toStream(out, c->getSExpr(), language);
1425   out << ")";
1426 }
1427 
toStream(std::ostream & out,const GetInfoCommand * c,bool cvc3Mode)1428 static void toStream(std::ostream& out, const GetInfoCommand* c, bool cvc3Mode)
1429 {
1430   out << "% (get-info " << c->getFlag() << ")";
1431 }
1432 
toStream(std::ostream & out,const SetOptionCommand * c,bool cvc3Mode)1433 static void toStream(std::ostream& out,
1434                      const SetOptionCommand* c,
1435                      bool cvc3Mode)
1436 {
1437   out << "OPTION \"" << c->getFlag() << "\" ";
1438   SExpr::toStream(out, c->getSExpr(), language::output::LANG_CVC4);
1439   out << ";";
1440 }
1441 
toStream(std::ostream & out,const GetOptionCommand * c,bool cvc3Mode)1442 static void toStream(std::ostream& out,
1443                      const GetOptionCommand* c,
1444                      bool cvc3Mode)
1445 {
1446   out << "% (get-option " << c->getFlag() << ")";
1447 }
1448 
toStream(std::ostream & out,const DatatypeDeclarationCommand * c,bool cvc3Mode)1449 static void toStream(std::ostream& out,
1450                      const DatatypeDeclarationCommand* c,
1451                      bool cvc3Mode)
1452 {
1453   const vector<DatatypeType>& datatypes = c->getDatatypes();
1454   //do not print tuple/datatype internal declarations
1455   if( datatypes.size()!=1 || ( !datatypes[0].getDatatype().isTuple() && !datatypes[0].getDatatype().isRecord() ) ){
1456     out << "DATATYPE" << endl;
1457     bool firstDatatype = true;
1458     for(vector<DatatypeType>::const_iterator i = datatypes.begin(),
1459           i_end = datatypes.end();
1460         i != i_end;
1461         ++i) {
1462       if(! firstDatatype) {
1463         out << ',' << endl;
1464       }
1465       const Datatype& dt = (*i).getDatatype();
1466       out << "  " << dt.getName();
1467       if(dt.isParametric()) {
1468         out << '[';
1469         for(size_t j = 0; j < dt.getNumParameters(); ++j) {
1470           if(j > 0) {
1471             out << ',';
1472           }
1473           out << dt.getParameter(j);
1474         }
1475         out << ']';
1476       }
1477       out << " = ";
1478       bool firstConstructor = true;
1479       for(Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) {
1480         if(! firstConstructor) {
1481           out << " | ";
1482         }
1483         firstConstructor = false;
1484         const DatatypeConstructor& c = *j;
1485         out << c.getName();
1486         if(c.getNumArgs() > 0) {
1487           out << '(';
1488           bool firstSelector = true;
1489           for(DatatypeConstructor::const_iterator k = c.begin(); k != c.end(); ++k) {
1490             if(! firstSelector) {
1491               out << ", ";
1492             }
1493             firstSelector = false;
1494             const DatatypeConstructorArg& selector = *k;
1495             Type t = SelectorType(selector.getType()).getRangeType();
1496             if( t.isDatatype() ){
1497               const Datatype & sdt = ((DatatypeType)t).getDatatype();
1498               out << selector.getName() << ": " << sdt.getName();
1499             }else{
1500               out << selector.getName() << ": " << t;
1501             }
1502           }
1503           out << ')';
1504         }
1505       }
1506       firstDatatype = false;
1507     }
1508     out << endl << "END;";
1509   }
1510 }
1511 
toStream(std::ostream & out,const CommentCommand * c,bool cvc3Mode)1512 static void toStream(std::ostream& out, const CommentCommand* c, bool cvc3Mode)
1513 {
1514   out << "% " << c->getComment();
1515 }
1516 
toStream(std::ostream & out,const EmptyCommand * c,bool cvc3Mode)1517 static void toStream(std::ostream& out, const EmptyCommand* c, bool cvc3Mode) {}
1518 
toStream(std::ostream & out,const EchoCommand * c,bool cvc3Mode)1519 static void toStream(std::ostream& out, const EchoCommand* c, bool cvc3Mode)
1520 {
1521   out << "ECHO \"" << c->getOutput() << "\";";
1522 }
1523 
1524 template <class T>
tryToStream(std::ostream & out,const Command * c,bool cvc3Mode)1525 static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode)
1526 {
1527   if(typeid(*c) == typeid(T)) {
1528     toStream(out, dynamic_cast<const T*>(c), cvc3Mode);
1529     return true;
1530   }
1531   return false;
1532 }
1533 
toStream(std::ostream & out,const CommandSuccess * s,bool cvc3Mode)1534 static void toStream(std::ostream& out, const CommandSuccess* s, bool cvc3Mode)
1535 {
1536   if(Command::printsuccess::getPrintSuccess(out)) {
1537     out << "OK" << endl;
1538   }
1539 }
1540 
toStream(std::ostream & out,const CommandUnsupported * s,bool cvc3Mode)1541 static void toStream(std::ostream& out,
1542                      const CommandUnsupported* s,
1543                      bool cvc3Mode)
1544 {
1545   out << "UNSUPPORTED" << endl;
1546 }
1547 
toStream(std::ostream & out,const CommandInterrupted * s,bool cvc3Mode)1548 static void toStream(std::ostream& out,
1549                      const CommandInterrupted* s,
1550                      bool cvc3Mode)
1551 {
1552   out << "INTERRUPTED" << endl;
1553 }
1554 
toStream(std::ostream & out,const CommandFailure * s,bool cvc3Mode)1555 static void toStream(std::ostream& out, const CommandFailure* s, bool cvc3Mode)
1556 {
1557   out << s->getMessage() << endl;
1558 }
1559 
1560 template <class T>
tryToStream(std::ostream & out,const CommandStatus * s,bool cvc3Mode)1561 static bool tryToStream(std::ostream& out,
1562                         const CommandStatus* s,
1563                         bool cvc3Mode)
1564 {
1565   if(typeid(*s) == typeid(T)) {
1566     toStream(out, dynamic_cast<const T*>(s), cvc3Mode);
1567     return true;
1568   }
1569   return false;
1570 }
1571 
1572 }/* CVC4::printer::cvc namespace */
1573 }/* CVC4::printer namespace */
1574 }/* CVC4 namespace */
1575