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, 13 insertions, 4 deletions

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 30de7bbad..ad3b91b07 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -55,19 +55,28 @@ class TheoryArith : public Theory {
               ProofNodeManager* pnm = nullptr);
   virtual ~TheoryArith();
 
+  //--------------------------------- initialization
+  /** get the official theory rewriter of this theory */
   TheoryRewriter* getTheoryRewriter() override;
+  /**
+   * Returns true if this theory needs an equality engine, which is assigned
+   * to it (d_equalityEngine) by the equality engine manager during
+   * TheoryEngine::finishInit, prior to calling finishInit for this theory.
+   * If this method returns true, it stores instructions for the notifications
+   * this Theory wishes to receive from its equality engine.
+   */
+  bool needsEqualityEngine(EeSetupInfo& esi) override;
+  /** finish initialization */
+  void finishInit() override;
+  //--------------------------------- end initialization
 
   /**
    * Does non-context dependent setup for a node connected to a theory.
    */
   void preRegisterTerm(TNode n) override;
 
-  void finishInit() override;
-
   TrustNode expandDefinition(Node node) override;
 
-  void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
-
   void check(Effort e) override;
   bool needsCheckLastEffort() override;
   void propagate(Effort e) override;