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.

2 files changed, 830 insertions, 89 deletions

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