src/printer/smt2/smt2_printer.cpp

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