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/array_proof.h | |
parent | 85df7998e4362e0a9c796146d07d7b9e91045a31 (diff) |
Adding garbage collection for Proof objects. (#1294)
Diffstat (limited to 'src/proof/array_proof.h')
-rw-r--r-- | src/proof/array_proof.h | 21 |
1 files changed, 13 insertions, 8 deletions
diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h index df8cb58a2..99ad956a5 100644 --- a/src/proof/array_proof.h +++ b/src/proof/array_proof.h @@ -38,15 +38,20 @@ class ProofArray : public Proof { void registerSkolem(Node equality, Node skolem); - void toStream(std::ostream& out); - void toStream(std::ostream& out, const ProofLetMap& map); - private: - void toStreamLFSC(std::ostream& out, TheoryProof* tp, - const theory::eq::EqProof& pf, const ProofLetMap& map); + void toStream(std::ostream& out) const override; + void toStream(std::ostream& out, const ProofLetMap& map) const override; - Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp, - const theory::eq::EqProof& pf, unsigned tb, - const ProofLetMap& map); + private: + void toStreamLFSC(std::ostream& out, + TheoryProof* tp, + const theory::eq::EqProof& pf, + const ProofLetMap& map) const; + + Node toStreamRecLFSC(std::ostream& out, + TheoryProof* tp, + const theory::eq::EqProof& pf, + unsigned tb, + const ProofLetMap& map) const; // It is simply an equality engine proof. std::shared_ptr<theory::eq::EqProof> d_proof; |