Remove sygus print callback (#4727)

This removes sygus print callbacks, since they are no longer necessary to support the sygus v1 parser.

This involved generalizing the scope of the datatype utility sygusToBuiltin. Now, printing "as sygus" simply is accomplished by doing sygusToBuiltin conversion and then calling the printer on the builtin term.

This is required for further work towards eliminating the Expr layer.

FYI @4tXJ7f

6 files changed, 18 insertions, 68 deletions

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 5a48a0220..9ec3ac5fd 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -266,7 +266,6 @@ void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){
 void Datatype::addSygusConstructor(Expr op,
                                    const std::string& cname,
                                    const std::vector<Type>& cargs,
-                                   std::shared_ptr<SygusPrintCallback> spc,
                                    int weight)
 {
   // avoid name clashes
@@ -275,7 +274,7 @@ void Datatype::addSygusConstructor(Expr op,
   std::string name = ss.str();
   unsigned cweight = weight >= 0 ? weight : (cargs.empty() ? 0 : 1);
   DatatypeConstructor c(name, cweight);
-  c.setSygus(op, spc);
+  c.setSygus(op);
   for( unsigned j=0; j<cargs.size(); j++ ){
     Debug("parser-sygus-debug") << "  arg " << j << " : " << cargs[j] << std::endl;
     std::stringstream sname;
@@ -288,12 +287,11 @@ void Datatype::addSygusConstructor(Expr op,
 void Datatype::addSygusConstructor(Kind k,
                                    const std::string& cname,
                                    const std::vector<Type>& cargs,
-                                   std::shared_ptr<SygusPrintCallback> spc,
                                    int weight)
 {
   ExprManagerScope ems(*d_em);
   Expr op = d_em->operatorOf(k);
-  addSygusConstructor(op, cname, cargs, spc, weight);
+  addSygusConstructor(op, cname, cargs, weight);
 }
 
 void Datatype::setTuple() {
@@ -526,15 +524,12 @@ DatatypeConstructor::DatatypeConstructor(std::string name, unsigned weight)
   d_internal = std::make_shared<DTypeConstructor>(name, weight);
 }
 
-void DatatypeConstructor::setSygus(Expr op,
-                                   std::shared_ptr<SygusPrintCallback> spc)
+void DatatypeConstructor::setSygus(Expr op)
 {
   PrettyCheckArgument(
       !isResolved(), this, "cannot modify a finalized Datatype constructor");
   Node opn = Node::fromExpr(op);
   d_internal->setSygus(op);
-  // print callback lives at the expression level currently
-  d_sygus_pc = spc;
 }
 
 const std::vector<DatatypeConstructorArg>* DatatypeConstructor::getArgs()
@@ -626,13 +621,6 @@ unsigned DatatypeConstructor::getWeight() const
   return d_internal->getWeight();
 }
 
-std::shared_ptr<SygusPrintCallback> DatatypeConstructor::getSygusPrintCallback() const
-{
-  PrettyCheckArgument(
-      isResolved(), this, "this datatype constructor is not yet resolved");
-  return d_sygus_pc;
-}
-
 Cardinality DatatypeConstructor::getCardinality(Type t) const
 {
   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 0da4c9f51..54095050f 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -171,32 +171,6 @@ class CVC4_PUBLIC DatatypeConstructorArg {
   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() {}
-  virtual ~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;
-};
-
 class DTypeConstructor;
 
 /**
@@ -284,14 +258,6 @@ class CVC4_PUBLIC DatatypeConstructor {
    * of the form (lambda (x) x).
    */
   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.
-   */
-  std::shared_ptr<SygusPrintCallback> getSygusPrintCallback() const;
   /** get weight
    *
    * Get the weight of this constructor. This value is used when computing the
@@ -428,7 +394,7 @@ class CVC4_PUBLIC DatatypeConstructor {
    * operator op. spc is the sygus callback of this datatype constructor,
    * which is stored in a shared pointer.
    */
-  void setSygus(Expr op, std::shared_ptr<SygusPrintCallback> spc);
+  void setSygus(Expr op);
 
   /**
    * Get the list of arguments to this constructor.
@@ -445,8 +411,6 @@ class CVC4_PUBLIC DatatypeConstructor {
   Expr d_constructor;
   /** the arguments of this constructor */
   std::vector<DatatypeConstructorArg> d_args;
-  /** sygus print callback */
-  std::shared_ptr<SygusPrintCallback> d_sygus_pc;
 };/* class DatatypeConstructor */
 
 class DType;
@@ -595,8 +559,6 @@ class CVC4_PUBLIC Datatype {
    *      this constructor encodes
    * cname : the name of the constructor (for printing only)
    * cargs : the arguments of the constructor
-   * spc : an (optional) callback that is used for custom printing. This is
-   *       to accomodate user-provided grammars in the sygus format.
    *
    * It should be the case that cargs are sygus datatypes that
    * encode the arguments of op. For example, a sygus constructor
@@ -611,7 +573,6 @@ class CVC4_PUBLIC Datatype {
   void addSygusConstructor(Expr op,
                            const std::string& cname,
                            const std::vector<Type>& cargs,
-                           std::shared_ptr<SygusPrintCallback> spc = nullptr,
                            int weight = -1);
   /**
    * Same as above, with builtin kind k.
@@ -619,7 +580,6 @@ class CVC4_PUBLIC Datatype {
   void addSygusConstructor(Kind k,
                            const std::string& cname,
                            const std::vector<Type>& cargs,
-                           std::shared_ptr<SygusPrintCallback> spc = nullptr,
                            int weight = -1);
 
   /** set that this datatype is a tuple */
diff --git a/src/expr/sygus_datatype.cpp b/src/expr/sygus_datatype.cpp
index d14f0d1a7..1efea4e15 100644
--- a/src/expr/sygus_datatype.cpp
+++ b/src/expr/sygus_datatype.cpp
@@ -14,8 +14,6 @@
 
 #include "expr/sygus_datatype.h"
 
-#include "printer/sygus_print_callback.h"
-
 using namespace CVC4::kind;
 
 namespace CVC4 {
@@ -30,14 +28,12 @@ std::string SygusDatatype::getName() const { return d_dt.getName(); }
 void SygusDatatype::addConstructor(Node op,
                                    const std::string& name,
                                    const std::vector<TypeNode>& argTypes,
-                                   std::shared_ptr<SygusPrintCallback> spc,
                                    int weight)
 {
   d_cons.push_back(SygusDatatypeConstructor());
   d_cons.back().d_op = op;
   d_cons.back().d_name = name;
   d_cons.back().d_argTypes = argTypes;
-  d_cons.back().d_pc = spc;
   d_cons.back().d_weight = weight;
 }
 
@@ -54,15 +50,14 @@ void SygusDatatype::addAnyConstantConstructor(TypeNode tn)
   std::vector<TypeNode> builtinArg;
   builtinArg.push_back(tn);
   addConstructor(
-      av, cname, builtinArg, printer::SygusEmptyPrintCallback::getEmptyPC(), 0);
+      av, cname, builtinArg, 0);
 }
 void SygusDatatype::addConstructor(Kind k,
                                    const std::vector<TypeNode>& argTypes,
-                                   std::shared_ptr<SygusPrintCallback> spc,
                                    int weight)
 {
   NodeManager* nm = NodeManager::currentNM();
-  addConstructor(nm->operatorOf(k), kindToString(k), argTypes, spc, weight);
+  addConstructor(nm->operatorOf(k), kindToString(k), argTypes, weight);
 }
 
 size_t SygusDatatype::getNumConstructors() const { return d_cons.size(); }
@@ -97,7 +92,6 @@ void SygusDatatype::initializeDatatype(TypeNode sygusType,
     d_dt.addSygusConstructor(d_cons[i].d_op.toExpr(),
                              d_cons[i].d_name,
                              cargs,
-                             d_cons[i].d_pc,
                              d_cons[i].d_weight);
   }
   Trace("sygus-type-cons") << "...built datatype " << d_dt << " ";
diff --git a/src/expr/sygus_datatype.h b/src/expr/sygus_datatype.h
index 1bf74d8d3..4342aa291 100644
--- a/src/expr/sygus_datatype.h
+++ b/src/expr/sygus_datatype.h
@@ -45,8 +45,6 @@ class SygusDatatypeConstructor
   std::string d_name;
   /** List of argument types. */
   std::vector<TypeNode> d_argTypes;
-  /** Print callback of the constructor. */
-  std::shared_ptr<SygusPrintCallback> d_pc;
   /** Weight of the constructor. */
   int d_weight;
 };
@@ -89,7 +87,6 @@ class SygusDatatype
   void addConstructor(Node op,
                       const std::string& name,
                       const std::vector<TypeNode>& argTypes,
-                      std::shared_ptr<SygusPrintCallback> spc = nullptr,
                       int weight = -1);
   /**
    * Add constructor that encodes an application of builtin kind k. Like above,
@@ -98,7 +95,6 @@ class SygusDatatype
    */
   void addConstructor(Kind k,
                       const std::vector<TypeNode>& argTypes,
-                      std::shared_ptr<SygusPrintCallback> spc = nullptr,
                       int weight = -1);
   /**
    * This adds a constructor that corresponds to the any constant constructor
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index ff6bdbde0..c97a24d6d 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -661,6 +661,15 @@ bool TypeNode::isCodatatype() const
   return false;
 }
 
+bool TypeNode::isSygusDatatype() const
+{
+  if (isDatatype())
+  {
+    return getDType().isSygus();
+  }
+  return false;
+}
+
 std::string TypeNode::toString() const {
   std::stringstream ss;
   OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage();
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 12c96d307..f957fe0d0 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -639,6 +639,9 @@ public:
   /** Is this a fully instantiated datatype type */
   bool isInstantiatedDatatype() const;
 
+  /** Is this a sygus datatype type */
+  bool isSygusDatatype() const;
+
   /**
    * Get instantiated datatype type. The type on which this method is called
    * should be a parametric datatype whose parameter list is the same size as