Move quantifiers engine private to own file (#5053)

This moves and renames the quantifiers engine private class to QuantifiersModules. This is in preparation for using a standard state and inference manager object in TheoryQuantifiers and QuantifiersEngine.

Initializing quantifiers engine is a bit non-standard since it is intentionally a separate entity from TheoryQuantifiers. However, the plan is for quantifiers engine to use the state and inference manager of TheoryQuantifiers.

This PR additionally moves the initialization of quantifiers modules to a QuantifiersEngine::finishInit() method. The motivation for is that we do not have a state and inference manager during construction of QuantifiersEngine, since these will live in TheoryQuantifiers and will be passed to QuantifiersEngine during TheoryQuantifiers::finishInit. This means that we need a final pass to initialize quantifiers engine after these are initialized, which thus must come as the last step of TheoryEngine::finishInit.

The next PR will connect the state and inference manager to QuantifiersEngine during TheoryQuantifiers::finishInit. Then, the plan is for many of the core utilities in QuantifiersEngine to migrate to state/inference manager, and finally for its modules to reference state and inference manager instead of QuantifiersEngine.

1 files changed, 8 insertions, 3 deletions

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 72c0efce1..d5d9b1726 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -46,7 +46,10 @@ class TheoryEngine;
 namespace theory {
 
 class DecisionManager;
-class QuantifiersEnginePrivate;
+
+namespace quantifiers {
+class QuantifiersModules;
+}
 
 // TODO: organize this more/review this, github issue #1163
 class QuantifiersEngine {
@@ -60,6 +63,8 @@ class QuantifiersEngine {
   QuantifiersEngine(TheoryEngine* te, DecisionManager& dm,
                     ProofNodeManager* pnm);
   ~QuantifiersEngine();
+  /** finish initialize */
+  void finishInit();
   //---------------------- external interface
   /** get theory engine */
   TheoryEngine* getTheoryEngine() const;
@@ -381,9 +386,9 @@ public:
   std::unique_ptr<quantifiers::TermEnumeration> d_term_enum;
   //------------- end quantifiers utilities
   /**
-   * The private utility, which contains all of the quantifiers modules.
+   * The modules utility, which contains all of the quantifiers modules.
    */
-  std::unique_ptr<QuantifiersEnginePrivate> d_private;
+  std::unique_ptr<quantifiers::QuantifiersModules> d_qmodules;
   //------------- temporary information during check
   /** current effort level */
   QuantifiersModule::QEffort d_curr_effort_level;