Sygus Lambda Grammars (#1390)

1 files changed, 93 insertions, 25 deletions

diff --git a/src/printer/sygus_print_callback.cpp b/src/printer/sygus_print_callback.cpp
index c956c32de..c5287e469 100644
--- a/src/printer/sygus_print_callback.cpp
+++ b/src/printer/sygus_print_callback.cpp
@@ -14,19 +14,32 @@
 
 #include "printer/sygus_print_callback.h"
 
+#include "expr/node.h"
+#include "printer/printer.h"
+
 using namespace CVC4::kind;
 using namespace std;
 
 namespace CVC4 {
 namespace printer {
 
-SygusLetExpressionPrinter::SygusLetExpressionPrinter(
-    Node let_body, std::vector<Node>& let_args, unsigned ninput_args)
+SygusExprPrintCallback::SygusExprPrintCallback(Expr body,
+                                               std::vector<Expr>& args)
+    : d_body(body), d_body_argument(-1)
 {
+  d_args.insert(d_args.end(), args.begin(), args.end());
+  for (unsigned i = 0, size = d_args.size(); i < size; i++)
+  {
+    if (d_args[i] == d_body)
+    {
+      d_body_argument = static_cast<int>(i);
+    }
+  }
 }
 
-void SygusLetExpressionConstructorPrinter::doStrReplace(
-    std::string& str, const std::string& oldStr, const std::string& newStr)
+void SygusExprPrintCallback::doStrReplace(std::string& str,
+                                          const std::string& oldStr,
+                                          const std::string& newStr) const
 {
   size_t pos = 0;
   while ((pos = str.find(oldStr, pos)) != std::string::npos)
@@ -36,28 +49,82 @@ void SygusLetExpressionConstructorPrinter::doStrReplace(
   }
 }
 
-void SygusLetExpressionConstructorPrinter::toStreamSygus(Printer* p,
-                                                         std::ostream& out,
-                                                         Expr e)
+void SygusExprPrintCallback::toStreamSygus(const Printer* p,
+                                           std::ostream& out,
+                                           Expr e) const
+{
+  // optimization: if body is equal to an argument, then just print that one
+  if (d_body_argument >= 0)
+  {
+    p->toStreamSygus(out, Node::fromExpr(e[d_body_argument]));
+  }
+  else
+  {
+    // make substitution
+    std::vector<Node> vars;
+    std::vector<Node> subs;
+    for (unsigned i = 0, size = d_args.size(); i < size; i++)
+    {
+      vars.push_back(Node::fromExpr(d_args[i]));
+      std::stringstream ss;
+      ss << "_setpc_var_" << i;
+      Node lv = NodeManager::currentNM()->mkBoundVar(
+          ss.str(), TypeNode::fromType(d_args[i].getType()));
+      subs.push_back(lv);
+    }
+
+    // the substituted body should be a non-sygus term
+    Node sbody = Node::fromExpr(d_body);
+    sbody =
+        sbody.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
+
+    std::stringstream body_out;
+    body_out << sbody;
+
+    // do string substitution
+    Assert(e.getNumChildren() == d_args.size());
+    std::string str_body = body_out.str();
+    for (unsigned i = 0, size = d_args.size(); i < size; i++)
+    {
+      std::stringstream old_str;
+      old_str << subs[i];
+      std::stringstream new_str;
+      p->toStreamSygus(new_str, Node::fromExpr(e[i]));
+      doStrReplace(str_body, old_str.str().c_str(), new_str.str().c_str());
+    }
+    out << str_body;
+  }
+}
+
+SygusLetExprPrintCallback::SygusLetExprPrintCallback(
+    Expr let_body, std::vector<Expr>& let_args, unsigned ninput_args)
+    : SygusExprPrintCallback(let_body, let_args),
+      d_num_let_input_args(ninput_args)
+{
+}
+
+void SygusLetExprPrintCallback::toStreamSygus(const Printer* p,
+                                              std::ostream& out,
+                                              Expr e) const
 {
   std::stringstream let_out;
   // print as let term
-  if (d_sygus_num_let_input_args > 0)
+  if (d_num_let_input_args > 0)
   {
     let_out << "(let (";
   }
   std::vector<Node> subs_lvs;
   std::vector<Node> new_lvs;
-  for (unsigned i = 0; i < d_sygus_let_args.size(); i++)
+  for (unsigned i = 0, size = d_args.size(); i < size; i++)
   {
-    Node v = d_sygus_let_args[i];
+    Node v = d_args[i];
     subs_lvs.push_back(v);
     std::stringstream ss;
     ss << "_l_" << new_lvs.size();
     Node lv = NodeManager::currentNM()->mkBoundVar(ss.str(), v.getType());
     new_lvs.push_back(lv);
     // map free variables to proper terms
-    if (i < d_sygus_num_let_input_args)
+    if (i < d_num_let_input_args)
     {
       // it should be printed as a let argument
       let_out << "(";
@@ -66,16 +133,17 @@ void SygusLetExpressionConstructorPrinter::toStreamSygus(Printer* p,
       let_out << ")";
     }
   }
-  if (d_sygus_num_let_input_args > 0)
+  if (d_num_let_input_args > 0)
   {
     let_out << ") ";
   }
   // print the body
-  Node slet_body = d_let_body.substitute(
+  Node slet_body = Node::fromExpr(d_body);
+  slet_body = slet_body.substitute(
       subs_lvs.begin(), subs_lvs.end(), new_lvs.begin(), new_lvs.end());
-  new_lvs.insert(new_lvs.end(), lvs.begin(), lvs.end());
+  // new_lvs.insert(new_lvs.end(), lvs.begin(), lvs.end());
   p->toStreamSygus(let_out, slet_body);
-  if (d_sygus_num_let_input_args > 0)
+  if (d_num_let_input_args > 0)
   {
     let_out << ")";
   }
@@ -83,32 +151,32 @@ void SygusLetExpressionConstructorPrinter::toStreamSygus(Printer* p,
   // ASSUMING : let_vars are interpreted literally and do not represent a class
   // of variables
   std::string lbody = let_out.str();
-  for (unsigned i = 0; i < d_sygus_let_args.size(); i++)
+  for (unsigned i = 0, size = d_args.size(); i < size; i++)
   {
     std::stringstream old_str;
     old_str << new_lvs[i];
     std::stringstream new_str;
-    if (i >= d_sygus_num_let_input_args)
+    if (i >= d_num_let_input_args)
     {
       p->toStreamSygus(new_str, Node::fromExpr(e[i]));
     }
     else
     {
-      new_str << d_sygus_let_args[i];
+      new_str << d_args[i];
     }
     doStrReplace(lbody, old_str.str().c_str(), new_str.str().c_str());
   }
   out << lbody;
 }
 
-SygusNamedConstructorPrinter::SygusNamedConstructorPrinter(std::string name)
+SygusNamedPrintCallback::SygusNamedPrintCallback(std::string name)
     : d_name(name)
 {
 }
 
-void SygusNamedConstructorPrinter::toStreamSygus(Printer* p,
-                                                 std::ostream& out,
-                                                 Expr e)
+void SygusNamedPrintCallback::toStreamSygus(const Printer* p,
+                                            std::ostream& out,
+                                            Expr e) const
 {
   if (e.getNumChildren() > 0)
   {
@@ -126,9 +194,9 @@ void SygusNamedConstructorPrinter::toStreamSygus(Printer* p,
   }
 }
 
-void SygusEmptyConstructorPrinter::toStreamSygus(const Printer* p,
-                                                 std::ostream& out,
-                                                 Expr e)
+void SygusEmptyPrintCallback::toStreamSygus(const Printer* p,
+                                            std::ostream& out,
+                                            Expr e) const
 {
   if (e.getNumChildren() == 1)
   {