diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-28 12:18:47 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-06-28 12:18:47 -0700 |
commit | aa0c64d35814ef892dbcd0cec805d44599009c41 (patch) | |
tree | ba17209644a2d8c2662728c327416ee42b449f8b /src/prop | |
parent | e799ab0164722e8a4f192ee13223d0eeec6ec004 (diff) |
Fix stale reference in MiniSat when generating UC (#2113)
In MiniSat's analyze(), we were taking a reference of a clause that
could be invalidated by a call to resolveOutUnit(). resolveOutUnit() can
lead to allocation of clauses which in turn can lead to clauses being
reallocated, making the reference stale. The commit encloses the
reference in a code block that makes the lifetime of the reference more
obvious and removes uses of the potentially stale reference.
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 67 |
1 files changed, 41 insertions, 26 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 3c8023395..8f5b37e74 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -698,34 +698,49 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) PROOF( ProofManager::getSatProof()->startResChain(confl); ) do{ assert(confl != CRef_Undef); // (otherwise should be UIP) - Clause& c = ca[confl]; - max_resolution_level = std::max(max_resolution_level, c.level()); - - if (c.removable()) - claBumpActivity(c); - - for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){ - Lit q = c[j]; - - if (!seen[var(q)] && level(var(q)) > 0) { - varBumpActivity(var(q)); - seen[var(q)] = 1; - if (level(var(q)) >= decisionLevel()) - pathC++; - else - out_learnt.push(q); - } else { - // We could be resolving a literal propagated by a clause/theory using - // information from a higher level - if (!seen[var(q)] && level(var(q)) == 0) { - max_resolution_level = std::max(max_resolution_level, user_level(var(q))); - } - // FIXME: can we do it lazily if we actually need the proof? - if (level(var(q)) == 0) { - PROOF( ProofManager::getSatProof()->resolveOutUnit(q); ) - } + { + // ! IMPORTANT ! + // It is not safe to use c after this block of code because + // resolveOutUnit() below may lead to clauses being allocated, which + // in turn may lead to reallocations that invalidate c. + Clause& c = ca[confl]; + max_resolution_level = std::max(max_resolution_level, c.level()); + + if (c.removable()) claBumpActivity(c); + } + + for (int j = (p == lit_Undef) ? 0 : 1, size = ca[confl].size(); + j < size; + j++) + { + Lit q = ca[confl][j]; + + if (!seen[var(q)] && level(var(q)) > 0) + { + varBumpActivity(var(q)); + seen[var(q)] = 1; + if (level(var(q)) >= decisionLevel()) + pathC++; + else + out_learnt.push(q); + } + else + { + // We could be resolving a literal propagated by a clause/theory + // using information from a higher level + if (!seen[var(q)] && level(var(q)) == 0) + { + max_resolution_level = + std::max(max_resolution_level, user_level(var(q))); + } + + // FIXME: can we do it lazily if we actually need the proof? + if (level(var(q)) == 0) + { + PROOF(ProofManager::getSatProof()->resolveOutUnit(q);) } + } } // Select next clause to look at: |