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.

8 files changed, 125 insertions, 25 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 */
diff --git a/src/printer/printer.h b/src/printer/printer.h
index fd788209c..918a95729 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -65,6 +65,14 @@ class Printer
   /** Write an UnsatCore out to a stream with this Printer. */
   virtual void toStream(std::ostream& out, const UnsatCore& core) const;
 
+  /** Print synth-fun command */
+  virtual void toStreamCmdSynthFun(std::ostream& out,
+                                   const std::string& sym,
+                                   const std::vector<Node>& vars,
+                                   TypeNode range,
+                                   bool isInv,
+                                   TypeNode sygusType);
+
  protected:
   /** Derived classes can construct, but no one else. */
   Printer() {}
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index b92490ae2..96a7f634d 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1304,7 +1304,6 @@ void Smt2Printer::toStream(std::ostream& out,
       || tryToStream<CommentCommand>(out, c, d_variant)
       || tryToStream<EmptyCommand>(out, c)
       || tryToStream<EchoCommand>(out, c, d_variant)
-      || tryToStream<SynthFunCommand>(out, c)
       || tryToStream<DeclareSygusFunctionCommand>(out, c)
       || tryToStream<DeclareSygusVarCommand>(out, c)
       || tryToStream<SygusConstraintCommand>(out, c)
@@ -2019,16 +2018,15 @@ static void toStream(std::ostream& out, const EchoCommand* c, Variant v)
    --------------------------------------------------------------------------
 */
 
-static void toStreamSygusGrammar(std::ostream& out, const Type& t)
+static void toStreamSygusGrammar(std::ostream& out, const TypeNode& t)
 {
-  if (!t.isNull() && t.isDatatype()
-      && TypeNode::fromType(t).getDType().isSygus())
+  if (!t.isNull() && t.isDatatype() && t.getDType().isSygus())
   {
     std::stringstream types_predecl, types_list;
     std::set<TypeNode> grammarTypes;
     std::list<TypeNode> typesToPrint;
-    grammarTypes.insert(TypeNode::fromType(t));
-    typesToPrint.push_back(TypeNode::fromType(t));
+    grammarTypes.insert(t);
+    typesToPrint.push_back(t);
     NodeManager* nm = NodeManager::currentNM();
     // for each datatype in grammar
     //   name
@@ -2067,7 +2065,8 @@ static void toStreamSygusGrammar(std::ostream& out, const Type& t)
         }
         Node consToPrint = nm->mkNode(kind::APPLY_CONSTRUCTOR, cchildren);
         // now, print it using the conversion to builtin with external
-        types_list << theory::datatypes::utils::sygusToBuiltin(consToPrint, true);
+        types_list << theory::datatypes::utils::sygusToBuiltin(consToPrint,
+                                                               true);
         types_list << ' ';
       }
       types_list << "))\n";
@@ -2077,35 +2076,39 @@ static void toStreamSygusGrammar(std::ostream& out, const Type& t)
   }
 }
 
-static void toStream(std::ostream& out, const SynthFunCommand* c)
+void Smt2Printer::toStreamCmdSynthFun(std::ostream& out,
+                                      const std::string& sym,
+                                      const std::vector<Node>& vars,
+                                      TypeNode range,
+                                      bool isInv,
+                                      TypeNode sygusType)
 {
-  out << '(' << c->getCommandName() << ' ' << CVC4::quoteSymbol(c->getSymbol())
+  out << '(' << (isInv ? "synth-inv " : "synth-fun ") << CVC4::quoteSymbol(sym)
       << ' ';
-  const std::vector<api::Term>& vars = c->getVars();
   out << '(';
   if (!vars.empty())
   {
     // print variable list
-    std::vector<api::Term>::const_iterator i = vars.begin(), i_end = vars.end();
-    out << '(' << *i << ' ' << i->getSort() << ')';
+    std::vector<Node>::const_iterator i = vars.cbegin(), i_end = vars.cend();
+    out << '(' << *i << ' ' << i->getType() << ')';
     ++i;
     while (i != i_end)
     {
-      out << " (" << *i << ' ' << i->getSort() << ')';
+      out << " (" << *i << ' ' << i->getType() << ')';
       ++i;
     }
   }
   out << ')';
   // if not invariant-to-synthesize, print return type
-  if (!c->isInv())
+  if (!isInv)
   {
-    out << ' ' << c->getSort();
+    out << ' ' << range;
   }
   out << '\n';
   // print grammar, if any
-  if (c->getGrammar() != nullptr)
+  if (sygusType != TypeNode::null())
   {
-    out << *c->getGrammar();
+    toStreamSygusGrammar(out, sygusType);
   }
   out << ')';
 }
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 640521a67..cb1ffe9bd 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -58,6 +58,14 @@ class Smt2Printer : public CVC4::Printer {
    */
   void toStream(std::ostream& out, const UnsatCore& core) 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) override;
