Dynamic allocation of equality engine in Theory (#4890)

This commit updates Theory so that equality engines are allocated dynamically. The plan is to make this configurable based on the theory combination method.

The fundamental changes include:
- Add `d_equalityEngine` (raw) pointer to Theory, which is the "official" equality engine of the theory.
- Standardize methods for initializing Theory. This is now made more explicit in the documentation in theory.h, and includes a method `finishInitStandalone` for users of Theory that don't have an associated TheoryEngine.
- Refactor TheoryEngine::finishInit, including how Theory is initialized to incorporate the new policy.
- Things related to master equality engine are now specific to EqEngineManagerDistributed and hence can be removed from TheoryEngine. This will be further refactored in forthcoming PRs.

Note that the majority of changes are due to changing `d_equalityEngine.` to `d_equalityEngine->` throughout. 

6 files changed, 91 insertions, 47 deletions

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index ab3b485a8..a70339c01 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -42,16 +42,29 @@ ArithCongruenceManager::ArithCongruenceManager(
       d_constraintDatabase(cd),
       d_setupLiteral(setup),
       d_avariables(avars),
-      d_ee(d_notify, c, "theory::arith::ArithCongruenceManager", true)
+      d_ee(nullptr)
 {
-  d_ee.addFunctionKind(kind::NONLINEAR_MULT);
-  d_ee.addFunctionKind(kind::EXPONENTIAL);
-  d_ee.addFunctionKind(kind::SINE);
-  d_ee.addFunctionKind(kind::IAND);
 }
 
 ArithCongruenceManager::~ArithCongruenceManager() {}
 
+bool ArithCongruenceManager::needsEqualityEngine(EeSetupInfo& esi)
+{
+  esi.d_notify = &d_notify;
+  esi.d_name = "theory::arith::ArithCongruenceManager";
+  return true;
+}
+
+void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee)
+{
+  Assert(ee != nullptr);
+  d_ee = ee;
+  d_ee->addFunctionKind(kind::NONLINEAR_MULT);
+  d_ee->addFunctionKind(kind::EXPONENTIAL);
+  d_ee->addFunctionKind(kind::SINE);
+  d_ee->addFunctionKind(kind::IAND);
+}
+
 ArithCongruenceManager::Statistics::Statistics():
   d_watchedVariables("theory::arith::congruence::watchedVariables", 0),
   d_watchedVariableIsZero("theory::arith::congruence::watchedVariableIsZero", 0),
@@ -141,10 +154,6 @@ bool ArithCongruenceManager::canExplain(TNode n) const {
   return d_explanationMap.find(n) != d_explanationMap.end();
 }
 
-void ArithCongruenceManager::setMasterEqualityEngine(eq::EqualityEngine* eq) {
-  d_ee.setMasterEqualityEngine(eq);
-}
-
 Node ArithCongruenceManager::externalToInternal(TNode n) const{
   Assert(canExplain(n));
   ExplainMap::const_iterator iter = d_explanationMap.find(n);
@@ -320,9 +329,9 @@ bool ArithCongruenceManager::propagate(TNode x){
 
 void ArithCongruenceManager::explain(TNode literal, std::vector<TNode>& assumptions) {
   if (literal.getKind() != kind::NOT) {
-    d_ee.explainEquality(literal[0], literal[1], true, assumptions);
+    d_ee->explainEquality(literal[0], literal[1], true, assumptions);
   } else {
-    d_ee.explainEquality(literal[0][0], literal[0][1], false, assumptions);
+    d_ee->explainEquality(literal[0][0], literal[0][1], false, assumptions);
   }
 }
 
@@ -392,9 +401,9 @@ void ArithCongruenceManager::assertionToEqualityEngine(bool isEquality, ArithVar
 
   Trace("arith-ee") << "Assert " << eq << ", pol " << isEquality << ", reason " << reason << std::endl;
   if(isEquality){
-    d_ee.assertEquality(eq, true, reason);
+    d_ee->assertEquality(eq, true, reason);
   }else{
-    d_ee.assertEquality(eq, false, reason);
+    d_ee->assertEquality(eq, false, reason);
   }
 }
 
@@ -417,7 +426,7 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP c){
   d_keepAlive.push_back(reason);
 
   Trace("arith-ee") << "Assert equalsConstant " << eq << ", reason " << reason << std::endl;
-  d_ee.assertEquality(eq, true, reason);
+  d_ee->assertEquality(eq, true, reason);
 }
 
 void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){
@@ -441,11 +450,11 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){
   d_keepAlive.push_back(reason);
 
   Trace("arith-ee") << "Assert equalsConstant2 " << eq << ", reason " << reason << std::endl;
-  d_ee.assertEquality(eq, true, reason);
+  d_ee->assertEquality(eq, true, reason);
 }
 
 void ArithCongruenceManager::addSharedTerm(Node x){
-  d_ee.addTriggerTerm(x, THEORY_ARITH);
+  d_ee->addTriggerTerm(x, THEORY_ARITH);
 }
 
 }/* CVC4::theory::arith namespace */
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index aeb72ec94..f3b5641b4 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -95,7 +95,8 @@ private:
 
   const ArithVariables& d_avariables;
 
