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

34 files changed, 127 insertions, 575 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 278632a90..af2d0b782 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -116,8 +116,6 @@ libcvc4_add_sources(
   printer/printer.h
   printer/smt2/smt2_printer.cpp
   printer/smt2/smt2_printer.h
-  printer/sygus_print_callback.cpp
-  printer/sygus_print_callback.h
   printer/tptp/tptp_printer.cpp
   printer/tptp/tptp_printer.h
   proof/arith_proof.cpp
@@ -987,7 +985,6 @@ install(FILES
         DESTINATION
           ${INCLUDE_INSTALL_DIR}/cvc4/parser)
 install(FILES
-          printer/sygus_print_callback.h
         DESTINATION
           ${INCLUDE_INSTALL_DIR}/cvc4/printer)
 install(FILES
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 456e5a606..fcf0c028e 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -49,7 +49,6 @@
 #include "options/main_options.h"
 #include "options/options.h"
 #include "options/smt_options.h"
-#include "printer/sygus_print_callback.h"
 #include "smt/model.h"
 #include "smt/smt_engine.h"
 #include "theory/logic_info.h"
@@ -2553,10 +2552,6 @@ void Grammar::addSygusConstructorTerm(
   Term op = purifySygusGTerm(term, args, cargs, ntsToUnres);
   std::stringstream ssCName;
   ssCName << op.getKind();
-  std::shared_ptr<SygusPrintCallback> spc;
-  // callback prints as the expression
-  spc = std::make_shared<printer::SygusExprPrintCallback>(
-      *op.d_expr, termVectorToExprs(args));
   if (!args.empty())
   {
     Term lbvl = Term(d_solver,
@@ -2568,7 +2563,7 @@ void Grammar::addSygusConstructorTerm(
                                                  {*lbvl.d_expr, *op.d_expr}));
   }
   dt.d_dtype->addSygusConstructor(
-      *op.d_expr, ssCName.str(), sortVectorToTypes(cargs), spc);
+      *op.d_expr, ssCName.str(), sortVectorToTypes(cargs));
 }
 
 Term Grammar::purifySygusGTerm(
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
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 2e17d812c..69c4eabfd 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -23,7 +23,6 @@
 #include "parser/antlr_input.h"
 #include "parser/parser.h"
 #include "parser/smt2/smt2_input.h"
-#include "printer/sygus_print_callback.h"
 #include "util/bitvector.h"
 
 // ANTLR defines these, which is really bad!
@@ -929,10 +928,6 @@ void Smt2::addSygusConstructorTerm(
   Trace("parser-sygus2") << "Purified operator " << op
                          << ", #args/cargs=" << args.size() << "/"
                          << cargs.size() << std::endl;
-  std::shared_ptr<SygusPrintCallback> spc;
-  // callback prints as the expression
-  spc = std::make_shared<printer::SygusExprPrintCallback>(
-      op.getExpr(), api::termVectorToExprs(args));
   if (!args.empty())
   {
     api::Term lbvl = d_solver->mkTerm(api::BOUND_VAR_LIST, args);
@@ -942,7 +937,7 @@ void Smt2::addSygusConstructorTerm(
   Trace("parser-sygus2") << "addSygusConstructor:  operator " << op
                          << std::endl;
   dt.getDatatype().addSygusConstructor(
-      op.getExpr(), ssCName.str(), api::sortVectorToTypes(cargs), spc);
+      op.getExpr(), ssCName.str(), api::sortVectorToTypes(cargs));
 }
 
 api::Term Smt2::purifySygusGTerm(api::Term term,
diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index 699899c1e..d0ebe5f19 100644
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -20,7 +20,6 @@
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
-#include "printer/sygus_print_callback.h"
 #include "theory/quantifiers/candidate_rewrite_database.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
@@ -344,7 +343,6 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
           sdts[i].addConstructor(lambdaOp,
                                  sscs.str(),
                                  argListc,
-                                 printer::SygusEmptyPrintCallback::getEmptyPC(),
                                  0);
         }
         // recursive apply
@@ -413,7 +411,6 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
       sdttl.addConstructor(lambdaOp,
                            ssc.str(),
                            argList,
-                           printer::SygusEmptyPrintCallback::getEmptyPC(),
                            0);
       Trace("srs-input-debug")
           << "Grammar for subterm " << n << " is: " << std::endl;
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 5d54759b9..67dbe1036 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -69,14 +69,6 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang)
   }
 }
 
