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, 0 deletions

diff --git a/src/theory/ee_manager.cpp b/src/theory/ee_manager.cpp
new file mode 100644
index 000000000..bec355e7d
--- /dev/null
+++ b/src/theory/ee_manager.cpp
@@ -0,0 +1,31 @@
+/*********************                                                        */
+/*! \file ee_manager.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Utilities for management of equality engines.
+ **/
+
+#include "theory/ee_manager.h"
+
+namespace CVC4 {
+namespace theory {
+
+const EeTheoryInfo* EqEngineManager::getEeTheoryInfo(TheoryId tid) const
+{
+  std::map<TheoryId, EeTheoryInfo>::const_iterator it = d_einfo.find(tid);
+  if (it != d_einfo.end())
+  {
+    return &it->second;
+  }
+  return nullptr;
+}
+
+}  // namespace theory
+}  // namespace CVC4