Update proof namespaces (#6614)

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

49 files changed, 389 insertions, 379 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 0bdd1c4fe..5faeddbed 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -155,6 +155,8 @@ libcvc5_add_sources(
   proof/lazy_proof_chain.h
   proof/lazy_tree_proof_generator.cpp
   proof/lazy_tree_proof_generator.h
+  proof/method_id.cpp
+  proof/method_id.h
   proof/proof.cpp
   proof/proof.h
   proof/proof_checker.cpp
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index 5542cfcf3..665415772 100644
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -82,9 +82,9 @@ void AssertionPipeline::push_back(Node n,
   }
 }
 
-void AssertionPipeline::pushBackTrusted(theory::TrustNode trn)
+void AssertionPipeline::pushBackTrusted(TrustNode trn)
 {
-  Assert(trn.getKind() == theory::TrustNodeKind::LEMMA);
+  Assert(trn.getKind() == TrustNodeKind::LEMMA);
   // push back what was proven
   push_back(trn.getProven(), false, false, trn.getGenerator());
 }
@@ -105,14 +105,14 @@ void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen)
   d_nodes[i] = n;
 }
 
-void AssertionPipeline::replaceTrusted(size_t i, theory::TrustNode trn)
+void AssertionPipeline::replaceTrusted(size_t i, TrustNode trn)
 {
   if (trn.isNull())
   {
     // null trust node denotes no change, nothing to do
     return;
   }
-  Assert(trn.getKind() == theory::TrustNodeKind::REWRITE);
+  Assert(trn.getKind() == TrustNodeKind::REWRITE);
   Assert(trn.getProven()[0] == d_nodes[i]);
   replace(i, trn.getNode(), trn.getGenerator());
 }
diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h
index af88d5164..b6bd8a94c 100644
--- a/src/preprocessing/assertion_pipeline.h
+++ b/src/preprocessing/assertion_pipeline.h
@@ -72,7 +72,7 @@ class AssertionPipeline
                  bool isInput = false,
                  ProofGenerator* pg = nullptr);
   /** Same as above, with TrustNode */
-  void pushBackTrusted(theory::TrustNode trn);
+  void pushBackTrusted(TrustNode trn);
 
   /**
    * Get the constant reference to the underlying assertions. It is only
@@ -97,7 +97,7 @@ class AssertionPipeline
    * Same as above, with TrustNode trn, which is of kind REWRITE and proves
    * d_nodes[i] = n for some n.
    */
