Move si solution reconstruction to own file, make more robust. Other refactoring.

7 files changed, 1259 insertions, 922 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 4ae3c16f8..60f3bc7c2 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -329,6 +329,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/ce_guided_instantiation.cpp \
 	theory/quantifiers/ce_guided_single_inv.h \
 	theory/quantifiers/ce_guided_single_inv.cpp \
+	theory/quantifiers/ce_guided_single_inv_sol.h \
+	theory/quantifiers/ce_guided_single_inv_sol.cpp \
 	theory/quantifiers/local_theory_ext.h \
 	theory/quantifiers/local_theory_ext.cpp \
 	theory/quantifiers/fun_def_process.h \
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 51cce2407..30eac03fb 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -32,21 +32,8 @@ using namespace std;
 
 namespace CVC4 {
 
-Node simpleNegate( Node n ){
-  if( n.getKind()==OR || n.getKind()==AND ){
-    std::vector< Node > children;
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      children.push_back( simpleNegate( n[i] ) );
-    }
-    return NodeManager::currentNM()->mkNode( n.getKind()==OR ? AND : OR, children );
-  }else{
-    return n.negate();
-  }
-}
-
-
-CegConjectureSingleInv::CegConjectureSingleInv( QuantifiersEngine * d_qe, Node q, CegConjecture * p ) : d_qe( d_qe ), d_parent( p ), d_quant( q ){
-
+CegConjectureSingleInv::CegConjectureSingleInv( QuantifiersEngine * qe, Node q, CegConjecture * p ) : d_qe( qe ), d_parent( p ), d_quant( q ){
+  d_sol = new CegConjectureSingleInvSol( qe );
 }
 
 Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) {
@@ -63,7 +50,7 @@ Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) {
       d_single_inv_sk_index[k] = i;
     }
     Node inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
-    inst = simpleNegate( inst );
+    inst = TermDb::simpleNegate( inst );
     Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl;
     return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst );
   }else{
@@ -212,7 +199,7 @@ void CegConjectureSingleInv::initialize() {
             disj.push_back( cr );
           }
           Node curr = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj );
-          curr = simpleNegate( curr );
+          curr = TermDb::simpleNegate( curr );
           Trace("cegqi-si") << "    " << curr;
           conjuncts.push_back( curr );
           if( !it->first.isNull() ){
@@ -414,7 +401,7 @@ bool CegConjectureSingleInv::analyzeSygusConjunct( Node p, Node n, std::map< Nod
     analyzeSygusConjunct( n[0][0], n[0][1], children, prog_invoke, progs, contains, false );
   }else{
     if( pol ){
-      n = simpleNegate( n );
+      n = TermDb::simpleNegate( n );
     }
     Trace("cegqi-si") << "Sygus conjunct : " << n << std::endl;
     children[p].push_back( n );
@@ -689,24 +676,25 @@ Node CegConjectureSingleInv::constructSolution( unsigned i, unsigned index ) {
     return d_inst[index][i];
   }else{
     Node cond = d_lemmas_produced[index];
-    cond = simpleNegate( cond );
+    cond = TermDb::simpleNegate( cond );
     Node ite1 = d_inst[index][i];
     Node ite2 = constructSolution( i, index+1 );
     return NodeManager::currentNM()->mkNode( ITE, cond, ite1, ite2 );
   }
 }
 
-Node CegConjectureSingleInv::getSolution( unsigned i, TypeNode stn, int& reconstructed ){
+Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& reconstructed ){
   Assert( !d_lemmas_produced.empty() );
-  Node s = constructSolution( i, 0 );
   const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
   Node varList = Node::fromExpr( dt.getSygusVarList() );
-  Node prog = d_quant[0][i];
+  Node prog = d_quant[0][sol_index];
   Node prog_app = d_single_inv_app_map[prog];
+  //get variables
   std::vector< Node > vars;
-  std::vector< Node > subs;
-  Trace("cegqi-si-debug-sol") << "Get solution for " << prog << ", which is applied as " << prog_app << std::endl;
+  Trace("csi-sol") << "Get solution for " << prog << ", which is applied as " << prog_app << std::endl;
   Assert( prog_app.getNumChildren()==varList.getNumChildren()+1 );
+  d_varList.clear();
+  d_sol->d_varList.clear();
   for( unsigned i=1; i<prog_app.getNumChildren(); i++ ){
     if( varList[i-1].getType().isBoolean() ){
       //TODO force boolean term conversion mode
@@ -715,135 +703,55 @@ Node CegConjectureSingleInv::getSolution( unsigned i, TypeNode stn, int& reconst
     }else{
       vars.push_back( prog_app[i] );
     }
-    subs.push_back( varList[i-1] );
-    d_varlist.push_back( varList[i-1] );
+    d_varList.push_back( varList[i-1] );
+    d_sol->d_varList.push_back( varList[i-1] );
   }
-  s = s.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+  //construct the solution
+  Node s = constructSolution( sol_index, 0 );
+  s = s.substitute( vars.begin(), vars.end(), d_varList.begin(), d_varList.end() );
   d_orig_solution = s;
-  Trace("cegqi-si-debug-sol") << "Solution (pre-rewrite): " << d_orig_solution << std::endl;
-  s = pullITEs( s );
-  //s = flattenITEs( s );
-  //do standard rewriting
-  s = Rewriter::rewrite( s );
 
-  std::map< Node, bool > sassign;
-  std::vector< Node > svars;
-  std::vector< Node > ssubs;
-  Trace("cegqi-si-debug-sol") << "Solution (pre-simplification): " << s << std::endl;
-  s = simplifySolution( s, sassign, svars, ssubs, subs, 0 );
-  Trace("cegqi-si-debug-sol") << "Solution (post-simplification): " << s << std::endl;
-  s = Rewriter::rewrite( s );
-  Trace("cegqi-si-debug-sol") << "Solution (post-rewrite): " << s << std::endl;
+  //simplify the solution
+  Trace("csi-sol") << "Solution (pre-simplification): " << d_orig_solution << std::endl;
+  s = d_sol->simplifySolution( s, stn );
+  Trace("csi-sol") << "Solution (post-simplification): " << s << std::endl;
   d_solution = s;
+
+  //reconstruct the solution into sygus if necessary
   reconstructed = 0;
   if( options::cegqiSingleInvReconstruct() && !stn.isNull() ){
-    int status;
-    d_templ_solution = collectReconstructNodes( d_qe->getTermDatabaseSygus(), d_solution, stn, status );
-    if( status==1 ){
-      setNeedsReconstruction( d_templ_solution, stn, Node::null(), TypeNode::null() );
-    }
-    Trace("cegqi-si-debug-sol") << "Induced solution template is : " << d_templ_solution << std::endl;
-    std::vector< TypeNode > rcons_tn;
-    for( std::map< TypeNode, std::map< Node, bool > >::iterator it = d_rcons_to_process.begin(); it != d_rcons_to_process.end(); ++it ){
-      TypeNode tn = it->first;
-      Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
-      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-      Trace("cegqi-si-rcons-stats") << it->second.size() << " terms to reconstruct of type " << dt.getName() << "." << std::endl;
-      Trace("cegqi-si-rcons") << it->second.size() << " terms to reconstruct of type " << dt.getName() << " : " << std::endl;
-      for( std::map< Node, bool >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
-        Trace("cegqi-si-rcons") << "  " << it2->first << std::endl;
-      }
-      Assert( !it->second.empty() );
-      rcons_tn.push_back( it->first );
+    d_sygus_solution = d_sol->reconstructSolution( s, stn, reconstructed );
+    if( reconstructed==1 ){
+      Trace("csi-sol") << "Solution (post-reconstruction into Sygus): " << d_sygus_solution << std::endl;
     }
-    bool success;
-    std::vector< TypeNode > incomplete;
-    unsigned index = 0;
-    do {
-      success = true;
-      std::vector< TypeNode > to_erase;
-      for( std::map< TypeNode, std::map< Node, bool > >::iterator it = d_rcons_to_process.begin(); it != d_rcons_to_process.end(); ++it ){
-        TypeNode stn = it->first;
-        if( it->second.empty() ){
-          to_erase.push_back( stn );
-        }else{
-          Node ns = d_qe->getTermDatabase()->getEnumerateTerm( stn, index );
-          if( ns.isNull() ){
-            to_erase.push_back( stn );
-            incomplete.push_back( stn );
-          }else{
-            Node nb = d_qe->getTermDatabaseSygus()->sygusToBuiltin( ns, stn );
-            Node nr = Rewriter::rewrite( nb );//d_qe->getTermDatabaseSygus()->getNormalized( stn, nb, false, false );
-            Trace("cegqi-si-rcons-debug2") << "  - try " << ns << " -> " << nr << " for " << stn << " " << nr.getKind() << std::endl;
-            if( it->second.find( nr )!=it->second.end() ){
-              Trace("cegqi-si-rcons") << "...reconstructed " << ns << " for term " << nr << std::endl;
-              d_reconstructed[nr][stn] = ns;
-              d_reconstructed_op[nr][stn] = false;
-              Assert( d_rewrite_to_rcons.find( nr )!=d_rewrite_to_rcons.end() );
-              Node nrr = d_rewrite_to_rcons[nr];
-              setReconstructed( nrr, stn );
-            }else{
-              /*
-              // look if it has a kind of a term that we need to reconstruct TODO
-              Kind nrk = nr.getKind();
-              std::map< Kind, std::map< Node, bool > >::iterator itk = d_rcons_kinds_to_process[stn].find( nrk );
-              if( itk!=d_rcons_kinds_to_process[stn].end() ){
-                Trace("cegqi-si-rcons") << "Term " << ns << " -> " << nr << " did not match, but has same operator " << nrk;
-                Trace("cegqi-si-rcons") << " as " << itk->second.size() << " waiting terms." << std::endl;
-                Assert( !itk->second.empty() );
-                for( std::map< Node, bool >::iterator itkn = itk->second.begin(); itkn != itk->second.end(); ++itkn ){
-
-                }
-              }
-              */
-            }
-            success = false;
-          }
-        }
-      }
-      for( unsigned i=0; i<to_erase.size(); i++ ){
-        Trace("cegqi-si-rcons-stats") << "......reconstructed all terms for type " << to_erase[i] << std::endl;
-        d_rcons_to_process.erase( to_erase[i] );
-      }
-      index++;
-      if( index%100==0 ){
-        Trace("cegqi-si-rcons-stats") << "Tried " << index << " for each type."  << std::endl;
-      }
-      if( success ){
-        if( incomplete.empty() ){
-          reconstructed = 1;
-          Trace("cegqi-si-debug-sol") << "Reconstructing sygus solution..." << std::endl;
-          d_sygus_solution = getReconstructedSolution( d_qe->getTermDatabaseSygus(), stn, d_templ_solution );
-          Trace("cegqi-si-debug-sol") << "Sygus solution is : " << d_sygus_solution << std::endl;
-        }
-      }
-    }while( !success );
   }
-  if( Trace.isOn("cegqi-si-debug-sol") ){
+
+
+  if( Trace.isOn("csi-sol") ){
     //debug solution
-    if( !debugSolution( d_solution ) ){
-      Trace("cegqi-si-debug-sol") << "WARNING : solution " << d_solution << " contains free constants." << std::endl;
+    if( !d_sol->debugSolution( d_solution ) ){
+      Trace("csi-sol") << "WARNING : solution " << d_solution << " contains free constants." << std::endl;
       //exit( 47 );
     }else{
       //exit( 49 );
     }
   }
   if( Trace.isOn("cegqi-stats") ){
-    int t_size = 0;
-    int num_ite = 0;
-    debugTermSize( d_orig_solution, t_size, num_ite );
-    //Trace("cegqi-stats") << "size " << t_size << " #ite " << num_ite << std::endl;
-    Trace("cegqi-stats") << t_size << " " << num_ite << " ";
-    t_size = 0;
-    num_ite = 0;
-    debugTermSize( d_solution, t_size, num_ite );
-    //Trace("cegqi-stats") << "simplified size " << t_size << " #ite " << num_ite << std::endl;
-    Trace("cegqi-stats") << t_size << " " << num_ite << " ";
-    t_size = 0;
-    num_ite = 0;
-    debugTermSize( d_templ_solution, t_size, num_ite );
-    //Trace("cegqi-stats") << "sygus size " << t_size << " #ite " << num_ite << std::endl;
-    Trace("cegqi-stats") << t_size << " " << num_ite << std::endl;
+    int tsize, itesize;
+    tsize = 0;itesize = 0;
+    d_sol->debugTermSize( d_orig_solution, tsize, itesize );
+    Trace("cegqi-stats") << tsize << " " << itesize << " ";
+    tsize = 0;itesize = 0;
+    d_sol->debugTermSize( d_solution, tsize, itesize );
+    Trace("cegqi-stats") << tsize << " " << itesize << " ";
+    if( !d_sygus_solution.isNull() ){
+      tsize = 0;itesize = 0;
+      d_sol->debugTermSize( d_sygus_solution, tsize, itesize );
+      Trace("cegqi-stats") << tsize << " - ";
+    }else{
+      Trace("cegqi-stats") << "null ";
+    }
+    Trace("cegqi-stats") << std::endl;
   }
   if( reconstructed==1 ){
     return d_sygus_solution;
@@ -852,727 +760,4 @@ Node CegConjectureSingleInv::getSolution( unsigned i, TypeNode stn, int& reconst
   }
 }
 
-bool CegConjectureSingleInv::debugSolution( Node sol ) {
-  if( sol.getKind()==SKOLEM ){
-    return false;
-  }else{
-    for( unsigned i=0; i<sol.getNumChildren(); i++ ){
-      if( !debugSolution( sol[i] ) ){
-        return false;
-      }
-    }
-    return true;
-  }
-
-}
-
-void CegConjectureSingleInv::debugTermSize( Node sol, int& t_size, int& num_ite ) {
-  t_size++;
-  if( sol.getKind()==ITE ){
-    num_ite++;
-  }
-  for( unsigned i=0; i<sol.getNumChildren(); i++ ){
-    debugTermSize( sol[i], t_size, num_ite );
-  }
-}
-
-Node CegConjectureSingleInv::pullITEs( Node s ) {
-  if( s.getKind()==ITE ){
-    bool success;
-    do {
-      success = false;
-      std::vector< Node > conj;
-      Node t;
-      Node rem;
-      if( pullITECondition( s, s, conj, t, rem, 0 ) ){
-        Assert( !conj.empty() );
-        Node cond = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj );
-        Trace("cegqi-si-debug-sol") << "For " << s << ", can pull " << cond << " -> " << t << " with remainder " << rem << std::endl;
-        t = pullITEs( t );
-        rem = pullITEs( rem );
-        s = NodeManager::currentNM()->mkNode( ITE, simpleNegate( cond ), t, rem );
-        //Trace("cegqi-si-debug-sol") << "Now : " << s << std::endl;
-        success = true;
-      }
-    }while( success );
-  }
-  return s;
-}
-
-// pull condition common to all ITE conditions in path of size > 1
-bool CegConjectureSingleInv::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;
-  bool isAnd;
-  if( n_ite[0].getKind()==AND || n_ite[0].getKind()==OR ){
-    isAnd = n_ite[0].getKind()==AND;
-    for( unsigned i=0; i<n_ite[0].getNumChildren(); i++ ){
-      Node cond = n_ite[0][i];
-      if( n_ite[0].getKind()==OR ){
-        cond = simpleNegate( cond );
-      }
-      curr_conj.push_back( cond );
-    }
-  }else{
-    Node neg = n_ite[0].negate();
-    if( std::find( conj.begin(), conj.end(), neg )!=conj.end() ){
-      isAnd = false;
-      curr_conj.push_back( neg );
-    }else{
-      isAnd = true;
-      curr_conj.push_back( n_ite[0] );
-    }
-  }
-  // take intersection with current conditions
-  std::vector< Node > new_conj;
-  std::vector< Node > prev_conj;
-  if( n_ite==root ){
-    new_conj.insert( new_conj.end(), curr_conj.begin(), curr_conj.end() );
-    Trace("cegqi-pull-ite") << "Pull ITE root " << n_ite << ", #conj = " << new_conj.size() << std::endl;
-  }else{
-    for( unsigned i=0; i<curr_conj.size(); i++ ){
-      if( std::find( conj.begin(), conj.end(), curr_conj[i] )!=conj.end() ){
-        new_conj.push_back( curr_conj[i] );
-      }
-    }
-    Trace("cegqi-pull-ite") << "Pull ITE " << n_ite << ", #conj = " << conj.size() << " intersect " << curr_conj.size() << " = " << new_conj.size() << std::endl;
-  }
-  //cannot go further
-  if( new_conj.empty() ){
-    return false;
-  }
-  //it is an intersection with current
-  conj.clear();
-  conj.insert( conj.end(), new_conj.begin(), new_conj.end() );
-  //recurse if possible
-  Node trec = n_ite[ isAnd ? 2 : 1 ];
-  Node tval = n_ite[ isAnd ? 1 : 2 ];
-  bool success = false;
-  if( trec.getKind()==ITE ){
-    prev_conj.insert( prev_conj.end(), conj.begin(), conj.end() );
-    success = pullITECondition( root, trec, conj, t, rem, depth+1 );
-  }
-  if( !success && depth>0 ){
-    t = trec;
-    rem = trec;
-    success = true;
-    if( trec.getKind()==ITE ){
-      //restore previous state
-      conj.clear();
-      conj.insert( conj.end(), prev_conj.begin(), prev_conj.end() );
-    }
-  }
-  if( success ){
-    //make remainder : strip out conditions in conj
-    Assert( !conj.empty() );
-    std::vector< Node > cond_c;
-    for( unsigned i=0; i<curr_conj.size(); i++ ){
-      if( std::find( conj.begin(), conj.end(), curr_conj[i] )==conj.end() ){
-        cond_c.push_back( curr_conj[i] );
-      }
-    }
-    if( cond_c.empty() ){
-      rem = isAnd ? tval : rem;
-    }else{
-      Node new_cond = cond_c.size()==1 ? cond_c[0] : NodeManager::currentNM()->mkNode( n_ite[0].getKind(), cond_c );
-      rem = NodeManager::currentNM()->mkNode( ITE, new_cond, isAnd ? tval : rem, isAnd ? rem : tval );
-    }
-    return true;
-  }else{
-    return false;
-  }
-}
-
-Node CegConjectureSingleInv::flattenITEs( Node n, bool rec ) {
-  Assert( !n.isNull() );
-  if( n.getKind()==ITE ){
-    Trace("csi-simp-debug") << "Flatten ITE : " << n << std::endl;
-    Node ret;
-    Node n0 = rec ? flattenITEs( n[0] ) : n[0];
-    Node n1 = rec ? flattenITEs( n[1] ) : n[1];
-    Node n2 = rec ? flattenITEs( n[2] ) : n[2];
-    Assert( !n0.isNull() );
-    Assert( !n1.isNull() );
-    Assert( !n2.isNull() );
-    if( n0.getKind()==NOT ){
-      ret = NodeManager::currentNM()->mkNode( ITE, n0[0], n2, n1 );
-    }else if( n0.getKind()==AND || n0.getKind()==OR ){
-      std::vector< Node > children;
-      for( unsigned i=1; i<n0.getNumChildren(); i++ ){
-        children.push_back( n0[i] );
-      }
-      Node rem = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( n0.getKind(), children );
-      if( n0.getKind()==AND ){
-        ret = NodeManager::currentNM()->mkNode( ITE, rem, NodeManager::currentNM()->mkNode( ITE, n0[0], n1, n2 ), n2 );
-      }else{
-        ret = NodeManager::currentNM()->mkNode( ITE, rem, n1, NodeManager::currentNM()->mkNode( ITE, n0[0], n1, n2 ) );
-      }
-    }else{
-      if( n0.getKind()==ITE ){
-        n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ),
-                                                   NodeManager::currentNM()->mkNode( AND, n0.negate(), n2 ) );
-      }else if( n0.getKind()==IFF ){
-        n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ),
-                                                   NodeManager::currentNM()->mkNode( AND, n0.negate(), n1.negate() ) );
-      }else{
-        return NodeManager::currentNM()->mkNode( ITE, n0, n1, n2 );
-      }
-      ret = NodeManager::currentNM()->mkNode( ITE, n0, n1, n2 );
-    }
-    Assert( !ret.isNull() );
-    return flattenITEs( ret, false );
-  }else{
-    if( n.getNumChildren()>0 ){
-      std::vector< Node > children;
-      if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-        children.push_back( n.getOperator() );
-      }
-      bool childChanged = false;
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        Node nc = flattenITEs( n[i] );
-        children.push_back( nc );
-        childChanged = childChanged || nc!=n[i];
-      }
-      if( !childChanged ){
-        return n;
-      }else{
-        return NodeManager::currentNM()->mkNode( n.getKind(), children );
-      }
-    }else{
-      return n;
-    }
-  }
-}
-
-// assign is from literals to booleans
-// union_find is from args to values
-
-bool CegConjectureSingleInv::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::vector< Node >& args ) {
-  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;
-    return pol==ita->second;
-  }else if( n.isConst() ){
-    return pol==(n==d_qe->getTermDatabase()->d_true);
-  }else{
-    Trace("csi-simp-debug") << "---assign " << n << " " << pol << std::endl;
-    assign[n] = pol;
-    new_assign.push_back( n );
-    if( ( pol && n.getKind()==AND ) || ( !pol && n.getKind()==OR ) ){
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        if( !getAssign( pol, n[i], assign, new_assign, vars, new_vars, new_subs, args ) ){
-          return false;
-        }
-      }
-    }else if( n.getKind()==NOT ){
-      return getAssign( !pol, n[0], assign, new_assign, vars, new_vars, new_subs, args );
-    }else if( pol && ( n.getKind()==IFF || n.getKind()==EQUAL ) ){
-      getAssignEquality( n, vars, new_vars, new_subs, args );
-    }
-  }
-  return true;
-}
-
-bool CegConjectureSingleInv::getAssignEquality( Node eq, std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs, std::vector< Node >& args ) {
-  Assert( eq.getKind()==IFF || eq.getKind()==EQUAL );
-  //try to find valid argument
-  for( unsigned r=0; r<2; r++ ){
-    if( std::find( args.begin(), args.end(), eq[r] )!=args.end() ){
-      Assert( std::find( vars.begin(), vars.end(), eq[r] )==vars.end() );
-      if( std::find( new_vars.begin(), new_vars.end(), eq[r] )==new_vars.end() ){
-        Node eqro = eq[r==0 ? 1 : 0 ];
-        if( !d_qe->getTermDatabase()->containsTerm( eqro, eq[r] ) ){
-          Trace("csi-simp-debug") << "---equality " << eq[r] << " = " << eqro << std::endl;
-          new_vars.push_back( eq[r] );
-          new_subs.push_back( eqro );
-          return true;
-        }
-      }
-    }
-  }
-  /*
-  TypeNode tn = eq[0].getType();
-  if( tn.isInteger() || tn.isReal() ){
-    std::map< Node, Node > msum;
-    if( QuantArith::getMonomialSumLit( eq, msum ) ){
-
-    }
-  }
-  */
-  return false;
-}
-
-Node CegConjectureSingleInv::simplifySolution( Node sol, std::map< Node, bool >& assign,
-                                               std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& args, int status ) {
-  Assert( vars.size()==subs.size() );
-  std::map< Node, bool >::iterator ita = assign.find( sol );
-  if( ita!=assign.end() ){
-    return NodeManager::currentNM()->mkConst( ita->second );
-  }else{
-    if( sol.getKind()==ITE ){
-      Trace("csi-simp") << "Simplify ITE " << std::endl;
-      std::vector< Node > children;
-      for( unsigned r=1; r<=2; r++ ){
-        std::vector< Node > new_assign;
-        std::vector< Node > new_vars;
-        std::vector< Node > new_subs;
-        if( getAssign( r==1, sol[0], assign, new_assign, vars, new_vars, new_subs, args ) ){
-          Trace("csi-simp") << "- branch " << r << " led to " << new_assign.size() << " assignments, " << new_vars.size() << " equalities." << std::endl;
-          unsigned prev_size = vars.size();
-          Node nc = sol[r];
-          if( !new_vars.empty() ){
-            nc = nc.substitute( new_vars.begin(), new_vars.end(), new_subs.begin(), new_subs.end() );
-            vars.insert( vars.end(), new_vars.begin(), new_vars.end() );
-            subs.insert( subs.end(), new_subs.begin(), new_subs.end() );
-          }
-          nc = simplifySolution( nc, assign, vars, subs, args, 0 );
-          children.push_back( nc );
-          //clean up substitution
-          if( !new_vars.empty() ){
-            vars.resize( prev_size );
-            subs.resize( prev_size );
-          }
-        }else{
-          Trace("csi-simp") << "- branch " << r << " of " << sol[0] << " is infeasible." << std::endl;
-        }
-        //clean up assignment
-        for( unsigned i=0; i<new_assign.size(); i++ ){
-          assign.erase( new_assign[i] );
-        }
-      }
-      if( children.size()==1 || ( children.size()==2 && children[0]==children[1] ) ){
-        return children[0];
-      }else{
-        Assert( children.size()==2 );
-        Node ncond = simplifySolution( sol[0], assign, vars, subs, args, 0 );
-        return NodeManager::currentNM()->mkNode( ITE, ncond, children[0], children[1] );
-      }
-    }else if( sol.getKind()==OR || sol.getKind()==AND ){
-      Trace("csi-simp") << "Simplify " << sol.getKind() << std::endl;
-      //collect new equalities
-      std::map< Node, bool > atoms;
-      std::vector< Node > inc;
-      std::vector< Node > children;
-      std::vector< Node > new_vars;
-      std::vector< Node > new_subs;
-      Node bc = sol.getKind()==OR ? d_qe->getTermDatabase()->d_true : d_qe->getTermDatabase()->d_false;
-      for( unsigned i=0; i<sol.getNumChildren(); i++ ){
-        bool do_exc = false;
-        Node c = sol[i];
-        Trace("csi-simp") << "  - child " << i << " : " << c << std::endl;
-        if( c.isConst() ){
-          if( c==bc ){
-            Trace("csi-simp") << "  ...singularity." << std::endl;
-            return bc;
-          }else{
-            do_exc = true;
-          }
-        }else{
-          Node atom = c.getKind()==NOT ? c[0] : c;
-          bool pol = c.getKind()!=NOT;
-          std::map< Node, bool >::iterator it = atoms.find( atom );
-          if( it==atoms.end() ){
-            atoms[atom] = pol;
-            if( status==0 && ( atom.getKind()==IFF || atom.getKind()==EQUAL ) ){
-              if( pol==( sol.getKind()==AND ) ){
-                Trace("csi-simp") << "  ...equality." << std::endl;
-                if( getAssignEquality( atom, vars, new_vars, new_subs, args ) ){
-                  children.push_back( sol[i] );
-                  do_exc = true;
-                }
-              }
-            }
-          }else{
-            //repeated atom
-            if( it->second!=pol ){
-              return NodeManager::currentNM()->mkConst( sol.getKind()==OR );
-            }else{
-              do_exc = true;
-            }
-          }
-        }
-        if( !do_exc ){
-          inc.push_back( sol[i] );
-        }else{
-          Trace("csi-simp") << "  ...exclude." << std::endl;
-        }
-      }
-      if( !new_vars.empty() ){
-        if( !inc.empty() ){
-          Node ret = inc.size()==1 ? sol[0] : NodeManager::currentNM()->mkNode( sol.getKind(), inc );
-          Trace("csi-simp") << "Base return is : " << ret << std::endl;
-          // apply substitution
-          ret = ret.substitute( new_vars.begin(), new_vars.end(), new_subs.begin(), new_subs.end() );
-          ret = Rewriter::rewrite( ret );
-          Trace("csi-simp") << "After substitution : " << ret << std::endl;
-          unsigned prev_size = vars.size();
-          vars.insert( vars.end(), new_vars.begin(), new_vars.end() );
-          subs.insert( subs.end(), new_subs.begin(), new_subs.end() );
-          ret = simplifySolution( ret, assign, vars, subs, args, 1 );
-          //clean up substitution
-          if( !vars.empty() ){
-            vars.resize( prev_size );
-            subs.resize( prev_size );
-          }
-          //Trace("csi-simp") << "After simplification : " << ret << std::endl;
-          if( ret.getKind()==sol.getKind() ){
-            for( unsigned i=0; i<ret.getNumChildren(); i++ ){
-              children.push_back( ret[i] );
-            }
-          }else{
-            children.push_back( ret );
-          }
-        }
-      }else{
-        //recurse on children
-        for( unsigned i=0; i<inc.size(); i++ ){
-          Node retc = simplifySolution( inc[i], assign, vars, subs, args, 0 );
-          if( retc.isConst() ){
-            if( retc==bc ){
-              return bc;
-            }
-          }else{
-            children.push_back( retc );
-          }
-        }
-      }
-      // now, remove all equalities that are implied
-      std::vector< Node > final_children;
-      for( unsigned i=0; i<children.size(); i++ ){
-        bool red = false;
-        Node atom = children[i].getKind()==NOT ? children[i][0] : children[i];
-        bool pol = children[i].getKind()!=NOT;
-        if( status==0 && ( atom.getKind()==IFF || atom.getKind()==EQUAL ) ){
-          if( pol!=( sol.getKind()==AND ) ){
-            std::vector< Node > tmp_vars;
-            std::vector< Node > tmp_subs;
-            if( getAssignEquality( atom, vars, tmp_vars, tmp_subs, args ) ){
-              Trace("csi-simp-debug") << "Check if " << children[i] << " is redundant in " << sol << std::endl;
-              for( unsigned j=0; j<children.size(); j++ ){
-                if( j!=i && ( j>i || std::find( final_children.begin(), final_children.end(), children[j] )!=final_children.end() ) ){
-                  Node sj = children[j].substitute( tmp_vars.begin(), tmp_vars.end(), tmp_subs.begin(), tmp_subs.end() );
-                  sj = Rewriter::rewrite( sj );
-                  if( sj==d_qe->getTermDatabase()->d_true ){
-                    Trace("csi-simp") << "--- " << children[i].negate() << " is implied by " << children[j].negate() << std::endl;
-                    red = true;
-                    break;
-                  }
-                }
-              }
-            }
-          }
-        }
-        if( !red ){
-          final_children.push_back( children[i] );
-        }
-      }
-
-      return final_children.size()==0 ? NodeManager::currentNM()->mkConst( sol.getKind()==AND ) :
-             ( final_children.size()==1 ? final_children[0] : NodeManager::currentNM()->mkNode( sol.getKind(), final_children ) );
-    }else{
-      //generic simplification
-      std::vector< Node > children;
-      if( sol.getMetaKind() == kind::metakind::PARAMETERIZED ){
-        children.push_back( sol.getOperator() );
-      }
-      bool childChanged = false;
-      for( unsigned i=0; i<sol.getNumChildren(); i++ ){
-        Node nc = simplifySolution( sol[i], assign, vars, subs, args, 0 );
-        childChanged = childChanged || nc!=sol[i];
-        children.push_back( nc );
-      }
-      if( childChanged ){
-        return NodeManager::currentNM()->mkNode( sol.getKind(), children );
-      }
-    }
-    return sol;
-  }
-}
-
-//TODO : accumulate assignment to literals as we traverse ITE
-Node CegConjectureSingleInv::collectReconstructNodes( TermDbSygus * tds, Node t, TypeNode stn, int& status ) {
-  std::map< TypeNode, Node >::iterator it = d_rcons_processed[t].find( stn );
-  if( it==d_rcons_processed[t].end() ){
-    TypeNode tn = t.getType();
-    Assert( datatypes::DatatypesRewriter::isTypeDatatype( stn ) );
-    const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
-    Assert( dt.isSygus() );
-    Trace("cegqi-si-rcons-debug") << "Check reconstruct " << t << " type " << tn << ", sygus type " << dt.getName() << ", kind " << t.getKind() << std::endl;
-    tds->registerSygusType( stn );
-    Node ret;
-    std::vector< Node > children;
-    if( t.getMetaKind() == kind::metakind::PARAMETERIZED ){
-      children.push_back( t.getOperator() );
-    }
-    bool childChanged = false;
-    std::vector< Node > rcons_child;
-    std::vector< TypeNode > rcons_child_tn;
-    Node rcons;
-    bool rcons_op;
-    bool rcons_set = false;
-    Kind tk = t.getKind();
-    int karg = tds->getKindArg( stn, tk );
-    //preprocessing to fit syntax
-    Node orig_t = t;
-    if( t.getNumChildren()>0 ){
-      // first, do standard minimizations
-      t = tds->minimizeBuiltinTerm( t );
-      bool success = true;
-      while( karg==-1 && success ){
-        success = false;
-        Node new_t;
-        Kind dk;
-        if( tds->isAntisymmetric( tk, dk ) ){
-          if( tds->hasKind( stn, dk ) ){
-            new_t = NodeManager::currentNM()->mkNode( dk, t[1], t[0] );
-          }
-        }
-        if( new_t.isNull() ){
-          for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-            Node g = tds->getGenericBase( stn, i );
-            if( g.getKind()==t.getKind() ){
-              Trace("cegqi-si-rcons-debug") << "Possible match ? " << g << " " << t << " for " << dt[i].getName() << std::endl;
-              std::map< int, Node > sigma;
-              if( tds->getMatch( g, t, sigma ) ){
-                //we found an exact match
-                bool msuccess = true;
-                for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
-                  if( sigma[j].isNull() ){
-                    msuccess = false;
-                    break;
-                  }
-                }
-                if( msuccess ){
-                  std::map< TypeNode, int > var_count;
-                  new_t = tds->mkGeneric( dt, i, var_count, sigma );
-                  Trace("cegqi-si-rcons-debug") << "Rewrote to : " << new_t << std::endl;
-                  break;
-                }
-              }
-            }
-          }
-          //expand things that have compact representations (these will not be found by enumeration if they aren't already in the syntax)
-          if( new_t.isNull() ){
-            if( t.getKind()==EQUAL && ( t[0].getType().isInteger() || t[0].getType().isReal() ) ){
-              new_t = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, t[0], t[1] ),
-                                                            NodeManager::currentNM()->mkNode( LEQ, t[1], t[0] ) );
-            }else if( t.getKind()==ITE ){
-              new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ),
-                                                            NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[2] ) );
-            }else if( t.getKind()==IFF ){
-              new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ),
-                                                            NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[1].negate() ) );
-            }else if( ( t.getKind()==OR || t.getKind()==AND ) && tds->hasKind( stn, NOT ) ){
-              new_t = simpleNegate( t ).negate();
-            }
-          }
-        }
-        if( !new_t.isNull() ){
-          t = new_t;
-          karg = tds->getKindArg( stn, t.getKind() );
-          success = true;
-          Trace("cegqi-si-rcons-debug") << "Try rewriting to " << new_t << ", now karg=" << karg << std::endl;
-        }
-      }
-    }
-    if( karg!=-1 ){
-      //flatten ITEs if necessary
-      if( t.getKind()==ITE ){
-        TypeNode cstn = tds->getArgType( dt[karg], 0 );
-        tds->registerSygusType( cstn );
-        Node prev_t;
-        while( !tds->hasKind( cstn, t[0].getKind() ) && t!=prev_t ){
-          prev_t = t;
-          Node exp_c = tds->expandBuiltinTerm( t[0] );
-          if( !exp_c.isNull() ){
-            t = NodeManager::currentNM()->mkNode( ITE, exp_c, t[1], t[2] );
-            Trace("cegqi-si-rcons-debug") << "Pre expand to " << t << std::endl;
-          }
-          t = flattenITEs( t, false );
-          if( t!=prev_t ){
-            Trace("cegqi-si-rcons-debug") << "Flatten ITE to " << t << std::endl;
-            std::map< Node, bool > sassign;
-            std::vector< Node > svars;
-            std::vector< Node > ssubs;
-            t = simplifySolution( t, sassign, svars, ssubs, d_varlist, 0 );
-          }
-          Assert( t.getKind()==ITE );
-        }
-      }
-      if( t.getNumChildren()==dt[karg].getNumArgs() ){
-        Trace("cegqi-si-rcons-debug") << "  Type has kind " << t.getKind() << ", recurse." << std::endl;
-        for( unsigned i=0; i<t.getNumChildren(); i++ ){
-          TypeNode cstn = tds->getArgType( dt[karg], i );
-          int status;
-          Node tc = collectReconstructNodes( tds, t[i], cstn, status );
-          if( status==1 ){
-            rcons_child.push_back( tc );
-            rcons_child_tn.push_back( cstn );
-          }
-          children.push_back( tc );
-          childChanged = childChanged || tc!=t[i];
-        }
-        rcons = Node::fromExpr( dt[karg].getConstructor() );
-        rcons_op = true;
-        rcons_set = true;
-      }else{
-        Trace("cegqi-si-rcons-debug") << "  Type has kind " << t.getKind() << ", but argument mismatch " << std::endl;
-        if( t.getNumChildren()>dt[karg].getNumArgs() && tds->isAssoc( t.getKind() ) && dt[karg].getNumArgs()==2 ){
-          // make n-ary applications into binary ones
-          TypeNode cstn = tds->getArgType( dt[karg], 0 );
-          int status;
-          Node t1 = collectReconstructNodes( tds, t[0], cstn, status );
-          children.push_back( t1 );
-          if( status==1 ){
-            rcons_child.push_back( t1 );
-            rcons_child_tn.push_back( cstn );
-          }
-          std::vector< Node > rem_children;
-          for( unsigned i=1; i<t.getNumChildren(); i++ ){
-            rem_children.push_back( t[i] );
-          }
-          Node t2 = NodeManager::currentNM()->mkNode( t.getKind(), rem_children );
-          cstn = tds->getArgType( dt[karg], 1 );
-          t2 = collectReconstructNodes( tds, t2, cstn, status );
-          children.push_back( t2 );
-          if( status==1 ){
-            rcons_child.push_back( t2 );
-            rcons_child_tn.push_back( cstn );
-          }
-          childChanged = true;
-          rcons = Node::fromExpr( dt[karg].getConstructor() );
-          rcons_op = true;
-          rcons_set = true;
-        }
-      }
-    }
-    if( !rcons_set ){
-      int carg = tds->getOpArg( stn, t );
-      if( carg==-1 ){
-        if( t.isConst() ){
-          ret = tds->builtinToSygusConst( t, stn );
-        }
-        if( ret.isNull() ){
-          Trace("cegqi-si-rcons") << "...Reconstruction needed for " << t << " sygus type " << dt.getName() << std::endl;
-        }
-      }else{
-        rcons = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, Node::fromExpr( dt[carg].getConstructor() ) );
-        rcons_op = false;
-        rcons_set = true;
-        Trace("cegqi-si-rcons-debug") << "  Type has constant." << std::endl;
-      }
-    }
-    if( ret.isNull() ){
-      if( !childChanged ){
-        ret = t;
-      }else{
-        ret = NodeManager::currentNM()->mkNode( t.getKind(), children );
-      }
-    }
-    // now, construct d_rcons_graph
-    for( unsigned i=0; i<rcons_child.size(); i++ ){
-      setNeedsReconstruction( rcons_child[i], rcons_child_tn[i], ret, stn );
-    }
-    status = !rcons_set || !d_rcons_graph[0][ret][stn].empty() ? 1 : 0;
-    if( rcons_set ){
-      d_reconstructed[ret][stn] = rcons;
-      d_reconstructed_op[ret][stn] = rcons_op;
-    }
-    d_rcons_processed[orig_t][stn] = ret;
-    d_rcons_processed_status[orig_t][stn] = status;
-    Trace("cegqi-si-rcons-debug") << "....return " << ret << " for " << orig_t << " in sygus type " << dt.getName() << ", status = " << status;
-    Trace("cegqi-si-rcons-debug") << ", rcons=" << rcons << ", rcons op : " << rcons_op << std::endl;
-    return ret;
-  }else{
-    status = d_rcons_processed_status[t][stn];
-    return it->second;
-  }
-}
-
-void CegConjectureSingleInv::setNeedsReconstruction( Node t, TypeNode stn, Node parent, TypeNode pstn ) {
-  Trace("cegqi-si-rcons-debug") << "Set reconstruction for " << t << " " << stn << " " << parent << " " << pstn << std::endl;
-  d_rcons_graph[0][parent][pstn][t][stn] = true;
-  if( !parent.isNull() ){
-    Node parentr = Rewriter::rewrite( parent );
-    d_rewrite_to_rcons[parentr] = parent;
-    d_rcons_to_rewrite[parent] = parentr;
-    d_rcons_to_process[pstn][parentr] = true;
-  }
-  d_rcons_graph[1][t][stn][parent][pstn] = true;
-  Node tr = Rewriter::rewrite( t );
-  d_rewrite_to_rcons[tr] = t;
-  d_rcons_to_rewrite[t] = tr;
-  d_rcons_to_process[stn][tr] = true;
-}
-
-void CegConjectureSingleInv::setReconstructed( Node t, TypeNode stn ) {
-  Assert( !t.isNull() );
-  if( Trace.isOn("cegqi-si-rcons-debug") ){
-    const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
-    Trace("cegqi-si-rcons-debug") << "set rcons : " << t << " in syntax " << dt.getName() << std::endl;
-  }
-  // clear all children, d_rcons_parents
-  std::vector< Node > to_set;
-  std::vector< TypeNode > to_set_tn;
-  for( unsigned r=0; r<2; r++){
-    unsigned ro = r==0 ? 1 : 0;
-    for( std::map< Node, std::map< TypeNode, bool > >::iterator it = d_rcons_graph[r][t][stn].begin(); it != d_rcons_graph[r][t][stn].end(); ++it ){
-      Node curr = it->first;
-      TypeNode stnc;
-      for( std::map< TypeNode, bool >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
-        stnc = it2->first;
-        d_rcons_graph[ro][curr][stnc][t].erase( stn );
-        if( d_rcons_graph[ro][curr][stnc][t].empty() ){
-          d_rcons_graph[ro][curr][stnc].erase( t );
-        }else{
-          Trace("cegqi-si-rcons-debug") << "  " << ( r==0 ? "child" : "parent" ) << " " << curr << " now has " << d_rcons_graph[ro][curr][stnc][t].size() << std::endl;
-        }
-      }
-      if( d_rcons_graph[ro][curr][stnc].empty() ){
-        if( !curr.isNull() ){
-          to_set.push_back( curr );
-          to_set_tn.push_back( stnc );
-        }
-      }
-    }
-  }
-  for( unsigned r=0; r<2; r++){
-    d_rcons_graph[r].erase( t );
-  }
-  d_rcons_to_process[stn].erase( d_rcons_to_rewrite[t] );
-  for( unsigned i=0; i<to_set.size(); i++ ){
-    setReconstructed( to_set[i], to_set_tn[i] );
-  }
-}
-
-Node CegConjectureSingleInv::getReconstructedSolution( TermDbSygus * tds, TypeNode stn, Node t ) {
-  std::map< TypeNode, Node >::iterator it = d_reconstructed[t].find( stn );
-  if( it!=d_reconstructed[t].end() ){
-    if( d_reconstructed_op[t][stn] ){
-      Assert( datatypes::DatatypesRewriter::isTypeDatatype( stn ) );
-      const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
-      Assert( dt.isSygus() );
-      std::vector< Node > children;
-      children.push_back( it->second );
-      int c = tds->getKindArg( stn, t.getKind() );
-      Assert( c!=-1 );
-      for( unsigned i=0; i<t.getNumChildren(); i++ ){
-        TypeNode stnc = tds->getArgType( dt[c], i );
-        Node nc = getReconstructedSolution( tds, stnc, t[i] );
-        children.push_back( nc );
-      }
-      return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
-    }else{
-      return it->second;
-    }
-  }else{
-    Trace("cegqi-si-rcons-debug") << "*** error : missing reconstruction for " << t << std::endl;
-    Assert( false );
-    return Node::null();
-  }
-}
-
-
-
 }
