[proofs] Fix open proof in SAT solver due to cycles (#7448)

diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index da49a5990c4fad2283d335d1b543bd662c7d3ef2..e650473b3f1874b9e0bf98acc53b92a39d630276 100644 (file)
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -348,6 +348,19 @@ void SatProofManager::explainLit(SatLiteral lit,
   Trace("sat-proof") << push << "SatProofManager::explainLit: Lit: " << lit;
   Node litNode = getClauseNode(lit);
   Trace("sat-proof") << " [" << litNode << "]\n";
+  // We don't need to explain nodes who are inputs. Note that it's *necessary*
+  // to avoid attempting such explanations because they can introduce cycles at
+  // the node level. For example, if a literal l depends on an input clause C
+  // but a literal l', node-equivalent to C, depends on l, we may have a cycle
+  // when building the overall SAT proof.
+  if (d_assumptions.contains(litNode))
+  {
+    Trace("sat-proof")
+        << "SatProofManager::explainLit: input assumption, ABORT\n";
+    return;
+  }
+  // We don't need to explain nodes who already have proofs.
+  //
   // Note that if we had two literals for (= a b) and (= b a) and we had already
   // a proof for (= a b) this test would return true for (= b a), which could
   // lead to open proof. However we should never have two literals like this in
@@ -626,7 +639,7 @@ void SatProofManager::finalizeProof(Node inConflictNode,
         if (it != d_cnfStream->getTranslationCache().end())
         {
           Trace("sat-proof") << it->second << "\n";
-          Trace("sat-proof") << "- " << fa << "\n";
+          Trace("sat-proof") << "  - " << fa << "\n";
           continue;
         }
         // then it's a clause
@@ -638,7 +651,7 @@ void SatProofManager::finalizeProof(Node inConflictNode,
           Trace("sat-proof") << it->second << " ";
         }
         Trace("sat-proof") << "\n";
-        Trace("sat-proof") << "- " << fa << "\n";
+        Trace("sat-proof") << "  - " << fa << "\n";
       }
     }
 
@@ -653,7 +666,7 @@ void SatProofManager::finalizeProof(Node inConflictNode,
       }
       // ignore input assumptions. This is necessary to avoid rare collisions
       // between input clauses and literals that are equivalent at the node
-      // level. In trying to justify the literal below if, it was previously
+      // level. In trying to justify the literal below, if it was previously
       // propagated (say, in a previous check-sat call that survived the
       // user-context changes) but no longer holds, then we may introduce a
       // bogus proof for it, rather than keeping it as an input.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 8ef4ed362900d322d96c62279011c288578254f9..fe7c3fdaf2339122b0b8f31d5b17c363d07455d5 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -852,6 +852,7 @@ set(regress_0_tests
   regress0/proofs/open-pf-datatypes.smt2
   regress0/proofs/open-pf-if-unordered-iff.smt2
   regress0/proofs/open-pf-rederivation.smt2
+  regress0/proofs/qgu-fuzz-1-bool-sat.smt2
   regress0/proofs/scope.smt2
   regress0/proofs/trust-subs-eq-open.smt2
   regress0/push-pop/boolean/fuzz_12.smt2
@@ -926,7 +927,7 @@ set(regress_0_tests
   regress0/quantifiers/issue4576.smt2
   regress0/quantifiers/issue5645-dt-cm-spurious.smt2
   regress0/quantifiers/issue5693-prenex.smt2
-  regress0/quantifiers/issue6475-rr-const.smt2 
+  regress0/quantifiers/issue6475-rr-const.smt2
   regress0/quantifiers/issue6603-dt-bool-cegqi.smt2
   regress0/quantifiers/issue6838-qpdt.smt2
   regress0/quantifiers/issue6996-trivial-elim.smt2
@@ -1727,7 +1728,7 @@ set(regress_1_tests
   regress1/nl/issue3656.smt2
   regress1/nl/issue3803-nl-check-model.smt2
   regress1/nl/issue3955-ee-double-notify.smt2
-  regress1/nl/issue3966-conf-coeff.smt2 
+  regress1/nl/issue3966-conf-coeff.smt2
   regress1/nl/issue4791-llr.smt2
   regress1/nl/issue5372-2-no-m-presolve.smt2
   regress1/nl/issue5660-mb-success.smt2
@@ -1927,7 +1928,7 @@ set(regress_1_tests
   regress1/quantifiers/issue5735-2-subtypes.smt2
   regress1/quantifiers/issue5766-wrong-sel-trigger.smt2
   regress1/quantifiers/issue5899-qe.smt2
-  regress1/quantifiers/issue6607-witness-te.smt2 
+  regress1/quantifiers/issue6607-witness-te.smt2
   regress1/quantifiers/issue6638-sygus-inst.smt2
   regress1/quantifiers/issue6642-em-types.smt2
   regress1/quantifiers/issue6699-nc-shadow.smt2
@@ -2236,7 +2237,7 @@ set(regress_1_tests
   regress1/strings/issue6653-rre-small.smt2
   regress1/strings/issue6777-seq-nth-eval-cm.smt2
   regress1/strings/issue6913.smt2
-  regress1/strings/issue6973-dup-lemma-conc.smt2 
+  regress1/strings/issue6973-dup-lemma-conc.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2

diff --git a/test/regress/regress0/proofs/qgu-fuzz-1-bool-sat.smt2 b/test/regress/regress0/proofs/qgu-fuzz-1-bool-sat.smt2
new file mode 100644 (file)
index 0000000..d9b10e2
--- /dev/null
+++ b/test/regress/regress0/proofs/qgu-fuzz-1-bool-sat.smt2
@@ -0,0 +1,7 @@
+; EXPECT: unsat
+(set-logic QF_UF)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(declare-fun d () Bool)
+(assert (and (or d b) (= c d) (not (ite d c false)) (= (or b d) (= b d))))
+(check-sat)
\ No newline at end of file