Make sygus pbe use sygus unif utility (#1724)

4 files changed, 317 insertions, 2903 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 347efac26..65b8ba133 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -149,20 +149,35 @@ bool CegConjecturePbe::initialize(Node n,
     if( candidates.size()==1 ){// conditional solutions for multiple function conjectures TODO?
       // collect a pool of types over which we will enumerate terms 
       Node c = candidates[0];
-      //the candidate must be input/output examples
-      if( d_examples_out_invalid.find( c )==d_examples_out_invalid.end() ){
+      // specification must have at least one example, and must be in PBE form
+      if (!d_examples[c].empty()
+          && d_examples_out_invalid.find(c) == d_examples_out_invalid.end())
+      {
         Assert( d_examples.find( c )!=d_examples.end() );
-        Trace("sygus-unif") << "It is input/output examples..." << std::endl;
-        TypeNode ctn = c.getType();
-        d_cinfo[c].initialize( c );
-        // collect the enumerator types / form the strategy
-        collectEnumeratorTypes(c, ctn, role_equal);
-        // if we have non-trivial strategies, then use pbe
-        if( d_cinfo[c].isNonTrivial() ){
-          // static learning of redundant constructors
-          staticLearnRedundantOps( c, lemmas );
-          d_is_pbe = true;
+        Trace("sygus-pbe") << "Initialize unif utility for " << c << "..."
+                           << std::endl;
+        d_sygus_unif[c].initialize(d_qe, c, d_candidate_to_enum[c], lemmas);
+        Assert(!d_candidate_to_enum[c].empty());
+        Trace("sygus-pbe") << "Initialize " << d_candidate_to_enum[c].size()
+                           << " enumerators for " << c << "..." << std::endl;
+        // initialize the enumerators
+        for (unsigned i = 0, size = d_candidate_to_enum[c].size(); i < size;
+             i++)
+        {
+          Node e = d_candidate_to_enum[c][i];
+          d_tds->registerEnumerator(e, c, d_parent, true);
+          Node g = d_tds->getActiveGuardForEnumerator(e);
+          d_enum_to_active_guard[e] = g;
+          d_enum_to_candidate[e] = c;
         }
+        Trace("sygus-pbe") << "Initialize " << d_examples[c].size()
+                           << " example points for " << c << "..." << std::endl;
+        // initialize the examples
+        for (unsigned i = 0, nex = d_examples[c].size(); i < nex; i++)
+        {
+          d_sygus_unif[c].addExample(d_examples[c][i], d_examples_out[c][i]);
+        }
+        d_is_pbe = true;
       }
     }
   }
@@ -292,715 +307,6 @@ Node CegConjecturePbe::evaluateBuiltin(TypeNode tn, Node bn, Node e,
   return Rewriter::rewrite(bn);
 }
 
-// ----------------------------- establishing enumeration types
-
-void CegConjecturePbe::registerEnumerator(
-    Node et, Node c, TypeNode tn, EnumRole enum_role, bool inSearch)
-{
-  if (d_einfo.find(et) == d_einfo.end())
-  {
-    Trace("sygus-unif-debug")
-        << "...register " << et << " for "
-        << ((DatatypeType)tn.toType()).getDatatype().getName();
-    Trace("sygus-unif-debug") << ", role = " << enum_role
-                              << ", in search = " << inSearch << std::endl;
-    d_einfo[et].initialize(c, 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[c].d_search_enum.find(tn);
-      if (itn == d_cinfo[c].d_search_enum.end())
-      {
-        // use this for the search
-        d_cinfo[c].d_search_enum[tn] = et;
-        d_cinfo[c].d_esym_list.push_back(et);
-        d_einfo[et].d_enum_slave.push_back(et);
-        // register measured term with database
-        d_qe->getTermDatabaseSygus()->registerEnumerator(et, c, d_parent, true);
-        d_einfo[et].d_active_guard =
-            d_qe->getTermDatabaseSygus()->getActiveGuardForEnumerator(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 CegConjecturePbe::collectEnumeratorTypes(Node e,
-                                              TypeNode tn,
-                                              NodeRole nrole)
-{
-  NodeManager* nm = NodeManager::currentNM();
-  if (d_cinfo[e].d_tinfo.find(tn) == d_cinfo[e].d_tinfo.end())
-  {
-    // register type
-    Trace("sygus-unif") << "Register enumerating type : " << tn << std::endl;
-    d_cinfo[e].initializeType( tn );
-  }
-  EnumTypeInfo& eti = d_cinfo[e].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 "
-        << ((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, e, 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, e, 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 "
-                << ((DatatypeType)tn.toType()).getDatatype().getName()
-                << std::endl;
-            registerEnumerator(et, e, 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(e, ct, nrole_c);
-            // otherwise use the previous
-            Assert(d_cinfo[e].d_tinfo[ct].d_enum.find(erole_c)
-                   != d_cinfo[e].d_tinfo[ct].d_enum.end());
-            et = d_cinfo[e].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 " << ((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 CegConjecturePbe::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 CegConjecturePbe::staticLearnRedundantOps( Node c, std::vector< Node >& lemmas ) {
-  for( unsigned i=0; i<d_cinfo[c].d_esym_list.size(); i++ ){
-    Node e = d_cinfo[c].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 " << c << " is : " << std::endl;
-  std::map<Node, std::map<NodeRole, bool> > visited;
-  std::map<Node, std::map<unsigned, bool> > needs_cons;
-  staticLearnRedundantOps(c,
-                          d_cinfo[c].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 CegConjecturePbe::staticLearnRedundantOps(
-    Node c,
-    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();
-    }
-    SygusUnif::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[c].d_tinfo.find( etn );
-      Assert( itt!=d_cinfo[c].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;
-        SygusUnif::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(c,
-                                  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[c].d_search_enum.find(etn);
-      if (itse == d_cinfo[c].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{
-    SygusUnif::indent("sygus-unif", ind);
-    Trace("sygus-unif") << e << " :: node role : " << nrole << std::endl;
-  }
-}
-
 // ------------------------------------------- solution construction from enumeration
 
 void CegConjecturePbe::getTermList(const std::vector<Node>& candidates,
@@ -1009,13 +315,19 @@ void CegConjecturePbe::getTermList(const std::vector<Node>& candidates,
   Valuation& valuation = d_qe->getValuation();
   for( unsigned i=0; i<candidates.size(); i++ ){
     Node v = candidates[i];
-    std::map< Node, CandidateInfo >::iterator it = d_cinfo.find( v );
-    if( it!=d_cinfo.end() ){
-      for( unsigned j=0; j<it->second.d_esym_list.size(); j++ ){
-        Node e = it->second.d_esym_list[j];
-        std::map< Node, EnumInfo >::iterator it = d_einfo.find( e );
-        Assert( it != d_einfo.end() );
-        Node gstatus = valuation.getSatValue(it->second.d_active_guard);
+    std::map<Node, std::vector<Node> >::iterator it =
+        d_candidate_to_enum.find(v);
+    if (it != d_candidate_to_enum.end())
+    {
+      for (unsigned j = 0; j < it->second.size(); j++)
+      {
+        Node e = it->second[j];
+        Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end());
+        Node g = d_enum_to_active_guard[e];
+        // Get whether the active guard for this enumerator is true,
+        // if so, then there may exist more values for it, and hence we add it
+        // to terms.
+        Node gstatus = valuation.getSatValue(g);
         if (!gstatus.isNull() && gstatus.getConst<bool>())
         {
           terms.push_back(e);
@@ -1049,15 +361,30 @@ bool CegConjecturePbe::constructCandidates(const std::vector<Node>& enums,
     }
     // only consider the enumerators that are at minimum size (for fairness)
     Trace("sygus-pbe-enum") << "...register " << enum_consider.size() << " / " << enums.size() << std::endl;
-    for( unsigned i=0; i<enum_consider.size(); i++ ){
+    NodeManager* nm = NodeManager::currentNM();
+    for (unsigned i = 0, ecsize = enum_consider.size(); i < ecsize; i++)
+    {
       unsigned j = enum_consider[i];
-      addEnumeratedValue( enums[j], enum_values[j], lems );
+      Node e = enums[j];
+      Node v = enum_values[j];
+      Assert(d_enum_to_candidate.find(e) != d_enum_to_candidate.end());
+      Node c = d_enum_to_candidate[e];
+      std::vector<Node> enum_lems;
+      d_sygus_unif[c].notifyEnumeration(e, v, enum_lems);
+      // the lemmas must be guarded by the active guard of the enumerator
+      Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end());
+      Node g = d_enum_to_active_guard[e];
+      for (unsigned j = 0, size = enum_lems.size(); j < size; j++)
+      {
+        enum_lems[j] = nm->mkNode(OR, g.negate(), enum_lems[j]);
+      }
+      lems.insert(lems.end(), enum_lems.begin(), enum_lems.end());
     }
   }
   for( unsigned i=0; i<candidates.size(); i++ ){
     Node c = candidates[i];
     //build decision tree for candidate
-    Node vc = constructSolution( c );
+    Node vc = d_sygus_unif[c].constructSolution();
     if( vc.isNull() ){     
       return false;
     }else{
@@ -1067,1356 +394,6 @@ bool CegConjecturePbe::constructCandidates(const std::vector<Node>& enums,
   return true;
 }
 
-void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& lems ) {
-  std::map< Node, EnumInfo >::iterator it = d_einfo.find( x );
-  Assert( it != d_einfo.end() );
-  Node gstatus = d_qe->getValuation().getSatValue(it->second.d_active_guard);
-  if (gstatus.isNull() || !gstatus.getConst<bool>())
-  {
-    Trace("sygus-pbe-enum-debug") << "  ...guard is inactive." << std::endl;
-    return;
-  }
-  Assert(
-      std::find(it->second.d_enum_vals.begin(), it->second.d_enum_vals.end(), v)
-      == it->second.d_enum_vals.end());
-  Node c = it->second.d_parent_candidate;
-  // The explanation for why the current value should be excluded in future
-  // iterations.
-  Node exp_exc;
-  if (d_examples_out_invalid.find(c) == d_examples_out_invalid.end())
-  {
-    std::map<Node, CandidateInfo>::iterator itc = d_cinfo.find(c);
-    Assert(itc != d_cinfo.end());
-    TypeNode xtn = x.getType();
-    Node bv = d_tds->sygusToBuiltin(v, xtn);
-    std::map<Node, std::vector<std::vector<Node> > >::iterator itx =
-        d_examples.find(c);
-    std::map<Node, std::vector<Node> >::iterator itxo = d_examples_out.find(c);
-    Assert(itx != d_examples.end());
-    Assert(itxo != d_examples_out.end());
-    Assert(itx->second.size() == itxo->second.size());
-    std::vector<Node> base_results;
-    // compte the results
-    for (unsigned j = 0, size = itx->second.size(); j < size; j++)
-    {
-      Node res = d_tds->evaluateBuiltin(xtn, bv, itx->second[j]);
-      Trace("sygus-pbe-enum-debug")
-          << "...got res = " << res << " from " << bv << std::endl;
-      base_results.push_back(res);
-    }
-    // is it excluded for domain-specific reason?
-    std::vector<Node> exp_exc_vec;
-    if (getExplanationForEnumeratorExclude(
-            c, x, v, base_results, it->second, exp_exc_vec))
-    {
-      Assert(!exp_exc_vec.empty());
-      exp_exc = exp_exc_vec.size() == 1
-                    ? exp_exc_vec[0]
-                    : NodeManager::currentNM()->mkNode(AND, exp_exc_vec);
-      Trace("sygus-pbe-enum")
-          << "  ...fail : term is excluded (domain-specific)" << std::endl;
-    }
-    else
-    {
-      // notify all slaves
-      Assert( !it->second.d_enum_slave.empty() );
-      //explanation for why this value should be excluded
-      for( unsigned s=0; s<it->second.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() );
-        Trace("sygus-pbe-enum") << "Process " << xs << " from " << s << std::endl;
-        //bool prevIsCover = false;
-        if (itv->second.getRole() == enum_io)
-        {
-          Trace("sygus-pbe-enum") << "   IO-Eval of ";
-          //prevIsCover = itv->second.isFeasible();
-        }else{
-          Trace("sygus-pbe-enum") << "Evaluation of ";
-        }
-        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;
-        std::map< Node, bool > cond_vals;
-        for (unsigned j = 0, size = base_results.size(); j < size; j++)
-        {
-          Node res = base_results[j];
-          Assert( res.isConst() );
-          if( !templ.isNull() ){
-            TNode tres = res;
-            res = templ.substitute( templ_var, res );
-            res = Rewriter::rewrite( res );
-            Assert( res.isConst() );
-          }
-          Node resb;
-          if (itv->second.getRole() == enum_io)
-          {
-            Node out = itxo->second[j];
-            Assert( out.isConst() );
-            resb = res==out ? d_true : d_false;
-          }else{
-            resb = res;
-          }
-          cond_vals[resb] = true;
-          results.push_back( resb );
-          if( Trace.isOn("sygus-pbe-enum") ){
-            if( resb.getType().isBoolean() ){
-              Trace("sygus-pbe-enum") << ( resb==d_true ? "1" : "0" );
-            }else{
-              Trace("sygus-pbe-enum") << "?";
-            }
-          }
-        }
-        bool keep = false;
-        if (itv->second.getRole() == enum_io)
-        {
-          // latter is the degenerate case of no examples
-          if (cond_vals.find(d_true) != cond_vals.end() || cond_vals.empty())
-          {
-            //check subsumbed/subsuming
-            std::vector< Node > subsume;
-            if( cond_vals.find( d_false )==cond_vals.end() ){
-              // it is the entire solution, we are done
-              Trace("sygus-pbe-enum") << "  ...success, full solution added to PBE pool : " << d_tds->sygusToBuiltin( v ) << std::endl;
-              if( !itv->second.isSolved() ){
-                itv->second.setSolved( v );
-                // it subsumes everything
-                itv->second.d_term_trie.clear();
-                itv->second.d_term_trie.addTerm(v, results, true, subsume);
-              }
-              keep = true;
-            }else{
-              Node val =
-                  itv->second.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() );
-                  Trace("sygus-pbe-enum") << " and subsumed " << subsume.size() << " terms";
-                }
-                Trace("sygus-pbe-enum") << "!   add to PBE pool : " << d_tds->sygusToBuiltin( v ) << std::endl;
-                keep = true;
-              }else{
-                Assert( subsume.empty() );
-                Trace("sygus-pbe-enum") << "  ...fail : subsumed" << std::endl;
-              }
-            }
-          }else{
-            Trace("sygus-pbe-enum") << "  ...fail : it does not satisfy examples." << std::endl;
-          }
-        }else{
-          // must be unique up to examples
-          Node val = itv->second.d_term_trie.addCond(v, results, true);
-          if (val == v)
-          {
-            Trace("sygus-pbe-enum") << "  ...success!   add to PBE pool : "
-                                    << d_tds->sygusToBuiltin(v) << std::endl;
-            keep = true;
-          }else{
-            Trace("sygus-pbe-enum")
-                << "  ...fail : term is not unique" << std::endl;
-          }
-          itc->second.d_cond_count++;
-        }
-        if( keep ){
-          // notify the parent to retry the build of PBE
-          itc->second.d_check_sol = true;
-          itv->second.addEnumValue( this, v, results );
-        }
-      }
-    }
-  }else{
-    Trace("sygus-pbe-enum-debug")
-        << "  ...examples do not have output." << std::endl;
-  }
-  // exclude this value on subsequent iterations
-  Node g = it->second.d_active_guard;
-  if (exp_exc.isNull())
-  {
-    // if we did not already explain why this should be excluded, use default
-    exp_exc = d_tds->getExplain()->getExplanationForEquality(x, v);
-  }
-  Node exlem =
-      NodeManager::currentNM()->mkNode(OR, g.negate(), exp_exc.negate());
-  Trace("sygus-pbe-enum-lemma")
-      << "CegConjecturePbe : enumeration exclude lemma : " << exlem
-      << std::endl;
-  lems.push_back(exlem);
-}
-
-bool CegConjecturePbe::useStrContainsEnumeratorExclude(Node x, EnumInfo& ei)
-{
-  TypeNode xbt = d_tds->sygusToBuiltinType(x.getType());
-  if (xbt.isString())
-  {
-    std::map<Node, bool>::iterator itx = d_use_str_contains_eexc.find(x);
-    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;
-    for (const Node& sn : ei.d_enum_slave)
-    {
-      std::map<Node, EnumInfo>::iterator itv = d_einfo.find(sn);
-      EnumRole er = itv->second.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;
-        return false;
-      }
-      if (itv->second.isConditional())
-      {
-        Trace("sygus-pbe-enum-debug")
-            << "  conditional slave : " << sn << std::endl;
-        d_use_str_contains_eexc[x] = false;
-        return false;
-      }
-    }
-    Trace("sygus-pbe-enum-debug")
-        << "...can use str.contains exclusion." << std::endl;
-    return d_use_str_contains_eexc[x];
-  }
-  return false;
-}
-
-bool CegConjecturePbe::getExplanationForEnumeratorExclude(
-    Node c,
-    Node x,
-    Node v,
-    std::vector<Node>& results,
-    EnumInfo& ei,
-    std::vector<Node>& exp)
-{
-  if (useStrContainsEnumeratorExclude(x, ei))
-  {
-    NodeManager* nm = NodeManager::currentNM();
-    // This check whether the example evaluates to something that is larger than
-    // the output for some input/output pair. If so, then this term is never
-    // useful. We generalize its explanation below.
-
-    if (Trace.isOn("sygus-pbe-cterm-debug"))
-    {
-      Trace("sygus-pbe-enum") << std::endl;
-    }
-    // check if all examples had longer length that the output
-    std::map<Node, std::vector<Node> >::iterator itxo = d_examples_out.find(c);
-    Assert(itxo != d_examples_out.end());
-    Assert(itxo->second.size() == results.size());
-    Trace("sygus-pbe-cterm-debug")
-        << "Check enumerator exclusion for " << x << " -> "
-        << 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++)
-    {
-      Assert(results[i].isConst());
-      Assert(itxo->second[i].isConst());
-      Trace("sygus-pbe-cterm-debug")
-          << "  " << results[i] << " <> " << itxo->second[i];
-      Node cont = nm->mkNode(STRING_STRCTN, itxo->second[i], results[i]);
-      Node contr = Rewriter::rewrite(cont);
-      if (contr == d_false)
-      {
-        cmp_indices.push_back(i);
-        Trace("sygus-pbe-cterm-debug") << "...not contained." << std::endl;
-      }
-      else
-      {
-        Trace("sygus-pbe-cterm-debug") << "...contained." << std::endl;
-      }
-    }
-    if (!cmp_indices.empty())
-    {
-      // we check invariance with respect to a negative contains test
-      NegContainsSygusInvarianceTest ncset;
-      ncset.init(x, d_examples[c], itxo->second, cmp_indices);
-      // construct the generalized explanation
-      d_tds->getExplain()->getExplanationFor(x, v, exp, ncset);
-      Trace("sygus-pbe-cterm")
-          << "PBE-cterm : enumerator exclude " << d_tds->sygusToBuiltin(v)
-          << " due to negative containment." << std::endl;
-      return true;
-    }
-  }
-  return false;
-}
-
-
-
-void CegConjecturePbe::EnumInfo::addEnumValue( CegConjecturePbe * pbe, Node v, std::vector< Node >& results ) {
-  d_enum_val_to_index[v] = d_enum_vals.size();
-  d_enum_vals.push_back( v );
-  d_enum_vals_res.push_back( results );
-  /*
-  if( getRole()==enum_io ){
-    // compute
-    if( d_enum_total.empty() ){
-      d_enum_total = results;
-    }else if( !d_enum_total_true ){
-      d_enum_total_true = true;
-      Assert( d_enum_total.size()==results.size() );
-      for( unsigned i=0; i<results.size(); i++ ){
-        if( d_enum_total[i]==pbe->d_true || results[i]==pbe->d_true ){
-          d_enum_total[i] = pbe->d_true;
-        }else{
-          d_enum_total[i] = pbe->d_false;
-          d_enum_total_true = false;
-        }
-      }
-    }
-  }
-  */
-}
-
-void CegConjecturePbe::EnumInfo::initialize(Node c, EnumRole role)
-{
-  d_parent_candidate = c;
-  d_role = role;
-}
-
-void CegConjecturePbe::EnumInfo::setSolved( Node slv ) {
-  d_enum_solved = slv;
-  //d_enum_total_true = true;
-}
-    
-void CegConjecturePbe::CandidateInfo::initialize( Node c ) {
-  d_this_candidate = c;
-  d_root = c.getType();
-}
-
-void CegConjecturePbe::CandidateInfo::initializeType( TypeNode tn ) {
-  d_tinfo[tn].d_this_type = tn;
-  d_tinfo[tn].d_parent = this;
-}
-
-Node CegConjecturePbe::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;
-}
-
-bool CegConjecturePbe::CandidateInfo::isNonTrivial() {
-  //TODO
-  return true;
-}
-
-// status : 0 : exact, -1 : vals is subset, 1 : vals is superset
-Node CegConjecturePbe::SubsumeTrie::addTermInternal(
-    Node t,
-    const std::vector<Node>& vals,
-    bool pol,
-    std::vector<Node>& subsumed,
-    bool spol,
-    unsigned index,
-    int status,
-    bool checkExistsOnly,
-    bool checkSubsume)
-{
-  if (index == vals.size())
-  {
-    if (status == 0)
-    {
-      // set the term if checkExistsOnly = false
-      if (d_term.isNull() && !checkExistsOnly)
-      {
-        d_term = t;
-      }
-    }
-    else if (status == 1)
-    {
-      Assert(checkSubsume);
-      // found a subsumed term
-      if (!d_term.isNull())
-      {
-        subsumed.push_back(d_term);
-        if (!checkExistsOnly)
-        {
-          // remove it if checkExistsOnly = false
-          d_term = Node::null();
-        }
-      }
-    }
-    else
-    {
-      Assert(!checkExistsOnly && checkSubsume);
-    }
-    return d_term;
-  }
-  NodeManager* nm = NodeManager::currentNM();
-  // the current value
-  Assert(pol || (vals[index].isConst() && vals[index].getType().isBoolean()));
-  Node cv = pol ? vals[index] : nm->mkConst(!vals[index].getConst<bool>());
-  // if checkExistsOnly = false, check if the current value is subsumed if
-  // checkSubsume = true, if so, don't add
-  if (!checkExistsOnly && checkSubsume)
-  {
-    Assert(cv.isConst() && cv.getType().isBoolean());
-    std::vector<bool> check_subsumed_by;
-    if (status == 0)
-    {
-      if (!cv.getConst<bool>())
-      {
-        check_subsumed_by.push_back(spol);
-      }
-    }
-    else if (status == -1)
-    {
-      check_subsumed_by.push_back(spol);
-      if (!cv.getConst<bool>())
-      {
-        check_subsumed_by.push_back(!spol);
-      }
-    }
-    // check for subsumed nodes
-    for (unsigned i = 0, size = check_subsumed_by.size(); i < size; i++)
-    {
-      bool csbi = check_subsumed_by[i];
-      Node csval = nm->mkConst(csbi);
-      // check if subsumed
-      std::map<Node, SubsumeTrie>::iterator itc = d_children.find(csval);
-      if (itc != d_children.end())
-      {
-        Node ret = itc->second.addTermInternal(t,
-                                               vals,
-                                               pol,
-                                               subsumed,
-                                               spol,
-                                               index + 1,
-                                               -1,
-                                               checkExistsOnly,
-                                               checkSubsume);
-        // ret subsumes t
-        if (!ret.isNull())
-        {
-          return ret;
-        }
-      }
-    }
-  }
-  Node ret;
-  std::vector<bool> check_subsume;
-  if (status == 0)
-  {
-    if (checkExistsOnly)
-    {
-      std::map<Node, SubsumeTrie>::iterator itc = d_children.find(cv);
-      if (itc != d_children.end())
-      {
-        ret = itc->second.addTermInternal(t,
-                                          vals,
-                                          pol,
-                                          subsumed,
-                                          spol,
-                                          index + 1,
-                                          0,
-                                          checkExistsOnly,
-                                          checkSubsume);
-      }
-    }
-    else
-    {
-      Assert(spol);
-      ret = d_children[cv].addTermInternal(t,
-                                           vals,
-                                           pol,
-                                           subsumed,
-                                           spol,
-                                           index + 1,
-                                           0,
-                                           checkExistsOnly,
-                                           checkSubsume);
-      if (ret != t)
-      {
-        // we were subsumed by ret, return
-        return ret;
-      }
-    }
-    if (checkSubsume)
-    {
-      Assert(cv.isConst() && cv.getType().isBoolean());
-      // check for subsuming
-      if (cv.getConst<bool>())
-      {
-        check_subsume.push_back(!spol);
-      }
-    }
-  }
-  else if (status == 1)
-  {
-    Assert(checkSubsume);
-    Assert(cv.isConst() && cv.getType().isBoolean());
-    check_subsume.push_back(!spol);
-    if (cv.getConst<bool>())
-    {
-      check_subsume.push_back(spol);
-    }
-  }
-  if (checkSubsume)
-  {
-    // check for subsumed terms
-    for (unsigned i = 0, size = check_subsume.size(); i < size; i++)
-    {
-      Node csval = nm->mkConst<bool>(check_subsume[i]);
-      std::map<Node, SubsumeTrie>::iterator itc = d_children.find(csval);
-      if (itc != d_children.end())
-      {
-        itc->second.addTermInternal(t,
-                                    vals,
-                                    pol,
-                                    subsumed,
-                                    spol,
-                                    index + 1,
-                                    1,
-                                    checkExistsOnly,
-                                    checkSubsume);
-        // clean up
-        if (itc->second.isEmpty())
-        {
-          Assert(!checkExistsOnly);
-          d_children.erase(csval);
-        }
-      }
-    }
-  }
-  return ret;
-}
-
-Node CegConjecturePbe::SubsumeTrie::addTerm(Node t,
-                                            const std::vector<Node>& vals,
-                                            bool pol,
-                                            std::vector<Node>& subsumed)
-{
-  return addTermInternal(t, vals, pol, subsumed, true, 0, 0, false, true);
-}
-
-Node CegConjecturePbe::SubsumeTrie::addCond(Node c,
-                                            const std::vector<Node>& vals,
-                                            bool pol)
-{
-  std::vector<Node> subsumed;
-  return addTermInternal(c, vals, pol, subsumed, true, 0, 0, false, false);
-}
-
-void CegConjecturePbe::SubsumeTrie::getSubsumed(const std::vector<Node>& vals,
-                                                bool pol,
-                                                std::vector<Node>& subsumed)
-{
-  addTermInternal(Node::null(), vals, pol, subsumed, true, 0, 1, true, true);
-}
-
-void CegConjecturePbe::SubsumeTrie::getSubsumedBy(
-    const std::vector<Node>& vals, bool pol, std::vector<Node>& subsumed_by)
-{
-  // flip polarities
-  addTermInternal(
-      Node::null(), vals, !pol, subsumed_by, false, 0, 1, true, true);
-}
-
-void CegConjecturePbe::SubsumeTrie::getLeavesInternal(
-    const std::vector<Node>& vals,
-    bool pol,
-    std::map<int, std::vector<Node> >& v,
-    unsigned index,
-    int status)
-{
-  if (index == vals.size())
-  {
-    Assert(!d_term.isNull());
-    Assert(std::find(v[status].begin(), v[status].end(), d_term)
-           == v[status].end());
-    v[status].push_back(d_term);
-  }
-  else
-  {
-    Assert(vals[index].isConst() && vals[index].getType().isBoolean());
-    bool curr_val_true = vals[index].getConst<bool>() == pol;
-    for (std::map<Node, SubsumeTrie>::iterator it = d_children.begin();
-         it != d_children.end();
-         ++it)
-    {
-      int new_status = status;
-      // if the current value is true
-      if (curr_val_true)
-      {
-        if (status != 0)
-        {
-          Assert(it->first.isConst() && it->first.getType().isBoolean());
-          new_status = (it->first.getConst<bool>() ? 1 : -1);
-          if (status != -2 && new_status != status)
-          {
-            new_status = 0;
-          }
-        }
-      }
-      it->second.getLeavesInternal(vals, pol, v, index + 1, new_status);
-    }
-  }
-}
-
-void CegConjecturePbe::SubsumeTrie::getLeaves(
-    const std::vector<Node>& vals,
-    bool pol,
-    std::map<int, std::vector<Node> >& v)
-{
-  getLeavesInternal(vals, pol, v, 0, -2);
-}
-
-Node CegConjecturePbe::constructSolution( Node c ){
-  std::map< Node, CandidateInfo >::iterator itc = d_cinfo.find( c );
-  Assert( itc!=d_cinfo.end() );
-  if( !itc->second.d_solution.isNull() ){
-    // already has a solution
-    return itc->second.d_solution;
-  }else{
-    // only check if an enumerator updated
-    if( itc->second.d_check_sol ){
-      Trace("sygus-pbe") << "Construct solution, #iterations = " << itc->second.d_cond_count << std::endl;
-      itc->second.d_check_sol = false;
-      // try multiple times if we have done multiple conditions, due to non-determinism
-      Node vc;
-      for( unsigned i=0; i<=itc->second.d_cond_count; i++ ){
-        Trace("sygus-pbe-dt") << "ConstructPBE for candidate: " << c << std::endl;
-        Node e = itc->second.getRootEnumerator();
-        UnifContext x;
-        x.initialize( this, c );
-        Node vcc = constructSolution(c, e, role_equal, x, 1);
-        if( !vcc.isNull() ){
-          if( vc.isNull() || ( !vc.isNull() && d_tds->getSygusTermSize( vcc )<d_tds->getSygusTermSize( vc ) ) ){
-            Trace("sygus-pbe") << "**** PBE SOLVED : " << c << " = " << vcc << std::endl;
-            Trace("sygus-pbe") << "...solved at iteration " << i << std::endl;
-            vc = vcc;
-          }
-        }
-      }
-      if( !vc.isNull() ){
-        itc->second.d_solution = vc;
-        return vc;
-      }
-      Trace("sygus-pbe") << "...failed to solve." << std::endl;
-    }
-    return Node::null();
-  }
-}
-
-Node CegConjecturePbe::constructBestSolvedTerm( std::vector< Node >& solved, UnifContext& x ){
-  Assert( !solved.empty() );
-  // TODO
-  return solved[0];
-}
-
-Node CegConjecturePbe::constructBestStringSolvedTerm( std::vector< Node >& solved, UnifContext& x ) {
-  Assert( !solved.empty() );
-  // TODO
-  return solved[0];
-}
-
-Node CegConjecturePbe::constructBestSolvedConditional( std::vector< Node >& solved, UnifContext& x ){
-  Assert( !solved.empty() );
-  // TODO
-  return solved[0];
-}
-
-Node CegConjecturePbe::constructBestConditional( std::vector< Node >& conds, UnifContext& x ) {
-  Assert( !conds.empty() );
-  // TODO
-  double r = Random::getRandom().pickDouble(0.0, 1.0);
-  unsigned cindex = r*conds.size();
-  if( cindex>conds.size() ){
-    cindex = conds.size() - 1;
-  }
-  return conds[cindex];
-}
-
-Node CegConjecturePbe::constructBestStringToConcat( std::vector< Node > strs,
-                                                    std::map< Node, unsigned > total_inc, 
-                                                    std::map< Node, std::vector< unsigned > > incr,
-                                                    UnifContext& x ) {
-  Assert( !strs.empty() );
-  std::random_shuffle(strs.begin(), strs.end());
-  // prefer one that has incremented by more than 0
-  for (const Node& ns : strs)
-  {
-    if (total_inc[ns] > 0)
-    {
-      return ns;
-    }
-  }
-  return strs[0];
-}
-
-Node CegConjecturePbe::constructSolution(
-    Node c, Node e, NodeRole nrole, UnifContext& x, int ind)
-{
-  TypeNode etn = e.getType();
-  if (Trace.isOn("sygus-pbe-dt-debug"))
-  {
-    SygusUnif::indent("sygus-pbe-dt-debug", ind);
-    Trace("sygus-pbe-dt-debug") << "ConstructPBE: (" << e << ", " << nrole
-                                << ") for type " << etn << " in context ";
-    SygusUnif::print_val("sygus-pbe-dt-debug", x.d_vals);
-    if (x.d_has_string_pos != role_invalid)
-    {
-      Trace("sygus-pbe-dt-debug") << ", string context [" << x.d_has_string_pos;
-      for (unsigned i = 0, size = x.d_str_pos.size(); i < size; i++)
-      {
-        Trace("sygus-pbe-dt-debug") << " " << x.d_str_pos[i];
-      }
-      Trace("sygus-pbe-dt-debug") << "]";
-    }
-    Trace("sygus-pbe-dt-debug") << std::endl;
-  }
-  // enumerator type info
-  std::map<TypeNode, EnumTypeInfo>::iterator itt = d_cinfo[c].d_tinfo.find(etn);
-  Assert(itt != d_cinfo[c].d_tinfo.end());
-  EnumTypeInfo& tinfo = itt->second;
-
-  // get the enumerator information
-  std::map< Node, EnumInfo >::iterator itn = d_einfo.find( e );
-  Assert( itn!=d_einfo.end() );
-  EnumInfo& einfo = itn->second;
-
-  Node ret_dt;
-  if (nrole == role_equal)
-  {
-    if (!x.isReturnValueModified())
-    {
-      if (einfo.isSolved())
-      {
-        // this type has a complete solution
-        ret_dt = einfo.getSolved();
-        SygusUnif::indent("sygus-pbe-dt", ind);
-        Trace("sygus-pbe-dt") << "return PBE: success : solved "
-                              << d_tds->sygusToBuiltin(ret_dt) << std::endl;
-        Assert(!ret_dt.isNull());
-      }
-      else
-      {
-        // could be conditionally solved
-        std::vector<Node> subsumed_by;
-        einfo.d_term_trie.getSubsumedBy(x.d_vals, true, subsumed_by);
-        if (!subsumed_by.empty())
-        {
-          ret_dt = constructBestSolvedTerm(subsumed_by, x);
-          SygusUnif::indent("sygus-pbe-dt", ind);
-          Trace("sygus-pbe-dt") << "return PBE: success : conditionally solved"
-                                << d_tds->sygusToBuiltin(ret_dt) << std::endl;
-        }
-        else
-        {
-          SygusUnif::indent("sygus-pbe-dt-debug", ind);
-          Trace("sygus-pbe-dt-debug")
-              << "  ...not currently conditionally solved." << std::endl;
-        }
-      }
-    }
-    if (ret_dt.isNull())
-    {
-      if (d_tds->sygusToBuiltinType(e.getType()).isString())
-      {
-        // 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() ){
-          Node et = itnt->second;
-          itet = d_einfo.find( et );
-          Assert(itet != d_einfo.end());
-        }else{
-          success = false;
-        }
-        if (success)
-        {
-          // get the current examples
-          std::map<Node, std::vector<Node> >::iterator itx =
-              d_examples_out.find(c);
-          Assert(itx != d_examples_out.end());
-          std::vector<String> ex_vals;
-          x.getCurrentStrings(this, itx->second, ex_vals);
-          Assert(itn->second.d_enum_vals.size()
-                 == itn->second.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++)
-          {
-            if (x.isStringSolved(
-                    this, ex_vals, itet->second.d_enum_vals_res[i]))
-            {
-              str_solved.push_back(itet->second.d_enum_vals[i]);
-            }
-          }
-          if (!str_solved.empty())
-          {
-            ret_dt = constructBestStringSolvedTerm(str_solved, x);
-            SygusUnif::indent("sygus-pbe-dt", ind);
-            Trace("sygus-pbe-dt") << "return PBE: success : string solved "
-                                  << d_tds->sygusToBuiltin(ret_dt) << std::endl;
-          }
-          else
-          {
-            SygusUnif::indent("sygus-pbe-dt-debug", ind);
-            Trace("sygus-pbe-dt-debug") << "  ...not currently string solved."
-                                        << std::endl;
-          }
-        }
-      }
-    }
-  }
-  else if (nrole == role_string_prefix || nrole == role_string_suffix)
-  {
-    // check if each return value is a prefix/suffix of all open examples
-    if (!x.isReturnValueModified() || x.d_has_string_pos == nrole)
-    {
-      std::map<Node, std::vector<unsigned> > incr;
-      bool isPrefix = nrole == role_string_prefix;
-      std::map<Node, unsigned> total_inc;
-      std::vector<Node> inc_strs;
-      std::map<Node, std::vector<Node> >::iterator itx = d_examples_out.find(c);
-      Assert(itx != d_examples_out.end());
-      // make the value of the examples
-      std::vector<String> ex_vals;
-      x.getCurrentStrings(this, itx->second, ex_vals);
-      if (Trace.isOn("sygus-pbe-dt-debug"))
-      {
-        SygusUnif::indent("sygus-pbe-dt-debug", ind);
-        Trace("sygus-pbe-dt-debug") << "current strings : " << std::endl;
-        for (unsigned i = 0, size = ex_vals.size(); i < size; i++)
-        {
-          SygusUnif::indent("sygus-pbe-dt-debug", ind + 1);
-          Trace("sygus-pbe-dt-debug") << ex_vals[i] << std::endl;
-        }
-      }
-
-      // 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());
-
-      for (unsigned i = 0, size = einfo.d_enum_vals.size(); i < size; i++)
-      {
-        Node val_t = einfo.d_enum_vals[i];
-        SygusUnif::indent("sygus-pbe-dt-debug", ind);
-        Trace("sygus-pbe-dt-debug") << "increment string values : " << val_t
-                                    << " : ";
-        Assert(einfo.d_enum_vals_res[i].size() == itx->second.size());
-        unsigned tot = 0;
-        bool exsuccess = x.getStringIncrement(this,
-                                              isPrefix,
-                                              ex_vals,
-                                              einfo.d_enum_vals_res[i],
-                                              incr[val_t],
-                                              tot);
-        if (!exsuccess)
-        {
-          incr.erase(val_t);
-          Trace("sygus-pbe-dt-debug") << "...fail" << std::endl;
-        }
-        else
-        {
-          total_inc[val_t] = tot;
-          inc_strs.push_back(val_t);
-          Trace("sygus-pbe-dt-debug") << "...success, total increment = " << tot
-                                      << std::endl;
-        }
-      }
-
-      if (!incr.empty())
-      {
-        ret_dt = constructBestStringToConcat(inc_strs, total_inc, incr, x);
-        Assert(!ret_dt.isNull());
-        SygusUnif::indent("sygus-pbe-dt", ind);
-        Trace("sygus-pbe-dt") << "PBE: CONCAT strategy : choose "
-                              << (isPrefix ? "pre" : "suf") << "fix value "
-                              << d_tds->sygusToBuiltin(ret_dt) << std::endl;
-        // update the context
-        bool ret = x.updateStringPosition(this, incr[ret_dt]);
-        AlwaysAssert(ret == (total_inc[ret_dt] > 0));
-        x.d_has_string_pos = nrole;
-      }else{
-        SygusUnif::indent("sygus-pbe-dt", ind);
-        Trace("sygus-pbe-dt") << "PBE: failed CONCAT strategy, no values are "
-                              << (isPrefix ? "pre" : "suf")
-                              << "fix of all examples." << std::endl;
-      }
-    }
-    else
-    {
-      SygusUnif::indent("sygus-pbe-dt", ind);
-      Trace("sygus-pbe-dt")
-          << "PBE: failed CONCAT strategy, prefix/suffix mismatch."
-          << std::endl;
-    }
-  }
-  if (ret_dt.isNull() && !einfo.isTemplated())
-  {
-    // we will try a single strategy
-    EnumTypeInfoStrat* etis = nullptr;
-    std::map<NodeRole, StrategyNode>::iterator itsn =
-        tinfo.d_snodes.find(nrole);
-    if (itsn != tinfo.d_snodes.end())
-    {
-      // strategy info
-      StrategyNode& snode = itsn->second;
-      if (x.d_visit_role[e].find(nrole) == x.d_visit_role[e].end())
-      {
-        x.d_visit_role[e][nrole] = true;
-        // try a random strategy
-        if (snode.d_strats.size() > 1)
-        {
-          std::random_shuffle(snode.d_strats.begin(), snode.d_strats.end());
-        }
-        // get an eligible strategy index
-        unsigned sindex = 0;
-        while (sindex < snode.d_strats.size()
-               && !snode.d_strats[sindex]->isValid(this, x))
-        {
-          sindex++;
-        }
-        // if we found a eligible strategy
-        if (sindex < snode.d_strats.size())
-        {
-          etis = snode.d_strats[sindex];
-        }
-      }
-    }
-    if (etis != nullptr)
-    {
-      StrategyType strat = etis->d_this;
-      SygusUnif::indent("sygus-pbe-dt", ind + 1);
-      Trace("sygus-pbe-dt") << "...try STRATEGY " << strat << "..."
-                            << std::endl;
-
-      std::map<unsigned, Node> look_ahead_solved_children;
-      std::vector<Node> dt_children_cons;
-      bool success = true;
-
-      // for ITE
-      Node split_cond_enum;
-      int split_cond_res_index = -1;
-
-      for (unsigned sc = 0, size = etis->d_cenum.size(); sc < size; sc++)
-      {
-        SygusUnif::indent("sygus-pbe-dt", ind + 1);
-        Trace("sygus-pbe-dt") << "construct PBE child #" << sc << "..."
-                              << std::endl;
-        Node rec_c;
-        std::map<unsigned, Node>::iterator itla =
-            look_ahead_solved_children.find(sc);
-        if (itla != look_ahead_solved_children.end())
-        {
-          rec_c = itla->second;
-          SygusUnif::indent("sygus-pbe-dt-debug", ind + 1);
-          Trace("sygus-pbe-dt-debug") << "ConstructPBE: look ahead solved : "
-                                      << d_tds->sygusToBuiltin(rec_c)
-                                      << std::endl;
-        }
-        else
-        {
-          std::pair<Node, NodeRole>& cenum = etis->d_cenum[sc];
-
-          // update the context
-          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());
-            Assert(split_cond_res_index >= 0);
-            Assert(split_cond_res_index
-                   < (int)itnc->second.d_enum_vals_res.size());
-            prev = x.d_vals;
-            bool ret = x.updateContext(
-                this,
-                itnc->second.d_enum_vals_res[split_cond_res_index],
-                sc == 1);
-            AlwaysAssert(ret);
-          }
-
-          // recurse
-          if (strat == strat_ITE && sc == 0)
-          {
-            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;
-
-            // only used if the return value is not modified
-            if (!x.isReturnValueModified())
-            {
-              if (x.d_uinfo.find(ce) == x.d_uinfo.end())
-              {
-                Trace("sygus-pbe-dt-debug2")
-                    << "  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());
-                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());
-                  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();
-                       k < size;
-                       k++)
-                  {
-                    Node cond = einfo_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);
-                    Trace("sygus-pbe-dt-debug2")
-                        << "  reg : PBE: " << d_tds->sygusToBuiltin(cond)
-                        << " has " << solved.size() << " solutions in branch "
-                        << i << std::endl;
-                    if (!solved.empty())
-                    {
-                      Node slv = constructBestSolvedTerm(solved, x);
-                      Trace("sygus-pbe-dt-debug2")
-                          << "  reg : PBE: ..." << d_tds->sygusToBuiltin(slv)
-                          << " is a solution under branch " << i;
-                      Trace("sygus-pbe-dt-debug2")
-                          << " of condition " << d_tds->sygusToBuiltin(cond)
-                          << std::endl;
-                      x.d_uinfo[ce].d_look_ahead_sols[cond][i] = slv;
-                    }
-                  }
-                }
-              }
-            }
-
-            // get the conditionals in the current context : they must be
-            // 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);
-
-            std::map<int, std::vector<Node> >::iterator itpc =
-                possible_cond.find(0);
-            if (itpc != possible_cond.end())
-            {
-              if (Trace.isOn("sygus-pbe-dt-debug"))
-              {
-                SygusUnif::indent("sygus-pbe-dt-debug", ind + 1);
-                Trace("sygus-pbe-dt-debug")
-                    << "PBE : We have " << itpc->second.size()
-                    << " distinguishable conditionals:" << std::endl;
-                for (Node& cond : itpc->second)
-                {
-                  SygusUnif::indent("sygus-pbe-dt-debug", ind + 2);
-                  Trace("sygus-pbe-dt-debug") << d_tds->sygusToBuiltin(cond)
-                                              << std::endl;
-                }
-              }
-
-              // static look ahead conditional : choose conditionals that have
-              // solved terms in at least one branch
-              //    only applicable if we have not modified the return value
-              std::map<int, std::vector<Node> > solved_cond;
-              if (!x.isReturnValueModified())
-              {
-                Assert(x.d_uinfo.find(ce) != x.d_uinfo.end());
-                int solve_max = 0;
-                for (Node& cond : itpc->second)
-                {
-                  std::map<Node, std::map<unsigned, Node> >::iterator itla =
-                      x.d_uinfo[ce].d_look_ahead_sols.find(cond);
-                  if (itla != x.d_uinfo[ce].d_look_ahead_sols.end())
-                  {
-                    int nsolved = itla->second.size();
-                    solve_max = nsolved > solve_max ? nsolved : solve_max;
-                    solved_cond[nsolved].push_back(cond);
-                  }
-                }
-                int n = solve_max;
-                while (n > 0)
-                {
-                  if (!solved_cond[n].empty())
-                  {
-                    rec_c = constructBestSolvedConditional(solved_cond[n], x);
-                    SygusUnif::indent("sygus-pbe-dt", ind + 1);
-                    Trace("sygus-pbe-dt")
-                        << "PBE: ITE strategy : choose solved conditional "
-                        << d_tds->sygusToBuiltin(rec_c) << " with " << n
-                        << " solved children..." << std::endl;
-                    std::map<Node, std::map<unsigned, Node> >::iterator itla =
-                        x.d_uinfo[ce].d_look_ahead_sols.find(rec_c);
-                    Assert(itla != x.d_uinfo[ce].d_look_ahead_sols.end());
-                    for (std::pair<const unsigned, Node>& las : itla->second)
-                    {
-                      look_ahead_solved_children[las.first] = las.second;
-                    }
-                    break;
-                  }
-                  n--;
-                }
-              }
-
-              // otherwise, guess a conditional
-              if (rec_c.isNull())
-              {
-                rec_c = constructBestConditional(itpc->second, x);
-                Assert(!rec_c.isNull());
-                SygusUnif::indent("sygus-pbe-dt", ind);
-                Trace("sygus-pbe-dt")
-                    << "PBE: ITE strategy : choose random conditional "
-                    << d_tds->sygusToBuiltin(rec_c) << std::endl;
-              }
-            }
-            else
-            {
-              // TODO (#1250) : degenerate case where children have different
-              // types?
-              SygusUnif::indent("sygus-pbe-dt", ind);
-              Trace("sygus-pbe-dt") << "return PBE: failed ITE strategy, "
-                                       "cannot find a distinguishable condition"
-                                    << std::endl;
-            }
-            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];
-              split_cond_enum = ce;
-              Assert(split_cond_res_index >= 0);
-              Assert(split_cond_res_index
-                     < (int)einfo_child.d_enum_vals_res.size());
-            }
-          }
-          else
-          {
-            rec_c = constructSolution(c, cenum.first, cenum.second, x, ind + 2);
-          }
-
-          // undo update the context
-          if (strat == strat_ITE && sc > 0)
-          {
-            x.d_vals = prev;
-          }
-        }
-        if (!rec_c.isNull())
-        {
-          dt_children_cons.push_back(rec_c);
-        }
-        else
-        {
-          success = false;
-          break;
-        }
-      }
-      if (success)
-      {
-        Assert(dt_children_cons.size() == etis->d_sol_templ_args.size());
-        // ret_dt = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR,
-        // dt_children );
-        ret_dt = etis->d_sol_templ;
-        ret_dt = ret_dt.substitute(etis->d_sol_templ_args.begin(),
-                                   etis->d_sol_templ_args.end(),
-                                   dt_children_cons.begin(),
-                                   dt_children_cons.end());
-        SygusUnif::indent("sygus-pbe-dt-debug", ind);
-        Trace("sygus-pbe-dt-debug")
-            << "PBE: success : constructed for strategy " << strat << std::endl;
-      }else{
-        SygusUnif::indent("sygus-pbe-dt-debug", ind);
-        Trace("sygus-pbe-dt-debug") << "PBE: failed for strategy " << strat
-                                    << std::endl;
-      }
-    }
-  }
-
-  if( !ret_dt.isNull() ){
-    Assert( ret_dt.getType()==e.getType() );
-  }
-  SygusUnif::indent("sygus-pbe-dt", ind);
-  Trace("sygus-pbe-dt") << "ConstructPBE: returned " << ret_dt << std::endl;
-  return ret_dt;
-}
-
-bool CegConjecturePbe::EnumTypeInfoStrat::isValid(CegConjecturePbe* 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;
-}
-
-CegConjecturePbe::UnifContext::UnifContext() : d_has_string_pos(role_invalid)
-{
-  d_true = NodeManager::currentNM()->mkConst(true);
-  d_false = NodeManager::currentNM()->mkConst(false);
-}
-
-bool CegConjecturePbe::UnifContext::updateContext( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol ) {
-  Assert( d_vals.size()==vals.size() );
-  bool changed = false;
-  Node poln = pol ? d_true : d_false;
-  for( unsigned i=0; i<vals.size(); i++ ){
-    if( vals[i]!=poln ){
-      if (d_vals[i] == d_true)
-      {
-        d_vals[i] = d_false;
-        changed = true;
-      }
-    }
-  }
-  if (changed)
-  {
-    d_visit_role.clear();
-  }
-  return changed;
-}
-
-bool CegConjecturePbe::UnifContext::updateStringPosition( CegConjecturePbe * pbe, std::vector< unsigned >& pos ) {
-  Assert( pos.size()==d_str_pos.size() );
-  bool changed = false;
-  for( unsigned i=0; i<pos.size(); i++ ){
-    if( pos[i]>0 ){
-      d_str_pos[i] += pos[i];
-      changed = true;
-    }
-  }
-  if (changed)
-  {
-    d_visit_role.clear();
-  }
-  return changed;
-}
-
-bool CegConjecturePbe::UnifContext::isReturnValueModified() {
-  if (d_has_string_pos != role_invalid)
-  {
-    return true;
-  }
-  return false;
-}
-
-void CegConjecturePbe::UnifContext::initialize( CegConjecturePbe * pbe, Node c ) {
-  Assert( d_vals.empty() );
-  Assert( d_str_pos.empty() );
-  
-  // initialize with #examples
-  Assert( pbe->d_examples.find( c )!=pbe->d_examples.end() );
-  unsigned sz = pbe->d_examples[c].size();
-  for( unsigned i=0; i<sz; i++ ){
-    d_vals.push_back(d_true);
-  }
-  
-  if( !pbe->d_examples_out[c].empty() ){
-    // output type of the examples
-    TypeNode exotn = pbe->d_examples_out[c][0].getType();
-    
-    if( exotn.isString() ){
-      for( unsigned i=0; i<sz; i++ ){
-        d_str_pos.push_back( 0 );
-      }
-    }
-  }
-  d_visit_role.clear();
-}
-
-void CegConjecturePbe::UnifContext::getCurrentStrings(
-    CegConjecturePbe* pbe,
-    const std::vector<Node>& vals,
-    std::vector<String>& ex_vals)
-{
-  bool isPrefix = d_has_string_pos == role_string_prefix;
-  String dummy;
-  for( unsigned i=0; i<vals.size(); i++ ){
-    if( d_vals[i]==pbe->d_true ){
-      Assert( vals[i].isConst() );
-      unsigned pos_value = d_str_pos[i];
-      if( pos_value>0 ){
-        Assert(d_has_string_pos != role_invalid);
-        String s = vals[i].getConst<String>();
-        Assert( pos_value<=s.size() );
-        ex_vals.push_back( isPrefix ? s.suffix( s.size()-pos_value ) : 
-                                      s.prefix( s.size()-pos_value ) );
-      }else{
-        ex_vals.push_back( vals[i].getConst<String>() );
-      }
-    }else{
-      // irrelevant, add dummy
-      ex_vals.push_back( dummy );
-    }
-  }
-}
-
-bool CegConjecturePbe::UnifContext::getStringIncrement(
-    CegConjecturePbe* pbe,
-    bool isPrefix,
-    const std::vector<String>& ex_vals,
-    const std::vector<Node>& vals,
-    std::vector<unsigned>& inc,
-    unsigned& tot)
-{
-  for( unsigned j=0; j<vals.size(); j++ ){
-    unsigned ival = 0;
-    if( d_vals[j]==pbe->d_true ){
-      // example is active in this context
-      Assert( vals[j].isConst() );
-      String mystr = vals[j].getConst<String>();
-      ival = mystr.size();
-      if( mystr.size()<=ex_vals[j].size() ){
-        if( !( isPrefix ? ex_vals[j].strncmp(mystr, ival) : ex_vals[j].rstrncmp(mystr, ival) ) ){
-          Trace("sygus-pbe-dt-debug") << "X";
-          return false;
-        }
-      }else{
-        Trace("sygus-pbe-dt-debug") << "X";
-        return false;
-      }
-    }
-    Trace("sygus-pbe-dt-debug") << ival;
-    tot += ival;
-    inc.push_back( ival );
-  }
-  return true;
-}
-bool CegConjecturePbe::UnifContext::isStringSolved(
-    CegConjecturePbe* pbe,
-    const std::vector<String>& ex_vals,
-    const std::vector<Node>& vals)
-{
-  for( unsigned j=0; j<vals.size(); j++ ){
-    if( d_vals[j]==pbe->d_true ){
-      // example is active in this context
-      Assert( vals[j].isConst() );
-      String mystr = vals[j].getConst<String>();
-      if( ex_vals[j]!=mystr ){
-        return false;
-      }
-    }
-  }
-  return true;
-}
-
-CegConjecturePbe::StrategyNode::~StrategyNode()
-{
-  for (unsigned j = 0, size = d_strats.size(); j < size; j++)
-  {
-    delete d_strats[j];
-  }
-  d_strats.clear();
-}
 }
 }
 }
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h
index dd98dd0aa..fb353a102 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.h
+++ b/src/theory/quantifiers/sygus/sygus_pbe.h
@@ -47,10 +47,10 @@ class CegConjecture;
 *     via Divide and Conquer" TACAS 2017. In particular, it may consider
 *     strategies for constructing decision trees when the grammar permits ITEs
 *     and a strategy for divide-and-conquer string synthesis when the grammar
-*     permits string concatenation. This is stored in a set of data structures
-*     within d_cinfo.
+*     permits string concatenation. This is managed through the SygusUnif
+*     utilities, d_sygus_unif.
 * (3) It makes (possibly multiple) calls to
-*     TermDatabaseSygus::registerMeasuredTerm(...) based
+*     TermDatabaseSygus::regstierEnumerator(...) based
 *     on the strategy, which inform the rest of the system to enumerate values
 *     of particular types in the grammar through use of fresh variables which
 *     we call "enumerators".
@@ -58,14 +58,14 @@ class CegConjecture;
 * Points (1)-(3) happen within a call to CegConjecturePbe::initialize(...).
 *
 * Notice that each enumerator is associated with a single
-* function-to-synthesize, but a function-to-sythesize may be mapped to multiple 
-* enumerators. Some public functions of this class expect an enumerator as 
-* input, which we map to a function-to-synthesize via 
+* function-to-synthesize, but a function-to-sythesize may be mapped to multiple
+* enumerators. Some public functions of this class expect an enumerator as
+* input, which we map to a function-to-synthesize via
 * TermDatabaseSygus::getSynthFunFor(e).
 *
 * An enumerator is initially "active" but may become inactive if the enumeration
 * exhausts all possible values in the datatype corresponding to syntactic
-* restrictions for it. The search may continue unless all enumerators become 
+* restrictions for it. The search may continue unless all enumerators become
 * inactive.
 *
 * (4) During search, the extension of quantifier-free datatypes procedure for
@@ -73,7 +73,7 @@ class CegConjecture;
 *     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
+*     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
 *     them. The interface for querying this is
@@ -216,6 +216,21 @@ class CegConjecturePbe : public SygusModule
   * search space pruning.
   */
   std::map< Node, bool > d_examples_out_invalid;
+  /**
+   * Map from candidates to sygus unif utility. This class implements
+   * the core algorithm (e.g. decision tree learning) that this module relies
+   * upon.
+   */
+  std::map<Node, SygusUnif> d_sygus_unif;
+  /**
+   * map from candidates to the list of enumerators that are being used to
+   * build solutions for that candidate by the above utility.
+   */
+  std::map<Node, std::vector<Node> > d_candidate_to_enum;
+  /** reverse map of above */
+  std::map<Node, Node> d_enum_to_candidate;
+  /** map from enumerators to active guards */
+  std::map<Node, Node> d_enum_to_active_guard;
   /** for each candidate variable (function-to-synthesize), input of I/O
    * examples */
   std::map< Node, std::vector< std::vector< Node > > > d_examples;
@@ -258,583 +273,6 @@ class CegConjecturePbe : public SygusModule
   std::map<Node, std::map<TypeNode, PbeTrie> > d_pbe_trie;
   //--------------------------------- end PBE search values
 
-  // -------------------------------- decision tree learning
-  /** Subsumption trie
-  *
-  * This class manages a set of terms for a PBE sygus enumerator.
-  *
-  * In PBE sygus, we are interested in, for each term t, the set of I/O examples
-  * that it satisfies, which can be represented by a vector of Booleans.
-  * For example, given conjecture:
-  *   f( 1 ) = 2 ^ f( 3 ) = 4 ^ f( -1 ) = 1 ^ f( 5 ) = 5
-  * If solutions for f are of the form (lambda x. [term]), then:
-  *   Term x satisfies 0001,
-  *   Term x+1 satisfies 1100,
-  *   Term 2 satisfies 0100.
-  * Above, term 2 is subsumed by term x+1, since the set of I/O examples that
-  * x+1 satisfies are a superset of those satisfied by 2.
-  */
-  class SubsumeTrie
-  {
-   public:
-    SubsumeTrie() {}
-    /**
-    * Adds term t to the trie, removes all terms that are subsumed by t from the
-    * trie and adds them to subsumed. The set of I/O examples that t satisfies
-    * is given by (pol ? vals : !vals).
-    */
-    Node addTerm(Node t,
-                 const std::vector<Node>& vals,
-                 bool pol,
-                 std::vector<Node>& subsumed);
-    /**
-    * Adds term c to the trie, without calculating/updating based on
-    * subsumption. This is useful for using this class to store conditionals
-    * in ITE strategies, where any conditional whose set of vals is unique
-    * (as opposed to not subsumed) is useful.
-    */
-    Node addCond(Node c, const std::vector<Node>& vals, bool pol);
-    /**
-     * Returns the set of terms that are subsumed by (pol ? vals : !vals).
-     */
-    void getSubsumed(const std::vector<Node>& vals,
-                     bool pol,
-                     std::vector<Node>& subsumed);
-    /**
-     * Returns the set of terms that subsume (pol ? vals : !vals). This
-     * is for instance useful when determining whether there exists a term
-     * that satisfies all active examples in the decision tree learning
-     * algorithm.
-     */
-    void getSubsumedBy(const std::vector<Node>& vals,
-                       bool pol,
-                       std::vector<Node>& subsumed_by);
-    /**
-    * Get the leaves of the trie, which we store in the map v.
-    * v[-1] stores the children that always evaluate to !pol,
-    * v[1] stores the children that always evaluate to pol,
-    * v[0] stores the children that both evaluate to true and false for at least
-    * one example.
-    */
-    void getLeaves(const std::vector<Node>& vals,
-                   bool pol,
-                   std::map<int, std::vector<Node> >& v);
-    /** is this trie empty? */
-    bool isEmpty() { return d_term.isNull() && d_children.empty(); }
-    /** clear this trie */
-    void clear()
-    {
-      d_term = Node::null();
-      d_children.clear();
-    }
-
-   private:
-    /** the term at this node */
-    Node d_term;
-    /** the children nodes of this trie */
-    std::map<Node, SubsumeTrie> d_children;
-    /** helper function for above functions */
-    Node addTermInternal(Node t,
-                         const std::vector<Node>& vals,
-                         bool pol,
-                         std::vector<Node>& subsumed,
-                         bool spol,
-                         unsigned index,
-                         int status,
-                         bool checkExistsOnly,
-                         bool checkSubsume);
-    /** helper function for above functions */
-    void getLeavesInternal(const std::vector<Node>& vals,
-                           bool pol,
-                           std::map<int, std::vector<Node> >& v,
-                           unsigned index,
-                           int status);
-  };
-  // -------------------------------- end decision tree learning
-
-  //------------------------------ 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.
-  */
-  class EnumInfo
-  {
-   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(Node c, 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; }
-    /**
-    * The candidate variable that this enumerator is for (see sygus_pbe.h).
-    */
-    Node d_parent_candidate;
-    /** 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;
-    /**
-    * The active guard of this enumerator (see
-    * TermDbSygus::d_enum_to_active_guard).
-    */
-    Node d_active_guard;
-    /**
-    * 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
-    /**
-    * 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(CegConjecturePbe* pbe,
-                      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);
-    /** Have we been notified that a complete solution exists? */
-    bool isSolved() { return !d_enum_solved.isNull(); }
-    /** Get the complete solution to the synthesis conjecture. */
-    Node getSolved() { return d_enum_solved; }
-    /** Values that have been enumerated for this enumerator */
-    std::vector<Node> d_enum_vals;
-    /**
-      * This either stores the values of f( I ) for inputs
-      * or the value of f( I ) = O if d_role==enum_io
-      */
-    std::vector<std::vector<Node> > d_enum_vals_res;
-    /**
-    * The set of values in d_enum_vals that have been "subsumed" by others
-    * (see SubsumeTrie for explanation of subsumed).
-    */
-    std::vector<Node> d_enum_subsume;
-    /** Map from values to their index in d_enum_vals. */
-    std::map<Node, unsigned> d_enum_val_to_index;
-    /**
-    * A subsumption trie containing the values in d_enum_vals. Depending on the
-    * role of this enumerator, values may either be added to d_term_trie with
-    * subsumption (if role=enum_io), or without (if role=enum_ite_condition or
-    * 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;
-
-  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
-   */
-  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 isNonTrivial();
-  };
-  /** maps a function-to-synthesize to the above information */
-  std::map< Node, CandidateInfo > d_cinfo;
-
-  //------------------------------ representation of an enumeration strategy
-  /** add enumerated value
-   *
-   * We have enumerated the value v for x. This function adds x->v to the
-   * relevant data structures that are used for strategy-specific construction
-   * of solutions when necessary, and returns a set of lemmas, which are added
-   * to the input argument lems. These lemmas are used to rule out models where
-   * x = v, to force that a new value is enumerated for x.
-   */
-  void addEnumeratedValue( Node x, Node v, std::vector< Node >& lems );
-  /** domain-specific enumerator exclusion techniques
-   *
-   * Returns true if the value v for x can be excluded based on a
-   * domain-specific exclusion technique like the ones below.
-   *
-   * c : the candidate variable that x is enumerating for,
-   * results : the values of v under the input examples of c,
-   * 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 c, Node x, 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
-   *
-   * Values v for x 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
-   * 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);
-  /** 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 c.
-   */
-  void collectEnumeratorTypes(Node c, TypeNode tn, NodeRole nrole);
-  /** register enumerator
-   *
-   * This registers that et is an enumerator for function-to-synthesize c
-   * 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, Node c, 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 c, and stores these into lemmas.
-   */
-  void staticLearnRedundantOps(Node c, 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 c,
-      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
-  /** Unification context
-   *
-   * This class maintains state information during calls to
-   * CegConjecturePbe::constructSolution, which implements unification-based
-   * approaches for construction solutions to synthesis conjectures.
-   */
-  class UnifContext
-  {
-   public:
-    UnifContext();
-    /** this intiializes this context for function-to-synthesize c */
-    void initialize(CegConjecturePbe* pbe, Node c);
-
-    //----------for ITE strategy
-    /** the value of the context conditional
-    *
-    * This stores a list of Boolean constants that is the same length of the
-    * number of input/output example pairs we are considering. For each i,
-    * if d_vals[i] = true, i/o pair #i is active according to this context
-    * if d_vals[i] = false, i/o pair #i is inactive according to this context
-    */
-    std::vector<Node> d_vals;
-    /** update the examples
-    *
-    * if pol=true, this method updates d_vals to d_vals & vals
-    * if pol=false, this method updates d_vals to d_vals & ( ~vals )
-    */
-    bool updateContext(CegConjecturePbe* pbe,
-                       std::vector<Node>& vals,
-                       bool pol);
-    //----------end for ITE strategy
-
-    //----------for CONCAT strategies
-    /** the position in the strings
-    *
-    * For each i/o example pair, this stores the length of the current solution
-    * for the input of the pair, where the solution for that input is a prefix
-    * or
-    * suffix of the output of the pair. For example, if our i/o pairs are:
-    *   f( "abcd" ) = "abcdcd"
-    *   f( "aa" ) = "aacd"
-    * If the solution we have currently constructed is str.++( x1, "c", ... ),
-    * then d_str_pos = ( 5, 3 ), where notice that
-    *   str.++( "abc", "c" ) is a prefix of "abcdcd" and
-    *   str.++( "aa", "c" ) is a prefix of "aacd".
-    */
-    std::vector<unsigned> d_str_pos;
-    /** has string position
-    *
-    * Whether the solution positions indicate a prefix or suffix of the output
-    * examples. If this is role_invalid, then we have not updated the string
-    * position.
-    */
-    NodeRole d_has_string_pos;
-    /** update the string examples
-    *
-    * This method updates d_str_pos to d_str_pos + pos.
-    */
-    bool updateStringPosition(CegConjecturePbe* pbe,
-                              std::vector<unsigned>& pos);
-    /** get current strings
-    *
-    * This returns the prefix/suffix of the string constants stored in vals
-    * of size d_str_pos, and stores the result in ex_vals. For example, if vals
-    * is (abcdcd", "aacde") and d_str_pos = ( 5, 3 ), then we add
-    * "d" and "de" to ex_vals.
-    */
-    void getCurrentStrings(CegConjecturePbe* pbe,
-                           const std::vector<Node>& vals,
-                           std::vector<String>& ex_vals);
-    /** get string increment
-    *
-    * If this method returns true, then inc and tot are updated such that
-    *   for all active indices i,
-    *      vals[i] is a prefix (or suffix if isPrefix=false) of ex_vals[i], and
-    *      inc[i] = str.len(vals[i])
-    *   for all inactive indices i, inc[i] = 0
-    * We set tot to the sum of inc[i] for i=1,...,n. This indicates the total
-    * number of characters incremented across all examples.
-    */
-    bool getStringIncrement(CegConjecturePbe* pbe,
-                            bool isPrefix,
-                            const std::vector<String>& ex_vals,
-                            const std::vector<Node>& vals,
-                            std::vector<unsigned>& inc,
-                            unsigned& tot);
-    /** returns true if ex_vals[i] = vals[i] for all active indices i. */
-    bool isStringSolved(CegConjecturePbe* pbe,
-                        const std::vector<String>& ex_vals,
-                        const std::vector<Node>& vals);
-    //----------end for CONCAT strategies
-
-    /** is return value modified?
-    *
-    * This returns true if we are currently in a state where the return value
-    * of the solution has been modified, e.g. by a previous node that solved
-    * for a prefix.
-    */
-    bool isReturnValueModified();
-    /** visited role
-    *
-    * This is the current set of enumerator/node role pairs we are currently
-    * visiting. This set is cleared when the context is updated.
-    */
-    std::map<Node, std::map<NodeRole, bool> > d_visit_role;
-
-    /** unif context enumerator information */
-    class UEnumInfo
-    {
-     public:
-      UEnumInfo() {}
-      /** map from conditions and branch positions to a solved node
-      *
-      * For example, if we have:
-      *   f( 1 ) = 2 ^ f( 3 ) = 4 ^ f( -1 ) = 1
-      * Then, valid entries in this map is:
-      *   d_look_ahead_sols[x>0][1] = x+1
-      *   d_look_ahead_sols[x>0][2] = 1
-      * For the first entry, notice that  for all input examples such that x>0
-      * evaluates to true, which are (1) and (3), we have that their output
-      * values for x+1 under the substitution that maps x to the input value,
-      * resulting in 2 and 4, are equal to the output value for the respective
-      * pairs.
-      */
-      std::map<Node, std::map<unsigned, Node> > d_look_ahead_sols;
-    };
-    /** map from enumerators to the above info class */
-    std::map<Node, UEnumInfo> d_uinfo;
-
-   private:
-    /** true and false nodes */
-    Node d_true;
-    Node d_false;
-  };
-
-  /** construct solution
-   *
-   * This method tries to construct a solution for function-to-synthesize c
-   * based on the strategy stored for c in d_cinfo, which may include
-   * synthesis-by-unification approaches for ite and string concatenation terms.
-   * These approaches include the work of Alur et al. TACAS 2017.
-   * If it cannot construct a solution, it returns the null node.
-   */
-  Node constructSolution( Node c );
-  /** helper function for construct solution.
-   *
-   * Construct a solution based on enumerator e for function-to-synthesize c
-   * with node role nrole in context x.
-   *
-   * ind is the term depth of the context (for debugging).
-   */
-  Node constructSolution(
-      Node c, Node e, NodeRole nrole, UnifContext& x, int ind);
-  /** Heuristically choose the best solved term from solved in context x,
-   * currently return the first. */
-  Node constructBestSolvedTerm( std::vector< Node >& solved, UnifContext& x );
-  /** Heuristically choose the best solved string term  from solved in context
-   * x, currently  return the first. */
-  Node constructBestStringSolvedTerm( std::vector< Node >& solved, UnifContext& x );
-  /** Heuristically choose the best solved conditional term  from solved in
-   * context x, currently random */
-  Node constructBestSolvedConditional( std::vector< Node >& solved, UnifContext& x );
-  /** Heuristically choose the best conditional term  from conds in context x,
-   * currently random */
-  Node constructBestConditional( std::vector< Node >& conds, UnifContext& x );
-  /** Heuristically choose the best string to concatenate from strs to the
-  * solution in context x, currently random
-  * incr stores the vector of indices that are incremented by this solution in
-  * example outputs.
-  * total_inc[x] is the sum of incr[x] for each x in strs.
-  */
-  Node constructBestStringToConcat( std::vector< Node > strs,
-                                    std::map< Node, unsigned > total_inc, 
-                                    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( c, d_cenum[1], ... ) = t1,
-   *    ...,
-   *   constructSolution( c, 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(CegConjecturePbe* pbe, UnifContext& x);
-  };
 };
 
 }/* namespace CVC4::theory::quantifiers */
diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp
index ee0590b6b..2250deb6f 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif.cpp
@@ -514,36 +514,250 @@ void SubsumeTrie::getLeaves(const std::vector<Node>& vals,
   getLeavesInternal(vals, pol, v, 0, -2);
 }
 
-SygusUnif::SygusUnif(QuantifiersEngine* qe) : d_qe(qe)
+SygusUnif::SygusUnif()
 {
-  d_tds = qe->getTermDatabaseSygus();
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
 }
 
 SygusUnif::~SygusUnif() {}
 
-void SygusUnif::initialize(Node candidate,
-                           std::vector<Node>& lemmas,
-                           std::vector<Node>& enums)
+void SygusUnif::initialize(QuantifiersEngine* qe,
+                           Node f,
+                           std::vector<Node>& enums,
+                           std::vector<Node>& lemmas)
 {
-  d_candidate = candidate;
-  // TODO
+  d_candidate = f;
+  d_qe = qe;
+  d_tds = qe->getTermDatabaseSygus();
+
+  TypeNode tn = f.getType();
+  d_cinfo[f].initialize(f);
+  // collect the enumerator types and form the strategy
+  collectEnumeratorTypes(f, tn, role_equal);
+  // add the enumerators
+  enums.insert(enums.end(),
+               d_cinfo[f].d_esym_list.begin(),
+               d_cinfo[f].d_esym_list.end());
+  // learn redundant ops
+  staticLearnRedundantOps(f, lemmas);
 }
 
 void SygusUnif::resetExamples()
 {
+  d_examples.clear();
+  d_examples_out.clear();
+  // also clear information in strategy tree
   // TODO
 }
 
 void SygusUnif::addExample(const std::vector<Node>& input, Node output)
 {
-  // TODO
+  d_examples[d_candidate].push_back(input);
+  d_examples_out[d_candidate].push_back(output);
 }
 
 void SygusUnif::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
 {
-  // TODO
+  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());
+  // The explanation for why the current value should be excluded in future
+  // iterations.
+  Node exp_exc;
+
+  std::map<Node, CandidateInfo>::iterator itc = d_cinfo.find(c);
+  Assert(itc != d_cinfo.end());
+  TypeNode xtn = e.getType();
+  Node bv = d_tds->sygusToBuiltin(v, xtn);
+  std::map<Node, std::vector<std::vector<Node> > >::iterator itx =
+      d_examples.find(c);
+  std::map<Node, std::vector<Node> >::iterator itxo = d_examples_out.find(c);
+  Assert(itx != d_examples.end());
+  Assert(itxo != d_examples_out.end());
+  Assert(itx->second.size() == itxo->second.size());
+  std::vector<Node> base_results;
+  // compte the results
+  for (unsigned j = 0, size = itx->second.size(); j < size; j++)
+  {
+    Node res = d_tds->evaluateBuiltin(xtn, bv, itx->second[j]);
+    Trace("sygus-pbe-enum-debug")
+        << "...got res = " << res << " from " << bv << std::endl;
+    base_results.push_back(res);
+  }
+  // is it excluded for domain-specific reason?
+  std::vector<Node> exp_exc_vec;
+  if (getExplanationForEnumeratorExclude(
+          c, e, v, base_results, it->second, exp_exc_vec))
+  {
+    Assert(!exp_exc_vec.empty());
+    exp_exc = exp_exc_vec.size() == 1
+                  ? exp_exc_vec[0]
+                  : NodeManager::currentNM()->mkNode(AND, exp_exc_vec);
+    Trace("sygus-pbe-enum")
+        << "  ...fail : term is excluded (domain-specific)" << std::endl;
+  }
+  else
+  {
+    // notify all slaves
+    Assert(!it->second.d_enum_slave.empty());
+    // explanation for why this value should be excluded
+    for (unsigned s = 0; s < it->second.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());
+      Trace("sygus-pbe-enum") << "Process " << xs << " from " << s << std::endl;
+      // bool prevIsCover = false;
+      if (itv->second.getRole() == enum_io)
+      {
+        Trace("sygus-pbe-enum") << "   IO-Eval of ";
+        // prevIsCover = itv->second.isFeasible();
+      }
+      else
+      {
+        Trace("sygus-pbe-enum") << "Evaluation of ";
+      }
+      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;
+      std::map<Node, bool> cond_vals;
+      for (unsigned j = 0, size = base_results.size(); j < size; j++)
+      {
+        Node res = base_results[j];
+        Assert(res.isConst());
+        if (!templ.isNull())
+        {
+          TNode tres = res;
+          res = templ.substitute(templ_var, res);
+          res = Rewriter::rewrite(res);
+          Assert(res.isConst());
+        }
+        Node resb;
+        if (itv->second.getRole() == enum_io)
+        {
+          Node out = itxo->second[j];
+          Assert(out.isConst());
+          resb = res == out ? d_true : d_false;
+        }
+        else
+        {
+          resb = res;
+        }
+        cond_vals[resb] = true;
+        results.push_back(resb);
+        if (Trace.isOn("sygus-pbe-enum"))
+        {
+          if (resb.getType().isBoolean())
+          {
+            Trace("sygus-pbe-enum") << (resb == d_true ? "1" : "0");
+          }
+          else
+          {
+            Trace("sygus-pbe-enum") << "?";
+          }
+        }
+      }
+      bool keep = false;
+      if (itv->second.getRole() == enum_io)
+      {
+        // latter is the degenerate case of no examples
+        if (cond_vals.find(d_true) != cond_vals.end() || cond_vals.empty())
+        {
+          // check subsumbed/subsuming
+          std::vector<Node> subsume;
+          if (cond_vals.find(d_false) == cond_vals.end())
+          {
+            // it is the entire solution, we are done
+            Trace("sygus-pbe-enum")
+                << "  ...success, full solution added to PBE pool : "
+                << d_tds->sygusToBuiltin(v) << std::endl;
+            if (!itv->second.isSolved())
+            {
+              itv->second.setSolved(v);
+              // it subsumes everything
+              itv->second.d_term_trie.clear();
+              itv->second.d_term_trie.addTerm(v, results, true, subsume);
+            }
+            keep = true;
+          }
+          else
+          {
+            Node val =
+                itv->second.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());
+                Trace("sygus-pbe-enum")
+                    << " and subsumed " << subsume.size() << " terms";
+              }
+              Trace("sygus-pbe-enum")
+                  << "!   add to PBE pool : " << d_tds->sygusToBuiltin(v)
+                  << std::endl;
+              keep = true;
+            }
+            else
+            {
+              Assert(subsume.empty());
+              Trace("sygus-pbe-enum") << "  ...fail : subsumed" << std::endl;
+            }
+          }
+        }
+        else
+        {
+          Trace("sygus-pbe-enum")
+              << "  ...fail : it does not satisfy examples." << std::endl;
+        }
+      }
+      else
+      {
+        // must be unique up to examples
+        Node val = itv->second.d_term_trie.addCond(v, results, true);
+        if (val == v)
+        {
+          Trace("sygus-pbe-enum") << "  ...success!   add to PBE pool : "
+                                  << d_tds->sygusToBuiltin(v) << std::endl;
+          keep = true;
+        }
+        else
+        {
+          Trace("sygus-pbe-enum")
+              << "  ...fail : term is not unique" << std::endl;
+        }
+        itc->second.d_cond_count++;
+      }
+      if (keep)
+      {
+        // notify the parent to retry the build of PBE
+        itc->second.d_check_sol = true;
+        itv->second.addEnumValue(this, v, results);
+      }
+    }
+  }
+
+  // exclude this value on subsequent iterations
+  if (exp_exc.isNull())
+  {
+    // if we did not already explain why this should be excluded, use default
+    exp_exc = d_tds->getExplain()->getExplanationForEquality(e, v);
+  }
+  exp_exc = exp_exc.negate();
+  Trace("sygus-pbe-enum-lemma")
+      << "SygusUnif : enumeration exclude lemma : " << exp_exc << std::endl;
+  lemmas.push_back(exp_exc);
 }
 
 Node SygusUnif::constructSolution()