-  void replaceTrusted(size_t i, theory::TrustNode trn);
+  void replaceTrusted(size_t i, TrustNode trn);
 
   IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; }
   const IteSkolemMap& getIteSkolemMap() const { return d_iteSkolemMap; }
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index dc47c9c8e..7578bcad6 100644
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -47,7 +47,7 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
   for (unsigned i = 0, size = assertions->size(); i < size; ++i)
   {
     Node assertion = (*assertions)[i];
-    std::vector<theory::TrustNode> newAsserts;
+    std::vector<TrustNode> newAsserts;
     std::vector<Node> newSkolems;
     TrustNode trn = pe->removeItes(assertion, newAsserts, newSkolems);
     if (!trn.isNull())
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 921442f0e..b05dbbe1c 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -474,7 +474,7 @@ Node NonClausalSimp::processLearnedLit(Node lit,
   return lit;
 }
 
-Node NonClausalSimp::processRewrittenLearnedLit(theory::TrustNode trn)
+Node NonClausalSimp::processRewrittenLearnedLit(TrustNode trn)
 {
   if (isProofEnabled())
   {
diff --git a/src/preprocessing/passes/non_clausal_simp.h b/src/preprocessing/passes/non_clausal_simp.h
index de16cc49a..329542f38 100644
--- a/src/preprocessing/passes/non_clausal_simp.h
+++ b/src/preprocessing/passes/non_clausal_simp.h
@@ -76,7 +76,7 @@ class NonClausalSimp : public PreprocessingPass
    * This tracks the proof in the learned literal preprocess proof generator
    * d_llpg below and returns the rewritten learned literal.
    */
-  Node processRewrittenLearnedLit(theory::TrustNode trn);
+  Node processRewrittenLearnedLit(TrustNode trn);
   /** Is proof enabled? */
   bool isProofEnabled() const;
   /** The proof node manager */
diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp
index 1eb21cd96..641cab162 100644
--- a/src/preprocessing/passes/theory_preprocess.cpp
+++ b/src/preprocessing/passes/theory_preprocess.cpp
@@ -44,7 +44,7 @@ PreprocessingPassResult TheoryPreprocess::applyInternal(
   for (unsigned i = 0, size = assertions->size(); i < size; ++i)
   {
     Node assertion = (*assertions)[i];
-    std::vector<theory::TrustNode> newAsserts;
+    std::vector<TrustNode> newAsserts;
     std::vector<Node> newSkolems;
     TrustNode trn = propEngine->preprocess(assertion, newAsserts, newSkolems);
     if (!trn.isNull())
diff --git a/src/preprocessing/passes/theory_rewrite_eq.cpp b/src/preprocessing/passes/theory_rewrite_eq.cpp
index 44aedc754..93ba2b7cd 100644
--- a/src/preprocessing/passes/theory_rewrite_eq.cpp
+++ b/src/preprocessing/passes/theory_rewrite_eq.cpp
@@ -45,7 +45,7 @@ PreprocessingPassResult TheoryRewriteEq::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-theory::TrustNode TheoryRewriteEq::rewriteAssertion(TNode n)
+TrustNode TheoryRewriteEq::rewriteAssertion(TNode n)
 {
   NodeManager* nm = NodeManager::currentNM();
   TheoryEngine* te = d_preprocContext->getTheoryEngine();
@@ -97,7 +97,7 @@ theory::TrustNode TheoryRewriteEq::rewriteAssertion(TNode n)
       if (ret.getKind() == kind::EQUAL && !ret[0].getType().isBoolean())
       {
         // For example, (= x y) ---> (and (>= x y) (<= x y))
-        theory::TrustNode trn = te->ppRewriteEquality(ret);
+        TrustNode trn = te->ppRewriteEquality(ret);
         // can make proof producing by using proof generator from trn
         ret = trn.isNull() ? Node(ret) : trn.getNode();
       }
diff --git a/src/preprocessing/passes/theory_rewrite_eq.h b/src/preprocessing/passes/theory_rewrite_eq.h
index 2312c38ed..73d20f77c 100644
--- a/src/preprocessing/passes/theory_rewrite_eq.h
+++ b/src/preprocessing/passes/theory_rewrite_eq.h
@@ -47,7 +47,7 @@ class TheoryRewriteEq : public PreprocessingPass
    *   (= x y) ---> (and (>= x y) (<= x y))
    * Returns the trust node corresponding to the rewrite.
    */
-  theory::TrustNode rewriteAssertion(TNode assertion);
+  TrustNode rewriteAssertion(TNode assertion);
 };
 
 }  // namespace passes
diff --git a/src/proof/conv_seq_proof_generator.cpp b/src/proof/conv_seq_proof_generator.cpp
index 65a7e462b..7b6a06ddd 100644
--- a/src/proof/conv_seq_proof_generator.cpp
+++ b/src/proof/conv_seq_proof_generator.cpp
@@ -122,13 +122,13 @@ std::shared_ptr<ProofNode> TConvSeqProofGenerator::getSubsequenceProofFor(
   return d_pnm->mkTrans(transChildren, f);
 }
 
-theory::TrustNode TConvSeqProofGenerator::mkTrustRewriteSequence(
+TrustNode TConvSeqProofGenerator::mkTrustRewriteSequence(
     const std::vector<Node>& cterms)
 {
   Assert(cterms.size() == d_tconvs.size() + 1);
   if (cterms[0] == cterms[cterms.size() - 1])
   {
-    return theory::TrustNode::null();
+    return TrustNode::null();
   }
   bool useThis = false;
   ProofGenerator* pg = nullptr;
@@ -163,8 +163,7 @@ theory::TrustNode TConvSeqProofGenerator::mkTrustRewriteSequence(
     }
   }
   Assert(pg != nullptr);
-  return theory::TrustNode::mkTrustRewrite(
-      cterms[0], cterms[cterms.size() - 1], pg);
+  return TrustNode::mkTrustRewrite(cterms[0], cterms[cterms.size() - 1], pg);
 }
 
 std::string TConvSeqProofGenerator::identify() const { return d_name; }
diff --git a/src/proof/conv_seq_proof_generator.h b/src/proof/conv_seq_proof_generator.h
index 8d4417134..ac8663b58 100644
--- a/src/proof/conv_seq_proof_generator.h
+++ b/src/proof/conv_seq_proof_generator.h
@@ -98,7 +98,7 @@ class TConvSeqProofGenerator : public ProofGenerator
    * then we return a trust node proving (= d e) with the 2nd component proof
    * generator, as it alone is capable of proving this equality.
    */
-  theory::TrustNode mkTrustRewriteSequence(const std::vector<Node>& cterms);
+  TrustNode mkTrustRewriteSequence(const std::vector<Node>& cterms);
 
  protected:
   using NodeIndexPairHashFunction =
diff --git a/src/proof/eager_proof_generator.cpp b/src/proof/eager_proof_generator.cpp
index 34ff4fa75..2a86f982c 100644
--- a/src/proof/eager_proof_generator.cpp
+++ b/src/proof/eager_proof_generator.cpp
@@ -20,7 +20,6 @@
 #include "proof/proof_node_manager.h"
 
 namespace cvc5 {
-namespace theory {
 
 EagerProofGenerator::EagerProofGenerator(ProofNodeManager* pnm,
                                          context::Context* c,
@@ -155,5 +154,4 @@ TrustNode EagerProofGenerator::mkTrustNodeSplit(Node f)
 
 std::string EagerProofGenerator::identify() const { return d_name; }
 
-}  // namespace theory
 }  // namespace cvc5
diff --git a/src/proof/eager_proof_generator.h b/src/proof/eager_proof_generator.h
index ada48d893..90e2787fd 100644
--- a/src/proof/eager_proof_generator.h
+++ b/src/proof/eager_proof_generator.h
@@ -29,8 +29,6 @@ namespace cvc5 {
 class ProofNode;
 class ProofNodeManager;
 
-namespace theory {
-
 /**
  * An eager proof generator, with explicit proof caching.
  *
@@ -191,7 +189,6 @@ class EagerProofGenerator : public ProofGenerator
   NodeProofNodeMap d_proofs;
 };
 
-}  // namespace theory
 }  // namespace cvc5
 
 #endif /* CVC5__PROOF__PROOF_GENERATOR_H */
diff --git a/src/proof/lazy_tree_proof_generator.cpp b/src/proof/lazy_tree_proof_generator.cpp
index a50b9efd4..225a6c75c 100644
--- a/src/proof/lazy_tree_proof_generator.cpp
+++ b/src/proof/lazy_tree_proof_generator.cpp
@@ -23,7 +23,6 @@
 #include "proof/proof_node_manager.h"
 
 namespace cvc5 {
-namespace theory {
 
 LazyTreeProofGenerator::LazyTreeProofGenerator(ProofNodeManager* pnm,
                                                const std::string& name)
@@ -142,5 +141,4 @@ std::ostream& operator<<(std::ostream& os, const LazyTreeProofGenerator& ltpg)
   return os;
 }
 
-}  // namespace theory
 }  // namespace cvc5
diff --git a/src/proof/lazy_tree_proof_generator.h b/src/proof/lazy_tree_proof_generator.h
index 8b8d344e9..ff5d0ad2e 100644
--- a/src/proof/lazy_tree_proof_generator.h
+++ b/src/proof/lazy_tree_proof_generator.h
@@ -25,7 +25,6 @@
 #include "proof/proof_node_manager.h"
 
 namespace cvc5 {
-namespace theory {
 namespace detail {
 /**
  * A single node in the proof tree created by the LazyTreeProofGenerator.
@@ -217,7 +216,6 @@ class LazyTreeProofGenerator : public ProofGenerator
  */
 std::ostream& operator<<(std::ostream& os, const LazyTreeProofGenerator& ltpg);
 
-}  // namespace theory
 }  // namespace cvc5
 
 #endif
diff --git a/src/proof/method_id.cpp b/src/proof/method_id.cpp
new file mode 100644
index 000000000..c5e8458cd
--- /dev/null
+++ b/src/proof/method_id.cpp
@@ -0,0 +1,118 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Implementation of method identifier
+ */
+
+#include "proof/method_id.h"
+
+#include "proof/proof_checker.h"
+#include "util/rational.h"
+
+namespace cvc5 {
+
+const char* toString(MethodId id)
+{
+  switch (id)
+  {
+    case MethodId::RW_REWRITE: return "RW_REWRITE";
+    case MethodId::RW_EXT_REWRITE: return "RW_EXT_REWRITE";
+    case MethodId::RW_REWRITE_EQ_EXT: return "RW_REWRITE_EQ_EXT";
+    case MethodId::RW_EVALUATE: return "RW_EVALUATE";
+    case MethodId::RW_IDENTITY: return "RW_IDENTITY";
+    case MethodId::RW_REWRITE_THEORY_PRE: return "RW_REWRITE_THEORY_PRE";
+    case MethodId::RW_REWRITE_THEORY_POST: return "RW_REWRITE_THEORY_POST";
+    case MethodId::SB_DEFAULT: return "SB_DEFAULT";
+    case MethodId::SB_LITERAL: return "SB_LITERAL";
+    case MethodId::SB_FORMULA: return "SB_FORMULA";
+    case MethodId::SBA_SEQUENTIAL: return "SBA_SEQUENTIAL";
+    case MethodId::SBA_SIMUL: return "SBA_SIMUL";
+    case MethodId::SBA_FIXPOINT: return "SBA_FIXPOINT";
+    default: return "MethodId::Unknown";
+  };
+}
+
+std::ostream& operator<<(std::ostream& out, MethodId id)
+{
+  out << toString(id);
+  return out;
+}
+
+Node mkMethodId(MethodId id)
+{
+  return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(id)));
+}
+
+bool getMethodId(TNode n, MethodId& i)
+{
+  uint32_t index;
+  if (!ProofRuleChecker::getUInt32(n, index))
+  {
+    return false;
+  }
+  i = static_cast<MethodId>(index);
+  return true;
+}
+
+bool getMethodIds(const std::vector<Node>& args,
+                  MethodId& ids,
+                  MethodId& ida,
+                  MethodId& idr,
+                  size_t index)
+{
+  ids = MethodId::SB_DEFAULT;
+  ida = MethodId::SBA_SEQUENTIAL;
+  idr = MethodId::RW_REWRITE;
+  for (size_t offset = 0; offset <= 2; offset++)
+  {
+    if (args.size() > index + offset)
+    {
+      MethodId& id = offset == 0 ? ids : (offset == 1 ? ida : idr);
+      if (!getMethodId(args[index + offset], id))
+      {
+        Trace("builtin-pfcheck")
+            << "Failed to get id from " << args[index + offset] << std::endl;
+        return false;
+      }
+    }
+    else
+    {
+      break;
+    }
+  }
+  Trace("builtin-pfcheck") << "Got MethodIds ids/ida/idr: " << ids << " / "
+                           << ida << " / " << idr << "\n";
+  return true;
+}
+
+void addMethodIds(std::vector<Node>& args,
+                  MethodId ids,
+                  MethodId ida,
+                  MethodId idr)
+{
+  bool ndefRewriter = (idr != MethodId::RW_REWRITE);
+  bool ndefApply = (ida != MethodId::SBA_SEQUENTIAL);
+  if (ids != MethodId::SB_DEFAULT || ndefRewriter || ndefApply)
+  {
+    args.push_back(mkMethodId(ids));
+  }
+  if (ndefApply || ndefRewriter)
+  {
+    args.push_back(mkMethodId(ida));
+  }
+  if (ndefRewriter)
+  {
+    args.push_back(mkMethodId(idr));
+  }
+}
+
+}  // namespace cvc5
diff --git a/src/proof/method_id.h b/src/proof/method_id.h
new file mode 100644
index 000000000..b353232f4
--- /dev/null
+++ b/src/proof/method_id.h
@@ -0,0 +1,109 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Method identifier enumeration
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__PROOF__METHOD_ID_H
+#define CVC5__PROOF__METHOD_ID_H
+
+#include "expr/node.h"
+
+namespace cvc5 {
+
+/**
+ * Identifiers for rewriters and substitutions, which we abstractly
+ * classify as "methods".  Methods have a unique identifier in the internal
+ * proof calculus implemented by the checker below.
+ *
+ * A "rewriter" is abstractly a method from Node to Node, where the output
+ * is semantically equivalent to the input. The identifiers below list
+ * various methods that have this contract. This identifier is used
+ * in a number of the builtin rules.
+ *
+ * A substitution is a method for turning a formula into a substitution.
+ */
+enum class MethodId : uint32_t
+{
+  //---------------------------- Rewriters
+  // Rewriter::rewrite(n)
+  RW_REWRITE,
+  // d_ext_rew.extendedRewrite(n);
+  RW_EXT_REWRITE,
+  // Rewriter::rewriteExtEquality(n)
+  RW_REWRITE_EQ_EXT,
+  // Evaluator::evaluate(n)
+  RW_EVALUATE,
+  // identity
+  RW_IDENTITY,
+  // theory preRewrite, note this is only intended to be used as an argument
+  // to THEORY_REWRITE in the final proof. It is not implemented in
+  // applyRewrite below, see documentation in proof_rule.h for THEORY_REWRITE.
+  RW_REWRITE_THEORY_PRE,
+  // same as above, for theory postRewrite
+  RW_REWRITE_THEORY_POST,
+  //---------------------------- Substitutions
+  // (= x y) is interpreted as x -> y, using Node::substitute
+  SB_DEFAULT,
+  // P, (not P) are interpreted as P -> true, P -> false using Node::substitute
+  SB_LITERAL,
+  // P is interpreted as P -> true using Node::substitute
+  SB_FORMULA,
+  //---------------------------- Substitution applications
+  // multiple substitutions are applied sequentially
+  SBA_SEQUENTIAL,
+  // multiple substitutions are applied simultaneously
+  SBA_SIMUL,
+  // multiple substitutions are applied to fix point
+  SBA_FIXPOINT
+  // For example, for x -> u, y -> f(z), z -> g(x), applying this substituion to
+  // y gives:
+  // - f(g(x)) for SBA_SEQUENTIAL
+  // - f(z) for SBA_SIMUL
+  // - f(g(u)) for SBA_FIXPOINT
+  // Notice that SBA_FIXPOINT should provide a terminating rewrite system
+  // as a substitution, or else non-termination will occur during proof
+  // checking.
+};
+/** Converts a rewriter id to a string. */
+const char* toString(MethodId id);
+/** Write a rewriter id to out */
+std::ostream& operator<<(std::ostream& out, MethodId id);
+/** Make a method id node */
+Node mkMethodId(MethodId id);
+
+/** get a method identifier from a node, return false if we fail */
+bool getMethodId(TNode n, MethodId& i);
+/**
+ * Get method identifiers from args starting at the given index. Store their
+ * values into ids, ida, and idr. This method returns false if args does not
+ * contain valid method identifiers at position index in args.
+ */
+bool getMethodIds(const std::vector<Node>& args,
+                  MethodId& ids,
+                  MethodId& ida,
+                  MethodId& idr,
+                  size_t index);
+/**
+ * Add method identifiers ids, ida and idr as nodes to args. This does not add
+ * ids, ida or idr if their values are the default ones.
+ */
+void addMethodIds(std::vector<Node>& args,
+                  MethodId ids,
+                  MethodId ida,
+                  MethodId idr);
+
+}  // namespace cvc5
+
+#endif /* CVC5__PROOF__METHOD_ID_H */
diff --git a/src/proof/theory_proof_step_buffer.cpp b/src/proof/theory_proof_step_buffer.cpp
index f00c664c8..79e98471d 100644
--- a/src/proof/theory_proof_step_buffer.cpp
+++ b/src/proof/theory_proof_step_buffer.cpp
@@ -20,7 +20,6 @@
 using namespace cvc5::kind;
 
 namespace cvc5 {
-namespace theory {
 
 TheoryProofStepBuffer::TheoryProofStepBuffer(ProofChecker* pc)
     : ProofStepBuffer(pc)
@@ -36,7 +35,7 @@ bool TheoryProofStepBuffer::applyEqIntro(Node src,
 {
   std::vector<Node> args;
   args.push_back(src);
-  builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr);
+  addMethodIds(args, ids, ida, idr);
   Node res = tryStep(PfRule::MACRO_SR_EQ_INTRO, exp, args);
   if (res.isNull())
   {
@@ -73,7 +72,7 @@ bool TheoryProofStepBuffer::applyPredTransform(Node src,
   // try to prove that tgt rewrites to src
   children.insert(children.end(), exp.begin(), exp.end());
   args.push_back(tgt);
-  builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr);
+  addMethodIds(args, ids, ida, idr);
   Node res = tryStep(PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
   if (res.isNull())
   {
@@ -93,7 +92,7 @@ bool TheoryProofStepBuffer::applyPredIntro(Node tgt,
 {
   std::vector<Node> args;
   args.push_back(tgt);
-  builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr);
+  addMethodIds(args, ids, ida, idr);
   Node res = tryStep(PfRule::MACRO_SR_PRED_INTRO, exp, args);
   if (res.isNull())
   {
@@ -113,7 +112,7 @@ Node TheoryProofStepBuffer::applyPredElim(Node src,
   children.push_back(src);
   children.insert(children.end(), exp.begin(), exp.end());
   std::vector<Node> args;
-  builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr);
+  addMethodIds(args, ids, ida, idr);
   Node srcRew = tryStep(PfRule::MACRO_SR_PRED_ELIM, children, args);
   if (CDProof::isSame(src, srcRew))
   {
@@ -236,5 +235,4 @@ Node TheoryProofStepBuffer::elimDoubleNegLit(Node n)
   return n;
 }
 
-}  // namespace theory
 }  // namespace cvc5
diff --git a/src/proof/theory_proof_step_buffer.h b/src/proof/theory_proof_step_buffer.h
index fc2e25e5a..ac58d3718 100644
--- a/src/proof/theory_proof_step_buffer.h
+++ b/src/proof/theory_proof_step_buffer.h
@@ -25,7 +25,6 @@
 #include "theory/builtin/proof_checker.h"
 
 namespace cvc5 {
-namespace theory {
 /**
  * Class used to speculatively try and buffer a set of proof steps before
  * sending them to a proof object, extended with theory-specfic proof rule
@@ -114,7 +113,6 @@ class TheoryProofStepBuffer : public ProofStepBuffer
   Node elimDoubleNegLit(Node n);
 };
 
-}  // namespace theory
 }  // namespace cvc5
 
 #endif /* CVC5__PROOF__THEORY_PROOF_STEP_BUFFER_H */
diff --git a/src/proof/trust_node.cpp b/src/proof/trust_node.cpp
index d99e6de51..6c5de13c7 100644
--- a/src/proof/trust_node.cpp
+++ b/src/proof/trust_node.cpp
@@ -19,7 +19,6 @@
 #include "proof/proof_generator.h"
 
 namespace cvc5 {
-namespace theory {
 
 const char* toString(TrustNodeKind tnk)
 {
@@ -146,5 +145,4 @@ std::ostream& operator<<(std::ostream& out, TrustNode n)
   return out;
 }
 
-}  // namespace theory
 }  // namespace cvc5
diff --git a/src/proof/trust_node.h b/src/proof/trust_node.h
index 200dececd..8971df1d1 100644
--- a/src/proof/trust_node.h
+++ b/src/proof/trust_node.h
@@ -25,8 +25,6 @@ namespace cvc5 {
 class ProofGenerator;
 class ProofNode;
 
-namespace theory {
-
 /** A kind for trust nodes */
 enum class TrustNodeKind : uint32_t
 {
@@ -172,7 +170,6 @@ class TrustNode
  */
 std::ostream& operator<<(std::ostream& out, TrustNode n);
 
-}  // namespace theory
 }  // namespace cvc5
 
 #endif /* CVC5__PROOF__TRUST_NODE_H */
diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp
index 6a2430f82..d09854bce 100644
--- a/src/prop/proof_cnf_stream.cpp
+++ b/src/prop/proof_cnf_stream.cpp
@@ -515,7 +515,7 @@ void ProofCnfStream::convertAndAssertIte(TNode node, bool negated)
   }
 }
 
-void ProofCnfStream::convertPropagation(theory::TrustNode trn)
+void ProofCnfStream::convertPropagation(TrustNode trn)
 {
   Node proven = trn.getProven();
   Trace("cnf") << "ProofCnfStream::convertPropagation: proven explanation"
diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h
index 97abdb077..9972581c0 100644
--- a/src/prop/proof_cnf_stream.h
+++ b/src/prop/proof_cnf_stream.h
@@ -83,7 +83,7 @@ class ProofCnfStream : public ProofGenerator
    * clause in the SAT solver, as this is handled internally by the SAT
    * solver. The clausification steps and the generator within the trust node
    * are saved in d_proof if we are producing proofs in the theory engine. */
-  void convertPropagation(theory::TrustNode ttn);
+  void convertPropagation(TrustNode ttn);
   /**
    * Ensure that the given node will have a designated SAT literal that is
    * definitionally equal to it.  The result of this function is that the Node
@@ -162,7 +162,7 @@ class ProofCnfStream : public ProofGenerator
   LazyCDProof d_proof;
   /** An accumulator of steps that may be applied to normalize the clauses
    * generated during clausification. */
-  theory::TheoryProofStepBuffer d_psb;
+  TheoryProofStepBuffer d_psb;
   /** Blocked proofs.
    *
    * These are proof nodes added to this class by external generators. */
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index bcf75b43a..fe3a5ecff 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -158,18 +158,16 @@ PropEngine::~PropEngine() {
   delete d_theoryProxy;
 }
 
-theory::TrustNode PropEngine::preprocess(
-    TNode node,
-    std::vector<theory::TrustNode>& newLemmas,
-    std::vector<Node>& newSkolems)
+TrustNode PropEngine::preprocess(TNode node,
+                                 std::vector<TrustNode>& newLemmas,
+                                 std::vector<Node>& newSkolems)
 {
   return d_theoryProxy->preprocess(node, newLemmas, newSkolems);
 }
 
-theory::TrustNode PropEngine::removeItes(
-    TNode node,
-    std::vector<theory::TrustNode>& newLemmas,
-    std::vector<Node>& newSkolems)
+TrustNode PropEngine::removeItes(TNode node,
+                                 std::vector<TrustNode>& newLemmas,
+                                 std::vector<Node>& newSkolems)
 {
   return d_theoryProxy->removeItes(node, newLemmas, newSkolems);
 }
@@ -205,14 +203,14 @@ void PropEngine::assertInputFormulas(
   }
 }
 
-void PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p)
+void PropEngine::assertLemma(TrustNode tlemma, theory::LemmaProperty p)
 {
   bool removable = isLemmaPropertyRemovable(p);
 
   // call preprocessor
-  std::vector<theory::TrustNode> ppLemmas;
+  std::vector<TrustNode> ppLemmas;
   std::vector<Node> ppSkolems;
-  theory::TrustNode tplemma =
+  TrustNode tplemma =
       d_theoryProxy->preprocessLemma(tlemma, ppLemmas, ppSkolems);
 
   Assert(ppSkolems.size() == ppLemmas.size());
@@ -244,12 +242,11 @@ void PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p)
   assertLemmasInternal(tplemma, ppLemmas, ppSkolems, removable);
 }
 
-void PropEngine::assertTrustedLemmaInternal(theory::TrustNode trn,
-                                            bool removable)
+void PropEngine::assertTrustedLemmaInternal(TrustNode trn, bool removable)
 {
   Node node = trn.getNode();
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << std::endl;
-  bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT;
+  bool negated = trn.getKind() == TrustNodeKind::CONFLICT;
   Assert(
       !isProofEnabled() || trn.getGenerator() != nullptr
       || options::unsatCores()
@@ -296,17 +293,16 @@ void PropEngine::assertInternal(
   }
 }
 
-void PropEngine::assertLemmasInternal(
-    theory::TrustNode trn,
-    const std::vector<theory::TrustNode>& ppLemmas,
-    const std::vector<Node>& ppSkolems,
-    bool removable)
+void PropEngine::assertLemmasInternal(TrustNode trn,
+                                      const std::vector<TrustNode>& ppLemmas,
+                                      const std::vector<Node>& ppSkolems,
+                                      bool removable)
 {
   if (!trn.isNull())
   {
     assertTrustedLemmaInternal(trn, removable);
   }
-  for (const theory::TrustNode& tnl : ppLemmas)
+  for (const TrustNode& tnl : ppLemmas)
   {
     assertTrustedLemmaInternal(tnl, removable);
   }
@@ -513,11 +509,11 @@ Node PropEngine::ensureLiteral(TNode n)
 Node PropEngine::getPreprocessedTerm(TNode n)
 {
   // must preprocess
-  std::vector<theory::TrustNode> newLemmas;
+  std::vector<TrustNode> newLemmas;
   std::vector<Node> newSkolems;
-  theory::TrustNode tpn = d_theoryProxy->preprocess(n, newLemmas, newSkolems);
+  TrustNode tpn = d_theoryProxy->preprocess(n, newLemmas, newSkolems);
   // send lemmas corresponding to the skolems introduced by preprocessing n
-  theory::TrustNode trnNull;
+  TrustNode trnNull;
   assertLemmasInternal(trnNull, newLemmas, newSkolems, false);
   return tpn.isNull() ? Node(n) : tpn.getNode();
 }
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 8903d4bc3..74da49cf6 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -94,9 +94,9 @@ class PropEngine
    * @return The (REWRITE) trust node corresponding to rewritten node via
    * preprocessing.
    */
-  theory::TrustNode preprocess(TNode node,
-                               std::vector<theory::TrustNode>& ppLemmas,
-                               std::vector<Node>& ppSkolems);
+  TrustNode preprocess(TNode node,
+                       std::vector<TrustNode>& ppLemmas,
+                       std::vector<Node>& ppSkolems);
   /**
    * Remove term ITEs (and more generally, term formulas) from the given node.
    * Return the REWRITE trust node corresponding to rewriting node. New lemmas
@@ -110,9 +110,9 @@ class PropEngine
    * @return The (REWRITE) trust node corresponding to rewritten node via
    * preprocessing.
    */
-  theory::TrustNode removeItes(TNode node,
-                               std::vector<theory::TrustNode>& ppLemmas,
-                               std::vector<Node>& ppSkolems);
+  TrustNode removeItes(TNode node,
+                       std::vector<TrustNode>& ppLemmas,
+                       std::vector<Node>& ppSkolems);
 
   /**
    * Converts the given formulas to CNF and assert the CNF to the SAT solver.
@@ -136,7 +136,7 @@ class PropEngine
    * @param trn the trust node storing the formula to assert
    * @param p the properties of the lemma
    */
-  void assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p);
+  void assertLemma(TrustNode tlemma, theory::LemmaProperty p);
 
   /**
    * If ever n is decided upon, it must be in the given phase.  This
@@ -321,7 +321,7 @@ class PropEngine
    * @param removable whether this lemma can be quietly removed based
    * on an activity heuristic
    */
-  void assertTrustedLemmaInternal(theory::TrustNode trn, bool removable);
+  void assertTrustedLemmaInternal(TrustNode trn, bool removable);
   /**
    * Assert node as a formula to the CNF stream
    * @param node The formula to assert
@@ -342,8 +342,8 @@ class PropEngine
    * skolem definitions and skolems obtained from preprocessing it, and
    * removable is whether the lemma is removable.
    */
-  void assertLemmasInternal(theory::TrustNode trn,
-                            const std::vector<theory::TrustNode>& ppLemmas,
+  void assertLemmasInternal(TrustNode trn,
+                            const std::vector<TrustNode>& ppLemmas,
                             const std::vector<Node>& ppSkolems,
                             bool removable);
 
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index b0eab66e9..845289841 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -96,7 +96,7 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
   TNode lNode = d_cnfStream->getNode(l);
   Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;
 
-  theory::TrustNode tte = d_theoryEngine->getExplanation(lNode);
+  TrustNode tte = d_theoryEngine->getExplanation(lNode);
   Node theoryExplanation = tte.getNode();
   if (options::produceProofs()
       && options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS)
@@ -184,26 +184,23 @@ SatValue TheoryProxy::getDecisionPolarity(SatVariable var) {
 
 CnfStream* TheoryProxy::getCnfStream() { return d_cnfStream; }
 
-theory::TrustNode TheoryProxy::preprocessLemma(
-    theory::TrustNode trn,
-    std::vector<theory::TrustNode>& newLemmas,
-    std::vector<Node>& newSkolems)
+TrustNode TheoryProxy::preprocessLemma(TrustNode trn,
+                                       std::vector<TrustNode>& newLemmas,
+                                       std::vector<Node>& newSkolems)
 {
   return d_tpp.preprocessLemma(trn, newLemmas, newSkolems);
 }
 
-theory::TrustNode TheoryProxy::preprocess(
-    TNode node,
-    std::vector<theory::TrustNode>& newLemmas,
-    std::vector<Node>& newSkolems)
+TrustNode TheoryProxy::preprocess(TNode node,
+                                  std::vector<TrustNode>& newLemmas,
+                                  std::vector<Node>& newSkolems)
 {
   return d_tpp.preprocess(node, newLemmas, newSkolems);
 }
 
-theory::TrustNode TheoryProxy::removeItes(
-    TNode node,
-    std::vector<theory::TrustNode>& newLemmas,
-    std::vector<Node>& newSkolems)
+TrustNode TheoryProxy::removeItes(TNode node,
+                                  std::vector<TrustNode>& newLemmas,
+                                  std::vector<Node>& newSkolems)
 {
   RemoveTermFormulas& rtf = d_tpp.getRemoveTermFormulas();
   return rtf.run(node, newLemmas, newSkolems, true);
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index d6ae1f975..f988c00e2 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -105,22 +105,22 @@ class TheoryProxy : public Registrar
    * Call the preprocessor on node, return trust node corresponding to the
    * rewrite.
    */
-  theory::TrustNode preprocessLemma(theory::TrustNode trn,
-                                    std::vector<theory::TrustNode>& newLemmas,
-                                    std::vector<Node>& newSkolems);
+  TrustNode preprocessLemma(TrustNode trn,
+                            std::vector<TrustNode>& newLemmas,
+                            std::vector<Node>& newSkolems);
   /**
    * Call the preprocessor on node, return trust node corresponding to the
    * rewrite.
    */
-  theory::TrustNode preprocess(TNode node,
-                               std::vector<theory::TrustNode>& newLemmas,
-                               std::vector<Node>& newSkolems);
+  TrustNode preprocess(TNode node,
+                       std::vector<TrustNode>& newLemmas,
+                       std::vector<Node>& newSkolems);
   /**
    * Remove ITEs from the node.
    */
-  theory::TrustNode removeItes(TNode node,
-                               std::vector<theory::TrustNode>& newLemmas,
-                               std::vector<Node>& newSkolems);
+  TrustNode removeItes(TNode node,
+                       std::vector<TrustNode>& newLemmas,
+                       std::vector<Node>& newSkolems);
   /**
    * Get the skolems within node and their corresponding definitions, store
    * them in sks and skAsserts respectively. Note that this method does not
diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h
index ba89a1063..997e97391 100644
--- a/src/smt/expand_definitions.h
+++ b/src/smt/expand_definitions.h
@@ -64,9 +64,9 @@ class ExpandDefs
    * Helper function for above, called to specify if we want proof production
    * based on the optional argument tpg.
    */
-  theory::TrustNode expandDefinitions(TNode n,
-                                      std::unordered_map<Node, Node>& cache,
-                                      TConvProofGenerator* tpg);
+  TrustNode expandDefinitions(TNode n,
+                              std::unordered_map<Node, Node>& cache,
+                              TConvProofGenerator* tpg);
   /** Reference to the environment. */
   Env& d_env;
   /** Reference to the SMT stats */
diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp
index 3f657db63..12a802f14 100644
--- a/src/smt/preprocess_proof_generator.cpp
+++ b/src/smt/preprocess_proof_generator.cpp
@@ -59,7 +59,7 @@ void PreprocessProofGenerator::notifyNewAssert(Node n, ProofGenerator* pg)
     {
       checkEagerPedantic(d_ra);
     }
-    d_src[n] = theory::TrustNode::mkTrustLemma(n, pg);
+    d_src[n] = TrustNode::mkTrustLemma(n, pg);
   }
   else
   {
@@ -67,7 +67,7 @@ void PreprocessProofGenerator::notifyNewAssert(Node n, ProofGenerator* pg)
   }
 }
 
-void PreprocessProofGenerator::notifyNewTrustedAssert(theory::TrustNode tn)
+void PreprocessProofGenerator::notifyNewTrustedAssert(TrustNode tn)
 {
   notifyNewAssert(tn.getProven(), tn.getGenerator());
 }
@@ -82,17 +82,17 @@ void PreprocessProofGenerator::notifyPreprocessed(Node n,
     return;
   }
   // call the trusted version
-  notifyTrustedPreprocessed(theory::TrustNode::mkTrustRewrite(n, np, pg));
+  notifyTrustedPreprocessed(TrustNode::mkTrustRewrite(n, np, pg));
 }
 
-void PreprocessProofGenerator::notifyTrustedPreprocessed(theory::TrustNode tnp)
+void PreprocessProofGenerator::notifyTrustedPreprocessed(TrustNode tnp)
 {
   if (tnp.isNull())
   {
     // no rewrite, nothing to do
     return;
   }
-  Assert(tnp.getKind() == theory::TrustNodeKind::REWRITE);
+  Assert(tnp.getKind() == TrustNodeKind::REWRITE);
   Node np = tnp.getNode();
   Trace("smt-proof-pp-debug")
       << "PreprocessProofGenerator::notifyPreprocessed: " << tnp.getProven()
@@ -161,8 +161,8 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
       }
 
       Trace("smt-pppg") << "...update" << std::endl;
-      theory::TrustNodeKind tnk = (*it).second.getKind();
-      if (tnk == theory::TrustNodeKind::REWRITE)
+      TrustNodeKind tnk = (*it).second.getKind();
+      if (tnk == TrustNodeKind::REWRITE)
       {
         Trace("smt-pppg") << "...rewritten from " << proven[0] << std::endl;
         Assert(proven.getKind() == kind::EQUAL);
@@ -185,17 +185,15 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
       else
       {
         Trace("smt-pppg") << "...lemma" << std::endl;
-        Assert(tnk == theory::TrustNodeKind::LEMMA);
+        Assert(tnk == TrustNodeKind::LEMMA);
       }
 
       if (!proofStepProcessed)
       {
         Trace("smt-pppg") << "...add missing step" << std::endl;
         // add trusted step, the rule depends on the kind of trust node
-        cdp.addStep(proven,
-                    tnk == theory::TrustNodeKind::LEMMA ? d_ra : d_rpp,
-                    {},
-                    {proven});
+        cdp.addStep(
+            proven, tnk == TrustNodeKind::LEMMA ? d_ra : d_rpp, {}, {proven});
       }
     }
   } while (success);
diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h
index 347f4af3b..a0e88b3e9 100644
--- a/src/smt/preprocess_proof_generator.h
+++ b/src/smt/preprocess_proof_generator.h
@@ -55,7 +55,7 @@ namespace smt {
  */
 class PreprocessProofGenerator : public ProofGenerator
 {
-  typedef context::CDHashMap<Node, theory::TrustNode> NodeTrustNodeMap;
+  typedef context::CDHashMap<Node, TrustNode> NodeTrustNodeMap;
 
  public:
   /**
@@ -82,14 +82,14 @@ class PreprocessProofGenerator : public ProofGenerator
    */
   void notifyNewAssert(Node n, ProofGenerator* pg);
   /**  Notify a new assertion, trust node version. */
-  void notifyNewTrustedAssert(theory::TrustNode tn);
+  void notifyNewTrustedAssert(TrustNode tn);
   /**
    * Notify that n was replaced by np due to preprocessing, where pg can
    * provide a proof of the equality n=np.
    */
   void notifyPreprocessed(Node n, Node np, ProofGenerator* pg);
   /** Notify preprocessed, trust node version */
-  void notifyTrustedPreprocessed(theory::TrustNode tnp);
+  void notifyTrustedPreprocessed(TrustNode tnp);
   /**
    * Get proof for f, which returns a proof based on proving an equality based
    * on transitivity of preprocessing steps, and then using the original
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 7176126fb..6498fa84f 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -431,7 +431,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
       MethodId ids = MethodId::SB_DEFAULT;
       if (args.size() >= 2)
       {
-        if (builtin::BuiltinProofRuleChecker::getMethodId(args[1], ids))
+        if (getMethodId(args[1], ids))
         {
           sargs.push_back(args[1]);
         }
@@ -439,7 +439,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
       MethodId ida = MethodId::SBA_SEQUENTIAL;
       if (args.size() >= 3)
       {
-        if (builtin::BuiltinProofRuleChecker::getMethodId(args[2], ida))
+        if (getMethodId(args[2], ida))
         {
           sargs.push_back(args[2]);
         }
@@ -471,7 +471,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
     MethodId idr = MethodId::RW_REWRITE;
     if (args.size() >= 4)
     {
-      if (builtin::BuiltinProofRuleChecker::getMethodId(args[3], idr))
+      if (getMethodId(args[3], idr))
       {
         rargs.push_back(args[3]);
       }
@@ -804,12 +804,12 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
     MethodId ids = MethodId::SB_DEFAULT;
     if (args.size() >= 2)
     {
-      builtin::BuiltinProofRuleChecker::getMethodId(args[1], ids);
+      getMethodId(args[1], ids);
     }
     MethodId ida = MethodId::SBA_SEQUENTIAL;
     if (args.size() >= 3)
     {
-      builtin::BuiltinProofRuleChecker::getMethodId(args[2], ida);
+      getMethodId(args[2], ida);
     }
     std::vector<std::shared_ptr<CDProof>> pfs;
     std::vector<TNode> vsList;
@@ -950,7 +950,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
     MethodId idr = MethodId::RW_REWRITE;
     if (args.size() >= 2)
     {
-      builtin::BuiltinProofRuleChecker::getMethodId(args[1], idr);
+      getMethodId(args[1], idr);
     }
     builtin::BuiltinProofRuleChecker* builtinPfC =
         static_cast<builtin::BuiltinProofRuleChecker*>(
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 3bb998688..692b7c889 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -53,17 +53,16 @@ RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u,
 
 RemoveTermFormulas::~RemoveTermFormulas() {}
 
-theory::TrustNode RemoveTermFormulas::run(
-    TNode assertion,
-    std::vector<theory::TrustNode>& newAsserts,
-    std::vector<Node>& newSkolems,
-    bool fixedPoint)
+TrustNode RemoveTermFormulas::run(TNode assertion,
+                                  std::vector<TrustNode>& newAsserts,
+                                  std::vector<Node>& newSkolems,
+                                  bool fixedPoint)
 {
   Node itesRemoved = runInternal(assertion, newAsserts, newSkolems);
   Assert(newAsserts.size() == newSkolems.size());
   if (itesRemoved == assertion)
   {
-    return theory::TrustNode::null();
+    return TrustNode::null();
   }
   // if running to fixed point, we run each new assertion through the
   // run lemma method
@@ -72,7 +71,7 @@ theory::TrustNode RemoveTermFormulas::run(
     size_t i = 0;
     while (i < newAsserts.size())
     {
-      theory::TrustNode trn = newAsserts[i];
+      TrustNode trn = newAsserts[i];
       // do not run to fixed point on subcall, since we are processing all
       // lemmas in this loop
       newAsserts[i] = runLemma(trn, newAsserts, newSkolems, false);
@@ -81,35 +80,33 @@ theory::TrustNode RemoveTermFormulas::run(
   }
   // The rewriting of assertion can be justified by the term conversion proof
   // generator d_tpg.
-  return theory::TrustNode::mkTrustRewrite(assertion, itesRemoved, d_tpg.get());
+  return TrustNode::mkTrustRewrite(assertion, itesRemoved, d_tpg.get());
 }
 
-theory::TrustNode RemoveTermFormulas::run(TNode assertion)
+TrustNode RemoveTermFormulas::run(TNode assertion)
 {
-  std::vector<theory::TrustNode> newAsserts;
+  std::vector<TrustNode> newAsserts;
   std::vector<Node> newSkolems;
   return run(assertion, newAsserts, newSkolems, false);
 }
 
-theory::TrustNode RemoveTermFormulas::runLemma(
-    theory::TrustNode lem,
-    std::vector<theory::TrustNode>& newAsserts,
-    std::vector<Node>& newSkolems,
-    bool fixedPoint)
+TrustNode RemoveTermFormulas::runLemma(TrustNode lem,
+                                       std::vector<TrustNode>& newAsserts,
+                                       std::vector<Node>& newSkolems,
+                                       bool fixedPoint)
 {
-  theory::TrustNode trn =
-      run(lem.getProven(), newAsserts, newSkolems, fixedPoint);
+  TrustNode trn = run(lem.getProven(), newAsserts, newSkolems, fixedPoint);
   if (trn.isNull())
   {
     // no change
     return lem;
   }
-  Assert(trn.getKind() == theory::TrustNodeKind::REWRITE);
+  Assert(trn.getKind() == TrustNodeKind::REWRITE);
   Node newAssertion = trn.getNode();
   if (!isProofEnabled())
   {
     // proofs not enabled, just take result
-    return theory::TrustNode::mkTrustLemma(newAssertion, nullptr);
+    return TrustNode::mkTrustLemma(newAssertion, nullptr);
   }
   Trace("rtf-proof-debug")
       << "RemoveTermFormulas::run: setup proof for processed new lemma"
@@ -128,11 +125,11 @@ theory::TrustNode RemoveTermFormulas::runLemma(
   // ------------------------------------------------------- EQ_RESOLVE
   // newAssertion
   d_lp->addStep(newAssertion, PfRule::EQ_RESOLVE, {assertionPre, naEq}, {});
-  return theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get());
+  return TrustNode::mkTrustLemma(newAssertion, d_lp.get());
 }
 
 Node RemoveTermFormulas::runInternal(TNode assertion,
-                                     std::vector<theory::TrustNode>& output,
+                                     std::vector<TrustNode>& output,
                                      std::vector<Node>& newSkolems)
 {
   NodeManager* nm = NodeManager::currentNM();
@@ -164,7 +161,7 @@ Node RemoveTermFormulas::runInternal(TNode assertion,
     if (!processedChildren.back())
     {
       // check if we should replace the current node
-      theory::TrustNode newLem;
+      TrustNode newLem;
       Node currt = runCurrent(curr, newLem);
       // if we replaced by a skolem, we do not recurse
       if (!currt.isNull())
@@ -251,7 +248,7 @@ Node RemoveTermFormulas::runInternal(TNode assertion,
 }
 
 Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr,
-                                    theory::TrustNode& newLem)
+                                    TrustNode& newLem)
 {
   TNode node = curr.first;
   uint32_t cval = curr.second;
@@ -498,7 +495,7 @@ Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr,
       Trace("rtf-debug") << "*** term formula removal introduced " << skolem
                          << " for " << node << std::endl;
 
-      newLem = theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get());
+      newLem = TrustNode::mkTrustLemma(newAssertion, d_lp.get());
 
       Trace("rtf-proof-debug") << "Checking closed..." << std::endl;
       newLem.debugCheckClosed("rtf-proof-debug",
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index c2b1f27f3..6f27b9462 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -88,24 +88,24 @@ class RemoveTermFormulas {
    * right hand side is assertion after removing term formulas, and the proof
    * generator (if provided) that can prove the equivalence.
    */
-  theory::TrustNode run(TNode assertion,
-                        std::vector<theory::TrustNode>& newAsserts,
-                        std::vector<Node>& newSkolems,
-                        bool fixedPoint = false);
+  TrustNode run(TNode assertion,
+                std::vector<TrustNode>& newAsserts,
+                std::vector<Node>& newSkolems,
+                bool fixedPoint = false);
   /**
    * Same as above, but does not track lemmas, and does not run to fixed point.
    * The relevant lemmas can be extracted by the caller later using getSkolems
    * and getLemmaForSkolem.
    */
-  theory::TrustNode run(TNode assertion);
+  TrustNode run(TNode assertion);
   /**
    * Same as above, but transforms a lemma, returning a LEMMA trust node that
    * proves the same formula as lem with term formulas removed.
    */
-  theory::TrustNode runLemma(theory::TrustNode lem,
-                             std::vector<theory::TrustNode>& newAsserts,
-                             std::vector<Node>& newSkolems,
-                             bool fixedPoint = false);
+  TrustNode runLemma(TrustNode lem,
+                     std::vector<TrustNode>& newAsserts,
+                     std::vector<Node>& newSkolems,
+                     bool fixedPoint = false);
 
   /**
    * Get proof generator that is responsible for all proofs for removing term
@@ -190,7 +190,7 @@ class RemoveTermFormulas {
    * the version of assertion with all term formulas removed.
    */
   Node runInternal(TNode assertion,
-                   std::vector<theory::TrustNode>& newAsserts,
+                   std::vector<TrustNode>& newAsserts,
                    std::vector<Node>& newSkolems);
   /**
    * This is called on curr of the form (t, val) where t is a term and val is
@@ -202,7 +202,7 @@ class RemoveTermFormulas {
    * Otherwise, if t should not be replaced in the term context, this method
    * returns the null node.
    */
-  Node runCurrent(std::pair<Node, uint32_t>& curr, theory::TrustNode& newLem);
+  Node runCurrent(std::pair<Node, uint32_t>& curr, TrustNode& newLem);
 
   /** Whether proofs are enabled */
   bool isProofEnabled() const;
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 8ada48cfe..4ab0b313b 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -36,6 +36,7 @@
 namespace cvc5 {
 
 class ProofNodeManager;
+class EagerProofGenerator;
 
 namespace context {
 class Context;
@@ -43,8 +44,6 @@ class UserContext;
 }
 
 namespace theory {
-
-class EagerProofGenerator;
 struct EeSetupInfo;
 
 namespace eq {
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index fce071e6e..f6306049b 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -97,14 +97,13 @@
 namespace cvc5 {
 
 class ProofNodeManager;
+class EagerProofGenerator;
 
 namespace context {
 class Context;
 }
 namespace theory {
 
-class EagerProofGenerator;
-
 namespace arith {
 
 class Comparison;
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index e3094ae88..b25fa4f69 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -56,9 +56,11 @@
 #include "util/statistics_stats.h"
 
 namespace cvc5 {
-namespace theory {
 
 class EagerProofGenerator;
+
+namespace theory {
+
 class TheoryModel;
 
 namespace arith {
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index 74e1a7cd8..d01ec081e 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -34,11 +34,9 @@ namespace cvc5 {
 
 class ProofGenerator;
 class ProofNode;
-
-namespace theory {
-
 class EagerProofGenerator;
 
+namespace theory {
 namespace booleans {
 
 /**
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index 9dfc9418f..7ec0525c9 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -26,39 +26,6 @@ using namespace cvc5::kind;
 
 namespace cvc5 {
 namespace theory {
-
-const char* toString(MethodId id)
-{
-  switch (id)
-  {
-    case MethodId::RW_REWRITE: return "RW_REWRITE";
-    case MethodId::RW_EXT_REWRITE: return "RW_EXT_REWRITE";
-    case MethodId::RW_REWRITE_EQ_EXT: return "RW_REWRITE_EQ_EXT";
-    case MethodId::RW_EVALUATE: return "RW_EVALUATE";
-    case MethodId::RW_IDENTITY: return "RW_IDENTITY";
-    case MethodId::RW_REWRITE_THEORY_PRE: return "RW_REWRITE_THEORY_PRE";
-    case MethodId::RW_REWRITE_THEORY_POST: return "RW_REWRITE_THEORY_POST";
-    case MethodId::SB_DEFAULT: return "SB_DEFAULT";
-    case MethodId::SB_LITERAL: return "SB_LITERAL";
-    case MethodId::SB_FORMULA: return "SB_FORMULA";
-    case MethodId::SBA_SEQUENTIAL: return "SBA_SEQUENTIAL";
-    case MethodId::SBA_SIMUL: return "SBA_SIMUL";
-    case MethodId::SBA_FIXPOINT: return "SBA_FIXPOINT";
-    default: return "MethodId::Unknown";
-  };
-}
-
-std::ostream& operator<<(std::ostream& out, MethodId id)
-{
-  out << toString(id);
-  return out;
-}
-
-Node mkMethodId(MethodId id)
-{
-  return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(id)));
-}
-
 namespace builtin {
 
 void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
@@ -250,17 +217,6 @@ Node BuiltinProofRuleChecker::applySubstitution(Node n,
   return ns;
 }
 
-bool BuiltinProofRuleChecker::getMethodId(TNode n, MethodId& i)
-{
-  uint32_t index;
-  if (!getUInt32(n, index))
-  {
-    return false;
-  }
-  i = static_cast<MethodId>(index);
-  return true;
-}
-
 Node BuiltinProofRuleChecker::checkInternal(PfRule id,
                                             const std::vector<Node>& children,
                                             const std::vector<Node>& args)
@@ -455,58 +411,6 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
   return Node::null();
 }
 
-bool BuiltinProofRuleChecker::getMethodIds(const std::vector<Node>& args,
-                                           MethodId& ids,
-                                           MethodId& ida,
-                                           MethodId& idr,
-                                           size_t index)
-{
-  ids = MethodId::SB_DEFAULT;
-  ida = MethodId::SBA_SEQUENTIAL;
-  idr = MethodId::RW_REWRITE;
-  for (size_t offset = 0; offset <= 2; offset++)
-  {
-    if (args.size() > index + offset)
-    {
-      MethodId& id = offset == 0 ? ids : (offset == 1 ? ida : idr);
-      if (!getMethodId(args[index + offset], id))
-      {
-        Trace("builtin-pfcheck")
-            << "Failed to get id from " << args[index + offset] << std::endl;
-        return false;
-      }
-    }
-    else
-    {
-      break;
-    }
-  }
-  Trace("builtin-pfcheck") << "Got MethodIds ids/ida/idr: " << ids << " / "
-                           << ida << " / " << idr << "\n";
-  return true;
-}
-
-void BuiltinProofRuleChecker::addMethodIds(std::vector<Node>& args,
-                                           MethodId ids,
-                                           MethodId ida,
-                                           MethodId idr)
-{
-  bool ndefRewriter = (idr != MethodId::RW_REWRITE);
-  bool ndefApply = (ida != MethodId::SBA_SEQUENTIAL);
-  if (ids != MethodId::SB_DEFAULT || ndefRewriter || ndefApply)
-  {
-    args.push_back(mkMethodId(ids));
-  }
-  if (ndefApply || ndefRewriter)
-  {
-    args.push_back(mkMethodId(ida));
-  }
-  if (ndefRewriter)
-  {
-    args.push_back(mkMethodId(idr));
-  }
-}
-
 bool BuiltinProofRuleChecker::getTheoryId(TNode n, TheoryId& tid)
 {
   uint32_t i;
diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h
index 892fc7a4b..1e671a7b3 100644
--- a/src/theory/builtin/proof_checker.h
+++ b/src/theory/builtin/proof_checker.h
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * Equality proof checker utility.
+ * Builtin proof checker utility.
  */
 
 #include "cvc5_private.h"
@@ -19,74 +19,13 @@
 #define CVC5__THEORY__BUILTIN__PROOF_CHECKER_H
 
 #include "expr/node.h"
+#include "proof/method_id.h"
 #include "proof/proof_checker.h"
 #include "proof/proof_node.h"
 #include "theory/quantifiers/extended_rewrite.h"
 
 namespace cvc5 {
 namespace theory {
-
-/**
- * Identifiers for rewriters and substitutions, which we abstractly
- * classify as "methods".  Methods have a unique identifier in the internal
- * proof calculus implemented by the checker below.
- *
- * A "rewriter" is abstractly a method from Node to Node, where the output
- * is semantically equivalent to the input. The identifiers below list
- * various methods that have this contract. This identifier is used
- * in a number of the builtin rules.
- *
- * A substitution is a method for turning a formula into a substitution.
- */
-enum class MethodId : uint32_t
-{
-  //---------------------------- Rewriters
-  // Rewriter::rewrite(n)
-  RW_REWRITE,
-  // d_ext_rew.extendedRewrite(n);
-  RW_EXT_REWRITE,
-  // Rewriter::rewriteExtEquality(n)
-  RW_REWRITE_EQ_EXT,
-  // Evaluator::evaluate(n)
-  RW_EVALUATE,
-  // identity
-  RW_IDENTITY,
-  // theory preRewrite, note this is only intended to be used as an argument
-  // to THEORY_REWRITE in the final proof. It is not implemented in
-  // applyRewrite below, see documentation in proof_rule.h for THEORY_REWRITE.
-  RW_REWRITE_THEORY_PRE,
-  // same as above, for theory postRewrite
-  RW_REWRITE_THEORY_POST,
-  //---------------------------- Substitutions
-  // (= x y) is interpreted as x -> y, using Node::substitute
-  SB_DEFAULT,
-  // P, (not P) are interpreted as P -> true, P -> false using Node::substitute
-  SB_LITERAL,
-  // P is interpreted as P -> true using Node::substitute
-  SB_FORMULA,
-  //---------------------------- Substitution applications
-  // multiple substitutions are applied sequentially
-  SBA_SEQUENTIAL,
-  // multiple substitutions are applied simultaneously
-  SBA_SIMUL,
-  // multiple substitutions are applied to fix point
-  SBA_FIXPOINT
-  // For example, for x -> u, y -> f(z), z -> g(x), applying this substituion to
-  // y gives:
-  // - f(g(x)) for SBA_SEQUENTIAL
-  // - f(z) for SBA_SIMUL
-  // - f(g(u)) for SBA_FIXPOINT
-  // Notice that SBA_FIXPOINT should provide a terminating rewrite system
-  // as a substitution, or else non-termination will occur during proof
-  // checking.
-};
-/** Converts a rewriter id to a string. */
-const char* toString(MethodId id);
-/** Write a rewriter id to out */
-std::ostream& operator<<(std::ostream& out, MethodId id);
-/** Make a method id node */
-Node mkMethodId(MethodId id);
-
 namespace builtin {
 
 /** A checker for builtin proofs */
@@ -166,26 +105,6 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
                                 MethodId ids = MethodId::SB_DEFAULT,
                                 MethodId ida = MethodId::SBA_SEQUENTIAL,
                                 MethodId idr = MethodId::RW_REWRITE);
-  /** get a method identifier from a node, return false if we fail */
-  static bool getMethodId(TNode n, MethodId& i);
-  /**
-   * Get method identifiers from args starting at the given index. Store their
-   * values into ids, ida, and idr. This method returns false if args does not
-   * contain valid method identifiers at position index in args.
-   */
-  bool getMethodIds(const std::vector<Node>& args,
-                    MethodId& ids,
-                    MethodId& ida,
-                    MethodId& idr,
-                    size_t index);
-  /**
-   * Add method identifiers ids, ida and idr as nodes to args. This does not add
-   * ids, ida or idr if their values are the default ones.
-   */
-  static void addMethodIds(std::vector<Node>& args,
-                           MethodId ids,
-                           MethodId ida,
-                           MethodId idr);
 
   /** get a TheoryId from a node, return false if we fail */
   static bool getTheoryId(TNode n, TheoryId& tid);
diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h
index 063cefd49..6417b501e 100644
--- a/src/theory/combination_engine.h
+++ b/src/theory/combination_engine.h
@@ -28,10 +28,10 @@ namespace cvc5 {
 
 class TheoryEngine;
 class Env;
+class EagerProofGenerator;
 
 namespace theory {
 
-class EagerProofGenerator;
 class ModelManager;
 class SharedSolver;
 
diff --git a/src/theory/datatypes/inference_manager.h b/src/theory/datatypes/inference_manager.h
index 2642ae0c5..019efa950 100644
--- a/src/theory/datatypes/inference_manager.h
+++ b/src/theory/datatypes/inference_manager.h
@@ -23,10 +23,10 @@
 #include "theory/inference_manager_buffered.h"
 
 namespace cvc5 {
-namespace theory {
 
 class EagerProofGenerator;
 
+namespace theory {
 namespace datatypes {
 
 /**
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index 1fc685992..3201bb2c8 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -24,11 +24,10 @@ namespace cvc5 {
 
 class TConvProofGenerator;
 class ProofNodeManager;
+class TrustNode;
 
 namespace theory {
 
-class TrustNode;
-
 namespace builtin {
 class BuiltinProofRuleChecker;
 }
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index b9c331acc..0e17f50a9 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -300,7 +300,7 @@ bool SharedTermsDatabase::isKnown(TNode literal) const {
   }
 }
 
-theory::TrustNode SharedTermsDatabase::explain(TNode literal) const
+TrustNode SharedTermsDatabase::explain(TNode literal) const
 {
   if (d_pfee != nullptr)
   {
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index b684ff56f..4e09ac23f 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -186,7 +186,7 @@ class SharedTermsDatabase : public context::ContextNotifyObj {
   /**
    * Returns an explanation of the propagation that came from the database.
    */
-  theory::TrustNode explain(TNode literal) const;
+  TrustNode explain(TNode literal) const;
 
   /**
    * Add an equality to propagate.
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; }
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index ffcaf392f..f293a2cc8 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -191,7 +191,7 @@ class TheoryEngine {
    * generator (if it exists),
    * @param theoryId The theory that sent the conflict
    */
-  void conflict(theory::TrustNode conflict, theory::TheoryId theoryId);
+  void conflict(TrustNode conflict, theory::TheoryId theoryId);
 
   /**
    * Debugging flag to ensure that shutdown() is called before the
@@ -272,7 +272,7 @@ class TheoryEngine {
    * @param atomsTo the theory that atoms of the lemma should be sent to
    * @param from the theory that sent the lemma
    */
-  void lemma(theory::TrustNode node,
+  void lemma(TrustNode node,
              theory::LemmaProperty p,
              theory::TheoryId atomsTo = theory::THEORY_LAST,
              theory::TheoryId from = theory::THEORY_LAST);
@@ -422,8 +422,7 @@ class TheoryEngine {
    * where the node is the one to be explained, and the theory is the
    * theory that sent the literal.
    */
-  theory::TrustNode getExplanation(
-      std::vector<NodeTheoryPair>& explanationVector);
+  TrustNode getExplanation(std::vector<NodeTheoryPair>& explanationVector);
 
   /** Are proofs enabled? */
   bool isProofEnabled() const;
@@ -433,7 +432,7 @@ class TheoryEngine {
    * Preprocess rewrite equality, called by the preprocessor to rewrite
    * equalities appearing in the input.
    */
-  theory::TrustNode ppRewriteEquality(TNode eq);
+  TrustNode ppRewriteEquality(TNode eq);
   /** Notify (preprocessed) assertions. */
   void notifyPreprocessedAssertions(const std::vector<Node>& assertions);
 
@@ -477,8 +476,7 @@ class TheoryEngine {
    * take this proof into account (when proofs are enabled).
    */
   theory::Theory::PPAssertStatus solve(
-      theory::TrustNode tliteral,
-      theory::TrustSubstitutionMap& substitutionOut);
+      TrustNode tliteral, theory::TrustSubstitutionMap& substitutionOut);
 
   /**
    * Preregister a Theory atom with the responsible theory (or
@@ -540,7 +538,7 @@ class TheoryEngine {
   /**
    * Returns an explanation of the node propagated to the SAT solver.
    */
-  theory::TrustNode getExplanation(TNode node);
+  TrustNode getExplanation(TNode node);
 
   /**
    * Get the pointer to the model object used by this theory engine.
diff --git a/src/theory/theory_engine_proof_generator.cpp b/src/theory/theory_engine_proof_generator.cpp
index f10716bd9..073accdae 100644
--- a/src/theory/theory_engine_proof_generator.cpp
+++ b/src/theory/theory_engine_proof_generator.cpp
@@ -30,21 +30,21 @@ TheoryEngineProofGenerator::TheoryEngineProofGenerator(ProofNodeManager* pnm,
   d_false = NodeManager::currentNM()->mkConst(false);
 }
 
-theory::TrustNode TheoryEngineProofGenerator::mkTrustExplain(
+TrustNode TheoryEngineProofGenerator::mkTrustExplain(
     TNode lit, Node exp, std::shared_ptr<LazyCDProof> lpf)
 {
   Node p;
-  theory::TrustNode trn;
+  TrustNode trn;
   if (lit == d_false)
   {
     // propagation of false is a conflict
-    trn = theory::TrustNode::mkTrustConflict(exp, this);
+    trn = TrustNode::mkTrustConflict(exp, this);
     p = trn.getProven();
     Assert(p.getKind() == NOT);
   }
   else
   {
-    trn = theory::TrustNode::mkTrustPropExp(lit, exp, this);
+    trn = TrustNode::mkTrustPropExp(lit, exp, this);
     p = trn.getProven();
     Assert(p.getKind() == IMPLIES && p.getNumChildren() == 2);
   }
diff --git a/src/theory/theory_engine_proof_generator.h b/src/theory/theory_engine_proof_generator.h
index ab0f616fe..68f7dea32 100644
--- a/src/theory/theory_engine_proof_generator.h
+++ b/src/theory/theory_engine_proof_generator.h
@@ -53,9 +53,9 @@ class TheoryEngineProofGenerator : public ProofGenerator
    * explanation already exists, then the previous explanation is taken, which
    * also suffices for proving the implication.
    */
-  theory::TrustNode mkTrustExplain(TNode lit,
-                                   Node exp,
-                                   std::shared_ptr<LazyCDProof> lpf);
+  TrustNode mkTrustExplain(TNode lit,
+                           Node exp,
+                           std::shared_ptr<LazyCDProof> lpf);
   /**
    * Get proof for, which expects implications corresponding to explained
    * propagations (=> exp lit) registered by the above method. This currently
diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h
index a81deabc2..672693366 100644
--- a/test/unit/test_smt.h
+++ b/test/unit/test_smt.h
@@ -115,10 +115,7 @@ class DummyOutputChannel : public cvc5::theory::OutputChannel
   void safePoint(Resource r) override {}
   void conflict(TNode n) override { push(CONFLICT, n); }
 
-  void trustedConflict(theory::TrustNode n) override
-  {
-    push(CONFLICT, n.getNode());
-  }
+  void trustedConflict(TrustNode n) override { push(CONFLICT, n.getNode()); }
 
   bool propagate(TNode n) override
   {
@@ -132,7 +129,7 @@ class DummyOutputChannel : public cvc5::theory::OutputChannel
     push(LEMMA, n);
   }
 
-  void trustedLemma(theory::TrustNode n, theory::LemmaProperty p) override
+  void trustedLemma(TrustNode n, theory::LemmaProperty p) override
   {
     push(LEMMA, n.getNode());
   }
@@ -250,10 +247,7 @@ class DummyTheory : public theory::Theory
     // do not assert to equality engine, since this theory does not use one
     return true;
   }
-  theory::TrustNode explain(TNode n) override
-  {
-    return theory::TrustNode::null();
-  }
+  TrustNode explain(TNode n) override { return TrustNode::null(); }
   Node getValue(TNode n) { return Node::null(); }
   std::string identify() const override { return "DummyTheory" + d_id; }