From bdc92b3bb257134c01c5e4818e97f71cbb66ab52 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 19 Mar 2021 13:05:47 -0500 Subject: [PATCH] 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. --- .../quantifiers/quantifiers_modules.cpp | 24 +++++++++ src/theory/quantifiers/quantifiers_modules.h | 7 +++ src/theory/quantifiers/theory_quantifiers.cpp | 48 +++++++++++++---- src/theory/quantifiers/theory_quantifiers.h | 9 ++-- src/theory/quantifiers_engine.cpp | 53 +++---------------- src/theory/quantifiers_engine.h | 5 +- src/theory/theory_engine.cpp | 13 ++--- 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& 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 d_inst_engine; /** model engine */ std::unique_ptr d_model_engine; + /** model builder */ + std::unique_ptr d_builder; /** bounded integers utility */ std::unique_ptr 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 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 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 d_tr_trie; /** extended model object */ - std::unique_ptr d_model; - /** model builder */ - std::unique_ptr d_builder; + quantifiers::FirstOrderModel* d_model; /** equality query class */ std::unique_ptr 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) { -- 2.30.2