diff options
author | Tim King <taking@cs.nyu.edu> | 2017-11-15 02:58:30 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2017-11-15 02:58:30 -0800 |
commit | 3c130b44fdecc62b1ace2a739e77f913cd606aa0 (patch) | |
tree | 6abfb806dd45c83606c04dda5c26e9c410ac2ee1 /src/theory | |
parent | 85df7998e4362e0a9c796146d07d7b9e91045a31 (diff) |
Adding garbage collection for Proof objects. (#1294)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 10 | ||||
-rw-r--r-- | src/theory/output_channel.h | 4 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 3 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 4 | ||||
-rw-r--r-- | src/theory/theory_test_utils.h | 6 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 4 |
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; } |