-  eq::EqualityEngine d_ee;
+  /** The equality engine being used by this class */
+  eq::EqualityEngine* d_ee;
 
   void raiseConflict(Node conflict);
 public:
@@ -108,8 +109,6 @@ public:
 
   bool canExplain(TNode n) const;
 
-  void setMasterEqualityEngine(eq::EqualityEngine* eq);
-
 private:
   Node externalToInternal(TNode n) const;
 
@@ -138,6 +137,19 @@ public:
   ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, SetupLiteralCallBack, const ArithVariables&, RaiseEqualityEngineConflict raiseConflict);
   ~ArithCongruenceManager();
 
+  //--------------------------------- initialization
+  /**
+   * Returns true if we need an equality engine, see
+   * Theory::needsEqualityEngine.
+   */
+  bool needsEqualityEngine(EeSetupInfo& esi);
+  /**
+   * Finish initialize. This class is instructed by TheoryArithPrivate to use
+   * the equality engine ee.
+   */
+  void finishInit(eq::EqualityEngine* ee);
+  //--------------------------------- end initialization
+
   Node explain(TNode literal);
   void explain(TNode lit, NodeBuilder<>& out);
 
@@ -166,10 +178,8 @@ public:
 
 
   void addSharedTerm(Node x);
-  
-  eq::EqualityEngine * getEqualityEngine() { return &d_ee; }
 
-private:
+ private:
   class Statistics {
   public:
     IntStat d_watchedVariables;
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index bc6e18a83..b95b5e243 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -56,10 +56,10 @@ TheoryRewriter* TheoryArith::getTheoryRewriter()
   return d_internal->getTheoryRewriter();
 }
 
-void TheoryArith::preRegisterTerm(TNode n){
-  d_internal->preRegisterTerm(n);
+bool TheoryArith::needsEqualityEngine(EeSetupInfo& esi)
+{
+  return d_internal->needsEqualityEngine(esi);
 }
-
 void TheoryArith::finishInit()
 {
   if (getLogicInfo().isTheoryEnabled(THEORY_ARITH)
@@ -72,17 +72,17 @@ void TheoryArith::finishInit()
     d_valuation.setUnevaluatedKind(kind::SINE);
     d_valuation.setUnevaluatedKind(kind::PI);
   }
+  // finish initialize internally
+  d_internal->finishInit();
 }
 
+void TheoryArith::preRegisterTerm(TNode n) { d_internal->preRegisterTerm(n); }
+
 TrustNode TheoryArith::expandDefinition(Node node)
 {
   return d_internal->expandDefinition(node);
 }
 
-void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) {
-  d_internal->setMasterEqualityEngine(eq);
-}
-
 void TheoryArith::addSharedTerm(TNode n){
   d_internal->addSharedTerm(n);
 }
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 30de7bbad..ad3b91b07 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -55,19 +55,28 @@ class TheoryArith : public Theory {
               ProofNodeManager* pnm = nullptr);
   virtual ~TheoryArith();
 
+  //--------------------------------- initialization
+  /** get the official theory rewriter of this theory */
   TheoryRewriter* getTheoryRewriter() override;
