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