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