Make sygus unif utility use sygus unif strategies (#1732)

5 files changed, 176 insertions, 1141 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h
index fb353a102..b45b602ec 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.h
+++ b/src/theory/quantifiers/sygus/sygus_pbe.h
@@ -70,9 +70,8 @@ class CegConjecture;
 *
 * (4) During search, the extension of quantifier-free datatypes procedure for
 *     SyGuS datatypes may ask this class whether current candidates can be
-*     discarded based on
-*     inferring when two candidate solutions are equivalent up to examples.
-*     For example, the candidate solutions:
+*     discarded based on inferring when two candidate solutions are equivalent
+*     up to examples. For example, the candidate solutions:
 *     f = \x ite( x < 0, x+1, x ) and f = \x x
 *     are equivalent up to examples on the above conjecture, since they have the
 *     same value on the points x = 0,5,6. Hence, we need only consider one of
@@ -85,12 +84,11 @@ class CegConjecture;
 *     CegConjecturePbe::getCandidateList(...), where this class returns the list
 *     of active enumerators.
 * (6) The parent class subsequently calls
-*     CegConjecturePbe::constructValues(...), which
-*     informs this class that new values have been enumerated for active
-*     enumerators, as indicated by the current model. This call also requests
-*     that based on these
+*     CegConjecturePbe::constructValues(...), which informs this class that new
+*     values have been enumerated for active enumerators, as indicated by the
+*     current model. This call also requests that based on these
 *     newly enumerated values, whether this class is now able to construct a
-*     solution based on the high-level strategy (stored in d_c_info).
+*     solution based on the high-level strategy (stored in d_sygus_unif).
 *
 * This class is not designed to work in incremental mode, since there is no way
 * to specify incremental problems in SyguS.
@@ -248,18 +246,36 @@ class CegConjecturePbe : public SygusModule
   void collectExamples( Node n, std::map< Node, bool >& visited, bool hasPol, bool pol );
 
   //--------------------------------- PBE search values
-  /** this class is an index of candidate solutions for PBE synthesis */
+  /**
+   * This class is an index of candidate solutions for PBE synthesis and their
+   * (concrete) evaluation on the set of input examples. For example, if the
+   * set of input examples for (x,y) is (0,1), (1,3), then:
+   *   term x is indexed by 0,1
+   *   term x+y is indexed by 1,4
+   *   term 0 is indexed by 0,0.
+   */
   class PbeTrie {
    public:
     PbeTrie() {}
     ~PbeTrie() {}
+    /** the data for this node in the trie */
     Node d_lazy_child;
+    /** the children for this node in the trie */
     std::map<Node, PbeTrie> d_children;
+    /** clear this trie */
     void clear() { d_children.clear(); }
+    /**
+     * Add term b as a value enumerated for enumerator e to the trie.
+     *
+     * cpbe : reference to the parent pbe utility which stores the examples,
+     * index : the index of the example we are processing,
+     * ntotal : the total of the examples for enumerator e.
+     */
     Node addPbeExample(TypeNode etn, Node e, Node b, CegConjecturePbe* cpbe,
                        unsigned index, unsigned ntotal);
 
    private:
+    /** Helper function for above, called when we get the current example ex. */
     Node addPbeExampleEval(TypeNode etn, Node e, Node b, std::vector<Node>& ex,
                            CegConjecturePbe* cpbe, unsigned index,
                            unsigned ntotal);
diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp
index 00658b6c4..27568fcce 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif.cpp
@@ -479,15 +479,7 @@ void SygusUnif::initialize(QuantifiersEngine* qe,
   d_qe = qe;
   d_tds = qe->getTermDatabaseSygus();
 
-  TypeNode tn = f.getType();
-  d_cinfo.initialize(f);
-  // collect the enumerator types and form the strategy
-  collectEnumeratorTypes(tn, role_equal);
-  // add the enumerators
-  enums.insert(
-      enums.end(), d_cinfo.d_esym_list.begin(), d_cinfo.d_esym_list.end());
-  // learn redundant ops
-  staticLearnRedundantOps(lemmas);
+  d_strategy.initialize(qe, f, enums, lemmas);
 }
 
 void SygusUnif::resetExamples()
@@ -509,11 +501,8 @@ void SygusUnif::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
   Node c = d_candidate;
   Assert(!d_examples.empty());
   Assert(d_examples.size() == d_examples_out.size());
-  std::map<Node, EnumInfo>::iterator it = d_einfo.find(e);
-  Assert(it != d_einfo.end());
-  Assert(
-      std::find(it->second.d_enum_vals.begin(), it->second.d_enum_vals.end(), v)
-      == it->second.d_enum_vals.end());
+
+  EnumInfo& ei = d_strategy.getEnumInfo(e);
   // The explanation for why the current value should be excluded in future
   // iterations.
   Node exp_exc;
@@ -531,8 +520,7 @@ void SygusUnif::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
   }
   // is it excluded for domain-specific reason?
   std::vector<Node> exp_exc_vec;
-  if (getExplanationForEnumeratorExclude(
-          e, v, base_results, it->second, exp_exc_vec))
+  if (getExplanationForEnumeratorExclude(e, v, base_results, exp_exc_vec))
   {
     Assert(!exp_exc_vec.empty());
     exp_exc = exp_exc_vec.size() == 1
@@ -544,19 +532,22 @@ void SygusUnif::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
   else
   {
     // notify all slaves
-    Assert(!it->second.d_enum_slave.empty());
+    Assert(!ei.d_enum_slave.empty());
     // explanation for why this value should be excluded
-    for (unsigned s = 0; s < it->second.d_enum_slave.size(); s++)
+    for (unsigned s = 0; s < ei.d_enum_slave.size(); s++)
     {
-      Node xs = it->second.d_enum_slave[s];
-      std::map<Node, EnumInfo>::iterator itv = d_einfo.find(xs);
-      Assert(itv != d_einfo.end());
+      Node xs = ei.d_enum_slave[s];
+
+      EnumInfo& eiv = d_strategy.getEnumInfo(xs);
+
+      EnumCache& ecv = d_ecache[xs];
+
       Trace("sygus-pbe-enum") << "Process " << xs << " from " << s << std::endl;
       // bool prevIsCover = false;
-      if (itv->second.getRole() == enum_io)
+      if (eiv.getRole() == enum_io)
       {
         Trace("sygus-pbe-enum") << "   IO-Eval of ";
-        // prevIsCover = itv->second.isFeasible();
+        // prevIsCover = eiv.isFeasible();
       }
       else
       {
@@ -565,8 +556,8 @@ void SygusUnif::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
       Trace("sygus-pbe-enum") << xs << " : ";
       // evaluate all input/output examples
       std::vector<Node> results;
-      Node templ = itv->second.d_template;
-      TNode templ_var = itv->second.d_template_arg;
+      Node templ = eiv.d_template;
+      TNode templ_var = eiv.d_template_arg;
       std::map<Node, bool> cond_vals;
       for (unsigned j = 0, size = base_results.size(); j < size; j++)
       {
@@ -580,7 +571,7 @@ void SygusUnif::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
           Assert(res.isConst());
         }
         Node resb;
-        if (itv->second.getRole() == enum_io)
+        if (eiv.getRole() == enum_io)
         {
           Node out = d_examples_out[j];
           Assert(out.isConst());
@@ -605,7 +596,7 @@ void SygusUnif::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
         }
       }
       bool keep = false;
-      if (itv->second.getRole() == enum_io)
+      if (eiv.getRole() == enum_io)
       {
         // latter is the degenerate case of no examples
         if (cond_vals.find(d_true) != cond_vals.end() || cond_vals.empty())
@@ -618,28 +609,25 @@ void SygusUnif::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
             Trace("sygus-pbe-enum")
                 << "  ...success, full solution added to PBE pool : "
                 << d_tds->sygusToBuiltin(v) << std::endl;
-            if (!itv->second.isSolved())
+            if (!ecv.isSolved())
             {
-              itv->second.setSolved(v);
+              ecv.setSolved(v);
               // it subsumes everything
-              itv->second.d_term_trie.clear();
-              itv->second.d_term_trie.addTerm(v, results, true, subsume);
+              ecv.d_term_trie.clear();
+              ecv.d_term_trie.addTerm(v, results, true, subsume);
             }
             keep = true;
           }
           else
           {
-            Node val =
-                itv->second.d_term_trie.addTerm(v, results, true, subsume);
+            Node val = ecv.d_term_trie.addTerm(v, results, true, subsume);
             if (val == v)
             {
               Trace("sygus-pbe-enum") << "  ...success";
               if (!subsume.empty())
               {
-                itv->second.d_enum_subsume.insert(
-                    itv->second.d_enum_subsume.end(),
-                    subsume.begin(),
-                    subsume.end());
+                ecv.d_enum_subsume.insert(
+                    ecv.d_enum_subsume.end(), subsume.begin(), subsume.end());
                 Trace("sygus-pbe-enum")
                     << " and subsumed " << subsume.size() << " terms";
               }
@@ -664,7 +652,7 @@ void SygusUnif::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
       else
       {
         // must be unique up to examples
-        Node val = itv->second.d_term_trie.addCond(v, results, true);
+        Node val = ecv.d_term_trie.addCond(v, results, true);
         if (val == v)
         {
           Trace("sygus-pbe-enum") << "  ...success!   add to PBE pool : "
@@ -676,13 +664,13 @@ void SygusUnif::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
           Trace("sygus-pbe-enum")
               << "  ...fail : term is not unique" << std::endl;
         }
-        d_cinfo.d_cond_count++;
+        d_cond_count++;
       }
       if (keep)
       {
-        // notify the parent to retry the build of PBE
-        d_cinfo.d_check_sol = true;
-        itv->second.addEnumValue(this, v, results);
+        // notify to retry the build of solution
+        d_check_sol = true;
+        ecv.addEnumValue(v, results);
       }
     }
   }
@@ -702,27 +690,27 @@ void SygusUnif::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
 Node SygusUnif::constructSolution()
 {
   Node c = d_candidate;
-  if (!d_cinfo.d_solution.isNull())
+  if (!d_solution.isNull())
   {
     // already has a solution
-    return d_cinfo.d_solution;
+    return d_solution;
   }
   else
   {
     // only check if an enumerator updated
-    if (d_cinfo.d_check_sol)
+    if (d_check_sol)
     {
-      Trace("sygus-pbe") << "Construct solution, #iterations = "
-                         << d_cinfo.d_cond_count << std::endl;
-      d_cinfo.d_check_sol = false;
+      Trace("sygus-pbe") << "Construct solution, #iterations = " << d_cond_count
+                         << std::endl;
+      d_check_sol = false;
       // try multiple times if we have done multiple conditions, due to
       // non-determinism
       Node vc;
-      for (unsigned i = 0; i <= d_cinfo.d_cond_count; i++)
+      for (unsigned i = 0; i <= d_cond_count; i++)
       {
         Trace("sygus-pbe-dt")
             << "ConstructPBE for candidate: " << c << std::endl;
-        Node e = d_cinfo.getRootEnumerator();
+        Node e = d_strategy.getRootEnumerator();
         UnifContext x;
         x.initialize(this);
         Node vcc = constructSolution(e, role_equal, x, 1);
@@ -741,7 +729,7 @@ Node SygusUnif::constructSolution()
       }
       if (!vc.isNull())
       {
-        d_cinfo.d_solution = vc;
+        d_solution = vc;
         return vc;
       }
       Trace("sygus-pbe") << "...failed to solve." << std::endl;
@@ -750,780 +738,54 @@ Node SygusUnif::constructSolution()
   }
 }
 
-// ----------------------------- establishing enumeration types
-
-void SygusUnif::registerEnumerator(Node et,
-                                   TypeNode tn,
-                                   EnumRole enum_role,
-                                   bool inSearch)
-{
-  if (d_einfo.find(et) == d_einfo.end())
-  {
-    Trace("sygus-unif-debug")
-        << "...register " << et << " for "
-        << static_cast<DatatypeType>(tn.toType()).getDatatype().getName();
-    Trace("sygus-unif-debug") << ", role = " << enum_role
-                              << ", in search = " << inSearch << std::endl;
-    d_einfo[et].initialize(enum_role);
-    // if we are actually enumerating this (could be a compound node in the
-    // strategy)
-    if (inSearch)
-    {
-      std::map<TypeNode, Node>::iterator itn = d_cinfo.d_search_enum.find(tn);
-      if (itn == d_cinfo.d_search_enum.end())
-      {
-        // use this for the search
-        d_cinfo.d_search_enum[tn] = et;
-        d_cinfo.d_esym_list.push_back(et);
-        d_einfo[et].d_enum_slave.push_back(et);
-      }
-      else
-      {
-        Trace("sygus-unif-debug")
-            << "Make " << et << " a slave of " << itn->second << std::endl;
-        d_einfo[itn->second].d_enum_slave.push_back(et);
-      }
-    }
-  }
-}
-
-void SygusUnif::collectEnumeratorTypes(TypeNode tn, NodeRole nrole)
-{
-  NodeManager* nm = NodeManager::currentNM();
-  if (d_cinfo.d_tinfo.find(tn) == d_cinfo.d_tinfo.end())
-  {
-    // register type
-    Trace("sygus-unif") << "Register enumerating type : " << tn << std::endl;
-    d_cinfo.initializeType(tn);
-  }
-  EnumTypeInfo& eti = d_cinfo.d_tinfo[tn];
-  std::map<NodeRole, StrategyNode>::iterator itsn = eti.d_snodes.find(nrole);
-  if (itsn != eti.d_snodes.end())
-  {
-    // already initialized
-    return;
-  }
-  StrategyNode& snode = eti.d_snodes[nrole];
-
-  // get the enumerator for this
-  EnumRole erole = getEnumeratorRoleForNodeRole(nrole);
-
-  Node ee;
-  std::map<EnumRole, Node>::iterator iten = eti.d_enum.find(erole);
-  if (iten == eti.d_enum.end())
-  {
-    ee = nm->mkSkolem("ee", tn);
-    eti.d_enum[erole] = ee;
-    Trace("sygus-unif-debug")
-        << "...enumerator " << ee << " for "
-        << static_cast<DatatypeType>(tn.toType()).getDatatype().getName()
-        << ", role = " << erole << std::endl;
-  }
-  else
-  {
-    ee = iten->second;
-  }
-
-  // roles that we do not recurse on
-  if (nrole == role_ite_condition)
-  {
-    Trace("sygus-unif-debug") << "...this register (non-io)" << std::endl;
-    registerEnumerator(ee, tn, erole, true);
-    return;
-  }
-
-  // look at information on how we will construct solutions for this type
-  Assert(tn.isDatatype());
-  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
-  Assert(dt.isSygus());
-
-  std::map<Node, std::vector<StrategyType> > cop_to_strat;
-  std::map<Node, unsigned> cop_to_cindex;
-  std::map<Node, std::map<unsigned, Node> > cop_to_child_templ;
-  std::map<Node, std::map<unsigned, Node> > cop_to_child_templ_arg;
-  std::map<Node, std::vector<unsigned> > cop_to_carg_list;
-  std::map<Node, std::vector<TypeNode> > cop_to_child_types;
-  std::map<Node, std::vector<Node> > cop_to_sks;
-
-  // whether we will enumerate the current type
-  bool search_this = false;
-  for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
-  {
-    Node cop = Node::fromExpr(dt[j].getConstructor());
-    Node op = Node::fromExpr(dt[j].getSygusOp());
-    Trace("sygus-unif-debug") << "--- Infer strategy from " << cop
-                              << " with sygus op " << op << "..." << std::endl;
-
-    // expand the evaluation to see if this constuctor induces a strategy
-    std::vector<Node> utchildren;
-    utchildren.push_back(cop);
-    std::vector<Node> sks;
-    std::vector<TypeNode> sktns;
-    for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
-    {
-      Type t = dt[j][k].getRangeType();
-      TypeNode ttn = TypeNode::fromType(t);
-      Node kv = nm->mkSkolem("ut", ttn);
-      sks.push_back(kv);
-      cop_to_sks[cop].push_back(kv);
-      sktns.push_back(ttn);
-      utchildren.push_back(kv);
-    }
-    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);
-    Trace("sygus-unif-debug2")
-        << "  Test evaluation of " << eut << "..." << std::endl;
-    eut = d_qe->getTermDatabaseSygus()->unfold(eut);
-    Trace("sygus-unif-debug2") << "  ...got " << eut;
-    Trace("sygus-unif-debug2") << ", type : " << eut.getType() << std::endl;
-
-    // candidate strategy
-    if (eut.getKind() == ITE)
-    {
-      cop_to_strat[cop].push_back(strat_ITE);
-    }
-    else if (eut.getKind() == STRING_CONCAT)
-    {
-      if (nrole != role_string_suffix)
-      {
-        cop_to_strat[cop].push_back(strat_CONCAT_PREFIX);
-      }
-      if (nrole != role_string_prefix)
-      {
-        cop_to_strat[cop].push_back(strat_CONCAT_SUFFIX);
-      }
-    }
-    else if (dt[j].isSygusIdFunc())
-    {
-      cop_to_strat[cop].push_back(strat_ID);
-    }
-
-    // the kinds for which there is a strategy
-    if (cop_to_strat.find(cop) != cop_to_strat.end())
-    {
-      // infer an injection from the arguments of the datatype
-      std::map<unsigned, unsigned> templ_injection;
-      std::vector<Node> vs;
-      std::vector<Node> ss;
-      std::map<Node, unsigned> templ_var_index;
-      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];
-        Trace("sygus-unif-debug2")
-            << "...set eval dt to " << sks[k] << std::endl;
-        Node esk = nm->mkNode(APPLY_UF, echildren);
-        vs.push_back(esk);
-        Node tvar = nm->mkSkolem("templ", esk.getType());
-        templ_var_index[tvar] = k;
-        Trace("sygus-unif-debug2") << "* template inference : looking for "
-                                   << tvar << " for arg " << k << std::endl;
-        ss.push_back(tvar);
-        Trace("sygus-unif-debug2")
-            << "* substitute : " << esk << " -> " << tvar << std::endl;
-      }
-      eut = eut.substitute(vs.begin(), vs.end(), ss.begin(), ss.end());
-      Trace("sygus-unif-debug2")
-          << "Constructor " << j << ", base term is " << eut << std::endl;
-      std::map<unsigned, Node> test_args;
-      if (dt[j].isSygusIdFunc())
-      {
-        test_args[0] = eut;
-      }
-      else
-      {
-        for (unsigned k = 0, size = eut.getNumChildren(); k < size; k++)
-        {
-          test_args[k] = eut[k];
-        }
-      }
-
-      // TODO : prefix grouping prefix/suffix
-      bool isAssoc = TermUtil::isAssoc(eut.getKind());
-      Trace("sygus-unif-debug2")
-          << eut.getKind() << " isAssoc = " << isAssoc << std::endl;
-      std::map<unsigned, std::vector<unsigned> > assoc_combine;
-      std::vector<unsigned> assoc_waiting;
-      int assoc_last_valid_index = -1;
-      for (std::pair<const unsigned, Node>& ta : test_args)
-      {
-        unsigned k = ta.first;
-        Node eut_c = ta.second;
-        // success if we can find a injection from args to sygus args
-        if (!inferTemplate(k, eut_c, templ_var_index, templ_injection))
-        {
-          Trace("sygus-unif-debug")
-              << "...fail: could not find injection (range)." << std::endl;
-          cop_to_strat.erase(cop);
-          break;
-        }
-        std::map<unsigned, unsigned>::iterator itti = templ_injection.find(k);
-        if (itti != templ_injection.end())
-        {
-          // if associative, combine arguments if it is the same variable
-          if (isAssoc && assoc_last_valid_index >= 0
-              && itti->second == templ_injection[assoc_last_valid_index])
-          {
-            templ_injection.erase(k);
-            assoc_combine[assoc_last_valid_index].push_back(k);
-          }
-          else
-          {
-            assoc_last_valid_index = (int)k;
-            if (!assoc_waiting.empty())
-            {
-              assoc_combine[k].insert(assoc_combine[k].end(),
-                                      assoc_waiting.begin(),
-                                      assoc_waiting.end());
-              assoc_waiting.clear();
-            }
-            assoc_combine[k].push_back(k);
-          }
-        }
-        else
-        {
-          // a ground argument
-          if (!isAssoc)
-          {
-            Trace("sygus-unif-debug")
-                << "...fail: could not find injection (functional)."
-                << std::endl;
-            cop_to_strat.erase(cop);
-            break;
-          }
-          else
-          {
-            if (assoc_last_valid_index >= 0)
-            {
-              assoc_combine[assoc_last_valid_index].push_back(k);
-            }
-            else
-            {
-              assoc_waiting.push_back(k);
-            }
-          }
-        }
-      }
-      if (cop_to_strat.find(cop) != cop_to_strat.end())
-      {
-        // construct the templates
-        if (!assoc_waiting.empty())
-        {
-          // could not find a way to fit some arguments into injection
-          cop_to_strat.erase(cop);
-        }
-        else
-        {
-          for (std::pair<const unsigned, Node>& ta : test_args)
-          {
-            unsigned k = ta.first;
-            Trace("sygus-unif-debug2")
-                << "- processing argument " << k << "..." << std::endl;
-            if (templ_injection.find(k) != templ_injection.end())
-            {
-              unsigned sk_index = templ_injection[k];
-              if (std::find(cop_to_carg_list[cop].begin(),
-                            cop_to_carg_list[cop].end(),
-                            sk_index)
-                  == cop_to_carg_list[cop].end())
-              {
-                cop_to_carg_list[cop].push_back(sk_index);
-              }
-              else
-              {
-                Trace("sygus-unif-debug")
-                    << "...fail: duplicate argument used" << std::endl;
-                cop_to_strat.erase(cop);
-                break;
-              }
-              // also store the template information, if necessary
-              Node teut;
-              if (isAssoc)
-              {
-                std::vector<unsigned>& ac = assoc_combine[k];
-                Assert(!ac.empty());
-                std::vector<Node> children;
-                for (unsigned ack = 0, size_ac = ac.size(); ack < size_ac;
-                     ack++)
-                {
-                  children.push_back(eut[ac[ack]]);
-                }
-                teut = children.size() == 1
-                           ? children[0]
-                           : nm->mkNode(eut.getKind(), children);
-                teut = Rewriter::rewrite(teut);
-              }
-              else
-              {
-                teut = ta.second;
-              }
-
-              if (!teut.isVar())
-              {
-                cop_to_child_templ[cop][k] = teut;
-                cop_to_child_templ_arg[cop][k] = ss[sk_index];
-                Trace("sygus-unif-debug")
-                    << "  Arg " << k << " (template : " << teut << " arg "
-                    << ss[sk_index] << "), index " << sk_index << std::endl;
-              }
-              else
-              {
-                Trace("sygus-unif-debug")
-                    << "  Arg " << k << ", index " << sk_index << std::endl;
-                Assert(teut == ss[sk_index]);
-              }
-            }
-            else
-            {
-              Assert(isAssoc);
-            }
-          }
-        }
-      }
-    }
-    if (cop_to_strat.find(cop) == cop_to_strat.end())
-    {
-      Trace("sygus-unif") << "...constructor " << cop
-                          << " does not correspond to a strategy." << std::endl;
-      search_this = true;
-    }
-    else
-    {
-      Trace("sygus-unif") << "-> constructor " << cop
-                          << " matches strategy for " << eut.getKind() << "..."
-                          << std::endl;
-      // collect children types
-      for (unsigned k = 0, size = cop_to_carg_list[cop].size(); k < size; k++)
-      {
-        TypeNode tn = sktns[cop_to_carg_list[cop][k]];
-        Trace("sygus-unif-debug")
-            << "   Child type " << k << " : "
-            << static_cast<DatatypeType>(tn.toType()).getDatatype().getName()
-            << std::endl;
-        cop_to_child_types[cop].push_back(tn);
-      }
-    }
-  }
-
-  // check whether we should also enumerate the current type
-  Trace("sygus-unif-debug2") << "  register this enumerator..." << std::endl;
-  registerEnumerator(ee, tn, erole, search_this);
-
-  if (cop_to_strat.empty())
-  {
-    Trace("sygus-unif") << "...consider " << dt.getName() << " a basic type"
-                        << std::endl;
-  }
-  else
-  {
-    for (std::pair<const Node, std::vector<StrategyType> >& cstr : cop_to_strat)
-    {
-      Node cop = cstr.first;
-      Trace("sygus-unif-debug")
-          << "Constructor " << cop << " has " << cstr.second.size()
-          << " strategies..." << std::endl;
-      for (unsigned s = 0, ssize = cstr.second.size(); s < ssize; s++)
-      {
-        EnumTypeInfoStrat* cons_strat = new EnumTypeInfoStrat;
-        StrategyType strat = cstr.second[s];
-
-        cons_strat->d_this = strat;
-        cons_strat->d_cons = cop;
-        Trace("sygus-unif-debug")
-            << "Process strategy #" << s << " for operator : " << cop << " : "
-            << strat << std::endl;
-        Assert(cop_to_child_types.find(cop) != cop_to_child_types.end());
-        std::vector<TypeNode>& childTypes = cop_to_child_types[cop];
-        Assert(cop_to_carg_list.find(cop) != cop_to_carg_list.end());
-        std::vector<unsigned>& cargList = cop_to_carg_list[cop];
-
-        std::vector<Node> sol_templ_children;
-        sol_templ_children.resize(cop_to_sks[cop].size());
-
-        for (unsigned j = 0, csize = childTypes.size(); j < csize; j++)
-        {
-          // calculate if we should allocate a new enumerator : should be true
-          // if we have a new role
-          NodeRole nrole_c = nrole;
-          if (strat == strat_ITE)
-          {
-            if (j == 0)
-            {
-              nrole_c = role_ite_condition;
-            }
-          }
-          else if (strat == strat_CONCAT_PREFIX)
-          {
-            if ((j + 1) < childTypes.size())
-            {
-              nrole_c = role_string_prefix;
-            }
-          }
-          else if (strat == strat_CONCAT_SUFFIX)
-          {
-            if (j > 0)
-            {
-              nrole_c = role_string_suffix;
-            }
-          }
-          // in all other cases, role is same as parent
-
-          // register the child type
-          TypeNode ct = childTypes[j];
-          Node csk = cop_to_sks[cop][cargList[j]];
-          cons_strat->d_sol_templ_args.push_back(csk);
-          sol_templ_children[cargList[j]] = csk;
-
-          EnumRole erole_c = getEnumeratorRoleForNodeRole(nrole_c);
-          // make the enumerator
-          Node et;
-          if (cop_to_child_templ[cop].find(j) != cop_to_child_templ[cop].end())
-          {
-            // it is templated, allocate a fresh variable
-            et = nm->mkSkolem("et", ct);
-            Trace("sygus-unif-debug")
-                << "...enumerate " << et << " of type "
-                << ((DatatypeType)ct.toType()).getDatatype().getName();
-            Trace("sygus-unif-debug") << " for arg " << j << " of "
-                                      << static_cast<DatatypeType>(tn.toType())
-                                             .getDatatype()
-                                             .getName()
-                                      << std::endl;
-            registerEnumerator(et, ct, erole_c, true);
-            d_einfo[et].d_template = cop_to_child_templ[cop][j];
-            d_einfo[et].d_template_arg = cop_to_child_templ_arg[cop][j];
-            Assert(!d_einfo[et].d_template.isNull());
-            Assert(!d_einfo[et].d_template_arg.isNull());
-          }
-          else
-          {
-            Trace("sygus-unif-debug")
-                << "...child type enumerate "
-                << ((DatatypeType)ct.toType()).getDatatype().getName()
-                << ", node role = " << nrole_c << std::endl;
-            collectEnumeratorTypes(ct, nrole_c);
-            // otherwise use the previous
-            Assert(d_cinfo.d_tinfo[ct].d_enum.find(erole_c)
-                   != d_cinfo.d_tinfo[ct].d_enum.end());
-            et = d_cinfo.d_tinfo[ct].d_enum[erole_c];
-          }
-          Trace("sygus-unif-debug")
-              << "Register child enumerator " << et << ", arg " << j << " of "
-              << cop << ", role = " << erole_c << std::endl;
-          Assert(!et.isNull());
-          cons_strat->d_cenum.push_back(std::pair<Node, NodeRole>(et, nrole_c));
-        }
-        // children that are unused in the strategy can be arbitrary
-        for (unsigned j = 0, stsize = sol_templ_children.size(); j < stsize;
-             j++)
-        {
-          if (sol_templ_children[j].isNull())
-          {
-            sol_templ_children[j] = cop_to_sks[cop][j].getType().mkGroundTerm();
-          }
-        }
-        sol_templ_children.insert(sol_templ_children.begin(), cop);
-        cons_strat->d_sol_templ =
-            nm->mkNode(APPLY_CONSTRUCTOR, sol_templ_children);
-        if (strat == strat_CONCAT_SUFFIX)
-        {
-          std::reverse(cons_strat->d_cenum.begin(), cons_strat->d_cenum.end());
-          std::reverse(cons_strat->d_sol_templ_args.begin(),
-                       cons_strat->d_sol_templ_args.end());
-        }
-        if (Trace.isOn("sygus-unif"))
-        {
-          Trace("sygus-unif") << "Initialized strategy " << strat;
-          Trace("sygus-unif")
-              << " for "
-              << static_cast<DatatypeType>(tn.toType()).getDatatype().getName()
-              << ", operator " << cop;
-          Trace("sygus-unif") << ", #children = " << cons_strat->d_cenum.size()
-                              << ", solution template = (lambda ( ";
-          for (const Node& targ : cons_strat->d_sol_templ_args)
-          {
-            Trace("sygus-unif") << targ << " ";
-          }
-          Trace("sygus-unif") << ") " << cons_strat->d_sol_templ << ")";
-          Trace("sygus-unif") << std::endl;
-        }
-        // make the strategy
-        snode.d_strats.push_back(cons_strat);
-      }
-    }
-  }
-}
-
-bool SygusUnif::inferTemplate(unsigned k,
-                              Node n,
-                              std::map<Node, unsigned>& templ_var_index,
-                              std::map<unsigned, unsigned>& templ_injection)
-{
-  if (n.getNumChildren() == 0)
-  {
-    std::map<Node, unsigned>::iterator itt = templ_var_index.find(n);
-    if (itt != templ_var_index.end())
-    {
-      unsigned kk = itt->second;
-      std::map<unsigned, unsigned>::iterator itti = templ_injection.find(k);
-      if (itti == templ_injection.end())
-      {
-        Trace("sygus-unif-debug")
-            << "...set template injection " << k << " -> " << kk << std::endl;
-        templ_injection[k] = kk;
-      }
-      else if (itti->second != kk)
-      {
-        // two distinct variables in this term, we fail
-        return false;
-      }
-    }
-    return true;
-  }
-  else
-  {
-    for (unsigned i = 0; i < n.getNumChildren(); i++)
-    {
-      if (!inferTemplate(k, n[i], templ_var_index, templ_injection))
-      {
-        return false;
-      }
-    }
-  }
-  return true;
-}
-
-void SygusUnif::staticLearnRedundantOps(std::vector<Node>& lemmas)
-{
-  for (unsigned i = 0; i < d_cinfo.d_esym_list.size(); i++)
-  {
-    Node e = d_cinfo.d_esym_list[i];
-    std::map<Node, EnumInfo>::iterator itn = d_einfo.find(e);
-    Assert(itn != d_einfo.end());
-    // see if there is anything we can eliminate
-    Trace("sygus-unif")
-        << "* Search enumerator #" << i << " : type "
-        << ((DatatypeType)e.getType().toType()).getDatatype().getName()
-        << " : ";
-    Trace("sygus-unif") << e << " has " << itn->second.d_enum_slave.size()
-                        << " slaves:" << std::endl;
-    for (unsigned j = 0; j < itn->second.d_enum_slave.size(); j++)
-    {
-      Node es = itn->second.d_enum_slave[j];
-      std::map<Node, EnumInfo>::iterator itns = d_einfo.find(es);
-      Assert(itns != d_einfo.end());
-      Trace("sygus-unif") << "  " << es << ", role = " << itns->second.getRole()
-                          << std::endl;
-    }
-  }
-  Trace("sygus-unif") << std::endl;
-  Trace("sygus-unif") << "Strategy for candidate " << d_candidate
-                      << " is : " << std::endl;
-  std::map<Node, std::map<NodeRole, bool> > visited;
-  std::map<Node, std::map<unsigned, bool> > needs_cons;
-  staticLearnRedundantOps(
-      d_cinfo.getRootEnumerator(), role_equal, visited, needs_cons, 0, false);
-  // now, check the needs_cons map
-  for (std::pair<const Node, std::map<unsigned, bool> >& nce : needs_cons)
-  {
-    Node em = nce.first;
-    const Datatype& dt =
-        static_cast<DatatypeType>(em.getType().toType()).getDatatype();
-    for (std::pair<const unsigned, bool>& nc : nce.second)
-    {
-      Assert(nc.first < dt.getNumConstructors());
-      if (!nc.second)
-      {
-        Node tst =
-            datatypes::DatatypesRewriter::mkTester(em, nc.first, dt).negate();
-        if (std::find(lemmas.begin(), lemmas.end(), tst) == lemmas.end())
-        {
-          Trace("sygus-unif")
-              << "...can exclude based on  : " << tst << std::endl;
-          lemmas.push_back(tst);
-        }
-      }
-    }
-  }
-}
-
-void SygusUnif::staticLearnRedundantOps(
-    Node e,
-    NodeRole nrole,
-    std::map<Node, std::map<NodeRole, bool> >& visited,
-    std::map<Node, std::map<unsigned, bool> >& needs_cons,
-    int ind,
-    bool isCond)
-{
-  std::map<Node, EnumInfo>::iterator itn = d_einfo.find(e);
-  Assert(itn != d_einfo.end());
-
-  if (visited[e].find(nrole) == visited[e].end()
-      || (isCond && !itn->second.isConditional()))
-  {
-    visited[e][nrole] = true;
-    // if conditional
-    if (isCond)
-    {
-      itn->second.setConditional();
-    }
-    indent("sygus-unif", ind);
-    Trace("sygus-unif") << e << " :: node role : " << nrole;
-    Trace("sygus-unif")
-        << ", type : "
-        << ((DatatypeType)e.getType().toType()).getDatatype().getName();
-    if (isCond)
-    {
-      Trace("sygus-unif") << ", conditional";
-    }
-    Trace("sygus-unif") << ", enum role : " << itn->second.getRole();
-
-    if (itn->second.isTemplated())
-    {
-      Trace("sygus-unif") << ", templated : (lambda "
-                          << itn->second.d_template_arg << " "
-                          << itn->second.d_template << ")" << std::endl;
-    }
-    else
-    {
-      Trace("sygus-unif") << std::endl;
-      TypeNode etn = e.getType();
-
-      // enumerator type info
-      std::map<TypeNode, EnumTypeInfo>::iterator itt =
-          d_cinfo.d_tinfo.find(etn);
-      Assert(itt != d_cinfo.d_tinfo.end());
-      EnumTypeInfo& tinfo = itt->second;
-
-      // strategy info
-      std::map<NodeRole, StrategyNode>::iterator itsn =
-          tinfo.d_snodes.find(nrole);
-      Assert(itsn != tinfo.d_snodes.end());
-      StrategyNode& snode = itsn->second;
-
-      if (snode.d_strats.empty())
-      {
-        return;
-      }
-      std::map<unsigned, bool> needs_cons_curr;
-      // various strategies
-      for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++)
-      {
-        EnumTypeInfoStrat* etis = snode.d_strats[j];
-        StrategyType strat = etis->d_this;
-        bool newIsCond = isCond || strat == strat_ITE;
-        indent("sygus-unif", ind + 1);
-        Trace("sygus-unif") << "Strategy : " << strat
-                            << ", from cons : " << etis->d_cons << std::endl;
-        int cindex = Datatype::indexOf(etis->d_cons.toExpr());
-        Assert(cindex != -1);
-        needs_cons_curr[static_cast<unsigned>(cindex)] = false;
-        for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
-        {
-          // recurse
-          staticLearnRedundantOps(
-              cec.first, cec.second, visited, needs_cons, ind + 2, newIsCond);
-        }
-      }
-      // get the master enumerator for the type of this enumerator
-      std::map<TypeNode, Node>::iterator itse = d_cinfo.d_search_enum.find(etn);
-      if (itse == d_cinfo.d_search_enum.end())
-      {
-        return;
-      }
-      Node em = itse->second;
-      Assert(!em.isNull());
-      // get the current datatype
-      const Datatype& dt =
-          static_cast<DatatypeType>(etn.toType()).getDatatype();
-      // all constructors that are not a part of a strategy are needed
-      for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++)
-      {
-        if (needs_cons_curr.find(j) == needs_cons_curr.end())
-        {
-          needs_cons_curr[j] = true;
-        }
-      }
-      // update the constructors that the master enumerator needs
-      if (needs_cons.find(em) == needs_cons.end())
-      {
-        needs_cons[em] = needs_cons_curr;
-      }
-      else
-      {
-        for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++)
-        {
-          needs_cons[em][j] = needs_cons[em][j] || needs_cons_curr[j];
-        }
-      }
-    }
-  }
-  else
-  {
-    indent("sygus-unif", ind);
-    Trace("sygus-unif") << e << " :: node role : " << nrole << std::endl;
-  }
-}
-
 // ------------------------------------ solution construction from enumeration
 
