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.

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 9f8451ba803c9d4a27e9767d35a153a5c44b89b9..be43a07cf7b626ed4bff23f568d31790376f645c 100644 (file)
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -238,9 +238,8 @@ void Printer::toStreamCmdDeclareVar(std::ostream& out,
 }
 
 void Printer::toStreamCmdSynthFun(std::ostream& out,
-                                  const std::string& sym,
+                                  Node f,
                                   const std::vector<Node>& vars,
-                                  TypeNode range,
                                   bool isInv,
                                   TypeNode sygusType) const
 {

diff --git a/src/printer/printer.h b/src/printer/printer.h
index bfc1dc64a3d691afcdfa9083c3df9a87aa84dca1..3c53e34e6c2929cbe5d6031bfb1dc62bed4586a3 100644 (file)
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -131,9 +131,8 @@ class Printer
 
   /** Print synth-fun command */
   virtual void toStreamCmdSynthFun(std::ostream& out,
-                                   const std::string& sym,
+                                   Node f,
                                    const std::vector<Node>& vars,
-                                   TypeNode range,
                                    bool isInv,
                                    TypeNode sygusType = TypeNode::null()) const;
 

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 1b71435388e0a8dedf44486d7f7b9ebd18a378ad..50bb79a9a4526c8d9f807cc430e61efbd21e3d9e 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -2016,14 +2016,15 @@ static void toStreamSygusGrammar(std::ostream& out, const TypeNode& t)
 }
 
 void Smt2Printer::toStreamCmdSynthFun(std::ostream& out,
-                                      const std::string& sym,
+                                      Node f,
                                       const std::vector<Node>& vars,
-                                      TypeNode range,
                                       bool isInv,
                                       TypeNode sygusType) const
 {
-  out << '(' << (isInv ? "synth-inv " : "synth-fun ") << CVC4::quoteSymbol(sym)
-      << ' ';
+  std::stringstream sym;
+  sym << f;
+  out << '(' << (isInv ? "synth-inv " : "synth-fun ")
+      << CVC4::quoteSymbol(sym.str()) << ' ';
   out << '(';
   if (!vars.empty())
   {
@@ -2041,6 +2042,8 @@ void Smt2Printer::toStreamCmdSynthFun(std::ostream& out,
   // if not invariant-to-synthesize, print return type
   if (!isInv)
   {
+    TypeNode ftn = f.getType();
+    TypeNode range = ftn.isFunction() ? ftn.getRangeType() : ftn;
     out << ' ' << range;
   }
   out << '\n';

diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 1e6be22d3908bbeb19c8a2492ea57767f3a59c5e..6ed0938f8051b967ded42e93d5b5022fad40f065 100644 (file)
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -117,13 +117,11 @@ class Smt2Printer : public CVC4::Printer
                              TypeNode type) const override;
 
   /** Print synth-fun command */
-  void toStreamCmdSynthFun(
-      std::ostream& out,
-      const std::string& sym,
-      const std::vector<Node>& vars,
-      TypeNode range,
-      bool isInv,
-      TypeNode sygusType = TypeNode::null()) const override;
+  void toStreamCmdSynthFun(std::ostream& out,
+                           Node f,
+                           const std::vector<Node>& vars,
+                           bool isInv,
+                           TypeNode sygusType = TypeNode::null()) const override;
 
   /** Print constraint command */
   void toStreamCmdConstraint(std::ostream& out, Node n) const override;

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 2a316409e0ecbb1d1f779735a6f1ceab1b4a1052..f3b0ee915eeb27973c182e766e6cf82a9f779932 100644 (file)
--- 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 3bb49b703f48dea80d141e1a90f7254ef992ab49..48ed0d5c9ed03e2fd354269265f6cc5615b96e40 100644 (file)
--- 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);
   }
 }