Sygus type info class (#3187)

11 files changed, 984 insertions, 691 deletions

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 334b3d638..cf05a6029 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -244,9 +244,10 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std:
   
   if( options::sygusFair()==SYGUS_FAIR_DIRECT ){
     if( dt[tindex].getNumArgs()>0 ){
+      quantifiers::SygusTypeInfo& nti = d_tds->getTypeInfo(ntn);
       // consider lower bounds for size of types
-      unsigned lb_add = d_tds->getMinConsTermSize( ntn, tindex );
-      unsigned lb_rem = n==a ? 0 : d_tds->getMinTermSize( ntn );
+      unsigned lb_add = nti.getMinConsTermSize(tindex);
+      unsigned lb_rem = n == a ? 0 : nti.getMinTermSize();
       Assert( lb_add>=lb_rem );
       d_currTermSize[a].set( d_currTermSize[a].get() + ( lb_add - lb_rem ) );
     }
@@ -558,10 +559,11 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e,
       << "Simple symmetry breaking for " << dt.getName() << ", constructor "
       << dt[tindex].getName() << ", at depth " << depth << std::endl;
 
+  quantifiers::SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
   // get the sygus operator
   Node sop = Node::fromExpr(dt[tindex].getSygusOp());
   // get the kind of the constructor operator
-  Kind nk = d_tds->getConsNumKind(tn, tindex);
+  Kind nk = ti.getConsNumKind(tindex);
   // is this the any-constant constructor?
   bool isAnyConstant = sop.getAttribute(SygusAnyConstAttribute());
 
@@ -621,8 +623,9 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e,
       // for each variable in the sygus type
       for (const Node& var : svl)
       {
-        unsigned sc = d_tds->getSubclassForVar(etn, var);
-        if (d_tds->getNumSubclassVars(etn, sc) == 1)
+        quantifiers::SygusTypeInfo& eti = d_tds->getTypeInfo(etn);
+        unsigned sc = eti.getSubclassForVar(var);
+        if (eti.getNumSubclassVars(sc) == 1)
         {
           // unique variable in singleton subclass, skip
           continue;
@@ -630,11 +633,11 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e,
         // Compute the "predecessor" variable in the subclass of var.
         Node predVar;
         unsigned scindex = 0;
-        if (d_tds->getIndexInSubclassForVar(etn, var, scindex))
+        if (eti.getIndexInSubclassForVar(var, scindex))
         {
           if (scindex > 0)
           {
-            predVar = d_tds->getVarSubclassIndex(etn, sc, scindex - 1);
+            predVar = eti.getVarSubclassIndex(sc, scindex - 1);
           }
         }
         Node preParentOp = getTraversalPredicate(tn, var, true);
@@ -656,7 +659,7 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e,
         Node finish = nm->mkNode(APPLY_UF, postParent, n);
         // check if we are constructing the symmetry breaking predicate for the
         // variable in question. If so, is-{x_i}( z ) is true.
-        int varCn = d_tds->getOpConsNum(tn, var);
+        int varCn = ti.getOpConsNum(var);
         if (varCn == static_cast<int>(tindex))
         {
           // the post value is true
@@ -749,7 +752,7 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e,
             // cannot do division since we have to consider when both are zero
             if (!req_const.isNull())
             {
-              if (d_tds->hasConst(tn, req_const))
+              if (ti.hasConst(req_const))
               {
                 argDeq = true;
               }
@@ -806,7 +809,7 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e,
         bool exp_not_all_const_valid = dt_index_nargs > 0;
         // does the parent have an any constant constructor?
         bool usingAnyConstCons =
-            usingSymCons && (d_tds->getAnyConstantConsNum(tn) != -1);
+            usingSymCons && (ti.getAnyConstantConsNum() != -1);
         for (unsigned j = 0; j < dt_index_nargs; j++)
         {
           Node nc = children[j];
@@ -816,13 +819,14 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e,
             continue;
           }
           TypeNode tnc = nc.getType();
-          int anyc_cons_num = d_tds->getAnyConstantConsNum(tnc);
+          quantifiers::SygusTypeInfo& cti = d_tds->getTypeInfo(tnc);
+          int anyc_cons_num = cti.getAnyConstantConsNum();
           const Datatype& cdt =
               static_cast<DatatypeType>(tnc.toType()).getDatatype();
           std::vector<Node> exp_const;
           for (unsigned k = 0, ncons = cdt.getNumConstructors(); k < ncons; k++)
           {
-            Kind nck = d_tds->getConsNumKind(tnc, k);
+            Kind nck = cti.getConsNumKind(k);
             bool red = false;
             Node tester = DatatypesRewriter::mkTester(nc, k, cdt);
             // check if the argument is redundant
@@ -838,7 +842,7 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e,
             }
             else
             {
-              Node cc = d_tds->getConsNumConst(tnc, k);
+              Node cc = cti.getConsNumConst(k);
               if (!cc.isNull())
               {
                 Trace("sygus-sb-simple-debug")
@@ -1355,11 +1359,12 @@ void SygusSymBreakNew::registerSizeTerm(Node e, std::vector<Node>& lemmas)
     // variables occur pre-traversal at top-level
     Node varList = Node::fromExpr(dt.getSygusVarList());
     std::vector<Node> constraints;
+    quantifiers::SygusTypeInfo& eti = d_tds->getTypeInfo(etn);
     for (const Node& v : varList)
     {
-      unsigned sc = d_tds->getSubclassForVar(etn, v);
+      unsigned sc = eti.getSubclassForVar(v);
       // no symmetry breaking occurs for variables in singleton subclasses
-      if (d_tds->getNumSubclassVars(etn, sc) > 1)
+      if (eti.getNumSubclassVars(sc) > 1)
       {
         Node preRootOp = getTraversalPredicate(etn, v, true);
         Node preRoot = nm->mkNode(APPLY_UF, preRootOp, e);
diff --git a/src/theory/datatypes/sygus_simple_sym.cpp b/src/theory/datatypes/sygus_simple_sym.cpp
index fb8bd7515..f1e8949af 100644
--- a/src/theory/datatypes/sygus_simple_sym.cpp
+++ b/src/theory/datatypes/sygus_simple_sym.cpp
@@ -95,7 +95,8 @@ class ReqTrie
   {
     if (!d_req_const.isNull())
     {
-      if (!tdb->hasConst(tn, d_req_const))
+      quantifiers::SygusTypeInfo& sti = tdb->getTypeInfo(tn);
+      if (!sti.hasConst(d_req_const))
       {
         return false;
       }
@@ -154,13 +155,15 @@ bool SygusSimpleSymBreak::considerArgKind(
 {
   const Datatype& pdt = ((DatatypeType)(tnp).toType()).getDatatype();
   const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-  Assert(d_tds->hasKind(tn, k));
-  Assert(d_tds->hasKind(tnp, pk));
+  quantifiers::SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
+  quantifiers::SygusTypeInfo& pti = d_tds->getTypeInfo(tnp);
+  Assert(ti.hasKind(k));
+  Assert(pti.hasKind(pk));
   Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk
                           << ", arg = " << arg << " in " << tnp << "?"
                           << std::endl;
-  int c = d_tds->getKindConsNum(tn, k);
-  int pc = d_tds->getKindConsNum(tnp, pk);
+  int c = ti.getKindConsNum(k);
+  int pc = pti.getKindConsNum(pk);
   // check for associativity
   if (k == pk && quantifiers::TermUtil::isAssoc(k))
   {
@@ -294,7 +297,7 @@ bool SygusSimpleSymBreak::considerArgKind(
       }
       if (!rt.empty() && (reqk != UNDEFINED_KIND || !reqkc.empty()))
       {
-        int pcr = d_tds->getKindConsNum(tnp, rt.d_req_kind);
+        int pcr = pti.getKindConsNum(rt.d_req_kind);
         if (pcr != -1)
         {
           Assert(pcr < static_cast<int>(pdt.getNumConstructors()));
@@ -429,7 +432,9 @@ bool SygusSimpleSymBreak::considerConst(
     return false;
   }
   // this can probably be made child grammar independent
-  int pc = d_tds->getKindConsNum(tnp, pk);
+  quantifiers::SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
+  quantifiers::SygusTypeInfo& pti = d_tds->getTypeInfo(tnp);
+  int pc = pti.getKindConsNum(pk);
   if (pdt[pc].getNumArgs() == 2)
   {
     Kind ok;
@@ -438,7 +443,7 @@ bool SygusSimpleSymBreak::considerConst(
     {
       Trace("sygus-sb-simple-debug")
           << pk << " has offset arg " << ok << " " << offset << std::endl;
-      int ok_arg = d_tds->getKindConsNum(tnp, ok);
+      int ok_arg = pti.getKindConsNum(ok);
       if (ok_arg != -1)
       {
         Trace("sygus-sb-simple-debug")
@@ -453,7 +458,7 @@ bool SygusSimpleSymBreak::considerConst(
               << ", status=" << status << std::endl;
           if (status == 0 && !co.isNull())
           {
-            if (d_tds->hasConst(tn, co))
+            if (ti.hasConst(co))
             {
               Trace("sygus-sb-simple")
                   << "  sb-simple : by offset reasoning, do not consider const "
@@ -474,8 +479,9 @@ bool SygusSimpleSymBreak::considerConst(
 bool SygusSimpleSymBreak::considerConst(
     const Datatype& pdt, TypeNode tnp, Node c, Kind pk, int arg)
 {
-  Assert(d_tds->hasKind(tnp, pk));
-  int pc = d_tds->getKindConsNum(tnp, pk);
+  quantifiers::SygusTypeInfo& pti = d_tds->getTypeInfo(tnp);
+  Assert(pti.hasKind(pk));
+  int pc = pti.getKindConsNum(pk);
   bool ret = true;
   Trace("sygus-sb-debug") << "Consider sygus const " << c << ", parent = " << pk
                           << ", arg = " << arg << "?" << std::endl;
@@ -499,7 +505,7 @@ bool SygusSimpleSymBreak::considerConst(
     Node sc = d_tutil->isSingularArg(c, pk, arg);
     if (!sc.isNull())
     {
-      if (d_tds->hasConst(tnp, sc))
+      if (pti.hasConst(sc))
       {
         Trace("sygus-sb-simple")
             << "  sb-simple : " << c << " is singular arg " << arg << " of "
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 fea2ce15a..d349e8ad4 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -225,7 +225,9 @@ int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status)
     d_rcons_to_status[stn][t] = -1;
     TypeNode tn = t.getType();
     Assert( stn.isDatatype() );
-    const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
+    const Datatype& dt = stn.getDatatype();
+    TermDbSygus* tds = d_qe->getTermDatabaseSygus();
+    SygusTypeInfo& sti = tds->getTypeInfo(stn);
     Assert( dt.isSygus() );
     Trace("csi-rcons-debug") << "Check reconstruct " << t << ", sygus type " << dt.getName() << ", kind " << t.getKind() << ", id : " << id << std::endl;
     int carg = -1;
@@ -234,14 +236,15 @@ int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status)
     Node min_t = minimizeBuiltinTerm(t);
     Trace("csi-rcons-debug") << "Minimized term is : " << min_t << std::endl;
     //check if op is in syntax sort
-    carg = d_qe->getTermDatabaseSygus()->getOpConsNum( stn, min_t );
+
+    carg = sti.getOpConsNum(min_t);
     if( carg!=-1 ){
       Trace("csi-rcons-debug") << "  Type has operator." << std::endl;
       d_reconstruct[id] = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, Node::fromExpr( dt[carg].getConstructor() ) );
       status = 0;
     }else{
       //check if kind is in syntax sort
-      karg = d_qe->getTermDatabaseSygus()->getKindConsNum( stn, min_t.getKind() );
+      karg = sti.getKindConsNum(min_t.getKind());
       if( karg!=-1 ){
         //collect the children of min_t
         std::vector< Node > tchildren;
@@ -374,7 +377,7 @@ int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status)
                 }
                 //get decompositions
                 for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-                  Kind k = d_qe->getTermDatabaseSygus()->getConsNumKind( stn, i );
+                  Kind k = sti.getConsNumKind(i);
                   getEquivalentTerms( k, min_t, equiv );
                 }
                 //assign ids to terms
@@ -683,6 +686,7 @@ Node CegSingleInvSol::builtinToSygusConst(Node c, TypeNode tn, int rcons_depth)
   }
   TermDbSygus* tds = d_qe->getTermDatabaseSygus();
   NodeManager* nm = NodeManager::currentNM();
+  SygusTypeInfo& ti = tds->getTypeInfo(tn);
   Node sc;
   d_builtin_const_to_sygus[tn][c] = sc;
   Assert(c.isConst());
@@ -709,7 +713,7 @@ Node CegSingleInvSol::builtinToSygusConst(Node c, TypeNode tn, int rcons_depth)
   }
   else
   {
-    int carg = tds->getOpConsNum(tn, c);
+    int carg = ti.getOpConsNum(c);
     if (carg != -1)
     {
       sc = nm->mkNode(APPLY_CONSTRUCTOR,
@@ -743,7 +747,7 @@ Node CegSingleInvSol::builtinToSygusConst(Node c, TypeNode tn, int rcons_depth)
           Kind pk = getPlusKind(TypeNode::fromType(dt.getSygusType()));
           if (pk != UNDEFINED_KIND)
           {
-            int arg = tds->getKindConsNum(tn, pk);
+            int arg = ti.getKindConsNum(pk);
             if (arg != -1)
             {
               Kind ck =
@@ -815,7 +819,8 @@ void CegSingleInvSol::registerType(TypeNode tn)
   TermDbSygus* tds = d_qe->getTermDatabaseSygus();
   // ensure it is registered
   tds->registerSygusType(tn);
-  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  const Datatype& dt = tn.getDatatype();
+  Assert(dt.isSygus());
   TypeNode btn = TypeNode::fromType(dt.getSygusType());
   // for constant reconstruction
   Kind ck = getComparisonKind(btn);
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 1e8012697..c319d7a37 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -85,7 +85,8 @@ bool Cegis::processInitialize(Node conj,
     {
       TypeNode ctn = candidates[i].getType();
       d_tds->registerSygusType(ctn);
-      if (d_tds->hasSubtermSymbolicCons(ctn))
+      SygusTypeInfo& cti = d_tds->getTypeInfo(ctn);
+      if (cti.hasSubtermSymbolicCons())
       {
         do_repair_const = true;
         // remember that we are doing grammar-based repair
diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
index b568b8f53..0cdfe4307 100644
--- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
@@ -48,8 +48,9 @@ void EnumStreamPermutation::reset(Node value)
   Node var_list = Node::fromExpr(tn.getDatatype().getSygusVarList());
   NodeManager* nm = NodeManager::currentNM();
   // get subtypes in value's type
+  SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
   std::vector<TypeNode> sf_types;
-  d_tds->getSubfieldTypes(tn, sf_types);
+  ti.getSubfieldTypes(sf_types);
   // associate variables with constructors in all subfield types
   std::map<Node, Node> cons_var;
   for (const Node& v : var_list)
@@ -84,7 +85,7 @@ void EnumStreamPermutation::reset(Node value)
     if (seen_vars.insert(var).second)
     {
       // do not add repeated vars
-      d_var_classes[d_tds->getSubclassForVar(tn, var)].push_back(var);
+      d_var_classes[ti.getSubclassForVar(var)].push_back(var);
     }
   }
   for (const std::pair<unsigned, std::vector<Node>>& p : d_var_classes)
@@ -339,8 +340,9 @@ void EnumStreamSubstitution::initialize(TypeNode tn)
   Node var_list = Node::fromExpr(tn.getDatatype().getSygusVarList());
   // get subtypes in value's type
   NodeManager* nm = NodeManager::currentNM();
+  SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
   std::vector<TypeNode> sf_types;
-  d_tds->getSubfieldTypes(tn, sf_types);
+  ti.getSubfieldTypes(sf_types);
   // associate variables with constructors in all subfield types
   for (const Node& v : var_list)
   {
@@ -361,8 +363,8 @@ void EnumStreamSubstitution::initialize(TypeNode tn)
   // split initial variables into classes
   for (const Node& v : var_list)
   {
-    Assert(d_tds->getSubclassForVar(tn, v) > 0);
-    d_var_classes[d_tds->getSubclassForVar(tn, v)].push_back(v);
+    Assert(ti.getSubclassForVar(v) > 0);
+    d_var_classes[ti.getSubclassForVar(v)].push_back(v);
   }
 }
 
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 208c8b9a0..ed3eec145 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -31,33 +31,6 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-void TypeNodeIdTrie::add(Node v, std::vector<TypeNode>& types)
-{
-  TypeNodeIdTrie* tnt = this;
-  for (unsigned i = 0, size = types.size(); i < size; i++)
-  {
-    tnt = &tnt->d_children[types[i]];
-  }
-  tnt->d_data.push_back(v);
-}
-
-void TypeNodeIdTrie::assignIds(std::map<Node, unsigned>& assign,
-                               unsigned& idCount)
-{
-  if (!d_data.empty())
-  {
-    for (const Node& v : d_data)
-    {
-      assign[v] = idCount;
-    }
-    idCount++;
-  }
-  for (std::pair<const TypeNode, TypeNodeIdTrie>& c : d_children)
-  {
-    c.second.assignIds(assign, idCount);
-  }
-}
-
 std::ostream& operator<<(std::ostream& os, EnumeratorRole r)
 {
   switch (r)
@@ -159,7 +132,8 @@ Node TermDbSygus::getProxyVariable(TypeNode tn, Node c)
   std::map<Node, Node>::iterator it = d_proxy_vars[tn].find(c);
   if (it == d_proxy_vars[tn].end())
   {
-    int anyC = getAnyConstantConsNum(tn);
+    SygusTypeInfo& ti = getTypeInfo(tn);
+    int anyC = ti.getAnyConstantConsNum();
     Node k;
     if (anyC == -1)
     {
@@ -340,11 +314,6 @@ Node TermDbSygus::sygusToBuiltin(Node n, TypeNode tn)
   return ret;
 }
 
-Node TermDbSygus::sygusSubstituted( TypeNode tn, Node n, std::vector< Node >& args ) {
-  Assert( d_var_list[tn].size()==args.size() );
-  return n.substitute( d_var_list[tn].begin(), d_var_list[tn].end(), args.begin(), args.end() );
-}
-
 unsigned TermDbSygus::getSygusTermSize( Node n ){
   if (n.getKind() != APPLY_CONSTRUCTOR)
   {
@@ -362,116 +331,29 @@ unsigned TermDbSygus::getSygusTermSize( Node n ){
   return weight + sum;
 }
 
-void TermDbSygus::registerSygusType( TypeNode tn ) {
-  std::map< TypeNode, TypeNode >::iterator itr = d_register.find( tn );
-  if( itr==d_register.end() ){
-    d_register[tn] = TypeNode::null();
-    if( tn.isDatatype() ){
-      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-      Trace("sygus-db") << "Register type " << dt.getName() << "..." << std::endl;
-      TypeNode btn = TypeNode::fromType( dt.getSygusType() );
-      d_register[tn] = btn;
-      if( !d_register[tn].isNull() ){
-        // get the sygus variable list
-        Node var_list = Node::fromExpr( dt.getSygusVarList() );
-        if( !var_list.isNull() ){
-          for( unsigned j=0; j<var_list.getNumChildren(); j++ ){
-            Node sv = var_list[j];
-            SygusVarNumAttribute svna;
-            sv.setAttribute( svna, j );
-            d_var_list[tn].push_back( sv );
-          }
-        }else{
-          // no arguments to synthesis functions
-          d_var_list[tn].clear();
-        }
-        // register connected types
-        for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
-        {
-          for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
-          {
-            TypeNode ctn = TypeNode::fromType(dt[i].getArgType(j));
-            registerSygusType(ctn);
-            // carry type attributes
-            if (d_has_subterm_sym_cons.find(ctn)
-                != d_has_subterm_sym_cons.end())
-            {
-              d_has_subterm_sym_cons[tn] = true;
-            }
-          }
-        }
-        //iterate over constructors
-        for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-          Expr sop = dt[i].getSygusOp();
-          Assert( !sop.isNull() );
-          Node n = Node::fromExpr( sop );
-          Trace("sygus-db") << "  Operator #" << i << " : " << sop;
-          if( sop.getKind() == kind::BUILTIN ){
-            Kind sk = NodeManager::operatorToKind( n );
-            Trace("sygus-db") << ", kind = " << sk;
-            d_kinds[tn][sk] = i;
-            d_arg_kind[tn][i] = sk;
-            if (sk == ITE)
-            {
-              // mark that this type has an ITE
-              d_hasIte[tn] = true;
-            }
-          }
-          else if (sop.isConst() && dt[i].getNumArgs() == 0)
-          {
-            Trace("sygus-db") << ", constant";
-            d_consts[tn][n] = i;
-            d_arg_const[tn][i] = n;
-          }
-          else if (sop.getKind() == LAMBDA)
-          {
-            // do type checking
-            Assert(sop[0].getNumChildren() == dt[i].getNumArgs());
-            for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
-            {
-              TypeNode ct = TypeNode::fromType(dt[i].getArgType(j));
-              TypeNode cbt = sygusToBuiltinType(ct);
-              TypeNode lat = TypeNode::fromType(sop[0][j].getType());
-              CVC4_CHECK(cbt.isSubtypeOf(lat))
-                  << "In sygus datatype " << dt.getName()
-                  << ", argument to a lambda constructor is not " << lat
-                  << std::endl;
-            }
-            if (sop[0].getKind() == ITE)
-            {
-              // mark that this type has an ITE
-              d_hasIte[tn] = true;
-            }
-          }
-          // symbolic constructors
-          if (n.getAttribute(SygusAnyConstAttribute()))
-          {
-            d_sym_cons_any_constant[tn] = i;
-            d_has_subterm_sym_cons[tn] = true;
-          }
-          // TODO (as part of #1170): we still do not properly catch type
-          // errors in sygus grammars for arguments of builtin operators.
-          // The challenge is that we easily ask for expected argument types of
-          // builtin operators e.g. PLUS. Hence the call to mkGeneric below
-          // will throw a type exception.
-          d_ops[tn][n] = i;
-          d_arg_ops[tn][i] = n;
-          Trace("sygus-db") << std::endl;
-          // ensure that terms that this constructor encodes are
-          // of the type specified in the datatype. This will fail if
-          // e.g. bitvector-and is a constructor of an integer grammar.
-          Node g = mkGeneric(dt, i);
-          TypeNode gtn = g.getType();
-          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);
-      }
-    }
+bool TermDbSygus::registerSygusType(TypeNode tn)
+{
+  std::map<TypeNode, bool>::iterator it = d_registerStatus.find(tn);
+  if (it != d_registerStatus.end())
+  {
+    // already registered
+    return it->second;
+  }
+  d_registerStatus[tn] = false;
+  // it must be a sygus datatype
+  if (!tn.isDatatype())
+  {
+    return false;
   }
+  const Datatype& dt = tn.getDatatype();
+  if (!dt.isSygus())
+  {
+    return false;
+  }
+  d_registerStatus[tn] = true;
+  SygusTypeInfo& sti = d_tinfo[tn];
+  sti.initialize(this, tn);
+  return true;
 }
 
 void TermDbSygus::registerEnumerator(Node e,
@@ -498,36 +380,24 @@ void TermDbSygus::registerEnumerator(Node e,
   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
+  SygusTypeInfo& eti = getTypeInfo(et);
   std::vector<TypeNode> sf_types;
-  getSubfieldTypes(et, sf_types);
-  // maps variables to the list of subfield types they occur in
-  std::map<Node, std::vector<TypeNode> > type_occurs;
-  std::map<TypeNode, std::vector<Node> >::iterator itv = d_var_list.find(et);
-  Assert(itv != d_var_list.end());
-  for (const Node& v : itv->second)
-  {
-    type_occurs[v].clear();
-  }
+  eti.getSubfieldTypes(sf_types);
   // for each type of subfield type of this enumerator
   for (unsigned i = 0, ntypes = sf_types.size(); i < ntypes; i++)
   {
     std::vector<unsigned> rm_indices;
     TypeNode stn = sf_types[i];
     Assert(stn.isDatatype());
+    SygusTypeInfo& sti = getTypeInfo(stn);
     const Datatype& dt = stn.getDatatype();
-    int anyC = getAnyConstantConsNum(stn);
+    int anyC = sti.getAnyConstantConsNum();
     for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
     {
       Expr sop = dt[i].getSygusOp();
       Assert(!sop.isNull());
       bool isAnyC = static_cast<int>(i) == anyC;
-      Node sopn = Node::fromExpr(sop);
-      if (type_occurs.find(sopn) != type_occurs.end())
-      {
-        // if it is a variable, store that it occurs in stn
-        type_occurs[sopn].push_back(stn);
-      }
-      else if (isAnyC && !useSymbolicCons)
+      if (isAnyC && !useSymbolicCons)
       {
         // if we are not using the any constant constructor
         // do not use the symbolic constructor
@@ -537,7 +407,7 @@ void TermDbSygus::registerEnumerator(Node e,
       {
         // if we are using the any constant constructor, do not use any
         // concrete constant
-        Node c_op = getConsNumConst(stn, i);
+        Node c_op = sti.getConsNumConst(i);
         if (!c_op.isNull())
         {
           rm_indices.push_back(i);
@@ -612,7 +482,7 @@ void TermDbSygus::registerEnumerator(Node e,
         // solution" clauses.
         const Datatype& dt = et.getDatatype();
         if (options::sygusStream()
-            || (!hasIte(et) && !dt.getSygusType().isBoolean()))
+            || (!eti.hasIte() && !dt.getSygusType().isBoolean()))
         {
           isActiveGen = true;
         }
@@ -637,39 +507,11 @@ void TermDbSygus::registerEnumerator(Node e,
   d_enum_var_agnostic[e] = isVarAgnostic;
   if (isVarAgnostic)
   {
-    // if not done so already, compute type class identifiers for each variable
-    if (d_var_subclass_id.find(et) == d_var_subclass_id.end())
-    {
-      d_var_subclass_id[et].clear();
-      TypeNodeIdTrie tnit;
-      for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs)
-      {
-        tnit.add(to.first, to.second);
-      }
-      // 0 is reserved for "no type class id"
-      unsigned typeIdCount = 1;
-      tnit.assignIds(d_var_subclass_id[et], typeIdCount);
-      // assign the list and reverse map to index
-      for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs)
-      {
-        Node v = to.first;
-        unsigned sc = d_var_subclass_id[et][v];
-        Trace("sygus-db") << v << " has subclass id " << sc << std::endl;
-        d_var_subclass_list_index[et][v] = d_var_subclass_list[et][sc].size();
-        d_var_subclass_list[et][sc].push_back(v);
-      }
-    }
+    // requires variable subclasses
+    eti.initializeVarSubclasses();
     // If no subclass has more than one variable, do not use variable agnostic
     // enumeration
-    bool useVarAgnostic = false;
-    for (std::pair<const unsigned, std::vector<Node> >& p :
-         d_var_subclass_list[et])
-    {
-      if (p.second.size() > 1)
-      {
-        useVarAgnostic = true;
-      }
-    }
+    bool useVarAgnostic = !eti.isSubclassVarTrivial();
     if (!useVarAgnostic)
     {
       Trace("sygus-db")
@@ -841,12 +683,13 @@ void TermDbSygus::clearSymBreakLemmas(Node e) { d_enum_to_sb_lemmas.erase(e); }
 
 bool TermDbSygus::isRegistered(TypeNode tn) const
 {
-  return d_register.find( tn )!=d_register.end();
+  return d_tinfo.find(tn) != d_tinfo.end();
 }
 
 TypeNode TermDbSygus::sygusToBuiltinType( TypeNode tn ) {
-  Assert( isRegistered( tn ) );
-  return d_register[tn];
+  std::map<TypeNode, SygusTypeInfo>::iterator it = d_tinfo.find(tn);
+  Assert(it != d_tinfo.end());
+  return it->second.getBuiltinType();
 }
 
 void TermDbSygus::toStreamSygus(const char* c, Node n)
@@ -866,78 +709,10 @@ void TermDbSygus::toStreamSygus(const char* c, Node n)
   }
 }
 
-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;
-    }
-    const Datatype& dt = tn.getDatatype();
-    if( !dt.isSygus() )
-    {
-      // do not recurse to non-sygus datatype types
-      return;
-    }
-    d_min_type_depth[root_tn][tn] = type_depth;
-    //compute for connected types
-    for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-      for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
-        computeMinTypeDepthInternal( root_tn, getArgType( dt[i], j ), type_depth+1 );
-      }
-    }
-  }
-}
-  
-unsigned TermDbSygus::getMinTypeDepth( TypeNode root_tn, TypeNode tn ){
-  std::map< TypeNode, unsigned >::iterator it = d_min_type_depth[root_tn].find( tn );
-  if( it==d_min_type_depth[root_tn].end() ){
-    Assert( d_min_type_depth[root_tn].find( tn )!=d_min_type_depth[root_tn].end() );  
-    return d_min_type_depth[root_tn][tn];
-  }else{
-    return it->second;
-  }
-}
-
-unsigned TermDbSygus::getMinTermSize( TypeNode tn ) {
-  Assert( isRegistered( tn ) );
-  std::map< TypeNode, unsigned >::iterator it = d_min_term_size.find( tn );
-  if( it==d_min_term_size.end() ){
-    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-    for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-      if (dt[i].getNumArgs() == 0)
-      {
-        d_min_term_size[tn] = 0;
-        return 0;
-      }
-    }
-    // TODO : improve
-    d_min_term_size[tn] = 1;
-    return 1;
-  }else{
-    return it->second;
-  }
-}
-
-unsigned TermDbSygus::getMinConsTermSize( TypeNode tn, unsigned cindex ) {
-  Assert( isRegistered( tn ) );
-  std::map< unsigned, unsigned >::iterator it = d_min_cons_term_size[tn].find( cindex );
-  if( it==d_min_cons_term_size[tn].end() ){
-    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-    Assert( cindex<dt.getNumConstructors() );
-    unsigned ret = 0;
-    if( dt[cindex].getNumArgs()>0 ){
-      ret = 1;
-      for( unsigned i=0; i<dt[cindex].getNumArgs(); i++ ){
-        ret += getMinTermSize( getArgType( dt[cindex], i ) );
-      }
-    }
-    d_min_cons_term_size[tn][cindex] = ret;
-    return ret;
-  }else{
-    return it->second;
-  }
+SygusTypeInfo& TermDbSygus::getTypeInfo(TypeNode tn)
+{
+  AlwaysAssert(d_tinfo.find(tn) != d_tinfo.end());
+  return d_tinfo[tn];
 }
 
 unsigned TermDbSygus::getSelectorWeight(TypeNode tn, Node sel)
@@ -971,114 +746,6 @@ unsigned TermDbSygus::getSelectorWeight(TypeNode tn, Node sel)
   return itsw->second[sel];
 }
 
-void TermDbSygus::getSubfieldTypes(TypeNode tn, std::vector<TypeNode>& sf_types)
-{
-  std::map<TypeNode, std::map<TypeNode, unsigned> >::iterator it =
-      d_min_type_depth.find(tn);
-  Assert(it != d_min_type_depth.end());
-  for (const std::pair<const TypeNode, unsigned>& st : it->second)
-  {
-    sf_types.push_back(st.first);
-  }
-}
-
-int TermDbSygus::getKindConsNum( TypeNode tn, Kind k ) {
-  Assert( isRegistered( tn ) );
-  std::map< TypeNode, std::map< Kind, int > >::iterator itt = d_kinds.find( tn );
-  if( itt!=d_kinds.end() ){
-    std::map< Kind, int >::iterator it = itt->second.find( k );
-    if( it!=itt->second.end() ){
-      return it->second;
-    }
-  }
-  return -1;
-}
-
-int TermDbSygus::getConstConsNum( TypeNode tn, Node n ){
-  Assert( isRegistered( tn ) );
-  std::map< TypeNode, std::map< Node, int > >::iterator itt = d_consts.find( tn );
-  if( itt!=d_consts.end() ){
-    std::map< Node, int >::iterator it = itt->second.find( n );
-    if( it!=itt->second.end() ){
-      return it->second;
-    }
-  }
-  return -1;
-}
-
-int TermDbSygus::getOpConsNum( TypeNode tn, Node n ) {
-  std::map< Node, int >::iterator it = d_ops[tn].find( n );
-  if( it!=d_ops[tn].end() ){
-    return it->second;
-  }else{
-    return -1;
-  }
-}
-
-bool TermDbSygus::hasKind( TypeNode tn, Kind k ) {
-  return getKindConsNum( tn, k )!=-1;
-}
-bool TermDbSygus::hasIte(TypeNode tn) const
-{
-  return d_hasIte.find(tn) != d_hasIte.end();
-}
-bool TermDbSygus::hasConst( TypeNode tn, Node n ) {
-  return getConstConsNum( tn, n )!=-1;
-}
-bool TermDbSygus::hasOp( TypeNode tn, Node n ) {
-  return getOpConsNum( tn, n )!=-1;
-}
-
-Node TermDbSygus::getConsNumOp( TypeNode tn, int i ) {
-  Assert( isRegistered( tn ) );
-  std::map< TypeNode, std::map< int, Node > >::iterator itt = d_arg_ops.find( tn );
-  if( itt!=d_arg_ops.end() ){
-    std::map< int, Node >::iterator itn = itt->second.find( i );
-    if( itn!=itt->second.end() ){
-      return itn->second;
-    }
-  }
-  return Node::null();
-}
-
-Node TermDbSygus::getConsNumConst( TypeNode tn, int i ) {
-  Assert( isRegistered( tn ) );
-  std::map< TypeNode, std::map< int, Node > >::iterator itt = d_arg_const.find( tn );
-  if( itt!=d_arg_const.end() ){
-    std::map< int, Node >::iterator itn = itt->second.find( i );
-    if( itn!=itt->second.end() ){
-      return itn->second;
-    }
-  }
-  return Node::null();
-}
-
-Kind TermDbSygus::getConsNumKind( TypeNode tn, int i ) {
-  Assert( isRegistered( tn ) );
-  std::map< TypeNode, std::map< int, Kind > >::iterator itt = d_arg_kind.find( tn );
-  if( itt!=d_arg_kind.end() ){
-    std::map< int, Kind >::iterator itk = itt->second.find( i );
-    if( itk!=itt->second.end() ){
-      return itk->second;
-    }
-  }
-  return UNDEFINED_KIND;
-}
-
-bool TermDbSygus::isKindArg( TypeNode tn, int i ) {
-  return getConsNumKind( tn, i )!=UNDEFINED_KIND;
-}
-
-bool TermDbSygus::isConstArg( TypeNode tn, int i ) {
-  Assert( isRegistered( tn ) );
-  std::map< TypeNode, std::map< int, Node > >::iterator itt = d_arg_const.find( tn );
-  if( itt!=d_arg_const.end() ){
-    return itt->second.find( i )!=itt->second.end();
-  }else{
-    return false;
-  }
-}
-
 TypeNode TermDbSygus::getArgType(const DatatypeConstructor& c, unsigned i) const
 {
   Assert(i < c.getNumArgs());
@@ -1099,99 +766,6 @@ bool TermDbSygus::isTypeMatch( const DatatypeConstructor& c1, const DatatypeCons
   }
 }
 
-int TermDbSygus::getAnyConstantConsNum(TypeNode tn) const
-{
-  Assert(isRegistered(tn));
-  std::map<TypeNode, unsigned>::const_iterator itt =
-      d_sym_cons_any_constant.find(tn);
-  if (itt != d_sym_cons_any_constant.end())
-  {
-    return static_cast<int>(itt->second);
-  }
-  return -1;
-}
-
-bool TermDbSygus::hasSubtermSymbolicCons(TypeNode tn) const
-{
-  return d_has_subterm_sym_cons.find(tn) != d_has_subterm_sym_cons.end();
-}
-
-unsigned TermDbSygus::getSubclassForVar(TypeNode tn, Node n) const
-{
-  std::map<TypeNode, std::map<Node, unsigned> >::const_iterator itc =
-      d_var_subclass_id.find(tn);
-  if (itc == d_var_subclass_id.end())
-  {
-    Assert(false);
-    return 0;
-  }
-  std::map<Node, unsigned>::const_iterator itcc = itc->second.find(n);
-  if (itcc == itc->second.end())
-  {
-    Assert(false);
-    return 0;
-  }
-  return itcc->second;
-}
-
-unsigned TermDbSygus::getNumSubclassVars(TypeNode tn, unsigned sc) const
-{
-  std::map<TypeNode, std::map<unsigned, std::vector<Node> > >::const_iterator
-      itv = d_var_subclass_list.find(tn);
-  if (itv == d_var_subclass_list.end())
-  {
-    Assert(false);
-    return 0;
-  }
-  std::map<unsigned, std::vector<Node> >::const_iterator itvv =
-      itv->second.find(sc);
-  if (itvv == itv->second.end())
-  {
-    Assert(false);
-    return 0;
-  }
-  return itvv->second.size();
-}
-Node TermDbSygus::getVarSubclassIndex(TypeNode tn,
-                                      unsigned sc,
-                                      unsigned i) const
-{
-  std::map<TypeNode, std::map<unsigned, std::vector<Node> > >::const_iterator
-      itv = d_var_subclass_list.find(tn);
-  if (itv == d_var_subclass_list.end())
-  {
-    Assert(false);
-    return Node::null();
-  }
-  std::map<unsigned, std::vector<Node> >::const_iterator itvv =
-      itv->second.find(sc);
-  if (itvv == itv->second.end() || i >= itvv->second.size())
-  {
-    Assert(false);
-    return Node::null();
-  }
-  return itvv->second[i];
-}
-
-bool TermDbSygus::getIndexInSubclassForVar(TypeNode tn,
-                                           Node v,
-                                           unsigned& index) const
-{
-  std::map<TypeNode, std::map<Node, unsigned> >::const_iterator itv =
-      d_var_subclass_list_index.find(tn);
-  if (itv == d_var_subclass_list_index.end())
-  {
-    return false;
-  }
-  std::map<Node, unsigned>::const_iterator itvv = itv->second.find(v);
-  if (itvv == itv->second.end())
-  {
-    return false;
-  }
-  index = itvv->second;
-  return true;
-}
-
 bool TermDbSygus::isSymbolicConsApp(Node n) const
 {
   if (n.getKind() != APPLY_CONSTRUCTOR)
@@ -1213,7 +787,9 @@ bool TermDbSygus::canConstructKind(TypeNode tn,
                                    std::vector<TypeNode>& argts,
                                    bool aggr)
 {
-  int c = getKindConsNum(tn, k);
+  Assert(isRegistered(tn));
+  SygusTypeInfo& ti = getTypeInfo(tn);
+  int c = ti.getKindConsNum(k);
   const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
   if (c != -1)
   {
@@ -1513,37 +1089,33 @@ Node TermDbSygus::evaluateBuiltin(TypeNode tn,
                                   std::vector<Node>& args,
                                   bool tryEval)
 {
-  if( !args.empty() ){
-    std::map< TypeNode, std::vector< Node > >::iterator it = d_var_list.find( tn );
-    Assert( it!=d_var_list.end() );
-    Assert( it->second.size()==args.size() );
-
-    Node res;
-    if (tryEval && options::sygusEvalOpt())
-    {
-      // Try evaluating, which is much faster than substitution+rewriting.
-      // This may fail if there is a subterm of bn under the
-      // substitution that is not constant, or if an operator in bn is not
-      // supported by the evaluator
-      res = d_eval->eval(bn, it->second, args);
-    }
-    if (!res.isNull())
-    {
-      Assert(res
-             == Rewriter::rewrite(bn.substitute(it->second.begin(),
-                                                it->second.end(),
-                                                args.begin(),
-                                                args.end())));
-      return res;
-    }
-    else
-    {
-      return Rewriter::rewrite(bn.substitute(
-          it->second.begin(), it->second.end(), args.begin(), args.end()));
-    }
-  }else{
+  if (args.empty())
+  {
     return Rewriter::rewrite( bn );
   }
+  Assert(isRegistered(tn));
+  SygusTypeInfo& ti = getTypeInfo(tn);
+  const std::vector<Node>& varlist = ti.getVarList();
+  Assert(varlist.size() == args.size());
+
+  Node res;
+  if (tryEval && options::sygusEvalOpt())
+  {
+    // Try evaluating, which is much faster than substitution+rewriting.
+    // This may fail if there is a subterm of bn under the
+    // substitution that is not constant, or if an operator in bn is not
+    // supported by the evaluator
+    res = d_eval->eval(bn, varlist, args);
+  }
+  if (!res.isNull())
+  {
+    Assert(res
+           == Rewriter::rewrite(bn.substitute(
+               varlist.begin(), varlist.end(), args.begin(), args.end())));
+    return res;
+  }
+  res = bn.substitute(varlist.begin(), varlist.end(), args.begin(), args.end());
+  return Rewriter::rewrite(res);
 }
 
 Node TermDbSygus::evaluateWithUnfolding(
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index e0312c516..6c62d7a1b 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -23,6 +23,7 @@
 #include "theory/quantifiers/extended_rewrite.h"
 #include "theory/quantifiers/sygus/sygus_eval_unfold.h"
 #include "theory/quantifiers/sygus/sygus_explain.h"
+#include "theory/quantifiers/sygus/type_info.h"
 #include "theory/quantifiers/term_database.h"
 
 namespace CVC4 {
@@ -31,23 +32,6 @@ namespace quantifiers {
 
 class SynthConjecture;
 
-/** A trie indexed by types that assigns unique identifiers to nodes. */
-class TypeNodeIdTrie
-{
- public:
-  /** children of this node */
-  std::map<TypeNode, TypeNodeIdTrie> d_children;
-  /** the data stored at this node */
-  std::vector<Node> d_data;
-  /** add v to this trie, indexed by types */
-  void add(Node v, std::vector<TypeNode>& types);
-  /**
-   * Assign each node in this trie an identifier such that
-   * assign[v1] = assign[v2] iff v1 and v2 are indexed by the same values.
-   */
-  void assignIds(std::map<Node, unsigned>& assign, unsigned& idCount);
-};
-
 /** role for registering an enumerator */
 enum EnumeratorRole
 {
@@ -78,10 +62,13 @@ class TermDbSygus {
    *
    * This initializes this database for sygus datatype type tn. This may
    * throw an assertion failure if the sygus grammar has type errors. Otherwise,
-   * after registering a sygus type, the query functions in this class (such
-   * as sygusToBuiltinType, getKindConsNum, etc.) can be called for tn.
+   * after registering a sygus type, the query function getTypeInfo can be
+   * called for tn.
+   *
+   * This method returns true if tn is a sygus datatype type and false
+   * otherwise.
    */
-  void registerSygusType(TypeNode tn);
+  bool registerSygusType(TypeNode tn);
 
   //------------------------------utilities
   /** get the explanation utility */
@@ -304,6 +291,11 @@ class TermDbSygus {
    */
   TypeNode sygusToBuiltinType(TypeNode tn);
   //-----------------------------end conversion from sygus to builtin
+  /**
+   * Get type information about sygus datatype type tn. The type tn should be
+   * (a subfield type of) a type that has been registered to this class.
+   */
+  SygusTypeInfo& getTypeInfo(TypeNode tn);
 
   /** print to sygus stream n on trace c */
   static void toStreamSygus(const char* c, Node n);
@@ -375,9 +367,7 @@ class TermDbSygus {
   /** cache of getProxyVariable */
   std::map<TypeNode, std::map<Node, Node> > d_proxy_vars;
   //-----------------------------end conversion from sygus to builtin
-
   // TODO :issue #1235 : below here needs refactor
-
  public:
   Node d_true;
   Node d_false;
@@ -388,150 +378,28 @@ class TermDbSygus {
   bool involvesDivByZero( Node n, std::map< Node, bool >& visited );
 
  private:
-  // information for sygus types
-  std::map<TypeNode, TypeNode> d_register;  // stores sygus -> builtin type
-  std::map<TypeNode, std::vector<Node> > d_var_list;
-  std::map<TypeNode, std::map<int, Kind> > d_arg_kind;
-  std::map<TypeNode, std::map<Kind, int> > d_kinds;
   /**
-   * Whether this sygus type has a constructors whose sygus operator is ITE,
-   * or is a lambda whose body is ITE.
+   * Maps types that we have called registerSygusType to a flag indicating
+   * whether that type is a sygus datatype type. Sygus datatype types that
+   * are in this map have initialized type information stored in the map below.
    */
-  std::map<TypeNode, bool> d_hasIte;
-  std::map<TypeNode, std::map<int, Node> > d_arg_const;
-  std::map<TypeNode, std::map<Node, int> > d_consts;
-  std::map<TypeNode, std::map<Node, int> > d_ops;
-  std::map<TypeNode, std::map<int, Node> > d_arg_ops;
-  std::map<TypeNode, std::map<Node, Node> > d_semantic_skolem;
-  // grammar information
-  // root -> type -> _
+  std::map<TypeNode, bool> d_registerStatus;
   /**
-   * For each sygus type t1, this maps datatype types t2 to the smallest size of
-   * a term of type t1 that includes t2 as a subterm. For example, for grammar:
-   *   A -> B+B | 0 | B-D
-   *   B -> C+C
-   *   ...
-   * we have that d_min_type_depth[A] = { A -> 0, B -> 1, C -> 2, D -> 1 }.
+   * The type information for each sygus datatype type that has been registered
+   * to this class.
    */
-  std::map<TypeNode, std::map<TypeNode, unsigned> > d_min_type_depth;
-  // std::map< TypeNode, std::map< Node, std::map< std::map< int, bool > > >
-  // d_consider_const;
-  // type -> cons -> _
-  std::map<TypeNode, unsigned> d_min_term_size;
-  std::map<TypeNode, std::map<unsigned, unsigned> > d_min_cons_term_size;
+  std::map<TypeNode, SygusTypeInfo> d_tinfo;
   /** a cache for getSelectorWeight */
   std::map<TypeNode, std::map<Node, unsigned> > d_sel_weight;
-  /**
-   * For each sygus type, the index of the "any constant" constructor, if it
-   * has one.
-   */
-  std::map<TypeNode, unsigned> d_sym_cons_any_constant;
-  /**
-   * Whether any subterm of this type contains a symbolic constructor. This
-   * corresponds to whether sygus repair techniques will ever have any effect
-   * for this type.
-   */
-  std::map<TypeNode, bool> d_has_subterm_sym_cons;
-  /**
-   * Map from sygus types and bound variables to their type subclass id. Note
-   * type class identifiers are computed for each type of registered sygus
-   * enumerators, but not all sygus types. For details, see getSubclassIdForVar.
-   */
-  std::map<TypeNode, std::map<Node, unsigned> > d_var_subclass_id;
-  /** the list of variables with given subclass */
-  std::map<TypeNode, std::map<unsigned, std::vector<Node> > >
-      d_var_subclass_list;
-  /** the index of each variable in the above list */
-  std::map<TypeNode, std::map<Node, unsigned> > d_var_subclass_list_index;
 
  public:  // general sygus utilities
   bool isRegistered(TypeNode tn) const;
-  // get the minimum depth of type in its parent grammar
-  unsigned getMinTypeDepth( TypeNode root_tn, TypeNode tn );
-  // get the minimum size for a constructor term
-  unsigned getMinTermSize( TypeNode tn );
-  unsigned getMinConsTermSize( TypeNode tn, unsigned cindex );
   /** get the weight of the selector, where tn is the domain of sel */
   unsigned getSelectorWeight(TypeNode tn, Node sel);
-  /** get subfield types
-   *
-   * This adds all "subfield types" of tn to sf_types. A type tnc is a subfield
-   * type of tn if there exists a selector chain S1( ... Sn( x )...) that has
-   * type tnc, where x has type tn. In other words, tnc is the type of some
-   * subfield of terms of type tn, at any depth.
-   */
-  void getSubfieldTypes(TypeNode tn, std::vector<TypeNode>& sf_types);
-
- public:
-  int getKindConsNum( TypeNode tn, Kind k );
-  int getConstConsNum( TypeNode tn, Node n );
-  int getOpConsNum( TypeNode tn, Node n );
-  bool hasKind( TypeNode tn, Kind k );
-  /**
-   * Returns true if this sygus type has a constructors whose sygus operator is
-   * ITE, or is a lambda whose body is ITE.
-   */
-  bool hasIte(TypeNode tn) const;
-  bool hasConst( TypeNode tn, Node n );
-  bool hasOp( TypeNode tn, Node n );
-  Node getConsNumConst( TypeNode tn, int i );
-  Node getConsNumOp( TypeNode tn, int i );
-  Kind getConsNumKind( TypeNode tn, int i );
-  bool isKindArg( TypeNode tn, int i );
-  bool isConstArg( TypeNode tn, int i );
   /** get arg type */
   TypeNode getArgType(const DatatypeConstructor& c, unsigned i) const;
-  /** is type match */
+  /** Do constructors c1 and c2 have the same type? */
   bool isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 );
-  /**
-   * Get the index of the "any constant" constructor of type tn if it has one,
-   * or returns -1 otherwise.
-   */
-  int getAnyConstantConsNum(TypeNode tn) const;
-  /** has subterm symbolic constructor
-   *
-   * Returns true if any subterm of type tn can be a symbolic constructor.
-   */
-  bool hasSubtermSymbolicCons(TypeNode tn) const;
-  //--------------------------------- variable subclasses
-  /** Get subclass id for variable
-   *
-   * This returns the "subclass" identifier for variable v in sygus
-   * type tn. A subclass identifier groups variables based on the sygus
-   * types they occur in:
-   *   A -> A + B | C + C | x | y | z | w | u
-   *   B -> y | z
-   *   C -> u
-   * The variables in this grammar can be grouped according to the sygus types
-   * they appear in:
-   *   { x,w } occur in A
-   *   { y,z } occur in A,B
-   *   { u } occurs in A,C
-   * We say that e.g. x, w are in the same subclass.
-   *
-   * If this method returns 0, then v is not a variable in sygus type tn.
-   * Otherwise, this method returns a positive value n, such that
-   * getSubclassIdForVar[v1] = getSubclassIdForVar[v2] iff v1 and v2 are in the
-   * same subclass.
-   *
-   * The type tn should be the type of an enumerator registered to this
-   * database, where notice that we do not compute this information for the
-   * subfield types of the enumerator.
-   */
-  unsigned getSubclassForVar(TypeNode tn, Node v) const;
-  /**
-   * Get the number of variable in the subclass with identifier sc for type tn.
-   */
-  unsigned getNumSubclassVars(TypeNode tn, unsigned sc) const;
-  /** Get the i^th variable in the subclass with identifier sc for type tn */
-  Node getVarSubclassIndex(TypeNode tn, unsigned sc, unsigned i) const;
-  /**
-   * Get the a variable's index in its subclass list. This method returns true
-   * iff variable v has been assigned a subclass in tn. It updates index to
-   * be v's index iff the method returns true.
-   */
-  bool getIndexInSubclassForVar(TypeNode tn, Node v, unsigned& index) const;
-  //--------------------------------- end variable subclasses
   /** return whether n is an application of a symbolic constructor */
   bool isSymbolicConsApp(Node n) const;
   /** can construct kind
@@ -560,7 +428,6 @@ class TermDbSygus {
                         bool aggr = false);
 
   TypeNode getSygusTypeForVar( Node v );
-  Node sygusSubstituted( TypeNode tn, Node n, std::vector< Node >& args );
   Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs );
   Node getNormalized(TypeNode t, Node prog);
   unsigned getSygusTermSize( Node n );
diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp
new file mode 100644
index 000000000..070e2ad9a
--- /dev/null
+++ b/src/theory/quantifiers/sygus/type_info.cpp
@@ -0,0 +1,468 @@
+/*********************                                                        */
+/*! \file type_info.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of sygus type info class
+ **/
+
+#include "theory/quantifiers/sygus/type_info.h"
+
+#include "base/cvc4_check.h"
+#include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+SygusTypeInfo::SygusTypeInfo()
+    : d_hasIte(false),
+      d_min_term_size(0),
+      d_sym_cons_any_constant(-1),
+      d_has_subterm_sym_cons(false)
+{
+}
+
+void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
+{
+  d_this = tn;
+  Assert(tn.isDatatype());
+  const Datatype& dt = tn.getDatatype();
+  Assert(dt.isSygus());
+  Trace("sygus-db") << "Register type " << dt.getName() << "..." << std::endl;
+  TypeNode btn = TypeNode::fromType(dt.getSygusType());
+  d_btype = btn;
+  Assert(!d_btype.isNull());
+  // get the sygus variable list
+  Node var_list = Node::fromExpr(dt.getSygusVarList());
+  if (!var_list.isNull())
+  {
+    for (unsigned j = 0; j < var_list.getNumChildren(); j++)
+    {
+      Node sv = var_list[j];
+      SygusVarNumAttribute svna;
+      sv.setAttribute(svna, j);
+      d_var_list.push_back(sv);
+    }
+  }
+  else
+  {
+    // no arguments to synthesis functions
+    d_var_list.clear();
+  }
+
+  // compute min term size information: this must be computed before registering
+  // subfield types
+  d_min_term_size = 1;
+  for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+  {
+    if (dt[i].getNumArgs() == 0)
+    {
+      d_min_term_size = 0;
+    }
+  }
+
+  // register connected types
+  for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+  {
+    for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
+    {
+      TypeNode ctn = TypeNode::fromType(dt[i].getArgType(j));
+      Trace("sygus-db") << "  register subfield type " << ctn << std::endl;
+      if (tds->registerSygusType(ctn))
+      {
+        SygusTypeInfo& stic = tds->getTypeInfo(ctn);
+        // carry type attributes
+        if (stic.d_has_subterm_sym_cons)
+        {
+          d_has_subterm_sym_cons = true;
+        }
+      }
+    }
+  }
+  // iterate over constructors
+  for (unsigned i = 0; i < dt.getNumConstructors(); i++)
+  {
+    Expr sop = dt[i].getSygusOp();
+    Assert(!sop.isNull());
+    Node n = Node::fromExpr(sop);
+    Trace("sygus-db") << "  Operator #" << i << " : " << sop;
+    if (sop.getKind() == kind::BUILTIN)
+    {
+      Kind sk = NodeManager::operatorToKind(n);
+      Trace("sygus-db") << ", kind = " << sk;
+      d_kinds[sk] = i;
+      d_arg_kind[i] = sk;
+      if (sk == ITE)
+      {
+        // mark that this type has an ITE
+        d_hasIte = true;
+      }
+    }
+    else if (sop.isConst() && dt[i].getNumArgs() == 0)
+    {
+      Trace("sygus-db") << ", constant";
+      d_consts[n] = i;
+      d_arg_const[i] = n;
+    }
+    else if (sop.getKind() == LAMBDA)
+    {
+      // do type checking
+      Assert(sop[0].getNumChildren() == dt[i].getNumArgs());
+      for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
+      {
+        TypeNode ct = TypeNode::fromType(dt[i].getArgType(j));
+        TypeNode cbt = tds->sygusToBuiltinType(ct);
+        TypeNode lat = TypeNode::fromType(sop[0][j].getType());
+        CVC4_CHECK(cbt.isSubtypeOf(lat))
+            << "In sygus datatype " << dt.getName()
+            << ", argument to a lambda constructor is not " << lat << std::endl;
+      }
+      if (sop[0].getKind() == ITE)
+      {
+        // mark that this type has an ITE
+        d_hasIte = true;
+      }
+    }
+    // symbolic constructors
+    if (n.getAttribute(SygusAnyConstAttribute()))
+    {
+      d_sym_cons_any_constant = i;
+      d_has_subterm_sym_cons = true;
+    }
+    // TODO (as part of #1170): we still do not properly catch type
+    // errors in sygus grammars for arguments of builtin operators.
+    // The challenge is that we easily ask for expected argument types of
+    // builtin operators e.g. PLUS. Hence the call to mkGeneric below
+    // will throw a type exception.
+    d_ops[n] = i;
+    d_arg_ops[i] = n;
+    Trace("sygus-db") << std::endl;
+    // ensure that terms that this constructor encodes are
+    // of the type specified in the datatype. This will fail if
+    // e.g. bitvector-and is a constructor of an integer grammar.
+    Node g = tds->mkGeneric(dt, i);
+    TypeNode gtn = g.getType();
+    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 minimum type depth information
+  computeMinTypeDepthInternal(tn, 0);
+  // compute minimum term size information
+  d_min_term_size = 1;
+  for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+  {
+    unsigned csize = 0;
+    if (dt[i].getNumArgs() > 0)
+    {
+      csize = 1;
+      for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
+      {
+        TypeNode ct = TypeNode::fromType(dt[i].getArgType(j));
+        if (ct == tn)
+        {
+          csize += d_min_term_size;
+        }
+        else if (tds->isRegistered(ct))
+        {
+          SygusTypeInfo& stic = tds->getTypeInfo(ct);
+          csize += stic.getMinTermSize();
+        }
+        else
+        {
+          Assert(!ct.isDatatype() || !ct.getDatatype().isSygus());
+        }
+      }
+    }
+    d_min_cons_term_size[i] = csize;
+  }
+}
+
+void SygusTypeInfo::initializeVarSubclasses()
+{
+  if (d_var_list.empty())
+  {
+    // no variables
+    return;
+  }
+  if (!d_var_subclass_id.empty())
+  {
+    // already computed
+    return;
+  }
+  // compute variable subclasses
+  std::vector<TypeNode> sf_types;
+  getSubfieldTypes(sf_types);
+  // maps variables to the list of subfield types they occur in
+  std::map<Node, std::vector<TypeNode> > type_occurs;
+  for (const Node& v : d_var_list)
+  {
+    type_occurs[v].clear();
+  }
+  // for each type of subfield type of this enumerator
+  for (unsigned i = 0, ntypes = sf_types.size(); i < ntypes; i++)
+  {
+    std::vector<unsigned> rm_indices;
+    TypeNode stn = sf_types[i];
+    Assert(stn.isDatatype());
+    const Datatype& dt = stn.getDatatype();
+    for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
+    {
+      Expr sop = dt[j].getSygusOp();
+      Assert(!sop.isNull());
+      Node sopn = Node::fromExpr(sop);
+      if (type_occurs.find(sopn) != type_occurs.end())
+      {
+        // if it is a variable, store that it occurs in stn
+        type_occurs[sopn].push_back(stn);
+      }
+    }
+  }
+  TypeNodeIdTrie tnit;
+  for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs)
+  {
+    tnit.add(to.first, to.second);
+  }
+  // 0 is reserved for "no type class id"
+  unsigned typeIdCount = 1;
+  tnit.assignIds(d_var_subclass_id, typeIdCount);
+  // assign the list and reverse map to index
+  for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs)
+  {
+    Node v = to.first;
+    unsigned sc = d_var_subclass_id[v];
+    Trace("sygus-db") << v << " has subclass id " << sc << std::endl;
+    d_var_subclass_list_index[v] = d_var_subclass_list[sc].size();
+    d_var_subclass_list[sc].push_back(v);
+  }
+}
+
+TypeNode SygusTypeInfo::getBuiltinType() const { return d_btype; }
+
+const std::vector<Node>& SygusTypeInfo::getVarList() const
+{
+  return d_var_list;
+}
+
+void SygusTypeInfo::computeMinTypeDepthInternal(TypeNode tn,
+                                                unsigned type_depth)
+{
+  std::map<TypeNode, unsigned>::iterator it = d_min_type_depth.find(tn);
+  if (it != d_min_type_depth.end() && type_depth >= it->second)
+  {
+    // no new information
+    return;
+  }
+  if (!tn.isDatatype())
+  {
+    // do not recurse to non-datatype types
+    return;
+  }
+  const Datatype& dt = tn.getDatatype();
+  if (!dt.isSygus())
+  {
+    // do not recurse to non-sygus datatype types
+    return;
+  }
+  d_min_type_depth[tn] = type_depth;
+  // compute for connected types
+  for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+  {
+    for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
+    {
+      TypeNode at = TypeNode::fromType(dt[i].getArgType(j));
+      computeMinTypeDepthInternal(at, type_depth + 1);
+    }
+  }
+}
+
+unsigned SygusTypeInfo::getMinTypeDepth(TypeNode tn) const
+{
+  std::map<TypeNode, unsigned>::const_iterator it = d_min_type_depth.find(tn);
+  if (it != d_min_type_depth.end())
+  {
+    Assert(false);
+    return 0;
+  }
+  return it->second;
+}
+
+unsigned SygusTypeInfo::getMinTermSize() const { return d_min_term_size; }
+
+unsigned SygusTypeInfo::getMinConsTermSize(unsigned cindex)
+{
+  std::map<unsigned, unsigned>::iterator it = d_min_cons_term_size.find(cindex);
+  if (it != d_min_cons_term_size.end())
+  {
+    return it->second;
+  }
+  Assert(false);
+  return 0;
+}
+
+void SygusTypeInfo::getSubfieldTypes(std::vector<TypeNode>& sf_types) const
+{
+  for (const std::pair<const TypeNode, unsigned>& st : d_min_type_depth)
+  {
+    sf_types.push_back(st.first);
+  }
+}
+
+int SygusTypeInfo::getKindConsNum(Kind k) const
+{
+  std::map<Kind, unsigned>::const_iterator it = d_kinds.find(k);
+  if (it != d_kinds.end())
+  {
+    return static_cast<int>(it->second);
+  }
+  return -1;
+}
+
+int SygusTypeInfo::getConstConsNum(Node n) const
+{
+  std::map<Node, unsigned>::const_iterator it = d_consts.find(n);
+  if (it != d_consts.end())
+  {
+    return static_cast<int>(it->second);
+  }
+  return -1;
+}
+
+int SygusTypeInfo::getOpConsNum(Node n) const
+{
+  std::map<Node, unsigned>::const_iterator it = d_ops.find(n);
+  if (it != d_ops.end())
+  {
+    return static_cast<int>(it->second);
+  }
+  return -1;
+}
+
+bool SygusTypeInfo::hasKind(Kind k) const { return getKindConsNum(k) != -1; }
+bool SygusTypeInfo::hasIte() const { return d_hasIte; }
+bool SygusTypeInfo::hasConst(Node n) const { return getConstConsNum(n) != -1; }
+bool SygusTypeInfo::hasOp(Node n) const { return getOpConsNum(n) != -1; }
+
+Node SygusTypeInfo::getConsNumOp(unsigned i) const
+{
+  std::map<unsigned, Node>::const_iterator itn = d_arg_ops.find(i);
+  if (itn != d_arg_ops.end())
+  {
+    return itn->second;
+  }
+  return Node::null();
+}
+
+Node SygusTypeInfo::getConsNumConst(unsigned i) const
+{
+  std::map<unsigned, Node>::const_iterator itn = d_arg_const.find(i);
+  if (itn != d_arg_const.end())
+  {
+    return itn->second;
+  }
+  return Node::null();
+}
+
+Kind SygusTypeInfo::getConsNumKind(unsigned i) const
+{
+  std::map<unsigned, Kind>::const_iterator itk = d_arg_kind.find(i);
+  if (itk != d_arg_kind.end())
+  {
+    return itk->second;
+  }
+  return UNDEFINED_KIND;
+}
+
+bool SygusTypeInfo::isKindArg(unsigned i) const
+{
+  return getConsNumKind(i) != UNDEFINED_KIND;
+}
+
+bool SygusTypeInfo::isConstArg(unsigned i) const
+{
+  return d_arg_const.find(i) != d_arg_const.end();
+}
+
+int SygusTypeInfo::getAnyConstantConsNum() const
+{
+  return d_sym_cons_any_constant;
+}
+
+bool SygusTypeInfo::hasSubtermSymbolicCons() const
+{
+  return d_has_subterm_sym_cons;
+}
+
+unsigned SygusTypeInfo::getSubclassForVar(Node n) const
+{
+  std::map<Node, unsigned>::const_iterator itcc = d_var_subclass_id.find(n);
+  if (itcc == d_var_subclass_id.end())
+  {
+    Assert(false);
+    return 0;
+  }
+  return itcc->second;
+}
+
+unsigned SygusTypeInfo::getNumSubclassVars(unsigned sc) const
+{
+  std::map<unsigned, std::vector<Node> >::const_iterator itvv =
+      d_var_subclass_list.find(sc);
+  if (itvv == d_var_subclass_list.end())
+  {
+    Assert(false);
+    return 0;
+  }
+  return itvv->second.size();
+}
+Node SygusTypeInfo::getVarSubclassIndex(unsigned sc, unsigned i) const
+{
+  std::map<unsigned, std::vector<Node> >::const_iterator itvv =
+      d_var_subclass_list.find(sc);
+  if (itvv == d_var_subclass_list.end() || i >= itvv->second.size())
+  {
+    Assert(false);
+    return Node::null();
+  }
+  return itvv->second[i];
+}
+
+bool SygusTypeInfo::getIndexInSubclassForVar(Node v, unsigned& index) const
+{
+  std::map<Node, unsigned>::const_iterator itvv =
+      d_var_subclass_list_index.find(v);
+  if (itvv == d_var_subclass_list_index.end())
+  {
+    return false;
+  }
+  index = itvv->second;
+  return true;
+}
+
+bool SygusTypeInfo::isSubclassVarTrivial() const
+{
+  for (const std::pair<const unsigned, std::vector<Node> >& p :
+       d_var_subclass_list)
+  {
+    if (p.second.size() > 1)
+    {
+      return false;
+    }
+  }
+  return true;
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/sygus/type_info.h b/src/theory/quantifiers/sygus/type_info.h
new file mode 100644
index 000000000..9ac93f7ae
--- /dev/null
+++ b/src/theory/quantifiers/sygus/type_info.h
@@ -0,0 +1,260 @@
+/*********************                                                        */
+/*! \file type_info.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Sygus type info data structure
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H
+
+#include <map>
+#include <unordered_set>
+
+#include "expr/node.h"
+#include "theory/quantifiers/sygus/type_node_id_trie.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class TermDbSygus;
+
+/**
+ * This data structure stores statically computed information regarding a sygus
+ * datatype type.
+ *
+ * To use an instance of this class x, call x.initialize(tn); where tn is a
+ * sygus datatype type. Then, most of the query methods on x can be called.
+ * As an exception, the variable subclass queries require that additionally
+ * x.initializeVarSubclasses() is called.
+ *
+ */
+class SygusTypeInfo
+{
+ public:
+  SygusTypeInfo();
+  //-------------------------------------------- initialize
+  /** initialize this information for sygus datatype type tn */
+  void initialize(TermDbSygus* tds, TypeNode tn);
+  /**
+   * Initialize the variable subclass information for this class. Must have
+   * called initialize(...) prior to calling this method.
+   */
+  void initializeVarSubclasses();
+  //-------------------------------------------- end initialize
+  /** Get the builtin type that this sygus type encodes */
+  TypeNode getBuiltinType() const;
+  /** Get the variable list (formal argument list) for the sygus type */
+  const std::vector<Node>& getVarList() const;
+  /**
+   * Return the index of the constructor of this sygus type that encodes
+   * application of the builtin Kind k, or -1 if one does not exist.
+   */
+  int getKindConsNum(Kind k) const;
+  /**
+   * Return the index of the constructor of this sygus type that encodes
+   * constant c, or -1 if one does not exist.
+   */
+  int getConstConsNum(Node c) const;
+  /**
+   * Return the index of the constructor of this sygus type whose builtin
+   * operator is n, or -1 if one does not exist.
+   */
+  int getOpConsNum(Node n) const;
+  /** Is there a constructor that encodes application of builtin Kind k? */
+  bool hasKind(Kind k) const;
+  /** Is there a constructor that encodes constant c? */
+  bool hasConst(Node c) const;
+  /** Is there a constructor whose builtin operator is n? */
+  bool hasOp(Node n) const;
+  /**
+   * Returns true if this sygus type has a constructor whose sygus operator is
+   * ITE, or is a lambda whose body is ITE.
+   */
+  bool hasIte() const;
+  /**
+   * Get the builtin kind for the i^th constructor of this sygus type. If the
+   * i^th constructor does not encode an application of a builtin kind, this
+   * method returns UNDEFINED_KIND.
+   */
+  Kind getConsNumKind(unsigned i) const;
+  /**
+   * Get the construct for the i^th constructor of this sygus type. If the
+   * i^th constructor does not encode a builtin constant, this method returns
+   * the null node.
+   */
+  Node getConsNumConst(unsigned i) const;
+  /** Get the builtin operator of the i^th constructor of this sygus type */
+  Node getConsNumOp(unsigned i) const;
+  /**
+   * Returns true if the i^th constructor encodes application of a builtin Kind.
+   */
+  bool isKindArg(unsigned i) const;
+  /**
+   * Returns true if the i^th constructor encodes a builtin constant.
+   */
+  bool isConstArg(unsigned i) const;
+  /**
+   * Get the index of the "any constant" constructor of type tn if it has one,
+   * or returns -1 otherwise.
+   */
+  int getAnyConstantConsNum() const;
+  /** has subterm symbolic constructor
+   *
+   * Returns true if any subterm of type tn can be a symbolic constructor.
+   */
+  bool hasSubtermSymbolicCons() const;
+  /** get subfield types
+   *
+   * This adds all "subfield types" of tn to sf_types. A type tnc is a subfield
+   * type of tn if there exists a selector chain S1( ... Sn( x )...) that has
+   * type tnc, where x has type tn. In other words, tnc is the type of some
+   * subfield of terms of type tn, at any depth.
+   */
+  void getSubfieldTypes(std::vector<TypeNode>& sf_types) const;
+  //--------------------------------- variable subclasses
+  /** Get subclass id for variable
+   *
+   * This returns the "subclass" identifier for variable v in sygus
+   * type tn. A subclass identifier groups variables based on the sygus
+   * types they occur in:
+   *   A -> A + B | C + C | x | y | z | w | u
+   *   B -> y | z
+   *   C -> u
+   * The variables in this grammar can be grouped according to the sygus types
+   * they appear in:
+   *   { x,w } occur in A
+   *   { y,z } occur in A,B
+   *   { u } occurs in A,C
+   * We say that e.g. x, w are in the same subclass.
+   *
+   * If this method returns 0, then v is not a variable in sygus type tn.
+   * Otherwise, this method returns a positive value n, such that
+   * getSubclassIdForVar[v1] = getSubclassIdForVar[v2] iff v1 and v2 are in the
+   * same subclass.
+   *
+   * The type tn should be the type of an enumerator registered to this
+   * database, where notice that we do not compute this information for the
+   * subfield types of the enumerator.
+   */
+  unsigned getSubclassForVar(Node v) const;
+  /**
+   * Get the number of variable in the subclass with identifier sc for type tn.
+   */
+  unsigned getNumSubclassVars(unsigned sc) const;
+  /** Get the i^th variable in the subclass with identifier sc for type tn */
+  Node getVarSubclassIndex(unsigned sc, unsigned i) const;
+  /**
+   * Get the a variable's index in its subclass list. This method returns true
+   * iff variable v has been assigned a subclass in tn. It updates index to
+   * be v's index iff the method returns true.
+   */
+  bool getIndexInSubclassForVar(Node v, unsigned& index) const;
+  /**
+   * Are the variable subclasses a trivial partition (each variable subclass
+   * has a single variable)?
+   */
+  bool isSubclassVarTrivial() const;
+  //--------------------------------- end variable subclasses
+  /**
+   * Get the minimum depth of type in this grammar
+   *
+   */
+  unsigned getMinTypeDepth(TypeNode tn) const;
+  /** Get the minimum size for a term of this sygus type */
+  unsigned getMinTermSize() const;
+  /**
+   * Get the minimum size for a term that is an application of a constructor of
+   * this type.
+   */
+  unsigned getMinConsTermSize(unsigned cindex);
+
+ private:
+  /** The sygus type that this class is for */
+  TypeNode d_this;
+  /** The builtin type that this sygus type encodes */
+  TypeNode d_btype;
+  /** The variable list of the sygus type */
+  std::vector<Node> d_var_list;
+  /**
+   * Maps constructor indices to the (builtin) Kind that they encode, if any.
+   */
+  std::map<unsigned, Kind> d_arg_kind;
+  /** Reverse of the above map */
+  std::map<Kind, unsigned> d_kinds;
+  /**
+   * Whether this sygus type has a constructors whose sygus operator is ITE,
+   * or is a lambda whose body is ITE.
+   */
+  bool d_hasIte;
+  /**
+   * Maps constructor indices to the constant that they encode, if any.
+   */
+  std::map<unsigned, Node> d_arg_const;
+  /** Reverse of the above map */
+  std::map<Node, unsigned> d_consts;
+  /**
+   * Maps constructor indices to the operator they encode.
+   */
+  std::map<unsigned, Node> d_arg_ops;
+  /** Reverse of the above map */
+  std::map<Node, unsigned> d_ops;
+  /**
+   * This maps the subfield datatype types T to the smallest size of a term of
+   * this sygus type that includes T as a subterm. For example, for type A with
+   * grammar:
+   *   A -> B+B | 0 | B-D
+   *   B -> C+C
+   *   ...
+   * we have that d_min_type_depth = { A -> 0, B -> 1, C -> 2, D -> 1 }.
+   */
+  std::map<TypeNode, unsigned> d_min_type_depth;
+  /** The minimimum size term of this type */
+  unsigned d_min_term_size;
+  /**
+   * Maps constructors to the minimum size term that is an application of that
+   * constructor.
+   */
+  std::map<unsigned, unsigned> d_min_cons_term_size;
+  /** a cache for getSelectorWeight */
+  std::map<Node, unsigned> d_sel_weight;
+  /**
+   * For each sygus type, the index of the "any constant" constructor, if it
+   * has one, or -1 otherwise.
+   */
+  int d_sym_cons_any_constant;
+  /**
+   * Whether any subterm of this type contains a symbolic constructor. This
+   * corresponds to whether sygus repair techniques will ever have any effect
+   * for this type.
+   */
+  bool d_has_subterm_sym_cons;
+  /**
+   * Map from sygus types and bound variables to their type subclass id. Note
+   * type class identifiers are computed for each type of registered sygus
+   * enumerators, but not all sygus types. For details, see getSubclassIdForVar.
+   */
+  std::map<Node, unsigned> d_var_subclass_id;
+  /** the list of variables with given subclass */
+  std::map<unsigned, std::vector<Node> > d_var_subclass_list;
+  /** the index of each variable in the above list */
+  std::map<Node, unsigned> d_var_subclass_list_index;
+  /** computes the map d_min_type_depth */
+  void computeMinTypeDepthInternal(TypeNode root_tn, unsigned type_depth);
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H */
diff --git a/src/theory/quantifiers/sygus/type_node_id_trie.cpp b/src/theory/quantifiers/sygus/type_node_id_trie.cpp
new file mode 100644
index 000000000..ffe2f533d
--- /dev/null
+++ b/src/theory/quantifiers/sygus/type_node_id_trie.cpp
@@ -0,0 +1,52 @@
+/*********************                                                        */
+/*! \file type_node_id_trie.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of type node identifier trie
+ **/
+
+#include "theory/quantifiers/sygus/type_node_id_trie.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+void TypeNodeIdTrie::add(Node v, std::vector<TypeNode>& types)
+{
+  TypeNodeIdTrie* tnt = this;
+  for (unsigned i = 0, size = types.size(); i < size; i++)
+  {
+    tnt = &tnt->d_children[types[i]];
+  }
+  tnt->d_data.push_back(v);
+}
+
+void TypeNodeIdTrie::assignIds(std::map<Node, unsigned>& assign,
+                               unsigned& idCount)
+{
+  if (!d_data.empty())
+  {
+    for (const Node& v : d_data)
+    {
+      assign[v] = idCount;
+    }
+    idCount++;
+  }
+  for (std::pair<const TypeNode, TypeNodeIdTrie>& c : d_children)
+  {
+    c.second.assignIds(assign, idCount);
+  }
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/sygus/type_node_id_trie.h b/src/theory/quantifiers/sygus/type_node_id_trie.h
new file mode 100644
index 000000000..d0798c7a9
--- /dev/null
+++ b/src/theory/quantifiers/sygus/type_node_id_trie.h
@@ -0,0 +1,55 @@
+/*********************                                                        */
+/*! \file type_node_id_trie.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Type node identifier trie data structure
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H
+
+#include <map>
+#include <vector>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class TermDbSygus;
+
+/**
+ * A trie indexed by types that assigns unique identifiers to nodes based on
+ * a vector of types.
+ */
+class TypeNodeIdTrie
+{
+ public:
+  /** children of this node */
+  std::map<TypeNode, TypeNodeIdTrie> d_children;
+  /** the data stored at this node */
+  std::vector<Node> d_data;
+  /** add v to this trie, indexed by types */
+  void add(Node v, std::vector<TypeNode>& types);
+  /**
+   * Assign each node in this trie an identifier such that
+   * assign[v1] = assign[v2] iff v1 and v2 are indexed by the same values.
+   */
+  void assignIds(std::map<Node, unsigned>& assign, unsigned& idCount);
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H */