-bool SygusUnif::useStrContainsEnumeratorExclude(Node x, EnumInfo& ei)
+bool SygusUnif::useStrContainsEnumeratorExclude(Node e)
 {
-  TypeNode xbt = d_tds->sygusToBuiltinType(x.getType());
+  TypeNode xbt = d_tds->sygusToBuiltinType(e.getType());
   if (xbt.isString())
   {
-    std::map<Node, bool>::iterator itx = d_use_str_contains_eexc.find(x);
+    std::map<Node, bool>::iterator itx = d_use_str_contains_eexc.find(e);
     if (itx != d_use_str_contains_eexc.end())
     {
       return itx->second;
     }
-    Trace("sygus-pbe-enum-debug")
-        << "Is " << x << " is str.contains exclusion?" << std::endl;
-    d_use_str_contains_eexc[x] = true;
+    Trace("sygus-pbe-enum-debug") << "Is " << e << " is str.contains exclusion?"
+                                  << std::endl;
+    d_use_str_contains_eexc[e] = true;
+    EnumInfo& ei = d_strategy.getEnumInfo(e);
     for (const Node& sn : ei.d_enum_slave)
     {
-      std::map<Node, EnumInfo>::iterator itv = d_einfo.find(sn);
-      EnumRole er = itv->second.getRole();
+      EnumInfo& eis = d_strategy.getEnumInfo(sn);
+      EnumRole er = eis.getRole();
       if (er != enum_io && er != enum_concat_term)
       {
         Trace("sygus-pbe-enum-debug") << "  incompatible slave : " << sn
                                       << ", role = " << er << std::endl;
-        d_use_str_contains_eexc[x] = false;
+        d_use_str_contains_eexc[e] = false;
         return false;
       }
-      if (itv->second.isConditional())
+      if (eis.isConditional())
       {
         Trace("sygus-pbe-enum-debug")
             << "  conditional slave : " << sn << std::endl;
-        d_use_str_contains_eexc[x] = false;
+        d_use_str_contains_eexc[e] = false;
         return false;
       }
     }
     Trace("sygus-pbe-enum-debug")
         << "...can use str.contains exclusion." << std::endl;
-    return d_use_str_contains_eexc[x];
+    return d_use_str_contains_eexc[e];
   }
   return false;
 }
 
