Connect the shared solver to theory engine (#5103)

This makes SharedSolver the main communication point for TheoryEngine during solving for combination-related solving tasks. This class is a generalization of SharedTermsDatabase, and in the distributed architecture is a wrapper around shared terms database.

It has 5 callbacks in theory engine: for preregistration, preNotifyFact (which calls addSharedTerms on theories), assertSharedEquality, explain, getEqualityStatus.

This PR has no intended behavior changes.

FYI @barrettcw

1 files changed, 10 insertions, 1 deletions

diff --git a/src/theory/ee_manager.h b/src/theory/ee_manager.h
index 8d65eb2f1..6e40ceb7b 100644
--- a/src/theory/ee_manager.h
+++ b/src/theory/ee_manager.h
@@ -30,6 +30,8 @@ class TheoryEngine;
 
 namespace theory {
 
+class SharedSolver;
+
 /**
  * This is (theory-agnostic) information associated with the management of
  * an equality engine for a single theory. This information is maintained
@@ -51,7 +53,12 @@ struct EeTheoryInfo
 class EqEngineManager
 {
  public:
-  EqEngineManager(TheoryEngine& te);
+   /**
+   * @param te Reference to the theory engine
+   * @param sharedSolver The shared solver that is being used in combination
+   * with this equality engine manager
+    */
+  EqEngineManager(TheoryEngine& te, SharedSolver& shs);
   virtual ~EqEngineManager() {}
   /**
    * Initialize theories, called during TheoryEngine::finishInit after theory
@@ -81,6 +88,8 @@ class EqEngineManager
  protected:
   /** Reference to the theory engine */
   TheoryEngine& d_te;
+  /** Reference to the shared solver */
+  SharedSolver& d_sharedSolver;
   /** Information related to the equality engine, per theory. */
   std::map<TheoryId, EeTheoryInfo> d_einfo;
 };