(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, 15 insertions, 3 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<Theory*>& paraTheories)
-    : CombinationEngine(te, paraTheories)
+    TheoryEngine& te,
+    const std::vector<Theory*>& 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);