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