From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Tue, 23 Feb 2021 17:31:38 +0000 (-0300)
Subject: [proof-new] Fix dangling pointer in SAT proof generation (#5963)
X-Git-Tag: cvc5-1.0.0~2235
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1e58294a927f8c3067ea0feaad0d891f82f42ebe;p=cvc5.git

[proof-new] Fix dangling pointer in SAT proof generation (#5963)

When a clause is being explained, the negation of each of its literals, other than the one it propagates, needs to be explained. This process may lead to the creation of new clauses in the SAT solver (because if a literal being explained was propagated and an explanation was not yet given, it will then be computed and added). This may lead to changes in the memory where clauses are, which may break the reference to the original clause being explained. To avoid this issue we store the literals in the reason before we start explaining their negations. We then iterate over them rather than over the clause, as before.
---

diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index 3def16b22..fb484429b 100644
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -331,9 +331,9 @@ void SatProofManager::processRedundantLit(
 void SatProofManager::explainLit(
     SatLiteral lit, std::unordered_set<TNode, TNodeHashFunction>& premises)
 {
+  Trace("sat-proof") << push << "SatProofManager::explainLit: Lit: " << lit;
   Node litNode = getClauseNode(lit);
-  Trace("sat-proof") << push << "SatProofManager::explainLit: Lit: " << lit
-                     << " [" << litNode << "]\n";
+  Trace("sat-proof") << " [" << litNode << "]\n";
   Minisat::Solver::TCRef reasonRef =
       d_solver->reason(Minisat::var(MinisatSatSolver::toMinisatLit(lit)));
   if (reasonRef == Minisat::Solver::TCRef_Undef)
@@ -352,6 +352,7 @@ void SatProofManager::explainLit(
     printClause(reason);
     Trace("sat-proof") << "\n";
   }
+#ifdef CVC4_ASSERTIONS
   // pedantically check that the negation of the literal to explain *does not*
   // occur in the reason, otherwise we will loop forever
   for (unsigned i = 0; i < size; ++i)
@@ -359,15 +360,26 @@ void SatProofManager::explainLit(
     AlwaysAssert(~MinisatSatSolver::toSatLiteral(reason[i]) != lit)
         << "cyclic justification\n";
   }
+#endif
   // add the reason clause first
   std::vector<Node> children{getClauseNode(reason)}, args;
   // save in the premises
   premises.insert(children.back());
+  // Since explainLit calls can reallocate memory in the
+  // SAT solver, we directly get the literals we need to explain so we no
+  // longer depend on the reference to reason
+  std::vector<Node> toExplain{children.back().begin(), children.back().end()};
   NodeManager* nm = NodeManager::currentNM();
   Trace("sat-proof") << push;
   for (unsigned i = 0; i < size; ++i)
   {
-    SatLiteral curr_lit = MinisatSatSolver::toSatLiteral(reason[i]);
+#ifdef CVC4_ASSERTIONS
+    // pedantically make sure that the reason stays the same
+    const Minisat::Clause& reloadedReason = d_solver->ca[reasonRef];
+    AlwaysAssert(size == static_cast<unsigned>(reloadedReason.size()));
+    AlwaysAssert(children[0] == getClauseNode(reloadedReason));
+#endif
+    SatLiteral curr_lit = d_cnfStream->getTranslationCache()[toExplain[i]];
     // ignore the lit we are trying to explain...
     if (curr_lit == lit)
     {