Add skolem definition manager (#6187)

This creates a central utility for managing "skolem definitions", e.g. mapping between skolems and the lemmas that define their behavior.

This utility is taken from the satRlv branch. It will also be used for the new implementation of the justification decision heuristic.

Note that this PR takes some helper functions out of term formula removal (e.g. hasSkolems) Prior to this PR, these helper functions were incorrect since term formula removal does not account for all introduced skolems. For instance, Theory::ppRewrite may introduce skolems directly. This PR consolidates these cases into the new class, which is called from PropEngine when lemmas and assertions are added. At the moment, the only use of this method is for CEGQI, which needs to do its own tracking of skolems in certain literals.

It also makes some minor reorganization to prop engine.

9 files changed, 319 insertions, 165 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 5ceb44615..54ece796a 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -209,6 +209,8 @@ libcvc4_add_sources(
   prop/sat_solver_factory.h
   prop/sat_solver_types.cpp
   prop/sat_solver_types.h
+  prop/skolem_def_manager.cpp
+  prop/skolem_def_manager.h
   prop/theory_proxy.cpp
   prop/theory_proxy.h
   smt/abduction_solver.cpp
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 71b27d8ec..3f53433ae 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -174,17 +174,15 @@ theory::TrustNode PropEngine::removeItes(
 void PropEngine::notifyPreprocessedAssertions(
     const std::vector<Node>& assertions)
 {
-  // notify the theory engine of preprocessed assertions
-  d_theoryEngine->notifyPreprocessedAssertions(assertions);
-  for (const Node& assertion : assertions)
-  {
-    d_decisionEngine->addAssertion(assertion);
-  }
+  // notify the theory proxy of preprocessed assertions
+  d_theoryProxy->notifyPreprocessedAssertions(assertions);
 }
 
 void PropEngine::assertFormula(TNode node) {
   Assert(!d_inCheckSat) << "Sat solver in solve()!";
   Debug("prop") << "assertFormula(" << node << ")" << std::endl;
+  // NOTE: we do not notify the theory proxy here, since we've already
+  // notified the theory proxy during notifyPreprocessedAssertions
   assertInternal(node, false, false, true);
 }
 
@@ -192,7 +190,7 @@ void PropEngine::assertSkolemDefinition(TNode node, TNode skolem)
 {
   Assert(!d_inCheckSat) << "Sat solver in solve()!";
   Debug("prop") << "assertFormula(" << node << ")" << std::endl;
-  d_decisionEngine->addSkolemDefinition(node, skolem);
+  d_theoryProxy->notifyAssertion(node, skolem);
   assertInternal(node, false, false, true);
 }
 
@@ -284,13 +282,13 @@ void PropEngine::assertLemmasInternal(
     if (!trn.isNull())
     {
       // notify the theory proxy of the lemma
-      d_decisionEngine->addAssertion(trn.getProven());
+      d_theoryProxy->notifyAssertion(trn.getProven());
     }
     Assert(ppSkolems.size() == ppLemmas.size());
     for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
     {
       Node lem = ppLemmas[i].getProven();
-      d_decisionEngine->addSkolemDefinition(lem, ppSkolems[i]);
+      d_theoryProxy->notifyAssertion(ppLemmas[i].getProven(), ppSkolems[i]);
     }
   }
 }
@@ -465,14 +463,14 @@ Node PropEngine::getPreprocessedTerm(TNode n,
   // get the preprocessed form of the term
   Node pn = getPreprocessedTerm(n);
   // initialize the set of skolems and assertions to process
-  std::vector<theory::TrustNode> toProcessAsserts;
+  std::vector<Node> toProcessAsserts;
   std::vector<Node> toProcess;
   d_theoryProxy->getSkolems(pn, toProcessAsserts, toProcess);
   size_t index = 0;
   // until fixed point is reached
   while (index < toProcess.size())
   {
-    theory::TrustNode ka = toProcessAsserts[index];
+    Node ka = toProcessAsserts[index];
     Node k = toProcess[index];
     index++;
     if (std::find(sks.begin(), sks.end(), k) != sks.end())
@@ -481,7 +479,7 @@ Node PropEngine::getPreprocessedTerm(TNode n,
       continue;
     }
     // must preprocess lemmas as well
-    Node kap = getPreprocessedTerm(ka.getProven());
+    Node kap = getPreprocessedTerm(ka);
     skAsserts.push_back(kap);
     sks.push_back(k);
     // get the skolems in the preprocessed form of the lemma ka
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index d0810324a..fe5d94122 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -220,6 +220,10 @@ class PropEngine
    * another skolem introduced by term formula removal, then calling this
    * method on (P k1) will include both k1 and k2 in sks, and their definitions
    * in skAsserts.
+   *
+   * Notice that this method is not frequently used. It is used for algorithms
+   * that explicitly care about knowing which skolems occur in the preprocessed
+   * form of a term, recursively.
    */
   Node getPreprocessedTerm(TNode n,
                            std::vector<Node>& skAsserts,
diff --git a/src/prop/skolem_def_manager.cpp b/src/prop/skolem_def_manager.cpp
new file mode 100644
index 000000000..c2a6a8462
--- /dev/null
+++ b/src/prop/skolem_def_manager.cpp
@@ -0,0 +1,173 @@
+/*********************                                                        */
+/*! \file skolem_def_manager.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 Skolem definition manager
+ **/
+
+#include "prop/skolem_def_manager.h"
+
+#include "expr/attribute.h"
+
+namespace CVC4 {
+namespace prop {
+
+SkolemDefManager::SkolemDefManager(context::Context* context,
+                                   context::UserContext* userContext)
+    : d_skDefs(userContext), d_skActive(context)
+{
+}
+
+SkolemDefManager::~SkolemDefManager() {}
+
+void SkolemDefManager::notifySkolemDefinition(TNode skolem, Node def)
+{
+  // Notice that skolem may have kind SKOLEM or BOOLEAN_TERM_VARIABLE
+  Trace("sk-defs") << "notifySkolemDefinition: " << def << " for " << skolem
+                   << std::endl;
+  // in very rare cases, a skolem may be generated twice for terms that are
+  // equivalent up to purification
+  if (d_skDefs.find(skolem) == d_skDefs.end())
+  {
+    d_skDefs.insert(skolem, def);
+  }
+}
+
+TNode SkolemDefManager::getDefinitionForSkolem(TNode skolem) const
+{
+  NodeNodeMap::const_iterator it = d_skDefs.find(skolem);
+  AlwaysAssert(it != d_skDefs.end()) << "No skolem def for " << skolem;
+  return it->second;
+}
+
+void SkolemDefManager::notifyAsserted(TNode literal,
+                                      std::vector<TNode>& activatedSkolems)
+{
+  std::unordered_set<Node, NodeHashFunction> skolems;
+  getSkolems(literal, skolems);
+  for (const Node& k : skolems)
+  {
+    if (d_skActive.find(k) != d_skActive.end())
+    {
+      // already active
+      continue;
+    }
+    d_skActive.insert(k);
+    // add to the activated list
+    activatedSkolems.push_back(k);
+  }
+}
+
+struct HasSkolemTag
+{
+};
+struct HasSkolemComputedTag
+{
+};
+/** Attribute true for nodes with skolems in them */
+typedef expr::Attribute<HasSkolemTag, bool> HasSkolemAttr;
+/** Attribute true for nodes where we have computed the above attribute */
+typedef expr::Attribute<HasSkolemComputedTag, bool> HasSkolemComputedAttr;
+
+bool SkolemDefManager::hasSkolems(TNode n) const
+{
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    if (cur.getAttribute(HasSkolemComputedAttr()))
+    {
+      visit.pop_back();
+      // already computed
+      continue;
+    }
+    it = visited.find(cur);
+    if (it == visited.end())
+    {
+      visited.insert(cur);
+      if (cur.getNumChildren() == 0)
+      {
+        visit.pop_back();
+        bool hasSkolem = false;
+        if (cur.isVar())
+        {
+          hasSkolem = (d_skDefs.find(cur) != d_skDefs.end());
+        }
+        cur.setAttribute(HasSkolemAttr(), hasSkolem);
+        cur.setAttribute(HasSkolemComputedAttr(), true);
+      }
+      else
+      {
+        visit.insert(visit.end(), cur.begin(), cur.end());
+      }
+    }
+    else
+    {
+      visit.pop_back();
+      bool hasSkolem = false;
+      for (TNode i : cur)
+      {
+        Assert(i.getAttribute(HasSkolemComputedAttr()));
+        if (i.getAttribute(HasSkolemAttr()))
+        {
+          hasSkolem = true;
+          break;
+        }
+      }
+      cur.setAttribute(HasSkolemAttr(), hasSkolem);
+      cur.setAttribute(HasSkolemComputedAttr(), true);
+    }
+  } while (!visit.empty());
+  Assert(n.getAttribute(HasSkolemComputedAttr()));
+  return n.getAttribute(HasSkolemAttr());
+}
+
+void SkolemDefManager::getSkolems(
+    TNode n, std::unordered_set<Node, NodeHashFunction>& skolems) const
+{
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    if (!hasSkolems(cur))
+    {
+      // does not have skolems, continue
+      continue;
+    }
+    it = visited.find(cur);
+    if (it == visited.end())
+    {
+      visited.insert(cur);
+      if (cur.isVar())
+      {
+        if (d_skDefs.find(cur) != d_skDefs.end())
+        {
+          skolems.insert(cur);
+        }
+      }
+      else
+      {
+        visit.insert(visit.end(), cur.begin(), cur.end());
+      }
+    }
+  } while (!visit.empty());
+}
+
+}  // namespace prop
+}  // namespace CVC4
diff --git a/src/prop/skolem_def_manager.h b/src/prop/skolem_def_manager.h
new file mode 100644
index 000000000..9bb118356
--- /dev/null
+++ b/src/prop/skolem_def_manager.h
@@ -0,0 +1,91 @@
+/*********************                                                        */
+/*! \file skolem_def_manager.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 Skolem definition manager
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__PROP__SKOLEM_DEF_MANAGER_H
+#define CVC4__PROP__SKOLEM_DEF_MANAGER_H
+
+#include <iosfwd>
+#include <unordered_set>
+#include <vector>
+
+#include "context/cdhashset.h"
+#include "context/cdinsert_hashmap.h"
+#include "context/context.h"
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace prop {
+
+/**
+ * This class manages the mapping between introduced skolems and the lemmas
+ * that define their behavior. It can be used to manage which lemmas are
+ * relevant in the current context, e.g. a lemma corresponding to a skolem
+ * definition for k is relevant when k appears in an asserted literal.
+ *
+ * It also has utilities for tracking (in a SAT-context-dependent manner) which
+ * skolems are "active", e.g. appear in any asserted literal.
+ */
+class SkolemDefManager
+{
+  using NodeNodeMap = context::CDInsertHashMap<Node, Node, NodeHashFunction>;
+  using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
+
+ public:
+  SkolemDefManager(context::Context* context,
+                   context::UserContext* userContext);
+
+  ~SkolemDefManager();
+
+  /**
+   * Notify skolem definition. This is called when a lemma def is added to the
+   * SAT solver that corresponds to the skolem definition for skolem k.
+   */
+  void notifySkolemDefinition(TNode k, Node def);
+  /**
+   * Get skolem definition for k, where k must be a skolem having a definition
+   * managed by this class.
+   */
+  TNode getDefinitionForSkolem(TNode k) const;
+  /**
+   * Notify that the given literal has been asserted. This method adds skolems
+   * that become "active" as a result of asserting this literal. A skolem
+   * is active in the SAT context if it appears in an asserted literal.
+   */
+  void notifyAsserted(TNode literal, std::vector<TNode>& activatedSkolems);
+
+  /**
+   * Get the set of skolems maintained by this class that occur in node n,
+   * add them to skolems.
+   *
+   * @param n The node to traverse
+   * @param skolems The set where the skolems are added
+   */
+  void getSkolems(TNode n,
+                  std::unordered_set<Node, NodeHashFunction>& skolems) const;
+  /** Does n have skolems having definitions managed by this class? */
+  bool hasSkolems(TNode n) const;
+
+ private:
+  /** skolems to definitions (user-context dependent) */
+  NodeNodeMap d_skDefs;
+  /** set of active skolems (SAT-context dependent) */
+  NodeSet d_skActive;
+};
+
+}  // namespace prop
+}  // namespace CVC4
+
+#endif /* CVC4__PROP__SKOLEM_DEF_MANAGER_H */
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 5ee472b93..66023cd88 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -42,7 +42,8 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine,
       d_decisionEngine(decisionEngine),
       d_theoryEngine(theoryEngine),
       d_queue(context),
-      d_tpp(*theoryEngine, userContext, pnm)
+      d_tpp(*theoryEngine, userContext, pnm),
+      d_skdm(new SkolemDefManager(context, userContext))
 {
 }
 
@@ -52,6 +53,29 @@ TheoryProxy::~TheoryProxy() {
 
 void TheoryProxy::finishInit(CnfStream* cnfStream) { d_cnfStream = cnfStream; }
 
+void TheoryProxy::notifyPreprocessedAssertions(
+    const std::vector<Node>& assertions)
+{
+  d_theoryEngine->notifyPreprocessedAssertions(assertions);
+  for (const Node& assertion : assertions)
+  {
+    d_decisionEngine->addAssertion(assertion);
+  }
+}
+
+void TheoryProxy::notifyAssertion(Node lem, TNode skolem)
+{
+  if (skolem.isNull())
+  {
+    d_decisionEngine->addAssertion(lem);
+  }
+  else
+  {
+    d_skdm->notifySkolemDefinition(skolem, lem);
+    d_decisionEngine->addSkolemDefinition(lem, skolem);
+  }
+}
+
 void TheoryProxy::variableNotify(SatVariable var) {
   d_theoryEngine->preRegister(getNode(SatLiteral(var)));
 }
@@ -194,16 +218,15 @@ theory::TrustNode TheoryProxy::removeItes(
 }
 
 void TheoryProxy::getSkolems(TNode node,
-                             std::vector<theory::TrustNode>& skAsserts,
+                             std::vector<Node>& skAsserts,
                              std::vector<Node>& sks)
 {
-  RemoveTermFormulas& rtf = d_tpp.getRemoveTermFormulas();
   std::unordered_set<Node, NodeHashFunction> skolems;
-  rtf.getSkolems(node, skolems);
+  d_skdm->getSkolems(node, skolems);
   for (const Node& k : skolems)
   {
     sks.push_back(k);
-    skAsserts.push_back(rtf.getLemmaForSkolem(k));
+    skAsserts.push_back(d_skdm->getDefinitionForSkolem(k));
   }
 }
 
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 83c64d726..01d98f1b9 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -29,6 +29,7 @@
 #include "expr/node.h"
 #include "prop/registrar.h"
 #include "prop/sat_solver_types.h"
+#include "prop/skolem_def_manager.h"
 #include "theory/theory.h"
 #include "theory/theory_preprocessor.h"
 #include "theory/trust_node.h"
@@ -62,6 +63,12 @@ class TheoryProxy : public Registrar
   /** Finish initialize */
   void finishInit(CnfStream* cnfStream);
 
+  /** Notify (preprocessed) assertions. */
+  void notifyPreprocessedAssertions(const std::vector<Node>& assertions);
+
+  /** Notify a lemma, possibly corresponding to a skolem definition */
+  void notifyAssertion(Node lem, TNode skolem = TNode::null());
+
   void theoryCheck(theory::Theory::Effort effort);
 
   void explainPropagation(SatLiteral l, SatClause& explanation);
@@ -124,7 +131,7 @@ class TheoryProxy : public Registrar
    * fixed point is reached.
    */
   void getSkolems(TNode node,
-                  std::vector<theory::TrustNode>& skAsserts,
+                  std::vector<Node>& skAsserts,
                   std::vector<Node>& sks);
   /** Preregister term */
   void preRegister(Node n) override;
@@ -153,6 +160,9 @@ class TheoryProxy : public Registrar
 
   /** The theory preprocessor */
   theory::TheoryPreprocessor d_tpp;
+
+  /** The skolem definition manager */
+  std::unique_ptr<SkolemDefManager> d_skdm;
 }; /* class TheoryProxy */
 
 }/* CVC4::prop namespace */
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 6f2f77a14..6202ab80c 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -34,7 +34,6 @@ RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u,
                                        ProofNodeManager* pnm)
     : d_tfCache(u),
       d_skolem_cache(u),
