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 | |
parent | 8de9510b8aa818f555294ebe88d9733cc10ff8b9 (diff) |
Remove ProofProxy (#1965)
Diffstat (limited to 'src')
-rw-r--r-- | src/proof/proof_manager.h | 4 | ||||
-rw-r--r-- | src/proof/sat_proof.h | 15 | ||||
-rw-r--r-- | src/proof/sat_proof_implementation.h | 13 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 19 | ||||
-rw-r--r-- | src/prop/bvminisat/core/SolverTypes.h | 8 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 24 | ||||
-rw-r--r-- | src/prop/minisat/core/SolverTypes.h | 28 |
7 files changed, 43 insertions, 68 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(); diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index 885e429f0..8d71e2f65 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -1412,7 +1412,7 @@ void Solver::relocAll(ClauseAllocator& to) // printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1); vec<Watcher>& ws = watches[p]; for (int j = 0; j < ws.size(); j++) - ca.reloc(ws[j].cref, to, d_bvp ? d_bvp->getSatProof()->getProxy() : NULL); + ca.reloc(ws[j].cref, to, d_bvp ? d_bvp->getSatProof() : NULL); } // All reasons: @@ -1421,19 +1421,19 @@ void Solver::relocAll(ClauseAllocator& to) Var v = var(trail[i]); if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)]))) - ca.reloc(vardata[v].reason, to, d_bvp ? d_bvp->getSatProof()->getProxy() : NULL); + ca.reloc(vardata[v].reason, to, d_bvp ? d_bvp->getSatProof() : NULL); } // All learnt: // for (int i = 0; i < learnts.size(); i++) - ca.reloc(learnts[i], to, d_bvp ? d_bvp->getSatProof()->getProxy() : NULL); + ca.reloc(learnts[i], to, d_bvp ? d_bvp->getSatProof() : NULL); // All original: // for (int i = 0; i < clauses.size(); i++) - ca.reloc(clauses[i], to, d_bvp ? d_bvp->getSatProof()->getProxy() : NULL); - + ca.reloc(clauses[i], to, d_bvp ? d_bvp->getSatProof() : NULL); + if(d_bvp){ d_bvp->getSatProof()->finishUpdateCRef(); } } @@ -1451,7 +1451,9 @@ void Solver::garbageCollect() to.moveTo(ca); } -void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to, CVC4::BVProofProxy* proxy) +void ClauseAllocator::reloc(CRef& cr, + ClauseAllocator& to, + CVC4::TSatProof<Solver>* proof) { CRef old = cr; // save the old reference @@ -1460,8 +1462,9 @@ void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to, CVC4::BVProofProxy* p cr = to.alloc(c, c.learnt()); c.relocate(cr); - if (proxy) { - proxy->updateCRef(old, cr); + if (proof) + { + proof->updateCRef(old, cr); } // Copy extra data-fields: diff --git a/src/prop/bvminisat/core/SolverTypes.h b/src/prop/bvminisat/core/SolverTypes.h index 1fd7ac5a7..302db104f 100644 --- a/src/prop/bvminisat/core/SolverTypes.h +++ b/src/prop/bvminisat/core/SolverTypes.h @@ -33,8 +33,8 @@ namespace CVC4 { namespace BVMinisat { class Solver; } -template <class Solver> class ProofProxy; -typedef ProofProxy<BVMinisat::Solver> BVProofProxy; +template <class Solver> +class TSatProof; } namespace CVC4 { @@ -256,7 +256,9 @@ class ClauseAllocator : public RegionAllocator<uint32_t> RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra())); } - void reloc(CRef& cr, ClauseAllocator& to, CVC4::BVProofProxy* proxy = NULL); + void reloc(CRef& cr, + ClauseAllocator& to, + CVC4::TSatProof<Solver>* proof = NULL); }; diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index b034f8460..0967f434c 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -29,8 +29,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "options/prop_options.h" #include "proof/clause_id.h" #include "proof/proof_manager.h" -#include "proof/sat_proof_implementation.h" #include "proof/sat_proof.h" +#include "proof/sat_proof_implementation.h" #include "prop/minisat/minisat.h" #include "prop/minisat/mtl/Sort.h" #include "prop/theory_proxy.h" @@ -1528,7 +1528,7 @@ void Solver::relocAll(ClauseAllocator& to) // printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1); vec<Watcher>& ws = watches[p]; for (int j = 0; j < ws.size(); j++) - ca.reloc(ws[j].cref, to, NULLPROOF( ProofManager::getSatProof()->getProxy() )); + ca.reloc(ws[j].cref, to, NULLPROOF(ProofManager::getSatProof())); } // All reasons: @@ -1537,19 +1537,22 @@ void Solver::relocAll(ClauseAllocator& to) Var v = var(trail[i]); if (hasReasonClause(v) && (ca[reason(v)].reloced() || locked(ca[reason(v)]))) - ca.reloc(vardata[v].reason, to, NULLPROOF( ProofManager::getSatProof()->getProxy() )); + ca.reloc( + vardata[v].reason, to, NULLPROOF(ProofManager::getSatProof())); } // All learnt: // for (int i = 0; i < clauses_removable.size(); i++) - ca.reloc(clauses_removable[i], to, NULLPROOF( ProofManager::getSatProof()->getProxy() )); + ca.reloc( + clauses_removable[i], to, NULLPROOF(ProofManager::getSatProof())); // All original: // for (int i = 0; i < clauses_persistent.size(); i++) - ca.reloc(clauses_persistent[i], to, NULLPROOF( ProofManager::getSatProof()->getProxy() )); + ca.reloc( + clauses_persistent[i], to, NULLPROOF(ProofManager::getSatProof())); - PROOF( ProofManager::getSatProof()->finishUpdateCRef(); ) + PROOF(ProofManager::getSatProof()->finishUpdateCRef();) } @@ -1811,7 +1814,9 @@ CRef Solver::updateLemmas() { return conflict; } -void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to, CVC4::CoreProofProxy* proxy) +void ClauseAllocator::reloc(CRef& cr, + ClauseAllocator& to, + CVC4::TSatProof<Solver>* proof) { // FIXME what is this CRef_lazy @@ -1823,8 +1828,9 @@ void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to, CVC4::CoreProofProxy* cr = to.alloc(c.level(), c, c.removable()); c.relocate(cr); - if (proxy) { - proxy->updateCRef(old, cr); + if (proof) + { + proof->updateCRef(old, cr); } // Copy extra data-fields: // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?) diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h index 116a39a49..bbd6e17a2 100644 --- a/src/prop/minisat/core/SolverTypes.h +++ b/src/prop/minisat/core/SolverTypes.h @@ -33,6 +33,14 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA namespace CVC4 { namespace Minisat { +class Solver; +} +template <class Solver> +class TSatProof; +} // namespace CVC4 + +namespace CVC4 { +namespace Minisat { //================================================================================================= // Variables, literals, lifted booleans, clauses: @@ -168,25 +176,11 @@ inline std::ostream& operator <<(std::ostream& out, Minisat::lbool val) { return out; } - -class Solver; - -class ProofProxyAbstract { -public: - virtual ~ProofProxyAbstract() {} - virtual void updateCRef(Minisat::CRef oldref, Minisat::CRef newref) = 0; -}; - } /* namespace CVC4::Minisat */ } /* namespace CVC4 */ namespace CVC4 { -template <class Solver> class ProofProxy; -typedef ProofProxy<CVC4::Minisat::Solver> CoreProofProxy; -} - -namespace CVC4 { namespace Minisat{ //================================================================================================= @@ -307,8 +301,10 @@ class ClauseAllocator : public RegionAllocator<uint32_t> RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra())); } - void reloc(CRef& cr, ClauseAllocator& to, CVC4::CoreProofProxy* proxy = NULL); - // Implementation moved to Solver.cc. + void reloc(CRef& cr, + ClauseAllocator& to, + CVC4::TSatProof<Solver>* proof = NULL); + // Implementation moved to Solver.cc. }; |