From: Andrew Reynolds Date: Wed, 14 Oct 2020 00:10:19 +0000 (-0500) Subject: (proof-new) Miscellaneous minor improvements and fixes to proofs in theory files... X-Git-Tag: cvc5-1.0.0~2718 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0fdf29ba194b8f6763ae41bea05b3208345d89b9;p=cvc5.git (proof-new) Miscellaneous minor improvements and fixes to proofs in theory files. (#5241) --- diff --git a/src/theory/eager_proof_generator.cpp b/src/theory/eager_proof_generator.cpp index bc101595f..c49c33790 100644 --- a/src/theory/eager_proof_generator.cpp +++ b/src/theory/eager_proof_generator.cpp @@ -30,7 +30,10 @@ EagerProofGenerator::EagerProofGenerator(ProofNodeManager* pnm, void EagerProofGenerator::setProofFor(Node f, std::shared_ptr pf) { // pf should prove f - Assert(pf->getResult() == f); + Assert(pf->getResult() == f) + << "EagerProofGenerator::setProofFor: unexpected result" << std::endl + << "Expected: " << f << std::endl + << "Actual: " << pf->getResult() << std::endl; d_proofs[f] = pf; } void EagerProofGenerator::setProofForConflict(Node conf, diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h index 48ae21347..4e350dca9 100644 --- a/src/theory/rewriter_tables_template.h +++ b/src/theory/rewriter_tables_template.h @@ -61,7 +61,7 @@ ${post_rewrite_set_cache} } } -Rewriter::Rewriter() +Rewriter::Rewriter() : d_tpg(nullptr) { for (size_t i = 0; i < kind::LAST_KIND; ++i) { diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 757f94d5b..681f3bca1 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -65,7 +65,6 @@ Theory::Theory(TheoryId id, d_satContext(satContext), d_userContext(userContext), d_logicInfo(logicInfo), - d_pnm(pnm), d_facts(satContext), d_factsHead(satContext, 0), d_sharedTermsIndex(satContext, 0), @@ -82,7 +81,8 @@ Theory::Theory(TheoryId id, d_equalityEngine(nullptr), d_allocEqualityEngine(nullptr), d_theoryState(nullptr), - d_inferManager(nullptr) + d_inferManager(nullptr), + d_pnm(pnm) { smtStatisticsRegistry()->registerStat(&d_checkTime); smtStatisticsRegistry()->registerStat(&d_computeCareGraphTime); @@ -388,13 +388,13 @@ Theory::PPAssertStatus Theory::ppAssert(TrustNode tin, if (in[0].isVar() && isLegalElimination(in[0], in[1]) && in[0].getKind() != kind::BOOLEAN_TERM_VARIABLE) { - outSubstitutions.addSubstitution(in[0], in[1]); + outSubstitutions.addSubstitutionSolved(in[0], in[1], tin); return PP_ASSERT_STATUS_SOLVED; } if (in[1].isVar() && isLegalElimination(in[1], in[0]) && in[1].getKind() != kind::BOOLEAN_TERM_VARIABLE) { - outSubstitutions.addSubstitution(in[1], in[0]); + outSubstitutions.addSubstitutionSolved(in[1], in[0], tin); return PP_ASSERT_STATUS_SOLVED; } if (in[0].isConst() && in[1].isConst()) diff --git a/src/theory/theory.h b/src/theory/theory.h index 86dbb60d6..9519624b7 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -123,9 +123,6 @@ class Theory { /** Information about the logic we're operating within. */ const LogicInfo& d_logicInfo; - /** Pointer to proof node manager */ - ProofNodeManager* d_pnm; - /** * The assertFact() queue. * @@ -237,6 +234,9 @@ class Theory { */ TheoryInferenceManager* d_inferManager; + /** Pointer to proof node manager */ + ProofNodeManager* d_pnm; + /** * Returns the next assertion in the assertFact() queue. * diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index 80b824ca0..e7cdb8f2c 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -57,8 +57,6 @@ TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine, { if (isProofEnabled()) { - // enable proofs in the term formula remover - d_tfr.setProofNodeManager(pnm); // push the proof context, since proof steps may be cleared on calls to // clearCache() below. d_pfContext.push(); diff --git a/src/theory/theory_proof_step_buffer.cpp b/src/theory/theory_proof_step_buffer.cpp index aa7e10370..5aa909a37 100644 --- a/src/theory/theory_proof_step_buffer.cpp +++ b/src/theory/theory_proof_step_buffer.cpp @@ -26,6 +26,33 @@ TheoryProofStepBuffer::TheoryProofStepBuffer(ProofChecker* pc) { } +bool TheoryProofStepBuffer::applyEqIntro(Node src, + Node tgt, + const std::vector& exp, + MethodId ids, + MethodId idr) +{ + std::vector args; + args.push_back(src); + builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, idr); + Node res = tryStep(PfRule::MACRO_SR_EQ_INTRO, exp, args); + if (res.isNull()) + { + // failed to apply + return false; + } + // should have concluded the expected equality + Node expected = src.eqNode(tgt); + if (res != expected) + { + // did not provide the correct target + popStep(); + return false; + } + // successfully proved src == tgt. + return true; +} + bool TheoryProofStepBuffer::applyPredTransform(Node src, Node tgt, const std::vector& exp, diff --git a/src/theory/theory_proof_step_buffer.h b/src/theory/theory_proof_step_buffer.h index 7a4cb368d..d67781428 100644 --- a/src/theory/theory_proof_step_buffer.h +++ b/src/theory/theory_proof_step_buffer.h @@ -36,6 +36,17 @@ class TheoryProofStepBuffer : public ProofStepBuffer TheoryProofStepBuffer(ProofChecker* pc = nullptr); ~TheoryProofStepBuffer() {} //---------------------------- utilities builtin proof rules + /** + * Apply equality introduction. If this method returns true, it adds proof + * step(s) to the buffer that conclude (= src tgt) from premises exp. In + * particular, it may attempt to apply the rule MACRO_SR_EQ_INTRO. This + * method should be applied when tgt is equivalent to src assuming exp. + */ + bool applyEqIntro(Node src, + Node tgt, + const std::vector& exp, + MethodId ids = MethodId::SB_DEFAULT, + MethodId idr = MethodId::RW_REWRITE); /** * Apply predicate transform. If this method returns true, it adds (at most * one) proof step to the buffer that conclude tgt from premises src, exp. In diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index 1adaae887..5d2711f1d 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -70,6 +70,8 @@ public: void safePoint(ResourceManager::Resource r) override {} void conflict(TNode n) override { push(CONFLICT, n); } + void trustedConflict(TrustNode n) override { push(CONFLICT, n.getNode()); } + bool propagate(TNode n) override { push(PROPAGATE, n); return true; @@ -81,6 +83,12 @@ public: return LemmaStatus(Node::null(), 0); } + LemmaStatus trustedLemma(TrustNode n, LemmaProperty p) override + { + push(LEMMA, n.getNode()); + return LemmaStatus(Node::null(), 0); + } + void requirePhase(TNode, bool) override {} void setIncomplete() override {} void handleUserAttribute(const char* attr, theory::Theory* t) override {} diff --git a/src/theory/trust_node.cpp b/src/theory/trust_node.cpp index b0c8f3b79..6c792e355 100644 --- a/src/theory/trust_node.cpp +++ b/src/theory/trust_node.cpp @@ -139,7 +139,8 @@ std::string TrustNode::identifyGenerator() const std::ostream& operator<<(std::ostream& out, TrustNode n) { - out << "(" << n.getKind() << " " << n.getProven() << ")"; + out << "(" << n.getKind() << " " << n.getProven() << " " + << n.identifyGenerator() << ")"; return out; }