src/printer/smt2/smt2_printer.cpp

   1 /*********************                                                        */
   2 /*! \file smt2_printer.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Andrew Reynolds, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief The pretty-printer interface for the SMT2 output language
  13  **
  14  ** The pretty-printer interface for the SMT2 output language.
  15  **/
  16
  17 #include "printer/smt2/smt2_printer.h"
  18
  19 #include <iostream>
  20 #include <string>
  21 #include <typeinfo>
  22 #include <vector>
  23
  24 #include "expr/node_manager_attributes.h"
  25 #include "options/language.h"
  26 #include "options/smt_options.h"
  27 #include "printer/dagification_visitor.h"
  28 #include "smt/smt_engine.h"
  29 #include "smt_util/boolean_simplification.h"
  30 #include "smt_util/node_visitor.h"
  31 #include "theory/arrays/theory_arrays_rewriter.h"
  32 #include "theory/quantifiers/quantifiers_attributes.h"
  33 #include "theory/substitutions.h"
  34 #include "theory/theory_model.h"
  35 #include "util/smt2_quote_string.h"
  36
  37 using namespace std;
  38
  39 namespace CVC4 {
  40 namespace printer {
  41 namespace smt2 {
  42
  43 static OutputLanguage variantToLanguage(Variant v);
  44
  45 static string smtKindString(Kind k, Variant v);
  46
  47 /** returns whether the variant is smt-lib 2.6 or greater */
  48 bool isVariant_2_6(Variant v)
  49 {
  50   return v == smt2_6_variant || v == smt2_6_1_variant;
  51 }
  52
  53 static void printBvParameterizedOp(std::ostream& out, TNode n);
  54 static void printFpParameterizedOp(std::ostream& out, TNode n);
  55
  56 static void toStreamRational(std::ostream& out,
  57                              const Rational& r,
  58                              bool decimal);
  59
  60 void Smt2Printer::toStream(
  61     std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const
  62 {
  63   if(dag != 0) {
  64     DagificationVisitor dv(dag);
  65     NodeVisitor<DagificationVisitor> visitor;
  66     visitor.run(dv, n);
  67     const theory::SubstitutionMap& lets = dv.getLets();
  68     if(!lets.empty()) {
  69       theory::SubstitutionMap::const_iterator i = lets.begin();
  70       theory::SubstitutionMap::const_iterator i_end = lets.end();
  71       for(; i != i_end; ++ i) {
  72         out << "(let ((";
  73         toStream(out, (*i).second, toDepth, types, TypeNode::null());
  74         out << ' ';
  75         toStream(out, (*i).first, toDepth, types, TypeNode::null());
  76         out << ")) ";
  77       }
  78     }
  79     Node body = dv.getDagifiedBody();
  80     toStream(out, body, toDepth, types, TypeNode::null());
  81     if(!lets.empty()) {
  82       theory::SubstitutionMap::const_iterator i = lets.begin();
  83       theory::SubstitutionMap::const_iterator i_end = lets.end();
  84       for(; i != i_end; ++ i) {
  85         out << ")";
  86       }
  87     }
  88   } else {
  89     toStream(out, n, toDepth, types, TypeNode::null());
  90   }
  91 }
  92
  93 static std::string maybeQuoteSymbol(const std::string& s) {
  94   // this is the set of SMT-LIBv2 permitted characters in "simple" (non-quoted) symbols
  95   if(s.find_first_not_of("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789~!@$%^&*_-+=<>.?/") != string::npos) {
  96     // need to quote it
  97     stringstream ss;
  98     ss << '|' << s << '|';
  99     return ss.str();
 100   }
 101   return s;
 102 }
 103
 104 static bool stringifyRegexp(Node n, stringstream& ss) {
 105   if(n.getKind() == kind::STRING_TO_REGEXP) {
 106     ss << n[0].getConst<String>().toString(true);
 107   } else if(n.getKind() == kind::REGEXP_CONCAT) {
 108     for(unsigned i = 0; i < n.getNumChildren(); ++i) {
 109       if(!stringifyRegexp(n[i], ss)) {
 110         return false;
 111       }
 112     }
 113   } else {
 114     return false;
 115   }
 116   return true;
 117 }
 118
 119 // force_nt is the type that n must have
 120 void Smt2Printer::toStream(std::ostream& out,
 121                            TNode n,
 122                            int toDepth,
 123                            bool types,
 124                            TypeNode force_nt) const
 125 {
 126   // null
 127   if(n.getKind() == kind::NULL_EXPR) {
 128     out << "null";
 129     return;
 130   }
 131
 132   // constant
 133   if(n.getMetaKind() == kind::metakind::CONSTANT) {
 134     switch(n.getKind()) {
 135     case kind::TYPE_CONSTANT:
 136       switch(n.getConst<TypeConstant>()) {
 137       case BOOLEAN_TYPE: out << "Bool"; break;
 138       case REAL_TYPE: out << "Real"; break;
 139       case INTEGER_TYPE: out << "Int"; break;
 140       case STRING_TYPE: out << "String"; break;
 141       case ROUNDINGMODE_TYPE: out << "RoundingMode"; break;
 142       default:
 143         // fall back on whatever operator<< does on underlying type; we
 144         // might luck out and be SMT-LIB v2 compliant
 145         kind::metakind::NodeValueConstPrinter::toStream(out, n);
 146       }
 147       break;
 148     case kind::BITVECTOR_TYPE:
 149       if(d_variant == sygus_variant ){
 150         out << "(BitVec " << n.getConst<BitVectorSize>().size << ")";
 151       }else{
 152         out << "(_ BitVec " << n.getConst<BitVectorSize>().size << ")";
 153       }
 154       break;
 155     case kind::FLOATINGPOINT_TYPE:
 156       out << "(_ FloatingPoint "
 157           << n.getConst<FloatingPointSize>().exponent() << " "
 158           << n.getConst<FloatingPointSize>().significand()
 159           << ")";
 160       break;
 161     case kind::CONST_BITVECTOR: {
 162       const BitVector& bv = n.getConst<BitVector>();
 163       const Integer& x = bv.getValue();
 164       unsigned n = bv.getSize();
 165       if(d_variant == sygus_variant ){
 166         out << "#b" << bv.toString();
 167       }else{
 168         out << "(_ ";
 169         out << "bv" << x <<" " << n;
 170         out << ")";
 171       }
 172
 173       // //out << "#b";
 174
 175       // while(n-- > 0) {
 176       //   out << (x.testBit(n) ? '1' : '0');
 177       // }
 178       break;
 179     }
 180     case kind::CONST_FLOATINGPOINT:
 181       out << n.getConst<FloatingPoint>();
 182       break;
 183     case kind::CONST_ROUNDINGMODE:
 184       switch (n.getConst<RoundingMode>()) {
 185       case roundNearestTiesToEven : out << "roundNearestTiesToEven"; break;
 186       case roundNearestTiesToAway : out << "roundNearestTiesToAway"; break;
 187       case roundTowardPositive : out << "roundTowardPositive"; break;
 188       case roundTowardNegative : out << "roundTowardNegative"; break;
 189       case roundTowardZero : out << "roundTowardZero"; break;
 190       default :
 191         Unreachable("Invalid value of rounding mode constant (%d)",n.getConst<RoundingMode>());
 192       }
 193       break;
 194     case kind::CONST_BOOLEAN:
 195       // the default would print "1" or "0" for bool, that's not correct
 196       // for our purposes
 197       out << (n.getConst<bool>() ? "true" : "false");
 198       break;
 199     case kind::BUILTIN:
 200       out << smtKindString(n.getConst<Kind>(), d_variant);
 201       break;
 202     case kind::CHAIN_OP:
 203       out << smtKindString(n.getConst<Chain>().getOperator(), d_variant);
 204       break;
 205     case kind::CONST_RATIONAL: {
 206       const Rational& r = n.getConst<Rational>();
 207       if(d_variant == sygus_variant ){
 208         if(r < 0) {
 209           out << "-" << -r;
 210         }else{
 211           toStreamRational(out, r, !force_nt.isNull() && !force_nt.isInteger());
 212         }
 213       }else{
 214         toStreamRational(out, r, !force_nt.isNull() && !force_nt.isInteger());
 215       }
 216       // Rational r = n.getConst<Rational>();
 217       // if(r < 0) {
 218       //   if(r.isIntegral()) {
 219       //     out << "(- " << -r << ')';
 220       //   } else {
 221       //     out << "(- (/ " << (-r).getNumerator() << ' ' << (-r).getDenominator() << "))";
 222       //   }
 223       // } else {
 224       //   if(r.isIntegral()) {
 225       //     out << r;
 226       //   } else {
 227       //     out << "(/ " << r.getNumerator() << ' ' << r.getDenominator() << ')';
 228       //   }
 229       // }
 230       break;
 231     }
 232
 233     case kind::CONST_STRING: {
 234       //const std::vector<unsigned int>& s = n.getConst<String>().getVec();
 235       std::string s = n.getConst<String>().toString(true);
 236       out << '"';
 237       for(size_t i = 0; i < s.size(); ++i) {
 238         //char c = String::convertUnsignedIntToChar(s[i]);
 239         char c = s[i];
 240         if(c == '"') {
 241           if(d_variant == smt2_0_variant) {
 242             out << "\\\"";
 243           } else {
 244             out << "\"\"";
 245           }
 246         } else {
 247           out << c;
 248         }
 249       }
 250       out << '"';
 251       break;
 252     }
 253
 254     case kind::STORE_ALL: {
 255       ArrayStoreAll asa = n.getConst<ArrayStoreAll>();
 256       out << "((as const " << asa.getType() << ") " << asa.getExpr() << ")";
 257       break;
 258     }
 259
 260     case kind::DATATYPE_TYPE:
 261     {
 262       const Datatype& dt = (NodeManager::currentNM()->getDatatypeForIndex(
 263           n.getConst<DatatypeIndexConstant>().getIndex()));
 264       if (dt.isTuple())
 265       {
 266         unsigned int n = dt[0].getNumArgs();
 267         if (n == 0)
 268         {
 269           out << "Tuple";
 270         }
 271         else
 272         {
 273           out << "(Tuple";
 274           for (unsigned int i = 0; i < n; i++)
 275           {
 276             out << " " << dt[0][i].getRangeType();
 277           }
 278           out << ")";
 279         }
 280       }
 281       else
 282       {
 283         out << maybeQuoteSymbol(dt.getName());
 284       }
 285       break;
 286     }
 287
 288     case kind::UNINTERPRETED_CONSTANT: {
 289       const UninterpretedConstant& uc = n.getConst<UninterpretedConstant>();
 290       out << '@' << uc;
 291       break;
 292     }
 293
 294     case kind::EMPTYSET:
 295       out << "(as emptyset " << n.getConst<EmptySet>().getType() << ")";
 296       break;
 297
 298     default:
 299       // fall back on whatever operator<< does on underlying type; we
 300       // might luck out and be SMT-LIB v2 compliant
 301       kind::metakind::NodeValueConstPrinter::toStream(out, n);
 302     }
 303
 304     return;
 305   }
 306
 307   if(n.getKind() == kind::SORT_TYPE) {
 308     string name;
 309     if(n.getNumChildren() != 0) {
 310       out << '(';
 311     }
 312     if(n.getAttribute(expr::VarNameAttr(), name)) {
 313       out << maybeQuoteSymbol(name);
 314     }
 315     if(n.getNumChildren() != 0) {
 316       for(unsigned i = 0; i < n.getNumChildren(); ++i) {
 317               out << ' ';
 318               toStream(out, n[i], toDepth, types, TypeNode::null());
 319       }
 320       out << ')';
 321     }
 322     return;
 323   }
 324
 325   if (!force_nt.isNull())
 326   {
 327     if (n.getType() != force_nt)
 328     {
 329       if (force_nt.isReal())
 330       {
 331         out << "(" << smtKindString(force_nt.isInteger() ? kind::TO_INTEGER
 332                                                          : kind::TO_REAL,
 333                                     d_variant)
 334             << " ";
 335         toStream(out, n, toDepth, types, TypeNode::null());
 336         out << ")";
 337       }
 338       else
 339       {
 340         Node nn = NodeManager::currentNM()->mkNode(
 341             kind::APPLY_TYPE_ASCRIPTION,
 342             NodeManager::currentNM()->mkConst(
 343                 AscriptionType(force_nt.toType())),
 344             n);
 345         toStream(out, nn, toDepth, types, TypeNode::null());
 346       }
 347       return;
 348     }
 349   }
 350
 351   // variable
 352   if (n.isVar())
 353   {
 354     string s;
 355     if (n.getAttribute(expr::VarNameAttr(), s))
 356     {
 357       out << maybeQuoteSymbol(s);
 358     }
 359     else
 360     {
 361       if (n.getKind() == kind::VARIABLE)
 362       {
 363         out << "var_";
 364       }
 365       else
 366       {
 367         out << n.getKind() << '_';
 368       }
 369       out << n.getId();
 370     }
 371     if (types)
 372     {
 373       // print the whole type, but not *its* type
 374       out << ":";
 375       n.getType().toStream(out, language::output::LANG_SMTLIB_V2_5);
 376     }
 377
 378     return;
 379   }
 380
 381   bool stillNeedToPrintParams = true;
 382   bool forceBinary = false; // force N-ary to binary when outputing children
 383   bool parametricTypeChildren = false;   // parametric operators that are (op t1 ... tn) where t1...tn must have same type
 384   bool typeChildren = false;  // operators (op t1...tn) where at least one of t1...tn may require a type cast e.g. Int -> Real
 385   // operator
 386   if(n.getNumChildren() != 0 &&
 387      n.getKind() != kind::INST_PATTERN_LIST &&
 388      n.getKind() != kind::APPLY_TYPE_ASCRIPTION) {
 389     out << '(';
 390   }
 391   switch(Kind k = n.getKind()) {
 392     // builtin theory
 393   case kind::APPLY: break;
 394   case kind::EQUAL:
 395   case kind::DISTINCT:
 396     out << smtKindString(k, d_variant) << " ";
 397     parametricTypeChildren = true;
 398     break;
 399   case kind::CHAIN: break;
 400   case kind::FUNCTION_TYPE:
 401     out << "->";
 402     for (Node nc : n)
 403     {
 404       out << " ";
 405       toStream(out, nc, toDepth, types, TypeNode::null());
 406     }
 407     out << ")";
 408     return;
 409   case kind::SEXPR: break;
 410
 411     // bool theory
 412   case kind::NOT:
 413   case kind::AND:
 414   case kind::IMPLIES:
 415   case kind::OR:
 416   case kind::XOR:
 417   case kind::ITE:
 418     out << smtKindString(k, d_variant) << " ";
 419     break;
 420
 421   // uf theory
 422   case kind::APPLY_UF: typeChildren = true; break;
 423   // higher-order
 424   case kind::HO_APPLY: break;
 425   case kind::LAMBDA:
 426     out << smtKindString(k, d_variant) << " ";
 427     break;
 428
 429   // arith theory
 430   case kind::PLUS:
 431   case kind::MULT:
 432   case kind::NONLINEAR_MULT:
 433   case kind::EXPONENTIAL:
 434   case kind::SINE:
 435   case kind::COSINE:
 436   case kind::TANGENT:
 437   case kind::COSECANT:
 438   case kind::SECANT:
 439   case kind::COTANGENT:
 440   case kind::ARCSINE:
 441   case kind::ARCCOSINE:
 442   case kind::ARCTANGENT:
 443   case kind::ARCCOSECANT:
 444   case kind::ARCSECANT:
 445   case kind::ARCCOTANGENT:
 446   case kind::SQRT:
 447   case kind::MINUS:
 448   case kind::UMINUS:
 449   case kind::LT:
 450   case kind::LEQ:
 451   case kind::GT:
 452   case kind::GEQ:
 453   case kind::DIVISION:
 454   case kind::DIVISION_TOTAL:
 455   case kind::INTS_DIVISION:
 456   case kind::INTS_DIVISION_TOTAL:
 457   case kind::INTS_MODULUS:
 458   case kind::INTS_MODULUS_TOTAL:
 459   case kind::ABS:
 460   case kind::IS_INTEGER:
 461   case kind::TO_INTEGER:
 462   case kind::TO_REAL:
 463   case kind::POW:
 464     parametricTypeChildren = true;
 465     out << smtKindString(k, d_variant) << " ";
 466     break;
 467
 468   case kind::DIVISIBLE:
 469     out << "(_ divisible " << n.getOperator().getConst<Divisible>().k << ")";
 470     stillNeedToPrintParams = false;
 471     break;
 472
 473     // arrays theory
 474   case kind::SELECT:
 475   case kind::STORE: typeChildren = true;
 476   case kind::PARTIAL_SELECT_0:
 477   case kind::PARTIAL_SELECT_1:
 478   case kind::ARRAY_TYPE:
 479     out << smtKindString(k, d_variant) << " ";
 480     break;
 481
 482   // string theory
 483   case kind::STRING_CONCAT:
 484     if(d_variant == z3str_variant) {
 485       out << "Concat ";
 486       for(unsigned i = 0; i < n.getNumChildren(); ++i) {
 487         toStream(out, n[i], -1, types, TypeNode::null());
 488         if(i + 1 < n.getNumChildren()) {
 489           out << ' ';
 490         }
 491         if(i + 2 < n.getNumChildren()) {
 492           out << "(Concat ";
 493         }
 494       }
 495       for(unsigned i = 0; i < n.getNumChildren() - 1; ++i) {
 496         out << ")";
 497       }
 498       return;
 499     }
 500     out << "str.++ ";
 501     break;
 502   case kind::STRING_IN_REGEXP: {
 503     stringstream ss;
 504     if(d_variant == z3str_variant && stringifyRegexp(n[1], ss)) {
 505       out << "= ";
 506       toStream(out, n[0], -1, types, TypeNode::null());
 507       out << " ";
 508       Node str = NodeManager::currentNM()->mkConst(String(ss.str()));
 509       toStream(out, str, -1, types, TypeNode::null());
 510       out << ")";
 511       return;
 512     }
 513     out << smtKindString(k, d_variant) << " ";
 514     break;
 515   }
 516   case kind::STRING_LENGTH:
 517   case kind::STRING_SUBSTR:
 518   case kind::STRING_CHARAT:
 519   case kind::STRING_STRCTN:
 520   case kind::STRING_STRIDOF:
 521   case kind::STRING_STRREPL:
 522   case kind::STRING_PREFIX:
 523   case kind::STRING_SUFFIX:
 524   case kind::STRING_LEQ:
 525   case kind::STRING_LT:
 526   case kind::STRING_ITOS:
 527   case kind::STRING_STOI:
 528   case kind::STRING_CODE:
 529   case kind::STRING_TO_REGEXP:
 530   case kind::REGEXP_CONCAT:
 531   case kind::REGEXP_UNION:
 532   case kind::REGEXP_INTER:
 533   case kind::REGEXP_STAR:
 534   case kind::REGEXP_PLUS:
 535   case kind::REGEXP_OPT:
 536   case kind::REGEXP_RANGE:
 537   case kind::REGEXP_LOOP:
 538   case kind::REGEXP_EMPTY:
 539   case kind::REGEXP_SIGMA: out << smtKindString(k, d_variant) << " "; break;
 540
 541   case kind::CARDINALITY_CONSTRAINT: out << "fmf.card "; break;
 542   case kind::CARDINALITY_VALUE: out << "fmf.card.val "; break;
 543
 544     // bv theory
 545   case kind::BITVECTOR_CONCAT: out << "concat "; forceBinary = true; break;
 546   case kind::BITVECTOR_AND: out << "bvand "; forceBinary = true; break;
 547   case kind::BITVECTOR_OR: out << "bvor "; forceBinary = true; break;
 548   case kind::BITVECTOR_XOR: out << "bvxor "; forceBinary = true; break;
 549   case kind::BITVECTOR_NOT: out << "bvnot "; break;
 550   case kind::BITVECTOR_NAND: out << "bvnand "; break;
 551   case kind::BITVECTOR_NOR: out << "bvnor "; break;
 552   case kind::BITVECTOR_XNOR: out << "bvxnor "; break;
 553   case kind::BITVECTOR_COMP: out << "bvcomp "; break;
 554   case kind::BITVECTOR_MULT: out << "bvmul "; forceBinary = true; break;
 555   case kind::BITVECTOR_PLUS: out << "bvadd "; forceBinary = true; break;
 556   case kind::BITVECTOR_SUB: out << "bvsub "; break;
 557   case kind::BITVECTOR_NEG: out << "bvneg "; break;
 558   case kind::BITVECTOR_UDIV: out << "bvudiv "; break;
 559   case kind::BITVECTOR_UDIV_TOTAL: out << "bvudiv_total "; break;
 560   case kind::BITVECTOR_UREM: out << "bvurem "; break;
 561   case kind::BITVECTOR_UREM_TOTAL: out << "bvurem_total "; break;
 562   case kind::BITVECTOR_SDIV: out << "bvsdiv "; break;
 563   case kind::BITVECTOR_SREM: out << "bvsrem "; break;
 564   case kind::BITVECTOR_SMOD: out << "bvsmod "; break;
 565   case kind::BITVECTOR_SHL: out << "bvshl "; break;
 566   case kind::BITVECTOR_LSHR: out << "bvlshr "; break;
 567   case kind::BITVECTOR_ASHR: out << "bvashr "; break;
 568   case kind::BITVECTOR_ULT: out << "bvult "; break;
 569   case kind::BITVECTOR_ULE: out << "bvule "; break;
 570   case kind::BITVECTOR_UGT: out << "bvugt "; break;
 571   case kind::BITVECTOR_UGE: out << "bvuge "; break;
 572   case kind::BITVECTOR_SLT: out << "bvslt "; break;
 573   case kind::BITVECTOR_SLE: out << "bvsle "; break;
 574   case kind::BITVECTOR_SGT: out << "bvsgt "; break;
 575   case kind::BITVECTOR_SGE: out << "bvsge "; break;
 576   case kind::BITVECTOR_TO_NAT: out << "bv2nat "; break;
 577   case kind::BITVECTOR_REDOR: out << "bvredor "; break;
 578   case kind::BITVECTOR_REDAND: out << "bvredand "; break;
 579
 580   case kind::BITVECTOR_EXTRACT:
 581   case kind::BITVECTOR_REPEAT:
 582   case kind::BITVECTOR_ZERO_EXTEND:
 583   case kind::BITVECTOR_SIGN_EXTEND:
 584   case kind::BITVECTOR_ROTATE_LEFT:
 585   case kind::BITVECTOR_ROTATE_RIGHT:
 586   case kind::INT_TO_BITVECTOR:
 587     printBvParameterizedOp(out, n);
 588     out << ' ';
 589     stillNeedToPrintParams = false;
 590     break;
 591
 592     // sets
 593   case kind::UNION:
 594   case kind::INTERSECTION:
 595   case kind::SETMINUS:
 596   case kind::SUBSET:
 597   case kind::CARD:
 598   case kind::JOIN:
 599   case kind::PRODUCT:
 600   case kind::TRANSPOSE:
 601   case kind::TCLOSURE:
 602     parametricTypeChildren = true;
 603     out << smtKindString(k, d_variant) << " ";
 604     break;
 605   case kind::MEMBER: typeChildren = true;
 606   case kind::SET_TYPE:
 607   case kind::SINGLETON:
 608   case kind::COMPLEMENT: out << smtKindString(k, d_variant) << " "; break;
 609   case kind::UNIVERSE_SET:out << "(as univset " << n.getType() << ")";break;
 610
 611     // fp theory
 612   case kind::FLOATINGPOINT_FP:
 613   case kind::FLOATINGPOINT_EQ:
 614   case kind::FLOATINGPOINT_ABS:
 615   case kind::FLOATINGPOINT_NEG:
 616   case kind::FLOATINGPOINT_PLUS:
 617   case kind::FLOATINGPOINT_SUB:
 618   case kind::FLOATINGPOINT_MULT:
 619   case kind::FLOATINGPOINT_DIV:
 620   case kind::FLOATINGPOINT_FMA:
 621   case kind::FLOATINGPOINT_SQRT:
 622   case kind::FLOATINGPOINT_REM:
 623   case kind::FLOATINGPOINT_RTI:
 624   case kind::FLOATINGPOINT_MIN:
 625   case kind::FLOATINGPOINT_MAX:
 626   case kind::FLOATINGPOINT_LEQ:
 627   case kind::FLOATINGPOINT_LT:
 628   case kind::FLOATINGPOINT_GEQ:
 629   case kind::FLOATINGPOINT_GT:
 630   case kind::FLOATINGPOINT_ISN:
 631   case kind::FLOATINGPOINT_ISSN:
 632   case kind::FLOATINGPOINT_ISZ:
 633   case kind::FLOATINGPOINT_ISINF:
 634   case kind::FLOATINGPOINT_ISNAN:
 635   case kind::FLOATINGPOINT_ISNEG:
 636   case kind::FLOATINGPOINT_ISPOS:
 637   case kind::FLOATINGPOINT_TO_REAL:
 638     out << smtKindString(k, d_variant) << ' ';
 639     break;
 640
 641   case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
 642   case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT:
 643   case kind::FLOATINGPOINT_TO_FP_REAL:
 644   case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
 645   case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
 646   case kind::FLOATINGPOINT_TO_FP_GENERIC:
 647   case kind::FLOATINGPOINT_TO_UBV:
 648   case kind::FLOATINGPOINT_TO_SBV:
 649     printFpParameterizedOp(out, n);
 650     out << ' ';
 651     stillNeedToPrintParams = false;
 652     break;
 653
 654     // datatypes
 655   case kind::APPLY_TYPE_ASCRIPTION: {
 656       TypeNode t = TypeNode::fromType(n.getOperator().getConst<AscriptionType>().getType());
 657       if(t.getKind() == kind::TYPE_CONSTANT &&
 658          t.getConst<TypeConstant>() == REAL_TYPE &&
 659          n[0].getType().isInteger()) {
 660         // Special case, in model output integer constants that should be
 661         // Real-sorted are wrapped in a type ascription.  Handle that here.
 662
 663         // Note: This is Tim making a guess about Morgan's Code.
 664         Assert(n[0].getKind() == kind::CONST_RATIONAL);
 665         toStreamRational(out, n[0].getConst<Rational>(), true);
 666
 667         //toStream(out, n[0], -1, false);
 668         //out << ".0";
 669
 670         return;
 671       }
 672       out << "(as ";
 673       toStream(out, n[0], toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null());
 674       out << ' ' << (t.isFunctionLike() ? t.getRangeType() : t) << ')';
 675       return;
 676     }
 677     break;
 678
 679     case kind::APPLY_CONSTRUCTOR:
 680     {
 681       typeChildren = true;
 682       const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
 683       if (dt.isTuple())
 684       {
 685         stillNeedToPrintParams = false;
 686         out << "mkTuple" << ( dt[0].getNumArgs()==0 ? "" : " ");
 687       }
 688     }
 689
 690     case kind::APPLY_TESTER:
 691     case kind::APPLY_SELECTOR:
 692     case kind::APPLY_SELECTOR_TOTAL:
 693     case kind::PARAMETRIC_DATATYPE: break;
 694
 695     // separation logic
 696     case kind::SEP_EMP:
 697     case kind::SEP_PTO:
 698     case kind::SEP_STAR:
 699     case kind::SEP_WAND: out << smtKindString(k, d_variant) << " "; break;
 700
 701     case kind::SEP_NIL:
 702       out << "(as sep.nil " << n.getType() << ")";
 703       break;
 704
 705       // quantifiers
 706     case kind::FORALL:
 707     case kind::EXISTS:
 708       if (k == kind::FORALL)
 709       {
 710         out << "forall ";
 711       }
 712       else
 713       {
 714         out << "exists ";
 715       }
 716       for (unsigned i = 0; i < 2; i++)
 717       {
 718         out << n[i] << " ";
 719         if (i == 0 && n.getNumChildren() == 3)
 720         {
 721           out << "(! ";
 722         }
 723       }
 724       if (n.getNumChildren() == 3)
 725       {
 726         out << n[2];
 727         out << ")";
 728       }
 729       out << ")";
 730       return;
 731       break;
 732     case kind::BOUND_VAR_LIST:
 733       // the left parenthesis is already printed (before the switch)
 734       for (TNode::iterator i = n.begin(), iend = n.end(); i != iend;)
 735       {
 736         out << '(';
 737         toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, types, 0);
 738         out << ' ';
 739         out << (*i).getType();
 740         // The following code do stange things
 741         // (*i).getType().toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
 742         //                         false, language::output::LANG_SMTLIB_V2_5);
 743         out << ')';
 744         if (++i != iend)
 745         {
 746           out << ' ';
 747         }
 748       }
 749       out << ')';
 750       return;
 751     case kind::INST_PATTERN: break;
 752     case kind::INST_PATTERN_LIST:
 753       for (unsigned i = 0; i < n.getNumChildren(); i++)
 754       {
 755         if (n[i].getKind() == kind::INST_ATTRIBUTE)
 756         {
 757           if (n[i][0].getAttribute(theory::FunDefAttribute()))
 758           {
 759             out << ":fun-def";
 760           }
 761         }
 762         else
 763         {
 764           out << ":pattern " << n[i];
 765         }
 766       }
 767       return;
 768       break;
 769
 770     default:
 771       // fall back on however the kind prints itself; this probably
 772       // won't be SMT-LIB v2 compliant, but it will be clear from the
 773       // output that support for the kind needs to be added here.
 774       out << n.getKind() << ' ';
 775   }
 776   if( n.getMetaKind() == kind::metakind::PARAMETERIZED &&
 777       stillNeedToPrintParams ) {
 778     if(toDepth != 0) {
 779       if( d_variant==sygus_variant && n.getKind()==kind::APPLY_CONSTRUCTOR ){
 780         std::stringstream ss;
 781         toStream(ss, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null());
 782         std::string tmp = ss.str();
 783         size_t pos = 0;
 784         if((pos = tmp.find("__Enum__", pos)) != std::string::npos){
 785            tmp.replace(pos, 8, "::");
 786         }
 787         out << tmp;
 788       }else if( n.getKind()==kind::APPLY_TESTER ){
 789         unsigned cindex = Datatype::indexOf(n.getOperator().toExpr());
 790         const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
 791         if (isVariant_2_6(d_variant))
 792         {
 793           out << "(_ is ";
 794           toStream(out, Node::fromExpr(dt[cindex].getConstructor()), toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null());
 795           out << ")";
 796         }else{
 797           out << "is-";
 798           toStream(out, Node::fromExpr(dt[cindex].getConstructor()), toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null());
 799         }
 800       }else{
 801         toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null());
 802       }
 803     } else {
 804       out << "(...)";
 805     }
 806     if(n.getNumChildren() > 0) {
 807       out << ' ';
 808     }
 809   }
 810   stringstream parens;
 811
 812   // calculate the child type casts
 813   std::map< unsigned, TypeNode > force_child_type;
 814   if( parametricTypeChildren ){
 815     if( n.getNumChildren()>1 ){
 816       TypeNode force_ct = n[0].getType();
 817       bool do_force = false;
 818       for(size_t i = 1; i < n.getNumChildren(); ++i ) {
 819         TypeNode ct = n[i].getType();
 820         if( ct!=force_ct ){
 821           force_ct = TypeNode::leastCommonTypeNode( force_ct, ct );
 822           do_force = true;
 823         }
 824       }
 825       if( do_force ){
 826         for(size_t i = 0; i < n.getNumChildren(); ++i ) {
 827           force_child_type[i] = force_ct;
 828         }
 829       }
 830     }
 831   // operators that may require type casting
 832   }else if( typeChildren ){
 833     if(n.getKind()==kind::SELECT){
 834       TypeNode indexType = TypeNode::leastCommonTypeNode( n[0].getType().getArrayIndexType(), n[1].getType() );
 835       TypeNode elemType = n[0].getType().getArrayConstituentType();
 836       force_child_type[0] = NodeManager::currentNM()->mkArrayType( indexType, elemType );
 837       force_child_type[1] = indexType;
 838     }else if(n.getKind()==kind::STORE){
 839       TypeNode indexType = TypeNode::leastCommonTypeNode( n[0].getType().getArrayIndexType(), n[1].getType() );
 840       TypeNode elemType = TypeNode::leastCommonTypeNode( n[0].getType().getArrayConstituentType(), n[2].getType() );
 841       force_child_type[0] = NodeManager::currentNM()->mkArrayType( indexType, elemType );
 842       force_child_type[1] = indexType;
 843       force_child_type[2] = elemType;
 844     }else if(n.getKind()==kind::MEMBER){
 845       TypeNode elemType = TypeNode::leastCommonTypeNode( n[0].getType(), n[1].getType().getSetElementType() );
 846       force_child_type[0] = elemType;
 847       force_child_type[1] = NodeManager::currentNM()->mkSetType( elemType );
 848     }else{
 849       // APPLY_UF, APPLY_CONSTRUCTOR, etc.
 850       Assert( n.hasOperator() );
 851       TypeNode opt = n.getOperator().getType();
 852       Assert( opt.getNumChildren() == n.getNumChildren() + 1 );
 853       for(size_t i = 0; i < n.getNumChildren(); ++i ) {
 854         force_child_type[i] = opt[i];
 855       }
 856     }
 857   }
 858
 859   for(size_t i = 0, c = 1; i < n.getNumChildren(); ) {
 860     if(toDepth != 0) {
 861       Node cn = n[i];
 862       std::map< unsigned, TypeNode >::iterator itfc = force_child_type.find( i );
 863       if( itfc!=force_child_type.end() ){
 864         toStream(out, cn, toDepth < 0 ? toDepth : toDepth - c, types, itfc->second);
 865       }else{
 866         toStream(out, cn, toDepth < 0 ? toDepth : toDepth - c, types, TypeNode::null());
 867       }
 868     } else {
 869       out << "(...)";
 870     }
 871     if(++i < n.getNumChildren()) {
 872       if(forceBinary && i < n.getNumChildren() - 1) {
 873         // not going to work properly for parameterized kinds!
 874         Assert(n.getMetaKind() != kind::metakind::PARAMETERIZED);
 875         out << " (" << smtKindString(n.getKind(), d_variant) << ' ';
 876         parens << ')';
 877         ++c;
 878       } else {
 879         out << ' ';
 880       }
 881     }
 882   }
 883   if(n.getNumChildren() != 0) {
 884     out << parens.str() << ')';
 885   }
 886 }/* Smt2Printer::toStream(TNode) */
 887
 888 static string smtKindString(Kind k, Variant v)
 889 {
 890   switch(k) {
 891     // builtin theory
 892   case kind::APPLY: break;
 893   case kind::EQUAL: return "=";
 894   case kind::DISTINCT: return "distinct";
 895   case kind::CHAIN: break;
 896   case kind::SEXPR: break;
 897
 898     // bool theory
 899   case kind::NOT: return "not";
 900   case kind::AND: return "and";
 901   case kind::IMPLIES: return "=>";
 902   case kind::OR: return "or";
 903   case kind::XOR: return "xor";
 904   case kind::ITE: return "ite";
 905
 906     // uf theory
 907   case kind::APPLY_UF: break;
 908
 909   case kind::LAMBDA:
 910     return "lambda";
 911
 912   // arith theory
 913   case kind::PLUS: return "+";
 914   case kind::MULT:
 915   case kind::NONLINEAR_MULT: return "*";
 916   case kind::EXPONENTIAL: return "exp";
 917   case kind::SINE: return "sin";
 918   case kind::COSINE: return "cos";
 919   case kind::TANGENT: return "tan";
 920   case kind::COSECANT: return "csc";
 921   case kind::SECANT: return "sec";
 922   case kind::COTANGENT: return "cot";
 923   case kind::ARCSINE: return "arcsin";
 924   case kind::ARCCOSINE: return "arccos";
 925   case kind::ARCTANGENT: return "arctan";
 926   case kind::ARCCOSECANT: return "arccsc";
 927   case kind::ARCSECANT: return "arcsec";
 928   case kind::ARCCOTANGENT: return "arccot";
 929   case kind::SQRT: return "sqrt";
 930   case kind::MINUS: return "-";
 931   case kind::UMINUS: return "-";
 932   case kind::LT: return "<";
 933   case kind::LEQ: return "<=";
 934   case kind::GT: return ">";
 935   case kind::GEQ: return ">=";
 936   case kind::DIVISION:
 937   case kind::DIVISION_TOTAL: return "/";
 938   case kind::INTS_DIVISION_TOTAL:
 939   case kind::INTS_DIVISION: return "div";
 940   case kind::INTS_MODULUS_TOTAL:
 941   case kind::INTS_MODULUS: return "mod";
 942   case kind::ABS: return "abs";
 943   case kind::IS_INTEGER: return "is_int";
 944   case kind::TO_INTEGER: return "to_int";
 945   case kind::TO_REAL: return "to_real";
 946   case kind::POW: return "^";
 947
 948     // arrays theory
 949   case kind::SELECT: return "select";
 950   case kind::STORE: return "store";
 951   case kind::ARRAY_TYPE: return "Array";
 952   case kind::PARTIAL_SELECT_0: return "partial_select_0";
 953   case kind::PARTIAL_SELECT_1: return "partial_select_1";
 954
 955     // bv theory
 956   case kind::BITVECTOR_CONCAT: return "concat";
 957   case kind::BITVECTOR_AND: return "bvand";
 958   case kind::BITVECTOR_OR: return "bvor";
 959   case kind::BITVECTOR_XOR: return "bvxor";
 960   case kind::BITVECTOR_NOT: return "bvnot";
 961   case kind::BITVECTOR_NAND: return "bvnand";
 962   case kind::BITVECTOR_NOR: return "bvnor";
 963   case kind::BITVECTOR_XNOR: return "bvxnor";
 964   case kind::BITVECTOR_COMP: return "bvcomp";
 965   case kind::BITVECTOR_MULT: return "bvmul";
 966   case kind::BITVECTOR_PLUS: return "bvadd";
 967   case kind::BITVECTOR_SUB: return "bvsub";
 968   case kind::BITVECTOR_NEG: return "bvneg";
 969   case kind::BITVECTOR_UDIV_TOTAL:
 970   case kind::BITVECTOR_UDIV: return "bvudiv";
 971   case kind::BITVECTOR_UREM: return "bvurem";
 972   case kind::BITVECTOR_SDIV: return "bvsdiv";
 973   case kind::BITVECTOR_SREM: return "bvsrem";
 974   case kind::BITVECTOR_SMOD: return "bvsmod";
 975   case kind::BITVECTOR_SHL: return "bvshl";
 976   case kind::BITVECTOR_LSHR: return "bvlshr";
 977   case kind::BITVECTOR_ASHR: return "bvashr";
 978   case kind::BITVECTOR_ULT: return "bvult";
 979   case kind::BITVECTOR_ULE: return "bvule";
 980   case kind::BITVECTOR_UGT: return "bvugt";
 981   case kind::BITVECTOR_UGE: return "bvuge";
 982   case kind::BITVECTOR_SLT: return "bvslt";
 983   case kind::BITVECTOR_SLE: return "bvsle";
 984   case kind::BITVECTOR_SGT: return "bvsgt";
 985   case kind::BITVECTOR_SGE: return "bvsge";
 986   case kind::BITVECTOR_REDOR: return "bvredor";
 987   case kind::BITVECTOR_REDAND: return "bvredand";
 988
 989   case kind::BITVECTOR_EXTRACT: return "extract";
 990   case kind::BITVECTOR_REPEAT: return "repeat";
 991   case kind::BITVECTOR_ZERO_EXTEND: return "zero_extend";
 992   case kind::BITVECTOR_SIGN_EXTEND: return "sign_extend";
 993   case kind::BITVECTOR_ROTATE_LEFT: return "rotate_left";
 994   case kind::BITVECTOR_ROTATE_RIGHT: return "rotate_right";
 995
 996   case kind::UNION: return "union";
 997   case kind::INTERSECTION: return "intersection";
 998   case kind::SETMINUS: return "setminus";
 999   case kind::SUBSET: return "subset";
1000   case kind::MEMBER: return "member";
1001   case kind::SET_TYPE: return "Set";
1002   case kind::SINGLETON: return "singleton";
1003   case kind::INSERT: return "insert";
1004   case kind::COMPLEMENT: return "complement";
1005   case kind::CARD: return "card";
1006   case kind::JOIN: return "join";
1007   case kind::PRODUCT: return "product";
1008   case kind::TRANSPOSE: return "transpose";
1009   case kind::TCLOSURE:
1010     return "tclosure";
1011
1012     // fp theory
1013   case kind::FLOATINGPOINT_FP: return "fp";
1014   case kind::FLOATINGPOINT_EQ: return "fp.eq";
1015   case kind::FLOATINGPOINT_ABS: return "fp.abs";
1016   case kind::FLOATINGPOINT_NEG: return "fp.neg";
1017   case kind::FLOATINGPOINT_PLUS: return "fp.add";
1018   case kind::FLOATINGPOINT_SUB: return "fp.sub";
1019   case kind::FLOATINGPOINT_MULT: return "fp.mul";
1020   case kind::FLOATINGPOINT_DIV: return "fp.div";
1021   case kind::FLOATINGPOINT_FMA: return "fp.fma";
1022   case kind::FLOATINGPOINT_SQRT: return "fp.sqrt";
1023   case kind::FLOATINGPOINT_REM: return "fp.rem";
1024   case kind::FLOATINGPOINT_RTI: return "fp.roundToIntegral";
1025   case kind::FLOATINGPOINT_MIN: return "fp.min";
1026   case kind::FLOATINGPOINT_MAX: return "fp.max";
1027   case kind::FLOATINGPOINT_MIN_TOTAL: return "fp.min_total";
1028   case kind::FLOATINGPOINT_MAX_TOTAL: return "fp.max_total";
1029
1030   case kind::FLOATINGPOINT_LEQ: return "fp.leq";
1031   case kind::FLOATINGPOINT_LT: return "fp.lt";
1032   case kind::FLOATINGPOINT_GEQ: return "fp.geq";
1033   case kind::FLOATINGPOINT_GT: return "fp.gt";
1034
1035   case kind::FLOATINGPOINT_ISN: return "fp.isNormal";
1036   case kind::FLOATINGPOINT_ISSN: return "fp.isSubnormal";
1037   case kind::FLOATINGPOINT_ISZ: return "fp.isZero";
1038   case kind::FLOATINGPOINT_ISINF: return "fp.isInfinite";
1039   case kind::FLOATINGPOINT_ISNAN: return "fp.isNaN";
1040   case kind::FLOATINGPOINT_ISNEG: return "fp.isNegative";
1041   case kind::FLOATINGPOINT_ISPOS: return "fp.isPositive";
1042
1043   case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: return "to_fp";
1044   case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: return "to_fp";
1045   case kind::FLOATINGPOINT_TO_FP_REAL: return "to_fp";
1046   case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: return "to_fp";
1047   case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: return "to_fp_unsigned";
1048   case kind::FLOATINGPOINT_TO_FP_GENERIC: return "to_fp_unsigned";
1049   case kind::FLOATINGPOINT_TO_UBV: return "fp.to_ubv";
1050   case kind::FLOATINGPOINT_TO_UBV_TOTAL: return "fp.to_ubv_total";
1051   case kind::FLOATINGPOINT_TO_SBV: return "fp.to_sbv";
1052   case kind::FLOATINGPOINT_TO_SBV_TOTAL: return "fp.to_sbv_total";
1053   case kind::FLOATINGPOINT_TO_REAL: return "fp.to_real";
1054   case kind::FLOATINGPOINT_TO_REAL_TOTAL: return "fp.to_real_total";
1055
1056   //string theory
1057   case kind::STRING_CONCAT: return "str.++";
1058   case kind::STRING_LENGTH: return v == z3str_variant ? "Length" : "str.len";
1059   case kind::STRING_SUBSTR: return "str.substr" ;
1060   case kind::STRING_STRCTN: return "str.contains" ;
1061   case kind::STRING_CHARAT: return "str.at" ;
1062   case kind::STRING_STRIDOF: return "str.indexof" ;
1063   case kind::STRING_STRREPL: return "str.replace" ;
1064   case kind::STRING_PREFIX: return "str.prefixof" ;
1065   case kind::STRING_SUFFIX: return "str.suffixof" ;
1066   case kind::STRING_LEQ: return "str.<=";
1067   case kind::STRING_LT: return "str.<";
1068   case kind::STRING_CODE: return "str.code";
1069   case kind::STRING_ITOS:
1070     return v == smt2_6_1_variant ? "str.from-int" : "int.to.str";
1071   case kind::STRING_STOI:
1072     return v == smt2_6_1_variant ? "str.to-int" : "str.to.int";
1073   case kind::STRING_IN_REGEXP:
1074     return v == smt2_6_1_variant ? "str.in-re" : "str.in.re";
1075   case kind::STRING_TO_REGEXP:
1076     return v == smt2_6_1_variant ? "str.to-re" : "str.to.re";
1077   case kind::REGEXP_CONCAT: return "re.++";
1078   case kind::REGEXP_UNION: return "re.union";
1079   case kind::REGEXP_INTER: return "re.inter";
1080   case kind::REGEXP_STAR: return "re.*";
1081   case kind::REGEXP_PLUS: return "re.+";
1082   case kind::REGEXP_OPT: return "re.opt";
1083   case kind::REGEXP_RANGE: return "re.range";
1084   case kind::REGEXP_LOOP: return "re.loop";
1085
1086   //sep theory
1087   case kind::SEP_STAR: return "sep";
1088   case kind::SEP_PTO: return "pto";
1089   case kind::SEP_WAND: return "wand";
1090   case kind::SEP_EMP: return "emp";
1091
1092   default:
1093     ; /* fall through */
1094   }
1095
1096   // no SMT way to print these
1097   return kind::kindToString(k);
1098 }
1099
1100 static void printBvParameterizedOp(std::ostream& out, TNode n)
1101 {
1102   out << "(_ ";
1103   switch(n.getKind()) {
1104   case kind::BITVECTOR_EXTRACT: {
1105     BitVectorExtract p = n.getOperator().getConst<BitVectorExtract>();
1106     out << "extract " << p.high << ' ' << p.low;
1107     break;
1108   }
1109   case kind::BITVECTOR_REPEAT:
1110     out << "repeat "
1111         << n.getOperator().getConst<BitVectorRepeat>().repeatAmount;
1112     break;
1113   case kind::BITVECTOR_ZERO_EXTEND:
1114     out << "zero_extend "
1115         << n.getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount;
1116     break;
1117   case kind::BITVECTOR_SIGN_EXTEND:
1118     out << "sign_extend "
1119         << n.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
1120     break;
1121   case kind::BITVECTOR_ROTATE_LEFT:
1122     out << "rotate_left "
1123         << n.getOperator().getConst<BitVectorRotateLeft>().rotateLeftAmount;
1124     break;
1125   case kind::BITVECTOR_ROTATE_RIGHT:
1126     out << "rotate_right "
1127         << n.getOperator().getConst<BitVectorRotateRight>().rotateRightAmount;
1128     break;
1129   case kind::INT_TO_BITVECTOR:
1130     out << "int2bv "
1131         << n.getOperator().getConst<IntToBitVector>().size;
1132     break;
1133   default:
1134     out << n.getKind();
1135   }
1136   out << ")";
1137 }
1138
1139 static void printFpParameterizedOp(std::ostream& out, TNode n)
1140 {
1141   out << "(_ ";
1142   switch(n.getKind()) {
1143   case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
1144     //out << "to_fp_bv "
1145     out << "to_fp "
1146         << n.getOperator().getConst<FloatingPointToFPIEEEBitVector>().t.exponent() << ' '
1147         << n.getOperator().getConst<FloatingPointToFPIEEEBitVector>().t.significand();
1148     break;
1149   case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT:
1150     //out << "to_fp_fp "
1151     out << "to_fp "
1152         << n.getOperator().getConst<FloatingPointToFPFloatingPoint>().t.exponent() << ' '
1153         << n.getOperator().getConst<FloatingPointToFPFloatingPoint>().t.significand();
1154     break;
1155   case kind::FLOATINGPOINT_TO_FP_REAL:
1156     //out << "to_fp_real "
1157     out << "to_fp "
1158         << n.getOperator().getConst<FloatingPointToFPReal>().t.exponent() << ' '
1159         << n.getOperator().getConst<FloatingPointToFPReal>().t.significand();
1160     break;
1161   case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
1162     //out << "to_fp_signed "
1163     out << "to_fp "
1164         << n.getOperator().getConst<FloatingPointToFPSignedBitVector>().t.exponent() << ' '
1165         << n.getOperator().getConst<FloatingPointToFPSignedBitVector>().t.significand();
1166     break;
1167   case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
1168     out << "to_fp_unsigned "
1169         << n.getOperator().getConst<FloatingPointToFPUnsignedBitVector>().t.exponent() << ' '
1170         << n.getOperator().getConst<FloatingPointToFPUnsignedBitVector>().t.significand();
1171     break;
1172   case kind::FLOATINGPOINT_TO_FP_GENERIC:
1173     out << "to_fp "
1174         << n.getOperator().getConst<FloatingPointToFPGeneric>().t.exponent() << ' '
1175         << n.getOperator().getConst<FloatingPointToFPGeneric>().t.significand();
1176     break;
1177   case kind::FLOATINGPOINT_TO_UBV:
1178     out << "fp.to_ubv "
1179         << n.getOperator().getConst<FloatingPointToUBV>().bvs.size;
1180     break;
1181   case kind::FLOATINGPOINT_TO_SBV:
1182     out << "fp.to_sbv "
1183         << n.getOperator().getConst<FloatingPointToSBV>().bvs.size;
1184     break;
1185   case kind::FLOATINGPOINT_TO_UBV_TOTAL:
1186     out << "fp.to_ubv_total "
1187         << n.getOperator().getConst<FloatingPointToUBVTotal>().bvs.size;
1188     break;
1189   case kind::FLOATINGPOINT_TO_SBV_TOTAL:
1190     out << "fp.to_sbv_total "
1191         << n.getOperator().getConst<FloatingPointToSBVTotal>().bvs.size;
1192     break;
1193   default:
1194     out << n.getKind();
1195   }
1196   out << ")";
1197 }
1198
1199 template <class T>
1200 static bool tryToStream(std::ostream& out, const Command* c);
1201 template <class T>
1202 static bool tryToStream(std::ostream& out, const Command* c, Variant v);
1203
1204 void Smt2Printer::toStream(std::ostream& out,
1205                            const Command* c,
1206                            int toDepth,
1207                            bool types,
1208                            size_t dag) const
1209 {
1210   expr::ExprSetDepth::Scope sdScope(out, toDepth);
1211   expr::ExprPrintTypes::Scope ptScope(out, types);
1212   expr::ExprDag::Scope dagScope(out, dag);
1213
1214   if (tryToStream<AssertCommand>(out, c) || tryToStream<PushCommand>(out, c)
1215       || tryToStream<PopCommand>(out, c)
1216       || tryToStream<CheckSatCommand>(out, c)
1217       || tryToStream<CheckSatAssumingCommand>(out, c)
1218       || tryToStream<QueryCommand>(out, c, d_variant)
1219       || tryToStream<ResetCommand>(out, c)
1220       || tryToStream<ResetAssertionsCommand>(out, c)
1221       || tryToStream<QuitCommand>(out, c)
1222       || tryToStream<DeclarationSequence>(out, c)
1223       || tryToStream<CommandSequence>(out, c)
1224       || tryToStream<DeclareFunctionCommand>(out, c)
1225       || tryToStream<DeclareTypeCommand>(out, c)
1226       || tryToStream<DefineTypeCommand>(out, c)
1227       || tryToStream<DefineNamedFunctionCommand>(out, c)
1228       || tryToStream<DefineFunctionCommand>(out, c)
1229       || tryToStream<DefineFunctionRecCommand>(out, c)
1230       || tryToStream<SimplifyCommand>(out, c)
1231       || tryToStream<GetValueCommand>(out, c)
1232       || tryToStream<GetModelCommand>(out, c)
1233       || tryToStream<GetAssignmentCommand>(out, c)
1234       || tryToStream<GetAssertionsCommand>(out, c)
1235       || tryToStream<GetProofCommand>(out, c)
1236       || tryToStream<GetUnsatAssumptionsCommand>(out, c)
1237       || tryToStream<GetUnsatCoreCommand>(out, c)
1238       || tryToStream<SetBenchmarkStatusCommand>(out, c, d_variant)
1239       || tryToStream<SetBenchmarkLogicCommand>(out, c, d_variant)
1240       || tryToStream<SetInfoCommand>(out, c, d_variant)
1241       || tryToStream<GetInfoCommand>(out, c)
1242       || tryToStream<SetOptionCommand>(out, c)
1243       || tryToStream<GetOptionCommand>(out, c)
1244       || tryToStream<DatatypeDeclarationCommand>(out, c, d_variant)
1245       || tryToStream<CommentCommand>(out, c, d_variant)
1246       || tryToStream<EmptyCommand>(out, c)
1247       || tryToStream<EchoCommand>(out, c, d_variant))
1248   {
1249     return;
1250   }
1251
1252   out << "ERROR: don't know how to print a Command of class: "
1253       << typeid(*c).name() << endl;
1254
1255 }/* Smt2Printer::toStream(Command*) */
1256
1257
1258 static std::string quoteSymbol(TNode n) {
1259   // #warning "check the old implementation. It seems off."
1260   std::stringstream ss;
1261   ss << language::SetLanguage(language::output::LANG_SMTLIB_V2_5);
1262   return CVC4::quoteSymbol(ss.str());
1263 }
1264
1265 template <class T>
1266 static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v);
1267
1268 void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const
1269 {
1270   if (tryToStream<CommandSuccess>(out, s, d_variant) ||
1271       tryToStream<CommandFailure>(out, s, d_variant) ||
1272       tryToStream<CommandRecoverableFailure>(out, s, d_variant) ||
1273       tryToStream<CommandUnsupported>(out, s, d_variant) ||
1274       tryToStream<CommandInterrupted>(out, s, d_variant)) {
1275     return;
1276   }
1277
1278   out << "ERROR: don't know how to print a CommandStatus of class: "
1279       << typeid(*s).name() << endl;
1280
1281 }/* Smt2Printer::toStream(CommandStatus*) */
1282
1283 void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core) const
1284 {
1285   out << "(" << std::endl;
1286   SmtEngine * smt = core.getSmtEngine();
1287   Assert( smt!=NULL );
1288   for(UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i) {
1289     std::string name;
1290     if (smt->getExpressionName(*i,name)) {
1291       // Named assertions always get printed
1292       out << maybeQuoteSymbol(name) << endl;
1293     } else if (options::dumpUnsatCoresFull()) {
1294       // Unnamed assertions only get printed if the option is set
1295       out << *i << endl;
1296     }
1297   }
1298   out << ")" << endl;
1299 }/* Smt2Printer::toStream(UnsatCore, map<Expr, string>) */
1300
1301 void Smt2Printer::toStream(std::ostream& out, const Model& m) const
1302 {
1303   //print the model comments
1304   std::stringstream c;
1305   m.getComments( c );
1306   std::string ln;
1307   while( std::getline( c, ln ) ){
1308     out << "; " << ln << std::endl;
1309   }
1310   //print the model
1311   out << "(model" << endl;
1312   this->Printer::toStream(out, m);
1313   out << ")" << endl;
1314   //print the heap model, if it exists
1315   Expr h, neq;
1316   if( m.getHeapModel( h, neq ) ){
1317     // description of the heap+what nil is equal to fully describes model
1318     out << "(heap" << endl;
1319     out << h << endl;
1320     out << neq << endl;
1321     out << ")" << std::endl;
1322   }
1323 }
1324
1325 namespace {
1326
1327 void DeclareTypeCommandToStream(std::ostream& out,
1328                                 const theory::TheoryModel& model,
1329                                 const DeclareTypeCommand& command,
1330                                 Variant variant)
1331 {
1332   TypeNode tn = TypeNode::fromType(command.getType());
1333   const std::vector<Node>* type_refs = model.getRepSet()->getTypeRepsOrNull(tn);
1334   if (options::modelUninterpDtEnum() && tn.isSort() && type_refs != nullptr)
1335   {
1336     if (isVariant_2_6(variant))
1337     {
1338       out << "(declare-datatypes ((" << command.getSymbol() << " 0)) (";
1339     }
1340     else
1341     {
1342       out << "(declare-datatypes () ((" << command.getSymbol() << " ";
1343     }
1344     for (Node type_ref : *type_refs)
1345     {
1346       out << "(" << type_ref << ")";
1347     }
1348     out << ")))" << endl;
1349   }
1350   else if (tn.isSort() && type_refs != nullptr)
1351   {
1352     // print the cardinality
1353     out << "; cardinality of " << tn << " is " << type_refs->size() << endl;
1354     out << command << endl;
1355     // print the representatives
1356     for (Node type_ref : *type_refs)
1357     {
1358       if (type_ref.isVar())
1359       {
1360         out << "(declare-fun " << quoteSymbol(type_ref) << " () " << tn << ")"
1361             << endl;
1362       }
1363       else
1364       {
1365         out << "; rep: " << type_ref << endl;
1366       }
1367     }
1368   }
1369   else
1370   {
1371     out << command << endl;
1372   }
1373 }
1374
1375 void DeclareFunctionCommandToStream(std::ostream& out,
1376                                     const theory::TheoryModel& model,
1377                                     const DeclareFunctionCommand& command)
1378 {
1379   Node n = Node::fromExpr(command.getFunction());
1380   if (command.getPrintInModelSetByUser())
1381   {
1382     if (!command.getPrintInModel())
1383     {
1384       return;
1385     }
1386   }
1387   else if (n.getKind() == kind::SKOLEM)
1388   {
1389     // don't print out internal stuff
1390     return;
1391   }
1392   Node val = Node::fromExpr(model.getSmtEngine()->getValue(n.toExpr()));
1393   if (val.getKind() == kind::LAMBDA)
1394   {
1395     out << "(define-fun " << n << " " << val[0] << " "
1396         << n.getType().getRangeType() << " " << val[1] << ")" << endl;
1397   }
1398   else
1399   {
1400     if (options::modelUninterpDtEnum() && val.getKind() == kind::STORE)
1401     {
1402       TypeNode tn = val[1].getType();
1403       const std::vector<Node>* type_refs =
1404           model.getRepSet()->getTypeRepsOrNull(tn);
1405       if (tn.isSort() && type_refs != nullptr)
1406       {
1407         Cardinality indexCard(type_refs->size());
1408         val = theory::arrays::TheoryArraysRewriter::normalizeConstant(
1409             val, indexCard);
1410       }
1411     }
1412     out << "(define-fun " << n << " () " << n.getType() << " ";
1413     if (val.getType().isInteger() && n.getType().isReal()
1414         && !n.getType().isInteger())
1415     {
1416       // toStreamReal(out, val, true);
1417       toStreamRational(out, val.getConst<Rational>(), true);
1418       // out << val << ".0";
1419     }
1420     else
1421     {
1422       out << val;
1423     }
1424     out << ")" << endl;
1425   }
1426 }
1427
1428 }  // namespace
1429
1430 void Smt2Printer::toStream(std::ostream& out,
1431                            const Model& model,
1432                            const Command* command) const
1433 {
1434   const theory::TheoryModel* theory_model =
1435       dynamic_cast<const theory::TheoryModel*>(&model);
1436   AlwaysAssert(theory_model != nullptr);
1437   if (const DeclareTypeCommand* dtc =
1438           dynamic_cast<const DeclareTypeCommand*>(command))
1439   {
1440     DeclareTypeCommandToStream(out, *theory_model, *dtc, d_variant);
1441   }
1442   else if (const DeclareFunctionCommand* dfc =
1443                dynamic_cast<const DeclareFunctionCommand*>(command))
1444   {
1445     DeclareFunctionCommandToStream(out, *theory_model, *dfc);
1446   }
1447   else if (const DatatypeDeclarationCommand* datatype_declaration_command =
1448                dynamic_cast<const DatatypeDeclarationCommand*>(command))
1449   {
1450     toStream(out, datatype_declaration_command, -1, false, 1);
1451   }
1452   else
1453   {
1454     Unreachable();
1455   }
1456 }
1457
1458 void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const
1459 {
1460   if (n.getKind() == kind::APPLY_CONSTRUCTOR)
1461   {
1462     TypeNode tn = n.getType();
1463     const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
1464     if (dt.isSygus())
1465     {
1466       int cIndex = Datatype::indexOf(n.getOperator().toExpr());
1467       Assert(!dt[cIndex].getSygusOp().isNull());
1468       SygusPrintCallback* spc = dt[cIndex].getSygusPrintCallback().get();
1469       if (spc != nullptr && options::sygusPrintCallbacks())
1470       {
1471         spc->toStreamSygus(this, out, n.toExpr());
1472       }
1473       else
1474       {
1475         if (n.getNumChildren() > 0)
1476         {
1477           out << "(";
1478         }
1479         out << dt[cIndex].getSygusOp();
1480         if (n.getNumChildren() > 0)
1481         {
1482           for (Node nc : n)
1483           {
1484             out << " ";
1485             toStreamSygus(out, nc);
1486           }
1487           out << ")";
1488         }
1489       }
1490       return;
1491     }
1492   }
1493   else
1494   {
1495     Node p = n.getAttribute(theory::SygusPrintProxyAttribute());
1496     if (!p.isNull())
1497     {
1498       out << p;
1499     }
1500     else
1501     {
1502       // cannot convert term to analog, print original
1503       out << n;
1504     }
1505   }
1506 }
1507
1508 static void toStream(std::ostream& out, const AssertCommand* c)
1509 {
1510   out << "(assert " << c->getExpr() << ")";
1511 }
1512
1513 static void toStream(std::ostream& out, const PushCommand* c)
1514 {
1515   out << "(push 1)";
1516 }
1517
1518 static void toStream(std::ostream& out, const PopCommand* c)
1519 {
1520   out << "(pop 1)";
1521 }
1522
1523 static void toStream(std::ostream& out, const CheckSatCommand* c)
1524 {
1525   Expr e = c->getExpr();
1526   if(!e.isNull() && !(e.getKind() == kind::CONST_BOOLEAN && e.getConst<bool>())) {
1527     out << PushCommand() << endl
1528         << AssertCommand(e) << endl
1529         << CheckSatCommand() << endl
1530         << PopCommand();
1531   } else {
1532     out << "(check-sat)";
1533   }
1534 }
1535
1536 static void toStream(std::ostream& out, const CheckSatAssumingCommand* c)
1537 {
1538   out << "(check-sat-assuming ( ";
1539   const vector<Expr>& terms = c->getTerms();
1540   copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, " "));
1541   out << "))";
1542 }
1543
1544 static void toStream(std::ostream& out, const QueryCommand* c, Variant v)
1545 {
1546   Expr e = c->getExpr();
1547   if(!e.isNull()) {
1548     if (v == smt2_0_variant)
1549     {
1550       out << PushCommand() << endl
1551           << AssertCommand(BooleanSimplification::negate(e)) << endl
1552           << CheckSatCommand() << endl
1553           << PopCommand();
1554     }
1555     else
1556     {
1557       out << CheckSatAssumingCommand(e.notExpr()) << endl;
1558     }
1559   } else {
1560     out << "(check-sat)";
1561   }
1562 }
1563
1564 static void toStream(std::ostream& out, const ResetCommand* c)
1565 {
1566   out << "(reset)";
1567 }
1568
1569 static void toStream(std::ostream& out, const ResetAssertionsCommand* c)
1570 {
1571   out << "(reset-assertions)";
1572 }
1573
1574 static void toStream(std::ostream& out, const QuitCommand* c)
1575 {
1576   out << "(exit)";
1577 }
1578
1579 static void toStream(std::ostream& out, const CommandSequence* c)
1580 {
1581   CommandSequence::const_iterator i = c->begin();
1582   if(i != c->end()) {
1583     for(;;) {
1584       out << *i;
1585       if(++i != c->end()) {
1586         out << endl;
1587       } else {
1588         break;
1589       }
1590     }
1591   }
1592 }
1593
1594 static void toStream(std::ostream& out, const DeclareFunctionCommand* c)
1595 {
1596   Type type = c->getType();
1597   out << "(declare-fun " << CVC4::quoteSymbol(c->getSymbol()) << " (";
1598   if(type.isFunction()) {
1599     FunctionType ft = type;
1600     const vector<Type> argTypes = ft.getArgTypes();
1601     if(argTypes.size() > 0) {
1602       copy( argTypes.begin(), argTypes.end() - 1,
1603             ostream_iterator<Type>(out, " ") );
1604       out << argTypes.back();
1605     }
1606     type = ft.getRangeType();
1607   }
1608
1609   out << ") " << type << ")";
1610 }
1611
1612 static void toStream(std::ostream& out, const DefineFunctionCommand* c)
1613 {
1614   Expr func = c->getFunction();
1615   const vector<Expr>* formals = &c->getFormals();
1616   out << "(define-fun " << func << " (";
1617   Type type = func.getType();
1618   Expr formula = c->getFormula();
1619   if(type.isFunction()) {
1620     vector<Expr> f;
1621     if(formals->empty()) {
1622       const vector<Type>& params = FunctionType(type).getArgTypes();
1623       for(vector<Type>::const_iterator j = params.begin(); j != params.end(); ++j) {
1624         f.push_back(NodeManager::currentNM()->mkSkolem("a", TypeNode::fromType(*j), "",
1625                                                        NodeManager::SKOLEM_NO_NOTIFY).toExpr());
1626       }
1627       formula = NodeManager::currentNM()->toExprManager()->mkExpr(kind::APPLY_UF, formula, f);
1628       formals = &f;
1629     }
1630     vector<Expr>::const_iterator i = formals->begin();
1631     for(;;) {
1632       out << "(" << (*i) << " " << (*i).getType() << ")";
1633       ++i;
1634       if(i != formals->end()) {
1635         out << " ";
1636       } else {
1637         break;
1638       }
1639     }
1640     type = FunctionType(type).getRangeType();
1641   }
1642   out << ") " << type << " " << formula << ")";
1643 }
1644
1645 static void toStream(std::ostream& out, const DefineFunctionRecCommand* c)
1646 {
1647   const vector<Expr>& funcs = c->getFunctions();
1648   const vector<vector<Expr> >& formals = c->getFormals();
1649   out << "(define-fun";
1650   if (funcs.size() > 1)
1651   {
1652     out << "s";
1653   }
1654   out << "-rec ";
1655   if (funcs.size() > 1)
1656   {
1657     out << "(";
1658   }
1659   for (unsigned i = 0, size = funcs.size(); i < size; i++)
1660   {
1661     if (funcs.size() > 1)
1662     {
1663       if (i > 0)
1664       {
1665         out << " ";
1666       }
1667       out << "(";
1668     }
1669     out << funcs[i] << " (";
1670     // print its type signature
1671     vector<Expr>::const_iterator itf = formals[i].begin();
1672     for (;;)
1673     {
1674       out << "(" << (*itf) << " " << (*itf).getType() << ")";
1675       ++itf;
1676       if (itf != formals[i].end())
1677       {
1678         out << " ";
1679       }
1680       else
1681       {
1682         break;
1683       }
1684     }
1685     Type type = funcs[i].getType();
1686     type = static_cast<FunctionType>(type).getRangeType();
1687     out << ") " << type;
1688     if (funcs.size() > 1)
1689     {
1690       out << ")";
1691     }
1692   }
1693   if (funcs.size() > 1)
1694   {
1695     out << ") (";
1696   }
1697   const vector<Expr>& formulas = c->getFormulas();
1698   for (unsigned i = 0, size = formulas.size(); i < size; i++)
1699   {
1700     if (i > 0)
1701     {
1702       out << " ";
1703     }
1704     out << formulas[i];
1705   }
1706   if (funcs.size() > 1)
1707   {
1708     out << ")";
1709   }
1710   out << ")";
1711 }
1712
1713 static void toStreamRational(std::ostream& out, const Rational& r, bool decimal)
1714 {
1715   bool neg = r.sgn() < 0;
1716
1717   // TODO:
1718   // We are currently printing (- (/ 5 3))
1719   // instead of (/ (- 5) 3) which is what is in the SMT-LIB value in the theory definition.
1720   // Before switching, I'll keep to what was there and send an email.
1721
1722   // Tim: Apologies for the ifs on one line but in this case they are cleaner.
1723
1724   if (neg) { out << "(- "; }
1725
1726   if(r.isIntegral()) {
1727     if (neg) {
1728       out << (-r);
1729     }else {
1730       out << r;
1731     }
1732     if (decimal) { out << ".0"; }
1733   }else{
1734     out << "(/ ";
1735     if(neg) {
1736       Rational abs_r = (-r);
1737       out << abs_r.getNumerator();
1738       if(decimal) { out << ".0"; }
1739       out << ' ' << abs_r.getDenominator();
1740       if(decimal) { out << ".0"; }
1741     }else{
1742       out << r.getNumerator();
1743       if(decimal) { out << ".0"; }
1744       out << ' ' << r.getDenominator();
1745       if(decimal) { out << ".0"; }
1746     }
1747     out << ')';
1748   }
1749
1750   if (neg) { out << ')';}
1751
1752   // if(r < 0) {
1753   //   Rational abs_r = -r;
1754   //   if(r.isIntegral()) {
1755   //     out << "(- " << abs_r << ')';
1756   //   } else {
1757   //     out << "(- (/ " << (-r).getNumerator() << ' ' << (-r).getDenominator() << "))";
1758   //   }
1759   // } else {
1760   //   if(r.isIntegral()) {
1761   //         out << r;
1762   //       } else {
1763   //         out << "(/ " << r.getNumerator() << ' ' << r.getDenominator() << ')';
1764   //       }
1765   //     }
1766 }
1767
1768 static void toStream(std::ostream& out, const DeclareTypeCommand* c)
1769 {
1770   out << "(declare-sort " << c->getSymbol() << " " << c->getArity() << ")";
1771 }
1772
1773 static void toStream(std::ostream& out, const DefineTypeCommand* c)
1774 {
1775   const vector<Type>& params = c->getParameters();
1776   out << "(define-sort " << c->getSymbol() << " (";
1777   if(params.size() > 0) {
1778     copy( params.begin(), params.end() - 1,
1779           ostream_iterator<Type>(out, " ") );
1780     out << params.back();
1781   }
1782   out << ") " << c->getType() << ")";
1783 }
1784
1785 static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c)
1786 {
1787   out << "DefineNamedFunction( ";
1788   toStream(out, static_cast<const DefineFunctionCommand*>(c));
1789   out << " )";
1790
1791   out << "ERROR: don't know how to output define-named-function command" << endl;
1792 }
1793
1794 static void toStream(std::ostream& out, const SimplifyCommand* c)
1795 {
1796   out << "(simplify " << c->getTerm() << ")";
1797 }
1798
1799 static void toStream(std::ostream& out, const GetValueCommand* c)
1800 {
1801   out << "(get-value ( ";
1802   const vector<Expr>& terms = c->getTerms();
1803   copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, " "));
1804   out << "))";
1805 }
1806
1807 static void toStream(std::ostream& out, const GetModelCommand* c)
1808 {
1809   out << "(get-model)";
1810 }
1811
1812 static void toStream(std::ostream& out, const GetAssignmentCommand* c)
1813 {
1814   out << "(get-assignment)";
1815 }
1816
1817 static void toStream(std::ostream& out, const GetAssertionsCommand* c)
1818 {
1819   out << "(get-assertions)";
1820 }
1821
1822 static void toStream(std::ostream& out, const GetProofCommand* c)
1823 {
1824   out << "(get-proof)";
1825 }
1826
1827 static void toStream(std::ostream& out, const GetUnsatAssumptionsCommand* c)
1828 {
1829   out << "(get-unsat-assumptions)";
1830 }
1831
1832 static void toStream(std::ostream& out, const GetUnsatCoreCommand* c)
1833 {
1834   out << "(get-unsat-core)";
1835 }
1836
1837 static void toStream(std::ostream& out,
1838                      const SetBenchmarkStatusCommand* c,
1839                      Variant v)
1840 {
1841   if(v == z3str_variant || v == smt2_0_variant) {
1842     out << "(set-info :status " << c->getStatus() << ")";
1843   } else {
1844     out << "(meta-info :status " << c->getStatus() << ")";
1845   }
1846 }
1847
1848 static void toStream(std::ostream& out,
1849                      const SetBenchmarkLogicCommand* c,
1850                      Variant v)
1851 {
1852   // Z3-str doesn't have string-specific logic strings(?), so comment it
1853   if(v == z3str_variant) {
1854     out << "; (set-logic " << c->getLogic() << ")";
1855   } else {
1856     out << "(set-logic " << c->getLogic() << ")";
1857   }
1858 }
1859
1860 static void toStream(std::ostream& out, const SetInfoCommand* c, Variant v)
1861 {
1862   if(v == z3str_variant || v == smt2_0_variant) {
1863     out << "(set-info :" << c->getFlag() << " ";
1864   } else {
1865     out << "(meta-info :" << c->getFlag() << " ";
1866   }
1867
1868   SExpr::toStream(out, c->getSExpr(), variantToLanguage(v));
1869   out << ")";
1870 }
1871
1872 static void toStream(std::ostream& out, const GetInfoCommand* c)
1873 {
1874   out << "(get-info :" << c->getFlag() << ")";
1875 }
1876
1877 static void toStream(std::ostream& out, const SetOptionCommand* c)
1878 {
1879   out << "(set-option :" << c->getFlag() << " ";
1880   SExpr::toStream(out, c->getSExpr(), language::output::LANG_SMTLIB_V2_5);
1881   out << ")";
1882 }
1883
1884 static void toStream(std::ostream& out, const GetOptionCommand* c)
1885 {
1886   out << "(get-option :" << c->getFlag() << ")";
1887 }
1888
1889 static void toStream(std::ostream& out, const Datatype & d) {
1890   for(Datatype::const_iterator ctor = d.begin(), ctor_end = d.end();
1891       ctor != ctor_end; ++ctor){
1892     if( ctor!=d.begin() ) out << " ";
1893     out << "(" << maybeQuoteSymbol(ctor->getName());
1894
1895     for(DatatypeConstructor::const_iterator arg = ctor->begin(), arg_end = ctor->end();
1896         arg != arg_end; ++arg){
1897       out << " (" << arg->getSelector() << " "
1898           << static_cast<SelectorType>(arg->getType()).getRangeType() << ")";
1899     }
1900     out << ")";
1901   }
1902 }
1903
1904 static void toStream(std::ostream& out,
1905                      const DatatypeDeclarationCommand* c,
1906                      Variant v)
1907 {
1908   const vector<DatatypeType>& datatypes = c->getDatatypes();
1909   Assert(!datatypes.empty());
1910   if (datatypes[0].getDatatype().isTuple())
1911   {
1912     // not necessary to print tuples
1913     Assert(datatypes.size() == 1);
1914     return;
1915   }
1916   out << "(declare-";
1917   if (datatypes[0].getDatatype().isCodatatype())
1918   {
1919     out << "co";
1920   }
1921   out << "datatypes";
1922   if (isVariant_2_6(v))
1923   {
1924     out << " (";
1925     for (vector<DatatypeType>::const_iterator i = datatypes.begin(),
1926                                               i_end = datatypes.end();
1927          i != i_end;
1928          ++i)
1929     {
1930       const Datatype& d = i->getDatatype();
1931       out << "(" << maybeQuoteSymbol(d.getName());
1932       out << " " << d.getNumParameters() << ")";
1933     }
1934     out << ") (";
1935     for (vector<DatatypeType>::const_iterator i = datatypes.begin(),
1936                                               i_end = datatypes.end();
1937          i != i_end;
1938          ++i)
1939     {
1940       const Datatype& d = i->getDatatype();
1941       out << "(";
1942       toStream(out, d);
1943       out << ")" << endl;
1944     }
1945     out << ")";
1946   }
1947   else
1948   {
1949     out << " () (";
1950     for (vector<DatatypeType>::const_iterator i = datatypes.begin(),
1951                                               i_end = datatypes.end();
1952          i != i_end;
1953          ++i)
1954     {
1955       const Datatype& d = i->getDatatype();
1956       out << "(" << maybeQuoteSymbol(d.getName()) << " ";
1957       toStream(out, d);
1958       out << ")" << endl;
1959     }
1960     out << ")";
1961   }
1962   out << ")";
1963 }
1964
1965 static void toStream(std::ostream& out, const CommentCommand* c, Variant v)
1966 {
1967   string s = c->getComment();
1968   size_t pos = 0;
1969   while((pos = s.find_first_of('"', pos)) != string::npos) {
1970     s.replace(pos, 1, (v == z3str_variant || v == smt2_0_variant) ? "\\\"" : "\"\"");
1971     pos += 2;
1972   }
1973   out << "(set-info :notes \"" << s << "\")";
1974 }
1975
1976 static void toStream(std::ostream& out, const EmptyCommand* c) {}
1977
1978 static void toStream(std::ostream& out, const EchoCommand* c, Variant v)
1979 {
1980   std::string s = c->getOutput();
1981   // escape all double-quotes
1982   size_t pos = 0;
1983   while((pos = s.find('"', pos)) != string::npos) {
1984     s.replace(pos, 1, (v == z3str_variant || v == smt2_0_variant) ? "\\\"" : "\"\"");
1985     pos += 2;
1986   }
1987   out << "(echo \"" << s << "\")";
1988 }
1989
1990 template <class T>
1991 static bool tryToStream(std::ostream& out, const Command* c)
1992 {
1993   if(typeid(*c) == typeid(T)) {
1994     toStream(out, dynamic_cast<const T*>(c));
1995     return true;
1996   }
1997   return false;
1998 }
1999
2000 template <class T>
2001 static bool tryToStream(std::ostream& out, const Command* c, Variant v)
2002 {
2003   if(typeid(*c) == typeid(T)) {
2004     toStream(out, dynamic_cast<const T*>(c), v);
2005     return true;
2006   }
2007   return false;
2008 }
2009
2010 static void toStream(std::ostream& out, const CommandSuccess* s, Variant v)
2011 {
2012   if(Command::printsuccess::getPrintSuccess(out)) {
2013     out << "success" << endl;
2014   }
2015 }
2016
2017 static void toStream(std::ostream& out, const CommandInterrupted* s, Variant v)
2018 {
2019   out << "interrupted" << endl;
2020 }
2021
2022 static void toStream(std::ostream& out, const CommandUnsupported* s, Variant v)
2023 {
2024 #ifdef CVC4_COMPETITION_MODE
2025   // if in competition mode, lie and say we're ok
2026   // (we have nothing to lose by saying success, and everything to lose
2027   // if we say "unsupported")
2028   out << "success" << endl;
2029 #else /* CVC4_COMPETITION_MODE */
2030   out << "unsupported" << endl;
2031 #endif /* CVC4_COMPETITION_MODE */
2032 }
2033
2034 static void errorToStream(std::ostream& out, std::string message, Variant v) {
2035   // escape all double-quotes
2036   size_t pos = 0;
2037   while((pos = message.find('"', pos)) != string::npos) {
2038     message.replace(pos, 1, (v == z3str_variant || v == smt2_0_variant) ? "\\\"" : "\"\"");
2039     pos += 2;
2040   }
2041   out << "(error \"" << message << "\")" << endl;
2042 }
2043
2044 static void toStream(std::ostream& out, const CommandFailure* s, Variant v) {
2045   errorToStream(out, s->getMessage(), v);
2046 }
2047
2048 static void toStream(std::ostream& out, const CommandRecoverableFailure* s,
2049                      Variant v) {
2050   errorToStream(out, s->getMessage(), v);
2051 }
2052
2053 template <class T>
2054 static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v)
2055 {
2056   if(typeid(*s) == typeid(T)) {
2057     toStream(out, dynamic_cast<const T*>(s), v);
2058     return true;
2059   }
2060   return false;
2061 }
2062
2063 static OutputLanguage variantToLanguage(Variant variant)
2064 {
2065   switch(variant) {
2066   case smt2_0_variant:
2067     return language::output::LANG_SMTLIB_V2_0;
2068   case z3str_variant:
2069     return language::output::LANG_Z3STR;
2070   case sygus_variant:
2071     return language::output::LANG_SYGUS;
2072   case no_variant:
2073   default:
2074     return language::output::LANG_SMTLIB_V2_5;
2075   }
2076 }
2077
2078 }/* CVC4::printer::smt2 namespace */
2079 }/* CVC4::printer namespace */
2080 }/* CVC4 namespace */