\ No newline at end of file
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index 85ba25a0f..4a9ed76fe 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -20,6 +20,7 @@
 #include "context/cdhashmap.h"
 #include "context/cdchunk_list.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/ce_guided_single_inv_sol.h"
 
 namespace CVC4 {
 namespace theory {
@@ -32,6 +33,7 @@ class CegConjectureSingleInv
 private:
   QuantifiersEngine * d_qe;
   CegConjecture * d_parent;
+  CegConjectureSingleInvSol * d_sol;
   bool analyzeSygusConjunct( Node n, Node p, std::map< Node, std::vector< Node > >& children,
                             std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke,
                             std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol );
@@ -44,7 +46,6 @@ private:
   int classifyTerm( Node n, std::map< Node, int >& subs_from_model );
   void collectProgVars( Node n, std::vector< Node >& vars );
   Node applyProgVarSubstitution( Node n, std::map< Node, int >& subs_from_model, std::vector< Node >& subs );
-
 public:
   CegConjectureSingleInv( QuantifiersEngine * qe, Node q, CegConjecture * p );
   // original conjecture
@@ -67,10 +68,9 @@ public:
   std::vector< Node > d_lemmas_produced;
   std::vector< std::vector< Node > > d_inst;
   // solution
-  std::vector< Node > d_varlist;
+  std::vector< Node > d_varList;
   Node d_orig_solution;
   Node d_solution;
-  Node d_templ_solution;
   Node d_sygus_solution;
 public:
   //get the single invocation lemma
@@ -80,38 +80,7 @@ public:
   //check
   void check( std::vector< Node >& lems );
   //get solution
-  Node getSolution( unsigned i, TypeNode stn, int& reconstructed );
-
-
-//solution simplification
-private:
-  bool debugSolution( Node sol );
-  void debugTermSize( Node sol, int& t_size, int& num_ite );
-  Node pullITEs( Node n );
-  bool pullITECondition( Node root, Node n, std::vector< Node >& conj, Node& t, Node& rem, int depth );
-  Node flattenITEs( Node n, bool rec = true );
-  Node simplifySolution( Node sol, std::map< Node, bool >& assign,
-                         std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& args, int status );
-  bool 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::vector< Node >& args );
-  bool getAssignEquality( Node eq, std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs, std::vector< Node >& args );
-//solution reconstruction
-private:
-  std::map< Node, std::map< TypeNode, Node > > d_rcons_processed;
-  std::map< Node, std::map< TypeNode, int > > d_rcons_processed_status;
-  std::map< Node, std::map< TypeNode, Node > > d_reconstructed;
-  std::map< Node, std::map< TypeNode, bool > > d_reconstructed_op;
-  std::map< Node, std::map< TypeNode, std::map< Node, std::map< TypeNode, bool > > > > d_rcons_graph[2];
-  std::map< TypeNode, std::map< Node, bool > > d_rcons_to_process;
-  std::map< Node, Node > d_rewrite_to_rcons;
-  std::map< Node, Node > d_rcons_to_rewrite;
-  // term t with sygus type st, returns inducted templated form of t
-  Node collectReconstructNodes( TermDbSygus * tds, Node t, TypeNode stn, int& status );
-  // set reconstructed
-  void setNeedsReconstruction( Node t, TypeNode stn, Node parent, TypeNode pstn );
-  void setReconstructed( Node tr, TypeNode stn );
-  // get solution
-  Node getReconstructedSolution( TermDbSygus * tds, TypeNode stn, Node t );
+  Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed );
 };
 
 }
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
new file mode 100644
index 000000000..02c4c3a28
--- /dev/null
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
@@ -0,0 +1,1006 @@
+/*********************                                                        */
+/*! \file ce_guided_single_inv.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief utility for processing single invocation synthesis conjectures
+ **
+ **/
+
+#include "theory/quantifiers/ce_guided_single_inv_sol.h"
+#include "theory/quantifiers/ce_guided_single_inv.h"
+#include "theory/quantifiers/ce_guided_instantiation.h"
+#include "theory/theory_engine.h"
+#include "theory/quantifiers/options.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/datatypes/datatypes_rewriter.h"
+#include "util/datatype.h"
+#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/trigger.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace std;
+
+namespace CVC4 {
+
+CegConjectureSingleInvSol::CegConjectureSingleInvSol( QuantifiersEngine * qe ) : d_qe( qe ){
+  d_id_count = 0;
+}
+
+bool CegConjectureSingleInvSol::debugSolution( Node sol ) {
+  if( sol.getKind()==SKOLEM ){
+    return false;
+  }else{
+    for( unsigned i=0; i<sol.getNumChildren(); i++ ){
+      if( !debugSolution( sol[i] ) ){
+        return false;
+      }
+    }
+    return true;
+  }
+
+}
+
+void CegConjectureSingleInvSol::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;
+    int prev_ite = num_ite;
+    t_size++;
+    if( sol.getKind()==ITE ){
+      num_ite++;
+    }
+    for( unsigned i=0; i<sol.getNumChildren(); i++ ){
+      debugTermSize( sol[i], t_size, num_ite );
+    }
+    d_dterm_size[sol] = t_size-prev;
+    d_dterm_ite_size[sol] = num_ite-prev_ite;
+  }else{
+    t_size += it->second;
+    num_ite += d_dterm_ite_size[sol];
+  }
+}
+
+
+Node CegConjectureSingleInvSol::pullITEs( Node s ) {
+  if( s.getKind()==ITE ){
+    bool success;
+    do {
+      success = false;
+      std::vector< Node > conj;
+      Node t;
+      Node rem;
+      if( pullITECondition( s, s, conj, t, rem, 0 ) ){
+        Assert( !conj.empty() );
+        Node cond = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj );
+        Trace("csi-sol-debug") << "For " << s << ", can pull " << cond << " -> " << t << " with remainder " << rem << std::endl;
+        t = pullITEs( t );
+        rem = pullITEs( rem );
+        s = NodeManager::currentNM()->mkNode( ITE, TermDb::simpleNegate( cond ), t, rem );
+        //Trace("csi-debug-sol") << "Now : " << s << std::endl;
+        success = true;
+      }
+    }while( success );
+  }
+  return 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 ) {
+  Assert( n_ite.getKind()==ITE );
+  std::vector< Node > curr_conj;
+  bool isAnd;
+  if( n_ite[0].getKind()==AND || n_ite[0].getKind()==OR ){
+    isAnd = n_ite[0].getKind()==AND;
+    for( unsigned i=0; i<n_ite[0].getNumChildren(); i++ ){
+      Node cond = n_ite[0][i];
+      if( n_ite[0].getKind()==OR ){
+        cond = TermDb::simpleNegate( cond );
+      }
+      curr_conj.push_back( cond );
+    }
+  }else{
+    Node neg = n_ite[0].negate();
+    if( std::find( conj.begin(), conj.end(), neg )!=conj.end() ){
+      isAnd = false;
+      curr_conj.push_back( neg );
+    }else{
+      isAnd = true;
+      curr_conj.push_back( n_ite[0] );
+    }
+  }
+  // take intersection with current conditions
+  std::vector< Node > new_conj;
+  std::vector< Node > prev_conj;
+  if( n_ite==root ){
+    new_conj.insert( new_conj.end(), curr_conj.begin(), curr_conj.end() );
+    Trace("csi-sol-debug") << "Pull ITE root " << n_ite << ", #conj = " << new_conj.size() << std::endl;
+  }else{
+    for( unsigned i=0; i<curr_conj.size(); i++ ){
+      if( std::find( conj.begin(), conj.end(), curr_conj[i] )!=conj.end() ){
+        new_conj.push_back( curr_conj[i] );
+      }
+    }
+    Trace("csi-sol-debug") << "Pull ITE " << n_ite << ", #conj = " << conj.size() << " intersect " << curr_conj.size() << " = " << new_conj.size() << std::endl;
+  }
+  //cannot go further
+  if( new_conj.empty() ){
+    return false;
+  }
+  //it is an intersection with current
+  conj.clear();
+  conj.insert( conj.end(), new_conj.begin(), new_conj.end() );
+  //recurse if possible
+  Node trec = n_ite[ isAnd ? 2 : 1 ];
+  Node tval = n_ite[ isAnd ? 1 : 2 ];
+  bool success = false;
+  if( trec.getKind()==ITE ){
+    prev_conj.insert( prev_conj.end(), conj.begin(), conj.end() );
+    success = pullITECondition( root, trec, conj, t, rem, depth+1 );
+  }
+  if( !success && depth>0 ){
+    t = trec;
+    rem = trec;
+    success = true;
+    if( trec.getKind()==ITE ){
+      //restore previous state
+      conj.clear();
+      conj.insert( conj.end(), prev_conj.begin(), prev_conj.end() );
+    }
+  }
+  if( success ){
+    //make remainder : strip out conditions in conj
+    Assert( !conj.empty() );
+    std::vector< Node > cond_c;
+    for( unsigned i=0; i<curr_conj.size(); i++ ){
+      if( std::find( conj.begin(), conj.end(), curr_conj[i] )==conj.end() ){
+        cond_c.push_back( curr_conj[i] );
+      }
+    }
+    if( cond_c.empty() ){
+      rem = isAnd ? tval : rem;
+    }else{
+      Node new_cond = cond_c.size()==1 ? cond_c[0] : NodeManager::currentNM()->mkNode( n_ite[0].getKind(), cond_c );
+      rem = NodeManager::currentNM()->mkNode( ITE, new_cond, isAnd ? tval : rem, isAnd ? rem : tval );
+    }
+    return true;
+  }else{
+    return false;
+  }
+}
+
+Node CegConjectureSingleInvSol::flattenITEs( Node n, bool rec ) {
+  Assert( !n.isNull() );
+  if( n.getKind()==ITE ){
+    Trace("csi-sol-debug") << "Flatten ITE." << std::endl;
+    Node ret;
+    Node n0 = rec ? flattenITEs( n[0] ) : n[0];
+    Node n1 = rec ? flattenITEs( n[1] ) : n[1];
+    Node n2 = rec ? flattenITEs( n[2] ) : n[2];
+    Assert( !n0.isNull() );
+    Assert( !n1.isNull() );
+    Assert( !n2.isNull() );
+    if( n0.getKind()==NOT ){
+      ret = NodeManager::currentNM()->mkNode( ITE, n0[0], n2, n1 );
+    }else if( n0.getKind()==AND || n0.getKind()==OR ){
+      std::vector< Node > children;
+      for( unsigned i=1; i<n0.getNumChildren(); i++ ){
+        children.push_back( n0[i] );
+      }
+      Node rem = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( n0.getKind(), children );
+      if( n0.getKind()==AND ){
+        ret = NodeManager::currentNM()->mkNode( ITE, rem, NodeManager::currentNM()->mkNode( ITE, n0[0], n1, n2 ), n2 );
+      }else{
+        ret = NodeManager::currentNM()->mkNode( ITE, rem, n1, NodeManager::currentNM()->mkNode( ITE, n0[0], n1, n2 ) );
+      }
+    }else{
+      if( n0.getKind()==ITE ){
+        n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ),
+                                                   NodeManager::currentNM()->mkNode( AND, n0.negate(), n2 ) );
+      }else if( n0.getKind()==IFF ){
+        n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ),
+                                                   NodeManager::currentNM()->mkNode( AND, n0.negate(), n1.negate() ) );
+      }else{
+        return NodeManager::currentNM()->mkNode( ITE, n0, n1, n2 );
+      }
+      ret = NodeManager::currentNM()->mkNode( ITE, n0, n1, n2 );
+    }
+    Assert( !ret.isNull() );
+    return flattenITEs( ret, false );
+  }else{
+    if( n.getNumChildren()>0 ){
+      std::vector< Node > children;
+      if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+        children.push_back( n.getOperator() );
+      }
+      bool childChanged = false;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        Node nc = flattenITEs( n[i] );
+        children.push_back( nc );
+        childChanged = childChanged || nc!=n[i];
+      }
+      if( !childChanged ){
+        return n;
+      }else{
+        return NodeManager::currentNM()->mkNode( n.getKind(), children );
+      }
+    }else{
+      return n;
+    }
+  }
+}
+
+// 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 ) {
+  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;
+    return pol==ita->second;
+  }else if( n.isConst() ){
+    return pol==(n==d_qe->getTermDatabase()->d_true);
+  }else{
+    Trace("csi-simp-debug") << "---assign " << n << " " << pol << std::endl;
+    assign[n] = pol;
+    new_assign.push_back( n );
+    if( ( pol && n.getKind()==AND ) || ( !pol && n.getKind()==OR ) ){
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        if( !getAssign( pol, n[i], assign, new_assign, vars, new_vars, new_subs ) ){
+          return false;
+        }
+      }
+    }else if( n.getKind()==NOT ){
+      return getAssign( !pol, n[0], assign, new_assign, vars, new_vars, new_subs );
+    }else if( pol && ( n.getKind()==IFF || n.getKind()==EQUAL ) ){
+      getAssignEquality( n, vars, new_vars, new_subs );
+    }
+  }
+  return true;
+}
+
+bool CegConjectureSingleInvSol::getAssignEquality( Node eq, std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs ) {
+  Assert( eq.getKind()==IFF || eq.getKind()==EQUAL );
+  //try to find valid argument
+  for( unsigned r=0; r<2; r++ ){
+    if( std::find( d_varList.begin(), d_varList.end(), eq[r] )!=d_varList.end() ){
+      Assert( std::find( vars.begin(), vars.end(), eq[r] )==vars.end() );
+      if( std::find( new_vars.begin(), new_vars.end(), eq[r] )==new_vars.end() ){
+        Node eqro = eq[r==0 ? 1 : 0 ];
+        if( !d_qe->getTermDatabase()->containsTerm( eqro, eq[r] ) ){
+          Trace("csi-simp-debug") << "---equality " << eq[r] << " = " << eqro << std::endl;
+          new_vars.push_back( eq[r] );
+          new_subs.push_back( eqro );
+          return true;
+        }
+      }
+    }
+  }
+  /*
+  TypeNode tn = eq[0].getType();
+  if( tn.isInteger() || tn.isReal() ){
+    std::map< Node, Node > msum;
+    if( QuantArith::getMonomialSumLit( eq, msum ) ){
+
+    }
+  }
+  */
+  return false;
+}
+
+Node CegConjectureSingleInvSol::simplifySolution( Node sol, TypeNode stn ){
+  int tsize, itesize;
+  if( Trace.isOn("csi-sol") ){
+    tsize = 0;itesize = 0;
+    debugTermSize( sol, tsize, itesize );
+    Trace("csi-sol") << tsize << " " << itesize << " rewrite..." << std::endl;
+    Trace("csi-sol-debug") << "sol : " << sol << "..." << std::endl;
+  }
+  Node sol0 = Rewriter::rewrite( sol );
+  Trace("csi-sol") << "now : " << sol0 << std::endl;
+  
+  Node curr_sol = sol0;
+  Node prev_sol;
+  do{
+    prev_sol = curr_sol;
+    //first, pull ITE conditions
+    if( Trace.isOn("csi-sol") ){
+      tsize = 0;itesize = 0;
+      debugTermSize( curr_sol, tsize, itesize );
+      Trace("csi-sol") << tsize << " " << itesize << " pull ITE..." << std::endl;
+      Trace("csi-sol-debug") << "sol : " << curr_sol << "..." << std::endl;
+    }
+    Node sol1 = pullITEs( curr_sol );
+    Trace("csi-sol") << "now : " << sol1 << std::endl;
+    //do standard rewriting
+    if( sol1!=curr_sol ){
+      if( Trace.isOn("csi-sol") ){
+        tsize = 0;itesize = 0;
+        debugTermSize( sol1, tsize, itesize );
+        Trace("csi-sol") << tsize << " " << itesize << " rewrite..." << std::endl;
+        Trace("csi-sol-debug") << "sol : " << sol1 << "..." << std::endl;
+      }
+      Node sol2 = Rewriter::rewrite( sol1 );
+      Trace("csi-sol") << "now : " << sol2 << std::endl;
+      curr_sol = sol2;
+    }
+    //now do branch analysis
+    if( Trace.isOn("csi-sol") ){
+      tsize = 0;itesize = 0;
+      debugTermSize( curr_sol, tsize, itesize );
+      Trace("csi-sol") << tsize << " " << itesize << " simplify solution..." << std::endl;
+      Trace("csi-sol-debug") << "sol : " << curr_sol << "..." << std::endl;
+    }
+    std::map< Node, bool > sassign;
+    std::vector< Node > svars;
+    std::vector< Node > ssubs;
+    Node sol3 = simplifySolutionNode( curr_sol, stn, sassign, svars, ssubs, 0 );
+    Trace("csi-sol") << "now : " << sol3 << std::endl;
+    if( sol3!=curr_sol ){
+      //do standard rewriting again
+      if( Trace.isOn("csi-sol" ) ){
+        tsize = 0;itesize = 0;
+        debugTermSize( sol3, tsize, itesize );
+        Trace("csi-sol") << tsize << " " << itesize << " rewrite..." << std::endl;
+      }
+      Node sol4 = Rewriter::rewrite( sol3 );
+      Trace("csi-sol") << "now : " << sol4 << std::endl;
+      curr_sol = sol4;
+    }
+  }while( curr_sol!=prev_sol );
+  
+  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 ) {
+
+  Assert( vars.size()==subs.size() );
+  std::map< Node, bool >::iterator ita = assign.find( sol );
+  if( ita!=assign.end() ){
+    //it is currently assigned a boolean value
+    return NodeManager::currentNM()->mkConst( ita->second );
+  }else{
+    d_qe->getTermDatabaseSygus()->registerSygusType( stn );
+    std::map< int, TypeNode > stnc;
+    if( !stn.isNull() ){
+      int karg = d_qe->getTermDatabaseSygus()->getKindArg( stn, sol.getKind() );
+      if( karg!=-1 ){
+        const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
+        if( dt[karg].getNumArgs()==sol.getNumChildren() ){
+          for( unsigned i=0; i<dt[karg].getNumArgs(); i++ ){
+            stnc[i] = d_qe->getTermDatabaseSygus()->getArgType( dt[karg], i );
+          }
+        }
+      }
+    }
+
+    if( sol.getKind()==ITE ){
+      Trace("csi-simp") << "Simplify ITE " << std::endl;
+      std::vector< Node > children;
+      for( unsigned r=1; r<=2; r++ ){
+        std::vector< Node > new_assign;
+        std::vector< Node > new_vars;
+        std::vector< Node > new_subs;
+        if( getAssign( r==1, sol[0], assign, new_assign, vars, new_vars, new_subs ) ){
+          Trace("csi-simp") << "- branch " << r << " led to " << new_assign.size() << " assignments, " << new_vars.size() << " equalities." << std::endl;
+          unsigned prev_size = vars.size();
+          Node nc = sol[r];
+          if( !new_vars.empty() ){
+            nc = nc.substitute( new_vars.begin(), new_vars.end(), new_subs.begin(), new_subs.end() );
+            vars.insert( vars.end(), new_vars.begin(), new_vars.end() );
+            subs.insert( subs.end(), new_subs.begin(), new_subs.end() );
+          }
+          nc = simplifySolutionNode( nc, stnc[r], assign, vars, subs, 0 );
+          children.push_back( nc );
+          //clean up substitution
+          if( !new_vars.empty() ){
+            vars.resize( prev_size );
+            subs.resize( prev_size );
+          }
+        }else{
+          Trace("csi-simp") << "- branch " << r << " of " << sol[0] << " is infeasible." << std::endl;
+        }
+        //clean up assignment
+        for( unsigned i=0; i<new_assign.size(); i++ ){
+          assign.erase( new_assign[i] );
+        }
+      }
+      if( children.size()==1 || ( children.size()==2 && children[0]==children[1] ) ){
+        return children[0];
+      }else{
+        Assert( children.size()==2 );
+        Node ncond = simplifySolutionNode( sol[0], stnc[0], assign, vars, subs, 0 );
+        Node ret = NodeManager::currentNM()->mkNode( ITE, ncond, children[0], children[1] );
+
+        //expand/flatten if necessary
+        Node orig_ret = ret;
+        if( !stnc[0].isNull() ){
+          d_qe->getTermDatabaseSygus()->registerSygusType( stnc[0] );
+          Node prev_ret;
+          while( !d_qe->getTermDatabaseSygus()->hasKind( stnc[0], ret[0].getKind() ) && ret!=prev_ret ){
+            prev_ret = ret;
+            Node exp_c = d_qe->getTermDatabaseSygus()->expandBuiltinTerm( ret[0] );
+            if( !exp_c.isNull() ){
+              Trace("csi-simp-debug") << "Pre expand to " << ret[0] << " to " << exp_c << std::endl;
+              ret = NodeManager::currentNM()->mkNode( ITE, exp_c, ret[1], ret[2] );
+            }
+            if( !d_qe->getTermDatabaseSygus()->hasKind( stnc[0], ret[0].getKind() ) ){
+              Trace("csi-sol") << "Flatten based on " << ret[0] << "." << std::endl;
+              ret = flattenITEs( ret, false );
+            }
+          }
+        }
+        return ret;
+        /*
+        if( orig_ret!=ret ){
+          Trace("csi-simp") << "Try expanded ITE" << std::endl;
+          return ret;//simplifySolutionNode( ret, stn, assign, vars, subs, status );
+        }else{
+          return ret;
+        }
+        */
+      }
+    }else if( sol.getKind()==OR || sol.getKind()==AND ){
+      Trace("csi-simp") << "Simplify " << sol.getKind() << std::endl;
+      //collect new equalities
+      std::map< Node, bool > atoms;
+      std::vector< Node > inc;
+      std::vector< Node > children;
+      std::vector< Node > new_vars;
+      std::vector< Node > new_subs;
+      Node bc = sol.getKind()==OR ? d_qe->getTermDatabase()->d_true : d_qe->getTermDatabase()->d_false;
+      for( unsigned i=0; i<sol.getNumChildren(); i++ ){
+        bool do_exc = false;
+        Node c;
+        std::map< Node, bool >::iterator ita = assign.find( sol[i] );
+        if( ita==assign.end() ){
+          c = sol[i];
+        }else{
+          c = NodeManager::currentNM()->mkConst( ita->second );
+        }
+        Trace("csi-simp") << "  - child " << i << " : " << c << std::endl;
+        if( c.isConst() ){
+          if( c==bc ){
+            Trace("csi-simp") << "  ...singularity." << std::endl;
+            return bc;
+          }else{
+            do_exc = true;
+          }
+        }else{
+          Node atom = c.getKind()==NOT ? c[0] : c;
+          bool pol = c.getKind()!=NOT;
+          std::map< Node, bool >::iterator it = atoms.find( atom );
+          if( it==atoms.end() ){
+            atoms[atom] = pol;
+            if( status==0 && ( atom.getKind()==IFF || atom.getKind()==EQUAL ) ){
+              if( pol==( sol.getKind()==AND ) ){
+                Trace("csi-simp") << "  ...equality." << std::endl;
+                if( getAssignEquality( atom, vars, new_vars, new_subs ) ){
+                  children.push_back( sol[i] );
+                  do_exc = true;
+                }
+              }
+            }
+          }else{
+            //repeated atom
+            if( it->second!=pol ){
+              return NodeManager::currentNM()->mkConst( sol.getKind()==OR );
+            }else{
+              do_exc = true;
+            }
+          }
+        }
+        if( !do_exc ){
+          inc.push_back( sol[i] );
+        }else{
+          Trace("csi-simp") << "  ...exclude." << std::endl;
+        }
+      }
+      if( !new_vars.empty() ){
+        if( !inc.empty() ){
+          Node ret = inc.size()==1 ? sol[0] : NodeManager::currentNM()->mkNode( sol.getKind(), inc );
+          Trace("csi-simp") << "Base return is : " << ret << std::endl;
+          // apply substitution
+          ret = ret.substitute( new_vars.begin(), new_vars.end(), new_subs.begin(), new_subs.end() );
+          ret = Rewriter::rewrite( ret );
+          Trace("csi-simp") << "After substitution : " << ret << std::endl;
+          unsigned prev_size = vars.size();
+          vars.insert( vars.end(), new_vars.begin(), new_vars.end() );
+          subs.insert( subs.end(), new_subs.begin(), new_subs.end() );
+          ret = simplifySolutionNode( ret, TypeNode::null(), assign, vars, subs, 1 );
+          //clean up substitution
+          if( !vars.empty() ){
+            vars.resize( prev_size );
+            subs.resize( prev_size );
+          }
+          //Trace("csi-simp") << "After simplification : " << ret << std::endl;
+          if( ret.isConst() ){
+            if( ret==bc ){
+              return bc;
+            }
+          }else{
+            if( ret.getKind()==sol.getKind() ){
+              for( unsigned i=0; i<ret.getNumChildren(); i++ ){
+                children.push_back( ret[i] );
+              }
+            }else{
+              children.push_back( ret );
+            }
+          }
+        }
+      }else{
+        //recurse on children
+        for( unsigned i=0; i<inc.size(); i++ ){
+          Node retc = simplifySolutionNode( inc[i], TypeNode::null(), assign, vars, subs, 0 );
+          if( retc.isConst() ){
+            if( retc==bc ){
+              return bc;
+            }
+          }else{
+            children.push_back( retc );
+          }
+        }
+      }
+      // now, remove all equalities that are implied
+      std::vector< Node > final_children;
+      for( unsigned i=0; i<children.size(); i++ ){
+        bool red = false;
+        Node atom = children[i].getKind()==NOT ? children[i][0] : children[i];
+        bool pol = children[i].getKind()!=NOT;
+        if( status==0 && ( atom.getKind()==IFF || atom.getKind()==EQUAL ) ){
+          if( pol!=( sol.getKind()==AND ) ){
+            std::vector< Node > tmp_vars;
+            std::vector< Node > tmp_subs;
+            if( getAssignEquality( atom, vars, tmp_vars, tmp_subs ) ){
+              Trace("csi-simp-debug") << "Check if " << children[i] << " is redundant in " << sol << std::endl;
+              for( unsigned j=0; j<children.size(); j++ ){
+                if( j!=i && ( j>i || std::find( final_children.begin(), final_children.end(), children[j] )!=final_children.end() ) ){
+                  Node sj = children[j].substitute( tmp_vars.begin(), tmp_vars.end(), tmp_subs.begin(), tmp_subs.end() );
+                  sj = Rewriter::rewrite( sj );
+                  if( sj==( sol.getKind()==AND ? d_qe->getTermDatabase()->d_false : d_qe->getTermDatabase()->d_true ) ){
+                    Trace("csi-simp") << "--- " << children[i].negate() << " is implied by " << children[j].negate() << std::endl;
+                    red = true;
+                    break;
+                  }
+                }
+              }
+              if( !red ){
+                Trace("csi-simp-debug") << "...is not." << std::endl;
+              }
+            }
+          }
+        }
+        if( !red ){
+          final_children.push_back( children[i] );
+        }
+      }
+      return final_children.size()==0 ? NodeManager::currentNM()->mkConst( sol.getKind()==AND ) :
+             ( final_children.size()==1 ? final_children[0] : NodeManager::currentNM()->mkNode( sol.getKind(), final_children ) );
+    }else{
+      //generic simplification
+      std::vector< Node > children;
+      if( sol.getMetaKind() == kind::metakind::PARAMETERIZED ){
+        children.push_back( sol.getOperator() );
+      }
+      bool childChanged = false;
+      for( unsigned i=0; i<sol.getNumChildren(); i++ ){
+        Node nc = simplifySolutionNode( sol[i], stnc[i], assign, vars, subs, 0 );
+        childChanged = childChanged || nc!=sol[i];
+        children.push_back( nc );
+      }
+      if( childChanged ){
+        return NodeManager::currentNM()->mkNode( sol.getKind(), children );
+      }
+    }
+    return sol;
+  }
+}
+
+
+
+
+
+
+Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int& reconstructed ) {
+  Trace("csi-rcons") << "Solution (pre-reconstruction) is : " << sol << std::endl;
+  int status;
+  d_root_id = collectReconstructNodes( sol, stn, status );
+  if( status==0 ){
+    Node ret = getReconstructedSolution( d_root_id );
+    Trace("csi-rcons") << "Sygus solution is : " << ret << std::endl;
+    Assert( !ret.isNull() );
+    reconstructed = 1;
+    return ret;
+  }else{
+    //Trace("csi-debug-sol") << "Induced solution template is : " << d_templ_solution << std::endl;
+    if( Trace.isOn("csi-rcons") ){
+      for( std::map< TypeNode, std::map< Node, int > >::iterator it = d_rcons_to_id.begin(); it != d_rcons_to_id.end(); ++it ){
+        TypeNode tn = it->first;
+        Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
+        const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+        Trace("csi-rcons") << "Terms to reconstruct of type " << dt.getName() << " : " << std::endl;
+        for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+          if( d_reconstruct.find( it2->second )==d_reconstruct.end() ){
+            Trace("csi-rcons") << "  " << it2->first << std::endl;
+          }
+        }
+        Assert( !it->second.empty() );
+      }
+    }
+    unsigned index = 0;
+    std::map< TypeNode, bool > active;
+    for( std::map< TypeNode, std::map< Node, int > >::iterator it = d_rcons_to_id.begin(); it != d_rcons_to_id.end(); ++it ){
+      active[it->first] = true;
+    }
+    //enumerate for all types
+    do {
+      std::vector< TypeNode > to_erase;
+      for( std::map< TypeNode, bool >::iterator it = active.begin(); it != active.end(); ++it ){
+        TypeNode stn = it->first;
+        Node ns = d_qe->getTermDatabase()->getEnumerateTerm( stn, index );
+        if( ns.isNull() ){
+          to_erase.push_back( stn );
+        }else{
+          Node nb = d_qe->getTermDatabaseSygus()->sygusToBuiltin( ns, stn );
+          Node nr = Rewriter::rewrite( nb );//d_qe->getTermDatabaseSygus()->getNormalized( stn, nb, false, false );
+          Trace("csi-rcons-debug2") << "  - try " << ns << " -> " << nr << " for " << stn << " " << nr.getKind() << std::endl;
+          std::map< Node, int >::iterator itt = d_rcons_to_id[stn].find( nr );
+          if( itt!= d_rcons_to_id[stn].end() ){
+            // if it is not already reconstructed
+            if( d_reconstruct.find( itt->second )==d_reconstruct.end() ){
+              Trace("csi-rcons") << "...reconstructed " << ns << " for term " << nr << std::endl;
+              bool do_check = getPathToRoot( itt->second );
+              setReconstructed( itt->second, ns );
+              if( do_check ){
+                Trace("csi-rcons-debug") << "...path to root, try reconstruction." << std::endl;
+                d_tmp_fail.clear();
+                Node ret = getReconstructedSolution( d_root_id );
+                if( !ret.isNull() ){
+                  Trace("csi-rcons") << "Sygus solution (after enumeration) is : " << ret << std::endl;
+                  reconstructed = 1;
+                  return ret;
+                }
+              }else{
+                Trace("csi-rcons-debug") << "...no path to root." << std::endl;
+              }
+            }
+          }
+        }
+      }
+      for( unsigned i=0; i<to_erase.size(); i++ ){
+        active.erase( to_erase[i] );
+      }
+      index++;
+      if( index%100==0 ){
+        Trace("csi-rcons-stats") << "Tried " << index << " for each type."  << std::endl;
+      }
+    }while( !active.empty() );
+
+    //if solution is null, we ran out of elements, return the original solution
+    return sol;
+  }
+}
+
+int CegConjectureSingleInvSol::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;
+    //Trace("csi-rcons-debug") << "-> (cached) " << status << " for " << d_rcons_to_id[stn][t] << std::endl;
+    return d_rcons_to_id[stn][t];
+  }else{
+    status = 1;
+    d_qe->getTermDatabaseSygus()->registerSygusType( stn );
+    int id = allocate( t, stn );
+    d_rcons_to_status[stn][t] = -1;
+    TypeNode tn = t.getType();
+    Assert( datatypes::DatatypesRewriter::isTypeDatatype( stn ) );
+    const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
+    Assert( dt.isSygus() );
+    Trace("csi-rcons-debug") << "Check reconstruct " << t << ", sygus type " << dt.getName() << ", kind " << t.getKind() << ", id : " << id << std::endl;
+    int carg = -1;
+    int karg = -1;
+    // first, do standard minimizations
+    Node min_t = d_qe->getTermDatabaseSygus()->minimizeBuiltinTerm( t );
+    Trace("csi-rcons-debug") << "Minimized term is : " << min_t << std::endl;
+    //check if op is in syntax sort
+    carg = d_qe->getTermDatabaseSygus()->getOpArg( stn, min_t );
+    if( carg!=-1 ){
+      Trace("csi-rcons-debug") << "  Type has constant." << std::endl;
+      d_reconstruct[id] = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, Node::fromExpr( dt[carg].getConstructor() ) );
+      status = 0;
+    }else{
+      //check if kind is in syntax sort
+      karg = d_qe->getTermDatabaseSygus()->getKindArg( stn, min_t.getKind() );
+      if( karg!=-1 ){
+        //collect the children of min_t
+        std::vector< Node > tchildren;
+        if( min_t.getNumChildren()>dt[karg].getNumArgs() && d_qe->getTermDatabaseSygus()->isAssoc( min_t.getKind() ) && dt[karg].getNumArgs()==2 ){
+          tchildren.push_back( min_t[0] );
+          std::vector< Node > rem_children;
+          for( unsigned i=1; i<min_t.getNumChildren(); i++ ){
+            rem_children.push_back( min_t[i] );
+          }
+          Node t2 = NodeManager::currentNM()->mkNode( min_t.getKind(), rem_children );
+          tchildren.push_back( t2 );
+          Trace("csi-rcons-debug") << "...split n-ary to binary " << min_t[0] << " " << t2 << "." << std::endl;
+        }else{
+          for( unsigned i=0; i<min_t.getNumChildren(); i++ ){
+            tchildren.push_back( min_t[i] );
+          }
+        }
+        //recurse on the children
+        if( tchildren.size()==dt[karg].getNumArgs() ){
+          Trace("csi-rcons-debug") << "Type for " << id << " has kind " << min_t.getKind() << ", recurse." << std::endl;
+          status = 0;
+          Node cons = Node::fromExpr( dt[karg].getConstructor() );
+          if( !collectReconstructNodes( id, tchildren, dt[karg], d_reconstruct_op[id][cons], status ) ){
+            Trace("csi-rcons-debug") << "...failure for " << id << " " << dt[karg].getName() << std::endl;
+            d_reconstruct_op[id].erase( cons );
+            status = 1;
+          }
+        }else{
+          Trace("csi-rcons-debug") << "Type for " << id << " has kind " << min_t.getKind() << ", but argument # mismatch." << std::endl;
+        }
+      }
+    }
+    if( status!=0 ){
+      Trace("csi-rcons-debug") << "Try matching for " << id << "." << std::endl;
+      //try other options
+      //match against other constructors
+      bool success;
+      int c_index = 0;
+      do{
+        success = false;
+        int index_found;
+        std::vector< Node > args;
+        if( d_qe->getTermDatabaseSygus()->getMatch( min_t, stn, index_found, args, karg, c_index ) ){
+          success = true;
+          status = 0;
+          Node cons = Node::fromExpr( dt[index_found].getConstructor() );
+          Trace("csi-rcons-debug") << "Try alternative for " << id << ", matching " << dt[index_found].getName() << " with children : " << std::endl;
+          for( unsigned i=0; i<args.size(); i++ ){
+            Trace("csi-rcons-debug") << "  " << args[i] << std::endl;
+          }
+          if( !collectReconstructNodes( id, args, dt[index_found], d_reconstruct_op[id][cons], status ) ){
+            d_reconstruct_op[id].erase( cons );
+            status = 1;
+          }else{
+            c_index = index_found+1;
+          }
+        }
+      }while( success && status!=0 );
+
+      if( status!=0 ){
+        // construct an equivalence class of terms that are equivalent to t
+        if( d_rep[id]==id ){
+          Trace("csi-rcons-debug") << "Try rewriting for " << id << "." << std::endl;
+          //get equivalence class of term
+          std::vector< Node > equiv;
+          if( tn.isBoolean() ){
+            Node curr = min_t;
+            Node new_t;
+            do{
+              new_t = Node::null();
+              if( curr.getKind()==EQUAL && ( curr[0].getType().isInteger() || curr[0].getType().isReal() ) ){
+                new_t = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, curr[0], curr[1] ),
+                                                              NodeManager::currentNM()->mkNode( LEQ, curr[1], curr[0] ) );
+              }else if( curr.getKind()==ITE ){
+                new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ),
+                                                              NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[2] ) );
+              }else if( curr.getKind()==IFF ){
+                new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ),
+                                                              NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[1].negate() ) );
+              }else if( curr.getKind()==OR || curr.getKind()==AND ){
+                new_t = TermDb::simpleNegate( curr ).negate();
+              }else if( curr.getKind()==NOT ){
+                new_t = TermDb::simpleNegate( curr[0] );
+              }else{
+                new_t = NodeManager::currentNM()->mkNode( NOT, NodeManager::currentNM()->mkNode( NOT, curr ) );
+              }
+              if( !new_t.isNull() ){
+                if( new_t!=min_t && std::find( equiv.begin(), equiv.end(), new_t )==equiv.end() ){
+                  curr = new_t;
+                  equiv.push_back( new_t );
+                }else{
+                  new_t = Node::null();
+                }
+              }
+            }while( !new_t.isNull()  );
+          }
+          //assign ids to terms
+          Trace("csi-rcons-debug") << "Term " << id << " is equivalent to " << equiv.size() << " terms : " << std::endl;
+          std::vector< int > equiv_ids;
+          for( unsigned i=0; i<equiv.size(); i++ ){
+            Trace("csi-rcons-debug") << "  " << equiv[i] << std::endl;
+            if( d_rcons_to_id[stn].find( equiv[i] )==d_rcons_to_id[stn].end() ){
+              int eq_id = allocate( equiv[i], stn );
+              d_eqc.erase( eq_id );
+              d_rep[eq_id] = id;
+              d_eqc[id].push_back( eq_id );
+              equiv_ids.push_back( eq_id );
+            }else{
+              equiv_ids.push_back( -1 );
+            }
+          }
+          // now, try each of them
+          for( unsigned i=0; i<equiv.size(); i++ ){
+            if( equiv_ids[i]!=-1 ){
+              collectReconstructNodes( equiv[i], stn, status );
+              //if one succeeds
+              if( status==0 ){
+                Node rsol = getReconstructedSolution( equiv_ids[i] );
+                Assert( !rsol.isNull() );
+                //set all members of the equivalence class that this is the reconstructed solution
+                setReconstructed( id, rsol );
+                break;
+              }
+            }
+          }
+        }else{
+          Trace("csi-rcons-debug") << "Do not try rewriting for " << id << ", rep = " << d_rep[id] << std::endl;
+        }
+      }
+    }
+    if( status!=0 ){
+      Trace("csi-rcons-debug") << "-> *** reconstruction required for id " << id << std::endl;
+    }else{
+      Trace("csi-rcons-debug") << "-> success for " << id << std::endl;
+    }
+    d_rcons_to_status[stn][t] = status;
+    return id;
+  }
+}
+
+bool CegConjectureSingleInvSol::collectReconstructNodes( int pid, std::vector< Node >& ts, const DatatypeConstructor& dtc, std::vector< int >& ids, int& status ) {
+  for( unsigned i=0; i<ts.size(); i++ ){
+    TypeNode cstn = d_qe->getTermDatabaseSygus()->getArgType( dtc, i );
+    int cstatus;
+    int c_id = collectReconstructNodes( ts[i], cstn, cstatus );
+    if( cstatus==-1 ){
+      return false;
+    }else if( cstatus!=0 ){
+      status = 1;
+    }
+    ids.push_back( c_id );
+  }
+  for( unsigned i=0; i<ids.size(); i++ ){
+    d_parents[ids[i]].push_back( pid );
+  }
+  return true;
+}
+
+  /*
+  //flatten ITEs if necessary  TODO : carry assignment or move this elsewhere
+  if( t.getKind()==ITE ){
+    TypeNode cstn = tds->getArgType( dt[karg], 0 );
+    tds->registerSygusType( cstn );
+    Node prev_t;
+    while( !tds->hasKind( cstn, t[0].getKind() ) && t!=prev_t ){
+      prev_t = t;
+      Node exp_c = tds->expandBuiltinTerm( t[0] );
+      if( !exp_c.isNull() ){
+        t = NodeManager::currentNM()->mkNode( ITE, exp_c, t[1], t[2] );
+        Trace("csi-rcons-debug") << "Pre expand to " << t << std::endl;
+      }
+      t = flattenITEs( t, false );
+      if( t!=prev_t ){
+        Trace("csi-rcons-debug") << "Flatten ITE to " << t << std::endl;
+        std::map< Node, bool > sassign;
+        std::vector< Node > svars;
+        std::vector< Node > ssubs;
+        t = simplifySolutionNode( t, sassign, svars, ssubs, 0 );
+      }
+      Assert( t.getKind()==ITE );
+    }
+  }
+  */
+
+
+Node CegConjectureSingleInvSol::CegConjectureSingleInvSol::getReconstructedSolution( int id, bool mod_eq ) {
+  std::map< int, Node >::iterator it = d_reconstruct.find( id );
+  if( it!=d_reconstruct.end() ){
+    return it->second;
+  }else{
+    if( std::find( d_tmp_fail.begin(), d_tmp_fail.end(), id )!=d_tmp_fail.end() ){
+      return Node::null();
+    }else{
+      // try each child option
+      std::map< int, std::map< Node, std::vector< int > > >::iterator ito = d_reconstruct_op.find( id );
+      if( ito!=d_reconstruct_op.end() ){
+        for( std::map< Node, std::vector< int > >::iterator itt = ito->second.begin(); itt != ito->second.end(); ++itt ){
+          std::vector< Node > children;
+          children.push_back( itt->first );
+          bool success = true;
+          for( unsigned i=0; i<itt->second.size(); i++ ){
+            Node nc = getReconstructedSolution( itt->second[i] );
+            if( nc.isNull() ){
+              success = false;
+              break;
+            }else{
+              children.push_back( nc );
+            }
+          }
+          if( success ){
+            Node ret = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
+            setReconstructed( id, ret );
+            return ret;
+          }
+        }
+      }
+      // try terms in the equivalence class of this
+      if( mod_eq ){
+        int rid = d_rep[id];
+        for( unsigned i=0; i<d_eqc[rid].size(); i++ ){
+          int tid = d_eqc[rid][i];
+          if( tid!=id ){
+            Node eret = getReconstructedSolution( tid, false );
+            if( !eret.isNull() ){
+              setReconstructed( id, eret );
+              return eret;
+            }
+          }
+        }
+      }
+      d_tmp_fail.push_back( id );
+      return Node::null();
+    }
+  }
+}
+
+int CegConjectureSingleInvSol::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;
+    Trace("csi-rcons-debug") << "id " << ret << " : " << n << std::endl;
+    d_id_node[d_id_count] = n;
+    d_id_type[d_id_count] = stn;
+    d_rep[d_id_count] = d_id_count;
+    d_eqc[d_id_count].push_back( d_id_count );
+    d_rcons_to_id[stn][n] = d_id_count;
+    d_id_count++;
+    return ret;
+  }else{
+    return it->second;
+  }
+}
+
+bool CegConjectureSingleInvSol::getPathToRoot( int id ) {
+  if( id==d_root_id ){
+    return true;
+  }else{
+    std::map< int, Node >::iterator it = d_reconstruct.find( id );
+    if( it!=d_reconstruct.end() ){
+      return false;
+    }else{
+      int rid = d_rep[id];
+      for( unsigned j=0; j<d_parents[rid].size(); j++ ){
+        if( getPathToRoot( d_parents[rid][j] ) ){
+          return true;
+        }
+      }
+      return false;
+    }
+  }
+}
+
+void CegConjectureSingleInvSol::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++ ){
+    d_reconstruct[d_eqc[rid][i]] = n;
+  }
+}
+
+}
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.h b/src/theory/quantifiers/ce_guided_single_inv_sol.h
new file mode 100644
index 000000000..6a4b6f90f
--- /dev/null
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.h
@@ -0,0 +1,92 @@
+/*********************                                                        */
+/*! \file ce_guided_single_inv_sol.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief utility for reconstructing solutions for single invocation synthesis conjectures
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_SOL_H
+#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_SOL_H
+
+#include "context/cdhashmap.h"
+#include "context/cdchunk_list.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+
+class CegConjectureSingleInv;
+
+class CegConjectureSingleInvSol
+{
+  friend class CegConjectureSingleInv;
+private:
+  QuantifiersEngine * d_qe;
+  std::vector< Node > d_varList;
+  std::map< Node, int > d_dterm_size;
+  std::map< Node, int > d_dterm_ite_size;
+//solution simplification
+private:
+  bool debugSolution( Node sol );
+  void debugTermSize( Node sol, int& t_size, int& num_ite );
+  Node pullITEs( Node n );
+  bool pullITECondition( Node root, Node n, std::vector< Node >& conj, Node& t, Node& rem, int depth );
+  Node flattenITEs( Node n, bool rec = true );
+  bool 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 getAssignEquality( Node eq, std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs );
+  Node simplifySolutionNode( Node sol, TypeNode stn, std::map< Node, bool >& assign,
+                             std::vector< Node >& vars, std::vector< Node >& subs, int status );
+public:
+  Node simplifySolution( Node sol, TypeNode stn );
+//solution reconstruction
+private:
+  int d_id_count;
+  int d_root_id;
+  std::map< int, Node > d_id_node;
+  std::map< int, TypeNode > d_id_type;
+  std::map< TypeNode, std::map< Node, int > > d_rcons_to_id;
+  std::map< TypeNode, std::map< Node, int > > d_rcons_to_status;
+
+  std::map< int, std::map< Node, std::vector< int > > > d_reconstruct_op;
+  std::map< int, Node > d_reconstruct;
+  std::map< int, std::vector< int > > d_parents;
+
+  std::map< int, std::vector< int > > d_eqc;
+  std::map< int, int > d_rep;
+
+  //cache when reconstructing solutions
+  std::vector< int > d_tmp_fail;
+  // get reconstructed solution
+  Node getReconstructedSolution( int id, bool mod_eq = true );
+
+  // allocate node with type
+  int allocate( Node n, TypeNode stn );
+  // term t with sygus type st, returns inducted templated form of t
+  int collectReconstructNodes( Node t, TypeNode stn, int& status );
+  bool collectReconstructNodes( int pid, std::vector< Node >& ts, const DatatypeConstructor& dtc, std::vector< int >& ids, int& status );
+  bool getPathToRoot( int id );
+  void setReconstructed( int id, Node n );
+public:
+  Node reconstructSolution( Node sol, TypeNode stn, int& reconstructed );
+public:
+  CegConjectureSingleInvSol( QuantifiersEngine * qe );
+};
+
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index cca2cb5e2..e3f73699b 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1145,6 +1145,18 @@ bool TermDb::containsTerm( Node n, Node t ) {
   }
 }
 
+Node TermDb::simpleNegate( Node n ){
+  if( n.getKind()==OR || n.getKind()==AND ){
+    std::vector< Node > children;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      children.push_back( simpleNegate( n[i] ) );
+    }
+    return NodeManager::currentNM()->mkNode( n.getKind()==OR ? AND : OR, children );
+  }else{
+    return n.negate();
+  }
+}
+
 
 void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){
   if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){
@@ -1404,6 +1416,85 @@ bool TermDbSygus::getMatch2( Node p, Node n, std::map< int, Node >& s, std::vect
   return false;
 }
 
+bool TermDbSygus::getMatch( Node t, TypeNode st, int& index_found, std::vector< Node >& args, int index_exc, int index_start ) {
+  Assert( datatypes::DatatypesRewriter::isTypeDatatype( st ) );
+  const Datatype& dt = ((DatatypeType)(st).toType()).getDatatype();
+  Assert( dt.isSygus() );
+  std::map< Kind, std::vector< Node > > kgens;
+  std::vector< Node > gens;
+  for( unsigned i=index_start; i<dt.getNumConstructors(); i++ ){
+    if( (int)i!=index_exc ){
+      Node g = getGenericBase( st, dt, i );
+      gens.push_back( g );
+      kgens[g.getKind()].push_back( g );
+      Trace("sygus-db-debug") << "Check generic base : " << g << " from " << dt[i].getName() << std::endl;
+      if( g.getKind()==t.getKind() ){
+        Trace("sygus-db-debug") << "Possible match ? " << g << " " << t << " for " << dt[i].getName() << std::endl;
+        std::map< int, Node > sigma;
+        if( getMatch( g, t, sigma ) ){
+          //we found an exact match
+          bool msuccess = true;
+          for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
+            if( sigma[j].isNull() ){
+              msuccess = false;
+              break;
+            }else{
+              args.push_back( sigma[j] );
+            }
+          }
+          if( msuccess ){
+            index_found = i;
+            return true;
+          }
+          //we found an exact match
+          //std::map< TypeNode, int > var_count;
+          //Node new_t = mkGeneric( dt, i, var_count, args );
+          //Trace("sygus-db-debug") << "Rewrote to : " << new_t << std::endl;
+          //return new_t;
+        }
+      }
+    }
+  }
+  /*
+  //otherwise, try to modulate based on kinds
+  for( std::map< Kind, std::vector< Node > >::iterator it = kgens.begin(); it != kgens.end(); ++it ){
+    if( it->second.size()>1 ){
+      for( unsigned i=0; i<it->second.size(); i++ ){
+        for( unsigned j=0; j<it->second.size(); j++ ){
+          if( i!=j ){
+            std::map< int, Node > sigma;
+            if( getMatch( it->second[i], it->second[j], sigma ) ){
+              if( sigma.size()==1 ){
+                //Node mod_pat = sigma.begin().second;
+                //Trace("cegqi-si-rcons-debug") << "Modulated pattern " << mod_pat << " from " << it->second[i] << " and " << it->second[j] << std::endl;
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+  */
+  return false;
+}
+
+Node TermDbSygus::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() ){
+    registerSygusType( tn );
+    std::map< TypeNode, int > var_count;
+    std::map< int, Node > pre;
+    Node g = mkGeneric( dt, c, var_count, pre );
+    Node gr = Rewriter::rewrite( g );
+    gr = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( gr.toExpr() ) );
+    Trace("sygus-db") << "Sygus DB : Generic base " << dt[c].getName() << " : " << gr << std::endl;
+    d_generic_base[tn][c] = gr;
+    return gr;
+  }else{
+    return it->second;
+  }
+}
+
 Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre ) {
   Assert( c>=0 && c<(int)dt.getNumConstructors() );
   Assert( dt.isSygus() );
@@ -1443,24 +1534,6 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int
   }
 }
 
