From f51d3e353fe8e50e5e73c37c17229e603a56ecdd Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 28 Aug 2020 15:40:16 -0500 Subject: [PATCH] (proof-new) Make CombinationEngine proof producing (#4955) Makes combination engine proof producing (for Boolean splits). Followup PRs will start to add proof production in TheoryEngine. --- src/theory/combination_care_graph.cpp | 18 +++++++++++++++--- src/theory/combination_care_graph.h | 3 ++- src/theory/combination_engine.cpp | 13 +++++++++---- src/theory/combination_engine.h | 14 ++++++++++++-- src/theory/theory_engine.cpp | 3 ++- src/theory/theory_engine.h | 5 +++++ 6 files changed, 45 insertions(+), 11 deletions(-) diff --git a/src/theory/combination_care_graph.cpp b/src/theory/combination_care_graph.cpp index 9374e7ecb..c390a4b25 100644 --- a/src/theory/combination_care_graph.cpp +++ b/src/theory/combination_care_graph.cpp @@ -22,8 +22,10 @@ namespace CVC4 { namespace theory { CombinationCareGraph::CombinationCareGraph( - TheoryEngine& te, const std::vector& paraTheories) - : CombinationEngine(te, paraTheories) + TheoryEngine& te, + const std::vector& paraTheories, + ProofNodeManager* pnm) + : CombinationEngine(te, paraTheories, pnm) { } @@ -62,7 +64,17 @@ void CombinationCareGraph::combineTheories() << "TheoryEngine::combineTheories(): requesting a split " << std::endl; Node split = equality.orNode(equality.notNode()); - sendLemma(split, carePair.d_theory); + TrustNode tsplit; + if (isProofEnabled()) + { + // make proof of splitting lemma + tsplit = d_cmbsPg->mkTrustNode(split, PfRule::SPLIT, {equality}); + } + else + { + tsplit = TrustNode::mkTrustLemma(split, nullptr); + } + sendLemma(tsplit, carePair.d_theory); // Could check the equality status here: // EqualityStatus es = getEqualityStatus(carePair.d_a, carePair.d_b); diff --git a/src/theory/combination_care_graph.h b/src/theory/combination_care_graph.h index 0fbefb16a..78f892f5e 100644 --- a/src/theory/combination_care_graph.h +++ b/src/theory/combination_care_graph.h @@ -35,7 +35,8 @@ class CombinationCareGraph : public CombinationEngine { public: CombinationCareGraph(TheoryEngine& te, - const std::vector& paraTheories); + const std::vector& paraTheories, + ProofNodeManager* pnm); ~CombinationCareGraph(); bool buildModel() override; diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp index 83aae3f54..e1317cf29 100644 --- a/src/theory/combination_engine.cpp +++ b/src/theory/combination_engine.cpp @@ -26,12 +26,15 @@ namespace CVC4 { namespace theory { CombinationEngine::CombinationEngine(TheoryEngine& te, - const std::vector& paraTheories) + const std::vector& paraTheories, + ProofNodeManager* pnm) : d_te(te), d_logicInfo(te.getLogicInfo()), d_paraTheories(paraTheories), d_eemanager(nullptr), - d_mmanager(nullptr) + d_mmanager(nullptr), + d_cmbsPg(pnm ? new EagerProofGenerator(pnm, te.getUserContext()) + : nullptr) { } @@ -100,15 +103,17 @@ theory::TheoryModel* CombinationEngine::getModel() return d_mmanager->getModel(); } +bool CombinationEngine::isProofEnabled() const { return d_cmbsPg != nullptr; } + eq::EqualityEngineNotify* CombinationEngine::getModelEqualityEngineNotify() { // by default, no notifications from model's equality engine return nullptr; } -void CombinationEngine::sendLemma(TNode node, TheoryId atomsTo) +void CombinationEngine::sendLemma(TrustNode trn, TheoryId atomsTo) { - d_te.lemma(node, RULE_INVALID, false, LemmaProperty::NONE, atomsTo); + d_te.lemma(trn.getNode(), RULE_INVALID, false, LemmaProperty::NONE, atomsTo); } void CombinationEngine::resetRound() diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h index cfe6562d4..3aabc549a 100644 --- a/src/theory/combination_engine.h +++ b/src/theory/combination_engine.h @@ -20,6 +20,7 @@ #include #include +#include "theory/eager_proof_generator.h" #include "theory/ee_manager.h" #include "theory/model_manager.h" @@ -39,7 +40,9 @@ namespace theory { class CombinationEngine { public: - CombinationEngine(TheoryEngine& te, const std::vector& paraTheories); + CombinationEngine(TheoryEngine& te, + const std::vector& paraTheories, + ProofNodeManager* pnm); virtual ~CombinationEngine(); /** Finish initialization */ @@ -91,13 +94,15 @@ class CombinationEngine virtual void combineTheories() = 0; protected: + /** Is proof enabled? */ + bool isProofEnabled() const; /** * Get model equality engine notify. Return the notification object for * who listens to the model's equality engine (if any). */ virtual eq::EqualityEngineNotify* getModelEqualityEngineNotify(); /** Send lemma to the theory engine, atomsTo is the theory to send atoms to */ - void sendLemma(TNode node, TheoryId atomsTo); + void sendLemma(TrustNode trn, TheoryId atomsTo); /** Reference to the theory engine */ TheoryEngine& d_te; /** Logic info of theory engine (cached) */ @@ -114,6 +119,11 @@ class CombinationEngine * model. */ std::unique_ptr d_mmanager; + /** + * An eager proof generator, if proofs are enabled. This proof generator is + * responsible for proofs of splitting lemmas generated in combineTheories. + */ + std::unique_ptr d_cmbsPg; }; } // namespace theory diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 0979d447b..bf74cd016 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -151,7 +151,7 @@ void TheoryEngine::finishInit() { // Initialize the theory combination architecture if (options::tcMode() == options::TcMode::CARE_GRAPH) { - d_tc.reset(new CombinationCareGraph(*this, paraTheories)); + d_tc.reset(new CombinationCareGraph(*this, paraTheories, d_pnm)); } else { @@ -213,6 +213,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_context(context), d_userContext(userContext), d_logicInfo(logicInfo), + d_pnm(nullptr), d_sharedTerms(this, context), d_tc(nullptr), d_quantEngine(nullptr), diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 61ee30bc8..b1543ad0b 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -144,6 +144,11 @@ class TheoryEngine { */ const LogicInfo& d_logicInfo; + //--------------------------------- new proofs + /** Proof node manager used by this theory engine, if proofs are enabled */ + ProofNodeManager* d_pnm; + //--------------------------------- end new proofs + /** * The database of shared terms. */ -- 2.30.2