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/array_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/array_proof.h')
-rw-r--r-- | src/proof/array_proof.h | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h index f40f13ea6..df8cb58a2 100644 --- a/src/proof/array_proof.h +++ b/src/proof/array_proof.h @@ -19,6 +19,7 @@ #ifndef __CVC4__ARRAY__PROOF_H #define __CVC4__ARRAY__PROOF_H +#include <memory> #include <unordered_set> #include "expr/expr.h" @@ -32,23 +33,23 @@ namespace CVC4 { // Proof object outputted by TheoryARRAY. class ProofArray : public Proof { public: - ProofArray(theory::eq::EqProof* pf, unsigned row, unsigned row1, - unsigned ext); + ProofArray(std::shared_ptr<theory::eq::EqProof> pf, unsigned row, + unsigned row1, unsigned ext); void registerSkolem(Node equality, Node skolem); void toStream(std::ostream& out); void toStream(std::ostream& out, const ProofLetMap& map); - void toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, - const ProofLetMap& map); - private: + void toStreamLFSC(std::ostream& out, TheoryProof* tp, + const theory::eq::EqProof& pf, const ProofLetMap& map); + Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp, - theory::eq::EqProof* pf, unsigned tb, + const theory::eq::EqProof& pf, unsigned tb, const ProofLetMap& map); - // it is simply an equality engine proof - theory::eq::EqProof* d_proof; + // It is simply an equality engine proof. + std::shared_ptr<theory::eq::EqProof> d_proof; /** Merge tag for ROW applications */ unsigned d_reasonRow; |