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 = n.getConst<Datatype>();
 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       out << n[0].getConst<Datatype>().getName() << '[';
 338       for(unsigned i = 1; i < n.getNumChildren(); ++i) {
 339         if(i > 1) {
 340           out << ',';
 341         }
 342         out << n[i];
 343       }
 344       out << ']';
 345       return;
 346       break;
 347     case kind::APPLY_TYPE_ASCRIPTION: {
 348         toStream(out, n[0], depth, types, false);
 349         out << "::";
 350         TypeNode t = TypeNode::fromType(n.getOperator().getConst<AscriptionType>().getType());
 351         out << (t.isFunctionLike() ? t.getRangeType() : t);
 352       }
 353       return;
 354       break;
 355     case kind::APPLY_CONSTRUCTOR: {
 356         TypeNode t = n.getType();
 357         if( t.isTuple() ){
 358           if( n.getNumChildren()==1 ){
 359             out << "TUPLE";
 360           }
 361         }else if( t.isRecord() ){
 362           const Record& rec = t.getRecord();
 363           out << "(# ";
 364           TNode::iterator i = n.begin();
 365           bool first = true;
 366           const Record::FieldVector& fields = rec.getFields();
 367           for(Record::FieldVector::const_iterator j = fields.begin(); j != fields.end(); ++i, ++j) {
 368             if(!first) {
 369               out << ", ";
 370             }
 371             out << (*j).first << " := ";
 372             toStream(out, *i, depth, types, false);
 373             first = false;
 374           }
 375           out << " #)";
 376           return;
 377         }else{
 378           toStream(op, n.getOperator(), depth, types, false);
 379         }
 380       }
 381       break;
 382     case kind::APPLY_SELECTOR:
 383     case kind::APPLY_SELECTOR_TOTAL: {
 384         TypeNode t = n.getType();
 385         if( t.isTuple() ){
 386           toStream(out, n[0], depth, types, true);
 387           out << '.' << Datatype::indexOf( n.getOperator().toExpr() );
 388         }else if( t.isRecord() ){
 389           toStream(out, n[0], depth, types, true);
 390           const Record& rec = t.getRecord();
 391           unsigned index = Datatype::indexOf( n.getOperator().toExpr() );
 392           std::pair<std::string, Type> fld = rec[index];
 393           out << '.' << fld.first;
 394         }else{
 395           toStream(op, n.getOperator(), depth, types, false);
 396         }
 397       }
 398       break;
 399     case kind::APPLY_TESTER:
 400       toStream(op, n.getOperator(), depth, types, false);
 401       break;
 402     case kind::CONSTRUCTOR_TYPE:
 403     case kind::SELECTOR_TYPE:
 404       if(n.getNumChildren() > 1) {
 405         if(n.getNumChildren() > 2) {
 406           out << '(';
 407         }
 408         for(unsigned i = 0; i < n.getNumChildren() - 1; ++i) {
 409           if(i > 0) {
 410             out << ", ";
 411           }
 412           toStream(out, n[i], depth, types, false);
 413         }
 414         if(n.getNumChildren() > 2) {
 415           out << ')';
 416         }
 417         out << " -> ";
 418       }
 419       toStream(out, n[n.getNumChildren() - 1], depth, types, false);
 420       return;
 421     case kind::TESTER_TYPE:
 422       toStream(out, n[0], depth, types, false);
 423       out << " -> BOOLEAN";
 424       return;
 425       break;
 426     case kind::TUPLE_UPDATE:
 427       toStream(out, n[0], depth, types, true);
 428       out << " WITH ." << n.getOperator().getConst<TupleUpdate>().getIndex() << " := ";
 429       toStream(out, n[1], depth, types, true);
 430       return;
 431       break;
 432     case kind::RECORD_UPDATE:
 433       toStream(out, n[0], depth, types, true);
 434       out << " WITH ." << n.getOperator().getConst<RecordUpdate>().getField() << " := ";
 435       toStream(out, n[1], depth, types, true);
 436       return;
 437       break;
 438
 439     // ARRAYS
 440     case kind::ARRAY_TYPE:
 441       out << "ARRAY ";
 442       toStream(out, n[0], depth, types, false);
 443       out << " OF ";
 444       toStream(out, n[1], depth, types, false);
 445       return;
 446       break;
 447     case kind::SELECT:
 448       toStream(out, n[0], depth, types, true);
 449       out << '[';
 450       toStream(out, n[1], depth, types, false);
 451       out << ']';
 452       return;
 453       break;
 454     case kind::STORE: {
 455       stack<TNode> stk;
 456       stk.push(n);
 457       while(stk.top()[0].getKind() == kind::STORE) {
 458         stk.push(stk.top()[0]);
 459       }
 460       if (bracket) {
 461         out << '(';
 462       }
 463       TNode x = stk.top();
 464       toStream(out, x[0], depth, types, false);
 465       out << " WITH [";
 466       toStream(out, x[1], depth, types, false);
 467       out << "] := ";
 468       toStream(out, x[2], depth, types, false);
 469       stk.pop();
 470       while(!stk.empty()) {
 471         x = stk.top();
 472         out << ", [";
 473         toStream(out, x[1], depth, types, false);
 474         out << "] := ";
 475         toStream(out, x[2], depth, types, false);
 476         stk.pop();
 477       }
 478       if (bracket) {
 479         out << ')';
 480       }
 481       return;
 482       break;
 483     }
 484
 485     // ARITHMETIC
 486     case kind::PLUS:
 487       op << '+';
 488       opType = INFIX;
 489       break;
 490     case kind::MULT:
 491       op << '*';
 492       opType = INFIX;
 493       break;
 494     case kind::MINUS:
 495       op << '-';
 496       opType = INFIX;
 497       break;
 498     case kind::UMINUS:
 499       op << '-';
 500       opType = PREFIX;
 501       break;
 502     case kind::DIVISION:
 503       op << '/';
 504       opType = INFIX;
 505       break;
 506     case kind::INTS_DIVISION:
 507       op << "DIV";
 508       opType = INFIX;
 509       break;
 510     case kind::INTS_MODULUS:
 511       op << "MOD";
 512       opType = INFIX;
 513       break;
 514     case kind::LT:
 515       op << '<';
 516       opType = INFIX;
 517       break;
 518     case kind::LEQ:
 519       op << "<=";
 520       opType = INFIX;
 521       break;
 522     case kind::GT:
 523       op << '>';
 524       opType = INFIX;
 525       break;
 526     case kind::GEQ:
 527       op << ">=";
 528       opType = INFIX;
 529       break;
 530     case kind::POW:
 531       op << '^';
 532       opType = INFIX;
 533       break;
 534     case kind::ABS:
 535       op << "ABS";
 536       opType = PREFIX;
 537       break;
 538     case kind::IS_INTEGER:
 539       op << "IS_INTEGER";
 540       opType = PREFIX;
 541       break;
 542     case kind::TO_INTEGER:
 543       op << "FLOOR";
 544       opType = PREFIX;
 545       break;
 546     case kind::TO_REAL:
 547       // ignore, there is no to-real in CVC language
 548       toStream(out, n[0], depth, types, false);
 549       return;
 550     case kind::DIVISIBLE:
 551       out << "DIVISIBLE(";
 552       toStream(out, n[0], depth, types, false);
 553       out << ", " << n.getOperator().getConst<Divisible>().k << ")";
 554       return;
 555
 556     // BITVECTORS
 557     case kind::BITVECTOR_XOR:
 558       op << "BVXOR";
 559       break;
 560     case kind::BITVECTOR_NAND:
 561       op << "BVNAND";
 562       break;
 563     case kind::BITVECTOR_NOR:
 564       op << "BVNOR";
 565       break;
 566     case kind::BITVECTOR_XNOR:
 567       op << "BVXNOR";
 568       break;
 569     case kind::BITVECTOR_COMP:
 570       op << "BVCOMP";
 571       break;
 572     case kind::BITVECTOR_UDIV:
 573       op << "BVUDIV";
 574       break;
 575     case kind::BITVECTOR_UDIV_TOTAL:
 576       op << "BVUDIV_TOTAL";
 577       break;
 578     case kind::BITVECTOR_UREM:
 579       op << "BVUREM";
 580       break;
 581     case kind::BITVECTOR_UREM_TOTAL:
 582       op << "BVUREM_TOTAL";
 583       break;
 584     case kind::BITVECTOR_SDIV:
 585       op << "BVSDIV";
 586       break;
 587     case kind::BITVECTOR_SREM:
 588       op << "BVSREM";
 589       break;
 590     case kind::BITVECTOR_SMOD:
 591       op << "BVSMOD";
 592       break;
 593     case kind::BITVECTOR_SHL:
 594       op << "BVSHL";
 595       break;
 596     case kind::BITVECTOR_LSHR:
 597       op << "BVLSHR";
 598       break;
 599     case kind::BITVECTOR_ASHR:
 600       op << "BVASHR";
 601       break;
 602     case kind::BITVECTOR_ULT:
 603       op << "BVLT";
 604       break;
 605     case kind::BITVECTOR_ULE:
 606       op << "BVLE";
 607       break;
 608     case kind::BITVECTOR_UGT:
 609       op << "BVGT";
 610       break;
 611     case kind::BITVECTOR_UGE:
 612       op << "BVGE";
 613       break;
 614     case kind::BITVECTOR_SLT:
 615       op << "BVSLT";
 616       break;
 617     case kind::BITVECTOR_SLE:
 618       op << "BVSLE";
 619       break;
 620     case kind::BITVECTOR_SGT:
 621       op << "BVSGT";
 622       break;
 623     case kind::BITVECTOR_SGE:
 624       op << "BVSGE";
 625       break;
 626     case kind::BITVECTOR_NEG:
 627       op << "BVUMINUS";
 628       break;
 629     case kind::BITVECTOR_NOT:
 630       op << "~";
 631       break;
 632     case kind::BITVECTOR_AND:
 633       op << "&";
 634       opType = INFIX;
 635       break;
 636     case kind::BITVECTOR_OR:
 637       op << "|";
 638       opType = INFIX;
 639       break;
 640     case kind::BITVECTOR_CONCAT:
 641       op << "@";
 642       opType = INFIX;
 643       break;
 644     case kind::BITVECTOR_PLUS: {
 645       // This interprets a BITVECTOR_PLUS as a bvadd in SMT-LIB
 646       Assert(n.getType().isBitVector());
 647       unsigned numc = n.getNumChildren()-2;
 648       unsigned child = 0;
 649       while (child < numc) {
 650         out << "BVPLUS(";
 651         out << BitVectorType(n.getType().toType()).getSize();
 652         out << ',';
 653         toStream(out, n[child], depth, types, false);
 654         out << ',';
 655         ++child;
 656       }
 657       out << "BVPLUS(";
 658       out << BitVectorType(n.getType().toType()).getSize();
 659       out << ',';
 660       toStream(out, n[child], depth, types, false);
 661       out << ',';
 662       toStream(out, n[child + 1], depth, types, false);
 663       while (child > 0) {
 664         out << ')';
 665         --child;
 666       }
 667       out << ')';
 668       return;
 669       break;
 670     }
 671     case kind::BITVECTOR_SUB:
 672       out << "BVSUB(";
 673       Assert(n.getType().isBitVector());
 674       out << BitVectorType(n.getType().toType()).getSize();
 675       out << ',';
 676       toStream(out, n[0], depth, types, false);
 677       out << ',';
 678       toStream(out, n[1], depth, types, false);
 679       out << ')';
 680       return;
 681       break;
 682     case kind::BITVECTOR_MULT: {
 683       Assert(n.getType().isBitVector());
 684       unsigned numc = n.getNumChildren()-2;
 685       unsigned child = 0;
 686       while (child < numc) {
 687         out << "BVMULT(";
 688         out << BitVectorType(n.getType().toType()).getSize();
 689         out << ',';
 690         toStream(out, n[child], depth, types, false);
 691         out << ',';
 692         ++child;
 693         }
 694       out << "BVMULT(";
 695       out << BitVectorType(n.getType().toType()).getSize();
 696       out << ',';
 697       toStream(out, n[child], depth, types, false);
 698       out << ',';
 699       toStream(out, n[child + 1], depth, types, false);
 700       while (child > 0) {
 701         out << ')';
 702         --child;
 703       }
 704       out << ')';
 705       return;
 706       break;
 707     }
 708     case kind::BITVECTOR_EXTRACT:
 709       op << n.getOperator().getConst<BitVectorExtract>();
 710       opType = POSTFIX;
 711       break;
 712     case kind::BITVECTOR_BITOF:
 713       op << n.getOperator().getConst<BitVectorBitOf>();
 714       opType = POSTFIX;
 715       break;
 716     case kind::BITVECTOR_REPEAT:
 717       out << "BVREPEAT(";
 718       toStream(out, n[0], depth, types, false);
 719       out << ", " << n.getOperator().getConst<BitVectorRepeat>() << ')';
 720       return;
 721       break;
 722     case kind::BITVECTOR_ZERO_EXTEND:
 723       out << "BVZEROEXTEND(";
 724       toStream(out, n[0], depth, types, false);
 725       out << ", " << n.getOperator().getConst<BitVectorZeroExtend>() << ')';
 726       return;
 727       break;
 728     case kind::BITVECTOR_SIGN_EXTEND:
 729       out << "SX(";
 730       toStream(out, n[0], depth, types, false);
 731       out << ", " << BitVectorType(n.getType().toType()).getSize() << ')';
 732       return;
 733       break;
 734     case kind::BITVECTOR_ROTATE_LEFT:
 735       out << "BVROTL(";
 736       toStream(out, n[0], depth, types, false);
 737       out << ", " << n.getOperator().getConst<BitVectorRotateLeft>() << ')';
 738       return;
 739       break;
 740     case kind::BITVECTOR_ROTATE_RIGHT:
 741       out << "BVROTR(";
 742       toStream(out, n[0], depth, types, false);
 743       out << ", " << n.getOperator().getConst<BitVectorRotateRight>() << ')';
 744       return;
 745       break;
 746
 747     // SETS
 748     case kind::SET_TYPE:
 749       out << "SET OF ";
 750       toStream(out, n[0], depth, types, false);
 751       return;
 752       break;
 753     case kind::UNION:
 754       op << '|';
 755       opType = INFIX;
 756       break;
 757     case kind::INTERSECTION:
 758       op << '&';
 759       opType = INFIX;
 760       break;
 761     case kind::SETMINUS:
 762       op << '-';
 763       opType = INFIX;
 764       break;
 765     case kind::SUBSET:
 766       op << "<=";
 767       opType = INFIX;
 768       break;
 769     case kind::MEMBER:
 770       op << "IS_IN";
 771       opType = INFIX;
 772       break;
 773     case kind::PRODUCT:
 774       op << "PRODUCT";
 775       opType = INFIX;
 776       break;
 777     case kind::JOIN:
 778       op << "JOIN";
 779       opType = INFIX;
 780       break;
 781     case kind::TRANSPOSE:
 782       op << "TRANSPOSE";
 783       opType = PREFIX;
 784       break;
 785     case kind::TCLOSURE:
 786       op << "TCLOSURE";
 787       opType = PREFIX;
 788       break;
 789     case kind::SINGLETON:
 790       out << "{";
 791       toStream(out, n[0], depth, types, false);
 792       out << "}";
 793       return;
 794       break;
 795     case kind::INSERT: {
 796       if(bracket) {
 797         out << '(';
 798       }
 799       out << '{';
 800       size_t i = 0;
 801       toStream(out, n[i++], depth, types, false);
 802       for(;i+1 < n.getNumChildren(); ++i) {
 803         out << ", ";
 804         toStream(out, n[i], depth, types, false);
 805       }
 806       out << "} | ";
 807       toStream(out, n[i], depth, types, true);
 808       if(bracket) {
 809         out << ')';
 810       }
 811       return;
 812       break;
 813     }
 814     case kind::CARD: {
 815       out << "||";
 816       toStream(out, n[0], depth, types, false);
 817       out << "||";
 818       return;
 819       break;
 820     }
 821
 822     // Quantifiers
 823     case kind::FORALL:
 824       out << "(FORALL";
 825       toStream(out, n[0], depth, types, false);
 826       out << " : ";
 827       toStream(out, n[1], depth, types, false);
 828       out << ')';
 829       // TODO: user patterns?
 830       return;
 831     case kind::EXISTS:
 832       out << "(EXISTS";
 833       toStream(out, n[0], depth, types, false);
 834       out << " : ";
 835       toStream(out, n[1], depth, types, false);
 836       out << ')';
 837       // TODO: user patterns?
 838       return;
 839     case kind::INST_CONSTANT:
 840       out << "INST_CONSTANT";
 841       break;
 842     case kind::BOUND_VAR_LIST:
 843       out << '(';
 844       for(size_t i = 0; i < n.getNumChildren(); ++i) {
 845         if(i > 0) {
 846           out << ", ";
 847         }
 848         toStream(out, n[i], -1, true, false); // ascribe types
 849       }
 850       out << ')';
 851       return;
 852     case kind::INST_PATTERN:
 853       out << "INST_PATTERN";
 854       break;
 855     case kind::INST_PATTERN_LIST:
 856       out << "INST_PATTERN_LIST";
 857       break;
 858
 859     default:
 860       Warning() << "Kind printing not implemented for the case of " << n.getKind() << endl;
 861       break;
 862   }
 863
 864   switch (opType) {
 865   case PREFIX:
 866     out << op.str() << '(';
 867     break;
 868   case INFIX:
 869     if (bracket) {
 870       out << '(';
 871     }
 872     break;
 873   case POSTFIX:
 874     out << '(';
 875     break;
 876   }
 877
 878   for (unsigned i = 0; i < n.getNumChildren(); ++ i) {
 879     if (i > 0) {
 880       if (opType == INFIX) {
 881         out << ' ' << op.str() << ' ';
 882       } else {
 883         out << ", ";
 884       }
 885     }
 886     toStream(out, n[i], depth, types, opType == INFIX);
 887   }
 888
 889   switch (opType) {
 890     case PREFIX:
 891       out << ')';
 892       break;
 893     case INFIX:
 894       if (bracket) {
 895         out << ')';
 896       }
 897       break;
 898     case POSTFIX:
 899       out << ')' << op.str();
 900       break;
 901   }
 902
 903 }/* CvcPrinter::toStream(TNode) */
 904
 905 template <class T>
 906 static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode) throw();
 907
 908 void CvcPrinter::toStream(std::ostream& out, const Command* c,
 909                            int toDepth, bool types, size_t dag) const throw() {
 910   expr::ExprSetDepth::Scope sdScope(out, toDepth);
 911   expr::ExprPrintTypes::Scope ptScope(out, types);
 912   expr::ExprDag::Scope dagScope(out, dag);
 913
 914   if(tryToStream<AssertCommand>(out, c, d_cvc3Mode) ||
 915      tryToStream<PushCommand>(out, c, d_cvc3Mode) ||
 916      tryToStream<PopCommand>(out, c, d_cvc3Mode) ||
 917      tryToStream<CheckSatCommand>(out, c, d_cvc3Mode) ||
 918      tryToStream<QueryCommand>(out, c, d_cvc3Mode) ||
 919      tryToStream<ResetCommand>(out, c, d_cvc3Mode) ||
 920      tryToStream<ResetAssertionsCommand>(out, c, d_cvc3Mode) ||
 921      tryToStream<QuitCommand>(out, c, d_cvc3Mode) ||
 922      tryToStream<DeclarationSequence>(out, c, d_cvc3Mode) ||
 923      tryToStream<CommandSequence>(out, c, d_cvc3Mode) ||
 924      tryToStream<DeclareFunctionCommand>(out, c, d_cvc3Mode) ||
 925      tryToStream<DeclareTypeCommand>(out, c, d_cvc3Mode) ||
 926      tryToStream<DefineTypeCommand>(out, c, d_cvc3Mode) ||
 927      tryToStream<DefineNamedFunctionCommand>(out, c, d_cvc3Mode) ||
 928      tryToStream<DefineFunctionCommand>(out, c, d_cvc3Mode) ||
 929      tryToStream<SimplifyCommand>(out, c, d_cvc3Mode) ||
 930      tryToStream<GetValueCommand>(out, c, d_cvc3Mode) ||
 931      tryToStream<GetModelCommand>(out, c, d_cvc3Mode) ||
 932      tryToStream<GetAssignmentCommand>(out, c, d_cvc3Mode) ||
 933      tryToStream<GetAssertionsCommand>(out, c, d_cvc3Mode) ||
 934      tryToStream<GetProofCommand>(out, c, d_cvc3Mode) ||
 935      tryToStream<GetUnsatCoreCommand>(out, c, d_cvc3Mode) ||
 936      tryToStream<SetBenchmarkStatusCommand>(out, c, d_cvc3Mode) ||
 937      tryToStream<SetBenchmarkLogicCommand>(out, c, d_cvc3Mode) ||
 938      tryToStream<SetInfoCommand>(out, c, d_cvc3Mode) ||
 939      tryToStream<GetInfoCommand>(out, c, d_cvc3Mode) ||
 940      tryToStream<SetOptionCommand>(out, c, d_cvc3Mode) ||
 941      tryToStream<GetOptionCommand>(out, c, d_cvc3Mode) ||
 942      tryToStream<DatatypeDeclarationCommand>(out, c, d_cvc3Mode) ||
 943      tryToStream<CommentCommand>(out, c, d_cvc3Mode) ||
 944      tryToStream<EmptyCommand>(out, c, d_cvc3Mode) ||
 945      tryToStream<EchoCommand>(out, c, d_cvc3Mode)) {
 946     return;
 947   }
 948
 949   out << "ERROR: don't know how to print a Command of class: "
 950       << typeid(*c).name() << endl;
 951
 952 }/* CvcPrinter::toStream(Command*) */
 953
 954 template <class T>
 955 static bool tryToStream(std::ostream& out, const CommandStatus* s, bool cvc3Mode) throw();
 956
 957 void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() {
 958
 959   if(tryToStream<CommandSuccess>(out, s, d_cvc3Mode) ||
 960      tryToStream<CommandFailure>(out, s, d_cvc3Mode) ||
 961      tryToStream<CommandUnsupported>(out, s, d_cvc3Mode) ||
 962      tryToStream<CommandInterrupted>(out, s, d_cvc3Mode)) {
 963     return;
 964   }
 965
 966   out << "ERROR: don't know how to print a CommandStatus of class: "
 967       << typeid(*s).name() << endl;
 968
 969 }/* CvcPrinter::toStream(CommandStatus*) */
 970
 971 void CvcPrinter::toStream(std::ostream& out, const Model& m, const Command* c) const throw() {
 972   const theory::TheoryModel& tm = (const theory::TheoryModel&) m;
 973   if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) {
 974     TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
 975     if( options::modelUninterpDtEnum() && tn.isSort() &&
 976         tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
 977       out << "DATATYPE" << std::endl;
 978       out << "  " << dynamic_cast<const DeclareTypeCommand*>(c)->getSymbol() << " = ";
 979       for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
 980         if (i>0) {
 981           out << "| ";
 982         }
 983         out << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << " ";
 984       }
 985       out << std::endl << "END;" << std::endl;
 986     } else {
 987       if( tn.isSort() ){
 988         // print the cardinality
 989         if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
 990           out << "% cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << std::endl;
 991         }
 992       }
 993       out << c << std::endl;
 994       if( tn.isSort() ){
 995         // print the representatives
 996         if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
 997           for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
 998             if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){
 999               out << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << " : " << tn << ";" << std::endl;
1000             }else{
1001               out << "% rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << std::endl;
1002             }
1003           }
1004         }
1005       }
1006     }
1007   } else if(dynamic_cast<const DeclareFunctionCommand*>(c) != NULL) {
1008     Node n = Node::fromExpr( ((const DeclareFunctionCommand*)c)->getFunction() );
1009     if(n.getKind() == kind::SKOLEM) {
1010       // don't print out internal stuff
1011       return;
1012     }
1013     TypeNode tn = n.getType();
1014     out << n << " : ";
1015     if( tn.isFunction() || tn.isPredicate() ){
1016       out << "(";
1017       for( size_t i=0; i<tn.getNumChildren()-1; i++ ){
1018         if( i>0 ) out << ", ";
1019         out << tn[i];
1020       }
1021       out << ") -> " << tn.getRangeType();
1022     }else{
1023       out << tn;
1024     }
1025     Node val = Node::fromExpr(tm.getSmtEngine()->getValue(n.toExpr()));
1026     if( options::modelUninterpDtEnum() && val.getKind() == kind::STORE ) {
1027       TypeNode tn = val[1].getType();
1028       if (tn.isSort() && tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
1029         Cardinality indexCard((*tm.d_rep_set.d_type_reps.find(tn)).second.size());
1030         val = theory::arrays::TheoryArraysRewriter::normalizeConstant( val, indexCard );
1031       }
1032     }
1033     out << " = " << val << ";" << std::endl;
1034
1035 /*
1036     //for table format (work in progress)
1037     bool printedModel = false;
1038     if( tn.isFunction() ){
1039       if( options::modelFormatMode()==MODEL_FORMAT_MODE_TABLE ){
1040         //specialized table format for functions
1041         RepSetIterator riter( &d_rep_set );
1042         riter.setFunctionDomain( n );
1043         while( !riter.isFinished() ){
1044           std::vector< Node > children;
1045           children.push_back( n );
1046           for( int i=0; i<riter.getNumTerms(); i++ ){
1047             children.push_back( riter.getTerm( i ) );
1048           }
1049           Node nn = NodeManager::currentNM()->mkNode( APPLY_UF, children );
1050           Node val = getValue( nn );
1051           out << val << " ";
1052           riter.increment();
1053         }
1054         printedModel = true;
1055       }
1056     }
1057 */
1058   }else{
1059     out << c << std::endl;
1060   }
1061 }
1062
1063 static void toStream(std::ostream& out, const AssertCommand* c, bool cvc3Mode) throw() {
1064   out << "ASSERT " << c->getExpr() << ";";
1065 }
1066
1067 static void toStream(std::ostream& out, const PushCommand* c, bool cvc3Mode) throw() {
1068   out << "PUSH;";
1069 }
1070
1071 static void toStream(std::ostream& out, const PopCommand* c, bool cvc3Mode) throw() {
1072   out << "POP;";
1073 }
1074
1075 static void toStream(std::ostream& out, const CheckSatCommand* c, bool cvc3Mode) throw() {
1076   Expr e = c->getExpr();
1077   if(cvc3Mode) {
1078     out << "PUSH; ";
1079   }
1080   if(!e.isNull()) {
1081     out << "CHECKSAT " << e << ";";
1082   } else {
1083     out << "CHECKSAT;";
1084   }
1085   if(cvc3Mode) {
1086     out << " POP;";
1087   }
1088 }
1089
1090 static void toStream(std::ostream& out, const QueryCommand* c, bool cvc3Mode) throw() {
1091   Expr e = c->getExpr();
1092   if(cvc3Mode) {
1093     out << "PUSH; ";
1094   }
1095   if(!e.isNull()) {
1096     out << "QUERY " << e << ";";
1097   } else {
1098     out << "QUERY TRUE;";
1099   }
1100   if(cvc3Mode) {
1101     out << " POP;";
1102   }
1103 }
1104
1105 static void toStream(std::ostream& out, const ResetCommand* c, bool cvc3Mode) throw() {
1106   out << "RESET;";
1107 }
1108
1109 static void toStream(std::ostream& out, const ResetAssertionsCommand* c, bool cvc3Mode) throw() {
1110   out << "RESET ASSERTIONS;";
1111 }
1112
1113 static void toStream(std::ostream& out, const QuitCommand* c, bool cvc3Mode) throw() {
1114   //out << "EXIT;";
1115 }
1116
1117 static void toStream(std::ostream& out, const CommandSequence* c, bool cvc3Mode) throw() {
1118   for(CommandSequence::const_iterator i = c->begin();
1119       i != c->end();
1120       ++i) {
1121     out << *i << endl;
1122   }
1123 }
1124
1125 static void toStream(std::ostream& out, const DeclarationSequence* c, bool cvc3Mode) throw() {
1126   DeclarationSequence::const_iterator i = c->begin();
1127   for(;;) {
1128     DeclarationDefinitionCommand* dd =
1129       static_cast<DeclarationDefinitionCommand*>(*i++);
1130     if(i != c->end()) {
1131       out << dd->getSymbol() << ", ";
1132     } else {
1133       out << *dd;
1134       break;
1135     }
1136   }
1137 }
1138
1139 static void toStream(std::ostream& out, const DeclareFunctionCommand* c, bool cvc3Mode) throw() {
1140   out << c->getSymbol() << " : " << c->getType() << ";";
1141 }
1142
1143 static void toStream(std::ostream& out, const DefineFunctionCommand* c, bool cvc3Mode) throw() {
1144   Expr func = c->getFunction();
1145   const vector<Expr>& formals = c->getFormals();
1146   Expr formula = c->getFormula();
1147   out << func << " : " << func.getType() << " = ";
1148   if(formals.size() > 0) {
1149     out << "LAMBDA(";
1150     vector<Expr>::const_iterator i = formals.begin();
1151     while(i != formals.end()) {
1152       out << (*i) << ":" << (*i).getType();
1153       if(++i != formals.end()) {
1154         out << ", ";
1155       }
1156     }
1157     out << "): ";
1158   }
1159   out << formula << ";";
1160 }
1161
1162 static void toStream(std::ostream& out, const DeclareTypeCommand* c, bool cvc3Mode) throw() {
1163   if(c->getArity() > 0) {
1164     //TODO?
1165     out << "ERROR: Don't know how to print parameterized type declaration "
1166            "in CVC language." << endl;
1167   } else {
1168     out << c->getSymbol() << " : TYPE;";
1169   }
1170 }
1171
1172 static void toStream(std::ostream& out, const DefineTypeCommand* c, bool cvc3Mode) throw() {
1173   if(c->getParameters().size() > 0) {
1174     out << "ERROR: Don't know how to print parameterized type definition "
1175            "in CVC language:" << endl << c->toString() << endl;
1176   } else {
1177     out << c->getSymbol() << " : TYPE = " << c->getType() << ";";
1178   }
1179 }
1180
1181 static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c, bool cvc3Mode) throw() {
1182   toStream(out, static_cast<const DefineFunctionCommand*>(c), cvc3Mode);
1183 }
1184
1185 static void toStream(std::ostream& out, const SimplifyCommand* c, bool cvc3Mode) throw() {
1186   out << "TRANSFORM " << c->getTerm() << ";";
1187 }
1188
1189 static void toStream(std::ostream& out, const GetValueCommand* c, bool cvc3Mode) throw() {
1190   const vector<Expr>& terms = c->getTerms();
1191   Assert(!terms.empty());
1192   out << "GET_VALUE ";
1193   copy(terms.begin(), terms.end() - 1, ostream_iterator<Expr>(out, ";\nGET_VALUE "));
1194   out << terms.back() << ";";
1195 }
1196
1197 static void toStream(std::ostream& out, const GetModelCommand* c, bool cvc3Mode) throw() {
1198   out << "COUNTERMODEL;";
1199 }
1200
1201 static void toStream(std::ostream& out, const GetAssignmentCommand* c, bool cvc3Mode) throw() {
1202   out << "% (get-assignment)";
1203 }
1204
1205 static void toStream(std::ostream& out, const GetAssertionsCommand* c, bool cvc3Mode) throw() {
1206   out << "WHERE;";
1207 }
1208
1209 static void toStream(std::ostream& out, const GetProofCommand* c, bool cvc3Mode) throw() {
1210   out << "DUMP_PROOF;";
1211 }
1212
1213 static void toStream(std::ostream& out, const GetUnsatCoreCommand* c, bool cvc3Mode) throw() {
1214   out << "DUMP_UNSAT_CORE;";
1215 }
1216
1217 static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c, bool cvc3Mode) throw() {
1218   out << "% (set-info :status " << c->getStatus() << ")";
1219 }
1220
1221 static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c, bool cvc3Mode) throw() {
1222   out << "OPTION \"logic\" \"" << c->getLogic() << "\";";
1223 }
1224
1225 static void toStream(std::ostream& out, const SetInfoCommand* c, bool cvc3Mode) throw() {
1226   out << "% (set-info " << c->getFlag() << " ";
1227   OutputLanguage language =
1228       cvc3Mode ? language::output::LANG_CVC3 : language::output::LANG_CVC4;
1229   SExpr::toStream(out, c->getSExpr(), language);
1230   out << ")";
1231 }
1232
1233 static void toStream(std::ostream& out, const GetInfoCommand* c, bool cvc3Mode) throw() {
1234   out << "% (get-info " << c->getFlag() << ")";
1235 }
1236
1237 static void toStream(std::ostream& out, const SetOptionCommand* c, bool cvc3Mode) throw() {
1238   out << "OPTION \"" << c->getFlag() << "\" ";
1239   SExpr::toStream(out, c->getSExpr(), language::output::LANG_CVC4);
1240   out << ";";
1241 }
1242
1243 static void toStream(std::ostream& out, const GetOptionCommand* c, bool cvc3Mode) throw() {
1244   out << "% (get-option " << c->getFlag() << ")";
1245 }
1246
1247 static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c, bool cvc3Mode) throw() {
1248   const vector<DatatypeType>& datatypes = c->getDatatypes();
1249   out << "DATATYPE" << endl;
1250   bool firstDatatype = true;
1251   for(vector<DatatypeType>::const_iterator i = datatypes.begin(),
1252         i_end = datatypes.end();
1253       i != i_end;
1254       ++i) {
1255     if(! firstDatatype) {
1256       out << ',' << endl;
1257     }
1258     const Datatype& dt = (*i).getDatatype();
1259     out << "  " << dt.getName();
1260     if(dt.isParametric()) {
1261       out << '[';
1262       for(size_t j = 0; j < dt.getNumParameters(); ++j) {
1263         if(j > 0) {
1264           out << ',';
1265         }
1266         out << dt.getParameter(j);
1267       }
1268       out << ']';
1269     }
1270     out << " = ";
1271     bool firstConstructor = true;
1272     for(Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) {
1273       if(! firstConstructor) {
1274         out << " | ";
1275       }
1276       firstConstructor = false;
1277       const DatatypeConstructor& c = *j;
1278       out << c.getName();
1279       if(c.getNumArgs() > 0) {
1280         out << '(';
1281         bool firstSelector = true;
1282         for(DatatypeConstructor::const_iterator k = c.begin(); k != c.end(); ++k) {
1283           if(! firstSelector) {
1284             out << ", ";
1285           }
1286           firstSelector = false;
1287           const DatatypeConstructorArg& selector = *k;
1288           Type t = SelectorType(selector.getType()).getRangeType();
1289           if( t.isDatatype() ){
1290             const Datatype & sdt = ((DatatypeType)t).getDatatype();
1291             out << selector.getName() << ": " << sdt.getName();
1292           }else{
1293             out << selector.getName() << ": " << t;
1294           }
1295         }
1296         out << ')';
1297       }
1298     }
1299   }
1300   out << endl << "END;";
1301 }
1302
1303 static void toStream(std::ostream& out, const CommentCommand* c, bool cvc3Mode) throw() {
1304   out << "% " << c->getComment();
1305 }
1306
1307 static void toStream(std::ostream& out, const EmptyCommand* c, bool cvc3Mode) throw() {
1308 }
1309
1310 static void toStream(std::ostream& out, const EchoCommand* c, bool cvc3Mode) throw() {
1311   out << "ECHO \"" << c->getOutput() << "\";";
1312 }
1313
1314 template <class T>
1315 static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode) throw() {
1316   if(typeid(*c) == typeid(T)) {
1317     toStream(out, dynamic_cast<const T*>(c), cvc3Mode);
1318     return true;
1319   }
1320   return false;
1321 }
1322
1323 static void toStream(std::ostream& out, const CommandSuccess* s, bool cvc3Mode) throw() {
1324   if(Command::printsuccess::getPrintSuccess(out)) {
1325     out << "OK" << endl;
1326   }
1327 }
1328
1329 static void toStream(std::ostream& out, const CommandUnsupported* s, bool cvc3Mode) throw() {
1330   out << "UNSUPPORTED" << endl;
1331 }
1332
1333 static void toStream(std::ostream& out, const CommandInterrupted* s, bool cvc3Mode) throw() {
1334   out << "INTERRUPTED" << endl;
1335 }
1336
1337 static void toStream(std::ostream& out, const CommandFailure* s, bool cvc3Mode) throw() {
1338   out << s->getMessage() << endl;
1339 }
1340
1341 template <class T>
1342 static bool tryToStream(std::ostream& out, const CommandStatus* s, bool cvc3Mode) throw() {
1343   if(typeid(*s) == typeid(T)) {
1344     toStream(out, dynamic_cast<const T*>(s), cvc3Mode);
1345     return true;
1346   }
1347   return false;
1348 }
1349
1350 }/* CVC4::printer::cvc namespace */
1351 }/* CVC4::printer namespace */
1352 }/* CVC4 namespace */