Create infrastructure for sygus modules (#1632)

10 files changed, 751 insertions, 392 deletions

diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index 7bcaa0cba..f2a1c334c 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -51,11 +51,20 @@ void collectDisjuncts( Node n, std::vector< Node >& d ) {
 CegConjecture::CegConjecture(QuantifiersEngine* qe)
     : d_qe(qe),
       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, this)),
+      d_ceg_pbe(new CegConjecturePbe(qe, this)),
+      d_ceg_cegis(new Cegis(qe, this)),
+      d_master(nullptr),
       d_refine_count(0),
-      d_syntax_guided(false) {}
+      d_syntax_guided(false)
+{
+  if (options::sygusPbe())
+  {
+    d_modules.push_back(d_ceg_pbe.get());
+  }
+  d_modules.push_back(d_ceg_cegis.get());
+}
 
 CegConjecture::~CegConjecture() {}
 
@@ -113,29 +122,21 @@ void CegConjecture::assign( Node q ) {
   d_base_inst = Rewriter::rewrite(d_qe->getInstantiate()->getInstantiation(
       d_embed_quant, vars, d_candidates));
   Trace("cegqi") << "Base instantiation is :      " << d_base_inst << std::endl;
-  d_base_body = d_base_inst;
-  if (d_base_body.getKind() == NOT && d_base_body[0].getKind() == FORALL)
-  {
-    for (const Node& v : d_base_body[0][0])
-    {
-      d_base_vars.push_back(v);
-    }
-    d_base_body = d_base_body[0][1];
-  }
 
   // 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);
-    } else {
-      for (unsigned i = 0; i < d_candidates.size(); i++) {
-        Node e = d_candidates[i];
-        d_qe->getTermDatabaseSygus()->registerEnumerator(e, e, this);
+    for (unsigned i = 0, size = d_modules.size(); i < size; i++)
+    {
+      if (d_modules[i]->initialize(d_base_inst, d_candidates, guarded_lemmas))
+      {
+        d_master = d_modules[i];
+        break;
       }
     }
+    Assert(d_master != nullptr);
   }
 
   if (d_qe->getQuantAttributes()->isSygus(q))
@@ -193,15 +194,6 @@ void CegConjecture::assign( Node q ) {
     d_qe->getOutputChannel().lemma( lem );
   }
 
-  // assign the cegis sampler if applicable
-  if (options::cegisSample() != CEGIS_SAMPLE_NONE)
-  {
-    Trace("cegis-sample") << "Initialize sampler for " << d_base_body << "..."
-                          << std::endl;
-    TypeNode bt = d_base_body.getType();
-    d_cegis_sampler.initialize(bt, d_base_vars, options::sygusSamples());
-  }
-
   Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation() << std::endl;
 }
 
