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