@@ -611,7 +825,7 @@ void SygusUnif::registerEnumerator(
         << static_cast<DatatypeType>(tn.toType()).getDatatype().getName();
     Trace("sygus-unif-debug") << ", role = " << enum_role
                               << ", in search = " << inSearch << std::endl;
-    d_einfo[et].initialize(c, enum_role);
+    d_einfo[et].initialize(enum_role);
     // if we are actually enumerating this (could be a compound node in the
     // strategy)
     if (inSearch)
@@ -1336,209 +1550,7 @@ void SygusUnif::staticLearnRedundantOps(
   }
 }
 
-// ------------------------------------------- solution construction from
-// enumeration
-
-void SygusUnif::addEnumeratedValue(Node x, Node v, std::vector<Node>& lems)
-{
-  std::map<Node, EnumInfo>::iterator it = d_einfo.find(x);
-  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());
-  Node c = it->second.d_parent_candidate;
-  // The explanation for why the current value should be excluded in future
-  // iterations.
-  Node exp_exc;
-
-  std::map<Node, CandidateInfo>::iterator itc = d_cinfo.find(c);
-  Assert(itc != d_cinfo.end());
-  TypeNode xtn = x.getType();
-  Node bv = d_tds->sygusToBuiltin(v, xtn);
-  std::map<Node, std::vector<std::vector<Node> > >::iterator itx =
-      d_examples.find(c);
-  std::map<Node, std::vector<Node> >::iterator itxo = d_examples_out.find(c);
-  Assert(itx != d_examples.end());
-  Assert(itxo != d_examples_out.end());
-  Assert(itx->second.size() == itxo->second.size());
-  std::vector<Node> base_results;
-  // compte the results
-  for (unsigned j = 0, size = itx->second.size(); j < size; j++)
-  {
-    Node res = d_tds->evaluateBuiltin(xtn, bv, itx->second[j]);
-    Trace("sygus-pbe-enum-debug")
-        << "...got res = " << res << " from " << bv << std::endl;
-    base_results.push_back(res);
-  }
-  // is it excluded for domain-specific reason?
-  std::vector<Node> exp_exc_vec;
-  if (getExplanationForEnumeratorExclude(
-          c, x, v, base_results, it->second, exp_exc_vec))
-  {
-    Assert(!exp_exc_vec.empty());
-    exp_exc = exp_exc_vec.size() == 1
-                  ? exp_exc_vec[0]
-                  : NodeManager::currentNM()->mkNode(AND, exp_exc_vec);
-    Trace("sygus-pbe-enum")
-        << "  ...fail : term is excluded (domain-specific)" << std::endl;
-  }
-  else
-  {
-    // notify all slaves
-    Assert(!it->second.d_enum_slave.empty());
-    // explanation for why this value should be excluded
-    for (unsigned s = 0; s < it->second.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());
-      Trace("sygus-pbe-enum") << "Process " << xs << " from " << s << std::endl;
-      // bool prevIsCover = false;
-      if (itv->second.getRole() == enum_io)
-      {
-        Trace("sygus-pbe-enum") << "   IO-Eval of ";
-        // prevIsCover = itv->second.isFeasible();
-      }
-      else
-      {
-        Trace("sygus-pbe-enum") << "Evaluation of ";
-      }
-      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;
-      std::map<Node, bool> cond_vals;
-      for (unsigned j = 0, size = base_results.size(); j < size; j++)
-      {
-        Node res = base_results[j];
-        Assert(res.isConst());
-        if (!templ.isNull())
-        {
-          TNode tres = res;
-          res = templ.substitute(templ_var, res);
-          res = Rewriter::rewrite(res);
-          Assert(res.isConst());
-        }
-        Node resb;
-        if (itv->second.getRole() == enum_io)
-        {
-          Node out = itxo->second[j];
-          Assert(out.isConst());
-          resb = res == out ? d_true : d_false;
-        }
-        else
-        {
-          resb = res;
-        }
-        cond_vals[resb] = true;
-        results.push_back(resb);
-        if (Trace.isOn("sygus-pbe-enum"))
-        {
-          if (resb.getType().isBoolean())
-          {
-            Trace("sygus-pbe-enum") << (resb == d_true ? "1" : "0");
-          }
-          else
-          {
-            Trace("sygus-pbe-enum") << "?";
-          }
-        }
-      }
-      bool keep = false;
-      if (itv->second.getRole() == enum_io)
-      {
-        // latter is the degenerate case of no examples
-        if (cond_vals.find(d_true) != cond_vals.end() || cond_vals.empty())
-        {
-          // check subsumbed/subsuming
-          std::vector<Node> subsume;
-          if (cond_vals.find(d_false) == cond_vals.end())
-          {
-            // it is the entire solution, we are done
-            Trace("sygus-pbe-enum")
-                << "  ...success, full solution added to PBE pool : "
-                << d_tds->sygusToBuiltin(v) << std::endl;
-            if (!itv->second.isSolved())
-            {
-              itv->second.setSolved(v);
-              // it subsumes everything
-              itv->second.d_term_trie.clear();
-              itv->second.d_term_trie.addTerm(v, results, true, subsume);
-            }
-            keep = true;
-          }
-          else
-          {
-            Node val =
-                itv->second.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());
-                Trace("sygus-pbe-enum")
-                    << " and subsumed " << subsume.size() << " terms";
-              }
-              Trace("sygus-pbe-enum")
-                  << "!   add to PBE pool : " << d_tds->sygusToBuiltin(v)
-                  << std::endl;
-              keep = true;
-            }
-            else
-            {
-              Assert(subsume.empty());
-              Trace("sygus-pbe-enum") << "  ...fail : subsumed" << std::endl;
-            }
-          }
-        }
-        else
-        {
-          Trace("sygus-pbe-enum")
-              << "  ...fail : it does not satisfy examples." << std::endl;
-        }
-      }
-      else
-      {
-        // must be unique up to examples
-        Node val = itv->second.d_term_trie.addCond(v, results, true);
-        if (val == v)
-        {
-          Trace("sygus-pbe-enum") << "  ...success!   add to PBE pool : "
-                                  << d_tds->sygusToBuiltin(v) << std::endl;
-          keep = true;
-        }
-        else
-        {
-          Trace("sygus-pbe-enum")
-              << "  ...fail : term is not unique" << std::endl;
-        }
-        itc->second.d_cond_count++;
-      }
-      if (keep)
-      {
-        // notify the parent to retry the build of PBE
-        itc->second.d_check_sol = true;
-        itv->second.addEnumValue(this, v, results);
-      }
-    }
-  }
-
-  // exclude this value on subsequent iterations
-  if (exp_exc.isNull())
-  {
-    // if we did not already explain why this should be excluded, use default
-    exp_exc = d_tds->getExplain()->getExplanationForEquality(x, v);
-  }
-  exp_exc = exp_exc.negate();
-  Trace("sygus-pbe-enum-lemma")
-      << "SygusUnif : enumeration exclude lemma : " << exp_exc << std::endl;
-  lems.push_back(exp_exc);
-}
+// ------------------------------------ solution construction from enumeration
 
 bool SygusUnif::useStrContainsEnumeratorExclude(Node x, EnumInfo& ei)
 {
@@ -1623,12 +1635,11 @@ bool SygusUnif::getExplanationForEnumeratorExclude(Node c,
         Trace("sygus-pbe-cterm-debug") << "...contained." << std::endl;
       }
     }
-    /* FIXME
     if (!cmp_indices.empty())
     {
       // we check invariance with respect to a negative contains test
       NegContainsSygusInvarianceTest ncset;
-      ncset.init(d_parent, x, itxo->second, cmp_indices);
+      ncset.init(x, d_examples[c], itxo->second, cmp_indices);
       // construct the generalized explanation
       d_tds->getExplain()->getExplanationFor(x, v, exp, ncset);
       Trace("sygus-pbe-cterm")
@@ -1636,7 +1647,6 @@ bool SygusUnif::getExplanationForEnumeratorExclude(Node c,
           << " due to negative containment." << std::endl;
       return true;
     }
-    */
   }
   return false;
 }
@@ -1645,16 +1655,14 @@ void SygusUnif::EnumInfo::addEnumValue(SygusUnif* pbe,
                                        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());
   d_enum_val_to_index[v] = d_enum_vals.size();
   d_enum_vals.push_back(v);
   d_enum_vals_res.push_back(results);
 }
 
-void SygusUnif::EnumInfo::initialize(Node c, EnumRole role)
-{
-  d_parent_candidate = c;
-  d_role = role;
-}
+void SygusUnif::EnumInfo::initialize(EnumRole role) { d_role = role; }
 
 void SygusUnif::EnumInfo::setSolved(Node slv) { d_enum_solved = slv; }
 
