Remove ProofProxy (#1965)

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();