Update proof namespaces (#6614)

This removes namespace theory from proof utilities, and moves MethodId to its own file in src/proof/.

1 files changed, 5 insertions, 5 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 676351dd5..85cd7e6b3 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -810,7 +810,7 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(
   return solveStatus;
 }
 
-theory::TrustNode TheoryEngine::ppRewriteEquality(TNode eq)
+TrustNode TheoryEngine::ppRewriteEquality(TNode eq)
 {
   Assert(eq.getKind() == kind::EQUAL);
   std::vector<SkolemLemma> lems;
@@ -1297,7 +1297,7 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The
   }
 }
 
-void TheoryEngine::lemma(theory::TrustNode tlemma,
+void TheoryEngine::lemma(TrustNode tlemma,
                          theory::LemmaProperty p,
                          theory::TheoryId atomsTo,
                          theory::TheoryId from)
@@ -1368,7 +1368,7 @@ void TheoryEngine::lemma(theory::TrustNode tlemma,
   d_lemmasAdded = true;
 }
 
-void TheoryEngine::conflict(theory::TrustNode tconflict, TheoryId theoryId)
+void TheoryEngine::conflict(TrustNode tconflict, TheoryId theoryId)
 {
   Assert(tconflict.getKind() == TrustNodeKind::CONFLICT);
   TNode conflict = tconflict.getNode();
@@ -1486,7 +1486,7 @@ void TheoryEngine::setIncomplete(theory::TheoryId theory,
   d_incompleteId = id;
 }
 
-theory::TrustNode TheoryEngine::getExplanation(
+TrustNode TheoryEngine::getExplanation(
     std::vector<NodeTheoryPair>& explanationVector)
 {
   Assert(explanationVector.size() == 1);
@@ -1788,7 +1788,7 @@ theory::TrustNode TheoryEngine::getExplanation(
     return trn;
   }
 
-  return theory::TrustNode::mkTrustPropExp(conclusion, expNode, nullptr);
+  return TrustNode::mkTrustPropExp(conclusion, expNode, nullptr);
 }
 
 bool TheoryEngine::isProofEnabled() const { return d_pnm != nullptr; }