Replace old sygus term reconstruction algorithm with a new one. (#5779)

This PR replaces the old algorithm for reconstructing sygus terms with a new "proper" implementation.

13 files changed, 1268 insertions, 1299 deletions

diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h
index a5fb33a1f..3313b507b 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.h
+++ b/src/theory/quantifiers/candidate_rewrite_database.h
@@ -58,8 +58,7 @@ class CandidateRewriteDatabase : public ExprMiner
                            bool filterPairs = true);
   ~CandidateRewriteDatabase() {}
   /**  Initialize this class */
-  void initialize(const std::vector<Node>& var,
-                  SygusSampler* ss = nullptr) override;
+  void initialize(const std::vector<Node>& var, SygusSampler* ss) override;
   /**  Initialize this class
    *
    * Serves the same purpose as the above function, but we will be using
@@ -75,7 +74,7 @@ class CandidateRewriteDatabase : public ExprMiner
   void initializeSygus(const std::vector<Node>& vars,
                        QuantifiersEngine* qe,
                        Node f,
-                       SygusSampler* ss = nullptr);
+                       SygusSampler* ss);
   /** add term
    *
    * Notifies this class that the solution sol was enumerated. This may
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 3e223fd7c..f93260f0c 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -23,6 +23,7 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
+#include "theory/quantifiers/sygus/sygus_reconstruct.h"
 #include "theory/quantifiers/sygus/sygus_utils.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_enumeration.h"
@@ -37,19 +38,17 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-CegSingleInv::CegSingleInv(QuantifiersEngine* qe)
+CegSingleInv::CegSingleInv(QuantifiersEngine* qe, SygusStatistics& s)
     : d_qe(qe),
       d_sip(new SingleInvocationPartition),
-      d_sol(new CegSingleInvSol(qe)),
+      d_srcons(new SygusReconstruct(qe->getTermDatabaseSygus(), s)),
       d_isSolved(false),
       d_single_invocation(false)
 {
-
 }
 
 CegSingleInv::~CegSingleInv()
 {
-  delete d_sol;  // (new CegSingleInvSol(qe)),
   delete d_sip;  // d_sip(new SingleInvocationPartition),
 }
 
@@ -296,7 +295,7 @@ struct sortSiInstanceIndices {
 
 Node CegSingleInv::getSolution(size_t sol_index,
                                TypeNode stn,
-                               int& reconstructed,
+                               int8_t& reconstructed,
                                bool rconsSygus)
 {
   Assert(sol_index < d_quant[0].getNumChildren());
@@ -316,21 +315,18 @@ Node CegSingleInv::getSolution(size_t sol_index,
   // must substitute to be proper variables
   const DType& dt = stn.getDType();
   Node varList = dt.getSygusVarList();
-  d_sol->d_varList.clear();
   Assert(d_single_inv_arg_sk.size() == varList.getNumChildren());
-  std::vector< Node > vars;
+  std::vector<Node> vars;
+  std::vector<Node> sygusVars;
   for (size_t i = 0, nvars = d_single_inv_arg_sk.size(); i < nvars; i++)
   {
     Trace("csi-sol") << d_single_inv_arg_sk[i] << " ";
     vars.push_back(d_single_inv_arg_sk[i]);
-    d_sol->d_varList.push_back(varList[i]);
+    sygusVars.push_back(varList[i]);
   }
   Trace("csi-sol") << std::endl;
-  Assert(vars.size() == d_sol->d_varList.size());
-  sol = sol.substitute(vars.begin(),
-                       vars.end(),
-                       d_sol->d_varList.begin(),
-                       d_sol->d_varList.end());
+  sol = sol.substitute(
+      vars.begin(), vars.end(), sygusVars.begin(), sygusVars.end());
   sol = reconstructToSyntax(sol, stn, reconstructed, rconsSygus);
   return s.getKind() == LAMBDA
              ? NodeManager::currentNM()->mkNode(LAMBDA, s[0], sol)
@@ -339,7 +335,6 @@ Node CegSingleInv::getSolution(size_t sol_index,
 
 Node CegSingleInv::getSolutionFromInst(size_t index)
 {
-  Assert(d_sol != NULL);
   Node prog = d_quant[0][index];
   Node s;
   // If it is unconstrained: either the variable does not appear in the
@@ -431,21 +426,20 @@ void CegSingleInv::setSolution()
 
 Node CegSingleInv::reconstructToSyntax(Node s,
                                        TypeNode stn,
-                                       int& reconstructed,
+                                       int8_t& reconstructed,
                                        bool rconsSygus)
 {
   // extract the lambda body
   Node sol = s;
   const DType& dt = stn.getDType();
 
-  //reconstruct the solution into sygus if necessary
+  // reconstruct the solution into sygus if necessary
   reconstructed = 0;
   if (options::cegqiSingleInvReconstruct()
           != options::CegqiSingleInvRconsMode::NONE
       && !dt.getSygusAllowAll() && !stn.isNull() && rconsSygus)
   {
-    d_sol->preregisterConjecture( d_orig_conjecture );
-    int enumLimit = -1;
+    int64_t enumLimit = -1;
     if (options::cegqiSingleInvReconstruct()
         == options::CegqiSingleInvRconsMode::TRY)
     {
@@ -456,12 +450,15 @@ Node CegSingleInv::reconstructToSyntax(Node s,
     {
       enumLimit = options::cegqiSingleInvReconstructLimit();
     }
-    sol = d_sol->reconstructSolution(s, stn, reconstructed, enumLimit);
-    if( reconstructed==1 ){
+    sol = d_srcons->reconstructSolution(s, stn, reconstructed, enumLimit);
+    if (reconstructed == 1)
+    {
       Trace("csi-sol") << "Solution (post-reconstruction into Sygus): " << sol
                        << std::endl;
     }
-  }else{
+  }
+  else
+  {
     Trace("csi-sol") << "Post-process solution..." << std::endl;
     Node prev = sol;
     sol = d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(sol);
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
index a650a58a9..c73954195 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
@@ -22,13 +22,14 @@
 #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
 #include "theory/quantifiers/inst_match_trie.h"
 #include "theory/quantifiers/single_inv_partition.h"
-#include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h"
+#include "theory/quantifiers/sygus/sygus_stats.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
 class SynthConjecture;
+class SygusReconstruct;
 
 // this class infers whether a conjecture is single invocation (Reynolds et al CAV 2015), and sets up the
 // counterexample-guided quantifier instantiation utility (d_cinst), and methods for solution
@@ -53,8 +54,8 @@ class CegSingleInv
   QuantifiersEngine* d_qe;
   // single invocation inference utility
   SingleInvocationPartition* d_sip;
-  // solution reconstruction
-  CegSingleInvSol* d_sol;
+  /** solution reconstruction */
+  std::unique_ptr<SygusReconstruct> d_srcons;
 
   // list of skolems for each argument of programs
   std::vector<Node> d_single_inv_arg_sk;
@@ -91,7 +92,7 @@ class CegSingleInv
   Node d_single_inv;
   
  public:
-  CegSingleInv(QuantifiersEngine* qe);
+  CegSingleInv(QuantifiersEngine* qe, SygusStatistics& s);
   ~CegSingleInv();
 
   // get simplified conjecture
@@ -132,11 +133,13 @@ class CegSingleInv
    */
   Node getSolution(size_t sol_index,
                    TypeNode stn,
-                   int& reconstructed,
+                   int8_t& reconstructed,
                    bool rconsSygus = true);
   //reconstruct to syntax
-  Node reconstructToSyntax( Node s, TypeNode stn, int& reconstructed,
-                            bool rconsSygus = true );
+  Node reconstructToSyntax(Node s,
+                           TypeNode stn,
+                           int8_t& reconstructed,
+                           bool rconsSygus = true);
   // is single invocation
   bool isSingleInvocation() const { return !d_single_inv.isNull(); }
   /** preregister conjecture */
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
deleted file mode 100644
index 509e4905e..000000000
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ /dev/null
@@ -1,1055 +0,0 @@
-/*********************                                                        */
-/*! \file ce_guided_single_inv_sol.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief utility for processing single invocation synthesis conjectures
- **
- **/
-#include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h"
-
-#include "expr/dtype.h"
-#include "expr/dtype_cons.h"
-#include "expr/node_algorithm.h"
-#include "options/quantifiers_options.h"
-#include "smt/command.h"
-#include "theory/arith/arith_msum.h"
-#include "theory/quantifiers/ematching/trigger.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/sygus/ce_guided_single_inv.h"
-#include "theory/quantifiers/sygus/synth_engine.h"
-#include "theory/quantifiers/sygus/term_database_sygus.h"
-#include "theory/quantifiers/term_enumeration.h"
-#include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
-#include "theory/rewriter.h"
-
-using namespace CVC4::kind;
-using namespace std;
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-bool doCompare(Node a, Node b, Kind k)
-{
-  Node com = NodeManager::currentNM()->mkNode(k, a, b);
-  com = Rewriter::rewrite(com);
-  Assert(com.getType().isBoolean());
-  return com.isConst() && com.getConst<bool>();
-}
-
-CegSingleInvSol::CegSingleInvSol(QuantifiersEngine* qe)
-    : d_qe(qe), d_id_count(0), d_root_id()
-{
-}
-
-void CegSingleInvSol::preregisterConjecture(Node q)
-{
-  Trace("csi-sol") << "Preregister conjecture : " << q << std::endl;
-  Node n = q;
-  if( n.getKind()==FORALL ){
-    n = n[1];
-  }
-  if( n.getKind()==EXISTS ){
-    if( n[0].getNumChildren()==d_varList.size() ){
-      std::vector< Node > evars;
-      for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
-        evars.push_back( n[0][i] );
-      }
-      n = n[1].substitute( evars.begin(), evars.end(), d_varList.begin(), d_varList.end() );
-    }else{
-      Trace("csi-sol") << "Not the same number of variables, return." << std::endl;
-      return;
-    }
-  }
-  Trace("csi-sol") << "Preregister node for solution reconstruction : " << n << std::endl;
-  registerEquivalentTerms( n );
-}
-
-Node CegSingleInvSol::reconstructSolution(Node sol,
-                                          TypeNode stn,
-                                          int& reconstructed,
-                                          int enumLimit)
-{
-  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;
-  }
-  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(tn.isDatatype());
-      const DType& dt = tn.getDType();
-      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());
-    }
-  }
-  if (enumLimit != 0)
-  {
-    int 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 tn = it->first;
-        Node ns = d_qe->getTermEnumeration()->getEnumerateTerm(tn, index);
-        if( ns.isNull() ){
-          to_erase.push_back(tn);
-        }else{
-          Node nb = d_qe->getTermDatabaseSygus()->sygusToBuiltin(ns, tn);
-          Node nr = Rewriter::rewrite(nb);  // d_qe->getTermDatabaseSygus()->getNormalized(
-                                            // tn, nb, false, false );
-          Trace("csi-rcons-debug2")
-              << "  - try " << ns << " -> " << nr << " for " << tn << " "
-              << nr.getKind() << std::endl;
-          std::map<Node, int>::iterator itt = d_rcons_to_id[tn].find(nr);
-          if (itt != d_rcons_to_id[tn].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;
-              setReconstructed(itt->second, ns);
-              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;
-              }
-            }
-          }
-        }
-      }
-      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() && (enumLimit < 0 || index < enumLimit));
-  }
-
-  // we ran out of elements, return null
-  reconstructed = -1;
-  Warning() << CommandFailure(
-      "Cannot get synth function: reconstruction to syntax failed.");
-  // could return sol here, however, we choose to fail by returning null, since
-  // it indicates a failure.
-  return Node::null();
-}
-
-int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status)
-{
-  std::map< Node, int >::iterator itri = d_rcons_to_status[stn].find( t );
-  if( itri!=d_rcons_to_status[stn].end() ){
-    status = itri->second;
-    //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;
-    // register the type
-    registerType(stn);
-    int id = allocate( t, stn );
-    d_rcons_to_status[stn][t] = -1;
-    TypeNode tn = t.getType();
-    Assert(stn.isDatatype());
-    const DType& dt = stn.getDType();
-    TermDbSygus* tds = d_qe->getTermDatabaseSygus();
-    SygusTypeInfo& sti = tds->getTypeInfo(stn);
-    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 = minimizeBuiltinTerm(t);
-    Trace("csi-rcons-debug") << "Minimized term is : " << min_t << std::endl;
-    //check if op is in syntax sort
-
-    carg = sti.getOpConsNum(min_t);
-    if( carg!=-1 ){
-      Trace("csi-rcons-debug") << "  Type has operator." << std::endl;
-      d_reconstruct[id] = NodeManager::currentNM()->mkNode(
-          APPLY_CONSTRUCTOR, dt[carg].getConstructor());
-      status = 0;
-    }else{
-      //check if kind is in syntax sort
-      karg = sti.getKindConsNum(min_t.getKind());
-      if( karg!=-1 ){
-        //collect the children of min_t
-        std::vector< Node > tchildren;
-        if( min_t.getNumChildren()>dt[karg].getNumArgs() && quantifiers::TermUtil::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 = 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 ){
-        //try constant reconstruction
-        if( min_t.isConst() ){
-          Trace("csi-rcons-debug") << "...try constant reconstruction." << std::endl;
-          Node min_t_c = builtinToSygusConst(min_t, stn);
-          if( !min_t_c.isNull() ){
-            Trace("csi-rcons-debug") << "   constant reconstruction success for " << id << ", result = " << min_t_c << std::endl;
-            d_reconstruct[id] = min_t_c;
-            status = 0;
-          }
-        }
-        if( status!=0 ){
-          //try identity functions
-          for (unsigned ii : d_id_funcs[stn])
-          {
-            Assert(dt[ii].getNumArgs() == 1);
-            //try to directly reconstruct from single argument
-            std::vector< Node > tchildren;
-            tchildren.push_back( min_t );
-            TypeNode stnc = dt[ii][0].getRangeType();
-            Trace("csi-rcons-debug") << "...try identity function " << dt[ii].getSygusOp() << ", child type is " << stnc << std::endl;
-            status = 0;
-            Node cons = dt[ii].getConstructor();
-            if( !collectReconstructNodes( id, tchildren, dt[ii], d_reconstruct_op[id][cons], status ) ){
-              d_reconstruct_op[id].erase( cons );
-              status = 1;
-            }else{
-              Trace("csi-rcons-debug") << "   identity function success for " << id << std::endl;
-              break;
-            }
-          }
-          if( status!=0 ){
-            //try other options, such as matching against other constructors
-            Trace("csi-rcons-debug") << "Try matching for " << id << "." << std::endl;
-            bool success;
-            int c_index = 0;
-            do{
-              success = false;
-              int index_found;
-              std::vector< Node > args;
-              if (getMatch(min_t, stn, index_found, args, karg, c_index))
-              {
-                success = true;
-                status = 0;
-                Node cons = 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 ){
-                      if( 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[0].getType().isBoolean() ){
-                        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{
-                        new_t = NodeManager::currentNM()->mkNode( NOT, NodeManager::currentNM()->mkNode( NOT, curr ) );
-                      }
-                    }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()==OR || curr.getKind()==AND ){
-                      new_t = TermUtil::simpleNegate( curr ).negate();
-                    }else if( curr.getKind()==NOT ){
-                      new_t = TermUtil::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() );
-                }
-                //get decompositions
-                for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-                  Kind k = sti.getConsNumKind(i);
-                  getEquivalentTerms( k, min_t, equiv );
-                }
-                //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 CegSingleInvSol::collectReconstructNodes(int pid,
-                                              std::vector<Node>& ts,
-                                              const DTypeConstructor& dtc,
-                                              std::vector<int>& ids,
-                                              int& status)
-{
-  Assert(dtc.getNumArgs() == ts.size());
-  for( unsigned i=0; i<ts.size(); i++ ){
-    TypeNode cstn = d_qe->getTermDatabaseSygus()->getArgType( dtc, i );
-    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;
-}
-
-Node CegSingleInvSol::CegSingleInvSol::getReconstructedSolution(int id,
-                                                                bool mod_eq)
-{
-  std::map< int, Node >::iterator it = d_reconstruct.find( id );
-  if( it!=d_reconstruct.end() ){
-    return it->second;
-  }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 CegSingleInvSol::allocate(Node n, TypeNode stn)
-{
-  std::map< Node, int >::iterator it = d_rcons_to_id[stn].find( n );
-  if( it==d_rcons_to_id[stn].end() ){
-    int ret = d_id_count;
-    if( Trace.isOn("csi-rcons-debug") ){
-      const DType& dt = stn.getDType();
-      Trace("csi-rcons-debug") << "id " << ret << " : " << n << " " <<  dt.getName() << 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 CegSingleInvSol::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 CegSingleInvSol::setReconstructed(int id, Node n)
-{
-  //set all equivalent to this as reconstructed
-  int rid = d_rep[id];
-  for( unsigned i=0; i<d_eqc[rid].size(); i++ ){
-    d_reconstruct[d_eqc[rid][i]] = n;
-  }
-}
-
-void CegSingleInvSol::getEquivalentTerms(Kind k,
-                                         Node n,
-                                         std::vector<Node>& equiv)
-{
-  if( k==AND || k==OR ){
-    equiv.push_back( NodeManager::currentNM()->mkNode( k, n, n ) );
-    equiv.push_back( NodeManager::currentNM()->mkNode( k, n, NodeManager::currentNM()->mkConst( k==AND ) ) );
-  }
-  //multiplication for integers
-  //TODO for bitvectors
-  Kind mk = ( k==PLUS || k==MINUS ) ? MULT : UNDEFINED_KIND;
-  if( mk!=UNDEFINED_KIND ){
-    if( n.getKind()==mk && n[0].isConst() && n[0].getType().isInteger() ){
-      bool success = true;
-      for( unsigned i=0; i<2; i++ ){
-        Node eq;
-        if( k==PLUS || k==MINUS ){
-          Node oth = NodeManager::currentNM()->mkConst( Rational(i==0 ? 1000 : -1000) );
-          eq = i==0 ? NodeManager::currentNM()->mkNode( LEQ, n[0], oth ) : NodeManager::currentNM()->mkNode( GEQ, n[0], oth );
-        }
-        if( !eq.isNull() ){
-          eq = Rewriter::rewrite( eq );
-          if (!eq.isConst() || !eq.getConst<bool>())
-          {
-            success = false;
-            break;
-          }
-        }
-      }
-      if( success ){
-        Node var = n[1];
-        Node rem;
-        if( k==PLUS || k==MINUS ){
-          int rem_coeff = (int)n[0].getConst<Rational>().getNumerator().getSignedInt();
-          if( rem_coeff>0 && k==PLUS ){
-            rem_coeff--;
-          }else if( rem_coeff<0 && k==MINUS ){
-            rem_coeff++;
-          }else{
-            success = false;
-          }
-          if( success ){
-            rem = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(rem_coeff) ), var );
-            rem = Rewriter::rewrite( rem );
-          }
-        }
-        if( !rem.isNull() ){
-          equiv.push_back( NodeManager::currentNM()->mkNode( k, rem, var ) );
-        }
-      }
-    }
-  }
-  //negative constants
-  if( k==MINUS ){
-    if( n.isConst() && n.getType().isInteger() && n.getConst<Rational>().getNumerator().strictlyNegative() ){
-      Node nn = NodeManager::currentNM()->mkNode( UMINUS, n );
-      nn = Rewriter::rewrite( nn );
-      equiv.push_back( NodeManager::currentNM()->mkNode( MINUS, NodeManager::currentNM()->mkConst( Rational(0) ), nn ) );
-    }
-  }
-  //inequalities
-  if( k==GEQ || k==LEQ || k==LT || k==GT || k==NOT ){
-    Node atom = n.getKind()==NOT ? n[0] : n;
-    bool pol = n.getKind()!=NOT;
-    Kind ak = atom.getKind();
-    if( ( ak==GEQ || ak==LEQ || ak==LT || ak==GT ) && ( pol || k!=NOT ) ){
-      Node t1 = atom[0];
-      Node t2 = atom[1];
-      if( !pol ){
-        ak = ak==GEQ ? LT : ( ak==LEQ ? GT : ( ak==LT ? GEQ : LEQ ) );
-      }
-      if( k==NOT ){
-        equiv.push_back( NodeManager::currentNM()->mkNode( ak==GEQ ? LT : ( ak==LEQ ? GT : ( ak==LT ? GEQ : LEQ ) ), t1, t2 ).negate() );
-      }else if( k==ak ){
-        equiv.push_back( NodeManager::currentNM()->mkNode( k, t1, t2 ) );
-      }else if( (k==GEQ || k==LEQ)==(ak==GEQ || ak==LEQ) ){
-        equiv.push_back( NodeManager::currentNM()->mkNode( k, t2, t1 ) );
-      }else if( t1.getType().isInteger() && t2.getType().isInteger() ){
-        if( (k==GEQ || k==GT)!=(ak==GEQ || ak==GT) ){
-          Node ts = t1;
-          t1 = t2;
-          t2 = ts;
-          ak = ak==GEQ ? LEQ : ( ak==LEQ ? GEQ : ( ak==LT ? GT : LT ) );
-        }
-        t2 = NodeManager::currentNM()->mkNode( PLUS, t2, NodeManager::currentNM()->mkConst( Rational( (ak==GT || ak==LEQ) ? 1 : -1 ) ) );
-        t2 = Rewriter::rewrite( t2 );
-        equiv.push_back( NodeManager::currentNM()->mkNode( k, t1, t2 ) );
-      }
-    }
-  }
-
-  //based on eqt cache
-  std::map< Node, Node >::iterator itet = d_eqt_rep.find( n );
-  if( itet!=d_eqt_rep.end() ){
-    Node rn = itet->second;
-    for( unsigned i=0; i<d_eqt_eqc[rn].size(); i++ ){
-      if( d_eqt_eqc[rn][i]!=n && d_eqt_eqc[rn][i].getKind()==k ){
-        if( std::find( equiv.begin(), equiv.end(), d_eqt_eqc[rn][i] )==equiv.end() ){
-          equiv.push_back( d_eqt_eqc[rn][i] );
-        }
-      }
-    }
-  }
-}
-
-void CegSingleInvSol::registerEquivalentTerms(Node n)
-{
-  for( unsigned i=0; i<n.getNumChildren(); i++ ){
-    registerEquivalentTerms( n[i] );
-  }
-  Node rn = Rewriter::rewrite( n );
-  if( rn!=n ){
-    Trace("csi-equiv") << "  eq terms : " << n << " " << rn << std::endl;
-    d_eqt_rep[n] = rn;
-    d_eqt_rep[rn] = rn;
-    if( std::find( d_eqt_eqc[rn].begin(), d_eqt_eqc[rn].end(), rn )==d_eqt_eqc[rn].end() ){
-      d_eqt_eqc[rn].push_back( rn );
-    }
-    if( std::find( d_eqt_eqc[rn].begin(), d_eqt_eqc[rn].end(), n )==d_eqt_eqc[rn].end() ){
-      d_eqt_eqc[rn].push_back( n );
-    }
-  }
-}
-
-Node CegSingleInvSol::builtinToSygusConst(Node c, TypeNode tn, int rcons_depth)
-{
-  std::map<Node, Node>::iterator it = d_builtin_const_to_sygus[tn].find(c);
-  if (it != d_builtin_const_to_sygus[tn].end())
-  {
-    return it->second;
-  }
-  TermDbSygus* tds = d_qe->getTermDatabaseSygus();
-  NodeManager* nm = NodeManager::currentNM();
-  SygusTypeInfo& ti = tds->getTypeInfo(tn);
-  Node sc;
-  d_builtin_const_to_sygus[tn][c] = sc;
-  Assert(c.isConst());
-  if (!tn.isDatatype())
-  {
-    // if we've traversed to a builtin type, simply return c
-    d_builtin_const_to_sygus[tn][c] = c;
-    return c;
-  }
-  const DType& dt = tn.getDType();
-  Trace("csi-rcons-debug") << "Try to reconstruct " << c << " in "
-                           << dt.getName() << std::endl;
-  if (!dt.isSygus())
-  {
-    // if we've traversed to a builtin datatype type, simply return c
-    d_builtin_const_to_sygus[tn][c] = c;
-    return c;
-  }
-  // if we are not interested in reconstructing constants, or the grammar allows
-  // them, return a proxy
-  if (!options::cegqiSingleInvReconstructConst() || dt.getSygusAllowConst())
-  {
-    sc = tds->getProxyVariable(tn, c);
-  }
-  else
-  {
-    int carg = ti.getOpConsNum(c);
-    if (carg != -1)
-    {
-      sc = nm->mkNode(APPLY_CONSTRUCTOR, dt[carg].getConstructor());
-    }
-    else
-    {
-      // identity functions
-      for (unsigned ii : d_id_funcs[tn])
-      {
-        Assert(dt[ii].getNumArgs() == 1);
-        // try to directly reconstruct from single argument
-        TypeNode tnc = tds->getArgType(dt[ii], 0);
-        Trace("csi-rcons-debug")
-            << "Based on id function " << dt[ii].getSygusOp()
-            << ", try reconstructing " << c << " instead in " << tnc
-            << std::endl;
-        Node n = builtinToSygusConst(c, tnc, rcons_depth);
-        if (!n.isNull())
-        {
-          sc = nm->mkNode(APPLY_CONSTRUCTOR, dt[ii].getConstructor(), n);
-          break;
-        }
-      }
-      if (sc.isNull())
-      {
-        if (rcons_depth < 1000)
-        {
-          // accelerated, recursive reconstruction of constants
-          Kind pk = getPlusKind(dt.getSygusType());
-          if (pk != UNDEFINED_KIND)
-          {
-            int arg = ti.getKindConsNum(pk);
-            if (arg != -1)
-            {
-              Kind ck = getComparisonKind(dt.getSygusType());
-              Kind pkm = getPlusKind(dt.getSygusType(), true);
-              // get types
-              Assert(dt[arg].getNumArgs() == 2);
-              TypeNode tn1 = tds->getArgType(dt[arg], 0);
-              TypeNode tn2 = tds->getArgType(dt[arg], 1);
-              // initialize d_const_list for tn1
-              registerType(tn1);
-              // iterate over all positive constants, largest to smallest
-              int start = d_const_list[tn1].size() - 1;
-              int end = d_const_list[tn1].size() - d_const_list_pos[tn1];
-              for (int i = start; i >= end; --i)
-              {
-                Node c1 = d_const_list[tn1][i];
-                // only consider if smaller than c, and
-                if (doCompare(c1, c, ck))
-                {
-                  Node c2 = nm->mkNode(pkm, c, c1);
-                  c2 = Rewriter::rewrite(c2);
-                  if (c2.isConst())
-                  {
-                    // reconstruct constant on the other side
-                    Node sc2 = builtinToSygusConst(c2, tn2, rcons_depth + 1);
-                    if (!sc2.isNull())
-                    {
-                      Node sc1 = builtinToSygusConst(c1, tn1, rcons_depth);
-                      Assert(!sc1.isNull());
-                      sc = nm->mkNode(APPLY_CONSTRUCTOR,
-                                      dt[arg].getConstructor(),
-                                      sc1,
-                                      sc2);
-                      break;
-                    }
-                  }
-                }
-              }
-            }
-          }
-        }
-      }
-    }
-  }
-  d_builtin_const_to_sygus[tn][c] = sc;
-  return sc;
-}
-
-struct sortConstants
-{
-  Kind d_comp_kind;
-  bool operator()(Node i, Node j)
-  {
-    return i != j && doCompare(i, j, d_comp_kind);
-  }
-};
-
-void CegSingleInvSol::registerType(TypeNode tn)
-{
-  if (d_const_list_pos.find(tn) != d_const_list_pos.end())
-  {
-    return;
-  }
-  d_const_list_pos[tn] = 0;
-  Assert(tn.isDatatype());
-
-  TermDbSygus* tds = d_qe->getTermDatabaseSygus();
-  // ensure it is registered
-  tds->registerSygusType(tn);
-  const DType& dt = tn.getDType();
-  Assert(dt.isSygus());
-  TypeNode btn = dt.getSygusType();
-  // for constant reconstruction
-  Kind ck = getComparisonKind(btn);
-  Node z = TermUtil::mkTypeValue(btn, 0);
-
-  // iterate over constructors
-  for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
-  {
-    Node n = dt[i].getSygusOp();
-    if (n.getKind() != kind::BUILTIN && n.isConst())
-    {
-      d_const_list[tn].push_back(n);
-      if (ck != UNDEFINED_KIND && doCompare(z, n, ck))
-      {
-        d_const_list_pos[tn]++;
-      }
-    }
-    if (dt[i].isSygusIdFunc())
-    {
-      d_id_funcs[tn].push_back(i);
-    }
-  }
-  // sort the constant list
-  if (!d_const_list[tn].empty())
-  {
-    if (ck != UNDEFINED_KIND)
-    {
-      sortConstants sc;
-      sc.d_comp_kind = ck;
-      std::sort(d_const_list[tn].begin(), d_const_list[tn].end(), sc);
-    }
-    Trace("csi-rcons") << "Type has " << d_const_list[tn].size()
-                       << " constants..." << std::endl
-                       << "  ";
-    for (unsigned i = 0; i < d_const_list[tn].size(); i++)
-    {
-      Trace("csi-rcons") << d_const_list[tn][i] << " ";
-    }
-    Trace("csi-rcons") << std::endl;
-    Trace("csi-rcons") << "Of these, " << d_const_list_pos[tn]
-                       << " are marked as positive." << std::endl;
-  }
-}
-
-bool CegSingleInvSol::getMatch(Node p,
-                               Node n,
-                               std::map<int, Node>& s,
-                               std::vector<int>& new_s)
-{
-  TermDbSygus* tds = d_qe->getTermDatabaseSygus();
-  if (tds->isFreeVar(p))
-  {
-    size_t vnum = tds->getFreeVarId(p);
-    Node prev = s[vnum];
-    s[vnum] = n;
-    if (prev.isNull())
-    {
-      new_s.push_back(vnum);
-    }
-    return prev.isNull() || prev == n;
-  }
-  if (n.getNumChildren() == 0)
-  {
-    return p == n;
-  }
-  if (n.getKind() == p.getKind() && n.getNumChildren() == p.getNumChildren())
-  {
-    // try both ways?
-    unsigned rmax =
-        TermUtil::isComm(n.getKind()) && n.getNumChildren() == 2 ? 2 : 1;
-    std::vector<int> new_tmp;
-    for (unsigned r = 0; r < rmax; r++)
-    {
-      bool success = true;
-      for (unsigned i = 0, size = n.getNumChildren(); i < size; i++)
-      {
-        int io = r == 0 ? i : (i == 0 ? 1 : 0);
-        if (!getMatch(p[i], n[io], s, new_tmp))
-        {
-          success = false;
-          for (unsigned j = 0; j < new_tmp.size(); j++)
-          {
-            s.erase(new_tmp[j]);
-          }
-          new_tmp.clear();
-          break;
-        }
-      }
-      if (success)
-      {
-        new_s.insert(new_s.end(), new_tmp.begin(), new_tmp.end());
-        return true;
-      }
-    }
-  }
-  return false;
-}
-
-bool CegSingleInvSol::getMatch(Node t,
-                               TypeNode st,
-                               int& index_found,
-                               std::vector<Node>& args,
-                               int index_exc,
-                               int index_start)
-{
-  Assert(st.isDatatype());
-  const DType& dt = st.getDType();
-  Assert(dt.isSygus());
-  std::map<Kind, std::vector<Node> > kgens;
-  std::vector<Node> gens;
-  for (unsigned i = index_start, ncons = dt.getNumConstructors(); i < ncons;
-       i++)
-  {
-    if ((int)i != index_exc)
-    {
-      Node g = getGenericBase(st, dt, i);
-      gens.push_back(g);
-      kgens[g.getKind()].push_back(g);
-      Trace("csi-sol-debug") << "Check generic base : " << g << " from "
-                             << dt[i].getName() << std::endl;
-      if (g.getKind() == t.getKind())
-      {
-        Trace("csi-sol-debug") << "Possible match ? " << g << " " << t
-                               << " for " << dt[i].getName() << std::endl;
-        std::map<int, Node> sigma;
-        std::vector<int> new_s;
-        if (getMatch(g, t, sigma, new_s))
-        {
-          // we found an exact match
-          bool msuccess = true;
-          for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
-          {
-            if (sigma[j].isNull())
-            {
-              msuccess = false;
-              break;
-            }
-            else
-            {
-              args.push_back(sigma[j]);
-            }
-          }
-          if (msuccess)
-          {
-            index_found = i;
-            return true;
-          }
-        }
-      }
-    }
-  }
-  return false;
-}
-
-Node CegSingleInvSol::getGenericBase(TypeNode tn, const DType& dt, int c)
-{
-  std::map<int, Node>::iterator it = d_generic_base[tn].find(c);
-  if (it != d_generic_base[tn].end())
-  {
-    return it->second;
-  }
-  TermDbSygus* tds = d_qe->getTermDatabaseSygus();
-  Assert(tds->isRegistered(tn));
-  Node g = tds->mkGeneric(dt, c);
-  Trace("csi-sol-debug") << "Generic is " << g << std::endl;
-  Node gr = Rewriter::rewrite(g);
-  Trace("csi-sol-debug") << "Generic rewritten is " << gr << std::endl;
-  d_generic_base[tn][c] = gr;
-  return gr;
-}
-
-Node CegSingleInvSol::minimizeBuiltinTerm(Node n)
-{
-  Kind nk = n.getKind();
-  if ((nk != EQUAL && nk != LEQ && nk != LT && nk != GEQ && nk != GT)
-      || !n[0].getType().isReal())
-  {
-    return n;
-  }
-  NodeManager* nm = NodeManager::currentNM();
-  bool changed = false;
-  std::vector<Node> mon[2];
-  for (unsigned r = 0; r < 2; r++)
-  {
-    unsigned ro = r == 0 ? 1 : 0;
-    Node c;
-    Node nc;
-    if (n[r].getKind() == PLUS)
-    {
-      for (unsigned i = 0; i < n[r].getNumChildren(); i++)
-      {
-        if (ArithMSum::getMonomial(n[r][i], c, nc)
-            && c.getConst<Rational>().isNegativeOne())
-        {
-          mon[ro].push_back(nc);
-          changed = true;
-        }
-        else
-        {
-          if (!n[r][i].isConst() || !n[r][i].getConst<Rational>().isZero())
-          {
-            mon[r].push_back(n[r][i]);
-          }
-        }
-      }
-    }
-    else
-    {
-      if (ArithMSum::getMonomial(n[r], c, nc)
-          && c.getConst<Rational>().isNegativeOne())
-      {
-        mon[ro].push_back(nc);
-        changed = true;
-      }
-      else
-      {
-        if (!n[r].isConst() || !n[r].getConst<Rational>().isZero())
-        {
-          mon[r].push_back(n[r]);
-        }
-      }
-    }
-  }
-  if (changed)
-  {
-    Node nn[2];
-    for (unsigned r = 0; r < 2; r++)
-    {
-      nn[r] = mon[r].size() == 0
-                  ? nm->mkConst(Rational(0))
-                  : (mon[r].size() == 1 ? mon[r][0] : nm->mkNode(PLUS, mon[r]));
-    }
-    return nm->mkNode(n.getKind(), nn[0], nn[1]);
-  }
-  return n;
-}
-
-Kind CegSingleInvSol::getComparisonKind(TypeNode tn)
-{
-  if (tn.isInteger() || tn.isReal())
-  {
-    return LT;
-  }
-  else if (tn.isBitVector())
-  {
-    return BITVECTOR_ULT;
-  }
-  return UNDEFINED_KIND;
-}
-
-Kind CegSingleInvSol::getPlusKind(TypeNode tn, bool is_neg)
-{
-  if (tn.isInteger() || tn.isReal())
-  {
-    return is_neg ? MINUS : PLUS;
-  }
-  else if (tn.isBitVector())
-  {
-    return is_neg ? BITVECTOR_SUB : BITVECTOR_PLUS;
-  }
-  return UNDEFINED_KIND;
-}
-}
-}
-}
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
deleted file mode 100644
index 9aec30049..000000000
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
+++ /dev/null
@@ -1,205 +0,0 @@
-/*********************                                                        */
-/*! \file ce_guided_single_inv_sol.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief 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 <map>
-#include <vector>
-
-#include "context/cdhashmap.h"
-#include "expr/dtype.h"
-#include "expr/node.h"
-
-namespace CVC4 {
-namespace theory {
-
-class QuantifiersEngine;
-
-namespace quantifiers {
-
-class CegSingleInv;
-
-/** CegSingleInvSol
- *
- * This function implements Figure 5 of "Counterexample-Guided Quantifier
- * Instantiation for Synthesis in SMT", Reynolds et al CAV 2015.
- *
- */
-class CegSingleInvSol
-{
-  friend class CegSingleInv;
-
- private:
-  QuantifiersEngine * d_qe;
-  std::vector< Node > d_varList;
-  std::map< Node, int > d_dterm_size;
-  std::map< Node, int > d_dterm_ite_size;
-
- public:
-  CegSingleInvSol(QuantifiersEngine* qe);
-  /** reconstruct solution
-   *
-   * Returns (if possible) a node that is equivalent to sol those syntax
-   * matches the grammar corresponding to sygus datatype stn.
-   * The value reconstructed is set to 1 if we successfully return a node,
-   * otherwise it is set to -1.
-   *
-   * This method quickly tries to match sol to the grammar induced by stn. If
-   * this fails, we use enumerative techniques to try to repair the solution.
-   * The number of iterations for this enumeration is bounded by the argument
-   * enumLimit if it is positive, and unbounded otherwise.
-   */
-  Node reconstructSolution(Node sol,
-                           TypeNode stn,
-                           int& reconstructed,
-                           int enumLimit);
-  /** preregister conjecture
-   *
-   * q : the synthesis conjecture this class is for.
-   * This is used as a heuristic to find terms in the original conjecture which
-   * may be helpful for using during reconstruction.
-   */
-  void preregisterConjecture(Node q);
-
- 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;
-  
-  //equivalent terms
-  std::map< Node, Node > d_eqt_rep;
-  std::map< Node, std::vector< Node > > d_eqt_eqc;
-
-  //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 DTypeConstructor& dtc,
-                               std::vector<int>& ids,
-                               int& status);
-  bool getPathToRoot( int id );
-  void setReconstructed( int id, Node n );
-  //get equivalent terms to n with top symbol k
-  void getEquivalentTerms( Kind k, Node n, std::vector< Node >& equiv );
-  //register equivalent terms
-  void registerEquivalentTerms( Node n );
-  /** builtin to sygus const
-   *
-   * Returns a sygus term of type tn that encodes the builtin constant c.
-   * If the sygus datatype tn allows any constant, this may return a variable
-   * with the attribute SygusPrintProxyAttribute that associates it with c.
-   *
-   * rcons_depth limits the number of recursive calls when doing accelerated
-   * constant reconstruction (currently limited to 1000). Notice this is hacky:
-   * depending upon order of calls, constant rcons may succeed, e.g. 1001, 999
-   * vs. 999, 1001.
-   */
-  Node builtinToSygusConst(Node c, TypeNode tn, int rcons_depth = 0);
-  /** cache for the above function */
-  std::map<TypeNode, std::map<Node, Node> > d_builtin_const_to_sygus;
-  /** sorted list of constants, per type */
-  std::map<TypeNode, std::vector<Node> > d_const_list;
-  /** number of positive constants, per type */
-  std::map<TypeNode, unsigned> d_const_list_pos;
-  /** list of constructor indices whose operators are identity functions */
-  std::map<TypeNode, std::vector<int> > d_id_funcs;
-  /** initialize the above information for sygus type tn */
-  void registerType(TypeNode tn);
-  /** get generic base
-   *
-   * This returns the builtin term that is the analog of an application of the
-   * c^th constructor of dt to fresh variables.
-   */
-  Node getGenericBase(TypeNode tn, const DType& dt, int c);
-  /** cache for the above function */
-  std::map<TypeNode, std::map<int, Node> > d_generic_base;
-  /** get match
-   *
-   * This function attempts to find a substitution for which p = n. If
-   * successful, this function returns a substitution in the form of s/new_s,
-   * where:
-   * s : substitution, where the domain are indices of terms in the sygus
-   * term database, and
-   * new_s : the members that were added to s on this call.
-   * Otherwise, this function returns false and s and new_s are unmodified.
-   */
-  bool getMatch(Node p,
-                Node n,
-                std::map<int, Node>& s,
-                std::vector<int>& new_s);
-  /** get match
-   *
-   * This function attempts to find a builtin term that is analog to a value
-   * of the sygus datatype st that is equivalent to n. If this function returns
-   * true, then it has found such a term. Then we set:
-   *   index_found : updated to the constructor index of the sygus term whose
-   *   analog to equivalent to n.
-   *   args : builtin terms corresponding to the match, in order.
-   * Otherwise, this function returns false and index_found and args are
-   * unmodified.
-   * For example, for grammar:
-   *   A -> 0 | 1 | x | +( A, A )
-   * Given input ( 5 + (x+1) ) and A we would return true, where:
-   *   index_found is set to 3 and args is set to { 5, x+1 }.
-   *
-   * index_exc : (if applicable) exclude a constructor index of st
-   * index_start : start index of constructors of st to try
-   */
-  bool getMatch(Node n,
-                TypeNode st,
-                int& index_found,
-                std::vector<Node>& args,
-                int index_exc = -1,
-                int index_start = 0);
-  /** given a term, construct an equivalent smaller one that respects syntax */
-  Node minimizeBuiltinTerm(Node n);
-  /**
-   * Return the kind of "is less than" for type tn, where tn is either Int or
-   * BV.
-   */
-  static Kind getComparisonKind(TypeNode tn);
-  /**
-   * Return the kind of "plus" for type tn, or "minus" if is_neg is true, where
-   * tn is either Int or BV.
-   */
-  static Kind getPlusKind(TypeNode tn, bool is_neg = false);
-};
-
-
-}
-}
-}
-
-#endif
diff --git a/src/theory/quantifiers/sygus/rcons_obligation_info.cpp b/src/theory/quantifiers/sygus/rcons_obligation_info.cpp
new file mode 100644
index 000000000..25aac1e93
--- /dev/null
+++ b/src/theory/quantifiers/sygus/rcons_obligation_info.cpp
@@ -0,0 +1,100 @@
+/*********************                                                        */
+/*! \file rcons_obligation_info.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Abdalrhman Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Reconstruct Obligation Info class implementation
+ **/
+
+#include "rcons_obligation_info.h"
+
+#include "expr/node_algorithm.h"
+#include "theory/datatypes/sygus_datatype_utils.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+RConsObligationInfo::RConsObligationInfo(Node builtin) : d_builtin(builtin) {}
+
+Node RConsObligationInfo::getBuiltin() const { return d_builtin; }
+
+void RConsObligationInfo::addCandidateSolution(Node candSol)
+{
+  d_candSols.emplace(candSol);
+}
+
+const std::unordered_set<Node, NodeHashFunction>&
+RConsObligationInfo::getCandidateSolutions() const
+{
+  return d_candSols;
+}
+
+void RConsObligationInfo::addCandidateSolutionToWatchSet(Node candSol)
+{
+  d_watchSet.emplace(candSol);
+}
+
+const std::unordered_set<Node, NodeHashFunction>&
+RConsObligationInfo::getWatchSet() const
+{
+  return d_watchSet;
+}
+
+std::string RConsObligationInfo::obToString(Node k,
+                                            const RConsObligationInfo& obInfo)
+{
+  return "ob<" + obInfo.getBuiltin().toString() + ", " + k.getType().toString()
+         + ">";
+}
+
+void RConsObligationInfo::printCandSols(
+    const Node& root,
+    const std::unordered_map<Node, RConsObligationInfo, NodeHashFunction>&
+        obInfo)
+{
+  std::unordered_set<Node, NodeHashFunction> visited;
+  std::vector<Node> stack;
+  stack.push_back(root);
+
+  Trace("sygus-rcons") << "\nEq classes: \n[";
+
+  while (!stack.empty())
+  {
+    const Node& k = stack.back();
+    stack.pop_back();
+    visited.emplace(k);
+
+    Trace("sygus-rcons") << std::endl
+                         << datatypes::utils::sygusToBuiltin(k) << " "
+                         << obToString(k, obInfo.at(k)) << ":\n [";
+
+    for (const Node& j : obInfo.at(k).getCandidateSolutions())
+    {
+      Trace("sygus-rcons") << datatypes::utils::sygusToBuiltin(j) << " ";
+      std::unordered_set<TNode, TNodeHashFunction> subObs;
+      expr::getVariables(j, subObs);
+      for (const TNode& l : subObs)
+      {
+        if (visited.find(l) == visited.cend()
+            && obInfo.find(l) != obInfo.cend())
+        {
+          stack.push_back(l);
+        }
+      }
+    }
+    Trace("sygus-rcons") << "]" << std::endl;
+  }
+
+  Trace("sygus-rcons") << "]" << std::endl;
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/sygus/rcons_obligation_info.h b/src/theory/quantifiers/sygus/rcons_obligation_info.h
new file mode 100644
index 000000000..5ebddd794
--- /dev/null
+++ b/src/theory/quantifiers/sygus/rcons_obligation_info.h
@@ -0,0 +1,150 @@
+/*********************                                                        */
+/*! \file rcons_obligation_info.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Abdalrhman Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief utility class for Sygus Reconstruct module
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H
+#define CVC4__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/**
+ * A utility class for Sygus Reconstruct obligations. An obligation is a builtin
+ * term t and a SyGuS type T, and indicates that we are trying to build a term
+ * of type T whose builtin analog is equivalent to t. The main algorithm encodes
+ * each obligation (t, T) as a skolem k of type T to embed obligations in
+ * candidate solutions (see d_candSols below). It mainly operates over skolems
+ * and stores cooresponding builtin terms and other info in instances of this
+ * class. Notice that the SyGuS type T of an obligation is not stored in this
+ * class as it can be inferred from the type of the skolem k.
+ */
+class RConsObligationInfo
+{
+ public:
+  /**
+   * Constructor. Default value needed for maps.
+   *
+   * @param builtin builtin term to reconstruct
+   */
+  explicit RConsObligationInfo(Node builtin = Node::null());
+
+  /**
+   * @return builtin term to reconstruct for this class' obligation
+   */
+  Node getBuiltin() const;
+
+  /**
+   * Add candidate solution to the set of candidate solutions for the
+   * corresponding obligation.
+   *
+   * @param candSol the candidate solution to add
+   */
+  void addCandidateSolution(Node candSol);
+
+  /**
+   * @return set of candidate solutions for this class' obligation
+   */
+  const std::unordered_set<Node, NodeHashFunction>& getCandidateSolutions()
+      const;
+
+  /**
+   * Add candidate solution to the set of candidate solutions waiting for the
+   * corresponding obligation to be solved.
+   *
+   * @param candSol the candidate solution to add to watch set
+   */
+  void addCandidateSolutionToWatchSet(Node candSol);
+
+  /**
+   * @return set of candidate solutions waiting for this class' obligation
+   * to be solved
+   */
+  const std::unordered_set<Node, NodeHashFunction>& getWatchSet() const;
+
+  /**
+   * Return a string representation of an obligation.
+   *
+   * @param k An obligation
+   * @param obInfo Obligation `k`'s info
+   * @return A string representation of `k`
+   */
+  static std::string obToString(Node k, const RConsObligationInfo& obInfo);
+
+  /**
+   * Print all reachable obligations and their candidate solutions from
+   * the `root` obligation and its candidate solutions.
+   *
+   * An obligation is reachable from the `root` obligation if it is the `root`
+   * obligation or is needed by one of the candidate solutions of other
+   * reachable obligations.
+   *
+   * For example, if we have:
+   *
+   * Obs = {c_z1, c_z2, c_z3, c_z4} // list of obligations in rcons algorithm
+   * CandSols = {c_z1 -> {(c_+ c_1 c_z2)}, c_z2 -> {(c_- c_z3)},
+   *             c_z3 -> {c_x}, c_z4 -> {}}
+   * root = c_z1
+   *
+   * Then, the set of reachable obligations from `root` is {c_z1, c_z2, c_z3}
+   *
+   * \note requires enabling "sygus-rcons" trace
+   *
+   * @param root The root obligation to start from
+   * @param obInfo a map from obligations to their corresponding infos
+   */
+  static void printCandSols(
+      const Node& root,
+      const std::unordered_map<Node, RConsObligationInfo, NodeHashFunction>&
+          obInfo);
+
+ private:
+  /** Builtin term for this class' obligation.
+   *
+   * To solve the obligation, this builtin term must be reconstructed in the
+   * specified grammar (sygus datatype type) of this class' obligation.
+   */
+  Node d_builtin;
+  /** A set of candidate solutions to this class' obligation.
+   *
+   * Each candidate solution is a sygus datatype term containing skolem subterms
+   * (sub-obligations). By replacing all sub-obligations with their
+   * corresponding solutions, we get a term whose builtin analog rewrites to
+   * `d_builtin` and hence solves this obligation. For example, given:
+   *   d_builtin = (+ x y)
+   * a possible set of candidate solutions would be:
+   *   d_candSols = {(c_+ c_z1 c_z2), (c_+ c_x c_z2), (c_+ c_z1 c_y),
+   *                 (c_+ c_x c_y)}
+   * where c_z1 and c_z2 are skolems. Notice that `d_candSols` may contain a
+   * pure term that solves the obligation ((c_+ c_x c_y) in this example).
+   */
+  std::unordered_set<Node, NodeHashFunction> d_candSols;
+  /** A set of candidate solutions waiting for this class' obligation to
+   * be solved.
+   *
+   * In the example above, (c_+ c_z1 c_z2) and (c_+ c_x c_z2) are in
+   * the watch-set of c_z2. Similarly, (c_+ c_z1 c_z2) and (c_+ c_z1 c_y) are in
+   * the watch-set of c_z1.
+   */
+  std::unordered_set<Node, NodeHashFunction> d_watchSet;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif  // CVC4__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H
diff --git a/src/theory/quantifiers/sygus/rcons_type_info.cpp b/src/theory/quantifiers/sygus/rcons_type_info.cpp
new file mode 100644
index 000000000..d24c4d25d
--- /dev/null
+++ b/src/theory/quantifiers/sygus/rcons_type_info.cpp
@@ -0,0 +1,72 @@
+/*********************                                                        */
+/*! \file rcons_type_info.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Abdalrhman Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Reconstruct Type Info class implementation
+ **/
+
+#include "theory/quantifiers/sygus/rcons_type_info.h"
+
+#include "theory/datatypes/sygus_datatype_utils.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+void RConsTypeInfo::initialize(TermDbSygus* tds,
+                               SygusStatistics& s,
+                               TypeNode stn,
+                               const std::vector<Node>& builtinVars)
+{
+  NodeManager* nm = NodeManager::currentNM();
+
+  d_enumerator.reset(new SygusEnumerator(tds, nullptr, s, true));
+  d_enumerator->initialize(nm->mkSkolem("sygus_rcons", stn));
+  d_crd.reset(new CandidateRewriteDatabase(true, false, true, false));
+  // since initial samples are not always useful for equivalence checks, set
+  // their number to 0
+  d_sygusSampler.initialize(stn, builtinVars, 0);
+  d_crd->initialize(builtinVars, &d_sygusSampler);
+}
+
+Node RConsTypeInfo::nextEnum()
+{
+  if (!d_enumerator->increment())
+  {
+    Trace("sygus-rcons") << "no increment" << std::endl;
+    return Node::null();
+  }
+
+  Node sz = d_enumerator->getCurrent();
+
+  Trace("sygus-rcons") << (sz == Node::null()
+                               ? sz
+                               : datatypes::utils::sygusToBuiltin(sz))
+                       << std::endl;
+
+  return sz;
+}
+
+Node RConsTypeInfo::addTerm(Node n)
+{
+  std::stringstream out;
+  return d_crd->addTerm(n, false, out);
+}
+
+void RConsTypeInfo::setBuiltinToOb(Node builtin, Node ob)
+{
+  d_ob[builtin] = ob;
+}
+
+Node RConsTypeInfo::builtinToOb(Node builtin) { return d_ob[builtin]; }
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/sygus/rcons_type_info.h b/src/theory/quantifiers/sygus/rcons_type_info.h
new file mode 100644
index 000000000..432d07687
--- /dev/null
+++ b/src/theory/quantifiers/sygus/rcons_type_info.h
@@ -0,0 +1,102 @@
+/*********************                                                        */
+/*! \file rcons_type_info.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Abdalrhman Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief utility class for Sygus Reconstruct module
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H
+#define CVC4__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H
+
+#include "theory/quantifiers/sygus/sygus_enumerator.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/**
+ * A utility class for Sygus Reconstruct datatype types (grammar non-terminals).
+ * This class is mainly responsible for enumerating sygus datatype type terms
+ * and building sets of equivalent builtin terms for the rcons algorithm.
+ */
+class RConsTypeInfo
+{
+ public:
+  /**
+   * Initialize a sygus enumerator and a candidate rewrite database for this
+   * class' sygus datatype type.
+   *
+   * @param tds Database for sygus terms
+   * @param s Statistics managed for the synth engine
+   * @param stn The sygus datatype type encoding the syntax restrictions
+   * @param builtinVars A list containing the builtin analog of sygus variable
+   *                    list for the sygus datatype type
+   */
+  void initialize(TermDbSygus* tds,
+                  SygusStatistics& s,
+                  TypeNode stn,
+                  const std::vector<Node>& builtinVars);
+
+  /**
+   * Returns the next enumerated term for the given sygus datatype type.
+   *
+   * @return The enumerated sygus term
+   */
+  Node nextEnum();
+
+  /**
+   * Add a pure term to the candidate rewrite database.
+   *
+   * @param n The term to add to the database
+   * @return A previous term `eq_n` added to this class, such that `n` is
+   * equivalent to `eq_n`. If no previous term equivalent to `n` exists then the
+   * result is `n` itself
+   */
+  Node addTerm(Node n);
+
+  /**
+   * Set the obligation responsible for solving the given builtin term.
+   *
+   * @param builtin The builtin term
+   * @param ob The corresponding obligation
+   */
+  void setBuiltinToOb(Node builtin, Node ob);
+
+  /**
+   * Return the obligation responsible for solving the given builtin term.
+   *
+   * @param builtin The builtin term
+   * @return The corresponding obligation
+   */
+  Node builtinToOb(Node builtin);
+
+ private:
+  /** Sygus terms enumerator for this class' Sygus datatype type */
+  std::unique_ptr<SygusEnumerator> d_enumerator;
+  /** Candidate rewrite database for this class' sygus datatype type */
+  std::unique_ptr<CandidateRewriteDatabase> d_crd;
+  /** Sygus sampler needed for initializing the candidate rewrite database */
+  SygusSampler d_sygusSampler;
+  /** A map from a builtin term to its obligation.
+   *
+   * Each sygus datatype type has its own version of this map because it is
+   * possible to have multiple obligations to reconstruct the same builtin term
+   * from different sygus datatype types.
+   */
+  std::unordered_map<Node, Node, NodeHashFunction> d_ob;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif  // CVC4__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H
diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
new file mode 100644
index 000000000..bd0f7c4dd
--- /dev/null
+++ b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
@@ -0,0 +1,491 @@
+/*********************                                                        */
+/*! \file sygus_reconstruct.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Abdalrhman Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief implementation for reconstruct
+ **/
+
+#include "theory/quantifiers/sygus/sygus_reconstruct.h"
+
+#include "expr/node_algorithm.h"
+#include "smt/command.h"
+#include "theory/datatypes/sygus_datatype_utils.h"
+#include "theory/rewriter.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+SygusReconstruct::SygusReconstruct(TermDbSygus* tds, SygusStatistics& s)
+    : d_tds(tds), d_stats(s)
+{
+}
+
+Node SygusReconstruct::reconstructSolution(Node sol,
+                                           TypeNode stn,
+                                           int8_t& reconstructed,
+                                           uint64_t enumLimit)
+{
+  Trace("sygus-rcons") << "SygusReconstruct::reconstructSolution: " << sol
+                       << std::endl;
+  Trace("sygus-rcons") << "- target sygus type is " << stn << std::endl;
+  Trace("sygus-rcons") << "- enumeration limit is " << enumLimit << std::endl;
+
+  // this method may get called multiple times with the same object. We need to
+  // reset the state to avoid conflicts
+  clear();
+
+  initialize(stn);
+
+  NodeManager* nm = NodeManager::currentNM();
+
+  /** a set of obligations that are not yet satisfied for each sygus datatype */
+  TypeObligationSetMap unsolvedObs;
+
+  // paramaters sol and stn constitute the main obligation to satisfy
+  Node mainOb = nm->mkSkolem("sygus_rcons", stn);
+
+  // add the main obligation to the set of obligations that are not yet
+  // satisfied
+  unsolvedObs[stn].emplace(mainOb);
+  d_obInfo.emplace(mainOb, RConsObligationInfo(sol));
+  d_stnInfo[stn].setBuiltinToOb(sol, mainOb);
+
+  // We need to add the main obligation to the crd in case it cannot be broken
+  // down by matching. By doing so, we can solve the obligation using
+  // enumeration and crd (if it is in the grammar)
+  d_stnInfo[stn].addTerm(sol);
+
+  // the set of unique (up to rewriting) patterns/shapes in the grammar used by
+  // matching
+  std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction> pool;
+
+  uint64_t count = 0;
+
+  // algorithm
+  while (d_sol[mainOb].isNull() && count < enumLimit)
+  {
+    // enumeration phase
+    // a temporary set of new obligations cached for processing in the match
+    // phase
+    TypeObligationSetMap obsPrime;
+    for (const std::pair<const TypeNode, ObligationSet>& pair : unsolvedObs)
+    {
+      // enumerate a new term
+      Trace("sygus-rcons") << "enum: " << stn << ": ";
+      Node sz = d_stnInfo[pair.first].nextEnum();
+      if (sz.isNull())
+      {
+        continue;
+      }
+      Node builtin = Rewriter::rewrite(datatypes::utils::sygusToBuiltin(sz));
+      // if enumerated term does not contain free variables, then its
+      // corresponding obligation can be solved immediately
+      if (sz.isConst())
+      {
+        Node rep = d_stnInfo[pair.first].addTerm(builtin);
+        Node k = d_stnInfo[pair.first].builtinToOb(rep);
+        // check if the enumerated term solves an obligation
+        if (k.isNull())
+        {
+          // if not, create an "artifical" obligation whose solution would be
+          // the enumerated term
+          k = nm->mkSkolem("sygus_rcons", pair.first);
+          d_obInfo.emplace(k, RConsObligationInfo(builtin));
+          d_stnInfo[pair.first].setBuiltinToOb(builtin, k);
+        }
+        // mark the obligation as solved
+        markSolved(k, sz);
+        // Since we added the term to the candidate rewrite database, there is
+        // no point in adding it to the pool too
+        continue;
+      }
+      // if there are no matches (all calls to notify return true)...
+      if (d_poolTrie.getMatches(builtin, this))
+      {
+        // then, this is a new term and we should add it to pool
+        d_poolTrie.addTerm(builtin);
+        pool[pair.first].push_back(sz);
+        for (Node k : pair.second)
+        {
+          if (d_sol[k].isNull())
+          {
+            Trace("sygus-rcons")
+                << "ob: " << RConsObligationInfo::obToString(k, d_obInfo[k])
+                << std::endl;
+            // try to match obligation k with the enumerated term sz
+            TypeObligationSetMap temp = matchNewObs(k, sz);
+            // cache the new obligations for processing in the match phase
+            for (const std::pair<const TypeNode, ObligationSet>& tempPair :
+                 temp)
+            {
+              obsPrime[tempPair.first].insert(tempPair.second.cbegin(),
+                                              tempPair.second.cend());
+            }
+          }
+        }
+      }
+    }
+    // match phase
+    while (!obsPrime.empty())
+    {
+      // a temporary set of new obligations cached for later processing
+      TypeObligationSetMap obsDPrime;
+      for (const std::pair<const TypeNode, ObligationSet>& pair : obsPrime)
+      {
+        for (const Node& k : pair.second)
+        {
+          unsolvedObs[pair.first].emplace(k);
+          if (d_sol[k].isNull())
+          {
+            Trace("sygus-rcons")
+                << "ob: " << RConsObligationInfo::obToString(k, d_obInfo[k])
+                << std::endl;
+            for (Node sz : pool[pair.first])
+            {
+              // try to match each newly generated and cached obligation
+              // with patterns in pool
+              TypeObligationSetMap temp = matchNewObs(k, sz);
+              // cache the new obligations for later processing
+              for (const std::pair<const TypeNode, ObligationSet>& tempPair :
+                   temp)
+              {
+                obsDPrime[tempPair.first].insert(tempPair.second.cbegin(),
+                                                 tempPair.second.cend());
+              }
+            }
+          }
+        }
+      }
+      obsPrime = std::move(obsDPrime);
+    }
+    // remove solved obligations from unsolvedObs
+    removeSolvedObs(unsolvedObs);
+    ++count;
+  }
+
+  if (Trace("sygus-rcons").isConnected())
+  {
+    RConsObligationInfo::printCandSols(mainOb, d_obInfo);
+    printPool(pool);
+  }
+
+  // if the main obligation is solved, return the solution
+  if (!d_sol[mainOb].isNull())
+  {
+    reconstructed = 1;
+    // The algorithm mostly works with rewritten terms and may not notice that
+    // the original terms contain variables eliminated by the rewriter. For
+    // example, rewrite((ite true 0 z)) = 0. In such cases, we replace those
+    // variables with ground values.
+    return d_sol[mainOb].isConst() ? Node(d_sol[mainOb])
+                                   : mkGround(d_sol[mainOb]);
+  }
+
+  // we ran out of elements, return null
+  reconstructed = -1;
+  Warning() << CommandFailure(
+      "Cannot get synth function: reconstruction to syntax failed.");
+  return d_sol[mainOb];
+}
+
+TypeObligationSetMap SygusReconstruct::matchNewObs(Node k, Node sz)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  TypeObligationSetMap obsPrime;
+
+  // obligations generated by match. Note that we might have already seen (and
+  // even solved) those obligations, hence the name "candidate obligations"
+  std::unordered_map<Node, Node, NodeHashFunction> candObs;
+  // the builtin terms corresponding to sygus variables in the grammar are bound
+  // variables. However, we want the `match` method to treat them as ground
+  // terms. So, we add redundant substitutions
+  candObs.insert(d_sygusVars.cbegin(), d_sygusVars.cend());
+
+  // try to match the obligation's builtin term with the pattern sz
+  if (expr::match(Rewriter::rewrite(datatypes::utils::sygusToBuiltin(sz)),
+                  d_obInfo[k].getBuiltin(),
+                  candObs))
+  {
+    // the bound variables z generated by the enumerators are reused across
+    // enumerated terms, so we need to replace them with our own skolems
+    std::vector<std::pair<Node, Node>> subs;
+    Trace("sygus-rcons") << "-- ct: " << sz << std::endl;
+    // remove redundant substitutions
+    for (const std::pair<const Node, Node>& pair : d_sygusVars)
+    {
+      candObs.erase(pair.first);
+    }
+    // for each candidate obligation
+    for (const std::pair<const Node, Node>& candOb : candObs)
+    {
+      TypeNode stn =
+          datatypes::utils::builtinVarToSygus(candOb.first).getType();
+      Node newVar;
+      // have we come across a similar obligation before?
+      Node rep = d_stnInfo[stn].addTerm(candOb.second);
+      if (!d_stnInfo[stn].builtinToOb(rep).isNull())
+      {
+        // if so, use the original obligation
+        newVar = d_stnInfo[stn].builtinToOb(rep);
+      }
+      else
+      {
+        // otherwise, create a new obligation of the corresponding sygus type
+        newVar = nm->mkSkolem("sygus_rcons", stn);
+        d_obInfo.emplace(newVar, candOb.second);
+        d_stnInfo[stn].setBuiltinToOb(candOb.second, newVar);
+        // if the candidate obligation is a constant and the grammar allows
+        // random constants
+        if (candOb.second.isConst()
+            && k.getType().getDType().getSygusAllowConst())
+        {
+          // then immediately solve the obligation
+          markSolved(newVar, d_tds->getProxyVariable(stn, candOb.second));
+        }
+        else
+        {
+          // otherwise, add this candidate obligation to this list of
+          // obligations
+          obsPrime[stn].emplace(newVar);
+        }
+      }
+      subs.emplace_back(datatypes::utils::builtinVarToSygus(candOb.first),
+                        newVar);
+    }
+    // replace original free vars in sz with new ones
+    if (!subs.empty())
+    {
+      sz = sz.substitute(subs.cbegin(), subs.cend());
+    }
+    // sz is solved if it has no sub-obligations or if all of them are solved
+    bool isSolved = true;
+    for (const std::pair<Node, Node>& sub : subs)
+    {
+      if (d_sol[sub.second].isNull())
+      {
+        isSolved = false;
+        d_subObs[sz].push_back(sub.second);
+      }
+    }
+
+    if (isSolved)
+    {
+      Node s = sz.substitute(d_sol);
+      markSolved(k, s);
+    }
+    else
+    {
+      // add sz as a possible solution to obligation k
+      d_obInfo[k].addCandidateSolution(sz);
+      d_parentOb[sz] = k;
+      d_obInfo[d_subObs[sz].back()].addCandidateSolutionToWatchSet(sz);
+    }
+  }
+
+  return obsPrime;
+}
+
+void SygusReconstruct::markSolved(Node k, Node s)
+{
+  // return if obligation k is already solved
+  if (!d_sol[k].isNull())
+  {
+    return;
+  }
+
+  Trace("sygus-rcons") << "sol: " << s << std::endl;
+  Trace("sygus-rcons") << "builtin sol: " << datatypes::utils::sygusToBuiltin(s)
+                       << std::endl;
+
+  // First, mark `k` as solved
+  d_obInfo[k].addCandidateSolution(s);
+  d_sol[k] = s;
+  d_parentOb[s] = k;
+
+  std::vector<Node> stack;
+  stack.push_back(k);
+
+  while (!stack.empty())
+  {
+    Node curr = stack.back();
+    stack.pop_back();
+
+    // for each partial solution/parent of the now solved obligation `curr`
+    for (Node parent : d_obInfo[curr].getWatchSet())
+    {
+      // remove `curr` and (possibly) other solved obligations from its list
+      // of children
+      while (!d_subObs[parent].empty()
+             && !d_sol[d_subObs[parent].back()].isNull())
+      {
+        d_subObs[parent].pop_back();
+      }
+
+      // if the partial solution does not have any more children...
+      if (d_subObs[parent].empty())
+      {
+        // then it is completely solved and can be used as a solution of its
+        // corresponding obligation
+        Node parentSol = parent.substitute(d_sol);
+        Node parentOb = d_parentOb[parent];
+        // proceed only if parent obligation is not already solved
+        if (d_sol[parentOb].isNull())
+        {
+          d_obInfo[parentOb].addCandidateSolution(parentSol);
+          d_sol[parentOb] = parentSol;
+          d_parentOb[parentSol] = parentOb;
+          // repeat the same process for the parent obligation
+          stack.push_back(parentOb);
+        }
+      }
+      else
+      {
+        // if it does have remaining children, add it to the watch list of one
+        // of them (picked arbitrarily)
+        d_obInfo[d_subObs[parent].back()].addCandidateSolutionToWatchSet(
+            parent);
+      }
+    }
+  }
+}
+
+void SygusReconstruct::initialize(TypeNode stn)
+{
+  std::vector<Node> builtinVars;
+
+  // Cache the sygus variables introduced by the problem (which we treat as
+  // ground terms when calling the `match` method) as opposed to the sygus
+  // variables introduced by the enumerators (which we treat as bound
+  // variables).
+  for (Node sv : stn.getDType().getSygusVarList())
+  {
+    builtinVars.push_back(datatypes::utils::sygusToBuiltin(sv));
+    d_sygusVars.emplace(datatypes::utils::sygusToBuiltin(sv),
+                        datatypes::utils::sygusToBuiltin(sv));
+  }
+
+  SygusTypeInfo stnInfo;
+  stnInfo.initialize(d_tds, stn);
+
+  // find the non-terminals of the grammar
+  std::vector<TypeNode> sfTypes;
+  stnInfo.getSubfieldTypes(sfTypes);
+
+  // initialize the enumerators and candidate rewrite databases. Notice here
+  // that we treat the sygus variables introduced by the problem as bound
+  // variables (needed for making sure that obligations are equal). This is fine
+  // as we will never add variables that were introduced by the enumerators to
+  // the database.
+  for (TypeNode tn : sfTypes)
+  {
+    d_stnInfo[tn].initialize(d_tds, d_stats, tn, builtinVars);
+  }
+}
+
+void SygusReconstruct::removeSolvedObs(TypeObligationSetMap& unsolvedObs)
+{
+  for (std::pair<const TypeNode, ObligationSet>& tempPair : unsolvedObs)
+  {
+    ObligationSet::iterator it = tempPair.second.begin();
+    while (it != tempPair.second.end())
+    {
+      if (d_sol[*it].isNull())
+      {
+        ++it;
+      }
+      else
+      {
+        it = tempPair.second.erase(it);
+      }
+    }
+  }
+}
+
+Node SygusReconstruct::mkGround(Node n) const
+{
+  // get the set of bound variables in n
+  std::unordered_set<TNode, TNodeHashFunction> vars;
+  expr::getVariables(n, vars);
+
+  std::unordered_map<TNode, TNode, TNodeHashFunction> subs;
+
+  // generate a ground value for each one of those variables
+  for (const TNode& var : vars)
+  {
+    subs.emplace(var, var.getType().mkGroundValue());
+  }
+
+  // substitute the variables with ground values
+  return n.substitute(subs);
+}
+
+bool SygusReconstruct::notify(Node s,
+                              Node n,
+                              std::vector<Node>& vars,
+                              std::vector<Node>& subs)
+{
+  for (size_t i = 0; i < vars.size(); ++i)
+  {
+    // We consider sygus variables as ground terms. So, if they are not equal to
+    // their substitution, then s is not matchable with n and we try the next
+    // term s. Example: If s = (+ z x) and n = (+ z y), then s is not matchable
+    // with n and we return true
+    if (d_sygusVars.find(vars[i]) != d_sygusVars.cend() && vars[i] != subs[i])
+    {
+      return true;
+    }
+  }
+  // Note: false here means that we finally found an s that is matchable with n,
+  // so we should not add n to the pool
+  return false;
+}
+
+void SygusReconstruct::clear()
+{
+  d_obInfo.clear();
+  d_stnInfo.clear();
+  d_sol.clear();
+  d_subObs.clear();
+  d_parentOb.clear();
+  d_sygusVars.clear();
+  d_poolTrie.clear();
+}
+
+void SygusReconstruct::printPool(
+    const std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction>&
+        pool) const
+{
+  Trace("sygus-rcons") << "\nPool:\n[";
+
+  for (const std::pair<const TypeNode, std::vector<Node>>& pair : pool)
+  {
+    Trace("sygus-rcons") << std::endl << pair.first << ":\n[" << std::endl;
+
+    for (const Node& sygusTerm : pair.second)
+    {
+      Trace("sygus-rcons") << "  "
+                           << Rewriter::rewrite(
+                                  datatypes::utils::sygusToBuiltin(sygusTerm))
+                                  .toString()
+                           << std::endl;
+    }
+
+    Trace("sygus-rcons") << "]" << std::endl;
+  }
+
+  Trace("sygus-rcons") << "]" << std::endl;
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.h b/src/theory/quantifiers/sygus/sygus_reconstruct.h
new file mode 100644
index 000000000..2d55c3f3d
--- /dev/null
+++ b/src/theory/quantifiers/sygus/sygus_reconstruct.h
@@ -0,0 +1,312 @@
+/*********************                                                        */
+/*! \file sygus_reconstruct.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Abdalrhman Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief utility for reconstructing terms to match a grammar
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H
+
+#include <map>
+#include <vector>
+
+#include "theory/quantifiers/sygus/rcons_obligation_info.h"
+#include "theory/quantifiers/sygus/rcons_type_info.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+using ObligationSet = std::unordered_set<Node, NodeHashFunction>;
+using TypeObligationSetMap =
+    std::unordered_map<TypeNode, ObligationSet, TypeNodeHashFunction>;
+
+/** SygusReconstruct
+ *
+ * This class implements an algorithm for reconstructing a given term such that
+ * the reconstructed term is equivalent to the original term and its syntax
+ * matches a specified grammar.
+ *
+ * Goal: find a term g in sygus type T_0 that is equivalent to builtin term t_0.
+ *
+ * rcons(t_0, T_0) returns g
+ * {
+ *   Obs: A map from sygus types T to a set of triples to reconstruct into T,
+ *        where each triple is of the form (k, t, s), where k is a skolem of
+ *        type T, t is a builtin term of the type encoded by T, and s is a
+ *        possibly null sygus term of type T representing the solution.
+ *
+ *   Sol: A map from skolems k to solutions s in the triples (k, t, s). That is,
+ *        Sol[k] = s.
+ *
+ *   CandSols : A map from a skolem k to a set of possible solutions for its
+ *              corresponding obligation. Whenever there is a successful match,
+ *              it is added to this set.
+ *
+ *   Pool : A map from a sygus type T to a set of enumerated terms in T.
+ *          The terms in this pool are patterns whose builtin analogs are used
+ *          for matching against the terms to reconstruct t in (k, t, s).
+ *
+ *   let k_0 be a fresh skolem of sygus type T_0
+ *   Obs[T_0] += (k_0, t_0, null)
+ *
+ *   while Sol[k_0] == null
+ *     Obs' = {} // map from T to sets of triples pending addition to Obs
+ *     // enumeration phase
+ *     for each subfield type T of T_0
+ *       // enumerated terms may contain variables z ranging over all terms of
+ *       // their type (subfield types of T_0)
+ *       s[z] = nextEnum(T)
+ *       builtin = rewrite(toBuiltIn(s[z]))
+ *       if (s[z] is ground)
+ *         // let X be the theory the solver is invoked with
+ *         find (k, t, s) in Obs[T] s.t. |=_X t = builtin
+ *         if no such triple exists
+ *           let k be a new variable of type : T
+ *           Obs[T] += (k, builtin, null)
+ *         markSolved(k, s[z])
+ *       else if no s' in Pool[T] and matcher sigma s.t.
+ *             rewrite(toBuiltIn(s')) * sigma = builtin
+ *         Pool[T] += s[z]
+ *         for each (k, t, null) in Obs[T]
+ *           Obs' += matchNewObs(k, s[z])
+ *     // match phase
+ *     while Obs' != {}
+ *       Obs'' = {}
+ *       for each (k, t, null) in Obs' // s = null for all triples in Obs'
+ *         Obs[T] += (k, t, null)
+ *         for each s[z] in Pool[T]
+ *           Obs'' += matchNewObs(k, s[z])
+ *       Obs' = Obs''
+ *   g = Sol[k_0]
+ *   instantiate free variables of g with arbitrary sygus datatype values
+ * }
+ *
+ * matchNewObs(k, s[z]) returns Obs'
+ * {
+ *   u = rewrite(toBuiltIn(s[z]))
+ *   if match(u, t) == {toBuiltin(z) -> t'}
+ *     // let X be the theory the solver is invoked with
+ *     if forall t' exists (k'', t'', s'') in Obs[T] s.t. |=_X t'' = t'
+ *       markSolved(k, s{z -> s''})
+ *     else
+ *       let k' be a new variable of type : typeOf(z)
+ *       CandSol[k] += s{z -> k'}
+ *       Obs'[typeOf(z)] += (k', t', null)
+ * }
+ *
+ * markSolved(k, s)
+ * {
+ *   if Sol[k] != null
+ *     return
+ *   Sol[k] = s
+ *   CandSols[k] += s
+ *   Stack = {k}
+ *   while Stack != {}
+ *     k' = pop(Stack)
+ *     for all k'' in CandSols keys
+ *       for all s'[k'] in CandSols[k'']
+ *         s'{k' -> Sol[k']}
+ *         if s' does not contain free variables in Obs
+ *           Sol[k''] = s'
+ *           push(Stack, k'')
+ * }
+ */
+class SygusReconstruct : public expr::NotifyMatch
+{
+ public:
+  /**
+   * Constructor.
+   *
+   * @param tds Database for sygus terms
+   * @param s Statistics managed for the synth engine
+   */
+  SygusReconstruct(TermDbSygus* tds, SygusStatistics& s);
+
+  /** Reconstruct solution.
+   *
+   * Return (if possible) a sygus encoding of a node that is equivalent to sol
+   * and whose syntax matches the grammar corresponding to sygus datatype stn.
+   *
+   * For example, given:
+   *   sol = (* 2 x)
+   *   stn = A sygus datatype encoding the grammar
+   *           Start -> (c_PLUS Start Start) | c_x | c_0 | c_1
+   * This method may return (c_PLUS c_x c_x) and set reconstructed to 1.
+   *
+   * @param sol The target term
+   * @param stn The sygus datatype type encoding the syntax restrictions
+   * @param reconstructed The flag to update, set to 1 if we successfully return
+   *                      a node, otherwise it is set to -1
+   * @param enumLimit A value to limit the effort spent by this class (roughly
+   *                  equal to the number of intermediate terms to try)
+   * @return The reconstructed sygus term
+   */
+  Node reconstructSolution(Node sol,
+                           TypeNode stn,
+                           int8_t& reconstructed,
+                           uint64_t enumLimit);
+
+ private:
+  /** Match obligation `k`'s builtin term with pattern `sz`.
+   *
+   * This function matches the builtin term to reconstruct for obligation `k`
+   * with the builtin analog of the pattern `sz`. If the match succeeds, `sz` is
+   * added to the set of candidate solutions for `k` and a set of new
+   * sub-obligations to satisfy is returned. If there are no new sub-obligations
+   * to satisfy, then `sz` is considered a solution to obligation `k` and
+   * `matchNewObs(k, sz)` is called. For example, given:
+   *
+   * Obs[typeOf(c_z1)] = {(c_z1, (+ 1 1), null)}
+   * Pool[typeOf(c_z1)] = {(c_+ c_z2 c_z3)}
+   * CandSols = {}
+   *
+   * Then calling `matchNewObs(c_z1, (c_+ c_z2 c_z3))` will result in:
+   *
+   * Obs[typeOf(c_z1)] = {(c_z1, (+ 1 1), null), (c_z4, 1, null)}
+   * Pool[typeOf(c_z1)] = {(c_+ c_z2 c_z3)}
+   * CandSols = {c_z1 -> {(c_+ c_z4 c_z4)}}
+   *
+   * and will return `{typeOf(c_z4) -> {c_z4}}`.
+   *
+   * Notice that `c_z2` and `c_z3` are not returned as new sub-obligations.
+   * Instead, `(c_+ c_z2 c_z3)` is instantiated with a new skolem `c_z4`, which
+   * is then added to the set of obligations. This is done to allow the reuse of
+   * patterns in `Pool`. Also, notice that only one new skolem/sub-obligation is
+   * generated. That's because the builtin analogs of `c_z2` and `c_z3` match
+   * with the same builtin term `1`.
+   *
+   * @param k free var whose builtin term we need to match
+   * @param sz a pattern to match `ob`s builtin term with
+   * @return a set of new obligations to satisfy if the match succeeds
+   */
+  TypeObligationSetMap matchNewObs(Node k, Node sz);
+
+  /** mark obligation `k` as solved.
+   *
+   * This function first marks `s` as the complete/constant solution for
+   * `ob`. Then it substitutes all instances of `ob` in partial solutions to
+   * other obligations with `s`. The function repeats those two steps for each
+   * partial solution that gets completed because of the second step. For
+   * example, given:
+   *
+   * CandSols = {
+   *  mainOb -> {(+ z1 1)},
+   *  z1 -> {(* z2 x)},
+   *  z2 -> {2}
+   * }
+   * Sol = {z2 -> 2}
+   *
+   * Then calling `markSolved(z2, 2)` will result in:
+   *
+   * CandSols = {
+   *  mainOb -> {(+ z1 1), (+ (* 2 x) 1)},
+   *  z1 -> {(* z2 x), (* 2 x)},
+   *  z2 -> {2}
+   * }
+   * Sol = {mainOb -> (+ (* 2 x) 1), z1 -> (* 2 x), z2 -> 2}
+   *
+   * Note: example uses builtin terms instead of sygus terms for simplicity.
+   *
+   * @param ob free var to mark as solved and substitute
+   * @param sol constant solution to `ob`
+   */
+  void markSolved(Node k, Node s);
+
+  /**
+   * Initialize a sygus enumerator and a candidate rewrite database for each
+   * sygus datatype type.
+   *
+   * @param stn The sygus datatype type encoding the syntax restrictions
+   */
+  void initialize(TypeNode stn);
+
+  /**
+   * Remove solved obligations from the given set of obligations.
+   *
+   * @param unsolvedObs A set of obligations containing solved ones
+   */
+  void removeSolvedObs(TypeObligationSetMap& obs);
+
+  /**
+   * Replace all variables in `n` with ground values. Before, calling `match`,
+   * `matchNewObs` rewrites the builtin analog of `n` which contains variables.
+   * The rewritten term, however, may contain fewer variables:
+   *
+   * rewrite((ite true z1 z2)) = z1 // n = (c_ite c_true c_z1 c_z2)
+   *
+   * In such cases, `matchNewObs` replaces the remaining variables (`c_z1`) with
+   * obligations and ignores the eliminated ones (`c_z2`). Since the values of
+   * the eliminated variables do not matter, they are replaced with some ground
+   * values by calling this method.
+   *
+   * @param n A term containing variables
+   * @return `n` with all vars in `n` replaced with ground values
+   */
+  Node mkGround(Node n) const;
+
+  /**
+   * A notification that s is equal to n * { vars -> subs }. This function
+   * should return false if we do not wish to be notified of further matches.
+   */
+  bool notify(Node s,
+              Node n,
+              std::vector<Node>& vars,
+              std::vector<Node>& subs) override;
+
+  /**
+   * Reset the state of this SygusReconstruct object.
+   */
+  void clear();
+
+  /**
+   * Print the pool of patterns/shape used in the matching phase.
+   *
+   * \note requires enabling "sygus-rcons" trace
+   *
+   * @param pool a pool of patterns/shapes to print
+   */
+  void printPool(const std::unordered_map<TypeNode,
+                                          std::vector<Node>,
+                                          TypeNodeHashFunction>& pool) const;
+
+  /** pointer to the sygus term database */
+  TermDbSygus* d_tds;
+  /** reference to the statistics of parent */
+  SygusStatistics& d_stats;
+
+  /** a map from an obligation to its reconstruction info */
+  std::unordered_map<Node, RConsObligationInfo, NodeHashFunction> d_obInfo;
+  /** a map from a sygus datatype type to its reconstruction info */
+  std::unordered_map<TypeNode, RConsTypeInfo, TypeNodeHashFunction> d_stnInfo;
+
+  /** a map from an obligation to its sygus solution (if it exists) */
+  std::unordered_map<TNode, TNode, TNodeHashFunction> d_sol;
+
+  /** a map from a candidate solution to its sub-obligations */
+  std::unordered_map<Node, std::vector<Node>, NodeHashFunction> d_subObs;
+  /** a map from a candidate solution to its parent obligation */
+  std::unordered_map<Node, Node, NodeHashFunction> d_parentOb;
+
+  /** a cache of sygus variables treated as ground terms by matching */
+  std::unordered_map<Node, Node, NodeHashFunction> d_sygusVars;
+
+  /** A trie for filtering out redundant terms from the paterns pool */
+  expr::MatchTrie d_poolTrie;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif  // CVC4__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 3a9864ea9..831216445 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -57,7 +57,7 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe,
       d_stats(s),
       d_tds(qe->getTermDatabaseSygus()),
       d_hasSolution(false),
-      d_ceg_si(new CegSingleInv(qe)),
+      d_ceg_si(new CegSingleInv(qe, s)),
       d_templInfer(new SygusTemplateInfer),
       d_ceg_proc(new SynthConjectureProcess(qe)),
       d_ceg_gc(new CegGrammarConstructor(d_tds, this)),
@@ -1037,7 +1037,7 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
   Trace("cegqi-sol-debug") << "Printing synth solution..." << std::endl;
   Assert(d_quant[0].getNumChildren() == d_embed_quant[0].getNumChildren());
   std::vector<Node> sols;
-  std::vector<int> statuses;
+  std::vector<int8_t> statuses;
   if (!getSynthSolutionsInternal(sols, statuses))
   {
     return;
@@ -1049,7 +1049,7 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
     if (!sol.isNull())
     {
       Node prog = d_embed_quant[0][i];
-      int status = statuses[i];
+      int8_t status = statuses[i];
       TypeNode tn = prog.getType();
       const DType& dt = tn.getDType();
       std::stringstream ss;
@@ -1161,7 +1161,7 @@ bool SynthConjecture::getSynthSolutions(
 {
   NodeManager* nm = NodeManager::currentNM();
   std::vector<Node> sols;
-  std::vector<int> statuses;
+  std::vector<int8_t> statuses;
   Trace("cegqi-debug") << "getSynthSolutions..." << std::endl;
   if (!getSynthSolutionsInternal(sols, statuses))
   {
@@ -1173,7 +1173,7 @@ bool SynthConjecture::getSynthSolutions(
   for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
   {
     Node sol = sols[i];
-    int status = statuses[i];
+    int8_t status = statuses[i];
     Trace("cegqi-debug") << "...got " << i << ": " << sol
                          << ", status=" << status << std::endl;
     // get the builtin solution
@@ -1220,7 +1220,7 @@ void SynthConjecture::recordSolution(std::vector<Node>& vs)
 }
 
 bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
-                                                std::vector<int>& statuses)
+                                                std::vector<int8_t>& statuses)
 {
   if (!d_hasSolution)
   {
@@ -1234,7 +1234,7 @@ bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
     Assert(tn.isDatatype());
     // get the solution
     Node sol;
-    int status = -1;
+    int8_t status = -1;
     if (isSingleInvocation())
     {
       Assert(d_ceg_si != NULL);
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 27c565795..1b9f656bd 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -199,6 +199,9 @@ class SynthConjecture
    */
   bool checkSideCondition(const std::vector<Node>& cvals) const;
 
+  /** get a reference to the statistics of parent */
+  SygusStatistics& getSygusStatistics() { return d_stats; };
+
  private:
   /** reference to quantifier engine */
   QuantifiersEngine* d_qe;
@@ -387,7 +390,7 @@ class SynthConjecture
    * the sygus datatype constructor corresponding to variable x.
    */
   bool getSynthSolutionsInternal(std::vector<Node>& sols,
-                                 std::vector<int>& status);
+                                 std::vector<int8_t>& status);
   //-------------------------------- sygus stream
   /**
    * Prints the current synthesis solution to the output stream indicated by