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

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 4d8f6d910..f5c997318 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -719,6 +719,22 @@ std::string SynthFunCommand::getCommandName() const
   return d_isInv ? "synth-inv" : "synth-fun";
 }
 
+void SynthFunCommand::toStream(std::ostream& out,
+                               int toDepth,
+                               bool types,
+                               size_t dag,
+                               OutputLanguage language) const
+{
+  std::vector<Node> nodeVars = termVectorToNodes(d_vars);
+  Printer::getPrinter(language)->toStreamCmdSynthFun(
+      out,
+      d_symbol,
+      nodeVars,
+      TypeNode::fromType(d_sort.getType()),
+      d_isInv,
+      TypeNode::fromType(d_grammar->resolve().getType()));
+}
+
 /* -------------------------------------------------------------------------- */
 /* class SygusConstraintCommand */
 /* -------------------------------------------------------------------------- */