From 944cb8e5381c47ccc49955a19609921399bb9437 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 18 Aug 2020 13:05:04 -0500
Subject: [PATCH] Quantifiers engine stores a pointer to the master equality
 engine (#4908)

This is work towards a configurable approach to theory combination.

Setting the master equality engine in QuantifiersEngine mimics setting EqualityEngine in Theory.
---
 src/theory/quantifiers_engine.cpp |  8 +++++++-
 src/theory/quantifiers_engine.h   |  7 +++++++
 src/theory/theory_engine.cpp      | 15 ++++++++-------
 src/theory/theory_engine.h        |  2 --
 4 files changed, 22 insertions(+), 10 deletions(-)

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index eafcc1e85..9fdf7e7aa 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -176,6 +176,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
                                      context::UserContext* u,
                                      TheoryEngine* te)
     : d_te(te),
+      d_masterEqualityEngine(nullptr),
       d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c, this)),
       d_tr_trie(new inst::TriggerTrie),
       d_model(nullptr),
@@ -274,6 +275,11 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
 
 QuantifiersEngine::~QuantifiersEngine() {}
 
+void QuantifiersEngine::setMasterEqualityEngine(eq::EqualityEngine* mee)
+{
+  d_masterEqualityEngine = mee;
+}
+
 context::Context* QuantifiersEngine::getSatContext()
 {
   return d_te->theoryOf(THEORY_QUANTIFIERS)->getSatContext();
@@ -1258,7 +1264,7 @@ QuantifiersEngine::Statistics::~Statistics(){
 
 eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine() const
 {
-  return d_te->getMasterEqualityEngine();
+  return d_masterEqualityEngine;
 }
 
 Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index dd86c0db9..eca108587 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -49,6 +49,7 @@ class QuantifiersEnginePrivate;
 
 // TODO: organize this more/review this, github issue #1163
 class QuantifiersEngine {
+  friend class ::CVC4::TheoryEngine;
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
   typedef context::CDList<Node> NodeList;
   typedef context::CDList<bool> BoolList;
@@ -102,6 +103,10 @@ public:
   inst::TriggerTrie* getTriggerDatabase() const;
   //---------------------- end utilities
  private:
+  //---------------------- private initialization
+  /** Set the master equality engine */
+  void setMasterEqualityEngine(eq::EqualityEngine* mee);
+  //---------------------- end private initialization
   /**
    * Maps quantified formulas to the module that owns them, if any module has
    * specifically taken ownership of it.
@@ -316,6 +321,8 @@ public:
  private:
   /** reference to theory engine object */
   TheoryEngine* d_te;
+  /** Pointer to the master equality engine */
+  eq::EqualityEngine* d_masterEqualityEngine;
   /** vector of utilities for quantifiers */
   std::vector<QuantifiersUtil*> d_util;
   /** vector of modules for quantifiers */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 07c160058..e86a09112 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -159,6 +159,13 @@ void TheoryEngine::finishInit() {
     d_aloc_curr_model_builder = true;
   }
 
+  // set the core equality engine on quantifiers engine
+  if (d_logicInfo.isQuantified())
+  {
+    d_quantEngine->setMasterEqualityEngine(
+        d_eeDistributed->getMasterEqualityEngine());
+  }
+
   // finish initializing the theories
   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
     Theory* t = d_theoryTable[theoryId];
@@ -545,7 +552,7 @@ void TheoryEngine::check(Theory::Effort effort) {
     if( Theory::fullEffort(effort) && !d_inConflict && !needCheck()) {
       // case where we are about to answer SAT, the master equality engine,
       // if it exists, must be consistent.
-      eq::EqualityEngine* mee = getMasterEqualityEngine();
+      eq::EqualityEngine* mee = d_eeDistributed->getMasterEqualityEngine();
       if (mee != NULL)
       {
         AlwaysAssert(mee->consistent());
@@ -1807,12 +1814,6 @@ SharedTermsDatabase* TheoryEngine::getSharedTermsDatabase()
   return &d_sharedTerms;
 }
 
-theory::eq::EqualityEngine* TheoryEngine::getMasterEqualityEngine()
-{
-  Assert(d_eeDistributed != nullptr);
-  return d_eeDistributed->getMasterEqualityEngine();
-}
-
 void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* proofRecipe) {
   Assert(explanationVector.size() > 0);
 
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index aa23aa29b..bedd54130 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -738,8 +738,6 @@ public:
 
   SharedTermsDatabase* getSharedTermsDatabase();
 
-  theory::eq::EqualityEngine* getMasterEqualityEngine();
-
   SortInference* getSortInference() { return &d_sortInfer; }
 
   /** Prints the assertions to the debug stream */
-- 
2.30.2