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 | |
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')
-rw-r--r-- | src/proof/cnf_proof.cpp | 11 | ||||
-rw-r--r-- | src/prop/cnf_stream.cpp | 11 |
2 files changed, 20 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); } diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 6690f12db..aa5bb92d9 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -160,8 +160,19 @@ void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) { // If we were called with something other than a theory atom (or // Boolean variable), we get a SatLiteral that is definitionally // equal to it. + // + // We are setting the current assertion to be null. This is because `toCNF` + // may add clauses to the SAT solver and we look up the current assertion + // in that case. Setting it to null ensures that the assertion stack is + // non-empty and that we are not associating a bogus assertion with the + // clause. This should be ok because we use the mapping back to assertions + // for clauses from input assertions only. + PROOF(if (d_cnfProof) { d_cnfProof->pushCurrentAssertion(Node::null()); }); + lit = toCNF(n, false); + PROOF(if (d_cnfProof) { d_cnfProof->popCurrentAssertion(); }); + // Store backward-mappings // These may already exist d_literalToNodeMap.insert_safe(lit, n); |