Refactor and generalize PBE strategies (#1410)

2 files changed, 1481 insertions, 824 deletions

diff --git a/src/theory/quantifiers/ce_guided_pbe.cpp b/src/theory/quantifiers/ce_guided_pbe.cpp
index 97cded35c..d46fed686 100644
--- a/src/theory/quantifiers/ce_guided_pbe.cpp
+++ b/src/theory/quantifiers/ce_guided_pbe.cpp
@@ -23,11 +23,10 @@
 
 using namespace CVC4;
 using namespace CVC4::kind;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace std;
 
 namespace CVC4 {
+namespace theory {
+namespace quantifiers {
 
 void indent( const char * c, int ind ) {
   if( Trace.isOn(c) ){
@@ -46,26 +45,55 @@ void print_val( const char * c, std::vector< Node >& vals, bool pol = true ){
   }
 }
 
-void CegConjecturePbe::print_role(const char* c, unsigned r)
+std::ostream& operator<<(std::ostream& os, EnumRole r)
 {
   switch(r){
-  case CegConjecturePbe::enum_io:Trace(c) << "IO";break;
-  case CegConjecturePbe::enum_ite_condition:Trace(c) << "CONDITION";break;
-  case CegConjecturePbe::enum_concat_term:Trace(c) << "CTERM";break;
-  case CegConjecturePbe::enum_any:Trace(c) << "ANY";break;
-  default:Trace(c) << "role_" << r;break;
+    case enum_invalid: os << "INVALID"; break;
+    case enum_io: os << "IO"; break;
+    case enum_ite_condition: os << "CONDITION"; break;
+    case enum_concat_term: os << "CTERM"; break;
+    default: os << "enum_" << static_cast<unsigned>(r); break;
   }
+  return os;
 }
 
-void CegConjecturePbe::print_strat(const char* c, unsigned s)
+std::ostream& operator<<(std::ostream& os, NodeRole r)
 {
-  switch (s)
+  switch (r)
   {
-    case CegConjecturePbe::strat_ITE: Trace(c) << "ITE"; break;
-    case CegConjecturePbe::strat_CONCAT: Trace(c) << "CONCAT"; break;
-    case CegConjecturePbe::strat_ID: Trace(c) << "ID"; break;
-    default: Trace(c) << "strat_" << s; break;
+    case role_equal: os << "equal"; break;
+    case role_string_prefix: os << "string_prefix"; break;
+    case role_string_suffix: os << "string_suffix"; break;
+    case role_ite_condition: os << "ite_condition"; break;
+    default: os << "role_" << static_cast<unsigned>(r); break;
   }
+  return os;
+}
+
+EnumRole getEnumeratorRoleForNodeRole(NodeRole r)
+{
+  switch (r)
+  {
+    case role_equal: return enum_io; break;
+    case role_string_prefix: return enum_concat_term; break;
+    case role_string_suffix: return enum_concat_term; break;
+    case role_ite_condition: return enum_ite_condition; break;
+    default: break;
+  }
+  return enum_invalid;
+}
+
+std::ostream& operator<<(std::ostream& os, StrategyType st)
+{
+  switch (st)
+  {
+    case strat_ITE: os << "ITE"; break;
+    case strat_CONCAT_PREFIX: os << "CONCAT_PREFIX"; break;
+    case strat_CONCAT_SUFFIX: os << "CONCAT_SUFFIX"; break;
+    case strat_ID: os << "ID"; break;
+    default: os << "strat_" << static_cast<unsigned>(st); break;
+  }
+  return os;
 }
 
 CegConjecturePbe::CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p)
@@ -196,7 +224,7 @@ void CegConjecturePbe::initialize(Node n,
         TypeNode ctn = c.getType();
         d_cinfo[c].initialize( c );
         // collect the enumerator types / form the strategy
-        collectEnumeratorTypes( c, ctn, enum_io );
+        collectEnumeratorTypes(c, ctn, role_equal);
         // if we have non-trivial strategies, then use pbe
         if( d_cinfo[c].isNonTrivial() ){
           // static learning of redundant constructors
@@ -340,289 +368,514 @@ Node CegConjecturePbe::evaluateBuiltin(TypeNode tn, Node bn, Node e,
 
 // ----------------------------- establishing enumeration types
 
-
-void CegConjecturePbe::registerEnumerator( Node et, Node c, TypeNode tn, unsigned enum_role, bool inSearch ) {
-  Trace("sygus-unif-debug") << "...register " << et << " for " << ((DatatypeType)tn.toType()).getDatatype().getName();
-  Trace("sygus-unif-debug") << ", role = ";
-  print_role( "sygus-unif-debug", enum_role );
-  Trace("sygus-unif-debug") << ", 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::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, unsigned enum_role ) {
-  if( d_cinfo[e].d_tinfo.find( tn )==d_cinfo[e].d_tinfo.end() ){
+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 );
   }
-  if( d_cinfo[e].d_tinfo[tn].d_enum.find( enum_role )==d_cinfo[e].d_tinfo[tn].d_enum.end() ){
-  
-    Node ee = NodeManager::currentNM()->mkSkolem( "ee", tn );
-    d_cinfo[e].d_tinfo[tn].d_enum[enum_role] = ee;
-    Trace("sygus-unif-debug") << "...enumerator " << ee << " for " << ((DatatypeType)tn.toType()).getDatatype().getName() << ", role = ";
-    print_role( "sygus-unif-debug", enum_role );
-    Trace("sygus-unif-debug") << std::endl;
-    // wait to register : may or may not actually be enumerating it
-
-    if( enum_role==enum_io ){
-      // look at information on how we will construct solutions for this type
-      Assert( tn.isDatatype() );
-      const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype();
-      Assert( dt.isSygus() );
-      std::map< Node, std::vector< TypeNode > > cop_to_child_types;
-      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, unsigned > cop_to_strat;
-      std::map< Node, unsigned > cop_to_cindex;
-
-      // look at builtin operartors first (when r=0), then defined operators
-      // (when r=1)
-      for( unsigned r=0; r<2; r++ ){
-        for( unsigned j=0; j<dt.getNumConstructors(); j++ ){
-          Node cop = Node::fromExpr( dt[j].getConstructor() );
-          Node op = Node::fromExpr( dt[j].getSygusOp() );
-          if( r==0 ){
-            cop_to_cindex[cop] = j;
-            if( op.getKind() == kind::BUILTIN ){
-              Kind sk = NodeManager::operatorToKind( op );
-              if( sk==kind::ITE ){
-                // we can do unification
-                Assert( dt[j].getNumArgs()==3 );
-                cop_to_strat[cop] = strat_ITE;
-              }else if( sk==kind::STRING_CONCAT ){
-                if( dt[j].getNumArgs()==2 ) {
-                  cop_to_strat[cop] = strat_CONCAT;
-                }
-              }
-              if( cop_to_strat.find( cop )!=cop_to_strat.end() ){
-                Trace("sygus-unif") << "...type " << dt.getName()
-                                    << " has strategy ";
-                print_strat("sygus-unif", cop_to_strat[cop]);
-                Trace("sygus-unif") << "..." << std::endl;
-                // add child types
-                for( unsigned k=0; k<dt[j].getNumArgs(); k++ ){
-                  TypeNode ct = TypeNode::fromType( dt[j][k].getRangeType() );
-                  Trace("sygus-unif") << "   Child type " << k << " : " << ((DatatypeType)ct.toType()).getDatatype().getName() << std::endl;
-                  cop_to_child_types[cop].push_back( ct );
-                }
-              }
+  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();
             }
-          }else if( cop_to_strat.find( cop )==cop_to_strat.end() ){
-            // could be a defined function (this handles the ICFP benchmarks)
-            std::vector< Node > utchildren;
-            utchildren.push_back( cop );
-            std::vector< Node > sks;
-            std::vector< TypeNode > sktns;
-            for( unsigned k=0; k<dt[j].getNumArgs(); k++ ){
-              Type t = dt[j][k].getRangeType();
-              TypeNode ttn = TypeNode::fromType( t );
-              Node kv = NodeManager::currentNM()->mkSkolem( "ut", ttn );
-              sks.push_back( kv );
-              sktns.push_back( ttn );
-              utchildren.push_back( kv );
+            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);
             }
-            Node ut = NodeManager::currentNM()->mkNode( kind::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( unsigned k=0; k<sbvl.getNumChildren(); k++ ){
-              echildren.push_back( sbvl[k] );
+            else
+            {
+              assoc_waiting.push_back(k);
             }
-            Node eut = NodeManager::currentNM()->mkNode( kind::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 << std::endl;       
-            Trace("sygus-unif-debug2") << "Type : " << eut.getType() << std::endl;     
-
-            if( eut.getKind()==kind::ITE ){
-              if( dt[j].getNumArgs()>=eut.getNumChildren() ){
-                cop_to_strat[cop] = strat_ITE;
-              }
-            }else if( eut.getKind()==kind::STRING_CONCAT ){
-              if (dt[j].getNumArgs() >= eut.getNumChildren()
-                  && eut.getNumChildren() == 2)
+          }
+        }
+      }
+      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_strat[cop] = strat_CONCAT;
-              }
-            }else if( eut.getKind()==kind::APPLY_UF ){
-              // identity operator?
-              if( dt[j].getNumArgs()==1 ){
-                cop_to_strat[cop] = strat_ID;
-              }
-            }
-            
-            if( cop_to_strat.find( cop )!=cop_to_strat.end() ){
-              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; k<sks.size(); k++ ){
-                Assert( sks[k].getType().isDatatype() );
-                const Datatype& cdt = ((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 = NodeManager::currentNM()->mkNode( kind::APPLY_UF, echildren );
-                vs.push_back( esk );
-                Node tvar = NodeManager::currentNM()->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") << "Defined constructor " << j << ", base term is " << eut << std::endl;
-              std::map< unsigned, Node > test_args;
-              if( cop_to_strat[cop] == strat_ID ){
-                test_args[0] = eut;
+                cop_to_carg_list[cop].push_back(sk_index);
               }else{
-                for( unsigned k=0; k<eut.getNumChildren(); k++ ){
-                  test_args[k] = eut[k];
-                }
+                Trace("sygus-unif-debug") << "...fail: duplicate argument used"
+                                          << std::endl;
+                cop_to_strat.erase(cop);
+                break;
               }
-              for( std::map< unsigned, Node >::iterator it = test_args.begin(); it != test_args.end(); ++it ){
-                unsigned k = it->first;
-                Node eut_c = it->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-debug2") << "...failed to find injection (range)." << std::endl;
-                  cop_to_strat.erase( cop );
-                  break;
-                }
-                if( templ_injection.find( k )==templ_injection.end() ){
-                  Trace("sygus-unif-debug2") << "...failed to find injection (domain)." << 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);
               }
-              if( cop_to_strat.find( cop )!=cop_to_strat.end() ){
-                Trace("sygus-unif") << "...type " << dt.getName() << " has defined constructor matching strategy ";
-                print_strat("sygus-unif", cop_to_strat[cop]);
-                Trace("sygus-unif") << "..." << std::endl;
-                for( unsigned k=0; k<eut.getNumChildren(); k++ ){
-                  Assert( templ_injection.find( k )!=templ_injection.end() );
-                  unsigned sk_index = templ_injection[k];
-                  //also store the template information, if necessary
-                  Node teut = eut[k];
-                  if( !teut.isVar() ){
-                    if( cop_to_strat[cop] == strat_ID ){
-                      Trace("sygus-unif-debug") << "...cannot use template with ID strategy." << std::endl;
-                      cop_to_strat.erase( cop );
-                    }else{
-                      cop_to_child_templ[cop][k] = teut;
-                      cop_to_child_templ_arg[cop][k] = ss[sk_index];
-                      Trace("sygus-unif") << "  Arg " << k << " : template : " << teut << ", arg " << ss[sk_index] << std::endl;
-                    }
-                  }else{
-                    Assert( teut==ss[sk_index] );
-                  }
-                }
-                // collect children types
-                for( unsigned k=0; k<dt[j].getNumArgs(); k++ ){
-                  Trace("sygus-unif") << "   Child type " << k << " : " << ((DatatypeType)sktns[k].toType()).getDatatype().getName() << std::endl;
-                  cop_to_child_types[cop].push_back( sktns[k] );
-                }
+              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);
+            }
           }
         }
       }
-      bool search_this = true;
-      for( std::map< Node, unsigned >::iterator itc = cop_to_strat.begin(); itc != cop_to_strat.end(); ++itc ){
-        if( itc->second==strat_CONCAT || ( itc->second==strat_ID && dt.getNumConstructors()==1 ) ){
-          search_this = false;
-          break;
-        }
+    }
+    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);
       }
-      Trace("sygus-unif-debug2") << "...this register..." << std::endl;
-      registerEnumerator( ee, e, tn, enum_role, search_this );
-      
-      if( cop_to_child_types.empty() ){
-        Trace("sygus-unif") << "...consider " << dt.getName() << " a basic type" << std::endl;
-      }else{
-        for( std::map< Node, std::vector< TypeNode > >::iterator itct = cop_to_child_types.begin(); itct != cop_to_child_types.end(); ++itct ){
-          Node cop = itct->first;
-          Assert( cop_to_strat.find( cop )!=cop_to_strat.end() );
-          unsigned strat = cop_to_strat[cop];
-          d_cinfo[e].d_tinfo[tn].d_strat[cop].d_this = strat;
-          Trace("sygus-unif-debug") << "Process strategy for operator : " << cop << " : ";
-          print_strat("sygus-unif-debug", strat );
-          Trace("sygus-unif-debug") << std::endl;
-
-          for( unsigned j=0; j<itct->second.size(); j++ ){
-            //calculate if we should allocate a new enumerator : should be true if we have a new role
-            unsigned enum_role_c = enum_role;
-            if( strat==strat_ITE ){
-              if( j==0 ){
-                enum_role_c = enum_ite_condition;
-              }else{
-                // role is the same as parent
-              }
-            }else if( strat==strat_CONCAT ){
-              enum_role_c = enum_concat_term;
-            }else if( strat==strat_ID ){
-              // role is the same as parent
+    }
+  }
+
+  // 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;
             }
-            
-            // register the child type
-            TypeNode ct = itct->second[j];
-            d_cinfo[e].d_tinfo[tn].d_strat[cop].d_csol_cts.push_back( ct );
-            
-            // 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 = NodeManager::currentNM()->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, enum_role_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() << ", role = ";
-              print_role( "sygus-unif-debug", enum_role_c );
-              Trace("sygus-unif-debug") << std::endl;
-              collectEnumeratorTypes( e, ct, enum_role_c );
-              // otherwise use the previous
-              Assert( d_cinfo[e].d_tinfo[ct].d_enum.find( enum_role_c )!=d_cinfo[e].d_tinfo[ct].d_enum.end() );
-              et = d_cinfo[e].d_tinfo[ct].d_enum[enum_role_c];
+          }
+          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;
             }
-            Trace("sygus-unif-debug") << "Register child enumerator " << et << ", arg " << j << " of " << cop << ", role = ";
-            print_role( "sygus-unif-debug", enum_role_c );
-            Trace("sygus-unif-debug") << std::endl;
-            Assert( !et.isNull() );
-            d_cinfo[e].d_tinfo[tn].d_strat[cop].d_cenum.push_back( et );
           }
-          Trace("sygus-unif") << "Initialized strategy ";
-          print_strat( "sygus-unif", strat );
+          // 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 = " << d_cinfo[e].d_tinfo[tn].d_strat[cop].d_cenum.size() << std::endl;
-          Assert( d_cinfo[e].d_tinfo[tn].d_strat[cop].d_cenum.size()==d_cinfo[e].d_tinfo[tn].d_strat[cop].d_csol_cts.size() );
+          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);
       }
-    }else{
-      Trace("sygus-unif-debug") << "...this register (non-io)" << std::endl;
-      registerEnumerator( ee, e, tn, enum_role, true );
     }
   }
 }
