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 /test/api/interactive_shell.py | |
| 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 'test/api/interactive_shell.py')
0 files changed, 0 insertions, 0 deletions