Sygus process conjecture (#1286)

* Initial infrastructure for static preprocessing for sygus conjectures.

* Initial infrastructure.

* Minor change in terminology, move enumerator to synth-fun mapping to sygus term database, minor fix and add documentation to NegContainsInvarianceTest.

* Clang format

* Fixing comments, more initial infrastructure.

* More

* Minor

* New clang format.

* Address review.

11 files changed, 725 insertions, 264 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index b05a3503c..0bcd35215 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -420,6 +420,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/rewrite_engine.h \
 	theory/quantifiers/sygus_grammar_cons.cpp \
 	theory/quantifiers/sygus_grammar_cons.h \
+	theory/quantifiers/sygus_process_conj.cpp \
+	theory/quantifiers/sygus_process_conj.h \
 	theory/quantifiers/symmetry_breaking.cpp \
 	theory/quantifiers/symmetry_breaking.h \
 	theory/quantifiers/term_database.cpp \
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 4999114eb..f27a852d9 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -262,7 +262,7 @@ void SygusSymBreakNew::registerTerm( Node n, std::vector< Node >& lemmas ) {
       registerSizeTerm( n, lemmas );
       if( d_register_st[n] ){
         d_term_to_anchor[n] = n;
-        d_term_to_anchor_conj[n] = d_tds->getConjectureFor(n);
+        d_term_to_anchor_conj[n] = d_tds->getConjectureForEnumerator(n);
         // this assertion fails if we have a sygus term in the search that is unmeasured
         Assert(d_term_to_anchor_conj[n] != NULL);
         d = 0;
@@ -361,29 +361,54 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std:
   Trace("sygus-sb-fair-debug") << "Tester " << exp << " is for depth " << d << " term in search size " << ssz << std::endl;
   //Assert( d<=ssz );
   if( options::sygusSymBreakLazy() ){
+    // dynamic symmetry breaking
     addSymBreakLemmasFor( ntn, n, d, lemmas );
   }
-     
-  // process simple symmetry breaking
+
   unsigned max_depth = ssz>=d ? ssz-d : 0;
   unsigned min_depth = d_simple_proc[exp];
   if( min_depth<=max_depth ){
     TNode x = getFreeVar( ntn );
-    Node rlv = getRelevancyCondition( n );
-    for( unsigned d=0; d<=max_depth; d++ ){
-      Node simple_sb_pred = getSimpleSymBreakPred( ntn, tindex, d );
-      if( !simple_sb_pred.isNull() ){
-        simple_sb_pred = simple_sb_pred.substitute( x, n );
-        if( !rlv.isNull() ){
-          simple_sb_pred = NodeManager::currentNM()->mkNode( kind::OR, rlv.negate(), simple_sb_pred ); 
+    std::vector<Node> sb_lemmas;
+    for (unsigned ds = 0; ds <= max_depth; ds++)
+    {
+      // static conjecture-independent symmetry breaking
+      Node ipred = getSimpleSymBreakPred(ntn, tindex, ds);
+      if (!ipred.isNull())
+      {
+        sb_lemmas.push_back(ipred);
+      }
+      // static conjecture-dependent symmetry breaking
+      std::map<Node, quantifiers::CegConjecture*>::iterator itc =
+          d_term_to_anchor_conj.find(n);
+      if (itc != d_term_to_anchor_conj.end())
+      {
+        quantifiers::CegConjecture* conj = itc->second;
+        Assert(conj != NULL);
+        Node dpred = conj->getSymmetryBreakingPredicate(x, a, ntn, tindex, ds);
+        if (!dpred.isNull())
+        {
+          sb_lemmas.push_back(dpred);
         }
-        lemmas.push_back( simple_sb_pred ); 
       }
     }
+
+    // add the above symmetry breaking predicates to lemmas
+    Node rlv = getRelevancyCondition(n);
+    for (unsigned i = 0; i < sb_lemmas.size(); i++)
+    {
+      Node pred = sb_lemmas[i].substitute(x, n);
+      if (!rlv.isNull())
+      {
+        pred = NodeManager::currentNM()->mkNode(kind::OR, rlv.negate(), pred);
+      }
+      lemmas.push_back(pred);
+    }
   }
   d_simple_proc[exp] = max_depth + 1;
-  
-  // add back testers for the children if they exist
+
+  // now activate the children those testers were previously asserted in this
+  // context and are awaiting activation, if they exist.
   if( options::sygusSymBreakLazy() ){
     for( unsigned j=0; j<dt[tindex].getNumArgs(); j++ ){
       Node sel = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex].getSelectorInternal( ntn.toType(), j ) ), n );
@@ -1054,9 +1079,10 @@ void SygusSymBreakNew::registerSizeTerm( Node e, std::vector< Node >& lemmas ) {
     if( e.getType().isDatatype() ){
       const Datatype& dt = ((DatatypeType)(e.getType()).toType()).getDatatype();
       if( dt.isSygus() ){
-        if (d_tds->isMeasuredTerm(e)) {
+        if (d_tds->isEnumerator(e))
+        {
           d_register_st[e] = true;
-          Node ag = d_tds->getActiveGuardForMeasureTerm( e );
+          Node ag = d_tds->getActiveGuardForEnumerator(e);
           if( !ag.isNull() ){
             d_anchor_to_active_guard[e] = ag;
           }
@@ -1157,10 +1183,11 @@ unsigned SygusSymBreakNew::getSearchSizeForAnchor( Node a ) {
   Trace("sygus-sb-debug2") << "get search size for anchor : " << a << std::endl;
   std::map< Node, Node >::iterator it = d_anchor_to_measure_term.find( a );
   Assert( it!=d_anchor_to_measure_term.end() );
-  return getSearchSizeForMeasureTerm( it->second );
+  return getSearchSizeForMeasureTerm(it->second);
 }
 
-unsigned SygusSymBreakNew::getSearchSizeForMeasureTerm( Node m ) {
+unsigned SygusSymBreakNew::getSearchSizeForMeasureTerm(Node m)
+{
   Trace("sygus-sb-debug2") << "get search size for measure : " << m << std::endl;
   std::map< Node, SearchSizeInfo * >::iterator its = d_szinfo.find( m );
   Assert( its!=d_szinfo.end() );
@@ -1243,7 +1270,7 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) {
   }
   //register any measured terms that we haven't encountered yet (should only be invoked on first call to check
   std::vector< Node > mts;
-  d_tds->getMeasuredTerms( mts );
+  d_tds->getEnumerators(mts);
   for( unsigned i=0; i<mts.size(); i++ ){
     registerSizeTerm( mts[i], lemmas );
   }
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index bb83b4850..9cfa7355d 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -146,8 +146,9 @@ private:
   void registerMeasureTerm( Node m );
   unsigned getSearchSizeFor( Node n );
   unsigned getSearchSizeForAnchor( Node n );
-  unsigned getSearchSizeForMeasureTerm( Node m );
-private:
+  unsigned getSearchSizeForMeasureTerm(Node m);
+
+ private:
   unsigned processSelectorChain( Node n, std::map< TypeNode, Node >& top_level, 
                                  std::map< Node, unsigned >& tdepth, std::vector< Node >& lemmas );
   bool debugTesters( Node n, Node vn, int ind, std::vector< Node >& lemmas );
diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp
index a380dcbf2..7fcc3f2af 100644
--- a/src/theory/quantifiers/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/ce_guided_conjecture.cpp
@@ -48,12 +48,14 @@ CegConjecture::CegConjecture(QuantifiersEngine* qe)
   d_refine_count = 0;
   d_ceg_si = new CegConjectureSingleInv(qe, this);
   d_ceg_pbe = new CegConjecturePbe(qe, this);
+  d_ceg_proc = new CegConjectureProcess(qe);
   d_ceg_gc = new CegGrammarConstructor(qe);
 }
 
 CegConjecture::~CegConjecture() {
   delete d_ceg_si;
   delete d_ceg_pbe;
+  delete d_ceg_proc;
   delete d_ceg_gc;
 }
 
@@ -63,12 +65,16 @@ void CegConjecture::assign( Node q ) {
   Trace("cegqi") << "CegConjecture : assign : " << q << std::endl;
   d_quant = q;
 
+  // simplify the quantified formula based on the process utility
+  d_simp_quant = d_ceg_proc->simplify(d_quant);
+
   std::map< Node, Node > templates; 
   std::map< Node, Node > templates_arg;
   //register with single invocation if applicable
-  if( d_qe->getQuantAttributes()->isSygus( d_quant ) ){
-    d_ceg_si->initialize( d_quant );
-    q = d_ceg_si->getSimplifiedConjecture();
+  if (d_qe->getQuantAttributes()->isSygus(q))
+  {
+    d_ceg_si->initialize(d_simp_quant);
+    d_simp_quant = d_ceg_si->getSimplifiedConjecture();
     // carry the templates
     for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
       Node v = q[0][i];
@@ -81,11 +87,12 @@ void CegConjecture::assign( Node q ) {
   }
 
   // convert to deep embedding and finalize single invocation here
-  d_embed_quant = d_ceg_gc->process( q, templates, templates_arg );
+  d_embed_quant = d_ceg_gc->process(d_simp_quant, templates, templates_arg);
   Trace("cegqi") << "CegConjecture : converted to embedding : " << d_embed_quant << std::endl;
 
   // we now finalize the single invocation module, based on the syntax restrictions
-  if( d_qe->getQuantAttributes()->isSygus( d_quant ) ){
+  if (d_qe->getQuantAttributes()->isSygus(q))
+  {
     d_ceg_si->finishInit( d_ceg_gc->isSyntaxRestricted(), d_ceg_gc->hasSyntaxITE() );
   }
 
@@ -99,22 +106,25 @@ void CegConjecture::assign( Node q ) {
   Trace("cegqi") << "Base quantified formula is : " << d_embed_quant << std::endl;
   //construct base instantiation
   d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( d_embed_quant, vars, d_candidates ) );
-  
-  // register this term with sygus database
+  Trace("cegqi") << "Base instantiation is :      " << d_base_inst << std::endl;
+
+  // register this term with sygus database and other utilities that impact
+  // the enumerative sygus search
   std::vector< Node > guarded_lemmas;
   if( !isSingleInvocation() ){
+    d_ceg_proc->initialize(d_base_inst, d_candidates);
     if( options::sygusPbe() ){
-      d_ceg_pbe->initialize( d_base_inst, d_candidates, guarded_lemmas );
+      d_ceg_pbe->initialize(d_base_inst, d_candidates, guarded_lemmas);
     } else {
       for (unsigned i = 0; i < d_candidates.size(); i++) {
         Node e = d_candidates[i];
-        d_qe->getTermDatabaseSygus()->registerMeasuredTerm(e, this);
+        d_qe->getTermDatabaseSygus()->registerEnumerator(e, e, this);
       }
     }
   }
-  
-  Trace("cegqi") << "Base instantiation is :      " << d_base_inst << std::endl;
-  if( d_qe->getQuantAttributes()->isSygus( d_quant ) ){
+
+  if (d_qe->getQuantAttributes()->isSygus(q))
+  {
     collectDisjuncts( d_base_inst, d_base_disj );
     Trace("cegqi") << "Conjecture has " << d_base_disj.size() << " disjuncts." << std::endl;
     //store the inner variables for each disjunct
@@ -130,7 +140,9 @@ void CegConjecture::assign( Node q ) {
       }
     }
     d_syntax_guided = true;
-  }else if( d_qe->getQuantAttributes()->isSynthesis( d_quant ) ){
+  }
+  else if (d_qe->getQuantAttributes()->isSynthesis(q))
+  {
     d_syntax_guided = false;
   }else{
     Assert( false );
@@ -612,6 +624,33 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
   }
 }
 
+Node CegConjecture::getSymmetryBreakingPredicate(
+    Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth)
+{
+  std::vector<Node> sb_lemmas;
+
+  // based on simple preprocessing
+  Node ppred =
+      d_ceg_proc->getSymmetryBreakingPredicate(x, e, tn, tindex, depth);
+  if (!ppred.isNull())
+  {
+    sb_lemmas.push_back(ppred);
+  }
+
+  // other static conjecture-dependent symmetry breaking goes here
+
+  if (!sb_lemmas.empty())
+  {
+    return sb_lemmas.size() == 1
+               ? sb_lemmas[0]
+               : NodeManager::currentNM()->mkNode(kind::AND, sb_lemmas);
+  }
+  else
+  {
+    return Node::null();
+  }
+}
+
 }/* namespace CVC4::theory::quantifiers */
 }/* namespace CVC4::theory */
 }/* namespace CVC4 */
diff --git a/src/theory/quantifiers/ce_guided_conjecture.h b/src/theory/quantifiers/ce_guided_conjecture.h
index dfd9c1623..b725449b4 100644
--- a/src/theory/quantifiers/ce_guided_conjecture.h
+++ b/src/theory/quantifiers/ce_guided_conjecture.h
@@ -18,9 +18,10 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_CONJECTURE_H
 #define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_CONJECTURE_H
 
-#include "theory/quantifiers/ce_guided_single_inv.h"
 #include "theory/quantifiers/ce_guided_pbe.h"
+#include "theory/quantifiers/ce_guided_single_inv.h"
 #include "theory/quantifiers/sygus_grammar_cons.h"
+#include "theory/quantifiers/sygus_process_conj.h"
 #include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
@@ -31,10 +32,8 @@ namespace quantifiers {
  * This class implements approaches for a synthesis conecjture, given by data
  * member d_quant.
  * This includes both approaches for synthesis in Reynolds et al CAV 2015. It
- * determines
- * which approach and optimizations are applicable to the conjecture, and has
- * interfaces for
- * implementing them.
+ * determines which approach and optimizations are applicable to the
+ * conjecture, and has interfaces for implementing them.
  */
 class CegConjecture {
 public:
@@ -46,7 +45,10 @@ public:
   Node getEmbeddedConjecture() { return d_embed_quant; }
   /** get next decision request */
   Node getNextDecisionRequest( unsigned& priority );
-  /** increment the number of times we have successfully done candidate refinement */
+
+  //-------------------------------for counterexample-guided check/refine
+  /** increment the number of times we have successfully done candidate
+   * refinement */
   void incrementRefineCount() { d_refine_count++; }
   /** whether the conjecture is waiting for a call to doCheck below */
   bool needsCheck( std::vector< Node >& lem );
@@ -73,6 +75,8 @@ public:
   /** Print the synthesis solution
    * singleInvocation is whether the solution was found by single invocation techniques.
    */
+  //-------------------------------end for counterexample-guided check/refine
+
   void printSynthSolution( std::ostream& out, bool singleInvocation );
   /** get guard, this is "G" in Figure 3 of Reynolds et al CAV 2015 */
   Node getGuard();
@@ -96,14 +100,21 @@ public:
   void getModelValues( std::vector< Node >& n, std::vector< Node >& v );
   /** get model value for term n */
   Node getModelValue( Node n );
+
+  //-----------------------------------refinement lemmas
   /** get number of refinement lemmas we have added so far */
   unsigned getNumRefinementLemmas() { return d_refinement_lemmas.size(); }
   /** get refinement lemma */
   Node getRefinementLemma( unsigned i ) { return d_refinement_lemmas[i]; }
   /** get refinement lemma */
   Node getRefinementBaseLemma( unsigned i ) { return d_refinement_lemmas_base[i]; }
+  //-----------------------------------end refinement lemmas
+
   /** get program by examples utility */
   CegConjecturePbe* getPbe() { return d_ceg_pbe; }
+  /** get the symmetry breaking predicate for type */
+  Node getSymmetryBreakingPredicate(
+      Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth);
   /** print out debug information about this conjecture */
   void debugPrint( const char * c );
 private:
@@ -113,11 +124,18 @@ private:
   CegConjectureSingleInv * d_ceg_si;
   /** program by examples utility */
   CegConjecturePbe * d_ceg_pbe;
+  /** utility for static preprocessing and analysis of conjectures */
+  CegConjectureProcess* d_ceg_proc;
   /** grammar utility */
   CegGrammarConstructor * d_ceg_gc;
-  /** list of constants for quantified formula */
+  /** list of constants for quantified formula
+  * The Skolems for the negation of d_embed_quant.
+  */
   std::vector< Node > d_candidates;
-  /** base instantiation */
+  /** base instantiation
+  * If d_embed_quant is forall d. exists y. P( d, y ), then
+  * this is the formula  P( candidates, y ).
+  */
   Node d_base_inst;
   /** expand base inst to disjuncts */
   std::vector< Node > d_base_disj;
@@ -126,12 +144,18 @@ private:
   std::vector< std::vector< Node > > d_inner_vars_disj;
   /** current extential quantifeirs whose couterexamples we must refine */
   std::vector< std::vector< Node > > d_ce_sk;
+
+  //-----------------------------------refinement lemmas
   /** refinement lemmas */
   std::vector< Node > d_refinement_lemmas;
   std::vector< Node > d_refinement_lemmas_base;
+  //-----------------------------------end refinement lemmas
+
   /** quantified formula asserted */
   Node d_quant;
-  /** quantified formula (after processing) */
+  /** quantified formula (after simplification) */
+  Node d_simp_quant;
+  /** quantified formula (after simplification, conversion to deep embedding) */
   Node d_embed_quant;
   /** candidate information */
   class CandidateInfo {
diff --git a/src/theory/quantifiers/ce_guided_pbe.cpp b/src/theory/quantifiers/ce_guided_pbe.cpp
index e4bf43963..cadfbbe86 100644
--- a/src/theory/quantifiers/ce_guided_pbe.cpp
+++ b/src/theory/quantifiers/ce_guided_pbe.cpp
@@ -45,7 +45,8 @@ void print_val( const char * c, std::vector< Node >& vals, bool pol = true ){
   }
 }
 
-void CegConjecturePbe::print_role( const char * c, unsigned r ){
+void CegConjecturePbe::print_role(const char* c, unsigned r)
+{
   switch(r){
   case CegConjecturePbe::enum_io:Trace(c) << "IO";break;
   case CegConjecturePbe::enum_ite_condition:Trace(c) << "CONDITION";break;
@@ -55,12 +56,14 @@ void CegConjecturePbe::print_role( const char * c, unsigned r ){
   }
 }
 
-void CegConjecturePbe::print_strat( const char * c, unsigned s ){
-  switch(s){
-  case CegConjecturePbe::strat_ITE:Trace(c) << "ITE";break;
-  case CegConjecturePbe::strat_CONCAT:Trace(c) << "CONCAT";break;
-  case CegConjecturePbe::strat_ID:Trace(c) << "ID";break;
-  default:Trace(c) << "strat_" << s;break;
+void CegConjecturePbe::print_strat(const char* c, unsigned s)
+{
+  switch (s)
+  {
+    case CegConjecturePbe::strat_ITE: Trace(c) << "ITE"; break;
+    case CegConjecturePbe::strat_CONCAT: Trace(c) << "CONCAT"; break;
+    case CegConjecturePbe::strat_ID: Trace(c) << "ID"; break;
+    default: Trace(c) << "strat_" << s; break;
   }
 }
 
@@ -144,7 +147,10 @@ void CegConjecturePbe::collectExamples( Node n, std::map< Node, bool >& visited,
   }
 }
 
-void CegConjecturePbe::initialize( Node n, std::vector< Node >& candidates, std::vector< Node >& lemmas ) {
+void CegConjecturePbe::initialize(Node n,
+                                  std::vector<Node>& candidates,
+                                  std::vector<Node>& lemmas)
+{
   Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl;
   
   for( unsigned i=0; i<candidates.size(); i++ ){
@@ -202,8 +208,8 @@ void CegConjecturePbe::initialize( Node n, std::vector< Node >& candidates, std:
   if( !d_is_pbe ){
     Trace("sygus-unif") << "Do not do PBE optimizations, register..." << std::endl;
     for( unsigned i=0; i<candidates.size(); i++ ){
-      d_qe->getTermDatabaseSygus()->registerMeasuredTerm(candidates[i],
-                                                         d_parent);
+      d_qe->getTermDatabaseSygus()->registerEnumerator(
+          candidates[i], candidates[i], d_parent);
     }
   }
 }
@@ -211,7 +217,6 @@ void CegConjecturePbe::initialize( Node n, std::vector< Node >& candidates, std:
 Node CegConjecturePbe::PbeTrie::addPbeExample(TypeNode etn, Node e, Node b,
                                               CegConjecturePbe* cpbe,
                                               unsigned index, unsigned ntotal) {
-  Assert(cpbe->getNumExamples(e) == ntotal);
   if (index == ntotal) {
     // lazy child holds the leaf data
     if (d_lazy_child.isNull()) {
@@ -253,7 +258,8 @@ Node CegConjecturePbe::PbeTrie::addPbeExampleEval(TypeNode etn, Node e, Node b,
 
 bool CegConjecturePbe::hasExamples(Node e) {
   if (isPbe()) {
-    e = getSynthFunctionForEnumerator(e);
+    e = d_tds->getSynthFunForEnumerator(e);
+    Assert(!e.isNull());
     std::map<Node, bool>::iterator itx = d_examples_invalid.find(e);
     if (itx == d_examples_invalid.end()) {
       return d_examples.find(e) != d_examples.end();
@@ -263,7 +269,8 @@ bool CegConjecturePbe::hasExamples(Node e) {
 }
 
 unsigned CegConjecturePbe::getNumExamples(Node e) {
-  e = getSynthFunctionForEnumerator(e);
+  e = d_tds->getSynthFunForEnumerator(e);
+  Assert(!e.isNull());
   std::map<Node, std::vector<std::vector<Node> > >::iterator it =
       d_examples.find(e);
   if (it != d_examples.end()) {
@@ -274,7 +281,8 @@ unsigned CegConjecturePbe::getNumExamples(Node e) {
 }
 
 void CegConjecturePbe::getExample(Node e, unsigned i, std::vector<Node>& ex) {
-  e = getSynthFunctionForEnumerator(e);
+  e = d_tds->getSynthFunForEnumerator(e);
+  Assert(!e.isNull());
   std::map<Node, std::vector<std::vector<Node> > >::iterator it =
       d_examples.find(e);
   if (it != d_examples.end()) {
@@ -286,7 +294,8 @@ void CegConjecturePbe::getExample(Node e, unsigned i, std::vector<Node>& ex) {
 }
 
 Node CegConjecturePbe::getExampleOut(Node e, unsigned i) {
-  e = getSynthFunctionForEnumerator(e);
+  e = d_tds->getSynthFunForEnumerator(e);
+  Assert(!e.isNull());
   std::map<Node, std::vector<Node> >::iterator it = d_examples_out.find(e);
   if (it != d_examples_out.end()) {
     Assert(i < it->second.size());
@@ -300,7 +309,8 @@ Node CegConjecturePbe::getExampleOut(Node e, unsigned i) {
 Node CegConjecturePbe::addSearchVal(TypeNode tn, Node e, Node bvr) {
   Assert(isPbe());
   Assert(!e.isNull());
-  e = getSynthFunctionForEnumerator(e);
+  e = d_tds->getSynthFunForEnumerator(e);
+  Assert(!e.isNull());
   std::map<Node, bool>::iterator itx = d_examples_invalid.find(e);
   if (itx == d_examples_invalid.end()) {
     unsigned nex = d_examples[e].size();
@@ -313,7 +323,8 @@ Node CegConjecturePbe::addSearchVal(TypeNode tn, Node e, Node bvr) {
 
 Node CegConjecturePbe::evaluateBuiltin(TypeNode tn, Node bn, Node e,
                                        unsigned i) {
-  e = getSynthFunctionForEnumerator(e);
+  e = d_tds->getSynthFunForEnumerator(e);
+  Assert(!e.isNull());
   std::map<Node, bool>::iterator itx = d_examples_invalid.find(e);
   if (itx == d_examples_invalid.end()) {
     std::map<Node, std::vector<std::vector<Node> > >::iterator it =
@@ -326,15 +337,6 @@ Node CegConjecturePbe::evaluateBuiltin(TypeNode tn, Node bn, Node e,
   return Rewriter::rewrite(bn);
 }
 
-Node CegConjecturePbe::getSynthFunctionForEnumerator(Node e) {
-  std::map<Node, Node>::const_iterator it = d_enum_to_candidate.find(e);
-  if (it != d_enum_to_candidate.end()) {
-    return it->second;
-  } else {
-    return e;
-  }
-}
-
 // ----------------------------- establishing enumeration types
 
 
@@ -343,7 +345,7 @@ void CegConjecturePbe::registerEnumerator( Node et, Node c, TypeNode tn, unsigne
   Trace("sygus-unif-debug") << ", role = ";
   print_role( "sygus-unif-debug", enum_role );
   Trace("sygus-unif-debug") << ", in search = " << inSearch << std::endl;
-  d_einfo[et].initialize( c, enum_role );
+  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 );
@@ -353,9 +355,9 @@ void CegConjecturePbe::registerEnumerator( Node et, Node c, TypeNode tn, unsigne
       d_cinfo[c].d_esym_list.push_back( et );
       d_einfo[et].d_enum_slave.push_back( et );
       //register measured term with database
-      d_enum_to_candidate[et] = c;
-      d_qe->getTermDatabaseSygus()->registerMeasuredTerm(et, d_parent, true);
-      d_einfo[et].d_active_guard = d_qe->getTermDatabaseSygus()->getActiveGuardForMeasureTerm( et );
+      d_qe->getTermDatabaseSygus()->registerEnumerator(et, c, d_parent, true);
+      d_einfo[et].d_active_guard =
+          d_qe->getTermDatabaseSygus()->getActiveGuardForEnumerator(et);
     }else{
       Trace("sygus-unif-debug") << "Make " << et << " a slave of " << itn->second << std::endl;
       d_einfo[itn->second].d_enum_slave.push_back( et );
@@ -388,8 +390,9 @@ void CegConjecturePbe::collectEnumeratorTypes( Node e, TypeNode tn, unsigned enu
       std::map< Node, std::map< unsigned, Node > > cop_to_child_templ_arg;
       std::map< Node, unsigned > cop_to_strat;
       std::map< Node, unsigned > cop_to_cindex;
-      
-      // look at builtin operartors first (when r=0), then defined operators (when r=1)
+
+      // look at builtin operartors first (when r=0), then defined operators
+      // (when r=1)
       for( unsigned r=0; r<2; r++ ){
         for( unsigned j=0; j<dt.getNumConstructors(); j++ ){
           Node cop = Node::fromExpr( dt[j].getConstructor() );
@@ -408,8 +411,9 @@ void CegConjecturePbe::collectEnumeratorTypes( Node e, TypeNode tn, unsigned enu
                 }
               }
               if( cop_to_strat.find( cop )!=cop_to_strat.end() ){
-                Trace("sygus-unif") << "...type " << dt.getName() << " has strategy ";
-                print_strat("sygus-unif",cop_to_strat[cop]); 
+                Trace("sygus-unif") << "...type " << dt.getName()
+                                    << " has strategy ";
+                print_strat("sygus-unif", cop_to_strat[cop]);
                 Trace("sygus-unif") << "..." << std::endl;
                 // add child types
                 for( unsigned k=0; k<dt[j].getNumArgs(); k++ ){
@@ -452,7 +456,9 @@ void CegConjecturePbe::collectEnumeratorTypes( Node e, TypeNode tn, unsigned enu
                 cop_to_strat[cop] = strat_ITE;
               }
             }else if( eut.getKind()==kind::STRING_CONCAT ){
-              if( dt[j].getNumArgs()>=eut.getNumChildren() && eut.getNumChildren()==2 ){
+              if (dt[j].getNumArgs() >= eut.getNumChildren()
+                  && eut.getNumChildren() == 2)
+              {
                 cop_to_strat[cop] = strat_CONCAT;
               }
             }else if( eut.getKind()==kind::APPLY_UF ){
@@ -508,7 +514,7 @@ void CegConjecturePbe::collectEnumeratorTypes( Node e, TypeNode tn, unsigned enu
               }
               if( cop_to_strat.find( cop )!=cop_to_strat.end() ){
                 Trace("sygus-unif") << "...type " << dt.getName() << " has defined constructor matching strategy ";
-                print_strat("sygus-unif",cop_to_strat[cop]);
+                print_strat("sygus-unif", cop_to_strat[cop]);
                 Trace("sygus-unif") << "..." << std::endl;
                 for( unsigned k=0; k<eut.getNumChildren(); k++ ){
                   Assert( templ_injection.find( k )!=templ_injection.end() );
@@ -605,8 +611,6 @@ void CegConjecturePbe::collectEnumeratorTypes( Node e, TypeNode tn, unsigned enu
             Trace("sygus-unif-debug") << std::endl;
             Assert( !et.isNull() );
             d_cinfo[e].d_tinfo[tn].d_strat[cop].d_cenum.push_back( et );
-            // need to make this take into account template
-            //Assert( et.getType()==e.getType() || d_einfo[et].getRole()!=enum_io );
           }
           Trace("sygus-unif") << "Initialized strategy ";
           print_strat( "sygus-unif", strat );
@@ -659,7 +663,7 @@ void CegConjecturePbe::staticLearnRedundantOps( Node c, std::vector< Node >& lem
       std::map< Node, EnumInfo >::iterator itns = d_einfo.find( es );
       Assert( itns!=d_einfo.end() );
       Trace("sygus-unif") << "  " << es << ", role = ";
-      print_role( "sygus-unif", itns->second.getRole() );
+      print_role("sygus-unif", itns->second.getRole());
       Trace("sygus-unif") << std::endl;
     }
   }
@@ -851,7 +855,8 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >&
         Assert( itv!=d_einfo.end() );
         Trace("sygus-pbe-enum") << "Process " << xs << " from " << s << std::endl;
         //bool prevIsCover = false;
-        if( itv->second.getRole()==enum_io ){
+        if (itv->second.getRole() == enum_io)
+        {
           Trace("sygus-pbe-enum") << "   IO-Eval of ";
           //prevIsCover = itv->second.isFeasible();
         }else{
@@ -874,7 +879,8 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >&
             Assert( res.isConst() );
           }
           Node resb;
-          if( itv->second.getRole()==enum_io ){
+          if (itv->second.getRole() == enum_io)
+          {
             Node out = itxo->second[j];
             Assert( out.isConst() );
             resb = res==out ? d_true : d_false;
@@ -892,7 +898,8 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >&
           }
         }
         bool keep = false;
-        if( itv->second.getRole()==enum_io ){
+        if (itv->second.getRole() == enum_io)
+        {
           if( cond_vals.find( d_true )!=cond_vals.end() || cond_vals.empty() ){  // latter is the degenerate case of no examples
             //check subsumbed/subsuming
             std::vector< Node > subsume;
@@ -956,7 +963,8 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >&
           if( Trace.isOn("sygus-pbe-enum") ){
             if( itv->second.getRole()==enum_io ){
               if( !prevIsCover && itv->second.isFeasible() ){
-                Trace("sygus-pbe-enum") << "...PBE : success : Evaluation of " << xs << " now covers all examples." << std::endl;
+                Trace("sygus-pbe-enum") << "...PBE : success : Evaluation of "
+          << xs << " now covers all examples." << std::endl;
               }
             }
           }
@@ -980,30 +988,76 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >&
   }
 }
 
-
-
+/** NegContainsSygusInvarianceTest
+*
+* This class is used to construct a minimal shape of a term that cannot
+* be contained in at least one output of an I/O pair.
+*
+* Say our PBE conjecture is:
+*
+* exists f.
+*   f( "abc" ) = "abc abc" ^
+*   f( "de" ) = "de de"
+*
+* Then, this class is used when there is a candidate solution t[x1] such that
+* either
+*   contains( "abc abc", t["abc"] ) ---> false or
+*   contains( "de de", t["de"] ) ---> false
+*
+* In particular it is used to determine whether certain generalizations of t[x1]
+* are still sufficient to falsify one of the above containments.
+*
+* For example:
+*
+* str.++( x1, "d" ) can be minimized to str.++( _, "d" )
+*   ...since contains( "abc abc", str.++( y, "d" ) ) ---> false,
+*      for any y.
+* str.replace( "de", x1, "b" ) can be minimized to str.replace( "de", x1, _ )
+*   ...since contains( "abc abc", str.replace( "de", "abc", y ) ) ---> false,
+*      for any y.
+*
+* It is an instance of quantifiers::SygusInvarianceTest, which
+* traverses the AST of a given term, replaces each subterm by a
+* fresh variable y and checks whether an invariance test (such as
+* the one specified by this class) holds.
+*
+*/
 class NegContainsSygusInvarianceTest : public quantifiers::SygusInvarianceTest {
 public:
   NegContainsSygusInvarianceTest(){}
   ~NegContainsSygusInvarianceTest(){}
-  Node d_ar;
-  std::vector< Node > d_exo;
-  std::vector< unsigned > d_neg_con_indices;
-  quantifiers::CegConjecturePbe* d_cpbe;
-
-  void init(quantifiers::CegConjecturePbe* cpbe, Node ar,
-            std::vector<Node>& exo, std::vector<unsigned>& ncind) {
-    if (cpbe->hasExamples(ar)) {
-      Assert(cpbe->getNumExamples(ar) == exo.size());
-      d_ar = ar;
+  /** 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.
+  *    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(quantifiers::CegConjecturePbe* cpbe,
+            Node e,
+            std::vector<Node>& exo,
+            std::vector<unsigned>& ncind)
+  {
+    if (cpbe->hasExamples(e))
+    {
+      Assert(cpbe->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_cpbe = cpbe;
     }
   }
-protected:  
+
+ protected:
+  /** checks whether contains( out_i, nvn[in_i] ) --> false for some I/O pair i.
+   */
   bool invariant( quantifiers::TermDbSygus * tds, Node nvn, Node x ){
-    if( !d_ar.isNull() ){
+    if (!d_enum.isNull())
+    {
       TypeNode tn = nvn.getType();
       Node nbv = tds->sygusToBuiltin( nvn, tn );
       Node nbvr = tds->extendedRewrite( nbv );
@@ -1011,7 +1065,7 @@ protected:
       for( unsigned i=0; i<d_neg_con_indices.size(); i++ ){
         unsigned ii = d_neg_con_indices[i];
         Assert( ii<d_exo.size() );
-        Node nbvre = d_cpbe->evaluateBuiltin(tn, nbvr, d_ar, ii);
+        Node nbvre = d_cpbe->evaluateBuiltin(tn, nbvr, d_enum, ii);
         Node out = d_exo[ii];
         Node cont = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, out, nbvre );
         Node contr = Rewriter::rewrite( cont );
@@ -1021,7 +1075,7 @@ protected:
             Trace("sygus-pbe-cterm") << nbv << " for any " << tds->sygusToBuiltin( x ) << " since " << std::endl;
             Trace("sygus-pbe-cterm") << "   PBE-cterm :    for input example : ";
             std::vector< Node > ex;
-            d_cpbe->getExample(d_ar, ii, ex);
+            d_cpbe->getExample(d_enum, ii, ex);
             for( unsigned j=0; j<ex.size(); j++ ){
               Trace("sygus-pbe-cterm") << ex[j] << " ";
             }
@@ -1035,6 +1089,18 @@ protected:
     }
     return false;
   }
+
+ private:
+  /** The enumerator whose value we are considering in this invariance test */
+  Node d_enum;
+  /** 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 PBE utility */
+  quantifiers::CegConjecturePbe* d_cpbe;
 };
 
 
@@ -1042,7 +1108,8 @@ bool CegConjecturePbe::getExplanationForEnumeratorExclude( Node c, Node x, Node
   if( ei.d_enum_slave.size()==1 ){
     // this check whether the example evaluates to something that is larger than the output
     //  if so, then this term is never useful when using a concatenation strategy
-    if( ei.getRole()==enum_concat_term ){
+    if (ei.getRole() == enum_concat_term)
+    {
       if( Trace.isOn("sygus-pbe-cterm-debug") ){
         Trace("sygus-pbe-enum") << std::endl;
       }
@@ -1078,7 +1145,7 @@ bool CegConjecturePbe::getExplanationForEnumeratorExclude( Node c, Node x, Node
       if( !cmp_indices.empty() ){
         //set up the inclusion set
         NegContainsSygusInvarianceTest ncset;
-        ncset.init(this, c, itxo->second, cmp_indices);
+        ncset.init(this, x, itxo->second, cmp_indices);
         d_tds->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;
@@ -1096,7 +1163,7 @@ void CegConjecturePbe::EnumInfo::addEnumValue( CegConjecturePbe * pbe, Node v, s
   d_enum_vals_res.push_back( results );
   /*
   if( getRole()==enum_io ){
-    // compute 
+    // compute
     if( d_enum_total.empty() ){
       d_enum_total = results;
     }else if( !d_enum_total_true ){
@@ -1464,12 +1531,16 @@ Node CegConjecturePbe::constructSolution( Node c, Node e, UnifContext& x, int in
   std::map< Node, EnumInfo >::iterator itn = d_einfo.find( e );
   Assert( itn!=d_einfo.end() );
   Node ret_dt;
-  if( itn->second.getRole()==enum_any ){
+  if (itn->second.getRole() == enum_any)
+  {
     indent("sygus-pbe-dt", ind);
     ret_dt = constructBestSolvedTerm( itn->second.d_enum_vals, x );
     Trace("sygus-pbe-dt") << "return PBE: success : use any " << d_tds->sygusToBuiltin( ret_dt ) << std::endl;
     Assert( !ret_dt.isNull() );
-  }else if( itn->second.getRole()==enum_io && !x.isReturnValueModified() && itn->second.isSolved() ){
+  }
+  else if (itn->second.getRole() == enum_io && !x.isReturnValueModified()
+           && itn->second.isSolved())
+  {
     // this type has a complete solution
     ret_dt = itn->second.getSolved();
     indent("sygus-pbe-dt", ind);
@@ -1485,7 +1556,8 @@ Node CegConjecturePbe::constructSolution( Node c, Node e, UnifContext& x, int in
       // get the term enumerator for this type
       bool success = true;
       std::map< Node, EnumInfo >::iterator itet;
-      if( itn->second.getRole()==enum_concat_term ){
+      if (itn->second.getRole() == enum_concat_term)
+      {
         itet = itn;
       }else{
         std::map< unsigned, Node >::iterator itnt = itt->second.d_enum.find( enum_concat_term );
@@ -1522,7 +1594,9 @@ Node CegConjecturePbe::constructSolution( Node c, Node e, UnifContext& x, int in
           Trace("sygus-pbe-dt-debug") << "  ...not currently string solved." << std::endl;
         }
       }
-    }else if( itn->second.getRole()==enum_io && !x.isReturnValueModified() ){
+    }
+    else if (itn->second.getRole() == enum_io && !x.isReturnValueModified())
+    {
       // it has an enumerated value that is conditionally correct under the current assumptions
       std::vector< Node > subsumed_by;
       itn->second.d_term_trie.getSubsumedBy( this, x.d_vals, true, subsumed_by );
@@ -1555,31 +1629,36 @@ Node CegConjecturePbe::constructSolution( Node c, Node e, UnifContext& x, int in
           Node incr_val;
           int incr_type = 0;
           std::map< Node, std::vector< unsigned > > incr;
-            
+
           // construct the child order based on heuristics
           std::vector< unsigned > corder;
-          std::unordered_set< unsigned > cused;
+          std::unordered_set<unsigned> cused;
           if( strat==strat_CONCAT ){
             for( unsigned r=0; r<2; r++ ){
               // Concatenate strategy can only be applied from the endpoints.
-              // This chooses the appropriate endpoint for which we stay within the same SyGuS type.
-              // In other words, if we are synthesizing based on a production rule ( T -> str.++( T1, ..., Tn ) ), then we
-              // prefer recursing on the 1st argument of the concat if T1 = T, and the last argument if Tn = T.
+              // This chooses the appropriate endpoint for which we stay within
+              // the same SyGuS type.
+              // In other words, if we are synthesizing based on a production
+              // rule ( T -> str.++( T1, ..., Tn ) ), then we
+              // prefer recursing on the 1st argument of the concat if T1 = T,
+              // and the last argument if Tn = T.
               unsigned sc = r==0 ? 0 : itts->second.d_cenum.size()-1;
               Node ce = itts->second.d_cenum[sc];
               if( ce.getType()==etn ){
                 // prefer simple recursion (self type)
                 Assert( d_einfo.find( ce )!=d_einfo.end() );
-                Assert( d_einfo[ce].getRole()==enum_concat_term );
+                Assert(d_einfo[ce].getRole() == enum_concat_term);
                 corder.push_back( sc );
-                cused.insert( sc );
+                cused.insert(sc);
                 break;
               }
             }
           }
           // fill remaining children for which there is no preference
-          for( unsigned sc=0; sc<itts->second.d_cenum.size(); sc++ ){
-            if( cused.find( sc )==cused.end() ){
+          for (unsigned sc = 0; sc < itts->second.d_cenum.size(); sc++)
+          {
+            if (cused.find(sc) == cused.end())
+            {
               corder.push_back( sc );
             }
           }
@@ -1709,7 +1788,7 @@ Node CegConjecturePbe::constructSolution( Node c, Node e, UnifContext& x, int in
                 std::map< Node, EnumInfo >::iterator itsc = d_einfo.find( ce );
                 Assert( itsc!=d_einfo.end() );
                 // ensured by the child order we set above
-                Assert( itsc->second.getRole()==enum_concat_term );
+                Assert(itsc->second.getRole() == enum_concat_term);
                 // check if each return value is a prefix/suffix of all open examples
                 incr_type = sc==0 ? -1 : 1;
                 if( x.d_has_string_pos==0 || x.d_has_string_pos==incr_type ){
diff --git a/src/theory/quantifiers/ce_guided_pbe.h b/src/theory/quantifiers/ce_guided_pbe.h
index e4c252194..ca0190dc0 100644
--- a/src/theory/quantifiers/ce_guided_pbe.h
+++ b/src/theory/quantifiers/ce_guided_pbe.h
@@ -35,7 +35,7 @@ class CegEntailmentInfer;
 * that are in Programming-By-Examples (PBE) form.
 *
 * [EX#1] An example of a synthesis conjecture in PBE form is :
-* exists f. forall x. 
+* exists f. forall x.
 * ( x = 0 => f( x ) = 2 ) ^ ( x = 5 => f( x ) = 7 ) ^ ( x = 6 => f( x ) = 8 )
 *
 * We say that the above conjecture has I/O examples (0)->2, (5)->7, (6)->8.
@@ -45,79 +45,104 @@ class CegEntailmentInfer;
 * (1) Infers whether the input conjecture is in PBE form or not.
 * (2) Based on this information and on the syntactic restrictions, it
 *     devises a strategy for enumerating terms and construction solutions,
-*     which is inspired by Alur et al. "Scaling Enumerative Program Synthesis 
-*     via Divide and Conquer" TACAS 2017. In particular, it may consider strategies
-*     for constructing decision trees when the grammar permits ITEs and a 
-*     strategy for divide-and-conquer string synthesis when the grammar permits
-*     string concatenation. This is stored in a set of data structures within 
-*     d_cinfo.
-* (3) It makes (possibly multiple) calls to 
+*     which is inspired by Alur et al. "Scaling Enumerative Program Synthesis
+*     via Divide and Conquer" TACAS 2017. In particular, it may consider
+*     strategies for constructing decision trees when the grammar permits ITEs
+*     and a strategy for divide-and-conquer string synthesis when the grammar
+*     permits string concatenation. This is stored in a set of data structures
+*     within d_cinfo.
+* (3) It makes (possibly multiple) calls to
 *     TermDatabaseSygus::registerMeasuredTerm(...) based
 *     on the strategy, which inform the rest of the system to enumerate values
-*     of particular types in the grammar through use of fresh variables which 
+*     of particular types in the grammar through use of fresh variables which
 *     we call "enumerators".
 *
 * Points (1)-(3) happen within a call to CegConjecturePbe::initialize(...).
 *
-* Notice that each enumerator is associated with a single function-to-synthesize,
+* Notice that each enumerator is associated with a single
+* function-to-synthesize,
 * but a function-to-sythesize may be mapped to multiple enumerators.
 * Some public functions of this class expect an enumerator as input, which we
-* map to a function-to-synthesize via getSynthFunctionForEnumerator.
+* map to a function-to-synthesize via TermDatabaseSygus::getSynthFunFor(e).
 *
 * An enumerator is initially "active" but may become inactive if the enumeration
-* exhausts all possible values in the datatype corresponding to syntactic restrictions
+* exhausts all possible values in the datatype corresponding to syntactic
+* restrictions
 * for it. The search may continue unless all enumerators become inactive.
 *
-* (4) During search, the extension of quantifier-free datatypes procedure for SyGuS 
-*     datatypes may ask this class whether current candidates can be discarded based on 
-*     inferring when two candidate solutions are equivalent up to examples. 
-*     For example, the candidate solutions: 
-*     f = \x ite( x<0, x+1, x ) and f = \x x 
-*     are equivalent up to examples on the above conjecture, since they have the same
-*     value on the points x = 0,5,6. Hence, we need only consider one of them.
-*     The interface for querying this is CegConjecturePbe::addSearchVal(...).
+* (4) During search, the extension of quantifier-free datatypes procedure for
+*     SyGuS datatypes may ask this class whether current candidates can be
+*     discarded based on
+*     inferring when two candidate solutions are equivalent up to examples.
+*     For example, the candidate solutions:
+*     f = \x ite( x<0, x+1, x ) and f = \x x
+*     are equivalent up to examples on the above conjecture, since they have the
+*     same value on the points x = 0,5,6. Hence, we need only consider one of
+*     them. The interface for querying this is
+* CegConjecturePbe::addSearchVal(...).
 *     For details, see Reynolds et al. SYNT 2017.
-* 
-* (5) When the extension of quantifier-free datatypes procedure for SyGuS datatypes
-*     terminates with a model, the parent of this class calls 
-*     CegConjecturePbe::getCandidateList(...), where this class returns the list of 
-*     active enumerators.
-* (6) The parent class subsequently calls CegConjecturePbe::constructValues(...), which
-*     informs this class that new values have been enumerated for active enumerators,
-*     as indicated by the current model. This call also requests that based on these
-*     newly enumerated values, whether this class is now able to construct a solution
-*     based on the high-level strategy (stored in d_c_info).
 *
-* This class is not designed to work in incremental mode, since there is no way to 
+* (5) When the extension of quantifier-free datatypes procedure for SyGuS
+*     datatypes terminates with a model, the parent of this class calls
+*     CegConjecturePbe::getCandidateList(...), where this class returns the list
+*     of active enumerators.
+* (6) The parent class subsequently calls
+*     CegConjecturePbe::constructValues(...), which
+*     informs this class that new values have been enumerated for active
+*     enumerators, as indicated by the current model. This call also requests
+*     that based on these
+*     newly enumerated values, whether this class is now able to construct a
+*     solution based on the high-level strategy (stored in d_c_info).
+*
+* This class is not designed to work in incremental mode, since there is no way
+* to
 * specify incremental problems in SyguS.
 *
 */
 class CegConjecturePbe {
-public:
-  CegConjecturePbe( QuantifiersEngine * qe, CegConjecture * p );
+ public:
+  CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p);
   ~CegConjecturePbe();
-  
-  /** initialize this class */
-  void initialize( Node n, std::vector< Node >& candidates, std::vector< Node >& lemmas );
+
+  /** initialize this class
+  *
+  * n is the "base instantiation" of the deep-embedding version of
+  *   the synthesis conjecture under "candidates".
+  *   (see CegConjecture::d_base_inst)
+  *
+  * This function may add lemmas to the vector lemmas corresponding
+  * to initial lemmas regarding static analysis of enumerators it
+  * introduced. For example, we may say that the top-level symbol
+  * of an enumerator is not ITE if it is being used to construct
+  * return values for decision trees.
+  */
+  void initialize(Node n,
+                  std::vector<Node>& candidates,
+                  std::vector<Node>& lemmas);
   /** get candidate list
-  * Adds all active enumerators associated with functions-to-synthesize in candidates to clist.
+  * Adds all active enumerators associated with functions-to-synthesize in
+  * candidates to clist.
   */
-  void getCandidateList( std::vector< Node >& candidates, std::vector< Node >& clist );
-  /** construct candidates 
-  * (1) Indicates that the list of enumerators in "enums" currently have model values "enum_values".
-  * (2) Asks whether based on these new enumerated values, we can construct a solution for
-  *     the functions-to-synthesize in "candidates". If so, this function returns "true" and
+  void getCandidateList(std::vector<Node>& candidates,
+                        std::vector<Node>& clist);
+  /** construct candidates
+  * (1) Indicates that the list of enumerators in "enums" currently have model
+  *     values "enum_values".
+  * (2) Asks whether based on these new enumerated values, we can construct a
+  *     solution for
+  *     the functions-to-synthesize in "candidates". If so, this function
+  *     returns "true" and
   *     adds solutions for candidates into "candidate_values".
-  * During this class, this class may add auxiliary lemmas to "lems", which the caller
-  * should send on the output channel via lemma(...). 
+  * During this class, this class may add auxiliary lemmas to "lems", which the
+  * caller should send on the output channel via lemma(...).
   */
-  bool constructCandidates( std::vector< Node >& enums, std::vector< Node >& enum_values, 
-                            std::vector< Node >& candidates, std::vector< Node >& candidate_values, 
-                            std::vector< Node >& lems );
+  bool constructCandidates(std::vector<Node>& enums,
+                           std::vector<Node>& enum_values,
+                           std::vector<Node>& candidates,
+                           std::vector<Node>& candidate_values,
+                           std::vector<Node>& lems);
   /** is PBE enabled for any enumerator? */
   bool isPbe() { return d_is_pbe; }
-  /** get candidate for enumerator */
-  Node getSynthFunctionForEnumerator(Node e);
   /** is the enumerator e associated with I/O example pairs? */
   bool hasExamples(Node e);
   /** get number of I/O example pairs for enumerator e */
@@ -127,33 +152,38 @@ public:
   void getExample(Node e, unsigned i, std::vector<Node>& ex);
   /** get the output value of the i^th I/O example for enumerator e */
   Node getExampleOut(Node e, unsigned i);
-  
+
   /** add the search val
-  * This function is called by the extension of quantifier-free datatypes procedure 
-  * for SyGuS datatypes when we are considering a value of enumerator e of sygus 
-  * type tn whose analog in the signature of builtin theory is bvr. 
-  * 
-  * For example, bvr = x + 1 when e is the datatype value Plus( x(), One() ) and 
+  * This function is called by the extension of quantifier-free datatypes
+  * procedure for SyGuS datatypes when we are considering a value of
+  * enumerator e of sygus type tn whose analog in the signature of builtin
+  * theory is bvr.
+  *
+  * For example, bvr = x + 1 when e is the datatype value Plus( x(), One() ) and
   * tn is a sygus datatype that encodes a subsignature of the integers.
   *
   * This returns either:
-  * - A SyGuS term whose analog is equivalent to bvr up to examples, in the above example,
-  *   it may return a term t of the form Plus( One(), x() ), such that this function was 
-  *   previously called with t as input.
+  * - A SyGuS term whose analog is equivalent to bvr up to examples, in the
+  *   above example,
+  *   it may return a term t of the form Plus( One(), x() ), such that this
+  *   function was previously called with t as input.
   * - e, indicating that no previous terms are equivalent to e up to examples.
   */
   Node addSearchVal(TypeNode tn, Node e, Node bvr);
   /** evaluate builtin
-  * This returns the evaluation of bn on the i^th example for the function-to-synthesis
-  * associated with enumerator e. If there are not at least i examples, it returns
-  * the rewritten form of bn.
-  * For example, if bn = x+5, e is an enumerator for f in the above example [EX#1], then
+  * This returns the evaluation of bn on the i^th example for the
+  * function-to-synthesis
+  * associated with enumerator e. If there are not at least i examples, it
+  * returns the rewritten form of bn.
+  * For example, if bn = x+5, e is an enumerator for f in the above example
+  * [EX#1], then
   *   evaluateBuiltin( tn, bn, e, 0 ) = 7
   *   evaluateBuiltin( tn, bn, e, 1 ) = 9
   *   evaluateBuiltin( tn, bn, e, 2 ) = 10
   */
-  Node evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i);       
-private:
+  Node evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i);
+
+ private:
   /** quantifiers engine associated with this class */
   QuantifiersEngine* d_qe;
   /** sygus term database of d_qe */
@@ -162,7 +192,8 @@ private:
   Node d_true;
   Node d_false;
   /** parent conjecture
-  * This is the data structure that contains global information about the conjecture.
+  * This is the data structure that contains global information about the
+  * conjecture.
   */
   CegConjecture* d_parent;
   /** is this a PBE conjecture for any function? */
@@ -180,7 +211,8 @@ private:
   *   exists f. forall x. ( x = 0 => f( x ) > 2 )
   * another example is:
   *   exists f. forall x. ( ( x = 0 => f( x ) = 2 ) V ( x = 3 => f( x ) = 3 ) )
-  * since the formula is not a conjunction (the example values are not entailed).
+  * since the formula is not a conjunction (the example values are not
+  * entailed).
   * However, the domain of f in both cases is finite, which can be used for
   * search space pruning.
   */
@@ -191,26 +223,20 @@ private:
   /** for each candidate variable (function-to-synthesize), output of I/O
    * examples */
   std::map< Node, std::vector< Node > > d_examples_out;
-  /** the list of example terms 
-   * For the example [EX#1] above, this is f( 0 ), f( 5 ), f( 6 ) 
+  /** the list of example terms
+   * For the example [EX#1] above, this is f( 0 ), f( 5 ), f( 6 )
    */
   std::map< Node, std::vector< Node > > d_examples_term;
-  /** map from enumerators to candidate varaibles (function-to-synthesize). An
-  * enumerator may not be equivalent
-  * to the candidate variable it maps so in synthesis-through-unification
-  * approaches (e.g. decision tree construction).
-  */
-  std::map<Node, Node> d_enum_to_candidate;
-  /** collect the PBE examples in n 
+  /** collect the PBE examples in n
   * This is called on the input conjecture, and will populate the above vectors.
   *   hasPol/pol denote the polarity of n in the conjecture.
   */
   void collectExamples( Node n, std::map< Node, bool >& visited, bool hasPol, bool pol );
-  
+
   //--------------------------------- PBE search values
   /** this class is an index of candidate solutions for PBE synthesis */
   class PbeTrie {
-  public:
+   public:
     PbeTrie() {}
     ~PbeTrie() {}
     Node d_lazy_child;
@@ -218,7 +244,8 @@ private:
     void clear() { d_children.clear(); }
     Node addPbeExample(TypeNode etn, Node e, Node b, CegConjecturePbe* cpbe,
                        unsigned index, unsigned ntotal);
-  private:
+
+   private:
     Node addPbeExampleEval(TypeNode etn, Node e, Node b, std::vector<Node>& ex,
                            CegConjecturePbe* cpbe, unsigned index,
                            unsigned ntotal);
@@ -231,9 +258,9 @@ private:
   */
   std::map<Node, std::map<TypeNode, PbeTrie> > d_pbe_trie;
   //--------------------------------- end PBE search values
-  
+
   // -------------------------------- decision tree learning
-  //index filter 
+  // index filter
   class IndexFilter {
   public:
     IndexFilter(){}
@@ -243,7 +270,7 @@ private:
     unsigned next( unsigned i );
     void clear() { d_next.clear(); }
     bool isEq( std::vector< Node >& vs, Node v );
-  };  
+  };
   // subsumption trie
   class SubsumeTrie {
   public:
@@ -265,22 +292,37 @@ private:
       d_term = Node::null();
       d_children.clear(); 
     }
-  private:
+
+   private:
     /** the term at this node */
     Node d_term;
     /** the children nodes of this trie */
-    std::map< Node, SubsumeTrie > d_children;
+    std::map<Node, SubsumeTrie> d_children;
     /** helper function for above functions */
-    Node addTermInternal( CegConjecturePbe * pbe, Node t, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed, bool spol, IndexFilter * f, 
-                          unsigned index, int status, bool checkExistsOnly, bool checkSubsume );
+    Node addTermInternal(CegConjecturePbe* pbe,
+                         Node t,
+                         std::vector<Node>& vals,
+                         bool pol,
+                         std::vector<Node>& subsumed,
+                         bool spol,
+                         IndexFilter* f,
+                         unsigned index,
+                         int status,
+                         bool checkExistsOnly,
+                         bool checkSubsume);
     /** helper function for above functions */
-    void getLeavesInternal( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::map< int, std::vector< Node > >& v, IndexFilter * f, 
-                            unsigned index, int status );
+    void getLeavesInternal(CegConjecturePbe* pbe,
+                           std::vector<Node>& vals,
+                           bool pol,
+                           std::map<int, std::vector<Node> >& v,
+                           IndexFilter* f,
+                           unsigned index,
+                           int status);
   };
   // -------------------------------- end decision tree learning
-  
+
   //------------------------------ representation of a enumeration strategy
-  
+
   /** roles for enumerators */
   enum {
     enum_io,
@@ -289,36 +331,39 @@ private:
     enum_any,
   };
   /** print the role with Trace c. */
-  static void print_role( const char * c, unsigned r );
+  static void print_role(const char* c, unsigned r);
   /** strategies for SyGuS datatype types */
-  enum {
+  enum
+  {
     strat_ITE,
     strat_CONCAT,
     strat_ID,
-  };  
+  };
   /** print the strategy with Trace c. */
-  static void print_strat( const char * c, unsigned s );
-  
+  static void print_strat(const char* c, unsigned s);
+
   /** information about an enumerator */
   class EnumInfo {
   public:
     EnumInfo() : d_role( enum_io ){}
-    /** initialize this class 
-    * c is the parent function-to-synthesize 
+    /** 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, unsigned role ){
+    void initialize(Node c, unsigned role)
+    {
       d_parent_candidate = c;
       d_role = role;
     }
     bool isTemplated() { return !d_template.isNull(); }
-    void addEnumValue( CegConjecturePbe * pbe, Node v, std::vector< Node >& results );
-    void setSolved( Node slv );
+    void addEnumValue(CegConjecturePbe* pbe,
+                      Node v,
+                      std::vector<Node>& results);
+    void setSolved(Node slv);
     bool isSolved() { return !d_enum_solved.isNull(); }
     Node getSolved() { return d_enum_solved; }
     unsigned getRole() { return d_role; }
-    
     Node d_parent_candidate;
     // for template
     Node d_template;
@@ -335,16 +380,17 @@ private:
     std::vector< Node > d_enum_subsume;
     std::map< Node, unsigned > d_enum_val_to_index;
     SubsumeTrie d_term_trie;
-  private:
-    /** whether an enumerated value for this conjecture has solved the entire conjecture */
+
+   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). */
     unsigned d_role;
   };
   /** maps enumerators to the information above */
   std::map< Node, EnumInfo > d_einfo;
-  
-  
+
   class CandidateInfo;
   /** represents a strategy for a SyGuS datatype type */
   class EnumTypeInfoStrat {
@@ -354,8 +400,7 @@ private:
     std::vector< TypeNode > d_csol_cts;
     std::vector< Node > d_cenum;
   };
-  
-  
+
   /** stores enumerators and strategies for a SyGuS datatype type */
   class EnumTypeInfo {
   public:
@@ -368,9 +413,9 @@ private:
     std::map< Node, EnumTypeInfoStrat > d_strat;
     bool isSolved( CegConjecturePbe * pbe );
   };
-  
-  
-  /** stores strategy and enumeration information for a function-to-synthesize */
+
+  /** stores strategy and enumeration information for a function-to-synthesize
+   */
   class CandidateInfo {
   public:
     CandidateInfo() : d_check_sol( false ), d_cond_count( 0 ){}
@@ -380,7 +425,8 @@ private:
     * of solutions.
     */
     TypeNode d_root;
-    /** Information for each SyGuS datatype type occurring in a field of d_root */
+    /** Information for each 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;
@@ -396,24 +442,31 @@ private:
   };
   /** maps a function-to-synthesize to the above information */
   std::map< Node, CandidateInfo > d_cinfo;
-  
+
   //------------------------------ representation of an enumeration strategy
   /** add enumerated value */
   void addEnumeratedValue( Node x, Node v, std::vector< Node >& lems );
   bool getExplanationForEnumeratorExclude( Node c, Node x, Node v, std::vector< Node >& results, EnumInfo& ei, std::vector< Node >& exp );
-  
+
   //------------------------------ strategy registration
-  void collectEnumeratorTypes( Node c, TypeNode tn, unsigned enum_role );
-  void registerEnumerator( Node et, Node c, TypeNode tn, unsigned enum_role, bool inSearch );
-  void staticLearnRedundantOps( Node c, std::vector< Node >& lemmas );
-  void staticLearnRedundantOps( Node c, Node e, std::map< Node, bool >& visited, std::vector< Node >& redundant, 
-                                std::vector< Node >& lemmas, int ind );
+  void collectEnumeratorTypes(Node c, TypeNode tn, unsigned enum_role);
+  void registerEnumerator(
+      Node et, Node c, TypeNode tn, unsigned enum_role, bool inSearch);
+  void staticLearnRedundantOps(Node c, std::vector<Node>& lemmas);
+  void staticLearnRedundantOps(Node c,
+                               Node e,
+                               std::map<Node, bool>& visited,
+                               std::vector<Node>& redundant,
+                               std::vector<Node>& lemmas,
+                               int ind);
 
   /** register candidate conditional */
-  bool inferTemplate( unsigned k, Node n, std::map< Node, unsigned >& templ_var_index, std::map< unsigned, unsigned >& templ_injection );  
-  //------------------------------ end strategy registration  
-  
-  
+  bool inferTemplate(unsigned k,
+                     Node n,
+                     std::map<Node, unsigned>& templ_var_index,
+                     std::map<unsigned, unsigned>& templ_injection);
+  //------------------------------ end strategy registration
+
   //------------------------------ constructing solutions
   class UnifContext {
   public:
@@ -453,16 +506,22 @@ private:
   * in context x, where ind is the term depth of the context.
   */
   Node constructSolution( Node c, Node e, UnifContext& x, int ind );
-  /** Heuristically choose the best solved term from solved in context x, currently return the first. */
+  /** 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. */
+  /** 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 */
+  /** 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 */
+  /** 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.
+  /** 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,
@@ -470,13 +529,13 @@ private:
                                     std::map< Node, std::vector< unsigned > > incr,
                                     UnifContext& x );
   //------------------------------ end constructing solutions
-  
-  /** get guard status 
+
+  /** get guard status
   * Returns 1 if g is asserted true in the SAT solver.
   * Returns -1 if g is asserted false in the SAT solver.
   * Returns 0 otherwise.
   */
-  int getGuardStatus( Node g );
+  int getGuardStatus(Node g);
 };
 
 
diff --git a/src/theory/quantifiers/sygus_process_conj.cpp b/src/theory/quantifiers/sygus_process_conj.cpp
new file mode 100644
index 000000000..600c09a58
--- /dev/null
+++ b/src/theory/quantifiers/sygus_process_conj.cpp
@@ -0,0 +1,97 @@
+/*********************                                                        */
+/*! \file sygus_process_conj.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 techniqures for static preprocessing and analysis
+ ** of sygus conjectures.
+ **/
+#include "theory/quantifiers/sygus_process_conj.h"
+
+#include <stack>
+
+#include "expr/datatype.h"
+#include "theory/quantifiers/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
+
+using namespace CVC4::kind;
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+CegConjectureProcess::CegConjectureProcess(QuantifiersEngine* qe) : d_qe(qe) {}
+CegConjectureProcess::~CegConjectureProcess() {}
+Node CegConjectureProcess::simplify(Node q)
+{
+  Trace("sygus-process") << "Simplify conjecture : " << q << std::endl;
+
+  return q;
+}
+
+void CegConjectureProcess::initialize(Node n, std::vector<Node>& candidates)
+{
+  if (Trace.isOn("sygus-process"))
+  {
+    Trace("sygus-process") << "Process conjecture : " << n
+                           << " with candidates: " << std::endl;
+    for (unsigned i = 0; i < candidates.size(); i++)
+    {
+      Trace("sygus-process") << "  " << candidates[i] << std::endl;
+    }
+  }
+  Node base;
+  if (n.getKind() == NOT && n[0].getKind() == FORALL)
+  {
+    base = n[0][1];
+  }
+  else
+  {
+    base = n;
+  }
+
+  std::vector<Node> conj;
+  if (base.getKind() == AND)
+  {
+    for (unsigned i = 0; i < base.getNumChildren(); i++)
+    {
+      conj.push_back(base[i]);
+    }
+  }
+  else
+  {
+    conj.push_back(base);
+  }
+
+  // initialize the information for synth funs
+  for (unsigned i = 0; i < candidates.size(); i++)
+  {
+    Node e = candidates[i];
+    // d_sf_info[e].d_arg_independent
+  }
+
+  // process the conjunctions
+  for (unsigned i = 0; i < conj.size(); i++)
+  {
+    processConjunct(conj[i]);
+  }
+}
+
+void CegConjectureProcess::processConjunct(Node c) {}
+Node CegConjectureProcess::getSymmetryBreakingPredicate(
+    Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth)
+{
+  return Node::null();
+}
+
+void CegConjectureProcess::debugPrint(const char* c) {}
+} /* namespace CVC4::theory::quantifiers */
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
diff --git a/src/theory/quantifiers/sygus_process_conj.h b/src/theory/quantifiers/sygus_process_conj.h
new file mode 100644
index 000000000..4637ae551
--- /dev/null
+++ b/src/theory/quantifiers/sygus_process_conj.h
@@ -0,0 +1,99 @@
+/*********************                                                        */
+/*! \file sygus_process_conj.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 Techniqures for static preprocessing and analysis of
+ ** sygus conjectures.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_PPROCESS_CONJ_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS_PROCESSS_CONJ_H
+
+#include "expr/node.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** This structure stores information regarding conjecture-specific
+* analysis of a function to synthesize.
+*/
+struct CegSynthFunProcessInfo
+{
+ public:
+  CegSynthFunProcessInfo() {}
+  ~CegSynthFunProcessInfo() {}
+  /** the set of arguments that this synth-fun is independent of */
+  std::map<unsigned, bool> d_arg_independent;
+};
+
+/** Ceg Conjecture Process
+*
+* This class implements static techniques for preprocessing and analysis of
+* sygus conjectures.
+*
+* It is used as a back-end to CegConjecture, which calls it using the following
+* interface:
+* (1) When a sygus conjecture is asserted, we call
+* CegConjectureProcess::simplify( q ),
+*     where q is the sygus conjecture in original form.
+*
+* (2) After a sygus conjecture is simplified and converted to deep
+* embedding form, we call CegConjectureProcess::initialize( n, candidates ).
+*
+* (3) During enumerative SyGuS search, calls may be made by
+* the extension of the quantifier-free datatypes decision procedure for
+* sygus to CegConjectureProcess::getSymmetryBreakingPredicate(...), which are
+* used for pruning search space based on conjecture-specific analysis.
+*/
+class CegConjectureProcess
+{
+ public:
+  CegConjectureProcess(QuantifiersEngine* qe);
+  ~CegConjectureProcess();
+  /** simplify the synthesis conjecture q
+  * Returns a formula that is equivalent to q.
+  */
+  Node simplify(Node q);
+  /** initialize
+  *
+  * n is the "base instantiation" of the deep-embedding version of
+  *   the synthesis conjecture under "candidates".
+  *   (see CegConjecture::d_base_inst)
+  */
+  void initialize(Node n, std::vector<Node>& candidates);
+  /** get symmetry breaking predicate
+  *
+  * Returns a formula that restricts the enumerative search space (for a given
+  * depth) for a term x of sygus type tn whose top symbol is the tindex^{th}
+  * constructor, where x is a subterm of enumerator e.
+  */
+  Node getSymmetryBreakingPredicate(
+      Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth);
+  /** print out debug information about this conjecture */
+  void debugPrint(const char* c);
+
+ private:
+  /** process conjunct */
+  void processConjunct(Node c);
+  /** for each synth-fun, information that is specific to this conjecture */
+  std::map<Node, CegSynthFunProcessInfo> d_sf_info;
+  /** reference to quantifier engine */
+  QuantifiersEngine* d_qe;
+};
+
+} /* namespace CVC4::theory::quantifiers */
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
+
+#endif
diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp
index a12397d8c..f298e9711 100644
--- a/src/theory/quantifiers/term_database_sygus.cpp
+++ b/src/theory/quantifiers/term_database_sygus.cpp
@@ -1368,11 +1368,15 @@ void TermDbSygus::registerSygusType( TypeNode tn ) {
   }
 }
 
-void TermDbSygus::registerMeasuredTerm(Node e, CegConjecture* conj,
-                                       bool mkActiveGuard) {
+void TermDbSygus::registerEnumerator(Node e,
+                                     Node f,
+                                     CegConjecture* conj,
+                                     bool mkActiveGuard)
+{
   Assert(d_enum_to_conjecture.find(e) == d_enum_to_conjecture.end());
   Trace("sygus-db") << "Register measured term : " << e << std::endl;
   d_enum_to_conjecture[e] = conj;
+  d_enum_to_synth_fun[e] = f;
   if( mkActiveGuard ){
     // make the guard
     Node eg = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "eG", NodeManager::currentNM()->booleanType() ) );
@@ -1387,11 +1391,13 @@ void TermDbSygus::registerMeasuredTerm(Node e, CegConjecture* conj,
   }
 }
 
-bool TermDbSygus::isMeasuredTerm(Node e) const {
+bool TermDbSygus::isEnumerator(Node e) const
+{
   return d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end();
 }
 
-CegConjecture* TermDbSygus::getConjectureFor(Node e) {
+CegConjecture* TermDbSygus::getConjectureForEnumerator(Node e)
+{
   std::map<Node, CegConjecture*>::iterator itm = d_enum_to_conjecture.find(e);
   if (itm != d_enum_to_conjecture.end()) {
     return itm->second;
@@ -1400,7 +1406,21 @@ CegConjecture* TermDbSygus::getConjectureFor(Node e) {
   }
 }
 
-Node TermDbSygus::getActiveGuardForMeasureTerm( Node e ) {
+Node TermDbSygus::getSynthFunForEnumerator(Node e)
+{
+  std::map<Node, Node>::iterator itsf = d_enum_to_synth_fun.find(e);
+  if (itsf != d_enum_to_synth_fun.end())
+  {
+    return itsf->second;
+  }
+  else
+  {
+    return Node::null();
+  }
+}
+
+Node TermDbSygus::getActiveGuardForEnumerator(Node e)
+{
   std::map<Node, Node>::iterator itag = d_enum_to_active_guard.find(e);
   if (itag != d_enum_to_active_guard.end()) {
     return itag->second;
@@ -1409,7 +1429,8 @@ Node TermDbSygus::getActiveGuardForMeasureTerm( Node e ) {
   }
 }
 
-void TermDbSygus::getMeasuredTerms( std::vector< Node >& mts ) {
+void TermDbSygus::getEnumerators(std::vector<Node>& mts)
+{
   for (std::map<Node, CegConjecture*>::iterator itm =
            d_enum_to_conjecture.begin();
        itm != d_enum_to_conjecture.end(); ++itm) {
diff --git a/src/theory/quantifiers/term_database_sygus.h b/src/theory/quantifiers/term_database_sygus.h
index 768047734..030963b58 100644
--- a/src/theory/quantifiers/term_database_sygus.h
+++ b/src/theory/quantifiers/term_database_sygus.h
@@ -83,6 +83,9 @@ private:
 private:
  /** mapping from enumerator terms to the conjecture they are associated with */
  std::map<Node, CegConjecture*> d_enum_to_conjecture;
+ /** mapping from enumerator terms to the function-to-synthesize they are
+  * associated with */
+ std::map<Node, Node> d_enum_to_synth_fun;
  /** mapping from enumerator terms to the guard they are associated with
  * The guard G for an enumerator e has the semantics
  *   "if G is true, then there are more values of e to enumerate".
@@ -129,21 +132,31 @@ public:
   /** register the sygus type */
   void registerSygusType( TypeNode tn );
   /** register a variable e that we will do enumerative search on
-   * conj is the conjecture that the enumeration for e is for.
+   * conj is the conjecture that the enumeration of e is for.
+   * f is the synth-fun that the enumeration of e is for.
    * mkActiveGuard is whether we want to make a active guard for e (see
    * d_enum_to_active_guard)
+   *
+   * Notice that enumerator e may not be equivalent
+   * to f in synthesis-through-unification approaches
+   * (e.g. decision tree construction for PBE synthesis).
    */
-  void registerMeasuredTerm(Node e, CegConjecture* conj,
-                            bool mkActiveGuard = false);
-  /** is e a measured term (enumerator)? */
-  bool isMeasuredTerm(Node e) const;
+  void registerEnumerator(Node e,
+                          Node f,
+                          CegConjecture* conj,
+                          bool mkActiveGuard = false);
+  /** is e an enumerator? */
+  bool isEnumerator(Node e) const;
   /** return the conjecture e is associated with */
-  CegConjecture* getConjectureFor(Node e);
+  CegConjecture* getConjectureForEnumerator(Node e);
+  /** return the function-to-synthesize e is associated with */
+  Node getSynthFunForEnumerator(Node e);
   /** get active guard for e */
-  Node getActiveGuardForMeasureTerm( Node e );
-  /** get all registered measure terms (enumerators) */
-  void getMeasuredTerms( std::vector< Node >& mts );
-public:  //general sygus utilities
+  Node getActiveGuardForEnumerator(Node e);
+  /** get all registered enumerators */
+  void getEnumerators(std::vector<Node>& mts);
+
+ public:  // general sygus utilities
   bool isRegistered( TypeNode tn );
   // get the minimum depth of type in its parent grammar
   unsigned getMinTypeDepth( TypeNode root_tn, TypeNode tn );