@@ -637,6 +890,7 @@ bool CegConjecturePbe::inferTemplate( unsigned k, Node n, std::map< Node, unsign
         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;
       }
     }
@@ -663,112 +917,137 @@ void CegConjecturePbe::staticLearnRedundantOps( Node c, std::vector< Node >& lem
       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 = ";
-      print_role("sygus-unif", itns->second.getRole());
-      Trace("sygus-unif") << std::endl;
+      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, bool > visited;
-  std::vector< Node > redundant;
-  staticLearnRedundantOps( c, d_cinfo[c].getRootEnumerator(), visited, redundant, lemmas, 0 );
-  for( unsigned i=0; i<lemmas.size(); i++ ){  
-    Trace("sygus-unif") << "...can exclude based on  : " << lemmas[i] << 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);
+  // 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, std::map< Node, bool >& visited, std::vector< Node >& redundant,
-                                                std::vector< Node >& lemmas, int ind ) {
-
+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)
+{
   std::map< Node, EnumInfo >::iterator itn = d_einfo.find( e );
-  Assert( itn!=d_einfo.end() );                                    
-  if( visited.find( e )==visited.end() ){
-    visited[e] = true;
+  Assert( itn!=d_einfo.end() );
+  if (visited[e].find(nrole) == visited[e].end())
+  {
+    visited[e][nrole] = true;
 
     indent("sygus-unif", ind);
-    Trace("sygus-unif") << e << " : role : ";
-    print_role("sygus-unif", itn->second.getRole());
-    Trace("sygus-unif") << " : ";
+    Trace("sygus-unif") << e << " :: node role : " << nrole;
+    Trace("sygus-unif")
+        << ", type : "
+        << ((DatatypeType)e.getType().toType()).getDatatype().getName();
+    Trace("sygus-unif") << ", enum role : " << itn->second.getRole();
 
     if( itn->second.isTemplated() ){
-      Trace("sygus-unif") << "basic, templated : \\ " << itn->second.d_template_arg << ". " << itn->second.d_template << std::endl;
+      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() );
-      if( itt->second.d_strat.empty() ){
-        Trace("sygus-unif") << "basic" << std::endl;
-      }else{
-        Trace("sygus-unif") << "compound" << std::endl;
-        // various strategies 
-        for( std::map< Node, EnumTypeInfoStrat >::iterator itts = itt->second.d_strat.begin(); itts!=itt->second.d_strat.end(); ++itts ){
+      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())
+      {
+        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;
           indent("sygus-unif", ind+1);
-          Trace("sygus-unif") << "Strategy : ";
-          unsigned strat = itts->second.d_this;
-          print_strat("sygus-unif", strat);
-          Trace("sygus-unif") << std::endl;
-          for( unsigned i=0; i<itts->second.d_cenum.size(); i++ ){
-            std::vector< Node > redundant_c;
-            bool no_repeat_op = false;
-            // do not repeat operators that the strategy uses
-            if( itts->second.d_csol_cts[i]==etn ){
-              if( strat==strat_ITE && i!=0 ){
-                no_repeat_op = true;
-              }else if( strat==strat_CONCAT || strat==strat_ID ){
-                no_repeat_op = true;
-              }
-            }
-            if( no_repeat_op ){
-              redundant_c.push_back( itts->first );
+          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);
+          }
+        }
+        // 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())
+        {
+          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;
             }
-            //do not use standard Boolean connectives in ITE conditions
-            if( strat==strat_ITE && i==0 && itts->second.d_csol_cts[1]==itts->second.d_csol_cts[2] ){
-              TypeNode ctn = itts->second.d_csol_cts[0];
-              const Datatype& cdt = ((DatatypeType)ctn.toType()).getDatatype();
-              for( unsigned j=0; j<cdt.getNumConstructors(); j++ ){
-                Kind ck = d_tds->getConsNumKind( ctn, j );
-                if( ck!=UNDEFINED_KIND && TermUtil::isBoolConnective( ck ) ){
-                  bool typeCorrect = true;
-                  for( unsigned k=0; k<cdt[j].getNumArgs(); k++ ){
-                    if( d_tds->getArgType( cdt[j], k )!=ctn ){
-                      typeCorrect = false;
-                      break;
-                    }
-                  }
-                  if( typeCorrect ){
-                    Trace("sygus-unif-debug") << "Exclude Boolean connective in ITE conditional : " << ck << " in conditional type " << cdt.getName() << std::endl;
-                    Node exc_cons = Node::fromExpr( cdt[j].getConstructor() );
-                    if( std::find( redundant_c.begin(), redundant_c.end(), exc_cons )==redundant_c.end() ){
-                      redundant_c.push_back( exc_cons );
-                    }
-                  }
-                }
-              }
+          }
+          // 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];
             }
-            // recurse
-            staticLearnRedundantOps( c, itts->second.d_cenum[i], visited, redundant_c, lemmas, ind+2 );
           }
         }
       }
     }
   }else{
     indent("sygus-unif", ind);
-    Trace("sygus-unif") << e << std::endl;
-  }
-  if( !redundant.empty() ){
-    // TODO : if this becomes more general, must get master enumerator here
-    if( itn->second.d_enum_slave.size()==1 ){
-      for( unsigned i=0; i<redundant.size(); i++ ){
-        int cindex = Datatype::indexOf( redundant[i].toExpr() );
-        Assert( cindex!=-1 );
-        const Datatype& dt = Datatype::datatypeOf( redundant[i].toExpr() );
-        Node tst = datatypes::DatatypesRewriter::mkTester( e, cindex, dt ).negate();
-        if( std::find( lemmas.begin(), lemmas.end(), tst )==lemmas.end() ){
-          lemmas.push_back( tst );
-        }
-      }
-    }
+    Trace("sygus-unif") << e << " :: node role : " << nrole << std::endl;
   }
 }
 
