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

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 67dbe1036..4b1fbbe22 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -117,5 +117,23 @@ 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)
+{
+  out << "ERROR: don't know how to print " << name << " command" << std::endl;
+}
+
+void Printer::toStreamCmdSynthFun(std::ostream& out,
+                                  const std::string& sym,
+                                  const std::vector<Node>& vars,
+                                  TypeNode range,
+                                  bool isInv,
+                                  TypeNode sygusType)
+{
+  printUnknownCommand(out, "synth-fun");
+}
 
 }/* CVC4 namespace */