1 files changed, 11 insertions, 8 deletions
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 345547301..001c947e9 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -116,9 +116,6 @@ private:
   /** the higher-order solver extension (or nullptr if it does not exist) */
   std::unique_ptr<HoExtension> d_ho;
 
-  /** Equaltity engine */
-  eq::EqualityEngine d_equalityEngine;
-
   /** Are we in conflict */
   context::CDO<bool> d_conflict;
 
@@ -186,10 +183,18 @@ private:
 
   ~TheoryUF();
 
-  TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
-
-  void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
+  //--------------------------------- initialization
+  /** get the official theory rewriter of this theory */
+  TheoryRewriter* getTheoryRewriter() override;
+  /**
+   * Returns true if we need an equality engine. If so, we initialize the
+   * information regarding how it should be setup. For details, see the
+   * documentation in Theory::needsEqualityEngine.
+   */
+  bool needsEqualityEngine(EeSetupInfo& esi) override;
+  /** finish initialization */
   void finishInit() override;
+  //--------------------------------- end initialization
 
   void check(Effort) override;
   TrustNode expandDefinition(Node node) override;
@@ -210,8 +215,6 @@ private:
 
   std::string identify() const override { return "THEORY_UF"; }
 
-  eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; }
-
   /** get a pointer to the uf with cardinality */
   CardinalityExtension* getCardinalityExtension() const { return d_thss.get(); }
   /** are we in conflict? */