diff options
Diffstat (limited to 'src/proof/sat_proof_implementation.h')
-rw-r--r-- | src/proof/sat_proof_implementation.h | 13 |
1 files changed, 0 insertions, 13 deletions
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(); |