+  /**
+   * Returns true if this theory needs an equality engine, which is assigned
+   * to it (d_equalityEngine) by the equality engine manager during
+   * TheoryEngine::finishInit, prior to calling finishInit for this theory.
+   * If this method returns true, it stores instructions for the notifications
+   * this Theory wishes to receive from its equality engine.
+   */
+  bool needsEqualityEngine(EeSetupInfo& esi) override;
+  /** finish initialization */
+  void finishInit() override;
+  //--------------------------------- end initialization
 
   /**
    * Does non-context dependent setup for a node connected to a theory.
    */
   void preRegisterTerm(TNode n) override;
 
-  void finishInit() override;
-
   TrustNode expandDefinition(Node node) override;
 
-  void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
-
   void check(Effort e) override;
   bool needsCheckLastEffort() override;
   void propagate(Effort e) override;
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 6f47ffb0e..8ca99d369 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -134,7 +134,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
           d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
       d_attemptSolSimplex(
           d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
-      d_nonlinearExtension(NULL),
+      d_nonlinearExtension(nullptr),
       d_pass1SDP(NULL),
       d_otherSDP(NULL),
       d_lastContextIntegerAttempted(c, -1),
@@ -159,12 +159,6 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
       d_statistics(),
       d_opElim(pnm, logicInfo)
 {
-  // only need to create if non-linear logic
-  if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear())
-  {
-    d_nonlinearExtension = new nl::NonlinearExtension(
-        containing, d_congruenceManager.getEqualityEngine());
-  }
 }
 
 TheoryArithPrivate::~TheoryArithPrivate(){
@@ -173,6 +167,24 @@ TheoryArithPrivate::~TheoryArithPrivate(){
   if(d_nonlinearExtension != NULL) { delete d_nonlinearExtension; }
 }
 
+TheoryRewriter* TheoryArithPrivate::getTheoryRewriter() { return &d_rewriter; }
+bool TheoryArithPrivate::needsEqualityEngine(EeSetupInfo& esi)
+{
+  return d_congruenceManager.needsEqualityEngine(esi);
+}
+void TheoryArithPrivate::finishInit()
+{
+  eq::EqualityEngine* ee = d_containing.getEqualityEngine();
+  Assert(ee != nullptr);
+  d_congruenceManager.finishInit(ee);
+  const LogicInfo& logicInfo = getLogicInfo();
+  // only need to create nonlinear extension if non-linear logic
+  if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear())
+  {
+    d_nonlinearExtension = new nl::NonlinearExtension(d_containing, ee);
+  }
+}
+
 static bool contains(const ConstraintCPVec& v, ConstraintP con){
   for(unsigned i = 0, N = v.size(); i < N; ++i){
     if(v[i] == con){
@@ -227,10 +239,6 @@ static void resolve(ConstraintCPVec& buf, ConstraintP c, const ConstraintCPVec&
   // return safeConstructNary(nb);
 }
 
-void TheoryArithPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
-  d_congruenceManager.setMasterEqualityEngine(eq);
-}
-
 TheoryArithPrivate::ModelException::ModelException(TNode n, const char* msg)
 {
   stringstream ss;
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 42ec7f47b..4c4aedf00 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -427,7 +427,17 @@ private:
                      ProofNodeManager* pnm);
   ~TheoryArithPrivate();
 
-  TheoryRewriter* getTheoryRewriter() { return &d_rewriter; }
+  //--------------------------------- initialization
+  /** get the official theory rewriter of this theory */
+  TheoryRewriter* getTheoryRewriter();
+  /**
+   * Returns true if we need an equality engine, see
+   * Theory::needsEqualityEngine.
+   */
+  bool needsEqualityEngine(EeSetupInfo& esi);
+  /** finish initialize */
+  void finishInit();
+  //--------------------------------- end initialization
 
   /**
    * Does non-context dependent setup for a node connected to a theory.
@@ -435,8 +445,6 @@ private:
   void preRegisterTerm(TNode n);
   TrustNode expandDefinition(Node node);
 
-  void setMasterEqualityEngine(eq::EqualityEngine* eq);
-
   void check(Theory::Effort e);
   bool needsCheckLastEffort();
   void propagate(Theory::Effort e);