Switching EqProof to use shared_ptr everywhere. (#1217)

This clarifies the memory ownership of EqProofs.

1 files changed, 9 insertions, 7 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index a17f506de..b43ba5591 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -17,6 +17,7 @@
 #include "theory/arrays/theory_arrays.h"
 
 #include <map>
+#include <memory>
 
 #include "expr/kind.h"
 #include "options/arrays_options.h"
@@ -395,7 +396,8 @@ bool TheoryArrays::propagate(TNode literal)
 }/* TheoryArrays::propagate(TNode) */
 
 
-void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof *proof) {
+void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions,
+                           eq::EqProof* proof) {
   // Do the work
   bool polarity = literal.getKind() != kind::NOT;
   TNode atom = polarity ? literal : literal[0];
@@ -831,16 +833,15 @@ Node TheoryArrays::explain(TNode literal) {
   return explanation;
 }
 
-Node TheoryArrays::explain(TNode literal, eq::EqProof *proof)
-{
+Node TheoryArrays::explain(TNode literal, eq::EqProof* proof) {
   ++d_numExplain;
-  Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::explain(" << literal << ")" << std::endl;
+  Debug("arrays") << spaces(getSatContext()->getLevel())
+                  << "TheoryArrays::explain(" << literal << ")" << std::endl;
   std::vector<TNode> assumptions;
   explain(literal, assumptions, proof);
   return mkAnd(assumptions);
 }
 
-
 /////////////////////////////////////////////////////////////////////////////
 // SHARING
 /////////////////////////////////////////////////////////////////////////////
@@ -2238,9 +2239,10 @@ bool TheoryArrays::dischargeLemmas()
 
 void TheoryArrays::conflict(TNode a, TNode b) {
   Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl;
-  eq::EqProof* proof = d_proofsEnabled ? new eq::EqProof() : NULL;
+  std::shared_ptr<eq::EqProof> proof = d_proofsEnabled ?
+      std::make_shared<eq::EqProof>() : nullptr;
 
-  d_conflictNode = explain(a.eqNode(b), proof);
+  d_conflictNode = explain(a.eqNode(b), proof.get());
 
   if (!d_inCheckModel) {
     ProofArray* proof_array = NULL;