Add the shared solver (#4982)

This PR adds the definition for the "shared solver", it does not connect it to TheoryEngine/CombinationEngine yet. This is an object that behaves like a "glue" theory solver and has a special role in TheoryEngine.

In the current architecture, the "SharedTermsDatabase" is the "shared solver", although in the central architecture, the shared solver will be required to behave differently. This PR adds the abstract definition of shared solver, where notice SharedSolverDistributed is a thin layer on top of SharedTermsDatabase.

In a followup PR, CombinationEngine will maintain a shared solver and ~5 blocks of code in TheoryEngine will be callbacks to the SharedSolver. Also, eventually the code for SharedTermsDatabase should be split: the parts involving equality reason/propagation/explanation should be migrated into SharedSolverDistributed, and the parts related to registration will remain in SharedTermsDatabase (to also be used in the planned SharedSolverCentral).

FYI @barrettcw

1 files changed, 12 insertions, 0 deletions

diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index b01cef377..034401b9a 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -44,6 +44,18 @@ SharedTermsDatabase::~SharedTermsDatabase()
   smtStatisticsRegistry()->unregisterStat(&d_statSharedTerms);
 }
 
+void SharedTermsDatabase::setEqualityEngine(eq::EqualityEngine* ee)
+{
+  // TODO (project #39): dynamic allocation of equality engine here
+}
+
+bool SharedTermsDatabase::needsEqualityEngine(EeSetupInfo& esi)
+{
+  esi.d_notify = &d_EENotify;
+  esi.d_name = "SharedTermsDatabase";
+  return true;
+}
+
 void SharedTermsDatabase::addEqualityToPropagate(TNode equality) {
   d_registeredEqualities.insert(equality);
   d_equalityEngine.addTriggerPredicate(equality);