Simplify synth-fun printer (#5682)

Simplifies synth-fun printing to assume that the function-to-synthesize should be printed with the proper name and return type.

2 files changed, 3 insertions, 10 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 2a316409e..f3b0ee915 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -685,9 +685,8 @@ void SynthFunCommand::toStream(std::ostream& out,
   std::vector<Node> nodeVars = termVectorToNodes(d_vars);
   Printer::getPrinter(language)->toStreamCmdSynthFun(
       out,
-      d_symbol,
+      d_fun.getNode(),
       nodeVars,
-      d_sort.getTypeNode(),
       d_isInv,
       d_grammar == nullptr ? TypeNode::null()
                            : d_grammar->resolve().getTypeNode());
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3bb49b703..48ed0d5c9 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1070,7 +1070,7 @@ void SmtEngine::declareSygusVar(const std::string& id, Node var, TypeNode type)
   if (Dump.isOn("raw-benchmark"))
   {
     getOutputManager().getPrinter().toStreamCmdDeclareVar(
-        getOutputManager().getDumpOut(), var, type);
+        getOutputManager().getDumpOut(), var, var.getType());
   }
   // don't need to set that the conjecture is stale
 }
@@ -1092,13 +1092,7 @@ void SmtEngine::declareSynthFun(const std::string& id,
   if (Dump.isOn("raw-benchmark"))
   {
     getOutputManager().getPrinter().toStreamCmdSynthFun(
-        getOutputManager().getDumpOut(),
-        id,
-        vars,
-        func.getType().isFunction() ? func.getType().getRangeType()
-                                    : func.getType(),
-        isInv,
-        sygusType);
+        getOutputManager().getDumpOut(), func, vars, isInv, sygusType);
   }
 }