src/printer/cvc/cvc_printer.cpp

   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-2018 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
  45 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
  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
  91 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() ){
 411           toStream(out, n[0], depth, types, true);
 412           const Datatype& dt = ((DatatypeType)t.toType()).getDatatype();
 413           int sindex = dt[0].getSelectorIndexInternal( opn.toExpr() );
 414           Assert( sindex>=0 );
 415           out << '.' << sindex;
 416         }else{
 417           toStream(op, opn, depth, types, false);
 418         }
 419       }
 420       break;
 421     case kind::APPLY_TESTER: {
 422       Assert( !n.getType().isTuple() && !n.getType().isRecord() );
 423       op << "is_";
 424       unsigned cindex = Datatype::indexOf(n.getOperator().toExpr());
 425       const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
 426       toStream(op, Node::fromExpr(dt[cindex].getConstructor()), depth, types, false);
 427     }
 428       break;
 429     case kind::CONSTRUCTOR_TYPE:
 430     case kind::SELECTOR_TYPE:
 431       if(n.getNumChildren() > 1) {
 432         if(n.getNumChildren() > 2) {
 433           out << '(';
 434         }
 435         for(unsigned i = 0; i < n.getNumChildren() - 1; ++i) {
 436           if(i > 0) {
 437             out << ", ";
 438           }
 439           toStream(out, n[i], depth, types, false);
 440         }
 441         if(n.getNumChildren() > 2) {
 442           out << ')';
 443         }
 444         out << " -> ";
 445       }
 446       toStream(out, n[n.getNumChildren() - 1], depth, types, false);
 447       return;
 448     case kind::TESTER_TYPE:
 449       toStream(out, n[0], depth, types, false);
 450       out << " -> BOOLEAN";
 451       return;
 452       break;
 453     case kind::TUPLE_UPDATE:
 454       toStream(out, n[0], depth, types, true);
 455       out << " WITH ." << n.getOperator().getConst<TupleUpdate>().getIndex() << " := ";
 456       toStream(out, n[1], depth, types, true);
 457       return;
 458       break;
 459     case kind::RECORD_UPDATE:
 460       toStream(out, n[0], depth, types, true);
 461       out << " WITH ." << n.getOperator().getConst<RecordUpdate>().getField() << " := ";
 462       toStream(out, n[1], depth, types, true);
 463       return;
 464       break;
 465
 466     // ARRAYS
 467     case kind::ARRAY_TYPE:
 468       out << "ARRAY ";
 469       toStream(out, n[0], depth, types, false);
 470       out << " OF ";
 471       toStream(out, n[1], depth, types, false);
 472       return;
 473       break;
 474     case kind::SELECT:
 475       toStream(out, n[0], depth, types, true);
 476       out << '[';
 477       toStream(out, n[1], depth, types, false);
 478       out << ']';
 479       return;
 480       break;
 481     case kind::STORE: {
 482       stack<TNode> stk;
 483       stk.push(n);
 484       while(stk.top()[0].getKind() == kind::STORE) {
 485         stk.push(stk.top()[0]);
 486       }
 487       if (bracket) {
 488         out << '(';
 489       }
 490       TNode x = stk.top();
 491       toStream(out, x[0], depth, types, false);
 492       out << " WITH [";
 493       toStream(out, x[1], depth, types, false);
 494       out << "] := ";
 495       toStream(out, x[2], depth, types, false);
 496       stk.pop();
 497       while(!stk.empty()) {
 498         x = stk.top();
 499         out << ", [";
 500         toStream(out, x[1], depth, types, false);
 501         out << "] := ";
 502         toStream(out, x[2], depth, types, false);
 503         stk.pop();
 504       }
 505       if (bracket) {
 506         out << ')';
 507       }
 508       return;
 509       break;
 510     }
 511
 512     // ARITHMETIC
 513     case kind::PLUS:
 514       op << '+';
 515       opType = INFIX;
 516       break;
 517     case kind::MULT:
 518     case kind::NONLINEAR_MULT:
 519       op << '*';
 520       opType = INFIX;
 521       break;
 522     case kind::MINUS:
 523       op << '-';
 524       opType = INFIX;
 525       break;
 526     case kind::UMINUS:
 527       op << '-';
 528       opType = PREFIX;
 529       break;
 530     case kind::DIVISION:
 531     case kind::DIVISION_TOTAL:
 532       op << '/';
 533       opType = INFIX;
 534       break;
 535     case kind::INTS_DIVISION:
 536     case kind::INTS_DIVISION_TOTAL:
 537       op << "DIV";
 538       opType = INFIX;
 539       break;
 540     case kind::INTS_MODULUS:
 541     case kind::INTS_MODULUS_TOTAL:
 542       op << "MOD";
 543       opType = INFIX;
 544       break;
 545     case kind::LT:
 546       op << '<';
 547       opType = INFIX;
 548       break;
 549     case kind::LEQ:
 550       op << "<=";
 551       opType = INFIX;
 552       break;
 553     case kind::GT:
 554       op << '>';
 555       opType = INFIX;
 556       break;
 557     case kind::GEQ:
 558       op << ">=";
 559       opType = INFIX;
 560       break;
 561     case kind::POW:
 562       op << '^';
 563       opType = INFIX;
 564       break;
 565     case kind::ABS:
 566       op << "ABS";
 567       opType = PREFIX;
 568       break;
 569     case kind::IS_INTEGER:
 570       op << "IS_INTEGER";
 571       opType = PREFIX;
 572       break;
 573     case kind::TO_INTEGER:
 574       op << "FLOOR";
 575       opType = PREFIX;
 576       break;
 577     case kind::TO_REAL:
 578       if (n[0].getKind() == kind::CONST_RATIONAL)
 579       {
 580         // print the constant as a rational
 581         toStreamRational(out, n[0], true);
 582       }
 583       else
 584       {
 585         // ignore, there is no to-real in CVC language
 586         toStream(out, n[0], depth, types, false);
 587       }
 588       return;
 589     case kind::DIVISIBLE:
 590       out << "DIVISIBLE(";
 591       toStream(out, n[0], depth, types, false);
 592       out << ", " << n.getOperator().getConst<Divisible>().k << ")";
 593       return;
 594
 595     // BITVECTORS
 596     case kind::BITVECTOR_XOR:
 597       op << "BVXOR";
 598       break;
 599     case kind::BITVECTOR_NAND:
 600       op << "BVNAND";
 601       break;
 602     case kind::BITVECTOR_NOR:
 603       op << "BVNOR";
 604       break;
 605     case kind::BITVECTOR_XNOR:
 606       op << "BVXNOR";
 607       break;
 608     case kind::BITVECTOR_COMP:
 609       op << "BVCOMP";
 610       break;
 611     case kind::BITVECTOR_UDIV:
 612       op << "BVUDIV";
 613       break;
 614     case kind::BITVECTOR_UDIV_TOTAL:
 615       op << "BVUDIV_TOTAL";
 616       break;
 617     case kind::BITVECTOR_UREM:
 618       op << "BVUREM";
 619       break;
 620     case kind::BITVECTOR_UREM_TOTAL:
 621       op << "BVUREM_TOTAL";
 622       break;
 623     case kind::BITVECTOR_SDIV:
 624       op << "BVSDIV";
 625       break;
 626     case kind::BITVECTOR_SREM:
 627       op << "BVSREM";
 628       break;
 629     case kind::BITVECTOR_SMOD:
 630       op << "BVSMOD";
 631       break;
 632     case kind::BITVECTOR_SHL:
 633       op << "BVSHL";
 634       break;
 635     case kind::BITVECTOR_LSHR:
 636       op << "BVLSHR";
 637       break;
 638     case kind::BITVECTOR_ASHR:
 639       op << "BVASHR";
 640       break;
 641     case kind::BITVECTOR_ULT:
 642       op << "BVLT";
 643       break;
 644     case kind::BITVECTOR_ULE:
 645       op << "BVLE";
 646       break;
 647     case kind::BITVECTOR_UGT:
 648       op << "BVGT";
 649       break;
 650     case kind::BITVECTOR_UGE:
 651       op << "BVGE";
 652       break;
 653     case kind::BITVECTOR_SLT:
 654       op << "BVSLT";
 655       break;
 656     case kind::BITVECTOR_SLE:
 657       op << "BVSLE";
 658       break;
 659     case kind::BITVECTOR_SGT:
 660       op << "BVSGT";
 661       break;
 662     case kind::BITVECTOR_SGE:
 663       op << "BVSGE";
 664       break;
 665     case kind::BITVECTOR_NEG:
 666       op << "BVUMINUS";
 667       break;
 668     case kind::BITVECTOR_NOT:
 669       op << "~";
 670       break;
 671     case kind::BITVECTOR_AND:
 672       op << "&";
 673       opType = INFIX;
 674       break;
 675     case kind::BITVECTOR_OR:
 676       op << "|";
 677       opType = INFIX;
 678       break;
 679     case kind::BITVECTOR_CONCAT:
 680       op << "@";
 681       opType = INFIX;
 682       break;
 683     case kind::BITVECTOR_PLUS: {
 684       // This interprets a BITVECTOR_PLUS as a bvadd in SMT-LIB
 685       Assert(n.getType().isBitVector());
 686       unsigned numc = n.getNumChildren()-2;
 687       unsigned child = 0;
 688       while (child < numc) {
 689         out << "BVPLUS(";
 690         out << BitVectorType(n.getType().toType()).getSize();
 691         out << ',';
 692         toStream(out, n[child], depth, types, false);
 693         out << ',';
 694         ++child;
 695       }
 696       out << "BVPLUS(";
 697       out << BitVectorType(n.getType().toType()).getSize();
 698       out << ',';
 699       toStream(out, n[child], depth, types, false);
 700       out << ',';
 701       toStream(out, n[child + 1], depth, types, false);
 702       while (child > 0) {
 703         out << ')';
 704         --child;
 705       }
 706       out << ')';
 707       return;
 708       break;
 709     }
 710     case kind::BITVECTOR_SUB:
 711       out << "BVSUB(";
 712       Assert(n.getType().isBitVector());
 713       out << BitVectorType(n.getType().toType()).getSize();
 714       out << ',';
 715       toStream(out, n[0], depth, types, false);
 716       out << ',';
 717       toStream(out, n[1], depth, types, false);
 718       out << ')';
 719       return;
 720       break;
 721     case kind::BITVECTOR_MULT: {
 722       Assert(n.getType().isBitVector());
 723       unsigned numc = n.getNumChildren()-2;
 724       unsigned child = 0;
 725       while (child < numc) {
 726         out << "BVMULT(";
 727         out << BitVectorType(n.getType().toType()).getSize();
 728         out << ',';
 729         toStream(out, n[child], depth, types, false);
 730         out << ',';
 731         ++child;
 732         }
 733       out << "BVMULT(";
 734       out << BitVectorType(n.getType().toType()).getSize();
 735       out << ',';
 736       toStream(out, n[child], depth, types, false);
 737       out << ',';
 738       toStream(out, n[child + 1], depth, types, false);
 739       while (child > 0) {
 740         out << ')';
 741         --child;
 742       }
 743       out << ')';
 744       return;
 745       break;
 746     }
 747     case kind::BITVECTOR_EXTRACT:
 748       op << n.getOperator().getConst<BitVectorExtract>();
 749       opType = POSTFIX;
 750       break;
 751     case kind::BITVECTOR_BITOF:
 752       op << n.getOperator().getConst<BitVectorBitOf>();
 753       opType = POSTFIX;
 754       break;
 755     case kind::BITVECTOR_REPEAT:
 756       out << "BVREPEAT(";
 757       toStream(out, n[0], depth, types, false);
 758       out << ", " << n.getOperator().getConst<BitVectorRepeat>() << ')';
 759       return;
 760       break;
 761     case kind::BITVECTOR_ZERO_EXTEND:
 762       out << "BVZEROEXTEND(";
 763       toStream(out, n[0], depth, types, false);
 764       out << ", " << n.getOperator().getConst<BitVectorZeroExtend>() << ')';
 765       return;
 766       break;
 767     case kind::BITVECTOR_SIGN_EXTEND:
 768       out << "SX(";
 769       toStream(out, n[0], depth, types, false);
 770       out << ", " << BitVectorType(n.getType().toType()).getSize() << ')';
 771       return;
 772       break;
 773     case kind::BITVECTOR_ROTATE_LEFT:
 774       out << "BVROTL(";
 775       toStream(out, n[0], depth, types, false);
 776       out << ", " << n.getOperator().getConst<BitVectorRotateLeft>() << ')';
 777       return;
 778       break;
 779     case kind::BITVECTOR_ROTATE_RIGHT:
 780       out << "BVROTR(";
 781       toStream(out, n[0], depth, types, false);
 782       out << ", " << n.getOperator().getConst<BitVectorRotateRight>() << ')';
 783       return;
 784       break;
 785
 786     // SETS
 787     case kind::SET_TYPE:
 788       out << "SET OF ";
 789       toStream(out, n[0], depth, types, false);
 790       return;
 791       break;
 792     case kind::UNION:
 793       op << '|';
 794       opType = INFIX;
 795       break;
 796     case kind::INTERSECTION:
 797       op << '&';
 798       opType = INFIX;
 799       break;
 800     case kind::SETMINUS:
 801       op << '-';
 802       opType = INFIX;
 803       break;
 804     case kind::SUBSET:
 805       op << "<=";
 806       opType = INFIX;
 807       break;
 808     case kind::MEMBER:
 809       op << "IS_IN";
 810       opType = INFIX;
 811       break;
 812     case kind::COMPLEMENT:
 813       op << "~";
 814       opType = PREFIX;
 815       break;
 816     case kind::PRODUCT:
 817       op << "PRODUCT";
 818       opType = INFIX;
 819       break;
 820     case kind::JOIN:
 821       op << "JOIN";
 822       opType = INFIX;
 823       break;
 824     case kind::TRANSPOSE:
 825       op << "TRANSPOSE";
 826       opType = PREFIX;
 827       break;
 828     case kind::TCLOSURE:
 829       op << "TCLOSURE";
 830       opType = PREFIX;
 831       break;
 832     case kind::IDEN:
 833       op << "IDEN";
 834       opType = PREFIX;
 835       break;
 836     case kind::JOIN_IMAGE:
 837       op << "JOIN_IMAGE";
 838       opType = INFIX;
 839       break;
 840     case kind::SINGLETON:
 841       out << "{";
 842       toStream(out, n[0], depth, types, false);
 843       out << "}";
 844       return;
 845       break;
 846     case kind::INSERT: {
 847       if(bracket) {
 848         out << '(';
 849       }
 850       out << '{';
 851       size_t i = 0;
 852       toStream(out, n[i++], depth, types, false);
 853       for(;i+1 < n.getNumChildren(); ++i) {
 854         out << ", ";
 855         toStream(out, n[i], depth, types, false);
 856       }
 857       out << "} | ";
 858       toStream(out, n[i], depth, types, true);
 859       if(bracket) {
 860         out << ')';
 861       }
 862       return;
 863       break;
 864     }
 865     case kind::CARD: {
 866       out << "CARD(";
 867       toStream(out, n[0], depth, types, false);
 868       out << ")";
 869       return;
 870       break;
 871     }
 872
 873     // Quantifiers
 874     case kind::FORALL:
 875       out << "(FORALL";
 876       toStream(out, n[0], depth, types, false);
 877       out << " : ";
 878       toStream(out, n[1], depth, types, false);
 879       out << ')';
 880       // TODO: user patterns?
 881       return;
 882     case kind::EXISTS:
 883       out << "(EXISTS";
 884       toStream(out, n[0], depth, types, false);
 885       out << " : ";
 886       toStream(out, n[1], depth, types, false);
 887       out << ')';
 888       // TODO: user patterns?
 889       return;
 890     case kind::INST_CONSTANT:
 891       out << "INST_CONSTANT";
 892       break;
 893     case kind::BOUND_VAR_LIST:
 894       out << '(';
 895       for(size_t i = 0; i < n.getNumChildren(); ++i) {
 896         if(i > 0) {
 897           out << ", ";
 898         }
 899         toStream(out, n[i], -1, true, false); // ascribe types
 900       }
 901       out << ')';
 902       return;
 903     case kind::INST_PATTERN:
 904       out << "INST_PATTERN";
 905       break;
 906     case kind::INST_PATTERN_LIST:
 907       out << "INST_PATTERN_LIST";
 908       break;
 909
 910     // string operators
 911     case kind::STRING_CONCAT:
 912       out << "CONCAT";
 913       break;
 914     case kind::STRING_CHARAT:
 915       out << "CHARAT";
 916       break;
 917     case kind::STRING_LENGTH:
 918       out << "LENGTH";
 919       break;
 920
 921     default:
 922       Warning() << "Kind printing not implemented for the case of " << n.getKind() << endl;
 923       break;
 924   }
 925
 926   switch (opType) {
 927   case PREFIX:
 928     out << op.str();
 929     if (n.getNumChildren() > 0)
 930     {
 931       out << '(';
 932     }
 933     break;
 934   case INFIX:
 935     if (bracket) {
 936       out << '(';
 937     }
 938     break;
 939   case POSTFIX:
 940     out << '(';
 941     break;
 942   }
 943
 944   for (unsigned i = 0; i < n.getNumChildren(); ++ i) {
 945     if (i > 0) {
 946       if (opType == INFIX) {
 947         out << ' ' << op.str() << ' ';
 948       } else {
 949         out << ", ";
 950       }
 951     }
 952     toStream(out, n[i], depth, types, opType == INFIX);
 953   }
 954
 955   switch (opType) {
 956     case PREFIX:
 957       if (n.getNumChildren() > 0)
 958       {
 959         out << ')';
 960       }
 961       break;
 962     case INFIX:
 963       if (bracket) {
 964         out << ')';
 965       }
 966       break;
 967     case POSTFIX:
 968       out << ')' << op.str();
 969       break;
 970   }
 971
 972 }/* CvcPrinter::toStream(TNode) */
 973
 974 template <class T>
 975 static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode);
 976
 977 void CvcPrinter::toStream(std::ostream& out,
 978                           const Command* c,
 979                           int toDepth,
 980                           bool types,
 981                           size_t dag) const
 982 {
 983   expr::ExprSetDepth::Scope sdScope(out, toDepth);
 984   expr::ExprPrintTypes::Scope ptScope(out, types);
 985   expr::ExprDag::Scope dagScope(out, dag);
 986
 987   if(tryToStream<AssertCommand>(out, c, d_cvc3Mode) ||
 988      tryToStream<PushCommand>(out, c, d_cvc3Mode) ||
 989      tryToStream<PopCommand>(out, c, d_cvc3Mode) ||
 990      tryToStream<CheckSatCommand>(out, c, d_cvc3Mode) ||
 991      tryToStream<CheckSatAssumingCommand>(out, c, d_cvc3Mode) ||
 992      tryToStream<QueryCommand>(out, c, d_cvc3Mode) ||
 993      tryToStream<ResetCommand>(out, c, d_cvc3Mode) ||
 994      tryToStream<ResetAssertionsCommand>(out, c, d_cvc3Mode) ||
 995      tryToStream<QuitCommand>(out, c, d_cvc3Mode) ||
 996      tryToStream<DeclarationSequence>(out, c, d_cvc3Mode) ||
 997      tryToStream<CommandSequence>(out, c, d_cvc3Mode) ||
 998      tryToStream<DeclareFunctionCommand>(out, c, d_cvc3Mode) ||
 999      tryToStream<DeclareTypeCommand>(out, c, d_cvc3Mode) ||
1000      tryToStream<DefineTypeCommand>(out, c, d_cvc3Mode) ||
1001      tryToStream<DefineNamedFunctionCommand>(out, c, d_cvc3Mode) ||
1002      tryToStream<DefineFunctionCommand>(out, c, d_cvc3Mode) ||
1003      tryToStream<SimplifyCommand>(out, c, d_cvc3Mode) ||
1004      tryToStream<GetValueCommand>(out, c, d_cvc3Mode) ||
1005      tryToStream<GetModelCommand>(out, c, d_cvc3Mode) ||
1006      tryToStream<GetAssignmentCommand>(out, c, d_cvc3Mode) ||
1007      tryToStream<GetAssertionsCommand>(out, c, d_cvc3Mode) ||
1008      tryToStream<GetProofCommand>(out, c, d_cvc3Mode) ||
1009      tryToStream<GetUnsatCoreCommand>(out, c, d_cvc3Mode) ||
1010      tryToStream<SetBenchmarkStatusCommand>(out, c, d_cvc3Mode) ||
1011      tryToStream<SetBenchmarkLogicCommand>(out, c, d_cvc3Mode) ||
1012      tryToStream<SetInfoCommand>(out, c, d_cvc3Mode) ||
1013      tryToStream<GetInfoCommand>(out, c, d_cvc3Mode) ||
1014      tryToStream<SetOptionCommand>(out, c, d_cvc3Mode) ||
1015      tryToStream<GetOptionCommand>(out, c, d_cvc3Mode) ||
1016      tryToStream<DatatypeDeclarationCommand>(out, c, d_cvc3Mode) ||
1017      tryToStream<CommentCommand>(out, c, d_cvc3Mode) ||
1018      tryToStream<EmptyCommand>(out, c, d_cvc3Mode) ||
1019      tryToStream<EchoCommand>(out, c, d_cvc3Mode)) {
1020     return;
1021   }
1022
1023   out << "ERROR: don't know how to print a Command of class: "
1024       << typeid(*c).name() << endl;
1025
1026 }/* CvcPrinter::toStream(Command*) */
1027
1028 template <class T>
1029 static bool tryToStream(std::ostream& out,
1030                         const CommandStatus* s,
1031                         bool cvc3Mode);
1032
1033 void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const
1034 {
1035   if(tryToStream<CommandSuccess>(out, s, d_cvc3Mode) ||
1036      tryToStream<CommandFailure>(out, s, d_cvc3Mode) ||
1037      tryToStream<CommandUnsupported>(out, s, d_cvc3Mode) ||
1038      tryToStream<CommandInterrupted>(out, s, d_cvc3Mode)) {
1039     return;
1040   }
1041
1042   out << "ERROR: don't know how to print a CommandStatus of class: "
1043       << typeid(*s).name() << endl;
1044
1045 }/* CvcPrinter::toStream(CommandStatus*) */
1046
1047 namespace {
1048
1049 void DeclareTypeCommandToStream(std::ostream& out,
1050                                 const theory::TheoryModel& model,
1051                                 const DeclareTypeCommand& command)
1052 {
1053   TypeNode type_node = TypeNode::fromType(command.getType());
1054   const std::vector<Node>* type_reps =
1055       model.getRepSet()->getTypeRepsOrNull(type_node);
1056   if (options::modelUninterpDtEnum() && type_node.isSort()
1057       && type_reps != nullptr)
1058   {
1059     out << "DATATYPE" << std::endl;
1060     out << "  " << command.getSymbol() << " = ";
1061     for (size_t i = 0; i < type_reps->size(); i++)
1062     {
1063       if (i > 0)
1064       {
1065         out << "| ";
1066       }
1067       out << (*type_reps)[i] << " ";
1068     }
1069     out << std::endl << "END;" << std::endl;
1070   }
1071   else if (type_node.isSort() && type_reps != nullptr)
1072   {
1073     out << "% cardinality of " << type_node << " is " << type_reps->size()
1074         << std::endl;
1075     out << command << std::endl;
1076     for (Node type_rep : *type_reps)
1077     {
1078       if (type_rep.isVar())
1079       {
1080         out << type_rep << " : " << type_node << ";" << std::endl;
1081       }
1082       else
1083       {
1084         out << "% rep: " << type_rep << std::endl;
1085       }
1086     }
1087   }
1088   else
1089   {
1090     out << command << std::endl;
1091   }
1092 }
1093
1094 void DeclareFunctionCommandToStream(std::ostream& out,
1095                                     const theory::TheoryModel& model,
1096                                     const DeclareFunctionCommand& command)
1097 {
1098   Node n = Node::fromExpr(command.getFunction());
1099   if (n.getKind() == kind::SKOLEM)
1100   {
1101     // don't print out internal stuff
1102     return;
1103   }
1104   TypeNode tn = n.getType();
1105   out << n << " : ";
1106   if (tn.isFunction() || tn.isPredicate())
1107   {
1108     out << "(";
1109     for (size_t i = 0; i < tn.getNumChildren() - 1; i++)
1110     {
1111       if (i > 0)
1112       {
1113         out << ", ";
1114       }
1115       out << tn[i];
1116     }
1117     out << ") -> " << tn.getRangeType();
1118   }
1119   else
1120   {
1121     out << tn;
1122   }
1123   Node val = Node::fromExpr(model.getSmtEngine()->getValue(n.toExpr()));
1124   if (options::modelUninterpDtEnum() && val.getKind() == kind::STORE)
1125   {
1126     TypeNode type_node = val[1].getType();
1127     if (tn.isSort())
1128     {
1129       if (const std::vector<Node>* type_reps =
1130               model.getRepSet()->getTypeRepsOrNull(type_node))
1131       {
1132         Cardinality indexCard(type_reps->size());
1133         val = theory::arrays::TheoryArraysRewriter::normalizeConstant(
1134             val, indexCard);
1135       }
1136     }
1137   }
1138   out << " = " << val << ";" << std::endl;
1139 }
1140
1141 }  // namespace
1142
1143 void CvcPrinter::toStream(std::ostream& out,
1144                           const Model& model,
1145                           const Command* command) const
1146 {
1147   const auto* theory_model = dynamic_cast<const theory::TheoryModel*>(&model);
1148   AlwaysAssert(theory_model != nullptr);
1149   if (const auto* declare_type_command =
1150           dynamic_cast<const DeclareTypeCommand*>(command))
1151   {
1152     DeclareTypeCommandToStream(out, *theory_model, *declare_type_command);
1153   }
1154   else if (const auto* dfc =
1155                dynamic_cast<const DeclareFunctionCommand*>(command))
1156   {
1157     DeclareFunctionCommandToStream(out, *theory_model, *dfc);
1158   }
1159   else
1160   {
1161     out << command << std::endl;
1162   }
1163 }
1164
1165 static void toStream(std::ostream& out, const AssertCommand* c, bool cvc3Mode)
1166 {
1167   out << "ASSERT " << c->getExpr() << ";";
1168 }
1169
1170 static void toStream(std::ostream& out, const PushCommand* c, bool cvc3Mode)
1171 {
1172   out << "PUSH;";
1173 }
1174
1175 static void toStream(std::ostream& out, const PopCommand* c, bool cvc3Mode)
1176 {
1177   out << "POP;";
1178 }
1179
1180 static void toStream(std::ostream& out, const CheckSatCommand* c, bool cvc3Mode)
1181 {
1182   Expr e = c->getExpr();
1183   if(cvc3Mode) {
1184     out << "PUSH; ";
1185   }
1186   if(!e.isNull()) {
1187     out << "CHECKSAT " << e << ";";
1188   } else {
1189     out << "CHECKSAT;";
1190   }
1191   if(cvc3Mode) {
1192     out << " POP;";
1193   }
1194 }
1195
1196 static void toStream(std::ostream& out,
1197                      const CheckSatAssumingCommand* c,
1198                      bool cvc3Mode)
1199 {
1200   const vector<Expr>& exprs = c->getTerms();
1201   if (cvc3Mode)
1202   {
1203     out << "PUSH; ";
1204   }
1205   out << "CHECKSAT";
1206   if (exprs.size() > 0)
1207   {
1208     out << " " << exprs[0];
1209     for (size_t i = 1, n = exprs.size(); i < n; ++i)
1210     {
1211       out << " AND " << exprs[i];
1212     }
1213   }
1214   out << ";";
1215   if (cvc3Mode)
1216   {
1217     out << " POP;";
1218   }
1219 }
1220
1221 static void toStream(std::ostream& out, const QueryCommand* c, bool cvc3Mode)
1222 {
1223   Expr e = c->getExpr();
1224   if(cvc3Mode) {
1225     out << "PUSH; ";
1226   }
1227   if(!e.isNull()) {
1228     out << "QUERY " << e << ";";
1229   } else {
1230     out << "QUERY TRUE;";
1231   }
1232   if(cvc3Mode) {
1233     out << " POP;";
1234   }
1235 }
1236
1237 static void toStream(std::ostream& out, const ResetCommand* c, bool cvc3Mode)
1238 {
1239   out << "RESET;";
1240 }
1241
1242 static void toStream(std::ostream& out,
1243                      const ResetAssertionsCommand* c,
1244                      bool cvc3Mode)
1245 {
1246   out << "RESET ASSERTIONS;";
1247 }
1248
1249 static void toStream(std::ostream& out, const QuitCommand* c, bool cvc3Mode)
1250 {
1251   //out << "EXIT;";
1252 }
1253
1254 static void toStream(std::ostream& out, const CommandSequence* c, bool cvc3Mode)
1255 {
1256   for(CommandSequence::const_iterator i = c->begin();
1257       i != c->end();
1258       ++i) {
1259     out << *i << endl;
1260   }
1261 }
1262
1263 static void toStream(std::ostream& out,
1264                      const DeclarationSequence* c,
1265                      bool cvc3Mode)
1266 {
1267   DeclarationSequence::const_iterator i = c->begin();
1268   for(;;) {
1269     DeclarationDefinitionCommand* dd =
1270       static_cast<DeclarationDefinitionCommand*>(*i++);
1271     if(i != c->end()) {
1272       out << dd->getSymbol() << ", ";
1273     } else {
1274       out << *dd;
1275       break;
1276     }
1277   }
1278 }
1279
1280 static void toStream(std::ostream& out,
1281                      const DeclareFunctionCommand* c,
1282                      bool cvc3Mode)
1283 {
1284   out << c->getSymbol() << " : " << c->getType() << ";";
1285 }
1286
1287 static void toStream(std::ostream& out,
1288                      const DefineFunctionCommand* c,
1289                      bool cvc3Mode)
1290 {
1291   Expr func = c->getFunction();
1292   const vector<Expr>& formals = c->getFormals();
1293   Expr formula = c->getFormula();
1294   out << func << " : " << func.getType() << " = ";
1295   if(formals.size() > 0) {
1296     out << "LAMBDA(";
1297     vector<Expr>::const_iterator i = formals.begin();
1298     while(i != formals.end()) {
1299       out << (*i) << ":" << (*i).getType();
1300       if(++i != formals.end()) {
1301         out << ", ";
1302       }
1303     }
1304     out << "): ";
1305   }
1306   out << formula << ";";
1307 }
1308
1309 static void toStream(std::ostream& out,
1310                      const DeclareTypeCommand* c,
1311                      bool cvc3Mode)
1312 {
1313   if(c->getArity() > 0) {
1314     //TODO?
1315     out << "ERROR: Don't know how to print parameterized type declaration "
1316            "in CVC language." << endl;
1317   } else {
1318     out << c->getSymbol() << " : TYPE;";
1319   }
1320 }
1321
1322 static void toStream(std::ostream& out,
1323                      const DefineTypeCommand* c,
1324                      bool cvc3Mode)
1325 {
1326   if(c->getParameters().size() > 0) {
1327     out << "ERROR: Don't know how to print parameterized type definition "
1328            "in CVC language:" << endl << c->toString() << endl;
1329   } else {
1330     out << c->getSymbol() << " : TYPE = " << c->getType() << ";";
1331   }
1332 }
1333
1334 static void toStream(std::ostream& out,
1335                      const DefineNamedFunctionCommand* c,
1336                      bool cvc3Mode)
1337 {
1338   toStream(out, static_cast<const DefineFunctionCommand*>(c), cvc3Mode);
1339 }
1340
1341 static void toStream(std::ostream& out, const SimplifyCommand* c, bool cvc3Mode)
1342 {
1343   out << "TRANSFORM " << c->getTerm() << ";";
1344 }
1345
1346 static void toStream(std::ostream& out, const GetValueCommand* c, bool cvc3Mode)
1347 {
1348   const vector<Expr>& terms = c->getTerms();
1349   Assert(!terms.empty());
1350   out << "GET_VALUE ";
1351   copy(terms.begin(), terms.end() - 1, ostream_iterator<Expr>(out, ";\nGET_VALUE "));
1352   out << terms.back() << ";";
1353 }
1354
1355 static void toStream(std::ostream& out, const GetModelCommand* c, bool cvc3Mode)
1356 {
1357   out << "COUNTERMODEL;";
1358 }
1359
1360 static void toStream(std::ostream& out,
1361                      const GetAssignmentCommand* c,
1362                      bool cvc3Mode)
1363 {
1364   out << "% (get-assignment)";
1365 }
1366
1367 static void toStream(std::ostream& out,
1368                      const GetAssertionsCommand* c,
1369                      bool cvc3Mode)
1370 {
1371   out << "WHERE;";
1372 }
1373
1374 static void toStream(std::ostream& out, const GetProofCommand* c, bool cvc3Mode)
1375 {
1376   out << "DUMP_PROOF;";
1377 }
1378
1379 static void toStream(std::ostream& out,
1380                      const GetUnsatCoreCommand* c,
1381                      bool cvc3Mode)
1382 {
1383   out << "DUMP_UNSAT_CORE;";
1384 }
1385
1386 static void toStream(std::ostream& out,
1387                      const SetBenchmarkStatusCommand* c,
1388                      bool cvc3Mode)
1389 {
1390   out << "% (set-info :status " << c->getStatus() << ")";
1391 }
1392
1393 static void toStream(std::ostream& out,
1394                      const SetBenchmarkLogicCommand* c,
1395                      bool cvc3Mode)
1396 {
1397   out << "OPTION \"logic\" \"" << c->getLogic() << "\";";
1398 }
1399
1400 static void toStream(std::ostream& out, const SetInfoCommand* c, bool cvc3Mode)
1401 {
1402   out << "% (set-info " << c->getFlag() << " ";
1403   OutputLanguage language =
1404       cvc3Mode ? language::output::LANG_CVC3 : language::output::LANG_CVC4;
1405   SExpr::toStream(out, c->getSExpr(), language);
1406   out << ")";
1407 }
1408
1409 static void toStream(std::ostream& out, const GetInfoCommand* c, bool cvc3Mode)
1410 {
1411   out << "% (get-info " << c->getFlag() << ")";
1412 }
1413
1414 static void toStream(std::ostream& out,
1415                      const SetOptionCommand* c,
1416                      bool cvc3Mode)
1417 {
1418   out << "OPTION \"" << c->getFlag() << "\" ";
1419   SExpr::toStream(out, c->getSExpr(), language::output::LANG_CVC4);
1420   out << ";";
1421 }
1422
1423 static void toStream(std::ostream& out,
1424                      const GetOptionCommand* c,
1425                      bool cvc3Mode)
1426 {
1427   out << "% (get-option " << c->getFlag() << ")";
1428 }
1429
1430 static void toStream(std::ostream& out,
1431                      const DatatypeDeclarationCommand* c,
1432                      bool cvc3Mode)
1433 {
1434   const vector<DatatypeType>& datatypes = c->getDatatypes();
1435   //do not print tuple/datatype internal declarations
1436   if( datatypes.size()!=1 || ( !datatypes[0].getDatatype().isTuple() && !datatypes[0].getDatatype().isRecord() ) ){
1437     out << "DATATYPE" << endl;
1438     bool firstDatatype = true;
1439     for(vector<DatatypeType>::const_iterator i = datatypes.begin(),
1440           i_end = datatypes.end();
1441         i != i_end;
1442         ++i) {
1443       if(! firstDatatype) {
1444         out << ',' << endl;
1445       }
1446       const Datatype& dt = (*i).getDatatype();
1447       out << "  " << dt.getName();
1448       if(dt.isParametric()) {
1449         out << '[';
1450         for(size_t j = 0; j < dt.getNumParameters(); ++j) {
1451           if(j > 0) {
1452             out << ',';
1453           }
1454           out << dt.getParameter(j);
1455         }
1456         out << ']';
1457       }
1458       out << " = ";
1459       bool firstConstructor = true;
1460       for(Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) {
1461         if(! firstConstructor) {
1462           out << " | ";
1463         }
1464         firstConstructor = false;
1465         const DatatypeConstructor& c = *j;
1466         out << c.getName();
1467         if(c.getNumArgs() > 0) {
1468           out << '(';
1469           bool firstSelector = true;
1470           for(DatatypeConstructor::const_iterator k = c.begin(); k != c.end(); ++k) {
1471             if(! firstSelector) {
1472               out << ", ";
1473             }
1474             firstSelector = false;
1475             const DatatypeConstructorArg& selector = *k;
1476             Type t = SelectorType(selector.getType()).getRangeType();
1477             if( t.isDatatype() ){
1478               const Datatype & sdt = ((DatatypeType)t).getDatatype();
1479               out << selector.getName() << ": " << sdt.getName();
1480             }else{
1481               out << selector.getName() << ": " << t;
1482             }
1483           }
1484           out << ')';
1485         }
1486       }
1487       firstDatatype = false;
1488     }
1489     out << endl << "END;";
1490   }
1491 }
1492
1493 static void toStream(std::ostream& out, const CommentCommand* c, bool cvc3Mode)
1494 {
1495   out << "% " << c->getComment();
1496 }
1497
1498 static void toStream(std::ostream& out, const EmptyCommand* c, bool cvc3Mode) {}
1499
1500 static void toStream(std::ostream& out, const EchoCommand* c, bool cvc3Mode)
1501 {
1502   out << "ECHO \"" << c->getOutput() << "\";";
1503 }
1504
1505 template <class T>
1506 static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode)
1507 {
1508   if(typeid(*c) == typeid(T)) {
1509     toStream(out, dynamic_cast<const T*>(c), cvc3Mode);
1510     return true;
1511   }
1512   return false;
1513 }
1514
1515 static void toStream(std::ostream& out, const CommandSuccess* s, bool cvc3Mode)
1516 {
1517   if(Command::printsuccess::getPrintSuccess(out)) {
1518     out << "OK" << endl;
1519   }
1520 }
1521
1522 static void toStream(std::ostream& out,
1523                      const CommandUnsupported* s,
1524                      bool cvc3Mode)
1525 {
1526   out << "UNSUPPORTED" << endl;
1527 }
1528
1529 static void toStream(std::ostream& out,
1530                      const CommandInterrupted* s,
1531                      bool cvc3Mode)
1532 {
1533   out << "INTERRUPTED" << endl;
1534 }
1535
1536 static void toStream(std::ostream& out, const CommandFailure* s, bool cvc3Mode)
1537 {
1538   out << s->getMessage() << endl;
1539 }
1540
1541 template <class T>
1542 static bool tryToStream(std::ostream& out,
1543                         const CommandStatus* s,
1544                         bool cvc3Mode)
1545 {
1546   if(typeid(*s) == typeid(T)) {
1547     toStream(out, dynamic_cast<const T*>(s), cvc3Mode);
1548     return true;
1549   }
1550   return false;
1551 }
1552
1553 }/* CVC4::printer::cvc namespace */
1554 }/* CVC4::printer namespace */
1555 }/* CVC4 namespace */