Builtin evaluation functions for sygus (#1991)

28 files changed, 837 insertions, 419 deletions

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index d697a6aaf..f19955d19 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -77,6 +77,11 @@ size_t Datatype::indexOf(Expr item) {
                 item.getType().isSelector(),
                 item,
                 "arg must be a datatype constructor, selector, or tester");
+  return indexOfInternal(item);
+}
+
+size_t Datatype::indexOfInternal(Expr item)
+{
   TNode n = Node::fromExpr(item);
   if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){
     return indexOf( item[0] );
@@ -91,6 +96,10 @@ size_t Datatype::cindexOf(Expr item) {
   PrettyCheckArgument(item.getType().isSelector(),
                 item,
                 "arg must be a datatype selector");
+  return cindexOfInternal(item);
+}
+size_t Datatype::cindexOfInternal(Expr item)
+{
   TNode n = Node::fromExpr(item);
   if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){
     return cindexOf( item[0] );
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 826711897..990548979 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -615,6 +615,13 @@ public:
    */
   static size_t cindexOf(Expr item) CVC4_PUBLIC;
 
+  /**
+   * Same as above, but without checks. These methods should be used by
+   * internal (Node-level) code.
+   */
+  static size_t indexOfInternal(Expr item);
+  static size_t cindexOfInternal(Expr item);
+
   /** The type for iterators over constructors. */
   typedef DatatypeConstructorIterator iterator;
   /** The (const) type for iterators over constructors. */
diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml
index 8d6f0baf3..b74244fe1 100644
--- a/src/options/datatypes_options.toml
+++ b/src/options/datatypes_options.toml
@@ -175,3 +175,12 @@ header = "options/datatypes_options.h"
   default    = "-1"
   read_only  = true
   help       = "tells enumerative sygus to only consider solutions up to term size N (-1 == no limit, default)"
+
+[[option]]
+  name       = "sygusEvalBuiltin"
+  category   = "regular"
+  long       = "sygus-eval-builtin"
+  type       = "bool"
+  default    = "true"
+  read_only  = true
+  help       = "use builtin kind for evaluation functions in sygus"
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index cc8edadd0..90f0494d8 100644
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -16,6 +16,9 @@
 
 #include "theory/datatypes/datatypes_rewriter.h"
 
+using namespace CVC4;
+using namespace CVC4::kind;
+
 namespace CVC4 {
 namespace theory {
 namespace datatypes {
@@ -50,7 +53,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in)
         }
       }
       TNode constructor = in[0].getOperator();
-      size_t constructorIndex = Datatype::indexOf(constructor.toExpr());
+      size_t constructorIndex = indexOf(constructor);
       const Datatype& dt = Datatype::datatypeOf(constructor.toExpr());
       const DatatypeConstructor& c = dt[constructorIndex];
       unsigned weight = c.getWeight();
@@ -105,6 +108,51 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in)
       return RewriteResponse(REWRITE_AGAIN_FULL, res);
     }
   }
+  else if (k == DT_SYGUS_EVAL)
+  {
+    // sygus evaluation function
+    Node ev = in[0];
+    if (ev.getKind() == APPLY_CONSTRUCTOR)
+    {
+      Trace("dt-sygus-util") << "Rewrite " << in << " by unfolding...\n";
+      const Datatype& dt =
+          static_cast<DatatypeType>(ev.getType().toType()).getDatatype();
+      unsigned i = indexOf(ev.getOperator());
+      Node op = Node::fromExpr(dt[i].getSygusOp());
+      // if it is the "any constant" constructor, return its argument
+      if (op.getAttribute(SygusAnyConstAttribute()))
+      {
+        Assert(ev.getNumChildren() == 1);
+        Assert(ev[0].getType().isComparableTo(in.getType()));
+        return RewriteResponse(REWRITE_AGAIN_FULL, ev[0]);
+      }
+      std::vector<Node> args;
+      for (unsigned j = 1, nchild = in.getNumChildren(); j < nchild; j++)
+      {
+        args.push_back(in[j]);
+      }
+      Assert(!dt.isParametric());
+      std::vector<Node> children;
+      for (const Node& evc : ev)
+      {
+        std::vector<Node> cc;
+        cc.push_back(evc);
+        cc.insert(cc.end(), args.begin(), args.end());
+        children.push_back(nm->mkNode(DT_SYGUS_EVAL, cc));
+      }
+      Node ret = mkSygusTerm(dt, i, children);
+      // if it is a variable, apply the substitution
+      if (ret.getKind() == BOUND_VARIABLE)
+      {
+        Assert(ret.hasAttribute(SygusVarNumAttribute()));
+        int vn = ret.getAttribute(SygusVarNumAttribute());
+        Assert(Node::fromExpr(dt.getSygusVarList())[vn] == ret);
+        ret = args[vn];
+      }
+      Trace("dt-sygus-util") << "...got " << ret << "\n";
+      return RewriteResponse(REWRITE_AGAIN_FULL, ret);
+    }
+  }
 
   if (k == kind::EQUAL)
   {
@@ -138,6 +186,119 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in)
   return RewriteResponse(REWRITE_DONE, in);
 }
 
