From 3c130b44fdecc62b1ace2a739e77f913cd606aa0 Mon Sep 17 00:00:00 2001 From: Tim King Date: Wed, 15 Nov 2017 02:58:30 -0800 Subject: [PATCH] Adding garbage collection for Proof objects. (#1294) --- src/proof/arith_proof.cpp | 19 +++++--- src/proof/arith_proof.h | 3 +- src/proof/array_proof.cpp | 31 ++++++++----- src/proof/array_proof.h | 21 +++++---- src/proof/proof_manager.cpp | 60 +++++++++++++------------- src/proof/proof_manager.h | 40 +++++++++-------- src/proof/proof_output_channel.cpp | 11 ++--- src/proof/proof_output_channel.h | 9 ++-- src/proof/theory_proof.cpp | 2 +- src/proof/uf_proof.cpp | 20 ++++++--- src/proof/uf_proof.h | 7 +-- src/smt/command.cpp | 9 ++-- src/smt/command.h | 5 ++- src/smt/smt_engine.cpp | 3 +- src/smt/smt_engine.h | 5 ++- src/smt/smt_engine_check_proof.cpp | 5 ++- src/theory/arrays/theory_arrays.cpp | 10 +++-- src/theory/output_channel.h | 4 +- src/theory/theory_engine.cpp | 3 +- src/theory/theory_engine.h | 4 +- src/theory/theory_test_utils.h | 6 ++- src/theory/uf/theory_uf.cpp | 4 +- src/util/proof.h | 11 ++--- test/unit/theory/theory_engine_white.h | 7 ++- test/unit/theory/theory_white.h | 8 ++-- 25 files changed, 180 insertions(+), 127 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 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 pf, unsigned row, - unsigned row1, unsigned ext) - : d_proof(pf), d_reasonRow(row), d_reasonRow1(row1), d_reasonExt(ext) {} +ProofArray::ProofArray(std::shared_ptr 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 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(getSatProof()), + static_cast(getCnfProof()), + static_cast(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 +#include #include #include @@ -58,7 +59,6 @@ const ClauseId ClauseIdEmpty(-1); const ClauseId ClauseIdUndef(-2); const ClauseId ClauseIdError(-3); -class Proof; template class TSatProof; typedef TSatProof< CVC4::Minisat::Solver> CoreSatProof; @@ -159,7 +159,7 @@ class ProofManager { int d_nextId; - Proof* d_fullProof; + std::unique_ptr 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 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 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 #include #include #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 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 d_proof; Node d_lemma; std::set 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& 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 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, diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 3df2c4f41..aea6365b7 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1210,12 +1210,12 @@ std::string GetModelCommand::getCommandName() const throw() { /* class GetProofCommand */ GetProofCommand::GetProofCommand() throw() - : d_result(nullptr), d_smtEngine(nullptr) {} + : d_smtEngine(nullptr), d_result(nullptr) {} void GetProofCommand::invoke(SmtEngine* smtEngine) { try { d_smtEngine = smtEngine; - d_result = smtEngine->getProof(); + d_result = &smtEngine->getProof(); d_commandStatus = CommandSuccess::instance(); } catch (RecoverableModalException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); @@ -1226,10 +1226,7 @@ void GetProofCommand::invoke(SmtEngine* smtEngine) { } } -Proof* GetProofCommand::getResult() const throw() { - return d_result; -} - +const Proof& GetProofCommand::getResult() const throw() { return *d_result; } void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const { if(! ok()) { this->Command::printResult(out, verbosity); diff --git a/src/smt/command.h b/src/smt/command.h index a60c85a3c..33f58aa99 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -637,7 +637,7 @@ class CVC4_PUBLIC GetProofCommand : public Command { GetProofCommand() throw(); ~GetProofCommand() throw() {} void invoke(SmtEngine* smtEngine); - Proof* getResult() const throw(); + const Proof& getResult() const throw(); void printResult(std::ostream& out, uint32_t verbosity = 2) const; Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); @@ -645,8 +645,9 @@ class CVC4_PUBLIC GetProofCommand : public Command { std::string getCommandName() const throw(); protected: - Proof* d_result; SmtEngine* d_smtEngine; + // d_result is owned by d_smtEngine. + const Proof* d_result; }; /* class GetProofCommand */ class CVC4_PUBLIC GetInstantiationsCommand : public Command { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e70f4db05..e4ec57bb4 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -5286,7 +5286,8 @@ UnsatCore SmtEngine::getUnsatCore() { } // TODO(#1108): Simplify the error reporting of this method. -Proof* SmtEngine::getProof() { +const Proof& SmtEngine::getProof() +{ Trace("smt") << "SMT getProof()" << endl; SmtScope smts(this); finalOptionsAreSet(); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 8961fbee0..18fc39857 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -524,8 +524,11 @@ public: * Get the last proof (only if immediately preceded by an UNSAT * or VALID query). Only permitted if CVC4 was built with proof * support and produce-proofs is on. + * + * The Proof object is owned by this SmtEngine until the SmtEngine is + * destroyed. */ - Proof* getProof(); + const Proof& getProof(); /** * Print all instantiations made by the quantifiers module. diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp index f48f6753d..76a30ef9b 100644 --- a/src/smt/smt_engine_check_proof.cpp +++ b/src/smt/smt_engine_check_proof.cpp @@ -32,6 +32,7 @@ #include "base/cvc4_assert.h" #include "base/output.h" #include "smt/smt_engine.h" +#include "util/proof.h" #include "util/statistics_registry.h" #if (IS_LFSC_BUILD && IS_PROOFS_BUILD) @@ -66,7 +67,7 @@ void SmtEngine::checkProof() { Chat() << "generating proof..." << endl; - Proof* pf = getProof(); + const Proof& pf = getProof(); Chat() << "checking proof..." << endl; @@ -112,7 +113,7 @@ void SmtEngine::checkProof() { ofstream pfStream(pfFile); pfStream << proof::plf_signatures << endl; - pf->toStream(pfStream); + pf.toStream(pfStream); pfStream.close(); lfscc_init(); lfscc_check_file(pfFile, false, false, false, false, false, false, false); diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index b43ba5591..af417f740 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -2245,15 +2245,17 @@ void TheoryArrays::conflict(TNode a, TNode b) { d_conflictNode = explain(a.eqNode(b), proof.get()); if (!d_inCheckModel) { - ProofArray* proof_array = NULL; + std::unique_ptr proof_array; if (d_proofsEnabled) { proof->debug_print("pf::array"); - proof_array = new ProofArray(proof, /*row=*/d_reasonRow, - /*row1=*/d_reasonRow1, /*ext=*/d_reasonExt); + proof_array.reset(new ProofArray(proof, + /*row=*/d_reasonRow, + /*row1=*/d_reasonRow1, + /*ext=*/d_reasonExt)); } - d_out->conflict(d_conflictNode, proof_array); + d_out->conflict(d_conflictNode, std::move(proof_array)); } d_conflict = true; diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 2c11097db..cc8cee481 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -19,6 +19,8 @@ #ifndef __CVC4__THEORY__OUTPUT_CHANNEL_H #define __CVC4__THEORY__OUTPUT_CHANNEL_H +#include + #include "base/cvc4_assert.h" #include "proof/proof_manager.h" #include "smt/logic_exception.h" @@ -97,7 +99,7 @@ class OutputChannel { * @param pf - a proof of the conflict. This is only non-null if proofs * are enabled. */ - virtual void conflict(TNode n, Proof* pf = nullptr) = 0; + virtual void conflict(TNode n, std::unique_ptr pf = nullptr) = 0; /** * Propagate a theory literal. diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 6c49f2914..d01bd537e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -202,7 +202,8 @@ bool TheoryEngine::EngineOutputChannel::propagate(TNode literal) { } void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, - Proof* proof) { + std::unique_ptr proof) +{ Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 9afd4e5d9..91a88274e 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -20,6 +20,7 @@ #define __CVC4__THEORY_ENGINE_H #include +#include #include #include #include @@ -265,7 +266,8 @@ class TheoryEngine { } } - void conflict(TNode conflictNode, Proof* pf = nullptr) override; + void conflict(TNode conflictNode, + std::unique_ptr pf = nullptr) override; bool propagate(TNode literal) override; theory::LemmaStatus lemma(TNode lemma, ProofRule rule, diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index 4e0fd3e4d..8c2355cf4 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -20,6 +20,7 @@ #define __CVC4__THEORY__THEORY_TEST_UTILS_H #include +#include #include #include @@ -27,6 +28,7 @@ #include "expr/node.h" #include "theory/interrupted.h" #include "theory/output_channel.h" +#include "util/proof.h" #include "util/unsafe_interrupt_exception.h" namespace CVC4 { @@ -67,8 +69,8 @@ public: ~TestOutputChannel() override {} void safePoint(uint64_t amount) override {} - - void conflict(TNode n, Proof* pf = nullptr) override { + void conflict(TNode n, std::unique_ptr pf) override + { push(CONFLICT, n); } diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 170621603..f97a4b639 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -634,8 +634,8 @@ void TheoryUF::conflict(TNode a, TNode b) { std::shared_ptr pf = d_proofsEnabled ? std::make_shared() : nullptr; d_conflictNode = explain(a.eqNode(b), pf.get()); - ProofUF* puf = d_proofsEnabled ? new ProofUF( pf ) : NULL; - d_out->conflict(d_conflictNode, puf); + std::unique_ptr puf(d_proofsEnabled ? new ProofUF(pf) : nullptr); + d_out->conflict(d_conflictNode, std::move(puf)); d_conflict = true; } diff --git a/src/util/proof.h b/src/util/proof.h index b34e4aed9..24f8bf42a 100644 --- a/src/util/proof.h +++ b/src/util/proof.h @@ -31,11 +31,12 @@ struct ExprHashFunction; typedef std::unordered_map ProofLetMap; -class CVC4_PUBLIC Proof { -public: - virtual ~Proof() { } - virtual void toStream(std::ostream& out) = 0; - virtual void toStream(std::ostream& out, const ProofLetMap& map) = 0; +class CVC4_PUBLIC Proof +{ + public: + virtual ~Proof() {} + virtual void toStream(std::ostream& out) const = 0; + virtual void toStream(std::ostream& out, const ProofLetMap& map) const = 0; };/* class Proof */ }/* CVC4 namespace */ diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 9e99ce884..d480bbb75 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -22,6 +22,7 @@ #include #include +#include #include #include "base/cvc4_assert.h" @@ -39,6 +40,7 @@ #include "theory/theory_engine.h" #include "theory/valuation.h" #include "util/integer.h" +#include "util/proof.h" #include "util/rational.h" using namespace CVC4; @@ -52,7 +54,10 @@ using namespace CVC4::theory::bv; using namespace std; class FakeOutputChannel : public OutputChannel { - void conflict(TNode n, Proof* pf) override { Unimplemented(); } + void conflict(TNode n, std::unique_ptr pf) override + { + Unimplemented(); + } bool propagate(TNode n) override { Unimplemented(); } LemmaStatus lemma(TNode n, ProofRule rule, bool removable, bool preprocess, bool sendAtoms) override { diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h index d1517d7c2..e66960654 100644 --- a/test/unit/theory/theory_white.h +++ b/test/unit/theory/theory_white.h @@ -15,9 +15,9 @@ **/ #include +#include #include -// taking: Add include for Proof*. #include "context/context.h" #include "expr/node.h" #include "expr/node_manager.h" @@ -25,7 +25,7 @@ #include "smt/smt_engine_scope.h" #include "theory/theory.h" #include "theory/theory_engine.h" - +#include "util/proof.h" using namespace CVC4; using namespace CVC4::theory; @@ -46,8 +46,8 @@ class TestOutputChannel : public OutputChannel { ~TestOutputChannel() override {} void safePoint(uint64_t amount) override {} - - void conflict(TNode n, Proof* pf = nullptr) override { + void conflict(TNode n, std::unique_ptr pf) override + { push(CONFLICT, n); } -- 2.30.2