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/uf_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/uf_proof.h')
-rw-r--r-- | src/proof/uf_proof.h | 31 |
1 files changed, 19 insertions, 12 deletions
diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h index b817ceb69..3dc7d9b58 100644 --- a/src/proof/uf_proof.h +++ b/src/proof/uf_proof.h @@ -19,28 +19,35 @@ #ifndef __CVC4__UF__PROOF_H #define __CVC4__UF__PROOF_H +#include <memory> #include <unordered_set> #include "expr/expr.h" -#include "proof/proof_manager.h" +#include "proof/theory_proof.h" #include "theory/uf/equality_engine.h" +#include "util/proof.h" namespace CVC4 { -//proof object outputted by TheoryUF +// proof object outputted by TheoryUF class ProofUF : public Proof { -private: - static Node toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map); -public: - ProofUF( theory::eq::EqProof * pf ) : d_proof( pf ) {} - //it is simply an equality engine proof - theory::eq::EqProof * d_proof; - void toStream(std::ostream& out); - void toStream(std::ostream& out, const ProofLetMap& map); - static void toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map); + public: + ProofUF(std::shared_ptr<theory::eq::EqProof> pf) : d_proof(pf) {} + void toStream(std::ostream& out) override; + void toStream(std::ostream& out, const ProofLetMap& map) 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 uf { class TheoryUF; |