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. 

4 files changed, 148 insertions, 116 deletions

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index c49909fe6..48ec81a1e 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -35,55 +35,65 @@ using namespace CVC4::theory::bv::utils;
 CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv, ExtTheory* extt)
     : SubtheorySolver(c, bv),
       d_notify(*this),
-      d_equalityEngine(d_notify, c, "theory::bv::ee", true),
       d_slicer(new Slicer()),
       d_isComplete(c, true),
       d_lemmaThreshold(16),
       d_useSlicer(false),
       d_preregisterCalled(false),
       d_checkCalled(false),
+      d_bv(bv),
       d_extTheory(extt),
       d_reasons(c)
 {
-  // The kinds we are treating as function application in congruence
-  d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT, true);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP);
-  d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT, true);
-  d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS, true);
-  d_equalityEngine.addFunctionKind(kind::BITVECTOR_EXTRACT, true);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT);
-  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE);
-  d_equalityEngine.addFunctionKind(kind::BITVECTOR_TO_NAT);
-  d_equalityEngine.addFunctionKind(kind::INT_TO_BITVECTOR);
 }
 
 CoreSolver::~CoreSolver() {}
 
-void CoreSolver::setMasterEqualityEngine(eq::EqualityEngine* eq) {
-  d_equalityEngine.setMasterEqualityEngine(eq);
+bool CoreSolver::needsEqualityEngine(EeSetupInfo& esi)
+{
+  esi.d_notify = &d_notify;
+  esi.d_name = "theory::bv::ee";
+  return true;
+}
+
+void CoreSolver::finishInit()
+{
+  // use the parent's equality engine, which may be the one we allocated above
+  d_equalityEngine = d_bv->getEqualityEngine();
+
+  // The kinds we are treating as function application in congruence
+  d_equalityEngine->addFunctionKind(kind::BITVECTOR_CONCAT, true);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_AND);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_OR);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_XOR);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_NOT);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_NAND);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_NOR);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_XNOR);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_COMP);
+  d_equalityEngine->addFunctionKind(kind::BITVECTOR_MULT, true);
+  d_equalityEngine->addFunctionKind(kind::BITVECTOR_PLUS, true);
+  d_equalityEngine->addFunctionKind(kind::BITVECTOR_EXTRACT, true);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_SUB);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_NEG);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_UDIV);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_UREM);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_SDIV);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_SREM);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_SMOD);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_SHL);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_LSHR);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_ASHR);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_ULT);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_ULE);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_UGT);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_UGE);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_SLT);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_SLE);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_SGT);
+  //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_SGE);
+  d_equalityEngine->addFunctionKind(kind::BITVECTOR_TO_NAT);
+  d_equalityEngine->addFunctionKind(kind::INT_TO_BITVECTOR);
 }
 
 void CoreSolver::enableSlicer() {
@@ -95,13 +105,14 @@ void CoreSolver::enableSlicer() {
 void CoreSolver::preRegister(TNode node) {
   d_preregisterCalled = true;
   if (node.getKind() == kind::EQUAL) {
-      d_equalityEngine.addTriggerEquality(node);
-      if (d_useSlicer) {
-        d_slicer->processEquality(node);
-        AlwaysAssert(!d_checkCalled);
+    d_equalityEngine->addTriggerEquality(node);
+    if (d_useSlicer)
+    {
+      d_slicer->processEquality(node);
+      AlwaysAssert(!d_checkCalled);
       }
   } else {
-    d_equalityEngine.addTerm(node);
+    d_equalityEngine->addTerm(node);
     // Register with the extended theory, for context-dependent simplification.
     // Notice we do this for registered terms but not internally generated
     // equivalence classes. The two should roughly cooincide. Since ExtTheory is
@@ -115,9 +126,9 @@ void CoreSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
   bool polarity = literal.getKind() != kind::NOT;
   TNode atom = polarity ? literal : literal[0];
   if (atom.getKind() == kind::EQUAL) {
-    d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
+    d_equalityEngine->explainEquality(atom[0], atom[1], polarity, assumptions);
   } else {
-    d_equalityEngine.explainPredicate(atom, polarity, assumptions);
+    d_equalityEngine->explainPredicate(atom, polarity, assumptions);
   }
 }
 
@@ -224,14 +235,14 @@ void CoreSolver::buildModel()
   TNodeSet constants;
   TNodeSet constants_in_eq_engine;
   // collect constants in equality engine
-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
   while (!eqcs_i.isFinished())
   {
     TNode repr = *eqcs_i;
     if (repr.getKind() == kind::CONST_BITVECTOR)
     {
       // must check if it's just the constant
-      eq::EqClassIterator it(repr, &d_equalityEngine);
+      eq::EqClassIterator it(repr, d_equalityEngine);
       if (!(++it).isFinished() || true)
       {
         constants.insert(repr);
@@ -243,7 +254,7 @@ void CoreSolver::buildModel()
 
   // build repr to value map
 
-  eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
+  eqcs_i = eq::EqClassesIterator(d_equalityEngine);
   while (!eqcs_i.isFinished())
   {
     TNode repr = *eqcs_i;
@@ -351,15 +362,16 @@ bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
     if (predicate.getKind() == kind::EQUAL) {
       if (negated) {
         // dis-equality
-        d_equalityEngine.assertEquality(predicate, false, reason);
+        d_equalityEngine->assertEquality(predicate, false, reason);
       } else {
         // equality
-        d_equalityEngine.assertEquality(predicate, true, reason);
+        d_equalityEngine->assertEquality(predicate, true, reason);
       }
     } else {
       // Adding predicate if the congruence over it is turned on
-      if (d_equalityEngine.isFunctionKind(predicate.getKind())) {
-        d_equalityEngine.assertPredicate(predicate, !negated, reason);
+      if (d_equalityEngine->isFunctionKind(predicate.getKind()))
+      {
+        d_equalityEngine->assertPredicate(predicate, !negated, reason);
       }
     }
   }
@@ -408,7 +420,7 @@ bool CoreSolver::storePropagation(TNode literal) {
 
 void CoreSolver::conflict(TNode a, TNode b) {
   std::vector<TNode> assumptions;
-  d_equalityEngine.explainEquality(a, b, true, assumptions);
+  d_equalityEngine->explainEquality(a, b, true, assumptions);
   Node conflict = flattenAnd(assumptions);
   d_bv->setConflict(conflict);
 }
@@ -434,7 +446,7 @@ bool CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel)
   }
   set<Node> termSet;
   d_bv->computeRelevantTerms(termSet);
-  if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
+  if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
   {
     return false;
   }
@@ -457,7 +469,7 @@ bool CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel)
 Node CoreSolver::getModelValue(TNode var) {
   Debug("bitvector-model") << "CoreSolver::getModelValue (" << var <<")";
   Assert(isComplete());
-  TNode repr = d_equalityEngine.getRepresentative(var);
+  TNode repr = d_equalityEngine->getRepresentative(var);
   Node result = Node();
   if (repr.getKind() == kind::CONST_BITVECTOR) {
     result = repr;
@@ -472,6 +484,35 @@ Node CoreSolver::getModelValue(TNode var) {
   return result;
 }
 
+void CoreSolver::addSharedTerm(TNode t)
+{
+  d_equalityEngine->addTriggerTerm(t, THEORY_BV);
+}
+
+EqualityStatus CoreSolver::getEqualityStatus(TNode a, TNode b)
+{
+  if (d_equalityEngine->areEqual(a, b))
+  {
+    // The terms are implied to be equal
+    return EQUALITY_TRUE;
+  }
+  if (d_equalityEngine->areDisequal(a, b, false))
+  {
+    // The terms are implied to be dis-equal
+    return EQUALITY_FALSE;
+  }
+  return EQUALITY_UNKNOWN;
+}
+
+bool CoreSolver::hasTerm(TNode node) const
+{
+  return d_equalityEngine->hasTerm(node);
+}
+void CoreSolver::addTermToEqualityEngine(TNode node)
+{
+  d_equalityEngine->addTerm(node);
+}
+
 CoreSolver::Statistics::Statistics()
   : d_numCallstoCheck("theory::bv::CoreSolver::NumCallsToCheck", 0)
   , d_slicerEnabled("theory::bv::CoreSolver::SlicerEnabled", false)
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index ea652e7cd..33f119e5f 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -70,9 +70,6 @@ class CoreSolver : public SubtheorySolver {
   /** The notify class for d_equalityEngine */
   NotifyClass d_notify;
 
-  /** Equality engine */
-  eq::EqualityEngine d_equalityEngine;
-
   /** Store a propagation to the bv solver */
   bool storePropagation(TNode literal);
 
@@ -88,6 +85,10 @@ class CoreSolver : public SubtheorySolver {
   bool d_preregisterCalled;
   bool d_checkCalled;
 
+  /** Pointer to the parent theory solver that owns this */
+  TheoryBV* d_bv;
+  /** Pointer to the equality engine of the parent */
+  eq::EqualityEngine* d_equalityEngine;
   /** Pointer to the extended theory module. */
   ExtTheory* d_extTheory;
 
@@ -100,36 +101,23 @@ class CoreSolver : public SubtheorySolver {
   Node getBaseDecomposition(TNode a);
   bool isCompleteForTerm(TNode term, TNodeBoolMap& seen);
   Statistics d_statistics;
-public:
- CoreSolver(context::Context* c, TheoryBV* bv, ExtTheory* extt);
- ~CoreSolver();
- bool isComplete() override { return d_isComplete; }
- void setMasterEqualityEngine(eq::EqualityEngine* eq);
- void preRegister(TNode node) override;
- bool check(Theory::Effort e) override;
- void explain(TNode literal, std::vector<TNode>& assumptions) override;
- bool collectModelInfo(TheoryModel* m, bool fullModel) override;
- Node getModelValue(TNode var) override;
- void addSharedTerm(TNode t) override
- {
-   d_equalityEngine.addTriggerTerm(t, THEORY_BV);
-  }
-  EqualityStatus getEqualityStatus(TNode a, TNode b) override
-  {
-    if (d_equalityEngine.areEqual(a, b)) {
-      // The terms are implied to be equal
-      return EQUALITY_TRUE;
-    }
-    if (d_equalityEngine.areDisequal(a, b, false)) {
-      // The terms are implied to be dis-equal
-      return EQUALITY_FALSE;
-    }
-    return EQUALITY_UNKNOWN;
-  }
-  bool hasTerm(TNode node) const { return d_equalityEngine.hasTerm(node); }
-  void addTermToEqualityEngine(TNode node) { d_equalityEngine.addTerm(node); }
+
+ public:
+  CoreSolver(context::Context* c, TheoryBV* bv, ExtTheory* extt);
+  ~CoreSolver();
+  bool needsEqualityEngine(EeSetupInfo& esi);
+  void finishInit();
+  bool isComplete() override { return d_isComplete; }
+  void preRegister(TNode node) override;
+  bool check(Theory::Effort e) override;
+  void explain(TNode literal, std::vector<TNode>& assumptions) override;
+  bool collectModelInfo(TheoryModel* m, bool fullModel) override;
+  Node getModelValue(TNode var) override;
+  void addSharedTerm(TNode t) override;
+  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
+  bool hasTerm(TNode node) const;
+  void addTermToEqualityEngine(TNode node);
   void enableSlicer();
-  eq::EqualityEngine * getEqualityEngine() { return &d_equalityEngine; }
 };
 
 
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 0a4499c11..ced320d92 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -113,13 +113,31 @@ TheoryBV::TheoryBV(context::Context* c,
 
 TheoryBV::~TheoryBV() {}
 
-void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
-  if (options::bitblastMode() == options::BitblastMode::EAGER)
+TheoryRewriter* TheoryBV::getTheoryRewriter() { return &d_rewriter; }
+
+bool TheoryBV::needsEqualityEngine(EeSetupInfo& esi)
+{
+  CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
+  if (core)
   {
-    return;
+    return core->needsEqualityEngine(esi);
   }
-  if (options::bitvectorEqualitySolver()) {
-    dynamic_cast<CoreSolver*>(d_subtheoryMap[SUB_CORE])->setMasterEqualityEngine(eq);
+  // otherwise we don't use an equality engine
+  return false;
+}
+
+void TheoryBV::finishInit()
+{
+  // these kinds are semi-evaluated in getModelValue (applications of this
+  // kind are treated as variables)
+  d_valuation.setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV);
+  d_valuation.setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
+
+  CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
+  if (core)
+  {
+    // must finish initialization in the core solver
+    core->finishInit();
   }
 }
 
@@ -185,16 +203,6 @@ Node TheoryBV::getBVDivByZero(Kind k, unsigned width) {
   Unreachable();
 }
 
-void TheoryBV::finishInit()
-{
-  // these kinds are semi-evaluated in getModelValue (applications of this
-  // kind are treated as variables)
-  TheoryModel* tm = d_valuation.getModel();
-  Assert(tm != nullptr);
-  tm->setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV);
-  tm->setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
-}
-
 TrustNode TheoryBV::expandDefinition(Node node)
 {
   Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node << ")" << std::endl;
@@ -582,16 +590,6 @@ void TheoryBV::propagate(Effort e) {
   }
 }
 
-
-eq::EqualityEngine * TheoryBV::getEqualityEngine() {
-  CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
-  if( core ){
-    return core->getEqualityEngine();
-  }else{
-    return NULL;
-  }
-}
-
 bool TheoryBV::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) {
   eq::EqualityEngine * ee = getEqualityEngine();
   if( ee ){
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index b0991c8b0..0e8877359 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -77,11 +77,18 @@ class TheoryBV : public Theory {
 
   ~TheoryBV();
 
-  TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
-
-  void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
-
+  //--------------------------------- initialization
+  /** get the official theory rewriter of this theory */
+  TheoryRewriter* getTheoryRewriter() override;
+  /**
+   * Returns true if we need an equality engine. If so, we initialize the
+   * information regarding how it should be setup. For details, see the
+   * documentation in Theory::needsEqualityEngine.
+   */
+  bool needsEqualityEngine(EeSetupInfo& esi) override;
+  /** finish initialization */
   void finishInit() override;
+  //--------------------------------- end initialization
 
   TrustNode expandDefinition(Node node) override;
 
@@ -99,8 +106,6 @@ class TheoryBV : public Theory {
 
   std::string identify() const override { return std::string("TheoryBV"); }
 
-  /** equality engine */
-  eq::EqualityEngine* getEqualityEngine() override;
   bool getCurrentSubstitution(int effort,
                               std::vector<Node>& vars,
                               std::vector<Node>& subs,