Builtin evaluation functions for sygus (#1991)

17 files changed, 405 insertions, 362 deletions

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;