From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 1 Dec 2021 19:41:11 +0000 (-0300)
Subject: [proofs] Add method to CDProof to obtain number of proof nodes (#7725)
X-Git-Tag: cvc5-1.0.0~740
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d676cc2b2d279041d26804c47494a2206bb74874;p=cvc5.git

[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 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;
   /**