From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 16 Dec 2020 20:02:58 +0000 (-0600)
Subject: Simplify synth-fun printer (#5682)
X-Git-Tag: cvc5-1.0.0~2434
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bc55a9c137f92d0a21574c10a74f194e3abf4073;p=cvc5.git

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 9f8451ba8..be43a07cf 100644
--- 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 bfc1dc64a..3c53e34e6 100644
--- 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 1b7143538..50bb79a9a 100644
--- 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 1e6be22d3..6ed0938f8 100644
--- 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 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);
   }
 }