From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 1 Sep 2021 18:31:56 +0000 (-0300)
Subject: [proof] [sat] Fix lost reference to reason when processing redundant literals (#7108)
X-Git-Tag: cvc5-1.0.0~1303
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=59e73be8a11f5490e0c8cfc4a5e2ab7ed07b352f;p=cvc5.git

[proof] [sat] Fix lost reference to reason when processing redundant literals (#7108)

Similarly to the issue when explaining literals, it's necassary to save the
reference to the reason for propagating a redundant literal, as adding
explanations that may be added to the SAT solver during the recursive
elimination of redundant literals may change the original reference.
---

diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index ad23bedc9..8891016a4 100644
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -305,11 +305,19 @@ void SatProofManager::processRedundantLit(
     printClause(reason);
     Trace("sat-proof") << "\n";
   }
-  // check if redundant literals in the reason. The first literal is the one we
-  // will be eliminating, so we check the others
+  // Since processRedundantLit calls can reallocate memory in the SAT solver due
+  // to explaining stuff, we directly get the literals and the clause node here
+  std::vector<SatLiteral> toProcess;
   for (unsigned i = 1, size = reason.size(); i < size; ++i)
   {
-    SatLiteral satLit = MinisatSatSolver::toSatLiteral(reason[i]);
+    toProcess.push_back(MinisatSatSolver::toSatLiteral(reason[i]));
+  }
+  Node clauseNode = getClauseNode(reason);
+    // check if redundant literals in the reason. The first literal is the one we
+  // will be eliminating, so we check the others
+  for (unsigned i = 0, size = toProcess.size(); i < size; ++i)
+  {
+    SatLiteral satLit = toProcess[i];
     // if literal does not occur in the conclusion we process it as well
     if (!conclusionLits.count(satLit))
     {
@@ -325,7 +333,6 @@ void SatProofManager::processRedundantLit(
   // reason, not only with ~lit, since the learned clause is built under the
   // assumption that the redundant literal is removed via the resolution with
   // the explanation of its negation
-  Node clauseNode = getClauseNode(reason);
   Node litNode = d_cnfStream->getNodeCache()[lit];
   bool negated = lit.isNegated();
   Assert(!negated || litNode.getKind() == kind::NOT);
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 17585d363..d1208ad0f 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2110,7 +2110,7 @@ set(regress_1_tests
   regress1/strings/bug686dd.smt2
   regress1/strings/bug768.smt2
   regress1/strings/bug799-min.smt2
-  regress1/strings/cee-norn-aes-trivially.smt2 
+  regress1/strings/cee-norn-aes-trivially.smt2
   regress1/strings/chapman150408.smt2
   regress1/strings/cmu-2db2-extf-reg.smt2
   regress1/strings/cmu-5042-0707-2.smt2
@@ -2509,6 +2509,7 @@ set(regress_2_tests
   regress2/ooo.rf6.smt2
   regress2/ooo.tag10.smt2
   regress2/piVC_5581bd.smt2
+  regress2/proofs/sat-proof-reloaded-reason.smt2
   regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2
   regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2
   regress2/quantifiers/cee-event-wrong-sat.smt2
diff --git a/test/regress/regress2/proofs/sat-proof-reloaded-reason.smt2 b/test/regress/regress2/proofs/sat-proof-reloaded-reason.smt2
new file mode 100644
index 000000000..8bc990b8b
--- /dev/null
+++ b/test/regress/regress2/proofs/sat-proof-reloaded-reason.smt2
@@ -0,0 +1,31 @@
+; COMMAND-LINE: --produce-proofs
+; EXPECT: sat
+;
+; This is a benchmark exercising a dangerous behavior in SAT proofs
+; where while eliminating redundant literals new clauses are added to
+; the SAT solver and the reference to the reason of a literal could be
+; lost.
+
+(set-logic QF_SLIA)
+(declare-const x Int)
+(declare-const x2 Int)
+(declare-const x22 Int)
+(declare-const x1 Int)
+(declare-fun s () String)
+(assert (not (= "0" (str.substr s (+ 1 1 1 1) 1))))
+(assert (not (= 1 (str.len (str.substr s (+ 1 1 1 1) (+ 1 1))))))
+(assert (ite (str.prefixof "-" (str.substr s (+ 1 1 1 1 1) (- (str.len s) (+ 1 1 1 1 1)))) (and (> (str.len (str.substr s (+ 1 1 1) (str.len s))) 1) (ite (= (- 1) (str.to_int (str.substr (str.substr s (+ 1 1 1 1 1) (- (str.len s) 1)) 1 1))) false true)) (= 1 (str.to_int (str.substr s x22 1)))))
+(assert (ite (str.prefixof "-" (str.substr s (+ 1 1) 1)) (ite (= (- 1) (str.to_int (str.substr (str.substr s (+ 1 1) (+ 1 1)) 1 (- (str.len (str.substr s 0 (+ 1 1))) 1)))) false true) (= 0 (str.to_int (str.substr s (+ 1 1) (+ 1 1))))))
+(assert (<= (ite (str.prefixof "-" (str.substr s 0 1)) (str.to_int (str.substr (str.substr s (+ 1 1 1) (+ 1 1 1)) 1 (- (str.len (str.substr s (+ 1 1 1) (+ 1 1 1))) 1))) (str.to_int (str.substr s 0 x2))) 0))
+(assert (ite (str.prefixof "-" (str.substr s 0 1)) (and (> (str.len (str.substr s 0 (+ 1 1))) 1) (= 0 (str.to_int (str.substr (str.substr s 0 (+ 1 1)) 1 (- (str.len (str.substr s 0 (+ 1 1))) 1))))) true))
+(assert (not (= 1 (str.len (str.substr s (+ 1 1 1 1 1) (- (str.len s) (+ 1 1 1 1 1)))))))
+(assert (ite (str.prefixof "-" (str.substr s (+ 1 1 1 1) (- (str.len s) (+ 1 1 1 1)))) true (= 1 (str.to_int (str.substr s (+ 1 1 1 1) 1)))))
+(assert (= 1 (str.len (str.substr s (+ 1 1 1) 1))))
+(assert (not (= 1 (str.len (str.substr s 1 (+ 1 1 1))))))
+(assert (> (- (str.len s) 1 (+ 1 1) (+ 1 1)) 0))
+(assert (= "0" (str.substr s 1 1)))
+(assert (not (<= (str.to_int (str.substr s x x1)) 0)))
+(assert (not (= 1 (str.len (str.substr s (+ 1 1) (- (+ 1 1 1) 1))))))
+(assert (str.in_re s (re.+ (re.range "0" "9"))))
+(assert (not (<= (ite (str.prefixof "-" (str.substr s (+ 1 1 1 1) 1)) (- (str.to_int (str.substr (str.substr s (+ 1 1 1 1) (+ 1 1)) 1 (- (str.len (str.substr s (+ 1 1) (+ 1 1))) 1)))) (str.to_int (str.substr s (+ 1 1 1 1) (+ 1 1)))) 1)))
+(check-sat)