src/printer/smt2/smt2_printer.cpp

   1 /*********************                                                        */
   2 /*! \file smt2_printer.cpp
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: Andrew Reynolds
   6  ** Minor contributors (to current version): Dejan Jovanovic, Tim King, Liana Hadarean, Francois Bobot
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief The pretty-printer interface for the SMT2 output language
  13  **
  14  ** The pretty-printer interface for the SMT2 output language.
  15  **/
  16
  17 #include "printer/smt2/smt2_printer.h"
  18
  19 #include <iostream>
  20 #include <vector>
  21 #include <string>
  22 #include <typeinfo>
  23
  24 #include "util/boolean_simplification.h"
  25 #include "printer/dagification_visitor.h"
  26 #include "util/node_visitor.h"
  27 #include "theory/substitutions.h"
  28 #include "util/language.h"
  29 #include "smt/smt_engine.h"
  30 #include "smt/options.h"
  31 #include "expr/node_manager_attributes.h"
  32
  33 #include "theory/theory_model.h"
  34 #include "theory/arrays/theory_arrays_rewriter.h"
  35
  36 using namespace std;
  37
  38 namespace CVC4 {
  39 namespace printer {
  40 namespace smt2 {
  41
  42 static string smtKindString(Kind k) throw();
  43
  44 static void printBvParameterizedOp(std::ostream& out, TNode n) throw();
  45
  46 void Smt2Printer::toStream(std::ostream& out, TNode n,
  47                            int toDepth, bool types, size_t dag) const throw() {
  48   if(dag != 0) {
  49     DagificationVisitor dv(dag);
  50     NodeVisitor<DagificationVisitor> visitor;
  51     visitor.run(dv, n);
  52     const theory::SubstitutionMap& lets = dv.getLets();
  53     if(!lets.empty()) {
  54       theory::SubstitutionMap::const_iterator i = lets.begin();
  55       theory::SubstitutionMap::const_iterator i_end = lets.end();
  56       for(; i != i_end; ++ i) {
  57         out << "(let ((";
  58         toStream(out, (*i).second, toDepth, types);
  59         out << ' ';
  60         toStream(out, (*i).first, toDepth, types);
  61         out << ")) ";
  62       }
  63     }
  64     Node body = dv.getDagifiedBody();
  65     toStream(out, body, toDepth, types);
  66     if(!lets.empty()) {
  67       theory::SubstitutionMap::const_iterator i = lets.begin();
  68       theory::SubstitutionMap::const_iterator i_end = lets.end();
  69       for(; i != i_end; ++ i) {
  70         out << ")";
  71       }
  72     }
  73   } else {
  74     toStream(out, n, toDepth, types);
  75   }
  76 }
  77
  78 static std::string maybeQuoteSymbol(const std::string& s) {
  79   // this is the set of SMT-LIBv2 permitted characters in "simple" (non-quoted) symbols
  80   if(s.find_first_not_of("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789~!@$%^&*_-+=<>.?/") != string::npos) {
  81     // need to quote it
  82     stringstream ss;
  83     ss << '|' << s << '|';
  84     return ss.str();
  85   }
  86   return s;
  87 }
  88
  89 void Smt2Printer::toStream(std::ostream& out, TNode n,
  90                            int toDepth, bool types) const throw() {
  91   // null
  92   if(n.getKind() == kind::NULL_EXPR) {
  93     out << "null";
  94     return;
  95   }
  96
  97   // variable
  98   if(n.isVar()) {
  99     string s;
 100     if(n.getAttribute(expr::VarNameAttr(), s)) {
 101       out << maybeQuoteSymbol(s);
 102     } else {
 103       if(n.getKind() == kind::VARIABLE) {
 104         out << "var_";
 105       } else {
 106         out << n.getKind() << '_';
 107       }
 108       out << n.getId();
 109     }
 110     if(types) {
 111       // print the whole type, but not *its* type
 112       out << ":";
 113       n.getType().toStream(out, language::output::LANG_SMTLIB_V2);
 114     }
 115
 116     return;
 117   }
 118
 119   // constant
 120   if(n.getMetaKind() == kind::metakind::CONSTANT) {
 121     switch(n.getKind()) {
 122     case kind::TYPE_CONSTANT:
 123       switch(n.getConst<TypeConstant>()) {
 124       case BOOLEAN_TYPE: out << "Bool"; break;
 125       case REAL_TYPE: out << "Real"; break;
 126       case INTEGER_TYPE: out << "Int"; break;
 127       default:
 128         // fall back on whatever operator<< does on underlying type; we
 129         // might luck out and be SMT-LIB v2 compliant
 130         kind::metakind::NodeValueConstPrinter::toStream(out, n);
 131       }
 132       break;
 133     case kind::BITVECTOR_TYPE:
 134       out << "(_ BitVec " << n.getConst<BitVectorSize>().size << ")";
 135       break;
 136     case kind::CONST_BITVECTOR: {
 137       const BitVector& bv = n.getConst<BitVector>();
 138       const Integer& x = bv.getValue();
 139       unsigned n = bv.getSize();
 140       out << "(_ ";
 141       out << "bv" << x <<" " << n;
 142       out << ")";
 143       // //out << "#b";
 144
 145       // while(n-- > 0) {
 146       //   out << (x.testBit(n) ? '1' : '0');
 147       // }
 148       break;
 149     }
 150     case kind::CONST_BOOLEAN:
 151       // the default would print "1" or "0" for bool, that's not correct
 152       // for our purposes
 153       out << (n.getConst<bool>() ? "true" : "false");
 154       break;
 155     case kind::BUILTIN:
 156       out << smtKindString(n.getConst<Kind>());
 157       break;
 158     case kind::CONST_RATIONAL: {
 159       Rational r = n.getConst<Rational>();
 160       if(r < 0) {
 161         if(r.isIntegral()) {
 162           out << "(- " << -r << ')';
 163         } else {
 164           out << "(- (/ " << (-r).getNumerator() << ' ' << (-r).getDenominator() << "))";
 165         }
 166       } else {
 167         if(r.isIntegral()) {
 168           out << r;
 169         } else {
 170           out << "(/ " << r.getNumerator() << ' ' << r.getDenominator() << ')';
 171         }
 172       }
 173       break;
 174     }
 175
 176     case kind::STORE_ALL: {
 177       ArrayStoreAll asa = n.getConst<ArrayStoreAll>();
 178       out << "(__array_store_all__ " << asa.getType() << " " << asa.getExpr() << ")";
 179       break;
 180     }
 181
 182     case kind::SUBRANGE_TYPE: {
 183       const SubrangeBounds& bounds = n.getConst<SubrangeBounds>();
 184       // No way to represent subranges in SMT-LIBv2; this is inspired
 185       // by yices format (but isn't identical to it).
 186       out << "(subrange " << bounds.lower << ' ' << bounds.upper << ')';
 187       break;
 188     }
 189     case kind::SUBTYPE_TYPE:
 190       // No way to represent predicate subtypes in SMT-LIBv2; this is
 191       // inspired by yices format (but isn't identical to it).
 192       out << "(subtype " << n.getConst<Predicate>() << ')';
 193       break;
 194
 195     case kind::DATATYPE_TYPE:
 196       out << maybeQuoteSymbol(n.getConst<Datatype>().getName());
 197       break;
 198
 199     case kind::UNINTERPRETED_CONSTANT: {
 200       const UninterpretedConstant& uc = n.getConst<UninterpretedConstant>();
 201       out << '@' << uc;
 202       break;
 203     }
 204
 205     default:
 206       // fall back on whatever operator<< does on underlying type; we
 207       // might luck out and be SMT-LIB v2 compliant
 208       kind::metakind::NodeValueConstPrinter::toStream(out, n);
 209     }
 210
 211     return;
 212   }
 213
 214   if(n.getKind() == kind::SORT_TYPE) {
 215     string name;
 216     if(n.getAttribute(expr::VarNameAttr(), name)) {
 217       out << maybeQuoteSymbol(name);
 218       return;
 219     }
 220   }
 221
 222   bool stillNeedToPrintParams = true;
 223   // operator
 224   if(n.getNumChildren() != 0 && n.getKind()!=kind::INST_PATTERN_LIST) out << '(';
 225   switch(Kind k = n.getKind()) {
 226     // builtin theory
 227   case kind::APPLY: break;
 228   case kind::EQUAL:
 229   case kind::DISTINCT: out << smtKindString(k) << " "; break;
 230   case kind::CHAIN: break;
 231   case kind::TUPLE: break;
 232   case kind::SEXPR: break;
 233
 234     // bool theory
 235   case kind::NOT:
 236   case kind::AND:
 237   case kind::IFF:
 238   case kind::IMPLIES:
 239   case kind::OR:
 240   case kind::XOR:
 241   case kind::ITE: out << smtKindString(k) << " "; break;
 242
 243     // uf theory
 244   case kind::APPLY_UF: break;
 245
 246     // arith theory
 247   case kind::PLUS:
 248   case kind::MULT:
 249   case kind::MINUS:
 250   case kind::UMINUS:
 251   case kind::LT:
 252   case kind::LEQ:
 253   case kind::GT:
 254   case kind::GEQ:
 255   case kind::DIVISION:
 256   case kind::DIVISION_TOTAL:
 257   case kind::INTS_DIVISION:
 258   case kind::INTS_DIVISION_TOTAL:
 259   case kind::INTS_MODULUS:
 260   case kind::INTS_MODULUS_TOTAL:
 261   case kind::ABS:
 262   case kind::IS_INTEGER:
 263   case kind::TO_INTEGER:
 264   case kind::TO_REAL: out << smtKindString(k) << " "; break;
 265
 266   case kind::DIVISIBLE:
 267     out << "(_ divisible " << n.getOperator().getConst<Divisible>().k << ")";
 268     stillNeedToPrintParams = false;
 269     break;
 270
 271     // arrays theory
 272   case kind::SELECT:
 273   case kind::STORE:
 274   case kind::ARRAY_TYPE: out << smtKindString(k) << " "; break;
 275
 276   // string theory
 277   case kind::STRING_CONCAT: out << "str.++ "; break;
 278   case kind::STRING_IN_REGEXP: out << "str.in.re "; break;
 279   case kind::STRING_LENGTH: out << "str.len "; break;
 280   case kind::STRING_SUBSTR: out << "str.substr "; break;
 281   case kind::STRING_STRCTN: out << "str.contain "; break;
 282   case kind::STRING_CHARAT: out << "str.at "; break;
 283   case kind::STRING_STRIDOF: out << "str.indexof "; break;
 284   case kind::STRING_STRREPL: out << "str.replace "; break;
 285   case kind::STRING_TO_REGEXP: out << "str.to.re "; break;
 286   case kind::REGEXP_CONCAT: out << "re.++ "; break;
 287   case kind::REGEXP_OR: out << "re.or "; break;
 288   case kind::REGEXP_INTER: out << "re.itr "; break;
 289   case kind::REGEXP_STAR: out << "re.* "; break;
 290   case kind::REGEXP_PLUS: out << "re.+ "; break;
 291   case kind::REGEXP_OPT: out << "re.opt "; break;
 292   case kind::REGEXP_RANGE: out << "re.range "; break;
 293
 294     // bv theory
 295   case kind::BITVECTOR_CONCAT: out << "concat "; break;
 296   case kind::BITVECTOR_AND: out << "bvand "; break;
 297   case kind::BITVECTOR_OR: out << "bvor "; break;
 298   case kind::BITVECTOR_XOR: out << "bvxor "; break;
 299   case kind::BITVECTOR_NOT: out << "bvnot "; break;
 300   case kind::BITVECTOR_NAND: out << "bvnand "; break;
 301   case kind::BITVECTOR_NOR: out << "bvnor "; break;
 302   case kind::BITVECTOR_XNOR: out << "bvxnor "; break;
 303   case kind::BITVECTOR_COMP: out << "bvcomp "; break;
 304   case kind::BITVECTOR_MULT: out << "bvmul "; break;
 305   case kind::BITVECTOR_PLUS: out << "bvadd "; break;
 306   case kind::BITVECTOR_SUB: out << "bvsub "; break;
 307   case kind::BITVECTOR_NEG: out << "bvneg "; break;
 308   case kind::BITVECTOR_UDIV: out << "bvudiv "; break;
 309   case kind::BITVECTOR_UDIV_TOTAL: out << "bvudiv_total "; break;
 310   case kind::BITVECTOR_UREM: out << "bvurem "; break;
 311   case kind::BITVECTOR_UREM_TOTAL: out << "bvurem_total "; break;
 312   case kind::BITVECTOR_SDIV: out << "bvsdiv "; break;
 313   case kind::BITVECTOR_SREM: out << "bvsrem "; break;
 314   case kind::BITVECTOR_SMOD: out << "bvsmod "; break;
 315   case kind::BITVECTOR_SHL: out << "bvshl "; break;
 316   case kind::BITVECTOR_LSHR: out << "bvlshr "; break;
 317   case kind::BITVECTOR_ASHR: out << "bvashr "; break;
 318   case kind::BITVECTOR_ULT: out << "bvult "; break;
 319   case kind::BITVECTOR_ULE: out << "bvule "; break;
 320   case kind::BITVECTOR_UGT: out << "bvugt "; break;
 321   case kind::BITVECTOR_UGE: out << "bvuge "; break;
 322   case kind::BITVECTOR_SLT: out << "bvslt "; break;
 323   case kind::BITVECTOR_SLE: out << "bvsle "; break;
 324   case kind::BITVECTOR_SGT: out << "bvsgt "; break;
 325   case kind::BITVECTOR_SGE: out << "bvsge "; break;
 326   case kind::BITVECTOR_TO_NAT: out << "bv2nat "; break;
 327
 328   case kind::BITVECTOR_EXTRACT:
 329   case kind::BITVECTOR_REPEAT:
 330   case kind::BITVECTOR_ZERO_EXTEND:
 331   case kind::BITVECTOR_SIGN_EXTEND:
 332   case kind::BITVECTOR_ROTATE_LEFT:
 333   case kind::BITVECTOR_ROTATE_RIGHT:
 334   case kind::INT_TO_BITVECTOR:
 335     printBvParameterizedOp(out, n);
 336     out << ' ';
 337     stillNeedToPrintParams = false;
 338     break;
 339
 340     // datatypes
 341   case kind::APPLY_TYPE_ASCRIPTION: {
 342       out << "as ";
 343       toStream(out, n[0], toDepth < 0 ? toDepth : toDepth - 1, types);
 344       out << ' ';
 345       TypeNode t = TypeNode::fromType(n.getOperator().getConst<AscriptionType>().getType());
 346       out << (t.isFunctionLike() ? t.getRangeType() : t);
 347       out << ')';
 348       return;
 349     }
 350     break;
 351   case kind::APPLY_TESTER:
 352   case kind::APPLY_CONSTRUCTOR:
 353   case kind::APPLY_SELECTOR:
 354   case kind::PARAMETRIC_DATATYPE:
 355     break;
 356
 357     // quantifiers
 358   case kind::FORALL:
 359   case kind::EXISTS:
 360     if( k==kind::FORALL ){
 361       out << "forall ";
 362     }else{
 363       out << "exists ";
 364     }
 365     for( unsigned i=0; i<2; i++) {
 366       out << n[i] << " ";
 367       if( i==0 && n.getNumChildren()==3 ){
 368         out << "(! ";
 369       }
 370     }
 371     if( n.getNumChildren()==3 ){
 372       out << n[2];
 373       out << ")";
 374     }
 375     out << ")";
 376     return;
 377     break;
 378   case kind::BOUND_VAR_LIST:
 379     // the left parenthesis is already printed (before the switch)
 380     for(TNode::iterator i = n.begin(), iend = n.end();
 381         i != iend; ) {
 382       out << '(';
 383       toStream(out, (*i), toDepth < 0 ? toDepth : toDepth - 1, types);
 384       out << ' ';
 385       out << (*i).getType();
 386       // The following code do stange things
 387       // (*i).getType().toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
 388       //                         false, language::output::LANG_SMTLIB_V2);
 389       out << ')';
 390       if(++i != iend) {
 391         out << ' ';
 392       }
 393     }
 394     out << ')';
 395     return;
 396   case kind::INST_PATTERN:
 397     break;
 398   case kind::INST_PATTERN_LIST:
 399     // TODO user patterns
 400     for(unsigned i=0; i<n.getNumChildren(); i++) {
 401       out << ":pattern " << n[i];
 402     }
 403     return;
 404     break;
 405
 406   default:
 407     // fall back on however the kind prints itself; this probably
 408     // won't be SMT-LIB v2 compliant, but it will be clear from the
 409     // output that support for the kind needs to be added here.
 410     out << n.getKind() << ' ';
 411   }
 412   if( n.getMetaKind() == kind::metakind::PARAMETERIZED &&
 413       stillNeedToPrintParams ) {
 414     if(toDepth != 0) {
 415       toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types);
 416     } else {
 417       out << "(...)";
 418     }
 419     if(n.getNumChildren() > 0) {
 420       out << ' ';
 421     }
 422   }
 423   for(TNode::iterator i = n.begin(),
 424         iend = n.end();
 425       i != iend; ) {
 426     if(toDepth != 0) {
 427       toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, types);
 428     } else {
 429       out << "(...)";
 430     }
 431     if(++i != iend) {
 432       out << ' ';
 433     }
 434   }
 435   if(n.getNumChildren() != 0) {
 436     out << ')';
 437   }
 438 }/* Smt2Printer::toStream(TNode) */
 439
 440 static string smtKindString(Kind k) throw() {
 441   switch(k) {
 442     // builtin theory
 443   case kind::APPLY: break;
 444   case kind::EQUAL: return "=";
 445   case kind::DISTINCT: return "distinct";
 446   case kind::CHAIN: break;
 447   case kind::TUPLE: break;
 448   case kind::SEXPR: break;
 449
 450     // bool theory
 451   case kind::NOT: return "not";
 452   case kind::AND: return "and";
 453   case kind::IFF: return "=";
 454   case kind::IMPLIES: return "=>";
 455   case kind::OR: return "or";
 456   case kind::XOR: return "xor";
 457   case kind::ITE: return "ite";
 458
 459     // uf theory
 460   case kind::APPLY_UF: break;
 461
 462     // arith theory
 463   case kind::PLUS: return "+";
 464   case kind::MULT: return "*";
 465   case kind::MINUS: return "-";
 466   case kind::UMINUS: return "-";
 467   case kind::LT: return "<";
 468   case kind::LEQ: return "<=";
 469   case kind::GT: return ">";
 470   case kind::GEQ: return ">=";
 471   case kind::DIVISION:
 472   case kind::DIVISION_TOTAL: return "/";
 473   case kind::INTS_DIVISION: return "div";
 474   case kind::INTS_DIVISION_TOTAL: return "INTS_DIVISION_TOTAL";
 475   case kind::INTS_MODULUS: return "mod";
 476   case kind::INTS_MODULUS_TOTAL: return "INTS_MODULUS_TOTAL";
 477   case kind::ABS: return "abs";
 478   case kind::IS_INTEGER: return "is_int";
 479   case kind::TO_INTEGER: return "to_int";
 480   case kind::TO_REAL: return "to_real";
 481
 482     // arrays theory
 483   case kind::SELECT: return "select";
 484   case kind::STORE: return "store";
 485   case kind::STORE_ALL: return "__array_store_all__";
 486   case kind::ARRAY_TYPE: return "Array";
 487
 488     // bv theory
 489   case kind::BITVECTOR_CONCAT: return "concat";
 490   case kind::BITVECTOR_AND: return "bvand";
 491   case kind::BITVECTOR_OR: return "bvor";
 492   case kind::BITVECTOR_XOR: return "bvxor";
 493   case kind::BITVECTOR_NOT: return "bvnot";
 494   case kind::BITVECTOR_NAND: return "bvnand";
 495   case kind::BITVECTOR_NOR: return "bvnor";
 496   case kind::BITVECTOR_XNOR: return "bvxnor";
 497   case kind::BITVECTOR_COMP: return "bvcomp";
 498   case kind::BITVECTOR_MULT: return "bvmul";
 499   case kind::BITVECTOR_PLUS: return "bvadd";
 500   case kind::BITVECTOR_SUB: return "bvsub";
 501   case kind::BITVECTOR_NEG: return "bvneg";
 502   case kind::BITVECTOR_UDIV: return "bvudiv";
 503   case kind::BITVECTOR_UREM: return "bvurem";
 504   case kind::BITVECTOR_SDIV: return "bvsdiv";
 505   case kind::BITVECTOR_SREM: return "bvsrem";
 506   case kind::BITVECTOR_SMOD: return "bvsmod";
 507   case kind::BITVECTOR_SHL: return "bvshl";
 508   case kind::BITVECTOR_LSHR: return "bvlshr";
 509   case kind::BITVECTOR_ASHR: return "bvashr";
 510   case kind::BITVECTOR_ULT: return "bvult";
 511   case kind::BITVECTOR_ULE: return "bvule";
 512   case kind::BITVECTOR_UGT: return "bvugt";
 513   case kind::BITVECTOR_UGE: return "bvuge";
 514   case kind::BITVECTOR_SLT: return "bvslt";
 515   case kind::BITVECTOR_SLE: return "bvsle";
 516   case kind::BITVECTOR_SGT: return "bvsgt";
 517   case kind::BITVECTOR_SGE: return "bvsge";
 518
 519   case kind::BITVECTOR_EXTRACT: return "extract";
 520   case kind::BITVECTOR_REPEAT: return "repeat";
 521   case kind::BITVECTOR_ZERO_EXTEND: return "zero_extend";
 522   case kind::BITVECTOR_SIGN_EXTEND: return "sign_extend";
 523   case kind::BITVECTOR_ROTATE_LEFT: return "rotate_left";
 524   case kind::BITVECTOR_ROTATE_RIGHT: return "rotate_right";
 525   default:
 526     ; /* fall through */
 527   }
 528
 529   // no SMT way to print these
 530   return kind::kindToString(k);
 531 }
 532
 533 static void printBvParameterizedOp(std::ostream& out, TNode n) throw() {
 534   out << "(_ ";
 535   switch(n.getKind()) {
 536   case kind::BITVECTOR_EXTRACT: {
 537     BitVectorExtract p = n.getOperator().getConst<BitVectorExtract>();
 538     out << "extract " << p.high << ' ' << p.low;
 539     break;
 540   }
 541   case kind::BITVECTOR_REPEAT:
 542     out << "repeat "
 543         << n.getOperator().getConst<BitVectorRepeat>().repeatAmount;
 544     break;
 545   case kind::BITVECTOR_ZERO_EXTEND:
 546     out << "zero_extend "
 547         << n.getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount;
 548     break;
 549   case kind::BITVECTOR_SIGN_EXTEND:
 550     out << "sign_extend "
 551         << n.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
 552     break;
 553   case kind::BITVECTOR_ROTATE_LEFT:
 554     out << "rotate_left "
 555         << n.getOperator().getConst<BitVectorRotateLeft>().rotateLeftAmount;
 556     break;
 557   case kind::BITVECTOR_ROTATE_RIGHT:
 558     out << "rotate_right "
 559         << n.getOperator().getConst<BitVectorRotateRight>().rotateRightAmount;
 560     break;
 561   case kind::INT_TO_BITVECTOR:
 562     out << "int2bv "
 563         << n.getOperator().getConst<IntToBitVector>().size;
 564     break;
 565   default:
 566     out << n.getKind();
 567   }
 568   out << ")";
 569 }
 570
 571 template <class T>
 572 static bool tryToStream(std::ostream& out, const Command* c) throw();
 573
 574 void Smt2Printer::toStream(std::ostream& out, const Command* c,
 575                            int toDepth, bool types, size_t dag) const throw() {
 576   expr::ExprSetDepth::Scope sdScope(out, toDepth);
 577   expr::ExprPrintTypes::Scope ptScope(out, types);
 578   expr::ExprDag::Scope dagScope(out, dag);
 579
 580   if(tryToStream<AssertCommand>(out, c) ||
 581      tryToStream<PushCommand>(out, c) ||
 582      tryToStream<PopCommand>(out, c) ||
 583      tryToStream<CheckSatCommand>(out, c) ||
 584      tryToStream<QueryCommand>(out, c) ||
 585      tryToStream<QuitCommand>(out, c) ||
 586      tryToStream<DeclarationSequence>(out, c) ||
 587      tryToStream<CommandSequence>(out, c) ||
 588      tryToStream<DeclareFunctionCommand>(out, c) ||
 589      tryToStream<DeclareTypeCommand>(out, c) ||
 590      tryToStream<DefineTypeCommand>(out, c) ||
 591      tryToStream<DefineNamedFunctionCommand>(out, c) ||
 592      tryToStream<DefineFunctionCommand>(out, c) ||
 593      tryToStream<SimplifyCommand>(out, c) ||
 594      tryToStream<GetValueCommand>(out, c) ||
 595      tryToStream<GetModelCommand>(out, c) ||
 596      tryToStream<GetAssignmentCommand>(out, c) ||
 597      tryToStream<GetAssertionsCommand>(out, c) ||
 598      tryToStream<GetProofCommand>(out, c) ||
 599      tryToStream<SetBenchmarkStatusCommand>(out, c) ||
 600      tryToStream<SetBenchmarkLogicCommand>(out, c) ||
 601      tryToStream<SetInfoCommand>(out, c) ||
 602      tryToStream<GetInfoCommand>(out, c) ||
 603      tryToStream<SetOptionCommand>(out, c) ||
 604      tryToStream<GetOptionCommand>(out, c) ||
 605      tryToStream<DatatypeDeclarationCommand>(out, c) ||
 606      tryToStream<CommentCommand>(out, c) ||
 607      tryToStream<EmptyCommand>(out, c) ||
 608      tryToStream<EchoCommand>(out, c)) {
 609     return;
 610   }
 611
 612   out << "ERROR: don't know how to print a Command of class: "
 613       << typeid(*c).name() << endl;
 614
 615 }/* Smt2Printer::toStream(Command*) */
 616
 617 static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() {
 618   Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr);
 619 }
 620
 621 template <class T>
 622 static bool tryToStream(std::ostream& out, const CommandStatus* s) throw();
 623
 624 void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const throw() {
 625
 626   if(tryToStream<CommandSuccess>(out, s) ||
 627      tryToStream<CommandFailure>(out, s) ||
 628      tryToStream<CommandUnsupported>(out, s)) {
 629     return;
 630   }
 631
 632   out << "ERROR: don't know how to print a CommandStatus of class: "
 633       << typeid(*s).name() << endl;
 634
 635 }/* Smt2Printer::toStream(CommandStatus*) */
 636
 637
 638 void Smt2Printer::toStream(std::ostream& out, const Model& m) const throw() {
 639   out << "(model" << std::endl;
 640   this->Printer::toStream(out, m);
 641   out << ")" << std::endl;
 642 }
 643
 644
 645 void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c) const throw() {
 646   const theory::TheoryModel& tm = (const theory::TheoryModel&) m;
 647   if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) {
 648     TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
 649     if( options::modelUninterpDtEnum() && tn.isSort() &&
 650         tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
 651       out << "(declare-datatypes () ((" << dynamic_cast<const DeclareTypeCommand*>(c)->getSymbol() << " ";
 652       for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
 653         out << "(" << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << ")";
 654       }
 655       out << ")))" << std::endl;
 656     } else {
 657       if( tn.isSort() ){
 658         //print the cardinality
 659         if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
 660           out << "; cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << std::endl;
 661         }
 662       }
 663       out << c << std::endl;
 664       if( tn.isSort() ){
 665         //print the representatives
 666         if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
 667           for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
 668             if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){
 669               out << "(declare-fun " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << " () " << tn << ")" << std::endl;
 670             }else{
 671               out << "; rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << std::endl;
 672             }
 673           }
 674         }
 675       }
 676     }
 677   } else if(dynamic_cast<const DeclareFunctionCommand*>(c) != NULL) {
 678     Node n = Node::fromExpr( ((const DeclareFunctionCommand*)c)->getFunction() );
 679     if(n.getKind() == kind::SKOLEM) {
 680       // don't print out internal stuff
 681       return;
 682     }
 683     Node val = Node::fromExpr(tm.getSmtEngine()->getValue(n.toExpr()));
 684     if(val.getKind() == kind::LAMBDA) {
 685       out << "(define-fun " << n << " " << val[0]
 686           << " " << n.getType().getRangeType()
 687           << " " << val[1] << ")" << std::endl;
 688     } else {
 689       if( options::modelUninterpDtEnum() && val.getKind() == kind::STORE ) {
 690         TypeNode tn = val[1].getType();
 691         if (tn.isSort() && tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
 692           Cardinality indexCard((*tm.d_rep_set.d_type_reps.find(tn)).second.size());
 693           val = theory::arrays::TheoryArraysRewriter::normalizeConstant( val, indexCard );
 694         }
 695       }
 696       out << "(define-fun " << n << " () "
 697           << n.getType() << " " << val << ")" << std::endl;
 698     }
 699 /*
 700     //for table format (work in progress)
 701     bool printedModel = false;
 702     if( tn.isFunction() ){
 703       if( options::modelFormatMode()==MODEL_FORMAT_MODE_TABLE ){
 704         //specialized table format for functions
 705         RepSetIterator riter( &d_rep_set );
 706         riter.setFunctionDomain( n );
 707         while( !riter.isFinished() ){
 708           std::vector< Node > children;
 709           children.push_back( n );
 710           for( int i=0; i<riter.getNumTerms(); i++ ){
 711             children.push_back( riter.getTerm( i ) );
 712           }
 713           Node nn = NodeManager::currentNM()->mkNode( APPLY_UF, children );
 714           Node val = getValue( nn );
 715           out << val << " ";
 716           riter.increment();
 717         }
 718         printedModel = true;
 719       }
 720     }
 721 */
 722   }else{
 723     out << c << std::endl;
 724   }
 725 }
 726
 727 void Smt2Printer::toStream(std::ostream& out, const Result& r) const throw() {
 728   if(r.getType() == Result::TYPE_SAT && r.isSat() == Result::SAT_UNKNOWN) {
 729     out << "unknown";
 730   } else {
 731     Printer::toStream(out, r);
 732   }
 733 }
 734
 735 static void toStream(std::ostream& out, const AssertCommand* c) throw() {
 736   out << "(assert " << c->getExpr() << ")";
 737 }
 738
 739 static void toStream(std::ostream& out, const PushCommand* c) throw() {
 740   out << "(push 1)";
 741 }
 742
 743 static void toStream(std::ostream& out, const PopCommand* c) throw() {
 744   out << "(pop 1)";
 745 }
 746
 747 static void toStream(std::ostream& out, const CheckSatCommand* c) throw() {
 748   Expr e = c->getExpr();
 749   if(!e.isNull()) {
 750     out << PushCommand() << endl
 751         << AssertCommand(e) << endl
 752         << CheckSatCommand() << endl
 753         << PopCommand() << endl;
 754   } else {
 755     out << "(check-sat)";
 756   }
 757 }
 758
 759 static void toStream(std::ostream& out, const QueryCommand* c) throw() {
 760   Expr e = c->getExpr();
 761   if(!e.isNull()) {
 762     out << PushCommand() << endl
 763         << AssertCommand(BooleanSimplification::negate(e)) << endl
 764         << CheckSatCommand() << endl
 765         << PopCommand() << endl;
 766   } else {
 767     out << "(check-sat)";
 768   }
 769 }
 770
 771 static void toStream(std::ostream& out, const QuitCommand* c) throw() {
 772   out << "(exit)";
 773 }
 774
 775 static void toStream(std::ostream& out, const CommandSequence* c) throw() {
 776   for(CommandSequence::const_iterator i = c->begin();
 777       i != c->end();
 778       ++i) {
 779     out << *i << endl;
 780   }
 781 }
 782
 783 static void toStream(std::ostream& out, const DeclareFunctionCommand* c) throw() {
 784   Type type = c->getType();
 785   out << "(declare-fun " << c->getSymbol() << " (";
 786   if(type.isFunction()) {
 787     FunctionType ft = type;
 788     const vector<Type> argTypes = ft.getArgTypes();
 789     if(argTypes.size() > 0) {
 790       copy( argTypes.begin(), argTypes.end() - 1,
 791             ostream_iterator<Type>(out, " ") );
 792       out << argTypes.back();
 793     }
 794     type = ft.getRangeType();
 795   }
 796
 797   out << ") " << type << ")";
 798 }
 799
 800 static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw() {
 801   Expr func = c->getFunction();
 802   const vector<Expr>* formals = &c->getFormals();
 803   out << "(define-fun " << func << " (";
 804   Type type = func.getType();
 805   Expr formula = c->getFormula();
 806   if(type.isFunction()) {
 807     vector<Expr> f;
 808     if(formals->empty()) {
 809       const vector<Type>& params = FunctionType(type).getArgTypes();
 810       for(vector<Type>::const_iterator j = params.begin(); j != params.end(); ++j) {
 811         f.push_back(NodeManager::currentNM()->mkSkolem("a", TypeNode::fromType(*j), "",
 812                                                        NodeManager::SKOLEM_NO_NOTIFY).toExpr());
 813       }
 814       formula = NodeManager::currentNM()->toExprManager()->mkExpr(kind::APPLY_UF, formula, f);
 815       formals = &f;
 816     }
 817     vector<Expr>::const_iterator i = formals->begin();
 818     for(;;) {
 819       out << "(" << (*i) << " " << (*i).getType() << ")";
 820       ++i;
 821       if(i != formals->end()) {
 822         out << " ";
 823       } else {
 824         break;
 825       }
 826     }
 827     type = FunctionType(type).getRangeType();
 828   }
 829   out << ") " << type << " " << formula << ")";
 830 }
 831
 832 static void toStream(std::ostream& out, const DeclareTypeCommand* c) throw() {
 833   out << "(declare-sort " << c->getSymbol() << " " << c->getArity() << ")";
 834 }
 835
 836 static void toStream(std::ostream& out, const DefineTypeCommand* c) throw() {
 837   const vector<Type>& params = c->getParameters();
 838   out << "(define-sort " << c->getSymbol() << " (";
 839   if(params.size() > 0) {
 840     copy( params.begin(), params.end() - 1,
 841           ostream_iterator<Type>(out, " ") );
 842     out << params.back();
 843   }
 844   out << ") " << c->getType() << ")";
 845 }
 846
 847 static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) throw() {
 848   out << "DefineNamedFunction( ";
 849   toStream(out, static_cast<const DefineFunctionCommand*>(c));
 850   out << " )";
 851
 852   out << "ERROR: don't know how to output define-named-function command" << endl;
 853 }
 854
 855 static void toStream(std::ostream& out, const SimplifyCommand* c) throw() {
 856   out << "Simplify( << " << c->getTerm() << " >> )";
 857
 858   out << "ERROR: don't know how to output simplify command" << endl;
 859 }
 860
 861 static void toStream(std::ostream& out, const GetValueCommand* c) throw() {
 862   out << "(get-value ( ";
 863   const vector<Expr>& terms = c->getTerms();
 864   copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, " "));
 865   out << " ))";
 866 }
 867
 868 static void toStream(std::ostream& out, const GetModelCommand* c) throw() {
 869   out << "(get-model)";
 870 }
 871
 872 static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() {
 873   out << "(get-assignment)";
 874 }
 875
 876 static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() {
 877   out << "(get-assertions)";
 878 }
 879
 880 static void toStream(std::ostream& out, const GetProofCommand* c) throw() {
 881   out << "(get-proof)";
 882 }
 883
 884 static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() {
 885   out << "(set-info :status " << c->getStatus() << ")";
 886 }
 887
 888 static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw() {
 889   out << "(set-logic " << c->getLogic() << ")";
 890 }
 891
 892 static void toStream(std::ostream& out, const SetInfoCommand* c) throw() {
 893   out << "(set-info :" << c->getFlag() << " ";
 894   toStream(out, c->getSExpr());
 895   out << ")";
 896 }
 897
 898 static void toStream(std::ostream& out, const GetInfoCommand* c) throw() {
 899   out << "(get-info :" << c->getFlag() << ")";
 900 }
 901
 902 static void toStream(std::ostream& out, const SetOptionCommand* c) throw() {
 903   out << "(set-option :" << c->getFlag() << " ";
 904   toStream(out, c->getSExpr());
 905   out << ")";
 906 }
 907
 908 static void toStream(std::ostream& out, const GetOptionCommand* c) throw() {
 909   out << "(get-option :" << c->getFlag() << ")";
 910 }
 911
 912 static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) throw() {
 913   const vector<DatatypeType>& datatypes = c->getDatatypes();
 914   out << "(declare-datatypes () (";
 915   for(vector<DatatypeType>::const_iterator i = datatypes.begin(),
 916         i_end = datatypes.end();
 917       i != i_end;
 918       ++i) {
 919
 920     const Datatype & d = i->getDatatype();
 921
 922     out << "(" << maybeQuoteSymbol(d.getName()) << "  ";
 923     for(Datatype::const_iterator ctor = d.begin(), ctor_end = d.end();
 924         ctor != ctor_end; ++ctor){
 925       if( ctor!=d.begin() ) out << " ";
 926       out << "(" << maybeQuoteSymbol(ctor->getName());
 927
 928       for(DatatypeConstructor::const_iterator arg = ctor->begin(), arg_end = ctor->end();
 929           arg != arg_end; ++arg){
 930         out << " (" << arg->getSelector() << " "
 931             << static_cast<SelectorType>(arg->getType()).getRangeType() << ")";
 932       }
 933       out << ")";
 934     }
 935     out << ")" << endl;
 936   }
 937   out << "))";
 938 }
 939
 940 static void toStream(std::ostream& out, const CommentCommand* c) throw() {
 941   string s = c->getComment();
 942   size_t pos = 0;
 943   while((pos = s.find_first_of('"', pos)) != string::npos) {
 944     s.replace(pos, 1, "\\\"");
 945     pos += 2;
 946   }
 947   out << "(set-info :notes \"" << s << "\")";
 948 }
 949
 950 static void toStream(std::ostream& out, const EmptyCommand* c) throw() {
 951 }
 952
 953 static void toStream(std::ostream& out, const EchoCommand* c) throw() {
 954   out << "(echo \"" << c->getOutput() << "\")";
 955 }
 956
 957 template <class T>
 958 static bool tryToStream(std::ostream& out, const Command* c) throw() {
 959   if(typeid(*c) == typeid(T)) {
 960     toStream(out, dynamic_cast<const T*>(c));
 961     return true;
 962   }
 963   return false;
 964 }
 965
 966 static void toStream(std::ostream& out, const CommandSuccess* s) throw() {
 967   if(Command::printsuccess::getPrintSuccess(out)) {
 968     out << "success" << endl;
 969   }
 970 }
 971
 972 static void toStream(std::ostream& out, const CommandUnsupported* s) throw() {
 973 #ifdef CVC4_COMPETITION_MODE
 974   // if in competition mode, lie and say we're ok
 975   // (we have nothing to lose by saying success, and everything to lose
 976   // if we say "unsupported")
 977   out << "success" << endl;
 978 #else /* CVC4_COMPETITION_MODE */
 979   out << "unsupported" << endl;
 980 #endif /* CVC4_COMPETITION_MODE */
 981 }
 982
 983 static void toStream(std::ostream& out, const CommandFailure* s) throw() {
 984   string message = s->getMessage();
 985   // escape all double-quotes
 986   size_t pos;
 987   while((pos = message.find('"')) != string::npos) {
 988     message = message.replace(pos, 1, "\\\"");
 989   }
 990   out << "(error \"" << message << "\")" << endl;
 991 }
 992
 993 template <class T>
 994 static bool tryToStream(std::ostream& out, const CommandStatus* s) throw() {
 995   if(typeid(*s) == typeid(T)) {
 996     toStream(out, dynamic_cast<const T*>(s));
 997     return true;
 998   }
 999   return false;
1000 }
1001
1002 }/* CVC4::printer::smt2 namespace */
1003 }/* CVC4::printer namespace */
1004 }/* CVC4 namespace */