From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 22 Nov 2017 20:25:59 +0000 (-0600)
Subject: Sygus Lambda Grammars (#1390)
X-Git-Tag: cvc5-1.0.0~5458
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=20704741e4609055d61e010b6981c6916d28019a;p=cvc5.git

Sygus Lambda Grammars (#1390)
---

diff --git a/src/Makefile.am b/src/Makefile.am
index dc0a2b62a..b3c4ec98c 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -67,6 +67,8 @@ libcvc4_la_SOURCES = \
 	printer/dagification_visitor.h \
 	printer/printer.cpp \
 	printer/printer.h \
+	printer/sygus_print_callback.cpp \
+	printer/sygus_print_callback.h \
 	printer/ast/ast_printer.cpp \
 	printer/ast/ast_printer.h \
 	printer/cvc/cvc_printer.cpp \
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index f654f2608..513cb2170 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -181,25 +181,18 @@ void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){
   d_sygus_allow_all = allow_all;
 }
 
-void Datatype::addSygusConstructor( CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs,
-                                    CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args ) {
+void Datatype::addSygusConstructor(CVC4::Expr op,
+                                   std::string& cname,
+                                   std::vector<CVC4::Type>& cargs,
+                                   std::shared_ptr<SygusPrintCallback> spc)
+{
   Debug("dt-sygus") << "--> Add constructor " << cname << " to " << getName() << std::endl;
-  if( !let_body.isNull() ){
-    Debug("dt-sygus") << "    let body = " << let_body << ", args = " << let_args.size() << "," << let_num_input_args << std::endl;
-    //TODO : remove arguments not occurring in body
-    //if this is a self identity function, ignore
-    if( let_args.size()==0 && let_args[0]==let_body ){
-      Debug("dt-sygus") << "    identity function " << cargs[0] << " to " << getName() << std::endl;
-      //TODO
-    }
-  }
+  Debug("dt-sygus") << "    sygus op : " << op << std::endl;
   std::string name = getName() + "_" + cname;
   std::string testerId("is-");
   testerId.append(name);
-  //checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
-  //checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
   CVC4::DatatypeConstructor c(name, testerId );
-  c.setSygus( op, let_body, let_args, let_num_input_args );
+  c.setSygus(op, spc);
   for( unsigned j=0; j<cargs.size(); j++ ){
     Debug("parser-sygus-debug") << "  arg " << j << " : " << cargs[j] << std::endl;
     std::stringstream sname;
@@ -208,13 +201,6 @@ void Datatype::addSygusConstructor( CVC4::Expr op, std::string& cname, std::vect
   }
   addConstructor(c);
 }
-
-void Datatype::addSygusConstructor( CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs ) {
-  CVC4::Expr let_body; 
-  std::vector< CVC4::Expr > let_args; 
-  unsigned let_num_input_args = 0;
-  addSygusConstructor( op, cname, cargs, let_body, let_args, let_num_input_args );
-}
                                     
 void Datatype::setTuple() {
   PrettyCheckArgument(!d_resolved, this, "cannot set tuple to a finalized Datatype");
@@ -784,7 +770,8 @@ DatatypeConstructor::DatatypeConstructor(std::string name)
       d_name(name + '\0' + "is_" + name),  // default tester name is "is_FOO"
       d_tester(),
       d_args(),
-      d_sygus_num_let_input_args(0) {
+      d_sygus_pc(nullptr)
+{
   PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
 }
 
@@ -796,16 +783,19 @@ DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester)
       d_name(name + '\0' + tester),
       d_tester(),
       d_args(),
-      d_sygus_num_let_input_args(0) {
+      d_sygus_pc(nullptr)
+{
   PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
   PrettyCheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
 }
 
-void DatatypeConstructor::setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_args ){
+void DatatypeConstructor::setSygus(Expr op,
+                                   std::shared_ptr<SygusPrintCallback> spc)
+{
+  PrettyCheckArgument(
+      !isResolved(), this, "cannot modify a finalized Datatype constructor");
   d_sygus_op = op;
-  d_sygus_let_body = let_body;
-  d_sygus_let_args.insert( d_sygus_let_args.end(), let_args.begin(), let_args.end() );
-  d_sygus_num_let_input_args = num_let_input_args;
+  d_sygus_pc = spc;
 }
 
 void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
@@ -882,37 +872,18 @@ Expr DatatypeConstructor::getSygusOp() const {
   return d_sygus_op;
 }
 
-Expr DatatypeConstructor::getSygusLetBody() const {
-  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-  return d_sygus_let_body;
-}
-
-unsigned DatatypeConstructor::getNumSygusLetArgs() const {
-  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-  return d_sygus_let_args.size();
-}
-
-Expr DatatypeConstructor::getSygusLetArg( unsigned i ) const {
-  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-  return d_sygus_let_args[i];
-}
-
-unsigned DatatypeConstructor::getNumSygusLetInputArgs() const {
-  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-  return d_sygus_num_let_input_args;
-}
-
 bool DatatypeConstructor::isSygusIdFunc() const {
   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-  return d_sygus_let_args.size()==1 && d_sygus_let_args[0]==d_sygus_let_body;
+  return (d_sygus_op.getKind() == kind::LAMBDA
+          && d_sygus_op[0].getNumChildren() == 1
+          && d_sygus_op[0][0] == d_sygus_op[1]);
 }
 
 SygusPrintCallback* DatatypeConstructor::getSygusPrintCallback() const
 {
   PrettyCheckArgument(
       isResolved(), this, "this datatype constructor is not yet resolved");
-  // TODO  (#1344) return the stored callback
-  return nullptr;
+  return d_sygus_pc.get();
 }
 
 Cardinality DatatypeConstructor::getCardinality( Type t ) const throw(IllegalArgumentException) {
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index a92a0738e..85ecfb946 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -191,7 +191,7 @@ class CVC4_PUBLIC SygusPrintCallback
 {
  public:
   SygusPrintCallback() {}
-  ~SygusPrintCallback() {}
+  virtual ~SygusPrintCallback() {}
   /**
    * Writes the term that sygus datatype expression e
    * encodes to stream out. p is the printer that
@@ -232,6 +232,7 @@ class CVC4_PUBLIC DatatypeConstructor {
    */
   DatatypeConstructor(std::string name, std::string tester);
 
+  ~DatatypeConstructor() {}
   /**
    * Add an argument (i.e., a data field) of the given name and type
    * to this Datatype constructor.  Selector names need not be unique;
@@ -287,29 +288,10 @@ class CVC4_PUBLIC DatatypeConstructor {
    * deep embedding.
    */
   Expr getSygusOp() const;
-  /** get sygus let body
-   *
-   * The sygus official format
-   * (http://www.sygus.org/SyGuS-COMP2015.html)
-   * allows for let expressions to occur in grammars.
-   *
-   * TODO (#1344) refactor this
-   */
-  Expr getSygusLetBody() const;
-  /** get number of sygus let args
-   * TODO (#1344) refactor this
-   */
-  unsigned getNumSygusLetArgs() const;
-  /** get sygus let arg
-   * TODO (#1344) refactor this
-   */
-  Expr getSygusLetArg( unsigned i ) const;
-  /** get number of let arguments that should be printed as arguments to let
-   * TODO (#1344) refactor this
-   */
-  unsigned getNumSygusLetInputArgs() const;
   /** is this a sygus identity function?
-   * TODO (#1344) refactor this
+   *
+   * This returns true if the sygus operator of this datatype constructor is
+   * of the form (lambda (x) x).
    */
   bool isSygusIdFunc() const;
   /** get sygus print callback
@@ -431,11 +413,13 @@ class CVC4_PUBLIC DatatypeConstructor {
   int getSelectorIndexInternal( Expr sel ) const;
 
   /** involves external type
+   *
    * Get whether this constructor has a subfield
    * in any constructor that is not a datatype type.
    */
   bool involvesExternalType() const;
   /** involves external type
+   *
    * Get whether this constructor has a subfield
    * in any constructor that is an uninterpreted type.
    */
@@ -443,13 +427,11 @@ class CVC4_PUBLIC DatatypeConstructor {
 
   /** set sygus
    *
-   * Set that this constructor is a sygus datatype
-   * constructor that encodes operator op.
-   * The remaining arguments are for handling
-   * let expressions in user-provided sygus
-   * grammars (see above).
+   * Set that this constructor is a sygus datatype constructor that encodes
+   * operator op. spc is the sygus callback of this datatype constructor,
+   * which is stored in a shared pointer.
    */
-  void setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_argus );
+  void setSygus(Expr op, std::shared_ptr<SygusPrintCallback> spc);
 
  private:
   /** the name of the constructor */
@@ -462,14 +444,11 @@ class CVC4_PUBLIC DatatypeConstructor {
   std::vector<DatatypeConstructorArg> d_args;
   /** sygus operator */
   Expr d_sygus_op;
-  /** sygus let body */
-  Expr d_sygus_let_body;
-  /** sygus let args */
-  std::vector<Expr> d_sygus_let_args;
-  /** sygus num let input args */
-  unsigned d_sygus_num_let_input_args;
+  /** sygus print callback */
+  std::shared_ptr<SygusPrintCallback> d_sygus_pc;
 
   /** shared selectors for each type
+   *
    * This stores the shared (constructor-agnotic)
    * selectors that access the fields of this datatype.
    * In the terminology of "Datatypes with Shared Selectors",
@@ -673,25 +652,18 @@ public:
    *      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
    * with op = PLUS should be such that cargs.size()>=2 and
    * the sygus type of cargs[i] is Real/Int for each i.
    */
-  void addSygusConstructor( CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs );
-  /** add sygus constructor (for let expression constructors)
-   *
-   * This adds a sygus constructor to this datatype, where
-   * this datatype should be currently unresolved.
-   *
-   * In contrast to the above function, the constructor we
-   * add corresponds to a let expression if let_body is
-   * non-null. For details, see documentation for
-   * DatatypeConstructor::getSygusLetBody above.
-   */
-  void addSygusConstructor( CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs,
-                            CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args );
+  void addSygusConstructor(CVC4::Expr op,
+                           std::string& cname,
+                           std::vector<CVC4::Type>& cargs,
+                           std::shared_ptr<SygusPrintCallback> spc = nullptr);
 
   /** set that this datatype is a tuple */
   void setTuple();
diff --git a/src/options/smt_options b/src/options/smt_options
index c701d5c20..fa6c3ae4e 100644
--- a/src/options/smt_options
+++ b/src/options/smt_options
@@ -40,7 +40,9 @@ option dumpProofs --dump-proofs bool :default false :link --proof :link-smt prod
 option dumpInstantiations --dump-instantiations bool :default false
  output instantiations of quantified formulas after every UNSAT/VALID response
 option sygusOut --sygus-out=MODE SygusSolutionOutMode :default SYGUS_SOL_OUT_STATUS_AND_DEF :include "options/sygus_out_mode.h" :handler stringToSygusSolutionOutMode :read-write
-  output mode for sygus
+ output mode for sygus
+option sygusPrintCallbacks --sygus-print-callbacks bool :default true
+ use sygus print callbacks to print sygus terms in the user-provided form (disable for debugging)
 option dumpSynth --dump-synth bool :read-write :default false
  output solution for synthesis conjectures after every UNSAT/VALID response
 option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate proofEnabledBuild :notify :notify notifyBeforeSearch
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index a72b0ac6e..7a681f327 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -21,6 +21,7 @@
 #include "parser/parser.h"
 #include "parser/smt1/smt1.h"
 #include "parser/smt2/smt2_input.h"
+#include "printer/sygus_print_callback.h"
 #include "smt/command.h"
 #include "util/bitvector.h"
 
@@ -926,23 +927,15 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
                             std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ) {
   Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl;
   Debug("parser-sygus") << "  add constructors..." << std::endl;
-  std::vector<std::string> df_name; 
-  std::vector<CVC4::Expr> df_op;
-  std::vector< std::vector<Expr> > df_let_args;
-  std::vector< Expr > df_let_body;
-  //dt.mkSygusConstructors( ops, cnames, cargs, sygus_to_builtin, 
-  //                        d_sygus_let_func_to_vars, d_sygus_let_func_to_body, d_sygus_let_func_to_num_input_vars, 
-  //                        df_name, df_op, df_let_args, df_let_body );
   
   Debug("parser-sygus") << "SMT2 sygus parser : Making constructors for sygus datatype " << dt.getName() << std::endl;
   Debug("parser-sygus") << "  add constructors..." << std::endl;
-  for( int i=0; i<(int)cnames.size(); i++ ){
+  for (unsigned i = 0, size = cnames.size(); i < size; i++)
+  {
     bool is_dup = false;
     bool is_dup_op = false;
-    Expr let_body;
-    std::vector< Expr > let_args;
-    unsigned let_num_input_args = 0;
-    for( int j=0; j<i; j++ ){
+    for (unsigned j = 0; j < i; j++)
+    {
       if( ops[i]==ops[j] ){
         is_dup_op = true;
         if( cargs[i].size()==cargs[j].size() ){
@@ -959,60 +952,122 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
         }
       }
     }
+    Debug("parser-sygus") << "SYGUS CONS " << i << " : ";
     if( is_dup ){
-      Debug("parser-sygus") << "--> Duplicate gterm : " << ops[i] << " at " << i << std::endl;
+      Debug("parser-sygus") << "--> Duplicate gterm : " << ops[i] << std::endl;
       ops.erase( ops.begin() + i, ops.begin() + i + 1 );
       cnames.erase( cnames.begin() + i, cnames.begin() + i + 1 );
       cargs.erase( cargs.begin() + i, cargs.begin() + i + 1 );
       i--;
-    }else if( is_dup_op ){
-      Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops[i] << " at " << i << std::endl;
-      //make into define-fun
-      std::vector<CVC4::Type> fsorts;
-      for( unsigned j=0; j<cargs[i].size(); j++ ){
-        Type bt = sygus_to_builtin[cargs[i][j]];
-        std::stringstream ss;
-        ss << dt.getName() << "_x_" << i << "_" << j;
-        Expr v = mkBoundVar(ss.str(), bt);
-        let_args.push_back( v );
-        fsorts.push_back( bt );
-        Debug("parser-sygus") << ": var " << i << " " << v << " with type " << bt << " from " << cargs[i][j] << std::endl;
+    }
+    else
+    {
+      std::shared_ptr<SygusPrintCallback> spc;
+      if (is_dup_op)
+      {
+        Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops[i]
+                              << std::endl;
+        // make into define-fun
+        std::vector<Type> ltypes;
+        for (unsigned j = 0, size = cargs[i].size(); j < size; j++)
+        {
+          ltypes.push_back(sygus_to_builtin[cargs[i][j]]);
+        }
+        std::vector<Expr> largs;
+        Expr lbvl = makeSygusBoundVarList(dt, i, ltypes, largs);
+
+        // make the let_body
+        std::vector<Expr> children;
+        if (ops[i].getKind() != kind::BUILTIN)
+        {
+          children.push_back(ops[i]);
+        }
+        children.insert(children.end(), largs.begin(), largs.end());
+        Kind sk = ops[i].getKind() != kind::BUILTIN
+                      ? kind::APPLY
+                      : getExprManager()->operatorToKind(ops[i]);
+        Expr body = getExprManager()->mkExpr(sk, children);
+        // replace by lambda
+        ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body);
+        Debug("parser-sygus") << "  ...replace op : " << ops[i] << std::endl;
+        // callback prints as the expression
+        spc = std::make_shared<printer::SygusExprPrintCallback>(body, largs);
       }
-      //make the let_body
-      std::vector< Expr > children;
-      if( ops[i].getKind() != kind::BUILTIN ){
-        children.push_back( ops[i] );
+      else
+      {
+        std::map<Expr, Expr>::iterator it =
+            d_sygus_let_func_to_body.find(ops[i]);
+        if (it != d_sygus_let_func_to_body.end())
+        {
+          Debug("parser-sygus") << "--> Let expression " << ops[i] << std::endl;
+          Expr let_body = it->second;
+          std::vector<Expr> let_args = d_sygus_let_func_to_vars[ops[i]];
+          unsigned let_num_input_args =
+              d_sygus_let_func_to_num_input_vars[ops[i]];
+          // the operator is just the body for the arguments
+          std::vector<Type> ltypes;
+          for (unsigned j = 0, size = let_args.size(); j < size; j++)
+          {
+            ltypes.push_back(let_args[j].getType());
+          }
+          std::vector<Expr> largs;
+          Expr lbvl = makeSygusBoundVarList(dt, i, ltypes, largs);
+          Expr sbody = let_body.substitute(let_args, largs);
+          ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, sbody);
+          Debug("parser-sygus") << "  ...replace op : " << ops[i] << std::endl;
+          // callback prints as a let expression
+          spc = std::make_shared<printer::SygusLetExprPrintCallback>(
+              let_body, let_args, let_num_input_args);
+        }
+        else if (ops[i].getType().isBitVector() && ops[i].isConst())
+        {
+          Debug("parser-sygus") << "--> Bit-vector constant " << ops[i] << " ("
+                                << cnames[i] << ")" << std::endl;
+          // Since there are multiple output formats for bit-vectors and
+          // we are required by sygus standards to print in the exact input
+          // format given by the user, we use a print callback to custom print
+          // the given name.
+          spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]);
+        }
+        else if (isDefinedFunction(ops[i]))
+        {
+          Debug("parser-sygus") << "--> Defined function " << ops[i]
+                                << std::endl;
+          // turn f into (lammbda (x) (f x))
+          // in a degenerate case, ops[i] may be a defined constant,
+          // in which case we do not replace by a lambda.
+          if (ops[i].getType().isFunction())
+          {
+            std::vector<Type> ftypes =
+                static_cast<FunctionType>(ops[i].getType()).getArgTypes();
+            std::vector<Expr> largs;
+            Expr lbvl = makeSygusBoundVarList(dt, i, ftypes, largs);
+            largs.insert(largs.begin(), ops[i]);
+            Expr body = getExprManager()->mkExpr(kind::APPLY, largs);
+            ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body);
+            Debug("parser-sygus") << "  ...replace op : " << ops[i]
+                                  << std::endl;
+          }
+          else
+          {
+            ops[i] = getExprManager()->mkExpr(kind::APPLY, ops[i]);
+            Debug("parser-sygus") << "  ...replace op : " << ops[i]
+                                  << std::endl;
+          }
+          // keep a callback to say it should be printed with the defined name
+          spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]);
+        }
+        else
+        {
+          Debug("parser-sygus") << "--> Default case " << ops[i] << std::endl;
+        }
       }
-      children.insert( children.end(), let_args.begin(), let_args.end() );
-      Kind sk = ops[i].getKind() != kind::BUILTIN ? kind::APPLY : getExprManager()->operatorToKind(ops[i]);
-      Debug("parser-sygus") << ": replace " << ops[i] << " " << ops[i].getKind() << " " << sk << std::endl;
-      let_body = getExprManager()->mkExpr( sk, children );
-      Debug("parser-sygus") << ": new body of function is " << let_body << std::endl;
-
-      Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType());
-      Debug("parser-sygus") << ": function type is " << ft << std::endl;
+      // must rename to avoid duplication
       std::stringstream ss;
-      ss << dt.getName() << "_df_" << i;
-      //replace operator and name
-      ops[i] = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
+      ss << dt.getName() << "_" << i << "_" << cnames[i];
       cnames[i] = ss.str();
-      // indicate we need a define function
-      df_name.push_back( ss.str() );
-      df_op.push_back( ops[i] );
-      df_let_args.push_back( let_args );
-      df_let_body.push_back( let_body );
-      
-      //d_sygus_defined_funs.push_back( ops[i] );
-      //preemptCommand( new DefineFunctionCommand(ss.str(), ops[i], let_args, let_body) );
-      dt.addSygusConstructor( ops[i], cnames[i], cargs[i], let_body, let_args, 0 );
-    }else{
-      std::map< CVC4::Expr, CVC4::Expr >::iterator it = d_sygus_let_func_to_body.find( ops[i] );
-      if( it!=d_sygus_let_func_to_body.end() ){
-        let_body = it->second;
-        let_args.insert( let_args.end(), d_sygus_let_func_to_vars[ops[i]].begin(), d_sygus_let_func_to_vars[ops[i]].end() );
-        let_num_input_args = d_sygus_let_func_to_num_input_vars[ops[i]];
-      }
-      dt.addSygusConstructor( ops[i], cnames[i], cargs[i], let_body, let_args, let_num_input_args );
+      // add the sygus constructor
+      dt.addSygusConstructor(ops[i], cnames[i], cargs[i], spc);
     }
   }
 
@@ -1030,28 +1085,25 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
           //identity element
           Type bt = dt.getSygusType();
           Debug("parser-sygus") << ":  make identity function for " << bt << ", argument type " << t << std::endl;
+
           std::stringstream ss;
-          ss << t << "_x_id";
-          Expr let_body = mkBoundVar(ss.str(), bt);
-          std::vector< Expr > let_args;
-          let_args.push_back( let_body );
-          //make the identity function
-          Type ft = getExprManager()->mkFunctionType(bt, bt);
-          std::stringstream ssid;
-          ssid << unresolved_gterm_sym[i] << "_id";
-          Expr id_op = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
-          // indicate we need a define function
-          df_name.push_back( ssid.str() );
-          df_op.push_back( id_op );
-          df_let_args.push_back( let_args );
-          df_let_body.push_back( let_body );
-          
-          //d_sygus_defined_funs.push_back( id_op );
-          //preemptCommand( new DefineFunctionCommand(ssid.str(), id_op, let_args, let_body) );
+          ss << t << "_x";
+          Expr var = mkBoundVar(ss.str(), bt);
+          std::vector<Expr> lchildren;
+          lchildren.push_back(
+              getExprManager()->mkExpr(kind::BOUND_VAR_LIST, var));
+          lchildren.push_back(var);
+          Expr id_op = getExprManager()->mkExpr(kind::LAMBDA, lchildren);
+
+          // empty sygus callback (should not be printed)
+          std::shared_ptr<SygusPrintCallback> sepc =
+              std::make_shared<printer::SygusEmptyPrintCallback>();
+
           //make the sygus argument list
           std::vector< Type > id_carg;
           id_carg.push_back( t );
-          dt.addSygusConstructor( id_op, unresolved_gterm_sym[i], id_carg, let_body, let_args, 0 );
+          dt.addSygusConstructor(id_op, unresolved_gterm_sym[i], id_carg, sepc);
+
           //add to operators
           ops.push_back( id_op );
         }
@@ -1060,12 +1112,21 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
       }
     }
   }
