1 files changed, 180 insertions, 0 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 0d5f367ad..5ce571904 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -19,6 +19,9 @@
 #include "printer/smt2/smt2_printer.h"
 
 #include <iostream>
+#include <vector>
+#include <string>
+#include <typeinfo>
 
 using namespace std;
 
@@ -235,6 +238,183 @@ void printBvParameterizedOp(std::ostream& out, TNode n) {
   out << ")";
 }
 
+template <class T>
+static bool tryToStream(std::ostream& out, const Command* c);
+
+void Smt2Printer::toStream(std::ostream& out, const Command* c,
+                           int toDepth, bool types) const {
+  expr::ExprSetDepth::Scope sdScope(out, toDepth);
+  expr::ExprPrintTypes::Scope ptScope(out, types);
+
+  if(tryToStream<AssertCommand>(out, c) ||
+     tryToStream<PushCommand>(out, c) ||
+     tryToStream<PopCommand>(out, c) ||
+     tryToStream<CheckSatCommand>(out, c) ||
+     tryToStream<QueryCommand>(out, c) ||
+     tryToStream<QuitCommand>(out, c) ||
+     tryToStream<CommandSequence>(out, c) ||
+     tryToStream<DeclarationCommand>(out, c) ||
+     tryToStream<DefineFunctionCommand>(out, c) ||
+     tryToStream<DefineNamedFunctionCommand>(out, c) ||
+     tryToStream<SimplifyCommand>(out, c) ||
+     tryToStream<GetValueCommand>(out, c) ||
+     tryToStream<GetAssignmentCommand>(out, c) ||
+     tryToStream<GetAssertionsCommand>(out, c) ||
+     tryToStream<SetBenchmarkStatusCommand>(out, c) ||
+     tryToStream<SetBenchmarkLogicCommand>(out, c) ||
+     tryToStream<SetInfoCommand>(out, c) ||
+     tryToStream<GetInfoCommand>(out, c) ||
+     tryToStream<SetOptionCommand>(out, c) ||
+     tryToStream<GetOptionCommand>(out, c) ||
+     tryToStream<DatatypeDeclarationCommand>(out, c)) {
+    return;
+  }
+
+  Unhandled("don't know how to print this command as SMT-LIBv2: %s", c->toString().c_str());
+
+}/* Smt2Printer::toStream() */
+
+static void toStream(std::ostream& out, const AssertCommand* c) {
+  out << "(assert " << c->getExpr() << ")";
+}
+
+static void toStream(std::ostream& out, const PushCommand* c) {
+  out << "(push 1)";
+}
+
+static void toStream(std::ostream& out, const PopCommand* c) {
+  out << "(pop 1)";
+}
+
+static void toStream(std::ostream& out, const CheckSatCommand* c) {
+  BoolExpr e = c->getExpr();
+  if(!e.isNull()) {
+    out << "(assert " << e << ")";
+  }
+  out << "(check-sat)";
+}
+
+static void toStream(std::ostream& out, const QueryCommand* c) {
+  Unhandled("query command");
+}
+
+static void toStream(std::ostream& out, const QuitCommand* c) {
+  out << "(exit)";
+}
+
+static void toStream(std::ostream& out, const CommandSequence* c) {
+  for(CommandSequence::const_iterator i = c->begin();
+      i != c->end();
+      ++i) {
+    out << *i << endl;
+  }
+}
+
+static void toStream(std::ostream& out, const DeclarationCommand* c) {
+  const vector<string>& declaredSymbols = c->getDeclaredSymbols();
+  Type declaredType = c->getDeclaredType();
+  for(vector<string>::const_iterator i = declaredSymbols.begin();
+      i != declaredSymbols.end();
+      ++i) {
+    if(declaredType.isFunction()) {
+      FunctionType ft = declaredType;
+      out << "(declare-fun " << *i << " (";
+      const vector<Type> argTypes = ft.getArgTypes();
+      if(argTypes.size() > 0) {
+        copy( argTypes.begin(), argTypes.end() - 1,
+              ostream_iterator<Type>(out, " ") );
+        out << argTypes.back();
+      }
+      out << ") " << ft.getRangeType() << ")";
+    } else {
+      out << "(declare-fun " << *i << " () " << declaredType << ")";
+    }
+  }
+}
+
+static void toStream(std::ostream& out, const DefineFunctionCommand* c) {
+  Expr func = c->getFunction();
+  const vector<Expr>& formals = c->getFormals();
+  Expr formula = c->getFormula();
+  out << "(define-fun " << func << " (";
+  for(vector<Expr>::const_iterator i = formals.begin();
+      i != formals.end();
+      ++i) {
+    out << "(" << (*i) << " " << (*i).getType() << ")";
+  }
+  out << ") " << FunctionType(func.getType()).getRangeType() << " " << formula << ")";
+}
+
+static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) {
+  out << "DefineNamedFunction( ";
+  toStream(out, static_cast<const DefineFunctionCommand*>(c));
+  out << " )";
+  Unhandled("define named function command");
+}
+
+static void toStream(std::ostream& out, const SimplifyCommand* c) {
+  out << "Simplify( << " << c->getTerm() << " >> )";
+  Unhandled("simplify command");
+}
+
+static void toStream(std::ostream& out, const GetValueCommand* c) {
+  out << "(get-value " << c->getTerm() << ")";
+}
+
+static void toStream(std::ostream& out, const GetAssignmentCommand* c) {
+  out << "(get-assignment)";
+}
+
+static void toStream(std::ostream& out, const GetAssertionsCommand* c) {
+  out << "(get-assertions)";
+}
+
+static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) {
+  out << "(set-info :status " << c->getStatus() << ")";
+}
+
+static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) {
+  out << "(set-logic " << c->getLogic() << ")";
+}
+
+static void toStream(std::ostream& out, const SetInfoCommand* c) {
+  out << "(set-info " << c->getFlag() << " " << c->getSExpr() << ")";
+}
+
+static void toStream(std::ostream& out, const GetInfoCommand* c) {
+  out << "(get-info " << c->getFlag() << ")";
+}
+
+static void toStream(std::ostream& out, const SetOptionCommand* c) {
+  out << "(set-option " << c->getFlag() << " " << c->getSExpr() << ")";
+}
+
+static void toStream(std::ostream& out, const GetOptionCommand* c) {
+  out << "(get-option " << c->getFlag() << ")";
+}
+
+static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) {
+  const vector<DatatypeType>& datatypes = c->getDatatypes();
+  out << "DatatypeDeclarationCommand([";
+  for(vector<DatatypeType>::const_iterator i = datatypes.begin(),
+        i_end = datatypes.end();
+      i != i_end;
+      ++i) {
+    out << *i << ";" << endl;
+  }
+  out << "])";
+  Unhandled("datatype declaration command");
+}
+
+template <class T>
+static bool tryToStream(std::ostream& out, const Command* c) {
+  if(typeid(*c) == typeid(T)) {
+    toStream(out, dynamic_cast<const T*>(c));
+    return true;
+  }
+  return false;
+}
+
 }/* CVC4::printer::smt2 namespace */
 }/* CVC4::printer namespace */
 }/* CVC4 namespace */