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, 2 insertions, 9 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 7639afdbf..cfca03515 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -154,14 +154,10 @@ class TheoryEngine {
   /** The proof generator */
   std::shared_ptr<TheoryEngineProofGenerator> d_tepg;
   //--------------------------------- end new proofs
-
-  /**
-   * The database of shared terms.
-   */
-  SharedTermsDatabase d_sharedTerms;
-
   /** The combination manager we are using */
   std::unique_ptr<theory::CombinationEngine> d_tc;
+  /** The shared solver of the above combination engine. */
+  theory::SharedSolver* d_sharedSolver;
   /**
    * The quantifiers engine
    */
@@ -176,9 +172,6 @@ class TheoryEngine {
   /** Default visitor for pre-registration */
   PreRegisterVisitor d_preRegistrationVisitor;
 
-  /** Visitor for collecting shared terms */
-  SharedTermsVisitor d_sharedTermsVisitor;
-
   /** are we in eager model building mode? (see setEagerModelBuilding). */
   bool d_eager_model_building;