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.cpp | |
| parent | 85df7998e4362e0a9c796146d07d7b9e91045a31 (diff) | |
Adding garbage collection for Proof objects. (#1294)
Diffstat (limited to 'src/proof/array_proof.cpp')
| -rw-r--r-- | src/proof/array_proof.cpp | 31 |
1 files changed, 21 insertions, 10 deletions
diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index 488c52e33..511a82617 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -115,24 +115,32 @@ inline static bool match(TNode n1, TNode n2) { return true; } -ProofArray::ProofArray(std::shared_ptr<theory::eq::EqProof> pf, unsigned row, - unsigned row1, unsigned ext) - : d_proof(pf), d_reasonRow(row), d_reasonRow1(row1), d_reasonExt(ext) {} +ProofArray::ProofArray(std::shared_ptr<theory::eq::EqProof> pf, + unsigned row, + unsigned row1, + unsigned ext) + : d_proof(pf), d_reasonRow(row), d_reasonRow1(row1), d_reasonExt(ext) +{ +} -void ProofArray::toStream(std::ostream& out) { +void ProofArray::toStream(std::ostream& out) const +{ ProofLetMap map; toStream(out, map); } -void ProofArray::toStream(std::ostream& out, const ProofLetMap& map) { +void ProofArray::toStream(std::ostream& out, const ProofLetMap& map) const +{ Trace("pf::array") << "; Print Array proof..." << std::endl; toStreamLFSC(out, ProofManager::getArrayProof(), *d_proof, map); Debug("pf::array") << "; Print Array proof done!" << std::endl; } -void ProofArray::toStreamLFSC(std::ostream& out, TheoryProof* tp, +void ProofArray::toStreamLFSC(std::ostream& out, + TheoryProof* tp, const theory::eq::EqProof& pf, - const ProofLetMap& map) { + const ProofLetMap& map) const +{ Debug("pf::array") << "Printing array proof in LFSC : " << std::endl; ArrayProofPrinter proofPrinter(d_reasonRow, d_reasonRow1, d_reasonExt); pf.debug_print("pf::array", 0, &proofPrinter); @@ -141,9 +149,12 @@ void ProofArray::toStreamLFSC(std::ostream& out, TheoryProof* tp, Debug("pf::array") << "Printing array proof in LFSC DONE" << std::endl; } -Node ProofArray::toStreamRecLFSC(std::ostream& out, TheoryProof* tp, - const theory::eq::EqProof& pf, unsigned tb, - const ProofLetMap& map) { +Node ProofArray::toStreamRecLFSC(std::ostream& out, + TheoryProof* tp, + const theory::eq::EqProof& pf, + unsigned tb, + const ProofLetMap& map) const +{ Debug("pf::array") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb |