diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-28 15:40:16 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-28 15:40:16 -0500 |
commit | f51d3e353fe8e50e5e73c37c17229e603a56ecdd (patch) | |
tree | d3a00e94d2850aaac623d81df04a0bfc7f762087 /src/theory/combination_engine.cpp | |
parent | c137366e668aff70b1739a1f2c5cf8e6e2e28a72 (diff) |
(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.
Diffstat (limited to 'src/theory/combination_engine.cpp')
-rw-r--r-- | src/theory/combination_engine.cpp | 13 |
1 files changed, 9 insertions, 4 deletions
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<Theory*>& paraTheories) + const std::vector<Theory*>& 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() |