src/printer/smt2/smt2_printer.cpp

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