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.

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 67dbe1036ab88b67e711eb51c129f7976581aaab..4b1fbbe22ca05bb67d1bfb9220c41778a42e7680 100644 (file)
--- 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 fd788209c8ed20c6d2745a7c3dc4222fdff52a95..918a957292cb80b2232d96f4d9452f9a5c79bcba 100644 (file)
--- 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 b92490ae26df3305b16e6dc4bc1809b0e149085e..96a7f634d4e3555abfa4c92e258803cb3fb5be05 100644 (file)
--- 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 640521a67ee8a53794f92a079b973b122e904f57..cb1ffe9bdd40e19dddc972bdcae91642dacaf6d2 100644 (file)
--- 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 4d8f6d9105a4863d651c9ae421dbc0f711eeb8e0..f5c997318ff4f63ca5a05143651ce9cd953eb11e 100644 (file)
--- 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 1674e0a62baf4234838d3566c0cfca1899f5f3db..fb7660b70a26597ec00111cbda39d6eb78f3e475 100644 (file)
--- 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 050935422ab91b916a2ee4b13fa7f2dc151aeacd..693baede25dcd2a2a0206585ba6486ff165f4610 100644 (file)
--- 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 13865b2eca1149dde00157937851b233459689df..7f6d3db9d238b1eee1f132831a927af677b2e974 100644 (file)
--- 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();
 }