-Node TermDbSygus::getGenericBase( TypeNode tn, int c ) {
-  std::map< int, Node >::iterator it = d_generic_base[tn].find( c );
-  if( it==d_generic_base[tn].end() ){
-    Assert( datatypes::DatatypesRewriter::isTypeDatatype( tn ) );
-    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-    Assert( dt.isSygus() );
-    registerSygusType( tn );
-    std::map< TypeNode, int > var_count;
-    std::map< int, Node > pre;
-    Node g = mkGeneric( dt, c, var_count, pre );
-    Node gr = Rewriter::rewrite( g );
-    d_generic_base[tn][c] = gr;
-    return gr;
-  }else{
-    return it->second;
-  }
-}
-
 Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) {
   std::map< Node, Node >::iterator it = d_sygus_to_builtin[tn].find( n );
   if( it==d_sygus_to_builtin[tn].end() ){
@@ -1474,6 +1547,7 @@ Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) {
       pre[j] = sygusToBuiltin( n[j], getArgType( dt[i], j ) );
     }
     Node ret = mkGeneric( dt, i, var_count, pre );
+    ret = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( ret.toExpr() ) );
     d_sygus_to_builtin[tn][n] = ret;
     return ret;
   }else{
@@ -1571,7 +1645,6 @@ int TermDbSygus::getTermSize( Node n ){
     }
     return 1+sum;
   }
