(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.

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()