@@ -937,7 +1216,9 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >&
           std::vector< Node > exp_exc_vec;
           if( getExplanationForEnumeratorExclude( c, x, v, 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( kind::AND, exp_exc_vec );
+            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{
             //if( cond_vals.size()!=2 ){
@@ -981,7 +1262,8 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >&
       // if we did not already explain why this should be excluded, use default
       exp_exc = d_tds->getExplain()->getExplanationForConstantEquality(x, v);
     }
-    Node exlem = NodeManager::currentNM()->mkNode( kind::OR, g.negate(), exp_exc.negate() );
+    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 );
   }else{
@@ -1017,7 +1299,8 @@ bool CegConjecturePbe::getExplanationForEnumeratorExclude( Node c, Node x, Node
         cmp_indices[index].push_back( i );
         */
         Trace("sygus-pbe-cterm-debug") << "  " << results[i] << " <> " << itxo->second[i];
-        Node cont = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, itxo->second[i], results[i] );
+        Node cont = NodeManager::currentNM()->mkNode(
+            STRING_STRCTN, itxo->second[i], results[i]);
         Node contr = Rewriter::rewrite( cont );
         if( contr==d_false ){
           cmp_indices.push_back( i );
@@ -1067,6 +1350,12 @@ void CegConjecturePbe::EnumInfo::addEnumValue( CegConjecturePbe * pbe, Node v, s
   */
 }
 
+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;
@@ -1083,7 +1372,7 @@ void CegConjecturePbe::CandidateInfo::initializeType( TypeNode tn ) {
 }
 
 Node CegConjecturePbe::CandidateInfo::getRootEnumerator() {
-  std::map< unsigned, Node >::iterator it = d_tinfo[d_root].d_enum.find( enum_io );
+  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;
 }
@@ -1346,7 +1635,7 @@ Node CegConjecturePbe::constructSolution( Node c ){
         Node e = itc->second.getRootEnumerator();
         UnifContext x;
         x.initialize( this, c );
-        Node vcc = constructSolution( c, e, x, 1 );
+        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;
@@ -1399,409 +1688,509 @@ Node CegConjecturePbe::constructBestStringToConcat( std::vector< Node > strs,
                                                     std::map< Node, std::vector< unsigned > > incr,
                                                     UnifContext& x ) {
   Assert( !strs.empty() );
-  // TODO
-  double r = Random::getRandom().pickDouble(0.0, 1.0);
-  unsigned cindex = r*strs.size();
-  if( cindex>strs.size() ){
-    cindex = strs.size() - 1;
-  }
-  return strs[cindex];
-}                         
-                                    
-Node CegConjecturePbe::constructSolution( Node c, Node e, UnifContext& x, int ind ) {
-  indent("sygus-pbe-dt-debug", ind);
-  Trace("sygus-pbe-dt-debug") << "ConstructPBE: enum: " << e << " in context ";
-  print_val("sygus-pbe-dt-debug", x.d_vals);
-  Trace("sygus-pbe-dt-debug") << std::endl;
+  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"))
+  {
+    indent("sygus-pbe-dt-debug", ind);
+    Trace("sygus-pbe-dt-debug") << "ConstructPBE: (" << e << ", " << nrole
+                                << ") for type " << etn << " in context ";
+    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 (itn->second.getRole() == enum_any)
-  {
-    indent("sygus-pbe-dt", ind);
-    ret_dt = constructBestSolvedTerm( itn->second.d_enum_vals, x );
-    Trace("sygus-pbe-dt") << "return PBE: success : use any " << d_tds->sygusToBuiltin( ret_dt ) << std::endl;
-    Assert( !ret_dt.isNull() );
-  }
-  else if (itn->second.getRole() == enum_io && !x.isReturnValueModified()
-           && itn->second.isSolved())
+  if (nrole == role_equal)
   {
-    // this type has a complete solution
-    ret_dt = itn->second.getSolved();
-    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{
-    TypeNode etn = e.getType();
-    std::map< TypeNode, EnumTypeInfo >::iterator itt = d_cinfo[c].d_tinfo.find( etn );
-    Assert( itt!=d_cinfo[c].d_tinfo.end() );
-    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;
-      if (itn->second.getRole() == enum_concat_term)
+    if (!x.isReturnValueModified())
+    {
+      if (einfo.isSolved())
       {
-        itet = itn;
-      }else{
-        std::map< unsigned, Node >::iterator itnt = itt->second.d_enum.find( enum_concat_term );
+        // this type has a complete solution
+        ret_dt = einfo.getSolved();
+        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(this, x.d_vals, true, subsumed_by);
+        if (!subsumed_by.empty())
+        {
+          ret_dt = constructBestSolvedTerm(subsumed_by, x);
+          indent("sygus-pbe-dt", ind);
+          Trace("sygus-pbe-dt") << "return PBE: success : conditionally solved"
+                                << d_tds->sygusToBuiltin(ret_dt) << std::endl;
+        }
+        else
+        {
+          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 ){
-        Assert( itet!=d_einfo.end() );
-
-        // 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< CVC4::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; i<itet->second.d_enum_vals.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 (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);
+            indent("sygus-pbe-dt", ind);
+            Trace("sygus-pbe-dt") << "return PBE: success : string solved "
+                                  << d_tds->sygusToBuiltin(ret_dt) << std::endl;
+          }
+          else
+          {
+            indent("sygus-pbe-dt-debug", ind);
+            Trace("sygus-pbe-dt-debug") << "  ...not currently string solved."
+                                        << std::endl;
           }
-        }
-        if( !str_solved.empty() ){
-          ret_dt = constructBestStringSolvedTerm( str_solved, x );
-          indent("sygus-pbe-dt", ind);
-          Trace("sygus-pbe-dt") << "return PBE: success : string solved " << d_tds->sygusToBuiltin( ret_dt ) << std::endl;
-        }else{
-          indent("sygus-pbe-dt-debug", ind);
-          Trace("sygus-pbe-dt-debug") << "  ...not currently string solved." << std::endl;
         }
       }
     }
-    else if (itn->second.getRole() == enum_io && !x.isReturnValueModified())
+  }
+  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)
     {
-      // it has an enumerated value that is conditionally correct under the current assumptions
-      std::vector< Node > subsumed_by;
-      itn->second.d_term_trie.getSubsumedBy( this, x.d_vals, true, subsumed_by );
-      if( !subsumed_by.empty() ){
-        ret_dt = constructBestSolvedTerm( subsumed_by, x );
+      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"))
+      {
+        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++)
+        {
+          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];
+        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());
         indent("sygus-pbe-dt", ind);
-        Trace("sygus-pbe-dt") << "return PBE: success : conditionally solved" << d_tds->sygusToBuiltin( ret_dt ) << std::endl;
+        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{
-        indent("sygus-pbe-dt-debug", ind);
-        Trace("sygus-pbe-dt-debug") << "  ...not currently conditionally solved." << std::endl;
+        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;
       }
     }
-    if( ret_dt.isNull() ){
-      if( !itn->second.isTemplated() ){
-        // try to construct a compound solution, if strategies are available
-        
-        // do various strategies 
-        for( std::map< Node, EnumTypeInfoStrat >::iterator itts = itt->second.d_strat.begin(); itts!=itt->second.d_strat.end(); ++itts ){
-          std::map< unsigned, Node > dt_children_cons;
-          unsigned strat = itts->second.d_this;
-          
-          bool success = true;
-          
-          // for ITE
-          std::map< unsigned, Node > look_ahead_solved_children;
-          Node split_cond_enum;
-          int split_cond_res_index = -1;
-          
-          //for CONCAT
-          Node incr_val;
-          int incr_type = 0;
-          std::map< Node, std::vector< unsigned > > incr;
-
-          // construct the child order based on heuristics
-          std::vector< unsigned > corder;
-          std::unordered_set<unsigned> cused;
-          if( strat==strat_CONCAT ){
-            for( unsigned r=0; r<2; r++ ){
-              // Concatenate strategy can only be applied from the endpoints.
-              // This chooses the appropriate endpoint for which we stay within
-              // the same SyGuS type.
-              // In other words, if we are synthesizing based on a production
-              // rule ( T -> str.++( T1, ..., Tn ) ), then we
-              // prefer recursing on the 1st argument of the concat if T1 = T,
-              // and the last argument if Tn = T.
-              unsigned sc = r==0 ? 0 : itts->second.d_cenum.size()-1;
-              Node ce = itts->second.d_cenum[sc];
-              if( ce.getType()==etn ){
-                // prefer simple recursion (self type)
-                Assert( d_einfo.find( ce )!=d_einfo.end() );
-                Assert(d_einfo[ce].getRole() == enum_concat_term);
-                corder.push_back( sc );
-                cused.insert(sc);
-                break;
-              }
-            }
+    else
+    {
+      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()
+               && !x.isValidStrategy(snode.d_strats[sindex]))
+        {
+          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;
+      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++)
+      {
+        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;
+          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);
           }
-          // fill remaining children for which there is no preference
-          for (unsigned sc = 0; sc < itts->second.d_cenum.size(); sc++)
+
+          // recurse
+          if (strat == strat_ITE && sc == 0)
           {
-            if (cused.find(sc) == cused.end())
+            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())
             {
-              corder.push_back( sc );
-            }
-          }
-          Assert( corder.size()==itts->second.d_cenum.size() );
-            
-            
-          for( unsigned scc=0; scc<corder.size(); scc++ ){
-            unsigned sc = corder[scc];
-            Node rec_c;
-            indent("sygus-pbe-dt", ind);
-            Trace("sygus-pbe-dt") << "construct PBE child #" << sc << "..." << std::endl;
-            std::map< unsigned, Node >::iterator itla = look_ahead_solved_children.find( sc );
-            if( itla!=look_ahead_solved_children.end() ){
-              rec_c = itla->second;
-              indent("sygus-pbe-dt-debug", ind+1);
-              Trace("sygus-pbe-dt-debug") << "ConstructPBE: look ahead solved : " << d_tds->sygusToBuiltin( rec_c ) << std::endl;
-            }else{
-              // get the child enumerator
-              Node ce = itts->second.d_cenum[sc];
-              if( strat==strat_ITE && scc==0 ){
-                Assert( itts->second.d_cenum.size()==3 ); // for now, fix to 3 child ITEs
-                // choose a condition
-                
-                // register the condition enumerator
-                std::map< Node, EnumInfo >::iterator itnc = d_einfo.find( ce );
-                Assert( itnc!=d_einfo.end() );
-                // 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;
-                    x.d_uinfo[ce].d_status = 0;
-                    Assert( itnc->second.d_enum_vals.size()==itnc->second.d_enum_vals_res.size() );
-                    for( unsigned i=1; i<=2; i++ ){
-                      Node te = itts->second.d_cenum[i];
-                      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; k<itnc->second.d_enum_vals.size(); k++ ){
-                        Node cond = itnc->second.d_enum_vals[k];
-                        std::vector< Node > solved;
-                        itnt->second.d_term_trie.getSubsumedBy( this, itnc->second.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-debug") << "  reg : PBE: ..." << d_tds->sygusToBuiltin( slv ) << " is a solution under branch " << i;
-                          Trace("sygus-pbe-dt-debug") << " 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
-                itnc->second.d_term_trie.getLeaves( this, x.d_vals, true, possible_cond );
-                
-                std::map< int, std::vector< Node > >::iterator itpc = possible_cond.find( 0 );
-                if( itpc!=possible_cond.end() ){
-                  indent("sygus-pbe-dt-debug", ind);
-                  Trace("sygus-pbe-dt-debug") << "PBE : We have " << itpc->second.size() << " distinguishable conditionals:" << std::endl;       
-                  for( unsigned k=0; k<itpc->second.size(); k++ ){                  
-                    indent("sygus-pbe-dt-debug", ind+1);
-                    Trace("sygus-pbe-dt-debug") << d_tds->sygusToBuiltin( itpc->second[k] ) << 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( unsigned k=0; k<itpc->second.size(); k++ ){
-                      Node cond = itpc->second[k];
-                      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 );
-                        indent("sygus-pbe-dt", ind);
-                        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::map< unsigned, Node >::iterator itla2 = itla->second.begin(); itla2 != itla->second.end(); ++itla2 ){
-                          look_ahead_solved_children[ itla2->first ] = itla2->second;
-                        }
-                        break;
-                      }
-                      n--;
+              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(
+                        this,
+                        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;
                     }
                   }
-                  
-                  // dynamic look ahead conditional : compute if there are any solved terms in this branch  TODO
-                  if( ind>0 ){
-                    
-                  }
-                  
-                  // otherwise, guess a conditional
-                  if( rec_c.isNull() ){
-                    rec_c = constructBestConditional( itpc->second, x );
-                    Assert( !rec_c.isNull() );
-                    indent("sygus-pbe-dt", ind);
-                    Trace("sygus-pbe-dt") << "PBE: ITE strategy : choose random conditional " << d_tds->sygusToBuiltin( rec_c ) << std::endl;
-                  }
-                }else{
-                  // TODO : degenerate case where children have different types
-                  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( itnc->second.d_enum_val_to_index.find( rec_c )!=itnc->second.d_enum_val_to_index.end() );
-                  split_cond_res_index = itnc->second.d_enum_val_to_index[rec_c];
-                  split_cond_enum = ce;
-                  Assert( split_cond_res_index>=0 );
-                  Assert( split_cond_res_index<(int)itnc->second.d_enum_vals_res.size() );
+              }
+            }
+
+            // 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(
+                this, 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"))
+              {
+                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)
+                {
+                  indent("sygus-pbe-dt-debug", ind + 2);
+                  Trace("sygus-pbe-dt-debug") << d_tds->sygusToBuiltin(cond)
+                                              << std::endl;
                 }
-              }else if( strat==strat_CONCAT && scc==0 ){
-                std::map< Node, EnumInfo >::iterator itsc = d_einfo.find( ce );
-                Assert( itsc!=d_einfo.end() );
-                // ensured by the child order we set above
-                Assert(itsc->second.getRole() == enum_concat_term);
-                // check if each return value is a prefix/suffix of all open examples
-                incr_type = sc==0 ? -1 : 1;
-                if( x.d_has_string_pos==0 || x.d_has_string_pos==incr_type ){
-                  bool isPrefix = incr_type==-1;
-                  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< CVC4::String > ex_vals;
-                  x.getCurrentStrings( this, itx->second, ex_vals );
-
-                  // check if there is a value for which is a prefix/suffix of all active examples
-                  Assert( itsc->second.d_enum_vals.size()==itsc->second.d_enum_vals_res.size() );
-                  
-                  for( unsigned i=0; i<itsc->second.d_enum_vals.size(); i++ ){
-                    Node val_t = itsc->second.d_enum_vals[i];
-                    indent("sygus-pbe-dt-debug", ind);
-                    Trace("sygus-pbe-dt-debug") << "increment string values : " << val_t << " : ";
-                    Assert( itsc->second.d_enum_vals_res[i].size()==itx->second.size() );
-                    unsigned tot = 0;
-                    bool exsuccess = x.getStringIncrement( this, isPrefix, ex_vals, itsc->second.d_enum_vals_res[i], incr[val_t], tot );
-                    if( tot==0 ){
-                      exsuccess = false;
-                    }
-                    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() ){
-                    rec_c = constructBestStringToConcat( inc_strs, total_inc, incr, x );
-                    incr_val = rec_c;
-                    Assert( !rec_c.isNull() );
-                    indent("sygus-pbe-dt", ind);
-                    Trace("sygus-pbe-dt") << "PBE: CONCAT strategy : choose " << ( isPrefix ? "pre" : "suf" ) << "fix value " << d_tds->sygusToBuiltin( rec_c ) << std::endl;
-                  }else{
-                    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;
+              // 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);
                   }
-                }else{
-                  indent("sygus-pbe-dt", ind);
-                  Trace("sygus-pbe-dt") << "PBE: failed CONCAT strategy, prefix/suffix mismatch." << std::endl;
-                }
-              }else{
-                // a standard term
-                
-                // store previous values
-                std::vector< Node > prev;
-                std::vector< unsigned > prev_str_pos;
-                int prev_has_str_pos = false;
-                // update the context
-                bool ret = false;
-                if( strat==strat_ITE ){
-                  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;
-                  ret = x.updateContext( this, itnc->second.d_enum_vals_res[split_cond_res_index], sc==1 );
-                }else if( strat==strat_CONCAT ){
-                  prev_str_pos = x.d_str_pos;
-                  prev_has_str_pos = x.d_has_string_pos;
-                  Assert( incr.find( incr_val )!=incr.end() );
-                  ret = x.updateStringPosition( this, incr[incr_val] );
-                  x.d_has_string_pos = incr_type;
-                }else if( strat==strat_ID ){
-                  ret = true;
                 }
-                // must have updated the context
-                AlwaysAssert( ret );
-                // recurse
-                rec_c = constructSolution( c, ce, x, ind+1 );
-                if( !rec_c.isNull() ){
-                  //revert context
-                  if( strat==strat_ITE ){
-                    x.d_vals = prev;
-                  }else if( strat==strat_CONCAT ){
-                    x.d_str_pos = prev_str_pos;
-                    x.d_has_string_pos = prev_has_str_pos;
+                int n = solve_max;
+                while (n > 0)
+                {
+                  if (!solved_cond[n].empty())
+                  {
+                    rec_c = constructBestSolvedConditional(solved_cond[n], x);
+                    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());
+                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?
+              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() ){
-              dt_children_cons[sc] = rec_c;
-            }else{
-              success = false;
-              break;
+              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());
             }
           }
-          if( success ){
-            std::vector< Node > dt_children;
-            Assert( !itts->first.isNull() );
-            dt_children.push_back( itts->first );
-            for( unsigned sc=0; sc<itts->second.d_cenum.size(); sc++ ){
-              std::map< unsigned, Node >::iterator itdc = dt_children_cons.find( sc );
-              Assert( itdc!=dt_children_cons.end() );
-              dt_children.push_back( itdc->second );
-            }         
-            ret_dt = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, dt_children );
-            indent("sygus-pbe-dt-debug", ind);
-            Trace("sygus-pbe-dt-debug") << "PBE: success : constructed for strategy ";
-            print_strat( "sygus-pbe-dt-debug", strat );
-            Trace("sygus-pbe-dt-debug") << std::endl;
-            break;
-          }else{
-            indent("sygus-pbe-dt-debug", ind);
-            Trace("sygus-pbe-dt-debug") << "PBE: failed for strategy ";
-            print_strat( "sygus-pbe-dt-debug", strat );
-            Trace("sygus-pbe-dt-debug") << std::endl;
+          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( ret_dt.isNull() ){
-          indent("sygus-pbe-dt", ind);
-          Trace("sygus-pbe-dt") << "return PBE: fail : all strategies failed " << std::endl;
+        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());
+        indent("sygus-pbe-dt-debug", ind);
+        Trace("sygus-pbe-dt-debug")
+            << "PBE: success : constructed for strategy " << strat << std::endl;
       }else{
-        indent("sygus-pbe-dt", ind);
-        Trace("sygus-pbe-dt") << "return PBE: fail : non-basic" << std::endl;
+        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() );
   }
@@ -1822,6 +2211,10 @@ bool CegConjecturePbe::UnifContext::updateContext( CegConjecturePbe * pbe, std::
       }
     }
   }
+  if (changed)
+  {
+    d_visit_role.clear();
+  }
   return changed;
 }
 
@@ -1834,16 +2227,35 @@ bool CegConjecturePbe::UnifContext::updateStringPosition( CegConjecturePbe * pbe
       changed = true;
     }
   }
+  if (changed)
+  {
+    d_visit_role.clear();
+  }
   return changed;
 }
 
 bool CegConjecturePbe::UnifContext::isReturnValueModified() {
-  if( d_has_string_pos!=0 ){
+  if (d_has_string_pos != role_invalid)
+  {
     return true;
   }
   return false;
 }
 
+bool CegConjecturePbe::UnifContext::isValidStrategy(EnumTypeInfoStrat* etis)
+{
+  StrategyType st = etis->d_this;
+  if (d_has_string_pos == role_string_prefix && st == strat_CONCAT_SUFFIX)
+  {
+    return false;
+  }
+  if (d_has_string_pos == role_string_suffix && st == strat_CONCAT_PREFIX)
+  {
+    return false;
+  }
+  return true;
+}
+
 void CegConjecturePbe::UnifContext::initialize( CegConjecturePbe * pbe, Node c ) {
   Assert( d_vals.empty() );
   Assert( d_str_pos.empty() );
@@ -1865,19 +2277,23 @@ void CegConjecturePbe::UnifContext::initialize( CegConjecturePbe * pbe, Node c )
       }
     }
   }
+  d_visit_role.clear();
 }
 
-
-void CegConjecturePbe::UnifContext::getCurrentStrings( CegConjecturePbe * pbe, std::vector< Node >& vals, std::vector< CVC4::String >& ex_vals ) {
-  bool isPrefix = d_has_string_pos==-1;
-  CVC4::String dummy;
+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!=0 );
-        CVC4::String s = vals[i].getConst<String>();
+        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 ) );
@@ -1891,13 +2307,20 @@ void CegConjecturePbe::UnifContext::getCurrentStrings( CegConjecturePbe * pbe, s
   }
 }
 
-bool CegConjecturePbe::UnifContext::getStringIncrement( CegConjecturePbe * pbe, bool isPrefix, std::vector< CVC4::String >& ex_vals, std::vector< Node >& vals, std::vector< unsigned >& inc, unsigned& tot ) {
+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() );
-      CVC4::String mystr = vals[j].getConst<String>();
+      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) ) ){
@@ -1915,12 +2338,16 @@ bool CegConjecturePbe::UnifContext::getStringIncrement( CegConjecturePbe * pbe,
   }
   return true;
 }
-bool CegConjecturePbe::UnifContext::isStringSolved( CegConjecturePbe * pbe, std::vector< CVC4::String >& ex_vals, std::vector< Node >& vals ) {
+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() );
-      CVC4::String mystr = vals[j].getConst<String>();
+      String mystr = vals[j].getConst<String>();
       if( ex_vals[j]!=mystr ){
         return false;
       }
