Refactor functions that print commands (Part 1) (#4869)

This PR is a step towards migrating commands to the Term/Sort level. The functions for printing synth-fun command and its grammar were modified to remove their dependency on command objects and use nodes instead of exprs and types. Similar changes to other functions that print commands will follow.

1 files changed, 14 insertions, 5 deletions

diff --git a/src/smt/command.h b/src/smt/command.h
index 1674e0a62..fb7660b70 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -205,11 +205,12 @@ class CVC4_PUBLIC Command
   virtual void invoke(SmtEngine* smtEngine) = 0;
   virtual void invoke(SmtEngine* smtEngine, std::ostream& out);
 
-  void toStream(std::ostream& out,
-                int toDepth = -1,
-                bool types = false,
-                size_t dag = 1,
-                OutputLanguage language = language::output::LANG_AUTO) const;
+  virtual void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const;
 
   std::string toString() const;
 
@@ -748,6 +749,14 @@ class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand
   /** returns this command's name */
   std::string getCommandName() const override;
 
+  /** prints the Synth-fun 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 function-to-synthesize */
   api::Term d_fun;