Switching EqProof to use shared_ptr everywhere. (#1217)

This clarifies the memory ownership of EqProofs.

1 files changed, 13 insertions, 9 deletions

diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h
index 3de53f866..b36909f78 100644
--- a/src/proof/arith_proof.h
+++ b/src/proof/arith_proof.h
@@ -19,6 +19,7 @@
 #ifndef __CVC4__ARITH__PROOF_H
 #define __CVC4__ARITH__PROOF_H
 
+#include <memory>
 #include <unordered_set>
 
 #include "expr/expr.h"
@@ -30,17 +31,20 @@ namespace CVC4 {
 
 //proof object outputted by TheoryArith
 class ProofArith : public Proof {
-private:
-  static Node toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map);
-public:
-  ProofArith( theory::eq::EqProof * pf ) : d_proof( pf ) {}
-  //it is simply an equality engine proof
-  theory::eq::EqProof * d_proof;
-  void toStream(std::ostream& out);
-  static void toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map);
+ public:
+  ProofArith(std::shared_ptr<theory::eq::EqProof> pf) : d_proof(pf) {}
+  void toStream(std::ostream& out) 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 arith {
 class TheoryArith;