[unsat-cores] [sat-proof] Fix open proofs due to theory lemmas (#8371)

Previously when producing sat proofs for unsat cores (no theory proofs) theory lemmas were becoming open leafs in the final proof, breaking the invariant that only inputs should be so. This commit guards against this by justifying these lemmas with a THEORY_LEMMA step.

Fixes cvc5/cvc5-projects#468

diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp
index 34442b143f32dab4a1875a981acd80f84931f8de..11d669a1839a64c581fab6e4dbfaeb48013ad878 100644 (file)
--- a/src/prop/proof_cnf_stream.cpp
+++ b/src/prop/proof_cnf_stream.cpp
@@ -594,7 +594,9 @@ void ProofCnfStream::convertPropagation(TrustNode trn)
     clauseExp = nm->mkNode(kind::OR, proven[0].notNode(), proven[1]);
   }
   normalizeAndRegister(clauseExp);
-  // consume steps
+  // consume steps if clausification being recorded. If we are not logging it,
+  // we need to add the clause as a closed step to the proof so that the SAT
+  // proof does not have non-input formulas as assumptions.
   if (proofLogging)
   {
     const std::vector<std::pair<Node, ProofStep>>& steps = d_psb.getSteps();
@@ -604,6 +606,10 @@ void ProofCnfStream::convertPropagation(TrustNode trn)
     }
     d_psb.clear();
   }
+  else
+  {
+    d_proof.addStep(clauseExp, PfRule::THEORY_LEMMA, {}, {clauseExp});
+  }
 }
 
 

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index b2c777e88ee048270fd5b2207497a6fe27e04344..678ef2107806868235e1ea5704458e7546312b08 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -73,6 +73,7 @@ PropEngine::PropEngine(Env& env, TheoryEngine* te)
       d_satSolver(nullptr),
       d_cnfStream(nullptr),
       d_pfCnfStream(nullptr),
+      d_theoryLemmaPg(d_env.getProofNodeManager(), d_env.getUserContext()),
       d_ppm(nullptr),
       d_interrupted(false),
       d_assumptions(d_env.getUserContext())
@@ -220,7 +221,16 @@ void PropEngine::assertTrustedLemmaInternal(TrustNode trn, bool removable)
   bool negated = trn.getKind() == TrustNodeKind::CONFLICT;
   // should have a proof generator if the theory engine is proof producing
   Assert(!d_env.isTheoryProofProducing() || trn.getGenerator() != nullptr);
