Sygus enumerators to conjecture (#1237)

* Initial revision of mapping sygus enumeration terms to CegConjectures. This will allow us to generalize conjecture-specific symmetry breaking.

* Change function names, simplify.

* Fix assertion, minor optimization

* Cleanup, documentation, simplification.

* Address review.

* Apply clang format.

8 files changed, 444 insertions, 313 deletions

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index bae3a9a88..c543c16e2 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -14,14 +14,15 @@
  ** Implementation of sygus utilities for theory of datatypes
  **/
 
+#include "theory/datatypes/datatypes_sygus.h"
 
 #include "expr/node_manager.h"
 #include "options/quantifiers_options.h"
 #include "theory/datatypes/datatypes_rewriter.h"
-#include "theory/datatypes/datatypes_sygus.h"
+#include "theory/datatypes/theory_datatypes.h"
+#include "theory/quantifiers/ce_guided_conjecture.h"
 #include "theory/quantifiers/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/datatypes/theory_datatypes.h"
 #include "theory/theory_model.h"
 
 using namespace CVC4;
@@ -246,7 +247,7 @@ void SygusSymBreakNew::registerTerm( Node n, std::vector< Node >& lemmas ) {
       std::map< Node, Node >::iterator it = d_term_to_anchor.find( n[0] );
       if( it!=d_term_to_anchor.end() ) {
         d_term_to_anchor[n] = it->second;
-        d_term_to_anchor_root[n] = d_term_to_anchor_root[n[0]];
+        d_term_to_anchor_conj[n] = d_term_to_anchor_conj[n[0]];
         d = d_term_to_depth[n[0]] + 1;
         is_top_level = computeTopLevel( tn, n[0] );
         success = true;
@@ -255,9 +256,9 @@ 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_root[n] = d_tds->isMeasuredTerm( n );
+        d_term_to_anchor_conj[n] = d_tds->getConjectureFor(n);
         // this assertion fails if we have a sygus term in the search that is unmeasured
-        Assert( !d_term_to_anchor_root[n].isNull() );
+        Assert(d_term_to_anchor_conj[n] != NULL);
         d = 0;
         is_top_level = true;
         success = true;
@@ -696,72 +697,134 @@ void SygusSymBreakNew::registerSearchTerm( TypeNode tn, unsigned d, Node n, bool
   }
 }
 
+/** EquivSygusInvarianceTest
+*
+* This class is used to construct a minimal shape of a term that is equivalent
+* up to rewriting to a RHS value,
+* given as input bvr.
+*
+* For example,
+*
+* ite( t>0, 0, 0 ) + s*0 ----> 0
+*
+* can be minimized to:
+*
+* ite( _, 0, 0 ) + _*0 ----> 0
+*
+* It also manages the case where the rewriting is invariant wrt a finite set of
+* examples occurring in the conjecture.
+*
+* It is an instance of quantifiers::SygusInvarianceTest which is the standard
+* interface for term generalization via
+* the TermRecBuild utility, which traverses the AST of a given term, replaces
+* each subterm by a fresh variable and
+* check whether the invariant, as specified by this class (equivalent up to
+* rewriting to a RHS) holds.
+*
+* For details, see Reynolds et al SYNT 2017.
+*/
 class EquivSygusInvarianceTest : public quantifiers::SygusInvarianceTest {
 public:
   EquivSygusInvarianceTest(){}
   ~EquivSygusInvarianceTest(){}
-  Node d_ex_ar;
-  Node d_bvr;
-  std::vector< Node > d_exo;
-  void init( quantifiers::TermDbSygus * tds, TypeNode tn, Node ar, Node bvr ) {
+  /** initialize this invariance test
+  * tn is the sygus type for e
+  * aconj/e are used for conjecture-specific symmetry breaking
+  * bvr is the builtin version of the right hand side of the rewrite that we are
+  * checking for invariance
+  */
+  void init(quantifiers::TermDbSygus* tds, TypeNode tn,
+            quantifiers::CegConjecture* aconj, Node e, Node bvr) {
     //compute the current examples
     d_bvr = bvr;
-    if( tds->hasPbeExamples( ar ) ){
-      d_ex_ar = ar;
-      unsigned nex = tds->getNumPbeExamples( ar );
+    if (aconj->getPbe()->hasExamples(e)) {
+      d_conj = aconj;
+      d_enum = e;
+      unsigned nex = aconj->getPbe()->getNumExamples(e);
       for( unsigned i=0; i<nex; i++ ){
-        d_exo.push_back( tds->evaluateBuiltin( tn, bvr, ar, i ) );
+        d_exo.push_back(d_conj->getPbe()->evaluateBuiltin(tn, bvr, e, i));
       }
     }
   }
 protected:
-  bool invariant( quantifiers::TermDbSygus * tds, Node nvn, Node x ){
-    TypeNode tn = nvn.getType();
-    Node nbv = tds->sygusToBuiltin( nvn, tn );
-    Node nbvr = tds->extendedRewrite( nbv );
-    Trace("sygus-sb-mexp-debug") << "  min-exp check : " << nbv << " -> " << nbvr << std::endl;
-    bool exc_arg = false;
-    // equivalent / singular up to normalization
-    if( nbvr==d_bvr ){
-      // gives the same result : then the explanation for the child is irrelevant 
-      exc_arg = true;
-      Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin( nvn ) << " is rewritten to " << nbvr;
-      Trace("sygus-sb-mexp") << " regardless of the content of " << tds->sygusToBuiltin( x ) << std::endl;
-    }else{
-      if( nbvr.isVar() ){
-        TypeNode xtn = x.getType();
-        if( xtn==tn ){
-          Node bx = tds->sygusToBuiltin( x, xtn );
-          Assert( bx.getType()==nbvr.getType() );
-          if( nbvr==bx ){
-            Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin( nvn ) << " always rewrites to argument " << nbvr << std::endl;
-            // rewrites to the variable : then the explanation of this is irrelevant as well
-            exc_arg = true;
-            d_bvr = nbvr;
-          }
-        }
-      }
-    }
-    // equivalent under examples
-    if( !exc_arg ){
-      if( !d_ex_ar.isNull() ){
-        bool ex_equiv = true;
-        for( unsigned j=0; j<d_exo.size(); j++ ){
-          Node nbvr_ex = tds->evaluateBuiltin( tn, nbvr, d_ex_ar, j );
-          if( nbvr_ex!=d_exo[j] ){
-            ex_equiv = false;
-            break;
-          }
-        }
-        if( ex_equiv ){
-          Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin( nvn );
-          Trace("sygus-sb-mexp") << " is the same w.r.t. examples regardless of the content of " << tds->sygusToBuiltin( x ) << std::endl;
-          exc_arg = true;
-        }
-      }
-    }
-    return exc_arg;
+ /** does nvn still rewrite to d_bvr? */
+ bool invariant(quantifiers::TermDbSygus* tds, Node nvn, Node x) {
+   TypeNode tn = nvn.getType();
+   Node nbv = tds->sygusToBuiltin(nvn, tn);
+   Node nbvr = tds->extendedRewrite(nbv);
+   Trace("sygus-sb-mexp-debug") << "  min-exp check : " << nbv << " -> " << nbvr
+                                << std::endl;
+   bool exc_arg = false;
+   // equivalent / singular up to normalization
+   if (nbvr == d_bvr) {
+     // gives the same result : then the explanation for the child is irrelevant
+     exc_arg = true;
+     Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn)
+                            << " is rewritten to " << nbvr;
+     Trace("sygus-sb-mexp") << " regardless of the content of "
+                            << tds->sygusToBuiltin(x) << std::endl;
+   } else {
+     if (nbvr.isVar()) {
+       TypeNode xtn = x.getType();
+       if (xtn == tn) {
+         Node bx = tds->sygusToBuiltin(x, xtn);
+         Assert(bx.getType() == nbvr.getType());
+         if (nbvr == bx) {
+           Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn)
+                                  << " always rewrites to argument " << nbvr
+                                  << std::endl;
+           // rewrites to the variable : then the explanation of this is
+           // irrelevant as well
+           exc_arg = true;
+           d_bvr = nbvr;
+         }
+       }
+     }
+   }
+   // equivalent under examples
+   if (!exc_arg) {
+     if (!d_enum.isNull()) {
+       bool ex_equiv = true;
+       for (unsigned j = 0; j < d_exo.size(); j++) {
+         Node nbvr_ex = d_conj->getPbe()->evaluateBuiltin(tn, nbvr, d_enum, j);
+         if (nbvr_ex != d_exo[j]) {
+           ex_equiv = false;
+           break;
+         }
+       }
+       if (ex_equiv) {
+         Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn);
+         Trace("sygus-sb-mexp")
+             << " is the same w.r.t. examples regardless of the content of "
+             << tds->sygusToBuiltin(x) << std::endl;
+         exc_arg = true;
+       }
+     }
+   }
+   return exc_arg;
   }
+
+ private:
+  /** the conjecture associated with the enumerator d_enum */
+  quantifiers::CegConjecture* d_conj;
+  /** the enumerator associated with the term we are doing an invariance test
+   * for */
+  Node d_enum;
+  /** the RHS of the evaluation */
+  Node d_bvr;
+  /** the result of the examples
+  * This is a finer-grained version of d_bvr, where for example if our input
+  * examples are:
+  * (x,y,z) = (3,2,4), (5,2,6), (3,2,1)
+  * On these examples, we have:
+  *
+  * ite( x>y, z, 0) ---> 4,6,1
+  *
+  * which can be minimized to:
+  *
+  * ite( x>y, z, _) ---> 4,6,1
+  */
+  std::vector<Node> d_exo;
 };
 
 
@@ -804,9 +867,9 @@ bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d,
   if( d_cache[a].d_search_val_proc.find( nv )==d_cache[a].d_search_val_proc.end() ){
     d_cache[a].d_search_val_proc[nv] = true;
     // get the root (for PBE symmetry breaking)
-    Assert( d_term_to_anchor_root.find( a )!=d_term_to_anchor_root.end() );
-    Node ar = d_term_to_anchor_root[a];
-    Assert( !ar.isNull() );
+    Assert(d_term_to_anchor_conj.find(a) != d_term_to_anchor_conj.end());
+    quantifiers::CegConjecture* aconj = d_term_to_anchor_conj[a];
+    Assert(aconj != NULL);
     Trace("sygus-sb-debug") << "  ...register search value " << nv << ", type=" << tn << std::endl;
     Node bv = d_tds->sygusToBuiltin( nv, tn );
     Trace("sygus-sb-debug") << "  ......builtin is " << bv << std::endl;
@@ -826,8 +889,14 @@ bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d,
       Node bad_val_bvr;
       bool by_examples = false;
       if( itsv==d_cache[a].d_search_val[tn].end() ){
+        // TODO (github #1210) conjecture-specific symmetry breaking
+        // this should be generalized and encapsulated within the CegConjecture
+        // class
         // is it equivalent under examples?
-        Node bvr_equiv = d_tds->addPbeSearchVal( tn, ar, bvr );
+        Node bvr_equiv;
+        if (aconj->getPbe()->hasExamples(a)) {
+          bvr_equiv = aconj->getPbe()->addSearchVal(tn, a, bvr);
+        }
         if( !bvr_equiv.isNull() ){
           if( bvr_equiv!=bvr ){
             Trace("sygus-sb-debug") << "......adding search val for " << bvr << " returned " << bvr_equiv << std::endl;
@@ -878,7 +947,7 @@ bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d,
         
         // do analysis of the evaluation  FIXME: does not work (evaluation is non-constant)
         EquivSygusInvarianceTest eset;
-        eset.init( d_tds, tn, ar, bvr );
+        eset.init(d_tds, tn, aconj, a, bvr);
         Trace("sygus-sb-mexp-debug") << "Minimize explanation for eval[" << d_tds->sygusToBuiltin( bad_val ) << "] = " << bvr << std::endl;
         d_tds->getExplanationFor( x, bad_val, exp, eset, bad_val_o, sz );
         do_exclude = true;
@@ -979,7 +1048,7 @@ 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 ).isNull() ){
+        if (d_tds->isMeasuredTerm(e)) {
           d_register_st[e] = true;
           Node ag = d_tds->getActiveGuardForMeasureTerm( e );
           if( !ag.isNull() ){
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index 7d88447ea..3e37fe728 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -22,13 +22,14 @@
 #include <iostream>
 #include <map>
 
-#include "expr/node.h"
-#include "expr/datatype.h"
-#include "context/context.h"
 #include "context/cdchunk_list.h"
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "context/cdo.h"
+#include "context/context.h"
+#include "expr/datatype.h"
+#include "expr/node.h"
+#include "theory/quantifiers/ce_guided_conjecture.h"
 #include "theory/quantifiers/term_database.h"
 
 namespace CVC4 {
@@ -69,7 +70,7 @@ private:
   Node d_zero;
 private:
   std::map< Node, Node > d_term_to_anchor;
-  std::map< Node, Node > d_term_to_anchor_root;
+  std::map<Node, quantifiers::CegConjecture*> d_term_to_anchor_conj;
   std::map< Node, unsigned > d_term_to_depth;
   std::map< Node, bool > d_is_top_level;
   void registerTerm( Node n, std::vector< Node >& lemmas );
diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp
index 745c64b35..a838a6a0c 100644
--- a/src/theory/quantifiers/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/ce_guided_conjecture.cpp
@@ -106,19 +106,10 @@ void CegConjecture::assign( Node q ) {
   if( !isSingleInvocation() ){
     if( options::sygusPbe() ){
       d_ceg_pbe->initialize( d_base_inst, d_candidates, guarded_lemmas );
-    }
-    for( unsigned i=0; i<d_candidates.size(); i++ ){
-      Node e = d_candidates[i];
-      if( options::sygusPbe() ){
-        std::vector< std::vector< Node > > exs;
-        std::vector< Node > exos;
-        std::vector< Node > exts;
-        // use the PBE examples, regardless of the search algorithm, since these help search space pruning
-        if( d_ceg_pbe->getPbeExamples( e, exs, exos, exts ) ){
-          d_qe->getTermDatabaseSygus()->registerPbeExamples( e, exs, exos, exts );
-        }
-      }else{
-        d_qe->getTermDatabaseSygus()->registerMeasuredTerm( e, e );
+    } else {
+      for (unsigned i = 0; i < d_candidates.size(); i++) {
+        Node e = d_candidates[i];
+        d_qe->getTermDatabaseSygus()->registerMeasuredTerm(e, this);
       }
     }
   }
diff --git a/src/theory/quantifiers/ce_guided_conjecture.h b/src/theory/quantifiers/ce_guided_conjecture.h
index c99867ac7..dfd9c1623 100644
--- a/src/theory/quantifiers/ce_guided_conjecture.h
+++ b/src/theory/quantifiers/ce_guided_conjecture.h
@@ -27,7 +27,15 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-/** a synthesis conjecture */
+/** a synthesis conjecture
+ * 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.
+ */
 class CegConjecture {
 public:
   CegConjecture( QuantifiersEngine * qe );
@@ -40,7 +48,7 @@ public:
   Node getNextDecisionRequest( unsigned& priority );
   /** 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 do_Check below */
+  /** whether the conjecture is waiting for a call to doCheck below */
   bool needsCheck( std::vector< Node >& lem );
   /** whether the conjecture is waiting for a call to doRefine below */
   bool needsRefinement();
@@ -94,6 +102,8 @@ public:
   Node getRefinementLemma( unsigned i ) { return d_refinement_lemmas[i]; }
   /** get refinement lemma */
   Node getRefinementBaseLemma( unsigned i ) { return d_refinement_lemmas_base[i]; }
+  /** get program by examples utility */
+  CegConjecturePbe* getPbe() { return d_ceg_pbe; }
   /** print out debug information about this conjecture */
   void debugPrint( const char * c );
 private:
diff --git a/src/theory/quantifiers/ce_guided_pbe.cpp b/src/theory/quantifiers/ce_guided_pbe.cpp
index 9fa87c11d..ac09a31d0 100644
--- a/src/theory/quantifiers/ce_guided_pbe.cpp
+++ b/src/theory/quantifiers/ce_guided_pbe.cpp
@@ -199,26 +199,138 @@ 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], candidates[i] );
+      d_qe->getTermDatabaseSygus()->registerMeasuredTerm(candidates[i],
+                                                         d_parent);
     }
   }
 }
 
-bool CegConjecturePbe::getPbeExamples( Node v, std::vector< std::vector< Node > >& exs, 
-                                       std::vector< Node >& exos, std::vector< Node >& exts ) {
-  std::map< Node, bool >::iterator itx = d_examples_invalid.find( v );
-  if( itx==d_examples_invalid.end() ){
-    Assert( d_examples.find( v )!=d_examples.end() );
-    exs = d_examples[v];
-    Assert( d_examples_out.find( v )!=d_examples_out.end() );
-    exos = d_examples_out[v];
-    Assert( d_examples_term.find( v )!=d_examples_term.end() );
-    exts = d_examples_term[v];
-    return true;
+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()) {
+      d_lazy_child = b;
+    }
+    return d_lazy_child;
+  } else {
+    std::vector<Node> ex;
+    if (d_children.empty()) {
+      if (d_lazy_child.isNull()) {
+        d_lazy_child = b;
+        return d_lazy_child;
+      } else {
+        // evaluate the lazy child
+        Assert(cpbe->d_examples.find(e) != cpbe->d_examples.end());
+        Assert(index < cpbe->d_examples[e].size());
+        ex = cpbe->d_examples[e][index];
+        addPbeExampleEval(etn, e, d_lazy_child, ex, cpbe, index, ntotal);
+        Assert(!d_children.empty());
+        d_lazy_child = Node::null();
+      }
+    } else {
+      Assert(cpbe->d_examples.find(e) != cpbe->d_examples.end());
+      Assert(index < cpbe->d_examples[e].size());
+      ex = cpbe->d_examples[e][index];
+    }
+    return addPbeExampleEval(etn, e, b, ex, cpbe, index, ntotal);
+  }
+}
+
+Node CegConjecturePbe::PbeTrie::addPbeExampleEval(TypeNode etn, Node e, Node b,
+                                                  std::vector<Node>& ex,
+                                                  CegConjecturePbe* cpbe,
+                                                  unsigned index,
+                                                  unsigned ntotal) {
+  Node eb = cpbe->d_tds->evaluateBuiltin(etn, b, ex);
+  return d_children[eb].addPbeExample(etn, e, b, cpbe, index + 1, ntotal);
+}
+
+bool CegConjecturePbe::hasExamples(Node e) {
+  if (isPbe()) {
+    e = getCandidateForEnumerator(e);
+    std::map<Node, bool>::iterator itx = d_examples_invalid.find(e);
+    if (itx == d_examples_invalid.end()) {
+      return d_examples.find(e) != d_examples.end();
+    }
   }
   return false;
 }
 
+unsigned CegConjecturePbe::getNumExamples(Node e) {
+  e = getCandidateForEnumerator(e);
+  std::map<Node, std::vector<std::vector<Node> > >::iterator it =
+      d_examples.find(e);
+  if (it != d_examples.end()) {
+    return it->second.size();
+  } else {
+    return 0;
+  }
+}
+
+void CegConjecturePbe::getExample(Node e, unsigned i, std::vector<Node>& ex) {
+  e = getCandidateForEnumerator(e);
+  std::map<Node, std::vector<std::vector<Node> > >::iterator it =
+      d_examples.find(e);
+  if (it != d_examples.end()) {
+    Assert(i < it->second.size());
+    ex.insert(ex.end(), it->second[i].begin(), it->second[i].end());
+  } else {
+    Assert(false);
+  }
+}
+
+Node CegConjecturePbe::getExampleOut(Node e, unsigned i) {
+  e = getCandidateForEnumerator(e);
+  std::map<Node, std::vector<Node> >::iterator it = d_examples_out.find(e);
+  if (it != d_examples_out.end()) {
+    Assert(i < it->second.size());
+    return it->second[i];
+  } else {
+    Assert(false);
+    return Node::null();
+  }
+}
+
+Node CegConjecturePbe::addSearchVal(TypeNode tn, Node e, Node bvr) {
+  Assert(isPbe());
+  Assert(!e.isNull());
+  e = getCandidateForEnumerator(e);
+  std::map<Node, bool>::iterator itx = d_examples_invalid.find(e);
+  if (itx == d_examples_invalid.end()) {
+    unsigned nex = d_examples[e].size();
+    Node ret = d_pbe_trie[e][tn].addPbeExample(tn, e, bvr, this, 0, nex);
+    Assert(ret.getType() == bvr.getType());
+    return ret;
+  }
+  return Node::null();
+}
+
+Node CegConjecturePbe::evaluateBuiltin(TypeNode tn, Node bn, Node e,
+                                       unsigned i) {
+  e = getCandidateForEnumerator(e);
+  std::map<Node, bool>::iterator itx = d_examples_invalid.find(e);
+  if (itx == d_examples_invalid.end()) {
+    std::map<Node, std::vector<std::vector<Node> > >::iterator it =
+        d_examples.find(e);
+    if (it != d_examples.end()) {
+      Assert(i < it->second.size());
+      return d_tds->evaluateBuiltin(tn, bn, it->second[i]);
+    }
+  }
+  return Rewriter::rewrite(bn);
+}
+
+Node CegConjecturePbe::getCandidateForEnumerator(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
 
@@ -239,7 +351,8 @@ 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_qe->getTermDatabaseSygus()->registerMeasuredTerm( et, c, true );
+      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 );
     }else{
       Trace("sygus-unif-debug") << "Make " << et << " a slave of " << itn->second << std::endl;
@@ -650,7 +763,6 @@ void CegConjecturePbe::staticLearnRedundantOps( Node c, Node e, std::map< Node,
   }
 }
 
-
 // ------------------------------------------- solution construction from enumeration
 
 void CegConjecturePbe::getCandidateList( std::vector< Node >& candidates, std::vector< Node >& clist ) {
@@ -873,13 +985,16 @@ public:
   Node d_ar;
   std::vector< Node > d_exo;
   std::vector< unsigned > d_neg_con_indices;
-  
-  void init( quantifiers::TermDbSygus * tds, Node ar, std::vector< Node >& exo, std::vector< unsigned >& ncind ) {
-    if( tds->hasPbeExamples( ar ) ){
-      Assert( tds->getNumPbeExamples( ar )==exo.size() );
+  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;
       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:  
@@ -892,7 +1007,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 = tds->evaluateBuiltin( tn, nbvr, d_ar, ii );
+        Node nbvre = d_cpbe->evaluateBuiltin(tn, nbvr, d_ar, ii);
         Node out = d_exo[ii];
         Node cont = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, out, nbvre );
         Node contr = Rewriter::rewrite( cont );
@@ -902,7 +1017,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;
-            tds->getPbeExample( d_ar, ii, ex );
+            d_cpbe->getExample(d_ar, ii, ex);
             for( unsigned j=0; j<ex.size(); j++ ){
               Trace("sygus-pbe-cterm") << ex[j] << " ";
             }
@@ -959,7 +1074,7 @@ bool CegConjecturePbe::getExplanationForEnumeratorExclude( Node c, Node x, Node
       if( !cmp_indices.empty() ){
         //set up the inclusion set
         NegContainsSygusInvarianceTest ncset;
-        ncset.init( d_tds, c, itxo->second, cmp_indices );
+        ncset.init(this, c, 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;
diff --git a/src/theory/quantifiers/ce_guided_pbe.h b/src/theory/quantifiers/ce_guided_pbe.h
index f40f29b2a..2f6f591ba 100644
--- a/src/theory/quantifiers/ce_guided_pbe.h
+++ b/src/theory/quantifiers/ce_guided_pbe.h
@@ -29,18 +29,52 @@ class CegConjecture;
 class CegConjecturePbe;
 class CegEntailmentInfer;
 
+/** CegConjecturePbe
+*
+* This class implements optimizations that target Programming-By-Examples (PBE)
+* synthesis conjectures.
+* [EX#1] An example of a PBE synthesis conjecture is:
+*
+* 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.
+*/
 class CegConjecturePbe {
 private:
   QuantifiersEngine* d_qe;
   quantifiers::TermDbSygus * d_tds;
   CegConjecture* d_parent;
 
+  /** for each candidate variable f (a function-to-synthesize), whether the
+  * conjecture is purely PBE for that variable
+  * In other words, all occurrences of f are guarded by equalities that
+  * constraint its arguments to constants.
+  */
   std::map< Node, bool > d_examples_invalid;
+  /** for each candidate variable (function-to-synthesize), whether the
+  * conjecture is purely PBE for that variable.
+  * An example of a conjecture for which d_examples_invalid is false but
+  * d_examples_out_invalid is true is:
+  * exists f. forall x. ( x = 0 => f( x ) > 2 )
+  */
   std::map< Node, bool > d_examples_out_invalid;
+  /** for each candidate variable (function-to-synthesize), input of I/O
+   * examples */
   std::map< Node, std::vector< std::vector< Node > > > d_examples;
+  /** 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 ) */
   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;
+
   void collectExamples( Node n, std::map< Node, bool >& visited, bool hasPol, bool pol );
   bool d_is_pbe;
 public:  
@@ -64,8 +98,49 @@ public:
   void initialize( Node n, std::vector< Node >& candidates, std::vector< Node >& lemmas );
   bool getPbeExamples( Node v, std::vector< std::vector< Node > >& exs, 
                        std::vector< Node >& exos, std::vector< Node >& exts);
+  /** is PBE enabled for any enumerator? */
   bool isPbe() { return d_is_pbe; }
-private:  // for registration
+  /** get candidate for enumerator */
+  Node getCandidateForEnumerator(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 */
+  unsigned getNumExamples(Node e);
+  /** get the input arguments for i^th I/O example for e, which is added to the
+   * vector ex */
+  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);
+  int getExampleId(Node n);
+  /** add the search val, returns an equivalent value (possibly the same) */
+  Node addSearchVal(TypeNode tn, Node e, Node bvr);
+  /** evaluate builtin */
+  Node evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i);
+
+ private:
+  /** this class is an index of candidate solutions for PBE synthesis */
+  class PbeTrie {
+   private:
+    Node addPbeExampleEval(TypeNode etn, Node e, Node b, std::vector<Node>& ex,
+                           CegConjecturePbe* cpbe, unsigned index,
+                           unsigned ntotal);
+
+   public:
+    PbeTrie() {}
+    ~PbeTrie() {}
+    Node d_lazy_child;
+    std::map<Node, PbeTrie> d_children;
+    void clear() { d_children.clear(); }
+    Node addPbeExample(TypeNode etn, Node e, Node b, CegConjecturePbe* cpbe,
+                       unsigned index, unsigned ntotal);
+  };
+  /** trie of candidate solutions tried, for each (enumerator, type),
+   * where type is a type in the grammar of the space of solutions for a subterm
+   * of e
+   */
+  std::map<Node, std::map<TypeNode, PbeTrie> > d_pbe_trie;
+
+ private:  // for 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 );
diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp
index f5c04fced..a12397d8c 100644
--- a/src/theory/quantifiers/term_database_sygus.cpp
+++ b/src/theory/quantifiers/term_database_sygus.cpp
@@ -19,9 +19,10 @@
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
 #include "smt/smt_engine.h"
-#include "theory/quantifiers/theory_quantifiers.h"
+#include "theory/quantifiers/ce_guided_conjecture.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers/theory_quantifiers.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
 
@@ -1367,10 +1368,11 @@ void TermDbSygus::registerSygusType( TypeNode tn ) {
   }
 }
 
-void TermDbSygus::registerMeasuredTerm( Node e, Node root, bool mkActiveGuard ) {
-  Assert( d_measured_term.find( e )==d_measured_term.end() );
-  Trace("sygus-db") << "Register measured term : " << e << " with root " << root << std::endl;
-  d_measured_term[e] = root;
+void TermDbSygus::registerMeasuredTerm(Node e, 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;
   if( mkActiveGuard ){
     // make the guard
     Node eg = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "eG", NodeManager::currentNM()->booleanType() ) );
@@ -1381,38 +1383,26 @@ void TermDbSygus::registerMeasuredTerm( Node e, Node root, bool mkActiveGuard )
     Node lem = NodeManager::currentNM()->mkNode( OR, eg, eg.negate() );
     Trace("cegqi-lemma") << "Cegqi::Lemma : enumerator : " << lem << std::endl;
     d_quantEngine->getOutputChannel().lemma( lem );
-    d_measured_term_active_guard[e] = eg;
+    d_enum_to_active_guard[e] = eg;
   }
 }
 
-void TermDbSygus::registerPbeExamples( Node e, std::vector< std::vector< Node > >& exs, 
-                                       std::vector< Node >& exos, std::vector< Node >& exts  ) {
-  Trace("sygus-db") << "Register " << exs.size() << " PBE examples with " << e << std::endl;
-  Assert( d_measured_term.find( e )==d_measured_term.end() || isMeasuredTerm( e )==e );
-  Assert( d_pbe_exs.find( e )==d_pbe_exs.end() );
-  Assert( exs.size()==exos.size() );
-  d_pbe_exs[e] = exs;
-  d_pbe_exos[e] = exos;
-  for( unsigned i=0; i<exts.size(); i++ ){
-    Trace("sygus-db-debug") << "  # " << i << " : " << exts[i] << std::endl;
-    Assert( exts[i].getKind()==APPLY_UF );
-    Assert( exts[i][0]==e );
-    d_pbe_term_id[exts[i]] = i;
-  }
+bool TermDbSygus::isMeasuredTerm(Node e) const {
+  return d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end();
 }
 
-Node TermDbSygus::isMeasuredTerm( Node e ) {
-  std::map< Node, Node >::iterator itm = d_measured_term.find( e );
-  if( itm!=d_measured_term.end() ){
+CegConjecture* TermDbSygus::getConjectureFor(Node e) {
+  std::map<Node, CegConjecture*>::iterator itm = d_enum_to_conjecture.find(e);
+  if (itm != d_enum_to_conjecture.end()) {
     return itm->second;
   }else{
-    return Node::null();
+    return NULL;
   }
 }
 
 Node TermDbSygus::getActiveGuardForMeasureTerm( Node e ) {
-  std::map< Node, Node >::iterator itag = d_measured_term_active_guard.find( e );
-  if( itag!=d_measured_term_active_guard.end() ){
+  std::map<Node, Node>::iterator itag = d_enum_to_active_guard.find(e);
+  if (itag != d_enum_to_active_guard.end()) {
     return itag->second;
   }else{
     return Node::null();
@@ -1420,54 +1410,13 @@ Node TermDbSygus::getActiveGuardForMeasureTerm( Node e ) {
 }
 
 void TermDbSygus::getMeasuredTerms( std::vector< Node >& mts ) {
-  for( std::map< Node, Node >::iterator itm = d_measured_term.begin(); itm != d_measured_term.end(); ++itm ){
+  for (std::map<Node, CegConjecture*>::iterator itm =
+           d_enum_to_conjecture.begin();
+       itm != d_enum_to_conjecture.end(); ++itm) {
     mts.push_back( itm->first );
   }
 }
 
-bool TermDbSygus::hasPbeExamples( Node e ) {
-  return d_pbe_exs.find( e )!=d_pbe_exs.end();
-}
-
-unsigned TermDbSygus::getNumPbeExamples( Node e ) {
-  std::map< Node, std::vector< std::vector< Node > > >::iterator it = d_pbe_exs.find( e );
-  if( it!=d_pbe_exs.end() ){
-    return it->second.size();
-  }else{
-    return 0;
-  }
-}
-
-void TermDbSygus::getPbeExample( Node e, unsigned i, std::vector< Node >& ex ) {
-  std::map< Node, std::vector< std::vector< Node > > >::iterator it = d_pbe_exs.find( e );
-  if( it!=d_pbe_exs.end() ){
-    Assert( i<it->second.size() );
-    Assert( i<d_pbe_exos[e].size() );
-    ex.insert( ex.end(), it->second[i].begin(), it->second[i].end() );
-  }else{
-    Assert( false );
-  }
-}
-Node TermDbSygus::getPbeExampleOut( Node e, unsigned i ) {
-  std::map< Node, std::vector< Node > >::iterator it = d_pbe_exos.find( e );
-  if( it!=d_pbe_exos.end() ){
-    Assert( i<it->second.size() );
-    return it->second[i];
-  }else{
-    Assert( false );
-    return Node::null();
-  }
-}
-
-int TermDbSygus::getPbeExampleId( Node n ) {
-  std::map< Node, unsigned >::iterator it = d_pbe_term_id.find( n );
-  if( it!=d_pbe_term_id.end() ){
-    return it->second;
-  }else{
-    return -1;
-  }
-}
-
 bool TermDbSygus::isRegistered( TypeNode tn ) {
   return d_register.find( tn )!=d_register.end();
 }
@@ -1942,7 +1891,8 @@ unsigned TermDbSygus::getAnchorDepth( Node n ) {
 void TermDbSygus::registerEvalTerm( Node n ) {
   if( options::sygusDirectEval() ){
     if( n.getKind()==APPLY_UF && !n.getType().isBoolean() ){
-      Trace("sygus-eager") << "TermDbSygus::eager: Register eval term : " << n << std::endl;
+      Trace("sygus-eager") << "TermDbSygus::eager: Register eval term : " << n
+                           << std::endl;
       TypeNode tn = n[0].getType();
       if( tn.isDatatype() ){
         const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
@@ -1950,15 +1900,6 @@ void TermDbSygus::registerEvalTerm( Node n ) {
           Node f = n.getOperator();
           Trace("sygus-eager") << "...the evaluation function is : " << f << std::endl;
           if( n[0].getKind()!=APPLY_CONSTRUCTOR ){
-            // check if it directly occurs in an input/ouput example
-            int pbe_id = getPbeExampleId( n );
-            if( pbe_id!=-1 ){
-              Node n_res = getPbeExampleOut( n[0], pbe_id );
-              if( !n_res.isNull() ){
-                Trace("sygus-eager") << "......do not evaluate " << n << " since it is an input/output example : " << n_res << std::endl;
-                return;
-              }
-            }
             d_evals[n[0]].push_back( n );
             TypeNode tn = n[0].getType();
             Assert( tn.isDatatype() );
@@ -2368,16 +2309,6 @@ Node TermDbSygus::evaluateBuiltin( TypeNode tn, Node bn, std::vector< Node >& ar
   }
 }
 
-Node TermDbSygus::evaluateBuiltin( TypeNode tn, Node bn, Node ar, unsigned i ) {
-  std::map< Node, std::vector< std::vector< Node > > >::iterator it = d_pbe_exs.find( ar );
-  if( it!=d_pbe_exs.end() ){
-    Assert( i<it->second.size() );
-    return evaluateBuiltin( tn, bn, it->second[i] );
-  }else{
-    return Rewriter::rewrite( bn );
-  }
-}
-
 Node TermDbSygus::evaluateWithUnfolding( Node n, std::map< Node, Node >& visited ) {
   std::map< Node, Node >::iterator it = visited.find( n );
   if( it==visited.end() ){
@@ -2448,50 +2379,6 @@ bool TermDbSygus::isGenericRedundant( TypeNode tn, unsigned i ) {
   }
 }
 
-Node TermDbSygus::PbeTrie::addPbeExample( TypeNode etn, Node e, Node b, quantifiers::TermDbSygus * tds, unsigned index, unsigned ntotal ) {
-  Assert( tds->getNumPbeExamples( e )==ntotal );
-  if( index==ntotal ){
-    //lazy child holds the leaf data
-    if( d_lazy_child.isNull() ){
-      d_lazy_child = b;
-    }
-    return d_lazy_child;
-  }else{
-    std::vector< Node > ex;
-    if( d_children.empty() ){
-      if( d_lazy_child.isNull() ){
-        d_lazy_child = b;
-        return d_lazy_child;
-      }else{
-        //evaluate the lazy child    
-        tds->getPbeExample( e, index, ex );
-        addPbeExampleEval( etn, e, d_lazy_child, ex, tds, index, ntotal );
-        Assert( !d_children.empty() );
-        d_lazy_child = Node::null();
-      }
-    }else{
-      tds->getPbeExample( e, index, ex );
-    }
-    return addPbeExampleEval( etn, e, b, ex, tds, index, ntotal );
-  }
-}
-
-Node TermDbSygus::PbeTrie::addPbeExampleEval( TypeNode etn, Node e, Node b, std::vector< Node >& ex, quantifiers::TermDbSygus * tds, unsigned index, unsigned ntotal ) {
-  Node eb = tds->evaluateBuiltin( etn, b, ex );
-  return d_children[eb].addPbeExample( etn, e, b, tds, index+1, ntotal );
-}
-
-Node TermDbSygus::addPbeSearchVal( TypeNode tn, Node e, Node bvr ){
-  Assert( !e.isNull() );
-  if( hasPbeExamples( e ) ){
-    unsigned nex = getNumPbeExamples( e );
-    Node ret = d_pbe_trie[e][tn].addPbeExample( tn, e, bvr, this, 0, nex );
-    Assert( ret.getType()==bvr.getType() );
-    return ret;
-  }
-  return Node::null();
-}
-
 Node TermDbSygus::extendedRewritePullIte( Node n ) {
   // generalize this?
   Assert( n.getNumChildren()==2 );
diff --git a/src/theory/quantifiers/term_database_sygus.h b/src/theory/quantifiers/term_database_sygus.h
index 8f55f55bd..768047734 100644
--- a/src/theory/quantifiers/term_database_sygus.h
+++ b/src/theory/quantifiers/term_database_sygus.h
@@ -23,6 +23,8 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class CegConjecture;
+
 class SygusInvarianceTest {
 protected:
   // check whether nvn[ x ] should be excluded
@@ -50,6 +52,7 @@ protected:
   bool invariant( quantifiers::TermDbSygus * tds, Node nvn, Node x );
 };
 
+// TODO :issue #1235 split and document this class
 class TermDbSygus {
 private:
   /** reference to the quantifiers engine */
@@ -78,38 +81,45 @@ private:
   void computeMinTypeDepthInternal( TypeNode root_tn, TypeNode tn, unsigned type_depth );
   bool involvesDivByZero( Node n, std::map< Node, bool >& visited );
 private:
-  // stores root
-  std::map< Node, Node > d_measured_term;
-  std::map< Node, Node > d_measured_term_active_guard;
-  //information for sygus types
-  std::map< TypeNode, TypeNode > d_register;  //stores sygus -> builtin type
-  std::map< TypeNode, std::vector< Node > > d_var_list;
-  std::map< TypeNode, std::map< int, Kind > > d_arg_kind;
-  std::map< TypeNode, std::map< Kind, int > > d_kinds;
-  std::map< TypeNode, std::map< int, Node > > d_arg_const;
-  std::map< TypeNode, std::map< Node, int > > d_consts;
-  std::map< TypeNode, std::map< Node, int > > d_ops;
-  std::map< TypeNode, std::map< int, Node > > d_arg_ops;
-  std::map< TypeNode, std::vector< int > > d_id_funcs;
-  std::map< TypeNode, std::vector< Node > > d_const_list; //sorted list of constants for type
-  std::map< TypeNode, unsigned > d_const_list_pos;
-  std::map< TypeNode, std::map< Node, Node > > d_semantic_skolem;
-  //information for builtin types
-  std::map< TypeNode, std::map< int, Node > > d_type_value;
-  std::map< TypeNode, Node > d_type_max_value;
-  std::map< TypeNode, std::map< Node, std::map< int, Node > > > d_type_value_offset;
-  std::map< TypeNode, std::map< Node, std::map< int, int > > > d_type_value_offset_status;
-  //normalized map
-  std::map< TypeNode, std::map< Node, Node > > d_normalized;
-  std::map< TypeNode, std::map< Node, Node > > d_sygus_to_builtin;
-  std::map< TypeNode, std::map< Node, Node > > d_builtin_const_to_sygus;
-  // grammar information
-  // root -> type -> _
-  std::map< TypeNode, std::map< TypeNode, unsigned > > d_min_type_depth;
-  //std::map< TypeNode, std::map< Node, std::map< std::map< int, bool > > > d_consider_const;
-  // type -> cons -> _
-  std::map< TypeNode, unsigned > d_min_term_size;
-  std::map< TypeNode, std::map< unsigned, unsigned > > d_min_cons_term_size;
+ /** 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 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".
+ */
+ std::map<Node, Node> d_enum_to_active_guard;
+ // information for sygus types
+ std::map<TypeNode, TypeNode> d_register;  // stores sygus -> builtin type
+ std::map<TypeNode, std::vector<Node> > d_var_list;
+ std::map<TypeNode, std::map<int, Kind> > d_arg_kind;
+ std::map<TypeNode, std::map<Kind, int> > d_kinds;
+ std::map<TypeNode, std::map<int, Node> > d_arg_const;
+ std::map<TypeNode, std::map<Node, int> > d_consts;
+ std::map<TypeNode, std::map<Node, int> > d_ops;
+ std::map<TypeNode, std::map<int, Node> > d_arg_ops;
+ std::map<TypeNode, std::vector<int> > d_id_funcs;
+ std::map<TypeNode, std::vector<Node> >
+     d_const_list;  // sorted list of constants for type
+ std::map<TypeNode, unsigned> d_const_list_pos;
+ std::map<TypeNode, std::map<Node, Node> > d_semantic_skolem;
+ // information for builtin types
+ std::map<TypeNode, std::map<int, Node> > d_type_value;
+ std::map<TypeNode, Node> d_type_max_value;
+ std::map<TypeNode, std::map<Node, std::map<int, Node> > > d_type_value_offset;
+ std::map<TypeNode, std::map<Node, std::map<int, int> > >
+     d_type_value_offset_status;
+ // normalized map
+ std::map<TypeNode, std::map<Node, Node> > d_normalized;
+ std::map<TypeNode, std::map<Node, Node> > d_sygus_to_builtin;
+ std::map<TypeNode, std::map<Node, Node> > d_builtin_const_to_sygus;
+ // grammar information
+ // root -> type -> _
+ std::map<TypeNode, std::map<TypeNode, unsigned> > d_min_type_depth;
+ // std::map< TypeNode, std::map< Node, std::map< std::map< int, bool > > >
+ // d_consider_const;
+ // type -> cons -> _
+ std::map<TypeNode, unsigned> d_min_term_size;
+ std::map<TypeNode, std::map<unsigned, unsigned> > d_min_cons_term_size;
 public:
   TermDbSygus( context::Context* c, QuantifiersEngine* qe );
   ~TermDbSygus(){}
@@ -118,13 +128,20 @@ public:
 public:
   /** register the sygus type */
   void registerSygusType( TypeNode tn );
-  /** register a term that we will do enumerative search on */
-  void registerMeasuredTerm( Node e, Node root, bool mkActiveGuard = false );
-  /** is measured term */
-  Node isMeasuredTerm( Node e );
-  /** get active guard */
+  /** register a variable e that we will do enumerative search on
+   * conj is the conjecture that the enumeration for e is for.
+   * mkActiveGuard is whether we want to make a active guard for e (see
+   * d_enum_to_active_guard)
+   */
+  void registerMeasuredTerm(Node e, CegConjecture* conj,
+                            bool mkActiveGuard = false);
+  /** is e a measured term (enumerator)? */
+  bool isMeasuredTerm(Node e) const;
+  /** return the conjecture e is associated with */
+  CegConjecture* getConjectureFor(Node e);
+  /** get active guard for e */
   Node getActiveGuardForMeasureTerm( Node e );
-  /** get measured terms */
+  /** get all registered measure terms (enumerators) */
   void getMeasuredTerms( std::vector< Node >& mts );
 public:  //general sygus utilities
   bool isRegistered( TypeNode tn );
@@ -239,7 +256,6 @@ public:
   void getExplanationFor( Node n, Node vn, std::vector< Node >& exp, SygusInvarianceTest& et );
   // builtin evaluation, returns rewrite( bn [ args / vars(tn) ] )
   Node evaluateBuiltin( TypeNode tn, Node bn, std::vector< Node >& args );
-  Node evaluateBuiltin( TypeNode tn, Node bn, Node ar, unsigned i );
   // evaluate with unfolding
   Node evaluateWithUnfolding( Node n, std::map< Node, Node >& visited );
   Node evaluateWithUnfolding( Node n );
@@ -256,39 +272,6 @@ private:
 public:
   bool isGenericRedundant( TypeNode tn, unsigned i );
   
-//sygus pbe
-private:
-  std::map< Node, std::vector< std::vector< Node > > > d_pbe_exs;
-  std::map< Node, std::vector< Node > > d_pbe_exos;
-  std::map< Node, unsigned > d_pbe_term_id;
-private:
-  class PbeTrie {
-  private:
-    Node addPbeExampleEval( TypeNode etn, Node e, Node b, std::vector< Node >& ex, quantifiers::TermDbSygus * tds, unsigned index, unsigned ntotal );
-  public:
-    PbeTrie(){}
-    ~PbeTrie(){}
-    Node d_lazy_child;
-    std::map< Node, PbeTrie > d_children;
-    void clear() { d_children.clear(); }
-    Node addPbeExample( TypeNode etn, Node e, Node b, TermDbSygus * tds, unsigned index, unsigned ntotal );
-  };
-  std::map< Node, std::map< TypeNode, PbeTrie > > d_pbe_trie;
-public:
-  /** register examples for an enumerative search term. 
-      This should be a comprehensive set of examples. */
-  void registerPbeExamples( Node e, std::vector< std::vector< Node > >& exs, 
-                            std::vector< Node >& exos, std::vector< Node >& exts );
-  /** get examples */
-  bool hasPbeExamples( Node e );
-  unsigned getNumPbeExamples( Node e );
-  /** return value is the required value for the example */
-  void getPbeExample( Node e, unsigned i, std::vector< Node >& ex );
-  Node getPbeExampleOut( Node e, unsigned i );
-  int getPbeExampleId( Node n );
-  /** add the search val, returns an equivalent value (possibly the same) */
-  Node addPbeSearchVal( TypeNode tn, Node e, Node bvr );
-
 // extended rewriting
 private:
   std::map< Node, Node > d_ext_rewrite_cache;