[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.

diff --git a/src/proof/proof.cpp b/src/proof/proof.cpp
index ffccd42ba4d37b2080a31a06ec07aa70f9329f18..d6724d51d7c7a3aa8ff0c6b034ac2c93ea19e2a0 100644 (file)
--- 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 7d8fa4155086eb7cf2f9dfe71c450b2c165c601b..109f60713fdbacadeb6cecef187e130b7bdd8868 100644 (file)
--- 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;
   /**