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.

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index eafcc1e851a8f1f32cce660a0a6b4262983d34d3..9fdf7e7aac2710d404452d64206ab98c166ae27e 100644 (file)
--- 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 dd86c0db9239e0e12c876b992073976706a4159a..eca10858761c3dd9da84ade52725cc37dec129eb 100644 (file)
--- 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 07c1600585f4d1b681f9d14aeaab3795d3be6278..e86a091127688c870c54d1b7712c43f7c2927cf0 100644 (file)
--- 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 aa23aa29b16682483b88d035b5767edaa6af597b..bedd5413032aec8aa1c598ff55474aba72820669 100644 (file)
--- 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 */