-void Printer::toStreamSygus(std::ostream& out, TNode n) const
-{
-  // no sygus-specific printing associated with this printer,
-  // just print the original term, without letification (the fifth argument is
-  // set to 0).
-  toStream(out, n, -1, false, 0);
-}
-
 void Printer::toStream(std::ostream& out, const Model& m) const
 {
   for(size_t i = 0; i < m.getNumCommands(); ++i) {
diff --git a/src/printer/printer.h b/src/printer/printer.h
index b18e318ee..fd788209c 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -65,21 +65,6 @@ class Printer
   /** Write an UnsatCore out to a stream with this Printer. */
   virtual void toStream(std::ostream& out, const UnsatCore& core) const;
 
-  /**
-   * 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;
-
  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 49f786f78..23503ea28 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -35,6 +35,7 @@
 #include "smt_util/boolean_simplification.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/substitutions.h"
 #include "theory/theory_model.h"
 #include "util/smt2_quote_string.h"
@@ -1493,51 +1494,6 @@ void Smt2Printer::toStream(std::ostream& out,
   }
 }
 
-void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const
-{
-  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().get();
-      if (spc != nullptr && options::sygusPrintCallbacks())
-      {
-        spc->toStreamSygus(this, out, n.toExpr());
-      }
-      else
-      {
-        if (n.getNumChildren() > 0)
-        {
-          out << "(";
-        }
-        // print operator without letification (the fifth argument is set to 0).
-        toStream(out, dt[cIndex].getSygusOp(), -1, false, 0);
-        if (n.getNumChildren() > 0)
-        {
-          for (Node nc : n)
-          {
-            out << " ";
-            toStreamSygus(out, nc);
-          }
-          out << ")";
-        }
-      }
-      return;
-    }
-  }
-  Node p = n.getAttribute(theory::SygusPrintProxyAttribute());
-  if (p.isNull())
-  {
-    p = n;
-  }
-  // cannot convert term to analog, print original, without letification.
-  toStream(out, p, -1, false, 0);
-}
-
 static void toStream(std::ostream& out, const AssertCommand* c)
 {
   out << "(assert " << c->getExpr() << ")";
@@ -2066,8 +2022,6 @@ static void toStreamSygusGrammar(std::ostream& out, const Type& t)
     //   name
     //   sygus type
     //   constructors in order
-    Printer* sygus_printer =
-        Printer::getPrinter(language::output::LANG_SYGUS_V2);
     do
     {
       Type curr = typesToPrint.front();
@@ -2100,8 +2054,8 @@ static void toStreamSygusGrammar(std::ostream& out, const Type& t)
           }
         }
         Node consToPrint = nm->mkNode(kind::APPLY_CONSTRUCTOR, cchildren);
-        // now, print it
-        sygus_printer->toStreamSygus(types_list, consToPrint);
+        // now, print it using the conversion to builtin with external
+        types_list << theory::datatypes::utils::sygusToBuiltin(consToPrint, true);
         types_list << ' ';
       }
       types_list << "))\n";
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 398e510cb..640521a67 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -57,11 +57,6 @@ class Smt2Printer : public CVC4::Printer {
    * with the core (UnsatCore::getSmtEngine) for printing named assertions.
    */
   void toStream(std::ostream& out, const UnsatCore& core) const override;
-  /**
-   * Write the term that sygus datatype term node n
-   * encodes to a stream with this Printer.
-   */
-  void toStreamSygus(std::ostream& out, TNode n) const override;
 
  private:
   void toStream(
diff --git a/src/printer/sygus_print_callback.cpp b/src/printer/sygus_print_callback.cpp
deleted file mode 100644
index a15bde3c3..000000000
--- a/src/printer/sygus_print_callback.cpp
+++ /dev/null
@@ -1,142 +0,0 @@
-/*********************                                                        */
-/*! \file sygus_print_callback.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Haniel Barbosa
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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"
-
-#include "expr/node.h"
-#include "printer/printer.h"
-
-using namespace CVC4::kind;
-using namespace std;
-
-namespace CVC4 {
-namespace printer {
-
-SygusExprPrintCallback::SygusExprPrintCallback(Expr body,
-                                               const 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 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)
-  {
-    str.replace(pos, oldStr.length(), newStr);
-    pos += newStr.length();
-  }
-}
-
-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());
-
-    // print to stream without letification
-    std::stringstream body_out;
-    p->toStream(body_out, sbody, -1, false, 0);
-
-    // 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;
-  }
-}
-
-SygusNamedPrintCallback::SygusNamedPrintCallback(std::string name)
-    : d_name(name)
-{
-}
-
-void SygusNamedPrintCallback::toStreamSygus(const Printer* p,
-                                            std::ostream& out,
-                                            Expr e) const
-{
-  if (e.getNumChildren() > 0)
-  {
-    out << "(";
-  }
-  out << d_name;
-  if (e.getNumChildren() > 0)
-  {
-    for (Expr ec : e)
-    {
-      out << " ";
-      p->toStreamSygus(out, ec);
-    }
-    out << ")";
-  }
-}
-
-void SygusEmptyPrintCallback::toStreamSygus(const Printer* p,
-                                            std::ostream& out,
-                                            Expr e) const
-{
-  if (e.getNumChildren() == 1)
-  {
-    p->toStreamSygus(out, e[0]);
-  }
-  else
-  {
-    Assert(false);
-  }
-}
-
-std::shared_ptr<SygusEmptyPrintCallback> SygusEmptyPrintCallback::d_empty_pc = nullptr;
-
-} /* CVC4::printer namespace */
-} /* CVC4 namespace */
diff --git a/src/printer/sygus_print_callback.h b/src/printer/sygus_print_callback.h
deleted file mode 100644
index 925c80ae8..000000000
--- a/src/printer/sygus_print_callback.h
+++ /dev/null
@@ -1,136 +0,0 @@
-/*********************                                                        */
-/*! \file sygus_print_callback.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Haniel Barbosa, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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_public.h"
-
-#ifndef CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H
-#define CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H
-
-#include <vector>
-
-#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, const 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 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 CVC4_PUBLIC SygusNamedPrintCallback : public SygusPrintCallback
-{
- public:
-  SygusNamedPrintCallback(std::string name);
-  ~SygusNamedPrintCallback() {}
-  /** 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 CVC4_PUBLIC SygusEmptyPrintCallback : public SygusPrintCallback
-{
- public:
-  SygusEmptyPrintCallback() {}
-  ~SygusEmptyPrintCallback() {}
-  /** print sygus term e on output out using printer p */
-  virtual void toStreamSygus(const Printer* p,
-                             std::ostream& out,
-                             Expr e) const override;
-  /* Retrieves empty callback pointer */
-  static inline std::shared_ptr<SygusEmptyPrintCallback> getEmptyPC()
-  {
-    if (!d_empty_pc)
-    {
-      d_empty_pc = std::make_shared<SygusEmptyPrintCallback>();
-    }
-    return d_empty_pc;
-  }
-
- private:
-  /* empty callback object */
-  static std::shared_ptr<SygusEmptyPrintCallback> d_empty_pc;
-};
-
-} /* CVC4::printer namespace */
-} /* CVC4 namespace */
-
-#endif /* CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H */
diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp
index 3caee52f9..e95b66bd7 100644
--- a/src/theory/datatypes/sygus_datatype_utils.cpp
+++ b/src/theory/datatypes/sygus_datatype_utils.cpp
@@ -19,7 +19,6 @@
 #include "expr/dtype.h"
 #include "expr/node_algorithm.h"
 #include "expr/sygus_datatype.h"
