diff options
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 54 |
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) |