-      d_lemmaCache(u),
       d_pnm(pnm),
       d_tpg(nullptr),
       d_lp(nullptr)
@@ -503,12 +502,6 @@ Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr,
 
       newLem = theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get());
 
-      // store in the lemma cache, if it is not already there.
-      if (d_lemmaCache.find(skolem) == d_lemmaCache.end())
-      {
-        d_lemmaCache.insert(skolem, newLem);
-      }
-
       Trace("rtf-proof-debug") << "Checking closed..." << std::endl;
       newLem.debugCheckClosed("rtf-proof-debug",
                               "RemoveTermFormulas::run:new_assert");
@@ -533,110 +526,6 @@ Node RemoveTermFormulas::getSkolemForNode(Node k) const
   return Node::null();
 }
 
-struct HasSkolemTag
-{
-};
-struct HasSkolemComputedTag
-{
-};
-/** Attribute true for nodes with skolems in them */
-typedef expr::Attribute<HasSkolemTag, bool> HasSkolemAttr;
-/** Attribute true for nodes where we have computed the above attribute */
-typedef expr::Attribute<HasSkolemComputedTag, bool> HasSkolemComputedAttr;
-
-bool RemoveTermFormulas::hasSkolems(TNode n) const
-{
-  std::unordered_set<TNode, TNodeHashFunction> visited;
-  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
-  std::vector<TNode> visit;
-  TNode cur;
-  visit.push_back(n);
-  do
-  {
-    cur = visit.back();
-    if (cur.getAttribute(HasSkolemComputedAttr()))
-    {
-      visit.pop_back();
-      // already computed
-      continue;
-    }
-    it = visited.find(cur);
-    if (it == visited.end())
-    {
-      visited.insert(cur);
-      if (cur.getNumChildren() == 0)
-      {
-        visit.pop_back();
-        bool hasSkolem = false;
-        if (cur.isVar())
-        {
-          hasSkolem = (d_lemmaCache.find(cur) != d_lemmaCache.end());
-        }
-        cur.setAttribute(HasSkolemAttr(), hasSkolem);
-        cur.setAttribute(HasSkolemComputedAttr(), true);
-      }
-      else
-      {
-        visit.insert(visit.end(), cur.begin(), cur.end());
-      }
-    }
-    else
-    {
-      visit.pop_back();
-      bool hasSkolem = false;
-      for (TNode i : cur)
-      {
-        Assert(i.getAttribute(HasSkolemComputedAttr()));
-        if (i.getAttribute(HasSkolemAttr()))
-        {
-          hasSkolem = true;
-          break;
-        }
-      }
-      cur.setAttribute(HasSkolemAttr(), hasSkolem);
-      cur.setAttribute(HasSkolemComputedAttr(), true);
-    }
-  } while (!visit.empty());
-  Assert(n.getAttribute(HasSkolemComputedAttr()));
-  return n.getAttribute(HasSkolemAttr());
-}
-
-void RemoveTermFormulas::getSkolems(
-    TNode n, std::unordered_set<Node, NodeHashFunction>& skolems) const
-{
-  std::unordered_set<TNode, TNodeHashFunction> visited;
-  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
-  std::vector<TNode> visit;
-  TNode cur;
-  visit.push_back(n);
-  do
-  {
-    cur = visit.back();
-    visit.pop_back();
-    if (!hasSkolems(cur))
-    {
-      // does not have skolems, continue
-      continue;
-    }
-    it = visited.find(cur);
-    if (it == visited.end())
-    {
-      visited.insert(cur);
-      if (cur.isVar())
-      {
-        if (d_lemmaCache.find(cur) != d_lemmaCache.end())
-        {
-          skolems.insert(cur);
-        }
-      }
-      else
-      {
-        visit.insert(visit.end(), cur.begin(), cur.end());
-      }
-    }
-  } while (!visit.empty());
-}
-
 Node RemoveTermFormulas::getAxiomFor(Node n)
 {
   NodeManager* nm = NodeManager::currentNM();
@@ -648,17 +537,6 @@ Node RemoveTermFormulas::getAxiomFor(Node n)
   return Node::null();
 }
 
-theory::TrustNode RemoveTermFormulas::getLemmaForSkolem(TNode n) const
-{
-  context::CDInsertHashMap<Node, theory::TrustNode, NodeHashFunction>::
-      const_iterator it = d_lemmaCache.find(n);
-  if (it == d_lemmaCache.end())
-  {
-    return theory::TrustNode::null();
-  }
-  return (*it).second;
-}
-
 ProofGenerator* RemoveTermFormulas::getTConvProofGenerator()
 {
   return d_tpg.get();
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index b6abaaa1f..22d5870b7 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -124,26 +124,6 @@ class RemoveTermFormulas {
    */
   static Node getAxiomFor(Node n);
 
-  /**
-   * Get the set of skolems introduced by this class that occur in node n,
-   * add them to skolems.
-   *
-   * @param n The node to traverse
-   * @param skolems The set where the skolems are added
-   */
-  void getSkolems(TNode n,
-                  std::unordered_set<Node, NodeHashFunction>& skolems) const;
-  /**
-   * Does n have skolems introduced by this class?
-   */
-  bool hasSkolems(TNode n) const;
-
-  /**
-   * Get the lemma for the skolem, or the null node if k is not a skolem this
-   * class introduced.
-   */
-  theory::TrustNode getLemmaForSkolem(TNode k) const;
-
  private:
   typedef context::CDInsertHashMap<
       std::pair<Node, uint32_t>,
@@ -177,11 +157,6 @@ class RemoveTermFormulas {
    *   d_tfCache[<ite( G, a, b ),0>] = d_tfCache[<ite( G, a, b ),1>] = k.
    */
   context::CDInsertHashMap<Node, Node, NodeHashFunction> d_skolem_cache;
-  /**
-   * Mapping from skolems to their corresponding lemma.
-   */
-  context::CDInsertHashMap<Node, theory::TrustNode, NodeHashFunction>
-      d_lemmaCache;
 
   /** gets the skolem for node
    *