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

diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index 0f8ad8e694df4fcba085847822511b349428e005..ad23bedc9eeb87ecb3986ff0045f3ae33bbd079d 100644 (file)
--- 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 205729553f4437012732fe67474b25ab2fa04481..db6a7ae489bc9c181e0698ef7d7fc97de3bccad1 100644 (file)
--- 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 (file)
index 0000000..24d20bf
--- /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 (file)
index 0000000..7095ec9
--- /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))))))