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/uf_proof.cpp | |
| parent | 85df7998e4362e0a9c796146d07d7b9e91045a31 (diff) | |
Adding garbage collection for Proof objects. (#1294)
Diffstat (limited to 'src/proof/uf_proof.cpp')
| -rw-r--r-- | src/proof/uf_proof.cpp | 20 |
1 files changed, 13 insertions, 7 deletions
diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index f882883e7..746cbbc54 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -66,21 +66,24 @@ inline static bool match(TNode n1, TNode n2) { return true; } - -void ProofUF::toStream(std::ostream& out) { +void ProofUF::toStream(std::ostream& out) const +{ ProofLetMap map; toStream(out, map); } -void ProofUF::toStream(std::ostream& out, const ProofLetMap& map) { +void ProofUF::toStream(std::ostream& out, const ProofLetMap& map) const +{ Trace("theory-proof-debug") << "; Print UF proof..." << std::endl; //AJR : carry this further? toStreamLFSC(out, ProofManager::getUfProof(), *d_proof, map); } -void ProofUF::toStreamLFSC(std::ostream& out, TheoryProof* tp, +void ProofUF::toStreamLFSC(std::ostream& out, + TheoryProof* tp, const theory::eq::EqProof& pf, - const ProofLetMap& map) { + const ProofLetMap& map) +{ Debug("pf::uf") << "ProofUF::toStreamLFSC starting" << std::endl; Debug("lfsc-uf") << "Printing uf proof in LFSC : " << std::endl; pf.debug_print("lfsc-uf"); @@ -88,9 +91,12 @@ void ProofUF::toStreamLFSC(std::ostream& out, TheoryProof* tp, toStreamRecLFSC( out, tp, pf, 0, map ); } -Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof* tp, +Node ProofUF::toStreamRecLFSC(std::ostream& out, + TheoryProof* tp, const theory::eq::EqProof& pf, - unsigned tb, const ProofLetMap& map) { + unsigned tb, + const ProofLetMap& map) +{ Debug("pf::uf") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb |