Refactor sygus eval unfold (#1946)

8 files changed, 352 insertions, 189 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 569bc3c48..aa4487c42 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -481,6 +481,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/sygus/sygus_pbe.h \
 	theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp \
 	theory/quantifiers/sygus/ce_guided_single_inv_sol.h \
+	theory/quantifiers/sygus/sygus_eval_unfold.cpp \
+	theory/quantifiers/sygus/sygus_eval_unfold.h \
 	theory/quantifiers/sygus/sygus_explain.cpp \
 	theory/quantifiers/sygus/sygus_explain.h \
 	theory/quantifiers/sygus/sygus_invariance.cpp \
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index ec17294f9..fc41c7561 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -28,7 +28,14 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-Cegis::Cegis(QuantifiersEngine* qe, CegConjecture* p) : SygusModule(qe, p) {}
+Cegis::Cegis(QuantifiersEngine* qe, CegConjecture* p)
+    : SygusModule(qe, p), d_eval_unfold(nullptr)
+{
+  if (options::sygusEvalUnfold())
+  {
+    d_eval_unfold = qe->getTermDatabaseSygus()->getEvalUnfold();
+  }
+}
 
 bool Cegis::initialize(Node n,
                        const std::vector<Node>& candidates,
@@ -100,7 +107,7 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
          add the lemmas below as well, in parallel. */
     }
   }
-  if (options::sygusEvalUnfold())
+  if (d_eval_unfold != nullptr)
   {
     Trace("cegqi-engine") << "  *** Do evaluation unfolding..." << std::endl;
     std::vector<Node> eager_terms, eager_vals, eager_exps;
@@ -108,11 +115,11 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
     {
       Trace("cegqi-debug") << "  register " << candidates[i] << " -> "
                            << candidate_values[i] << std::endl;
-      d_tds->registerModelValue(candidates[i],
-                                candidate_values[i],
-                                eager_terms,
-                                eager_vals,
-                                eager_exps);
+      d_eval_unfold->registerModelValue(candidates[i],
+                                        candidate_values[i],
+                                        eager_terms,
+                                        eager_vals,
+                                        eager_exps);
     }
     Trace("cegqi-debug") << "...produced " << eager_terms.size()
                          << " evaluation unfold lemmas.\n";
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index e5ee6bc56..70f3ce8b6 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -65,6 +65,8 @@ class Cegis : public SygusModule
                                        std::vector<Node>& lems) override;
 
  protected:
