Switching EqProof to use shared_ptr everywhere. (#1217)

This clarifies the memory ownership of EqProofs.

1 files changed, 19 insertions, 12 deletions

diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h
index b817ceb69..3dc7d9b58 100644
--- a/src/proof/uf_proof.h
+++ b/src/proof/uf_proof.h
@@ -19,28 +19,35 @@
 #ifndef __CVC4__UF__PROOF_H
 #define __CVC4__UF__PROOF_H
 
+#include <memory>
 #include <unordered_set>
 
 #include "expr/expr.h"
-#include "proof/proof_manager.h"
+#include "proof/theory_proof.h"
 #include "theory/uf/equality_engine.h"
+#include "util/proof.h"
 
 namespace CVC4 {
 
-//proof object outputted by TheoryUF
+// proof object outputted by TheoryUF
 class ProofUF : public Proof {
-private:
-  static Node toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map);
-public:
-  ProofUF( theory::eq::EqProof * pf ) : d_proof( pf ) {}
-  //it is simply an equality engine proof
-  theory::eq::EqProof * d_proof;
-  void toStream(std::ostream& out);
-  void toStream(std::ostream& out, const ProofLetMap& map);
-  static void toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map);
+ public:
+  ProofUF(std::shared_ptr<theory::eq::EqProof> pf) : d_proof(pf) {}
+  void toStream(std::ostream& out) override;
+  void toStream(std::ostream& out, const ProofLetMap& map) override;
+
+ private:
+  static void toStreamLFSC(std::ostream& out, TheoryProof* tp,
+                           const theory::eq::EqProof& pf,
+                           const ProofLetMap& map);
+  static Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp,
+                              const theory::eq::EqProof& pf, unsigned tb,
+                              const ProofLetMap& map);
+
+  // it is simply an equality engine proof
+  std::shared_ptr<theory::eq::EqProof> d_proof;
 };
 
-
 namespace theory {
 namespace uf {
 class TheoryUF;