Add the distributed equality engine manager (#4867)

This is the first step towards making the approach for theory combination in CVC4 configurable.

This PR introduces the "distributed equality engine manager", which encapsulates the current policy that TheoryEngine uses regarding equality engines: each Theory creates a separate copy of an equality engine. The eventual plan is that the official equality engine of Theory is not necessarily unique to the theory, if equality engines are shared. A variant of this class could implement that policy.

This PR does not impact the code, it simply adds the definition of the class. A forthcoming PR will integrate this class into TheoryEngine, which will use dynamic allocation for equality engine objects.

FYI @barrettcw

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).