diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-05 18:09:24 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-05 18:09:24 -0500 |
| commit | 2283ee3b0327441c29caf26be977c1e4cd13c637 (patch) | |
| tree | 18bc8401f863fab8cb5f57d0c28a729650303d44 /src/theory/quantifiers/quantifiers_modules.h | |
| parent | dde3aac0417c10cdd1f8217f653bcdf95d94290c (diff) | |
Do not have quantifiers model inherit from theory model (#6493)
This is work towards making the initialization of theory engine, theory models, quantifiers engine more flexible.
This makes it so that the specialized quantifiers models classes (FirstOrderModel) do not inherit from TheoryModel. There is no longer any reason for this, since FirstOrderModel does not have any override methods.
As a result of this PR, there is only one kind of TheoryModel and it is constructed immediately when ModelManager is constructed.
This required refactoring the initialization of when FirstOrderModel is constructed in ModelBuilder classes in quantifiers.
This also avoids the need for casting TheoryModel to FirstOrderModel.
Diffstat (limited to 'src/theory/quantifiers/quantifiers_modules.h')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_modules.h | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h index 659be0381..f41e81f34 100644 --- a/src/theory/quantifiers/quantifiers_modules.h +++ b/src/theory/quantifiers/quantifiers_modules.h @@ -61,6 +61,7 @@ class QuantifiersModules QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, + QModelBuilder* builder, std::vector<QuantifiersModule*>& modules); private: @@ -74,8 +75,6 @@ class QuantifiersModules std::unique_ptr<InstantiationEngine> d_inst_engine; /** model engine */ std::unique_ptr<ModelEngine> d_model_engine; - /** model builder */ - std::unique_ptr<quantifiers::QModelBuilder> d_builder; /** bounded integers utility */ std::unique_ptr<BoundedIntegers> d_bint; /** Conflict find mechanism for quantifiers */ |