-bool SygusUnif::getExplanationForEnumeratorExclude(Node x,
+bool SygusUnif::getExplanationForEnumeratorExclude(Node e,
                                                    Node v,
                                                    std::vector<Node>& results,
-                                                   EnumInfo& ei,
                                                    std::vector<Node>& exp)
 {
-  if (useStrContainsEnumeratorExclude(x, ei))
+  if (useStrContainsEnumeratorExclude(e))
   {
     NodeManager* nm = NodeManager::currentNM();
     // This check whether the example evaluates to something that is larger than
@@ -1536,9 +798,9 @@ bool SygusUnif::getExplanationForEnumeratorExclude(Node x,
     }
     // check if all examples had longer length that the output
     Assert(d_examples_out.size() == results.size());
-    Trace("sygus-pbe-cterm-debug")
-        << "Check enumerator exclusion for " << x << " -> "
-        << d_tds->sygusToBuiltin(v) << " based on str.contains." << std::endl;
+    Trace("sygus-pbe-cterm-debug") << "Check enumerator exclusion for " << e
+                                   << " -> " << d_tds->sygusToBuiltin(v)
+                                   << " based on str.contains." << std::endl;
     std::vector<unsigned> cmp_indices;
     for (unsigned i = 0, size = results.size(); i < size; i++)
     {
@@ -1562,9 +824,9 @@ bool SygusUnif::getExplanationForEnumeratorExclude(Node x,
     {
       // we check invariance with respect to a negative contains test
       NegContainsSygusInvarianceTest ncset;
-      ncset.init(x, d_examples, d_examples_out, cmp_indices);
+      ncset.init(e, d_examples, d_examples_out, cmp_indices);
       // construct the generalized explanation
-      d_tds->getExplain()->getExplanationFor(x, v, exp, ncset);
+      d_tds->getExplain()->getExplanationFor(e, v, exp, ncset);
       Trace("sygus-pbe-cterm")
           << "PBE-cterm : enumerator exclude " << d_tds->sygusToBuiltin(v)
           << " due to negative containment." << std::endl;
@@ -1574,9 +836,7 @@ bool SygusUnif::getExplanationForEnumeratorExclude(Node x,
   return false;
 }
 
-void SygusUnif::EnumInfo::addEnumValue(SygusUnif* pbe,
-                                       Node v,
-                                       std::vector<Node>& results)
+void SygusUnif::EnumCache::addEnumValue(Node v, std::vector<Node>& results)
 {
   // should not have been enumerated before
   Assert(d_enum_val_to_index.find(v) == d_enum_val_to_index.end());
@@ -1585,29 +845,6 @@ void SygusUnif::EnumInfo::addEnumValue(SygusUnif* pbe,
   d_enum_vals_res.push_back(results);
 }
 
-void SygusUnif::EnumInfo::initialize(EnumRole role) { d_role = role; }
-
-void SygusUnif::EnumInfo::setSolved(Node slv) { d_enum_solved = slv; }
-
-void SygusUnif::CandidateInfo::initialize(Node c)
-{
-  d_this_candidate = c;
-  d_root = c.getType();
-}
-
-void SygusUnif::CandidateInfo::initializeType(TypeNode tn)
-{
-  d_tinfo[tn].d_this_type = tn;
-  d_tinfo[tn].d_parent = this;
-}
-
-Node SygusUnif::CandidateInfo::getRootEnumerator()
-{
-  std::map<EnumRole, Node>::iterator it = d_tinfo[d_root].d_enum.find(enum_io);
-  Assert(it != d_tinfo[d_root].d_enum.end());
-  return it->second;
-}
-
 Node SygusUnif::constructBestSolvedTerm(std::vector<Node>& solved,
                                         UnifContext& x)
 {
@@ -1685,24 +922,22 @@ Node SygusUnif::constructSolution(Node e,
     Trace("sygus-pbe-dt-debug") << std::endl;
   }
   // enumerator type info
-  std::map<TypeNode, EnumTypeInfo>::iterator itt = d_cinfo.d_tinfo.find(etn);
-  Assert(itt != d_cinfo.d_tinfo.end());
-  EnumTypeInfo& tinfo = itt->second;
+  EnumTypeInfo& tinfo = d_strategy.getEnumTypeInfo(etn);
 
   // get the enumerator information
-  std::map<Node, EnumInfo>::iterator itn = d_einfo.find(e);
-  Assert(itn != d_einfo.end());
-  EnumInfo& einfo = itn->second;
+  EnumInfo& einfo = d_strategy.getEnumInfo(e);
+
+  EnumCache& ecache = d_ecache[e];
 
   Node ret_dt;
   if (nrole == role_equal)
   {
     if (!x.isReturnValueModified())
     {
-      if (einfo.isSolved())
+      if (ecache.isSolved())
       {
         // this type has a complete solution
-        ret_dt = einfo.getSolved();
+        ret_dt = ecache.getSolved();
         indent("sygus-pbe-dt", ind);
         Trace("sygus-pbe-dt") << "return PBE: success : solved "
                               << d_tds->sygusToBuiltin(ret_dt) << std::endl;
@@ -1712,7 +947,7 @@ Node SygusUnif::constructSolution(Node e,
       {
         // could be conditionally solved
         std::vector<Node> subsumed_by;
-        einfo.d_term_trie.getSubsumedBy(x.d_vals, true, subsumed_by);
+        ecache.d_term_trie.getSubsumedBy(x.d_vals, true, subsumed_by);
         if (!subsumed_by.empty())
         {
           ret_dt = constructBestSolvedTerm(subsumed_by, x);
@@ -1734,37 +969,25 @@ Node SygusUnif::constructSolution(Node e,
       {
         // check if a current value that closes all examples
         // get the term enumerator for this type
-        bool success = true;
-        std::map<Node, EnumInfo>::iterator itet;
         std::map<EnumRole, Node>::iterator itnt =
             tinfo.d_enum.find(enum_concat_term);
-        if (itnt != itt->second.d_enum.end())
+        if (itnt != tinfo.d_enum.end())
         {
           Node et = itnt->second;
-          itet = d_einfo.find(et);
-          Assert(itet != d_einfo.end());
-        }
-        else
-        {
-          success = false;
-        }
-        if (success)
-        {
+
+          EnumCache& ecachet = d_ecache[et];
           // get the current examples
           std::vector<String> ex_vals;
           x.getCurrentStrings(this, d_examples_out, ex_vals);
-          Assert(itn->second.d_enum_vals.size()
-                 == itn->second.d_enum_vals_res.size());
+          Assert(ecache.d_enum_vals.size() == ecache.d_enum_vals_res.size());
 
           // test each example in the term enumerator for the type
           std::vector<Node> str_solved;
-          for (unsigned i = 0, size = itet->second.d_enum_vals.size(); i < size;
-               i++)
+          for (unsigned i = 0, size = ecachet.d_enum_vals.size(); i < size; i++)
           {
-            if (x.isStringSolved(
-                    this, ex_vals, itet->second.d_enum_vals_res[i]))
+            if (x.isStringSolved(this, ex_vals, ecachet.d_enum_vals_res[i]))
             {
-              str_solved.push_back(itet->second.d_enum_vals[i]);
+              str_solved.push_back(ecachet.d_enum_vals[i]);
             }
           }
           if (!str_solved.empty())
@@ -1809,21 +1032,21 @@ Node SygusUnif::constructSolution(Node e,
 
       // check if there is a value for which is a prefix/suffix of all active
       // examples
-      Assert(einfo.d_enum_vals.size() == einfo.d_enum_vals_res.size());
+      Assert(ecache.d_enum_vals.size() == ecache.d_enum_vals_res.size());
 
-      for (unsigned i = 0, size = einfo.d_enum_vals.size(); i < size; i++)
+      for (unsigned i = 0, size = ecache.d_enum_vals.size(); i < size; i++)
       {
-        Node val_t = einfo.d_enum_vals[i];
+        Node val_t = ecache.d_enum_vals[i];
         Assert(incr.find(val_t) == incr.end());
         indent("sygus-pbe-dt-debug", ind);
         Trace("sygus-pbe-dt-debug")
             << "increment string values : " << val_t << " : ";
-        Assert(einfo.d_enum_vals_res[i].size() == d_examples_out.size());
+        Assert(ecache.d_enum_vals_res[i].size() == d_examples_out.size());
         unsigned tot = 0;
         bool exsuccess = x.getStringIncrement(this,
                                               isPrefix,
                                               ex_vals,
-                                              einfo.d_enum_vals_res[i],
+                                              ecache.d_enum_vals_res[i],
                                               incr[val_t],
                                               tot);
         if (!exsuccess)
@@ -1890,7 +1113,7 @@ Node SygusUnif::constructSolution(Node e,
         // get an eligible strategy index
         unsigned sindex = 0;
         while (sindex < snode.d_strats.size()
-               && !snode.d_strats[sindex]->isValid(this, x))
+               && !snode.d_strats[sindex]->isValid(&x))
         {
           sindex++;
         }
@@ -1940,16 +1163,14 @@ Node SygusUnif::constructSolution(Node e,
           std::vector<Node> prev;
           if (strat == strat_ITE && sc > 0)
           {
-            std::map<Node, EnumInfo>::iterator itnc =
-                d_einfo.find(split_cond_enum);
-            Assert(itnc != d_einfo.end());
+            EnumCache& ecache_cond = d_ecache[split_cond_enum];
             Assert(split_cond_res_index >= 0);
             Assert(split_cond_res_index
-                   < (int)itnc->second.d_enum_vals_res.size());
+                   < (int)ecache_cond.d_enum_vals_res.size());
             prev = x.d_vals;
             bool ret = x.updateContext(
                 this,
-                itnc->second.d_enum_vals_res[split_cond_res_index],
+                ecache_cond.d_enum_vals_res[split_cond_res_index],
                 sc == 1);
             AlwaysAssert(ret);
           }
@@ -1959,10 +1180,7 @@ Node SygusUnif::constructSolution(Node e,
           {
             Node ce = cenum.first;
 
-            // register the condition enumerator
-            std::map<Node, EnumInfo>::iterator itnc = d_einfo.find(ce);
-            Assert(itnc != d_einfo.end());
-            EnumInfo& einfo_child = itnc->second;
+            EnumCache& ecache_child = d_ecache[ce];
 
             // only used if the return value is not modified
             if (!x.isReturnValueModified())
@@ -1973,25 +1191,24 @@ Node SygusUnif::constructSolution(Node e,
                     << "  reg : PBE: Look for direct solutions for conditional "
                        "enumerator "
                     << ce << " ... " << std::endl;
-                Assert(einfo_child.d_enum_vals.size()
-                       == einfo_child.d_enum_vals_res.size());
+                Assert(ecache_child.d_enum_vals.size()
+                       == ecache_child.d_enum_vals_res.size());
                 for (unsigned i = 1; i <= 2; i++)
                 {
                   std::pair<Node, NodeRole>& te_pair = etis->d_cenum[i];
                   Node te = te_pair.first;
-                  std::map<Node, EnumInfo>::iterator itnt = d_einfo.find(te);
-                  Assert(itnt != d_einfo.end());
+                  EnumCache& ecache_te = d_ecache[te];
                   bool branch_pol = (i == 1);
                   // for each condition, get terms that satisfy it in this
                   // branch
-                  for (unsigned k = 0, size = einfo_child.d_enum_vals.size();
+                  for (unsigned k = 0, size = ecache_child.d_enum_vals.size();
                        k < size;
                        k++)
                   {
-                    Node cond = einfo_child.d_enum_vals[k];
+                    Node cond = ecache_child.d_enum_vals[k];
                     std::vector<Node> solved;
-                    itnt->second.d_term_trie.getSubsumedBy(
-                        einfo_child.d_enum_vals_res[k], branch_pol, solved);
+                    ecache_te.d_term_trie.getSubsumedBy(
+                        ecache_child.d_enum_vals_res[k], branch_pol, solved);
                     Trace("sygus-pbe-dt-debug2")
                         << "  reg : PBE: " << d_tds->sygusToBuiltin(cond)
                         << " has " << solved.size() << " solutions in branch "
@@ -2016,7 +1233,7 @@ Node SygusUnif::constructSolution(Node e,
             // distinguishable
             std::map<int, std::vector<Node> > possible_cond;
             std::map<Node, int> solved_cond;  // stores branch
-            einfo_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond);
+            ecache_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond);
 
             std::map<int, std::vector<Node> >::iterator itpc =
                 possible_cond.find(0);
@@ -2101,13 +1318,13 @@ Node SygusUnif::constructSolution(Node e,
             }
             if (!rec_c.isNull())
             {
-              Assert(einfo_child.d_enum_val_to_index.find(rec_c)
-                     != einfo_child.d_enum_val_to_index.end());
-              split_cond_res_index = einfo_child.d_enum_val_to_index[rec_c];
+              Assert(ecache_child.d_enum_val_to_index.find(rec_c)
+                     != ecache_child.d_enum_val_to_index.end());
+              split_cond_res_index = ecache_child.d_enum_val_to_index[rec_c];
               split_cond_enum = ce;
               Assert(split_cond_res_index >= 0);
               Assert(split_cond_res_index
-                     < (int)einfo_child.d_enum_vals_res.size());
+                     < (int)ecache_child.d_enum_vals_res.size());
             }
           }
           else
@@ -2163,27 +1380,6 @@ Node SygusUnif::constructSolution(Node e,
   return ret_dt;
 }
 
-bool SygusUnif::EnumTypeInfoStrat::isValid(SygusUnif* pbe, UnifContext& x)
-{
-  if ((x.d_has_string_pos == role_string_prefix
-       && d_this == strat_CONCAT_SUFFIX)
-      || (x.d_has_string_pos == role_string_suffix
-          && d_this == strat_CONCAT_PREFIX))
-  {
-    return false;
-  }
-  return true;
-}
-
-SygusUnif::StrategyNode::~StrategyNode()
-{
-  for (unsigned j = 0, size = d_strats.size(); j < size; j++)
-  {
-    delete d_strats[j];
-  }
-  d_strats.clear();
-}
-
 void SygusUnif::indent(const char* c, int ind)
 {
   if (Trace.isOn(c))
diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h
index 9bb321a09..4e7806bf0 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.h
+++ b/src/theory/quantifiers/sygus/sygus_unif.h
@@ -265,11 +265,11 @@ class SubsumeTrie
  *
  * This class maintains:
  * (1) A "strategy tree" based on the syntactic restrictions for f that is
- * constructed during initialize,
+ * constructed during initialize (d_strategy),
  * (2) A set of input/output examples that are the specification for f. This
  * can be updated via calls to resetExmaples/addExamples,
- * (3) A set of terms that have been enumerated for enumerators. This can be
- * updated via calls to notifyEnumeration.
+ * (3) A set of terms that have been enumerated for enumerators (d_ecache). This
+ * can be updated via calls to notifyEnumeration.
  *
  * Based on the above, solutions can be constructed via calls to
  * constructSolution.
@@ -353,72 +353,25 @@ class SygusUnif
                         bool pol = true);
   //-----------------------end debug printing
 
-  //------------------------------ representation of a enumeration strategy
   /**
   * This class stores information regarding an enumerator, including:
-  * - Information regarding the role of this enumerator (see EnumRole), its
-  * parent, whether it is templated, its slave enumerators, and so on, and
-  * - A database of values that have been enumerated for this enumerator.
-  *
-  * We say an enumerator is a master enumerator if it is the variable that
-  * we use to enumerate values for its sort. Master enumerators may have
-  * (possibly multiple) slave enumerators, stored in d_enum_slave. We make
-  * the first enumerator for each type a master enumerator, and any additional
-  * ones slaves of it.
+  * a database of values that have been enumerated for this enumerator.
   */
-  class EnumInfo
+  class EnumCache
   {
    public:
-    EnumInfo() : d_role(enum_io), d_is_conditional(false) {}
-    /** initialize this class
-    *
-    * c is the parent function-to-synthesize
-    * role is the "role" the enumerator plays in the high-level strategy,
-    *   which is one of enum_* above.
-    */
-    void initialize(EnumRole role);
-    /** is this enumerator associated with a template? */
-    bool isTemplated() { return !d_template.isNull(); }
-    /** set conditional
-      *
-      * This flag is set to true if this enumerator may not apply to all
-      * input/output examples. For example, if this enumerator is used
-      * as an output value beneath a conditional in an instance of strat_ITE,
-      * then this enumerator is conditional.
-      */
-    void setConditional() { d_is_conditional = true; }
-    /** is conditional */
-    bool isConditional() { return d_is_conditional; }
-    /** get the role of this enumerator */
-    EnumRole getRole() { return d_role; }
-    /** enumerator template
-    *
-    * If d_template non-null, enumerated values V are immediately transformed to
-    * d_template { d_template_arg -> V }.
-    */
-    Node d_template;
-    Node d_template_arg;
-    /**
-    * Slave enumerators of this enumerator. These are other enumerators that
-    * have the same type, but a different role in the strategy tree. We
-    * generally
-    * only use one enumerator per type, and hence these slaves are notified when
-    * values are enumerated for this enumerator.
-    */
-    std::vector<Node> d_enum_slave;
-
-    //---------------------------enumerated values
+    EnumCache() {}
     /**
     * Notify this class that the term v has been enumerated for this enumerator.
     * Its evaluation under the set of examples in pbe are stored in results.
     */
-    void addEnumValue(SygusUnif* pbe, Node v, std::vector<Node>& results);
+    void addEnumValue(Node v, std::vector<Node>& results);
     /**
     * Notify this class that slv is the complete solution to the synthesis
     * conjecture. This occurs rarely, for instance, when during an ITE strategy
     * we find that a single enumerated term covers all examples.
     */
-    void setSolved(Node slv);
+    void setSolved(Node slv) { d_enum_solved = slv; }
     /** Have we been notified that a complete solution exists? */
     bool isSolved() { return !d_enum_solved.isNull(); }
     /** Get the complete solution to the synthesis conjecture. */
@@ -444,174 +397,61 @@ class SygusUnif
     * enum_concat_term).
     */
     SubsumeTrie d_term_trie;
-    //---------------------------end enumerated values
    private:
     /**
       * Whether an enumerated value for this conjecture has solved the entire
       * conjecture.
       */
     Node d_enum_solved;
-    /** the role of this enumerator (one of enum_* above). */
-    EnumRole d_role;
-    /** is this enumerator conditional */
-    bool d_is_conditional;
   };
   /** maps enumerators to the information above */
-  std::map<Node, EnumInfo> d_einfo;
+  std::map<Node, EnumCache> d_ecache;
 
-  class CandidateInfo;
-  class EnumTypeInfoStrat;
-
-  /** represents a node in the strategy graph
-   *
-   * It contains a list of possible strategies which are tried during calls
-   * to constructSolution.
-   */
-  class StrategyNode
-  {
-   public:
-    StrategyNode() {}
-    ~StrategyNode();
-    /** the set of strategies to try at this node in the strategy graph */
-    std::vector<EnumTypeInfoStrat*> d_strats;
-  };
-
-  /** stores enumerators and strategies for a SyGuS datatype type */
-  class EnumTypeInfo
-  {
-   public:
-    EnumTypeInfo() : d_parent(NULL) {}
-    /** the parent candidate info (see below) */
-    CandidateInfo* d_parent;
-    /** the type that this information is for */
-    TypeNode d_this_type;
-    /** map from enum roles to enumerators for this type */
-    std::map<EnumRole, Node> d_enum;
-    /** map from node roles to strategy nodes */
-    std::map<NodeRole, StrategyNode> d_snodes;
-  };
-
-  /** stores strategy and enumeration information for a function-to-synthesize
+  /**
+   * Whether we will try to construct solution on the next call to
+   * constructSolution. This flag is set to true when we successfully
+   * register a new value for an enumerator.
    */
-  class CandidateInfo
-  {
-   public:
-    CandidateInfo() : d_check_sol(false), d_cond_count(0) {}
-    Node d_this_candidate;
-    /**
-     * The root sygus datatype for the function-to-synthesize,
-     * which encodes the overall syntactic restrictions on the space
-     * of solutions.
-     */
-    TypeNode d_root;
-    /** Info for sygus datatype type occurring in a field of d_root */
-    std::map<TypeNode, EnumTypeInfo> d_tinfo;
-    /** list of all enumerators for the function-to-synthesize */
-    std::vector<Node> d_esym_list;
-    /**
-     * Maps sygus datatypes to their search enumerator. This is the (single)
-     * enumerator of that type that we enumerate values for.
-     */
-    std::map<TypeNode, Node> d_search_enum;
-    bool d_check_sol;
-    unsigned d_cond_count;
-    Node d_solution;
-    void initialize(Node c);
-    void initializeType(TypeNode tn);
-    Node getRootEnumerator();
-  };
+  bool d_check_sol;
+  /** The number of values we have enumerated for all enumerators. */
+  unsigned d_cond_count;
+  /** The solution for the function of this class, if one has been found */
+  Node d_solution;
   /** the candidate for this class */
   Node d_candidate;
   /** maps a function-to-synthesize to the above information */
-  CandidateInfo d_cinfo;
+  SygusUnifStrategy d_strategy;
 
-  //------------------------------ representation of an enumeration strategy
   /** domain-specific enumerator exclusion techniques
    *
-   * Returns true if the value v for x can be excluded based on a
+   * Returns true if the value v for e can be excluded based on a
    * domain-specific exclusion technique like the ones below.
    *
    * results : the values of v under the input examples,
-   * ei : the enumerator information for x,
    * exp : if this function returns true, then exp contains a (possibly
    * generalize) explanation for why v can be excluded.
    */
-  bool getExplanationForEnumeratorExclude(Node x,
+  bool getExplanationForEnumeratorExclude(Node e,
                                           Node v,
                                           std::vector<Node>& results,
-                                          EnumInfo& ei,
                                           std::vector<Node>& exp);
-  /** returns true if we can exlude values of x based on negative str.contains
+  /** returns true if we can exlude values of e based on negative str.contains
    *
-   * Values v for x may be excluded if we realize that the value of v under the
+   * Values v for e may be excluded if we realize that the value of v under the
    * substitution for some input example will never be contained in some output
    * example. For details on this technique, see NegContainsSygusInvarianceTest
    * in sygus_invariance.h.
    *
-   * This function depends on whether x is being used to enumerate values
+   * This function depends on whether e is being used to enumerate values
    * for any node that is conditional in the strategy graph. For example,
    * nodes that are children of ITE strategy nodes are conditional. If any node
    * is conditional, then this function returns false.
    */
-  bool useStrContainsEnumeratorExclude(Node x, EnumInfo& ei);
+  bool useStrContainsEnumeratorExclude(Node e);
   /** cache for the above function */
   std::map<Node, bool> d_use_str_contains_eexc;
 
-  //------------------------------ strategy registration
-  /** collect enumerator types
-   *
-   * This builds the strategy for enumerated values of type tn for the given
-   * role of nrole, for solutions to function-to-synthesize of this class.
-   */
-  void collectEnumeratorTypes(TypeNode tn, NodeRole nrole);
-  /** register enumerator
-   *
-   * This registers that et is an enumerator of type tn, having enumerator
-   * role enum_role.
-   *
-   * inSearch is whether we will enumerate values based on this enumerator.
-   * A strategy node is represented by a (enumerator, node role) pair. Hence,
-   * we may use enumerators for which this flag is false to represent strategy
-   * nodes that have child strategies.
-   */
-  void registerEnumerator(Node et,
-                          TypeNode tn,
-                          EnumRole enum_role,
-                          bool inSearch);
-  /** infer template */
-  bool inferTemplate(unsigned k,
-                     Node n,
-                     std::map<Node, unsigned>& templ_var_index,
-                     std::map<unsigned, unsigned>& templ_injection);
-  /** static learn redundant operators
-   *
-   * This learns static lemmas for pruning enumerative space based on the
-   * strategy for the function-to-synthesize of this class, and stores these
-   * into lemmas.
-   */
-  void staticLearnRedundantOps(std::vector<Node>& lemmas);
-  /** helper for static learn redundant operators
-   *
-   * (e, nrole) specify the strategy node in the graph we are currently
-   * analyzing, visited stores the nodes we have already visited.
-   *
-   * This method builds the mapping needs_cons, which maps (master) enumerators
-   * to a map from the constructors that it needs.
-   *
-   * ind is the depth in the strategy graph we are at (for debugging).
-   *
-   * isCond is whether the current enumerator is conditional (beneath a
-   * conditional of an strat_ITE strategy).
-   */
-  void staticLearnRedundantOps(
-      Node e,
-      NodeRole nrole,
-      std::map<Node, std::map<NodeRole, bool> >& visited,
-      std::map<Node, std::map<unsigned, bool> >& needs_cons,
-      int ind,
-      bool isCond);
-  //------------------------------ end strategy registration
-
+  //------------------------------ constructing solutions
   /** helper function for construct solution.
    *
    * Construct a solution based on enumerator e for function-to-synthesize of
@@ -644,41 +484,6 @@ class SygusUnif
                                    std::map<Node, std::vector<unsigned> > incr,
                                    UnifContext& x);
   //------------------------------ end constructing solutions
-
-  /** represents a strategy for a SyGuS datatype type
-   *
-   * This represents a possible strategy to apply when processing a strategy
-   * node in constructSolution. When applying the strategy represented by this
-   * class, we may make recursive calls to the children of the strategy,
-   * given in d_cenum. If all recursive calls to constructSolution for these
-   * children are successful, say:
-   *   constructSolution( d_cenum[1], ... ) = t1,
-   *    ...,
-   *   constructSolution( d_cenum[n], ... ) = tn,
-   * Then, the solution returned by this strategy is
-   *   d_sol_templ * { d_sol_templ_args -> (t1,...,tn) }
-   * where * is application of substitution.
-   */
-  class EnumTypeInfoStrat
-  {
-   public:
-    /** the type of strategy this represents */
-    StrategyType d_this;
-    /** the sygus datatype constructor that induced this strategy
-     *
-     * For example, this may be a sygus datatype whose sygus operator is ITE,
-     * if the strategy type above is strat_ITE.
-     */
-    Node d_cons;
-    /** children of this strategy */
-    std::vector<std::pair<Node, NodeRole> > d_cenum;
-    /** the arguments for the (templated) solution */
-    std::vector<Node> d_sol_templ_args;
-    /** the template for the solution */
-    Node d_sol_templ;
-    /** Returns true if argument is valid strategy in context x */
-    bool isValid(SygusUnif* pbe, UnifContext& x);
-  };
 };
 
 } /* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index c5899128d..c397dec52 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -108,6 +108,19 @@ Node SygusUnifStrategy::getRootEnumerator()
   return it->second;
 }
 
+EnumInfo& SygusUnifStrategy::getEnumInfo(Node e)
+{
+  std::map<Node, EnumInfo>::iterator it = d_einfo.find(e);
+  Assert(it != d_einfo.end());
+  return it->second;
+}
+
+EnumTypeInfo& SygusUnifStrategy::getEnumTypeInfo(TypeNode tn)
+{
+  std::map<TypeNode, EnumTypeInfo>::iterator it = d_tinfo.find(tn);
+  Assert(it != d_tinfo.end());
+  return it->second;
+}
 // ----------------------------- establishing enumeration types
 
 void SygusUnifStrategy::registerEnumerator(Node et,
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h
index 94eadbc68..9a6c7ea4a 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h
@@ -143,11 +143,6 @@ class EnumInfo
   std::vector<Node> d_enum_slave;
 
  private:
-  /**
-    * Whether an enumerated value for this conjecture has solved the entire
-    * conjecture.
-    */
-  Node d_enum_solved;
   /** the role of this enumerator (one of enum_* above). */
   EnumRole d_role;
   /** is this enumerator conditional */
@@ -250,18 +245,28 @@ class SygusUnifStrategy
                   std::vector<Node>& lemmas);
   /** Get the root enumerator for this class */
   Node getRootEnumerator();
-  /** maps enumerators to relevant information */
-  std::map<Node, EnumInfo> d_einfo;
-  /** list of all enumerators for the function-to-synthesize */
-  std::vector<Node> d_esym_list;
-  /** Info for sygus datatype type occurring in a field of d_root */
-  std::map<TypeNode, EnumTypeInfo> d_tinfo;
+  /**
+   * Get the enumerator info for enumerator e, where e must be an enumerator
+   * initialized by this class (in enums after a call to initialize).
+   */
+  EnumInfo& getEnumInfo(Node e);
+  /**
+   * Get the enumerator type info for sygus type t, where t must be the type
+   * of some enumerator initialized by this class
+   */
+  EnumTypeInfo& getEnumTypeInfo(TypeNode tn);
 
  private:
   /** reference to quantifier engine */
   QuantifiersEngine* d_qe;
   /** The candidate variable this strategy is for */
   Node d_candidate;
+  /** maps enumerators to relevant information */
+  std::map<Node, EnumInfo> d_einfo;
+  /** list of all enumerators for the function-to-synthesize */
+  std::vector<Node> d_esym_list;
+  /** Info for sygus datatype type occurring in a field of d_root */
+  std::map<TypeNode, EnumTypeInfo> d_tinfo;
   /**
     * The root sygus datatype for the function-to-synthesize,
     * which encodes the overall syntactic restrictions on the space