@@ -1942,4 +2369,14 @@ int CegConjecturePbe::getGuardStatus( Node g ) {
   }
 }
 
+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/ce_guided_pbe.h b/src/theory/quantifiers/ce_guided_pbe.h
index b357e4d15..1abdda6a6 100644
--- a/src/theory/quantifiers/ce_guided_pbe.h
+++ b/src/theory/quantifiers/ce_guided_pbe.h
@@ -25,6 +25,70 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+/** roles for enumerators
+ *
+ * This indicates the role of an enumerator that is allocated by approaches
+ * for synthesis-by-unification (see details below).
+ *   io : the enumerator should enumerate values that are overall solutions
+ *        for the function-to-synthesize,
+ *   ite_condition : the enumerator should enumerate values that are useful
+ *                   in ite conditions in the ITE strategy,
+ *   concat_term : the enumerator should enumerate values that are used as
+ *                 components of string concatenation solutions.
+ */
+enum EnumRole
+{
+  enum_invalid,
+  enum_io,
+  enum_ite_condition,
+  enum_concat_term,
+};
+std::ostream& operator<<(std::ostream& os, EnumRole r);
+
+/** roles for strategy nodes
+ *
+ * This indicates the role of a strategy node, which is a subprocedure of
+ * CegConjecturePbe::constructSolution (see details below).
+ *   equal : the node constructed must be equal to the overall solution for
+ *           the function-to-synthesize,
+ *   string_prefix/suffix : the node constructed must be a prefix/suffix
+ *                          of the function-to-synthesize,
+ *   ite_condition : the node constructed must be a condition that makes some
+ *                   active input examples true and some input examples false.
+ */
+enum NodeRole
+{
+  role_invalid,
+  role_equal,
+  role_string_prefix,
+  role_string_suffix,
+  role_ite_condition,
+};
+std::ostream& operator<<(std::ostream& os, NodeRole r);
+
+/** enumerator role for node role */
+EnumRole getEnumeratorRoleForNodeRole(NodeRole r);
+
+/** strategy types
+ *
+ * This indicates a strategy for synthesis-by-unification (see details below).
+ *   ITE : strategy for constructing if-then-else solutions via decision
+ *         tree learning techniques,
+ *   CONCAT_PREFIX/SUFFIX : strategy for constructing string concatenation
+ *         solutions via a divide and conquer approach,
+ *   ID : identity strategy used for calling strategies on child type through
+ *        an identity function.
+ */
+enum StrategyType
+{
+  strat_INVALID,
+  strat_ITE,
+  strat_CONCAT_PREFIX,
+  strat_CONCAT_SUFFIX,
+  strat_ID,
+};
+std::ostream& operator<<(std::ostream& os, StrategyType st);
+
 class CegConjecture;
 
 /** CegConjecturePbe
@@ -316,26 +380,12 @@ class CegConjecturePbe {
 
   //------------------------------ representation of a enumeration strategy
 
-  /** roles for enumerators */
-  enum {
-    enum_io,
-    enum_ite_condition,
-    enum_concat_term,
-    enum_any,
-  };
-  /** print the role with Trace c. */
-  static void print_role(const char* c, unsigned r);
-  /** strategies for SyGuS datatype types */
-  enum
-  {
-    strat_ITE,
-    strat_CONCAT,
-    strat_ID,
-  };
-  /** print the strategy with Trace c. */
-  static void print_strat(const char* c, unsigned s);
-
-  /** information about an enumerator */
+  /** information about an 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,
+   */
   class EnumInfo {
   public:
     EnumInfo() : d_role( enum_io ){}
@@ -344,11 +394,7 @@ class CegConjecturePbe {
     * role is the "role" the enumerator plays in the high-level strategy,
     *   which is one of enum_* above.
     */
-    void initialize(Node c, unsigned role)
-    {
-      d_parent_candidate = c;
-      d_role = role;
-    }
+    void initialize(Node c, EnumRole role);
     bool isTemplated() { return !d_template.isNull(); }
     void addEnumValue(CegConjecturePbe* pbe,
                       Node v,
@@ -356,7 +402,7 @@ class CegConjecturePbe {
     void setSolved(Node slv);
     bool isSolved() { return !d_enum_solved.isNull(); }
     Node getSolved() { return d_enum_solved; }
-    unsigned getRole() { return d_role; }
+    EnumRole getRole() { return d_role; }
     Node d_parent_candidate;
     // for template
     Node d_template;
@@ -366,9 +412,10 @@ class CegConjecturePbe {
     std::vector< Node > d_enum_slave;
     /** values we have enumerated */
     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
-    */
+    /**
+     * 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;
     std::vector< Node > d_enum_subsume;
     std::map< Node, unsigned > d_enum_val_to_index;
@@ -379,32 +426,70 @@ class CegConjecturePbe {
      * conjecture */
     Node d_enum_solved;
     /** the role of this enumerator (one of enum_* above). */
-    unsigned d_role;
+    EnumRole d_role;
   };
   /** maps enumerators to the information above */
   std::map< Node, EnumInfo > d_einfo;
 
   class CandidateInfo;
-  /** represents a strategy for a SyGuS datatype type */
+
+  /** 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 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) }
+   */
   class EnumTypeInfoStrat {
-  public:
-    unsigned d_this;
-    /** conditional solutions */
-    std::vector< TypeNode > d_csol_cts;
-    std::vector< Node > d_cenum;
+   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;
+  };
+
+  /** 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;
-    // role -> _
-    std::map< unsigned, Node > d_enum;
+    /** the type that this information is for */
     TypeNode d_this_type;
-    // strategies for enum_io role
-    std::map< Node, EnumTypeInfoStrat > d_strat;
-    bool isSolved( CegConjecturePbe * pbe );
+    /** 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
@@ -413,17 +498,20 @@ class CegConjecturePbe {
   public:
     CandidateInfo() : d_check_sol( false ), d_cond_count( 0 ){}
     Node d_this_candidate;
-    /** root SyGuS datatype for the function-to-synthesize,
-    * which encodes the overall syntactic restrictions on the space
-    * of solutions.
-    */
-    TypeNode d_root;
-    /** Information for each SyGuS datatype type occurring in a field of d_root
+    /**
+     * 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 enumerator */
+    /**
+     * 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;
@@ -442,76 +530,208 @@ class CegConjecturePbe {
   bool getExplanationForEnumeratorExclude( Node c, Node x, Node v, std::vector< Node >& results, EnumInfo& ei, std::vector< Node >& exp );
 
   //------------------------------ strategy registration
-  void collectEnumeratorTypes(Node c, TypeNode tn, unsigned enum_role);
+  /** 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, unsigned enum_role, bool inSearch);
-  void staticLearnRedundantOps(Node c, std::vector<Node>& lemmas);
-  void staticLearnRedundantOps(Node c,
-                               Node e,
-                               std::map<Node, bool>& visited,
-                               std::vector<Node>& redundant,
-                               std::vector<Node>& lemmas,
-                               int ind);
-
-  /** register candidate conditional */
+      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).
+   */
+  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);
   //------------------------------ end strategy registration
 
   //------------------------------ constructing solutions
   class UnifContext {
   public:
-    UnifContext() : d_has_string_pos(0) {}
-    //IndexFilter d_filter;
-    // the value of the context conditional
-    std::vector< Node > d_vals;
-    // update the examples
-    bool updateContext( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol );
-    // the position in the strings
-    std::vector< unsigned > d_str_pos;
-    // 0 : pos not modified, 1 : pos indicates suffix incremented, -1 : pos indicates prefix incremented
-    int d_has_string_pos;
-    // update the string examples
-    bool updateStringPosition( CegConjecturePbe * pbe, std::vector< unsigned >& pos );
-    // is return value modified 
-    bool isReturnValueModified();
-    class UEnumInfo {
+   UnifContext() : d_has_string_pos(role_invalid) {}
+   /** 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();
+   /** returns true if argument is valid strategy in this context */
+   bool isValidStrategy(EnumTypeInfoStrat* etis);
+   /** 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() : d_status(-1){}
-      int d_status;
-      // enum val -> polarity -> solved
-      std::map< Node, std::map< unsigned, Node > > d_look_ahead_sols;
+     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;
     };
-    // enumerator -> info
+    /** map from enumerators to the above info class */
     std::map< Node, UEnumInfo > d_uinfo;
-    void initialize( CegConjecturePbe * pbe, Node c );
-    void getCurrentStrings( CegConjecturePbe * pbe, std::vector< Node >& vals, std::vector< CVC4::String >& ex_vals );
-    bool getStringIncrement( CegConjecturePbe * pbe, bool isPrefix, std::vector< CVC4::String >& ex_vals, 
-                             std::vector< Node >& vals, std::vector< unsigned >& inc, unsigned& tot );
-    bool isStringSolved( CegConjecturePbe * pbe, std::vector< CVC4::String >& ex_vals, std::vector< Node >& vals );
   };
-  /** construct solution */
+
+  /** 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,
-  * in context x, where ind is the term depth of the context.
-  */
-  Node constructSolution( Node c, Node e, UnifContext& x, int ind );
+   *
+   * 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
+  /** 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,
+  /** 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
+  /** 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.
@@ -524,14 +744,14 @@ class CegConjecturePbe {
   //------------------------------ end constructing solutions
 
   /** get guard status
-  * Returns 1 if g is asserted true in the SAT solver.
-  * Returns -1 if g is asserted false in the SAT solver.
-  * Returns 0 otherwise.
-  */
+   *
+   * Returns 1 if g is asserted true in the SAT solver.
+   * Returns -1 if g is asserted false in the SAT solver.
+   * Returns 0 otherwise.
+   */
   int getGuardStatus(Node g);
 };
 
-
 }/* namespace CVC4::theory::quantifiers */
 }/* namespace CVC4::theory */
 }/* namespace CVC4 */