From d676cc2b2d279041d26804c47494a2206bb74874 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 1 Dec 2021 16:41:11 -0300
Subject: [PATCH] [proofs] Add method to CDProof to obtain number of proof
 nodes (#7725)

Useful for example to easily see by how much a proof grew after some reconstruction expansion.
---
 src/proof/proof.cpp | 2 ++
 src/proof/proof.h   | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/src/proof/proof.cpp b/src/proof/proof.cpp
index ffccd42ba..d6724d51d 100644
--- a/src/proof/proof.cpp
+++ b/src/proof/proof.cpp
@@ -408,6 +408,8 @@ bool CDProof::hasStep(Node fact)
   return false;
 }
 
+size_t CDProof::getNumProofNodes() const { return d_nodes.size(); }
+
 ProofNodeManager* CDProof::getManager() const { return d_manager; }
 
 bool CDProof::shouldOverwrite(ProofNode* pn, PfRule newId, CDPOverwrite opol)
diff --git a/src/proof/proof.h b/src/proof/proof.h
index 7d8fa4155..109f60713 100644
--- a/src/proof/proof.h
+++ b/src/proof/proof.h
@@ -227,6 +227,8 @@ class CDProof : public ProofGenerator
                 bool doCopy = false);
   /** Return true if fact already has a proof step */
   bool hasStep(Node fact);
+  /** Return how many proof nodes currently in proof */
+  size_t getNumProofNodes() const;
   /** Get the proof manager for this proof */
   ProofNodeManager* getManager() const;
   /**
-- 
2.30.2