Sygus print callbacks (#1348)

* Initial infrastructure for sygus printing.

* Minor

* Minor improvements

* Format

* Minor

* Empty constructor printer.

* Format

* Minor

* Format

* Address.

8 files changed, 399 insertions, 16 deletions

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index a8cd83215..f654f2608 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -907,6 +907,14 @@ bool DatatypeConstructor::isSygusIdFunc() const {
   return d_sygus_let_args.size()==1 && d_sygus_let_args[0]==d_sygus_let_body;
 }
 
+SygusPrintCallback* DatatypeConstructor::getSygusPrintCallback() const
+{
+  PrettyCheckArgument(
+      isResolved(), this, "this datatype constructor is not yet resolved");
+  // TODO  (#1344) return the stored callback
+  return nullptr;
+}
+
 Cardinality DatatypeConstructor::getCardinality( Type t ) const throw(IllegalArgumentException) {
   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index da0a9813f..a92a0738e 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -178,6 +178,32 @@ public:
   DatatypeConstructorArg(std::string name, Expr selector);
 };/* class DatatypeConstructorArg */
 
+class Printer;
+
+/** sygus datatype constructor printer
+ *
+ * This is a virtual class that is used to specify
+ * a custom printing callback for sygus terms. This is
+ * useful for sygus grammars that include defined
+ * functions or let expressions.
+ */
+class CVC4_PUBLIC SygusPrintCallback
+{
+ public:
+  SygusPrintCallback() {}
+  ~SygusPrintCallback() {}
+  /**
+   * Writes the term that sygus datatype expression e
+   * encodes to stream out. p is the printer that
+   * requested that expression e be written on output
+   * stream out. Calls may be made to p to print
+   * subterms of e.
+   */
+  virtual void toStreamSygus(const Printer* p,
+                             std::ostream& out,
+                             Expr e) const = 0;
+};
+
 /**
  * A constructor for a Datatype.
  */
@@ -286,6 +312,13 @@ class CVC4_PUBLIC DatatypeConstructor {
    * TODO (#1344) refactor this
    */
   bool isSygusIdFunc() const;
+  /** get sygus print callback
+   * This class stores custom ways of printing
+   * sygus datatype constructors, for instance,
+   * to handle defined or let expressions that
+   * appear in user-provided grammars.
+   */
+  SygusPrintCallback* getSygusPrintCallback() const;
 
   /**
    * Get the tester name for this Datatype constructor.
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index fd7a4ee19..e50b1970f 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -70,7 +70,12 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() {
   }
 }/* Printer::makePrinter() */
 
-
+void Printer::toStreamSygus(std::ostream& out, TNode n) const throw()
+{
+  // no sygus-specific printing associated with this printer,
+  // just print the original term
+  toStream(out, n, -1, false, 1);
+}
 
 void Printer::toStream(std::ostream& out, const Model& m) const throw() {
   for(size_t i = 0; i < m.getNumCommands(); ++i) {
diff --git a/src/printer/printer.h b/src/printer/printer.h
index ea4865fce..9baeeb8b6 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -69,14 +69,27 @@ public:
   /** Write a CommandStatus out to a stream with this Printer. */
   virtual void toStream(std::ostream& out, const CommandStatus* s) const throw() = 0;
 
-
-
   /** Write a Model out to a stream with this Printer. */
   virtual void toStream(std::ostream& out, const Model& m) const throw();
 
   /** Write an UnsatCore out to a stream with this Printer. */
   virtual void toStream(std::ostream& out, const UnsatCore& core) const throw();
 
+  /**
+   * Write the term that sygus datatype term n
+   * encodes to a stream with this Printer.
+   * For example, consider the datatype term
+   *   (C_plus (C_minus C_x C_0) C_y)
+   * where C_plus, C_minus, C_x, C_0, C_y are constructors
+   * whose sygus operators are PLUS, MINUS, x, 0, y.
+   * In this case, this method is equivalent to printing
+   * the integer term:
+   *   (PLUS (MINUS x 0) y)
+   * This method may make calls to sygus printing callback
+   * methods stored in sygus datatype constructors.
+   */
+  virtual void toStreamSygus(std::ostream& out, TNode n) const throw();
+
 };/* class Printer */
 
 }/* CVC4 namespace */
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 8a80ba59e..6ceb79001 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -364,9 +364,10 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::CHAIN: break;
   case kind::FUNCTION_TYPE:
     out << "->";
-    for(size_t i = 0; i < n.getNumChildren(); ++i) {
+    for (Node nc : n)
+    {
       out << " ";
-      toStream(out, n[i], toDepth, types, TypeNode::null());
+      toStream(out, nc, toDepth, types, TypeNode::null());
     }
     out << ")";
     return;
@@ -382,11 +383,13 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
 
     // uf theory
   case kind::APPLY_UF: typeChildren = true; break;
-    // higher-order
+  // higher-order
   case kind::HO_APPLY: break;
-  case kind::LAMBDA: out << smtKindString(k) << " "; break;
-  
-    // arith theory
+  case kind::LAMBDA:
+    out << smtKindString(k) << " ";
+    break;
+
+  // arith theory
   case kind::PLUS:
   case kind::MULT:
   case kind::NONLINEAR_MULT:
@@ -819,10 +822,11 @@ static string smtKindString(Kind k) throw() {
 
     // uf theory
   case kind::APPLY_UF: break;
-  
-  case kind::LAMBDA: return "lambda";
 
-    // arith theory
+  case kind::LAMBDA:
+    return "lambda";
+
+  // arith theory
   case kind::PLUS: return "+";
   case kind::MULT:
   case kind::NONLINEAR_MULT: return "*";
@@ -1310,6 +1314,47 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
   }
 }
 
+void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const throw()
+{
+  if (n.getKind() == kind::APPLY_CONSTRUCTOR)
+  {
+    TypeNode tn = n.getType();
+    const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+    if (dt.isSygus())
+    {
+      int cIndex = Datatype::indexOf(n.getOperator().toExpr());
+      Assert(!dt[cIndex].getSygusOp().isNull());
+      SygusPrintCallback* spc = dt[cIndex].getSygusPrintCallback();
+      if (spc != nullptr)
+      {
+        spc->toStreamSygus(this, out, n.toExpr());
+      }
+      else
+      {
+        if (n.getNumChildren() > 0)
+        {
+          out << "(";
+        }
+        out << dt[cIndex].getSygusOp();
+        if (n.getNumChildren() > 0)
+        {
+          for (Node nc : n)
+          {
+            out << " ";
+            toStreamSygus(out, nc);
+          }
+          out << ")";
+        }
+      }
+      return;
+    }
+  }
+  else
+  {
+    // cannot convert term to analog, print original
+    toStream(out, n, -1, false, 1);
+  }
+}
 
 static void toStream(std::ostream& out, const AssertCommand* c) throw() {
   out << "(assert " << c->getExpr() << ")";
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index b7e9e1f40..96f55d7a2 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -48,11 +48,17 @@ public:
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
   void toStream(std::ostream& out, const SExpr& sexpr) const throw();
   void toStream(std::ostream& out, const Model& m) const throw();
-  /** print the unsat core to the stream out.
-  * We use the expression names that are stored in the SMT engine associated 
-  * with the core (UnsatCore::getSmtEngine) for printing named assertions.
-  */
+  /**
+   * Writes the unsat core to the stream out.
+   * We use the expression names that are stored in the SMT engine associated
+   * with the core (UnsatCore::getSmtEngine) for printing named assertions.
+   */
   void toStream(std::ostream& out, const UnsatCore& core) const throw();
+  /**
+   * Write the term that sygus datatype term node n
+   * encodes to a stream with this Printer.
+   */
+  virtual void toStreamSygus(std::ostream& out, TNode n) const throw() override;
 };/* class Smt2Printer */
 
 }/* CVC4::printer::smt2 namespace */
diff --git a/src/printer/sygus_print_callback.cpp b/src/printer/sygus_print_callback.cpp
new file mode 100644
index 000000000..c956c32de
--- /dev/null
+++ b/src/printer/sygus_print_callback.cpp
@@ -0,0 +1,144 @@
+/*********************                                                        */
+/*! \file sygus_print_callback.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of sygus print callbacks
+ **/
+
+#include "printer/sygus_print_callback.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)
+{
+}
+
+void SygusLetExpressionConstructorPrinter::doStrReplace(
+    std::string& str, const std::string& oldStr, const std::string& newStr)
+{
+  size_t pos = 0;
+  while ((pos = str.find(oldStr, pos)) != std::string::npos)
+  {
+    str.replace(pos, oldStr.length(), newStr);
+    pos += newStr.length();
+  }
+}
+
+void SygusLetExpressionConstructorPrinter::toStreamSygus(Printer* p,
+                                                         std::ostream& out,
+                                                         Expr e)
+{
+  std::stringstream let_out;
+  // print as let term
+  if (d_sygus_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++)
+  {
+    Node v = d_sygus_let_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)
+    {
+      // it should be printed as a let argument
+      let_out << "(";
+      let_out << lv << " " << lv.getType() << " ";
+      p->toStreamSygus(let_out, e[i]);
+      let_out << ")";
+    }
+  }
+  if (d_sygus_num_let_input_args > 0)
+  {
+    let_out << ") ";
+  }
+  // print the body
+  Node slet_body = d_let_body.substitute(
+      subs_lvs.begin(), subs_lvs.end(), new_lvs.begin(), new_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)
+  {
+    let_out << ")";
+  }
+  // do variable substitutions since
+  // 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++)
+  {
+    std::stringstream old_str;
+    old_str << new_lvs[i];
+    std::stringstream new_str;
+    if (i >= d_sygus_num_let_input_args)
+    {
+      p->toStreamSygus(new_str, Node::fromExpr(e[i]));
+    }
+    else
+    {
+      new_str << d_sygus_let_args[i];
+    }
+    doStrReplace(lbody, old_str.str().c_str(), new_str.str().c_str());
+  }
+  out << lbody;
+}
+
+SygusNamedConstructorPrinter::SygusNamedConstructorPrinter(std::string name)
+    : d_name(name)
+{
+}
+
+void SygusNamedConstructorPrinter::toStreamSygus(Printer* p,
+                                                 std::ostream& out,
+                                                 Expr e)
+{
+  if (e.getNumChildren() > 0)
+  {
+    out << "(";
+  }
+  out << d_name;
+  if (e.getNumChildren() > 0)
+  {
+    for (Expr ec : e)
+    {
+      out << " ";
+      p->toStreamSygus(out, ec);
+    }
+    out << ")";
+  }
+}
+
+void SygusEmptyConstructorPrinter::toStreamSygus(const Printer* p,
+                                                 std::ostream& out,
+                                                 Expr e)
+{
+  if (e.getNumChildren() == 1)
+  {
+    p->toStreamSygus(out, e[0]);
+  }
+  else
+  {
+    Assert(false);
+  }
+}
+
+} /* CVC4::printer namespace */
+} /* CVC4 namespace */
diff --git a/src/printer/sygus_print_callback.h b/src/printer/sygus_print_callback.h
new file mode 100644
index 000000000..cdeec32f0
--- /dev/null
+++ b/src/printer/sygus_print_callback.h
@@ -0,0 +1,129 @@
+/*********************                                                        */
+/*! \file sygus_print_callback.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief sygus print callback functions
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H
+#define __CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H
+
+#include <vector>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace printer {
+
+/** sygus let expression constructor printer
+ *
+ * This class is used for printing sygus
+ * datatype constructor terms whose top symbol
+ * is a let expression.
+ * For example, for grammar:
+ *   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))
+ * CVC4's support for let expressions in grammars
+ * is highly limited, since notice that the
+ * argument y : B is unused.
+ *
+ * For the above constructor, we have that
+ *   d_let_body is (+ z 1),
+ *   d_sygus_let_args is { y, z },
+ *   d_sygus_num_let_input_args is 1, since
+ *     y is an original input argument of the
+ *     let expression, but z is not.
+ */
+class SygusLetExpressionConstructorPrinter
+    : public SygusDatatypeConstructorPrinter
+{
+ public:
+  SygusLetExpressionPrinter(Node let_body,
+                            std::vector<Node>& let_args,
+                            unsigned ninput_args);
+  ~SygusLetExpressionPrinter() {}
+  /** 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;
+};
+
+/** sygus named constructor printer
+ *
+ * This callback is used for explicitly naming
+ * the builtin term that a sygus datatype constructor
+ * should be printed as. This is used for printing
+ * terms in sygus grammars that involve defined
+ * functions. For example, for grammar :
+ *   A -> f( A ) | 0
+ * where f is defined as:
+ *   (define-fun ((x Int)) Int (+ x 1))
+ * this class can be used as a callback for printing
+ * the first sygus datatype constructor f, where we use
+ * analog operator (lambda (x) (+ x 1)).
+ */
+class SygusNamedConstructorPrinter : public SygusDatatypeConstructorPrinter
+{
+ public:
+  SygusNamedConstructorPrinter(std::string name);
+  ~SygusNamedConstructorPrinter() {}
+  /** print sygus term e on output out using printer p */
+  virtual void toStreamSygus(const Printer* p,
+                             std::ostream& out,
+                             Expr e) const override;
+
+ private:
+  /** the defined function name */
+  std::string d_name;
+};
+
+/** sygus empty printer
+ *
+ * This callback is used for printing constructors whose operators are
+ * implicit, such as identity functions. For example, for grammar :
+ *   A -> B
+ *   B -> x | 0 | 1
+ * 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
+{
+ public:
+  SygusEmptyConstructorPrinter(std::string name);
+  ~SygusEmptyConstructorPrinter() {}
+  /** print sygus term e on output out using printer p */
+  virtual void toStreamSygus(const Printer* p,
+                             std::ostream& out,
+                             Expr e) const override;
+};
+
+} /* CVC4::printer namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H */