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

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() {