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/sat_proof_implementation.h | |
parent | 8de9510b8aa818f555294ebe88d9733cc10ff8b9 (diff) |
Remove ProofProxy (#1965)
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(); |