Quantifiers subdirectories (#1608)

1 files changed, 2460 insertions, 0 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
new file mode 100644
index 000000000..17c4c482d
--- /dev/null
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -0,0 +1,2460 @@
+/*********************                                                        */
+/*! \file ce_guided_pbe.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief utility for processing programming by examples synthesis conjectures
+ **
+ **/
+#include "theory/quantifiers/sygus/sygus_pbe.h"
+
+#include "expr/datatype.h"
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/datatypes/datatypes_rewriter.h"
+#include "util/random.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+void indent( const char * c, int ind ) {
+  if( Trace.isOn(c) ){
+    for( int i=0; i<ind; i++ ){ 
+      Trace(c) << "  "; 
+    }
+  } 
+}
+
+void print_val( const char * c, std::vector< Node >& vals, bool pol = true ){
+  if( Trace.isOn(c) ){
+    for( unsigned i=0; i<vals.size(); i++ ){
+      //Trace(c) << ( pol ? vals[i] : !vals[i] );
+      Trace(c) << ( ( pol ? vals[i].getConst<bool>() : !vals[i].getConst<bool>() ) ? "1" : "0" );
+    }
+  }
+}
+
+std::ostream& operator<<(std::ostream& os, EnumRole r)
+{
+  switch(r){
+    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;
+}
+
+std::ostream& operator<<(std::ostream& os, NodeRole r)
+{
+  switch (r)
+  {
+    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)
+    : d_qe(qe),
+      d_parent(p){
+  d_tds = d_qe->getTermDatabaseSygus();
+  d_true = NodeManager::currentNM()->mkConst(true);
+  d_false = NodeManager::currentNM()->mkConst(false);
+  d_is_pbe = false;
+}
+
+CegConjecturePbe::~CegConjecturePbe() {
+
+}
+
+//--------------------------------- collecting finite input/output domain information
+
+void CegConjecturePbe::collectExamples( Node n, std::map< Node, bool >& visited, bool hasPol, bool pol ) {
+  if( visited.find( n )==visited.end() ){
+    visited[n] = true;
+    Node neval;
+    Node n_output;
+    if( n.getKind()==APPLY_UF && n.getNumChildren()>0 ){
+      neval = n;
+      if( hasPol ){
+        n_output = !pol ? d_true : d_false;
+      }
+    }else if( n.getKind()==EQUAL && hasPol && !pol ){
+      for( unsigned r=0; r<2; r++ ){
+        if( n[r].getKind()==APPLY_UF && n[r].getNumChildren()>0 ){
+          neval = n[r];
+          if( n[1-r].isConst() ){
+            n_output = n[1-r];
+          }
+        }
+      }
+    }
+    if( !neval.isNull() ){
+      if( neval.getKind()==APPLY_UF && neval.getNumChildren()>0 ){
+        // is it an evaluation function?
+        if( d_examples.find( neval[0] )!=d_examples.end() ){
+          std::map< Node, bool >::iterator itx = d_examples_invalid.find( neval[0] );
+          if( itx==d_examples_invalid.end() ){
+            //collect example
+            bool success = true;
+            std::vector< Node > ex;
+            for( unsigned j=1; j<neval.getNumChildren(); j++ ){
+              if( !neval[j].isConst() ){
+                success = false;
+                break;
+              }else{
+                ex.push_back( neval[j] );
+              }
+            }
+            if( success ){
+              d_examples[neval[0]].push_back( ex );
+              d_examples_out[neval[0]].push_back( n_output );
+              d_examples_term[neval[0]].push_back( neval );
+              if( n_output.isNull() ){
+                d_examples_out_invalid[neval[0]] = true;
+              }else{
+                Assert( n_output.isConst() );
+              }
+              //finished processing this node
+              return;
+            }else{
+              d_examples_invalid[neval[0]] = true;
+              d_examples_out_invalid[neval[0]] = true;
+            }
+          }
+        }
+      }
+    }
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      bool newHasPol;
+      bool newPol;
+      QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
+      collectExamples( n[i], visited, newHasPol, newPol );
+    }
+  }
+}
+
+void CegConjecturePbe::initialize(Node n,
+                                  std::vector<Node>& candidates,
+                                  std::vector<Node>& lemmas)
+{
+  Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl;
+  
+  for( unsigned i=0; i<candidates.size(); i++ ){
+    Node v = candidates[i];
+    d_examples[v].clear();
+    d_examples_out[v].clear();
+    d_examples_term[v].clear();
+  }
+  
+  std::map< Node, bool > visited;
+  collectExamples( n, visited, true, true );
+  
+  for( unsigned i=0; i<candidates.size(); i++ ){
+    Node v = candidates[i];
+    Trace("sygus-pbe") << "  examples for " << v << " : ";
+    if( d_examples_invalid.find( v )!=d_examples_invalid.end() ){
+      Trace("sygus-pbe") << "INVALID" << std::endl;
+    }else{
+      Trace("sygus-pbe") << std::endl;
+      for( unsigned j=0; j<d_examples[v].size(); j++ ){
+        Trace("sygus-pbe") << "    ";
+        for( unsigned k=0; k<d_examples[v][j].size(); k++ ){
+          Trace("sygus-pbe") << d_examples[v][j][k] << " ";
+        }
+        if( !d_examples_out[v][j].isNull() ){
+          Trace("sygus-pbe") << " -> " << d_examples_out[v][j];
+        }
+        Trace("sygus-pbe") << std::endl;
+      }
+    }
+  }
+  
+  //register candidates
+  if( options::sygusUnifCondSol() ){
+    if( candidates.size()==1 ){// conditional solutions for multiple function conjectures TODO?
+      // collect a pool of types over which we will enumerate terms 
+      Node c = candidates[0];
+      //the candidate must be input/output examples
+      if( d_examples_out_invalid.find( c )==d_examples_out_invalid.end() ){
+        Assert( d_examples.find( c )!=d_examples.end() );
+        Trace("sygus-unif") << "It is input/output examples..." << std::endl;
+        TypeNode ctn = c.getType();
+        d_cinfo[c].initialize( c );
+        // collect the enumerator types / form the strategy
+        collectEnumeratorTypes(c, ctn, role_equal);
+        // if we have non-trivial strategies, then use pbe
+        if( d_cinfo[c].isNonTrivial() ){
+          // static learning of redundant constructors
+          staticLearnRedundantOps( c, lemmas );
+          d_is_pbe = true;
+        }
+      }
+    }
+  }
+  if( !d_is_pbe ){
+    Trace("sygus-unif") << "Do not do PBE optimizations, register..." << std::endl;
+    for( unsigned i=0; i<candidates.size(); i++ ){
+      d_qe->getTermDatabaseSygus()->registerEnumerator(
+          candidates[i], candidates[i], d_parent);
+    }
+  }
+}
+
+Node CegConjecturePbe::PbeTrie::addPbeExample(TypeNode etn, Node e, Node b,
+                                              CegConjecturePbe* cpbe,
+                                              unsigned index, unsigned ntotal) {
+  if (index == ntotal) {
+    // lazy child holds the leaf data
+    if (d_lazy_child.isNull()) {
+      d_lazy_child = b;
+    }
+    return d_lazy_child;
+  } else {
+    std::vector<Node> ex;
+    if (d_children.empty()) {
+      if (d_lazy_child.isNull()) {
+        d_lazy_child = b;
+        return d_lazy_child;
+      } else {
+        // evaluate the lazy child
+        Assert(cpbe->d_examples.find(e) != cpbe->d_examples.end());
+        Assert(index < cpbe->d_examples[e].size());
+        ex = cpbe->d_examples[e][index];
+        addPbeExampleEval(etn, e, d_lazy_child, ex, cpbe, index, ntotal);
+        Assert(!d_children.empty());
+        d_lazy_child = Node::null();
+      }
+    } else {
+      Assert(cpbe->d_examples.find(e) != cpbe->d_examples.end());
+      Assert(index < cpbe->d_examples[e].size());
+      ex = cpbe->d_examples[e][index];
+    }
+    return addPbeExampleEval(etn, e, b, ex, cpbe, index, ntotal);
+  }
+}
+
+Node CegConjecturePbe::PbeTrie::addPbeExampleEval(TypeNode etn, Node e, Node b,
+                                                  std::vector<Node>& ex,
+                                                  CegConjecturePbe* cpbe,
+                                                  unsigned index,
+                                                  unsigned ntotal) {
+  Node eb = cpbe->d_tds->evaluateBuiltin(etn, b, ex);
+  return d_children[eb].addPbeExample(etn, e, b, cpbe, index + 1, ntotal);
+}
+
+bool CegConjecturePbe::hasExamples(Node e) {
+  if (isPbe()) {
+    e = d_tds->getSynthFunForEnumerator(e);
+    Assert(!e.isNull());
+    std::map<Node, bool>::iterator itx = d_examples_invalid.find(e);
+    if (itx == d_examples_invalid.end()) {
+      return d_examples.find(e) != d_examples.end();
+    }
+  }
+  return false;
+}
+
+unsigned CegConjecturePbe::getNumExamples(Node e) {
+  e = d_tds->getSynthFunForEnumerator(e);
+  Assert(!e.isNull());
+  std::map<Node, std::vector<std::vector<Node> > >::iterator it =
+      d_examples.find(e);
+  if (it != d_examples.end()) {
+    return it->second.size();
+  } else {
+    return 0;
+  }
+}
+
+void CegConjecturePbe::getExample(Node e, unsigned i, std::vector<Node>& ex) {
+  e = d_tds->getSynthFunForEnumerator(e);
+  Assert(!e.isNull());
+  std::map<Node, std::vector<std::vector<Node> > >::iterator it =
+      d_examples.find(e);
+  if (it != d_examples.end()) {
+    Assert(i < it->second.size());
+    ex.insert(ex.end(), it->second[i].begin(), it->second[i].end());
+  } else {
+    Assert(false);
+  }
+}
+
+Node CegConjecturePbe::getExampleOut(Node e, unsigned i) {
+  e = d_tds->getSynthFunForEnumerator(e);
+  Assert(!e.isNull());
+  std::map<Node, std::vector<Node> >::iterator it = d_examples_out.find(e);
+  if (it != d_examples_out.end()) {
+    Assert(i < it->second.size());
+    return it->second[i];
+  } else {
+    Assert(false);
+    return Node::null();
+  }
+}
+
+Node CegConjecturePbe::addSearchVal(TypeNode tn, Node e, Node bvr) {
+  Assert(isPbe());
+  Assert(!e.isNull());
+  e = d_tds->getSynthFunForEnumerator(e);
+  Assert(!e.isNull());
+  std::map<Node, bool>::iterator itx = d_examples_invalid.find(e);
+  if (itx == d_examples_invalid.end()) {
+    unsigned nex = d_examples[e].size();
+    Node ret = d_pbe_trie[e][tn].addPbeExample(tn, e, bvr, this, 0, nex);
+    Assert(ret.getType() == bvr.getType());
+    return ret;
+  }
+  return Node::null();
+}
+
+Node CegConjecturePbe::evaluateBuiltin(TypeNode tn, Node bn, Node e,
+                                       unsigned i) {
+  e = d_tds->getSynthFunForEnumerator(e);
+  Assert(!e.isNull());
+  std::map<Node, bool>::iterator itx = d_examples_invalid.find(e);
+  if (itx == d_examples_invalid.end()) {
+    std::map<Node, std::vector<std::vector<Node> > >::iterator it =
+        d_examples.find(e);
+    if (it != d_examples.end()) {
+      Assert(i < it->second.size());
+      return d_tds->evaluateBuiltin(tn, bn, it->second[i]);
+    }
+  }
+  return Rewriter::rewrite(bn);
+}
+
+// ----------------------------- establishing enumeration types
+
+void CegConjecturePbe::registerEnumerator(
+    Node et, Node c, TypeNode tn, EnumRole enum_role, bool inSearch)
+{
+  if (d_einfo.find(et) == d_einfo.end())
+  {
+    Trace("sygus-unif-debug")
+        << "...register " << et << " for "
+        << ((DatatypeType)tn.toType()).getDatatype().getName();
+    Trace("sygus-unif-debug") << ", role = " << enum_role
+                              << ", in search = " << inSearch << std::endl;
+    d_einfo[et].initialize(c, enum_role);
+    // if we are actually enumerating this (could be a compound node in the
+    // strategy)
+    if (inSearch)
+    {
+      std::map<TypeNode, Node>::iterator itn =
+          d_cinfo[c].d_search_enum.find(tn);
+      if (itn == d_cinfo[c].d_search_enum.end())
+      {
+        // use this for the search
+        d_cinfo[c].d_search_enum[tn] = et;
+        d_cinfo[c].d_esym_list.push_back(et);
+        d_einfo[et].d_enum_slave.push_back(et);
+        // register measured term with database
+        d_qe->getTermDatabaseSygus()->registerEnumerator(et, c, d_parent, true);
+        d_einfo[et].d_active_guard =
+            d_qe->getTermDatabaseSygus()->getActiveGuardForEnumerator(et);
+      }
+      else
+      {
+        Trace("sygus-unif-debug") << "Make " << et << " a slave of "
+                                  << itn->second << std::endl;
+        d_einfo[itn->second].d_enum_slave.push_back(et);
+      }
+    }
+  }
+}
+
+void CegConjecturePbe::collectEnumeratorTypes(Node e,
+                                              TypeNode tn,
+                                              NodeRole nrole)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  if (d_cinfo[e].d_tinfo.find(tn) == d_cinfo[e].d_tinfo.end())
+  {
+    // register type
+    Trace("sygus-unif") << "Register enumerating type : " << tn << std::endl;
+    d_cinfo[e].initializeType( tn );
+  }
+  EnumTypeInfo& eti = d_cinfo[e].d_tinfo[tn];
+  std::map<NodeRole, StrategyNode>::iterator itsn = eti.d_snodes.find(nrole);
+  if (itsn != eti.d_snodes.end())
+  {
+    // already initialized
+    return;
+  }
+  StrategyNode& snode = eti.d_snodes[nrole];
+
+  // get the enumerator for this
+  EnumRole erole = getEnumeratorRoleForNodeRole(nrole);
+
+  Node ee;
+  std::map<EnumRole, Node>::iterator iten = eti.d_enum.find(erole);
+  if (iten == eti.d_enum.end())
+  {
+    ee = nm->mkSkolem("ee", tn);
+    eti.d_enum[erole] = ee;
+    Trace("sygus-unif-debug")
+        << "...enumerator " << ee << " for "
+        << ((DatatypeType)tn.toType()).getDatatype().getName()
+        << ", role = " << erole << std::endl;
+  }
+  else
+  {
+    ee = iten->second;
+  }
+
+  // roles that we do not recurse on
+  if (nrole == role_ite_condition)
+  {
+    Trace("sygus-unif-debug") << "...this register (non-io)" << std::endl;
+    registerEnumerator(ee, e, tn, erole, true);
+    return;
+  }
+
+  // look at information on how we will construct solutions for this type
+  Assert(tn.isDatatype());
+  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  Assert(dt.isSygus());
+
+  std::map<Node, std::vector<StrategyType> > cop_to_strat;
+  std::map<Node, unsigned> cop_to_cindex;
+  std::map<Node, std::map<unsigned, Node> > cop_to_child_templ;
+  std::map<Node, std::map<unsigned, Node> > cop_to_child_templ_arg;
+  std::map<Node, std::vector<unsigned> > cop_to_carg_list;
+  std::map<Node, std::vector<TypeNode> > cop_to_child_types;
+  std::map<Node, std::vector<Node> > cop_to_sks;
+
+  // whether we will enumerate the current type
+  bool search_this = false;
+  for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
+  {
+    Node cop = Node::fromExpr(dt[j].getConstructor());
+    Node op = Node::fromExpr(dt[j].getSygusOp());
+    Trace("sygus-unif-debug") << "--- Infer strategy from " << cop
+                              << " with sygus op " << op << "..." << std::endl;
+
+    // expand the evaluation to see if this constuctor induces a strategy
+    std::vector<Node> utchildren;
+    utchildren.push_back(cop);
+    std::vector<Node> sks;
+    std::vector<TypeNode> sktns;
+    for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
+    {
+      Type t = dt[j][k].getRangeType();
+      TypeNode ttn = TypeNode::fromType(t);
+      Node kv = nm->mkSkolem("ut", ttn);
+      sks.push_back(kv);
+      cop_to_sks[cop].push_back(kv);
+      sktns.push_back(ttn);
+      utchildren.push_back(kv);
+    }
+    Node ut = nm->mkNode(APPLY_CONSTRUCTOR, utchildren);
+    std::vector<Node> echildren;
+    echildren.push_back(Node::fromExpr(dt.getSygusEvaluationFunc()));
+    echildren.push_back(ut);
+    Node sbvl = Node::fromExpr(dt.getSygusVarList());
+    for (const Node& sbv : sbvl)
+    {
+      echildren.push_back(sbv);
+    }
+    Node eut = nm->mkNode(APPLY_UF, echildren);
+    Trace("sygus-unif-debug2") << "  Test evaluation of " << eut << "..."
+                               << std::endl;
+    eut = d_qe->getTermDatabaseSygus()->unfold(eut);
+    Trace("sygus-unif-debug2") << "  ...got " << eut;
+    Trace("sygus-unif-debug2") << ", type : " << eut.getType() << std::endl;
+
+    // candidate strategy
+    if (eut.getKind() == ITE)
+    {
+      cop_to_strat[cop].push_back(strat_ITE);
+    }
+    else if (eut.getKind() == STRING_CONCAT)
+    {
+      if (nrole != role_string_suffix)
+      {
+        cop_to_strat[cop].push_back(strat_CONCAT_PREFIX);
+      }
+      if (nrole != role_string_prefix)
+      {
+        cop_to_strat[cop].push_back(strat_CONCAT_SUFFIX);
+      }
+    }
+    else if (dt[j].isSygusIdFunc())
+    {
+      cop_to_strat[cop].push_back(strat_ID);
+    }
+
+    // the kinds for which there is a strategy
+    if (cop_to_strat.find(cop) != cop_to_strat.end())
+    {
+      // infer an injection from the arguments of the datatype
+      std::map<unsigned, unsigned> templ_injection;
+      std::vector<Node> vs;
+      std::vector<Node> ss;
+      std::map<Node, unsigned> templ_var_index;
+      for (unsigned k = 0, sksize = sks.size(); k < sksize; k++)
+      {
+        Assert(sks[k].getType().isDatatype());
+        const Datatype& cdt =
+            static_cast<DatatypeType>(sks[k].getType().toType()).getDatatype();
+        echildren[0] = Node::fromExpr(cdt.getSygusEvaluationFunc());
+        echildren[1] = sks[k];
+        Trace("sygus-unif-debug2") << "...set eval dt to " << sks[k]
+                                   << std::endl;
+        Node esk = nm->mkNode(APPLY_UF, echildren);
+        vs.push_back(esk);
+        Node tvar = nm->mkSkolem("templ", esk.getType());
+        templ_var_index[tvar] = k;
+        Trace("sygus-unif-debug2") << "* template inference : looking for "
+                                   << tvar << " for arg " << k << std::endl;
+        ss.push_back(tvar);
+        Trace("sygus-unif-debug2") << "* substitute : " << esk << " -> " << tvar
+                                   << std::endl;
+      }
+      eut = eut.substitute(vs.begin(), vs.end(), ss.begin(), ss.end());
+      Trace("sygus-unif-debug2") << "Constructor " << j << ", base term is "
+                                 << eut << std::endl;
+      std::map<unsigned, Node> test_args;
+      if (dt[j].isSygusIdFunc())
+      {
+        test_args[0] = eut;
+      }
+      else
+      {
+        for (unsigned k = 0, size = eut.getNumChildren(); k < size; k++)
+        {
+          test_args[k] = eut[k];
+        }
+      }
+
+      // TODO : prefix grouping prefix/suffix
+      bool isAssoc = TermUtil::isAssoc(eut.getKind());
+      Trace("sygus-unif-debug2") << eut.getKind() << " isAssoc = " << isAssoc
+                                 << std::endl;
+      std::map<unsigned, std::vector<unsigned> > assoc_combine;
+      std::vector<unsigned> assoc_waiting;
+      int assoc_last_valid_index = -1;
+      for (std::pair<const unsigned, Node>& ta : test_args)
+      {
+        unsigned k = ta.first;
+        Node eut_c = ta.second;
+        // success if we can find a injection from args to sygus args
+        if (!inferTemplate(k, eut_c, templ_var_index, templ_injection))
+        {
+          Trace("sygus-unif-debug")
+              << "...fail: could not find injection (range)." << std::endl;
+          cop_to_strat.erase(cop);
+          break;
+        }
+        std::map<unsigned, unsigned>::iterator itti = templ_injection.find(k);
+        if (itti != templ_injection.end())
+        {
+          // if associative, combine arguments if it is the same variable
+          if (isAssoc && assoc_last_valid_index >= 0
+              && itti->second == templ_injection[assoc_last_valid_index])
+          {
+            templ_injection.erase(k);
+            assoc_combine[assoc_last_valid_index].push_back(k);
+          }
+          else
+          {
+            assoc_last_valid_index = (int)k;
+            if (!assoc_waiting.empty())
+            {
+              assoc_combine[k].insert(assoc_combine[k].end(),
+                                      assoc_waiting.begin(),
+                                      assoc_waiting.end());
+              assoc_waiting.clear();
+            }
+            assoc_combine[k].push_back(k);
+          }
+        }
+        else
+        {
+          // a ground argument
+          if (!isAssoc)
+          {
+            Trace("sygus-unif-debug")
+                << "...fail: could not find injection (functional)."
+                << std::endl;
+            cop_to_strat.erase(cop);
+            break;
+          }
+          else
+          {
+            if (assoc_last_valid_index >= 0)
+            {
+              assoc_combine[assoc_last_valid_index].push_back(k);
+            }
+            else
+            {
+              assoc_waiting.push_back(k);
+            }
+          }
+        }
+      }
+      if (cop_to_strat.find(cop) != cop_to_strat.end())
+      {
+        // construct the templates
+        if (!assoc_waiting.empty())
+        {
+          // could not find a way to fit some arguments into injection
+          cop_to_strat.erase(cop);
+        }
+        else
+        {
+          for (std::pair<const unsigned, Node>& ta : test_args)
+          {
+            unsigned k = ta.first;
+            Trace("sygus-unif-debug2") << "- processing argument " << k << "..."
+                                       << std::endl;
+            if (templ_injection.find(k) != templ_injection.end())
+            {
+              unsigned sk_index = templ_injection[k];
+              if (std::find(cop_to_carg_list[cop].begin(),
+                            cop_to_carg_list[cop].end(),
+                            sk_index)
+                  == cop_to_carg_list[cop].end())
+              {
+                cop_to_carg_list[cop].push_back(sk_index);
+              }else{
+                Trace("sygus-unif-debug") << "...fail: duplicate argument used"
+                                          << std::endl;
+                cop_to_strat.erase(cop);
+                break;
+              }
+              // also store the template information, if necessary
+              Node teut;
+              if (isAssoc)
+              {
+                std::vector<unsigned>& ac = assoc_combine[k];
+                Assert(!ac.empty());
+                std::vector<Node> children;
+                for (unsigned ack = 0, size_ac = ac.size(); ack < size_ac;
+                     ack++)
+                {
+                  children.push_back(eut[ac[ack]]);
+                }
+                teut = children.size() == 1
+                           ? children[0]
+                           : nm->mkNode(eut.getKind(), children);
+                teut = Rewriter::rewrite(teut);
+              }
+              else
+              {
+                teut = ta.second;
+              }
+
+              if (!teut.isVar())
+              {
+                cop_to_child_templ[cop][k] = teut;
+                cop_to_child_templ_arg[cop][k] = ss[sk_index];
+                Trace("sygus-unif-debug")
+                    << "  Arg " << k << " (template : " << teut << " arg "
+                    << ss[sk_index] << "), index " << sk_index << std::endl;
+              }
+              else
+              {
+                Trace("sygus-unif-debug") << "  Arg " << k << ", index "
+                                          << sk_index << std::endl;
+                Assert(teut == ss[sk_index]);
+              }
+            }
+            else
+            {
+              Assert(isAssoc);
+            }
+          }
+        }
+      }
+    }
+    if (cop_to_strat.find(cop) == cop_to_strat.end())
+    {
+      Trace("sygus-unif") << "...constructor " << cop
+                          << " does not correspond to a strategy." << std::endl;
+      search_this = true;
+    }
+    else
+    {
+      Trace("sygus-unif") << "-> constructor " << cop
+                          << " matches strategy for " << eut.getKind() << "..."
+                          << std::endl;
+      // collect children types
+      for (unsigned k = 0, size = cop_to_carg_list[cop].size(); k < size; k++)
+      {
+        TypeNode tn = sktns[cop_to_carg_list[cop][k]];
+        Trace("sygus-unif-debug")
+            << "   Child type " << k << " : "
+            << static_cast<DatatypeType>(tn.toType()).getDatatype().getName()
+            << std::endl;
+        cop_to_child_types[cop].push_back(tn);
+      }
+    }
+  }
+
+  // check whether we should also enumerate the current type
+  Trace("sygus-unif-debug2") << "  register this enumerator..." << std::endl;
+  registerEnumerator(ee, e, tn, erole, search_this);
+
+  if (cop_to_strat.empty())
+  {
+    Trace("sygus-unif") << "...consider " << dt.getName() << " a basic type"
+                        << std::endl;
+  }
+  else
+  {
+    for (std::pair<const Node, std::vector<StrategyType> >& cstr : cop_to_strat)
+    {
+      Node cop = cstr.first;
+      Trace("sygus-unif-debug") << "Constructor " << cop << " has "
+                                << cstr.second.size() << " strategies..."
+                                << std::endl;
+      for (unsigned s = 0, ssize = cstr.second.size(); s < ssize; s++)
+      {
+        EnumTypeInfoStrat* cons_strat = new EnumTypeInfoStrat;
+        StrategyType strat = cstr.second[s];
+
+        cons_strat->d_this = strat;
+        cons_strat->d_cons = cop;
+        Trace("sygus-unif-debug") << "Process strategy #" << s
+                                  << " for operator : " << cop << " : " << strat
+                                  << std::endl;
+        Assert(cop_to_child_types.find(cop) != cop_to_child_types.end());
+        std::vector<TypeNode>& childTypes = cop_to_child_types[cop];
+        Assert(cop_to_carg_list.find(cop) != cop_to_carg_list.end());
+        std::vector<unsigned>& cargList = cop_to_carg_list[cop];
+
+        std::vector<Node> sol_templ_children;
+        sol_templ_children.resize(cop_to_sks[cop].size());
+
+        for (unsigned j = 0, csize = childTypes.size(); j < csize; j++)
+        {
+          // calculate if we should allocate a new enumerator : should be true
+          // if we have a new role
+          NodeRole nrole_c = nrole;
+          if (strat == strat_ITE)
+          {
+            if (j == 0)
+            {
+              nrole_c = role_ite_condition;
+            }
+          }
+          else if (strat == strat_CONCAT_PREFIX)
+          {
+            if ((j + 1) < childTypes.size())
+            {
+              nrole_c = role_string_prefix;
+            }
+          }
+          else if (strat == strat_CONCAT_SUFFIX)
+          {
+            if (j > 0)
+            {
+              nrole_c = role_string_suffix;
+            }
+          }
+          // in all other cases, role is same as parent
+
+          // register the child type
+          TypeNode ct = childTypes[j];
+          Node csk = cop_to_sks[cop][cargList[j]];
+          cons_strat->d_sol_templ_args.push_back(csk);
+          sol_templ_children[cargList[j]] = csk;
+
+          EnumRole erole_c = getEnumeratorRoleForNodeRole(nrole_c);
+          // make the enumerator
+          Node et;
+          if (cop_to_child_templ[cop].find(j) != cop_to_child_templ[cop].end())
+          {
+            // it is templated, allocate a fresh variable
+            et = nm->mkSkolem("et", ct);
+            Trace("sygus-unif-debug")
+                << "...enumerate " << et << " of type "
+                << ((DatatypeType)ct.toType()).getDatatype().getName();
+            Trace("sygus-unif-debug")
+                << " for arg " << j << " of "
+                << ((DatatypeType)tn.toType()).getDatatype().getName()
+                << std::endl;
+            registerEnumerator(et, e, ct, erole_c, true);
+            d_einfo[et].d_template = cop_to_child_templ[cop][j];
+            d_einfo[et].d_template_arg = cop_to_child_templ_arg[cop][j];
+            Assert(!d_einfo[et].d_template.isNull());
+            Assert(!d_einfo[et].d_template_arg.isNull());
+          }
+          else
+          {
+            Trace("sygus-unif-debug")
+                << "...child type enumerate "
+                << ((DatatypeType)ct.toType()).getDatatype().getName()
+                << ", node role = " << nrole_c << std::endl;
+            collectEnumeratorTypes(e, ct, nrole_c);
+            // otherwise use the previous
+            Assert(d_cinfo[e].d_tinfo[ct].d_enum.find(erole_c)
+                   != d_cinfo[e].d_tinfo[ct].d_enum.end());
+            et = d_cinfo[e].d_tinfo[ct].d_enum[erole_c];
+          }
+          Trace("sygus-unif-debug") << "Register child enumerator " << et
+                                    << ", arg " << j << " of " << cop
+                                    << ", role = " << erole_c << std::endl;
+          Assert(!et.isNull());
+          cons_strat->d_cenum.push_back(std::pair<Node, NodeRole>(et, nrole_c));
+        }
+        // children that are unused in the strategy can be arbitrary
+        for (unsigned j = 0, stsize = sol_templ_children.size(); j < stsize;
+             j++)
+        {
+          if (sol_templ_children[j].isNull())
+          {
+            sol_templ_children[j] = cop_to_sks[cop][j].getType().mkGroundTerm();
+          }
+        }
+        sol_templ_children.insert(sol_templ_children.begin(), cop);
+        cons_strat->d_sol_templ =
+            nm->mkNode(APPLY_CONSTRUCTOR, sol_templ_children);
+        if (strat == strat_CONCAT_SUFFIX)
+        {
+          std::reverse(cons_strat->d_cenum.begin(), cons_strat->d_cenum.end());
+          std::reverse(cons_strat->d_sol_templ_args.begin(),
+                       cons_strat->d_sol_templ_args.end());
+        }
+        if (Trace.isOn("sygus-unif"))
+        {
+          Trace("sygus-unif") << "Initialized strategy " << strat;
+          Trace("sygus-unif") << " for " << ((DatatypeType)tn.toType()).getDatatype().getName() << ", operator " << cop;
+          Trace("sygus-unif") << ", #children = " << cons_strat->d_cenum.size()
+                              << ", solution template = (lambda ( ";
+          for (const Node& targ : cons_strat->d_sol_templ_args)
+          {
+            Trace("sygus-unif") << targ << " ";
+          }
+          Trace("sygus-unif") << ") " << cons_strat->d_sol_templ << ")";
+          Trace("sygus-unif") << std::endl;
+        }
+        // make the strategy
+        snode.d_strats.push_back(cons_strat);
+      }
+    }
+  }
+}
+
+bool CegConjecturePbe::inferTemplate( unsigned k, Node n, std::map< Node, unsigned >& templ_var_index, std::map< unsigned, unsigned >& templ_injection ){
+  if( n.getNumChildren()==0 ){
+    std::map< Node, unsigned >::iterator itt = templ_var_index.find( n );
+    if( itt!=templ_var_index.end() ){
+      unsigned kk = itt->second;
+      std::map< unsigned, unsigned >::iterator itti = templ_injection.find( k );
+      if( itti==templ_injection.end() ){
+        Trace("sygus-unif-debug") << "...set template injection " << k <<  " -> " << kk << std::endl;
+        templ_injection[k] = kk;
+      }else if( itti->second!=kk ){
+        // two distinct variables in this term, we fail
+        return false;
+      }
+    }
+    return true;
+  }else{
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      if( !inferTemplate( k, n[i], templ_var_index, templ_injection ) ){
+        return false;
+      }
+    }
+  }
+  return true;
+}
+
+void CegConjecturePbe::staticLearnRedundantOps( Node c, std::vector< Node >& lemmas ) {
+  for( unsigned i=0; i<d_cinfo[c].d_esym_list.size(); i++ ){
+    Node e = d_cinfo[c].d_esym_list[i];
+    std::map< Node, EnumInfo >::iterator itn = d_einfo.find( e );
+    Assert( itn!=d_einfo.end() );
+    // see if there is anything we can eliminate
+    Trace("sygus-unif") << "* Search enumerator #" << i << " : type " << ((DatatypeType)e.getType().toType()).getDatatype().getName() << " : ";
+    Trace("sygus-unif") << e << " has " << itn->second.d_enum_slave.size() << " slaves:" << std::endl;
+    for( unsigned j=0; j<itn->second.d_enum_slave.size(); j++ ){
+      Node es = itn->second.d_enum_slave[j];
+      std::map< Node, EnumInfo >::iterator itns = d_einfo.find( es );
+      Assert( itns!=d_einfo.end() );
+      Trace("sygus-unif") << "  " << es << ", role = " << itns->second.getRole()
+                          << std::endl;
+    }
+  }
+  Trace("sygus-unif") << std::endl;
+  Trace("sygus-unif") << "Strategy for candidate " << c << " is : " << std::endl;
+  std::map<Node, std::map<NodeRole, bool> > visited;
+  std::map<Node, std::map<unsigned, bool> > needs_cons;
+  staticLearnRedundantOps(c,
+                          d_cinfo[c].getRootEnumerator(),
+                          role_equal,
+                          visited,
+                          needs_cons,
+                          0,
+                          false);
+  // now, check the needs_cons map
+  for (std::pair<const Node, std::map<unsigned, bool> >& nce : needs_cons)
+  {
+    Node em = nce.first;
+    const Datatype& dt =
+        static_cast<DatatypeType>(em.getType().toType()).getDatatype();
+    for (std::pair<const unsigned, bool>& nc : nce.second)
+    {
+      Assert(nc.first < dt.getNumConstructors());
+      if (!nc.second)
+      {
+        Node tst =
+            datatypes::DatatypesRewriter::mkTester(em, nc.first, dt).negate();
+        if (std::find(lemmas.begin(), lemmas.end(), tst) == lemmas.end())
+        {
+          Trace("sygus-unif") << "...can exclude based on  : " << tst
+                              << std::endl;
+          lemmas.push_back(tst);
+        }
+      }
+    }
+  }
+}
+
+void CegConjecturePbe::staticLearnRedundantOps(
+    Node c,
+    Node e,
+    NodeRole nrole,
+    std::map<Node, std::map<NodeRole, bool> >& visited,
+    std::map<Node, std::map<unsigned, bool> >& needs_cons,
+    int ind,
+    bool isCond)
+{
+  std::map< Node, EnumInfo >::iterator itn = d_einfo.find( e );
+  Assert( itn!=d_einfo.end() );
+
+  if (visited[e].find(nrole) == visited[e].end()
+      || (isCond && !itn->second.isConditional()))
+  {
+    visited[e][nrole] = true;
+    // if conditional
+    if (isCond)
+    {
+      itn->second.setConditional();
+    }
+    indent("sygus-unif", ind);
+    Trace("sygus-unif") << e << " :: node role : " << nrole;
+    Trace("sygus-unif")
+        << ", type : "
+        << ((DatatypeType)e.getType().toType()).getDatatype().getName();
+    if (isCond)
+    {
+      Trace("sygus-unif") << ", conditional";
+    }
+    Trace("sygus-unif") << ", enum role : " << itn->second.getRole();
+
+    if( itn->second.isTemplated() ){
+      Trace("sygus-unif") << ", templated : (lambda "
+                          << itn->second.d_template_arg << " "
+                          << itn->second.d_template << ")" << std::endl;
+    }else{
+      Trace("sygus-unif") << std::endl;
+      TypeNode etn = e.getType();
+
+      // enumerator type info
+      std::map< TypeNode, EnumTypeInfo >::iterator itt = d_cinfo[c].d_tinfo.find( etn );
+      Assert( itt!=d_cinfo[c].d_tinfo.end() );
+      EnumTypeInfo& tinfo = itt->second;
+
+      // strategy info
+      std::map<NodeRole, StrategyNode>::iterator itsn =
+          tinfo.d_snodes.find(nrole);
+      Assert(itsn != tinfo.d_snodes.end());
+      StrategyNode& snode = itsn->second;
+
+      if (snode.d_strats.empty())
+      {
+        return;
+      }
+      std::map<unsigned, bool> needs_cons_curr;
+      // various strategies
+      for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++)
+      {
+        EnumTypeInfoStrat* etis = snode.d_strats[j];
+        StrategyType strat = etis->d_this;
+        bool newIsCond = isCond || strat == strat_ITE;
+        indent("sygus-unif", ind + 1);
+        Trace("sygus-unif") << "Strategy : " << strat
+                            << ", from cons : " << etis->d_cons << std::endl;
+        int cindex = Datatype::indexOf(etis->d_cons.toExpr());
+        Assert(cindex != -1);
+        needs_cons_curr[static_cast<unsigned>(cindex)] = false;
+        for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
+        {
+          // recurse
+          staticLearnRedundantOps(c,
+                                  cec.first,
+                                  cec.second,
+                                  visited,
+                                  needs_cons,
+                                  ind + 2,
+                                  newIsCond);
+        }
+      }
+      // get the master enumerator for the type of this enumerator
+      std::map<TypeNode, Node>::iterator itse =
+          d_cinfo[c].d_search_enum.find(etn);
+      if (itse == d_cinfo[c].d_search_enum.end())
+      {
+        return;
+      }
+      Node em = itse->second;
+      Assert(!em.isNull());
+      // get the current datatype
+      const Datatype& dt =
+          static_cast<DatatypeType>(etn.toType()).getDatatype();
+      // all constructors that are not a part of a strategy are needed
+      for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++)
+      {
+        if (needs_cons_curr.find(j) == needs_cons_curr.end())
+        {
+          needs_cons_curr[j] = true;
+        }
+      }
+      // update the constructors that the master enumerator needs
+      if (needs_cons.find(em) == needs_cons.end())
+      {
+        needs_cons[em] = needs_cons_curr;
+      }
+      else
+      {
+        for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++)
+        {
+          needs_cons[em][j] = needs_cons[em][j] || needs_cons_curr[j];
+        }
+      }
+    }
+  }else{
+    indent("sygus-unif", ind);
+    Trace("sygus-unif") << e << " :: node role : " << nrole << std::endl;
+  }
+}
+
+// ------------------------------------------- solution construction from enumeration
+
+void CegConjecturePbe::getCandidateList( std::vector< Node >& candidates, std::vector< Node >& clist ) {
+  Valuation& valuation = d_qe->getValuation();
+  for( unsigned i=0; i<candidates.size(); i++ ){
+    Node v = candidates[i];
+    std::map< Node, CandidateInfo >::iterator it = d_cinfo.find( v );
+    if( it!=d_cinfo.end() ){
+      for( unsigned j=0; j<it->second.d_esym_list.size(); j++ ){
+        Node e = it->second.d_esym_list[j];
+        std::map< Node, EnumInfo >::iterator it = d_einfo.find( e );
+        Assert( it != d_einfo.end() );
+        Node gstatus = valuation.getSatValue(it->second.d_active_guard);
+        if (!gstatus.isNull() && gstatus.getConst<bool>())
+        {
+          clist.push_back( e );
+        }
+      }
+    }
+  }
+}
+
+bool CegConjecturePbe::constructCandidates( std::vector< Node >& enums, std::vector< Node >& enum_values, 
+                                            std::vector< Node >& candidates, std::vector< Node >& candidate_values, 
+                                            std::vector< Node >& lems ) {
+  Assert( enums.size()==enum_values.size() );
+  if( !enums.empty() ){
+    unsigned min_term_size = 0;
+    std::vector< unsigned > enum_consider;
+    Trace("sygus-pbe-enum") << "Register new enumerated values : " << std::endl;
+    for( unsigned i=0; i<enums.size(); i++ ){
+      Trace("sygus-pbe-enum") << "  " << enums[i] << " -> " << enum_values[i] << std::endl;
+      unsigned sz = d_tds->getSygusTermSize( enum_values[i] );
+      if( i==0 || sz<min_term_size ){
+        enum_consider.clear();
+        min_term_size = sz;
+        enum_consider.push_back( i );
+      }else if( sz==min_term_size ){
+        enum_consider.push_back( i );
+      }
+    }
+    // only consider the enumerators that are at minimum size (for fairness)
+    Trace("sygus-pbe-enum") << "...register " << enum_consider.size() << " / " << enums.size() << std::endl;
+    for( unsigned i=0; i<enum_consider.size(); i++ ){
+      unsigned j = enum_consider[i];
+      addEnumeratedValue( enums[j], enum_values[j], lems );
+    }
+  }
+  for( unsigned i=0; i<candidates.size(); i++ ){
+    Node c = candidates[i];
+    //build decision tree for candidate
+    Node vc = constructSolution( c );
+    if( vc.isNull() ){     
+      return false;
+    }else{
+      candidate_values.push_back( vc );
+    }
+  }
+  return true;
+}
+
+void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& lems ) {
+  std::map< Node, EnumInfo >::iterator it = d_einfo.find( x );
+  Assert( it != d_einfo.end() );
+  Node gstatus = d_qe->getValuation().getSatValue(it->second.d_active_guard);
+  if (gstatus.isNull() || !gstatus.getConst<bool>())
+  {
+    Trace("sygus-pbe-enum-debug") << "  ...guard is inactive." << std::endl;
+    return;
+  }
+  Assert(
+      std::find(it->second.d_enum_vals.begin(), it->second.d_enum_vals.end(), v)
+      == it->second.d_enum_vals.end());
+  Node c = it->second.d_parent_candidate;
+  // The explanation for why the current value should be excluded in future
+  // iterations.
+  Node exp_exc;
+  if (d_examples_out_invalid.find(c) == d_examples_out_invalid.end())
+  {
+    std::map<Node, CandidateInfo>::iterator itc = d_cinfo.find(c);
+    Assert(itc != d_cinfo.end());
+    TypeNode xtn = x.getType();
+    Node bv = d_tds->sygusToBuiltin(v, xtn);
+    std::map<Node, std::vector<std::vector<Node> > >::iterator itx =
+        d_examples.find(c);
+    std::map<Node, std::vector<Node> >::iterator itxo = d_examples_out.find(c);
+    Assert(itx != d_examples.end());
+    Assert(itxo != d_examples_out.end());
+    Assert(itx->second.size() == itxo->second.size());
+    std::vector<Node> base_results;
+    // compte the results
+    for (unsigned j = 0, size = itx->second.size(); j < size; j++)
+    {
+      Node res = d_tds->evaluateBuiltin(xtn, bv, itx->second[j]);
+      Trace("sygus-pbe-enum-debug")
+          << "...got res = " << res << " from " << bv << std::endl;
+      base_results.push_back(res);
+    }
+    // is it excluded for domain-specific reason?
+    std::vector<Node> exp_exc_vec;
+    if (getExplanationForEnumeratorExclude(
+            c, x, v, base_results, it->second, exp_exc_vec))
+    {
+      Assert(!exp_exc_vec.empty());
+      exp_exc = exp_exc_vec.size() == 1
+                    ? exp_exc_vec[0]
+                    : NodeManager::currentNM()->mkNode(AND, exp_exc_vec);
+      Trace("sygus-pbe-enum")
+          << "  ...fail : term is excluded (domain-specific)" << std::endl;
+    }
+    else
+    {
+      // notify all slaves
+      Assert( !it->second.d_enum_slave.empty() );
+      //explanation for why this value should be excluded
+      for( unsigned s=0; s<it->second.d_enum_slave.size(); s++ ){
+        Node xs = it->second.d_enum_slave[s];
+        std::map< Node, EnumInfo >::iterator itv = d_einfo.find( xs );
+        Assert( itv!=d_einfo.end() );
+        Trace("sygus-pbe-enum") << "Process " << xs << " from " << s << std::endl;
+        //bool prevIsCover = false;
+        if (itv->second.getRole() == enum_io)
+        {
+          Trace("sygus-pbe-enum") << "   IO-Eval of ";
+          //prevIsCover = itv->second.isFeasible();
+        }else{
+          Trace("sygus-pbe-enum") << "Evaluation of ";
+        }
+        Trace("sygus-pbe-enum")  << xs <<  " : ";
+        //evaluate all input/output examples
+        std::vector< Node > results;
+        Node templ = itv->second.d_template;
+        TNode templ_var = itv->second.d_template_arg;
+        std::map< Node, bool > cond_vals;
+        for (unsigned j = 0, size = base_results.size(); j < size; j++)
+        {
+          Node res = base_results[j];
+          Assert( res.isConst() );
+          if( !templ.isNull() ){
+            TNode tres = res;
+            res = templ.substitute( templ_var, res );
+            res = Rewriter::rewrite( res );
+            Assert( res.isConst() );
+          }
+          Node resb;
+          if (itv->second.getRole() == enum_io)
+          {
+            Node out = itxo->second[j];
+            Assert( out.isConst() );
+            resb = res==out ? d_true : d_false;
+          }else{
+            resb = res;
+          }
+          cond_vals[resb] = true;
+          results.push_back( resb );
+          if( Trace.isOn("sygus-pbe-enum") ){
+            if( resb.getType().isBoolean() ){
+              Trace("sygus-pbe-enum") << ( resb==d_true ? "1" : "0" );
+            }else{
+              Trace("sygus-pbe-enum") << "?";
+            }
+          }
+        }
+        bool keep = false;
+        if (itv->second.getRole() == enum_io)
+        {
+          // latter is the degenerate case of no examples
+          if (cond_vals.find(d_true) != cond_vals.end() || cond_vals.empty())
+          {
+            //check subsumbed/subsuming
+            std::vector< Node > subsume;
+            if( cond_vals.find( d_false )==cond_vals.end() ){
+              // it is the entire solution, we are done
+              Trace("sygus-pbe-enum") << "  ...success, full solution added to PBE pool : " << d_tds->sygusToBuiltin( v ) << std::endl;
+              if( !itv->second.isSolved() ){
+                itv->second.setSolved( v );
+                // it subsumes everything
+                itv->second.d_term_trie.clear();
+                itv->second.d_term_trie.addTerm( this, v, results, true, subsume );
+              }
+              keep = true;
+            }else{
+              Node val = itv->second.d_term_trie.addTerm( this, v, results, true, subsume );
+              if( val==v ){
+                Trace("sygus-pbe-enum") << "  ...success"; 
+                if( !subsume.empty() ){
+                  itv->second.d_enum_subsume.insert( itv->second.d_enum_subsume.end(), subsume.begin(), subsume.end() );
+                  Trace("sygus-pbe-enum") << " and subsumed " << subsume.size() << " terms";
+                }
+                Trace("sygus-pbe-enum") << "!   add to PBE pool : " << d_tds->sygusToBuiltin( v ) << std::endl;
+                keep = true;
+              }else{
+                Assert( subsume.empty() );
+                Trace("sygus-pbe-enum") << "  ...fail : subsumed" << std::endl;
+              }
+            }
+          }else{
+            Trace("sygus-pbe-enum") << "  ...fail : it does not satisfy examples." << std::endl;
+          }
+        }else{
+          // must be unique up to examples
+          Node val = itv->second.d_term_trie.addCond(this, v, results, true);
+          if (val == v)
+          {
+            Trace("sygus-pbe-enum") << "  ...success!   add to PBE pool : "
+                                    << d_tds->sygusToBuiltin(v) << std::endl;
+            keep = true;
+          }else{
+            Trace("sygus-pbe-enum")
+                << "  ...fail : term is not unique" << std::endl;
+          }
+          itc->second.d_cond_count++;
+        }
+        if( keep ){
+          // notify the parent to retry the build of PBE
+          itc->second.d_check_sol = true;
+          itv->second.addEnumValue( this, v, results );
+        }
+      }
+    }
+  }else{
+    Trace("sygus-pbe-enum-debug")
+        << "  ...examples do not have output." << std::endl;
+  }
+  // exclude this value on subsequent iterations
+  Node g = it->second.d_active_guard;
+  if (exp_exc.isNull())
+  {
+    // if we did not already explain why this should be excluded, use default
+    exp_exc = d_tds->getExplain()->getExplanationForConstantEquality(x, v);
+  }
+  Node exlem =
+      NodeManager::currentNM()->mkNode(OR, g.negate(), exp_exc.negate());
+  Trace("sygus-pbe-enum-lemma")
+      << "CegConjecturePbe : enumeration exclude lemma : " << exlem
+      << std::endl;
+  lems.push_back(exlem);
+}
+
+bool CegConjecturePbe::useStrContainsEnumeratorExclude(Node x, EnumInfo& ei)
+{
+  TypeNode xbt = d_tds->sygusToBuiltinType(x.getType());
+  if (xbt.isString())
+  {
+    std::map<Node, bool>::iterator itx = d_use_str_contains_eexc.find(x);
+    if (itx != d_use_str_contains_eexc.end())
+    {
+      return itx->second;
+    }
+    Trace("sygus-pbe-enum-debug")
+        << "Is " << x << " is str.contains exclusion?" << std::endl;
+    d_use_str_contains_eexc[x] = true;
+    for (const Node& sn : ei.d_enum_slave)
+    {
+      std::map<Node, EnumInfo>::iterator itv = d_einfo.find(sn);
+      EnumRole er = itv->second.getRole();
+      if (er != enum_io && er != enum_concat_term)
+      {
+        Trace("sygus-pbe-enum-debug") << "  incompatible slave : " << sn
+                                      << ", role = " << er << std::endl;
+        d_use_str_contains_eexc[x] = false;
+        return false;
+      }
+      if (itv->second.isConditional())
+      {
+        Trace("sygus-pbe-enum-debug")
+            << "  conditional slave : " << sn << std::endl;
+        d_use_str_contains_eexc[x] = false;
+        return false;
+      }
+    }
+    Trace("sygus-pbe-enum-debug")
+        << "...can use str.contains exclusion." << std::endl;
+    return d_use_str_contains_eexc[x];
+  }
+  return false;
+}
+
+bool CegConjecturePbe::getExplanationForEnumeratorExclude(
+    Node c,
+    Node x,
+    Node v,
+    std::vector<Node>& results,
+    EnumInfo& ei,
+    std::vector<Node>& exp)
+{
+  if (useStrContainsEnumeratorExclude(x, ei))
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    // This check whether the example evaluates to something that is larger than
+    // the output for some input/output pair. If so, then this term is never
+    // useful. We generalize its explanation below.
+
+    if (Trace.isOn("sygus-pbe-cterm-debug"))
+    {
+      Trace("sygus-pbe-enum") << std::endl;
+    }
+    // check if all examples had longer length that the output
+    std::map<Node, std::vector<Node> >::iterator itxo = d_examples_out.find(c);
+    Assert(itxo != d_examples_out.end());
+    Assert(itxo->second.size() == results.size());
+    Trace("sygus-pbe-cterm-debug")
+        << "Check enumerator exclusion for " << x << " -> "
+        << d_tds->sygusToBuiltin(v) << " based on str.contains." << std::endl;
+    std::vector<unsigned> cmp_indices;
+    for (unsigned i = 0, size = results.size(); i < size; i++)
+    {
+      Assert(results[i].isConst());
+      Assert(itxo->second[i].isConst());
+      Trace("sygus-pbe-cterm-debug")
+          << "  " << results[i] << " <> " << itxo->second[i];
+      Node cont = nm->mkNode(STRING_STRCTN, itxo->second[i], results[i]);
+      Node contr = Rewriter::rewrite(cont);
+      if (contr == d_false)
+      {
+        cmp_indices.push_back(i);
+        Trace("sygus-pbe-cterm-debug") << "...not contained." << std::endl;
+      }
+      else
+      {
+        Trace("sygus-pbe-cterm-debug") << "...contained." << std::endl;
+      }
+    }
+    if (!cmp_indices.empty())
+    {
+      // we check invariance with respect to a negative contains test
+      NegContainsSygusInvarianceTest ncset;
+      ncset.init(d_parent, x, itxo->second, cmp_indices);
+      // construct the generalized explanation
+      d_tds->getExplain()->getExplanationFor(x, v, exp, ncset);
+      Trace("sygus-pbe-cterm")
+          << "PBE-cterm : enumerator exclude " << d_tds->sygusToBuiltin(v)
+          << " due to negative containment." << std::endl;
+      return true;
+    }
+  }
+  return false;
+}
+
+
+
+void CegConjecturePbe::EnumInfo::addEnumValue( CegConjecturePbe * pbe, Node v, std::vector< Node >& results ) {
+  d_enum_val_to_index[v] = d_enum_vals.size();
+  d_enum_vals.push_back( v );
+  d_enum_vals_res.push_back( results );
+  /*
+  if( getRole()==enum_io ){
+    // compute
+    if( d_enum_total.empty() ){
+      d_enum_total = results;
+    }else if( !d_enum_total_true ){
+      d_enum_total_true = true;
+      Assert( d_enum_total.size()==results.size() );
+      for( unsigned i=0; i<results.size(); i++ ){
+        if( d_enum_total[i]==pbe->d_true || results[i]==pbe->d_true ){
+          d_enum_total[i] = pbe->d_true;
+        }else{
+          d_enum_total[i] = pbe->d_false;
+          d_enum_total_true = false;
+        }
+      }
+    }
+  }
+  */
+}
+
+void CegConjecturePbe::EnumInfo::initialize(Node c, EnumRole role)
+{
+  d_parent_candidate = c;
+  d_role = role;
+}
+
+void CegConjecturePbe::EnumInfo::setSolved( Node slv ) {
+  d_enum_solved = slv;
+  //d_enum_total_true = true;
+}
+    
+void CegConjecturePbe::CandidateInfo::initialize( Node c ) {
+  d_this_candidate = c;
+  d_root = c.getType();
+}
+
+void CegConjecturePbe::CandidateInfo::initializeType( TypeNode tn ) {
+  d_tinfo[tn].d_this_type = tn;
+  d_tinfo[tn].d_parent = this;
+}
+
+Node CegConjecturePbe::CandidateInfo::getRootEnumerator() {
+  std::map<EnumRole, Node>::iterator it = d_tinfo[d_root].d_enum.find(enum_io);
+  Assert( it!=d_tinfo[d_root].d_enum.end() );
+  return it->second;
+}
+
+bool CegConjecturePbe::CandidateInfo::isNonTrivial() {
+  //TODO
+  return true;
+}
+
+// status : 0 : exact, -1 : vals is subset, 1 : vals is superset
+Node CegConjecturePbe::SubsumeTrie::addTermInternal( CegConjecturePbe * pbe, Node t, std::vector< Node >& vals, bool pol, 
+                                                     std::vector< Node >& subsumed, bool spol, IndexFilter * f, 
+                                                     unsigned index, int status, bool checkExistsOnly, bool checkSubsume ) {
+  if( index==vals.size() ){
+    if( status==0 ){
+      // set the term if checkExistsOnly = false
+      if( d_term.isNull() && !checkExistsOnly ){
+        d_term = t;
+      }
+    }else if( status==1 ){
+      Assert( checkSubsume );
+      // found a subsumed term
+      if( !d_term.isNull() ){
+        subsumed.push_back( d_term );
+        if( !checkExistsOnly ){
+          // remove it if checkExistsOnly = false
+          d_term = Node::null();
+        }
+      }
+    }else{
+      Assert( !checkExistsOnly && checkSubsume );
+    }
+    return d_term;
+  }else{
+    // the current value 
+    Assert( pol || ( vals[index].isConst() && vals[index].getType().isBoolean() ) );
+    Node cv = pol ? vals[index] : ( vals[index]==pbe->d_true ? pbe->d_false : pbe->d_true );
+    // if checkExistsOnly = false, check if the current value is subsumed if checkSubsume = true, if so, don't add
+    if( !checkExistsOnly && checkSubsume ){
+      std::vector< bool > check_subsumed_by;
+      if( status==0 ){
+        if( cv==pbe->d_false ){
+          check_subsumed_by.push_back( spol );
+        }
+      }else if( status==-1 ){
+        check_subsumed_by.push_back( spol );
+        if( cv==pbe->d_false ){
+          check_subsumed_by.push_back( !spol );
+        }
+      }
+      // check for subsumed nodes
+      for( unsigned i=0; i<check_subsumed_by.size(); i++ ){
+        Node csval = check_subsumed_by[i] ? pbe->d_true : pbe->d_false;
+        // check if subsumed
+        std::map< Node, SubsumeTrie >::iterator itc = d_children.find( csval );
+        if( itc!=d_children.end() ){
+          unsigned next_index = f ? f->next( index ) : index+1;
+          Node ret = itc->second.addTermInternal( pbe, t, vals, pol, subsumed, spol, f, next_index, -1, checkExistsOnly, checkSubsume );
+          // ret subsumes t
+          if( !ret.isNull() ){
+            return ret;
+          }
+        }
+      }
+    }
+    Node ret;
+    std::vector< bool > check_subsume;
+    if( status==0 ){
+      unsigned next_index = f ? f->next( index ) : index+1;
+      if( checkExistsOnly ){
+        std::map< Node, SubsumeTrie >::iterator itc = d_children.find( cv );
+        if( itc!=d_children.end() ){
+          ret = itc->second.addTermInternal( pbe, t, vals, pol, subsumed, spol, f, next_index, 0, checkExistsOnly, checkSubsume );
+        }
+      }else{
+        Assert( spol );
+        ret = d_children[cv].addTermInternal( pbe, t, vals, pol, subsumed, spol, f, next_index, 0, checkExistsOnly, checkSubsume );
+        if( ret!=t ){
+          // we were subsumed by ret, return
+          return ret;
+        }
+      }
+      if( checkSubsume ){
+        // check for subsuming
+        if( cv==pbe->d_true ){
+          check_subsume.push_back( !spol );
+        }
+      }
+    }else if( status==1 ){
+      Assert( checkSubsume );
+      check_subsume.push_back( !spol );
+      if( cv==pbe->d_true ){
+        check_subsume.push_back( spol );
+      }
+    }
+    if( checkSubsume ){
+      // check for subsumed terms
+      for( unsigned i=0; i<check_subsume.size(); i++ ){
+        Node csval = check_subsume[i] ? pbe->d_true : pbe->d_false;
+        std::map< Node, SubsumeTrie >::iterator itc = d_children.find( csval );
+        if( itc!=d_children.end() ){
+          unsigned next_index = f ? f->next( index ) : index+1;
+          itc->second.addTermInternal( pbe, t, vals, pol, subsumed, spol, f, next_index, 1, checkExistsOnly, checkSubsume );
+          // clean up
+          if( itc->second.isEmpty() ){
+            Assert( !checkExistsOnly );
+            d_children.erase( csval );
+          }
+        }
+      }
+    }
+    return ret;
+  }
+}
+
+Node CegConjecturePbe::SubsumeTrie::addTerm( CegConjecturePbe * pbe, Node t, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed, IndexFilter * f ) {
+  unsigned start_index = f ? f->start() : 0;
+  return addTermInternal( pbe, t, vals, pol, subsumed, true, f, start_index, 0, false, true );
+}
+
+Node CegConjecturePbe::SubsumeTrie::addCond( CegConjecturePbe * pbe, Node c, std::vector< Node >& vals, bool pol, IndexFilter * f ) {
+  unsigned start_index = f ? f->start() : 0;
+  std::vector< Node > subsumed;
+  return addTermInternal( pbe, c, vals, pol, subsumed, true, f, start_index, 0, false, false );
+}
+
+void CegConjecturePbe::SubsumeTrie::getSubsumed( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed, IndexFilter * f ){
+  unsigned start_index = f ? f->start() : 0;
+  addTermInternal( pbe, Node::null(), vals, pol, subsumed, true, f, start_index, 1, true, true );
+}
+
+void CegConjecturePbe::SubsumeTrie::getSubsumedBy( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed_by, IndexFilter * f ){
+  // flip polarities
+  unsigned start_index = f ? f->start() : 0;
+  addTermInternal( pbe, Node::null(), vals, !pol, subsumed_by, false, f, start_index, 1, true, true );
+}
+
+void CegConjecturePbe::SubsumeTrie::getLeavesInternal( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::map< int, std::vector< Node > >& v, 
+                                                       IndexFilter * f, unsigned index, int status ) {
+  if( index==vals.size() ){
+    Assert( !d_term.isNull() );
+    Assert( std::find( v[status].begin(), v[status].end(), d_term )==v[status].end() );
+    v[status].push_back( d_term );
+  }else{
+    Assert( vals[index].isConst() && vals[index].getType().isBoolean() );
+    // filter should be for cv
+    Assert( f==NULL || vals[index]==( pol ? pbe->d_true : pbe->d_false ) );
+    for( std::map< Node, SubsumeTrie >::iterator it = d_children.begin(); it != d_children.end(); ++it ){
+      int new_status = status;
+      // if the current value is true
+      if( vals[index]==( pol ? pbe->d_true : pbe->d_false ) ){
+        if( status!=0 ){
+          new_status = ( it->first == pbe->d_true ? 1 : -1 );
+          if( status!=-2 && new_status!=status ){
+            new_status = 0;
+          }
+        }
+      }
+      unsigned next_index = f ? f->next( index ) : index+1;
+      it->second.getLeavesInternal( pbe, vals, pol, v, f, next_index, new_status );
+    }
+  }
+}
+
+void CegConjecturePbe::SubsumeTrie::getLeaves( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::map< int, std::vector< Node > >& v, IndexFilter * f ) {
+  unsigned start_index = f ? f->start() : 0;
+  getLeavesInternal( pbe, vals, pol, v, f, start_index, -2 );
+}
+
+void CegConjecturePbe::IndexFilter::mk( std::vector< Node >& vals, bool pol ) {
+  Trace("sygus-pbe-debug") << "Make for : ";
+  print_val( "sygus-pbe-debug", vals, pol );
+  Trace("sygus-pbe-debug") << std::endl;
+  Node poln = NodeManager::currentNM()->mkConst( pol );
+  
+  unsigned curr_index = 0;
+  while( curr_index<vals.size() && vals[curr_index]!=poln ){
+    curr_index++;
+  }
+  d_next[0] = curr_index;
+  Trace("sygus-pbe-debug") << "0 -> " << curr_index << std::endl;
+  unsigned i = curr_index;
+  while( i<vals.size() ){
+    while( i<vals.size() && vals[i]!=poln ){
+      i++;
+    }
+    i++;
+    d_next[curr_index+1] = i;
+    Trace("sygus-pbe-debug") << curr_index+1 << " -> " << i << std::endl;
+    curr_index = i;
+  }
+  
+  // verify it is correct
+  unsigned j = start();
+  for( unsigned k=0; k<j; k++ ){
+    AlwaysAssert( vals[k]!=poln );
+  }
+  Trace("sygus-pbe-debug") << "...start : " << j << std::endl;
+  unsigned counter = 0;
+  while( j<vals.size() ){
+    Trace("sygus-pbe-debug") << "...at : " << j << std::endl;
+    AlwaysAssert( vals[j]==poln );
+    unsigned jj = next( j );
+    AlwaysAssert( jj>j );
+    for( unsigned k=(j+1); k<jj; k++ ){
+      AlwaysAssert( vals[k]!=poln );
+    }
+    AlwaysAssert( counter<=vals.size() );
+    counter++;
+    j = jj;
+  }
+  
+  
+}
+
+unsigned CegConjecturePbe::IndexFilter::start() {
+  std::map< unsigned, unsigned >::iterator it = d_next.find( 0 );
+  if( it==d_next.end() ){
+    return 0;
+  }else{
+    return it->second;
+  }
+}
+
+unsigned CegConjecturePbe::IndexFilter::next( unsigned i ) {
+  std::map< unsigned, unsigned >::iterator it = d_next.find( i+1 );
+  if( it==d_next.end() ){
+    return i+1;
+  }else{
+    return it->second;
+  }      
+}
+
+bool CegConjecturePbe::IndexFilter::isEq( std::vector< Node >& vals, Node v ) {
+  unsigned index = start();
+  while( index<vals.size() ){
+    if( vals[index]!=v ){
+      return false;
+    }
+    index = next( index );
+  }
+  return true;
+}
+
+Node CegConjecturePbe::constructSolution( Node c ){
+  std::map< Node, CandidateInfo >::iterator itc = d_cinfo.find( c );
+  Assert( itc!=d_cinfo.end() );
+  if( !itc->second.d_solution.isNull() ){
+    // already has a solution
+    return itc->second.d_solution;
+  }else{
+    // only check if an enumerator updated
+    if( itc->second.d_check_sol ){
+      Trace("sygus-pbe") << "Construct solution, #iterations = " << itc->second.d_cond_count << std::endl;
+      itc->second.d_check_sol = false;
+      // try multiple times if we have done multiple conditions, due to non-determinism
+      Node vc;
+      for( unsigned i=0; i<=itc->second.d_cond_count; i++ ){
+        Trace("sygus-pbe-dt") << "ConstructPBE for candidate: " << c << std::endl;
+        Node e = itc->second.getRootEnumerator();
+        UnifContext x;
+        x.initialize( this, c );
+        Node vcc = constructSolution(c, e, role_equal, x, 1);
+        if( !vcc.isNull() ){
+          if( vc.isNull() || ( !vc.isNull() && d_tds->getSygusTermSize( vcc )<d_tds->getSygusTermSize( vc ) ) ){
+            Trace("sygus-pbe") << "**** PBE SOLVED : " << c << " = " << vcc << std::endl;
+            Trace("sygus-pbe") << "...solved at iteration " << i << std::endl;
+            vc = vcc;
+          }
+        }
+      }
+      if( !vc.isNull() ){
+        itc->second.d_solution = vc;
+        return vc;
+      }
+      Trace("sygus-pbe") << "...failed to solve." << std::endl;
+    }
+    return Node::null();
+  }
+}
+
+Node CegConjecturePbe::constructBestSolvedTerm( std::vector< Node >& solved, UnifContext& x ){
+  Assert( !solved.empty() );
+  // TODO
+  return solved[0];
+}
+
+Node CegConjecturePbe::constructBestStringSolvedTerm( std::vector< Node >& solved, UnifContext& x ) {
+  Assert( !solved.empty() );
+  // TODO
+  return solved[0];
+}
+
+Node CegConjecturePbe::constructBestSolvedConditional( std::vector< Node >& solved, UnifContext& x ){
+  Assert( !solved.empty() );
+  // TODO
+  return solved[0];
+}
+
+Node CegConjecturePbe::constructBestConditional( std::vector< Node >& conds, UnifContext& x ) {
+  Assert( !conds.empty() );
+  // TODO
+  double r = Random::getRandom().pickDouble(0.0, 1.0);
+  unsigned cindex = r*conds.size();
+  if( cindex>conds.size() ){
+    cindex = conds.size() - 1;
+  }
+  return conds[cindex];
+}
+
+Node CegConjecturePbe::constructBestStringToConcat( std::vector< Node > strs,
+                                                    std::map< Node, unsigned > total_inc, 
+                                                    std::map< Node, std::vector< unsigned > > incr,
+                                                    UnifContext& x ) {
+  Assert( !strs.empty() );
+  std::random_shuffle(strs.begin(), strs.end());
+  // prefer one that has incremented by more than 0
+  for (const Node& ns : strs)
+  {
+    if (total_inc[ns] > 0)
+    {
+      return ns;
+    }
+  }
+  return strs[0];
+}
+
+Node CegConjecturePbe::constructSolution(
+    Node c, Node e, NodeRole nrole, UnifContext& x, int ind)
+{
+  TypeNode etn = e.getType();
+  if (Trace.isOn("sygus-pbe-dt-debug"))
+  {
+    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 (nrole == role_equal)
+  {
+    if (!x.isReturnValueModified())
+    {
+      if (einfo.isSolved())
+      {
+        // 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)
+        {
+          // 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;
+          }
+        }
+      }
+    }
+  }
+  else if (nrole == role_string_prefix || nrole == role_string_suffix)
+  {
+    // check if each return value is a prefix/suffix of all open examples
+    if (!x.isReturnValueModified() || x.d_has_string_pos == nrole)
+    {
+      std::map<Node, std::vector<unsigned> > incr;
+      bool isPrefix = nrole == role_string_prefix;
+      std::map<Node, unsigned> total_inc;
+      std::vector<Node> inc_strs;
+      std::map<Node, std::vector<Node> >::iterator itx = d_examples_out.find(c);
+      Assert(itx != d_examples_out.end());
+      // make the value of the examples
+      std::vector<String> ex_vals;
+      x.getCurrentStrings(this, itx->second, ex_vals);
+      if (Trace.isOn("sygus-pbe-dt-debug"))
+      {
+        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") << "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", ind);
+        Trace("sygus-pbe-dt") << "PBE: failed CONCAT strategy, no values are "
+                              << (isPrefix ? "pre" : "suf")
+                              << "fix of all examples." << std::endl;
+      }
+    }
+    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);
+          }
+
+          // recurse
+          if (strat == strat_ITE && sc == 0)
+          {
+            Node ce = cenum.first;
+
+            // register the condition enumerator
+            std::map<Node, EnumInfo>::iterator itnc = d_einfo.find(ce);
+            Assert(itnc != d_einfo.end());
+            EnumInfo& einfo_child = itnc->second;
+
+            // only used if the return value is not modified
+            if (!x.isReturnValueModified())
+            {
+              if (x.d_uinfo.find(ce) == x.d_uinfo.end())
+              {
+                Trace("sygus-pbe-dt-debug2")
+                    << "  reg : PBE: Look for direct solutions for conditional "
+                       "enumerator "
+                    << ce << " ... " << std::endl;
+                Assert(einfo_child.d_enum_vals.size()
+                       == einfo_child.d_enum_vals_res.size());
+                for (unsigned i = 1; i <= 2; i++)
+                {
+                  std::pair<Node, NodeRole>& te_pair = etis->d_cenum[i];
+                  Node te = te_pair.first;
+                  std::map<Node, EnumInfo>::iterator itnt = d_einfo.find(te);
+                  Assert(itnt != d_einfo.end());
+                  bool branch_pol = (i == 1);
+                  // for each condition, get terms that satisfy it in this
+                  // branch
+                  for (unsigned k = 0, size = einfo_child.d_enum_vals.size();
+                       k < size;
+                       k++)
+                  {
+                    Node cond = einfo_child.d_enum_vals[k];
+                    std::vector<Node> solved;
+                    itnt->second.d_term_trie.getSubsumedBy(
+                        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;
+                    }
+                  }
+                }
+              }
+            }
+
+            // 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;
+                }
+              }
+
+              // static look ahead conditional : choose conditionals that have
+              // solved terms in at least one branch
+              //    only applicable if we have not modified the return value
+              std::map<int, std::vector<Node> > solved_cond;
+              if (!x.isReturnValueModified())
+              {
+                Assert(x.d_uinfo.find(ce) != x.d_uinfo.end());
+                int solve_max = 0;
+                for (Node& cond : itpc->second)
+                {
+                  std::map<Node, std::map<unsigned, Node> >::iterator itla =
+                      x.d_uinfo[ce].d_look_ahead_sols.find(cond);
+                  if (itla != x.d_uinfo[ce].d_look_ahead_sols.end())
+                  {
+                    int nsolved = itla->second.size();
+                    solve_max = nsolved > solve_max ? nsolved : solve_max;
+                    solved_cond[nsolved].push_back(cond);
+                  }
+                }
+                int n = solve_max;
+                while (n > 0)
+                {
+                  if (!solved_cond[n].empty())
+                  {
+                    rec_c = constructBestSolvedConditional(solved_cond[n], x);
+                    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() ){
+              Assert(einfo_child.d_enum_val_to_index.find(rec_c)
+                     != einfo_child.d_enum_val_to_index.end());
+              split_cond_res_index = einfo_child.d_enum_val_to_index[rec_c];
+              split_cond_enum = ce;
+              Assert(split_cond_res_index >= 0);
+              Assert(split_cond_res_index
+                     < (int)einfo_child.d_enum_vals_res.size());
+            }
+          }
+          else
+          {
+            rec_c = constructSolution(c, cenum.first, cenum.second, x, ind + 2);
+          }
+
+          // undo update the context
+          if (strat == strat_ITE && sc > 0)
+          {
+            x.d_vals = prev;
+          }
+        }
+        if (!rec_c.isNull())
+        {
+          dt_children_cons.push_back(rec_c);
+        }
+        else
+        {
+          success = false;
+          break;
+        }
+      }
+      if (success)
+      {
+        Assert(dt_children_cons.size() == etis->d_sol_templ_args.size());
+        // ret_dt = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR,
+        // dt_children );
+        ret_dt = etis->d_sol_templ;
+        ret_dt = ret_dt.substitute(etis->d_sol_templ_args.begin(),
+                                   etis->d_sol_templ_args.end(),
+                                   dt_children_cons.begin(),
+                                   dt_children_cons.end());
+        indent("sygus-pbe-dt-debug", ind);
+        Trace("sygus-pbe-dt-debug")
+            << "PBE: success : constructed for strategy " << strat << std::endl;
+      }else{
+        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() );
+  }
+  indent("sygus-pbe-dt", ind);
+  Trace("sygus-pbe-dt") << "ConstructPBE: returned " << ret_dt << std::endl;
+  return ret_dt;
+}
+
+bool CegConjecturePbe::UnifContext::updateContext( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol ) {
+  Assert( d_vals.size()==vals.size() );
+  bool changed = false;
+  Node poln = pol ? pbe->d_true : pbe->d_false;
+  for( unsigned i=0; i<vals.size(); i++ ){
+    if( vals[i]!=poln ){
+      if( d_vals[i]==pbe->d_true ){
+        d_vals[i] = pbe->d_false;
+        changed = true;
+      }
+    }
+  }
+  if (changed)
+  {
+    d_visit_role.clear();
+  }
+  return changed;
+}
+
+bool CegConjecturePbe::UnifContext::updateStringPosition( CegConjecturePbe * pbe, std::vector< unsigned >& pos ) {
+  Assert( pos.size()==d_str_pos.size() );
+  bool changed = false;
+  for( unsigned i=0; i<pos.size(); i++ ){
+    if( pos[i]>0 ){
+      d_str_pos[i] += pos[i];
+      changed = true;
+    }
+  }
+  if (changed)
+  {
+    d_visit_role.clear();
+  }
+  return changed;
+}
+
+bool CegConjecturePbe::UnifContext::isReturnValueModified() {
+  if (d_has_string_pos != role_invalid)
+  {
+    return true;
+  }
+  return false;
+}
+
+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() );
+  
+  // initialize with #examples
+  Assert( pbe->d_examples.find( c )!=pbe->d_examples.end() );
+  unsigned sz = pbe->d_examples[c].size();
+  for( unsigned i=0; i<sz; i++ ){
+    d_vals.push_back( pbe->d_true );
+  }
+  
+  if( !pbe->d_examples_out[c].empty() ){
+    // output type of the examples
+    TypeNode exotn = pbe->d_examples_out[c][0].getType();
+    
+    if( exotn.isString() ){
+      for( unsigned i=0; i<sz; i++ ){
+        d_str_pos.push_back( 0 );
+      }
+    }
+  }
+  d_visit_role.clear();
+}
+
+void CegConjecturePbe::UnifContext::getCurrentStrings(
+    CegConjecturePbe* pbe,
+    const std::vector<Node>& vals,
+    std::vector<String>& ex_vals)
+{
+  bool isPrefix = d_has_string_pos == role_string_prefix;
+  String dummy;
+  for( unsigned i=0; i<vals.size(); i++ ){
+    if( d_vals[i]==pbe->d_true ){
+      Assert( vals[i].isConst() );
+      unsigned pos_value = d_str_pos[i];
+      if( pos_value>0 ){
+        Assert(d_has_string_pos != role_invalid);
+        String s = vals[i].getConst<String>();
+        Assert( pos_value<=s.size() );
+        ex_vals.push_back( isPrefix ? s.suffix( s.size()-pos_value ) : 
+                                      s.prefix( s.size()-pos_value ) );
+      }else{
+        ex_vals.push_back( vals[i].getConst<String>() );
+      }
+    }else{
+      // irrelevant, add dummy
+      ex_vals.push_back( dummy );
+    }
+  }
+}
+
+bool CegConjecturePbe::UnifContext::getStringIncrement(
+    CegConjecturePbe* pbe,
+    bool isPrefix,
+    const std::vector<String>& ex_vals,
+    const std::vector<Node>& vals,
+    std::vector<unsigned>& inc,
+    unsigned& tot)
+{
+  for( unsigned j=0; j<vals.size(); j++ ){
+    unsigned ival = 0;
+    if( d_vals[j]==pbe->d_true ){
+      // example is active in this context
+      Assert( vals[j].isConst() );
+      String mystr = vals[j].getConst<String>();
+      ival = mystr.size();
+      if( mystr.size()<=ex_vals[j].size() ){
+        if( !( isPrefix ? ex_vals[j].strncmp(mystr, ival) : ex_vals[j].rstrncmp(mystr, ival) ) ){
+          Trace("sygus-pbe-dt-debug") << "X";
+          return false;
+        }
+      }else{
+        Trace("sygus-pbe-dt-debug") << "X";
+        return false;
+      }
+    }
+    Trace("sygus-pbe-dt-debug") << ival;
+    tot += ival;
+    inc.push_back( ival );
+  }
+  return true;
+}
+bool CegConjecturePbe::UnifContext::isStringSolved(
+    CegConjecturePbe* pbe,
+    const std::vector<String>& ex_vals,
+    const std::vector<Node>& vals)
+{
+  for( unsigned j=0; j<vals.size(); j++ ){
+    if( d_vals[j]==pbe->d_true ){
+      // example is active in this context
+      Assert( vals[j].isConst() );
+      String mystr = vals[j].getConst<String>();
+      if( ex_vals[j]!=mystr ){
+        return false;
+      }
+    }
+  }
+  return true;
+}
+
+CegConjecturePbe::StrategyNode::~StrategyNode()
+{
+  for (unsigned j = 0, size = d_strats.size(); j < size; j++)
+  {
+    delete d_strats[j];
+  }
+  d_strats.clear();
+}
+}
+}
+}