-
 }
 
 bool TermDbSygus::isAssoc( Kind k ) {
@@ -1868,7 +1941,8 @@ TypeNode TermDbSygus::getArgType( const DatatypeConstructor& c, int i ) {
 }
 
 Node TermDbSygus::minimizeBuiltinTerm( Node n ) {
-  if( ( n.getKind()==EQUAL || n.getKind()==LEQ ) && ( n[0].getType().isInteger() || n[0].getType().isReal() ) ){
+  if( ( n.getKind()==EQUAL || n.getKind()==LEQ || n.getKind()==LT || n.getKind()==GEQ || n.getKind()==GT ) && 
+      ( n[0].getType().isInteger() || n[0].getType().isReal() ) ){
     bool changed = false;
     std::vector< Node > mon[2];
     for( unsigned r=0; r<2; r++ ){
@@ -1908,12 +1982,12 @@ Node TermDbSygus::expandBuiltinTerm( Node t ){
   if( t.getKind()==EQUAL && ( t[0].getType().isInteger() || t[0].getType().isReal() ) ){
     return NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, t[0], t[1] ),
                                                   NodeManager::currentNM()->mkNode( LEQ, t[1], t[0] ) );
-  }else if( t.getKind()==ITE ){
+  }else if( t.getKind()==ITE && t.getType().isBoolean() ){
     return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ),
-                                                  NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[2] ) );
+                                                 NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[2] ) );
   }else if( t.getKind()==IFF ){
     return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ),
