Dynamic allocation of model equality engine (#4911)

This makes the equality engine manager responsible for initializing the equality engine of the model.

It also moves the base equality engine manager class to its own file.

Notice the code in TheoryEngine will undergo significant cleaning in forthcoming PRs when the "ModelManagerDistributed" is added. This PR adds temporary calls there to preserve the current behavior.

1 files changed, 22 insertions, 16 deletions

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 4c7600da2..725a932a2 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -29,9 +29,9 @@ namespace theory {
 TheoryModel::TheoryModel(context::Context* c,
                          std::string name,
                          bool enableFuncModels)
-    : d_substitutions(c, false),
-      d_modelBuilt(false),
-      d_modelBuiltSuccess(false),
+    : d_name(name),
+      d_substitutions(c, false),
+      d_equalityEngine(nullptr),
       d_using_model_core(false),
       d_enableFuncModels(enableFuncModels)
 {
@@ -39,10 +39,26 @@ TheoryModel::TheoryModel(context::Context* c,
   Assert(d_enableFuncModels || !options::ufHo());
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
+}
+
+TheoryModel::~TheoryModel() {}
+
+void TheoryModel::setEqualityEngine(eq::EqualityEngine* ee)
+{
+  d_equalityEngine = ee;
+}
 
-  d_eeContext = new context::Context();
-  d_equalityEngine = new eq::EqualityEngine(d_eeContext, name, false);
+bool TheoryModel::needsEqualityEngine(EeSetupInfo& esi)
+{
+  // no notifications
+  esi.d_name = d_name;
+  esi.d_constantsAreTriggers = false;
+  return true;
+}
 
+void TheoryModel::finishInit()
+{
+  Assert(d_equalityEngine != nullptr);
   // The kinds we are treating as function application in congruence
   d_equalityEngine->addFunctionKind(kind::APPLY_UF, false, options::ufHo());
   d_equalityEngine->addFunctionKind(kind::HO_APPLY);
@@ -51,21 +67,13 @@ TheoryModel::TheoryModel(context::Context* c,
   d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR);
   d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
   d_equalityEngine->addFunctionKind(kind::APPLY_TESTER);
-  d_eeContext->push();
   // do not interpret APPLY_UF if we are not assigning function values
-  if (!enableFuncModels)
+  if (!d_enableFuncModels)
   {
     setSemiEvaluatedKind(kind::APPLY_UF);
   }
 }
 
-TheoryModel::~TheoryModel()
-{
-  d_eeContext->pop();
-  delete d_equalityEngine;
-  delete d_eeContext;
-}
-
 void TheoryModel::reset(){
   d_modelBuilt = false;
   d_modelBuiltSuccess = false;
@@ -83,8 +91,6 @@ void TheoryModel::reset(){
   d_uf_terms.clear();
   d_ho_uf_terms.clear();
   d_uf_models.clear();
-  d_eeContext->pop();
-  d_eeContext->push();
   d_using_model_core = false;
   d_model_core.clear();
 }