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