-  
-  
-  for( unsigned i=0; i<df_name.size(); i++ ){
-    d_sygus_defined_funs.push_back( df_op[i] );
-    preemptCommand( new DefineFunctionCommand(df_name[i], df_op[i], df_let_args[i], df_let_body[i]) );
+}
+
+Expr Smt2::makeSygusBoundVarList(Datatype& dt,
+                                 unsigned i,
+                                 const std::vector<Type>& ltypes,
+                                 std::vector<Expr>& lvars)
+{
+  for (unsigned j = 0, size = ltypes.size(); j < size; j++)
+  {
+    std::stringstream ss;
+    ss << dt.getName() << "_x_" << i << "_" << j;
+    Expr v = mkBoundVar(ss.str(), ltypes[j]);
+    lvars.push_back(v);
   }
+  return getExprManager()->mkExpr(kind::BOUND_VAR_LIST, lvars);
 }
 
 const void Smt2::getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed ) {
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 9614c5524..84c049ce9 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -319,6 +319,19 @@ private:
                                    std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
                                    std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr );
 
+  /** make sygus bound var list
+   *
+   * This is used for converting non-builtin sygus operators to lambda
+   * expressions. It takes as input a datatype and constructor index (for
+   * naming) and a vector of type ltypes.
+   * It appends a bound variable to lvars for each type in ltypes, and returns
+   * a bound variable list whose children are lvars.
+   */
+  Expr makeSygusBoundVarList(Datatype& dt,
+                             unsigned i,
+                             const std::vector<Type>& ltypes,
+                             std::vector<Expr>& lvars);
+
   void addArithmeticOperators();
 
   void addBitvectorOperators();
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,
diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp
index e1bc32761..bc6817560 100644
--- a/src/theory/quantifiers/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/ce_guided_conjecture.cpp
@@ -15,7 +15,9 @@
 #include "theory/quantifiers/ce_guided_conjecture.h"
 
 #include "expr/datatype.h"
