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).

diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index c8284762cb09c0e03814e1da78f72dda4b4b95e7..21636650dfa9b67c382f358d58c8bba4bd1cb4a6 100644 (file)
--- 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 6690f12dbae34c4bfad4a1e008be966c78f99313..aa5bb92d94e99e91e0833803736d7bfb9ab18eb7 100644 (file)
--- 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 62c9c87b1c19ddf78289e02ce92b083c8c05cfcb..15728ec1d019fd1b6c6226d1681641aa7a2040c6 100644 (file)
--- 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 (file)
index 0000000..6c557d9
--- /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)