2 files changed, 2 insertions, 85 deletions

diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index c8f5ebb4d..5811257ed 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -573,62 +573,6 @@ void ProofEqEngine::explainWithProof(Node lit,
   Trace("pfee-proof") << "pfee::explainWithProof: finished" << std::endl;
 }
 
-
-ProofEqEngine::FactProofGenerator::FactProofGenerator(context::Context* c,
-                                                      ProofNodeManager* pnm)
-    : ProofGenerator(), d_facts(c), d_pnm(pnm)
-{
-}
-
-bool ProofEqEngine::FactProofGenerator::addStep(Node fact, ProofStep ps)
-{
-  if (d_facts.find(fact) != d_facts.end())
-  {
-    // duplicate
-    return false;
-  }
-  Node symFact = CDProof::getSymmFact(fact);
-  if (!symFact.isNull())
-  {
-    if (d_facts.find(symFact) != d_facts.end())
-    {
-      // duplicate due to symmetry
-      return false;
-    }
-  }
-  d_facts.insert(fact, std::make_shared<ProofStep>(ps));
-  return true;
-}
-
-std::shared_ptr<ProofNode> ProofEqEngine::FactProofGenerator::getProofFor(
-    Node fact)
-{
-  Trace("pfee-fact-gen") << "FactProofGenerator::getProofFor: " << fact
-                         << std::endl;
-  NodeProofStepMap::iterator it = d_facts.find(fact);
-  if (it == d_facts.end())
-  {
-    Node symFact = CDProof::getSymmFact(fact);
-    if (symFact.isNull())
-    {
-      Trace("pfee-fact-gen") << "...cannot find step" << std::endl;
-      Assert(false);
-      return nullptr;
-    }
-    it = d_facts.find(symFact);
-    if (it == d_facts.end())
-    {
-      Assert(false);
-      Trace("pfee-fact-gen") << "...cannot find step (no sym)" << std::endl;
-      return nullptr;
-    }
-  }
-  Trace("pfee-fact-gen") << "...return via step " << *(*it).second << std::endl;
-  CDProof cdp(d_pnm);
-  cdp.addStep(fact, *(*it).second);
-  return cdp.getProofFor(fact);
-}
-
 }  // namespace eq
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h
index 49fde759e..67740d51f 100644
--- a/src/theory/uf/proof_equality_engine.h
+++ b/src/theory/uf/proof_equality_engine.h
@@ -22,11 +22,11 @@
 
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
+#include "expr/buffered_proof_generator.h"
 #include "expr/lazy_proof.h"
 #include "expr/node.h"
 #include "expr/proof_node.h"
 #include "expr/proof_node_manager.h"
-#include "expr/proof_step_buffer.h"
 #include "theory/eager_proof_generator.h"
 #include "theory/uf/equality_engine.h"
 
@@ -243,33 +243,6 @@ class ProofEqEngine : public EagerProofGenerator
   TrustNode explain(Node conc);
 
  private:
-  /**
-   * The default proof generator (for simple facts). This class is a context
-   * dependent mapping from formulas to proof steps. It does not generate
-   * ProofNode until it is asked to provide a proof for a given fact.
-   */
-  class FactProofGenerator : public ProofGenerator
-  {
-    typedef context::
-        CDHashMap<Node, std::shared_ptr<ProofStep>, NodeHashFunction>
-            NodeProofStepMap;
-
-   public:
-    FactProofGenerator(context::Context* c, ProofNodeManager* pnm);
-    ~FactProofGenerator() {}
-    /** add step */
-    bool addStep(Node fact, ProofStep ps);
-    /** Get proof for */
-    std::shared_ptr<ProofNode> getProofFor(Node f) override;
-    /** identify */
-    std::string identify() const override { return "FactProofGenerator"; }
-
-   private:
-    /** maps expected to ProofStep */
-    NodeProofStepMap d_facts;
-    /** the proof node manager */
-    ProofNodeManager* d_pnm;
-  };
   /** Assert internal */
   bool assertFactInternal(TNode pred, bool polarity, TNode reason);
   /** holds */
@@ -302,7 +275,7 @@ class ProofEqEngine : public EagerProofGenerator
   /** Reference to the equality engine */
   eq::EqualityEngine& d_ee;
   /** The default proof generator (for simple facts) */
-  FactProofGenerator d_factPg;
+  BufferedProofGenerator d_factPg;
   /** common nodes */
   Node d_true;
   Node d_false;