diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/proof/sat_proof.h | 16 | ||||
| -rw-r--r-- | src/proof/sat_proof_implementation.h | 9 |
2 files changed, 20 insertions, 5 deletions
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index 54ad28377..bda8094be 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -313,8 +313,22 @@ class TSatProof { // to SAT solver IdToConflicts d_assumptionConflictsDebug; - // resolutions + // Resolutions. + + /** + * Map from ClauseId to resolution chain corresponding proving the + * clause corresponding to the ClauseId. d_resolutionChains owns the + * memory of the ResChain* it contains. + */ IdResMap d_resolutionChains; + + /* + * Stack containting current ResChain* we are working on. d_resStack + * owns the memory for the ResChain* it contains. Invariant: no + * ResChain* pointer can be both in d_resStack and + * d_resolutionChains. Memory ownership is transfered from + * d_resStack to d_resolutionChains via registerResolution. + */ ResStack d_resStack; bool d_checkRes; diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index a22e38f72..4f3330ef7 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -258,7 +258,6 @@ TSatProof<Solver>::~TSatProof() { delete seen_input_it->second; } - // TODO: Have an expert check this. typedef typename IdResMap::const_iterator ResolutionChainIterator; ResolutionChainIterator resolution_it = d_resolutionChains.begin(); ResolutionChainIterator resolution_it_end = d_resolutionChains.end(); @@ -267,6 +266,8 @@ TSatProof<Solver>::~TSatProof() { delete current; } + // It could be the case that d_resStack is not empty at destruction time + // (for example in the SAT case). typename ResStack::const_iterator resolution_stack_it = d_resStack.begin(); typename ResStack::const_iterator resolution_stack_it_end = d_resStack.end(); for (; resolution_stack_it != resolution_stack_it_end; @@ -718,7 +719,9 @@ void TSatProof<Solver>::registerResolution(ClauseId id, ResChain<Solver>* res) { removeRedundantFromRes(res, id); Assert(res->redundantRemoved()); - // TODO: Have someone with a clue check this. + // Because the SAT solver can add the same clause multiple times, it + // could be the case that a resolution chain for this clause already + // exists (e.g. when removing units in addClause). if (hasResolutionChain(id)) { ResChain<Solver>* current = d_resolutionChains.find(id)->second; delete current; @@ -797,7 +800,6 @@ void TSatProof<Solver>::endResChain(typename Solver::TLit lit) { template <class Solver> void TSatProof<Solver>::cancelResChain() { Assert(d_resStack.size() > 0); - // TODO: Expert check. ResolutionChain* back = d_resStack.back(); delete back; d_resStack.pop_back(); @@ -898,7 +900,6 @@ void TSatProof<Solver>::finalizeProof(typename Solver::TCRef conflict_ref) { print(conflict_id); } - // TODO: Run this rotation by someone. ResChain<Solver>* res = new ResChain<Solver>(conflict_id); // Here, the call to resolveUnit() can reallocate memory in the // clause allocator. So reload conflict ptr each time. |