Adding garbage collection for Proof objects. (#1294)

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,