Adding garbage collection for Proof objects. (#1294)

6 files changed, 20 insertions, 11 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index b43ba5591..af417f740 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -2245,15 +2245,17 @@ void TheoryArrays::conflict(TNode a, TNode b) {
   d_conflictNode = explain(a.eqNode(b), proof.get());
 
   if (!d_inCheckModel) {
-    ProofArray* proof_array = NULL;
+    std::unique_ptr<ProofArray> proof_array;
 
     if (d_proofsEnabled) {
       proof->debug_print("pf::array");
-      proof_array = new ProofArray(proof, /*row=*/d_reasonRow,
-                                   /*row1=*/d_reasonRow1, /*ext=*/d_reasonExt);
+      proof_array.reset(new ProofArray(proof,
+                                       /*row=*/d_reasonRow,
+                                       /*row1=*/d_reasonRow1,
+                                       /*ext=*/d_reasonExt));
     }
 
-    d_out->conflict(d_conflictNode, proof_array);
+    d_out->conflict(d_conflictNode, std::move(proof_array));
   }
 
   d_conflict = true;
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 2c11097db..cc8cee481 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -19,6 +19,8 @@
 #ifndef __CVC4__THEORY__OUTPUT_CHANNEL_H
 #define __CVC4__THEORY__OUTPUT_CHANNEL_H
 
+#include <memory>
+
 #include "base/cvc4_assert.h"
 #include "proof/proof_manager.h"
 #include "smt/logic_exception.h"
@@ -97,7 +99,7 @@ class OutputChannel {
    * @param pf - a proof of the conflict. This is only non-null if proofs
    * are enabled.
    */
-  virtual void conflict(TNode n, Proof* pf = nullptr) = 0;
+  virtual void conflict(TNode n, std::unique_ptr<Proof> pf = nullptr) = 0;
 
   /**
    * Propagate a theory literal.
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 6c49f2914..d01bd537e 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -202,7 +202,8 @@ bool TheoryEngine::EngineOutputChannel::propagate(TNode literal) {
 }
 
 void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode,
-                                                 Proof* proof) {
+                                                 std::unique_ptr<Proof> proof)
+{
   Trace("theory::conflict")
       << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode
       << ")" << std::endl;
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 9afd4e5d9..91a88274e 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -20,6 +20,7 @@
 #define __CVC4__THEORY_ENGINE_H
 
 #include <deque>
+#include <memory>
 #include <set>
 #include <unordered_map>
 #include <vector>
@@ -265,7 +266,8 @@ class TheoryEngine {
       }
     }
 
-    void conflict(TNode conflictNode, Proof* pf = nullptr) override;
+    void conflict(TNode conflictNode,
+                  std::unique_ptr<Proof> pf = nullptr) override;
     bool propagate(TNode literal) override;
 
     theory::LemmaStatus lemma(TNode lemma, ProofRule rule,
diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index 4e0fd3e4d..8c2355cf4 100644
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -20,6 +20,7 @@
 #define __CVC4__THEORY__THEORY_TEST_UTILS_H
 
 #include <iostream>
+#include <memory>
 #include <utility>
 #include <vector>
 
@@ -27,6 +28,7 @@
 #include "expr/node.h"
 #include "theory/interrupted.h"
 #include "theory/output_channel.h"
+#include "util/proof.h"
 #include "util/unsafe_interrupt_exception.h"
 
 namespace CVC4 {
@@ -67,8 +69,8 @@ public:
   ~TestOutputChannel() override {}
 
   void safePoint(uint64_t amount) override {}
-
-  void conflict(TNode n, Proof* pf = nullptr) override {
+  void conflict(TNode n, std::unique_ptr<Proof> pf) override
+  {
     push(CONFLICT, n);
   }
 
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 170621603..f97a4b639 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -634,8 +634,8 @@ void TheoryUF::conflict(TNode a, TNode b) {
   std::shared_ptr<eq::EqProof> pf =
       d_proofsEnabled ? std::make_shared<eq::EqProof>() : nullptr;
   d_conflictNode = explain(a.eqNode(b), pf.get());
-  ProofUF* puf = d_proofsEnabled ? new ProofUF( pf ) : NULL;
-  d_out->conflict(d_conflictNode, puf);
+  std::unique_ptr<ProofUF> puf(d_proofsEnabled ? new ProofUF(pf) : nullptr);
+  d_out->conflict(d_conflictNode, std::move(puf));
   d_conflict = true;
 }