diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-07-13 13:24:43 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-13 13:24:43 -0700 |
commit | ca65101e2d56a476367c8ad09b416b66403be7a7 (patch) | |
tree | f0217edeee991073146d7d681cdf64c6c3476f22 /src/prop | |
parent | c369afa180b7cb3d9388c39d18fcb81e8246ff21 (diff) |
Properly clean up assertion stack in CnfProof (#2147)
Fixes issue #2137. CnfProof has a stack of assertions that are being
converted to clauses. Previously, it could happen that while an
assertion was being added, TheoryProxy::explainPropagation() would be
called from Solver::reason() and push an assertion to the stack that was
then not removed. This lead to a clause id of the assertion being
associated with the explanation instead, which in turn could lead to a
wrong unsat core. This commit identifies two cases where
TheoryProxy::explainPropagation() is called without cleaning up the
assertion stack afterwards. It also adds an assertion that the assertion
stack must be empty when we are getting the unsat core.
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 59 |
1 files changed, 34 insertions, 25 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 8f5b37e74..c312ac146 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -236,33 +236,34 @@ void Solver::resizeVars(int newSize) { } CRef Solver::reason(Var x) { + Debug("pf::sat") << "Solver::reason(" << x << ")" << std::endl; - // If we already have a reason, just return it - if (vardata[x].reason != CRef_Lazy) return vardata[x].reason; + // If we already have a reason, just return it + if (vardata[x].reason != CRef_Lazy) return vardata[x].reason; - // What's the literal we are trying to explain - Lit l = mkLit(x, value(x) != l_True); + // What's the literal we are trying to explain + Lit l = mkLit(x, value(x) != l_True); - // Get the explanation from the theory - SatClause explanation_cl; - // FIXME: at some point return a tag with the theory that spawned you - proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l), - explanation_cl); - vec<Lit> explanation; - MinisatSatSolver::toMinisatClause(explanation_cl, explanation); + // Get the explanation from the theory + SatClause explanation_cl; + // FIXME: at some point return a tag with the theory that spawned you + proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l), explanation_cl); + vec<Lit> explanation; + MinisatSatSolver::toMinisatClause(explanation_cl, explanation); - Debug("pf::sat") << "Solver::reason: explanation_cl = " << explanation_cl << std::endl; + Debug("pf::sat") << "Solver::reason: explanation_cl = " << explanation_cl + << std::endl; - // Sort the literals by trail index level - lemma_lt lt(*this); - sort(explanation, lt); - Assert(explanation[0] == l); + // Sort the literals by trail index level + lemma_lt lt(*this); + sort(explanation, lt); + Assert(explanation[0] == l); - // Compute the assertion level for this clause - int explLevel = 0; - if (assertionLevelOnly()) - { - explLevel = assertionLevel; + // Compute the assertion level for this clause + int explLevel = 0; + if (assertionLevelOnly()) + { + explLevel = assertionLevel; } else { @@ -321,10 +322,15 @@ CRef Solver::reason(Var x) { // FIXME: at some point will need more information about where this explanation // came from (ie. the theory/sharing) Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)" << std::endl; - PROOF (ClauseId id = ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA); - ProofManager::getCnfProof()->registerConvertedClause(id, true); - // no need to pop current assertion as this is not converted to cnf - ); + PROOF(ClauseId id = ProofManager::getSatProof()->registerClause( + real_reason, THEORY_LEMMA); + ProofManager::getCnfProof()->registerConvertedClause(id, true); + // explainPropagation() pushes the explanation on the assertion stack + // in CnfProof, so we need to pop it here. This is important because + // reason() may be called indirectly while adding a clause, which can + // lead to a wrong assertion being associated with the clause being + // added (see issue #2137). + ProofManager::getCnfProof()->popCurrentAssertion();); vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x)); clauses_removable.push(real_reason); attachClause(real_reason); @@ -1021,6 +1027,9 @@ void Solver::propagateTheory() { MinisatSatSolver::toMinisatClause(explanation_cl, explanation); ClauseId id; // FIXME: mark it as explanation here somehow? addClause(explanation, true, id); + // explainPropagation() pushes the explanation on the assertion + // stack in CnfProof, so we need to pop it here. + PROOF(ProofManager::getCnfProof()->popCurrentAssertion();) } } } |