From ca65101e2d56a476367c8ad09b416b66403be7a7 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 13 Jul 2018 13:24:43 -0700 Subject: [PATCH] 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. --- src/proof/cnf_proof.cpp | 12 +++- src/proof/cnf_proof.h | 5 ++ src/proof/proof_manager.cpp | 3 + src/proof/sat_proof_implementation.h | 3 + src/prop/minisat/core/Solver.cc | 59 +++++++++++-------- test/regress/Makefile.tests | 1 + .../regress0/push-pop/issue2137.min.smt2 | 11 ++++ 7 files changed, 67 insertions(+), 27 deletions(-) create mode 100644 test/regress/regress0/push-pop/issue2137.min.smt2 diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index d7672f1b4..016198735 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -161,10 +161,14 @@ void CnfProof::setCnfDependence(Node from, Node to) { } void CnfProof::pushCurrentAssertion(Node assertion) { - Debug("proof:cnf") << "CnfProof::pushCurrentAssertion " - << assertion << std::endl; + Debug("proof:cnf") << "CnfProof::pushCurrentAssertion " << assertion + << std::endl; d_currentAssertionStack.push_back(assertion); + + Debug("proof:cnf") << "CnfProof::pushCurrentAssertion " + << "new stack size = " << d_currentAssertionStack.size() + << std::endl; } void CnfProof::popCurrentAssertion() { @@ -174,6 +178,10 @@ void CnfProof::popCurrentAssertion() { << d_currentAssertionStack.back() << std::endl; d_currentAssertionStack.pop_back(); + + Debug("proof:cnf") << "CnfProof::popCurrentAssertion " + << "new stack size = " << d_currentAssertionStack.size() + << std::endl; } Node CnfProof::getCurrentAssertion() { diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index 99a347744..32833d9a1 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -127,6 +127,11 @@ public: void popCurrentDefinition(); Node getCurrentDefinition(); + /** + * Checks whether the assertion stack is empty. + */ + bool isAssertionStackEmpty() const { return d_currentAssertionStack.empty(); } + void setProofRecipe(LemmaProofRecipe* proofRecipe); LemmaProofRecipe getProofRecipe(const std::set &lemma); bool haveProofRecipe(const std::set &lemma); diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index d8ab811bc..f2205e2ed 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -332,6 +332,9 @@ void ProofManager::traceUnsatCore() { d_satProof->collectClausesUsed(used_inputs, used_lemmas); + // At this point, there should be no assertions without a clause id + Assert(d_cnfProof->isAssertionStackEmpty()); + IdToSatClause::const_iterator it = used_inputs.begin(); for(; it != used_inputs.end(); ++it) { Node node = d_cnfProof->getAssertionForClause(it->first); diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index 68050d93c..82e7cb7b2 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -565,6 +565,9 @@ ClauseId TSatProof::registerUnitClause(typename Solver::TLit lit, if (kind == INPUT) { Assert(d_inputClauses.find(newId) == d_inputClauses.end()); + Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new " + "input (UNIT CLAUSE): " + << lit << std::endl; d_inputClauses.insert(newId); } if (kind == THEORY_LEMMA) { 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 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 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();) } } } diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 3c02ea13c..377e91897 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -580,6 +580,7 @@ REG0_TESTS = \ regress0/push-pop/inc-double-u.smt2 \ regress0/push-pop/incremental-subst-bug.cvc \ regress0/push-pop/issue1986.smt2 \ + regress0/push-pop/issue2137.min.smt2 \ regress0/push-pop/quant-fun-proc-unfd.smt2 \ regress0/push-pop/simple_unsat_cores.smt2 \ regress0/push-pop/test.00.cvc \ diff --git a/test/regress/regress0/push-pop/issue2137.min.smt2 b/test/regress/regress0/push-pop/issue2137.min.smt2 new file mode 100644 index 000000000..372e8f1f3 --- /dev/null +++ b/test/regress/regress0/push-pop/issue2137.min.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --incremental --check-unsat-cores +; EXPECT: sat +; EXPECT: unsat +(set-logic ALL) +(declare-fun a () Real) +(declare-fun b () Bool) +(assert (< 0 a)) +(assert (xor b (< 0 a 0) false)) +(check-sat) +(assert (not b)) +(check-sat) -- 2.30.2