Adding garbage collection for Proof objects. (#1294)

1 files changed, 21 insertions, 19 deletions

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 */