diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-23 06:53:06 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-23 08:53:06 -0500 |
commit | 4c2138a14c4abba2431bc8ba51359d3a565baf05 (patch) | |
tree | 4bf45363b8b76895138669cd8097c2be49f02f80 /src/proof | |
parent | 8de9510b8aa818f555294ebe88d9733cc10ff8b9 (diff) |
Remove ProofProxy (#1965)
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/proof_manager.h | 4 | ||||
-rw-r--r-- | src/proof/sat_proof.h | 15 | ||||
-rw-r--r-- | src/proof/sat_proof_implementation.h | 13 |
3 files changed, 0 insertions, 32 deletions
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 047c32e83..d1833fd07 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -80,10 +80,6 @@ class LFSCUFProof; class LFSCBitVectorProof; class LFSCRewriterProof; -template <class Solver> class ProofProxy; -typedef ProofProxy< CVC4::Minisat::Solver> CoreProofProxy; -typedef ProofProxy< CVC4::BVMinisat::Solver> BVProofProxy; - namespace prop { typedef uint64_t SatVariable; class SatLiteral; diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index 19a8d30cf..57e3a9bc1 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -38,8 +38,6 @@ // Forward declarations. namespace CVC4 { class CnfProof; -template <class Solver> -class ProofProxy; } /* namespace CVC4 */ namespace CVC4 { @@ -192,7 +190,6 @@ class TSatProof { */ void storeUnitResolution(typename Solver::TLit lit); - ProofProxy<Solver>* getProxy() { return d_proxy; } /** * Constructs the SAT proof for the given clause, * by collecting the needed clauses in the d_seen @@ -341,8 +338,6 @@ class TSatProof { const ClauseId d_emptyClauseId; const ClauseId d_nullId; - // proxy class to break circular dependencies - ProofProxy<Solver>* d_proxy; // temporary map for updating CRefs ClauseIdMap d_temp_clauseId; @@ -379,16 +374,6 @@ class TSatProof { Statistics d_statistics; }; /* class TSatProof */ -template <class S> -class ProofProxy { - private: - TSatProof<S>* d_proof; - - public: - ProofProxy(TSatProof<S>* pf); - void updateCRef(typename S::TCRef oldref, typename S::TCRef newref); -}; /* class ProofProxy */ - template <class SatSolver> class LFSCSatProof : public TSatProof<SatSolver> { private: diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index daf98ceea..e3cbae361 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -184,16 +184,6 @@ void ResChain<Solver>::addRedundantLit(typename Solver::TLit lit) { } } -/// ProxyProof -template <class Solver> -ProofProxy<Solver>::ProofProxy(TSatProof<Solver>* proof) : d_proof(proof) {} - -template <class Solver> -void ProofProxy<Solver>::updateCRef(typename Solver::TCRef oldref, - typename Solver::TCRef newref) { - d_proof->updateCRef(oldref, newref); -} - /// SatProof template <class Solver> TSatProof<Solver>::TSatProof(Solver* solver, context::Context* context, @@ -227,13 +217,10 @@ TSatProof<Solver>::TSatProof(Solver* solver, context::Context* context, d_seenLemmas(), d_satProofConstructed(false), d_statistics(name) { - d_proxy = new ProofProxy<Solver>(this); } template <class Solver> TSatProof<Solver>::~TSatProof() { - delete d_proxy; - // FIXME: double free if deleted clause also appears in d_seenLemmas? IdToSatClause::const_iterator it = d_deletedTheoryLemmas.begin(); IdToSatClause::const_iterator end = d_deletedTheoryLemmas.end(); |