Move and rename sygus solver classes (#2488)

33 files changed, 753 insertions, 611 deletions

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 82aa570c2..db1ce1c05 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -22,7 +22,6 @@
 #include "printer/printer.h"
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/datatypes/theory_datatypes.h"
-#include "theory/quantifiers/sygus/ce_guided_conjecture.h"
 #include "theory/quantifiers/sygus/sygus_explain.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
@@ -313,11 +312,11 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std:
       // static conjecture-dependent symmetry breaking
       Trace("sygus-sb-debug")
           << "  conjecture-dependent symmetry breaking...\n";
-      std::map<Node, quantifiers::CegConjecture*>::iterator itc =
+      std::map<Node, quantifiers::SynthConjecture*>::iterator itc =
           d_anchor_to_conj.find(a);
       if (itc != d_anchor_to_conj.end())
       {
-        quantifiers::CegConjecture* conj = itc->second;
+        quantifiers::SynthConjecture* conj = itc->second;
         Assert(conj != NULL);
         Node dpred = conj->getSymmetryBreakingPredicate(x, a, ntn, tindex, ds);
         if (!dpred.isNull())
@@ -803,7 +802,7 @@ Node SygusSymBreakNew::registerSearchValue(
     d_cache[a].d_search_val_proc.insert(cnv);
     // get the root (for PBE symmetry breaking)
     Assert(d_anchor_to_conj.find(a) != d_anchor_to_conj.end());
-    quantifiers::CegConjecture* aconj = d_anchor_to_conj[a];
+    quantifiers::SynthConjecture* aconj = d_anchor_to_conj[a];
     Assert(aconj != NULL);
     Trace("sygus-sb-debug") << "  ...register search value " << cnv
                             << ", type=" << tn << std::endl;
@@ -827,9 +826,9 @@ Node SygusSymBreakNew::registerSearchValue(
       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?
+        // this should be generalized and encapsulated within the
+        // SynthConjecture class.
+        // Is it equivalent under examples?
         Node bvr_equiv;
         if (options::sygusSymBreakPbe())
         {
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index e2ed4192a..99f9672e7 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -30,8 +30,8 @@
 #include "expr/datatype.h"
 #include "expr/node.h"
 #include "theory/datatypes/sygus_simple_sym.h"
-#include "theory/quantifiers/sygus/ce_guided_conjecture.h"
 #include "theory/quantifiers/sygus/sygus_explain.h"
+#include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus_sampler.h"
 #include "theory/quantifiers/term_database.h"
 
@@ -152,7 +152,7 @@ class SygusSymBreakNew
   /**
    * Map from anchors to the conjecture they are associated with.
    */
-  std::map<Node, quantifiers::CegConjecture*> d_anchor_to_conj;
+  std::map<Node, quantifiers::SynthConjecture*> d_anchor_to_conj;
   /**
    * Map from terms (selector chains) to their depth. The depth of a selector
    * chain S1( ... Sn( x ) ... ) is:
@@ -229,7 +229,7 @@ private:
    * (2) static symmetry breaking clauses for subterms of n (those added to
    * lemmas on getSimpleSymBreakPred, see function below),
    * (3) conjecture-specific symmetry breaking lemmas, see
-   * CegConjecture::getSymmetryBreakingPredicate,
+   * SynthConjecture::getSymmetryBreakingPredicate,
    * (4) fairness conflicts if sygusFair() is SYGUS_FAIR_DIRECT, e.g.:
    *    size( d ) <= 1 V ~is-C1( d ) V ~is-C2( d.1 )
    * where C1 and C2 are non-nullary constructors.
diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index 3b7aab0b2..bba5b3c18 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -20,9 +20,9 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
-#include "theory/quantifiers/sygus/ce_guided_instantiation.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 
 using namespace std;
 using namespace CVC4::kind;
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index dde6dc4a9..ff906a95b 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -17,7 +17,7 @@
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/rewrite_engine.h"
-#include "theory/quantifiers/sygus/ce_guided_instantiation.h"
+#include "theory/quantifiers/sygus/synth_engine.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 
@@ -229,10 +229,11 @@ void QuantAttributes::computeAttributes( Node q ) {
     d_fun_defs[f] = true;
   }
   if( d_qattr[q].d_sygus ){
-    if( d_quantEngine->getCegInstantiation()==NULL ){
+    if (d_quantEngine->getSynthEngine() == nullptr)
+    {
       Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl;
     }
-    d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation(), 2 );
+    d_quantEngine->setOwner(q, d_quantEngine->getSynthEngine(), 2);
   }
 }
 
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 7d8db8c03..36690cfcc 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -42,12 +42,11 @@ bool CegqiOutputSingleInv::addLemma( Node n ) {
   return d_out->addLemma( n );
 }
 
-CegConjectureSingleInv::CegConjectureSingleInv(QuantifiersEngine* qe,
-                                               CegConjecture* p)
+CegSingleInv::CegSingleInv(QuantifiersEngine* qe, SynthConjecture* p)
     : d_qe(qe),
       d_parent(p),
       d_sip(new SingleInvocationPartition),
-      d_sol(new CegConjectureSingleInvSol(qe)),
+      d_sol(new CegSingleInvSol(qe)),
       d_cosi(new CegqiOutputSingleInv(this)),
       d_cinst(new CegInstantiator(d_qe, d_cosi, false, false)),
       d_c_inst_match_trie(NULL),
@@ -61,17 +60,17 @@ CegConjectureSingleInv::CegConjectureSingleInv(QuantifiersEngine* qe,
   }
 }
 
-CegConjectureSingleInv::~CegConjectureSingleInv() {
+CegSingleInv::~CegSingleInv()
+{
   if (d_c_inst_match_trie) {
     delete d_c_inst_match_trie;
   }
   delete d_cosi;
-  delete d_sol;  // (new CegConjectureSingleInvSol(qe)),
+  delete d_sol;  // (new CegSingleInvSol(qe)),
   delete d_sip;  // d_sip(new SingleInvocationPartition),
 }
 
-void CegConjectureSingleInv::getInitialSingleInvLemma(Node g,
-                                                      std::vector<Node>& lems)
+void CegSingleInv::getInitialSingleInvLemma(Node g, std::vector<Node>& lems)
 {
   Assert(!g.isNull());
   Assert(!d_single_inv.isNull());
@@ -114,12 +113,13 @@ void CegConjectureSingleInv::getInitialSingleInvLemma(Node g,
   d_cinst->registerCounterexampleLemma(lems, d_single_inv_sk);
 }
 
-void CegConjectureSingleInv::initialize( Node q ) {
+void CegSingleInv::initialize(Node q)
+{
   // can only register one quantified formula with this
   Assert( d_quant.isNull() );
   d_quant = q;
   d_simp_quant = q;
-  Trace("cegqi-si") << "CegConjectureSingleInv::initialize : " << q << std::endl;
+  Trace("cegqi-si") << "CegSingleInv::initialize : " << q << std::endl;
   // infer single invocation-ness
 
   // get the variables
@@ -293,7 +293,7 @@ void CegConjectureSingleInv::initialize( Node q ) {
   }
 }
 
-void CegConjectureSingleInv::finishInit(bool syntaxRestricted)
+void CegSingleInv::finishInit(bool syntaxRestricted)
 {
   Trace("cegqi-si-debug") << "Single invocation: finish init" << std::endl;
   // do not do single invocation if grammar is restricted and CEGQI_SI_MODE_ALL is not enabled
@@ -343,9 +343,10 @@ void CegConjectureSingleInv::finishInit(bool syntaxRestricted)
   }
 }
 
-bool CegConjectureSingleInv::doAddInstantiation( std::vector< Node >& subs ){
+bool CegSingleInv::doAddInstantiation(std::vector<Node>& subs)
+{
   Assert( d_single_inv_sk.size()==subs.size() );
-  Trace("cegqi-si-inst-debug") << "CegConjectureSingleInv::doAddInstantiation, #vars = ";
+  Trace("cegqi-si-inst-debug") << "CegSingleInv::doAddInstantiation, #vars = ";
   Trace("cegqi-si-inst-debug") << d_single_inv_sk.size() << "..." << std::endl;
   std::stringstream siss;
   if( Trace.isOn("cegqi-si-inst-debug") || Trace.isOn("cegqi-engine") ){
@@ -400,19 +401,23 @@ bool CegConjectureSingleInv::doAddInstantiation( std::vector< Node >& subs ){
   return true;
 }
 
-bool CegConjectureSingleInv::isEligibleForInstantiation( Node n ) {
+bool CegSingleInv::isEligibleForInstantiation(Node n)
+{
   return n.getKind()!=SKOLEM || std::find( d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end(), n )!=d_single_inv_arg_sk.end();
 }
 
-bool CegConjectureSingleInv::addLemma( Node n ) {
+bool CegSingleInv::addLemma(Node n)
+{
   d_curr_lemmas.push_back( n );
   return true;
 }
 
-bool CegConjectureSingleInv::check( std::vector< Node >& lems ) {
+bool CegSingleInv::check(std::vector<Node>& lems)
+{
   if( !d_single_inv.isNull() ) {
-    Trace("cegqi-si-debug") << "CegConjectureSingleInv::check..." << std::endl;
-    Trace("cegqi-si-debug") << "CegConjectureSingleInv::check consulting ceg instantiation..." << std::endl;
+    Trace("cegqi-si-debug") << "CegSingleInv::check..." << std::endl;
+    Trace("cegqi-si-debug")
+        << "CegSingleInv::check consulting ceg instantiation..." << std::endl;
     d_curr_lemmas.clear();
     Assert( d_cinst!=NULL );
     //call check for instantiator
@@ -427,7 +432,11 @@ bool CegConjectureSingleInv::check( std::vector< Node >& lems ) {
   }
 }
 
-Node CegConjectureSingleInv::constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index, std::map< Node, Node >& weak_imp ) {
+Node CegSingleInv::constructSolution(std::vector<unsigned>& indices,
+                                     unsigned i,
+                                     unsigned index,
+                                     std::map<Node, Node>& weak_imp)
+{
   Assert( index<d_inst.size() );
   Assert( i<d_inst[index].size() );
   unsigned uindex = indices[index];
@@ -449,7 +458,7 @@ Node CegConjectureSingleInv::constructSolution( std::vector< unsigned >& indices
 
 //TODO: use term size?
 struct sortSiInstanceIndices {
-  CegConjectureSingleInv* d_ccsi;
+  CegSingleInv* d_ccsi;
   int d_i;
   bool operator() (unsigned i, unsigned j) {
     if( d_ccsi->d_inst[i][d_i].isConst() && !d_ccsi->d_inst[j][d_i].isConst() ){
@@ -460,8 +469,8 @@ struct sortSiInstanceIndices {
   }
 };
 
-
-Node CegConjectureSingleInv::postProcessSolution( Node n ){
+Node CegSingleInv::postProcessSolution(Node n)
+{
   bool childChanged = false;
   Kind k = n.getKind();
   if( n.getKind()==INTS_DIVISION_TOTAL ){
@@ -487,8 +496,11 @@ Node CegConjectureSingleInv::postProcessSolution( Node n ){
   }
 }
 
-
-Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& reconstructed, bool rconsSygus ){
+Node CegSingleInv::getSolution(unsigned sol_index,
+                               TypeNode stn,
+                               int& reconstructed,
+                               bool rconsSygus)
+{
   Assert( d_sol!=NULL );
   Assert( !d_lemmas_produced.empty() );
   const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
@@ -563,7 +575,11 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
   return reconstructToSyntax( s, stn, reconstructed, rconsSygus );
 }
 
-Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& reconstructed, bool rconsSygus ) {
+Node CegSingleInv::reconstructToSyntax(Node s,
+                                       TypeNode stn,
+                                       int& reconstructed,
+                                       bool rconsSygus)
+{
   d_solution = s;
   const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
 
@@ -645,13 +661,9 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec
   }
 }
 
-bool CegConjectureSingleInv::needsCheck() {
-  return true;
-}
+bool CegSingleInv::needsCheck() { return true; }
 
-void CegConjectureSingleInv::preregisterConjecture( Node q ) {
-  d_orig_conjecture = q;
-}
+void CegSingleInv::preregisterConjecture(Node q) { d_orig_conjecture = q; }
 
 bool DetTrace::DetTraceTrie::add( Node loc, std::vector< Node >& val, unsigned index ){
   if( index==val.size() ){
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
index b27163549..c797bc3cb 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
@@ -28,18 +28,17 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-class CegConjecture;
-class CegConjectureSingleInv;
-class CegEntailmentInfer;
+class SynthConjecture;
+class CegSingleInv;
 
 class CegqiOutputSingleInv : public CegqiOutput {
-public:
-  CegqiOutputSingleInv( CegConjectureSingleInv * out ) : d_out( out ){}
-  virtual ~CegqiOutputSingleInv() {}
-  CegConjectureSingleInv * d_out;
-  bool doAddInstantiation(std::vector<Node>& subs) override;
-  bool isEligibleForInstantiation(Node n) override;
-  bool addLemma(Node lem) override;
+ public:
+ CegqiOutputSingleInv(CegSingleInv* out) : d_out(out) {}
+ virtual ~CegqiOutputSingleInv() {}
+ CegSingleInv* d_out;
+ bool doAddInstantiation(std::vector<Node>& subs) override;
+ bool isEligibleForInstantiation(Node n) override;
+ bool addLemma(Node lem) override;
 };
 
 class DetTrace {
@@ -123,7 +122,8 @@ private:
 // (2) inferring whether the conjecture corresponds to a deterministic transistion system (by utility d_ti).
 // For these techniques, we may generate a template (d_templ) which specifies a restricted
 // solution space. We may in turn embed this template as a SyGuS grammar.
-class CegConjectureSingleInv {
+class CegSingleInv
+{
  private:
   friend class CegqiOutputSingleInv;
   //presolve
@@ -138,14 +138,16 @@ class CegConjectureSingleInv {
                          unsigned index, std::map<Node, Node>& weak_imp);
   Node postProcessSolution(Node n);
  private:
+  /** pointer to the quantifiers engine */
   QuantifiersEngine* d_qe;
-  CegConjecture* d_parent;
+  /** the parent of this class */
+  SynthConjecture* d_parent;
   // single invocation inference utility
   SingleInvocationPartition* d_sip;
   // transition inference module for each function to synthesize
   std::map< Node, TransitionInference > d_ti;
   // solution reconstruction
-  CegConjectureSingleInvSol* d_sol;
+  CegSingleInvSol* d_sol;
   // the instantiator's output channel
   CegqiOutputSingleInv* d_cosi;
   // the instantiator
@@ -197,8 +199,8 @@ class CegConjectureSingleInv {
   std::map< Node, Node > d_templ_arg;
   
  public:
-  CegConjectureSingleInv( QuantifiersEngine * qe, CegConjecture * p );
-  ~CegConjectureSingleInv();
+  CegSingleInv(QuantifiersEngine* qe, SynthConjecture* p);
+  ~CegSingleInv();
 
   // get simplified conjecture
   Node getSimplifiedConjecture() { return d_simp_quant; }
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
index e575dff9b..7f7c56f84 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -20,8 +20,8 @@
 #include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/sygus/ce_guided_instantiation.h"
 #include "theory/quantifiers/sygus/ce_guided_single_inv.h"
+#include "theory/quantifiers/sygus/synth_engine.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
@@ -42,10 +42,13 @@ bool doCompare(Node a, Node b, Kind k)
   return com.isConst() && com.getConst<bool>();
 }
 
-CegConjectureSingleInvSol::CegConjectureSingleInvSol(QuantifiersEngine* qe)
-    : d_qe(qe), d_id_count(0), d_root_id() {}
+CegSingleInvSol::CegSingleInvSol(QuantifiersEngine* qe)
+    : d_qe(qe), d_id_count(0), d_root_id()
+{
+}
 
-bool CegConjectureSingleInvSol::debugSolution( Node sol ) {
+bool CegSingleInvSol::debugSolution(Node sol)
+{
   if( sol.getKind()==SKOLEM ){
     return false;
   }else{
@@ -59,7 +62,8 @@ bool CegConjectureSingleInvSol::debugSolution( Node sol ) {
 
 }
 
-void CegConjectureSingleInvSol::debugTermSize( Node sol, int& t_size, int& num_ite ) {
+void CegSingleInvSol::debugTermSize(Node sol, int& t_size, int& num_ite)
+{
   std::map< Node, int >::iterator it = d_dterm_size.find( sol );
   if( it==d_dterm_size.end() ){
     int prev = t_size;
@@ -79,8 +83,8 @@ void CegConjectureSingleInvSol::debugTermSize( Node sol, int& t_size, int& num_i
   }
 }
 
-
-Node CegConjectureSingleInvSol::pullITEs( Node s ) {
+Node CegSingleInvSol::pullITEs(Node s)
+{
   if( s.getKind()==ITE ){
     bool success;
     do {
@@ -107,7 +111,13 @@ Node CegConjectureSingleInvSol::pullITEs( Node s ) {
 }
 
 // pull condition common to all ITE conditions in path of size > 1
-bool CegConjectureSingleInvSol::pullITECondition( Node root, Node n_ite, std::vector< Node >& conj, Node& t, Node& rem, int depth ) {
+bool CegSingleInvSol::pullITECondition(Node root,
+                                       Node n_ite,
+                                       std::vector<Node>& conj,
+                                       Node& t,
+                                       Node& rem,
+                                       int depth)
+{
   Assert( n_ite.getKind()==ITE );
   std::vector< Node > curr_conj;
   std::vector< Node > orig_conj;
@@ -196,7 +206,8 @@ bool CegConjectureSingleInvSol::pullITECondition( Node root, Node n_ite, std::ve
   }
 }
 
-Node CegConjectureSingleInvSol::flattenITEs( Node n, bool rec ) {
+Node CegSingleInvSol::flattenITEs(Node n, bool rec)
+{
   Assert( !n.isNull() );
   if( n.getKind()==ITE ){
     Trace("csi-sol-debug") << "Flatten ITE." << std::endl;
@@ -260,8 +271,14 @@ Node CegConjectureSingleInvSol::flattenITEs( Node n, bool rec ) {
 // assign is from literals to booleans
 // union_find is from args to values
 
-bool CegConjectureSingleInvSol::getAssign( bool pol, Node n, std::map< Node, bool >& assign, std::vector< Node >& new_assign, std::vector< Node >& vars,
-                                        std::vector< Node >& new_vars, std::vector< Node >& new_subs ) {
+bool CegSingleInvSol::getAssign(bool pol,
+                                Node n,
+                                std::map<Node, bool>& assign,
+                                std::vector<Node>& new_assign,
+                                std::vector<Node>& vars,
+                                std::vector<Node>& new_vars,
+                                std::vector<Node>& new_subs)
+{
   std::map< Node, bool >::iterator ita = assign.find( n );
   if( ita!=assign.end() ){
     Trace("csi-simp-debug") << "---already assigned, lookup " << pol << " " << ita->second << std::endl;
@@ -287,7 +304,11 @@ bool CegConjectureSingleInvSol::getAssign( bool pol, Node n, std::map< Node, boo
   return true;
 }
 
-bool CegConjectureSingleInvSol::getAssignEquality( Node eq, std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs ) {
+bool CegSingleInvSol::getAssignEquality(Node eq,
+                                        std::vector<Node>& vars,
+                                        std::vector<Node>& new_vars,
+                                        std::vector<Node>& new_subs)
+{
   Assert( eq.getKind()==EQUAL );
   //try to find valid argument
   for( unsigned r=0; r<2; r++ ){
@@ -309,7 +330,8 @@ bool CegConjectureSingleInvSol::getAssignEquality( Node eq, std::vector< Node >&
   return false;
 }
 
-Node CegConjectureSingleInvSol::simplifySolution( Node sol, TypeNode stn ){
+Node CegSingleInvSol::simplifySolution(Node sol, TypeNode stn)
+{
   int tsize, itesize;
   if( Trace.isOn("csi-sol") ){
     tsize = 0;itesize = 0;
@@ -373,9 +395,13 @@ Node CegConjectureSingleInvSol::simplifySolution( Node sol, TypeNode stn ){
   return curr_sol;
 }
 
-Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, std::map< Node, bool >& assign,
-                                                      std::vector< Node >& vars, std::vector< Node >& subs, int status ) {
-
+Node CegSingleInvSol::simplifySolutionNode(Node sol,
+                                           TypeNode stn,
+                                           std::map<Node, bool>& assign,
+                                           std::vector<Node>& vars,
+                                           std::vector<Node>& subs,
+                                           int status)
+{
   Assert( vars.size()==subs.size() );
   std::map< Node, bool >::iterator ita = assign.find( sol );
   if( ita!=assign.end() ){
@@ -618,8 +644,8 @@ Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, st
   }
 }
 
-
-void CegConjectureSingleInvSol::preregisterConjecture( Node q ) {
+void CegSingleInvSol::preregisterConjecture(Node q)
+{
   Trace("csi-sol") << "Preregister conjecture : " << q << std::endl;
   Node n = q;
   if( n.getKind()==FORALL ){
@@ -641,10 +667,10 @@ void CegConjectureSingleInvSol::preregisterConjecture( Node q ) {
   registerEquivalentTerms( n );
 }
 
-Node CegConjectureSingleInvSol::reconstructSolution(Node sol,
-                                                    TypeNode stn,
-                                                    int& reconstructed,
-                                                    int enumLimit)
+Node CegSingleInvSol::reconstructSolution(Node sol,
+                                          TypeNode stn,
+                                          int& reconstructed,
+                                          int enumLimit)
 {
   Trace("csi-rcons") << "Solution (pre-reconstruction) is : " << sol << std::endl;
   int status;
@@ -743,7 +769,8 @@ Node CegConjectureSingleInvSol::reconstructSolution(Node sol,
   return Node::null();
 }
 
-int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, int& status ) {
+int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status)
+{
   std::map< Node, int >::iterator itri = d_rcons_to_status[stn].find( t );
   if( itri!=d_rcons_to_status[stn].end() ){
     status = itri->second;
@@ -956,7 +983,12 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in
   }
 }
 
-bool CegConjectureSingleInvSol::collectReconstructNodes( int pid, std::vector< Node >& ts, const DatatypeConstructor& dtc, std::vector< int >& ids, int& status ) {
+bool CegSingleInvSol::collectReconstructNodes(int pid,
+                                              std::vector<Node>& ts,
+                                              const DatatypeConstructor& dtc,
+                                              std::vector<int>& ids,
+                                              int& status)
+{
   Assert( dtc.getNumArgs()==ts.size() );
   for( unsigned i=0; i<ts.size(); i++ ){
     TypeNode cstn = d_qe->getTermDatabaseSygus()->getArgType( dtc, i );
@@ -1001,8 +1033,9 @@ bool CegConjectureSingleInvSol::collectReconstructNodes( int pid, std::vector< N
   }
   */
 
-
-Node CegConjectureSingleInvSol::CegConjectureSingleInvSol::getReconstructedSolution( int id, bool mod_eq ) {
+Node CegSingleInvSol::CegSingleInvSol::getReconstructedSolution(int id,
+                                                                bool mod_eq)
+{
   std::map< int, Node >::iterator it = d_reconstruct.find( id );
   if( it!=d_reconstruct.end() ){
     return it->second;
@@ -1053,7 +1086,8 @@ Node CegConjectureSingleInvSol::CegConjectureSingleInvSol::getReconstructedSolut
   }
 }
 
-int CegConjectureSingleInvSol::allocate( Node n, TypeNode stn ) {
+int CegSingleInvSol::allocate(Node n, TypeNode stn)
+{
   std::map< Node, int >::iterator it = d_rcons_to_id[stn].find( n );
   if( it==d_rcons_to_id[stn].end() ){
     int ret = d_id_count;
@@ -1073,7 +1107,8 @@ int CegConjectureSingleInvSol::allocate( Node n, TypeNode stn ) {
   }
 }
 
-bool CegConjectureSingleInvSol::getPathToRoot( int id ) {
+bool CegSingleInvSol::getPathToRoot(int id)
+{
   if( id==d_root_id ){
     return true;
   }else{
@@ -1092,7 +1127,8 @@ bool CegConjectureSingleInvSol::getPathToRoot( int id ) {
   }
 }
 
-void CegConjectureSingleInvSol::setReconstructed( int id, Node n ) {
+void CegSingleInvSol::setReconstructed(int id, Node n)
+{
   //set all equivalent to this as reconstructed
   int rid = d_rep[id];
   for( unsigned i=0; i<d_eqc[rid].size(); i++ ){
@@ -1100,7 +1136,10 @@ void CegConjectureSingleInvSol::setReconstructed( int id, Node n ) {
   }
 }
 
-void CegConjectureSingleInvSol::getEquivalentTerms( Kind k, Node n, std::vector< Node >& equiv ) {
+void CegSingleInvSol::getEquivalentTerms(Kind k,
+                                         Node n,
+                                         std::vector<Node>& equiv)
+{
   if( k==AND || k==OR ){
     equiv.push_back( NodeManager::currentNM()->mkNode( k, n, n ) );
     equiv.push_back( NodeManager::currentNM()->mkNode( k, n, NodeManager::currentNM()->mkConst( k==AND ) ) );
@@ -1201,7 +1240,8 @@ void CegConjectureSingleInvSol::getEquivalentTerms( Kind k, Node n, std::vector<
   }
 }
 
-void CegConjectureSingleInvSol::registerEquivalentTerms( Node n ) {
+void CegSingleInvSol::registerEquivalentTerms(Node n)
+{
   for( unsigned i=0; i<n.getNumChildren(); i++ ){
     registerEquivalentTerms( n[i] );
   }
@@ -1219,9 +1259,7 @@ void CegConjectureSingleInvSol::registerEquivalentTerms( Node n ) {
   }
 }
 
-Node CegConjectureSingleInvSol::builtinToSygusConst(Node c,
-                                                    TypeNode tn,
-                                                    int rcons_depth)
+Node CegSingleInvSol::builtinToSygusConst(Node c, TypeNode tn, int rcons_depth)
 {
   std::map<Node, Node>::iterator it = d_builtin_const_to_sygus[tn].find(c);
   if (it != d_builtin_const_to_sygus[tn].end())
@@ -1350,7 +1388,7 @@ struct sortConstants
   }
 };
 
-void CegConjectureSingleInvSol::registerType(TypeNode tn)
+void CegSingleInvSol::registerType(TypeNode tn)
 {
   if (d_const_list_pos.find(tn) != d_const_list_pos.end())
   {
@@ -1407,10 +1445,10 @@ void CegConjectureSingleInvSol::registerType(TypeNode tn)
   }
 }
 
-bool CegConjectureSingleInvSol::getMatch(Node p,
-                                         Node n,
-                                         std::map<int, Node>& s,
-                                         std::vector<int>& new_s)
+bool CegSingleInvSol::getMatch(Node p,
+                               Node n,
+                               std::map<int, Node>& s,
+                               std::vector<int>& new_s)
 {
   TermDbSygus* tds = d_qe->getTermDatabaseSygus();
   if (tds->isFreeVar(p))
@@ -1461,12 +1499,12 @@ bool CegConjectureSingleInvSol::getMatch(Node p,
   return false;
 }
 
-bool CegConjectureSingleInvSol::getMatch(Node t,
-                                         TypeNode st,
-                                         int& index_found,
-                                         std::vector<Node>& args,
-                                         int index_exc,
-                                         int index_start)
+bool CegSingleInvSol::getMatch(Node t,
+                               TypeNode st,
+                               int& index_found,
+                               std::vector<Node>& args,
+                               int index_exc,
+                               int index_start)
 {
   Assert(st.isDatatype());
   const Datatype& dt = static_cast<DatatypeType>(st.toType()).getDatatype();
@@ -1517,9 +1555,7 @@ bool CegConjectureSingleInvSol::getMatch(Node t,
   return false;
 }
 
-Node CegConjectureSingleInvSol::getGenericBase(TypeNode tn,
-                                               const Datatype& dt,
-                                               int c)
+Node CegSingleInvSol::getGenericBase(TypeNode tn, const Datatype& dt, int c)
 {
   std::map<int, Node>::iterator it = d_generic_base[tn].find(c);
   if (it != d_generic_base[tn].end())
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
index 8d18611cf..fb0862413 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
@@ -24,19 +24,19 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class CegSingleInv;
 
-class CegConjectureSingleInv;
-
-/** CegConjectureSingleInvSol
+/** CegSingleInvSol
  *
  * This function implements Figure 5 of "Counterexample-Guided Quantifier
  * Instantiation for Synthesis in SMT", Reynolds et al CAV 2015.
  *
  */
-class CegConjectureSingleInvSol
+class CegSingleInvSol
 {
-  friend class CegConjectureSingleInv;
-private:
+  friend class CegSingleInv;
+
+ private:
   QuantifiersEngine * d_qe;
   std::vector< Node > d_varList;
   std::map< Node, int > d_dterm_size;
@@ -55,7 +55,7 @@ private:
                              std::vector< Node >& vars, std::vector< Node >& subs, int status );
 
  public:
-  CegConjectureSingleInvSol(QuantifiersEngine* qe);
+  CegSingleInvSol(QuantifiersEngine* qe);
   /** simplify solution
    *
    * Returns the simplified version of node sol whose syntax is restricted by
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 204daa49a..fbe0da7a8 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -16,7 +16,7 @@
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
-#include "theory/quantifiers/sygus/ce_guided_conjecture.h"
+#include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/theory_engine.h"
 
@@ -28,7 +28,7 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-Cegis::Cegis(QuantifiersEngine* qe, CegConjecture* p)
+Cegis::Cegis(QuantifiersEngine* qe, SynthConjecture* p)
     : SygusModule(qe, p), d_eval_unfold(nullptr), d_using_gr_repair(false)
 {
   if (options::sygusEvalUnfold())
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index ce4186eb2..c7392b378 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -41,7 +41,7 @@ namespace quantifiers {
 class Cegis : public SygusModule
 {
  public:
-  Cegis(QuantifiersEngine* qe, CegConjecture* p);
+  Cegis(QuantifiersEngine* qe, SynthConjecture* p);
   ~Cegis() override {}
   /** initialize */
   virtual bool initialize(Node n,
@@ -69,11 +69,11 @@ class Cegis : public SygusModule
  protected:
   /** the evaluation unfold utility of d_tds */
   SygusEvalUnfold* d_eval_unfold;
-  /** If CegConjecture::d_base_inst is exists y. P( d, y ), then this is y. */
+  /** If SynthConjecture::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 ).
+   * If SynthConjecture::d_base_inst is exists y. P( d, y ), then this is the
+   * formula P( SynthConjecture::d_candidates, y ).
    */
   Node d_base_body;
   //----------------------------------cegis-implementation-specific
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 56cc40244..456f44019 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -17,8 +17,8 @@
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
-#include "theory/quantifiers/sygus/ce_guided_conjecture.h"
 #include "theory/quantifiers/sygus/sygus_unif_rl.h"
+#include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/theory_engine.h"
 
@@ -28,7 +28,7 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-CegisUnif::CegisUnif(QuantifiersEngine* qe, CegConjecture* p)
+CegisUnif::CegisUnif(QuantifiersEngine* qe, SynthConjecture* p)
     : Cegis(qe, p), d_sygus_unif(p), d_u_enum_manager(qe, p)
 {
 }
@@ -299,8 +299,8 @@ void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars,
       OR, d_parent->getGuard().negate(), plem));
 }
 
-CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe,
-                                           CegConjecture* parent)
+CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(
+    QuantifiersEngine* qe, SynthConjecture* parent)
     : DecisionStrategyFmf(qe->getSatContext(), qe->getValuation()),
       d_qe(qe),
       d_parent(parent)
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index ae2d7964b..00cc5af72 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -47,7 +47,7 @@ namespace quantifiers {
 class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
 {
  public:
-  CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe, CegConjecture* parent);
+  CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe, SynthConjecture* parent);
   /** Make the n^th literal of this strategy (G_uq_n).
    *
    * This call may add new lemmas of the form described above
@@ -96,7 +96,7 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
   /** sygus term database of d_qe */
   TermDbSygus* d_tds;
   /** reference to the parent conjecture */
-  CegConjecture* d_parent;
+  SynthConjecture* d_parent;
   /** whether this module has been initialized */
   bool d_initialized;
   /** null node */
@@ -194,7 +194,7 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
 class CegisUnif : public Cegis
 {
  public:
-  CegisUnif(QuantifiersEngine* qe, CegConjecture* p);
+  CegisUnif(QuantifiersEngine* qe, SynthConjecture* p);
   ~CegisUnif() override;
   /** Retrieves enumerators for constructing solutions
    *
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index e05df8581..eadbf766a 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -20,9 +20,9 @@
 #include "options/quantifiers_options.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/datatypes/datatypes_rewriter.h"
-#include "theory/quantifiers/sygus/ce_guided_conjecture.h"
 #include "theory/quantifiers/sygus/sygus_grammar_norm.h"
 #include "theory/quantifiers/sygus/sygus_process_conj.h"
+#include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 
@@ -33,7 +33,7 @@ namespace theory {
 namespace quantifiers {
 
 CegGrammarConstructor::CegGrammarConstructor(QuantifiersEngine* qe,
-                                             CegConjecture* p)
+                                             SynthConjecture* p)
     : d_qe(qe), d_parent(p), d_is_syntax_restricted(false)
 {
 }
@@ -95,10 +95,11 @@ Node CegGrammarConstructor::process(Node q,
 {
   // convert to deep embedding and finalize single invocation here
   // now, construct the grammar
-  Trace("cegqi") << "CegConjecture : convert to deep embedding..." << std::endl;
+  Trace("cegqi") << "SynthConjecture : convert to deep embedding..."
+                 << std::endl;
   std::map< TypeNode, std::vector< Node > > extra_cons;
   if( options::sygusAddConstGrammar() ){
-    Trace("cegqi") << "CegConjecture : collect constants..." << std::endl;
+    Trace("cegqi") << "SynthConjecture : collect constants..." << std::endl;
     collectTerms( q[1], extra_cons );
   }
   std::map<TypeNode, std::vector<Node>> exc_cons;
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
index 33c0a836b..022031bef 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
@@ -24,7 +24,7 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-class CegConjecture;
+class SynthConjecture;
 
 /** utility for constructing datatypes that correspond to syntactic restrictions,
 * and applying the deep embedding from Section 4 of Reynolds et al CAV 2015.
@@ -32,7 +32,7 @@ class CegConjecture;
 class CegGrammarConstructor
 {
 public:
- CegGrammarConstructor(QuantifiersEngine* qe, CegConjecture* p);
+ CegGrammarConstructor(QuantifiersEngine* qe, SynthConjecture* p);
  ~CegGrammarConstructor() {}
  /** process
   *
@@ -114,7 +114,7 @@ public:
   /** parent conjecture
   * This contains global information about the synthesis conjecture.
   */
-  CegConjecture* d_parent;
+  SynthConjecture* d_parent;
   /** is the syntax restricted? */
   bool d_is_syntax_restricted;
   /** collect terms */
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index 868e69b21..3d066e8dd 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -22,7 +22,6 @@
 #include "smt/smt_engine_scope.h"
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
-#include "theory/quantifiers/sygus/ce_guided_conjecture.h"
 #include "theory/quantifiers/sygus/sygus_grammar_red.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp
index 54a3cce50..24b47b216 100644
--- a/src/theory/quantifiers/sygus/sygus_invariance.cpp
+++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp
@@ -14,8 +14,8 @@
 
 #include "theory/quantifiers/sygus/sygus_invariance.h"
 
-#include "theory/quantifiers/sygus/ce_guided_conjecture.h"
 #include "theory/quantifiers/sygus/sygus_pbe.h"
+#include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
 using namespace CVC4::kind;
@@ -87,7 +87,7 @@ bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
 }
 
 void EquivSygusInvarianceTest::init(
-    TermDbSygus* tds, TypeNode tn, CegConjecture* aconj, Node e, Node bvr)
+    TermDbSygus* tds, TypeNode tn, SynthConjecture* aconj, Node e, Node bvr)
 {
   // compute the current examples
   d_bvr = bvr;
diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h
index 20cd1fd03..59761da5c 100644
--- a/src/theory/quantifiers/sygus/sygus_invariance.h
+++ b/src/theory/quantifiers/sygus/sygus_invariance.h
@@ -27,7 +27,7 @@ namespace theory {
 namespace quantifiers {
 
 class TermDbSygus;
-class CegConjecture;
+class SynthConjecture;
 
 /* SygusInvarianceTest
 *
@@ -181,7 +181,7 @@ class EquivSygusInvarianceTest : public SygusInvarianceTest
    * are checking for invariance
    */
   void init(
-      TermDbSygus* tds, TypeNode tn, CegConjecture* aconj, Node e, Node bvr);
+      TermDbSygus* tds, TypeNode tn, SynthConjecture* aconj, Node e, Node bvr);
 
  protected:
   /** checks whether the analog of nvn still rewrites to d_bvr */
@@ -189,7 +189,7 @@ class EquivSygusInvarianceTest : public SygusInvarianceTest
 
  private:
   /** the conjecture associated with the enumerator d_enum */
-  CegConjecture* d_conj;
+  SynthConjecture* d_conj;
   /** the enumerator associated with the term for which this test is for */
   Node d_enum;
   /** the RHS of the evaluation */
diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp
index b36fe4281..3471472fa 100644
--- a/src/theory/quantifiers/sygus/sygus_module.cpp
+++ b/src/theory/quantifiers/sygus/sygus_module.cpp
@@ -18,7 +18,7 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-SygusModule::SygusModule(QuantifiersEngine* qe, CegConjecture* p)
+SygusModule::SygusModule(QuantifiersEngine* qe, SynthConjecture* p)
     : d_qe(qe), d_tds(qe->getTermDatabaseSygus()), d_parent(p)
 {
 }
diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index e2a9fae80..c1b12dfd0 100644
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -25,20 +25,20 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-class CegConjecture;
+class SynthConjecture;
 
 /** 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.
+ * This is the base class of sygus modules, owned by SynthConjecture. The
+ * purpose of this class is to, when applicable, suggest candidate solutions for
+ * SynthConjecture to test.
  *
- * In more detail, an instance of the conjecture class (CegConjecture) creates
+ * In more detail, an instance of the conjecture class (SynthConjecture) 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:
+ * conjecture (see SynthConjecture::d_base_inst) is the formula:
  *   exists y. P( k, y )
  * where k are the "candidate" variables for the conjecture.
  *
@@ -48,12 +48,12 @@ class CegConjecture;
 class SygusModule
 {
  public:
-  SygusModule(QuantifiersEngine* qe, CegConjecture* p);
+  SygusModule(QuantifiersEngine* qe, SynthConjecture* p);
   virtual ~SygusModule() {}
   /** initialize
    *
    * n is the "base instantiation" of the deep-embedding version of the
-   * synthesis conjecture under candidates (see CegConjecture::d_base_inst).
+   * synthesis conjecture under candidates (see SynthConjecture::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.
@@ -127,7 +127,7 @@ class SygusModule
   /** sygus term database of d_qe */
   quantifiers::TermDbSygus* d_tds;
   /** reference to the parent conjecture */
-  CegConjecture* d_parent;
+  SynthConjecture* d_parent;
 };
 
 } /* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 6a82b9dad..9a6645560 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -28,7 +28,7 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-CegConjecturePbe::CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p)
+SygusPbe::SygusPbe(QuantifiersEngine* qe, SynthConjecture* p)
     : SygusModule(qe, p)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
@@ -36,13 +36,15 @@ CegConjecturePbe::CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p)
   d_is_pbe = false;
 }
 
-CegConjecturePbe::~CegConjecturePbe() {
-
-}
+SygusPbe::~SygusPbe() {}
 
 //--------------------------------- collecting finite input/output domain information
 
-void CegConjecturePbe::collectExamples( Node n, std::map< Node, bool >& visited, bool hasPol, bool pol ) {
+void SygusPbe::collectExamples(Node n,
+                               std::map<Node, bool>& visited,
+                               bool hasPol,
+                               bool pol)
+{
   if( visited.find( n )==visited.end() ){
     visited[n] = true;
     Node neval;
@@ -116,9 +118,9 @@ void CegConjecturePbe::collectExamples( Node n, std::map< Node, bool >& visited,
   }
 }
 
-bool CegConjecturePbe::initialize(Node n,
-                                  const std::vector<Node>& candidates,
-                                  std::vector<Node>& lemmas)
+bool SygusPbe::initialize(Node n,
+                          const std::vector<Node>& candidates,
+                          std::vector<Node>& lemmas)
 {
   Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl;
 
@@ -248,9 +250,13 @@ bool CegConjecturePbe::initialize(Node n,
   return true;
 }
 
-Node CegConjecturePbe::PbeTrie::addPbeExample(TypeNode etn, Node e, Node b,
-                                              CegConjecturePbe* cpbe,
-                                              unsigned index, unsigned ntotal) {
+Node SygusPbe::PbeTrie::addPbeExample(TypeNode etn,
+                                      Node e,
+                                      Node b,
+                                      SygusPbe* cpbe,
+                                      unsigned index,
+                                      unsigned ntotal)
+{
   if (index == ntotal) {
     // lazy child holds the leaf data
     if (d_lazy_child.isNull()) {
@@ -281,16 +287,20 @@ Node CegConjecturePbe::PbeTrie::addPbeExample(TypeNode etn, Node e, Node b,
   }
 }
 
-Node CegConjecturePbe::PbeTrie::addPbeExampleEval(TypeNode etn, Node e, Node b,
-                                                  std::vector<Node>& ex,
-                                                  CegConjecturePbe* cpbe,
-                                                  unsigned index,
-                                                  unsigned ntotal) {
+Node SygusPbe::PbeTrie::addPbeExampleEval(TypeNode etn,
+                                          Node e,
+                                          Node b,
+                                          std::vector<Node>& ex,
+                                          SygusPbe* 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) {
+bool SygusPbe::hasExamples(Node e)
+{
   if (isPbe()) {
     e = d_tds->getSynthFunForEnumerator(e);
     Assert(!e.isNull());
@@ -302,7 +312,8 @@ bool CegConjecturePbe::hasExamples(Node e) {
   return false;
 }
 
-unsigned CegConjecturePbe::getNumExamples(Node e) {
+unsigned SygusPbe::getNumExamples(Node e)
+{
   e = d_tds->getSynthFunForEnumerator(e);
   Assert(!e.isNull());
   std::map<Node, std::vector<std::vector<Node> > >::iterator it =
@@ -314,7 +325,8 @@ unsigned CegConjecturePbe::getNumExamples(Node e) {
   }
 }
 
-void CegConjecturePbe::getExample(Node e, unsigned i, std::vector<Node>& ex) {
+void SygusPbe::getExample(Node e, unsigned i, std::vector<Node>& ex)
+{
   e = d_tds->getSynthFunForEnumerator(e);
   Assert(!e.isNull());
   std::map<Node, std::vector<std::vector<Node> > >::iterator it =
@@ -327,7 +339,8 @@ void CegConjecturePbe::getExample(Node e, unsigned i, std::vector<Node>& ex) {
   }
 }
 
-Node CegConjecturePbe::getExampleOut(Node e, unsigned i) {
+Node SygusPbe::getExampleOut(Node e, unsigned i)
+{
   e = d_tds->getSynthFunForEnumerator(e);
   Assert(!e.isNull());
   std::map<Node, std::vector<Node> >::iterator it = d_examples_out.find(e);
@@ -340,7 +353,8 @@ Node CegConjecturePbe::getExampleOut(Node e, unsigned i) {
   }
 }
 
-Node CegConjecturePbe::addSearchVal(TypeNode tn, Node e, Node bvr) {
+Node SygusPbe::addSearchVal(TypeNode tn, Node e, Node bvr)
+{
   Assert(isPbe());
   Assert(!e.isNull());
   e = d_tds->getSynthFunForEnumerator(e);
@@ -355,8 +369,8 @@ Node CegConjecturePbe::addSearchVal(TypeNode tn, Node e, Node bvr) {
   return Node::null();
 }
 
-Node CegConjecturePbe::evaluateBuiltin(TypeNode tn, Node bn, Node e,
-                                       unsigned i) {
+Node SygusPbe::evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i)
+{
   e = d_tds->getSynthFunForEnumerator(e);
   Assert(!e.isNull());
   std::map<Node, bool>::iterator itx = d_examples_invalid.find(e);
@@ -373,8 +387,8 @@ Node CegConjecturePbe::evaluateBuiltin(TypeNode tn, Node bn, Node e,
 
 // ------------------------------------------- solution construction from enumeration
 
-void CegConjecturePbe::getTermList(const std::vector<Node>& candidates,
-                                   std::vector<Node>& terms)
+void SygusPbe::getTermList(const std::vector<Node>& candidates,
+                           std::vector<Node>& terms)
 {
   Valuation& valuation = d_qe->getValuation();
   for( unsigned i=0; i<candidates.size(); i++ ){
@@ -401,11 +415,11 @@ void CegConjecturePbe::getTermList(const std::vector<Node>& candidates,
   }
 }
 
-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)
+bool SygusPbe::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() ){
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h
index 49d853248..66e19b6c9 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.h
+++ b/src/theory/quantifiers/sygus/sygus_pbe.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_PBE_H
-#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_PBE_H
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H
 
 #include "context/cdhashmap.h"
 #include "theory/quantifiers/sygus/sygus_module.h"
@@ -25,79 +25,79 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-class CegConjecture;
+class SynthConjecture;
 
-/** CegConjecturePbe
-*
-* This class implements optimizations that target synthesis conjectures
-* that are in Programming-By-Examples (PBE) form.
-*
-* [EX#1] An example of a synthesis conjecture in PBE form 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.
-*
-* Internally, this class does the following for SyGuS inputs:
-*
-* (1) Infers whether the input conjecture is in PBE form or not.
-* (2) Based on this information and on the syntactic restrictions, it
-*     devises a strategy for enumerating terms and construction solutions,
-*     which is inspired by Alur et al. "Scaling Enumerative Program Synthesis
-*     via Divide and Conquer" TACAS 2017. In particular, it may consider
-*     strategies for constructing decision trees when the grammar permits ITEs
-*     and a strategy for divide-and-conquer string synthesis when the grammar
-*     permits string concatenation. This is managed through the SygusUnif
-*     utilities, d_sygus_unif.
-* (3) It makes (possibly multiple) calls to
-*     TermDatabaseSygus::regstierEnumerator(...) based
-*     on the strategy, which inform the rest of the system to enumerate values
-*     of particular types in the grammar through use of fresh variables which
-*     we call "enumerators".
-*
-* Points (1)-(3) happen within a call to CegConjecturePbe::initialize(...).
-*
-* Notice that each enumerator is associated with a single
-* function-to-synthesize, but a function-to-sythesize may be mapped to multiple
-* enumerators. Some public functions of this class expect an enumerator as
-* input, which we map to a function-to-synthesize via
-* TermDatabaseSygus::getSynthFunFor(e).
-*
-* An enumerator is initially "active" but may become inactive if the enumeration
-* exhausts all possible values in the datatype corresponding to syntactic
-* restrictions for it. The search may continue unless all enumerators become
-* inactive.
-*
-* (4) During search, the extension of quantifier-free datatypes procedure for
-*     SyGuS datatypes may ask this class whether current candidates can be
-*     discarded based on inferring when two candidate solutions are equivalent
-*     up to examples. For example, the candidate solutions:
-*     f = \x ite( x < 0, x+1, x ) and f = \x x
-*     are equivalent up to examples on the above conjecture, since they have the
-*     same value on the points x = 0,5,6. Hence, we need only consider one of
-*     them. The interface for querying this is
-*       CegConjecturePbe::addSearchVal(...).
-*     For details, see Reynolds et al. SYNT 2017.
-*
-* (5) When the extension of quantifier-free datatypes procedure for SyGuS
-*     datatypes terminates with a model, the parent of this class calls
-*     CegConjecturePbe::getCandidateList(...), where this class returns the list
-*     of active enumerators.
-* (6) The parent class subsequently calls
-*     CegConjecturePbe::constructValues(...), which informs this class that new
-*     values have been enumerated for active enumerators, as indicated by the
-*     current model. This call also requests that based on these
-*     newly enumerated values, whether this class is now able to construct a
-*     solution based on the high-level strategy (stored in d_sygus_unif).
-*
-* This class is not designed to work in incremental mode, since there is no way
-* to specify incremental problems in SyguS.
-*/
-class CegConjecturePbe : public SygusModule
+/** SygusPbe
+ *
+ * This class implements optimizations that target synthesis conjectures
+ * that are in Programming-By-Examples (PBE) form.
+ *
+ * [EX#1] An example of a synthesis conjecture in PBE form 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.
+ *
+ * Internally, this class does the following for SyGuS inputs:
+ *
+ * (1) Infers whether the input conjecture is in PBE form or not.
+ * (2) Based on this information and on the syntactic restrictions, it
+ *     devises a strategy for enumerating terms and construction solutions,
+ *     which is inspired by Alur et al. "Scaling Enumerative Program Synthesis
+ *     via Divide and Conquer" TACAS 2017. In particular, it may consider
+ *     strategies for constructing decision trees when the grammar permits ITEs
+ *     and a strategy for divide-and-conquer string synthesis when the grammar
+ *     permits string concatenation. This is managed through the SygusUnif
+ *     utilities, d_sygus_unif.
+ * (3) It makes (possibly multiple) calls to
+ *     TermDatabaseSygus::regstierEnumerator(...) based
+ *     on the strategy, which inform the rest of the system to enumerate values
+ *     of particular types in the grammar through use of fresh variables which
+ *     we call "enumerators".
+ *
+ * Points (1)-(3) happen within a call to SygusPbe::initialize(...).
+ *
+ * Notice that each enumerator is associated with a single
+ * function-to-synthesize, but a function-to-sythesize may be mapped to multiple
+ * enumerators. Some public functions of this class expect an enumerator as
+ * input, which we map to a function-to-synthesize via
+ * TermDatabaseSygus::getSynthFunFor(e).
+ *
+ * An enumerator is initially "active" but may become inactive if the
+ * enumeration exhausts all possible values in the datatype corresponding to
+ * syntactic restrictions for it. The search may continue unless all enumerators
+ * become inactive.
+ *
+ * (4) During search, the extension of quantifier-free datatypes procedure for
+ *     SyGuS datatypes may ask this class whether current candidates can be
+ *     discarded based on inferring when two candidate solutions are equivalent
+ *     up to examples. For example, the candidate solutions:
+ *     f = \x ite( x < 0, x+1, x ) and f = \x x
+ *     are equivalent up to examples on the above conjecture, since they have
+ * the same value on the points x = 0,5,6. Hence, we need only consider one of
+ *     them. The interface for querying this is
+ *       SygusPbe::addSearchVal(...).
+ *     For details, see Reynolds et al. SYNT 2017.
+ *
+ * (5) When the extension of quantifier-free datatypes procedure for SyGuS
+ *     datatypes terminates with a model, the parent of this class calls
+ *     SygusPbe::getCandidateList(...), where this class returns the list
+ *     of active enumerators.
+ * (6) The parent class subsequently calls
+ *     SygusPbe::constructValues(...), which informs this class that new
+ *     values have been enumerated for active enumerators, as indicated by the
+ *     current model. This call also requests that based on these
+ *     newly enumerated values, whether this class is now able to construct a
+ *     solution based on the high-level strategy (stored in d_sygus_unif).
+ *
+ * This class is not designed to work in incremental mode, since there is no way
+ * to specify incremental problems in SyguS.
+ */
+class SygusPbe : public SygusModule
 {
  public:
-  CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p);
-  ~CegConjecturePbe();
+  SygusPbe(QuantifiersEngine* qe, SynthConjecture* p);
+  ~SygusPbe();
 
   /** initialize this class
   *
@@ -276,7 +276,7 @@ class CegConjecturePbe : public SygusModule
     Node addPbeExample(TypeNode etn,
                        Node e,
                        Node b,
-                       CegConjecturePbe* cpbe,
+                       SygusPbe* cpbe,
                        unsigned index,
                        unsigned ntotal);
 
@@ -286,7 +286,7 @@ class CegConjecturePbe : public SygusModule
                            Node e,
                            Node b,
                            std::vector<Node>& ex,
-                           CegConjecturePbe* cpbe,
+                           SygusPbe* cpbe,
                            unsigned index,
                            unsigned ntotal);
   };
diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
index b0b6159be..a2454758a 100644
--- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp
+++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
@@ -29,7 +29,7 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-void CegConjectureProcessFun::init(Node f)
+void SynthConjectureProcessFun::init(Node f)
 {
   d_synth_fun = f;
   Assert(f.getType().isFunction());
@@ -47,11 +47,11 @@ void CegConjectureProcessFun::init(Node f)
     Node k = NodeManager::currentNM()->mkBoundVar(ss.str(), atn);
     d_arg_vars.push_back(k);
     d_arg_var_num[k] = j;
-    d_arg_props.push_back(CegConjectureProcessArg());
+    d_arg_props.push_back(SynthConjectureProcessArg());
   }
 }
 
-bool CegConjectureProcessFun::checkMatch(
+bool SynthConjectureProcessFun::checkMatch(
     Node cn, Node n, std::unordered_map<unsigned, Node>& n_arg_map)
 {
   std::vector<Node> vars;
@@ -73,7 +73,7 @@ bool CegConjectureProcessFun::checkMatch(
   return cn_subs == n;
 }
 
-bool CegConjectureProcessFun::isArgVar(Node n, unsigned& arg_index)
+bool SynthConjectureProcessFun::isArgVar(Node n, unsigned& arg_index)
 {
   if (n.isVar())
   {
@@ -88,7 +88,7 @@ bool CegConjectureProcessFun::isArgVar(Node n, unsigned& arg_index)
   return false;
 }
 
-Node CegConjectureProcessFun::inferDefinition(
+Node SynthConjectureProcessFun::inferDefinition(
     Node n,
     std::unordered_map<Node, unsigned, NodeHashFunction>& term_to_arg_carry,
     std::unordered_map<Node,
@@ -166,8 +166,8 @@ Node CegConjectureProcessFun::inferDefinition(
   return visited[n];
 }
 
-unsigned CegConjectureProcessFun::assignRelevantDef(Node def,
-                                                    std::vector<unsigned>& args)
+unsigned SynthConjectureProcessFun::assignRelevantDef(
+    Node def, std::vector<unsigned>& args)
 {
   unsigned id = 0;
   if (def.isNull())
@@ -250,7 +250,7 @@ unsigned CegConjectureProcessFun::assignRelevantDef(Node def,
   return rid;
 }
 
-void CegConjectureProcessFun::processTerms(
+void SynthConjectureProcessFun::processTerms(
     std::vector<Node>& ns,
     std::vector<Node>& ks,
     Node nf,
@@ -504,12 +504,12 @@ void CegConjectureProcessFun::processTerms(
   }
 }
 
-bool CegConjectureProcessFun::isArgRelevant(unsigned i)
+bool SynthConjectureProcessFun::isArgRelevant(unsigned i)
 {
   return d_arg_props[i].d_relevant;
 }
 
-void CegConjectureProcessFun::getIrrelevantArgs(
+void SynthConjectureProcessFun::getIrrelevantArgs(
     std::unordered_set<unsigned>& args)
 {
   for (unsigned i = 0; i < d_arg_vars.size(); i++)
@@ -521,15 +521,15 @@ void CegConjectureProcessFun::getIrrelevantArgs(
   }
 }
 
-CegConjectureProcess::CegConjectureProcess(QuantifiersEngine* qe) {}
-CegConjectureProcess::~CegConjectureProcess() {}
-Node CegConjectureProcess::preSimplify(Node q)
+SynthConjectureProcess::SynthConjectureProcess(QuantifiersEngine* qe) {}
+SynthConjectureProcess::~SynthConjectureProcess() {}
+Node SynthConjectureProcess::preSimplify(Node q)
 {
   Trace("sygus-process") << "Pre-simplify conjecture : " << q << std::endl;
   return q;
 }
 
-Node CegConjectureProcess::postSimplify(Node q)
+Node SynthConjectureProcess::postSimplify(Node q)
 {
   Trace("sygus-process") << "Post-simplify conjecture : " << q << std::endl;
   Assert(q.getKind() == FORALL);
@@ -561,7 +561,7 @@ Node CegConjectureProcess::postSimplify(Node q)
     getComponentVector(AND, base, conjuncts);
 
     // process the conjunctions
-    for (std::map<Node, CegConjectureProcessFun>::iterator it =
+    for (std::map<Node, SynthConjectureProcessFun>::iterator it =
              d_sf_info.begin();
          it != d_sf_info.end();
          ++it)
@@ -577,7 +577,7 @@ Node CegConjectureProcess::postSimplify(Node q)
   return q;
 }
 
-void CegConjectureProcess::initialize(Node n, std::vector<Node>& candidates)
+void SynthConjectureProcess::initialize(Node n, std::vector<Node>& candidates)
 {
   if (Trace.isOn("sygus-process"))
   {
@@ -590,13 +590,13 @@ void CegConjectureProcess::initialize(Node n, std::vector<Node>& candidates)
   }
 }
 
-bool CegConjectureProcess::isArgRelevant(Node f, unsigned i)
+bool SynthConjectureProcess::isArgRelevant(Node f, unsigned i)
 {
   if (!options::sygusArgRelevant())
   {
     return true;
   }
-  std::map<Node, CegConjectureProcessFun>::iterator its = d_sf_info.find(f);
+  std::map<Node, SynthConjectureProcessFun>::iterator its = d_sf_info.find(f);
   if (its != d_sf_info.end())
   {
     return its->second.isArgRelevant(i);
@@ -605,10 +605,10 @@ bool CegConjectureProcess::isArgRelevant(Node f, unsigned i)
   return true;
 }
 
-bool CegConjectureProcess::getIrrelevantArgs(Node f,
-                                             std::unordered_set<unsigned>& args)
+bool SynthConjectureProcess::getIrrelevantArgs(
+    Node f, std::unordered_set<unsigned>& args)
 {
-  std::map<Node, CegConjectureProcessFun>::iterator its = d_sf_info.find(f);
+  std::map<Node, SynthConjectureProcessFun>::iterator its = d_sf_info.find(f);
   if (its != d_sf_info.end())
   {
     its->second.getIrrelevantArgs(args);
@@ -617,7 +617,7 @@ bool CegConjectureProcess::getIrrelevantArgs(Node f,
   return false;
 }
 
-void CegConjectureProcess::processConjunct(
+void SynthConjectureProcess::processConjunct(
     Node n, Node f, std::unordered_set<Node, NodeHashFunction>& synth_fv)
 {
   Trace("sygus-process-arg-deps") << "Process conjunct: " << std::endl;
@@ -655,7 +655,7 @@ void CegConjectureProcess::processConjunct(
   // process the applications of synthesis functions
   if (!ns.empty())
   {
-    std::map<Node, CegConjectureProcessFun>::iterator its = d_sf_info.find(f);
+    std::map<Node, SynthConjectureProcessFun>::iterator its = d_sf_info.find(f);
     if (its != d_sf_info.end())
     {
       its->second.processTerms(ns, ks, nf, synth_fv_n, free_vars);
@@ -663,7 +663,7 @@ void CegConjectureProcess::processConjunct(
   }
 }
 
-Node CegConjectureProcess::CegConjectureProcess::flatten(
+Node SynthConjectureProcess::SynthConjectureProcess::flatten(
     Node n,
     Node f,
     std::unordered_set<Node, NodeHashFunction>& synth_fv,
@@ -728,7 +728,7 @@ Node CegConjectureProcess::CegConjectureProcess::flatten(
   return visited[n];
 }
 
-void CegConjectureProcess::getFreeVariables(
+void SynthConjectureProcess::getFreeVariables(
     Node n,
     std::unordered_set<Node, NodeHashFunction>& synth_fv,
     std::unordered_map<Node,
@@ -779,16 +779,16 @@ void CegConjectureProcess::getFreeVariables(
   } while (!visit.empty());
 }
 
-Node CegConjectureProcess::getSymmetryBreakingPredicate(
+Node SynthConjectureProcess::getSymmetryBreakingPredicate(
     Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth)
 {
   return Node::null();
 }
 
-void CegConjectureProcess::debugPrint(const char* c) {}
-void CegConjectureProcess::getComponentVector(Kind k,
-                                              Node n,
-                                              std::vector<Node>& args)
+void SynthConjectureProcess::debugPrint(const char* c) {}
+void SynthConjectureProcess::getComponentVector(Kind k,
+                                                Node n,
+                                                std::vector<Node>& args)
 {
   if (n.getKind() == k)
   {
diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h
index b16118b2e..199619699 100644
--- a/src/theory/quantifiers/sygus/sygus_process_conj.h
+++ b/src/theory/quantifiers/sygus/sygus_process_conj.h
@@ -88,10 +88,10 @@ namespace quantifiers {
  * position in the function to synthesize is
  * relevant.
  */
-class CegConjectureProcessArg
+class SynthConjectureProcessArg
 {
  public:
-  CegConjectureProcessArg() : d_var_single_occ(false), d_relevant(false) {}
+  SynthConjectureProcessArg() : d_var_single_occ(false), d_relevant(false) {}
   /** template definition
    * This is the term s[z] described
    * under "Argument Invariance" above.
@@ -120,11 +120,11 @@ class CegConjectureProcessArg
 * It maintains information about each of the function to
 * synthesize's arguments.
 */
-struct CegConjectureProcessFun
+struct SynthConjectureProcessFun
 {
  public:
-  CegConjectureProcessFun() {}
-  ~CegConjectureProcessFun() {}
+  SynthConjectureProcessFun() {}
+  ~SynthConjectureProcessFun() {}
   /** initialize this class for function f */
   void init(Node f);
   /** process terms
@@ -159,12 +159,12 @@ struct CegConjectureProcessFun
   /** the synth fun associated with this */
   Node d_synth_fun;
   /** properties of each argument */
-  std::vector<CegConjectureProcessArg> d_arg_props;
+  std::vector<SynthConjectureProcessArg> d_arg_props;
   /** variables for each argument type of f
    *
    * These are used to express templates for argument
    * invariance, in the data member
-   * CegConjectureProcessArg::d_template.
+   * SynthConjectureProcessArg::d_template.
    */
   std::vector<Node> d_arg_vars;
   /** map from d_arg_vars to the argument #
@@ -254,51 +254,50 @@ struct CegConjectureProcessFun
 };
 
 /** Ceg Conjecture Process
-*
-* This class implements static techniques for preprocessing and analysis of
-* sygus conjectures.
-*
-* It is used as a back-end to CegConjecture, which calls it using the following
-* interface:
-* (1) When a sygus conjecture is asserted, we call
-* CegConjectureProcess::simplify( q ),
-*     where q is the sygus conjecture in original form.
-*
-* (2) After a sygus conjecture is simplified and converted to deep
-* embedding form, we call CegConjectureProcess::initialize( n, candidates ).
-*
-* (3) During enumerative SyGuS search, calls may be made by
-* the extension of the quantifier-free datatypes decision procedure for
-* sygus to CegConjectureProcess::getSymmetryBreakingPredicate(...), which are
-* used for pruning search space based on conjecture-specific analysis.
-*/
-class CegConjectureProcess
+ *
+ * This class implements static techniques for preprocessing and analysis of
+ * sygus conjectures.
+ *
+ * It is used as a back-end to SynthConjecture, which calls it using the
+ * following interface: (1) When a sygus conjecture is asserted, we call
+ * SynthConjectureProcess::simplify( q ),
+ *     where q is the sygus conjecture in original form.
+ *
+ * (2) After a sygus conjecture is simplified and converted to deep
+ * embedding form, we call SynthConjectureProcess::initialize( n, candidates ).
+ *
+ * (3) During enumerative SyGuS search, calls may be made by
+ * the extension of the quantifier-free datatypes decision procedure for
+ * sygus to SynthConjectureProcess::getSymmetryBreakingPredicate(...), which are
+ * used for pruning search space based on conjecture-specific analysis.
+ */
+class SynthConjectureProcess
 {
  public:
-  CegConjectureProcess(QuantifiersEngine* qe);
-  ~CegConjectureProcess();
+  SynthConjectureProcess(QuantifiersEngine* qe);
+  ~SynthConjectureProcess();
   /** simplify the synthesis conjecture q
-  * Returns a formula that is equivalent to q.
-  * This simplification pass is called before all others
-  * in CegConjecture::assign.
-  *
-  * This function is intended for simplifications that
-  * impact whether or not the synthesis conjecture is
-  * single-invocation.
-  */
+   * Returns a formula that is equivalent to q.
+   * This simplification pass is called before all others
+   * in SynthConjecture::assign.
+   *
+   * This function is intended for simplifications that
+   * impact whether or not the synthesis conjecture is
+   * single-invocation.
+   */
   Node preSimplify(Node q);
   /** simplify the synthesis conjecture q
-  * Returns a formula that is equivalent to q.
-  * This simplification pass is called after all others
-  * in CegConjecture::assign.
-  */
+   * Returns a formula that is equivalent to q.
+   * This simplification pass is called after all others
+   * in SynthConjecture::assign.
+   */
   Node postSimplify(Node q);
   /** initialize
-  *
-  * n is the "base instantiation" of the deep-embedding version of
-  *   the synthesis conjecture under "candidates".
-  *   (see CegConjecture::d_base_inst)
-  */
+   *
+   * n is the "base instantiation" of the deep-embedding version of
+   *   the synthesis conjecture under "candidates".
+   *   (see SynthConjecture::d_base_inst)
+   */
   void initialize(Node n, std::vector<Node>& candidates);
   /** is the i^th argument of the function-to-synthesize f relevant? */
   bool isArgRelevant(Node f, unsigned i);
@@ -352,7 +351,7 @@ class CegConjectureProcess
                          std::unordered_set<Node, NodeHashFunction>,
                          NodeHashFunction>& free_vars);
   /** for each synth-fun, information that is specific to this conjecture */
-  std::map<Node, CegConjectureProcessFun> d_sf_info;
+  std::map<Node, SynthConjectureProcessFun> d_sf_info;
 
   /** get component vector */
   void getComponentVector(Kind k, Node n, std::vector<Node>& args);
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 66639b750..b8d98a6f7 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -18,7 +18,7 @@
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
 #include "theory/datatypes/datatypes_rewriter.h"
-#include "theory/quantifiers/sygus/ce_guided_conjecture.h"
+#include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
 #include <math.h>
@@ -29,7 +29,7 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-SygusUnifRl::SygusUnifRl(CegConjecture* p) : d_parent(p) {}
+SygusUnifRl::SygusUnifRl(SynthConjecture* p) : d_parent(p) {}
 SygusUnifRl::~SygusUnifRl() {}
 void SygusUnifRl::initializeCandidate(
     QuantifiersEngine* qe,
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index aad3c0b49..7b07de34e 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -35,7 +35,7 @@ using BoolNodePairMap =
 using NodePairMap = std::unordered_map<Node, Node, NodeHashFunction>;
 using NodePair = std::pair<Node, Node>;
 
-class CegConjecture;
+class SynthConjecture;
 
 /** Sygus unification Refinement Lemmas utility
  *
@@ -46,7 +46,7 @@ class CegConjecture;
 class SygusUnifRl : public SygusUnif
 {
  public:
-  SygusUnifRl(CegConjecture* p);
+  SygusUnifRl(SynthConjecture* p);
   ~SygusUnifRl();
 
   /** initialize */
@@ -105,7 +105,7 @@ class SygusUnifRl : public SygusUnif
 
  protected:
   /** reference to the parent conjecture */
-  CegConjecture* d_parent;
+  SynthConjecture* d_parent;
   /* Functions-to-synthesize (a.k.a. candidates) with unification strategies */
   std::unordered_set<Node, NodeHashFunction> d_unif_candidates;
   /** construct sol */
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 30c0a3ae1..fde69d196 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file ce_guided_conjecture.cpp
+/*! \file synth_conjecture.cpp
  ** \verbatim
  ** Top contributors (to current version):
  **   Andrew Reynolds, Tim King, Haniel Barbosa
@@ -9,10 +9,10 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief implementation of class that encapsulates counterexample-guided instantiation
- **        techniques for a single SyGuS synthesis conjecture
+ ** \brief Implementation of class that encapsulates techniques for a single
+ ** (SyGuS) synthesis conjecture.
  **/
-#include "theory/quantifiers/sygus/ce_guided_conjecture.h"
+#include "theory/quantifiers/sygus/synth_conjecture.h"
 
 #include "expr/datatype.h"
 #include "options/base_options.h"
@@ -26,7 +26,7 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/sygus/ce_guided_instantiation.h"
+#include "theory/quantifiers/sygus/synth_engine.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/theory_engine.h"
@@ -38,13 +38,13 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-CegConjecture::CegConjecture(QuantifiersEngine* qe)
+SynthConjecture::SynthConjecture(QuantifiersEngine* qe)
     : d_qe(qe),
-      d_ceg_si(new CegConjectureSingleInv(qe, this)),
-      d_ceg_proc(new CegConjectureProcess(qe)),
+      d_ceg_si(new CegSingleInv(qe, this)),
+      d_ceg_proc(new SynthConjectureProcess(qe)),
       d_ceg_gc(new CegGrammarConstructor(qe, this)),
       d_sygus_rconst(new SygusRepairConst(qe)),
-      d_ceg_pbe(new CegConjecturePbe(qe, this)),
+      d_ceg_pbe(new SygusPbe(qe, this)),
       d_ceg_cegis(new Cegis(qe, this)),
       d_ceg_cegisUnif(new CegisUnif(qe, this)),
       d_master(nullptr),
@@ -63,30 +63,33 @@ CegConjecture::CegConjecture(QuantifiersEngine* qe)
   d_modules.push_back(d_ceg_cegis.get());
 }
 
-CegConjecture::~CegConjecture() {}
+SynthConjecture::~SynthConjecture() {}
 
-void CegConjecture::assign( Node q ) {
-  Assert( d_embed_quant.isNull() );
-  Assert( q.getKind()==FORALL );
-  Trace("cegqi") << "CegConjecture : assign : " << q << std::endl;
+void SynthConjecture::assign(Node q)
+{
+  Assert(d_embed_quant.isNull());
+  Assert(q.getKind() == FORALL);
+  Trace("cegqi") << "SynthConjecture : assign : " << q << std::endl;
   d_quant = q;
   NodeManager* nm = NodeManager::currentNM();
 
   // pre-simplify the quantified formula based on the process utility
   d_simp_quant = d_ceg_proc->preSimplify(d_quant);
 
-  std::map< Node, Node > templates; 
-  std::map< Node, Node > templates_arg;
-  //register with single invocation if applicable
+  std::map<Node, Node> templates;
+  std::map<Node, Node> templates_arg;
+  // register with single invocation if applicable
   if (d_qe->getQuantAttributes()->isSygus(q))
   {
     d_ceg_si->initialize(d_simp_quant);
     d_simp_quant = d_ceg_si->getSimplifiedConjecture();
     // carry the templates
-    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+    for (unsigned i = 0; i < q[0].getNumChildren(); i++)
+    {
       Node v = q[0][i];
       Node templ = d_ceg_si->getTemplate(v);
-      if( !templ.isNull() ){
+      if (!templ.isNull())
+      {
         templates[v] = templ;
         templates_arg[v] = d_ceg_si->getTemplateArg(v);
       }
@@ -100,23 +103,28 @@ void CegConjecture::assign( Node q ) {
 
   // convert to deep embedding and finalize single invocation here
   d_embed_quant = d_ceg_gc->process(d_simp_quant, templates, templates_arg);
-  Trace("cegqi") << "CegConjecture : converted to embedding : " << d_embed_quant << std::endl;
+  Trace("cegqi") << "SynthConjecture : converted to embedding : "
+                 << d_embed_quant << std::endl;
 
-  // we now finalize the single invocation module, based on the syntax restrictions
+  // we now finalize the single invocation module, based on the syntax
+  // restrictions
   if (d_qe->getQuantAttributes()->isSygus(q))
   {
     d_ceg_si->finishInit(d_ceg_gc->isSyntaxRestricted());
   }
 
-  Assert( d_candidates.empty() );
-  std::vector< Node > vars;
-  for( unsigned i=0; i<d_embed_quant[0].getNumChildren(); i++ ){
-    vars.push_back( d_embed_quant[0][i] );
-    Node e = NodeManager::currentNM()->mkSkolem( "e", d_embed_quant[0][i].getType() );
-    d_candidates.push_back( e );
+  Assert(d_candidates.empty());
+  std::vector<Node> vars;
+  for (unsigned i = 0; i < d_embed_quant[0].getNumChildren(); i++)
+  {
+    vars.push_back(d_embed_quant[0][i]);
+    Node e =
+        NodeManager::currentNM()->mkSkolem("e", d_embed_quant[0][i].getType());
+    d_candidates.push_back(e);
   }
-  Trace("cegqi") << "Base quantified formula is : " << d_embed_quant << std::endl;
-  //construct base instantiation
+  Trace("cegqi") << "Base quantified formula is : " << d_embed_quant
+                 << std::endl;
+  // construct base instantiation
   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;
@@ -139,8 +147,9 @@ void CegConjecture::assign( Node q ) {
 
   // register this term with sygus database and other utilities that impact
   // the enumerative sygus search
-  std::vector< Node > guarded_lemmas;
-  if( !isSingleInvocation() ){
+  std::vector<Node> guarded_lemmas;
+  if (!isSingleInvocation())
+  {
     d_ceg_proc->initialize(d_base_inst, d_candidates);
     for (unsigned i = 0, size = d_modules.size(); i < size; i++)
     {
@@ -162,7 +171,7 @@ void CegConjecture::assign( Node q ) {
       d_inner_vars.push_back(v);
     }
   }
-  
+
   // initialize the guard
   d_feasible_guard = nm->mkSkolem("G", nm->booleanType());
   d_feasible_guard = Rewriter::rewrite(d_feasible_guard);
@@ -183,22 +192,27 @@ void CegConjecture::assign( Node q ) {
 
   if (isSingleInvocation())
   {
-    std::vector< Node > lems;
+    std::vector<Node> lems;
     d_ceg_si->getInitialSingleInvLemma(d_feasible_guard, lems);
-    for( unsigned i=0; i<lems.size(); i++ ){
-      Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation " << i << " : " << lems[i] << std::endl;
-      d_qe->getOutputChannel().lemma( lems[i] );
-      if( Trace.isOn("cegqi-debug") ){
-        Node rlem = Rewriter::rewrite( lems[i] );
+    for (unsigned i = 0; i < lems.size(); i++)
+    {
+      Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation " << i << " : "
+                           << lems[i] << std::endl;
+      d_qe->getOutputChannel().lemma(lems[i]);
+      if (Trace.isOn("cegqi-debug"))
+      {
+        Node rlem = Rewriter::rewrite(lems[i]);
         Trace("cegqi-debug") << "...rewritten : " << rlem << std::endl;
       }
     }
   }
   Node gneg = d_feasible_guard.negate();
-  for( unsigned i=0; i<guarded_lemmas.size(); i++ ){
+  for (unsigned i = 0; i < guarded_lemmas.size(); i++)
+  {
     Node lem = nm->mkNode(OR, gneg, guarded_lemmas[i]);
-    Trace("cegqi-lemma") << "Cegqi::Lemma : initial (guarded) lemma : " << lem << std::endl;
-    d_qe->getOutputChannel().lemma( lem );
+    Trace("cegqi-lemma") << "Cegqi::Lemma : initial (guarded) lemma : " << lem
+                         << std::endl;
+    d_qe->getOutputChannel().lemma(lem);
   }
 
   if (options::sygusStream())
@@ -210,18 +224,21 @@ void CegConjecture::assign( Node q ) {
         d_stream_strategy.get());
     d_current_stream_guard = d_stream_strategy->getLiteral(0);
   }
-  Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation() << std::endl;
+  Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation()
+                 << std::endl;
 }
 
-Node CegConjecture::getGuard() const { return d_feasible_guard; }
+Node SynthConjecture::getGuard() const { return d_feasible_guard; }
 
-bool CegConjecture::isSingleInvocation() const {
+bool SynthConjecture::isSingleInvocation() const
+{
   return d_ceg_si->isSingleInvocation();
 }
 
-bool CegConjecture::needsCheck()
+bool SynthConjecture::needsCheck()
 {
-  if( isSingleInvocation() && !d_ceg_si->needsCheck() ){
+  if (isSingleInvocation() && !d_ceg_si->needsCheck())
+  {
     return false;
   }
   bool value;
@@ -244,15 +261,16 @@ bool CegConjecture::needsCheck()
   return true;
 }
 
-
-void CegConjecture::doSingleInvCheck(std::vector< Node >& lems) {
-  if( d_ceg_si!=NULL ){
+void SynthConjecture::doSingleInvCheck(std::vector<Node>& lems)
+{
+  if (d_ceg_si != NULL)
+  {
     d_ceg_si->check(lems);
   }
 }
 
-bool CegConjecture::needsRefinement() const { return d_set_ce_sk_vars; }
-void CegConjecture::doCheck(std::vector<Node>& lems)
+bool SynthConjecture::needsRefinement() const { return d_set_ce_sk_vars; }
+void SynthConjecture::doCheck(std::vector<Node>& lems)
 {
   Assert(d_master != nullptr);
 
@@ -331,11 +349,14 @@ void CegConjecture::doCheck(std::vector<Node>& lems)
 
   NodeManager* nm = NodeManager::currentNM();
 
-  //must get a counterexample to the value of the current candidate
+  // 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;
+  if (constructed_cand)
+  {
+    if (Trace.isOn("cegqi-check"))
+    {
+      Trace("cegqi-check") << "CegConjuncture : check candidate : "
+                           << std::endl;
       for (unsigned i = 0, size = candidate_values.size(); i < size; i++)
       {
         Trace("cegqi-check") << "  " << i << " : " << d_candidates[i] << " -> "
@@ -347,13 +368,16 @@ void CegConjecture::doCheck(std::vector<Node>& lems)
                                   d_candidates.end(),
                                   candidate_values.begin(),
                                   candidate_values.end());
-  }else{
+  }
+  else
+  {
     inst = d_base_inst;
   }
-  
-  //check whether we will run CEGIS on inner skolem variables
+
+  // check whether we will run CEGIS on inner skolem variables
   bool sk_refine = (!isGround() || d_refine_count == 0) && constructed_cand;
-  if( sk_refine ){
+  if (sk_refine)
+  {
     if (options::cegisSample() == CEGIS_SAMPLE_TRUST)
     {
       // we have that the current candidate passed a sample test
@@ -366,13 +390,16 @@ void CegConjecture::doCheck(std::vector<Node>& lems)
       return;
     }
     Assert(!d_set_ce_sk_vars);
-  }else{
-    if( !constructed_cand ){
+  }
+  else
+  {
+    if (!constructed_cand)
+    {
       return;
     }
   }
-  
-  //immediately skolemize inner existentials
+
+  // immediately skolemize inner existentials
   Node lem;
   // introduce the skolem variables
   std::vector<Node> sks;
@@ -488,16 +515,18 @@ void CegConjecture::doCheck(std::vector<Node>& lems)
   lem = getStreamGuardedLemma(lem);
   lems.push_back(lem);
 }
-        
-void CegConjecture::doRefine( std::vector< Node >& lems ){
-  Assert( lems.empty() );
+
+void SynthConjecture::doRefine(std::vector<Node>& lems)
+{
+  Assert(lems.empty());
   Assert(d_set_ce_sk_vars);
 
-  //first, make skolem substitution
-  Trace("cegqi-refine") << "doRefine : construct skolem substitution..." << std::endl;
-  std::vector< Node > sk_vars;
-  std::vector< Node > sk_subs;
-  //collect the substitution over all disjuncts
+  // first, make skolem substitution
+  Trace("cegqi-refine") << "doRefine : construct skolem substitution..."
+                        << std::endl;
+  std::vector<Node> sk_vars;
+  std::vector<Node> sk_subs;
+  // collect the substitution over all disjuncts
   if (!d_ce_sk_vars.empty())
   {
     Trace("cegqi-refine") << "Get model values for skolems..." << std::endl;
@@ -521,8 +550,9 @@ void CegConjecture::doRefine( std::vector< Node >& lems ){
     Assert(d_inner_vars.empty());
   }
 
-  std::vector< Node > lem_c;
-  Trace("cegqi-refine") << "doRefine : Construct refinement lemma..." << std::endl;
+  std::vector<Node> lem_c;
+  Trace("cegqi-refine") << "doRefine : Construct refinement lemma..."
+                        << std::endl;
   Trace("cegqi-refine-debug")
       << "  For counterexample skolems : " << d_ce_sk_vars << std::endl;
   Node base_lem;
@@ -535,12 +565,13 @@ void CegConjecture::doRefine( std::vector< Node >& lems ){
     base_lem = d_base_inst.negate();
   }
 
-  Assert( sk_vars.size()==sk_subs.size() );
+  Assert(sk_vars.size() == sk_subs.size());
 
   Trace("cegqi-refine") << "doRefine : substitute..." << std::endl;
-  base_lem = base_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
+  base_lem = base_lem.substitute(
+      sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end());
   Trace("cegqi-refine") << "doRefine : rewrite..." << std::endl;
-  base_lem = Rewriter::rewrite( base_lem );
+  base_lem = Rewriter::rewrite(base_lem);
   Trace("cegqi-refine") << "doRefine : register refinement lemma " << base_lem
                         << "..." << std::endl;
   d_master->registerRefinementLemma(sk_vars, base_lem, lems);
@@ -550,16 +581,20 @@ void CegConjecture::doRefine( std::vector< Node >& lems ){
   d_ce_sk_var_mvs.clear();
 }
 
-void CegConjecture::preregisterConjecture( Node q ) {
-  d_ceg_si->preregisterConjecture( q );
+void SynthConjecture::preregisterConjecture(Node q)
+{
+  d_ceg_si->preregisterConjecture(q);
 }
 
-void CegConjecture::getModelValues( std::vector< Node >& n, std::vector< Node >& v ) {
+void SynthConjecture::getModelValues(std::vector<Node>& n, std::vector<Node>& v)
+{
   Trace("cegqi-engine") << "  * Value is : ";
-  for( unsigned i=0; i<n.size(); i++ ){
-    Node nv = getModelValue( n[i] );
-    v.push_back( nv );
-    if( Trace.isOn("cegqi-engine") ){
+  for (unsigned i = 0; i < n.size(); i++)
+  {
+    Node nv = getModelValue(n[i]);
+    v.push_back(nv);
+    if (Trace.isOn("cegqi-engine"))
+    {
       TypeNode tn = nv.getType();
       Trace("cegqi-engine") << n[i] << " -> ";
       std::stringstream ss;
@@ -572,23 +607,26 @@ void CegConjecture::getModelValues( std::vector< Node >& n, std::vector< Node >&
         Trace("cegqi-engine-rr") << " -> " << bv << std::endl;
       }
     }
-    Assert( !nv.isNull() );
+    Assert(!nv.isNull());
   }
   Trace("cegqi-engine") << std::endl;
 }
 
-Node CegConjecture::getModelValue( Node n ) {
+Node SynthConjecture::getModelValue(Node n)
+{
   Trace("cegqi-mv") << "getModelValue for : " << n << std::endl;
-  return d_qe->getModel()->getValue( n );
+  return d_qe->getModel()->getValue(n);
 }
 
-void CegConjecture::debugPrint( const char * c ) {
+void SynthConjecture::debugPrint(const char* c)
+{
   Trace(c) << "Synthesis conjecture : " << d_embed_quant << std::endl;
   Trace(c) << "  * Candidate programs : " << d_candidates << std::endl;
   Trace(c) << "  * Counterexample skolems : " << d_ce_sk_vars << std::endl;
 }
 
-Node CegConjecture::getCurrentStreamGuard() const {
+Node SynthConjecture::getCurrentStreamGuard() const
+{
   if (d_stream_strategy != nullptr)
   {
     // the stream guard is the current asserted literal of the stream strategy
@@ -603,7 +641,7 @@ Node CegConjecture::getCurrentStreamGuard() const {
   return Node::null();
 }
 
-Node CegConjecture::getStreamGuardedLemma(Node n) const
+Node SynthConjecture::getStreamGuardedLemma(Node n) const
 {
   if (options::sygusStream())
   {
@@ -615,20 +653,20 @@ Node CegConjecture::getStreamGuardedLemma(Node n) const
   return n;
 }
 
-CegConjecture::SygusStreamDecisionStrategy::SygusStreamDecisionStrategy(
+SynthConjecture::SygusStreamDecisionStrategy::SygusStreamDecisionStrategy(
     context::Context* satContext, Valuation valuation)
     : DecisionStrategyFmf(satContext, valuation)
 {
 }
 
-Node CegConjecture::SygusStreamDecisionStrategy::mkLiteral(unsigned i)
+Node SynthConjecture::SygusStreamDecisionStrategy::mkLiteral(unsigned i)
 {
   NodeManager* nm = NodeManager::currentNM();
   Node curr_stream_guard = nm->mkSkolem("G_Stream", nm->booleanType());
   return curr_stream_guard;
 }
 
-void CegConjecture::printAndContinueStream()
+void SynthConjecture::printAndContinueStream()
 {
   Assert(d_master != nullptr);
   // we have generated a solution, print it
@@ -668,9 +706,11 @@ void CegConjecture::printAndContinueStream()
   d_qe->getOutputChannel().lemma(exc_lem);
 }
 
-void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation ) {
+void SynthConjecture::printSynthSolution(std::ostream& out,
+                                         bool singleInvocation)
+{
   Trace("cegqi-debug") << "Printing synth solution..." << std::endl;
-  Assert( d_quant[0].getNumChildren()==d_embed_quant[0].getNumChildren() );
+  Assert(d_quant[0].getNumChildren() == d_embed_quant[0].getNumChildren());
   std::vector<Node> sols;
   std::vector<int> statuses;
   if (!getSynthSolutionsInternal(sols, statuses, singleInvocation))
@@ -690,7 +730,7 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
       ss << prog;
       std::string f(ss.str());
       f.erase(f.begin());
-      CegInstantiation* cei = d_qe->getCegInstantiation();
+      SynthEngine* cei = d_qe->getSynthEngine();
       ++(cei->d_statistics.d_solutions);
 
       bool is_unique_term = true;
@@ -747,8 +787,8 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
   }
 }
 
-void CegConjecture::getSynthSolutions(std::map<Node, Node>& sol_map,
-                                      bool singleInvocation)
+void SynthConjecture::getSynthSolutions(std::map<Node, Node>& sol_map,
+                                        bool singleInvocation)
 {
   NodeManager* nm = NodeManager::currentNM();
   TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus();
@@ -784,9 +824,9 @@ void CegConjecture::getSynthSolutions(std::map<Node, Node>& sol_map,
   }
 }
 
-bool CegConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
-                                              std::vector<int>& statuses,
-                                              bool singleInvocation)
+bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
+                                                std::vector<int>& statuses,
+                                                bool singleInvocation)
 {
   for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
   {
@@ -868,7 +908,7 @@ bool CegConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
   return true;
 }
 
-Node CegConjecture::getSymmetryBreakingPredicate(
+Node SynthConjecture::getSymmetryBreakingPredicate(
     Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth)
 {
   std::vector<Node> sb_lemmas;
@@ -895,6 +935,6 @@ Node CegConjecture::getSymmetryBreakingPredicate(
   }
 }
 
-}/* namespace CVC4::theory::quantifiers */
-}/* namespace CVC4::theory */
-}/* namespace CVC4 */
+}  // namespace quantifiers
+}  // namespace theory
+} /* namespace CVC4 */
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index adc75056e..1cbd4e949 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file ce_guided_conjecture.h
+/*! \file synth_conjecture.h
  ** \verbatim
  ** Top contributors (to current version):
  **   Andrew Reynolds, Tim King, Haniel Barbosa
@@ -9,14 +9,14 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief class that encapsulates counterexample-guided instantiation
- **        techniques for a single SyGuS synthesis conjecture
+ ** \brief Class that encapsulates techniques for a single (SyGuS) synthesis
+ ** conjecture.
  **/
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_CONJECTURE_H
-#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_CONJECTURE_H
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H
+#define __CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H
 
 #include <memory>
 
@@ -42,10 +42,11 @@ namespace quantifiers {
  * determines which approach and optimizations are applicable to the
  * conjecture, and has interfaces for implementing them.
  */
-class CegConjecture {
-public:
-  CegConjecture( QuantifiersEngine * qe );
-  ~CegConjecture();
+class SynthConjecture
+{
+ public:
+  SynthConjecture(QuantifiersEngine* qe);
+  ~SynthConjecture();
   /** get original version of conjecture */
   Node getConjecture() { return d_quant; }
   /** get deep embedding version of conjecture */
@@ -58,18 +59,19 @@ public:
   bool needsCheck();
   /** whether the conjecture is waiting for a call to doRefine below */
   bool needsRefinement() const;
-  /** do single invocation check 
-  * This updates Gamma for an iteration of step 2 of Figure 1 of Reynolds et al CAV 2015.
-  */
-  void doSingleInvCheck(std::vector< Node >& lems);
-  /** do syntax-guided enumerative check 
-  * This is step 2(a) of Figure 3 of Reynolds et al CAV 2015.
-  */
+  /** do single invocation check
+   * This updates Gamma for an iteration of step 2 of Figure 1 of Reynolds et al
+   * CAV 2015.
+   */
+  void doSingleInvCheck(std::vector<Node>& lems);
+  /** 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);
-  /** do refinement 
-  * This is step 2(b) of Figure 3 of Reynolds et al CAV 2015.
-  */
-  void doRefine(std::vector< Node >& lems);
+  /** do refinement
+   * This is step 2(b) of Figure 3 of Reynolds et al CAV 2015.
+   */
+  void doRefine(std::vector<Node>& lems);
   //-------------------------------end for counterexample-guided check/refine
   /**
    * prints the synthesis solution to output stream out.
@@ -77,7 +79,7 @@ public:
    * singleInvocation : set to true if we should consult the single invocation
    * module to get synthesis solutions.
    */
-  void printSynthSolution( std::ostream& out, bool singleInvocation );
+  void printSynthSolution(std::ostream& out, bool singleInvocation);
   /** get synth solutions
    *
    * This returns a map from function-to-synthesize variables to their
@@ -99,43 +101,45 @@ public:
   bool isGround() { return d_inner_vars.empty(); }
   /** are we using single invocation techniques */
   bool isSingleInvocation() const;
-  /** preregister conjecture 
-  * This is used as a heuristic for solution reconstruction, so that we 
-  * remember expressions in the conjecture before preprocessing, since they
-  * may be helpful during solution reconstruction (Figure 5 of Reynolds et al CAV 2015)
-  */
-  void preregisterConjecture( Node q );
+  /** preregister conjecture
+   * This is used as a heuristic for solution reconstruction, so that we
+   * remember expressions in the conjecture before preprocessing, since they
+   * may be helpful during solution reconstruction (Figure 5 of Reynolds et al
+   * CAV 2015)
+   */
+  void preregisterConjecture(Node q);
   /** assign conjecture q to this class */
-  void assign( Node q );
+  void assign(Node q);
   /** has a conjecture been assigned to this class */
   bool isAssigned() { return !d_embed_quant.isNull(); }
   /** get model values for terms n, store in vector v */
-  void getModelValues( std::vector< Node >& n, std::vector< Node >& v );
+  void getModelValues(std::vector<Node>& n, std::vector<Node>& v);
   /** get model value for term n */
-  Node getModelValue( Node n );
+  Node getModelValue(Node n);
 
   /** get utility for static preprocessing and analysis of conjectures */
-  CegConjectureProcess* getProcess() { return d_ceg_proc.get(); }
+  SynthConjectureProcess* getProcess() { return d_ceg_proc.get(); }
   /** get constant repair utility */
   SygusRepairConst* getRepairConst() { return d_sygus_rconst.get(); }
   /** get program by examples module */
-  CegConjecturePbe* getPbe() { return d_ceg_pbe.get(); }
+  SygusPbe* getPbe() { return d_ceg_pbe.get(); }
   /** get the symmetry breaking predicate for type */
   Node getSymmetryBreakingPredicate(
       Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth);
   /** print out debug information about this conjecture */
-  void debugPrint( const char * c );
-private:
+  void debugPrint(const char* c);
+
+ private:
   /** reference to quantifier engine */
-  QuantifiersEngine * d_qe;
+  QuantifiersEngine* d_qe;
   /** The feasible guard. */
   Node d_feasible_guard;
   /** the decision strategy for the feasible guard */
   std::unique_ptr<DecisionStrategy> d_feasible_strategy;
   /** single invocation utility */
-  std::unique_ptr<CegConjectureSingleInv> d_ceg_si;
+  std::unique_ptr<CegSingleInv> d_ceg_si;
   /** utility for static preprocessing and analysis of conjectures */
-  std::unique_ptr<CegConjectureProcess> d_ceg_proc;
+  std::unique_ptr<SynthConjectureProcess> d_ceg_proc;
   /** grammar utility */
   std::unique_ptr<CegGrammarConstructor> d_ceg_gc;
   /** repair constant utility */
@@ -143,7 +147,7 @@ private:
 
   //------------------------modules
   /** program by examples module */
-  std::unique_ptr<CegConjecturePbe> d_ceg_pbe;
+  std::unique_ptr<SygusPbe> d_ceg_pbe;
   /** CEGIS module */
   std::unique_ptr<Cegis> d_ceg_cegis;
   /** CEGIS UNIF module */
@@ -159,17 +163,17 @@ private:
   //------------------------end modules
 
   /** list of constants for quantified formula
-  * The outer Skolems for the negation of d_embed_quant.
-  */
-  std::vector< Node > d_candidates;
+   * The outer Skolems for the negation of d_embed_quant.
+   */
+  std::vector<Node> d_candidates;
   /** base instantiation
-  * If d_embed_quant is forall d. exists y. P( d, y ), then
-  * this is the formula  exists y. P( d_candidates, y ). Notice that
-  * (exists y. F) is shorthand above for ~( forall y. ~F ).
-  */
+   * If d_embed_quant is forall d. exists y. P( d, y ), then
+   * this is the formula  exists y. P( d_candidates, y ). Notice that
+   * (exists y. F) is shorthand above for ~( forall y. ~F ).
+   */
   Node d_base_inst;
   /** list of variables on inner quantification */
-  std::vector< Node > d_inner_vars;
+  std::vector<Node> d_inner_vars;
   /**
    * The set of skolems for the current "verification" lemma, if one exists.
    * This may be added to during calls to doCheck(). The model values for these
@@ -195,11 +199,12 @@ private:
   /** (negated) conjecture after simplification, conversion to deep embedding */
   Node d_embed_quant;
   /** candidate information */
-  class CandidateInfo {
-  public:
-    CandidateInfo(){}
+  class CandidateInfo
+  {
+   public:
+    CandidateInfo() {}
     /** list of terms we have instantiated candidates with */
-    std::vector< Node > d_inst;
+    std::vector<Node> d_inst;
   };
   std::map<Node, CandidateInfo> d_cinfo;
   /**
@@ -210,12 +215,14 @@ private:
   /** number of times we have called doRefine */
   unsigned d_refine_count;
   /** get candidadate */
-  Node getCandidate( unsigned int i ) { return d_candidates[i]; }
+  Node getCandidate(unsigned int i) { return d_candidates[i]; }
   /** record instantiation (this is used to construct solutions later) */
-  void recordInstantiation( std::vector< Node >& vs ) {
-    Assert( vs.size()==d_candidates.size() );
-    for( unsigned i=0; i<vs.size(); i++ ){
-      d_cinfo[d_candidates[i]].d_inst.push_back( vs[i] );
+  void recordInstantiation(std::vector<Node>& vs)
+  {
+    Assert(vs.size() == d_candidates.size());
+    for (unsigned i = 0; i < vs.size(); i++)
+    {
+      d_cinfo[d_candidates[i]].d_inst.push_back(vs[i]);
     }
   }
   /** get synth solutions internal
@@ -284,8 +291,8 @@ private:
   std::map<Node, ExpressionMinerManager> d_exprm;
 };
 
-} /* namespace CVC4::theory::quantifiers */
-} /* namespace CVC4::theory */
+}  // namespace quantifiers
+}  // namespace theory
 } /* namespace CVC4 */
 
 #endif
diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index d30cccd87..56844ec1f 100644
--- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file ce_guided_instantiation.cpp
+/*! \file synth_engine.cpp
  ** \verbatim
  ** Top contributors (to current version):
  **   Andrew Reynolds, Tim King, Morgan Deters
@@ -9,11 +9,11 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief counterexample guided instantiation class
- **   This class is the entry point for both synthesis algorithms in Reynolds et al CAV 2015
+ ** \brief Implementation of the quantifiers module for managing all approaches
+ ** to synthesis, in particular, those described in Reynolds et al CAV 2015.
  **
  **/
-#include "theory/quantifiers/sygus/ce_guided_instantiation.h"
+#include "theory/quantifiers/sygus/synth_engine.h"
 
 #include "options/quantifiers_options.h"
 #include "smt/smt_engine.h"
@@ -31,26 +31,27 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){
-  d_conj = new CegConjecture( qe );
+SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c)
+    : QuantifiersModule(qe)
+{
+  d_conj = new SynthConjecture(qe);
   d_last_inst_si = false;
 }
 
-CegInstantiation::~CegInstantiation(){ 
-  delete d_conj;
-}
+SynthEngine::~SynthEngine() { delete d_conj; }
 
-bool CegInstantiation::needsCheck( Theory::Effort e ) {
+bool SynthEngine::needsCheck(Theory::Effort e)
+{
   return !d_quantEngine->getTheoryEngine()->needCheck()
          && e >= Theory::EFFORT_LAST_CALL;
 }
 
-QuantifiersModule::QEffort CegInstantiation::needsModel(Theory::Effort e)
+QuantifiersModule::QEffort SynthEngine::needsModel(Theory::Effort e)
 {
   return d_conj->isSingleInvocation() ? QEFFORT_STANDARD : QEFFORT_MODEL;
 }
 
-void CegInstantiation::check(Theory::Effort e, QEffort quant_e)
+void SynthEngine::check(Theory::Effort e, QEffort quant_e)
 {
   // are we at the proper effort level?
   unsigned echeck =
@@ -100,7 +101,7 @@ void CegInstantiation::check(Theory::Effort e, QEffort quant_e)
       << "Finished Counterexample Guided Instantiation engine." << std::endl;
 }
 
-bool CegInstantiation::assignConjecture(Node q)
+bool SynthEngine::assignConjecture(Node q)
 {
   if (d_conj->isAssigned())
   {
@@ -231,7 +232,7 @@ bool CegInstantiation::assignConjecture(Node q)
   return true;
 }
 
-void CegInstantiation::registerQuantifier(Node q)
+void SynthEngine::registerQuantifier(Node q)
 {
   if (d_quantEngine->getOwner(q) == this)
   {  // && d_eval_axioms.find( q )==d_eval_axioms.end() ){
@@ -247,24 +248,30 @@ void CegInstantiation::registerQuantifier(Node q)
         // assign it now
         assignConjecture(q);
       }
-    }else{
-      Assert( d_conj->getEmbeddedConjecture()==q );
     }
-  }else{
+    else
+    {
+      Assert(d_conj->getEmbeddedConjecture() == q);
+    }
+  }
+  else
+  {
     Trace("cegqi-debug") << "Register quantifier : " << q << std::endl;
   }
 }
 
-void CegInstantiation::checkConjecture(CegConjecture* conj)
+void SynthEngine::checkConjecture(SynthConjecture* conj)
 {
   Node q = conj->getEmbeddedConjecture();
   Node aq = conj->getConjecture();
-  if( Trace.isOn("cegqi-engine-debug") ){
+  if (Trace.isOn("cegqi-engine-debug"))
+  {
     conj->debugPrint("cegqi-engine-debug");
     Trace("cegqi-engine-debug") << std::endl;
   }
 
-  if( !conj->needsRefinement() ){
+  if (!conj->needsRefinement())
+  {
     Trace("cegqi-engine-debug") << "Do conjecture check..." << std::endl;
     if (conj->isSingleInvocation())
     {
@@ -308,7 +315,9 @@ void CegInstantiation::checkConjecture(CegConjecture* conj)
       {
         ++(d_statistics.d_cegqi_lemmas_ce);
         addedLemma = true;
-      }else{
+      }
+      else
+      {
         // this may happen if we eagerly unfold, simplify to true
         Trace("cegqi-engine-debug")
             << "  ...FAILED to add candidate!" << std::endl;
@@ -317,7 +326,9 @@ void CegInstantiation::checkConjecture(CegConjecture* conj)
     if (addedLemma)
     {
       Trace("cegqi-engine") << "  ...check for counterexample." << std::endl;
-    }else{
+    }
+    else
+    {
       if (conj->needsRefinement())
       {
         // immediately go to refine candidate
@@ -325,41 +336,50 @@ void CegInstantiation::checkConjecture(CegConjecture* conj)
         return;
       }
     }
-  }else{
+  }
+  else
+  {
     Trace("cegqi-engine") << "  *** Refine candidate phase..." << std::endl;
-    std::vector< Node > rlems;
-    conj->doRefine( rlems );
+    std::vector<Node> rlems;
+    conj->doRefine(rlems);
     bool addedLemma = false;
-    for( unsigned i=0; i<rlems.size(); i++ ){
+    for (unsigned i = 0; i < rlems.size(); i++)
+    {
       Node lem = rlems[i];
-      Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem << std::endl;
-      bool res = d_quantEngine->addLemma( lem );
-      if( res ){
+      Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem
+                           << std::endl;
+      bool res = d_quantEngine->addLemma(lem);
+      if (res)
+      {
         ++(d_statistics.d_cegqi_lemmas_refine);
         conj->incrementRefineCount();
         addedLemma = true;
-      }else{
+      }
+      else
+      {
         Trace("cegqi-warn") << "  ...FAILED to add refinement!" << std::endl;
       }
     }
-    if( addedLemma ){
+    if (addedLemma)
+    {
       Trace("cegqi-engine") << "  ...refine candidate." << std::endl;
     }
   }
 }
 
-void CegInstantiation::printSynthSolution( std::ostream& out ) {
-  if( d_conj->isAssigned() )
+void SynthEngine::printSynthSolution(std::ostream& out)
+{
+  if (d_conj->isAssigned())
   {
-    d_conj->printSynthSolution( out, d_last_inst_si );
+    d_conj->printSynthSolution(out, d_last_inst_si);
   }
   else
   {
-    Assert( false );
+    Assert(false);
   }
 }
 
-void CegInstantiation::getSynthSolutions(std::map<Node, Node>& sol_map)
+void SynthEngine::getSynthSolutions(std::map<Node, Node>& sol_map)
 {
   if (d_conj->isAssigned())
   {
@@ -367,22 +387,25 @@ void CegInstantiation::getSynthSolutions(std::map<Node, Node>& sol_map)
   }
 }
 
-void CegInstantiation::preregisterAssertion( Node n ) {
-  //check if it sygus conjecture
-  if( QuantAttributes::checkSygusConjecture( n ) ){
-    //this is a sygus conjecture
+void SynthEngine::preregisterAssertion(Node n)
+{
+  // check if it sygus conjecture
+  if (QuantAttributes::checkSygusConjecture(n))
+  {
+    // this is a sygus conjecture
     Trace("cegqi") << "Preregister sygus conjecture : " << n << std::endl;
-    d_conj->preregisterConjecture( n );
+    d_conj->preregisterConjecture(n);
   }
 }
 
-CegInstantiation::Statistics::Statistics()
-    : d_cegqi_lemmas_ce("CegInstantiation::cegqi_lemmas_ce", 0),
-      d_cegqi_lemmas_refine("CegInstantiation::cegqi_lemmas_refine", 0),
-      d_cegqi_si_lemmas("CegInstantiation::cegqi_lemmas_si", 0),
-      d_solutions("CegConjecture::solutions", 0),
-      d_candidate_rewrites_print("CegConjecture::candidate_rewrites_print", 0),
-      d_candidate_rewrites("CegConjecture::candidate_rewrites", 0)
+SynthEngine::Statistics::Statistics()
+    : d_cegqi_lemmas_ce("SynthEngine::cegqi_lemmas_ce", 0),
+      d_cegqi_lemmas_refine("SynthEngine::cegqi_lemmas_refine", 0),
+      d_cegqi_si_lemmas("SynthEngine::cegqi_lemmas_si", 0),
+      d_solutions("SynthConjecture::solutions", 0),
+      d_candidate_rewrites_print("SynthConjecture::candidate_rewrites_print",
+                                 0),
+      d_candidate_rewrites("SynthConjecture::candidate_rewrites", 0)
 
 {
   smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_ce);
@@ -393,7 +416,8 @@ CegInstantiation::Statistics::Statistics()
   smtStatisticsRegistry()->registerStat(&d_candidate_rewrites);
 }
 
-CegInstantiation::Statistics::~Statistics(){
+SynthEngine::Statistics::~Statistics()
+{
   smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_ce);
   smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_refine);
   smtStatisticsRegistry()->unregisterStat(&d_cegqi_si_lemmas);
@@ -402,6 +426,6 @@ CegInstantiation::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites);
 }
 
-}/* namespace CVC4::theory::quantifiers */
-}/* namespace CVC4::theory */
-}/* namespace CVC4 */
+}  // namespace quantifiers
+}  // namespace theory
+} /* namespace CVC4 */
diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.h b/src/theory/quantifiers/sygus/synth_engine.h
index 6bf33effb..a7004c5c7 100644
--- a/src/theory/quantifiers/sygus/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/sygus/synth_engine.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file ce_guided_instantiation.h
+/*! \file synth_engine.h
  ** \verbatim
  ** Top contributors (to current version):
  **   Andrew Reynolds, Mathias Preiner, Tim King
@@ -9,28 +9,30 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief counterexample guided instantiation class
+ ** \brief The quantifiers module for managing all approaches to synthesis,
+ ** in particular, those described in Reynolds et al CAV 2015.
  **/
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_INSTANTIATION_H
-#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_INSTANTIATION_H
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H
+#define __CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H
 
 #include "context/cdhashmap.h"
-#include "theory/quantifiers/sygus/ce_guided_conjecture.h"
+#include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-class CegInstantiation : public QuantifiersModule
+class SynthEngine : public QuantifiersModule
 {
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
-private:
+
+ private:
   /** the quantified formula stating the synthesis conjecture */
-  CegConjecture * d_conj;
+  SynthConjecture* d_conj;
   /** last instantiation by single invocation module? */
   bool d_last_inst_si;
   /** the conjecture we are waiting to assign */
@@ -48,38 +50,41 @@ private:
    */
   bool assignConjecture(Node q);
   /** check conjecture */
-  void checkConjecture(CegConjecture* conj);
+  void checkConjecture(SynthConjecture* conj);
+
+ public:
+  SynthEngine(QuantifiersEngine* qe, context::Context* c);
+  ~SynthEngine();
+
+ public:
+  bool needsCheck(Theory::Effort e) override;
+  QEffort needsModel(Theory::Effort e) override;
+  /* Call during quantifier engine's check */
+  void check(Theory::Effort e, QEffort quant_e) override;
+  /* Called for new quantifiers */
+  void registerQuantifier(Node q) override;
+  /** Identify this module (for debugging, dynamic configuration, etc..) */
+  std::string identify() const override { return "SynthEngine"; }
+  /** print solution for synthesis conjectures */
+  void printSynthSolution(std::ostream& out);
+  /** get synth solutions
+   *
+   * This function adds entries to sol_map that map functions-to-synthesize
+   * with their solutions, for all active conjectures (currently just the one
+   * assigned to d_conj). This should be called immediately after the solver
+   * answers unsat for sygus input.
+   *
+   * For details on what is added to sol_map, see
+   * SynthConjecture::getSynthSolutions.
+   */
+  void getSynthSolutions(std::map<Node, Node>& sol_map);
+  /** preregister assertion (before rewrite) */
+  void preregisterAssertion(Node n);
 
  public:
-  CegInstantiation( QuantifiersEngine * qe, context::Context* c );
-  ~CegInstantiation();
-public:
- bool needsCheck(Theory::Effort e) override;
- QEffort needsModel(Theory::Effort e) override;
- /* Call during quantifier engine's check */
- void check(Theory::Effort e, QEffort quant_e) override;
- /* Called for new quantifiers */
- void registerQuantifier(Node q) override;
- /** Identify this module (for debugging, dynamic configuration, etc..) */
- std::string identify() const override { return "CegInstantiation"; }
- /** print solution for synthesis conjectures */
- void printSynthSolution(std::ostream& out);
- /** get synth solutions
-  *
-  * This function adds entries to sol_map that map functions-to-synthesize
-  * with their solutions, for all active conjectures (currently just the one
-  * assigned to d_conj). This should be called immediately after the solver
-  * answers unsat for sygus input.
-  *
-  * For details on what is added to sol_map, see
-  * CegConjecture::getSynthSolutions.
-  */
- void getSynthSolutions(std::map<Node, Node>& sol_map);
- /** preregister assertion (before rewrite) */
- void preregisterAssertion(Node n);
-public:
-  class Statistics {
-  public:
+  class Statistics
+  {
+   public:
     IntStat d_cegqi_lemmas_ce;
     IntStat d_cegqi_lemmas_refine;
     IntStat d_cegqi_si_lemmas;
@@ -88,12 +93,12 @@ public:
     IntStat d_candidate_rewrites;
     Statistics();
     ~Statistics();
-  };/* class CegInstantiation::Statistics */
+  }; /* class SynthEngine::Statistics */
   Statistics d_statistics;
-}; /* class CegInstantiation */
+}; /* class SynthEngine */
 
-} /* namespace CVC4::theory::quantifiers */
-} /* namespace CVC4::theory */
+}  // namespace quantifiers
+}  // namespace theory
 } /* namespace CVC4 */
 
 #endif
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 64adea6c5..1f4e34c1f 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -423,7 +423,7 @@ void TermDbSygus::registerSygusType( TypeNode tn ) {
 
 void TermDbSygus::registerEnumerator(Node e,
                                      Node f,
-                                     CegConjecture* conj,
+                                     SynthConjecture* conj,
                                      bool mkActiveGuard,
                                      bool useSymbolicCons)
 {
@@ -522,9 +522,9 @@ bool TermDbSygus::isEnumerator(Node e) const
   return d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end();
 }
 
-CegConjecture* TermDbSygus::getConjectureForEnumerator(Node e) const
+SynthConjecture* TermDbSygus::getConjectureForEnumerator(Node e) const
 {
-  std::map<Node, CegConjecture*>::const_iterator itm =
+  std::map<Node, SynthConjecture*>::const_iterator itm =
       d_enum_to_conjecture.find(e);
   if (itm != d_enum_to_conjecture.end()) {
     return itm->second;
@@ -563,9 +563,11 @@ bool TermDbSygus::usingSymbolicConsForEnumerator(Node e) const
 
 void TermDbSygus::getEnumerators(std::vector<Node>& mts)
 {
-  for (std::map<Node, CegConjecture*>::iterator itm =
+  for (std::map<Node, SynthConjecture*>::iterator itm =
            d_enum_to_conjecture.begin();
-       itm != d_enum_to_conjecture.end(); ++itm) {
+       itm != d_enum_to_conjecture.end();
+       ++itm)
+  {
     mts.push_back( itm->first );
   }
 }
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index fee556cf8..b7bdba3ab 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -29,7 +29,7 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-class CegConjecture;
+class SynthConjecture;
 
 // TODO :issue #1235 split and document this class
 class TermDbSygus {
@@ -76,13 +76,13 @@ class TermDbSygus {
    */
   void registerEnumerator(Node e,
                           Node f,
-                          CegConjecture* conj,
+                          SynthConjecture* conj,
                           bool mkActiveGuard = false,
                           bool useSymbolicCons = false);
   /** is e an enumerator registered with this class? */
   bool isEnumerator(Node e) const;
   /** return the conjecture e is associated with */
-  CegConjecture* getConjectureForEnumerator(Node e) const;
+  SynthConjecture* getConjectureForEnumerator(Node e) const;
   /** return the function-to-synthesize e is associated with */
   Node getSynthFunForEnumerator(Node e) const;
   /** get active guard for e */
@@ -252,7 +252,7 @@ class TermDbSygus {
   //------------------------------enumerators
   /** mapping from enumerator terms to the conjecture they are associated with
    */
-  std::map<Node, CegConjecture*> d_enum_to_conjecture;
+  std::map<Node, SynthConjecture*> d_enum_to_conjecture;
   /** mapping from enumerator terms to the function-to-synthesize they are
    * associated with 
    */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 7a5652e2f..320f50afb 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -47,8 +47,8 @@
 #include "theory/quantifiers/relevant_domain.h"
 #include "theory/quantifiers/rewrite_engine.h"
 #include "theory/quantifiers/skolemize.h"
-#include "theory/quantifiers/sygus/ce_guided_instantiation.h"
 #include "theory/quantifiers/sygus/sygus_eval_unfold.h"
+#include "theory/quantifiers/sygus/synth_engine.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_canonize.h"
 #include "theory/quantifiers/term_database.h"
@@ -96,7 +96,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
       d_qcf(nullptr),
       d_rr_engine(nullptr),
       d_sg_gen(nullptr),
-      d_ceg_inst(nullptr),
+      d_synth_e(nullptr),
       d_lte_part_inst(nullptr),
       d_fs(nullptr),
       d_i_cbqi(nullptr),
@@ -192,8 +192,8 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
     }
   }
   if( options::ceGuidedInst() ){
-    d_ceg_inst.reset(new quantifiers::CegInstantiation(this, c));
-    d_modules.push_back(d_ceg_inst.get());
+    d_synth_e.reset(new quantifiers::SynthEngine(this, c));
+    d_modules.push_back(d_synth_e.get());
     //needsBuilder = true;
   }  
   //finite model finding
@@ -374,9 +374,9 @@ quantifiers::RewriteEngine* QuantifiersEngine::getRewriteEngine() const
 {
   return d_rr_engine.get();
 }
-quantifiers::CegInstantiation* QuantifiersEngine::getCegInstantiation() const
+quantifiers::SynthEngine* QuantifiersEngine::getSynthEngine() const
 {
-  return d_ceg_inst.get();
+  return d_synth_e.get();
 }
 quantifiers::InstStrategyEnum* QuantifiersEngine::getInstStrategyEnum() const
 {
@@ -1148,8 +1148,9 @@ void QuantifiersEngine::printInstantiations( std::ostream& out ) {
 }
 
 void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
-  if( d_ceg_inst ){
-    d_ceg_inst->printSynthSolution( out );
+  if (d_synth_e)
+  {
+    d_synth_e->printSynthSolution(out);
   }else{
     out << "Internal error : module for synth solution not found." << std::endl;
   }
@@ -1260,7 +1261,7 @@ Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){
 
 void QuantifiersEngine::getSynthSolutions(std::map<Node, Node>& sol_map)
 {
-  d_ceg_inst->getSynthSolutions(sol_map);
+  d_synth_e->getSynthSolutions(sol_map);
 }
 
 void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 77713744b..512f0c651 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -68,7 +68,7 @@ namespace quantifiers {
   class RewriteEngine;
   class QModelBuilder;
   class ConjectureGenerator;
-  class CegInstantiation;
+  class SynthEngine;
   class LtePartialInst;
   class AlphaEquivalence;
   class InstStrategyEnum;
@@ -150,7 +150,7 @@ public:
   /** rewrite rules utility */
   quantifiers::RewriteEngine* getRewriteEngine() const;
   /** ceg instantiation */
-  quantifiers::CegInstantiation* getCegInstantiation() const;
+  quantifiers::SynthEngine* getSynthEngine() const;
   /** get full saturation */
   quantifiers::InstStrategyEnum* getInstStrategyEnum() const;
   /** get inst strategy cbqi */
@@ -375,7 +375,7 @@ public:
   /** subgoal generator */
   std::unique_ptr<quantifiers::ConjectureGenerator> d_sg_gen;
   /** ceg instantiation */
-  std::unique_ptr<quantifiers::CegInstantiation> d_ceg_inst;
+  std::unique_ptr<quantifiers::SynthEngine> d_synth_e;
   /** lte partial instantiation */
   std::unique_ptr<quantifiers::LtePartialInst> d_lte_part_inst;
   /** full saturation */