diff options
author | Tim King <taking@cs.nyu.edu> | 2017-10-25 14:28:07 -0700 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2017-10-25 14:28:07 -0700 |
commit | 0e3f99d90a5fcafd04b04adf0d3e7e71ccfa65b0 (patch) | |
tree | d0a60841c95046ab9b19923d393f663805e962da /src/proof/arith_proof.h | |
parent | c49ef48588c708bfef3c7a0f9db8219415301a94 (diff) |
Switching EqProof to use shared_ptr everywhere. (#1217)
This clarifies the memory ownership of EqProofs.
Diffstat (limited to 'src/proof/arith_proof.h')
-rw-r--r-- | src/proof/arith_proof.h | 22 |
1 files changed, 13 insertions, 9 deletions
diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h index 3de53f866..b36909f78 100644 --- a/src/proof/arith_proof.h +++ b/src/proof/arith_proof.h @@ -19,6 +19,7 @@ #ifndef __CVC4__ARITH__PROOF_H #define __CVC4__ARITH__PROOF_H +#include <memory> #include <unordered_set> #include "expr/expr.h" @@ -30,17 +31,20 @@ namespace CVC4 { //proof object outputted by TheoryArith class ProofArith : public Proof { -private: - static Node toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map); -public: - ProofArith( theory::eq::EqProof * pf ) : d_proof( pf ) {} - //it is simply an equality engine proof - theory::eq::EqProof * d_proof; - void toStream(std::ostream& out); - static void toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map); + public: + ProofArith(std::shared_ptr<theory::eq::EqProof> pf) : d_proof(pf) {} + void toStream(std::ostream& out) override; + private: + static void toStreamLFSC(std::ostream& out, TheoryProof* tp, + const theory::eq::EqProof& pf, + const ProofLetMap& map); + static Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp, + const theory::eq::EqProof& pf, + unsigned tb, const ProofLetMap& map); + // it is simply an equality engine proof + std::shared_ptr<theory::eq::EqProof> d_proof; }; - namespace theory { namespace arith { class TheoryArith; |