-                                                  NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[1].negate() ) );
+                                                 NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[1].negate() ) );
   }
   return Node::null();
 }
\ No newline at end of file
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 1e457f8ec..e4e34ce7f 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -317,8 +317,13 @@ public:
   int isInstanceOf( Node n1, Node n2 );
   /** filter all nodes that have instances */
   void filterInstances( std::vector< Node >& nodes );
+
+//general utilities
+public:
   /** simple check for contains term */
-  bool containsTerm( Node n, Node t );
+  static bool containsTerm( Node n, Node t );
+  /** simple negate */
+  static Node simpleNegate( Node n );
 
 //for sygus
 private:
@@ -374,8 +379,14 @@ public:
   TNode getVarInc( TypeNode tn, std::map< TypeNode, int >& var_count );
   bool isVar( Node n ) { return d_fv_stype.find( n )!=d_fv_stype.end(); }
   int getVarNum( Node n ) { return d_fv_num[n]; }
+private:
+  std::map< TypeNode, std::map< int, Node > > d_generic_base;
+  std::map< TypeNode, std::vector< Node > > d_generic_templ;
+  Node getGenericBase( TypeNode tn, const Datatype& dt, int c );
   bool getMatch( Node p, Node n, std::map< int, Node >& s );
   bool getMatch2( Node p, Node n, std::map< int, Node >& s, std::vector< int >& new_s );
+public:
+  bool getMatch( Node n, TypeNode st, int& index_found, std::vector< Node >& args, int index_exc = -1, int index_start = 0 );
 private:
   //information for sygus types
   std::map< TypeNode, TypeNode > d_register;  //stores sygus type
@@ -394,7 +405,6 @@ private:
   std::map< TypeNode, std::map< Node, Node > > d_normalized;
   std::map< TypeNode, std::map< Node, Node > > d_sygus_to_builtin;
   std::map< TypeNode, std::map< Node, Node > > d_builtin_const_to_sygus;
-  std::map< TypeNode, std::map< int, Node > > d_generic_base;
 public:
   TermDbSygus(){}
   bool isRegistered( TypeNode tn );
@@ -432,7 +442,6 @@ public:
   Node getTypeMaxValue( TypeNode tn );
   TypeNode getSygusType( Node v );
   Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre );
-  Node getGenericBase( TypeNode tn, int c );
   Node sygusToBuiltin( Node n, TypeNode tn );
   Node builtinToSygusConst( Node c, TypeNode tn );
   Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs );