Add the central equality engine manager (#6893)

This class is responsible for setting up the central equality engine. It relies on a new static method Theory::usesCentralEqualityEngine, which will be refined in followup PRs.

This PR does not change the behavior, it only adds the class.

Further PRs will connect this class to CombinationEngine, make it optionally enabled, and make the remaining changes to TheoryEngine to make it compatible.

5 files changed, 465 insertions, 1 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index b6bf49ed8..796de9b4a 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -662,6 +662,8 @@ libcvc5_add_sources(
   theory/decision_strategy.h
   theory/ee_manager.cpp
   theory/ee_manager.h
+  theory/ee_manager_central.cpp
+  theory/ee_manager_central.h
   theory/ee_manager_distributed.cpp
   theory/ee_manager_distributed.h
   theory/ee_setup_info.h
diff --git a/src/theory/ee_manager_central.cpp b/src/theory/ee_manager_central.cpp
new file mode 100644
index 000000000..f98bce970
--- /dev/null
+++ b/src/theory/ee_manager_central.cpp
@@ -0,0 +1,306 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Equality engine manager for central equality engine architecture
+ */
+
+#include "theory/ee_manager_central.h"
+
+#include "theory/quantifiers_engine.h"
+#include "theory/shared_solver.h"
+#include "theory/theory_engine.h"
+#include "theory/theory_state.h"
+
+namespace cvc5 {
+namespace theory {
+
+EqEngineManagerCentral::EqEngineManagerCentral(TheoryEngine& te,
+                                               SharedSolver& shs,
+                                               ProofNodeManager* pnm)
+    : EqEngineManager(te, shs),
+      d_masterEENotify(nullptr),
+      d_masterEqualityEngine(nullptr),
+      d_centralEENotify(*this),
+      d_centralEqualityEngine(
+          d_centralEENotify, te.getSatContext(), "central::ee", true)
+{
+  for (TheoryId theoryId = theory::THEORY_FIRST;
+       theoryId != theory::THEORY_LAST;
+       ++theoryId)
+  {
+    d_theoryNotify[theoryId] = nullptr;
+  }
+  if (pnm != nullptr)
+  {
+    d_centralPfee.reset(new eq::ProofEqEngine(d_te.getSatContext(),
+                                              d_te.getUserContext(),
+                                              d_centralEqualityEngine,
+                                              pnm));
+    d_centralEqualityEngine.setProofEqualityEngine(d_centralPfee.get());
+  }
+}
+
+EqEngineManagerCentral::~EqEngineManagerCentral() {}
+
+void EqEngineManagerCentral::initializeTheories()
+{
+  context::Context* c = d_te.getSatContext();
+  // initialize the shared solver
+  EeSetupInfo esis;
+  if (d_sharedSolver.needsEqualityEngine(esis))
+  {
+    // the shared solver uses central equality engine
+    d_sharedSolver.setEqualityEngine(&d_centralEqualityEngine);
+  }
+  else
+  {
+    Unreachable() << "Expected shared solver to use equality engine";
+  }
+  // whether to use master equality engine as central
+  bool masterEqToCentral = true;
+  // setup info for each theory
+  std::map<TheoryId, EeSetupInfo> esiMap;
+  // set of theories that need equality engines
+  std::unordered_set<TheoryId> eeTheories;
+  const LogicInfo& logicInfo = d_te.getLogicInfo();
+  for (TheoryId theoryId = theory::THEORY_FIRST;
+       theoryId != theory::THEORY_LAST;
+       ++theoryId)
+  {
+    Theory* t = d_te.theoryOf(theoryId);
+    if (t == nullptr)
+    {
+      // theory not active, skip
+      continue;
+    }
+    if (!t->needsEqualityEngine(esiMap[theoryId]))
+    {
+      // theory said it doesn't need an equality engine, skip
+      continue;
+    }
+    // otherwise add it to the set of equality engine theories
+    eeTheories.insert(theoryId);
+    // if the logic has a theory that does not use central equality engine,
+    // we can't use the central equality engine for the master equality
+    // engine
+    if (theoryId != THEORY_QUANTIFIERS && logicInfo.isTheoryEnabled(theoryId)
+        && !Theory::usesCentralEqualityEngine(theoryId))
+    {
+      Trace("ee-central") << "Must use separate master equality engine due to "
+                          << theoryId << std::endl;
+      masterEqToCentral = false;
+    }
+  }
+
+  // initialize the master equality engine, which may be the central equality
+  // engine
+  if (logicInfo.isQuantified())
+  {
+    // construct the master equality engine
+    Assert(d_masterEqualityEngine == nullptr);
+    QuantifiersEngine* qe = d_te.getQuantifiersEngine();
+    Assert(qe != nullptr);
+    d_masterEENotify.reset(new quantifiers::MasterNotifyClass(qe));
+    if (!masterEqToCentral)
+    {
+      d_masterEqualityEngineAlloc.reset(new eq::EqualityEngine(
+          *d_masterEENotify.get(), d_te.getSatContext(), "master::ee", false));
+      d_masterEqualityEngine = d_masterEqualityEngineAlloc.get();
+    }
+    else
+    {
+      Trace("ee-central")
+          << "Master equality engine is the central equality engine"
+          << std::endl;
+      d_masterEqualityEngine = &d_centralEqualityEngine;
+      d_centralEENotify.d_newClassNotify.push_back(d_masterEENotify.get());
+    }
+  }
+
+  // allocate equality engines per theory
+  for (TheoryId theoryId = theory::THEORY_FIRST;
+       theoryId != theory::THEORY_LAST;
+       ++theoryId)
+  {
+    Trace("ee-central") << "Setup equality engine for " << theoryId
+                        << std::endl;
+    // always allocate an object in d_einfo here
+    EeTheoryInfo& eet = d_einfo[theoryId];
+    if (eeTheories.find(theoryId) == eeTheories.end())
+    {
+      Trace("ee-central") << "..." << theoryId << " does not need ee"
+                          << std::endl;
+      continue;
+    }
+    Theory* t = d_te.theoryOf(theoryId);
+    Assert(t != nullptr);
+    Assert(esiMap.find(theoryId) != esiMap.end());
+    EeSetupInfo& esi = esiMap[theoryId];
+    if (esi.d_useMaster)
+    {
+      Trace("ee-central") << "...uses master" << std::endl;
+      // the theory said it wants to use the master equality engine
+      eet.d_usedEe = d_masterEqualityEngine;
+      continue;
+    }
+    // set the notify
+    eq::EqualityEngineNotify* notify = esi.d_notify;
+    d_theoryNotify[theoryId] = notify;
+    // split on whether integrated, or whether asked for master
+    if (t->usesCentralEqualityEngine())
+    {
+      Trace("ee-central") << "...uses central" << std::endl;
+      // the theory uses the central equality engine
+      eet.d_usedEe = &d_centralEqualityEngine;
+      if (logicInfo.isTheoryEnabled(theoryId))
+      {
+        // add to vectors for the kinds of notifications
+        if (esi.needsNotifyNewClass())
+        {
+          d_centralEENotify.d_newClassNotify.push_back(notify);
+        }
+        if (esi.needsNotifyMerge())
+        {
+          d_centralEENotify.d_mergeNotify.push_back(notify);
+        }
+        if (esi.needsNotifyDisequal())
+        {
+          d_centralEENotify.d_disequalNotify.push_back(notify);
+        }
+      }
+      continue;
+    }
+    Trace("ee-central") << "...uses new" << std::endl;
+    eet.d_allocEe.reset(allocateEqualityEngine(esi, c));
+    // the theory uses the equality engine
+    eet.d_usedEe = eet.d_allocEe.get();
+    if (!masterEqToCentral)
+    {
+      // set the master equality engine of the theory's equality engine
+      eet.d_allocEe->setMasterEqualityEngine(d_masterEqualityEngine);
+    }
+  }
+
+  // set the master equality engine of the theory's equality engine
+  if (!masterEqToCentral)
+  {
+    d_centralEqualityEngine.setMasterEqualityEngine(d_masterEqualityEngine);
+  }
+}
+
+void EqEngineManagerCentral::notifyBuildingModel() {}
+
+EqEngineManagerCentral::CentralNotifyClass::CentralNotifyClass(
+    EqEngineManagerCentral& eemc)
+    : d_eemc(eemc), d_mNotify(nullptr), d_quantEngine(nullptr)
+{
+}
+
+bool EqEngineManagerCentral::CentralNotifyClass::eqNotifyTriggerPredicate(
+    TNode predicate, bool value)
+{
+  Trace("eem-central") << "eqNotifyTriggerPredicate: " << predicate
+                       << std::endl;
+  return d_eemc.eqNotifyTriggerPredicate(predicate, value);
+}
+
+bool EqEngineManagerCentral::CentralNotifyClass::eqNotifyTriggerTermEquality(
+    TheoryId tag, TNode t1, TNode t2, bool value)
+{
+  Trace("eem-central") << "eqNotifyTriggerTermEquality: " << t1 << " " << t2
+                       << value << ", tag = " << tag << std::endl;
+  return d_eemc.eqNotifyTriggerTermEquality(tag, t1, t2, value);
+}
+
+void EqEngineManagerCentral::CentralNotifyClass::eqNotifyConstantTermMerge(
+    TNode t1, TNode t2)
+{
+  Trace("eem-central") << "eqNotifyConstantTermMerge: " << t1 << " " << t2
+                       << std::endl;
+  d_eemc.eqNotifyConstantTermMerge(t1, t2);
+}
+
+void EqEngineManagerCentral::CentralNotifyClass::eqNotifyNewClass(TNode t)
+{
+  Trace("eem-central") << "...eqNotifyNewClass " << t << std::endl;
+  // notify all theories that have new equivalence class notifications
+  for (eq::EqualityEngineNotify* notify : d_newClassNotify)
+  {
+    notify->eqNotifyNewClass(t);
+  }
+}
+
+void EqEngineManagerCentral::CentralNotifyClass::eqNotifyMerge(TNode t1,
+                                                               TNode t2)
+{
+  Trace("eem-central") << "...eqNotifyMerge " << t1 << ", " << t2 << std::endl;
+  // notify all theories that have merge notifications
+  for (eq::EqualityEngineNotify* notify : d_mergeNotify)
+  {
+    notify->eqNotifyMerge(t1, t2);
+  }
+}
+
+void EqEngineManagerCentral::CentralNotifyClass::eqNotifyDisequal(TNode t1,
+                                                                  TNode t2,
+                                                                  TNode reason)
+{
+  Trace("eem-central") << "...eqNotifyDisequal " << t1 << ", " << t2
+                       << std::endl;
+  // notify all theories that have disequal notifications
+  for (eq::EqualityEngineNotify* notify : d_disequalNotify)
+  {
+    notify->eqNotifyDisequal(t1, t2, reason);
+  }
+}
+
+bool EqEngineManagerCentral::eqNotifyTriggerPredicate(TNode predicate,
+                                                      bool value)
+{
+  // always propagate with the shared solver
+  Trace("eem-central") << "...propagate " << predicate << ", " << value
+                       << " with shared solver" << std::endl;
+  return d_sharedSolver.propagateLit(predicate, value);
+}
+
+bool EqEngineManagerCentral::eqNotifyTriggerTermEquality(TheoryId tag,
+                                                         TNode a,
+                                                         TNode b,
+                                                         bool value)
+{
+  // propagate to theory engine
+  bool ok = d_sharedSolver.propagateLit(a.eqNode(b), value);
+  if (!ok)
+  {
+    return false;
+  }
+  // no need to propagate shared term equalities to the UF theory
+  if (tag == THEORY_UF)
+  {
+    return true;
+  }
+  // propagate shared equality
+  return d_sharedSolver.propagateSharedEquality(tag, a, b, value);
+}
+
+void EqEngineManagerCentral::eqNotifyConstantTermMerge(TNode t1, TNode t2)
+{
+  Node lit = t1.eqNode(t2);
+  Node conflict = d_centralEqualityEngine.mkExplainLit(lit);
+  Trace("eem-central") << "...explained conflict of " << lit << " ... "
+                       << conflict << std::endl;
+  d_sharedSolver.sendConflict(TrustNode::mkTrustConflict(conflict));
+  return;
+}
+
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/ee_manager_central.h b/src/theory/ee_manager_central.h
new file mode 100644
index 000000000..eb13b7820
--- /dev/null
+++ b/src/theory/ee_manager_central.h
@@ -0,0 +1,130 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Equality engine manager for central equality engine architecture
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__EE_MANAGER_CENTRAL__H
+#define CVC5__THEORY__EE_MANAGER_CENTRAL__H
+
+#include <map>
+#include <memory>
+
+#include "theory/ee_manager.h"
+#include "theory/quantifiers/master_eq_notify.h"
+#include "theory/uf/equality_engine.h"
+
+namespace cvc5 {
+namespace theory {
+
+/**
+ * The (central) equality engine manager. This encapsulates an architecture
+ * in which all applicable theories use a single central equality engine.
+ *
+ * This class is not responsible for actually initializing equality engines in
+ * theories (since this class does not have access to the internals of Theory).
+ * Instead, it is only responsible for the construction of the equality
+ * engine objects themselves. TheoryEngine is responsible for querying this
+ * class during finishInit() to determine the equality engines to pass to each
+ * theories based on getEeTheoryInfo.
+ *
+ * It also may allocate a "master" equality engine, which is intuitively the
+ * equality engine of the theory of quantifiers. If all theories use the
+ * central equality engine, then the master equality engine is the same as the
+ * central equality engine.
+ *
+ * The theories that use central equality engine are determined by
+ * Theory::usesCentralEqualityEngine.
+ *
+ * The main idea behind this class is to use a notification class on the
+ * central equality engine which dispatches *multiple* notifications to the
+ * theories that use the central equality engine.
+ */
+class EqEngineManagerCentral : public EqEngineManager
+{
+ public:
+  EqEngineManagerCentral(TheoryEngine& te,
+                         SharedSolver& shs,
+                         ProofNodeManager* pnm);
+  ~EqEngineManagerCentral();
+  /**
+   * Initialize theories. This method allocates unique equality engines
+   * per theories and connects them to a master equality engine.
+   */
+  void initializeTheories() override;
+  /** Notify this class that we are building the model. */
+  void notifyBuildingModel();
+
+ private:
+  /**
+   * Notify class for central equality engine. This class dispatches
+   * notifications from the central equality engine to the appropriate
+   * theory(s).
+   */
+  class CentralNotifyClass : public theory::eq::EqualityEngineNotify
+  {
+   public:
+    CentralNotifyClass(EqEngineManagerCentral& eemc);
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
+    bool eqNotifyTriggerTermEquality(TheoryId tag,
+                                     TNode t1,
+                                     TNode t2,
+                                     bool value) override;
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override;
+    void eqNotifyNewClass(TNode t) override;
+    void eqNotifyMerge(TNode t1, TNode t2) override;
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override;
+    /** Parent */
+    EqEngineManagerCentral& d_eemc;
+    /** List of notify classes that need new class notification */
+    std::vector<eq::EqualityEngineNotify*> d_newClassNotify;
+    /** List of notify classes that need merge notification */
+    std::vector<eq::EqualityEngineNotify*> d_mergeNotify;
+    /** List of notify classes that need disequality notification */
+    std::vector<eq::EqualityEngineNotify*> d_disequalNotify;
+    /** The model notify class */
+    eq::EqualityEngineNotify* d_mNotify;
+    /** The quantifiers engine */
+    QuantifiersEngine* d_quantEngine;
+  };
+  /** Notification when predicate gets value in central equality engine */
+  bool eqNotifyTriggerPredicate(TNode predicate, bool value);
+  bool eqNotifyTriggerTermEquality(TheoryId tag,
+                                   TNode t1,
+                                   TNode t2,
+                                   bool value);
+  /** Notification when constants are merged in central equality engine */
+  void eqNotifyConstantTermMerge(TNode t1, TNode t2);
+  /** The master equality engine notify class */
+  std::unique_ptr<quantifiers::MasterNotifyClass> d_masterEENotify;
+  /** The master equality engine. */
+  eq::EqualityEngine* d_masterEqualityEngine;
+  /** The master equality engine, if we allocated it */
+  std::unique_ptr<eq::EqualityEngine> d_masterEqualityEngineAlloc;
+  /** The central equality engine notify class */
+  CentralNotifyClass d_centralEENotify;
+  /** The central equality engine. */
+  eq::EqualityEngine d_centralEqualityEngine;
+  /** The proof equality engine for the central equality engine */
+  std::unique_ptr<eq::ProofEqEngine> d_centralPfee;
+  /**
+   * A table of from theory IDs to notify classes.
+   */
+  eq::EqualityEngineNotify* d_theoryNotify[theory::THEORY_LAST];
+};
+
+}  // namespace theory
+}  // namespace cvc5
+
+#endif /* CVC5__THEORY__EE_MANAGER_CENTRAL__H */
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 10c31edb7..891a3ca08 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -598,5 +598,26 @@ eq::EqualityEngine* Theory::getEqualityEngine()
   return d_equalityEngine;
 }
 
+bool Theory::usesCentralEqualityEngine() const
+{
+  return usesCentralEqualityEngine(d_id);
+}
+
+bool Theory::usesCentralEqualityEngine(TheoryId id)
+{
+  if (id == THEORY_BUILTIN)
+  {
+    return true;
+  }
+  if (options::eeMode() == options::EqEngineMode::DISTRIBUTED)
+  {
+    return false;
+  }
+  // Below are all theories with an equality engine except id ==THEORY_ARITH
+  return id == THEORY_UF || id == THEORY_DATATYPES || id == THEORY_BAGS
+         || id == THEORY_FP || id == THEORY_SETS || id == THEORY_STRINGS
+         || id == THEORY_SEP || id == THEORY_ARRAYS || id == THEORY_BV;
+}
+
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 4dbb7a436..7149d8e3f 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -307,13 +307,13 @@ class Theory {
    * class (see addSharedTerm).
    */
   virtual void notifySharedTerm(TNode n);
-
   /**
    * Notify in conflict, called when a conflict clause is added to TheoryEngine
    * by any theory (not necessarily this one). This signals that the theory
    * should suspend what it is currently doing and wait for backtracking.
    */
   virtual void notifyInConflict();
+
  public:
   //--------------------------------- initialization
   /**
@@ -876,6 +876,11 @@ class Theory {
    * E |= lit in the theory.
    */
   virtual std::pair<bool, Node> entailmentCheck(TNode lit);
+
+  /** uses central equality engine */
+  bool usesCentralEqualityEngine() const;
+  /** uses central equality engine (static) */
+  static bool usesCentralEqualityEngine(TheoryId id);
 };/* class Theory */
 
 std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level);