@@ -1886,6 +1894,7 @@ Node SygusUnif::constructSolution(
       for (unsigned i = 0, size = einfo.d_enum_vals.size(); i < size; i++)
       {
         Node val_t = einfo.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 << " : ";
diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h
index 68ed442a8..d46fb9c86 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.h
+++ b/src/theory/quantifiers/sygus/sygus_unif.h
@@ -339,7 +339,7 @@ class SygusUnif
   friend class UnifContext;
 
  public:
-  SygusUnif(QuantifiersEngine* qe);
+  SygusUnif();
   ~SygusUnif();
 
   /** initialize
@@ -356,7 +356,10 @@ class SygusUnif
    * those that exclude ITE from enumerators whose role is enum_io when the
    * strategy is ITE_strat).
    */
-  void initialize(Node f, std::vector<Node>& enums, std::vector<Node>& lemmas);
+  void initialize(QuantifiersEngine* qe,
+                  Node f,
+                  std::vector<Node>& enums,
+                  std::vector<Node>& lemmas);
   /** reset examples
    *
    * Reset the specification for f.
@@ -432,7 +435,7 @@ class SygusUnif
     * role is the "role" the enumerator plays in the high-level strategy,
     *   which is one of enum_* above.
     */
-    void initialize(Node c, EnumRole role);
+    void initialize(EnumRole role);
     /** is this enumerator associated with a template? */
     bool isTemplated() { return !d_template.isNull(); }
     /** set conditional
@@ -447,10 +450,6 @@ class SygusUnif
     bool isConditional() { return d_is_conditional; }
     /** get the role of this enumerator */
     EnumRole getRole() { return d_role; }
-    /**
-    * The candidate variable that this enumerator is for (see sygus_pbe.h).
-    */
-    Node d_parent_candidate;
     /** enumerator template
     *
     * If d_template non-null, enumerated values V are immediately transformed to
@@ -586,15 +585,6 @@ class SygusUnif
   std::map<Node, CandidateInfo> d_cinfo;
 
   //------------------------------ representation of an enumeration strategy
-  /** add enumerated value
-   *
-   * We have enumerated the value v for x. This function adds x->v to the
-   * relevant data structures that are used for strategy-specific construction
-   * of solutions when necessary, and returns a set of lemmas, which are added
-   * to the input argument lems. These lemmas are used to rule out models where
-   * x = v, to force that a new value is enumerated for x.
-   */
-  void addEnumeratedValue(Node x, Node v, std::vector<Node>& lems);
   /** domain-specific enumerator exclusion techniques
    *
    * Returns true if the value v for x can be excluded based on a