-#include "printer/sygus_print_callback.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/evaluator.h"
@@ -327,9 +326,18 @@ struct SygusToBuiltinTermAttributeId
 typedef expr::Attribute<SygusToBuiltinTermAttributeId, Node>
     SygusToBuiltinTermAttribute;
 
+// A variant of the above attribute for cases where we introduce a fresh
+// variable. This is to support sygusToBuiltin on non-constant sygus terms,
+// where sygus variables should be mapped to canonical builtin variables.
+// It is important to cache this so that sygusToBuiltin is deterministic.
+struct SygusToBuiltinVarAttributeId
+{
+};
+typedef expr::Attribute<SygusToBuiltinVarAttributeId, Node>
+    SygusToBuiltinVarAttribute;
+
 Node sygusToBuiltin(Node n, bool isExternal)
 {
-  Assert(n.isConst());
   std::unordered_map<TNode, Node, TNodeHashFunction> visited;
   std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
   std::vector<TNode> visit;
@@ -343,6 +351,9 @@ Node sygusToBuiltin(Node n, bool isExternal)
     it = visited.find(cur);
     if (it == visited.end())
     {
+      // Notice this condition succeeds in roughly 99% of the executions of this
+      // method (based on our coverage tests), hence the else if / else cases
+      // below do not significantly impact performance.
       if (cur.getKind() == APPLY_CONSTRUCTOR)
       {
         if (!isExternal && cur.hasAttribute(SygusToBuiltinTermAttribute()))
@@ -359,6 +370,27 @@ Node sygusToBuiltin(Node n, bool isExternal)
           }
         }
       }
+      else if (cur.getType().isSygusDatatype())
+      {
+        Assert (cur.isVar());
+        if (cur.hasAttribute(SygusToBuiltinVarAttribute()))
+        {
+          // use the previously constructed variable for it
+          visited[cur] = cur.getAttribute(SygusToBuiltinVarAttribute());
+        }
+        else
+        {
+          std::stringstream ss;
+          ss << cur;
+          const DType& dt = cur.getType().getDType();
+          // make a fresh variable
+          NodeManager * nm = NodeManager::currentNM();
+          Node var = nm->mkBoundVar(ss.str(), dt.getSygusType());
+          SygusToBuiltinVarAttribute stbv;
+          cur.setAttribute(stbv, var);
+          visited[cur] = var;
+        }
+      }
       else
       {
         // non-datatypes are themselves
@@ -664,28 +696,10 @@ TypeNode substituteAndGeneralizeSygusType(TypeNode sdt,
               << "    Arg #" << k << ": " << argtNew << std::endl;
           cargs.push_back(argtNew);
         }
-        // callback prints as the expression
-        std::shared_ptr<SygusPrintCallback> spc;
-        std::vector<Expr> args;
-        if (op.getKind() == LAMBDA)
-        {
-          Node opBody = op[1];
-          for (const Node& v : op[0])
-          {
-            args.push_back(v.toExpr());
-          }
-          spc = std::make_shared<printer::SygusExprPrintCallback>(
-              opBody.toExpr(), args);
-        }
-        else if (cargs.empty())
-        {
-          spc = std::make_shared<printer::SygusExprPrintCallback>(op.toExpr(),
-                                                                  args);
-        }
         std::stringstream ss;
         ss << ops.getKind();
         Trace("dtsygus-gen-debug") << "Add constructor : " << ops << std::endl;
-        sdts.back().addConstructor(ops, ss.str(), cargs, spc);
+        sdts.back().addConstructor(ops, ss.str(), cargs);
       }
       Trace("dtsygus-gen-debug")
           << "Set sygus : " << dtc.getSygusType() << " " << abvl << std::endl;