+  /** the evaluation unfold utility of d_tds */
+  SygusEvalUnfold* d_eval_unfold;
   /** If CegConjecture::d_base_inst is exists y. P( d, y ), then this is y. */
   std::vector<Node> d_base_vars;
   /**
diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
new file mode 100644
index 000000000..09df1eeab
--- /dev/null
+++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
@@ -0,0 +1,199 @@
+/*********************                                                        */
+/*! \file sygus_eval_unfold.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of sygus_eval_unfold
+ **/
+
+#include "theory/quantifiers/sygus/sygus_eval_unfold.h"
+
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+
+using namespace std;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+SygusEvalUnfold::SygusEvalUnfold(TermDbSygus* tds) : d_tds(tds) {}
+
+void SygusEvalUnfold::registerEvalTerm(Node n)
+{
+  Assert(options::sygusEvalUnfold());
+  // is this an APPLY_UF term with head that is a sygus datatype term?
+  if (n.getKind() != APPLY_UF)
+  {
+    return;
+  }
+  TypeNode tn = n[0].getType();
+  if (!tn.isDatatype())
+  {
+    return;
+  }
+  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  if (!dt.isSygus())
+  {
+    return;
+  }
+  Node f = n.getOperator();
+  if (n[0].getKind() == APPLY_CONSTRUCTOR)
+  {
+    // constructors should be unfolded and reduced already
+    return;
+  }
+  if (d_eval_processed.find(n) != d_eval_processed.end())
+  {
+    return;
+  }
+  Trace("sygus-eval-unfold")
+      << "SygusEvalUnfold: register eval term : " << n << std::endl;
+  d_eval_processed.insert(n);
+  // is it the sygus evaluation function?
+  Node eval_op = Node::fromExpr(dt.getSygusEvaluationFunc());
+  if (n.getOperator() != eval_op)
+  {
+    return;
+  }
+  // register this evaluation term with its head
+  d_evals[n[0]].push_back(n);
+  Node var_list = Node::fromExpr(dt.getSygusVarList());
+  d_eval_args[n[0]].push_back(std::vector<Node>());
+  for (unsigned j = 1, size = n.getNumChildren(); j < size; j++)
+  {
+    d_eval_args[n[0]].back().push_back(n[j]);
+  }
+  Node a = TermDbSygus::getAnchor(n[0]);
+  d_subterms[a].insert(n[0]);
+}
+
+void SygusEvalUnfold::registerModelValue(Node a,
+                                         Node v,
+                                         std::vector<Node>& terms,
+                                         std::vector<Node>& vals,
+                                         std::vector<Node>& exps)
+{
+  std::map<Node, std::unordered_set<Node, NodeHashFunction> >::iterator its =
+      d_subterms.find(a);
+  if (its == d_subterms.end())
+  {
+    return;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  SygusExplain* sy_exp = d_tds->getExplain();
+  Trace("sygus-eval-unfold")
+      << "SygusEvalUnfold: " << a << ", has " << its->second.size()
+      << " registered subterms." << std::endl;
+  for (const Node& n : its->second)
+  {
+    Trace("sygus-eval-unfold-debug") << "...process : " << n << std::endl;
+    std::map<Node, std::vector<std::vector<Node> > >::iterator it =
+        d_eval_args.find(n);
+    if (it != d_eval_args.end() && !it->second.empty())
+    {
+      TNode at = a;
+      TNode vt = v;
+      Node vn = n.substitute(at, vt);
+      vn = Rewriter::rewrite(vn);
+      unsigned start = d_node_mv_args_proc[n][vn];
+      // get explanation in terms of testers
+      std::vector<Node> antec_exp;
+      sy_exp->getExplanationForEquality(n, vn, antec_exp);
+      Node antec =
+          antec_exp.size() == 1 ? antec_exp[0] : nm->mkNode(AND, antec_exp);
+      // Node antec = n.eqNode( vn );
+      TypeNode tn = n.getType();
+      Assert(tn.isDatatype());
+      const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+      Assert(dt.isSygus());
+      Trace("sygus-eval-unfold")
+          << "SygusEvalUnfold: Register model value : " << vn << " for " << n
+          << std::endl;
+      unsigned curr_size = it->second.size();
+      Trace("sygus-eval-unfold")
+          << "...it has " << curr_size << " evaluations, already processed "
+          << start << "." << std::endl;
+      Node bTerm = d_tds->sygusToBuiltin(vn, tn);
+      Trace("sygus-eval-unfold") << "Built-in term : " << bTerm << std::endl;
+      std::vector<Node> vars;
+      Node var_list = Node::fromExpr(dt.getSygusVarList());
+      for (const Node& v : var_list)
+      {
+        vars.push_back(v);
+      }
+      // evaluation children
+      std::vector<Node> eval_children;
+      eval_children.push_back(Node::fromExpr(dt.getSygusEvaluationFunc()));
+      eval_children.push_back(n);
+      // for each evaluation
+      for (unsigned i = start; i < curr_size; i++)
+      {
+        Node res;
+        Node expn;
+        // should we unfold?
+        bool do_unfold = false;
+        if (options::sygusEvalUnfoldBool())
+        {
+          if (bTerm.getKind() == ITE || bTerm.getType().isBoolean())
+          {
+            do_unfold = true;
+          }
+        }
+        if (do_unfold)
+        {
+          // TODO (#1949) : this is replicated for different values, possibly
+          // do better caching
+          std::map<Node, Node> vtm;
+          std::vector<Node> exp;
+          vtm[n] = vn;
+          eval_children.insert(
+              eval_children.end(), it->second[i].begin(), it->second[i].end());
+          Node eval_fun = nm->mkNode(APPLY_UF, eval_children);
+          eval_children.resize(2);
+          res = d_tds->unfold(eval_fun, vtm, exp);
+          expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp);
+        }
+        else
+        {
+          EvalSygusInvarianceTest esit;
+          eval_children.insert(
+              eval_children.end(), it->second[i].begin(), it->second[i].end());
+          Node conj = nm->mkNode(APPLY_UF, eval_children);
+          eval_children[1] = vn;
+          Node eval_fun = nm->mkNode(APPLY_UF, eval_children);
+          res = d_tds->evaluateWithUnfolding(eval_fun);
+          esit.init(conj, n, res);
+          eval_children.resize(2);
+          eval_children[1] = n;
+
+          // evaluate with minimal explanation
+          std::vector<Node> mexp;
+          sy_exp->getExplanationFor(n, vn, mexp, esit);
+          Assert(!mexp.empty());
+          expn = mexp.size() == 1 ? mexp[0] : nm->mkNode(AND, mexp);
+        }
+        Assert(!res.isNull());
+        terms.push_back(d_evals[n][i]);
+        vals.push_back(res);
+        exps.push_back(expn);
+        Trace("sygus-eval-unfold")
+            << "Conclude : " << d_evals[n][i] << " == " << res << std::endl;
+        Trace("sygus-eval-unfold") << "   from " << expn << std::endl;
+      }
+      d_node_mv_args_proc[n][vn] = curr_size;
+    }
+  }
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.h b/src/theory/quantifiers/sygus/sygus_eval_unfold.h
new file mode 100644
index 000000000..94f37c845
--- /dev/null
+++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.h
@@ -0,0 +1,116 @@
+/*********************                                                        */
+/*! \file sygus_eval_unfold.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief sygus_eval_unfold
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H
+
+#include <map>
+#include "expr/node.h"
+#include "theory/quantifiers/sygus/sygus_invariance.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class TermDbSygus;
+
+/** SygusEvalUnfold
+ *
+ * This class implements techniques for eagerly unfolding sygus evaluation
+ * functions. For example, given sygus datatype type corresponding to grammar:
+ *   A -> 0 | 1 | A+A
+ * whose evaluation function is eval, this class adds lemmas that "eagerly
+ * unfold" applications of eval based on the model values of evaluation heads
+ * in refinement lemmas.
+ */
+class SygusEvalUnfold
+{
+ public:
+  SygusEvalUnfold(TermDbSygus* tds);
+  ~SygusEvalUnfold() {}
+  /** register evaluation term
+   *
+   * This is called by TermDatabase, during standard effort calls when a term
+   * n is registered as an equivalence class in the master equality engine.
+   * If this term is of the form:
+   *   eval( a, t1, ..., tn )
+   * where a is a symbolic term of sygus datatype type (not a application of a
+   * constructor), then we remember that n is an evaluation function application
+   * for evaluation head a.
+   */
+  void registerEvalTerm(Node n);
+  /** register model value
+   *
+   * This notifies this class that the model value M(a) of an anchor term a is
+   * currently v. Assume in the following that the top symbol of v is some sygus
+   * datatype constructor C_op.
+   *
+   * If we have registered terms eval( a, T1 ), ..., eval( a, Tm ), then we
+   * ensure that for each i=1,...,m, a lemma of one of the two forms is
+   * generated:
+   * [A] a=v => eval( a, Ti ) = [[unfold( eval( v, Ti ) )]]
+   * [B] is-C_op(v) => eval(a, Ti ) = op(eval( a.1, Ti ), ..., eval( a.k, Ti )),
+   * where this corresponds to a "one step folding" of the sygus evaluation
+   * function, i.e. op is a builtin operator encoded by constructor C_op.
+   *
+   * We decide which kind of lemma to send ([A] or [B]) based on the symbol
+   * C_op. If op is an ITE, or if C_op is a Boolean operator, then we add [B].
+   * Otherwise, we add [A]. The intuition of why [B] is better than [A] for the
+   * former is that evaluation unfolding can lead to useful conflict analysis.
+   *
+   * For each lemma C => eval( a, T ) = T' we infer is necessary, we add C to
+   * exps, eval( a, T ) to terms, and T' to vals. The caller should send the
+   * corresponding lemma on the output channel.
+   *
+   * We do the above scheme *for each* selector chain (see d_subterms below)
+   * applied to a.
+   */
+  void registerModelValue(Node a,
+                          Node v,
+                          std::vector<Node>& exps,
+                          std::vector<Node>& terms,
+                          std::vector<Node>& vals);
+
+ private:
+  /** sygus term database associated with this utility */
+  TermDbSygus* d_tds;
+  /** the set of evaluation terms we have already processed */
+  std::unordered_set<Node, NodeHashFunction> d_eval_processed;
+  /** map from evaluation heads to evaluation function applications */
+  std::map<Node, std::vector<Node> > d_evals;
+  /**
+   * Map from evaluation function applications to their arguments (minus the
+   * evaluation head). For example, eval(x,0,1) is mapped to { 0, 1 }.
+   */
+  std::map<Node, std::vector<std::vector<Node> > > d_eval_args;
+  /**
+   * For each (a,M(a)) pair, the number of terms in d_evals that we have added
+   * lemmas for
+   */
+  std::map<Node, std::map<Node, unsigned> > d_node_mv_args_proc;
+  /** subterms map
+   *
+   * This maps anchor terms to the set of shared selector chains with
+   * them as an anchor, for example x may map to { x, x.1, x.2, x.1.1 }.
+   */
+  std::map<Node, std::unordered_set<Node, NodeHashFunction> > d_subterms;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H */
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 5efa1198b..37a8ae382 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -34,7 +34,8 @@ namespace quantifiers {
 TermDbSygus::TermDbSygus(context::Context* c, QuantifiersEngine* qe)
     : d_quantEngine(qe),
       d_syexp(new SygusExplain(this)),
-      d_ext_rw(new ExtendedRewriter(true))
+      d_ext_rw(new ExtendedRewriter(true)),
+      d_eval_unfold(new SygusEvalUnfold(this))
 {
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
@@ -1287,162 +1288,6 @@ unsigned TermDbSygus::getAnchorDepth( Node n ) {
   }
 }
 
-
-void TermDbSygus::registerEvalTerm( Node n ) {
-  if (options::sygusEvalUnfold())
-  {
-    if( n.getKind()==APPLY_UF && !n.getType().isBoolean() ){
-      TypeNode tn = n[0].getType();
-      if( tn.isDatatype() ){
-        const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-        if( dt.isSygus() ){
-          Node f = n.getOperator();
-          if( n[0].getKind()!=APPLY_CONSTRUCTOR ){
-            if (d_eval_processed.find(n) == d_eval_processed.end())
-            {
-              Trace("sygus-eager")
-                  << "TermDbSygus::eager: Register eval term : " << n
-                  << std::endl;
-              d_eval_processed.insert(n);
-              d_evals[n[0]].push_back(n);
-              TypeNode tn = n[0].getType();
-              Assert(tn.isDatatype());
-              const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-              Node var_list = Node::fromExpr(dt.getSygusVarList());
-              Assert(dt.isSygus());
-              d_eval_args[n[0]].push_back(std::vector<Node>());
-              bool isConst = true;
-              for (unsigned j = 1; j < n.getNumChildren(); j++)
-              {
-                d_eval_args[n[0]].back().push_back(n[j]);
-                if (!n[j].isConst())
-                {
-                  isConst = false;
-                }
-              }
-              d_eval_args_const[n[0]].push_back(isConst);
-              Node a = getAnchor(n[0]);
-              d_subterms[a][n[0]] = true;
-            }
-          }
-        }
-      }    
-    }
-  }
-}
-
-void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& terms, std::vector< Node >& vals, std::vector< Node >& exps ) {
-  std::map< Node, std::map< Node, bool > >::iterator its = d_subterms.find( a );
-  if( its!=d_subterms.end() ){
-    Trace("sygus-eager") << "registerModelValue : " << a << ", has " << its->second.size() << " registered subterms." << std::endl;
-    for( std::map< Node, bool >::iterator itss = its->second.begin(); itss != its->second.end(); ++itss ){
-      Node n = itss->first;
-      Trace("sygus-eager-debug") << "...process : " << n << std::endl;
-      std::map< Node, std::vector< std::vector< Node > > >::iterator it = d_eval_args.find( n );
-      if( it!=d_eval_args.end() && !it->second.empty() ){
-        TNode at = a;
-        TNode vt = v;
-        Node vn = n.substitute( at, vt );
-        vn = Rewriter::rewrite( vn );
-        unsigned start = d_node_mv_args_proc[n][vn];
-        // get explanation in terms of testers
-        std::vector< Node > antec_exp;
-        d_syexp->getExplanationForEquality(n, vn, antec_exp);
-        Node antec = antec_exp.size()==1 ? antec_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, antec_exp );
-        //Node antec = n.eqNode( vn );
-        TypeNode tn = n.getType();
-        Assert( tn.isDatatype() );
-        const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-        Assert( dt.isSygus() );
-        Trace("sygus-eager") << "TermDbSygus::eager: Register model value : " << vn << " for " << n << std::endl;
-        Trace("sygus-eager") << "...it has " << it->second.size() << " evaluations, already processed " << start << "." << std::endl;
-        Node bTerm = sygusToBuiltin( vn, tn );
-        Trace("sygus-eager") << "Built-in term : " << bTerm << std::endl;
-        std::vector< Node > vars;
-        Node var_list = Node::fromExpr( dt.getSygusVarList() );
-        for( unsigned j=0; j<var_list.getNumChildren(); j++ ){
-          vars.push_back( var_list[j] );
-        }
-        //evaluation children
-        std::vector< Node > eval_children;
-        eval_children.push_back( Node::fromExpr( dt.getSygusEvaluationFunc() ) );
-        eval_children.push_back( n );
-        //for each evaluation
-        for( unsigned i=start; i<it->second.size(); i++ ){
-          Node res;
-          Node expn;
-          // unfold?
-          bool do_unfold = false;
-          if (options::sygusEvalUnfoldBool())
-          {
-            if( bTerm.getKind()==ITE || bTerm.getType().isBoolean() ){
-              do_unfold = true;
-            }
-          }
-          if( do_unfold ){
-            // TODO : this is replicated for different values, possibly do better caching
-            std::map< Node, Node > vtm; 
-            std::vector< Node > exp;
-            vtm[n] = vn;
-            eval_children.insert( eval_children.end(), it->second[i].begin(), it->second[i].end() );
-            Node eval_fun = NodeManager::currentNM()->mkNode( kind::APPLY_UF, eval_children );
-            eval_children.resize( 2 );  
-            res = unfold( eval_fun, vtm, exp );
-            expn = exp.size()==1 ? exp[0] : NodeManager::currentNM()->mkNode( kind::AND, exp );
-          }else{
-
-            EvalSygusInvarianceTest esit;
-            eval_children.insert( eval_children.end(), it->second[i].begin(), it->second[i].end() );
-            Node conj =
-                NodeManager::currentNM()->mkNode(kind::APPLY_UF, eval_children);
-            eval_children[1] = vn;
-            Node eval_fun = NodeManager::currentNM()->mkNode( kind::APPLY_UF, eval_children );
-            res = evaluateWithUnfolding(eval_fun);
-            esit.init(conj, n, res);
-            eval_children.resize( 2 );  
-            eval_children[1] = n;
-            
-            //evaluate with minimal explanation
-            std::vector< Node > mexp;
-            d_syexp->getExplanationFor(n, vn, mexp, esit);
-            Assert( !mexp.empty() );
-            expn = mexp.size()==1 ? mexp[0] : NodeManager::currentNM()->mkNode( kind::AND, mexp );
-            
-            //if all constant, we can use evaluation to minimize the explanation
-            //Assert( i<d_eval_args_const[n].size() );
-            //if( d_eval_args_const[n][i] ){
-              /*
-              std::map< Node, Node > vtm; 
-              std::map< Node, Node > visited; 
-              std::map< Node, std::vector< Node > > exp;
-              vtm[n] = vn;
-              res = crefEvaluate( eval_fun, vtm, visited, exp );
-              Assert( !exp[eval_fun].empty() );
-              expn = exp[eval_fun].size()==1 ? exp[eval_fun][0] : NodeManager::currentNM()->mkNode( kind::AND, exp[eval_fun] );
-              */
-              /*
-            //otherwise, just do a substitution
-            }else{
-              Assert( vars.size()==it->second[i].size() );
-              res = bTerm.substitute( vars.begin(), vars.end(), it->second[i].begin(), it->second[i].end() );
-              res = Rewriter::rewrite( res );
-              expn = antec;
-            }
-            */
-          }
-          Assert( !res.isNull() );
-          terms.push_back( d_evals[n][i] );
-          vals.push_back( res );
-          exps.push_back( expn );
-          Trace("sygus-eager") << "Conclude : " << d_evals[n][i] << " == " << res << ", cref eval = " << d_eval_args_const[n][i] << std::endl;
-          Trace("sygus-eager") << "   from " << expn << std::endl;
-        }
-        d_node_mv_args_proc[n][vn] = it->second.size();
-      }
-    }
-  }
-}
-
 Node TermDbSygus::unfold( Node en, std::map< Node, Node >& vtm, std::vector< Node >& exp, bool track_exp ) {
   if( en.getKind()==kind::APPLY_UF ){
     Trace("sygus-db-debug") << "Unfold : " << en << std::endl;
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index d53e436e0..9f370cd15 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -20,6 +20,7 @@
 #include <unordered_set>
 
 #include "theory/quantifiers/extended_rewrite.h"
+#include "theory/quantifiers/sygus/sygus_eval_unfold.h"
 #include "theory/quantifiers/sygus/sygus_explain.h"
 #include "theory/quantifiers/term_database.h"
 
@@ -52,6 +53,8 @@ class TermDbSygus {
   SygusExplain* getExplain() { return d_syexp.get(); }
   /** get the extended rewrite utility */
   ExtendedRewriter* getExtRewriter() { return d_ext_rw.get(); }
+  /** evaluation unfolding utility */
+  SygusEvalUnfold* getEvalUnfold() { return d_eval_unfold.get(); }
   //------------------------------end utilities
 
   //------------------------------enumerators
@@ -210,8 +213,10 @@ class TermDbSygus {
   //------------------------------utilities
   /** sygus explanation */
   std::unique_ptr<SygusExplain> d_syexp;
-  /** sygus explanation */
+  /** extended rewriter */
   std::unique_ptr<ExtendedRewriter> d_ext_rw;
+  /** evaluation function unfolding utility */
+  std::unique_ptr<SygusEvalUnfold> d_eval_unfold;
   //------------------------------end utilities
 
   //------------------------------enumerators
@@ -344,21 +349,7 @@ public: // for symmetry breaking
   bool considerConst( TypeNode tn, TypeNode tnp, Node c, Kind pk, int arg );
   bool considerConst( const Datatype& pdt, TypeNode tnp, Node c, Kind pk, int arg );
   int solveForArgument( TypeNode tnp, unsigned cindex, unsigned arg );
-  
-//for eager instantiation
-  // TODO (as part of #1235) move some of these functions to sygus_explain.h
- private:
-  /** the set of evaluation terms we have already processed */
-  std::unordered_set<Node, NodeHashFunction> d_eval_processed;
-  std::map< Node, std::map< Node, bool > > d_subterms;
-  std::map< Node, std::vector< Node > > d_evals;
-  std::map< Node, std::vector< std::vector< Node > > > d_eval_args;
-  std::map< Node, std::vector< bool > > d_eval_args_const;
-  std::map< Node, std::map< Node, unsigned > > d_node_mv_args_proc;
-
 public:
-  void registerEvalTerm( Node n );
-  void registerModelValue( Node n, Node v, std::vector< Node >& exps, std::vector< Node >& terms, std::vector< Node >& vals );
   Node unfold( Node en, std::map< Node, Node >& vtm, std::vector< Node >& exp, bool track_exp = true );
   Node unfold( Node en ){
     std::map< Node, Node > vtm;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index b5f179822..3746c2e1c 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -20,24 +20,24 @@
 #include "theory/arrays/theory_arrays.h"
 #include "theory/datatypes/theory_datatypes.h"
 #include "theory/quantifiers/alpha_equivalence.h"
-#include "theory/quantifiers/fmf/ambqi_builder.h"
 #include "theory/quantifiers/anti_skolem.h"
-#include "theory/quantifiers/fmf/bounded_integers.h"
-#include "theory/quantifiers/sygus/ce_guided_instantiation.h"
 #include "theory/quantifiers/cegqi/ceg_t_instantiator.h"
+#include "theory/quantifiers/cegqi/inst_strategy_cbqi.h"
 #include "theory/quantifiers/conjecture_generator.h"
+#include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
+#include "theory/quantifiers/ematching/instantiation_engine.h"
+#include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/equality_infer.h"
 #include "theory/quantifiers/equality_query.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/fmf/ambqi_builder.h"
+#include "theory/quantifiers/fmf/bounded_integers.h"
 #include "theory/quantifiers/fmf/full_model_check.h"
+#include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/inst_propagator.h"
-#include "theory/quantifiers/cegqi/inst_strategy_cbqi.h"
-#include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
 #include "theory/quantifiers/inst_strategy_enumerative.h"
 #include "theory/quantifiers/instantiate.h"
-#include "theory/quantifiers/ematching/instantiation_engine.h"
 #include "theory/quantifiers/local_theory_ext.h"
-#include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/quant_conflict_find.h"
 #include "theory/quantifiers/quant_epr.h"
 #include "theory/quantifiers/quant_relevance.h"
@@ -47,11 +47,12 @@
 #include "theory/quantifiers/relevant_domain.h"
 #include "theory/quantifiers/rewrite_engine.h"
 #include "theory/quantifiers/skolemize.h"
-#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/sygus/ce_guided_instantiation.h"
+#include "theory/quantifiers/sygus/sygus_eval_unfold.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers/ematching/trigger.h"
 #include "theory/sep/theory_sep.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/equality_engine.h"
@@ -847,7 +848,7 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within
     {
       if (d_sygus_tdb)
       {
-        d_sygus_tdb->registerEvalTerm(n);
+        d_sygus_tdb->getEvalUnfold()->registerEvalTerm(n);
       }
 
       // added contains also the Node that just have been asserted in this