(proof-new) Adding API for converting EqProof into ProofNode (#4747)

Also puts EqProof into its own module. Next will come the implementation of the API.

1 files changed, 0 insertions, 61 deletions

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 1dd9ba8b6..b532bcfa5 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -2412,67 +2412,6 @@ bool EqClassIterator::isFinished() const {
   return d_current == null_id;
 }
 
-void EqProof::debug_print(const char* c, unsigned tb, PrettyPrinter* prettyPrinter) const {
-  std::stringstream ss;
-  debug_print(ss, tb, prettyPrinter);
-  Debug(c) << ss.str();
-}
-void EqProof::debug_print(std::ostream& os,
-                          unsigned tb,
-                          PrettyPrinter* prettyPrinter) const
-{
-  for (unsigned i = 0; i < tb; i++)
-  {
-    os << "  ";
-  }
-
-  if (prettyPrinter)
-  {
-    os << prettyPrinter->printTag(d_id);
-  }
-  else
-  {
-    os << static_cast<MergeReasonType>(d_id);
-  }
-  os << "(";
-  if (d_children.empty() && d_node.isNull())
-  {
-    os << ")";
-    return;
-  }
-  if (!d_node.isNull())
-  {
-    os << std::endl;
-    for (unsigned i = 0; i < tb + 1; ++i)
-    {
-      os << "  ";
-    }
-    os << d_node << (!d_children.empty() ? "," : "");
-  }
-  unsigned size = d_children.size();
-  for (unsigned i = 0; i < size; ++i)
-  {
-    os << std::endl;
-    d_children[i]->debug_print(os, tb + 1, prettyPrinter);
-    if (i < size - 1)
-    {
-      for (unsigned j = 0; j < tb + 1; ++j)
-      {
-        os << "  ";
-      }
-      os << ",";
-    }
-  }
-  if (size > 0)
-  {
-    for (unsigned i = 0; i < tb; ++i)
-    {
-      os << "  ";
-    }
-  }
-  os << ")" << std::endl;
-}
-
 } // Namespace uf
 } // Namespace theory
 } // Namespace CVC4