From: Andrew Reynolds Date: Tue, 17 Sep 2019 17:26:03 +0000 (-0500) Subject: Encapsulate relevant domain (#3293) X-Git-Tag: cvc5-1.0.0~3943 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2bb23eca6e3a239c33f5f4eb2dd0056de0738686;p=cvc5.git Encapsulate relevant domain (#3293) --- diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index 70d855f45..83856dfc4 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -32,8 +32,8 @@ using namespace inst; namespace quantifiers { -InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe) - : QuantifiersModule(qe) +InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe, RelevantDomain* rd) + : QuantifiersModule(qe), d_rd(rd) { } @@ -93,18 +93,17 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) // this stratification since effort level r=1 may be highly expensive in the // case where we have a quantified formula with many entailed instances. FirstOrderModel* fm = d_quantEngine->getModel(); - RelevantDomain* rd = d_quantEngine->getRelevantDomain(); unsigned nquant = fm->getNumAssertedQuantifiers(); std::map alreadyProc; for (unsigned r = rstart; r <= rend; r++) { - if (rd || r > 0) + if (d_rd || r > 0) { if (r == 0) { Trace("inst-alg") << "-> Relevant domain instantiate..." << std::endl; Trace("inst-alg-debug") << "Compute relevant domain..." << std::endl; - rd->compute(); + d_rd->compute(); Trace("inst-alg-debug") << "...finished" << std::endl; } else @@ -161,7 +160,6 @@ bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd) { return false; } - RelevantDomain* rd = d_quantEngine->getRelevantDomain(); unsigned final_max_i = 0; std::vector maxs; std::vector max_zero; @@ -178,7 +176,7 @@ bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd) unsigned ts; if (isRd) { - ts = rd->getRDomain(f, i)->d_terms.size(); + ts = d_rd->getRDomain(f, i)->d_terms.size(); } else { @@ -284,9 +282,9 @@ bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd) } else if (isRd) { - terms.push_back(rd->getRDomain(f, i)->d_terms[childIndex[i]]); + terms.push_back(d_rd->getRDomain(f, i)->d_terms[childIndex[i]]); Trace("inst-alg-rd") - << " " << rd->getRDomain(f, i)->d_terms[childIndex[i]] + << " " << d_rd->getRDomain(f, i)->d_terms[childIndex[i]] << std::endl; } else diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h index e58993182..48285c877 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -20,6 +20,7 @@ #include "context/context.h" #include "context/context_mm.h" #include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/relevant_domain.h" namespace CVC4 { namespace theory { @@ -61,7 +62,7 @@ namespace quantifiers { class InstStrategyEnum : public QuantifiersModule { public: - InstStrategyEnum(QuantifiersEngine* qe); + InstStrategyEnum(QuantifiersEngine* qe, RelevantDomain* rd); ~InstStrategyEnum() {} /** Needs check. */ bool needsCheck(Theory::Effort e) override; @@ -79,6 +80,8 @@ class InstStrategyEnum : public QuantifiersModule } private: + /** Pointer to the relevant domain utility of quantifiers engine */ + RelevantDomain* d_rd; /** process quantified formula * * q is the quantified formula we are constructing instances for. 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 d_inst_prop; + /** relevant domain */ + std::unique_ptr 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& 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(); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index e1fc742af..323158404 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -32,7 +32,6 @@ #include "theory/quantifiers/quant_epr.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/relevant_domain.h" #include "theory/quantifiers/skolemize.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_database.h" @@ -104,10 +103,6 @@ public: /** get trigger database */ inst::TriggerTrie* getTriggerDatabase() const; //---------------------- end utilities - //---------------------- utilities (TODO move these utilities #1163) - /** get relevant domain */ - quantifiers::RelevantDomain* getRelevantDomain() const; - //---------------------- end utilities private: /** * Maps quantified formulas to the module that owns them, if any module has @@ -314,8 +309,6 @@ public: std::unique_ptr d_tr_trie; /** extended model object */ std::unique_ptr d_model; - /** relevant domain */ - std::unique_ptr d_rel_dom; /** model builder */ std::unique_ptr d_builder; /** utility for effectively propositional logic */