diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-17 12:26:03 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-17 12:26:03 -0500 |
commit | 2bb23eca6e3a239c33f5f4eb2dd0056de0738686 (patch) | |
tree | ffc149ba83f4ad739676859417451f34b69e54c7 /src/theory/quantifiers_engine.cpp | |
parent | a983ec175a7b7a2c247274735b9740c417114d94 (diff) |
Encapsulate relevant domain (#3293)
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 27 |
1 files changed, 11 insertions, 16 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 507d938b4..1eb62945b 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -47,6 +47,7 @@ class QuantifiersEnginePrivate public: QuantifiersEnginePrivate() : d_inst_prop(nullptr), + d_rel_dom(nullptr), d_alpha_equiv(nullptr), d_inst_engine(nullptr), d_model_engine(nullptr), @@ -66,6 +67,8 @@ class QuantifiersEnginePrivate //------------------------------ private quantifier utilities /** quantifiers instantiation propagator */ std::unique_ptr<quantifiers::InstPropagator> d_inst_prop; + /** relevant domain */ + std::unique_ptr<quantifiers::RelevantDomain> d_rel_dom; //------------------------------ end private quantifier utilities //------------------------------ quantifiers modules /** alpha equivalence */ @@ -100,14 +103,12 @@ class QuantifiersEnginePrivate * This constructs the above modules based on the current options. It adds * a pointer to each module it constructs to modules. This method sets * needsBuilder to true if we require a strategy-specific model builder - * utility, and needsRelDom to true if we require the relevant domain * utility. */ void initialize(QuantifiersEngine* qe, context::Context* c, std::vector<QuantifiersModule*>& modules, - bool& needsBuilder, - bool& needsRelDom) + bool& needsBuilder) { // add quantifiers modules if (options::quantConflictFind() || options::quantRewriteRules()) @@ -176,9 +177,9 @@ class QuantifiersEnginePrivate // full saturation : instantiate from relevant domain, then arbitrary terms if (options::fullSaturateQuant() || options::fullSaturateInterleave()) { - d_fs.reset(new quantifiers::InstStrategyEnum(qe)); + d_rel_dom.reset(new quantifiers::RelevantDomain(qe)); + d_fs.reset(new quantifiers::InstStrategyEnum(qe, d_rel_dom.get())); modules.push_back(d_fs.get()); - needsRelDom = true; } } }; @@ -190,7 +191,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c, this)), d_tr_trie(new inst::TriggerTrie), d_model(nullptr), - d_rel_dom(nullptr), d_builder(nullptr), d_qepr(nullptr), d_term_util(new quantifiers::TermUtil(this)), @@ -263,14 +263,13 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_inst_when_phase = 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() ); bool needsBuilder = false; - bool needsRelDom = false; - d_private->initialize(this, c, d_modules, needsBuilder, needsRelDom); + d_private->initialize(this, c, d_modules, needsBuilder); - if( needsRelDom ){ - d_rel_dom.reset(new quantifiers::RelevantDomain(this)); - d_util.push_back(d_rel_dom.get()); + if (d_private->d_rel_dom.get()) + { + d_util.push_back(d_private->d_rel_dom.get()); } - + // if we require specialized ways of building the model if( needsBuilder ){ Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl; @@ -324,10 +323,6 @@ EqualityQuery* QuantifiersEngine::getEqualityQuery() const { return d_eq_query.get(); } -quantifiers::RelevantDomain* QuantifiersEngine::getRelevantDomain() const -{ - return d_rel_dom.get(); -} quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const { return d_builder.get(); |