diff --git a/src/theory/datatypes/sygus_datatype_utils.h b/src/theory/datatypes/sygus_datatype_utils.h
index 593577b8e..88ee6d33b 100644
--- a/src/theory/datatypes/sygus_datatype_utils.h
+++ b/src/theory/datatypes/sygus_datatype_utils.h
@@ -145,7 +145,7 @@ Node applySygusArgs(const DType& dt,
                     const std::vector<Node>& args);
 /** Sygus to builtin
  *
- * This method converts a constant term of SyGuS datatype type to its builtin
+ * This method converts a term n of SyGuS datatype type to its builtin
  * equivalent. For example, given input C_*( C_x(), C_y() ), this method returns
  * x*y, assuming C_+, C_x, and C_y have sygus operators *, x, and y
  * respectively.
@@ -154,8 +154,12 @@ Node applySygusArgs(const DType& dt,
  * that was provided. This includes the use of defined functions. This argument
  * should typically be false, unless we are e.g. exporting the value of the
  * term as a final solution.
+ * 
+ * If n is not constant, then its non-constant subterms that have sygus
+ * datatype types are replaced by fresh variables (of the same name, if that
+ * subterm is a variable, and having arbitrary name otherwise).
  */
-Node sygusToBuiltin(Node c, bool isExternal = false);
+Node sygusToBuiltin(Node n, bool isExternal = false);
 /** Sygus to builtin eval
  *
  * This method returns the rewritten form of (DT_SYGUS_EVAL n args). Notice that
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index fda08bb0e..c279f0558 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -1566,8 +1566,7 @@ void SygusExtension::check( std::vector< Node >& lemmas ) {
       {
         Trace("dt-sygus") << "* DT model : " << prog << " -> ";
         std::stringstream ss;
-        Printer::getPrinter(options::outputLanguage())
-            ->toStreamSygus(ss, progv);
+        quantifiers::TermDbSygus::toStreamSygus(ss, progv);
         Trace("dt-sygus") << ss.str() << std::endl;
       }
       // first check that the value progv for prog is what we expected
diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index cabd78643..4593f36f1 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -202,10 +202,9 @@ bool CandidateRewriteDatabase::addTerm(Node sol,
           out << "(" << (verified ? "" : "candidate-") << "rewrite ";
           if (d_using_sygus)
           {
-            Printer* p = Printer::getPrinter(options::outputLanguage());
-            p->toStreamSygus(out, sol);
+            TermDbSygus::toStreamSygus(out, sol);
             out << " ";
-            p->toStreamSygus(out, eq_sol);
+            TermDbSygus::toStreamSygus(out, eq_sol);
           }
           else
           {
diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp
index c89fc6424..45b627ba4 100644
--- a/src/theory/quantifiers/candidate_rewrite_filter.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp
@@ -163,12 +163,11 @@ bool CandidateRewriteFilter::filterPair(Node n, Node eq_n)
   }
   if (Trace.isOn("sygus-rr-filter"))
   {
-    Printer* p = Printer::getPrinter(options::outputLanguage());
     std::stringstream ss;
     ss << "(redundant-rewrite ";
-    p->toStreamSygus(ss, n);
+    TermDbSygus::toStreamSygus(ss, n);
     ss << " ";
-    p->toStreamSygus(ss, eq_n);
+    TermDbSygus::toStreamSygus(ss, eq_n);
     ss << ")";
     Trace("sygus-rr-filter") << ss.str() << std::endl;
   }
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index de75af083..dcdd89c1b 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -297,11 +297,10 @@ bool CegisCoreConnective::constructSolution(
   {
     Trace("sygus-ccore")
         << "CegisCoreConnective: Construct candidate solutions..." << std::endl;
-    Printer* p = Printer::getPrinter(options::outputLanguage());
     for (unsigned i = 0, size = candidates.size(); i < size; i++)
     {
       std::stringstream ss;
-      p->toStreamSygus(ss, candidate_values[i]);
+      TermDbSygus::toStreamSygus(ss, candidate_values[i]);
       Trace("sygus-ccore") << "  " << candidates[i] << " -> " << ss.str()
                            << std::endl;
     }
diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
index 64e604d0b..91df9d0d6 100644
--- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
@@ -97,7 +97,7 @@ void EnumStreamPermutation::reset(Node value)
       for (const Node& var : p.second)
       {
         std::stringstream ss;
-        Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, var);
+        TermDbSygus::toStreamSygus(ss, var);
         Trace("synth-stream-concrete") << " " << ss.str();
       }
       Trace("synth-stream-concrete") << " ]";
@@ -111,7 +111,7 @@ Node EnumStreamPermutation::getNext()
   if (Trace.isOn("synth-stream-concrete"))
   {
     std::stringstream ss;
-    Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, d_value);
+    TermDbSygus::toStreamSygus(ss, d_value);
     Trace("synth-stream-concrete")
         << " ....streaming next permutation for value : " << ss.str()
         << " with " << d_perm_state_class.size() << " permutation classes\n";
@@ -203,8 +203,7 @@ Node EnumStreamPermutation::getNext()
   if (Trace.isOn("synth-stream-concrete"))
   {
     std::stringstream ss;
-    Printer::getPrinter(options::outputLanguage())
-        ->toStreamSygus(ss, perm_value);
+    TermDbSygus::toStreamSygus(ss, perm_value);
     Trace("synth-stream-concrete")
         << " ....return new perm " << ss.str() << "\n";
   }
@@ -291,8 +290,7 @@ void EnumStreamPermutation::PermutationState::getLastPerm(
     if (Trace.isOn("synth-stream-concrete"))
     {
       std::stringstream ss;
-      Printer::getPrinter(options::outputLanguage())
-          ->toStreamSygus(ss, d_vars[d_last_perm[i]]);
+      TermDbSygus::toStreamSygus(ss, d_vars[d_last_perm[i]]);
       Trace("synth-stream-concrete") << " " << ss.str();
     }
     vars.push_back(d_vars[d_last_perm[i]]);
@@ -373,7 +371,7 @@ void EnumStreamSubstitution::resetValue(Node value)
   if (Trace.isOn("synth-stream-concrete"))
   {
     std::stringstream ss;
-    Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, value);
+    TermDbSygus::toStreamSygus(ss, value);
     Trace("synth-stream-concrete")
         << " * Streaming concrete: registering value " << ss.str() << "\n";
   }
@@ -402,7 +400,7 @@ void EnumStreamSubstitution::resetValue(Node value)
       for (const Node& var : p.second)
       {
         std::stringstream ss;
-        Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, var);
+        TermDbSygus::toStreamSygus(ss, var);
         Trace("synth-stream-concrete") << " " << ss.str();
       }
       Trace("synth-stream-concrete") << " ]";
@@ -416,7 +414,7 @@ Node EnumStreamSubstitution::getNext()
   if (Trace.isOn("synth-stream-concrete"))
   {
     std::stringstream ss;
-    Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, d_value);
+    TermDbSygus::toStreamSygus(ss, d_value);
     Trace("synth-stream-concrete")
         << " ..streaming next combination of " << ss.str() << "\n";
   }
@@ -471,7 +469,7 @@ Node EnumStreamSubstitution::getNext()
   if (Trace.isOn("synth-stream-concrete-debug"))
   {
     std::stringstream ss;
-    Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, d_last);
+    TermDbSygus::toStreamSygus(ss, d_last);
     Trace("synth-stream-concrete-debug")
         << " ..using base perm " << ss.str() << "\n";
   }
@@ -521,8 +519,7 @@ Node EnumStreamSubstitution::getNext()
   if (Trace.isOn("synth-stream-concrete"))
   {
     std::stringstream ss;
-    Printer::getPrinter(options::outputLanguage())
-        ->toStreamSygus(ss, comb_value);
+    TermDbSygus::toStreamSygus(ss, comb_value);
     Trace("synth-stream-concrete")
         << " ....register new comb value " << ss.str()
         << " with rewritten form " << builtin_comb_value
@@ -531,20 +528,21 @@ Node EnumStreamSubstitution::getNext()
   if (!builtin_comb_value.isConst()
       && !d_comb_values.insert(builtin_comb_value).second)
   {
-    std::stringstream ss, ss1;
-    Printer::getPrinter(options::outputLanguage())
-        ->toStreamSygus(ss, comb_value);
-    Trace("synth-stream-concrete")
-        << " ..term " << ss.str() << " is REDUNDANT with " << builtin_comb_value
-        << "\n ..excluding all other concretizations (had "
-        << d_comb_values.size() << " already)\n\n";
+    if (Trace.isOn("synth-stream-concrete"))
+    {
+      std::stringstream ss, ss1;
+      TermDbSygus::toStreamSygus(ss, comb_value);
+      Trace("synth-stream-concrete")
+          << " ..term " << ss.str() << " is REDUNDANT with " << builtin_comb_value
+          << "\n ..excluding all other concretizations (had "
+          << d_comb_values.size() << " already)\n\n";
+    }
     return Node::null();
   }
   if (Trace.isOn("synth-stream-concrete"))
   {
     std::stringstream ss;
-    Printer::getPrinter(options::outputLanguage())
-        ->toStreamSygus(ss, comb_value);
+    TermDbSygus::toStreamSygus(ss, comb_value);
     Trace("synth-stream-concrete")
         << " ..return new comb " << ss.str() << "\n\n";
   }
@@ -581,8 +579,7 @@ void EnumStreamSubstitution::CombinationState::getLastComb(
     if (Trace.isOn("synth-stream-concrete"))
     {
       std::stringstream ss;
-      Printer::getPrinter(options::outputLanguage())
-          ->toStreamSygus(ss, d_vars[d_last_comb[i]]);
+      TermDbSygus::toStreamSygus(ss, d_vars[d_last_comb[i]]);
       Trace("synth-stream-concrete") << " " << ss.str();
     }
     vars.push_back(d_vars[d_last_comb[i]]);
diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp
index b71a92260..ee37d7b4b 100644
--- a/src/theory/quantifiers/sygus/sygus_abduct.cpp
+++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp
@@ -19,7 +19,6 @@
 #include "expr/dtype.h"
 #include "expr/node_algorithm.h"
 #include "expr/sygus_datatype.h"
-#include "printer/sygus_print_callback.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index cb30a408e..bd5f7ae50 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -18,7 +18,6 @@
 
 #include "expr/datatype.h"
 #include "options/quantifiers_options.h"
-#include "printer/sygus_print_callback.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/sygus/sygus_grammar_norm.h"
@@ -492,7 +491,7 @@ bool CegGrammarConstructor::isHandledType(TypeNode t)
 }
 
 Node CegGrammarConstructor::createLambdaWithZeroArg(
-    Kind k, TypeNode bArgType, std::shared_ptr<SygusPrintCallback> spc)
+    Kind k, TypeNode bArgType)
 {
   NodeManager* nm = NodeManager::currentNM();
   std::vector<Node> opLArgs;
@@ -513,9 +512,6 @@ Node CegGrammarConstructor::createLambdaWithZeroArg(
     zarg = bv::utils::mkZero(size);
   }
   Node body = nm->mkNode(k, zarg, opLArgs.back());
-  // use a print callback since we do not want to print the lambda
-  spc = std::make_shared<printer::SygusExprPrintCallback>(body.toExpr(),
-                                                          opLArgsExpr);
   // create operator
   Node op = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, opLArgs), body);
   Trace("sygus-grammar-def") << "\t...building lambda op " << op << "\n";
@@ -1137,15 +1133,6 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       {
         Node op =
             nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, opLArgs), monomial);
-        // use a print callback since we do not want to print the lambda
-        std::shared_ptr<SygusPrintCallback> spc;
-        std::vector<Expr> opLArgsExpr;
-        for (unsigned j = 0, nvars = opLArgs.size(); j < nvars; j++)
-        {
-          opLArgsExpr.push_back(opLArgs[j].toExpr());
-        }
-        spc = std::make_shared<printer::SygusExprPrintCallback>(
-            monomial.toExpr(), opLArgsExpr);
         // add it as a constructor
         std::stringstream ssop;
         ssop << "monomial_" << sdc.d_name;
@@ -1153,7 +1140,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
         // a generalization of a non-Boolean variable (which has weight 0).
         // This ensures that e.g. ( c1*x >= 0 ) has the same weight as
         // ( x >= 0 ).
-        sdts[iat].d_sdt.addConstructor(op, ssop.str(), opCArgs, spc, 0);
+        sdts[iat].d_sdt.addConstructor(op, ssop.str(), opCArgs, 0);
       }
     }
     if (polynomialGrammar)
@@ -1167,14 +1154,6 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       Assert(sumChildren.size() > 1);
       Node ops = nm->mkNode(PLUS, sumChildren);
       Node op = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, lambdaVars), ops);
-      std::shared_ptr<SygusPrintCallback> spc;
-      std::vector<Expr> lambdaVarsExpr;
-      for (unsigned j = 0, nvars = lambdaVars.size(); j < nvars; j++)
-      {
-        lambdaVarsExpr.push_back(lambdaVars[j].toExpr());
-      }
-      spc = std::make_shared<printer::SygusExprPrintCallback>(ops.toExpr(),
-                                                              lambdaVarsExpr);
       Trace("sygus-grammar-def") << "any term operator is " << op << std::endl;
       // make the any term datatype, add to back
       // do not consider the exclusion criteria of the generator
@@ -1182,7 +1161,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       // a simultaneous generalization of set of non-Boolean variables.
       // This ensures that ( c1*x + c2*y >= 0 ) has the same weight as
       // e.g. ( x >= 0 ) or ( y >= 0 ).
-      sdts[iat].d_sdt.addConstructor(op, "polynomial", cargsAnyTerm, spc, 0);
+      sdts[iat].d_sdt.addConstructor(op, "polynomial", cargsAnyTerm, 0);
       // mark that predicates should be of the form (= pol 0) and (<= pol 0)
       itgat->second.second = true;
     }
@@ -1223,7 +1202,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       Trace("sygus-grammar-def") << "...add for variable " << ss.str() << std::endl;
       std::vector<TypeNode> cargsEmpty;
       // make boolean variables weight as non-nullary constructors
-      sdtBool.addConstructor(sygus_vars[i], ss.str(), cargsEmpty, nullptr, 1);
+      sdtBool.addConstructor(sygus_vars[i], ss.str(), cargsEmpty, 1);
     }
   }
   // add constants
@@ -1270,8 +1249,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     // predicates
     if (zarg)
     {
-      std::shared_ptr<SygusPrintCallback> spc;
-      Node op = createLambdaWithZeroArg(k, types[i], spc);
+      Node op = createLambdaWithZeroArg(k, types[i]);
       ss << "eq_" << types[i];
       sdtBool.addConstructor(op, ss.str(), cargs);
     }
@@ -1283,7 +1261,6 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       cargs.pop_back();
     }
     // type specific predicates
-    std::shared_ptr<SygusPrintCallback> spc;
     std::stringstream ssop;
     if (types[i].isReal())
     {
@@ -1291,7 +1268,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       Trace("sygus-grammar-def") << "...add for " << k << std::endl;
       if (zarg)
       {
-        Node op = createLambdaWithZeroArg(kind, types[i], spc);
+        Node op = createLambdaWithZeroArg(kind, types[i]);
         ssop << "leq_" << types[i];
         sdtBool.addConstructor(op, ssop.str(), cargs);
       }
@@ -1307,7 +1284,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       Trace("sygus-grammar-def") << "...add for " << k << std::endl;
       if (zarg)
       {
-        Node op = createLambdaWithZeroArg(kind, types[i], spc);
+        Node op = createLambdaWithZeroArg(kind, types[i]);
         ssop << "leq_" << types[i];
         sdtBool.addConstructor(op, ssop.str(), cargs);
       }
@@ -1522,22 +1499,20 @@ void CegGrammarConstructor::SygusDatatypeGenerator::addConstructor(
     Node op,
     const std::string& name,
     const std::vector<TypeNode>& consTypes,
-    std::shared_ptr<SygusPrintCallback> spc,
     int weight)
 {
   if (shouldInclude(op))
   {
-    d_sdt.addConstructor(op, name, consTypes, spc, weight);
+    d_sdt.addConstructor(op, name, consTypes, weight);
   }
 }
 void CegGrammarConstructor::SygusDatatypeGenerator::addConstructor(
     Kind k,
     const std::vector<TypeNode>& consTypes,
-    std::shared_ptr<SygusPrintCallback> spc,
     int weight)
 {
   NodeManager* nm = NodeManager::currentNM();
-  addConstructor(nm->operatorOf(k), kindToString(k), consTypes, spc, weight);
+  addConstructor(nm->operatorOf(k), kindToString(k), consTypes, weight);
 }
 bool CegGrammarConstructor::SygusDatatypeGenerator::shouldInclude(Node op) const
 {
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
index b0c575809..fd7f84484 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
@@ -200,7 +200,6 @@ public:
     void addConstructor(Node op,
                         const std::string& name,
                         const std::vector<TypeNode>& consTypes,
-                        std::shared_ptr<SygusPrintCallback> spc = nullptr,
                         int weight = -1);
     /**
      * Possibly add a constructor to d_sdt, based on the criteria mentioned
@@ -208,7 +207,6 @@ public:
      */
     void addConstructor(Kind k,
                         const std::vector<TypeNode>& consTypes,
-                        std::shared_ptr<SygusPrintCallback> spc = nullptr,
                         int weight = -1);
     /** Should we include constructor with operator op? */
     bool shouldInclude(Node op) const;
