More flexible design for model manager distributed (#4976)

This PR makes it so that the distributed model manager can be used independently of the architecture for equality engine management for theories, meaning the choice of using a separate equality engine for the model can be done in both the current distributed architecture, or the proposed central architecture (where there would be 2 equality engines, the central one and the model one). The "central model manager" on the other hand will only be combined with the central architecture. This will make it easier to test the centralized equality engine manager, since all things related to model construction can be preserved when using a central architecture.

This PR moves some of the responsibilities from the (distributed) equality engine manager to the distributed model manager, including the management of the context of the model equality engine and the allocation of its equality engine.

This PR is not intended to make any behavior changes to the current architecture.

1 files changed, 13 insertions, 14 deletions

diff --git a/src/theory/model_manager_distributed.h b/src/theory/model_manager_distributed.h
index 2f86c0b00..2cf35d039 100644
--- a/src/theory/model_manager_distributed.h
+++ b/src/theory/model_manager_distributed.h
@@ -19,7 +19,7 @@
 
 #include <memory>
 
-#include "theory/ee_manager_distributed.h"
+#include "theory/ee_manager.h"
 #include "theory/model_manager.h"
 
 namespace CVC4 {
@@ -29,17 +29,20 @@ class TheoryEngine;
 namespace theory {
 
 /**
- * Manager for building models in a distributed architecture. Its prepare
- * model method uses collectModelInfo to assert all equalities from the equality
- * engine of each theory into the equality engine of the model. It additionally
- * uses the model equality engine context to clear the information from
- * the model's equality engine, as maintained by the distributed equality
- * engine manager.
+ * Manager for building models where the equality engine of the model is
+ * a separate instance. Notice that this manager can be used regardless of the
+ * method for managing the equality engines of the theories (which is the
+ * responsibility of the equality engine manager eem referenced by this class).
+ *
+ * Its prepare model method uses collectModelInfo to assert all equalities from
+ * the equality engine of each theory into the equality engine of the model. It
+ * additionally uses the model equality engine context to clear the information
+ * from the model's equality engine, which is maintained by this class.
  */
 class ModelManagerDistributed : public ModelManager
 {
  public:
-  ModelManagerDistributed(TheoryEngine& te, EqEngineManagerDistributed& eem);
+  ModelManagerDistributed(TheoryEngine& te, EqEngineManager& eem);
   ~ModelManagerDistributed();
 
   /** Prepare the model, as described above. */
@@ -49,13 +52,9 @@ class ModelManagerDistributed : public ModelManager
    * model, return true if successful.
    */
   bool finishBuildModel() const override;
-
  protected:
-  /**
-   * Distributed equality engine manager, which maintains the context of the
-   * model's equality engine.
-   */
-  EqEngineManagerDistributed& d_eem;
+  /** Initialize model equality engine */
+  void initializeModelEqEngine(eq::EqualityEngineNotify* notify) override;
 };
 
 }  // namespace theory