+#include "options/base_options.h"
 #include "options/quantifiers_options.h"
+#include "printer/printer.h"
 #include "prop/prop_engine.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/quantifiers/first_order_model.h"
@@ -428,8 +430,7 @@ void CegConjecture::getModelValues( std::vector< Node >& n, std::vector< Node >&
       TypeNode tn = nv.getType();
       Trace("cegqi-engine") << n[i] << " -> ";
       std::stringstream ss;
-      std::vector< Node > lvs;
-      TermDbSygus::printSygusTerm( ss, nv, lvs );
+      Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, nv);
       Trace("cegqi-engine") << ss.str() << " ";
     }
     Assert( !nv.isNull() );
@@ -621,8 +622,7 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
       if( status==0 ){
         out << sol;
       }else{
-        std::vector< Node > lvs;
-        TermDbSygus::printSygusTerm( out, sol, lvs );
+        Printer::getPrinter(options::outputLanguage())->toStreamSygus(out, sol);
       }
       out << ")" << std::endl;
     }
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 03026069f..b2b4fe18c 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -143,22 +143,12 @@ void CegConjectureSingleInv::initialize( Node q ) {
       d_sip->debugPrint( "cegqi-si" );
 
       //map from program to bound variables
-      std::vector< Node > order_vars;
-      std::map< Node, Node > single_inv_app_map;
-      for( unsigned j=0; j<progs.size(); j++ ){
-        Node prog = progs[j];
-        Node pv = d_sip->getFirstOrderVariableForFunction(prog);
-        if (!pv.isNull())
-        {
-          Node inv = d_sip->getFunctionInvocationFor(prog);
-          Assert(!inv.isNull());
-          single_inv_app_map[prog] = inv;
-          Trace("cegqi-si") << "  " << pv << ", " << inv << " is associated with program " << prog << std::endl;
-          d_prog_to_sol_index[prog] = order_vars.size();
-          order_vars.push_back( pv );
-        }else{
-          Trace("cegqi-si") << "  " << prog << " has no fo var." << std::endl;
-        }
+      std::vector<Node> funcs;
+      d_sip->getFunctions(funcs);
+      for (unsigned j = 0, size = funcs.size(); j < size; j++)
+      {
+        Assert(std::find(progs.begin(), progs.end(), funcs[j]) != progs.end());
+        d_prog_to_sol_index[funcs[j]] = j;
       }
 
       //check if it is single invocation
@@ -180,7 +170,8 @@ void CegConjectureSingleInv::initialize( Node q ) {
             Trace("cegqi-inv") << "  postcondition : " << d_trans_post[prog] << std::endl;
             std::vector<Node> sivars;
             d_sip->getSingleInvocationVariables(sivars);
-            Node invariant = single_inv_app_map[prog];
+            Node invariant = d_sip->getFunctionInvocationFor(prog);
+            Assert(!invariant.isNull());
             invariant = invariant.substitute(sivars.begin(),
                                              sivars.end(),
                                              prog_templ_vars.begin(),
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index b618fc5d5..9a18d13fb 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -55,6 +55,17 @@ typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute;
 struct SynthesisAttributeId {};
 typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute;
 
+/** Attribute for setting printing information for sygus variables
+ *
+ * For variable d of sygus datatype type, if
+ * d.getAttribute(SygusPrintProxyAttribute) = t, then printing d will print t.
+ */
+struct SygusPrintProxyAttributeId
+{
+};
+typedef expr::Attribute<SygusPrintProxyAttributeId, Node>
+    SygusPrintProxyAttribute;
+
 namespace quantifiers {
 
 /** Attribute priority for rewrite rules */
diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp
index e212e0dfb..8625d9089 100644
--- a/src/theory/quantifiers/term_database_sygus.cpp
+++ b/src/theory/quantifiers/term_database_sygus.cpp
@@ -21,6 +21,7 @@
 #include "smt/smt_engine.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/ce_guided_conjecture.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers/theory_quantifiers.h"
@@ -277,13 +278,6 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int
       ret = children[0];
     }else{
       ret = NodeManager::currentNM()->mkNode( ok, children );
-      /*
-      Node n = NodeManager::currentNM()->mkNode( APPLY, children );
-      //must expand definitions
-      Node ne = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( n.toExpr() ) );
-      Trace("sygus-db-debug") << "Expanded definitions in " << n << " to " << ne << std::endl;
-      return ne;
-      */
     }
   }
   Trace("sygus-db-debug") << "...returning " << ret << std::endl;
@@ -345,13 +339,12 @@ Node TermDbSygus::builtinToSygusConst( Node c, TypeNode tn, int rcons_depth ) {
     // if we are not interested in reconstructing constants, or the grammar allows them, return a proxy
     if( !options::cegqiSingleInvReconstructConst() || dt.getSygusAllowConst() ){
       Node k = NodeManager::currentNM()->mkSkolem( "sy", tn, "sygus proxy" );
-      SygusProxyAttribute spa;
+      SygusPrintProxyAttribute spa;
       k.setAttribute(spa,c);
       sc = k;
     }else{
       int carg = getOpConsNum( tn, c );
       if( carg!=-1 ){
-        //sc = Node::fromExpr( dt[carg].getSygusOp() );
         sc = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, Node::fromExpr( dt[carg].getConstructor() ) );
       }else{
         //identity functions
@@ -1545,110 +1538,28 @@ void doStrReplace(std::string& str, const std::string& oldStr, const std::string
 
 Kind TermDbSygus::getOperatorKind( Node op ) {
   Assert( op.getKind()!=BUILTIN );
-  if( smt::currentSmtEngine()->isDefinedFunction( op.toExpr() ) ){
+  Assert(!smt::currentSmtEngine()->isDefinedFunction(op.toExpr()));
+  if (op.getKind() == LAMBDA)
+  {
     return APPLY;
   }else{
     TypeNode tn = op.getType();
     if( tn.isConstructor() ){
       return APPLY_CONSTRUCTOR;
-    }else if( tn.isSelector() ){
+    }
+    else if (tn.isSelector())
+    {
       return APPLY_SELECTOR;
-    }else if( tn.isTester() ){
+    }
+    else if (tn.isTester())
+    {
       return APPLY_TESTER;
-    }else{
-      return NodeManager::operatorToKind( op );
     }
-  }
-}
-
-void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs ) {
-  if( n.getKind()==APPLY_CONSTRUCTOR ){
-    TypeNode tn = n.getType();
-    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-    if( dt.isSygus() ){
-      int cIndex = Datatype::indexOf( n.getOperator().toExpr() );
-      Assert( !dt[cIndex].getSygusOp().isNull() );
-      if( dt[cIndex].getSygusLetBody().isNull() ){
-        if( n.getNumChildren()>0 ){
-          out << "(";
-        }
-        Node op = dt[cIndex].getSygusOp();
-        if( op.getType().isBitVector() && op.isConst() ){
-          //print in the style it was given
-          Trace("sygus-print-bvc") << "[Print " << op << " " << dt[cIndex].getName() << "]" << std::endl;
-          std::stringstream ss;
-          ss << dt[cIndex].getName();
-          std::string str = ss.str();
-          std::size_t found = str.find_last_of("_");
-          Assert( found!=std::string::npos );
-          std::string name = std::string( str.begin() + found +1, str.end() );
-          out << name;
-        }else{
-          out << op;
-        }
-        if( n.getNumChildren()>0 ){
-          for( unsigned i=0; i<n.getNumChildren(); i++ ){
-            out << " ";
-            printSygusTerm( out, n[i], lvs );
-          }
-          out << ")";
-        }
-      }else{
-        std::stringstream let_out;
-        //print as let term
-        if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
-          let_out << "(let (";
-        }
-        std::vector< Node > subs_lvs;
-        std::vector< Node > new_lvs;
-        for( unsigned i=0; i<dt[cIndex].getNumSygusLetArgs(); i++ ){
-          Node v = Node::fromExpr( dt[cIndex].getSygusLetArg( 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<dt[cIndex].getNumSygusLetInputArgs() ){
-            //it should be printed as a let argument
-            let_out << "(";
-            let_out << lv << " " << lv.getType() << " ";
-            printSygusTerm( let_out, n[i], lvs );
-            let_out << ")";
-          }
-        }
-        if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
-          let_out << ") ";
-        }
-        //print the body
-        Node let_body = Node::fromExpr( dt[cIndex].getSygusLetBody() );
-        let_body = 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() );
-        printSygusTerm( let_out, let_body, new_lvs );
-        if( dt[cIndex].getNumSygusLetInputArgs()>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<dt[cIndex].getNumSygusLetArgs(); i++ ){
-          std::stringstream old_str;
-          old_str << new_lvs[i];
-          std::stringstream new_str;
-          if( i>=dt[cIndex].getNumSygusLetInputArgs() ){
-            printSygusTerm( new_str, n[i], lvs );
-          }else{
-            new_str << Node::fromExpr( dt[cIndex].getSygusLetArg( i ) );
-          }
-          doStrReplace( lbody, old_str.str().c_str(), new_str.str().c_str() );
-        }
-        out << lbody;
-      }
-      return;
+    else if (tn.isFunction())
+    {
+      return APPLY_UF;
     }
-  }else if( !n.getAttribute(SygusProxyAttribute()).isNull() ){
-    out << n.getAttribute(SygusProxyAttribute());
-  }else{
-    out << n;
+    return NodeManager::operatorToKind(op);
   }
 }
 
diff --git a/src/theory/quantifiers/term_database_sygus.h b/src/theory/quantifiers/term_database_sygus.h
index 5ff1612c9..45851c0c8 100644
--- a/src/theory/quantifiers/term_database_sygus.h
+++ b/src/theory/quantifiers/term_database_sygus.h
@@ -198,8 +198,6 @@ public:
   
   /** get operator kind */
   static Kind getOperatorKind( Node op );
-  /** print sygus term */
-  static void printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs );
 
   /** get anchor */
   static Node getAnchor( Node n );
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index d2a8a14f0..5ac21dafb 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -62,10 +62,6 @@ typedef expr::Attribute<RrPriorityAttributeId, uint64_t> RrPriorityAttribute;
 struct LtePartialInstAttributeId {};
 typedef expr::Attribute< LtePartialInstAttributeId, bool > LtePartialInstAttribute;
 
-// attribute for sygus proxy variables
-struct SygusProxyAttributeId {};
-typedef expr::Attribute<SygusProxyAttributeId, Node> SygusProxyAttribute;
-
 // attribute for associating a synthesis function with a first order variable
 struct SygusSynthGrammarAttributeId {};
 typedef expr::Attribute<SygusSynthGrammarAttributeId, Node>