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/proof | |
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/proof')
-rw-r--r-- | src/proof/cnf_proof.cpp | 12 | ||||
-rw-r--r-- | src/proof/cnf_proof.h | 5 | ||||
-rw-r--r-- | src/proof/proof_manager.cpp | 3 | ||||
-rw-r--r-- | src/proof/sat_proof_implementation.h | 3 |
4 files changed, 21 insertions, 2 deletions
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<Node> &lemma); bool haveProofRecipe(const std::set<Node> &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<Solver>::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) { |