Dynamic allocation of model equality engine (#4911)

This makes the equality engine manager responsible for initializing the equality engine of the model.

It also moves the base equality engine manager class to its own file.

Notice the code in TheoryEngine will undergo significant cleaning in forthcoming PRs when the "ModelManagerDistributed" is added. This PR adds temporary calls there to preserve the current behavior.

1 files changed, 31 insertions, 46 deletions

diff --git a/src/theory/ee_manager_distributed.h b/src/theory/ee_manager_distributed.h
index ededa956e..693466867 100644
--- a/src/theory/ee_manager_distributed.h
+++ b/src/theory/ee_manager_distributed.h
@@ -21,8 +21,7 @@
 #include <map>
 #include <memory>
 
-#include "theory/ee_setup_info.h"
-#include "theory/theory.h"
+#include "theory/ee_manager.h"
 #include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
@@ -32,38 +31,6 @@ class TheoryEngine;
 namespace theory {
 
 /**
- * This is (theory-agnostic) information associated with the management of
- * an equality engine for a single theory. This information is maintained
- * by the manager class below.
- *
- * Currently, this simply is the equality engine itself, which is a unique_ptr
- * for memory management purposes.
- */
-struct EeTheoryInfo
-{
-  EeTheoryInfo() : d_usedEe(nullptr) {}
-  /** The equality engine that the theory uses (if it exists) */
-  eq::EqualityEngine* d_usedEe;
-  /** The equality engine allocated by this theory (if it exists) */
-  std::unique_ptr<eq::EqualityEngine> d_allocEe;
-};
-
-/** Virtual base class for equality engine managers */
-class EqEngineManager
-{
- public:
-  virtual ~EqEngineManager() {}
-  /**
-   * Get the equality engine theory information for theory with the given id.
-   */
-  const EeTheoryInfo* getEeTheoryInfo(TheoryId tid) const;
-
- protected:
-  /** Information related to the equality engine, per theory. */
-  std::map<TheoryId, EeTheoryInfo> d_einfo;
-};
-
-/**
  * The (distributed) equality engine manager. This encapsulates an architecture
  * in which all theories maintain their own copy of an equality engine.
  *
@@ -84,18 +51,30 @@ class EqEngineManagerDistributed : public EqEngineManager
   EqEngineManagerDistributed(TheoryEngine& te);
   ~EqEngineManagerDistributed();
   /**
-   * Finish initialize, called by TheoryEngine::finishInit after theory
-   * objects have been created but prior to their final initialization. This
-   * sets up equality engines for all theories.
-   *
-   * This method is context-independent, and is applied once during
-   * the lifetime of TheoryEngine (during finishInit).
+   * Initialize theories. This method allocates unique equality engines
+   * per theories and connects them to a master equality engine.
    */
-  void finishInit();
-  /** get the master equality engine */
-  eq::EqualityEngine* getMasterEqualityEngine();
+  void initializeTheories() override;
+  /**
+   * Initialize model. This method allocates a new equality engine for the
+   * model.
+   */
+  void initializeModel(TheoryModel* m) override;
+  /**
+   * Get the model equality engine context. This is a dummy context that is
+   * used for clearing the contents of the model's equality engine via
+   * pop/push.
+   */
+  context::Context* getModelEqualityEngineContext();
+  /** get the model equality engine */
+  eq::EqualityEngine* getModelEqualityEngine();
+  /** get the core equality engine */
+  eq::EqualityEngine* getCoreEqualityEngine() override;
 
  private:
+  /** Allocate equality engine that is context-dependent on c with info esi */
+  eq::EqualityEngine* allocateEqualityEngine(EeSetupInfo& esi,
+                                             context::Context* c);
   /** notify class for master equality engine */
   class MasterNotifyClass : public theory::eq::EqualityEngineNotify
   {
@@ -126,15 +105,21 @@ class EqEngineManagerDistributed : public EqEngineManager
     /** Pointer to quantifiers engine */
     QuantifiersEngine* d_quantEngine;
   };
-  /** Allocate equality engine that is context-dependent on c with info esi */
-  eq::EqualityEngine* allocateEqualityEngine(EeSetupInfo& esi,
-                                             context::Context* c);
   /** Reference to the theory engine */
   TheoryEngine& d_te;
   /** The master equality engine notify class */
   std::unique_ptr<MasterNotifyClass> d_masterEENotify;
   /** The master equality engine. */
   std::unique_ptr<eq::EqualityEngine> d_masterEqualityEngine;
+  /**
+   * A dummy context for the model equality engine, so we can clear it
+   * independently of search context.
+   */
+  context::Context d_modelEeContext;
+  /**
+   * The equality engine of the model.
+   */
+  std::unique_ptr<eq::EqualityEngine> d_modelEqualityEngine;
 };
 
 }  // namespace theory