Dynamic allocation of equality engine in Theory (#4890)

This commit updates Theory so that equality engines are allocated dynamically. The plan is to make this configurable based on the theory combination method.

The fundamental changes include:
- Add `d_equalityEngine` (raw) pointer to Theory, which is the "official" equality engine of the theory.
- Standardize methods for initializing Theory. This is now made more explicit in the documentation in theory.h, and includes a method `finishInitStandalone` for users of Theory that don't have an associated TheoryEngine.
- Refactor TheoryEngine::finishInit, including how Theory is initialized to incorporate the new policy.
- Things related to master equality engine are now specific to EqEngineManagerDistributed and hence can be removed from TheoryEngine. This will be further refactored in forthcoming PRs.

Note that the majority of changes are due to changing `d_equalityEngine.` to `d_equalityEngine->` throughout. 

1 files changed, 16 insertions, 6 deletions

diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index aeb72ec94..f3b5641b4 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -95,7 +95,8 @@ private:
 
   const ArithVariables& d_avariables;
 
-  eq::EqualityEngine d_ee;
+  /** The equality engine being used by this class */
+  eq::EqualityEngine* d_ee;
 
   void raiseConflict(Node conflict);
 public:
@@ -108,8 +109,6 @@ public:
 
   bool canExplain(TNode n) const;
 
-  void setMasterEqualityEngine(eq::EqualityEngine* eq);
-
 private:
   Node externalToInternal(TNode n) const;
 
@@ -138,6 +137,19 @@ public:
   ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, SetupLiteralCallBack, const ArithVariables&, RaiseEqualityEngineConflict raiseConflict);
   ~ArithCongruenceManager();
 
+  //--------------------------------- initialization
+  /**
+   * Returns true if we need an equality engine, see
+   * Theory::needsEqualityEngine.
+   */
+  bool needsEqualityEngine(EeSetupInfo& esi);
+  /**
+   * Finish initialize. This class is instructed by TheoryArithPrivate to use
+   * the equality engine ee.
+   */
+  void finishInit(eq::EqualityEngine* ee);
+  //--------------------------------- end initialization
+
   Node explain(TNode literal);
   void explain(TNode lit, NodeBuilder<>& out);
 
@@ -166,10 +178,8 @@ public:
 
 
   void addSharedTerm(Node x);
-  
-  eq::EqualityEngine * getEqualityEngine() { return &d_ee; }
 
-private:
+ private:
   class Statistics {
   public:
     IntStat d_watchedVariables;