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.

7 files changed, 91 insertions, 68 deletions

diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index 0b1f18f5b..11d9a116c 100644
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -27,6 +27,7 @@ QuantifiersModules::QuantifiersModules()
       d_alpha_equiv(nullptr),
       d_inst_engine(nullptr),
       d_model_engine(nullptr),
+      d_builder(nullptr),
       d_bint(nullptr),
       d_qcf(nullptr),
       d_sg_gen(nullptr),
@@ -82,6 +83,22 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe,
   {
     d_model_engine.reset(new ModelEngine(qe, qs, qim, qr));
     modules.push_back(d_model_engine.get());
+    Trace("quant-init-debug")
+        << "Initialize model engine, mbqi : " << options::mbqiMode() << " "
+        << options::fmfBound() << std::endl;
+    if (useFmcModel())
+    {
+      Trace("quant-init-debug") << "...make fmc builder." << std::endl;
+      d_builder.reset(new fmcheck::FullModelChecker(qs, qr));
+    }
+    else
+    {
+      Trace("quant-init-debug")
+          << "...make default model builder." << std::endl;
+      d_builder.reset(new QModelBuilder(qs, qr));
+    }
+    // !!!!!!!!!!!!! temporary (project #15)
+    d_builder->finishInit(qe);
   }
   if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE)
   {
@@ -106,6 +123,13 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe,
   }
 }
 
+bool QuantifiersModules::useFmcModel()
+{
+  return options::mbqiMode() == options::MbqiMode::FMC
+         || options::mbqiMode() == options::MbqiMode::TRUST
+         || options::fmfBound();
+}
+
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h
index 3b460283b..c111eba25 100644
--- a/src/theory/quantifiers/quantifiers_modules.h
+++ b/src/theory/quantifiers/quantifiers_modules.h
@@ -21,6 +21,8 @@
 #include "theory/quantifiers/conjecture_generator.h"
 #include "theory/quantifiers/ematching/instantiation_engine.h"
 #include "theory/quantifiers/fmf/bounded_integers.h"
+#include "theory/quantifiers/fmf/full_model_check.h"
+#include "theory/quantifiers/fmf/model_builder.h"
 #include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/inst_strategy_enumerative.h"
 #include "theory/quantifiers/quant_conflict_find.h"
@@ -59,6 +61,9 @@ class QuantifiersModules
                   DecisionManager* dm,
                   std::vector<QuantifiersModule*>& modules);
 
+  /** Whether we use the full model check builder and corresponding model */
+  static bool useFmcModel();
+
  private:
   //------------------------------ quantifier utilities
   /** relevant domain */
@@ -70,6 +75,8 @@ 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 */
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index e054fd309..5bcc80eb0 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -16,17 +16,12 @@
 
 #include "theory/quantifiers/theory_quantifiers.h"
 
-#include "base/check.h"
-#include "expr/kind.h"
 #include "expr/proof_node_manager.h"
 #include "options/quantifiers_options.h"
-#include "theory/quantifiers/ematching/instantiation_engine.h"
-#include "theory/quantifiers/fmf/model_engine.h"
-#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/fmf/first_order_model_fmc.h"
+#include "theory/quantifiers/quantifiers_modules.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 #include "theory/valuation.h"
 
 using namespace CVC4::kind;
@@ -46,8 +41,7 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
       d_qstate(c, u, valuation, logicInfo),
       d_qreg(),
       d_treg(d_qstate, d_qreg),
