1 files changed, 0 insertions, 56 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