@@ -241,10 +233,8 @@ void CegConjecture::doSingleInvCheck(std::vector< Node >& lems) {
 
 void CegConjecture::doBasicCheck(std::vector< Node >& lems) {
   std::vector< Node > model_terms;
-  std::vector< Node > clist;
-  getCandidateList( clist, true );
-  Assert( clist.size()==d_quant[0].getNumChildren() );
-  getModelValues( clist, model_terms );
+  Assert(d_candidates.size() == d_quant[0].getNumChildren());
+  getModelValues(d_candidates, model_terms);
   if (d_qe->getInstantiate()->addInstantiation(d_quant, model_terms))
   {
     //record the instantiation
@@ -257,62 +247,57 @@ void CegConjecture::doBasicCheck(std::vector< Node >& lems) {
 bool CegConjecture::needsRefinement() { 
   return !d_ce_sk.empty();
 }
+void CegConjecture::doCheck(std::vector<Node>& lems)
+{
+  Assert(d_master != nullptr);
 
-void CegConjecture::getCandidateList( std::vector< Node >& clist, bool forceOrig ) {
-  if( d_ceg_pbe->isPbe() && !forceOrig ){
-    d_ceg_pbe->getCandidateList( d_candidates, clist );
-  }else{
-    clist.insert( clist.end(), d_candidates.begin(), d_candidates.end() );
-  }
-}
+  // get the list of terms that the master strategy is interested in
+  std::vector<Node> terms;
+  d_master->getTermList(d_candidates, terms);
 
-bool CegConjecture::constructCandidates( std::vector< Node >& clist, std::vector< Node >& model_values, std::vector< Node >& candidate_values, 
-                                         std::vector< Node >& lems ) {
-  Assert( clist.size()==model_values.size() );
-  if( d_ceg_pbe->isPbe() ){
-    return d_ceg_pbe->constructCandidates( clist, model_values, d_candidates, candidate_values, lems );
-  }else{
-    Assert( model_values.size()==d_candidates.size() );
-    candidate_values.insert( candidate_values.end(), model_values.begin(), model_values.end() );
-  }
-  return true;
-}
+  // get their model value
+  std::vector<Node> enum_values;
+  getModelValues(terms, enum_values);
 
-void CegConjecture::doCheck(std::vector< Node >& lems, std::vector< Node >& model_values) {
-  std::vector< Node > clist;
-  getCandidateList( clist );
-  std::vector< Node > c_model_values;
+  std::vector<Node> candidate_values;
   Trace("cegqi-check") << "CegConjuncture : check, build candidates..." << std::endl;
-  bool constructed_cand = constructCandidates( clist, model_values, c_model_values, lems );
+  bool constructed_cand = d_master->constructCandidates(
+      terms, enum_values, d_candidates, candidate_values, lems);
+
+  NodeManager* nm = NodeManager::currentNM();
 
   //must get a counterexample to the value of the current candidate
   Node inst;
   if( constructed_cand ){
     if( Trace.isOn("cegqi-check")  ){
       Trace("cegqi-check") << "CegConjuncture : check candidate : " << std::endl;
-      for( unsigned i=0; i<c_model_values.size(); i++ ){
-        Trace("cegqi-check") << "  " << i << " : " << d_candidates[i] << " -> " << c_model_values[i] << std::endl;
+      for (unsigned i = 0, size = candidate_values.size(); i < size; i++)
+      {
+        Trace("cegqi-check") << "  " << i << " : " << d_candidates[i] << " -> "
+                             << candidate_values[i] << std::endl;
       }
     }
-    Assert( c_model_values.size()==d_candidates.size() );
-    inst = d_base_inst.substitute( d_candidates.begin(), d_candidates.end(), c_model_values.begin(), c_model_values.end() );
+    Assert(candidate_values.size() == d_candidates.size());
+    inst = d_base_inst.substitute(d_candidates.begin(),
+                                  d_candidates.end(),
+                                  candidate_values.begin(),
+                                  candidate_values.end());
   }else{
     inst = d_base_inst;
   }
   
   //check whether we will run CEGIS on inner skolem variables
-  bool sk_refine = ( !isGround() || d_refine_count==0 ) && ( !d_ceg_pbe->isPbe() || constructed_cand );
+  bool sk_refine = (!isGround() || d_refine_count == 0) && constructed_cand;
   if( sk_refine ){
     if (options::cegisSample() == CEGIS_SAMPLE_TRUST)
     {
       // we have that the current candidate passed a sample test
       // since we trust sampling in this mode, we assert there is no
       // counterexample to the conjecture here.
-      NodeManager* nm = NodeManager::currentNM();
       Node lem = nm->mkNode(OR, d_quant.negate(), nm->mkConst(false));
       lem = getStreamGuardedLemma(lem);
       lems.push_back(lem);
-      recordInstantiation(c_model_values);
+      recordInstantiation(candidate_values);
       return;
     }
     Assert( d_ce_sk.empty() );
@@ -352,7 +337,7 @@ void CegConjecture::doCheck(std::vector< Node >& lems, std::vector< Node >& mode
     }
   }
   if( constructed_cand ){
-    Node lem = NodeManager::currentNM()->mkNode( OR, ic );
+    Node lem = nm->mkNode(OR, ic);
     lem = Rewriter::rewrite( lem );
     //eagerly unfold applications of evaluation function
     if( options::sygusDirectEval() ){
@@ -362,7 +347,7 @@ void CegConjecture::doCheck(std::vector< Node >& lems, std::vector< Node >& mode
     }
     lem = getStreamGuardedLemma(lem);
     lems.push_back( lem );
-    recordInstantiation( c_model_values );
+    recordInstantiation(candidate_values);
   }
 }
         
@@ -433,7 +418,7 @@ void CegConjecture::doRefine( std::vector< Node >& lems ){
   
   base_lem = base_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
   base_lem = Rewriter::rewrite( base_lem );
-  d_refinement_lemmas.push_back(base_lem);
+  d_master->registerRefinementLemma(base_lem);
 
   Node lem =
       NodeManager::currentNM()->mkNode(OR, getGuard().negate(), base_lem);
@@ -533,6 +518,7 @@ Node CegConjecture::getNextDecisionRequest( unsigned& priority ) {
             return curr_stream_guard;
           }else{
             if( !value ){
+              Assert(d_master != nullptr);
               Trace("cegqi-debug") << "getNextDecision : we have a new solution since stream guard was propagated false: " << curr_stream_guard << std::endl;
               // we have generated a solution, print it
               // get the current output stream
@@ -545,14 +531,15 @@ Node CegConjecture::getNextDecisionRequest( unsigned& priority ) {
               // We will not refine the current candidate solution since it is a solution
               // thus, we clear information regarding the current refinement
               d_ce_sk.clear();
-              // However, we need to exclude the current solution using an explicit refinement 
-              // so that we proceed to the next solution. 
-              std::vector< Node > clist;
-              getCandidateList( clist );
+              // However, we need to exclude the current solution using an
+              // explicit refinement
+              // so that we proceed to the next solution.
+              std::vector<Node> terms;
+              d_master->getTermList(d_candidates, terms);
               Trace("cegqi-debug") << "getNextDecision : solution was : " << std::endl;
               std::vector< Node > exp;
-              for( unsigned i=0; i<clist.size(); i++ ){
-                Node cprog = clist[i];
+              for (const Node& cprog : terms)
+              {
                 Node sol = cprog;
                 if( !d_cinfo[cprog].d_inst.empty() ){
                   sol = d_cinfo[cprog].d_inst.back();
@@ -811,84 +798,6 @@ Node CegConjecture::getSymmetryBreakingPredicate(
   }
 }
 
-bool CegConjecture::sampleAddRefinementLemma(std::vector<Node>& vals,
-                                             std::vector<Node>& lems)
-{
-  if (Trace.isOn("cegis-sample"))
-  {
-    Trace("cegis-sample") << "Check sampling for candidate solution"
-                          << std::endl;
-    for (unsigned i = 0, size = vals.size(); i < size; i++)
-    {
-      Trace("cegis-sample")
-          << "  " << d_candidates[i] << " -> " << vals[i] << std::endl;
-    }
-  }
-  Assert(vals.size() == d_candidates.size());
-  Node sbody = d_base_body.substitute(
-      d_candidates.begin(), d_candidates.end(), vals.begin(), vals.end());
-  Trace("cegis-sample-debug") << "Sample " << sbody << std::endl;
-  // do eager unfolding
-  std::map<Node, Node> visited_n;
-  sbody = d_qe->getTermDatabaseSygus()->getEagerUnfold(sbody, visited_n);
-  Trace("cegis-sample") << "Sample (after unfolding): " << sbody << std::endl;
-
-  NodeManager* nm = NodeManager::currentNM();
-  for (unsigned i = 0, size = d_cegis_sampler.getNumSamplePoints(); i < size;
-       i++)
-  {
-    if (d_cegis_sample_refine.find(i) == d_cegis_sample_refine.end())
-    {
-      Node ev = d_cegis_sampler.evaluate(sbody, i);
-      Trace("cegis-sample-debug")
-          << "...evaluate point #" << i << " to " << ev << std::endl;
-      Assert(ev.isConst());
-      Assert(ev.getType().isBoolean());
-      if (!ev.getConst<bool>())
-      {
-        Trace("cegis-sample-debug") << "...false for point #" << i << std::endl;
-        // mark this as a CEGIS point (no longer sampled)
-        d_cegis_sample_refine.insert(i);
-        std::vector<Node> vars;
-        std::vector<Node> pt;
-        d_cegis_sampler.getSamplePoint(i, vars, pt);
-        Assert(d_base_vars.size() == pt.size());
-        Node rlem = d_base_body.substitute(
-            d_base_vars.begin(), d_base_vars.end(), pt.begin(), pt.end());
-        rlem = Rewriter::rewrite(rlem);
-        if (std::find(
-                d_refinement_lemmas.begin(), d_refinement_lemmas.end(), rlem)
-            == d_refinement_lemmas.end())
-        {
-          if (Trace.isOn("cegis-sample"))
-          {
-            Trace("cegis-sample") << "   false for point #" << i << " : ";
-            for (const Node& cn : pt)
-            {
-              Trace("cegis-sample") << cn << " ";
-            }
-            Trace("cegis-sample") << std::endl;
-          }
-          Trace("cegqi-engine") << "  *** Refine by sampling" << std::endl;
-          d_refinement_lemmas.push_back(rlem);
-          // if trust, we are not interested in sending out refinement lemmas
-          if (options::cegisSample() != CEGIS_SAMPLE_TRUST)
-          {
-            Node lem = nm->mkNode(OR, getGuard().negate(), rlem);
-            lems.push_back(lem);
-          }
-          return true;
-        }
-        else
-        {
-          Trace("cegis-sample-debug") << "...duplicate." << std::endl;
-        }
-      }
-    }
-  }
-  return false;
-}
-
 }/* namespace CVC4::theory::quantifiers */
 }/* namespace CVC4::theory */
 }/* namespace CVC4 */
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h
index 1ef8fef10..9f3335ee2 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h
@@ -20,9 +20,10 @@
 
 #include <memory>
 
-#include "theory/quantifiers/sygus/sygus_pbe.h"
 #include "theory/quantifiers/sygus/ce_guided_single_inv.h"
+#include "theory/quantifiers/sygus/cegis.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
+#include "theory/quantifiers/sygus/sygus_pbe.h"
 #include "theory/quantifiers/sygus/sygus_process_conj.h"
 #include "theory/quantifiers/sygus_sampler.h"
 #include "theory/quantifiers_engine.h"
@@ -57,8 +58,6 @@ public:
   bool needsCheck( std::vector< Node >& lem );
   /** whether the conjecture is waiting for a call to doRefine below */
   bool needsRefinement();
-  /** get the list of candidates */
-  void getCandidateList( std::vector< Node >& clist, bool forceOrig = false );
   /** do single invocation check 
   * This updates Gamma for an iteration of step 2 of Figure 1 of Reynolds et al CAV 2015.
   */
@@ -66,7 +65,7 @@ public:
   /** do syntax-guided enumerative check 
   * This is step 2(a) of Figure 3 of Reynolds et al CAV 2015.
   */
-  void doCheck(std::vector< Node >& lems, std::vector< Node >& model_values);
+  void doCheck(std::vector<Node>& lems);
   /** do basic check 
   * This is called for non-SyGuS synthesis conjectures
   */
@@ -118,26 +117,6 @@ public:
   /** 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
-   *
-   * If d_embed_quant is forall d. exists y. P( d, y ), then a refinement
-   * lemma is one of the form ~P( d_candidates, c ) for some c.
-   */
-  Node getRefinementLemma( unsigned i ) { return d_refinement_lemmas[i]; }
-  /** sample add refinement lemma
-   *
-   * This function will check if there is a sample point in d_sampler that
-   * refutes the candidate solution (d_quant_vars->vals). If so, it adds a
-   * refinement lemma to the lists d_refinement_lemmas that corresponds to that
-   * sample point, and adds a lemma to lems if cegisSample mode is not trust.
-   */
-  bool sampleAddRefinementLemma(std::vector<Node>& vals,
-                                std::vector<Node>& lems);
-  //-----------------------------------end refinement lemmas
-
   /** get program by examples utility */
   CegConjecturePbe* getPbe() { return d_ceg_pbe.get(); }
   /** get utility for static preprocessing and analysis of conjectures */
@@ -152,12 +131,26 @@ private:
   QuantifiersEngine * d_qe;
   /** single invocation utility */
   std::unique_ptr<CegConjectureSingleInv> d_ceg_si;
-  /** program by examples utility */
-  std::unique_ptr<CegConjecturePbe> d_ceg_pbe;
   /** utility for static preprocessing and analysis of conjectures */
   std::unique_ptr<CegConjectureProcess> d_ceg_proc;
   /** grammar utility */
   std::unique_ptr<CegGrammarConstructor> d_ceg_gc;
+
+  //------------------------modules
+  /** program by examples module */
+  std::unique_ptr<CegConjecturePbe> d_ceg_pbe;
+  /** CEGIS module */
+  std::unique_ptr<Cegis> d_ceg_cegis;
+  /** the set of active modules (subset of the above list) */
+  std::vector<SygusModule*> d_modules;
+  /** master module
+   *
+   * This is the module (one of those above) that takes sole responsibility
+   * for this conjecture, determined during assign(...).
+   */
+  SygusModule* d_master;
+  //------------------------end modules
+
   /** list of constants for quantified formula
   * The outer Skolems for the negation of d_embed_quant.
   */
@@ -167,13 +160,6 @@ private:
   * this is the formula  exists y. P( d_candidates, y ).
   */
   Node d_base_inst;
-  /** If d_base_inst is exists y. P( d, y ), then this is y. */
-  std::vector<Node> d_base_vars;
-  /**
-   * If d_base_inst is exists y. P( d, y ), then this is the formula
-   * P( d_candidates, y ).
-   */
-  Node d_base_body;
   /** expand base inst to disjuncts */
   std::vector< Node > d_base_disj;
   /** list of variables on inner quantification */
@@ -182,10 +168,6 @@ private:
   /** 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;
-  //-----------------------------------end refinement lemmas
 
   /** the asserted (negated) conjecture */
   Node d_quant;
@@ -203,9 +185,6 @@ private:
   std::map< Node, CandidateInfo > d_cinfo;  
   /** number of times we have called doRefine */
   unsigned d_refine_count;
-  /** construct candidates */
-  bool constructCandidates( std::vector< Node >& clist, std::vector< Node >& model_values, 
-                            std::vector< Node >& candidate_values, std::vector< Node >& lems );
   /** get candidadate */
   Node getCandidate( unsigned int i ) { return d_candidates[i]; }
   /** record instantiation (this is used to construct solutions later) */
@@ -262,18 +241,6 @@ private:
    * rewrite rules.
    */
   std::map<Node, SygusSamplerExt> d_sampler;
-  /** sampler object for the option cegisSample()
-   *
-   * This samples points of the type of the inner variables of the synthesis
-   * conjecture (d_base_vars).
-   */
-  SygusSampler d_cegis_sampler;
-  /** cegis sample refine points
-   *
-   * Stores the list of indices of sample points in d_cegis_sampler we have
-   * added as refinement lemmas.
-   */
-  std::unordered_set<unsigned> d_cegis_sample_refine;
 };
 
 } /* namespace CVC4::theory::quantifiers */
diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
index 35098f5ea..125682e8c 100644
--- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
@@ -21,8 +21,6 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
-//FIXME : remove this include (github issue #1156)
-#include "theory/bv/theory_bv_rewriter.h"
 
 using namespace CVC4::kind;
 using namespace std;
@@ -125,61 +123,10 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
         Trace("cegqi-engine") << "  ...try single invocation." << std::endl;
         return;
       }
-      //ignore return value here
-      std::vector< Node > clist;
-      conj->getCandidateList( clist );
-      std::vector< Node > model_values;
-      conj->getModelValues( clist, model_values );
-      if( options::sygusDirectEval() ){
-        bool addedEvalLemmas = false;
-        if( options::sygusCRefEval() ){
-          Trace("cegqi-engine") << "  *** Do conjecture refinement evaluation..." << std::endl;
-          // see if any refinement lemma is refuted by evaluation
-          std::vector< Node > cre_lems;
-          getCRefEvaluationLemmas( conj, clist, model_values, cre_lems );
-          if( !cre_lems.empty() ){
-            for( unsigned j=0; j<cre_lems.size(); j++ ){
-              Node lem = cre_lems[j];
-              if( d_quantEngine->addLemma( lem ) ){
-                Trace("cegqi-lemma") << "Cegqi::Lemma : cref evaluation : " << lem << std::endl;
-                addedEvalLemmas = true;
-              }
-            }
-            if( addedEvalLemmas ){
-              //return;
-            }
-          }
-        }
-        Trace("cegqi-engine") << "  *** Do direct evaluation..." << std::endl;
-        std::vector< Node > eager_terms; 
-        std::vector< Node > eager_vals; 
-        std::vector< Node > eager_exps;
-        for( unsigned j=0; j<clist.size(); j++ ){
-          Trace("cegqi-debug") << "  register " << clist[j] << " -> " << model_values[j] << std::endl;
-          d_quantEngine->getTermDatabaseSygus()->registerModelValue( clist[j], model_values[j], eager_terms, eager_vals, eager_exps );
-        }
-        Trace("cegqi-debug") << "...produced " << eager_terms.size()  << " eager evaluation lemmas." << std::endl;
-        if( !eager_terms.empty() ){
-          for( unsigned j=0; j<eager_terms.size(); j++ ){
-            Node lem = NodeManager::currentNM()->mkNode( kind::OR, eager_exps[j].negate(), eager_terms[j].eqNode( eager_vals[j] ) );
-            if( d_quantEngine->getTheoryEngine()->isTheoryEnabled(THEORY_BV) ){
-              //FIXME: hack to incorporate hacks from BV for division by zero (github issue #1156)
-              lem = bv::TheoryBVRewriter::eliminateBVSDiv( lem );
-            }
-            if( d_quantEngine->addLemma( lem ) ){
-              Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << lem << std::endl;
-              addedEvalLemmas = true;
-            }
-          }
-        }
-        if( addedEvalLemmas ){
-          return;
-        }
-      }
       
       Trace("cegqi-engine") << "  *** Check candidate phase..." << std::endl;
       std::vector< Node > cclems;
-      conj->doCheck( cclems, model_values );
+      conj->doCheck(cclems);
       bool addedLemma = false;
       for( unsigned i=0; i<cclems.size(); i++ ){
         Node lem = cclems[i];
@@ -236,95 +183,6 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
   }
 }
 
-void CegInstantiation::getCRefEvaluationLemmas( CegConjecture * conj, std::vector< Node >& vs, std::vector< Node >& ms, std::vector< Node >& lems ) {
-  Trace("sygus-cref-eval") << "Cref eval : conjecture has " << conj->getNumRefinementLemmas() << " refinement lemmas." << std::endl;
-  unsigned nlemmas = conj->getNumRefinementLemmas();
-  if (nlemmas > 0 || options::cegisSample() != CEGIS_SAMPLE_NONE)
-  {
-    Assert( vs.size()==ms.size() );
-
-    TermDbSygus* tds = d_quantEngine->getTermDatabaseSygus();
-    Node nfalse = d_quantEngine->getTermUtil()->d_false;
-    Node neg_guard = conj->getGuard().negate();
-    for (unsigned i = 0; i <= nlemmas; i++)
-    {
-      if (i == nlemmas)
-      {
-        bool addedSample = false;
-        // find a new one by sampling, if applicable
-        if (options::cegisSample() != CEGIS_SAMPLE_NONE)
-        {
-          addedSample = conj->sampleAddRefinementLemma(ms, lems);
-        }
-        if (!addedSample)
-        {
-          return;
-        }
-      }
-      Node lem;
-      std::map< Node, Node > visited;
-      std::map< Node, std::vector< Node > > exp;
-      lem = conj->getRefinementLemma(i);
-      if( !lem.isNull() ){
-        std::vector< Node > lem_conj;
-        //break into conjunctions
-        if( lem.getKind()==kind::AND ){
-          for( unsigned i=0; i<lem.getNumChildren(); i++ ){
-            lem_conj.push_back( lem[i] );
-          }
-        }else{
-          lem_conj.push_back( lem );
-        }
-        EvalSygusInvarianceTest vsit;
-        for( unsigned j=0; j<lem_conj.size(); j++ ){
-          Node lemc = lem_conj[j];
-          Trace("sygus-cref-eval") << "Check refinement lemma conjunct " << lemc << " against current model." << std::endl;
-          Trace("sygus-cref-eval2") << "Check refinement lemma conjunct " << lemc << " against current model." << std::endl;
-          Node cre_lem;
-          Node lemcs = lemc.substitute( vs.begin(), vs.end(), ms.begin(), ms.end() );
-          Trace("sygus-cref-eval2") << "...under substitution it is : " << lemcs << std::endl;
-          Node lemcsu = vsit.doEvaluateWithUnfolding(tds, lemcs);
-          Trace("sygus-cref-eval2") << "...after unfolding is : " << lemcsu << std::endl;
-          if( lemcsu==d_quantEngine->getTermUtil()->d_false ){
-            std::vector< Node > msu;
-            std::vector< Node > mexp;
-            msu.insert( msu.end(), ms.begin(), ms.end() );
-            for( unsigned k=0; k<vs.size(); k++ ){
-              vsit.setUpdatedTerm(msu[k]);
-              msu[k] = vs[k];
-              // substitute for everything except this
-              Node sconj =
-                  lemc.substitute(vs.begin(), vs.end(), msu.begin(), msu.end());
-              vsit.init(sconj, vs[k], nfalse);
-              // get minimal explanation for this
-              Node ut = vsit.getUpdatedTerm();
-              Trace("sygus-cref-eval2-debug")
-                  << "  compute min explain of : " << vs[k] << " = " << ut
-                  << std::endl;
-              d_quantEngine->getTermDatabaseSygus()
-                  ->getExplain()
-                  ->getExplanationFor(vs[k], ut, mexp, vsit);
-              msu[k] = ut;
-            }
-            if( !mexp.empty() ){
-              Node en = mexp.size()==1 ? mexp[0] : NodeManager::currentNM()->mkNode( kind::AND, mexp );
-              cre_lem = NodeManager::currentNM()->mkNode( kind::OR, en.negate(), neg_guard );
-            }else{
-              cre_lem = neg_guard;
-            }
-          }
-          if( !cre_lem.isNull() ){
-            if( std::find( lems.begin(), lems.end(), cre_lem )==lems.end() ){
-              Trace("sygus-cref-eval") << "...produced lemma : " << cre_lem << std::endl;
-              lems.push_back( cre_lem );
-            }
-          }
-        }
-      }
-    }
-  }
-}
-
 void CegInstantiation::printSynthSolution( std::ostream& out ) {
   if( d_conj->isAssigned() )
   {
diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.h b/src/theory/quantifiers/sygus/ce_guided_instantiation.h
index 087836d5a..1b1d5e44b 100644
--- a/src/theory/quantifiers/sygus/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.h
@@ -33,9 +33,6 @@ private:
   CegConjecture * d_conj;
   /** last instantiation by single invocation module? */
   bool d_last_inst_si;
-private: //for direct evaluation
-  /** get refinement evaluation */
-  void getCRefEvaluationLemmas( CegConjecture * conj, std::vector< Node >& vs, std::vector< Node >& ms, std::vector< Node >& lems );
 private:
   /** check conjecture */
   void checkCegConjecture( CegConjecture * conj );
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
new file mode 100644
index 000000000..a571c85fb
--- /dev/null
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -0,0 +1,354 @@
+/*********************                                                        */
+/*! \file cegis.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 cegis
+ **/
+
+#include "theory/quantifiers/sygus/cegis.h"
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/sygus/ce_guided_conjecture.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+// FIXME : remove these includes (github issue #1156)
+#include "theory/bv/theory_bv_rewriter.h"
+#include "theory/theory_engine.h"
+
+using namespace std;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+Cegis::Cegis(QuantifiersEngine* qe, CegConjecture* p) : SygusModule(qe, p) {}
+bool Cegis::initialize(Node n,
+                       const std::vector<Node>& candidates,
+                       std::vector<Node>& lemmas)
+{
+  d_base_body = n;
+  if (d_base_body.getKind() == NOT && d_base_body[0].getKind() == FORALL)
+  {
+    for (const Node& v : d_base_body[0][0])
+    {
+      d_base_vars.push_back(v);
+    }
+    d_base_body = d_base_body[0][1];
+  }
+
+  // assign the cegis sampler if applicable
+  if (options::cegisSample() != CEGIS_SAMPLE_NONE)
+  {
+    Trace("cegis-sample") << "Initialize sampler for " << d_base_body << "..."
+                          << std::endl;
+    TypeNode bt = d_base_body.getType();
+    d_cegis_sampler.initialize(bt, d_base_vars, options::sygusSamples());
+  }
+
+  // initialize an enumerator for each candidate
+  TermDbSygus* tds = d_qe->getTermDatabaseSygus();
+  for (unsigned i = 0; i < candidates.size(); i++)
+  {
+    tds->registerEnumerator(candidates[i], candidates[i], d_parent);
+  }
+  return true;
+}
+
+void Cegis::getTermList(const std::vector<Node>& candidates,
+                        std::vector<Node>& enums)
+{
+  enums.insert(enums.end(), candidates.begin(), candidates.end());
+}
+
+/** construct candidate */
+bool Cegis::constructCandidates(const std::vector<Node>& enums,
+                                const std::vector<Node>& enum_values,
+                                const std::vector<Node>& candidates,
+                                std::vector<Node>& candidate_values,
+                                std::vector<Node>& lems)
+{
+  candidate_values.insert(
+      candidate_values.end(), enum_values.begin(), enum_values.end());
+
+  if (options::sygusDirectEval())
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    bool addedEvalLemmas = false;
+    if (options::sygusCRefEval())
+    {
+      Trace("cegqi-engine") << "  *** Do conjecture refinement evaluation..."
+                            << std::endl;
+      // see if any refinement lemma is refuted by evaluation
+      std::vector<Node> cre_lems;
+      getRefinementEvalLemmas(candidates, candidate_values, cre_lems);
+      if (!cre_lems.empty())
+      {
+        for (unsigned j = 0; j < cre_lems.size(); j++)
+        {
+          Node lem = cre_lems[j];
+          if (d_qe->addLemma(lem))
+          {
+            Trace("cegqi-lemma") << "Cegqi::Lemma : cref evaluation : " << lem
+                                 << std::endl;
+            addedEvalLemmas = true;
+          }
+        }
+        // we could, but do not return here.
+        // experimentally, it is better to add the lemmas below as well,
+        // in parallel.
+      }
+    }
+    Trace("cegqi-engine") << "  *** Do direct evaluation..." << std::endl;
+    std::vector<Node> eager_terms;
+    std::vector<Node> eager_vals;
+    std::vector<Node> eager_exps;
+    TermDbSygus* tds = d_qe->getTermDatabaseSygus();
+    for (unsigned j = 0, size = candidates.size(); j < size; j++)
+    {
+      Trace("cegqi-debug") << "  register " << candidates[j] << " -> "
+                           << candidate_values[j] << std::endl;
+      tds->registerModelValue(candidates[j],
+                              candidate_values[j],
+                              eager_terms,
+                              eager_vals,
+                              eager_exps);
+    }
+    Trace("cegqi-debug") << "...produced " << eager_terms.size()
+                         << " eager evaluation lemmas." << std::endl;
+
+    for (unsigned j = 0, size = eager_terms.size(); j < size; j++)
+    {
+      Node lem = nm->mkNode(kind::OR,
+                            eager_exps[j].negate(),
+                            eager_terms[j].eqNode(eager_vals[j]));
+      if (d_qe->getTheoryEngine()->isTheoryEnabled(THEORY_BV))
+      {
+        // FIXME: hack to incorporate hacks from BV for division by zero
+        // (github issue #1156)
+        lem = bv::TheoryBVRewriter::eliminateBVSDiv(lem);
+      }
+      if (d_qe->addLemma(lem))
+      {
+        Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << lem
+                             << std::endl;
+        addedEvalLemmas = true;
+      }
+    }
+    if (addedEvalLemmas)
+    {
+      return false;
+    }
+  }
+
+  return true;
+}
+
+void Cegis::registerRefinementLemma(Node lem)
+{
+  d_refinement_lemmas.push_back(lem);
+}
+
+void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs,
+                                    const std::vector<Node>& ms,
+                                    std::vector<Node>& lems)
+{
+  Trace("sygus-cref-eval") << "Cref eval : conjecture has "
+                           << getNumRefinementLemmas() << " refinement lemmas."
+                           << std::endl;
+  unsigned nlemmas = getNumRefinementLemmas();
+  if (nlemmas > 0 || options::cegisSample() != CEGIS_SAMPLE_NONE)
+  {
+    Assert(vs.size() == ms.size());
+
+    TermDbSygus* tds = d_qe->getTermDatabaseSygus();
+    NodeManager* nm = NodeManager::currentNM();
+
+    Node nfalse = nm->mkConst(false);
+    Node neg_guard = d_parent->getGuard().negate();
+    for (unsigned i = 0; i <= nlemmas; i++)
+    {
+      if (i == nlemmas)
+      {
+        bool addedSample = false;
+        // find a new one by sampling, if applicable
+        if (options::cegisSample() != CEGIS_SAMPLE_NONE)
+        {
+          addedSample = sampleAddRefinementLemma(vs, ms, lems);
+        }
+        if (!addedSample)
+        {
+          return;
+        }
+      }
+      Node lem;
+      std::map<Node, Node> visited;
+      std::map<Node, std::vector<Node> > exp;
+      lem = getRefinementLemma(i);
+      if (!lem.isNull())
+      {
+        std::vector<Node> lem_conj;
+        // break into conjunctions
+        if (lem.getKind() == kind::AND)
+        {
+          for (unsigned i = 0; i < lem.getNumChildren(); i++)
+          {
+            lem_conj.push_back(lem[i]);
+          }
+        }
+        else
+        {
+          lem_conj.push_back(lem);
+        }
+        EvalSygusInvarianceTest vsit;
+        for (unsigned j = 0; j < lem_conj.size(); j++)
+        {
+          Node lemc = lem_conj[j];
+          Trace("sygus-cref-eval") << "Check refinement lemma conjunct " << lemc
+                                   << " against current model." << std::endl;
+          Trace("sygus-cref-eval2") << "Check refinement lemma conjunct "
+                                    << lemc << " against current model."
+                                    << std::endl;
+          Node cre_lem;
+          Node lemcs =
+              lemc.substitute(vs.begin(), vs.end(), ms.begin(), ms.end());
+          Trace("sygus-cref-eval2") << "...under substitution it is : " << lemcs
+                                    << std::endl;
+          Node lemcsu = vsit.doEvaluateWithUnfolding(tds, lemcs);
+          Trace("sygus-cref-eval2") << "...after unfolding is : " << lemcsu
+                                    << std::endl;
+          if (lemcsu.isConst() && !lemcsu.getConst<bool>())
+          {
+            std::vector<Node> msu;
+            std::vector<Node> mexp;
+            msu.insert(msu.end(), ms.begin(), ms.end());
+            for (unsigned k = 0; k < vs.size(); k++)
+            {
+              vsit.setUpdatedTerm(msu[k]);
+              msu[k] = vs[k];
+              // substitute for everything except this
+              Node sconj =
+                  lemc.substitute(vs.begin(), vs.end(), msu.begin(), msu.end());
+              vsit.init(sconj, vs[k], nfalse);
+              // get minimal explanation for this
+              Node ut = vsit.getUpdatedTerm();
+              Trace("sygus-cref-eval2-debug")
+                  << "  compute min explain of : " << vs[k] << " = " << ut
+                  << std::endl;
+              tds->getExplain()->getExplanationFor(vs[k], ut, mexp, vsit);
+              msu[k] = ut;
+            }
+            if (!mexp.empty())
+            {
+              Node en =
+                  mexp.size() == 1 ? mexp[0] : nm->mkNode(kind::AND, mexp);
+              cre_lem = nm->mkNode(kind::OR, en.negate(), neg_guard);
+            }
+            else
+            {
+              cre_lem = neg_guard;
+            }
+          }
+          if (!cre_lem.isNull())
+          {
+            if (std::find(lems.begin(), lems.end(), cre_lem) == lems.end())
+            {
+              Trace("sygus-cref-eval") << "...produced lemma : " << cre_lem
+                                       << std::endl;
+              lems.push_back(cre_lem);
+            }
+          }
+        }
+      }
+    }
+  }
+}
+
+bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates,
+                                     const std::vector<Node>& vals,
+                                     std::vector<Node>& lems)
+{
+  if (Trace.isOn("cegis-sample"))
+  {
+    Trace("cegis-sample") << "Check sampling for candidate solution"
+                          << std::endl;
+    for (unsigned i = 0, size = vals.size(); i < size; i++)
+    {
+      Trace("cegis-sample") << "  " << candidates[i] << " -> " << vals[i]
+                            << std::endl;
+    }
+  }
+  Assert(vals.size() == candidates.size());
+  Node sbody = d_base_body.substitute(
+      candidates.begin(), candidates.end(), vals.begin(), vals.end());
+  Trace("cegis-sample-debug") << "Sample " << sbody << std::endl;
+  // do eager unfolding
+  std::map<Node, Node> visited_n;
+  sbody = d_qe->getTermDatabaseSygus()->getEagerUnfold(sbody, visited_n);
+  Trace("cegis-sample") << "Sample (after unfolding): " << sbody << std::endl;
+
+  NodeManager* nm = NodeManager::currentNM();
+  for (unsigned i = 0, size = d_cegis_sampler.getNumSamplePoints(); i < size;
+       i++)
+  {
+    if (d_cegis_sample_refine.find(i) == d_cegis_sample_refine.end())
+    {
+      Node ev = d_cegis_sampler.evaluate(sbody, i);
+      Trace("cegis-sample-debug") << "...evaluate point #" << i << " to " << ev
+                                  << std::endl;
+      Assert(ev.isConst());
+      Assert(ev.getType().isBoolean());
+      if (!ev.getConst<bool>())
+      {
+        Trace("cegis-sample-debug") << "...false for point #" << i << std::endl;
+        // mark this as a CEGIS point (no longer sampled)
+        d_cegis_sample_refine.insert(i);
+        std::vector<Node> vars;
+        std::vector<Node> pt;
+        d_cegis_sampler.getSamplePoint(i, vars, pt);
+        Assert(d_base_vars.size() == pt.size());
+        Node rlem = d_base_body.substitute(
+            d_base_vars.begin(), d_base_vars.end(), pt.begin(), pt.end());
+        rlem = Rewriter::rewrite(rlem);
+        if (std::find(
+                d_refinement_lemmas.begin(), d_refinement_lemmas.end(), rlem)
+            == d_refinement_lemmas.end())
+        {
+          if (Trace.isOn("cegis-sample"))
+          {
+            Trace("cegis-sample") << "   false for point #" << i << " : ";
+            for (const Node& cn : pt)
+            {
+              Trace("cegis-sample") << cn << " ";
+            }
+            Trace("cegis-sample") << std::endl;
+          }
+          Trace("cegqi-engine") << "  *** Refine by sampling" << std::endl;
+          d_refinement_lemmas.push_back(rlem);
+          // if trust, we are not interested in sending out refinement lemmas
+          if (options::cegisSample() != CEGIS_SAMPLE_TRUST)
+          {
+            Node lem = nm->mkNode(OR, d_parent->getGuard().negate(), rlem);
+            lems.push_back(lem);
+          }
+          return true;
+        }
+        else
+        {
+          Trace("cegis-sample-debug") << "...duplicate." << std::endl;
+        }
+      }
+    }
+  }
+  return false;
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
new file mode 100644
index 000000000..2cb668fa1
--- /dev/null
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -0,0 +1,121 @@
+/*********************                                                        */
+/*! \file cegis.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 cegis
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__CEGIS_H
+#define __CVC4__THEORY__QUANTIFIERS__CEGIS_H
+
+#include <map>
+#include "theory/quantifiers/sygus/sygus_module.h"
+#include "theory/quantifiers/sygus_sampler.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** Cegis
+ *
+ * The default sygus module for synthesis, counterexample-guided inductive
+ * synthesis (CEGIS).
+ *
+ * It initializes a list of sygus enumerators that are one-to-one with
+ * candidates, and returns a list of candidates that are the model values
+ * of these enumerators on calls to constructCandidates.
+ *
+ * It implements an optimization (getRefinementEvalLemmas) that evaluates all
+ * previous refinement lemmas for a term before returning it as a candidate
+ * in calls to constructCandidates.
+ */
+class Cegis : public SygusModule
+{
+ public:
+  Cegis(QuantifiersEngine* qe, CegConjecture* p);
+  ~Cegis() {}
+  /** initialize */
+  virtual bool initialize(Node n,
+                          const std::vector<Node>& candidates,
+                          std::vector<Node>& lemmas) override;
+  /** get term list */
+  virtual void getTermList(const std::vector<Node>& candidates,
+                           std::vector<Node>& enums) override;
+  /** construct candidate */
+  virtual bool constructCandidates(const std::vector<Node>& enums,
+                                   const std::vector<Node>& enum_values,
+                                   const std::vector<Node>& candidates,
+                                   std::vector<Node>& candidate_values,
+                                   std::vector<Node>& lems) override;
+  /** register refinement lemma */
+  virtual void registerRefinementLemma(Node lem) override;
+
+ private:
+  /** If CegConjecture::d_base_inst is exists y. P( d, y ), then this is y. */
+  std::vector<Node> d_base_vars;
+  /**
+   * If CegConjecture::d_base_inst is exists y. P( d, y ), then this is the
+   * formula P( CegConjecture::d_candidates, y ).
+   */
+  Node d_base_body;
+
+  //-----------------------------------refinement lemmas
+  /** refinement lemmas */
+  std::vector<Node> d_refinement_lemmas;
+  /** get number of refinement lemmas we have added so far */
+  unsigned getNumRefinementLemmas() { return d_refinement_lemmas.size(); }
+  /** get refinement lemma
+   *
+   * If d_embed_quant is forall d. exists y. P( d, y ), then a refinement
+   * lemma is one of the form ~P( d_candidates, c ) for some c.
+   */
+  Node getRefinementLemma(unsigned i) { return d_refinement_lemmas[i]; }
+  /** sample add refinement lemma
+   *
+   * This function will check if there is a sample point in d_sampler that
+   * refutes the candidate solution (d_quant_vars->vals). If so, it adds a
+   * refinement lemma to the lists d_refinement_lemmas that corresponds to that
+   * sample point, and adds a lemma to lems if cegisSample mode is not trust.
+   */
+  bool sampleAddRefinementLemma(const std::vector<Node>& candidates,
+                                const std::vector<Node>& vals,
+                                std::vector<Node>& lems);
+  //-----------------------------------end refinement lemmas
+
+  /** Get refinement evaluation lemmas
+   *
+   * Given a candidate solution ms for candidates vs, this function adds lemmas
+   * to lems based on evaluating the conjecture, instantiated for ms, on lemmas
+   * for previous refinements (d_refinement_lemmas).
+   */
+  void getRefinementEvalLemmas(const std::vector<Node>& vs,
+                               const std::vector<Node>& ms,
+                               std::vector<Node>& lems);
+  /** sampler object for the option cegisSample()
+   *
+   * This samples points of the type of the inner variables of the synthesis
+   * conjecture (d_base_vars).
+   */
+  SygusSampler d_cegis_sampler;
+  /** cegis sample refine points
+   *
+   * Stores the list of indices of sample points in d_cegis_sampler we have
+   * added as refinement lemmas.
+   */
+  std::unordered_set<unsigned> d_cegis_sample_refine;
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__CEGIS_H */
diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp
new file mode 100644
index 000000000..19e064350
--- /dev/null
+++ b/src/theory/quantifiers/sygus/sygus_module.cpp
@@ -0,0 +1,28 @@
+/*********************                                                        */
+/*! \file sygus_module.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of sygus_module
+ **/
+
+#include "theory/quantifiers/sygus/sygus_module.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+SygusModule::SygusModule(QuantifiersEngine* qe, CegConjecture* p)
+    : d_qe(qe), d_parent(p)
+{
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
new file mode 100644
index 000000000..230ea7a61
--- /dev/null
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -0,0 +1,120 @@
+/*********************                                                        */
+/*! \file sygus_module.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief sygus_module
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
+
+#include <map>
+#include "expr/node.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class CegConjecture;
+
+/** SygusModule
+ *
+ * This is the base class of sygus modules, owned by CegConjecture. The purpose
+ * of this class is to, when applicable, suggest candidate solutions for
+ * CegConjecture to test.
+ *
+ * In more detail, an instance of the conjecture class (CegConjecture) creates
+ * the negated deep embedding form of the synthesis conjecture. In the
+ * following, assume this is:
+ *   forall d. exists x. P( d, x )
+ * where d are of sygus datatype type. The "base instantiation" of this
+ * conjecture (see CegConjecture::d_base_inst) is the formula:
+ *   exists y. P( k, y )
+ * where k are the "candidate" variables for the conjecture.
+ *
+ * Modules implement an initialize function, which determines whether the module
+ * will take responsibility for the given conjecture.
+ */
+class SygusModule
+{
+ public:
+  SygusModule(QuantifiersEngine* qe, CegConjecture* p);
+  ~SygusModule() {}
+  /** initialize
+   *
+   * 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 argument lemmas, which should be
+   * sent out on the output channel of quantifiers by the caller.
+   *
+   * This function returns true if this module will take responsibility for
+   * constructing candidates for the given conjecture.
+   */
+  virtual bool initialize(Node n,
+                          const std::vector<Node>& candidates,
+                          std::vector<Node>& lemmas) = 0;
+  /** get term list
+   *
+   * This gets the list of terms that will appear as arguments to a subsequent
+   * call to constructCandidates.
+   */
+  virtual void getTermList(const std::vector<Node>& candidates,
+                           std::vector<Node>& terms) = 0;
+  /** construct candidate
+   *
+   * This function takes as input:
+   *   terms : the terms returned by a call to getTermList,
+   *   term_values : the current model values of terms,
+   *   candidates : the list of candidates.
+   *
+   * If this function returns true, it adds to candidate_values a list of terms
+   * of the same length and type as candidates that are candidate solutions
+   * to the synthesis conjecture in question. This candidate { v } will then be
+   * tested by testing the (un)satisfiablity of P( v, k' ) for fresh k' by the
+   * caller.
+   *
+   * This function may also add lemmas to lems, which are sent out as lemmas
+   * on the output channel of quantifiers by the caller. For an example of
+   * such lemmas, see SygusPbe::constructCandidates.
+   *
+   * This function may return false if it does not have a candidate it wants
+   * to test on this iteration. In this case, lems should be non-empty.
+   */
+  virtual bool constructCandidates(const std::vector<Node>& terms,
+                                   const std::vector<Node>& term_values,
+                                   const std::vector<Node>& candidates,
+                                   std::vector<Node>& candidate_values,
+                                   std::vector<Node>& lems) = 0;
+  /** register refinement lemma
+   *
+   * Assume this module, on a previous call to constructCandidates, added the
+   * value { v } to candidate_values for candidates = { k }. This function is
+   * called if the base instantiation of the synthesis conjecture has a model
+   * under this substitution. In particular, in the above example, this function
+   * is called when the refinement lemma P( v, k' ) has a model. The argument
+   * lem in the call to this function is P( v, k' ).
+   */
+  virtual void registerRefinementLemma(Node lem) {}
+ protected:
+  /** reference to quantifier engine */
+  QuantifiersEngine* d_qe;
+  /** reference to the parent conjecture */
+  CegConjecture* d_parent;
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H */
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 17c4c482d..36e883848 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -97,8 +97,8 @@ std::ostream& operator<<(std::ostream& os, StrategyType st)
 }
 
 CegConjecturePbe::CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p)
-    : d_qe(qe),
-      d_parent(p){
+    : SygusModule(qe, p)
+{
   d_tds = d_qe->getTermDatabaseSygus();
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
@@ -176,8 +176,8 @@ void CegConjecturePbe::collectExamples( Node n, std::map< Node, bool >& visited,
   }
 }
 
-void CegConjecturePbe::initialize(Node n,
-                                  std::vector<Node>& candidates,
+bool CegConjecturePbe::initialize(Node n,
+                                  const std::vector<Node>& candidates,
                                   std::vector<Node>& lemmas)
 {
   Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl;
@@ -234,13 +234,7 @@ void CegConjecturePbe::initialize(Node n,
       }
     }
   }
-  if( !d_is_pbe ){
-    Trace("sygus-unif") << "Do not do PBE optimizations, register..." << std::endl;
-    for( unsigned i=0; i<candidates.size(); i++ ){
-      d_qe->getTermDatabaseSygus()->registerEnumerator(
-          candidates[i], candidates[i], d_parent);
-    }
-  }
+  return d_is_pbe;
 }
 
 Node CegConjecturePbe::PbeTrie::addPbeExample(TypeNode etn, Node e, Node b,
@@ -1077,7 +1071,9 @@ void CegConjecturePbe::staticLearnRedundantOps(
 
 // ------------------------------------------- solution construction from enumeration
 
-void CegConjecturePbe::getCandidateList( std::vector< Node >& candidates, std::vector< Node >& clist ) {
+void CegConjecturePbe::getTermList(const std::vector<Node>& candidates,
+                                   std::vector<Node>& terms)
+{
   Valuation& valuation = d_qe->getValuation();
   for( unsigned i=0; i<candidates.size(); i++ ){
     Node v = candidates[i];
@@ -1090,16 +1086,19 @@ void CegConjecturePbe::getCandidateList( std::vector< Node >& candidates, std::v
         Node gstatus = valuation.getSatValue(it->second.d_active_guard);
         if (!gstatus.isNull() && gstatus.getConst<bool>())
         {
-          clist.push_back( e );
+          terms.push_back(e);
         }
       }
     }
   }
 }
 
-bool CegConjecturePbe::constructCandidates( std::vector< Node >& enums, std::vector< Node >& enum_values, 
-                                            std::vector< Node >& candidates, std::vector< Node >& candidate_values, 
-                                            std::vector< Node >& lems ) {
+bool CegConjecturePbe::constructCandidates(const std::vector<Node>& enums,
+                                           const std::vector<Node>& enum_values,
+                                           const std::vector<Node>& candidates,
+                                           std::vector<Node>& candidate_values,
+                                           std::vector<Node>& lems)
+{
   Assert( enums.size()==enum_values.size() );
   if( !enums.empty() ){
     unsigned min_term_size = 0;
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h
index ce1f2bf5e..2b800db81 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.h
+++ b/src/theory/quantifiers/sygus/sygus_pbe.h
@@ -18,7 +18,7 @@
 #define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_PBE_H
 
 #include "context/cdhashmap.h"
-#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/sygus/sygus_module.h"
 
 namespace CVC4 {
 namespace theory {
@@ -158,48 +158,58 @@ class CegConjecture;
 * This class is not designed to work in incremental mode, since there is no way
 * to specify incremental problems in SyguS.
 */
-class CegConjecturePbe {
+class CegConjecturePbe : public SygusModule
+{
  public:
   CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p);
   ~CegConjecturePbe();
 
   /** 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
+  bool initialize(Node n,
+                  const std::vector<Node>& candidates,
+                  std::vector<Node>& lemmas) override;
+  /** get term list
+   *
   * Adds all active enumerators associated with functions-to-synthesize in
-  * candidates to clist.
+  * candidates to terms.
   */
-  void getCandidateList(std::vector<Node>& candidates,
-                        std::vector<Node>& clist);
+  void getTermList(const std::vector<Node>& candidates,
+                   std::vector<Node>& terms) override;
   /** 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(...).
-  */
-  bool constructCandidates(std::vector<Node>& enums,
-                           std::vector<Node>& enum_values,
-                           std::vector<Node>& candidates,
+   *
+   * This function attempts to use unification-based approaches for constructing
+   * solutions for all functions-to-synthesize (indicated by candidates). These
+   * approaches include decision tree learning and a divide-and-conquer
+   * algorithm based on string concatenation.
+   *
+   * Calls to this function are such that terms is the list of active
+   * enumerators (returned by getTermList), and term_values are their current
+   * model values. This function registers { terms -> terms_values } in
+   * the database of values that have been enumerated, which are in turn used
+   * for constructing candidate solutions when possible.
+   *
+   * This function also excludes models where (terms = terms_values) by adding
+   * blocking clauses to lems. For example, for grammar:
+   *   A -> A+A | x | 1 | 0
+   * and a call where terms = { d } and term_values = { +( x, 1 ) }, it adds:
+   *   ~G V ~is_+( d ) V ~is_x( d.1 ) V ~is_1( d.2 )
+   * to lems, where G is active guard of the enumerator d (see
+   * TermDatabaseSygus::getActiveGuardForEnumerator). This blocking clause
+   * indicates that d should not be given the model value +( x, 1 ) anymore,
+   * since { d -> +( x, 1 ) } has now been added to the database of this class.
+   */
+  bool constructCandidates(const std::vector<Node>& terms,
+                           const std::vector<Node>& term_values,
+                           const std::vector<Node>& candidates,
                            std::vector<Node>& candidate_values,
-                           std::vector<Node>& lems);
+                           std::vector<Node>& lems) override;
   /** is PBE enabled for any enumerator? */
   bool isPbe() { return d_is_pbe; }
   /** is the enumerator e associated with I/O example pairs? */
@@ -243,15 +253,11 @@ class CegConjecturePbe {
   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 */
   quantifiers::TermDbSygus * d_tds;
   /** true and false nodes */
   Node d_true;
   Node d_false;
-  /** A reference to the conjecture that owns this class. */
-  CegConjecture* d_parent;
   /** is this a PBE conjecture for any function? */
   bool d_is_pbe;
   /** for each candidate variable f (a function-to-synthesize), whether the