diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-14 22:13:38 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-14 22:13:38 -0500 |
commit | 2b5902b1c54b1a4717273d501333dd37b8715f9d (patch) | |
tree | 13de163d456f1a5dfcf3e74c5f91e90d092addee /src/theory/quantifiers_engine.h | |
parent | 4a1b5ea5568fb6c688f407946f9a7fbb1cec3c31 (diff) |
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.
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r-- | src/theory/quantifiers_engine.h | 11 |
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; |