summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/proof/arith_proof.cpp19
-rw-r--r--src/proof/arith_proof.h3
-rw-r--r--src/proof/array_proof.cpp31
-rw-r--r--src/proof/array_proof.h21
-rw-r--r--src/proof/proof_manager.cpp60
-rw-r--r--src/proof/proof_manager.h40
-rw-r--r--src/proof/proof_output_channel.cpp11
-rw-r--r--src/proof/proof_output_channel.h9
-rw-r--r--src/proof/theory_proof.cpp2
-rw-r--r--src/proof/uf_proof.cpp20
-rw-r--r--src/proof/uf_proof.h7
-rw-r--r--src/smt/command.cpp9
-rw-r--r--src/smt/command.h5
-rw-r--r--src/smt/smt_engine.cpp3
-rw-r--r--src/smt/smt_engine.h5
-rw-r--r--src/smt/smt_engine_check_proof.cpp5
-rw-r--r--src/theory/arrays/theory_arrays.cpp10
-rw-r--r--src/theory/output_channel.h4
-rw-r--r--src/theory/theory_engine.cpp3
-rw-r--r--src/theory/theory_engine.h4
-rw-r--r--src/theory/theory_test_utils.h6
-rw-r--r--src/theory/uf/theory_uf.cpp4
-rw-r--r--src/util/proof.h11
23 files changed, 170 insertions, 122 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,
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<ProofArray> 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 <memory>
+
#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<Proof> 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> 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 <deque>
+#include <memory>
#include <set>
#include <unordered_map>
#include <vector>
@@ -265,7 +266,8 @@ class TheoryEngine {
}
}
- void conflict(TNode conflictNode, Proof* pf = nullptr) override;
+ void conflict(TNode conflictNode,
+ std::unique_ptr<Proof> 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 <iostream>
+#include <memory>
#include <utility>
#include <vector>
@@ -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<Proof> 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<eq::EqProof> pf =
d_proofsEnabled ? std::make_shared<eq::EqProof>() : 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<ProofUF> 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<Expr, ProofLetCount, ExprHashFunction> 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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback