Refactor functions that print commands (Part 2) (#4905)

This PR is a step towards migrating commands to the Term/Sort level. It replaces the dynamic casts for printing commands with direct calls to corresponding functions. Those functions now take node level arguments instead of commands to make them available for internal code.

13 files changed, 2305 insertions, 747 deletions

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 7e91b3b99..6c84b73bc 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -44,6 +44,8 @@ class Datatype;
 class DatatypeConstructor;
 class DatatypeConstructorArg;
 class ExprManager;
+class GetAbductCommand;
+class GetInterpolCommand;
 class NodeManager;
 class SmtEngine;
 class SynthFunCommand;
@@ -1950,8 +1952,10 @@ std::ostream& operator<<(std::ostream& out,
  */
 class CVC4_PUBLIC Grammar
 {
-  friend class Solver;
+  friend class CVC4::GetAbductCommand;
+  friend class CVC4::GetInterpolCommand;
   friend class CVC4::SynthFunCommand;
+  friend class Solver;
 
  public:
   /**
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 1923594f3..d4f28c186 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -132,55 +132,6 @@ void AstPrinter::toStream(std::ostream& out,
 template <class T>
 static bool tryToStream(std::ostream& out, const Command* c);
 
-void AstPrinter::toStream(std::ostream& out,
-                          const Command* c,
-                          int toDepth,
-                          bool types,
-                          size_t dag) const
-{
-  expr::ExprSetDepth::Scope sdScope(out, toDepth);
-  expr::ExprPrintTypes::Scope ptScope(out, types);
-  expr::ExprDag::Scope dagScope(out, dag);
-
-  if(tryToStream<EmptyCommand>(out, c) ||
-     tryToStream<AssertCommand>(out, c) ||
-     tryToStream<PushCommand>(out, c) ||
-     tryToStream<PopCommand>(out, c) ||
-     tryToStream<CheckSatCommand>(out, c) ||
-     tryToStream<CheckSatAssumingCommand>(out, c) ||
-     tryToStream<QueryCommand>(out, c) ||
-     tryToStream<ResetCommand>(out, c) ||
-     tryToStream<ResetAssertionsCommand>(out, c) ||
-     tryToStream<QuitCommand>(out, c) ||
-     tryToStream<DeclarationSequence>(out, c) ||
-     tryToStream<CommandSequence>(out, c) ||
-     tryToStream<DeclareFunctionCommand>(out, c) ||
-     tryToStream<DeclareTypeCommand>(out, c) ||
-     tryToStream<DefineTypeCommand>(out, c) ||
-     tryToStream<DefineNamedFunctionCommand>(out, c) ||
-     tryToStream<DefineFunctionCommand>(out, c) ||
-     tryToStream<SimplifyCommand>(out, c) ||
-     tryToStream<GetValueCommand>(out, c) ||
-     tryToStream<GetModelCommand>(out, c) ||
-     tryToStream<GetAssignmentCommand>(out, c) ||
-     tryToStream<GetAssertionsCommand>(out, c) ||
-     tryToStream<GetProofCommand>(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) ||
-     tryToStream<CommentCommand>(out, c)) {
-    return;
-  }
-
-  out << "ERROR: don't know how to print a Command of class: "
-      << typeid(*c).name() << endl;
-
-}/* AstPrinter::toStream(Command*) */
-
 template <class T>
 static bool tryToStream(std::ostream& out, const CommandStatus* s);
 
@@ -211,198 +162,236 @@ void AstPrinter::toStream(std::ostream& out,
   Unreachable();
 }
 
-static void toStream(std::ostream& out, const EmptyCommand* c)
+void AstPrinter::toStreamCmdEmpty(std::ostream& out,
+                                  const std::string& name) const
 {
-  out << "EmptyCommand(" << c->getName() << ")";
+  out << "EmptyCommand(" << name << ')';
 }
 
-static void toStream(std::ostream& out, const AssertCommand* c)
+void AstPrinter::toStreamCmdEcho(std::ostream& out,
+                                 const std::string& output) const
 {
-  out << "Assert(" << c->getExpr() << ")";
+  out << "EchoCommand(" << output << ')';
 }
 
-static void toStream(std::ostream& out, const PushCommand* c)
+void AstPrinter::toStreamCmdAssert(std::ostream& out, Node n) const
 {
-  out << "Push()";
+  out << "Assert(" << n << ')';
 }
 
-static void toStream(std::ostream& out, const PopCommand* c) { out << "Pop()"; }
+void AstPrinter::toStreamCmdPush(std::ostream& out) const { out << "Push()"; }
+
+void AstPrinter::toStreamCmdPop(std::ostream& out) const { out << "Pop()"; }
 
-static void toStream(std::ostream& out, const CheckSatCommand* c)
+void AstPrinter::toStreamCmdCheckSat(std::ostream& out, Node n) const
 {
-  Expr e = c->getExpr();
-  if(e.isNull()) {
+  if (n.isNull())
+  {
     out << "CheckSat()";
-  } else {
-    out << "CheckSat(" << e << ")";
+  }
+  else
+  {
+    out << "CheckSat(" << n << ')';
   }
 }
 
-static void toStream(std::ostream& out, const CheckSatAssumingCommand* c)
+void AstPrinter::toStreamCmdCheckSatAssuming(
+    std::ostream& out, const std::vector<Node>& nodes) const
 {
-  const vector<Expr>& terms = c->getTerms();
   out << "CheckSatAssuming( << ";
-  copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, ", "));
+  copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, ", "));
   out << ">> )";
 }
 
-static void toStream(std::ostream& out, const QueryCommand* c)
+void AstPrinter::toStreamCmdQuery(std::ostream& out, Node n) const
 {
-  out << "Query(" << c->getExpr() << ')';
+  out << "Query(" << n << ')';
 }
 
-static void toStream(std::ostream& out, const ResetCommand* c)
-{
-  out << "Reset()";
-}
+void AstPrinter::toStreamCmdReset(std::ostream& out) const { out << "Reset()"; }
 
-static void toStream(std::ostream& out, const ResetAssertionsCommand* c)
+void AstPrinter::toStreamCmdResetAssertions(std::ostream& out) const
 {
   out << "ResetAssertions()";
 }
 
-static void toStream(std::ostream& out, const QuitCommand* c)
-{
-  out << "Quit()";
-}
+void AstPrinter::toStreamCmdQuit(std::ostream& out) const { out << "Quit()"; }
 
-static void toStream(std::ostream& out, const DeclarationSequence* c)
+void AstPrinter::toStreamCmdDeclarationSequence(
+    std::ostream& out, const std::vector<Command*>& sequence) const
 {
   out << "DeclarationSequence[" << endl;
-  for(CommandSequence::const_iterator i = c->begin();
-      i != c->end();
-      ++i) {
+  for (CommandSequence::const_iterator i = sequence.cbegin();
+       i != sequence.cend();
+       ++i)
+  {
     out << *i << endl;
   }
   out << "]";
 }
 
-static void toStream(std::ostream& out, const CommandSequence* c)
+void AstPrinter::toStreamCmdCommandSequence(
+    std::ostream& out, const std::vector<Command*>& sequence) const
 {
   out << "CommandSequence[" << endl;
-  for(CommandSequence::const_iterator i = c->begin();
-      i != c->end();
-      ++i) {
+  for (CommandSequence::const_iterator i = sequence.cbegin();
+       i != sequence.cend();
+       ++i)
+  {
     out << *i << endl;
   }
   out << "]";
 }
 
-static void toStream(std::ostream& out, const DeclareFunctionCommand* c)
+void AstPrinter::toStreamCmdDeclareFunction(std::ostream& out,
+                                            const std::string& id,
+                                            TypeNode type) const
 {
-  out << "Declare(" << c->getSymbol() << "," << c->getType() << ")";
+  out << "Declare(" << id << "," << type << ')';
 }
 
-static void toStream(std::ostream& out, const DefineFunctionCommand* c)
+void AstPrinter::toStreamCmdDefineFunction(std::ostream& out,
+                                           const std::string& id,
+                                           const std::vector<Node>& formals,
+                                           TypeNode range,
+                                           Node formula) const
 {
-  Expr func = c->getFunction();
-  const std::vector<Expr>& formals = c->getFormals();
-  Expr formula = c->getFormula();
-  out << "DefineFunction( \"" << func << "\", [";
-  if(formals.size() > 0) {
-    copy( formals.begin(), formals.end() - 1,
-          ostream_iterator<Expr>(out, ", ") );
+  out << "DefineFunction( \"" << id << "\", [";
+  if (formals.size() > 0)
+  {
+    copy(formals.begin(), formals.end() - 1, ostream_iterator<Node>(out, ", "));
     out << formals.back();
   }
   out << "], << " << formula << " >> )";
 }
 
-static void toStream(std::ostream& out, const DeclareTypeCommand* c)
+void AstPrinter::toStreamCmdDeclareType(std::ostream& out,
+                                        const std::string& id,
+                                        size_t arity,
+                                        TypeNode type) const
 {
-  out << "DeclareType(" << c->getSymbol() << "," << c->getArity() << ","
-      << c->getType() << ")";
+  out << "DeclareType(" << id << "," << arity << "," << type << ')';
 }
 
-static void toStream(std::ostream& out, const DefineTypeCommand* c)
+void AstPrinter::toStreamCmdDefineType(std::ostream& out,
+                                       const std::string& id,
+                                       const std::vector<TypeNode>& params,
+                                       TypeNode t) const
 {
-  const vector<Type>& params = c->getParameters();
-  out << "DefineType(" << c->getSymbol() << ",[";
-  if(params.size() > 0) {
-    copy( params.begin(), params.end() - 1,
-          ostream_iterator<Type>(out, ", ") );
+  out << "DefineType(" << id << ",[";
+  if (params.size() > 0)
+  {
+    copy(params.begin(),
+         params.end() - 1,
+         ostream_iterator<TypeNode>(out, ", "));
     out << params.back();
   }
-  out << "]," << c->getType() << ")";
+  out << "]," << t << ')';
 }
 
-static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c)
+void AstPrinter::toStreamCmdDefineNamedFunction(
+    std::ostream& out,
+    const std::string& id,
+    const std::vector<Node>& formals,
+    TypeNode range,
+    Node formula) const
 {
   out << "DefineNamedFunction( ";
-  toStream(out, static_cast<const DefineFunctionCommand*>(c));
-  out << " )";
+  toStreamCmdDefineFunction(out, id, formals, range, formula);
+  out << " )" << std::endl;
 }
 
-static void toStream(std::ostream& out, const SimplifyCommand* c)
+void AstPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const
 {
-  out << "Simplify( << " << c->getTerm() << " >> )";
+  out << "Simplify( << " << n << " >> )";
 }
 
-static void toStream(std::ostream& out, const GetValueCommand* c)
+void AstPrinter::toStreamCmdGetValue(std::ostream& out,
+                                     const std::vector<Node>& nodes) const
 {
   out << "GetValue( << ";
-  const vector<Expr>& terms = c->getTerms();
-  copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, ", "));
+  copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, ", "));
   out << ">> )";
 }
 
-static void toStream(std::ostream& out, const GetModelCommand* c)
+void AstPrinter::toStreamCmdGetModel(std::ostream& out) const
 {
   out << "GetModel()";
 }
 
-static void toStream(std::ostream& out, const GetAssignmentCommand* c)
+void AstPrinter::toStreamCmdGetAssignment(std::ostream& out) const
 {
   out << "GetAssignment()";
 }
-static void toStream(std::ostream& out, const GetAssertionsCommand* c)
+
+void AstPrinter::toStreamCmdGetAssertions(std::ostream& out) const
 {
   out << "GetAssertions()";
 }
-static void toStream(std::ostream& out, const GetProofCommand* c)
+
+void AstPrinter::toStreamCmdGetProof(std::ostream& out) const
 {
   out << "GetProof()";
 }
-static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c)
+
+void AstPrinter::toStreamCmdGetUnsatCore(std::ostream& out) const
 {
-  out << "SetBenchmarkStatus(" << c->getStatus() << ")";
+  out << "GetUnsatCore()";
 }
-static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c)
+
+void AstPrinter::toStreamCmdSetBenchmarkStatus(std::ostream& out,
+                                               BenchmarkStatus status) const
 {
-  out << "SetBenchmarkLogic(" << c->getLogic() << ")";
+  out << "SetBenchmarkStatus(" << status << ')';
 }
-static void toStream(std::ostream& out, const SetInfoCommand* c)
+
+void AstPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out,
+                                              const std::string& logic) const
 {
-  out << "SetInfo(" << c->getFlag() << ", " << c->getSExpr() << ")";
+  out << "SetBenchmarkLogic(" << logic << ')';
 }
 
-static void toStream(std::ostream& out, const GetInfoCommand* c)
+void AstPrinter::toStreamCmdSetInfo(std::ostream& out,
+                                    const std::string& flag,
+                                    SExpr sexpr) const
 {
-  out << "GetInfo(" << c->getFlag() << ")";
+  out << "SetInfo(" << flag << ", " << sexpr << ')';
 }
-static void toStream(std::ostream& out, const SetOptionCommand* c)
+
+void AstPrinter::toStreamCmdGetInfo(std::ostream& out,
+                                    const std::string& flag) const
+{
+  out << "GetInfo(" << flag << ')';
+}
+
+void AstPrinter::toStreamCmdSetOption(std::ostream& out,
+                                      const std::string& flag,
+                                      SExpr sexpr) const
 {
-  out << "SetOption(" << c->getFlag() << ", " << c->getSExpr() << ")";
+  out << "SetOption(" << flag << ", " << sexpr << ')';
 }
 
-static void toStream(std::ostream& out, const GetOptionCommand* c)
+void AstPrinter::toStreamCmdGetOption(std::ostream& out,
+                                      const std::string& flag) const
 {
-  out << "GetOption(" << c->getFlag() << ")";
+  out << "GetOption(" << flag << ')';
 }
 
-static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c)
+void AstPrinter::toStreamCmdDatatypeDeclaration(
+    std::ostream& out, const std::vector<TypeNode>& datatypes) const
 {
-  const vector<Type>& datatypes = c->getDatatypes();
   out << "DatatypeDeclarationCommand([";
-  for (const Type& t : datatypes)
+  for (const TypeNode& t : datatypes)
   {
     out << t << ";" << endl;
   }
   out << "])";
 }
 
-static void toStream(std::ostream& out, const CommentCommand* c)
+void AstPrinter::toStreamCmdComment(std::ostream& out,
+                                    const std::string& comment) const
 {
-  out << "CommentCommand([" << c->getComment() << "])";
+  out << "CommentCommand([" << comment << "])";
 }
 
 template <class T>
diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h
index 2fd7da749..17e052037 100644
--- a/src/printer/ast/ast_printer.h
+++ b/src/printer/ast/ast_printer.h
@@ -27,7 +27,8 @@ namespace CVC4 {
 namespace printer {
 namespace ast {
 
-class AstPrinter : public CVC4::Printer {
+class AstPrinter : public CVC4::Printer
+{
  public:
   using CVC4::Printer::toStream;
   void toStream(std::ostream& out,
@@ -35,23 +36,150 @@ class AstPrinter : public CVC4::Printer {
                 int toDepth,
                 bool types,
                 size_t dag) const override;
-  void toStream(std::ostream& out,
-                const Command* c,
-                int toDepth,
-                bool types,
-                size_t dag) const override;
   void toStream(std::ostream& out, const CommandStatus* s) const override;
   void toStream(std::ostream& out, const Model& m) const override;
 
+  /** Print empty command */
+  void toStreamCmdEmpty(std::ostream& out,
+                        const std::string& name) const override;
+
+  /** Print echo command */
+  void toStreamCmdEcho(std::ostream& out,
+                       const std::string& output) const override;
+
+  /** Print assert command */
+  void toStreamCmdAssert(std::ostream& out, Node n) const override;
+
+  /** Print push command */
+  void toStreamCmdPush(std::ostream& out) const override;
+
+  /** Print pop command */
+  void toStreamCmdPop(std::ostream& out) const override;
+
+  /** Print declare-fun command */
+  void toStreamCmdDeclareFunction(std::ostream& out,
+                                  const std::string& id,
+                                  TypeNode type) const override;
+
+  /** Print declare-sort command */
+  void toStreamCmdDeclareType(std::ostream& out,
+                              const std::string& id,
+                              size_t arity,
+                              TypeNode type) const override;
+
+  /** Print define-sort command */
+  void toStreamCmdDefineType(std::ostream& out,
+                             const std::string& id,
+                             const std::vector<TypeNode>& params,
+                             TypeNode t) const override;
+
+  /** Print define-fun command */
+  void toStreamCmdDefineFunction(std::ostream& out,
+                                 const std::string& id,
+                                 const std::vector<Node>& formals,
+                                 TypeNode range,
+                                 Node formula) const override;
+
+  /** Print define-named-fun command */
+  void toStreamCmdDefineNamedFunction(std::ostream& out,
+                                      const std::string& id,
+                                      const std::vector<Node>& formals,
+                                      TypeNode range,
+                                      Node formula) const override;
+
+  /** Print check-sat command */
+  void toStreamCmdCheckSat(std::ostream& out,
+                           Node n = Node::null()) const override;
+
+  /** Print check-sat-assuming command */
+  void toStreamCmdCheckSatAssuming(
+      std::ostream& out, const std::vector<Node>& nodes) const override;
+
+  /** Print query command */
+  void toStreamCmdQuery(std::ostream& out, Node n) const override;
+
+  /** Print simplify command */
+  void toStreamCmdSimplify(std::ostream& out, Node nodes) const override;
+
+  /** Print get-value command */
+  void toStreamCmdGetValue(std::ostream& out,
+                           const std::vector<Node>& n) const override;
+
+  /** Print get-assignment command */
+  void toStreamCmdGetAssignment(std::ostream& out) const override;
+
+  /** Print get-model command */
+  void toStreamCmdGetModel(std::ostream& out) const override;
+
+  /** Print get-proof command */
+  void toStreamCmdGetProof(std::ostream& out) const override;
+
+  /** Print get-unsat-core command */
+  void toStreamCmdGetUnsatCore(std::ostream& out) const override;
+
+  /** Print get-assertions command */
+  void toStreamCmdGetAssertions(std::ostream& out) const override;
+
+  /** Print set-info :status command */
+  void toStreamCmdSetBenchmarkStatus(std::ostream& out,
+                                     BenchmarkStatus status) const override;
+
+  /** Print set-logic command */
+  void toStreamCmdSetBenchmarkLogic(std::ostream& out,
+                                    const std::string& logic) const override;
+
+  /** Print set-info command */
+  void toStreamCmdSetInfo(std::ostream& out,
+                          const std::string& flag,
+                          SExpr sexpr) const override;
+
+  /** Print get-info command */
+  void toStreamCmdGetInfo(std::ostream& out,
+                          const std::string& flag) const override;
+
+  /** Print set-option command */
+  void toStreamCmdSetOption(std::ostream& out,
+                            const std::string& flag,
+                            SExpr sexpr) const override;
+
+  /** Print get-option command */
+  void toStreamCmdGetOption(std::ostream& out,
+                            const std::string& flag) const override;
+
+  /** Print declare-datatype(s) command */
+  void toStreamCmdDatatypeDeclaration(
+      std::ostream& out, const std::vector<TypeNode>& datatypes) const override;
+
+  /** Print reset command */
+  void toStreamCmdReset(std::ostream& out) const override;
+
+  /** Print reset-assertions command */
+  void toStreamCmdResetAssertions(std::ostream& out) const override;
+
+  /** Print quit command */
+  void toStreamCmdQuit(std::ostream& out) const override;
+
+  /** Print comment command */
+  void toStreamCmdComment(std::ostream& out,
+                          const std::string& comment) const override;
+
+  /** Print command sequence command */
+  void toStreamCmdCommandSequence(
+      std::ostream& out, const std::vector<Command*>& sequence) const override;
+
+  /** Print declaration sequence command */
+  void toStreamCmdDeclarationSequence(
+      std::ostream& out, const std::vector<Command*>& sequence) const override;
+
  private:
   void toStream(std::ostream& out, TNode n, int toDepth, bool types) const;
   void toStream(std::ostream& out,
                 const Model& m,
                 const Command* c) const override;
-};/* class AstPrinter */
+}; /* class AstPrinter */
 
-}/* CVC4::printer::ast namespace */
-}/* CVC4::printer namespace */
-}/* CVC4 namespace */
+}  // namespace ast
+}  // namespace printer
+}  // namespace CVC4
 
 #endif /* CVC4__PRINTER__AST_PRINTER_H */
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 243592456..8120d1d88 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -1038,57 +1038,6 @@ void CvcPrinter::toStream(
 template <class T>
 static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode);
 
-void CvcPrinter::toStream(std::ostream& out,
-                          const Command* c,
-                          int toDepth,
-                          bool types,
-                          size_t dag) const
-{
-  expr::ExprSetDepth::Scope sdScope(out, toDepth);
-  expr::ExprPrintTypes::Scope ptScope(out, types);
-  expr::ExprDag::Scope dagScope(out, dag);
-
-  if(tryToStream<AssertCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<PushCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<PopCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<CheckSatCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<CheckSatAssumingCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<QueryCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<ResetCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<ResetAssertionsCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<QuitCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<DeclarationSequence>(out, c, d_cvc3Mode) ||
-     tryToStream<CommandSequence>(out, c, d_cvc3Mode) ||
-     tryToStream<DeclareFunctionCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<DeclareTypeCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<DefineTypeCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<DefineNamedFunctionCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<DefineFunctionCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<SimplifyCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<GetValueCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<GetModelCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<GetAssignmentCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<GetAssertionsCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<GetProofCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<GetUnsatCoreCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<SetBenchmarkStatusCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<SetBenchmarkLogicCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<SetInfoCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<GetInfoCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<SetOptionCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<GetOptionCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<DatatypeDeclarationCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<CommentCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<EmptyCommand>(out, c, d_cvc3Mode) ||
-     tryToStream<EchoCommand>(out, c, d_cvc3Mode)) {
-    return;
-  }
-
-  out << "ERROR: don't know how to print a Command of class: "
-      << typeid(*c).name() << endl;
-
-}/* CvcPrinter::toStream(Command*) */
-
 template <class T>
 static bool tryToStream(std::ostream& out,
                         const CommandStatus* s,
@@ -1245,294 +1194,316 @@ void CvcPrinter::toStream(std::ostream& out,
   }
 }
 
-static void toStream(std::ostream& out, const AssertCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdAssert(std::ostream& out, Node n) const
 {
-  out << "ASSERT " << c->getExpr() << ";";
+  out << "ASSERT " << n << ';';
 }
 
-static void toStream(std::ostream& out, const PushCommand* c, bool cvc3Mode)
-{
-  out << "PUSH;";
-}
+void CvcPrinter::toStreamCmdPush(std::ostream& out) const { out << "PUSH;"; }
 
-static void toStream(std::ostream& out, const PopCommand* c, bool cvc3Mode)
-{
-  out << "POP;";
-}
+void CvcPrinter::toStreamCmdPop(std::ostream& out) const { out << "POP;"; }
 
-static void toStream(std::ostream& out, const CheckSatCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdCheckSat(std::ostream& out, Node n) const
 {
-  Expr e = c->getExpr();
-  if(cvc3Mode) {
+  if (d_cvc3Mode)
+  {
     out << "PUSH; ";
   }
-  if(!e.isNull()) {
-    out << "CHECKSAT " << e << ";";
-  } else {
+  if (!n.isNull())
+  {
+    out << "CHECKSAT " << n << ';';
+  }
+  else
+  {
     out << "CHECKSAT;";
   }
-  if(cvc3Mode) {
+  if (d_cvc3Mode)
+  {
     out << " POP;";
   }
 }
 
-static void toStream(std::ostream& out,
-                     const CheckSatAssumingCommand* c,
-                     bool cvc3Mode)
+void CvcPrinter::toStreamCmdCheckSatAssuming(
+    std::ostream& out, const std::vector<Node>& nodes) const
 {
-  const vector<Expr>& exprs = c->getTerms();
-  if (cvc3Mode)
+  if (d_cvc3Mode)
   {
     out << "PUSH; ";
   }
   out << "CHECKSAT";
-  if (exprs.size() > 0)
+  if (nodes.size() > 0)
   {
-    out << " " << exprs[0];
-    for (size_t i = 1, n = exprs.size(); i < n; ++i)
+    out << ' ' << nodes[0];
+    for (size_t i = 1, n = nodes.size(); i < n; ++i)
     {
-      out << " AND " << exprs[i];
+      out << " AND " << nodes[i];
     }
   }
-  out << ";";
-  if (cvc3Mode)
+  out << ';';
+  if (d_cvc3Mode)
   {
     out << " POP;";
   }
 }
 
-static void toStream(std::ostream& out, const QueryCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdQuery(std::ostream& out, Node n) const
 {
-  Expr e = c->getExpr();
-  if(cvc3Mode) {
+  if (d_cvc3Mode)
+  {
     out << "PUSH; ";
   }
-  if(!e.isNull()) {
-    out << "QUERY " << e << ";";
-  } else {
+  if (!n.isNull())
+  {
+    out << "QUERY " << n << ';';
+  }
+  else
+  {
     out << "QUERY TRUE;";
   }
-  if(cvc3Mode) {
+  if (d_cvc3Mode)
+  {
     out << " POP;";
   }
 }
 
-static void toStream(std::ostream& out, const ResetCommand* c, bool cvc3Mode)
-{
-  out << "RESET;";
-}
+void CvcPrinter::toStreamCmdReset(std::ostream& out) const { out << "RESET;"; }
 
-static void toStream(std::ostream& out,
-                     const ResetAssertionsCommand* c,
-                     bool cvc3Mode)
+void CvcPrinter::toStreamCmdResetAssertions(std::ostream& out) const
 {
   out << "RESET ASSERTIONS;";
 }
 
-static void toStream(std::ostream& out, const QuitCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdQuit(std::ostream& out) const
 {
-  //out << "EXIT;";
+  // out << "EXIT;";
 }
 
-static void toStream(std::ostream& out, const CommandSequence* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdCommandSequence(
+    std::ostream& out, const std::vector<Command*>& sequence) const
 {
-  for(CommandSequence::const_iterator i = c->begin();
-      i != c->end();
-      ++i) {
+  for (CommandSequence::const_iterator i = sequence.cbegin();
+       i != sequence.cend();
+       ++i)
+  {
     out << *i << endl;
   }
 }
 
-static void toStream(std::ostream& out,
-                     const DeclarationSequence* c,
-                     bool cvc3Mode)
+void CvcPrinter::toStreamCmdDeclarationSequence(
+    std::ostream& out, const std::vector<Command*>& sequence) const
 {
-  DeclarationSequence::const_iterator i = c->begin();
-  for(;;) {
+  DeclarationSequence::const_iterator i = sequence.cbegin();
+  for (;;)
+  {
     DeclarationDefinitionCommand* dd =
-      static_cast<DeclarationDefinitionCommand*>(*i++);
-    if(i != c->end()) {
+        static_cast<DeclarationDefinitionCommand*>(*i++);
+    if (i != sequence.cend())
+    {
       out << dd->getSymbol() << ", ";
-    } else {
+    }
+    else
+    {
       out << *dd;
       break;
     }
   }
 }
 
-static void toStream(std::ostream& out,
-                     const DeclareFunctionCommand* c,
-                     bool cvc3Mode)
+void CvcPrinter::toStreamCmdDeclareFunction(std::ostream& out,
+                                            const std::string& id,
+                                            TypeNode type) const
 {
-  out << c->getSymbol() << " : " << c->getType() << ";";
+  out << id << " : " << type << ';';
 }
 
-static void toStream(std::ostream& out,
-                     const DefineFunctionCommand* c,
-                     bool cvc3Mode)
+void CvcPrinter::toStreamCmdDefineFunction(std::ostream& out,
+                                           const std::string& id,
+                                           const std::vector<Node>& formals,
+                                           TypeNode range,
+                                           Node formula) const
 {
-  Expr func = c->getFunction();
-  const vector<Expr>& formals = c->getFormals();
-  Expr formula = c->getFormula();
-  out << func << " : " << func.getType() << " = ";
-  if(formals.size() > 0) {
+  std::vector<TypeNode> sorts;
+  sorts.reserve(formals.size() + 1);
+  for (const Node& n : formals)
+  {
+    sorts.push_back(n.getType());
+  }
+  sorts.push_back(range);
+
+  out << id << " : " << NodeManager::currentNM()->mkFunctionType(sorts)
+      << " = ";
+  if (formals.size() > 0)
+  {
     out << "LAMBDA(";
-    vector<Expr>::const_iterator i = formals.begin();
-    while(i != formals.end()) {
+    vector<Node>::const_iterator i = formals.cbegin();
+    while (i != formals.end())
+    {
       out << (*i) << ":" << (*i).getType();
-      if(++i != formals.end()) {
+      if (++i != formals.end())
+      {
         out << ", ";
       }
     }
     out << "): ";
   }
-  out << formula << ";";
+  out << formula << ';';
 }
 
-static void toStream(std::ostream& out,
-                     const DeclareTypeCommand* c,
-                     bool cvc3Mode)
+void CvcPrinter::toStreamCmdDeclareType(std::ostream& out,
+                                        const std::string& id,
+                                        size_t arity,
+                                        TypeNode type) const
 {
-  if(c->getArity() > 0) {
-    //TODO?
+  if (arity > 0)
+  {
+    // TODO?
     out << "ERROR: Don't know how to print parameterized type declaration "
-           "in CVC language." << endl;
-  } else {
-    out << c->getSymbol() << " : TYPE;";
+           "in CVC language."
+        << std::endl;
+  }
+  else
+  {
+    out << id << " : TYPE;";
   }
 }
 
-static void toStream(std::ostream& out,
-                     const DefineTypeCommand* c,
-                     bool cvc3Mode)
+void CvcPrinter::toStreamCmdDefineType(std::ostream& out,
+                                       const std::string& id,
+                                       const std::vector<TypeNode>& params,
+                                       TypeNode t) const
 {
-  if(c->getParameters().size() > 0) {
+  if (params.size() > 0)
+  {
     out << "ERROR: Don't know how to print parameterized type definition "
-           "in CVC language:" << endl << c->toString() << endl;
-  } else {
-    out << c->getSymbol() << " : TYPE = " << c->getType() << ";";
+           "in CVC language:"
+        << std::endl;
+  }
+  else
+  {
+    out << id << " : TYPE = " << t << ';';
   }
 }
 
-static void toStream(std::ostream& out,
-                     const DefineNamedFunctionCommand* c,
-                     bool cvc3Mode)
+void CvcPrinter::toStreamCmdDefineNamedFunction(
+    std::ostream& out,
+    const std::string& id,
+    const std::vector<Node>& formals,
+    TypeNode range,
+    Node formula) const
 {
-  toStream(out, static_cast<const DefineFunctionCommand*>(c), cvc3Mode);
+  toStreamCmdDefineFunction(out, id, formals, range, formula);
 }
 
-static void toStream(std::ostream& out, const SimplifyCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const
 {
-  out << "TRANSFORM " << c->getTerm() << ";";
+  out << "TRANSFORM " << n << ';';
 }
 
-static void toStream(std::ostream& out, const GetValueCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdGetValue(std::ostream& out,
+                                     const std::vector<Node>& nodes) const
 {
-  const vector<Expr>& terms = c->getTerms();
-  Assert(!terms.empty());
+  Assert(!nodes.empty());
   out << "GET_VALUE ";
-  copy(terms.begin(), terms.end() - 1, ostream_iterator<Expr>(out, ";\nGET_VALUE "));
-  out << terms.back() << ";";
+  copy(nodes.begin(),
+       nodes.end() - 1,
+       ostream_iterator<Node>(out, ";\nGET_VALUE "));
+  out << nodes.back() << ';';
 }
 
-static void toStream(std::ostream& out, const GetModelCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdGetModel(std::ostream& out) const
 {
   out << "COUNTERMODEL;";
 }
 
-static void toStream(std::ostream& out,
-                     const GetAssignmentCommand* c,
-                     bool cvc3Mode)
+void CvcPrinter::toStreamCmdGetAssignment(std::ostream& out) const
 {
   out << "% (get-assignment)";
 }
 
-static void toStream(std::ostream& out,
-                     const GetAssertionsCommand* c,
-                     bool cvc3Mode)
+void CvcPrinter::toStreamCmdGetAssertions(std::ostream& out) const
 {
   out << "WHERE;";
 }
 
-static void toStream(std::ostream& out, const GetProofCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdGetProof(std::ostream& out) const
 {
   out << "DUMP_PROOF;";
 }
 
-static void toStream(std::ostream& out,
-                     const GetUnsatCoreCommand* c,
-                     bool cvc3Mode)
+void CvcPrinter::toStreamCmdGetUnsatCore(std::ostream& out) const
 {
   out << "DUMP_UNSAT_CORE;";
 }
 
-static void toStream(std::ostream& out,
-                     const SetBenchmarkStatusCommand* c,
-                     bool cvc3Mode)
+void CvcPrinter::toStreamCmdSetBenchmarkStatus(std::ostream& out,
+                                               BenchmarkStatus status) const
 {
-  out << "% (set-info :status " << c->getStatus() << ")";
+  out << "% (set-info :status " << status << ')';
 }
 
-static void toStream(std::ostream& out,
-                     const SetBenchmarkLogicCommand* c,
-                     bool cvc3Mode)
+void CvcPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out,
+                                              const std::string& logic) const
 {
-  out << "OPTION \"logic\" \"" << c->getLogic() << "\";";
+  out << "OPTION \"logic\" \"" << logic << "\";";
 }
 
-static void toStream(std::ostream& out, const SetInfoCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdSetInfo(std::ostream& out,
+                                    const std::string& flag,
+                                    SExpr sexpr) const
 {
-  out << "% (set-info " << c->getFlag() << " ";
+  out << "% (set-info " << flag << ' ';
   OutputLanguage language =
-      cvc3Mode ? language::output::LANG_CVC3 : language::output::LANG_CVC4;
-  SExpr::toStream(out, c->getSExpr(), language);
-  out << ")";
+      d_cvc3Mode ? language::output::LANG_CVC3 : language::output::LANG_CVC4;
+  SExpr::toStream(out, sexpr, language);
+  out << ')';
 }
 
-static void toStream(std::ostream& out, const GetInfoCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdGetInfo(std::ostream& out,
+                                    const std::string& flag) const
 {
-  out << "% (get-info " << c->getFlag() << ")";
+  out << "% (get-info " << flag << ')';
 }
 
-static void toStream(std::ostream& out,
-                     const SetOptionCommand* c,
-                     bool cvc3Mode)
+void CvcPrinter::toStreamCmdSetOption(std::ostream& out,
+                                      const std::string& flag,
+                                      SExpr sexpr) const
 {
-  out << "OPTION \"" << c->getFlag() << "\" ";
-  SExpr::toStream(out, c->getSExpr(), language::output::LANG_CVC4);
-  out << ";";
+  out << "OPTION \"" << flag << "\" ";
+  SExpr::toStream(out, sexpr, language::output::LANG_CVC4);
+  out << ';';
 }
 
-static void toStream(std::ostream& out,
-                     const GetOptionCommand* c,
-                     bool cvc3Mode)
+void CvcPrinter::toStreamCmdGetOption(std::ostream& out,
+                                      const std::string& flag) const
 {
-  out << "% (get-option " << c->getFlag() << ")";
+  out << "% (get-option " << flag << ')';
 }
 
-static void toStream(std::ostream& out,
-                     const DatatypeDeclarationCommand* c,
-                     bool cvc3Mode)
+void CvcPrinter::toStreamCmdDatatypeDeclaration(
+    std::ostream& out, const std::vector<TypeNode>& datatypes) const
 {
-  const vector<Type>& datatypes = c->getDatatypes();
   Assert(!datatypes.empty() && datatypes[0].isDatatype());
-  const DType& dt0 = TypeNode::fromType(datatypes[0]).getDType();
-  //do not print tuple/datatype internal declarations
+  const DType& dt0 = datatypes[0].getDType();
+  // do not print tuple/datatype internal declarations
   if (datatypes.size() != 1 || (!dt0.isTuple() && !dt0.isRecord()))
   {
     out << "DATATYPE" << endl;
     bool firstDatatype = true;
-    for (const Type& t : datatypes)
+    for (const TypeNode& t : datatypes)
     {
-      if(! firstDatatype) {
+      if (!firstDatatype)
+      {
         out << ',' << endl;
       }
-      const DType& dt = TypeNode::fromType(t).getDType();
+      const DType& dt = t.getDType();
       out << "  " << dt.getName();
-      if(dt.isParametric()) {
+      if (dt.isParametric())
+      {
         out << '[';
-        for(size_t j = 0; j < dt.getNumParameters(); ++j) {
-          if(j > 0) {
+        for (size_t j = 0; j < dt.getNumParameters(); ++j)
+        {
+          if (j > 0)
+          {
             out << ',';
           }
           out << dt.getParameter(j);
@@ -1578,16 +1549,21 @@ static void toStream(std::ostream& out,
   }
 }
 
-static void toStream(std::ostream& out, const CommentCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdComment(std::ostream& out,
+                                    const std::string& comment) const
 {
-  out << "% " << c->getComment();
+  out << "% " << comment;
 }
 
-static void toStream(std::ostream& out, const EmptyCommand* c, bool cvc3Mode) {}
+void CvcPrinter::toStreamCmdEmpty(std::ostream& out,
+                                  const std::string& name) const
+{
+}
 
-static void toStream(std::ostream& out, const EchoCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdEcho(std::ostream& out,
+                                 const std::string& output) const
 {
-  out << "ECHO \"" << c->getOutput() << "\";";
+  out << "ECHO \"" << output << "\";";
 }
 
 template <class T>
diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h
index f5a06a082..0fd3d3a49 100644
--- a/src/printer/cvc/cvc_printer.h
+++ b/src/printer/cvc/cvc_printer.h
@@ -27,23 +27,151 @@ namespace CVC4 {
 namespace printer {
 namespace cvc {
 
-class CvcPrinter : public CVC4::Printer {
+class CvcPrinter : public CVC4::Printer
+{
  public:
   using CVC4::Printer::toStream;
-  CvcPrinter(bool cvc3Mode = false) : d_cvc3Mode(cvc3Mode) { }
+  CvcPrinter(bool cvc3Mode = false) : d_cvc3Mode(cvc3Mode) {}
   void toStream(std::ostream& out,
                 TNode n,
                 int toDepth,
                 bool types,
                 size_t dag) const override;
-  void toStream(std::ostream& out,
-                const Command* c,
-                int toDepth,
-                bool types,
-                size_t dag) const override;
   void toStream(std::ostream& out, const CommandStatus* s) const override;
   void toStream(std::ostream& out, const Model& m) const override;
 
+  /** Print empty command */
+  void toStreamCmdEmpty(std::ostream& out,
+                        const std::string& name) const override;
+
+  /** Print echo command */
+  void toStreamCmdEcho(std::ostream& out,
+                       const std::string& output) const override;
+
+  /** Print assert command */
+  void toStreamCmdAssert(std::ostream& out, Node n) const override;
+
+  /** Print push command */
+  void toStreamCmdPush(std::ostream& out) const override;
+
+  /** Print pop command */
+  void toStreamCmdPop(std::ostream& out) const override;
+
+  /** Print declare-fun command */
+  void toStreamCmdDeclareFunction(std::ostream& out,
+                                  const std::string& id,
+                                  TypeNode type) const override;
+
+  /** Print declare-sort command */
+  void toStreamCmdDeclareType(std::ostream& out,
+                              const std::string& id,
+                              size_t arity,
+                              TypeNode type) const override;
+
+  /** Print define-sort command */
+  void toStreamCmdDefineType(std::ostream& out,
+                             const std::string& id,
+                             const std::vector<TypeNode>& params,
+                             TypeNode t) const override;
+
+  /** Print define-fun command */
+  void toStreamCmdDefineFunction(std::ostream& out,
+                                 const std::string& id,
+                                 const std::vector<Node>& formals,
+                                 TypeNode range,
+                                 Node formula) const override;
+
+  /** Print define-named-fun command */
+  void toStreamCmdDefineNamedFunction(std::ostream& out,
+                                      const std::string& id,
+                                      const std::vector<Node>& formals,
+                                      TypeNode range,
+                                      Node formula) const override;
+
+  /** Print check-sat command */
+  void toStreamCmdCheckSat(std::ostream& out,
+                           Node n = Node::null()) const override;
+
+  /** Print check-sat-assuming command */
+  void toStreamCmdCheckSatAssuming(
+      std::ostream& out, const std::vector<Node>& nodes) const override;
+
+  /** Print query command */
+  void toStreamCmdQuery(std::ostream& out, Node n) const override;
+
+  /** Print simplify command */
+  void toStreamCmdSimplify(std::ostream& out, Node nodes) const override;
+
+  /** Print get-value command */
+  void toStreamCmdGetValue(std::ostream& out,
+                           const std::vector<Node>& n) const override;
+
+  /** Print get-assignment command */
+  void toStreamCmdGetAssignment(std::ostream& out) const override;
+
+  /** Print get-model command */
+  void toStreamCmdGetModel(std::ostream& out) const override;
+
+  /** Print get-proof command */
+  void toStreamCmdGetProof(std::ostream& out) const override;
+
+  /** Print get-unsat-core command */
+  void toStreamCmdGetUnsatCore(std::ostream& out) const override;
+
+  /** Print get-assertions command */
+  void toStreamCmdGetAssertions(std::ostream& out) const override;
+
+  /** Print set-info :status command */
+  void toStreamCmdSetBenchmarkStatus(std::ostream& out,
+                                     BenchmarkStatus status) const override;
+
+  /** Print set-logic command */
+  void toStreamCmdSetBenchmarkLogic(std::ostream& out,
+                                    const std::string& logic) const override;
+
+  /** Print set-info command */
+  void toStreamCmdSetInfo(std::ostream& out,
+                          const std::string& flag,
+                          SExpr sexpr) const override;
+
+  /** Print get-info command */
+  void toStreamCmdGetInfo(std::ostream& out,
+                          const std::string& flag) const override;
+
+  /** Print set-option command */
+  void toStreamCmdSetOption(std::ostream& out,
+                            const std::string& flag,
+                            SExpr sexpr) const override;
+
+  /** Print get-option command */
+  void toStreamCmdGetOption(std::ostream& out,
+                            const std::string& flag) const override;
+
+  /** Print declare-datatype(s) command */
+  void toStreamCmdDatatypeDeclaration(
+      std::ostream& out, const std::vector<TypeNode>& datatypes) const override;
+
+  /** Print reset command */
+  void toStreamCmdReset(std::ostream& out) const override;
+
+  /** Print reset-assertions command */
+  void toStreamCmdResetAssertions(std::ostream& out) const override;
+
+  /** Print quit command */
+  void toStreamCmdQuit(std::ostream& out) const override;
+
+  /** Print comment command */
+  void toStreamCmdComment(std::ostream& out,
+                          const std::string& comment) const override;
+
+  /** Print command sequence command */
+  void toStreamCmdCommandSequence(
+      std::ostream& out, const std::vector<Command*>& sequence) const override;
+
+  /** Print declaration sequence command */
+  void toStreamCmdDeclarationSequence(
+      std::ostream& out, const std::vector<Command*>& sequence) const override;
+
  private:
   void toStream(
       std::ostream& out, TNode n, int toDepth, bool types, bool bracket) const;
@@ -52,10 +180,10 @@ class CvcPrinter : public CVC4::Printer {
                 const Command* c) const override;
 
   bool d_cvc3Mode;
-};/* class CvcPrinter */
+}; /* class CvcPrinter */
 
-}/* CVC4::printer::cvc namespace */
-}/* CVC4::printer namespace */
-}/* CVC4 namespace */
+}  // namespace cvc
+}  // namespace printer
+}  // namespace CVC4
 
 #endif /* CVC4__PRINTER__CVC_PRINTER_H */
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 4b1fbbe22..0e7550518 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -85,8 +85,7 @@ void Printer::toStream(std::ostream& out, const Model& m) const
 void Printer::toStream(std::ostream& out, const UnsatCore& core) const
 {
   for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
-    AssertCommand cmd(*i);
-    toStream(out, &cmd, -1, false, -1);
+    toStreamCmdAssert(out, Node::fromExpr(*i));
     out << std::endl;
   }
 }/* Printer::toStream(UnsatCore) */
@@ -117,23 +116,316 @@ Printer* Printer::getPrinter(OutputLanguage lang)
   return d_printers[lang].get();
 }
 
-/**
- * Write an error to `out` stating that command `name` is not supported by this
- * printer.
- */
-void printUnknownCommand(std::ostream& out, const std::string& name)
+void Printer::printUnknownCommand(std::ostream& out,
+                                  const std::string& name) const
 {
   out << "ERROR: don't know how to print " << name << " command" << std::endl;
 }
 
+void Printer::toStreamCmdEmpty(std::ostream& out, const std::string& name) const
+{
+  printUnknownCommand(out, "empty");
+}
+
+void Printer::toStreamCmdEcho(std::ostream& out,
+                              const std::string& output) const
+{
+  printUnknownCommand(out, "echo");
+}
+
+void Printer::toStreamCmdAssert(std::ostream& out, Node n) const
+{
+  printUnknownCommand(out, "assert");
+}
+
+void Printer::toStreamCmdPush(std::ostream& out) const
+{
+  printUnknownCommand(out, "push");
+}
+
+void Printer::toStreamCmdPop(std::ostream& out) const
+{
+  printUnknownCommand(out, "pop");
+}
+
+void Printer::toStreamCmdDeclareFunction(std::ostream& out,
+                                         const std::string& id,
+                                         TypeNode type) const
+{
+  printUnknownCommand(out, "declare-fun");
+}
+
+void Printer::toStreamCmdDeclareType(std::ostream& out,
+                                     const std::string& id,
+                                     size_t arity,
+                                     TypeNode type) const
+{
+  printUnknownCommand(out, "declare-sort");
+}
+
+void Printer::toStreamCmdDefineType(std::ostream& out,
+                                    const std::string& id,
+                                    const std::vector<TypeNode>& params,
+                                    TypeNode t) const
+{
+  printUnknownCommand(out, "define-sort");
+}
+
+void Printer::toStreamCmdDefineFunction(std::ostream& out,
+                                        const std::string& id,
+                                        const std::vector<Node>& formals,
+                                        TypeNode range,
+                                        Node formula) const
+{
+  printUnknownCommand(out, "define-fun");
+}
+
+void Printer::toStreamCmdDefineNamedFunction(std::ostream& out,
+                                             const std::string& id,
+                                             const std::vector<Node>& formals,
+                                             TypeNode range,
+                                             Node formula) const
+{
+  printUnknownCommand(out, "define-named-function");
+}
+
+void Printer::toStreamCmdDefineFunctionRec(
+    std::ostream& out,
+    const std::vector<Node>& funcs,
+    const std::vector<std::vector<Node>>& formals,
+    const std::vector<Node>& formulas) const
+{
+  printUnknownCommand(out, "define-fun-rec");
+}
+
+void Printer::toStreamCmdSetUserAttribute(std::ostream& out,
+                                          const std::string& attr,
+                                          Node n) const
+{
+  printUnknownCommand(out, "set-user-attribute");
+}
+
+void Printer::toStreamCmdCheckSat(std::ostream& out, Node n) const
+{
+  printUnknownCommand(out, "check-sat");
+}
+
+void Printer::toStreamCmdCheckSatAssuming(std::ostream& out,
+                                          const std::vector<Node>& nodes) const
+{
+  printUnknownCommand(out, "check-sat-assuming");
+}
+
+void Printer::toStreamCmdQuery(std::ostream& out, Node n) const
+{
+  printUnknownCommand(out, "query");
+}
+
+void Printer::toStreamCmdDeclareVar(std::ostream& out,
+                                    Node var,
+                                    TypeNode type) const
+{
+  printUnknownCommand(out, "declare-var");
+}
+
 void Printer::toStreamCmdSynthFun(std::ostream& out,
                                   const std::string& sym,
                                   const std::vector<Node>& vars,
                                   TypeNode range,
                                   bool isInv,
-                                  TypeNode sygusType)
+                                  TypeNode sygusType) const
+{
+  printUnknownCommand(out, isInv ? "synth-inv" : "synth-fun");
+}
+
+void Printer::toStreamCmdConstraint(std::ostream& out, Node n) const
+{
+  printUnknownCommand(out, "constraint");
+}
+
+void Printer::toStreamCmdInvConstraint(
+    std::ostream& out, Node inv, Node pre, Node trans, Node post) const
+{
+  printUnknownCommand(out, "inv-constraint");
+}
+
+void Printer::toStreamCmdCheckSynth(std::ostream& out) const
+{
+  printUnknownCommand(out, "check-synth");
+}
+
+void Printer::toStreamCmdSimplify(std::ostream& out, Node n) const
+{
+  printUnknownCommand(out, "simplify");
+}
+
+void Printer::toStreamCmdExpandDefinitions(std::ostream& out, Node n) const
+{
+  printUnknownCommand(out, "expand-definitions");
+}
+
+void Printer::toStreamCmdGetValue(std::ostream& out,
+                                  const std::vector<Node>& nodes) const
+{
+  printUnknownCommand(out, "get-value");
+}
+
+void Printer::toStreamCmdGetAssignment(std::ostream& out) const
+{
+  printUnknownCommand(out, "get-assignment");
+}
+
+void Printer::toStreamCmdGetModel(std::ostream& out) const
+{
+  printUnknownCommand(out, "ge-model");
+}
+
+void Printer::toStreamCmdBlockModel(std::ostream& out) const
+{
+  printUnknownCommand(out, "block-model");
+}
+
+void Printer::toStreamCmdBlockModelValues(std::ostream& out,
+                                          const std::vector<Node>& nodes) const
+{
+  printUnknownCommand(out, "block-model-values");
+}
+
+void Printer::toStreamCmdGetProof(std::ostream& out) const
+{
+  printUnknownCommand(out, "get-proof");
+}
+
+void Printer::toStreamCmdGetInstantiations(std::ostream& out) const
+{
+  printUnknownCommand(out, "get-instantiations");
+}
+
+void Printer::toStreamCmdGetSynthSolution(std::ostream& out) const
+{
+  printUnknownCommand(out, "get-synth-solution");
+}
+
+void Printer::toStreamCmdGetInterpol(std::ostream& out,
+                                     const std::string& name,
+                                     Node conj,
+                                     TypeNode sygusType) const
+{
+  printUnknownCommand(out, "get-interpol");
+}
+
+void Printer::toStreamCmdGetAbduct(std::ostream& out,
+                                   const std::string& name,
+                                   Node conj,
+                                   TypeNode sygusType) const
+{
+  printUnknownCommand(out, "get-abduct");
+}
+
+void Printer::toStreamCmdGetQuantifierElimination(std::ostream& out,
+                                                  Node n) const
+{
+  printUnknownCommand(out, "get-quantifier-elimination");
+}
+
+void Printer::toStreamCmdGetUnsatAssumptions(std::ostream& out) const
+{
+  printUnknownCommand(out, "get-unsat-assumption");
+}
+
+void Printer::toStreamCmdGetUnsatCore(std::ostream& out) const
+{
+  printUnknownCommand(out, "get-unsat-core");
+}
+
+void Printer::toStreamCmdGetAssertions(std::ostream& out) const
+{
+  printUnknownCommand(out, "get-assertions");
+}
+
+void Printer::toStreamCmdSetBenchmarkStatus(std::ostream& out,
+                                            BenchmarkStatus status) const
+{
+  printUnknownCommand(out, "set-info");
+}
+
+void Printer::toStreamCmdSetBenchmarkLogic(std::ostream& out,
+                                           const std::string& logic) const
+{
+  printUnknownCommand(out, "set-logic");
+}
+
+void Printer::toStreamCmdSetInfo(std::ostream& out,
+                                 const std::string& flag,
+                                 SExpr sexpr) const
+{
+  printUnknownCommand(out, "set-info");
+}
+
+void Printer::toStreamCmdGetInfo(std::ostream& out,
+                                 const std::string& flag) const
+{
+  printUnknownCommand(out, "get-info");
+}
+
+void Printer::toStreamCmdSetOption(std::ostream& out,
+                                   const std::string& flag,
+                                   SExpr sexpr) const
+{
+  printUnknownCommand(out, "set-option");
+}
+
+void Printer::toStreamCmdGetOption(std::ostream& out,
+                                   const std::string& flag) const
+{
+  printUnknownCommand(out, "get-option");
+}
+
+void Printer::toStreamCmdSetExpressionName(std::ostream& out,
+                                           Node n,
+                                           const std::string& name) const
+{
+  printUnknownCommand(out, "set-expression-name");
+}
+
+void Printer::toStreamCmdDatatypeDeclaration(
+    std::ostream& out, const std::vector<TypeNode>& datatypes) const
+{
+  printUnknownCommand(
+      out, datatypes.size() == 1 ? "declare-datatype" : "declare-datatypes");
+}
+
+void Printer::toStreamCmdReset(std::ostream& out) const
+{
+  printUnknownCommand(out, "reset");
+}
+
+void Printer::toStreamCmdResetAssertions(std::ostream& out) const
+{
+  printUnknownCommand(out, "reset-assertions");
+}
+
+void Printer::toStreamCmdQuit(std::ostream& out) const
+{
+  printUnknownCommand(out, "quit");
+}
+
+void Printer::toStreamCmdComment(std::ostream& out,
+                                 const std::string& comment) const
+{
+  printUnknownCommand(out, "comment");
+}
+
+void Printer::toStreamCmdCommandSequence(
+    std::ostream& out, const std::vector<Command*>& sequence) const
+{
+  printUnknownCommand(out, "sequence");
+}
+
+void Printer::toStreamCmdDeclarationSequence(
+    std::ostream& out, const std::vector<Command*>& sequence) const
 {
-  printUnknownCommand(out, "synth-fun");
+  printUnknownCommand(out, "sequence");
 }
 
 }/* CVC4 namespace */
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 918a95729..3b737ec5f 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -49,13 +49,6 @@ class Printer
                         bool types,
                         size_t dag) const = 0;
 
-  /** Write a Command out to a stream with this Printer. */
-  virtual void toStream(std::ostream& out,
-                        const Command* c,
-                        int toDepth,
-                        bool types,
-                        size_t dag) const = 0;
-
   /** Write a CommandStatus out to a stream with this Printer. */
   virtual void toStream(std::ostream& out, const CommandStatus* s) const = 0;
 
@@ -65,13 +58,211 @@ class Printer
   /** Write an UnsatCore out to a stream with this Printer. */
   virtual void toStream(std::ostream& out, const UnsatCore& core) const;
 
+  /** Print empty command */
+  virtual void toStreamCmdEmpty(std::ostream& out,
+                                const std::string& name) const;
+
+  /** Print echo command */
+  virtual void toStreamCmdEcho(std::ostream& out,
+                               const std::string& output) const;
+
+  /** Print assert command */
+  virtual void toStreamCmdAssert(std::ostream& out, Node n) const;
+
+  /** Print push command */
+  virtual void toStreamCmdPush(std::ostream& out) const;
+
+  /** Print pop command */
+  virtual void toStreamCmdPop(std::ostream& out) const;
+
+  /** Print declare-fun command */
+  virtual void toStreamCmdDeclareFunction(std::ostream& out,
+                                          const std::string& id,
+                                          TypeNode type) const;
+
+  /** Print declare-sort command */
+  virtual void toStreamCmdDeclareType(std::ostream& out,
+                                      const std::string& id,
+                                      size_t arity,
+                                      TypeNode type) const;
+
+  /** Print define-sort command */
+  virtual void toStreamCmdDefineType(std::ostream& out,
+                                     const std::string& id,
+                                     const std::vector<TypeNode>& params,
+                                     TypeNode t) const;
+
+  /** Print define-fun command */
+  virtual void toStreamCmdDefineFunction(std::ostream& out,
+                                         const std::string& id,
+                                         const std::vector<Node>& formals,
+                                         TypeNode range,
+                                         Node formula) const;
+
+  /** Print define-named-fun command */
+  virtual void toStreamCmdDefineNamedFunction(std::ostream& out,
+                                              const std::string& id,
+                                              const std::vector<Node>& formals,
+                                              TypeNode range,
+                                              Node formula) const;
+
+  /** Print define-fun-rec command */
+  virtual void toStreamCmdDefineFunctionRec(
+      std::ostream& out,
+      const std::vector<Node>& funcs,
+      const std::vector<std::vector<Node>>& formals,
+      const std::vector<Node>& formulas) const;
+
+  /** Print set-user-attribute command */
+  void toStreamCmdSetUserAttribute(std::ostream& out,
+                                   const std::string& attr,
+                                   Node n) const;
+
+  /** Print check-sat command */
+  virtual void toStreamCmdCheckSat(std::ostream& out,
+                                   Node n = Node::null()) const;
+
+  /** Print check-sat-assuming command */
+  virtual void toStreamCmdCheckSatAssuming(
+      std::ostream& out, const std::vector<Node>& nodes) const;
+
+  /** Print query command */
+  virtual void toStreamCmdQuery(std::ostream& out, Node n) const;
+
+  /** Print declare-var command */
+  virtual void toStreamCmdDeclareVar(std::ostream& out,
+                                     Node var,
+                                     TypeNode type) const;
+
   /** Print synth-fun command */
   virtual void toStreamCmdSynthFun(std::ostream& out,
                                    const std::string& sym,
                                    const std::vector<Node>& vars,
                                    TypeNode range,
                                    bool isInv,
-                                   TypeNode sygusType);
+                                   TypeNode sygusType) const;
+
+  /** Print constraint command */
+  virtual void toStreamCmdConstraint(std::ostream& out, Node n) const;
+
+  /** Print inv-constraint command */
+  virtual void toStreamCmdInvConstraint(
+      std::ostream& out, Node inv, Node pre, Node trans, Node post) const;
+
+  /** Print check-synth command */
+  virtual void toStreamCmdCheckSynth(std::ostream& out) const;
+
+  /** Print simplify command */
+  virtual void toStreamCmdSimplify(std::ostream& out, Node n) const;
+
+  /** Print expand-definitions command */
+  void toStreamCmdExpandDefinitions(std::ostream& out, Node n) const;
+
+  /** Print get-value command */
+  virtual void toStreamCmdGetValue(std::ostream& out,
+                                   const std::vector<Node>& nodes) const;
+
+  /** Print get-assignment command */
+  virtual void toStreamCmdGetAssignment(std::ostream& out) const;
+
+  /** Print get-model command */
+  virtual void toStreamCmdGetModel(std::ostream& out) const;
+
+  /** Print block-model command */
+  void toStreamCmdBlockModel(std::ostream& out) const;
+
+  /** Print block-model-values command */
+  void toStreamCmdBlockModelValues(std::ostream& out,
+                                   const std::vector<Node>& nodes) const;
+
+  /** Print get-proof command */
+  virtual void toStreamCmdGetProof(std::ostream& out) const;
+
+  /** Print get-instantiations command */
+  void toStreamCmdGetInstantiations(std::ostream& out) const;
+
+  /** Print get-synth-solution command */
+  void toStreamCmdGetSynthSolution(std::ostream& out) const;
+
+  /** Print get-interpol command */
+  void toStreamCmdGetInterpol(std::ostream& out,
+                              const std::string& name,
+                              Node conj,
+                              TypeNode sygusType) const;
+
+  /** Print get-abduct command */
+  virtual void toStreamCmdGetAbduct(std::ostream& out,
+                                    const std::string& name,
+                                    Node conj,
+                                    TypeNode sygusType) const;
+
+  /** Print get-quantifier-elimination command */
+  void toStreamCmdGetQuantifierElimination(std::ostream& out, Node n) const;
+
+  /** Print get-unsat-assumptions command */
+  virtual void toStreamCmdGetUnsatAssumptions(std::ostream& out) const;
+
+  /** Print get-unsat-core command */
+  virtual void toStreamCmdGetUnsatCore(std::ostream& out) const;
+
+  /** Print get-assertions command */
+  virtual void toStreamCmdGetAssertions(std::ostream& out) const;
+
+  /** Print set-info :status command */
+  virtual void toStreamCmdSetBenchmarkStatus(std::ostream& out,
+                                             BenchmarkStatus status) const;
+
+  /** Print set-logic command */
+  virtual void toStreamCmdSetBenchmarkLogic(std::ostream& out,
+                                            const std::string& logic) const;
+
+  /** Print set-info command */
+  virtual void toStreamCmdSetInfo(std::ostream& out,
+                                  const std::string& flag,
+                                  SExpr sexpr) const;
+
+  /** Print get-info command */
+  virtual void toStreamCmdGetInfo(std::ostream& out,
+                                  const std::string& flag) const;
+
+  /** Print set-option command */
+  virtual void toStreamCmdSetOption(std::ostream& out,
+                                    const std::string& flag,
+                                    SExpr sexpr) const;
+
+  /** Print get-option command */
+  virtual void toStreamCmdGetOption(std::ostream& out,
+                                    const std::string& flag) const;
+
+  /** Print set-expression-name command */
+  void toStreamCmdSetExpressionName(std::ostream& out,
+                                    Node n,
+                                    const std::string& name) const;
+
+  /** Print declare-datatype(s) command */
+  virtual void toStreamCmdDatatypeDeclaration(
+      std::ostream& out, const std::vector<TypeNode>& datatypes) const;
+
+  /** Print reset command */
+  virtual void toStreamCmdReset(std::ostream& out) const;
+
+  /** Print reset-assertions command */
+  virtual void toStreamCmdResetAssertions(std::ostream& out) const;
+
+  /** Print quit command */
+  virtual void toStreamCmdQuit(std::ostream& out) const;
+
+  /** Print comment command */
+  virtual void toStreamCmdComment(std::ostream& out,
+                                  const std::string& comment) const;
+
+  /** Print command sequence command */
+  virtual void toStreamCmdCommandSequence(
+      std::ostream& out, const std::vector<Command*>& sequence) const;
+
+  /** Print declaration sequence command */
+  virtual void toStreamCmdDeclarationSequence(
+      std::ostream& out, const std::vector<Command*>& sequence) const;
 
  protected:
   /** Derived classes can construct, but no one else. */
@@ -91,6 +282,12 @@ class Printer
     getPrinter(lang)->toStream(out, m, c);
   }
 
+  /**
+   * Write an error to `out` stating that command `name` is not supported by
+   * this printer.
+   */
+  void printUnknownCommand(std::ostream& out, const std::string& name) const;
+
  private:
   /** Disallow copy, assignment  */
   Printer(const Printer&) = delete;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 96a7f634d..3d76c81dc 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1261,65 +1261,6 @@ static bool tryToStream(std::ostream& out, const Command* c);
 template <class T>
 static bool tryToStream(std::ostream& out, const Command* c, Variant v);
 
-void Smt2Printer::toStream(std::ostream& out,
-                           const Command* c,
-                           int toDepth,
-                           bool types,
-                           size_t dag) const
-{
-  expr::ExprSetDepth::Scope sdScope(out, toDepth);
-  expr::ExprPrintTypes::Scope ptScope(out, types);
-  expr::ExprDag::Scope dagScope(out, dag);
-
-  if (tryToStream<AssertCommand>(out, c) || tryToStream<PushCommand>(out, c)
-      || tryToStream<PopCommand>(out, c) || tryToStream<CheckSatCommand>(out, c)
-      || tryToStream<CheckSatAssumingCommand>(out, c)
-      || tryToStream<QueryCommand>(out, c, d_variant)
-      || tryToStream<ResetCommand>(out, c)
-      || tryToStream<ResetAssertionsCommand>(out, c)
-      || tryToStream<QuitCommand>(out, c)
-      || tryToStream<DeclarationSequence>(out, c)
-      || tryToStream<CommandSequence>(out, c)
-      || tryToStream<DeclareFunctionCommand>(out, c)
-      || tryToStream<DeclareTypeCommand>(out, c)
-      || tryToStream<DefineTypeCommand>(out, c)
-      || tryToStream<DefineNamedFunctionCommand>(out, c)
-      || tryToStream<DefineFunctionCommand>(out, c)
-      || tryToStream<DefineFunctionRecCommand>(out, c)
-      || tryToStream<SimplifyCommand>(out, c)
-      || tryToStream<GetValueCommand>(out, c)
-      || tryToStream<GetModelCommand>(out, c)
-      || tryToStream<GetAssignmentCommand>(out, c)
-      || tryToStream<GetAssertionsCommand>(out, c)
-      || tryToStream<GetProofCommand>(out, c)
-      || tryToStream<GetUnsatAssumptionsCommand>(out, c)
-      || tryToStream<GetUnsatCoreCommand>(out, c)
-      || tryToStream<SetBenchmarkStatusCommand>(out, c, d_variant)
-      || tryToStream<SetBenchmarkLogicCommand>(out, c, d_variant)
-      || tryToStream<SetInfoCommand>(out, c, d_variant)
-      || tryToStream<GetInfoCommand>(out, c)
-      || tryToStream<SetOptionCommand>(out, c)
-      || tryToStream<GetOptionCommand>(out, c)
-      || tryToStream<DatatypeDeclarationCommand>(out, c, d_variant)
-      || tryToStream<CommentCommand>(out, c, d_variant)
-      || tryToStream<EmptyCommand>(out, c)
-      || tryToStream<EchoCommand>(out, c, d_variant)
-      || tryToStream<DeclareSygusFunctionCommand>(out, c)
-      || tryToStream<DeclareSygusVarCommand>(out, c)
-      || tryToStream<SygusConstraintCommand>(out, c)
-      || tryToStream<SygusInvConstraintCommand>(out, c)
-      || tryToStream<CheckSynthCommand>(out, c)
-      || tryToStream<GetAbductCommand>(out, c))
-  {
-    return;
-  }
-
-  out << "ERROR: don't know how to print a Command of class: "
-      << typeid(*c).name() << endl;
-
-}/* Smt2Printer::toStream(Command*) */
-
-
 static std::string quoteSymbol(TNode n) {
   std::stringstream ss;
   ss << n;
@@ -1494,7 +1435,7 @@ void Smt2Printer::toStream(std::ostream& out,
   else if (const DatatypeDeclarationCommand* datatype_declaration_command =
                dynamic_cast<const DatatypeDeclarationCommand*>(command))
   {
-    toStream(out, datatype_declaration_command, -1, false, 1);
+    out << datatype_declaration_command;
   }
   else
   {
@@ -1502,147 +1443,156 @@ void Smt2Printer::toStream(std::ostream& out,
   }
 }
 
-static void toStream(std::ostream& out, const AssertCommand* c)
+void Smt2Printer::toStreamCmdAssert(std::ostream& out, Node n) const
 {
-  out << "(assert " << c->getExpr() << ")";
+  out << "(assert " << n << ')';
 }
 
-static void toStream(std::ostream& out, const PushCommand* c)
+void Smt2Printer::toStreamCmdPush(std::ostream& out) const
 {
   out << "(push 1)";
 }
 
-static void toStream(std::ostream& out, const PopCommand* c)
-{
-  out << "(pop 1)";
-}
+void Smt2Printer::toStreamCmdPop(std::ostream& out) const { out << "(pop 1)"; }
 
-static void toStream(std::ostream& out, const CheckSatCommand* c)
+void Smt2Printer::toStreamCmdCheckSat(std::ostream& out, Node n) const
 {
-  Expr e = c->getExpr();
-  if(!e.isNull() && !(e.getKind() == kind::CONST_BOOLEAN && e.getConst<bool>())) {
-    out << PushCommand() << endl
-        << AssertCommand(e) << endl
-        << CheckSatCommand() << endl
-        << PopCommand();
-  } else {
+  if (!n.isNull())
+  {
+    toStreamCmdPush(out);
+    out << std::endl;
+    toStreamCmdAssert(out, n);
+    out << std::endl;
+    toStreamCmdCheckSat(out);
+    out << std::endl;
+    toStreamCmdPop(out);
+  }
+  else
+  {
     out << "(check-sat)";
   }
 }
 
-static void toStream(std::ostream& out, const CheckSatAssumingCommand* c)
+void Smt2Printer::toStreamCmdCheckSatAssuming(
+    std::ostream& out, const std::vector<Node>& nodes) const
 {
   out << "(check-sat-assuming ( ";
-  const vector<Expr>& terms = c->getTerms();
-  copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, " "));
+  copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, " "));
   out << "))";
 }
 
-static void toStream(std::ostream& out, const QueryCommand* c, Variant v)
+void Smt2Printer::toStreamCmdQuery(std::ostream& out, Node n) const
 {
-  Expr e = c->getExpr();
-  if(!e.isNull()) {
-    if (v == smt2_0_variant)
+  if (!n.isNull())
+  {
+    if (d_variant == smt2_0_variant)
     {
-      out << PushCommand() << endl
-          << AssertCommand(BooleanSimplification::negate(e)) << endl
-          << CheckSatCommand() << endl
-          << PopCommand();
+      toStreamCmdCheckSat(out, BooleanSimplification::negate(n));
     }
     else
     {
-      out << CheckSatAssumingCommand(e.notExpr()) << endl;
+      toStreamCmdCheckSatAssuming(out, {n});
     }
-  } else {
-    out << "(check-sat)";
+  }
+  else
+  {
+    toStreamCmdCheckSat(out);
   }
 }
 
-static void toStream(std::ostream& out, const ResetCommand* c)
+void Smt2Printer::toStreamCmdReset(std::ostream& out) const
 {
   out << "(reset)";
 }
 
-static void toStream(std::ostream& out, const ResetAssertionsCommand* c)
+void Smt2Printer::toStreamCmdResetAssertions(std::ostream& out) const
 {
   out << "(reset-assertions)";
 }
 
-static void toStream(std::ostream& out, const QuitCommand* c)
-{
-  out << "(exit)";
-}
+void Smt2Printer::toStreamCmdQuit(std::ostream& out) const { out << "(exit)"; }
 
-static void toStream(std::ostream& out, const CommandSequence* c)
+void Smt2Printer::toStreamCmdCommandSequence(
+    std::ostream& out, const std::vector<Command*>& sequence) const
 {
-  CommandSequence::const_iterator i = c->begin();
-  if(i != c->end()) {
-    for(;;) {
+  CommandSequence::const_iterator i = sequence.cbegin();
+  if (i != sequence.cend())
+  {
+    for (;;)
+    {
       out << *i;
-      if(++i != c->end()) {
+      if (++i != sequence.cend())
+      {
         out << endl;
-      } else {
+      }
+      else
+      {
         break;
       }
     }
   }
 }
 
-static void toStream(std::ostream& out, const DeclareFunctionCommand* c)
+void Smt2Printer::toStreamCmdDeclarationSequence(
+    std::ostream& out, const std::vector<Command*>& sequence) const
+{
+  toStreamCmdCommandSequence(out, sequence);
+}
+
+void Smt2Printer::toStreamCmdDeclareFunction(std::ostream& out,
+                                             const std::string& id,
+                                             TypeNode type) const
 {
-  Type type = c->getType();
-  out << "(declare-fun " << CVC4::quoteSymbol(c->getSymbol()) << " (";
-  if(type.isFunction()) {
-    FunctionType ft = type;
-    const vector<Type> argTypes = ft.getArgTypes();
-    if(argTypes.size() > 0) {
-      copy( argTypes.begin(), argTypes.end() - 1,
-            ostream_iterator<Type>(out, " ") );
+  out << "(declare-fun " << CVC4::quoteSymbol(id) << " (";
+  if (type.isFunction())
+  {
+    const vector<TypeNode> argTypes = type.getArgTypes();
+    if (argTypes.size() > 0)
+    {
+      copy(argTypes.begin(),
+           argTypes.end() - 1,
+           ostream_iterator<TypeNode>(out, " "));
       out << argTypes.back();
     }
-    type = ft.getRangeType();
+    type = type.getRangeType();
   }
 
-  out << ") " << type << ")";
+  out << ") " << type << ')';
 }
 
-static void toStream(std::ostream& out, const DefineFunctionCommand* c)
+void Smt2Printer::toStreamCmdDefineFunction(std::ostream& out,
+                                            const std::string& id,
+                                            const std::vector<Node>& formals,
+                                            TypeNode range,
+                                            Node formula) const
 {
-  Expr func = c->getFunction();
-  const vector<Expr>* formals = &c->getFormals();
-  out << "(define-fun " << func << " (";
-  Type type = func.getType();
-  Expr formula = c->getFormula();
-  if(type.isFunction()) {
-    vector<Expr> f;
-    if(formals->empty()) {
-      const vector<Type>& params = FunctionType(type).getArgTypes();
-      for(vector<Type>::const_iterator j = params.begin(); j != params.end(); ++j) {
-        f.push_back(NodeManager::currentNM()->mkSkolem("a", TypeNode::fromType(*j), "",
-                                                       NodeManager::SKOLEM_NO_NOTIFY).toExpr());
-      }
-      formula = NodeManager::currentNM()->toExprManager()->mkExpr(kind::APPLY_UF, formula, f);
-      formals = &f;
-    }
-    vector<Expr>::const_iterator i = formals->begin();
-    for(;;) {
+  out << "(define-fun " << id << " (";
+  if (!formals.empty())
+  {
+    vector<Node>::const_iterator i = formals.cbegin();
+    for (;;)
+    {
       out << "(" << (*i) << " " << (*i).getType() << ")";
       ++i;
-      if(i != formals->end()) {
+      if (i != formals.cend())
+      {
         out << " ";
-      } else {
+      }
+      else
+      {
         break;
       }
     }
-    type = FunctionType(type).getRangeType();
   }
-  out << ") " << type << " " << formula << ")";
+  out << ") " << range << ' ' << formula << ')';
 }
 
-static void toStream(std::ostream& out, const DefineFunctionRecCommand* c)
+void Smt2Printer::toStreamCmdDefineFunctionRec(
+    std::ostream& out,
+    const std::vector<Node>& funcs,
+    const std::vector<std::vector<Node>>& formals,
+    const std::vector<Node>& formulas) const
 {
-  const vector<api::Term>& funcs = c->getFunctions();
-  const vector<vector<api::Term> >& formals = c->getFormals();
   out << "(define-fun";
   if (funcs.size() > 1)
   {
@@ -1665,10 +1615,10 @@ static void toStream(std::ostream& out, const DefineFunctionRecCommand* c)
     }
     out << funcs[i] << " (";
     // print its type signature
-    vector<api::Term>::const_iterator itf = formals[i].begin();
+    vector<Node>::const_iterator itf = formals[i].cbegin();
     for (;;)
     {
-      out << "(" << (*itf) << " " << (*itf).getSort() << ")";
+      out << "(" << (*itf) << " " << (*itf).getType() << ")";
       ++itf;
       if (itf != formals[i].end())
       {
@@ -1679,8 +1629,8 @@ static void toStream(std::ostream& out, const DefineFunctionRecCommand* c)
         break;
       }
     }
-    api::Sort type = funcs[i].getSort();
-    type = type.getFunctionCodomainSort();
+    TypeNode type = funcs[i].getType();
+    type = type.getRangeType();
     out << ") " << type;
     if (funcs.size() > 1)
     {
@@ -1691,7 +1641,6 @@ static void toStream(std::ostream& out, const DefineFunctionRecCommand* c)
   {
     out << ") (";
   }
-  const vector<api::Term>& formulas = c->getFormulas();
   for (unsigned i = 0, size = formulas.size(); i < size; i++)
   {
     if (i > 0)
@@ -1744,115 +1693,129 @@ static void toStreamRational(std::ostream& out,
   }
 }
 
-static void toStream(std::ostream& out, const DeclareTypeCommand* c)
+void Smt2Printer::toStreamCmdDeclareType(std::ostream& out,
+                                         const std::string& id,
+                                         size_t arity,
+                                         TypeNode type) const
 {
-  out << "(declare-sort " << CVC4::quoteSymbol(c->getSymbol()) << " "
-      << c->getArity() << ")";
+  out << "(declare-sort " << CVC4::quoteSymbol(id) << " " << arity << ")";
 }
 
-static void toStream(std::ostream& out, const DefineTypeCommand* c)
+void Smt2Printer::toStreamCmdDefineType(std::ostream& out,
+                                        const std::string& id,
+                                        const std::vector<TypeNode>& params,
+                                        TypeNode t) const
 {
-  const vector<Type>& params = c->getParameters();
-  out << "(define-sort " << c->getSymbol() << " (";
-  if(params.size() > 0) {
-    copy( params.begin(), params.end() - 1,
-          ostream_iterator<Type>(out, " ") );
+  out << "(define-sort " << CVC4::quoteSymbol(id) << " (";
+  if (params.size() > 0)
+  {
+    copy(
+        params.begin(), params.end() - 1, ostream_iterator<TypeNode>(out, " "));
     out << params.back();
   }
-  out << ") " << c->getType() << ")";
+  out << ") " << t << ")";
 }
 
-static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c)
+void Smt2Printer::toStreamCmdDefineNamedFunction(
+    std::ostream& out,
+    const std::string& id,
+    const std::vector<Node>& formals,
+    TypeNode range,
+    Node formula) const
 {
   out << "DefineNamedFunction( ";
-  toStream(out, static_cast<const DefineFunctionCommand*>(c));
-  out << " )";
+  toStreamCmdDefineFunction(out, id, formals, range, formula);
+  out << " )" << std::endl;
 
-  out << "ERROR: don't know how to output define-named-function command" << endl;
+  printUnknownCommand(out, "define-named-function");
 }
 
-static void toStream(std::ostream& out, const SimplifyCommand* c)
+void Smt2Printer::toStreamCmdSimplify(std::ostream& out, Node n) const
 {
-  out << "(simplify " << c->getTerm() << ")";
+  out << "(simplify " << n << ')';
 }
 
-static void toStream(std::ostream& out, const GetValueCommand* c)
+void Smt2Printer::toStreamCmdGetValue(std::ostream& out,
+                                      const std::vector<Node>& nodes) const
 {
   out << "(get-value ( ";
-  const vector<Expr>& terms = c->getTerms();
-  copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, " "));
+  copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, " "));
   out << "))";
 }
 
-static void toStream(std::ostream& out, const GetModelCommand* c)
+void Smt2Printer::toStreamCmdGetModel(std::ostream& out) const
 {
   out << "(get-model)";
 }
 
-static void toStream(std::ostream& out, const GetAssignmentCommand* c)
+void Smt2Printer::toStreamCmdGetAssignment(std::ostream& out) const
 {
   out << "(get-assignment)";
 }
 
-static void toStream(std::ostream& out, const GetAssertionsCommand* c)
+void Smt2Printer::toStreamCmdGetAssertions(std::ostream& out) const
 {
   out << "(get-assertions)";
 }
 
-static void toStream(std::ostream& out, const GetProofCommand* c)
+void Smt2Printer::toStreamCmdGetProof(std::ostream& out) const
 {
   out << "(get-proof)";
 }
 
-static void toStream(std::ostream& out, const GetUnsatAssumptionsCommand* c)
+void Smt2Printer::toStreamCmdGetUnsatAssumptions(std::ostream& out) const
 {
   out << "(get-unsat-assumptions)";
 }
 
-static void toStream(std::ostream& out, const GetUnsatCoreCommand* c)
+void Smt2Printer::toStreamCmdGetUnsatCore(std::ostream& out) const
 {
   out << "(get-unsat-core)";
 }
 
-static void toStream(std::ostream& out,
-                     const SetBenchmarkStatusCommand* c,
-                     Variant v)
+void Smt2Printer::toStreamCmdSetBenchmarkStatus(std::ostream& out,
+                                                BenchmarkStatus status) const
 {
-  out << "(set-info :status " << c->getStatus() << ")";
+  out << "(set-info :status " << status << ')';
 }
 
-static void toStream(std::ostream& out,
-                     const SetBenchmarkLogicCommand* c,
-                     Variant v)
+void Smt2Printer::toStreamCmdSetBenchmarkLogic(std::ostream& out,
+                                               const std::string& logic) const
 {
-  out << "(set-logic " << c->getLogic() << ")";
+  out << "(set-logic " << logic << ')';
 }
 
-static void toStream(std::ostream& out, const SetInfoCommand* c, Variant v)
+void Smt2Printer::toStreamCmdSetInfo(std::ostream& out,
+                                     const std::string& flag,
+                                     SExpr sexpr) const
 {
-  out << "(set-info :" << c->getFlag() << " ";
-  SExpr::toStream(out, c->getSExpr(), variantToLanguage(v));
-  out << ")";
+  out << "(set-info :" << flag << ' ';
+  SExpr::toStream(out, sexpr, variantToLanguage(d_variant));
+  out << ')';
 }
 
-static void toStream(std::ostream& out, const GetInfoCommand* c)
+void Smt2Printer::toStreamCmdGetInfo(std::ostream& out,
+                                     const std::string& flag) const
 {
-  out << "(get-info :" << c->getFlag() << ")";
+  out << "(get-info :" << flag << ')';
 }
 
-static void toStream(std::ostream& out, const SetOptionCommand* c)
+void Smt2Printer::toStreamCmdSetOption(std::ostream& out,
+                                       const std::string& flag,
+                                       SExpr sexpr) const
 {
-  out << "(set-option :" << c->getFlag() << " ";
-  SExpr::toStream(out, c->getSExpr(), language::output::LANG_SMTLIB_V2_5);
-  out << ")";
+  out << "(set-option :" << flag << ' ';
+  SExpr::toStream(out, sexpr, language::output::LANG_SMTLIB_V2_5);
+  out << ')';
 }
 
-static void toStream(std::ostream& out, const GetOptionCommand* c)
+void Smt2Printer::toStreamCmdGetOption(std::ostream& out,
+                                       const std::string& flag) const
 {
-  out << "(get-option :" << c->getFlag() << ")";
+  out << "(get-option :" << flag << ')';
 }
 
-static void toStream(std::ostream& out, const DType& dt)
+void Smt2Printer::toStream(std::ostream& out, const DType& dt) const
 {
   for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
   {
@@ -1871,14 +1834,12 @@ static void toStream(std::ostream& out, const DType& dt)
   }
 }
 
-static void toStream(std::ostream& out,
-                     const DatatypeDeclarationCommand* c,
-                     Variant v)
+void Smt2Printer::toStreamCmdDatatypeDeclaration(
+    std::ostream& out, const std::vector<TypeNode>& datatypes) const
 {
-  const std::vector<Type>& datatypes = c->getDatatypes();
   Assert(!datatypes.empty());
   Assert(datatypes[0].isDatatype());
-  const DType& d0 = TypeNode::fromType(datatypes[0]).getDType();
+  const DType& d0 = datatypes[0].getDType();
   if (d0.isTuple())
   {
     // not necessary to print tuples
@@ -1891,21 +1852,21 @@ static void toStream(std::ostream& out,
     out << "co";
   }
   out << "datatypes";
-  if (isVariant_2_6(v))
+  if (isVariant_2_6(d_variant))
   {
     out << " (";
-    for (const Type& t : datatypes)
+    for (const TypeNode& t : datatypes)
     {
       Assert(t.isDatatype());
-      const DType& d = TypeNode::fromType(t).getDType();
+      const DType& d = t.getDType();
       out << "(" << CVC4::quoteSymbol(d.getName());
       out << " " << d.getNumParameters() << ")";
     }
     out << ") (";
-    for (const Type& t : datatypes)
+    for (const TypeNode& t : datatypes)
     {
       Assert(t.isDatatype());
-      const DType& d = TypeNode::fromType(t).getDType();
+      const DType& d = t.getDType();
       if (d.isParametric())
       {
         out << "(par (";
@@ -1937,7 +1898,7 @@ static void toStream(std::ostream& out,
     for (unsigned j = 1, ndt = datatypes.size(); j < ndt; j++)
     {
       Assert(datatypes[j].isDatatype());
-      const DType& dj = TypeNode::fromType(datatypes[j]).getDType();
+      const DType& dj = datatypes[j].getDType();
       if (dj.getNumParameters() != nparam)
       {
         success = false;
@@ -1974,10 +1935,10 @@ static void toStream(std::ostream& out,
       out << std::endl;
     }
     out << ") (";
-    for (const Type& t : datatypes)
+    for (const TypeNode& t : datatypes)
     {
       Assert(t.isDatatype());
-      const DType& dt = TypeNode::fromType(t).getDType();
+      const DType& dt = t.getDType();
       out << "(" << CVC4::quoteSymbol(dt.getName()) << " ";
       toStream(out, dt);
       out << ")";
@@ -1987,26 +1948,33 @@ static void toStream(std::ostream& out,
   out << ")" << endl;
 }
 
-static void toStream(std::ostream& out, const CommentCommand* c, Variant v)
+void Smt2Printer::toStreamCmdComment(std::ostream& out,
+                                     const std::string& comment) const
 {
-  string s = c->getComment();
+  std::string s = comment;
   size_t pos = 0;
-  while((pos = s.find_first_of('"', pos)) != string::npos) {
-    s.replace(pos, 1, v == smt2_0_variant ? "\\\"" : "\"\"");
+  while ((pos = s.find_first_of('"', pos)) != string::npos)
+  {
+    s.replace(pos, 1, d_variant == smt2_0_variant ? "\\\"" : "\"\"");
     pos += 2;
   }
   out << "(set-info :notes \"" << s << "\")";
 }
 
-static void toStream(std::ostream& out, const EmptyCommand* c) {}
+void Smt2Printer::toStreamCmdEmpty(std::ostream& out,
+                                   const std::string& name) const
+{
+}
 
-static void toStream(std::ostream& out, const EchoCommand* c, Variant v)
+void Smt2Printer::toStreamCmdEcho(std::ostream& out,
+                                  const std::string& output) const
 {
-  std::string s = c->getOutput();
+  std::string s = output;
   // escape all double-quotes
   size_t pos = 0;
-  while((pos = s.find('"', pos)) != string::npos) {
-    s.replace(pos, 1, v == smt2_0_variant ? "\\\"" : "\"\"");
+  while ((pos = s.find('"', pos)) != string::npos)
+  {
+    s.replace(pos, 1, d_variant == smt2_0_variant ? "\\\"" : "\"\"");
     pos += 2;
   }
   out << "(echo \"" << s << "\")";
@@ -2081,7 +2049,7 @@ void Smt2Printer::toStreamCmdSynthFun(std::ostream& out,
                                       const std::vector<Node>& vars,
                                       TypeNode range,
                                       bool isInv,
-                                      TypeNode sygusType)
+                                      TypeNode sygusType) const
 {
   out << '(' << (isInv ? "synth-inv " : "synth-fun ") << CVC4::quoteSymbol(sym)
       << ' ';
@@ -2113,60 +2081,43 @@ void Smt2Printer::toStreamCmdSynthFun(std::ostream& out,
   out << ')';
 }
 
-static void toStream(std::ostream& out, const DeclareSygusFunctionCommand* c)
-{
-  out << '(' << c->getCommandName() << ' ' << CVC4::quoteSymbol(c->getSymbol());
-
-  FunctionType ft = c->getType();
-  stringstream ss;
-
-  for (const Type& i : ft.getArgTypes())
-  {
-    ss << i << ' ';
-  }
-
-  string argTypes = ss.str();
-  argTypes.pop_back();
-
-  out << " (" << argTypes << ") " << ft.getRangeType() << ')';
-}
-
-static void toStream(std::ostream& out, const DeclareSygusVarCommand* c)
+void Smt2Printer::toStreamCmdDeclareVar(std::ostream& out,
+                                        Node var,
+                                        TypeNode type) const
 {
-  out << '(' << c->getCommandName() << ' ' << c->getVar() << ' ' << c->getType()
-      << ')';
+  out << "(declare-var " << var << ' ' << type << ')';
 }
 
-static void toStream(std::ostream& out, const SygusConstraintCommand* c)
+void Smt2Printer::toStreamCmdConstraint(std::ostream& out, Node n) const
 {
-  out << '(' << c->getCommandName() << ' ' << c->getExpr() << ')';
+  out << "(constraint " << n << ')';
 }
 
-static void toStream(std::ostream& out, const SygusInvConstraintCommand* c)
+void Smt2Printer::toStreamCmdInvConstraint(
+    std::ostream& out, Node inv, Node pre, Node trans, Node post) const
 {
-  out << '(' << c->getCommandName() << ' ';
-  copy(c->getPredicates().cbegin(),
-       c->getPredicates().cend(),
-       std::ostream_iterator<Expr>(out, " "));
-  out << ')';
+  out << "(inv-constraint " << inv << ' ' << pre << ' ' << trans << ' ' << post
+      << ')';
 }
 
-static void toStream(std::ostream& out, const CheckSynthCommand* c)
+void Smt2Printer::toStreamCmdCheckSynth(std::ostream& out) const
 {
-  out << '(' << c->getCommandName() << ')';
+  out << "(check-synth)";
 }
 
-static void toStream(std::ostream& out, const GetAbductCommand* c)
+void Smt2Printer::toStreamCmdGetAbduct(std::ostream& out,
+                                       const std::string& name,
+                                       Node conj,
+                                       TypeNode sygusType) const
 {
-  out << '(';
-  out << c->getCommandName() << ' ';
-  out << c->getAbductName() << ' ';
-  out << c->getConjecture();
+  out << "(get-abduct ";
+  out << name << ' ';
+  out << conj << ' ';
 
   // print grammar, if any
-  if (c->getGrammar() != nullptr)
+  if (!sygusType.isNull())
   {
-    out << *c->getGrammar();
+    toStreamSygusGrammar(out, sygusType);
   }
   out << ')';
 }
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index cb1ffe9bd..6b57823a4 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -35,20 +35,17 @@ enum Variant
                    // support for the string standard
   sygus_variant    // variant for sygus
 };                 /* enum Variant */
-class Smt2Printer : public CVC4::Printer {
+
+class Smt2Printer : public CVC4::Printer
+{
  public:
-  Smt2Printer(Variant variant = no_variant) : d_variant(variant) { }
+  Smt2Printer(Variant variant = no_variant) : d_variant(variant) {}
   using CVC4::Printer::toStream;
   void toStream(std::ostream& out,
                 TNode n,
                 int toDepth,
                 bool types,
                 size_t dag) const override;
-  void toStream(std::ostream& out,
-                const Command* c,
-                int toDepth,
-                bool types,
-                size_t dag) const override;
   void toStream(std::ostream& out, const CommandStatus* s) const override;
   void toStream(std::ostream& out, const Model& m) const override;
   /**
@@ -58,13 +55,179 @@ class Smt2Printer : public CVC4::Printer {
    */
   void toStream(std::ostream& out, const UnsatCore& core) const override;
 
-  /** Print synth fun command */
+  /** Print empty command */
+  void toStreamCmdEmpty(std::ostream& out,
+                        const std::string& name) const override;
+
+  /** Print echo command */
+  void toStreamCmdEcho(std::ostream& out,
+                       const std::string& output) const override;
+
+  /** Print assert command */
+  void toStreamCmdAssert(std::ostream& out, Node n) const override;
+
+  /** Print push command */
+  void toStreamCmdPush(std::ostream& out) const override;
+
+  /** Print pop command */
+  void toStreamCmdPop(std::ostream& out) const override;
+
+  /** Print declare-fun command */
+  void toStreamCmdDeclareFunction(std::ostream& out,
+                                  const std::string& id,
+                                  TypeNode type) const override;
+
+  /** Print declare-sort command */
+  void toStreamCmdDeclareType(std::ostream& out,
+                              const std::string& id,
+                              size_t arity,
+                              TypeNode type) const override;
+
+  /** Print define-sort command */
+  void toStreamCmdDefineType(std::ostream& out,
+                             const std::string& id,
+                             const std::vector<TypeNode>& params,
+                             TypeNode t) const override;
+
+  /** Print define-fun command */
+  void toStreamCmdDefineFunction(std::ostream& out,
+                                 const std::string& id,
+                                 const std::vector<Node>& formals,
+                                 TypeNode range,
+                                 Node formula) const override;
+
+  /** Print define-named-fun command */
+  void toStreamCmdDefineNamedFunction(std::ostream& out,
+                                      const std::string& id,
+                                      const std::vector<Node>& formals,
+                                      TypeNode range,
+                                      Node formula) const override;
+
+  /** Print define-fun-rec command */
+  void toStreamCmdDefineFunctionRec(
+      std::ostream& out,
+      const std::vector<Node>& funcs,
+      const std::vector<std::vector<Node>>& formals,
+      const std::vector<Node>& formulas) const override;
+
+  /** Print check-sat command */
+  void toStreamCmdCheckSat(std::ostream& out,
+                           Node n = Node::null()) const override;
+
+  /** Print check-sat-assuming command */
+  void toStreamCmdCheckSatAssuming(
+      std::ostream& out, const std::vector<Node>& nodes) const override;
+
+  /** Print query command */
+  void toStreamCmdQuery(std::ostream& out, Node n) const override;
+
+  /** Print declare-var command */
+  void toStreamCmdDeclareVar(std::ostream& out,
+                             Node var,
+                             TypeNode type) const override;
+
+  /** Print synth-fun command */
   void toStreamCmdSynthFun(std::ostream& out,
                            const std::string& sym,
                            const std::vector<Node>& vars,
                            TypeNode range,
                            bool isInv,
-                           TypeNode sygusType) override;
+                           TypeNode sygusType) const override;
+
+  /** Print constraint command */
+  void toStreamCmdConstraint(std::ostream& out, Node n) const override;
+
+  /** Print inv-constraint command */
+  void toStreamCmdInvConstraint(std::ostream& out,
+                                Node inv,
+                                Node pre,
+                                Node trans,
+                                Node post) const override;
+
+  /** Print check-synth command */
+  void toStreamCmdCheckSynth(std::ostream& out) const override;
+
+  /** Print simplify command */
+  void toStreamCmdSimplify(std::ostream& out, Node nodes) const override;
+
+  /** Print get-value command */
+  void toStreamCmdGetValue(std::ostream& out,
+                           const std::vector<Node>& n) const override;
+
+  /** Print get-assignment command */
+  void toStreamCmdGetAssignment(std::ostream& out) const override;
+
+  /** Print get-model command */
+  void toStreamCmdGetModel(std::ostream& out) const override;
+
+  /** Print get-proof command */
+  void toStreamCmdGetProof(std::ostream& out) const override;
+
+  /** Print get-abduct command */
+  void toStreamCmdGetAbduct(std::ostream& out,
+                            const std::string& name,
+                            Node conj,
+                            TypeNode sygusType) const override;
+
+  /** Print get-unsat-assumptions command */
+  void toStreamCmdGetUnsatAssumptions(std::ostream& out) const override;
+
+  /** Print get-unsat-core command */
+  void toStreamCmdGetUnsatCore(std::ostream& out) const override;
+
+  /** Print get-assertions command */
+  void toStreamCmdGetAssertions(std::ostream& out) const override;
+
+  /** Print set-info :status command */
+  void toStreamCmdSetBenchmarkStatus(std::ostream& out,
+                                     BenchmarkStatus status) const override;
+
+  /** Print set-logic command */
+  void toStreamCmdSetBenchmarkLogic(std::ostream& out,
+                                    const std::string& logic) const override;
+
+  /** Print set-info command */
+  void toStreamCmdSetInfo(std::ostream& out,
+                          const std::string& flag,
+                          SExpr sexpr) const override;
+
+  /** Print get-info command */
+  void toStreamCmdGetInfo(std::ostream& out,
+                          const std::string& flag) const override;
+
+  /** Print set-option command */
+  void toStreamCmdSetOption(std::ostream& out,
+                            const std::string& flag,
+                            SExpr sexpr) const override;
+
+  /** Print get-option command */
+  void toStreamCmdGetOption(std::ostream& out,
+                            const std::string& flag) const override;
+
+  /** Print declare-datatype(s) command */
+  void toStreamCmdDatatypeDeclaration(
+      std::ostream& out, const std::vector<TypeNode>& datatypes) const override;
+
+  /** Print reset command */
+  void toStreamCmdReset(std::ostream& out) const override;
+
+  /** Print reset-assertions command */
+  void toStreamCmdResetAssertions(std::ostream& out) const override;
+
+  /** Print quit command */
+  void toStreamCmdQuit(std::ostream& out) const override;
+
+  /** Print comment command */
+  void toStreamCmdComment(std::ostream& out,
+                          const std::string& comment) const override;
+
+  /** Print command sequence command */
+  void toStreamCmdCommandSequence(
+      std::ostream& out, const std::vector<Command*>& sequence) const override;
+
+  /** Print declaration sequence command */
+  void toStreamCmdDeclarationSequence(
+      std::ostream& out, const std::vector<Command*>& sequence) const override;
 
  private:
   void toStream(
@@ -73,12 +236,13 @@ class Smt2Printer : public CVC4::Printer {
                 const Model& m,
                 const Command* c) const override;
   void toStream(std::ostream& out, const SExpr& sexpr) const;
+  void toStream(std::ostream& out, const DType& dt) const;
 
   Variant d_variant;
-};/* class Smt2Printer */
+}; /* class Smt2Printer */
 
-}/* CVC4::printer::smt2 namespace */
-}/* CVC4::printer namespace */
-}/* CVC4 namespace */
+}  // namespace smt2
+}  // namespace printer
+}  // namespace CVC4
 
 #endif /* CVC4__PRINTER__SMT2_PRINTER_H */
diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp
index f1c1089ad..c4623f76a 100644
--- a/src/printer/tptp/tptp_printer.cpp
+++ b/src/printer/tptp/tptp_printer.cpp
@@ -39,15 +39,6 @@ void TptpPrinter::toStream(
   n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
 }/* TptpPrinter::toStream() */
 
-void TptpPrinter::toStream(std::ostream& out,
-                           const Command* c,
-                           int toDepth,
-                           bool types,
-                           size_t dag) const
-{
-  c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
-}/* TptpPrinter::toStream() */
-
 void TptpPrinter::toStream(std::ostream& out, const CommandStatus* s) const
 {
   s->toStream(out, language::output::LANG_SMTLIB_V2_5);
diff --git a/src/printer/tptp/tptp_printer.h b/src/printer/tptp/tptp_printer.h
index d183a19d0..6682b495e 100644
--- a/src/printer/tptp/tptp_printer.h
+++ b/src/printer/tptp/tptp_printer.h
@@ -27,7 +27,8 @@ namespace CVC4 {
 namespace printer {
 namespace tptp {
 
-class TptpPrinter : public CVC4::Printer {
+class TptpPrinter : public CVC4::Printer
+{
  public:
   using CVC4::Printer::toStream;
   void toStream(std::ostream& out,
@@ -35,27 +36,23 @@ class TptpPrinter : public CVC4::Printer {
                 int toDepth,
                 bool types,
                 size_t dag) const override;
-  void toStream(std::ostream& out,
-                const Command* c,
-                int toDepth,
-                bool types,
-                size_t dag) const override;
   void toStream(std::ostream& out, const CommandStatus* s) const override;
   void toStream(std::ostream& out, const Model& m) const override;
   /** print unsat core to stream
-  * We use the expression names stored in the SMT engine associated with the unsat core
-  * with UnsatCore::getSmtEngine.
-  */
+   * We use the expression names stored in the SMT engine associated with the
+   * unsat core with UnsatCore::getSmtEngine.
+   */
   void toStream(std::ostream& out, const UnsatCore& core) const override;
 
  private:
   void toStream(std::ostream& out,
                 const Model& m,
                 const Command* c) const override;
-};/* class TptpPrinter */
 
-}/* CVC4::printer::tptp namespace */
-}/* CVC4::printer namespace */
-}/* CVC4 namespace */
+}; /* class TptpPrinter */
+
+}  // namespace tptp
+}  // namespace printer
+}  // namespace CVC4
 
 #endif /* CVC4__PRINTER__TPTP_PRINTER_H */
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 2383167a6..99e0a6c25 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -105,6 +105,34 @@ std::ostream& operator<<(std::ostream& out, BenchmarkStatus status)
   }
 }
 
+// !!! Temporary until commands are migrated to the new API !!!
+std::vector<Node> exprVectorToNodes(const std::vector<Expr>& exprs)
+{
+  std::vector<Node> nodes;
+  nodes.reserve(exprs.size());
+
+  for (Expr e : exprs)
+  {
+    nodes.push_back(Node::fromExpr(e));
+  }
+
+  return nodes;
+}
+
+// !!! Temporary until commands are migrated to the new API !!!
+std::vector<TypeNode> typeVectorToTypeNodes(const std::vector<Type>& types)
+{
+  std::vector<TypeNode> typeNodes;
+  typeNodes.reserve(types.size());
+
+  for (Type t : types)
+  {
+    typeNodes.push_back(TypeNode::fromType(t));
+  }
+
+  return typeNodes;
+}
+
 /* -------------------------------------------------------------------------- */
 /* class CommandPrintSuccess                                                  */
 /* -------------------------------------------------------------------------- */
@@ -194,15 +222,6 @@ std::string Command::toString() const
   return ss.str();
 }
 
-void Command::toStream(std::ostream& out,
-                       int toDepth,
-                       bool types,
-                       size_t dag,
-                       OutputLanguage language) const
-{
-  Printer::getPrinter(language)->toStream(out, this, toDepth, types, dag);
-}
-
 void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const
 {
   Printer::getPrinter(language)->toStream(out, this);
@@ -240,6 +259,15 @@ Command* EmptyCommand::exportTo(ExprManager* exprManager,
 Command* EmptyCommand::clone() const { return new EmptyCommand(d_name); }
 std::string EmptyCommand::getCommandName() const { return "empty"; }
 
+void EmptyCommand::toStream(std::ostream& out,
+                            int toDepth,
+                            bool types,
+                            size_t dag,
+                            OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdEmpty(out, d_name);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class EchoCommand                                                          */
 /* -------------------------------------------------------------------------- */
@@ -273,6 +301,15 @@ Command* EchoCommand::exportTo(ExprManager* exprManager,
 Command* EchoCommand::clone() const { return new EchoCommand(d_output); }
 std::string EchoCommand::getCommandName() const { return "echo"; }
 
+void EchoCommand::toStream(std::ostream& out,
+                           int toDepth,
+                           bool types,
+                           size_t dag,
+                           OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdEcho(out, d_output);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class AssertCommand                                                        */
 /* -------------------------------------------------------------------------- */
@@ -314,6 +351,15 @@ Command* AssertCommand::clone() const
 
 std::string AssertCommand::getCommandName() const { return "assert"; }
 
+void AssertCommand::toStream(std::ostream& out,
+                             int toDepth,
+                             bool types,
+                             size_t dag,
+                             OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdAssert(out, Node::fromExpr(d_expr));
+}
+
 /* -------------------------------------------------------------------------- */
 /* class PushCommand                                                          */
 /* -------------------------------------------------------------------------- */
@@ -344,6 +390,15 @@ Command* PushCommand::exportTo(ExprManager* exprManager,
 Command* PushCommand::clone() const { return new PushCommand(); }
 std::string PushCommand::getCommandName() const { return "push"; }
 
+void PushCommand::toStream(std::ostream& out,
+                           int toDepth,
+                           bool types,
+                           size_t dag,
+                           OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdPush(out);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class PopCommand                                                           */
 /* -------------------------------------------------------------------------- */
@@ -374,6 +429,15 @@ Command* PopCommand::exportTo(ExprManager* exprManager,
 Command* PopCommand::clone() const { return new PopCommand(); }
 std::string PopCommand::getCommandName() const { return "pop"; }
 
+void PopCommand::toStream(std::ostream& out,
+                          int toDepth,
+                          bool types,
+                          size_t dag,
+                          OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdPop(out);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class CheckSatCommand                                                      */
 /* -------------------------------------------------------------------------- */
@@ -430,6 +494,16 @@ Command* CheckSatCommand::clone() const
 
 std::string CheckSatCommand::getCommandName() const { return "check-sat"; }
 
+void CheckSatCommand::toStream(std::ostream& out,
+                               int toDepth,
+                               bool types,
+                               size_t dag,
+                               OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdCheckSat(out,
+                                                     Node::fromExpr(d_expr));
+}
+
 /* -------------------------------------------------------------------------- */
 /* class CheckSatAssumingCommand                                              */
 /* -------------------------------------------------------------------------- */
@@ -505,6 +579,21 @@ std::string CheckSatAssumingCommand::getCommandName() const
   return "check-sat-assuming";
 }
 
+void CheckSatAssumingCommand::toStream(std::ostream& out,
+                                       int toDepth,
+                                       bool types,
+                                       size_t dag,
+                                       OutputLanguage language) const
+{
+  std::vector<Node> nodes;
+  nodes.reserve(d_terms.size());
+  for (const Expr& e : d_terms)
+  {
+    nodes.push_back(Node::fromExpr(e));
+  }
+  Printer::getPrinter(language)->toStreamCmdCheckSatAssuming(out, nodes);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class QueryCommand                                                         */
 /* -------------------------------------------------------------------------- */
@@ -559,6 +648,15 @@ Command* QueryCommand::clone() const
 
 std::string QueryCommand::getCommandName() const { return "query"; }
 
+void QueryCommand::toStream(std::ostream& out,
+                            int toDepth,
+                            bool types,
+                            size_t dag,
+                            OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdQuery(out, d_expr);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class DeclareSygusVarCommand */
 /* -------------------------------------------------------------------------- */
@@ -605,51 +703,14 @@ std::string DeclareSygusVarCommand::getCommandName() const
   return "declare-var";
 }
 
-/* -------------------------------------------------------------------------- */
-/* class DeclareSygusFunctionCommand                                          */
-/* -------------------------------------------------------------------------- */
-
-DeclareSygusFunctionCommand::DeclareSygusFunctionCommand(const std::string& id,
-                                                         Expr func,
-                                                         Type t)
-    : DeclarationDefinitionCommand(id), d_func(func), d_type(t)
-{
-}
-
-Expr DeclareSygusFunctionCommand::getFunction() const { return d_func; }
-Type DeclareSygusFunctionCommand::getType() const { return d_type; }
-
-void DeclareSygusFunctionCommand::invoke(SmtEngine* smtEngine)
-{
-  try
-  {
-    smtEngine->declareSygusVar(
-        d_symbol, Node::fromExpr(d_func), TypeNode::fromType(d_type));
-    d_commandStatus = CommandSuccess::instance();
-  }
-  catch (exception& e)
-  {
-    d_commandStatus = new CommandFailure(e.what());
-  }
-}
-
-Command* DeclareSygusFunctionCommand::exportTo(
-    ExprManager* exprManager, ExprManagerMapCollection& variableMap)
+void DeclareSygusVarCommand::toStream(std::ostream& out,
+                                      int toDepth,
+                                      bool types,
+                                      size_t dag,
+                                      OutputLanguage language) const
 {
-  return new DeclareSygusFunctionCommand(
-      d_symbol,
-      d_func.exportTo(exprManager, variableMap),
-      d_type.exportTo(exprManager, variableMap));
-}
-
-Command* DeclareSygusFunctionCommand::clone() const
-{
-  return new DeclareSygusFunctionCommand(d_symbol, d_func, d_type);
-}
-
-std::string DeclareSygusFunctionCommand::getCommandName() const
-{
-  return "declare-fun";
+  Printer::getPrinter(language)->toStreamCmdDeclareVar(
+      out, Node::fromExpr(d_var), TypeNode::fromType(d_type));
 }
 
 /* -------------------------------------------------------------------------- */
@@ -780,6 +841,16 @@ std::string SygusConstraintCommand::getCommandName() const
   return "constraint";
 }
 
+void SygusConstraintCommand::toStream(std::ostream& out,
+                                      int toDepth,
+                                      bool types,
+                                      size_t dag,
+                                      OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdConstraint(out,
+                                                       Node::fromExpr(d_expr));
+}
+
 /* -------------------------------------------------------------------------- */
 /* class SygusInvConstraintCommand */
 /* -------------------------------------------------------------------------- */
@@ -833,6 +904,20 @@ std::string SygusInvConstraintCommand::getCommandName() const
   return "inv-constraint";
 }
 
+void SygusInvConstraintCommand::toStream(std::ostream& out,
+                                         int toDepth,
+                                         bool types,
+                                         size_t dag,
+                                         OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdInvConstraint(
+      out,
+      Node::fromExpr(d_predicates[0]),
+      Node::fromExpr(d_predicates[1]),
+      Node::fromExpr(d_predicates[2]),
+      Node::fromExpr(d_predicates[3]));
+}
+
 /* -------------------------------------------------------------------------- */
 /* class CheckSynthCommand                                                    */
 /* -------------------------------------------------------------------------- */
@@ -900,6 +985,15 @@ Command* CheckSynthCommand::clone() const { return new CheckSynthCommand(); }
 
 std::string CheckSynthCommand::getCommandName() const { return "check-synth"; }
 
+void CheckSynthCommand::toStream(std::ostream& out,
+                                 int toDepth,
+                                 bool types,
+                                 size_t dag,
+                                 OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdCheckSynth(out);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class ResetCommand                                                         */
 /* -------------------------------------------------------------------------- */
@@ -926,6 +1020,15 @@ Command* ResetCommand::exportTo(ExprManager* exprManager,
 Command* ResetCommand::clone() const { return new ResetCommand(); }
 std::string ResetCommand::getCommandName() const { return "reset"; }
 
+void ResetCommand::toStream(std::ostream& out,
+                            int toDepth,
+                            bool types,
+                            size_t dag,
+                            OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdReset(out);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class ResetAssertionsCommand                                               */
 /* -------------------------------------------------------------------------- */
@@ -959,6 +1062,15 @@ std::string ResetAssertionsCommand::getCommandName() const
   return "reset-assertions";
 }
 
+void ResetAssertionsCommand::toStream(std::ostream& out,
+                                      int toDepth,
+                                      bool types,
+                                      size_t dag,
+                                      OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdResetAssertions(out);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class QuitCommand                                                          */
 /* -------------------------------------------------------------------------- */
@@ -978,6 +1090,15 @@ Command* QuitCommand::exportTo(ExprManager* exprManager,
 Command* QuitCommand::clone() const { return new QuitCommand(); }
 std::string QuitCommand::getCommandName() const { return "exit"; }
 
+void QuitCommand::toStream(std::ostream& out,
+                           int toDepth,
+                           bool types,
+                           size_t dag,
+                           OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdQuit(out);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class CommentCommand                                                       */
 /* -------------------------------------------------------------------------- */
@@ -999,6 +1120,15 @@ Command* CommentCommand::exportTo(ExprManager* exprManager,
 Command* CommentCommand::clone() const { return new CommentCommand(d_comment); }
 std::string CommentCommand::getCommandName() const { return "comment"; }
 
+void CommentCommand::toStream(std::ostream& out,
+                              int toDepth,
+                              bool types,
+                              size_t dag,
+                              OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdComment(out, d_comment);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class CommandSequence                                                      */
 /* -------------------------------------------------------------------------- */
@@ -1102,6 +1232,30 @@ CommandSequence::iterator CommandSequence::end()
 
 std::string CommandSequence::getCommandName() const { return "sequence"; }
 
+void CommandSequence::toStream(std::ostream& out,
+                               int toDepth,
+                               bool types,
+                               size_t dag,
+                               OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdCommandSequence(out,
+                                                            d_commandSequence);
+}
+
+/* -------------------------------------------------------------------------- */
+/* class DeclarationSequence                                                  */
+/* -------------------------------------------------------------------------- */
+
+void DeclarationSequence::toStream(std::ostream& out,
+                                   int toDepth,
+                                   bool types,
+                                   size_t dag,
+                                   OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdDeclarationSequence(
+      out, d_commandSequence);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class DeclarationDefinitionCommand                                         */
 /* -------------------------------------------------------------------------- */
@@ -1174,6 +1328,16 @@ std::string DeclareFunctionCommand::getCommandName() const
   return "declare-fun";
 }
 
+void DeclareFunctionCommand::toStream(std::ostream& out,
+                                      int toDepth,
+                                      bool types,
+                                      size_t dag,
+                                      OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdDeclareFunction(
+      out, d_func.toString(), TypeNode::fromType(d_type));
+}
+
 /* -------------------------------------------------------------------------- */
 /* class DeclareTypeCommand                                                   */
 /* -------------------------------------------------------------------------- */
@@ -1209,6 +1373,16 @@ std::string DeclareTypeCommand::getCommandName() const
   return "declare-sort";
 }
 
+void DeclareTypeCommand::toStream(std::ostream& out,
+                                  int toDepth,
+                                  bool types,
+                                  size_t dag,
+                                  OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdDeclareType(
+      out, d_type.toString(), d_arity, TypeNode::fromType(d_type));
+}
+
 /* -------------------------------------------------------------------------- */
 /* class DefineTypeCommand                                                    */
 /* -------------------------------------------------------------------------- */
@@ -1255,6 +1429,19 @@ Command* DefineTypeCommand::clone() const
 
 std::string DefineTypeCommand::getCommandName() const { return "define-sort"; }
 
+void DefineTypeCommand::toStream(std::ostream& out,
+                                 int toDepth,
+                                 bool types,
+                                 size_t dag,
+                                 OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdDefineType(
+      out,
+      d_symbol,
+      typeVectorToTypeNodes(d_params),
+      TypeNode::fromType(d_type));
+}
+
 /* -------------------------------------------------------------------------- */
 /* class DefineFunctionCommand                                                */
 /* -------------------------------------------------------------------------- */
@@ -1333,6 +1520,20 @@ std::string DefineFunctionCommand::getCommandName() const
   return "define-fun";
 }
 
+void DefineFunctionCommand::toStream(std::ostream& out,
+                                     int toDepth,
+                                     bool types,
+                                     size_t dag,
+                                     OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdDefineFunction(
+      out,
+      d_func.toString(),
+      exprVectorToNodes(d_formals),
+      Node::fromExpr(d_func).getType().getRangeType(),
+      Node::fromExpr(d_formula));
+}
+
 /* -------------------------------------------------------------------------- */
 /* class DefineNamedFunctionCommand                                           */
 /* -------------------------------------------------------------------------- */
@@ -1377,6 +1578,20 @@ Command* DefineNamedFunctionCommand::clone() const
       d_symbol, d_func, d_formals, d_formula, d_global);
 }
 
+void DefineNamedFunctionCommand::toStream(std::ostream& out,
+                                          int toDepth,
+                                          bool types,
+                                          size_t dag,
+                                          OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdDefineNamedFunction(
+      out,
+      d_func.toString(),
+      exprVectorToNodes(d_formals),
+      Node::fromExpr(d_func).getType().getRangeType(),
+      Node::fromExpr(d_formula));
+}
+
 /* -------------------------------------------------------------------------- */
 /* class DefineFunctionRecCommand                                             */
 /* -------------------------------------------------------------------------- */
@@ -1454,6 +1669,26 @@ std::string DefineFunctionRecCommand::getCommandName() const
   return "define-fun-rec";
 }
 
+void DefineFunctionRecCommand::toStream(std::ostream& out,
+                                        int toDepth,
+                                        bool types,
+                                        size_t dag,
+                                        OutputLanguage language) const
+{
+  std::vector<std::vector<Node>> formals;
+  formals.reserve(d_formals.size());
+  for (const std::vector<api::Term>& formal : d_formals)
+  {
+    formals.push_back(api::termVectorToNodes(formal));
+  }
+
+  Printer::getPrinter(language)->toStreamCmdDefineFunctionRec(
+      out,
+      api::termVectorToNodes(d_funcs),
+      formals,
+      api::termVectorToNodes(d_formulas));
+}
+
 /* -------------------------------------------------------------------------- */
 /* class SetUserAttribute                                                     */
 /* -------------------------------------------------------------------------- */
@@ -1523,6 +1758,16 @@ std::string SetUserAttributeCommand::getCommandName() const
   return "set-user-attribute";
 }
 
+void SetUserAttributeCommand::toStream(std::ostream& out,
+                                       int toDepth,
+                                       bool types,
+                                       size_t dag,
+                                       OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdSetUserAttribute(
+      out, d_attr, Node::fromExpr(d_expr));
+}
+
 /* -------------------------------------------------------------------------- */
 /* class SimplifyCommand                                                      */
 /* -------------------------------------------------------------------------- */
@@ -1577,6 +1822,15 @@ Command* SimplifyCommand::clone() const
 
 std::string SimplifyCommand::getCommandName() const { return "simplify"; }
 
+void SimplifyCommand::toStream(std::ostream& out,
+                               int toDepth,
+                               bool types,
+                               size_t dag,
+                               OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdSimplify(out, d_term);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class ExpandDefinitionsCommand                                             */
 /* -------------------------------------------------------------------------- */
@@ -1625,6 +1879,16 @@ std::string ExpandDefinitionsCommand::getCommandName() const
   return "expand-definitions";
 }
 
+void ExpandDefinitionsCommand::toStream(std::ostream& out,
+                                        int toDepth,
+                                        bool types,
+                                        size_t dag,
+                                        OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdExpandDefinitions(
+      out, Node::fromExpr(d_term));
+}
+
 /* -------------------------------------------------------------------------- */
 /* class GetValueCommand                                                      */
 /* -------------------------------------------------------------------------- */
@@ -1724,6 +1988,16 @@ Command* GetValueCommand::clone() const
 
 std::string GetValueCommand::getCommandName() const { return "get-value"; }
 
+void GetValueCommand::toStream(std::ostream& out,
+                               int toDepth,
+                               bool types,
+                               size_t dag,
+                               OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdGetValue(
+      out, exprVectorToNodes(d_terms));
+}
+
 /* -------------------------------------------------------------------------- */
 /* class GetAssignmentCommand                                                 */
 /* -------------------------------------------------------------------------- */
@@ -1793,6 +2067,15 @@ std::string GetAssignmentCommand::getCommandName() const
   return "get-assignment";
 }
 
+void GetAssignmentCommand::toStream(std::ostream& out,
+                                    int toDepth,
+                                    bool types,
+                                    size_t dag,
+                                    OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdGetAssignment(out);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class GetModelCommand                                                      */
 /* -------------------------------------------------------------------------- */
@@ -1857,6 +2140,15 @@ Command* GetModelCommand::clone() const
 
 std::string GetModelCommand::getCommandName() const { return "get-model"; }
 
+void GetModelCommand::toStream(std::ostream& out,
+                               int toDepth,
+                               bool types,
+                               size_t dag,
+                               OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdGetModel(out);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class BlockModelCommand */
 /* -------------------------------------------------------------------------- */
@@ -1898,6 +2190,15 @@ Command* BlockModelCommand::clone() const
 
 std::string BlockModelCommand::getCommandName() const { return "block-model"; }
 
+void BlockModelCommand::toStream(std::ostream& out,
+                                 int toDepth,
+                                 bool types,
+                                 size_t dag,
+                                 OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdBlockModel(out);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class BlockModelValuesCommand */
 /* -------------------------------------------------------------------------- */
@@ -1960,6 +2261,16 @@ std::string BlockModelValuesCommand::getCommandName() const
   return "block-model-values";
 }
 
+void BlockModelValuesCommand::toStream(std::ostream& out,
+                                       int toDepth,
+                                       bool types,
+                                       size_t dag,
+                                       OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdBlockModelValues(
+      out, exprVectorToNodes(d_terms));
+}
+
 /* -------------------------------------------------------------------------- */
 /* class GetProofCommand                                                      */
 /* -------------------------------------------------------------------------- */
@@ -2020,6 +2331,15 @@ Command* GetProofCommand::clone() const
 
 std::string GetProofCommand::getCommandName() const { return "get-proof"; }
 
+void GetProofCommand::toStream(std::ostream& out,
+                               int toDepth,
+                               bool types,
+                               size_t dag,
+                               OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdGetProof(out);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class GetInstantiationsCommand                                             */
 /* -------------------------------------------------------------------------- */
@@ -2073,6 +2393,15 @@ std::string GetInstantiationsCommand::getCommandName() const
   return "get-instantiations";
 }
 
+void GetInstantiationsCommand::toStream(std::ostream& out,
+                                        int toDepth,
+                                        bool types,
+                                        size_t dag,
+                                        OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdGetInstantiations(out);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class GetSynthSolutionCommand                                              */
 /* -------------------------------------------------------------------------- */
@@ -2121,7 +2450,16 @@ Command* GetSynthSolutionCommand::clone() const
 
 std::string GetSynthSolutionCommand::getCommandName() const
 {
-  return "get-instantiations";
+  return "get-synth-solution";
+}
+
+void GetSynthSolutionCommand::toStream(std::ostream& out,
+                                       int toDepth,
+                                       bool types,
+                                       size_t dag,
+                                       OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdGetSynthSolution(out);
 }
 
 /* -------------------------------------------------------------------------- */
@@ -2218,6 +2556,19 @@ std::string GetInterpolCommand::getCommandName() const
   return "get-interpol";
 }
 
+void GetInterpolCommand::toStream(std::ostream& out,
+                                  int toDepth,
+                                  bool types,
+                                  size_t dag,
+                                  OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdGetInterpol(
+      out,
+      d_name,
+      d_conj.getNode(),
+      TypeNode::fromType(d_sygus_grammar->resolve().getType()));
+}
+
 /* -------------------------------------------------------------------------- */
 /* class GetAbductCommand                                                     */
 /* -------------------------------------------------------------------------- */
@@ -2308,6 +2659,19 @@ Command* GetAbductCommand::clone() const
 
 std::string GetAbductCommand::getCommandName() const { return "get-abduct"; }
 
+void GetAbductCommand::toStream(std::ostream& out,
+                                int toDepth,
+                                bool types,
+                                size_t dag,
+                                OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdGetAbduct(
+      out,
+      d_name,
+      d_conj.getNode(),
+      TypeNode::fromType(d_sygus_grammar->resolve().getType()));
+}
+
 /* -------------------------------------------------------------------------- */
 /* class GetQuantifierEliminationCommand                                      */
 /* -------------------------------------------------------------------------- */
@@ -2373,6 +2737,16 @@ std::string GetQuantifierEliminationCommand::getCommandName() const
   return d_doFull ? "get-qe" : "get-qe-disjunct";
 }
 
+void GetQuantifierEliminationCommand::toStream(std::ostream& out,
+                                               int toDepth,
+                                               bool types,
+                                               size_t dag,
+                                               OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdGetQuantifierElimination(
+      out, Node::fromExpr(d_expr));
+}
+
 /* -------------------------------------------------------------------------- */
 /* class GetUnsatAssumptionsCommand                                           */
 /* -------------------------------------------------------------------------- */
@@ -2439,6 +2813,15 @@ std::string GetUnsatAssumptionsCommand::getCommandName() const
   return "get-unsat-assumptions";
 }
 
+void GetUnsatAssumptionsCommand::toStream(std::ostream& out,
+                                          int toDepth,
+                                          bool types,
+                                          size_t dag,
+                                          OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdGetUnsatAssumptions(out);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class GetUnsatCoreCommand                                                  */
 /* -------------------------------------------------------------------------- */
@@ -2500,6 +2883,15 @@ std::string GetUnsatCoreCommand::getCommandName() const
   return "get-unsat-core";
 }
 
+void GetUnsatCoreCommand::toStream(std::ostream& out,
+                                   int toDepth,
+                                   bool types,
+                                   size_t dag,
+                                   OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdGetUnsatCore(out);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class GetAssertionsCommand                                                 */
 /* -------------------------------------------------------------------------- */
@@ -2557,6 +2949,15 @@ std::string GetAssertionsCommand::getCommandName() const
   return "get-assertions";
 }
 
+void GetAssertionsCommand::toStream(std::ostream& out,
+                                    int toDepth,
+                                    bool types,
+                                    size_t dag,
+                                    OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdGetAssertions(out);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class SetBenchmarkStatusCommand                                            */
 /* -------------------------------------------------------------------------- */
@@ -2603,6 +3004,15 @@ std::string SetBenchmarkStatusCommand::getCommandName() const
   return "set-info";
 }
 
+void SetBenchmarkStatusCommand::toStream(std::ostream& out,
+                                         int toDepth,
+                                         bool types,
+                                         size_t dag,
+                                         OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdSetBenchmarkStatus(out, d_status);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class SetBenchmarkLogicCommand                                             */
 /* -------------------------------------------------------------------------- */
@@ -2642,6 +3052,15 @@ std::string SetBenchmarkLogicCommand::getCommandName() const
   return "set-logic";
 }
 
+void SetBenchmarkLogicCommand::toStream(std::ostream& out,
+                                        int toDepth,
+                                        bool types,
+                                        size_t dag,
+                                        OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdSetBenchmarkLogic(out, d_logic);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class SetInfoCommand                                                       */
 /* -------------------------------------------------------------------------- */
@@ -2684,6 +3103,15 @@ Command* SetInfoCommand::clone() const
 
 std::string SetInfoCommand::getCommandName() const { return "set-info"; }
 
+void SetInfoCommand::toStream(std::ostream& out,
+                              int toDepth,
+                              bool types,
+                              size_t dag,
+                              OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdSetInfo(out, d_flag, d_sexpr);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class GetInfoCommand                                                       */
 /* -------------------------------------------------------------------------- */
@@ -2750,6 +3178,15 @@ Command* GetInfoCommand::clone() const
 
 std::string GetInfoCommand::getCommandName() const { return "get-info"; }
 
+void GetInfoCommand::toStream(std::ostream& out,
+                              int toDepth,
+                              bool types,
+                              size_t dag,
+                              OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdGetInfo(out, d_flag);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class SetOptionCommand                                                     */
 /* -------------------------------------------------------------------------- */
@@ -2791,6 +3228,15 @@ Command* SetOptionCommand::clone() const
 
 std::string SetOptionCommand::getCommandName() const { return "set-option"; }
 
+void SetOptionCommand::toStream(std::ostream& out,
+                                int toDepth,
+                                bool types,
+                                size_t dag,
+                                OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdSetOption(out, d_flag, d_sexpr);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class GetOptionCommand                                                     */
 /* -------------------------------------------------------------------------- */
@@ -2845,6 +3291,15 @@ Command* GetOptionCommand::clone() const
 
 std::string GetOptionCommand::getCommandName() const { return "get-option"; }
 
+void GetOptionCommand::toStream(std::ostream& out,
+                                int toDepth,
+                                bool types,
+                                size_t dag,
+                                OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdGetOption(out, d_flag);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class SetExpressionNameCommand                                             */
 /* -------------------------------------------------------------------------- */
@@ -2879,6 +3334,16 @@ std::string SetExpressionNameCommand::getCommandName() const
   return "set-expr-name";
 }
 
+void SetExpressionNameCommand::toStream(std::ostream& out,
+                                        int toDepth,
+                                        bool types,
+                                        size_t dag,
+                                        OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdSetExpressionName(
+      out, Node::fromExpr(d_expr), d_name);
+}
+
 /* -------------------------------------------------------------------------- */
 /* class DatatypeDeclarationCommand                                           */
 /* -------------------------------------------------------------------------- */
@@ -2922,4 +3387,14 @@ std::string DatatypeDeclarationCommand::getCommandName() const
   return "declare-datatypes";
 }
 
+void DatatypeDeclarationCommand::toStream(std::ostream& out,
+                                          int toDepth,
+                                          bool types,
+                                          size_t dag,
+                                          OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdDatatypeDeclaration(
+      out, typeVectorToTypeNodes(d_datatypes));
+}
+
 }  // namespace CVC4
diff --git a/src/smt/command.h b/src/smt/command.h
index fb7660b70..95274884f 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -210,7 +210,7 @@ class CVC4_PUBLIC Command
       int toDepth = -1,
       bool types = false,
       size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const;
+      OutputLanguage language = language::output::LANG_AUTO) const = 0;
 
   std::string toString() const;
 
@@ -308,6 +308,12 @@ class CVC4_PUBLIC EmptyCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 
  protected:
   std::string d_name;
@@ -326,6 +332,12 @@ class CVC4_PUBLIC EchoCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 
  protected:
   std::string d_output;
@@ -347,6 +359,12 @@ class CVC4_PUBLIC AssertCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class AssertCommand */
 
 class CVC4_PUBLIC PushCommand : public Command
@@ -357,6 +375,12 @@ class CVC4_PUBLIC PushCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class PushCommand */
 
 class CVC4_PUBLIC PopCommand : public Command
@@ -367,6 +391,12 @@ class CVC4_PUBLIC PopCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class PopCommand */
 
 class CVC4_PUBLIC DeclarationDefinitionCommand : public Command
@@ -402,6 +432,12 @@ class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class DeclareFunctionCommand */
 
 class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand
@@ -421,6 +457,12 @@ class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class DeclareTypeCommand */
 
 class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand
@@ -443,6 +485,12 @@ class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class DefineTypeCommand */
 
 class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand
@@ -467,6 +515,12 @@ class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 
  protected:
   /** The function we are defining */
@@ -499,6 +553,12 @@ class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand
   Command* exportTo(ExprManager* exprManager,
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class DefineNamedFunctionCommand */
 
 /**
@@ -529,6 +589,12 @@ class CVC4_PUBLIC DefineFunctionRecCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 
  protected:
   /** functions we are defining */
@@ -564,6 +630,12 @@ class CVC4_PUBLIC SetUserAttributeCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 
  private:
   SetUserAttributeCommand(const std::string& attr,
@@ -595,6 +667,12 @@ class CVC4_PUBLIC CheckSatCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 
  private:
   Expr d_expr;
@@ -620,6 +698,12 @@ class CVC4_PUBLIC CheckSatAssumingCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 
  private:
   std::vector<Expr> d_terms;
@@ -644,6 +728,12 @@ class CVC4_PUBLIC QueryCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class QueryCommand */
 
 /* ------------------- sygus commands  ------------------ */
@@ -670,6 +760,13 @@ class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand
   Command* clone() const override;
   /** returns this command's name */
   std::string getCommandName() const override;
+  /** prints this command */
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 
  protected:
   /** the declared variable */
@@ -678,37 +775,6 @@ class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand
   Type d_type;
 };
 
-/** Declares a sygus universal function variable */
-class CVC4_PUBLIC DeclareSygusFunctionCommand
-    : public DeclarationDefinitionCommand
-{
- public:
-  DeclareSygusFunctionCommand(const std::string& id, Expr func, Type type);
-  /** returns the declared function variable */
-  Expr getFunction() const;
-  /** returns the declared function variable's type */
-  Type getType() const;
-  /** invokes this command
-   *
-   * The declared sygus function variable is communicated to the SMT engine in
-   * case a synthesis conjecture is built later on.
-   */
-  void invoke(SmtEngine* smtEngine) override;
-  /** exports command to given expression manager */
-  Command* exportTo(ExprManager* exprManager,
-                    ExprManagerMapCollection& variableMap) override;
-  /** creates a copy of this command */
-  Command* clone() const override;
-  /** returns this command's name */
-  std::string getCommandName() const override;
-
- protected:
-  /** the declared function variable */
-  Expr d_func;
-  /** the declared function variable's type */
-  Type d_type;
-};
-
 /** Declares a sygus function-to-synthesize
  *
  * This command is also used for the special case in which we are declaring an
@@ -748,8 +814,7 @@ class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand
   Command* clone() const override;
   /** returns this command's name */
   std::string getCommandName() const override;
-
-  /** prints the Synth-fun command */
+  /** prints this command */
   void toStream(
       std::ostream& out,
       int toDepth = -1,
@@ -790,6 +855,13 @@ class CVC4_PUBLIC SygusConstraintCommand : public Command
   Command* clone() const override;
   /** returns this command's name */
   std::string getCommandName() const override;
+  /** prints this command */
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 
  protected:
   /** the declared constraint */
@@ -830,6 +902,13 @@ class CVC4_PUBLIC SygusInvConstraintCommand : public Command
   Command* clone() const override;
   /** returns this command's name */
   std::string getCommandName() const override;
+  /** prints this command */
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 
  protected:
   /** the place holder predicates with which to build the actual constraint
@@ -863,6 +942,13 @@ class CVC4_PUBLIC CheckSynthCommand : public Command
   Command* clone() const override;
   /** returns this command's name */
   std::string getCommandName() const override;
+  /** prints this command */
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 
  protected:
   /** result of the check-synth call */
@@ -891,6 +977,12 @@ class CVC4_PUBLIC SimplifyCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class SimplifyCommand */
 
 class CVC4_PUBLIC ExpandDefinitionsCommand : public Command
@@ -910,6 +1002,12 @@ class CVC4_PUBLIC ExpandDefinitionsCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class ExpandDefinitionsCommand */
 
 class CVC4_PUBLIC GetValueCommand : public Command
@@ -930,6 +1028,12 @@ class CVC4_PUBLIC GetValueCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class GetValueCommand */
 
 class CVC4_PUBLIC GetAssignmentCommand : public Command
@@ -947,6 +1051,12 @@ class CVC4_PUBLIC GetAssignmentCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class GetAssignmentCommand */
 
 class CVC4_PUBLIC GetModelCommand : public Command
@@ -962,6 +1072,12 @@ class CVC4_PUBLIC GetModelCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 
  protected:
   Model* d_result;
@@ -979,6 +1095,12 @@ class CVC4_PUBLIC BlockModelCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class BlockModelCommand */
 
 /** The command to block model values. */
@@ -993,6 +1115,12 @@ class CVC4_PUBLIC BlockModelValuesCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 
  protected:
   /** The terms we are blocking */
@@ -1011,6 +1139,12 @@ class CVC4_PUBLIC GetProofCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 
  protected:
   SmtEngine* d_smtEngine;
@@ -1029,6 +1163,12 @@ class CVC4_PUBLIC GetInstantiationsCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 
  protected:
   SmtEngine* d_smtEngine;
@@ -1045,6 +1185,12 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 
  protected:
   SmtEngine* d_smtEngine;
@@ -1085,6 +1231,12 @@ class CVC4_PUBLIC GetInterpolCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 
  protected:
   /** The name of the interpolation predicate */
@@ -1138,6 +1290,12 @@ class CVC4_PUBLIC GetAbductCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 
  protected:
   /** The name of the abduction predicate */
@@ -1173,6 +1331,12 @@ class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class GetQuantifierEliminationCommand */
 
 class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command
@@ -1186,6 +1350,12 @@ class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 
  protected:
   std::vector<Expr> d_result;
@@ -1204,6 +1374,12 @@ class CVC4_PUBLIC GetUnsatCoreCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 
  protected:
   // the result of the unsat core call
@@ -1225,6 +1401,12 @@ class CVC4_PUBLIC GetAssertionsCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class GetAssertionsCommand */
 
 class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command
@@ -1242,6 +1424,12 @@ class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class SetBenchmarkStatusCommand */
 
 class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command
@@ -1258,6 +1446,12 @@ class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class SetBenchmarkLogicCommand */
 
 class CVC4_PUBLIC SetInfoCommand : public Command
@@ -1277,6 +1471,12 @@ class CVC4_PUBLIC SetInfoCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class SetInfoCommand */
 
 class CVC4_PUBLIC GetInfoCommand : public Command
@@ -1297,6 +1497,12 @@ class CVC4_PUBLIC GetInfoCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class GetInfoCommand */
 
 class CVC4_PUBLIC SetOptionCommand : public Command
@@ -1316,6 +1522,12 @@ class CVC4_PUBLIC SetOptionCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class SetOptionCommand */
 
 class CVC4_PUBLIC GetOptionCommand : public Command
@@ -1336,6 +1548,12 @@ class CVC4_PUBLIC GetOptionCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class GetOptionCommand */
 
 // Set expression name command
@@ -1359,6 +1577,12 @@ class CVC4_PUBLIC SetExpressionNameCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class SetExpressionNameCommand */
 
 class CVC4_PUBLIC DatatypeDeclarationCommand : public Command
@@ -1376,6 +1600,12 @@ class CVC4_PUBLIC DatatypeDeclarationCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class DatatypeDeclarationCommand */
 
 class CVC4_PUBLIC ResetCommand : public Command
@@ -1387,6 +1617,12 @@ class CVC4_PUBLIC ResetCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class ResetCommand */
 
 class CVC4_PUBLIC ResetAssertionsCommand : public Command
@@ -1398,6 +1634,12 @@ class CVC4_PUBLIC ResetAssertionsCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class ResetAssertionsCommand */
 
 class CVC4_PUBLIC QuitCommand : public Command
@@ -1409,6 +1651,12 @@ class CVC4_PUBLIC QuitCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class QuitCommand */
 
 class CVC4_PUBLIC CommentCommand : public Command
@@ -1425,11 +1673,17 @@ class CVC4_PUBLIC CommentCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class CommentCommand */
 
 class CVC4_PUBLIC CommandSequence : public Command
 {
- private:
+ protected:
   /** All the commands to be executed (in sequence) */
   std::vector<Command*> d_commandSequence;
   /** Next command to be executed */
@@ -1458,10 +1712,22 @@ class CVC4_PUBLIC CommandSequence : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class CommandSequence */
 
 class CVC4_PUBLIC DeclarationSequence : public CommandSequence
 {
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
 };
 
 }  // namespace CVC4