Refactor initialization of quantifiers model and builder (#6175)

This is in preparation for breaking several circular dependencies and moving
the instantiate utility into the theory inference manager.

1 files changed, 8 insertions, 45 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index d6aaeed3f..7d5c4cf19 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -51,6 +51,7 @@ QuantifiersEngine::QuantifiersEngine(
     quantifiers::QuantifiersRegistry& qr,
     quantifiers::TermRegistry& tr,
     quantifiers::QuantifiersInferenceManager& qim,
+    quantifiers::FirstOrderModel* qm,
     ProofNodeManager* pnm)
     : d_qstate(qstate),
       d_qim(qim),
@@ -60,58 +61,20 @@ QuantifiersEngine::QuantifiersEngine(
       d_qreg(qr),
       d_treg(tr),
       d_tr_trie(new inst::TriggerTrie),
-      d_model(nullptr),
-      d_builder(nullptr),
-      d_eq_query(nullptr),
+      d_model(qm),
+      d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(qstate, qm)),
       d_instantiate(
           new quantifiers::Instantiate(this, qstate, qim, d_qreg, pnm)),
       d_skolemize(new quantifiers::Skolemize(d_qstate, d_pnm)),
       d_quants_prereg(qstate.getUserContext()),
       d_quants_red(qstate.getUserContext())
 {
-  //---- utilities
-  // quantifiers registry must come before the other utilities
+  // initialize the utilities
+  d_util.push_back(d_eq_query.get());
+  // quantifiers registry must come before the remaining utilities
   d_util.push_back(&d_qreg);
   d_util.push_back(tr.getTermDatabase());
-
   d_util.push_back(d_instantiate.get());
-
-  Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
-  Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
-
-  //---- end utilities
-
-  // Finite model finding requires specialized ways of building the model.
-  // We require constructing the model and model builder here, since it is
-  // required for initializing the CombinationEngine.
-  if (options::finiteModelFind() || options::fmfBound())
-  {
-    Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl;
-    if (options::mbqiMode() == options::MbqiMode::FMC
-        || options::mbqiMode() == options::MbqiMode::TRUST
-        || options::fmfBound())
-    {
-      Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
-      d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
-          qstate, qr, tr, "FirstOrderModelFmc"));
-      d_builder.reset(new quantifiers::fmcheck::FullModelChecker(qstate, qr));
-    }else{
-      Trace("quant-engine-debug") << "...make default model builder." << std::endl;
-      d_model.reset(
-          new quantifiers::FirstOrderModel(qstate, qr, tr, "FirstOrderModel"));
-      d_builder.reset(new quantifiers::QModelBuilder(qstate, qr));
-    }
-    d_builder->finishInit(this);
-  }else{
-    d_model.reset(
-        new quantifiers::FirstOrderModel(qstate, qr, tr, "FirstOrderModel"));
-  }
-  //!!!!!!!!!!!!!!!!!!!!! temporary (project #15)
-  d_model->finishInit(this);
-  // initialize the equality query
-  d_eq_query.reset(
-      new quantifiers::EqualityQueryQuantifiersEngine(qstate, d_model.get()));
-  d_util.insert(d_util.begin(), d_eq_query.get());
 }
 
 QuantifiersEngine::~QuantifiersEngine() {}
@@ -157,11 +120,11 @@ quantifiers::QuantifiersRegistry& QuantifiersEngine::getQuantifiersRegistry()
 
 quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const
 {
-  return d_builder.get();
+  return d_qmodules->d_builder.get();
 }
 quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const
 {
-  return d_model.get();
+  return d_model;
 }
 quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const
 {