Dynamic allocation of equality engine for shared solver (#5152)

This updates shared solver to have dynamic allocation of equality engine, analogous to theory solvers.

1 files changed, 12 insertions, 0 deletions

diff --git a/src/theory/ee_manager_distributed.cpp b/src/theory/ee_manager_distributed.cpp
index 360b1257b..3fb5fc0ce 100644
--- a/src/theory/ee_manager_distributed.cpp
+++ b/src/theory/ee_manager_distributed.cpp
@@ -34,6 +34,18 @@ EqEngineManagerDistributed::~EqEngineManagerDistributed()
 void EqEngineManagerDistributed::initializeTheories()
 {
   context::Context* c = d_te.getSatContext();
+  // initialize the shared solver
+  EeSetupInfo esis;
+  if (d_sharedSolver.needsEqualityEngine(esis))
+  {
+    // allocate an equality engine for the shared terms database
+    d_stbEqualityEngine.reset(allocateEqualityEngine(esis, c));
+    d_sharedSolver.setEqualityEngine(d_stbEqualityEngine.get());
+  }
+  else
+  {
+    Unhandled() << "Expected shared solver to use equality engine";
+  }
 
   // allocate equality engines per theory
   for (TheoryId theoryId = theory::THEORY_FIRST;