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, 10 insertions, 22 deletions

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 */