From 3c130b44fdecc62b1ace2a739e77f913cd606aa0 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Wed, 15 Nov 2017 02:58:30 -0800
Subject: Adding garbage collection for Proof objects. (#1294)

---
 test/unit/theory/theory_engine_white.h | 7 ++++++-
 test/unit/theory/theory_white.h        | 8 ++++----
 2 files changed, 10 insertions(+), 5 deletions(-)

(limited to 'test/unit')

diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 9e99ce884..d480bbb75 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -22,6 +22,7 @@
 
 #include <deque>
 #include <iostream>
+#include <memory>
 #include <string>
 
 #include "base/cvc4_assert.h"
@@ -39,6 +40,7 @@
 #include "theory/theory_engine.h"
 #include "theory/valuation.h"
 #include "util/integer.h"
+#include "util/proof.h"
 #include "util/rational.h"
 
 using namespace CVC4;
@@ -52,7 +54,10 @@ using namespace CVC4::theory::bv;
 using namespace std;
 
 class FakeOutputChannel : public OutputChannel {
-  void conflict(TNode n, Proof* pf) override { Unimplemented(); }
+  void conflict(TNode n, std::unique_ptr<Proof> pf) override
+  {
+    Unimplemented();
+  }
   bool propagate(TNode n) override { Unimplemented(); }
   LemmaStatus lemma(TNode n, ProofRule rule, bool removable, bool preprocess,
                     bool sendAtoms) override {
diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index d1517d7c2..e66960654 100644
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -15,9 +15,9 @@
  **/
 
 #include <cxxtest/TestSuite.h>
+#include <memory>
 #include <vector>
 
-// taking: Add include for Proof*.
 #include "context/context.h"
 #include "expr/node.h"
 #include "expr/node_manager.h"
@@ -25,7 +25,7 @@
 #include "smt/smt_engine_scope.h"
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
-
+#include "util/proof.h"
 
 using namespace CVC4;
 using namespace CVC4::theory;
@@ -46,8 +46,8 @@ class TestOutputChannel : public OutputChannel {
   ~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);
   }
 
-- 
cgit v1.2.3