@@ -260,13 +258,9 @@ public:
    * and an extra zero argument of that same type.  For example, for k = LEQ and
    * bArgType = Int, the operator will be lambda x : Int. x + 0.  Currently the
    * supported input types are Real (thus also Int) and BitVector.
-   *
-   * This method also creates a print callback for the operator, saved via the
-   * argument spc, if the caller wishes to not print the lambda.
    */
   static Node createLambdaWithZeroArg(Kind k,
-                                      TypeNode bArgType,
-                                      std::shared_ptr<SygusPrintCallback> spc);
+                                      TypeNode bArgType);
   //---------------- end grammar construction
 };
 
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index 819dd6de9..939256b2b 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -18,7 +18,6 @@
 #include "expr/datatype.h"
 #include "expr/node_manager_attributes.h"  // for VarNameAttr
 #include "options/quantifiers_options.h"
-#include "printer/sygus_print_callback.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
@@ -84,8 +83,7 @@ SygusGrammarNorm::TypeObject::TypeObject(TypeNode src_tn, TypeNode unres_tn)
 
 void SygusGrammarNorm::TypeObject::addConsInfo(
     SygusGrammarNorm* sygus_norm,
-    const DTypeConstructor& cons,
-    std::shared_ptr<SygusPrintCallback> spc)
+    const DTypeConstructor& cons)
 {
   Trace("sygus-grammar-normalize") << "...for " << cons.getName() << "\n";
   /* Recover the sygus operator to not lose reference to the original
@@ -107,7 +105,7 @@ void SygusGrammarNorm::TypeObject::addConsInfo(
   }
 
   d_sdt.addConstructor(
-      sygus_op, cons.getName(), consTypes, spc, cons.getWeight());
+      sygus_op, cons.getName(), consTypes, cons.getWeight());
 }
 
 void SygusGrammarNorm::TypeObject::initializeDatatype(
@@ -225,7 +223,6 @@ void SygusGrammarNorm::TransfChain::buildType(SygusGrammarNorm* sygus_norm,
     to.d_sdt.addConstructor(iden_op,
                             "id",
                             ctypes,
-                            printer::SygusEmptyPrintCallback::getEmptyPC(),
                             0);
     Trace("sygus-grammar-normalize-chain")
         << "\tAdding  " << t << " to " << to.d_unres_tn << "\n";
@@ -267,7 +264,6 @@ void SygusGrammarNorm::TransfChain::buildType(SygusGrammarNorm* sygus_norm,
   to.d_sdt.addConstructor(iden_op,
                           "id_next",
                           ctypes,
-                          printer::SygusEmptyPrintCallback::getEmptyPC(),
                           0);
 }
 
@@ -472,7 +468,7 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn,
   {
     unsigned oi = op_pos[i];
     Assert(oi < dt.getNumConstructors());
-    to.addConsInfo(this, dt[oi], dtt[oi].getSygusPrintCallback());
+    to.addConsInfo(this, dt[oi]);
   }
   /* Build normalize datatype */
   if (Trace.isOn("sygus-grammar-normalize"))
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
index 7b635884b..5994d0e7d 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
@@ -198,8 +198,7 @@ class SygusGrammarNorm
      * The types of the arguments of "cons" are recursively normalized
      */
     void addConsInfo(SygusGrammarNorm* sygus_norm,
-                     const DTypeConstructor& cons,
-                     std::shared_ptr<SygusPrintCallback> spc);
+                     const DTypeConstructor& cons);
 
     /** initializes a datatype with the information in the type object
      *
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp
index 77b193a75..42572a0c7 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.cpp
+++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp
@@ -21,7 +21,6 @@
 #include "expr/node_algorithm.h"
 #include "expr/sygus_datatype.h"
 #include "options/smt_options.h"
-#include "printer/sygus_print_callback.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index cff8f581d..3e632fc56 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -129,11 +129,10 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
   if (Trace.isOn("sygus-repair-const"))
   {
     Trace("sygus-repair-const") << "Repair candidate solutions..." << std::endl;
-    Printer* p = Printer::getPrinter(options::outputLanguage());
     for (unsigned i = 0, size = candidates.size(); i < size; i++)
     {
       std::stringstream ss;
-      p->toStreamSygus(ss, candidate_values[i]);
+      TermDbSygus::toStreamSygus(ss, candidate_values[i]);
       Trace("sygus-repair-const")
           << "  " << candidates[i] << " -> " << ss.str() << std::endl;
     }
@@ -151,9 +150,8 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
         cv, free_var_count, sk_vars, sk_vars_to_subs, useConstantsAsHoles);
     if (Trace.isOn("sygus-repair-const"))
     {
-      Printer* p = Printer::getPrinter(options::outputLanguage());
       std::stringstream ss;
-      p->toStreamSygus(ss, cv);
+      TermDbSygus::toStreamSygus(ss, cv);
       Trace("sygus-repair-const")
           << "Solution #" << i << " : " << ss.str() << std::endl;
       if (skeleton == cv)
@@ -163,7 +161,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
       else
       {
         std::stringstream sss;
-        p->toStreamSygus(sss, skeleton);
+        TermDbSygus::toStreamSygus(sss, skeleton);
         Trace("sygus-repair-const")
             << "...inferred skeleton : " << sss.str() << std::endl;
       }
@@ -269,8 +267,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
     if (Trace.isOn("sygus-repair-const") || Trace.isOn("sygus-engine"))
     {
       std::stringstream sss;
-      Printer::getPrinter(options::outputLanguage())
-          ->toStreamSygus(sss, repair_cv[i]);
+      TermDbSygus::toStreamSygus(sss, repair_cv[i]);
       ss << "  * " << candidates[i] << " -> " << sss.str() << std::endl;
     }
   }
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 9fb0702b1..86cb69f48 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -713,8 +713,7 @@ Node SygusUnifRl::DecisionTreeInfo::buildSolMinCond(Node cons,
       if (Trace.isOn("sygus-unif-sol"))
       {
         std::stringstream ss;
-        Printer::getPrinter(options::outputLanguage())
-            ->toStreamSygus(ss, hd_mv[e]);
+        TermDbSygus::toStreamSygus(ss, hd_mv[e]);
         Trace("sygus-unif-sol")
             << "  add evaluation head (" << hd_counter << "/" << d_hds.size()
             << "): " << e << " -> " << ss.str() << std::endl;
@@ -766,7 +765,7 @@ Node SygusUnifRl::DecisionTreeInfo::buildSolMinCond(Node cons,
     if (Trace.isOn("sygus-unif-sol"))
     {
       std::stringstream ss;
-      Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, cv);
+      TermDbSygus::toStreamSygus(ss, cv);
       Trace("sygus-unif-sol")
           << "  add condition (" << c_counter << "/" << d_conds.size()
           << "): " << ce << " -> " << ss.str() << std::endl;
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 6ade49b6d..9608de743 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -373,7 +373,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
         for (const Node& fc : fail_cvs)
         {
           std::stringstream ss;
-          Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, fc);
+          TermDbSygus::toStreamSygus(ss, fc);
           Trace("sygus-engine") << ss.str() << " ";
         }
         Trace("sygus-engine") << std::endl;
@@ -434,7 +434,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
         Node onv = nv.isNull() ? d_qe->getModel()->getValue(terms[i]) : nv;
         TypeNode tn = onv.getType();
         std::stringstream ss;
-        Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, onv);
+        TermDbSygus::toStreamSygus(ss, onv);
         if (printDebug)
         {
           sygusEnumOut << " " << ss.str();
@@ -559,7 +559,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
       {
         Node v = candidate_values[i];
         std::stringstream ss;
-        Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, v);
+        TermDbSygus::toStreamSygus(ss, v);
         out << "(" << d_quant[0][i] << " " << ss.str() << ")";
       }
       out << ")" << std::endl;
@@ -1193,8 +1193,8 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
         }
         else
         {
-          Printer::getPrinter(options::outputLanguage())
-              ->toStreamSygus(out, sol);
+          Node bsol = datatypes::utils::sygusToBuiltin(sol, true);
+          out << bsol;
         }
         out << ")" << std::endl;
       }
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index ac1c7d342..c2a02e715 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -723,19 +723,18 @@ void TermDbSygus::toStreamSygus(const char* c, Node n)
 {
   if (Trace.isOn(c))
   {
-    if (n.isNull())
-    {
-      Trace(c) << n;
-    }
-    else
-    {
-      std::stringstream ss;
-      Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, n);
-      Trace(c) << ss.str();
-    }
+    std::stringstream ss;
+    toStreamSygus(ss, n);
+    Trace(c) << ss.str();
   }
 }
 
+void TermDbSygus::toStreamSygus(std::ostream& out, Node n)
+{
+  // use external conversion
+  out << datatypes::utils::sygusToBuiltin(n, true);
+}
+
 SygusTypeInfo& TermDbSygus::getTypeInfo(TypeNode tn)
 {
   AlwaysAssert(d_tinfo.find(tn) != d_tinfo.end());
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 97cdc6ddd..921b08de5 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -310,7 +310,9 @@ class TermDbSygus {
 
   /** print to sygus stream n on trace c */
   static void toStreamSygus(const char* c, Node n);
-
+  /** print to sygus stream n on output out */
+  static void toStreamSygus(std::ostream& out, Node n);
+  
  private:
   /** reference to the quantifiers engine */
   QuantifiersEngine* d_quantEngine;