diff options
author | Tim King <taking@cs.nyu.edu> | 2017-11-15 02:58:30 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2017-11-15 02:58:30 -0800 |
commit | 3c130b44fdecc62b1ace2a739e77f913cd606aa0 (patch) | |
tree | 6abfb806dd45c83606c04dda5c26e9c410ac2ee1 /src/proof/proof_manager.h | |
parent | 85df7998e4362e0a9c796146d07d7b9e91045a31 (diff) |
Adding garbage collection for Proof objects. (#1294)
Diffstat (limited to 'src/proof/proof_manager.h')
-rw-r--r-- | src/proof/proof_manager.h | 40 |
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 */ |