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, 8 insertions, 0 deletions

diff --git a/src/printer/printer.h b/src/printer/printer.h
index fd788209c..918a95729 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -65,6 +65,14 @@ class Printer
   /** Write an UnsatCore out to a stream with this Printer. */
   virtual void toStream(std::ostream& out, const UnsatCore& core) 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);
+
  protected:
   /** Derived classes can construct, but no one else. */
   Printer() {}