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.

1 files changed, 6 insertions, 23 deletions

diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp
index 4e1aacbac..5b7bd1552 100644
--- a/src/theory/quantifiers/term_registry.cpp
+++ b/src/theory/quantifiers/term_registry.cpp
@@ -29,12 +29,12 @@ namespace quantifiers {
 
 TermRegistry::TermRegistry(QuantifiersState& qs, QuantifiersRegistry& qr)
     : d_presolve(qs.getUserContext(), true),
-      d_useFmcModel(false),
       d_presolveCache(qs.getUserContext()),
       d_termEnum(new TermEnumeration),
       d_termPools(new TermPools(qs)),
       d_termDb(new TermDb(qs, qr)),
-      d_sygusTdb(nullptr)
+      d_sygusTdb(nullptr),
+      d_qmodel(nullptr)
 {
   if (options::sygus() || options::sygusInst())
   {
@@ -44,27 +44,12 @@ TermRegistry::TermRegistry(QuantifiersState& qs, QuantifiersRegistry& qr)
   Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
   Trace("quant-engine-debug")
       << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
-  // Finite model finding requires specialized ways of building the model.
-  // We require constructing the model here, since it is required for
-  // initializing the CombinationEngine and the rest of quantifiers engine.
-  if ((options::finiteModelFind() || options::fmfBound())
-      && (options::mbqiMode() == options::MbqiMode::FMC
-          || options::mbqiMode() == options::MbqiMode::TRUST
-          || options::fmfBound()))
-  {
-    d_useFmcModel = true;
-    d_qmodel.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
-        qs, qr, *this, "FirstOrderModelFmc"));
-  }
-  else
-  {
-    d_qmodel.reset(
-        new quantifiers::FirstOrderModel(qs, qr, *this, "FirstOrderModel"));
-  }
 }
 
-void TermRegistry::finishInit(QuantifiersInferenceManager* qim)
+void TermRegistry::finishInit(FirstOrderModel* fm,
+                              QuantifiersInferenceManager* qim)
 {
+  d_qmodel = fm;
   d_termDb->finishInit(qim);
   if (d_sygusTdb.get())
   {
@@ -149,9 +134,7 @@ TermEnumeration* TermRegistry::getTermEnumeration() const
 
 TermPools* TermRegistry::getTermPools() const { return d_termPools.get(); }
 
-FirstOrderModel* TermRegistry::getModel() const { return d_qmodel.get(); }
-
-bool TermRegistry::useFmcModel() const { return d_useFmcModel; }
+FirstOrderModel* TermRegistry::getModel() const { return d_qmodel; }
 
 }  // namespace quantifiers
 }  // namespace theory