diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-03-10 23:25:21 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-10 23:25:21 -0700 |
commit | edcc81b08b4d6c67da81b7ba2fcefbab3286f02c (patch) | |
tree | 2ed2aabf8763b96228d4629056a2d04208c8eab5 /src/proof | |
parent | ad2fc7c63e8f9d91ff0b750207fdae5fd029134b (diff) |
Set assertion in `CnfStream::ensureLiteral()` (#3927)
Fixes #3814. `CnfProof` has a stack of assertions that are being
converted to clauses. `CnfStream::ensureLiteral()` can result in clauses
being added to the SAT solver. When adding a clause, we require an
assertion that can be associated with the clause
(https://github.com/CVC4/CVC4/blob/ba6ade0fc3f4cd339885652bb9bf5c87113c498d/src/prop/minisat/core/Solver.cc#L471-L476).
However, in the issue that was reported, the stack was empty, resulting
in an assertion failure. This commit fixes the issue by setting the
current assertion to be the null node when a literal is being ensured
(and changing the proof code to update the assertion associated with a
literal if it is currently null). This should be ok since the clauses
are not inputs or lemmas (if they are, the assertion associated with the
clause will be updated).
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/cnf_proof.cpp | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index c8284762c..21636650d 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -69,7 +69,7 @@ ProofRule CnfProof::getProofRule(ClauseId clause) { Node CnfProof::getAssertionForClause(ClauseId clause) { ClauseIdToNode::const_iterator it = d_clauseToAssertion.find(clause); - Assert(it != d_clauseToAssertion.end()); + Assert(it != d_clauseToAssertion.end() && !(*it).second.isNull()); return (*it).second; } @@ -135,8 +135,15 @@ void CnfProof::setClauseAssertion(ClauseId clause, Node expr) { // case we keep the first assertion. For example asserting a /\ b // and then b /\ c where b is an atom, would assert b twice (note // that since b is top level, it is not cached by the CnfStream) - if (d_clauseToAssertion.find(clause) != d_clauseToAssertion.end()) + // + // Note: If the current assertion associated with the clause is null, we + // update it because it means that it was previously added the clause without + // associating it with an assertion. + const auto& it = d_clauseToAssertion.find(clause); + if (it != d_clauseToAssertion.end() && (*it).second != Node::null()) + { return; + } d_clauseToAssertion.insert (clause, expr); } |