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, 43 insertions, 11 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 5916390a6..2d1eeab84 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -44,21 +44,54 @@ namespace cvc5 {
 namespace theory {
 
 QuantifiersEngine::QuantifiersEngine(
-    quantifiers::QuantifiersState& qstate,
+    quantifiers::QuantifiersState& qs,
     quantifiers::QuantifiersRegistry& qr,
     quantifiers::TermRegistry& tr,
     quantifiers::QuantifiersInferenceManager& qim,
     ProofNodeManager* pnm)
-    : d_qstate(qstate),
+    : d_qstate(qs),
       d_qim(qim),
       d_te(nullptr),
       d_pnm(pnm),
       d_qreg(qr),
       d_treg(tr),
-      d_model(d_treg.getModel()),
-      d_quants_prereg(qstate.getUserContext()),
-      d_quants_red(qstate.getUserContext())
+      d_model(nullptr),
+      d_quants_prereg(qs.getUserContext()),
+      d_quants_red(qs.getUserContext())
 {
+  Trace("quant-init-debug")
+      << "Initialize model engine, mbqi : " << options::mbqiMode() << " "
+      << options::fmfBound() << 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::fmfBound()
+      || (options::finiteModelFind()
+          && (options::mbqiMode() == options::MbqiMode::FMC
+              || options::mbqiMode() == options::MbqiMode::TRUST)))
+  {
+    Trace("quant-init-debug") << "...make fmc builder." << std::endl;
+    d_builder.reset(
+        new quantifiers::fmcheck::FullModelChecker(qs, qim, qr, tr));
+  }
+  else
+  {
+    Trace("quant-init-debug") << "...make default model builder." << std::endl;
+    d_builder.reset(new quantifiers::QModelBuilder(qs, qim, qr, tr));
+  }
+  // set the model object
+  d_builder->finishInit();
+  d_model = d_builder->getModel();
+
+  // Finish initializing the term registry by hooking it up to the model and the
+  // inference manager. The former is required since theories are not given
+  // access to the model in their constructors currently.
+  // The latter is required due to a cyclic dependency between the term
+  // database and the instantiate module. Term database needs inference manager
+  // since it sends out lemmas when term indexing is inconsistent, instantiate
+  // needs term database for entailment checks.
+  d_treg.finishInit(d_model, &d_qim);
+
   // initialize the utilities
   d_util.push_back(d_model->getEqualityQuery());
   // quantifiers registry must come before the remaining utilities
@@ -72,10 +105,13 @@ QuantifiersEngine::~QuantifiersEngine() {}
 
 void QuantifiersEngine::finishInit(TheoryEngine* te)
 {
+  // connect the quantifiers model to the underlying theory model
+  d_model->finishInit(te->getModel());
   d_te = te;
   // Initialize the modules and the utilities here.
   d_qmodules.reset(new quantifiers::QuantifiersModules);
-  d_qmodules->initialize(d_qstate, d_qim, d_qreg, d_treg, d_modules);
+  d_qmodules->initialize(
+      d_qstate, d_qim, d_qreg, d_treg, d_builder.get(), d_modules);
   if (d_qmodules->d_rel_dom.get())
   {
     d_util.push_back(d_qmodules->d_rel_dom.get());
@@ -95,11 +131,7 @@ quantifiers::QuantifiersRegistry& QuantifiersEngine::getQuantifiersRegistry()
 
 quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const
 {
-  return d_qmodules->d_builder.get();
-}
-quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const
-{
-  return d_model;
+  return d_builder.get();
 }
 
 /// !!!!!!!!!!!!!! temporary (project #15)