Sygus Lambda Grammars (#1390)

3 files changed, 163 insertions, 54 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 6ceb79001..82871a1d5 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1325,7 +1325,7 @@ void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const throw()
       int cIndex = Datatype::indexOf(n.getOperator().toExpr());
       Assert(!dt[cIndex].getSygusOp().isNull());
       SygusPrintCallback* spc = dt[cIndex].getSygusPrintCallback();
-      if (spc != nullptr)
+      if (spc != nullptr && options::sygusPrintCallbacks())
       {
         spc->toStreamSygus(this, out, n.toExpr());
       }
@@ -1351,8 +1351,16 @@ void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const throw()
   }
   else
   {
-    // cannot convert term to analog, print original
-    toStream(out, n, -1, false, 1);
+    Node p = n.getAttribute(theory::SygusPrintProxyAttribute());
+    if (!p.isNull())
+    {
+      out << p;
+    }
+    else
+    {
+      // cannot convert term to analog, print original
+      out << n;
+    }
   }
 }
 
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)
   {
diff --git a/src/printer/sygus_print_callback.h b/src/printer/sygus_print_callback.h
index cdeec32f0..84da0f86c 100644
--- a/src/printer/sygus_print_callback.h
+++ b/src/printer/sygus_print_callback.h
@@ -12,18 +12,62 @@
  ** \brief sygus print callback functions
  **/
 
-#include "cvc4_private.h"
+#include "cvc4_public.h"
 
 #ifndef __CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H
 #define __CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H
 
 #include <vector>
 
-#include "expr/node.h"
+#include "expr/datatype.h"
+#include "expr/expr.h"
 
 namespace CVC4 {
 namespace printer {
 
+/** sygus expression constructor printer
+ *
+ * This class is used for printing sygus datatype constructor terms whose top
+ * symbol is an expression, such as a custom defined lambda. For example, for
+ * sygus grammar:
+ *    A -> (+ x A B) | x | y
+ *    B -> 0 | 1
+ * The first constructor, call it C_f for A takes two arguments (A, B) and has
+ * sygus operator
+ *   (lambda ((z Int) (w Int)) (+ x z w))
+ * For this operator, we set a print callback that prints, e.g. the term
+ *   C_f( t1, t2 )
+ * is printed as:
+ *   "(+ x [out1] [out2])"
+ * where out1 is the result of p->toStreamSygus(out,t1) and
+ *       out2 is the result of p->toStreamSygus(out,t2).
+ */
+class CVC4_PUBLIC SygusExprPrintCallback : public SygusPrintCallback
+{
+ public:
+  SygusExprPrintCallback(Expr body, std::vector<Expr>& args);
+  ~SygusExprPrintCallback() {}
+  /** print sygus term e on output out using printer p */
+  virtual void toStreamSygus(const Printer* p,
+                             std::ostream& out,
+                             Expr e) const override;
+
+ protected:
+  /** body of the sygus term */
+  Expr d_body;
+  /** arguments */
+  std::vector<Expr> d_args;
+  /** body argument */
+  int d_body_argument;
+  /** do string replace
+   *
+   * Replaces all occurrences of oldStr with newStr in str.
+   */
+  void doStrReplace(std::string& str,
+                    const std::string& oldStr,
+                    const std::string& newStr) const;
+};
+
 /** sygus let expression constructor printer
  *
  * This class is used for printing sygus
@@ -33,8 +77,8 @@ namespace printer {
  *   A -> (let ((x B)) (+ A 1)) | x | (+ A A) | 0
  *   B -> 0 | 1
  * the first constructor for A takes as arguments
- * (B,A) and has operator
- *   (lambda ((y B) (z A)) (+ z 1))
+ * (B,A) and has sygus operator
+ *   (lambda ((y Int) (z Int)) (+ z 1))
  * CVC4's support for let expressions in grammars
  * is highly limited, since notice that the
  * argument y : B is unused.
@@ -46,32 +90,21 @@ namespace printer {
  *     y is an original input argument of the
  *     let expression, but z is not.
  */
-class SygusLetExpressionConstructorPrinter
-    : public SygusDatatypeConstructorPrinter
+class CVC4_PUBLIC SygusLetExprPrintCallback : public SygusExprPrintCallback
 {
  public:
-  SygusLetExpressionPrinter(Node let_body,
-                            std::vector<Node>& let_args,
+  SygusLetExprPrintCallback(Expr let_body,
+                            std::vector<Expr>& let_args,
                             unsigned ninput_args);
-  ~SygusLetExpressionPrinter() {}
+  ~SygusLetExprPrintCallback() {}
   /** print sygus term e on output out using printer p */
   virtual void toStreamSygus(const Printer* p,
                              std::ostream& out,
                              Expr e) const override;
 
  private:
-  /** let body of the sygus term */
-  Node d_sygus_let_body;
-  /** let arguments */
-  std::vector<Node> d_sygus_let_args;
   /** number of arguments that are interpreted as input arguments */
-  unsigned d_sygus_num_let_input_args;
-  /** do string replace
-   * Replaces all occurrences of oldStr with newStr in str.
-   */
-  void doStrReplace(std::string& str,
-                    const std::string& oldStr,
-                    const std::string& newStr) const;
+  unsigned d_num_let_input_args;
 };
 
 /** sygus named constructor printer
@@ -88,11 +121,11 @@ class SygusLetExpressionConstructorPrinter
  * the first sygus datatype constructor f, where we use
  * analog operator (lambda (x) (+ x 1)).
  */
-class SygusNamedConstructorPrinter : public SygusDatatypeConstructorPrinter
+class CVC4_PUBLIC SygusNamedPrintCallback : public SygusPrintCallback
 {
  public:
-  SygusNamedConstructorPrinter(std::string name);
-  ~SygusNamedConstructorPrinter() {}
+  SygusNamedPrintCallback(std::string name);
+  ~SygusNamedPrintCallback() {}
   /** print sygus term e on output out using printer p */
   virtual void toStreamSygus(const Printer* p,
                              std::ostream& out,
@@ -112,11 +145,11 @@ class SygusNamedConstructorPrinter : public SygusDatatypeConstructorPrinter
  * The first constructor of A, call it cons, has sygus operator (lambda (x) x).
  * Call toStreamSygus on cons( t ) should call toStreamSygus on t directly.
  */
-class SygusEmptyConstructorPrinter : public SygusDatatypeConstructorPrinter
+class CVC4_PUBLIC SygusEmptyPrintCallback : public SygusPrintCallback
 {
  public:
-  SygusEmptyConstructorPrinter(std::string name);
-  ~SygusEmptyConstructorPrinter() {}
+  SygusEmptyPrintCallback() {}
+  ~SygusEmptyPrintCallback() {}
   /** print sygus term e on output out using printer p */
   virtual void toStreamSygus(const Printer* p,
                              std::ostream& out,