-      d_qim(*this, d_qstate, pnm),
-      d_qengine(d_qstate, d_qreg, d_treg, d_qim, pnm)
+      d_qim(*this, d_qstate, pnm)
 {
   // Finish initializing the term registry by hooking it up to the inference
   // manager. This is required due to a cyclic dependency between the term
@@ -73,10 +67,42 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
   // use the inference manager as the official inference manager
   d_inferManager = &d_qim;
 
+  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())
+  {
+    if (QuantifiersModules::useFmcModel())
+    {
+      d_qmodel.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
+          d_qstate, d_qreg, d_treg, "FirstOrderModelFmc"));
+    }
+    else
+    {
+      d_qmodel.reset(new quantifiers::FirstOrderModel(
+          d_qstate, d_qreg, d_treg, "FirstOrderModel"));
+    }
+  }
+  else
+  {
+    d_qmodel.reset(new quantifiers::FirstOrderModel(
+        d_qstate, d_qreg, d_treg, "FirstOrderModel"));
+  }
+
+  // construct the quantifiers engine
+  d_qengine.reset(new QuantifiersEngine(
+      d_qstate, d_qreg, d_treg, d_qim, d_qmodel.get(), pnm));
+
+  //!!!!!!!!!!!!!! temporary (project #15)
+  d_qmodel->finishInit(d_qengine.get());
+
   // Set the pointer to the quantifiers engine, which this theory owns. This
   // pointer will be retreived by TheoryEngine and set to all theories
   // post-construction.
-  d_quantEngine = &d_qengine;
+  d_quantEngine = d_qengine.get();
 }
 
 TheoryQuantifiers::~TheoryQuantifiers() {
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index e9785fcea..9714ec718 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -20,6 +20,7 @@
 #define CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
 
 #include "expr/node.h"
+#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/proof_checker.h"
 #include "theory/quantifiers/quantifiers_inference_manager.h"
 #include "theory/quantifiers/quantifiers_registry.h"
@@ -87,13 +88,15 @@ class TheoryQuantifiers : public Theory {
   /** The quantifiers state */
   QuantifiersState d_qstate;
   /** The quantifiers registry */
-  quantifiers::QuantifiersRegistry d_qreg;
+  QuantifiersRegistry d_qreg;
+  /** extended model object */
+  std::unique_ptr<FirstOrderModel> d_qmodel;
   /** The term registry */
-  quantifiers::TermRegistry d_treg;
+  TermRegistry d_treg;
   /** The quantifiers inference manager */
   QuantifiersInferenceManager d_qim;
   /** The quantifiers engine, which lives here */
-  QuantifiersEngine d_qengine;
+  std::unique_ptr<QuantifiersEngine> d_qengine;
 };/* class TheoryQuantifiers */
 
 }/* CVC4::theory::quantifiers namespace */
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
 {
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 92b90c375..625bac40a 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -68,6 +68,7 @@ class QuantifiersEngine {
                     quantifiers::QuantifiersRegistry& qr,
                     quantifiers::TermRegistry& tr,
                     quantifiers::QuantifiersInferenceManager& qim,
+                    quantifiers::FirstOrderModel* qm,
                     ProofNodeManager* pnm);
   ~QuantifiersEngine();
   //---------------------- external interface
@@ -247,9 +248,7 @@ public:
   /** all triggers will be stored in this trie */
   std::unique_ptr<inst::TriggerTrie> d_tr_trie;
   /** extended model object */
-  std::unique_ptr<quantifiers::FirstOrderModel> d_model;
-  /** model builder */
-  std::unique_ptr<quantifiers::QModelBuilder> d_builder;
+  quantifiers::FirstOrderModel* d_model;
   /** equality query class */
   std::unique_ptr<quantifiers::EqualityQueryQuantifiersEngine> d_eq_query;
   /** instantiate utility */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 64181a8ee..efa3f9163 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -167,18 +167,19 @@ void TheoryEngine::finishInit()
     d_quantEngine = d_theoryTable[THEORY_QUANTIFIERS]->getQuantifiersEngine();
     Assert(d_quantEngine != nullptr);
   }
+  // finish initializing the quantifiers engine, which must come before
+  // initializing theory combination, since quantifiers engine may have a
+  // special model builder object
+  if (d_logicInfo.isQuantified())
+  {
+    d_quantEngine->finishInit(this, d_decManager.get());
+  }
   // initialize the theory combination manager, which decides and allocates the
   // equality engines to use for all theories.
   d_tc->finishInit();
   // get pointer to the shared solver
   d_sharedSolver = d_tc->getSharedSolver();
 
-  // finish initializing the quantifiers engine
-  if (d_logicInfo.isQuantified())
-  {
-    d_quantEngine->finishInit(this, d_decManager.get());
-  }
-
   // finish initializing the theories by linking them with the appropriate
   // utilities and then calling their finishInit method.
   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {