Add the combination engine (#4939)

This adds the combination engine, which is the module of TheoryEngine which implements the combineTheories method and owns the various components of theory combination, which includes equality engine manager, model manager, and the "shared solver" (to come later). It will have two variants, CombinationCareGraph and CombinationModelBased, the former is added with this PR.

FYI @barrettcw

The next PR will connect this module to TheoryEngine and remove a few existing methods from TheoryEngine, as they are implemented in the modules of this class.

1 files changed, 4 insertions, 1 deletions

diff --git a/src/theory/ee_manager_distributed.cpp b/src/theory/ee_manager_distributed.cpp
index 39275dd2d..ea618fcae 100644
--- a/src/theory/ee_manager_distributed.cpp
+++ b/src/theory/ee_manager_distributed.cpp
@@ -96,13 +96,16 @@ void EqEngineManagerDistributed::initializeTheories()
   }
 }
 
-void EqEngineManagerDistributed::initializeModel(TheoryModel* m)
+void EqEngineManagerDistributed::initializeModel(
+    TheoryModel* m, eq::EqualityEngineNotify* notify)
 {
   Assert(m != nullptr);
   // initialize the model equality engine
   EeSetupInfo esim;
   if (m->needsEqualityEngine(esim))
   {
+    // use the provided notification object
+    esim.d_notify = notify;
     d_modelEqualityEngine.reset(
         allocateEqualityEngine(esim, &d_modelEeContext));
     m->setEqualityEngine(d_modelEqualityEngine.get());