From e3cd14dcc00eddef1238dce4e9c90be18858bb73 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 14 Jul 2021 20:02:30 -0300
Subject: [PATCH] [proof] Fix open proof issues in SAT proof (#6887)

Commit d1eee40cc (PR #6346), in a foolish attempt to prevent speculated issues, introduced an overwriting policy to addition of resolution chains during SAT solving at the SAT proof manager. First, this is nonsensical because the lazy proof chain is context-dependent and at the same level other ways of proving that clause are simply redundant and therefore should be ignored. Second, and catastrophically, this policy, for reasons beyond me, can lead to open SAT proofs when the same clause is rederived at the same level.

So this commit simply reverts the change and adds an optimization that when the clause would be rederived at the same level we do nothing and leave the method.
---
 src/prop/sat_proof_manager.cpp                  | 17 +++++++++++------
 test/regress/CMakeLists.txt                     |  2 ++
 .../regress0/proofs/open-pf-datatypes.smt2      | 11 +++++++++++
 .../regress0/proofs/open-pf-rederivation.smt2   |  6 ++++++
 4 files changed, 30 insertions(+), 6 deletions(-)
 create mode 100644 test/regress/regress0/proofs/open-pf-datatypes.smt2
 create mode 100644 test/regress/regress0/proofs/open-pf-rederivation.smt2

diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index 0f8ad8e69..ad23bedc9 100644
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -162,6 +162,16 @@ void SatProofManager::endResChain(Node conclusion,
                                   const std::set<SatLiteral>& conclusionLits)
 {
   Trace("sat-proof") << ", " << conclusion << "\n";
+  if (d_resChains.hasGenerator(conclusion))
+  {
+    Trace("sat-proof")
+        << "SatProofManager::endResChain: skip repeated proof of " << conclusion
+        << "\n";
+    // clearing
+    d_resLinks.clear();
+    d_redundantLits.clear();
+    return;
+  }
   // first process redundant literals
   std::set<SatLiteral> visited;
   unsigned pos = d_resLinks.size();
@@ -240,11 +250,6 @@ void SatProofManager::endResChain(Node conclusion,
       return;
     }
   }
-  if (Trace.isOn("sat-proof") && d_resChains.hasGenerator(conclusion))
-  {
-    Trace("sat-proof") << "SatProofManager::endResChain: replacing proof of "
-                       << conclusion << "\n";
-  }
   // since the conclusion can be both reordered and without duplicates and the
   // SAT solver does not record this information, we use a MACRO_RESOLUTION
   // step, which bypasses these. Note that we could generate a chain resolution
@@ -252,7 +257,7 @@ void SatProofManager::endResChain(Node conclusion,
   // post-processing.
   ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args);
   // note that we must tell the proof generator to overwrite if repeated
-  d_resChainPg.addStep(conclusion, ps, CDPOverwrite::ALWAYS);
+  d_resChainPg.addStep(conclusion, ps);
   // the premises of this resolution may not have been justified yet, so we do
   // not pass assumptions to check closedness
   d_resChains.addLazyStep(conclusion, &d_resChainPg);
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 205729553..db6a7ae48 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -829,7 +829,9 @@ set(regress_0_tests
   regress0/printer/tuples_and_records.cvc
   regress0/proofs/cyclic-ucp.smt2
   regress0/proofs/issue277-circuit-propagator.smt2
+  regress0/proofs/open-pf-datatypes.smt2
   regress0/proofs/open-pf-if-unordered-iff.smt2
+  regress0/proofs/open-pf-rederivation.smt2
   regress0/proofs/scope.smt2
   regress0/proofs/trust-subs-eq-open.smt2
   regress0/push-pop/boolean/fuzz_12.smt2
diff --git a/test/regress/regress0/proofs/open-pf-datatypes.smt2 b/test/regress/regress0/proofs/open-pf-datatypes.smt2
new file mode 100644
index 000000000..24d20bfd8
--- /dev/null
+++ b/test/regress/regress0/proofs/open-pf-datatypes.smt2
@@ -0,0 +1,11 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-datatypes ((C 0)) (((r) (b))))
+(declare-datatypes ((P 0)) (((a (f C) (s C)))))
+(declare-fun p () P)
+(declare-fun p2 () P)
+(declare-fun p3 () P)
+(declare-fun p4 () P)
+(declare-fun p5 () P)
+(assert (distinct p p2 p3 p4 p5))
+(check-sat)
diff --git a/test/regress/regress0/proofs/open-pf-rederivation.smt2 b/test/regress/regress0/proofs/open-pf-rederivation.smt2
new file mode 100644
index 000000000..7095ec942
--- /dev/null
+++ b/test/regress/regress0/proofs/open-pf-rederivation.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --bv-solver=simple
+; EXPECT: unsat
+(set-logic ALL)
+(declare-const __ (_ BitVec 7))
+(assert (bvule ((_ zero_extend 31) ((_ zero_extend 16) ((_ zero_extend 8) __))) ((_ zero_extend 30) ((_ zero_extend 1) ((_ zero_extend 16) ((_ zero_extend 8) __))))))
+(check-sat-assuming ((not (bvule (bvsub ((_ zero_extend 32) ((_ zero_extend 1) ((_ zero_extend 16) ((_ zero_extend 8) __)))) (_ bv1 64)) (bvsub ((_ zero_extend 1) ((_ zero_extend 1) ((_ zero_extend 31) ((_ zero_extend 16) ((_ zero_extend 8) __))))) (_ bv1 64))))))
-- 
2.30.2