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/proof/proof_output_channel.h | |
parent | 85df7998e4362e0a9c796146d07d7b9e91045a31 (diff) |
Adding garbage collection for Proof objects. (#1294)
Diffstat (limited to 'src/proof/proof_output_channel.h')
-rw-r--r-- | src/proof/proof_output_channel.h | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/proof/proof_output_channel.h b/src/proof/proof_output_channel.h index 9516eb71b..e2958e8a5 100644 --- a/src/proof/proof_output_channel.h +++ b/src/proof/proof_output_channel.h @@ -16,13 +16,14 @@ #ifndef __CVC4__PROOF_OUTPUT_CHANNEL_H #define __CVC4__PROOF_OUTPUT_CHANNEL_H +#include <memory> #include <set> #include <unordered_set> #include "expr/node.h" -#include "util/proof.h" #include "theory/output_channel.h" #include "theory/theory.h" +#include "util/proof.h" namespace CVC4 { @@ -35,7 +36,7 @@ class ProofOutputChannel : public theory::OutputChannel { * This may be called at most once per ProofOutputChannel. * Requires that `n` and `pf` are non-null. */ - void conflict(TNode n, Proof* pf) override; + void conflict(TNode n, std::unique_ptr<Proof> pf) override; bool propagate(TNode x) override; theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool) override; theory::LemmaStatus splitLemma(TNode, bool) override; @@ -50,12 +51,12 @@ class ProofOutputChannel : public theory::OutputChannel { * Returns the proof passed into the conflict() call. * Requires hasConflict() to hold. */ - Proof* getConflictProof(); + const Proof& getConflictProof() const; Node getLastLemma() const { return d_lemma; } private: Node d_conflict; - Proof* d_proof; + std::unique_ptr<Proof> d_proof; Node d_lemma; std::set<Node> d_propagations; }; /* class ProofOutputChannel */ |