+Kind getOperatorKindForSygusBuiltin(Node op)
+{
+  Assert(op.getKind() != BUILTIN);
+  if (op.getKind() == LAMBDA)
+  {
+    // we use APPLY_UF instead of APPLY, since the rewriter for APPLY_UF
+    // does beta-reduction but does not for APPLY
+    return APPLY_UF;
+  }
+  TypeNode tn = op.getType();
+  if (tn.isConstructor())
+  {
+    return APPLY_CONSTRUCTOR;
+  }
+  else if (tn.isSelector())
+  {
+    return APPLY_SELECTOR;
+  }
+  else if (tn.isTester())
+  {
+    return APPLY_TESTER;
+  }
+  else if (tn.isFunction())
+  {
+    return APPLY_UF;
+  }
+  return NodeManager::operatorToKind(op);
+}
+
+Node DatatypesRewriter::mkSygusTerm(const Datatype& dt,
+                                    unsigned i,
+                                    const std::vector<Node>& children)
+{
+  Trace("dt-sygus-util") << "Make sygus term " << dt.getName() << "[" << i
+                         << "] with children: " << children << std::endl;
+  Assert(i < dt.getNumConstructors());
+  Assert(dt.isSygus());
+  Assert(!dt[i].getSygusOp().isNull());
+  std::vector<Node> schildren;
+  Node op = Node::fromExpr(dt[i].getSygusOp());
+  // if it is the any constant, we simply return the child
+  if (op.getAttribute(SygusAnyConstAttribute()))
+  {
+    Assert(children.size() == 1);
+    return children[0];
+  }
+  if (op.getKind() != BUILTIN)
+  {
+    schildren.push_back(op);
+  }
+  schildren.insert(schildren.end(), children.begin(), children.end());
+  Node ret;
+  if (op.getKind() == BUILTIN)
+  {
+    ret = NodeManager::currentNM()->mkNode(op, schildren);
+    Trace("dt-sygus-util") << "...return (builtin) " << ret << std::endl;
+    return ret;
+  }
+  Kind ok = getOperatorKindForSygusBuiltin(op);
+  if (schildren.size() == 1 && ok == kind::UNDEFINED_KIND)
+  {
+    ret = schildren[0];
+  }
+  else
+  {
+    ret = NodeManager::currentNM()->mkNode(ok, schildren);
+  }
+  Trace("dt-sygus-util") << "...return " << ret << std::endl;
+  return ret;
+}
+Node DatatypesRewriter::mkSygusEvalApp(const std::vector<Node>& children)
+{
+  if (options::sygusEvalBuiltin())
+  {
+    return NodeManager::currentNM()->mkNode(DT_SYGUS_EVAL, children);
+  }
+  // otherwise, using APPLY_UF
+  Assert(!children.empty());
+  Assert(children[0].getType().isDatatype());
+  const Datatype& dt =
+      static_cast<DatatypeType>(children[0].getType().toType()).getDatatype();
+  Assert(dt.isSygus());
+  std::vector<Node> schildren;
+  schildren.push_back(Node::fromExpr(dt.getSygusEvaluationFunc()));
+  schildren.insert(schildren.end(), children.begin(), children.end());
+  return NodeManager::currentNM()->mkNode(APPLY_UF, schildren);
+}
+
+bool DatatypesRewriter::isSygusEvalApp(Node n)
+{
+  if (options::sygusEvalBuiltin())
+  {
+    return n.getKind() == DT_SYGUS_EVAL;
+  }
+  // otherwise, using APPLY_UF
+  if (n.getKind() != APPLY_UF || n.getNumChildren() == 0)
+  {
+    return false;
+  }
+  TypeNode tn = n[0].getType();
+  if (!tn.isDatatype())
+  {
+    return false;
+  }
+  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  if (!dt.isSygus())
+  {
+    return false;
+  }
+  Node eval_op = Node::fromExpr(dt.getSygusEvaluationFunc());
+  return eval_op == n.getOperator();
+}
+
 RewriteResponse DatatypesRewriter::preRewrite(TNode in)
 {
   Trace("datatypes-rewrite-debug") << "pre-rewriting " << in << std::endl;
@@ -162,7 +323,7 @@ RewriteResponse DatatypesRewriter::preRewrite(TNode in)
         Node op = in.getOperator();
         // get the constructor object
         const DatatypeConstructor& dtc =
-            Datatype::datatypeOf(op.toExpr())[Datatype::indexOf(op.toExpr())];
+            Datatype::datatypeOf(op.toExpr())[indexOf(op)];
         // create ascribed constructor type
         Node tc = NodeManager::currentNM()->mkConst(
             AscriptionType(dtc.getSpecializedConstructorType(t)));
@@ -214,7 +375,7 @@ RewriteResponse DatatypesRewriter::rewriteSelector(TNode in)
     TypeNode argType = in[0].getType();
     TNode selector = in.getOperator();
     TNode constructor = in[0].getOperator();
-    size_t constructorIndex = Datatype::indexOf(constructor.toExpr());
+    size_t constructorIndex = indexOf(constructor);
     const Datatype& dt = Datatype::datatypeOf(selector.toExpr());
     const DatatypeConstructor& c = dt[constructorIndex];
     Trace("datatypes-rewrite-debug") << "Rewriting collapsable selector : "
@@ -294,8 +455,7 @@ RewriteResponse DatatypesRewriter::rewriteTester(TNode in)
 {
   if (in[0].getKind() == kind::APPLY_CONSTRUCTOR)
   {
-    bool result = Datatype::indexOf(in.getOperator().toExpr())
-                  == Datatype::indexOf(in[0].getOperator().toExpr());
+    bool result = indexOf(in.getOperator()) == indexOf(in[0].getOperator());
     Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
                                << "Rewrite trivial tester " << in << " "
                                << result << std::endl;
@@ -313,11 +473,10 @@ RewriteResponse DatatypesRewriter::rewriteTester(TNode in)
     return RewriteResponse(REWRITE_DONE,
                            NodeManager::currentNM()->mkConst(true));
   }
-  // could try dt.getNumConstructors()==2 &&
-  // Datatype::indexOf(in.getOperator())==1 ?
+  // could try dt.getNumConstructors()==2 && indexOf(in.getOperator())==1 ?
   else if (!options::dtUseTesters())
   {
-    unsigned tindex = Datatype::indexOf(in.getOperator().toExpr());
+    unsigned tindex = indexOf(in.getOperator());
     Trace("datatypes-rewrite-debug") << "Convert " << in << " to equality "
                                      << in[0] << " " << tindex << std::endl;
     Node neq = mkTester(in[0], tindex, dt);
@@ -416,7 +575,7 @@ int DatatypesRewriter::isInstCons(Node t, Node n, const Datatype& dt)
 {
   if (n.getKind() == kind::APPLY_CONSTRUCTOR)
   {
-    int index = Datatype::indexOf(n.getOperator().toExpr());
+    int index = indexOf(n.getOperator());
     const DatatypeConstructor& c = dt[index];
     Type nt = n.getType().toType();
     for (unsigned i = 0, size = n.getNumChildren(); i < size; i++)
@@ -440,7 +599,7 @@ int DatatypesRewriter::isTester(Node n, Node& a)
     if (n.getKind() == kind::APPLY_TESTER)
     {
       a = n[0];
-      return Datatype::indexOf(n.getOperator().toExpr());
+      return indexOf(n.getOperator());
     }
   }
   else
@@ -472,7 +631,7 @@ int DatatypesRewriter::isTester(Node n)
   {
     if (n.getKind() == kind::APPLY_TESTER)
     {
-      return Datatype::indexOf(n.getOperator().toExpr());
+      return indexOf(n.getOperator().toExpr());
     }
   }
   else
@@ -497,6 +656,24 @@ int DatatypesRewriter::isTester(Node n)
   return -1;
 }
 
+struct DtIndexAttributeId
+{
+};
+typedef expr::Attribute<DtIndexAttributeId, uint64_t> DtIndexAttribute;
+
+unsigned DatatypesRewriter::indexOf(Node n)
+{
+  if (!n.hasAttribute(DtIndexAttribute()))
+  {
+    Assert(n.getType().isConstructor() || n.getType().isTester()
+           || n.getType().isSelector());
+    unsigned index = Datatype::indexOfInternal(n.toExpr());
+    n.setAttribute(DtIndexAttribute(), index);
+    return index;
+  }
+  return n.getAttribute(DtIndexAttribute());
+}
+
 Node DatatypesRewriter::mkTester(Node n, int i, const Datatype& dt)
 {
   if (options::dtUseTesters())
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 8d9ddbf50..ed504e6bf 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -26,6 +26,19 @@
 
 namespace CVC4 {
 namespace theory {
+
+/** sygus var num */
+struct SygusVarNumAttributeId
+{
+};
+typedef expr::Attribute<SygusVarNumAttributeId, uint64_t> SygusVarNumAttribute;
+
+/** Attribute true for variables that represent any constant */
+struct SygusAnyConstAttributeId
+{
+};
+typedef expr::Attribute<SygusAnyConstAttributeId, bool> SygusAnyConstAttribute;
+
 namespace datatypes {
 
 class DatatypesRewriter {
@@ -59,6 +72,12 @@ public:
  static int isTester(Node n, Node& a);
  /** is tester, same as above but does not update an argument */
  static int isTester(Node n);
+ /**
+  * Get the index of a constructor or tester in its datatype, or the
+  * index of a selector in its constructor.  (Zero is always the
+  * first index.)
+  */
+ static unsigned indexOf(Node n);
  /** make tester is-C( n ), where C is the i^{th} constructor of dt */
  static Node mkTester(Node n, int i, const Datatype& dt);
  /** make tester split
@@ -102,6 +121,25 @@ public:
   *   C( x, y ) and z
   */
  static bool checkClash(Node n1, Node n2, std::vector<Node>& rew);
+ /** make sygus term
+  *
+  * This function returns a builtin term f( children[0], ..., children[n] )
+  * where f is the builtin op that the i^th constructor of sygus datatype dt
+  * encodes.
+  */
+ static Node mkSygusTerm(const Datatype& dt,
+                         unsigned i,
+                         const std::vector<Node>& children);
+ /** make sygus evaluation function application */
+ static Node mkSygusEvalApp(const std::vector<Node>& children);
+ /** is sygus evaluation function */
+ static bool isSygusEvalApp(Node n);
+ /**
+  * Get the builtin sygus operator for constructor term n of sygus datatype
+  * type. For example, if n is the term C_+( d1, d2 ) where C_+ is a sygus
+  * constructor whose sygus op is the builtin operator +, this method returns +.
+  */
+ static Node getSygusOpForCTerm(Node n);
 
 private:
  /** rewrite constructor term in */
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 328ef03d4..7773e7c5f 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -214,12 +214,22 @@ bool SygusSymBreakNew::computeTopLevel( TypeNode tn, Node n ){
 }
 
 void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std::vector< Node >& lemmas ) {
-  d_active_terms.insert( n );
-  Trace("sygus-sb-debug2") << "Sygus : activate term : " << n << " : " << exp << std::endl;  
-  
   TypeNode ntn = n.getType();
-  const Datatype& dt = ((DatatypeType)ntn.toType()).getDatatype();
-  
+  if (!ntn.isDatatype())
+  {
+    // nothing to do for non-datatype types
+    return;
+  }
+  const Datatype& dt = static_cast<DatatypeType>(ntn.toType()).getDatatype();
+  if (!dt.isSygus())
+  {
+    // nothing to do for non-sygus-datatype type
+    return;
+  }
+  d_active_terms.insert(n);
+  Trace("sygus-sb-debug2") << "Sygus : activate term : " << n << " : " << exp
+                           << std::endl;
+
   // get the search size for this
   Assert( d_term_to_anchor.find( n )!=d_term_to_anchor.end() );
   Node a = d_term_to_anchor[n];
@@ -280,6 +290,7 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std:
     addSymBreakLemmasFor( ntn, n, d, lemmas );
   }
 
+  Trace("sygus-sb-debug") << "Get simple symmetry breaking predicates...\n";
   unsigned max_depth = ssz>=d ? ssz-d : 0;
   unsigned min_depth = d_simple_proc[exp];
   if( min_depth<=max_depth ){
@@ -289,12 +300,15 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std:
     for (unsigned ds = 0; ds <= max_depth; ds++)
     {
       // static conjecture-independent symmetry breaking
+      Trace("sygus-sb-debug") << "  simple symmetry breaking...\n";
       Node ipred = getSimpleSymBreakPred(ntn, tindex, ds, usingSymCons);
       if (!ipred.isNull())
       {
         sb_lemmas.push_back(ipred);
       }
       // static conjecture-dependent symmetry breaking
+      Trace("sygus-sb-debug")
+          << "  conjecture-dependent symmetry breaking...\n";
       std::map<Node, quantifiers::CegConjecture*>::iterator itc =
           d_anchor_to_conj.find(a);
       if (itc != d_anchor_to_conj.end())
@@ -326,6 +340,7 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std:
   // now activate the children those testers were previously asserted in this
   // context and are awaiting activation, if they exist.
   if( options::sygusSymBreakLazy() ){
+    Trace("sygus-sb-debug") << "Do lazy symmetry breaking...\n";
     for( unsigned j=0; j<dt[tindex].getNumArgs(); j++ ){
       Node sel = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex].getSelectorInternal( ntn.toType(), j ) ), n );
       Trace("sygus-sb-debug2") << "  activate child sel : " << sel << std::endl;
@@ -336,6 +351,7 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std:
         assertTesterInternal( (*itt).second, sel, d_testers_exp[sel], lemmas );
       }
     }
+    Trace("sygus-sb-debug") << "...finished" << std::endl;
   }
 }
 
@@ -397,15 +413,32 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn,
   {
     return it->second;
   }
+  // this function is only called on sygus datatype types
+  Assert(tn.isDatatype());
   NodeManager* nm = NodeManager::currentNM();
   Node n = getFreeVar(tn);
   const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  Assert(dt.isSygus());
   Assert(tindex >= 0 && tindex < static_cast<int>(dt.getNumConstructors()));
+
+  Trace("sygus-sb-simple-debug")
+      << "Simple symmetry breaking for " << dt.getName() << ", constructor "
+      << dt[tindex].getName() << ", at depth " << depth << std::endl;
+
+  // if we are the "any constant" constructor, we do no symmetry breaking
+  // only do simple symmetry breaking up to depth 2
+  Node sop = Node::fromExpr(dt[tindex].getSygusOp());
+  if (sop.getAttribute(SygusAnyConstAttribute()) || depth > 2)
+  {
+    d_simple_sb_pred[tn][tindex][usingSymCons][depth] = Node::null();
+    return Node::null();
+  }
   // conjunctive conclusion of lemma
   std::vector<Node> sbp_conj;
 
   if (depth == 0)
   {
+    Trace("sygus-sb-simple-debug") << "  Size..." << std::endl;
     // fairness
     if (options::sygusFair() == SYGUS_FAIR_DT_SIZE)
     {
@@ -419,10 +452,11 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn,
 
   // symmetry breaking
   Kind nk = d_tds->getConsNumKind(tn, tindex);
-  // only do simple symmetry breaking up to depth 2
-  if (options::sygusSymBreak() && depth < 2)
+  if (options::sygusSymBreak())
   {
+    // the number of (sygus) arguments
     unsigned dt_index_nargs = dt[tindex].getNumArgs();
+
     // builtin type
     TypeNode tnb = TypeNode::fromType(dt.getSygusType());
     // get children
@@ -439,6 +473,7 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn,
 
     // direct solving for children
     //   for instance, we may want to insist that the LHS of MINUS is 0
+    Trace("sygus-sb-simple-debug") << "  Solve children..." << std::endl;
     std::map<unsigned, unsigned> children_solved;
     for (unsigned j = 0; j < dt_index_nargs; j++)
     {
@@ -458,6 +493,8 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn,
     {
       if (nk != UNDEFINED_KIND)
       {
+        Trace("sygus-sb-simple-debug")
+            << "  Equality reasoning about children..." << std::endl;
         // commutative operators
         if (quantifiers::TermUtil::isComm(nk))
         {
@@ -541,9 +578,9 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn,
             {
               const Datatype& cdt =
                   static_cast<DatatypeType>(tnc.toType()).getDatatype();
-              Node guard_val = nm->mkNode(
-                  APPLY_CONSTRUCTOR,
-                  Node::fromExpr(cdt[anyc_cons_num_c].getConstructor()));
+              Node fv = d_tds->getFreeVar(tnc, 0);
+              Node guard_val = datatypes::DatatypesRewriter::getInstCons(
+                  fv, cdt, anyc_cons_num_c);
               Node exp = d_tds->getExplain()->getExplanationForEquality(
                   children[c1], guard_val);
               sym_lem_deq = nm->mkNode(OR, exp, sym_lem_deq);
@@ -552,8 +589,8 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn,
           }
         }
 
-        Trace("sygus-sb-simple-debug") << "Process arguments for " << tn
-                                       << " : " << nk << " : " << std::endl;
+        Trace("sygus-sb-simple-debug") << "  Redundant operators..."
+                                       << std::endl;
         // singular arguments (e.g. 0 for mult)
         // redundant arguments (e.g. 0 for plus, 1 for mult)
         // right-associativity
@@ -716,19 +753,50 @@ void SygusSymBreakNew::registerSearchTerm( TypeNode tn, unsigned d, Node n, bool
   }
 }
 
-bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d, std::vector< Node >& lemmas ) {
-  Assert( n.getType()==nv.getType() );
-  Assert( nv.getKind()==APPLY_CONSTRUCTOR );
-  TypeNode tn = n.getType(); 
-  // currently bottom-up, could be top-down?
+Node SygusSymBreakNew::registerSearchValue(
+    Node a, Node n, Node nv, unsigned d, std::vector<Node>& lemmas)
+{
+  Assert(n.getType().isComparableTo(nv.getType()));
+  TypeNode tn = n.getType();
+  if (!tn.isDatatype())
+  {
+    // don't register non-datatype terms, instead we return the
+    // selector chain n.
+    return n;
+  }
+  const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype();
+  if (!dt.isSygus())
+  {
+    // don't register non-sygus-datatype terms
+    return n;
+  }
+  Assert(nv.getKind() == APPLY_CONSTRUCTOR);
+  NodeManager* nm = NodeManager::currentNM();
+  // we call the body of this function in a bottom-up fashion
+  // this ensures that the "abstraction" of the model value is available
   if( nv.getNumChildren()>0 ){
-    const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype();
-    unsigned cindex = Datatype::indexOf( nv.getOperator().toExpr() );
-    for( unsigned i=0; i<nv.getNumChildren(); i++ ){
-      Node sel = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex].getSelectorInternal( tn.toType(), i ) ), n );
-      if( !registerSearchValue( a, sel, nv[i], d+1, lemmas ) ){
-        return false;
+    unsigned cindex = DatatypesRewriter::indexOf(nv.getOperator());
+    std::vector<Node> rcons_children;
+    rcons_children.push_back(nv.getOperator());
+    bool childrenChanged = false;
+    for (unsigned i = 0, nchild = nv.getNumChildren(); i < nchild; i++)
+    {
+      Node sel = nm->mkNode(
+          APPLY_SELECTOR_TOTAL,
+          Node::fromExpr(dt[cindex].getSelectorInternal(tn.toType(), i)),
+          n);
+      Node nvc = registerSearchValue(a, sel, nv[i], d + 1, lemmas);
+      if (nvc.isNull())
+      {
+        return Node::null();
       }
+      rcons_children.push_back(nvc);
+      childrenChanged = childrenChanged || nvc != nv[i];
+    }
+    // reconstruct the value, which may be a skeleton
+    if (childrenChanged)
+    {
+      nv = nm->mkNode(APPLY_CONSTRUCTOR, rcons_children);
     }
   }
   Trace("sygus-sb-debug2") << "Registering search value " << n << " -> " << nv << std::endl;
@@ -750,7 +818,7 @@ bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d,
       quantifiers::DivByZeroSygusInvarianceTest dbzet;
       Trace("sygus-sb-mexp-debug") << "Minimize explanation for div-by-zero in " << d_tds->sygusToBuiltin( nv ) << std::endl;
       registerSymBreakLemmaForValue(a, nv, dbzet, Node::null(), lemmas);
-      return false;
+      return Node::null();
     }else{
       std::unordered_map<Node, Node, NodeHashFunction>::iterator itsv =
           d_cache[a].d_search_val[tn].find(bvr);
@@ -885,11 +953,11 @@ bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d,
 
         Trace("sygus-sb-mexp-debug") << "Minimize explanation for eval[" << d_tds->sygusToBuiltin( bad_val ) << "] = " << bvr << std::endl;
         registerSymBreakLemmaForValue(a, bad_val, eset, bad_val_o, lemmas);
-        return false;
+        return Node::null();
       }
     }
   }
-  return true;
+  return nv;
 }
 
 void SygusSymBreakNew::registerSymBreakLemmaForValue(
@@ -1179,6 +1247,9 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) {
   for( std::map< Node, bool >::iterator it = d_register_st.begin(); it != d_register_st.end(); ++it ){
     if( it->second ){
       Node prog = it->first;
+      Trace("dt-sygus-debug") << "Checking model value of " << prog << "..."
+                              << std::endl;
+      Assert(prog.getType().isDatatype());
       Node progv = d_td->getValuation().getModel()->getValue( prog );
       if (Trace.isOn("dt-sygus"))
       {
@@ -1214,7 +1285,9 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) {
         
         // register the search value ( prog -> progv ), this may invoke symmetry breaking 
         if( options::sygusSymBreakDynamic() ){
-          if( !registerSearchValue( prog, prog, progv, 0, lemmas ) ){
+          Node rsv = registerSearchValue(prog, prog, progv, 0, lemmas);
+          if (rsv.isNull())
+          {
             Trace("sygus-sb") << "  SygusSymBreakNew::check: ...added new symmetry breaking lemma for " << prog << "." << std::endl;
           }
           else
@@ -1226,6 +1299,7 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) {
     }
   }
   //register any measured terms that we haven't encountered yet (should only be invoked on first call to check
+  Trace("sygus-sb") << "Register size terms..." << std::endl;
   std::vector< Node > mts;
   d_tds->getEnumerators(mts);
   for( unsigned i=0; i<mts.size(); i++ ){
@@ -1251,7 +1325,12 @@ bool SygusSymBreakNew::checkTesters(Node n,
                                     int ind,
                                     std::vector<Node>& lemmas)
 {
-  Assert( vn.getKind()==kind::APPLY_CONSTRUCTOR );
+  if (vn.getKind() != kind::APPLY_CONSTRUCTOR)
+  {
+    // all datatype terms should be constant here
+    Assert(!vn.getType().isDatatype());
+    return true;
+  }
   if( Trace.isOn("sygus-sb-warn") ){
     Node prog_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, n );
     Node prog_szv = d_td->getValuation().getModel()->getValue( prog_sz );
@@ -1262,7 +1341,7 @@ bool SygusSymBreakNew::checkTesters(Node n,
   }
   TypeNode tn = n.getType();
   const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype();
-  int cindex = Datatype::indexOf( vn.getOperator().toExpr() );
+  int cindex = DatatypesRewriter::indexOf(vn.getOperator());
   Node tst = DatatypesRewriter::mkTester( n, cindex, dt );
   bool hastst = d_td->getValuation().getModel()->hasTerm( tst );
   Node tstrep = d_td->getValuation().getModel()->getRepresentative( tst );
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index eaed2a866..d08150a15 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -283,8 +283,21 @@ private:
    * z -> t for all terms t of appropriate depth, including d.
    * This function strengthens blocking clauses using generalization techniques
    * described in Reynolds et al SYNT 2017.
-   */
-  bool registerSearchValue( Node a, Node n, Node nv, unsigned d, std::vector< Node >& lemmas );
+   *
+   * The return value of this function is an abstraction of model assignment
+   * of nv to n, or null if we wish to exclude the model assignment nv to n.
+   * The return value of this method is different from nv itself, e.g. if it
+   * contains occurrences of the "any constant" constructor. For example, if
+   * nv is C_+( C_x(), C_{any_constant}( 5 ) ), then the return value of this
+   * function will either be null, or C_+( C_x(), C_{any_constant}( n.1.0 ) ),
+   * where n.1.0 is the appropriate selector chain applied to n. We build this
+   * abstraction since the semantics of C_{any_constant} is "any constant" and
+   * not "some constant". Thus, we should consider the subterm
+   * C_{any_constant}( 5 ) above to be an unconstrained variable (as represented
+   * by a selector chain), instead of the concrete value 5.
+   */
+  Node registerSearchValue(
+      Node a, Node n, Node nv, unsigned d, std::vector<Node>& lemmas);
   /** Register symmetry breaking lemma
    *
    * This function adds the symmetry breaking lemma template lem for terms of
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 65f258de1..9c7365ac1 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -114,4 +114,7 @@ typerule DT_SIZE_BOUND ::CVC4::theory::datatypes::DtBoundTypeRule
 operator DT_SYGUS_BOUND 2 "datatypes sygus bound"
 typerule DT_SYGUS_BOUND ::CVC4::theory::datatypes::DtSygusBoundTypeRule
 
+operator DT_SYGUS_EVAL 1: "datatypes sygus evaluation function"
+typerule DT_SYGUS_EVAL ::CVC4::theory::datatypes::DtSyguEvalTypeRule
+
 endtheory
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 18fadd052..4c79a31e9 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -65,8 +65,6 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
   d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
   //d_equalityEngine.addFunctionKind(kind::DT_SIZE);
   //d_equalityEngine.addFunctionKind(kind::DT_HEIGHT_BOUND);
-  //d_equalityEngine.addFunctionKind(kind::DT_SYGUS_TERM_ORDER);
-  //d_equalityEngine.addFunctionKind(kind::DT_SYGUS_IS_CONST);
   d_equalityEngine.addFunctionKind(kind::APPLY_TESTER);
   //d_equalityEngine.addFunctionKind(kind::APPLY_UF);
 
@@ -530,6 +528,8 @@ void TheoryDatatypes::finishInit() {
     quantifiers::TermDbSygus * tds = getQuantifiersEngine()->getTermDatabaseSygus();
     Assert( tds!=NULL );
     d_sygus_sym_break = new SygusSymBreakNew( this, tds, getSatContext() );
+    // do congruence on evaluation functions
+    d_equalityEngine.addFunctionKind(kind::DT_SYGUS_EVAL);
   }
 }
 
@@ -546,7 +546,7 @@ Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) {
     Node selector_use;
     TypeNode ndt = n[0].getType();
     if( options::dtSharedSelectors() ){
-      size_t selectorIndex = Datatype::indexOf(selectorExpr);
+      size_t selectorIndex = DatatypesRewriter::indexOf(selector);
       Trace("dt-expand") << "...selector index = " << selectorIndex << std::endl;
       Assert( selectorIndex<c.getNumArgs() );
       selector_use = Node::fromExpr( c.getSelectorInternal( ndt.toType(), selectorIndex ) );
@@ -961,7 +961,7 @@ Node TheoryDatatypes::getLabel( Node n ) {
 
 int TheoryDatatypes::getLabelIndex( EqcInfo* eqc, Node n ){
   if( eqc && !eqc->d_constructor.get().isNull() ){
-    return Datatype::indexOf( eqc->d_constructor.get().getOperator().toExpr() );
+    return DatatypesRewriter::indexOf(eqc->d_constructor.get().getOperator());
   }else{
     Node lbl = getLabel( n );
     if( lbl.isNull() ){
@@ -970,7 +970,6 @@ int TheoryDatatypes::getLabelIndex( EqcInfo* eqc, Node n ){
       int tindex = DatatypesRewriter::isTester( lbl );
       Assert( tindex!=-1 );
       return tindex;
-      //return Datatype::indexOf( getLabel( n ).getOperator().toExpr() );
     }
   }
 }
@@ -998,7 +997,6 @@ void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >
       for( int i=0; i<n_lbl; i++ ){
         Node t = d_labels_data[n][i];
         Assert( t.getKind()==NOT );
-        //pcons[ Datatype::indexOf( t[0].getOperator().toExpr() ) ] = false;
         int tindex = DatatypesRewriter::isTester( t[0] );
         Assert( tindex!=-1 );
         pcons[ tindex ] = false;
@@ -1077,7 +1075,6 @@ void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node
       Assert( ti.getKind()==NOT );
       j = ti;
       jt = j[0];
-      //int jtindex = Datatype::indexOf( jt.getOperator().toExpr() );
       int jtindex = DatatypesRewriter::isTester( jt );
       Assert( jtindex!=-1 );
       if( jtindex==ttindex ){
@@ -1212,7 +1209,7 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){
   //check labels
   NodeIntMap::iterator lbl_i = d_labels.find( n );
   if( lbl_i != d_labels.end() ){
-    size_t constructorIndex = Datatype::indexOf(c.getOperator().toExpr());
+    size_t constructorIndex = DatatypesRewriter::indexOf(c.getOperator());
     int n_lbl = (*lbl_i).second;
     for( int i=0; i<n_lbl; i++ ){
       Node t = d_labels_data[n][i];
@@ -1296,7 +1293,7 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) {
   }
   if( s.getKind()==kind::APPLY_SELECTOR_TOTAL ){
     Expr selectorExpr = s.getOperator().toExpr();
-    size_t constructorIndex = Datatype::indexOf(c.getOperator().toExpr());
+    size_t constructorIndex = DatatypesRewriter::indexOf(c.getOperator());
     const Datatype& dt = Datatype::datatypeOf(selectorExpr);
     const DatatypeConstructor& dtc = dt[constructorIndex];
     int selectorIndex = dtc.getSelectorIndexInternal( selectorExpr );
@@ -1305,10 +1302,6 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) {
     //if( wrong ){
     //  return;
     //}
-    //if( Datatype::indexOf(c.getOperator().toExpr())!=Datatype::cindexOf(s.getOperator().toExpr()) ){
-    //  mkExpDefSkolem( s.getOperator(), s[0].getType(), s.getType() );
-    //  r = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[s.getOperator().toExpr()], s[0] );
-    //}else{
     r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c );
     if( options::dtRefIntro() ){
       use_s = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), use_s );
@@ -2267,7 +2260,8 @@ std::pair<bool, Node> TheoryDatatypes::entailmentCheck(TNode lit, const Entailme
       Node r = d_equalityEngine.getRepresentative( n );
       EqcInfo * ei = getOrMakeEqcInfo( r, false );
       int l_index = getLabelIndex( ei, r );
-      int t_index = (int)Datatype::indexOf( atom.getOperator().toExpr() );
+      int t_index =
+          static_cast<int>(DatatypesRewriter::indexOf(atom.getOperator()));
       Trace("dt-entail") << "  Tester indices are " << t_index << " and " << l_index << std::endl;
       if( l_index!=-1 && (l_index==t_index)==pol ){
         std::vector< TNode > exp_c;
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 6ba64d8dd..94a99d46e 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -359,6 +359,52 @@ class DtSygusBoundTypeRule {
   }
 }; /* class DtSygusBoundTypeRule */
 
+class DtSyguEvalTypeRule
+{
+ public:
+  inline static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    TypeNode headType = n[0].getType(check);
+    if (!headType.isDatatype())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "datatype sygus eval takes a datatype head");
+    }
+    const Datatype& dt =
+        static_cast<DatatypeType>(headType.toType()).getDatatype();
+    if (!dt.isSygus())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "datatype sygus eval must have a datatype head that is sygus");
+    }
+    if (check)
+    {
+      Node svl = Node::fromExpr(dt.getSygusVarList());
+      if (svl.getNumChildren() + 1 != n.getNumChildren())
+      {
+        throw TypeCheckingExceptionPrivate(n,
+                                           "wrong number of arguments to a "
+                                           "datatype sygus evaluation "
+                                           "function");
+      }
+      for (unsigned i = 0, nvars = svl.getNumChildren(); i < nvars; i++)
+      {
+        TypeNode vtype = svl[i].getType(check);
+        TypeNode atype = n[i + 1].getType(check);
+        if (!vtype.isComparableTo(atype))
+        {
+          throw TypeCheckingExceptionPrivate(
+              n,
+              "argument type mismatch in a datatype sygus evaluation function");
+        }
+      }
+    }
+    return TypeNode::fromType(dt.getSygusType());
+  }
+}; /* class DtSygusBoundTypeRule */
+
 } /* CVC4::theory::datatypes namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp
index ee03b7815..a3d205a12 100644
--- a/src/theory/datatypes/type_enumerator.cpp
+++ b/src/theory/datatypes/type_enumerator.cpp
@@ -188,7 +188,7 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
      Debug("dt-enum-debug") << "done : " << t << std::endl;
      Assert( t.getKind()==kind::APPLY_CONSTRUCTOR );
      // start with the constructor for which a ground term is constructed
-     d_zeroCtor = Datatype::indexOf( t.getOperator().toExpr() );
+     d_zeroCtor = datatypes::DatatypesRewriter::indexOf(t.getOperator());
      d_has_debruijn = 0;
    }
    Debug("dt-enum") << "zero ctor : " << d_zeroCtor << std::endl;
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index ecb6db2fb..0f3dd74ae 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -23,7 +23,6 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/skolemize.h"
 #include "theory/quantifiers/sygus/ce_guided_instantiation.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
@@ -46,6 +45,7 @@ CegConjecture::CegConjecture(QuantifiersEngine* qe)
       d_ceg_cegis(new Cegis(qe, this)),
       d_ceg_cegisUnif(new CegisUnif(qe, this)),
       d_master(nullptr),
+      d_set_ce_sk_vars(false),
       d_repair_index(0),
       d_refine_count(0),
       d_syntax_guided(false)
@@ -239,10 +239,7 @@ void CegConjecture::doBasicCheck(std::vector< Node >& lems) {
   }
 }
 
-bool CegConjecture::needsRefinement() { 
-  return !d_ce_sk.empty();
-}
-
+bool CegConjecture::needsRefinement() const { return d_set_ce_sk_vars; }
 void CegConjecture::doCheck(std::vector<Node>& lems)
 {
   Assert(d_master != nullptr);
@@ -278,7 +275,7 @@ void CegConjecture::doCheck(std::vector<Node>& lems)
       }
       d_repair_index++;
       if (d_sygus_rconst->repairSolution(
-              d_candidates, fail_cvs, candidate_values))
+              d_candidates, fail_cvs, candidate_values, true))
       {
         constructed_cand = true;
       }
@@ -332,7 +329,7 @@ void CegConjecture::doCheck(std::vector<Node>& lems)
       recordInstantiation(candidate_values);
       return;
     }
-    Assert( d_ce_sk.empty() );
+    Assert(!d_set_ce_sk_vars);
   }else{
     if( !constructed_cand ){
       return;
@@ -340,33 +337,40 @@ void CegConjecture::doCheck(std::vector<Node>& lems)
   }
   
   //immediately skolemize inner existentials
-  Node instr = Rewriter::rewrite(inst);
+  d_set_ce_sk_vars = sk_refine;
   Node lem;
-  if (instr.getKind() == NOT && instr[0].getKind() == FORALL)
+  if (inst.getKind() == NOT && inst[0].getKind() == FORALL)
   {
+    // introduce the skolem variables
+    std::vector<Node> sks;
     if (constructed_cand)
     {
-      lem = d_qe->getSkolemize()->getSkolemizedBody(instr[0]).negate();
+      std::vector<Node> vars;
+      for (const Node& v : inst[0][0])
+      {
+        Node sk = nm->mkSkolem("rsk", v.getType());
+        sks.push_back(sk);
+        vars.push_back(v);
+      }
+      lem = inst[0][1].substitute(
+          vars.begin(), vars.end(), sks.begin(), sks.end());
+      lem = lem.negate();
     }
     if (sk_refine)
     {
-      Assert(!isGround());
-      d_ce_sk.push_back(instr[0]);
+      d_ce_sk_vars.insert(d_ce_sk_vars.end(), sks.begin(), sks.end());
     }
+    Assert(!isGround());
   }
   else
   {
     if (constructed_cand)
     {
       // use the instance itself
-      lem = instr;
-    }
-    if (sk_refine)
-    {
-      // we add null so that one test of the conjecture for the empty
-      // substitution is checked
-      d_ce_sk.push_back(Node::null());
+      lem = inst;
     }
+    // we add null so that one test of the conjecture for the empty
+    // substitution is checked
   }
   if (!lem.isNull())
   {
@@ -399,21 +403,19 @@ void CegConjecture::doCheck(std::vector<Node>& lems)
         
 void CegConjecture::doRefine( std::vector< Node >& lems ){
   Assert( lems.empty() );
-  Assert( d_ce_sk.size()==1 );
+  Assert(d_set_ce_sk_vars);
 
   //first, make skolem substitution
   Trace("cegqi-refine") << "doRefine : construct skolem substitution..." << std::endl;
   std::vector< Node > sk_vars;
   std::vector< Node > sk_subs;
   //collect the substitution over all disjuncts
-  Node ce_q = d_ce_sk[0];
-  if (!ce_q.isNull())
+  if (!d_ce_sk_vars.empty())
   {
-    std::vector<Node> skolems;
-    d_qe->getSkolemize()->getSkolemConstants(ce_q, skolems);
-    Assert(d_inner_vars.size() == skolems.size());
+    Trace("cegqi-refine") << "Get model values for skolems..." << std::endl;
+    Assert(d_inner_vars.size() == d_ce_sk_vars.size());
     std::vector<Node> model_values;
-    getModelValues(skolems, model_values);
+    getModelValues(d_ce_sk_vars, model_values);
     sk_vars.insert(sk_vars.end(), d_inner_vars.begin(), d_inner_vars.end());
     sk_subs.insert(sk_subs.end(), model_values.begin(), model_values.end());
   }
@@ -425,12 +427,10 @@ void CegConjecture::doRefine( std::vector< Node >& lems ){
   std::vector< Node > lem_c;
   Trace("cegqi-refine") << "doRefine : Construct refinement lemma..." << std::endl;
   Trace("cegqi-refine-debug")
-      << "  For counterexample point : " << ce_q << std::endl;
+      << "  For counterexample skolems : " << d_ce_sk_vars << std::endl;
   Node base_lem;
-  if (!ce_q.isNull())
+  if (d_base_inst.getKind() == NOT && d_base_inst[0].getKind() == FORALL)
   {
-    Assert(d_base_inst.getKind() == kind::NOT
-           && d_base_inst[0].getKind() == kind::FORALL);
     base_lem = d_base_inst[0][1];
   }
   else
@@ -440,13 +440,16 @@ void CegConjecture::doRefine( std::vector< Node >& lems ){
 
   Assert( sk_vars.size()==sk_subs.size() );
 
-  Trace("cegqi-refine") << "doRefine : construct and finalize lemmas..." << std::endl;
-
+  Trace("cegqi-refine") << "doRefine : substitute..." << std::endl;
   base_lem = base_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
+  Trace("cegqi-refine") << "doRefine : rewrite..." << std::endl;
   base_lem = Rewriter::rewrite( base_lem );
+  Trace("cegqi-refine") << "doRefine : register refinement lemma " << base_lem
+                        << "..." << std::endl;
   d_master->registerRefinementLemma(sk_vars, base_lem, lems);
-
-  d_ce_sk.clear();
+  Trace("cegqi-refine") << "doRefine : finished" << std::endl;
+  d_set_ce_sk_vars = false;
+  d_ce_sk_vars.clear();
 }
 
 void CegConjecture::preregisterConjecture( Node q ) {
@@ -483,15 +486,8 @@ Node CegConjecture::getModelValue( Node n ) {
 
 void CegConjecture::debugPrint( const char * c ) {
   Trace(c) << "Synthesis conjecture : " << d_embed_quant << std::endl;
-  Trace(c) << "  * Candidate program/output symbol : ";
-  for( unsigned i=0; i<d_candidates.size(); i++ ){
-    Trace(c) << d_candidates[i] << " ";
-  }
-  Trace(c) << std::endl;
-  Trace(c) << "  * Candidate ce skolems : ";
-  for( unsigned i=0; i<d_ce_sk.size(); i++ ){
-    Trace(c) << d_ce_sk[i] << " ";
-  }
+  Trace(c) << "  * Candidate programs : " << d_candidates << std::endl;
+  Trace(c) << "  * Counterexample skolems : " << d_ce_sk_vars << std::endl;
 }
 
 Node CegConjecture::getCurrentStreamGuard() const {
@@ -604,7 +600,8 @@ void CegConjecture::printAndContinueStream()
 
   // We will not refine the current candidate solution since it is a solution
   // thus, we clear information regarding the current refinement
-  d_ce_sk.clear();
+  d_set_ce_sk_vars = false;
+  d_ce_sk_vars.clear();
   // However, we need to exclude the current solution using an explicit
   // blocking clause, so that we proceed to the next solution.
   std::vector<Node> terms;
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h
index 231f9f14e..bf0ca4b16 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h
@@ -60,7 +60,7 @@ public:
   /** whether the conjecture is waiting for a call to doCheck below */
   bool needsCheck( std::vector< Node >& lem );
   /** whether the conjecture is waiting for a call to doRefine below */
-  bool needsRefinement();
+  bool needsRefinement() const;
   /** do single invocation check 
   * This updates Gamma for an iteration of step 2 of Figure 1 of Reynolds et al CAV 2015.
   */
@@ -173,11 +173,16 @@ private:
   /** list of variables on inner quantification */
   std::vector< Node > d_inner_vars;
   /**
-   * The set of current existentially quantified formulas whose couterexamples
-   * we must refine. This may be added to during calls to doCheck(). The model
-   * values for skolems of these formulas are analyzed during doRefine().
+   * The set of skolems for the current "verification" lemma, if one exists.
+   * This may be added to during calls to doCheck(). The model values for these
+   * skolems are analyzed during doRefine().
    */
-  std::vector<Node> d_ce_sk;
+  std::vector<Node> d_ce_sk_vars;
+  /**
+   * Whether the above vector has been set. We have this flag since the above
+   * vector may be set to empty (e.g. for ground synthesis conjectures).
+   */
+  bool d_set_ce_sk_vars;
 
   /** the asserted (negated) conjecture */
   Node d_quant;
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
index 24b57d025..8b15d241e 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -1211,11 +1211,21 @@ Node CegConjectureSingleInvSol::builtinToSygusConst(Node c,
   Node sc;
   d_builtin_const_to_sygus[tn][c] = sc;
   Assert(c.isConst());
-  Assert(tn.isDatatype());
+  if (!tn.isDatatype())
+  {
+    // if we've traversed to a builtin type, simply return c
+    d_builtin_const_to_sygus[tn][c] = c;
+    return c;
+  }
   const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
   Trace("csi-rcons-debug") << "Try to reconstruct " << c << " in "
                            << dt.getName() << std::endl;
-  Assert(dt.isSygus());
+  if (!dt.isSygus())
+  {
+    // if we've traversed to a builtin datatype type, simply return c
+    d_builtin_const_to_sygus[tn][c] = c;
+    return c;
+  }
   // if we are not interested in reconstructing constants, or the grammar allows
   // them, return a proxy
   if (!options::cegqiSingleInvReconstructConst() || dt.getSygusAllowConst())
@@ -1496,9 +1506,7 @@ Node CegConjectureSingleInvSol::getGenericBase(TypeNode tn,
   }
   TermDbSygus* tds = d_qe->getTermDatabaseSygus();
   Assert(tds->isRegistered(tn));
-  std::map<TypeNode, int> var_count;
-  std::map<int, Node> pre;
-  Node g = tds->mkGeneric(dt, c, var_count, pre);
+  Node g = tds->mkGeneric(dt, c);
   Trace("csi-sol-debug") << "Generic is " << g << std::endl;
   Node gr = Rewriter::rewrite(g);
   Trace("csi-sol-debug") << "Generic rewritten is " << gr << std::endl;
diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
index 09df1eeab..36cbb89fe 100644
--- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
+++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/sygus_eval_unfold.h"
 
 #include "options/quantifiers_options.h"
+#include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
 using namespace std;
@@ -30,27 +31,11 @@ SygusEvalUnfold::SygusEvalUnfold(TermDbSygus* tds) : d_tds(tds) {}
 void SygusEvalUnfold::registerEvalTerm(Node n)
 {
   Assert(options::sygusEvalUnfold());
-  // is this an APPLY_UF term with head that is a sygus datatype term?
-  if (n.getKind() != APPLY_UF)
+  // is this a sygus evaluation function application?
+  if (!datatypes::DatatypesRewriter::isSygusEvalApp(n))
   {
     return;
   }
-  TypeNode tn = n[0].getType();
-  if (!tn.isDatatype())
-  {
-    return;
-  }
-  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
-  if (!dt.isSygus())
-  {
-    return;
-  }
-  Node f = n.getOperator();
-  if (n[0].getKind() == APPLY_CONSTRUCTOR)
-  {
-    // constructors should be unfolded and reduced already
-    return;
-  }
   if (d_eval_processed.find(n) != d_eval_processed.end())
   {
     return;
@@ -58,10 +43,15 @@ void SygusEvalUnfold::registerEvalTerm(Node n)
   Trace("sygus-eval-unfold")
       << "SygusEvalUnfold: register eval term : " << n << std::endl;
   d_eval_processed.insert(n);
-  // is it the sygus evaluation function?
-  Node eval_op = Node::fromExpr(dt.getSygusEvaluationFunc());
-  if (n.getOperator() != eval_op)
+  TypeNode tn = n[0].getType();
+  // since n[0] is an evaluation head, we know tn is a sygus datatype
+  Assert(tn.isDatatype());
+  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  Assert(dt.isSygus());
+  if (n[0].getKind() == APPLY_CONSTRUCTOR)
   {
+    // constructors should be unfolded and reduced already
+    Assert(false);
     return;
   }
   // register this evaluation term with its head
@@ -112,6 +102,7 @@ void SygusEvalUnfold::registerModelValue(Node a,
           antec_exp.size() == 1 ? antec_exp[0] : nm->mkNode(AND, antec_exp);
       // Node antec = n.eqNode( vn );
       TypeNode tn = n.getType();
+      // n occurs as an evaluation head, thus it has sygus datatype type
       Assert(tn.isDatatype());
       const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
       Assert(dt.isSygus());
@@ -132,7 +123,6 @@ void SygusEvalUnfold::registerModelValue(Node a,
       }
       // evaluation children
       std::vector<Node> eval_children;
-      eval_children.push_back(Node::fromExpr(dt.getSygusEvaluationFunc()));
       eval_children.push_back(n);
       // for each evaluation
       for (unsigned i = start; i < curr_size; i++)
@@ -157,8 +147,9 @@ void SygusEvalUnfold::registerModelValue(Node a,
           vtm[n] = vn;
           eval_children.insert(
               eval_children.end(), it->second[i].begin(), it->second[i].end());
-          Node eval_fun = nm->mkNode(APPLY_UF, eval_children);
-          eval_children.resize(2);
+          Node eval_fun =
+              datatypes::DatatypesRewriter::mkSygusEvalApp(eval_children);
+          eval_children.resize(1);
           res = d_tds->unfold(eval_fun, vtm, exp);
           expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp);
         }
@@ -167,13 +158,15 @@ void SygusEvalUnfold::registerModelValue(Node a,
           EvalSygusInvarianceTest esit;
           eval_children.insert(
               eval_children.end(), it->second[i].begin(), it->second[i].end());
-          Node conj = nm->mkNode(APPLY_UF, eval_children);
-          eval_children[1] = vn;
-          Node eval_fun = nm->mkNode(APPLY_UF, eval_children);
+          Node conj =
+              datatypes::DatatypesRewriter::mkSygusEvalApp(eval_children);
+          eval_children[0] = vn;
+          Node eval_fun =
+              datatypes::DatatypesRewriter::mkSygusEvalApp(eval_children);
           res = d_tds->evaluateWithUnfolding(eval_fun);
           esit.init(conj, n, res);
-          eval_children.resize(2);
-          eval_children[1] = n;
+          eval_children.resize(1);
+          eval_children[0] = n;
 
           // evaluate with minimal explanation
           std::vector<Node> mexp;
diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp
index 2be6c9d91..f472353e5 100644
--- a/src/theory/quantifiers/sygus/sygus_explain.cpp
+++ b/src/theory/quantifiers/sygus/sygus_explain.cpp
@@ -123,16 +123,23 @@ void SygusExplain::getExplanationForEquality(Node n,
                                              std::vector<Node>& exp,
                                              std::map<unsigned, bool>& cexc)
 {
-  Assert(n.getType() == vn.getType());
+  // since builtin types occur in grammar, types are comparable but not
+  // necessarily equal
+  Assert(n.getType().isComparableTo(n.getType()));
   if (n == vn)
   {
     return;
   }
-  Assert(vn.getKind() == kind::APPLY_CONSTRUCTOR);
   TypeNode tn = n.getType();
-  Assert(tn.isDatatype());
+  if (!tn.isDatatype())
+  {
+    // sygus datatype fields that are not sygus datatypes are treated as
+    // abstractions only, hence we disregard this field
+    return;
+  }
+  Assert(vn.getKind() == kind::APPLY_CONSTRUCTOR);
   const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype();
-  int i = Datatype::indexOf(vn.getOperator().toExpr());
+  int i = datatypes::DatatypesRewriter::indexOf(vn.getOperator());
   Node tst = datatypes::DatatypesRewriter::mkTester(n, i, dt);
   exp.push_back(tst);
   for (unsigned j = 0; j < vn.getNumChildren(); j++)
@@ -178,10 +185,16 @@ void SygusExplain::getExplanationFor(TermRecBuild& trb,
                                      int& sz)
 {
   Assert(vnr.isNull() || vn != vnr);
+  Assert(n.getType().isComparableTo(vn.getType()));
+  TypeNode ntn = n.getType();
+  if (!ntn.isDatatype())
+  {
+    // sygus datatype fields that are not sygus datatypes are treated as
+    // abstractions only, hence we disregard this field
+    return;
+  }
   Assert(vn.getKind() == APPLY_CONSTRUCTOR);
   Assert(vnr.isNull() || vnr.getKind() == APPLY_CONSTRUCTOR);
-  Assert(n.getType() == vn.getType());
-  TypeNode ntn = n.getType();
   std::map<unsigned, bool> cexc;
   // for each child, 
   // check whether replacing that child by a fresh variable
@@ -210,7 +223,7 @@ void SygusExplain::getExplanationFor(TermRecBuild& trb,
     }
   }
   const Datatype& dt = ((DatatypeType)ntn.toType()).getDatatype();
-  int cindex = Datatype::indexOf(vn.getOperator().toExpr());
+  int cindex = datatypes::DatatypesRewriter::indexOf(vn.getOperator());
   Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors());
   Node tst = datatypes::DatatypesRewriter::mkTester(n, cindex, dt);
   exp.push_back(tst);
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index d745cb6da..79db09175 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -18,9 +18,10 @@
 
 #include "expr/datatype.h"
 #include "options/quantifiers_options.h"
+#include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/sygus/ce_guided_conjecture.h"
-#include "theory/quantifiers/sygus/sygus_process_conj.h"
 #include "theory/quantifiers/sygus/sygus_grammar_norm.h"
+#include "theory/quantifiers/sygus/sygus_process_conj.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 
@@ -302,20 +303,16 @@ Node CegGrammarConstructor::convertToEmbedding( Node n, std::map< Node, Node >&
         op = cur;
       }
       // is the operator a synth function?
+      bool makeEvalFun = false;
       if( !op.isNull() ){
         std::map< Node, Node >::iterator its = synth_fun_vars.find( op );
         if( its!=synth_fun_vars.end() ){
-          Assert( its->second.getType().isDatatype() );
-          // will make into an application of an evaluation function
-          const Datatype& dt = ((DatatypeType)its->second.getType().toType()).getDatatype();
-          Assert( dt.isSygus() );
-          children.push_back( Node::fromExpr( dt.getSygusEvaluationFunc() ) );
           children.push_back( its->second );
-          childChanged = true;
-          ret_k = kind::APPLY_UF;
+          makeEvalFun = true;
         }
       }
-      if( !childChanged ){
+      if (!makeEvalFun)
+      {
         // otherwise, we apply the previous operator
         if( cur.getMetaKind() == kind::metakind::PARAMETERIZED ){
           children.push_back( cur.getOperator() );
@@ -328,7 +325,13 @@ Node CegGrammarConstructor::convertToEmbedding( Node n, std::map< Node, Node >&
         childChanged = childChanged || cur[i] != it->second;
         children.push_back(it->second);
       }
-      if (childChanged) {
+      if (makeEvalFun)
+      {
+        // will make into an application of an evaluation function
+        ret = datatypes::DatatypesRewriter::mkSygusEvalApp(children);
+      }
+      else if (childChanged)
+      {
         ret = NodeManager::currentNM()->mkNode(ret_k, children);
       }
       visited[cur] = ret;
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index a468e1383..d1990d6c7 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -20,6 +20,7 @@
 #include "printer/sygus_print_callback.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
+#include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
 #include "theory/quantifiers/sygus/ce_guided_conjecture.h"
 #include "theory/quantifiers/sygus/sygus_grammar_red.h"
@@ -125,11 +126,14 @@ void SygusGrammarNorm::TypeObject::buildDatatype(SygusGrammarNorm* sygus_norm,
       std::stringstream ss;
       ss << d_unres_tn << "_any_constant";
       std::string cname(ss.str());
-      std::vector<Type> empty_arg_types;
+      std::vector<Type> builtin_arg;
+      builtin_arg.push_back(dt.getSygusType());
       // we add this constructor first since we use left associative chains
       // and our symmetry breaking should group any constants together
       // beneath the same application
-      d_dt.addSygusConstructor(av.toExpr(), cname, empty_arg_types);
+      // we set its weight to zero since it should be considered at the
+      // same level as constants.
+      d_dt.addSygusConstructor(av.toExpr(), cname, builtin_arg, nullptr, 0);
     }
   }
   for (unsigned i = 0, size_d_ops = d_ops.size(); i < size_d_ops; ++i)
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
index 47cc19377..f72a83e5a 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
@@ -36,12 +36,6 @@ namespace quantifiers {
 
 class SygusGrammarNorm;
 
-/** Attribute true for variables that represent any constant */
-struct SygusAnyConstAttributeId
-{
-};
-typedef expr::Attribute<SygusAnyConstAttributeId, bool> SygusAnyConstAttribute;
-
 /** Operator position trie class
  *
  * This data structure stores an unresolved type corresponding to the
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 9919dff49..80d41a73d 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -47,55 +47,64 @@ void CegConjecturePbe::collectExamples( Node n, std::map< Node, bool >& visited,
     visited[n] = true;
     Node neval;
     Node n_output;
-    if( n.getKind()==APPLY_UF && n.getNumChildren()>0 ){
+    bool neval_is_evalapp = false;
+    if (datatypes::DatatypesRewriter::isSygusEvalApp(n))
+    {
       neval = n;
       if( hasPol ){
         n_output = !pol ? d_true : d_false;
       }
+      neval_is_evalapp = true;
     }else if( n.getKind()==EQUAL && hasPol && !pol ){
       for( unsigned r=0; r<2; r++ ){
-        if( n[r].getKind()==APPLY_UF && n[r].getNumChildren()>0 ){
+        if (datatypes::DatatypesRewriter::isSygusEvalApp(n[r]))
+        {
           neval = n[r];
           if( n[1-r].isConst() ){
             n_output = n[1-r];
           }
+          neval_is_evalapp = true;
         }
       }
     }
-    if( !neval.isNull() ){
-      if( neval.getKind()==APPLY_UF && neval.getNumChildren()>0 ){
-        // is it an evaluation function?
-        if( d_examples.find( neval[0] )!=d_examples.end() ){
-          std::map< Node, bool >::iterator itx = d_examples_invalid.find( neval[0] );
-          if( itx==d_examples_invalid.end() ){
-            //collect example
-            bool success = true;
-            std::vector< Node > ex;
-            for( unsigned j=1; j<neval.getNumChildren(); j++ ){
-              if( !neval[j].isConst() ){
-                success = false;
-                break;
-              }else{
-                ex.push_back( neval[j] );
-              }
-            }
-            if( success ){
-              d_examples[neval[0]].push_back( ex );
-              d_examples_out[neval[0]].push_back( n_output );
-              d_examples_term[neval[0]].push_back( neval );
-              if( n_output.isNull() ){
-                d_examples_out_invalid[neval[0]] = true;
-              }else{
-                Assert( n_output.isConst() );
-              }
-              //finished processing this node
-              return;
-            }else{
-              d_examples_invalid[neval[0]] = true;
-              d_examples_out_invalid[neval[0]] = true;
-            }
+    // is it an evaluation function?
+    if (neval_is_evalapp && d_examples.find(neval[0]) != d_examples.end())
+    {
+      // get the evaluation head
+      Node eh = neval[0];
+      std::map<Node, bool>::iterator itx = d_examples_invalid.find(eh);
+      if (itx == d_examples_invalid.end())
+      {
+        // collect example
+        bool success = true;
+        std::vector<Node> ex;
+        for (unsigned j = 1, nchild = neval.getNumChildren(); j < nchild; j++)
+        {
+          if (!neval[j].isConst())
+          {
+            success = false;
+            break;
+          }
+          ex.push_back(neval[j]);
+        }
+        if (success)
+        {
+          d_examples[eh].push_back(ex);
+          d_examples_out[eh].push_back(n_output);
+          d_examples_term[eh].push_back(neval);
+          if (n_output.isNull())
+          {
+            d_examples_out_invalid[eh] = true;
+          }
+          else
+          {
+            Assert(n_output.isConst());
           }
+          // finished processing this node
+          return;
         }
+        d_examples_invalid[eh] = true;
+        d_examples_out_invalid[eh] = true;
       }
     }
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
index a961c9780..ef530e722 100644
--- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp
+++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
@@ -17,6 +17,7 @@
 #include <stack>
 
 #include "expr/datatype.h"
+#include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 77930fb42..4aaccc71e 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -19,6 +19,7 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
 #include "theory/quantifiers/sygus/sygus_grammar_norm.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
@@ -61,9 +62,18 @@ void SygusRepairConst::registerSygusType(TypeNode tn,
   if (tprocessed.find(tn) == tprocessed.end())
   {
     tprocessed[tn] = true;
-    Assert(tn.isDatatype());
+    if (!tn.isDatatype())
+    {
+      // may have recursed to a non-datatype, e.g. in the case that we have
+      // "any constant" constructors
+      return;
+    }
     const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
-    Assert(dt.isSygus());
+    if (!dt.isSygus())
+    {
+      // may have recursed to a non-sygus-datatype
+      return;
+    }
     // check if this datatype allows all constants
     if (dt.getSygusAllowConst())
     {
@@ -292,19 +302,22 @@ bool SygusRepairConst::isRepairable(Node n, bool useConstantsAsHoles)
   TypeNode tn = n.getType();
   Assert(tn.isDatatype());
   const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
-  Assert(dt.isSygus());
-  Node op = n.getOperator();
-  unsigned cindex = Datatype::indexOf(op.toExpr());
-  if (dt[cindex].getNumArgs() > 0)
+  if (!dt.isSygus())
   {
     return false;
   }
+  Node op = n.getOperator();
+  unsigned cindex = datatypes::DatatypesRewriter::indexOf(op);
   Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp());
   if (sygusOp.getAttribute(SygusAnyConstAttribute()))
   {
     // if it represents "any constant" then it is repairable
     return true;
   }
+  if (dt[cindex].getNumArgs() > 0)
+  {
+    return false;
+  }
   if (useConstantsAsHoles && dt.getSygusAllowConst())
   {
     if (sygusOp.isConst())
@@ -445,7 +458,7 @@ Node SygusRepairConst::getFoQuery(const std::vector<Node>& candidates,
     if (it == visited.end())
     {
       visited[cur] = Node::null();
-      if (cur.getKind() == APPLY_UF && cur.getNumChildren() > 0)
+      if (datatypes::DatatypesRewriter::isSygusEvalApp(cur))
       {
         Node v = cur[0];
         if (std::find(sk_vars.begin(), sk_vars.end(), v) != sk_vars.end())
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index a96505ce4..759ee6ffa 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -17,6 +17,7 @@
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
+#include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/sygus/ce_guided_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
@@ -80,7 +81,7 @@ Node SygusUnifRl::purifyLemma(Node n,
   // We retrive model value now because purified node may not have a value
   Node nv = n;
   // Whether application of a function-to-synthesize
-  bool fapp = k == APPLY_UF && size > 0;
+  bool fapp = datatypes::DatatypesRewriter::isSygusEvalApp(n);
   bool u_fapp = false;
   bool nu_fapp = false;
   if (fapp)
@@ -135,10 +136,10 @@ Node SygusUnifRl::purifyLemma(Node n,
   Node nb;
   if (childChanged)
   {
-    if (fapp && n.hasOperator())
+    if (n.getMetaKind() == metakind::PARAMETERIZED)
     {
       Trace("sygus-unif-rl-purify-debug") << "Node " << n
-                                          << " has operator and fapp is true\n";
+                                          << " is parameterized\n";
       children.insert(children.begin(), n.getOperator());
     }
     if (Trace.isOn("sygus-unif-rl-purify-debug"))
@@ -165,11 +166,6 @@ Node SygusUnifRl::purifyLemma(Node n,
     std::map<Node, Node>::const_iterator it = d_app_to_purified.find(nb);
     if (it == d_app_to_purified.end())
     {
-      if (!childChanged)
-      {
-        Assert(nb.hasOperator());
-        children.insert(children.begin(), n.getOperator());
-      }
       // Build purified head with fresh skolem and recreate node
       std::stringstream ss;
       ss << nb[0] << "_" << d_cand_to_hd_count[nb[0]]++;
@@ -183,10 +179,10 @@ Node SygusUnifRl::purifyLemma(Node n,
       d_cand_to_eval_hds[nb[0]].push_back(new_f);
       // Maps new enumerator to its respective tuple of arguments
       d_hd_to_pt[new_f] =
-          std::vector<Node>(children.begin() + 2, children.end());
+          std::vector<Node>(children.begin() + 1, children.end());
       if (Trace.isOn("sygus-unif-rl-purify-debug"))
       {
-        Trace("sygus-unif-rl-purify-debug") << "...[" << new_f << "] --> (";
+        Trace("sygus-unif-rl-purify-debug") << "...[" << new_f << "] --> ( ";
         for (const Node& pt_i : d_hd_to_pt[new_f])
         {
           Trace("sygus-unif-rl-purify-debug") << pt_i << " ";
@@ -194,9 +190,11 @@ Node SygusUnifRl::purifyLemma(Node n,
         Trace("sygus-unif-rl-purify-debug") << ")\n";
       }
       // replace first child and rebulid node
-      children[1] = new_f;
-      Assert(children.size() > 1);
-      np = NodeManager::currentNM()->mkNode(k, children);
+      Assert(children.size() > 0);
+      children[0] = new_f;
+      Trace("sygus-unif-rl-purify-debug") << "Make sygus eval app " << children
+                                          << std::endl;
+      np = datatypes::DatatypesRewriter::mkSygusEvalApp(children);
       d_app_to_purified[nb] = np;
     }
     else
@@ -846,17 +844,18 @@ Node SygusUnifRl::DecisionTreeInfo::PointSeparator::evaluate(Node n,
   Assert(d_dt->d_unif->d_hd_to_pt.find(n) != d_dt->d_unif->d_hd_to_pt.end());
   std::vector<Node> pt = d_dt->d_unif->d_hd_to_pt[n];
   // compute the result
-  Node res = d_dt->d_unif->d_tds->evaluateBuiltin(tn, builtin_cond, pt);
   if (Trace.isOn("sygus-unif-rl-sep"))
   {
-    Trace("sygus-unif-rl-sep") << "...got res = " << res << " from cond "
-                               << builtin_cond << " on pt " << n << " ( ";
+    Trace("sygus-unif-rl-sep") << "Evaluate cond " << builtin_cond << " on pt "
+                               << n << " ( ";
     for (const Node& pti : pt)
     {
       Trace("sygus-unif-rl-sep") << pti << " ";
     }
     Trace("sygus-unif-rl-sep") << ")\n";
   }
+  Node res = d_dt->d_unif->d_tds->evaluateBuiltin(tn, builtin_cond, pt);
+  Trace("sygus-unif-rl-sep") << "...got res = " << res << "\n";
   // If condition is templated, recompute result accordingly
   Node templ = d_dt->d_template.first;
   TNode templ_var = d_dt->d_template.second;
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index e236613c0..5a5ca1719 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -208,6 +208,8 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
   }
 
   // look at information on how we will construct solutions for this type
+  // we know this is a sygus datatype since it is either the top-level type
+  // in the strategy graph, or was recursed by a strategy we inferred.
   Assert(tn.isDatatype());
   const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
   Assert(dt.isSygus());
@@ -246,14 +248,13 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
     }
     Node ut = nm->mkNode(APPLY_CONSTRUCTOR, utchildren);
     std::vector<Node> echildren;
-    echildren.push_back(Node::fromExpr(dt.getSygusEvaluationFunc()));
     echildren.push_back(ut);
     Node sbvl = Node::fromExpr(dt.getSygusVarList());
     for (const Node& sbv : sbvl)
     {
       echildren.push_back(sbv);
     }
-    Node eut = nm->mkNode(APPLY_UF, echildren);
+    Node eut = datatypes::DatatypesRewriter::mkSygusEvalApp(echildren);
     Trace("sygus-unif-debug2") << "  Test evaluation of " << eut << "..."
                                << std::endl;
     eut = d_qe->getTermDatabaseSygus()->unfold(eut);
@@ -292,13 +293,10 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
       for (unsigned k = 0, sksize = sks.size(); k < sksize; k++)
       {
         Assert(sks[k].getType().isDatatype());
-        const Datatype& cdt =
-            static_cast<DatatypeType>(sks[k].getType().toType()).getDatatype();
-        echildren[0] = Node::fromExpr(cdt.getSygusEvaluationFunc());
-        echildren[1] = sks[k];
+        echildren[0] = sks[k];
         Trace("sygus-unif-debug2") << "...set eval dt to " << sks[k]
                                    << std::endl;
-        Node esk = nm->mkNode(APPLY_UF, echildren);
+        Node esk = datatypes::DatatypesRewriter::mkSygusEvalApp(echildren);
         vs.push_back(esk);
         Node tvar = nm->mkSkolem("templ", esk.getType());
         templ_var_index[tvar] = k;
@@ -803,8 +801,7 @@ void SygusUnifStrategy::staticLearnRedundantOps(
       continue;
     }
     EnumTypeInfoStrat* etis = snode.d_strats[j];
-    unsigned cindex =
-        static_cast<unsigned>(Datatype::indexOf(etis->d_cons.toExpr()));
+    unsigned cindex = datatypes::DatatypesRewriter::indexOf(etis->d_cons);
     // constructors that correspond to strategies are not needed
     // the intuition is that the strategy itself is responsible for constructing
     // all terms that use the given constructor
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 8f20e2ffc..76836d838 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -17,8 +17,8 @@
 #include "base/cvc4_check.h"
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
+#include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/sygus/sygus_grammar_norm.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
@@ -139,19 +139,16 @@ Node TermDbSygus::mkGeneric(const Datatype& dt,
   Assert( dt.isSygus() );
   Assert( !dt[c].getSygusOp().isNull() );
   std::vector< Node > children;
-  Node op = Node::fromExpr( dt[c].getSygusOp() );
-  if( op.getKind()!=BUILTIN ){
-    children.push_back( op );
-  }
-  Trace("sygus-db-debug") << "mkGeneric " << dt.getName() << " " << op << " " << op.getKind() << "..." << std::endl;
+  Trace("sygus-db-debug") << "mkGeneric " << dt.getName() << " " << c << "..."
+                          << std::endl;
   for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++)
   {
-    TypeNode tna = getArgType( dt[c], i );
     Node a;
     std::map< int, Node >::iterator it = pre.find( i );
     if( it!=pre.end() ){
       a = it->second;
     }else{
+      TypeNode tna = TypeNode::fromType(dt[c].getArgType(i));
       a = getFreeVarInc( tna, var_count, true );
     }
     Trace("sygus-db-debug")
@@ -159,21 +156,7 @@ Node TermDbSygus::mkGeneric(const Datatype& dt,
     Assert( !a.isNull() );
     children.push_back( a );
   }
-  Node ret;
-  if( op.getKind()==BUILTIN ){
-    Trace("sygus-db-debug") << "Make builtin node..." << std::endl;
-    ret = NodeManager::currentNM()->mkNode( op, children );
-  }else{
-    Kind ok = getOperatorKind( op );
-    Trace("sygus-db-debug") << "Operator kind is " << ok << std::endl;
-    if( children.size()==1 && ok==kind::UNDEFINED_KIND ){
-      ret = children[0];
-    }else{
-      ret = NodeManager::currentNM()->mkNode( ok, children );
-    }
-  }
-  Trace("sygus-db-debug") << "...returning " << ret << std::endl;
-  return ret;
+  return datatypes::DatatypesRewriter::mkSygusTerm(dt, c, children);
 }
 
 Node TermDbSygus::mkGeneric(const Datatype& dt, int c, std::map<int, Node>& pre)
@@ -194,49 +177,39 @@ struct SygusToBuiltinAttributeId
 typedef expr::Attribute<SygusToBuiltinAttributeId, Node>
     SygusToBuiltinAttribute;
 
-Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) {
-  std::map<TypeNode, int> var_count;
-  return sygusToBuiltin(n, tn, var_count);
-}
-
-Node TermDbSygus::sygusToBuiltin(Node n,
-                                 TypeNode tn,
-                                 std::map<TypeNode, int>& var_count)
+Node TermDbSygus::sygusToBuiltin(Node n, TypeNode tn)
 {
   Assert( n.getType()==tn );
-  Assert( tn.isDatatype() );
-
+  if (!tn.isDatatype())
+  {
+    return n;
+  }
   // has it already been computed?
-  if (var_count.empty() && n.hasAttribute(SygusToBuiltinAttribute()))
+  if (n.hasAttribute(SygusToBuiltinAttribute()))
   {
     return n.getAttribute(SygusToBuiltinAttribute());
   }
   Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n
                           << ", type = " << tn << std::endl;
   const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  if (!dt.isSygus())
+  {
+    return n;
+  }
   if (n.getKind() == APPLY_CONSTRUCTOR)
   {
-    bool var_count_empty = var_count.empty();
-    unsigned i = Datatype::indexOf(n.getOperator().toExpr());
+    unsigned i = datatypes::DatatypesRewriter::indexOf(n.getOperator());
     Assert(n.getNumChildren() == dt[i].getNumArgs());
     std::map<int, Node> pre;
     for (unsigned j = 0, size = n.getNumChildren(); j < size; j++)
     {
-      // if the child is a symbolic constructor, do not include it
-      if (!isSymbolicConsApp(n[j]))
-      {
-        pre[j] = sygusToBuiltin(
-            n[j], TypeNode::fromType(dt[i].getArgType(j)), var_count);
-      }
+      pre[j] = sygusToBuiltin(n[j], TypeNode::fromType(dt[i].getArgType(j)));
     }
-    Node ret = mkGeneric(dt, i, var_count, pre);
+    Node ret = mkGeneric(dt, i, pre);
     Trace("sygus-db-debug")
         << "SygusToBuiltin : Generic is " << ret << std::endl;
-    // cache if we had a fresh variable count
-    if (var_count_empty)
-    {
-      n.setAttribute(SygusToBuiltinAttribute(), ret);
-    }
+    // cache
+    n.setAttribute(SygusToBuiltinAttribute(), ret);
     return ret;
   }
   if (n.hasAttribute(SygusPrintProxyAttribute()))
@@ -259,20 +232,20 @@ Node TermDbSygus::sygusSubstituted( TypeNode tn, Node n, std::vector< Node >& ar
 }
 
 unsigned TermDbSygus::getSygusTermSize( Node n ){
-  if( n.getNumChildren()==0 ){
+  if (n.getKind() != APPLY_CONSTRUCTOR)
+  {
     return 0;
-  }else{
-    Assert(n.getKind() == APPLY_CONSTRUCTOR);
-    unsigned sum = 0;
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      sum += getSygusTermSize( n[i] );
-    }
-    const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
-    int cindex = Datatype::indexOf(n.getOperator().toExpr());
-    Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors());
-    unsigned weight = dt[cindex].getWeight();
-    return weight + sum;
   }
+  unsigned sum = 0;
+  for (unsigned i = 0; i < n.getNumChildren(); i++)
+  {
+    sum += getSygusTermSize(n[i]);
+  }
+  const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
+  int cindex = datatypes::DatatypesRewriter::indexOf(n.getOperator());
+  Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors());
+  unsigned weight = dt[cindex].getWeight();
+  return weight + sum;
 }
 
 class ReqTrie {
@@ -778,6 +751,7 @@ void TermDbSygus::registerSygusType( TypeNode tn ) {
           CVC4_CHECK(gtn.isSubtypeOf(btn))
               << "Sygus datatype " << dt.getName()
               << " encodes terms that are not of type " << btn << std::endl;
+          Trace("sygus-db") << "...done register Operator #" << i << std::endl;
         }
         // compute min type depth information
         computeMinTypeDepthInternal(tn, tn, 0);
@@ -817,6 +791,8 @@ void TermDbSygus::registerEnumerator(Node e,
     d_enum_to_active_guard[e] = eg;
   }
 
+  Trace("sygus-db") << "  registering symmetry breaking clauses..."
+                    << std::endl;
   d_enum_to_using_sym_cons[e] = useSymbolicCons;
   // depending on if we are using symbolic constructors, introduce symmetry
   // breaking lemma templates for each relevant subtype of the grammar
@@ -858,9 +834,12 @@ void TermDbSygus::registerEnumerator(Node e,
     for (unsigned& rindex : rm_indices)
     {
       // make the apply-constructor corresponding to an application of the
-      // "any constant" constructor
-      Node exc_val = nm->mkNode(APPLY_CONSTRUCTOR,
-                                Node::fromExpr(dt[rindex].getConstructor()));
+      // constant or "any constant" constructor
+      // we call getInstCons since in the case of any constant constructors, it
+      // is necessary to generate a term of the form any_constant( x.0 ) for a
+      // fresh variable x.0.
+      Node fv = getFreeVar(stn, 0);
+      Node exc_val = datatypes::DatatypesRewriter::getInstCons(fv, dt, rindex);
       // should not include the constuctor in any subterm
       Node x = getFreeVar(stn, 0);
       Trace("sygus-db") << "Construct symmetry breaking lemma from " << x
@@ -875,6 +854,7 @@ void TermDbSygus::registerEnumerator(Node e,
       registerSymBreakLemma(e, lem, stn, dt[rindex].getWeight());
     }
   }
+  Trace("sygus-db") << "  ...finished" << std::endl;
 }
 
 bool TermDbSygus::isEnumerator(Node e) const
@@ -991,8 +971,12 @@ TypeNode TermDbSygus::sygusToBuiltinType( TypeNode tn ) {
 void TermDbSygus::computeMinTypeDepthInternal( TypeNode root_tn, TypeNode tn, unsigned type_depth ) {
   std::map< TypeNode, unsigned >::iterator it = d_min_type_depth[root_tn].find( tn );
   if( it==d_min_type_depth[root_tn].end() || type_depth<it->second ){
+    if (!tn.isDatatype())
+    {
+      // do not recurse to non-datatype types
+      return;
+    }
     d_min_type_depth[root_tn][tn] = type_depth;
-    Assert( tn.isDatatype() );
     const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
     //compute for connected types
     for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
@@ -1232,9 +1216,10 @@ bool TermDbSygus::isSymbolicConsApp(Node n) const
     return false;
   }
   TypeNode tn = n.getType();
+  Assert(tn.isDatatype());
   const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
   Assert(dt.isSygus());
-  unsigned cindex = Datatype::indexOf(n.getOperator().toExpr());
+  unsigned cindex = datatypes::DatatypesRewriter::indexOf(n.getOperator());
   Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp());
   // it is symbolic if it represents "any constant"
   return sygusOp.getAttribute(SygusAnyConstAttribute());
@@ -1377,34 +1362,6 @@ void doStrReplace(std::string& str, const std::string& oldStr, const std::string
   }
 }
 
-Kind TermDbSygus::getOperatorKind( Node op ) {
-  Assert( op.getKind()!=BUILTIN );
-  if (op.getKind() == LAMBDA)
-  {
-    // we use APPLY_UF instead of APPLY, since the rewriter for APPLY_UF
-    // does beta-reduction but does not for APPLY
-    return APPLY_UF;
-  }else{
-    TypeNode tn = op.getType();
-    if( tn.isConstructor() ){
-      return APPLY_CONSTRUCTOR;
-    }
-    else if (tn.isSelector())
-    {
-      return APPLY_SELECTOR;
-    }
-    else if (tn.isTester())
-    {
-      return APPLY_TESTER;
-    }
-    else if (tn.isFunction())
-    {
-      return APPLY_UF;
-    }
-    return NodeManager::operatorToKind(op);
-  }
-}
-
 Node TermDbSygus::getAnchor( Node n ) {
   if( n.getKind()==APPLY_SELECTOR_TOTAL ){
     return getAnchor( n[0] );
@@ -1422,81 +1379,118 @@ unsigned TermDbSygus::getAnchorDepth( Node n ) {
 }
 
 Node TermDbSygus::unfold( Node en, std::map< Node, Node >& vtm, std::vector< Node >& exp, bool track_exp ) {
-  if( en.getKind()==kind::APPLY_UF ){
-    Trace("sygus-db-debug") << "Unfold : " << en << std::endl;
-    Node ev = en[0];
-    if( track_exp ){
-      std::map< Node, Node >::iterator itv = vtm.find( en[0] );
-      if( itv!=vtm.end() ){
-        ev = itv->second;
-      }else{
-        Assert( false );
-      }
-      Assert( en[0].getType()==ev.getType() );
-      Assert( ev.isConst() );
+  if (!datatypes::DatatypesRewriter::isSygusEvalApp(en))
+  {
+    Assert(en.isConst());
+    return en;
+  }
+  Trace("sygus-db-debug") << "Unfold : " << en << std::endl;
+  Node ev = en[0];
+  if (track_exp)
+  {
+    std::map<Node, Node>::iterator itv = vtm.find(en[0]);
+    Assert(itv != vtm.end());
+    if (itv != vtm.end())
+    {
+      ev = itv->second;
     }
-    Assert( ev.getKind()==kind::APPLY_CONSTRUCTOR );
-    std::vector< Node > args;
-    for( unsigned i=1; i<en.getNumChildren(); i++ ){
-      args.push_back( en[i] );
+    Assert(en[0].getType() == ev.getType());
+    Assert(ev.isConst());
+  }
+  Assert(ev.getKind() == kind::APPLY_CONSTRUCTOR);
+  std::vector<Node> args;
+  for (unsigned i = 1, nchild = en.getNumChildren(); i < nchild; i++)
+  {
+    args.push_back(en[i]);
+  }
+
+  Type headType = en[0].getType().toType();
+  NodeManager* nm = NodeManager::currentNM();
+  const Datatype& dt = static_cast<DatatypeType>(headType).getDatatype();
+  unsigned i = datatypes::DatatypesRewriter::indexOf(ev.getOperator());
+  if (track_exp)
+  {
+    // explanation
+    Node ee = nm->mkNode(
+        kind::APPLY_TESTER, Node::fromExpr(dt[i].getTester()), en[0]);
+    if (std::find(exp.begin(), exp.end(), ee) == exp.end())
+    {
+      exp.push_back(ee);
     }
-    const Datatype& dt = ((DatatypeType)(ev.getType()).toType()).getDatatype();
-    unsigned i = Datatype::indexOf( ev.getOperator().toExpr() );
-    if( track_exp ){
-      //explanation
-      Node ee = NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), en[0] );
-      if( std::find( exp.begin(), exp.end(), ee )==exp.end() ){
-        exp.push_back( ee );
-      }
+  }
+  // if we are a symbolic constructor, unfolding returns the subterm itself
+  Node sop = Node::fromExpr(dt[i].getSygusOp());
+  if (sop.getAttribute(SygusAnyConstAttribute()))
+  {
+    Trace("sygus-db-debug") << "...it is an any-constant constructor"
+                            << std::endl;
+    Assert(dt[i].getNumArgs() == 1);
+    if (en[0].getKind() == APPLY_CONSTRUCTOR)
+    {
+      return en[0][0];
     }
-    Assert( !dt.isParametric() );
-    std::map< int, Node > pre;
-    for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
-      std::vector< Node > cc;
-      //get the evaluation argument for the selector
-      Type rt = dt[i][j].getRangeType();
-      const Datatype & ad = ((DatatypeType)dt[i][j].getRangeType()).getDatatype();
-      cc.push_back( Node::fromExpr( ad.getSygusEvaluationFunc() ) );
-      Node s;
-      if( en[0].getKind()==kind::APPLY_CONSTRUCTOR ){
-        s = en[0][j];
-      }else{
-        s = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal( en[0].getType().toType(), j ), en[0] );
-      }
-      cc.push_back( s );
-      if( track_exp ){
-        //update vtm map
-        vtm[s] = ev[j];
-      }
-      cc.insert( cc.end(), args.begin(), args.end() );
-      pre[j] = NodeManager::currentNM()->mkNode( kind::APPLY_UF, cc );
+    else
+    {
+      return nm->mkNode(
+          APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headType, 0), en[0]);
     }
-    Node ret = mkGeneric(dt, i, pre);
-    // if it is a variable, apply the substitution
-    if( ret.getKind()==kind::BOUND_VARIABLE ){
-      Assert( ret.hasAttribute(SygusVarNumAttribute()) );
-      int i = ret.getAttribute(SygusVarNumAttribute());
-      Assert( Node::fromExpr( dt.getSygusVarList() )[i]==ret );
-      ret = args[i];
+  }
+
+  Assert(!dt.isParametric());
+  std::map<int, Node> pre;
+  for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
+  {
+    std::vector<Node> cc;
+    Node s;
+    // get the j^th subfield of en
+    if (en[0].getKind() == kind::APPLY_CONSTRUCTOR)
+    {
+      // if it is a concrete constructor application, as an optimization,
+      // just return the argument
+      s = en[0][j];
     }
     else
     {
-      ret = Rewriter::rewrite(ret);
+      s = nm->mkNode(kind::APPLY_SELECTOR_TOTAL,
+                     dt[i].getSelectorInternal(headType, j),
+                     en[0]);
     }
-    return ret;
-  }else{
-    Assert( en.isConst() );
+    cc.push_back(s);
+    if (track_exp)
+    {
+      // update vtm map
+      vtm[s] = ev[j];
+    }
+    cc.insert(cc.end(), args.begin(), args.end());
+    pre[j] = datatypes::DatatypesRewriter::mkSygusEvalApp(cc);
+  }
+  Node ret = mkGeneric(dt, i, pre);
+  // if it is a variable, apply the substitution
+  if (ret.getKind() == kind::BOUND_VARIABLE)
+  {
+    Assert(ret.hasAttribute(SygusVarNumAttribute()));
+    int i = ret.getAttribute(SygusVarNumAttribute());
+    Assert(Node::fromExpr(dt.getSygusVarList())[i] == ret);
+    return args[i];
   }
-  return en;
+  ret = Rewriter::rewrite(ret);
+  return ret;
 }
 
+Node TermDbSygus::unfold(Node en)
+{
+  std::map<Node, Node> vtm;
+  std::vector<Node> exp;
+  return unfold(en, vtm, exp, false);
+}
 
 Node TermDbSygus::getEagerUnfold( Node n, std::map< Node, Node >& visited ) {
   std::map< Node, Node >::iterator itv = visited.find( n );
   if( itv==visited.end() ){
     Trace("cegqi-eager-debug") << "getEagerUnfold " << n << std::endl;
     Node ret;
-    if( n.getKind()==APPLY_UF ){
+    if (datatypes::DatatypesRewriter::isSygusEvalApp(n))
+    {
       TypeNode tn = n[0].getType();
       Trace("cegqi-eager-debug") << "check " << n[0].getType() << std::endl;
       if( tn.isDatatype() ){
@@ -1573,7 +1567,9 @@ Node TermDbSygus::evaluateWithUnfolding(
       visited.find(n);
   if( it==visited.end() ){
     Node ret = n;
-    while( ret.getKind()==APPLY_UF && ret[0].getKind()==APPLY_CONSTRUCTOR ){
+    while (datatypes::DatatypesRewriter::isSygusEvalApp(ret)
+           && ret[0].getKind() == APPLY_CONSTRUCTOR)
+    {
       ret = unfold( ret );
     }    
     if( ret.getNumChildren()>0 ){
@@ -1606,7 +1602,11 @@ Node TermDbSygus::evaluateWithUnfolding( Node n ) {
 
 bool TermDbSygus::isEvaluationPoint(Node n) const
 {
-  if (n.getKind() != APPLY_UF || n.getNumChildren() == 0 || !n[0].isVar())
+  if (!datatypes::DatatypesRewriter::isSygusEvalApp(n))
+  {
+    return false;
+  }
+  if (!n[0].isVar())
   {
     return false;
   }
@@ -1617,18 +1617,7 @@ bool TermDbSygus::isEvaluationPoint(Node n) const
       return false;
     }
   }
-  TypeNode tn = n[0].getType();
-  if (!tn.isDatatype())
-  {
-    return false;
-  }
-  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
-  if (!dt.isSygus())
-  {
-    return false;
-  }
-  Node eval_op = Node::fromExpr(dt.getSygusEvaluationFunc());
-  return eval_op == n.getOperator();
+  return true;
 }
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 163d65d19..c4a035e2c 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -172,13 +172,8 @@ class TermDbSygus {
    *
    * Given a sygus datatype term n of type tn, this function returns its analog,
    * that is, the term that n encodes.
-   *
-   * Notice that each occurrence of a symbolic constructor application is
-   * replaced by a unique variable. To track counters for introducing unique
-   * variables, we use the var_count map.
    */
   Node sygusToBuiltin(Node n, TypeNode tn);
-  Node sygusToBuiltin(Node n, TypeNode tn, std::map<TypeNode, int>& var_count);
   /** same as above, but without tn */
   Node sygusToBuiltin(Node n) { return sygusToBuiltin(n, n.getType()); }
   /** evaluate builtin
@@ -385,10 +380,6 @@ class TermDbSygus {
   Node getSemanticSkolem( TypeNode tn, Node n, bool doMk = true );
   /** involves div-by-zero */
   bool involvesDivByZero( Node n );
-  
-  /** get operator kind */
-  static Kind getOperatorKind( Node op );
-
   /** get anchor */
   static Node getAnchor( Node n );
   static unsigned getAnchorDepth( Node n );
@@ -398,13 +389,32 @@ public: // for symmetry breaking
   bool considerConst( TypeNode tn, TypeNode tnp, Node c, Kind pk, int arg );
   bool considerConst( const Datatype& pdt, TypeNode tnp, Node c, Kind pk, int arg );
   int solveForArgument( TypeNode tnp, unsigned cindex, unsigned arg );
-public:
-  Node unfold( Node en, std::map< Node, Node >& vtm, std::vector< Node >& exp, bool track_exp = true );
-  Node unfold( Node en ){
-    std::map< Node, Node > vtm;
-    std::vector< Node > exp;
-    return unfold( en, vtm, exp, false );
-  }
+
+ public:
+  /** unfold
+   *
+   * This method returns the one-step unfolding of an evaluation function
+   * application. An example of a one step unfolding is:
+   *    eval( C_+( d1, d2 ), t ) ---> +( eval( d1, t ), eval( d2, t ) )
+   *
+   * This function does this unfolding for a (possibly symbolic) evaluation
+   * head, where the argument "variable to model" vtm stores the model value of
+   * variables from this head. This allows us to track an explanation of the
+   * unfolding in the vector exp when track_exp is true.
+   *
+   * For example, if vtm[d] = C_+( C_x(), C_0() ) and track_exp is true, then
+   * this method applied to eval( d, t ) will return
+   * +( eval( d.0, t ), eval( d.1, t ) ), and is-C_+( d ) is added to exp.
+   */
+  Node unfold(Node en,
+              std::map<Node, Node>& vtm,
+              std::vector<Node>& exp,
+              bool track_exp = true);
+  /**
+   * Same as above, but without explanation tracking. This is used for concrete
+   * evaluation heads
+   */
+  Node unfold(Node en);
   Node getEagerUnfold( Node n, std::map< Node, Node >& visited );
 };
 
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index fb4f7e831..c1daa9288 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -605,9 +605,15 @@ Node SygusSampler::getSygusRandomValue(TypeNode tn,
                                        double rinc,
                                        unsigned depth)
 {
-  Assert(tn.isDatatype());
+  if (!tn.isDatatype())
+  {
+    return getRandomValue(tn);
+  }
   const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
-  Assert(dt.isSygus());
+  if (!dt.isSygus())
+  {
+    return getRandomValue(tn);
+  }
   Assert(d_rvalue_cindices.find(tn) != d_rvalue_cindices.end());
   Trace("sygus-sample-grammar")
       << "Sygus random value " << tn << ", depth = " << depth
@@ -671,9 +677,15 @@ void SygusSampler::registerSygusType(TypeNode tn)
   if (d_rvalue_cindices.find(tn) == d_rvalue_cindices.end())
   {
     d_rvalue_cindices[tn].clear();
-    Assert(tn.isDatatype());
+    if (!tn.isDatatype())
+    {
+      return;
+    }
     const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
-    Assert(dt.isSygus());
+    if (!dt.isSygus())
+    {
+      return;
+    }
     for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
     {
       const DatatypeConstructor& dtc = dt[i];
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index 70f8bbcee..2880713af 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -76,10 +76,6 @@ typedef expr::Attribute<AbsTypeFunDefAttributeId, bool> AbsTypeFunDefAttribute;
 struct QuantIdNumAttributeId {};
 typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute;
 
-/** sygus var num */
-struct SygusVarNumAttributeId {};
-typedef expr::Attribute<SygusVarNumAttributeId, uint64_t> SygusVarNumAttribute;
-
 /** Attribute to mark Skolems as virtual terms */
 struct VirtualTermSkolemAttributeId {};
 typedef expr::Attribute< VirtualTermSkolemAttributeId, bool > VirtualTermSkolemAttribute;