From: Andrew Reynolds Date: Wed, 16 Mar 2022 00:41:06 +0000 (-0500) Subject: Ensure trusted steps are given for skolem lemmas when proofs are enabled (#8302) X-Git-Tag: cvc5-1.0.0~246 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1c382bb55e11c383285e188db6fa30a51af8b556;p=cvc5.git Ensure trusted steps are given for skolem lemmas when proofs are enabled (#8302) Fixes cvc5/cvc5-projects#492. --- diff --git a/src/preprocessing/passes/theory_rewrite_eq.cpp b/src/preprocessing/passes/theory_rewrite_eq.cpp index 782d4569d..9ca1c82ce 100644 --- a/src/preprocessing/passes/theory_rewrite_eq.cpp +++ b/src/preprocessing/passes/theory_rewrite_eq.cpp @@ -107,7 +107,9 @@ TrustNode TheoryRewriteEq::rewriteAssertion(TNode n) if (ret.getKind() == kind::EQUAL && !ret[0].getType().isBoolean()) { // For example, (= x y) ---> (and (>= x y) (<= x y)) - TrustNode trn = te->ppRewriteEquality(ret); + std::vector lems; + TrustNode trn = te->ppRewrite(ret, lems); + Assert(lems.empty()); // can make proof producing by using proof generator from trn if (!trn.isNull() && trn.getNode() != ret) { diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index 5028cba1b..76f8f54d6 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -225,6 +225,22 @@ enum class PfRule : uint32_t // the quantifiers rewriter involves constructing new bound variables that are // not guaranteed to be consistent on each call. THEORY_REWRITE, + // ======== Theory Preprocess + // Children: none + // Arguments: (F, tid) + // ---------------------------------------- + // Conclusion: F + // where F is an equality of the form t = Theory::ppRewrite(t) for the theory + // with identifier tid. Notice this is a "trusted" rule. + THEORY_PREPROCESS, + // ======== Theory Preprocess + // Children: none + // Arguments: (F, tid) + // ---------------------------------------- + // Conclusion: F + // where F was added as a new assertion by theory preprocessing from the + // theory with identifier tid. + THEORY_PREPROCESS_LEMMA, // The remaining rules in this section have the signature of a "trusted rule": // // Children: ? @@ -240,11 +256,6 @@ enum class PfRule : uint32_t PREPROCESS, // where F was added as a new assertion by some preprocessing pass. PREPROCESS_LEMMA, - // where F is an equality of the form t = Theory::ppRewrite(t) for some - // theory. Notice this is a "trusted" rule. - THEORY_PREPROCESS, - // where F was added as a new assertion by theory preprocessing. - THEORY_PREPROCESS_LEMMA, // where F is an equality of the form t = t' where t was replaced by t' // based on theory expand definitions. THEORY_EXPAND_DEF, diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 067dc8b0c..cc705109e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -743,13 +743,36 @@ theory::Theory::PPAssertStatus TheoryEngine::solve( return solveStatus; } -TrustNode TheoryEngine::ppRewriteEquality(TNode eq) +TrustNode TheoryEngine::ppRewrite(TNode term, + std::vector& lems) { - Assert(eq.getKind() == kind::EQUAL); - std::vector lems; - TrustNode trn = theoryOf(eq)->ppRewrite(eq, lems); - // should never introduce a skolem to eliminate an equality Assert(lems.empty()); + TheoryId tid = d_env.theoryOf(term); + TrustNode trn = d_theoryTable[tid]->ppRewrite(term, lems); + // should never introduce a skolem to eliminate an equality + Assert(lems.empty() || term.getKind() != kind::EQUAL); + if (!isProofEnabled()) + { + return trn; + } + Assert(d_lazyProof != nullptr); + // if proofs are enabled, must ensure we have proofs for all the skolem lemmas + for (SkolemLemma& skl : lems) + { + TrustNode tskl = skl.d_lemma; + Assert(tskl.getKind() == TrustNodeKind::LEMMA); + if (tskl.getGenerator() == nullptr) + { + Node proven = tskl.getProven(); + Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(tid); + d_lazyProof->addStep( + proven, PfRule::THEORY_PREPROCESS_LEMMA, {}, {proven, tidn}); + skl.d_lemma = TrustNode::mkTrustLemma(proven, d_lazyProof.get()); + } + } + // notice that we don't ensure proofs are processed for the returned (rewrite) + // trust node, this is the responsibility of the caller, i.e. theory + // preprocessor. return trn; } @@ -1798,7 +1821,10 @@ TrustNode TheoryEngine::getExplanation( return TrustNode::mkTrustPropExp(conclusion, expNode, nullptr); } -bool TheoryEngine::isProofEnabled() const { return d_pnm != nullptr; } +bool TheoryEngine::isProofEnabled() const +{ + return d_env.isTheoryProofProducing(); +} void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) { bool hasFailure = false; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index c107ef1a9..75defade5 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -171,10 +171,15 @@ class TheoryEngine : protected EnvObj } /** - * Preprocess rewrite equality, called by the preprocessor to rewrite - * equalities appearing in the input. + * Preprocess rewrite, called: + * (1) on equalities by the preprocessor to rewrite equalities appearing in + * the input, + * (2) on non-equalities by the theory preprocessor. + * + * Calls the ppRewrite of the theory of term and adds the associated skolem + * lemmas to lems, for details see Theory::ppRewrite. */ - TrustNode ppRewriteEquality(TNode eq); + TrustNode ppRewrite(TNode term, std::vector& lems); /** Notify (preprocessed) assertions. */ void notifyPreprocessedAssertions(const std::vector& assertions); diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index e92722a2a..26f9e759f 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -440,9 +440,11 @@ Node TheoryPreprocessor::preprocessWithProof(Node term, return term; } // call ppRewrite for the given theory - TrustNode trn = d_engine.theoryOf(term)->ppRewrite(term, lems); + std::vector newLems; + TrustNode trn = d_engine.ppRewrite(term, newLems); Trace("tpp-debug2") << "preprocessWithProof returned " << trn - << ", #lems = " << lems.size() << std::endl; + << ", #lems = " << newLems.size() << std::endl; + lems.insert(lems.end(), newLems.begin(), newLems.end()); if (trn.isNull()) { // no change, return diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5a1d8f832..32604095f 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -950,6 +950,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-issue492-skolem-lemma-pf.smt2 regress0/proofs/qgu-fuzz-1-bool-sat.smt2 regress0/proofs/qgu-fuzz-2-bool-chainres-checking.smt2 regress0/proofs/qgu-fuzz-3-chainres-checking.smt2 diff --git a/test/regress/regress0/proofs/proj-issue492-skolem-lemma-pf.smt2 b/test/regress/regress0/proofs/proj-issue492-skolem-lemma-pf.smt2 new file mode 100644 index 000000000..b21a447c7 --- /dev/null +++ b/test/regress/regress0/proofs/proj-issue492-skolem-lemma-pf.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(set-info :status sat) +(set-option :produce-proofs true) +(assert (exists ((x (Set (_ BitVec 16)))) (set.member (set.choose (set.inter x x)) (set.inter x x)))) +(check-sat)