1 files changed, 25 insertions, 5 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h
index fecdafb17..e40534dc4 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -39,6 +39,7 @@
 #include "theory/assertion.h"
 #include "theory/care_graph.h"
 #include "theory/decision_manager.h"
+#include "theory/ee_setup_info.h"
 #include "theory/logic_info.h"
 #include "theory/output_channel.h"
 #include "theory/theory_id.h"
@@ -265,6 +266,30 @@ class Theory {
   bool isLegalElimination(TNode x, TNode val);
 
  public:
+  //--------------------------------- initialization
+  /**
+   * @return The theory rewriter associated with this theory. This is primarily
+   * called for the purposes of initializing the rewriter.
+   */
+  virtual TheoryRewriter* getTheoryRewriter() = 0;
+  /**
+   * !!!! TODO: use this method (https://github.com/orgs/CVC4/projects/39).
+   *
+   * Returns true if this theory needs an equality engine for checking
+   * satisfiability.
+   *
+   * If this method returns true, then the equality engine manager will
+   * initialize its equality engine field via setEqualityEngine above during
+   * TheoryEngine::finishInit, prior to calling finishInit for this theory.
+   *
+   * Additionally, if this method returns true, then this method is required to
+   * update the argument esi with instructions for initializing and setting up
+   * notifications from its equality engine, which is commonly done with
+   * a notifications class (eq::EqualityEngineNotify).
+   */
+  virtual bool needsEqualityEngine(EeSetupInfo& esi);
+  //--------------------------------- end initialization
+
   /**
    * Return the ID of the theory responsible for the given type.
    */
@@ -331,11 +356,6 @@ class Theory {
   virtual ~Theory();
 
   /**
-   * @return The theory rewriter associated with this theory.
-   */
-  virtual TheoryRewriter* getTheoryRewriter() = 0;
-
-  /**
    * Subclasses of Theory may add additional efforts.  DO NOT CHECK
    * equality with one of these values (e.g. if STANDARD xxx) but
    * rather use range checks (or use the helper functions below).