Adding garbage collection for Proof objects. (#1294)

diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index dd3ac0bde285373c4b82f5e285539c3b637cfe42..89221dc6913efab7713786ca6e60b24a4a9f6381 100644 (file)
--- 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 b36909f785dc93d9d123c76269fc48ffe34a8bfe..0a44f45c0e4b732c707a98b5dfa808dfeea037a1 100644 (file)
--- 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 488c52e334252cf7c9b7d51190d0aea72e296318..511a82617a83ecd5e1c59aa50ae3276f3de1445a 100644 (file)
--- 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 df8cb58a2b7d6e4af5a0e8416a03dffd9a8545ae..99ad956a59ebc17b5e7fc5f2b32d8c78fcc25c51 100644 (file)
--- 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 ba327f5f7798b9eb85c249759aee027b8db8a70f..89adf6c2b90b1b7b2db46ec1b52a1719a0543e52 100644 (file)
--- 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 f77a967264db018b02c877b80e80848dd438c441..047c32e8382145b43b2bec4dda8da956276a268a 100644 (file)
--- 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 85a742dfafeb1a3564f6a31c00b443451397286a..a75987c06a5c0135f59c8c4f3152a7fcbecbf577 100644 (file)
--- 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 9516eb71b22bb2a099b54979ff7af602bdad65f8..e2958e8a507cd1da937c74fa58d9fdcdb18527af 100644 (file)
--- 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 62dcd00068cd21af51733ca679d7c4293b3fc5bd..47a1191ada28eb4eaac1a4f44b5b43ea861d43ae 100644 (file)
--- 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 f882883e74e7c5e97039e349867aa92ffc9d1d53..746cbbc54d1bc8bda11104ff4a731999e74b26b1 100644 (file)
--- 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 3dc7d9b58e2d04c4feac6ccee0886cdd998f8e52..1b14bd15fe59de61237746779c2ae78ccabc7924 100644 (file)
--- 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 3df2c4f41e087125fae1526cbb11a2dd4c61618b..aea6365b7506c6bf72a4a593f562c3597587a877 100644 (file)
--- 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 a60c85a3cf1ae5e9a4593d260d10cfcc20829d00..33f58aa997044d73e1a10aaf18870134934f2eb5 100644 (file)
--- 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 e70f4db059e677fd1ac7819ba9cd858fa933466a..e4ec57bb4807426056183e342430953163d69aab 100644 (file)
--- 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 8961fbee0831123eb0fa3f16f680245fa5439ce9..18fc39857acf8d642ab523e06a20fd57eab3c270 100644 (file)
--- 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 f48f6753da3c91fda23f7af5d36aeb1270165ceb..76a30ef9b1ccb491af5277185f594f9a885957d4 100644 (file)
--- 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 b43ba559120da10accf8bf8462579345113450b3..af417f7401725f9ba4973d873c209b65635de09f 100644 (file)
--- 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 2c11097db1e03c233b1b9369d1223c32e9c435a4..cc8cee48180457e83634ee5c5602a697d13cb537 100644 (file)
--- 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 6c49f2914574685ae6c2a7984511316eda620e96..d01bd537ec46b30bd84ad1d84b17b1dbb503f092 100644 (file)
--- 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 9afd4e5d9ce3ad5821c1afea2cf892b91763fd0d..91a88274e1f3deaf9a779b1bd7db2e655dab852f 100644 (file)
--- 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 4e0fd3e4db9d81705e740fd8d42e5dbf4bba6151..8c2355cf4626678983f153193a4919ce1e707047 100644 (file)
--- 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 1706216039ebef1f737a41072eb11f3059c180aa..f97a4b63962e5f0585b315fef2c98da29c1bb4a6 100644 (file)
--- 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 b34e4aed900fb092be71812d6cd19169ccdf22a5..24f8bf42a65cbb70e3fda55fcfcbd60e846b56b6 100644 (file)
--- 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 */

diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 9e99ce8842127f3e6c743c50dc0ffdb168becabf..d480bbb75ef781f1739b5a84cad2a841aa73b8ad 100644 (file)
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -22,6 +22,7 @@
 
 #include <deque>
 #include <iostream>
+#include <memory>
 #include <string>
 
 #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<Proof> 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 d1517d7c269fef03d8aa732e0e1a3ce21a19353e..e669606545f8454991c593ba31f92c93e50662d9 100644 (file)
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -15,9 +15,9 @@
  **/
 
 #include <cxxtest/TestSuite.h>
+#include <memory>
 #include <vector>
 
-// 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<Proof> pf) override
+  {
     push(CONFLICT, n);
   }