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;