From 2044c5b87f2b7fde24c3a57a626e903663f34e15 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Thu, 24 Mar 2022 12:32:42 -0300 Subject: [PATCH] [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 --- src/prop/proof_cnf_stream.cpp | 8 +++++++- src/prop/prop_engine.cpp | 12 +++++++++++- src/prop/prop_engine.h | 3 +++ test/regress/cli/CMakeLists.txt | 15 ++++++++------- .../regress0/proofs/proj-issue468-mkScope.smt2 | 10 ++++++++++ 5 files changed, 39 insertions(+), 9 deletions(-) create mode 100644 test/regress/cli/regress0/proofs/proj-issue468-mkScope.smt2 diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp index 34442b143..11d669a18 100644 --- 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>& 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 b2c777e88..678ef2107 100644 --- 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 f852a39c6..34bce5671 100644 --- 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 d_pfCnfStream; + /** A default proof generator for theory lemmas */ + CDProof d_theoryLemmaPg; /** The proof manager for prop engine */ std::unique_ptr d_ppm; diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 67bcd6bca..c428eda3a 100644 --- 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 index 000000000..acd4aad85 --- /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 -- 2.30.2