Refactor quantifiers engine initialization (#5813)

This is a step towards breaking up the quantifiers engine.

The key change is that QuantifiersEngine will not be passed as a pointer to the modules it contains. This PR makes it so that necessary modules take a QuantifiersState, which will eventually be extended as needed with additional query methods. For now, modules will take both until the dependencies on QuantifersEngine are removed.

This required that QuantifiersEngine now lives in TheoryQuantifiers, instead of in TheoryEngine, since the QuantifiersEngine must be initialized with QuantifiersState, which is a member of TheoryQuantifiers. Now, TheoryEngine retrieves the QuantifiersEngine from TheoryQuantifiers prior to finishing initialization on theories.

1 files changed, 7 insertions, 12 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 27ae0018e..16d68ea5c 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -169,8 +169,10 @@ void TheoryEngine::finishInit()
   // initialize the quantifiers engine
   if (d_logicInfo.isQuantified())
   {
-    // initialize the quantifiers engine
-    d_quantEngine = new QuantifiersEngine(this, *d_decManager.get(), d_pnm);
+    // get the quantifiers engine, which is initialized by the quantifiers
+    // theory
+    d_quantEngine = d_theoryTable[THEORY_QUANTIFIERS]->getQuantifiersEngine();
+    Assert(d_quantEngine != nullptr);
   }
   // initialize the theory combination manager, which decides and allocates the
   // equality engines to use for all theories.
@@ -178,10 +180,11 @@ void TheoryEngine::finishInit()
   // get pointer to the shared solver
   d_sharedSolver = d_tc->getSharedSolver();
 
-  // set the core equality engine on quantifiers engine
+  // finish initializing the quantifiers engine
   if (d_logicInfo.isQuantified())
   {
-    d_quantEngine->setMasterEqualityEngine(d_tc->getCoreEqualityEngine());
+    d_quantEngine->finishInit(
+        this, d_decManager.get(), d_tc->getCoreEqualityEngine());
   }
 
   // finish initializing the theories by linking them with the appropriate
@@ -205,12 +208,6 @@ void TheoryEngine::finishInit()
     // finish initializing the theory
     t->finishInit();
   }
-
-  // finish initializing the quantifiers engine
-  if (d_logicInfo.isQuantified())
-  {
-    d_quantEngine->finishInit();
-  }
 }
 
 ProofNodeManager* TheoryEngine::getProofNodeManager() const { return d_pnm; }
@@ -283,8 +280,6 @@ TheoryEngine::~TheoryEngine() {
     }
   }
 
-  delete d_quantEngine;
-
   smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime);
   smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded);
 }