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 | |
parent | 85df7998e4362e0a9c796146d07d7b9e91045a31 (diff) |
Adding garbage collection for Proof objects. (#1294)
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/arith_proof.cpp | 19 | ||||
-rw-r--r-- | src/proof/arith_proof.h | 3 | ||||
-rw-r--r-- | src/proof/array_proof.cpp | 31 | ||||
-rw-r--r-- | src/proof/array_proof.h | 21 | ||||
-rw-r--r-- | src/proof/proof_manager.cpp | 60 | ||||
-rw-r--r-- | src/proof/proof_manager.h | 40 | ||||
-rw-r--r-- | src/proof/proof_output_channel.cpp | 11 | ||||
-rw-r--r-- | src/proof/proof_output_channel.h | 9 | ||||
-rw-r--r-- | src/proof/theory_proof.cpp | 2 | ||||
-rw-r--r-- | src/proof/uf_proof.cpp | 20 | ||||
-rw-r--r-- | src/proof/uf_proof.h | 7 |
11 files changed, 129 insertions, 94 deletions
diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp index dd3ac0bde..89221dc69 100644 --- a/src/proof/arith_proof.cpp +++ b/src/proof/arith_proof.cpp @@ -67,26 +67,31 @@ inline static bool match(TNode n1, TNode n2) { return true; } - -void ProofArith::toStream(std::ostream& out) { +void ProofArith::toStream(std::ostream& out) const +{ Trace("theory-proof-debug") << "; Print Arith proof..." << std::endl; //AJR : carry this further? ProofLetMap map; toStreamLFSC(out, ProofManager::getArithProof(), *d_proof, map); } -void ProofArith::toStreamLFSC(std::ostream& out, TheoryProof* tp, +void ProofArith::toStreamLFSC(std::ostream& out, + TheoryProof* tp, const theory::eq::EqProof& pf, - const ProofLetMap& map) { + const ProofLetMap& map) +{ Debug("lfsc-arith") << "Printing arith proof in LFSC : " << std::endl; pf.debug_print("lfsc-arith"); Debug("lfsc-arith") << std::endl; toStreamRecLFSC(out, tp, pf, 0, map); } -Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof* tp, - const theory::eq::EqProof& pf, unsigned tb, - const ProofLetMap& map) { +Node ProofArith::toStreamRecLFSC(std::ostream& out, + TheoryProof* tp, + const theory::eq::EqProof& pf, + unsigned tb, + const ProofLetMap& map) +{ Debug("pf::arith") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h index b36909f78..0a44f45c0 100644 --- a/src/proof/arith_proof.h +++ b/src/proof/arith_proof.h @@ -33,7 +33,8 @@ namespace CVC4 { class ProofArith : public Proof { public: ProofArith(std::shared_ptr<theory::eq::EqProof> pf) : d_proof(pf) {} - void toStream(std::ostream& out) override; + void toStream(std::ostream& out) const override; + private: static void toStreamLFSC(std::ostream& out, TheoryProof* tp, const theory::eq::EqProof& pf, 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 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; diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index ba327f5f7..89adf6c2b 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -56,18 +56,18 @@ std::string append(const std::string& str, uint64_t num) { return os.str(); } -ProofManager::ProofManager(context::Context* context, ProofFormat format): - d_context(context), - d_satProof(NULL), - d_cnfProof(NULL), - d_theoryProof(NULL), - d_inputFormulas(), - d_inputCoreFormulas(context), - d_outputCoreFormulas(context), - d_nextId(0), - d_fullProof(NULL), - d_format(format), - d_deps(context) +ProofManager::ProofManager(context::Context* context, ProofFormat format) + : d_context(context), + d_satProof(NULL), + d_cnfProof(NULL), + d_theoryProof(NULL), + d_inputFormulas(), + d_inputCoreFormulas(context), + d_outputCoreFormulas(context), + d_nextId(0), + d_fullProof(), + d_format(format), + d_deps(context) { } @@ -75,24 +75,23 @@ ProofManager::~ProofManager() { if (d_satProof) delete d_satProof; if (d_cnfProof) delete d_cnfProof; if (d_theoryProof) delete d_theoryProof; - if (d_fullProof) delete d_fullProof; } ProofManager* ProofManager::currentPM() { return smt::currentProofManager(); } - -Proof* ProofManager::getProof(SmtEngine* smt) { - if (currentPM()->d_fullProof != NULL) { - return currentPM()->d_fullProof; +const Proof& ProofManager::getProof(SmtEngine* smt) +{ + if (!currentPM()->d_fullProof) + { + Assert(currentPM()->d_format == LFSC); + currentPM()->d_fullProof.reset(new LFSCProof( + smt, + static_cast<LFSCCoreSatProof*>(getSatProof()), + static_cast<LFSCCnfProof*>(getCnfProof()), + static_cast<LFSCTheoryProofEngine*>(getTheoryProofEngine()))); } - Assert (currentPM()->d_format == LFSC); - - currentPM()->d_fullProof = new LFSCProof(smt, - (LFSCCoreSatProof*)getSatProof(), - (LFSCCnfProof*)getCnfProof(), - (LFSCTheoryProofEngine*)getTheoryProofEngine()); - return currentPM()->d_fullProof; + return *(currentPM()->d_fullProof); } CoreSatProof* ProofManager::getSatProof() { @@ -551,12 +550,13 @@ LFSCProof::LFSCProof(SmtEngine* smtEngine, , d_smtEngine(smtEngine) {} -void LFSCProof::toStream(std::ostream& out, const ProofLetMap& map) { +void LFSCProof::toStream(std::ostream& out, const ProofLetMap& map) const +{ Unreachable(); } -void LFSCProof::toStream(std::ostream& out) { - +void LFSCProof::toStream(std::ostream& out) const +{ Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER); Assert(!d_satProof->proofConstructed()); @@ -743,7 +743,8 @@ void LFSCProof::toStream(std::ostream& out) { void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, std::ostream& os, std::ostream& paren, - ProofLetMap& globalLetMap) { + ProofLetMap& globalLetMap) const +{ os << "\n ;; In the preprocessor we trust \n"; NodeSet::const_iterator it = assertions.begin(); NodeSet::const_iterator end = assertions.end(); @@ -842,7 +843,8 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, os << "\n"; } -void LFSCProof::checkUnrewrittenAssertion(const NodeSet& rewrites) { +void LFSCProof::checkUnrewrittenAssertion(const NodeSet& rewrites) const +{ Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion starting" << std::endl; NodeSet::const_iterator rewrite; diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index f77a96726..047c32e83 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -20,6 +20,7 @@ #define __CVC4__PROOF_MANAGER_H #include <iosfwd> +#include <memory> #include <unordered_map> #include <unordered_set> @@ -58,7 +59,6 @@ const ClauseId ClauseIdEmpty(-1); const ClauseId ClauseIdUndef(-2); const ClauseId ClauseIdError(-3); -class Proof; template <class Solver> class TSatProof; typedef TSatProof< CVC4::Minisat::Solver> CoreSatProof; @@ -159,7 +159,7 @@ class ProofManager { int d_nextId; - Proof* d_fullProof; + std::unique_ptr<Proof> d_fullProof; ProofFormat d_format; // used for now only in debug builds CDNodeToNodes d_deps; @@ -187,7 +187,7 @@ public: static void initTheoryProofEngine(); // getting various proofs - static Proof* getProof(SmtEngine* smt); + static const Proof& getProof(SmtEngine* smt); static CoreSatProof* getSatProof(); static CnfProof* getCnfProof(); static TheoryProofEngine* getTheoryProofEngine(); @@ -299,29 +299,31 @@ private: std::set<Node> satClauseToNodeSet(prop::SatClause* clause); };/* class ProofManager */ -class LFSCProof : public Proof { - LFSCCoreSatProof* d_satProof; - LFSCCnfProof* d_cnfProof; - LFSCTheoryProofEngine* d_theoryProof; - SmtEngine* d_smtEngine; +class LFSCProof : public Proof +{ + public: + LFSCProof(SmtEngine* smtEngine, + LFSCCoreSatProof* sat, + LFSCCnfProof* cnf, + LFSCTheoryProofEngine* theory); + ~LFSCProof() override {} + void toStream(std::ostream& out) const override; + void toStream(std::ostream& out, const ProofLetMap& map) const override; + private: // FIXME: hack until we get preprocessing void printPreprocessedAssertions(const NodeSet& assertions, std::ostream& os, std::ostream& paren, - ProofLetMap& globalLetMap); + ProofLetMap& globalLetMap) const; - void checkUnrewrittenAssertion(const NodeSet& assertions); + void checkUnrewrittenAssertion(const NodeSet& assertions) const; -public: - LFSCProof(SmtEngine* smtEngine, - LFSCCoreSatProof* sat, - LFSCCnfProof* cnf, - LFSCTheoryProofEngine* theory); - virtual void toStream(std::ostream& out); - virtual void toStream(std::ostream& out, const ProofLetMap& map); - virtual ~LFSCProof() {} -};/* class LFSCProof */ + LFSCCoreSatProof* d_satProof; + LFSCCnfProof* d_cnfProof; + LFSCTheoryProofEngine* d_theoryProof; + SmtEngine* d_smtEngine; +}; /* class LFSCProof */ std::ostream& operator<<(std::ostream& out, CVC4::ProofRule k); }/* CVC4 namespace */ diff --git a/src/proof/proof_output_channel.cpp b/src/proof/proof_output_channel.cpp index 85a742dfa..a75987c06 100644 --- a/src/proof/proof_output_channel.cpp +++ b/src/proof/proof_output_channel.cpp @@ -24,18 +24,19 @@ namespace CVC4 { ProofOutputChannel::ProofOutputChannel() : d_conflict(), d_proof(nullptr) {} - -Proof* ProofOutputChannel::getConflictProof() { +const Proof& ProofOutputChannel::getConflictProof() const +{ Assert(hasConflict()); - return d_proof; + return *d_proof; } -void ProofOutputChannel::conflict(TNode n, Proof* pf) { +void ProofOutputChannel::conflict(TNode n, std::unique_ptr<Proof> pf) +{ Trace("pf::tp") << "ProofOutputChannel: CONFLICT: " << n << std::endl; Assert(!hasConflict()); Assert(!d_proof); d_conflict = n; - d_proof = pf; + d_proof = std::move(pf); Assert(hasConflict()); Assert(d_proof); } diff --git a/src/proof/proof_output_channel.h b/src/proof/proof_output_channel.h index 9516eb71b..e2958e8a5 100644 --- a/src/proof/proof_output_channel.h +++ b/src/proof/proof_output_channel.h @@ -16,13 +16,14 @@ #ifndef __CVC4__PROOF_OUTPUT_CHANNEL_H #define __CVC4__PROOF_OUTPUT_CHANNEL_H +#include <memory> #include <set> #include <unordered_set> #include "expr/node.h" -#include "util/proof.h" #include "theory/output_channel.h" #include "theory/theory.h" +#include "util/proof.h" namespace CVC4 { @@ -35,7 +36,7 @@ class ProofOutputChannel : public theory::OutputChannel { * This may be called at most once per ProofOutputChannel. * Requires that `n` and `pf` are non-null. */ - void conflict(TNode n, Proof* pf) override; + void conflict(TNode n, std::unique_ptr<Proof> pf) override; bool propagate(TNode x) override; theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool) override; theory::LemmaStatus splitLemma(TNode, bool) override; @@ -50,12 +51,12 @@ class ProofOutputChannel : public theory::OutputChannel { * Returns the proof passed into the conflict() call. * Requires hasConflict() to hold. */ - Proof* getConflictProof(); + const Proof& getConflictProof() const; Node getLastLemma() const { return d_lemma; } private: Node d_conflict; - Proof* d_proof; + std::unique_ptr<Proof> d_proof; Node d_lemma; std::set<Node> d_propagations; }; /* class ProofOutputChannel */ diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 62dcd0006..47a1191ad 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -1057,7 +1057,7 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, th->check(theory::Theory::EFFORT_FULL); } else { Debug("pf::tp") << "Calling oc.d_proof->toStream(os)" << std::endl; - oc.getConflictProof()->toStream(os, map); + oc.getConflictProof().toStream(os, map); Debug("pf::tp") << "Calling oc.d_proof->toStream(os) -- DONE!" << std::endl; } 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 diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h index 3dc7d9b58..1b14bd15f 100644 --- a/src/proof/uf_proof.h +++ b/src/proof/uf_proof.h @@ -30,11 +30,12 @@ namespace CVC4 { // proof object outputted by TheoryUF -class ProofUF : public Proof { +class ProofUF : public Proof +{ 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; + void toStream(std::ostream& out) const override; + void toStream(std::ostream& out, const ProofLetMap& map) const override; private: static void toStreamLFSC(std::ostream& out, TheoryProof* tp, |