From edcc81b08b4d6c67da81b7ba2fcefbab3286f02c Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 10 Mar 2020 23:25:21 -0700 Subject: [PATCH] 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). --- src/proof/cnf_proof.cpp | 11 +++++++++-- src/prop/cnf_stream.cpp | 11 +++++++++++ test/regress/CMakeLists.txt | 1 + test/regress/regress0/arrays/issue3814.smt2 | 12 ++++++++++++ 4 files changed, 33 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress0/arrays/issue3814.smt2 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); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 62c9c87b1..15728ec1d 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -76,6 +76,7 @@ set(regress_0_tests regress0/arrays/incorrect8.smtv1.smt2 regress0/arrays/incorrect9.smtv1.smt2 regress0/arrays/issue3813-massign-assert.smt2 + regress0/arrays/issue3814.smt2 regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smtv1.smt2 regress0/arrays/x2.smtv1.smt2 regress0/arrays/x3.smtv1.smt2 diff --git a/test/regress/regress0/arrays/issue3814.smt2 b/test/regress/regress0/arrays/issue3814.smt2 new file mode 100644 index 000000000..6c557d99d --- /dev/null +++ b/test/regress/regress0/arrays/issue3814.smt2 @@ -0,0 +1,12 @@ +; REQUIRES: proof +; COMMAND-LINE: --produce-unsat-cores +; EXPECT: sat +(set-logic QF_AX) +(declare-fun a () (Array Bool Bool)) +(declare-fun b () (Array Bool Bool)) +(declare-fun c () Bool) +(declare-fun d () Bool) +(declare-fun e () Bool) +(assert (= a (store b c d))) +(assert (= e (select a (select b d)))) +(check-sat) -- 2.30.2