1 files changed, 11 insertions, 0 deletions
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index f96062b61..d90af4a31 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -159,6 +159,11 @@ class Rewriter {
 
   void clearCachesInternal();
 
+  /**
+   * Has n been rewritten with proofs? This checks if n is in d_tpgNodes.
+   */
+  bool hasRewrittenWithProofs(TNode n) const;
+
   /** The resource manager, for tracking resource usage */
   ResourceManager* d_resourceManager;
 
@@ -167,6 +172,12 @@ class Rewriter {
 
   /** The proof generator */
   std::unique_ptr<TConvProofGenerator> d_tpg;
+  /**
+   * Nodes rewritten with proofs. Since d_tpg contains a reference to all
+   * nodes that have been rewritten with proofs, we can keep only a TNode
+   * here.
+   */
+  std::unordered_set<TNode> d_tpgNodes;
 #ifdef CVC5_ASSERTIONS
   std::unique_ptr<std::unordered_set<Node>> d_rewriteStack = nullptr;
 #endif /* CVC5_ASSERTIONS */