+
  private:
   void toStream(
       std::ostream& out, TNode n, int toDepth, bool types, TypeNode nt) const;
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 */
 /* -------------------------------------------------------------------------- */
diff --git a/src/smt/command.h b/src/smt/command.h
index 1674e0a62..fb7660b70 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -205,11 +205,12 @@ class CVC4_PUBLIC Command
   virtual void invoke(SmtEngine* smtEngine) = 0;
   virtual void invoke(SmtEngine* smtEngine, std::ostream& out);
 
-  void toStream(std::ostream& out,
-                int toDepth = -1,
-                bool types = false,
-                size_t dag = 1,
-                OutputLanguage language = language::output::LANG_AUTO) const;
+  virtual void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const;
 
   std::string toString() const;
 
@@ -748,6 +749,14 @@ class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand
   /** returns this command's name */
   std::string getCommandName() const override;
 
+  /** prints the Synth-fun command */
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
+
  protected:
   /** the function-to-synthesize */
   api::Term d_fun;
diff --git a/src/smt/dump.h b/src/smt/dump.h
index 050935422..693baede2 100644
--- a/src/smt/dump.h
+++ b/src/smt/dump.h
@@ -40,6 +40,17 @@ class CVC4_PUBLIC CVC4dumpstream
     return *this;
   }
 
+  // Note(abdoo8080): temporarily overloading operator<< for strings to allow us
+  // to print commands provided as strings
+  CVC4dumpstream& operator<<(const std::string& str)
+  {
+    if (d_os != nullptr)
+    {
+      (*d_os) << str << std::endl;
+    }
+    return *this;
+  }
+
  private:
   std::ostream* d_os;
 }; /* class CVC4dumpstream */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 13865b2ec..7f6d3db9d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1324,9 +1324,36 @@ void SmtEngine::declareSynthFun(const std::string& id,
     setUserAttribute("sygus-synth-grammar", func, attr_value, "");
   }
   Trace("smt") << "SmtEngine::declareSynthFun: " << func << "\n";
-  // dumping SynthFunCommand from smt-engine is currently broken (please take at
-  // CVC4/cvc4-projects#211)
-  // Dump("raw-benchmark") << SynthFunCommand(id, func, sygusType, isInv, vars);
+
+  // !!! TEMPORARY: We cannot construct a SynthFunCommand since we cannot
+  // construct a Term-level Grammar from a Node-level sygus TypeNode. Thus we
+  // must print the command using the Node-level utility method for now.
+
+  if (Dump.isOn("raw-benchmark"))
+  {
+    std::vector<Node> nodeVars;
+    nodeVars.reserve(vars.size());
+    for (const Expr& var : vars)
+    {
+      nodeVars.push_back(Node::fromExpr(var));
+    }
+
+    std::stringstream ss;
+
+    Printer::getPrinter(options::outputLanguage())
+        ->toStreamCmdSynthFun(
+            ss,
+            id,
+            nodeVars,
+            func.getType().isFunction()
+                ? TypeNode::fromType(func.getType()).getRangeType()
+                : TypeNode::fromType(func.getType()),
+            isInv,
+            TypeNode::fromType(sygusType));
+
+    Dump("raw-benchmark") << ss.str();
+  }
+
   // sygus conjecture is now stale
   setSygusConjectureStale();
 }