-  assertInternal(trn.getNode(), negated, removable, false, trn.getGenerator());
+  // if we are producing proofs for the SAT solver but not for theory engine,
+  // then we need to prevent the lemma of being added as an assumption (since
+  // the generator will be null). We use the default proof generator for lemmas.
+  if (isProofEnabled() && !d_env.isTheoryProofProducing()
+      && !trn.getGenerator())
+  {
+    d_theoryLemmaPg.addStep(node, PfRule::THEORY_LEMMA, {}, {node});
+    trn = TrustNode::mkReplaceGenTrustNode(trn, &d_theoryLemmaPg);
+  }
+  assertInternal(node, negated, removable, false, trn.getGenerator());
 }
 
 void PropEngine::assertInternal(

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index f852a39c63051cd1485a0c95d68df88055b05108..34bce5671a1b10e328f6c32d921f0a157f1413b1 100644 (file)
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -22,6 +22,7 @@
 
 #include "context/cdlist.h"
 #include "expr/node.h"
+#include "proof/proof.h"
 #include "proof/trust_node.h"
 #include "prop/skolem_def_manager.h"
 #include "smt/env_obj.h"
@@ -361,6 +362,8 @@ class PropEngine : protected EnvObj
   CnfStream* d_cnfStream;
   /** Proof-producing CNF converter */
   std::unique_ptr<ProofCnfStream> d_pfCnfStream;
+  /** A default proof generator for theory lemmas */
+  CDProof d_theoryLemmaPg;
 
   /** The proof manager for prop engine */
   std::unique_ptr<PropPfManager> d_ppm;

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 67bcd6bcaafc476fcb70006f4ee0297a4a07d329..c428eda3ac6e51d9a2ad6b41f3c77f74cd96b30e 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -535,7 +535,7 @@ set(regress_0_tests
   regress0/datatypes/mutually-recursive.cvc.smt2
   regress0/datatypes/pair-bool-bool.cvc.smt2
   regress0/datatypes/pair-real-bool.smt2
-  regress0/datatypes/par-updater-type-rule.smt2 
+  regress0/datatypes/par-updater-type-rule.smt2
   regress0/datatypes/parametric-alt-list.cvc.smt2
   regress0/datatypes/proj-issue172.smt2
   regress0/datatypes/proj-issue474-app-cons-value.smt2
@@ -951,6 +951,7 @@ set(regress_0_tests
   regress0/proofs/proj-issue342-eager-checking-no-proof-checking.smt2
   regress0/proofs/proj-issue430-coverings-double-negation.smt2
   regress0/proofs/proj-issue462-sat-proof-option.smt2
+  regress0/proofs/proj-issue468-mkScope.smt2
   regress0/proofs/proj-issue492-skolem-lemma-pf.smt2
   regress0/proofs/qgu-fuzz-1-bool-sat.smt2
   regress0/proofs/qgu-fuzz-2-bool-chainres-checking.smt2
@@ -1243,7 +1244,7 @@ set(regress_0_tests
   regress0/sets/issue5400-card-minus-univ.smt2
   regress0/sets/issue5400-2-card-minus-univ.smt2
   regress0/sets/issue5402-1-card.smt2
-  regress0/sets/issue5402-2-card-finite.smt2 
+  regress0/sets/issue5402-2-card-finite.smt2
   regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2
   regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2
   regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2
@@ -1973,7 +1974,7 @@ set(regress_1_tests
   regress1/nl/issue5662-nl-tc-min.smt2
   regress1/nl/issue7924-sqrt-partial.smt2
   regress1/nl/issue7948-3-unsound-sin-region.smt2
-  regress1/nl/issue8016-iand-rewrite.smt2 
+  regress1/nl/issue8016-iand-rewrite.smt2
   regress1/nl/issue8052-iand-rewrite.smt2
   regress1/nl/issue8118-elim-sin.smt2
   regress1/nl/issue8162-drop-pi-bound.smt2
@@ -2181,8 +2182,8 @@ set(regress_1_tests
   regress1/quantifiers/issue5279-nqe.smt2
   regress1/quantifiers/issue5288-vts-real-int.smt2
   regress1/quantifiers/issue5365-nqe.smt2
-  regress1/quantifiers/issue5373-1-qe-inc.smt2 
-  regress1/quantifiers/issue5373-2.smt2 
+  regress1/quantifiers/issue5373-1-qe-inc.smt2
+  regress1/quantifiers/issue5373-2.smt2
   regress1/quantifiers/issue5378-witness.smt2
   regress1/quantifiers/issue5469-aext.smt2
   regress1/quantifiers/issue5470-aext.smt2
@@ -2530,7 +2531,7 @@ set(regress_1_tests
   regress1/strings/issue6777-seq-nth-eval-cm.smt2
   regress1/strings/issue6913.smt2
   regress1/strings/issue6973-dup-lemma-conc.smt2
-  regress1/strings/issue7677-test-const-rv.smt2 
+  regress1/strings/issue7677-test-const-rv.smt2
   regress1/strings/issue7918-learned-rewrite.smt2
   regress1/strings/issue8094-witness-model.smt2
   regress1/strings/kaluza-fl.smt2
@@ -2669,7 +2670,7 @@ set(regress_1_tests
   regress1/sygus/inv-missed-sol-true.sy
   regress1/sygus/inv-unused.sy
   regress1/sygus/interpol1.smt2
-  regress1/sygus/interpol1-push-pop.smt2 
+  regress1/sygus/interpol1-push-pop.smt2
   regress1/sygus/interpol3.smt2
   regress1/sygus/interpol3-next.smt2
   regress1/sygus/interpol_arr1.smt2

diff --git a/test/regress/cli/regress0/proofs/proj-issue468-mkScope.smt2 b/test/regress/cli/regress0/proofs/proj-issue468-mkScope.smt2
new file mode 100644 (file)
index 0000000..acd4aad
--- /dev/null
+++ b/test/regress/cli/regress0/proofs/proj-issue468-mkScope.smt2
@@ -0,0 +1,10 @@
+; EXPECT: unsat
+; EXPECT: (
+; EXPECT: a0
+; EXPECT: )
+(set-logic QF_BV)
+(declare-const __ (_ BitVec 1))
+(set-option :unsat-cores-mode sat-proof)
+(assert (! (bvsgt __ __) :named a0))
+(check-sat)
+(get-unsat-core)
\ No newline at end of file