Make sygus unif utility (#1720)

7 files changed, 3092 insertions, 185 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 53fc3b8bd..9b1b71efc 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -472,6 +472,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/sygus/sygus_module.h \
 	theory/quantifiers/sygus/sygus_process_conj.cpp \
 	theory/quantifiers/sygus/sygus_process_conj.h \
+	theory/quantifiers/sygus/sygus_unif.cpp \
+	theory/quantifiers/sygus/sygus_unif.h \
 	theory/quantifiers/sygus/term_database_sygus.cpp \
 	theory/quantifiers/sygus/term_database_sygus.h \
 	theory/quantifiers/sygus_sampler.cpp \
diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp
index 6b4c6488d..f4aa07673 100644
--- a/src/theory/quantifiers/sygus/sygus_invariance.cpp
+++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp
@@ -157,20 +157,16 @@ bool DivByZeroSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
   return false;
 }
 
-void NegContainsSygusInvarianceTest::init(CegConjecture* conj,
-                                          Node e,
+void NegContainsSygusInvarianceTest::init(Node e,
+                                          std::vector<std::vector<Node> >& ex,
                                           std::vector<Node>& exo,
                                           std::vector<unsigned>& ncind)
 {
-  if (conj->getPbe()->hasExamples(e))
-  {
-    Assert(conj->getPbe()->getNumExamples(e) == exo.size());
-    d_enum = e;
-    d_exo.insert(d_exo.end(), exo.begin(), exo.end());
-    d_neg_con_indices.insert(
-        d_neg_con_indices.end(), ncind.begin(), ncind.end());
-    d_conj = conj;
-  }
+  Assert(ex.size() == exo.size());
+  d_enum = e;
+  d_ex.insert(d_ex.end(), ex.begin(), ex.end());
+  d_exo.insert(d_exo.end(), exo.begin(), exo.end());
+  d_neg_con_indices.insert(d_neg_con_indices.end(), ncind.begin(), ncind.end());
 }
 
 bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds,
@@ -187,7 +183,7 @@ bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds,
     {
       unsigned ii = d_neg_con_indices[i];
       Assert(ii < d_exo.size());
-      Node nbvre = d_conj->getPbe()->evaluateBuiltin(tn, nbvr, d_enum, ii);
+      Node nbvre = tds->evaluateBuiltin(tn, nbvr, d_ex[ii]);
       Node out = d_exo[ii];
       Node cont =
           NodeManager::currentNM()->mkNode(kind::STRING_STRCTN, out, nbvre);
@@ -203,11 +199,9 @@ bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds,
                                    << tds->sygusToBuiltin(x) << " since "
                                    << std::endl;
           Trace("sygus-pbe-cterm") << "   PBE-cterm :    for input example : ";
-          std::vector<Node> ex;
-          d_conj->getPbe()->getExample(d_enum, ii, ex);
-          for (unsigned j = 0; j < ex.size(); j++)
+          for (unsigned j = 0, size = d_ex[ii].size(); j < size; j++)
           {
-            Trace("sygus-pbe-cterm") << ex[j] << " ";
+            Trace("sygus-pbe-cterm") << d_ex[ii][j] << " ";
           }
           Trace("sygus-pbe-cterm") << std::endl;
           Trace("sygus-pbe-cterm")
diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h
index 9e357f928..577923f5b 100644
--- a/src/theory/quantifiers/sygus/sygus_invariance.h
+++ b/src/theory/quantifiers/sygus/sygus_invariance.h
@@ -234,21 +234,21 @@ class DivByZeroSygusInvarianceTest : public SygusInvarianceTest
 class NegContainsSygusInvarianceTest : public SygusInvarianceTest
 {
  public:
-  NegContainsSygusInvarianceTest() : d_conj(nullptr) {}
+  NegContainsSygusInvarianceTest() {}
 
   /** initialize this invariance test
-   *  cpbe is the conjecture utility.
    *  e is the enumerator which we are reasoning about (associated with a synth
    *    fun).
-   *  exo is the list of outputs of the PBE conjecture.
-   *  ncind is the set of possible indices of the PBE conjecture to check
-   *    invariance of non-containment.
+   *  ex is the list of inputs,
+   *  exo is the list of outputs,
+   *  ncind is the set of possible example indices to check invariance of
+   *  non-containment.
    *    For example, in the above example, when t[x1] = "ab", then this
    *    has the index 1 since contains("de de", "ab") ---> false but not
    *    the index 0 since contains("abc abc","ab") ---> true.
    */
-  void init(CegConjecture* conj,
-            Node e,
+  void init(Node e,
+            std::vector<std::vector<Node> >& ex,
             std::vector<Node>& exo,
             std::vector<unsigned>& ncind);
 
@@ -259,14 +259,14 @@ class NegContainsSygusInvarianceTest : public SygusInvarianceTest
  private:
   /** The enumerator whose value we are considering in this invariance test */
   Node d_enum;
+  /** The input examples */
+  std::vector<std::vector<Node> > d_ex;
   /** The output examples for the enumerator */
   std::vector<Node> d_exo;
   /** The set of I/O pair indices i such that
    *    contains( out_i, nvn[in_i] ) ---> false
    */
   std::vector<unsigned> d_neg_con_indices;
-  /** reference to the conjecture associated with this test */
-  CegConjecture* d_conj;
 };
 
 } /* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 528f47624..347efac26 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -28,74 +28,6 @@ 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)
     : SygusModule(qe, p)
 {
@@ -971,7 +903,7 @@ void CegConjecturePbe::staticLearnRedundantOps(
     {
       itn->second.setConditional();
     }
-    indent("sygus-unif", ind);
+    SygusUnif::indent("sygus-unif", ind);
     Trace("sygus-unif") << e << " :: node role : " << nrole;
     Trace("sygus-unif")
         << ", type : "
@@ -1012,7 +944,7 @@ void CegConjecturePbe::staticLearnRedundantOps(
         EnumTypeInfoStrat* etis = snode.d_strats[j];
         StrategyType strat = etis->d_this;
         bool newIsCond = isCond || strat == strat_ITE;
-        indent("sygus-unif", ind + 1);
+        SygusUnif::indent("sygus-unif", ind + 1);
         Trace("sygus-unif") << "Strategy : " << strat
                             << ", from cons : " << etis->d_cons << std::endl;
         int cindex = Datatype::indexOf(etis->d_cons.toExpr());
@@ -1064,7 +996,7 @@ void CegConjecturePbe::staticLearnRedundantOps(
       }
     }
   }else{
-    indent("sygus-unif", ind);
+    SygusUnif::indent("sygus-unif", ind);
     Trace("sygus-unif") << e << " :: node role : " << nrole << std::endl;
   }
 }
@@ -1402,7 +1334,7 @@ bool CegConjecturePbe::getExplanationForEnumeratorExclude(
     {
       // we check invariance with respect to a negative contains test
       NegContainsSygusInvarianceTest ncset;
-      ncset.init(d_parent, x, itxo->second, cmp_indices);
+      ncset.init(x, d_examples[c], itxo->second, cmp_indices);
       // construct the generalized explanation
       d_tds->getExplain()->getExplanationFor(x, v, exp, ncset);
       Trace("sygus-pbe-cterm")
@@ -1823,10 +1755,10 @@ Node CegConjecturePbe::constructSolution(
   TypeNode etn = e.getType();
   if (Trace.isOn("sygus-pbe-dt-debug"))
   {
-    indent("sygus-pbe-dt-debug", ind);
+    SygusUnif::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);
+    SygusUnif::print_val("sygus-pbe-dt-debug", x.d_vals);
     if (x.d_has_string_pos != role_invalid)
     {
       Trace("sygus-pbe-dt-debug") << ", string context [" << x.d_has_string_pos;
@@ -1857,7 +1789,7 @@ Node CegConjecturePbe::constructSolution(
       {
         // this type has a complete solution
         ret_dt = einfo.getSolved();
-        indent("sygus-pbe-dt", ind);
+        SygusUnif::indent("sygus-pbe-dt", ind);
         Trace("sygus-pbe-dt") << "return PBE: success : solved "
                               << d_tds->sygusToBuiltin(ret_dt) << std::endl;
         Assert(!ret_dt.isNull());
@@ -1870,13 +1802,13 @@ Node CegConjecturePbe::constructSolution(
         if (!subsumed_by.empty())
         {
           ret_dt = constructBestSolvedTerm(subsumed_by, x);
-          indent("sygus-pbe-dt", ind);
+          SygusUnif::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);
+          SygusUnif::indent("sygus-pbe-dt-debug", ind);
           Trace("sygus-pbe-dt-debug")
               << "  ...not currently conditionally solved." << std::endl;
         }
@@ -1924,13 +1856,13 @@ Node CegConjecturePbe::constructSolution(
           if (!str_solved.empty())
           {
             ret_dt = constructBestStringSolvedTerm(str_solved, x);
-            indent("sygus-pbe-dt", ind);
+            SygusUnif::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);
+            SygusUnif::indent("sygus-pbe-dt-debug", ind);
             Trace("sygus-pbe-dt-debug") << "  ...not currently string solved."
                                         << std::endl;
           }
@@ -1954,11 +1886,11 @@ Node CegConjecturePbe::constructSolution(
       x.getCurrentStrings(this, itx->second, ex_vals);
       if (Trace.isOn("sygus-pbe-dt-debug"))
       {
-        indent("sygus-pbe-dt-debug", ind);
+        SygusUnif::indent("sygus-pbe-dt-debug", ind);
         Trace("sygus-pbe-dt-debug") << "current strings : " << std::endl;
         for (unsigned i = 0, size = ex_vals.size(); i < size; i++)
         {
-          indent("sygus-pbe-dt-debug", ind + 1);
+          SygusUnif::indent("sygus-pbe-dt-debug", ind + 1);
           Trace("sygus-pbe-dt-debug") << ex_vals[i] << std::endl;
         }
       }
@@ -1970,7 +1902,7 @@ Node CegConjecturePbe::constructSolution(
       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);
+        SygusUnif::indent("sygus-pbe-dt-debug", ind);
         Trace("sygus-pbe-dt-debug") << "increment string values : " << val_t
                                     << " : ";
         Assert(einfo.d_enum_vals_res[i].size() == itx->second.size());
@@ -1999,7 +1931,7 @@ Node CegConjecturePbe::constructSolution(
       {
         ret_dt = constructBestStringToConcat(inc_strs, total_inc, incr, x);
         Assert(!ret_dt.isNull());
-        indent("sygus-pbe-dt", ind);
+        SygusUnif::indent("sygus-pbe-dt", ind);
         Trace("sygus-pbe-dt") << "PBE: CONCAT strategy : choose "
                               << (isPrefix ? "pre" : "suf") << "fix value "
                               << d_tds->sygusToBuiltin(ret_dt) << std::endl;
@@ -2008,7 +1940,7 @@ Node CegConjecturePbe::constructSolution(
         AlwaysAssert(ret == (total_inc[ret_dt] > 0));
         x.d_has_string_pos = nrole;
       }else{
-        indent("sygus-pbe-dt", ind);
+        SygusUnif::indent("sygus-pbe-dt", ind);
         Trace("sygus-pbe-dt") << "PBE: failed CONCAT strategy, no values are "
                               << (isPrefix ? "pre" : "suf")
                               << "fix of all examples." << std::endl;
@@ -2016,7 +1948,7 @@ Node CegConjecturePbe::constructSolution(
     }
     else
     {
-      indent("sygus-pbe-dt", ind);
+      SygusUnif::indent("sygus-pbe-dt", ind);
       Trace("sygus-pbe-dt")
           << "PBE: failed CONCAT strategy, prefix/suffix mismatch."
           << std::endl;
@@ -2057,7 +1989,7 @@ Node CegConjecturePbe::constructSolution(
     if (etis != nullptr)
     {
       StrategyType strat = etis->d_this;
-      indent("sygus-pbe-dt", ind + 1);
+      SygusUnif::indent("sygus-pbe-dt", ind + 1);
       Trace("sygus-pbe-dt") << "...try STRATEGY " << strat << "..."
                             << std::endl;
 
@@ -2071,7 +2003,7 @@ Node CegConjecturePbe::constructSolution(
 
       for (unsigned sc = 0, size = etis->d_cenum.size(); sc < size; sc++)
       {
-        indent("sygus-pbe-dt", ind + 1);
+        SygusUnif::indent("sygus-pbe-dt", ind + 1);
         Trace("sygus-pbe-dt") << "construct PBE child #" << sc << "..."
                               << std::endl;
         Node rec_c;
@@ -2080,7 +2012,7 @@ Node CegConjecturePbe::constructSolution(
         if (itla != look_ahead_solved_children.end())
         {
           rec_c = itla->second;
-          indent("sygus-pbe-dt-debug", ind + 1);
+          SygusUnif::indent("sygus-pbe-dt-debug", ind + 1);
           Trace("sygus-pbe-dt-debug") << "ConstructPBE: look ahead solved : "
                                       << d_tds->sygusToBuiltin(rec_c)
                                       << std::endl;
@@ -2179,13 +2111,13 @@ Node CegConjecturePbe::constructSolution(
             {
               if (Trace.isOn("sygus-pbe-dt-debug"))
               {
-                indent("sygus-pbe-dt-debug", ind + 1);
+                SygusUnif::indent("sygus-pbe-dt-debug", ind + 1);
                 Trace("sygus-pbe-dt-debug")
                     << "PBE : We have " << itpc->second.size()
                     << " distinguishable conditionals:" << std::endl;
                 for (Node& cond : itpc->second)
                 {
-                  indent("sygus-pbe-dt-debug", ind + 2);
+                  SygusUnif::indent("sygus-pbe-dt-debug", ind + 2);
                   Trace("sygus-pbe-dt-debug") << d_tds->sygusToBuiltin(cond)
                                               << std::endl;
                 }
@@ -2216,7 +2148,7 @@ Node CegConjecturePbe::constructSolution(
                   if (!solved_cond[n].empty())
                   {
                     rec_c = constructBestSolvedConditional(solved_cond[n], x);
-                    indent("sygus-pbe-dt", ind + 1);
+                    SygusUnif::indent("sygus-pbe-dt", ind + 1);
                     Trace("sygus-pbe-dt")
                         << "PBE: ITE strategy : choose solved conditional "
                         << d_tds->sygusToBuiltin(rec_c) << " with " << n
@@ -2239,7 +2171,7 @@ Node CegConjecturePbe::constructSolution(
               {
                 rec_c = constructBestConditional(itpc->second, x);
                 Assert(!rec_c.isNull());
-                indent("sygus-pbe-dt", ind);
+                SygusUnif::indent("sygus-pbe-dt", ind);
                 Trace("sygus-pbe-dt")
                     << "PBE: ITE strategy : choose random conditional "
                     << d_tds->sygusToBuiltin(rec_c) << std::endl;
@@ -2249,7 +2181,7 @@ Node CegConjecturePbe::constructSolution(
             {
               // TODO (#1250) : degenerate case where children have different
               // types?
-              indent("sygus-pbe-dt", ind);
+              SygusUnif::indent("sygus-pbe-dt", ind);
               Trace("sygus-pbe-dt") << "return PBE: failed ITE strategy, "
                                        "cannot find a distinguishable condition"
                                     << std::endl;
@@ -2295,11 +2227,11 @@ Node CegConjecturePbe::constructSolution(
                                    etis->d_sol_templ_args.end(),
                                    dt_children_cons.begin(),
                                    dt_children_cons.end());
-        indent("sygus-pbe-dt-debug", ind);
+        SygusUnif::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);
+        SygusUnif::indent("sygus-pbe-dt-debug", ind);
         Trace("sygus-pbe-dt-debug") << "PBE: failed for strategy " << strat
                                     << std::endl;
       }
@@ -2309,7 +2241,7 @@ Node CegConjecturePbe::constructSolution(
   if( !ret_dt.isNull() ){
     Assert( ret_dt.getType()==e.getType() );
   }
-  indent("sygus-pbe-dt", ind);
+  SygusUnif::indent("sygus-pbe-dt", ind);
   Trace("sygus-pbe-dt") << "ConstructPBE: returned " << ret_dt << std::endl;
   return ret_dt;
 }
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h
index 38a170fbe..dd98dd0aa 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.h
+++ b/src/theory/quantifiers/sygus/sygus_pbe.h
@@ -19,75 +19,12 @@
 
 #include "context/cdhashmap.h"
 #include "theory/quantifiers/sygus/sygus_module.h"
+#include "theory/quantifiers/sygus/sygus_unif.h"
 
 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
diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp
new file mode 100644
index 000000000..ee0590b6b
--- /dev/null
+++ b/src/theory/quantifiers/sygus/sygus_unif.cpp
@@ -0,0 +1,2284 @@
+/*********************                                                        */
+/*! \file sygus_unif.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of sygus_unif
+ **/
+
+#include "theory/quantifiers/sygus/sygus_unif.h"
+
+#include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
+#include "util/random.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+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;
+}
+
+UnifContext::UnifContext() : d_has_string_pos(role_invalid)
+{
+  d_true = NodeManager::currentNM()->mkConst(true);
+  d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+bool UnifContext::updateContext(SygusUnif* pbe,
+                                std::vector<Node>& vals,
+                                bool pol)
+{
+  Assert(d_vals.size() == vals.size());
+  bool changed = false;
+  Node poln = pol ? d_true : d_false;
+  for (unsigned i = 0; i < vals.size(); i++)
+  {
+    if (vals[i] != poln)
+    {
+      if (d_vals[i] == d_true)
+      {
+        d_vals[i] = d_false;
+        changed = true;
+      }
+    }
+  }
+  if (changed)
+  {
+    d_visit_role.clear();
+  }
+  return changed;
+}
+
+bool UnifContext::updateStringPosition(SygusUnif* 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 UnifContext::isReturnValueModified()
+{
+  if (d_has_string_pos != role_invalid)
+  {
+    return true;
+  }
+  return false;
+}
+
+void UnifContext::initialize(SygusUnif* pbe, Node c)
+{
+  Assert(d_vals.empty());
+  Assert(d_str_pos.empty());
+
+  // initialize with #examples
+  Assert(pbe->d_examples.find(c) != pbe->d_examples.end());
+  unsigned sz = pbe->d_examples[c].size();
+  for (unsigned i = 0; i < sz; i++)
+  {
+    d_vals.push_back(d_true);
+  }
+
+  if (!pbe->d_examples_out[c].empty())
+  {
+    // output type of the examples
+    TypeNode exotn = pbe->d_examples_out[c][0].getType();
+
+    if (exotn.isString())
+    {
+      for (unsigned i = 0; i < sz; i++)
+      {
+        d_str_pos.push_back(0);
+      }
+    }
+  }
+  d_visit_role.clear();
+}
+
+void UnifContext::getCurrentStrings(SygusUnif* 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 UnifContext::getStringIncrement(SygusUnif* 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 UnifContext::isStringSolved(SygusUnif* 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;
+}
+
+// status : 0 : exact, -1 : vals is subset, 1 : vals is superset
+Node SubsumeTrie::addTermInternal(Node t,
+                                  const std::vector<Node>& vals,
+                                  bool pol,
+                                  std::vector<Node>& subsumed,
+                                  bool spol,
+                                  unsigned index,
+                                  int status,
+                                  bool checkExistsOnly,
+                                  bool checkSubsume)
+{
+  if (index == vals.size())
+  {
+    if (status == 0)
+    {
+      // set the term if checkExistsOnly = false
+      if (d_term.isNull() && !checkExistsOnly)
+      {
+        d_term = t;
+      }
+    }
+    else if (status == 1)
+    {
+      Assert(checkSubsume);
+      // found a subsumed term
+      if (!d_term.isNull())
+      {
+        subsumed.push_back(d_term);
+        if (!checkExistsOnly)
+        {
+          // remove it if checkExistsOnly = false
+          d_term = Node::null();
+        }
+      }
+    }
+    else
+    {
+      Assert(!checkExistsOnly && checkSubsume);
+    }
+    return d_term;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  // the current value
+  Assert(pol || (vals[index].isConst() && vals[index].getType().isBoolean()));
+  Node cv = pol ? vals[index] : nm->mkConst(!vals[index].getConst<bool>());
+  // if checkExistsOnly = false, check if the current value is subsumed if
+  // checkSubsume = true, if so, don't add
+  if (!checkExistsOnly && checkSubsume)
+  {
+    Assert(cv.isConst() && cv.getType().isBoolean());
+    std::vector<bool> check_subsumed_by;
+    if (status == 0)
+    {
+      if (!cv.getConst<bool>())
+      {
+        check_subsumed_by.push_back(spol);
+      }
+    }
+    else if (status == -1)
+    {
+      check_subsumed_by.push_back(spol);
+      if (!cv.getConst<bool>())
+      {
+        check_subsumed_by.push_back(!spol);
+      }
+    }
+    // check for subsumed nodes
+    for (unsigned i = 0, size = check_subsumed_by.size(); i < size; i++)
+    {
+      bool csbi = check_subsumed_by[i];
+      Node csval = nm->mkConst(csbi);
+      // check if subsumed
+      std::map<Node, SubsumeTrie>::iterator itc = d_children.find(csval);
+      if (itc != d_children.end())
+      {
+        Node ret = itc->second.addTermInternal(t,
+                                               vals,
+                                               pol,
+                                               subsumed,
+                                               spol,
+                                               index + 1,
+                                               -1,
+                                               checkExistsOnly,
+                                               checkSubsume);
+        // ret subsumes t
+        if (!ret.isNull())
+        {
+          return ret;
+        }
+      }
+    }
+  }
+  Node ret;
+  std::vector<bool> check_subsume;
+  if (status == 0)
+  {
+    if (checkExistsOnly)
+    {
+      std::map<Node, SubsumeTrie>::iterator itc = d_children.find(cv);
+      if (itc != d_children.end())
+      {
+        ret = itc->second.addTermInternal(t,
+                                          vals,
+                                          pol,
+                                          subsumed,
+                                          spol,
+                                          index + 1,
+                                          0,
+                                          checkExistsOnly,
+                                          checkSubsume);
+      }
+    }
+    else
+    {
+      Assert(spol);
+      ret = d_children[cv].addTermInternal(t,
+                                           vals,
+                                           pol,
+                                           subsumed,
+                                           spol,
+                                           index + 1,
+                                           0,
+                                           checkExistsOnly,
+                                           checkSubsume);
+      if (ret != t)
+      {
+        // we were subsumed by ret, return
+        return ret;
+      }
+    }
+    if (checkSubsume)
+    {
+      Assert(cv.isConst() && cv.getType().isBoolean());
+      // check for subsuming
+      if (cv.getConst<bool>())
+      {
+        check_subsume.push_back(!spol);
+      }
+    }
+  }
+  else if (status == 1)
+  {
+    Assert(checkSubsume);
+    Assert(cv.isConst() && cv.getType().isBoolean());
+    check_subsume.push_back(!spol);
+    if (cv.getConst<bool>())
+    {
+      check_subsume.push_back(spol);
+    }
+  }
+  if (checkSubsume)
+  {
+    // check for subsumed terms
+    for (unsigned i = 0, size = check_subsume.size(); i < size; i++)
+    {
+      Node csval = nm->mkConst<bool>(check_subsume[i]);
+      std::map<Node, SubsumeTrie>::iterator itc = d_children.find(csval);
+      if (itc != d_children.end())
+      {
+        itc->second.addTermInternal(t,
+                                    vals,
+                                    pol,
+                                    subsumed,
+                                    spol,
+                                    index + 1,
+                                    1,
+                                    checkExistsOnly,
+                                    checkSubsume);
+        // clean up
+        if (itc->second.isEmpty())
+        {
+          Assert(!checkExistsOnly);
+          d_children.erase(csval);
+        }
+      }
+    }
+  }
+  return ret;
+}
+
+Node SubsumeTrie::addTerm(Node t,
+                          const std::vector<Node>& vals,
+                          bool pol,
+                          std::vector<Node>& subsumed)
+{
+  return addTermInternal(t, vals, pol, subsumed, true, 0, 0, false, true);
+}
+
+Node SubsumeTrie::addCond(Node c, const std::vector<Node>& vals, bool pol)
+{
+  std::vector<Node> subsumed;
+  return addTermInternal(c, vals, pol, subsumed, true, 0, 0, false, false);
+}
+
+void SubsumeTrie::getSubsumed(const std::vector<Node>& vals,
+                              bool pol,
+                              std::vector<Node>& subsumed)
+{
+  addTermInternal(Node::null(), vals, pol, subsumed, true, 0, 1, true, true);
+}
+
+void SubsumeTrie::getSubsumedBy(const std::vector<Node>& vals,
+                                bool pol,
+                                std::vector<Node>& subsumed_by)
+{
+  // flip polarities
+  addTermInternal(
+      Node::null(), vals, !pol, subsumed_by, false, 0, 1, true, true);
+}
+
+void SubsumeTrie::getLeavesInternal(const std::vector<Node>& vals,
+                                    bool pol,
+                                    std::map<int, std::vector<Node> >& v,
+                                    unsigned index,
+                                    int status)
+{
+  if (index == vals.size())
+  {
+    Assert(!d_term.isNull());
+    Assert(std::find(v[status].begin(), v[status].end(), d_term)
+           == v[status].end());
+    v[status].push_back(d_term);
+  }
+  else
+  {
+    Assert(vals[index].isConst() && vals[index].getType().isBoolean());
+    bool curr_val_true = vals[index].getConst<bool>() == pol;
+    for (std::map<Node, SubsumeTrie>::iterator it = d_children.begin();
+         it != d_children.end();
+         ++it)
+    {
+      int new_status = status;
+      // if the current value is true
+      if (curr_val_true)
+      {
+        if (status != 0)
+        {
+          Assert(it->first.isConst() && it->first.getType().isBoolean());
+          new_status = (it->first.getConst<bool>() ? 1 : -1);
+          if (status != -2 && new_status != status)
+          {
+            new_status = 0;
+          }
+        }
+      }
+      it->second.getLeavesInternal(vals, pol, v, index + 1, new_status);
+    }
+  }
+}
+
+void SubsumeTrie::getLeaves(const std::vector<Node>& vals,
+                            bool pol,
+                            std::map<int, std::vector<Node> >& v)
+{
+  getLeavesInternal(vals, pol, v, 0, -2);
+}
+
+SygusUnif::SygusUnif(QuantifiersEngine* qe) : d_qe(qe)
+{
+  d_tds = qe->getTermDatabaseSygus();
+  d_true = NodeManager::currentNM()->mkConst(true);
+  d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+SygusUnif::~SygusUnif() {}
+
+void SygusUnif::initialize(Node candidate,
+                           std::vector<Node>& lemmas,
+                           std::vector<Node>& enums)
+{
+  d_candidate = candidate;
+  // TODO
+}
+
+void SygusUnif::resetExamples()
+{
+  // TODO
+}
+
+void SygusUnif::addExample(const std::vector<Node>& input, Node output)
+{
+  // TODO
+}
+
+void SygusUnif::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
+{
+  // TODO
+}
+
+Node SygusUnif::constructSolution()
+{
+  Node c = d_candidate;
+  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();
+  }
+}
+
+// ----------------------------- establishing enumeration types
+
+void SygusUnif::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 "
+        << static_cast<DatatypeType>(tn.toType()).getDatatype().getName();
+    Trace("sygus-unif-debug") << ", role = " << enum_role
+                              << ", in search = " << inSearch << std::endl;
+    d_einfo[et].initialize(c, enum_role);
+    // 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);
+      }
+      else
+      {
+        Trace("sygus-unif-debug")
+            << "Make " << et << " a slave of " << itn->second << std::endl;
+        d_einfo[itn->second].d_enum_slave.push_back(et);
+      }
+    }
+  }
+}
+
+void SygusUnif::collectEnumeratorTypes(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 "
+        << static_cast<DatatypeType>(tn.toType()).getDatatype().getName()
+        << ", role = " << erole << std::endl;
+  }
+  else
+  {
+    ee = iten->second;
+  }
+
+  // roles that we do not recurse on
+  if (nrole == role_ite_condition)
+  {
+    Trace("sygus-unif-debug") << "...this register (non-io)" << std::endl;
+    registerEnumerator(ee, 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 "
+                                      << static_cast<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 "
+              << static_cast<DatatypeType>(tn.toType()).getDatatype().getName()
+              << ", operator " << cop;
+          Trace("sygus-unif") << ", #children = " << cons_strat->d_cenum.size()
+                              << ", solution template = (lambda ( ";
+          for (const Node& targ : cons_strat->d_sol_templ_args)
+          {
+            Trace("sygus-unif") << targ << " ";
+          }
+          Trace("sygus-unif") << ") " << cons_strat->d_sol_templ << ")";
+          Trace("sygus-unif") << std::endl;
+        }
+        // make the strategy
+        snode.d_strats.push_back(cons_strat);
+      }
+    }
+  }
+}
+
+bool SygusUnif::inferTemplate(unsigned k,
+                              Node n,
+                              std::map<Node, unsigned>& templ_var_index,
+                              std::map<unsigned, unsigned>& templ_injection)
+{
+  if (n.getNumChildren() == 0)
+  {
+    std::map<Node, unsigned>::iterator itt = templ_var_index.find(n);
+    if (itt != templ_var_index.end())
+    {
+      unsigned kk = itt->second;
+      std::map<unsigned, unsigned>::iterator itti = templ_injection.find(k);
+      if (itti == templ_injection.end())
+      {
+        Trace("sygus-unif-debug")
+            << "...set template injection " << k << " -> " << kk << std::endl;
+        templ_injection[k] = kk;
+      }
+      else if (itti->second != kk)
+      {
+        // two distinct variables in this term, we fail
+        return false;
+      }
+    }
+    return true;
+  }
+  else
+  {
+    for (unsigned i = 0; i < n.getNumChildren(); i++)
+    {
+      if (!inferTemplate(k, n[i], templ_var_index, templ_injection))
+      {
+        return false;
+      }
+    }
+  }
+  return true;
+}
+
+void SygusUnif::staticLearnRedundantOps(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 SygusUnif::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 SygusUnif::addEnumeratedValue(Node x, Node v, std::vector<Node>& lems)
+{
+  std::map<Node, EnumInfo>::iterator it = d_einfo.find(x);
+  Assert(it != d_einfo.end());
+  Assert(
+      std::find(it->second.d_enum_vals.begin(), it->second.d_enum_vals.end(), v)
+      == it->second.d_enum_vals.end());
+  Node c = it->second.d_parent_candidate;
+  // The explanation for why the current value should be excluded in future
+  // iterations.
+  Node exp_exc;
+
+  std::map<Node, CandidateInfo>::iterator itc = d_cinfo.find(c);
+  Assert(itc != d_cinfo.end());
+  TypeNode xtn = x.getType();
+  Node bv = d_tds->sygusToBuiltin(v, xtn);
+  std::map<Node, std::vector<std::vector<Node> > >::iterator itx =
+      d_examples.find(c);
+  std::map<Node, std::vector<Node> >::iterator itxo = d_examples_out.find(c);
+  Assert(itx != d_examples.end());
+  Assert(itxo != d_examples_out.end());
+  Assert(itx->second.size() == itxo->second.size());
+  std::vector<Node> base_results;
+  // compte the results
+  for (unsigned j = 0, size = itx->second.size(); j < size; j++)
+  {
+    Node res = d_tds->evaluateBuiltin(xtn, bv, itx->second[j]);
+    Trace("sygus-pbe-enum-debug")
+        << "...got res = " << res << " from " << bv << std::endl;
+    base_results.push_back(res);
+  }
+  // is it excluded for domain-specific reason?
+  std::vector<Node> exp_exc_vec;
+  if (getExplanationForEnumeratorExclude(
+          c, x, v, base_results, it->second, exp_exc_vec))
+  {
+    Assert(!exp_exc_vec.empty());
+    exp_exc = exp_exc_vec.size() == 1
+                  ? exp_exc_vec[0]
+                  : NodeManager::currentNM()->mkNode(AND, exp_exc_vec);
+    Trace("sygus-pbe-enum")
+        << "  ...fail : term is excluded (domain-specific)" << std::endl;
+  }
+  else
+  {
+    // notify all slaves
+    Assert(!it->second.d_enum_slave.empty());
+    // explanation for why this value should be excluded
+    for (unsigned s = 0; s < it->second.d_enum_slave.size(); s++)
+    {
+      Node xs = it->second.d_enum_slave[s];
+      std::map<Node, EnumInfo>::iterator itv = d_einfo.find(xs);
+      Assert(itv != d_einfo.end());
+      Trace("sygus-pbe-enum") << "Process " << xs << " from " << s << std::endl;
+      // bool prevIsCover = false;
+      if (itv->second.getRole() == enum_io)
+      {
+        Trace("sygus-pbe-enum") << "   IO-Eval of ";
+        // prevIsCover = itv->second.isFeasible();
+      }
+      else
+      {
+        Trace("sygus-pbe-enum") << "Evaluation of ";
+      }
+      Trace("sygus-pbe-enum") << xs << " : ";
+      // evaluate all input/output examples
+      std::vector<Node> results;
+      Node templ = itv->second.d_template;
+      TNode templ_var = itv->second.d_template_arg;
+      std::map<Node, bool> cond_vals;
+      for (unsigned j = 0, size = base_results.size(); j < size; j++)
+      {
+        Node res = base_results[j];
+        Assert(res.isConst());
+        if (!templ.isNull())
+        {
+          TNode tres = res;
+          res = templ.substitute(templ_var, res);
+          res = Rewriter::rewrite(res);
+          Assert(res.isConst());
+        }
+        Node resb;
+        if (itv->second.getRole() == enum_io)
+        {
+          Node out = itxo->second[j];
+          Assert(out.isConst());
+          resb = res == out ? d_true : d_false;
+        }
+        else
+        {
+          resb = res;
+        }
+        cond_vals[resb] = true;
+        results.push_back(resb);
+        if (Trace.isOn("sygus-pbe-enum"))
+        {
+          if (resb.getType().isBoolean())
+          {
+            Trace("sygus-pbe-enum") << (resb == d_true ? "1" : "0");
+          }
+          else
+          {
+            Trace("sygus-pbe-enum") << "?";
+          }
+        }
+      }
+      bool keep = false;
+      if (itv->second.getRole() == enum_io)
+      {
+        // latter is the degenerate case of no examples
+        if (cond_vals.find(d_true) != cond_vals.end() || cond_vals.empty())
+        {
+          // check subsumbed/subsuming
+          std::vector<Node> subsume;
+          if (cond_vals.find(d_false) == cond_vals.end())
+          {
+            // it is the entire solution, we are done
+            Trace("sygus-pbe-enum")
+                << "  ...success, full solution added to PBE pool : "
+                << d_tds->sygusToBuiltin(v) << std::endl;
+            if (!itv->second.isSolved())
+            {
+              itv->second.setSolved(v);
+              // it subsumes everything
+              itv->second.d_term_trie.clear();
+              itv->second.d_term_trie.addTerm(v, results, true, subsume);
+            }
+            keep = true;
+          }
+          else
+          {
+            Node val =
+                itv->second.d_term_trie.addTerm(v, results, true, subsume);
+            if (val == v)
+            {
+              Trace("sygus-pbe-enum") << "  ...success";
+              if (!subsume.empty())
+              {
+                itv->second.d_enum_subsume.insert(
+                    itv->second.d_enum_subsume.end(),
+                    subsume.begin(),
+                    subsume.end());
+                Trace("sygus-pbe-enum")
+                    << " and subsumed " << subsume.size() << " terms";
+              }
+              Trace("sygus-pbe-enum")
+                  << "!   add to PBE pool : " << d_tds->sygusToBuiltin(v)
+                  << std::endl;
+              keep = true;
+            }
+            else
+            {
+              Assert(subsume.empty());
+              Trace("sygus-pbe-enum") << "  ...fail : subsumed" << std::endl;
+            }
+          }
+        }
+        else
+        {
+          Trace("sygus-pbe-enum")
+              << "  ...fail : it does not satisfy examples." << std::endl;
+        }
+      }
+      else
+      {
+        // must be unique up to examples
+        Node val = itv->second.d_term_trie.addCond(v, results, true);
+        if (val == v)
+        {
+          Trace("sygus-pbe-enum") << "  ...success!   add to PBE pool : "
+                                  << d_tds->sygusToBuiltin(v) << std::endl;
+          keep = true;
+        }
+        else
+        {
+          Trace("sygus-pbe-enum")
+              << "  ...fail : term is not unique" << std::endl;
+        }
+        itc->second.d_cond_count++;
+      }
+      if (keep)
+      {
+        // notify the parent to retry the build of PBE
+        itc->second.d_check_sol = true;
+        itv->second.addEnumValue(this, v, results);
+      }
+    }
+  }
+
+  // exclude this value on subsequent iterations
+  if (exp_exc.isNull())
+  {
+    // if we did not already explain why this should be excluded, use default
+    exp_exc = d_tds->getExplain()->getExplanationForEquality(x, v);
+  }
+  exp_exc = exp_exc.negate();
+  Trace("sygus-pbe-enum-lemma")
+      << "SygusUnif : enumeration exclude lemma : " << exp_exc << std::endl;
+  lems.push_back(exp_exc);
+}
+
+bool SygusUnif::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 SygusUnif::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;
+      }
+    }
+    /* FIXME
+    if (!cmp_indices.empty())
+    {
+      // we check invariance with respect to a negative contains test
+      NegContainsSygusInvarianceTest ncset;
+      ncset.init(d_parent, x, itxo->second, cmp_indices);
+      // 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 SygusUnif::EnumInfo::addEnumValue(SygusUnif* 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);
+}
+
+void SygusUnif::EnumInfo::initialize(Node c, EnumRole role)
+{
+  d_parent_candidate = c;
+  d_role = role;
+}
+
+void SygusUnif::EnumInfo::setSolved(Node slv) { d_enum_solved = slv; }
+
+void SygusUnif::CandidateInfo::initialize(Node c)
+{
+  d_this_candidate = c;
+  d_root = c.getType();
+}
+
+void SygusUnif::CandidateInfo::initializeType(TypeNode tn)
+{
+  d_tinfo[tn].d_this_type = tn;
+  d_tinfo[tn].d_parent = this;
+}
+
+Node SygusUnif::CandidateInfo::getRootEnumerator()
+{
+  std::map<EnumRole, Node>::iterator it = d_tinfo[d_root].d_enum.find(enum_io);
+  Assert(it != d_tinfo[d_root].d_enum.end());
+  return it->second;
+}
+
+Node SygusUnif::constructBestSolvedTerm(std::vector<Node>& solved,
+                                        UnifContext& x)
+{
+  Assert(!solved.empty());
+  return solved[0];
+}
+
+Node SygusUnif::constructBestStringSolvedTerm(std::vector<Node>& solved,
+                                              UnifContext& x)
+{
+  Assert(!solved.empty());
+  return solved[0];
+}
+
+Node SygusUnif::constructBestSolvedConditional(std::vector<Node>& solved,
+                                               UnifContext& x)
+{
+  Assert(!solved.empty());
+  return solved[0];
+}
+
+Node SygusUnif::constructBestConditional(std::vector<Node>& conds,
+                                         UnifContext& x)
+{
+  Assert(!conds.empty());
+  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 SygusUnif::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 SygusUnif::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(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()
+               && !snode.d_strats[sindex]->isValid(this, x))
+        {
+          sindex++;
+        }
+        // if we found a eligible strategy
+        if (sindex < snode.d_strats.size())
+        {
+          etis = snode.d_strats[sindex];
+        }
+      }
+    }
+    if (etis != nullptr)
+    {
+      StrategyType strat = etis->d_this;
+      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(
+                        einfo_child.d_enum_vals_res[k], branch_pol, solved);
+                    Trace("sygus-pbe-dt-debug2")
+                        << "  reg : PBE: " << d_tds->sygusToBuiltin(cond)
+                        << " has " << solved.size() << " solutions in branch "
+                        << i << std::endl;
+                    if (!solved.empty())
+                    {
+                      Node slv = constructBestSolvedTerm(solved, x);
+                      Trace("sygus-pbe-dt-debug2")
+                          << "  reg : PBE: ..." << d_tds->sygusToBuiltin(slv)
+                          << " is a solution under branch " << i;
+                      Trace("sygus-pbe-dt-debug2")
+                          << " of condition " << d_tds->sygusToBuiltin(cond)
+                          << std::endl;
+                      x.d_uinfo[ce].d_look_ahead_sols[cond][i] = slv;
+                    }
+                  }
+                }
+              }
+            }
+
+            // get the conditionals in the current context : they must be
+            // distinguishable
+            std::map<int, std::vector<Node> > possible_cond;
+            std::map<Node, int> solved_cond;  // stores branch
+            einfo_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond);
+
+            std::map<int, std::vector<Node> >::iterator itpc =
+                possible_cond.find(0);
+            if (itpc != possible_cond.end())
+            {
+              if (Trace.isOn("sygus-pbe-dt-debug"))
+              {
+                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 SygusUnif::EnumTypeInfoStrat::isValid(SygusUnif* pbe, UnifContext& x)
+{
+  if ((x.d_has_string_pos == role_string_prefix
+       && d_this == strat_CONCAT_SUFFIX)
+      || (x.d_has_string_pos == role_string_suffix
+          && d_this == strat_CONCAT_PREFIX))
+  {
+    return false;
+  }
+  return true;
+}
+
+SygusUnif::StrategyNode::~StrategyNode()
+{
+  for (unsigned j = 0, size = d_strats.size(); j < size; j++)
+  {
+    delete d_strats[j];
+  }
+  d_strats.clear();
+}
+
+void SygusUnif::indent(const char* c, int ind)
+{
+  if (Trace.isOn(c))
+  {
+    for (int i = 0; i < ind; i++)
+    {
+      Trace(c) << "  ";
+    }
+  }
+}
+
+void SygusUnif::print_val(const char* c, std::vector<Node>& vals, bool pol)
+{
+  if (Trace.isOn(c))
+  {
+    for (unsigned i = 0; i < vals.size(); i++)
+    {
+      Trace(c) << ((pol ? vals[i].getConst<bool>() : !vals[i].getConst<bool>())
+                       ? "1"
+                       : "0");
+    }
+  }
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h
new file mode 100644
index 000000000..68ed442a8
--- /dev/null
+++ b/src/theory/quantifiers/sygus/sygus_unif.h
@@ -0,0 +1,758 @@
+/*********************                                                        */
+/*! \file sygus_unif.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief sygus_unif
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H
+
+#include <map>
+#include "expr/node.h"
+#include "theory/quantifiers_engine.h"
+
+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
+ * SygusUnif::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 SygusUnif;
+
+/** Unification context
+  *
+  * This class maintains state information during calls to
+  * SygusUnif::constructSolution, which implements unification-based
+  * approaches for construction solutions to synthesis conjectures.
+  */
+class UnifContext
+{
+ public:
+  UnifContext();
+  /** this intiializes this context for function-to-synthesize c */
+  void initialize(SygusUnif* 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(SygusUnif* 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(SygusUnif* 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(SygusUnif* 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(SygusUnif* 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(SygusUnif* pbe,
+                      const std::vector<String>& ex_vals,
+                      const std::vector<Node>& vals);
+  //----------end for CONCAT strategies
+
+  /** is return value modified?
+  *
+  * This returns true if we are currently in a state where the return value
+  * of the solution has been modified, e.g. by a previous node that solved
+  * for a prefix.
+  */
+  bool isReturnValueModified();
+  /** visited role
+  *
+  * This is the current set of enumerator/node role pairs we are currently
+  * visiting. This set is cleared when the context is updated.
+  */
+  std::map<Node, std::map<NodeRole, bool> > d_visit_role;
+
+  /** unif context enumerator information */
+  class UEnumInfo
+  {
+   public:
+    UEnumInfo() {}
+    /** map from conditions and branch positions to a solved node
+    *
+    * For example, if we have:
+    *   f( 1 ) = 2 ^ f( 3 ) = 4 ^ f( -1 ) = 1
+    * Then, valid entries in this map is:
+    *   d_look_ahead_sols[x>0][1] = x+1
+    *   d_look_ahead_sols[x>0][2] = 1
+    * For the first entry, notice that  for all input examples such that x>0
+    * evaluates to true, which are (1) and (3), we have that their output
+    * values for x+1 under the substitution that maps x to the input value,
+    * resulting in 2 and 4, are equal to the output value for the respective
+    * pairs.
+    */
+    std::map<Node, std::map<unsigned, Node> > d_look_ahead_sols;
+  };
+  /** map from enumerators to the above info class */
+  std::map<Node, UEnumInfo> d_uinfo;
+
+ private:
+  /** true and false nodes */
+  Node d_true;
+  Node d_false;
+};
+
+/** Subsumption trie
+*
+* This class manages a set of terms for a PBE sygus enumerator.
+*
+* In PBE sygus, we are interested in, for each term t, the set of I/O examples
+* that it satisfies, which can be represented by a vector of Booleans.
+* For example, given conjecture:
+*   f( 1 ) = 2 ^ f( 3 ) = 4 ^ f( -1 ) = 1 ^ f( 5 ) = 5
+* If solutions for f are of the form (lambda x. [term]), then:
+*   Term x satisfies 0001,
+*   Term x+1 satisfies 1100,
+*   Term 2 satisfies 0100.
+* Above, term 2 is subsumed by term x+1, since the set of I/O examples that
+* x+1 satisfies are a superset of those satisfied by 2.
+*/
+class SubsumeTrie
+{
+ public:
+  SubsumeTrie() {}
+  /**
+  * Adds term t to the trie, removes all terms that are subsumed by t from the
+  * trie and adds them to subsumed. The set of I/O examples that t satisfies
+  * is given by (pol ? vals : !vals).
+  */
+  Node addTerm(Node t,
+               const std::vector<Node>& vals,
+               bool pol,
+               std::vector<Node>& subsumed);
+  /**
+  * Adds term c to the trie, without calculating/updating based on
+  * subsumption. This is useful for using this class to store conditionals
+  * in ITE strategies, where any conditional whose set of vals is unique
+  * (as opposed to not subsumed) is useful.
+  */
+  Node addCond(Node c, const std::vector<Node>& vals, bool pol);
+  /**
+    * Returns the set of terms that are subsumed by (pol ? vals : !vals).
+    */
+  void getSubsumed(const std::vector<Node>& vals,
+                   bool pol,
+                   std::vector<Node>& subsumed);
+  /**
+    * Returns the set of terms that subsume (pol ? vals : !vals). This
+    * is for instance useful when determining whether there exists a term
+    * that satisfies all active examples in the decision tree learning
+    * algorithm.
+    */
+  void getSubsumedBy(const std::vector<Node>& vals,
+                     bool pol,
+                     std::vector<Node>& subsumed_by);
+  /**
+  * Get the leaves of the trie, which we store in the map v.
+  * v[-1] stores the children that always evaluate to !pol,
+  * v[1] stores the children that always evaluate to pol,
+  * v[0] stores the children that both evaluate to true and false for at least
+  * one example.
+  */
+  void getLeaves(const std::vector<Node>& vals,
+                 bool pol,
+                 std::map<int, std::vector<Node> >& v);
+  /** is this trie empty? */
+  bool isEmpty() { return d_term.isNull() && d_children.empty(); }
+  /** clear this trie */
+  void clear()
+  {
+    d_term = Node::null();
+    d_children.clear();
+  }
+
+ private:
+  /** the term at this node */
+  Node d_term;
+  /** the children nodes of this trie */
+  std::map<Node, SubsumeTrie> d_children;
+  /** helper function for above functions */
+  Node addTermInternal(Node t,
+                       const std::vector<Node>& vals,
+                       bool pol,
+                       std::vector<Node>& subsumed,
+                       bool spol,
+                       unsigned index,
+                       int status,
+                       bool checkExistsOnly,
+                       bool checkSubsume);
+  /** helper function for above functions */
+  void getLeavesInternal(const std::vector<Node>& vals,
+                         bool pol,
+                         std::map<int, std::vector<Node> >& v,
+                         unsigned index,
+                         int status);
+};
+
+/** Sygus unification utility
+ *
+ * This utility implements synthesis-by-unification style approaches for a
+ * single function to synthesize f.
+ * These approaches include a combination of:
+ * (1) Decision tree learning, inspired by Alur et al TACAS 2017,
+ * (2) Divide-and-conquer via string concatenation.
+ *
+ * This class maintains:
+ * (1) A "strategy tree" based on the syntactic restrictions for f that is
+ * constructed during initialize,
+ * (2) A set of input/output examples that are the specification for f. This
+ * can be updated via calls to resetExmaples/addExamples,
+ * (3) A set of terms that have been enumerated for enumerators. This can be
+ * updated via calls to notifyEnumeration.
+ *
+ * Based on the above, solutions can be constructed via calls to
+ * constructSolution.
+ */
+class SygusUnif
+{
+  friend class UnifContext;
+
+ public:
+  SygusUnif(QuantifiersEngine* qe);
+  ~SygusUnif();
+
+  /** initialize
+   *
+   * This initializes this class with function-to-synthesize f. We also call
+   * f the candidate variable.
+   *
+   * This call constructs a set of enumerators for the relevant subfields of
+   * the grammar of f and adds them to enums. These enumerators are those that
+   * should be later given to calls to notifyEnumeration below.
+   *
+   * This also may result in lemmas being added to lemmas,
+   * which correspond to static symmetry breaking predicates (for example,
+   * those that exclude ITE from enumerators whose role is enum_io when the
+   * strategy is ITE_strat).
+   */
+  void initialize(Node f, std::vector<Node>& enums, std::vector<Node>& lemmas);
+  /** reset examples
+   *
+   * Reset the specification for f.
+   *
+   * Notice that this does not reset the
+   */
+  void resetExamples();
+  /** add example
+   *
+   * This adds input -> output to the specification for f. The arity of
+   * input should be equal to the number of arguments in the sygus variable
+   * list of the grammar of f. That is, if we are searching for solutions for f
+   * of the form (lambda v1...vn. t), then the arity of input should be n.
+   */
+  void addExample(const std::vector<Node>& input, Node output);
+
+  /**
+   * Notify that the value v has been enumerated for enumerator e. This call
+   * will add lemmas L to lemmas such that L entails e^M != v for all future
+   * models M.
+   */
+  void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas);
+  /** construct solution
+   *
+   * This attempts to construct a solution based on the current set of
+   * enumerated values. Returns null if it cannot (for example, if the
+   * set of enumerated values is insufficient, or if a non-deterministic
+   * strategy aborts).
+   */
+  Node constructSolution();
+
+  //-----------------------debug printing
+  /** print ind indentations on trace c */
+  static void indent(const char* c, int ind);
+  /** print (pol ? vals : !vals) as a bit-string on trace c  */
+  static void print_val(const char* c,
+                        std::vector<Node>& vals,
+                        bool pol = true);
+  //-----------------------end debug printing
+ private:
+  /** reference to quantifier engine */
+  QuantifiersEngine* d_qe;
+  /** sygus term database of d_qe */
+  quantifiers::TermDbSygus* d_tds;
+  /** true and false nodes */
+  Node d_true;
+  Node d_false;
+  /** input of I/O examples */
+  std::map<Node, std::vector<std::vector<Node> > > d_examples;
+  /** output of I/O examples */
+  std::map<Node, std::vector<Node> > d_examples_out;
+
+  //------------------------------ representation of a enumeration strategy
+  /**
+  * This class stores information regarding an enumerator, including:
+  * - Information regarding the role of this enumerator (see EnumRole), its
+  * parent, whether it is templated, its slave enumerators, and so on, and
+  * - A database of values that have been enumerated for this enumerator.
+  *
+  * We say an enumerator is a master enumerator if it is the variable that
+  * we use to enumerate values for its sort. Master enumerators may have
+  * (possibly multiple) slave enumerators, stored in d_enum_slave. We make
+  * the first enumerator for each type a master enumerator, and any additional
+  * ones slaves of it.
+  */
+  class EnumInfo
+  {
+   public:
+    EnumInfo() : d_role(enum_io), d_is_conditional(false) {}
+    /** initialize this class
+    *
+    * c is the parent function-to-synthesize
+    * role is the "role" the enumerator plays in the high-level strategy,
+    *   which is one of enum_* above.
+    */
+    void initialize(Node c, EnumRole role);
+    /** is this enumerator associated with a template? */
+    bool isTemplated() { return !d_template.isNull(); }
+    /** set conditional
+      *
+      * This flag is set to true if this enumerator may not apply to all
+      * input/output examples. For example, if this enumerator is used
+      * as an output value beneath a conditional in an instance of strat_ITE,
+      * then this enumerator is conditional.
+      */
+    void setConditional() { d_is_conditional = true; }
+    /** is conditional */
+    bool isConditional() { return d_is_conditional; }
+    /** get the role of this enumerator */
+    EnumRole getRole() { return d_role; }
+    /**
+    * The candidate variable that this enumerator is for (see sygus_pbe.h).
+    */
+    Node d_parent_candidate;
+    /** enumerator template
+    *
+    * If d_template non-null, enumerated values V are immediately transformed to
+    * d_template { d_template_arg -> V }.
+    */
+    Node d_template;
+    Node d_template_arg;
+    /**
+    * Slave enumerators of this enumerator. These are other enumerators that
+    * have the same type, but a different role in the strategy tree. We
+    * generally
+    * only use one enumerator per type, and hence these slaves are notified when
+    * values are enumerated for this enumerator.
+    */
+    std::vector<Node> d_enum_slave;
+
+    //---------------------------enumerated values
+    /**
+    * Notify this class that the term v has been enumerated for this enumerator.
+    * Its evaluation under the set of examples in pbe are stored in results.
+    */
+    void addEnumValue(SygusUnif* pbe, Node v, std::vector<Node>& results);
+    /**
+    * Notify this class that slv is the complete solution to the synthesis
+    * conjecture. This occurs rarely, for instance, when during an ITE strategy
+    * we find that a single enumerated term covers all examples.
+    */
+    void setSolved(Node slv);
+    /** Have we been notified that a complete solution exists? */
+    bool isSolved() { return !d_enum_solved.isNull(); }
+    /** Get the complete solution to the synthesis conjecture. */
+    Node getSolved() { return d_enum_solved; }
+    /** Values that have been enumerated for this enumerator */
+    std::vector<Node> d_enum_vals;
+    /**
+      * This either stores the values of f( I ) for inputs
+      * or the value of f( I ) = O if d_role==enum_io
+      */
+    std::vector<std::vector<Node> > d_enum_vals_res;
+    /**
+    * The set of values in d_enum_vals that have been "subsumed" by others
+    * (see SubsumeTrie for explanation of subsumed).
+    */
+    std::vector<Node> d_enum_subsume;
+    /** Map from values to their index in d_enum_vals. */
+    std::map<Node, unsigned> d_enum_val_to_index;
+    /**
+    * A subsumption trie containing the values in d_enum_vals. Depending on the
+    * role of this enumerator, values may either be added to d_term_trie with
+    * subsumption (if role=enum_io), or without (if role=enum_ite_condition or
+    * enum_concat_term).
+    */
+    SubsumeTrie d_term_trie;
+    //---------------------------end enumerated values
+   private:
+    /**
+      * Whether an enumerated value for this conjecture has solved the entire
+      * conjecture.
+      */
+    Node d_enum_solved;
+    /** the role of this enumerator (one of enum_* above). */
+    EnumRole d_role;
+    /** is this enumerator conditional */
+    bool d_is_conditional;
+  };
+  /** maps enumerators to the information above */
+  std::map<Node, EnumInfo> d_einfo;
+
+  class CandidateInfo;
+  class EnumTypeInfoStrat;
+
+  /** represents a node in the strategy graph
+   *
+   * It contains a list of possible strategies which are tried during calls
+   * to constructSolution.
+   */
+  class StrategyNode
+  {
+   public:
+    StrategyNode() {}
+    ~StrategyNode();
+    /** the set of strategies to try at this node in the strategy graph */
+    std::vector<EnumTypeInfoStrat*> d_strats;
+  };
+
+  /** stores enumerators and strategies for a SyGuS datatype type */
+  class EnumTypeInfo
+  {
+   public:
+    EnumTypeInfo() : d_parent(NULL) {}
+    /** the parent candidate info (see below) */
+    CandidateInfo* d_parent;
+    /** the type that this information is for */
+    TypeNode d_this_type;
+    /** map from enum roles to enumerators for this type */
+    std::map<EnumRole, Node> d_enum;
+    /** map from node roles to strategy nodes */
+    std::map<NodeRole, StrategyNode> d_snodes;
+  };
+
+  /** stores strategy and enumeration information for a function-to-synthesize
+   */
+  class CandidateInfo
+  {
+   public:
+    CandidateInfo() : d_check_sol(false), d_cond_count(0) {}
+    Node d_this_candidate;
+    /**
+     * The root sygus datatype for the function-to-synthesize,
+     * which encodes the overall syntactic restrictions on the space
+     * of solutions.
+     */
+    TypeNode d_root;
+    /** Info for sygus datatype type occurring in a field of d_root */
+    std::map<TypeNode, EnumTypeInfo> d_tinfo;
+    /** list of all enumerators for the function-to-synthesize */
+    std::vector<Node> d_esym_list;
+    /**
+     * Maps sygus datatypes to their search enumerator. This is the (single)
+     * enumerator of that type that we enumerate values for.
+     */
+    std::map<TypeNode, Node> d_search_enum;
+    bool d_check_sol;
+    unsigned d_cond_count;
+    Node d_solution;
+    void initialize(Node c);
+    void initializeType(TypeNode tn);
+    Node getRootEnumerator();
+  };
+  /** the candidate for this class */
+  Node d_candidate;
+  /** maps a function-to-synthesize to the above information */
+  std::map<Node, CandidateInfo> d_cinfo;
+
+  //------------------------------ representation of an enumeration strategy
+  /** add enumerated value
+   *
+   * We have enumerated the value v for x. This function adds x->v to the
+   * relevant data structures that are used for strategy-specific construction
+   * of solutions when necessary, and returns a set of lemmas, which are added
+   * to the input argument lems. These lemmas are used to rule out models where
+   * x = v, to force that a new value is enumerated for x.
+   */
+  void addEnumeratedValue(Node x, Node v, std::vector<Node>& lems);
+  /** domain-specific enumerator exclusion techniques
+   *
+   * Returns true if the value v for x can be excluded based on a
+   * domain-specific exclusion technique like the ones below.
+   *
+   * c : the candidate variable that x is enumerating for,
+   * results : the values of v under the input examples of c,
+   * ei : the enumerator information for x,
+   * exp : if this function returns true, then exp contains a (possibly
+   * generalize) explanation for why v can be excluded.
+   */
+  bool getExplanationForEnumeratorExclude(Node c,
+                                          Node x,
+                                          Node v,
+                                          std::vector<Node>& results,
+                                          EnumInfo& ei,
+                                          std::vector<Node>& exp);
+  /** returns true if we can exlude values of x based on negative str.contains
+   *
+   * Values v for x may be excluded if we realize that the value of v under the
+   * substitution for some input example will never be contained in some output
+   * example. For details on this technique, see NegContainsSygusInvarianceTest
+   * in sygus_invariance.h.
+   *
+   * This function depends on whether x is being used to enumerate values
+   * for any node that is conditional in the strategy graph. For example,
+   * nodes that are children of ITE strategy nodes are conditional. If any node
+   * is conditional, then this function returns false.
+   */
+  bool useStrContainsEnumeratorExclude(Node x, EnumInfo& ei);
+  /** cache for the above function */
+  std::map<Node, bool> d_use_str_contains_eexc;
+
+  //------------------------------ strategy registration
+  /** collect enumerator types
+   *
+   * This builds the strategy for enumerated values of type tn for the given
+   * role of nrole, for solutions to function-to-synthesize c.
+   */
+  void collectEnumeratorTypes(Node c, TypeNode tn, NodeRole nrole);
+  /** register enumerator
+   *
+   * This registers that et is an enumerator for function-to-synthesize c
+   * of type tn, having enumerator role enum_role.
+   *
+   * inSearch is whether we will enumerate values based on this enumerator.
+   * A strategy node is represented by a (enumerator, node role) pair. Hence,
+   * we may use enumerators for which this flag is false to represent strategy
+   * nodes that have child strategies.
+   */
+  void registerEnumerator(
+      Node et, Node c, TypeNode tn, EnumRole enum_role, bool inSearch);
+  /** infer template */
+  bool inferTemplate(unsigned k,
+                     Node n,
+                     std::map<Node, unsigned>& templ_var_index,
+                     std::map<unsigned, unsigned>& templ_injection);
+  /** static learn redundant operators
+   *
+   * This learns static lemmas for pruning enumerative space based on the
+   * strategy for the function-to-synthesize c, and stores these into lemmas.
+   */
+  void staticLearnRedundantOps(Node c, std::vector<Node>& lemmas);
+  /** helper for static learn redundant operators
+   *
+   * (e, nrole) specify the strategy node in the graph we are currently
+   * analyzing, visited stores the nodes we have already visited.
+   *
+   * This method builds the mapping needs_cons, which maps (master) enumerators
+   * to a map from the constructors that it needs.
+   *
+   * ind is the depth in the strategy graph we are at (for debugging).
+   *
+   * isCond is whether the current enumerator is conditional (beneath a
+   * conditional of an strat_ITE strategy).
+   */
+  void staticLearnRedundantOps(
+      Node c,
+      Node e,
+      NodeRole nrole,
+      std::map<Node, std::map<NodeRole, bool> >& visited,
+      std::map<Node, std::map<unsigned, bool> >& needs_cons,
+      int ind,
+      bool isCond);
+  //------------------------------ end strategy registration
+
+  /** helper function for construct solution.
+   *
+   * Construct a solution based on enumerator e for function-to-synthesize c
+   * with node role nrole in context x.
+   *
+   * ind is the term depth of the context (for debugging).
+   */
+  Node constructSolution(
+      Node c, Node e, NodeRole nrole, UnifContext& x, int ind);
+  /** Heuristically choose the best solved term from solved in context x,
+   * currently return the first. */
+  Node constructBestSolvedTerm(std::vector<Node>& solved, UnifContext& x);
+  /** Heuristically choose the best solved string term  from solved in context
+   * x, currently  return the first. */
+  Node constructBestStringSolvedTerm(std::vector<Node>& solved, UnifContext& x);
+  /** Heuristically choose the best solved conditional term  from solved in
+   * context x, currently random */
+  Node constructBestSolvedConditional(std::vector<Node>& solved,
+                                      UnifContext& x);
+  /** Heuristically choose the best conditional term  from conds in context x,
+   * currently random */
+  Node constructBestConditional(std::vector<Node>& conds, UnifContext& x);
+  /** Heuristically choose the best string to concatenate from strs to the
+  * solution in context x, currently random
+  * incr stores the vector of indices that are incremented by this solution in
+  * example outputs.
+  * total_inc[x] is the sum of incr[x] for each x in strs.
+  */
+  Node constructBestStringToConcat(std::vector<Node> strs,
+                                   std::map<Node, unsigned> total_inc,
+                                   std::map<Node, std::vector<unsigned> > incr,
+                                   UnifContext& x);
+  //------------------------------ end constructing solutions
+
+  /** represents a strategy for a SyGuS datatype type
+   *
+   * This represents a possible strategy to apply when processing a strategy
+   * node in constructSolution. When applying the strategy represented by this
+   * class, we may make recursive calls to the children of the strategy,
+   * given in d_cenum. If all recursive calls to constructSolution for these
+   * children are successful, say:
+   *   constructSolution( c, d_cenum[1], ... ) = t1,
+   *    ...,
+   *   constructSolution( c, d_cenum[n], ... ) = tn,
+   * Then, the solution returned by this strategy is
+   *   d_sol_templ * { d_sol_templ_args -> (t1,...,tn) }
+   * where * is application of substitution.
+   */
+  class EnumTypeInfoStrat
+  {
+   public:
+    /** the type of strategy this represents */
+    StrategyType d_this;
+    /** the sygus datatype constructor that induced this strategy
+     *
+     * For example, this may be a sygus datatype whose sygus operator is ITE,
+     * if the strategy type above is strat_ITE.
+     */
+    Node d_cons;
+    /** children of this strategy */
+    std::vector<std::pair<Node, NodeRole> > d_cenum;
+    /** the arguments for the (templated) solution */
+    std::vector<Node> d_sol_templ_args;
+    /** the template for the solution */
+    Node d_sol_templ;
+    /** Returns true if argument is valid strategy in context x */
+    bool isValid(SygusUnif* pbe, UnifContext& x);
+  };
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */